From aeaa803f9a46f3de2d55f353768d0b052bfa04fc Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 8 Feb 2014 09:07:39 -0800 Subject: [PATCH] feat(builtin): add num type (the base type that will be used to build nat, int, real) Signed-off-by: Leonardo de Moura --- src/builtin/CMakeLists.txt | 1 + src/builtin/num.lean | 104 +++++++++++++++++++++++++++++++++++++ src/builtin/obj/num.olean | Bin 0 -> 4100 bytes 3 files changed, 105 insertions(+) create mode 100644 src/builtin/num.lean create mode 100644 src/builtin/obj/num.olean diff --git a/src/builtin/CMakeLists.txt b/src/builtin/CMakeLists.txt index fcc7891c9..ba32e2edb 100644 --- a/src/builtin/CMakeLists.txt +++ b/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") diff --git a/src/builtin/num.lean b/src/builtin/num.lean new file mode 100644 index 000000000..b5016f31b --- /dev/null +++ b/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 diff --git a/src/builtin/obj/num.olean b/src/builtin/obj/num.olean new file mode 100644 index 0000000000000000000000000000000000000000..4e23f136deb6e41a0462ad6393f0f9177e6d21af GIT binary patch literal 4100 zcma)9Uuzsy6u)zK+ezJ67F|u6U!;C1qXnA~<8~bM zcDp4UVDJGfRBSclW^zkzG6TMCGs#8@i>!5nvWxR*3ZU$}`2xVZWP3%DI#}`ZlPqBn zYUgR_lTNS>jQwWwnl0rHRqXriwj_`}Ps`H8%Mdd27_u>7B+laK8r;$5$UwFc!YN$T ziIO(rlCdP2(2}18kD2u|OVYplyjsA35nBYz`(a7y;j%bn8|v5!n0(qIdYPWSiCd58 zMWAa(?U3DP1+`(pGfDOrfqFxLFA*hgv1REw#j4amQ1#Qfuaa_1vNR2GE`*s33$>Bc z*2gXL!wNO1M@cz_+D38KXgGW7-bvm*;T~=q0MttU&v9gQbtae5y^c%ObRKAfnnnuI z;dUE<@^!kxKGL{HK+661FYk14V-T(96-wUQ30tkGmq_&rZ3WhaY>6)x3LAoA*65Dx zPYL8`@o-gW5vbh^VAudE%=7Dp%Uuy?Rxu5tG;l>@!;*5oHT}4O9)V60&X8 zd^gfEr$n$(_P`|y+SRr*K^64$J2Erae$6fgvAl}VLE^WWk>#MwOwBfe-gf(DCXzY^ z@oxa~e8`K53$&s!KLF6If7C~LVI&J7$fiGJH!`F+rhQ#k%wW3H?t)LZ2gj8O)Ip$? zPeIp&ex|5xL^pID{30<#H)hh;vaksBRT&6_O7EO26kgiv8gv$eJ;3o-fII5!C&0}d z)AKvfI)GoZlGH%n9(}6SI7el`Ea&Ck8K&@Mh?@HV_W=AF;Cev?!`C^R$a|#BQDveQ zf}_=l_w!=Vt9QUe?LX6%Wi4XFYu~OEmZ@@q@PG-PJ`yAD?*Po61N;pj?-iy`$sqhe zTWm)cY{hPct)3XhC&z|-Hp*Dh#e7{e|FclwYY|=rp61L2Dqpg@@=4l`xeHzIf%B3) zY14(r_JN#d@*&N5(=`o=pRzkf|2%u|ItYIe-2wVHQ4ab;KW+8fHG4(lpLZK*9L&c6 z(#1Qt1VEy$1Cd@=@da6H_;fAov{g183;h5he*%n%$f}AgI*Y!&qTeeGsaQt}#*brt z$?uj~XA>WcV{OyX$E?6<8f3Zji{lY2J_eA6Z**kTsCZ~lCFP!&x%waJHY?2=-3s9HuPI>j*Ys54ZR!NB>a|l8DcF1me8)vQ1a2Y=bmi(*&WuyRC z!c^#ZnGmU&vxBiiNdlmCD8Aig zPn&YpAh53Q;lIESCk5z--&0vEWEbMp!LiZ2WnXA`K|Jrnj=p>g4jXmYDTggPY}LaD T1b?nW`Ii9wOY!DBe)<0oF*u-k literal 0 HcmV?d00001