From 587402299e849ee9ee10b004f8c26e0f8e2daecc Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 23 Oct 2017 22:54:36 +0200
Subject: [PATCH] Plainness and persistence of implications and wands.

---
 theories/base_logic/derived.v   | 26 ++++++++++++++------------
 theories/base_logic/primitive.v | 14 ++++++++++++++
 2 files changed, 28 insertions(+), 12 deletions(-)

diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index 7506e6d47..76e2f0b93 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -1004,14 +1004,15 @@ Qed.
 (* Plain *)
 Global Instance pure_plain φ : Plain (⌜φ⌝ : uPred M)%I.
 Proof. by rewrite /Plain plainly_pure. Qed.
-Global Instance pure_impl_plain φ Q : Plain Q → Plain (⌜φ⌝ → Q)%I.
+Global Instance impl_plain P Q : Plain P → Plain Q → Plain (P → Q).
 Proof.
-  rewrite /Plain pure_impl_forall plainly_forall. auto using forall_mono.
+  rewrite /Plain=> HP HQ.
+  by rewrite {2}HP -plainly_impl_plainly -HQ plainly_elim.
 Qed.
-Global Instance pure_wand_plain φ Q : Plain Q → Plain (⌜φ⌝ -∗ Q)%I.
+Global Instance wand_plain P Q : Plain P → Plain Q → Plain (P -∗ Q)%I.
 Proof.
-  intros HQ. rewrite /Plain -persistently_pure -!impl_wand_persistently.
-  rewrite persistently_pure pure_impl_forall plainly_forall. auto using forall_mono.
+  rewrite /Plain=> HP HQ.
+  by rewrite {2}HP -{1}(plainly_elim P) !wand_impl_plainly -plainly_impl_plainly -HQ.
 Qed.
 Global Instance plainly_plain P : Plain (â–  P).
 Proof. by intros; apply plainly_intro'. Qed.
@@ -1051,16 +1052,17 @@ Proof. destruct mx; apply _. Qed.
 (* Persistence *)
 Global Instance pure_persistent φ : Persistent (⌜φ⌝ : uPred M)%I.
 Proof. by rewrite /Persistent persistently_pure. Qed.
-Global Instance pure_impl_persistent φ Q :
-  Persistent Q → Persistent (⌜φ⌝ → Q)%I.
+Global Instance impl_persistent P Q :
+  Plain P → Persistent Q → Persistent (P → Q).
 Proof.
-  rewrite /Persistent pure_impl_forall persistently_forall. auto using forall_mono.
+  rewrite /Plain /Persistent=> HP HQ.
+  rewrite {2}HP -persistently_impl_plainly. by rewrite -HQ plainly_elim.
 Qed.
-Global Instance pure_wand_persistent φ Q :
-  Persistent Q → Persistent (⌜φ⌝ -∗ Q)%I.
+Global Instance wand_persistent P Q :
+  Plain P → Persistent Q → Persistent (P -∗ Q)%I.
 Proof.
-  rewrite /Persistent -impl_wand pure_impl_forall persistently_forall.
-  auto using forall_mono.
+  rewrite /Plain /Persistent=> HP HQ.
+  by rewrite {2}HP -{1}(plainly_elim P) !wand_impl_plainly -persistently_impl_plainly -HQ.
 Qed.
 Global Instance plainly_persistent P : Persistent (â–  P).
 Proof. by rewrite /Persistent persistently_plainly. Qed.
diff --git a/theories/base_logic/primitive.v b/theories/base_logic/primitive.v
index df0570e73..71af3c09c 100644
--- a/theories/base_logic/primitive.v
+++ b/theories/base_logic/primitive.v
@@ -480,6 +480,20 @@ Proof.
   by rewrite cmra_core_l cmra_core_idemp.
 Qed.
 
+Lemma persistently_impl_plainly P Q : (■ P → □ Q) ⊢ □ (■ P → Q).
+Proof.
+  unseal; split=> /= n x ? HPQ n' x' ????.
+  eapply uPred_mono with (core x), cmra_included_includedN; auto.
+  apply (HPQ n' x); eauto using cmra_validN_le.
+Qed.
+
+Lemma plainly_impl_plainly P Q : (■ P → ■ Q) ⊢ ■ (■ P → Q).
+Proof.
+  unseal; split=> /= n x ? HPQ n' x' ????.
+  eapply uPred_mono with ε, cmra_included_includedN; auto.
+  apply (HPQ n' x); eauto using cmra_validN_le.
+Qed.
+
 (* Later *)
 Lemma later_mono P Q : (P ⊢ Q) → ▷ P ⊢ ▷ Q.
 Proof.
-- 
GitLab