Beautify proofs.

model/ExampleROProofMode.v

@@ -244,13 +244,9 @@ Proof using.
   xletfun => F HF.
   ram_apply_let (rule_box_up2 (fun (x:int) => (x + n)%Z) n).
   { intros. xdef. xletapp rule_box_get => m ->.
-    ram_apply rule_add. { iIntros "?".
-
-iSplitR.  iModIntro. auto. auto with iFrame. } } (* TODO : improve. *)
+    ram_apply rule_add. { auto with iFrame. } } (* TODO : improve. *)
   { iIntros "Hq Hp". iDestruct (Box_fold with "[$Hq $Hp]") as "$".
     auto with iFrame. }
   unlock. xpull=> u /= _. apply rule_htop_post. ram_apply rule_box_get.
-  math_rewrite (2 * (n + n) = 4 * n)%Z.
-iIntros "$ !>". auto 10 with iFrame.        (* TODO: improve. *)
-
+  math_rewrite (2 * (n + n) = 4 * n)%Z. auto with iFrame.
 Qed.

model/LambdaSepRO.v

@@ -1851,6 +1851,29 @@ Instance ROFrame_from_and (P Q : hprop) :
   FromAnd (P ∗ Q) P Q → FromAnd (ROFrame P Q) P Q | 1000.
 Proof. rewrite /FromAnd=>->. apply ROFrame_intro. Qed.
 
+(** Setup iModIntro to work with normally. *)
+
+Lemma modality_normally_mixin :
+  modality_mixin normally MIEnvId
+                 (MIEnvTransform (λ P Q : hprop, TCAnd (TCEq P Q) (Normal P))).
+Proof.
+  split; simpl.
+  - by intros P h [-> ?].
+  - by intros P Q [-> ?]; apply normally_intro.
+  - by rewrite normally_hempty.
+  - by intros P Q ?; f_equiv.
+  - by intros P Q; rewrite normally_hstar.
+Qed.
+Definition modality_normally :=
+  Modality _ modality_normally_mixin.
+Instance from_modal_normally P :
+  FromModal modality_normally (normally P) (normally P) P.
+Proof. by rewrite /FromModal. Qed.
+(* Low priority to force annotation. *)
+Instance from_modal_abs_normally P :
+  FromModal modality_normally (normally P) (<absorb> normally P) P | 100.
+Proof. by rewrite /FromModal -bi.absorbingly_intro. Qed.
+
 (** Frame instances *)
 
 Class MakeNormally (P Q : hprop) :=
@@ -1922,32 +1945,38 @@ Hint Mode FrameOrWand ! - - : typeclass_instances.
 Instance frame_or_wand_frame (R P Q : hprop) :
   Frame false R P Q → FrameOrWand R P Q | 0.
 Proof. done. Qed.
-Instance frame_or_wand_wand (R P : hprop) :
-  FrameOrWand R P (R -∗ P) | 1.
+Instance frame_or_wand_normally_wand (R P : hprop) :
+  Normal R →
+  FrameOrWand R (normally P) (normally (R -∗ P)%I) | 1.
+Proof.
+  unfold FrameOrWand. iIntros (?) "[? H] !>". rewrite normally_erase.
+  by iApply "H".
+Qed.
+(* The following default instance will not be used if P is of the form
+   [normally X]. *)
+Lemma frame_or_wand_wand (R P : hprop) :
+  FrameOrWand R P (R -∗ P).
 Proof. unfold FrameOrWand. iIntros "[? H]". by iApply "H". Qed.
+Hint Extern 1 (FrameOrWand _ ?P _) =>
+  lazymatch P with
+  | normally _ => fail
+  | _ => simple eapply @frame_or_wand_wand
+  end
+: typeclass_instances.
 
-(* We try all these framing schemes, in this order:
-   TODO : there are computations to share. *)
-
+(* We try all these framing schemes, in this order: *)
 (* 1st step: if we are tying to frame an RO, we first see if it is
    needed on the LHS. If so, then we also make it available on the
-   RHS. We do this only if the RHS is not of the form [normally P],
-   because otherwise we cannot get rid of this RO permission. *)
-Lemma frame_roframe_ro_lr p (R P P' Q Q' S : hprop) :
+   RHS. *)
+Instance frame_roframe_ro_lr p (R P P' Q Q' S : hprop) :
   DupFrameRO R P P' → FrameOrWand (RO R) Q Q' →
-  MakeROFrame P' Q' S → Frame p (RO R) (ROFrame P Q) S.
+  MakeROFrame P' Q' S → Frame p (RO R) (ROFrame P Q) S | 1.
 Proof.
   rewrite /Frame /DupFrameRO /FrameOrWand /MakeROFrame
           bi.affinely_persistently_if_elim=><- <- ->.
   assert (HR:=@RO_duplicatable R). unfold duplicatable in HR. rewrite {1}HR.
   by rewrite /bi_sep /= hstar_assoc ROFrame_frame_r ROFrame_frame_l.
 Qed.
-Hint Extern 1 (Frame _ (RO _) (ROFrame _ ?Q) _) =>
-  lazymatch Q with
-  | normally _ => fail
-  | _ => simple eapply @frame_roframe_ro_lr
-  end
-: typeclass_instances.
 
 (* 2nd step: we try to frame on the LHS. *)
 Instance frame_roframe_l p (R P P' Q S : hprop) :
@@ -1970,29 +1999,6 @@ Proof.
   rewrite /DupFrameRO /FrameOrWand /MakeROFrame /Frame=><- ->. apply ROFrame_frame_r.
 Qed.
 
-(** Setup iModIntro to work with normally. *)
-
-Lemma modality_normally_mixin :
-  modality_mixin normally MIEnvId
-                 (MIEnvTransform (λ P Q : hprop, TCAnd (TCEq P Q) (Normal P))).
-Proof.
-  split; simpl.
-  - by intros P h [-> ?].
-  - by intros P Q [-> ?]; apply normally_intro.
-  - by rewrite normally_hempty.
-  - by intros P Q ?; f_equiv.
-  - by intros P Q; rewrite normally_hstar.
-Qed.
-Definition modality_normally :=
-  Modality _ modality_normally_mixin.
-Instance from_modal_normally P :
-  FromModal modality_normally (normally P) (normally P) P.
-Proof. by rewrite /FromModal. Qed.
-(* Low priority to force annotation. *)
-Instance from_modal_abs_normally P :
-  FromModal modality_normally (normally P) (<absorb> normally P) P | 100.
-Proof. by rewrite /FromModal -bi.absorbingly_intro. Qed.
-
 (** A bit of automation for ROFrame and normally. *)
 Hint Extern 2 (envs_entails _ (ROFrame _ _)) => progress iFrame : iFrame.
 Hint Extern 2 (envs_entails _ (<absorb> ROFrame _ _)) => progress iFrame : iFrame.
@@ -2004,6 +2010,13 @@ Hint Extern 0 (envs_entails _ (ROFrame _ \[])) => iSplitL.
 Hint Extern 0 (envs_entails _ (ROFrame emp%I _)) => iSplitR.
 Hint Extern 0 (envs_entails _ (ROFrame _ emp%I)) => iSplitL.
 
+Hint Extern 0 (envs_entails _ (<absorb> ROFrame \[_] _)) => iSplitR.
+Hint Extern 0 (envs_entails _ (<absorb> ROFrame _ \[_])) => iSplitL.
+Hint Extern 0 (envs_entails _ (<absorb> ROFrame \[] _)) => iSplitR.
+Hint Extern 0 (envs_entails _ (<absorb> ROFrame _ \[])) => iSplitL.
+Hint Extern 0 (envs_entails _ (<absorb> ROFrame emp%I _)) => iSplitR.
+Hint Extern 0 (envs_entails _ (<absorb> ROFrame _ emp%I)) => iSplitL.
+
 Hint Extern 0 (envs_entails _ (normally _)) => iModIntro (normally _).
 Hint Extern 0 (envs_entails _ (<absorb> normally _)) => iModIntro (normally _)%I.
 
@@ -2055,6 +2068,3 @@ Ltac ram_apply_let lem :=
   eapply rule_let_ramified_frame_read_only_locked; [eapply lem|iPrepare|].
 
 End ProofMode.
-
-
-