Allow stripping of timeless ▷s below ■ modalities.

theories/proofmode/class_instances.v

@@ -831,23 +831,25 @@ Proof. apply later_intro. Qed.
 Global Instance from_modal_except_0 P : FromModal (◇ P) P.
 Proof. apply except_0_intro. Qed.
 
+(* IntoExcept0 *)
+Global Instance into_timeless_except_0 P : IntoExcept0 (◇ P) P.
+Proof. by rewrite /IntoExcept0. Qed.
+Global Instance into_timeless_later P : Timeless P → IntoExcept0 (▷ P) P.
+Proof. by rewrite /IntoExcept0. Qed.
+Global Instance into_timeless_later_if p P : Timeless P → IntoExcept0 (▷?p P) P.
+Proof. rewrite /IntoExcept0. destruct p; auto using except_0_intro. Qed.
+
+Global Instance into_timeless_bare P Q : IntoExcept0 P Q → IntoExcept0 (■ P) (■ Q).
+Proof. rewrite /IntoExcept0=> ->. by rewrite except_0_bare_2. Qed.
+Global Instance into_timeless_persistently P Q : IntoExcept0 P Q → IntoExcept0 (□ P) (□ Q).
+Proof. rewrite /IntoExcept0=> ->. by rewrite except_0_persistently. Qed.
+
 (* ElimModal *)
-Global Instance elim_modal_except_0 P Q : IsExcept0 Q → ElimModal (◇ P) P Q Q.
+Global Instance elim_modal_timeless P Q :
+  IntoExcept0 P P' → IsExcept0 Q → ElimModal P P' Q Q.
 Proof.
   intros. rewrite /ElimModal (except_0_intro (_ -∗ _)%I).
-  by rewrite -except_0_sep wand_elim_r.
-Qed.
-Global Instance elim_modal_timeless_later P Q :
-  Timeless P → IsExcept0 Q → ElimModal (▷ P) P Q Q.
-Proof.
-  intros. rewrite /ElimModal (except_0_intro (_ -∗ _)%I) (timeless P).
-  by rewrite -except_0_sep wand_elim_r.
-Qed.
-Global Instance elim_modal_timeless_later_if p P Q :
-  Timeless P → IsExcept0 Q → ElimModal (▷?p P) P Q Q.
-Proof.
-  destruct p; simpl; auto using elim_modal_timeless_later.
-  intros _ _. by rewrite /ElimModal wand_elim_r.
+  by rewrite (into_except_0 P) -except_0_sep wand_elim_r.
 Qed.
 
 (* Frame *)

theories/proofmode/classes.v

@@ -211,6 +211,12 @@ Instance maybe_frame_default {PROP : bi} (R P : PROP) :
   TCOr (Affine R) (Absorbing P) → MaybeFrame false R P P | 100.
 Proof. intros. rewrite /MaybeFrame /=. apply: sep_elim_r. Qed.
 
+Class IntoExcept0 {PROP : sbi} (P Q : PROP) := into_except_0 : P ⊢ ◇ Q.
+Arguments IntoExcept0 {_} _%I _%I : simpl never.
+Arguments into_except_0 {_} _%I _%I {_}.
+Hint Mode IntoExcept0 + ! - : typeclass_instances.
+Hint Mode IntoExcept0 + - ! : typeclass_instances.
+
 (* The class [IntoLaterN] has only two instances:
 
 - The default instance [IntoLaterN n P P], i.e. [▷^n P -∗ P]
@@ -294,5 +300,7 @@ Instance into_forall_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A → PROP) :
   IntoForall P Φ → IntoForall (tc_opaque P) Φ := id.
 Instance from_modal_tc_opaque {PROP : bi} (P Q : PROP) :
   FromModal P Q → FromModal (tc_opaque P) Q := id.
+(* Higher precedence than [elim_modal_timeless], so that [iAssert] does not
+   loop (see test [test_iAssert_modality] in proofmode.v). *)
 Instance elim_modal_tc_opaque {PROP : bi} (P P' Q Q' : PROP) :
-  ElimModal P P' Q Q' → ElimModal (tc_opaque P) P' Q Q' := id.
+  ElimModal P P' Q Q' → ElimModal (tc_opaque P) P' Q Q' | 100 := id.

theories/tests/proofmode.v

@@ -120,6 +120,9 @@ Proof.
   by iMod "HF".
 Qed.
 
+Lemma test_iMod_bare_timeless P `{!Timeless P} : ■ ▷ P -∗ ◇ ■ P.
+Proof. iIntros "H". iMod "H". done. Qed.
+
 Lemma test_iAssumption_False P : False -∗ P.
 Proof. iIntros "H". done. Qed.