From d2b5af237e5fcc43ccecece8a33b135539fafe2b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 3 Nov 2014 18:57:55 -0800
Subject: [PATCH] refactor(library): use new 'structure' command to define prod
 and sigma

---
 library/data/prod.lean             | 10 ++--------
 library/data/sigma.lean            | 11 ++---------
 tests/lean/run/structure_test.lean |  2 +-
 3 files changed, 5 insertions(+), 18 deletions(-)

diff --git a/library/data/prod.lean b/library/data/prod.lean
index 6accd74255..dd4681fb19 100644
--- a/library/data/prod.lean
+++ b/library/data/prod.lean
@@ -8,9 +8,8 @@ import logic.inhabited logic.eq logic.decidable general_notation
 
 open inhabited decidable eq.ops
 
--- The cartesian product.
-inductive prod (A B : Type) : Type :=
-  mk : A → B → prod A B
+structure prod (A B : Type) :=
+mk :: (pr1 : A) (pr2 : B)
 
 definition pair := @prod.mk
 
@@ -24,8 +23,6 @@ namespace prod
   protected theorem destruct {P : A × B → Prop} (p : A × B) (H : ∀a b, P (a, b)) : P p :=
   rec H p
 
-  definition pr1 (p : prod A B) := rec (λ x y, x) p
-  definition pr2 (p : prod A B) := rec (λ x y, y) p
   notation `pr₁` := pr1
   notation `pr₂` := pr2
 
@@ -37,9 +34,6 @@ namespace prod
   theorem pr2.pair : pr₂ (a, b) = b :=
   rfl
 
-  protected theorem eta (p : prod A B) : pair (pr₁ p) (pr₂ p) = p :=
-  destruct p (λx y, eq.refl (x, y))
-
   variables {a₁ a₂ : A} {b₁ b₂ : B}
 
   theorem pair_eq : a₁ = a₂ → b₁ = b₂ → (a₁, b₁) = (a₂, b₂) :=
diff --git a/library/data/sigma.lean b/library/data/sigma.lean
index 411d4fa33c..55609bf624 100644
--- a/library/data/sigma.lean
+++ b/library/data/sigma.lean
@@ -4,8 +4,8 @@
 import logic.inhabited logic.cast
 open inhabited eq.ops
 
-inductive sigma {A : Type} (B : A → Type) : Type :=
-dpair : Πx : A, B x → sigma B
+structure sigma {A : Type} (B : A → Type) :=
+dpair :: (dpr1 : A) (dpr2 : B dpr1)
 
 notation `Σ` binders `,` r:(scoped P, sigma P) := r
 
@@ -13,19 +13,12 @@ namespace sigma
   universe variables u v
   variables {A A' : Type.{u}} {B : A → Type.{v}} {B' : A' → Type.{v}}
 
-  --without reducible tag, slice.composition_functor in algebra.category.constructions fails
-  definition dpr1 [reducible] (p : Σ x, B x) : A := rec (λ a b, a) p
-  definition dpr2 [reducible] (p : Σ x, B x) : B (dpr1 p) := rec (λ a b, b) p
-
   theorem dpr1_dpair (a : A) (b : B a) : dpr1 (dpair a b) = a := rfl
   theorem dpr2_dpair (a : A) (b : B a) : dpr2 (dpair a b) = b := rfl
 
   protected theorem destruct {P : sigma B → Prop} (p : sigma B) (H : ∀a b, P (dpair a b)) : P p :=
   rec H p
 
-  protected theorem eta (p : sigma B) : dpair (dpr1 p) (dpr2 p) = p :=
-  destruct p (take a b, rfl)
-
   theorem dpair_eq {a₁ a₂ : A} {b₁ : B a₁} {b₂ : B a₂} (H₁ : a₁ = a₂) (H₂ : eq.rec_on H₁ b₁ = b₂) :
     dpair a₁ b₁ = dpair a₂ b₂ :=
   dcongr_arg2 dpair H₁ H₂
diff --git a/tests/lean/run/structure_test.lean b/tests/lean/run/structure_test.lean
index f268a33d71..767f78b39c 100644
--- a/tests/lean/run/structure_test.lean
+++ b/tests/lean/run/structure_test.lean
@@ -18,7 +18,7 @@ section
   include E
    -- include Ha
 
-  structure point3d_color (B C : Type) (D : B → Type) extends point (foo A) B, sigma D renaming x→y a→w :=
+  structure point3d_color (B C : Type) (D : B → Type) extends point (foo A) B, sigma D renaming dpr1→y dpr2→w :=
   mk :: (c : color) (H : x == y)
 
   check point3d_color.c