From 89b76adb28d84045ab9be13e3b2adbce193c0ed0 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sun, 13 Jun 2021 11:47:54 +0200
Subject: [PATCH] move persistently_forall_2 out of BI interface

---
 iris/base_logic/bi.v             | 42 +++++++++++------
 iris/bi/big_op.v                 | 80 ++++++++++++++++++++++----------
 iris/bi/derived_laws.v           | 28 +++++------
 iris/bi/extensions.v             |  8 ++++
 iris/bi/interface.v              | 15 ++++--
 iris/bi/lib/core.v               | 10 ++--
 iris/bi/monpred.v                | 24 +++++++---
 iris/bi/plainly.v                | 26 ++++++-----
 iris/bi/telescopes.v             |  2 +-
 iris/proofmode/class_instances.v |  8 ++--
 tests/bi.v                       |  4 +-
 tests/proofmode.ref              |  2 +
 tests/proofmode.v                |  5 +-
 tests/proofmode_monpred.v        |  7 +--
 tests/telescopes.v               |  2 +-
 15 files changed, 175 insertions(+), 88 deletions(-)

diff --git a/iris/base_logic/bi.v b/iris/base_logic/bi.v
index f555ec335..cf20a664c 100644
--- a/iris/base_logic/bi.v
+++ b/iris/base_logic/bi.v
@@ -56,7 +56,16 @@ Proof.
     + apply forall_intro=>[[]].
     + etrans; first exact: persistently_forall_2.
       apply persistently_mono. exact: pure_intro.
-  - exact: @persistently_forall_2.
+  - (* ((<pers> P) ∧ (<pers> Q)) ⊢ <pers> (P ∧ Q) (ADMISSIBLE) *)
+    intros P Q.
+    trans (uPred_forall (M:=M) (λ b : bool, uPred_persistently (if b then P else Q))).
+    + apply forall_intro=>[[]].
+      * apply and_elim_l.
+      * apply and_elim_r.
+    + etrans; first exact: persistently_forall_2.
+      apply persistently_mono. apply and_intro.
+      * etrans; first apply (forall_elim true). done.
+      * etrans; first apply (forall_elim false). done.
   - exact: @persistently_exist_1.
   - (* <pers> P ∗ Q ⊢ <pers> P (ADMISSIBLE) *)
     intros. etrans; first exact: sep_comm'.
@@ -89,12 +98,6 @@ Canonical Structure uPredI (M : ucmra) : bi :=
      bi_bi_mixin := uPred_bi_mixin M;
      bi_bi_later_mixin := uPred_bi_later_mixin M |}.
 
-Global Instance uPred_pure_forall M : BiPureForall (uPredI M).
-Proof. exact: @pure_forall_2. Qed.
-
-Global Instance uPred_later_contractive {M} : BiLaterContractive (uPredI M).
-Proof. apply later_contractive. Qed.
-
 Lemma uPred_internal_eq_mixin M : BiInternalEqMixin (uPredI M) (@uPred_internal_eq M).
 Proof.
   split.
@@ -118,7 +121,6 @@ Proof.
   - exact: plainly_elim_persistently.
   - exact: plainly_idemp_2.
   - exact: @plainly_forall_2.
-  - exact: persistently_impl_plainly.
   - exact: plainly_impl_plainly.
   - (* P ⊢ ■ emp (ADMISSIBLE) *)
     intros P.
@@ -137,9 +139,6 @@ Qed.
 Global Instance uPred_plainly M : BiPlainly (uPredI M) :=
   {| bi_plainly_mixin := uPred_plainly_mixin M |}.
 
-Global Instance uPred_prop_ext M : BiPropExt (uPredI M).
-Proof. exact: prop_ext_2. Qed.
-
 Lemma uPred_bupd_mixin M : BiBUpdMixin (uPredI M) uPred_bupd.
 Proof.
   split.
@@ -151,9 +150,6 @@ Proof.
 Qed.
 Global Instance uPred_bi_bupd M : BiBUpd (uPredI M) := {| bi_bupd_mixin := uPred_bupd_mixin M |}.
 
-Global Instance uPred_bi_bupd_plainly M : BiBUpdPlainly (uPredI M).
-Proof. exact: bupd_plainly. Qed.
-
 (** extra BI instances *)
 
 Global Instance uPred_affine M : BiAffine (uPredI M) | 0.
@@ -162,9 +158,27 @@ Proof. intros P. exact: pure_intro. Qed.
 many lemmas that have [BiAffine] as a premise. *)
 Global Hint Immediate uPred_affine : core.
 
+Global Instance uPred_persistently_forall M : BiPersistentlyForall (uPredI M).
+Proof. exact: @persistently_forall_2. Qed.
+
+Global Instance uPred_pure_forall M : BiPureForall (uPredI M).
+Proof. exact: @pure_forall_2. Qed.
+
+Global Instance uPred_later_contractive {M} : BiLaterContractive (uPredI M).
+Proof. apply later_contractive. Qed.
+
+Global Instance uPred_persistently_impl_plainly M : BiPersistentlyImplPlainly (uPredI M).
+Proof. exact: persistently_impl_plainly. Qed.
+
 Global Instance uPred_plainly_exist_1 M : BiPlainlyExist (uPredI M).
 Proof. exact: @plainly_exist_1. Qed.
 
+Global Instance uPred_prop_ext M : BiPropExt (uPredI M).
+Proof. exact: prop_ext_2. Qed.
+
+Global Instance uPred_bi_bupd_plainly M : BiBUpdPlainly (uPredI M).
+Proof. exact: bupd_plainly. Qed.
+
 (** Re-state/export lemmas about Iris-specific primitive connectives (own, valid) *)
 
 Module uPred.
diff --git a/iris/bi/big_op.v b/iris/bi/big_op.v
index 1c901198a..0ba0adb94 100644
--- a/iris/bi/big_op.v
+++ b/iris/bi/big_op.v
@@ -249,8 +249,11 @@ Section sep_list.
     intros HΦ. apply (anti_symm _).
     { apply forall_intro=> k; apply forall_intro=> x.
       apply impl_intro_l, pure_elim_l=> ?; by apply: big_sepL_lookup. }
-    rewrite -big_sepL_intro. setoid_rewrite pure_impl_forall.
-    by rewrite intuitionistic_intuitionistically.
+    revert Φ HΦ. induction l as [|x l IH]=> Φ HΦ /=.
+    { apply: affine. }
+    rewrite -persistent_and_sep_1. apply and_intro.
+    - rewrite (forall_elim 0) (forall_elim x) pure_True // True_impl. done.
+    - rewrite -IH. apply forall_intro => k. by rewrite (forall_elim (S k)).
   Qed.
 
   Lemma big_sepL_impl Φ Ψ l :
@@ -725,13 +728,18 @@ Section sep_list2.
       ⌜length l1 = length l2⌝
       ∧ (∀ k x1 x2, ⌜l1 !! k = Some x1⌝ → ⌜l2 !! k = Some x2⌝ → Φ k x1 x2).
   Proof.
-    intros. apply (anti_symm _).
-    - apply and_intro; [apply big_sepL2_length|].
+    intros HΦ. apply (anti_symm _).
+    { apply and_intro; [apply big_sepL2_length|].
       apply forall_intro=> k. apply forall_intro=> x1. apply forall_intro=> x2.
-      do 2 (apply impl_intro_l; apply pure_elim_l=> ?). by apply :big_sepL2_lookup.
-    - apply pure_elim_l=> ?. rewrite -big_sepL2_intro //.
-      repeat setoid_rewrite pure_impl_forall.
-      by rewrite intuitionistic_intuitionistically.
+      do 2 (apply impl_intro_l; apply pure_elim_l=> ?). by apply :big_sepL2_lookup. }
+    apply pure_elim_l=> Hlen.
+    revert l2 Φ HΦ Hlen. induction l1 as [|x1 l1 IH]=> -[|x2 l2] Φ HΦ Hlen; simplify_eq/=.
+    { by apply (affine _). }
+    rewrite -persistent_and_sep_1. apply and_intro.
+    - rewrite (forall_elim 0) (forall_elim x1) (forall_elim x2).
+      by rewrite !pure_True // !True_impl.
+    - rewrite -IH //.
+      by apply forall_intro=> k; by rewrite (forall_elim (S k)).
   Qed.
 
   Lemma big_sepL2_impl Φ Ψ l1 l2 :
@@ -1414,11 +1422,18 @@ Section sep_map.
     (∀ k x, Persistent (Φ k x)) →
     ([∗ map] k↦x ∈ m, Φ k x) ⊣⊢ (∀ k x, ⌜m !! k = Some x⌝ → Φ k x).
   Proof.
-    intros. apply (anti_symm _).
+    intros HΦ. apply (anti_symm _).
     { apply forall_intro=> k; apply forall_intro=> x.
       apply impl_intro_l, pure_elim_l=> ?; by apply: big_sepM_lookup. }
-    rewrite -big_sepM_intro. setoid_rewrite pure_impl_forall.
-    by rewrite intuitionistic_intuitionistically.
+    revert Φ HΦ. induction m as [|i x m ? IH] using map_ind=> Φ HΦ.
+    { rewrite big_sepM_empty. apply: affine. }
+    rewrite big_sepM_insert // -persistent_and_sep_1. apply and_intro.
+    - rewrite (forall_elim i) (forall_elim x) lookup_insert.
+      by rewrite pure_True // True_impl.
+    - rewrite -IH. apply forall_mono=> k; apply forall_mono=> y.
+      apply impl_intro_l, pure_elim_l=> ?.
+      rewrite lookup_insert_ne; last by intros ?; simplify_map_eq.
+      by rewrite pure_True // True_impl.
   Qed.
 
   Lemma big_sepM_impl Φ Ψ m :
@@ -2172,12 +2187,16 @@ Section map2.
       ∧ (∀ k x1 x2, ⌜m1 !! k = Some x1⌝ → ⌜m2 !! k = Some x2⌝ → Φ k x1 x2).
   Proof.
     intros. apply (anti_symm _).
-    - apply and_intro; [apply big_sepM2_lookup_iff|].
+    { apply and_intro; [apply big_sepM2_lookup_iff|].
       apply forall_intro=> k. apply forall_intro=> x1. apply forall_intro=> x2.
-      do 2 (apply impl_intro_l; apply pure_elim_l=> ?). by apply :big_sepM2_lookup.
-    - apply pure_elim_l=> ?. rewrite -big_sepM2_intro //.
-      repeat setoid_rewrite pure_impl_forall.
-      by rewrite intuitionistic_intuitionistically.
+      do 2 (apply impl_intro_l; apply pure_elim_l=> ?). by apply: big_sepM2_lookup. }
+    apply pure_elim_l=> Hdom. rewrite big_sepM2_eq /big_sepM2_def.
+    apply and_intro; [by apply pure_intro|].
+    rewrite big_sepM_forall. f_equiv=> k.
+    apply forall_intro=> -[x1 x2]. rewrite (forall_elim x1) (forall_elim x2).
+    apply impl_intro_l, pure_elim_l.
+    intros (?&?&[= <- <-]&?&?)%map_lookup_zip_with_Some.
+    by rewrite !pure_True // !True_impl.
   Qed.
 
   Lemma big_sepM2_impl Φ Ψ m1 m2 :
@@ -2561,13 +2580,19 @@ Section gset.
   Qed.
 
   Lemma big_sepS_forall `{BiAffine PROP} Φ X :
-    (∀ x, Persistent (Φ x)) → ([∗ set] x ∈ X, Φ x) ⊣⊢ (∀ x, ⌜x ∈ X⌝ → Φ x).
+    (∀ x, Persistent (Φ x)) →
+    ([∗ set] x ∈ X, Φ x) ⊣⊢ (∀ x, ⌜x ∈ X⌝ → Φ x).
   Proof.
-    intros. apply (anti_symm _).
+    intros HΦ. apply (anti_symm _).
     { apply forall_intro=> x.
       apply impl_intro_l, pure_elim_l=> ?; by apply: big_sepS_elem_of. }
-    rewrite -big_sepS_intro. setoid_rewrite pure_impl_forall.
-    by rewrite intuitionistic_intuitionistically.
+    revert Φ HΦ. induction X as [|x X ? IH] using set_ind_L=> Φ HΦ.
+    { rewrite big_sepS_empty. apply: affine. }
+    rewrite big_sepS_insert // -persistent_and_sep_1. apply and_intro.
+    - rewrite (forall_elim x) pure_True ?True_impl; last set_solver. done.
+    - rewrite -IH. apply forall_mono=> y.
+      apply impl_intro_l, pure_elim_l=> ?.
+      by rewrite pure_True ?True_impl; last set_solver.
   Qed.
 
   Lemma big_sepS_impl Φ Ψ X :
@@ -2800,13 +2825,20 @@ Section gmultiset.
   Qed.
 
   Lemma big_sepMS_forall `{BiAffine PROP} Φ X :
-    (∀ x, Persistent (Φ x)) → ([∗ mset] x ∈ X, Φ x) ⊣⊢ (∀ x, ⌜x ∈ X⌝ → Φ x).
+    (∀ x, Persistent (Φ x)) →
+    ([∗ mset] x ∈ X, Φ x) ⊣⊢ (∀ x, ⌜x ∈ X⌝ → Φ x).
   Proof.
-    intros. apply (anti_symm _).
+    intros HΦ. apply (anti_symm _).
     { apply forall_intro=> x.
       apply impl_intro_l, pure_elim_l=> ?; by apply: big_sepMS_elem_of. }
-    rewrite -big_sepMS_intro. setoid_rewrite pure_impl_forall.
-    by rewrite intuitionistic_intuitionistically.
+    revert Φ HΦ. induction X as [|x X IH] using gmultiset_ind=> Φ HΦ.
+    { rewrite big_sepMS_empty. apply: affine. }
+    rewrite big_sepMS_disj_union.
+    rewrite big_sepMS_singleton -persistent_and_sep_1. apply and_intro.
+    - rewrite (forall_elim x) pure_True ?True_impl; last multiset_solver. done.
+    - rewrite -IH. apply forall_mono=> y.
+      apply impl_intro_l, pure_elim_l=> ?.
+      by rewrite pure_True ?True_impl; last multiset_solver.
   Qed.
 
   Lemma big_sepMS_impl Φ Ψ X :
diff --git a/iris/bi/derived_laws.v b/iris/bi/derived_laws.v
index e90d5bb5c..9d29b036c 100644
--- a/iris/bi/derived_laws.v
+++ b/iris/bi/derived_laws.v
@@ -846,23 +846,24 @@ Proof.
   by rewrite /bi_absorbingly comm persistently_absorbing.
 Qed.
 
-Lemma persistently_forall {A} (Ψ : A → PROP) :
+Lemma persistently_forall_1 {A} (Ψ : A → PROP) :
+  <pers> (∀ a, Ψ a) ⊢ ∀ a, <pers> (Ψ a).
+Proof. apply forall_intro=> x. by rewrite (forall_elim x). Qed.
+Lemma persistently_forall `{!BiPersistentlyForall PROP} {A} (Ψ : A → PROP) :
   <pers> (∀ a, Ψ a) ⊣⊢ ∀ a, <pers> (Ψ a).
-Proof.
-  apply (anti_symm _); auto using persistently_forall_2.
-  apply forall_intro=> x. by rewrite (forall_elim x).
-Qed.
+Proof. apply (anti_symm _); auto using persistently_forall_1, persistently_forall_2. Qed.
 Lemma persistently_exist {A} (Ψ : A → PROP) :
   <pers> (∃ a, Ψ a) ⊣⊢ ∃ a, <pers> (Ψ a).
 Proof.
-  apply (anti_symm _); auto using persistently_exist_1.
+  apply (anti_symm _); first by auto using persistently_exist_1.
   apply exist_elim=> x. by rewrite (exist_intro x).
 Qed.
 Lemma persistently_and P Q : <pers> (P ∧ Q) ⊣⊢ <pers> P ∧ <pers> Q.
-Proof. rewrite !and_alt persistently_forall. by apply forall_proper=> -[]. Qed.
+Proof. apply (anti_symm _); by auto using persistently_and_2. Qed.
 Lemma persistently_or P Q : <pers> (P ∨ Q) ⊣⊢ <pers> P ∨ <pers> Q.
 Proof. rewrite !or_alt persistently_exist. by apply exist_proper=> -[]. Qed.
-Lemma persistently_impl P Q : <pers> (P → Q) ⊢ <pers> P → <pers> Q.
+Lemma persistently_impl P Q :
+  <pers> (P → Q) ⊢ <pers> P → <pers> Q.
 Proof.
   apply impl_intro_l; rewrite -persistently_and.
   apply persistently_mono, impl_elim with P; auto.
@@ -875,6 +876,8 @@ Qed.
 
 Lemma persistently_True_emp : <pers> True ⊣⊢ <pers> emp.
 Proof. apply (anti_symm _); auto using persistently_emp_intro. Qed.
+Lemma persistently_True : True ⊢ <pers> True.
+Proof. rewrite persistently_True_emp. apply persistently_emp_intro. Qed.
 
 Lemma persistently_and_emp P : <pers> P ⊣⊢ <pers> (emp ∧ P).
 Proof.
@@ -922,9 +925,8 @@ Lemma persistently_pure φ : <pers> ⌜φ⌝ ⊣⊢ ⌜φ⌝.
 Proof.
   apply (anti_symm _).
   { by rewrite persistently_into_absorbingly absorbingly_pure. }
-  apply pure_elim'=> Hφ.
-  trans (∀ x : False, <pers> True : PROP)%I; [by apply forall_intro|].
-  rewrite persistently_forall_2. auto using persistently_mono, pure_intro.
+  apply pure_elim'=> Hφ. rewrite persistently_True.
+  auto using persistently_mono, pure_intro.
 Qed.
 
 Lemma persistently_sep_dup P : <pers> P ⊣⊢ <pers> P ∗ <pers> P.
@@ -1083,7 +1085,7 @@ Qed.
 Lemma intuitionistically_and P Q : □ (P ∧ Q) ⊣⊢ □ P ∧ □ Q.
 Proof. by rewrite /bi_intuitionistically persistently_and affinely_and. Qed.
 Lemma intuitionistically_forall {A} (Φ : A → PROP) : □ (∀ x, Φ x) ⊢ ∀ x, □ Φ x.
-Proof. by rewrite /bi_intuitionistically persistently_forall affinely_forall. Qed.
+Proof. by rewrite /bi_intuitionistically persistently_forall_1 affinely_forall. Qed.
 Lemma intuitionistically_or P Q : □ (P ∨ Q) ⊣⊢ □ P ∨ □ Q.
 Proof. by rewrite /bi_intuitionistically persistently_or affinely_or. Qed.
 Lemma intuitionistically_exist {A} (Φ : A → PROP) : □ (∃ x, Φ x) ⊣⊢ ∃ x, □ Φ x.
@@ -1547,7 +1549,7 @@ Proof. intros. by rewrite /Persistent persistently_and -!persistent. Qed.
 Global Instance or_persistent P Q :
   Persistent P → Persistent Q → Persistent (P ∨ Q).
 Proof. intros. by rewrite /Persistent persistently_or -!persistent. Qed.
-Global Instance forall_persistent {A} (Ψ : A → PROP) :
+Global Instance forall_persistent `{!BiPersistentlyForall PROP} {A} (Ψ : A → PROP) :
   (∀ x, Persistent (Ψ x)) → Persistent (∀ x, Ψ x).
 Proof.
   intros. rewrite /Persistent persistently_forall.
diff --git a/iris/bi/extensions.v b/iris/bi/extensions.v
index 6764ebe25..e54908d50 100644
--- a/iris/bi/extensions.v
+++ b/iris/bi/extensions.v
@@ -28,6 +28,13 @@ Global Arguments löb_weak {_ _} _ _.
 Notation BiLaterContractive PROP :=
   (Contractive (bi_later (PROP:=PROP))) (only parsing).
 
+(** The class [BiPersistentlyForall] states that universal quantification
+commutes with the persistently modality. The reverse direction of the entailment
+described by this type class is derivable, so it is not included. *)
+Class BiPersistentlyForall (PROP : bi) :=
+  persistently_forall_2 : ∀ {A} (Ψ : A → PROP), (∀ a, <pers> (Ψ a)) ⊢ <pers> (∀ a, Ψ a).
+Global Hint Mode BiPersistentlyForall ! : typeclass_instances.
+
 (** The class [BiPureForall] states that universal quantification commutes with
 the embedding of pure propositions. The reverse direction of the entailment
 described by this type class is derivable, so it is not included.
@@ -36,3 +43,4 @@ An instance of [BiPureForall] itself is derivable if we assume excluded middle
 in Coq, see the lemma [bi_pure_forall_em] in [derived_laws]. *)
 Class BiPureForall (PROP : bi) :=
   pure_forall_2 : ∀ {A} (φ : A → Prop), (∀ a, ⌜ φ a ⌝) ⊢@{PROP} ⌜ ∀ a, φ a ⌝.
+Global Hint Mode BiPureForall ! : typeclass_instances.
diff --git a/iris/bi/interface.v b/iris/bi/interface.v
index a6c66ad0b..2e80cf981 100644
--- a/iris/bi/interface.v
+++ b/iris/bi/interface.v
@@ -101,8 +101,13 @@ Section bi_mixin.
     (* In the ordered RA model: [ε ≼ core x]. *)
     bi_mixin_persistently_emp_2 : emp ⊢ <pers> emp;
 
-    bi_mixin_persistently_forall_2 {A} (Ψ : A → PROP) :
-      (∀ a, <pers> (Ψ a)) ⊢ <pers> (∀ a, Ψ a);
+    (* The laws of a "frame" (https://ncatlab.org/nlab/show/frame, not to be
+    confused with separation logic terminology): commuting with finite
+    conjunction and infinite disjunction.
+    The null-ary case, [True ⊢ <pers> True], is derivable from the other laws
+    ([persistently_True]). *)
+    bi_mixin_persistently_and_2 (P Q : PROP) :
+      ((<pers> P) ∧ (<pers> Q)) ⊢ <pers> (P ∧ Q);
     bi_mixin_persistently_exist_1 {A} (Ψ : A → PROP) :
       <pers> (∃ a, Ψ a) ⊢ ∃ a, <pers> (Ψ a);
 
@@ -364,9 +369,9 @@ Proof. eapply bi_mixin_persistently_idemp_2, bi_bi_mixin. Qed.
 Lemma persistently_emp_2 : emp ⊢@{PROP} <pers> emp.
 Proof. eapply bi_mixin_persistently_emp_2, bi_bi_mixin. Qed.
 
-Lemma persistently_forall_2 {A} (Ψ : A → PROP) :
-  (∀ a, <pers> (Ψ a)) ⊢ <pers> (∀ a, Ψ a).
-Proof. eapply bi_mixin_persistently_forall_2, bi_bi_mixin. Qed.
+Lemma persistently_and_2 (P Q : PROP) :
+  ((<pers> P) ∧ (<pers> Q)) ⊢ <pers> (P ∧ Q).
+Proof. eapply bi_mixin_persistently_and_2, bi_bi_mixin. Qed.
 Lemma persistently_exist_1 {A} (Ψ : A → PROP) :
   <pers> (∃ a, Ψ a) ⊢ ∃ a, <pers> (Ψ a).
 Proof. eapply bi_mixin_persistently_exist_1, bi_bi_mixin. Qed.
diff --git a/iris/bi/lib/core.v b/iris/bi/lib/core.v
index 94d004fbd..9b4c499ab 100644
--- a/iris/bi/lib/core.v
+++ b/iris/bi/lib/core.v
@@ -26,7 +26,8 @@ Section core.
     by iApply "HPQ".
   Qed.
 
-  Global Instance coreP_persistent P : Persistent (coreP P).
+  Global Instance coreP_persistent `{!BiPersistentlyForall PROP, !BiPersistentlyImplPlainly PROP} P :
+    Persistent (coreP P).
   Proof.
     rewrite /coreP /Persistent. iIntros "HC" (Q).
     iApply persistently_wand_affinely_plainly. iIntros "#HQ".
@@ -63,7 +64,8 @@ Section core.
     [<affine>] modality makes it stronger since it appears in the LHS of the
     [⊢] in the premise. As a user, you have to prove [<affine> coreP P ⊢ Q],
     which is weaker than [coreP P ⊢ Q]. *)
-  Lemma coreP_entails P Q : (<affine> coreP P ⊢ Q) ↔ (P ⊢ <pers> Q).
+  Lemma coreP_entails `{!BiPersistentlyForall PROP, !BiPersistentlyImplPlainly PROP} P Q :
+    (<affine> coreP P ⊢ Q) ↔ (P ⊢ <pers> Q).
   Proof.
     split.
     - iIntros (HP) "HP". iDestruct (coreP_intro with "HP") as "#HcP {HP}".
@@ -71,7 +73,9 @@ Section core.
     - iIntros (->) "HcQ". by iDestruct (coreP_elim with "HcQ") as "#HQ".
   Qed.
   (** A more convenient variant of the above lemma for affine [P]. *)
-  Lemma coreP_entails' P Q `{!Affine P} : (coreP P ⊢ Q) ↔ (P ⊢ □ Q).
+  Lemma coreP_entails' `{!BiPersistentlyForall PROP, !BiPersistentlyImplPlainly PROP}
+      P Q `{!Affine P} :
+    (coreP P ⊢ Q) ↔ (P ⊢ □ Q).
   Proof.
     rewrite -(affine_affinely (coreP P)) coreP_entails. split.
     - rewrite -{2}(affine_affinely P). by intros ->.
diff --git a/iris/bi/monpred.v b/iris/bi/monpred.v
index afda962f8..d54c3a8aa 100644
--- a/iris/bi/monpred.v
+++ b/iris/bi/monpred.v
@@ -287,7 +287,7 @@ Proof.
   - intros P Q [?]. split=> i /=. by f_equiv.
   - intros P. split=> i. by apply bi.persistently_idemp_2.
   - split=> i. by apply bi.persistently_emp_intro.
-  - intros A Ψ. split=> i. by apply bi.persistently_forall_2.
+  - intros A Ψ. split=> i. by apply bi.persistently_and_2.
   - intros A Ψ. split=> i. by apply bi.persistently_exist_1.
   - intros P Q. split=> i. apply bi.sep_elim_l, _.
   - intros P Q. split=> i. by apply bi.persistently_and_sep_elim.
@@ -401,6 +401,10 @@ Proof. unseal. split. solve_proper. Qed.
 Global Instance monPred_in_flip_mono : Proper ((⊑) ==> flip (⊢)) (@monPred_in I PROP).
 Proof. solve_proper. Qed.
 
+Global Instance monPred_persistently_forall :
+  BiPersistentlyForall PROP → BiPersistentlyForall monPredI.
+Proof. intros ? A φ. split=> /= i. unseal. by apply persistently_forall_2. Qed.
+
 Global Instance monPred_pure_forall : BiPureForall PROP → BiPureForall monPredI.
 Proof. intros ? A φ. split=> /= i. unseal. by apply pure_forall_2. Qed.
 
@@ -476,7 +480,8 @@ Global Instance monPred_objectively_flip_mono' :
   Proper (flip (⊢) ==> flip (⊢)) (@monPred_objectively I PROP).
 Proof. intros ???. by apply monPred_objectively_mono. Qed.
 
-Global Instance monPred_objectively_persistent P : Persistent P → Persistent (<obj> P).
+Global Instance monPred_objectively_persistent `{!BiPersistentlyForall PROP} P :
+  Persistent P → Persistent (<obj> P).
 Proof. rewrite monPred_objectively_unfold. apply _. Qed.
 Global Instance monPred_objectively_absorbing P : Absorbing P → Absorbing (<obj> P).
 Proof. rewrite monPred_objectively_unfold. apply _. Qed.
@@ -937,10 +942,6 @@ Proof.
     rewrite -plainly_idemp_2. f_equiv. by apply bi.forall_intro=>_.
   - intros A Ψ. split=> i /=. apply bi.forall_intro=> j.
     rewrite plainly_forall. apply bi.forall_intro=> a. by rewrite !bi.forall_elim.
-  - intros P Q. split=> i /=. setoid_rewrite bi.pure_impl_forall.
-    setoid_rewrite <-plainly_forall.
-    do 2 setoid_rewrite bi.persistently_forall. do 4 f_equiv.
-    apply persistently_impl_plainly.
   - intros P Q. split=> i /=.
     setoid_rewrite bi.pure_impl_forall. rewrite 2!bi.forall_elim //.
     do 2 setoid_rewrite <-plainly_forall.
@@ -956,6 +957,17 @@ Qed.
 Global Instance monPred_bi_plainly `{BiPlainly PROP} : BiPlainly monPredI :=
   {| bi_plainly_mixin := monPred_plainly_mixin |}.
 
+Global Instance minPred_bi_persistently_impl_plainly
+     `{!BiPlainly PROP, !BiPersistentlyForall PROP, !BiPersistentlyImplPlainly PROP} :
+  BiPersistentlyImplPlainly monPredI.
+Proof.
+  intros P Q. rewrite monPred_plainly_eq. unseal.
+  split=> i /=. setoid_rewrite bi.pure_impl_forall.
+  setoid_rewrite <-plainly_forall.
+  do 2 setoid_rewrite bi.persistently_forall. do 4 f_equiv.
+  apply: persistently_impl_plainly.
+Qed.
+
 Global Instance monPred_bi_prop_ext
   `{!BiPlainly PROP, !BiInternalEq PROP, !BiPropExt PROP} : BiPropExt monPredI.
 Proof.
diff --git a/iris/bi/plainly.v b/iris/bi/plainly.v
index dff0afd99..c050f38c8 100644
--- a/iris/bi/plainly.v
+++ b/iris/bi/plainly.v
@@ -23,11 +23,9 @@ Record BiPlainlyMixin (PROP : bi) `(Plainly PROP) := {
   bi_plainly_mixin_plainly_forall_2 {A} (Ψ : A → PROP) :
     (∀ a, ■ (Ψ a)) ⊢ ■ (∀ a, Ψ a);
 
-  (* The following two laws are very similar, and indeed they hold not just
-     for persistently and plainly, but for any modality defined as `M P n x :=
-     ∀ y, R x y → P n y`. *)
-  bi_plainly_mixin_persistently_impl_plainly (P Q : PROP) :
-    (■ P → <pers> Q) ⊢ <pers> (■ P → Q);
+  (* The following law and [persistently_impl_plainly] below are very similar,
+     and indeed they hold not just for persistently and plainly, but for any
+     modality defined as `M P n x := ∀ y, R x y → P n y`. *)
   bi_plainly_mixin_plainly_impl_plainly (P Q : PROP) :
     (■ P → ■ Q) ⊢ ■ (■ P → Q);
 
@@ -45,6 +43,14 @@ Class BiPlainly (PROP : bi) := {
 Global Hint Mode BiPlainly ! : typeclass_instances.
 Global Arguments bi_plainly_plainly : simpl never.
 
+Class BiPersistentlyImplPlainly `{!BiPlainly PROP} :=
+  persistently_impl_plainly (P Q : PROP) :
+    (■ P → <pers> Q) ⊢ <pers> (■ P → Q).
+Global Arguments BiPersistentlyImplPlainly : clear implicits.
+Global Arguments BiPersistentlyImplPlainly _ {_}.
+Global Arguments persistently_impl_plainly _ {_ _} _.
+Global Hint Mode BiPersistentlyImplPlainly ! - : typeclass_instances.
+
 Class BiPlainlyExist `{!BiPlainly PROP} :=
   plainly_exist_1 A (Ψ : A → PROP) :
     ■ (∃ a, Ψ a) ⊢ ∃ a, ■ (Ψ a).
@@ -75,8 +81,6 @@ Section plainly_laws.
   Proof. eapply bi_plainly_mixin_plainly_idemp_2, bi_plainly_mixin. Qed.
   Lemma plainly_forall_2 {A} (Ψ : A → PROP) : (∀ a, ■ (Ψ a)) ⊢ ■ (∀ a, Ψ a).
   Proof. eapply bi_plainly_mixin_plainly_forall_2, bi_plainly_mixin. Qed.
-  Lemma persistently_impl_plainly P Q : (■ P → <pers> Q) ⊢ <pers> (■ P → Q).
-  Proof. eapply bi_plainly_mixin_persistently_impl_plainly, bi_plainly_mixin. Qed.
   Lemma plainly_impl_plainly P Q : (■ P → ■ Q) ⊢ ■ (■ P → Q).
   Proof. eapply bi_plainly_mixin_plainly_impl_plainly, bi_plainly_mixin. Qed.
   Lemma plainly_absorb P Q : ■ P ∗ Q ⊢ ■ P.
@@ -270,9 +274,9 @@ Proof. apply impl_intro_l. by rewrite plainly_and_sep_l_1 wand_elim_r. Qed.
 Lemma impl_wand_affinely_plainly P Q : (■ P → Q) ⊣⊢ (<affine> ■ P -∗ Q).
 Proof. by rewrite -(persistently_elim_plainly P) impl_wand_intuitionistically. Qed.
 
-Lemma persistently_wand_affinely_plainly P Q :
+Lemma persistently_wand_affinely_plainly `{!BiPersistentlyImplPlainly PROP} P Q :
   (<affine> ■ P -∗ <pers> Q) ⊢ <pers> (<affine> ■ P -∗ Q).
-Proof. rewrite -!impl_wand_affinely_plainly. apply persistently_impl_plainly. Qed.
+Proof. rewrite -!impl_wand_affinely_plainly. apply: persistently_impl_plainly. Qed.
 
 Lemma plainly_wand_affinely_plainly P Q :
   (<affine> ■ P -∗ ■ Q) ⊢ ■ (<affine> ■ P -∗ Q).
@@ -362,7 +366,7 @@ Proof. intros; destruct p; simpl; apply _. Qed.
 Lemma plain_persistent P : Plain P → Persistent P.
 Proof. intros. by rewrite /Persistent -plainly_elim_persistently. Qed.
 
-Global Instance impl_persistent P Q :
+Global Instance impl_persistent `{!BiPersistentlyImplPlainly PROP} P Q :
   Absorbing P → Plain P → Persistent Q → Persistent (P → Q).
 Proof.
   intros. by rewrite /Persistent {2}(plain P) -persistently_impl_plainly
@@ -372,7 +376,7 @@ Qed.
 Global Instance plainly_persistent P : Persistent (â–  P).
 Proof. by rewrite /Persistent persistently_elim_plainly. Qed.
 
-Global Instance wand_persistent P Q :
+Global Instance wand_persistent `{!BiPersistentlyImplPlainly PROP} P Q :
   Plain P → Persistent Q → Absorbing Q → Persistent (P -∗ Q).
 Proof.
   intros. rewrite /Persistent {2}(plain P). trans (<pers> (■ P → Q))%I.
diff --git a/iris/bi/telescopes.v b/iris/bi/telescopes.v
index 66bde8307..67d8df26c 100644
--- a/iris/bi/telescopes.v
+++ b/iris/bi/telescopes.v
@@ -71,7 +71,7 @@ Section telescopes.
   Global Instance bi_tforall_absorbing Ψ :
     (∀ x, Absorbing (Ψ x)) → Absorbing (∀.. x, Ψ x).
   Proof. rewrite bi_tforall_forall. apply _. Qed.
-  Global Instance bi_tforall_persistent Ψ :
+  Global Instance bi_tforall_persistent `{!BiPersistentlyForall PROP} Ψ :
     (∀ x, Persistent (Ψ x)) → Persistent (∀.. x, Ψ x).
   Proof. rewrite bi_tforall_forall. apply _. Qed.
 
diff --git a/iris/proofmode/class_instances.v b/iris/proofmode/class_instances.v
index d63b2fae9..2e7b93e3d 100644
--- a/iris/proofmode/class_instances.v
+++ b/iris/proofmode/class_instances.v
@@ -937,7 +937,7 @@ Proof. rewrite /IntoForall=> HP. by rewrite HP affinely_forall. Qed.
 Global Instance into_forall_intuitionistically {A} P (Φ : A → PROP) :
   IntoForall P Φ → IntoForall (□ P) (λ a, □ (Φ a))%I.
 Proof. rewrite /IntoForall=> HP. by rewrite HP intuitionistically_forall. Qed.
-Global Instance into_forall_persistently {A} P (Φ : A → PROP) :
+Global Instance into_forall_persistently `{!BiPersistentlyForall PROP} {A} P (Φ : A → PROP) :
   IntoForall P Φ → IntoForall (<pers> P) (λ a, <pers> (Φ a))%I.
 Proof. rewrite /IntoForall=> HP. by rewrite HP persistently_forall. Qed.
 
@@ -1003,13 +1003,15 @@ Proof.
   - by rewrite (into_pure P) -pure_wand_forall wand_elim_l.
 Qed.
 
-Global Instance from_forall_intuitionistically `{BiAffine PROP} {A} P (Φ : A → PROP) name :
+Global Instance from_forall_intuitionistically `{!BiAffine PROP, !BiPersistentlyForall PROP}
+    {A} P (Φ : A → PROP) name :
   FromForall P Φ name → FromForall (□ P) (λ a, □ (Φ a))%I name.
 Proof.
   rewrite /FromForall=> <-. setoid_rewrite intuitionistically_into_persistently.
   by rewrite persistently_forall.
 Qed.
-Global Instance from_forall_persistently {A} P (Φ : A → PROP) name :
+Global Instance from_forall_persistently `{!BiPersistentlyForall PROP}
+    {A} P (Φ : A → PROP) name :
   FromForall P Φ name → FromForall (<pers> P) (λ a, <pers> (Φ a))%I name.
 Proof. rewrite /FromForall=> <-. by rewrite persistently_forall. Qed.
 
diff --git a/tests/bi.v b/tests/bi.v
index 1dc3b77c6..87f512560 100644
--- a/tests/bi.v
+++ b/tests/bi.v
@@ -1,10 +1,10 @@
 From iris.bi Require Import bi plainly.
 
 (** See https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/610 *)
-Lemma test_impl_persistent_1 `{!BiPlainly PROP} :
+Lemma test_impl_persistent_1 `{!BiPlainly PROP, !BiPersistentlyImplPlainly PROP} :
   Persistent (PROP:=PROP) (True → True).
 Proof. apply _. Qed.
-Lemma test_impl_persistent_2 `{!BiPlainly PROP} :
+Lemma test_impl_persistent_2 `{!BiPlainly PROP, !BiPersistentlyImplPlainly PROP} :
   Persistent (PROP:=PROP) (True → True → True).
 Proof. apply _. Qed.
 
diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index d03482932..d4a763178 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -3,6 +3,7 @@
 1 goal
   
   PROP : bi
+  BiPersistentlyForall0 : BiPersistentlyForall PROP
   P, Q : PROP
   ============================
   "H2" : ∀ x : nat, ⌜x = 0⌝ ∨ ⌜x = 1⌝
@@ -13,6 +14,7 @@
 1 goal
   
   PROP : bi
+  BiPersistentlyForall0 : BiPersistentlyForall PROP
   P, Q : PROP
   ============================
   "H2" : ∀ x : nat, ⌜x = 0⌝ ∨ ⌜x = 1⌝
diff --git a/tests/proofmode.v b/tests/proofmode.v
index fa820d1ff..73027cdbd 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -22,7 +22,8 @@ Proof.
 Qed.
 
 Check "demo_0".
-Lemma demo_0 P Q : □ (P ∨ Q) -∗ (∀ x, ⌜x = 0⌝ ∨ ⌜x = 1⌝) → (Q ∨ P).
+Lemma demo_0 `{!BiPersistentlyForall PROP} P Q :
+  □ (P ∨ Q) -∗ (∀ x, ⌜x = 0⌝ ∨ ⌜x = 1⌝) → (Q ∨ P).
 Proof.
   iIntros "H #H2". Show. iDestruct "H" as "###H".
   (* should remove the disjunction "H" *)
@@ -701,7 +702,7 @@ Proof.
   iIntros "#HPQ HQ !>". iNext. by iRewrite "HPQ" in "HQ".
 Qed.
 
-Lemma test_iIntros_modalities `(!Absorbing P) :
+Lemma test_iIntros_modalities `{!BiPersistentlyForall PROP} `(!Absorbing P) :
   ⊢ <pers> (▷ ∀  x : nat, ⌜ x = 0 ⌝ → ⌜ x = 0 ⌝ -∗ False -∗ P -∗ P).
 Proof.
   iIntros (x ??).
diff --git a/tests/proofmode_monpred.v b/tests/proofmode_monpred.v
index 66d9f61aa..b9da25e42 100644
--- a/tests/proofmode_monpred.v
+++ b/tests/proofmode_monpred.v
@@ -72,14 +72,15 @@ Section tests.
     iIntros "H HP". by iApply "H".
   Qed.
 
-  Lemma test_objectively P Q : <obj> emp -∗ <obj> P -∗ <obj> Q -∗ <obj> (P ∗ Q).
+  Lemma test_objectively `{!BiPersistentlyForall PROP} P Q :
+    <obj> emp -∗ <obj> P -∗ <obj> Q -∗ <obj> (P ∗ Q).
   Proof. iIntros "#? HP HQ". iModIntro. by iSplitL "HP". Qed.
 
-  Lemma test_objectively_absorbing P Q R `{!Absorbing P} :
+  Lemma test_objectively_absorbing `{!BiPersistentlyForall PROP} P Q R `{!Absorbing P} :
     <obj> emp -∗ <obj> P -∗ <obj> Q -∗ R -∗ <obj> (P ∗ Q).
   Proof. iIntros "#? HP HQ HR". iModIntro. by iSplitL "HP". Qed.
 
-  Lemma test_objectively_affine P Q R `{!Affine R} :
+  Lemma test_objectively_affine `{!BiPersistentlyForall PROP} P Q R `{!Affine R} :
     <obj> emp -∗ <obj> P -∗ <obj> Q -∗ R -∗ <obj> (P ∗ Q).
   Proof. iIntros "#? HP HQ HR". iModIntro. by iSplitL "HP". Qed.
 
diff --git a/tests/telescopes.v b/tests/telescopes.v
index 1e7fcc3e5..74df376f9 100644
--- a/tests/telescopes.v
+++ b/tests/telescopes.v
@@ -32,7 +32,7 @@ Section basic_tests.
   Lemma test_pure_tforall `{!BiPureForall PROP} {TT : tele} (φ : TT → Prop) :
     (∀.. x, ⌜ φ x ⌝) -∗ ∀.. x, ⌜ φ x ⌝ : PROP.
   Proof. iIntros (H) "!%". done. Qed.
-  Lemma test_pure_tforall_persistent {TT : tele} (Φ : TT → PROP) :
+  Lemma test_pure_tforall_persistent `{!BiPersistentlyForall PROP} {TT : tele} (Φ : TT → PROP) :
     (∀.. x, <pers> (Φ x)) -∗ <pers> ∀.. x, Φ x.
   Proof. iIntros "#H !>" (x). done. Qed.
   Lemma test_pure_texists_intuitionistic {TT : tele} (Φ : TT → PROP) :
-- 
GitLab