Merge branch 'iris-proofmode' of gitlab.inria.fr:charguer/cfml into iris-proofmode

model/LambdaSepRO.v

@@ -1556,6 +1556,15 @@ Proof.
   apply normally_himpl. apply hwand_move_l. hsimpl. apply hwand_cancel.
 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 *)
 
@@ -1596,10 +1605,112 @@ Proof using.
 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.
+
+
+*)