From 876771dfaa3823d16b0a79756b0d0a31d7d75d2b Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 23 May 2018 10:29:59 +0200
Subject: [PATCH] =?UTF-8?q?Rename=20`cmra=5FopM=5Fassoc`=20=E2=86=92=20`cm?=
 =?UTF-8?q?ra=5Fop=5FopM=5Fassoc`=20and=20`cmra=5FopM=5Fassoc'`=20?=
 =?UTF-8?q?=E2=86=92=20`cmra=5FopM=5FopM=5Fassoc`.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Thanks to @jung for proposing these names.
---
 CHANGELOG.md                     |  3 +++
 theories/algebra/cmra.v          | 14 ++++++++++----
 theories/algebra/local_updates.v |  8 ++++----
 theories/algebra/updates.v       |  8 ++++----
 4 files changed, 21 insertions(+), 12 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index a199aaa80..bcf5ff865 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -24,6 +24,9 @@ Changes in Coq:
   - `IntoLaterNEnvs` → `MaybeIntoLaterNEnvs`
 * Rename:
   - `frag_auth_op` → `frac_auth_frag_op`
+  - `cmra_opM_assoc` → `cmra_op_opM_assoc`
+  - `cmra_opM_assoc_L` → `cmra_op_opM_assoc_L`
+  - `cmra_opM_assoc'` → `cmra_opM_opM_assoc`
 * `namespaces` has been moved to std++.
 
 ## Iris 3.1.0 (released 2017-12-19)
diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index ead978084..b22018df5 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -327,7 +327,7 @@ Global Instance IdFree_proper : Proper ((≡) ==> iff) (@IdFree A).
 Proof. intros x y Hxy. rewrite /IdFree. by setoid_rewrite Hxy. Qed.
 
 (** ** Op *)
-Lemma cmra_opM_assoc x y mz : (x ⋅ y) ⋅? mz ≡ x ⋅ (y ⋅? mz).
+Lemma cmra_op_opM_assoc x y mz : (x ⋅ y) ⋅? mz ≡ x ⋅ (y ⋅? mz).
 Proof. destruct mz; by rewrite /= -?assoc. Qed.
 
 (** ** Validity *)
@@ -662,8 +662,8 @@ Section cmra_leibniz.
   Lemma cmra_pcore_idemp_L x cx : pcore x = Some cx → pcore cx = Some cx.
   Proof. unfold_leibniz. apply cmra_pcore_idemp'. Qed.
 
-  Lemma cmra_opM_assoc_L x y mz : (x â‹… y) â‹…? mz = x â‹… (y â‹…? mz).
-  Proof. unfold_leibniz. apply cmra_opM_assoc. Qed.
+  Lemma cmra_op_opM_assoc_L x y mz : (x â‹… y) â‹…? mz = x â‹… (y â‹…? mz).
+  Proof. unfold_leibniz. apply cmra_op_opM_assoc. Qed.
 
   (** ** Core *)
   Lemma cmra_pcore_r_L x cx : pcore x = Some cx → x ⋅ cx = x.
@@ -1334,8 +1334,14 @@ Section option.
   Lemma op_is_Some ma mb : is_Some (ma ⋅ mb) ↔ is_Some ma ∨ is_Some mb.
   Proof. rewrite -!not_eq_None_Some op_None. destruct ma, mb; naive_solver. Qed.
 
-  Lemma cmra_opM_assoc' a mb mc : a ⋅? mb ⋅? mc ≡ a ⋅? (mb ⋅ mc).
+  Lemma cmra_opM_opM_assoc a mb mc : a ⋅? mb ⋅? mc ≡ a ⋅? (mb ⋅ mc).
   Proof. destruct mb, mc; by rewrite /= -?assoc. Qed.
+  Lemma cmra_opM_opM_assoc_L `{!LeibnizEquiv A} a mb mc : a â‹…? mb â‹…? mc = a â‹…? (mb â‹… mc).
+  Proof. unfold_leibniz. apply cmra_opM_opM_assoc. Qed.
+  Lemma cmra_opM_opM_swap a mb mc : a ⋅? mb ⋅? mc ≡ a ⋅? mc ⋅? mb.
+  Proof. by rewrite !cmra_opM_opM_assoc (comm _ mb). Qed.
+  Lemma cmra_opM_opM_swap_L `{!LeibnizEquiv A} a mb mc : a â‹…? mb â‹…? mc = a â‹…? mc â‹…? mb.
+  Proof. by rewrite !cmra_opM_opM_assoc_L (comm_L _ mb). Qed.
 
   Global Instance Some_core_id a : CoreId a → CoreId (Some a).
   Proof. by constructor. Qed.
diff --git a/theories/algebra/local_updates.v b/theories/algebra/local_updates.v
index 3b4a36ff4..920ae9a31 100644
--- a/theories/algebra/local_updates.v
+++ b/theories/algebra/local_updates.v
@@ -29,7 +29,7 @@ Section updates.
     (∀ n, ✓{n} x → ✓{n} (z ⋅ x)) → (x,y) ~l~> (z ⋅ x, z ⋅ y).
   Proof.
     intros Hv n mz Hxv Hx; simpl in *; split; [by auto|].
-    by rewrite Hx -cmra_opM_assoc.
+    by rewrite Hx -cmra_op_opM_assoc.
   Qed.
   Lemma op_local_update_discrete `{!CmraDiscrete A} x y z :
     (✓ x → ✓ (z ⋅ x)) → (x,y) ~l~> (z ⋅ x, z ⋅ y).
@@ -41,15 +41,15 @@ Section updates.
     (x,y) ~l~> (x',y') → (x,y ⋅ yf) ~l~> (x', y' ⋅ yf).
   Proof.
     intros Hup n mz Hxv Hx; simpl in *.
-    destruct (Hup n (Some (yf â‹…? mz))); [done|by rewrite /= -cmra_opM_assoc|].
-    by rewrite cmra_opM_assoc.
+    destruct (Hup n (Some (yf â‹…? mz))); [done|by rewrite /= -cmra_op_opM_assoc|].
+    by rewrite cmra_op_opM_assoc.
   Qed.
 
   Lemma cancel_local_update x y z `{!Cancelable x} :
     (x â‹… y, x â‹… z) ~l~> (y, z).
   Proof.
     intros n f ? Heq. split; first by eapply cmra_validN_op_r.
-    apply (cancelableN x); first done. by rewrite -cmra_opM_assoc.
+    apply (cancelableN x); first done. by rewrite -cmra_op_opM_assoc.
   Qed.
 
   Lemma local_update_discrete `{!CmraDiscrete A} (x y x' y' : A) :
diff --git a/theories/algebra/updates.v b/theories/algebra/updates.v
index 372130355..e9570d8ef 100644
--- a/theories/algebra/updates.v
+++ b/theories/algebra/updates.v
@@ -64,10 +64,10 @@ Lemma cmra_updateP_op (P1 P2 Q : A → Prop) x1 x2 :
 Proof.
   intros Hx1 Hx2 Hy n mz ?.
   destruct (Hx1 n (Some (x2 â‹…? mz))) as (y1&?&?).
-  { by rewrite /= -cmra_opM_assoc. }
+  { by rewrite /= -cmra_op_opM_assoc. }
   destruct (Hx2 n (Some (y1 â‹…? mz))) as (y2&?&?).
-  { by rewrite /= -cmra_opM_assoc (comm _ x2) cmra_opM_assoc. }
-  exists (y1 â‹… y2); split; last rewrite (comm _ y1) cmra_opM_assoc; auto.
+  { by rewrite /= -cmra_op_opM_assoc (comm _ x2) cmra_op_opM_assoc. }
+  exists (y1 â‹… y2); split; last rewrite (comm _ y1) cmra_op_opM_assoc; auto.
 Qed.
 Lemma cmra_updateP_op' (P1 P2 : A → Prop) x1 x2 :
   x1 ~~>: P1 → x2 ~~>: P2 →
@@ -79,7 +79,7 @@ Proof.
 Qed.
 
 Lemma cmra_update_op_l x y : x â‹… y ~~> x.
-Proof. intros n mz. rewrite comm cmra_opM_assoc. apply cmra_validN_op_r. Qed.
+Proof. intros n mz. rewrite comm cmra_op_opM_assoc. apply cmra_validN_op_r. Qed.
 Lemma cmra_update_op_r x y : x â‹… y ~~> y.
 Proof. rewrite comm. apply cmra_update_op_l. Qed.
 
-- 
GitLab