Merge branch 'ralf/dom-size' into 'master'

relate size of map to size of its domain

See merge request !320

CHANGELOG.md

@@ -152,7 +152,7 @@ API-breaking change is listed.
   `map_filter_singleton_False`, `map_filter_comm`, `map_union_least`,
   `map_subseteq_difference_l`, `insert_difference`, `insert_difference'`,
   `difference_insert`, `difference_insert_subseteq`. (by Hai Dang)
-- Add `map_size_disj_union`.
+- Add `map_size_disj_union`, `size_dom`, `size_list_to_set`.
 - Tweak reduction on `gset`, so that `cbn` matches the behavior by `simpl` and
   does not unfold `gset` operations. (by Paolo G. Giarrusso, BedRock Systems)
 - Add `get_head` tactic to determine the syntactic head of a function

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, size_list_to_set.
+  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 size_list_to_set 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.