From c6b84830e93de64e6576ad78ae79001566b163db Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 3 Dec 2017 22:17:10 +0100
Subject: [PATCH] =?UTF-8?q?Prove=20stronger=20versions=20of=20`Persistent?=
 =?UTF-8?q?=20(P=20-=E2=88=97=20Q)`=20and=20`Plain=20(P=20-=E2=88=97=20Q)`?=
 =?UTF-8?q?.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 theories/bi/derived.v | 34 +++++++++++++++-------------------
 1 file changed, 15 insertions(+), 19 deletions(-)

diff --git a/theories/bi/derived.v b/theories/bi/derived.v
index 28265d2c3..3373fa7a5 100644
--- a/theories/bi/derived.v
+++ b/theories/bi/derived.v
@@ -1757,17 +1757,6 @@ Proof.
   intros. by rewrite /Persistent {2}(plain P) -persistently_impl_plainly
                      -(persistent Q) (plainly_elim_absorbingly P) absorbing.
 Qed.
-(* TODO : can we prove this lemma under positivity of the BI (or even
-   weaker assumptions) ? *)
-Global Instance wand_persistent `{AffineBI PROP} P Q :
-  Plain P → Persistent Q → Persistent (P -∗ Q).
-Proof.
- intros. by rewrite /Persistent {2}(plain P) wand_impl_plainly
-   -persistently_impl_plainly -wand_impl_plainly -(persistent Q) (plainly_elim P).
-Qed.
-Global Instance pure_wand_persistent φ Q :
-  Persistent Q → Absorbing Q → Persistent (⌜φ⌝ -∗ Q).
-Proof. intros. rewrite pure_wand_forall. apply _. Qed.
 
 Global Instance sep_persistent P Q :
   Persistent P → Persistent Q → Persistent (P ∗ Q).
@@ -1785,6 +1774,15 @@ Global Instance from_option_persistent {A} P (Ψ : A → PROP) (mx : option A) :
   (∀ x, Persistent (Ψ x)) → Persistent P → Persistent (from_option Ψ P mx).
 Proof. destruct mx; apply _. Qed.
 
+Global Instance wand_persistent P Q :
+  Plain P → Persistent Q → Absorbing Q → Persistent (P -∗ Q).
+Proof.
+  intros. rewrite /Persistent {2}(plain P). trans (bi_persistently (bi_plainly P → Q)).
+  - rewrite -persistently_impl_plainly -wand_impl_affinely_plainly -(persistent Q).
+    by rewrite affinely_plainly_elim.
+  - apply persistently_mono, wand_intro_l. by rewrite sep_and impl_elim_r.
+Qed.
+
 (* Plainness instances *)
 Global Instance pure_plain φ : Plain (⌜φ⌝%I : PROP).
 Proof. by rewrite /Plain plainly_pure. Qed.
@@ -1815,16 +1813,14 @@ Proof.
   intros. by rewrite /Plain {2}(plain P) -plainly_impl_plainly -(plain Q)
                      (plainly_elim_absorbingly P) absorbing.
 Qed.
-(* TODO : can we prove this lemma under positivity of the BI (or even
-   weaker assumptions) ? *)
-Global Instance wand_plain `{AffineBI PROP} P Q :
-  Plain P → Plain Q → Plain (P -∗ Q).
+Global Instance wand_plain P Q :
+  Plain P → Plain Q → Absorbing Q → Plain (P -∗ Q).
 Proof.
-  intros. rewrite /Plain {2}(plain P) wand_impl_plainly -plainly_impl_plainly.
-  by rewrite -wand_impl_plainly -(plain Q) (plainly_elim P).
+  intros. rewrite /Plain {2}(plain P). trans (bi_plainly (bi_plainly P → Q)).
+  - rewrite -plainly_impl_plainly -wand_impl_affinely_plainly -(plain Q).
+    by rewrite affinely_plainly_elim.
+  - apply plainly_mono, wand_intro_l. by rewrite sep_and impl_elim_r.
 Qed.
-Global Instance pure_wand_plain φ Q `{!Absorbing Q} : Plain Q → Plain (⌜φ⌝ -∗ Q).
-Proof. intros ?. rewrite pure_wand_forall. apply _. Qed.
 Global Instance sep_plain P Q : Plain P → Plain Q → Plain (P ∗ Q).
 Proof. intros. by rewrite /Plain -plainly_sep_2 -!plain. Qed.
 
-- 
GitLab