3.8. Exercícios
Defina cada função e prove ou enuncie cada teorema, substituindo sorry. Baixe o arquivo de exercícios Lecture03.lean e abra-o no VS Code. O arquivo já contém as definições de AExp, eval, appendPretty e reverse da aula.
Exercício 1. Defina a função predecessor, com pred 0 = 0.
def pred : ℕ → ℕ := sorry
-- Esperado: #eval pred 5 dá 4, #eval pred 0 dá 0.
Exercício 2. Defina a duplicação por recursão, sem *, e prove a equação fechada por computação.
def double : ℕ → ℕ := sorry
theorem double_five : double 5 = 10 := sorry
Exercício 3. Defina o ambiente que leva "x" a 3, "y" a 17 e todo outro nome a 201, e prove as duas avaliações por computação.
def someEnv : String → ℤ := sorry
theorem eval_sub :
eval someEnv
(AExp.sub (AExp.var "y") (AExp.var "x")) = 14 :=
sorry
theorem eval_div_zero :
eval someEnv
(AExp.div (AExp.var "y") (AExp.num 0)) = 0 :=
sorry
Exercício 4. Defina a soma de uma lista de números naturais, e prove a equação fechada por computação.
def sumList : List ℕ → ℕ := sorry
theorem sumList_example : sumList [1, 2, 3] = 6 := sorry
Exercício 5. Defina o comprimento de uma lista, com argumento de tipo implícito, e prove a equação fechada por computação.
def length {α : Type} : List α → ℕ := sorry
theorem length_three : length [1, 2, 3] = 3 := sorry
Exercício 6. Defina map, que aplica uma função a cada elemento, e enuncie, com sorry, as suas duas leis funtoriais. Mapear a função identidade não muda nada, e mapear uma composição equivale a compor os mapeamentos.
def map {α β : Type} (f : α → β) : List α → List β :=
sorry
-- Enuncie as duas leis aqui como teoremas provados por
-- sorry:
-- map_ident : mapear (fun x => x) sobre xs dá xs.
-- map_comp : map g (map f xs) é igual a mapear a
-- composição das duas sobre xs.
Exercício 7. Defina flatten, que concatena uma lista de listas com appendPretty, e enuncie, com sorry, que o comprimento do resultado é a soma dos comprimentos das listas internas, usando length, map e sumList dos exercícios acima.
def flatten {α : Type} : List (List α) → List α := sorry
-- Enuncie flatten_length aqui como um teorema provado por
-- sorry: length (flatten xss) é igual a
-- sumList (map length xss).
Exercício 8. Complete simplify, que remove as somas com 0, os produtos por 1 e as divisões por 1, seguindo os casos dados, e enuncie, com sorry, a sua correção. Simplificar preserva o valor sob todo ambiente.
def simplify : AExp → AExp
| AExp.add (AExp.num 0) e₂ => simplify e₂
| AExp.add e₁ (AExp.num 0) => simplify e₁
| AExp.sub e₁ e₂ => sorry
| AExp.mul e₁ e₂ => sorry
| AExp.div e₁ e₂ => sorry
| AExp.add e₁ e₂ =>
AExp.add (simplify e₁) (simplify e₂)
| e => e
-- Enuncie simplify_correct aqui como um teorema provado
-- por sorry: para todo env e todo e, eval env
-- (simplify e) é igual a eval env e.
Exercício 9. Defina o tamanho de uma expressão, contando cada construtor, e a sua profundidade, contando a maior cadeia de construtores, e enuncie, com sorry, que a profundidade nunca excede o tamanho.
def size : AExp → ℕ := sorry
def depth : AExp → ℕ := sorry
theorem depth_le_size (e : AExp) :
depth e ≤ size e := sorry
Exercício 10. Defina mirror, que troca os operandos de cada soma e de cada produto e deixa o resto inalterado, e enuncie, com sorry, que espelhar preserva o valor sob todo ambiente.
def mirror : AExp → AExp := sorry
-- Enuncie mirror_eval aqui como um teorema provado por
-- sorry.