From db3bcdba5594aeb5e24a39947d75e51abf321199 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 6 Feb 2014 09:20:52 -0800 Subject: [PATCH] refactor(builtin): move pair definition and theorems to pair.lean Signed-off-by: Leonardo de Moura --- src/builtin/CMakeLists.txt | 3 ++- src/builtin/obj/pair.olean | Bin 0 -> 1141 bytes src/builtin/obj/sum.olean | Bin 10205 -> 9146 bytes src/builtin/pair.lean | 10 ++++++++++ src/builtin/sum.lean | 10 +--------- 5 files changed, 13 insertions(+), 10 deletions(-) create mode 100644 src/builtin/obj/pair.olean create mode 100644 src/builtin/pair.lean diff --git a/src/builtin/CMakeLists.txt b/src/builtin/CMakeLists.txt index 17822f71b1..aaaf08ca92 100644 --- a/src/builtin/CMakeLists.txt +++ b/src/builtin/CMakeLists.txt @@ -95,7 +95,8 @@ add_theory("Real.lean" "${CMAKE_CURRENT_BINARY_DIR}/Int.olean") add_theory("specialfn.lean" "${CMAKE_CURRENT_BINARY_DIR}/Real.olean") add_theory("subtype.lean" "${CMAKE_CURRENT_BINARY_DIR}/kernel.olean") add_theory("optional.lean" "${CMAKE_CURRENT_BINARY_DIR}/subtype.olean") -add_theory("sum.lean" "${CMAKE_CURRENT_BINARY_DIR}/optional.olean") +add_theory("pair.lean" "${CMAKE_CURRENT_BINARY_DIR}/kernel.olean") +add_theory("sum.lean" "${CMAKE_CURRENT_BINARY_DIR}/optional.olean" "${CMAKE_CURRENT_BINARY_DIR}/pair.olean") update_interface("kernel.olean" "kernel" "-n") update_interface("Nat.olean" "library/arith" "-n") diff --git a/src/builtin/obj/pair.olean b/src/builtin/obj/pair.olean new file mode 100644 index 0000000000000000000000000000000000000000..9c4f04f81d5dff17693097edcdf820ad3cc69ad5 GIT binary patch literal 1141 zcmZuxT~7ir5Zv}ai(m2L7k+C1qmQ7Eny85eP4vxYa>OHo2zZ={Ki|&m;eoLad()k^ zJ3B25`*Aerbo;Sn!*oAJ!z7jWI2pu!$!5<{Dz9-z>?rCc;_Qtq7_l!N-ReGPBe5PD zXWPt}lKo~Tz|_to8U!I^R$&22!)%dIBTnN89zI4BEY_IxO=YyYgI=9l$U+KKV7M$3 z2~=R13L}Dp#1haFYFIKM=ALOvEwJ&YWDAhh1(d^c*@dftT1U1p$4sanZA1mICstY^ zT*RJL!eziU!WF=+)4-0u+T(P(a+%V~;CUcLn)$4yN-m+OwXJ?!HLywC>0_S=w{HWv ziIFHY8)WIm zCSaYA${U2#e|`$?I4{oy44E_F2`|+f%*$FcQ{bw|ogwf>FMxiHS@V+_W8&|$HA;rP zf4$LHS)V*Q??W4>2@I*rlmaB#fw!;O_{&^@Ho6>ULl-qaf+(NRP(Tr8*a5|d^k$b7 z;a(2+0oBI?KwW#7!y~{Zw;cmM_!oGMpSSNBb6;)p(pXm2ApeA5P6C?_TW|QSU{uxS V{5F0~-SKP@ug%;IUhnZ&^8-iBNzVWP literal 0 HcmV?d00001 diff --git a/src/builtin/obj/sum.olean b/src/builtin/obj/sum.olean index 0cc215017c2ce3bfb3c7af3c74dd8ad2ff16ce4c..737fd28a9e84e83297b2c54a2a59fc0ce8c9eb5d 100644 GIT binary patch literal 9146 zcma)CZH$~%6~6b*ezZFsX)NL|u_@i|0;OiBF0_Ecu1i@GQfdqW{j-_v&brgi&TMC= zv<(`gKTs0?n1CUnY7`>q9}we5su&_}E&b7!#;t|40g1K*f*(nX+p5v?Jm-Dib7ywf zxJl2Rdp_ONf&1KO^?kq$`fuy7;-({h5H2?)@4?N8MiW&+;zE-DY+m# z4}LBehU@jJbKMw`q-YLfMLU3X^yWgXycei*oiYG^9R?ngg)aV*RXS{$TD_Jyo9~5W z4?wO9&=shA70{6SK=VN{>w9!|x+Gw{-c*|k6r<4}BDy{&QP2=^+_7Fg-~bl7LUYP> zAXKhWt6I1yutEYvnJjEH_+y~u$=Hw!+zt%fDs`NU^*P3;XSP0_ItzL*{|YqoYEaeq zj{sBZH9(yhU#mCADz#>#?wrM{)6i9r<8ZYRxyA;GIhZ|nTD%M0VLNDUAdijms-jjS z7`gRe5)^^u&Dx@PTHZT76Wfu4%o@sU0?K&aEP}HKr>8-XlmNIHU@JgDTxygjC9&{B z{Vn-0IyO61-|u`bOqQy%WmzH@O5?Np8WZViT!VYwVI~e?jv`r17>;Fy4$ylhDznW> zZC4Wm=TsJ0;T||4KWpTl_t<@mK3u6a7VZ8pI7qv3{w^?Hw)iV|>rO-}h_F50Z9h~4!pxi{2-G;Fy2(T=oa3r`mq*JBwYFxgf=r@&`kSk5;OZ+Kh z#YOABpcTr1CPl_Vxsk#|Hv*j^%BVO=xopz0ah*~?&2oavTy2*@x;IA?o_v16_2W$LVf zs0Nngkf!PlLT*V_v9}S&b(oq$86`56L=uAvfJTB5y9HxSzb%HcI;WU4(rS`YrV(FF zLl@}Y%u2B7ih{Nn5}v!Vkl zNgcOjTnR*HIfl`08pe#*Kzxcaq<$KxBorqbkS-(*#9Y=gr!m$B7^Xh86FVj0mNu6q zRh%o9ky+8)Ci1?;{-t+zoHKK+uh3H6bE2OikLU&j2iEeFy=(2U~5MViXhZJ{C)HVP}ZV3?{_ z_A0dwtC7E%d;*(lkn=wUp&_yuZ{rt9WQrb!&@W+ZvDH|FsT0g0Gj)V<z57=CGEIJx=ndkv+{7Ic@T=uT>?-UwZ<~x z65~anQeB>|a7z}Tr)gpmLsaICf+4(O4pRQ|;u$c_Wq^MI{F`&JXjP$4zYege+7I0V zy}A$56j^Au37pH8kMm3MuZWD#K{CozP6v+N$L^9rhnJt0OYU+ldt6PFqjH>i!sZ=) zbv&xtFbWExQ}{M=55x9+J+y1q;BqmhCT#TugW`thOAHfkGAw_Fb^Zs zbV*vHOIV`*3PLYg~137YmHvFTFXv;^9OO?7DHP%660pN_avP&5MnIM`$ z#(re68pwB%2XMC)0`kOO4=ex*uuhgLtn1wJS<8rX!8b?#G`OvDPM* zec9t#i$B>HWcpwu_s(&0^rM9r;paj4vHbJbuyj;_=q}0&f)~63H`8870H?0b$z%nwqJbO0y!lobe zAc_m!$%9|?oxvTa(u*hu|0M{@@idO#PV>uBgHC9E?V$jZs%q%8p#G7(+$ZJzLvK6G z&iK)%%gZYTR0iZ;Nmcg){CXCE-$Bu1pFW)W$H0?!1l8Lywv?t^{OXP5eZ+QUvn(gN z{_B|GQGl-j(B(mSu8}85jGcd+{(sS;P)x(6smdte#B|ZO8!MDH^OHuyCvn#BMR7L8 z_LIFJMwAgZ*kJd9$Mbl39^>n#N5At=#7?nj)hWFXK%Y6fa|6)mZERQ*^7|lS@Nv9_@-;%8st&^AW0g5iZE8jq+^0`fyp=h(%;LR(}=Z#{k&JM+EUdwU^VhmLR}8 zlK%y;g7p97{mUNN=F+{?&or8PCS6NY8@dYwG?U+*tm%0W^<$D8j#>CVO0)Si81w24 zMJrH^CLxO-A0#s4_{pRhw}h2`j;ljaGtOqCwmg<=l8WvqG5-qlXRU5jVqp;d6^VuZ zL~J2A2!KB!z+K8L^d~XK8vX=)Q424n%c&sZ=y^79Obe-~vlS%mq?Y-o0qJ89MoRek z_Pdzw0Fs)2#-X-9OQ%ur{#>>tiJ6eJuMW=(>jL$!f;=tOcFK5#>-8I_e4r`M=k?uC zcZn9THv!%P_@e;5a2M1_d2vrVU{AZ1h>$;TR$eeG$zq(_W1<)EbyNj7YgV76K7-B8 z$oE-;9n(iXXj}kzha1HT*0rd62rShF_CAGh%ZxT9FC9sq0c2M)$EaIDCU8UBjlY;q z;EJ(D_(aoJM|;}vl)cOeQ9(M^2{HVjUm&lz{)z?e3Rw6!^(WZ97@f-)pSS2-0u{HTAri&cSQd!+`N*506NcTgNK9u2>|W6TE#uj{liDC#XBB2g%QYqj18t4C-Nw=P>>_u+S&KzXY_swSku0l3va>McW+v z1#XA(nVj5GM0>OZO6X0ZFSvgrY7KhvSlksLcMjl9%L=XZY*kHm?32IudcZ#cs1P*; z1mqk)81!0FObff37B=`77-$eKbi?ol3pvE zRci96*YFAM&jAVvNS4b=wZ&Alw4{mCKGYnKNPm(`;}nZ(g7XhXg$MS(ETmd!=7~-B zp2Z|9u`r0$+DmLJXj{NpRAQks$%J6H$IvB`T2&4%u&TH_p_7K8s#s;=4#AR!42%he zL&P4C(9PppcBMA4Pu}0^wIy%aJA}$~^p9YcPWfxpKuSvfl+1?lqA-fW7>88CU@v%T zMW~T>n7xTt6MYl17^K(~oiX8D39Rb%^ut1wXo%nW|nR=D|m`Yt$dqXETH{ArAqQA|5RxDdm4J^a)(H zALuoO@j1eMF$pVJh=*8o8{wGqA^Y`0I8S{#Vfh%QQ@+NQ z;feg1G(VQTZqbipGEdlp$wXVTAiHCQ{fP&Vsj{?i3kuUL7@QN)J%v^?P2g(S!vx3a w6q$NZhT5I7Ck1qgoIH!(H&crKXxK880~}oZzYzUj0ohRcU2S3;{=d$D0i-Cqs{jB1 literal 10205 zcma)CYmD4g6~Fh+zPi&v((* zIrrRi&pr3N?qjxIP0F?9N;NV5V=Jp`^+wA)m^5lh)%eyzxs{^LLyN5=Yf0LyueB=m zTDfYLl4awXhgM5#jbzCTxoI}Zl+$Z8Z(F% zNs8vsR{T;u0gs|%z~*V2>wqp0-3D|Y=iC{l=lTe|all18+!Lmr(m6@qFanO*jBP)# z%r@xkwoP)lC3T|yKu_~%e9otlC#G10NCTTp_+UaictR{VH`&>9FL<2l40}6iQtbpC zQ(JQQLKYZ9$}}*pC{OcTkG9%xJfJrKRa5Q&s=OZy=mgM%lrRZ&N#bx9l1tW%w#=5s z8>dxmKwklHTXL>dFRi2%ZdxrJ9FkdfyKwg->O$C6YSmDFA&tR?Z^^?Md>geA^M?K{ zFih@8&w54~Q?D?RV^tV#)>o;Z4@=E?7Rv&c_(=>@Bi#f{sW$^Pk~Xz^OKM81QTOw* z@b-_Qm*{$6M*%Jj#K+NoLJBy(hj)eIT^Mu=pqX#wQT44330fBsZ02hK>PL1_+oG5? zc?hL1%##D-M)Euh6aiwM7slq1)m7kPUx4QUz5`I;1hYUn_}h6mS8A@*A2BxPmdn*< zBJy*tyx2U{SW2hj1hnc@(2xGqI!OK4&aA#vX|^i0gFarAm-D9;=M&Ou^LwMq@7~>M z@)Wr4;CC1KJzLL(K|vZrz4>YMtB>abx(BElDvo~dE>1YV_yQ;n7Z^Q>Qd02 zp=u|C&|{#U2$JaBXF!Y`LZ+7)(=)X8_bA{L*yus!{XW_hpy8idbhnV5iBoB%yjYFv z(;QANm70(%Eji)v6Vi&>y{3CTqgv~@T5z7sOc)06S)%(%m3Yg9mXd14M;^7K6Mi}9 z9wBFbRL(T%*}{KIc4Z2&hF=C&+G0JONsn{As4U50iL7Rtl3;x!Ekay8pk|Af&by=zrKcZ;1yxiRhC)Cy zJ*j%aQ(|r@+*w$~u@Yi3+l0O>{I*U1-kx2gWX|<_>VJ>~qDuiyfa;d?UT_ulj>0+U z@k7-cW=z9`9(W&Zje;}^p+S3sS7mLzPatJ(;y9RPP`#GNGSP5tas4_eNG(YI(^k87~sFxGz9vGC;%>n_dvxkX_ z4A{u5ry=q*hcX;=Xb5ZeYld)74WdpkA^wK(x~I|JpcWUXuELWX>fNBV) zQF;sl>{jv*2TvqIHPfJ~C)nm()6wGk!{WeT$HU@OKv>*3`gQSKoC@T4o*}px-Q{M% z3a8qu=*^kAW4G7sWc-6>e^cXCdv60*rVZFfhL4U|SqYvD}Qfrcft;)ld z))BOg-3zEZs!bLNb}#J(Cwr~|8(cCEvW7|E(2MP}5D61nUh6CuNdARx31Gu%#Nr%c zKgTJ#Ivp^U6SBD+z|My-XXkvUHegx^k(l)A-v=h{-%*TG9D2fyaakJeH^xehFB9>` zh?U7lPPbaBgW?RjbQCiV-%^G%)r6(RLa1EHQ%@pv(6h!9wB|!ll&Izf2u16~<_*o0BU}=DZ zh$D!7EJTton4oSCrb(o&S>g99^lNel&Bj681aME5DSnU;qg#R2z(*+_=TohGM}a-| ze^owkcFuv-+NW4PZvz^toi16I5Ui6K+kTTHp^f=7Kv?WlFJdvOQXx)4rK7mxBF8?_ ztNSVR9FJt6&1;ngK{R`i5h@*Sy!NDk^Hw_aMM9v1hUr7e@`DCU@F?rRI4cN> z7|Wi$8Q9H{1hh|e4+9z5VsY8CXK49Zpp27KTFFSYI#17ev4`rsr#k!5^8x@gio=T& zC^0=}wuGa-d}X(JJc{#^J;tPOTzmpV7wZxqEG;s{t^;_GNrPhVcb208eFCV~s3#S5 z3vu}qnit{=5(s!fwIA&+5FkIw#YY7J#IFL3!V_jEQ2OL3uu*_-0Pq#Sc4S%a^99(s zO?PDxdTtNhz;*#VAEID8+IIk)KkB>ocd#=gU@yB{fWMz}H<+;?_y+^5h_6$2o{zxx zUj2G;Oz0LDLX9F^IxH@s_C*0cD)77z?d;h->2aaQukA~fgDdq`ef3DsO|51at>+-u z0m#dct2g+hrdN0nWeJ1+9XZ@A7&aVac^0+51EXwAi}?2Og)J^()cAUa3=B1-pbxd@ z1hH@Bn zFZCKJhrN2kzlntDj>&Y8@JC3Xm_GrdoleLTjl4OcZR|TRqWvu)tx!zORm`OEeqy5A z8n-g)%neq}Cw5lzMRvv}>jzeVhCRI?N+heGi4NgJ@J=4TTb1~nX;JCyyO|p1*Z`B3 zi}EJ{jAwMd%#4iQ!%k~J{v8}=x+DqF{sUbnI1UBf^vj=xPwWTy`3$eJ%gf=l$^MI7 z@<3EeO6{+o_5*aG-$$ZUjl(5A3)^7XsnoK%k1@VB#Y@UIEq`HTF`I_eg3Q`Tn)T|# zi5xS6MNY@VuMtLjE!c|yI1stv^o=^?68h)}M-LXpvKO!Lur{6gaypyKj;C{JXp0a{ z@p-J!T!r>tUH!2be+1@eH$h#H@NSaUgiE}d;0*T- z$D`^z$74fRjrp5^+RI&+!w765#xn!E5dbOd_|u+N0o6@zAHMJncPa<9+$}-5TZ3}! zqIo+_p(pP9ITTA zhdbU6z_Ev7{Syw1u^xbiWS4ppTfRFWz&}*Ji8fbxABY+{z|yRo(|ch|$?7x-XY3h%PsI@_lF5}!HTtCKMig{eLb#2m4Jgf3*=bA8w zL%#4928tm|sec?K=-UOgb90~B40NxPPC&e_et7&3`>DCZVQGyMji*dm? zh{6*GST_+A2~1P8+@~lMfT_xtFsB*LEDijS;l9rHTR@|pELGc7#b%_nn_CE@k2|9q z<<#@&k8%pl=c2?z`?JBMnrLAq2xb+x3##x?5{Y{b-JL0R9JFKT=}xf&>2`B~D;oyu zmjE=YXkug)z2gp0F=iFA%pr|CvWk00crkh!Y;C_VEgh1lwtB7S;d;MN8IBglHvRms zg7hM$|GL6(8se+E}5ctml^x5x~fc`>I_YxUi1^OeRuL1q> zU@C-u`3tO{ZvBGlPk7N0WjlzBjOdw?6^7>#9Xdt%aD|BuV$skFx)OkC0FIy37qX{8 zP_mXVoLu!)>!)MVbKXjz=MrYel`PgA4in0cQe7qBRWM2kASX59D~H+1@H;1c%xHg# zU}&(1EeQm4dG`($;m%<>{~0FK6LYU b!M3Js-RQ-Ck?BwWS<~3r+R|?POW%J0hWS3X diff --git a/src/builtin/pair.lean b/src/builtin/pair.lean new file mode 100644 index 0000000000..2b82fab4c4 --- /dev/null +++ b/src/builtin/pair.lean @@ -0,0 +1,10 @@ +-- Copyright (c) 2014 Microsoft Corporation. All rights reserved. +-- Released under Apache 2.0 license as described in the file LICENSE. +-- Author: Leonardo de Moura +definition pair {A : (Type U)} {B : (Type U)} (a : A) (b : B) := tuple a, b +theorem pair_inj1 {A : (Type U)} {B : A → (Type U)} {a b : sig x, B x} (H : a = b) : proj1 a = proj1 b +:= subst (refl (proj1 a)) H +theorem pair_inj2 {A B : (Type U)} {a b : A # B} (H : a = b) : proj2 a = proj2 b +:= subst (refl (proj2 a)) H +theorem pairext_proj {A B : (Type U)} {p : A # B} {a : A} {b : B} (H1 : proj1 p = a) (H2 : proj2 p = b) : p = (pair a b) +:= @pairext A (λ x, B) p (pair a b) H1 (to_heq H2) diff --git a/src/builtin/sum.lean b/src/builtin/sum.lean index d14b25025c..8283c6a593 100644 --- a/src/builtin/sum.lean +++ b/src/builtin/sum.lean @@ -2,6 +2,7 @@ -- Released under Apache 2.0 license as described in the file LICENSE. -- Author: Leonardo de Moura import macros +import pair import subtype import optional using subtype @@ -12,15 +13,6 @@ definition sum_pred (A B : (Type U)) := λ p : (optional A) # (optional B), (pro definition sum (A B : (Type U)) := subtype ((optional A) # (optional B)) (sum_pred A B) namespace sum --- TODO: move pair, pair_inj1 and pair_inj2 to separate file -definition pair {A : (Type U)} {B : (Type U)} (a : A) (b : B) := tuple a, b -theorem pair_inj1 {A : (Type U)} {B : A → (Type U)} {a b : sig x, B x} (H : a = b) : proj1 a = proj1 b -:= subst (refl (proj1 a)) H -theorem pair_inj2 {A B : (Type U)} {a b : A # B} (H : a = b) : proj2 a = proj2 b -:= subst (refl (proj2 a)) H -theorem pairext_proj {A B : (Type U)} {p : A # B} {a : A} {b : B} (H1 : proj1 p = a) (H2 : proj2 p = b) : p = (pair a b) -:= @pairext A (λ x, B) p (pair a b) H1 (to_heq H2) - theorem inl_pred {A : (Type U)} (a : A) (B : (Type U)) : sum_pred A B (pair (some a) none) := not_intro (assume N : (some a = none) = (none = (optional::@none B)),