Merge branch 'robbert/big_rename' into 'gen_proofmode'

Renaming and notations for modalities gen_proofmode

See merge request FP/iris-coq!126

ProofMode.md

@@ -117,7 +117,7 @@ Modalities
 - `iModIntro mod` : introduction of a modality. The type class `FromModal` is
   used to specify which modalities this tactic should introduce. Instances of
   that type class include: later, except 0, basic update and fancy update,
-  persistently, affinely, plainly, absorbingly, absolutely, and relatively.
+  persistently, affinely, plainly, absorbingly, objectively, and subjectively.
   The optional argument `mod` can be used to specify what modality to introduce
   in case of ambiguity, e.g. `⎡|==> P⎤`.
 - `iAlways` : a deprecated alias of `iModIntro`.

theories/base_logic/derived.v

@@ -16,8 +16,7 @@ Notation "P ⊢ Q" := (bi_entails (PROP:=uPredI M) P%I Q%I).
 Notation "P ⊣⊢ Q" := (equiv (A:=uPredI M) P%I Q%I).
 
 (* Own and valid derived *)
-Lemma persistently_cmra_valid_1 {A : cmraT} (a : A) :
-  ✓ a ⊢ bi_persistently (✓ a : uPred M).
+Lemma persistently_cmra_valid_1 {A : cmraT} (a : A) : ✓ a ⊢ <pers> (✓ a : uPred M).
 Proof. by rewrite {1}plainly_cmra_valid_1 plainly_elim_persistently. Qed.
 Lemma affinely_persistently_ownM (a : M) : CoreId a → □ uPred_ownM a ⊣⊢ uPred_ownM a.
 Proof.

theories/base_logic/upred.v

@@ -457,21 +457,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) → bi_persistently P ⊢ bi_persistently Q *)
+  - (* (P ⊢ Q) → <pers> P ⊢ <pers> Q *)
     intros P QR HP. unseal; split=> n x ? /=. by apply HP, cmra_core_validN.
-  - (* bi_persistently P ⊢ bi_persistently (bi_persistently P) *)
+  - (* <pers> P ⊢ <pers> <pers> P *)
     intros P. unseal; split=> n x ?? /=. by rewrite cmra_core_idemp.
-  - (* P ⊢ bi_persistently emp (ADMISSIBLE) *)
+  - (* P ⊢ <pers> emp (ADMISSIBLE) *)
     by unseal.
-  - (* (∀ a, bi_persistently (Ψ a)) ⊢ bi_persistently (∀ a, Ψ a) *)
+  - (* (∀ a, <pers> (Ψ a)) ⊢ <pers> (∀ a, Ψ a) *)
     by unseal.
-  - (* bi_persistently (∃ a, Ψ a) ⊢ ∃ a, bi_persistently (Ψ a) *)
+  - (* <pers> (∃ a, Ψ a) ⊢ ∃ a, <pers> (Ψ a) *)
     by unseal.
-  - (* bi_persistently P ∗ Q ⊢ bi_persistently P (ADMISSIBLE) *)
+  - (* <pers> P ∗ Q ⊢ <pers> 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.
-  - (* bi_persistently P ∧ Q ⊢ P ∗ Q *)
+  - (* <pers> P ∧ Q ⊢ P ∗ Q *)
     intros P Q. unseal; split=> n x ? [??]; simpl in *.
     exists (core x), x; rewrite ?cmra_core_l; auto.
 Qed.
@@ -523,9 +523,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.
-  - (* ▷ bi_persistently P ⊢ bi_persistently (▷ P) *)
+  - (* ▷ <pers> P ⊢ <pers> ▷ P *)
     by unseal.
-  - (* bi_persistently (▷ P) ⊢ ▷ bi_persistently P *)
+  - (* <pers> ▷ P ⊢ ▷ <pers> P *)
     by unseal.
   - (* ▷ P ⊢ ▷ False ∨ (▷ False → P) *)
     intros P. unseal; split=> -[|n] x ? /= HP; [by left|right].
@@ -552,13 +552,13 @@ Proof.
     unseal; split=> n' x; split; apply HP; eauto using @ucmra_unit_validN.
   - (* (P ⊢ Q) → ■ P ⊢ ■ Q *)
     intros P QR HP. unseal; split=> n x ? /=. by apply HP, ucmra_unit_validN.
-  - (* ■ P ⊢ bi_persistently P *)
+  - (* ■ P ⊢ <pers> P *)
     unseal; split; simpl; eauto using uPred_mono, @ucmra_unit_leastN.
   - (* ■ P ⊢ ■ ■ P *)
     unseal; split=> n x ?? //.
   - (* (∀ a, ■ (Ψ a)) ⊢ ■ (∀ a, Ψ a) *)
     by unseal.
-  - (* (■ P → bi_persistently Q) ⊢ bi_persistently (■ P → Q) *)
+  - (* (■ P → <pers> Q) ⊢ <pers> (■ P → Q) *)
     unseal; split=> /= n x ? HPQ n' x' ????.
     eapply uPred_mono with n' (core x)=>//; [|by apply cmra_included_includedN].
     apply (HPQ n' x); eauto using cmra_validN_le.
@@ -665,8 +665,7 @@ 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 ⊢ bi_persistently (uPred_ownM (core a)).
+Lemma persistently_ownM_core (a : M) : uPred_ownM a ⊢ <pers> uPred_ownM (core a).
 Proof.
   rewrite /bi_persistently /=. unseal.
   split=> n x Hx /=. by apply cmra_core_monoN.

theories/bi/big_op.v

@@ -127,8 +127,7 @@ Section sep_list.
   Proof. auto using and_intro, big_sepL_mono, and_elim_l, and_elim_r. Qed.
 
   Lemma big_sepL_persistently `{BiAffine PROP} Φ l :
-    bi_persistently ([∗ list] k↦x ∈ l, Φ k x) ⊣⊢
-    [∗ list] k↦x ∈ l, bi_persistently (Φ k x).
+    <pers> ([∗ list] k↦x ∈ l, Φ k x) ⊣⊢ [∗ list] k↦x ∈ l, <pers> (Φ k x).
   Proof. apply (big_opL_commute _). Qed.
 
   Lemma big_sepL_forall `{BiAffine PROP} Φ l :
@@ -266,8 +265,7 @@ Section and_list.
   Proof. auto using and_intro, big_andL_mono, and_elim_l, and_elim_r. Qed.
 
   Lemma big_andL_persistently Φ l :
-    bi_persistently ([∧ list] k↦x ∈ l, Φ k x) ⊣⊢
-    [∧ list] k↦x ∈ l, bi_persistently (Φ k x).
+    <pers> ([∧ list] k↦x ∈ l, Φ k x) ⊣⊢ [∧ list] k↦x ∈ l, <pers> (Φ k x).
   Proof. apply (big_opL_commute _). Qed.
 
   Lemma big_andL_forall `{BiAffine PROP} Φ l :
@@ -398,8 +396,7 @@ Section gmap.
   Proof. auto using and_intro, big_sepM_mono, and_elim_l, and_elim_r. Qed.
 
   Lemma big_sepM_persistently `{BiAffine PROP} Φ m :
-    (bi_persistently ([∗ map] k↦x ∈ m, Φ k x)) ⊣⊢
-      ([∗ map] k↦x ∈ m, bi_persistently (Φ k x)).
+    (<pers> ([∗ map] k↦x ∈ m, Φ k x)) ⊣⊢ ([∗ map] k↦x ∈ m, <pers> (Φ k x)).
   Proof. apply (big_opM_commute _). Qed.
 
   Lemma big_sepM_forall `{BiAffine PROP} Φ m :
@@ -564,7 +561,7 @@ Section gset.
   Proof. auto using and_intro, big_sepS_mono, and_elim_l, and_elim_r. Qed.
 
   Lemma big_sepS_persistently `{BiAffine PROP} Φ X :
-    bi_persistently ([∗ set] y ∈ X, Φ y) ⊣⊢ [∗ set] y ∈ X, bi_persistently (Φ y).
+    <pers> ([∗ set] y ∈ X, Φ y) ⊣⊢ [∗ set] y ∈ X, <pers> (Φ y).
   Proof. apply (big_opS_commute _). Qed.
 
   Lemma big_sepS_forall `{BiAffine PROP} Φ X :
@@ -672,8 +669,7 @@ Section gmultiset.
   Proof. auto using and_intro, big_sepMS_mono, and_elim_l, and_elim_r. Qed.
 
   Lemma big_sepMS_persistently `{BiAffine PROP} Φ X :
-    bi_persistently ([∗ mset] y ∈ X, Φ y) ⊣⊢
-      [∗ mset] y ∈ X, bi_persistently (Φ y).
+    <pers> ([∗ mset] y ∈ X, Φ y) ⊣⊢ [∗ mset] y ∈ X, <pers> (Φ y).
   Proof. apply (big_opMS_commute _). Qed.
 
   Global Instance big_sepMS_empty_persistent Φ :

theories/bi/derived_connectives.v

@@ -13,7 +13,7 @@ Arguments bi_wand_iff {_} _%I _%I : simpl never.
 Instance: Params (@bi_wand_iff) 1.
 Infix "∗-∗" := bi_wand_iff (at level 95, no associativity) : bi_scope.
 
-Class Persistent {PROP : bi} (P : PROP) := persistent : P ⊢ bi_persistently P.
+Class Persistent {PROP : bi} (P : PROP) := persistent : P ⊢ <pers> P.
 Arguments Persistent {_} _%I : simpl never.
 Arguments persistent {_} _%I {_}.
 Hint Mode Persistent + ! : typeclass_instances.
@@ -23,7 +23,10 @@ Definition bi_affinely {PROP : bi} (P : PROP) : PROP := (emp ∧ P)%I.
 Arguments bi_affinely {_} _%I : simpl never.
 Instance: Params (@bi_affinely) 1.
 Typeclasses Opaque bi_affinely.
-Notation "□ P" := (bi_affinely (bi_persistently P))%I
+Notation "'<affine>' P" := (bi_affinely P)
+  (at level 20, right associativity) : bi_scope.
+
+Notation "□ P" := (<affine> <pers> P)%I
   (at level 20, right associativity) : bi_scope.
 
 Class Affine {PROP : bi} (Q : PROP) := affine : Q ⊢ emp.
@@ -36,31 +39,40 @@ Hint Mode BiAffine ! : typeclass_instances.
 Existing Instance absorbing_bi | 0.
 
 Class BiPositive (PROP : bi) :=
-  bi_positive (P Q : PROP) : bi_affinely (P ∗ Q) ⊢ bi_affinely P ∗ Q.
+  bi_positive (P Q : PROP) : <affine> (P ∗ Q) ⊢ <affine> P ∗ Q.
 Hint Mode BiPositive ! : typeclass_instances.
 
 Definition bi_absorbingly {PROP : bi} (P : PROP) : PROP := (True ∗ P)%I.
 Arguments bi_absorbingly {_} _%I : simpl never.
 Instance: Params (@bi_absorbingly) 1.
 Typeclasses Opaque bi_absorbingly.
+Notation "'<absorb>' P" := (bi_absorbingly P)
+  (at level 20, right associativity) : bi_scope.
 
-Class Absorbing {PROP : bi} (P : PROP) := absorbing : bi_absorbingly P ⊢ P.
+Class Absorbing {PROP : bi} (P : PROP) := absorbing : <absorb> P ⊢ P.
 Arguments Absorbing {_} _%I : simpl never.
 Arguments absorbing {_} _%I.
 Hint Mode Absorbing + ! : typeclass_instances.
 
 Definition bi_persistently_if {PROP : bi} (p : bool) (P : PROP) : PROP :=
-  (if p then bi_persistently P else P)%I.
+  (if p then <pers> P else P)%I.
 Arguments bi_persistently_if {_} !_ _%I /.
 Instance: Params (@bi_persistently_if) 2.
 Typeclasses Opaque bi_persistently_if.
+Notation "'<pers>?' p P" := (bi_persistently_if p P)
+  (at level 20, p at level 9, P at level 20,
+   right associativity, format "'<pers>?' p  P") : bi_scope.
 
 Definition bi_affinely_if {PROP : bi} (p : bool) (P : PROP) : PROP :=
-  (if p then bi_affinely P else P)%I.
+  (if p then <affine> P else P)%I.
 Arguments bi_affinely_if {_} !_ _%I /.
 Instance: Params (@bi_affinely_if) 2.
 Typeclasses Opaque bi_affinely_if.
-Notation "□? p P" := (bi_affinely_if p (bi_persistently_if p P))%I
+Notation "'<affine>?' p P" := (bi_affinely_if p P)
+  (at level 20, p at level 9, P at level 20,
+   right associativity, format "'<affine>?' p  P") : bi_scope.
+
+Notation "□? p P" := (<affine>?p <pers>?p P)%I
   (at level 20, p at level 9, P at level 20,
    right associativity, format "□? p  P") : bi_scope.
 

theories/bi/embedding.v

@@ -22,7 +22,7 @@ Record BiEmbedMixin (PROP1 PROP2 : bi) `(Embed PROP1 PROP2) := {
   bi_embed_mixin_exist_1 A (Φ : A → PROP1) : ⎡∃ x, Φ x⎤ ⊢ ∃ x, ⎡Φ x⎤;
   bi_embed_mixin_sep P Q : ⎡P ∗ Q⎤ ⊣⊢ ⎡P⎤ ∗ ⎡Q⎤;
   bi_embed_mixin_wand_2 P Q : (⎡P⎤ -∗ ⎡Q⎤) ⊢ ⎡P -∗ Q⎤;
-  bi_embed_mixin_persistently P : ⎡bi_persistently P⎤ ⊣⊢ bi_persistently ⎡P⎤
+  bi_embed_mixin_persistently P : ⎡<pers> P⎤ ⊣⊢ <pers> ⎡P⎤
 }.
 
 Class BiEmbed (PROP1 PROP2 : bi) := {
@@ -79,7 +79,7 @@ Section embed_laws.
   Proof. eapply bi_embed_mixin_sep, bi_embed_mixin. Qed.
   Lemma embed_wand_2 P Q : (⎡P⎤ -∗ ⎡Q⎤) ⊢ ⎡P -∗ Q⎤.
   Proof. eapply bi_embed_mixin_wand_2, bi_embed_mixin. Qed.
-  Lemma embed_persistently P : ⎡bi_persistently P⎤ ⊣⊢ bi_persistently ⎡P⎤.
+  Lemma embed_persistently P : ⎡<pers> P⎤ ⊣⊢ <pers> ⎡P⎤.
   Proof. eapply bi_embed_mixin_persistently, bi_embed_mixin. Qed.
 End embed_laws.
 
@@ -141,14 +141,13 @@ Section embed.
   Proof. by rewrite embed_and !embed_impl. Qed.
   Lemma embed_wand_iff P Q : ⎡P ∗-∗ Q⎤ ⊣⊢ (⎡P⎤ ∗-∗ ⎡Q⎤).
   Proof. by rewrite embed_and !embed_wand. Qed.
-  Lemma embed_affinely P : ⎡bi_affinely P⎤ ⊣⊢ bi_affinely ⎡P⎤.
+  Lemma embed_affinely P : ⎡<affine> P⎤ ⊣⊢ <affine> ⎡P⎤.
   Proof. by rewrite embed_and embed_emp. Qed.
-  Lemma embed_absorbingly P : ⎡bi_absorbingly P⎤ ⊣⊢ bi_absorbingly ⎡P⎤.
+  Lemma embed_absorbingly P : ⎡<absorb> P⎤ ⊣⊢ <absorb> ⎡P⎤.
   Proof. by rewrite embed_sep embed_pure. Qed.
-  Lemma embed_persistently_if P b :
-    ⎡bi_persistently_if b P⎤ ⊣⊢ bi_persistently_if b ⎡P⎤.
+  Lemma embed_persistently_if P b : ⎡<pers>?b P⎤ ⊣⊢ <pers>?b ⎡P⎤.
   Proof. destruct b; simpl; auto using embed_persistently. Qed.
-  Lemma embed_affinely_if P b : ⎡bi_affinely_if b P⎤ ⊣⊢ bi_affinely_if b ⎡P⎤.
+  Lemma embed_affinely_if P b : ⎡<affine>?b P⎤ ⊣⊢ <affine>?b ⎡P⎤.
   Proof. destruct b; simpl; auto using embed_affinely. Qed.
   Lemma embed_hforall {As} (Φ : himpl As PROP1):
     ⎡bi_hforall Φ⎤ ⊣⊢ bi_hforall (hcompose embed Φ).
@@ -233,6 +232,6 @@ End sbi_embed.
 
 (* Not defined using an ordinary [Instance] because the default
 [class_apply @bi_embed_plainly] shelves the [BiPlainly] premise, making proof
-search for the other premises fail. See the proof of [monPred_absolutely_plain]
+search for the other premises fail. See the proof of [monPred_objectively_plain]
 for an example where it would fail with a regular [Instance].*)
 Hint Extern 4 (Plain ⎡_⎤) => eapply @embed_plain : typeclass_instances.

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 Φ Ψ : ((bi_persistently (∀ x, Φ x -∗ Ψ x)) → ∀ x, F Φ x -∗ F Ψ x)%I;
+  bi_mono_pred Φ Ψ : (<pers> (∀ 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, bi_persistently (∀ x, F Φ x -∗ Φ x) → Φ x)%I.
+  (∀ Φ : A -n> PROP, <pers> (∀ 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, bi_persistently (∀ x, Φ x -∗ F Φ x) ∧ Φ x)%I.
+  (∃ Φ : A -n> PROP, <pers> (∀ x, Φ x -∗ F Φ x) ∧ Φ x)%I.
 
 Section least.
   Context {PROP : bi} {A : ofeT} (F : (A → PROP) → (A → PROP)) `{!BiMonoPred F}.

theories/bi/interface.v

@@ -6,6 +6,7 @@ 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 "'<pers>' P" (at level 20, right associativity).
 Reserved Notation "▷ P" (at level 20, right associativity).
 
 Section bi_mixin.
@@ -38,6 +39,7 @@ Section bi_mixin.
     (bi_exist _ (λ x, .. (bi_exist _ (λ y, P)) ..)).
   Local Infix "∗" := bi_sep.
   Local Infix "-∗" := bi_wand.
+  Local Notation "'<pers>' P" := (bi_persistently P).
   Local Notation "x ≡ y" := (sbi_internal_eq _ x y).
   Local Notation "▷ P" := (sbi_later P).
 
@@ -102,27 +104,23 @@ Section bi_mixin.
 
     (* Persistently *)
     (* In the ordered RA model: Holds without further assumptions. *)
-    bi_mixin_persistently_mono P Q :
-      (P ⊢ Q) → bi_persistently P ⊢ bi_persistently Q;
+    bi_mixin_persistently_mono P Q : (P ⊢ Q) → <pers> P ⊢ <pers> Q;
     (* In the ordered RA model: `core` is idempotent *)
-    bi_mixin_persistently_idemp_2 P :
-      bi_persistently P ⊢ bi_persistently (bi_persistently P);
+    bi_mixin_persistently_idemp_2 P : <pers> P ⊢ <pers> <pers> P;
 
     (* In the ordered RA model: `ε ≼ core x` *)
-    bi_mixin_persistently_emp_intro P : P ⊢ bi_persistently emp;
+    bi_mixin_persistently_emp_intro P : P ⊢ <pers> emp;
 
     bi_mixin_persistently_forall_2 {A} (Ψ : A → PROP) :
-      (∀ a, bi_persistently (Ψ a)) ⊢ bi_persistently (∀ a, Ψ a);
+      (∀ a, <pers> (Ψ a)) ⊢ <pers> (∀ a, Ψ a);
     bi_mixin_persistently_exist_1 {A} (Ψ : A → PROP) :
-      bi_persistently (∃ a, Ψ a) ⊢ ∃ a, bi_persistently (Ψ a);
+      <pers> (∃ a, Ψ a) ⊢ ∃ a, <pers> (Ψ a);
 
     (* In the ordered RA model: [core x ≼ core (x ⋅ y)].
        Note that this implies that the core is monotone. *)
-    bi_mixin_persistently_absorbing P Q :
-      bi_persistently P ∗ Q ⊢ bi_persistently P;
+    bi_mixin_persistently_absorbing P Q : <pers> P ∗ Q ⊢ <pers> P;
     (* In the ordered RA model: [x ⋅ core x = core x]. *)
-    bi_mixin_persistently_and_sep_elim P Q :
-      bi_persistently P ∧ Q ⊢ P ∗ Q;
+    bi_mixin_persistently_and_sep_elim P Q : <pers> P ∧ Q ⊢ P ∗ Q;
   }.
 
   Record SbiMixin := {
@@ -149,10 +147,8 @@ 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 :
-      ▷ bi_persistently P ⊢ bi_persistently (▷ P);
-    sbi_mixin_later_persistently_2 P :
-      bi_persistently (▷ P) ⊢ ▷ bi_persistently P;
+    sbi_mixin_later_persistently_1 P : ▷ <pers> P ⊢ <pers> ▷ P;
+    sbi_mixin_later_persistently_2 P : <pers> ▷ P ⊢ ▷ <pers> P;
 
     sbi_mixin_later_false_em P : ▷ P ⊢ ▷ False ∨ (▷ False → P);
   }.
@@ -292,6 +288,7 @@ 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 "'<pers>' P" := (bi_persistently P) : bi_scope.
 
 Infix "≡" := sbi_internal_eq : bi_scope.
 Notation "▷ P" := (sbi_later P) : bi_scope.
@@ -391,25 +388,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) → bi_persistently P ⊢ bi_persistently Q.
+Lemma persistently_mono P Q : (P ⊢ Q) → <pers> P ⊢ <pers> Q.
 Proof. eapply bi_mixin_persistently_mono, bi_bi_mixin. Qed.
-Lemma persistently_idemp_2 P :
-  bi_persistently P ⊢ bi_persistently (bi_persistently P).
+Lemma persistently_idemp_2 P : <pers> P ⊢ <pers> <pers> P.
 Proof. eapply bi_mixin_persistently_idemp_2, bi_bi_mixin. Qed.
 
-Lemma persistently_emp_intro P : P ⊢ bi_persistently emp.
+Lemma persistently_emp_intro P : P ⊢ <pers> emp.
 Proof. eapply bi_mixin_persistently_emp_intro, bi_bi_mixin. Qed.
 
 Lemma persistently_forall_2 {A} (Ψ : A → PROP) :
-  (∀ a, bi_persistently (Ψ a)) ⊢ bi_persistently (∀ a, Ψ a).
+  (∀ a, <pers> (Ψ a)) ⊢ <pers> (∀ a, Ψ a).
 Proof. eapply bi_mixin_persistently_forall_2, bi_bi_mixin. Qed.
 Lemma persistently_exist_1 {A} (Ψ : A → PROP) :
-  bi_persistently (∃ a, Ψ a) ⊢ ∃ a, bi_persistently (Ψ a).
+  <pers> (∃ a, Ψ a) ⊢ ∃ a, <pers> (Ψ a).
 Proof. eapply bi_mixin_persistently_exist_1, bi_bi_mixin. Qed.
 
-Lemma persistently_absorbing P Q : bi_persistently P ∗ Q ⊢ bi_persistently P.
+Lemma persistently_absorbing P Q : <pers> P ∗ Q ⊢ <pers> P.
 Proof. eapply (bi_mixin_persistently_absorbing bi_entails), bi_bi_mixin. Qed.
-Lemma persistently_and_sep_elim P Q : bi_persistently P ∧ Q ⊢ P ∗ Q.
+Lemma persistently_and_sep_elim P Q : <pers> P ∧ Q ⊢ P ∗ Q.
 Proof. eapply (bi_mixin_persistently_and_sep_elim bi_entails), bi_bi_mixin. Qed.
 End bi_laws.
 
@@ -459,9 +455,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 : ▷ bi_persistently P ⊢ bi_persistently (▷ P).
+Lemma later_persistently_1 P : ▷ <pers> P ⊢ <pers> ▷ P.
 Proof. eapply (sbi_mixin_later_persistently_1 bi_entails), sbi_sbi_mixin. Qed.
-Lemma later_persistently_2 P : bi_persistently (▷ P) ⊢ ▷ bi_persistently P.
+Lemma later_persistently_2 P : <pers> ▷ P ⊢ ▷ <pers> P.
 Proof. eapply (sbi_mixin_later_persistently_2 bi_entails), sbi_sbi_mixin. Qed.
 
 Lemma later_false_em P : ▷ P ⊢ ▷ False ∨ (▷ False → P).

theories/bi/plainly.v

@@ -13,7 +13,7 @@ Record BiPlainlyMixin (PROP : sbi) `(Plainly PROP) := {
   bi_plainly_mixin_plainly_ne : NonExpansive plainly;
 
   bi_plainly_mixin_plainly_mono P Q : (P ⊢ Q) → ■ P ⊢ ■ Q;
-  bi_plainly_mixin_plainly_elim_persistently P : ■ P ⊢ bi_persistently P;
+  bi_plainly_mixin_plainly_elim_persistently P : ■ P ⊢ <pers> P;
   bi_plainly_mixin_plainly_idemp_2 P : ■ P ⊢ ■ ■ P;
 
   bi_plainly_mixin_plainly_forall_2 {A} (Ψ : A → PROP) :
@@ -23,7 +23,7 @@ Record BiPlainlyMixin (PROP : sbi) `(Plainly PROP) := {
      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 :
-    (■ P → bi_persistently Q) ⊢ bi_persistently (■ P → Q);
+    (■ P → <pers> Q) ⊢ <pers> (■ P → Q);
   bi_plainly_mixin_plainly_impl_plainly P Q : (■ P → ■ Q) ⊢ ■ (■ P → Q);
 
   bi_plainly_mixin_plainly_emp_intro P : P ⊢ ■ emp;
@@ -59,14 +59,13 @@ Section plainly_laws.
 
   Lemma plainly_mono P Q : (P ⊢ Q) → ■ P ⊢ ■ Q.
   Proof. eapply bi_plainly_mixin_plainly_mono, bi_plainly_mixin. Qed.
-  Lemma plainly_elim_persistently P : ■ P ⊢ bi_persistently P.
+  Lemma plainly_elim_persistently P : ■ P ⊢ <pers> P.
   Proof. eapply bi_plainly_mixin_plainly_elim_persistently, bi_plainly_mixin. Qed.
   Lemma plainly_idemp_2 P : ■ P ⊢ ■ ■ P.
   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 → bi_persistently Q) ⊢ bi_persistently (■ P → Q).
+  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.
@@ -119,19 +118,19 @@ Global Instance plainly_flip_mono' :
   Proper (flip (⊢) ==> flip (⊢)) (@plainly PROP _).
 Proof. intros P Q; apply plainly_mono. Qed.
 
-Lemma affinely_plainly_elim P : bi_affinely (■ P) ⊢ P.
+Lemma affinely_plainly_elim P : <affine> ■ P ⊢ P.
 Proof. by rewrite plainly_elim_persistently affinely_persistently_elim. Qed.
 
-Lemma persistently_plainly P : bi_persistently (■ P) ⊣⊢ ■ P.
+Lemma persistently_plainly P : <pers> ■ P ⊣⊢ ■ P.
 Proof.
   apply (anti_symm _).
   - by rewrite persistently_elim_absorbingly /bi_absorbingly comm plainly_absorb.
   - by rewrite {1}plainly_idemp_2 plainly_elim_persistently.
 Qed.
-Lemma persistently_if_plainly P p : bi_persistently_if p (■ P) ⊣⊢ ■ P.
+Lemma persistently_if_plainly P p : <pers>?p ■ P ⊣⊢ ■ P.
 Proof. destruct p; last done. exact: persistently_plainly. Qed.
 
-Lemma plainly_persistently P : ■ (bi_persistently P) ⊣⊢ ■ P.
+Lemma plainly_persistently P : ■ <pers> P ⊣⊢ ■ P.
 Proof.
   apply (anti_symm _).
   - rewrite -{1}(left_id True%I bi_and (■ _)%I) (plainly_emp_intro True%I).
@@ -140,7 +139,7 @@ Proof.
   - by rewrite {1}plainly_idemp_2 (plainly_elim_persistently P).
 Qed.
 
-Lemma absorbingly_plainly P : bi_absorbingly (■ P) ⊣⊢ ■ P.
+Lemma absorbingly_plainly P : <absorb> ■ P ⊣⊢ ■ P.
 Proof. by rewrite -(persistently_plainly P) absorbingly_persistently. Qed.
 
 Lemma plainly_and_sep_elim P Q : ■ P ∧ Q -∗ (emp ∧ P) ∗ Q.
@@ -149,7 +148,7 @@ Lemma plainly_and_sep_assoc P Q R : ■ P ∧ (Q ∗ R) ⊣⊢ (■ P ∧ Q) ∗
 Proof. by rewrite -(persistently_plainly P) persistently_and_sep_assoc. Qed.
 Lemma plainly_and_emp_elim P : emp ∧ ■ P ⊢ P.
 Proof. by rewrite plainly_elim_persistently persistently_and_emp_elim. Qed.
-Lemma plainly_elim_absorbingly P : ■ P ⊢ bi_absorbingly P.
+Lemma plainly_elim_absorbingly P : ■ P ⊢ <absorb> P.
 Proof. by rewrite plainly_elim_persistently persistently_elim_absorbingly. Qed.
 Lemma plainly_elim P `{!Absorbing P} : ■ P ⊢ P.
 Proof. by rewrite plainly_elim_persistently persistently_elim. Qed.
@@ -214,7 +213,7 @@ Proof.
   by rewrite plainly_and_sep_assoc (comm bi_and) plainly_and_emp_elim.
 Qed.
 
-Lemma plainly_affinely P : ■ (bi_affinely P) ⊣⊢ ■ P.
+Lemma plainly_affinely P : ■ <affine> P ⊣⊢ ■ P.
 Proof. by rewrite /bi_affinely plainly_and -plainly_True_emp plainly_pure left_id. Qed.
 
 Lemma and_sep_plainly P Q : ■ P ∧ ■ Q ⊣⊢ ■ P ∗ ■ Q.
@@ -252,7 +251,7 @@ Qed.
 Lemma impl_wand_plainly_2 P Q : (■ P -∗ Q) ⊢ (■ P → Q).
 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) ⊣⊢ (bi_affinely (■ P) -∗ Q).
+Lemma impl_wand_affinely_plainly P Q : (■ P → Q) ⊣⊢ (<affine> ■ P -∗ Q).
 Proof. by rewrite -(persistently_plainly P) impl_wand_affinely_persistently. Qed.
 
 Section plainly_affine_bi.
@@ -351,7 +350,7 @@ Proof. by rewrite /Persistent persistently_plainly. Qed.
 Global Instance wand_persistent P Q :
   Plain P → Persistent Q → Absorbing Q → Persistent (P -∗ Q).
 Proof.
-  intros. rewrite /Persistent {2}(plain P). trans (bi_persistently (■ P → Q)%I).
+  intros. rewrite /Persistent {2}(plain P). trans (<pers> (■ P → Q))%I.
   - rewrite -persistently_impl_plainly impl_wand_affinely_plainly -(persistent Q).
     by rewrite affinely_plainly_elim.
   - apply persistently_mono, wand_intro_l. by rewrite sep_and impl_elim_r.
@@ -428,13 +427,13 @@ Proof. intros. by rewrite /Plain -plainly_sep_2 -!plain. Qed.
 
 Global Instance plainly_plain P : Plain (■ P).
 Proof. by rewrite /Plain plainly_idemp. Qed.
-Global Instance persistently_plain P : Plain P → Plain (bi_persistently P).
+Global Instance persistently_plain P : Plain P → Plain (<pers> P).
 Proof.
   rewrite /Plain=> HP. rewrite {1}HP plainly_persistently persistently_plainly //.
 Qed.
-Global Instance affinely_plain P : Plain P → Plain (bi_affinely P).
+Global Instance affinely_plain P : Plain P → Plain (<affine> P).
 Proof. rewrite /bi_affinely. apply _. Qed.
-Global Instance absorbingly_plain P : Plain P → Plain (bi_absorbingly P).
+Global Instance absorbingly_plain P : Plain P → Plain (<absorb> P).
 Proof. rewrite /bi_absorbingly. apply _. Qed.
 Global Instance from_option_plain {A} P (Ψ : A → PROP) (mx : option A) :
   (∀ x, Plain (Ψ x)) → Plain P → Plain (from_option Ψ P mx).
@@ -449,7 +448,7 @@ Proof.
   rewrite -(internal_eq_refl True%I a) plainly_pure; auto.
 Qed.
 
-Lemma plainly_alt P : ■ P ⊣⊢ bi_affinely P ≡ emp.
+Lemma plainly_alt P : ■ P ⊣⊢ <affine> P ≡ emp.
 Proof.
   rewrite -plainly_affinely. apply (anti_symm (⊢)).
   - rewrite -prop_ext. apply plainly_mono, and_intro; apply wand_intro_l.

theories/program_logic/total_adequacy.v

@@ -17,7 +17,7 @@ Definition twptp_pre (twptp : list (expr Λ) → iProp Σ)
     state_interp σ1 ={⊤}=∗ state_interp σ2 ∗ twptp t2)%I.
 
 Lemma twptp_pre_mono (twptp1 twptp2 : list (expr Λ) → iProp Σ) :
-  ((bi_persistently (∀ t, twptp1 t -∗ twptp2 t)) →
+  (<pers> (∀ t, twptp1 t -∗ twptp2 t) →
   ∀ t, twptp_pre twptp1 t -∗ twptp_pre twptp2 t)%I.
 Proof.