|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (find-LATEX "2025adapting-lean-tuts.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2025adapting-lean-tuts.tex" :end))
% (defun C () (interactive) (find-LATEXsh "lualatex 2025adapting-lean-tuts.tex" "Success!!!"))
% (defun D () (interactive) (find-pdf-page "~/LATEX/2025adapting-lean-tuts.pdf"))
% (defun d () (interactive) (find-pdftools-page "~/LATEX/2025adapting-lean-tuts.pdf"))
% (defun e () (interactive) (find-LATEX "2025adapting-lean-tuts.tex"))
% (defun o () (interactive) (find-LATEX "2022ebl.tex"))
% (defun u () (interactive) (find-latex-upload-links "2025adapting-lean-tuts"))
% (defun v () (interactive) (find-2a '(e) '(d)))
% (defun d0 () (interactive) (find-ebuffer "2025adapting-lean-tuts.pdf"))
% (defun cv () (interactive) (C) (ee-kill-this-buffer) (v) (g))
% (defun oe () (interactive) (find-2a '(o) '(e)))
% (code-eec-LATEX "2025adapting-lean-tuts")
% (find-pdf-page "~/LATEX/2025adapting-lean-tuts.pdf")
% (find-sh0 "cp -v ~/LATEX/2025adapting-lean-tuts.pdf /tmp/")
% (find-sh0 "cp -v ~/LATEX/2025adapting-lean-tuts.pdf /tmp/pen/")
% (find-xournalpp "/tmp/2025adapting-lean-tuts.pdf")
% file:///home/edrx/LATEX/2025adapting-lean-tuts.pdf
% file:///tmp/2025adapting-lean-tuts.pdf
% file:///tmp/pen/2025adapting-lean-tuts.pdf
% http://anggtwu.net/LATEX/2025adapting-lean-tuts.pdf
% (find-LATEX "2019.mk")
% (find-Deps1-links "Caepro5 Piecewise2 Maxima2")
% (find-Deps1-cps "Caepro5 Piecewise2 Maxima2")
% (find-Deps1-anggs "Caepro5 Piecewise2 Maxima2")
% (find-MM-aula-links "2025adapting-lean-tuts" "2" "adab" "adab")
% «.screenshotdimens» (to "screenshotdimens")
% «.geometries» (to "geometries")
% «.screenshotgeometry» (to "screenshotgeometry")
% «.defs» (to "defs")
% «.defs-T-and-B» (to "defs-T-and-B")
% «.defs-caepro» (to "defs-caepro")
% «.defs-pict2e» (to "defs-pict2e")
% «.defs-maxima» (to "defs-maxima")
% «.defs-V» (to "defs-V")
% «.defs-Aipim» (to "defs-Aipim")
% «.title» (to "title")
% «.links» (to "links")
%
% «.abstract» (to "abstract")
% «.abstract-bib» (to "abstract-bib")
% «.o-puro» (to "o-puro")
% «.introducao» (to "introducao")
% «.o-puro-e-um-lixo» (to "o-puro-e-um-lixo")
% «.teste-niv-deriv» (to "teste-niv-deriv")
% «.teste-niv-diag» (to "teste-niv-diag")
% «.teste-niv-lim» (to "teste-niv-lim")
% «.aipim» (to "aipim")
% «.antonio» (to "antonio")
% «.calc» (to "calc")
% «.manga» (to "manga")
% «.plonk» (to "plonk")
% «.outros-cursos» (to "outros-cursos")
% «.executable-notes» (to "executable-notes")
% «.plonkando-aprender» (to "plonkando-aprender")
% «.lean-e-haskell» (to "lean-e-haskell")
% «.em-poucas-horas» (to "em-poucas-horas")
% «.natural-deduction-tc1» (to "natural-deduction-tc1")
% «.obrigado» (to "obrigado")
\documentclass[oneside,12pt]{article}
\usepackage[colorlinks,citecolor=DarkRed,urlcolor=DarkRed]{hyperref} % (find-es "tex" "hyperref")
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{pict2e}
\usepackage[x11names,svgnames]{xcolor} % (find-es "tex" "xcolor")
\usepackage{colorweb} % (find-es "tex" "colorweb")
%\usepackage{tikz}
%
% (find-LATEX "dednat7-test1.tex")
%\usepackage{proof} % For derivation trees ("%:" lines)
%\input diagxy % For 2D diagrams ("%D" lines)
%\xyoption{curve} % For the ".curve=" feature in 2D diagrams
%
\usepackage{edrx21} % (find-LATEX "edrx21.sty")
\input edrxaccents.tex % (find-LATEX "edrxaccents.tex")
\input edrx21chars.tex % (find-LATEX "edrx21chars.tex")
\input edrxheadfoot.tex % (find-LATEX "edrxheadfoot.tex")
\input edrxgac2.tex % (find-LATEX "edrxgac2.tex")
\usepackage{cite}
%
% «screenshotdimens» (to ".screenshotdimens")
% Based on: (emacsconf2021a "screenshotdimens")
\newdimen\slidewidth
\slidewidth=15cm
\slidewidth=10.5cm
\slidewidth=16cm
\usepackage[paperwidth=\slidewidth,
paperheight=0.625\slidewidth,
top=1.5cm, bottom=.25cm, left=1cm, right=1cm, includefoot
]{geometry}
%
\begin{document}
% ____ _ _
% / ___| ___ ___ _ __ ___ ___| |_ _ __(_) ___ ___
% | | _ / _ \/ _ \| '_ ` _ \ / _ \ __| '__| |/ _ \/ __|
% | |_| | __/ (_) | | | | | | __/ |_| | | | __/\__ \
% \____|\___|\___/|_| |_| |_|\___|\__|_| |_|\___||___/
%
% «geometries» (to ".geometries")
% «screenshotgeometry» (to ".screenshotgeometry")
% (find-LATEX "2021emacsconf.tex" "geometries")
% (find-es "tex" "pagestyle")
\savegeometry{original}
\newgeometry{top=0cm, left=0cm, right=0cm, ignoreheadfoot, bottom=0cm}
\savegeometry{screenshot}
\loadgeometry{original}
%
\def\originalgeometry{
\loadgeometry{original}
\setlength{\parindent}{18pt}
\pagestyle{headings}}
\def\screenshotgeometry{
\loadgeometry{screenshot}
\setlength{\parindent}{0cm}
\pagestyle{empty}}
% ____ __
% | _ \ ___ / _|___
% | | | |/ _ \ |_/ __|
% | |_| | __/ _\__ \
% |____/ \___|_| |___/
%
% «defs» (to ".defs")
% (find-LATEX "edrx21defs.tex" "colors")
% (find-LATEX "edrx21.sty")
\def\drafturl{http://anggtwu.net/2025.1-C2.html}
\def\drafturl{http://anggtwu.net/math-b.html\#2025-ebl}
\def\draftfooter{\tiny \href{\drafturl}{\jobname{}} \ColorBrown{\shorttoday{} \hours}}
\catcode`\^^J=10
\directlua{dofile "dednat7load.lua"} % (find-LATEX "dednat7load.lua")
\directlua{dednat7preamble()} % (find-angg "LUA/DednatPreamble1.lua")
\directlua{dednat7oldheads()} % (find-angg "LUA/Dednat7oldheads.lua")
% «defs-T-and-B» (to ".defs-T-and-B")
\long\def\ColorDarkOrange#1{{\color{orange!90!black}#1}}
\def\T(Total: #1 pts){{\bf(Total: #1)}}
\def\T(Total: #1 pts){{\bf(Total: #1 pts)}}
\def\T(Total: #1 pts){\ColorRed{\bf(Total: #1 pts)}}
\def\B (#1 pts){\ColorDarkOrange{\bf(#1 pts)}}
% «defs-caepro» (to ".defs-caepro")
%L dofile "Caepro5.lua" -- (find-angg "LUA/Caepro5.lua" "LaTeX")
\def\Caurl #1{\expr{Caurl("#1")}}
\def\Cahref#1#2{\href{\Caurl{#1}}{#2}}
\def\Ca #1{\Cahref{#1}{#1}}
% «defs-pict2e» (to ".defs-pict2e")
%L dofile "Piecewise2.lua" -- (find-LATEX "Piecewise2.lua")
%L --dofile "Escadas1.lua" -- (find-LATEX "Escadas1.lua")
\def\pictgridstyle{\color{GrayPale}\linethickness{0.3pt}}
\def\pictaxesstyle{\linethickness{0.5pt}}
\def\pictnaxesstyle{\color{GrayPale}\linethickness{0.5pt}}
\celllower=2.5pt
% «defs-maxima» (to ".defs-maxima")
%L dofile "Maxima2.lua" -- (find-angg "LUA/Maxima2.lua")
\pu
% «defs-V» (to ".defs-V")
%L --- See: (find-angg "LUA/MiniV1.lua" "problem-with-V")
%L V = MiniV
%L v = V.fromab
\pu
\def\tabl#1{\begin{tabular}{l}#1\end{tabular}}
\def\tabc#1{\begin{tabular}{c}#1\end{tabular}}
\def\und #1#2{\underbrace{#1}_{#2}}
\def\undl#1#2{\underbrace{#1}_{\tabl{#2}}}
\def\undc#1#2{\underbrace{#1}_{\tabc{#2}}}
\def\rarr{\ColorRed{⇒}}
\def\P#1{\left( #1 \right)}
% «defs-Aipim» (to ".defs-Aipim")
% (c2m251introp 5 "defs-Aipim")
% (c2m251introa "defs-Aipim")
\def\und#1#2{\underbrace{#1}_{#2}}
\def\setdepthto#1#2{\setbox1\hbox{$#2$}%
\dp1=#1%
\box1}
%
\sa{[Aipim]} {\CFname{Aipim}{}}
\sa {Aipim} {\sqrt{a^2+b^2}=a+b}
\sa {Aipim u}{ % Aipim with "\und"s
\sa{a 0} {\setdepthto{2pt}{a}}
\sa{b 0} {\setdepthto{2pt}{b}}
\sa{a} {\und{\ga{a 0}}{3}}
\sa{b} {\und{\ga{b 0}}{4}}
\sa{a^2} {\und{\ga{a}^2}{9}}
\sa{a^2} {\und{{\ga{a}}^2}{9}}
\sa{b^2} {\und{{\ga{b}}^2}{16}}
\sa{a^2+b^2 0} {\und{\ga{a^2}+\ga{b^2}}{25}}
\sa{a^2+b^2} {\setdepthto{0pt}{\ga{a^2+b^2 0}}}
\sa{sqrt(a^2+b^2) 0} {\sqrt{\ga{a^2+b^2}}}
\sa{sqrt(a^2+b^2) 1} {\setdepthto{50pt}{\ga{sqrt(a^2+b^2) 0}}}
\sa{sqrt(a^2+b^2)} {\und{\ga{sqrt(a^2+b^2) 1}}{5}}
\sa{a+b} {\und{\ga{a}+\ga{b}}{7}}
\sa{sqrt(a^2+b^2)=a+b} {\und{\ga{sqrt(a^2+b^2)} = \ga{a+b}}{\False}}
\ga{sqrt(a^2+b^2)=a+b}
}
% (find-LATEX "2021emacsconf.tex" "defs")
\def\incgr#1#2{\includegraphics[#1]{2021emacsconf/#2}}
\def\incgr#1#2{\includegraphics[#1]{2025adapting-lean-tuts/#2}}
% _____ _ _ _
% |_ _(_) |_| | ___ _ __ __ _ __ _ ___
% | | | | __| |/ _ \ | '_ \ / _` |/ _` |/ _ \
% | | | | |_| | __/ | |_) | (_| | (_| | __/
% |_| |_|\__|_|\___| | .__/ \__,_|\__, |\___|
% |_| |___/
%
% «title» (to ".title")
% (adabp 1 "title")
% (adaba "title")
\thispagestyle{empty}
\begin{center}
\vspace*{0.5cm}
\begin{tabular}{c}
\phantom{a}\\[-15pt]
{\Large {\bf Adapting Lean Tutorials}} \\[1pt]
{\Large {\bf to the Brazilian Case}} \\[1pt]
\\[-9pt]
\ColorGray{(talk @ XXI EBL)}\\[-5pt]
\\[-9pt]
{\tiny\url{http://anggtwu.net/math-b.html#2025-ebl}}\\[8pt]
Eduardo Ochs \\
Serra Negra, 2022may13 \\
\end{tabular}
\end{center}
\newpage
% «links» (to ".links")
% (adabp 2 "links")
% (adaba "links")
% {\bf Links}
% \scalebox{0.6}{\def\colwidth{16cm}\firstcol{
% }\anothercol{
% }}
\newpage
% «abstract» (to ".abstract")
% (adabp 2 "abstract")
% (adaba "abstract")
% (find-angg "EBL2025/Submission-Template-EN.tex")
{\bf Abstract}
\def\cite #1{\CFname{#1}{}}
\def\bibitem#1{\CFname{#1}{}}
\scalebox{0.75}{\def\colwidth{14cm}\firstcol{
Lean4 (\cite{Overview}) is a proof assistant that is also a
general-purpose language, and that has ``metaprogramming facilities''
(\cite{Meta}) that let people extend its syntax in many ways. It is
becoming very popular, and the page \cite{Courses} has links to more
than 40 courses on Lean, or using Lean.
\msk
{\sl I don't think that these courses are adequate for Brazilians.}
They all start from some point like ``everybody knows VSCode'' and
they move to non-trivial ideas very quickly. But ``everybody knows the
programs such and such'' is not true in Brazil at all; half of the
Brazilian logicians that I know only use computers in a very basic
way, and here ``knowledge about programs does not propagate'' (see
\cite{EmacsConf2024}).
\msk
In this presentation I will show how I adapted the approach in
\cite{EmacsConf2024} -- that I use to teach Maxima to undergraduate
students with {\sl very} little experience with computers -- to create
a short workshop on Lean (\cite{Oficina0}) that teaches people how to
install Lean4, how to navigate its manuals, how to understand its
interface, and how to run and modify simplified versions of some
examples from the main books on Lean.
}\anothercol{
}}
\newpage
% «abstract-bib» (to ".abstract-bib")
% (adabp 3 "abstract-bib")
% (adaba "abstract-bib")
{\bf Abstract (2)}
\scalebox{0.8}{\def\colwidth{16cm}\firstcol{
\par \bibitem{Overview} {\em Lean Documentation Overview}:
\par \url{https://lean-lang.org/lean4/doc/}.
\ssk
\par \bibitem{Meta} {\em Metaprogramming in Lean4}:
\par \url{https://leanprover-community.github.io/lean4-metaprogramming-book/}
\ssk
\par \bibitem{Courses} {\em Courses using Lean}:
\par \url{https://leanprover-community.github.io/teaching/courses.html}
\ssk
\par \bibitem{EmacsConf2024} {\em Emacs, eev, and Maxima -- Now!}:
\par \url{http://anggtwu.net/emacsconf2024.html}.
\ssk
\par \bibitem{Oficina0} {\em Oficina de Lean4 -- versão 0}:
\par \url{http://anggtwu.net/2024-lean4-oficina-0.html}.
}\anothercol{
}}
\newpage
% «o-puro» (to ".o-puro")
% (adabp 4 "o-puro")
% (adaba "o-puro")
{\bf O PURO
(Pólo Universitário de Rio das Ostras / UFF):
}
% (find-TH "2025-voce-atropelou-a-selana" "as-fotos")
% (lodp 2 "dm-at-puro")
% (loda "dm-at-puro")
$$\includegraphics[height=5.5cm]{2019logicday-PURO.pdf}$$
\newpage
% «introducao» (to ".introducao")
% (adabp 5 "introducao")
% (adaba "introducao")
{\bf Introdução}
As minhas matérias principais são Cálculo 2 e 3
pra Engenharia de Produção (EP) e pra
Ciência da Computação (CC).
\msk
Em 2022.1 -- primeiro semestre pós-pandemia --
alguns colegas meus abriram um processo contra mim
``porque eu estava aprovando alunos que não sabiam
o suficiente''.
\msk
Agora eu começo C2 com uns ``testes de nivelamento''
que me dão provas documentais que de que os alunos
estão chegando em C2 sem saberem nada da matéria do
Ensino Médio e nada de Cálculo 1.
\msk
($→$ e eu uso o Maxima)
\newpage
% «o-puro-e-um-lixo» (to ".o-puro-e-um-lixo")
% (adabp 6 "o-puro-e-um-lixo")
% (adaba "o-puro-e-um-lixo")
{\bf O PURO é um lixo e o meu
departamento mais ainda}
\msk
Agora os primeiros links em destaque
na minha página são estes:
\def\HEAD{\par\standout{2025:} }
\def\dlink#1#2{\href{#1}{#2}}
\bsk
\HEAD \dlink{2024.2-PR2.html\#o-puro-e-um-lixo}{O PURO é um lixo}
(\dlink{2025.1-C2.html\#o-puro-e-um-lixo}{links})
\HEAD \dlink{2025-oficio-da-EP-resp.html\#macaco}{Derive como um macaco}
\HEAD \dlink{2025-voce-atropelou-a-selana.html}{Você atropelou a Selana}
\HEAD \dlink{2025-caraca-ate-o-walter.html}{Caraca, até o Walter???}
\bsk
O ``derive como um macaco'' é sobre
reclamações dos alunos.
\ssk
{\bf Recomendo muito!!!}
\newpage
% «teste-niv-deriv» (to ".teste-niv-deriv")
% (adabp 7 "teste-niv-deriv")
% (adaba "teste-niv-deriv")
% (c2m251tn2p 3 "por-favor-escrevam")
% (c2m251tn2a "por-favor-escrevam")
% (patp 10 "substituicao")
% (pata "substituicao")
\scalebox{1.1}{\def\colwidth{10cm}\firstcol{
{\bf Teste de nivelamento (Cálculo 2)}
\ssk
Por favor escrevam nesta folha...
\begin{itemize}
\item seu nome (legível),
\item com quem você fez C1 (e GA e Prog1), em que semestre foi, e que
livros você usou -- e se você fez várias vezes fale sobre cada vez,
\item a questão e tudo que você conseguir fazer pra resolver ela. A
questão é:
%
$$\ddx \,f(\sen(x^4) + \ln x) \;=\; \ColorRed{?}$$
\end{itemize}
}\anothercol{
}}
\newpage
% «teste-niv-diag» (to ".teste-niv-diag")
% (adabp 8 "teste-niv-diag")
% (adaba "teste-niv-diag")
% (patp 12 "um-diagrama")
% (pata "um-diagrama")
\def\pmatt#1#2{\pmat{#1 \\\\[-10pt] #2}}
\sa{nw}{\pmatt{\ddx f(g(x)) = }{ f'(g(x))g'(x))}}
\sa{ne}{\pmatt{\ddx f(42x) = }{ f'(42x)·42}}
\sa{sw}{\pmatt{\ddx \sin(g(x)) = }{ \cos(g(x))g'(x)}}
\sa{se}{\pmatt{\ddx \sin(42x) = }{ \cos(42x)·42}}
\scalebox{1.0}{\def\colwidth{10.5cm}\firstcol{
$\scalebox{1.25}{$
\ddx \,f(\sen(x^4) + \ln x) \;=\; \ColorRed{?}
$}
$
%\vspace*{0.25cm}
$$\scalebox{1.25}{$
\begin{array}{ccc}
\ga{nw} & → & \ga{ne} \\\\[-5pt]
↓ & \searrow & ↓ \\\\[-5pt]
\ga{sw} & → & \ga{se} \\
\end{array}
$}
$$
\vspace*{0.25cm}
Os passos intermediários são óbvios
pra gente -- mas pros alunos não!!!
}\anothercol{
}}
\newpage
% «teste-niv-lim» (to ".teste-niv-lim")
% (adabp 9 "teste-niv-lim")
% (adaba "teste-niv-lim")
% (c2m251tnp 3 "por-favor-escrevam")
% (c2m251tna "por-favor-escrevam")
% (c2m251tnp 3 "defs-teste")
% (c2m251tna "defs-teste")
{\bf Outro teste de nivelamento}
\scalebox{0.95}{\def\colwidth{11cm}\firstcol{
Lembre que:
%
$$\begin{array}{rcl}
f'(a) &=& \D\lim_{ε \to 0} \frac {f(a+ε)-f(a)} {ε} \\ \\[-10pt]
\D\left.\P{\ddx f(x)}\right|_{x=a}
&=& \D\lim_{ε \to 0} \frac {f(a+ε)-f(a)} {ε} \\
\end{array}
$$
Cada limite abaixo representa a derivada de certa função $f$ em certo
número $a$. Diga o que são $f$ e $a$ em cada caso.
%
$$\begin{array}{ll}
\text{a)} & \D\lim_{h \to 0} \frac {(1+h)^{10} - 1} {h} \\ \\[-10pt]
\text{b)} & \D\lim_{h \to 0} \frac {\sqrt[4]{16+h}-2} {h} \\
\end{array}
$$
}\anothercol{
}}
\newpage
% «aipim» (to ".aipim")
% (adabp 10 "aipim")
% (adaba "aipim")
% (c2m251introp 5 "aprender-A-e-B")
% (c2m251introa "aprender-A-e-B")
{\bf Aipim}
\scalebox{1.0}{\def\colwidth{6.5cm}\firstcol{
Seja:
%
$$\ga{[Aipim]} \;=\; \P{\ga{Aipim}}$$
Todo mundo sabe que:
$$\ga{Aipim u}$$
}\def\colwidth{5cm}\anothercol{
{}
...e mesmo assim os alunos de C2 continuam usando \standout{MONTES} de
aipins nas suas contas, e eles não entendem o que tá errado...
\msk
Veja o ``Derive como um macaco''.
}}
\newpage
% «antonio» (to ".antonio")
% (adabp 11 "antonio")
% (adaba "antonio")
{\bf Uma desculpa pra aprender Lean}
\scalebox{1.0}{\def\colwidth{11cm}\firstcol{
{}
\vspace*{0cm}
Um dos objetivos do curso de C2 é a gente aprender a lidar
com algumas contas muito grandes e muito complicadas...
\ssk
A gente quer aprender a fazer contas fáceis de justificar
e de revisar...
\ssk
Mas justificar ``\standout{no sentido Antônio}'' não serve!!!
\ssk
O que vai dar pontos na prova é vocês saberem justificar
os passos de vocês ``\standout{no sentido calc sem rw}''...
}\anothercol{
}}
\newpage
% «calc» (to ".calc")
% (adabp 12 "calc")
% (adaba "calc")
% (find-fline "~/LATEX/2025adapting-lean-tuts/calc-with-rw.pdf")
% (find-fline "~/LATEX/2025adapting-lean-tuts/calc-without-rw.pdf")
% (emacsconf2021p 3 "screenshots")
% (emacsconf2021a "screenshots")
\screenshotgeometry
%\pagecolor{black}
\incgr{width=\paperwidth}{calc-with-rw.pdf}
\newpage
\incgr{width=\paperwidth}{calc-without-rw.pdf}
\originalgeometry
%\pagecolor{white}
% \newpage
% «manga» (to ".manga")
% (adabp 14 "manga")
% (adaba "manga")
% (c2m251introp 6 "manga")
% (c2m251introa "manga")
{\bf Manga}
\scalebox{1.0}{\def\colwidth{11cm}\firstcol{
\vspace*{-0.25cm}
O `$=$' é uma manga.
Outra manga:
%
$$\begin{array}{rcl}
2(y+z) & \rarr & 2·(y+z) \\
f(y+z) & \rarr & f \; \standout{ap} \; (y+z) \\
(a+b)[a:=42] & \rarr & (a+b) \; \standout{s} \; [a:=42] \\
\end{array}
$$
%\vspace*{-0.25cm}
$$\scalebox{0.9}{$
(\undl{a+b=b+a}{expressão \\ original; \\ caso geral; \\ ``antes''})
\undl{\bmat{a:=42}}{substituição: \\ $a$ \standout{vira} 42}
= \;\;
(\undl{42+b=b+42}{expressão nova; \\ caso particular; \\ ``depois''})
$}
$$
}\anothercol{
}}
\newpage
% «plonk» (to ".plonk")
% (adabp 15 "plonk")
% (adaba "plonk")
% (find-eev2024lsubs "8:50")
% (find-TH "emacsconf2024")
{\bf ``Emacs, eev, and Maxima -- Now!''}
\scalebox{0.8}{\def\colwidth{12cm}\firstcol{
\vspace*{-0.1cm}
\url{http://anggtwu.net/emacsconf2024.html}
\ssk
Esse foi o título da minha apresentação na EmacsConf 2024...
O ``Now!'' queria dizer:
\ssk
\begin{quote}
``...in less than one hour and even for people \\
who have never seen a terminal in their lives.''
\end{quote}
Outra idéia importante da apresentação: ``plonk''.
% (find-eev2024lsubs "10:02")
\begin{quote}
I prefer this simpler definition here... \\
for me ``plonk'' is the sound \\
that a person makes when he, or she, or they \\
hits the bottom of my list of priorities.
\end{quote}
Eu aprendi a plonkar alunos que não conseguem perguntar
e ajustei o meu material pra ser fácil perguntar.
}\anothercol{
}}
\newpage
% «outros-cursos» (to ".outros-cursos")
% (adabp 16 "outros-cursos")
% (adaba "outros-cursos")
{\bf Outros cursos de Lean}
\scalebox{0.9}{\def\colwidth{14cm}\firstcol{
Durante a pandemia eu fiz um curso de Lean --
o do Francesco Noseda, da UFRJ.
\ssk
Nesse curso Lean deixou de ser algo impossível pra mim --
mas eu aprendi pouco, eu passei meses quebrando a cara
com coisas que deveriam ser óbvias pro público alvo
do curso mas pra mim eram dificílimas...
\bsk
Aqui tem um monte de outros cursos de Lean:
{\footnotesize
\url{https://leanprover-community.github.io/teaching/courses.html}
}
\bsk
{\sl Como fazer algo menos frustrante que esses cursos
e ficar amigo das pessoas certas -- que interagem mais?}
\bsk
WSL $→$ Debian $→$ Emacs $→$ eev $→$ Maxima
$→$ executable notes $→$ Lean
}\anothercol{
}}
\newpage
% «executable-notes» (to ".executable-notes")
% (adabp 17 "executable-notes")
% (adaba "executable-notes")
% (find-fline "~/LATEX/2025adapting-lean-tuts/executable-notes.pdf")
% (emacsconf2021p 3 "screenshots")
% (emacsconf2021a "screenshots")
\screenshotgeometry
\incgr{width=\paperwidth}{executable-notes.pdf}
\originalgeometry
\newpage
% «plonkando-aprender» (to ".plonkando-aprender")
% (adabp 18 "plonkando-aprender")
% (adaba "plonkando-aprender")
% (find-telegachat "@leanlangbr#390" "usando um editor mais comum")
% (find-telegachat "@leanlangbr#405" "Alias, melhor: nao vale a pena eu aprender VS Code SOZINHO")
{\bf Plonkando o povo do ``Não tem muito o que aprender''}
\scalebox{0.65}{\def\colwidth{18cm}\firstcol{
\par [Celso:] Se a ideia é criar entusiasmo acerca da linguagem, eu acho que o
\par melhor seria introduzir eles usando um editor mais comum, tipo o
\par VSCode. Querendo ou não, familiaridade é muito importante quando nós
\par estamos aprendendo algo, e introduzir a uma linguagem e a um editor ao
\par mesmo tempo talvez seja muita coisa desconhecida ao mesmo tempo.
\msk
\par [Eu:] ...mas nenhum desses alunos [da CC e da EP do PURO] tem interesses
\par em comum com os outros, e eles nao tem uma cultura de aprender juntos,
\par de ensinarem coisas uns pros outros, e de disponibilizarem as coisas que
\par eles fizeram em blog posts ou no github.
\par Entao acho que nao vale a pena eu aprender VS Code pra tentar
\par interagir com esses alunos.
\par Alias, melhor: nao vale a pena eu aprender VS Code SOZINHO pra tentar
\par interagir com esses alunos. Mas se algum dia eu ficar amigo de alguem
\par que saiba usar VS Code e que tope me ensinar e' outra historia.
\msk
\par [Thiago:] Não quis dizer que lean é fácil, quis dizer que usar o lean no vscode é fácil
\par \ColorRed{Não tem muito o que aprender}
\msk
\par [Eu:] Mas uma das minhas segundas intenções com essa oficina é fazer com que pessoas
\par que usam VSCode ou neovim façam oficinas explicando como usar o Lean neles
}\anothercol{
}}
\newpage
% «lean-e-haskell» (to ".lean-e-haskell")
% (adabp 19 "lean-e-haskell")
% (adaba "lean-e-haskell")
{\bf Lean como um Haskell melhorado}
\scalebox{0.9}{\def\colwidth{10cm}\firstcol{
O que é o Lean?
Ele pode ser usado como proof assistant,
Ele pode ser usado como uma linguagem ``normal'',
Ele é um Haskell melhorado e com menos mangas,
Ele tem um fórum muito bom no Zulip Chat,
A sintaxe dele é extensível (``metaprogramming''),
Ele pode falar com programas externos...
\bsk
Exemplo:
``Tactics \& Keyframes: Visualizing Lean 4 Proofs
in Blender''
(David Renshaw, 2024)
\ssk
\url{http://www.youtube.com/watch?v=KuxFWwwlEtc}
}\def\colwidth{5cm}\anothercol{
\msk
\incgr{height=2cm}{lean-maze.pdf}
}}
\newpage
% «em-poucas-horas» (to ".em-poucas-horas")
% (adabp 20 "em-poucas-horas")
% (adaba "em-poucas-horas")
% (find-1stclassvideo-links "2024lean4of0")
% (find-1stclassvideo-links "2024lean4of0a2")
{\bf O que a gente consegue aprender
de Lean em poucas horas?}
\scalebox{0.9}{\def\colwidth{16cm}\firstcol{
\vspace*{0cm}
\standout{Importante:} ``Aprender a fazer (com ajuda)''
é diferente de ``assistir um vídeo e dizer `ah, entendi!'\,''
\bsk
Resposta curta: a gente consegue aprender 1) a acessar
a documentação com elisp hyperlinks, 2) as teclas principais,
3) a rodar snippets, 4) a entender uns programas muito básicos, e
5) traduzir pra Lean demonstrações simples em Dedução Natural...
\bsk
Ta-daaaa:
\url{http://anggtwu.net/2024-lean4-oficina-0.html}
Essa página tem as legendas de um vídeo
e links pro vídeo e pra outras coisas!
}\anothercol{
}}
\newpage
% «natural-deduction-tc1» (to ".natural-deduction-tc1")
% (adabp 21 "natural-deduction-tc1")
% (adaba "natural-deduction-tc1")
\screenshotgeometry
\incgr{width=\paperwidth}{theorem-tc1.pdf}
\originalgeometry
\newpage
% «obrigado» (to ".obrigado")
% (adabp 22 "obrigado")
% (adaba "obrigado")
Obrigado --
e desculpem qualquer coisa! $\smile$
% «ideias» (to ".ideias")
% Eu trabalho num lugar que é um lixo
% Optativa de lambda-cálculo
% Courses using Lean
% Livros principais
% (find-lean4-intro "1. Download the five manuals")
% (find-lean4-intro "3. Test the five manuals")
% (patp 10 "substituicao")
% (pata "substituicao")
% (ebl2022p 14 "bottle-R")
% (ebl2022a "bottle-R")
\GenericWarning{Success:}{Success!!!} % Used by `M-x cv'
\end{document}
% (find-pdfpages2-links "~/LATEX/" "2025adapting-lean-tuts")
% Local Variables:
% coding: utf-8-unix
% ee-tla: "adab"
% ee-tla: "adab"
% End: