From 4d25cb7f473e14f5dfbb1e59041218fc93709c26 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 26 Jan 2014 18:52:41 -0800 Subject: [PATCH] feat(library/tactic): add simplify_tactic based on the simplifier Signed-off-by: Leonardo de Moura --- src/builtin/kernel.lean | 3 + src/builtin/obj/kernel.olean | Bin 28944 -> 29094 bytes src/builtin/tactic.lua | 6 ++ src/frontends/lean/parser_expr.cpp | 20 +++++ src/frontends/lean/parser_macros.cpp | 1 + src/frontends/lean/parser_types.h | 2 +- src/kernel/kernel_decls.cpp | 1 + src/kernel/kernel_decls.h | 3 + src/kernel/metavar.cpp | 4 + src/kernel/metavar.h | 4 + src/kernel/type_checker.cpp | 8 ++ src/kernel/type_checker.h | 2 + src/library/simplifier/simplifier.h | 1 + src/library/tactic/CMakeLists.txt | 3 +- src/library/tactic/register_module.h | 2 + src/library/tactic/simplify_tactic.cpp | 116 +++++++++++++++++++++++++ src/library/tactic/simplify_tactic.h | 12 +++ src/util/sexpr/options.cpp | 30 ++++++- src/util/sexpr/options.h | 10 +++ tests/lean/simp_tac.lean | 8 ++ tests/lean/simp_tac.lean.expected.out | 4 + 21 files changed, 236 insertions(+), 4 deletions(-) create mode 100644 src/library/tactic/simplify_tactic.cpp create mode 100644 src/library/tactic/simplify_tactic.h create mode 100644 tests/lean/simp_tac.lean create mode 100644 tests/lean/simp_tac.lean.expected.out diff --git a/src/builtin/kernel.lean b/src/builtin/kernel.lean index 2b92e86c9..93c9252cb 100644 --- a/src/builtin/kernel.lean +++ b/src/builtin/kernel.lean @@ -173,6 +173,9 @@ theorem refute {a : Bool} (H : ¬ a → false) : a theorem symm {A : TypeU} {a b : A} (H : a = b) : b = a := subst (refl a) H +theorem eqmpr {a b : Bool} (H1 : a = b) (H2 : b) : a +:= (symm H1) ◂ H2 + theorem trans {A : TypeU} {a b c : A} (H1 : a = b) (H2 : b = c) : a = c := subst H1 H2 diff --git a/src/builtin/obj/kernel.olean b/src/builtin/obj/kernel.olean index a8fbfea5d8dce00f3c96465c3aa63ee4c0231db9..9eb02226890703ab1f5b10d08a2239d43d896108 100644 GIT binary patch literal 29094 zcmb_l37DN#dH$FC{}(Y4F_b8aiG&FR4Kc_fY9a)|nbd&jP`jWvGsztonaqUA1QHZC zgc9wewT-2V0un%4ZJ{k%)XJtP_NicPZC&cdX05FYpe+j6?|t91-G6R|#HaH-IrE+E zJKy=X^PT0NOigr0CdbAnx|#dQw@!{<(4F4W&5EOlQTKsi_I8WpO^bb$nuGd@{>trnh#pkQ*DBFzm!OX=v+WBrDaC-Kq+| zl%TF)sU@w`r)EZG#-}DxkQaA;lodyo_|+1=scE7^2@%vx_hr5+M)5nVfOH9hm$(eF}`W@#CUfL8uz26hl+VYRNeElp-r2! z!hYLNp7##3ip)C(RR>9&)~+s2=GZ1TkF;Go)^m=M?{m@XV2WoEz&63f0OyG@1Aq^L zh^PVV+XglGIn@3&$+>UG)gp-OI#e1lJ~qY zF59VE;8;cubhnLfnb|@npzz?jcy(k0N;s5Qa3ou>U>U%pH1E3DhMZ>u3q_lFJT=+f zw0UNG90QGoaXG+)4=)Qx2C~LkhmdAk&YYVSlMY8`d~#-bDq;!(lg7P({pXRwm4GEL z3f!;`TE`wz(WE539BQ5y)(fpX&oOX!Q{YB*IGXQ|q^*e)jCHl01Wx6{y(P!2JXmAh`@f%RkxK)

J+lZgV+3gf1eX8V;1TfM^KGBC>*=hCKUDvhr4LKNx&$ z>tuIZ&**CcOUVSIXUs~RV1RRZU7VBEfYu>NhA@(&5QpOQ*P>kq$#NCO-oqqt7gzd-0T+2M8fHzN1O^tQNr>DD6QQ?sOU?510_9qox>@jq$ z&Y75zXr`8ssF@nqg>0S&W>GeDc!@D!u1+0k2a70=H=jwv2+69Jop0qEI*NSz1AS{<17UN zCvmkPZ3&~%T{i6*hQXjIa)&d)6Gnz}$bFE`CprpGes()bSrsO8p_MoR%#5Vmr|-&M z539t_8wQZl$*lK|nY^Lz)++cWG!d)c4Dj_F|6+h|ID#S)yCYApMqP09izG*QEN@4C z+80@g@qE*Ho#|=Qaa&PFwoc4s;KI!G_yyx56lhk`IbV(;Meh%K7Ng zVwX$UnczDCYHF7PWUJMlq<2_}r1zSfgBHl1% z(N}i{E0@zREq()NMO}y#l>G|D()XfywUh(DIO`$)4i>&04YIqCv@td#?M`=MJXv<( zbMeD9M{D~ZATJh@L#?GK_zaR;kO(25dB8fpX>(_0dSnvbHJD3~)dsYKw{{kKa}b(A zYA(a%l;6+B1pg?4S48lS0p838e}~+T~japAFw)4ztO&Toc=m6-$N>|1t==7 zi=gb84L*!gkS6DOb0kt+jiiF5qL-`)4sVwgdr~K-W;*!C@L!Wvc(;t$xc{ObloR*} zP*zg19xZ+p6?cV%IvjBK)#69cSX%s705#_u0Y0KRL<;D3=4nm;3$$n~34duNazvZ7 zD@Bt&ZfIf9==l-(5ZU_I>_YHwBKWre7qawbfb#>lhXzU%zy-P$w*x3Rpqnh?mdFiL z7ORhJp4x&2xdq3L&wg=4xQr?r$l_+1<9zuFVDa%Kpx%}6<5uFvkcXe;FoJD6leP%L z$JrDu6+_I!035_Co zlOv-F@<`S~pcGkm02EnwM({HR=5Dcs@U8Ve#knIFbUWQ`o2RopNH<>qo|57Df&uix z)WiYhgiI@BD7J632aLI-QnHFgeFa*Fp5p$!^6YccVb_`a%T% zfvt>Wab}(vjOe{sNnaYP!!!8 z!7rh~i8eUhO}+p%%ZJ=v{)?9J3OKoOb|e<%tC&yf2Nd&2$AJLdf)4PXk%)wUiQrcN zN(cW{pxKLGkj?+WBXp!~}5Fzm2G5R{Wg4rf$`FTmn zPI<2{GKj6whU@>3YZ5);b_xmX$+;UE_MS!AwdhKp*G#+!e_#!K{9xxXThr(mg7ZvT z157O>(&nE5l-T~qp#0t1_W_+XK_Z!Hoj(o*i9BVHQM}~Uv(bj~2|nqkRw7An*}e(U z^T}w_|FDNF&KARaC~!=)mSTCFT?sw`P+I>aK+Wlw02d#L^be5`ffR<|^~de$Rhr{FVwVI`i&UE5sk#$ia+uE=j>gQo+$Dawp!MGERO%53KVKBGPFUn&vau6l3Q50n{{~iToYjH1aEG>+@*lH=vbR28gJG z2r))fvW`)|my)#p`HfL>oI)Io(TikC?x}{vGmOxb4gg)WtNhmhYD!##HGKqwPI55! z{GNW28wT1`a-c<$leM9`9a$0y61TlLpJmNbaVFc)z0q!RLMnxUL)?=ipwI6m54ckm z4-Q5n@!$}E;=!Q+#e?S>lz)fapfY=?y^#l;ZXfM^jv))v?VfM@K#O350}spaZPv^Y z^*n&`C5HjLEjkeTmPGA9uKYS{IQ(6n(TlB4Zn}H^*lvcs-P-5~FQ>EAu$WbLyY?X$ z0yfHgY|POUcP1Z)HbLoO92(g6W#>#IP!5viiiM?O3|%tYE}lamoPP{qeIo$}`Bjcu z&7|qBv_?z6Xp(9Gw&c`d34a-e5O@?oZa4Gi1LR>u{sMq<>dOtvf2nmd9=K7uOr&yE zaW1+P`-)P)J4rw!^R;pHK_OR&$fF~yD5wS5bWC41jQ};Ydz65=cQP&?0GsS5zbR7S zA{G=6k(k88ac?0OFrX56EZWKx7!1f1j<>>mfJ{6AART$}G_>tu!8Vj+(TzJ6PzK~f zr@;ccoS-IHS$kQ~mjiPsig+??tVou;0_%`lQ={XI%S=Ou^6g|*m{{?2PW&Z6A||~w zf-eIo?O6p-+OryBBwcI1UE+kcv_Y5)APvge zRLYzINkPFdxRgSo0q5XaLBF!373(Mz&EGqT6RlZ|`!nY$ctz`-MX=ge0~_w9))0W# za{Jt4Q6Q9LwzpZDG3prXI-{{{ehLc3*jE4)hfW13=X07t#UO?7N`PzShY)naR~N6r z?|9N61CjCV8$~Hs|LbVGb16Dti7(DX9?>{{7iUsENgFMtjZ)c+XAkBZ)^G7<*0pe8 zPOw#?&z2KC8I;WbbPS^Tp8-(wCk`1RXU-~_AeR+3sW zYdM*99tIM#CIIrzG2diRaTObE2Dl4;rnuCSj8)fr1=QmK5>N9Lht{H}Q~^G+AjdGJ z;-j%63?c`oV0u5B%VLJF(5GwgR10Sl>IS} z?3N`+^&}u)3|Nb=6b$on$eZ)BhQ%F7(s_silzy%;BFRWbq<$Blx2Bq*Gw3)O^e^s2 zJ=qfbllHz0A^H%M!4EsDwAW$5)$W;2VItWwB#Am*g1mI-oe{hgpw#IygYs+TCEbF6 z%EV&5%Xo(sJL0ySXX?JG@t9)``r$bN{bO-epr_bH@K{va%K{1~Tknlt=R_PYG5X8V zSVq4Cpp5=q1{GI{Sde38U*lJ@B&?@$FcvAUXC0E3X$5|pn}7<^c0Hd^9#jXJ;=h6m zI09L&MH@Zg8$IDWIV*}*gvVLZrO;d0Iyfe_8Un3J#m|=lD`Zd{@BCzOJUdfkC_P{- z7Fv>pz~Xl;+Ng1vH$n%2Yet@o(KU`+^E~A(` z7q?J)MR>opk6YW_kg;X}Xd7hku|WQ3s1X?-0Jw(yh-5%mjI*u7f-;%9k^rW#R`TCq0v$*p4vM-v%Pu8mBhUm8;LC1|xT5=B^)v>Kog zLeR7sLW)ClMbL(FomES37)p`9%A$R$yKnNt>Z>ekb4{A$7|~Np$d>?W z3Hc|2OD&~}b4OlY>9iwX$FMB>G8(z_32vgZZ?Z(b4`5rxUuzb7oxBnwl-HnIod%HK zg*-J={)C0sH434NnCor~H_nahRv7RV;7APQCgg*G@N~G0yp1^Mq3=%3oY5DR~p0S^d)Y8{|BJvPM}1A&crMJb zOpqR7)S#B;-v`)a!w;>j6lEB!kx44_E~7t_)CNo%=lkbAtBhX(nrqCDFeZu3K9eqKEo#(V zsAWQx@YrW5qQ}lol$+G>k=3y}y9bcpoHdDogVJ0jO~NdV)yS`04l8Sv29w zs3q?)Ee(^75@u5QLo zfmA!WMHK4FS@)XQNaTD3m*0RY2!)F2?manex_4>~-j4Ds+sLkXVowK$78INA50)(f zR&G~XfTW6$FCSdH4>?iO=L0tl5-{XOqHYLpA2pF%a#dpouU-DxfZ{m11$E`a4#d-^fshbfjBm*_S)%C}2tc zZ~^SWN4?%0<0iJr6+W)i7mn0d8dkBN;gY@<&m>5)qF-oWDX(M!wVwWOzHh%By`70h zX_nuJ?WqCmlo;DnbpK)K-dX|t&F(1UM#u5NpZiF+BQxA_PwTXRPp^LGQ%imgXlS$r z-MherR@geNAtuHet+Tn97SBLG7jpvg=P|_rmT||XAZ!j#66LQ08IGUG=Q+SDdJZD! z8K#>Vxx|FuM{|P2vPbgS5!?SN@_Ae6z6bKL&1mx}&M4-j8zuYQIwzn@#Y2}Q9xP^a z3hjC9&=3z#Xj&IbJUk@qC!Xh8*F-${D0^=EAz8~Xwk$E`qw6myN|DL>=31jp5_m*F zx1^Wj9Dq{OlOMCfK2{aGmLN!%YwSt^65pN~Sj5!o#UxoaF`-ScHC$CZg)pUBpiIJ) z^CP9=(ow)D5I4K69jP!Qaaxhk;2O#GF!bvuSFEF{T-_fT*qv;xwS8{^T(lR8R$g&A z3Pst`1n00ikDcsF&@ulM?yGJ*!n8+*cMFyXnpkvOAB5>*~zL951}T-KI$78kG+-qu!BTLe9Uwja*XT{ z)b)E;l>3k7?a|elK-~C)06_uW-vUrRVQG(~*6yyN!^P`#;O9H*;tYU%45CZaL)ZWm zw0K_yY)yTG&Rkp5Tf?EgXX0WY;0lha2xEh$Lx`Y|#95mPuntiPQ{Hsvnu6 z>2fTF>2HV=GzmyY=|PVs{l9@xG{M&aJc?7f6Cmm<_pPG8SB=N@860l4pW%1^yi?PW+`*_^IVoTnv0G zC=&+7qG=SRO_{8SB)yQm8hlbcS-8Tp%$d?tuxy2wGkjEa7^&HaAw*3Vpg1&UP_+UA z%p8XjZd)PWMpY+@S?kfPAG0=Caj!q$Iyp8qv9af2^sCuB{X-P=MAa&exIa+D89cPAh%=1 z{RUO5I8~Cwg=)}dgeKK0u21?%Az`m9z&Dy!BSv7Gez;YzcDqNO6vj^hi>o<(TB;P#(71;X>S>s?@3bf77jYzBj0=T( z0Yx0cs3amyGbxOqs{8_AD23a;ArNjpC?Ia<6)0qFq!M`(q4E*bBq+X1L5s}hGJ~oQ zvUCT)4-x!5fPd~4+uXUMqw;jXqIk6|5AqQW69*HQtr5+v`pc(kpD+eP{~a`*QHk(> z0)-zLuymFt05e}fs^u+~t3HlN^n9^k+2RC{C%(zKMZ@Nqf(j*O&g6Qwx1{3u@{R12 zOwViLJ28Y*5tpQ?I!f`<12&qw-x*oQ@>3k}Km*e+;}elxfhz6Z{y2hvLU37WzX}jw zO^^Uj`7M;@UqwFEI|L(kxU`q_y@K>%o#!H&D{%WWOGlJ(xgB|_B41IEuyr+}Bp}{Cld@klLlL|tg1Zc?9$>fY06qv^)ZGL|FJFbihnAr5y_WFP zjt-;AjIlu4G@;0ODypNBCxPg{%`v)3u(x~J;aW2&C{FNR4#uydeS_&Kfd6sYgm(wk zPnu0YY>6=+Zq}ru>EfY8llTl-M#NhrZ8y@lbXX6HzbGu-$Np81Do@Z7r}?ltM=F%A zgdz#6{s2t=Lo_H(Sc>u+07C-R!+`iF3@b+6JA3IOu@+OI6?b~G==!MDIO<7P%|a(tV=g(M0r;ySQwgE3*gu!-L>i5$(U~);(YGFGNCxuOt$N?-)Ceu>!;s+Uy*_ve z(q~yhm8}mz_E5ioU1_=S!DDd8$zAqSxMSyLwb<#SlHg&rYU3es@Y)+~IJ*r_{2ub0 z5ti8MAt+q&aTLlO|6K&J$h%Uk%ntmdLG{bn?e77u2DhX;?gKo_bA;3>?}SuEG+l-| zfCS$0RzCvMXBa2%jXQE21e_& zw6~2u!kEhy-;S=2T0(Ty&ki>*i`F`bJpHdw(I}p`qZF^lg&E4Bt(YP2+pYRh5eyD8;!!PPeuD#!bQ_p{{M@W<|?r^ zy-y26Y8puC_hkH}8@DO7{mW|X|K?&KL{%D-rtSsdBxwZuKo$qiZkQnz>jUXA1u zvgBV4bS(L|2y)k>W#enH^y>!J?`OAv2e?||h7M-+sYoI2n&Bb#3Aio^Cb$6n<9*KV zdEh^NEWToGXHEZC(dzo0B=_5(M)Ubj1iu@>`yzP1fjwINfTjtN%+_i&eiJH!GJnf5 zfp)!Zwm*}xSKBhfP(7Gv^Mlf6rrhK1#E4*aelq9x5b~Pe_agWo5&V7x{}W9gWVas> zYzhY2T-<;T7^Xhe$8^wb3727EeUWb>lh(H&Gz|(LUs-h~ZFh+PfI42jiXe|$a)O)( zP6ge@OkqK;&ksobI0IIXL1CYulsJMLn6bs#rP z;yHs5fsb0f3!;7s@E>P!*PWx0x9>s|1Y4O{`T>ADqdOT!p6-Oq|1>z2#99q=YH~^& z9~UhgPKN8Ch9F&4&|2&XW;63wGP#eDX}qI?MD*iIpN!xy4eT*Fw~#=>vrW#J zz;ZH&supJPbE^oma5rqWo@})LnP7T+)c(*K%z$N+_qhb*-!9_-dXp@b2y=sD-4n^Mh_ z1O-``So%71fgg?2Mm*3u)VgU7{k}Y_AG7L7*6VPGA6C`akKyBNkv&r5)XVQEwHyu<<^O;|7+4^BJ>e;B0!XxC>O-4x@iVEL8 zoT}1hO4hossL^8*2^I_dZXXVX)E6C_P++DZO_e%bhcYO?dl=DMyK7dhklNpVbx0z1 zAz_|K;reA9;xKE7uvz1I4athv?qa%^*K@lX@tWzept^Z`$1)@d+jWkn=BT=w5;zQ? zBtX9|ttI9}0;_8@OC%6qLA2YYma)o6sl zLKs;-&oXmpS9F2>7BbFA-;f*&to^hrafA?T`{igTM~K@-r&22bN~K;1u;~cjXl3n_ zket_Wgsj0%qkWQYBG(zLS+>VfyvkdpoF3xlEOmO|fa6Ny^w z@p(}L8l2)npSVBdd6C#Udt)XfRX6^r@A}AbjvJDG!e=-YmN?uP` zPH)r@r(d`dh}t`-zxt%vHAgviemV;K?O+?sw|^hiQg8#>?*S^t0R>-Nl*a_3;=Z{3 zzFs5>BZR~=@U5Dz;UrsHPX;_ZGHqXmaX~ogZap6P9iJVb$%fdEo~t|&rE*3T1c8B-qUH!HtVxn9VbftQ`CA{8k?=S+%jnBcW~xU;%W7l%cwWixC8{Ga|Jm0IB7-Rj3=uil zQ*hlrcP#tnF%CF zeq?< zJ@483-S2+y`#oo$Gnp709vB}P9UIQvPriA4^n&53>EWz+QFWi3CzNiDR+1p`xAv36o&%tqOr4{jbEn;9L?@|mg4!&$f*85lF_q&9A3o5es@ zY9gmq6@IC~SixRv8oxI&GcYqcF^-PB`1)r!aA=8N4bhvJB02PsK$GnrysnBt{LU&6 zT?S|mkS4D^oun_mI0My#Ncsg?=ioVqYY-In?i_mXvcF2kDB-~P5D>FHD_a#mRp3KB zfE)bupjp^SZ~1bPTSh+is_}97IU2;geLLqpc-alf82K38G&wdpJPqV-ymWBU6HGOH ze%7~XGAr!2{p5M)GAB}bM`7pynbYu^#Tu?{cJoAAO{aRwDEl6SSqIWQO8~YAE(O>l z#qp;e;;w*8&*j+FGDf!V^}VL}B(P z$(PqG@ZhDh8U>9N)WGnT(dn6KDgm7bHj6hzHK2z}Nd<=zgB>dX9wxb)#THz7HLz2> zNyii8!yO3v>g zheraIy=ZWwy3QtcunLrt{Bo%tZ>%G%KhLr7@TQ=R>R_Pnjix2R339Px0a~D}8&_vPp3sk0tN5;BH-3x>R&`95a zg2$a`7kQ4^)0+pUk+#-g93~c%(aTe#)446>bTGPvjA}V>)&QYCG)t%oPU`dOJH`4N zx&2`Ak8&paq7(XM{;|v3utD42RSrgEiXp$w2;t;&-+JI&t(dOH{14P+(7$AvTeT; z+e6|kn+f#1H<*d#7OP}YN=E^xI~m)r3t7uNqk$)%6rlVBP>85eyC}poLuwME**TRDEWcw~su|>vts`09XbUnSWoH{C zeY{D9z$x4<$XlXlOjk^Mg<&yxiqhds$b?bhTyg>0g(OGgDbH?2FNcCK7g~=qz|26Z zedez0Er?3|ytNlClgtL6n5i4)Zta3^2Z~gEF~GNQ{XYfx)HdO&q_(`0*QYG54MHH1sB)kfeUTe}F| z9*ky?&=r^z`Enu?{BQ)Xh~P&6ZYRQ(0*iHy$}(Itszd&twH_bUU~~BV-R86xRHIE| zjNM5lK8|7O>Jt(CWCX7UD26`;@LtPMj$x|xE9i`=sgwV!Y|Qg-yzic-?*--WkjrZU zip%RFsCXvA4d?}HN}k&zlhSHr6)F|KR7FU5e`(#G)$xg$HvX~vm#`}DR*)L+znBM= z1U?Otm7J`@i=W28j?mDD1MRL}{1lMo#WwIuo|ZN^rKnHw?$h)bRAg*agE!cFpkS1=_x_qND-sedyrdL8myn zD}w(7gyU^-rki{bMppH?d-*%w0jl>W>U9-Ez6gmsXZEI5sYDU+#`qC1Si5^(po`!ra&gok zpzPdaZ-Qu)6CMUAULJ|yqX2P3BVVHpLWDeIV`15PSrt~_2okOWih)7_bRlSFtD;Q0jq6JT$&X`jh~IjL*+FF?;XaIV9#SVr`0hG=asY; zlp1K{&Cddq*`6~ff1mFAK+aIm$Y$E-k3mObPX%N&FLm`&;LtuHCp}|5vh?)UO{kvN z0H^!I9;!H7itM4nG4WcO<=31_@P7cx>;D&^Wcm%jrH7*Z5E>GY!*JI7*clh-$2Aq( zM+du}<7hZ3P2>TzD5@KSPHi<2w4crvOJJgsXvX7{TE_fLcIu}Y_}Ic3B{Z$+r8L2bJ-5td;X1X zw(AGk)OO%Swv#(!xW&}MN-{DeeS3o<#8ZPN_j$YH-_!&t%f{3ZIJyqa4ltX)#2Tjq zZt2niYfI@s*@L+IW5PWI>6FjUe|s^DNtEJt@!x$6BZxbEzTIe9i5N0u*ynCHG-sH_ z0GTE8mjS#TI?Y&zEA*m{!LAY~N4WeBujm79OnGql{E?k3`&AHNJ*v`F%PvLlS5@d= z2-rCD#b;0ChKg5u2TpMMgX}^J+l|k;Q>a9PWw|9F7mr{{X7^*~5(p0%`pl3nPx)Ix1Ni|&(+-OOr)_kkDg%B+;CZ4Iy7M(JO z+Oh)n)L6`cl)+)WyoSXwl9BvANvt-!CJv}vrr;Tu?S
V!k^d zpt60;GK?|CYSIObUFIjDQ`$TkAkQN5QvfRYVA0|v>J6(Erzj7hs)K_TZ^Z9-E3W{N z=j{^zQ;(#bP5Ilu<4gBbfLw-wiO378B z%>}nQf-smr=Y8|_c7>xgR(}52dw5HD$`FJJ7FehIck0}>EF~x|rUNqut&-fE!G}cp zBY?8Q9~)FmV>>8D(JS0@2%>2>(YDyW0w6Vo_||=no#RLnb5ti&n{^_M;!=Z(sD4a} z+6deBA6mDwo>S(`M7wq#ng|T+X}W`oLCU;@4+L_M^3e&Xg+}Rq13-ySlS}+T>+BF8 z*PvLu*BYxK=SrtTtu}_UemH0GZh~l{gA$@4!VZWj{-Ma0(TPoMJ38HX-o)re9JK_~ zD&g1>+#9WzvSBlnmvT>I1?7j9#E@%O1?#d*n^5%VR>av?6HltM2 zn4|cfiQr~{+5;~zsJQV^YxDQ_q8pWS7Rl7l!$`YfD8)^>#eYBWEkziIT%p)5VnErB z=5sZ&3>uIrK5vr-{UoZ%dhLg+&jMm>aRO`B{L5jOog6lgUN=bd7N3LZ^Ox2ZB&B|E zm7G9wKIF*0unesZ-*Xh)u0)cnLoP?WE|(z|UqF+}Ar8>{x3v|?MzSIuz2H3onQ@UF zg~9ydi`FCx;e4WZRS1Vecus+UiUNBNE9Bf=Iv1wh2tl$HXcBjN2d?E#+amZ*fO4lx z3@UC^y2SE+HlWVj@qetxF*p4-^ZQM;*Cy6t3J&g>D2vMjKgE> z$7 zHK4TorNGp%=kUYmR|#WJI_hPZ6c(Pm;~6tZB;c{&DN>i9{^4|eU`75sF5_em1^Uh+{l&mqo9CtO;i%|QlHS5VdXv0sMMmR zg@8`X9{`|QQW|0^f;W_>*|7YEWefFNo(6P2g%CQa(RpAosVtg9d;+ID(o6Z8$SdT_ zCu_WFjyxeSC=Oska!{@_2=}M*vV5|WrkxdG+`S)dkk}4xkxHcmOwCYqmeukl%Er!` zfO4o6SOYZ6KLEs+FmTG2y!k~_M&D7Ck(jc{moPELS2;{VUQ@$SD!P7bKq5yz$Uo?i zmHuTD;&BzehGabP{ifs;vMXN=Ee@);15EfD*O21A9Ix@kiD6OlRlaauz8Wt0$QMo| z<%acGbGLa~+}ivOfEAXHsXnFS9k?cI z<!w6qFEH476nG*3E z=!hZ?Y@WgU>K%Fo!l`Jq&bI+Nxd5KJ%$ocI0Li(1k+HLVME(PG9*k%EauOPCjsFNx zTgaURms_hX-N3Sh*Z4lviR{lX`Le zQC!nAl~35ojXmjvFGALx1a6d#>Q>-_j0nf_r zY)bpm800chS7&E_W@YsA?_m*{<(>%sE5Tr)@)o-;Z}qa=61ioryE)3ne5zaso#xz> zBu$)Dw}vKRiO-V~Oq9;_>)skjxY2N}O+2ov9DK9UaY>K{?zV23Akj5~!phsd>USQj z(Gg0nMU~zMFmZ%$X~;Rkx1zGB7dKI(${h09WE2E;q}+5*RpdtWw4}B94*}Lw2ZE~< zU&@dF04&w^EhUe8*%P9Ep6wzkp@BInm45^jz;BC%t8x+$P@DwptC5;+fYTCPd!X-z6!Yc2pMtdI&gT;ouwIC6at*1ndd4*5uLnH68|Nk@TI z{KEz45ueZcaEv#xb*-pci~h>MD)uy5^4Efk)B~hOrPLEXQepmENHHvrYy}|~qS2b= zcS(Tw^Z-suf^8Sme;TIidyD#XtjQZ4rw4B@`F2!>d)(7FG0@ZdwF_x6vd5q;UQ8+2 ziyQRDi8V8^jA)$A&9tDux|$R7{PUP%FS~G$O~KeanIzg@4`jH#FrUaiF9BV##-Ux= zr~mq5{ygksH>34;at0wDPfqZ=@zy{tH4pQQbg-D{G!I_cX}q;& z9zLOI%*Z_Z0J)oa4zTXTJox;1{`etVD?m+=7_VdMFPJ&S=2D=}XR1hmDMIgPa{*dS z@BVa;syI~{End@rr1$&+EY56zU!B*13E8qv2{<9va8$7iW6HHaPsUX8>jfEUiMA7X zh;=r$rN)fRX-5LWm9pzW26we9=A?FYpY!j`wuWtAHh>o6g{D>1(Gue9FpSS82Y zO33kgSLyLLad}#^p5LgE?tTEiz8R-Ca9y8{zGyP3V;5#iHA2lRMIHfC(#Vk!#ADoi zNoqEXZMT1oFUeNe7rWZ(aO+NN#W%CMM4?aI@1Ug7nZ(s<5Eoa+MDSPx8}Go%g?Qx< zn&3(*HA22V8o2IwLoc69@hki_n1qsJ9RYiZW0HU>QQZ)b2P>>lLZvHc+kX{0RSX;t zkS}x;uLek`Vrkg83)i?U8UxU{3*n$6D0{Lh!hINt{2MZ!eOZxUvjlMvM5Z{<(y7<$ zg@snmNq#}Cad)5r3+h0fuT&Ly8z=exj;`!q@Gp+DG3jb#V#>Z>Z$B?xVTB=(m0nH- zD7~BpPMW3|eR>}p(0z5UYqnBpho#oJ zM5!^(!{)|+8qj!}C4^Xj-(=UJ(I*n`BZvl*96m0C=YwKeOUk4ch;sd?6p72VSoUbE z=CYkH0KJm@zY(iQz_S4!Mp3>95aU%tl>E7Bd|aQs62nc^!H7%yo*O-T>S>`Yqg@z; z^j-(9t3A8{YKQI>`PF+#zs3|D+FlQkyfkqi$r}>+bH~|X)PTzZ6>rEhN*=>LDn|B*qJcGs`O85_`Rf04v~InPVt+&l0eU^L#FxIbR9OFI?QHZMDzHhBv` z@dTC5vB~nt64U+Rw0YE%#;L-?y~@(p(B?AZRc0Th$Mjh3Pi{7V1#!b_T^bs+&dUCz zkNr3e#Xy2qNT)hN$~p&VX;SpcY6G()pKl%?nHU@DctiRPoSpv32WI(dHCNo*M)T+5 z;xQ4kZ{J?bX44OdDUxR6>qf;eI+fo>07|-Z0jdr<&!B2G0@fvZgBYOIDF$IPi20qn zShgM^l)nEn3q*!Oyh*Q47xy$JIqQou%u?~An5GvQq7-_?l~Q0vESHlC`mI4cZ!4wWv?;hrYXK}1)has~tQ=Wu;;(^|?>Fe)0nH2u+c^5=qj zl5L&FLcwqpkgJoUGuoTGidUT-M>o-X>ExSx(MB!H_7$MgA9Kh?Tzfv`%y=W1P&E}8 zl2K$?7^(bd&0bWH=tld84Q#@ubTim|_M$OX*u-izno;Wg?FPDty%?bM{-*%Bq3{T+ zT1`>O5;v-oO(LLFtGPd^Vo9qL3_{058Wj?F?kHh!86>*MF64n@!y_~P7%n&;-p^#h z#NW9QKz8hl1^4EMOlPmSYz19?JFYhdVYA}H6ko>2I9~H~FG9E^?PuD%=K~SNqh)1~YqU&UOj6Mdl=v4=~$$=_?p6jL^2&sDfx0pjB1BN4ok;0g?Vn;;rYEiWQV zpTTt+3jSz<_qE9j0O26PqLp(@g+m@#*B-#@NbB1A(-ivlLSaYi_j3^-4C0CJy0%C_ z6V<)+qyvBf+yX$}OYmcWCDK(9{CEUE5y4La^*&Df6u|r8i#nUY>gB2Ed|(+mKVS{N z@o1xHGq8@DaO5%--BHccHlzB9B}OL%XS+8$95#!B!u~RwoNd--s4EMhrvm=r6orSI z)gyHja9Co^N9!Z$YC0J$ff8RsRuJ(NNw*tSDw$yx*F)V4>|gab_J;ydRy}Tw`>Y<< zj#W5axzrj_)t_3)AF~bX%u9tBiF+0|13XFK^KvsP1Kh-;1{I^s$Vk9;!2O$aMp(5$2S5jPlZ&@@&;AG znhgxo>T?W^5m>Xiz?$lrPUhKZdILfZKXbkrg-}_-En+7^d>XUBK)$tUZNY2gQMXA2 zd72A47gvSEd&F`-!*>-Eqq9tf9*`_r&EsegpfcU4<_nN9~}T={Pyd-bFfgX;%4%w;V|})~<;(?6dZeEoWc( zCfNbk@L*Pi)dLW#xE0q*$A1&S?GgN31aC92c{Hbe0pKyvmVAfzNqUZn71E?U3#+=M z87F{Wp7B->L21h0czoCv-+gskf+|wb&h0-pnPLu;*&MTXq*-$OSf}ZgbNWHy=V;`m zojAICnJ*P1d(z8Eu6p8NyUt>?o{VeeUy))^JdHWe)mB3GAWrpb4F69p%)zH(0Qbjj zJA$>JJnyE%M{Hy#VQV8z9B)zBtlh~%R7exd(BboExf+ezJOTLfhQzo)J?a0ySsAVw z%^Jg1A>P1}5`*eR-qQ#Qt0wxY=K#HK7piKWjG5iCJrhy$lL@y#oVM5?%KN4%=HowG;vQ} z{eY4Gbpu_(xFdq!h~SP0{+)r%qo8KXUG`%I9DJuhCUmKYp3CHAk0;iln^m2v*Kim5 zHR}&jSaH4kg{%>%?sLT|VfX<*R^m(3mIdia+J-W|d3MerU2n}5z}{|4|FnHxTsHBUebb2l#mg#Ff@KE`ad zh~YH94*WNe#XsBRIpY5|Ufp~<*}V_k$lCWu@PP>aAc8+Mu*0kGlbA5cT(1W56b6Fn z?zM}+yWVZKzn8IFw`E45x&0!G=dKS^?s^_ zg&yy^(!)!5b8#&uV43C#zNUk3%eZ?e7CeeVTHk^&G-!Ohm)Rb-yUS(3+r$2qrxN7j zmYg8vz!NKXW2Um8(@A1Yqd*Bx@*^WTSJAr_Bu1fmbW&9fS%uw5G}ZJobV|EV zMDRZ%h!VmfppbAy)Gq+uQFnW_h`hmr`T_3Y8yBh4WTSx+h-n+Q)6uTxI@NA@><74STTD$$v%gza#j|2>!~zj*xR3 z2`oG}?M+aG}#ZP z_(rBmRM6F#GjcaBnvZ#024}1Qn@OS znC4^Fv=%VHzX&9lT_cYe)O-xOtw@xAaYA?huxqOc)Og)|*z1^#l^0=DjOuI}>hOCi zAih2&G$yM@-A!n@&;~p7h7BmXf6$wGzjJy!lf3IP(99MejCO_hGwF!iO&bI9d|q#` z%jTo>@_jHQhkpq`o@A87iVoj8kglSys22fk1G5n}g=`#+e~G_!Ae2_}5$GliSZFB7 z-nv$e3|vk<6SWYcH79vL)TZvB6mq5gkf99 zf(M@ZmWKh9OT7Z1T#DOEJrNGraO*fUgSAA+5!`9Cj?+mbJ%>`ZHlTZThs*0bnI!2^ z19Oue??(`#tz&&4uCS{PRdsCn&nM?mE31u6Jr23iw=obm{tAe#V`=guFeFWJ*HilA z4wnSq<|fdPPZ*7Y{)syMLQ2`%M*m%zqGPT1**`rBJ1fKnuUqfMupHcg)_XvT zTFRd#spzZmzPNQ+ClQqqBH|Tzfy6bMR7>NTz!D3g7LU}yIQeco74_Zk^-V2pjPsbe zO4up=ntda#X^)TzjDmX`a$~|M-2$`S!+RLAI?Ea2{L~S&lNf^Wk zs+<;g!!FCNPnHGV$EVv4MxM%sB8bnI|oWI&& zSLW;1mZw?c;^cIIij&s@tY?&)xd7D$TQe`UZmA`g1PRXqg>+k2q@9IzwLexz!fAaT zifo;WYc6>cF2Cp< zQt`*uIA4Y$_`u0sUyp0(R9q(~cwk*?{to1EBf%I=>$A!eEt9%?j|-WCZlL|(%E>|I SkNj`(^3%tMUW@+)@&5tUWX~!9 diff --git a/src/builtin/tactic.lua b/src/builtin/tactic.lua index 6e8c9af6e..5d5eef914 100644 --- a/src/builtin/tactic.lua +++ b/src/builtin/tactic.lua @@ -16,3 +16,9 @@ const_tactic("unfold_all", unfold_tac) const_tactic("beta", beta_tac) tactic_macro("apply", { macro_arg.Expr }, function (env, e) return apply_tac(e) end) tactic_macro("unfold", { macro_arg.Id }, function (env, id) return unfold_tac(id) end) + +tactic_macro("simp", { macro_arg.Ids }, + function (env, ids) + return simp_tac(ids) + end +) diff --git a/src/frontends/lean/parser_expr.cpp b/src/frontends/lean/parser_expr.cpp index e054de01b..54f219174 100644 --- a/src/frontends/lean/parser_expr.cpp +++ b/src/frontends/lean/parser_expr.cpp @@ -372,6 +372,15 @@ parser_imp::macro_result parser_imp::parse_macro(list const & ar args.emplace_back(k, &n); return parse_macro(tail(arg_kinds), fn, prec, args, p); } + case macro_arg_kind::Ids: { + buffer ns; + args.emplace_back(k, &ns); + while (curr_is_identifier()) { + ns.push_back(curr_name()); + next(); + } + return parse_macro(tail(arg_kinds), fn, prec, args, p); + } case macro_arg_kind::Tactic: { tactic t = parse_tactic_expr(); args.emplace_back(k, &t); @@ -428,6 +437,17 @@ parser_imp::macro_result parser_imp::parse_macro(list const & ar case macro_arg_kind::Id: push_name(L, *static_cast(arg)); break; + case macro_arg_kind::Ids: { + buffer const & ids = *static_cast*>(arg); + lua_newtable(L); + int i = 1; + for (auto const & id : ids) { + push_name(L, id); + lua_rawseti(L, -2, i); + i = i + 1; + } + break; + } case macro_arg_kind::String: lua_pushstring(L, static_cast(arg)->c_str()); break; diff --git a/src/frontends/lean/parser_macros.cpp b/src/frontends/lean/parser_macros.cpp index d242c6186..6c36a4ae2 100644 --- a/src/frontends/lean/parser_macros.cpp +++ b/src/frontends/lean/parser_macros.cpp @@ -131,6 +131,7 @@ void open_macros(lua_State * L) { SET_ENUM("Exprs", macro_arg_kind::Exprs); SET_ENUM("Parameters", macro_arg_kind::Parameters); SET_ENUM("Id", macro_arg_kind::Id); + SET_ENUM("Ids", macro_arg_kind::Ids); SET_ENUM("String", macro_arg_kind::String); SET_ENUM("Int", macro_arg_kind::Int); SET_ENUM("Comma", macro_arg_kind::Comma); diff --git a/src/frontends/lean/parser_types.h b/src/frontends/lean/parser_types.h index 0787d0375..d172e3529 100644 --- a/src/frontends/lean/parser_types.h +++ b/src/frontends/lean/parser_types.h @@ -26,7 +26,7 @@ struct parameter { }; typedef buffer parameter_buffer; -enum class macro_arg_kind { Expr, Exprs, Parameters, Id, Int, String, Comma, Assign, Tactic, Tactics }; +enum class macro_arg_kind { Expr, Exprs, Parameters, Id, Ids, Int, String, Comma, Assign, Tactic, Tactics }; struct macro { list m_arg_kinds; luaref m_fn; diff --git a/src/kernel/kernel_decls.cpp b/src/kernel/kernel_decls.cpp index 9cfebfa16..072efa8df 100644 --- a/src/kernel/kernel_decls.cpp +++ b/src/kernel/kernel_decls.cpp @@ -54,6 +54,7 @@ MK_CONSTANT(or_intror_fn, name("or_intror")); MK_CONSTANT(or_elim_fn, name("or_elim")); MK_CONSTANT(refute_fn, name("refute")); MK_CONSTANT(symm_fn, name("symm")); +MK_CONSTANT(eqmpr_fn, name("eqmpr")); MK_CONSTANT(trans_fn, name("trans")); MK_CONSTANT(ne_symm_fn, name("ne_symm")); MK_CONSTANT(eq_ne_trans_fn, name("eq_ne_trans")); diff --git a/src/kernel/kernel_decls.h b/src/kernel/kernel_decls.h index b789acbad..05dc88b0d 100644 --- a/src/kernel/kernel_decls.h +++ b/src/kernel/kernel_decls.h @@ -155,6 +155,9 @@ inline expr mk_refute_th(expr const & e1, expr const & e2) { return mk_app({mk_r expr mk_symm_fn(); bool is_symm_fn(expr const & e); inline expr mk_symm_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_symm_fn(), e1, e2, e3, e4}); } +expr mk_eqmpr_fn(); +bool is_eqmpr_fn(expr const & e); +inline expr mk_eqmpr_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_eqmpr_fn(), e1, e2, e3, e4}); } expr mk_trans_fn(); bool is_trans_fn(expr const & e); inline expr mk_trans_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_trans_fn(), e1, e2, e3, e4, e5, e6}); } diff --git a/src/kernel/metavar.cpp b/src/kernel/metavar.cpp index b519d8b24..b58bd84cd 100644 --- a/src/kernel/metavar.cpp +++ b/src/kernel/metavar.cpp @@ -424,6 +424,10 @@ context metavar_env_cell::instantiate_metavars(context const & ctx) const { return context(new_entries.size(), new_entries.data()); } +metavar_env::metavar_env(ro_metavar_env const & s):m_ptr(s.m_ptr) { + if (m_ptr) m_ptr->inc_ref(); +} + bool cached_metavar_env::update(optional const & menv) { if (!menv) { m_menv = none_menv(); diff --git a/src/kernel/metavar.h b/src/kernel/metavar.h index 1ad69ac1a..d226e360d 100644 --- a/src/kernel/metavar.h +++ b/src/kernel/metavar.h @@ -196,6 +196,7 @@ public: context instantiate_metavars(context const & ctx) const; }; +class ro_metavar_env; /** \brief Reference to metavariable environment (cell). */ @@ -205,6 +206,8 @@ class metavar_env { friend class metavar_env_cell; metavar_env_cell * m_ptr; explicit metavar_env(metavar_env_cell * ptr):m_ptr(ptr) { if (m_ptr) m_ptr->inc_ref(); } + friend class type_checker; + explicit metavar_env(ro_metavar_env const & s); public: metavar_env():m_ptr(new metavar_env_cell()) { m_ptr->inc_ref(); } metavar_env(name const & prefix):m_ptr(new metavar_env_cell(prefix)) { m_ptr->inc_ref(); } @@ -243,6 +246,7 @@ inline context instantiate_metavars(optional const & menv, context \brief Read-only reference to metavariable environment (cell). */ class ro_metavar_env { + friend class metavar_env; metavar_env_cell * m_ptr; public: ro_metavar_env():m_ptr(new metavar_env_cell()) { m_ptr->inc_ref(); } diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index dead83e80..2eb4c5dd7 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -482,6 +482,10 @@ expr type_checker::infer_type(expr const & e, context const & ctx, metavar_env c expr type_checker::infer_type(expr const & e, context const & ctx, metavar_env const & menv) { return m_ptr->infer_type(e, ctx, some_menv(menv), nullptr); } +expr type_checker::infer_type(expr const & e, context const & ctx, ro_metavar_env const & menv) { + // metavariable environment is not updated when unification constraints are not provided + return infer_type(e, ctx, metavar_env(menv)); +} expr type_checker::infer_type(expr const & e, context const & ctx) { return infer_type(e, ctx, none_menv(), nullptr); } @@ -518,6 +522,10 @@ bool type_checker::is_proposition(expr const & e, context const & ctx) { bool type_checker::is_proposition(expr const & e, context const & ctx, metavar_env const & menv) { return is_proposition(e, ctx, some_menv(menv)); } +bool type_checker::is_proposition(expr const & e, context const & ctx, ro_metavar_env const & menv) { + // metavariable environment is not updated when unification constraints are not provided + return is_proposition(e, ctx, metavar_env(menv)); +} bool type_checker::is_flex_proposition(expr e, context ctx, optional const & menv) { while (is_pi(e)) { ctx = extend(ctx, abst_name(e), abst_domain(e)); diff --git a/src/kernel/type_checker.h b/src/kernel/type_checker.h index d91b52f45..f37cdc26d 100644 --- a/src/kernel/type_checker.h +++ b/src/kernel/type_checker.h @@ -50,6 +50,7 @@ public: expr infer_type(expr const & e, context const & ctx, optional const & menv, buffer * new_constraints); expr infer_type(expr const & e, context const & ctx, metavar_env const & menv, buffer & new_constraints); expr infer_type(expr const & e, context const & ctx, metavar_env const & menv); + expr infer_type(expr const & e, context const & ctx, ro_metavar_env const & menv); /** \brief Return the type of \c e in the context \c ctx. @@ -95,6 +96,7 @@ public: /** \brief Return true iff \c e is a proposition (i.e., it has type Bool) */ bool is_proposition(expr const & e, context const & ctx, optional const & menv); bool is_proposition(expr const & e, context const & ctx, metavar_env const & menv); + bool is_proposition(expr const & e, context const & ctx, ro_metavar_env const & menv); bool is_proposition(expr const & e, context const & ctx = context()); /** \brief Return true iff \c e is a proposition or is a Pi s.t. the range is a flex_proposition */ diff --git a/src/library/simplifier/simplifier.h b/src/library/simplifier/simplifier.h index 2c4e5d9f3..1ff032c54 100644 --- a/src/library/simplifier/simplifier.h +++ b/src/library/simplifier/simplifier.h @@ -8,6 +8,7 @@ Author: Leonardo de Moura #include "util/lua.h" #include "kernel/environment.h" #include "library/expr_pair.h" +#include "library/simplifier/rewrite_rule_set.h" namespace lean { expr_pair simplify(expr const & e, ro_environment const & env, context const & ctx, options const & pts, diff --git a/src/library/tactic/CMakeLists.txt b/src/library/tactic/CMakeLists.txt index 5d3a881c9..8c799aaae 100644 --- a/src/library/tactic/CMakeLists.txt +++ b/src/library/tactic/CMakeLists.txt @@ -1,4 +1,5 @@ add_library(tactic goal.cpp proof_builder.cpp cex_builder.cpp -proof_state.cpp tactic.cpp boolean_tactics.cpp apply_tactic.cpp) +proof_state.cpp tactic.cpp boolean_tactics.cpp apply_tactic.cpp +simplify_tactic.cpp) target_link_libraries(tactic ${LEAN_LIBS}) diff --git a/src/library/tactic/register_module.h b/src/library/tactic/register_module.h index 7cfc7de4d..5af048863 100644 --- a/src/library/tactic/register_module.h +++ b/src/library/tactic/register_module.h @@ -13,6 +13,7 @@ Author: Leonardo de Moura #include "library/tactic/tactic.h" #include "library/tactic/boolean_tactics.h" #include "library/tactic/apply_tactic.h" +#include "library/tactic/simplify_tactic.h" namespace lean { inline void open_tactic_module(lua_State * L) { @@ -23,6 +24,7 @@ inline void open_tactic_module(lua_State * L) { open_tactic(L); open_boolean_tactics(L); open_apply_tactic(L); + open_simplify_tactic(L); } inline void register_tactic_module() { script_state::register_module(open_tactic_module); diff --git a/src/library/tactic/simplify_tactic.cpp b/src/library/tactic/simplify_tactic.cpp new file mode 100644 index 000000000..81bff475d --- /dev/null +++ b/src/library/tactic/simplify_tactic.cpp @@ -0,0 +1,116 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include +#include "util/buffer.h" +#include "util/sexpr/option_declarations.h" +#include "kernel/type_checker.h" +#include "kernel/kernel.h" +#include "library/simplifier/simplifier.h" +#include "library/tactic/tactic.h" + +#ifndef LEAN_SIMP_TAC_ASSUMPTIONS +#define LEAN_SIMP_TAC_ASSUMPTIONS true +#endif + +namespace lean { +static name g_simp_tac_assumptions {"simp_tac", "assumptions"}; +RegisterBoolOption(g_simp_tac_assumptions, LEAN_SIMP_TAC_ASSUMPTIONS, "(simplifier tactic) use goal assumptions as rewrite rules"); +bool get_simp_tac_assumptions(options const & opts) { return opts.get_bool(g_simp_tac_assumptions, LEAN_SIMP_TAC_ASSUMPTIONS); } + +static name g_assumption("assump"); + +static optional simplify_tactic(ro_environment const & env, io_state const & ios, proof_state const & s, + unsigned num_ns, name const * ns, options const & extra_opts) { + if (empty(s.get_goals())) + return none_proof_state(); + options opts = join(extra_opts, ios.get_options()); + + auto const & p = head(s.get_goals()); + name const & gname = p.first; + goal const & g = p.second; + ro_metavar_env const & menv = s.get_menv(); + type_checker tc(env); + + bool use_assumptions = get_simp_tac_assumptions(opts); + buffer rule_sets; + if (use_assumptions) { + rule_sets.push_back(rewrite_rule_set(env)); + rewrite_rule_set & rs = rule_sets[0]; + for (auto const & p : g.get_hypotheses()) { + if (tc.is_proposition(p.second, context(), menv)) { + expr H = mk_constant(p.first, p.second); + rs.insert(g_assumption, p.second, H); + } + } + } + for (unsigned i = 0; i < num_ns; i++) { + rule_sets.push_back(get_rewrite_rule_set(env, ns[i])); + } + + expr conclusion = g.get_conclusion(); + auto r = simplify(conclusion, env, context(), opts, rule_sets.size(), rule_sets.data()); + expr new_conclusion = r.first; + expr eq_proof = r.second; + if (new_conclusion == g.get_conclusion()) + return optional(s); + bool solved = is_true(new_conclusion); + goals rest_gs = tail(s.get_goals()); + goals new_gs; + if (solved) + new_gs = rest_gs; + else + new_gs = goals(mk_pair(gname, update(g, new_conclusion)), rest_gs); + proof_builder pb = s.get_proof_builder(); + proof_builder new_pb = mk_proof_builder([=](proof_map const & m, assignment const & a) -> expr { + proof_map new_m(m); + if (solved) + new_m.insert(gname, mk_eqt_elim_th(conclusion, eq_proof)); + else + new_m.insert(gname, mk_eqmpr_th(conclusion, new_conclusion, eq_proof, find(m, gname))); + return pb(new_m, a); + }); + return some(proof_state(s, new_gs, new_pb)); +} + +tactic simplify_tactic(unsigned num_ns, name const * ns, options const & opts) { + std::vector names(ns, ns + num_ns); + return mk_tactic01([=](ro_environment const & env, io_state const & ios, proof_state const & s) -> optional { + return simplify_tactic(env, ios, s, names.size(), names.data(), opts); + }); +} + +static int mk_simplify_tactic(lua_State * L) { + int nargs = lua_gettop(L); + if (nargs == 0) { + return push_tactic(L, simplify_tactic(1, &get_default_rewrite_rule_set_id(), options())); + } else if (nargs == 1 && is_options(L, 1)) { + return push_tactic(L, simplify_tactic(1, &get_default_rewrite_rule_set_id(), to_options(L, 1))); + } else { + buffer rs; + if (lua_isstring(L, 1)) { + rs.push_back(lua_tostring(L, 1)); + } else if (lua_istable(L, 1)) { + int n = objlen(L, 1); + for (int i = 1; i <= n; i++) { + lua_rawgeti(L, 1, i); + rs.push_back(to_name_ext(L, -1)); + lua_pop(L, 1); + } + } else { + rs.push_back(to_name_ext(L, 1)); + } + options opts; + if (nargs >= 2) + opts = to_options(L, 2); + return push_tactic(L, simplify_tactic(rs.size(), rs.data(), opts)); + } +} + +void open_simplify_tactic(lua_State * L) { + SET_GLOBAL_FUN(mk_simplify_tactic, "simp_tac"); +} +} diff --git a/src/library/tactic/simplify_tactic.h b/src/library/tactic/simplify_tactic.h new file mode 100644 index 000000000..5e552836e --- /dev/null +++ b/src/library/tactic/simplify_tactic.h @@ -0,0 +1,12 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include "library/tactic/tactic.h" +namespace lean { +tactic simplify_tactic(options const & opts, unsigned num_ns, name const * ns); +void open_simplify_tactic(lua_State * L); +} diff --git a/src/util/sexpr/options.cpp b/src/util/sexpr/options.cpp index 9acac9f21..c24608817 100644 --- a/src/util/sexpr/options.cpp +++ b/src/util/sexpr/options.cpp @@ -151,6 +151,23 @@ options join(options const & opts1, options const & opts2) { return options(r); } +/** + \brief Return a new set of options based on \c opts by adding the prefix \c prefix. + + The procedure throws an exception if \c opts contains an options (o, v), s.t. prefix + o is + an unknow option in Lean. +*/ +options add_prefix(name const & prefix, options const & opts) { + std::cout << "prefix: " << prefix << "\n"; + option_declarations const & decls = get_option_declarations(); + return map(opts.m_value, [&](sexpr const & p) { + name n = prefix + to_name(car(p)); + if (decls.find(n) == decls.end()) + throw exception(sstream() << "unknown option '" << n << "'"); + return cons(sexpr(n), cdr(p)); + }); +} + format pp(options const & o) { bool unicode = get_pp_unicode(o); format r; @@ -182,13 +199,13 @@ std::ostream & operator<<(std::ostream & out, options const & o) { DECL_UDATA(options) -static int mk_options(lua_State * L) { +int mk_options(name const & prefix, lua_State * L) { options r; int nargs = lua_gettop(L); if (nargs % 2 != 0) throw exception("options expects an even number of arguments"); for (int i = 1; i < nargs; i+=2) { - name k = to_name_ext(L, i); + name k = prefix + to_name_ext(L, i); auto it = get_option_declarations().find(k); if (it == get_option_declarations().end()) { throw exception(sstream() << "unknown option '" << k.to_string().c_str() << "'"); @@ -207,6 +224,10 @@ static int mk_options(lua_State * L) { return push_options(L, r); } +static int mk_options(lua_State * L) { + return mk_options(name(), L); +} + static int options_tostring(lua_State * L) { std::ostringstream out; out << to_options(L, 1); @@ -284,6 +305,10 @@ static int options_update_string(lua_State * L) { return push_options(L, to_options(L, 1).update(to_name_ext(L, 2), lua_tostring(L, 3))); } +static int options_join(lua_State * L) { + return push_options(L, join(to_options(L, 1), to_options(L, 2))); +} + static int options_get(lua_State * L) { name k = to_name_ext(L, 2); auto it = get_option_declarations().find(k); @@ -329,6 +354,7 @@ static const struct luaL_Reg options_m[] = { {"empty", safe_function}, {"get", safe_function}, {"update", safe_function}, + {"join", safe_function}, // low-level API {"get_bool", safe_function}, {"get_int", safe_function}, diff --git a/src/util/sexpr/options.h b/src/util/sexpr/options.h index 285ede42a..fcc2d3103 100644 --- a/src/util/sexpr/options.h +++ b/src/util/sexpr/options.h @@ -62,6 +62,14 @@ public: */ friend options join(options const & opts1, options const & opts2); + /** + \brief Return a new set of options based on \c opts by adding the prefix \c prefix. + + The procedure throws an exception if \c opts contains an options (o, v), s.t. prefix + o is + an unknow option in Lean. + */ + friend options add_prefix(name const & prefix, options const & opts); + friend format pp(options const & o); friend std::ostream & operator<<(std::ostream & out, options const & o); @@ -80,6 +88,8 @@ struct mk_option_declaration { mk_option_declaration(name const & n, option_kind k, char const * default_value, char const * description); }; +int mk_options(name const & prefix, lua_State * L); + #define LEAN_MAKE_OPTION_NAME_CORE(LINE) LEAN_OPTION_ ## LINE #define LEAN_MAKE_OPTION_NAME(LINE) LEAN_MAKE_OPTION_NAME_CORE(LINE) #define LEAN_OPTION_UNIQUE_NAME LEAN_MAKE_OPTION_NAME(__LINE__) diff --git a/tests/lean/simp_tac.lean b/tests/lean/simp_tac.lean new file mode 100644 index 000000000..5917ddf42 --- /dev/null +++ b/tests/lean/simp_tac.lean @@ -0,0 +1,8 @@ +import tactic + +-- Create a simple rewrite set +rewrite_set simple +add_rewrite Nat::add_zeror Nat::add_zerol Nat::add_comm eq_id : simple + +-- Prove the following theorem using the simplifier with the rewrite set simple +theorem Test (a b : Nat) : 0 + a + 0 + b = b + a := (by simp simple) diff --git a/tests/lean/simp_tac.lean.expected.out b/tests/lean/simp_tac.lean.expected.out new file mode 100644 index 000000000..6d960aeaf --- /dev/null +++ b/tests/lean/simp_tac.lean.expected.out @@ -0,0 +1,4 @@ + Set: pp::colors + Set: pp::unicode + Imported 'tactic' + Proved: Test