From d7efdff83d658b687b63de04b9c24537b7e45f43 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 2 Jan 2014 22:48:10 -0800 Subject: [PATCH] feat(builtin/Nat): add more leq theorems Signed-off-by: Leonardo de Moura --- src/builtin/Nat.lean | 50 +++++++++++++++++++++++++++++++++++++- src/builtin/obj/Nat.olean | Bin 12937 -> 15930 bytes 2 files changed, 49 insertions(+), 1 deletion(-) diff --git a/src/builtin/Nat.lean b/src/builtin/Nat.lean index de983fb55..50c0867b9 100644 --- a/src/builtin/Nat.lean +++ b/src/builtin/Nat.lean @@ -30,16 +30,39 @@ Infix 50 > : gt. Definition id (a : Nat) := a. Notation 55 | _ | : id. +Axiom SuccNeZero (a : Nat) : a + 1 ≠ 0. Axiom SuccInj {a b : Nat} (H : a + 1 = b + 1) : a = b Axiom PlusZero (a : Nat) : a + 0 = a. Axiom PlusSucc (a b : Nat) : a + (b + 1) = (a + b) + 1. Axiom MulZero (a : Nat) : a * 0 = 0. Axiom MulSucc (a b : Nat) : a * (b + 1) = a * b + a. -Axiom LeDef (a b : Nat) : a ≤ b ⇔ ∃ c : Nat, a + c = b. +Axiom LeDef (a b : Nat) : a ≤ b ⇔ ∃ c, a + c = b. Axiom Induction {P : Nat → Bool} (Hb : P 0) (iH : Π (n : Nat) (H : P n), P (n + 1)) (a : Nat) : P a. Theorem ZeroNeOne : 0 ≠ 1 := Trivial. +Theorem NeZeroPred' (a : Nat) : a ≠ 0 ⇒ ∃ b, b + 1 = a +:= Induction (show 0 ≠ 0 ⇒ ∃ b, b + 1 = 0, + assume H : 0 ≠ 0, FalseElim (∃ b, b + 1 = 0) H) + (λ (n : Nat) (iH : n ≠ 0 ⇒ ∃ b, b + 1 = n), + assume H : n + 1 ≠ 0, + DisjCases (EM (n = 0)) + (λ Heq0 : n = 0, ExistsIntro 0 (calc 0 + 1 = n + 1 : { Symm Heq0 })) + (λ Hne0 : n ≠ 0, + ExistsElim (MP iH Hne0) + (λ (w : Nat) (Hw : w + 1 = n), + ExistsIntro (w + 1) (calc w + 1 + 1 = n + 1 : { Hw })))) + a. + +Theorem NeZeroPred {a : Nat} (H : a ≠ 0) : ∃ b, b + 1 = a +:= MP (NeZeroPred' a) H. + +Theorem Destruct {B : Bool} {a : Nat} (H1: a = 0 → B) (H2 : Π n, a = n + 1 → B) : B +:= DisjCases (EM (a = 0)) + (λ Heq0 : a = 0, H1 Heq0) + (λ Hne0 : a ≠ 0, ExistsElim (NeZeroPred Hne0) + (λ (w : Nat) (Hw : w + 1 = a), H2 w (Symm Hw))). + Theorem ZeroPlus (a : Nat) : 0 + a = a := Induction (show 0 + 0 = 0, Trivial) (λ (n : Nat) (iH : 0 + n = n), @@ -178,6 +201,16 @@ Theorem PlusInj' (a b c : Nat) : a + b = a + c ⇒ b = c Theorem PlusInj {a b c : Nat} (H : a + b = a + c) : b = c := MP (PlusInj' a b c) H. +Theorem PlusEq0 {a b : Nat} (H : a + b = 0) : a = 0 +:= Destruct (λ H1 : a = 0, H1) + (λ (n : Nat) (H1 : a = n + 1), + AbsurdElim (a = 0) + H (calc a + b = n + 1 + b : { H1 } + ... = n + (1 + b) : Symm (PlusAssoc n 1 b) + ... = n + (b + 1) : { PlusComm 1 b } + ... = n + b + 1 : PlusAssoc n b 1 + ... ≠ 0 : SuccNeZero (n + b))) + Theorem LeIntro {a b c : Nat} (H : a + c = b) : a ≤ b := EqMP (Symm (LeDef a b)) (show (∃ x, a + x = b), ExistsIntro c H). @@ -205,6 +238,21 @@ Theorem LeInj {a b : Nat} (H : a ≤ b) (c : Nat) : a + c ≤ b + c ... = a + w + c : PlusAssoc a w c ... = b + c : { Hw })). +Theorem LeAntiSymm {a b : Nat} (H1 : a ≤ b) (H2 : b ≤ a) : a = b +:= ExistsElim (LeElim H1) + (λ (w1 : Nat) (Hw1 : a + w1 = b), + ExistsElim (LeElim H2) + (λ (w2 : Nat) (Hw2 : b + w2 = a), + let L1 : w1 + w2 = 0 + := PlusInj (calc a + (w1 + w2) = a + w1 + w2 : { PlusAssoc a w1 w2 } + ... = b + w2 : { Hw1 } + ... = a : Hw2 + ... = a + 0 : Symm (PlusZero a)), + L2 : w1 = 0 := PlusEq0 L1 + in calc a = a + 0 : Symm (PlusZero a) + ... = a + w1 : { Symm L2 } + ... = b : Hw1)). + SetOpaque ge true. SetOpaque lt true. SetOpaque gt true. diff --git a/src/builtin/obj/Nat.olean b/src/builtin/obj/Nat.olean index 6e917a20a95d88cc1500a1559e182d31ea49c997..50bf3901e9720003055162abec77d415b178f709 100644 GIT binary patch literal 15930 zcmb7LX^>q-6~5i~y-8+%pj8S%kz~j)31ERCl!Z$OFUVxk5P_t`04AA9UWOMYGh`ML zEiIQ41vP3!t3(u)04}9~dzD+^8WRP64l}0K3Wq;pyUw7ZW_YH9>>FMQc zefpf!r~CFyO|(ZRcXuY*S@B~w?7eAfdN#YUJw4f;$X+ozo!L#Jv)KZZ*|DkFY|TVx zbSAUM-~7JJ3gxo7&ctkIa&vn&%O@S=imd2ibNlG7UD>9o+0og~)Fcp$eJ(NApplnA z_s&fupyv^EEkGM3P$zJi=&DOHS>xvFRH5}s?Uh1c6J4w0awa7omCVi z;jDda=Kd{k{TEZdMcJAISp#qjHqY(cxv70^dwMDm9Cj0K@58VoO!;zD`)O7eqMF$f zfen*;0=8emKD$11q-rQpe~Uq9$uP>LC=8a9;te?4M^6S2YmDc0<;2`fA}YXy9tnz0 zQtB_EVy-oEMj`|n6mf~#NiVH&v8Q~++{FAcH6RX=C{s|K!#qimNTMQA=q2?5FVe;~ z?62xnXItCZy&K|W*{QD4KG2z&ol)B~?M~KAtv=Y9u-P!VYi=jwNuRxvxC`8xk7Yxs zYr=iDv)&29hy(9luR&28!iv+hhPz5=xSt%YF&T`&d9g*&7CypcrVP z6yP!naZ%Q^2hb_OuIaZkH%#r{-ac^Cbm34}CmdxNC(F?~x4OJDv-5`0X%{^Ca~;ZU zO{ZY|T<0dYc64H2nb=E+&}KOUBDqyrKiOW9nxb^HygQY!p3Yy#M4BK=Jr~;KT%<~j9B{0!a6U@d z;4)&Lz`hj-1ava(N5gF|cD-tES%x;%adNus13Wb{bPlSoM!~t${hLj+TPR{Zj-#W{ zBdV`M5$#1Z8jj1PYg|2eI>HWqHb)bkS9`-0>XpFJB)1ZsQ@<@yA)_)^@V+7bS_Rl5 zMd*gGYg|th!Y*&m%uc(|=|sGY(0xAsIax2Hgv>YMRCFR+$I1t%9N#nhG36T$QGc?LX;Fin~9lf zB>On4<-Idf3`UQmc(isFR7q(9Ve+zm;Bv7RYa|(`46%j)|IZYZY=SBMo8vzQs74Y) z`VU6_6>BCXcrze4&00hHFNXUQs{caglf9^hdCdVX(5_|h@2WonODvMbdXghy%0aJ* zsl&`)GUYbnDC~{_Ig9-s?F)jmq#>u9CMYLJAFqZITG;9Yc{s8RP>^wy#x0(fWOa$5O4CnVG6Pxb@kc;8t3+Fi~o!Sihu~ zjQS}$vl>M$X6&jeNuj{;1`!1?Sc6&V=^7rrrJ^)|S;%++3lFaq?}y&a862YWLvlnB zA4#=~YZdcMQVH4xX>;a$reR(HkQYYl8w4q05@euN4ErH2dlt26YKak>wSo^=gCIra z!=X)LRTX$7JIR)E|VNkSnhG&7cJ%EU4HG-t`Fg{{oo z0mjMzr4=xEzouR(11*vvRS^W%osn1-D(Lu-D>CeZ3SA#L8F(}3;qRUgUa~q^aS8G< zO5RhC3h;YDAG$Lis|O-w&YT)1Wx{_PBZg;tjSxQsy-#5HUPh0WtJXMI$QEz*@+(}a z9sKN*AkaTdA0(FK<_ajw4Seqdufsj~Dq2J_gVB}_!XgCUB-b||qXSift+>%A{aMr; zh6wk8p!qxsu6$UNBm*{s4kkO%OJX->zJy{cz|wS|LsFWCg3|6${M!dK-7si(4XXO6 z8!#V!O2!BR)$0}D-kr=*E|D0*U4Xo!7Z<={&F*mv)s3{h|nAycVu1BAJcr{@GYKZt^c`7J4jK!*TqhvJ0+)Gx%(Rb{!l z1`h%BE{>FEYO#X$Y+zc77i0`e=DxPfPIt!UW+UVG31H82C}&3liO->-7o5zkoW$*r zOiAH;L-l>EQr_x0lyqPh(K*!OFliS>%Yb?5g9g3m0>IC(6Ptk6eoqANI_;&d$c|xn zrf!6Uj$zd-Z5}kUtI7++^xRA*3q+z>l5?}u4%XrCN$}17AUU%JPX9IK1vPsh55Fr( zzT}FQ3$he2xHhpbMzJcIXV4g?Xhu9sTbzXh08NGT!ZEpkYB*e3cH(&UN)e36LIQ3P zAZ0g4vY=go2WA9+%~Qb_TZzNs5kErRdh)2k;ucIPub&S!%#BvUxdqhi^{AND4p*2F z)W+(8NV(wv7_SK`_?^@W7X(FmZ(w(U=#C~ZTPW%yx!HuFP2>XqU>GUdK8)BlN1z5~ zgOs|sJ)zV-Oz|y=-PVJv;$jpXK`~Rz;uP7Y-k3z8X0E4fL6)(y@!M?<$c_ftq6J7~ zdlewB?Ijxqi}N_D+zup#l;c%onT~RQO0F~Pb^w|0179YPNWjlIuRJ*kc$XtFYV~k^ zdCG;QCk!Ev)z`h2tCo$RSPp=2N|71ND0oNjv*z9N z%t`=<+YcrO*~Od|_Vr?;`#`AP$tsoMvj_Wt)DHMtU11lYcrXP*C%(DbFVu}Fy6fD; zjHi%IC(rjdydqV=nq)~5&E2%vpj#N{mm|Bw%Oyj&D$({TD)x&&pj#xDhnz>DjTV5q zp$OFvxx$JdmQx2!X)-M57ZL^o{+7xm=>PX^dBgG1;)i_GJ|CSr13{!>#b{j0Qa;RH z+SNR%iG4nG0~SJL2_fK+GOSHYOmzv>UnnKJ?Zn zAS7xRk%`wQ69zjt-#wN630V9zvM?`aHWaGb<9u5;a7qmtAV4Ea^MT`p58HrV!~oR( z9!2~?5$zP7JE1@c|3}aZsjU5dSuyr84F7@7*m6~GeqQY21|1TI8+7|;iHS~FbIA&l96}U)8jo z6Vr<8K`&qqtq&^N=n5g2gxNO^fOb`Hal^c9M{pV@qMQ!SH+k|NfkDDti*aTWnmEW6k0(O- zBYMpjD!|H-xKMPga51MWHra1-9*&vEDIP3N1fV)8Me;E%U*fpsgLUA^&1Fs+lTC=% zLJ@6>S_F7uelFM02c4XkR+3C>ny`}LI7?euvb10c1UQtm=M=C=F~?yzZ@HrQQm6-D ziU|Ravp<-$4?&vZjuEwkC=|+2Q*z+wq z-k{^hq62FLP$y6<(~R#%T{b|`6>+++uRi6*auYqjg2W^4xn*5?=-z&Vmh^-gZwV}F z6O{I|s7mn9g(_~>^X+;@dtJ5=1EfR5VHZ0tM3)|?#pin0pYY?#E^+T3*Nn}~P4Cjn z$ubO2d&RCC1m#kSpL@tPvTsv6e$3^V>yUUB4qD}L0sv8@NYbyl?#sCr0_%B5sYRgi(Qhp!NZy>4FE+^A>Xb^2NlO!w9w<@_R?3lQn= zo2be&zZI(AM)g$4n7=)!of8>|=>x3LAYero0QtKyBm~s_gudY#Wdq>DX+NL9jT%+{ zbp#}g0tGZugi}H&$$XrhKD=&B{>mj#rLT+XQQ+`GJ!dr45DCH7l_iC1;f+OT@S;|e zOFrmzsQF>O+hr}Vre#U%xF#vI{)13eK0#Z4n7FJW&C3rj2iPqrv{>I^br>ZANBoGA zae=x4$NWnQ_fUM4;^T&Yzv3$&e6yN={r_OY4UTNIrBYaS&OxmFA@HLt#l-D?nu?o% zdtlCL{wf1;mYIFd4`z1$7ww1E?91Ac+~FONAG!2|Mp0!mQVb>Z`45RWlX zL^VPpKJeyPq5LT4)Bw^j(1{B|vn z*QFK|&<3kgJ>qk%9_Nsd5>&=G;U~)$ojIc%&BNz^nFk*7z@qZxU1k1vbpDzAkZlC< z)9W9h|FsFA7K-kIqYkrV0+oN0(+R8mceIt0f=R}6o%UCnzQj*#>j^;4Rapg9(GN%v ztCQXX=YIhKA5wqn8s(6>W^%T}KR&68RYg|iY|H&=0a;R#py+3@{cG@$as4J#e~YS& z>vyi!7)Xt4AppEd<$tP+GPg%a?riIu3* zczWGwQ@O9zCh{pz$&aEufg(=r{3?X;{Akh{!#niGX?|RJKa`mtEgNhX$b*VLbp`l_ zp7Z(;)Hn^D&u+T1Vv!77^1$T$);JAnQgq||M89l-jc0-A!7Aw>+Yvx0aJxzx-5Srv zFgT@8DjSPjUw#xDD4&GoM|B`WZ$~@PXD}9M7f;F+?*aC3kOJEveKtQ*R%QjrI>5&B zm{l=Z!xqt4;fnm>Aj`vLHDo}_4pr3vWcq{kqBJf7Y^v-PWrhkbq^jMaoA&<7;W`(6 i`AwtxJiB1LokcD8_sCIeywq}k{cA=hcdf6%&3S!>OjwfET_9j*_KY-$YGP5#F&+p=|ZY{J}B9~-F;n=cKH8Mk6^!c4QqZ5W*} zi-#M7H5N75@mS}BlvgNs5JE;80r%>!vi5p`nEPa<5czR6U$rOkEI=?1}IY^U2G zfOD6Pjt+Ynm{u`Zf?WjrF?K)^CEB8*OLH6OnCXduC-(eQtvG{LK+Lq^3H)WIcTAbm zF=a}hb0gm4hDy%>5sj!8l`a&i)Om(cxtm+dg{Tk9R$58DG?My}NNQuF`V73{oR1O2 zP%zH99mfAR&97fX`#x$GZ#NatOY`*ysuoybx3UJKo62Cg zW{OOeEJ1{6-9hqIlf&(8s(@Z?axv#=nnV#LlXR8RyMo~5b>vd{fb=`p*t7}e7&F69 z>f0OR6XPa5UQu5;Qb(qZgj53yW8UrDHDiri8iT$P6qt}b z>XfFtl%%2d4vY&h*mJl%$8@;unDcm7>)W@EndUwtn+_|%TkV)~Mh9Gj zKUbd%iw8%h0@05}x`n(wGEY{S4BepY=_gq);Qah}fvYDsj7t>}bJqgf#Z4^)Xs0(7 zODPmP)91$*>zlk2Nsi%K49tOQa4ZtI=-Bq>swc?!6pg82E|q8r!E-RKZfB_4SXHMm zQr+i*`O6rh(nFQ>QOT9`B2nFa{A(t7O%LU)1IYV=WRtN?K#gLM5-|jjq&??&-`~1r z3l{RFNkCmp>}>>#DKLOFsepi3`ED+4M0ZM$<&g(NCa8o!^P{^do=%DV1ySEfNq1pY zMcq#PbyyTk;-@{p+!p&O7AP>hQ~@2g&>NuCk#_=9O%&XQ#XH(70LfkqDmzbTENY}~ zXC^O-k1hyA1+#Dm=8Wnc#OUs8nA0!GallcyeAI_O6trf?0o=329RMjq&gSPam*emS zg5~3YD74Tvmeg{gs~X>oZ0m^3esV==Nq_LEpa z*BokPg*t=jMk{DQO)*R$nQJJIbG20ML>uh-4F(eRhRYqTmTzyhm<@nP>H_suFlQE$ z)6wiTSS+VFRzE0Pk;tJi4z1dy52COq%q%uk?;;{t6JL^QG}C~})=0IO1tX`LD1hrQ z;0mz9)gmq`vKI^#Ig7@H2*~m0{$*#u%V?nrUT$_}P#D#4lTqh09~!GP>?;685vxEs z2-5XY4%?Spj!LKfv{LTgsF_mjPU*#koM%u@>r(GCL*W$LBbN^I$n+HJcFx-ex=;GS zbS3zi!1Mrb&`8;yc9qF~93*E)d7wt`f`~#hsJI$&7`QdP$}Fp)w1(mpPh-!Mt(V3M zBv2N`C0Wmlb_6iJ1OwtaRG2Y$E zVhC8~2lG0HwDT7fZ4;C_?Lw)4z112nD2>a2svr5H3OQK)likk4;T|D5*ND*^5H#A zeaIUwK3d$ex{q@6momI3@{1(N^ao&jTQ8~un|ks45Wrn(CVDTP-qYv&esI%riV#CK zVNv>r%>+y7IUNLNCCo|Vp5No3gaX@_oGWT|(g<7wHSM21?O71=SQHD)80Y~S!t=zM+QCJ*iLo~)BYG_U0T!S`w;jze6tt!f_+NsOC3ht$*I|we zp53*rBmtsOll0u8=|B^Hb28z#+EFv$jI#YuF?G#J>R0=c!aD$Tcx_^T?`QV8XrJma zCgw49))4`ffT_Yz>O-d$stUAFKzi^_L{b<7Cg4k;hba3>WDDjcdL9U+f9+KCheaV2 z)F4n{{>8RfRB+s zEkvbN7J-zbgX~TD#civGi*+jJ(&4HQEZShBEx#-5QD&ROlIwL%_ zyT#lEb|u}#J`cIeQX-(A1Ln$R7^&{^+*J2e#)xh5A!xp}{J-Cp zSD=F1*M8GJOTCQPBtQw%EedWU$h?Z5jFQ&GKFh5^1zQs%9+nsfl)Q@LE3%VeQCgGu z{gxNv8c^#nob2<1G$7!#FBHApyaAz5yN^nOKiM$Y1MS{ZIpmJp6lGYjGk--@@dT!Z zL0SRKE$U4?$HC9<2uGpk(*!v_~zwhlMy-hBgL56z(ziv`IdI}dr6`*o1Z z+1R1rPJ*Sg0SCJK5@Gv6`^a>RQiA;V629~f-7q+|xn8noE$CK}I=4dVjC+{Q3`r%j zNFATJpk+OvwZ&i=F80#ZD10J=p8iGgY{*7Dh5G^M`miPUP_nT@nlI7@C-@pzdpmOb zAFaCOa|>T+0R4u@P)T$VIn!Uob5aV$u*?7N9#6ay6RFT{&_k&ERcrduKy>gFMC=<5 zwI1$j+G`onGLq4_SDccd6F_arcHz_08>C17mQl2@q0{zM1p3uhh+a*Q%`wj_vN z)6vs%kLy8y5}spMC)I&pheZa^owOqPY0Vwe5VW}W_55^lj^V%39G>UlJP^H%#3K1P zDHlKWQCZPt?j)ID5I@qB{ZkSWAgcfruK}t~xej(Eu3IwPX!bqIl*4Akdu?IN)6gNF zyceLP!F>ucPi8Ro|Dim3U9O#2J~(n;ddP`f5b%)X_Y{c2hQ15BLMrg9wD6)>wb8e7 zc|HIUR=(R~q~r*YLT-FEnfexPdA;}zr%H7YB~l+0sea6O?+A+cK8(EDVwv()Uof?4 z(#{2EcBYTUJb_d-Ef=r<5IFJrj}-i|f)9BxJCk02nBc6b%whOJnDc*+V3ciC2>-jM zfTEL_M(4^|MFjGMuL1Jk3T>m+UZ7hlU^WLoooD#TRf7B_wVh15tJ@c)MgCR)v+tPWY3sT^CUXP>LhyvvqCgq3t zVz>^QWxylzlSg@BUr)EC9gw8uF^G~UV2$!1ER|k|o9aqb$##?6y594cy=7Hl*P@UD zYoJZuWo1m$kXAqQ6u!2u+&U;f1x@qM1<}m^^M+{V|4~9TYiu-j$;iel@Xt^F2Uy@w A@&Et;