diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index 7506e6d47f3a94ba8e1ccb09a87b7a4701c63cb4..76e2f0b93f95fe2009df2061b39f9c2611ef8971 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 df0570e73873128d1fe32adc119b211da8c9e4f5..71af3c09c56ce281cbe9286998f2087a975e92d5 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.