From 7f25dd6646e4dd461862945680fc11cfd427af43 Mon Sep 17 00:00:00 2001
From: Jeremy Avigad <avigad@cmu.edu>
Date: Thu, 31 Dec 2015 12:51:20 -0800
Subject: [PATCH] feat(library/data/nat/bigops): sums and products over
 intervals of natural numbers

---
 library/algebra/algebra.md    |   2 +-
 library/algebra/interval.lean |  19 ++++
 library/data/nat/bigops.lean  | 199 ++++++++++++++++++++++++++++++++++
 3 files changed, 219 insertions(+), 1 deletion(-)
 create mode 100644 library/data/nat/bigops.lean

diff --git a/library/algebra/algebra.md b/library/algebra/algebra.md
index edef40b0d9..59af7d8a91 100644
--- a/library/algebra/algebra.md
+++ b/library/algebra/algebra.md
@@ -7,7 +7,7 @@ Algebraic structures.
 * [relation](relation.lean)
 * [binary](binary.lean) : binary operations
 * [order](order.lean)
-* [intervals](intervals.lean)
+* [interval](interval.lean)
 * [lattice](lattice.lean)
 * [complete lattice](complete_lattice.lean)
 * [group](group.lean)
diff --git a/library/algebra/interval.lean b/library/algebra/interval.lean
index 84e130e5c5..98ba3bcad8 100644
--- a/library/algebra/interval.lean
+++ b/library/algebra/interval.lean
@@ -107,6 +107,25 @@ open nat eq.ops
   proposition Icc_zero (n : ℕ) : '[0, n] = '(-∞, n] :=
   have '[0, n] = '[0, ∞) ∩ '(-∞, n], from rfl,
   by+ rewrite [this, Icu_zero, univ_inter]
+
+  proposition bij_on_add_Icc_zero (m n : ℕ) : bij_on (add m) ('[0, n]) ('[m, m+n]) :=
+  have mapsto : ∀₀ i ∈ '[0, n], m + i ∈ '[m, m+n], from
+    (take i, assume imem,
+      have H1 : m ≤ m + i, from !le_add_right,
+      have H2 : m + i ≤ m + n, from add_le_add_left (and.right imem) m,
+      show m + i ∈ '[m, m+n], from and.intro H1 H2),
+  have injon : inj_on (add m) ('[0, n]), from
+    (take i j, assume Hi Hj H, !eq_of_add_eq_add_left H),
+  have surjon : surj_on (add m) ('[0, n]) ('[m, m+n]), from
+    (take j, assume Hj : j ∈ '[m, m+n],
+      obtain lej jle, from Hj,
+      let i := j - m in
+      have ile : i ≤ n, from calc
+        j - m ≤ m + n - m : nat.sub_le_sub_right jle m
+          ... = n         : nat.add_sub_cancel_left,
+      have iadd : m + i = j, by rewrite add.comm; apply nat.sub_add_cancel lej,
+      exists.intro i (and.intro (and.intro !zero_le ile) iadd)),
+  bij_on.mk mapsto injon surjon
 end nat
 
 section nat -- put the instances in the intervals namespace
diff --git a/library/data/nat/bigops.lean b/library/data/nat/bigops.lean
new file mode 100644
index 0000000000..cb97ca40d8
--- /dev/null
+++ b/library/data/nat/bigops.lean
@@ -0,0 +1,199 @@
+/-
+Copyright (c) 2015 Jeremy Avigad. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Jeremy Avigad
+
+Finite sums and products over intervals of natural numbers.
+-/
+import data.nat.order algebra.group_bigops algebra.interval
+
+namespace nat
+
+/- sums -/
+
+section add_monoid
+
+variables {A : Type} [add_monoid A]
+
+definition sum_up_to (n : ℕ) (f : ℕ → A) : A :=
+  nat.rec_on n 0 (λ n a, a + f n)
+
+notation `∑` binders ` < ` n `, ` r:(scoped f, sum_up_to n f) := r
+
+proposition sum_up_to_zero (f : ℕ → A) : (∑ i < 0, f i) = 0 := rfl
+
+proposition sum_up_to_succ (n : ℕ) (f : ℕ → A) : (∑ i < succ n, f i) = (∑ i < n, f i) + f n := rfl
+
+proposition sum_up_to_one (f : ℕ → A) : (∑ i < 1, f i) = f 0 := zero_add (f 0)
+
+definition sum_range (m n : ℕ) (f : ℕ → A) : A := sum_up_to (succ n - m) (λ i, f (i + m))
+
+notation `∑` binders `=` m `...` n `, ` r:(scoped f, sum_range m n f) := r
+
+proposition sum_range_def (m n : ℕ) (f : ℕ → A) :
+            (∑ i = m...n, f i) = (∑ i < (succ n - m), f (i + m)) := rfl
+
+proposition sum_range_self (m : ℕ) (f : ℕ → A) :
+            (∑ i = m...m, f i) = f m :=
+  by rewrite [↑sum_range, succ_sub !le.refl, nat.sub_self, sum_up_to_one, zero_add]
+
+proposition sum_range_succ {m n : ℕ} (f : ℕ → A) (H : m ≤ succ n) :
+            (∑ i = m...succ n, f i) = (∑ i = m...n, f i) + f (succ n) :=
+  by rewrite [↑sum_range, succ_sub H, sum_up_to_succ, nat.sub_add_cancel H]
+
+proposition sum_up_to_succ_eq_sum_range_zero (n : ℕ) (f : ℕ → A) :
+            (∑ i < succ n, f i) = (∑ i = 0...n, f i) := rfl
+
+end add_monoid
+
+section finset
+  variables {A : Type} [add_comm_monoid A]
+  open finset
+
+proposition sum_up_to_eq_Sum_upto (n : ℕ) (f : ℕ → A) :
+            (∑ i < n, f i) = (∑ i ∈ upto n, f i) :=
+begin
+  induction n with n ih,
+    {exact rfl},
+  have H : upto n ∩ '{n} = ∅, from
+    inter_eq_empty
+      (take x,
+        suppose x ∈ upto n,
+        have x < n, from lt_of_mem_upto this,
+        suppose x ∈ '{n},
+        have x = n, using this, by rewrite -mem_singleton_iff; apply this,
+        have n < n, from eq.subst this `x < n`,
+        show false, from !lt.irrefl this),
+  rewrite [sum_up_to_succ, ih, upto_succ, Sum_union _ H, Sum_singleton]
+end
+
+end finset
+
+section set
+  variables {A : Type} [add_comm_monoid A]
+  open set intervals
+
+proposition sum_range_eq_sum_interval_aux (m n : ℕ) (f : ℕ → A) :
+            (∑ i = m...m+n, f i) = (∑ i ∈ '[m, m + n], f i) :=
+begin
+  induction n with n ih,
+    {rewrite [nat.add_zero, sum_range_self, Icc_self, Sum_singleton]},
+  have H : m ≤ succ (m + n), from le_of_lt (lt_of_le_of_lt !le_add_right !lt_succ_self),
+  have H' : '[m, m + n] ∩ '{succ (m + n)} = ∅, from
+    eq_empty_of_forall_not_mem (take x, assume H1,
+      have x = succ (m + n), from eq_of_mem_singleton (and.right H1),
+      have succ (m + n) ≤ m + n, from eq.subst this (and.right (and.left H1)),
+      show false, from not_lt_of_ge this !lt_succ_self),
+  rewrite [add_succ, sum_range_succ f H, Icc_eq_Icc_union_Ioc !le_add_right !le_succ,
+           nat.Ioc_eq_Icc_succ, Icc_self, Sum_union f H', Sum_singleton, ih]
+end
+
+proposition sum_range_eq_sum_interval {m n : ℕ} (f : ℕ → A) (H : m ≤ n) :
+            (∑ i = m...n, f i) = (∑ i ∈ '[m, n], f i) :=
+  have n = m + (n - m), by rewrite [add.comm, nat.sub_add_cancel H],
+  using this, by rewrite this; apply sum_range_eq_sum_interval_aux
+
+proposition sum_range_offset (m n : ℕ) (f : ℕ → A) :
+            (∑ i = m...m+n, f i) = (∑ i = 0...n, f (m + i)) :=
+  have bij_on (add m) ('[0, n]) ('[m, m+n]), from !nat.bij_on_add_Icc_zero,
+  by+ rewrite [-zero_add n at {2}, *sum_range_eq_sum_interval_aux, Sum_eq_of_bij_on f this, zero_add]
+
+end set
+
+/- products -/
+
+section monoid
+
+variables {A : Type} [monoid A]
+
+definition prod_up_to (n : ℕ) (f : ℕ → A) : A :=
+  nat.rec_on n 1 (λ n a, a * f n)
+
+notation `∏` binders ` < ` n `, ` r:(scoped f, prod_up_to n f) := r
+
+proposition prod_up_to_zero (f : ℕ → A) : (∏ i < 0, f i) = 1 := rfl
+
+proposition prod_up_to_succ (n : ℕ) (f : ℕ → A) : (∏ i < succ n, f i) = (∏ i < n, f i) * f n := rfl
+
+proposition prod_up_to_one (f : ℕ → A) : (∏ i < 1, f i) = f 0 := one_mul (f 0)
+
+definition prod_range (m n : ℕ) (f : ℕ → A) : A := prod_up_to (succ n - m) (λ i, f (i + m))
+
+notation `∏` binders `=` m `...` n `, ` r:(scoped f, prod_range m n f) := r
+
+proposition prod_range_def (m n : ℕ) (f : ℕ → A) :
+            (∏ i = m...n, f i) = (∏ i < (succ n - m), f (i + m)) := rfl
+
+proposition prod_range_self (m : ℕ) (f : ℕ → A) :
+            (∏ i = m...m, f i) = f m :=
+by rewrite [↑prod_range, succ_sub !le.refl, nat.sub_self, prod_up_to_one, zero_add]
+
+proposition prod_range_succ {m n : ℕ} (f : ℕ → A) (H : m ≤ succ n) :
+            (∏ i = m...succ n, f i) = (∏ i = m...n, f i) * f (succ n) :=
+by rewrite [↑prod_range, succ_sub H, prod_up_to_succ, nat.sub_add_cancel H]
+
+proposition prod_up_to_succ_eq_prod_range_zero (n : ℕ) (f : ℕ → A) :
+            (∏ i < succ n, f i) = (∏ i = 0...n, f i) := rfl
+
+end monoid
+
+section finset
+  variables {A : Type} [comm_monoid A]
+  open finset
+
+proposition prod_up_to_eq_Prod_upto (n : ℕ) (f : ℕ → A) :
+            (∏ i < n, f i) = (∏ i ∈ upto n, f i) :=
+begin
+  induction n with n ih,
+    {exact rfl},
+  have H : upto n ∩ '{n} = ∅, from
+    inter_eq_empty
+      (take x,
+        suppose x ∈ upto n,
+        have x < n, from lt_of_mem_upto this,
+        suppose x ∈ '{n},
+        have x = n, using this, by rewrite -mem_singleton_iff; apply this,
+        have n < n, from eq.subst this `x < n`,
+        show false, from !lt.irrefl this),
+  rewrite [prod_up_to_succ, ih, upto_succ, Prod_union _ H, Prod_singleton]
+end
+
+end finset
+
+section set
+  variables {A : Type} [comm_monoid A]
+  open set intervals
+
+proposition prod_range_eq_prod_interval_aux (m n : ℕ) (f : ℕ → A) :
+            (∏ i = m...m+n, f i) = (∏ i ∈ '[m, m + n], f i) :=
+begin
+  induction n with n ih,
+    {rewrite [nat.add_zero, prod_range_self, Icc_self, Prod_singleton]},
+  have H : m ≤ succ (m + n), from le_of_lt (lt_of_le_of_lt !le_add_right !lt_succ_self),
+  have H' : '[m, m + n] ∩ '{succ (m + n)} = ∅, from
+    eq_empty_of_forall_not_mem (take x, assume H1,
+      have x = succ (m + n), from eq_of_mem_singleton (and.right H1),
+      have succ (m + n) ≤ m + n, from eq.subst this (and.right (and.left H1)),
+      show false, from not_lt_of_ge this !lt_succ_self),
+  rewrite [add_succ, prod_range_succ f H, Icc_eq_Icc_union_Ioc !le_add_right !le_succ,
+           nat.Ioc_eq_Icc_succ, Icc_self, Prod_union f H', Prod_singleton, ih]
+end
+
+proposition prod_range_eq_prod_interval {m n : ℕ} (f : ℕ → A) (H : m ≤ n) :
+            (∏ i = m...n, f i) = (∏ i ∈ '[m, n], f i) :=
+  have n = m + (n - m), by rewrite [add.comm, nat.sub_add_cancel H],
+  using this, by rewrite this; apply prod_range_eq_prod_interval_aux
+
+proposition prod_range_offset (m n : ℕ) (f : ℕ → A) :
+            (∏ i = m...m+n, f i) = (∏ i = 0...n, f (m + i)) :=
+  have bij_on (add m) ('[0, n]) ('[m, m+n]), from !nat.bij_on_add_Icc_zero,
+  by+ rewrite [-zero_add n at {2}, *prod_range_eq_prod_interval_aux, Prod_eq_of_bij_on f this,
+               zero_add]
+
+end set
+
+
+
+
+
+end nat