From 42f4c16a00eb42df20f33b5f1a019f0f95e79e2b Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 16 Jan 2016 17:38:30 +0100
Subject: [PATCH] More about finiteness of sets.

---
 theories/collections.v | 11 +++++++++++
 theories/fin_map_dom.v |  5 +++++
 2 files changed, 16 insertions(+)

diff --git a/theories/collections.v b/theories/collections.v
index 2b54cd0c..b34b5cdc 100644
--- a/theories/collections.v
+++ b/theories/collections.v
@@ -591,6 +591,11 @@ Definition set_finite `{ElemOf A B} (X : B) := ∃ l : list A, ∀ x, x ∈ X 
 
 Section finite.
   Context `{SimpleCollection A B}.
+  Global Instance set_finite_subseteq :
+     Proper (flip (⊆) ==> impl) (@set_finite A B _).
+  Proof. intros X Y HX [l Hl]; exists l; solve_elem_of. Qed.
+  Global Instance set_finite_proper : Proper ((≡) ==> iff) (@set_finite A B _).
+  Proof. by intros X Y [??]; split; apply set_finite_subseteq. Qed.
   Lemma empty_finite : set_finite ∅.
   Proof. by exists []; intros ?; rewrite elem_of_empty. Qed.
   Lemma singleton_finite (x : A) : set_finite {[ x ]}.
@@ -614,4 +619,10 @@ Section more_finite.
   Proof. intros [l ?]; exists l; intros x [??]%elem_of_intersection; auto. Qed.
   Lemma difference_finite X Y : set_finite X → set_finite (X ∖ Y).
   Proof. intros [l ?]; exists l; intros x [??]%elem_of_difference; auto. Qed.
+  Lemma difference_finite_inv X Y `{∀ x, Decision (x ∈ Y)} :
+    set_finite Y → set_finite (X ∖ Y) → set_finite X.
+  Proof.
+    intros [l ?] [k ?]; exists (l ++ k).
+    intros x ?; destruct (decide (x ∈ Y)); rewrite elem_of_app; solve_elem_of.
+  Qed.
 End more_finite.
diff --git a/theories/fin_map_dom.v b/theories/fin_map_dom.v
index e8169bf0..7c4e7697 100644
--- a/theories/fin_map_dom.v
+++ b/theories/fin_map_dom.v
@@ -108,6 +108,11 @@ Proof.
   rewrite !elem_of_dom, lookup_fmap, <-!not_eq_None_Some.
   destruct (m !! i); naive_solver.
 Qed.
+Lemma dom_finite {A} (m : M A) : set_finite (dom D m).
+Proof.
+  induction m using map_ind; rewrite ?dom_empty, ?dom_insert;
+    eauto using empty_finite, union_finite, singleton_finite.
+Qed.
 
 Context `{!LeibnizEquiv D}.
 Lemma dom_empty_L {A} : dom D (@empty (M A) _) = ∅.
-- 
GitLab