Another Modified Hoare State Monad

HoareState2.v

Set Implicit Arguments.

Unset Strict Implicit.
Unset Printing Implicit Defensive.
Require Import LibTactics.

Require Import Program.

Section hoare_state_monad.

Variable st : Set.

Definition Pre : Type := st -> Prop.

Definition Post (a : Type) : Type := st -> a -> st -> Prop.

Program Definition HoareState (E : Type) (pre : Pre) (a : Type) (post : Post a) (post' : E -> st -> Prop) : Type :=
  forall i : {t : st | pre t}, {c : sum (a * st) E |
                                       match c with
                                       | inl (x, f) => post (proj1_sig i) x f
                                       | inr b => post' b (proj1_sig i)
                                       end}.

Definition top : Pre := fun st => True.

Program Definition ret {B : Type} (a : Type) : forall x,
    @HoareState B top a (fun i y f => i = f /\ y = x) (fun _ _ => False) := fun x s => exist _ (inl (x, s)) _.

Program Definition bind : forall a b P1 P2 Q1 Q2 B BQ1 BQ2,
    (@HoareState B P1 a Q1 BQ1) -> (forall (x : a), @HoareState B (P2 x) b (Q2 x) BQ2) ->
    @HoareState B (fun s1 => P1 s1 /\ forall x s2, Q1 s1 x s2 -> P2 x s2) 
                b
                (fun s1 y s3 => exists x, exists s2, Q1 s1 x s2 /\ Q2 x s2 y s3)
                (fun y s1 => exists x, exists s2, BQ1 x s1 \/ BQ2 x s2) :=
  fun a b P1 P2 Q1 Q2 B BQ1 BQ2 c1 c2 s1 => match c1 s1 as y with
                                 | inl (x, s2) => match c2 x s2 with
                                                 | inl (x', s3) => inl (x', s3)
                                                 | inr R' => inr R'
                                                 end
                                 | inr R => inr R
                                 end.
Next Obligation.
  eapply p0; eauto.
  cbv in Heq_y.
  destruct c1.
  destruct x0.
  - simpl in y.
    destruct p1.
    inversion Heq_y.
    subst.
    auto.
  - simpl in y.
    inversion Heq_y.
Defined.
Next Obligation.
  simpl in *.
  destruct c2.
  cases x0.
  - cbv in Heq_y.
    simpl in *.
    subst.
    destruct p1.
    exists x s2.
    split;
      auto.
    destruct c1.
    destruct x0.
    destruct p1.
    simpl in *.
    inversion Heq_y.
    subst.
    auto.
    inversion Heq_y.
    inversion Heq_anonymous.
    subst.
    auto.
  - cbv in Heq_y.
    inversion Heq_anonymous.
Defined.
Next Obligation.
  destruct c2.
  destruct x0.
  simpl in *.
  inversion Heq_anonymous.
  simpl in *.
  exists b0 s2.
  right.
  auto.
Defined.
Next Obligation.
  destruct c1.
  destruct x.
  simpl in *.
  inversion Heq_y.
  simpl in *.
  exists b0 s1.
  left.
  auto.
Defined.

Program Definition failT {B : Type} (b : B) (A : Type) : @HoareState B top A (fun _ _ _ => True) (fun _ _ => True) := fun s => exist _ (inr b) _.

Program Definition get {B : Type} : @HoareState B top st (fun i x f => i = f /\ x = i) (fun _ _ => False) := fun s => exist _ (inl (s, s)) _.

Program Definition put {B : Type} (x : st) : @HoareState B top unit (fun _ _ f => f = x) (fun _ _ => False) := fun  _ => exist _ (inl (tt, x)) _.

End hoare_state_monad.

Infix ">>=" := bind (right associativity, at level 71).

Delimit Scope monad_scope with monad.
Open Scope monad_scope.

Notation "x <- m ; p" := (m >>= fun x => p)%monad
    (at level 68, right associativity,
     format "'[' x  <-  '[' m ']' ; '//' '[' p ']' ']'") : monad_scope.

Close Scope monad_scope.