diff --git a/library/algebra/group_bigops.lean b/library/algebra/group_bigops.lean index d10398d9b..48e6d3bcb 100644 --- a/library/algebra/group_bigops.lean +++ b/library/algebra/group_bigops.lean @@ -9,27 +9,77 @@ Finite products on a monoid, and finite sums on an additive monoid. There are th Prod, Sum (in namespace finset) : products and sums over finsets Prod, Sum (in namespace set) : products and sums over finite sets +We also define internal functions Prodl_semigroup and Prod_semigroup that can be used to define +operations over commutative semigroups where there is no unit. We put them into their own namespaces +so that they won't be very prominent. They can be used to define Min and Max in the number systems, +or Inter for finsets. + We have to be careful with dependencies. This theory imports files from finset and list, which import basic files from nat. -/ import .group .group_power data.list.basic data.list.perm data.finset.basic data.set.finite -open function binary quot subtype list finset +open function binary quot subtype list variables {A B : Type} variable [deceqA : decidable_eq A] +definition mulf [sgB : semigroup B] (f : A → B) : B → A → B := +λ b a, b * f a + /- -- list versions. -/ +/- Prodl_semigroup: product indexed by a list, with a default for the empty list -/ + +namespace Prodl_semigroup + variable [semigroup B] + + definition Prodl_semigroup (dflt : B) : ∀ (l : list A) (f : A → B), B + | [] f := dflt + | (a :: l) f := list.foldl (mulf f) (f a) l + + theorem Prodl_semigroup_nil (dflt : B) (f : A → B) : Prodl_semigroup dflt nil f = dflt := rfl + + theorem Prodl_semigroup_cons (dflt : B) (f : A → B) (a : A) (l : list A) : + Prodl_semigroup dflt (a::l) f = list.foldl (mulf f) (f a) l := rfl + + theorem Prodl_semigroup_singleton (dflt : B) (f : A → B) (a : A) : + Prodl_semigroup dflt [a] f = f a := rfl + + theorem Prodl_semigroup_cons_cons (dflt : B) (f : A → B) (a₁ a₂ : A) (l : list A) : + Prodl_semigroup dflt (a₁::a₂::l) f = f a₁ * Prodl_semigroup dflt (a₂::l) f := + begin + rewrite [↑Prodl_semigroup, foldl_cons, ↑mulf at {2}], + generalize (f a₂), + induction l with a l ih, + {intro x, exact rfl}, + intro x, + rewrite [*foldl_cons, ↑mulf at {2,3}, mul.assoc, ih] + end + + theorem Prodl_semigroup_binary (dflt : B) (f : A → B) (a₁ a₂ : A) : + Prodl_semigroup dflt [a₁, a₂] f = f a₁ * f a₂ := rfl + + section deceqA + include deceqA + + theorem Prodl_semigroup_insert_of_mem (dflt : B) (f : A → B) {a : A} {l : list A} : a ∈ l → + Prodl_semigroup dflt (insert a l) f = Prodl_semigroup dflt l f := + assume ainl, by rewrite [insert_eq_of_mem ainl] + + theorem Prodl_semigroup_insert_insert_of_not_mem (dflt : B) (f : A → B) + {a₁ a₂ : A} {l : list A} (h₁ : a₂ ∉ l) (h₂ : a₁ ∉ insert a₂ l) : + Prodl_semigroup dflt (insert a₁ (insert a₂ l)) f = + f a₁ * Prodl_semigroup dflt (insert a₂ l) f := + by rewrite [insert_eq_of_not_mem h₂, insert_eq_of_not_mem h₁, Prodl_semigroup_cons_cons] + end deceqA +end Prodl_semigroup + /- Prodl: product indexed by a list -/ section monoid - variable [mB : monoid B] - include mB - - definition mulf (f : A → B) : B → A → B := - λ b a, b * f a + variable [monoid B] definition Prodl (l : list A) (f : A → B) : B := list.foldl (mulf f) 1 l @@ -90,12 +140,10 @@ section monoid from take a' Pa'in, Pconst a' (mem_cons_of_mem a Pa'in), by rewrite [Prodl_cons f, Pconst a !mem_cons, Prodl_eq_pow_of_const b Pconstl, length_cons, add_one, pow_succ b] - end monoid section comm_monoid - variable [cmB : comm_monoid B] - include cmB + variable [comm_monoid B] theorem Prodl_mul (l : list A) (f g : A → B) : Prodl l (λx, f x * g x) = Prodl l f * Prodl l g := list.induction_on l @@ -108,8 +156,7 @@ end comm_monoid /- Suml: sum indexed by a list -/ section add_monoid - variable [amB : add_monoid B] - include amB + variable [add_monoid B] local attribute add_monoid.to_monoid [trans_instance] definition Suml (l : list A) (f : A → B) : B := Prodl l f @@ -135,7 +182,6 @@ section add_monoid theorem Suml_zero (l : list A) : Suml l (λ x, 0) = (0:B) := Prodl_one l theorem Suml_singleton (a : A) (f : A → B) : Suml [a] f = f a := Prodl_singleton a f - end add_monoid section add_comm_monoid @@ -151,15 +197,65 @@ end add_comm_monoid -- finset versions -/ -/- Prod: product indexed by a finset -/ +/- Prod_semigroup : product indexed by a finset, with a default for the empty finset -/ namespace finset - variable [cmB : comm_monoid B] - include cmB + variable [comm_semigroup B] theorem mulf_rcomm (f : A → B) : right_commutative (mulf f) := right_commutative_compose_right (@has_mul.mul B _) f (@mul.right_comm B _) + namespace Prod_semigroup + open Prodl_semigroup + + private theorem Prodl_semigroup_eq_Prodl_semigroup_of_perm + (dflt : B) (f : A → B) {l₁ l₂ : list A} (p : perm l₁ l₂) : + Prodl_semigroup dflt l₁ f = Prodl_semigroup dflt l₂ f := + perm.induction_on p + rfl -- nil nil + (take x l₁ l₂ p ih, + by rewrite [*Prodl_semigroup_cons, perm.foldl_eq_of_perm (mulf_rcomm f) p]) + (take x y l, + begin rewrite [*Prodl_semigroup_cons, *foldl_cons, ↑mulf, mul.comm] end) + (take l₁ l₂ l₃ p₁ p₂ ih₁ ih₂, eq.trans ih₁ ih₂) + + definition Prod_semigroup (dflt : B) (s : finset A) (f : A → B) : B := + quot.lift_on s + (λ l, Prodl_semigroup dflt (elt_of l) f) + (λ l₁ l₂ p, Prodl_semigroup_eq_Prodl_semigroup_of_perm dflt f p) + + theorem Prod_semigroup_empty (dflt : B) (f : A → B) : Prod_semigroup dflt ∅ f = dflt := rfl + + section deceqA + include deceqA + + theorem Prod_semigroup_singleton (dflt : B) (f : A → B) (a : A) : + Prod_semigroup dflt '{a} f = f a := rfl + + theorem Prod_semigroup_insert_insert (dflt : B) (f : A → B) {a₁ a₂ : A} {s : finset A} : + a₂ ∉ s → a₁ ∉ insert a₂ s → + Prod_semigroup dflt (insert a₁ (insert a₂ s)) f = + f a₁ * Prod_semigroup dflt (insert a₂ s) f := + quot.induction_on s + (take l h₁ h₂, Prodl_semigroup_insert_insert_of_not_mem dflt f h₁ h₂) + + theorem Prod_semigroup_insert (dflt : B) (f : A → B) {a : A} {s : finset A} (anins : a ∉ s) + (sne : s ≠ ∅) : + Prod_semigroup dflt (insert a s) f = f a * Prod_semigroup dflt s f := + obtain a' (a's : a' ∈ s), from exists_mem_of_ne_empty sne, + have H : s = insert a' (erase a' s), from eq.symm (insert_erase a's), + begin+ + rewrite [H, Prod_semigroup_insert_insert dflt f !not_mem_erase (eq.subst H anins)] + end + end deceqA + end Prod_semigroup +end finset + +/- Prod: product indexed by a finset -/ + +namespace finset + variable [comm_monoid B] + theorem Prodl_eq_Prodl_of_perm (f : A → B) {l₁ l₂ : list A} : perm l₁ l₂ → Prodl l₁ f = Prodl l₂ f := λ p, perm.foldl_eq_of_perm (mulf_rcomm f) p 1 @@ -249,8 +345,7 @@ end finset /- Sum: sum indexed by a finset -/ namespace finset - variable [acmB : add_comm_monoid B] - include acmB + variable [add_comm_monoid B] local attribute add_comm_monoid.to_comm_monoid [trans_instance] definition Sum (s : finset A) (f : A → B) : B := Prod s f @@ -294,8 +389,7 @@ open classical /- Prod: product indexed by a set -/ section Prod - variable [cmB : comm_monoid B] - include cmB + variable [comm_monoid B] noncomputable definition Prod (s : set A) (f : A → B) : B := finset.Prod (to_finset s) f @@ -375,8 +469,7 @@ end Prod /- Sum: sum indexed by a set -/ section Sum - variable [acmB : add_comm_monoid B] - include acmB + variable [add_comm_monoid B] local attribute add_comm_monoid.to_comm_monoid [trans_instance] noncomputable definition Sum (s : set A) (f : A → B) : B := Prod s f @@ -414,4 +507,47 @@ section Sum (∑ j ∈ t, f j) = (∑ i ∈ s, f (g i)) := Prod_eq_of_bij_on f H end Sum +/- Prod_semigroup : product indexed by a set, with a default for the empty set -/ + +namespace Prod_semigroup + variable [comm_semigroup B] + + noncomputable definition Prod_semigroup (dflt : B) (s : set A) (f : A → B) : B := + finset.Prod_semigroup.Prod_semigroup dflt (to_finset s) f + + theorem Prod_semigroup_empty (dflt : B) (f : A → B) : Prod_semigroup dflt ∅ f = dflt := + by rewrite [↑Prod_semigroup, to_finset_empty] + + theorem Prod_semigroup_of_not_finite (dflt : B) {s : set A} (nfins : ¬ finite s) (f : A → B) : + Prod_semigroup dflt s f = dflt := + by rewrite [↑Prod_semigroup, to_finset_of_not_finite nfins] + + theorem Prod_semigroup_singleton (dflt : B) (f : A → B) (a : A) : + Prod_semigroup dflt ('{a}) f = f a := + by rewrite [↑Prod_semigroup, to_finset_insert, to_finset_empty, + finset.Prod_semigroup.Prod_semigroup_singleton dflt f a] + + theorem Prod_semigroup_insert_insert (dflt : B) (f : A → B) {a₁ a₂ : A} {s : set A} + [h : finite s] : + a₂ ∉ s → a₁ ∉ insert a₂ s → + Prod_semigroup dflt (insert a₁ (insert a₂ s)) f = + f a₁ * Prod_semigroup dflt (insert a₂ s) f := + begin + rewrite [↑Prod_semigroup, -+mem_to_finset_eq, +to_finset_insert], + intro h1 h2, + apply finset.Prod_semigroup.Prod_semigroup_insert_insert dflt f h1 h2 + end + + theorem Prod_semigroup_insert (dflt : B) (f : A → B) {a : A} {s : set A} [h : finite s] : + a ∉ s → s ≠ ∅ → Prod_semigroup dflt (insert a s) f = f a * Prod_semigroup dflt s f := + begin + rewrite [↑Prod_semigroup, -mem_to_finset_eq, +to_finset_insert, -finset.to_set_empty], + intro h1 h2, + apply finset.Prod_semigroup.Prod_semigroup_insert dflt f h1, + intro h3, revert h2, rewrite [-h3, to_set_to_finset], + intro h4, exact (h4 rfl) + end + +end Prod_semigroup + end set diff --git a/library/data/finset/basic.lean b/library/data/finset/basic.lean index 853c9218f..14ec70e3b 100644 --- a/library/data/finset/basic.lean +++ b/library/data/finset/basic.lean @@ -244,7 +244,7 @@ protected theorem induction_on {P : finset A → Prop} (s : finset A) P s := finset.induction H1 H2 s -theorem exists_me_of_ne_empty {s : finset A} : s ≠ ∅ → ∃ a : A, a ∈ s := +theorem exists_mem_of_ne_empty {s : finset A} : s ≠ ∅ → ∃ a : A, a ∈ s := begin induction s with a s nin ih, {intro h, exact absurd rfl h}, @@ -270,7 +270,7 @@ quot.lift_on s (λ l, to_finset_of_nodup (erase a (elt_of l)) (nodup_erase_of_nodup a (has_property l))) (λ (l₁ l₂ : nodup_list A) (p : l₁ ~ l₂), quot.sound (erase_perm_erase_of_perm a p)) -theorem mem_erase (a : A) (s : finset A) : a ∉ erase a s := +theorem not_mem_erase (a : A) (s : finset A) : a ∉ erase a s := quot.induction_on s (λ l, list.mem_erase_of_nodup _ (has_property l)) @@ -284,7 +284,7 @@ theorem erase_empty (a : A) : erase a ∅ = ∅ := rfl theorem ne_of_mem_erase {a b : A} {s : finset A} : b ∈ erase a s → b ≠ a := -by intro h beqa; subst b; exact absurd h !mem_erase +by intro h beqa; subst b; exact absurd h !not_mem_erase theorem mem_of_mem_erase {a b : A} {s : finset A} : b ∈ erase a s → b ∈ s := quot.induction_on s (λ l bin, mem_of_mem_erase bin) @@ -304,7 +304,7 @@ open decidable theorem erase_insert {a : A} {s : finset A} : 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 !mem_erase) + (λ bin, by subst b; exact absurd bin !not_mem_erase) (λ bin, by subst b; contradiction)) (λ bnea : b ≠ a, iff.intro (λ bin, diff --git a/library/data/hf.lean b/library/data/hf.lean index 652103f21..13334fe48 100644 --- a/library/data/hf.lean +++ b/library/data/hf.lean @@ -270,8 +270,8 @@ by intros; substvars; contradiction definition erase (a : hf) (s : hf) : hf := of_finset (erase a (to_finset s)) -theorem mem_erase (a : hf) (s : hf) : a ∉ erase a s := -begin unfold [mem, erase], rewrite to_finset_of_finset, apply finset.mem_erase end +theorem not_mem_erase (a : hf) (s : hf) : a ∉ erase a s := +begin unfold [mem, erase], rewrite to_finset_of_finset, apply finset.not_mem_erase end theorem card_erase_of_mem {a : hf} {s : hf} : a ∈ s → card (erase a s) = pred (card s) := begin unfold mem, intro h, unfold [erase, card], rewrite to_finset_of_finset, apply finset.card_erase_of_mem h end @@ -283,7 +283,7 @@ theorem erase_empty (a : hf) : erase a ∅ = ∅ := rfl theorem ne_of_mem_erase {a b : hf} {s : hf} : b ∈ erase a s → b ≠ a := -by intro h beqa; subst b; exact absurd h !mem_erase +by intro h beqa; subst b; exact absurd h !not_mem_erase theorem mem_of_mem_erase {a b : hf} {s : hf} : b ∈ erase a s → b ∈ s := begin unfold [erase, mem], rewrite to_finset_of_finset, intro h, apply mem_of_mem_erase h end @@ -389,7 +389,7 @@ begin take s₂, suppose ∅ ⊆ s₂, !zero_le, take s₂, suppose insert a s₁ ⊆ s₂, assert a ∈ s₂, from mem_of_subset_of_mem this !mem_insert, - have a ∉ erase a s₂, from !mem_erase, + have a ∉ erase a s₂, from !not_mem_erase, have s₁ ⊆ erase a s₂, from subset_of_forall (take x xin, by_cases (suppose x = a, by subst x; contradiction)