refactor(library): reorganize init folder and add setoid

library/data/sigma.lean

@@ -17,18 +17,10 @@ namespace sigma
   definition unpack {C : (Σa, B a) → Type} {u : Σa, B a} (H : C ⟨u.1 , u.2⟩) : C u :=
   destruct u (λx y H, H) H
 
-  theorem dpair_eq {a₁ a₂ : A} {b₁ : B a₁} {b₂ : B a₂} (H₁ : a₁ = a₂) (H₂ : eq.rec_on H₁ b₁ = b₂) :
-    ⟨a₁, b₁⟩ = ⟨a₂, b₂⟩ :=
-  dcongr_arg2 mk H₁ H₂
-
   theorem dpair_heq {a : A} {a' : A'} {b : B a} {b' : B' a'}
       (HB : B == B') (Ha : a == a') (Hb : b == b') : ⟨a, b⟩ == ⟨a', b'⟩ :=
   hcongr_arg4 @mk (heq.type_eq Ha) HB Ha Hb
 
-  protected theorem equal {p₁ p₂ : Σa : A, B a} :
-    ∀(H₁ : p₁.1 = p₂.1) (H₂ : eq.rec_on H₁ p₁.2 = p₂.2), p₁ = p₂ :=
-  destruct p₁ (take a₁ b₁, destruct p₂ (take a₂ b₂ H₁ H₂, dpair_eq H₁ H₂))
-
   protected theorem hequal {p : Σa : A, B a} {p' : Σa' : A', B' a'} (HB : B == B') :
     ∀(H₁ : p.1 == p'.1) (H₂ : p.2 == p'.2), p == p' :=
   destruct p (take a₁ b₁, destruct p' (take a₂ b₂ H₁ H₂, dpair_heq HB H₁ H₂))

library/init/default.lean

@@ -8,4 +8,4 @@ Authors: Leonardo de Moura
 prelude
 import init.datatypes init.reserved_notation init.tactic init.logic
 import init.relation init.wf init.nat init.wf_k init.prod init.priority
-import init.bool init.num init.sigma init.measurable
+import init.bool init.num init.sigma init.measurable init.setoid

library/init/relation.lean

@@ -20,6 +20,8 @@ definition symmetric := ∀⦃x y⦄, x ≺ y → y ≺ x
 
 definition transitive := ∀⦃x y z⦄, x ≺ y → y ≺ z → x ≺ z
 
+definition equivalence := reflexive R ∧ symmetric R ∧ transitive R
+
 definition irreflexive := ∀x, ¬ x ≺ x
 
 definition anti_symmetric := ∀⦃x y⦄, x ≺ y → y ≺ x → x = y

library/init/setoid.lean

@@ -0,0 +1,28 @@
+/-
+Copyright (c) 2015 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Authors: Leonardo de Moura
+-/
+prelude
+import init.relation
+
+structure setoid [class] (A : Type) :=
+(r : A → A → Prop) (iseqv : equivalence r)
+
+namespace setoid
+  infix `≈` := setoid.r
+
+  variable {A : Type}
+  variable [s : setoid A]
+  include s
+
+  theorem refl (a : A) : a ≈ a :=
+  and.elim_left (@setoid.iseqv A s) a
+
+  theorem symm {a b : A} : a ≈ b → b ≈ a :=
+  λ H, and.elim_left (and.elim_right (@setoid.iseqv A s)) a b H
+
+  theorem trans {a b c : A} : a ≈ b → b ≈ c → a ≈ c :=
+  λ H₁ H₂, and.elim_right (and.elim_right (@setoid.iseqv A s)) a b c H₁ H₂
+end setoid

library/init/sigma.lean

@@ -29,6 +29,13 @@ namespace sigma
   variable  (Ra  : A → A → Prop)
   variable  (Rb  : ∀ a, B a → B a → Prop)
 
+  theorem dpair_eq : ∀ {a₁ a₂ : A} {b₁ : B a₁} {b₂ : B a₂} (H₁ : a₁ = a₂), eq.rec_on H₁ b₁ = b₂ → ⟨a₁, b₁⟩ = ⟨a₂, b₂⟩
+  | a₁ a₁ b₁ b₁ rfl rfl := rfl
+
+  protected theorem equal {p₁ p₂ : Σa : A, B a} :
+    ∀(H₁ : p₁.1 = p₂.1) (H₂ : eq.rec_on H₁ p₁.2 = p₂.2), p₁ = p₂ :=
+  destruct p₁ (take a₁ b₁, destruct p₂ (take a₂ b₂ H₁ H₂, dpair_eq H₁ H₂))
+
   -- Lexicographical order based on Ra and Rb
   inductive lex : sigma B → sigma B → Prop :=
   | left  : ∀{a₁ b₁} a₂ b₂, Ra a₁ a₂   → lex ⟨a₁, b₁⟩ ⟨a₂, b₂⟩
@@ -59,6 +66,5 @@ namespace sigma
   -- The lexicographical order of well founded relations is well-founded
   definition lex.wf (Ha : well_founded Ra) (Hb : ∀ x, well_founded (Rb x)) : well_founded (lex Ra Rb) :=
   well_founded.intro (λp, destruct p (λa b, lex.accessible (Ha a) Hb b))
-
   end
 end sigma