From 68b85aff007882fff22101c0e020f7e697298165 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 6 Sep 2017 17:07:49 +0200
Subject: [PATCH] =?UTF-8?q?A=20rather=20ad-hoc=20IntoSep=20rule=20for=20`?=
 =?UTF-8?q?=E2=96=A0=20=E2=96=B7=20(P=20=E2=88=97=20Q)`.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 theories/bi/derived.v                |  8 +++++++-
 theories/proofmode/class_instances.v | 20 +++++++++++++++++---
 2 files changed, 24 insertions(+), 4 deletions(-)

diff --git a/theories/bi/derived.v b/theories/bi/derived.v
index 4b7ccddc9..010a153ec 100644
--- a/theories/bi/derived.v
+++ b/theories/bi/derived.v
@@ -1561,7 +1561,13 @@ Proof. by rewrite {1}(except_0_intro P) except_0_sep. Qed.
 Lemma except_0_frame_r P Q : ◇ P ∗ Q ⊢ ◇ (P ∗ Q).
 Proof. by rewrite {1}(except_0_intro Q) except_0_sep. Qed.
 
-(* Discrete instances *)
+Lemma later_bare_1 `{!Timeless (emp%I : PROP)} P : ▷ ■ P ⊢ ◇ ■ ▷ P.
+Proof.
+  rewrite /bi_bare later_and (timeless emp%I) except_0_and.
+  by apply and_mono, except_0_intro.
+Qed.
+
+(* Timeless instances *)
 Global Instance Timeless_proper : Proper ((≡) ==> iff) (@Timeless PROP).
 Proof. solve_proper. Qed.
 
diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index c5888cbb4..693472312 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -353,9 +353,12 @@ Qed.
 Global Instance into_sep_pure φ ψ : @IntoSep PROP ⌜φ ∧ ψ⌝ ⌜φ⌝ ⌜ψ⌝.
 Proof. by rewrite /IntoSep pure_and persistent_and_sep_1. Qed.
 
-Global Instance into_sep_bare `{PositiveBI PROP} P Q1 Q2 :
-  IntoSep P Q1 Q2 → IntoSep (■ P) (■ Q1) (■ Q2).
-Proof. rewrite /IntoSep /= => ->. by rewrite bare_sep. Qed.
+(* FIXME: This instance is kind of strange, it just gets rid of the â– . Also, it
+overlaps with `into_sep_bare_later`, and hence has lower precedence. *)
+Global Instance into_sep_bare P Q1 Q2 :
+  IntoSep P Q1 Q2 → IntoSep (■ P) Q1 Q2 | 20.
+Proof. rewrite /IntoSep /= => ->. by rewrite bare_elim. Qed.
+
 Global Instance into_sep_persistently `{PositiveBI PROP} P Q1 Q2 :
   IntoSep P Q1 Q2 → IntoSep (□ P) (□ Q1) (□ Q2).
 Proof. rewrite /IntoSep /= => ->. by rewrite persistently_sep. Qed.
@@ -761,6 +764,17 @@ Global Instance into_sep_except_0 P Q1 Q2 :
   IntoSep P Q1 Q2 → IntoSep (◇ P) (◇ Q1) (◇ Q2).
 Proof. rewrite /IntoSep=> ->. by rewrite except_0_sep. Qed.
 
+(* FIXME: This instance is overly specific, generalize it. *)
+Global Instance into_sep_bare_later `{!Timeless (emp%I : PROP)} P Q1 Q2 :
+  Affine Q1 → Affine Q2 → IntoSep P Q1 Q2 → IntoSep (■ ▷ P) (■ ▷ Q1) (■ ▷ Q2).
+Proof.
+  rewrite /IntoSep /= => ?? ->.
+  rewrite -{1}(affine_bare Q1) -{1}(affine_bare Q2) later_sep !later_bare_1.
+  rewrite -except_0_sep /bi_except_0 bare_or. apply or_elim, bare_elim.
+  rewrite -(idemp bi_and (â–  â–· False)%I) persistent_and_sep_1.
+  by rewrite -(False_elim Q1) -(False_elim Q2).
+Qed.
+
 (* FromOr *)
 Global Instance from_or_later P Q1 Q2 :
   FromOr P Q1 Q2 → FromOr (▷ P) (▷ Q1) (▷ Q2).
-- 
GitLab