Remove notations for bi_bare and bi_persistently.

(□ P) now means (bi_bare (bi_persistently P)).

This is motivated by the fact that these two modalities are rarely
used separately.

In the case of an affine BI, we keep the □ notation. This means that a
bi_bare is inserted each time we use □. Hence, a few adaptations need
to be done in the proof mode class instances.

theories/base_logic/derived.v

@@ -36,9 +36,9 @@ Global Instance uPred_affine : AffineBI (uPredI M) | 0.
 Proof. intros P. rewrite /Affine. by apply bi.pure_intro. Qed.
 
 (* Own and valid derived *)
-Lemma persistently_ownM (a : M) : CoreId a → □ uPred_ownM a ⊣⊢ uPred_ownM a.
+Lemma bare_persistently_ownM (a : M) : CoreId a → □ uPred_ownM a ⊣⊢ uPred_ownM a.
 Proof.
-  intros; apply (anti_symm _); first by rewrite persistently_elim.
+  rewrite affine_bare=>?; apply (anti_symm _); [by rewrite persistently_elim|].
   by rewrite {1}persistently_ownM_core core_id_core.
 Qed.
 Lemma ownM_invalid (a : M) : ¬ ✓{0} a → uPred_ownM a ⊢ False.
@@ -47,9 +47,9 @@ Global Instance ownM_mono : Proper (flip (≼) ==> (⊢)) (@uPred_ownM M).
 Proof. intros a b [b' ->]. by rewrite ownM_op sep_elim_l. Qed.
 Lemma ownM_unit' : uPred_ownM ε ⊣⊢ True.
 Proof. apply (anti_symm _); first by apply pure_intro. apply ownM_empty. Qed.
-Lemma persistently_cmra_valid {A : cmraT} (a : A) : □ ✓ a ⊣⊢ ✓ a.
+Lemma bare_persistently_cmra_valid {A : cmraT} (a : A) : □ ✓ a ⊣⊢ ✓ a.
 Proof.
-  intros; apply (anti_symm _); first by rewrite persistently_elim.
+  rewrite affine_bare. intros; apply (anti_symm _); first by rewrite persistently_elim.
   apply:persistently_cmra_valid_1.
 Qed.
 
@@ -98,9 +98,11 @@ Proof. intros. apply limit_preserving_entails; solve_proper. Qed.
 (* Persistence *)
 Global Instance cmra_valid_persistent {A : cmraT} (a : A) :
   Persistent (✓ a : uPred M)%I.
-Proof. by intros; rewrite /Persistent persistently_cmra_valid. Qed.
-Global Instance ownM_persistent : CoreId a → Persistent (@uPred_ownM M a).
-Proof. intros. by rewrite /Persistent persistently_ownM. Qed.
+Proof. rewrite /Persistent. apply persistently_cmra_valid_1. Qed.
+Global Instance ownM_persistent a : CoreId a → Persistent (@uPred_ownM M a).
+Proof.
+  intros. rewrite /Persistent -{2}(core_id_core a). apply persistently_ownM_core.
+Qed.
 
 (* For big ops *)
 Global Instance uPred_ownM_sep_homomorphism :

theories/base_logic/lib/viewshifts.v

@@ -81,5 +81,8 @@ Lemma vs_alloc N P : ▷ P ={↑N}=> inv N P.
 Proof. iIntros "!# HP". by iApply inv_alloc. Qed.
 
 Lemma wand_fupd_alt E1 E2 P Q : (P ={E1,E2}=∗ Q) ⊣⊢ ∃ R, R ∗ (P ∗ R ={E1,E2}=> Q).
-Proof. rewrite bi.wand_alt. by setoid_rewrite bi.persistently_impl_wand. Qed.
+Proof.
+  rewrite bi.wand_alt. do 2 f_equiv. setoid_rewrite bi.affine_bare; last apply _.
+  by rewrite bi.persistently_impl_wand.
+Qed.
 End vs.

theories/base_logic/upred.v

@@ -438,21 +438,21 @@ Proof.
   - (* (P ⊢ Q -∗ R) → P ∗ Q ⊢ R *)
     intros P Q R. unseal=> HPQR. split; intros n x ? (?&?&?&?&?). ofe_subst.
     eapply HPQR; eauto using cmra_validN_op_l.
-  - (* (P ⊢ Q) → □ P ⊢ □ Q *)
+  - (* (P ⊢ Q) → bi_persistently P ⊢ bi_persistently Q *)
     intros P QR HP. unseal; split=> n x ? /=. by apply HP, cmra_core_validN.
-  - (* □ P ⊢ □ □ P *)
+  - (* bi_persistently P ⊢ bi_persistently (bi_persistently P) *)
     intros P. unseal; split=> n x ?? /=. by rewrite cmra_core_idemp.
-  - (* (∀ a, □ Ψ a) ⊢ □ ∀ a, Ψ a *)
+  - (* (∀ a, bi_persistently (Ψ a)) ⊢ bi_persistently (∀ a, Ψ a) *)
     by unseal.
-  - (* □ (∃ a, Ψ a) ⊢ ∃ a, □ Ψ a *)
+  - (* bi_persistently (∃ a, Ψ a) ⊢ ∃ a, bi_persistently (Ψ a) *)
     by unseal.
-  - (* P ⊢ □ emp (ADMISSIBLE) *)
+  - (* P ⊢ bi_persistently emp (ADMISSIBLE) *)
     intros P. unfold uPred_emp; unseal; by split=> n x ? _.
-  - (* □ P ∗ Q ⊢ □ P (ADMISSIBLE) *)
+  - (* bi_persistently P ∗ Q ⊢ bi_persistently P (ADMISSIBLE) *)
     intros P Q. move: (uPred_persistently P)=> P'.
     unseal; split; intros n x ? (x1&x2&?&?&_); ofe_subst;
       eauto using uPred_mono, cmra_includedN_l.
-  - (* □ P ∧ Q ⊢ (emp ∧ P) ∗ Q *)
+  - (* bi_persistently P ∧ Q ⊢ (emp ∧ P) ∗ Q *)
     intros P Q. unseal; split=> n x ? [??]; simpl in *.
     exists (core x), x; rewrite ?cmra_core_l; auto.
 Qed.
@@ -489,9 +489,9 @@ Proof.
   - (* ▷ P ∗ ▷ Q ⊢ ▷ (P ∗ Q) *)
     intros P Q. unseal; split=> -[|n] x ? /=; [done|intros (x1&x2&Hx&?&?)].
     exists x1, x2; eauto using dist_S.
-  - (* ▷ □ P ⊢ □ ▷ P *)
+  - (* ▷ bi_persistently P ⊢ bi_persistently (▷ P) *)
     by unseal.
-  - (* □ ▷ P ⊢ ▷ □ P *)
+  - (* bi_persistently (▷ P) ⊢ ▷ bi_persistently P *)
     by unseal.
   - (* ▷ P ⊢ ▷ False ∨ (▷ False → P) *)
     intros P. unseal; split=> -[|n] x ? /= HP; [by left|right].
@@ -570,7 +570,8 @@ Proof.
     by rewrite (assoc op _ z1) -(comm op z1) (assoc op z1)
       -(assoc op _ a2) (comm op z1) -Hy1 -Hy2.
 Qed.
-Lemma persistently_ownM_core (a : M) : uPred_ownM a ⊢ □ uPred_ownM (core a).
+Lemma persistently_ownM_core (a : M) :
+  uPred_ownM a ⊢ bi_persistently (uPred_ownM (core a)).
 Proof.
   rewrite /bi_persistently /=. unseal.
   split=> n x Hx /=. by apply cmra_core_monoN.
@@ -601,7 +602,8 @@ Lemma cmra_valid_elim {A : cmraT} (a : A) : ¬ ✓{0} a → ✓ a ⊢ (False : u
 Proof.
   intros Ha. unseal. split=> n x ??; apply Ha, cmra_validN_le with n; auto.
 Qed.
-Lemma persistently_cmra_valid_1 {A : cmraT} (a : A) : ✓ a ⊢ □ (✓ a : uPred M).
+Lemma persistently_cmra_valid_1 {A : cmraT} (a : A) :
+  ✓ a ⊢ bi_persistently (✓ a : uPred M).
 Proof. by unseal. Qed.
 Lemma cmra_valid_weaken {A : cmraT} (a b : A) : ✓ (a ⋅ b) ⊢ (✓ a : uPred M).
 Proof. unseal; split=> n x _; apply cmra_validN_op_l. Qed.

theories/bi/big_op.v

@@ -126,7 +126,8 @@ Section sep_list.
   Proof. auto using and_intro, big_sepL_mono, and_elim_l, and_elim_r. Qed.
 
   Lemma big_sepL_persistently `{AffineBI PROP} Φ l :
-    (□ [∗ list] k↦x ∈ l, Φ k x) ⊣⊢ ([∗ list] k↦x ∈ l, □ Φ k x).
+    (bi_persistently ([∗ list] k↦x ∈ l, Φ k x)) ⊣⊢
+    ([∗ list] k↦x ∈ l, bi_persistently (Φ k x)).
   Proof. apply (big_opL_commute _). Qed.
 
   Lemma big_sepL_forall `{AffineBI PROP} Φ l :
@@ -144,12 +145,12 @@ Section sep_list.
 
   Lemma big_sepL_impl Φ Ψ l :
     ([∗ list] k↦x ∈ l, Φ k x) -∗
-    ⬕ (∀ k x, ⌜l !! k = Some x⌝ → Φ k x -∗ Ψ k x) -∗
+    □ (∀ k x, ⌜l !! k = Some x⌝ → Φ k x -∗ Ψ k x) -∗
     [∗ list] k↦x ∈ l, Ψ k x.
   Proof.
     apply wand_intro_l. revert Φ Ψ. induction l as [|x l IH]=> Φ Ψ /=.
     { by rewrite sep_elim_r. }
-    rewrite bare_persistently_sep_dup -assoc [(⬕ _ ∗ _)%I]comm -!assoc assoc.
+    rewrite bare_persistently_sep_dup -assoc [(□ _ ∗ _)%I]comm -!assoc assoc.
     apply sep_mono.
     - rewrite (forall_elim 0) (forall_elim x) pure_True // True_impl.
       by rewrite bare_persistently_elim wand_elim_l.
@@ -264,7 +265,8 @@ Section and_list.
   Proof. auto using and_intro, big_andL_mono, and_elim_l, and_elim_r. Qed.
 
   Lemma big_andL_persistently Φ l :
-    (□ [∧ list] k↦x ∈ l, Φ k x) ⊣⊢ ([∧ list] k↦x ∈ l, □ Φ k x).
+    (bi_persistently ([∧ list] k↦x ∈ l, Φ k x)) ⊣⊢
+    ([∧ list] k↦x ∈ l, bi_persistently (Φ k x)).
   Proof. apply (big_opL_commute _). Qed.
 
   Lemma big_andL_forall `{AffineBI PROP} Φ l :
@@ -394,7 +396,8 @@ Section gmap.
   Proof. auto using and_intro, big_sepM_mono, and_elim_l, and_elim_r. Qed.
 
   Lemma big_sepM_persistently `{AffineBI PROP} Φ m :
-    (□ [∗ map] k↦x ∈ m, Φ k x) ⊣⊢ ([∗ map] k↦x ∈ m, □ Φ k x).
+    (bi_persistently ([∗ map] k↦x ∈ m, Φ k x)) ⊣⊢
+      ([∗ map] k↦x ∈ m, bi_persistently (Φ k x)).
   Proof. apply (big_opM_commute _). Qed.
 
   Lemma big_sepM_forall `{AffineBI PROP} Φ m :
@@ -416,13 +419,13 @@ Section gmap.
 
   Lemma big_sepM_impl Φ Ψ m :
     ([∗ map] k↦x ∈ m, Φ k x) -∗
-    ⬕ (∀ k x, ⌜m !! k = Some x⌝ → Φ k x -∗ Ψ k x) -∗
+    □ (∀ k x, ⌜m !! k = Some x⌝ → Φ k x -∗ Ψ k x) -∗
     [∗ map] k↦x ∈ m, Ψ k x.
   Proof.
     apply wand_intro_l. induction m as [|i x m ? IH] using map_ind.
     { by rewrite sep_elim_r. }
     rewrite !big_sepM_insert // bare_persistently_sep_dup.
-    rewrite -assoc [(⬕ _ ∗ _)%I]comm -!assoc assoc. apply sep_mono.
+    rewrite -assoc [(□ _ ∗ _)%I]comm -!assoc assoc. apply sep_mono.
     - rewrite (forall_elim i) (forall_elim x) pure_True ?lookup_insert //.
       by rewrite True_impl bare_persistently_elim wand_elim_l.
     - rewrite comm -IH /=.
@@ -559,7 +562,7 @@ Section gset.
   Proof. auto using and_intro, big_sepS_mono, and_elim_l, and_elim_r. Qed.
 
   Lemma big_sepS_persistently `{AffineBI PROP} Φ X :
-    □ ([∗ set] y ∈ X, Φ y) ⊣⊢ ([∗ set] y ∈ X, □ Φ y).
+    bi_persistently ([∗ set] y ∈ X, Φ y) ⊣⊢ ([∗ set] y ∈ X, bi_persistently (Φ y)).
   Proof. apply (big_opS_commute _). Qed.
 
   Lemma big_sepS_forall `{AffineBI PROP} Φ X :
@@ -577,13 +580,13 @@ Section gset.
 
   Lemma big_sepS_impl Φ Ψ X :
     ([∗ set] x ∈ X, Φ x) -∗
-    ⬕ (∀ x, ⌜x ∈ X⌝ → Φ x -∗ Ψ x) -∗
+    □ (∀ x, ⌜x ∈ X⌝ → Φ x -∗ Ψ x) -∗
     [∗ set] x ∈ X, Ψ x.
   Proof.
     apply wand_intro_l. induction X as [|x X ? IH] using collection_ind_L.
     { by rewrite sep_elim_r. }
     rewrite !big_sepS_insert // bare_persistently_sep_dup.
-    rewrite -assoc [(⬕ _ ∗ _)%I]comm -!assoc assoc. apply sep_mono.
+    rewrite -assoc [(□ _ ∗ _)%I]comm -!assoc assoc. apply sep_mono.
     - rewrite (forall_elim x) pure_True; last set_solver.
       by rewrite True_impl bare_persistently_elim wand_elim_l.
     - rewrite comm -IH /=. apply sep_mono_l, bare_mono, persistently_mono.
@@ -667,7 +670,8 @@ Section gmultiset.
   Proof. auto using and_intro, big_sepMS_mono, and_elim_l, and_elim_r. Qed.
 
   Lemma big_sepMS_persistently `{AffineBI PROP} Φ X :
-    □ ([∗ mset] y ∈ X, Φ y) ⊣⊢ ([∗ mset] y ∈ X, □ Φ y).
+    bi_persistently ([∗ mset] y ∈ X, Φ y) ⊣⊢
+      ([∗ mset] y ∈ X, bi_persistently (Φ y)).
   Proof. apply (big_opMS_commute _). Qed.
 
   Global Instance big_sepMS_empty_persistent Φ :

theories/bi/fixpoint.v

@@ -6,7 +6,7 @@ Import bi.
 (** Least and greatest fixpoint of a monotone function, defined entirely inside
     the logic.  *)
 Class BIMonoPred {PROP : bi} {A : ofeT} (F : (A → PROP) → (A → PROP)) := {
-  bi_mono_pred Φ Ψ : ((□ ∀ x, Φ x -∗ Ψ x) → ∀ x, F Φ x -∗ F Ψ x)%I;
+  bi_mono_pred Φ Ψ : ((bi_persistently (∀ x, Φ x -∗ Ψ x)) → ∀ x, F Φ x -∗ F Ψ x)%I;
   bi_mono_pred_ne Φ : NonExpansive Φ → NonExpansive (F Φ)
 }.
 Arguments bi_mono_pred {_ _ _ _} _ _.
@@ -14,11 +14,11 @@ Local Existing Instance bi_mono_pred_ne.
 
 Definition bi_least_fixpoint {PROP : bi} {A : ofeT}
     (F : (A → PROP) → (A → PROP)) (x : A) : PROP :=
-  (∀ Φ : A -n> PROP, □ (∀ x, F Φ x -∗ Φ x) → Φ x)%I.
+  (∀ Φ : A -n> PROP, bi_persistently (∀ x, F Φ x -∗ Φ x) → Φ x)%I.
 
 Definition bi_greatest_fixpoint {PROP : bi} {A : ofeT}
     (F : (A → PROP) → (A → PROP)) (x : A) : PROP :=
-  (∃ Φ : A -n> PROP, □ (∀ x, Φ x -∗ F Φ x) ∧ Φ x)%I.
+  (∃ Φ : A -n> PROP, bi_persistently (∀ x, Φ x -∗ F Φ x) ∧ Φ x)%I.
 
 Section least.
   Context {PROP : bi} {A : ofeT} (F : (A → PROP) → (A → PROP)) `{!BIMonoPred F}.
@@ -48,13 +48,13 @@ Section least.
   Qed.
 
   Lemma least_fixpoint_ind (Φ : A → PROP) `{!NonExpansive Φ} :
-    ⬕ (∀ y, F Φ y -∗ Φ y) -∗ ∀ x, bi_least_fixpoint F x -∗ Φ x.
+    □ (∀ y, F Φ y -∗ Φ y) -∗ ∀ x, bi_least_fixpoint F x -∗ Φ x.
   Proof.
     iIntros "#HΦ" (x) "HF". by iApply ("HF" $! (CofeMor Φ) with "[#]").
   Qed.
 
   Lemma least_fixpoint_strong_ind (Φ : A → PROP) `{!NonExpansive Φ} :
-    ⬕ (∀ y, F (λ x, Φ x ∧ bi_least_fixpoint F x) y -∗ Φ y) -∗
+    □ (∀ y, F (λ x, Φ x ∧ bi_least_fixpoint F x) y -∗ Φ y) -∗
     ∀ x, bi_least_fixpoint F x -∗ Φ x.
   Proof.
     trans (∀ x, bi_least_fixpoint F x -∗ Φ x ∧ bi_least_fixpoint F x)%I.
@@ -96,6 +96,6 @@ Section greatest.
   Qed.
 
   Lemma greatest_fixpoint_coind (Φ : A → PROP) `{!NonExpansive Φ} :
-    ⬕ (∀ y, Φ y -∗ F Φ y) -∗ ∀ x, Φ x -∗ bi_greatest_fixpoint F x.
+    □ (∀ y, Φ y -∗ F Φ y) -∗ ∀ x, Φ x -∗ bi_greatest_fixpoint F x.
   Proof. iIntros "#HΦ" (x) "Hx". iExists (CofeMor Φ). auto. Qed.
 End greatest.

theories/bi/interface.v

@@ -5,7 +5,6 @@ Reserved Notation "'emp'".
 Reserved Notation "'⌜' φ '⌝'" (at level 1, φ at level 200, format "⌜ φ ⌝").
 Reserved Notation "P ∗ Q" (at level 80, right associativity).
 Reserved Notation "P -∗ Q" (at level 99, Q at level 200, right associativity).
-Reserved Notation "□ P" (at level 20, right associativity).
 Reserved Notation "▷ P" (at level 20, right associativity).
 
 Section bi_mixin.
@@ -39,7 +38,6 @@ Section bi_mixin.
   Local Notation "x ≡ y" := (bi_internal_eq _ x y).
   Local Infix "∗" := bi_sep.
   Local Infix "-∗" := bi_wand.
-  Local Notation "□ P" := (bi_persistently P).
   Local Notation "▷ P" := (bi_later P).
 
   Record BIMixin := {
@@ -100,17 +98,21 @@ Section bi_mixin.
     bi_mixin_wand_elim_l' P Q R : (P ⊢ Q -∗ R) → P ∗ Q ⊢ R;
 
     (* Persistently *)
-    bi_mixin_persistently_mono P Q : (P ⊢ Q) → □ P ⊢ □ Q;
-    bi_mixin_persistently_idemp_2 P : □ P ⊢ □ □ P;
+    bi_mixin_persistently_mono P Q :
+      (P ⊢ Q) → bi_persistently P ⊢ bi_persistently Q;
+    bi_mixin_persistently_idemp_2 P :
+      bi_persistently P ⊢ bi_persistently (bi_persistently P);
 
     bi_mixin_persistently_forall_2 {A} (Ψ : A → PROP) :
-      (∀ a, □ Ψ a) ⊢ □ ∀ a, Ψ a;
+      (∀ a, bi_persistently (Ψ a)) ⊢ bi_persistently (∀ a, Ψ a);
     bi_mixin_persistently_exist_1 {A} (Ψ : A → PROP) :
-      □ (∃ a, Ψ a) ⊢ ∃ a, □ Ψ a;
+      bi_persistently (∃ a, Ψ a) ⊢ ∃ a, bi_persistently (Ψ a);
 
-    bi_mixin_persistently_emp_intro P : P ⊢ □ emp;
-    bi_mixin_persistently_absorbing P Q : □ P ∗ Q ⊢ □ P;
-    bi_mixin_persistently_and_sep_elim P Q : □ P ∧ Q ⊢ (emp ∧ P) ∗ Q;
+    bi_mixin_persistently_emp_intro P : P ⊢ bi_persistently emp;
+    bi_mixin_persistently_absorbing P Q :
+      bi_persistently P ∗ Q ⊢ bi_persistently P;
+    bi_mixin_persistently_and_sep_elim P Q :
+      bi_persistently P ∧ Q ⊢ (emp ∧ P) ∗ Q;
   }.
 
   Record SBIMixin := {
@@ -127,8 +129,10 @@ Section bi_mixin.
       (▷ ∃ a, Φ a) ⊢ ▷ False ∨ (∃ a, ▷ Φ a);
     sbi_mixin_later_sep_1 P Q : ▷ (P ∗ Q) ⊢ ▷ P ∗ ▷ Q;
     sbi_mixin_later_sep_2 P Q : ▷ P ∗ ▷ Q ⊢ ▷ (P ∗ Q);
-    sbi_mixin_later_persistently_1 P : ▷ □ P ⊢ □ ▷ P;
-    sbi_mixin_later_persistently_2 P : □ ▷ P ⊢ ▷ □ P;
+    sbi_mixin_later_persistently_1 P :
+      ▷ bi_persistently P ⊢ bi_persistently (▷ P);
+    sbi_mixin_later_persistently_2 P :
+      bi_persistently (▷ P) ⊢ ▷ bi_persistently P;
 
     sbi_mixin_later_false_em P : ▷ P ⊢ ▷ False ∨ (▷ False → P);
   }.
@@ -281,7 +285,6 @@ Notation "∀ x .. y , P" :=
   (bi_forall (λ x, .. (bi_forall (λ y, P)) ..)%I) : bi_scope.
 Notation "∃ x .. y , P" :=
   (bi_exist (λ x, .. (bi_exist (λ y, P)) ..)%I) : bi_scope.
-Notation "□ P" := (bi_persistently P) : bi_scope.
 
 Infix "≡" := bi_internal_eq : bi_scope.
 Notation "▷ P" := (bi_later P) : bi_scope.
@@ -399,21 +402,24 @@ Lemma wand_elim_l' P Q R : (P ⊢ Q -∗ R) → P ∗ Q ⊢ R.
 Proof. eapply bi_mixin_wand_elim_l', bi_bi_mixin. Qed.
 
 (* Persistently *)
-Lemma persistently_mono P Q : (P ⊢ Q) → □ P ⊢ □ Q.
+Lemma persistently_mono P Q : (P ⊢ Q) → bi_persistently P ⊢ bi_persistently Q.
 Proof. eapply bi_mixin_persistently_mono, bi_bi_mixin. Qed.
-Lemma persistently_idemp_2 P : □ P ⊢ □ □ P.
+Lemma persistently_idemp_2 P :
+  bi_persistently P ⊢ bi_persistently (bi_persistently P).
 Proof. eapply bi_mixin_persistently_idemp_2, bi_bi_mixin. Qed.
 
-Lemma persistently_forall_2 {A} (Ψ : A → PROP) : (∀ a, □ Ψ a) ⊢ □ ∀ a, Ψ a.
+Lemma persistently_forall_2 {A} (Ψ : A → PROP) :
+  (∀ a, bi_persistently (Ψ a)) ⊢ bi_persistently (∀ a, Ψ a).
 Proof. eapply bi_mixin_persistently_forall_2, bi_bi_mixin. Qed.
-Lemma persistently_exist_1 {A} (Ψ : A → PROP) : □ (∃ a, Ψ a) ⊢ ∃ a, □ Ψ a.
+Lemma persistently_exist_1 {A} (Ψ : A → PROP) :
+  bi_persistently (∃ a, Ψ a) ⊢ ∃ a, bi_persistently (Ψ a).
 Proof. eapply bi_mixin_persistently_exist_1, bi_bi_mixin. Qed.
 
-Lemma persistently_emp_intro P : P ⊢ □ emp.
+Lemma persistently_emp_intro P : P ⊢ bi_persistently emp.
 Proof. eapply bi_mixin_persistently_emp_intro, bi_bi_mixin. Qed.
-Lemma persistently_absorbing P Q : □ P ∗ Q ⊢ □ P.
+Lemma persistently_absorbing P Q : bi_persistently P ∗ Q ⊢ bi_persistently P.
 Proof. eapply (bi_mixin_persistently_absorbing bi_entails), bi_bi_mixin. Qed.
-Lemma persistently_and_sep_elim P Q : □ P ∧ Q ⊢ (emp ∧ P) ∗ Q.
+Lemma persistently_and_sep_elim P Q : bi_persistently P ∧ Q ⊢ (emp ∧ P) ∗ Q.
 Proof. eapply bi_mixin_persistently_and_sep_elim, bi_bi_mixin. Qed.
 End bi_laws.
 
@@ -444,9 +450,9 @@ Lemma later_sep_1 P Q : ▷ (P ∗ Q) ⊢ ▷ P ∗ ▷ Q.
 Proof. eapply sbi_mixin_later_sep_1, sbi_sbi_mixin. Qed.
 Lemma later_sep_2 P Q : ▷ P ∗ ▷ Q ⊢ ▷ (P ∗ Q).
 Proof. eapply sbi_mixin_later_sep_2, sbi_sbi_mixin. Qed.
-Lemma later_persistently_1 P : ▷ □ P ⊢ □ ▷ P.
+Lemma later_persistently_1 P : ▷ bi_persistently P ⊢ bi_persistently (▷ P).
 Proof. eapply (sbi_mixin_later_persistently_1 bi_entails), sbi_sbi_mixin. Qed.
-Lemma later_persistently_2 P : □ ▷ P ⊢ ▷ □ P.
+Lemma later_persistently_2 P : bi_persistently (▷ P) ⊢ ▷ bi_persistently P.
 Proof. eapply (sbi_mixin_later_persistently_2 bi_entails), sbi_sbi_mixin. Qed.
 
 Lemma later_false_em P : ▷ P ⊢ ▷ False ∨ (▷ False → P).

theories/program_logic/hoare.v

@@ -37,7 +37,7 @@ Global Instance ht_proper E :
 Proof. solve_proper. Qed.
 Lemma ht_mono E P P' Φ Φ' e :
   (P ⊢ P') → (∀ v, Φ' v ⊢ Φ v) → {{ P' }} e @ E {{ Φ' }} ⊢ {{ P }} e @ E {{ Φ }}.
-Proof. by intros; apply persistently_mono, wand_mono, wp_mono. Qed.
+Proof. intros. by apply bare_mono, persistently_mono, wand_mono, wp_mono. Qed.
 Global Instance ht_mono' E :
   Proper (flip (⊢) ==> eq ==> pointwise_relation _ (⊢) ==> (⊢)) (ht E).
 Proof. solve_proper. Qed.

theories/proofmode/classes.v

@@ -3,7 +3,7 @@ Set Default Proof Using "Type".
 Import bi.
 
 Class FromAssumption {PROP : bi} (p : bool) (P Q : PROP) :=
-  from_assumption : ⬕?p P ⊢ Q.
+  from_assumption : □?p P ⊢ Q.
 Arguments FromAssumption {_} _ _%I _%I : simpl never.
 Arguments from_assumption {_} _ _%I _%I {_}.
 (* No need to restrict Hint Mode, we have a default instance that will always
@@ -50,19 +50,19 @@ Arguments from_pure {_} _%I _%type_scope {_}.
 Hint Mode FromPure + ! - : typeclass_instances.
 
 Class IntoPersistent {PROP : bi} (p : bool) (P Q : PROP) :=
-  into_persistent : □?p P ⊢ □ Q.
+  into_persistent : bi_persistently_if p P ⊢ bi_persistently Q.
 Arguments IntoPersistent {_} _ _%I _%I : simpl never.
 Arguments into_persistent {_} _ _%I _%I {_}.
 Hint Mode IntoPersistent + + ! - : typeclass_instances.
 
 Class FromPersistent {PROP : bi} (a p : bool) (P Q : PROP) :=
-  from_persistent : ■?a □?p Q ⊢ P.
+  from_persistent : bi_bare_if a (bi_persistently_if p Q) ⊢ P.
 Arguments FromPersistent {_} _ _ _%I _%I : simpl never.
 Arguments from_persistent {_} _ _ _%I _%I {_}.
 Hint Mode FromPersistent + - - ! - : typeclass_instances.
 
 Class FromBare {PROP : bi} (P Q : PROP) :=
-  from_bare : ■ Q ⊢ P.
+  from_bare : bi_bare Q ⊢ P.
 Arguments FromBare {_} _%I _%type_scope : simpl never.
 Arguments from_bare {_} _%I _%type_scope {_}.
 Hint Mode FromBare + ! - : typeclass_instances.
@@ -91,7 +91,7 @@ Converting an assumption [R] into a wand [P -∗ Q] is done in three stages:
 - Instantiate the premise of the wand or implication.
 *)
 Class IntoWand {PROP : bi} (p q : bool) (R P Q : PROP) :=
-  into_wand : ⬕?p R ⊢ ⬕?q P -∗ Q.
+  into_wand : □?p R ⊢ □?q P -∗ Q.
 Arguments IntoWand {_} _ _ _%I _%I _%I : simpl never.
 Arguments into_wand {_} _ _ _%I _%I _%I {_}.
 Hint Mode IntoWand + + + ! - - : typeclass_instances.
@@ -122,7 +122,7 @@ Hint Mode FromAnd + ! - - : typeclass_instances.
 Hint Mode FromAnd + - ! ! : typeclass_instances. (* For iCombine *)
 
 Class IntoAnd {PROP : bi} (p : bool) (P Q1 Q2 : PROP) :=
-  into_and : ⬕?p P ⊢ ⬕?p (Q1 ∧ Q2).
+  into_and : □?p P ⊢ □?p (Q1 ∧ Q2).
 Arguments IntoAnd {_} _ _%I _%I _%I : simpl never.
 Arguments into_and {_} _ _%I _%I _%I {_}.
 Hint Mode IntoAnd + + ! - - : typeclass_instances.
@@ -196,13 +196,13 @@ Proof. done. Qed.
 Instance is_app_app {A} (l1 l2 : list A) : IsApp (l1 ++ l2) l1 l2.
 Proof. done. Qed.
 
-Class Frame {PROP : bi} (p : bool) (R P Q : PROP) := frame : ⬕?p R ∗ Q ⊢ P.
+Class Frame {PROP : bi} (p : bool) (R P Q : PROP) := frame : □?p R ∗ Q ⊢ P.
 Arguments Frame {_} _ _%I _%I _%I.
 Arguments frame {_ _} _%I _%I _%I {_}.
 Hint Mode Frame + + ! ! - : typeclass_instances.
 
 Class MaybeFrame {PROP : bi} (p : bool) (R P Q : PROP) :=
-  maybe_frame : ⬕?p R ∗ Q ⊢ P.
+  maybe_frame : □?p R ∗ Q ⊢ P.
 Arguments MaybeFrame {_} _ _%I _%I _%I.
 Arguments maybe_frame {_} _%I _%I _%I {_}.
 Hint Mode MaybeFrame + + ! ! - : typeclass_instances.

theories/proofmode/coq_tactics.v

@@ -22,7 +22,7 @@ Record envs_wf {PROP} (Δ : envs PROP) := {
 }.
 
 Coercion of_envs {PROP} (Δ : envs PROP) : PROP :=
-  (⌜envs_wf Δ⌝ ∧ ⬕ [∧] env_persistent Δ ∗ [∗] env_spatial Δ)%I.
+  (⌜envs_wf Δ⌝ ∧ □ [∧] env_persistent Δ ∗ [∗] env_spatial Δ)%I.
 Instance: Params (@of_envs) 1.
 Arguments of_envs : simpl never.
 
@@ -126,7 +126,7 @@ Implicit Types Δ : envs PROP.
 Implicit Types P Q : PROP.
 
 Lemma of_envs_eq Δ :
-  of_envs Δ = (⌜envs_wf Δ⌝ ∧ ⬕ [∧] env_persistent Δ ∗ [∗] env_spatial Δ)%I.
+  of_envs Δ = (⌜envs_wf Δ⌝ ∧ □ [∧] env_persistent Δ ∗ [∗] env_spatial Δ)%I.
 Proof. done. Qed.
 
 Lemma envs_lookup_delete_Some Δ Δ' i p P :
@@ -139,7 +139,7 @@ Proof.
 Qed.
 
 Lemma envs_lookup_sound Δ i p P :
-  envs_lookup i Δ = Some (p,P) → Δ ⊢ ⬕?p P ∗ envs_delete i p Δ.
+  envs_lookup i Δ = Some (p,P) → Δ ⊢ □?p P ∗ envs_delete i p Δ.
 Proof.
   rewrite /envs_lookup /envs_delete /of_envs=>?. apply pure_elim_l=> Hwf.
   destruct Δ as [Γp Γs], (Γp !! i) eqn:?; simplify_eq/=.
@@ -153,7 +153,7 @@ Proof.
     rewrite (env_lookup_perm Γs) //=. by rewrite !assoc -(comm _ P).
 Qed.
 Lemma envs_lookup_persistent_sound Δ i P :
-  envs_lookup i Δ = Some (true,P) → Δ ⊢ ⬕ P ∗ Δ.
+  envs_lookup i Δ = Some (true,P) → Δ ⊢ □ P ∗ Δ.
 Proof.
   intros. rewrite -persistently_and_bare_sep_l. apply and_intro; last done.
   rewrite envs_lookup_sound //; simpl.
@@ -161,25 +161,25 @@ Proof.
 Qed.
 
 Lemma envs_lookup_split Δ i p P :
-  envs_lookup i Δ = Some (p,P) → Δ ⊢ ⬕?p P ∗ (⬕?p P -∗ Δ).
+  envs_lookup i Δ = Some (p,P) → Δ ⊢ □?p P ∗ (□?p P -∗ Δ).
 Proof.
   rewrite /envs_lookup /of_envs=>?. apply pure_elim_l=> Hwf.
   destruct Δ as [Γp Γs], (Γp !! i) eqn:?; simplify_eq/=.
   - rewrite pure_True // left_id.
     rewrite (env_lookup_perm Γp) //= bare_persistently_and and_sep_bare_persistently.
-    cancel [⬕ P]%I. apply wand_intro_l. solve_sep_entails.
+    cancel [□ P]%I. apply wand_intro_l. solve_sep_entails.
   - destruct (Γs !! i) eqn:?; simplify_eq/=.
     rewrite (env_lookup_perm Γs) //=. rewrite pure_True // left_id.
     cancel [P]. apply wand_intro_l. solve_sep_entails.
 Qed.
 
 Lemma envs_lookup_delete_sound Δ Δ' i p P :
-  envs_lookup_delete i Δ = Some (p,P,Δ') → Δ ⊢ ⬕?p P ∗ Δ'.
+  envs_lookup_delete i Δ = Some (p,P,Δ') → Δ ⊢ □?p P ∗ Δ'.
 Proof. intros [? ->]%envs_lookup_delete_Some. by apply envs_lookup_sound. Qed.
 
 Lemma envs_lookup_delete_list_sound Δ Δ' js rp p Ps :
   envs_lookup_delete_list js rp Δ = Some (p,Ps,Δ') →
-  Δ ⊢ ⬕?p [∗] Ps ∗ Δ'.
+  Δ ⊢ □?p [∗] Ps ∗ Δ'.
 Proof.
   revert Δ Δ' p Ps. induction js as [|j js IH]=> Δ Δ'' p Ps ?; simplify_eq/=.
   { by rewrite bare_persistently_emp left_id. }
@@ -209,7 +209,7 @@ Proof.
 Qed.
 
 Lemma envs_snoc_sound Δ p i P :
-  envs_lookup i Δ = None → Δ ⊢ ⬕?p P -∗ envs_snoc Δ p i P.
+  envs_lookup i Δ = None → Δ ⊢ □?p P -∗ envs_snoc Δ p i P.
 Proof.
   rewrite /envs_lookup /envs_snoc /of_envs=> ?; apply pure_elim_l=> Hwf.
   destruct Δ as [Γp Γs], (Γp !! i) eqn:?, (Γs !! i) eqn:?; simplify_eq/=.
@@ -225,7 +225,7 @@ Proof.
 Qed.
 
 Lemma envs_app_sound Δ Δ' p Γ :
-  envs_app p Γ Δ = Some Δ' → Δ ⊢ (if p then ⬕ [∧] Γ else [∗] Γ) -∗ Δ'.
+  envs_app p Γ Δ = Some Δ' → Δ ⊢ (if p then □ [∧] Γ else [∗] Γ) -∗ Δ'.
 Proof.
   rewrite /of_envs /envs_app=> ?; apply pure_elim_l=> Hwf.
   destruct Δ as [Γp Γs], p; simplify_eq/=.
@@ -248,12 +248,12 @@ Proof.
 Qed.