Verificação Formal de Software

1.10. Exercícios🔗

Prove cada enunciado em Lean, substituindo sorry por uma prova. Baixe o arquivo de exercícios Lecture01.lean e abra-o no VS Code.

Exercício 1. A implicação compõe.

theorem declaration uses `sorry`exercise1 (P Q R : Prop)
    (hPQ : P → Q) (hQR : Q → R) : P → R := byP:PropQ:PropR:ProphPQ:P → QhQR:Q → R⊢ P → R
  sorryAll goals completed! 🐙

Exercício 2. A conjunção distribui sobre a disjunção.

theorem declaration uses `sorry`exercise2 (P Q R : Prop) :
    P ∧ (Q ∨ R) ↔ (P ∧ Q) ∨ (P ∧ R) := byP:PropQ:PropR:Prop⊢ P ∧ (Q ∨ R) ↔ P ∧ Q ∨ P ∧ R
  sorryAll goals completed! 🐙

Exercício 3. A disjunção associa.

theorem declaration uses `sorry`exercise3 (P Q R : Prop) :
    (P ∨ Q) ∨ R → P ∨ (Q ∨ R) := byP:PropQ:PropR:Prop⊢ (P ∨ Q) ∨ R → P ∨ Q ∨ R
  sorryAll goals completed! 🐙

Exercício 4. Esta direção da primeira lei de De Morgan é construtiva.

theorem declaration uses `sorry`exercise4 (P Q : Prop) : ¬P ∨ ¬Q → ¬(P ∧ Q) := byP:PropQ:Prop⊢ ¬P ∨ ¬Q → ¬(P ∧ Q)
  sorryAll goals completed! 🐙

Exercício 5. Lei de Peirce.C. S. Peirce, On the Algebra of Logic: A Contribution to the Philosophy of Notation, American Journal of Mathematics 7(2), 1885, pp. 180–196. Ela requer raciocínio clássico; considere uma análise de casos sobre Classical.em P.

theorem declaration uses `sorry`exercise5 (P Q : Prop) : ((P → Q) → P) → P := byP:PropQ:Prop⊢ ((P → Q) → P) → P
  sorryAll goals completed! 🐙

Exercício 6. A disjunção distribui sobre a conjunção.

theorem declaration uses `sorry`exercise6 (P Q R : Prop) :
    P ∨ (Q ∧ R) ↔ (P ∨ Q) ∧ (P ∨ R) := byP:PropQ:PropR:Prop⊢ P ∨ Q ∧ R ↔ (P ∨ Q) ∧ (P ∨ R)
  sorryAll goals completed! 🐙

Exercício 7. Uma implicação para uma conjunção divide-se em duas implicações.

theorem declaration uses `sorry`exercise7 (P Q R : Prop) :
    (P → Q ∧ R) ↔ (P → Q) ∧ (P → R) := byP:PropQ:PropR:Prop⊢ P → Q ∧ R ↔ (P → Q) ∧ (P → R)
  sorryAll goals completed! 🐙

Exercício 8. De uma disjunção e da negação de um dos disjuntos, o outro vale.

theorem declaration uses `sorry`exercise8 (P Q : Prop) : (P ∨ Q) → ¬P → Q := byP:PropQ:Prop⊢ P ∨ Q → ¬P → Q
  sorryAll goals completed! 🐙

Exercício 9. Nenhuma proposição é equivalente à sua própria negação.

theorem declaration uses `sorry`exercise9 (P : Prop) : ¬(P ↔ ¬P) := byP:Prop⊢ ¬(P ↔ ¬P)
  sorryAll goals completed! 🐙

Exercício 10. De duas proposições quaisquer, uma implica a outra. Requer raciocínio clássico; considere uma análise de casos sobre Classical.em P.

theorem declaration uses `sorry`exercise10 (P Q : Prop) : (P → Q) ∨ (Q → P) := byP:PropQ:Prop⊢ (P → Q) ∨ (Q → P)
  sorryAll goals completed! 🐙