diff --git a/model/LambdaWP.v b/model/LambdaWP.v index 7b04a8ecf733af421589c204c6038f3dd77ec646..e93fff22fb8972ff84f728ac2334cf03110314f6 100644 --- a/model/LambdaWP.v +++ b/model/LambdaWP.v @@ -33,6 +33,73 @@ Global Instance Inhab_formula : Inhab formula. Proof using. apply (Inhab_of_val (fun _ => \[])). Qed. +(* ---------------------------------------------------------------------- *) +(* ** Definition of [local] for WP *) + +(** The [local] predicate is a predicate transformer that typically + applies to a WP, and allows for application + of the frame rule, of the rule of consequence, of the garbage + collection rule, and of extraction rules for existentials and + pure facts. *) + +Definition local (F:formula) : formula := + fun Q => Hexists Q', F Q' \* (Q' \---* (Q \*+ \Top)). + +(** The [is_local] predicate asserts that a predicate is subject + to all the rules that the [local] predicate transformer supports. *) + +Definition is_local (F:formula) := + F = local F. + + +(* ---------------------------------------------------------------------- *) +(* ** Properties of [local] for WP *) + +Lemma local_weaken : forall Q' F H Q, + is_local F -> + H ==> F Q -> + Q ===> Q' -> + H ==> F Q'. +Proof using. + introv L M W. rewrite (rm L). hchanges (rm M). + unfold local. hsimpl Q. + hchanges (>> qwand_of_qimpl W). + (* TODO: simplify *) + applys qwand_himpl_r. hsimpl. +Qed. + +Lemma local_top : forall F H Q, + is_local F -> + H ==> F (Q \*+ \Top) -> + H ==> F Q. +Proof using. + introv L M. rewrite L. hchanges (rm M). unfold local. + hsimpl (Q \*+ \Top). hchanges (qwand_of_qimpl (Q \*+ \Top)). + hsimpl. +Qed. + +Lemma local_frame : forall H1 H2 F H Q, + is_local F -> + H ==> H1 \* H2 -> + H1 ==> F (fun x => H2 \--* Q x) -> + H ==> F Q. +Proof using. + introv L W M. rewrites (rm L). hchanges (rm W). hchanges (rm M). + unfold local. hsimpl (fun x : val => H2 \--* Q x). (* TODO: simplify *) + (* TODO: needs hqwand *) + applys qwand_move_l. intros x. hchanges (hwand_cancel H2). +Qed. + +Lemma local_frame_top : forall H1 H2 F H Q, + is_local F -> + H ==> H1 \* H2 -> + H1 ==> F (fun x => H2 \--* Q x \* \Top) -> + H ==> F Q. +Proof using. + introv L W M. applys* local_top. applys* local_frame. +Qed. + + (* ---------------------------------------------------------------------- *) (* ** Definition of CF blocks *) @@ -75,6 +142,7 @@ Definition WP_for (v1 v2:val) (F3:int->formula) : formula := fun Q => *) + (* ---------------------------------------------------------------------- *) (* ** Definition of the CF generator *) @@ -85,16 +153,16 @@ Definition WP_for (v1 v2:val) (F3:int->formula) : formula := fun Q => Definition WP_def WP (t:trm) := match t with - | trm_val v => WP_val v - | trm_var x => WP_fail (* unbound variable *) - | trm_fun x t1 => WP_val (val_fun x t1) - | trm_fix f x t1 => WP_val (val_fix f x t1) - | trm_if t0 t1 t2 => WP_if (WP t0) (WP t1) (WP t2) - | trm_seq t1 t2 => WP_seq (WP t1) (WP t2) - | trm_let x t1 t2 => WP_let (WP t1) (fun X => WP (subst x X t2)) - | trm_app t1 t2 => wp (triple t) - | trm_while t1 t2 => WP_fail (* TODO *) - | trm_for x t1 t2 t3 => WP_fail (* TODO *) + | trm_val v => local (WP_val v) + | trm_var x => local (WP_fail) (* unbound variable *) + | trm_fun x t1 => local (WP_val (val_fun x t1)) + | trm_fix f x t1 => local (WP_val (val_fix f x t1)) + | trm_if t0 t1 t2 => local (WP_if (WP t0) (WP t1) (WP t2)) + | trm_seq t1 t2 => local (WP_seq (WP t1) (WP t2)) + | trm_let x t1 t2 => local (WP_let (WP t1) (fun X => WP (subst x X t2))) + | trm_app t1 t2 => local (wp (triple t)) + | trm_while t1 t2 => local (WP_fail) (* TODO *) + | trm_for x t1 t2 t3 => local (WP_fail) (* TODO *) end. Definition WP := FixFun WP_def. diff --git a/model/SepTactics.v b/model/SepTactics.v index 03e958c6d783746f45daa03c9a742d2447493aa6..611c393657343d394aea7f91b8e654918abbc0a1 100644 --- a/model/SepTactics.v +++ b/model/SepTactics.v @@ -1234,6 +1234,19 @@ Qed. Arguments hwand_cancel : clear implicits. Arguments hwand_cancel_part : clear implicits. +Lemma hwand_of_himpl : forall (H1 H2:hprop), + H1 ==> H2 -> + \[] ==> (H1 \--* H2). +Proof using. + introv M. unfold hwand. hsimpl \[]. hchanges M. +Qed. + +Lemma hstar_hwand : forall H1 H2 H3, + (H1 \--* H2) \* H3 ==> H1 \--* (H2 \* H3). +Proof using. + intros. unfold hwand. hsimpl ;=> H4 M. hchanges M. +Qed. + (* ---------------------------------------------------------------------- *) (* ** Magic wand on [A->hprop] *) @@ -1263,6 +1276,32 @@ Proof using. hchanges (hwand_cancel_part H). Qed. +Lemma qwand_of_qimpl : forall A (Q1 Q2:A->hprop), + Q1 ===> Q2 -> + \[] ==> (Q1 \---* Q2). +Proof using. + introv M. unfold qwand, hforall. intros h N x. hhsimpl. + hchanges (hwand_of_himpl (M x)). +Qed. + +Arguments qwand_of_qimpl [A]. + +Lemma qwand_himpl_r : forall A (Q1 Q2 Q2':A->hprop), + Q2 ===> Q2' -> + (Q1 \---* Q2) ==> (Q1 \---* Q2'). +Proof using. + introv M. unfold qwand. applys himpl_hforall. + intros x. applys* hwand_himpl_r. +Qed. + +Lemma qwand_move_l : forall H A (Q1 Q2:A->hprop), + Q1 \*+ H ===> Q2 -> + H ==> (Q1 \---* Q2). +Proof using. + introv M. unfold qwand. intros h Hh x. hhsimpl. + applys hwand_move_l. hchanges M. +Qed. + (* ********************************************************************** *) (* * Predicates [local] and [is_local] for structural operations *)