Commit 60374f02 authored by charguer's avatar charguer

local for wp

parent a2bd2a04
......@@ -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.
......
......@@ -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 *)
......
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