From ae01cec590a6bf9bef6450977a2e03813a206d1a Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 3 May 2018 22:36:07 +0200
Subject: [PATCH] =?UTF-8?q?Make=20the=20behavior=20of=20`iSplit`=20on=20`P?=
 =?UTF-8?q?=20=E2=88=97=20=E2=96=A1=20Q`=20consistent=20with=20that=20of?=
 =?UTF-8?q?=20`iDestruct`.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

It now turns the goal into `P` and `<pers> Q`, which is dual to
`iDestruct`, which turns `P ∧ <pers> Q` into `P` and `□ Q`.
---
 theories/proofmode/class_instances_bi.v | 22 +++++++++++++---------
 theories/proofmode/classes.v            |  5 ++++-
 theories/tests/proofmode.v              | 16 ++++++++++++++++
 3 files changed, 33 insertions(+), 10 deletions(-)

diff --git a/theories/proofmode/class_instances_bi.v b/theories/proofmode/class_instances_bi.v
index e431e99a6..5b118cd10 100644
--- a/theories/proofmode/class_instances_bi.v
+++ b/theories/proofmode/class_instances_bi.v
@@ -22,6 +22,11 @@ Global Instance into_absorbingly_True : @IntoAbsorbingly PROP True emp | 0.
 Proof. by rewrite /IntoAbsorbingly -absorbingly_True_emp absorbingly_pure. Qed.
 Global Instance into_absorbingly_absorbing P : Absorbing P → IntoAbsorbingly P P | 1.
 Proof. intros. by rewrite /IntoAbsorbingly absorbing_absorbingly. Qed.
+Global Instance into_absorbingly_intuitionistically P :
+  IntoAbsorbingly (<pers> P) (â–¡ P) | 0.
+Proof.
+  by rewrite /IntoAbsorbingly -absorbingly_intuitionistically_into_persistently.
+Qed.
 Global Instance into_absorbingly_default P : IntoAbsorbingly (<absorb> P) P | 100.
 Proof. by rewrite /IntoAbsorbingly. Qed.
 
@@ -382,19 +387,18 @@ Proof. by rewrite /FromImpl -embed_impl => <-. Qed.
 Global Instance from_and_and P1 P2 : FromAnd (P1 ∧ P2) P1 P2 | 100.
 Proof. by rewrite /FromAnd. Qed.
 Global Instance from_and_sep_persistent_l P1 P1' P2 :
-  FromAffinely P1 P1' → Persistent P1' → FromAnd (P1 ∗ P2) P1' P2 | 9.
+  Persistent P1 → IntoAbsorbingly P1' P1 → FromAnd (P1 ∗ P2) P1' P2 | 9.
 Proof.
-  rewrite /FromAffinely /FromAnd=> <- ?. by rewrite persistent_and_affinely_sep_l_1.
+  rewrite /IntoAbsorbingly /FromAnd=> ? ->.
+  rewrite persistent_and_affinely_sep_l_1 {1}(persistent_persistently_2 P1).
+  by rewrite absorbingly_elim_persistently -{2}(intuitionistically_elim P1).
 Qed.
 Global Instance from_and_sep_persistent_r P1 P2 P2' :
-  FromAffinely P2 P2' → Persistent P2' → FromAnd (P1 ∗ P2) P1 P2' | 10.
-Proof.
-  rewrite /FromAffinely /FromAnd=> <- ?. by rewrite persistent_and_affinely_sep_r_1.
-Qed.
-Global Instance from_and_sep_persistent P1 P2 :
-  Persistent P1 → Persistent P2 → FromAnd (P1 ∗ P2) P1 P2 | 11.
+  Persistent P2 → IntoAbsorbingly P2' P2 → FromAnd (P1 ∗ P2) P1 P2' | 10.
 Proof.
-  rewrite /FromAffinely /FromAnd. intros ??. by rewrite -persistent_and_sep_1.
+  rewrite /IntoAbsorbingly /FromAnd=> ? ->.
+  rewrite persistent_and_affinely_sep_r_1 {1}(persistent_persistently_2 P2).
+  by rewrite absorbingly_elim_persistently -{2}(intuitionistically_elim P2).
 Qed.
 
 Global Instance from_and_pure φ ψ : @FromAnd PROP ⌜φ ∧ ψ⌝ ⌜φ⌝ ⌜ψ⌝.
diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index f892b7bff..4ad095999 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -117,11 +117,14 @@ Arguments FromModal {_ _ _} _ _%I _%I _%I : simpl never.
 Arguments from_modal {_ _ _} _ _ _%I _%I {_}.
 Hint Mode FromModal - + - - - ! - : typeclass_instances.
 
+(** The [FromAffinely P Q] class is used to add an [<affine>] modality to the
+proposition [Q].
+
+The input is [Q] and the output is [P]. *)
 Class FromAffinely {PROP : bi} (P Q : PROP) :=
   from_affinely : <affine> Q ⊢ P.
 Arguments FromAffinely {_} _%I _%I : simpl never.
 Arguments from_affinely {_} _%I _%I {_}.
-Hint Mode FromAffinely + ! - : typeclass_instances.
 Hint Mode FromAffinely + - ! : typeclass_instances.
 
 (** The [IntoAbsorbingly P Q] class is used to add an [<absorb>] modality to
diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index 1a8abb751..b8024b8f8 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -444,4 +444,20 @@ Lemma test_apply_affine_wand `{!BiPlainly PROP} (P : PROP) :
   P -∗ (∀ Q : PROP, <affine> ■ (Q -∗ <pers> Q) -∗ <affine> ■ (P -∗ Q) -∗ Q).
 Proof. iIntros "HP" (Q) "_ #HPQ". by iApply "HPQ". Qed.
 
+Lemma test_and_sep (P Q R : PROP) : P ∧ (Q ∗ □ R) ⊢ (P ∧ Q) ∗ □ R.
+Proof.
+  iIntros "H". repeat iSplit.
+  - iDestruct "H" as "[$ _]".
+  - iDestruct "H" as "[_ [$ _]]".
+  - iDestruct "H" as "[_ [_ #$]]".
+Qed.
+
+Lemma test_and_sep_2 (P Q R : PROP) `{!Persistent R, !Affine R} :
+  P ∧ (Q ∗ R) ⊢ (P ∧ Q) ∗ R.
+Proof.
+  iIntros "H". repeat iSplit.
+  - iDestruct "H" as "[$ _]".
+  - iDestruct "H" as "[_ [$ _]]".
+  - iDestruct "H" as "[_ [_ #$]]".
+Qed.
 End tests.
-- 
GitLab