From 795acc70a6a50e114a92324b9154f4e127e9c319 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 9 Apr 2015 19:30:09 -0700
Subject: [PATCH] refactor(library/data/finset): move finset to its own
 directory

---
 .../data/{finset.lean => finset/basic.lean}   | 46 +++++++++++++++----
 library/data/finset/default.lean              | 10 ++++
 library/data/list/basic.lean                  |  2 +-
 tests/lean/run/finset1.lean                   | 20 +++++++-
 4 files changed, 65 insertions(+), 13 deletions(-)
 rename library/data/{finset.lean => finset/basic.lean} (81%)
 create mode 100644 library/data/finset/default.lean

diff --git a/library/data/finset.lean b/library/data/finset/basic.lean
similarity index 81%
rename from library/data/finset.lean
rename to library/data/finset/basic.lean
index 02545ee14..1b2a09d2e 100644
--- a/library/data/finset.lean
+++ b/library/data/finset/basic.lean
@@ -155,6 +155,32 @@ theorem card_erase_of_not_mem {a : A} {s : finset A} : a ∉ s → card (erase a
 quot.induction_on s (λ l nainl, list.length_erase_of_not_mem nainl)
 end erase
 
+/- disjoint -/
+definition disjoint (s₁ s₂ : finset A) : Prop :=
+quot.lift_on₂ s₁ s₂ (λ l₁ l₂, disjoint (elt_of l₁) (elt_of l₂))
+  (λ v₁ v₂ w₁ w₂ p₁ p₂, propext (iff.intro
+    (λ d₁ a, and.intro
+      (λ ainw₁ : a ∈ elt_of w₁,
+        have ainv₁  : a ∈ elt_of v₁, from mem_perm (perm.symm p₁) ainw₁,
+        have nainv₂ : a ∉ elt_of v₂, from disjoint_left d₁ ainv₁,
+        not_mem_perm p₂ nainv₂)
+      (λ ainw₂ : a ∈ elt_of w₂,
+        have ainv₂ : a ∈ elt_of v₂,  from mem_perm (perm.symm p₂) ainw₂,
+        have nainv₁ : a ∉ elt_of v₁, from disjoint_right d₁ ainv₂,
+        not_mem_perm p₁ nainv₁))
+    (λ d₂ a, and.intro
+      (λ ainv₁ : a ∈ elt_of v₁,
+        have ainw₁  : a ∈ elt_of w₁, from mem_perm p₁ ainv₁,
+        have nainw₂ : a ∉ elt_of w₂, from disjoint_left d₂ ainw₁,
+        not_mem_perm (perm.symm p₂) nainw₂)
+      (λ ainv₂ : a ∈ elt_of v₂,
+        have ainw₂  : a ∈ elt_of w₂, from mem_perm p₂ ainv₂,
+        have nainw₁ : a ∉ elt_of w₁, from disjoint_right d₂ ainw₂,
+        not_mem_perm (perm.symm p₁) nainw₁))))
+
+theorem disjoint.comm {s₁ s₂ : finset A} : disjoint s₁ s₂ → disjoint s₂ s₁ :=
+quot.induction_on₂ s₁ s₂ (λ l₁ l₂ d, list.disjoint.comm d)
+
 /- union -/
 section union
 variable [h : decidable_eq A]
@@ -209,20 +235,20 @@ end union
 /- acc -/
 section acc
 variable {B : Type}
-definition acc (f : B → A → B) (rcomm : ∀ b a₁ a₂, f (f b a₁) a₂ = f (f b a₂) a₁) (b : B) (s : finset A) : B :=
+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)
 
-definition bigsum (s : finset A) (f : A → nat) : nat :=
-acc (compose_right nat.add f) (right_commutative_compose_right nat.add f nat.add.right_comm) 0 s
+section union
+variable [h : decidable_eq A]
+include h
 
-definition bigprod (s : finset A) (f : A → nat) : nat :=
-acc (compose_right nat.mul f) (right_commutative_compose_right nat.mul f nat.mul.right_comm) 1 s
+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
 
-definition bigand (s : finset A) (p : A → Prop) : Prop :=
-acc (compose_right and p) (right_commutative_compose_right and p (λ a b c, propext (and.right_comm a b c))) true s
-
-definition bigor (s : finset A) (p : A → Prop) : Prop :=
-acc (compose_right or p) (right_commutative_compose_right or p (λ a b c, propext (or.right_comm a b c))) false s
 end acc
 end finset
diff --git a/library/data/finset/default.lean b/library/data/finset/default.lean
new file mode 100644
index 000000000..8f1d99146
--- /dev/null
+++ b/library/data/finset/default.lean
@@ -0,0 +1,10 @@
+/-
+Copyright (c) 2015 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Module: data.finset
+Author: Leonardo de Moura
+
+Finite sets
+-/
+import data.finset.basic
diff --git a/library/data/list/basic.lean b/library/data/list/basic.lean
index 9ac9e3223..92e02a9f4 100644
--- a/library/data/list/basic.lean
+++ b/library/data/list/basic.lean
@@ -1083,7 +1083,7 @@ theorem foldl_union_of_disjoint (f : B → A → B) (b : B) {l₁ l₂ : list A}
         : foldl f b (union l₁ l₂) = foldl f (foldl f b l₁) l₂ :=
 by rewrite [union_eq_append d, foldl_append]
 
-theorem foldr_union_of_dijoint  (f : A → B → B) (b : B) (l₁ l₂ : list A) (d : disjoint l₁ l₂)
+theorem foldr_union_of_dijoint  (f : A → B → B) (b : B) {l₁ l₂ : list A} (d : disjoint l₁ l₂)
         : foldr f b (union l₁ l₂) = foldr f (foldr f b l₂) l₁ :=
 by rewrite [union_eq_append d, foldr_append]
 end union
diff --git a/tests/lean/run/finset1.lean b/tests/lean/run/finset1.lean
index 3d095a78e..81f492877 100644
--- a/tests/lean/run/finset1.lean
+++ b/tests/lean/run/finset1.lean
@@ -1,5 +1,21 @@
-import data.finset
-open nat list finset
+import data.finset algebra.function algebra.binary
+open nat list finset function binary
+
+variable {A : Type}
+
+-- TODO define for group
+definition bigsum (s : finset A) (f : A → nat) : nat :=
+acc (compose_right nat.add f) (right_commutative_compose_right nat.add f nat.add.right_comm) 0 s
+
+definition bigprod (s : finset A) (f : A → nat) : nat :=
+acc (compose_right nat.mul f) (right_commutative_compose_right nat.mul f nat.mul.right_comm) 1 s
+
+definition bigand (s : finset A) (p : A → Prop) : Prop :=
+acc (compose_right and p) (right_commutative_compose_right and p (λ a b c, propext (and.right_comm a b c))) true s
+
+definition bigor (s : finset A) (p : A → Prop) : Prop :=
+acc (compose_right or p) (right_commutative_compose_right or p (λ a b c, propext (or.right_comm a b c))) false s
+
 
 example : to_finset [1, 3, 1] = to_finset [3, 3, 3, 1] :=
 dec_trivial