From a7db8a2bacd08bc2bb175500f9a26ac44d730614 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 14 Apr 2015 20:39:58 -0700
Subject: [PATCH] theorem(library/data/countable): prove that the product of
 two countable types is countable

---
 library/data/countable.lean   | 38 ++++++++++++++++++++++++++++++++++-
 library/data/nat/default.lean |  2 +-
 2 files changed, 38 insertions(+), 2 deletions(-)

diff --git a/library/data/countable.lean b/library/data/countable.lean
index d4da9ed15b..309d8ae8d7 100644
--- a/library/data/countable.lean
+++ b/library/data/countable.lean
@@ -73,5 +73,41 @@ countable.mk
   (λ s, pickle_sum s)
   (λ n, unpickle_sum n)
   (λ s, unpickle_pickle_sum s)
-
 end sum
+
+section prod
+variables {A B : Type}
+variables [h₁ : countable A] [h₂ : countable B]
+include h₁ h₂
+
+definition pickle_prod : A × B → nat
+| (a, b) := mkpair (pickle a) (pickle b)
+
+definition unpickle_prod (n : nat) : option (A × B) :=
+match unpair n with
+| (n₁, n₂) :=
+  match unpickle A n₁ with
+  | some a :=
+    match unpickle B n₂ with
+    | some b := some (a, b)
+    | none   := none
+    end
+  | none   := none
+  end
+end
+
+theorem unpickle_pickle_prod : ∀ p : A × B, unpickle_prod (pickle_prod p) = some p
+| (a, b) :=
+  begin
+    esimp [pickle_prod, unpickle_prod, prod.cases_on],
+    rewrite [unpair_mkpair],
+    esimp,
+    rewrite [*countable.picklek]
+  end
+
+definition countable_product [instance] {A B : Type} [h₁ : countable A] [h₂ : countable B] : countable (A × B) :=
+countable.mk
+  pickle_prod
+  unpickle_prod
+  unpickle_pickle_prod
+end prod
diff --git a/library/data/nat/default.lean b/library/data/nat/default.lean
index dcb1f4ec11..3349fb2b92 100644
--- a/library/data/nat/default.lean
+++ b/library/data/nat/default.lean
@@ -3,4 +3,4 @@ Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Jeremy Avigad
 -/
-import .basic .order .sub .div .bquant .sqrt
+import .basic .order .sub .div .bquant .sqrt .pairing .power