feat(library/data/set/finite): add more finiteness facts
This commit is contained in:
Jeremy Avigad
Leonardo de Moura
parent
eb181485eb
commit
7df59d8b12
3 changed files with 173 additions and 37 deletions
|
|
@ -67,10 +67,11 @@ theorem to_set_image {B : Type} [h : decidable_eq B] (f : A → B) (s : finset A
|
|||
definition decidable_mem_to_set [instance] (x : A) (s : finset A) : decidable (x ∈ ts s) :=
|
||||
decidable_of_decidable_of_eq _ !mem_eq_mem_to_set
|
||||
|
||||
theorem eq_of_to_set_eq_to_set {s t : finset A} (H : to_set s = to_set t) : s = t :=
|
||||
ext (take x, by rewrite [mem_eq_mem_to_set s, H])
|
||||
|
||||
theorem eq_eq_to_set_eq : (s = t) = (ts s = ts t) :=
|
||||
propext (iff.intro
|
||||
(assume H, H ▸ rfl)
|
||||
(assume H, ext (take x, by rewrite [mem_eq_mem_to_set s, H])))
|
||||
propext (iff.intro (assume H, H ▸ rfl) !eq_of_to_set_eq_to_set)
|
||||
|
||||
definition decidable_to_set_eq [instance] (s t : finset A) : decidable (ts s = ts t) :=
|
||||
decidable_of_decidable_of_eq _ !eq_eq_to_set_eq
|
||||
|
|
|
|||
|
|
@ -178,10 +178,16 @@ notation `{` binder `|` r:(scoped:1 P, set_of P) `}` := r
|
|||
definition filter (P : X → Prop) (s : set X) : set X := λx, x ∈ s ∧ P x
|
||||
notation `{` binder ∈ s `|` r:(scoped:1 p, filter p s) `}` := r
|
||||
|
||||
-- '{x, y, z}
|
||||
/- insert -/
|
||||
|
||||
definition insert (x : X) (a : set X) : set X := {y : X | y = x ∨ y ∈ a}
|
||||
|
||||
-- '{x, y, z}
|
||||
notation `'{`:max a:(foldr `,` (x b, insert x b) ∅) `}`:0 := a
|
||||
|
||||
theorem subset_insert (x : X) (a : set X) : a ⊆ insert x a :=
|
||||
take y, assume ys, or.inr ys
|
||||
|
||||
/- filter -/
|
||||
|
||||
theorem eq_filter_of_subset {s t : set X} (ssubt : s ⊆ t) : s = {x ∈ t | x ∈ s} :=
|
||||
|
|
|
|||
|
|
@ -6,10 +6,9 @@ Author: Jeremy Avigad
|
|||
The notion of "finiteness" for sets. This approach is not computational: for example, just because
|
||||
an element s : set A satsifies finite s doesn't mean that we can compute the cardinality. For
|
||||
a computational representation, use the finset type.
|
||||
|
||||
-/
|
||||
import data.set.function data.finset logic.choice
|
||||
open [coercions] finset nat
|
||||
open nat
|
||||
|
||||
variable {A : Type}
|
||||
|
||||
|
|
@ -17,80 +16,210 @@ namespace set
|
|||
|
||||
definition finite [class] (s : set A) : Prop := ∃ (s' : finset A), s = finset.to_set s'
|
||||
|
||||
theorem finite_of_finset [instance] (s : finset A) : finite s :=
|
||||
theorem finite_finset [instance] (s : finset A) : finite (finset.to_set s) :=
|
||||
exists.intro s rfl
|
||||
|
||||
noncomputable definition finset_of_finite (s : set A) [fins : finite s] : finset A := some fins
|
||||
/- to finset: casts every set to a finite set -/
|
||||
|
||||
theorem to_set_of_finset_of_finite (s : set A) [fins : finite s] :
|
||||
finset.to_set (finset_of_finite s) = s :=
|
||||
eq.symm (some_spec fins)
|
||||
|
||||
-- this casts every set to a finite set
|
||||
noncomputable definition to_finset (s : set A) : finset A :=
|
||||
if fins : finite s then finset_of_finite s else finset.empty
|
||||
if fins : finite s then some fins else finset.empty
|
||||
|
||||
theorem to_set_of_to_finset_of_finite (s : set A) [fins : finite s] :
|
||||
finset.to_set (to_finset s) = s :=
|
||||
by rewrite [↑set.to_finset, dif_pos fins]; apply to_set_of_finset_of_finite
|
||||
theorem to_finset_of_not_finite {s : set A} (nfins : ¬ finite s) : to_finset s = (#finset ∅) :=
|
||||
by rewrite [↑to_finset, dif_neg nfins]
|
||||
|
||||
theorem to_set_of_to_finset_of_not_finite {s : set A} (nfins : ¬ finite s) : to_finset s = ∅ :=
|
||||
by rewrite [↑set.to_finset, dif_neg nfins]
|
||||
theorem to_set_to_finset (s : set A) [fins : finite s] : finset.to_set (to_finset s) = s :=
|
||||
by rewrite [↑to_finset, dif_pos fins]; exact eq.symm (some_spec fins)
|
||||
|
||||
theorem to_finset_of_to_set (s : finset A) : to_finset (finset.to_set s) = s :=
|
||||
by rewrite [finset.eq_eq_to_set_eq, to_set_of_to_finset_of_finite s]
|
||||
theorem mem_to_finset_eq (a : A) (s : set A) [fins : finite s] :
|
||||
(#finset a ∈ to_finset s) = (a ∈ s) :=
|
||||
by rewrite [-to_set_to_finset at {2}]
|
||||
|
||||
theorem to_set_to_finset_of_not_finite {s : set A} (nfins : ¬ finite s) :
|
||||
finset.to_set (to_finset s) = ∅ :=
|
||||
by rewrite [to_finset_of_not_finite nfins]
|
||||
|
||||
theorem to_finset_to_set (s : finset A) : to_finset (finset.to_set s) = s :=
|
||||
by rewrite [finset.eq_eq_to_set_eq, to_set_to_finset (finset.to_set s)]
|
||||
|
||||
theorem to_finset_eq_of_to_set_eq {s : set A} {t : finset A} (H : finset.to_set t = s) :
|
||||
to_finset s = t :=
|
||||
finset.eq_of_to_set_eq_to_set (by subst [s]; rewrite to_finset_to_set)
|
||||
|
||||
/- finiteness -/
|
||||
|
||||
theorem finite_of_to_set_to_finset_eq {s : set A} (H : finset.to_set (to_finset s) = s) :
|
||||
finite s :=
|
||||
by rewrite -H; apply finite_finset
|
||||
|
||||
theorem finite_empty [instance] : finite (∅ : set A) :=
|
||||
exists.intro finset.empty (by rewrite [finset.to_set_empty])
|
||||
by rewrite [-finset.to_set_empty]; apply finite_finset
|
||||
|
||||
theorem to_finset_empty : to_finset (∅ : set A) = (#finset ∅) :=
|
||||
to_finset_eq_of_to_set_eq !finset.to_set_empty
|
||||
|
||||
theorem finite_insert [instance] (a : A) (s : set A) [fins : finite s] : finite (insert a s) :=
|
||||
exists.intro (finset.insert a (finset_of_finite s))
|
||||
(by rewrite [finset.to_set_insert, to_set_of_finset_of_finite])
|
||||
exists.intro (finset.insert a (to_finset s))
|
||||
(by rewrite [finset.to_set_insert, to_set_to_finset])
|
||||
|
||||
theorem to_finset_insert (a : A) (s : set A) [fins : finite s] :
|
||||
to_finset (insert a s) = finset.insert a (to_finset s) :=
|
||||
by apply to_finset_eq_of_to_set_eq; rewrite [finset.to_set_insert, to_set_to_finset]
|
||||
|
||||
example : finite '{1, 2, 3} := _
|
||||
|
||||
theorem finite_union [instance] (s t : set A) [fins : finite s] [fint : finite t] :
|
||||
finite (s ∪ t) :=
|
||||
exists.intro (#finset finset_of_finite s ∪ finset_of_finite t)
|
||||
(by rewrite [finset.to_set_union, *to_set_of_finset_of_finite])
|
||||
exists.intro (#finset to_finset s ∪ to_finset t)
|
||||
(by rewrite [finset.to_set_union, *to_set_to_finset])
|
||||
|
||||
theorem to_finset_union (s t : set A) [fins : finite s] [fint : finite t] :
|
||||
to_finset (s ∪ t) = (#finset to_finset s ∪ to_finset t) :=
|
||||
by apply to_finset_eq_of_to_set_eq; rewrite [finset.to_set_union, *to_set_to_finset]
|
||||
|
||||
theorem finite_inter [instance] (s t : set A) [fins : finite s] [fint : finite t] :
|
||||
finite (s ∩ t) :=
|
||||
exists.intro (#finset finset_of_finite s ∩ finset_of_finite t)
|
||||
(by rewrite [finset.to_set_inter, *to_set_of_finset_of_finite])
|
||||
exists.intro (#finset to_finset s ∩ to_finset t)
|
||||
(by rewrite [finset.to_set_inter, *to_set_to_finset])
|
||||
|
||||
theorem to_finset_inter (s t : set A) [fins : finite s] [fint : finite t] :
|
||||
to_finset (s ∩ t) = (#finset to_finset s ∩ to_finset t) :=
|
||||
by apply to_finset_eq_of_to_set_eq; rewrite [finset.to_set_inter, *to_set_to_finset]
|
||||
|
||||
theorem finite_filter [instance] (s : set A) (p : A → Prop) [h : decidable_pred p]
|
||||
[fins : finite s] :
|
||||
finite {x ∈ s | p x} :=
|
||||
exists.intro (finset.filter p (finset_of_finite s))
|
||||
(by rewrite [finset.to_set_filter, *to_set_of_finset_of_finite])
|
||||
exists.intro (finset.filter p (to_finset s))
|
||||
(by rewrite [finset.to_set_filter, *to_set_to_finset])
|
||||
|
||||
theorem finite_image [instance] {B : Type} [h : decidable_eq B] (f : A → B) (s : finset A)
|
||||
theorem to_finset_filter (s : set A) (p : A → Prop) [h : decidable_pred p] [fins : finite s] :
|
||||
to_finset {x ∈ s | p x} = (#finset {x ∈ to_finset s | p x}) :=
|
||||
by apply to_finset_eq_of_to_set_eq; rewrite [finset.to_set_filter, to_set_to_finset]
|
||||
|
||||
theorem finite_image [instance] {B : Type} [h : decidable_eq B] (f : A → B) (s : set A)
|
||||
[fins : finite s] :
|
||||
finite (f '[s]) :=
|
||||
exists.intro (finset.image f (finset_of_finite s))
|
||||
(by rewrite [finset.to_set_image, *to_set_of_finset_of_finite])
|
||||
exists.intro (finset.image f (to_finset s))
|
||||
(by rewrite [finset.to_set_image, *to_set_to_finset])
|
||||
|
||||
theorem to_finset_image {B : Type} [h : decidable_eq B] (f : A → B) (s : set A)
|
||||
[fins : finite s] :
|
||||
to_finset (f '[s]) = (#finset f '[to_finset s]) :=
|
||||
by apply to_finset_eq_of_to_set_eq; rewrite [finset.to_set_image, to_set_to_finset]
|
||||
|
||||
theorem finite_diff [instance] (s t : set A) [fins : finite s] : finite (s \ t) :=
|
||||
!finite_filter
|
||||
|
||||
theorem to_finset_diff (s t : set A) [fins : finite s] [fint : finite t] :
|
||||
to_finset (s \ t) = (#finset to_finset s \ to_finset t) :=
|
||||
by apply to_finset_eq_of_to_set_eq; rewrite [finset.to_set_diff, *to_set_to_finset]
|
||||
|
||||
theorem finite_subset {s t : set A} [fint : finite t] (ssubt : s ⊆ t) : finite s :=
|
||||
by rewrite (eq_filter_of_subset ssubt); apply finite_filter
|
||||
|
||||
theorem to_finset_subset_to_finset_eq (s t : set A) [fins : finite s] [fint : finite t] :
|
||||
(#finset to_finset s ⊆ to_finset t) = (s ⊆ t) :=
|
||||
by rewrite [finset.subset_eq_to_set_subset, *to_set_to_finset]
|
||||
|
||||
theorem finite_of_finite_insert {s : set A} {a : A} (finias : finite (insert a s)) : finite s :=
|
||||
finite_subset (subset_insert a s)
|
||||
|
||||
-- question: how can I avoid the parenthesis in the notation below?
|
||||
-- this didn't work: notation `𝒫`:max s := powerset s, nor variants
|
||||
|
||||
theorem finite_powerset (s : set A) [fins : finite s] : finite (𝒫 s) :=
|
||||
assert H : (𝒫 s) = finset.to_set '[finset.to_set (#finset 𝒫 (to_finset s))],
|
||||
from setext (take t, iff.intro
|
||||
(suppose t ∈ 𝒫 s,
|
||||
assert t ⊆ s, from this,
|
||||
assert finite t, from finite_subset this,
|
||||
have (#finset to_finset t ∈ 𝒫 (to_finset s)),
|
||||
by rewrite [finset.mem_powerset_iff_subset, to_finset_subset_to_finset_eq]; apply `t ⊆ s`,
|
||||
mem_image this (by rewrite to_set_to_finset))
|
||||
(assume H',
|
||||
obtain t' [(tmem : (#finset t' ∈ 𝒫 (to_finset s))) (teq : finset.to_set t' = t)],
|
||||
from H',
|
||||
show t ⊆ s,
|
||||
begin
|
||||
rewrite [-teq, finset.mem_powerset_iff_subset at tmem, -to_set_to_finset s],
|
||||
rewrite -finset.subset_eq_to_set_subset, assumption
|
||||
end)),
|
||||
by rewrite H; apply finite_image
|
||||
|
||||
/- induction for finite sets -/
|
||||
|
||||
theorem induction_finite [recursor 6] {P : set A → Prop}
|
||||
(H1 : P ∅)
|
||||
(H2 : ∀ ⦃a : A⦄, ∀ {s : set A} [fins : finite s], a ∉ s → P s → P (insert a s)) :
|
||||
∀ (s : set A), finite s → P s :=
|
||||
begin
|
||||
intro s fins,
|
||||
rewrite [-to_set_to_finset s],
|
||||
generalize to_finset s,
|
||||
intro s',
|
||||
induction s' using finset.induction with a s' nains ih,
|
||||
{rewrite finset.to_set_empty, apply H1},
|
||||
rewrite [finset.to_set_insert],
|
||||
apply H2,
|
||||
{rewrite -finset.mem_eq_mem_to_set, assumption},
|
||||
exact ih
|
||||
end
|
||||
|
||||
theorem induction_on_finite {P : set A → Prop} (s : set A) (fins : finite s)
|
||||
(H1 : P ∅)
|
||||
(H2 : ∀ ⦃a : A⦄, ∀ {s : set A} [fins : finite s], a ∉ s → P s → P (insert a s)) :
|
||||
P s :=
|
||||
induction_finite H1 H2 s fins
|
||||
|
||||
/- cardinality -/
|
||||
|
||||
noncomputable definition card (s : set A) := finset.card (set.to_finset s)
|
||||
|
||||
theorem card_of_finset (s : finset A) : card s = finset.card s :=
|
||||
by rewrite [↑card, to_finset_of_to_set]
|
||||
theorem card_to_set (s : finset A) : card (finset.to_set s) = finset.card s :=
|
||||
by rewrite [↑card, to_finset_to_set]
|
||||
|
||||
theorem card_of_not_finite {s : set A} (nfins : ¬ finite s) : card s = 0 :=
|
||||
by rewrite [↑card, to_finset_of_not_finite nfins]
|
||||
|
||||
theorem card_empty : card (∅ : set A) = 0 :=
|
||||
by rewrite [-finset.to_set_empty, card_to_set]
|
||||
|
||||
theorem card_insert_of_mem {a : A} {s : set A} (H : a ∈ s) : card (insert a s) = card s :=
|
||||
if fins : finite s then
|
||||
(by rewrite [↑card, to_finset_insert, -mem_to_finset_eq at H, finset.card_insert_of_mem H])
|
||||
else
|
||||
(assert ¬ finite (insert a s), from suppose _, absurd (!finite_of_finite_insert this) fins,
|
||||
by rewrite [card_of_not_finite fins, card_of_not_finite this])
|
||||
|
||||
theorem card_insert_of_not_mem {a : A} {s : set A} [fins : finite s] (H : a ∉ s) :
|
||||
card (insert a s) = card s + 1 :=
|
||||
by rewrite [↑card, to_finset_insert, -mem_to_finset_eq at H, finset.card_insert_of_not_mem H]
|
||||
|
||||
theorem card_insert_le (a : A) (s : set A) [fins : finite s] :
|
||||
card (insert a s) ≤ card s + 1 :=
|
||||
if H : a ∈ s then by rewrite [card_insert_of_mem H]; apply le_succ
|
||||
else by rewrite [card_insert_of_not_mem H]
|
||||
|
||||
theorem card_singleton (a : A) : card '{a} = 1 :=
|
||||
by rewrite [card_insert_of_not_mem !not_mem_empty, card_empty]
|
||||
|
||||
/-
|
||||
-- TODO: get induction working somehow.
|
||||
set_option formatter.hide_full_terms false
|
||||
|
||||
theorem eq_empty_of_card_eq_zero {s : set A} [fins : finite s] (H : card s = 0) : s = ∅ :=
|
||||
begin
|
||||
induction s with a s' fins' anins IH,
|
||||
{rewrite card_empty at H},
|
||||
rewrite (card_insert_of_not_mem anins) at H,
|
||||
apply nat.no_confusion H,
|
||||
end
|
||||
-/
|
||||
|
||||
theorem card_add_card (s₁ s₂ : set A) [fins₁ : finite s₁] [fins₂ : finite s₂] :
|
||||
card s₁ + card s₂ = card (s₁ ∪ s₂) + card (s₁ ∩ s₂) :=
|
||||
begin
|
||||
rewrite [-to_set_of_to_finset_of_finite s₁, -to_set_of_to_finset_of_finite s₂],
|
||||
rewrite [-finset.to_set_union, -finset.to_set_inter, *card_of_finset],
|
||||
rewrite [-to_set_to_finset s₁, -to_set_to_finset s₂],
|
||||
rewrite [-finset.to_set_union, -finset.to_set_inter, *card_to_set],
|
||||
apply finset.card_add_card
|
||||
end
|
||||
|
||||
|
|
|
|||
Loading…
Reference in a new issue