From 2d5800ace4724fe2e4d2a12032bf17ba715ff188 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 2 Jan 2014 18:24:32 -0800 Subject: [PATCH] feat(builtin/Nat): leq axiom, and some theorems Signed-off-by: Leonardo de Moura --- src/builtin/Nat.lean | 51 ++++++++++++++++++++++++++++++++++++++ src/builtin/obj/Nat.olean | Bin 15338 -> 20087 bytes 2 files changed, 51 insertions(+) diff --git a/src/builtin/Nat.lean b/src/builtin/Nat.lean index acd4c8ebf..de983fb55 100644 --- a/src/builtin/Nat.lean +++ b/src/builtin/Nat.lean @@ -1,4 +1,5 @@ Import kernel. +Import macros. Variable Nat : Type. Alias ℕ : Nat. @@ -34,6 +35,7 @@ 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 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. @@ -154,6 +156,55 @@ Theorem MulAssoc (a b c : Nat) : a * (b * c) = a * b * c ... = (n + 1) * b * c : { Symm (SuccMul n b) }) a. +Theorem PlusInj' (a b c : Nat) : a + b = a + c ⇒ b = c +:= Induction (assume H : 0 + b = 0 + c, + calc b = 0 + b : Symm (ZeroPlus b) + ... = 0 + c : H + ... = c : ZeroPlus c) + (λ (n : Nat) (iH : n + b = n + c ⇒ b = c), + assume H : n + 1 + b = n + 1 + c, + let L1 : n + b + 1 = n + c + 1 + := (calc n + b + 1 = n + (b + 1) : Symm (PlusAssoc n b 1) + ... = n + (1 + b) : { PlusComm b 1 } + ... = n + 1 + b : PlusAssoc n 1 b + ... = n + 1 + c : H + ... = n + (1 + c) : Symm (PlusAssoc n 1 c) + ... = n + (c + 1) : { PlusComm 1 c } + ... = n + c + 1 : PlusAssoc n c 1), + L2 : n + b = n + c := SuccInj L1 + in MP iH L2) + a. + +Theorem PlusInj {a b c : Nat} (H : a + b = a + c) : b = c +:= MP (PlusInj' a b c) H. + +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). + +Theorem LeElim {a b : Nat} (H : a ≤ b) : ∃ x, a + x = b +:= EqMP (LeDef a b) H. + +Theorem LeRefl (a : Nat) : a ≤ a := LeIntro (PlusZero a). + +Theorem LeZero (a : Nat) : 0 ≤ a := LeIntro (ZeroPlus a). + +Theorem LeTrans {a b c : Nat} (H1 : a ≤ b) (H2 : b ≤ c) : a ≤ c +:= ExistsElim (LeElim H1) + (λ (w1 : Nat) (Hw1 : a + w1 = b), + ExistsElim (LeElim H2) + (λ (w2 : Nat) (Hw2 : b + w2 = c), + LeIntro (calc a + (w1 + w2) = a + w1 + w2 : PlusAssoc a w1 w2 + ... = b + w2 : { Hw1 } + ... = c : Hw2))). + +Theorem LeInj {a b : Nat} (H : a ≤ b) (c : Nat) : a + c ≤ b + c +:= ExistsElim (LeElim H) + (λ (w : Nat) (Hw : a + w = b), + LeIntro (calc a + c + w = a + (c + w) : Symm (PlusAssoc a c w) + ... = a + (w + c) : { PlusComm c w } + ... = a + w + c : PlusAssoc a w c + ... = b + c : { Hw })). + SetOpaque ge true. SetOpaque lt true. SetOpaque gt true. diff --git a/src/builtin/obj/Nat.olean b/src/builtin/obj/Nat.olean index 78e095058851836d9dce7618c73e6b94f001e9bc..677e5c5a99e974afd22d3220c049561ebf7a8c5c 100644 GIT binary patch literal 20087 zcmbVUTaa8u89wLCnVp$^P{Dg4DlQv>B$!PUEDKPOOHzhQL4swpgiSJ$h0QMPC4i_< z1)@GF0t!^XpoxfRNvU{!u%d`5i)Zgvs!$QURD4h$6ifU2{_gYt=XB4^u3OOQ)BRt* z|I&Z=IWuSGXZzE0duC?)ng7eT?7e<|VJW+=zcAOI&90nY$cjs*m$FWt6+7pbvU6u= zrWdo~nLF;y3Sl{Kd1iKLX6}mqQr4Ptlp8WX!pp0sckj+FnO~Y-nwg&iLtdOl&U10m zs*&zpo^6o6k)#)bw5*Xjz;&T#ot@>5Y9mP7^{Hn*anQ`2-`|s!H0cBVY^<0LW{ed( z!Rv;K^XBJgofKU4IK=KayCRavbNV z`^D%U$L>qmohXVq7mbW?UII8dG1cLmW%Ru$Q+*#u>U#|&cc|oL=)Q*Cm$N&8_GM~( zO4~U`+e?kMncdbp2wFqQuVOcXT@)Y6+ol^5c6 z+E}qUn=Fd{4Ovz&zT%t~ox{wWG9!|!Q`scsu0wMg2n$lXHGq-q1dimD`pagQ7kBg* z=B<7eu%7OrzOWK#T#X$TSoQ$_yri7GDKeO#;}QvPU#05e<=Ig{OM)ZghJe@d4?_Cx zCQ=F-j#NmfkPfc&Z0#c}6U(rFa#76e+2b>u3r;L`4#x+XA& zf)SOqT4~)fw|jXP3({C|nbjWFzRRVZ*@Sh_STVENQO*UW$Tkv)e0EzVDn1~_G9jVN zkY7^{cb;#%#%DJoc1i!zxjyoE4vCDv^)^IPF1NQW%ui0*jnR9Rw^uA)Gk@dy{!P~}^cNRV+VhCT;;u4`ili<%ZIwIQ zaPJ@qs&*}`pPqBE$DdztUQg_N8IjglpR*rU5`}3BM@1UC zU*)Dm_f4!;CWl>WKK<;2Z<_hP{L z%>AE(FV6!SUX09c)lztCfWVt#COPUUhPbljNt83VLPl&0ku5ZVq{gcf5)~~50x@r} z(ha|-wyHpW>dAEUgo#^#Pf`;+E10mse>|z8DUM?P)p2y2#3kr9f`hR;L*{XfzkDsP ztC;6!a%LDVDzEtwBMA?#02??7YmH)Iyxe7$zo~)k)Rk0YwNC;ML06hV?b47Pvi!F| zVOX|JdoXo@@F{o84dx4&dRGWC`8bRo_hQ|`G*jqCC|h1MyP?UMut zh5T%c<_AX>id8~Qq?~|IL+Qe>;-X2jXj{e^0Q;>bajlAg!tH7>Yl5DV*=W_kAem}H z8niaR!9yfh#gobgUHSKTt&8=?AkRz~Li#8lDY$cach#rzqmXb^Y`IXP?gsLsRT^Y+?mQHVllLakGgI185g6lR*aT`dh+L4e`+!lGGN#%ng!)DTkdyq$zocUS;)A@9y&PaLY zwR+^D)g2@%zZ7?gU=>hjAbHpU5)}fK( zLrL$+CLV6`=)@h4qL?a0xl$Vj`#9gs<`R^@

_p8IY(X`y$j$2@&q8T;l$f|oA925f!5nboqnw|34V&}-h)BYv2TcYZJaD_>w z&&cLf(||$sQRS47b2sGJqYeh|QzEmFN&iVsRRy&50QlXrWwe(^3ur({n#K)DQAr8G z!`9d-qjUtC)&P?u=@h}W&87tJ$5a?hX?=v(YUjsSuq#K3n&yiRwnNMqTKPnzf{px> zUJx+p@3kly0Q4X!7|bX->S59ANXs4vhkBeE#Mg>fJuV)Od?pM80!Yhb)i~TL>*it> zY*3ZG2rpTTeX8AhPez-x5Q&q1dCKZ-6X=SX+T3N;|yjXl!b?&#InP}#dl%T^n%I|>I@qP%vhs2A>{JCCq%Cn%uFkN<; z65abLhfU?M@;>{~5Xrs(3dk(KsOa2fR?25+)dDLY0i_)3ssp_XCq4%?&xE6hkjt1R z;kyZ}l}L_{GbIc+CoRli@VuNP8Ps`BSl z#4-Y=Qf}8YqCc-i6eJAh??C$p1?euc@;P2>M4ttD9MJ)f`P7y10#8Yb9`lP*`ltr0MBl`I{NJRhLqBXX~$ z3o|>HmumIMKVN9i`ltNu*<^(>$92XcI(E}mc@Czs` z-{b{7D%eWMyPbhDSsB@&vLnshQOBvgZj4p=d_Ee*^dIp^4|0Pgy=Q8m15Cec8|vyFs}MViGJ73qd~ z5ctAKfu_I;e)XD8iNBn{vCirRrmU6lLE!Nt1x6+h7kJ`GfofM%v?;raaP1I*BFZ?9 z+10#;ottX=MU#Rm4m&!#4G#O5Ylsc3{I$xY4l@Q)f;fP-Hm}VpHd9r-7&{B54ty*m z$*GEY%`_6nHVyVb8VpfGtk?!#@{e(9s42z; zlC+~tQ57aM8gh}RsoaTD`ELOA*IE%H%o?Ey(tu6VdsghG#b^k`?#JFfMGdOXi_sd> zWkF!(74?9uoNrW^P(V7T3*5TY7Q)myeL$Fu`885qX~@FB*wm6{hyH zHSYt@CNvwGVd|U??jmt-ve7;)@i!-(?f&MZvwhOB)gFi$Xb{N=2r3g7hSTJkP|;H# zbWEM??B1f?53$Qw*vC}=moly)zjaao3q=}|(Fg?BibCb0EXhks5!oQUA;~I4P1vCK z54GpKuNV$>pk(hN#fwhPHIq{@cubJ|X^;-Q9jJ7e@W`@Jl+8$q@G8p`J2g?~U}XND z6jYCmM8?W(?qV%6je<~77zY*E4U*{YH3Im+{dFFza@;)&9P}N#&Ql@5pNbM3l1#)+ zf;V>xlhq%A>Zh31*z$e%Hg;u+)*cg^hfK!zOi}L)HNKe+c750zXXb`Q>nGK19={nE z@j?n<`PxmgQBkWq0@l&nuebzGi20{U7m$sF zkGkhTePcM8_yLYmisK@YO_rauQDZk=mP<@q}x@e_H zxOeW{lipp|OfR?>gB6m$j}H$e$t6-u{mm#xs&L!A83+YGsMe%dB@4GEhr$dQ*nSiV z$I-F-l!=@3Gc+K1lItw)4GZ#R>UaQKM++EoD5&}sXV?SA;9TlM;q*} zU`!dL!EyHtyUhZ5`iL<08c*W_hcUpq5gf-ED~ygbM+u5oq&bXzMh7`g7|8+V;B)AB zy-CyHU8BH~3sQrZlMr%hxCbPs4in8`M`0xg?IH;5XON=}y4r4oVG}SA^d?k4^G#}b zRW5szQWxbbEG0P3sDZN{gZ#w4BY7-(47o?5`mu<6c*mo+t)@bUBl}}8SfM0A({AW0MbZi4bE;<((Sg}Hwz&ARL|w)t zx4$tJ&+B$oE2N(Ab3ndGE|!8Z+TRk}TknA1-q1zI2O&F95VbPu9ABunm-@spRzm=PJ*0=Vz%q`V_5y3xv=!JVTbcXqj3dMOE9(nrt86c3`vCnGvKJDJ0^wUp3 za0JayUD{l50}_W`!?#1S>*)6l?D|jKU?Y=8j3=$ZVv8Dnm!fwR&2MCFoMs%B_!5cg zT|fBk`i6dh=5HK`Z-LZ%0Ut}&-p1>e0gj*$u1WM|9K>Lm2XC#pvkTl>vl-4MyFkp8_BdgP1X^B*%H zLgB|1FnoGAw(-KqmY+T_u>DFK-{dP4I-C6sE7Mn;;RZLR{YxSyzO1(|LFFbQd{nz% z*6w3s4+h?h<}IZCijJO%(YKxw5}2vxhFsE;^7HIYqFu)>IT=dK_x_8($vuw2CY9+S z#(-$0inWUy-S1&QjN4p_&F&&Cn8`rFr;z%qV#vk&;rO@MHdFyR(}) zia895O(|aa#UPxt#y5FfO2)4qOM>YjO_x2XI%$pH3f#=sYO{I7jWkME`p19952Y#> z7KP6a>TaGZWJ%C|(aQ||1`IjG?l-mjgh;>um+m7Z!1pS~A6->am5xP{N)CV{LD}3_ zthr0IU>s6EooHrD3yG#tVBVUOfkcVfV-iQ`n_Q$yPI1$Sq#A*6*{_T|?FuXA?JtH5 zrkCP|`9F$v(T^1v=L&HWGIC`6Z#MbGH5{&zKb*s=H1)?lQ2mF4Oo`}@qq(4sZ=?R=RH1anDN3mHQzxbLD)d80kI$ literal 15338 zcmb_jTZ~;*8Qy!JedY`XkcLW|2ntN60qcYghKmu1y#OspOK4SSNnqMJrBkQp)VXjm z1`(PdQDP$Dq7U-Y#>-+w-_W$p-_Bm$;owRG# z8|O)pL@YGvCAJeKWJO*{=T5%+g%HhY5MHi8HsL z(W;3aU7n9bKSR-5AX?T$9pO6Y4L4@Fle!wB?fTH$Pn|Gh+q;Ldk|sUS&BltEV8&Q+ z0CQbev9;fycPMC`!!A}o#_9%?ZKxtZI`Sqhtc0&iqmnlQkTp z?vJCohSdvLohXW)i$+E|7l2MqPIWpr7=7nws_%hDeHR0{LnUiby_nTcusVTqts38? z?Ixq`LZfYN)>;RkjYMA0YC^jxzL~jy9XEO%J+&^|@^Dr{xU*;Z;K7}}BNi{jZPQq> zBbzLW?$@)dV0^_nEjovpIc<6*SEsW{;C>dxCI}Xkc547V*(cePSL*MaUtZkTUFci= z3NS_YP+wRHG_E!s7TD>5{?+Sybx8@HY-G`4YbQc$~$>zxv%e#s-6$FwwY{R{S5LE3Iuzseu2sVzT_}lAAoi9B#AwcDv5OTWKLv|A(FFE8??pZ#t=ypB) zydY?({*c2g+Gu|s#S7zBDSA#og1A4CA+-7P^9@CDSND($Bz~q){FH+%s^DTp#K8^g z_m#wDsw0?5G|LJdwe?H-TcH0HR=2WRzRE zHFl;>3Y;`@)8LY?-@v#{n7GwMP4Fx*U|N{Z^!1y+(MB~GA5Wtj5v2qfI8=6+=p^puPytA@xZ z%>9i~Z4Fu*5axA`i}fY71iJE{v8{{sR}jxk7#a>9NbuxJHbxRVjq%fB%NHf;t|LE9 zSzPQlU9R)D#)^YL$=_;B<3f$F8LhqYR6vDv%N@jGb(dCmvpPJ_%{D8bqC{2E zKp8RtmvNuwDs0)(SEOhm?aJU_$oCk;WCoFB+*y!@Q?b;Q-Yht`46D(yL>#9L!1_Bxghf&jb)QUS*MEe0tL( zK=|5Wlhw;qB-+g6?X}gSsthf;kLi$E{~~3{QXdK#N^?PR%v$0ufkUXcO~+j`E4Hz% z8FD+Y2k#O(TVerWZWx0iL8?xu=tH#HI~s6`zDax;kEOg{lR+EqK^{>o=4%N~pCdaR zk?omn^~klWyGT@iDIODGg@?A{3F`b`w&CK%nk#`vUH~HJS12692^j6w4ZMlD!m?LOb93$ zo(JmMQxI75M-#<>N0)nX$h;p+tLh`p9Lhbhh5|v_qff&3|{8hQTW>)-} zZOzU%At{fX-f>mz@r)eB-rpgM_mU8*ny@7kSh`tq50PVzL*#!Cl)uO7K2{sjMIMk# z)j-4EZ^Y-?ghj1R5=;dM6nzK`J=-I97@_U^{VxLzRTubf)Gw5yaHF{$1a0Y>6>QMG z3&q|r*VS8>rs55RFzrT&Unz4hLr3e%QMX^~Op>4Gy7#2jAL34W+Sn}P>dyL|7t+CG zkujwlBsw(+4wy7ZJOwcH;DIehr@e~`Ahn_3As9HIecMPJgP<%DoO?eSPVIsMKHZTx zCMkr48s{SmoZd(rV;2#OaR%q1Avh+fLPiWhdMxaDsUpszB6GE|=&)$oU=t!XV9@@k z`bywD4jg;cLFbbyWEL{zALUTBfwrE)eD`h{<(HBLG$16gaYIs6QbPE!Gmr@1cRAG zM?EZhA^IUZ2PB!{Aih?<>T&UK;xi47QsR{Zymb)EyQIJZO{`jkJnP4Slf(bFYEUeM9*t5dxa>7rs6= z7?OLj``y|ZnR0I}U4ili6xWCSt#ar!H9=vU(1&z5kVGWy88#KFzsxD9-P7P^gBl5A zntuM}J~E4Lf0GzbZvOu2z{zy^eNL)e5M$k^UzjAHbR_d3xX6htRNnP z_4j^Dnu%sUNeMcPqx=bI9q+q9d`P^=%-`!pXI|xXDW^;cFMNkMEGmbUPuh=$DE0$L z0JD5n*|}y`%4cZR0xO?`q+IH%3%v^`J_j}Lgp-JHmN8AjHwz8FTuDSZAJQ+ew&IBT zk20&kt}3Dl=_I1+tPrb)hytc@*bd05zFT%*526u$m5R8HU{WcMYZ}p4YY~MAgZU@O zzNREyGb>+bTO)b~;%P(&yyh>@HpW(-zm%oeL4tEodY08AtTx2kKZ=n!=|o7$YkqMB z{ZxHgEpvPyQ1bBH!$!JGmQF_A4^Z(b5#Qr_v-bHTA9XkfgM6|fp!-Dp@7& z0Nw&jmi<0CUN#%F)CRjad|d)3;C49ak=oV{W#m2f=|~r07yLVilVmapBtgy z-a2YqF5tceLtuwj?IVbe;~b))5i9>~o^4J_zOc|f=_++rCswolI}(t)hwS&pyR7Pv0)DW1z$PpSpYz(74STZ}W9#BJ$tmEut7d5IG%jGCfZ@6! zfHF0n6}N$MdF{N2C8)x_3*w51rKHVLIVbKIc21geg$Od4&Wqb-6`P@I7aQYOPzSyi zG8v^*O{8LjJ&{qi!7al?6KBBn-2om+fXGi4ElDe1;{iI02cgVYkF1OL^)Vd9V~5g5 z)MoFHYqMiwA4(=*!uKPW6+?|xv;5wqvzv_-MUfOy8eMR%WcjUP%Sj>FWs z1hb2VXOpY#%M$-^(%J4GPCDBs-L%>ZG4(9DGkX4{5GPTQa@7?qH&%Qhy0e{5Th{7> ztTGn%IpQNJ;~Mhc5E(_uXas|MM4`@-^%%8bT<8AAsj@K&O63U3`y{~i-HGhg8 zr8?1xZhetvAC4_2F!?qS2Bjf!P?)TfC8sRSj$nqWEbCO;;M_=*(42(HZTmqb4-j-$>h$KAWYLEo|Kyc`nz8tts$EjS8myiz=-CcUSS) zN+VYv3i?12mHzWzpdlK&eNKs-c&thy3M5kI2no->m?3iYppBnrahuRhN(+EP8ecmM zh3pi{(o-5h*-$%e;u$9NI%I-sagBhg7`A^HtHjfaVA@n+7MdBV@@RYt8VA1@RA4R| zLK^D!;3m9C!992DRNPU=@0P2|q9J4;DG~e3?1hSZL~vP>2@K$+Wc*0tGoMRJg&9t! z#v811m5E06&f0jDjpNng_