rename more _op and _core lemmas now that those names are available

CHANGELOG.md

@@ -74,8 +74,11 @@ HeapLang, which is now in a separate package `coq-iris-heap-lang`.
   `PCore`, `Valid`, `ValidN`, `Unit`) to have a `_instance` suffix, so that
   their original names are available to use as lemma names.
 * Rename `frac_valid'`→`frac_valid`, `frac_op'`→`frac_op`,
-  `ufrac_op'`→`ufrac_op`. Those names were previously blocked by typeclass
-  instances.
+  `ufrac_op'`→`ufrac_op`, `coPset_op_union` → `coPset_op`, `coPset_core_self` →
+  `coPset_core`, `gset_op_union` → `gset_op`, `gset_core_self` → `gset_core`,
+  `gmultiset_op_disj_union` → `gmultiset_op`, `gmultiset_core_empty` →
+  `gmultiset_core`, `nat_op_plus` → `nat_op`, `max_nat_op_max` →
+  `max_nat_op`. Those names were previously blocked by typeclass instances.
 
 **Changes in `bi`:**
 
@@ -256,8 +259,14 @@ s/\bcmraT\b/cmra/g
 s/\bCmraT\b/Cmra/g
 s/\bucmraT\b/ucmra/g
 s/\bUcmraT\b/Ucmra/g
-# u?frac_op/valid lemmas
+# _op/valid/core lemmas
 s/\b(u?frac_(op|valid))'/\1/g
+s/\b((coPset|gset)_op)_union\b/\1/g
+s/\b((coPset|gset)_core)_self\b/\1/g
+s/\b(gmultiset_op)_disj_union\b/\1/g
+s/\b(gmultiset_core)_empty\b/\1/g
+s/\b(nat_op)_plus\b/\1/g
+s/\b(max_nat_op)_max\b/\1/g
 EOF
 ```
 

iris/algebra/coPset.v

@@ -16,14 +16,14 @@ Section coPset.
   Local Instance coPset_op_instance : Op coPset := union.
   Local Instance coPset_pcore_instance : PCore coPset := Some.
 
-  Lemma coPset_op_union X Y : X ⋅ Y = X ∪ Y.
+  Lemma coPset_op X Y : X ⋅ Y = X ∪ Y.
   Proof. done. Qed.
-  Lemma coPset_core_self X : core X = X.
+  Lemma coPset_core X : core X = X.
   Proof. done. Qed.
   Lemma coPset_included X Y : X ≼ Y ↔ X ⊆ Y.
   Proof.
     split.
-    - intros [Z ->]. rewrite coPset_op_union. set_solver.
+    - intros [Z ->]. rewrite coPset_op. set_solver.
     - intros (Z&->&?)%subseteq_disjoint_union_L. by exists Z.
   Qed.
 
@@ -33,9 +33,9 @@ Section coPset.
     - solve_proper.
     - solve_proper.
     - solve_proper.
-    - intros X1 X2 X3. by rewrite !coPset_op_union assoc_L.
-    - intros X1 X2. by rewrite !coPset_op_union comm_L.
-    - intros X. by rewrite coPset_core_self idemp_L.
+    - intros X1 X2 X3. by rewrite !coPset_op assoc_L.
+    - intros X1 X2. by rewrite !coPset_op comm_L.
+    - intros X. by rewrite coPset_core idemp_L.
   Qed.
   Canonical Structure coPsetR := discreteR coPset coPset_ra_mixin.
 
@@ -43,7 +43,7 @@ Section coPset.
   Proof. apply discrete_cmra_discrete. Qed.
 
   Lemma coPset_ucmra_mixin : UcmraMixin coPset.
-  Proof. split; [done | | done]. intros X. by rewrite coPset_op_union left_id_L. Qed.
+  Proof. split; [done | | done]. intros X. by rewrite coPset_op left_id_L. Qed.
   Canonical Structure coPsetUR := Ucmra coPset coPset_ucmra_mixin.
 
   Lemma coPset_opM X mY : X ⋅? mY = X ∪ default ∅ mY.
@@ -56,7 +56,7 @@ Section coPset.
   Proof.
     intros (Z&->&?)%subseteq_disjoint_union_L.
     rewrite local_update_unital_discrete=> Z' _ /leibniz_equiv_iff->.
-    split; first done. rewrite coPset_op_union. set_solver.
+    split; first done. rewrite coPset_op. set_solver.
   Qed.
 End coPset.
 

iris/algebra/gmap.v

@@ -147,6 +147,8 @@ Local Instance gmap_pcore_instance : PCore (gmap K A) := λ m, Some (omap pcore
 Local Instance gmap_valid_instance : Valid (gmap K A) := λ m, ∀ i, ✓ (m !! i).
 Local Instance gmap_validN_instance : ValidN (gmap K A) := λ n m, ∀ i, ✓{n} (m !! i).
 
+Lemma gmap_op m1 m2 : m1 ⋅ m2 = merge op m1 m2.
+Proof. done. Qed.
 Lemma lookup_op m1 m2 i : (m1 ⋅ m2) !! i = m1 !! i ⋅ m2 !! i.
 Proof. by apply lookup_merge. Qed.
 Lemma lookup_core m i : core m !! i = core (m !! i).

iris/algebra/gmultiset.v

@@ -16,15 +16,15 @@ Section gmultiset.
   Local Instance gmultiset_op_instance : Op (gmultiset K) := disj_union.
   Local Instance gmultiset_pcore_instance : PCore (gmultiset K) := λ X, Some ∅.
 
-  Lemma gmultiset_op_disj_union X Y : X ⋅ Y = X ⊎ Y.
+  Lemma gmultiset_op X Y : X ⋅ Y = X ⊎ Y.
   Proof. done. Qed.
-  Lemma gmultiset_core_empty X : core X = ∅.
+  Lemma gmultiset_core X : core X = ∅.
   Proof. done. Qed.
   Lemma gmultiset_included X Y : X ≼ Y ↔ X ⊆ Y.
   Proof.
     split.
     - intros [Z ->%leibniz_equiv].
-      rewrite gmultiset_op_disj_union. apply gmultiset_disj_union_subseteq_l.
+      rewrite gmultiset_op. apply gmultiset_disj_union_subseteq_l.
     - intros ->%gmultiset_disj_union_difference. by exists (Y ∖ X).
   Qed.
 
@@ -34,10 +34,10 @@ Section gmultiset.
     - by intros X Y Z ->%leibniz_equiv.
     - by intros X Y ->%leibniz_equiv.
     - solve_proper.
-    - intros X1 X2 X3. by rewrite !gmultiset_op_disj_union assoc_L.
-    - intros X1 X2. by rewrite !gmultiset_op_disj_union comm_L.
-    - intros X. by rewrite gmultiset_core_empty left_id.
-    - intros X1 X2 HX. rewrite !gmultiset_core_empty. exists ∅.
+    - intros X1 X2 X3. by rewrite !gmultiset_op assoc_L.
+    - intros X1 X2. by rewrite !gmultiset_op comm_L.
+    - intros X. by rewrite gmultiset_core left_id.
+    - intros X1 X2 HX. rewrite !gmultiset_core. exists ∅.
       by rewrite left_id.
   Qed.
 
@@ -49,7 +49,7 @@ Section gmultiset.
   Lemma gmultiset_ucmra_mixin : UcmraMixin (gmultiset K).
   Proof.
     split; [done | | done]. intros X.
-    by rewrite gmultiset_op_disj_union left_id_L.
+    by rewrite gmultiset_op left_id_L.
   Qed.
   Canonical Structure gmultisetUR := Ucmra (gmultiset K) gmultiset_ucmra_mixin.
 
@@ -68,7 +68,7 @@ Section gmultiset.
   Proof.
     intros HXY. rewrite local_update_unital_discrete=> Z' _. intros ->%leibniz_equiv.
     split; first done. apply leibniz_equiv_iff, (inj (.⊎ Y)).
-    rewrite -HXY !gmultiset_op_disj_union.
+    rewrite -HXY !gmultiset_op.
     by rewrite -(comm_L _ Y) (comm_L _ Y') assoc_L.
   Qed.
 

iris/algebra/gset.v

@@ -15,21 +15,21 @@ Section gset.
   Local Instance gset_op_instance : Op (gset K) := union.
   Local Instance gset_pcore_instance : PCore (gset K) := λ X, Some X.
 
-  Lemma gset_op_union X Y : X ⋅ Y = X ∪ Y.
+  Lemma gset_op X Y : X ⋅ Y = X ∪ Y.
   Proof. done. Qed.
-  Lemma gset_core_self X : core X = X.
+  Lemma gset_core X : core X = X.
   Proof. done. Qed.
   Lemma gset_included X Y : X ≼ Y ↔ X ⊆ Y.
   Proof.
     split.
-    - intros [Z ->]. rewrite gset_op_union. set_solver.
+    - intros [Z ->]. rewrite gset_op. set_solver.
     - intros (Z&->&?)%subseteq_disjoint_union_L. by exists Z.
   Qed.
 
   Lemma gset_ra_mixin : RAMixin (gset K).
   Proof.
     apply ra_total_mixin; apply _ || eauto; [].
-    intros X. by rewrite gset_core_self idemp_L.
+    intros X. by rewrite gset_core idemp_L.
   Qed.
   Canonical Structure gsetR := discreteR (gset K) gset_ra_mixin.
 
@@ -37,7 +37,7 @@ Section gset.
   Proof. apply discrete_cmra_discrete. Qed.
 
   Lemma gset_ucmra_mixin : UcmraMixin (gset K).
-  Proof. split; [ done | | done ]. intros X. by rewrite gset_op_union left_id_L. Qed.
+  Proof. split; [ done | | done ]. intros X. by rewrite gset_op left_id_L. Qed.
   Canonical Structure gsetUR := Ucmra (gset K) gset_ucmra_mixin.
 
   Lemma gset_opM X mY : X ⋅? mY = X ∪ default ∅ mY.
@@ -50,11 +50,11 @@ Section gset.
   Proof.
     intros (Z&->&?)%subseteq_disjoint_union_L.
     rewrite local_update_unital_discrete=> Z' _ /leibniz_equiv_iff->.
-    split; [done|]. rewrite gset_op_union. set_solver.
+    split; [done|]. rewrite gset_op. set_solver.
   Qed.
 
   Global Instance gset_core_id X : CoreId X.
-  Proof. by apply core_id_total; rewrite gset_core_self. Qed.
+  Proof. by apply core_id_total; rewrite gset_core. Qed.
 
   Lemma big_opS_singletons X :
     ([^op set] x ∈ X, {[ x ]}) = X.

iris/algebra/lib/gset_bij.v

@@ -171,7 +171,7 @@ Section gset_bij.
   Lemma gset_bij_elem_agree a1 b1 a2 b2 :
     ✓ (gset_bij_elem a1 b1 ⋅ gset_bij_elem a2 b2) → (a1 = a2 ↔ b1 = b2).
   Proof.
-    rewrite /gset_bij_elem -view_frag_op gset_op_union view_frag_valid.
+    rewrite /gset_bij_elem -view_frag_op gset_op view_frag_valid.
     setoid_rewrite gset_bij_view_rel_iff. intros. apply gset_bijective_pair.
     naive_solver eauto using subseteq_gset_bijective, O.
   Qed.
@@ -188,7 +188,7 @@ Section gset_bij.
     gset_bij_auth 1 L ~~> gset_bij_auth 1 ({[(a, b)]} ∪ L).
   Proof.
     intros. apply view_update=> n bijL.
-    rewrite !gset_bij_view_rel_iff gset_op_union.
+    rewrite !gset_bij_view_rel_iff gset_op.
     set_solver by eauto using gset_bijective_extend.
   Qed.
 End gset_bij.

iris/algebra/lib/mono_nat.v

@@ -33,13 +33,13 @@ Section mono_nat.
 
   Lemma mono_nat_lb_op n1 n2 :
     mono_nat_lb n1 ⋅ mono_nat_lb n2 = mono_nat_lb (n1 `max` n2).
-  Proof. rewrite -auth_frag_op max_nat_op_max //. Qed.
+  Proof. rewrite -auth_frag_op max_nat_op //. Qed.
 
   Lemma mono_nat_auth_lb_op q n :
     mono_nat_auth q n ≡ mono_nat_auth q n ⋅ mono_nat_lb n.
   Proof.
     rewrite /mono_nat_auth /mono_nat_lb.
-    rewrite -!assoc -auth_frag_op max_nat_op_max.
+    rewrite -!assoc -auth_frag_op max_nat_op.
     rewrite Nat.max_id //.
   Qed.
 

iris/algebra/numbers.v

@@ -7,7 +7,7 @@ Section nat.
   Local Instance nat_validN_instance : ValidN nat := λ n x, True.
   Local Instance nat_pcore_instance : PCore nat := λ x, Some 0.
   Local Instance nat_op_instance : Op nat := plus.
-  Definition nat_op_plus x y : x ⋅ y = x + y := eq_refl.
+  Definition nat_op x y : x ⋅ y = x + y := eq_refl.
   Lemma nat_included (x y : nat) : x ≼ y ↔ x ≤ y.
   Proof. by rewrite nat_le_sum. Qed.
   Lemma nat_ra_mixin : RAMixin nat.
@@ -56,7 +56,7 @@ Section max_nat.
   Local Instance max_nat_validN_instance : ValidN max_nat := λ n x, True.
   Local Instance max_nat_pcore_instance : PCore max_nat := Some.
   Local Instance max_nat_op_instance : Op max_nat := λ n m, MaxNat (max_nat_car n `max` max_nat_car m).
-  Definition max_nat_op_max x y : MaxNat x ⋅ MaxNat y = MaxNat (x `max` y) := eq_refl.
+  Definition max_nat_op x y : MaxNat x ⋅ MaxNat y = MaxNat (x `max` y) := eq_refl.
 
   Lemma max_nat_included x y : x ≼ y ↔ max_nat_car x ≤ max_nat_car y.
   Proof.
@@ -67,9 +67,9 @@ Section max_nat.
   Lemma max_nat_ra_mixin : RAMixin max_nat.
   Proof.
     apply ra_total_mixin; apply _ || eauto.
-    - intros [x] [y] [z]. repeat rewrite max_nat_op_max. by rewrite Nat.max_assoc.
-    - intros [x] [y]. by rewrite max_nat_op_max Nat.max_comm.
-    - intros [x]. by rewrite max_nat_op_max Max.max_idempotent.
+    - intros [x] [y] [z]. repeat rewrite max_nat_op. by rewrite Nat.max_assoc.
+    - intros [x] [y]. by rewrite max_nat_op Nat.max_comm.
+    - intros [x]. by rewrite max_nat_op Max.max_idempotent.
   Qed.
   Canonical Structure max_natR : cmra := discreteR max_nat max_nat_ra_mixin.
 
@@ -88,12 +88,12 @@ Section max_nat.
   Proof.
     move: x y x' => [x] [y] [y'] /= ?.
     rewrite local_update_unital_discrete=> [[z]] _.
-    rewrite 2!max_nat_op_max. intros [= ?].
+    rewrite 2!max_nat_op. intros [= ?].
     split; first done. apply f_equal. lia.
   Qed.
 
   Global Instance : IdemP (=@{max_nat}) (⋅).
-  Proof. intros [x]. rewrite max_nat_op_max. apply f_equal. lia. Qed.
+  Proof. intros [x]. rewrite max_nat_op. apply f_equal. lia. Qed.
 
   Global Instance max_nat_is_op (x y : nat) :
     IsOp (MaxNat (x `max` y)) (MaxNat x) (MaxNat y).