From 9720d840952f9efe1618ec0526be309567507ef5 Mon Sep 17 00:00:00 2001 From: Jeremy Avigad Date: Sun, 17 May 2015 16:00:38 +1000 Subject: [PATCH] refactor(library/algebra/group_bigops.lean,library/data/nat/bigops.lean): add ext principle, clean up file --- library/algebra/group_bigops.lean | 44 +++++++++++++++++++------------ library/data/nat/bigops.lean | 37 ++++++++++++-------------- 2 files changed, 44 insertions(+), 37 deletions(-) diff --git a/library/algebra/group_bigops.lean b/library/algebra/group_bigops.lean index be4f96689..edaac182e 100644 --- a/library/algebra/group_bigops.lean +++ b/library/algebra/group_bigops.lean @@ -99,9 +99,11 @@ section comm_monoid theorem Prod_empty (f : A → B) : Prod ∅ f = 1 := Prodl_nil f - section decidable_eq - variable [H : decidable_eq A] - include H + 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, !Prodl_mul) + + section deceqA + include deceqA theorem Prod_insert_of_mem (f : A → B) {a : A} {s : finset A} : a ∈ s → Prod (insert a s) f = Prod s f := @@ -119,10 +121,19 @@ section comm_monoid quot.induction_on₂ s₁ s₂ (λ l₁ l₂ d, Prodl_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, !Prodl_mul) + theorem Prod_ext {s : finset A} {f g : A → B} : + (∀{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 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 := Prodl_append l₁ l₂ f - section decidable_eq - variable [H : decidable_eq A] - include H + section deceqA + include deceqA 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 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 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 - end decidable_eq + end deceqA end add_monoid section add_comm_monoid @@ -175,20 +185,20 @@ section add_comm_monoid notation `∑` binders `∈` s, r:(scoped f, Sum s f) := r 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 - variable [H : decidable_eq A] - include H + section deceqA + include deceqA 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_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 + 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 + end deceqA end add_comm_monoid end algebra diff --git a/library/data/nat/bigops.lean b/library/data/nat/bigops.lean index c79e5752e..c1de0b381 100644 --- a/library/data/nat/bigops.lean +++ b/library/data/nat/bigops.lean @@ -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 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 - +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 include deceqA 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 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 -/ definition Prod (s : finset A) (f : A → nat) : nat := algebra.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_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 include deceqA 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 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 + 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 -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 -/ 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 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 - +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 include deceqA 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 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 -/ definition Sum (s : finset A) (f : A → nat) : nat := algebra.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_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 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 - 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 - 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 (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) : + 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₂ = ∅) : + 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 -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