lean2/library/data/set/finite.lean

316 lines
13 KiB
Text
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

/-
Copyright (c) 2015 Jeremy Avigad. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
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.card logic.choice
open nat
variable {A : Type}
namespace set
definition finite [class] (s : set A) : Prop := ∃ (s' : finset A), s = finset.to_set s'
theorem finite_finset [instance] (s : finset A) : finite (finset.to_set s) :=
exists.intro s rfl
/- to finset: casts every set to a finite set -/
noncomputable definition to_finset (s : set A) : finset A :=
if fins : finite s then some fins else finset.empty
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_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 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) :=
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 (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 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 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 (to_finset s))
(by rewrite [finset.to_set_filter, *to_set_to_finset])
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 (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)
theorem finite_upto [instance] (n : ) : finite {i | i < n} :=
by rewrite [-finset.to_set_upto n]; apply finite_finset
theorem to_finset_upto (n : ) : to_finset {i | i < n} = finset.upto n :=
by apply (to_finset_eq_of_to_set_eq !finset.to_set_upto)
-- 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) [fins : 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
/- cardinality -/
noncomputable definition card (s : set A) := finset.card (set.to_finset s)
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]
/- Note: the induction tactic does not work well with the set induction principle with the
extra predicate "finite". -/
theorem eq_empty_of_card_eq_zero {s : set A} [fins : finite s] : card s = 0 → s = ∅ :=
induction_on_finite s
(by intro H; exact rfl)
(begin
intro a s' fins' anins IH H,
rewrite (card_insert_of_not_mem anins) at H,
apply nat.no_confusion H
end)
theorem card_upto (n : ) : card {i | i < n} = n :=
by rewrite [↑card, to_finset_upto, finset.card_upto]
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_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
theorem card_union (s₁ s₂ : set A) [fins₁ : finite s₁] [fins₂ : finite s₂] :
card (s₁ s₂) = card s₁ + card s₂ - card (s₁ ∩ s₂) :=
calc
card (s₁ s₂) = card (s₁ s₂) + card (s₁ ∩ s₂) - card (s₁ ∩ s₂) : add_sub_cancel
... = card s₁ + card s₂ - card (s₁ ∩ s₂) : card_add_card s₁ s₂
theorem card_union_of_disjoint {s₁ s₂ : set A} [fins₁ : finite s₁] [fins₂ : finite s₂] (H : s₁ ∩ s₂ = ∅) :
card (s₁ s₂) = card s₁ + card s₂ :=
by rewrite [card_union, H, card_empty]
theorem card_eq_card_add_card_diff {s₁ s₂ : set A} [fins₁ : finite s₁] [fins₂ : finite s₂] (H : s₁ ⊆ s₂) :
card s₂ = card s₁ + card (s₂ \ s₁) :=
have H1 : s₁ ∩ (s₂ \ s₁) = ∅,
from eq_empty_of_forall_not_mem (take x, assume H, (and.right (and.right H)) (and.left H)),
have s₂ = s₁ (s₂ \ s₁), from eq.symm (union_diff_cancel H),
calc
card s₂ = card (s₁ (s₂ \ s₁)) : {this}
... = card s₁ + card (s₂ \ s₁) : card_union_of_disjoint H1
theorem card_le_card_of_subset {s₁ s₂ : set A} [fins₁ : finite s₁] [fins₂ : finite s₂] (H : s₁ ⊆ s₂) :
card s₁ ≤ card s₂ :=
calc
card s₂ = card s₁ + card (s₂ \ s₁) : card_eq_card_add_card_diff H
... ≥ card s₁ : le_add_right
variable {B : Type}
theorem card_image_eq_of_inj_on {f : A → B} {s : set A} [fins : finite s] (injfs : inj_on f s) :
card (image f s) = card s :=
begin
rewrite [↑card, to_finset_image];
apply finset.card_image_eq_of_inj_on,
rewrite to_set_to_finset,
apply injfs
end
theorem card_le_of_inj_on (a : set A) (b : set B) [finb : finite b]
(Pex : ∃ f : A → B, inj_on f a ∧ (image f a ⊆ b)) :
card a ≤ card b :=
by_cases
(assume fina : finite a,
obtain f H, from Pex,
finset.card_le_of_inj_on (to_finset a) (to_finset b)
(exists.intro f
begin
rewrite [finset.subset_eq_to_set_subset, finset.to_set_image, *to_set_to_finset],
exact H
end))
(assume nfina : ¬ finite a,
by rewrite [card_of_not_finite nfina]; exact !zero_le)
theorem card_image_le (f : A → B) (s : set A) [fins : finite s] : card (image f s) ≤ card s :=
by rewrite [↑card, to_finset_image]; apply finset.card_image_le
theorem inj_on_of_card_image_eq {f : A → B} {s : set A} [fins : finite s]
(H : card (image f s) = card s) : inj_on f s :=
begin
rewrite -to_set_to_finset,
apply finset.inj_on_of_card_image_eq,
rewrite [-to_finset_to_set (finset.image _ _), finset.to_set_image, to_set_to_finset],
exact H
end
theorem card_pos_of_mem {a : A} {s : set A} [fins : finite s] (H : a ∈ s) : card s > 0 :=
have (#finset a ∈ to_finset s), by rewrite [finset.mem_eq_mem_to_set, to_set_to_finset]; apply H,
finset.card_pos_of_mem this
theorem eq_of_card_eq_of_subset {s₁ s₂ : set A} [fins₁ : finite s₁] [fins₂ : finite s₂]
(Hcard : card s₁ = card s₂) (Hsub : s₁ ⊆ s₂) :
s₁ = s₂ :=
begin
rewrite [-to_set_to_finset s₁, -to_set_to_finset s₂, -finset.eq_eq_to_set_eq],
apply finset.eq_of_card_eq_of_subset Hcard,
rewrite [to_finset_subset_to_finset_eq],
exact Hsub
end
theorem exists_two_of_card_gt_one {s : set A} (H : 1 < card s) : ∃ a b, a ∈ s ∧ b ∈ s ∧ a ≠ b :=
assert fins : finite s, from
by_contradiction
(assume nfins, by rewrite [card_of_not_finite nfins at H]; apply !not_succ_le_zero H),
by rewrite [-to_set_to_finset s]; apply finset.exists_two_of_card_gt_one H
end set