From 2b7bc7b67371342aa4e68e5f0e1f6a3af4a842a5 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 31 Jan 2014 17:59:57 -0800
Subject: [PATCH] test(tests/lean/exp): simulating HOL constructions

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 tests/lean/exp/nat.lean | 41 +++++++++++++++++++++++++++++++++++++++++
 1 file changed, 41 insertions(+)
 create mode 100644 tests/lean/exp/nat.lean

diff --git a/tests/lean/exp/nat.lean b/tests/lean/exp/nat.lean
new file mode 100644
index 000000000..98acf60eb
--- /dev/null
+++ b/tests/lean/exp/nat.lean
@@ -0,0 +1,41 @@
+import macros
+
+definition injective {A B : (Type U)} (f : A → B)  := ∀ x1 x2, f x1 = f x2 → x1 = x2
+definition non_surjective {A B : (Type U)} (f : A → B) := ∃ y, ∀ x, ¬ f x = y
+
+-- The set of individuals
+variable ind : Type
+-- ind is infinite, i.e., there is a function f s.t. f is injective, and not surjective
+axiom infinity : ∃ f : ind → ind, injective f ∧ non_surjective f
+
+theorem nonempty_ind : nonempty ind
+-- We use as the witness for non-emptiness, the value w in ind that is not convered by f.
+:= obtain f His, from infinity,
+   obtain w Hw, from and_elimr His,
+      nonempty_intro w
+
+definition S := ε (nonempty_ex_intro infinity) (λ f, injective f ∧ non_surjective f)
+definition Z := ε nonempty_ind (λ y, ∀ x, ¬ S x = y)
+
+theorem injective_S      : injective S
+:= and_eliml (exists_to_eps infinity)
+
+theorem non_surjective_S : non_surjective S
+:= and_elimr (exists_to_eps infinity)
+
+theorem S_ne_Z (i : ind) : S i ≠ Z
+:= obtain w Hw, from non_surjective_S,
+     eps_ax nonempty_ind w Hw i
+
+definition N (i : ind) : Bool
+:= ∀ P, P Z → (∀ x, P x → P (S x)) → P i
+
+theorem N_Z : N Z
+:= λ P Hz Hi, Hz
+
+theorem N_S (i : ind) (H : N i) : N (S i)
+:= λ P Hz Hi, Hi i (H P Hz Hi)
+
+theorem N_smallest : ∀ P : ind → Bool, P Z → (∀ x, P x → P (S x)) → (∀ i, N i → P i)
+:= λ P Hz Hi i Hni, Hni P Hz Hi
+