From eaf886cb5afdefaf4be0d8cf6dca6df2f3d588c3 Mon Sep 17 00:00:00 2001 From: Jeremy Avigad Date: Fri, 7 Aug 2015 20:53:30 -0400 Subject: [PATCH] refactor(library/algebra/group_bigops,library/*): put group_bigops in 'finset' namespace, in preparation for set versions --- library/algebra/group_bigops.lean | 11 +++-- library/data/finset/bigops.lean | 16 ++++---- library/data/finset/card.lean | 2 +- library/data/finset/partition.lean | 8 ++-- library/data/nat/bigops.lean | 40 +++++++++++-------- library/data/set/basic.lean | 4 +- library/data/set/finite.lean | 2 +- library/theories/group_theory/action.lean | 4 +- library/theories/group_theory/finsubg.lean | 6 +-- .../number_theory/prime_factorization.lean | 2 +- 10 files changed, 53 insertions(+), 42 deletions(-) diff --git a/library/algebra/group_bigops.lean b/library/algebra/group_bigops.lean index 3c308ec836..291953e97c 100644 --- a/library/algebra/group_bigops.lean +++ b/library/algebra/group_bigops.lean @@ -7,6 +7,9 @@ Finite products on a monoid, and finite sums on an additive monoid. 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 .group .group_power data.list.basic data.list.perm data.finset.basic open algebra function binary quot subtype list finset @@ -99,7 +102,7 @@ end comm_monoid /- Prod: product indexed by a finset -/ -section comm_monoid +namespace finset variable [cmB : comm_monoid B] include cmB @@ -159,7 +162,7 @@ section comm_monoid theorem Prod_one (s : finset A) : Prod s (λ x, 1) = (1:B) := quot.induction_on s (take u, !Prodl_one) -end comm_monoid +end finset section add_monoid variable [amB : add_monoid B] @@ -201,7 +204,7 @@ end add_comm_monoid /- Sum -/ -section add_comm_monoid +namespace finset variable [acmB : add_comm_monoid B] include acmB local attribute add_comm_monoid.to_comm_monoid [trans-instance] @@ -228,6 +231,6 @@ section add_comm_monoid end deceqA theorem Sum_zero (s : finset A) : Sum s (λ x, 0) = (0:B) := Prod_one s -end add_comm_monoid +end finset end algebra diff --git a/library/data/finset/bigops.lean b/library/data/finset/bigops.lean index ac69062389..f9b83e674f 100644 --- a/library/data/finset/bigops.lean +++ b/library/data/finset/bigops.lean @@ -36,7 +36,7 @@ include deceqB definition Unionl (l : list A) (f : A → finset B) : finset B := algebra.Prodl l f notation `⋃` binders `←` l, r:(scoped f, Unionl l f) := r -definition Union (s : finset A) (f : A → finset B) : finset B := algebra.Prod s f +definition Union (s : finset A) (f : A → finset B) : finset B := algebra.finset.Prod s f notation `⋃` binders `∈` s, r:(scoped f, finset.Union s f) := r theorem Unionl_nil (f : A → finset B) : Unionl [] f = ∅ := algebra.Prodl_nil f @@ -57,20 +57,20 @@ section deceqA theorem Unionl_empty (l : list A) : Unionl l (λ x, ∅) = (∅ : finset B) := algebra.Prodl_one l end deceqA -theorem Union_empty (f : A → finset B) : Union ∅ f = ∅ := algebra.Prod_empty f +theorem Union_empty (f : A → finset B) : Union ∅ f = ∅ := algebra.finset.Prod_empty f theorem Union_mul (s : finset A) (f g : A → finset B) : - Union s (λx, f x ∪ g x) = Union s f ∪ Union s g := algebra.Prod_mul s f g + Union s (λx, f x ∪ g x) = Union s f ∪ Union s g := algebra.finset.Prod_mul s f g section deceqA include deceqA theorem Union_insert_of_mem (f : A → finset B) {a : A} {s : finset A} (H : a ∈ s) : - Union (insert a s) f = Union s f := algebra.Prod_insert_of_mem f H + Union (insert a s) f = Union s f := algebra.finset.Prod_insert_of_mem f H private theorem Union_insert_of_not_mem (f : A → finset B) {a : A} {s : finset A} (H : a ∉ s) : - Union (insert a s) f = f a ∪ Union s f := algebra.Prod_insert_of_not_mem f H + Union (insert a s) f = f a ∪ Union s f := algebra.finset.Prod_insert_of_not_mem f H theorem Union_union (f : A → finset B) {s₁ s₂ : finset A} (disj : s₁ ∩ s₂ = ∅) : - Union (s₁ ∪ s₂) f = Union s₁ f ∪ Union s₂ f := algebra.Prod_union f disj + Union (s₁ ∪ s₂) f = Union s₁ f ∪ Union s₂ f := algebra.finset.Prod_union f disj theorem Union_ext {s : finset A} {f g : A → finset B} (H : ∀x, x ∈ s → f x = g x) : - Union s f = Union s g := algebra.Prod_ext H - theorem Union_empty' (s : finset A) : Union s (λ x, ∅) = (∅ : finset B) := algebra.Prod_one s + Union s f = Union s g := algebra.finset.Prod_ext H + theorem Union_empty' (s : finset A) : Union s (λ x, ∅) = (∅ : finset B) := algebra.finset.Prod_one s -- this will eventually be an instance of something more general theorem inter_Union (s : finset B) (t : finset A) (f : A → finset B) : diff --git a/library/data/finset/card.lean b/library/data/finset/card.lean index 06aa6f9678..78cff73e3b 100644 --- a/library/data/finset/card.lean +++ b/library/data/finset/card.lean @@ -6,7 +6,7 @@ Author: Jeremy Avigad Cardinality calculations for finite sets. -/ import .to_set .bigops data.set.function data.nat.power data.nat.bigops -open nat eq.ops +open nat nat.finset eq.ops namespace finset diff --git a/library/data/finset/partition.lean b/library/data/finset/partition.lean index b3b1242248..f31bc5286d 100644 --- a/library/data/finset/partition.lean +++ b/library/data/finset/partition.lean @@ -45,13 +45,13 @@ begin end theorem class_equation (f : @partition A _) : - card (partition.set f) = nat.Sum (equiv_classes f) card := + card (partition.set f) = nat.finset.Sum (equiv_classes f) card := let s := (partition.set f), p := (partition.part f), img := image p s in calc card s = card (Union s p) : partition.complete f ... = card (Union img id) : image_eq_Union_index_image s p ... = card (Union (equiv_classes f) id) : rfl - ... = nat.Sum (equiv_classes f) card : card_Union_of_disjoint _ id (equiv_class_disjoint f) + ... = nat.finset.Sum (equiv_classes f) card : card_Union_of_disjoint _ id (equiv_class_disjoint f) lemma equiv_class_refl {f : A → finset A} (Pequiv : is_partition f) : ∀ a, a ∈ f a := take a, by rewrite [Pequiv a a] @@ -113,9 +113,9 @@ begin rewrite [binary_union P at {1}], apply Union_union, exact binary_inter_emp end -open nat +open nat nat.finset section -open algebra +open algebra algebra.finset variables {B : Type} [acmB : add_comm_monoid B] include acmB diff --git a/library/data/nat/bigops.lean b/library/data/nat/bigops.lean index 58e90b2345..aa188ae318 100644 --- a/library/data/nat/bigops.lean +++ b/library/data/nat/bigops.lean @@ -38,25 +38,29 @@ end deceqA /- Prod -/ -definition Prod (s : finset A) (f : A → nat) : nat := algebra.Prod s f +namespace finset + +definition Prod (s : finset A) (f : A → nat) : nat := algebra.finset.Prod s f notation `∏` binders `∈` s, r:(scoped f, Prod s f) := r -theorem Prod_empty (f : A → nat) : Prod ∅ f = 1 := algebra.Prod_empty f +theorem Prod_empty (f : A → nat) : Prod ∅ f = 1 := algebra.finset.Prod_empty f theorem Prod_mul (s : finset A) (f g : A → nat) : Prod s (λx, f x * g x) = Prod s f * Prod s g := - algebra.Prod_mul s f g + algebra.finset.Prod_mul s f g section deceqA include deceqA 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.Prod_insert_of_mem f H + 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.Prod_insert_of_not_mem f H + 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.Prod_union f disj + Prod (s₁ ∪ s₂) f = Prod s₁ f * Prod s₂ f := algebra.finset.Prod_union f disj theorem Prod_ext {s : finset A} {f g : A → nat} (H : ∀x, x ∈ s → f x = g x) : - Prod s f = Prod s g := algebra.Prod_ext H - theorem Prod_one (s : finset A) : Prod s (λ x, nat.succ 0) = 1 := algebra.Prod_one s + Prod s f = Prod s g := algebra.finset.Prod_ext H + theorem Prod_one (s : finset A) : Prod s (λ x, nat.succ 0) = 1 := algebra.finset.Prod_one s end deceqA +end finset + /- Suml -/ definition Suml (l : list A) (f : A → nat) : nat := algebra.Suml l f @@ -82,23 +86,27 @@ end deceqA /- Sum -/ -definition Sum (s : finset A) (f : A → nat) : nat := algebra.Sum s f +namespace finset + +definition Sum (s : finset A) (f : A → nat) : nat := algebra.finset.Sum s f notation `∑` binders `∈` s, r:(scoped f, Sum s f) := r -theorem Sum_empty (f : A → nat) : Sum ∅ f = 0 := algebra.Sum_empty f +theorem Sum_empty (f : A → nat) : Sum ∅ f = 0 := algebra.finset.Sum_empty f theorem Sum_add (s : finset A) (f g : A → nat) : Sum s (λx, f x + g x) = Sum s f + Sum s g := - algebra.Sum_add s f g + algebra.finset.Sum_add s f g section deceqA include deceqA 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.Sum_insert_of_mem f H + 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.Sum_insert_of_not_mem f H + 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.Sum_union f disj + Sum (s₁ ∪ s₂) f = Sum s₁ f + Sum s₂ f := algebra.finset.Sum_union f disj theorem Sum_ext {s : finset A} {f g : A → nat} (H : ∀x, x ∈ s → f x = g x) : - Sum s f = Sum s g := algebra.Sum_ext H - theorem Sum_zero (s : finset A) : Sum s (λ x, zero) = 0 := algebra.Sum_zero s + Sum s f = Sum s g := algebra.finset.Sum_ext H + theorem Sum_zero (s : finset A) : Sum s (λ x, zero) = 0 := algebra.finset.Sum_zero s end deceqA +end finset + end nat diff --git a/library/data/set/basic.lean b/library/data/set/basic.lean index 9af5769229..25153cdbe3 100644 --- a/library/data/set/basic.lean +++ b/library/data/set/basic.lean @@ -3,7 +3,7 @@ Copyright (c) 2014 Jeremy Avigad. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: Jeremy Avigad, Leonardo de Moura -/ -import logic algebra.binary +import logic.connectives algebra.binary open eq.ops binary definition set [reducible] (X : Type) := X → Prop @@ -219,7 +219,7 @@ theorem union_diff_cancel {s t : set X} [dec : Π x, decidable (x ∈ s)] (H : s setext (take x, iff.intro (assume H1 : x ∈ s ∪ (t \ s), or.elim H1 (assume H2, !H H2) (assume H2, and.left H2)) (assume H1 : x ∈ t, - decidable.by_cases + decidable.by_cases (suppose x ∈ s, or.inl this) (suppose x ∉ s, or.inr (and.intro H1 this)))) diff --git a/library/data/set/finite.lean b/library/data/set/finite.lean index 10094a2b99..4616e702d8 100644 --- a/library/data/set/finite.lean +++ b/library/data/set/finite.lean @@ -7,7 +7,7 @@ The notion of "finiteness" for sets. This approach is not computational: for exa an element s : set A satsifies finite s doesn't mean that we can compute the cardinality. For a computational representation, use the finset type. -/ -import data.set.function data.finset logic.choice +import data.set.function data.finset.card logic.choice open nat variable {A : Type} diff --git a/library/theories/group_theory/action.lean b/library/theories/group_theory/action.lean index a07b437601..afd09c1a57 100644 --- a/library/theories/group_theory/action.lean +++ b/library/theories/group_theory/action.lean @@ -249,7 +249,7 @@ lemma subg_moversets_of_orbit_eq_stab_lcosets : existsi b, subst Ph₂, assumption end)) -open nat +open nat nat.finset theorem orbit_stabilizer_theorem : card H = card (orbit hom H a) * card (stab hom H a) := calc card H = card (fin_lcosets (stab hom H a) H) * card (stab hom H a) : lagrange_theorem stab_subset @@ -297,7 +297,7 @@ take a b, propext (iff.intro (assume Peq, Peq ▸ in_orbit_refl)) variables (hom) (H) -open nat finset.partition fintype +open nat nat.finset finset.partition fintype definition orbit_partition : @partition S _ := mk univ (orbit hom H) orbit_is_partition diff --git a/library/theories/group_theory/finsubg.lean b/library/theories/group_theory/finsubg.lean index 92c0be801e..fb09c39c94 100644 --- a/library/theories/group_theory/finsubg.lean +++ b/library/theories/group_theory/finsubg.lean @@ -173,8 +173,8 @@ definition fin_lcoset_partition_subg (Psub : H ⊆ G) := open nat theorem lagrange_theorem (Psub : H ⊆ G) : card G = card (fin_lcosets H G) * card H := calc - card G = nat.Sum (fin_lcosets H G) card : class_equation (fin_lcoset_partition_subg Psub) - ... = nat.Sum (fin_lcosets H G) (λ x, card H) : nat.Sum_ext (take g P, fin_lcosets_card_eq g P) + card G = nat.finset.Sum (fin_lcosets H G) card : class_equation (fin_lcoset_partition_subg Psub) + ... = nat.finset.Sum (fin_lcosets H G) (λ x, card H) : nat.finset.Sum_ext (take g P, fin_lcosets_card_eq g P) ... = card (fin_lcosets H G) * card H : Sum_const_eq_card_mul end fin_lcoset @@ -304,7 +304,7 @@ fintype.mk (all_lcosets G H) lemma card_lcoset_type : card (lcoset_type G H) = card (fin_lcosets H G) := length_all_lcosets -open nat +open nat nat.finset variable [finsubgH : is_finsubg H] include finsubgH diff --git a/library/theories/number_theory/prime_factorization.lean b/library/theories/number_theory/prime_factorization.lean index 892bcc6b30..596a572c03 100644 --- a/library/theories/number_theory/prime_factorization.lean +++ b/library/theories/number_theory/prime_factorization.lean @@ -10,7 +10,7 @@ Multiplicity and prime factors. We have: -/ import data.nat data.finset .primes -open eq.ops finset well_founded decidable +open eq.ops finset well_founded decidable nat.finset namespace nat