refactor(library/algebra): combine group_bigops and group_set_bigops
This commit is contained in:
Jeremy Avigad
parent
f1daf8f24e
commit
0e3b13f1a0
4 changed files with 114 additions and 114 deletions
|
|
@ -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.
|
||||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Reference in a new issue