Provide "lookup" and commuting lemmas as equations that always apply, and fix some inconsistent lemma naming

!507 (closed) ballooned into this huge change. This contains the following two MRs:

• !526 (merged)
• !531 (merged)

There is more that could be done, but that is postponed (we should probably open an issue):

• non_empty change as discussed in !526 (comment 97794)
• Direction of equality in fmap/omap/alter lemmas, see !531 (comment 97789)

stdpp/gmultiset.v

@@ -88,15 +88,15 @@ Section basic_lemmas.
   (* Multiplicity *)
   Lemma multiplicity_empty x : multiplicity x ∅ = 0.
   Proof. done. Qed.
-  Lemma multiplicity_singleton x : multiplicity x {[+ x +]} = 1.
-  Proof. unfold multiplicity; simpl. by rewrite lookup_singleton. Qed.
+  Lemma multiplicity_singleton_eq x : multiplicity x {[+ x +]} = 1.
+  Proof. unfold multiplicity; simpl. by rewrite lookup_singleton_eq. Qed.
   Lemma multiplicity_singleton_ne x y : x ≠ y → multiplicity x {[+ y +]} = 0.
   Proof. intros. unfold multiplicity; simpl. by rewrite lookup_singleton_ne. Qed.
-  Lemma multiplicity_singleton' x y :
+  Lemma multiplicity_singleton x y :
     multiplicity x {[+ y +]} = if decide (x = y) then 1 else 0.
   Proof.
     destruct (decide _) as [->|].
-    - by rewrite multiplicity_singleton.
+    - by rewrite multiplicity_singleton_eq.
     - by rewrite multiplicity_singleton_ne.
   Qed.
   Lemma multiplicity_union X Y x :
@@ -138,7 +138,7 @@ Section basic_lemmas.
   Proof. rewrite elem_of_multiplicity, multiplicity_empty. lia. Qed.
   Lemma gmultiset_elem_of_singleton x y : x ∈@{gmultiset A} {[+ y +]} ↔ x = y.
   Proof.
-    rewrite elem_of_multiplicity, multiplicity_singleton'.
+    rewrite elem_of_multiplicity, multiplicity_singleton.
     case_decide; naive_solver lia.
   Qed.
   Lemma gmultiset_elem_of_union X Y x : x ∈ X ∪ Y ↔ x ∈ X ∨ x ∈ Y.
@@ -212,7 +212,7 @@ Section multiset_unfold.
   Proof. constructor. by rewrite multiplicity_empty. Qed.
   Global Instance multiset_unfold_singleton x :
     MultisetUnfold x {[+ x +]} 1.
-  Proof. constructor. by rewrite multiplicity_singleton. Qed.
+  Proof. constructor. by rewrite multiplicity_singleton_eq. Qed.
   Global Instance multiset_unfold_union x X Y n m :
     MultisetUnfold x X n → MultisetUnfold x Y m →
     MultisetUnfold x (X ∪ Y) (n `max` m).
@@ -318,25 +318,27 @@ Ltac multiset_instantiate :=
 to ensure we do not use the lemma if it leads to information loss. *)
 Local Lemma multiplicity_singleton_forget `{Countable A} x y :
   ∃ n, multiplicity (A:=A) x {[+ y +]} = n ∧ n ≤ 1.
-Proof. rewrite multiplicity_singleton'. case_decide; eauto with lia. Qed.
+Proof. rewrite multiplicity_singleton. case_decide; eauto with lia. Qed.
 
 Ltac multiset_simplify_singletons :=
   repeat match goal with
   | H : context [multiplicity ?x {[+ ?y +]}] |- _ =>
      first
-       [progress rewrite ?multiplicity_singleton ?multiplicity_singleton_ne in H; [|done..]
+       [progress rewrite ?multiplicity_singleton_eq
+                         ?multiplicity_singleton_ne in H; [|done..]
        (* This second case does *not* use ssreflect matching (due to [destruct]
        and the [->] pattern). If the default Coq matching goes wrong it will
        fail and fall back to the third case, which is strictly more general,
        just slower. *)
        |destruct (multiplicity_singleton_forget x y) as (?&->&?); clear y
-       |rewrite multiplicity_singleton' in H; destruct (decide (x = y)); simplify_eq/=]
+       |rewrite multiplicity_singleton in H; destruct (decide (x = y)); simplify_eq/=]
   | |- context [multiplicity ?x {[+ ?y +]}] =>
      first
-       [progress rewrite ?multiplicity_singleton ?multiplicity_singleton_ne; [|done..]
+       [progress rewrite ?multiplicity_singleton_eq
+                         ?multiplicity_singleton_ne; [|done..]
        (* Similar to above, this second case does *not* use ssreflect matching. *)
        |destruct (multiplicity_singleton_forget x y) as (?&->&?); clear y
-       |rewrite multiplicity_singleton'; destruct (decide (x = y)); simplify_eq/=]
+       |rewrite multiplicity_singleton; destruct (decide (x = y)); simplify_eq/=]
   end.
 End tactics.
 
@@ -430,8 +432,7 @@ Section more_lemmas.
   Global Instance gmultiset_singleton_inj : Inj (=) (=@{gmultiset A}) singletonMS.
   Proof.
     intros x1 x2 Hx. rewrite gmultiset_eq in Hx. specialize (Hx x1).
-    rewrite multiplicity_singleton, multiplicity_singleton' in Hx.
-    case_decide; [done|lia].
+    rewrite !multiplicity_singleton in Hx. repeat case_decide; done || lia.
   Qed.
   Lemma gmultiset_non_empty_singleton x : {[+ x +]} ≠@{gmultiset A} ∅.
   Proof. multiset_solver. Qed.
@@ -515,10 +516,10 @@ Section more_lemmas.
     revert Y; induction X as [|x n X HX IH] using map_ind; intros Y.
     { by rewrite (left_id_L _ _ Y), map_to_list_empty. }
     destruct (Y !! x) as [n'|] eqn:HY.
-    - rewrite <-(insert_delete Y x n') by done.
+    - rewrite <-(insert_delete_id Y x n') by done.
       erewrite <-insert_union_with by done.
       rewrite !map_to_list_insert, !bind_cons
-        by (by rewrite ?lookup_union_with, ?lookup_delete, ?HX).
+        by (by rewrite ?lookup_union_with, ?lookup_delete_eq, ?HX).
       rewrite (assoc_L _), <-(comm (++) (f (_,n'))), <-!(assoc_L _), <-IH.
       rewrite (assoc_L _). f_equiv.
       rewrite (comm _); simpl. by rewrite Pos2Nat.inj_add, replicate_add.
@@ -538,7 +539,7 @@ Section more_lemmas.
     destruct X as [X]. unfold elements, gmultiset_elements.
     set (f xn := let '(x, n) := xn in replicate (Pos.to_nat n) x); simpl.
     unfold elem_of at 2, gmultiset_elem_of, multiplicity; simpl.
-    rewrite elem_of_list_bind. split.
+    rewrite list_elem_of_bind. split.
     - intros [[??] [[<- ?]%elem_of_replicate ->%elem_of_map_to_list]]; lia.
     - intros. destruct (X !! x) as [n|] eqn:Hx; [|lia].
       exists (x,n); split; [|by apply elem_of_map_to_list].
@@ -566,7 +567,7 @@ Section more_lemmas.
   Proof.
     intros ? Hf. unfold set_fold; simpl.
     rewrite <-foldr_app. apply (foldr_permutation R f b).
-    - intros j1 a1 j2 a2 c ? Ha1%elem_of_list_lookup_2 Ha2%elem_of_list_lookup_2.
+    - intros j1 a1 j2 a2 c ? Ha1%list_elem_of_lookup_2 Ha2%list_elem_of_lookup_2.
       rewrite gmultiset_elem_of_elements in Ha1, Ha2. eauto.
     - rewrite (comm (++)). apply gmultiset_elements_disj_union.
   Qed.