1.9. Exemplos Resolvidos
Cada exemplo abaixo aparece de três formas, como uma derivação em dedução natural, como um termo de prova e como uma prova por táticas. As três apresentam a mesma prova, e Lean verifica os dois scripts de prova na construção das notas. Estas proposições são disjuntas dos exemplos das seções anteriores e dos exercícios.
1.9.1. Uma Conjunção Implica uma das suas Partes
A eliminação projeta a parte esquerda, e a implicação descarta a suposição P ∧ Q.
[P ∧ Q]
────────── ∧E₁
P
──────────── →I
P ∧ Q → P
example (P Q : Prop) : P ∧ Q → P :=
fun h => h.left
example (P Q : Prop) : P ∧ Q → P := P:PropQ:Prop⊢ P ∧ Q → P
P:PropQ:Proph:P ∧ Q⊢ P
All goals completed! 🐙
1.9.2. Ex Falso Quodlibet
A partir de uma prova do absurdo, a eliminação de ⊥ prova qualquer proposição.3
[⊥]
────── ⊥E
P
──────── →I
⊥ → P
example (P : Prop) : False → P :=
fun h => False.elim h
example (P : Prop) : False → P := P:Prop⊢ False → P
P:Proph:False⊢ P
All goals completed! 🐙
1.9.3. Modus Ponens
Uma implicação e o seu antecedente, ambos projetados da conjunção, combinam-se por →E para dar o consequente.4
[(P→Q)∧P] [(P→Q)∧P]
───────────── ∧E₁ ───────────── ∧E₂
P → Q P
────────────────────────────── →E
Q
──────────────────────────────── →I
(P → Q) ∧ P → Q
example (P Q : Prop) : (P → Q) ∧ P → Q :=
fun h => h.left h.right
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! 🐙
1.9.4. A Disjunção Comuta
A análise de casos sobre a disjunção a remonta com os disjuntos trocados.
[P] [Q]
[P ∨ Q] ─────── ∨I₂ ─────── ∨I₁
Q ∨ P Q ∨ P
───────────────────────────────────── ∨E
Q ∨ P
────────────────────── →I
P ∨ Q → Q ∨ P
example (P Q : Prop) : P ∨ Q → Q ∨ P :=
fun h => h.elim
(fun hP => Or.inr hP)
(fun hQ => Or.inl hQ)
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! 🐙
1.9.5. Eliminação da Dupla Negação
Esta direção requer raciocínio clássico. Classical.byContradiction descarta a suposição ¬P após derivar ⊥ dela junto com ¬¬P.5
[¬P] [¬¬P]
────────────── ¬E
⊥
────────── RAA
P
─────────────── →I
¬¬P → P
example (P : Prop) : ¬¬P → P :=
fun h => Classical.byContradiction (fun hnP => h hnP)
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! 🐙