Lean
Usamos o proof assistant Lean para algumas atividades obrigatórias.
- Instale o Lean no teu computador
- configure teu editor para ativar o modo Lean
- Numa pasta no teu computador use o comando
leanpkg new fmclean
(Isso vai criar uma nova pasta chamadafmclean
e iniciar um repositório git nela.) - 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
é a h a : P a
, ou seja, um dado que a
tem a propriedade P.
Para usar uma proposição universal (∃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.