From ddaf948c72d4728098e78a391bc785a5c71160f4 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 30 Jan 2014 19:38:51 -0800 Subject: [PATCH] feat(builtin/kernel): add nonempty_fun theorem Signed-off-by: Leonardo de Moura --- src/builtin/kernel.lean | 4 ++++ src/builtin/obj/kernel.olean | Bin 37764 -> 37933 bytes src/kernel/kernel_decls.cpp | 1 + src/kernel/kernel_decls.h | 3 +++ 4 files changed, 8 insertions(+) diff --git a/src/builtin/kernel.lean b/src/builtin/kernel.lean index f62506aaf..12fac3cfc 100644 --- a/src/builtin/kernel.lean +++ b/src/builtin/kernel.lean @@ -85,6 +85,10 @@ theorem eps_singleton {A : TypeU} (H : nonempty A) (a : A) : ε H (λ x, x = a) Ha : P a := refl a in eps_ax H a Ha +-- A function space (∀ x : A, B x) is nonempty if forall a : A, we have nonempty (B a) +theorem nonempty_fun {A : TypeU} {B : A → TypeU} (Hn : ∀ a, nonempty (B a)) : nonempty (∀ x, B x) +:= nonempty_intro (λ x, ε (Hn x) (λ y, true)) + -- if-then-else expression definition ite {A : TypeU} (c : Bool) (a b : A) : A := ε (nonempty_intro a) (λ r, (c → r = a) ∧ (¬ c → r = b)) diff --git a/src/builtin/obj/kernel.olean b/src/builtin/obj/kernel.olean index dd58cad8503851cf575cd6b3f773ab7cb1476e5e..001db09eaf01a750dffd7249b94cc7a1b28bddb8 100644 GIT binary patch literal 37933 zcmb__37DQmmF~CvTgSwaXB<#O!Wa?=rUfEPSR@e8NrM|07Zhnaoxh>A(;YgUkT^Pk zm=+Zf#oZukh~R>bjte3f1vgL-+(2;ybrcC+Wv-*+cJF!Lx3=%=KMUU5&(qcCt2%Y+ z)Y9EGR_80%jgC!?j%WGQC|H0m;oHACIZ=aqt;xM87?&{qDc`nxu_xr_6(UB2$=pla%fL4yJ0je`Rw*NRz=J6!?q?!iq zpMHy4L1Q5$(A_Y)c4{q!fXXMdiswc#poT+91P2m>6$=3#qss ztJh3zjAH;<6#D@_VgIslY~ax(>j=_K%c*m+V%*Uf937vUoQRZy!enua*nc)TJQT3> zMTHyH<<_ynDo{%D%b{j_WgTMmd5(d*tAjL}`vZLs6m3nMAO|}FpgGF&arwqFHVtja zis2y(9S|yhTCHOFp>k!-&7K$QnF4G0`84Ojgi7>jgUV!gWUR-m=L2DH6p}ZfU~x~g zhdf8`wd+={Mc6t4?NG6pj8>j1oyKh;r^4u5GOFRgSp$RyP|T$$*lECv?|7?kH;AHNm9h5U(AuoH<5QX3;B;G_j2lSbNDkWHME96+ zmQ4kE-Wp8BGK+p`l(XXmC_5?JkBhmMc}4}VnVgsy862IQ?7~DvL-vD#pfUQNOmsg_ zp=)h&FtO+fZH5s>6;I@eTYdtioK2KFyO_7D_u272LKGH@;`6@DfG9>iKMXEqfnq5pug zINoUpI3n^!K(bOmfoq7Uh)k~?9Y1@lJ7vj5!h2Az<9$9TFhIy!sZY`NK{hdC>R6Ew z{j|cdizc!WwNsqPD*(>!IGtoyc8cXgT+6cKBo#y-FO>r*C)iAuMa4*1s0&j(&mJ_x z5b!O0q!VOd&0cCog=#lT8Z6yJIwE)$`8*%=#r*{UU&`7G0ba*=ei^{Cs>0xu$!>qM z;H2f;r8nMxvp%K@`{Q#Zm%19&BeF6mvMyHv!b_-VBgULD`pEjWg$|p;UxH$0O*JojD&RjX3HF zRZJdaq;J8qMEX{MQuEsYo+;}SbJPMQbO+i(rZJZ?-GVyl-D~;^t1(Tle)-_!q=i`1 z_|UqsDav4Ka&-OZ&=~q;W$e$HGie!Gxpv*;s$izQV&WWhZm`Q{fD+b~05!4q03_CN zo~3tNjg#BCmRx!}F!HjrIL?9)dpU0fruTxP#(7@^-w$vB8KD&B9*BxfC|F4ooa^0$ zRSXo07M``M4BezvOG#hJu)K=qb5%Vfefz7`ijf|KX|1#k+3E*wLot!;J{0=3iH2V<-358J&dA_vANM3?2e5lS)aG-2C(Fx9|kB9egt4+ z0m|Q^_yr0P1T-5|M^~>IoSGaO$KoEGCFp7xct{r9s&-#cnn6NW%;c0mN@Ri`i{QUU z@Z$jQBf=*HA~NGgi4cuHq#xH=yH+H0#u;Qv$B=J_|?ACaVU+U}ppO4-hNIa^HE#j3+kN;b z@Kvi(fLg7?5}@=5PkRMRC&g{l#Mg;T@EZ}l9pGN9W#FC@q#lOE(4qg#`aL zdvICP@Put1ht^Cm3Cj=lDP}z1@Ojx@28_!==O}uBiX$HlJgD~0IEG^Wj1UsM-8s3X z1%Bg4Ws|7l^Y<{4#D8}L?*SB@-y`6(!squdWr^ZHo? ze{NuYim@!o%ofL}Jk=@_w#iB`w)+gju`=0RJ2AGtduY#?Z&pBe-vc9RHlTexCH*T@ zilYZ2_-i0^ZE&hNUy7D~?{UAh2RE)A-_6X-qJ9rWKV+qTQ${}aL?zWA8+-`QV&OLt z{9gcNgIw#lkMV01dv6PJO7=s~^IUGX?g^JzW_MtPk`B2F(#gcy|Bn3pK7#*kV7^hI z0QO*Zh=Oq?IKqEfO>O+083_}AP4|x=CVBi%1pj1Uz7YbppbQ<>zviIdS<@E0J7mA?X1?cY@Ea)^8>LUw){DybI=QAE5l{tOI81Y0@G3^zk@?*}$ zB~?kyw4&E9nbwkvY4jg(C@~^#rIL=awtOovR`|%G$CFV<*6W2+VGf3UMqvkp>(YD~ zit|ER21*SSwC4OV03{Cup!_pDJs~+mL8El075;EkSWmA{Ib?X8Ls^{!9O}o%r2HSO zMw(u`aW(Sk6M)nE^id+-Z$1$AMv+)8)xuD~{awyAiB_LK4yc;b;{on>Aj(ZBNI(Vy z0@>B9i~}%1qhPh2-okbi6*tNM$!ffeySClhLBNoy$Nd(CBtv`xh)UY~MDU3Kx!=n7 z1(+m|WI$^mhqvCqNM?jbAJuZm%S9Ex$=HdcTM&tglOcL%fYf-9 z%UriRxI0Ei(kx^t7`h!R>qdA0+GT`fTGL#JT21pHgYt*GYvi|Z+SF|R9biRal5|iZ z0zovg!SQa`gzcs#G48!lbDTmPOqye5U32|lOH+CZKuzgjfSS@F0HrzDcrMK$2g(1` zOLHrl=#Xd*!%B1VHZ->}VTmL%Bx!qfE;5W%oyo>@H)X>4vLIz?m@>lP$YJw8gW3Er zE1V1%>m-9CP%9Z62~aXvVo;%42JYRn-Y5f3w}?eFy}YF6YMq)UZndKBV0L za=^x!&yDNhtifg!!RVi64;t9^WoJ(!Q4X5riiM?O1YI)QD4tCqoQT-@=5iOM{3=I# zuNyrV6Rpv*FGV5{lNdRY9N0MY7}-^lzz&K_Li8!AjvGsU*{3V#Sf1IQf^n zo{v!kz5t-C=Y;@eJud<%>p2}DBW3<#gNhfB*h>JuFa*_nYa9~XXh??Ee5)8Mthx;> z@l0;oO6Iu3<;w`Q#TdvrI4n9`g2gtH(foaoc%F^X!V6s&DR^hV2aDjfun4{^r3TaV z{V+6$B!%sLmTrtTCcDmQ>@j~SDkaS`0rKrxJ_u03=PZK?zKY6W{Kb04Ats%O)dlxH z@uWcxBFmc<<*HEMH3Hf60xNO^_2N}{MmCPW#j9wZ%R=fcAFEY&yJH=DcR1;bhoHzL*uFidwSo zcjGxCs>>V0%Qm;_1dX~aoV_fLDn$g+9HdZErU6d?6w_+}N*D&A!;J$2hd z283q$MaH~?{FbP6fvGqT4~9}K7lg(l>@&vg39q7c#;L0&cKQ?!LBeE$2A1o1fikxx zO96_5C9e+^5e1uLMyHwotZNJ{ce-#bvs|mZqDN8LFGp zAa{*aiVF=&qUelK8e!RnB%Jn~FsCL4Yxf6|2?P6sGzTSvoY!2QSL70ERHh7^8a*G} zYWf!d)buYjs4{&#e-y<{R#*->b9RtbwiU$+m}YSUK@`zE3CYEL-1#@)D&`Dr7@b%> zXcrBJ&zTq5a2pX`5AY5|nd0MCWUB$)<;_oTXsH%DuOxIbddd(G zA&U#}h$$6!$BwX$9FkHPE$#*s+~YO&;A0bBt?7b`gi|?_w}W5&;81=goAW#8qk<_E z`H-qOnKz?FPJKlL-vUqz-&+mJ@5Ex3-_VOp{jD8oHw?Y_nT{Qu)g;XA@{pOVhy;i!S9?D|@v|j@R~uM97Mep{Hg^Ha2T^D$fU3;A z&uVJS?BD3fekjNor}mXCruHlt(F!W0ER0vtub>i{YWa&5Rx%tAjF2V3}) ztdM8XTbP;^cd-pc!-S2$7B}IO`D^enW2O$NTo_{F0fwced6j2;m1lgKv!bnw@im=pje!U$B<`z*dBZU#?IbnhQVDpLwD{J zgDnlIq%GV4dNP2|0p#&X`DlO+t8zB`uyMQ?jTvMX-h}3#wFj5K+fIK6Y%H6PJ~cKP zWMdmz#Kso@E`vN0HlVCS(O@q^tkC<&XdnndVygk6k*$p=MPZ_@Z>>9 zB}dp{hoaT8(0JbfF}^G+ zMrohmz2mr}Rf zUx-kh!nn`5@)#Ux( zNQ$Icpezm%tXxYI_zuAH2qLnS=Z7HWlTX`e zIzA3G1g^~7vzHfYm^hfEY)E`BR9>_z{6sJq`qBkf^4L}M--yZ!X);iY+n@t#gL1aX zeua6NLFFZw1d~yJ{$P*AFxZpah?_=dHK7*`Q7;i;`^oql;`qt*d_?%BA-l!PUQ;^j zlF7y7l@w@Q;4tq}V0#$ohGp&jcvkfK89@kx(JSu)+G61e^?4U_&u;)61cf;FD)`Sth=%UpCYD>`AYs-ym&P~fR6;_UHn*CR&@@}DC~vlAWl!94 zQNHEPXl57?I;qiSp|N4KYEct9`2%c z0<^MxbCqT`w@#C62eU|L^`R(kPFCH)PvMt%9SI4hcdEI=a15kh{GLsnKKoe+3RDA2k5BWr(+=eV-evN6BNRr0YA&+E1I#4Y+n9n+a)y;?TYt9G)Q5*lR*zm6Ma z3E|@M*$x(IIe|@GH>NV)=#V>8a(h86lIPq0`lkz2uxuAv-St8w-R zbW0_x>sbF)uXcnQ`(lK~lVYd&c!s$+vVeFUpn;aO($94VQ8CVq6J+!$_5qC;eHw@0 z*+<33Asjr8Lqqbd+VP21HmH>ZJS&f6#ov?4AeUT`M6OzyZ)_U(dM<6^~yhBD1pgQkX$ox~G6Q5)(6O2>!Fw5K2Um_Wj{hG&45)&=U&v`f(B-KEST2(b5XCajVDBIS6lA+DfqNFfUX1Z2K@Y}eF2a7!N-rYm=aMw6xE!&f@qX_tTBa)s zjOyxHJyy++5&_LXce9>RZ+v^fq~8J(JW$aCEbm2-8K`q|t1M1Olf3Q41hKG`PXV}B z3njv0j%|gVcq*o3d*Lx2ZsbcNB89_`+ACYeK2+IpvN5EuZUaf&JxD*#p-mc_C{1(+ zUgO$G2Mp#{qn3CimfRH6btER%+lcxdpu(;ip8~}89D&50ctCvk$Oqh2@ATPtEHD}< zxF`aHI&diS(85uOL&pe+z@4RVmpWLs1V2e|kQ7iUmRD)SB1A}+>#Jq8{@uZua#mm4S4=szA0~FU|0C`Ma ztTw1|Gt`ki80KBjwC-hs?LIRQk~9}&2K2or#i(`k$LP?61@Ae4M;uT#c zz=bS+4MDOMgJVrQjeS``DqMBvczoFnr50QXY(fCYNDQuhT^>C$#T4I!Te5Te&Z}+?^_H0xs zNr81rzzGh9w^%#ZVDs^TzBH(a_d1Y~lwKdfH=y$IsRl#msI}%|Df89n7pudC-r{1b zPL=7t<7!6=HEjEIC1}yrxX+QRU5ZLE$#igMuI8z0U5@1VysMaaMZ~8zsr}v49$1V% zrxm&09XL^C62~somP&*v#2k7X^HxdZt)MFKZ3gA1q-sOkeP~}HU0s5TUb@1?rbJh~ ze%-_M+(phZx}1zjT)hLt#mYM)_$~v>$08Tg#db_UCxyz1@W>3szl|>5ZZ(b>ci(T4 zUrluaP?4!{$-vk8aAovs852hP-> zdCmd$s2djchD3zx8GyeAh*v0Bo}7?DWRj0Ko0*Y}t&@}*+8C?rda`_;@C>P(s$)$J~ z_-t}|nh?+}`*yRy6B1`Pe|yUPR~Zx^z!NV&Ad~BLi#Ye+*<{~MbSg;IzK@E+TZsBW z6uMcg;|H2RRZ}M?vaYCbkhbtqkjM#s3?Q$57XJ=#AJ%@{pyumk!!1-Fgo3k1JI%St zsCg;#2C)FU$-a$(SK;|OId*dRXbzTtojs%pq*Q8-DASKZ(eybMedo+LLDPV2lo9kP zR8M6t9+L4?74C^CQ86Xf##KQ=F#n=V5Hz1F{b8^ zcWzF>pEsy^CD=>S{p>8%ep2z0Td`j867N`&cqtR!wVn#P)WOur7mbAD>1Kd+ootJf zI0WqnbD~jBY?lZR_9AnxvO6WMaqG;imK*w+-Yl$v|9dC&R4Wx+Vf z5Xt3*w~C8f(X9A(8$iwO>j0GpeZ!#U?QmEZ=4Ujb6p8KtM+mcs*=eU;NyJ36>us@o7}V3%Me| z8FN@R%P#{1`BvwW?&eP%o}Y@*yGVX)#Ia)|k9Q?iiZ&9B*9n^2jgRJkF0hhI7P~ed z1b4hM+ISMXqNwqxy)@?>7PGH`j9VDAD#%h62iLOIzn7&*>=-pMk{A!z9Os*^qv(Sr zq{%Bk#dq*5OZhH9S<3eS%2Mt&sKt{eD!=Hr=jJ^vAYd-Vn*lXYVDYD|6#YRw$udr5 z0cSCgoA*THvp4Swox1ap@J$U+WL$fOH7v^~gNi=y#uZ^0&z=t%FW%@AYRw7^NhzeO zgZFtgebInSn1z$6A&TBQpnDe8RGiX*qH zqOq_jkN~v~M{iAnp~zk7aM+A0#jxLz!Fp761el7~KUzyt6ux+C9aTrM9%?zd-ja@{ zw{|5^vP~!;37I%=OejBTrZY2y;dh>jF$)MqN;C( z(kI4>;RV(hGo9Aa_NcGiZJh*gy2=-swV;fqt5MA0>tU;O+>@{P9IqFOFTRG3L%UAa zy|t`5s9LzM*ukK`^MkfcesJ+HV)(*oE04BV((=e3T)=Y5~B-`Vh5O0U?`H!=nLUxov4L^%o%N zl;f`v{96S7PXJ-TS?e{BMu`y9Vg!)wxXX;8d~ zdul=c)LMsPISSl!9<+B__~|LC%dMfOxhc?JjtSSqo2&!ZSZnKyst_5($xI7EYpty6 zF`2;DYDcx~B(T02dWnz%V+ZMk4Vkpw+c5LcxuG z$t08kqnty0#)C&k@E;=h7<9V`Vz$@?xc@*Ha`AIKD7Z3T z`Y;Q7zw^iwStHO|9VkP&VXIR9qdm-!$Rl1$-2Xga9KOgc9!9t| zjpFMR$vy@;kvuVi`$lkX1otzr^&@tB62NJx8#b7=E=9@E!7U5B;dX;_!F(y?w+k8g z&qkL|Fx(l_|GTXE8)SDrn3Ia(k`6o|f^n137p$0W_QQmwHkiYO^< ze6$4S&!z0S6_f0V7p(Sh>p4@Hf0xVsl|o~ZA)ze;TLMpv;7JjDx`7p!(?U}6m}o}} ziLxTbnJ|mvjZm0{JCe8cWR?9VoypOa_C1U^9U*6UGsh$YE8;h4V%a|P!IF~haO%82 z>h?gvp>$%$XG_O*@}&mOnnLA?TzNA3Xx66y+-HFmJQ->qMGbSQc`i3lYLs)TJnA)edm{Bf9Yx@KUn=Gj#r{%v&zr@g$7ljoq z!pEh>;t^|+@lhWkg%;azSe=%ZF9KLlkJySj<-Hi-K8ScR8EgZ!O$R@{R|^6{o44MZ z$P@KFG}`?`uk9CNkmPxZmoXXBr)|V2UuIDp&H!mOytyGXJhzW_o6z!w_EeD@7NBVU zL2hRK&gktW#y2kpH`zWk^@ZNfBqJ_2GzeKfpU*Pv_R$p7ndm8lCl-%F%d=3M82lJb zMc*ob)FwMCEDG5;p0QZqZ+i>|sSi}FMuoYCvp(2M1BJemN<39tNi>=;Ug!e9ZEvd` zkw{%=d?wLVK%`Mg!fYYIdW)Aeb{>`E|EjEa9%>|OmWP2yOBcmrB6gUHdqqI8>l{t! zXu5+MI0v9KFbYs1=VbsB4Y)<6g=%UbzBX-MhRUFUX{1H<8w6yOOfbTw-=jooyq=oP zit|Yh?Lxp(wp@8VbsmOpUmn$>w+NhLvK^WR+HkZ0kW|>g+Hc}GR6R5x@yz5p8wA&GXljB6>)w`GlNPRFKzu78s}@7mskGk# zB&s_sWk`Z{VqGx=_FBj|qvV1?FY8JIAr#wwEqLH-qjCzMOlloKnbdlK^+5Out7{{E zwEyEkE0Yk(7V6|;y~?=G+BM7e#|>z2s+hb!!y%>=^dNy5K~HE5daw14xYp1rqN*$w zyA$)G1=J+PghUGN$Ot#D*U|?VB&mVX`up4H}61knK#9+B&O)4 zp_i~6STRbSX^*qe`w}bKS6ESf(<@iH9a_k5AT~^mqZW%&8ga5U4|CtBcNi$d*RS@Z zFWy6*e%_&=*}e<*Tk5mS4juJZ+b{RE%?B137~iqB??JN++<^A?K#F-lv52Iu2~5R( zar^sKB5A_s1^87>*Jx5K&C3EE=D}@BsPz~O(Z;WR*_eB=dRf9CTHcJ}*H%Pb z$6-&d%BQ^@cpBgu^tj6kH;Q+ajaF50l~FsWeq{MUlyLMFzo~(z6t;66vcI;-+ppQW zl_i%L`N! z13|Vi8f~-#pfk%myEZt9&=W+0j(cztd0B8_=ZOind77wpp1(ea8KhGz0l3rx-h< zW{91|fdmB?{`p%OC$s_-IRX2I8_oOJUajQzaFW@AF5(`~#lsPwwRq>yIXq6ZiRa^L zNZ8VMP`LLaqX0Q?-6!AMKX;Dhpz&EfN&ak)l$~Z!M+3tGB(1p-3GLz;`=ZWaq$#oE zdGP^g|2B%bV7I)IAPRD?PDx8`c1M#QGL_C#(FtbJdFnx>eY25$Ni}LjC~J~CBJ$l6 zZ)mem2ir0y49*LqWw7$jktj%aPrb^e(mGGAF~N;{c@?@f&|?Xp@<98qeExkODzXe> z$~L0_TDFh%XVFx)Uq5+eT1I5=yoh6t+>&0l=46t#Q6`iLt3gx#O?8JOHqfo|m zUxHtZHh({m_o82^wRnkJ?{ z3>rB1Q!r-6?@ zlWA^NlNPE*Eg;J|#we_t{kEP&S#bmCxH#`3|9 z>xrgoPx%LgSJ>!%V1ecm@0fIM3_|MMXwC6XgT8&8DrAc|mol4%Su*jJGkg-1-W=l2 z&GqRqE-`sJP~n|~s_0}UqIVv|xG`dJeyw9+TlIZehhGCObBFBX+;m?uws4E!2BNtk zVkHyi%aS;z-r3s}W?w*8b64Xi>DrmP{dbV=R+7x&?6nCypIELBz0}NC_tMiSzxm2|*+8`XmS@;%k0GK!bKcrX%@izex1tY0q4RLn&NQtCT7Hk>zo|H^C8^>* zfhM?694F%y{HVA-#%z95U?-sWRvbp#O~nD#DbAq29NcjiLT>u{Ad0$<(5LTFeuEEQ z+WO}s{CJ#g^RW-&e<%0Jl`VENSH0y~khAP9CLc5!{_~phW+U&`lUpMAr3il6z`g^_ zVwA`6;8fqQPVb8+LH3VJ(d$-rMN!K}YWD|cpu-)s+Jn))MOD%C^|Lv+p{6u|O6KS> z3MhUiuSS~aqztZEW07Nu&sqy}CA9>daZEDOdN(S|5mIJ)q1`@~L&sSYAk$4X?b$*F z6U~@V2$zeS-W^?HIIT+)hS7=b-=UZX9a74DX4UFs!#sS`-EV3Ew$ZoLJLp&K$*W>$&6+_|NAI)VWf%%q zB8CZ=(~b~G|E-tYm{CX;tIydalAA^!3XNvLS95YYS*x}36G(O=-@x*lKv(K`X9N)n zoxZ;X@IK-)uTkpw9n>;#Yoo;hx6MZ_H{p&gR?zr-R9NT1z0D zj=SH~!a$eUZ|hrOOvQ5sF>*sqDn%p*dZ|ecAc>+Ma}o#c?jWiDBTM>W6thA!IB5Qa z?a2l(av(mzLGdEc76%6KcCNIV1V!EFj!{vAP)nRevIU$5IRvBP3KWceQYu?GAGL&4 zmP=FL`Myuz1@)GB)|3QUjgB$2$--odE2@jB%)Ms<<^CU6%t$2+vPX63+`8V*Fskde; z2$<~Y^bpun@Zo4Z<4lsoM?p7#0?Pcy2~?(9AQIP76A2h;z1x;r)smYn6I=z@&fI z`s0{8*5CW66{J8r(ce|ptT&umCm^fd`r~N3r$3-NEg97Jj{U9FIzd%n%)S+V2|y<9 zKl5n+P#|3ZDi>6SK_od7^J$wMP3RyZo)%#o_yIs6+zU{N!Vdus=&mki?Xo{vYJjhmBn-tezra9N?ZVkuV~nJAM2yK#2rC>_qZYfD*}l040+90W$3OeH9?Z zt5N;S&A8AoxJWV_j*JBH{K&fJ`E%9`W$u5(*}qoDgMBfTgY4_6RD~}R6J)!AvC-~Y S|1{Oj@~4llddBEjH~YVRIC1j; literal 37764 zcmb__3!Gh5b@zGPbMFm?DzyRvl4zKL1i~XywN()UXhKy40-{wXlgW%soy>&EBqaC( zA*1*Ji--~NQ;dKW5k$~pMT10qgSFHrLPXPQtyWvK^;N$0|Nr;voVl3?^2Tdftvs)?y=_3%hmtk|@6 z_{^;18`!CXve+;W8 z?FG{0b#9&XYhIIq>cJ#EC#yHU>?k#Y!ant;hu-v|q>VEi9A6E@>@k&%ik~X*As)aD ze&(XsyH2mapX3&hkH@5)$qC5 z@-=I-!v5M%p4W$YHifqYO$SJwhSx4m;Mk@&Pqfo^qURi?--FTXK&odRzz)Ir0Ov|D zeSi;uif94s+W|NDd6NA$*?H)a_lqHl>q)YR(UB2$=pla%fL4yJ0qQe+*5czhnJ1Fu zQyLn0X!;7Zg2qBhV0h!`x~X*(0xAz|7cYupKn;hI2o56#D;5G=qs2*Q}k|6vqIvC@uzg;2~w<*ubMn))AzemQ&|s#kiv}FgiXpIT0xZg~{TMVE?(~ z@EE|-7Zq+)ms!Uet3WBqFNd1zm36e$=Q#!*UK6BI9Rl=yP;@kLf*kB=0L@XBjmtNd zvT1N*RtybV=zvi1({2~bj*%;CZuY!H&lFh8&!<`d6DrZC11gilBV#>g-3NpNP)Oc@ zg2g@C9`YQ$*R5Z*4q@vAv_r*WGFo}6bQ-sXoEoF^$f$+`XDtv~j$$4~!A{G)_>Q;w zR&GBSd}RIj@W$HcOM^%$1mkDKYMf#~b8)+PW!47t0u;#*#&T5R@;LodfH#0*u_|Nl z6=ZM)+Bh6p4VqqN)q&N)v9TGfqTix+aU%X^2c^T$i^ErFOozv_$xw5moKC4d4R}$V zW{9OpifhsE+L|LSlVv;u#BAa+p@Z-=&v$=`J(!rsMhDkr#XYxWa)X!H@?_jV`bKiV z{wBJ|jI(Si(DT+{DwbI+mPR={PJptLvi-Q2Ynf+M@Y>0ViIIWP$;n}usA$N3Fc36G z|C5Q%_Y{V$O)f_3RFHgGxt!Tl zq=dzXmc{W-L%yH)E&#*~ttU?K&DR-PeZ?<}QAg57WHsi0z{+<3A=`10yPn7dKNP{g zi{OU=-baKR1R~(!NBISVSy;wCgpRyRlRV-dUs zpcwu*z~9=U;~1t`A3$Xz7zh48YHgl>Ft^DM@tIpZHZYfBb zLP&G!mKON^6qQY)iqH3AB#Hm)5&TDh($6;x%9kj4*@|kV3V9zu#%cO^;O-u)mO7w* zdbycEEd`G3jSsF$@`n9DQf%D^P;C8k1ixuu?h>hOsLtkfi*p7y3=a%%TsxWN3s8j_ z=1U+`ntHwjoaTKd0+~K}R%-Me;4hcV!FTHUT53>NpWi=Ojgx*l!Q{LuH9hptk3*>( z<$C}%ulpnTeFO93jAcn?t~f^JNmiM#O;&=jeb+D?E0e?PCdM`lAJa4Dn*-3@_rZvo z4QM}=2L1z7ilc`j_(LF^ZG$raf(wVwv5A6-qkfDoDrK;mMk9161vQtJdWZ`4WWe{A5&8FBGDPcx5~c z3~nqvFOWqr6qz`(5)g4_63ta+!Ua^k{0>+Gf6oqPsj@Y#7Jk^@SYsHrnP`R4hd{#R zL=7p(bZb_JGoPoTLw*uUMUqDVlA#=s0|~3Pu*&>0cwAnhcsoHBCqOp=GeqjoKZUUQdUm~ z4h_u5q#W~=rq^v+gM9h~;PgJ!TgImOefV<#io|NEk;kHv`@8&c0BQBP?2!n6irV>y zq1=pu1jvv)_`R%*1FXO^1*`4!R<@(4xk>&fR^w$nY}>6}1PsX{?zbo;8lrMEN&5+) zFOac~`>mXdY?45d0j+@?-nyV)G9x_tsK(6AMHRovm_^d^EO^W@S(HXX+gg?+EtHew z7}06aY5{Bc6Ty(QL+wdB2clLMcMw3vjQmLk<@d1L!2s`#I+LFS)Qmct4#UbVh(yK7 z5S=sR`&&Prk22RC9@rD3BWV_zA%^b6%BB&{N4uu^WPqCHQvhn3@a=quca8iL^mS@B z{{pb0FiAS75Ti#U8yFuBo3K69B*wibYK~KggE4!NPMezR2V0ubp#U`{szg&-h+1iG zkwH##hXedsFU_r}&>_(rc#-DhZD{UbScxPuBx!qfqFbuYWMjIAGNBMykg_yP8DVf_ z**W)q`Ct+vTxSdQu+s|~3#Y>L@VO(q7kV^m?XFfM>hBK``zzIhGG<(p%wl90-BogJIS*}=EDn`&HvyI{_34{|7JKtR9 zqLg3dXzxvEpME)GqDyScCP;s!<&C#GI z8Z!%-TveQdF2zC^fEKoCG7#B31IuT&6$L5_vKD0YmsSUqD;A+-OLK)_jW? zE3CQ$Eb&Zfc4(B!gp0F6n`UZ{%0?X)>?=#KI6son{C$vkzM-}8p43GOzKZw3B6uw) zi+7N6Uqmgp&pj67h$MyWeU@&FHYU5`v9iY;j61=;7@)*`Hb4cRml#yMlDIDgILbK0 zq!Y2apors1gB(Pbw^x*_Lj5a1cDmn+9C5fskV1`&2&bi6>B z+mfXK#liIElna}J+_@N8Q7Q>#Hwo8{of z(TOz!_Wpk8oQct)+ACLu8+%`Px|ycarngZhcg&xBlV0^v`2$tKX=Pf1qCIz_Q?998 z60*hP3z$+bzAaa3enGh&ShDh{b~_(s_sj)c&Y3BH2hr zq2WoS14kC^4?P*BpS4R-L+7f1=na=A+ z6L(yi3LfjsTxB&4W_EFaguW$ImEQ%ekpu6>=rLg{fJwooy&uCT#q*xCx)k5zJ=J)FG7zg_wA#VQFbz?HOO~ z8K35?XzOA;&N7BiOAAI6QjLI?=yDPC&DdR>=@yRSOm?0QT!CVNooyEKtPk3Q55U;j z`^+%73uoxgono-15=+{`$3ailcq>32pIFLcKMup8)~ShB4z0hGld1uI8r0$&68Hw3>9a54lb zpM2U*)A12jX71<9DGd_`la!4LbM$hDMUg_P1f%A6r2fcKNd`4 zN(v!lMhRq!Pg%q7@$9mO1%6F}`pRFTg*hg#w3ZL! zd1oln@n)H%hC(lm_Xxn|BoRP09xqUrKLwI{YKp%@MKHpt!Sz%4OqGjjk}D8SM8R>2 z9H5&Qz!Mi(k$)7R=R8enb`v12SNRc+LraG_VC}Kd zx%??>f5=(}0vT5=_412cvr_TAS=&t9qE9q2ok=#UWi!2MC+jJpQI_zVxKWlce)~w~ zt`_N_EZvyO_Jthe&Xnil@GK!x)X`7#F>7h<<6JKv<5o}xsT|s^#=iiCxMo}IppO2% zS?vh5_UX5l))QiqwriTRwinD4h08K1b_}f~* z!Q(g_%(u!L#VQ-rN&=phN3-JZOJ$JD#1QM1`54vmL<}Oe91y_+2||91@U6uLwT|?2 zSsVq6g`{;voEsM_E;N*BzS7#=Mksa?Pf;7{1WHd0m1$2u?va6nYYopXN2~MEIs$_y z3hp&-ic}X^>zQ8k@S@(4Fd70)QHH=_5<@tdZ1_o>9GRq+T}PS83`0;W2<%L`>Aen+ zo7h9#EI{W*TyEiIW=ni=@hKh)ES)E4@hJ{w4MQrtewMX33W0%=+w%gmOxEJoi}CD_ zds;815ZIAIV8`GM?))IyYl7pYFv}WDvZAO#t<>w_rWmj|ILonq{a6%vpT2~;1 z<_CV*tb`;AVJV4JRu+6Wlvu*3np{X2g%EU#!rU{7LVE*ImK%knN@qt|Zy^cC3n>Qg zu%;$&1coq(mQo(rwvOa{G++d2&ax%Gzf-U{nteITV+by^vh^5(C_trk8jP`E&`aZX zZH);_%8c3`Ya)=Fi(+D(Gf4DW7J=VmUG&wBg%Q@teH{?PRbHmmqy+$-$K+c02LRSK`855P0p#&t@p6E2vsVD**KUY$ ze{G@oYpb^p#5X^%#i`7w75g))!7NM&Gc(v0o^)Nsllk>Gt z>o%w(dmzsH5qr$$>q^DpCGRyUKB7DK@kI})W1kXs5LgE9f^|b@%2pESPQrA-}YRQClyJ__QH*N+Ql~x(|l#Exxj8cE^}J zyKr*w`jVH$^Gx?*qxI!Lk4I{{fmw``b(-8n1lJna`f@`}OkP`h$Kh^J%IDC}zvw8| z*n>M`1!J?sq97@E#>!M6(a$94Np~l4&C=a zKepp--oag^S$OsQG>}Wx!>LLJv@(I`Ti4c48|vYqYn3a*K9|IMsOLOuNYsOG-SO*N zG#Rq8FzBb$1r|m_>PK$<8jK-^UQ2Km{fHv4w2H=Os!CzIw<|@|lKtZ|wMKe-=2fw0 zt4>J@Y*GSFa4@{Znq7m{+(2I%RK$A&$Vf^TMet%&y2VOz4xMA}TJ=epuSUOE9eoX{ zTdGX=)ls`rsA1cuD?v+HHz0+=X@Fw#jRa>=rKe7D>9rQg@p*SKQLoF1Pi<2Bd!{|` z6@5-em(A|Li7JygcB8gbBJ`KN84TYBQj*A}5yU%{{J4hWW%mK~dD7KpAotSMTdg|L z6|Z0Sa6K0e5|>NE!QX53%>#j-H~)n6ZK zrEXZ*8xj#_cAZk6adDH4Ai{;h4l`g;yuj)6hsZCeRd($J;m=y3LEW3>B_2bw@# zQ>P@duBmW~^Xg~ucc?vxwI4R9daZ1@jp{`xIBT>sZ?9el-~z@=u>iZt z?nc2&@4DLxQJ8P z0TAug+eOJ=8*pEphvp;Ee7TZe_@xbnns@17TAEQ3OhND!EuJfT$1GQAT(Ya^c)Wb9 zU4m4%6{N|_#4Zf`ejE^C!Yc+o%{p9rcQ2&lQys7wGX!hyJQTSPWcjwt#jFYBGL!MW+ilM@`)1O0|vaQ33m@Wg~cm zjPbX6SV-V`CX!E0zGZFhZlaxYG7(PRcZEZoaJi^mtR_9%pDr61#I?R<1NuH4eIhHl zUrNu!$I%B?;aq6h0CmKO**=(VasWtC9*~bdaahoqlvcypT!y_Pf>EFr7(JVD=MG7z)D3In8d&;dvw7hMNK$zyDC})i{eSvqkR~9YZ44a#SRcMNetpI zqe^j>-;u$3RJ9P^<8TdXAD*IQC8~~SqFAL`7B^ec(TI|jK;ex(%2IaBQ*otWRXQ`n zEPhg0*|p#HQ82LLCj_l<-vzQ2U}eAU!(qJTORR9-!K)j^Gp)iV*N^%y04DNcKqZ9T zemcPEI$vbgf-;(zH_hM+S4155tx;Ae_kI{E!{C#^0pNAgx;W&Bi zx0`V6!Yrdv#+)UI##}*hu|7oY)i#`c_P-Bhh{T!^klRnjw2EJ$S>gEC5&Z86{!avd zV_^F{cKaQ`O^}vs$9+B*xG=FaC{IJHVwxdC9mwx3KwSi(DSp!c#P{;1E`f>=G>iUc z1XJ|E%BmPz>;MS%LyUIzimD^)s&|nEEl))uE3M-w{h2KkKZ33ZJhF#l4lyvkUTt55 zXU5<7fv@&6tgijc#z-YPV$EwGkK%-eo1;ZOa0z`#GUP4Xbk^uPi`$}k00kzS4b)jk z1oAxKEVH7poYXv)%57f&{29sx>KlM1mj1t~74F(x8l}w^hSW3;0S@AxTIQnV928jL z+PLRDVDGf>(^FIzSwl~AQ=q>H6K;q%SqHAN*7m8uiSdy^oXoVT%ronHOeV0U-cc>H z1lG+M?Q|4x!ifHBHj9VtVP?>=d`%u1-$U#&1q96vD4qh>k+m~mlx=%f?BM6$9N3Mu za|~>6fS4_I0iMsVI4BSa6)4gjgyEr@S)DfCJ~1z$(=ZF(w6yOXc~pt45or5ll`w3B zmt%Nay5v__mV2X8llzkhJ~o1niy$`fN>0l^B?yhRZ=+DKy1B&z(27{exQFTRws>t7 zZX75_htn%>m~_~xl(6L)5_!~XiThUqjKdq;;$ei_n^1g)`hJ3eP9*zAaK8xdAHgRY z*#0`Z9SCrf)D0WV+83at)!z+h9tzxUa4wiHf&6wO1OF9e<)0bujOqVTR{dGBdoZ|> z;>no6`LXuN5qye)HLIS-X;LLKts2NYr3=RVB&!O%;}+7R-4|?fLA+M3B3#R57sT;$P7L!?Z8(!34J5z8m#>$rk_u zMJ}xmfzUN5W84`W7`NRe5&+tGc`HG_=+YN6qPOx@2K-Fx$4gNQ22~J=j>WTrU?dR7 zOhG>?Cou}`^OCG;H3sGNoc2bv{RhQ_72XN&=m_#;O)_5+Yne?ji7Jn^+Rlu3NnVQVu3B4YYGD?CVbx(4 z?nvI&lhyVQY9>cl+4nGFQ8|IV?QCu>0b3*QrQouI`cR={I-EMw>980mr0K+t&z6qE zNPGily%f(pktelAt6D6H9M_E%BpK5~o;e z>l*8(Ip`wTdqGfYHK22>HIK7hhdca;R0mdx&lZXG6<|s?zXDyor1Ce@I(BEiF&8=d7R}PX{RFodNJ5u3kF;qP_E1DBv@l=l5zs7T)2l_X>HUB?Bm_ zALzBigZ||Ca4%yrrcc|5QNGNgIQ*IlO1woPG+0q5#KafbQ%!DIfTH;axtaAlqqmnB z_r3`&S@pdR)IfY~T3v{4K?9qRHZ*S#kWq@4@nwcS^$(Wzit|Yh?P6eQVW8UU zsq0k2_i_MWg6V_otCI;DMs-2t8k6f> z%yBqbXh7nb$#q6kbwg7VBZi&1w`BxTP!W79AgdNb^{I5;0!*qqEM+ULW)|y;A+Xm% z#u+6S40>5t5(qKZ&iPj8wNXjWlS$D#Wl|GBXa>S-t*-NG6xTHZAzQH1=)795GOjaN zv+R5j)f;Ojug`F#L2o6{-9`csgPzbB^v?H=IA)DCQPmcUJ&AeI0veLyLZ5^`JXhPm z%=uLLIs;w!n*yltw;o{Pe7Cnz0j8@vQC#Rv@%F?Ny)^U^mIEtBsdEUJ)$5H!XWEKh zuCxtW$ZsSzOpT)!wGSxA$u>O9eWTv7pb%fb+LJORyqY@i7|`r&hy9lNEVDyLJr+3b zYpeVF4UF$tJ6}Pw4BUXumq3bnK;iDN2d3h_xbxLIku>4+0{oPwYcwgA>cT*WiBJdP z<_3d&SFexqj_)mjG8FqUa+M6m$;a5~#?(iM1mO*3Hk2?*vp{cmcu$MD-<~Bzh9+i3 z?Ggib@VninLuphOCJdrwGm7t95p^AhJtY|y7!LwZ10d_@Y`4OV;$3CZs%ox+gX%|@ zA4Ew-U-6q7cuFzfKdrPUvvn)WH(KHR9;+RV4uk)yGZ?7G$7z~eg{EzFdA*N^Iv%UgLlYzx-oJZnqAtVtPH|bkLo%=-0Q{D zzzUpIH(>rs^{PIA+Fyu`D9ezMV+krQw!+ym1VJlt&s*^fn&LXXMytTT#=H^paV zeGW|-e}BFZe(45`}}NKlvIpTCun;tCFh!oJ}~^L|#ZR&sk7 z$!rC-xW{v`Gvc!rClcMmB5M_%k7*#Gxr@TRA9)!-&Rcg-X^0}nLF2P}lKe|Ur_&AU zYG7D^Q&vPmyLiUFsCy`BO6+*}AvdX@VEG(38ZZgxa-p?*_yVhJlL3A+ zXzL7n?)EbZ<#(fp#C#Z|P{tHmHGOFF_mj%MwTIw;`k>Mu<$#<*bU?Y<|G`jl!1n=E z?fU^X9q^@OE3pJ1aWAaHu^o7(9nQeqg>zB%wo#=s@e>EsM0X&{S@iHc!+BO)WtXqN ziX8^Z{6@%Rbb$dPp;`8_Yv)v z!!-usN99&v0adO+a^2(YS)U6bPozZXYuZ@6$MsRir5L08EGx3B<%^iUbE5940IA#o zXspZN%4a;r7br|cd1>1gpFuk`O-z3XnBnG+GN#^ZPh$1xA|t;JpiCbtyxVYp2p~;g zM`Y}pyq;&CoAq3VNH)6&1eB<|Z8{{HUCe4Lx`*>wZJVv4eK)5}%bWICI{$0okp)(= z{3e$!r>@D1``M>~$R&?vN~XD4O+r;DOQJ;i~NMV>8S zQp+Pt>dQkI+#Kg(%};Uf7_!yBAEe?uDV5#K1~}cTP`rnu<5W%D zxzRaM$xWnu&U39HhM4O=m~sNTlM~4qqr0XK7wQxQQU-*}Vx$%aG=gXLoDuB0jg#)buac`2fi0F+hM) zb-m8vZdN}a>;;6D2F5cD0H!Gw(7x2%iy2Lt&fdMLCo}D%;-v1xSQtPz!|KdfHRtD< z!Smf#&{DOH7BdU1jyG_Mv&>6$2eLRT_(^wrKYGDMy4z7eWmI&||AZA=vDFmn%i>dq78@?)}M-ct(r6`Os{sbHs5SN9;2@I+=;+-3NdkBNpe^=I0uk`?Btx zabUKKy%*ODRx+8H0|z#c>Dv3 zouJm#IY@MWjN&Jd0`DuOin|s~7%YyH#S5|;=l9mEFIw#e^xlfYXnUwQpgQ#!)YXYf zwBp}G6ipqWPxpWQVuu5Vj{fu78oI@~=M7hs_8APj-4fF7gF-6a?jX6uagKo1Y zuZqF7YX?jnz0Z1=8X_~)Ap+*KBLwdA3bB)`RjlFnmC9oEIh#as)4-t6Xcl}m#}zaB zTQMIv1CX)4##E`}mryJ4%K)Y1uK>J{xL*aR)bVQonPkMf2>K_WHMaVIM*G(rIodxt z67C$4~>p7+~@`r&Cj1O$n;F0-2dZ> z8L5Op#^u5sui4Hps`ltN$JXE+68vQ`#UIz0sT6nr>Z&p4AL@lnv#H$Z7ozm+cHc?^+`|i~cURX1(FmIr>M0U(#XX%{&M*_Lr@$}2g=dN6+W@sxeg~jL z@?C%u3Af%1`*S{pT8dYr`j?w=p^@VVxBUr(hf de36(S%l*bihu8V1so^X?d3^PAN5_V<{|kl)F17#w diff --git a/src/kernel/kernel_decls.cpp b/src/kernel/kernel_decls.cpp index 72c05cbad..c9adf1d3c 100644 --- a/src/kernel/kernel_decls.cpp +++ b/src/kernel/kernel_decls.cpp @@ -29,6 +29,7 @@ MK_CONSTANT(proof_irrel_fn, name("proof_irrel")); MK_CONSTANT(substp_fn, name("substp")); MK_CONSTANT(eps_th_fn, name("eps_th")); MK_CONSTANT(eps_singleton_fn, name("eps_singleton")); +MK_CONSTANT(nonempty_fun_fn, name("nonempty_fun")); MK_CONSTANT(ite_fn, name("ite")); MK_CONSTANT(not_intro_fn, name("not_intro")); MK_CONSTANT(eta_fn, name("eta")); diff --git a/src/kernel/kernel_decls.h b/src/kernel/kernel_decls.h index d5d9f9438..d9993117c 100644 --- a/src/kernel/kernel_decls.h +++ b/src/kernel/kernel_decls.h @@ -81,6 +81,9 @@ inline expr mk_eps_th_th(expr const & e1, expr const & e2, expr const & e3, expr expr mk_eps_singleton_fn(); bool is_eps_singleton_fn(expr const & e); inline expr mk_eps_singleton_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_eps_singleton_fn(), e1, e2, e3}); } +expr mk_nonempty_fun_fn(); +bool is_nonempty_fun_fn(expr const & e); +inline expr mk_nonempty_fun_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_nonempty_fun_fn(), e1, e2, e3}); } expr mk_ite_fn(); bool is_ite_fn(expr const & e); inline bool is_ite(expr const & e) { return is_app(e) && is_ite_fn(arg(e, 0)) && num_args(e) == 5; }