From ff701a98128a6e1f160272d40cac4d5843ff6bf7 Mon Sep 17 00:00:00 2001 From: Jeremy Avigad Date: Sat, 16 May 2015 22:26:59 +1000 Subject: [PATCH] feat(library/data/nat/bigops.lean): add finite products and sums for nat --- library/algebra/group_bigops.lean | 90 +++++++++++++-------------- library/algebra/ring.lean | 2 +- library/data/nat/bigops.lean | 100 ++++++++++++++++++++++++++++++ 3 files changed, 144 insertions(+), 48 deletions(-) create mode 100644 library/data/nat/bigops.lean diff --git a/library/algebra/group_bigops.lean b/library/algebra/group_bigops.lean index 9bda92e1c..eb36ffa51 100644 --- a/library/algebra/group_bigops.lean +++ b/library/algebra/group_bigops.lean @@ -60,19 +60,17 @@ namespace list -- i.e. algebra.list 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_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] + 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 @@ -120,30 +118,30 @@ namespace finset list.prod_nil f section decidable_eq - variable [H : decidable_eq A] - include H + 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_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_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_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) + end decidable_eq 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 -/ @@ -169,15 +167,14 @@ namespace list 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 + 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 @@ -210,19 +207,18 @@ namespace finset theorem sum_empty (f : A → B) : sum ∅ f = 0 := prod_empty f section decidable_eq - variable [H : decidable_eq A] - include H + 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 + end decidable_eq - 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 diff --git a/library/algebra/ring.lean b/library/algebra/ring.lean index 67f32f299..2c1569b0e 100644 --- a/library/algebra/ring.lean +++ b/library/algebra/ring.lean @@ -63,7 +63,7 @@ end semiring /- comm semiring -/ -structure comm_semiring [class] (A : Type) extends semiring A, comm_semigroup A +structure comm_semiring [class] (A : Type) extends semiring A, comm_monoid A -- TODO: we could also define a cancelative comm_semiring, i.e. satisfying -- c ≠ 0 → c * a = c * b → a = b. diff --git a/library/data/nat/bigops.lean b/library/data/nat/bigops.lean new file mode 100644 index 000000000..8c9624dc2 --- /dev/null +++ b/library/data/nat/bigops.lean @@ -0,0 +1,100 @@ +/- +Copyright (c) 2015 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: Jeremy Avigad + +Finite products and sums on the natural numbers. +-/ +import data.nat.basic data.nat.order algebra.group_bigops +open list + +namespace nat + open [classes] algebra + local attribute nat.comm_semiring [instance] + variable {A : Type} + + /- list.prod and list.sum -/ + + definition list.prod (l : list A) (f : A → nat) : nat := algebra.list.prod l f + notation `∏` binders `←` l, r:(scoped f, list.prod l f) := r + definition list.sum (l : list A) (f : A → nat) : nat := algebra.list.sum l f + notation `∑` binders `←` l, r:(scoped f, list.sum l f) := r + + namespace list -- i.e. nat.list + open list -- i.e. ordinary lists + + theorem prod_nil (f : A → nat) : prod [] f = 1 := algebra.list.prod_nil f + theorem prod_cons (f : A → nat) (a : A) (l : list A) : prod (a::l) f = f a * prod l f := + algebra.list.prod_cons f a l + theorem prod_append (l₁ l₂ : list A) (f : A → nat) : prod (l₁++l₂) f = prod l₁ f * prod l₂ f := + algebra.list.prod_append l₁ l₂ f + section decidable_eq + variable [H : decidable_eq A] + include H + theorem prod_insert_of_mem (f : A → nat) {a : A} {l : list A} (H : a ∈ l) : + prod (insert a l) f = prod l f := algebra.list.prod_insert_of_mem f H + theorem prod_insert_of_not_mem (f : A → nat) {a : A} {l : list A} (H : a ∉ l) : + prod (insert a l) f = f a * prod l f := algebra.list.prod_insert_of_not_mem f H + theorem prod_union {l₁ l₂ : list A} (f : A → nat) (d : disjoint l₁ l₂) : + prod (union l₁ l₂) f = prod l₁ f * prod l₂ f := algebra.list.prod_union f d + end decidable_eq + theorem prod_mul (l : list A) (f g : A → nat) : + prod l (λx, f x * g x) = prod l f * prod l g := algebra.list.prod_mul l f g + + theorem sum_nil (f : A → nat) : sum [] f = 0 := algebra.list.sum_nil f + theorem sum_cons (f : A → nat) (a : A) (l : list A) : sum (a::l) f = f a + sum l f := + algebra.list.sum_cons f a l + theorem sum_append (l₁ l₂ : list A) (f : A → nat) : sum (l₁++l₂) f = sum l₁ f + sum l₂ f := + algebra.list.sum_append l₁ l₂ f + section decidable_eq + variable [H : decidable_eq A] + include H + theorem sum_insert_of_mem (f : A → nat) {a : A} {l : list A} (H : a ∈ l) : + sum (insert a l) f = sum l f := algebra.list.sum_insert_of_mem f H + theorem sum_insert_of_not_mem (f : A → nat) {a : A} {l : list A} (H : a ∉ l) : + sum (insert a l) f = f a + sum l f := algebra.list.sum_insert_of_not_mem f H + theorem sum_union {l₁ l₂ : list A} (f : A → nat) (d : disjoint l₁ l₂) : + sum (union l₁ l₂) f = sum l₁ f + sum l₂ f := algebra.list.sum_union f d + end decidable_eq + theorem sum_add (l : list A) (f g : A → nat) : sum l (λx, f x + g x) = sum l f + sum l g := + algebra.list.sum_add l f g + end list + + /- finset.prod and finset.sum -/ + + definition finset.prod (s : finset A) (f : A → nat) : nat := algebra.finset.prod s f + notation `∏` binders `∈` s, r:(scoped f, finset.prod s f) := r + definition finset.sum (s : finset A) (f : A → nat) : nat := algebra.finset.sum s f + notation `∑` binders `∈` s, r:(scoped f, finset.sum s f) := r + + namespace finset + open finset + theorem prod_empty (f : A → nat) : finset.prod ∅ f = 1 := algebra.finset.prod_empty f + section decidable_eq + variable [H : decidable_eq A] + include H + theorem prod_insert_of_mem (f : A → nat) {a : A} {s : finset A} (H : a ∈ s) : + prod (insert a s) f = prod s f := algebra.finset.prod_insert_of_mem f H + theorem prod_insert_of_not_mem (f : A → nat) {a : A} {s : finset A} (H : a ∉ s) : + prod (insert a s) f = f a * prod s f := algebra.finset.prod_insert_of_not_mem f H + theorem prod_union (f : A → nat) {s₁ s₂ : finset A} (disj : s₁ ∩ s₂ = ∅) : + prod (s₁ ∪ s₂) f = prod s₁ f * prod s₂ f := algebra.finset.prod_union f disj + end decidable_eq + theorem prod_mul (s : finset A) (f g : A → nat) : prod s (λx, f x * g x) = prod s f * prod s g := + algebra.finset.prod_mul s f g + + theorem sum_empty (f : A → nat) : finset.sum ∅ f = 0 := algebra.finset.sum_empty f + section decidable_eq + variable [H : decidable_eq A] + include H + theorem sum_insert_of_mem (f : A → nat) {a : A} {s : finset A} (H : a ∈ s) : + sum (insert a s) f = sum s f := algebra.finset.sum_insert_of_mem f H + theorem sum_insert_of_not_mem (f : A → nat) {a : A} {s : finset A} (H : a ∉ s) : + sum (insert a s) f = f a + sum s f := algebra.finset.sum_insert_of_not_mem f H + theorem sum_union (f : A → nat) {s₁ s₂ : finset A} (disj : s₁ ∩ s₂ = ∅) : + sum (s₁ ∪ s₂) f = sum s₁ f + sum s₂ f := algebra.finset.sum_union f disj + end decidable_eq + theorem sum_add (s : finset A) (f g : A → nat) : sum s (λx, f x + g x) = sum s f + sum s g := + algebra.finset.sum_add s f g + end finset +end nat