From fa4b60963b536dc9f45f79a6cf2a09de3a702a55 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 8 Feb 2014 10:55:34 -0800 Subject: [PATCH] feat(builtin/num): define lt predicate, and prove basic theorems Signed-off-by: Leonardo de Moura --- src/builtin/num.lean | 62 ++++++++++++++++++++++++++++++++++++++ src/builtin/obj/num.olean | Bin 4095 -> 6452 bytes 2 files changed, 62 insertions(+) diff --git a/src/builtin/num.lean b/src/builtin/num.lean index b5016f31b..8f938cb31 100644 --- a/src/builtin/num.lean +++ b/src/builtin/num.lean @@ -94,11 +94,73 @@ theorem induction {P : num → Bool} (H1 : P zero) (H2 : ∀ n, P n → P (succ show P a, from subst Qa abst_eq +theorem induction_on {P : num → Bool} (a : num) (H1 : P zero) (H2 : ∀ n, P n → P (succ n)) : P a +:= induction H1 H2 a + +definition lt (m n : num) := ∃ P, (∀ i, P (succ i) → P i) ∧ P m ∧ ¬ P n +infix 50 < : lt + +theorem lt_elim {m n : num} {B : Bool} (H1 : m < n) + (H2 : ∀ (P : num → Bool), (∀ i, P (succ i) → P i) → P m → ¬ P n → B) + : B +:= obtain P Pdef, from H1, + H2 P (and_eliml Pdef) (and_eliml (and_elimr Pdef)) (and_elimr (and_elimr Pdef)) + +theorem lt_intro {m n : num} {P : num → Bool} (H1 : ∀ i, P (succ i) → P i) (H2 : P m) (H3 : ¬ P n) : m < n +:= exists_intro P (and_intro H1 (and_intro H2 H3)) + +set_opaque lt true + +theorem lt_nrefl (n : num) : ¬ (n < n) +:= not_intro + (assume N : n < n, + lt_elim N (λ P Pred Pn nPn, absurd Pn nPn)) + +theorem lt_succ {m n : num} : succ m < n → m < n +:= assume H : succ m < n, + lt_elim H + (λ (P : num → Bool) (Pred : ∀ i, P (succ i) → P i) (Psm : P (succ m)) (nPn : ¬ P n), + have Pm : P m, + from Pred m Psm, + show m < n, + from lt_intro Pred Pm nPn) + +theorem not_lt_zero (n : num) : ¬ (n < zero) +:= induction_on n + (show ¬ (zero < zero), + from lt_nrefl zero) + (λ (n : num) (iH : ¬ (n < zero)), + show ¬ (succ n < zero), + from not_intro + (assume N : succ n < zero, + have nLTzero : n < zero, + from lt_succ N, + show false, + from absurd nLTzero iH)) + +theorem z_lt_succ_z : zero < succ zero +:= let P : num → Bool := λ x, x = zero + in have Pred : ∀ i, P (succ i) → P i, + from take i, assume Ps : P (succ i), + have si_eq_z : succ i = zero, + from Ps, + have si_ne_z : succ i ≠ zero, + from succ_nz i, + show P i, + from absurd_elim (P i) si_eq_z (succ_nz i), + have Pz : P zero, + from (refl zero), + have nPs : ¬ P (succ zero), + from succ_nz zero, + show zero < succ zero, + from lt_intro Pred Pz nPs + set_opaque num true set_opaque Z true set_opaque S true set_opaque zero true set_opaque succ true +set_opaque lt true end definition num := num::num diff --git a/src/builtin/obj/num.olean b/src/builtin/obj/num.olean index 49a7901a7f7c6bac0d86286511c3633485b94f53..8d769ae92ba9595c57ebb6a3a817a938d6f84b3b 100644 GIT binary patch literal 6452 zcma)BU2I%O6`r}f>2=u<+?A+hKmwFBb|P94w}3E}EJaDZgYUW@fInS{K6B@obNkxXU6NTs2@(w z%$)yo=FGX9b}MV-E6rAB+@Ec(uC>>@=EvE3p0$iy%{96O+SxeUeReG~-SeiLo%Wpb}3;3GC9oKdA+l-K7;}UDL?`dE6u#weO7h~1!+=ic5rMe6M!WE(JwSW zMv}{lh!c6cOI_JTZW+5D+R2atqeY1rBNo%Ebs-1oJpgJiu&OwvzGLN1?gy5p$tC;? z18RzWUWk44B%Iy#HYrqIbvauxWo|4HmPLKGrVbe_0&jLXW+&5L@O&0vZxD0_Yh!8o z0iqfciP^58;CLS?KS#>_B&9DJ^eSosM^Y0mIrXKXQ8^R^u0;;>bxOV$ix9mDc&L@r zZP$aZpi+Ol%AG|~=pB%Eh)Tu?2NK1C_$CBD;$<$?^Q?YG%C(7o36s=?F9_@$W(daB z{jZWHDlDuY0{9NezAQl<%=m+oOkusDm8Y&xdd4a+)>{&CHWv&kB}dzB2_S2pnx%*r zz+@i7CEE{-htpX40{3S#Bp}%+;UR2PiSlgJ2V+hmp(#HI8Z(_1nxuX=xiyOmM(hM& zsE0YphmYb&Qd7egL6lM#(Z^}&!`QV%9|3x5ryi20%%B!5XeLSi1)z2W@QXxA8<#9C zCtH~k2+FCu_hp{!ktiJjI~&4Ofi<*{UFl<&@nME)l%q%Cgwn>bR&RLs)VzJ%-DMtj zYXFo=`lqp^cU1HA)(dyur0xKYe_44Lb(jS{tRj zv)X92vQAgB7nK!AXNx9&B1&unC*~B*k^U);>`WfEq9RF)izTk*S~#Z|N;*sdYH28b zyf~k+CV9e0uPojoh}EmJ=xt{&)H>6)Ju6Q~*|RuS>5}gCq6{bGpzk_y4=&1t?dcTg zr%QkjnPA>#=2~{|V5yA5?={X!^!P`w6k&UoFpLU zVGpp!0Fkc8tp66fs(`_l2CM4VGtI0!1Q~g^e4rp*b$b;QK}%mG@snWdRg$@SE)O9V zJba;0vQQtUrjpd^o%8KW1&cEb?7ssD@sLLn8>l{GUIC!mbf=B-s7MqVI5xeJ_`tn;{vr>f6vn={IT0ye5$)-Aj|jsDCOI==%)t zksUr_|2n|*VZgTmLai`-dW?g=QrAhK-q}*J(r9%u&Tn%4HrB-knix7X<3CL%O~O}z zyO{a1li_tkrqFiI_UCI4l*i>2I}*LGeOXV1OIpyn&J2zl#U8!Ck1=I&+$JioxH11C zx(f88)Rp?xN+Rz0=5qjtdjMRU9lZZIqL?jVJfo4Dm5zo%HEL%|tT*Pk50<|Jj0($= zvYhZ5)8wR1CpAgdn&gV3u)f=G4%5#1-8z6VnTCGM;Ez$^BGl-7aTn;v08;C$_2Wy*u+A0mb!>LNn~nQbuA zwry6^x3Ja>?HxwXyGnXyfjp9clMTmo&oCx7s;$BDz^)yiC_&?+0P(1T<-6o~8E9w> zQo9K6K*zi~sCLkI2g6)>FEr|>_(wqDKL z!el6qD0(OBAi?(>g#z~m27l5BzyY24NITTjXc^ABgv8HnijK; zMrHl5uK8{D{g7j(r^}GP3|>vo9|HOcP>nw35_^oauL6CB=xabPF^<0y)Y1OGOvORt zV5;ADcXo%L8PxF8SpD4F6Y>$~oC(sL)1o^t?iT>Oi;RZvKQGBXf;_+05X_h>;oDHc zov&vrtuXUY-@Xty`koTL0p^~3vB}SB(GX&7;IzXvA7zh zS^+$5gUNSgZO0}{*hd15(H&q+JmlzzxHH>-lIr?1~kaND(V)#_AW_XDk>5M0Ji$vhXG4K!u<3f{edQu!Uw*rS!C)0BCqz8QZ%kzd0BDw)BA zNPfpGi2Qe&Rbw>j=Rj*_;^=Cv;LCyEQ0}+;$k5=CkBa>_#Bjd19|6@`6Gue7EbWvu z0k#bs>Leg;=Hijocz7J`hmfyQ`XMFupOe^T(vS!Hp#W9mZ=8lNExOjM?_c8{yWeB; a9$WO-6%H=^?+r+21L+;lmmkCbl>86A(3N}u delta 266 zcmdmD^k06%b~XVf1_lNuMh2!(1|X4?Uov?Y+j1G7#H8X9pac*wf`}jxVZ{t0y(ibQ zJ1~Y!-p8)Q=rj2tyDMY(WOWWXW}kp~AWvj+3`aF%@Z=jD+B`8J<=yNcGIlaQr#Db} zG^ZwG*yL8uM8>Ge&pBm*BCK3t903eqMX8gMxl(w+Rxz-1gS16WzQVOyJR8Kk4px#2 zV%`8V^EOZ8zQPDJA)8l&F>3P^-WEnSu(LtV5ayWzQdt5u#g;#bEeptJWSo3gLXA6s Q(Z3)OB+n2$Swd0<0O@r&v;Y7A