5.6. Provas por Casamento de Padrões e Recursão
Sob o princípio PAT, uma função recursiva que devolve uma prova é uma prova por indução, e a chamada recursiva é a hipótese de indução. Uma definição por casamento de padrões sobre uma lista tem uma equação para a lista vazia e uma para um cons, e a equação para x :: xs pode chamar a função na lista menor xs, que é o apelo à hipótese de indução. A seção mostra duas identidades de listas provadas desse modo e afirma claramente que a teoria geral da indução estrutural sobre tipos indutivos arbitrários é o tema das semanas 6 e 7. Aqui a recursão aparece apenas como um dispositivo de prova progressiva.
Duas identidades auxiliares vêm primeiro. Anexar a lista vazia à direita nada muda, e a anexação é associativa. Cada uma é provada por recursão sobre a primeira lista, e a chamada recursiva carrega a hipótese de indução; congrArg (List.cons x) reconstrói o cons ao redor dela.
namespace Forward
theorem append_nil {α : Type} :
∀ (xs : List α), appendPretty xs [] = xs
| [] => rfl
| x :: xs => congrArg (List.cons x) (append_nil xs)
theorem append_assoc {α : Type} :
∀ (xs ys zs : List α),
appendPretty (appendPretty xs ys) zs
= appendPretty xs (appendPretty ys zs)
| [], _, _ => rfl
| x :: xs, ys, zs =>
congrArg (List.cons x) (append_assoc xs ys zs)
end Forward
A reversão se distribui sobre a anexação, em ordem invertida. A prova recorre sobre a primeira lista, usando as duas auxiliares e a chamada recursiva, que simp consome como regras de reescrita.
namespace Forward
theorem reverse_append {α : Type} :
∀ (xs ys : List α),
reverse (appendPretty xs ys)
= appendPretty (reverse ys) (reverse xs)
α:Typeys:List α⊢ reverse (appendPretty [] ys) = appendPretty (reverse ys) (reverse []) α:Typeys:List α⊢ reverse (appendPretty [] ys) = appendPretty (reverse ys) (reverse [])
All goals completed! 🐙
α:Typex:αxs:List αys:List α⊢ reverse (appendPretty (x :: xs) ys) = appendPretty (reverse ys) (reverse (x :: xs)) α:Typex:αxs:List αys:List α⊢ reverse (appendPretty (x :: xs) ys) = appendPretty (reverse ys) (reverse (x :: xs))
All goals completed! 🐙
end Forward
O mesmo enunciado provado pela tática induction da Aula 4 é a mesma prova em outra roupagem. O caso base é o ramo nil, e o caso do passo é o ramo cons, cuja hipótese de indução ih é exatamente a chamada recursiva acima.
namespace Forward
theorem reverse_append_tactical {α : Type}
(xs ys : List α) :
reverse (appendPretty xs ys)
= appendPretty (reverse ys) (reverse xs) := α:Typexs:List αys:List α⊢ reverse (appendPretty xs ys) = appendPretty (reverse ys) (reverse xs)
induction xs with
α:Typeys:List α⊢ reverse (appendPretty [] ys) = appendPretty (reverse ys) (reverse [])
All goals completed! 🐙
α:Typeys:List αx:αxs':List αih:reverse (appendPretty xs' ys) = appendPretty (reverse ys) (reverse xs')⊢ reverse (appendPretty (x :: xs') ys) = appendPretty (reverse ys) (reverse (x :: xs'))
All goals completed! 🐙
end Forward
5.6.1. Exemplos
Os exemplos abaixo provam identidades de listas e de números por recursão, colocam a prova recursiva ao lado da tática induction, nomeiam a chamada recursiva como a hipótese de indução e marcam a disciplina que as semanas 6 e 7 formalizam.
Example 1. Uma prova por recursão sobre ℕ, o seu caso base 0 e o seu caso do passo n + 1, reescrevendo a indução da Aula 4 como casamento de padrões. A identidade é add 0 n = n para o add da Aula 3.
namespace Forward
theorem add_zero_rec :
∀ (n : ℕ), add 0 n = n
| 0 => rfl
n:ℕ⊢ add 0 (n + 1) = n + 1 n:ℕ⊢ add 0 (n + 1) = n + 1 All goals completed! 🐙
end Forward
Example 2. O caso base da associatividade sozinho. A primeira lista vazia faz os dois lados se reduzirem ao mesmo termo, de modo que rfl o fecha.
namespace Forward
example {α : Type} (ys zs : List α) :
appendPretty (appendPretty [] ys) zs
= appendPretty [] (appendPretty ys zs) :=
rfl
end Forward
Example 3. O caso do passo torna explícita a hipótese de indução. A chamada recursiva ih prova a associatividade das listas menores, e congrArg (List.cons x) reconstrói o cons ao redor dela.
namespace Forward
example {α : Type} (x : α) (xs ys zs : List α)
(ih : appendPretty (appendPretty xs ys) zs
= appendPretty xs (appendPretty ys zs)) :
appendPretty (appendPretty (x :: xs) ys) zs
= appendPretty (x :: xs) (appendPretty ys zs) :=
congrArg (List.cons x) ih
end Forward
Example 4. O caso base de reverse_append, onde a reversão da lista vazia e a identidade à direita da anexação juntas fecham o objetivo.
namespace Forward
example {α : Type} (ys : List α) :
reverse (appendPretty [] ys)
= appendPretty (reverse ys)
(reverse ([] : List α)) := α:Typeys:List α⊢ reverse (appendPretty [] ys) = appendPretty (reverse ys) (reverse [])
All goals completed! 🐙
end Forward
Example 5. O caso do passo de reverse_append, usando a hipótese de indução ih e a associatividade da anexação.
namespace Forward
example {α : Type} (x : α) (xs ys : List α)
(ih : reverse (appendPretty xs ys)
= appendPretty (reverse ys) (reverse xs)) :
reverse (appendPretty (x :: xs) ys)
= appendPretty (reverse ys)
(reverse (x :: xs)) := α:Typex:αxs:List αys:List αih:reverse (appendPretty xs ys) = appendPretty (reverse ys) (reverse xs)⊢ reverse (appendPretty (x :: xs) ys) = appendPretty (reverse ys) (reverse (x :: xs))
All goals completed! 🐙
end Forward
Example 6. A identidade à direita da anexação pela tática induction. É a mesma prova que o append_nil recursivo acima, em outra roupagem.
namespace Forward
example {α : Type} (xs : List α) :
appendPretty xs [] = xs := α:Typexs:List α⊢ appendPretty xs [] = xs
induction xs with
α:Type⊢ appendPretty [] [] = [] All goals completed! 🐙
α:Typex:αxs':List αih:appendPretty xs' [] = xs'⊢ appendPretty (x :: xs') [] = x :: xs' All goals completed! 🐙
end Forward
Example 7. A prova recursiva concluída se apoia em propext, que simp usa, e não em sorryAx, de modo que a recursão é genuína.
namespace Forward
#print axioms reverse_append
end Forward
Example 8. Nem toda definição recursiva é aceita. A definição abaixo chama a si mesma na mesma lista, de modo que nenhum argumento diminui e a recursão nunca termina, e Lean a rejeita com um erro de terminação. A disciplina que as semanas 6 e 7 formalizam é exatamente o que exclui definições como essa.
def loopForever {α : Type} : List α → List α
| [] => []
| x :: xs => loopForever (x :: xs)
Example 9. Uma identidade, duas provas. A associatividade da anexação por recursão e pela tática induction provam a mesma proposição, e ambas se apoiam apenas na recursão estrutural.
namespace Forward
example {α : Type} (xs ys zs : List α) :
appendPretty (appendPretty xs ys) zs
= appendPretty xs (appendPretty ys zs) := α:Typexs:List αys:List αzs:List α⊢ appendPretty (appendPretty xs ys) zs = appendPretty xs (appendPretty ys zs)
induction xs with
α:Typeys:List αzs:List α⊢ appendPretty (appendPretty [] ys) zs = appendPretty [] (appendPretty ys zs) All goals completed! 🐙
α:Typeys:List αzs:List αx:αxs':List αih:appendPretty (appendPretty xs' ys) zs = appendPretty xs' (appendPretty ys zs)⊢ appendPretty (appendPretty (x :: xs') ys) zs = appendPretty (x :: xs') (appendPretty ys zs) All goals completed! 🐙
end Forward
Example 10. A forma geral. Uma recursão estrutural sobre um tipo indutivo tem um ramo por construtor, e cada chamada recursiva, tomada sobre um valor menor, é a hipótese de indução para aquele ramo. As semanas 6 e 7 tornam isso preciso para tipos indutivos arbitrários; o reverse_reverse dos exemplos resolvidos é mais uma instância.
namespace Forward
example {α : Type} (xs : List α) :
reverse (appendPretty xs []) = reverse xs := α:Typexs:List α⊢ reverse (appendPretty xs []) = reverse xs
All goals completed! 🐙
end Forward