3.7. Exemplos Resolvidos
Cada exemplo abaixo é conduzido por inteiro, da escolha das equações às verificações que a seguem. Eles são disjuntos dos exercícios, e Lean verifica cada linha na construção das notas.
3.7.1. Subtração truncada
A subtração sobre ℕ não tem resultados negativos, então sub 3 7 deve ser 0. A recursão descasca um succ de cada argumento ao mesmo tempo, o que faz de m + 1, n + 1 a equação recursiva. Dois casos base a interrompem. Subtrair zero devolve o primeiro argumento, e subtrair de zero devolve zero. As equações são tentadas em ordem, então o par 0, 0 cai na primeira delas e nunca alcança a segunda.
def sub : ℕ → ℕ → ℕ
| m, 0 => m
| 0, _ => 0
| m + 1, n + 1 => sub m n
A primeira verificação executa a equação recursiva três vezes, e a segunda esgota o primeiro argumento antes do segundo.
#eval sub 7 3
#eval sub 3 7
As duas verificações são equações fechadas, então cada uma é também um teorema que rfl prova.
example : sub 3 7 = 0 := rfl
3.7.2. Avaliar uma expressão passo a passo
Tome a expressão (x + 3) * y da §3.2 e um ambiente que leva "x" a 2 e "y" a 4. Cada passo abaixo aplica uma equação de eval, primeiro o caso mul, depois o caso add, depois os casos var e num, e a aritmética de ℤ conclui a computação.
eval env ((x + 3) * y) = eval env (x + 3) * eval env y = (eval env x + eval env 3) * env "y" = (env "x" + 3) * env "y" = (2 + 3) * 4 = 20
O ambiente é uma função de nomes em inteiros, e o casamento de padrões sobre cadeias de caracteres o define.
def workedEnv : String → ℤ
| "x" => 2
| "y" => 4
| _ => 0
Lean realiza a mesma computação.
#eval eval workedEnv
(AExp.mul (AExp.add (AExp.var "x") (AExp.num 3))
(AExp.var "y"))
A expressão não contém variáveis de Lean, apenas nomes de variáveis que o ambiente resolve, então a equação é fechada e rfl a prova.
example : eval workedEnv
(AExp.mul (AExp.add (AExp.var "x") (AExp.num 3))
(AExp.var "y")) = 20 := rfl
3.7.3. O que a computação resolve
A função add recursa sobre o seu segundo argumento. Esse único fato decide quais equações rfl prova. A primeira equação abaixo é fechada, então os dois lados computam para 9. A segunda é geral, mas add m 0 casa a primeira equação de add qualquer que seja m, e reduz a m em um passo.
example : add 2 7 = 9 := rfl
example (m : ℕ) : add m 0 = m := rfl
Trocar os argumentos muda tudo. Em add 0 m a variável está onde a recursão olha, equação alguma se aplica e o termo trava. A afirmação é verdadeira e rfl não a prova.
namespace Worked
theorem zero_add (m : ℕ) : add 0 m = m := m:ℕ⊢ add 0 m = m
All goals completed! 🐙
end Worked
A prova exige indução estrutural sobre m, assunto das próximas aulas. A lição se generaliza. O que a computação resolve depende da forma da recursão, não da forma do enunciado.
3.7.4. Da definição ao enunciado
Uma definição costuma sugerir as leis que deve satisfazer. Acrescentar um elemento ao final de uma lista é a imagem espelhada de cons, então a operação recursa sobre a lista e a reconstrói em torno da chamada recursiva.
def snoc {α : Type} : List α → α → List α
| [], y => [y]
| x :: xs, y => x :: snoc xs y
#eval snoc [1, 2] 3
A reversão e snoc devem concordar: reverter x :: xs põe x ao final da reversão de xs. Enunciar a lei não custa nada, e o enunciado é o que uma aula adiante prova.
namespace Worked
theorem reverse_cons {α : Type} (x : α) (xs : List α) :
reverse (x :: xs) = snoc (reverse xs) x := α:Typex:αxs:List α⊢ reverse (x :: xs) = snoc (reverse xs) x
All goals completed! 🐙
end Worked
A computação não a resolve. O lado esquerdo desdobra para appendPretty (reverse xs) [x], o lado direito trava na lista variável, e os dois se encontram apenas sob indução. Escrever o enunciado primeiro, e prová-lo depois, é como um desenvolvimento cresce.