From 407d8414f6c79e2bc70eb879b717bd66f2350e59 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 11 Aug 2021 17:58:43 +0200
Subject: [PATCH] relate size of map to size of its domain

---
 theories/fin_map_dom.v | 17 +++++++++++++++++
 theories/fin_sets.v    | 16 ++++++++++++++++
 2 files changed, 33 insertions(+)

diff --git a/theories/fin_map_dom.v b/theories/fin_map_dom.v
index c9951d4a..75aeb309 100644
--- a/theories/fin_map_dom.v
+++ b/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.
diff --git a/theories/fin_sets.v b/theories/fin_sets.v
index 5f5168a7..0f81651d 100644
--- a/theories/fin_sets.v
+++ b/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.
-- 
GitLab