From 008e2f3be208983213abb8df115282448b0b3625 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 14 Sep 2020 14:12:34 +0200
Subject: [PATCH] fix '_L' suffix

---
 CHANGELOG.md                       | 6 +++++-
 tests/one_shot.v                   | 2 +-
 tests/one_shot_once.v              | 2 +-
 theories/algebra/agree.v           | 2 +-
 theories/algebra/auth.v            | 2 +-
 theories/algebra/lib/excl_auth.v   | 2 +-
 theories/algebra/lib/frac_auth.v   | 2 +-
 theories/algebra/lib/ufrac_auth.v  | 2 +-
 theories/base_logic/lib/boxes.v    | 2 +-
 theories/base_logic/lib/gen_heap.v | 8 ++++----
 theories/heap_lang/lib/counter.v   | 2 +-
 11 files changed, 18 insertions(+), 14 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 4579eb471..3f5aebcf2 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -7,8 +7,12 @@ lemma.
 
 **Changes in `algebra`:**
 
-* Rename `agree_op_{inv,invL}'` to `to_agree_op_{inv,invL}`, and add
+* Rename `agree_op_{inv,invL}'` to `to_agree_op_{inv,inv_L}`, and add
   `to_agree_op_invN`.
+* Rename `auth_auth_frac_op_invL` to `auth_auth_frac_op_inv_L`,
+  `excl_auth_agreeL` to `excl_auth_agree_L`,
+  `frac_auth_agreeL` to `frac_auth_agree_L`, and
+  `ufrac_auth_agreeL` to `ufrac_auth_agree_L`.
 
 **Changes in `proofmode`:**
 
diff --git a/tests/one_shot.v b/tests/one_shot.v
index 58e1953b2..13b4e05aa 100644
--- a/tests/one_shot.v
+++ b/tests/one_shot.v
@@ -81,7 +81,7 @@ Proof.
     iInv N as "[[Hl >Hγ]|H]"; last iDestruct "H" as (m') "[Hl Hγ]".
     { by iDestruct (own_valid_2 with "Hγ Hγ'") as %?. }
     wp_load. Show.
-    iDestruct (own_valid_2 with "Hγ Hγ'") as %?%to_agree_op_invL; subst.
+    iDestruct (own_valid_2 with "Hγ Hγ'") as %?%to_agree_op_inv_L; subst.
     iModIntro. iSplitL "Hl".
     { iNext; iRight; by eauto. }
     wp_apply wp_assert. wp_pures. by case_bool_decide.
diff --git a/tests/one_shot_once.v b/tests/one_shot_once.v
index f93480ae3..40efb5efc 100644
--- a/tests/one_shot_once.v
+++ b/tests/one_shot_once.v
@@ -99,7 +99,7 @@ Proof.
     + iDestruct "Hinv" as "[[Hl >Hγ]|H]"; last iDestruct "H" as (m') "[Hl Hγ]".
       { by iDestruct (own_valid_2 with "Hγ Hγ'") as %?. }
       wp_load. Show.
-      iDestruct (own_valid_2 with "Hγ Hγ'") as %?%to_agree_op_invL; subst.
+      iDestruct (own_valid_2 with "Hγ Hγ'") as %?%to_agree_op_inv_L; subst.
       iModIntro. iSplitL "Hl Hγ"; first by eauto with iFrame.
       wp_pures. iApply wp_assert. wp_op. by case_bool_decide.
 Qed.
diff --git a/theories/algebra/agree.v b/theories/algebra/agree.v
index e3d0baf4f..7ace47cea 100644
--- a/theories/algebra/agree.v
+++ b/theories/algebra/agree.v
@@ -241,7 +241,7 @@ Lemma to_agree_op_invN a b n : ✓{n} (to_agree a ⋅ to_agree b) → a ≡{n}
 Proof. by intros ?%agree_op_invN%(inj to_agree). Qed.
 Lemma to_agree_op_inv a b : ✓ (to_agree a ⋅ to_agree b) → a ≡ b.
 Proof. by intros ?%agree_op_inv%(inj to_agree). Qed.
-Lemma to_agree_op_invL `{!LeibnizEquiv A} a b : ✓ (to_agree a ⋅ to_agree b) → a = b.
+Lemma to_agree_op_inv_L `{!LeibnizEquiv A} a b : ✓ (to_agree a ⋅ to_agree b) → a = b.
 Proof. by intros ?%to_agree_op_inv%leibniz_equiv. Qed.
 
 (** Internalized properties *)
diff --git a/theories/algebra/auth.v b/theories/algebra/auth.v
index 6df092d8c..d8f9fbbe8 100644
--- a/theories/algebra/auth.v
+++ b/theories/algebra/auth.v
@@ -329,7 +329,7 @@ Proof.
   intros ?. apply equiv_dist. intros n.
   by eapply auth_auth_frac_op_invN, cmra_valid_validN.
 Qed.
-Lemma auth_auth_frac_op_invL `{!LeibnizEquiv A} q a p b :
+Lemma auth_auth_frac_op_inv_L `{!LeibnizEquiv A} q a p b :
   ✓ (●{p} a ⋅ ●{q} b) → a = b.
 Proof. by intros ?%auth_auth_frac_op_inv%leibniz_equiv. Qed.
 
diff --git a/theories/algebra/lib/excl_auth.v b/theories/algebra/lib/excl_auth.v
index 9a0866583..c66266846 100644
--- a/theories/algebra/lib/excl_auth.v
+++ b/theories/algebra/lib/excl_auth.v
@@ -57,7 +57,7 @@ Section excl_auth.
   Proof.
     intros. apply equiv_dist=> n. by apply excl_auth_agreeN, cmra_valid_validN.
   Qed.
-  Lemma excl_auth_agreeL `{!LeibnizEquiv A} a b : ✓ (●E a ⋅ ◯E b) → a = b.
+  Lemma excl_auth_agree_L `{!LeibnizEquiv A} a b : ✓ (●E a ⋅ ◯E b) → a = b.
   Proof. intros. by apply leibniz_equiv, excl_auth_agree. Qed.
 
   Lemma excl_auth_agreeI {M} a b : ✓ (●E a ⋅ ◯E b) ⊢@{uPredI M} (a ≡ b).
diff --git a/theories/algebra/lib/frac_auth.v b/theories/algebra/lib/frac_auth.v
index 14cc4b58b..9fbdca93f 100644
--- a/theories/algebra/lib/frac_auth.v
+++ b/theories/algebra/lib/frac_auth.v
@@ -60,7 +60,7 @@ Section frac_auth.
   Proof.
     intros. apply equiv_dist=> n. by apply frac_auth_agreeN, cmra_valid_validN.
   Qed.
-  Lemma frac_auth_agreeL `{!LeibnizEquiv A} a b : ✓ (●F a ⋅ ◯F b) → a = b.
+  Lemma frac_auth_agree_L `{!LeibnizEquiv A} a b : ✓ (●F a ⋅ ◯F b) → a = b.
   Proof. intros. by apply leibniz_equiv, frac_auth_agree. Qed.
 
   Lemma frac_auth_includedN n q a b : ✓{n} (●F a ⋅ ◯F{q} b) → Some b ≼{n} Some a.
diff --git a/theories/algebra/lib/ufrac_auth.v b/theories/algebra/lib/ufrac_auth.v
index 9020deebf..c8423c36c 100644
--- a/theories/algebra/lib/ufrac_auth.v
+++ b/theories/algebra/lib/ufrac_auth.v
@@ -80,7 +80,7 @@ Section ufrac_auth.
   Proof.
     intros. apply equiv_dist=> n. by eapply ufrac_auth_agreeN, cmra_valid_validN.
   Qed.
-  Lemma ufrac_auth_agreeL `{!LeibnizEquiv A} p a b : ✓ (●U{p} a ⋅ ◯U{p} b) → a = b.
+  Lemma ufrac_auth_agree_L `{!LeibnizEquiv A} p a b : ✓ (●U{p} a ⋅ ◯U{p} b) → a = b.
   Proof. intros. by eapply leibniz_equiv, ufrac_auth_agree. Qed.
 
   Lemma ufrac_auth_includedN n p q a b : ✓{n} (●U{p} a ⋅ ◯U{q} b) → Some b ≼{n} Some a.
diff --git a/theories/base_logic/lib/boxes.v b/theories/base_logic/lib/boxes.v
index a02be5297..3af37d7be 100644
--- a/theories/base_logic/lib/boxes.v
+++ b/theories/base_logic/lib/boxes.v
@@ -78,7 +78,7 @@ Lemma box_own_auth_agree γ b1 b2 :
   box_own_auth γ (●E b1) ∗ box_own_auth γ (◯E b2) ⊢ ⌜b1 = b2⌝.
 Proof.
   rewrite /box_own_prop -own_op own_valid prod_validI /= and_elim_l.
-  by iDestruct 1 as %?%excl_auth_agreeL.
+  by iDestruct 1 as %?%excl_auth_agree_L.
 Qed.
 
 Lemma box_own_auth_update γ b1 b2 b3 :
diff --git a/theories/base_logic/lib/gen_heap.v b/theories/base_logic/lib/gen_heap.v
index 7a4b7e544..8504c9296 100644
--- a/theories/base_logic/lib/gen_heap.v
+++ b/theories/base_logic/lib/gen_heap.v
@@ -202,7 +202,7 @@ Section gen_heap.
     apply wand_intro_r.
     rewrite mapsto_eq /mapsto_def -own_op -auth_frag_op own_valid discrete_valid.
     f_equiv. rewrite auth_frag_valid singleton_op singleton_valid -pair_op.
-    by intros [_ ?%to_agree_op_invL].
+    by intros [_ ?%to_agree_op_inv_L].
   Qed.
 
   Lemma mapsto_combine l q1 q2 v1 v2 :
@@ -264,7 +264,7 @@ Section gen_heap.
     iAssert ⌜ γm1 = γm2 ⌝%I as %->.
     { iDestruct (own_valid_2 with "Hγm1 Hγm2") as %Hγ; iPureIntro.
       move: Hγ. rewrite -auth_frag_op singleton_op=> /auth_frag_valid /=.
-      rewrite singleton_valid. apply: to_agree_op_invL. }
+      rewrite singleton_valid. apply: to_agree_op_inv_L. }
     iDestruct (own_valid_2 with "Hm1 Hm2") as %?%namespace_map_token_valid_op.
     iExists γm2. iFrame "Hγm2". rewrite namespace_map_token_union //. by iSplitL "Hm1".
   Qed.
@@ -290,10 +290,10 @@ Section gen_heap.
     iAssert ⌜ γm1 = γm2 ⌝%I as %->.
     { iDestruct (own_valid_2 with "Hγm1 Hγm2") as %Hγ; iPureIntro.
       move: Hγ. rewrite -auth_frag_op singleton_op=> /auth_frag_valid /=.
-      rewrite singleton_valid. apply: to_agree_op_invL. }
+      rewrite singleton_valid. apply: to_agree_op_inv_L. }
     iDestruct (own_valid_2 with "Hm1 Hm2") as %Hγ; iPureIntro.
     move: Hγ. rewrite -namespace_map_data_op namespace_map_data_valid.
-    move=> /to_agree_op_invL. naive_solver.
+    move=> /to_agree_op_inv_L. naive_solver.
   Qed.
   Lemma meta_set `{Countable A} E l (x : A) N :
     ↑ N ⊆ E → meta_token l E ==∗ meta l N x.
diff --git a/theories/heap_lang/lib/counter.v b/theories/heap_lang/lib/counter.v
index 0cc86cfab..f79e35315 100644
--- a/theories/heap_lang/lib/counter.v
+++ b/theories/heap_lang/lib/counter.v
@@ -159,7 +159,7 @@ Section contrib_spec.
   Proof.
     iIntros (Φ) "[#? Hγf] HΦ".
     rewrite /read /=. wp_lam. iInv N as (c) ">[Hγ Hl]". wp_load.
-    iDestruct (own_valid_2 with "Hγ Hγf") as % <-%frac_auth_agreeL.
+    iDestruct (own_valid_2 with "Hγ Hγf") as % <-%frac_auth_agree_L.
     iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
     by iApply "HΦ".
   Qed.
-- 
GitLab