From 66ec538c6353b827bb28a3ce53e3cf0155b0d41e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 3 Jan 2014 11:12:57 -0800 Subject: [PATCH] doc(doc/lean/calc.md): calculational proof documentation Signed-off-by: Leonardo de Moura --- doc/lean/calc.md | 82 ++++++++++++++++++++++++++++++++++++++ src/builtin/obj/Nat.olean | Bin 15904 -> 15911 bytes 2 files changed, 82 insertions(+) create mode 100644 doc/lean/calc.md diff --git a/doc/lean/calc.md b/doc/lean/calc.md new file mode 100644 index 000000000..8a8674aae --- /dev/null +++ b/doc/lean/calc.md @@ -0,0 +1,82 @@ +Calculational Proofs +==================== + +A calculational proof is just a chain of intermediate results that are +meant to be composed by basic principles such as the transitivity of +`=`. In Lean, a calculation proof starts with the keyword `calc`, and has +the following syntax + + calc _0 'op_1' _1 ':' _1 + '...' 'op_2' _2 ':' _2 + ... + '...' 'op_n' _n ':' _n + +Each `_i` is a proof for `_{i-1} op_i _i`. +Recall that proofs are also expressions in Lean. The `_i` +may also be of the form `{ }`, where `` is a proof +for some equality `a = b`. The form `{ }` is just syntax sugar +for + + Subst (Refl _{i-1}) + +That is, we are claiming we can obtain `_i` by replacing `a` with `b` +in `_{i-1}`. + +Here is an example + +```lean + Variables a b c d e : Nat. + Axiom Ax1 : a = b. + Axiom Ax2 : b = c + 1. + Axiom Ax3 : c = d. + Axiom Ax4 : e = 1 + d. + + Theorem T : a = e + := calc a = b : Ax1 + ... = c + 1 : Ax2 + ... = d + 1 : { Ax3 } + ... = 1 + d : Nat::PlusComm d 1 + ... = e : Symm Ax4. +``` + +The proof expressions `_i` do not need to be explicitly provided. +We can use `by ` or `by ` to (try to) automatically construct the +proof expression using the given tactic or solver. + +Even when tactics and solvers are not used, we can still use the elaboration engine to fill +gaps in our calculational proofs. In the previous examples, we can use `_` as arguments for the +`Nat::PlusComm` theorem. The Lean elaboration engine will infer `d` and `1` for us. +Here is the same example using placeholders. + +```lean + Theorem T' : a = e + := calc a = b : Ax1 + ... = c + 1 : Ax2 + ... = d + 1 : { Ax3 } + ... = 1 + d : Nat::PlusComm _ _ + ... = e : Symm Ax4. +``` + +We can also use the operators `=>`, `⇒`, `<=>`, `⇔` and `≠` in calculational proofs. +Here is an example. + +```lean + Theorem T2 (a b c : Nat) (H1 : a = b) (H2 : b = c + 1) : a ≠ 0 + := calc a = b : H1 + ... = c + 1 : H2 + ... ≠ 0 : Nat::SuccNeZero _. +``` + +The Lean `let` construct can also be used to build calculational-like proofs. + +```lean + Variable P : Nat → Nat → Bool. + Variable f : Nat → Nat. + Axiom Axf (a : Nat) : f (f a) = a. + + Theorem T3 (a b : Nat) (H : P (f (f (f (f a)))) (f (f b))) : P a b + := let s1 : P (f (f a)) (f (f b)) := Subst H (Axf a), + s2 : P a (f (f b)) := Subst s1 (Axf a), + s3 : P a b := Subst s2 (Axf b) + in s3. +``` \ No newline at end of file diff --git a/src/builtin/obj/Nat.olean b/src/builtin/obj/Nat.olean index 5a341daf346c46389367389258eeed0a7ebb8a67..5eab6eba9cc03aa2eb94c2ee5ce7c5744a0c7785 100644 GIT binary patch literal 15911 zcmb7LeUOz^8Gp}t?_KupO!|j|__@F?yONm-Izy$d3&PGN0TBpA6uiscg$v6r+}#D7 zbox*tBgM2vv(!Yi8dI~(nLeDrxtGBGEyCjHkGTx<)LV0sT%1erLky|igf?TSTuL2 zQW}l);hVk@X+fDcUKtvz3@aI9yvA7>JgPjFrYJBf~&Y`eVeLi$R}gV|NDHJQ$IpN;B$7WT0VM0|5`;{GgNKI7$IBlZM9dpQtro6D400 zrBmx+WATVgj{^{eD5RNQC{)SwxX966-WCxQWfU%N#j+tx`C@bn469k_Mmj}c z;qXR>ZC%)+i;*FfL5cQj2c4;1Xgkm-xRc_wnb^ln1Q4y1<+XHZd^8XhV1n)mib+x` zq)?%2hMb-Vjs``XD&t_5(b#S&FCHIiE>jNT5Q#E5(;3VOibN81BDq;oZ?hsTDkJ{t zH`NTSD}#d&CyFMUL3u}IbZk_{DzDeEr!wuq$$-tm;eqjW%qJ~+DRC!xJd3lUPE1m4 zZGvI8k%*}W+q_bYI^l4MEOx0*Cvli*x@uu?o`F+p#fBtgVeKX5%ZAGlg*qKfmV82A*-SFcnQ(9<2a& zQ;74TyxxIH5$sCz3T7|NuZ*tSP^y}Y7jl%)m?%e`H+u{Jt}#mVm4-&k3x+D2ITKxr z{}l2yQ|Do7{JWB(U(MFpjONxpU%<{o;|Bu9$!0tt~qMMz0W7 zlh5&(-1K3YF&NrS7GAIz_=bXET;6)F^t;VG!+7EFm`P&%r}FsE2Pr|bFbip;!1D3_ zQAyQaF!hm8FQ}c*Iv z;e%}n68C%)yWSlhkx5Cr0 zso}aP&r0Bkepe8kTJNG!ob@DsVSQgGeRv`INexg-QJ*n0UW%Gu9v!Qi+-O9cN9dMx zV#J7SoI~9K(G}*(I#{Ag1c16k=~d{qP_fnMieguz`zUAEp!+!8vk~1*Xc)PD=vDn) zMaz>-En)%k#WT>}h=#u1iC%FAtpW=eQP5-s6g|V$Hd^@x07`(Mw+Bt3X3bS*V9tH( zb7Xv+{m$bQO^ip%Zd=lh1u8rUqKfRU;zTbe(CkN3DCp4*Biq-OcWkMqvRy!u`mtF? zwEEn--z1O~)zWb7EDZ>B$~c&1V9A~l6H+NjE^WasdI5~(oasfkwu=Iiq)@k^fbe@X zZWp2MNL$pFZKM&JmhnK-o%=<2QPrAzvu;6&|#ER?c9HGhY3xb120I>Wim zXbuFRQLrdXIs`jHNqYgMTG3JtImIN?V6v0(;ll9@k3k2R_u@a#Nu%T5DRdw*RoSF~PgkK0s zilqf?pysCyqdtwvqHmZ$08iqmXn;kntmL9D#c~*zu!3?@DA6a7Vj6&^H`~(D(X9`0Om4(d zpCpPSImu-?bVxcZi4t6JP`3gjsNmHtLIF!h z*=?Gcz66jjXDZR4WTHaYq;hIeHFuP$ySU;J1cN(8^}5#4A{kN@g21}F85ID08@zB1 zO6t0ABJh$=nCk9t1~0N2(!#~bN7M(hQ31XW^1ycLp==;hrsh%;TKMl`Me)`mE5x^F zlKLK&_chyGW1z(d9U~V6n|$n)vD;_g=Smm%;5hmsH$5O#uH*Y4miIQ`E7`)!8AVW| z3~V^e%>EB?1BIof5^mj~V($TJuNkQaK~Vh|4L$FC64XZG<70UP8TF#6yP&BjG0QK3 zVY$yGF`6tnqdg$`Zwp8!)l%T1@0bO3?*}rb*)xrDf1smmiGa&J;Br?ZF4ps+iSviI zOQ#qLQK;U1fzh#*)jcjKMV0{QTL8M-NzMH)d)Ov$^L03tzX9$4PLRWx=8&99&30lk z`;>eWOHEHn5~G#bG&&{Uq+!ETlE_J2Mq@hpL@}`Ex@=a$2j2+Pe*o0z8-XK8Q;E&1hNLK`hVJ*1$m|8U-~sC-u}U{7QhY zwmHdJHP8mv1)*DkJPaF=&wPO%#*{HKe*U6YIyg3s{uG)EJUyMo7K;^&y1XA8GLw%V?1wN1fG(XfBPz=SAawuS22T#j8_?4dQneZLL(5&$;EWgf@ z)s+)R6)bLDqONX+Y8h(SIYeEPjS9%Mrcv|JD`f+ba?Sv_?*;j|Z{X-Z#<M^H4s zprFm6;g}{bVu+qv9mrBj2fx0?0O@O;Y@P!G*{%lUsz$P5F}aVU%i}<#pa6;Ngffk! z+u(DCUIS3|Jb)OklH;9q@FSJJVqy~TTaJj4X@}Kmm6J#hROZf^(TJfa2ANo4L)(O5 zpfa`fmt1I|q}OK!K0*1XS2_VfF4={FfR|%sc>@7+W>J2&kQia|pkv&3B`rrB1$I&` z3j|sYHkVTjWKgMnx@^7djy$~5C;`HIjMenaQ?mfHM0(OTxAby`X;PX__3+y;x^~ zq1RfuBnFlShQ5F{{Rt3gSUHJZ#PfI-YxDxBmW9w|Nh1WQIPaKZN$1HY0tRi?X{JE` z&|k}Qkb&yEdQ+c|NvYo{f_RK^CEa@gkWqTl79wQD&da+c`;LXmX4CJk(rY3 z&p9AKM1M@aesu<*S2^pB0iK!kihc#_{tt>-@HDJ|68<&Nb0?vGC2bge1k3--o3`Oe zNQrWQD58N{`VA2iW4c$y)`-WQleLO#a=?vfDgFtK6a_UU$AF# zm;yE@v;u={q>f})o@7~Jq89-4Yl0FAFEB6_e}v|ugfoHQkXSA-*6KbbcR7%+OoX4- zm^0PEx74_!8$#TG2B8_#RjaVh?~tN6$VI`Ii-_pc^H}Od&YwDr}{Qs$4um#8^{YP)6vYN51nL`TqF~! zfn;!B)NUeeb}G_bBoJUvFfK~MBE`4|d@lwaQBGcjNmM&LYQH-e?}0SQheq`H3kxky zw(he~lB${&Tgj`om|p9qoqhnCirq(C_fgk<%yi?JA>>O9toeXChNfGTy&rvXKc$vr zQ+tE;uvv?h_XrCTFEFnzv&zHpiY*@qH0W=lw2z}Jg8#^Mag~bK$dlPsQ7aZG2@$(Y z+F)Lmhid+n-pmtDTmm#&cdB{*IJbXvygDEcDAO>!=tVj`DbX$b%p0x+TbGpmcU*?D z+z+RLN%-@bToUOX+79VRg_}G8V${bQxfNXI;2o6VzA3#)M83{E*!QCGH#Or5VW=hD z*i9m;hC6c;(5FLx*_o7if;-b7#k6)01Kx6qK{WnkK$PA{9%!9v0L-hAT3G$ijQpp4 zi^}qDH!G^v0TtH}=om#8lQm622J(pWXIPTR`nl`=!gZfQ_hLK~-io)eByy2kp3QD6 zr|C*ElWM~(#XGr~n2%dHMsus&F+L95WCsyrz4FP|o`AzTE+@py34J6xiWR2$JJ6FI zh@O24`BO7UZNo+K)H};wVy4Lx5Md^Gi2a^HSM2w!>;4Me$&fMr3hB}8RHV(P53t07 zfEBs`h#8!M03fT-(`Jwk0KT8L`Z#X1sMKHkK|)EQfJLMrl?#`Y+($WSE5SvW|fj}c7M(|X_-KPl<{X&^{G=|j&vE!!^n zmG8bq?x#Kk8^$r&$Z1NsIa!2Q@h`!}<|w1M-p)`ldYgCV?8eVB#2&#GXazXYkIh6^ zj6v%`tC%rxOvZqp1R(C1-5xw3e1gAk87P>9M3iMZ+n9*Pf8r(V;wiPs5W zEzHA6P2q~mjPxrwx!6Bw2Ek@-{HIgEoNT|mkT|4~J=R0P{sb6_qCdMXFU*q(@E6W{ zJ~iVQsU|)Q$;3reA47%&{wp3rC%(NK?IYHf;!r>>(jr1iYLu8CfNFeAY!%YF{mf$ipBIA3%EyjbGZ)BuqJWJw6aj`tSxlCx_+*8 zK1Fe)PXfK&^`xC_`vFlzLwZ4W%bi?X34dJ8;e%&~b6gURy=y*RhXbgmGlsmf{@GRDFMC8sfO?=47awu(vh$(DOy%~Va{h+NVIUZP{ zvCl~}l$az{IUQ8%r2OjSTfc&AN0j0DkV0@s7qCDiSBw8f;AAY~zckaxbx#zB>f!S|n zzW4XdH#6s)J2p}u8r|3!sb~2=vwX|evGIxQvikUFeIz??Xgsqkh9(cG!^jah{zZK`Kob_fKS>9Xq- zu=bR(u@T{cZVwtmu$SQBXsZxJj;1JRVXgxm)14^z@^$wFEe@a-U^8uG0)MjZYD<-B zOO<|WN5$hAg&qJTD$!FEdZKcr%mcE(cT;D+VD&*Yr4!eM5!Vk#TpJsL&p@lrIhY`t zf^yb=CX@fB$@l{5cTl!ydsYG7v{jSq*RQCrsgI8Zh67@7eH*5QG4*o*dzeai;c@QD$SG=X}QG$kaMjpbm+sQ*fP7?x#v*(WX)uCHG#h(qJ9= z*S@F@x3;lyBh<;V>C&lhZ!{;G+Ba3Zo{%Z^2L}@|%SSg%u4g^zvMWhDO=7+->j$g` zciF}=QG^u-t9zMFDz|<_oT=6CbtUamGH7MN@zOKqoZ&oU;p`RlGe_$gxf}*uRswpr z&)Rdw8<#hRq;_}`P4JcD^$qiaSKy2-TSppoaX`XJb!XU5B70v8h^YC7iJ546t7sK* zE|oYwtJ>`tRK-@yDmb;#Tt7TCF10Qdrb)5C!faK1h<_J}{-+I%H0w)78e2G$t;L_7 zYRlVI_#XdOQ|k-a26xfZHkJ$AQ_#dIfPTIX0Fp^xONk9f(6Y^ohnn7v!8^pYl=DH* zZhpVQm)YllJXgk#^yFSkrcOh2|jWsfQ*CP2Gq=Lva^ypvD0-yL)VNcO0$E8_-7Tf#objR2*8Z6==+}NS%52irqTZuDYCvzYex89~-CSw_ zTk9ubNe*pG2?WogN!AYz97T`%^BNhYuH`}`kB`xltaqAQtaI&Nj;dvy3Iu%@qTfd| ze+4jI@bq_^`yZBRSfo$?dt@Kd*}eh z)G>fwMDtRq74%NQfMC3?0njp7eL9oOQ-|0?!2ef@N--go{>}Mc165~|MEVbA-ibYv zGUWD0GfNZczhKalaD4}Z?{?xE?Be-oX zWIK+E?>Z0{);;>i1Z~Mf7aeavn(DeAwiOg+*usQ(Aj%9de-#ab#RdJ3#2j7an%H%q z%93x@exBgyx{!TXLuN)I<6YGuXhM1POrB?8%;Z{{l41sqHrP>2H>blUz7K*dyjFlEmgz#Sc_m#sfeF zWR^ry(NFOib+g#xF9RoaJ$zsm7ae1kW3c25?iGkM&RAhI*&!gwOLIB~)4W_FVu(nHq8daRC>(|4fk7x{biURF z%Bw&LW+5pp)&2|y+fy8ajdm>(K4iwG!x_jlqOd2#EH--~-bP3eJVs2H;BzTZ*j}v` zM}oHWWMsB-rbApRo{SzM%Ofc)M1ZB8_N!&y%Qzktyxj40L@_k7hs+(sE5(X> zg#_~zP$Y+U^JV3Lsn-ckS(&Z|%C%7*1S2~fnP?E#G_9m*VJkB?L9m_x)hiJ24K=;3 z4ZO&PT$LfHZjRJynU?FB(BppxGlnM`oguy7@y&NJeODFuH8h252N{Ob;sm82+4P>F{jkoy$C&}H z!AZcXHzS~@+#vUEOz-L-SF1%-Ggxi8K-h%hn^ymO+RGdSskG#XIOR3)43TtwE%|p?%>bDbIxq z^&2Gd3xW#zN&`r1_0<5&cgZ)~(}$J^K1^;lop#AL>DaV-Q;Gasmaz22NzZNS7vd++ z2+TjBd8cOtK}ULl4AM;a7Z~Us<2ONZARe##Yg4HYNu!Reg2#1e%6<6WR6eBV$Y)9) zzE|o)?hWzMqRGL12pvp&zWMT+b+(~j2gi9k{29U=0!UVRPA2ezuV`65Ph=H zaB|nx^TYMji7O(0oYf6YuStm0gS(yqfQfoyb|&jePf~giU z14;|W<%JbcC?4{XW@5atZgL_@et!V$cn_s@Opy2<8b;v_a}ABS5%M&sUk%{b2)4(U zW|9x`BD#lKTqf=GC=3CWtB9AyZ5+hrtg#=C@Iil)G}&HEZ!4Q2qrHfl{U|Vbw>^uP ze$(dh+-yw(M5bAC=H{SHHhrZZPUy{K(41!tn!i0s-C-!DVWob_BU%OoNyUfF_LD$9 zA+j@g3?`bzUZicS$xLVR3)kcvs{#Sc>}28D70NJT3k}W$K3G}xq(8j2<3sld|J+D- z%(U^J?M3m5ACa!!e^RC57ECSIOhxJi+Sy*$KzeaGDKIaQh7SYmrR7NEToEiTQ=%&V z5N5&xPM;g_m6^Sy3d$Oq@=9(7F*WG*XBo-+zKrN&ryjV0r$K6+KRuz=eihiYf@3f0 zAXV#PR2{)lUY?+(iR{yFJVXI9Yd9TrxwM%4_98*DYlCi40219U1m^jjbi-tR9|y?o zK($ckXiF?8&+Bc!w`_&f7l?_!LFeDD}gdqRDxtCnj^{^mh`N zm;`Hcfr-hqHl7OMSPi11l9=H5XU`1^vUKW#PZV4U%(FWvSdmG6ZJ{~hfXu*z=So($ zI4T^pIxA7=Y*4NQQdlu8K3RCI6t+CPa~u*}iRJ$7d1gM4!_yBQ4zdL_>zm|5@a6#G z6rVrc3We`}bvtIRk;YC(^8h^-Az| z33`Z(3dy^;us0d<*=Z118YTFjo;bcu?BYi%Y5e079mAI)!+Dnqkn(rz@lK z7xv-v80G`&g`N_ABY^#Flwn@a{0Tbk&^^vi@#vaAkH$RDB0)Am#+ZT$Cv9DtKZ(M;j0e$*;wIhwg6LkBAstF24R{P$G_BGBV zh2|w0w6Ex5y9o$tocbxzt3z?FfNCdbqbmc~Rl40!*ipa?RSfTs#p_^M#Ii7 z23*U;!s4J_4Rlr92|2nH?h4@D1lv|csRTR&F(2v%1;zBT)sL}!;$?hM^aQbZ+LXiW zGLX0r(0#rTDi31Euc175ByjdjF+3Ru2e6RzEfh6?Z_P)Ft3eHr2}e!lmZ@rH5esE2 zKllpT?DCH%{3er;yyOiP zaKmvyzp@Dr=JXVs>^F{=W1i#kcUg%7bSJe)UZy#GE#>;k(37*EV<8`@LcJQAXj9Z6 z%#uMjkDl~J#~p^gYNjzwL}}tkrX5$vv=9#>>`eMiEm-8}a2a+BrO6*0=x1P>)q#%I z?@0PPp-uFC$PRS1lmTK9Yb#Y#9k%lC*_;LWTsrGMfQI1x0em2U-xttX=25IVs1^fj zADX#p@h-rc15{lrPU{=2du7g<=p!r?*Cq1NW!dpC-9hy!0Ttg&Z6AavRUD7hbMRq- z+{OB_>;)N%4K*R*fYgp-fvcaW#rJv{C!WRyD2(h(`TB9uy5{8g2K|1rh{M}nW{ZQG z;wn!*p`lYivu{BqN@NYKtJF7G5VTWKMCNY0sJYzlkt`C zHhdaOCRpY<(QyR3In3RR9@is>Ou4H&|)hROS#|$on(PQDkyfk=K+YgugtXGKKE`GgB zD2Qfesn>rA*6MXV)X~hR!zj*nZWl+NB}ms^84#WzNC(d$NIA@4ZaVZ0B)Uhm+&>1a zaKy(G{wuV;^0RM(?$P%lh8rBk=$1-lIoO0+?q`rkU2?wd4c&prQ%Qfp49@r(>=w%HSQ&7rXiyF=rSenS0e<#-Jk*TzSMvMn?KZQzv3eU-Rq#$LXkiB z!~k=F5mWjkY|))FI-_}f_tq5n!kw2mmwZ?0-j*5n2IW2Ebx>oA0axnN@Xmp~% zpP-c0s{B+Xxg|d^ph#*G9DNY`e})XrsOJOt7l4{ve-)_GohDZ|5PV9x*UGBQ4G|G# zJpm#^d$pKJ*Ks@FL4I0AFs~`gg2F*LCAL+S$^m7!O+EWs-9+w%K(`0&J~Z*s&PO54 zyFJNZj4$Ms1O2>~FgVlgVc4~fMMxf1`O{axugoZ>N##Hc9!v+-1dKD1g-cgpa(}BF z2sdeUqkYOhVSNzz?PzBmblVLKE!+a6)vaDbXCG4(s3i`n=zXu*I`;laMr4Vexphci_Dqvs07gCe)p695-wH=P P`HinxGP>b3{3`r^27xV;