Lean

Usamos o proof assistant Lean para algumas atividades obrigatórias.

1. Instale o Lean 4 no teu computador para usar com o VS Code.
2. Numa pasta no teu computador use o comando lake new myfmclearn. (Isso vai criar uma nova pasta chamada myfmclearn e iniciar um repositório git nela.) Se preferir, pode fazer isso dentro do VS Code, pelo caminho seguinte: ∀ › New Project… › Create Standalone Project… e escolher o nome myfmclearn.
3. Cria dentro do teu projeto uma pasta chamadada Solutions.
4. Cada vez que você trabalha em qualquer arquivo dentro do teu repositório git, não esqueça de commit’ar teu trabalho imediatamente, mesmo sendo um progresso pequeno; e faça push imediatamente: é teu “comprovante” que tal dia tu fez tal trabalho!

Quando eu escrevi esse FAQ estava referindo à versão anterior do Lean (Lean 3). Se achar alguma dica/comando que não funciona, pode ser que não atualizei/corrigi ainda.

Como sempre: procure ajuda no Zulip, no canal #proofassistants.

Como posso compartilhar meu código para receber feedback ou tirar uma dúvida?

• Se teu código é «stand-alone», usando ```lean para iniciar o bloco de código no Zulip, já ativa o link para o Lean playground.
• Alternativamente podes compartilhar teu repo no github (que já deve ser visível no teu profile no Zulip!)

Ataques (do alvo)

Se meu alvo já está nos meus dados

Lean: exact d onde d é o rótulo do dado, ou apenas assumption e Lean vai tentar achar teu alvo nos seus dados.

⇒: Se meu alvo é uma implicação P ⇒ Q

Texto: «Suponha P.»

Lean: intro hp onde hp é o nome que escolhemos para rotular esse dado.

Efeitos:

• ganhamos o P nos dados
• o alvo vira Q

∧: Se meu alvo é uma conjunção P ∧ Q

Texto: «Parte L: [demonstro P aqui]. Parte R: [demonstro Q aqui].»

Lean: split

Efeitos: nossa demonstração separa em duas partes, copiando/colando os dados atuais e: a primeira parte tem como alvo P, a segunda parte tem com alvo Q. Precisamos demonstrar ambas as partes.

∨: Se meu alvo é uma disjunção P ∨ Q

Tenho o direito de escolher a parte esquerda (P) ou a parde direita (Q). Tenho então de escolher uma das duas alternativas:

• Texto: «Escolho a esquerda para demonstrar.» Lean: left
  Efeito: O alvo vira P.

• Texto: «Escolho a direita para demonstrar.» Lean: right
  Efeito: O alvo vira Q.

∀: Se meu alvo é uma proposição universal (∀x:A)[ φ(x) ]

Basta solicitar um arbitrio objeto a do tipo A e demonstrar que φ(a).

Texto: «Seja a : A.» Efeito: O alvo vira φ(a).

Lean: intro a

∃: Se meu alvo é uma proposição existencial (∃x:A)[ φ(x) ]

Preciso achar um objeto do tipo A e demonstrar que meu objeto tem a propriedade φ. Supondo que queremos afirmar que um certo objeto a : A é o objeto que procuramos:

Texto: «Vou demonstrar que φ(a).» Efeito: O alvo vira φ(a).

Lean: existsi a

=: Se meu alvo é uma equação da forma t = t.

Texto: «Imediato (pela reflexividade da =).»

Lean: refl

=: Se meu alvo é uma equação da forma s = t.

Precisamos calcular usando substituições no s até chegar no t ou vice versa. Alternativamente podemos calcular começando no s para chegar até um objeto w, parar lá, pegar o t e calcular até chegar no mesmo objeto w.

Texto: «Calculamos: […cálculo aqui…]»

Lean: veja embaixo o como usar igualdades (para aplicá-las no alvo). Depois, veja como usar o calc que fica muito mais próximo no humano «Calculamos: […]»

¬: Se meu alvo é uma negação ¬P

Então na verdade é uma implicação: P ⇒ ⊥; e logo já sabes o que fazer.

⇔: Se meu alvo é uma equivalência P ⇔ Q

Então na verdade é uma conjunção: (P ⇒ Q) ∧ (Q ⇒ P) e logo já sabes o que fazer.

Como usar meus dados

∨: Para usar uma disjunção P ∨ Q

Texto: «Separamos em casos. Caso L: […]. Caso R: […].»

Efeito: Dois novos “jogos” são criados onde todos os dados/alvos atuais são copiados e colados em cada um, só que no primeiro temos o P como dado extra, e no segundo temos o Q. Precisamos «fechar» ambos! Cuidado: cada joguinho tem seu próprio escopo, então mudanças/efeitos que linhas de demonstração têm nos dados/alvos executados no primeiro caso, não vão afetar o segundo.

Lean: rcases hor onde hor é o rotulo da disjunção que queremos usar. Para dar rótulos às hipoteses de cada caso (por exemplo hp para o P e hq para o Q) usamos rcases hor with (hp | hq)

∧: Para usar uma conjunçào P ∧ Q

Text: Escrevendo «Obtenha o lado esqeurdo da P∧Q.» ganhamos o P nos nossos dados. Similarmente «Obtenha o lado direito da P∧Q.» nos dá o Q. Só que: ninguém merece escrever isso, então como humanos, tendo P∧Q nos nossos dados consideramos que já temos feito ámbas essas linhas acima e já temos ámbos os dados P e Q nos nossos dados!

Lean: rcases h onde h é o rótulo do P∧Q nos nossos dados.
Melhor dar nossos próprios nomes às duas partes da conjunção que vamos ganhar como dados, e fazemos isso com: rcases h with ⟨hp , hq⟩ assim teremos nos dados hp : P e hq : Q.

Cuidado: a palavra usada no Lean é confusa, pois não corresponde à palavra «casos» na lingua humana!

⇒: Para usar uma implicação P ⇒ Q

Podemos aplicá-la no P mas para fazer isso precisamos também ter P nos nossos dados.

Texto: «Como P⇒Q e P, logo Q.» ou «Aplique P⇒Q em P para obter Q.» Efeito: ganhamos o Q nos dados.

Lean: have hq : Q := hpq hp onde hq é o rótulo que eu escolhi para o dado que vou ganhar, e hpq é o rótulo do meu dado P→Q e hp o rótulo do meu P.

Text: Quando nosso alvo é Q e já temos P⇒Q nos nossos dados (mas ainda não o P para usá-lo e terminar), podemos dizer «Basta demonstrar o P (pois P⇒Q).» Efeito: o alvo muda de Q para P.

Lean: apply hpq onde novamente hpq é o rótulo da implicação P→Q que temos nos dados.

¬: Para usar uma negação ¬P

Novamente: a negação ¬P é a implicação P⇒⊥. Então sabes como usar.

∀: Para usar uma proposição universal (∀x:A)[ φ(x) ]

Basta aplicá-la em qualquer objeto a do tipo A e ela fornece o novo dado φ(a).

Texto: «Como a é um A, pela (fulana) temos φ(a).»

Lean: Tratamos uma proposição universal como se fosse uma função. Tendo a : A e h : (∀x : A, P x) a aplicação do h no a (que denotamos por h a) é uma demonstração de P a, ou seja, da afirmação que o a tem a propriedade P.

∃: Para usar uma proposição existencial (∃x:A)[ φ(x) ]

Podemos solicitar um a do tipo A que tem a propriedade φ:

Texto: «Seja a um A tal que φ(a).»

Lean: cases h with a ha onde h é o rótulo do existencial, a o nome para o objeto que solicitamos e ha o rótulo do fato que nosso objeto a tem tal propriedade.

Cuidado: a palavra usada no Lean é confusa, pois não corresponde à palavra «casos» na lingua humana!

=, ⇔: Para usar uma equação s = t ou uma equivalência P⇔Q

Texto: Substituimos objetos iguais por iguais citando a igualdade, e proposições equivalentes por equivalentes citando a equivalência.

Lean: usamos o rw heq onde heq é o nome da igualdade que queremos usar.

Obs: o Lean substitua de esquerda para a direita; para substituir na direção oposta use rw ← em vez de rw.

Obs: o Lean tenta usar a igualdade para substituir algo no alvo. Se quiser aplicar tal substituição em algum dado rótulado por h, especifique adicionando um at h, assim: rw heq at h onde novamente heq é o rótulo da igualdade que queremos usar e h é o rótulo da hipótese que queremos efetuar tal substituição.

Lean: usamos o rw para equivalências na mesma maneira. Além disso, lembre-se que uma equivalência é apenas uma conjunção, então podemos usá-la nessa forma também.

Podemos juntar varios rw h₁, rw ←h₂, …, rw hₙ consecutivos por rw [h₁, ←h₂, …, hₙ]

Usando dados on the fly

Observe que podemos usar dados para compor novos dados «on the fly»: tendo f : A → B e a : A o f a denota a aplicação da implição f no dado a e logo é (demonstração de) B. Assim, se nosso alvo no momento era B podemos escrever exact f a para fechar. A mesma coisa aplica para o resto dos conectivos, por exemplo se h : P∧Q entaõ h.left : P e h.right : Q.

Conversion mode

Se sentir vontade de caminhar nos teus dados e alvos e reescrever ou simplificar umas (sub)partes deles, veja o como usar o conv. Não é necessário mas tem gente que não sobrevive sem conv.

Ex Falso Quodlibet

Também conhecido como: «explodi o mundo e logo meu alvo também morreu.»

Texto: «Eu vou achar uma contradição.»

Lean: exfalso

Efeito: O alvo vira ⊥.

Talvéz já temos uma contradição óbvia dentro dos nossos dados. Para dizer isso pra o Lean e fechar a demonstração:

Lean: contradiction

Indução

Texto: «Por indução no n.»

Lean: induction n with w hw onde w é o nome do arbitrário natural da H.I. e hw o rótulo da H.I. mesmo.

Obs: se conseguir demonstrar sem usar a hipótese indutiva, significa que não era necessário usar indução. Talvez sequer precisou tratar a base e a demonstração final do passo indutivo em formas diferentes! Ou seja, atacando diretamente o ∀ teria dado certo. Mas pode ser que precisou realmente tratar diferente o caso zero e o caso sucessor de alglém. Isso fazemos com o cases n onde n é o natural que queremos deparar nos casos n = O e n = Sn’ para algum natural n’. Para escolher o nome usamos: cases n with n'.

Tips

1. Em vez de usar intro h, intro h', intro h'' etc., use intro h h' h''.
2. Aproveite padrões aninhados para efetuar intros e extrações. Por exemplo, se teu alvo é P ∧ Q → R → S ∧ T → G dá para introduzir tudo e já “desembalar” as conjunções assim:
   intro ⟨hp, hq⟩ hr ⟨hs, ht⟩.
3. O rcases que executamos para usar conjunções e disjunções permite casamento arbitrariamente profundo (aninhado): querendo usar um dado como o P ∨ (Q ∧ (R ∨ S)) podemos usar o seguinte with: rcases h with (hp | ⟨hq , (hr | hs)⟩).
4. Para repetir um tactic até não puder mais aplicá-lo use repeat { tactic }.
5. O processo inverso de intro é o revert: use revert h₁ … hₙ para tirar essas hipoteses dos dados e «devolvê-las» para a parte dos alvos. Isso é bastante útil quando quisermos «fazer indução cedo, antes de “sejar” umas variáveis para carregar os ∀’s na nossa HI, a fortalecendo nesse jeito». Mas para isso temos também o «especializado» induction n generalizing z₁ … zₙ onde z₁,…zₙ são variáveis nos dados que queremos ganhá-las “com ∀” nas hipotéses indutivas.
6. Use injection quando quer «apagar os construtores numa igualdade no alvo, por exemplo um alvo Sn=Sm viraria n=m. Tendo uma tal igualdade nos dados rotulada por h use injection h with h₁ … hₙ para ganhar como novo dado as igualdades inferidas. Neste exemplo, tendo o dado h : succ n = succ m, usando injection h with h' ganhamos o novo dado h' : n = m.
7. Se precisar dum dado P que não tens, mas tu consegue demonstrá-lo, use o have h : P onde h o rótulo que tu quer escolher para dar esse dado. Lean vai criar um novo joguinho com este alvo e, se conseguir demonstrá-lo, vai adicionar o h : P nos dados do joguinho original. Ou seja: «aceito te dar o dado que tu queres ter, basta só demonstrá-lo.»
8. Lean perdoa demais: aparecendo uma nova variável livre num enunciado, vai acabar a declarando implicitamente. Pode ser conveniente mas na verdade acaba sendo um tiro no pé mais vezes: considere o que acontece se tu quer referir àlgo já definido chamado jadecla e em vez de escrever jadecla mesmo para referir a ele acabou escrevendo jadecia, por engano. O desejado seria receber um Name Error aqui, mas em vez disso Lean vai considerar que é um nome novo e portnato considerar que tu tá querendo uma declaração implícita dessa nova variável para ser usada. Para desativar isso (recomendo muito), use:
   set_option autoImplicit false

Feitiços não-construtivos

Primeiramente tente demonstrar os teoremas sem usar os seguintes “feitiços” não-construtivos. Considere que uma demonstração que precisou pelo menos um deles, pelo menos uma vez, é “manchada” com a mancha incomputacional de «não-construtiva». Qualquer demonstração de outro teorema que vai acabar usando esta, será considerada manchada também. Obs: continuaria uma demonstração correta.

⛤ LEM (Law of Excluded Middle)

Para qualquer proposição P que podemos imaginar, o LEM nos dá de presente o P∨¬P, que usamos (como disjunção) para separar nos casos P e ¬P.

Texto: «Separo em casos. Caso P: […]. Caso ¬P: […].»

Lean: by_cases h : P onde P é a proposição que escolhemos e h o rótulo da hipótese correspondente para cada caso (P e ¬P aqui).

⛤ RAA (Reductio Ad Absurdum)

Tendo como alvo qualquer proposição P, supomos sua negação ¬P e tentamos achar uma contradição (⊥).

Texto: «Vamos supor que não P, e chegar num absurdo.»

Efeito: Ganhamos o ¬P nos dados; o alvo vira ⊥.

Lean: by_contradiction hboom onde hboom é o rótulo que escolhemos para chamar o dado. O Lean entende a abreviação by_contra para este tactic.

Dá para ver as parenteses implícitas?

Dá sim. Use a linha seguinte no teu código:

set_option pp.parens true

para ver as parenteses implícitas a partir desta linha, e troque o true para false para deixá-las implícitas a partir de tal linha.

Gostei desse option, o que mais tem?

Para ver e buscar nos options, use #help option

E depois?

Dominou tudo isto? Veja o Theorem Proving in Lean e o Mathematics in Lean.