phanerozoic/Coq-Stdpp huggingface dataset:
(* stdpp/fin_map_dom.v *)
Lemma kmap_dom_inv
    `{FinMapDom K1 M1 D1, !Elements K1 D1, !FinSet K1 D1, FinMapDom K2 M2 D2}
    {A} (f : K1 → K2) `{!Inj (=) (=) f} (m' : M2 A) (X : D1) :
  dom m' ≡ set_map f X →
  ∃ m : M1 A, m' = kmap f m ∧ dom m ≡ X.
Proof.
  revert X. induction m' as [|k' x m' Hk IH] using map_ind; intros X Hm'.
  { exists ∅. rewrite dom_empty in Hm'. assert (X ≡ ∅) as -> by set_solver.
    by rewrite kmap_empty, dom_empty. }
  apply not_elem_of_dom in Hk. rewrite dom_insert in Hm'.
  assert (k' ∈ set_map (D:=D2) f X) as (k & -> & ?)%elem_of_map by set_solver.
  destruct (IH (X ∖ {[ k ]})) as (m & -> & HX').
  { rewrite (set_map_difference _), <-Hm'. set_solver. }
  exists (<[k:=x]> m). split; [by rewrite kmap_insert|].
  rewrite dom_insert, HX'. intros k''. destruct (decide (k'' = k)); set_solver.
Qed.
(* stdpp/fin_map_dom.v *)
Lemma kmap_dom_inv_L
    `{FinMapDom K1 M1 D1, !Elements K1 D1, !FinSet K1 D1, FinMapDom K2 M2 D2,
      !LeibnizEquiv D1, !LeibnizEquiv D2}
    {A} (f : K1 → K2) `{!Inj (=) (=) f} (m' : M2 A) (X : D1) :
  dom m' = set_map f X →
  ∃ m : M1 A, m' = kmap f m ∧ dom m = X.
Proof. unfold_leibniz. by apply kmap_dom_inv. Qed.
(* stdpp/fin_map_dom.v *)
Instance set_unfold_dom_seq `{FinMapDom nat M D} {A} start (xs : list A) i :
  SetUnfoldElemOf i (dom (map_seq start (M:=M A) xs)) (start ≤ i < start + length xs).
Proof. constructor. by rewrite dom_seq, elem_of_set_seq. Qed.
(* stdpp/fin_sets.v *)
(* Operations *)
Instance set_size `{Elements A C} : Size C
:= length ∘ elements.
(* stdpp/fin_sets.v *)
Definition set_fold `{Elements A C} {B}
  (f : A → B → B) (b : B) : C → B
:= foldr f b ∘ elements.
(* stdpp/fin_sets.v *)
Instance set_filter
    `{Elements A C, Empty C, Singleton A C, Union C} : Filter A C
:= λ P _ X,
  list_to_set (filter P (elements X)).
(* stdpp/fin_sets.v *)
Definition set_map `{Elements A C, Singleton B D, Empty D, Union D}
    (f : A → B) (X : C) : D
:=
  list_to_set (f <$> elements X).
(* stdpp/fin_sets.v *)
Instance : Params (@set_map) 8
:= {}.
(* stdpp/fin_sets.v *)
Definition set_bind `{Elements A SA, Empty SB, Union SB}
    (f : A → SB) (X : SA) : SB
:=
  ⋃ (f <$> elements X).
(* stdpp/fin_sets.v *)
Instance : Params (@set_bind) 6
:= {}.
(* stdpp/fin_sets.v *)
Definition set_omap `{Elements A C, Singleton B D, Empty D, Union D}
    (f : A → option B) (X : C) : D
:=
  list_to_set (omap f (elements X)).
(* stdpp/fin_sets.v *)
Instance : Params (@set_omap) 8
:= {}.
(* stdpp/fin_sets.v *)
Instance set_fresh `{Elements A C, Fresh A (list A)} : Fresh A C
:=
  fresh ∘ elements.
(* stdpp/fin_sets.v *)
(* We generalize the [fresh] operation on sets to generate lists of fresh
elements w.r.t. a set [X]. *)
Fixpoint fresh_list `{Fresh A C, Union C, Singleton A C}
    (n : nat) (X : C) : list A
:=
  match n with
  | 0 => []
  | S n => let x := fresh X in x :: fresh_list n ({[ x ]} ∪ X)
  end.
(* stdpp/fin_sets.v *)
Instance : Params (@fresh_list) 6
:= {}.
(* stdpp/fin_sets.v *)
(* The following inductive predicate classifies that a list of elements is
in fact fresh w.r.t. a set [X]. *)
Inductive Forall_fresh `{ElemOf A C} (X : C) : list A → Prop
:=
  | Forall_fresh_nil : Forall_fresh X []
  | Forall_fresh_cons x xs :
     x ∉ xs → x ∉ X → Forall_fresh X xs → Forall_fresh X (x :: xs).
(* stdpp/fin_sets.v *)
Lemma fin_set_finite X : set_finite X.
Proof. by exists (elements X); intros; rewrite elem_of_elements. Qed.
(* stdpp/fin_sets.v *)
Instance elem_of_dec_slow : RelDecision (∈@{C}) | 100.
Proof.
  refine (λ x X, cast_if (decide_rel (∈) x (elements X)));
    by rewrite <-(elem_of_elements _).
Defined.
(* stdpp/fin_sets.v *)
(* * The [elements] operation *)
Instance set_unfold_elements X x P :
  SetUnfoldElemOf x X P → SetUnfoldElemOf x (elements X) P.
Proof. constructor. by rewrite elem_of_elements, (set_unfold_elem_of x X P). Qed.
(* stdpp/fin_sets.v *)
Instance elements_proper: Proper ((≡) ==> (≡ₚ)) (elements (C:=C)).
Proof.
  intros ?? E. apply NoDup_Permutation.
  - apply NoDup_elements.
  - apply NoDup_elements.
  - intros. by rewrite !elem_of_elements, E.
Qed.
(* stdpp/fin_sets.v *)
Lemma elements_empty : elements (∅ : C) = [].
Proof.
  apply elem_of_nil_inv; intros x.
  rewrite elem_of_elements, elem_of_empty; tauto.
Qed.
(* stdpp/fin_sets.v *)
Lemma elements_empty_iff X : elements X = [] ↔ X ≡ ∅.
Proof.
  rewrite <-Permutation_nil_r. split; [|intros ->; by rewrite elements_empty].
  intros HX. apply elem_of_equiv_empty; intros x.
  rewrite <-elem_of_elements, HX. apply not_elem_of_nil.
Qed.
(* stdpp/fin_sets.v *)
Lemma elements_empty_inv X : elements X = [] → X ≡ ∅.
Proof. apply elements_empty_iff. Qed.
(* stdpp/fin_sets.v *)
Lemma elements_union_singleton X x :
  x ∉ X → elements ({[ x ]} ∪ X) ≡ₚ x :: elements X.
Proof.
  intros ?; apply NoDup_Permutation.
  { apply NoDup_elements. }
  { by constructor; rewrite ?elem_of_elements; try apply NoDup_elements. }
  intros y; rewrite elem_of_elements, elem_of_union, elem_of_singleton.
  by rewrite elem_of_cons, elem_of_elements.
Qed.
(* stdpp/fin_sets.v *)
Lemma elements_singleton x : elements ({[ x ]} : C) = [x].
Proof.
  apply Permutation_singleton_r. by rewrite <-(right_id ∅ (∪) {[x]}),
    elements_union_singleton, elements_empty by set_solver.
Qed.
(* stdpp/fin_sets.v *)
Lemma elements_disj_union X Y :
  X ## Y → elements (X ∪ Y) ≡ₚ elements X ++ elements Y.
Proof.
  intros HXY. apply NoDup_Permutation.
  - apply NoDup_elements.
  - apply NoDup_app. set_solver by eauto using NoDup_elements.
  - set_solver.
Qed.
(* stdpp/fin_sets.v *)
Lemma elements_submseteq X Y : X ⊆ Y → elements X ⊆+ elements Y.
Proof.
  intros; apply NoDup_submseteq; eauto using NoDup_elements.
  intros x. rewrite !elem_of_elements; auto.
Qed.
(* stdpp/fin_sets.v *)
Lemma list_to_set_elements X : list_to_set (elements X) ≡ X.
Proof. intros ?. rewrite elem_of_list_to_set. apply elem_of_elements. Qed.
(* stdpp/fin_sets.v *)
Lemma list_to_set_elements_L `{!LeibnizEquiv C} X : list_to_set (elements X) = X.
Proof. unfold_leibniz. apply list_to_set_elements. Qed.
(* stdpp/fin_sets.v *)
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.
(* stdpp/fin_sets.v *)
(* * The [size] operation *)
Instance set_size_proper: Proper ((≡) ==> (=)) (@size C _).
Proof. intros ?? E. apply Permutation_length. by rewrite E. Qed.
(* stdpp/fin_sets.v *)
Lemma size_empty : size (∅ : C) = 0.
Proof. unfold size, set_size. simpl. by rewrite elements_empty. Qed.
(* stdpp/fin_sets.v *)
Lemma size_empty_iff X : size X = 0 ↔ X ≡ ∅.
Proof.
  split; [|intros ->; by rewrite size_empty].
  intros; apply equiv_empty; intros x; rewrite <-elem_of_elements.
  by rewrite (nil_length_inv (elements X)), ?elem_of_nil.
Qed.
(* stdpp/fin_sets.v *)
Lemma size_empty_inv X : size X = 0 → X ≡ ∅.
Proof. apply size_empty_iff. Qed.
(* stdpp/fin_sets.v *)
Lemma size_non_empty_iff X : size X ≠ 0 ↔ X ≢ ∅.
Proof. by rewrite size_empty_iff. Qed.
(* stdpp/fin_sets.v *)
Lemma set_choose_or_empty X : (∃ x, x ∈ X) ∨ X ≡ ∅.
Proof.
  destruct (elements X) as [|x l] eqn:HX; [right|left].
  - apply equiv_empty; intros x. by rewrite <-elem_of_elements, HX, elem_of_nil.
  - exists x. rewrite <-elem_of_elements, HX. by left.
Qed.
(* stdpp/fin_sets.v *)
Lemma set_choose X : X ≢ ∅ → ∃ x, x ∈ X.
Proof. intros. by destruct (set_choose_or_empty X). Qed.
(* stdpp/fin_sets.v *)
Lemma set_choose_L `{!LeibnizEquiv C} X : X ≠ ∅ → ∃ x, x ∈ X.
Proof. unfold_leibniz. apply set_choose. Qed.
(* stdpp/fin_sets.v *)
Lemma size_pos_elem_of X : 0 < size X → ∃ x, x ∈ X.
Proof.
  intros Hsz. destruct (set_choose_or_empty X) as [|HX]; [done|].
  contradict Hsz. rewrite HX, size_empty; lia.
Qed.
(* stdpp/fin_sets.v *)
Lemma size_singleton (x : A) : size ({[ x ]} : C) = 1.
Proof. unfold size, set_size. simpl. by rewrite elements_singleton. Qed.
(* stdpp/fin_sets.v *)
Lemma size_singleton_inv X x y : size X = 1 → x ∈ X → y ∈ X → x = y.
Proof.
  unfold size, set_size. simpl. rewrite <-!elem_of_elements.
  generalize (elements X). intros [|? l]; intro; simplify_eq/=.
  rewrite (nil_length_inv l), !list_elem_of_singleton by done; congruence.
Qed.
(* stdpp/fin_sets.v *)
Lemma size_1_elem_of X : size X = 1 → ∃ x, X ≡ {[ x ]}.
Proof.
  intros E. destruct (size_pos_elem_of X) as [x ?]; auto with lia.
  exists x. apply set_equiv. split.
  - rewrite elem_of_singleton. eauto using size_singleton_inv.
  - set_solver.
Qed.
(* stdpp/fin_sets.v *)
Lemma size_union X Y : X ## Y → size (X ∪ Y) = size X + size Y.
Proof.
  intros. unfold size, set_size. simpl. rewrite <-length_app.
  apply Permutation_length, NoDup_Permutation.
  - apply NoDup_elements.
  - apply NoDup_app; repeat split; try apply NoDup_elements.
    intros x; rewrite !elem_of_elements; set_solver.
  - intros. by rewrite elem_of_app, !elem_of_elements, elem_of_union.
Qed.
(* stdpp/fin_sets.v *)
Lemma size_union_alt X Y : size (X ∪ Y) = size X + size (Y ∖ X).
Proof.
  rewrite <-size_union by set_solver.
  setoid_replace (Y ∖ X) with ((Y ∪ X) ∖ X) by set_solver.
  rewrite <-union_difference, (comm (∪)); set_solver.
Qed.
(* stdpp/fin_sets.v *)
Lemma size_difference X Y : Y ⊆ X → size (X ∖ Y) = size X - size Y.
Proof.
  intros. rewrite (union_difference Y X) at 2 by done.
  rewrite size_union by set_solver. lia.
Qed.
(* stdpp/fin_sets.v *)
Lemma size_difference_alt X Y : size (X ∖ Y) = size X - size (X ∩ Y).
Proof.
  intros. rewrite <-size_difference by set_solver.
  apply set_size_proper. set_solver.
Qed.
(* stdpp/fin_sets.v *)
Lemma size_difference_le X1 X2 : size (X1 ∖ X2) ≤ size X1.
Proof. rewrite size_difference_alt. lia. Qed.
(* stdpp/fin_sets.v *)
Lemma size_union_le X1 X2 : size (X1 ∪ X2) ≤ size X1 + size X2.
Proof. rewrite size_union_alt, size_difference_alt. lia. Qed.
(* stdpp/fin_sets.v *)
Lemma set_subseteq_size_equiv X1 X2 : X1 ⊆ X2 → size X2 ≤ size X1 → X1 ≡ X2.
Proof.
  intros. apply (anti_symm _); [done|].
  apply empty_difference_subseteq, size_empty_iff.
  rewrite size_difference by done. lia.
Qed.
(* stdpp/fin_sets.v *)
Lemma set_subseteq_size_eq `{!LeibnizEquiv C} X1 X2 :
  X1 ⊆ X2 → size X2 ≤ size X1 → X1 = X2.
Proof. unfold_leibniz. apply set_subseteq_size_equiv. Qed.
(* stdpp/fin_sets.v *)
Lemma subseteq_size X Y : X ⊆ Y → size X ≤ size Y.
Proof. intros. rewrite (union_difference X Y), size_union_alt by done. lia. Qed.
(* stdpp/fin_sets.v *)
Lemma subset_size X Y : X ⊂ Y → size X < size Y.
Proof.
  intros. rewrite (union_difference X Y) by set_solver.
  rewrite size_union_alt, difference_twice.
  cut (size (Y ∖ X) ≠ 0); [lia |].
  by apply size_non_empty_iff, non_empty_difference.
Qed.
(* stdpp/fin_sets.v *)
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.
(* stdpp/fin_sets.v *)
(* * Induction principles *)
Lemma set_wf : well_founded (⊂@{C}).
Proof. apply (wf_projected (<) size); auto using subset_size, lt_wf. Qed.
(* stdpp/fin_sets.v *)
Lemma set_ind (P : C → Prop) :
  Proper ((≡) ==> impl) P →
  P ∅ → (∀ x X, x ∉ X → P X → P ({[ x ]} ∪ X)) → ∀ X, P X.
Proof.
  intros ? Hemp Hadd. apply well_founded_induction with (⊂).
  { apply set_wf. }
  intros X IH. destruct (set_choose_or_empty X) as [[x ?]|HX].
  - rewrite (union_difference {[ x ]} X) by set_solver.
    apply Hadd; [set_solver|]. apply IH; set_solver.
  - by rewrite HX.
Qed.
(* stdpp/fin_sets.v *)
Lemma set_ind_L `{!LeibnizEquiv C} (P : C → Prop) :
  P ∅ → (∀ x X, x ∉ X → P X → P ({[ x ]} ∪ X)) → ∀ X, P X.
Proof. apply set_ind. by intros ?? ->%leibniz_equiv_iff. Qed.
(* stdpp/fin_sets.v *)
(* * The [set_fold] operation *)
Lemma set_fold_ind {B} (P : B → C → Prop) (f : A → B → B) (b : B) :
  (∀ x, Proper ((≡) ==> impl) (P x)) →
  P b ∅ → (∀ x X r, x ∉ X → P r X → P (f x r) ({[ x ]} ∪ X)) →
  ∀ X, P (set_fold f b X) X.
Proof.
  intros ? Hemp Hadd.
  cut (∀ l, NoDup l → ∀ X, (∀ x, x ∈ X ↔ x ∈ l) → P (foldr f b l) X).
  { intros help ?. apply help; [apply NoDup_elements|].
    symmetry. apply elem_of_elements. }
  induction 1 as [|x l ?? IH]; simpl.
  - intros X HX. setoid_rewrite elem_of_nil in HX.
    rewrite equiv_empty; [done|]. set_solver.
  - intros X HX. setoid_rewrite elem_of_cons in HX.
    rewrite (union_difference {[ x ]} X) by set_solver.
    apply Hadd; [set_solver|]. apply IH; set_solver.
Qed.
(* stdpp/fin_sets.v *)
Lemma set_fold_ind_L `{!LeibnizEquiv C}
    {B} (P : B → C → Prop) (f : A → B → B) (b : B) :
  P b ∅ → (∀ x X r, x ∉ X → P r X → P (f x r) ({[ x ]} ∪ X)) →
  ∀ X, P (set_fold f b X) X.
Proof. apply set_fold_ind. solve_proper. Qed.
(* stdpp/fin_sets.v *)
Lemma set_fold_proper {B} (R : relation B) `{!PreOrder R}
    (f : A → B → B) (b : B) `{!∀ a, Proper (R ==> R) (f a)}
    (Hf : ∀ a1 a2 b, R (f a1 (f a2 b)) (f a2 (f a1 b))) :
  Proper ((≡) ==> R) (set_fold f b : C → B).
Proof. intros ?? E. apply (foldr_permutation R f b); auto. by rewrite E. Qed.
(* stdpp/fin_sets.v *)
Lemma set_fold_empty {B} (f : A → B → B) (b : B) :
  set_fold f b (∅ : C) = b.
Proof. by unfold set_fold; simpl; rewrite elements_empty. Qed.
(* stdpp/fin_sets.v *)
Lemma set_fold_singleton {B} (f : A → B → B) (b : B) (a : A) :
  set_fold f b ({[a]} : C) = f a b.
Proof. by unfold set_fold; simpl; rewrite elements_singleton. Qed.
(* stdpp/fin_sets.v *)
Lemma set_fold_union (f : A → A → A) (b : A) X Y :
  IdemP (=) f →
  Comm (=) f →
  Assoc (=) f →
  set_fold f b (X ∪ Y) = set_fold f (set_fold f b X) Y.
Proof.
  intros. apply (set_fold_union_strong _ _ _ _ _ _).
  - intros x b' _. by rewrite (assoc_L f), (idemp f).
  - intros x1 x2 b' _ _ _. by rewrite !(assoc_L f), (comm_L f x1).
Qed.
(* stdpp/fin_sets.v *)
(* Generalization of [set_fold_disj_union] (below) with a.) a relation [R]
instead of equality b.) a function [f : A → B → B] instead of [f : A → A → A],
and c.) premises that ensure the elements are in [X ∪ Y]. *)
Lemma set_fold_disj_union_strong {B} (R : relation B) `{!PreOrder R}
    (f : A → B → B) (b : B) X Y :
  (∀ x, Proper (R ==> R) (f x)) →
  (∀ x1 x2 b',
    (** This is morally commutativity + associativity for elements of [X ∪ Y] *)
    x1 ∈ X ∪ Y → x2 ∈ X ∪ Y → x1 ≠ x2 →
    R (f x1 (f x2 b')) (f x2 (f x1 b'))) →
  X ## Y →
  R (set_fold f b (X ∪ Y)) (set_fold f (set_fold f b X) Y).
Proof. intros. apply set_fold_union_strong; set_solver. Qed.
(* stdpp/fin_sets.v *)
Lemma set_fold_disj_union (f : A → A → A) (b : A) X Y :
  Comm (=) f →
  Assoc (=) f →
  X ## Y →
  set_fold f b (X ∪ Y) = set_fold f (set_fold f b X) Y.
Proof.
  intros. apply (set_fold_disj_union_strong _ _ _ _ _ _); [|done].
  intros x1 x2 b' _ _ _. by rewrite !(assoc_L f), (comm_L f x1).
Qed.
(* stdpp/fin_sets.v *)
Lemma set_fold_comm_acc_strong {B} (R : relation B) `{!PreOrder R}
    (f : A → B → B) (g : B → B) (b : B) X :
  (∀ x, Proper (R ==> R) (f x)) →
  (∀ x y, x ∈ X → R (f x (g y)) (g (f x y))) →
  R (set_fold f (g b) X) (g (set_fold f b X)).
Proof.
  intros. unfold set_fold; simpl.
  apply foldr_comm_acc_strong; [done|solve_proper|set_solver].
Qed.
(* stdpp/fin_sets.v *)
Lemma set_fold_comm_acc {B} (f : A → B → B) (g : B → B) (b : B) X :
  (∀ x y, f x (g y) = g (f x y)) →
  set_fold f (g b) X = g (set_fold f b X).
Proof. intros. apply (set_fold_comm_acc_strong _); [solve_proper|auto]. Qed.
(* stdpp/fin_sets.v *)
(* * Minimal elements *)
Lemma minimal_exists_elem_of R `{!Transitive R, ∀ x y, Decision (R x y)} X :
  X ≢ ∅ → ∃ x, x ∈ X ∧ minimal R x X.
Proof.
  pattern X; apply set_ind; clear X.
  { by intros X X' HX; setoid_rewrite HX. }
  { done. }
  intros x X ? IH Hemp. destruct (set_choose_or_empty X) as [[z ?]|HX].
  { destruct IH as (x' & Hx' & Hmin); [set_solver|].
    destruct (decide (R x x')).
    - exists x; split; [set_solver|].
      eapply union_minimal; [eapply singleton_minimal|by eapply minimal_weaken].
    - exists x'; split; [set_solver|].
      by eapply union_minimal; [apply singleton_minimal_not_above|]. }
  exists x; split; [set_solver|].
  rewrite HX, (right_id _ (∪)). apply singleton_minimal.
Qed.
(* stdpp/fin_sets.v *)
Lemma minimal_exists_elem_of_L R `{!LeibnizEquiv C, !Transitive R,
    ∀ x y, Decision (R x y)} X :
  X ≠ ∅ → ∃ x, x ∈ X ∧ minimal R x X.
Proof. unfold_leibniz. apply (minimal_exists_elem_of R). Qed.
(* stdpp/fin_sets.v *)
Lemma minimal_exists R `{!Transitive R,
    ∀ x y, Decision (R x y)} `{!Inhabited A} X :
  ∃ x, minimal R x X.
Proof.
  destruct (set_choose_or_empty X) as [ (y & Ha) | Hne].
  - edestruct (minimal_exists_elem_of R X) as (x & Hel & Hmin); first set_solver.
    exists x. done.
  - exists inhabitant. intros y Hel. set_solver.
Qed.
(* stdpp/fin_sets.v *)
(* * Filter *)
Lemma elem_of_filter (P : A → Prop) `{!∀ x, Decision (P x)} X x :
  x ∈ filter P X ↔ P x ∧ x ∈ X.
Proof.
  unfold filter, set_filter.
  by rewrite elem_of_list_to_set, list_elem_of_filter, elem_of_elements.
Qed.
(* stdpp/fin_sets.v *)
Instance set_unfold_filter (P : A → Prop) `{!∀ x, Decision (P x)} X Q x :
  SetUnfoldElemOf x X Q → SetUnfoldElemOf x (filter P X) (P x ∧ Q).
Proof.
  intros ?; constructor. by rewrite elem_of_filter, (set_unfold_elem_of x X Q).
Qed.
(* stdpp/fin_sets.v *)
Lemma filter_empty : filter P ∅ ≡@{C} ∅.
Proof. set_solver. Qed.
(* stdpp/fin_sets.v *)
Lemma filter_singleton x :
    filter P {[ x ]} ≡@{C} if decide (P x) then {[ x ]} else ∅.
Proof. case_decide; set_solver. Qed.
(* stdpp/fin_sets.v *)
Lemma filter_singleton_True x : P x → filter P {[ x ]} ≡@{C} {[ x ]}.
Proof. set_solver. Qed.
(* stdpp/fin_sets.v *)
Lemma filter_singleton_False x : ¬P x → filter P {[ x ]} ≡@{C} ∅.
Proof. set_solver. Qed.
(* stdpp/fin_sets.v *)
Lemma filter_empty_not_elem_of X x : filter P X ≡ ∅ → P x → x ∉ X.
Proof. set_solver. Qed.
(* stdpp/fin_sets.v *)
Lemma disjoint_filter X Y : X ## Y → filter P X ## filter P Y.
Proof. set_solver. Qed.
(* stdpp/fin_sets.v *)
Lemma filter_union X Y : filter P (X ∪ Y) ≡ filter P X ∪ filter P Y.
Proof. set_solver. Qed.
(* stdpp/fin_sets.v *)
Lemma disjoint_filter_complement X : filter P X ## filter (λ x, ¬P x) X.
Proof. set_solver. Qed.
(* stdpp/fin_sets.v *)
Lemma filter_union_complement X : filter P X ∪ filter (λ x, ¬P x) X ≡ X.
Proof. intros x. destruct (decide (P x)); set_solver. Qed.
(* stdpp/fin_sets.v *)
Lemma filter_subseteq X : filter P X ⊆ X.
Proof. set_solver. Qed.
(* stdpp/fin_sets.v *)
Lemma size_filter_le X : size (filter P X) ≤ size X.
Proof. apply subseteq_size, filter_subseteq. Qed.
(* stdpp/fin_sets.v *)
Lemma filter_id X : filter P X ≡ X ↔ ∀ x, x ∈ X → P x.
Proof. set_solver. Qed.
(* stdpp/fin_sets.v *)
Lemma filter_empty_L : filter P ∅ =@{C} ∅.
Proof. unfold_leibniz. apply filter_empty. Qed.
(* stdpp/fin_sets.v *)
Lemma filter_singleton_L x :
      filter P {[ x ]} =@{C} if decide (P x) then {[ x ]} else ∅.
Proof. unfold_leibniz. apply filter_singleton. Qed.
(* stdpp/fin_sets.v *)
Lemma filter_singleton_True_L x : P x → filter P {[ x ]} =@{C} {[ x ]}.
Proof. unfold_leibniz. apply filter_singleton_True. Qed.
(* stdpp/fin_sets.v *)
Lemma filter_singleton_False_L x : ¬P x → filter P {[ x ]} =@{C} ∅.
Proof. unfold_leibniz. apply filter_singleton_False. Qed.
(* stdpp/fin_sets.v *)
Lemma filter_empty_not_elem_of_L X x : filter P X = ∅ → P x → x ∉ X.
Proof. unfold_leibniz. apply filter_empty_not_elem_of. Qed.
(* stdpp/fin_sets.v *)
Lemma filter_union_L X Y : filter P (X ∪ Y) = filter P X ∪ filter P Y.
Proof. unfold_leibniz. apply filter_union. Qed.
(* stdpp/fin_sets.v *)
Lemma filter_union_complement_L X Y : filter P X ∪ filter (λ x, ¬P x) X = X.
Proof. unfold_leibniz. apply filter_union_complement. Qed.
(* stdpp/fin_sets.v *)
Lemma filter_id_L X : filter P X = X ↔ ∀ x, x ∈ X → P x.
Proof. unfold_leibniz. apply filter_id. Qed.
(* stdpp/fin_sets.v *)
Lemma elem_of_map (f : A → B) (X : C) y :
    y ∈ set_map (D:=D) f X ↔ ∃ x, y = f x ∧ x ∈ X.
Proof.
    unfold set_map. rewrite elem_of_list_to_set, list_elem_of_fmap.
    by setoid_rewrite elem_of_elements.
  Qed.
(* stdpp/fin_sets.v *)
Instance set_unfold_map (f : A → B) (X : C) (P : A → Prop) y :
    (∀ x, SetUnfoldElemOf x X (P x)) →
    SetUnfoldElemOf y (set_map (D:=D) f X) (∃ x, y = f x ∧ P x).
Proof. constructor. rewrite elem_of_map; naive_solver. Qed.
(* stdpp/fin_sets.v *)
Instance set_map_proper :
    Proper (pointwise_relation _ (=) ==> (≡) ==> (≡)) (set_map (C:=C) (D:=D)).
Proof. intros f g ? X Y. set_unfold; naive_solver. Qed.
(* stdpp/fin_sets.v *)
Instance set_map_mono :
    Proper (pointwise_relation _ (=) ==> (⊆) ==> (⊆)) (set_map (C:=C) (D:=D)).
Proof. intros f g ? X Y. set_unfold; naive_solver. Qed.
(* stdpp/fin_sets.v *)
Lemma elem_of_map_1 (f : A → B) (X : C) (y : B) :
    y ∈ set_map (D:=D) f X → ∃ x, y = f x ∧ x ∈ X.
Proof. set_solver. Qed.
(* stdpp/fin_sets.v *)
Lemma elem_of_map_2 (f : A → B) (X : C) (x : A) :
    x ∈ X → f x ∈ set_map (D:=D) f X.
Proof. set_solver. Qed.
(* stdpp/fin_sets.v *)
Lemma elem_of_map_2_alt (f : A → B) (X : C) (x : A) (y : B) :
    x ∈ X → y = f x → y ∈ set_map (D:=D) f X.
Proof. set_solver. Qed.
(* stdpp/fin_sets.v *)
Lemma set_map_empty (f : A → B) :
    set_map (C:=C) (D:=D) f ∅ = ∅.
Proof. unfold set_map. rewrite elements_empty. done. Qed.
(* stdpp/fin_sets.v *)
Lemma set_map_union (f : A → B) (X Y : C) :
    set_map (D:=D) f (X ∪ Y) ≡ set_map (D:=D) f X ∪ set_map (D:=D) f Y.
Proof. set_solver. Qed.
(* stdpp/fin_sets.v *)
(* This cannot be using [=] because [list_to_set_singleton] does not hold for [=]. *)
Lemma set_map_singleton (f : A → B) (x : A) :
    set_map (C:=C) (D:=D) f {[x]} ≡ {[f x]}.
Proof. set_solver. Qed.
(* stdpp/fin_sets.v *)
Lemma list_to_set_fmap (f : A → B) (l : list A) :
    list_to_set (f <$> l) ≡@{D} set_map f (list_to_set (C:=C) l).
Proof. set_solver. Qed.
(* stdpp/fin_sets.v *)
Lemma set_map_union_L `{!LeibnizEquiv D} (f : A → B) (X Y : C) :
    set_map (D:=D) f (X ∪ Y) = set_map (D:=D) f X ∪ set_map (D:=D) f Y.
Proof. unfold_leibniz. apply set_map_union. Qed.
(* stdpp/fin_sets.v *)
Lemma set_map_singleton_L `{!LeibnizEquiv D} (f : A → B) (x : A) :
    set_map (C:=C) (D:=D) f {[x]} = {[f x]}.
Proof. unfold_leibniz. apply set_map_singleton. Qed.
(* stdpp/fin_sets.v *)
Lemma list_to_set_fmap_L `{!LeibnizEquiv C, !LeibnizEquiv D}
      (f : A → B) (l : list A) :
    list_to_set (f <$> l) =@{D} set_map f (list_to_set (C:=C) l).
Proof. unfold_leibniz. apply list_to_set_fmap. Qed.
(* stdpp/fin_sets.v *)
Lemma set_map_difference `{Set_ B D} (f : A → B) `{!Inj (=) (=) f} (X Y : C) :
  set_map (D:=D) f (X ∖ Y) ≡ set_map (D:=D) f X ∖ set_map (D:=D) f Y.
Proof. set_solver. Qed.
(* stdpp/fin_sets.v *)
Lemma set_map_difference_L `{Set_ B D, !LeibnizEquiv D}
    (f : A → B) `{!Inj (=) (=) f} (X Y : C) :
  set_map (D:=D) f (X ∖ Y) = set_map (D:=D) f X ∖ set_map (D:=D) f Y.
Proof. unfold_leibniz. by apply set_map_difference. Qed.
(* stdpp/fin_sets.v *)
Notation set_bind
:= (set_bind (A:=A) (SA:=C) (SB:=SB)).
(* stdpp/fin_sets.v *)
Lemma elem_of_set_bind (f : A → SB) (X : C) y :
    y ∈ set_bind f X ↔ ∃ x, x ∈ X ∧ y ∈ f x.
Proof.
    unfold set_bind. rewrite !elem_of_union_list. set_solver.
  Qed.
(* stdpp/fin_sets.v *)
Instance set_unfold_set_bind (f : A → SB) (X : C)
       (y : B) (P : A → Prop) (Q : A → Prop) :
    (∀ x, SetUnfoldElemOf y (f x) (P x)) →
    (∀ x, SetUnfoldElemOf x X (Q x)) →
    SetUnfoldElemOf y (set_bind f X) (∃ x, Q x ∧ P x).
Proof.
    intros HSU1 HSU2. constructor.
    rewrite elem_of_set_bind. set_solver.
  Qed.
(* stdpp/fin_sets.v *)
Instance set_bind_proper :
    Proper (pointwise_relation _ (≡) ==> (≡) ==> (≡)) set_bind.
Proof. unfold pointwise_relation; intros f1 f2 Hf X1 X2 HX. set_solver. Qed.
(* stdpp/fin_sets.v *)
Instance set_bind_mono :
    Proper (pointwise_relation _ (⊆) ==> (⊆) ==> (⊆)) set_bind.
Proof. unfold pointwise_relation; intros f1 f2 Hf X1 X2 HX. set_solver. Qed.
(* stdpp/fin_sets.v *)
Lemma set_bind_ext (f g : A → SB) (X Y : C) :
    (∀ x, x ∈ X → x ∈ Y → f x ≡ g x) → X ≡ Y → set_bind f X ≡ set_bind g Y.
Proof. set_solver. Qed.
(* stdpp/fin_sets.v *)
Lemma set_bind_singleton f x : set_bind f {[x]} ≡ f x.
Proof. set_solver. Qed.
(* stdpp/fin_sets.v *)
Lemma set_bind_singleton_L `{!LeibnizEquiv SB} f x : set_bind f {[x]} = f x.
Proof. unfold_leibniz. apply set_bind_singleton. Qed.
(* stdpp/fin_sets.v *)
Lemma set_bind_disj_union f (X Y : C) :
    X ## Y → set_bind f (X ∪ Y) ≡ set_bind f X ∪ set_bind f Y.
Proof. set_solver. Qed.