More about finiteness of sets.

prelude/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.

prelude/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) _) = ∅.