feat(builtin): add num type (the base type that will be used to build nat, int, real)

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/builtin/CMakeLists.txt

@@ -96,6 +96,7 @@ add_theory("specialfn.lean"    "${CMAKE_CURRENT_BINARY_DIR}/Real.olean")
 add_theory("subtype.lean"      "${CMAKE_CURRENT_BINARY_DIR}/Nat.olean")
 add_theory("optional.lean"     "${CMAKE_CURRENT_BINARY_DIR}/subtype.olean")
 add_theory("sum.lean"          "${CMAKE_CURRENT_BINARY_DIR}/optional.olean")
+add_theory("num.lean"          "${CMAKE_CURRENT_BINARY_DIR}/Nat.olean")
 
 update_interface("kernel.olean"       "kernel" "-n")
 update_interface("Nat.olean"          "library/arith" "-n")

src/builtin/num.lean

@@ -0,0 +1,104 @@
+import macros
+import subtype
+using subtype
+
+namespace num
+theorem inhabited_ind : inhabited 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,
+      inhabited_intro w
+
+definition S := ε (inhabited_ex_intro infinity) (λ f, injective f ∧ non_surjective f)
+definition Z := ε inhabited_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 inhabited_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
+
+definition num := subtype ind N
+
+theorem inhab : inhabited num
+:= subtype_inhabited (exists_intro Z N_Z)
+
+definition zero : num
+:= abst Z inhab
+
+theorem zero_pred : N Z
+:= N_Z
+
+definition succ (n : num) : num
+:= abst (S (rep n)) inhab
+
+theorem succ_pred (n : num) : N (S (rep n))
+:= have N_n : N (rep n),
+     from P_rep n,
+   show N (S (rep n)),
+     from N_S N_n
+
+theorem succ_inj (a b : num) : succ a = succ b → a = b
+:= assume Heq1 : succ a = succ b,
+   have Heq2 : S (rep a) = S (rep b),
+      from abst_inj inhab (succ_pred a) (succ_pred b) Heq1,
+   have rep_eq : (rep a) = (rep b),
+      from injective_S (rep a) (rep b) Heq2,
+   show a = b,
+      from rep_inj rep_eq
+
+theorem succ_nz (a : num) : succ a ≠ zero
+:= assume R : succ a = zero,
+   have Heq1 : S (rep a) = Z,
+      from abst_inj inhab (succ_pred a) zero_pred R,
+   show false,
+      from absurd Heq1 (S_ne_Z (rep a))
+
+theorem induction {P : num → Bool} (H1 : P zero) (H2 : ∀ n, P n → P (succ n)) : ∀ a, P a
+:= take a,
+   let Q := λ x, N x ∧ P (abst x inhab)
+   in have QZ : Q Z,
+        from and_intro zero_pred H1,
+      have QS : ∀ x, Q x → Q (S x),
+        from take x, assume Qx,
+               have Hp1 : P (succ (abst x inhab)),
+                 from H2 (abst x inhab) (and_elimr Qx),
+               have Hp2 : P (abst (S (rep (abst x inhab))) inhab),
+                 from Hp1,
+               have Nx : N x,
+                 from and_eliml Qx,
+               have rep_eq : rep (abst x inhab) = x,
+                 from rep_abst inhab x Nx,
+               show Q (S x),
+                 from and_intro (N_S Nx) (subst Hp2 rep_eq),
+      have Qa : P (abst (rep a) inhab),
+        from and_elimr (N_smallest Q QZ QS (rep a) (P_rep a)),
+      have abst_eq : abst (rep a) inhab = a,
+        from abst_rep inhab a,
+      show P a,
+        from subst Qa abst_eq
+
+set_opaque num  true
+set_opaque Z    true
+set_opaque S    true
+set_opaque zero true
+set_opaque succ true
+end
+
+definition num := num::num