From 01ffa4a8eef56b4550789cd61cf1b020c24f02a9 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sun, 13 Nov 2022 10:48:57 +0100
Subject: [PATCH] remove _plain from soundness lemma names

---
 iris/base_logic/derived.v           |  6 ++---
 iris/base_logic/lib/fancy_updates.v | 36 ++++++++++++++---------------
 iris/base_logic/lib/later_credits.v |  4 ++--
 iris/program_logic/adequacy.v       |  4 ++--
 iris/program_logic/total_adequacy.v |  2 +-
 5 files changed, 26 insertions(+), 26 deletions(-)

diff --git a/iris/base_logic/derived.v b/iris/base_logic/derived.v
index af8e2ab96..8b61b8196 100644
--- a/iris/base_logic/derived.v
+++ b/iris/base_logic/derived.v
@@ -87,13 +87,13 @@ Proof. split; [split|]; try apply _; [apply ownM_op | apply ownM_unit']. Qed.
 (** Soundness statement: facts derived in the logic / under modalities also hold
 outside the logic / without the modalities.
 (The other modalities, â–¡ and â– , can simply be stripped so they are obvious.) *)
-Lemma bupd_plain_soundness P `{!Plain P} : (⊢ |==> P) → ⊢ P.
+Lemma bupd_soundness P `{!Plain P} : (⊢ |==> P) → ⊢ P.
 Proof. rewrite bupd_plain. done. Qed.
 
 Lemma laterN_soundness P n : (⊢ ▷^n P) → ⊢ P.
 Proof. induction n; eauto using later_soundness. Qed.
 
-Lemma modal_plain_soundness P `{!Plain P} n :
+Lemma modal_soundness P `{!Plain P} n :
   (⊢ Nat.iter n (bupd ∘ bi_later) P) → ⊢ P.
 Proof.
   intros H. apply (laterN_soundness _ n).
@@ -115,7 +115,7 @@ Proof. intros H. by eapply pure_soundness. Qed.
 Corollary consistency_modal n :
   ¬ ⊢@{uPredI M} Nat.iter n (bupd ∘ bi_later) False.
 Proof.
-  intros H. eapply pure_soundness, modal_plain_soundness, H.
+  intros H. eapply pure_soundness, modal_soundness, H.
   apply _.
 Qed.
 
diff --git a/iris/base_logic/lib/fancy_updates.v b/iris/base_logic/lib/fancy_updates.v
index 9e5b9737f..582e0111c 100644
--- a/iris/base_logic/lib/fancy_updates.v
+++ b/iris/base_logic/lib/fancy_updates.v
@@ -135,7 +135,7 @@ Qed.
 (** Note: the [_no_lc] soundness lemmas also allow generating later credits, but
   these cannot be used for anything. They are merely provided to enable making
   the adequacy proof generic in whether later credits are used. *)
-Lemma fupd_plain_soundness_no_lc `{!invGpreS Σ} E1 E2 (P : iProp Σ) `{!Plain P} m :
+Lemma fupd_soundness_no_lc `{!invGpreS Σ} E1 E2 (P : iProp Σ) `{!Plain P} m :
   (∀ `{Hinv: !invGS_gen HasNoLc Σ}, £ m ⊢ |={E1,E2}=> P) → ⊢ P.
 Proof.
   iIntros (Hfupd). apply later_soundness. iMod wsat_alloc as (Hw) "[Hw HE]".
@@ -148,10 +148,10 @@ Proof.
   iMod ("H" with "[$]") as "[Hw [HE >H']]"; iFrame.
 Qed.
 
-Lemma fupd_plain_soundness_lc `{!invGpreS Σ} n E1 E2 (P : iProp Σ) `{!Plain P} :
+Lemma fupd_soundness_lc `{!invGpreS Σ} n E1 E2 (P : iProp Σ) `{!Plain P} :
   (∀ `{Hinv: !invGS_gen HasLc Σ}, £ n ⊢@{iPropI Σ} |={E1,E2}=> P) → ⊢ P.
 Proof.
-  iIntros (Hfupd). eapply (lc_plain_soundness (S n)); first done.
+  iIntros (Hfupd). eapply (lc_soundness (S n)); first done.
   intros Hc. rewrite lc_succ.
   iIntros "[Hone Hn]". rewrite -le_upd_trans. iApply bupd_le_upd.
   iMod wsat_alloc as (Hw) "[Hw HE]".
@@ -167,26 +167,26 @@ Qed.
 
 (** Generic soundness lemma for the fancy update, parameterized by [use_credits]
   on whether to use credits or not. *)
-Lemma fupd_plain_soundness_gen `{!invGpreS Σ} (P : iProp Σ) `{!Plain P}
+Lemma fupd_soundness_gen `{!invGpreS Σ} (P : iProp Σ) `{!Plain P}
   (hlc : has_lc) n E1 E2 :
   (∀ `{Hinv : invGS_gen hlc Σ},
     £ n ={E1,E2}=∗ P) →
   ⊢ P.
 Proof.
   destruct hlc.
-  - apply fupd_plain_soundness_lc. done.
-  - apply fupd_plain_soundness_no_lc. done.
+  - apply fupd_soundness_lc. done.
+  - apply fupd_soundness_no_lc. done.
 Qed.
 
 (** [step_fupdN] soundness lemmas *)
 
-Lemma step_fupdN_plain_soundness_no_lc `{!invGpreS Σ} (P : iProp Σ) `{!Plain P} n m :
+Lemma step_fupdN_soundness_no_lc `{!invGpreS Σ} (P : iProp Σ) `{!Plain P} n m :
   (∀ `{Hinv: !invGS_gen HasNoLc Σ}, £ m ⊢@{iPropI Σ} |={⊤,∅}=> |={∅}▷=>^n P) →
   ⊢ P.
 Proof.
   intros Hiter.
   apply (laterN_soundness _  (S n)); simpl.
-  apply (fupd_plain_soundness_no_lc ⊤ ⊤ _ m)=> Hinv. iIntros "Hc".
+  apply (fupd_soundness_no_lc ⊤ ⊤ _ m)=> Hinv. iIntros "Hc".
   iPoseProof (Hiter Hinv) as "H". clear Hiter.
   iApply fupd_plainly_mask_empty. iSpecialize ("H" with "Hc").
   iMod (step_fupdN_plain with "H") as "H". iMod "H". iModIntro.
@@ -194,11 +194,11 @@ Proof.
   iNext. iMod "H" as "#H". auto.
 Qed.
 
-Lemma step_fupdN_plain_soundness_no_lc' `{!invGpreS Σ} (P : iProp Σ) `{!Plain P} n m :
+Lemma step_fupdN_soundness_no_lc' `{!invGpreS Σ} (P : iProp Σ) `{!Plain P} n m :
   (∀ `{Hinv: !invGS_gen HasNoLc Σ}, £ m ⊢@{iPropI Σ} |={⊤}[∅]▷=>^n P) →
   ⊢ P.
 Proof.
-  iIntros (Hiter). eapply (step_fupdN_plain_soundness_no_lc _ n m)=>Hinv.
+  iIntros (Hiter). eapply (step_fupdN_soundness_no_lc _ n m)=>Hinv.
   iIntros "Hcred". destruct n as [|n].
   { by iApply fupd_mask_intro_discard; [|iApply (Hiter Hinv)]. }
    simpl in Hiter |- *. iMod (Hiter with "Hcred") as "H". iIntros "!>!>!>".
@@ -206,12 +206,12 @@ Proof.
   simpl. iMod "H". iIntros "!>!>!>". iMod "H". by iApply "IH".
 Qed.
 
-Lemma step_fupdN_plain_soundness_lc `{!invGpreS Σ} (P : iProp Σ) `{!Plain P} n m :
+Lemma step_fupdN_soundness_lc `{!invGpreS Σ} (P : iProp Σ) `{!Plain P} n m :
   (∀ `{Hinv: !invGS_gen HasLc Σ}, £ m ⊢@{iPropI Σ} |={⊤,∅}=> |={∅}▷=>^n P) →
   ⊢ P.
 Proof.
   intros Hiter.
-  eapply (fupd_plain_soundness_lc (m + n)); [apply _..|].
+  eapply (fupd_soundness_lc (m + n)); [apply _..|].
   iIntros (Hinv) "Hlc". rewrite lc_split.
   iDestruct "Hlc" as "[Hm Hn]". iMod (Hiter with "Hm") as "Hupd".
   clear Hiter.
@@ -222,16 +222,16 @@ Proof.
     by iApply ("IH" with "Hn Hupd").
 Qed.
 
-Lemma step_fupdN_plain_soundness_lc' `{!invGpreS Σ} (P : iProp Σ) `{!Plain P} n m :
+Lemma step_fupdN_soundness_lc' `{!invGpreS Σ} (P : iProp Σ) `{!Plain P} n m :
   (∀ `{Hinv: !invGS_gen hlc Σ}, £ m ⊢@{iPropI Σ} |={⊤}[∅]▷=>^n P) →
   ⊢ P.
 Proof.
   intros Hiter.
-  eapply (fupd_plain_soundness_lc (m + n) ⊤ ⊤); [apply _..|].
+  eapply (fupd_soundness_lc (m + n) ⊤ ⊤); [apply _..|].
   iIntros (Hinv) "Hlc". rewrite lc_split.
   iDestruct "Hlc" as "[Hm Hn]". iPoseProof (Hiter with "Hm") as "Hupd".
   clear Hiter.
-  (* FIXME can we reuse [step_fupdN_plain_soundness_lc] instead of redoing the induction? *)
+  (* FIXME can we reuse [step_fupdN_soundness_lc] instead of redoing the induction? *)
   iInduction n as [|n] "IH"; simpl.
   - by iModIntro.
   - rewrite lc_succ. iDestruct "Hn" as "[Hone Hn]".
@@ -241,13 +241,13 @@ Qed.
 
 (** Generic soundness lemma for the fancy update, parameterized by [use_credits]
   on whether to use credits or not. *)
-Lemma step_fupdN_plain_soundness_gen `{!invGpreS Σ} (P : iProp Σ) `{!Plain P}
+Lemma step_fupdN_soundness_gen `{!invGpreS Σ} (P : iProp Σ) `{!Plain P}
   (hlc : has_lc) (n m : nat) :
   (∀ `{Hinv : invGS_gen hlc Σ},
     £ m ={⊤,∅}=∗ |={∅}▷=>^n P) →
   ⊢ P.
 Proof.
   destruct hlc.
-  - apply step_fupdN_plain_soundness_lc. done.
-  - apply step_fupdN_plain_soundness_no_lc. done.
+  - apply step_fupdN_soundness_lc. done.
+  - apply step_fupdN_soundness_no_lc. done.
 Qed.
diff --git a/iris/base_logic/lib/later_credits.v b/iris/base_logic/lib/later_credits.v
index b787593a7..09b55d1c7 100644
--- a/iris/base_logic/lib/later_credits.v
+++ b/iris/base_logic/lib/later_credits.v
@@ -357,11 +357,11 @@ Module le_upd.
     iModIntro. iExists C. iFrame.
   Qed.
 
-  Lemma lc_plain_soundness `{!lcGpreS Σ} m (P : iProp Σ) `{!Plain P} :
+  Lemma lc_soundness `{!lcGpreS Σ} m (P : iProp Σ) `{!Plain P} :
     (∀ {Hc: lcGS Σ}, £ m -∗ |==£> P) → ⊢ P.
   Proof.
     intros H. apply (laterN_soundness _ (S m)).
-    eapply bupd_plain_soundness; first apply _.
+    eapply bupd_soundness; first apply _.
     iStartProof.
     iMod (lc_alloc m) as (C) "[H● H◯]".
     iPoseProof (H C) as "Hc". iSpecialize ("Hc" with "Hâ—¯").
diff --git a/iris/program_logic/adequacy.v b/iris/program_logic/adequacy.v
index ccd97d2d1..af16bb748 100644
--- a/iris/program_logic/adequacy.v
+++ b/iris/program_logic/adequacy.v
@@ -156,7 +156,7 @@ Local Lemma wp_progress_gen (hlc : has_lc) Σ Λ `{!invGpreS Σ} es σ1 n κs t2
 Proof.
   iIntros (Hwp ??).
   eapply pure_soundness.
-  eapply (step_fupdN_plain_soundness_gen _ hlc (steps_sum num_laters_per_step 0 n)
+  eapply (step_fupdN_soundness_gen _ hlc (steps_sum num_laters_per_step 0 n)
     (steps_sum num_laters_per_step 0 n)).
   iIntros (Hinv) "Hcred".
   iMod Hwp as (stateI Φ fork_post state_interp_mono) "(Hσ & Hwp)".
@@ -214,7 +214,7 @@ Lemma wp_strong_adequacy_gen (hlc : has_lc) Σ Λ `{!invGpreS Σ} s es σ1 n κs
 Proof.
   iIntros (Hwp ?).
   eapply pure_soundness.
-  eapply (step_fupdN_plain_soundness_gen _ hlc (steps_sum num_laters_per_step 0 n)
+  eapply (step_fupdN_soundness_gen _ hlc (steps_sum num_laters_per_step 0 n)
     (steps_sum num_laters_per_step 0 n)).
   iIntros (Hinv) "Hcred".
   iMod Hwp as (stateI Φ fork_post state_interp_mono) "(Hσ & Hwp & Hφ)".
diff --git a/iris/program_logic/total_adequacy.v b/iris/program_logic/total_adequacy.v
index 6e295a130..64e52d0fa 100644
--- a/iris/program_logic/total_adequacy.v
+++ b/iris/program_logic/total_adequacy.v
@@ -134,7 +134,7 @@ Theorem twp_total Σ Λ `{!invGpreS Σ} s e σ Φ n :
   sn erased_step ([e], σ). (* i.e. ([e], σ) is strongly normalizing *)
 Proof.
   intros Hwp. apply (soundness (M:=iResUR Σ) _  1); simpl.
-  apply (fupd_plain_soundness_no_lc ⊤ ⊤ _ 0)=> Hinv. iIntros "_".
+  apply (fupd_soundness_no_lc ⊤ ⊤ _ 0)=> Hinv. iIntros "_".
   iMod (Hwp) as (stateI num_laters_per_step fork_post stateI_mono) "[Hσ H]".
   set (iG := IrisG Hinv stateI fork_post num_laters_per_step stateI_mono).
   iApply (@twptp_total _ _ iG _ n with "Hσ").
-- 
GitLab