6.8. Exercícios
Defina cada função e prove cada lei em Lean, substituindo sorry. Baixe o arquivo de exercícios Lecture06.lean e o abra no VS Code. Cada tipo é dado; a sua tarefa são as funções e as provas. As leis aqui se resolvem por rfl ou decide sobre valores fechados, já que as provas por indução pertencem à Aula 7. Os exercícios 9 e 10 são opcionais.
Exercise 1. Defina turnRight sobre as quatro direções da bússola, e prove por decide que virar à direita quatro vezes devolve o norte.
namespace FuncEx
inductive Direction where
| north | east | south | west
deriving DecidableEq
def turnRight : Direction → Direction :=
sorry
theorem turn_four :
turnRight (turnRight (turnRight
(turnRight Direction.north))) = Direction.north :=
sorry
end FuncEx
Exercise 2. Defina lastOpt, o último elemento de uma lista como uma opção, e prove o seu valor sobre a lista vazia e sobre uma lista concreta.
namespace FuncEx
def lastOpt {α : Type} : List α → Option α :=
sorry
theorem last_opt_nil {α : Type} :
lastOpt ([] : List α) = none :=
sorry
theorem last_opt_example :
lastOpt [3, 1, 4] = some 4 :=
sorry
end FuncEx
Exercise 3. Defina a área de um retângulo e prove uma área concreta.
namespace FuncEx
structure Rectangle where
width : ℕ
height : ℕ
def area (r : Rectangle) : ℕ :=
sorry
theorem area_example :
area { width := 3, height := 4 } = 12 :=
sorry
end FuncEx
Exercise 4. Estenda o retângulo a uma caixa com uma profundidade, e defina o seu volume a partir dos campos herdados.
namespace FuncExBox
structure Rectangle where
width : ℕ
height : ℕ
structure Box extends Rectangle where
depth : ℕ
def volume (b : Box) : ℕ :=
sorry
theorem volume_example :
volume { width := 2, height := 3, depth := 4 } = 24 :=
sorry
end FuncExBox
Exercise 5. Complete as instâncias de Doubler, dobrando um número por adição e uma lista por autoconcatenação, e o seletor, depois prove o valor dobrado para ℕ.
namespace FuncEx
class Doubler (α : Type) where
dup : α → α
instance : Doubler ℕ :=
sorry
instance {α : Type} : Doubler (List α) :=
sorry
def applyDup {α : Type} [Doubler α] (a : α) : α :=
sorry
theorem dup_nat : applyDup (3 : ℕ) = 6 :=
sorry
end FuncEx
Exercise 6. Conte as folhas e as ramificações de uma árvore binária, e verifique a relação entre elas sobre uma árvore concreta.
namespace FuncEx
inductive Tree (α : Type) where
| leaf
| branch (l : Tree α) (x : α) (r : Tree α)
def leaves {α : Type} : Tree α → ℕ :=
sorry
def nodes {α : Type} : Tree α → ℕ :=
sorry
def tx : Tree ℕ :=
.branch (.branch .leaf 1 .leaf) 2 .leaf
theorem leaves_nodes : leaves tx = nodes tx + 1 :=
sorry
end FuncEx
Exercise 7. Defina replicate, a lista de n cópias de um valor, e prove o seu valor em 0.
namespace FuncEx
def replicate {α : Type} : ℕ → α → List α :=
sorry
theorem replicate_zero {α : Type} (x : α) :
replicate 0 x = [] :=
sorry
end FuncEx
Exercise 8. Defina isEmpty por um match, e prove as suas duas leis computacionais.
namespace FuncEx
def isEmpty {α : Type} : List α → Bool :=
sorry
theorem is_empty_nil {α : Type} :
isEmpty ([] : List α) = true :=
sorry
theorem is_empty_cons {α : Type} (x : α)
(xs : List α) : isEmpty (x :: xs) = false :=
sorry
end FuncEx
Exercise 9. Opcional. Uma árvore rosa ramifica em uma lista de subárvores. Defina rsize, o número dos seus nós, notando a recursão aninhada através de List.
namespace FuncEx
inductive Rose (α : Type) where
| node (x : α) (children : List (Rose α))
def rsize {α : Type} : Rose α → ℕ :=
sorry
end FuncEx
Exercise 10. Opcional. Um vetor indexado pelo comprimento exclui o caso vazio no seu tipo. Defina a cabeça total de um vetor não vazio e a avalie.
namespace FuncEx
inductive Vec (α : Type) : ℕ → Type where
| nil : Vec α 0
| cons {n : ℕ} : α → Vec α n → Vec α (n + 1)
def vhead {α : Type} {n : ℕ} : Vec α (n + 1) → α :=
sorry
def vx : Vec ℕ 2 := .cons 3 (.cons 4 .nil)
end FuncEx