Lean

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

1. Instale o Lean no teu computador Seguindo os links lá, se tu usa Windows, dê uma olhada no vídeo Installing the Lean theorem prover (windows) no YouTube.
2. Configure teu editor para ativar o modo Lean
3. Numa pasta no teu computador use o comando leanpkg new fmclean (Isso vai criar uma nova pasta chamada fmclean e iniciar um repositório git nela.)
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 fez tal trabalho!

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!)

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 P: [demonstro P aqui]. Parte Q: [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 1: «Escolho a esquerda para demonstrar.» Mais humano: «Vou demonstrar P.»
  Lean 1: left,
  Efeito 1: O alvo vira P.

• Texto 2: «Escolho a direita para demonstrar.» Mais humano: «Vou demonstrar Q.»
  Lean 2: right,
  Efeito 2: 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 igualdade t = t.

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

Lean: refl,

Se meu alvo é uma igualdade 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.

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.

Para usar uma disjunção P ∨ Q

Texto: «Separamos em casos. Caso P: […]. Caso Q: […].»

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: cases 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) use: cases 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: cases h, onde h é o rótulo do P∧Q nos nossos dados.
Nesse exemplo o Lean vai nomear os dois novos dados (P e Q) por h_left : P e h_right : Q respectivamente. Melhor dar seus próprios nomes, e fazemos isso com cases 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 ter P nos nossos dados.

Texto: «Como P⇒Q e P, logo 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 implicacã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 igualdade 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

Não esqueça terminar os tactics com ,.

Em vez de usar intro h, intro h', intro h'', etc., use intros h h' h'',.

Para repetir um tactic até não puder mais aplicá-lo use repeat { tactic }.

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.

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.

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 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.»

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.

E depois?

Dominou tudo isto? Veja o [lean-theoremproving][Theorem Proving in Lean].