From 608e2838bf747277c663d88b90405df27ca8fb60 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 10 Apr 2015 05:52:19 -0700
Subject: [PATCH] feat(library/data/list): define bigop for lists

---
 library/data/list/bigop.lean | 50 ++++++++++++++++++++++++++++++++++--
 1 file changed, 48 insertions(+), 2 deletions(-)

diff --git a/library/data/list/bigop.lean b/library/data/list/bigop.lean
index 7403e4175..eabe8b966 100644
--- a/library/data/list/bigop.lean
+++ b/library/data/list/bigop.lean
@@ -5,6 +5,52 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Module: data.list.bigop
 Authors: Leonardo de Moura
 
-Big operators for lists
+Big operator for lists
 -/
-import data.list.comb
+import algebra.group data.list.comb data.list.set
+open algebra function binary quot
+
+namespace list
+variables {A B : Type}
+variable  [g : group B]
+include g
+
+protected definition mulf (f : A → B) : B → A → B :=
+λ b a, b * f a
+
+definition bigop (l : list A) (f : A → B) : B :=
+foldl (mulf f) 1 l
+
+private theorem foldl_const (f : A → B) : ∀ (l : list A) (b : B), foldl (mulf f) b l = b * foldl (mulf f) 1 l
+| []     b := by rewrite [*foldl_nil, mul_one]
+| (a::l) b := by rewrite [*foldl_cons, foldl_const, {foldl _ (list.mulf f 1 a) _}foldl_const, ↑mulf, one_mul, mul.assoc]
+
+theorem bigop_nil (f : A → B) : bigop [] f = 1 :=
+rfl
+
+theorem bigop_cons (f : A → B) (a : A) (l : list A) : bigop (a::l) f = f a * bigop l f :=
+by rewrite [↑bigop, foldl_cons, foldl_const, ↑mulf, one_mul]
+
+theorem bigop_append : ∀ (l₁ l₂ : list A) (f : A → B), bigop (l₁++l₂) f = bigop l₁ f * bigop l₂ f
+| []    l₂ f  := by rewrite [append_nil_left, bigop_nil, one_mul]
+| (a::l) l₂ f := by rewrite [append_cons, *bigop_cons, bigop_append, mul.assoc]
+
+section insert
+variable [H : decidable_eq A]
+include H
+
+theorem bigop_insert_of_mem (f : A → B) {a : A} {l : list A} : a ∈ l → bigop (insert a l) f = bigop l f :=
+assume ainl, by rewrite [insert_eq_of_mem ainl]
+
+theorem bigop_insert_of_not_mem (f : A → B) {a : A} {l : list A} : a ∉ l → bigop (insert a l) f = f a * bigop l f :=
+assume nainl, by rewrite [insert_eq_of_not_mem nainl, bigop_cons]
+end insert
+
+section union
+variable [H : decidable_eq A]
+include H
+
+definition bigop_union {l₁ l₂ : list A} (f : A → B) (d : disjoint l₁ l₂) : bigop (union l₁ l₂) f = bigop l₁ f * bigop l₂ f :=
+by rewrite [union_eq_append d, bigop_append]
+end union
+end list