Work on ROFrame.

model/LambdaSepRO.v

@@ -1476,55 +1476,113 @@ 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) \*+ normally H3).
 Proof using.
-  introv M. rewrite <- hstar_assoc. applys rule_frame. 
+  introv M. rewrite <- hstar_assoc. applys rule_frame.
   { applys~ rule_frame_read_only'. }
   { applys normal_normally. }
 Qed.
 
+(* ---------------------------------------------------------------------- *)
+(* ** Definition ofe the ROFrame connective *)
+
+Definition ROFrame (H1 H2 : hprop) :=
+  Hexists H3, normally H3 \* (RO(H3) \--* H1) \* normally(H3 \--* H2).
+
+Lemma ROFrame_himpl : forall H1 H2 H1' H2',
+  H1 ==> H1' -> H2 ==> H2' -> ROFrame H1 H2 ==> ROFrame H1' H2'.
+Proof.
+  unfold ROFrame. intros H1 H2 H1' H2' MONO1 MONO2.
+  apply himpl_hexists_l=>H3. apply himpl_hexists_r with H3. hsimpl.
+  eapply himpl_trans; [apply himpl_frame_r|apply himpl_frame_l].
+  { auto using  hwand_himpl_r. } { auto using normally_himpl, hwand_himpl_r. }
+Qed.
+
+Lemma ROFrame_intro : forall H1 H2,
+  H1 \* normally H2 ==> ROFrame H1 H2.
+Proof.
+  intros. unfold ROFrame. apply himpl_hexists_r with \[].
+  rewrite normally_hempty, RO_empty, hstar_hempty_l.
+  eapply himpl_trans; [apply himpl_frame_r|apply himpl_frame_l].
+  - apply normally_himpl. apply hwand_move_l. hsimpl.
+  - apply hwand_move_l. hsimpl.
+Qed.
+
+Lemma ROFrame_frame_l : forall H1 H2 H3,
+  H1 \* ROFrame H2 H3 ==> ROFrame (H1 \* H2) H3.
+Proof.
+  intros. unfold ROFrame. hpull=>HF. apply himpl_hexists_r with HF. hsimpl.
+  apply hwand_move_l. hsimpl. apply hwand_cancel.
+Qed.
+
+Lemma ROFrame_frame_lr : forall H1 H2 H3,
+  normal H1 ->
+  H1 \* ROFrame H2 H3 ==> ROFrame (RO(H1) \* H2) (H1 \* H3).
+Proof.
+  intros H1 H2 H3 NORM.
+  unfold ROFrame. hpull=>HF. apply himpl_hexists_r with (H1 \* HF).
+  hchange (normally_intro NORM). rewrite normally_hstar. hsimpl.
+  eapply himpl_trans; [apply himpl_frame_r|apply himpl_frame_l].
+  - apply hwand_move_l. hchange (RO_star H1 HF). hsimpl.
+    rewrite hstar_comm. apply hwand_cancel.
+  - apply normally_himpl, hwand_move_l. hsimpl. apply hwand_cancel.
+Qed.
+
+Lemma ROFrame_frame_lr' : forall H1 H2 H3,
+  normal H1 ->
+  H1 \* ROFrame H2 (H1 \--* H3) ==> ROFrame (RO(H1) \* H2) H3.
+Proof.
+  intros H1 H2 H3 NORM. hchange (@ROFrame_frame_lr H1 H2 (H1 \--* H3) NORM).
+  hsimpl. apply ROFrame_himpl; [hsimpl|]. apply hwand_cancel.
+Qed.
+
+Lemma ROFrame_frame_r : forall H1 H2 H3,
+  normal H1 ->
+  H1 \* ROFrame H2 H3 ==> ROFrame H2 (H1 \* H3).
+Proof.
+  intros H1 H2 H3 NORM.
+  unfold ROFrame. hpull=>HF. apply himpl_hexists_r with HF. hsimpl.
+  hchange (normally_intro NORM). rewrite hstar_hempty_r, <-normally_hstar.
+  apply normally_himpl. apply hwand_move_l. hsimpl. apply hwand_cancel.
+Qed.
 
 (* ---------------------------------------------------------------------- *)
 (* ** Ramified read-only frame rule *)
 
 Lemma rule_ramified_frame_read_only_core : forall H2 t H Q H' Q',
   triple t H' Q' ->
-  H = normally H2 \* (RO H2 \--* H') \* normally ((Q' \*+ normally H2) \---* Q) ->
+  H = normally H2 \* (RO H2 \--* H') \* normally (H2 \--* (Q' \---* Q)) ->
   triple t H Q.
 Proof using.
   introv M W. subst H.
-  forwards K: rule_frame_read_only_with_frame t (RO H2 \--* H') H2 ((Q' \*+ normally H2) \---* Q) Q'.
+  forwards K: rule_frame_read_only_with_frame t (RO H2 \--* H') H2 (H2 \--* (Q' \---* Q)) Q'.
   { applys~ rule_consequence M. hchanges (hwand_cancel (RO H2)). }
-  { clear M. applys rule_consequence (rm K). 
+  { clear M. applys rule_consequence (rm K).
     { hsimpl. }
-    { intros x. hchange (>> normally_erase (Q' \*+ normally H2 \---* Q)).
-      hchange (>> qwand_cancel_part (normally H2)).
-      hchange (qwand_himpl_hwand x). hchanges (hwand_cancel (Q' x)). } }
+    { intros x. hchange (>> normally_erase (H2 \--* (Q' \---* Q))).
+      hchange (>> normally_erase H2). hchange (>> hwand_cancel H2 (Q' \---* Q)).
+      hsimpl. apply qwand_cancel. } }
 Qed.
 
 Lemma rule_ramified_frame_read_only : forall t H Q H' Q',
   triple t H' Q' ->
-  H ==> Hexists H2, normally H2 
-                 \* (RO H2 \--* (H' \* RO \Top))
-                 \* normally ((Q' \*+ normally H2) \---* Q) ->
+  H ==> ROFrame H' (Q' \---* Q) ->
   triple t H Q.
 Proof using.
   introv M W. applys~ rule_consequence Q (rm W).
   applys rule_extract_hexists. intros H2.
-  asserts M': (triple t (H' \* RO \Top) Q').
-  { applys* rule_consequence (H' \* \Top). hsimpl.
-    applys~ rule_htop_pre. }
+  asserts M': (triple t H' Q').
+  { applys* rule_consequence H'. }
   clear M. applys* rule_ramified_frame_read_only_core.
 Qed.
 
 Lemma rule_ramified_frame_read_only_direct : forall H2 t H Q H' Q',
   triple t H' Q' ->
-  H ==> normally H2 \* (RO H2 \--* (H' \* RO \Top)) \* normally ((Q' \*+ normally H2) \---* Q) ->
+  H ==> normally H2 \* (RO H2 \--* H') \*
+        normally (H2 \--* (Q' \---* Q)) ->
   triple t H Q.
 Proof using.
-  introv M W. applys rule_ramified_frame_read_only M. hchanges W.
+  introv M W. applys rule_ramified_frame_read_only M. unfold ROFrame. hchanges W.
 Qed.
 
-
-
 (* ---------------------------------------------------------------------- *)
 
 

model/SepTactics.v

@@ -2234,11 +2234,17 @@ Hint Extern 2 (envs_entails _ (_ \* _)) => progress iFrame : iFrame.
 
 Hint Extern 3 (envs_entails _ ?P) => is_evar P; iAccu.
 Hint Extern 3 (envs_entails _ (?P _)) => is_evar P; iAccu.
+
 Hint Extern 0 (envs_entails _ (\[_] \* _)) => iSplitR.
 Hint Extern 0 (envs_entails _ (\[_] ∗ _)) => iSplitR.
 Hint Extern 0 (envs_entails _ (_ \* \[_])) => iSplitL.
 Hint Extern 0 (envs_entails _ (_ ∗ \[_])) => iSplitL.
 
+Hint Extern 0 (envs_entails _ (\[] \* _)) => iSplitR.
+Hint Extern 0 (envs_entails _ (\[] ∗ _)) => iSplitR.
+Hint Extern 0 (envs_entails _ (_ \* \[])) => iSplitL.
+Hint Extern 0 (envs_entails _ (_ ∗ \[])) => iSplitL.
+
 (** * Specific Proofmode instances about hpure and htop. *)
 
 Global Instance htop_absorbing : Absorbing \Top.