michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(library/algebra/group_bigops.lean,library/data/nat/bigops.lean): add ext principle, clean up file

Browse source
This commit is contained in:
Jeremy Avigad 2015-05-17 16:00:38 +10:00
parent 4764f6e8ec
commit 9720d84095
2 changed files with 44 additions and 37 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

44
library/algebra/group_bigops.lean
View file

@ -99,9 +99,11 @@ section comm_monoid
theorem Prod_empty (f : A → B) : Prod ∅ f = 1 := theorem Prod_empty (f : A → B) : Prod ∅ f = 1 :=
Prodl_nil f Prodl_nil f
section 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 :=
variable [H : decidable_eq A] quot.induction_on s (take u, !Prodl_mul)
include H
section deceqA
include deceqA
theorem Prod_insert_of_mem (f : A → B) {a : A} {s : finset A} : theorem Prod_insert_of_mem (f : A → B) {a : A} {s : finset A} :
a ∈ s → Prod (insert a s) f = Prod s f := a ∈ s → Prod (insert a s) f = Prod s f :=
@ -119,10 +121,19 @@ section comm_monoid
quot.induction_on₂ s₁ s₂ quot.induction_on₂ s₁ s₂
(λ l₁ l₂ d, Prodl_union f d), (λ l₁ l₂ d, Prodl_union f d),
H1 (disjoint_of_inter_empty disj) 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 := theorem Prod_ext {s : finset A} {f g : A → B} :
quot.induction_on s (take u, !Prodl_mul) (∀{x}, x ∈ s → f x = g x) → Prod s f = Prod s g :=
finset.induction_on s
(assume H, rfl)
(take s' x, assume H1 : x ∉ s',
assume IH : (∀ {x : A}, x ∈ s' → f x = g x) → Prod s' f = Prod s' g,
assume H2 : ∀{y}, y ∈ insert x s' → f y = g y,
assert H3 : ∀y, y ∈ s' → f y = g y, from
take y, assume H', H2 (mem_insert_of_mem _ H'),
assert H4 : f x = g x, from H2 !mem_insert,
by rewrite [Prod_insert_of_not_mem f H1, Prod_insert_of_not_mem g H1, IH H3, H4])
end deceqA
end comm_monoid end comm_monoid
section add_monoid section add_monoid
@ -141,16 +152,15 @@ section add_monoid
theorem Suml_append (l₁ l₂ : list A) (f : A → B) : Suml (l₁++l₂) f = Suml l₁ f + Suml l₂ f := theorem Suml_append (l₁ l₂ : list A) (f : A → B) : Suml (l₁++l₂) f = Suml l₁ f + Suml l₂ f :=
Prodl_append l₁ l₂ f Prodl_append l₁ l₂ f
section decidable_eq section deceqA
variable [H : decidable_eq A] include deceqA
include H
theorem Suml_insert_of_mem (f : A → B) {a : A} {l : list A} (H : a ∈ l) : theorem Suml_insert_of_mem (f : A → B) {a : A} {l : list A} (H : a ∈ l) :
Suml (insert a l) f = Suml l f := Prodl_insert_of_mem f H Suml (insert a l) f = Suml l f := Prodl_insert_of_mem f H
theorem Suml_insert_of_not_mem (f : A → B) {a : A} {l : list A} (H : a ∉ l) : theorem Suml_insert_of_not_mem (f : A → B) {a : A} {l : list A} (H : a ∉ l) :
Suml (insert a l) f = f a + Suml l f := Prodl_insert_of_not_mem f H Suml (insert a l) f = f a + Suml l f := Prodl_insert_of_not_mem f H
theorem Suml_union {l₁ l₂ : list A} (f : A → B) (d : disjoint l₁ l₂) : theorem Suml_union {l₁ l₂ : list A} (f : A → B) (d : disjoint l₁ l₂) :
Suml (union l₁ l₂) f = Suml l₁ f + Suml l₂ f := Prodl_union f d Suml (union l₁ l₂) f = Suml l₁ f + Suml l₂ f := Prodl_union f d
end decidable_eq end deceqA
end add_monoid end add_monoid
section add_comm_monoid section add_comm_monoid
@ -175,20 +185,20 @@ section add_comm_monoid
notation `∑` binders `∈` s, r:(scoped f, Sum s f) := r notation `∑` binders `∈` s, r:(scoped f, Sum s f) := r
theorem Sum_empty (f : A → B) : Sum ∅ f = 0 := Prod_empty f theorem Sum_empty (f : A → B) : Sum ∅ f = 0 := Prod_empty f
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
section decidable_eq section deceqA
variable [H : decidable_eq A] include deceqA
include H
theorem Sum_insert_of_mem (f : A → B) {a : A} {s : finset A} (H : a ∈ s) : 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 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) : 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 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₂ = ∅) : 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 Sum (s₁ ∪ s₂) f = Sum s₁ f + Sum s₂ f := Prod_union f disj
end decidable_eq theorem Sum_ext {s : finset A} {f g : A → B} (H : ∀x, x ∈ s → f x = g x) :
Sum s f = Sum s g := Prod_ext H
theorem Sum_add (s : finset A) (f g : A → B) : end deceqA
Sum s (λx, f x + g x) = Sum s f + Sum s g := Prod_mul s f g
end add_comm_monoid end add_comm_monoid
end algebra end algebra

37
library/data/nat/bigops.lean
View file

@ -23,7 +23,8 @@ theorem Prodl_cons (f : A → nat) (a : A) (l : list A) : Prodl (a::l) f = f a *
algebra.Prodl_cons f a l algebra.Prodl_cons f a l
theorem Prodl_append (l₁ l₂ : list A) (f : A → nat) : Prodl (l₁++l₂) f = Prodl l₁ f * Prodl l₂ f := theorem Prodl_append (l₁ l₂ : list A) (f : A → nat) : Prodl (l₁++l₂) f = Prodl l₁ f * Prodl l₂ f :=
algebra.Prodl_append l₁ l₂ f algebra.Prodl_append l₁ l₂ f
theorem Prodl_mul (l : list A) (f g : A → nat) :
Prodl l (λx, f x * g x) = Prodl l f * Prodl l g := algebra.Prodl_mul l f g
section deceqA section deceqA
include deceqA include deceqA
theorem Prodl_insert_of_mem (f : A → nat) {a : A} {l : list A} (H : a ∈ l) : theorem Prodl_insert_of_mem (f : A → nat) {a : A} {l : list A} (H : a ∈ l) :
@ -34,16 +35,14 @@ section deceqA
Prodl (union l₁ l₂) f = Prodl l₁ f * Prodl l₂ f := algebra.Prodl_union f d Prodl (union l₁ l₂) f = Prodl l₁ f * Prodl l₂ f := algebra.Prodl_union f d
end deceqA end deceqA
theorem Prodl_mul (l : list A) (f g : A → nat) :
Prodl l (λx, f x * g x) = Prodl l f * Prodl l g := algebra.Prodl_mul l f g
/- Prod -/ /- Prod -/
definition Prod (s : finset A) (f : A → nat) : nat := algebra.Prod s f definition Prod (s : finset A) (f : A → nat) : nat := algebra.Prod s f
notation `∏` binders `∈` s, r:(scoped f, Prod s f) := r 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.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
section deceqA section deceqA
include deceqA include deceqA
theorem Prod_insert_of_mem (f : A → nat) {a : A} {s : finset A} (H : a ∈ s) : theorem Prod_insert_of_mem (f : A → nat) {a : A} {s : finset A} (H : a ∈ s) :
@ -52,11 +51,10 @@ section deceqA
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.Prod_insert_of_not_mem f H
theorem Prod_union (f : A → nat) {s₁ s₂ : finset A} (disj : s₁ ∩ s₂ = ∅) : 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.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
end deceqA end deceqA
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
/- Suml -/ /- Suml -/
definition Suml (l : list A) (f : A → nat) : nat := algebra.Suml l f definition Suml (l : list A) (f : A → nat) : nat := algebra.Suml l f
@ -67,7 +65,8 @@ theorem Suml_cons (f : A → nat) (a : A) (l : list A) : Suml (a::l) f = f a + S
algebra.Suml_cons f a l algebra.Suml_cons f a l
theorem Suml_append (l₁ l₂ : list A) (f : A → nat) : Suml (l₁++l₂) f = Suml l₁ f + Suml l₂ f := theorem Suml_append (l₁ l₂ : list A) (f : A → nat) : Suml (l₁++l₂) f = Suml l₁ f + Suml l₂ f :=
algebra.Suml_append l₁ l₂ f algebra.Suml_append l₁ l₂ f
theorem Suml_add (l : list A) (f g : A → nat) : Suml l (λx, f x + g x) = Suml l f + Suml l g :=
algebra.Suml_add l f g
section deceqA section deceqA
include deceqA include deceqA
theorem Suml_insert_of_mem (f : A → nat) {a : A} {l : list A} (H : a ∈ l) : theorem Suml_insert_of_mem (f : A → nat) {a : A} {l : list A} (H : a ∈ l) :
@ -78,26 +77,24 @@ section deceqA
Suml (union l₁ l₂) f = Suml l₁ f + Suml l₂ f := algebra.Suml_union f d Suml (union l₁ l₂) f = Suml l₁ f + Suml l₂ f := algebra.Suml_union f d
end deceqA end deceqA
theorem Suml_add (l : list A) (f g : A → nat) : Suml l (λx, f x + g x) = Suml l f + Suml l g :=
algebra.Suml_add l f g
/- Sum -/ /- Sum -/
definition Sum (s : finset A) (f : A → nat) : nat := algebra.Sum s f definition Sum (s : finset A) (f : A → nat) : nat := algebra.Sum s f
notation `∑` binders `∈` s, r:(scoped f, Sum s f) := r 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.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
section deceqA section deceqA
include deceqA include deceqA
theorem Sum_insert_of_mem (f : A → nat) {a : A} {s : finset A} (H : a ∈ s) : 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.Sum_insert_of_mem f H
theorem Sum_insert_of_not_mem (f : A → nat) {a : A} {s : finset A} (H : a ∉ s) : 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.Sum_insert_of_not_mem f H
theorem Sum_union (f : A → nat) {s₁ s₂ : finset A} (disj : s₁ ∩ s₂ = ∅) : 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.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
end deceqA end deceqA
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
end nat end nat