Commit 0e67038d authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Prove rule_let_ramified_frame_read_only.

parent 2f5df25a
......@@ -1589,138 +1589,22 @@ Proof using.
clear M. applys* rule_ramified_frame_read_only_core.
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.
Lemma rule_let_ramified_frame_read_only : forall x t1 t2 H1 H Q1 Q Q',
triple t1 H1 Q1 ->
H ==> ROFrame H1 (Q1 \---* Q') ->
(forall (X:val), triple (subst x X t2) (Q' X) Q) ->
triple (trm_let x t1 t2) H Q.
Proof.
intros x t1 t2 H1 H Q1 Q Q' Ht1 IMPL Ht2L.
eapply rule_consequence; [apply IMPL| |auto].
apply rule_extract_hexists. intros H2. rewrite <-hstar_assoc.
eapply rule_let.
- rewrite hstar_comm. apply rule_frame_read_only, _.
eapply rule_consequence; [|apply Ht1|auto].
hchange (hwand_cancel (RO H2) H1); [|hsimpl]. hsimpl.
apply RO_covariant, normally_erase.
- intros X. eapply rule_consequence; [|apply Ht2L|auto].
hchange (hwand_cancel H2 (Q1 \---* Q')).
{ rewrite hstar_comm. apply himpl_frame_r, normally_erase. }
hchange (qwand_himpl_hwand X). hchange (hwand_cancel (Q1 X) (Q' X)). hsimpl.
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