From VLSM.Lib Require Import Itauto.[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_plugin.cmxs (using legacy method) ... done]
[Loading ML file btauto_plugin.cmxs (using legacy method) ... done]
[Loading ML file coq-itauto.plugin ... done]
From stdpp Require Import prelude fin_maps.
From VLSM.Lib Require Import Preamble.

Utility: Finite Set Utility Definitions and Results

For some reason, this instance is not exported by stdpp.

#[export] Existing Instance elem_of_dec_slow.

Section sec_fin_set.

Context
  `{FinSet A C}.

Section sec_general.

If X is a subset of Y, then the elements of X are a sublist of the elements of Y.

Lemma elements_subseteq (X Y : C) :
  X ⊆ Y -> elements X ⊆ elements Y.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X, Y: C
X ⊆ Y → elements X ⊆ elements Y
Proof.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X, Y: C
X ⊆ Y → elements X ⊆ elements Y by set_solver. Qed.

Lemma union_size_ge_size1
  (X Y : C) :
  size (X ∪ Y) >= size X.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X, Y: C
size (X ∪ Y) ≥ size X
Proof.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X, Y: C
size (X ∪ Y) ≥ size X
  apply subseteq_size.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X, Y: C
X ⊆ X ∪ Y
  apply subseteq_union.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X, Y: C
X ∪ (X ∪ Y) ≡ X ∪ Y
  by set_solver.
Qed.

Lemma union_size_ge_size2
  (X Y : C) :
  size (X ∪ Y) >= size Y.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X, Y: C
size (X ∪ Y) ≥ size Y
Proof.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X, Y: C
size (X ∪ Y) ≥ size Y
  apply subseteq_size.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X, Y: C
Y ⊆ X ∪ Y
  apply subseteq_union.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X, Y: C
Y ∪ (X ∪ Y) ≡ X ∪ Y
  by set_solver.
Qed.

Lemma union_size_ge_average
  (X Y : C) :
  2 * size (X ∪ Y) >= size X + size Y.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X, Y: C
2 * size (X ∪ Y) ≥ size X + size Y
Proof.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X, Y: C
2 * size (X ∪ Y) ≥ size X + size Y
  specialize (union_size_ge_size1 X Y) as Hx.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X, Y: C
Hx: size (X ∪ Y) ≥ size X
2 * size (X ∪ Y) ≥ size X + size Y
  specialize (union_size_ge_size2 X Y) as Hy.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X, Y: C
Hx: size (X ∪ Y) ≥ size X
Hy: size (X ∪ Y) ≥ size Y
2 * size (X ∪ Y) ≥ size X + size Y
  by lia.
Qed.

Lemma difference_size_le_self
  (X Y : C) :
  size (X ∖  Y) <= size X.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X, Y: C
size (X ∖ Y) ≤ size X
Proof.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X, Y: C
size (X ∖ Y) ≤ size X
  apply subseteq_size.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X, Y: C
X ∖ Y ⊆ X
  apply elem_of_subseteq.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X, Y: C
∀ x : A, x ∈ X ∖ Y → x ∈ X
  intros x Hx.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X, Y: C
x: A
Hx: x ∈ X ∖ Y
x ∈ X
  apply elem_of_difference in Hx.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X, Y: C
x: A
Hx: x ∈ X ∧ x ∉ Y
x ∈ X
  by itauto.
Qed.

Lemma union_size_le_sum
  (X Y : C) :
  size (X ∪ Y) <= size X + size Y.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X, Y: C
size (X ∪ Y) ≤ size X + size Y
Proof.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X, Y: C
size (X ∪ Y) ≤ size X + size Y
  specialize (size_union_alt X Y) as Halt.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X, Y: C
Halt: size (X ∪ Y) = size X + size (Y ∖ X)
size (X ∪ Y) ≤ size X + size Y
  rewrite Halt.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X, Y: C
Halt: size (X ∪ Y) = size X + size (Y ∖ X)
size X + size (Y ∖ X) ≤ size X + size Y
  specialize (difference_size_le_self Y X).A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X, Y: C
Halt: size (X ∪ Y) = size X + size (Y ∖ X)
size (Y ∖ X) ≤ size Y
→ size X + size (Y ∖ X) ≤ size X + size Y
  by lia.
Qed.

Lemma intersection_size1
  (X Y : C) :
  size (X ∩ Y) <= size X.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X, Y: C
size (X ∩ Y) ≤ size X
Proof.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X, Y: C
size (X ∩ Y) ≤ size X
  apply (subseteq_size (X ∩ Y) X).A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X, Y: C
X ∩ Y ⊆ X
  by set_solver.
Qed.

Lemma intersection_size2
  (X Y : C) :
  size (X ∩ Y) <= size Y.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X, Y: C
size (X ∩ Y) ≤ size Y
Proof.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X, Y: C
size (X ∩ Y) ≤ size Y
  apply (subseteq_size (X ∩ Y) Y).A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X, Y: C
X ∩ Y ⊆ Y
  by set_solver.
Qed.

Lemma difference_size_subset
  (X Y : C)
  (Hsub : Y ⊆ X) :
  (Z.of_nat (size (X ∖ Y)) = Z.of_nat (size X) - Z.of_nat (size Y))%Z.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X, Y: C
Hsub: Y ⊆ X
Z.of_nat (size (X ∖ Y)) =
(Z.of_nat (size X) - Z.of_nat (size Y))%Z
Proof.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X, Y: C
Hsub: Y ⊆ X
Z.of_nat (size (X ∖ Y)) =
(Z.of_nat (size X) - Z.of_nat (size Y))%Z
  assert (Htemp : Y ∪ (X ∖ Y) ≡ X).A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X, Y: C
Hsub: Y ⊆ X
Y ∪ X ∖ Y ≡ X
A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X, Y: C
Hsub: Y ⊆ X
Htemp: Y ∪ X ∖ Y ≡ X
Z.of_nat (size (X ∖ Y)) =
(Z.of_nat (size X) - Z.of_nat (size Y))%Z
  {A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X, Y: C
Hsub: Y ⊆ X
Y ∪ X ∖ Y ≡ X
    apply set_equiv_equivalence.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X, Y: C
Hsub: Y ⊆ X
Y ∪ X ∖ Y ∈ X
    intros a.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X, Y: C
Hsub: Y ⊆ X
a: A
a ∈ Y ∪ X ∖ Y ↔ a ∈ X
    split; intros Ha.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X, Y: C
Hsub: Y ⊆ X
a: A
Ha: a ∈ Y ∪ X ∖ Y
a ∈ X
A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X, Y: C
Hsub: Y ⊆ X
a: A
Ha: a ∈ X
a ∈ Y ∪ X ∖ Y
    -A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X, Y: C
Hsub: Y ⊆ X
a: A
Ha: a ∈ Y ∪ X ∖ Y
a ∈ X by set_solver.
    -A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X, Y: C
Hsub: Y ⊆ X
a: A
Ha: a ∈ X
a ∈ Y ∪ X ∖ Y destruct (decide (a ∈ Y)).A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X, Y: C
Hsub: Y ⊆ X
a: A
Ha: a ∈ X
e: a ∈ Y
a ∈ Y ∪ X ∖ Y
A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X, Y: C
Hsub: Y ⊆ X
a: A
Ha: a ∈ X
n: a ∉ Y
a ∈ Y ∪ X ∖ Y
      +A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X, Y: C
Hsub: Y ⊆ X
a: A
Ha: a ∈ X
e: a ∈ Y
a ∈ Y ∪ X ∖ Y by apply elem_of_union; left; itauto.
      +A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X, Y: C
Hsub: Y ⊆ X
a: A
Ha: a ∈ X
n: a ∉ Y
a ∈ Y ∪ X ∖ Y by apply elem_of_union; right; set_solver.
  }A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X, Y: C
Hsub: Y ⊆ X
Htemp: Y ∪ X ∖ Y ≡ X
Z.of_nat (size (X ∖ Y)) =
(Z.of_nat (size X) - Z.of_nat (size Y))%Z
  assert (Htemp2 : size Y + size (X ∖ Y) = size X).A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X, Y: C
Hsub: Y ⊆ X
Htemp: Y ∪ X ∖ Y ≡ X
size Y + size (X ∖ Y) = size X
A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X, Y: C
Hsub: Y ⊆ X
Htemp: Y ∪ X ∖ Y ≡ X
Htemp2: size Y + size (X ∖ Y) = size X
Z.of_nat (size (X ∖ Y)) =
(Z.of_nat (size X) - Z.of_nat (size Y))%Z
  {A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X, Y: C
Hsub: Y ⊆ X
Htemp: Y ∪ X ∖ Y ≡ X
size Y + size (X ∖ Y) = size X
    specialize (size_union Y (X ∖ Y)) as Hun.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X, Y: C
Hsub: Y ⊆ X
Htemp: Y ∪ X ∖ Y ≡ X
Hun: Y ## X ∖ Y
→ size (Y ∪ X ∖ Y) = size Y + size (X ∖ Y)
size Y + size (X ∖ Y) = size X
    spec Hun.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X, Y: C
Hsub: Y ⊆ X
Htemp: Y ∪ X ∖ Y ≡ X
Hun: Y ## X ∖ Y
→ size (Y ∪ X ∖ Y) = size Y + size (X ∖ Y)
Y ## X ∖ Y
A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X, Y: C
Hsub: Y ⊆ X
Htemp: Y ∪ X ∖ Y ≡ X
Hun: size (Y ∪ X ∖ Y) = size Y + size (X ∖ Y)
size Y + size (X ∖ Y) = size X
    {A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X, Y: C
Hsub: Y ⊆ X
Htemp: Y ∪ X ∖ Y ≡ X
Hun: Y ## X ∖ Y
→ size (Y ∪ X ∖ Y) = size Y + size (X ∖ Y)
Y ## X ∖ Y
      apply elem_of_disjoint.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X, Y: C
Hsub: Y ⊆ X
Htemp: Y ∪ X ∖ Y ≡ X
Hun: Y ## X ∖ Y
→ size (Y ∪ X ∖ Y) = size Y + size (X ∖ Y)
∀ x : A, x ∈ Y → x ∈ X ∖ Y → False
      intros a Ha Ha2.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X, Y: C
Hsub: Y ⊆ X
Htemp: Y ∪ X ∖ Y ≡ X
Hun: Y ## X ∖ Y
→ size (Y ∪ X ∖ Y) = size Y + size (X ∖ Y)
a: A
Ha: a ∈ Y
Ha2: a ∈ X ∖ Y
False
      apply elem_of_difference in Ha2.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X, Y: C
Hsub: Y ⊆ X
Htemp: Y ∪ X ∖ Y ≡ X
Hun: Y ## X ∖ Y
→ size (Y ∪ X ∖ Y) = size Y + size (X ∖ Y)
a: A
Ha: a ∈ Y
Ha2: a ∈ X ∧ a ∉ Y
False
      by itauto.
    }A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X, Y: C
Hsub: Y ⊆ X
Htemp: Y ∪ X ∖ Y ≡ X
Hun: size (Y ∪ X ∖ Y) = size Y + size (X ∖ Y)
size Y + size (X ∖ Y) = size X
    rewrite Htemp in Hun.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X, Y: C
Hsub: Y ⊆ X
Htemp: Y ∪ X ∖ Y ≡ X
Hun: size X = size Y + size (X ∖ Y)
size Y + size (X ∖ Y) = size X
    by itauto.
  }A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X, Y: C
Hsub: Y ⊆ X
Htemp: Y ∪ X ∖ Y ≡ X
Htemp2: size Y + size (X ∖ Y) = size X
Z.of_nat (size (X ∖ Y)) =
(Z.of_nat (size X) - Z.of_nat (size Y))%Z
  by lia.
Qed.

Lemma difference_with_intersection
  (X Y : C) :
  X ∖ Y ≡ X ∖ (X ∩ Y).A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X, Y: C
X ∖ Y ≡ X ∖ (X ∩ Y)
Proof.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X, Y: C
X ∖ Y ≡ X ∖ (X ∩ Y)
  by set_solver.
Qed.

Lemma difference_size
  (X Y : C) :
  (Z.of_nat (size (X ∖ Y)) = Z.of_nat (size X) - Z.of_nat (size (X ∩ Y)))%Z.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X, Y: C
Z.of_nat (size (X ∖ Y)) =
(Z.of_nat (size X) - Z.of_nat (size (X ∩ Y)))%Z
Proof.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X, Y: C
Z.of_nat (size (X ∖ Y)) =
(Z.of_nat (size X) - Z.of_nat (size (X ∩ Y)))%Z
  rewrite difference_with_intersection.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X, Y: C
Z.of_nat (size (X ∖ (X ∩ Y))) =
(Z.of_nat (size X) - Z.of_nat (size (X ∩ Y)))%Z
  specialize (difference_size_subset X (X ∩ Y)) as Hdif.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X, Y: C
Hdif: X ∩ Y ⊆ X
→ Z.of_nat (size (X ∖ (X ∩ Y))) =
  (Z.of_nat (size X) - Z.of_nat (size (X ∩ Y)))%Z
Z.of_nat (size (X ∖ (X ∩ Y))) =
(Z.of_nat (size X) - Z.of_nat (size (X ∩ Y)))%Z
  by set_solver.
Qed.

Lemma difference_size_ge_disjoint_case
  (X Y : C) :
  size (X ∖ Y) >= size X - size Y.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X, Y: C
size (X ∖ Y) ≥ size X - size Y
Proof.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X, Y: C
size (X ∖ Y) ≥ size X - size Y
  specialize (difference_size X Y).A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X, Y: C
Z.of_nat (size (X ∖ Y)) =
(Z.of_nat (size X) - Z.of_nat (size (X ∩ Y)))%Z
→ size (X ∖ Y) ≥ size X - size Y
  specialize (intersection_size2 X Y).A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X, Y: C
size (X ∩ Y) ≤ size Y
→ Z.of_nat (size (X ∖ Y)) =
  (Z.of_nat (size X) - Z.of_nat (size (X ∩ Y)))%Z
  → size (X ∖ Y) ≥ size X - size Y
  by lia.
Qed.

Lemma list_to_set_size
  (l : list A) :
  size (list_to_set l (C := C)) <= length l.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
l: list A
size (list_to_set l) ≤ length l
Proof.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
l: list A
size (list_to_set l) ≤ length l
  induction l; cbn.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
size ∅ ≤ 0
A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
a: A
l: list A
IHl: size (list_to_set l) ≤ length l
size ({[a]} ∪ list_to_set l) ≤ S (length l)
  -A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
size ∅ ≤ 0 by rewrite size_empty; lia.
  -A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
a: A
l: list A
IHl: size (list_to_set l) ≤ length l
size ({[a]} ∪ list_to_set l) ≤ S (length l) specialize (union_size_le_sum ({[ a ]}) (list_to_set l)) as Hun_size.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
a: A
l: list A
IHl: size (list_to_set l) ≤ length l
Hun_size: size ({[a]} ∪ list_to_set l)
≤ size {[a]} + size (list_to_set l)
size ({[a]} ∪ list_to_set l) ≤ S (length l)
    by rewrite size_singleton in Hun_size; lia.
Qed.

#[export] Instance fin_set_subseteq_dec : RelDecision (⊆@{C}).A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
RelDecision subseteq
Proof.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
RelDecision subseteq
  intros X Y.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X, Y: C
Decision (X ⊆ Y)
  eapply @Decision_iff with (P := set_Forall (fun a => a ∈ Y) X).A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X, Y: C
set_Forall (λ a : A, a ∈ Y) X ↔ X ⊆ Y
A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X, Y: C
Decision (set_Forall (λ a : A, a ∈ Y) X)
  -A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X, Y: C
set_Forall (λ a : A, a ∈ Y) X ↔ X ⊆ Y by set_solver.
  -A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X, Y: C
Decision (set_Forall (λ a : A, a ∈ Y) X) by typeclasses eauto.
Qed.

#[export] Instance fin_set_empty_eq_dec :
  forall (X : C), Decision (X ≡ ∅).A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
∀ X : C, Decision (X ≡ ∅)
Proof.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
∀ X : C, Decision (X ≡ ∅)
  intros.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X: C
Decision (X ≡ ∅)
  destruct (decide (elements X = [])).A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X: C
e: elements X = []
Decision (X ≡ ∅)
A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X: C
n: elements X ≠ []
Decision (X ≡ ∅)
  -A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X: C
e: elements X = []
Decision (X ≡ ∅) by left; rewrite <- elements_empty_iff.
  -A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X: C
n: elements X ≠ []
Decision (X ≡ ∅) by right; rewrite <- elements_empty_iff.
Qed.

#[export] Instance fin_set_singleton_eq_dec :
  forall (X : C) (x : A), Decision (X ≡ {[x]}).A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
∀ (X : C) (x : A), Decision (X ≡ {[x]})
Proof.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
∀ (X : C) (x : A), Decision (X ≡ {[x]})
  intros X x.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X: C
x: A
Decision (X ≡ {[x]})
  destruct (decide (elements X = [x])) as [Heq|Heq].A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X: C
x: A
Heq: elements X = [x]
Decision (X ≡ {[x]})
A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X: C
x: A
Heq: elements X ≠ [x]
Decision (X ≡ {[x]})
  -A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X: C
x: A
Heq: elements X = [x]
Decision (X ≡ {[x]}) left; intro i.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X: C
x: A
Heq: elements X = [x]
i: A
i ∈ X ↔ i ∈ {[x]}
    rewrite elem_of_singleton, <- elem_of_elements.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X: C
x: A
Heq: elements X = [x]
i: A
i ∈ elements X ↔ i = x
    by rewrite Heq, elem_of_list_singleton.
  -A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X: C
x: A
Heq: elements X ≠ [x]
Decision (X ≡ {[x]}) right; contradict Heq.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X: C
x: A
Heq: X ≡ {[x]}
elements X = [x]
    apply Permutation_singleton_r.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
X: C
x: A
Heq: X ≡ {[x]}
elements X ≡ₚ [x]
    by rewrite Heq, elements_singleton.
Qed.

#[export] Instance finset_equiv_dec `{FinSet A C} : RelDecision (≡@{C}).A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
H7: ElemOf A C
H8: Empty C
H9: Singleton A C
H10: Union C
H11: Intersection C
H12: Difference C
H13: Elements A C
EqDecision1: EqDecision A
H14: FinSet A C
RelDecision equiv
Proof.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
H7: ElemOf A C
H8: Empty C
H9: Singleton A C
H10: Union C
H11: Intersection C
H12: Difference C
H13: Elements A C
EqDecision1: EqDecision A
H14: FinSet A C
RelDecision equiv
  intros X Y.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
H7: ElemOf A C
H8: Empty C
H9: Singleton A C
H10: Union C
H11: Intersection C
H12: Difference C
H13: Elements A C
EqDecision1: EqDecision A
H14: FinSet A C
X, Y: C
Decision (X ≡ Y)
  destruct (decide (elements X ≡ₚ elements Y));
    [| by right; contradict n; rewrite n].A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
H7: ElemOf A C
H8: Empty C
H9: Singleton A C
H10: Union C
H11: Intersection C
H12: Difference C
H13: Elements A C
EqDecision1: EqDecision A
H14: FinSet A C
X, Y: C
p: elements X ≡ₚ elements Y
Decision (X ≡ Y)
  left; intros a.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
H7: ElemOf A C
H8: Empty C
H9: Singleton A C
H10: Union C
H11: Intersection C
H12: Difference C
H13: Elements A C
EqDecision1: EqDecision A
H14: FinSet A C
X, Y: C
p: elements X ≡ₚ elements Y
a: A
a ∈ X ↔ a ∈ Y
  rewrite <- !elem_of_elements, !elem_of_list_lookup.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
H7: ElemOf A C
H8: Empty C
H9: Singleton A C
H10: Union C
H11: Intersection C
H12: Difference C
H13: Elements A C
EqDecision1: EqDecision A
H14: FinSet A C
X, Y: C
p: elements X ≡ₚ elements Y
a: A
(∃ i : nat, elements X !! i = Some a)
↔ (∃ i : nat, elements Y !! i = Some a)
  split; intros (i & Hi); [| symmetry in p];
    apply Permutation_inj in p as (Hlen & f & Hinjf & Hp).A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
H7: ElemOf A C
H8: Empty C
H9: Singleton A C
H10: Union C
H11: Intersection C
H12: Difference C
H13: Elements A C
EqDecision1: EqDecision A
H14: FinSet A C
X, Y: C
Hlen: length (elements X) = length (elements Y)
f: nat → nat
Hinjf: Inj eq eq f
Hp: ∀ i : nat, elements X !! i = elements Y !! f i
a: A
i: nat
Hi: elements X !! i = Some a
∃ i : nat, elements Y !! i = Some a
A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
H7: ElemOf A C
H8: Empty C
H9: Singleton A C
H10: Union C
H11: Intersection C
H12: Difference C
H13: Elements A C
EqDecision1: EqDecision A
H14: FinSet A C
X, Y: C
Hlen: length (elements Y) = length (elements X)
f: nat → nat
Hinjf: Inj eq eq f
Hp: ∀ i : nat, elements Y !! i = elements X !! f i
a: A
i: nat
Hi: elements Y !! i = Some a
∃ i : nat, elements X !! i = Some a
  -A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
H7: ElemOf A C
H8: Empty C
H9: Singleton A C
H10: Union C
H11: Intersection C
H12: Difference C
H13: Elements A C
EqDecision1: EqDecision A
H14: FinSet A C
X, Y: C
Hlen: length (elements X) = length (elements Y)
f: nat → nat
Hinjf: Inj eq eq f
Hp: ∀ i : nat, elements X !! i = elements Y !! f i
a: A
i: nat
Hi: elements X !! i = Some a
∃ i : nat, elements Y !! i = Some a by rewrite Hp in Hi; eexists.
  -A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
H7: ElemOf A C
H8: Empty C
H9: Singleton A C
H10: Union C
H11: Intersection C
H12: Difference C
H13: Elements A C
EqDecision1: EqDecision A
H14: FinSet A C
X, Y: C
Hlen: length (elements Y) = length (elements X)
f: nat → nat
Hinjf: Inj eq eq f
Hp: ∀ i : nat, elements Y !! i = elements X !! f i
a: A
i: nat
Hi: elements Y !! i = Some a
∃ i : nat, elements X !! i = Some a by rewrite Hp in Hi; eexists.
Qed.

End sec_general.

Section sec_filter.

Context
  (P P2 : A -> Prop)
  `{!forall x, Decision (P x)}
  `{!forall x, Decision (P2 x)}
  (X Y : C).

Lemma filter_subset
  (Hsub : X ⊆ Y) :
  filter P X ⊆ filter P Y.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
P, P2: A → Prop
H7: ∀ x : A, Decision (P x)
H8: ∀ x : A, Decision (P2 x)
X, Y: C
Hsub: X ⊆ Y
filter P X ⊆ filter P Y
Proof.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
P, P2: A → Prop
H7: ∀ x : A, Decision (P x)
H8: ∀ x : A, Decision (P2 x)
X, Y: C
Hsub: X ⊆ Y
filter P X ⊆ filter P Y
  intros a HaX.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
P, P2: A → Prop
H7: ∀ x : A, Decision (P x)
H8: ∀ x : A, Decision (P2 x)
X, Y: C
Hsub: X ⊆ Y
a: A
HaX: a ∈ filter P X
a ∈ filter P Y
  apply elem_of_filter in HaX.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
P, P2: A → Prop
H7: ∀ x : A, Decision (P x)
H8: ∀ x : A, Decision (P2 x)
X, Y: C
Hsub: X ⊆ Y
a: A
HaX: P a ∧ a ∈ X
a ∈ filter P Y
  apply elem_of_filter.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
P, P2: A → Prop
H7: ∀ x : A, Decision (P x)
H8: ∀ x : A, Decision (P2 x)
X, Y: C
Hsub: X ⊆ Y
a: A
HaX: P a ∧ a ∈ X
P a ∧ a ∈ Y
  by set_solver.
Qed.

Lemma filter_subprop
  (Hsub : forall a, (P a -> P2 a)) :
  filter P X ⊆ filter P2 X.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
P, P2: A → Prop
H7: ∀ x : A, Decision (P x)
H8: ∀ x : A, Decision (P2 x)
X, Y: C
Hsub: ∀ a : A, P a → P2 a
filter P X ⊆ filter P2 X
Proof.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
P, P2: A → Prop
H7: ∀ x : A, Decision (P x)
H8: ∀ x : A, Decision (P2 x)
X, Y: C
Hsub: ∀ a : A, P a → P2 a
filter P X ⊆ filter P2 X
  intros a HaP.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
P, P2: A → Prop
H7: ∀ x : A, Decision (P x)
H8: ∀ x : A, Decision (P2 x)
X, Y: C
Hsub: ∀ a : A, P a → P2 a
a: A
HaP: a ∈ filter P X
a ∈ filter P2 X
  apply elem_of_filter in HaP.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
P, P2: A → Prop
H7: ∀ x : A, Decision (P x)
H8: ∀ x : A, Decision (P2 x)
X, Y: C
Hsub: ∀ a : A, P a → P2 a
a: A
HaP: P a ∧ a ∈ X
a ∈ filter P2 X
  apply elem_of_filter.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
P, P2: A → Prop
H7: ∀ x : A, Decision (P x)
H8: ∀ x : A, Decision (P2 x)
X, Y: C
Hsub: ∀ a : A, P a → P2 a
a: A
HaP: P a ∧ a ∈ X
P2 a ∧ a ∈ X
  by itauto.
Qed.

End sec_filter.

End sec_fin_set.

Section sec_map.

Context
  `{FinSet A C}
  `{FinSet B D}.

Lemma set_map_subset
  (f : A -> B)
  (X Y : C)
  (Hsub : X ⊆ Y) :
  set_map (D := D) f X ⊆ set_map (D := D) f Y.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
B, D: Type
H7: ElemOf B D
H8: Empty D
H9: Singleton B D
H10: Union D
H11: Intersection D
H12: Difference D
H13: Elements B D
EqDecision1: EqDecision B
H14: FinSet B D
f: A → B
X, Y: C
Hsub: X ⊆ Y
set_map f X ⊆ set_map f Y
Proof.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
B, D: Type
H7: ElemOf B D
H8: Empty D
H9: Singleton B D
H10: Union D
H11: Intersection D
H12: Difference D
H13: Elements B D
EqDecision1: EqDecision B
H14: FinSet B D
f: A → B
X, Y: C
Hsub: X ⊆ Y
set_map f X ⊆ set_map f Y
  intros a Ha.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
B, D: Type
H7: ElemOf B D
H8: Empty D
H9: Singleton B D
H10: Union D
H11: Intersection D
H12: Difference D
H13: Elements B D
EqDecision1: EqDecision B
H14: FinSet B D
f: A → B
X, Y: C
Hsub: X ⊆ Y
a: B
Ha: a ∈ set_map f X
a ∈ set_map f Y
  apply elem_of_map in Ha.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
B, D: Type
H7: ElemOf B D
H8: Empty D
H9: Singleton B D
H10: Union D
H11: Intersection D
H12: Difference D
H13: Elements B D
EqDecision1: EqDecision B
H14: FinSet B D
f: A → B
X, Y: C
Hsub: X ⊆ Y
a: B
Ha: ∃ x : A, a = f x ∧ x ∈ X
a ∈ set_map f Y
  apply elem_of_map.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
B, D: Type
H7: ElemOf B D
H8: Empty D
H9: Singleton B D
H10: Union D
H11: Intersection D
H12: Difference D
H13: Elements B D
EqDecision1: EqDecision B
H14: FinSet B D
f: A → B
X, Y: C
Hsub: X ⊆ Y
a: B
Ha: ∃ x : A, a = f x ∧ x ∈ X
∃ x : A, a = f x ∧ x ∈ Y
  by firstorder.
Qed.

Lemma set_map_size_upper_bound
  (f : A -> B)
  (X : C) :
  size (set_map (D := D) f X) <= size X.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
B, D: Type
H7: ElemOf B D
H8: Empty D
H9: Singleton B D
H10: Union D
H11: Intersection D
H12: Difference D
H13: Elements B D
EqDecision1: EqDecision B
H14: FinSet B D
f: A → B
X: C
size (set_map f X) ≤ size X
Proof.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
B, D: Type
H7: ElemOf B D
H8: Empty D
H9: Singleton B D
H10: Union D
H11: Intersection D
H12: Difference D
H13: Elements B D
EqDecision1: EqDecision B
H14: FinSet B D
f: A → B
X: C
size (set_map f X) ≤ size X
  unfold set_map.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
B, D: Type
H7: ElemOf B D
H8: Empty D
H9: Singleton B D
H10: Union D
H11: Intersection D
H12: Difference D
H13: Elements B D
EqDecision1: EqDecision B
H14: FinSet B D
f: A → B
X: C
size (list_to_set (f <$> elements X)) ≤ size X
  remember (f <$> elements X) as fX.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
B, D: Type
H7: ElemOf B D
H8: Empty D
H9: Singleton B D
H10: Union D
H11: Intersection D
H12: Difference D
H13: Elements B D
EqDecision1: EqDecision B
H14: FinSet B D
f: A → B
X: C
fX: list B
HeqfX: fX = f <$> elements X
size (list_to_set fX) ≤ size X
  set (x := size (list_to_set _)).A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
B, D: Type
H7: ElemOf B D
H8: Empty D
H9: Singleton B D
H10: Union D
H11: Intersection D
H12: Difference D
H13: Elements B D
EqDecision1: EqDecision B
H14: FinSet B D
f: A → B
X: C
fX: list B
HeqfX: fX = f <$> elements X
x:= size (list_to_set fX): nat
x ≤ size X
  cut (x <= length fX); [| by apply list_to_set_size].A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
B, D: Type
H7: ElemOf B D
H8: Empty D
H9: Singleton B D
H10: Union D
H11: Intersection D
H12: Difference D
H13: Elements B D
EqDecision1: EqDecision B
H14: FinSet B D
f: A → B
X: C
fX: list B
HeqfX: fX = f <$> elements X
x:= size (list_to_set fX): nat
x ≤ length fX → x ≤ size X
  enough (length fX = size X) by lia.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
B, D: Type
H7: ElemOf B D
H8: Empty D
H9: Singleton B D
H10: Union D
H11: Intersection D
H12: Difference D
H13: Elements B D
EqDecision1: EqDecision B
H14: FinSet B D
f: A → B
X: C
fX: list B
HeqfX: fX = f <$> elements X
x:= size (list_to_set fX): nat
length fX = size X
  unfold size, set_size.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
B, D: Type
H7: ElemOf B D
H8: Empty D
H9: Singleton B D
H10: Union D
H11: Intersection D
H12: Difference D
H13: Elements B D
EqDecision1: EqDecision B
H14: FinSet B D
f: A → B
X: C
fX: list B
HeqfX: fX = f <$> elements X
x:= size (list_to_set fX): nat
length fX = (length ∘ elements) X
  simpl; subst fX.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
B, D: Type
H7: ElemOf B D
H8: Empty D
H9: Singleton B D
H10: Union D
H11: Intersection D
H12: Difference D
H13: Elements B D
EqDecision1: EqDecision B
H14: FinSet B D
f: A → B
X: C
x:= size (list_to_set (f <$> elements X)): nat
length (f <$> elements X) = length (elements X)
  by apply fmap_length.
Qed.

Lemma elem_of_set_map_inj (f : A -> B) `{!Inj (=) (=) f} (a : A) (X : C) :
  f a ∈@{D} fin_sets.set_map f X <-> a ∈ X.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
B, D: Type
H7: ElemOf B D
H8: Empty D
H9: Singleton B D
H10: Union D
H11: Intersection D
H12: Difference D
H13: Elements B D
EqDecision1: EqDecision B
H14: FinSet B D
f: A → B
Inj0: Inj eq eq f
a: A
X: C
f a ∈ set_map f X ↔ a ∈ X
Proof.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
B, D: Type
H7: ElemOf B D
H8: Empty D
H9: Singleton B D
H10: Union D
H11: Intersection D
H12: Difference D
H13: Elements B D
EqDecision1: EqDecision B
H14: FinSet B D
f: A → B
Inj0: Inj eq eq f
a: A
X: C
f a ∈ set_map f X ↔ a ∈ X
  intros; rewrite elem_of_map.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
B, D: Type
H7: ElemOf B D
H8: Empty D
H9: Singleton B D
H10: Union D
H11: Intersection D
H12: Difference D
H13: Elements B D
EqDecision1: EqDecision B
H14: FinSet B D
f: A → B
Inj0: Inj eq eq f
a: A
X: C
(∃ x : A, f a = f x ∧ x ∈ X) ↔ a ∈ X
  split; [| by eexists].A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
B, D: Type
H7: ElemOf B D
H8: Empty D
H9: Singleton B D
H10: Union D
H11: Intersection D
H12: Difference D
H13: Elements B D
EqDecision1: EqDecision B
H14: FinSet B D
f: A → B
Inj0: Inj eq eq f
a: A
X: C
(∃ x : A, f a = f x ∧ x ∈ X) → a ∈ X
  intros (_v & HeqAv & H_v).A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
B, D: Type
H7: ElemOf B D
H8: Empty D
H9: Singleton B D
H10: Union D
H11: Intersection D
H12: Difference D
H13: Elements B D
EqDecision1: EqDecision B
H14: FinSet B D
f: A → B
Inj0: Inj eq eq f
a: A
X: C
_v: A
HeqAv: f a = f _v
H_v: _v ∈ X
a ∈ X
  eapply inj in HeqAv; [| done].A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
B, D: Type
H7: ElemOf B D
H8: Empty D
H9: Singleton B D
H10: Union D
H11: Intersection D
H12: Difference D
H13: Elements B D
EqDecision1: EqDecision B
H14: FinSet B D
f: A → B
Inj0: Inj eq eq f
a: A
X: C
_v: A
H_v: _v ∈ X
HeqAv: a = _v
a ∈ X
  by subst.
Qed.

Lemma set_map_id (X : C) : X ≡ set_map id X.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
B, D: Type
H7: ElemOf B D
H8: Empty D
H9: Singleton B D
H10: Union D
H11: Intersection D
H12: Difference D
H13: Elements B D
EqDecision1: EqDecision B
H14: FinSet B D
X: C
X ≡ set_map id X
Proof.A, C: Type
H: ElemOf A C
H0: Empty C
H1: Singleton A C
H2: Union C
H3: Intersection C
H4: Difference C
H5: Elements A C
EqDecision0: EqDecision A
H6: FinSet A C
B, D: Type
H7: ElemOf B D
H8: Empty D
H9: Singleton B D
H10: Union D
H11: Intersection D
H12: Difference D
H13: Elements B D
EqDecision1: EqDecision B
H14: FinSet B D
X: C
X ≡ set_map id X by set_solver. Qed.

End sec_map.

Definition mmap_insert
  {I A SA : Type} {MI : Type -> Type}
  `{FinMap I MI} `{FinSet A SA} (i : I) (a : A) (m : MI SA) :=
  <[ i := {[ a ]} ∪ m !!! i ]> m.

Lemma elem_of_mmap_insert
  {I A SA : Type} {MI : Type -> Type}
  `{FinMap I MI} `{FinSet A SA} (m : MI SA) (i j : I) (a b : A) :
    b ∈ mmap_insert i a m !!! j <-> (a = b /\ i = j) \/ (b ∈ m !!! j).I, A, SA: Type
MI: Type → Type
H: FMap MI
H0: ∀ A : Type, Lookup I A (MI A)
H1: ∀ A : Type, Empty (MI A)
H2: ∀ A : Type, PartialAlter I A (MI A)
H3: OMap MI
H4: Merge MI
H5: ∀ A : Type, MapFold I A (MI A)
EqDecision0: EqDecision I
H6: FinMap I MI
H7: ElemOf A SA
H8: Empty SA
H9: Singleton A SA
H10: Union SA
H11: Intersection SA
H12: Difference SA
H13: Elements A SA
EqDecision1: EqDecision A
H14: FinSet A SA
m: MI SA
i, j: I
a, b: A
b ∈ mmap_insert i a m !!! j
↔ a = b ∧ i = j ∨ b ∈ m !!! j
Proof.I, A, SA: Type
MI: Type → Type
H: FMap MI
H0: ∀ A : Type, Lookup I A (MI A)
H1: ∀ A : Type, Empty (MI A)
H2: ∀ A : Type, PartialAlter I A (MI A)
H3: OMap MI
H4: Merge MI
H5: ∀ A : Type, MapFold I A (MI A)
EqDecision0: EqDecision I
H6: FinMap I MI
H7: ElemOf A SA
H8: Empty SA
H9: Singleton A SA
H10: Union SA
H11: Intersection SA
H12: Difference SA
H13: Elements A SA
EqDecision1: EqDecision A
H14: FinSet A SA
m: MI SA
i, j: I
a, b: A
b ∈ mmap_insert i a m !!! j
↔ a = b ∧ i = j ∨ b ∈ m !!! j
  unfold mmap_insert.I, A, SA: Type
MI: Type → Type
H: FMap MI
H0: ∀ A : Type, Lookup I A (MI A)
H1: ∀ A : Type, Empty (MI A)
H2: ∀ A : Type, PartialAlter I A (MI A)
H3: OMap MI
H4: Merge MI
H5: ∀ A : Type, MapFold I A (MI A)
EqDecision0: EqDecision I
H6: FinMap I MI
H7: ElemOf A SA
H8: Empty SA
H9: Singleton A SA
H10: Union SA
H11: Intersection SA
H12: Difference SA
H13: Elements A SA
EqDecision1: EqDecision A
H14: FinSet A SA
m: MI SA
i, j: I
a, b: A
b ∈ <[i:={[a]} ∪ m !!! i]> m !!! j
↔ a = b ∧ i = j ∨ b ∈ m !!! j
  destruct (decide (i = j)) as [<- | Hij].I, A, SA: Type
MI: Type → Type
H: FMap MI
H0: ∀ A : Type, Lookup I A (MI A)
H1: ∀ A : Type, Empty (MI A)
H2: ∀ A : Type, PartialAlter I A (MI A)
H3: OMap MI
H4: Merge MI
H5: ∀ A : Type, MapFold I A (MI A)
EqDecision0: EqDecision I
H6: FinMap I MI
H7: ElemOf A SA
H8: Empty SA
H9: Singleton A SA
H10: Union SA
H11: Intersection SA
H12: Difference SA
H13: Elements A SA
EqDecision1: EqDecision A
H14: FinSet A SA
m: MI SA
i: I
a, b: A
b ∈ <[i:={[a]} ∪ m !!! i]> m !!! i
↔ a = b ∧ i = i ∨ b ∈ m !!! i
I, A, SA: Type
MI: Type → Type
H: FMap MI
H0: ∀ A : Type, Lookup I A (MI A)
H1: ∀ A : Type, Empty (MI A)
H2: ∀ A : Type, PartialAlter I A (MI A)
H3: OMap MI
H4: Merge MI
H5: ∀ A : Type, MapFold I A (MI A)
EqDecision0: EqDecision I
H6: FinMap I MI
H7: ElemOf A SA
H8: Empty SA
H9: Singleton A SA
H10: Union SA
H11: Intersection SA
H12: Difference SA
H13: Elements A SA
EqDecision1: EqDecision A
H14: FinSet A SA
m: MI SA
i, j: I
a, b: A
Hij: i ≠ j
b ∈ <[i:={[a]} ∪ m !!! i]> m !!! j
↔ a = b ∧ i = j ∨ b ∈ m !!! j
  -I, A, SA: Type
MI: Type → Type
H: FMap MI
H0: ∀ A : Type, Lookup I A (MI A)
H1: ∀ A : Type, Empty (MI A)
H2: ∀ A : Type, PartialAlter I A (MI A)
H3: OMap MI
H4: Merge MI
H5: ∀ A : Type, MapFold I A (MI A)
EqDecision0: EqDecision I
H6: FinMap I MI
H7: ElemOf A SA
H8: Empty SA
H9: Singleton A SA
H10: Union SA
H11: Intersection SA
H12: Difference SA
H13: Elements A SA
EqDecision1: EqDecision A
H14: FinSet A SA
m: MI SA
i: I
a, b: A
b ∈ <[i:={[a]} ∪ m !!! i]> m !!! i
↔ a = b ∧ i = i ∨ b ∈ m !!! i rewrite lookup_total_insert.I, A, SA: Type
MI: Type → Type
H: FMap MI
H0: ∀ A : Type, Lookup I A (MI A)
H1: ∀ A : Type, Empty (MI A)
H2: ∀ A : Type, PartialAlter I A (MI A)
H3: OMap MI
H4: Merge MI
H5: ∀ A : Type, MapFold I A (MI A)
EqDecision0: EqDecision I
H6: FinMap I MI
H7: ElemOf A SA
H8: Empty SA
H9: Singleton A SA
H10: Union SA
H11: Intersection SA
H12: Difference SA
H13: Elements A SA
EqDecision1: EqDecision A
H14: FinSet A SA
m: MI SA
i: I
a, b: A
b ∈ {[a]} ∪ m !!! i ↔ a = b ∧ i = i ∨ b ∈ m !!! i
    by destruct (decide (a = b)); set_solver.
  -I, A, SA: Type
MI: Type → Type
H: FMap MI
H0: ∀ A : Type, Lookup I A (MI A)
H1: ∀ A : Type, Empty (MI A)
H2: ∀ A : Type, PartialAlter I A (MI A)
H3: OMap MI
H4: Merge MI
H5: ∀ A : Type, MapFold I A (MI A)
EqDecision0: EqDecision I
H6: FinMap I MI
H7: ElemOf A SA
H8: Empty SA
H9: Singleton A SA
H10: Union SA
H11: Intersection SA
H12: Difference SA
H13: Elements A SA
EqDecision1: EqDecision A
H14: FinSet A SA
m: MI SA
i, j: I
a, b: A
Hij: i ≠ j
b ∈ <[i:={[a]} ∪ m !!! i]> m !!! j
↔ a = b ∧ i = j ∨ b ∈ m !!! j rewrite lookup_total_insert_ne by done.I, A, SA: Type
MI: Type → Type
H: FMap MI
H0: ∀ A : Type, Lookup I A (MI A)
H1: ∀ A : Type, Empty (MI A)
H2: ∀ A : Type, PartialAlter I A (MI A)
H3: OMap MI
H4: Merge MI
H5: ∀ A : Type, MapFold I A (MI A)
EqDecision0: EqDecision I
H6: FinMap I MI
H7: ElemOf A SA
H8: Empty SA
H9: Singleton A SA
H10: Union SA
H11: Intersection SA
H12: Difference SA
H13: Elements A SA
EqDecision1: EqDecision A
H14: FinSet A SA
m: MI SA
i, j: I
a, b: A
Hij: i ≠ j
b ∈ m !!! j ↔ a = b ∧ i = j ∨ b ∈ m !!! j
    by set_solver.
Qed.