From 30714902c1ab5d295b3ef8cbd0cb5a550eef7ef0 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 9d152c84b..cdecce17d 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -1004,14 +1004,15 @@ Qed.
 (* Plain *)
 Global Instance pure_plain φ : PlainP (⌜φ⌝ : uPred M)%I.
 Proof. by rewrite /PlainP plainly_pure. Qed.
-Global Instance pure_impl_plain φ Q : PlainP Q → PlainP (⌜φ⌝ → Q)%I.
+Global Instance impl_plain P Q : PlainP P → PlainP Q → PlainP (P → Q).
 Proof.
-  rewrite /PlainP pure_impl_forall plainly_forall. auto using forall_mono.
+  rewrite /PlainP=> HP HQ.
+  by rewrite {2}HP -plainly_impl_plainly -HQ plainly_elim.
 Qed.
-Global Instance pure_wand_plain φ Q : PlainP Q → PlainP (⌜φ⌝ -∗ Q)%I.
+Global Instance wand_plain P Q : PlainP P → PlainP Q → PlainP (P -∗ Q)%I.
 Proof.
-  rewrite /PlainP -always_impl_wand pure_impl_forall plainly_forall.
-  auto using forall_mono.
+  rewrite /PlainP=> HP HQ.
+  by rewrite {2}HP -{1}(plainly_elim P) !wand_impl_plainly -plainly_impl_plainly -HQ.
 Qed.
 Global Instance plainly_plain P : PlainP (☃ P).
 Proof. by intros; apply plainly_intro'. Qed.
@@ -1051,16 +1052,17 @@ Proof. destruct mx; apply _. Qed.
 (* Persistence *)
 Global Instance pure_persistent φ : PersistentP (⌜φ⌝ : uPred M)%I.
 Proof. by rewrite /PersistentP always_pure. Qed.
-Global Instance pure_impl_persistent φ Q :
-  PersistentP Q → PersistentP (⌜φ⌝ → Q)%I.
+Global Instance impl_persistent P Q :
+  PlainP P → PersistentP Q → PersistentP (P → Q).
 Proof.
-  rewrite /PersistentP pure_impl_forall always_forall. auto using forall_mono.
+  rewrite /PlainP /PersistentP=> HP HQ.
+  rewrite {2}HP -always_impl_plainly. by rewrite -HQ plainly_elim.
 Qed.
-Global Instance pure_wand_persistent φ Q :
-  PersistentP Q → PersistentP (⌜φ⌝ -∗ Q)%I.
+Global Instance wand_persistent P Q :
+  PlainP P → PersistentP Q → PersistentP (P -∗ Q)%I.
 Proof.
-  rewrite /PersistentP -always_impl_wand pure_impl_forall always_forall.
-  auto using forall_mono.
+  rewrite /PlainP /PersistentP=> HP HQ.
+  by rewrite {2}HP -{1}(plainly_elim P) !wand_impl_plainly -always_impl_plainly -HQ.
 Qed.
 Global Instance plainly_persistent P : PersistentP (☃ P).
 Proof. by rewrite /PersistentP always_plainly. Qed.
diff --git a/theories/base_logic/primitive.v b/theories/base_logic/primitive.v
index 98a50e054..00389a413 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 always_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