6.7. Exemplos Resolvidos
Cada exemplo abaixo é conduzido por extenso e verbalizado. Eles são disjuntos dos exemplos das seções e dos exercícios, e Lean verifica cada linha quando as notas são compiladas.
6.7.1. Expressões aritméticas e sua avaliação
Uma expressão aritmética é uma constante, uma variável, uma soma ou um produto, e isto é um tipo indutivo com quatro construtores, dois deles recursivos. Um avaliador toma um ambiente que dá um valor a cada variável e computa o valor de uma expressão por recursão sobre a sua estrutura.
namespace Func
inductive AExp where
| const (i : ℤ)
| var (x : String)
| add (a b : AExp)
| mul (a b : AExp)
def eval (env : String → ℤ) : AExp → ℤ
| .const i => i
| .var x => env x
| .add a b => eval env a + eval env b
| .mul a b => eval env a * eval env b
end Func
A expressão abaixo lê 2 + x × 5, e sob um ambiente que dá a x o valor 3 ela avalia para 17.
namespace Func
def sampleEnv : String → ℤ :=
fun s => if s = "x" then 3 else 0
def e1 : AExp :=
.add (.const 2) (.mul (.var "x") (.const 5))
#eval eval sampleEnv e1
end Func
A equação de definição para uma soma dá a lei eval env (add a b) = eval env a + eval env b, e ela vale por computação, já que a equação é exatamente o passo da recursão.
namespace Func
example (env : String → ℤ) (a b : AExp) :
eval env (.add a b)
= eval env a + eval env b := rfl
end Func
Essas expressões são a sintaxe de uma pequena linguagem, e o ambiente é o seu estado. A semântica operacional das semanas de lógica de Hoare se apoia exatamente nesta forma.
6.7.2. Uma classe de tipos para tamanho
A classe Size da §6.5 se estende a árvores com mais uma instância, e uma função então mede uma lista inteira de valores dimensionáveis. A resolução fornece a instância de árvore para cada elemento e a estrutura da lista conduz a recursão.
namespace Func
instance {α : Type} : Size (Tree α) where
size := treeSize
def totalSize {α : Type} [Size α] : List α → ℕ
| [] => 0
| x :: xs => Size.size x + totalSize xs
end Func
A lista abaixo guarda uma árvore e o seu espelho, cada uma de tamanho 2, então o total é 4.
namespace Func
#eval totalSize [t1, mirror t1]
end Func
A função pede [Size α] uma vez, e a resolução encontra a instância de árvore porque os elementos são árvores. A instância de Membership da Aula 2 e a instância de associatividade da Aula 4 são o mesmo mecanismo visto às claras, uma operação atada a um tipo e encontrada pelo seu tipo.
6.7.3. Um registro com uma extensão
Um registro reúne campos relacionados sob um nome, e extends constrói um registro especializado sobre um geral. Uma conta tem um titular e um saldo, e uma conta nomeada acrescenta um apelido mantendo os dois campos herdados.
namespace Func
structure Account where
owner : String
balance : ℤ
structure NamedAccount extends Account where
nickname : String
def acc : NamedAccount :=
{ owner := "A", balance := 100, nickname := "main" }
example : acc.owner = "A" := rfl
example : acc.balance = 100 := ⊢ acc.balance = 100 All goals completed! 🐙
end Func
Construir o registro com a sintaxe de campos e projetar um campo devolve esse campo, por computação. O único construtor de uma estrutura é a mesma ideia do And.intro da Aula 1, um construtor reunindo vários argumentos, com os campos nomeados em vez de posicionais.
6.7.4. Espelhando uma árvore
O mirror da §6.6 troca as subárvores em cada ramificação, então espelhar duas vezes deve devolver a árvore original. Sobre uma árvore fechada isso vale por computação.
namespace Func
example : mirror (mirror t1) = t1 := rfl
end Func
A lei geral mirror (mirror t) = t, para toda árvore t, não é uma computação. Ela precisa de indução estrutural, com as chamadas recursivas de mirror fornecendo as hipóteses de indução para as duas subárvores, e é o primeiro exemplo resolvido da Aula 7. Isto fecha o ciclo com o reverse_reverse da Aula 5, que provou o análogo para listas por recursão, e prepara a indução que virá.