From 2e07f00333a9babb55bcbd2913537aaaa99a2b6b Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 17 Dec 2021 15:44:24 +0100
Subject: [PATCH] rename the new dfrac_agree update lemmas for consistency

---
 iris/algebra/lib/dfrac_agree.v  | 8 ++++----
 iris/base_logic/lib/ghost_var.v | 2 +-
 2 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/iris/algebra/lib/dfrac_agree.v b/iris/algebra/lib/dfrac_agree.v
index 693287c55..8bd125b3c 100644
--- a/iris/algebra/lib/dfrac_agree.v
+++ b/iris/algebra/lib/dfrac_agree.v
@@ -101,7 +101,7 @@ Section lemmas.
   (** While [cmra_update_exclusive] takes care of most updates, it is not sufficient
       for this one since there is no abstraction-preserving way to rewrite
       [to_dfrac_agree d1 v1 â‹… to_dfrac_agree d2 v2] into something simpler. *)
-  Lemma to_dfrac_agree_update_2 d1 d2 a1 a2 a' :
+  Lemma dfrac_agree_update_2 d1 d2 a1 a2 a' :
     d1 ⋅ d2 = DfracOwn 1 →
     to_dfrac_agree d1 a1 â‹… to_dfrac_agree d2 a2 ~~>
     to_dfrac_agree d1 a' â‹… to_dfrac_agree d2 a'.
@@ -110,13 +110,13 @@ Section lemmas.
     apply cmra_update_exclusive.
     rewrite dfrac_agree_op_valid Hq //.
   Qed.
-  Lemma to_frac_agree_update_2 q1 q2 a1 a2 a' :
+  Lemma frac_agree_update_2 q1 q2 a1 a2 a' :
     (q1 + q2 = 1)%Qp →
     to_frac_agree q1 a1 â‹… to_frac_agree q2 a2 ~~>
     to_frac_agree q1 a' â‹… to_frac_agree q2 a'.
-  Proof. intros Hq. apply to_dfrac_agree_update_2. rewrite dfrac_op_own Hq //. Qed.
+  Proof. intros Hq. apply dfrac_agree_update_2. rewrite dfrac_op_own Hq //. Qed.
 
-  Lemma to_dfrac_agree_persist d a :
+  Lemma dfrac_agree_persist d a :
     to_dfrac_agree d a ~~> to_dfrac_agree DfracDiscarded a.
   Proof.
     rewrite /to_dfrac_agree. apply prod_update; last done.
diff --git a/iris/base_logic/lib/ghost_var.v b/iris/base_logic/lib/ghost_var.v
index 46a0fd5f1..625634567 100644
--- a/iris/base_logic/lib/ghost_var.v
+++ b/iris/base_logic/lib/ghost_var.v
@@ -79,7 +79,7 @@ Section lemmas.
     ghost_var γ q1 a1 -∗ ghost_var γ q2 a2 ==∗ ghost_var γ q1 b ∗ ghost_var γ q2 b.
   Proof.
     intros Hq. unseal. rewrite -own_op. iApply own_update_2.
-    apply to_frac_agree_update_2. done.
+    apply frac_agree_update_2. done.
   Qed.
   Lemma ghost_var_update_halves b γ a1 a2 :
     ghost_var γ (1/2) a1 -∗
-- 
GitLab