From 5524871ecb5c423ece67b84f8712d680e4acee7c Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Mon, 4 Dec 2017 19:16:23 +0100
Subject: [PATCH] AffineBI -> BiAffine, PositiveBI -> BiPositive.

---
 theories/base_logic/derived.v        |  4 +-
 theories/bi/big_op.v                 | 60 ++++++++++++------------
 theories/bi/counter_examples.v       |  4 +-
 theories/bi/derived.v                | 68 ++++++++++++++--------------
 theories/bi/tactics.v                |  2 +-
 theories/proofmode/class_instances.v | 20 ++++----
 theories/proofmode/coq_tactics.v     |  4 +-
 7 files changed, 81 insertions(+), 81 deletions(-)

diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index 09441f149..f3da2382d 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -32,7 +32,7 @@ Proof.
 Qed.
 
 (* Affine *)
-Global Instance uPred_affine : AffineBI (uPredI M) | 0.
+Global Instance uPred_affine : BiAffine (uPredI M) | 0.
 Proof. intros P. rewrite /Affine. by apply bi.pure_intro. Qed.
 
 (* Own and valid derived *)
@@ -131,6 +131,6 @@ Proof. split; [split; try apply _|]. apply ownM_op. apply ownM_unit'. Qed.
 End derived.
 
 (* Also add this to the global hint database, otherwise [eauto] won't work for
-many lemmas that have [AffineBI] as a premise. *)
+many lemmas that have [BiAffine] as a premise. *)
 Hint Immediate uPred_affine.
 End uPred.
diff --git a/theories/bi/big_op.v b/theories/bi/big_op.v
index aba95a69c..2ae8c66a5 100644
--- a/theories/bi/big_op.v
+++ b/theories/bi/big_op.v
@@ -55,7 +55,7 @@ Section sep_list.
 
   Lemma big_sepL_nil Φ : ([∗ list] k↦y ∈ nil, Φ k y) ⊣⊢ emp.
   Proof. done. Qed.
-  Lemma big_sepL_nil' `{AffineBI PROP} P Φ : P ⊢ [∗ list] k↦y ∈ nil, Φ k y.
+  Lemma big_sepL_nil' `{BiAffine PROP} P Φ : P ⊢ [∗ list] k↦y ∈ nil, Φ k y.
   Proof. apply (affine _). Qed.
   Lemma big_sepL_cons Φ x l :
     ([∗ list] k↦y ∈ x :: l, Φ k y) ⊣⊢ Φ 0 x ∗ [∗ list] k↦y ∈ l, Φ (S k) y.
@@ -75,7 +75,7 @@ Section sep_list.
     (∀ k y, l !! k = Some y → Φ k y ⊣⊢ Ψ k y) →
     ([∗ list] k ↦ y ∈ l, Φ k y) ⊣⊢ ([∗ list] k ↦ y ∈ l, Ψ k y).
   Proof. apply big_opL_proper. Qed.
-  Lemma big_sepL_submseteq `{AffineBI PROP} (Φ : A → PROP) l1 l2 :
+  Lemma big_sepL_submseteq `{BiAffine PROP} (Φ : A → PROP) l1 l2 :
     l1 ⊆+ l2 → ([∗ list] y ∈ l2, Φ y) ⊢ [∗ list] y ∈ l1, Φ y.
   Proof.
     intros [l ->]%submseteq_Permutation. by rewrite big_sepL_app sep_elim_l.
@@ -125,16 +125,16 @@ Section sep_list.
     ⊢ ([∗ list] k↦x ∈ l, Φ k x) ∧ ([∗ list] k↦x ∈ l, Ψ k x).
   Proof. auto using and_intro, big_sepL_mono, and_elim_l, and_elim_r. Qed.
 
-  Lemma big_sepL_plainly `{AffineBI PROP} Φ l :
+  Lemma big_sepL_plainly `{BiAffine PROP} Φ l :
     bi_plainly ([∗ list] k↦x ∈ l, Φ k x) ⊣⊢ [∗ list] k↦x ∈ l, bi_plainly (Φ k x).
   Proof. apply (big_opL_commute _). Qed.
 
-  Lemma big_sepL_persistently `{AffineBI PROP} Φ l :
+  Lemma big_sepL_persistently `{BiAffine PROP} Φ l :
     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 :
+  Lemma big_sepL_forall `{BiAffine PROP} Φ l :
     (∀ k x, Persistent (Φ k x)) →
     ([∗ list] k↦x ∈ l, Φ k x) ⊣⊢ (∀ k x, ⌜l !! k = Some x⌝ → Φ k x).
   Proof.
@@ -287,7 +287,7 @@ Section and_list.
     [∧ list] k↦x ∈ l, bi_persistently (Φ k x).
   Proof. apply (big_opL_commute _). Qed.
 
-  Lemma big_andL_forall `{AffineBI PROP} Φ l :
+  Lemma big_andL_forall `{BiAffine PROP} Φ l :
     ([∧ list] k↦x ∈ l, Φ k x) ⊣⊢ (∀ k x, ⌜l !! k = Some x⌝ → Φ k x).
   Proof.
     apply (anti_symm _).
@@ -328,7 +328,7 @@ Section gmap.
     (∀ k x, m !! k = Some x → Φ k x ⊣⊢ Ψ k x) →
     ([∗ map] k ↦ x ∈ m, Φ k x) ⊣⊢ ([∗ map] k ↦ x ∈ m, Ψ k x).
   Proof. apply big_opM_proper. Qed.
-  Lemma big_sepM_subseteq `{AffineBI PROP} Φ m1 m2 :
+  Lemma big_sepM_subseteq `{BiAffine PROP} Φ m1 m2 :
     m2 ⊆ m1 → ([∗ map] k ↦ x ∈ m1, Φ k x) ⊢ [∗ map] k ↦ x ∈ m2, Φ k x.
   Proof. intros. by apply big_sepL_submseteq, map_to_list_submseteq. Qed.
 
@@ -339,7 +339,7 @@ Section gmap.
 
   Lemma big_sepM_empty Φ : ([∗ map] k↦x ∈ ∅, Φ k x) ⊣⊢ emp.
   Proof. by rewrite big_opM_empty. Qed.
-  Lemma big_sepM_empty' `{AffineBI PROP} P Φ : P ⊢ [∗ map] k↦x ∈ ∅, Φ k x.
+  Lemma big_sepM_empty' `{BiAffine PROP} P Φ : P ⊢ [∗ map] k↦x ∈ ∅, Φ k x.
   Proof. rewrite big_sepM_empty. apply: affine. Qed.
 
   Lemma big_sepM_insert Φ m i x :
@@ -420,16 +420,16 @@ Section gmap.
     ⊢ ([∗ map] k↦x ∈ m, Φ k x) ∧ ([∗ map] k↦x ∈ m, Ψ k x).
   Proof. auto using and_intro, big_sepM_mono, and_elim_l, and_elim_r. Qed.
 
-  Lemma big_sepM_plainly `{AffineBI PROP} Φ m :
+  Lemma big_sepM_plainly `{BiAffine PROP} Φ m :
     bi_plainly ([∗ map] k↦x ∈ m, Φ k x) ⊣⊢ [∗ map] k↦x ∈ m, bi_plainly (Φ k x).
   Proof. apply (big_opM_commute _). Qed.
 
-  Lemma big_sepM_persistently `{AffineBI PROP} Φ m :
+  Lemma big_sepM_persistently `{BiAffine PROP} Φ m :
     (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 :
+  Lemma big_sepM_forall `{BiAffine PROP} Φ m :
     (∀ k x, Persistent (Φ k x)) →
     ([∗ map] k↦x ∈ m, Φ k x) ⊣⊢ (∀ k x, ⌜m !! k = Some x⌝ → Φ k x).
   Proof.
@@ -499,7 +499,7 @@ Section gset.
     (∀ x, x ∈ X → Φ x ⊣⊢ Ψ x) →
     ([∗ set] x ∈ X, Φ x) ⊣⊢ ([∗ set] x ∈ X, Ψ x).
   Proof. apply big_opS_proper. Qed.
-  Lemma big_sepS_subseteq `{AffineBI PROP} Φ X Y :
+  Lemma big_sepS_subseteq `{BiAffine PROP} Φ X Y :
     Y ⊆ X → ([∗ set] x ∈ X, Φ x) ⊢ [∗ set] x ∈ Y, Φ x.
   Proof. intros. by apply big_sepL_submseteq, elements_submseteq. Qed.
 
@@ -509,7 +509,7 @@ Section gset.
 
   Lemma big_sepS_empty Φ : ([∗ set] x ∈ ∅, Φ x) ⊣⊢ emp.
   Proof. by rewrite big_opS_empty. Qed.
-  Lemma big_sepS_empty' `{!AffineBI PROP} P Φ : P ⊢ [∗ set] x ∈ ∅, Φ x.
+  Lemma big_sepS_empty' `{!BiAffine PROP} P Φ : P ⊢ [∗ set] x ∈ ∅, Φ x.
   Proof. rewrite big_sepS_empty. apply: affine. Qed.
 
   Lemma big_sepS_insert Φ X x :
@@ -575,12 +575,12 @@ Section gset.
     by apply sep_mono_r, wand_intro_l.
   Qed.
 
-  Lemma big_sepS_filter `{AffineBI PROP}
+  Lemma big_sepS_filter `{BiAffine PROP}
       (P : A → Prop) `{∀ x, Decision (P x)} Φ X :
     ([∗ set] y ∈ filter P X, Φ y) ⊣⊢ ([∗ set] y ∈ X, ⌜P y⌝ → Φ y).
   Proof. setoid_rewrite <-decide_emp. apply big_sepS_filter'. Qed.
 
-  Lemma big_sepS_filter_acc `{AffineBI PROP}
+  Lemma big_sepS_filter_acc `{BiAffine PROP}
       (P : A → Prop) `{∀ y, Decision (P y)} Φ X Y :
     (∀ y, y ∈ Y → P y → y ∈ X) →
     ([∗ set] y ∈ X, Φ y) -∗
@@ -596,15 +596,15 @@ Section gset.
     ([∗ set] y ∈ X, Φ y ∧ Ψ y) ⊢ ([∗ set] y ∈ X, Φ y) ∧ ([∗ set] y ∈ X, Ψ y).
   Proof. auto using and_intro, big_sepS_mono, and_elim_l, and_elim_r. Qed.
 
-  Lemma big_sepS_plainly `{AffineBI PROP} Φ X :
+  Lemma big_sepS_plainly `{BiAffine PROP} Φ X :
     bi_plainly ([∗ set] y ∈ X, Φ y) ⊣⊢ [∗ set] y ∈ X, bi_plainly (Φ y).
   Proof. apply (big_opS_commute _). Qed.
 
-  Lemma big_sepS_persistently `{AffineBI PROP} Φ X :
+  Lemma big_sepS_persistently `{BiAffine PROP} Φ X :
     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 :
+  Lemma big_sepS_forall `{BiAffine PROP} Φ X :
     (∀ x, Persistent (Φ x)) → ([∗ set] x ∈ X, Φ x) ⊣⊢ (∀ x, ⌜x ∈ X⌝ → Φ x).
   Proof.
     intros. apply (anti_symm _).
@@ -671,7 +671,7 @@ Section gmultiset.
     (∀ x, x ∈ X → Φ x ⊣⊢ Ψ x) →
     ([∗ mset] x ∈ X, Φ x) ⊣⊢ ([∗ mset] x ∈ X, Ψ x).
   Proof. apply big_opMS_proper. Qed.
-  Lemma big_sepMS_subseteq `{AffineBI PROP} Φ X Y :
+  Lemma big_sepMS_subseteq `{BiAffine PROP} Φ X Y :
     Y ⊆ X → ([∗ mset] x ∈ X, Φ x) ⊢ [∗ mset] x ∈ Y, Φ x.
   Proof. intros. by apply big_sepL_submseteq, gmultiset_elements_submseteq. Qed.
 
@@ -681,7 +681,7 @@ Section gmultiset.
 
   Lemma big_sepMS_empty Φ : ([∗ mset] x ∈ ∅, Φ x) ⊣⊢ emp.
   Proof. by rewrite big_opMS_empty. Qed.
-  Lemma big_sepMS_empty' `{!AffineBI PROP} P Φ : P ⊢ [∗ mset] x ∈ ∅, Φ x.
+  Lemma big_sepMS_empty' `{!BiAffine PROP} P Φ : P ⊢ [∗ mset] x ∈ ∅, Φ x.
   Proof. rewrite big_sepMS_empty. apply: affine. Qed.
 
   Lemma big_sepMS_union Φ X Y :
@@ -714,11 +714,11 @@ Section gmultiset.
     ([∗ mset] y ∈ X, Φ y ∧ Ψ y) ⊢ ([∗ mset] y ∈ X, Φ y) ∧ ([∗ mset] y ∈ X, Ψ y).
   Proof. auto using and_intro, big_sepMS_mono, and_elim_l, and_elim_r. Qed.
 
-  Lemma big_sepMS_plainly `{AffineBI PROP} Φ X :
+  Lemma big_sepMS_plainly `{BiAffine PROP} Φ X :
     bi_plainly ([∗ mset] y ∈ X, Φ y) ⊣⊢ [∗ mset] y ∈ X, bi_plainly (Φ y).
   Proof. apply (big_opMS_commute _). Qed.
 
-  Lemma big_sepMS_persistently `{AffineBI PROP} Φ X :
+  Lemma big_sepMS_persistently `{BiAffine PROP} Φ X :
     bi_persistently ([∗ mset] y ∈ X, Φ y) ⊣⊢
       [∗ mset] y ∈ X, bi_persistently (Φ y).
   Proof. apply (big_opMS_commute _). Qed.
@@ -756,11 +756,11 @@ Section list.
   Implicit Types l : list A.
   Implicit Types Φ Ψ : nat → A → PROP.
 
-  Lemma big_sepL_later `{AffineBI PROP} Φ l :
+  Lemma big_sepL_later `{BiAffine PROP} Φ l :
     ▷ ([∗ list] k↦x ∈ l, Φ k x) ⊣⊢ ([∗ list] k↦x ∈ l, ▷ Φ k x).
   Proof. apply (big_opL_commute _). Qed.
 
-  Lemma big_sepL_laterN `{AffineBI PROP} Φ n l :
+  Lemma big_sepL_laterN `{BiAffine PROP} Φ n l :
     ▷^n ([∗ list] k↦x ∈ l, Φ k x) ⊣⊢ ([∗ list] k↦x ∈ l, ▷^n Φ k x).
   Proof. apply (big_opL_commute _). Qed.
 
@@ -781,11 +781,11 @@ Section gmap.
   Implicit Types m : gmap K A.
   Implicit Types Φ Ψ : K → A → PROP.
 
-  Lemma big_sepM_later `{AffineBI PROP} Φ m :
+  Lemma big_sepM_later `{BiAffine PROP} Φ m :
     ▷ ([∗ map] k↦x ∈ m, Φ k x) ⊣⊢ ([∗ map] k↦x ∈ m, ▷ Φ k x).
   Proof. apply (big_opM_commute _). Qed.
 
-  Lemma big_sepM_laterN `{AffineBI PROP} Φ n m :
+  Lemma big_sepM_laterN `{BiAffine PROP} Φ n m :
     ▷^n ([∗ map] k↦x ∈ m, Φ k x) ⊣⊢ ([∗ map] k↦x ∈ m, ▷^n Φ k x).
   Proof. apply (big_opM_commute _). Qed.
 
@@ -803,11 +803,11 @@ Section gset.
   Implicit Types X : gset A.
   Implicit Types Φ : A → PROP.
 
-  Lemma big_sepS_later `{AffineBI PROP} Φ X :
+  Lemma big_sepS_later `{BiAffine PROP} Φ X :
     ▷ ([∗ set] y ∈ X, Φ y) ⊣⊢ ([∗ set] y ∈ X, ▷ Φ y).
   Proof. apply (big_opS_commute _). Qed.
 
-  Lemma big_sepS_laterN `{AffineBI PROP} Φ n X :
+  Lemma big_sepS_laterN `{BiAffine PROP} Φ n X :
     ▷^n ([∗ set] y ∈ X, Φ y) ⊣⊢ ([∗ set] y ∈ X, ▷^n Φ y).
   Proof. apply (big_opS_commute _). Qed.
 
@@ -825,11 +825,11 @@ Section gmultiset.
   Implicit Types X : gmultiset A.
   Implicit Types Φ : A → PROP.
 
-  Lemma big_sepMS_later `{AffineBI PROP} Φ X :
+  Lemma big_sepMS_later `{BiAffine PROP} Φ X :
     ▷ ([∗ mset] y ∈ X, Φ y) ⊣⊢ ([∗ mset] y ∈ X, ▷ Φ y).
   Proof. apply (big_opMS_commute _). Qed.
 
-  Lemma big_sepMS_laterN `{AffineBI PROP} Φ n X :
+  Lemma big_sepMS_laterN `{BiAffine PROP} Φ n X :
     ▷^n ([∗ mset] y ∈ X, Φ y) ⊣⊢ ([∗ mset] y ∈ X, ▷^n Φ y).
   Proof. apply (big_opMS_commute _). Qed.
 
diff --git a/theories/bi/counter_examples.v b/theories/bi/counter_examples.v
index d3410120a..e3e1214d3 100644
--- a/theories/bi/counter_examples.v
+++ b/theories/bi/counter_examples.v
@@ -5,7 +5,7 @@ Set Default Proof Using "Type*".
 (** This proves that we need the â–· in a "Saved Proposition" construction with
 name-dependent allocation. *)
 Module savedprop. Section savedprop.
-  Context `{AffineBI PROP}.
+  Context `{BiAffine PROP}.
   Notation "¬ P" := (□ (P → False))%I : bi_scope.
   Implicit Types P : PROP.
 
@@ -65,7 +65,7 @@ End savedprop. End savedprop.
 
 (** This proves that we need the â–· when opening invariants. *)
 Module inv. Section inv.
-  Context `{AffineBI PROP}.
+  Context `{BiAffine PROP}.
   Implicit Types P : PROP.
 
   (** Assumptions *)
diff --git a/theories/bi/derived.v b/theories/bi/derived.v
index 232c7f7de..33d351edc 100644
--- a/theories/bi/derived.v
+++ b/theories/bi/derived.v
@@ -39,11 +39,11 @@ Arguments Affine {_} _%I : simpl never.
 Arguments affine {_} _%I {_}.
 Hint Mode Affine + ! : typeclass_instances.
 
-Class AffineBI (PROP : bi) := absorbing_bi (Q : PROP) : Affine Q.
+Class BiAffine (PROP : bi) := absorbing_bi (Q : PROP) : Affine Q.
 Existing Instance absorbing_bi | 0.
 
-Class PositiveBI (PROP : bi) :=
-  positive_bi (P Q : PROP) : bi_affinely (P ∗ Q) ⊢ bi_affinely P ∗ Q.
+Class BiPositive (PROP : bi) :=
+  bi_positive (P Q : PROP) : bi_affinely (P ∗ Q) ⊢ bi_affinely P ∗ Q.
 
 Definition bi_absorbingly {PROP : bi} (P : PROP) : PROP := (True ∗ P)%I.
 Arguments bi_absorbingly {_} _%I : simpl never.
@@ -732,11 +732,11 @@ Proof.
   - by rewrite !and_elim_l right_id.
   - by rewrite !and_elim_r.
 Qed.
-Lemma affinely_sep `{PositiveBI PROP} P Q :
+Lemma affinely_sep `{BiPositive PROP} P Q :
   bi_affinely (P ∗ Q) ⊣⊢ bi_affinely P ∗ bi_affinely Q.
 Proof.
   apply (anti_symm _), affinely_sep_2.
-  by rewrite -{1}affinely_idemp positive_bi !(comm _ (bi_affinely P)%I) positive_bi.
+  by rewrite -{1}affinely_idemp bi_positive !(comm _ (bi_affinely P)%I) bi_positive.
 Qed.
 Lemma affinely_forall {A} (Φ : A → PROP) :
   bi_affinely (∀ a, Φ a) ⊢ ∀ a, bi_affinely (Φ a).
@@ -815,7 +815,7 @@ Proof. by rewrite /bi_absorbingly !assoc (comm _ P). Qed.
 Lemma absorbingly_sep_lr P Q : bi_absorbingly P ∗ Q ⊣⊢ P ∗ bi_absorbingly Q.
 Proof. by rewrite absorbingly_sep_l absorbingly_sep_r. Qed.
 
-Lemma affinely_absorbingly `{!PositiveBI PROP} P :
+Lemma affinely_absorbingly `{!BiPositive PROP} P :
   bi_affinely (bi_absorbingly P) ⊣⊢ bi_affinely P.
 Proof.
   apply (anti_symm _), affinely_mono, absorbingly_intro.
@@ -875,12 +875,12 @@ Proof. apply (anti_symm _); auto using True_sep_2. Qed.
 Lemma sep_True P `{!Absorbing P} : P ∗ True ⊣⊢ P.
 Proof. by rewrite comm True_sep. Qed.
 
-Section affine_bi.
-  Context `{AffineBI PROP}.
+Section bi_affine.
+  Context `{BiAffine PROP}.
 
-  Global Instance affine_bi_absorbing P : Absorbing P | 0.
+  Global Instance bi_affine_absorbing P : Absorbing P | 0.
   Proof. by rewrite /Absorbing /bi_absorbingly (affine True%I) left_id. Qed.
-  Global Instance affine_bi_positive : PositiveBI PROP.
+  Global Instance bi_affine_positive : BiPositive PROP.
   Proof. intros P Q. by rewrite !affine_affinely. Qed.
 
   Lemma True_emp : True ⊣⊢ emp.
@@ -906,7 +906,7 @@ Section affine_bi.
     - by rewrite pure_True // True_impl.
     - by rewrite pure_False // False_impl True_emp.
   Qed.
-End affine_bi.
+End bi_affine.
 
 (* Properties of the persistence modality *)
 Hint Resolve persistently_mono.
@@ -1044,7 +1044,7 @@ Qed.
 Lemma persistently_sep_2 P Q :
   bi_persistently P ∗ bi_persistently Q ⊢ bi_persistently (P ∗ Q).
 Proof. by rewrite -persistently_and_sep persistently_and -and_sep_persistently. Qed.
-Lemma persistently_sep `{PositiveBI PROP} P Q :
+Lemma persistently_sep `{BiPositive PROP} P Q :
   bi_persistently (P ∗ Q) ⊣⊢ bi_persistently P ∗ bi_persistently Q.
 Proof.
   apply (anti_symm _); auto using persistently_sep_2.
@@ -1076,7 +1076,7 @@ Lemma impl_wand_persistently_2 P Q : (bi_persistently P -∗ Q) ⊢ (bi_persiste
 Proof. apply impl_intro_l. by rewrite persistently_and_sep_l_1 wand_elim_r. Qed.
 
 Section persistently_affinely_bi.
-  Context `{AffineBI PROP}.
+  Context `{BiAffine PROP}.
 
   Lemma persistently_emp : bi_persistently emp ⊣⊢ emp.
   Proof. by rewrite -!True_emp persistently_pure. Qed.
@@ -1243,7 +1243,7 @@ Qed.
 Lemma plainly_sep_2 P Q :
   bi_plainly P ∗ bi_plainly Q ⊢ bi_plainly (P ∗ Q).
 Proof. by rewrite -plainly_and_sep plainly_and -and_sep_plainly. Qed.
-Lemma plainly_sep `{PositiveBI PROP} P Q :
+Lemma plainly_sep `{BiPositive PROP} P Q :
   bi_plainly (P ∗ Q) ⊣⊢ bi_plainly P ∗ bi_plainly Q.
 Proof.
   apply (anti_symm _); auto using plainly_sep_2.
@@ -1271,7 +1271,7 @@ Lemma impl_wand_plainly_2 P Q : (bi_plainly P -∗ Q) ⊢ (bi_plainly P → Q).
 Proof. apply impl_intro_l. by rewrite plainly_and_sep_l_1 wand_elim_r. Qed.
 
 Section plainly_affinely_bi.
-  Context `{AffineBI PROP}.
+  Context `{BiAffine PROP}.
 
   Lemma plainly_emp : bi_plainly emp ⊣⊢ emp.
   Proof. by rewrite -!True_emp plainly_pure. Qed.
@@ -1316,7 +1316,7 @@ Lemma affinely_persistently_exist {A} (Φ : A → PROP) : □ (∃ x, Φ x) ⊣
 Proof. by rewrite persistently_exist affinely_exist. Qed.
 Lemma affinely_persistently_sep_2 P Q : □ P ∗ □ Q ⊢ □ (P ∗ Q).
 Proof. by rewrite affinely_sep_2 persistently_sep_2. Qed.
-Lemma affinely_persistently_sep `{PositiveBI PROP} P Q : □ (P ∗ Q) ⊣⊢ □ P ∗ □ Q.
+Lemma affinely_persistently_sep `{BiPositive PROP} P Q : □ (P ∗ Q) ⊣⊢ □ P ∗ □ Q.
 Proof. by rewrite -affinely_sep -persistently_sep. Qed.
 
 Lemma affinely_persistently_idemp P : □ □ P ⊣⊢ □ P.
@@ -1368,7 +1368,7 @@ Lemma affinely_plainly_exist {A} (Φ : A → PROP) : ■ (∃ x, Φ x) ⊣⊢ 
 Proof. by rewrite plainly_exist affinely_exist. Qed.
 Lemma affinely_plainly_sep_2 P Q : ■ P ∗ ■ Q ⊢ ■ (P ∗ Q).
 Proof. by rewrite affinely_sep_2 plainly_sep_2. Qed.
-Lemma affinely_plainly_sep `{PositiveBI PROP} P Q : ■ (P ∗ Q) ⊣⊢ ■ P ∗ ■ Q.
+Lemma affinely_plainly_sep `{BiPositive PROP} P Q : ■ (P ∗ Q) ⊣⊢ ■ P ∗ ■ Q.
 Proof. by rewrite -affinely_sep -plainly_sep. Qed.
 
 Lemma affinely_plainly_idemp P : ■ ■ P ⊣⊢ ■ P.
@@ -1427,7 +1427,7 @@ Proof. destruct p; simpl; auto using affinely_exist. Qed.
 Lemma affinely_if_sep_2 p P Q :
   bi_affinely_if p P ∗ bi_affinely_if p Q ⊢ bi_affinely_if p (P ∗ Q).
 Proof. destruct p; simpl; auto using affinely_sep_2. Qed.
-Lemma affinely_if_sep `{PositiveBI PROP} p P Q :
+Lemma affinely_if_sep `{BiPositive PROP} p P Q :
   bi_affinely_if p (P ∗ Q) ⊣⊢ bi_affinely_if p P ∗ bi_affinely_if p Q.
 Proof. destruct p; simpl; auto using affinely_sep. Qed.
 
@@ -1466,7 +1466,7 @@ Proof. destruct p; simpl; auto using persistently_exist. Qed.
 Lemma persistently_if_sep_2 p P Q :
   bi_persistently_if p P ∗ bi_persistently_if p Q ⊢ bi_persistently_if p (P ∗ Q).
 Proof. destruct p; simpl; auto using persistently_sep_2. Qed.
-Lemma persistently_if_sep `{PositiveBI PROP} p P Q :
+Lemma persistently_if_sep `{BiPositive PROP} p P Q :
   bi_persistently_if p (P ∗ Q) ⊣⊢ bi_persistently_if p P ∗ bi_persistently_if p Q.
 Proof. destruct p; simpl; auto using persistently_sep. Qed.
 
@@ -1496,7 +1496,7 @@ Lemma affinely_persistently_if_exist {A} p (Ψ : A → PROP) :
 Proof. destruct p; simpl; auto using affinely_persistently_exist. Qed.
 Lemma affinely_persistently_if_sep_2 p P Q : □?p P ∗ □?p Q ⊢ □?p (P ∗ Q).
 Proof. destruct p; simpl; auto using affinely_persistently_sep_2. Qed.
-Lemma affinely_persistently_if_sep `{PositiveBI PROP} p P Q :
+Lemma affinely_persistently_if_sep `{BiPositive PROP} p P Q :
   □?p (P ∗ Q) ⊣⊢ □?p P ∗ □?p Q.
 Proof. destruct p; simpl; auto using affinely_persistently_sep. Qed.
 
@@ -1527,7 +1527,7 @@ Lemma plainly_if_or p P Q : bi_plainly_if p (P ∨ Q) ⊣⊢ bi_plainly_if p P 
 Proof. destruct p; simpl; auto using plainly_or. Qed.
 Lemma plainly_if_exist {A} p (Ψ : A → PROP) : (bi_plainly_if p (∃ a, Ψ a)) ⊣⊢ ∃ a, bi_plainly_if p (Ψ a).
 Proof. destruct p; simpl; auto using plainly_exist. Qed.
-Lemma plainly_if_sep `{PositiveBI PROP} p P Q :
+Lemma plainly_if_sep `{BiPositive PROP} p P Q :
   bi_plainly_if p (P ∗ Q) ⊣⊢ bi_plainly_if p P ∗ bi_plainly_if p Q.
 Proof. destruct p; simpl; auto using plainly_sep. Qed.
 
@@ -1557,7 +1557,7 @@ Lemma affinely_plainly_if_exist {A} p (Ψ : A → PROP) :
 Proof. destruct p; simpl; auto using affinely_plainly_exist. Qed.
 Lemma affinely_plainly_if_sep_2 p P Q : ■?p P ∗ ■?p Q ⊢ ■?p (P ∗ Q).
 Proof. destruct p; simpl; auto using affinely_plainly_sep_2. Qed.
-Lemma affinely_plainly_if_sep `{PositiveBI PROP} p P Q :
+Lemma affinely_plainly_if_sep `{BiPositive PROP} p P Q :
   ■?p (P ∗ Q) ⊣⊢ ■?p P ∗ ■?p Q.
 Proof. destruct p; simpl; auto using affinely_plainly_sep. Qed.
 
@@ -1626,7 +1626,7 @@ Lemma impl_wand_2 P `{!Persistent P} Q : (P -∗ Q) ⊢ P → Q.
 Proof. apply impl_intro_l. by rewrite persistent_and_sep_1 wand_elim_r. Qed.
 
 Section persistent_bi_absorbing.
-  Context `{AffineBI PROP}.
+  Context `{BiAffine PROP}.
 
   Lemma persistent_and_sep P Q `{HPQ : !TCOr (Persistent P) (Persistent Q)} :
     P ∧ Q ⊣⊢ P ∗ Q.
@@ -1858,11 +1858,11 @@ Proof.
   split; [split|]; try apply _. apply plainly_or. apply plainly_pure.
 Qed.
 
-Global Instance bi_plainly_sep_weak_homomorphism `{PositiveBI PROP} :
+Global Instance bi_plainly_sep_weak_homomorphism `{BiPositive PROP} :
   WeakMonoidHomomorphism bi_sep bi_sep (≡) (@bi_plainly PROP).
 Proof. split; try apply _. apply plainly_sep. Qed.
 
-Global Instance bi_plainly_sep_homomorphism `{AffineBI PROP} :
+Global Instance bi_plainly_sep_homomorphism `{BiAffine PROP} :
   MonoidHomomorphism bi_sep bi_sep (≡) (@bi_plainly PROP).
 Proof. split. apply _. apply plainly_emp. Qed.
 
@@ -1886,11 +1886,11 @@ Proof.
   split; [split|]; try apply _. apply persistently_or. apply persistently_pure.
 Qed.
 
-Global Instance bi_persistently_sep_weak_homomorphism `{PositiveBI PROP} :
+Global Instance bi_persistently_sep_weak_homomorphism `{BiPositive PROP} :
   WeakMonoidHomomorphism bi_sep bi_sep (≡) (@bi_persistently PROP).
 Proof. split; try apply _. apply persistently_sep. Qed.
 
-Global Instance bi_persistently_sep_homomorphism `{AffineBI PROP} :
+Global Instance bi_persistently_sep_homomorphism `{BiAffine PROP} :
   MonoidHomomorphism bi_sep bi_sep (≡) (@bi_persistently PROP).
 Proof. split. apply _. apply persistently_emp. Qed.
 
@@ -1978,7 +1978,7 @@ Qed.
 
 Lemma later_True : ▷ True ⊣⊢ True.
 Proof. apply (anti_symm (⊢)); auto using later_intro. Qed.
-Lemma later_emp `{!AffineBI PROP} : ▷ emp ⊣⊢ emp.
+Lemma later_emp `{!BiAffine PROP} : ▷ emp ⊣⊢ emp.
 Proof. by rewrite -True_emp later_True. Qed.
 Lemma later_forall {A} (Φ : A → PROP) : (▷ ∀ a, Φ a) ⊣⊢ (∀ a, ▷ Φ a).
 Proof.
@@ -2059,7 +2059,7 @@ Proof. induction n as [|n IH]; simpl; by rewrite -?later_intro. Qed.
 
 Lemma laterN_True n : ▷^n True ⊣⊢ True.
 Proof. apply (anti_symm (⊢)); auto using laterN_intro, True_intro. Qed.
-Lemma laterN_emp `{!AffineBI PROP} n : ▷^n emp ⊣⊢ emp.
+Lemma laterN_emp `{!BiAffine PROP} n : ▷^n emp ⊣⊢ emp.
 Proof. by rewrite -True_emp laterN_True. Qed.
 Lemma laterN_forall {A} n (Φ : A → PROP) : (▷^n ∀ a, Φ a) ⊣⊢ (∀ a, ▷^n Φ a).
 Proof. induction n as [|n IH]; simpl; rewrite -?later_forall ?IH; auto. Qed.
@@ -2124,7 +2124,7 @@ Proof. apply (anti_symm _); rewrite /bi_except_0; auto. Qed.
 
 Lemma except_0_True : ◇ True ⊣⊢ True.
 Proof. rewrite /bi_except_0. apply (anti_symm _); auto. Qed.
-Lemma except_0_emp `{!AffineBI PROP} : ◇ emp ⊣⊢ emp.
+Lemma except_0_emp `{!BiAffine PROP} : ◇ emp ⊣⊢ emp.
 Proof. by rewrite -True_emp except_0_True. Qed.
 Lemma except_0_or P Q : ◇ (P ∨ Q) ⊣⊢ ◇ P ∨ ◇ Q.
 Proof. rewrite /bi_except_0. apply (anti_symm _); auto. Qed.
@@ -2208,7 +2208,7 @@ Proof.
   rewrite /Timeless /bi_except_0 pure_alt later_exist_false.
   apply or_elim, exist_elim; [auto|]=> Hφ. rewrite -(exist_intro Hφ). auto.
 Qed.
-Global Instance emp_timeless `{AffineBI PROP} : Timeless (emp : PROP)%I.
+Global Instance emp_timeless `{BiAffine PROP} : Timeless (emp : PROP)%I.
 Proof. rewrite -True_emp. apply _. Qed.
 
 Global Instance and_timeless P Q : Timeless P → Timeless Q → Timeless (P ∧ Q).
@@ -2305,13 +2305,13 @@ Global Instance bi_except_0_sep_weak_homomorphism :
   WeakMonoidHomomorphism bi_sep bi_sep (≡) (@bi_except_0 PROP).
 Proof. split; try apply _. apply except_0_sep. Qed.
 
-Global Instance bi_later_monoid_sep_homomorphism `{!AffineBI PROP} :
+Global Instance bi_later_monoid_sep_homomorphism `{!BiAffine PROP} :
   MonoidHomomorphism bi_sep bi_sep (≡) (@bi_later PROP).
 Proof. split; try apply _. apply later_emp. Qed.
-Global Instance bi_laterN_sep_homomorphism `{!AffineBI PROP} n :
+Global Instance bi_laterN_sep_homomorphism `{!BiAffine PROP} n :
   MonoidHomomorphism bi_sep bi_sep (≡) (@bi_laterN PROP n).
 Proof. split; try apply _. apply laterN_emp. Qed.
-Global Instance bi_except_0_sep_homomorphism `{!AffineBI PROP} :
+Global Instance bi_except_0_sep_homomorphism `{!BiAffine PROP} :
   MonoidHomomorphism bi_sep bi_sep (≡) (@bi_except_0 PROP).
 Proof. split; try apply _. apply except_0_emp. Qed.
 
diff --git a/theories/bi/tactics.v b/theories/bi/tactics.v
index 9fdb1345a..b755cce52 100644
--- a/theories/bi/tactics.v
+++ b/theories/bi/tactics.v
@@ -32,7 +32,7 @@ Module bi_reflection. Section bi_reflection.
   Qed.
 
   (* Can be related to the RHS being affine *)
-  Lemma flatten_entails `{AffineBI PROP} Σ e1 e2 :
+  Lemma flatten_entails `{BiAffine PROP} Σ e1 e2 :
     flatten e2 ⊆+ flatten e1 → eval Σ e1 ⊢ eval Σ e2.
   Proof. intros. rewrite !eval_flatten. by apply big_sepL_submseteq. Qed.
   Lemma flatten_equiv Σ e1 e2 :
diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index 035f37995..5c350e019 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -50,7 +50,7 @@ Proof.
   rewrite /FromAssumption /= =><-.
   by rewrite persistently_elim plainly_elim_persistently.
 Qed.
-Global Instance from_assumption_plainly_l_false `{AffineBI PROP} P Q :
+Global Instance from_assumption_plainly_l_false `{BiAffine PROP} P Q :
   FromAssumption true P Q → FromAssumption false (bi_plainly P) Q.
 Proof.
   rewrite /FromAssumption /= =><-.
@@ -62,7 +62,7 @@ Proof. rewrite /FromAssumption /= =><-. by rewrite affinely_persistently_if_elim
 Global Instance from_assumption_persistently_l_true P Q :
   FromAssumption true P Q → FromAssumption true (bi_persistently P) Q.
 Proof. rewrite /FromAssumption /= =><-. by rewrite persistently_idemp. Qed.
-Global Instance from_assumption_persistently_l_false `{AffineBI PROP} P Q :
+Global Instance from_assumption_persistently_l_false `{BiAffine PROP} P Q :
   FromAssumption true P Q → FromAssumption false (bi_persistently P) Q.
 Proof. rewrite /FromAssumption /= =><-. by rewrite affine_affinely. Qed.
 Global Instance from_assumption_affinely_l_true p P Q :
@@ -224,7 +224,7 @@ Proof.
   rewrite /FromAssumption /IntoWand=> HP. by rewrite HP affinely_persistently_if_elim.
 Qed.
 
-Global Instance into_wand_impl_false_false `{!AffineBI PROP} P Q P' :
+Global Instance into_wand_impl_false_false `{!BiAffine PROP} P Q P' :
   FromAssumption false P P' → IntoWand false false (P' → Q) P Q.
 Proof.
   rewrite /FromAssumption /IntoWand /= => ->. apply wand_intro_r.
@@ -274,7 +274,7 @@ Proof. by rewrite /IntoWand affinely_plainly_elim. Qed.
 Global Instance into_wand_plainly_true q R P Q :
   IntoWand true q R P Q → IntoWand true q (bi_plainly R) P Q.
 Proof. by rewrite /IntoWand /= persistently_plainly plainly_elim_persistently. Qed.
-Global Instance into_wand_plainly_false `{!AffineBI PROP} q R P Q :
+Global Instance into_wand_plainly_false `{!BiAffine PROP} q R P Q :
   IntoWand false q R P Q → IntoWand false q (bi_plainly R) P Q.
 Proof. by rewrite /IntoWand plainly_elim. Qed.
 
@@ -284,7 +284,7 @@ Proof. by rewrite /IntoWand affinely_persistently_elim. Qed.
 Global Instance into_wand_persistently_true q R P Q :
   IntoWand true q R P Q → IntoWand true q (bi_persistently R) P Q.
 Proof. by rewrite /IntoWand /= persistently_idemp. Qed.
-Global Instance into_wand_persistently_false `{!AffineBI PROP} q R P Q :
+Global Instance into_wand_persistently_false `{!BiAffine PROP} q R P Q :
   IntoWand false q R P Q → IntoWand false q (bi_persistently R) P Q.
 Proof. by rewrite /IntoWand persistently_elim. Qed.
 
@@ -388,7 +388,7 @@ Proof.
   by rewrite -(affine_affinely Q) affinely_and_r affinely_and (from_affinely P').
 Qed.
 
-Global Instance into_and_sep `{PositiveBI PROP} P Q : IntoAnd true (P ∗ Q) P Q.
+Global Instance into_and_sep `{BiPositive PROP} P Q : IntoAnd true (P ∗ Q) P Q.
 Proof.
   by rewrite /IntoAnd /= persistently_sep -and_sep_persistently persistently_and.
 Qed.
@@ -460,10 +460,10 @@ Global Instance into_sep_affinely P Q1 Q2 :
   IntoSep P Q1 Q2 → IntoSep (bi_affinely P) Q1 Q2 | 20.
 Proof. rewrite /IntoSep /= => ->. by rewrite affinely_elim. Qed.
 
-Global Instance into_sep_plainly `{PositiveBI PROP} P Q1 Q2 :
+Global Instance into_sep_plainly `{BiPositive PROP} P Q1 Q2 :
   IntoSep P Q1 Q2 → IntoSep (bi_plainly P) (bi_plainly Q1) (bi_plainly Q2).
 Proof. rewrite /IntoSep /= => ->. by rewrite plainly_sep. Qed.
-Global Instance into_sep_persistently `{PositiveBI PROP} P Q1 Q2 :
+Global Instance into_sep_persistently `{BiPositive PROP} P Q1 Q2 :
   IntoSep P Q1 Q2 →
   IntoSep (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
 Proof. rewrite /IntoSep /= => ->. by rewrite persistently_sep. Qed.
@@ -609,7 +609,7 @@ Proof.
   - by rewrite (into_pure P) -pure_wand_forall wand_elim_l.
 Qed.
 
-Global Instance from_forall_affinely `{AffineBI PROP} {A} P (Φ : A → PROP) :
+Global Instance from_forall_affinely `{BiAffine PROP} {A} P (Φ : A → PROP) :
   FromForall P Φ → FromForall (bi_affinely P)%I (λ a, bi_affinely (Φ a))%I.
 Proof.
   rewrite /FromForall=> <-. rewrite affine_affinely. by setoid_rewrite affinely_elim.
@@ -1234,7 +1234,7 @@ Global Instance from_later_sep n P1 P2 Q1 Q2 :
   FromLaterN n P1 Q1 → FromLaterN n P2 Q2 → FromLaterN n (P1 ∗ P2) (Q1 ∗ Q2).
 Proof. intros ??; red. by rewrite laterN_sep; apply sep_mono. Qed.
 
-Global Instance from_later_affinely n P Q `{AffineBI PROP} :
+Global Instance from_later_affinely n P Q `{BiAffine PROP} :
   FromLaterN n P Q → FromLaterN n (bi_affinely P) (bi_affinely Q).
 Proof. rewrite /FromLaterN=><-. by rewrite affinely_elim affine_affinely. Qed.
 Global Instance from_later_plainly n P Q :
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 08708214e..0648e9070 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -458,7 +458,7 @@ Global Instance affine_env_snoc Γ i P :
 Proof. by constructor. Qed.
 
 (* If the BI is affine, no need to walk on the whole environment. *)
-Global Instance affine_env_bi `(AffineBI PROP) Γ : AffineEnv Γ | 0.
+Global Instance affine_env_bi `(BiAffine PROP) Γ : AffineEnv Γ | 0.
 Proof. induction Γ; apply _. Qed.
 
 Instance affine_env_spatial Δ :
@@ -800,7 +800,7 @@ Lemma tac_specialize_persistent_helper Δ Δ'' j q P R R' Q :
   envs_lookup j Δ = Some (q,P) →
   envs_entails Δ (bi_absorbingly R) →
   IntoPersistent false R R' →
-  (if q then TCTrue else AffineBI PROP) →
+  (if q then TCTrue else BiAffine PROP) →
   envs_replace j q true (Esnoc Enil j R') Δ = Some Δ'' →
   envs_entails Δ'' Q → envs_entails Δ Q.
 Proof.
-- 
GitLab