From 9ac050a90f495a1c81fd92d8f7aa2f0e0b9f019f Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 29 Mar 2019 19:31:40 +0100
Subject: [PATCH] more consistent naming

---
 theories/base_logic/bi.v                | 8 ++++----
 theories/base_logic/derived.v           | 6 +++---
 theories/base_logic/lib/fancy_updates.v | 2 +-
 theories/base_logic/upred.v             | 4 ++--
 4 files changed, 10 insertions(+), 10 deletions(-)

diff --git a/theories/base_logic/bi.v b/theories/base_logic/bi.v
index 5a6ef337e..dd7f9f7e5 100644
--- a/theories/base_logic/bi.v
+++ b/theories/base_logic/bi.v
@@ -206,11 +206,11 @@ Lemma ofe_fun_validI {A} {B : A → ucmraT} (g : ofe_fun B) : ✓ g ⊣⊢ ∀ i
 Proof. exact: uPred_primitive.ofe_fun_validI. Qed.
 
 (** Consistency/soundness statement *)
-Lemma soundness_pure φ : bi_emp_valid (PROP:=uPredI M) ⌜ φ ⌝ → φ.
-Proof. apply soundness_pure. Qed.
+Lemma pure_soundness φ : bi_emp_valid (PROP:=uPredI M) ⌜ φ ⌝ → φ.
+Proof. apply pure_soundness. Qed.
 
-Lemma soundness_later P : bi_emp_valid (▷ P) → bi_emp_valid P.
-Proof. apply soundness_later. Qed.
+Lemma later_soundness P : bi_emp_valid (▷ P) → bi_emp_valid P.
+Proof. apply later_soundness. Qed.
 End restate.
 
 (** See [derived.v] for the version for basic updates. *)
diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index 721431164..0adcc1a5c 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -92,7 +92,7 @@ Global Instance uPred_ownM_sep_homomorphism :
 Proof. split; [split; try apply _|]. apply ownM_op. apply ownM_unit'. Qed.
 
 (** Consistency/soundness statement *)
-Lemma soundness_bupd_plain P `{!Plain P} : bi_emp_valid (|==> P) → bi_emp_valid P.
+Lemma bupd_plain_soundness P `{!Plain P} : bi_emp_valid (|==> P) → bi_emp_valid P.
 Proof.
   eapply bi_emp_valid_mono. etrans; last exact: bupd_plainly. apply bupd_mono'.
   apply: plain.
@@ -101,8 +101,8 @@ Qed.
 Corollary soundness φ n : (▷^n ⌜ φ ⌝ : uPred M)%I → φ.
 Proof.
   induction n as [|n IH]=> /=.
-  - apply soundness_pure.
-  - intros H. by apply IH, soundness_later.
+  - apply pure_soundness.
+  - intros H. by apply IH, later_soundness.
 Qed.
 
 Corollary consistency_modal n : ¬ (▷^n False : uPred M)%I.
diff --git a/theories/base_logic/lib/fancy_updates.v b/theories/base_logic/lib/fancy_updates.v
index eed3e7016..6dfaa0d0c 100644
--- a/theories/base_logic/lib/fancy_updates.v
+++ b/theories/base_logic/lib/fancy_updates.v
@@ -62,7 +62,7 @@ Qed.
 Lemma fupd_plain_soundness `{!invPreG Σ} E1 E2 (P: iProp Σ) `{!Plain P}:
   (∀ `{Hinv: !invG Σ}, bi_emp_valid (|={E1,E2}=> P)) → bi_emp_valid P.
 Proof.
-  iIntros (Hfupd). apply soundness_later. iMod wsat_alloc as (Hinv) "[Hw HE]".
+  iIntros (Hfupd). apply later_soundness. iMod wsat_alloc as (Hinv) "[Hw HE]".
   iAssert (|={⊤,E2}=> P)%I as "H".
   { iMod fupd_intro_mask'; last iApply Hfupd. done. }
   rewrite uPred_fupd_eq /uPred_fupd_def.
diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index d9c180eb0..b9c90e970 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -801,10 +801,10 @@ Lemma ofe_fun_validI {A} {B : A → ucmraT} (g : ofe_fun B) : ✓ g ⊣⊢ ∀ i
 Proof. by unseal. Qed.
 
 (** Consistency/soundness statement *)
-Lemma soundness_pure φ : (True ⊢ ⌜ φ ⌝) → φ.
+Lemma pure_soundness φ : (True ⊢ ⌜ φ ⌝) → φ.
 Proof. unseal=> -[H]. by apply (H 0 ε); eauto using ucmra_unit_validN. Qed.
 
-Lemma soundness_later P : (True ⊢ ▷ P) → (True ⊢ P).
+Lemma later_soundness P : (True ⊢ ▷ P) → (True ⊢ P).
 Proof.
   unseal=> -[HP]; split=> n x Hx _.
   apply uPred_mono with n ε; eauto using ucmra_unit_leastN.
-- 
GitLab