From 5caa983919db36f973b340a4a76f22e08a0a3611 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 10 Apr 2015 06:13:32 -0700
Subject: [PATCH] feat(library/data/finset): redefine bigop for finset

---
 library/data/finset/basic.lean | 20 --------------------
 library/data/finset/bigop.lean | 34 ++++++++++++++++++++++++----------
 2 files changed, 24 insertions(+), 30 deletions(-)

diff --git a/library/data/finset/basic.lean b/library/data/finset/basic.lean
index c215324ef..02dfc52c9 100644
--- a/library/data/finset/basic.lean
+++ b/library/data/finset/basic.lean
@@ -231,24 +231,4 @@ theorem empty_union (s : finset A) : ∅ ∪ s = s :=
 calc ∅ ∪ s = s ∪ ∅ : union.comm
        ... = s     : union_empty
 end union
-
-/- acc -/
-section acc
-variable {B : Type}
-variables (f : B → A → B) (rcomm : right_commutative f) (b : B)
-
-definition acc  (s : finset A) : B :=
-quot.lift_on s (λ l : nodup_list A, list.foldl f b (elt_of l))
-  (λ l₁ l₂ p, foldl_eq_of_perm rcomm p b)
-
-section union
-variable [h : decidable_eq A]
-include h
-
-definition acc_union {s₁ s₂ : finset A} : disjoint s₁ s₂ → acc f rcomm b (s₁ ∪ s₂) = acc f rcomm (acc f rcomm b s₁) s₂ :=
-quot.induction_on₂ s₁ s₂
-  (λ l₁ l₂ d, foldl_union_of_disjoint f b d)
-end union
-
-end acc
 end finset
diff --git a/library/data/finset/bigop.lean b/library/data/finset/bigop.lean
index 565ccf97e..ac8f2a8eb 100644
--- a/library/data/finset/bigop.lean
+++ b/library/data/finset/bigop.lean
@@ -5,22 +5,36 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Module: data.finset
 Author: Leonardo de Moura
 
-Finite sets big operators
+Big operator for finite sets
 -/
-import algebra.group data.finset.basic
-open algebra finset function binary quot
+import algebra.group data.finset.basic data.list.bigop
+open algebra finset function binary quot subtype
 
 namespace finset
 variables {A B : Type}
 variable  [g : comm_group B]
 include g
 
-protected definition mulf (f : A → B) : B → A → B :=
-λ b a, b * f a
-
-protected theorem mulf_rcomm (f : A → B) : right_commutative (mulf f) :=
-right_commutative_compose_right (@has_mul.mul B g) f (@mul.right_comm B g)
-
 definition bigop (s : finset A) (f : A → B) : B :=
-acc (mulf f) (mulf_rcomm f) 1 s
+quot.lift_on s
+  (λ l, list.bigop (elt_of l) f)
+  (λ l₁ l₂ p, list.bigop_of_perm f p)
+
+theorem bigop_empty (f : A → B) : bigop ∅ f = 1 :=
+list.bigop_nil f
+
+variable [H : decidable_eq A]
+include H
+
+theorem bigop_insert_of_mem (f : A → B) {a : A} {s : finset A} : a ∈ s → bigop (insert a s) f = bigop s f :=
+quot.induction_on s
+  (λ l ainl, list.bigop_insert_of_mem f ainl)
+
+theorem bigop_insert_of_not_mem (f : A → B) {a : A} {s : finset A} : a ∉ s → bigop (insert a s) f = f a * bigop s f :=
+quot.induction_on s
+  (λ l nainl, list.bigop_insert_of_not_mem f nainl)
+
+theorem bigop_union (f : A → B) {s₁ s₂ : finset A} : disjoint s₁ s₂ → bigop (s₁ ∪ s₂) f = bigop s₁ f * bigop s₂ f :=
+quot.induction_on₂ s₁ s₂
+  (λ l₁ l₂ d, list.bigop_union f d)
 end finset