feat(library/init/measurable): add 'measurable' type class

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

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)

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