1.8. Provando com Táticas
Escrever termos de prova à mão torna-se impraticável à medida que as provas crescem. Uma tática é um comando que transforma o estado de prova, o objetivo junto com as hipóteses em escopo, um passo por vez. A palavra-chave by entra no modo de táticas, e Lean elabora a sequência de táticas em um termo de prova, então uma prova por táticas e uma prova por termos produzem o mesmo objeto subjacente.
A tática exact fecha um objetivo com um termo que o prova, o que recupera a prova em modo de termo acima.
example (P : Prop) (h : P) : P := P:Proph:P⊢ P
All goals completed! 🐙
As táticas raciocinam em duas direções. Um passo regressivo reduz o objetivo a subobjetivos mais simples, e um passo progressivo deriva novas hipóteses a partir das que estão em escopo. Cada conectivo vem com táticas que o introduzem, provando um objetivo daquela forma, e táticas que o eliminam, usando uma hipótese daquela forma. Tomamos os conectivos um a um.
1.8.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.8.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.8.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.8.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.8.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! 🐙
1.8.6. Exemplos
As provas abaixo demonstram novamente esses dez teoremas, agora com táticas. Cada uma pode ser lida ao lado do termo de prova da seção anterior.
Exemplo 1. A implicação é reflexiva.
example (P : Prop) : P → P := P:Prop⊢ P → P
P:Proph:P⊢ P
All goals completed! 🐙
Exemplo 2. Uma conjunção implica cada uma das suas partes.
example (P Q : Prop) : P ∧ Q → P := P:PropQ:Prop⊢ P ∧ Q → P
P:PropQ:Proph:P ∧ Q⊢ P
All goals completed! 🐙
Exemplo 3. Um disjunto implica a disjunção.
example (P Q : Prop) : P → P ∨ Q := P:PropQ:Prop⊢ P → P ∨ Q
P:PropQ:Proph:P⊢ P ∨ Q
All goals completed! 🐙
Exemplo 4. Qualquer coisa decorre do absurdo.
example (P : Prop) : False → P := P:Prop⊢ False → P
P:Proph:False⊢ P
All goals completed! 🐙
Exemplo 5. Modus ponens, empacotado como uma única implicação.
example (P Q : Prop) : (P → Q) ∧ P → Q := P:PropQ:Prop⊢ (P → Q) ∧ P → Q
P:PropQ:Proph:(P → Q) ∧ P⊢ Q
P:PropQ:Proph:(P → Q) ∧ P⊢ P
All goals completed! 🐙
Exemplo 6. A disjunção comuta.
example (P Q : Prop) : P ∨ Q → Q ∨ P := P:PropQ:Prop⊢ 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! 🐙
Exemplo 7. Introdução da dupla negação.
example (P : Prop) : P → ¬¬P := P:Prop⊢ P → ¬¬P
P:ProphP:PhnP:¬P⊢ False
All goals completed! 🐙
Exemplo 8. Contraposição.
example (P Q : Prop) : (P → Q) → (¬Q → ¬P) := P:PropQ:Prop⊢ (P → Q) → ¬Q → ¬P
P:PropQ:ProphPQ:P → QhnQ:¬QhP:P⊢ False
All goals completed! 🐙
Exemplo 9. Eliminação da dupla negação, que requer raciocínio clássico.
example (P : Prop) : ¬¬P → P := P:Prop⊢ ¬¬P → P
P:Proph:¬¬P⊢ P
P:Proph:¬¬P⊢ ¬P → False
P:Proph:¬¬PhnP:¬P⊢ False
All goals completed! 🐙
Exemplo 10. O currying transforma uma hipótese conjuntiva em implicações aninhadas.
example (P Q R : Prop) : (P ∧ Q → R) → (P → (Q → R)) := P:PropQ:PropR:Prop⊢ (P ∧ Q → R) → P → Q → R
P:PropQ:PropR:Proph:P ∧ Q → RhP:PhQ:Q⊢ R
All goals completed! 🐙