Rename `cmra_opM_assoc` → `cmra_op_opM_assoc` and `cmra_opM_assoc'` → `cmra_opM_opM_assoc`.

Thanks to @jung for proposing these names.

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)

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.

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) :

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.