From 811bc6a31fe7600d19ec155dd36812f758eac7f2 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 3 Dec 2014 18:54:24 -0800
Subject: [PATCH] feat(library/init/measurable): add 'measurable' type class

---
 library/init/default.lean      |  2 +-
 library/init/measurable.lean   | 39 ++++++++++++++++++++++++++++++++++
 tests/lean/run/measurable.lean |  7 ++++++
 3 files changed, 47 insertions(+), 1 deletion(-)
 create mode 100644 library/init/measurable.lean
 create mode 100644 tests/lean/run/measurable.lean

diff --git a/library/init/default.lean b/library/init/default.lean
index 41d8783c68..28e21993e6 100644
--- a/library/init/default.lean
+++ b/library/init/default.lean
@@ -7,4 +7,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
+import init.bool init.num init.sigma init.measurable
diff --git a/library/init/measurable.lean b/library/init/measurable.lean
new file mode 100644
index 0000000000..752a5e6180
--- /dev/null
+++ b/library/init/measurable.lean
@@ -0,0 +1,39 @@
+/-
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Authors: Leonardo de Moura
+-/
+prelude
+import init.nat
+open nat
+
+inductive measurable [class] (A : Type) :=
+mk : (A → nat) → measurable A
+
+definition size_of {A : Type} [s : measurable A] (a : A) : nat :=
+measurable.rec_on s (λ f, f) a
+
+definition nat.measurable [instance] : measurable nat :=
+measurable.mk (λ a, a)
+
+definition option.measurable [instance] (A : Type) (s : measurable A) : measurable (option A) :=
+measurable.mk (λ a, option.cases_on a zero (λ a, size_of a))
+
+definition prod.measurable [instance] (A B : Type) (sa : measurable A) (sb : measurable B) : measurable (prod A B) :=
+measurable.mk (λ p, prod.cases_on p (λ a b, size_of a + size_of b))
+
+definition sum.measurable [instance] (A B : Type) (sa : measurable A) (sb : measurable B) : measurable (sum A B) :=
+measurable.mk (λ s, sum.cases_on s (λ a, size_of a) (λ b, size_of b))
+
+definition bool.measurable [instance] : measurable bool :=
+measurable.mk (λb, zero)
+
+definition Prop.measurable [instance] : measurable Prop :=
+measurable.mk (λp, zero)
+
+definition unit.measurable [instance] : measurable unit :=
+measurable.mk (λu, zero)
+
+definition fn.measurable [instance] (A : Type) (B : A → Type) : measurable (Π x, B x) :=
+measurable.mk (λf, zero)
diff --git a/tests/lean/run/measurable.lean b/tests/lean/run/measurable.lean
new file mode 100644
index 0000000000..95b6c9af45
--- /dev/null
+++ b/tests/lean/run/measurable.lean
@@ -0,0 +1,7 @@
+open prod nat
+
+example (a b : nat) : size_of (a, true, bool.tt, (λ c d : nat, c + d), option.some b) = a + b :=
+rfl
+
+example : size_of (pair (pair (pair 2 true) (λ a : nat, a)) (option.some 3)) = 5 :=
+rfl