Add lemmas about list_to_map

theories/fin_map_dom.v

@@ -156,6 +156,13 @@ Proof.
   intros m1 m2 EQm. apply elem_of_equiv. intros i.
   rewrite !elem_of_dom, EQm. done.
 Qed.
+Lemma dom_list_to_map {A : Type} (l : list (K * A)) :
+  dom D (list_to_map l : M A) ≡ list_to_set l.*1.
+Proof.
+  induction l as [|?? IH].
+  - by rewrite dom_empty.
+  - simpl. by rewrite dom_insert, IH.
+Qed.
 (** If [D] has Leibniz equality, we can show an even stronger result.  This is a
 common case e.g. when having a [gmap K A] where the key [K] has Leibniz equality
 (and thus also [gset K], the usual domain) but the value type [A] does not. *)
@@ -197,6 +204,9 @@ Section leibniz.
     (∀ i, i ∈ X ↔ ∃ x, m !! i = Some x ∧ is_Some (f i x)) →
     dom D (map_imap f m) = X.
   Proof. unfold_leibniz; apply dom_imap. Qed.
+  Lemma dom_list_to_map_L {A : Type} (l : list (K * A)) :
+    dom D (list_to_map l : M A) = list_to_set l.*1.
+  Proof. unfold_leibniz. apply dom_list_to_map. Qed.
 End leibniz.
 
 (** * Set solver instances *)

theories/fin_maps.v

@@ -838,6 +838,15 @@ Proof. done. Qed.
 Lemma list_to_map_cons {A} (l : list (K * A)) i x :
   list_to_map ((i, x) :: l) = <[i:=x]>(list_to_map l : M A).
 Proof. done. Qed.
+Lemma list_to_map_snoc {A} (l : list (K * A)) i x :
+  i ∉ l.*1 → list_to_map (l ++ [(i, x)]) = <[i:=x]>(list_to_map l : M A).
+Proof.
+  induction l as [|[k y] l IH]; [done|].
+  intros [Hneq Hni]%not_elem_of_cons. simpl.
+  rewrite (IH Hni).
+  rewrite insert_commute; [done|].
+  rewrite comm; [apply Hneq|apply _].
+Qed.
 Lemma list_to_map_fmap {A B} (f : A → B) l :
   list_to_map (prod_map id f <$> l) = f <$> (list_to_map l : M A).
 Proof.