4.8. Exercícios
Prove cada enunciado em Lean, substituindo sorry. Baixe o arquivo de exercícios Lecture04.lean e abra-o no VS Code. O arquivo já contém as definições de add e mul e os teoremas da §4.6, então os exercícios de indução podem se apoiar neles. Os exercícios 1 a 6 usam apenas intro, apply e exact; os exercícios 7 a 9 usam induction, simp e rw; o exercício 10 é opcional.
Exercise 1. Duas maneiras de alimentar hipóteses a uma função. A primeira fornece a mesma premissa duas vezes; a segunda reordena as premissas antes de aplicar.
namespace Backward
theorem contract (a b : Prop) :
(a → a → b) → a → b :=
sorry
theorem pull (a b c : Prop) :
a → (a → b → c) → b → c :=
sorry
end Backward
Exercise 2. Uma implicação cuja conclusão é uma conjunção se divide em uma implicação para cada parte.
namespace Backward
theorem imp_into_and (a b c : Prop) :
(a → b) → (a → c) → a → b ∧ c :=
sorry
end Backward
Exercise 3. Duas provas do mesmo enunciado, diferindo na injeção que escolhem.
namespace Backward
theorem left_choice (a : Prop) :
a → a ∨ a :=
sorry
-- Dê uma resposta diferente da de `left_choice`:
theorem right_choice (a : Prop) :
a → a ∨ a :=
sorry
end Backward
Exercise 4. Um revezamento de três implicações leva a primeira hipótese à última conclusão.
namespace Backward
theorem relay (a b c d : Prop) :
(a → b) → (b → c) → (c → d) → a → d :=
sorry
end Backward
Exercise 5. Uma proposição junto com a sua negação prova qualquer coisa. Lembre que ¬a abrevia a → False.
namespace Backward
theorem absurd_imp (a b : Prop) :
a → ¬ a → b :=
sorry
end Backward
Exercise 6. Uma implicação a partir de um existencial produz uma implicação universalmente quantificada. Este exercício prova essa direção, e a recíproca também vale.
namespace Backward
theorem exists_imp {α : Type} (p : α → Prop) (q : Prop) :
((∃ x, p x) → q) → ∀ x, p x → q :=
sorry
end Backward
Exercise 7. Um é a identidade à esquerda de mul, por indução no segundo argumento.
namespace Backward
theorem one_mul (n : ℕ) :
mul 1 n = n :=
sorry
end Backward
Exercise 8. A parcela à esquerda de uma soma aninhada passa pela do meio, reescrevendo com associatividade e comutatividade.
namespace Backward
theorem add_left_comm (l m n : ℕ) :
add l (add m n) = add m (add l n) :=
sorry
end Backward
Exercise 9. A parcela à direita de uma soma aninhada passa pela do meio.
namespace Backward
theorem add_right_comm (l m n : ℕ) :
add (add l m) n = add (add l n) m :=
sorry
end Backward
Exercise 10. Opcional. Somar um número a si mesmo é igual a multiplicá-lo por dois, e os dois lados já coincidem por computação.
namespace Backward
theorem two_mul (n : ℕ) :
add n n = mul n 2 :=
sorry
end Backward