From c24f26bf3897d9067af8fa40763d574934685a3e Mon Sep 17 00:00:00 2001 From: djvelleman <110697570+djvelleman@users.noreply.github.com> Date: Sun, 4 Feb 2024 17:44:06 -0500 Subject: [PATCH] Add "decide" to list of keywords to highlight --- docs/Chap6.html | 14 +++++++------- docs/Chap7.html | 2 +- docs/Chap8.html | 2 +- docs/How-To-Prove-It-With-Lean.pdf | Bin 2301484 -> 2301473 bytes lean.xml | 1 + 5 files changed, 10 insertions(+), 9 deletions(-) diff --git a/docs/Chap6.html b/docs/Chap6.html index 12f79e7..32e1c29 100644 --- a/docs/Chap6.html +++ b/docs/Chap6.html @@ -480,7 +480,7 @@
theorem Example_6_1_3 : ∀ n ≥ 5, 2 ^ n > n ^ 2 := by
by_induc
-- Base Case
- ·
+ decidedecide
done
-- Induction Step
· fix n : Nat
@@ -877,7 +877,7 @@ 6.3. Recursion
theorem ??Example_6_3_1:: : ∀ n ≥ 4, fact n > 2 ^ n := by
by_induc
-- Base Case
- ·
+ decidedecide
done
-- Induction Step
· fix n : Nat
@@ -910,7 +910,7 @@ 6.3. Recursion
theorem Example_6_3_1 : ∀ n ≥ 4, fact n > 2 ^ n := by
by_induc
-- Base Case
- ·
+ decidedecide
done
-- Induction Step
· fix n : Nat
@@ -932,7 +932,7 @@ 6.3. Recursion
theorem Example_6_3_1 : ∀ n ≥ 4, fact n > 2 ^ n := by
by_induc
-- Base Case
- ·
+ decidedecide
done
-- Induction Step
· fix n : Nat
@@ -1321,13 +1321,13 @@ To
by_cases h1 : n = 0
-- Case 1. h1 : n = 0
· rewrite [h1] --Goal : Fib 0 < 2 ^ 0
-
+ decidedecide
done
-- Case 2. h1 : ¬n = 0
· by_cases h2 : n = 1
-- Case 2.1. h2 : n = 1
· rewrite [h2]
-
+ decidedecide
done
-- Case 2.2. h2 : ¬n = 1
· obtain (k : Nat) (h3 : n = k + 2) from
@@ -1409,7 +1409,7 @@ To
rewrite [←pqsqrt2, p'halfp]
ring
done
- have h8 : 2 > 0 := by decide
+ have h8 : 2 > 0 := by decide
rewrite [mul_left_cancel_iff_of_pos h8] at h7
--h7 : 2 * (p' * p') = q * q
have h9 : nat_even (q * q) := Exists.intro (p' * p') h7.symm
diff --git a/docs/Chap7.html b/docs/Chap7.html
index e859b0b..dcca3a5 100644
--- a/docs/Chap7.html
+++ b/docs/Chap7.html
@@ -754,7 +754,7 @@ 7.2. Prime Factorizati
by rw [h6]
_ = p * 0 := by ring
_ = 0 := rewrite [h7]
-
+ decidedecide
done
have m_pos : 0 < m := Nat.pos_of_ne_zero h5
have m_lt_n : m < n := by
diff --git a/docs/Chap8.html b/docs/Chap8.html
index 92f8a4b..34aaa63 100644
--- a/docs/Chap8.html
+++ b/docs/Chap8.html
@@ -1298,7 +1298,7 @@ 8.1½. Debts Paid
apply Iff.intro
-- (→)
· assume h1 : numElts A 1 --Goal : ∃ (x : U), A = {x}
- have h2 : 1 > 0 := by decide
+ have h2 : 1 > 0 := by decide
obtain (x : U) (h3 : x ∈ A) from nonempty_of_pos_numElts h1 h2
have h4 : numElts (A \ {x}) 0 := remove_one_numElts h1 h3
rewrite [zero_elts_iff_empty] at h4
diff --git a/docs/How-To-Prove-It-With-Lean.pdf b/docs/How-To-Prove-It-With-Lean.pdf
index 79ed09b308f3973bcd91bfb73254df4fe89808c8..75890f2ea74a53fc4b9c68482aac845c1009d6b5 100644
GIT binary patch
delta 32128
zcmZ6xQ+S?T)GZt|jjhJE-PpFx# ~9~;gLPf&XpJ!@
z##~jM(ct<2ML-C62t){E$hQ!vknbVTAuu7ZA#fq^AqXLeAxI&}At)iJA!s4!As8W;
zAy^^UAwL>%dX51~o?EQ#vlT`db#OmTW^jkgo{L*1H*I6Xz^Rw2N|v+*Xm*)pfl|M5
z3I1O{=Z?^c6dvMF<^_$dnq>_nsKWQuKd=s1GLs(;nBr#Tdy;4Vl_|v93}=|001Myu
zyB-Y$x8+*AQE#S~N-piAkMp?_=9ok}uj~yO#Kp^VwgUlw`<;`R;CXhpaw&4Q1ET4h
zkSurvnL@NThC<2GNHUBwMTeJ+-($C}h4QaqypCf6u9_S_#0QtGor>{4e~P%f+O4Gh*lHl8`#hNy5rFgMx2Vn6dZ)iE5lz3{g#7~tL$#EKGqVRJ>*Jub$erR4;MPI_
z#Eq;?Vc}#U^z0}o-l%1`)QumXgm)xx#PcIb4M9Gr*K3eM=GY&lSHg+C@Z}Oet{^Nv@IBPVYq!|yN6rGQ4u54$2KEHBJ>Mr
z0%6oH;cZ^A2~3<}`_~Om;SCinLFRs~OjUxHcH);zv*bi60evhLvo|ix5b1tNF2?5u
z@%$82g~4&?TQX+ve+dn}bsYP^-4&1X7VNJDvG`a$SQLW`{@==?C^UYZtE*icH8c?;
z>nEx7Cl*Cs|I!6JwMQLANkk7l*SzXkxH)5YNDkVemgu7Ww{Wg^BD~XeeZ7~!w}Snb
zP|peAa*YllEAa(bFfDFT06D1IizRNDvTT0Jc+E6DT!tcgbnospgR
z(qE=6A0gWx&L)NF)CFU$t(=KEX6BXjS8_^AN6vBfvPi>2YZKqGqK$5YZ^n5&LcuYeyAe=t^Sdbn(57HBYZk^JljKyK!OSDb84hxRn<{Qy|T9T3&wMP
zS-Jq`XnMQ{^&R{|1+~v|FeZ{WzIjCE+O)>xo|ja0l)*?RZLIrF0I%`r;MFtslHT)@
zw$gR{Vu$<^ZInT6^D0h)-s&+{ooAu!Uz3S3rr_gM&)$1m7bgS&57(MZRQ0X;NfP%V
z=KLwGAA!1UAm)#k%^2kZq{%C9y?%%#(oY%IZ1*W`lu#qo(3%1oMaR3|B&Lue`kktp
zjO5p)K}(1h4xFF2Wx`N2PJMhTh(CAts?JJ@o+<;r^9SyCoQPJL_11;8NqUrdNbqV2
zXJM3*+?VYQoxlqLp)&Hk!DmVq_2S_RI?tpJS*8?%%$ltV&muNSc}r*o*u3d!B5F1o
z5JP`DdE1&;wsXmRE7}Zs;f7hiBL;YzTpasT>wU4~mds_u%*l}LY<#;pJK$9v4!6z{
zF|dk)p15o*?p3SBoPfK^1}MR8!*(CP0ao#3F~%#%-f^4_+>J7YQJx8eIN`>oRX4gUGsJ(yr3oetx(
zN9?{zNQm)#ILw?kOmSu_VnfDF=rL5;
zENP^GshKrUaxp*07H=V-qNamQ(gwp#XsUvz7`BpzWp@*0$EqUUi1hIxlcV)ySsWR=)Vke0L@5%=KRC$UOHmzwL@&$3~d|)Y~R{i|DOmW5c
z+VgtAZKMx!GT@ga)A>q+lRnu!gqva`{_zJx2Z~qH;wZ8o8wHPBeYT|e-vdV$2RTfz
zS!*o)sVUbmzU&8V>!{TrwK@U3E{YrNger&jbDbBV_X=>_g;93D8+CH$w*5OR+%6Pn
zLEJamKW(nozh`AZlrRLU(@PY1pXs)f@KxS`(8Xh>@wro;|M2&7Go;9ytn3@ltQ0ws
z?CKKCF>s9trXqw2<;G>3C(>#ezdT`!xD0b9gj79`f``*PR7g%YHCNS@y<{v-pHRw#
zigPWl|2X^BbaRG_M1^V^{KfS!0!KE0$;%qZBa-yj?bI!4%rYgi+q
z@;h)to+)=hnDENj2i5>LOL;xSx>OVphfZ;WyJxMqseaant0PB&aXe9I@gBWx4)f%V
zMmmhoAh96r=z8h>mQ9u}K(t_y0;c;;$U?;x>}_okTtZEVm^m<4oUu9ez=>Q!+4;Lj
zm95gQ!lt`#rIJ!I7&kwWAnB|Vdhs^3frBmyo>SB65mwT;7`-oe84G&RgRur^*usw)
zqb`!2zjauRPs<-Dr`UR%y8KLu;|QhKm?DXa0M#o|B4!n%Wu&<>P>Hj@cltR&KUmpu
z75o_jBDKI;g~&f}R9Up_xUU>AafT{~ibE%Urwufw6;fggv1R>{p3HFiv9WrKfcwdA
zYU%K@Ib1MT6neYUqUG?7d3*=(rtqu&5<7F8!O%n
z9lR&fCg10EIcE4Lu-QT}d;`JR$EJh+TE#m#`SEji&(?Mf&TQ+lg5JtYy^Bp%dI${E
zF>P^W=j0XqV=9UlQa
z8MmRNcm23x_)oX)oKl0s^9bMS-B~UOa)Yg6y$ILq$&}Vssnht&;5=FV4
z4v4Ygs*872{BFWj>->OF|%(0hk
zBU+i7X^kWhz-9iA>I3WsUUgho^N^$_`l`PbNmzHmUz;@Q?voyXQmS0A76x6xPg+dD
zZd;g}xXVOiCHRXsRkSFJ;hSN@G+wMySWL>IX4bmzpCKSb`iFOZFh39Sy^n{EA#N$A
z*HVjJ-|Y@4UXltw2;dpo4~uX#JLTi9k9p=IpRHW`R#pD`JS6q#B~sy}?(u932)Q{r
zgrFst1HogNNE-m(Dxvv!u%(yaCk{quMaMkYe7kMxR9M0IwhM}H5`6L)mGRZ=N_7)OPftT^H@u-jkKVxwzT;KCH#)zxl$X0eu7Q)a0t|cH;zNj)5y|D|GPB}Wc-LXI~
z^?oh#4gQm?-NjcJx(FSu=bgVV*7lz7y>Uc^h4^HA2V4
zwlHohAOM89E5>j5&|dKIrYJhbe;#sWLP9aa^JY>rN~Zda1kr;F0p+y3DPpM9+;`>*
zp`_8vhc(2!p&O7I2d?Fw1fEeV;Kgp&c#{(2)JR%yD$8$x+s|bs=J=OF9*5iKm|Hn<
zK@UNj>8cl`-0oD@Fq*I11XXcA+}Q_VQX3t>%WOQ=m&RgB)^tJKtW+;&;qk^z4{=a?
z)ezRRBtt24ApN^zcO|%4x2eahTC<#kyqh}GgBMc04A@@V!g`n}NPf`*n^TjQkLN`L
z4)at=%kdFDgM=eG+EDOK5b%B71i&{7j^IHo5x5wj0$g;8Z)_~AY#<|ZZ0r`{G~6^8
zz`N4#oVwt571x5Yc4orX-M#(;%LSx^#v5PS2;r^(uNIT(m&A^-yQLM9d)niPI4tQ%
zN1|9;N&WD{@7_I>>$z-Dw1u>X%bnS`Xdke$!dHc%C&n#E(s~W~D=5Dd{~~^f4!q0j
zPMEEjhiy}cVgFYjxQIxSTgJ8m>?uJ-pemIwMrbS%S;g$fc8}87kvVmbD0Bc@iN@`R
zhXc{0e6sedYCGNaI_F|Z%~Ra;=sQ_`IE=aJ<
zymLpj4)3-@Wo(n=N(IG>oNhXCG+bQEq7aD1@sD~GIx?Z?590s<<9(zKFa|XvfcQnO
zLrd>YQ_Vk5|9g8Gjmsz_(Z;dwo_V0&=Luog9vEcGFZWopZPVRD#;#^pE^K}p?XDPw
zbNl;4?FW6_mR5IH5$P5Zh&HxN6Q9plLgN_`baro=MQtR)Jg&v+Y3y%5&O!f8#(-@XxvNOe;kC?(zi&&7NfSY>v$Wu1JI9*+jQmzH
zFD7d2gx4mA@-zVQzndsGBq6!0DCC@~WLx6rVU?gRosQekb$oV8Fdg3lL`g?ujbfCj
zO}s*V%vInOJd10l>h&_!>A2UxOJ;*Mzoy;kcq4uSlkukLWGt^}@~65Ct1oCi^C8d8`Ys(fB8v$v%y
z#@F*C$totV`}~RL|Qyp
zkt+u4ojxG<8x_QZkyPZ}Rj^^_kc3x(Dt1jBiQ??PPmXI(UVEwlatf)E%m%pMBc_7h
zL)}vqN5j6Z_xlnd3XN`UV~Rms0Q+&!Tmnu~_tkQK7MfHip|jxQ`@csFr#I3UZ-2~RSW5-BNHft>9zT={^pWn#VL6dV)DSNWTj%=`CMt2?=J(ue
z2WDnj5&}X+#6<`B7U9x>v$m8J;kv;9
zJG$AttrT9mFTeRnDX5@!eJ%XE;r->JM2FO0I@6>GZyCAszB9G@3#cJMPDmrsP3R=c
zf3wmoDSKGBO5TpI^Hg}gnX-)3%Db_jY>)oFPYB80i=W!40zCx;{xI`O{vEhAsZBxd8uWlglkL&n7Z^foBH)1f2FKA`P1duePAoA}+fCN!P_o7lBbCVu-(#O0mz+O#TeA2!hgKbq
zJ8krsm*ReG4=$agT2f)zBAIWW1H`mFKd#NYRnS6}dsMlVQRuCOBeIFF|?OLaLxaV|vO4+4Mvet>Cs1a5?3
z`^0qw%tG16KAkyUuHEP%`P2l{QOOfIB|l9&-`B)(B}0ecB+#JI#*~}X0EJ0OU&Nu`
z47y43utvRFRBg_Tbw#*{2*Zrc5rl&61`&=prq8Jj3p^@`z@XFYjH9`nN3NKN5|35x
z-b@K~ry7m$H9?GaxWm8|hWEvd3RO?5m=>61JzFJa2=;I#dOzFkW8W@JyLc+W3`-i-N*O{`LZut
zy&$YeQsnzMy)ZWTtG4<|`K)u*ZNH@~yHoU-3h<7!uV_u8r3h4}wOxGZ>sZ#m%uSp|
z&U1OSPDoDl25g=DJjSznVDCO7hHB~yRab6#Uk1NNBXv1N&6P(jz)bcg#7!HzhUz#?
zGsK>c(`jHhl+Zl+u<4HAEND0Gj>l>H!V{F50)cyDI*uJznp3
z+CxVUtgA>AhQ_-c9dn0bm~O0l3%y*5KcMguzn7udbDrc?H#J14XT6a|K!|KRgX&@0oqi9v2n=fKsr2=ih6=+0zcIKn
z!_4H~`m`Lq%(p0sxar02(GWq8ej@cWY5KR#LA8*3Uy~Qj5KfA-DW@muEMuBsf2ABf
zv*cJL#L)ZzZc>4XzAWEwK#KNuS_hd~?-9jL#W
z(+G(%DQAZTRual
zqzGDqBhN!Ff~Fkv>l4l3d&(xULSM&P&GBf)^1+(JKK$c1p7|`IN~ZUlS?+&DaDKvuA70z+1kFKNV*pxLA=PDkhUq0bO41i~}2wOiQ9GH@;uQlcR^lWjxxr@_vcKy->
zl~(1|G0lX!TTi5yv^1yH*K1>m^%zh6Wd#kOAU{n?Y-N*F`QS>GXX>GiG4gSh7r+@Z
zmh}nk+~pHuQ)9tG^G)?+=`0&Ezd?8I9Cq`%rOyHbk=7_L{giaElW;uhff0NSe
zz(?yyefk0mVvEu*PQ~_pv}gg2zYG6g^iI@qOg{mf+9AepafuqfrpsR4^9F5H|!c%^7SA$s}b57i4Tfx;hq9#>sAsne)C
zbK$Vtp5lRZcC5%k3$+29AVpOtuG0*l$(8LRryPQCDT##l=G~Zd(o^HA=aXo;D)1WQ%mwW;1bzkWd{Nsip3UkcN4n;5-4McpdBKiP`a<$fpLP$yFub$6ob0=mz%
z9Z?}IZ{d$`Q)gd!wDco&lKcdaUV%DZvq?$!&PPJWcSUwl(Wt~gJElCDzqVc0OGu+z
zl`UDnDdM^+`i(_oNzb=f+oFv#3$Ha&$#}1DtHNk=1{Sjd*D7(x!%SjRZt2uSgl|L<
zF~!2OVU`xs*jg-Q_Q-O0Pmda%{fROy$v;6fdB#ZTBz^2xU=$WDcz8bm9l0oKVQKII
zj{OO)OI(+~HJfx;f!m}QH3V&tV5o5wUHA(5Vq)VvXqR}VFK3m0-I+0ZPNTwO3lYVk
zc2rqtUKMq2p{0uHMs)eDMEM!5R>Dbg7Z3jr0@#u#c4dLYHWP-?g*Kez0mUj~?;Tw!
znjW*d3)>#I%R8lE$FFUGwIB|Ua{)%*%($7)cWqbC_%C2HjuPQNcBy1U;cR=!-PGqrZ1rYP3_!
z(j1KcexZt~EU`)@aqH!;E-9R})$-3*saY-))1dXLB