relate size of map to size of its domain

theories/fin_map_dom.v

@@ -165,6 +165,23 @@ Proof.
   - simpl. by rewrite dom_insert, IH.
 Qed.
 
+(** Alternative definition of [dom] in terms of [map_to_list]. *)
+Lemma dom_alt {A} (m : M A) :
+  dom D m ≡ list_to_set (map_to_list m).*1.
+Proof.
+  rewrite <-(list_to_map_to_list m) at 1.
+  rewrite dom_list_to_map.
+  done.
+Qed.
+
+Lemma size_dom `{!Elements K D, !FinSet K D} {A} (m : M A) :
+  size (dom D m) = size m.
+Proof.
+  rewrite dom_alt, list_to_set_size.
+  2:{ apply NoDup_fst_map_to_list. }
+  unfold size, map_size. rewrite fmap_length. done.
+Qed.
+
 Lemma dom_singleton_inv {A} (m : M A) i :
   dom D m ≡ {[i]} → ∃ x, m = {[i := x]}.
 Proof.

theories/fin_sets.v

@@ -119,6 +119,15 @@ Proof. intros ?. rewrite elem_of_list_to_set. apply elem_of_elements. Qed.
 Lemma list_to_set_elements_L `{!LeibnizEquiv C} X : list_to_set (elements X) = X.
 Proof. unfold_leibniz. apply list_to_set_elements. Qed.
 
+Lemma elements_list_to_set l :
+  NoDup l → elements (list_to_set (C:=C) l) ≡ₚ l.
+Proof.
+  intros Hl. induction Hl.
+  { rewrite list_to_set_nil. rewrite elements_empty. done. }
+  rewrite list_to_set_cons, elements_disj_union by set_solver.
+  rewrite elements_singleton. apply Permutation_skip. done.
+Qed.
+
 (** * The [size] operation *)
 Global Instance set_size_proper: Proper ((≡) ==> (=)) (@size C _).
 Proof. intros ?? E. apply Permutation_length. by rewrite E. Qed.
@@ -194,6 +203,13 @@ Proof.
   by apply size_non_empty_iff, non_empty_difference.
 Qed.
 
+Lemma list_to_set_size l :
+  NoDup l → size (list_to_set (C:=C) l) = length l.
+Proof.
+  intros Hl. unfold size, set_size. simpl.
+  rewrite elements_list_to_set; done.
+Qed.
+
 (** * Induction principles *)
 Lemma set_wf : wf (⊂@{C}).
 Proof. apply (wf_projected (<) size); auto using subset_size, lt_wf. Qed.