1.5. Primeiras Provas 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.
A prova mais simples usa uma hipótese diretamente.
example (P : Prop) (h : P) : P := h
Aqui h nomeia a suposição de que P vale, e a prova é o próprio h. Uma prova de uma proposição é um termo cujo tipo é aquela proposição. 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 maioria das provas usa táticas, comandos que transformam o objetivo passo a passo. A palavra-chave by entra no modo de táticas. Cada conectivo vem com regras para introduzi-lo, provando um objetivo daquela forma, e regras para eliminá-lo, usando uma hipótese daquela forma.
1.5.1. Implicação
A tática intro introduz uma implicação. Para provar P → Q, suponha P sob um nome escolhido e prove Q.
example (P Q : Prop) (hQ : Q) : P → Q := P:PropQ:ProphQ:Q⊢ P → Q
P:PropQ:ProphQ:Q_hP:P⊢ Q
All goals completed! 🐙
A tática exact fecha o objetivo com um termo que o prova. Para usar uma implicação, aplique-a a uma prova do seu antecedente. Uma hipótese hPQ de tipo P → Q é uma função de provas de P em provas de Q, então hPQ hP prova Q. Esta é a regra de modus ponens.
example (P Q : Prop) (hPQ : P → Q) (hP : P) : Q := hPQ hP
A tática apply usa a mesma regra na direção regressiva. Aplicar hPQ ao objetivo Q deixa P como novo objetivo.
example (P Q : Prop) (hPQ : P → Q) (hP : P) : Q := P:PropQ:ProphPQ:P → QhP:P⊢ Q
P:PropQ:ProphPQ:P → QhP:P⊢ P
All goals completed! 🐙
A tática have raciocina progressivamente, adicionando uma nova hipótese derivada das atuais, e show enuncia o objetivo corrente explicitamente. As duas fazem as provas se lerem como argumentos matemáticos estruturados.
example (P Q R : Prop) (hPQ : P → Q) (hQR : Q → R)
(hP : P) : R := P:PropQ:PropR:ProphPQ:P → QhQR:Q → RhP:P⊢ R
P:PropQ:PropR:ProphPQ:P → QhQR:Q → RhP:PhQ:Q⊢ R
P:PropQ:PropR:ProphPQ:P → QhQR:Q → RhP:PhQ:Q⊢ R
All goals completed! 🐙
1.5.2. Conjunção
Para provar P ∧ Q, prove as duas partes. A tática constructor divide o objetivo em dois, e o marcador · delimita a prova de cada um.
example (P Q : Prop) (h : P ∧ Q) : Q ∧ P := P:PropQ:Proph:P ∧ Q⊢ Q ∧ P
P:PropQ:Proph:P ∧ Q⊢ QP:PropQ:Proph:P ∧ Q⊢ P
P:PropQ:Proph:P ∧ Q⊢ Q All goals completed! 🐙
P:PropQ:Proph:P ∧ Q⊢ P All goals completed! 🐙
Para usar uma conjunção, projete as suas partes com .left e .right. O construtor anônimo ⟨_, _⟩ constrói o par diretamente, dando uma prova em estilo de termo.
example (P Q : Prop) (h : P ∧ Q) : Q ∧ P :=
⟨h.right, h.left⟩
1.5.3. Disjunção
Para provar P ∨ Q, escolha um lado. Or.inl a prova a partir de P, e Or.inr a prova a partir de Q. Para usar uma disjunção, raciocine por casos. A tática cases produz um objetivo por disjunto.
example (P Q : Prop) (h : P ∨ Q) : Q ∨ P := P:PropQ:Proph:P ∨ Q⊢ Q ∨ P
cases h with
P:PropQ:ProphP:P⊢ Q ∨ P All goals completed! 🐙
P:PropQ:ProphQ:Q⊢ Q ∨ P All goals completed! 🐙
1.5.4. Negação
Em Lean, ¬P é definida como P → False, onde False é a proposição sem prova. Uma prova de ¬P é uma função que transforma qualquer prova de P em uma prova de False.
example (P : Prop) (hP : P) (hnP : ¬P) : False := hnP hP
Toda tática para implicação, portanto, funciona para negação. A direção contrapositiva abaixo precisa apenas de intro e de aplicação.
theorem contrapositive (P Q : Prop) (hPQ : P → Q) :
¬Q → ¬P := P:PropQ:ProphPQ:P → Q⊢ ¬Q → ¬P
P:PropQ:ProphPQ:P → QhnQ:¬QhP:P⊢ False
All goals completed! 🐙
Introduzir a dupla negação é igualmente direto.
example (P : Prop) (hP : P) : ¬¬P := fun hnP => hnP hP
A segunda lei de De Morgan combina as regras vistas até aqui. A tática constructor também introduz um bicondicional, dividindo-o nas duas implicações.
theorem deMorgan_or (P Q : Prop) : ¬(P ∨ Q) ↔ ¬P ∧ ¬Q := P:PropQ:Prop⊢ ¬(P ∨ Q) ↔ ¬P ∧ ¬Q
P:PropQ:Prop⊢ ¬(P ∨ Q) → ¬P ∧ ¬QP:PropQ:Prop⊢ ¬P ∧ ¬Q → ¬(P ∨ Q)
P:PropQ:Prop⊢ ¬(P ∨ Q) → ¬P ∧ ¬Q P:PropQ:Proph:¬(P ∨ Q)⊢ ¬P ∧ ¬Q
P:PropQ:Proph:¬(P ∨ Q)⊢ ¬PP:PropQ:Proph:¬(P ∨ Q)⊢ ¬Q
P:PropQ:Proph:¬(P ∨ Q)⊢ ¬P P:PropQ:Proph:¬(P ∨ Q)hP:P⊢ False
All goals completed! 🐙
P:PropQ:Proph:¬(P ∨ Q)⊢ ¬Q P:PropQ:Proph:¬(P ∨ Q)hQ:Q⊢ False
All goals completed! 🐙
P:PropQ:Prop⊢ ¬P ∧ ¬Q → ¬(P ∨ Q) P:PropQ:Proph:¬P ∧ ¬QhPQ:P ∨ Q⊢ False
cases hPQ with
P:PropQ:Proph:¬P ∧ ¬QhP:P⊢ False All goals completed! 🐙
P:PropQ:Proph:¬P ∧ ¬QhQ:Q⊢ False All goals completed! 🐙
1.5.5. Raciocínio Clássico
As regras usadas até aqui são construtivas. Dois princípios da lógica clássica não decorrem delas, a lei do terceiro excluído e a eliminação da dupla negação. Lean fornece os dois no namespace Classical.
#check Classical.em
Classical.byContradiction prova P a partir de uma prova de que ¬P é impossível. Com ela, a eliminação da dupla negação está a uma aplicação de distância.
theorem not_not_elim (P : Prop) (h : ¬¬P) : P := P:Proph:¬¬P⊢ P
P:Proph:¬¬P⊢ ¬P → False
P:Proph:¬¬PhnP:¬P⊢ False
All goals completed! 🐙
A primeira lei de De Morgan requer raciocínio clássico. Uma análise de casos sobre Classical.em P decide qual disjunto provar.
theorem deMorgan_and (P Q : Prop) : ¬(P ∧ Q) → ¬P ∨ ¬Q := P:PropQ:Prop⊢ ¬(P ∧ Q) → ¬P ∨ ¬Q
P:PropQ:Proph:¬(P ∧ Q)⊢ ¬P ∨ ¬Q
cases Classical.em P with
P:PropQ:Proph:¬(P ∧ Q)hP:P⊢ ¬P ∨ ¬Q All goals completed! 🐙
P:PropQ:Proph:¬(P ∧ Q)hnP:¬P⊢ ¬P ∨ ¬Q All goals completed! 🐙