From 1e579d5566773ab1699a76d2706237a666f4b613 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 3 Dec 2017 22:16:35 +0100
Subject: [PATCH] One direction of wand_impl_persistently holds for non-affine
 BIs.

---
 theories/bi/derived.v | 20 ++++++++++++--------
 1 file changed, 12 insertions(+), 8 deletions(-)

diff --git a/theories/bi/derived.v b/theories/bi/derived.v
index 0b1a61b92..28265d2c3 100644
--- a/theories/bi/derived.v
+++ b/theories/bi/derived.v
@@ -1072,6 +1072,9 @@ Proof.
   by rewrite (comm bi_and) persistently_and_emp_elim wand_elim_l.
 Qed.
 
+Lemma wand_impl_persistently_2 P Q : (bi_persistently P -∗ Q) ⊢ (bi_persistently P → Q).
+Proof. apply impl_intro_l. by rewrite persistently_and_sep_l_1 wand_elim_r. Qed.
+
 Section persistently_affinely_bi.
   Context `{AffineBI PROP}.
 
@@ -1095,6 +1098,11 @@ Section persistently_affinely_bi.
     by rewrite -persistently_and_sep_r persistently_elim impl_elim_r.
   Qed.
 
+  Lemma wand_impl_persistently P Q : (bi_persistently P -∗ Q) ⊣⊢ (bi_persistently P → Q).
+  Proof.
+    apply (anti_symm (⊢)). apply wand_impl_persistently_2. by rewrite -impl_wand_1.
+  Qed.
+
   Lemma wand_alt P Q : (P -∗ Q) ⊣⊢ ∃ R, R ∗ bi_persistently (P ∗ R → Q).
   Proof.
     apply (anti_symm (⊢)).
@@ -1259,6 +1267,9 @@ Proof.
   by rewrite (comm bi_and) plainly_and_emp_elim wand_elim_l.
 Qed.
 
+Lemma wand_impl_plainly_2 P Q : (bi_plainly P -∗ Q) ⊢ (bi_plainly P → Q).
+Proof. apply impl_intro_l. by rewrite plainly_and_sep_l_1 wand_elim_r. Qed.
+
 Section plainly_affinely_bi.
   Context `{AffineBI PROP}.
 
@@ -1280,16 +1291,9 @@ Section plainly_affinely_bi.
     by rewrite -plainly_and_sep_r plainly_elim impl_elim_r.
   Qed.
 
-  Lemma wand_impl_persistently P Q : (bi_persistently P -∗ Q) ⊣⊢ (bi_persistently P → Q).
-  Proof.
-    apply (anti_symm (⊢)); [|by rewrite -impl_wand_1].
-    apply impl_intro_l. by rewrite persistently_and_sep_l wand_elim_r.
-  Qed.
-
   Lemma wand_impl_plainly P Q : (bi_plainly P -∗ Q) ⊣⊢ (bi_plainly P → Q).
   Proof.
-    apply (anti_symm (⊢)); [|by rewrite -impl_wand_1].
-    apply impl_intro_l. by rewrite plainly_and_sep_l wand_elim_r.
+    apply (anti_symm (⊢)). by rewrite wand_impl_plainly_2. by rewrite -impl_wand_1.
   Qed.
 End plainly_affinely_bi.
 
-- 
GitLab