From 0e3b13f1a0e80c893136be2debe8ee6a65742e82 Mon Sep 17 00:00:00 2001 From: Jeremy Avigad Date: Sat, 19 Dec 2015 14:10:20 -0500 Subject: [PATCH] refactor(library/algebra): combine group_bigops and group_set_bigops --- library/algebra/algebra.md | 7 +- library/algebra/group_bigops.lean | 117 +++++++++++++++++- library/algebra/group_set_bigops.lean | 102 --------------- .../number_theory/prime_factorization.lean | 2 +- 4 files changed, 114 insertions(+), 114 deletions(-) delete mode 100644 library/algebra/group_set_bigops.lean diff --git a/library/algebra/algebra.md b/library/algebra/algebra.md index 7b150b647..8d7bca16a 100644 --- a/library/algebra/algebra.md +++ b/library/algebra/algebra.md @@ -11,15 +11,12 @@ Algebraic structures. * [complete lattice](complete_lattice.lean) * [group](group.lean) * [group_power](group_power.lean) : nat and int powers -* [group_bigops](group_bigops.lean) : products and sums over finsets -* [group_set_bigops](group_set_bigops.lean) : products and sums over finite sets +* [group_bigops](group_bigops.lean) : products and sums over lists, finsets and sets * [ring](ring.lean) * [ordered_group](ordered_group.lean) * [ordered_ring](ordered_ring.lean) -* [ring_power](ring_power.lean) : power in ring structures * [field](field.lean) * [ordered_field](ordered_field.lean) +* [ring_power](ring_power.lean) : power in ring structures * [bundled](bundled.lean) : bundled versions of the algebraic structures * [category](category/category.md) : category theory (outdated, see HoTT category theory folder) - -We set a low priority for algebraic operations, so that the elaborator tries concrete structures first. \ No newline at end of file diff --git a/library/algebra/group_bigops.lean b/library/algebra/group_bigops.lean index ea04e14aa..87b6fc714 100644 --- a/library/algebra/group_bigops.lean +++ b/library/algebra/group_bigops.lean @@ -3,20 +3,25 @@ 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. +Finite products on a monoid, and finite sums on an additive monoid. There are three versions: + + Prodl, Suml : products and sums over lists + Prod, Sum (in namespace finset) : products and sums over finsets + Prod, Sum (in namespace set) : products and sums over finite sets 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. - -Bigops based on finsets go in the namespace algebra.finset. There are also versions based on sets, -defined in group_set_bigops.lean. +import basic files from nat. -/ -import .group .group_power data.list.basic data.list.perm data.finset.basic +import .group .group_power data.list.basic data.list.perm data.finset.basic data.set.finite open function binary quot subtype list finset variables {A B : Type} variable [deceqA : decidable_eq A] +/- +-- list versions. +-/ + /- Prodl: product indexed by a list -/ section monoid @@ -99,6 +104,10 @@ section comm_monoid by rewrite [*Prodl_cons, IH, *mul.assoc, mul.left_comm (Prodl l f)]) end comm_monoid +/- +-- finset versions +-/ + /- Prod: product indexed by a finset -/ namespace finset @@ -231,3 +240,99 @@ namespace finset theorem Sum_zero (s : finset A) : Sum s (λ x, 0) = (0:B) := Prod_one s end finset + +/- +-- set versions +-/ + +namespace set +open classical + +/- Prod: product indexed by a set -/ + +section Prod + variable [cmB : comm_monoid B] + include cmB + + noncomputable definition Prod (s : set A) (f : A → B) : B := finset.Prod (to_finset s) f + + -- ∏ x ∈ s, f x + notation `∏` binders `∈` s, r:(scoped f, prod s f) := r + + theorem Prod_empty (f : A → B) : Prod ∅ f = 1 := + by rewrite [↑Prod, to_finset_empty] + + theorem Prod_of_not_finite {s : set A} (nfins : ¬ finite s) (f : A → B) : Prod s f = 1 := + by rewrite [↑Prod, to_finset_of_not_finite nfins] + + theorem Prod_mul (s : set A) (f g : A → B) : Prod s (λx, f x * g x) = Prod s f * Prod s g := + by rewrite [↑Prod, finset.Prod_mul] + + theorem Prod_insert_of_mem (f : A → B) {a : A} {s : set A} (H : a ∈ s) : + Prod (insert a s) f = Prod s f := + by_cases + (suppose finite s, + assert (#finset a ∈ set.to_finset s), by rewrite mem_to_finset_eq; apply H, + by rewrite [↑Prod, to_finset_insert, finset.Prod_insert_of_mem f this]) + (assume nfs : ¬ finite s, + assert ¬ finite (insert a s), from assume H, nfs (finite_of_finite_insert H), + by rewrite [Prod_of_not_finite nfs, Prod_of_not_finite this]) + + theorem Prod_insert_of_not_mem (f : A → B) {a : A} {s : set A} [finite s] (H : a ∉ s) : + Prod (insert a s) f = f a * Prod s f := + assert (#finset a ∉ set.to_finset s), by rewrite mem_to_finset_eq; apply H, + by rewrite [↑Prod, to_finset_insert, finset.Prod_insert_of_not_mem f this] + + theorem Prod_union (f : A → B) {s₁ s₂ : set A} [finite s₁] [finite s₂] + (disj : s₁ ∩ s₂ = ∅) : + Prod (s₁ ∪ s₂) f = Prod s₁ f * Prod s₂ f := + begin + rewrite [↑Prod, to_finset_union], + apply finset.Prod_union, + apply finset.eq_of_to_set_eq_to_set, + rewrite [finset.to_set_inter, *to_set_to_finset, finset.to_set_empty, disj] + end + + theorem Prod_ext {s : set A} {f g : A → B} (H : ∀{x}, x ∈ s → f x = g x) : Prod s f = Prod s g := + by_cases + (suppose finite s, + by esimp [Prod]; apply finset.Prod_ext; intro x; rewrite [mem_to_finset_eq]; apply H) + (assume nfs : ¬ finite s, + by rewrite [*Prod_of_not_finite nfs]) + + theorem Prod_one (s : set A) : Prod s (λ x, 1) = (1:B) := + by rewrite [↑Prod, finset.Prod_one] +end Prod + +/- Sum -/ + +section Sum + variable [acmB : add_comm_monoid B] + include acmB + local attribute add_comm_monoid.to_comm_monoid [trans_instance] + + noncomputable definition Sum (s : set 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 + 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 + + theorem Sum_insert_of_mem (f : A → B) {a : A} {s : set 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 : set A} [finite s] (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₂ : set A} [finite s₁] [finite s₂] + (disj : s₁ ∩ s₂ = ∅) : + Sum (s₁ ∪ s₂) f = Sum s₁ f + Sum s₂ f := Prod_union f disj + theorem Sum_ext {s : set A} {f g : A → B} (H : ∀x, x ∈ s → f x = g x) : + Sum s f = Sum s g := Prod_ext H + + theorem Sum_zero (s : set A) : Sum s (λ x, 0) = (0:B) := Prod_one s +end Sum + +end set diff --git a/library/algebra/group_set_bigops.lean b/library/algebra/group_set_bigops.lean deleted file mode 100644 index a3065a685..000000000 --- a/library/algebra/group_set_bigops.lean +++ /dev/null @@ -1,102 +0,0 @@ -/- -Copyright (c) 2015 Jeremy Avigad. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Author: Jeremy Avigad - -Set-based version of group_bigops. --/ -import .group_bigops data.set.finite -open set classical - -namespace set - -variables {A B : Type} - -/- Prod: product indexed by a set -/ - -section Prod - variable [cmB : comm_monoid B] - include cmB - - noncomputable definition Prod (s : set A) (f : A → B) : B := finset.Prod (to_finset s) f - - -- ∏ x ∈ s, f x - notation `∏` binders `∈` s, r:(scoped f, prod s f) := r - - theorem Prod_empty (f : A → B) : Prod ∅ f = 1 := - by rewrite [↑Prod, to_finset_empty] - - theorem Prod_of_not_finite {s : set A} (nfins : ¬ finite s) (f : A → B) : Prod s f = 1 := - by rewrite [↑Prod, to_finset_of_not_finite nfins] - - theorem Prod_mul (s : set A) (f g : A → B) : Prod s (λx, f x * g x) = Prod s f * Prod s g := - by rewrite [↑Prod, finset.Prod_mul] - - theorem Prod_insert_of_mem (f : A → B) {a : A} {s : set A} (H : a ∈ s) : - Prod (insert a s) f = Prod s f := - by_cases - (suppose finite s, - assert (#finset a ∈ set.to_finset s), by rewrite mem_to_finset_eq; apply H, - by rewrite [↑Prod, to_finset_insert, finset.Prod_insert_of_mem f this]) - (assume nfs : ¬ finite s, - assert ¬ finite (insert a s), from assume H, nfs (finite_of_finite_insert H), - by rewrite [Prod_of_not_finite nfs, Prod_of_not_finite this]) - - theorem Prod_insert_of_not_mem (f : A → B) {a : A} {s : set A} [finite s] (H : a ∉ s) : - Prod (insert a s) f = f a * Prod s f := - assert (#finset a ∉ set.to_finset s), by rewrite mem_to_finset_eq; apply H, - by rewrite [↑Prod, to_finset_insert, finset.Prod_insert_of_not_mem f this] - - theorem Prod_union (f : A → B) {s₁ s₂ : set A} [finite s₁] [finite s₂] - (disj : s₁ ∩ s₂ = ∅) : - Prod (s₁ ∪ s₂) f = Prod s₁ f * Prod s₂ f := - begin - rewrite [↑Prod, to_finset_union], - apply finset.Prod_union, - apply finset.eq_of_to_set_eq_to_set, - rewrite [finset.to_set_inter, *to_set_to_finset, finset.to_set_empty, disj] - end - - theorem Prod_ext {s : set A} {f g : A → B} (H : ∀{x}, x ∈ s → f x = g x) : Prod s f = Prod s g := - by_cases - (suppose finite s, - by esimp [Prod]; apply finset.Prod_ext; intro x; rewrite [mem_to_finset_eq]; apply H) - (assume nfs : ¬ finite s, - by rewrite [*Prod_of_not_finite nfs]) - - theorem Prod_one (s : set A) : Prod s (λ x, 1) = (1:B) := - by rewrite [↑Prod, finset.Prod_one] -end Prod - -/- Sum -/ - -section Sum - variable [acmB : add_comm_monoid B] - include acmB - local attribute add_comm_monoid.to_comm_monoid [trans_instance] - - noncomputable definition Sum (s : set 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 - 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 - - theorem Sum_insert_of_mem (f : A → B) {a : A} {s : set 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 : set A} [finite s] (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₂ : set A} [finite s₁] [finite s₂] - (disj : s₁ ∩ s₂ = ∅) : - Sum (s₁ ∪ s₂) f = Sum s₁ f + Sum s₂ f := Prod_union f disj - theorem Sum_ext {s : set A} {f g : A → B} (H : ∀x, x ∈ s → f x = g x) : - Sum s f = Sum s g := Prod_ext H - - theorem Sum_zero (s : set A) : Sum s (λ x, 0) = (0:B) := Prod_one s -end Sum - -end set diff --git a/library/theories/number_theory/prime_factorization.lean b/library/theories/number_theory/prime_factorization.lean index 93daba201..78625b908 100644 --- a/library/theories/number_theory/prime_factorization.lean +++ b/library/theories/number_theory/prime_factorization.lean @@ -9,7 +9,7 @@ Multiplicity and prime factors. We have: prime_factors n := the finite set of prime factors of n, assuming n > 0 -/ -import data.nat data.finset .primes algebra.group_set_bigops +import data.nat data.finset .primes algebra.group_bigops open eq.ops finset well_founded decidable namespace nat