From 94a3136904a90de9e35f2e6a532a6f75266a799d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 22 Jan 2014 08:21:11 -0800 Subject: [PATCH] feat(builtin/kernel): add Hilbert's operator, and derive axiom of choice using it Signed-off-by: Leonardo de Moura --- src/builtin/kernel.lean | 13 +++++++++++++ src/builtin/obj/kernel.olean | Bin 25296 -> 25921 bytes src/kernel/kernel_decls.cpp | 4 ++++ src/kernel/kernel_decls.h | 13 +++++++++++++ 4 files changed, 30 insertions(+) diff --git a/src/builtin/kernel.lean b/src/builtin/kernel.lean index 2b324829e..8a8847285 100644 --- a/src/builtin/kernel.lean +++ b/src/builtin/kernel.lean @@ -58,6 +58,11 @@ axiom funext {A : TypeU} {B : A → TypeU} {f g : ∀ x : A, B x} (H : ∀ x : A -- Forall extensionality axiom allext {A : TypeU} {B C : A → Bool} (H : ∀ x : A, B x = C x) : (∀ x : A, B x) = (∀ x : A, C x) +-- Epsilon (Hilbert's operator) +variable eps {A : TypeU} (P : A → Bool) : A +alias ε : eps +axiom eps_ax {A : TypeU} {P : A → Bool} {a : A} : P a → P (ε P) + -- Proof irrelevance axiom proof_irrel {a : Bool} (H1 H2 : a) : H1 = H2 @@ -196,6 +201,14 @@ theorem exists_intro {A : TypeU} {P : A → Bool} (a : A) (H : P a) : Exists A P := assume H1 : (∀ x : A, ¬ P x), absurd H (H1 a) +theorem exists_to_eps {A : TypeU} {P : A → Bool} (H : ∃ x, P x) : P (ε P) +:= exists_elim H (λ (w : A) (Hw : P w), @eps_ax A P w Hw) + +theorem axiom_of_choice {A : TypeU} {B : TypeU} {R : A → B → Bool} (H : ∀ x, ∃ y, R x y) : ∃ f, ∀ x, R x (f x) +:= exists_intro + (λ x, ε (λ y, R x y)) -- witness for f + (λ x, exists_to_eps (H x)) -- proof that witness satisfies ∀ x, R x (f x) + theorem boolext {a b : Bool} (Hab : a → b) (Hba : b → a) : a = b := or_elim (boolcomplete a) (λ Hat : a = true, or_elim (boolcomplete b) diff --git a/src/builtin/obj/kernel.olean b/src/builtin/obj/kernel.olean index df77b2434f850228b853334ade621e1529534f5d..81a63524bf7c3ce1b5f6884a9f124e26c3ee4e69 100644 GIT binary patch literal 25921 zcmcIt3z%J1bw20Zd+tO?EU5}@2nGog5-^556q*2ez?A_i1PQIulwp$G!02QqnM^{! zsNe%4h@b+IA|jv=1s|x?S|7y+f(n9)P*A8s1Ql(427L6f{{P>vd*)_B_`c5fvF|#2 zuf6tq@7FnDXrR?MxVnF!mASus!(ji$*6{jPR-BsUxz$=xtQZ=}R<%}V#jdmp)5A`4QIuYp`ih5Wp%z{L;t`?|6rDn3~y*<;c0c>fKey4K_lBJ`m&ljvRhf= zM+Mpn)>=_NacHD(qEb$F^)s+9+Y);3^s3IcmOx}8;@c_ zJH2VsNNy_m*sH?FtmSG%zrEZ0J+|ehq>X&^uUR|L-&zmkPQ0{nF+P~8wJtku&DyN6 zU;E4R_F;~s^5&pvlFVs%jbbs!HoJMET@9yt$|(E37`^tTd8PpDBDg=m@ls4T;7KqM zJ%D|?zzzQPv;V5>Job(ciXp0NKY2v|>ecMfLH`;6tsGkev`cuz%%dpGUz6kk6$?Ce z!R2ZNjTzKHYg7OFk@ZvpD)(&^OQRZ4!=a>t>BL~g41fnq?nbc*PhJhI6mKJEnI+Z) zdgXyYn~0)IT?vxlOn~NUJ%jSDxoqm&loc!cEcn0{{u+&`ag|pQNN^CeYa!fWenB$vIW7vw0?Q ztQ8=H0CH|HEqEAJD1B@s4o5pXf>g&e)}DjfDbrDs9ahT83AWHehYnAzF zGu>|$b-kfFJ#Br9T0!y zKo6PpEmq?L9c;GN?KY>~pc-vLU*jO3Boh~-S-N^>1TTr;y8w#eO96h-vX^6+YP}AX zO%(LPcK$E2YR|v%zI&SfB8c8fF5d%CT)sDgmq+jlfM89Db!%i&T8*qSa>*}M5pv+W zjeutrITinLDJo&LP?|w%+zV(mMDDI49~|PwHZOh<4fM9?!+~~3FMa?$TmVJu5CBe?mll1-T??LgwrpNGnr z5Jbcq<6dAeEqY#{i{L0SDwd8Ql8vvpt8DRoG>Ml7BFHJoHX$z8YtHb)-fwte*y^$> zjJ^`o+zKd;OabJ&ejOyAH7+?f=Ht*!ndD(oU_kvKfa}i6w;QT+|p@fW>FX!y~D-5`tqrAlBk$3JTdw^ZZLuVLiP) z6_DX^0`2oB;LtuHCp~U8vh@0M)?oF#7&x7eO{C)esp3h%O1ze4`8m51d1eg|+%REgX$qP75zgkj}% zM510~XYXtOX}CP#!9r@V)%$F0O42MOA;!~L8!M|e=9DHepC)RF@);Bo^A85)S9#CN z&sFFt++ZiSSm0nJ9y0&$t<77}HU-B2ZralN=NFn)=g6w$zljkO+p)50yFUX-Lj5;D zIqv@elu-W*khWt!k?nH8`AwZ{*Q8cj=q1}>SlLeQjFv9u|7!t8hNN$AP(*BM&}5&t zJN`|fNm-hpj*N7UfXcUl*}P_jbdWO(Q3pAiqyx>K(g9@1KgVw406sha1s7xbFIRj) z+}1kVXxZu`WXLejU2lXOQ(TubOXho`_Ijr4>i|-q@lnSTCA82E+nk~~3o8${)~(*j zus5JD*P}U8uZDd-YH!fudNp9<%r8DUdPZ)jcq+CnWOF=eVB7edIgFKPu5S z+mD^ensC4{9}@`FnoaW4NE1&iWNNjtl94F?A}EB?+VY7&U;yNQ8Nn9-=uPP`F^< zwi_t-N5N3YA2U!v?Nz{|x+IZjQURr>9+p;A!1*MoV3N^mS3yS&$N@V#igeO6RV0&M z{x}#Fk4y?dK?+p4NK#2v1>5G^DL5;oFA5=$z2rRzLgzgPaX@yP4v?8LpJ7l@W9`8J z>ukdsAzvPcq^>z+)?yQf;5A+su*7rIpsb5dnL}+^0sm2(Bt<1n|XzZd~c7aSta{stqi-|(dr4&O7huEkS|^WqKW*6;aTz@4p8#{ z4M2q=ac6S55iXr57iWeAlA9Hx%AP3vhBtqOJ-7{@v*^fBZ|B=7vl%zNV$<@xqMAz3 z4U@KDOw;lmTIMJWC@B^KloX2$DvsmbM^07CGcH8+30BxLq&OSDuw##)rPFG~B6sb@ zrY6e7DBcuDTD9LsZ|Waf(`$EHE6*D0Uy1EUFos;zW|&up>`h_X@BX4?jFEFV>=ZhK zL_|ebz`@x|NW0QclgMPU3&=C6lve_jQjU!voS}FP5snAAoGV8f$?_~}dcE4UC!nrv z11P>QNb$0O!M%PCT}Vmd%uyMetOB%8P$zP_b^hmHE0(WNMu%>*zGBZQo{tZAdIQn6!$sMGPo# zm||0fLX-GtIoCR^@SSR?#_quh!FpD*LvL9ruM0qXPbB2QT{;)Kt)n2A6jOKV#j~>h84)Bwxf7hUSf_wd z-e=4uQR=h9>A>{s-JRYOC$C&k2{ejk=~a<|7C`Q0ifaHmthSSgZKl~dXmqP`&&Nuu z@oaR^Q4hP!?Z!`xFb=?*!n_|XQpxK8&YfmO!baW3b%&`W!VM_(5ezQ2>eM*4TS~&g zjAvPmI2^Rim)nml2HqHlB>7drfcb?$6}N-z1y$xl05$8b1*pkvok7+Yk(Fa$+s>j4 z%&f5opRaIjhRfS~Y+3obv?snU@ zVlFwh+a{k(THH=J4THu;(3Y7vjg`SnITqN(U1lbr~At_F?7U5dMbPj_J;#UXf?Q*Z>e5D}*? zrm4R5>xWi`Ng|y`q;Gd+7&PU^4$mCXZV|xNn?YEbJ1>Ig6AVf$9%-P0!t5}>4osb> zk4V%=I!Oqz&vxrmpr8_|fMR=8QWGung+3K9msXn8X=x##1sY;P%9?NtX-FQ2$0w~> ze#2Rl`YoPBN1l=hoz&<&u$WZFs~w?}Pv8{ydnq4{yh6VGlnSqsO<^Ax6bCRNIVheo zhzl*spP$lBGn-PSNw$Mqq*C1*)lJc*3i=Xd3;Li-N9Be>za4LJBuUP>YD z8F2(EN=0d1@=MS$##e0|o?#aJ*2YDt=q<4Ti5#5eBMw=ofU*hkI11m4FrN6zMRGCH zk*_)iRhD}K)x`KRR_&D3wCfQ?6 z94b+60G3`Q>Eg;Ozl=5BLU;*z3}w`SO!X-pZ^bjyK=IY7ez6Mk)fiu#O!;0)Z5lAQ zg(4kq3?VfXdTG3W0$5gr#Fj(j@olIY&o|UlB3_AJ!3jtDHjE_il1Z;Xn1@2+ydR*G z3*bD6lVchY8GB)QXY)v)r@OjrZ+1eVsqq5~D*B|)t0G;WGSW`e?ME4=EF96ASUbOdFH5;A|xiqsJX@EkJbK;(ydaUGT4wG5Zf zCaoZ_E#;`hcc3`KVID$3kiKKd(FAsnxTF{TOfBWw+7W&T-!RW)p}x|%q{U^Sk0 zsHZaMr_d{=zUm96=#*(Lk4l(}N-5!U023u}&cT)j^|i~Ogp4~HE{_;7%0d&+!rfbv zuT<$%MrS1n2TJPa%a0u#*B^dproceT{a*w~X0x`J-D>m=CI=RD2~T~LBYNs|L)uN* z@yk1-eghghQ15JDAdf>am!WnCKrP3&5JWN8i{II2fpRkniOuPwlh_P^3S)TliQg;9 z@>4;Ei)o5W&taSbkE81qo8;|6;t)F^;wvDpwz%1-jNoQfu4!mwDd28!pqzaVL8QdQ zeibUU!&yNp^wS9*U#D+UWn{OuA>h}TNZ2V+$}YNZiQSnHs@=gX7o<=a(oFTf&}~w2 zZfk$F+XB682P!7e3%(0bO88y`?>De^8yUPV7>en>_AMp7Q40#cZ~l&Tb*C#}Ed6jS z94eBNs42H`W*SKB^FZY1L4sakI#{jhySR&FNrk%Fm3^iL{O4q!NwNE`?PHsUU6|*A zKrS`U52FqqiQuCK)~c_*awlE;h0ODPAiJd-pm2)v1A9o!gRi*8jvul$12mM8;tfb*#%gnR0qEaCEBt| z2{<9vaH6>jV?Gne*$Err6(i!Qv++yq_Gw|hXqxAqU`z~=-0`vKe6i6uI{VE zo!Qo~?WI`IV!Y6_%8EZnrI>t*;25U#)Tu7rijW+icNKou$Kh#BTL0Nu4}9GmyVvnt z?T)%=GO1%1W=l0f%_~Lz8lGx+_h;%jafg!Oj|%GL`&+BNF^0KwTH|a9XE=f40i{ zu@bRC3=|}dUc88^_ZUz=9#fZN;UF|!fI=@{wg{p?Cx?&6pqOXu!JjvCO)@lWpADLw zs!EZ#VVcZNiUPLZlD-T>6*)%XyG2C-@L-Cv86a6XO_cnFuKQ>g&A9olFW0pm%w`{t zp{7rpeu%6jUG#uZ*7DEwGrR#RS2y)DfTGJ=W)|Kr za=R?mG_7wsxzMA53nmB2KMn)Yz{T?ns-IR3CwNXiBlI6)Fll`n;(^H%Is z9B2KqS&*|}{u57})v7kx9IcB3muwbkMLnsVDxBq2*69t2$c$InW^ZT2XMKp=`~`*( zH+un;h9(+R-<)bF(KgU71i}SU)}E;7kb8>fTeS~&#rlT9)k6cT+TOid%HHXRq;#(O zMHCy1bqOYpZ_<-cz)!;K22d8k9{zW$g%dMUk>= zj|IJv;`@(CiWi{X%^9f^%?a7j-m2*2M6!VOPTzQmsiGpOlDdXQA5g3xS6W%npX5aQ z+p}|`mjL8it2n@*`t9-y1M`RRd<6=IJJY+!*f|(V^?#2&~9FHv(^bw-vP`QPRdT551)s zy-nWZ_F%<}4Y!kh#xf6Oz#^l55sKSO&^Xu%U7hNED8=eaQOl`>XVAWb_L=pII33YP zlGt^-2a^?@>$eLDjE+X~Vt^ZY*+6Uch(A2n$bjBPrTV zPdk0loxSKrT2>QGXzMw_0s}lPDh>sx(13^6e@aWv1NaMqhXMSZcV5fhj*rsGID)9* zg^=8EhlYuRNy~=BEL4AHSNMrytWU{BbAGLXq+iwzs_*EwQURZ!gL2HFWzC+-974Dp z%1)E)vDgdjDOV~&7XKNN z*eS&Bv0gk%ekWoCs3l)QCXdB48BjP2WMVBLaml!j9Cqe*vSHTtBe!n?!78`?b_&bA zQF4C}j*x5Dxe+OYRr%u~V5ygKVT!_wjB-&G z1suXu<>G2fIvP>38c-Ovq_23a!E-dZmZ@Y`S^PZ~_v7rp^5_Pi30mR4>e~Vk{mX^$ z$KtD2h^oHy&c9$4CfqdCUkjMXoGEzATb_VQCbq~InYDEmnp!AE@%37(blj7#_^eZ_ z$k*cbp6nqv(58b4@xH2S}q5g12WWR=-c7=Caiz~TuE5by7!HS1`G)khl~ zEwttt29&RAXTC(G-Hrnx|2km#W}-Qf9z%%b=mo5NdBe(r&&a-RIUD6UqkVAqvLS>n z{?!USWBui#TJolGVo2ptD0UJKXj+J3krmQK6h*6PF8@b60XiMyg9F^lBt4+>5FY<= zEIR<<44{sRH>-5&AIo-PjlqeE~p@CL23IB?+-Tb2?gDPK1gCFU@? zYzdbt2mG{$s0kllgmj$TTkRqpyELmQlADp3VKvv|TiKAcSJ`lOFVT%MWMVnMe5)#7 z4u{k9s%*;+0$b=LaCHRFMCHZo)(`L!=v%(yJ_7(Qbe1M%yad!Mrm0?a01Mf6pdJOK zDSzWFtzPjxziLaMA_a|M|53>leYhGJW%jl-OOBUd!05@!IZaSF7DbO0`9tkEngVN3 z$Y}RqpsqpJqtTWAq2=us;GyNEGr9z=1&dLmZ99EiVWDDB}Y4%Krzma*tP;8WrMo z3@I_FUgSNsV9ix-Mu9a(dBd($wbigXx*HQwxfKFe)SJu$AIBIg+m*;9PG-up(A+-_ zLxedt5#W~gj%pbrv0epoh}H7_R%HI4_u+>Jqmz!U*A$T*R@&7iAZTI}TfTyk56!yN z!0f0ju_4xOj39IBMNqTlE_9p6Z>jW2ic%3G%xzQ*4-Z_`xq||qIK2!HIToFhG4pj?IG}v4e)dG=6Q)X z&pQw!B=7&w_n_?jK+5-Cv`aqPK_E`>TrCfSRg1J&&SSUt5v&>p-faKsuKi({@^YU{ z;M+3p9*PBzqL9{m-|wN`cPmIR#Kp;~O0LR@1TNFy9f?s3~oH6n}XabkgFd0lkbgr{L2KR)P$v8`Kz?)-mxPTotge9_NTUy0skSU)Gjv;LV&T67 zpsfU~+vvq0$@4<5V=|`K?8PXru?wif&#Zv>B974DOO3@|Z(p*fHoajQib0UZfOCDj zzPxt}XlD8@YlinW>4?X%bO`xBpHDXI#$qb!4)m1Ue;uH%KJEmVxV=kkbeI>Q?PTU8 zX7ye?`!`k_{IpzeC!dZ63lN1P_r-dDH9Dz%)Sb2-i5_jOa^VdD4JHwFq49Ykx?$Q= za412C}wRy>W%d`!RVAbWJz#(rRTEscJhAoPz-1V-v7pe0<#VMoucTH}hS zQ*MLBpdAiK9?s#*x~;E_*EGoe+a2gww5;It)p#EucaH}!!SsAzmhf#D_2Z*Pz;okD zjzc$q@^;2^wlo>KG(?4>yVAz9xCX=vJh_Y*;t+HhJU6gEt88k%Z8c*!M$BHFW};`~ z7)cI;eHvWDDu?|L?8qD9n~=q$sIBI(Pg`B%G8CVw$S)8!@uYVjyd1Acs{I zeyKoT!B#8E6Gq1e#@nMKXvm8@KFyAK4g4xaZ*+|0&_V)DmOHav6)W*Ot3Y%Ppq)XQ zvQF(Jea<-!de#F3HWI9J|!ySa_;BF>cS!agS}jF6pBj?RD#i+k+c`+)b7aDW(Qj4W603a^3o@ zu;2ER=bdbhr11_#*9^JS@S4TZ~ZsChH6QL>G%HBYPy z^s4=VHXTKeh7u&f1pqD7mX0X84rABASy{1az$PEW!cVhVEM26@z)9S&`k|_mW$9g5 z&4CkWg&t5D8yp%=wG@}0UJ#vuLJ|WCK0Dkhd5+N=Hm=-&iGMWuVI(&^#7Sy4hKEhs z4nb#8P_ct#B?$GQm_<`?P@j*MBdop5?FY<LvsQzN$(Z&nZ7)Q4#U<(LjM^UGGQD1J&LDYfa;R&K*+=0#FSp3dr zrtD`$_7yr)_Nbc;r4#M6xTChr^IvL+4QHwKW22)({q3=_LHJrek|RJ4s&nqk*RwqZ zu+4MCD&4#uxY?^J?`)q3dwd?8TDf36*1~lWv6mPm(#I*iAHf_zt!TKu%Bj)@K8>w_ z^Fpk!W~c!%Mn=c`+au#+qa8|+(G--^NcZ&sH8D>E$gU8(r&^1s4UP{Ooe;Ul05>}U zA%mY2dr@)*EcY_f!JLpva;F1DsgE{2f&5pZ^~3`>#SjD*W^6x&APV|(6CkslJUMHB z;$voce|rn`TT7AW>)y~mHnt%vEISQs93IbLknyqhruM)v2Q`>P&IL?%4Im7x+^}(M zb%(j+nCSCq7*TS_S`H>icSy@K&^nE=&M*%VzQ)>}DbKWQo&*+6fG~AoFgHXPO(=U% zZ24(jWXwImT*@$t)>-pVN-{u74eX~u2~n<2;oe}lX0_TXa1O(7HEsQd`XX@Y+tdp- zm%w@}Z4b0+)YjXbo~ zRsY~{J6R@>Bk;oA8UihtbjxsYIl&!>;LCaI~~K3@n7w=MBG@&neQ zRJ2a#5TIE838C#0(Ow~EiE}Ah_hRd10H=kJ=<98u0ZGus1JioQ zju%_AB_PbYRin0O4Xht!638C$3uin)7*Ueh%YYHdJWaU*RD99{#Fz_?{D`$U9?J9+ z5=PwsQ)z%`*d!lc3Hs9dst8^UP+s~tz^z)SHUiGHQF#<#oDo5~k6E(}fI#4!wm|6E zfkg2}23ESW9H{MuLd(Q8043J75xfrIQ<4SFH|#0J+JQ}j{ex$%AItKn;a1pGfxWdC zh>w~HRHw}H{tf8qlg%M_I?uJRpsmyTpRg8Z{Zzr^ z1%BS3e7Z4Ly4i}J1%BRr&MH0tM^;bVoJIdG!njP~M~HIl36O4(v%iSC_}&`9e+8%* z{5OHzt0&fYINB)&;u0_AEjB2T5{v3KqEObMRM9#T?RIdMXkU)tR}9R1l?o6K7KbR9 zufjyQ&01>wCkc|Ax=7tSKuk>UjNn}c=DjrFU(q^M{1F6Q`G3`#9skiWIjKW`C7*D( zPmZHhM%%!9KwP5S3s9|JQ>)+TZDr#AUo=KPh=_N_-PWh9;AMd=LZHa0*gAqpHkDe& zaFs8(bV!!_fF8*^U0@V0!w5d8kZ?hiJmyJI-c8;Q0l zK~B;9LxA$tj||FJ=}ZW6hJr#q(>i|;8f>KZrzT{mPNS`!1P=WZa?-=rB2RBPdmVPq zM+2w(<%CQ;yB7#EP$W@HxBM3xb;SEIKt=sy0HxDU0M4F=axDr41|apH!p6v;g*pw} zM+MGhKZ?$2@}Jh?ZR~gKlPIFV#bwH(EHX=kv7SSd9*Uv3j_ApLv4TWDLm}mV4p7Sf z0-%)pB|uHd#|_HQ;jmu;JU5y|VHiBoNH3~LTBZK|V#-}9B zLK=d#ZnW4~_wf_xmzuvOYK8JQD5U0Z4azU{k(ZBZ>S?;cPj0h7W+WamKUPccMLQIj z{5$AN8=s#OeMk9Q;F$Q1jdkDs9!OH^zX8g3e*h?@{s>UM`;$S=ci5oh|J==YEm|e< z9oWiu3TLZkJxDD%H?2`1+1oqxcZQKVG&$$(NPJW2dVGU9CRDzK!v4iTXM_I%C>#70 zplt9rfU*HHc>Y-q!}9ek<2Tx1Tk-p6BNo&hJkt(Zw)+SfGOTl#8k&U40Vzx7gfC^f zz67le6jP&(DK6&=d+3KP-q6n&uJYjEnM2!P>&`U5Bn2ktoGJSO_8#xmd zUj&5!v*a`eCqO<0xB_)(>ogT`+?~bL*BGX2n#zOt{FSDtC! zhh;Sr{1o`X1iM(J(*#{DAbqsNrFS zrZ2LV9V8oQJOG7Tjc9H^YdMk8w-|+_q|`4$UG}8u4`eGtMd_#4`U_ckF2KFT3Hv&P zXz^+S;V`c$qS)IxI+MvhKM=TWkjZ{#|BBgwu;In;Vm7%_Hl;AMYSwrI?Po1v1($XF zBZ!ISktjGRfKavo$S~Z24|mvl^d#ZTcbYbEqTRXR2e)D?@i4^6kG4LtnE|k39fk74;Q-~Tzl-3D z0m^Gf7*rgIc+ZErk*VL4Q;iaXUZ$=8n8BD*CgC`s;#d(Qh+;{NYztT*Qygc5R{B8= zH2)NZl;A92BL~!1QZ};Np35v<$;?wIk3U&ssQCn`l4lbf4?VJrjD+JXpcbzJK84{Th{fA0gYk;a3P^E0(YqRiri5K|{uCFEFp zbb<$#by))E>?n+tyH)@c=aT^ThzHD{Wk+!c&)1z%@*3-u?sfxZ&-XgE<1RUN`X--F zTHHiA3xme%z(#I5nP6}e_glrq<|ee~(=qLGPI)cAs2*j79Z9?=XXz5}8)!`e90>BI zyXCu^2+`U8qNunyGNHae$;m%5VYn2RfdnaV8b%hp&o8b(w|a<(lebxFV8e#dRbi1x z*O65~%XDoxKUm7~4s~+0n`A@HPv-!FTytbZ+P(@#EI!!;8kNC8+Ahu9y8TJ18c8di z5Ic^+hM~9-jllrLjnPOg^z;dR4qz^?tw>Y|=)ri(nYDVYDhn|yAR3CBty^)!Rg?BD zZpJ`vj)hKY3?6t)CX4QnoWLor^jh8!WrcqE(weLqqeut>N&>i$5)@xF2%9G5i+pJ( z&1_bkCdCe6k!p2CvsW9+2&kChF{ zM=&r6jR#SOTkyMhFlxnUi3JRvL$bW>kaZIzpAb(I+66fuyC;|9UF9mlR9S8eU?SHe z>T+^DQj?1V15?UXoI9ypWhz(l(4a1tL=tl=^GyINu$L$>V)1hnl2D2Awbo#VFcdx9 zdF5vU4j#hmo|71(L0l9{$7ca#8YtdBCw)3x;08^LDc?;fevkT=Q22-dze$v&r^rjs3hXv!k@gbq(ge zhOU+{FxGS4E=Zd=sO}9WVKg@8(n@eqI@0sqFOYD(q3*U3(Z-Ss!f+2P;kxl{uu(`1 z4Ix38gMAcid$PtrP==r#F9h2p5MF}1&)|)hL?LMxH&DT^%%PY~dO=`IDoyuPMQKD& zEUnBx2(Xqq8rX9-B$x8zKLJa7dzT;I$CeO&lPnj}2qng7t9&uQ#0cEz`#Ih?KKNNv zkpsPnGPjqH@k&z&$6JB&bkCraN7zvwuFQ2aU{~FcWMI}9;1zQ)!l^KVPBh#eDM+d7H1s4vnKb&8(cMTI2qU%m0$i6>#$SGD zr2r%4{*MBru-O&qlGbRWqqc;3>JtLdQ)d`bY-Pu*w?%z)8`Qfy7|6`%hjFT1OR98( zmM+u}^XhkxS)g2rLTXn0}L0-0cbkOFz*Gmx?vZx`Q**K;j=BN+jB?U{MdW z8kOQ=Hjv7*@lWyFfd5?lQ~W#*-@bqBAhR9!Tph@z?zxSMbH3gl!7m%wxVq*Zo}?SM z%00ILxtn{wWX*|t@V(6B^M_*12Q_7+SXaKJY}{VTRd)b&GFL?c+Tq4Jy{1QpmPNbF zs)))g&=cx%An8532^L1Wb4{o>=*v1Ks*lu&kj9PXcAR-vpeJYQhU;FMh6eju1ix-z zy7~1UYfk;@zW>^mZ$afL^5J};Yn2thi7vVFK7y1iu4)oa zNx@U6xp=FbksRyWOOGRwJ-u1aZ=P?LIDlMN#^ELE_2Fm>>Cu*4d=9rAx1|=L<)_hC z-vKFEOtYdp`O4m!K|FJPuI4{*^(ceG6+par2QO@XD8IX8jm_-DcJ=tT~xkwa+tS9H%ae zg3>^XKzbom&VLP1;{66--BZU$pC5w$g(MqIrhZy;p|_r!U>(m=qFmm3$9wN%)|M}& zG*5zsr1>2{84Gu0@gV3#LT?djH-KMpK#Qr}9|7ti&7S~DJ6zMb=iPrc zs63e;%;o!`nX^|DcQvYZ1lFY;ZqDh&Y%!)*`gFMsM7Y_#`+`_3&yf6dCS{|<${TG8 z_ZN(46D{hIyw!$L#cUAZeP4NoNuY12%QJe>cLj-)dkZpUYk|8Q5S`Ql8~1Jp$*_wy zqO{!UP@>#_XP7Uq$-}ojWLGdM$4!WlL75yv=rOL8r%;yx>rE&&=&|WRz@k(o7u{J1 ztHu-#Mv)3^)uOaQ4E-kt`5(~kR+BW4I^J9A7D(~|2qy1C#LQ9CRhc{52NcUaDli8L z1yYd%WFQr6<}R#gSYvsSBE!J^0n}Ha*ux55HZgkg2cUk*+nwkiMehn=(sQ_YITW>W z)d48wV;}o^P84HCKA_xOdw9lEq_r^m!=Mxb8E>F4q|3{LD00t6;OXLHrv*-LkI_t5t9ZD4saii>Dw-dJ+J7UUo^^GLuQJa4D{0G&X~lNDx& zk!1F2KKcu+@**KY(1}P+jRNylQ8qj{H14m}kLDQD;MHL_WuGg!Y=u61G0r{7Rcf*n zrrjlPUERCgRF}S$>0({+W)$5sP7yJpB4Y0{VK!NUqf2H0RMJowz{6?sC1Ev2P&|G5 zHiv$0=hFq%Pi0|U%lh+2*jjU^b6zuStA zki;&&%6B?UytkmN}tONZkt!k+S zR!vb8iCn5XhJUC1bM$gOa<3!q>Pyu_=EjOjz#!t6h91Wh#L~D!#Dd z$f3^oW6!SJ7);W7RMKF4thI5Zuc^mtWu0ECR5L>=UV=4z3eb0NvQE$n_xV@YcUQY0 z9*g%|A*%W$INt)?f>%@V+*2X_Wepg+nhB7Jjp>APQCQn_p^K-e334HaIO!=@tn0J1 zDA%qbr==>}@M=akW3(n=`uCn`wL8Yo;S7wNI2V_}@gu9O-$DuuQdfCzmgt5{CpsKG z^d{qV-%jBxG@9LjkY5K_v6)y-q$g40NQ?qjzMPh09og3{ZBd^^oy@h3;(dJaE)Zc% zVhiDBwe(Hri6K?bN3o6RfG)&u1=GnEQ5A(P&jJ&J0E71M=7jWe$=;xIKdJ{$<_93a zl#`i%GT*rwRYw6?Xi_aj5zicoX_|`(sJl8y($z62kk+cjoE_NZGR~{R(Rid^_71XI zctby=o9CkcLod#nncHH~ozy*giDdSC{ehJN#p#j`bJPg$5!)VIiIFR;B?!Io0LJFG1 z{}Yla$nR!F#vIyZR=ap59vH?*R-%GQD(vtoMQJBaMvG0Bici2$Bp$_sUYUrqb?yGv z#r!K$oD}PF}Ke%X{_5o&j=4 zpjc-`=Kl^%ajaD)CY^BX>$20XZvjCQ3wosk(Fy}y!Z;~{uZ`gAB6u=TPl1^&cLA>W z(M^E>a%&M{+8tC34;Aj}+?|0>ov*R>poQ(bcYGsj1SIdL_6LXLB_S^JkRsok`i-MsO7Tie z;HKEh>oc|DwnhhH-eu_2l{yB|T)Y@#xz-Q*Jsr0dbnecY3m!#NS}%uVjg#~7j#B@K zoi4EfV2l?x5!5BkU(rfExL;j`YNl<$P5_}-vP(al7Pjj$*zjC zffsQV5=8YNt;?%V84p?C8TzdeJTHQ8L%%jrZwL59J?y6bvL9n%S1 ztQNKGeL{Zh90zV59n+?S#1w<$J#6HPjBFMrqa6 z+sqaZyo*gUd+}=q3TwnXu~6pJ!>&qEt;d0^+jiXHpqCFAiw^+Qec}fJ$^ah%ICHKQ zybf+or-!j$(ckdsH@~9Ntbh8lH6m{H+^9B>BHC4Bp^+x~et_9X&IQT6t$RfMyyD^a z7ESDT@#TROXhF1m8QMf05Ua@Gs5E!;xSXPKAK2VGiimYaUv6XAB8=0Qk+p9+xUa-9 z%A|wIDUt?~{bs)kUSyrRNbKgz_zb$(VP7r)_vqUujvjizR$K{?8?xdmfO6s00B3SC z(;$^qn^3X28;V1_^&m=`yTP{QAy(*vP@Oapw#`F8B&qM>ZA`)RF1`fiv+e@saAC;U z(bKTU(TI9;S8unES*^ovScc*xNauhHeS4buz-AE2W@@eR(Iy-5I+g*U_-B2&VK;Y$ z4#l+?sj$Bepq_$U4=@RPw@+fgz-pPkCTCXfN8P{H+GIdBrl5_xGn*iaRGy3VlIvph zN~X?UE*~AeOM%+7k3=02xJ1;2#yX$mV9%?`Aq%sI1nWKC*4Nkw+1fqQ?zHvf2`8@W zdiZ5?*`*Zr(9FzmiP@RL9lG((Hqiq&0+a_n2T)Oa6Trj+uyS+2&*}aHtg0tvpN%!!}M|wBywXg&)s4OnVW0KhhBs6wk316EMW~JYAU+t+o(%wKzx>`kdf$Q z!H_|{c?OW^sjwFPi?vJ=7%_WwTZx`cU?e#V{%M|Wh09^L0aP^H4p7nXWq|b@_6}=n z;)K(D=R7Opfw##XMU0+BBEL(^CiXVX)4X??BpOT5o8~K6U_!nU8uQiZehy*V(_yNP zHT&75E7+^+6haPmSpqoxyWxBs+dRFpYH=qTWvROWDs$ZpFqt=(S+#k&kH5>3`12;v zydgK`l*nxl8@#O;YT1xU;WO)k&*{iI3lueYw|HJ#L&O!lJYjdQsaGHkv_Q0^7j zFrhR*W<5wC+8>mAL|a1r^1~6mRaryvHQ?*PF|ErB3Ys`%q40h{wjz-aqdBA9EjmV* zI4IG4dTW3ilX43%d+cBHDwB(vmwP30c^^YS{(+9>Er7c4U!3qajOMMtV=~jW3mXc@ u&d2^8)|BTbuDAd3!M&!XioI%=39?tm1=z~sptgIhHE)fqJ`Vqj#s2|a=@8!l diff --git a/src/kernel/kernel_decls.cpp b/src/kernel/kernel_decls.cpp index 5d2e2efd5..96ac9e016 100644 --- a/src/kernel/kernel_decls.cpp +++ b/src/kernel/kernel_decls.cpp @@ -21,6 +21,8 @@ MK_CONSTANT(refl_fn, name("refl")); MK_CONSTANT(subst_fn, name("subst")); MK_CONSTANT(funext_fn, name("funext")); MK_CONSTANT(allext_fn, name("allext")); +MK_CONSTANT(eps_fn, name("eps")); +MK_CONSTANT(eps_ax_fn, name("eps_ax")); MK_CONSTANT(proof_irrel_fn, name("proof_irrel")); MK_CONSTANT(substp_fn, name("substp")); MK_CONSTANT(not_intro_fn, name("not_intro")); @@ -60,6 +62,8 @@ MK_CONSTANT(congr2_fn, name("congr2")); MK_CONSTANT(congr_fn, name("congr")); MK_CONSTANT(exists_elim_fn, name("exists_elim")); MK_CONSTANT(exists_intro_fn, name("exists_intro")); +MK_CONSTANT(exists_to_eps_fn, name("exists_to_eps")); +MK_CONSTANT(axiom_of_choice_fn, name("axiom_of_choice")); MK_CONSTANT(boolext_fn, name("boolext")); MK_CONSTANT(iff_intro_fn, name("iff_intro")); MK_CONSTANT(eqt_intro_fn, name("eqt_intro")); diff --git a/src/kernel/kernel_decls.h b/src/kernel/kernel_decls.h index c94c8c953..5ca3840e5 100644 --- a/src/kernel/kernel_decls.h +++ b/src/kernel/kernel_decls.h @@ -55,6 +55,13 @@ inline expr mk_funext_th(expr const & e1, expr const & e2, expr const & e3, expr expr mk_allext_fn(); bool is_allext_fn(expr const & e); inline expr mk_allext_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_allext_fn(), e1, e2, e3, e4}); } +expr mk_eps_fn(); +bool is_eps_fn(expr const & e); +inline bool is_eps(expr const & e) { return is_app(e) && is_eps_fn(arg(e, 0)); } +inline expr mk_eps(expr const & e1, expr const & e2) { return mk_app({mk_eps_fn(), e1, e2}); } +expr mk_eps_ax_fn(); +bool is_eps_ax_fn(expr const & e); +inline expr mk_eps_ax_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_eps_ax_fn(), e1, e2, e3, e4}); } expr mk_proof_irrel_fn(); bool is_proof_irrel_fn(expr const & e); inline expr mk_proof_irrel_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_proof_irrel_fn(), e1, e2, e3}); } @@ -171,6 +178,12 @@ inline expr mk_exists_elim_th(expr const & e1, expr const & e2, expr const & e3, expr mk_exists_intro_fn(); bool is_exists_intro_fn(expr const & e); inline expr mk_exists_intro_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_exists_intro_fn(), e1, e2, e3, e4}); } +expr mk_exists_to_eps_fn(); +bool is_exists_to_eps_fn(expr const & e); +inline expr mk_exists_to_eps_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_exists_to_eps_fn(), e1, e2, e3}); } +expr mk_axiom_of_choice_fn(); +bool is_axiom_of_choice_fn(expr const & e); +inline expr mk_axiom_of_choice_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_axiom_of_choice_fn(), e1, e2, e3, e4}); } expr mk_boolext_fn(); bool is_boolext_fn(expr const & e); inline expr mk_boolext_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_boolext_fn(), e1, e2, e3, e4}); }