Commit 0cd44cb8 authored by charguer's avatar charguer

normally_investigate

parent d76039be
......@@ -1482,6 +1482,15 @@ Proof using.
Qed.
Lemma rule_frame_read_only_with_frame' : forall t H1 H2 H3 Q1,
triple t (H1 \* RO H2) Q1 ->
triple t (H1 \* normally H2 \* normally H3) ((Q1 \*+ normally H2) \*+ H3).
Proof using.
introv M. lets N: rule_frame_read_only_with_frame H3 M.
applys rule_consequence N. { hsimpl. } { intros x. hsimpl. apply normally_erase. }
Qed.
(* ---------------------------------------------------------------------- *)
(* ** Ramified read-only frame rule *)
......@@ -1526,10 +1535,110 @@ Qed.
(* ---------------------------------------------------------------------- *)
(* todo: move *)
Lemma hwand_hstar_l : forall H1 H2 H3,
(H1 \--* (H2 \--* H3)) ==> ((H1 \* H2) \--* H3).
Proof using.
intros. unfold hwand. hsimpl ;=> H4 M. hchange M.
hpull ;=> H5 N. hchanges N.
Qed.
(* todo: reprove [hwand_cancel_part] using the above. *)
(**
Lemma normally_hwand : forall A {IA:Inhab A} (Q1 Q2:A->hprop),
normally (Q1 \---* Q2) ==> normally Q1 \---* normally Q2.
Proof using.
intros. unfold hwand. rewrite normally_hexists. hpull ;=> H3.
rewrite normally_hstar, normally_hpure. hsimpl (normally H3).
intros M. rewrite <- normally_hstar. applys~ normally_himpl.
Qed.
*)
(* ---------------------------------------------------------------------- *)
Arguments normally_hwand : clear implicits.
Definition ROFrame H1 H2 :=
Hexists H, normally H \* (RO H \--* H1) \* normally (H \--* H2).
Lemma rule_ramified_frame_read_only_ROFrame : forall t H Q H' Q',
triple t H' Q' ->
H ==> ROFrame H' (normally (Q' \---* Q)) ->
triple t H Q.
Proof using.
introv M W. applys rule_ramified_frame_read_only M.
hchange W. unfold ROFrame. hpull ;=> H2. hsimpl H2.
hchanges (normally_hwand H2 (normally (Q' \---* Q))).
skip_rewrite (H' \* RO \Top = H'). (* TODO: easy to remove top before *)
hsimpl.
unfold qwand at 2. rewrite normally_hforall; try typeclass.
(*
applys rule_consequence;
[ | applys rule_ramified_frame_read_only_core (rm M); reflexivity | ].
*)
Abort.
(* ---------------------------------------------------------------------- *)
(*
Definition ROFrame' H1 H2 :=
Hexists H, normally H2 \* (RO H \--* H1) \* (H \--* H2).
Lemma ROFrame'_himpl_ROFRame : forall H1 H2,
ROFrame' H1 (normally H2) ==> ROFrame H1 H2.
Lemma rule_ramified_frame_read_only : forall t H Q H' Q',
triple t H' Q' ->
H ==> ROFrame H (normally (Q' \---* Q)) ->
triple t H Q.
Proof using.Qed.
Lemma hwand_normally : forall H1 H2,
H1 \--* normally H2 ==> normally (H1 \--* H2).
Proof using.
intros. intros h (H3&(h1&h2&N1&N2&N3&N4)). split.
{ exists H3. exists h1 h2. splits~. hhsimpl.
introv M. hchanges M. applys normally_erase. }
Abort.
Definition hqwand (H:hprop) A (Q:A->hprop) :=
hforall (fun x => hwand H (Q x)).
Notation "H \--*+ Q" := (hqwand H Q)
(at level 43) : heap_scope.
Lemma hwand_normally : forall H1 H2,
H1 \--* normally H2 ==> normally (H1 \--* H2).
Proof using.
intros. intros h (H3&(h1&h2&N1&N2&N3&N4)). split.
{ exists H3. exists h1 h2. splits~. hhsimpl.
introv M. hchanges M. applys normally_erase. }
{ lets (N2a&N2b): hpure_inv N2. lets: N2a ()
unfold hwand
Qed.
Lemma hwand_normally' : forall H1 H2,
normally H1 \--* normally H2 ==> normally (H1 \--* H2).
Proof using.
Qed.
*)
......
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