From 0c89ae1c244faca6af2c52945988dab985d353a5 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 28 Jan 2021 10:23:25 +0100
Subject: [PATCH] =?UTF-8?q?Rename=20`equiv=5Fspec`=20=E2=86=92=20`equiv=5F?=
 =?UTF-8?q?entails`=20to=20be=20consistent=20with=20conventions=20in=20std?=
 =?UTF-8?q?++.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Hence, also rename (the old) `equiv_entails` → `equiv_entails_1_1` and
`equiv_entails_sym` → `equiv_entails_1_2`, and add `equiv_entails_2` for completeness.
---
 CHANGELOG.md                        |  6 ++++++
 iris/base_logic/bi.v                |  2 +-
 iris/base_logic/upred.v             |  2 +-
 iris/bi/big_op.v                    |  4 ++--
 iris/bi/derived_laws.v              | 25 ++++++++++++++-----------
 iris/bi/embedding.v                 | 14 +++++++-------
 iris/bi/interface.v                 |  6 +++---
 iris/bi/lib/counterexamples.v       |  4 ++--
 iris/bi/monpred.v                   | 24 ++++++++++++------------
 iris/proofmode/environments.v       |  2 +-
 iris/proofmode/modalities.v         |  2 +-
 iris/proofmode/modality_instances.v | 12 ++++++------
 iris/proofmode/monpred.v            |  2 +-
 iris/si_logic/bi.v                  |  2 +-
 iris/si_logic/siprop.v              |  2 +-
 15 files changed, 59 insertions(+), 50 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index fe61684a7..24abae3d3 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -101,6 +101,8 @@ HeapLang, which is now in a separate package `coq-iris-heap-lang`.
   `big_sepS` lemmas.
 * Add lemmas for big-ops of magic wands: `big_sepL_wand`, `big_sepL2_wand`,
   `big_sepM_wand`, `big_sepM2_wand`, `big_sepS_wand`, `big_sepMS_wand`.
+* Rename `equiv_entails` → `equiv_entails_1_1`,
+  `equiv_entails_sym` → `equiv_entails_1_2`, and `equiv_spec` → `equiv_entails`.
 
 **Changes in `proofmode`:**
 
@@ -267,6 +269,10 @@ s/\b(gmultiset_op)_disj_union\b/\1/g
 s/\b(gmultiset_core)_empty\b/\1/g
 s/\b(nat_op)_plus\b/\1/g
 s/\b(max_nat_op)_max\b/\1/g
+# equiv_spec
+s/\bequiv_entails\b/equiv_entails_1_1/g
+s/\bequiv_entails_sym\b/equiv_entails_1_2/g
+s/\bequiv_spec\b/equiv_entails/g
 EOF
 ```
 
diff --git a/iris/base_logic/bi.v b/iris/base_logic/bi.v
index c23006250..77be327e6 100644
--- a/iris/base_logic/bi.v
+++ b/iris/base_logic/bi.v
@@ -18,7 +18,7 @@ Lemma uPred_bi_mixin (M : ucmra) :
 Proof.
   split.
   - exact: entails_po.
-  - exact: equiv_spec.
+  - exact: equiv_entails.
   - exact: pure_ne.
   - exact: and_ne.
   - exact: or_ne.
diff --git a/iris/base_logic/upred.v b/iris/base_logic/upred.v
index 0a0d4d8be..a369af8d7 100644
--- a/iris/base_logic/upred.v
+++ b/iris/base_logic/upred.v
@@ -467,7 +467,7 @@ Proof.
 Qed.
 Lemma entails_anti_sym : AntiSymm (⊣⊢) (⊢).
 Proof. intros P Q HPQ HQP; split=> x n; by split; [apply HPQ|apply HQP]. Qed.
-Lemma equiv_spec P Q : (P ⊣⊢ Q) ↔ (P ⊢ Q) ∧ (Q ⊢ P).
+Lemma equiv_entails P Q : (P ⊣⊢ Q) ↔ (P ⊢ Q) ∧ (Q ⊢ P).
 Proof.
   split.
   - intros HPQ; split; split=> x i; apply HPQ.
diff --git a/iris/bi/big_op.v b/iris/bi/big_op.v
index 67c4e5393..d0ed67236 100644
--- a/iris/bi/big_op.v
+++ b/iris/bi/big_op.v
@@ -499,7 +499,7 @@ Section sep_list2.
     ([∗ list] k ↦ y1;y2 ∈ l1;l2, Φ k y1 y2) ⊣⊢ [∗ list] k ↦ y1;y2 ∈ l1;l2, Ψ k y1 y2.
   Proof.
     intros; apply (anti_symm _);
-      apply big_sepL2_mono; auto using equiv_entails, equiv_entails_sym.
+      apply big_sepL2_mono; auto using equiv_entails_1_1, equiv_entails_1_2.
   Qed.
   Lemma big_sepL2_proper_2 `{!Equiv A, !Equiv B} Φ Ψ l1 l2 l1' l2' :
     l1 ≡ l1' → l2 ≡ l2' →
@@ -1375,7 +1375,7 @@ Section map2.
     ([∗ map] k ↦ y1;y2 ∈ m1;m2, Φ k y1 y2) ⊣⊢ [∗ map] k ↦ y1;y2 ∈ m1;m2, Ψ k y1 y2.
   Proof.
     intros; apply (anti_symm _);
-      apply big_sepM2_mono; auto using equiv_entails, equiv_entails_sym.
+      apply big_sepM2_mono; auto using equiv_entails_1_1, equiv_entails_1_2.
   Qed.
   Lemma big_sepM2_proper_2 `{!Equiv A, !Equiv B} Φ Ψ m1 m2 m1' m2' :
     m1 ≡ m1' → m2 ≡ m2' →
diff --git a/iris/bi/derived_laws.v b/iris/bi/derived_laws.v
index 19e0dedc0..cc1d2cccb 100644
--- a/iris/bi/derived_laws.v
+++ b/iris/bi/derived_laws.v
@@ -29,15 +29,18 @@ Notation "P ⊣⊢ Q" := (P ⊣⊢@{PROP} Q).
 
 (* Derived stuff about the entailment *)
 Global Instance entails_anti_sym : AntiSymm (⊣⊢) (@bi_entails PROP).
-Proof. intros P Q ??. by apply equiv_spec. Qed.
-Lemma equiv_entails P Q : (P ⊣⊢ Q) → (P ⊢ Q).
-Proof. apply equiv_spec. Qed.
-Lemma equiv_entails_sym P Q : (Q ⊣⊢ P) → (P ⊢ Q).
-Proof. apply equiv_spec. Qed.
+Proof. intros P Q ??. by apply equiv_entails. Qed.
+Lemma equiv_entails_1_1 P Q : (P ⊣⊢ Q) → (P ⊢ Q).
+Proof. apply equiv_entails. Qed.
+Lemma equiv_entails_1_2 P Q : (P ⊣⊢ Q) → (Q ⊢ P).
+Proof. apply equiv_entails. Qed.
+Lemma equiv_entails_2 P Q : (P ⊢ Q) → (Q ⊢ P) → (P ⊣⊢ Q).
+Proof. intros. by apply equiv_entails. Qed.
+
 Global Instance entails_proper :
   Proper ((⊣⊢) ==> (⊣⊢) ==> iff) ((⊢) : relation PROP).
 Proof.
-  move => P1 P2 /equiv_spec [HP1 HP2] Q1 Q2 /equiv_spec [HQ1 HQ2]; split=>?.
+  move => P1 P2 /equiv_entails [HP1 HP2] Q1 Q2 /equiv_entails [HQ1 HQ2]; split=>?.
   - by trans P1; [|trans Q1].
   - by trans P2; [|trans Q2].
 Qed.
@@ -119,14 +122,14 @@ Local Hint Immediate False_elim : core.
 Lemma entails_eq_True P Q : (P ⊢ Q) ↔ ((P → Q)%I ≡ True%I).
 Proof.
   split=>EQ.
-  - apply bi.equiv_spec; split; [by apply True_intro|].
+  - apply bi.equiv_entails; split; [by apply True_intro|].
     apply impl_intro_r. rewrite and_elim_r //.
   - trans (P ∧ True)%I.
     + apply and_intro; first done. by apply pure_intro.
     + rewrite -EQ impl_elim_r. done.
 Qed.
 Lemma entails_impl_True P Q : (P ⊢ Q) ↔ (True ⊢ (P → Q)).
-Proof. rewrite entails_eq_True equiv_spec; naive_solver. Qed.
+Proof. rewrite entails_eq_True equiv_entails; naive_solver. Qed.
 
 Lemma and_mono P P' Q Q' : (P ⊢ Q) → (P' ⊢ Q') → P ∧ P' ⊢ Q ∧ Q'.
 Proof. auto. Qed.
@@ -229,7 +232,7 @@ Qed.
 Lemma exist_impl_forall {A} P (Ψ : A → PROP) :
   ((∃ x : A, Ψ x) → P) ⊣⊢ ∀ x : A, Ψ x → P.
 Proof.
-  apply equiv_spec; split.
+  apply equiv_entails; split.
   - apply forall_intro=>x. by rewrite -exist_intro.
   - apply impl_intro_r, impl_elim_r', exist_elim=>x.
     apply impl_intro_r. by rewrite (forall_elim x) impl_elim_r.
@@ -457,7 +460,7 @@ Proof. by apply forall_intro=> a; rewrite forall_elim. Qed.
 Lemma exist_wand_forall {A} P (Ψ : A → PROP) :
   ((∃ x : A, Ψ x) -∗ P) ⊣⊢ ∀ x : A, Ψ x -∗ P.
 Proof.
-  apply equiv_spec; split.
+  apply equiv_entails; split.
   - apply forall_intro=>x. by rewrite -exist_intro.
   - apply wand_intro_r, wand_elim_r', exist_elim=>x.
     apply wand_intro_r. by rewrite (forall_elim x) wand_elim_r.
@@ -1598,7 +1601,7 @@ Lemma limit_preserving_equiv {A : ofe} `{Cofe A} (Φ Ψ : A → PROP) :
   NonExpansive Φ → NonExpansive Ψ → LimitPreserving (λ x, Φ x ⊣⊢ Ψ x).
 Proof.
   intros HΦ HΨ. eapply limit_preserving_ext.
-  { intros x. symmetry; apply equiv_spec. }
+  { intros x. symmetry; apply equiv_entails. }
   apply limit_preserving_and; by apply limit_preserving_entails.
 Qed.
 Global Instance limit_preserving_Persistent {A:ofe} `{Cofe A} (Φ : A → PROP) :
diff --git a/iris/bi/embedding.v b/iris/bi/embedding.v
index 530a2d0e3..509f35cc1 100644
--- a/iris/bi/embedding.v
+++ b/iris/bi/embedding.v
@@ -134,7 +134,7 @@ Section embed.
 
   Global Instance embed_inj : Inj (≡) (≡) embed.
   Proof.
-    intros P Q EQ. apply bi.equiv_spec, conj; apply (inj embed); rewrite EQ //.
+    intros P Q EQ. apply bi.equiv_entails, conj; apply (inj embed); rewrite EQ //.
   Qed.
 
   Lemma embed_emp_valid (P : PROP1) : (⊢ ⎡P⎤) ↔ (⊢ P).
@@ -149,12 +149,12 @@ Section embed.
 
   Lemma embed_forall A (Φ : A → PROP1) : ⎡∀ x, Φ x⎤ ⊣⊢ ∀ x, ⎡Φ x⎤.
   Proof.
-    apply bi.equiv_spec; split; [|apply embed_forall_2].
+    apply bi.equiv_entails; split; [|apply embed_forall_2].
     apply bi.forall_intro=>?. by rewrite bi.forall_elim.
   Qed.
   Lemma embed_exist A (Φ : A → PROP1) : ⎡∃ x, Φ x⎤ ⊣⊢ ∃ x, ⎡Φ x⎤.
   Proof.
-    apply bi.equiv_spec; split; [apply embed_exist_1|].
+    apply bi.equiv_entails; split; [apply embed_exist_1|].
     apply bi.exist_elim=>?. by rewrite -bi.exist_intro.
   Qed.
   Lemma embed_and P Q : ⎡P ∧ Q⎤ ⊣⊢ ⎡P⎤ ∧ ⎡Q⎤.
@@ -163,18 +163,18 @@ Section embed.
   Proof. rewrite !bi.or_alt embed_exist. by f_equiv=>-[]. Qed.
   Lemma embed_impl P Q : ⎡P → Q⎤ ⊣⊢ (⎡P⎤ → ⎡Q⎤).
   Proof.
-    apply bi.equiv_spec; split; [|apply embed_impl_2].
+    apply bi.equiv_entails; split; [|apply embed_impl_2].
     apply bi.impl_intro_l. by rewrite -embed_and bi.impl_elim_r.
   Qed.
   Lemma embed_wand P Q : ⎡P -∗ Q⎤ ⊣⊢ (⎡P⎤ -∗ ⎡Q⎤).
   Proof.
-    apply bi.equiv_spec; split; [|apply embed_wand_2].
+    apply bi.equiv_entails; split; [|apply embed_wand_2].
     apply bi.wand_intro_l. by rewrite -embed_sep bi.wand_elim_r.
   Qed.
   Lemma embed_pure φ : ⎡⌜φ⌝⎤ ⊣⊢ ⌜φ⌝.
   Proof.
     rewrite (@bi.pure_alt PROP1) (@bi.pure_alt PROP2) embed_exist.
-    do 2 f_equiv. apply bi.equiv_spec. split; [apply bi.True_intro|].
+    do 2 f_equiv. apply bi.equiv_entails. split; [apply bi.True_intro|].
     rewrite -(_ : (emp → emp : PROP1) ⊢ True) ?embed_impl;
       last apply bi.True_intro.
     apply bi.impl_intro_l. by rewrite right_id.
@@ -293,7 +293,7 @@ Section embed.
 
     Lemma embed_internal_eq (A : ofe) (x y : A) : ⎡x ≡ y⎤ ⊣⊢@{PROP2} x ≡ y.
     Proof.
-      apply bi.equiv_spec; split; [apply embed_internal_eq_1|].
+      apply bi.equiv_entails; split; [apply embed_internal_eq_1|].
       etrans; [apply (internal_eq_rewrite x y (λ y, ⎡x ≡ y⎤%I)); solve_proper|].
       rewrite -(internal_eq_refl True%I) embed_pure.
       eapply bi.impl_elim; [done|]. apply bi.True_intro.
diff --git a/iris/bi/interface.v b/iris/bi/interface.v
index ce04316c2..5447c68ed 100644
--- a/iris/bi/interface.v
+++ b/iris/bi/interface.v
@@ -47,7 +47,7 @@ Section bi_mixin.
 
   Record BiMixin := {
     bi_mixin_entails_po : PreOrder bi_entails;
-    bi_mixin_equiv_spec P Q : (P ≡ Q) ↔ (P ⊢ Q) ∧ (Q ⊢ P);
+    bi_mixin_equiv_entails P Q : (P ≡ Q) ↔ (P ⊢ Q) ∧ (Q ⊢ P);
 
     (** Non-expansiveness *)
     bi_mixin_pure_ne n : Proper (iff ==> dist n) bi_pure;
@@ -278,8 +278,8 @@ Implicit Types A : Type.
 (* About the entailment *)
 Global Instance entails_po : PreOrder (@bi_entails PROP).
 Proof. eapply bi_mixin_entails_po, bi_bi_mixin. Qed.
-Lemma equiv_spec P Q : P ≡ Q ↔ (P ⊢ Q) ∧ (Q ⊢ P).
-Proof. eapply bi_mixin_equiv_spec, bi_bi_mixin. Qed.
+Lemma equiv_entails P Q : P ≡ Q ↔ (P ⊢ Q) ∧ (Q ⊢ P).
+Proof. eapply bi_mixin_equiv_entails, bi_bi_mixin. Qed.
 
 (* Non-expansiveness *)
 Global Instance pure_ne n : Proper (iff ==> dist n) (@bi_pure PROP).
diff --git a/iris/bi/lib/counterexamples.v b/iris/bi/lib/counterexamples.v
index 156759a0d..2ddae631c 100644
--- a/iris/bi/lib/counterexamples.v
+++ b/iris/bi/lib/counterexamples.v
@@ -169,7 +169,7 @@ Module inv. Section inv.
   Proof. intros P Q ?. by apply fupd_mono. Qed.
   Global Instance fupd_proper E : Proper ((⊣⊢) ==> (⊣⊢)) (fupd E).
   Proof.
-    intros P Q; rewrite !bi.equiv_spec=> -[??]; split; by apply fupd_mono.
+    intros P Q; rewrite !bi.equiv_entails=> -[??]; split; by apply fupd_mono.
   Qed.
 
   Lemma fupd_frame_r E P Q : fupd E P ∗ Q ⊢ fupd E (P ∗ Q).
@@ -307,7 +307,7 @@ Module linear. Section linear.
   Proof. intros P Q ?. by apply fupd_mono. Qed.
   Global Instance fupd_proper E1 E2 : Proper ((⊣⊢) ==> (⊣⊢)) (fupd E1 E2).
   Proof.
-    intros P Q; rewrite !bi.equiv_spec=> -[??]; split; by apply fupd_mono.
+    intros P Q; rewrite !bi.equiv_entails=> -[??]; split; by apply fupd_mono.
   Qed.
 
   Lemma fupd_frame_r E1 E2 P Q : fupd E1 E2 P ∗ Q ⊢ fupd E1 E2 (P ∗ Q).
diff --git a/iris/bi/monpred.v b/iris/bi/monpred.v
index f09bf301b..0e9f1eb97 100644
--- a/iris/bi/monpred.v
+++ b/iris/bi/monpred.v
@@ -98,7 +98,7 @@ Global Instance monPred_at_ne (R : relation I) :
   ∀ n, Proper (dist n ==> R ==> dist n) monPred_at.
 Proof.
   intros ????? [Hd] ?? HR. rewrite Hd.
-  apply equiv_dist, bi.equiv_spec; split; f_equiv; rewrite ->HR; done.
+  apply equiv_dist, bi.equiv_entails; split; f_equiv; rewrite ->HR; done.
 Qed.
 Global Instance monPred_at_proper (R : relation I) :
   Proper (R ==> R ==> iff) (⊑) → Reflexive R →
@@ -255,8 +255,8 @@ Proof.
     + intros P. by split.
     + intros P Q R [H1] [H2]. split => ?. by rewrite H1 H2.
   - split.
-    + intros [HPQ]. split; split => i; move: (HPQ i); by apply bi.equiv_spec.
-    + intros [[] []]. split=>i. by apply bi.equiv_spec.
+    + intros [HPQ]. split; split => i; move: (HPQ i); by apply bi.equiv_entails.
+    + intros [[] []]. split=>i. by apply bi.equiv_entails.
   - intros P φ ?. split=> i. by apply bi.pure_intro.
   - intros φ P HP. split=> i. apply bi.pure_elim'=> ?. by apply HP.
   - intros P Q. split=> i. by apply bi.and_elim_l.
@@ -508,18 +508,18 @@ Lemma monPred_objectively_elim P : <obj> P ⊢ P.
 Proof. rewrite monPred_objectively_unfold. unseal. split=>?. apply bi.forall_elim. Qed.
 Lemma monPred_objectively_idemp P : <obj> <obj> P ⊣⊢ <obj> P.
 Proof.
-  apply bi.equiv_spec; split; [by apply monPred_objectively_elim|].
+  apply bi.equiv_entails; split; [by apply monPred_objectively_elim|].
   unseal. split=>i /=. by apply bi.forall_intro=>_.
 Qed.
 
 Lemma monPred_objectively_forall {A} (Φ : A → monPred) : <obj> (∀ x, Φ x) ⊣⊢ ∀ x, <obj> (Φ x).
 Proof.
-  unseal. split=>i. apply bi.equiv_spec; split=>/=;
+  unseal. split=>i. apply bi.equiv_entails; split=>/=;
     do 2 apply bi.forall_intro=>?; by do 2 rewrite bi.forall_elim.
 Qed.
 Lemma monPred_objectively_and P Q : <obj> (P ∧ Q) ⊣⊢ <obj> P ∧ <obj> Q.
 Proof.
-  unseal. split=>i. apply bi.equiv_spec; split=>/=.
+  unseal. split=>i. apply bi.equiv_entails; split=>/=.
   - apply bi.and_intro; do 2 f_equiv.
     + apply bi.and_elim_l.
     + apply bi.and_elim_r.
@@ -539,12 +539,12 @@ Lemma monPred_objectively_sep_2 P Q : <obj> P ∗ <obj> Q ⊢ <obj> (P ∗ Q).
 Proof. unseal. split=>i /=. apply bi.forall_intro=>?. by rewrite !bi.forall_elim. Qed.
 Lemma monPred_objectively_sep `{BiIndexBottom bot} P Q : <obj> (P ∗ Q) ⊣⊢ <obj> P ∗ <obj> Q.
 Proof.
-  apply bi.equiv_spec, conj, monPred_objectively_sep_2. unseal. split=>i /=.
+  apply bi.equiv_entails, conj, monPred_objectively_sep_2. unseal. split=>i /=.
   rewrite (bi.forall_elim bot). by f_equiv; apply bi.forall_intro=>j; f_equiv.
 Qed.
 Lemma monPred_objectively_embed (P : PROP) : <obj> ⎡P⎤ ⊣⊢ ⎡P⎤.
 Proof.
-  apply bi.equiv_spec; split; unseal; split=>i /=.
+  apply bi.equiv_entails; split; unseal; split=>i /=.
   - by rewrite (bi.forall_elim inhabitant).
   - by apply bi.forall_intro.
 Qed.
@@ -567,12 +567,12 @@ Proof.
 Qed.
 Lemma monPred_subjectively_exist {A} (Φ : A → monPred) : <subj> (∃ x, Φ x) ⊣⊢ ∃ x, <subj> (Φ x).
 Proof.
-  unseal. split=>i. apply bi.equiv_spec; split=>/=;
+  unseal. split=>i. apply bi.equiv_entails; split=>/=;
     do 2 apply bi.exist_elim=>?; by do 2 rewrite -bi.exist_intro.
 Qed.
 Lemma monPred_subjectively_or P Q : <subj> (P ∨ Q) ⊣⊢ <subj> P ∨ <subj> Q.
 Proof.
-  unseal. split=>i. apply bi.equiv_spec; split=>/=.
+  unseal. split=>i. apply bi.equiv_entails; split=>/=.
   - apply bi.exist_elim=>?. by rewrite -!bi.exist_intro.
   - apply bi.or_elim; do 2 f_equiv.
     + apply bi.or_intro_l.
@@ -584,7 +584,7 @@ Proof. unseal. split=>i /=. apply bi.exist_elim=>?. by rewrite -!bi.exist_intro.
 
 Lemma monPred_subjectively_idemp P : <subj> <subj> P ⊣⊢ <subj> P.
 Proof.
-  apply bi.equiv_spec; split; [|by apply monPred_subjectively_intro].
+  apply bi.equiv_entails; split; [|by apply monPred_subjectively_intro].
   unseal. split=>i /=. by apply bi.exist_elim=>_.
 Qed.
 
@@ -869,7 +869,7 @@ Proof. rewrite monPred_internal_eq_unfold. by apply monPred_at_embed. Qed.
 Lemma monPred_equivI `{!BiInternalEq PROP'} P Q :
   P ≡ Q ⊣⊢@{PROP'} ∀ i, P i ≡ Q i.
 Proof.
-  apply bi.equiv_spec. split.
+  apply bi.equiv_entails. split.
   - apply bi.forall_intro=> ?. apply (f_equivI (flip monPred_at _)).
   - by rewrite -{2}(sig_monPred_sig P) -{2}(sig_monPred_sig Q)
                -f_equivI -sig_equivI !discrete_fun_equivI.
diff --git a/iris/proofmode/environments.v b/iris/proofmode/environments.v
index ba5796dd3..5001cd299 100644
--- a/iris/proofmode/environments.v
+++ b/iris/proofmode/environments.v
@@ -439,7 +439,7 @@ Global Instance of_envs_proper' :
   Proper (env_Forall2 (⊣⊢) ==> env_Forall2 (⊣⊢) ==> (⊣⊢)) (@of_envs' PROP).
 Proof.
   intros Γp1 Γp2 Hp Γs1 Γs2 Hs; apply (anti_symm (⊢)); apply of_envs_mono';
-    eapply (env_Forall2_impl (⊣⊢)); by eauto using equiv_entails.
+    eapply (env_Forall2_impl (⊣⊢)); by eauto using equiv_entails_1_1.
 Qed.
 
 Global Instance of_envs_mono : Proper (envs_Forall2 (⊢) ==> (⊢)) (@of_envs PROP).
diff --git a/iris/proofmode/modalities.v b/iris/proofmode/modalities.v
index a2f494d09..7b215c7e3 100644
--- a/iris/proofmode/modalities.v
+++ b/iris/proofmode/modalities.v
@@ -136,7 +136,7 @@ Section modality.
   Global Instance modality_flip_mono' : Proper (flip (⊢) ==> flip (⊢)) M.
   Proof. intros P Q. apply modality_mono. Qed.
   Global Instance modality_proper : Proper ((≡) ==> (≡)) M.
-  Proof. intros P Q. rewrite !equiv_spec=> -[??]; eauto using modality_mono. Qed.
+  Proof. intros P Q. rewrite !equiv_entails=> -[??]; eauto using modality_mono. Qed.
 End modality.
 
 Section modality1.
diff --git a/iris/proofmode/modality_instances.v b/iris/proofmode/modality_instances.v
index ea0d67984..f35432dd5 100644
--- a/iris/proofmode/modality_instances.v
+++ b/iris/proofmode/modality_instances.v
@@ -9,7 +9,7 @@ Section modalities.
   Lemma modality_persistently_mixin :
     modality_mixin (@bi_persistently PROP) MIEnvId MIEnvClear.
   Proof.
-    split; simpl; eauto using equiv_entails_sym, persistently_intro,
+    split; simpl; eauto using equiv_entails_1_2, persistently_intro,
       persistently_mono, persistently_sep_2 with typeclass_instances.
   Qed.
   Definition modality_persistently :=
@@ -18,7 +18,7 @@ Section modalities.
   Lemma modality_affinely_mixin :
     modality_mixin (@bi_affinely PROP) MIEnvId (MIEnvForall Affine).
   Proof.
-    split; simpl; eauto using equiv_entails_sym, affinely_intro, affinely_mono,
+    split; simpl; eauto using equiv_entails_1_2, affinely_intro, affinely_mono,
       affinely_sep_2 with typeclass_instances.
   Qed.
   Definition modality_affinely :=
@@ -27,7 +27,7 @@ Section modalities.
   Lemma modality_intuitionistically_mixin :
     modality_mixin (@bi_intuitionistically PROP) MIEnvId MIEnvIsEmpty.
   Proof.
-    split; simpl; eauto using equiv_entails_sym, intuitionistically_emp,
+    split; simpl; eauto using equiv_entails_1_2, intuitionistically_emp,
       affinely_mono, persistently_mono, intuitionistically_idemp,
       intuitionistically_sep_2 with typeclass_instances.
   Qed.
@@ -39,7 +39,7 @@ Section modalities.
       (MIEnvTransform IntoEmbed) (MIEnvTransform IntoEmbed).
   Proof.
     split; simpl; split_and?;
-      eauto using equiv_entails_sym, embed_emp_2, embed_sep, embed_and.
+      eauto using equiv_entails_1_2, embed_emp_2, embed_sep, embed_and.
     - intros P Q. rewrite /IntoEmbed=> ->. by rewrite embed_intuitionistically_2.
     - by intros P Q ->.
   Qed.
@@ -49,7 +49,7 @@ Section modalities.
   Lemma modality_plainly_mixin `{BiPlainly PROP} :
     modality_mixin (@plainly PROP _) (MIEnvForall Plain) MIEnvClear.
   Proof.
-    split; simpl; split_and?; eauto using equiv_entails_sym, plainly_intro,
+    split; simpl; split_and?; eauto using equiv_entails_1_2, plainly_intro,
       plainly_mono, plainly_and, plainly_sep_2 with typeclass_instances.
   Qed.
   Definition modality_plainly `{BiPlainly PROP} :=
@@ -59,7 +59,7 @@ Section modalities.
     modality_mixin (@bi_laterN PROP n)
       (MIEnvTransform (MaybeIntoLaterN false n)) (MIEnvTransform (MaybeIntoLaterN false n)).
   Proof.
-    split; simpl; split_and?; eauto using equiv_entails_sym, laterN_intro,
+    split; simpl; split_and?; eauto using equiv_entails_1_2, laterN_intro,
       laterN_mono, laterN_and, laterN_sep with typeclass_instances.
     rewrite /MaybeIntoLaterN=> P Q ->. by rewrite laterN_intuitionistically_2.
   Qed.
diff --git a/iris/proofmode/monpred.v b/iris/proofmode/monpred.v
index 4170bc9fd..bd70d2493 100644
--- a/iris/proofmode/monpred.v
+++ b/iris/proofmode/monpred.v
@@ -36,7 +36,7 @@ Section modalities.
   Proof.
     split; simpl; split_and?; intros;
       try select (TCDiag _ _ _) (fun H => destruct H);
-      eauto using bi.equiv_entails_sym, objective_objectively,
+      eauto using bi.equiv_entails_1_2, objective_objectively,
         monPred_objectively_mono, monPred_objectively_and,
         monPred_objectively_sep_2 with typeclass_instances.
   Qed.
diff --git a/iris/si_logic/bi.v b/iris/si_logic/bi.v
index 47a2e322f..40464d70f 100644
--- a/iris/si_logic/bi.v
+++ b/iris/si_logic/bi.v
@@ -25,7 +25,7 @@ Lemma siProp_bi_mixin :
 Proof.
   split.
   - exact: entails_po.
-  - exact: equiv_spec.
+  - exact: equiv_entails.
   - exact: pure_ne.
   - exact: and_ne.
   - exact: or_ne.
diff --git a/iris/si_logic/siprop.v b/iris/si_logic/siprop.v
index 94778022e..d4e4b09ea 100644
--- a/iris/si_logic/siprop.v
+++ b/iris/si_logic/siprop.v
@@ -155,7 +155,7 @@ Proof.
 Qed.
 Lemma entails_anti_symm : AntiSymm (≡) siProp_entails.
 Proof. intros P Q HPQ HQP; split=> n; by split; [apply HPQ|apply HQP]. Qed.
-Lemma equiv_spec P Q : (P ≡ Q) ↔ (P ⊢ Q) ∧ (Q ⊢ P).
+Lemma equiv_entails P Q : (P ≡ Q) ↔ (P ⊢ Q) ∧ (Q ⊢ P).
 Proof.
   split.
   - intros HPQ; split; split=> i; apply HPQ.
-- 
GitLab