From 3442e7aedcb48d1e1f10862d494632f8010319ca Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 18 Mar 2020 16:13:40 +0100
Subject: [PATCH] =?UTF-8?q?Turn=20some=20forgotten=20uses=20of=20`bi=5Femp?=
 =?UTF-8?q?=5Fvalid`=20into=20the=20new=20`=E2=8A=A2`=20notation.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 theories/base_logic/bi.v                |  6 +++---
 theories/base_logic/derived.v           |  2 +-
 theories/base_logic/lib/fancy_updates.v |  4 ++--
 theories/bi/embedding.v                 |  2 +-
 theories/proofmode/class_instances_bi.v |  6 +++---
 theories/proofmode/classes.v            |  6 +++---
 theories/proofmode/coq_tactics.v        |  6 +++---
 theories/proofmode/ltac_tactics.v       | 10 +++++-----
 theories/si_logic/bi.v                  |  6 +++---
 9 files changed, 24 insertions(+), 24 deletions(-)

diff --git a/theories/base_logic/bi.v b/theories/base_logic/bi.v
index df9d498f1..3b93a6e65 100644
--- a/theories/base_logic/bi.v
+++ b/theories/base_logic/bi.v
@@ -204,13 +204,13 @@ Lemma discrete_fun_validI {A} {B : A → ucmraT} (g : discrete_fun B) : ✓ g 
 Proof. exact: uPred_primitive.discrete_fun_validI. Qed.
 
 (** Consistency/soundness statement *)
-Lemma pure_soundness φ : bi_emp_valid (PROP:=uPredI M) ⌜ φ ⌝ → φ.
+Lemma pure_soundness φ : (⊢@{uPredI M} ⌜ φ ⌝) → φ.
 Proof. apply pure_soundness. Qed.
 
-Lemma internal_eq_soundness {A : ofeT} (x y : A) : (True ⊢ x ≡ y) → x ≡ y.
+Lemma internal_eq_soundness {A : ofeT} (x y : A) : (⊢@{uPredI M} x ≡ y) → x ≡ y.
 Proof. apply internal_eq_soundness. Qed.
 
-Lemma later_soundness P : bi_emp_valid (▷ P) → bi_emp_valid P.
+Lemma later_soundness P : (⊢ ▷ P) → ⊢ P.
 Proof. apply later_soundness. Qed.
 (** See [derived.v] for a similar soundness result for basic updates. *)
 End restate.
diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index e300eb8e5..01dff355c 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -84,7 +84,7 @@ Global Instance uPred_ownM_sep_homomorphism :
 Proof. split; [split; try apply _|]. apply ownM_op. apply ownM_unit'. Qed.
 
 (** Consistency/soundness statement *)
-Lemma bupd_plain_soundness P `{!Plain P} : bi_emp_valid (|==> P) → bi_emp_valid P.
+Lemma bupd_plain_soundness P `{!Plain P} : (⊢ |==> P) → ⊢ P.
 Proof.
   eapply bi_emp_valid_mono. etrans; last exact: bupd_plainly. apply bupd_mono'.
   apply: plain.
diff --git a/theories/base_logic/lib/fancy_updates.v b/theories/base_logic/lib/fancy_updates.v
index 3be5ca307..6317a7487 100644
--- a/theories/base_logic/lib/fancy_updates.v
+++ b/theories/base_logic/lib/fancy_updates.v
@@ -59,8 +59,8 @@ Proof.
     by iFrame.
 Qed.
 
-Lemma fupd_plain_soundness `{!invPreG Σ} E1 E2 (P: iProp Σ) `{!Plain P}:
-  (∀ `{Hinv: !invG Σ}, bi_emp_valid (|={E1,E2}=> P)) → bi_emp_valid P.
+Lemma fupd_plain_soundness `{!invPreG Σ} E1 E2 (P: iProp Σ) `{!Plain P} :
+  (∀ `{Hinv: !invG Σ}, ⊢ |={E1,E2}=> P) → ⊢ P.
 Proof.
   iIntros (Hfupd). apply later_soundness. iMod wsat_alloc as (Hinv) "[Hw HE]".
   iAssert (|={⊤,E2}=> P)%I as "H".
diff --git a/theories/bi/embedding.v b/theories/bi/embedding.v
index 3eaa91784..bbf87f95d 100644
--- a/theories/bi/embedding.v
+++ b/theories/bi/embedding.v
@@ -15,7 +15,7 @@ Record BiEmbedMixin (PROP1 PROP2 : bi) `(Embed PROP1 PROP2) := {
   bi_embed_mixin_ne : NonExpansive (embed (A:=PROP1) (B:=PROP2));
   bi_embed_mixin_mono : Proper ((⊢) ==> (⊢)) (embed (A:=PROP1) (B:=PROP2));
   bi_embed_mixin_emp_valid_inj (P : PROP1) :
-    bi_emp_valid (PROP:=PROP2) ⎡P⎤ → bi_emp_valid P;
+    (⊢@{PROP2} ⎡P⎤) → ⊢ P;
   bi_embed_mixin_emp_2 : emp ⊢@{PROP2} ⎡emp⎤;
   bi_embed_mixin_impl_2 (P Q : PROP1) :
     (⎡P⎤ → ⎡Q⎤) ⊢@{PROP2} ⎡P → Q⎤;
diff --git a/theories/proofmode/class_instances_bi.v b/theories/proofmode/class_instances_bi.v
index f5adfc0d3..fd6b4d4d5 100644
--- a/theories/proofmode/class_instances_bi.v
+++ b/theories/proofmode/class_instances_bi.v
@@ -31,7 +31,7 @@ Implicit Types P Q R : PROP.
 Implicit Types mP : option PROP.
 
 (** AsEmpValid *)
-Global Instance as_emp_valid_emp_valid P : AsEmpValid0 (bi_emp_valid P) P | 0.
+Global Instance as_emp_valid_emp_valid P : AsEmpValid0 (⊢ P) P | 0.
 Proof. by rewrite /AsEmpValid. Qed.
 Global Instance as_emp_valid_entails P Q : AsEmpValid0 (P ⊢ Q) (P -∗ Q).
 Proof. split. apply bi.entails_wand. apply bi.wand_entails. Qed.
@@ -986,10 +986,10 @@ Qed.
 (* These instances must be used only after [into_forall_wand_pure] and
 [into_forall_wand_pure] above. *)
 Global Instance into_forall_wand P Q :
-  IntoForall (P -∗ Q) (λ _ : bi_emp_valid P, Q) | 10.
+  IntoForall (P -∗ Q) (λ _ : ⊢ P, Q) | 10.
 Proof. rewrite /IntoForall. apply forall_intro=><-. rewrite emp_wand //. Qed.
 Global Instance into_forall_impl `{!BiAffine PROP} P Q :
-  IntoForall (P → Q) (λ _ : bi_emp_valid P, Q) | 10.
+  IntoForall (P → Q) (λ _ : ⊢ P, Q) | 10.
 Proof. rewrite /IntoForall. apply forall_intro=><-. rewrite -True_emp True_impl //. Qed.
 
 (** FromForall *)
diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index a71e35277..d9603ff41 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -492,7 +492,7 @@ Hint Mode IntoEmbed + + + ! -  : typeclass_instances.
    [Hint Mode - ! -], but the fact that Coq ignores primitive
    projections for hints modes would make this fail.*)
 Class AsEmpValid {PROP : bi} (φ : Prop) (P : PROP) :=
-  as_emp_valid : φ ↔ bi_emp_valid P.
+  as_emp_valid : φ ↔ ⊢ P.
 Arguments AsEmpValid {_} _%type _%I.
 Class AsEmpValid0 {PROP : bi} (φ : Prop) (P : PROP) :=
   as_emp_valid_0 : AsEmpValid φ P.
@@ -500,10 +500,10 @@ Arguments AsEmpValid0 {_} _%type _%I.
 Existing Instance as_emp_valid_0 | 0.
 
 Lemma as_emp_valid_1 (φ : Prop) {PROP : bi} (P : PROP) `{!AsEmpValid φ P} :
-  φ → bi_emp_valid P.
+  φ → ⊢ P.
 Proof. by apply as_emp_valid. Qed.
 Lemma as_emp_valid_2 (φ : Prop) {PROP : bi} (P : PROP) `{!AsEmpValid φ P} :
-  bi_emp_valid P → φ.
+  (⊢ P) → φ.
 Proof. by apply as_emp_valid. Qed.
 
 (* Input: [P]; Outputs: [N],
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index ccf395f4d..8d38f7f97 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -15,7 +15,7 @@ Implicit Types Δ : envs PROP.
 Implicit Types P Q : PROP.
 
 (** * Starting and stopping the proof mode *)
-Lemma tac_start P : envs_entails (Envs Enil Enil 1) P → bi_emp_valid P.
+Lemma tac_start P : envs_entails (Envs Enil Enil 1) P → ⊢ P.
 Proof.
   rewrite envs_entails_eq !of_envs_eq /=.
   rewrite intuitionistically_True_emp left_id=><-.
@@ -477,7 +477,7 @@ Proof.
   by rewrite -(entails_wand P) // intuitionistically_emp emp_wand.
 Qed.
 
-Definition IntoEmpValid (φ : Type) (P : PROP) := φ → bi_emp_valid P.
+Definition IntoEmpValid (φ : Type) (P : PROP) := φ → ⊢ P.
 (** These lemmas are [Defined] because the guardedness checker must see
 through them. See https://gitlab.mpi-sws.org/iris/iris/issues/274. For the
 same reason, their bodies use as little automation as possible. *)
@@ -489,7 +489,7 @@ Proof. rewrite /IntoEmpValid => Hφ Hi1 Hi2. apply Hi1, Hi2, Hφ. Defined.
 Lemma into_emp_valid_forall {A} (φ : A → Type) P x :
   IntoEmpValid (φ x) P → IntoEmpValid (∀ x : A, φ x) P.
 Proof. rewrite /IntoEmpValid => Hi1 Hi2. apply Hi1, Hi2. Defined.
-Lemma into_emp_valid_proj φ P : IntoEmpValid φ P → φ → bi_emp_valid P.
+Lemma into_emp_valid_proj φ P : IntoEmpValid φ P → φ → ⊢ P.
 Proof. intros HP. apply HP. Defined.
 
 (** When called by the proof mode, the proof of [P] is produced by calling
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index 493d2ebbb..418f25c0d 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -747,7 +747,7 @@ Tactic Notation "iPoseProofCoreHyp" constr(H) "as" constr(Hnew) :=
     end.
 
 (* The tactic [iIntoEmpValid] tactic "imports a Coq lemma into the proofmode",
-i.e. it solves a goal [IntoEmpValid ψ ?Q]. The argument [ψ] must be of the
+i.e., it solves a goal [IntoEmpValid ψ ?Q]. The argument [ψ] must be of the
 following shape:
 
 [∀ (x_1 : A_1) .. (x_n : A_n), φ]
@@ -756,14 +756,14 @@ for which we have an instance [AsEmpValid φ ?Q].
 
 Examples of such [φ]s are
 
-- [bi_emp_valid P], in which case [?Q] is unified with [P].
+- [⊢ P], in which case [?Q] is unified with [P].
 - [P1 ⊢ P2], in which case [?Q] is unified with [P1 -∗ P2].
 - [P1 ⊣⊢ P2], in which case [?Q] is unified with [P1 ↔ P2].
 
 The tactic instantiates each dependent argument [x_i : A_i] with an evar, and
 generates a goal [A_i] for each non-dependent argument [x_i : A_i].
 
-For example, if goal is [bi_emp_valid (∀ x, P x → R1 x ⊢ R2 x) ?Q], then the
+For example, if goal is [IntoEmpValid (∀ x, P x → R1 x ⊢ R2 x) ?Q], then the
 [iIntoEmpValid] tactic generates an evar [?x], a subgoal [P ?x], and unifies
 [?Q] with [R1 ?x -∗ R2 ?x]. *)
 Ltac iIntoEmpValid_go := first
@@ -772,7 +772,7 @@ Ltac iIntoEmpValid_go := first
      [(*goal for [φ] *)|iIntoEmpValid_go]
   |(* Case [∀ x : A, φ] *)
    notypeclasses refine (into_emp_valid_forall _ _ _ _); iIntoEmpValid_go
-  |(* Case [P ⊢ Q], [P ⊣⊢ Q], [bi_emp_valid P] *)
+  |(* Case [P ⊢ Q], [P ⊣⊢ Q], [⊢ P] *)
    notypeclasses refine (into_emp_valid_here _ _ _)].
 
 Ltac iIntoEmpValid :=
@@ -3191,7 +3191,7 @@ Tactic Notation "iAccu" :=
 
 (** Automation *)
 Hint Extern 0 (_ ⊢ _) => iStartProof : core.
-Hint Extern 0 (bi_emp_valid _) => iStartProof : core.
+Hint Extern 0 (⊢ _) => iStartProof : core.
 
 (* Make sure that by and done solve trivial things in proof mode *)
 Hint Extern 0 (envs_entails _ _) => iPureIntro; try done : core.
diff --git a/theories/si_logic/bi.v b/theories/si_logic/bi.v
index d7d9f5aa3..d613e3f0e 100644
--- a/theories/si_logic/bi.v
+++ b/theories/si_logic/bi.v
@@ -159,13 +159,13 @@ Proof. done. Qed.
 
 Module siProp.
 Section restate.
-Lemma pure_soundness φ : bi_emp_valid (PROP:=siPropI) ⌜ φ ⌝ → φ.
+Lemma pure_soundness φ : (⊢@{siPropI} ⌜ φ ⌝) → φ.
 Proof. apply pure_soundness. Qed.
 
-Lemma internal_eq_soundness {A : ofeT} (x y : A) : (True ⊢@{siPropI} x ≡ y) → x ≡ y.
+Lemma internal_eq_soundness {A : ofeT} (x y : A) : (⊢@{siPropI} x ≡ y) → x ≡ y.
 Proof. apply internal_eq_soundness. Qed.
 
-Lemma later_soundness P : bi_emp_valid (PROP:=siPropI) (▷ P) → bi_emp_valid P.
+Lemma later_soundness (P : siProp) : (⊢ ▷ P) → ⊢ P.
 Proof. apply later_soundness. Qed.
 End restate.
 End siProp.
-- 
GitLab