Modified Hoare State Monad

HoareState.v

Set Implicit Arguments.

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

Require Import Program.
Require Import List.
Require Import Omega.

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 : Set) (pre : Pre) (a : Type) (post : Post a) : 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 _ => True
                                 end}.

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

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


Program Definition bind : forall a b P1 P2 Q1 Q2 B,
    (@HoareState B P1 a Q1) -> (forall (x : a), @HoareState B (P2 x) b (Q2 x)) ->
    @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 B a b P1 P2 Q1 Q2 c1 c2 s1 => match c1 s1 as y with
                                 | inl (x, s2) => c2 x s2
                                 | inr R => _
                                 end.
Next Obligation.
  eapply p.
  cbv in Heq_y.
  destruct c1.
  destruct x0.
  - simpl in y.
    destruct p0.
    inversion Heq_y.
    subst.
    auto.
  - simpl in y.
    inversion Heq_y.
Defined.
Next Obligation.
  destruct (c2 x).
  destruct x0.
  cbv in Heq_y.
  simpl in *.
  destruct p0.
  exists x s2.
  split;
    auto.
  destruct c1.
  destruct x0.
  destruct p0.
  simpl in *.
  inversion Heq_y.
  subst.
  auto.
  inversion Heq_y.
  simpl in *.
  auto.
Defined.
Next Obligation.
  simpl in *.
  inversion Heq_y.
  exists (@inr (a * st) Q2 R).
  auto.
Defined.

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

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

Program Definition put {B : Set} (x : st) : @HoareState B top unit (fun _ _ f => f = x) := 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.