Commit f16cb659 authored by charguer's avatar charguer

red via hoare rules

parent fcad5dc2
......@@ -387,6 +387,160 @@ Ltac simpl_abs := (* LATER: will be removed once [abs] computes *)
end.
(* ********************************************************************** *)
(* * New Reasoning Rules *)
Module New.
(* ---------------------------------------------------------------------- *)
(* ** Hoare rules *)
Definition hoare (t:trm) (H:hprop) (Q:val->hprop) :=
forall h, H h -> exists h' v, red h t h' v /\ Q v h'.
Lemma hoare_extract_hexists : forall t (A:Type) (J:A->hprop) Q,
(forall x, hoare t (J x) Q) ->
hoare t (hexists J) Q.
Proof using. introv M (x&HF). applys* M. Qed.
Lemma hoare_consequence : forall t H' Q' H Q,
hoare t H' Q' ->
H ==> H' ->
Q' ===> Q ->
hoare t H Q.
Proof using.
introv M MH MQ HF. forwards (h'&v&R&K): M h.
{ hhsimpl~. }
exists h' v. splits~. { hhsimpl. auto. }
Qed.
(*
Lemma hoare_consequence_post : forall t Q' H Q,
hoare t H Q' ->
Q' ===> Q ->
hoare t H Q.
Proof using.
intros. applys* hoare_consequence.
Qed.
*)
Lemma hoare_val : forall v H Q,
H ==> Q v ->
hoare (trm_val v) H Q.
Proof using.
introv M HF. exists h v. splits.
{ applys red_val. }
{ hhsimpl~. }
Qed.
Lemma hoare_fix : forall f x t1 H Q,
H ==> Q (val_fix f x t1) ->
hoare (trm_fix f x t1) H Q.
Proof using.
introv M HF. exists___. splits.
{ applys red_fix. }
{ hhsimpl~. }
Qed.
Lemma hoare_let : forall x t1 t2 H Q Q1,
hoare t1 H Q1 ->
(forall (X:val), hoare (subst x X t2) (Q1 X) Q) ->
hoare (trm_let x t1 t2) H Q.
Proof using.
introv M1 M2 HF.
lets~ (h1'&v1&R1&K1): (rm M1) h.
forwards* (h2'&v2&R2&K2): (rm M2) h1'.
exists h2' v2. splits~.
{ applys~ red_let R2. }
Qed.
(* ---------------------------------------------------------------------- *)
(* ** SL rules *)
Definition triple (t:trm) (H:hprop) (Q:val->hprop) :=
forall H', hoare t (H \* H') (Q \*+ \Top \*+ H').
Lemma rule_extract_hexists : forall t (A:Type) (J:A->hprop) Q,
(forall x, triple t (J x) Q) ->
triple t (hexists J) Q.
Proof using.
introv M. intros HF. rewrite hstar_hexists.
applys hoare_extract_hexists. intros. applys* M.
Qed.
Lemma rule_consequence : forall t H' Q' H Q,
H ==> H' ->
triple t H' Q' ->
Q' ===> Q ->
triple t H Q.
Proof using.
introv MH M MQ. intros HF. applys hoare_consequence M.
{ hchanges MH. }
{ intros x. hchanges (MQ x). }
Qed.
Lemma rule_frame : forall t H Q H',
triple t H Q ->
triple t (H \* H') (Q \*+ H').
Proof using.
introv M. intros HF.
applys hoare_consequence (M (HF \* H')).
{ hsimpl. }
{ hsimpl. }
Qed.
Lemma rule_htop_post : forall t H Q,
triple t H (Q \*+ \Top) ->
triple t H Q.
Proof using.
introv M. unfolds triple. intros HF.
applys hoare_consequence (M HF).
{ hsimpl. }
{ intros x. hsimpl. }
Qed.
Lemma rule_htop_pre : forall t H Q,
triple t H Q ->
triple t (H \* \Top) Q.
Proof using.
introv M. applys rule_htop_post. applys~ rule_frame.
Qed.
Lemma rule_val : forall v H Q,
H ==> Q v ->
triple (trm_val v) H Q.
Proof using.
introv M. intros HF. applys hoare_val. { hchanges M. }
Qed.
Lemma rule_fix : forall f x t1 H Q,
H ==> Q (val_fix f x t1) ->
triple (trm_fix f x t1) H Q.
Proof using.
introv M. intros HF. applys hoare_fix. { hchanges M. }
Qed.
Lemma rule_let : forall x t1 t2 H Q Q1,
triple t1 H Q1 ->
(forall (X:val), triple (subst x X t2) (Q1 X) Q) ->
triple (trm_let x t1 t2) H Q.
Proof using.
introv M1 M2. intros HF. applys hoare_let.
{ applys M1. }
{ intros X. simpl. applys hoare_consequence.
{ applys M2. }
{ hsimpl. }
{ intros v. hsimpl. } }
Qed.
End New.
(* ********************************************************************** *)
(* * Reasoning Rules *)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment