Commit ebc91424 authored by charguer's avatar charguer

wand and wp

parent 187cefbb
(*
Definition is_extractible F :=
forall A (J:A->hprop) Q,
(forall x, F (J x) Q) ->
F (hexists J) Q.
*)
Lemma rule_if_val : forall v t1 t2 H Q,
triple (If v = val_int 0 then t2 else t1) H Q ->
triple (trm_if v t1 t2) H Q.
......
......@@ -268,6 +268,11 @@ Definition hpure (P:Prop) : hprop :=
Notation "\[ P ]" := (hpure P)
(at level 0, P at level 99, format "\[ P ]") : heap_scope.
(** Forall *)
Definition hforall (A : Type) (J : A -> hprop) : hprop :=
fun h => forall x, J x h.
(** Disjunction *)
Definition hor (H1 H2 : hprop) : hprop :=
......@@ -283,10 +288,17 @@ Definition hand (H1 H2 : hprop) : hprop :=
Definition hwand (H1 H2 : hprop) : hprop :=
hexists (fun (H:hprop) => H \* (hpure (H \* H1 ==> H2))).
(** Forall *)
Notation "H1 \--* H2" := (hwand H1 H2)
(at level 43) : heap_scope.
(** Magic wand for post-conditions *)
Definition qwand A (Q1 Q2:A->hprop) :=
hforall (fun x => hwand (Q1 x) (Q2 x)).
Notation "Q1 \---* Q2" := (qwand Q1 Q2)
(at level 43) : heap_scope.
Definition hforall (A : Type) (J : A -> hprop) : hprop :=
fun h => forall x, J x h.
(* ---------------------------------------------------------------------- *)
(* ** Additional notation for entailment *)
......
......@@ -1170,6 +1170,72 @@ Tactic Notation "hchange" constr(E1) constr(E2) constr(E3) :=
(* ********************************************************************** *)
(* * Properties of the magic wand *)
(* ---------------------------------------------------------------------- *)
(* ** Magic wand on [hprop] *)
Lemma hwand_himpl_r : forall H1 H2 H2',
H2 ==> H2' ->
(H1 \--* H2) ==> (H1 \--* H2').
Proof using.
intros. unfold hwand. hsimpl ;=> H3 M. hchanges~ M.
Qed.
Lemma hwand_himpl_l : forall H1' H1 H2,
H1' ==> H1 ->
(H1 \--* H2) ==> (H1' \--* H2).
Proof using.
intros. unfold hwand. hsimpl ;=> H3 M. hchanges M. hchanges H.
Qed.
Lemma hwand_cancel : forall H1 H2,
H1 \* (H1 \--* H2) ==> H2.
Proof using.
intros. unfold hwand. hsimpl ;=> H3 M. hchanges M.
Qed.
Lemma hwand_cancel_part : forall H1 H2 H3,
H1 \* ((H1 \* H2) \--* H3) ==> (H2 \--* H3).
Proof using.
intros. unfold hwand. hsimpl ;=> H4 M. hchanges M.
Qed.
Lemma hwand_cancel_part_trans : forall H1 H2 H3 H4,
H2 ==> ((H1 \* H3) \--* H4) ->
H1 \* H2 ==> (H3 \--* H4).
Proof using.
introv M. hchange (>> himpl_frame_r H1 M).
rew_heap. apply hwand_cancel_part.
Qed.
Arguments hwand_cancel : clear implicits.
Arguments hwand_cancel_part : clear implicits.
(* ---------------------------------------------------------------------- *)
(* ** Magic wand on [A->hprop] *)
Lemma qwand_himpl_hwand: forall A (x:A) (Q1 Q2:A->hprop),
(Q1 \---* Q2) ==> (Q1 x \--* Q2 x).
Proof using.
intros. unfold qwand, hforall. intros h. auto.
Qed.
Arguments qwand_himpl_hwand [ A ].
Lemma qwand_cancel : forall A (Q1 Q2:A->hprop),
Q1 \*+ (Q1 \---* Q2) ===> Q2.
Proof using.
intros. intros x.
hchange (qwand_himpl_hwand x Q1 Q2).
hchanges (hwand_cancel (Q1 x)).
Qed.
(* ********************************************************************** *)
(* * Predicates [local] and [is_local] for structural operations *)
......@@ -1304,6 +1370,18 @@ Proof using.
hchange WQ. hsimpl.
Qed.
(** Ramified frame rule *)
Lemma local_ramified_frame : forall Q1 H1 F H Q,
is_local F ->
F H1 Q1 ->
H ==> H1 \* (Q1 \---* Q) ->
F H Q.
Proof using.
introv L M W. applys~ local_frame (Q1 \---* Q) M.
hchanges qwand_cancel.
Qed.
(** Weakening on pre and post from [local] *)
Lemma local_weaken : forall H' Q' F H Q,
......@@ -1448,6 +1526,18 @@ Proof using.
{ hsimpl. }
Qed.
(** Extraction of pure facts from the pre-condition under local *)
Lemma local_extract_prop : forall F H Q P,
is_local F ->
(H ==> H \* \[P]) ->
(P -> F H Q) ->
F H Q.
Proof using.
introv L M N. applys~ local_weaken_pre M. rewrite hstar_comm.
applys~ local_extract_hprop.
Qed.
(** Extraction of contradictions from the pre-condition under local *)
Lemma local_extract_false : forall F H Q,
......@@ -1752,6 +1842,49 @@ Tactic Notation "xchange_show" "<-" constr(E) :=
(* ********************************************************************** *)
(* * Weakest-preconditions *)
(* ---------------------------------------------------------------------- *)
(* ** Definition of the weakest precondition for a formula *)
Definition wp (B : Type) (F:hprop->(B->hprop)->Prop) (Q:B->hprop) : hprop :=
Hexists (H:hprop), H \* \[F H Q].
Lemma wp_equiv : forall B (F:~~B) H Q,
is_local F -> (* in fact, only requires weaken-pre and extract-hexists rules to hold *)
F H Q <-> (H ==> wp F Q).
Proof using.
intros. unfold wp. iff M.
{ hsimpl. rew_heap~. }
{ applys~ local_weaken_pre M. xpull~. }
Qed.
Lemma wp_conseq : forall B (F:~~B) Q1 Q2,
is_local F ->
Q1 ===> Q2 ->
wp F Q1 ==> wp F Q1.
Proof using.
introv L W. unfold wp. hpull ;=> H1 M. hsimpl. xapplys M.
Qed.
Lemma wp_frame : forall B (F:~~B) H Q,
is_local F ->
(wp F Q) \* H ==> wp F (Q \*+ H).
Proof using.
introv L. unfold wp. hpull ;=> H1 M. hsimpl. xapplys M.
Qed.
Lemma wp_absorb : forall B (F:~~B) Q,
is_local F ->
wp F Q \* \Top ==> wp F Q.
Proof using.
introv L. unfold wp. hpull ;=> H1 M. hsimpl. xapplys M.
Qed.
(* ********************************************************************** *)
(* * Tactics for representation predicates *)
......@@ -1933,6 +2066,8 @@ Tactic Notation "xunfolds" constr(E) :=
Tactic Notation "xunfolds" constr(E) "at" constr(n) :=
xunfold E at n; xunfolds_post tt.
(* ********************************************************************** *)
(* * Instantiating Iris Proof Mode *)
......
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