From dc2fbe6bfc22342cbf19b869a43eb35bdf6f3ef8 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 18 Jun 2016 09:49:22 -0700
Subject: [PATCH] refacto(library): move prod inhabited and has_decidable_eq
 instances to init folder

---
 library/data/prod.lean | 14 --------------
 library/init/prod.lean | 16 ++++++++++++++++
 2 files changed, 16 insertions(+), 14 deletions(-)

diff --git a/library/data/prod.lean b/library/data/prod.lean
index c9152ab49d..311abb062e 100644
--- a/library/data/prod.lean
+++ b/library/data/prod.lean
@@ -15,20 +15,6 @@ namespace prod
   protected theorem eq {p₁ p₂ : prod A B} : pr₁ p₁ = pr₁ p₂ → pr₂ p₁ = pr₂ p₂ → p₁ = p₂ :=
   destruct p₁ (take a₁ b₁, destruct p₂ (take a₂ b₂ H₁ H₂, pair_eq H₁ H₂))
 
-  protected definition is_inhabited [instance] [h₁ : inhabited A] [h₂ : inhabited B] : inhabited (prod A B) :=
-  inhabited.mk (default A, default B)
-
-  protected definition has_decidable_eq [instance] [h₁ : decidable_eq A] [h₂ : decidable_eq B] : ∀ p₁ p₂ : A × B, decidable (p₁ = p₂)
-  | (a, b) (a', b') :=
-    match h₁ a a' with
-    | tt e₁ :=
-      match h₂ b b' with
-      | tt e₂ := tt sorry -- by left; congruence; repeat assumption
-      | ff n₂ := ff sorry -- by right; intro h; injection h; contradiction
-      end
-    | ff n₁ := ff sorry -- by right; intro h; injection h; contradiction
-    end
-
   definition swap {A : Type} : A × A → A × A
   | (a, b) := (b, a)
 
diff --git a/library/init/prod.lean b/library/init/prod.lean
index ff131ff513..678b84191b 100644
--- a/library/init/prod.lean
+++ b/library/init/prod.lean
@@ -21,3 +21,19 @@ namespace prod
   end ops
 
 end prod
+
+protected definition prod.is_inhabited [instance] {A B : Type} [inhabited A] [inhabited B] : inhabited (prod A B) :=
+inhabited.mk (default A, default B)
+
+open decidable
+
+protected definition prod.has_decidable_eq [instance] {A B : Type} [h₁ : decidable_eq A] [h₂ : decidable_eq B] : ∀ p₁ p₂ : A × B, decidable (p₁ = p₂)
+| (a, b) (a', b') :=
+  match h₁ a a' with
+  | tt e₁ :=
+    match h₂ b b' with
+    | tt e₂ := tt (eq.rec_on e₁ (eq.rec_on e₂ rfl))
+    | ff n₂ := ff (assume h, prod.no_confusion h (λ e₁' e₂', absurd e₂' n₂))
+    end
+  | ff n₁ := ff (assume h, prod.no_confusion h (λ e₁' e₂', absurd e₁' n₁))
+  end