Commit 42f4c16a authored by Robbert Krebbers's avatar Robbert Krebbers

More about finiteness of sets.

parent ced43e23
......@@ -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.
intros [l ?] [k ?]; exists (l ++ k).
intros x ?; destruct (decide (x Y)); rewrite elem_of_app; solve_elem_of.
End more_finite.
......@@ -108,6 +108,11 @@ Proof.
rewrite !elem_of_dom, lookup_fmap, <-!not_eq_None_Some.
destruct (m !! i); naive_solver.
Lemma dom_finite {A} (m : M A) : set_finite (dom D m).
induction m using map_ind; rewrite ?dom_empty, ?dom_insert;
eauto using empty_finite, union_finite, singleton_finite.
Context `{!LeibnizEquiv D}.
Lemma dom_empty_L {A} : dom D (@empty (M A) _) = .
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment