From 7499050658800a43047a03e40e8f0a6b8f40593a Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 1 Sep 2017 15:02:20 +0200
Subject: [PATCH] =?UTF-8?q?Allow=20stripping=20of=20timeless=20=E2=96=B7s?=
 =?UTF-8?q?=20below=20=E2=96=A0=20modalities.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 theories/proofmode/class_instances.v | 30 +++++++++++++++-------------
 theories/proofmode/classes.v         | 10 +++++++++-
 theories/tests/proofmode.v           |  3 +++
 3 files changed, 28 insertions(+), 15 deletions(-)

diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index 15ce9ea17..c5888cbb4 100644
--- a/theories/proofmode/class_instances.v
+++ b/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 *)
diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index 575a5722d..7263098d0 100644
--- a/theories/proofmode/classes.v
+++ b/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.
diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index ea1a0fc45..c704ba30c 100644
--- a/theories/tests/proofmode.v
+++ b/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.
 
-- 
GitLab