From 7df59d8b12e31e00e4870938fd4596cb91f73501 Mon Sep 17 00:00:00 2001 From: Jeremy Avigad Date: Thu, 6 Aug 2015 16:43:18 -0400 Subject: [PATCH] feat(library/data/set/finite): add more finiteness facts --- library/data/finset/to_set.lean | 7 +- library/data/set/basic.lean | 8 +- library/data/set/finite.lean | 195 ++++++++++++++++++++++++++------ 3 files changed, 173 insertions(+), 37 deletions(-) diff --git a/library/data/finset/to_set.lean b/library/data/finset/to_set.lean index 3c7d3d2cb4..4b5edb4c06 100644 --- a/library/data/finset/to_set.lean +++ b/library/data/finset/to_set.lean @@ -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 diff --git a/library/data/set/basic.lean b/library/data/set/basic.lean index 8105d3e77f..f0e14f3f0a 100644 --- a/library/data/set/basic.lean +++ b/library/data/set/basic.lean @@ -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} := diff --git a/library/data/set/finite.lean b/library/data/set/finite.lean index c94a99280d..788a659cc4 100644 --- a/library/data/set/finite.lean +++ b/library/data/set/finite.lean @@ -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