From 66553268d0476785bafcbe1afedaf377cc63ca4c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 22 Jan 2014 09:41:07 -0800 Subject: [PATCH] feat(builtin/kernel): add skolem_th, we need it to justify skolemization preprocessing step Signed-off-by: Leonardo de Moura --- src/builtin/kernel.lean | 15 +++++++++++++-- src/builtin/obj/kernel.olean | Bin 26580 -> 26954 bytes src/kernel/kernel_decls.cpp | 1 + src/kernel/kernel_decls.h | 3 +++ 4 files changed, 17 insertions(+), 2 deletions(-) diff --git a/src/builtin/kernel.lean b/src/builtin/kernel.lean index 6af5c9be7..97be45784 100644 --- a/src/builtin/kernel.lean +++ b/src/builtin/kernel.lean @@ -211,10 +211,12 @@ theorem exists_intro {A : TypeU} {P : A → Bool} (a : A) (H : P a) : Exists A P absurd H (H1 a) theorem nonempty_ex_intro {A : TypeU} {P : A → Bool} (H : ∃ x, P x) : nonempty A -:= exists_elim H (λ (w : A) (Hw : P w), exists_intro w trivial) +:= obtain (w : A) (Hw : P w), from H, + exists_intro w trivial theorem exists_to_eps {A : TypeU} {P : A → Bool} (H : ∃ x, P x) : P (ε (nonempty_ex_intro H) P) -:= exists_elim H (λ (w : A) (Hw : P w), @eps_ax A (nonempty_ex_intro H) P w Hw) +:= obtain (w : A) (Hw : P w), from H, + @eps_ax A (nonempty_ex_intro H) 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 @@ -233,6 +235,15 @@ theorem boolext {a b : Bool} (Hab : a → b) (Hba : b → a) : a = b theorem iff_intro {a b : Bool} (Hab : a → b) (Hba : b → a) : a ↔ b := boolext Hab Hba +theorem skolem_th {A : TypeU} {B : TypeU} {P : A → B → Bool} : + (∀ x, ∃ y, P x y) ↔ ∃ f, (∀ x, P x (f x)) +:= iff_intro + (λ H : (∀ x, ∃ y, P x y), + @axiom_of_choice A B P H) + (λ H : (∃ f, (∀ x, P x (f x))), + take x, obtain (fw : A → B) (Hw : ∀ x, P x (fw x)), from H, + exists_intro (fw x) (Hw x)) + theorem eqt_intro {a : Bool} (H : a) : a = true := boolext (assume H1 : a, trivial) (assume H2 : true, H) diff --git a/src/builtin/obj/kernel.olean b/src/builtin/obj/kernel.olean index c927d1ac2e9df35d53a0851ab4207695668c91b4..d588daba736cd2dd13ddd47463d08f150663d8d6 100644 GIT binary patch delta 7223 zcmaJ_33L_J8J;`yW?p~?CMF>vA!L1ogzO;@APJC=KxBuoFCjpXup?NhERi0I34tK_ z1E}SQQCTV~s4Y@Nl#0??fog-GS`ub~ ztt2WPI9o!!j)mvY*`%3LINcj5W>T4VR>DHanLN43fr|knn7ibacf5ZTqK2MM9+&YW zN8|wqu6Cqw4ypn+-Skp? zXtcf^*dqnGTu>R#NWV-S=SKH##&kIdlF;u0noz!EIiBJ{NerP%SG|Jn>d=km^@{e? zV^XcyCTi$4P}I?>UV}W14tp!zoia&mp_-Ht#RRsh2s?9go$RpWl-L1sB#BpS3xvg9 zP`59NCc2rDANd$~%FN?DtrY60EVYN&N!6*t<9`Oeifb3co|5XPB@qK9F~aCf>SA3! z3VQd7HzFaz%cs(pg~g_6@!gR>y! zmd3IHj4Y~38@j-V#z3VHZmyi41D00K&Jc@{i*d7Z4yaZUs9cKA1<*W>I6H!j5htfH zX{1u;^f-}48R?N8cF8u4el$KkGn>u(Qw{VU%}o;m6C7fNazZbsCwNqupk|cO<@Eg6 zmmwCAyNc2mK?U{8$kt`?7G{*i9&RT(6JwMHPh%#X%}5NsZ4WiKN}Tk}GI5la=Y=KB zXDP_K)mlFRthqqkiQF!~qz#z`y^n!oA_?QJMBg?sF7$VfVyH=IK|q*)oB2a)tUH8sWLR`C@g1X?R$_>9gEJl z;TeYhNR6lD*l6)B#ZykOywbZJZy4J<0^UUl#>%^+6p&#pr>L}~q_LMxff=akbKK&$ zVbA)<>P%8wk<*4rW49!Br!X_XvF%s73zTB6l7jw=cnMT3okzDbqv>p3M>?C^$@>9} z22}nC#=hDbM^r87zqv8;oQvr*LVU>GiM}wDsOrvNLrp_l`nvOdYUxwty#P*t`FAmP z`6}?Pst>vH7Kw}8m#uQzP(s|7++;2&*-d|*_U09pUIHh;>_v?IW-r352m()ap3^#= z!Bm}BPbqyDh)?Kx-$?N(9q2n$Tx0w-b?8?hKBKaJ#o`O*+@h!ZJ?XgtRn=R6m+UZ_ zogXY7rWN^_;smwi7kOF{v4)exxI>@km*_5yvigVj|0mc=@slhCDM$+b5VK|9KS zUOiV=RnzO#QWT+!o3yikx#!;yQAYmb_Z~(e12V-j8Zw~BGoQV8g^@edFrXwS-p>%> zQ0{C>q6Vm|O684%RdCIGYzAK6oC3LzVE@%eZ)?IA7BXubp?%`Li3Mbfa`X_~j;wyTy zaDN2Su{}pPFp_GEqJq{dYhBn{I2|p@$SH2;T%{c4X!4s#x$7>uu40NBlqR~-ut8gs zdq7NZk$BJW{Z5Yqw>xv=C2}>P<_*aZduUr#80{Mp+&>L7DvWeMl~#sCu08F#Pn!+yF;!PD*R?lwC@zlYx4E*x zw}keooTA0WvEmeMF7BUo%6A(>5nV^Qa(yJUW5@$kG4z$lb&9?%jthEU`OIRUxfDDs zf<~2i#W`A8GPD49NOk$q2LLKpwhm@IH$4Z{>eKJ*HWwv9;g@J;3Mjn%=P~E;k&bejcV4?!I55(L+3^&h>dh>WLZ(YrB}g-y6hq> zbCbW=e8QM~ZQz-P_A|70R7vq#yf}iOxy6!HU&~Mu&C~WQGV3umaK`h3X&!aAyh37h zxQAcLMxvZFlz-^;V}n1nQ^4$ny;b7xzpCYYLiTmGD;kLlZc12``EFV=7ZJa+TAT?Eh3 zu`%7obDH*t5l6${B`O*|2m)5JPMR?{LW)DyD%yvP`Au|bLKHnQF=|kwZ<*oV78 zvhiMv<7q(X>K<-D_j@f2=4Kc%+9zd~OwYt@v-~$VLqx-yB%sgm+Az0)sEW3g;U%N= z2{BVK%avDIZ*A8CS1{(i!7BXmW$u8^%z%$diW z^}SFF*`o($bPwkvRejLyzL%Sn&D~45Gf`EF_pnkFnY13m1+f-qlGPoPl>bQbI zz8i2ktS}7yH917HrsgJv zYdr-|3(t5E0x)Y{@*REXWs7}wRJHYq7&$ayTC%M2nrWlNt1{Yfx->0Y-Zq1$cOCvA zv_`Rc{-{+^y#-wbPde~z2XZ^BGwYP(TGh04dQ3`T-B+l_qo=x#Fl!KAgc5Z><__7#~s~y@5mi3@Yjx{5hbyjDG*Hj}*n>9C9bfwq`22-t2tZEQ!0lHhY~Y;zUc23vJnLhSJMG$y zXH-$t=Ti*yRge7#3g>-G#*G$coWyisr+s608c%SiePl0;Az!%jmhpbKK0>=0xcS*3 z2LW=s865zfHFAf@q5E!ojocwrT%BPxOP-6Xr@JGlvATahE)y2wfo$lzqqvOfr*kX- zUol)au&Mzc#y99rb(N%g9VeM~^?ecCjhgYX;Zk9=U1WD8R1gUVBEOFt z=f~=XhYrpkHT=4q($NZbBSlMOMqrFuxTB;NpEa%>PA66PN{)8Wus__Hbg--|O}jTF XiG8T1gkLv4+H8ZqvRkzE-qQa8`k%_I delta 7088 zcmai3XLMCn7QW}U0KNc1LVyrbAAy%Z3MC0rLK=h;N@5_O#3XB#87%Z;Y8GA3AJcuOab&Ute`E4i$pm^ByF{CX9?Ps6wyXs&9hZ> zD(Uv_<=|_@@~1xp)VH{P9{!5ksKh%xVK%VE@^f4`7ch#sbp#)i)EHgAMpsj-b2+6-^>G#yWw;YO%kVh|w1uCROFxttV!8)-RB9bZq z#}fi!PewGo)-NrCox%u92FG+Q3EZ1OIPfwRDfLcE@Ni`8+wf6&T6XLc5VPDQWn&EA z_-ka-Gie#f@`q_fu}^^&Bsv1)fanM+Oi%21&e7DuoOCp&7v*ecMJ!$4!B7%oG>9^x zdSM-=G!rB&k=yA>x|}{FfW22Vt%bb{6 z3$9TI0j{412{7t0M$0KCXT@kFvwyyK54b_;%1SvlR{86<(hUl&VysYBp~I~c8yJgxFga4r=nX4r;iV`oDQT=_RWO59{f<`! z96Pgtaj0X}j4R;X$qry>3X8R#2;Y_BXq1#>8V^#pfm!)4V?HRQkFmTzrpE${RqHf@ zXH_2=bwmTlr70__feusDpkdzE!48UIC&qyzV5iC(EgdvB z>o`k>_}ML)hSK3SZDn;3XIs2RJ+g)sz6nl{mqQo_yc~iT(FQ!#h>Z+E!a-E3>uF0? ztvEr~vb&1oa`P03Q;bhY97PXjd&L>rpPeV(XYN_vUMV^2Jm+CTowpxR_|P~@4&^rZ zBqvR5qo~2dJi8G&A3?@>sv4X>(YO%c@Zqb4Lr44*V#?5`F8oYF;{rNHJCq2@N8<_! zj2~6%&uJt&cG1Nr6n;yw=UQXseeOhdk#-Cz3m2DM-ODnx7sYuxKD1z3 zG6&H|PAZ@3QHqC&S4{iZ<_2HKj} zRnonAv0@#a&g&=EP~6N2iplRdI0mxHvOJLdYrr{Vt_e-s9pL_v)24TE($<4o^7BR{ z$Qj29_jhP~+XG#%r9(80E8Yso@oy)+ASZph?K}+G{U11mUdX8UI2@JZWXUwQ)7*l% zw$H10;+=Ss=weY6ysUv{0O+dx~O{`6gnX#^ecvs^f$b%P{_% zBw8$(@;p9Llq&kjD3|3m^9l!IQbjljP(_#ps3OD-#{3Eu=Zlv30plYe&9rl5rZ__9 zMox_}FNZjNS4uc%Wj#$9)mIGQ)NCHrs|8PL^DFkA3n}HD?=H%F9=IMhh$G!}6x1ck z+`|`f9lJd!U(U1Ec{rJ0DWL)XLFgv8y@x+Hu6UqGE`pSbVx&Y?7mjT-V0VV&02Am> zqkXfIxOX-wD%r{}KRIy*SiJ&!gOhLFARlsBqy_hJAQH7SfclzOYtcv7gqAEfVeN zt+9~_{A#6+7Hn3>NTt%mcq~V0ECwv@$t1@Bp!D5+xN6NTQX=%2rATlvUDMbfGaN31SX4loSoC zw{>-|-vluPYBdCEz#&@oftkk88TzIqzos5*Xamjpwxl}bE#7Dzu5+s#JC-ok@dV>) zX&!Y^c?SY|TA-9lnC}P%mSD*PcKpDb16xuv*iR#UFuq%Knk9td~O8vg@5%VEXUvXX)(;gIX4VW6Gac#=-I! zEiRUYM6mvPTk0*z*;|B5z#?;xFJu&Cna>`+9RjdHju|@{-m^i_W^DJ zSqt(g*K~t~YR{rUt=~Iu=z0~sF=>5%4Y&3ZIpgdsejic$4IACz{>p`SgSm&*S^)Ra zmeTH`hW3{F0h zXij+twM zPp|S2XjqjW4}3ih!i9O8rk6)6%STax5-tYsrK6#FmP+a%;_0)n@jys=Ovz+F*29>7 zgwBXF z$(6krKfOmJAEwS5v)|HcYCEN{rOI|ys*nH;k5$7562YyA-gcZk=t5Oz7C@Aaz(YXl zOy^ZqVbRuQ93Se#0Lx^dQn14}`NS=!JVk1RYOzgB9F;&$-%GxK1tlnps|91qVxvzk5ZWXL_zAEv<6 zEUaIj3&>?Y>_6IY0kqqI-%e!@5F$nwdVN~5%+|$e<3y{Bq9|sMlPUb+vh!uc+AF2) z3|cxhw#A9&1sG9h&tHJlDT6k$i*E=l=y7V}ptW-(QPJ4l05`b>MXuF1CXRbBI?#C< z!!G6CK1Mvt8OzU&q(l9~9xM%??9`UsXL5>g{c+-Z(S?Ux_>v1z%cx&FYygBdJOCa>QtGRtiDxZUEI8Olbmkg zgH=R&C6jO5b`veDOc(QLM`c&hL`N$VbCe!u2I=FYDic=hrhpnhvba;VVg4O?l;ZE0 zoxqm{b@S#cw9W~75BjQrr)b{Hh!mVGHiEG?Z~=F)0LDDiz|&Z&N%T_N&YAZ8u%qD> zj}HR7-v8+@7TaEZyz9%e>NV~trB_8pi~|Q5vK#$jo}`MZIei;BtTUKadB!Q{yga-Q z7?kJ7>FcUKVUHsk`2rGG-BmPFPIZj>0yY}Ll^}in>3_l>TCq~Wq!QyXX9(?XH(`eB zr@pb(V;nl;kNdQo6Jk-Vrq67iy>QXOO8Rm}d-|xlcHqZQQ>*v~pvvwL_lxEWCy2a_cu z=;dz->Y)t);XQT4E0Ox}87q;wlxk;;>Q{$(^q9E9^PCinZEko-x@Xn}`e4SqgahEI z&iV#Wt@v9&wc_v4S+|{&V;dXNJ|EIqJfqT}-mcn1SGCiJ64?9vg;PD%irL_vy1+ff zZ0@N8{@PrmwzC>@_rS&hZY(}?Re(Rhih3{n5iqDE-^-zW$zPK1Wl6fx+p{8jHcP(w z-)eJ}%sX?kI7_&bF3x~a`xj(USD*Tkd%pgd@1l-DZ_@A5qB}ENc;oXwZo>5I1;R`z z?>uPzVO>HN`Lb)OxI*gt6I2ih2Vyq6?SOLXEv|SOr{-t!){gU?#2lYZ+)I4sm{-}9 tB=#@T9-ld~UCxb+pk1|XMQ7Suo17F08Kncy_Ain+ivDU`CTn)#zX7unpt=A6 diff --git a/src/kernel/kernel_decls.cpp b/src/kernel/kernel_decls.cpp index 5757cc3ea..83f6f9fda 100644 --- a/src/kernel/kernel_decls.cpp +++ b/src/kernel/kernel_decls.cpp @@ -70,6 +70,7 @@ 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(skolem_th_fn, name("skolem_th")); MK_CONSTANT(eqt_intro_fn, name("eqt_intro")); MK_CONSTANT(eqf_intro_fn, name("eqf_intro")); MK_CONSTANT(neq_elim_fn, name("neq_elim")); diff --git a/src/kernel/kernel_decls.h b/src/kernel/kernel_decls.h index 0821e5c24..75f1167f9 100644 --- a/src/kernel/kernel_decls.h +++ b/src/kernel/kernel_decls.h @@ -203,6 +203,9 @@ inline expr mk_boolext_th(expr const & e1, expr const & e2, expr const & e3, exp expr mk_iff_intro_fn(); bool is_iff_intro_fn(expr const & e); inline expr mk_iff_intro_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_iff_intro_fn(), e1, e2, e3, e4}); } +expr mk_skolem_th_fn(); +bool is_skolem_th_fn(expr const & e); +inline expr mk_skolem_th_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_skolem_th_fn(), e1, e2, e3}); } expr mk_eqt_intro_fn(); bool is_eqt_intro_fn(expr const & e); inline expr mk_eqt_intro_th(expr const & e1, expr const & e2) { return mk_app({mk_eqt_intro_fn(), e1, e2}); }