diff --git a/algebra/big_operators.lean b/algebra/big_operators.lean index c94db282dcc4f..684a643ace638 100644 --- a/algebra/big_operators.lean +++ b/algebra/big_operators.lean @@ -5,70 +5,61 @@ Authors: Johannes Hölzl Some big operators for lists and finite sets. -/ -import algebra.group data.list data.list.comb algebra.group_power data.set.finite data.finset.basic +import algebra.group data.list data.list.comb algebra.group_power data.set.finite data.finset data.list.perm -open function list universes u v w variables {α : Type u} {β : Type v} {γ : Type w} -section foldl_semigroup -variable [semigroup α] +namespace list +-- move to list.sum, needs to match exactly, otherwise transport fails +definition prod [has_mul α] [has_one α] : list α → α := list.foldl (*) 1 -lemma foldl_mul_assoc : ∀{l : list α} {a₁ a₂}, l.foldl (*) (a₁ * a₂) = a₁ * l.foldl (*) a₂ -| [] a₁ a₂ := by simp -| (a :: l) a₁ a₂ := - calc (a::l).foldl (*) (a₁ * a₂) = l.foldl (*) (a₁ * (a₂ * a)) : by simp - ... = a₁ * (a::l).foldl (*) a₂ : by rw [foldl_mul_assoc]; simp +section monoid +variables [monoid α] {l l₁ l₂ : list α} {a : α} -lemma foldl_mul_eq_mul_foldr : - ∀{l : list α} {a₁ a₂}, l.foldl (*) a₁ * a₂ = a₁ * l.foldr (*) a₂ -| [] a₁ a₂ := by simp -| (a :: l) a₁ a₂ := by simp [foldl_mul_assoc]; rw [foldl_mul_eq_mul_foldr] +@[simp] theorem prod_nil : ([] : list α).prod = 1 := rfl -end foldl_semigroup +@[simp] theorem prod_cons : (a::l).prod = a * l.prod := +calc (a::l).prod = foldl (*) (a * 1) l : by simp [list.prod] + ... = _ : foldl_assoc -section list_prod_monoid -variable [monoid α] - -protected definition list.prod (l : list α) : α := l.foldl (*) 1 - -@[simp] theorem prod_nil : [].prod = 1 := rfl - -@[simp] theorem prod_cons {a : α} {l : list α} : (a::l).prod = a * l.prod := -by simp [list.prod, foldl_mul_assoc.symm] - -@[simp] theorem prod_append {l₁ l₂ : list α} : (l₁ ++ l₂).prod = l₁.prod * l₂.prod := -by simp [list.prod, foldl_mul_assoc.symm] +@[simp] theorem prod_append : (l₁ ++ l₂).prod = l₁.prod * l₂.prod := +calc (l₁ ++ l₂).prod = foldl (*) (foldl (*) 1 l₁ * 1) l₂ : by simp [list.prod] + ... = l₁.prod * l₂.prod : foldl_assoc @[simp] theorem prod_join {l : list (list α)} : l.join.prod = (l.map list.prod).prod := by induction l; simp [list.join, *] at * -@[simp] theorem prod_replicate {a : α} {n : ℕ} : (list.replicate n a).prod = a ^ n := +@[simp] theorem prod_replicate {n : ℕ} : (list.replicate n a).prod = a ^ n := begin induction n with n ih, { show [].prod = (1:α), refl }, { show (a :: list.replicate n a).prod = a ^ (n+1), simp [pow_succ, ih] } end -end list_prod_monoid +end monoid -section list_prod_comm_monoid +section comm_monoid +open list variable [comm_monoid α] lemma prod_eq_of_perm {l₁ l₂ : list α} (h : perm l₁ l₂) : l₁.prod = l₂.prod := by induction h; repeat { simp [*] } -end list_prod_comm_monoid +lemma prod_reverse {l : list α} : l.reverse.prod = l.prod := +prod_eq_of_perm $ perm.perm_rev_simp l + +end comm_monoid + +end list namespace finset section prod_comm_monoid +open list variables [comm_monoid β] (s : finset α) (f : α → β) -protected definition prod : β := -quot.lift_on s (λl, (l.val.map f).prod) $ - assume ⟨l₁, hl₁⟩ ⟨l₂, hl₂⟩ (h : perm l₁ l₂), show (l₁.map f).prod = (l₂.map f).prod, - from prod_eq_of_perm $ h.perm_map _ +protected definition prod : β := s.fold (*) 1 f variables {s f} {s₁ s₂ : finset α} @@ -76,43 +67,142 @@ variables {s f} {s₁ s₂ : finset α} variable [decidable_eq α] -@[simp] lemma prod_to_finset {l : list α} (h : nodup l) : (to_finset l).prod f = (l.map f).prod := -by rw [←to_finset_eq_of_nodup h]; refl +@[simp] lemma prod_to_finset_of_nodup {l : list α} (h : nodup l) : + (to_finset_of_nodup l h).prod f = (l.map f).prod := +fold_to_finset_of_nodup h -@[simp] lemma prod_insert {a : α} : a ∉ s → (insert a s).prod f = f a * s.prod f := -quot.induction_on s $ assume ⟨l, hl⟩ (h : a ∉ l), - show ((l.insert a).map f).prod = f a * (l.map f).prod, by simp [h, list.insert] +@[simp] lemma prod_insert {a : α} : a ∉ s → (insert a s).prod f = f a * s.prod f := fold_insert @[simp] lemma prod_singleton {a : α} : ({a}:finset α).prod f = f a := -by simp [singleton] - -lemma prod_union_inter_eq : - (s₁ ∪ s₂).prod f * (s₁ ∩ s₂).prod f = s₁.prod f * s₂.prod f := -s₁.induction_on - (by simp [empty_union, empty_inter]) - begin - intros a s ha ih, - by_cases a ∈ s₂ with h₂, - { have h' : a ∉ s ∩ s₂, from assume ha', ha $ mem_of_mem_inter_left ha', - have h'' : insert a s ∪ s₂ = s ∪ s₂, - { rw [←insert_union], exact insert_eq_of_mem (mem_union_right _ h₂) }, - simp [insert_inter_of_mem, h₂, h', h'', ih, ha] }, - { have h' : a ∉ s ∪ s₂, from assume h, (mem_or_mem_of_mem_union h).elim ha h₂, - rw [insert_inter_of_not_mem h₂, ←insert_union], - simp [h', ih, -mul_comm, ha] } - end +eq.trans fold_singleton (by simp) + +lemma prod_image [decidable_eq γ] {s : finset γ} {g : γ → α} : + (∀x∈s, ∀y∈s, g x = g y → x = y) → (s.image g).prod f = s.prod (λx, f (g x)) := +fold_image + +lemma prod_union_inter : (s₁ ∪ s₂).prod f * (s₁ ∩ s₂).prod f = s₁.prod f * s₂.prod f := +fold_union_inter lemma prod_union (h : s₁ ∩ s₂ = ∅) : (s₁ ∪ s₂).prod f = s₁.prod f * s₂.prod f := -by rw [←prod_union_inter_eq, h]; simp +by rw [←prod_union_inter, h]; simp lemma prod_mul_distrib {g : α → β} : s.prod (λx, f x * g x) = s.prod f * s.prod g := -s.induction_on (by simp) (by simp {contextual:=tt}) - -lemma prod_image [decidable_eq γ] {s : finset γ} {g : γ → α} : - (∀x∈s, ∀y∈s, g x = g y → x = y) → (s.image g).prod f = s.prod (λx, f (g x)) := -quot.induction_on s $ assume ⟨l, hl⟩ h, - show ((finset.to_finset_of_nodup l hl).image g).prod f = (l.map (f ∘ g)).prod, - by rw [←map_map, image_to_finset_of_nodup hl h]; refl +eq.trans (by simp; refl) fold_op_distrib end prod_comm_monoid end finset + +/- transport versions to additive -/ +-- TODO: change transport_multiplicative_to_additive to use attribute +run_cmd transport_multiplicative_to_additive [ + /- map operations -/ + (`has_mul.mul, `has_add.add), (`has_one.one, `has_zero.zero), (`has_inv.inv, `has_neg.neg), + (`has_mul, `has_add), (`has_one, `has_zero), (`has_inv, `has_neg), + /- map constructors -/ + (`has_mul.mk, `has_add.mk), (`has_one, `has_zero.mk), (`has_inv, `has_neg.mk), + /- map structures -/ + (`semigroup, `add_semigroup), + (`monoid, `add_monoid), + (`group, `add_group), + (`comm_semigroup, `add_comm_semigroup), + (`comm_monoid, `add_comm_monoid), + (`comm_group, `add_comm_group), + (`left_cancel_semigroup, `add_left_cancel_semigroup), + (`right_cancel_semigroup, `add_right_cancel_semigroup), + (`left_cancel_semigroup.mk, `add_left_cancel_semigroup.mk), + (`right_cancel_semigroup.mk, `add_right_cancel_semigroup.mk), + /- map instances -/ + (`semigroup.to_has_mul, `add_semigroup.to_has_add), + (`semigroup_to_is_associative, `add_semigroup_to_is_associative), + (`comm_semigroup_to_is_commutative, `add_comm_semigroup_to_is_commutative), + (`monoid.to_has_one, `add_monoid.to_has_zero), + (`group.to_has_inv, `add_group.to_has_neg), + (`comm_semigroup.to_semigroup, `add_comm_semigroup.to_add_semigroup), + (`monoid.to_semigroup, `add_monoid.to_add_semigroup), + (`comm_monoid.to_monoid, `add_comm_monoid.to_add_monoid), + (`comm_monoid.to_comm_semigroup, `add_comm_monoid.to_add_comm_semigroup), + (`group.to_monoid, `add_group.to_add_monoid), + (`comm_group.to_group, `add_comm_group.to_add_group), + (`comm_group.to_comm_monoid, `add_comm_group.to_add_comm_monoid), + (`left_cancel_semigroup.to_semigroup, `add_left_cancel_semigroup.to_add_semigroup), + (`right_cancel_semigroup.to_semigroup, `add_right_cancel_semigroup.to_add_semigroup), + /- map projections -/ + (`semigroup.mul_assoc, `add_semigroup.add_assoc), + (`comm_semigroup.mul_comm, `add_comm_semigroup.add_comm), + (`left_cancel_semigroup.mul_left_cancel, `add_left_cancel_semigroup.add_left_cancel), + (`right_cancel_semigroup.mul_right_cancel, `add_right_cancel_semigroup.add_right_cancel), + (`monoid.one_mul, `add_monoid.zero_add), + (`monoid.mul_one, `add_monoid.add_zero), + (`group.mul_left_inv, `add_group.add_left_neg), + (`group.mul, `add_group.add), + (`group.mul_assoc, `add_group.add_assoc), + /- map lemmas -/ + (`mul_assoc, `add_assoc), + (`mul_comm, `add_comm), + (`mul_left_comm, `add_left_comm), + (`mul_right_comm, `add_right_comm), + (`one_mul, `zero_add), + (`mul_one, `add_zero), + (`mul_left_inv, `add_left_neg), + (`mul_left_cancel, `add_left_cancel), + (`mul_right_cancel, `add_right_cancel), + (`mul_left_cancel_iff, `add_left_cancel_iff), + (`mul_right_cancel_iff, `add_right_cancel_iff), + (`inv_mul_cancel_left, `neg_add_cancel_left), + (`inv_mul_cancel_right, `neg_add_cancel_right), + (`eq_inv_mul_of_mul_eq, `eq_neg_add_of_add_eq), + (`inv_eq_of_mul_eq_one, `neg_eq_of_add_eq_zero), + (`inv_inv, `neg_neg), + (`mul_right_inv, `add_right_neg), + (`mul_inv_cancel_left, `add_neg_cancel_left), + (`mul_inv_cancel_right, `add_neg_cancel_right), + (`mul_inv_rev, `neg_add_rev), + (`mul_inv, `neg_add), + (`inv_inj, `neg_inj), + (`group.mul_left_cancel, `add_group.add_left_cancel), + (`group.mul_right_cancel, `add_group.add_right_cancel), + (`group.to_left_cancel_semigroup, `add_group.to_left_cancel_add_semigroup), + (`group.to_right_cancel_semigroup, `add_group.to_right_cancel_add_semigroup), + (`eq_inv_of_eq_inv, `eq_neg_of_eq_neg), + (`eq_inv_of_mul_eq_one, `eq_neg_of_add_eq_zero), + (`eq_mul_inv_of_mul_eq, `eq_add_neg_of_add_eq), + (`inv_mul_eq_of_eq_mul, `neg_add_eq_of_eq_add), + (`mul_inv_eq_of_eq_mul, `add_neg_eq_of_eq_add), + (`eq_mul_of_mul_inv_eq, `eq_add_of_add_neg_eq), + (`eq_mul_of_inv_mul_eq, `eq_add_of_neg_add_eq), + (`mul_eq_of_eq_inv_mul, `add_eq_of_eq_neg_add), + (`mul_eq_of_eq_mul_inv, `add_eq_of_eq_add_neg), + (`one_inv, `neg_zero), + (`left_inverse_inv, `left_inverse_neg), + (`inv_eq_inv_iff_eq, `neg_eq_neg_iff_eq), + (`inv_eq_one_iff_eq_one, `neg_eq_zero_iff_eq_zero), + (`eq_one_of_inv_eq_one, `eq_zero_of_neg_eq_zero), + (`eq_inv_iff_eq_inv, `eq_neg_iff_eq_neg), + (`eq_of_mul_inv_eq_one, `eq_of_add_neg_eq_zero), + (`mul_eq_iff_eq_inv_mul, `add_eq_iff_eq_neg_add), + (`mul_eq_iff_eq_mul_inv, `add_eq_iff_eq_add_neg), + -- (`mul_eq_one_of_mul_eq_one, `add_eq_zero_of_add_eq_zero) not needed for commutative groups + -- (`muleq_one_iff_mul_eq_one, `add_eq_zero_iff_add_eq_zero) + + --NEW: + (`list.prod, `list.sum), + (`list.prod.equations._eqn_1, `list.sum.equations._eqn_1), + (`list.prod_nil, `list.sum_nil), + (`list.prod_cons, `list.sum_cons), + (`list.prod_append, `list.sum_append), + (`list.prod_join, `list.sum_join), + (`list.prod_eq_of_perm, `list.sum_eq_of_perm), + (`list.prod_reverse, `list.sum_reverse), + (`finset.prod._proof_1, `finset.sum._proof_1), + (`finset.prod._proof_2, `finset.sum._proof_2), + (`finset.prod, `finset.sum), + (`finset.prod.equations._eqn_1, `finset.sum.equations._eqn_1), + (`finset.prod_empty, `finset.sum_empty), + (`finset.prod_insert, `finset.sum_insert), + (`finset.prod_singleton, `finset.sum_singleton), + (`finset.prod_union_inter, `finset.sum_union_inter), + (`finset.prod_union, `finset.sum_union), + (`finset.prod_to_finset_of_nodup, `finset.sum_to_finset_of_nodup), + (`finset.prod_image, `finset.sum_image), + (`finset.prod_mul_distrib, `finset.sum_add_distrib) + ] diff --git a/data/finset/basic.lean b/data/finset/basic.lean index db880598c5dd6..ff93bec8a3d14 100644 --- a/data/finset/basic.lean +++ b/data/finset/basic.lean @@ -5,17 +5,20 @@ Author: Leonardo de Moura, Jeremy Avigad, Minchao Wu Finite sets. -/ - import data.list.set data.list.perm tactic.finish open list subtype nat -attribute [reducible] insert - universes u v w +variables {α : Type u} {β : Type v} {γ : Type w} -def nodup_list (α : Type u) := {l : list α // nodup l} +@[simp] lemma or_self_or (a b : Prop) : a ∨ a ∨ b ↔ a ∨ b := +calc a ∨ a ∨ b ↔ (a ∨ a) ∨ b : or.assoc.symm + ... ↔ _ : by rw [or_self] -variables {α : Type u} {β : Type v} {γ : Type w} +theorem perm_insert_cons_of_not_mem [decidable_eq α] {a : α} {l : list α} (h : a ∉ l) : perm (list.insert a l) (a :: l) := +have list.insert a l = a :: l, from if_neg h, by rw this + +def nodup_list (α : Type u) := {l : list α // nodup l} def to_nodup_list_of_nodup {l : list α} (n : nodup l) : nodup_list α := ⟨l, n⟩ @@ -48,6 +51,11 @@ namespace finset def to_finset_of_nodup (l : list α) (n : nodup l) : finset α := ⟦to_nodup_list_of_nodup n⟧ +@[elab_as_eliminator] +protected theorem induction_on_to_finset {α : Type u} {p : finset α → Prop} (s : finset α) + (h : ∀ (l : list α) (h : nodup l), p (to_finset_of_nodup l h)) : p s := +quot.induction_on s $ assume ⟨l, hl⟩, h l hl + def to_finset [decidable_eq α] (l : list α) : finset α := ⟦to_nodup_list l⟧ @@ -69,6 +77,8 @@ instance has_decidable_eq [decidable_eq α] : decidable_eq (finset α) := | decidable.is_false n := decidable.is_false (λ e : ⟦l₁⟧ = ⟦l₂⟧, absurd (quotient.exact e) n) end) +section mem + def mem (a : α) (s : finset α) : Prop := quot.lift_on s (λ l, a ∈ l.1) (λ l₁ l₂ (e : l₁ ~ l₂), propext (iff.intro @@ -77,6 +87,10 @@ quot.lift_on s (λ l, a ∈ l.1) instance : has_mem α (finset α) := ⟨mem⟩ +@[simp] lemma mem_to_finset_of_nodup_eq {a : α} {l : list α} (n : nodup l) : + (a ∈ to_finset_of_nodup l n) = (a ∈ l) := +rfl + theorem mem_of_mem_list {a : α} {l : nodup_list α} : a ∈ l.1 → a ∈ @id (finset α) ⟦l⟧ := λ ainl, ainl @@ -93,27 +107,72 @@ instance decidable_mem [h : decidable_eq α] : ∀ (a : α) (s : finset α), dec theorem mem_to_finset [decidable_eq α] {a : α} {l : list α} : a ∈ l → a ∈ to_finset l := λ ainl, mem_erase_dup.mpr ainl -theorem mem_to_finset_of_nodup {a : α} {l : list α} (n : nodup l) : a ∈ l → a ∈ to_finset_of_nodup l n := -λ ainl, ainl - /- extensionality -/ theorem ext {s₁ s₂ : finset α} : (∀ a, a ∈ s₁ ↔ a ∈ s₂) → s₁ = s₂ := quotient.induction_on₂ s₁ s₂ (λ l₁ l₂ e, quot.sound (perm.perm_ext l₁.2 l₂.2 e)) +end mem + +/- subset -/ +section subset +protected def subset (s₁ s₂ : finset α) : Prop := +quotient.lift_on₂ s₁ s₂ (λ l₁ l₂, l₁.1 ⊆ l₂.1) + (λ v₁ v₂ w₁ w₂ p₁ p₂, propext (iff.intro + (λ s₁ a i, perm.mem_of_perm p₂ (s₁ (perm.mem_of_perm (perm.symm p₁) i))) + (λ s₂ a i, perm.mem_of_perm (perm.symm p₂) (s₂ (perm.mem_of_perm p₁ i))))) + +instance : has_subset (finset α) := ⟨finset.subset⟩ + +-- theorem subset_univ [h : fintype α] (s : finset α) : s ⊆ univ := +-- quot.induction_on s (λ l a i, fintype.complete a) + +theorem subset.refl (s : finset α) : s ⊆ s := +quot.induction_on s (λ l, list.subset.refl l.1) + +theorem subset.trans {s₁ s₂ s₃ : finset α} : s₁ ⊆ s₂ → s₂ ⊆ s₃ → s₁ ⊆ s₃ := +quotient.induction_on₃ s₁ s₂ s₃ (λ l₁ l₂ l₃ h₁ h₂, list.subset.trans h₁ h₂) + +theorem mem_of_subset_of_mem {s₁ s₂ : finset α} {a : α} : s₁ ⊆ s₂ → a ∈ s₁ → a ∈ s₂ := +quotient.induction_on₂ s₁ s₂ (λ l₁ l₂ h₁ h₂, h₁ h₂) + +theorem subset.antisymm {s₁ s₂ : finset α} (H₁ : s₁ ⊆ s₂) (H₂ : s₂ ⊆ s₁) : s₁ = s₂ := +ext (λ x, iff.intro (λ H, mem_of_subset_of_mem H₁ H) (λ H, mem_of_subset_of_mem H₂ H)) + +theorem subset_of_forall {s₁ s₂ : finset α} : (∀x, x ∈ s₁ → x ∈ s₂) → s₁ ⊆ s₂ := +quotient.induction_on₂ s₁ s₂ (λ l₁ l₂ H, H) + +end subset + +section empty +variables {s : finset α} {a b : α} + /- empty -/ protected def empty : finset α := to_finset_of_nodup [] nodup_nil instance : has_emptyc (finset α) := ⟨finset.empty⟩ -@[simp] theorem not_mem_empty (a : α) : a ∉ (∅ : finset α) := -λ aine, aine +@[simp] theorem not_mem_empty : a ∉ (∅ : finset α) := λ aine, aine + +@[simp] theorem mem_empty_iff : a ∈ (∅ : finset α) ↔ false := iff_false_intro not_mem_empty + +theorem empty_subset : ∅ ⊆ s := quot.induction_on s (λ l, list.nil_subset l.1) + +theorem eq_empty_of_forall_not_mem (H : ∀x, x ∉ s) : s = ∅ := ext (λ x, iff_false_intro (H x)) + +theorem eq_empty_of_subset_empty (h : s ⊆ ∅) : s = ∅ := subset.antisymm h empty_subset + +theorem subset_empty_iff (x : finset α) : x ⊆ ∅ ↔ x = ∅ := +iff.intro eq_empty_of_subset_empty (λ xeq, by rw xeq; apply subset.refl ∅) -@[simp] theorem mem_empty_iff (x : α) : x ∈ (∅ : finset α) ↔ false := -iff_false_intro (not_mem_empty _) +theorem exists_mem_of_ne_empty : s ≠ ∅ → ∃ a : α, a ∈ s := +finset.induction_on_to_finset s $ assume l hl, + match l, hl with + | [] := assume _ h, false.elim $ h rfl + | (a :: l) := assume _ _, ⟨a, by simp⟩ + end -theorem eq_empty_of_forall_not_mem {s : finset α} (H : ∀x, x ∉ s) : s = ∅ := -ext (λ x, iff_false_intro (H x)) +end empty -- /- universe -/ -- def univ [h : fintype A] : finset A := @@ -124,21 +183,9 @@ ext (λ x, iff_false_intro (H x)) -- theorem mem_univ_eq [fintype A] (x : A) : x ∈ univ = true := propext (iff_true_intro !mem_univ) -/- card -/ -def card (s : finset α) : nat := -quot.lift_on s - (λ l, length l.1) - (λ l₁ l₂ p, perm.length_eq_length_of_perm p) - -theorem card_empty : card (∅ : finset α) = 0 := -rfl - -lemma ne_empty_of_card_eq_succ {s : finset α} {n : nat} : card s = succ n → s ≠ ∅ := -λ h hn, by rw hn at h; contradiction - /- insert -/ section insert -variable [decidable_eq α] +variables [decidable_eq α] {s t : finset α} {a b : α} protected def insert (a : α) (s : finset α) : finset α := quot.lift_on s @@ -147,180 +194,77 @@ quot.lift_on s instance : has_insert α (finset α) := ⟨finset.insert⟩ -theorem mem_insert (a : α) (s : finset α) : a ∈ insert a s := -quot.induction_on s - (λ l : nodup_list α, mem_to_finset_of_nodup _ (mem_insert_self _ _)) - -theorem mem_insert_of_mem {a : α} {s : finset α} (b : α) : a ∈ s → a ∈ insert b s := -quot.induction_on s - (λ (l : nodup_list α) (ainl : a ∈ ⟦l⟧), mem_to_finset_of_nodup _ (mem_insert_of_mem ainl)) - -theorem eq_or_mem_of_mem_insert {x a : α} {s : finset α} : x ∈ insert a s → x = a ∨ x ∈ s := -quot.induction_on s (λ l : nodup_list α, λ H, list.eq_or_mem_of_mem_insert H) - -theorem mem_of_mem_insert_of_ne {x a : α} {s : finset α} (xin : x ∈ insert a s) : x ≠ a → x ∈ s := -or_resolve_right (eq_or_mem_of_mem_insert xin) - -theorem mem_insert_iff (x a : α) (s : finset α) : x ∈ insert a s ↔ (x = a ∨ x ∈ s) := -iff.intro eq_or_mem_of_mem_insert - (λ h, or.elim h (λ l, by rw l; apply mem_insert) (λ r, mem_insert_of_mem _ r)) +@[simp] theorem mem_insert_iff : a ∈ insert b s ↔ (a = b ∨ a ∈ s) := +finset.induction_on_to_finset s $ assume l hl, show a ∈ insert b l ↔ (a = b ∨ a ∈ l), by simp -theorem mem_singleton_iff (x a : α) : x ∈ (insert a (∅ : finset α)) ↔ (x = a) := -by rw [mem_insert_iff, mem_empty_iff, or_false] - -theorem mem_singleton (a : α) : a ∈ ({a} : finset α) := mem_insert a ∅ - -theorem mem_singleton_of_eq {x a : α} (H : x = a) : x ∈ ({a} : finset α) := -by rw H; apply mem_insert - -theorem eq_of_mem_singleton {x a : α} (H : x ∈ insert a (∅:finset α)) : x = a := -iff.mp (mem_singleton_iff _ _) H - -theorem eq_of_singleton_eq {a b : α} (H : insert a ∅ = insert b (∅:finset α)) : a = b := -have a ∈ insert b ∅, by rw ←H; apply mem_singleton, -eq_of_mem_singleton this +theorem mem_insert : a ∈ insert a s := by simp +theorem mem_insert_of_mem : a ∈ s → a ∈ insert b s := by simp {contextual := tt} +theorem mem_of_mem_insert_of_ne (h : b ∈ insert a s) : b ≠ a → b ∈ s := +or_resolve_right (mem_insert_iff.mp h) -theorem insert_eq_of_mem {a : α} {s : finset α} (H : a ∈ s) : insert a s = s := +@[simp] theorem insert_eq_of_mem (h : a ∈ s) : insert a s = s := ext (λ x, by rw mem_insert_iff; apply or_iff_right_of_imp; intro eq; rw eq; assumption) -theorem singleton_ne_empty (a : α) : ({a} : finset α) ≠ ∅ := -begin - intro H, - apply not_mem_empty a, - rw ←H, - apply mem_insert -end +@[simp] theorem insert.comm : insert a (insert b s) = insert b (insert a s) := +ext $ by simp -theorem pair_eq_singleton (a : α) : ({a, a} : finset α) = {a} := -show insert a {a} = ({a} : finset α), by rw [insert_eq_of_mem]; apply mem_singleton - --- useful in proofs by induction -theorem forall_of_forall_insert {p : α → Prop} {a : α} {s : finset α} - (H : ∀ x, x ∈ insert a s → p x) : - ∀ x, x ∈ s → p x := -λ x xs, H x (mem_insert_of_mem _ xs) - -theorem insert.comm (x y : α) (s : finset α) : insert x (insert y s) = insert y (insert x s) := -ext (λ a, begin repeat {rw mem_insert_iff}, rw [propext or.left_comm] end) +@[simp] theorem insert_idem : insert a (insert a s) = insert a s := +ext $ by simp [mem_insert_iff] -theorem card_insert_of_mem {a : α} {s : finset α} : a ∈ s → card (insert a s) = card s := -quot.induction_on s - (λ (l : nodup_list α) (ainl : a ∈ ⟦l⟧), list.length_insert_of_mem ainl) +@[simp] theorem insert_ne_empty : insert a s ≠ ∅ := +assume h, @not_mem_empty α a $ h ▸ by simp -theorem card_insert_of_not_mem {a : α} {s : finset α} : a ∉ s → card (insert a s) = card s + 1 := -quot.induction_on s - (λ (l : nodup_list α) (nainl : a ∉ ⟦l⟧), list.length_insert_of_not_mem nainl) +theorem subset_insert [h : decidable_eq α] : s ⊆ insert a s := +subset_of_forall (λ x h, mem_insert_of_mem h) -theorem card_insert_le (a : α) (s : finset α) : - card (insert a s) ≤ card s + 1 := -if H : a ∈ s then by rw [card_insert_of_mem H]; apply le_succ -else by rw [card_insert_of_not_mem H] - -theorem perm_insert_cons_of_not_mem [decidable_eq α] {a : α} {l : list α} (h : a ∉ l) : perm (list.insert a l) (a :: l) := -have list.insert a l = a :: l, from if_neg h, by rw this +theorem insert_subset_insert (h : s ⊆ t) : insert a s ⊆ insert a t := +subset_of_forall $ assume x, by simp; exact or.imp_right (mem_of_subset_of_mem h) @[recursor 6] protected theorem induction {p : finset α → Prop} - (H1 : p ∅) - (H2 : ∀ ⦃a : α⦄, ∀{s : finset α}, ¬ a ∈ s → p s → p (insert a s)) : - ∀s, p s := -λ s, -quot.induction_on s - (λ u, - subtype.rec_on u - (λ l, - list.rec_on l - (λ nodup_l, H1) - (λ a l', - λ IH nodup_al', - have aux₁: a ∉ l', from not_mem_of_nodup_cons nodup_al', - have ndl' : nodup l', from nodup_of_nodup_cons nodup_al', - have p1 : p (quot.mk _ (subtype.mk l' ndl')), from IH ndl', - have a ∉ @id (finset α) (quot.mk _ (subtype.mk l' ndl')), from aux₁, - have p' : p (insert a (quot.mk _ (subtype.mk l' ndl'))), from H2 this p1, - have list.insert a l' = a :: l', from if_neg aux₁, - have hperm : perm (list.insert a l') (a :: l'), by rw this, - begin - apply @eq.subst _ p _ _ _ p', - apply quot.sound, - exact hperm - end))) + (h₁ : p ∅) (h₂ : ∀⦃a : α⦄, ∀{s : finset α}, a ∉ s → p s → p (insert a s)) (s) : p s := +finset.induction_on_to_finset s $ λl, list.rec_on l + (assume _, h₁) + (assume a l ih hal, + let l' := to_finset_of_nodup l $ nodup_of_nodup_cons hal in + have insert a l' = to_finset_of_nodup (a :: l) hal, + from ext $ by simp, + this ▸ @h₂ a l' (not_mem_of_nodup_cons hal) (ih _)) protected theorem induction_on {p : finset α → Prop} (s : finset α) - (H1 : p ∅) - (H2 : ∀ ⦃a : α⦄, ∀ {s : finset α}, a ∉ s → p s → p (insert a s)) : - p s := -finset.induction H1 H2 s - -theorem exists_mem_of_ne_empty {s : finset α} : s ≠ ∅ → ∃ a : α, a ∈ s := -@finset.induction_on _ _ (λ x, x ≠ ∅ → ∃ a : α, a ∈ x) s -(λ h, absurd rfl h) -(by intros a s nin ih h; existsi a; apply mem_insert) + (h₁ : p ∅) (h₂ : ∀ ⦃a : α⦄, ∀ {s : finset α}, a ∉ s → p s → p (insert a s)) : p s := +finset.induction h₁ h₂ s -theorem eq_empty_of_card_eq_zero {s : finset α} (H : card s = 0) : s = ∅ := -@finset.induction_on _ _ (λ x, card x = 0 → x = ∅) s -(λ h, rfl) -(by intros a s' H1 Ih H; rw (card_insert_of_not_mem H1) at H; contradiction) H +-- useful in proofs by induction +theorem forall_of_forall_insert {p : α → Prop} (H : ∀ x, x ∈ insert a s → p x) : + ∀ x, x ∈ s → p x := +λ x xs, H x (mem_insert_of_mem xs) end insert -/- erase -/ -section erase -variable [decidable_eq α] - -def erase (a : α) (s : finset α) : finset α := -quot.lift_on s - (λ l, to_finset_of_nodup (l.1.erase a) (nodup_erase_of_nodup a l.2)) - (λ (l₁ l₂ : nodup_list α) (p : l₁ ~ l₂), quot.sound (perm.erase_perm_erase_of_perm a p)) +section singleton +variables [decidable_eq α] {a b : α} {s : finset α} -theorem not_mem_erase (a : α) (s : finset α) : a ∉ erase a s := -quot.induction_on s - (λ l, list.mem_erase_of_nodup _ l.2) +@[simp] theorem mem_singleton_iff : b ∈ ({a} : finset α) ↔ (b = a) := +show b ∈ insert a ∅ ↔ b = a, by simp -theorem card_erase_of_mem {a : α} {s : finset α} : a ∈ s → card (erase a s) = pred (card s) := -quot.induction_on s (λ l ainl, list.length_erase_of_mem ainl) +theorem mem_singleton : a ∈ ({a} : finset α) := mem_insert -theorem card_erase_of_not_mem {a : α} {s : finset α} : a ∉ s → card (erase a s) = card s := -quot.induction_on s (λ l nainl, length_erase_of_not_mem nainl) +theorem mem_singleton_of_eq (h : b = a) : b ∈ ({a} : finset α) := +by rw h; apply mem_insert -theorem erase_empty (a : α) : erase a ∅ = ∅ := rfl +theorem eq_of_mem_singleton (h : b ∈ ({a}:finset α)) : b = a := +iff.mp mem_singleton_iff h -theorem ne_of_mem_erase {a b : α} {s : finset α} : b ∈ erase a s → b ≠ a := -by intros h beqa; subst b; exact absurd h (not_mem_erase _ _) +theorem eq_of_singleton_eq (h : {a} = ({b}:finset α)) : a = b := +have a ∈ ({b} : finset α), by rw ←h; apply mem_singleton, +eq_of_mem_singleton this -theorem mem_of_mem_erase {a b : α} {s : finset α} : b ∈ erase a s → b ∈ s := -quot.induction_on s (λ l bin, mem_of_mem_erase bin) +@[simp] theorem singleton_ne_empty : ({a} : finset α) ≠ ∅ := insert_ne_empty -theorem mem_erase_of_ne_of_mem {a b : α} {s : finset α} : a ≠ b → a ∈ s → a ∈ erase b s := -quot.induction_on s (λ l n ain, list.mem_erase_of_ne_of_mem n ain) +@[simp] theorem insert_singelton_self_eq : ({a, a} : finset α) = {a} := +show insert a {a} = ({a} : finset α), by rw [insert_eq_of_mem]; apply mem_singleton -theorem mem_erase_iff (a b : α) (s : finset α) : a ∈ erase b s ↔ a ∈ s ∧ a ≠ b := -iff.intro - (λ H, and.intro (mem_of_mem_erase H) (ne_of_mem_erase H)) - (λ H, mem_erase_of_ne_of_mem (and.right H) (and.left H)) - -open decidable -theorem erase_insert {a : α} {s : finset α} : a ∉ s → erase a (insert a s) = s := -λ anins, finset.ext (λ b, by_cases - (λ beqa : b = a, iff.intro - (λ bin, by subst b; exact absurd bin (not_mem_erase _ _)) - (λ bin, by subst b; contradiction)) - (λ bnea : b ≠ a, iff.intro - (λ bin, - have b ∈ insert a s, from mem_of_mem_erase bin, - mem_of_mem_insert_of_ne this bnea) - (λ bin, - have b ∈ insert a s, from mem_insert_of_mem _ bin, - mem_erase_of_ne_of_mem bnea this))) - -theorem insert_erase {a : α} {s : finset α} : a ∈ s → insert a (erase a s) = s := -λ ains, finset.ext (λ b, by_cases - (λ h : b = a, iff.intro - (λ bin, by subst b; assumption) - (λ bin, by subst b; apply mem_insert)) - (λ hn : b ≠ a, iff.intro - (λ bin, mem_of_mem_erase (mem_of_mem_insert_of_ne bin hn)) -(λ bin, mem_insert_of_mem _ (mem_erase_of_ne_of_mem hn bin)))) -end erase +end singleton /- union -/ section union @@ -335,59 +279,47 @@ quotient.lift_on₂ s₁ s₂ instance : has_union (finset α) := ⟨finset.union⟩ -theorem mem_union_left {a : α} {s₁ : finset α} (s₂ : finset α) : a ∈ s₁ → a ∈ s₁ ∪ s₂ := -quotient.induction_on₂ s₁ s₂ (λ l₁ l₂ ainl₁, list.mem_union_left ainl₁ _) +@[simp] theorem mem_union_iff {a : α} {s₁ s₂ : finset α} : a ∈ s₁ ∪ s₂ ↔ a ∈ s₁ ∨ a ∈ s₂ := +quotient.induction_on₂ s₁ s₂ (λ l₁ l₂, list.mem_union_iff) -theorem mem_union_l {a : α} {s₁ : finset α} {s₂ : finset α} : a ∈ s₁ → a ∈ s₁ ∪ s₂ := -mem_union_left s₂ +theorem mem_union_left {a : α} {s₁ : finset α} (s₂ : finset α) : a ∈ s₁ → a ∈ s₁ ∪ s₂ := +by rw [mem_union_iff]; exact or.inl theorem mem_union_right {a : α} {s₂ : finset α} (s₁ : finset α) : a ∈ s₂ → a ∈ s₁ ∪ s₂ := -quotient.induction_on₂ s₁ s₂ (λ l₁ l₂ ainl₂, list.mem_union_right _ ainl₂) - -theorem mem_union_r {a : α} {s₂ : finset α} {s₁ : finset α} : a ∈ s₂ → a ∈ s₁ ∪ s₂ := -mem_union_right s₁ +by rw [mem_union_iff]; exact or.inr theorem mem_or_mem_of_mem_union {a : α} {s₁ s₂ : finset α} : a ∈ s₁ ∪ s₂ → a ∈ s₁ ∨ a ∈ s₂ := -quotient.induction_on₂ s₁ s₂ (λ l₁ l₂ ainl₁l₂, list.mem_or_mem_of_mem_union ainl₁l₂) - -theorem mem_union_iff (a : α) (s₁ s₂ : finset α) : a ∈ s₁ ∪ s₂ ↔ a ∈ s₁ ∨ a ∈ s₂ := -iff.intro - (λ h, mem_or_mem_of_mem_union h) - (λ d, or.elim d - (λ i, mem_union_left _ i) -(λ i, mem_union_right _ i)) +mem_union_iff.mp -theorem union_comm (s₁ s₂ : finset α) : s₁ ∪ s₂ = s₂ ∪ s₁ := -ext (λ a, by repeat {rw mem_union_iff}; exact or.comm) +@[simp] theorem union_comm (s₁ s₂ : finset α) : s₁ ∪ s₂ = s₂ ∪ s₁ := +ext $ by simp -theorem union_assoc (s₁ s₂ s₃ : finset α) : (s₁ ∪ s₂) ∪ s₃ = s₁ ∪ (s₂ ∪ s₃) := -ext (λ a, by repeat {rw mem_union_iff}; exact or.assoc) +@[simp] theorem union_assoc (s₁ s₂ s₃ : finset α) : (s₁ ∪ s₂) ∪ s₃ = s₁ ∪ (s₂ ∪ s₃) := +ext $ by simp theorem union_left_comm (s₁ s₂ s₃ : finset α) : s₁ ∪ (s₂ ∪ s₃) = s₂ ∪ (s₁ ∪ s₃) := -left_comm _ union_comm union_assoc s₁ s₂ s₃ +ext $ by simp theorem union_right_comm (s₁ s₂ s₃ : finset α) : (s₁ ∪ s₂) ∪ s₃ = (s₁ ∪ s₃) ∪ s₂ := -right_comm _ union_comm union_assoc s₁ s₂ s₃ +ext $ by simp -theorem union_self (s : finset α) : s ∪ s = s := -ext (λ a, iff.intro - (λ ain, or.elim (mem_or_mem_of_mem_union ain) (λ i, i) (λ i, i)) - (λ i, mem_union_left _ i)) +@[simp] theorem union_self (s : finset α) : s ∪ s = s := +ext $ by simp -theorem union_empty (s : finset α) : s ∪ ∅ = s := -ext (λ a, iff.intro - (λ l, or.elim (mem_or_mem_of_mem_union l) (λ i, i) (λ i, absurd i (not_mem_empty _))) - (λ r, mem_union_left _ r)) +@[simp] theorem union_empty (s : finset α) : s ∪ ∅ = s := +ext $ by simp -theorem empty_union (s : finset α) : ∅ ∪ s = s := -calc ∅ ∪ s = s ∪ ∅ : union_comm _ _ - ... = s : union_empty _ +@[simp] theorem empty_union (s : finset α) : ∅ ∪ s = s := +ext $ by simp -theorem insert_eq (a : α) (s : finset α) : insert a s = insert a ∅ ∪ s := -ext (λ x, by rw [mem_insert_iff, mem_union_iff, mem_singleton_iff]) +theorem insert_eq (a : α) (s : finset α) : insert a s = {a} ∪ s := +ext $ by simp -theorem insert_union (a : α) (s t : finset α) : insert a (s ∪ t) = insert a s ∪ t := -by rw [insert_eq, insert_eq a s, union_assoc] +@[simp] theorem insert_union (a : α) (s t : finset α) : insert a s ∪ t = insert a (s ∪ t) := +ext $ by simp + +@[simp] theorem union_insert (a : α) (s t : finset α) : s ∪ insert a t = insert a (s ∪ t) := +ext $ by simp end union @@ -397,66 +329,71 @@ variable [decidable_eq α] protected def inter (s₁ s₂ : finset α) : finset α := quotient.lift_on₂ s₁ s₂ - (λ l₁ l₂, - to_finset_of_nodup (list.inter l₁.1 l₂.1) - (nodup_inter_of_nodup _ l₁.2)) + (λ l₁ l₂, to_finset_of_nodup (list.inter l₁.1 l₂.1) (nodup_inter_of_nodup _ l₁.2)) (λ v₁ v₂ w₁ w₂ p₁ p₂, quot.sound (perm.perm_inter p₁ p₂)) instance : has_inter (finset α) := ⟨finset.inter⟩ +@[simp] theorem mem_inter_iff (a : α) (s₁ s₂ : finset α) : a ∈ s₁ ∩ s₂ ↔ a ∈ s₁ ∧ a ∈ s₂ := +quotient.induction_on₂ s₁ s₂ (λ l₁ l₂, mem_inter_iff _ _ _) + theorem mem_of_mem_inter_left {a : α} {s₁ s₂ : finset α} : a ∈ s₁ ∩ s₂ → a ∈ s₁ := -quotient.induction_on₂ s₁ s₂ (λ l₁ l₂ ainl₁l₂, list.mem_of_mem_inter_left ainl₁l₂) +by rw [mem_inter_iff]; exact and.left theorem mem_of_mem_inter_right {a : α} {s₁ s₂ : finset α} : a ∈ s₁ ∩ s₂ → a ∈ s₂ := -quotient.induction_on₂ s₁ s₂ (λ l₁ l₂ ainl₁l₂, list.mem_of_mem_inter_right ainl₁l₂) +by rw [mem_inter_iff]; exact and.right theorem mem_inter {a : α} {s₁ s₂ : finset α} : a ∈ s₁ → a ∈ s₂ → a ∈ s₁ ∩ s₂ := -quotient.induction_on₂ s₁ s₂ (λ l₁ l₂ ainl₁ ainl₂, list.mem_inter_of_mem_of_mem ainl₁ ainl₂) - -theorem mem_inter_iff (a : α) (s₁ s₂ : finset α) : a ∈ s₁ ∩ s₂ ↔ a ∈ s₁ ∧ a ∈ s₂ := -iff.intro - (λ h, and.intro (mem_of_mem_inter_left h) (mem_of_mem_inter_right h)) -(λ h, mem_inter (and.elim_left h) (and.elim_right h)) +by rw [mem_inter_iff]; exact and.intro -theorem inter_comm (s₁ s₂ : finset α) : s₁ ∩ s₂ = s₂ ∩ s₁ := -ext (λ a, by repeat {rw mem_inter_iff}; exact and.comm) +@[simp] theorem inter_comm (s₁ s₂ : finset α) : s₁ ∩ s₂ = s₂ ∩ s₁ := +ext $ by simp -theorem inter_assoc (s₁ s₂ s₃ : finset α) : (s₁ ∩ s₂) ∩ s₃ = s₁ ∩ (s₂ ∩ s₃) := -ext (λ a, by repeat {rw mem_inter_iff}; exact and.assoc) +@[simp] theorem inter_assoc (s₁ s₂ s₃ : finset α) : (s₁ ∩ s₂) ∩ s₃ = s₁ ∩ (s₂ ∩ s₃) := +ext $ by simp -theorem inter_left_comm (s₁ s₂ s₃ : finset α) : s₁ ∩ (s₂ ∩ s₃) = s₂ ∩ (s₁ ∩ s₃) := -left_comm _ inter_comm inter_assoc s₁ s₂ s₃ +@[simp] theorem inter_left_comm (s₁ s₂ s₃ : finset α) : s₁ ∩ (s₂ ∩ s₃) = s₂ ∩ (s₁ ∩ s₃) := +ext $ by simp -theorem inter_right_comm (s₁ s₂ s₃ : finset α) : (s₁ ∩ s₂) ∩ s₃ = (s₁ ∩ s₃) ∩ s₂ := -right_comm _ inter_comm inter_assoc s₁ s₂ s₃ +@[simp] theorem inter_right_comm (s₁ s₂ s₃ : finset α) : (s₁ ∩ s₂) ∩ s₃ = (s₁ ∩ s₃) ∩ s₂ := +ext $ by simp -theorem inter_self (s : finset α) : s ∩ s = s := -ext (λ a, iff.intro - (λ h, mem_of_mem_inter_right h) - (λ h, mem_inter h h)) +@[simp] theorem inter_self (s : finset α) : s ∩ s = s := +ext $ by simp -theorem inter_empty (s : finset α) : s ∩ ∅ = ∅ := -ext (λ a, iff.intro - (λ h, absurd (mem_of_mem_inter_right h) (not_mem_empty _)) - (λ h, absurd h (not_mem_empty _))) +@[simp] theorem inter_empty (s : finset α) : s ∩ ∅ = ∅ := +ext $ by simp -theorem empty_inter (s : finset α) : ∅ ∩ s = ∅ := -calc ∅ ∩ s = s ∩ ∅ : inter_comm _ _ - ... = ∅ : inter_empty _ +@[simp] theorem empty_inter (s : finset α) : ∅ ∩ s = ∅ := +ext $ by simp -theorem insert_inter_of_mem {s₁ s₂ : finset α} {a : α} (h : a ∈ s₂) : +@[simp] theorem insert_inter_of_mem {s₁ s₂ : finset α} {a : α} (h : a ∈ s₂) : insert a s₁ ∩ s₂ = insert a (s₁ ∩ s₂) := -ext $ assume a', by by_cases a' = a with h'; simp [mem_inter_iff, mem_insert_iff, h, h'] +ext $ by simp; intro x; constructor; finish + +@[simp] theorem inter_insert_of_mem {s₁ s₂ : finset α} {a : α} (h : a ∈ s₁) : + s₁ ∩ insert a s₂ = insert a (s₁ ∩ s₂) := +by rw [inter_comm, insert_inter_of_mem h, inter_comm] -theorem insert_inter_of_not_mem {s₁ s₂ : finset α} {a : α} (h : a ∉ s₂) : +@[simp] theorem insert_inter_of_not_mem {s₁ s₂ : finset α} {a : α} (h : a ∉ s₂) : insert a s₁ ∩ s₂ = s₁ ∩ s₂ := ext $ assume a', by by_cases a' = a with h'; simp [mem_inter_iff, mem_insert_iff, h, h'] -theorem singleton_inter_of_mem {a : α} {s : finset α} : a ∈ s → insert a ∅ ∩ s = insert a ∅ := -by simp [insert_inter_of_mem, empty_inter] {contextual:=tt} +@[simp] theorem inter_insert_of_not_mem {s₁ s₂ : finset α} {a : α} (h : a ∉ s₁) : + s₁ ∩ insert a s₂ = s₁ ∩ s₂ := +by rw [inter_comm, insert_inter_of_not_mem h, inter_comm] + +@[simp] theorem singleton_inter_of_mem {a : α} {s : finset α} : a ∈ s → {a} ∩ s = {a} := +show a ∈ s → insert a ∅ ∩ s = insert a ∅, by simp {contextual := tt} + +@[simp] theorem singleton_inter_of_not_mem {a : α} {s : finset α} : a ∉ s → {a} ∩ s = ∅ := +show a ∉ s → insert a ∅ ∩ s = ∅, by simp {contextual := tt} + +@[simp] theorem inter_singleton_of_mem {a : α} {s : finset α} (h : a ∈ s) : s ∩ {a} = {a} := +by rw [inter_comm, singleton_inter_of_mem h] -theorem singleton_inter_of_not_mem {a : α} {s : finset α} : a ∉ s → insert a ∅ ∩ s = ∅ := -by simp [insert_inter_of_not_mem, empty_inter] {contextual:=tt} +@[simp] theorem inter_singleton_of_not_mem {a : α} {s : finset α} (h : a ∉ s) : s ∩ {a} = ∅ := +by rw [inter_comm, singleton_inter_of_not_mem h] end inter @@ -465,167 +402,104 @@ section inter variable [decidable_eq α] theorem inter_distrib_left (s t u : finset α) : s ∩ (t ∪ u) = (s ∩ t) ∪ (s ∩ u) := -ext (λ x, by rw [mem_inter_iff];repeat {rw mem_union_iff};repeat {rw mem_inter_iff}; apply iff.intro; repeat {finish}) +ext $ begin simp [mem_inter_iff, mem_union_iff], intro x, apply iff.intro, repeat {finish} end theorem inter_distrib_right (s t u : finset α) : (s ∪ t) ∩ u = (s ∩ u) ∪ (t ∩ u) := -ext (λ x, by rw [mem_inter_iff]; repeat {rw mem_union_iff}; repeat {rw mem_inter_iff}; apply iff.intro; repeat {finish}) +ext $ begin simp [mem_inter_iff, mem_union_iff], intro x, apply iff.intro, repeat {finish} end theorem union_distrib_left (s t u : finset α) : s ∪ (t ∩ u) = (s ∪ t) ∩ (s ∪ u) := -ext (λ x, by rw [mem_union_iff]; repeat {rw mem_inter_iff}; repeat {rw mem_union_iff}; apply iff.intro; repeat {finish}) +ext $ begin simp [mem_inter_iff, mem_union_iff], intro x, apply iff.intro, repeat {finish} end theorem union_distrib_right (s t u : finset α) : (s ∩ t) ∪ u = (s ∪ u) ∩ (t ∪ u) := -ext (λ x, by rw [mem_union_iff]; repeat {rw mem_inter_iff}; repeat {rw mem_union_iff}; apply iff.intro; repeat {finish}) +ext $ begin simp [mem_inter_iff, mem_union_iff], intro x, apply iff.intro, repeat {finish} end end inter -protected def subset_aux {α : Type u} (l₁ l₂ : list α) := ∀ ⦃a : α⦄, a ∈ l₁ → a ∈ l₂ -/- subset -/ -protected def subset (s₁ s₂ : finset α) : Prop := -quotient.lift_on₂ s₁ s₂ - (λ l₁ l₂, finset.subset_aux l₁.1 l₂.1) - (λ v₁ v₂ w₁ w₂ p₁ p₂, propext (iff.intro - (λ s₁ a i, perm.mem_of_perm p₂ (s₁ (perm.mem_of_perm (perm.symm p₁) i))) - (λ s₂ a i, perm.mem_of_perm (perm.symm p₂) (s₂ (perm.mem_of_perm p₁ i))))) - -instance : has_subset (finset α) := ⟨finset.subset⟩ +/- erase -/ +section erase +variables [decidable_eq α] {a b c : α} {s t : finset α} -theorem empty_subset (s : finset α) : ∅ ⊆ s := -quot.induction_on s (λ l, list.nil_subset l.1) +def erase (a : α) (s : finset α) : finset α := +quot.lift_on s + (λ l, to_finset_of_nodup (l.1.erase a) (nodup_erase_of_nodup a l.2)) + (λ (l₁ l₂ : nodup_list α) (p : l₁ ~ l₂), quot.sound (perm.erase_perm_erase_of_perm a p)) --- theorem subset_univ [h : fintype α] (s : finset α) : s ⊆ univ := --- quot.induction_on s (λ l a i, fintype.complete a) +@[simp] theorem mem_erase_iff : a ∈ erase b s ↔ a ≠ b ∧ a ∈ s := +finset.induction_on_to_finset s $ λ l hl, mem_erase_iff_of_nodup hl -theorem subset.refl (s : finset α) : s ⊆ s := -quot.induction_on s (λ l, list.subset.refl l.1) +theorem not_mem_erase : a ∉ erase a s := by simp -theorem subset.trans {s₁ s₂ s₃ : finset α} : s₁ ⊆ s₂ → s₂ ⊆ s₃ → s₁ ⊆ s₃ := -quotient.induction_on₃ s₁ s₂ s₃ (λ l₁ l₂ l₃ h₁ h₂, list.subset.trans h₁ h₂) +@[simp] theorem erase_empty : erase a ∅ = ∅ := rfl -theorem mem_of_subset_of_mem {s₁ s₂ : finset α} {a : α} : s₁ ⊆ s₂ → a ∈ s₁ → a ∈ s₂ := -quotient.induction_on₂ s₁ s₂ (λ l₁ l₂ h₁ h₂, h₁ h₂) +theorem ne_of_mem_erase : b ∈ erase a s → b ≠ a := by simp {contextual:=tt} -theorem subset.antisymm {s₁ s₂ : finset α} (H₁ : s₁ ⊆ s₂) (H₂ : s₂ ⊆ s₁) : s₁ = s₂ := -ext (λ x, iff.intro (λ H, mem_of_subset_of_mem H₁ H) (λ H, mem_of_subset_of_mem H₂ H)) +theorem mem_of_mem_erase : b ∈ erase a s → b ∈ s := by simp {contextual:=tt} --- alternative name -theorem eq_of_subset_of_subset {s₁ s₂ : finset α} (H₁ : s₁ ⊆ s₂) (H₂ : s₂ ⊆ s₁) : s₁ = s₂ := -subset.antisymm H₁ H₂ +theorem mem_erase_of_ne_of_mem : a ≠ b → a ∈ s → a ∈ erase b s := by simp {contextual:=tt} -theorem subset_of_forall {s₁ s₂ : finset α} : (∀x, x ∈ s₁ → x ∈ s₂) → s₁ ⊆ s₂ := -quotient.induction_on₂ s₁ s₂ (λ l₁ l₂ H, H) +theorem erase_insert (h : a ∉ s) : erase a (insert a s) = s := +ext $ assume x, by simp; constructor; finish -theorem subset_insert [h : decidable_eq α] (s : finset α) (a : α) : s ⊆ insert a s := -subset_of_forall (λ x h, mem_insert_of_mem _ h) +theorem insert_erase (h : a ∈ s) : insert a (erase a s) = s := +ext $ assume x, by simp; constructor; finish -theorem eq_empty_of_subset_empty {x : finset α} (H : x ⊆ ∅) : x = ∅ := -subset.antisymm H (empty_subset x) +theorem erase_subset_erase (h : s ⊆ t) : erase a s ⊆ erase a t := +subset_of_forall $ assume x, by simp; exact and_implies_right (mem_of_subset_of_mem h) -theorem subset_empty_iff (x : finset α) : x ⊆ ∅ ↔ x = ∅ := -iff.intro eq_empty_of_subset_empty (λ xeq, by rw xeq; apply subset.refl ∅) +theorem erase_subset : erase a s ⊆ s := +subset_of_forall $ assume x, by simp {contextual:=tt} -section -variable [decidable_eq α] +theorem erase_eq_of_not_mem (h : a ∉ s) : erase a s = s := +ext $ assume b, by by_cases b = a; simp [*] -theorem erase_subset_erase (a : α) {s t : finset α} (H : s ⊆ t) : erase a s ⊆ erase a t := -begin - apply subset_of_forall, - intro x, - repeat {rw mem_erase_iff}, - intro H', - show x ∈ t ∧ x ≠ a, from and.intro (mem_of_subset_of_mem H (and.left H')) (and.right H') -end - -theorem erase_subset (a : α) (s : finset α) : erase a s ⊆ s := -begin - apply subset_of_forall, - intro x, - rw mem_erase_iff, - intro H, - apply and.left H -end - -theorem erase_eq_of_not_mem {a : α} {s : finset α} (anins : a ∉ s) : erase a s = s := -eq_of_subset_of_subset (erase_subset _ _) - (subset_of_forall (λ x, λ xs : x ∈ s, - have x ≠ a, from λ H', anins (eq.subst H' xs), -mem_erase_of_ne_of_mem this xs)) - -theorem erase_insert_subset (a : α) (s : finset α) : erase a (insert a s) ⊆ s := -decidable.by_cases - (λ ains : a ∈ s, by rw [insert_eq_of_mem ains]; apply erase_subset) - (λ nains : a ∉ s, by rw [erase_insert nains]; apply subset.refl) +theorem erase_insert_subset : erase a (insert a s) ⊆ s := +by by_cases a ∈ s; simp [h, erase_subset, erase_insert, subset.refl] -theorem erase_subset_of_subset_insert {a : α} {s t : finset α} (H : s ⊆ insert a t) : - erase a s ⊆ t := -subset.trans (erase_subset_erase _ H) (erase_insert_subset _ _) +theorem erase_subset_of_subset_insert (h : s ⊆ insert a t) : erase a s ⊆ t := +subset.trans (erase_subset_erase h) erase_insert_subset -theorem insert_erase_subset (a : α) (s : finset α) : s ⊆ insert a (erase a s) := +theorem insert_erase_subset : s ⊆ insert a (erase a s) := decidable.by_cases (λ ains : a ∈ s, by rw [insert_erase ains]; apply subset.refl) (λ nains : a ∉ s, by rw[erase_eq_of_not_mem nains]; apply subset_insert) -theorem insert_subset_insert (a : α) {s t : finset α} (H : s ⊆ t) : insert a s ⊆ insert a t := -begin - apply subset_of_forall, - intro x, - repeat {rw mem_insert_iff}, - intro H', - cases H' with xeqa xins, - exact (or.inl xeqa), - exact (or.inr (mem_of_subset_of_mem H xins)) -end - -theorem subset_insert_of_erase_subset {s t : finset α} {a : α} (H : erase a s ⊆ t) : - s ⊆ insert a t := -subset.trans (insert_erase_subset a s) (insert_subset_insert _ H) +theorem subset_insert_of_erase_subset (h : erase a s ⊆ t) : s ⊆ insert a t := +subset.trans insert_erase_subset (insert_subset_insert h) theorem subset_insert_iff (s t : finset α) (a : α) : s ⊆ insert a t ↔ erase a s ⊆ t := iff.intro erase_subset_of_subset_insert subset_insert_of_erase_subset -end +end erase /- upto -/ section upto +variables {n m l : ℕ} -def upto (n : nat) : finset nat := +def upto (n : ℕ) : finset ℕ := to_finset_of_nodup (list.upto n) (nodup_upto n) -theorem card_upto : ∀ n, card (upto n) = n := -list.length_upto - -theorem lt_of_mem_upto {n a : nat} : a ∈ upto n → a < n := -@list.lt_of_mem_upto n a +theorem lt_of_mem_upto : m ∈ upto n → m < n := +@list.lt_of_mem_upto n m -theorem mem_upto_succ_of_mem_upto {n a : nat} : a ∈ upto n → a ∈ upto (succ n) := +theorem mem_upto_succ_of_mem_upto : m ∈ upto n → m ∈ upto (succ n) := list.mem_upto_succ_of_mem_upto -theorem mem_upto_of_lt {n a : nat} : a < n → a ∈ upto n := -@list.mem_upto_of_lt n a +theorem mem_upto_of_lt : m < n → m ∈ upto n := +@list.mem_upto_of_lt n m -theorem mem_upto_iff (a n : nat) : a ∈ upto n ↔ a < n := +theorem mem_upto_iff : m ∈ upto n ↔ m < n := iff.intro lt_of_mem_upto mem_upto_of_lt theorem upto_zero : upto 0 = ∅ := rfl -theorem upto_succ (n : ℕ) : upto (succ n) = upto n ∪ insert n ∅ := -begin - apply ext, intro x, - rw [mem_union_iff], repeat {rw mem_upto_iff}, - rw [mem_singleton_iff, ←le_iff_lt_or_eq], - apply iff.intro, - {intro h, apply le_of_lt_succ, exact h}, - {apply lt_succ_of_le} -end +theorem upto_succ : upto (succ n) = insert n (upto n) := +ext $ by simp [mem_upto_iff, mem_insert_iff, lt_succ_iff_le, le_iff_lt_or_eq] end upto /- useful rules for calculations with quantifiers -/ theorem exists_mem_empty_iff (p : α → Prop) : (∃ x, x ∈ (∅ : finset α) ∧ p x) ↔ false := -iff.intro - (λ H, - let ⟨x,H1⟩ := H in - not_mem_empty α (H1.left)) - (λ H, false.elim H) +⟨λ⟨x, hx⟩, not_mem_empty (hx.left), false.elim⟩ theorem exists_mem_insert_iff [d : decidable_eq α] (a : α) (s : finset α) (p : α → Prop) : @@ -633,24 +507,24 @@ theorem exists_mem_insert_iff [d : decidable_eq α] iff.intro (λ H, let ⟨x,H1,H2⟩ := H in - or.elim (eq_or_mem_of_mem_insert H1) + or.elim (mem_insert_iff.mp H1) (λ l, or.inl (eq.subst l H2)) (λ r, or.inr ⟨x, ⟨r, H2⟩⟩)) (λ H, or.elim H - (λ l, ⟨a, ⟨mem_insert _ _, l⟩⟩) - (λ r, let ⟨x,H2,H3⟩ := r in ⟨x, ⟨mem_insert_of_mem _ H2, H3⟩⟩)) + (λ l, ⟨a, ⟨mem_insert, l⟩⟩) + (λ r, let ⟨x,H2,H3⟩ := r in ⟨x, ⟨mem_insert_of_mem H2, H3⟩⟩)) theorem forall_mem_empty_iff (p : α → Prop) : (∀ x, x ∈ (∅ : finset α) → p x) ↔ true := -iff.intro (λ H, trivial) (λ H x H', absurd H' (not_mem_empty _)) +iff.intro (λ H, trivial) (λ H x H', absurd H' not_mem_empty) theorem forall_mem_insert_iff [d : decidable_eq α] (a : α) (s : finset α) (p : α → Prop) : (∀ x, x ∈ insert a s → p x) ↔ p a ∧ (∀ x, x ∈ s → p x) := iff.intro - (λ H, and.intro (H _ (mem_insert _ _)) (λ x H', H _ (mem_insert_of_mem _ H'))) + (λ H, and.intro (H _ mem_insert) (λ x H', H _ (mem_insert_of_mem H'))) (λ H x, λ H' : x ∈ insert a s, - or.elim (eq_or_mem_of_mem_insert H') + or.elim (mem_insert_iff.mp H') (λ l, eq.subst (eq.symm l) H.left) (λ r, and.right H _ r)) @@ -690,4 +564,35 @@ quot.induction_on s $ assume ⟨l, hl⟩, end image +section card +variables [decidable_eq α] {a : α} {s : finset α} {n : ℕ} + +/- card -/ +def card (s : finset α) : nat := +quot.lift_on s (λ l, length l.1) (λ l₁ l₂ p, perm.length_eq_length_of_perm p) + +@[simp] theorem card_empty : card (∅ : finset α) = 0 := rfl + +lemma ne_empty_of_card_eq_succ : card s = succ n → s ≠ ∅ := +λ h hn, by rw hn at h; contradiction + +@[simp] theorem card_insert_of_not_mem : a ∉ s → card (insert a s) = card s + 1 := +quot.induction_on s (λ (l : nodup_list α) (nainl : a ∉ ⟦l⟧), list.length_insert_of_not_mem nainl) + +theorem card_insert_le : card (insert a s) ≤ card s + 1 := +if h : a ∈ s then by simp [h, le_add_left] else by rw [card_insert_of_not_mem h] + +theorem eq_empty_of_card_eq_zero : card s = 0 → s = ∅ := +s.induction_on + (assume _, rfl) + (assume a s ha ih, by rw [card_insert_of_not_mem ha]; exact assume h, nat.no_confusion h) + +theorem card_erase_of_mem : a ∈ s → card (erase a s) = pred (card s) := +quot.induction_on s (λ l ainl, list.length_erase_of_mem ainl) + +theorem card_upto : card (upto n) = n := +list.length_upto n + +end card + end finset diff --git a/data/finset/default.lean b/data/finset/default.lean new file mode 100644 index 0000000000000..3b589b29bda6e --- /dev/null +++ b/data/finset/default.lean @@ -0,0 +1 @@ +import data.finset.basic data.finset.fold diff --git a/data/finset/fold.lean b/data/finset/fold.lean new file mode 100644 index 0000000000000..f9c6c22ab0218 --- /dev/null +++ b/data/finset/fold.lean @@ -0,0 +1,97 @@ +/- +Copyright (c) 2017 Johannes Hölzl. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: Johannes Hölzl + +Fold on finite sets +-/ +import data.list.set data.list.perm tactic.finish data.finset.basic +open list subtype nat finset + +universes u v w +variables {α : Type u} {β : Type v} {γ : Type w} + +namespace list +variables {op : α → α → α} [ha : is_associative α op] [hc : is_commutative α op] +local notation a * b := op a b +local notation l <*> a := foldl op a l + +section associative +include ha + +lemma foldl_assoc : ∀{l : list α} {a₁ a₂}, l <*> (a₁ * a₂) = a₁ * (l <*> a₂) +| [] a₁ a₂ := by simp +| (a :: l) a₁ a₂ := + calc a::l <*> (a₁ * a₂) = l <*> (a₁ * (a₂ * a)) : by simp [ha.assoc] + ... = a₁ * (a::l <*> a₂) : by rw [foldl_assoc]; simp + +lemma foldl_op_eq_op_foldr_assoc : ∀{l : list α} {a₁ a₂}, (l <*> a₁) * a₂ = a₁ * l.foldr (*) a₂ +| [] a₁ a₂ := by simp +| (a :: l) a₁ a₂ := by simp [foldl_assoc, ha.assoc]; rw [foldl_op_eq_op_foldr_assoc] +end associative + +section commutative +include ha hc + +lemma foldl_assoc_comm_cons {l : list α} {a₁ a₂} : (a₁ :: l) <*> a₂ = a₁ * (l <*> a₂) := +by rw [foldl_cons, hc.comm, foldl_assoc] + +lemma fold_op_eq_of_perm {l₁ l₂ : list α} {a : α} (h : perm l₁ l₂) : l₁ <*> a = l₂ <*> a := +by induction h; simp [*, -foldl_cons, foldl_assoc_comm_cons]; cc + +end commutative + +end list + +namespace finset + +section fold +variables (op : β → β → β) [hc : is_commutative β op] [ha : is_associative β op] {f : α → β} {b : β} +local notation a * b := op a b +include hc ha + +def fold (b : β) (f : α → β) (s : finset α) : β := +quot.lift_on s (λl, (l.val.map f).foldl op b) (λl₁ l₂, list.fold_op_eq_of_perm ∘ perm.perm_map _) + +variable {op} + +@[simp] lemma fold_to_finset_of_nodup {l : list α} (hl : nodup l) : + (to_finset_of_nodup l hl).fold op b f = (l.map f).foldl op b := rfl + +@[simp] lemma fold_empty : (∅:finset α).fold op b f = b := rfl + +variables [decidable_eq α] [decidable_eq γ] + +@[simp] lemma fold_insert {s : finset α} {a : α} : + a ∉ s → (insert a s).fold op b f = f a * s.fold op b f := +finset.induction_on_to_finset s $ assume l hl (h : a ∉ l), + show ((if a ∈ l then l else a :: l).map f).foldl op b = f a * (l.map f).foldl op b, + begin rw [if_neg h], simp [-foldl_map, -foldl_cons], exact list.foldl_assoc_comm_cons end + +@[simp] lemma fold_singleton {a : α} : ({a}:finset α).fold op b f = f a * b := +calc ({a}:finset α).fold op b f = f a * (∅:finset α).fold op b f : fold_insert $ by simp + ... = f a * b : by rw [fold_empty] + +@[simp] lemma fold_image {g : γ → α} {s : finset γ} : + (∀x∈s, ∀y∈s, g x = g y → x = y) → (s.image g).fold op b f = s.fold op b (f ∘ g) := +finset.induction_on_to_finset s $ assume l hl hg, by rw [image_to_finset_of_nodup hl hg]; simp + +lemma fold_op_distrib {s : finset α} {f g : α → β} {b₁ b₂ : β} : + s.fold op (b₁ * b₂) (λx, f x * g x) = s.fold op b₁ f * s.fold op b₂ g := +s.induction_on (by simp) (by simp {contextual := tt}; cc) + +lemma fold_hom + {op₁ : β → β → β} [is_commutative β op₁] [is_associative β op₁] + {op₂ : γ → γ → γ} [is_commutative γ op₂] [is_associative γ op₂] + {s : finset α} {f : α → β} {b : β} {m : β → γ} (hm : ∀x y, m (op₁ x y) = op₂ (m x) (m y)) : + m (s.fold op₁ b f) = s.fold op₂ (m b) (λx, m (f x)) := +s.induction_on (by simp) (by simp [hm] {contextual := tt}) + +lemma fold_union_inter {s₁ s₂ : finset α} {b₁ b₂ : β} : + (s₁ ∪ s₂).fold op b₁ f * (s₁ ∩ s₂).fold op b₂ f = s₁.fold op b₂ f * s₂.fold op b₁ f := +s₁.induction_on + (by simp [empty_union, empty_inter]; cc) + (assume a s h, by by_cases a ∈ s₂; simp [*]; cc) + +end fold +end finset diff --git a/data/list/set.lean b/data/list/set.lean index 9f887197baafe..3a8522f03eb95 100644 --- a/data/list/set.lean +++ b/data/list/set.lean @@ -493,20 +493,22 @@ theorem nodup_erase_of_nodup [decidable_eq α] (a : α) : ∀ {l}, nodup l → n have aux : nodup (b :: l.erase a), from nodup_cons nbineal ndeal, begin rw [erase_cons_tail _ aneb], exact aux end) -theorem mem_erase_of_nodup [decidable_eq α] (a : α) : ∀ {l}, nodup l → a ∉ l.erase a -| [] n := (not_mem_nil _) -| (b::l) n := - have ndl : nodup l, from nodup_of_nodup_cons n, - have naineal : a ∉ l.erase a, from mem_erase_of_nodup ndl, - have nbinl : b ∉ l, from not_mem_of_nodup_cons n, - by_cases - (λ aeqb : b = a, begin rw [aeqb.symm, erase_cons_head], exact nbinl end) - (λ aneb : b ≠ a, - have aux : a ∉ b :: l.erase a, from - assume ainbeal : a ∈ b :: l.erase a, or.elim (eq_or_mem_of_mem_cons ainbeal) - (λ aeqb : a = b, absurd aeqb.symm aneb) - (λ aineal : a ∈ l.erase a, absurd aineal naineal), - begin rw [erase_cons_tail _ aneb], exact aux end) +theorem mem_erase_iff_of_nodup [decidable_eq α] {a b : α} : + ∀ {l}, nodup l → (a ∈ l.erase b ↔ (a ≠ b ∧ a ∈ l)) +| [] hn := by simp +| (c :: l) hn := + begin + by_cases c = b with h₁, + { by_cases a = b with h₂, + { simp [h₁, h₂, erase_cons_head], + exact h₁ ▸ not_mem_of_nodup_cons hn }, + { simp [h₁, h₂] } }, + { simp [h₁, erase_cons_tail, mem_erase_iff_of_nodup (nodup_of_nodup_cons hn)], + by_cases a = b; cc } + end + +theorem mem_erase_of_nodup [decidable_eq α] {a : α} {l} (h : nodup l) : a ∉ l.erase a := +by rw [mem_erase_iff_of_nodup h]; simp def erase_dup [decidable_eq α] : list α → list α | [] := []