Oficina de Lean4 - versão 0 (legendas)

Link pro vídeo no Youtube: aqui.
As legendas dele em Lua estão aqui,
e o resto desta página tem uma conversão das legendas em Lua
pra um formato um pouco mais legível.
A minha página sobre eev e Lean4 é esta aqui: link.

Update: já definimos as datas da oficina!
Aula 1: 6a, 26/jul/2024, 15:00-17:00
Aula 2: 6a, 02/ago/2024, 15:00-17:00
Aula 3: 6a, 09/ago/2024, 15:00-17:00
Ela vai ser quase toda por Telegram e um pouquinho por Google Meet!

Links pra algumas coisas que eu menciono no vídeo:
"Tactics & Keyframes: Visualizing Lean 4 Proofs in Blender" (David Renshaw, 2024)
Página do Graham Hutton, página do "Programming in Haskell"
Historinha sobre "é óbvio", parte 1: Visaud#01:00 até 03:09
Historinha sobre "é óbvio", parte 2: Visaud#51:45 até 52:24
LuaTreeLean: https://github.com/edrx/LuaTreeLean
PDF com meus os diagramas: .tex.html, PDF, .zip
Meu mini-tutorial de Emacs Lisp: (find-elisp-intro)
Fale comigo se você estiver interessado na oficina!

Aqui tem algumas gravações de usuários avançados usando Lean -
mas eu tou tentando preparar exercícios que todo mundo consiga fazer!
Instalação do Emacs e do eev no Windows: (find-windows-beginner-intro)
Instalação do Lean (versão muito preliminar): (find-lean4-intro)

Links pros 5 "livros" principais sobre Lean:

(find-fplean4doc "introduction") (find-lean4doc "whatIsLean") (find-leanmetadoc "main/01_intro") (find-tclean4doc "title_page") (find-tpil4doc "introduction")

Um diagrama do vídeo:

Legendas do vídeo:

00:00
00:02 Oi, gente! O meu nome é Eduardo Ochs, e eu tou
00:05 pretendendo dar uma oficina de Lean4
00:08 daqui um tempo... e esse vídeo é para
00:10 explicar algumas coisas que seriam
00:11 difíceis de explicar só por uma página
00:14 na internet.

00:15 Os dados da oficina vão estar todos
00:17 aqui nessa URL, e essa daqui é minha
00:20 página sobre Lean4.

00:22 Primeiro: o que que é o Lean4?
00:24 O Lean4 é parecido com Haskell, mas
00:27 ele é bem mais fácil de instalar, e tem
00:30 uma interface muito bacana que eu vou
00:32 mostrar daqui a pouco. Ele pode ser usado
00:34 como proof assistant - muita gente pensa
00:38 nele como proof assistant, só que eu ainda
00:40 não sei usar ele como proof assistant...
00:42 eu comecei a aprender ele porque eu queria
00:46 usar ele como proof assistant pra umas
00:47 coisas super complicadas, e...
00:50 ainda não sei o suficiente para isso...

00:52 mas tou adorando ele como uma linguagem
00:54 parecida com Haskell, e mais legal, com uma
00:58 interface bacana, e tal...

01:00 e o mais importante é que ele é muito
01:02 extensível - no sentido de que é fácil
01:04 você definir sintaxes novas nele... definir
01:08 mini-linguagens, DSLs, todas essas coisas
01:11 assim... se vocês quiserem explicações pra
01:13 isso tem nesse manual daqui, já vou
01:15 explicar qual é...

01:17 então, um dos manuais principais do Lean4
01:19 é o "Metaprogramming in Lean4",
01:22 e aí um dos capítulos
01:25 explica essa história de definir as
01:29 sintaxes novas - nessa seção daqui.

01:36 Voltando...
01:42 Primeiro: quem é o público alvo dessa
01:45 oficina?
01:48 Vai ser uma oficina muito básica, e
01:52 a ideia é que ela vai ser direcionada
01:54 pra pessoas que tentaram aprender Haskell
01:57 mas que empacaram mais ou menos nos mesmos
01:59 lugares que eu.

02:00 A partir de um determinado ponto os
02:02 livros começam a mostrar umas coisas
02:04 super complicadas e meio que exigir que
02:06 a gente entenda todos os detalhes delas
02:08 de cabeça... eles não dão nenhuma
02:10 informação sobre como a gente poderia
02:12 fazer as "contas" no papel pra conseguir
02:16 entender os detalhes daquilo.

02:17 Então - aqui tem um exemplo. Um
02:21 amigo meu que tá trabalhando na Holanda...
02:25 uma das tarefas dele como pós-doc é
02:29 orientar os alunos que estão fazendo
02:32 curso de Haskell lá... e eles usam o livro
02:36 do Hutton, então eu tentei aprender a usar
02:38 livro do Hutton também... a capa dele é essa,
02:42 aqui tá o índice do livro...
02:46 e o capítulo 12 do livro é o capítulo
02:50 onde ele começa a explicar mônadas.

02:53 E aí ele...
02:56 define umas coisas que eu só fui entender agora...
03:01 eu já tentei decifrar esse capítulo várias
03:02 vezes nos últimos três ou quatro anos e só
03:05 comecei a entender agora...

03:07 então, ele tem essas figurinhas aqui para
03:09 explicar o que que é uma "state monad".
03:12 E aí ele define
03:14 essa coisa daqui, ó...
03:20 ele diz que a gente vai definir um tipo
03:22 novo desse jeito daqui...
03:23 e depois uma função "app", que usa esse tipo...
03:27 depois uma função "fmap", que é uma instância
03:31 do funtor ST, whatever that means...
03:34 e aí ele põe essa figurinha daqui.

03:37 Até hoje de tarde eu não fazia a menor
03:39 ideia de se essa figura era uma coisa
03:40 precisa ou não.

03:42 Se fosse certamente estavam faltando
03:44 muitos detalhes aqui, e
03:46 eu ainda não tinha certeza de como
03:49 completar esses detalhes.

03:51 Então... deixa eu mostrar uma
03:53 figura aqui.

03:56 Essa primeira definição... essas duas
04:00 definições daqui, essa e essa, estão nesse
04:04 primeiro diagrama.

04:06 Então, no livro do Hutton
04:07 elas aparecem como essas três linhas
04:09 daqui - essa definição de um newtype,
04:12 depois o tipo da da função "app", depois a
04:14 definição da "app" em si...

04:16 e aí esse tipo de figura daqui
04:17 me ajudou muito a decifrar essas coisas.

04:20 Eu pego essa expressão daqui de baixo,
04:22 e embaixo de cada subexpressão dela
04:24 eu escrevo qual é o tipo dela.

04:27 O ideal seria fazer uma animação
04:30 dizendo quais são os tipos que eu
04:31 descubro primeiro e como é que a
04:34 inferência de tipos funciona, e como é
04:36 que a gente vai descobrindo tudo aos
04:38 poucos... mas nesse caso aqui eu ainda não
04:40 fiz a animação.

04:42 Então, a grande dificuldade para mim
04:44 foi entender o que é essa operação S daqui
04:46 e esse underbrace daqui...

04:51 e o legal é que quando
04:53 eu faço esse tipo de diagrama eu consigo
04:55 apontar pra um underbrace e
04:57 dizer: é esse o underbrace que eu
05:00 ainda não tenho certeza... e depois de
05:02 horas eu descobri que se eu
05:05 escrevesse esse underbrace desse jeito
05:07 daqui... desculpa, esse underbrace daqui...
05:12 usando essa definição de newtype aqui, que diz
05:14 que "ST a" é sempre equivalente a
05:16 S (State→(a,State)),
05:18 aí tudo ficava claro... aí as
05:22 regras não ficavam mais tão
05:25 misteriosas.

05:27 Então, voltando.
05:30 Até pouquíssimo tempo atrás eu não sabia
05:32 decifrar
05:34 trechos difíceis do Hutton - eu não
05:38 sabia que ferramentas usar para
05:40 completar os detalhes deles... e esse tipo
05:42 de diagrama tem me ajudado muito.

05:45 Agora vem o diagrama... opa, peraí...
05:49 ah deixa eu mostrar o diagrama da página
05:52 seguinte... aqui.
05:55 Lembra que agora há pouco eu mostrei
05:57 essa figurinha no livro do Hutton
06:00 e disse que até pouco tempo atrás eu não
06:01 fazia ideia de se essa figura era só uma...
06:06 se ela era informal ou não...
06:08 então, nessa página o o Hutton introduz
06:13 algumas linhas a mais, aqui...

06:15 ele diz que a gente vai definir o fmap desse
06:17 jeito daqui, e aí ele mostra essa figura como
06:20 se fosse óbvia... e para mim ela não é!
06:23 Eu preciso fazer todas essas type
06:25 inferences daqui para descobrir qual é o
06:27 tipo
06:28 da g da st, da s, da x, da s', etc, e
06:33 das outras expressões que são compostas
06:35 a partir delas... e aí quando eu descubro
06:38 todos esses tipos daqui eu consigo
06:39 transformar esse diagrama daqui num
06:41 diagrama que tem não só esses símbolos
06:44 que são nomes de termos, como esses tipos
06:48 daqui...
06:50 então esse s daqui é de tipo State
06:52 essa coisa daqui é de tipo ST a, etc...
06:56 e aí tudo fez sentido para mim.

07:00 Então, voltando... agora eu preciso contar uma
07:02 historinha, tá... eu vou contar ela de um
07:04 jeito bem resumido e eu vou botar o link
07:06 do lugar onde vocês podem ler o texto dela.

07:09 Há um tempo atrás eu fiz dois
07:11 vídeos sobre didática... um deles ficou
07:14 muito bom e outro tem só alguns trechos bons.
07:16 Esse vídeo é o que tem alguns trechos bons.

07:18 E ele tem essa historinha que eu
07:22 acho bem importante. É o seguinte... eu
07:25 não vou ler ela toda agora, mas é
07:28 uma história sobre alguém... um
07:30 professor que ensina uma coisa super
07:31 difícil, um aluno não entende e ele diz:
07:34 "mas isso é óbvio!" Aí o aluno diz:
07:38 "não é óbvio não!"... mas o aluno vai
07:40 pra casa pensar, ele pensa, pensa, pensa muito,
07:42 depois no dia seguinte ele volta e ele
07:46 virou uma pessoa para quem aquilo é
07:47 óbvio. Ele não sabe explicar pra as
07:49 outras pessoas quais são os detalhes
07:51 daquilo, ele só sabe dizer pras pessoas
07:54 "ah, isso é óbvio!"... mas ele virou a
07:57 pessoa para quem isso é óbvio.

08:00 Eu não gosto dessa ideia de aprender coisas
08:02 complicadas e virar uma pessoa que só
08:04 sabe dizer "ah, isso é óbvio!", e e eu tou há
08:07 vários anos trabalhando em alternativas
08:09 pra isso. Essa alternativas são descobrir
08:12 os diagramas que faltam e encontrar um
08:16 jeito mais ou menos mecânico e formal de
08:19 produzir esses diagramas que faltam.

08:21 Então, essa oficina de Lean
08:24 vai ser principalmente sobre um modo de
08:29 produzir esses diagramas que faltam e de
08:31 apresentar as coisas que os livros sobre Lean
08:33 apresentam de um jeito muito difícil
08:36 com esses diagramas.

08:38 Então vou mostrar os pontos em que eu
08:40 empacava... e que ficaram
08:42 muito mais simples depois que eu aprendi
08:43 a fazer diagramas. Então: não tenho
08:45 certeza se esses diagramas vão funcionar
08:48 pra outras pessoas - é isso que eu quero
08:50 testar - mas são os diagramas que
08:52 funcionaram para mim.

08:54 E aí eu quero
08:56 descobrir quais são as dificuldades dos
08:57 outros, se isso faz sentido, se elas têm
09:00 os tipos delas de diagramas e coisas
09:03 do gênero...

09:04 Então, tem um monte de técnicas
09:06 didáticas por trás disso daqui...
09:09 e eu também vou mostrar como eu
09:11 transformei os exemplos dos livro de Lean
09:14 em exemplos que são mais fáceis de testar
09:16 passo a passo.

09:18 E aí aqui tem tem um
09:20 caso muito mais simples de
09:23 de situação em que eu fiz algo parecido
09:26 com essa técnica...
09:29 eu peguei coisas que eram explicadas de
09:31 um jeito complicado, com exemplos grandes...
09:33 e desmontei os exemplos em exemplos
09:35 muito simples. Então, por exemplo se a
09:37 gente quiser aprender o que que é essa
09:38 expressão aqui em Lisp eu posso
09:41 desmontar ela em várias expressões
09:42 pequenininhas, e aí eu posso executar
09:45 cada uma dessas expressões - quando eu
09:47 executo ela o resultado aparece aqui
09:49 embaixo... e aí com isso eu tenho todas as
09:51 expressões visíveis de uma vez, e eu
09:54 consigo comparar duas expressões, ver
09:56 onde é que tão as dificuldades ver onde
09:58 aparece algum conceito novo, e coisas assim...

10:02 e eu vou mostrar como fazer isso com os
10:06 exemplos dos manuais de Lean
10:09 de um modo que todos os pedaços
10:14 deles ficam visíveis ao mesmo tempo e é
10:16 muito fácil checar detalhes.

10:18 O meu plano é fazer a oficina em
10:21 três aulas só. A primeira aula vai ser
10:24 uma aula sobre instalação do Lean
10:26 e de outras coisas - a gente vai
10:29 usar o Emacs e o eev, mas eu tenho um
10:34 método para instalar eles no no Windows...

10:39 Então, nessa primeira oficina... ela
10:43 demora um pouco, porque alguns passos são
10:44 demorados, mas vocês podem fazer outras
10:46 coisas ao mesmo tempo... vai ter alguns
10:48 momentos em que
10:50 a gente vai ver que o computador vai
10:52 passar 20 ou 30 minutos instalando
10:54 alguma coisa, aí vocês vão fazer outra
10:57 coisa, e quando voltarem tá tudo
10:58 instalado.

11:00 Depois que tiver tudo instalado a gente
11:02 vai poder usar esse tipo de hiperlink
11:04 daqui pra ir pros manuais principais.

11:06 Então: o Lean tem cinco manuais principais.
11:10 Por exemplo esse aqui vai pro Functional
11:13 Programing in Lean, pra uma seção dele que é a
11:16 introdução dele... e ele abre esse manual
11:19 no browser. Então, repara: isso aqui é o
11:22 título do manual, "Functional Programing...",
11:25 aqui tem o índice, e a gente abriu a
11:27 introdução...

11:29 e aqui tem um outro manual que é
11:32 o "Lean Manual",
11:35 aqui tem o "Metaprograming in Lean4",
11:39 aqui tem o "Type Checking in Lean 4",
11:43 que é super técnico mas acho que os
11:46 matemáticos vão ter algumas dúvidas que
11:48 vão ser respondidas aqui, e aqui tem
11:51 o "Theorem Proving in Lean4", que é um dos
11:56 mais básicos.

11:58 E... a coisa que eu mais gosto no Emacs
12:02 é que dá para criar hiperlinks para tudo
12:06 e os hiperlinks são esses programinhas
12:08 de uma linha em Emacs Lisp. E eu
12:11 já dei um montão de oficinas sobre isso,
12:13 já melhorei meu material sobre isso
12:15 bastante, hoje em dia as pessoas acham
12:17 super fácil de aprender.

12:19 Então aqui tem um exemplo mais exótico.
12:22 É um hiperlink que vai abrir um vídeo numa
12:25 determinada posição. Esse vídeo é
12:27 espetacular - é um vídeo que foi feito há
12:28 poucas semanas atrás...

12:32 sobre... bom deixa eu ver o título dele...
12:36 eu esqueci o título. Vou fazer isso
12:41 aqui... é alguma coisa como
12:44 "Visualizing Proofs in Lean using Blender".

12:47 Então é um cara que usa Lean para
12:51 gerar código que usa o Blender
12:54 para fazer animações... é muito
12:55 impressionante. E nesse trecho daqui, a
12:59 partir do 6:50, ele
13:05 mostra como é que ele estendeu a
13:07 linguagem do Lean pra ela reconhecer
13:10 essas posições do jogo de xadrez aqui em
13:13 caracteres Unicode...

13:20 E aí o programa
13:22 dele faz coisas tipo demonstrar que uma
13:24 determinada posição é um mate em cinco
13:26 jogadas, e
13:29 ele pega a prova que é gerada pelo Lean e
13:32 anima ela usando Blender.

13:35 Então dá para fazer esse tipo de
13:36 coisa. É difícil, né, mas já faz a gente
13:40 ter bastante vontade de aprender o Lean...
13:42 é o que eu tô tentando fazer agora.

13:44 Aqui tem um programa relativamente
13:47 básico, que eu fiz... opa, peraí,
13:53 caramba... ah tá, faltou isso.

13:57 Então, esse programa daqui chama uma
14:01 biblioteca que eu fiz... e deixa eu
14:04 primeiro mostrar uma coisa...
14:06 Ah, peraí, deixa eu só fazer uma
14:08 coisinha aqui...

14:12 Pronto. Uma coisa muito legal da
14:14 interface do Lean é que a gente tem duas
14:16 teclas, que eu vou chamar de "go to" e
14:19 "go back". Por exemplo, se eu tou com
14:22 cursor aqui, em cima desse "LuaTree" aqui,
14:26 e aperto a tecla de "go to" ele vai
14:29 pro arquivo LuaTree.lean; se eu aperto a tecla
14:33 de "go back" ele volta para cá.

14:37 Além disso o Lean tem esse tipo de
14:41 comando daqui, que gera uma
14:44 mensagem aqui na "echo area"...
14:46 deixa eu diminuir a fonte... em alguns
14:50 casos a mensagem é bem grande e eu
14:53 também posso pedir para ele mostrar
14:54 todas as mensagens de uma vez.

14:56 Então você bato f10 l l - opa, peraí,
14:59 não era isso...
15:02 se eu bato uma sequência misteriosa
15:06 de teclas ele mostra todas as mensagens
15:08 de uma vez...
15:10 e se eu passeio por várias linhas ele dá
15:13 um highlight na mensagem correspondente
15:14 à linha em que eu tou.

15:19 E essa última...
15:22 bom, aqui nesse programa eu defini
15:24 uma linguagenzinha que entende só as
15:27 operações "-" e "^" e números,
15:33 e a linguagem entende elas com a
15:36 precedência certa.

15:37 Então por exemplo, essa linha daqui
15:39 entende essa expressão daqui e
15:41 parentesisa ela de uma determinada
15:44 forma... essa aqui faz algo parecido mas
15:47 ela produz uma coisa num formato que
15:50 agora não quero explicar, e essa última
15:52 pega essa coisa no formato complicado
15:53 transforma ela numa árvore em 2D.

15:56 Tá, então eu tou mais ou menos nesse nível...
15:58 eu tou aprendendo fazer linguagens muito
16:01 simples, e eu tou tentando entender como é
16:03 que comandos do link são
16:06 definidos usando esse método...
16:11 o Lean começa com uma linguagem muito
16:14 básica e depois ele define um montão
16:17 de extensões escritas em Lean mesmo.

16:21 Então, vamos voltar...
16:24 eu tava aqui...
16:27 isso foi só uma demonstração.

16:31 Na primeira aula a gente vai aprender a
16:33 interface do Lean, que eu já mostrei
16:35 algumas coisas dela, e a gente vai
16:37 aprender uma outra coisa bacana que a
16:38 gente pode fazer no Emacs: a gente pode
16:41 acessar o meu conjunto de anotações
16:44 sobre Lean.

16:46 Por exemplo, esse link aqui
16:47 vai pro bloco sobre "coerção", que tá aqui...
16:51 toda essa parte aqui tem links
16:53 para documentação, sendo que alguns links
16:56 são um pouco mais estranhos... esse link
16:57 daqui é um link pro resultado de um grep:
16:59 ele vai procurar todas as
17:03 ocorrências disso aqui no código fonte
17:05 das bibliotecas básicas do Lean
17:11 e vai mostrar elas na tela... tá, então
17:14 quando eu tava aprendendo sobre coerção
17:16 eu usei esse tipo de coisa, e esses links
17:19 pro grep vão ser super úteis, e eu vou
17:21 mostrar porquê.

17:22 Então essas são as minhas
17:23 notas sobre coerção, e isso aqui é um
17:27 bloquinho, um snippet [de código Lean]...

17:29 se eu rodo esse comando
17:31 daqui ele abre o meu arquivo temporário
17:34 aqui à direita... deixa eu apagar o
17:37 conteúdo dele...

17:39 e ele bota isso aqui no clipboard do Emacs.
17:43 Aí eu posso ir para cá, bater a tecla de
17:46 "copy"m e ele copia essas coisas aqui pro
17:50 meu arquivo de teste,
17:54 e aí eu posso examinar o resultado
17:56 de cada coisa dessas.

17:58 Esse "#check" aqui ele pega esse termo daqui
17:59 e faz algumas expansões nele...

18:03 então: o "+" em
18:06 princípio não sabe somar um número
18:08 natural, que é esse 2, com um inteiro...

18:11 mas na verdade esse "+" daqui é
18:12 transformado num "'+' heterogêneo",
18:15 que pode receber objetos de dois tipos
18:17 diferentes, e se for necessário ele
18:19 aplica uma coerção em algum deles.

18:22 Então quando a gente pede pro #check mostrar
18:24 que termo é esse daqui ele mostra o termo
18:25 ligeiramente transformado, e mostra que o 2
18:28 recebeu um operador de coerção, aqui...

18:30 a gente também pode examinar
18:34 versões mais detalhadas disso e
18:36 descobrir exatamente qual coerção é
18:38 usada nesse ponto.

18:40 Aí aqui tem um exemplo muito pequeno,
18:42 muito menor do que os do manual...
18:43 de eu definindo dois tipos diferentes
18:48 e definindo uma coerção entre eles...
18:51 e aqui tem vários testes, tá, que eu não vou
18:53 detalhar agora.

18:54 Então, isso é só um exemplo de como as minhas
18:57 anotações têm hiperlinks e têm snippets.
19:01 Deixa eu voltar...

19:03 É isso que a gente vai aprender na primeira aula.
19:05 Então, na primeira aula a gente vai aprender
19:07 a acessar os manuais principais,
19:09 vai aprender o básico da interface,
19:10 vai aprender a apontar
19:14 pra posições de vídeos,
19:19 e a testar código que já existe...
19:21 por exemplo, os meus snippets.

19:23 Aí... eu acho que isso é o que cabe
19:27 na cabeça das pessoas na primeira aula.
19:29 Depois vai estar todo mundo cansado, e uma
19:32 semana depois a gente faz a aula 2, em
19:35 que a gente vai aprender as coisas
19:37 básicas da linguagem - que estão
19:39 explicadas num dos manuais do Lean, o
19:42 "Functional Programming in Lean".

19:44 Então a gente vai começar nessa
19:46 seção daqui,
19:48 "1.1 Evaluating Expressions", e vai
19:52 possivelmente até a seção 1.5, e eu vou
19:55 traduzir... mostrar para vocês
19:59 as minhas traduções de várias dessas
20:01 demonstrações [?] daqui, por exemplo isso...

20:06 o manual mostra vários trechinhos de
20:08 código - deixa encontrar um interessante...

20:11 e aí por exemplo eu juntei todos os
20:14 trechinho sobre structures num bloco só,
20:17 mostrei várias comparações entre várias
20:20 sintaxes possíveis, fiz um exemplo muito
20:22 mais simples que esse, e tal... então a
20:25 gente vai ver como testar isso...

20:27 e a gente vai considerar que os manuais
20:29 do Lean são a fonte definitiva,
20:30 escrita por pessoas que têm muita prática
20:33 em didática, só que
20:36 elas estão em países em que o ensino é
20:40 muito melhor, em que eles têm
20:43 turmas enormes em que pessoas estão
20:45 aprendendo essas coisas, e tal...

20:47 é o contrário da situação em que eu tou,
20:49 eu tou totalmente isolado, trabalhando num
20:51 campus muito lixo da UFF no interior do
20:54 Estado do Rio de Janeiro...

21:00 Então, outra coisa que a gente vai ver é
21:02 uma coisa que os livros apresentam num
21:05 formato bem difícil - eles dão exercícios
21:08 bem difíceis...

21:10 Eu imagino que todo mundo queira
21:12 aprender um pouquinho sobre
21:14 como usar Lean como
21:16 proof assistant...

21:19 Então a gente vai começar com exemplo muito
21:21 simples... eu prefiro explicar Curry-Howard
21:25 a partir desse exemplo simples daqui, que
21:26 só usa implicação e...

21:28 Peraí, vamos começar por aqui,
21:31 que é a versão em Dedução Natural dele.

21:33 então, isso aqui é o "e". Se eu sei que
21:37 P∧R é verdade eu sei que P é verdade,
21:40 se eu sei que P é verdade e P→Q é
21:42 verdade eu sei que Q é verdade...

21:45 Então, aqui tem a tradução dessa
21:48 demonstração simples em dedução
21:50 natural para uma demonstração em
21:53 conjuntos... então isso para mim é o
21:55 primeiro exemplo interessante de
21:57 Curry-Howard...

21:59 E aqui à esquerda a gente diz qual é o
22:02 elemento do conjunto se eu conheço um
22:04 elemento desse conjunto A'×B daqui -
22:06 o elemento p - então a primeira projeção,
22:11 πp, vai ser um elemento desse conjunto
22:12 daqui, A'.

22:14 Eu acho que essa notação daqui é
22:17 a notação mais familiar para
22:20 matemáticos, e a gente vai ver
22:24 que o Lean costuma usar uma convenção que
22:27 para mim é estranha - é uma convenção
22:29 usada pelo pessoal de linguagens
22:31 funcionais...

22:35 deixa eu pegar uma figura aqui...
22:35 aqui é um outro trecho daquele
22:39 vídeo que eu falei que é maravilhoso...

22:44 Em geral a gente quer aprender o Lean
22:48 como provador de teoremas
22:50 começando por "táticas".

22:52 Muita gente começa rodando o Lean
22:54 no browser, no tal do
22:56 "Natural Numbers Game" e aí aquilo é um
23:00 tutorial que já começa direto por táticas.

23:02 O meu primeiro contato com Lean
23:04 foi no meio da pandemia quando um cara
23:05 chamado Francesco Noseda, que é um professor
23:11 da UFRJ... ele deu um curso de Lean online
23:15 e eu participei, e no curso dele ele supunha
23:18 que as pessoas sabiam um bocado
23:21 sobre técnicas de demonstração em
23:24 Cálculo de Sequentes e Fitch, e apesar
23:28 que eu trabalho com Lógica a minha
23:29 formação é muito estranha - eu nunca tive
23:31 um curso formal disso...

23:33 então, eu sou meio ruim nessas coisas...
23:35 eu sou bom em Dedução Natural,
23:37 mas eu tenho pouca prática com
23:38 técnicas de demonstração, Cálculo de
23:40 Sequentes, coisas assim
23:42 formalizadas do jeito tradicional para
23:46 quem fez um curso de Lógica.

23:49 Então, eu ralei muito pra
23:51 entender aquilo, e eu fiquei com a sensação
23:52 de que faltavam diagramas. Nesse vídeo eu
23:55 consigo mostrar para vocês que tipo de
23:56 diagrama faltava.

23:58 No curso do Francesco e a gente não
24:03 conseguia... a gente via esse tipo de coisa
24:05 daqui - aqui tem um exemplo de que
24:08 hipóteses a gente tem num certo momento
24:12 e o que que a gente quer provar...

24:18 e nessa figura daqui ele mostra
24:21 que quando a gente roda essa tática daqui
24:23 o nosso conjunto de hipóteses e
24:27 a coisa que a gente quer provar mudam
24:29 desse bloquinho de cima para esse
24:31 bloquinho de baixo.

24:32 Então para mim quando a gente consegue
24:35 ver o "antes" e o "depois" na mesma
24:37 tela fica muito mais fácil de entender,
24:40 e na época do curso de Francesco ele não
24:43 mostrou isso, ele não tinha técnicas pra
24:45 mostrar isso... e eu passei dias tentando
24:48 fazer as figurinhas para conseguir
24:51 entender quais eram as táticas principais.

24:54 Agora, outro motivo pra gente
24:56 não aprender táticas nesse meu curso de
24:58 três aulas é que mesmo o Theorem Proving
25:03 Lean... deixa eu aumentar a letra de novo...
25:06 ele só ensina táticas no capítulo 5 dele.

25:10 Então, antes ele ensina a Teoria de
25:13 Tipos básica até quantificadores, outros
25:16 modos de demonstrar proposições simples...
25:18 as táticas só aparecem no capítulo 5.

25:21 Então, a gente vai aprender essas
25:26 coisas na aula 2, e na aula 2 eu
25:29 só vou supor que as pessoas sabem um
25:31 pouquinho de Matemática e têm uma noção de
25:34 tipos mesmo que seja de linguagens como C,
25:36 e já tentaram aprender Haskell e
25:40 quebraram a cara...

25:40 que elas têm uma noção de coisas
25:43 mais básicas, mas empacaram -
25:45 possivelmente nos mesmos lugares que eu.

25:47 Então, isso é aula 2, e eu
25:51 suponho que a aula 2 vai
25:53 interessar pra um bocado de gente...
25:56 e a aula 2 é desculpa para as
25:58 pessoas aprenderem a aula 1, e na aula 1
26:00 eu vou apresentar o Emacs e a
26:03 biblioteca que eu fiz pro Emacs, que é
26:05 essa biblioteca de hiperlinks e outras
26:07 coisas, que é o eev.

26:10 A aula 3 eu ainda não preparei o
26:14 material dela direito, e ela é bem mais
26:16 avançada... eu não sei quanta gente
26:18 vai se interessar por ela,
26:21 porque tem bem pouca gente no Brasil que
26:24 se interessa por linguagens funcionais, e
26:27 até onde eu sei a maioria das pessoas
26:28 que se interessam por linguagens funcionais
26:30 está super sem tempo, então eu não sei
26:33 quantas pessoas vão fazer
26:35 esse meu minicurso...

26:38 e na verdade para mim o mínimo é 1 -
26:41 se tiver uma pessoa interessada e for uma
26:42 pessoa animada, que tem coragem de dizer
26:45 "eu não entendi isso aqui" quando eu mostrar
26:47 um determinado exemplo, para mim já tá bom...
26:49 porque eu consigo testar esse material e
26:53 transformar ele num blog post grande, em
26:56 alguma coisa publicável, sei lá...

27:00 então, digamos que a aula 3 interesse
27:02 para bem menos gente, e pode ser que
27:05 algumas pessoas assistam a aula 3 mais por
27:11 curiosidade mas achem tudo muito avançado...

27:14 Basicamente na aula 3 a gente vai ver
27:16 as figuras que me salvaram
27:18 para entender várias coisas do Lean.

27:20 Aqui tem um exemplo dessas figuras...
27:24 ih, não, tou na página errada, deixa eu ir
27:28 pra outra página... tá aqui.

27:32 Por exemplo, isso aqui é um exemplo de
27:36 mônadas sem usar a notação "do", que vou
27:40 supor que vocês já ouviram falar. Então,
27:43 isso aqui é um exemplinho de mônadas com
27:45 a notação "do" traduzida pra uma notação
27:47 mais básica e com as anotações de tipos.

27:50 E pra mim tinha umas coisas que eram
27:52 super misteriosas, que é... por exemplo,
27:54 como é que a gente descobre que uma
27:56 operação dessas, que usa a mônada
27:59 de listas retorna uma lista?

28:03 E aí a gente tem que fazer
28:06 essas type inferences todas pra entender
28:09 como é que esse "bind" vai funcionar,
28:14 porque tem que ser o bind "da mônada
28:16 associada a isso aqui" e aí esse bind
28:19 determina qual vai ser o "pure", e o pure
28:22 vai fazer com que o resultado seja uma
28:24 lista de pares do tipo A×B...

28:26 então eu
28:28 ficava lendo os capítulos sobre
28:32 mônadas dos tutoriais, eles davam um
28:34 montão de exemplos de uso, um montão de
28:36 analogias... e nada fazia muito sentido pra
28:38 mim, e a partir do momento em que eu
28:40 consegui ver todos esses detalhes
28:42 tudo ficou muito mais claro. Então eu vou
28:44 apresentar isso e a gente vai discutir e
28:48 eu vou tentar descobrir se esse tipo de
28:49 coisa ajuda outras pessoas também, ou não...

28:53 Aqui tem um outro exemplo de coisa...
28:56 de figura que me ajudou muito.
28:58 Deixa eu pegar esse pedacinho dela.

29:05 Vamos olhar só pra parte de cima dela.
29:08 Isso aqui é uma função que recebe
29:13 esses argumentos implícitos aqui, então o
29:15 usuário não precisa dar esses argumentos,
29:17 o Lean vai inferir esses argumentos
29:19 a partir do resto...

29:23 Aí tem essa coisa muito misteriosa aqui,
29:25 que eu levei meses para entender, e aí
29:27 tem essa coisa um pouco mais clara aqui...
29:29 aqui a gente tem o produto dos dois
29:31 tipos, que a gente pode considerar que é um
29:32 produto cartesiano de dois conjuntos, e
29:35 um ponto desse produto cartesiano.

29:37 Aqui tem uma coisa invisível...

29:41 e aí essa função que recebe esses
29:44 argumentos vai retornar o resultado
29:45 dessa coisa daqui aqui.

29:47 Tem uma expressão que vai pegar esse ab,
29:48 que é um par, vai separar ele
29:52 em lado esquerdo e lado direito,
29:54 vai colocar o lado esquerdo
29:56 dentro da variável a e vai ignorar o lado
29:58 direito... e aí aqui à direita a gente vai
30:00 retornar o resultado disso.

30:03 E aí como é que a gente faz pra
30:05 entender uma coisa dessas?

30:08 Eu descobri que o melhor modo de entender
30:10 essas coisas é a gente olhar pro parser
30:12 do Lean.

30:15 Então a gente vai dar uma olhada em como
30:20 cada estrutura sintática é definida lá...
30:23 algumas têm comentários bem interessantes,
30:25 outras têm só referências e outras coisas
30:27 [?] que mais ou menos legível

30:29 E aí eu fui
30:30 descobrindo eh que essa coisa aqui era
30:34 uma "typeAscription", essa coisa
30:36 misteriosa daqui era um "instance binder",
30:39 e a partir do nome [?] que eu descobri isso
30:40 eu consegui descobrir quais seções do
30:42 manual explicavam essas coisas... e aí aos
30:46 pouquinhos tudo foi ficando claro.

30:49 Essa figura daqui pode ser dividida
30:51 em figuras que detalham...
30:53 bom, eu não consegui fazer um
30:56 parsing diagram que coubesse numa linha só,
31:01 ficava muito grande, então eu dividi
31:02 isso em vários...

31:02 por exemplo, esse {α β} entre chaves aqui
31:08 ele pode ser transformado
31:12 nessa árvore daqui, bem maior...

31:14 isso aqui é parseado pelo "implicitBinder"...

31:18 essa outra estrutura daqui
31:21 é parseada pelo instBinder...

31:28 e essa última daqui é parseada
31:32 desse jeito daqui...
31:33 e o "let" é parseado por essas duas
31:38 árvores daqui de baixo.

31:40 Tá, então a gente vai entender isso aqui,
31:44 que é um outro tipo de diagrama
31:45 que me salvou...

31:48 E... ai caramba... aqui.
31:58 E basicamente é isso.
32:01 Talvez tenha um outro tipo de
32:04 diagrama, que é pra gente entender o que
32:07 que é um "Pratt parser" e como é que o
32:11 Lean entende precedência, macros e outras
32:13 coisas... mas eu ainda não tenho exemplos
32:15 muito bons dele... então é basicamente isso.

32:21 Tem mais uma seção aqui... peraí.
32:28 Ah, não, era só isso. Eu já expliquei qual
32:30 era minha motivação, meu público alvo, a
32:33 história da didática e tudo mais, e só
32:36 falta falar uma coisa.

32:38 É o seguinte eu já
32:39 disse que eu tou trabalhando num campus
32:40 da UFF que é muito pequeno. Eu já tinha
32:43 uma noção de que esse campus era um lixo,
32:45 até um tempo atrás... mas
32:48 nos últimos do anos eu consegui
32:50 descobrir que ele é um lixo, assim, 10
32:52 vezes maior do que eu pensava...

32:55 não dá para interagir com os meus colegas de lá
32:57 nem mesmo para para discutir os cursos
32:59 que eu tou dando e técnicas de didática...
33:02 e eu oferecia umas oficinas de Software
33:03 Livre pros... basicamente pros alunos,
33:07 e eles não iam nunca, e eu não entendia
33:09 porquê...

33:10 e aí durante a greve eu ofereci
33:12 essas oficinas divulgando elas pro
33:14 pessoal de todos os cursos e eu vi que
33:16 as pessoas de Produção Cultural e
33:18 Psicologia iam nas oficinas, ficavam
33:21 super animadas, faziam milhões
33:22 de perguntas... mas os alunos da
33:25 Computação e da Engenharia - eles não iam
33:27 de jeito nenhum.

33:29 Aí eu fui entendendo aos poucos - até
33:31 porque eu conversei com umas pessoas que
33:33 estudaram em Niterói - que eles têm uma
33:36 mentalidade na qual é inconcebível você
33:39 estudar junto com os colegas, você tirar
33:41 dúvida dos colegas, você ir na oficina
33:43 dos colegas... então eles não tem uma
33:47 mentalidade de "estamos na universidade
33:50 pública, vamos fazer tudo que aparecer,
33:52 vamos aprender tudo que der, e vamos
33:54 compartilhar o conhecimento"...

33:56 É uma coisa muito estranha. Eles
33:58 talvez tenham pego um pouco da mentalidade
34:00 do pessoal da Engenharia de Produção, não
34:03 sei direito... mas de qualquer forma é
34:07 péssimo.

34:08 E aí eu tô querendo dar essa oficina
34:10 pra fazer contato com pessoas
34:12 de outras universidades, descobrir que
34:13 que elas estão fazendo, descobrir como é que
34:15 eu posso participar dos projetos delas,
34:17 grudar nelas de alguma forma fazendo
34:20 coisas interessantes junto com elas online...

34:23 Deixa eu só mostrar uma coisinha que faltou.
34:26 Eu mostrei como é que esses
34:28 links daqui vão para seções dos manuais...
34:31 por exemplo, esse aqui abre
34:35 a versão em HTML do
34:37 "Functional Programing in Lean"...

34:42 e todos esses manuais tem exceto um têm
34:46 fonte um formato super fácil de acessar,
34:52 e a gente consegue extrair os
34:55 bloquinhos de código dessa fonte.

34:58 Então, por exemplo, nesse manual
35:03 daqui, do "Metaprograming", tem uma seção...
35:06 repara que esse link daqui veio pra uma subseção
35:11 dessa página, a subseção se chama "Building
35:13 a DSL and a syntax for it"...

35:15 é um exemplo mais ou menos básico
35:16 de como criar uma linguagenzinha nova...

35:21 e eu também posso ir pro código fonte
35:24 disso aqui, que gerou esse HTML...

35:28 Então, se eu rodo esse hiperlink daqui
35:33 ele abre o código fonte disso...
35:35 repara, esse título aparece
35:38 desse jeito aqui, e esse bloquinho de
35:40 código aparece desse jeito... isso aqui é
35:43 um arquivo em Lean, o arquivo parseou
35:46 essas coisas daqui
35:48 interpretou esse bloquinho daqui como
35:52 Lean, coloriu tudo do jeito certo, e,
35:59 por exemplo... talvez se eu usar a tecla
36:01 de "go to" aqui talvez ele vá
36:03 pra definição do "inductive"... bom,
36:07 talvez, mas eu não tenho certeza...

36:11 Tudo funciona exatamente como
36:14 naquele outro demo que eu mostrei - cada
36:15 "#check" desses mostra um output aqui
36:19 embaixo, e se eu bater f10 l l...

36:24 opa, não, seu eu bater essa
36:26 sequência misteriosa de teclas daqui
36:29 ele mostra todas as mensagens de uma vez.

36:32 Então: a gente vai ver como acessar esse...
36:36 o código fonte, e extrair o código fonte
36:40 e criar arquivos menores com isso, em que
36:42 a gente possa fazer nossos experimentos...
36:45 modificar coisas, simplificar coisas
36:47 acrescentar coisas, etc...

36:49 Então isso é uma coisa que a gente
36:51 vai ver superficialmente na primeira
36:53 aula e depois a gente vai usar
36:55 bastante.

36:57 E... é isso. O vídeo era isso aí.
37:01 Qualquer coisa acessem essas
37:04 páginas pra mais informações e entrem
37:07 em contato comigo... e se vocês tiverem
37:09 algum interesse no curso por
37:11 favor peguem os meus contatos e mandem
37:13 ou e-mail ou mensagem por WhatsApp ou
37:16 por Telegram. É isso por enquanto!

37:20