Verificação Formal de Software

1.6. 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! 🐙