Weaker ROFrame connective.

model/LambdaSepRO.v

@@ -1373,20 +1373,16 @@ Proof.
   intros. hchanges normally_hwand. rewrite normally_Normal_eq; auto.
 Qed.
 
-Lemma normally_hwand_or_hwand_false : forall H1 H2,
-  H1 \--* normally H2 ==> hor (normally (H1 \--* H2)) (H1 \--* \[False]).
+Lemma normally_hwand_hstar : forall H1 H2,
+  H1 \* (H1 \--* normally H2) ==> H1 \* normally (H1 \--* H2).
 Proof.
-  intros H1 H2 h Hh. tests Hhr : (h^r = fmap_empty).
-  - left. split; [|auto]. destruct Hh as [H0 Hh]. exists H0.
-    revert Hh. rewrite hstar_comm, hstar_pure. intros [??].
-    rewrite hstar_comm, hstar_pure. split; [|auto]. hchanges H.
-    apply normally_erase.
-  - right. eexists (eq h). rewrite hstar_comm, hstar_pure. split; [|auto].
-    destruct Hh as [H0 Hh]. rewrite hstar_comm, hstar_pure in Hh.
-    destruct Hh as [IMPL Hh]. intros h' (h1 & h2 & ? & Hh2 & Hh12 & ?).
-    destruct Hhr. subst. destruct (IMPL (h1 \u h2)) as (_ & EMP); last first.
-    { eapply fmap_union_eq_empty_inv_l. rewrite <- heap_union_r; eauto. }
-    eexists _, _. eauto.
+  intros H1 H2 h (h1 & h2 & Hh1 & Hh2 & ? & ->). eexists _, _.
+  split; [eauto|split; [|eauto]]; []. destruct Hh2 as [H0 IMPL].
+  rewrite hstar_comm, hstar_pure in IMPL. destruct IMPL as [IMPL ?]. split.
+  { exists H0. rewrite hstar_comm, hstar_pure.
+    eauto using himpl_trans, normally_erase. }
+  destruct (IMPL (h1 \u h2)). { eexists _, _; eauto. }
+  eapply fmap_union_eq_empty_inv_r. rewrite <- heap_union_r; eauto.
 Qed.
 
 (** Alternative definition of [Normal] in terms of [normally] *)
@@ -1490,14 +1486,22 @@ Lemma rule_frame_read_only_with_frame : forall t H1 H2 H3 Q1,
 Proof using.
   introv M. rewrite <- hstar_assoc. applys rule_frame.
   { applys~ rule_frame_read_only'. }
-  { applys normal_normally. }
+  { applys Normal_normally. }
+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.
 
 (* ---------------------------------------------------------------------- *)
 (* ** Definition ofe the ROFrame connective *)
 
 Definition ROFrame (H1 H2 : hprop) :=
-  Hexists H3, normally H3 \* (RO(H3) \--* H1) \* normally(H3 \--* H2).
+  Hexists H3, normally H3 \* (RO(H3) \--* H1) \* (H3 \--* H2).
 
 Lemma ROFrame_himpl : forall H1 H2 H1' H2',
   H1 ==> H1' -> H2 ==> H2' -> ROFrame H1 H2 ==> ROFrame H1' H2'.
@@ -1505,17 +1509,16 @@ 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. }
+  { auto using  hwand_himpl_r. } { auto using hwand_himpl_r. }
 Qed.
 
 Lemma ROFrame_intro : forall H1 H2,
-  H1 \* normally H2 ==> ROFrame H1 H2.
+  H1 \* 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.
+  eapply himpl_trans; [apply himpl_frame_r|apply himpl_frame_l];
+    apply hwand_move_l; hsimpl.
 Qed.
 
 Lemma ROFrame_frame_l : forall H1 H2 H3,
@@ -1526,7 +1529,7 @@ Proof.
 Qed.
 
 Lemma ROFrame_frame_lr : forall H1 H2 H3,
-  normal H1 ->
+  Normal H1 ->
   H1 \* ROFrame H2 H3 ==> ROFrame (RO(H1) \* H2) (H1 \* H3).
 Proof.
   intros H1 H2 H3 NORM.
@@ -1535,11 +1538,11 @@ Proof.
   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.
+  - apply hwand_move_l. hsimpl. apply hwand_cancel.
 Qed.
 
 Lemma ROFrame_frame_lr' : forall H1 H2 H3,
-  normal H1 ->
+  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).
@@ -1547,45 +1550,36 @@ Proof.
 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.
+  intros H1 H2 H3. unfold ROFrame. hpull=>HF. apply himpl_hexists_r with HF.
+  hsimpl. 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 *)
 
 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 (H2 \--* (Q' \---* Q)) ->
+  H = normally H2 \* (RO H2 \--* H') \* (H2 \--* normally (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 (H2 \--* (Q' \---* Q)) Q'.
+  introv M W. subst H. applys rule_consequence; [| |auto].
+  { hchange (>> normally_hwand_hstar (normally H2) (Q' \---* Q)); [|auto]; [].
+    rewrite hstar_comm. apply himpl_frame_r, hwand_himpl_l, normally_erase. }
+  forwards K: rule_frame_read_only_with_frame t
+          (RO H2 \--* H') H2 (normally H2 \--* (Q' \---* Q)) Q'.
   { applys~ rule_consequence M. hchanges (hwand_cancel (RO H2)). }
   { clear M. applys rule_consequence (rm K).
     { hsimpl. }
-    { intros x. hchange (>> normally_erase (H2 \--* (Q' \---* Q))).
-      hchange (>> normally_erase H2). hchange (>> hwand_cancel H2 (Q' \---* Q)).
+    { intros x. hchange (>> normally_erase (normally H2 \--* (Q' \---* Q))).
+      hchange (>> hwand_cancel (normally 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 ==> ROFrame H' (Q' \---* Q) ->
+  H ==> ROFrame H' (normally (Q' \---* Q)) ->
   triple t H Q.
 Proof using.
   introv M W. applys~ rule_consequence Q (rm W).
@@ -1595,15 +1589,6 @@ Proof using.
   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') \*
-        normally (H2 \--* (Q' \---* Q)) ->
-  triple t H Q.
-Proof using.
-  introv M W. applys rule_ramified_frame_read_only M. unfold ROFrame. hchanges W.
-Qed.
-
 (* ---------------------------------------------------------------------- *)
 (* todo: move *)
 

model/SepTactics.v

@@ -1372,7 +1372,6 @@ Proof using.
   hchanges (hwand_cancel_part H).
 Qed.
 
-
 (* ********************************************************************** *)
 (* * Predicates [local] and [is_local] for structural operations *)