1.7. Dedução Natural em Lean
Em Lean, enunciamos uma proposição e a provamos em uma única declaração. A palavra-chave example introduz um enunciado anônimo, e theorem introduz um enunciado com nome. As hipóteses aparecem antes dos dois-pontos como suposições nomeadas, e a proposição a provar, o objetivo, aparece depois.
Lean codifica a dedução natural diretamente. Uma prova de uma proposição é um termo cujo tipo é aquela proposição, uma suposição aberta é uma variável daquele tipo, e cada regra de dedução torna-se um modo de construir ou desmontar termos. A prova mais simples usa uma suposição diretamente, a regra de suposição da dedução natural.
example (P : Prop) (h : P) : P := h
Aqui h nomeia a suposição de que P vale, e a prova é o próprio h. A Aula 3 desenvolve essa correspondência entre proposições e tipos.W. A. Howard, The Formulae-as-Types Notion of Construction, em To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, Academic Press, 1980.
A Tabela 1.7.1 mapeia cada regra da seção de dedução natural ao termo de Lean que a realiza. Uma regra de introdução constrói um termo, e uma regra de eliminação o desmonta.
Regra | Termo em Lean | Exemplo |
|---|---|---|
suposição | um nome de hipótese |
|
→I |
|
|
→E | aplicação |
|
∧I |
|
|
∧E₁, ∧E₂ |
|
|
∨I₁, ∨I₂ |
|
|
∨E |
|
|
¬I |
|
|
¬E |
aplicação em |
|
⊥E |
|
|
Tabela 1.7.1. As regras de dedução natural e os termos de Lean que as realizam.
Como ¬P abrevia P → False, as regras da negação reutilizam os termos da implicação. Para ver a correspondência em uma derivação completa, tome P ∧ Q → Q ∧ P. Ela descarta a suposição P ∧ Q, projeta cada uma das partes e as remonta na ordem oposta.
[P ∧ Q] [P ∧ Q]
───────── ∧E₂ ───────── ∧E₁
Q P
─────────────────────────── ∧I
Q ∧ P
───────────────────────────── →I
P ∧ Q → Q ∧ P
O termo em Lean segue a derivação passo a passo. A abstração fun h => … é o →I que descarta P ∧ Q, as projeções h.right e h.left são os dois passos ∧E, e o par ⟨_, _⟩ é o ∧I.
example (P Q : Prop) : P ∧ Q → Q ∧ P :=
fun h => ⟨h.right, h.left⟩
1.7.1. Exemplos
As provas abaixo codificam as dez derivações da seção anterior como termos de prova. Cada termo espelha a sua derivação, com uma regra de introdução construindo um termo e uma regra de eliminação o desmontando.
Exemplo 1. A implicação é reflexiva.
example (P : Prop) : P → P :=
fun h => h
Exemplo 2. Uma conjunção implica cada uma das suas partes.
example (P Q : Prop) : P ∧ Q → P :=
fun h => h.left
Exemplo 3. Um disjunto implica a disjunção.
example (P Q : Prop) : P → P ∨ Q :=
fun h => Or.inl h
Exemplo 4. Qualquer coisa decorre do absurdo.
example (P : Prop) : False → P :=
fun h => False.elim h
Exemplo 5. Modus ponens, empacotado como uma única implicação.
example (P Q : Prop) : (P → Q) ∧ P → Q :=
fun h => h.left h.right
Exemplo 6. A disjunção comuta.
example (P Q : Prop) : P ∨ Q → Q ∨ P :=
fun h => h.elim
(fun hP => Or.inr hP)
(fun hQ => Or.inl hQ)
Exemplo 7. Introdução da dupla negação.
example (P : Prop) : P → ¬¬P :=
fun hP hnP => hnP hP
Este exemplo merece o desdobramento completo, porque a sua prova tem duas funções onde o enunciado parece ter uma implicação só. Como ¬A é A → False, a dupla negação desdobra-se duas vezes, de fora para dentro. Primeiro ¬¬P é ¬P → False, depois é (P → False) → False, e o enunciado inteiro é P → ((P → False) → False). Os parênteses da negação interna são obrigatórios. A seta associa à direita, então P → P → P → False é a proposição P → (P → (P → False)), que é outra e é falsa.
O termo tem então uma função por seta, e fun hP hnP => hnP hP abrevia fun hP => fun hnP => hnP hP. A primeira função é o →I que descarta P e devolve uma prova de ¬¬P. Essa prova é ela mesma uma função, e a segunda função é o ¬I que descarta ¬P. O parâmetro dela tem tipo ¬P, e não P, ponto em que é fácil se enganar. Restam no contexto hP de tipo P e hnP de tipo P → False, e sobra provar False. Uma hipótese negativa é uma função em False, então aplicá-la ao que ela nega é o ¬E, e hnP hP fecha a prova. A ordem inversa não tipa, porque hP não é função.
example (P : Prop) : P → ¬¬P :=
fun (hP : P) =>
fun (hnP : ¬P) => hnP hP
Exemplo 8. Contraposição.
example (P Q : Prop) : (P → Q) → (¬Q → ¬P) :=
fun hPQ hnQ hP => hnQ (hPQ hP)
Exemplo 9. Eliminação da dupla negação, que requer raciocínio clássico.
example (P : Prop) : ¬¬P → P :=
fun h => Classical.byContradiction (fun hnP => h hnP)
Exemplo 10. O currying transforma uma hipótese conjuntiva em implicações aninhadas.
example (P Q R : Prop) : (P ∧ Q → R) → (P → (Q → R)) :=
fun h hP hQ => h ⟨hP, hQ⟩