5.8. Exercícios
Prove cada enunciado em Lean, substituindo sorry. Baixe o arquivo de exercícios Lecture05.lean e o abra no VS Code. Cada exercício pede uma prova estruturada. Os exercícios 1 a 6 usam fix, assume, have, show e os nomes das regras apenas, sem táticas; os exercícios 7 e 8 usam calc; os exercícios 9 e 10 são opcionais.
Exercise 1. O combinador S, distribuindo um argumento por duas funções.
namespace Forward
theorem S (a b c : Prop) :
(a → b → c) → (a → b) → a → c :=
sorry
end Forward
Exercise 2. Currificação e descurrificação, as duas direções como um bicondicional.
namespace Forward
theorem curry_iff (a b c : Prop) :
(a ∧ b → c) ↔ (a → b → c) :=
sorry
end Forward
Exercise 3. Um bicondicional é simétrico, construído a partir das suas duas direções.
namespace Forward
theorem iff_symm (a b : Prop) :
(a ↔ b) → (b ↔ a) :=
sorry
end Forward
Exercise 4. A não contradição, lembrando que ¬ a abrevia a → False.
namespace Forward
theorem non_contradiction (a : Prop) :
¬ (a ∧ ¬ a) :=
sorry
end Forward
Exercise 5. Uma implicação a partir de uma disjunção se divide em duas.
namespace Forward
theorem or_imp (a b c : Prop) :
(a ∨ b → c) ↔ (a → c) ∧ (b → c) :=
sorry
end Forward
Exercise 6. Uma regra do ponto único concreta. Instanciar a guarda no valor fixo colapsa o quantificador.
namespace Forward
theorem forall_eq_three (P : ℕ → Prop) :
(∀ x, x = 3 → P x) ↔ P 3 :=
sorry
end Forward
Exercise 7. Duplicar uma soma, por calc. Dica: Nat.two_mul abre a duplicação e ac_rfl fecha o rearranjo.
namespace Forward
theorem two_distrib (a b : ℕ) :
2 * (a + b) = a + a + (b + b) :=
sorry
end Forward
Exercise 8. Distributividade à direita da multiplicação sobre uma soma, por calc.
namespace Forward
theorem calc_chain (a b c : ℕ) :
(a + b) * c = a * c + b * c :=
sorry
end Forward
Exercise 9. Opcional. A regra do ponto único concreta para ∃, o seu espelho no lado existencial.
namespace Forward
theorem exists_eq_three (P : ℕ → Prop) :
(∃ x, x = 3 ∧ P x) ↔ P 3 :=
sorry
end Forward
Exercise 10. Opcional. Currificar uma conjunção tripla, ambas as direções.
namespace Forward
theorem curry_three (a b c d : Prop) :
(a ∧ b ∧ c → d) ↔ (a → b → c → d) :=
sorry
end Forward