diff --git a/library/algebra/group_set_bigops.lean b/library/algebra/group_set_bigops.lean index d4c75463f..3a3dc4196 100644 --- a/library/algebra/group_set_bigops.lean +++ b/library/algebra/group_set_bigops.lean @@ -82,6 +82,8 @@ section Sum notation `∑` binders `∈` s, r:(scoped f, Sum s f) := r theorem Sum_empty (f : A → B) : Sum ∅ f = 0 := Prod_empty f + theorem Sum_of_not_finite {s : set A} (nfins : ¬ finite s) (f : A → B) : Sum s f = 0 := + Prod_of_not_finite nfins f theorem Sum_add (s : set A) (f g : A → B) : Sum s (λx, f x + g x) = Sum s f + Sum s g := Prod_mul s f g diff --git a/library/data/encodable.lean b/library/data/encodable.lean index 596619c1a..a4fae3e58 100644 --- a/library/data/encodable.lean +++ b/library/data/encodable.lean @@ -6,7 +6,7 @@ Author: Leonardo de Moura Type class for encodable types. Note that every encodable type is countable. -/ -import data.fintype data.list data.sum data.nat data.subtype data.countable data.equiv +import data.fintype data.list data.sum data.nat.div data.subtype data.countable data.equiv open option list nat function structure encodable [class] (A : Type) := @@ -72,7 +72,7 @@ theorem decode_encode_sum : ∀ s : sum A B, decode_sum (encode_sum s) = some s assert aux : 2 > 0, from dec_trivial, begin esimp [encode_sum, decode_sum], - rewrite [mul_mod_right, if_pos (eq.refl 0), mul_div_cancel_left _ aux, encodable.encodek] + rewrite [mul_mod_right, if_pos (eq.refl (0 : nat)), mul_div_cancel_left _ aux, encodable.encodek] end | (sum.inr b) := assert aux₁ : 2 > 0, from dec_trivial, diff --git a/library/data/nat/bigops.lean b/library/data/nat/bigops.lean index aa188ae31..5dd70a54e 100644 --- a/library/data/nat/bigops.lean +++ b/library/data/nat/bigops.lean @@ -5,8 +5,8 @@ Author: Jeremy Avigad Finite products and sums on the natural numbers. -/ -import data.nat.basic data.nat.order algebra.group_bigops -open list finset +import data.nat.basic data.nat.order algebra.group_bigops algebra.group_set_bigops +open list namespace nat open [classes] algebra @@ -36,9 +36,10 @@ section deceqA theorem Prodl_one (l : list A) : Prodl l (λ x, nat.succ 0) = 1 := algebra.Prodl_one l end deceqA -/- Prod -/ +/- Prod over finset -/ namespace finset +open finset definition Prod (s : finset A) (f : A → nat) : nat := algebra.finset.Prod s f notation `∏` binders `∈` s, r:(scoped f, Prod s f) := r @@ -61,6 +62,32 @@ end deceqA end finset +/- Prod over set -/ + +namespace set +open set + +noncomputable definition Prod (s : set A) (f : A → nat) : nat := algebra.set.Prod s f +notation `∏` binders `∈` s, r:(scoped f, Prod s f) := r + +theorem Prod_empty (f : A → nat) : Prod ∅ f = 1 := algebra.set.Prod_empty f +theorem Prod_of_not_finite {s : set A} (nfins : ¬ finite s) (f : A → nat) : Prod s f = 1 := + algebra.set.Prod_of_not_finite nfins f +theorem Prod_mul (s : set A) (f g : A → nat) : Prod s (λx, f x * g x) = Prod s f * Prod s g := + algebra.set.Prod_mul s f g +theorem Prod_insert_of_mem (f : A → nat) {a : A} {s : set A} (H : a ∈ s) : + Prod (insert a s) f = Prod s f := algebra.set.Prod_insert_of_mem f H +theorem Prod_insert_of_not_mem (f : A → nat) {a : A} {s : set A} [fins : finite s] (H : a ∉ s) : + Prod (insert a s) f = f a * Prod s f := algebra.set.Prod_insert_of_not_mem f H +theorem Prod_union (f : A → nat) {s₁ s₂ : set A} [fins₁ : finite s₁] [fins₂ : finite s₂] + (disj : s₁ ∩ s₂ = ∅) : + Prod (s₁ ∪ s₂) f = Prod s₁ f * Prod s₂ f := algebra.set.Prod_union f disj +theorem Prod_ext {s : set A} {f g : A → nat} (H : ∀x, x ∈ s → f x = g x) : + Prod s f = Prod s g := algebra.set.Prod_ext H +theorem Prod_one (s : set A) : Prod s (λ x, nat.succ 0) = 1 := algebra.set.Prod_one s + +end set + /- Suml -/ definition Suml (l : list A) (f : A → nat) : nat := algebra.Suml l f @@ -84,10 +111,10 @@ section deceqA theorem Suml_zero (l : list A) : Suml l (λ x, zero) = 0 := algebra.Suml_zero l end deceqA -/- Sum -/ +/- Sum over a finset -/ namespace finset - +open finset definition Sum (s : finset A) (f : A → nat) : nat := algebra.finset.Sum s f notation `∑` binders `∈` s, r:(scoped f, Sum s f) := r @@ -109,4 +136,30 @@ end deceqA end finset +/- Sum over a set -/ + +namespace set +open set + +noncomputable definition Sum (s : set A) (f : A → nat) : nat := algebra.set.Sum s f +notation `∏` binders `∈` s, r:(scoped f, Sum s f) := r + +theorem Sum_empty (f : A → nat) : Sum ∅ f = 0 := algebra.set.Sum_empty f +theorem Sum_of_not_finite {s : set A} (nfins : ¬ finite s) (f : A → nat) : Sum s f = 0 := + algebra.set.Sum_of_not_finite nfins f +theorem Sum_add (s : set A) (f g : A → nat) : Sum s (λx, f x + g x) = Sum s f + Sum s g := + algebra.set.Sum_add s f g +theorem Sum_insert_of_mem (f : A → nat) {a : A} {s : set A} (H : a ∈ s) : + Sum (insert a s) f = Sum s f := algebra.set.Sum_insert_of_mem f H +theorem Sum_insert_of_not_mem (f : A → nat) {a : A} {s : set A} [fins : finite s] (H : a ∉ s) : + Sum (insert a s) f = f a + Sum s f := algebra.set.Sum_insert_of_not_mem f H +theorem Sum_union (f : A → nat) {s₁ s₂ : set A} [fins₁ : finite s₁] [fins₂ : finite s₂] + (disj : s₁ ∩ s₂ = ∅) : + Sum (s₁ ∪ s₂) f = Sum s₁ f + Sum s₂ f := algebra.set.Sum_union f disj +theorem Sum_ext {s : set A} {f g : A → nat} (H : ∀x, x ∈ s → f x = g x) : + Sum s f = Sum s g := algebra.set.Sum_ext H +theorem Sum_zero (s : set A) : Sum s (λ x, 0) = 0 := algebra.set.Sum_zero s + +end set + end nat diff --git a/library/data/set/card.lean b/library/data/set/card.lean new file mode 100644 index 000000000..8afb5d98a --- /dev/null +++ b/library/data/set/card.lean @@ -0,0 +1,150 @@ +/- +Copyright (c) 2015 Jeremy Avigad. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: Jeremy Avigad + +Cardinality of finite sets. +-/ +import .finite data.finset.card +open nat + +namespace set + +variable {A : Type} + +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 diff --git a/library/data/set/default.lean b/library/data/set/default.lean index 2169b5d1d..aa8656dc0 100644 --- a/library/data/set/default.lean +++ b/library/data/set/default.lean @@ -3,4 +3,4 @@ Copyright (c) 2014 Jeremy Avigad. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: Jeremy Avigad -/ -import .basic .function .map .finite +import .basic .function .map .finite .card diff --git a/library/data/set/finite.lean b/library/data/set/finite.lean index 4616e702d..69c2720e6 100644 --- a/library/data/set/finite.lean +++ b/library/data/set/finite.lean @@ -7,7 +7,7 @@ The notion of "finiteness" for sets. This approach is not computational: for exa 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 +import data.set.function data.finset.to_set logic.choice open nat variable {A : Type} @@ -176,141 +176,4 @@ theorem induction_on_finite {P : set A → Prop} (s : set A) [fins : finite 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 diff --git a/library/data/set/set.md b/library/data/set/set.md index 5a5c4e173..77fa25ccd 100644 --- a/library/data/set/set.md +++ b/library/data/set/set.md @@ -8,4 +8,5 @@ Subsets of an arbitrary type. * [function](function.lean) : functions from one set to another * [map](map.lean) : set functions bundled with their domain and codomain * [finite](finite.lean) : the "finite" predicate on sets +* [card](card.lean) : cardinality (for finite sets) * [classical_inverse](classical_inverse.lean) : inverse functions, defined classically \ No newline at end of file