rename `agree_op_{inv,invL}'` to `to_agree_op_{inv,invL}`

CHANGELOG.md

@@ -5,6 +5,11 @@ lemma.
 
 ## Iris master
 
+**Changes in `algebra`:**
+
+* Rename `agree_op_{inv,invL}'` to `to_agree_op_{inv,invL}`, and add
+  `to_agree_op_invN`.
+
 **Changes in `proofmode`:**
 
 * The proofmode now preserves user-supplied names for existentials when using

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 %?%agree_op_invL'; subst.
+    iDestruct (own_valid_2 with "Hγ Hγ'") as %?%to_agree_op_invL; subst.
     iModIntro. iSplitL "Hl".
     { iNext; iRight; by eauto. }
     wp_apply wp_assert. wp_pures. by case_bool_decide.

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 %?%agree_op_invL'; subst.
+      iDestruct (own_valid_2 with "Hγ Hγ'") as %?%to_agree_op_invL; subst.
       iModIntro. iSplitL "Hl Hγ"; first by eauto with iFrame.
       wp_pures. iApply wp_assert. wp_op. by case_bool_decide.
 Qed.

theories/algebra/agree.v

@@ -237,10 +237,12 @@ Lemma agree_op_inv x y : ✓ (x ⋅ y) → x ≡ y.
 Proof.
   intros ?. apply equiv_dist=>n. by apply agree_op_invN, cmra_valid_validN.
 Qed.
-Lemma agree_op_inv' a b : ✓ (to_agree a ⋅ to_agree b) → a ≡ b.
+Lemma to_agree_op_invN a b n : ✓{n} (to_agree a ⋅ to_agree b) → a ≡{n}≡ b.
+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 agree_op_invL' `{!LeibnizEquiv A} a b : ✓ (to_agree a ⋅ to_agree b) → a = b.
-Proof. by intros ?%agree_op_inv'%leibniz_equiv. Qed.
+Lemma to_agree_op_invL `{!LeibnizEquiv A} a b : ✓ (to_agree a ⋅ to_agree b) → a = b.
+Proof. by intros ?%to_agree_op_inv%leibniz_equiv. Qed.
 
 (** Internalized properties *)
 Lemma agree_equivI {M} a b : to_agree a ≡ to_agree b ⊣⊢@{uPredI M} (a ≡ 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 [_ ?%agree_op_invL'].
+    by intros [_ ?%to_agree_op_invL].
   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: agree_op_invL'. }
+      rewrite singleton_valid. apply: to_agree_op_invL. }
     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: agree_op_invL'. }
+      rewrite singleton_valid. apply: to_agree_op_invL. }
     iDestruct (own_valid_2 with "Hm1 Hm2") as %Hγ; iPureIntro.
     move: Hγ. rewrite -namespace_map_data_op namespace_map_data_valid.
-    move=> /agree_op_invL'. naive_solver.
+    move=> /to_agree_op_invL. naive_solver.
   Qed.
   Lemma meta_set `{Countable A} E l (x : A) N :
     ↑ N ⊆ E → meta_token l E ==∗ meta l N x.