diff --git a/library/algebra/algebra.md b/library/algebra/algebra.md index ecc78ff069..7b53237b2c 100644 --- a/library/algebra/algebra.md +++ b/library/algebra/algebra.md @@ -8,6 +8,8 @@ Algebraic structures. * [binary](binary.lean) : binary operations * [wf](wf.lean) : well-founded relations * [group](group.lean) +* [group_power](group_power.lean) : nat and int powers +* [group_bigops](group_bigops.lean) : finite products and sums * [ring](ring.lean) * [ordered_group](ordered_group.lean) * [ordered_ring](ordered_ring.lean) diff --git a/library/algebra/group_bigops.lean b/library/algebra/group_bigops.lean new file mode 100644 index 0000000000..9bda92e1cc --- /dev/null +++ b/library/algebra/group_bigops.lean @@ -0,0 +1,229 @@ +/- +Copyright (c) 2015 Jeremy Avigad. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Leonardo de Moura, Jeremy Avigad + +Finite products on a monoid, and finite sums on an additive monoid. These are called + + algebra.list.prod + algebra.finset.prod + algebra.list.sum + algebra.finset.sum + +So when we open algebra we have list.prod etc., and when we migrate to nat, we have +nat.list.prod etc. + +We have to be careful with dependencies. This theory imports files from finset and list, which +import basic files from nat. Then nat imports this file to instantiate finite products and sums. +-/ +import .group data.list.basic data.list.perm data.finset.basic +open algebra function binary quot subtype + +namespace algebra + +/- list.prod -/ + +namespace list -- i.e. algebra.list + open list -- i.e. ordinary lists + + variable {A : Type} + + section monoid + variables {B : Type} [mB : monoid B] + include mB + + definition mulf (f : A → B) : B → A → B := + λ b a, b * f a + + definition prod (l : list A) (f : A → B) : B := + list.foldl (mulf f) 1 l + + -- ∏ x ← l, f x + notation `∏` binders `←` l, r:(scoped f, prod l f) := r + + private theorem foldl_const (f : A → B) : + ∀ (l : list A) (b : B), foldl (mulf f) b l = b * foldl (mulf f) 1 l + | [] b := by rewrite [*foldl_nil, mul_one] + | (a::l) b := by rewrite [*foldl_cons, foldl_const, {foldl _ (mulf f 1 a) _}foldl_const, ↑mulf, + one_mul, mul.assoc] + + theorem prod_nil (f : A → B) : prod [] f = 1 := rfl + + theorem prod_cons (f : A → B) (a : A) (l : list A) : prod (a::l) f = f a * prod l f := + by rewrite [↑prod, foldl_cons, foldl_const, ↑mulf, one_mul] + + theorem prod_append : + ∀ (l₁ l₂ : list A) (f : A → B), prod (l₁++l₂) f = prod l₁ f * prod l₂ f + | [] l₂ f := by rewrite [append_nil_left, prod_nil, one_mul] + | (a::l) l₂ f := by rewrite [append_cons, *prod_cons, prod_append, mul.assoc] + + section decidable_eq + variable [H : decidable_eq A] + include H + + theorem prod_insert_of_mem (f : A → B) {a : A} {l : list A} : a ∈ l → + prod (insert a l) f = prod l f := + assume ainl, by rewrite [insert_eq_of_mem ainl] + + theorem prod_insert_of_not_mem (f : A → B) {a : A} {l : list A} : + a ∉ l → prod (insert a l) f = f a * prod l f := + assume nainl, by rewrite [insert_eq_of_not_mem nainl, prod_cons] + + theorem prod_union {l₁ l₂ : list A} (f : A → B) (d : disjoint l₁ l₂) : + prod (union l₁ l₂) f = prod l₁ f * prod l₂ f := + by rewrite [union_eq_append d, prod_append] + + end decidable_eq + end monoid + + section comm_monoid + variables {B : Type} [cmB : comm_monoid B] + include cmB + + theorem prod_mul (l : list A) (f g : A → B) : prod l (λx, f x * g x) = prod l f * prod l g := + list.induction_on l + (by rewrite [*prod_nil, mul_one]) + (take a l, + assume IH, + by rewrite [*prod_cons, IH, *mul.assoc, mul.left_comm (prod l f)]) + + end comm_monoid +end list + +/- finset.prod -/ + +namespace finset + open finset + variables {A B : Type} + variable [cmB : comm_monoid B] + include cmB + + theorem mulf_rcomm (f : A → B) : right_commutative (list.mulf f) := + right_commutative_compose_right (@has_mul.mul B cmB) f (@mul.right_comm B cmB) + + section + open perm + theorem listprod_of_perm (f : A → B) {l₁ l₂ : list A} : + l₁ ~ l₂ → list.prod l₁ f = list.prod l₂ f := + λ p, foldl_eq_of_perm (mulf_rcomm f) p 1 + end + + definition prod (s : finset A) (f : A → B) : B := + quot.lift_on s + (λ l, list.prod (elt_of l) f) + (λ l₁ l₂ p, listprod_of_perm f p) + + -- ∏ x ∈ s, f x + notation `∏` binders `∈` s, r:(scoped f, prod s f) := r + + theorem prod_empty (f : A → B) : prod ∅ f = 1 := + list.prod_nil f + + section decidable_eq + variable [H : decidable_eq A] + include H + + theorem prod_insert_of_mem (f : A → B) {a : A} {s : finset A} : + a ∈ s → prod (insert a s) f = prod s f := + quot.induction_on s + (λ l ainl, list.prod_insert_of_mem f ainl) + + theorem prod_insert_of_not_mem (f : A → B) {a : A} {s : finset A} : + a ∉ s → prod (insert a s) f = f a * prod s f := + quot.induction_on s + (λ l nainl, list.prod_insert_of_not_mem f nainl) + + theorem prod_union (f : A → B) {s₁ s₂ : finset A} (disj : s₁ ∩ s₂ = ∅) : + prod (s₁ ∪ s₂) f = prod s₁ f * prod s₂ f := + have H1 : disjoint s₁ s₂ → prod (s₁ ∪ s₂) f = prod s₁ f * prod s₂ f, from + quot.induction_on₂ s₁ s₂ + (λ l₁ l₂ d, list.prod_union f d), + H1 (disjoint_of_inter_empty disj) + + theorem prod_mul (s : finset A) (f g : A → B) : prod s (λx, f x * g x) = prod s f * prod s g := + quot.induction_on s (take u, !list.prod_mul) + + end decidable_eq +end finset + +/- list.sum -/ + +namespace list + open list + variable {A : Type} + + section add_monoid + variables {B : Type} [amB : add_monoid B] + include amB + local attribute add_monoid.to_monoid [instance] + + definition sum (l : list A) (f : A → B) : B := prod l f + + -- ∑ x ← l, f x + notation `∑` binders `←` l, r:(scoped f, sum l f) := r + + theorem sum_nil (f : A → B) : sum [] f = 0 := prod_nil f + theorem sum_cons (f : A → B) (a : A) (l : list A) : sum (a::l) f = f a + sum l f := + prod_cons f a l + theorem sum_append (l₁ l₂ : list A) (f : A → B) : sum (l₁++l₂) f = sum l₁ f + sum l₂ f := + prod_append l₁ l₂ f + + section decidable_eq + variable [H : decidable_eq A] + include H + + theorem sum_insert_of_mem (f : A → B) {a : A} {l : list A} (H : a ∈ l) : + sum (insert a l) f = sum l f := prod_insert_of_mem f H + theorem sum_insert_of_not_mem (f : A → B) {a : A} {l : list A} (H : a ∉ l) : + sum (insert a l) f = f a * sum l f := prod_insert_of_not_mem f H + theorem sum_union {l₁ l₂ : list A} (f : A → B) (d : disjoint l₁ l₂) : + sum (union l₁ l₂) f = sum l₁ f + sum l₂ f := prod_union f d + end decidable_eq + end add_monoid + + section add_comm_monoid + variables {B : Type} [acmB : add_comm_monoid B] + include acmB + local attribute add_comm_monoid.to_comm_monoid [instance] + + theorem sum_add (l : list A) (f g : A → B) : sum l (λx, f x + g x) = sum l f + sum l g := + prod_mul l f g + end add_comm_monoid +end list + +/- finset.sum -/ + +namespace finset + open finset + variable {A : Type} + + section add_comm_monoid + variables {B : Type} [acmB : add_comm_monoid B] + include acmB + local attribute add_comm_monoid.to_comm_monoid [instance] + + definition sum (s : finset A) (f : A → B) : B := prod s f + + -- ∑ x ∈ s, f x + notation `∑` binders `∈` s, r:(scoped f, sum s f) := r + + theorem sum_empty (f : A → B) : sum ∅ f = 0 := prod_empty f + + section decidable_eq + variable [H : decidable_eq A] + include H + + theorem sum_insert_of_mem (f : A → B) {a : A} {s : finset A} (H : a ∈ s) : + sum (insert a s) f = sum s f := prod_insert_of_mem f H + theorem sum_insert_of_not_mem (f : A → B) {a : A} {s : finset A} (H : a ∉ s) : + sum (insert a s) f = f a + sum s f := prod_insert_of_not_mem f H + theorem sum_union (f : A → B) {s₁ s₂ : finset A} (disj : s₁ ∩ s₂ = ∅) : + sum (s₁ ∪ s₂) f = sum s₁ f + sum s₂ f := prod_union f disj + theorem sum_add (s : finset A) (f g : A → B) : + sum s (λx, f x + g x) = sum s f + sum s g := prod_mul s f g + + end decidable_eq + end add_comm_monoid +end finset + +end algebra diff --git a/library/algebra/group_pow.lean b/library/algebra/group_power.lean similarity index 100% rename from library/algebra/group_pow.lean rename to library/algebra/group_power.lean diff --git a/library/data/finset/bigop.lean b/library/data/finset/bigop.lean deleted file mode 100644 index fa728a1742..0000000000 --- a/library/data/finset/bigop.lean +++ /dev/null @@ -1,41 +0,0 @@ -/- -Copyright (c) 2015 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Author: Leonardo de Moura - -Big operator for finite sets. --/ -import algebra.group data.finset.basic data.list.bigop -open algebra finset function binary quot subtype - -namespace finset -variables {A B : Type} -variable [g : comm_monoid B] -include g - -definition bigop (s : finset A) (f : A → B) : B := -quot.lift_on s - (λ l, list.bigop (elt_of l) f) - (λ l₁ l₂ p, list.bigop_of_perm f p) - -theorem bigop_empty (f : A → B) : bigop ∅ f = 1 := -list.bigop_nil f - -variable [H : decidable_eq A] -include H - -theorem bigop_insert_of_mem (f : A → B) {a : A} {s : finset A} : a ∈ s → bigop (insert a s) f = bigop s f := -quot.induction_on s - (λ l ainl, list.bigop_insert_of_mem f ainl) - -theorem bigop_insert_of_not_mem (f : A → B) {a : A} {s : finset A} : a ∉ s → bigop (insert a s) f = f a * bigop s f := -quot.induction_on s - (λ l nainl, list.bigop_insert_of_not_mem f nainl) - -theorem bigop_union (f : A → B) {s₁ s₂ : finset A} (disj : s₁ ∩ s₂ = ∅) : -bigop (s₁ ∪ s₂) f = bigop s₁ f * bigop s₂ f := -have H1 : disjoint s₁ s₂ → bigop (s₁ ∪ s₂) f = bigop s₁ f * bigop s₂ f, from - quot.induction_on₂ s₁ s₂ - (λ l₁ l₂ d, list.bigop_union f d), -H1 (disjoint_of_inter_empty disj) -end finset diff --git a/library/data/finset/default.lean b/library/data/finset/default.lean index 737a195a00..e674f993d5 100644 --- a/library/data/finset/default.lean +++ b/library/data/finset/default.lean @@ -5,4 +5,4 @@ Author: Leonardo de Moura Finite sets. -/ -import data.finset.basic data.finset.comb data.finset.card data.finset.bigop +import .basic .comb .to_set .card diff --git a/library/data/finset/finset.md b/library/data/finset/finset.md index 27f2ac2b0d..744a37c1f3 100644 --- a/library/data/finset/finset.md +++ b/library/data/finset/finset.md @@ -5,5 +5,5 @@ Finite sets. By default, `import list` imports everything here. [basic](basic.lean) : basic operations and properties [comb](comb.lean) : combinators and list constructions +[to_set](to_set.lean) : interactions with sets [card](card.lean) : cardinality -[bigop](bigop.lean) : "big" operations \ No newline at end of file diff --git a/library/data/list/bigop.lean b/library/data/list/bigop.lean deleted file mode 100644 index bfb5481fdf..0000000000 --- a/library/data/list/bigop.lean +++ /dev/null @@ -1,69 +0,0 @@ -/- -Copyright (c) 2015 Leonardo de Moura. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Module: data.list.bigop -Authors: Leonardo de Moura - -Big operator for lists --/ -import algebra.group data.list.comb data.list.set data.list.perm -open algebra function binary quot - -namespace list -variables {A B : Type} -variable [g : monoid B] -include g - -definition mulf (f : A → B) : B → A → B := -λ b a, b * f a - -definition bigop (l : list A) (f : A → B) : B := -foldl (mulf f) 1 l - -private theorem foldl_const (f : A → B) : ∀ (l : list A) (b : B), foldl (mulf f) b l = b * foldl (mulf f) 1 l -| [] b := by rewrite [*foldl_nil, mul_one] -| (a::l) b := by rewrite [*foldl_cons, foldl_const, {foldl _ (mulf f 1 a) _}foldl_const, ↑mulf, one_mul, mul.assoc] - -theorem bigop_nil (f : A → B) : bigop [] f = 1 := -rfl - -theorem bigop_cons (f : A → B) (a : A) (l : list A) : bigop (a::l) f = f a * bigop l f := -by rewrite [↑bigop, foldl_cons, foldl_const, ↑mulf, one_mul] - -theorem bigop_append : ∀ (l₁ l₂ : list A) (f : A → B), bigop (l₁++l₂) f = bigop l₁ f * bigop l₂ f -| [] l₂ f := by rewrite [append_nil_left, bigop_nil, one_mul] -| (a::l) l₂ f := by rewrite [append_cons, *bigop_cons, bigop_append, mul.assoc] - -section insert -variable [H : decidable_eq A] -include H - -theorem bigop_insert_of_mem (f : A → B) {a : A} {l : list A} : a ∈ l → bigop (insert a l) f = bigop l f := -assume ainl, by rewrite [insert_eq_of_mem ainl] - -theorem bigop_insert_of_not_mem (f : A → B) {a : A} {l : list A} : a ∉ l → bigop (insert a l) f = f a * bigop l f := -assume nainl, by rewrite [insert_eq_of_not_mem nainl, bigop_cons] -end insert - -section union -variable [H : decidable_eq A] -include H - -definition bigop_union {l₁ l₂ : list A} (f : A → B) (d : disjoint l₁ l₂) : bigop (union l₁ l₂) f = bigop l₁ f * bigop l₂ f := -by rewrite [union_eq_append d, bigop_append] -end union -end list - -namespace list -open perm -variables {A B : Type} -variable [g : comm_monoid B] -include g - -theorem mulf_rcomm (f : A → B) : right_commutative (mulf f) := -right_commutative_compose_right (@has_mul.mul B g) f (@mul.right_comm B g) - -theorem bigop_of_perm (f : A → B) {l₁ l₂ : list A} : l₁ ~ l₂ → bigop l₁ f = bigop l₂ f := -λ p, foldl_eq_of_perm (mulf_rcomm f) p 1 -end list diff --git a/library/data/list/default.lean b/library/data/list/default.lean index 4158c178bd..e5116d8323 100644 --- a/library/data/list/default.lean +++ b/library/data/list/default.lean @@ -3,5 +3,4 @@ Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: Jeremy Avigad -/ -import data.list.basic data.list.comb data.list.set data.list.perm -import data.list.bigop data.list.as_type +import .basic .comb .set .perm .as_type diff --git a/library/data/list/list.md b/library/data/list/list.md index 34cf6a826d..1326271b40 100644 --- a/library/data/list/list.md +++ b/library/data/list/list.md @@ -7,5 +7,4 @@ List of elements of a fixed type. By default, `import list` imports everything h [comb](comb.lean) : combinators and list constructions [set](set.lean) : set-like operations (these support the finset construction) [perm](perm.lean) : equivalence up to permutation (these support the finset construction) -[bigop](bigop.lean) : "big" operations [as_type](as_type.lean) : treats a list as a type \ No newline at end of file diff --git a/library/data/nat/nat.md b/library/data/nat/nat.md index de5fa6ba99..19439db4a0 100644 --- a/library/data/nat/nat.md +++ b/library/data/nat/nat.md @@ -7,4 +7,6 @@ The natural numbers. * [order](order.lean) : less-than, less-then-or-equal, etc. * [bquant](bquant.lean) : bounded quantifiers * [sub](sub.lean) : subtraction, and distance -* [div](div.lean) : div, mod, gcd, and lcm \ No newline at end of file +* [div](div.lean) : div, mod, gcd, and lcm +* [power](power.lean) +* [bigops](bigops.lean) : finite sums and products \ No newline at end of file diff --git a/library/data/nat/power.lean b/library/data/nat/power.lean index 048b860515..8421555e83 100644 --- a/library/data/nat/power.lean +++ b/library/data/nat/power.lean @@ -5,7 +5,7 @@ Authors: Leonardo de Moura, Jeremy Avigad The power function on the natural numbers. -/ -import data.nat.basic data.nat.order data.nat.div algebra.group_pow +import data.nat.basic data.nat.order data.nat.div algebra.group_power namespace nat