From 30570c843faece9b776019df30bcaa981fe00eaa Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 5 Feb 2014 17:33:06 -0800 Subject: [PATCH] feat(builtin): add optional type Signed-off-by: Leonardo de Moura --- src/builtin/CMakeLists.txt | 2 + src/builtin/kernel.lean | 3 ++ src/builtin/obj/kernel.olean | Bin 49208 -> 49327 bytes src/builtin/obj/optional.olean | Bin 0 -> 3710 bytes src/builtin/obj/subtype.olean | Bin 0 -> 3049 bytes src/builtin/optional.lean | 69 +++++++++++++++++++++++++++++++++ src/builtin/subtype.lean | 27 +++++-------- src/kernel/kernel_decls.cpp | 1 + src/kernel/kernel_decls.h | 4 ++ 9 files changed, 88 insertions(+), 18 deletions(-) create mode 100644 src/builtin/obj/optional.olean create mode 100644 src/builtin/obj/subtype.olean create mode 100644 src/builtin/optional.lean diff --git a/src/builtin/CMakeLists.txt b/src/builtin/CMakeLists.txt index 40cb8f1df..36ff51bfb 100644 --- a/src/builtin/CMakeLists.txt +++ b/src/builtin/CMakeLists.txt @@ -93,6 +93,8 @@ add_kernel_theory("Nat.lean" ${CMAKE_CURRENT_BINARY_DIR}/kernel.olean) add_theory("Int.lean" "${CMAKE_CURRENT_BINARY_DIR}/Nat.olean") 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") update_interface("kernel.olean" "kernel" "-n") update_interface("Nat.olean" "library/arith" "-n") diff --git a/src/builtin/kernel.lean b/src/builtin/kernel.lean index 0d155c5aa..9fcf643a7 100644 --- a/src/builtin/kernel.lean +++ b/src/builtin/kernel.lean @@ -88,6 +88,9 @@ theorem absurd {a : Bool} (H1 : a) (H2 : ¬ a) : false definition Exists (A : (Type U)) (P : A → Bool) := ¬ (∀ x, ¬ (P x)) +definition exists_unique {A : (Type U)} (p : A → Bool) +:= ∃ x, p x ∧ ∀ y, y ≠ x → ¬ p y + axiom case (P : Bool → Bool) (H1 : P true) (H2 : P false) (a : Bool) : P a theorem false_elim (a : Bool) (H : false) : a diff --git a/src/builtin/obj/kernel.olean b/src/builtin/obj/kernel.olean index 2c41e93644c73a46bdbe947eee05667c0fa2d9b7..6c1b816f472ab11adfac0a85f132c3a9d4489623 100644 GIT binary patch literal 49327 zcmcJ237B0~mF}5t-Jv3eR&k_XLy*LhC`7~o6iE;w3M2^P0G2m3kRnMXR3#7;mA08W zPA&R7F}1?cy^d|!60z4zK{ zuf3){oPEySxPGELJvp_0B6I)pEz?t{Pt43tWW@_r@+>o>IDPA|BSWj%J;IH755Dz zgMc)O-LlPVv!Z_xAlG>^(#If4_$MEaMxj_@eP)mmf{8dLZkL?chAcnmT@xQJhNp2by=lOTE$jnSw?D4 zB#4B{Sb{NZo|!s*s=HnSc|x`iYWGI67|D`jH<|uPTAH2gt~blZzpAH$4iQzGch^sK z&5(bx?E}Od3HcAIo4=JSOq);O-{NK=6ETvBtt{=e)h~RE$V;e~MWV2A#w^vf6(yug zkW}8LNOTd3_D90zWiRQo&SLT3vTkwKTY1vcRf)z2^;Z4lf{!G1wEXV$I1sY~!k7Xd z;=%LFzLxdU+jn1*Tg1Aj)%bY&NvZ_(gL~Wkw4e!>0996SF`b#7hqsC0k6J zCF9>Cn?AVsAw>7o5P-F(x4`FErtXhF`Nw}rJn}j8$nL0hFxnlRSUmM-n&$b=Bwac6Bw&AP;z$=sybws=BPoeM5$Tq%4y-QCKd=x zZ`?dOHNAOeW26I7;osAcETd>%46q{j5`e4j&;QH%akY8rNJVILz*4vn$goch%*|m z?4|6P8Xf~E*^L8Sx-ZF|3^-GGd=g>yUV`$5%|ZMY4%e{O0AmyX4k3epq*fZ{I`&0h zQD3J3LEu_|hY(>3;4-sZ@w@KHtl=6^>TxGHOQyNmb{07j3SqaUWX3E%~=tAJwWq2#|?u^2pF%m zI(56oR=HyvZOWS13_o%mYSfe?*JKrl$)yGrDrlVzq>AgvH+p|(!>eVQTjb=C;0PLw zu&=$@mibx-L|Q5eudP#{Z!WF1U}2ps3+e0Wh(~A7=x*9Hk;G+<9E@CraUMV^ z`uqr90PrSLG*z5!M|RxX*SVH4Uqqyw-LhsD!RRm`WVTz8u7jzY6UM26R;oC)2&WvgF?-f?*%BAzX+h>(8U1v zT!M5bl7uhs4C^9!vQD9{i}oLzglP3{qvS_n(R#XPX75+v7<$g2rvnmKiF6fcYiv+$ zWh|Tn4Kk>q{|oXO`lSFh^!EeQ&@Tfh+z$Y}kJkD@fcHm%kgQl?{rgZqr*2_QL(C(g zTuMUTm@ctgFeaP1PMLxK90nYi@^TMM60m9Yl;B<*9@iMCTL)dM(-!joiiCsJh>=ZX z!NLvEx;5Yr14|P5NCZC$P;>L;sBd$a+&gJX|2RsAWyTi<{wSAJIK^5J${&+xgbYLm zZ;du12GJnc%!e$~E30J#Wz|Ki%uGUFU?Q3fOi@pi6>#p4tn45wRE`!I1f~2>0as%A zbOb*GP;&b>fWp1fpnNY%=xUVGP;#CH^vFUxX=f%toFfBND#yO9R~Gr+Knk+B!ZN+G z7$}OwY^*`v_QBC4AmQxjb*Y?_n2gzKd{9K!42k8%I$gKZ1l4 zI4jOZmQ$%)USg-lgA(|5q^D*S&X=r3ejbs?)F9T3nKz@N!PDoZ_AaRo7Pnw{)< z6B)3oKN`Ks`)@SRP1#?I;MV~j9cH$Lwed!2v!Vm+uyp&XWo$;TZH~|4tTc%8q950>eTh00{xyU33l7OF@Mic{EQ4X?P%rUaw_*DFG%Dp2IQxa%OA3a;Ey8s z;|T6F&@l{`%imy@Bq{BP!j}Zlh*A#x{{SV<6OH$WC+Rn!yBV_fGmw@5Z;#;riQpXu zk~OYNjo-lJA|NGpQi~hGAbtuoA2c@l^Ii_82>zF@Usr-~wmTB7L4IjazMcI33Z+`Q z+yziG(%k@em(-BzoShb0Gt>LD1=#~g^P2FTR+n&`JTS<&`+(8U@SfHxzldD^H$XA` z8v`A~_W%^b_X6BAs`)<4<`*%4DyraNIhUoZVZ09l{k2tk_NFE$xi9b8{RS6XscpzA zkfgv7gq+R&4u#S@`f%X=2IZd!N?sUQtO+u3^IL1-{oOG$Pf$WH`6rM}Qc8bBfjIb6 z1pf>KaG+6?3OtA^^DFERR_A!I8EH1zC(NfXI`0b541VjLZm^JprNp$(!SpGG=4c~@ z=7g!xya2-W#`OWL|HUHwk#kU?^ka5K(m{HE1zPlDwa{a? zTzH_7ysZ;$JTfF{yU?7&_QPV&1d@d2hbWV%TvC>X{p^y_#J@=yEU>Pe3?2a%C4=1n zN(PSvC>elC{$n;{XnJUSq9_9nmx3rk)LTG4Y?(0JiPJXs9kVGMVx{evdK5tVjaJ%M zMkgI1R+KSkYWBw(c7L`P^xqh=)^Zc4DT;(}j5P#E>G*_a5@o+@d z6%@Il;JM)H9Ws{P>exc-paFw~VmJrDguHVUQq2>9BX*u>Q2rOPlVecuJob1eGj$>O z@ju>b#YR|q(sIC_BJhcTmJS!)EnBmE5iSnDPS1n4S%6%a>u#WFGcdboHrIogR)a$CzaYzrCmrlW7JA}x3Xey)U4hIDM84m z*c*nGKZ(<6{=cZ`VlSX1T|&ar)zVs*($4%{(g^BZqObs=f_~92X(z=X)c8n!(EPyx ztqS7JuQ$rsp5Q5`ooY^aDoQ2v{Q#EKc+SS*;bs05tFd#*y6W*LG~vdFw8KDX5KAuF z6w831dFJUvC0F~SRIG4zmHz{`SVm8ph=bw!T8lg~H}9Guf10)TGjA|OJzI6g=()ne z&V}9s0V?P`)1bmF;X?lzN5Cgu#j}75Yl*S`8J39=2a9$*&7EiMHr-v5Y=aL0Ap0JL}~SCToplL@>SpjdlJ1dlebnB@*9hh7XD32id0H;%HBTK~IJ z76Yn=OTDSnRiG;n(Ycs~0E?HRv{e64#=!oMv0~T1J-TzZ8G^?J9gVTQltt}uKpcKo+WzSF$|>V z=9Xsecp)j7g9CB4)VbRn(AGJGMaVFuJwQKu2l8Ac?+6~qEYD2ocJ;)Y(s9<(hcLUa zwIzM_hv4N!#0gaEFpltKbSY`P+Mwcnoa%FsGlEE57$Zz8H;eas8y4D?7Pr+|M(uE~ zO6~ZER{2RrN5Kxy>L#|%^9bFd9RA@M`Wl)+K1u%xtFY81$ABu%$0IlakY}y=q(S*4 zC(BC*kr^3OxRi?ECZ{4*B#9WyBUSWCq7FtVD3tcJYTU~tykKKOG{Z6Ktyqj$L>qFT&hAQ_)h6@avF3##lo()EEE zV(}Ry=@`^MO0TZTnA?dKNsL+qv%X*V+1z=l!={YP(I0pdM@&64Gam?`{xELam-<#)5qLOG)XU2 zR>+ga2zi-BUgl2w(K7tI36}RlHagoROV8C=yFYBsXRLud5gWaE*jQaNC{pB=fSi#? zY@CU{SHs?m$ObkO2cROEsx|clg^R7F!E{`;m(&^7Rvfx(ZWg-^BgOcHJ8J82)QGj$ z1LUbi{sw?fLM^}?&>nzjGhxefH)p7fYmfB!$3_9<%yG%)D^S3=MtLv^#&?$0dAW{G z;rhY+Jd+P;^-Z8Dp8o-$uF6tNS+)m8;wEryxH z0Bq@xB#8Gs%lPRHcON%zjQhp9p#5_N-K~L7=hs`39m@XS0#FivD?qXGHh^kCd1LVT z_1+}kj7mG1>)G7ksC_)^DRSEADeL7HJE8Rxlbc8FhEC4~hU3BvZKugya3h`DYQ~|` z^YCz&ewXP^6lX?VIEa?1yPM2Ysn(`DJG*hrx)2c~DkAnY^tJ43M>K{xYH){ARMrVI z9y6S~nF>h8wP+hj(Y6PyqMbbIeSlQwNHu~o?j#>U4T6e$Ct68y?=q--B1^Xe{5yj0 z0k|Yw&1iZ)nx2m(hM)~P7FDG#6lu6*iF^dHmHRyyej*sqI|!jLKh+Yh;mT*DP>YQE ztN_Z{P9)^ySq7BP#2|F~;2!5%HeW$mNN!vTCZtq_R#G$bG+$C>|9erfY?KVo8}^0P zHZH)Op~?Deo|J3XjzY4V*v&z)TMGY!$ZKBs5WzSv++_LkB|f6^ytud&I8lBdM>eh_ zW!s-eVH_^1HFfAD`x;aSZP}A_MWFH}R2w@8BQDMba_m49*a0c9m)L>&X9ucbSMXii zrg&GXizz(CqEAtl#$lp1@yiBkIn2uo_8jNlang8<9X779j?z}#({;)Xh^p+?eC zT4ii=jYR^!C1(_MzQhtb6<=QjSh4%P2wGBJghU)_ z#R0*%m0?F`n^b4e5RR{RA&e2Uruata)n7(F5e8%9h!+NPSe^qb)BHd!kj&XA^jbi_ zyBMsxL<9BvHGuWOe%#7RaR6bJmjFpEHPkPmAP%*=Wpna=gyai^-Ez55-<8j9n+a+y;!z0sC1@x@o1DcQ}}h2o{QzcU!f&CYRqPgY=5&R)QO-4Tg$WwHkS23dU0GOA5%E_oCRUt2X zO6DC93Cs5HTgI&~a11-o0)uo{0hMQm8IL(>qB?BcX;qGM2G{6X#jMqoH#=u4X0;Pv z0erW7)(PY>EFsslua1h3suz17y&02lc?+u5=*h_6iagu1kZ(Yix77-vBOW;qj_Pr2 z9H64q?Vu4yRsIzD5Iuj&&SO6sfe#?u<%(5SsFnmgD-UPIaxj%aE)#L}78bMg$zPxo z8PuH-{3SuiPczhA29ssz@=sp$^GEP#2qWx^BKf0Y(G}Uy`-(rWiS|lC3CBxe7i$ReBW!hQY5oU*bunNy zQHe8jR_zWXwbZowTNG$ML^!CwEl3Wvpo&6RjV2Ppp8zI8c#5i=B|HT}$aH>EGYUq0 zS#A`P3Vq0Mhgvlu3C9a5PCEWLBAsW((7l!b*(!s|yAxs&q(jJ-9$*6)c>zdqqsR$j zY$aD*74ncrwL27-{~Y;bpV&K-hbg6J#-y})+|gHDpUi>ktg{by&~y&`0rR;pu1)A< zL@$Z<%cf%g& zF;rSXqfWXx65V)TtBzd6EE064Wga*!e&~A}>}qK7G$gBO4|@RQax&hn$X54|=;Iho zc-|{{JdPv~({&W>s$67bu2&v+c=G+5FE0$roWf8aPhuZ1?gGwPy~4W_5qm8&Dzr!Q zzIc7_$`8eZ%q^4;z&F1A5YiX-!=VkG5U!aWLhvAfE({n{Fo1CK)=iSAWqbSvT-ZW! z6d*jL!QbqVC6**dH`^oP@u=4mGVTMg)0RObTVIBQbAUN+)jih^xB+4nrHSUit41Ro zY8SIlMm!SJL$V1J>fM$7Sr1el#8n1W>ru#hUBuv`AzYo}yGMgp(`c7}VjujWD7ORR zZH0oNUh<a{3Co*Y-s0B1;zi3c1+NO8j#ny@s8hwBv#dd(OJ8VmVr4 zA7!h2@^mWlBFqK9x7_fS&sHF4i9}Ds?m%}Ob-kv`(q{lm{2vJD4J>^oz_T^QpJcH0 z)GUr8uwAo{?{1E9V1K4_Kv3{_4nRKs&fZ~Abw2WVu8qId`5XaxqmNPTgciO?Us)+2 zD1YYfUQzeYs}2K=9^uH?{9}l0JPIfo{~>I};XMx&G=4t(;ZCDC6s0guyo*NZrFOMd z*X?MsARYP!FTau4BS1T_20XI z8Q~!1FmO4a8A#RLRrv42^`g&X7utRrGgMqeU-X-xq;4tUIA3O$}0iNf?j1% zb(bu`zLVl6W=G8m|n!v++Sc^}?^ou9bK(xQ#ZlReWgV|Upg^jTk{ z*nEkWjXlxQ9tG3?xKxSfl(bCr;!OTDgB&+A1~&Gku5h5|q_7#Ki=zSa7_*>2z?1ev zBxv3!E5suuLC|Bqz>i^*<;pzchYP0SD7N+s54K|#V(TgVtv(osrO6A=wjI~61%^EN zb;OOVVyxAbG^i&tr3axjr-k(T4pzJ3dRz3JGydVD?tPv zZ2FUO#4dpNzu?Aibw$_f7<0A@oVLN| zHZysc7k295-axAu2XThY(JpT5tQ>V;Y0{31tHTN?loKvGkFLREhLxjZDCOkecq=E_ zfXfdXO4&RVsQ6dlD|lyeCDWuQuLW zM*(5DedD5fP1>6reFP}kP9&5&xgLQ~`d<@jSz+->OBz_$HD1}9uU{@}yk{Ta<0Oe< za4*#q!zjpC!0O@&MuW>g-cD#xadS1kFrMszUGViOA|M$dUol_1^wy}oc`W8Aughwk zQW(iJm0lELCs+7RC6SL|#PNu)@m^%NLGjbne7P1K#7%9~CgUx&-luTTAa^)HYJ9jR zHx$~fj?&WNv4CZpiAF_w7n1uov?A6692D~%6l$}xH$WIifM%`&mBKx4pjodxC1{I!Ot7mxSh>z0C)%GP1~8n$aOG-9@3yZ2d#EdoiSt-Y(Rd`0qVQa zRPh^2=TY&!uC7aF9b86e&`4-B=?NByHiV2;c*zJTig=+$E!z|atg*N3)? zzLyC_r${9Xiai6E@UA%JtYIK7P^G&ZydYS*zM!ir|?9kGx@g%$83s9RfW z7S4}EaTSu_aPGhx72#m&J3zJ90eGC?CGxQ668HS;93$5FnVUQS-(ktne$@AW8R$m* zg9!dGfiHgq5$Zrku!Z`6HZdpqR!ATsbT^A+DW z+`i%ePpo=~R~?FsU0Ew+DaR5XS4q%SXT_Jx%fER zQp+N0o5H|O2W5#7c z-AIT;#{!Y?nbP7;%k&HSVL6FWXxyHxs>aa)k0Kf{j-it&rr)7Z!ejImcz-PYeFXnt zpj$-!(ZHcCebRMjU>McVGmuPJl1Zd51UMH3$?(Z=Lg7zBQeEI=Tx&guq_pvo{}snm z_S}j|_LOL_+TR+@eqsKPT<+BnS_vj4G&>ayU=cxLP?Tk5r9Cd^CK6~kF?M%6VnSd! zg+o&dqd-gzqrd}5^S=ROkULQzFe!H@^dL}OhJ=?!^m>CB`KvhWz_(^bOaP)b zbl{WG>>rWvbq3vPt+N=o8`5jp#OG#6S7Yn={y{V1?7T1ci(%|~hb|%4j|LagtPZhQ zx(5*6%_WE)$H-z2rniCPw!-&=qTs zCkTFu?>eK)ZbBIX!qAtzB5sV*PmGRqw*$LwbRd|0*#5iQ*2D~YD|rMR^_FqoPL0%B z4t?E{e#->SsbHSY9I19183PU#*k_5sW?dtroNs-ch&%S=;vrm zm*M?@LTe5=GV1R^QsZ;zFBE=6!h&dst0EpA9}ht(9F-`b9gx?{g7fRuOFBOzVh3%qok%Jq3X_0X!Dy63Je{ej zd95V_Dx0e%#d9hs)d-U}gd^1XE913+NB(t>eH8C@bJ0?lnB)dZ5FzmXFY=%K) zV)NN#vrEmeL5Q+y6I-%Njv4iu=(%5otu5 zRY8Y6b&0A5luLvmXimmY*VkuFm^ja6(!05ubEsZQQ&ag%fU0*lE(J(SfQvTaSS6l% zXpzA%=+7_Ptu7-}BL(74k;6}}n}Z?^P5Ga5*hY}OV7%~8d;=Ym*P|Mt0L z0LAoofx>f;(6!>}e73zecsEZ1(sppvTu-of9C})-EkNH&CMt?uC5ju=b@Qa&uH}Fj zcJoNH7PmcHUDs*sgw_CGZ=PI7vclqc)SO+fsmq!s$H;hmZKS2O=YqO94oVY9$W1hx z=HCN{Hy!##Uhj#vqR_-KM1y&gwEBDyt83K_V_vQ5&V5a*#qqtOZJup}b@tKZj9xc? zvh~okN`Y^!jiB~%RjHDge7ywIIU?1r_Y2JvjLRkun@YOBA`9nvfyV*i1dfgBpr@Uz z)!0#1=N2{8T-cQ!YsGFg=I*rE&Sl(w>TPCfjeWfh2keKTDK2bn0)X2P-#U*FUj)=| zZ(8A2mg%Mqk27dIx~$5)J(_elz#NCtN|>Q8!;~1G+iJWFU;`uJoyg`#TPUEna0Y#3qls^eO{-paUa&cBej3fgwIqHLU#}pxFTc+>_mF0FrbE5FWH~c4>Z^;g|bm zHYAR}C|SPLaC4@kwH;oAPQhfF4T%$c5=(&|4dUb~`lQz&T+(@> zT@?M+1?VDcF!rqSULtoq7&RQ7-0|R0?JJs>(;Z>*&K*xf6|a?+GXN8J`~}CZ8>KMV z=AB4x23FXE{Q}-w-r_r=w?g>ME7;NLK-QVvZ2+kkaTp{HE7yr$PpuU5%YdeiA`#|q z^BqIHyeKZUDfkiPR;y|L0SW!OH!N zHUMf}S3@Tb<%I{7PBE`Xsr>5=0Hb1BjhbTo4_!u9^vfk&n@}YbxmQ}Nu^6Pk0;(a* z>Fk(1t3|yJ_d-tWBe{!38BGmeus6M?AKoKNQx#tYMx}Uai8=8`& z`~^+*;sKCaJOtprJ~;;#rgP_3D;Xe~JR)+9!L=S0Z4L@*?PkdUuCwHVG+8a*1jIQ~ zqo~9+3VF3ZIcwk0JCxQFfJAEu{{K2F=`p^Z2>wvqKMt#Adz^@=^f)o|9fektc82wj zvom5T0K6GICU$lpZD7O-tE(+(?dIisU?N{{^zq??^Kvx~lR$;TvKDul1MK7AC01Kp zN^Gj0e!3y05eHj08@=5}i;C|Cf$Q@v;UsYeC*0PdP)epxDmio%&`%yPpt>d68uG0p zP%W(?d$+t5%R1{=`3Gi(rqj_K(PpjG!LjM6OFS{Du3`W9eOh&o5ZL|6S4 zZ9DeAb*NFIG+MhQ459{4Ra!5%BzjfoHrtwX3%pkXPaR;YY#nNe>&4v)DKD@h=PLGb zNWD*{Xh30S_${ zbMgs;C@u<4YfMwN>%6t4);SEZ`ZJoR7O|S$)K!xqz9ro_)nNSbx^Q3LUTGJht-H5^ z&5t%7KCUGiqYgWD^LbGw%%e=K&JIi zAXuFj$;NPriYt2FAZcC5D1i{!yvKLX=%$C|G~Wg`RJPJXN>iZ<|A;I(g@1$%f-!>J z$1G{y8PyTzUaP30`fbe829~F1WHJ^*QC!up)q*=}gYWL?q&Ldg?=cTUt3=T72>aK9 z3$!jIQ&*ut!n_)wO#Xix)Z*-yJd@)3uXUkznjZnOLZb%kwSJ`)yPf91HC5P|4BTqU z6b31ZWt?=!*>lLZs08g#5TM+=b}g{9e!31|V~Hj4#H{rh%eElf*1rv^X|S3b2!6p$ zV{Ks#*{Zx%FskTdEMkfudMaOMNIkLvuR?>YT1_vjf45xE3Si3a3O~FZ0L5^s(Mgt{ z{$Lnt&KJ0xw6`0TemyF9VpHB=pi}x60M^Cy6?TBxpmjMCv~PX2Cb0zR!hobtZ|-Gz z9{#n2RAV(zSI`_s>uBQyC5P_<)B@pq2DOt%Ev~J5zbnos@rM?ZC7OD-pg#kG)}@>KA~L4{ zt=pp2^-=KJ|F%)#hotS-yC=6y>xU2$x%fCi8?pt|B)V6a*dtvwDP0Nif7N>PYlz%^*zFMr_pnCZny>^Mbc`>bjtvjlFacYZS5wt_tc_?!w(_;LjKS5-ACR6^_ASdeIp;Xp=A3z*= z;cqs+xGY}aM#usXX+H}f-I?UV7WZB&_KN{yd3I|0l=TyvH%_OV2jMu*gDIr)5N+=e zI?Sbqatt(J^-P=jlXdF`@@E6}?q&HG1G942DYb1c3fm2#9EB${_R~fr6B!mH?v~n# zs8ALLh!vj#Y>2C)=4$Eqf~l`Wu^Z$fYp2*o)e}^#tqPFj4&M1WZ(Wv!~nKuL51Yua2r^ zSbiedI<;}b=*G#>v9%kg#%k}V8ybSoai$PSG5QNSvd0`NLzM!^sVLu;%C>wGtp*i{ z>kOXFdptqy!O0>eF%HA59%+e_4~F1$ySstyO+>)PxjnnDr9AQC+|xeY>zYAWy5QG= zBo=-)MynbOrrKsnHg5mhXT^pvC5lJei1t}T^45U^FuzrsU1z_Uv!NDVf)Ue3+M76Z zz-@g*l~OR9loV{{kXUsnL~SKfc#^eqQrOc#Cj~4w+M6(Rz8c-0g))=XQu9tYO}0PM z_UQmg(w}OY)Hp^A#fMHnD1?d8rrU205`l%$9GideZ2!TttrI@RV6h!E%?Vh-vyeD> z28e@z?6&>SL388Ga{ zYUfB0iJuFrr&y- zw1w=W2I|)a610~f(UCZ%(WYpU_SrO!+x@IOhZ}22|8pd>w~^-P+x)y#ddHDiUqaWP zi>y`1eDVE;Iq*!#AFRES?J(FNT?Uj zUj));LDS74fUaGPlr4E1qNJ0j%=n;`ZSHt4E>qx_vBdqEkus zbDWJ!tUz4JwSfFrEUE)7`DXKrZcXB<_LyO-NKtpE%s|x*`+Lv)cEO51J$0 z0Z8q`34ROs6%&|~9Ot(Il>7Y7D%yuf#)wZwur1K7jDyiehFSN9-?gl&I>Mt$Atcwn z)e8ALxblL)U9qIuK%?hdQig{7QN#9kEN{k-;sRr~491t3Kfl1;{yFNXY#M)92)@9I zgYkFmMXAK}$IvF3Q4`f;`c9@BawV%r6B+r7405J_6iRuwI9^->yVzip;oAiq4iRjkXya@FSsHEa)q`A0PJbZ z16us1zk9WXRXbV*7q0eRpS``ehWN$RfVXZj3-zx)&IMKJivn|KjL)o&o_RXa^aYc` zeS4>{TH2WKLgUVJgN!@RHJtc)0(~fz7QmW(1$vMzz+$T7EO9peQdG&tkB{I905x~N z44@XGCj#U{k?Q3D=Sb`o1{GHme5HY%=MX#z;32dMIE=o6#e+wEkA_1ccS@cI{O2#S zlwXj@SD0n#RndHfYzuPe#33JzEXJ+T@i$L3WYj32QDV^@I;crxz9SedYdXiEA=-3~ z9Z;iw=IS-Q9I;==krDE|gC-e1rWc*eMD$MW?j^_9cqIhdbF2+f3`a`PVH}&}D^XCp z@N(A?{E9PZGGN|`%66g#kwx+u7+E?mt@Rnqjzj32P$PdF@(dy(D(A+gg5Ae)>m~+| zJjECvztK-R0bP46>MU|gc@K~f`lxX$lX$>tQvV1N(zl7`YD3U#F{h$YA{@(gUJV14 zr*@8d5TjU%_A*8^T~$X%HQckaX;2MW?z7dX3feomNCf)8074zOedjbJuRwK_qSONt z9r`T~%ou-D#qE!Jbe8lp4mJ|SZL+N1`s@Vs!HPp~4^eSIb?Pyov$m!q9xBB1@?87dUS9 zowu3A5HtO`T-`|Aiv*A)3j`Qk{ZNcMnz$_NLmwdxB$zlm?+of8_nmjK8dC`UN<-56 zpw}YgER6L%kq7Ph{6p&tvdBI)yVQgQ5xEfrokd0(e@3BxI20JPlM> zWv3VbpN@h!i)s|q316tMV0jJhHsWI*Ev3k1*h0O=@cgluEe&81Jkxj(i?CK5`vQqn zd5-1WOnC}G>3eMiry_W&fwThuwGNIS_4Vbx(;jN-8c)`6lo16d6&iM*#yuXqx41uMk^E$&GokECbLlsV9<~LmLWBt{m-Fb_|LOfU}MMJ&pW!f*T{q zSSNiWsOD`V@O(msJ8Pxs_Y2wKIp|9ZI`)O6^JOGov4o#k($JE~Ft^C6QeW4UfI_&r zuJFhsIWl-;#oJCB;>cKo-dqhFUXcVfotu44=R5V9fxV-TxP7VWU)|!^2CgD9eaAE| z%QT%tmFOXOy&m@B9+^dR3!FFZ2h-V3BoI#Ldw{rtRs4#-f;vzC98d5gclB;>P+=$h zJh*};g&*avnTJT&)>aqC@QT7j+G3Ah%iab%TU^O%&I4-obxZO+qB6+?MB-{{A^{_f zKihnx1xj{KU8Ru{c;wNQW7Kk;@7B?QvjH{9r?NQWn+Mtkf(9O~~LH01I2L)0JpoL_%DPf!S)Uw^+rr@ZLNLVprR5YYH8eQGI4Pg zd03%)5OIb3cftl)TNM0hPg?JHjga2-FmRAJO^p`d;#qsN3ob|HK6g2F~yYdQRM zb}FZy8)*LzavJ8NrbJi+MMAE)u}MTyg7XfigV%#kO&xDQsYLQdfVA%FY=9EU-veaW zAAUSQ%3Qtr=UU06M#q)#f!r&ev#cb~kKNR@$29uY5M}HVVJ67FTp|D;&Jkn_Abw!N zTZ=t+;&185zJN*vJk+qEWsXU`{c-C4z4Sc!)iVI{<+F zSZ=X(86iG03CA0Z^==Z5g&cJ6P`6oQa~VEdo8CA*I=f}Yb7?ih&uqFkrShg{)jbe& zKW20)I=9C|G*kQ}x{i0;<*nE?V+%TqXYlW^jCIXBCR6U~X9ezvOifQtO;2q;Q?H$$ zinR%BqS}t;!$&vW!x3SP$X+sJaAM%5Iw-HXV?BOk>?pj=EBR>`9&7`^F669^$xa&C3wO@aiGdW()O4 zm%ASmJAsyTv0MS!JMDW>jy;&&Q#*ZP#vUKqZ=mGpn~D926(^(>)n!!g@n>$DI6CX7 zg|*6>9i~*kSa)`_KL;Kjb9M=!8%H|Kcp&#guWirShb(8Bgls`)bgkLEJ5%nVwG#ae zn@qa^+=rSla0zyu9#VsvU#tKM9fq4F)#X;~I$S$@=7tTvw;qpDCuWjb(HhWodI43* z7Le%g3y{39hS7sH;d$;S4T18x040>TQF;c+byutt$0TS10QQub`YXHDSWPShR$1||H*(;#R2K@!~H zI(CynFA#``7b@*FQh@(y$?zD#??({JQr-B}i)p<4S^W?Q?l>Ah~aA~OIkh{8@`5D=qd!1l#y$Y zr7;cT;GvIxWbqnrMzFMO z&tKDU6PdVh{WS;a35Z12I+J5hQz!CxBKyp!Os0NPz%efnegrV(hMf^%r+ z7|(svfX#^?yG!S}etl=(*!B)NB2(AE9=ZvA)WzSvTSsz48nog$ zkko`~{k>(K3H$-zy)6ABu((Uoug#+A@NZEVjb4V75cNZVHEPR3_Isw^81-!;SOJ14 zS=n7vAC>4LNRAQfuYQ2Z&VXmg8XzZIi4#_!Lh6Y%q$buGn560@hRKtmbXq}gG6FzS z4rTIZ%Q{K@C4zsAAY$6^UxC}O{~pW%?=S;Rtyn#PwFRgiX4qmVNw%u!d-#ExY0LP8 z&!I4qYCIrChN(G`t5+L2`-z|6DI}*5okYs`@UI@Sqe!ESc;1-ALEtQSB$!!fz1dIu z#NNnFWL{pu!WgWR6^Mov6e`z>k9^2nf*!{za~LrehIfJy)VS6LEqFA_Fn|Sn^x}{q zA`)l8qdcOEnu{$zd>sk{#RYo=92yuMCXr~uUz{1;15ZyVi=%gusn;|kdLpr?if~=z zPe#z6F4OlmZCM|V3FLa-jSvD@vN&rQ*x-7a7H9rA3C8f^L>B;`+1DM^eTx7NT3_I} z7dXSJB;SK#gSGPaqlVuEqBK+)QBZIU=?qcT#dIbla=ZpuUBJ`U1_rR;sYDnyP_tBn z?!;5+#v_2hPl7ja!m(g!%?CMku*U^>@={&ApQXcG648*D(2%0u2J%116Z#M}qgW4$ z{O}C>(XQYboTr9w50V(Z-7xk0To4q`)vB+v8VioTYShT`4wtaq+(qjf{y~~+oM^ZT zKr*4&>CdbpKOEHvnALZJbFgqYR4>3~_k&7LKBrGd3@V^k0f!)oEzu-8C=%om(11h|1ZM6H(CMT*q~)X&JDm{5 z2R;!sepi_w>i9xX5d>#=iQ^k&6lry4)ac9=MXMxaoY*!#wPidjPRsJ#YON^NZko=<#@A=XspoAT zKP_wf26k$rEH<7qGBvd&D-3OPYiBy!Hae9R$8OrxF>Ipctl2RB@~l-HqncK6tOrK3 z!oa*$tYuAE;=d|8VdG|AH>@o3{3V;FN2ez?O`ubd@PEb;9P+1re|8CKoI<8Y}HVHl)bFF zM~n;#k`#Mo(;Kp)R|t@6KMmzRC=&k3#}iN~me}4tm>7`BBYO@W56m2+m?=j3iW-a% z2dqG7?|7YvMh5mnyBK&Pz&2~21h5n@7#9|`e|vjg_O%PA^XaLr<7mq&4bm#M>ymY( z_GE%6Xp9ArVR~v}+r(%`3i%(|!Du}Q#e5VCPTp+xCuv!B{b`V0op`VYd+eU z7&S-U{g%s#IUKG(tYHpNC`?*R;NSdaAr~={iLWf|_SKs|PUHo&%REuoG-aOZ`ic_D z1t==-QzSYMRf|xtd)ZC;m9J#=0c@L}bvK^zEH$F@Vcku;FT5gYqvwxKjsY=S9ApZ7 zhzHLv$6C@&?~p@CZXVm7S>xkbXQ&a>kLd2V`@)YVZRBHOl07EP zlkxAdO`lx62r)b*0fw zx65!z1t`1Vav{C(Qg1QWQ66tWb!F zZcQ&;_yX2HiH*nBOtkxgooYq*m58o!$m$%F+#QCdHrb^+N{HpCHIH3BDcn`W0)fd* z(<2j;(^H!w9jFTbo{3@!Rr6wi6~U7LvMD6y6Rk!GYjo|Fty5!Nq!t68`d>nbr4;@W zREX-y0LAM{fJ>xsfTh>+3cK+6fBVFi=`E?5SB61pRw`JePXQ5`^`!tur5vAKN?o!n z(cZ=^wQkh1P^%y>*?iN;;*1z1K5W-Zbj=dbZMkPAX^G| z6z5AMFsRrdC^&``>BkteYBz@5tVgkRHI&g#)BuUjrIatjAX39Q5#-Ra$wt)f(8RbJ za5k6W`)Yu~0~BIl!Y-tMO;ZXeEOKf#w=Cp%jIk*fX%SdXbuqyn`_v$wya#Y$>xah zX~dBmP~+6nphBu&rLx3%7_s8QZMvDRIX*7eoK#-ts;UC+Fbj@#5I|Md1|ZTxQP@(a zz}Q?^>%q$58d+Ah;rFS;BU{cL-Mo1`Nrddi++2xD%hmnu&&mC*Kc8K%;9VKitjWdS0w zQ^ybedSK-C4@&3Yn=x?qtyz{8O_#{O8vOS5AlTQGU|-K0f(9tfpwRe$q%J@FTT$aj zKW}6IrG^3x=?4U|{UsYfk|jk2+25m5lhaOs3i*oxDi6IA;Qk9xej7!?mk)+cBv00< z)J}BN*d=7Ei;R+&!m{;b*HqeTz;zfogPj&9p%UpT(bm|Y*~(bC3pB`}M1MD~CHi{+ zO7wpKDAC^wP`K{{csITE{Q&QY3L#ms!uCthzDvWxn+AA|f_mw;=DVyqIFrp>XHOx1 zf-4`3Zt!U>>1JG)XU) zM({%bHA7zp@FC)U7@#Khj~JA@)xui?m()(GqGAKOb7jPX$7Gg8h> zcVOj1K%!J)*c|!L9l!d1-}lcQW7T;ft)$yMmGXMZp5iXZgdlBXGq~w z2IYqm{AYj*W6&i-f*Us^L+=4GR#m-jP#U*8MSa7ryi)|z$ z`MnV^Hx6Jv(2Rhs1iKR)(M|ywSOiMfTEfTw*|kxM3fIFZIE}MmD=s;qxRNTjmRa~0PS<1e=jHSZ#Q*7hsFpv-nNKuz4Y zMDR-hSA_X(ZcW~(Z8k6{!UFD#*45_q+CAwjIX8}#ApFJpE$Jn%Q>(S*t1%}-fMnam zXMlKjvcfc}MFlC!?`{Ke$@0|*-VSgDwM^5OhuC$_^*Fttqs1_$GwY2aibvuhZ+*qu z+}*>(#?59?O?paGshZb;3O1kIdfUR)aT@}ctcdNe6PXNtBZB`L!G8lNbN#zOe`l2> zyYsy>f6Y+*ybLyNN8{0Q8uJ46pVI)0&2mA>9ZUp}Wpcwv7gK}GQyIaAT zsC;PvnACFMA4?R^zw!R4G@ValxDDj;4v-dW-;dybMeqj(k~KNfLy^gOKuY|imN$Y! zd=F?oX>9V_tQ4mR@t3Y*mxFM&Hwvvp?ldUZ68gue)dJ=&fSQs18{pp38cJ<%(?e@+ zdbe&w_65=&UHC`VmT;Wx)8}vV38R? zc)bQq@Ti=@#+IF^3kv;-U3m5;*01N?dDlI#CObryZbnw3I~C3(B%k{QDrNb5BY2;I z`Q^dLb0dp2MFwtuZasXwJ7)HflrTzuIf^r=rC*^!9B}Fq_-kSr2a=*x;z3r~v%!98 zZH@<%AkKRD8JFT*51MQ z=dmdobOzTPill?~eq+_%mKMjxy-!2Ophti9*P+SXB>=jcnKOzM2h&QJA|>HT?LTB4 zok$OZ2t~>PNhB>tDSnPMhGH>?Qu13CpaMBaD+$V^wG5XgTIg|DT9$4n!J|qdLu?6C zLhA{lx5*CyWC^+^DjXMc>@LGG#@a~>455?S@RZZrGr6(@^7;n z#rgB@jG_)GE_*_SA)0f9dJuQ~<l?@$sYso${3`>xK>VH0}#X& z`E23vTiqPU)vwla<1beh3F(-*1AVVT!L8~1u>dtJHF}ly>`p|rapotlWJVy`LN=rD zPM_~(7aG`7Yd?V@ka9Q$U_ss~g|zT^;E0_k7?l5t>}W}EDxi{o1e_ivc=;cPZrt4n zOHX>vKE6}F0?@*tVsz{FET4yqMg1^_O?Wisf6@b=&+5Syh#HX0=eX zw)p1iHb)@je-z2>20KKqnZsH)*(M;ZRX`k`jb&o^^>EQ9M}gH`tstU%h|dGe+Tggr z00rz&42r8)7@Vm~dvt8fo_eDqEBUa4Yx$m9-7aAH3K8(f=dNyfm}pn(205~%^mG8O z`)pAbPgqde!%ZwT`L7DSsa&x*ToYB+WwbMExyP*>!iwUFfL0xh@*orx|B0nR`92J) z{E0Mlu^(IGkYL#PPHjkvGQ8&@p9)I#AyHXC@`4X1dNu8|7?c{HWcQmtDA3Bt?Ttn` z+n9vN?JU}BFC_O2thBlJ6Sh9o?wF`d$vQ1+~RBUk=c*@^rL` zl_dV3!467&Q5ZV17I`_1wx>m2KHvKLnK!ti9%(vf#QF(?Fw-dMFqtXoJd;he@v|l9 z!JVd}PvSe&8e_)6q8$%W_po-G99^5-1}_C+%|wd;iiyP$#K^_*N`e^2u!o8bquXo( z-EOyuE`6bXhovj`cyb4Ai*#eVI6i}SAXLUp!5Kgu6bO6GBqcAs2RzHJ{L;&U*~>J` z60kTP1T?2S7obFWUIejYQ5*!#SoR8gbCZueZmkO`NwIDi)K6!=1`EGBq|lfy2Cjery$k@1BhwIdd_$4DypuAtssX1->NK zo@`+83TD2Q0AES)6a(}9qCg!tyJv}AXNG|E?A*%CZ7(D>yAVK}Ew%5q3uqmOFb@|D z;RhIJ7vP$!-*4I--Q9gR->oHwG0u zIo0PNX9Q8WG)5Q(gA4e38&=v$5_hY!gw}ZnaA+O>=qf+WYGh|Tu^ZpMhX?7FwI zXrKjdFggvW_^{{`MDdY+{bzs*){85w=i0QV)(dE-XAA=(dVS^2N;X5^Yu5v@_=pr< z6NHpzz?kmKCudaBL`6%S& zR?{paS9|ULjygZb@TDW%=#f%2^*Ss!L)6cJ)ZDWRAC+letu&d z`)*XoG_L{3hhh0^0cr*RI)GYFyxt(|3o&yzfNe3M2(f*>UHIt@M-Hbq#rws&qW!}U zov=Yn=Qo1bQB?CA0g9Ci0E(420aOR-8^Y%|dgHzUjkaywb#r4}n4P<-n09J)-Q40% zs58EPdc@A@bRA-3`WOG~1I8@&DXQt@$*s7CJoEdfOAbO^bO!8VmXB4+= z*|g4v5D_CPBKABOzGPEQbcS8D;EYPN)d@2nGo8Dc3P{GaXd6k-Kom^c{u z2x==2dL;ZrF`#!SQenQv3a;Tw+!dBjrDB=96Le74+)Pf8lgej6i0l#+?s2X``Qc8*@i~B6I22;nZc}_H)zxHy3N&TcOgR`@a$`rWam1UcwU4p` z!7Cz&RhD+PIKP*twNNpPVu$_NZHkg@d74Cxq@%XV*azWQa3P`YI?NY0?>2z?&l zMJN>iw6YLTiT)B>`GOi^G{Y0h5o?yubm(=^Z;4g7I~qiEQlsNw6)lxTbBIsilqY#9 zPnVRS)3Lwe6*XSfN1hNE6bBfQ9F!brt~GOUQoN#@raeFb`QaeH*v4=aI+f}ZQQZ_> zs-Q1XwxAEXqy(%vbjhU?=T;nC?LU80_f(V$ddUsoh?|~rjo08BX2JjEYob&oD?$Mh z#d}ydWVhC&O^D11dl+yh9DU6ix^=4cLzTRBpiygzD;_HrC z`C90Lk9;M26m`DDk_NXj|17|Y!-rdo@*=A%#i3Rl?*o=rhHdR_-ozSjA#7jIqKsi6 zQ+--weID0|GX4SA!`?`|!txxonQlU91(Lx!GV@lzxU&eWAxVYKaSOn@u$O_JIDoRs zi-Dw`67_Sa&_d4)KRvp2I(aQY`US!%C?wyl0No-I;3@O0DBcCoYb;&kJVK(hUghZ= zhaOM2co*gQGAL?J`AP(N%Tqlacsb@TLqUPg<;AT12(Hs*OV=XJgyck5uT);I*VdPK zF*fR$&Nb`R@|}LQQ{9Wlp!_;+)Fpzz9XVbS){AkXwl%nJy>2#0Qzc7nfqe@~kv6{_ zL1rsWM&Cj063*MysAfhkYF1lIc}6snns6yK-!u%jzQ8u@9u^p+yAr6} zJIszSFkM^x2d>5We-aF9i(9?gp72pWT2Cid*EEG8J9yU8`dA4Tv^g26&1n#w!9Vt*7B3!f=>N7>{< z;kw|ao}`JL#8b3JaJ=%Tp)&31$GtOeNl1|IM1CX8v3Z3;5+{zuG75TH8+MSrKh&fT<&sm532Ld{`Ivf z8Z`RM=f1iRwtF|Thk8^m6h6Vjv3=HhUiWRNf#Ep}6&4L#C*Hx8lV4$0yoxJKbolpl zn4T2ihv5ix7#fY|JJMl}#IQacRY%U_B?=6tWga*!zUfEnA8P1<&53Lkg?TJME+^yJ zifmOEi5`y8WeSD#u{Xe|58vc6BN4mxafc`0d-LU$L7h_>8e<=h0p~96$7m<}a3W&& zNsMUFF3bDsPWQ?W)lO4A=>6Oi_{O&vA$?yyY}zQlfaRqG=@TvuK!gL(#H>{?wIs@0 z+Cm$Ap*Y$KKJLT++0q486mjcjM?^dk?Q`J}x(~pewj3h4^<_FZ513=t+;!}LH$ZHn zHqjk;)oGCqW^6r3C7vc*RO-o#-d$OQUgxoP4ZsS2ynAQ64q|Z8!08ExJ@^Jv|J5`o z2H1np`iS7mW&k)uiF!`i%YWTSI7ktxqmLi_p7^h+Hq!QB|2rJ zt>Rb$?lCwWlkMz@fK9rY-1qxVIM`?;@plOs5cql+Q117&}D{B#= z)w!DFPXmS>I4DjbutW2YA5L%ZEMh+34TaJN-Hi{xvkRuP&0Z9b5h3}X3oJf}D4qup z?umEOw&TLRfK9V)l-v|lRDnRI{h^NHIacE=%EMTF-kL|JQMnaKEsDI_6H$#yqGP~Z zPj-1z!|m^at~ClTbH~jLs@^9`=x{cQ^`w6gzzTnCm;bLv=7_v?c^n?H1&@=V-scs; z_?G{kPo9njb@4=dNSpA}>V1mLx_I)!7ogu<6zAJtbp?H_;5x{8GulFo9Ay{XF|u`X z{ie=Xcx`YNKd7#z9$@Ue0O(x8t69%Zj-XwaS+ll7m4tA)k%As?kPDj^qE>>w2%y{s znyRjz52Mj*&1=F4z(O2Wp8{ml=ehWwyMv1fZKNraGYX6$&`Nx-`hooM0iPgoj-DJJAOTv7!$#)#oJsn8z)Pzq z6>)gIa>n76CB%-6JUOnXvdhRdiV}r3Zm&0}`UZ;Icu&u$(sPxHcfx!dp}alXt((i7 zajcZ$v&nHruAduWD`nPnBE?(pG^toFRG`jfbCg)=Mnj_yUuTSosQNr@h1BgliYZkd z^-^?@N1bX=^<#Mka0^`D)UuLltMIhT-Ec5l*;US2sluj<+tmj|%VE*RbX?su-|DK* zp~X_MM9^k`A_8qp5j3sR@NEswlJkL1J1qjedqEF#NAzzbdU|?wA98`%qLt)9FkPw5 zbGiVV=mMgf_?frhO6$_kg0mTr)MA_iD`bofbM8-7TZ5f z%WDDVkVT$kqsVkL(lD2TzJEB?5uADyz3l@vV9-BYrXC=c)5ChAKtiAHft|0Ihw@=G zp6Qt$LlqCpPlPek^8rZ5Hh-dLgR5qHIE+cbnD1JpM5W2)UuGDNn{y0o96%naUugkZ zv~gf`U~X*cu^X{yDzJ@}O3bo?(3lrq25ubY_BtDGzoHb|dzB{x+WJeje{U2^li3vL zzKyJI!O-%hX@jcwMphwf^>I4X(^xWsP@Au?q82+?|BCDLW9%d^)i55TwEi`Y;^juk z1xOUij>4af?|}q&IMyzlOJICh%NZ**eKzK?IPc4nn)l&)PGqdb8_%couK>t%QN^na z%$OJ}fQ=)Y#Y;E@R}YONhl(wWvmBbt;@T(Aom1yI8Yo`dFqdFWLT}IKpux6++!YAq z4=c{FNXYVMf)hSO&v}O#bp%S!&Rht2IgxWJOH{n0Xq<$;>@g$5!BE8;t;i4OP=^CS zYugJ9YS1;NK?>C4{=vy_SH<6W8((Z! zE^*o|Ja0Uc$9v)4J)9(H6-c$lj78|kD9-OJA8}uA(j6GHYXubQ2}hqt*5bj#@)25- z^HSrDm}>QfMBwUWFMg?^cpqAnT;CtT4@B^T5xmsE#sv)Z%K*MX?HF8R zXZO&qll5-=Lv2u!OQxwFWqiyJDvfAsh57$Dx{Mr$(P(&{}1 z2Q^yrT9EueH}eftn%+t)3r4PdGtrz#&!V}jL4sHhP;;xe4rsav1yq+)7f}@5d-2||*E!MYojy3gy-b2LBAkC4 zpP0=Kz=tX|WNIO+bn2hYc4CdeRO?Jh8n*#~*ji2?O8?#CpBh$QcVi-I{IrjH<2*26owLRbH6?;MGSgrLeY)F@Vv_Pgsd;Aj6Y8&4}@n%N;mw=^&0bg<8 zzeMoM5&VjQjqgFtmb(DIiSK$9$b>Ex(R1l9xC2Esry#e7f!H8);J+H=7N`G45EdJFa?46>Gcwh} znAuFMq^PWfyj`4i!&+To!~(7{WyX&iE95l*8ar6#+%p;8Blj! zsbS#F#YfPAGv{4?O$XnWaTmds15frS3h55|DKuz&9IzRgw7biBs9$7%wuJTS&;IAN+Mx!1xj#|A6ZSWq90X|7=^|i$*M}OTA~_$GH@Ez#FQ&Na$8#9 zeTLw4et!giX`ov~{mQ@rK8i^t^4f${1J6KlrWKh~$`r9HDiS8vodK197F3$7wNkpk ztZ7O&K8nBMMCzWmV$wY|8oc)B*1cDme^JPtPNn@03`tYJkKi97_{RwT$-u6Va}x^El+YDUfI2w2-;vzlIz=2422l{|`wc4;{Lw?k+KRQx2-_0Pp=5Rit%HB(w%mVa| zP8dUB$g>JMwWoGaf=BBBET*Nd9iQvbgyGa3!8qGNiXC27evGUH;c|BrJMb;9#p}4D zHgG8KR9=nI_>4v;%<3!#?gq|^_#J>cEL+FNZo9Lyf9fpVrYoQ27<2%4y#trPH_OMM zLYCbtf{!(D;2nopnXeAM!84fym+*lywdkid^z(jK&an%(*9vZCIY1K#yVss*$i(UP z23@iCID+7(xXn3Tb~Ea*z8LtdH^djC_L+BgL&*V7HRa9qp!h zJ9Sd)J#dQ^y`E{6~BD~feBJ@=;}1I{|rRpJzKWauI$hiDtYgi?%;*4*+Xcrf0{_& zn<=P3=M9i!;0Hiv$nd;C{veIF4{9s>8~7QD8lMBdt|8q;Br9~6nI8oZ-Q9DLgdCL@ zuhkP`Ce!bHyL1CnDxni8q0A=4TXA#%okjZ4D~>iyHM7q#IyrSAY9;Ai-Xon8Jc3)M zen9u)$usTF%0sCnf$+`ZczLLS1NT_bY|1yEYH;5?2&tTJ+HbhnCkHVF#|fC4T-j|2 zO-t}C9aJu%iR9>IlNr&U)^6^NW~HMNi1Y&lfAQ`R{CfM3Qw_yzljOI7P7AY=xseUb zMoGrgo|?MXda@I{t0&d7rVnBA=98B{L|zj-@~@NaBY4}pug0V|3`1TMWj&K)bN9J~ z4;lu10%wY$e;)SCV)tu-v9Mbx_qaF-(Y|IHCUN$Mm75d>mBmxSh!7whG7ik%%+U)W zcKIwGHYKjU!Dzoq6|ryRFf}$Q_3$IHsd<3?Bb)S(1Hh(61fNim8!`^e-r|*PE_Odk z6gq?~t3I)38$+@up9GfA!F4aEoU>eqnS1fcLAx^@&Rv*2$tD)N!dz+%qbhUN6 zMxUl&lCCzXini@jFBL+i2s5J)Q&ZR|lS$`6TZ`;3J*}%b2Od}+hjt~(;|ao9m6qrU zaMtF@R+LwVMF!K5dpIHb8VmiIQI6F&o8B5Xyvb1WsP4FJo(@c&Y}wNaAc{$a8-oxGc;0&@rCY>pA^mP5hKb49&!LaW&1l7NjRiA5ck5!!*{f97gox-nKwK%a`wax8@ zslAWpYcWXO{mIs!XH_bEb4`Nn-Q&rW#5^I%Gmo$^YpyWPnp`E9CxA<37TD2&FE*&T zf@7@)h|q7Irq$RogM9`86z)ow+l5<=xic+x=Q3u$xi&Si*1qS44fbQu0SC4=1HfZ~ zZ(KmAk%W*x+{BGLz89^0#S`(mwnvlDv}0q8ITAwYFpO?0B@~ik)_^2D6WP49g$l;} z5>JEeRiXHB|=Q?J18V>PMcSvdpMTF zkK`8>>H=LJEw{6@j;qW3fl2OJiaqe%yfU(fAko<~bXyE^?#b>a0Frdu06u8r?9#k4 zu%wQ}@dqW#lZecPj1DPv85CQeG-y^lYJ-k}p=jXdhj7if(AO{uniQ$PdE{9D6FYuU zVk`EoNfdC44aDXb7g*VA#E5Z5>YgJ3~tB8(~%Q7JPELQEohyN;RR z2|O6%@5Ib6L#&w@nvY@vC{G! zfQcD@NZECw6b{?mjp8<7g?q3cB6`c){Xj4pHQl^|18u^!_Uyjyn;eHhW5ng}Y4-C8Tpt#IN>*}Rtv^4KW!MIk7-$2=5^)i8b1*qEuv!_Lw0A)38 z1ILikqCpf{qnn3jtYJl4Zshp_XjH=VmjJMDmn- zm-Vaer7zG^K+?qvEUgp%Kx*x6g+2fn_kkUz3+Gmr2#79>7HJ*AwfJLM>J0<62CV4A zb(S2ECadKufau>Xy5_@-%hzFO9!@P^4^$<9Hvo)&);g3vz~pz0wX_Djeh*Fb+wDLcSaGb*^FVWv z{Z)5?#A9&T$3LFE!0L-jh)r)ooaT8-BMMu08@}x)^Tv0DtiN6g#3XSpC*0O^IivC; zOCH_O6eka$11J0VHc9IRXqMFsXyF%5&t+=QbCS9~GKK!k@~xwy!-h&n#4C{dE}R0T zmVroz4*DDr1LNeox-072CKork8Af$)?8k5{--M2gFfPXAo3uwzI;JNEWp!`DDBXg+ zb;;O0~7xkicFXbmI`T5D?#ij_q4xgZRiZA^v*-YLM-0N3OC zxmLJQe4fU7-Gz#MF0#+tnmESK@$fS1D#JEMwuiYEL}^MUMiLgdb_SsQ??k_x;3WVR z7ViSc-=QzxZBT1H_}5!JchfZ4Y0iX7+Q)!p6NaUVoWdQs08u@{QeR4aQ; z1r+pfKftltAgYUsiH)Wp9^&QWjf3%4pTRco+2}~@kMB78pxlov4VT3J!5;L zU2F*9yPCGiq8ksN*Ak1tiL;d+dJCCCNIRGRM}Ttqe=?}`I@&ot|K$3w^%mV}UJ7JoH3{skj+w&UY4%-H zg*%hJx0-T=euiQTZ9B%1!*%mvTpMEN*4XH~v;8keQRr6u5t84A5YXvZ2XN4c# z9RNvl!06L{V;Gq(xBI_Q``nRs(e<%`uGgFYvn-Tu?g4LbdgkE}akDhgM~B=^QhJ!+$d%?y$za z%@+7-@$P32TXu&pk2moIM)o47T)8i8_&$f9M_TCTo;~xx}z_GQ7K&CgNj31yiS9 z*5iV$v9DD%chg~RL9HOnd!H=OXLT4SAwZ1 zPIk(6R#RQ11PmedX5cR7oC4nA&H$Bw{7*=iH`|4O*4S}B0dNd3ko$sc%UILBEZ|7{ zprJzHJPKf_Z2ruy-2LoV(IP$YUPgN0WUK|k*Q~wuM@>lR=K8w#yW)Jpg(m0JWQnHH zE$L5T7#q?r^^}NFi77zqwtNk)!F3M>Z++aV^V8DytKRFkPU@!-62165K_4Dl)Ta=Gdb1NA;=`F(&#@S6yw_IKz^a0}nLYvp&4H8|^f_WqC6nA2<+Vd9Zpn(T-;inF`UiIWe8d97RBgmY?EggCIz6v= zd#7#`w6ihzx_wa4ib1M^E`>Z4$Gyug>>wJC0b>Z;`b&lorxw8?Xq&Kmpv;v_>pqYs zeMSITsk9VpaWA7`OE`0tP|wd2I}3*@<9W$a>yBV&|Va_ z6GAyE&pa3|ulANJmkgO}bCx_`3I+}GTGrQw*> zo&Q&S8(lYMa!P&hk}raHSsT5${;CRt#Ct_^(1R)_sh;=M4Rvrex`z7@TNd~?(=mYz z9*5Q$2F2eJL_tf?2+=0q92KnTCxY!0n>LPYT0gRG!={OKwRhAF4aw&eGl;vr@Rk|F z70B{(sCWN-sS=Q|aH=R_@-Pf80mbGUJdr;tGpX#s)jw172+ z)53lR4sL+xd^LLT94IS`tEJ{{1dUcpgOdQMSih@jT7%1JnVonE{m@*DX=d>CK_l=m z?twP%_iW$q+13u;kdi4*8RC z=|AgKJ;5%Z{;~1(c9@tyuXGF$Fc+-@0FQK;!=Fx22+*sb7pG5-MIGpLox&1arP&mG z3_hz_aGjxF>&a}|*9d5=zTmI)V^mDF6oKmWb76&)+5PL{WieqgOm7&Uw282@Wt@{I z5BeA~o>on`^ES!crE%>;9&3%9X(E{c!1>_SsHMEafMiiZ6#tn9I`KIVaSo^!5n+Lq zy6Hpz!E2aINS|S?d61;doKi>M$wer$Py_Yr0tuQSXmmIVM4zGn_8B$G?S5#U8jh{x z_C}I{jw$`%HMmaCI1=l#82ZM@T7~P+$00?ENLHk094S=AK{&j~)vj-3PmtFcM|S!u zDm5^iPm5(9#SjwO#q(zj7`y>A-5dhwIt1U~ldaHckZK7*6y#o=Xk4|_r28~^Ji^ci zuSX}i#o+bBrTv_VyVh(3e7@g0tGVc?8>-GpY+J%Veyg26g?eT|8K zZW&(n9CTZV9-jgj3$$SX3CzElvDUyuT>sKqrYgMHkMnxtN1?wN|ev zWpXr$4s}-&bA~wxE(ecfr>N2Xn0tsP>hY64ez4n1L_55 z9HL>6AN3skx`F&A+K8A?vubMrxz zIOD{D_+C-cLb1WMI}gIx0($$2Fo#a3vc0VpCX+>SV;Sxnmw-LZ#Ohy@GiDhH+fN$c zwD(7G07lor)O2)MJ-w|Bxe&Im{lu1Ehjg6{wMrcft=GbZ-0H=D(>3_hT8?Tfv~?cP z;y3*ztgURapRL+PV3*xsjI1SoaW&xWTkU?sf0HKusFl7bptU2~&)Y_{N%efaJhw2C z^fBQDcW%@DXw5dJ(fE0Sj2}*oEqdo%zCg!*v7x*4ei9g#kFSW}O8|1$pgI{K4;)l0 z0rEj)#bjeBmUR3T)YzhgMvcXAXroV}^O@kZY-zvHn)ytu{h~fC z?#=yrOK^13;JA(>@-{mXIH6X8X`Bx9V0opM0^bU3IYwXNR`LxOjDjr1WX zSB8##;4H5@1#l3a?G61}$XJiB_8B5k=mUKSwNJzl6DWA%IBHR1G5?;5=F^}B=HJwC zAXzuuSkR9o-(Wb})8P{uR`xd>M*A}j2h>dFF`&JsW+QGY)NMpzUgoyPDoEbMM;7d# z%kx;q^FG$!3R{L>i-B-69#Z}CEa;gIkWAQ^JniSs(cyow8^P5PJR^c<8rZ(TJZ2Pi z=?~~K`r>oTELk8_KvmWT#F>zHG_#-&1GD4N+iwl#A@}VaY<`-Rj4O#GbXYffgo1^+ zzW0GzO(h&teAZf^A}2wxS!ATaqbT|@(LwN}7xHw|PT@7}%nwbrivcXM8fQ^SQ38uE z)K^b8sKNV^_?SmaP;wcT4gb^d{I-}a4d4;n(|81ruwHHZ0*Op{o?W?_at%ODrEC*O zpArbKq8IqDbwDZkgXmUU?$g-qx1yzP@nj809Wgj$Lc{K{_*J06Jr4%tEEXrBKhNSq z1!WA}etXThS9N=xJRtdY8La@{XusbFs6AT=rWoC9zfrJ$4-d+ZHN@^^{(9784|#*w z#*4z3JIiu_8LTU^L~~k7p^|PBmlZMI@&e8LXlZq}L2kW-1m{3xQfKd%0epxF;2eN* zTv|nmn`?Al^R0a?=%@!2Z9D^Sf8GjyVhMg?G~nh6b$yg8Ne!A3fW@qk+&fS*L}azo ziad`Isl`xiNyuAe`!?Uw{%XC2+N+O_F=95XcA`^~KPX$@RYa!mn8sz9rmbiaJp`|} z!(Uuxi|&R_;Ae_N)m{+W@EiO%&fkac#t*{eEVZdg|oP zZ*qd*K1_fA;h1~2ANLcK0{3jcpW2u@`YFsk+fNw~0pBw{*6jyWXFr45yKAPxnCqSGwcby{61qR(Rke+!yC&`-ApjC^tv6|-GW9-)^eL})WOoF)^OS4j?q z9z<+5$R)>@qgK=26hI+t0jT@RX@DJmaH)dSZlR!YsUsRY85cNV?%rewX+!m1n)lT6Hjl5!+Uf!FP5OV6 z23R+`W!kpSXzZcY?hF!u#HogOdj`Ggp8p{qFCVZPvm|s2IwKp*=ljuGj;=#zfGGZP zNvXvg72DB6YEbjC1BwHN9qh}j+6}m2%Xu3&`q8=~N`sh7YDLRaKe7v`O1FSSzt%Dn zT7v$suqx^wa&DNmult8{QC;IMLs!%|DLn%gtLxarlTC3vMkU8nXu6I=lK~}J;|b3z z{u-k`= zYpaOIxsBbq5H%h{8W-g z*EO*oLBNolvo?E; z)XM7Ltr%KO5NlBfe#=0;5>kCTg6KQ+9^!rnAiodJ7e$6XXxDt**#6IkK4`PGxaLN@ z`^FgIp*6sOrzM|dr}dMUB!VDMy|CsEt!U}@z6s* zvUsg`qkl8JaEx@rmfo;97Bn%j)q}x~A*IpoO-%7LSz@+^oz7JtBPpvlPwe zR=_mx4^b(v*lpn8Uab8QYPS=-(?Ff)t9}g7&hqN}VneqM!vfW~fNiXB}i|`VV z2~)$&7;64}bWmV(Ft8SmnpQusiv|-Yk`3qR?kReCT+c|STpHL~#!aFz8F133|I6me z=Nyd%EquR$&INu6@NU-r3J7{(>NfzI%%F7o9-`jU?=v*rvXK3*={IJ5n+TSH zAZnJ6uB}TYX02)MI$}NO1x)S?Ixx5dgl6S;?eLgq>!9aG|9Pe=+=xXBc;e9btFHFc@WIZff};8Hk$pk zPaKUjBJ&C1n5>f(h{Ot3R%pdXJ~Uf`UgvPwSQz>)7(t8cZP1)KsOtdQs~d+55s^4^ zhCHInn)B^?=z3HJigWe~ICQWa9+7A?;V;gN?t!N#ltt-XX6iOTL{BtE<=+3> zh?-G=M7oF!`_V28%qg7n)X*KcrY45&Fo=~j3is8jo7s#&>uE-dJn#AQNyE)u^uD2Q zrB@A|bTBOClIVLw-vgEBqXmIo-4=p_m9cpaaH`v^n8TA=CC9wpt|KB_h!ZEbhYbV% z$y@uWO?Ik%Vrps}9x6w(eLnY18Qq&3x)R#{Zffts`#F4Xp-#@|Z&H ze)Sc1N=0G@$nm>V2{Sqx#ojy>mXH)*)YiV}Unj~=b)x9hJ`iG}qmzJQ+8Zs)7vsx` zRCx%D`qpiGKDxox+#DK0#$n1XH4{+4#bwTNEQ!xV2Zv2T@CNCfQ8Sr8d(nBQ)~E^gEZ^ wIN49oMQy6)jvQmHs~Xb9`Bd2>&O-Eu4k(d`pOhM?w;iD4C&ykm(HYPFFNcDaEC2ui diff --git a/src/builtin/obj/optional.olean b/src/builtin/obj/optional.olean new file mode 100644 index 0000000000000000000000000000000000000000..53b5f0d30941528eb6bc3c2f38874d758f8e0413 GIT binary patch literal 3710 zcmZ`+OK%)S5bl{-G)sbHARu|*K;*~T1SAM=1cHEM%RCeyR(KvJWA8Ygu%21ZjuSfv zUvr8g1mb|ioxp|PKoF-~5q|=Xh%5Dd)jd7lI3u}Sudc3FSNB$a*559yJB4Y5f5laz`<7YpfVp1u$_L9=aoZFpuzWinRt_a4v~mi4nW;ua{JaEjP$&{2U@jdU@B>lV$fEE&Qq=lJ_|e$xp=IR z8Kbr#(3(-jxheM7RAT_X#sDnlGBW8o*CvvSI^VJ_rRE5q;u4~#fxZS1ytgyPfAcU1 z78cY@S(Vc@^`#74DT657%0`piy3O#BP**Z>!sRCLxmlqPOV~#YNGqo_k~Vd5wa8=* zcY26&fK{{`keT*G73FreQ8e~gL1yGsc&_-)4)1s+EsaI+;Yj;C=Ux%^lygi!)XP}r zF26Xm9x}YX+Qd@pV|x_d5KiYP6y=qCvys+p4vtB<_`IYxI81=f0_-v*nOW9jW_se! zIU9z7YN6hSrY7qgFl}18E|YUjCX}vy(9W8Q_E|KVvW3Oc3V^42!B;ZT!h1O#>P||C z)D$p^Z=94#o!0qyB9j>0**;(ofT~((TAA~)aVqk3%=ul8l_zI92SE>h;%_(gRLkVH_8P~GQ z-WboQ2HNhdSKgbTxp>ZX>082yf=*)%<-#t?&E}Y{;uZtO#N=Lvxoy&HDGg6Y4<>`u zi>wb62mBB~CiVGF@IQff8{n6FDhn<JXNIm`6WWMS4EodySp30#QAGq9n1+UcN608NV9Tun=PZ+ zf%p#>#m7Q)8pICSdnRp$MfPoV0F-guCj1<1qYAs#}~$*^{d z^X)ST{R6@IcJ!WO?fZ%iK2dgvZ+JS5*+gD&4v?sp5mfGi1J}P#|vn_qRzuf3g z=p_K`5NY;nAn?>&yVhxY4UtQJh8&fYn|H4sb|=G~sUpRGffh}N4m!=YYI{3=DV$Dj z*nIb^n(M&3z69bAY@+%$9xVk(E!rkft*ZDeo3Yk8(7QOvXWe`TXZq^-2h2lccsxn7 zeNe~&;BQ1}>{FuNsXL&5pUMf7&F=jV;+SI2I_CIrz(6qRBt^9KH&K9p0l1Y~agDVh z>>&7PoawzX!*@l8X6JNh_w+c*n%2?*Kpp=}Sn`^f3g#rx=VT4tpjuHrZ6|4nv}qW}N^ literal 0 HcmV?d00001 diff --git a/src/builtin/obj/subtype.olean b/src/builtin/obj/subtype.olean new file mode 100644 index 0000000000000000000000000000000000000000..c4ee00afdfb7cd8801512ebe998f6f5c2339533a GIT binary patch literal 3049 zcma)8O>-MX5S^Koy_*jS!U0+4g5s}0DnL}J00{*NRY~MPIk}{ga8a$wE38D8#A;*g z8~h3G;0rlJLUGH#$lsyg>)oA=k*cy)Uca8{>5tbvy_$@Ycsv-65|cl6xIdkwnR%L| z<78xVX(!IiZZa@#_N<>BO%oHjo947N?t!5D@)sKi1A+T?G8q}!g2*K!TK!38LhM_- z6b3-SDR)RUyH;*kII5MN(qu|+*rzl658!c~CLrb})hQjF_N!+A1FoJ0tS>VPyS+b! zXimwWv+5Oc6!&M@T$d@fO&GbZSqt27ychR}S+Z-)I@W2tK@F9WK0|EKIkz5vOdGEjUd*gfWLB3I$t>G5HEc$C z@p?XTl#vgrh)0O+3b8IZ9L};liZGNS;bD{!&>8sy zd_c&0lM+j|E;1EQRHtxyC2(2#EbmX@;^*9y>niFwQ*!cn?V zpRAaYS5Wr8XjCb?-&@>&uvVw}a0B=}UfKXamY%q;PMN22ME&|Q)J)lkIA8TGo+Y0r zb6YXy(R$?i1WlBUMn8ny^6{`58q~Z+>knPSN!4WJTaY#K3qTtAM}T!Id<@tmya;&j zLg1$HFij3Kh}FKVu(BDry=gj`40^*fl?h|WP)jdmqbh{TPecEOMTs`Wa?Q$9_H}aD zdz(9pkfM{#)>4nyD=*pr(mE6S6i`X{3`j}1%tb1603%6CZ%omESf!aCmjJ11fmWqm z(_|od<6(8m%s!Eopqd!6TG)UxgkS<4YormhBbvURgUx_jc&Q^+VF#kd!}sTqb>Ryj z&G1XW11hjDnrGbXvZ-{-+!o`Q*paJ$Lq=FH)~TUWtQ;b%K0;o-HOjm@l$8>=*Gnq5 zIS*e91Ec;$ZxM42__M!ayV7t)-&~dDlhX97IlMexu;GQ;Gg$;PZkZgBlFs zH?&K515nw%33w0|&O+DK{^)FB;}^WHXHGo+LMF@XXg~je(!xKm)z-U!BIbrYfjr%i(B*qCzhw9W zM=$tuQco)u2Vdg#H=2rFau%W{;Yp5sf4$$-2o|G zKxL2K5n;(%^X9By^hGY4G=>p#MMpiL)LF~ilIa_dcTMG6dCliT;#fMe<7Y_1o_YjR zO5|f8ZLc2ybK#Dm7s_BbWUG|W@S#(CF9sGCfGw!kSlv{ a8k-uFBQQ}BIn5}Szn<-_@$PN>y#EiS9s1Y+ literal 0 HcmV?d00001 diff --git a/src/builtin/optional.lean b/src/builtin/optional.lean new file mode 100644 index 000000000..b804888d2 --- /dev/null +++ b/src/builtin/optional.lean @@ -0,0 +1,69 @@ +import subtype +import macros +using subtype +-- We are encoding the (optional A) as a subset of A → Bool where +-- none is the predicate that is false everywhere +-- some(a) is the predicate that is true only at a +definition optional_pred (A : (Type U)) := (λ p : A → Bool, (∀ x, ¬ p x) ∨ exists_unique p) +definition optional (A : (Type U)) := subtype (A → Bool) (optional_pred A) + +namespace optional +theorem some_pred {A : (Type U)} (a : A) : optional_pred A (λ x, x = a) +:= or_intror + (∀ x, ¬ x = a) + (exists_intro a + (and_intro (refl a) (take y, assume H : y ≠ a, H))) + +theorem none_pred (A : (Type U)) : optional_pred A (λ x, false) +:= or_introl (take x, not_false_trivial) (exists_unique (λ x, false)) + +theorem optional_inhabited (A : (Type U)) : inhabited (optional A) +:= subtype_inhabited (exists_intro (λ x, false) (none_pred A)) + +definition none {A : (Type U)} : optional A +:= abst (λ x, false) (optional_inhabited A) + +definition some {A : (Type U)} (a : A) : optional A +:= abst (λ x, x = a) (optional_inhabited A) + +definition is_some {A : (Type U)} (n : optional A) := ∃ x : A, some x = n + +theorem injectivity {A : (Type U)} {a a' : A} : some a = some a' → a = a' +:= assume Heq, + let eq_reps : (λ x, x = a) = (λ x, x = a') := abst_inj (optional_inhabited A) (some_pred a) (some_pred a') Heq + in (congr1 a eq_reps) ◂ (refl a) + +theorem distinct {A : (Type U)} (a : A) : some a ≠ none +:= assume N : some a = none, + let eq_reps : (λ x, x = a) = (λ x, false) := abst_inj (optional_inhabited A) (some_pred a) (none_pred A) N + in (congr1 a eq_reps) ◂ (refl a) + +definition value {A : (Type U)} (n : optional A) (H : is_some n) : A +:= ε (inhabited_ex_intro H) (λ x, some x = n) + +theorem is_some_some {A : (Type U)} (a : A) : is_some (some a) +:= exists_intro a (refl (some a)) + +theorem not_is_some_none {A : (Type U)} : ¬ is_some (@none A) +:= assume N : is_some (@none A), + obtain (w : A) (Hw : some w = @none A), from N, + absurd Hw (distinct w) + +theorem value_some {A : (Type U)} (a : A) (H : is_some (some a)) : value (some a) H = a +:= let eq1 : some (value (some a) H) = some a := eps_ax (inhabited_ex_intro H) a (refl (some a)) + in injectivity eq1 + +-- TODO +-- theorem dichotomy {A : (Type U)} (n : optional A) : n = none ∨ ∃ a, n = some a +-- theorem induction {A : (Type U)} {P : optional A → Bool} (H1 : P none) (H2 : ∀ x, P (some x)) : ∀ o, P o + +set_opaque some true +set_opaque none true +set_opaque is_some true +set_opaque value true +end +set_opaque optional true +set_opaque optional_pred true +definition optional_inhabited := optional::optional_inhabited +add_rewrite optional::is_some_some optional::not_is_some_none optional::distinct optional::value_some + diff --git a/src/builtin/subtype.lean b/src/builtin/subtype.lean index 503241a6b..caa550730 100644 --- a/src/builtin/subtype.lean +++ b/src/builtin/subtype.lean @@ -1,6 +1,4 @@ -import heq import macros - -- Simulate "subtypes" using Sigma types and proof irrelevance definition subtype (A : (Type U)) (P : A → Bool) := sig x, P x @@ -30,23 +28,16 @@ theorem abst_rep {A : (Type U)} {P : A → Bool} (H : inhabited (subtype A P)) ( @eps_ax (subtype A P) H (λ x, rep x = rep a) a (refl (rep a)) in rep_inj s1 -theorem rep_abst {A : (Type U)} {P : A → Bool} (H : inhabited (subtype A P)) : ∀ r, P r ↔ rep (abst r H) = r -:= take r, iff_intro - (assume Hl : P r, - @eps_ax (subtype A P) H (λ x, rep x = r) (tuple (subtype A P) : r, Hl) (refl r)) - (assume Hr : rep (abst r H) = r, - let s1 : P (rep (abst r H)) := P_rep (abst r H) - in subst s1 Hr) +theorem rep_abst {A : (Type U)} {P : A → Bool} (H : inhabited (subtype A P)) : ∀ r, P r → rep (abst r H) = r +:= take r, assume Hl : P r, + @eps_ax (subtype A P) H (λ x, rep x = r) (tuple (subtype A P) : r, Hl) (refl r) -theorem abst_abst {A : (Type U)} {P : A → Bool} (H : inhabited (subtype A P)) {r r' : A} : - P r → P r' → (abst r H = abst r' H ↔ r = r') -:= assume Hr Hr', iff_intro - (assume Heq : abst r H = abst r' H, - calc r = rep (abst r H) : symm ((rep_abst H r) ◂ Hr) - ... = rep (abst r' H) : { Heq } - ... = r' : (rep_abst H r') ◂ Hr') - (assume Heq : r = r', - calc abst r H = abst r' H : { Heq }) +theorem abst_inj {A : (Type U)} {P : A → Bool} (H : inhabited (subtype A P)) {r r' : A} : + P r → P r' → abst r H = abst r' H → r = r' +:= assume Hr Hr' Heq, + calc r = rep (abst r H) : symm (rep_abst H r Hr) + ... = rep (abst r' H) : { Heq } + ... = r' : rep_abst H r' Hr' theorem ex_rep {A : (Type U)} {P : A → Bool} (H : inhabited (subtype A P)) : ∀ a, ∃ r, abst r H = a ∧ P r diff --git a/src/kernel/kernel_decls.cpp b/src/kernel/kernel_decls.cpp index 2234e6d63..6aeb89e18 100644 --- a/src/kernel/kernel_decls.cpp +++ b/src/kernel/kernel_decls.cpp @@ -27,6 +27,7 @@ MK_CONSTANT(em_fn, name("em")); MK_CONSTANT(not_intro_fn, name("not_intro")); MK_CONSTANT(absurd_fn, name("absurd")); MK_CONSTANT(exists_fn, name("exists")); +MK_CONSTANT(exists_unique_fn, name("exists_unique")); MK_CONSTANT(case_fn, name("case")); MK_CONSTANT(false_elim_fn, name("false_elim")); MK_CONSTANT(mt_fn, name("mt")); diff --git a/src/kernel/kernel_decls.h b/src/kernel/kernel_decls.h index b3029d55b..34768f45a 100644 --- a/src/kernel/kernel_decls.h +++ b/src/kernel/kernel_decls.h @@ -72,6 +72,10 @@ expr mk_exists_fn(); bool is_exists_fn(expr const & e); inline bool is_exists(expr const & e) { return is_app(e) && is_exists_fn(arg(e, 0)) && num_args(e) == 3; } inline expr mk_exists(expr const & e1, expr const & e2) { return mk_app({mk_exists_fn(), e1, e2}); } +expr mk_exists_unique_fn(); +bool is_exists_unique_fn(expr const & e); +inline bool is_exists_unique(expr const & e) { return is_app(e) && is_exists_unique_fn(arg(e, 0)) && num_args(e) == 3; } +inline expr mk_exists_unique(expr const & e1, expr const & e2) { return mk_app({mk_exists_unique_fn(), e1, e2}); } expr mk_case_fn(); bool is_case_fn(expr const & e); inline expr mk_case_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_case_fn(), e1, e2, e3, e4}); }