From cf35e7bed78be20a7e5e8aee4a5f23c70264e1b5 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 2 Jan 2014 22:47:45 -0800 Subject: [PATCH] feat(frontends/lean): add support for disequalities in calculational proofs Signed-off-by: Leonardo de Moura --- src/builtin/kernel.lean | 9 +++++++++ src/builtin/obj/kernel.olean | Bin 16364 -> 17140 bytes src/frontends/lean/parser_calc.cpp | 22 +++++++++++++++++----- 3 files changed, 26 insertions(+), 5 deletions(-) diff --git a/src/builtin/kernel.lean b/src/builtin/kernel.lean index 1e442e053..7086b72c4 100644 --- a/src/builtin/kernel.lean +++ b/src/builtin/kernel.lean @@ -177,6 +177,15 @@ 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 NeSymm {A : TypeU} {a b : A} (H : a ≠ b) : b ≠ a +:= assume H1 : b = a, MP H (Symm H1). + +Theorem EqNeTrans {A : TypeU} {a b c : A} (H1 : a = b) (H2 : b ≠ c) : a ≠ c +:= Subst H2 (Symm H1). + +Theorem NeEqTrans {A : TypeU} {a b c : A} (H1 : a ≠ b) (H2 : b = c) : a ≠ c +:= Subst 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 69ecb664dcc7b3ac83dd10e9ca3b5c5bd97d35d5..12ef425d3bc4935167acf13d386c360b02d3aaf4 100644 GIT binary patch delta 5353 zcmZu#3viTI75?x2|D>VWln??ekZiJ>Y#xvYyLpobn?N9RBG42HEtV!gpvbF8hqe^D zMaQ8~irAw>2g?X{#_gq-A!HU$OU-wX?Wfic zO&Q5BNP)FV7%~nplxP{+P)KB;2Fd|B#$qPND=_#NNIwWCGJqj#K1hEQ6m?cxfdU|s zEy|+~f$s<5hL ze^ia5+vAru7eXw)LV%xPn?-=D85RRR#V`!m%P>M;n-JI9p*JR!jYOMTsisv0q$jSM z&hd!datw=IE|wIv5>hGZB!l!Qwp#`1W~gaRM<%xC>O4q1r5wUkGevi2xTjR2l)dJ|khO^` zGL6M(sOu$uit|&22+t5H3rg)r88!*>K zZ%F0Y&z*uJRrCj<&^hY!<{X7Y+qAeiqB`lh;zWD}B(lxf>!-j=gmVBT!nuIbZS&~8 z;%2pjD#HaiO%S^s@BsCND^xE%8{QOq7-C5XRkE@WnR*{&l_7e_i_GOI5?McTh{sbw z4$(Ivm1-ZIjfB*Gx*Yj*_fj+NT3zPD{SYY82C9uzS>8PPS%|Yx0KKFn zwJEc}eu$9(Z;-v*wQs9@!~4+wV9lX$${q~c70K6#q8MU zSdd|;`aDCgClwA8JI7mlm!}_9^tIYKm@v()g`I;*_9)CxfN&Std~$PNu#i{C&Zn-* z_T+YG`IWcB;Qb|Z`IPxEVzBd}!{(&dyudh3JM1ltA55AyCI@hj>Rh+HlWtW$kbDs$ z+3vf1_!2{}2zIsM?HbRQ%cml%_I=?rva9?^!CMKBSNvR($azxouH}+hFjdD>QN#49 zejqhas!jz`;|1bsd%Sy0dVw%+SMgQMT@qvI6YD1FU__L7F%#gCgWX0iPOe+_CGcs> zI17B*G76uHah4wg*FoK>Ez3A-*fLVMYF5ivpgFwb`;5#M53;|uK})Vb?*7_C2dbtv z3_+Y0L{-d6ZinQj4j!dQlUfKf}GRG&XFRiT!5d5qrnp-b<&dn-;tR zahmV-tmgX`KIMBo4_twcY$3nrgAlq)LHE~$)Or(Jh_=`4pt14t3^QowP+RS!K%aM# z+FNO4{iIwBt@MRS`d)39+D2Dv$FzJKMr8|p$A{m=jBRKj>r4sgIP*0fW5|$H`XFs+ z3DTmv`)JveMjEOsr_)m$HAH8oObUF+t|HL({OhZ}5dMp4K`b0N=n1V4=wN+m&^|cK zsoDrL$La6&)%0#`a^RR@-FS~vLG46pkGExRg)s1PEK0A&b2F37(GShwTk-g~pMaGN zPxak;4MEW*Vt|OAMc8 z!@s0k^&OFO{>0z-@D0FGe3CcNl7^T%OM4o&CVvaD+;M*gD7Ts41J+@s)gKIT@?>5n z#Jo&=c5tqIKXv$KkOkGzAY)i*GSqv^4bhJ>1iIf4SIMAk|GNDq4K=nVojiGBtVm68 zMq}x;&yV4-_`xf2{|TxR_n!eJ?!Oq6iW?9SI)xy9glSfbW?(Pskear@zGJk z{{Cuax^?;+oos5TY2c3fBE+0`!wB6Qw^WvNF%NS738P@{!$r+wlW##eAqqkv*d+JW zv%n6XgU$?oUsrEJ!iS|^2=VmP^Ey#xSb2+O*Im%t#1=0yK~ z?RQpHzd)Cp8~f^gX~OenOgf!hgm++FivCYPDf%UYoO;A$odHaMJR*JhHuvR4+SwA9 zi!@5=#0{}(+2p?f#pJtyrKXHAQ$_=wLAug1K@HM~sgZVEn4L9Vj?S99<`|U}y`=RH zGfnTH$EP;V9b^ma^s0fb)As-+kM|971|<)%kX8*dCabVU61&WaU7^g@*1RpyTgtWhQJoO;^HTcr1^Pv6d*N=+vJUyd^m7s) zP^hgWq-}(%@YHg4o3njz1ME1vqlTKR=VNW%$rT2wt?qKFt!y%aaeglIi=^D%`i;mL zGDg-7THd$?soaHn*(e@S&MP2$rBC@R;D1`2uS1vH(;k(wKqc*?^6N1W07?DPqOMU- z`z*DB_O!>6PBg;|sasHxirog}ilIDi#WWt{&JipkuSVrdn z@BmE9A0z_?=v`nFAW-L4%yPEllyY98o{s7nyZlOHf^*!}eG0$EobF-dob-H1@?XWU zdmW_{9o6b4UFzseZZT5l2!hZfpuzd+djTasK4s)j6mCJ8zzH2SN{(wlUQL}XQuJ$> z@Ar!=kbfO=j_^zqYd7?qBQonIm`}`d-@r9Colz2=4wPw)z EKRKc{ng9R* delta 4419 zcmZu!Yiv}<6}~g~IxOBL*gPG)e(u`qx4jRW^?S`DVB`WqHcbLa3^56biwTNET5x1& zLZe7k8gWQVqqHd!Ka#2ukt)$PKr7l9s2Wm-G_B;cU}#h+K#+oHQ=nBl-#Pd0wXCdk z&wl63ne&=6bLZYVpstU-(^WvL3v1|LK{35j_<*)<)78S3YGs*UAjc4;L4IBd!8iyH z1uG%8ZdtS{T&65~GMoxIkjR`IdMo^}vT0V)*7R(MBWx-c@F|8tz+r|Vz-JlG0qkRV zFC8gLX!Rj|TvR#t4CJBS9Z%z51t_<8WcfT`u{$47>@ENdvW10!8HS4tQWqH(K)R<2 zfQT!AW#1ec3V3ec4Lh5-rdJ9BWCd!T(Tf0#eJ&UfFcBlwdm)#$!#(c%2F#4ciTc!H9TblNF&ZqB|hUnq) z6^RCDiT6f8@!kX|Z5B63r#P(yU<-Xzo>{LZpn<$BRl(`Ofs{;ld6^G#NB%2hpmCz44dA(2I3udU!E!ZtvOupLl(u!H^`Nvn+%kA~-9Exoqr zq=%waDoxKvcgI&kED7Du5Rs{0gFI=79`Yj-o@y#~&K=@$H%L81Z&p;7ZZ|S%4~{Wp zMo||dg9$xMUsP;fxfTL(x6X&_8D>4}y@uDLSfmd?%ye_j*o7s|>3S8Nwx3&u~LyAL{+|qu71H zVL+JIFVg8)wR(ZB#qL`?oK=%eA^~lu!m3D+3xwL}SE;uu(YV<_E8u5+6nw}JNO&)x zqx93NWZqGi6+M&b=T*xZ2QhJ)p=02u84}(zbc`OUUY&PrrlI52%UZXwA!M$(UjjfU zLBxdY*A>u`77sNCnBna_ z##vvnrQbj)1fs;(;}oi`4SfR=*B33X?TwGHAP0Io8D{IMx(%-GHa`Qww94PeDzGapyl4Ifo4ZUW>x%OA zjqC!5Q@UEWW9(VB$64^fB|GI?GrZg}yuO=FNDJ?Ix#K6n&30S7!UlMEJ6<+O;Rv(% zWyp)8YrisenPoI>i%p>(Do&^C=8x&S2J1VX>$_RkuIVg4(>3$@wwdkK6EFiZt>_Xz zgi>@~i41rIZO;zi)b1G>+CW`3i|B*KTsqMZY<><3{-W6YR`$1p%eyh#3#2@Bx1l(1 z!OS(OZd}#MhsBIGwM*b%49lk20jF|3aW};%z17&({5-_df}Oigv||X`rcX>5I^w89~aQjg4ZLLrH_U{=ZFUnwE~e1j#i29pI<=7vA&V!GUqt z$}*r$q(k`XGHn^SZG0hT!~X3KuZlWq(P;ej(Dz_OTKN@vJ6RH%M8sAYq=+uJ6y_OV zmt=+Z8rqX+2&H^MA9bcm=}(FBb!)Ri>r2cp$T38{3Md|Mz_{=S2H9)TgVs2oXNwKu zrn84+)n2CasRDI~9!V|_{SbO$<26L7hUk2?e_GpTx-pN^OR0(K>*U;6M@ zfcbpzYI-~!SI6ma`njePQ;;?cTut&Y4NBzu(h)ZO!?n z&&^M|+yF;YZhN>ODlNxjoW6VwoTje!@K)@7%L#$x^Vf`e7ZN@J*_@N-y+JeR0L2qf zRc9{rcC+zM8S;WK9}t&DYMZxAdo;fv-u=|{0DaNkvO(UgoK`05#V9)Wa(*Aes`SAH zK&j_P202Q)5fEQXPE1<*EVuLo9qdSaEn6-7e@4Sp6H^ofWnBHin>5cSsXUjU=L!DNR%p!_*Rm|(J*f%*;Y&G{oBkAhmA;D~4E|1N3sw z;_ypi!3ZSHZ3cN)4m#aauRh~-%~@8vwHLGYaR&c{maOH!040Mj0fR8eA54x+;9_CB ry1e@~bb6)4e8qBC8h5B>XCLc&YWqYDXVkQYaBpc|k#EuDvL*iq%mWx3 diff --git a/src/frontends/lean/parser_calc.cpp b/src/frontends/lean/parser_calc.cpp index 3868b0457..124afe443 100644 --- a/src/frontends/lean/parser_calc.cpp +++ b/src/frontends/lean/parser_calc.cpp @@ -44,22 +44,34 @@ void calc_proof_parser::add_trans_step(expr const & op1, expr const & op2, trans m_trans_ops.emplace_front(op1, op2, d); } +static name g_eq_imp_trans("EqImpTrans"); +static name g_imp_eq_trans("ImpEqTrans"); +static name g_imp_trans("ImpTrans"); +static name g_eq_ne_trans("EqNeTrans"); +static name g_ne_eq_trans("NeEqTrans"); +static name g_neq("neq"); + calc_proof_parser::calc_proof_parser() { expr imp = mk_implies_fn(); expr eq = mk_homo_eq_fn(); expr iff = mk_iff_fn(); + expr neq = mk_constant(g_neq); + add_supported_operator(op_data(imp, 2)); add_supported_operator(op_data(eq, 3)); add_supported_operator(op_data(iff, 2)); + add_supported_operator(op_data(neq, 3)); add_trans_step(eq, eq, trans_data(mk_trans_fn(), 6, eq)); - add_trans_step(eq, imp, trans_data(mk_constant("EqImpTrans"), 5, imp)); - add_trans_step(imp, eq, trans_data(mk_constant("ImpEqTrans"), 5, imp)); - add_trans_step(imp, imp, trans_data(mk_constant("ImpTrans"), 5, imp)); + add_trans_step(eq, imp, trans_data(mk_constant(g_eq_imp_trans), 5, imp)); + add_trans_step(imp, eq, trans_data(mk_constant(g_imp_eq_trans), 5, imp)); + add_trans_step(imp, imp, trans_data(mk_constant(g_imp_trans), 5, imp)); add_trans_step(iff, iff, trans_data(mk_trans_fn(), 6, iff)); - add_trans_step(iff, imp, trans_data(mk_constant("EqImpTrans"), 5, imp)); - add_trans_step(imp, iff, trans_data(mk_constant("ImpEqTrans"), 5, imp)); + add_trans_step(iff, imp, trans_data(mk_constant(g_eq_imp_trans), 5, imp)); + add_trans_step(imp, iff, trans_data(mk_constant(g_imp_eq_trans), 5, imp)); add_trans_step(eq, iff, trans_data(mk_trans_fn(), 6, iff)); add_trans_step(iff, eq, trans_data(mk_trans_fn(), 6, iff)); + add_trans_step(eq, neq, trans_data(mk_constant(g_eq_ne_trans), 6, neq)); + add_trans_step(neq, eq, trans_data(mk_constant(g_ne_eq_trans), 6, neq)); } optional calc_proof_parser::find_op(operator_info const & op, pos_info const & p) const {