4.6. Provas por Indução Matemática
A tática induction realiza indução estrutural sobre uma variável, produzindo um subobjetivo nomeado por construtor do seu tipo. Para ℕ, construído com Nat.zero e Nat.succ, a indução estrutural é a indução matemática ordinária. Os nomes depois de um construtor ligam os seus argumentos e a hipótese de indução, então o ramo | succ n' ih fornece o predecessor n' e a hipótese ih sobre ele. A forma geral para ℕ se lê assim.
induction n with | zero => (prova do caso base) | succ n' ih => (prova do caso do passo)
A seção relembra add e mul da Aula 3 e prova as leis que a computação deixou em aberto lá. O arquivo de exercícios extraído repete as definições, então ele é autônomo.
namespace Backward
def add : ℕ → ℕ → ℕ
| m, Nat.zero => m
| m, Nat.succ n => Nat.succ (add m n)
def mul : ℕ → ℕ → ℕ
| _, Nat.zero => 0
| m, Nat.succ n => add m (mul m n)
end Backward
Os dois primeiros teoremas fornecem as equações para add quando o seu primeiro argumento é zero ou um sucessor, que a própria definição não dá, pois add recorre sobre o seu segundo argumento. Cada prova induz sobre esse segundo argumento, a variável que a recursão consome, e fecha o caso do passo com simp, usando as equações que definem add e a hipótese de indução.
namespace Backward
theorem add_zero (n : ℕ) : add 0 n = n := n:ℕ⊢ add 0 n = n
induction n with
⊢ add 0 0 = 0 All goals completed! 🐙
n':ℕih:add 0 n' = n'⊢ add 0 (n' + 1) = n' + 1 All goals completed! 🐙
theorem add_succ (m n : ℕ) :
add (Nat.succ m) n = Nat.succ (add m n) := m:ℕn:ℕ⊢ add m.succ n = (add m n).succ
induction n with
m:ℕ⊢ add m.succ 0 = (add m 0).succ All goals completed! 🐙
m:ℕn':ℕih:add m.succ n' = (add m n').succ⊢ add m.succ (n' + 1) = (add m (n' + 1)).succ All goals completed! 🐙
end Backward
Comutatividade e associatividade seguem, com os dois teoremas acima descarregando o caso base e o caso do passo da primeira. Eles reprovam as proposições enunciadas com sorry como SorryTheorems.add_comm e SorryTheorems.add_assoc na Aula 3, aqui como os novos teoremas Backward.add_comm e Backward.add_assoc. As declarações anteriores mantêm as suas provas com sorryAx, e outros enunciados da Aula 3, entre eles mul_comm, mul_assoc e reverse_reverse, continuam em aberto.
namespace Backward
theorem add_comm (m n : ℕ) : add m n = add n m := m:ℕn:ℕ⊢ add m n = add n m
induction n with
m:ℕ⊢ add m 0 = add 0 m All goals completed! 🐙
m:ℕn':ℕih:add m n' = add n' m⊢ add m (n' + 1) = add (n' + 1) m All goals completed! 🐙
theorem add_assoc (l m n : ℕ) :
add (add l m) n = add l (add m n) := l:ℕm:ℕn:ℕ⊢ add (add l m) n = add l (add m n)
induction n with
l:ℕm:ℕ⊢ add (add l m) 0 = add l (add m 0) All goals completed! 🐙
l:ℕm:ℕn':ℕih:add (add l m) n' = add l (add m n')⊢ add (add l m) (n' + 1) = add l (add m (n' + 1)) All goals completed! 🐙
end Backward
As duas instâncias abaixo registram add como associativo e comutativo, que é o que ac_rfl consulta. O comando instance é o que a Aula 2 usou para Membership e companhia, e o capítulo 5 do guia explica o mecanismo, na semana 6 da disciplina.
namespace Backward
instance Associative_add : Std.Associative add :=
{ assoc := add_assoc }
instance Commutative_add : Std.Commutative add :=
{ comm := add_comm }
end Backward
A distributividade fecha a seção, com ac_rfl terminando o que simp deixa.
namespace Backward
theorem mul_add (l m n : ℕ) :
mul l (add m n) = add (mul l m) (mul l n) := l:ℕm:ℕn:ℕ⊢ mul l (add m n) = add (mul l m) (mul l n)
induction n with
l:ℕm:ℕ⊢ mul l (add m 0) = add (mul l m) (mul l 0) All goals completed! 🐙
l:ℕm:ℕn':ℕih:mul l (add m n') = add (mul l m) (mul l n')⊢ mul l (add m (n' + 1)) = add (mul l m) (mul l (n' + 1))
l:ℕm:ℕn':ℕih:mul l (add m n') = add (mul l m) (mul l n')⊢ add l (add (mul l m) (mul l n')) = add (mul l m) (add l (mul l n'))
All goals completed! 🐙
end Backward
O guia oferece duas dicas. Induza sobre o argumento que a recursão consome, e leia um caso base difícil como sinal de variável de indução errada ou de um teorema auxiliar que falta.[addzero]
O guia chama add 0 n = n de add_zero, embora add recorra sobre o seu segundo argumento e a convenção usual leia o zero do enunciado, o que daria zero_add. O terceiro exemplo trabalhado da Aula 3 chamou o mesmo enunciado de zero_add. Estas notas mantêm os nomes do guia.
4.6.1. Exemplos
Os exemplos abaixo induzem sobre ℕ e uma vez sobre listas, observam os dois subobjetivos e verificam sobre o que as provas terminadas repousam. Nos objetivos, Lean imprime Nat.succ n' como n' + 1 e usa o + interno, não o nosso add, então um trace que mostra n' + 1 reflete o impressor, não uma mudança de definição.
Example 1. induction n with produz um ramo por construtor, e o trace mostra os objetivos do caso base e do passo.
example (n : ℕ) : add 0 n = n := n:ℕ⊢ add 0 n = n
induction n with
⊢ add 0 0 = 0
⊢ add 0 0 = 0
All goals completed! 🐙
n':ℕih:add 0 n' = n'⊢ add 0 (n' + 1) = n' + 1
n':ℕih:add 0 n' = n'⊢ add 0 (n' + 1) = n' + 1
All goals completed! 🐙
Example 2. O caso base sozinho. O zero à direita casa com a primeira equação de add, então rfl o fecha.
example : add 0 0 = 0 := ⊢ add 0 0 = 0
All goals completed! 🐙
Example 3. O caso do passo sozinho, a partir da sua hipótese de indução.
example (n' : ℕ) (ih : add 0 n' = n') :
add 0 (Nat.succ n') = Nat.succ n' := n':ℕih:add 0 n' = n'⊢ add 0 n'.succ = n'.succ
All goals completed! 🐙
Example 4. add_succ segue o mesmo padrão em um enunciado com duas variáveis, induzindo sobre a segunda, que a recursão consome.
example (m n : ℕ) :
add (Nat.succ m) n = Nat.succ (add m n) := m:ℕn:ℕ⊢ add m.succ n = (add m n).succ
induction n with
m:ℕ⊢ add m.succ 0 = (add m 0).succ All goals completed! 🐙
m:ℕn':ℕih:add m.succ n' = (add m n').succ⊢ add m.succ (n' + 1) = (add m (n' + 1)).succ All goals completed! 🐙
Example 5. A associatividade, induzindo sobre a última variável.
example (l m n : ℕ) :
add (add l m) n = add l (add m n) := l:ℕm:ℕn:ℕ⊢ add (add l m) n = add l (add m n)
induction n with
l:ℕm:ℕ⊢ add (add l m) 0 = add l (add m 0) All goals completed! 🐙
l:ℕm:ℕn':ℕih:add (add l m) n' = add l (add m n')⊢ add (add l m) (n' + 1) = add l (add m (n' + 1)) All goals completed! 🐙
Example 6. A variável de indução errada emperra o roteiro ingênuo. Induzir sobre m deixa objetivos que nem rfl nem a hipótese de indução fecham, e os traces mostram por quê: a recursão de add consome n, que os dois objetivos deixam intocado. O enunciado continua demonstrável, pois add_succ acima é exatamente ele, mas a rotina de caso base e passo das provas anteriores não se sustenta aqui.
example (m n : ℕ) :
add (Nat.succ m) n = Nat.succ (add m n) := m:ℕn:ℕ⊢ add m.succ n = (add m n).succ
induction m with
n:ℕ⊢ add (Nat.succ 0) n = (add 0 n).succ
n:ℕ⊢ add (Nat.succ 0) n = (add 0 n).succ
All goals completed! 🐙
n:ℕm':ℕih:add m'.succ n = (add m' n).succ⊢ add (m' + 1).succ n = (add (m' + 1) n).succ
n:ℕm':ℕih:add m'.succ n = (add m' n).succ⊢ add (m' + 1).succ n = (add (m' + 1) n).succ
All goals completed! 🐙
Example 7. Com as duas instâncias registradas, ac_rfl raciocina sobre add como raciocina sobre +.
example (a b c : ℕ) :
add (add a b) c = add c (add b a) := a:ℕb:ℕc:ℕ⊢ add (add a b) c = add c (add b a)
All goals completed! 🐙
Example 8. A equação recursiva de mul sobre o seu primeiro argumento, por indução sobre o segundo.
example (n : ℕ) : mul 0 n = 0 := n:ℕ⊢ mul 0 n = 0
induction n with
⊢ mul 0 0 = 0 All goals completed! 🐙
n':ℕih:mul 0 n' = 0⊢ mul 0 (n' + 1) = 0 All goals completed! 🐙
Example 9. A indução sobre uma lista tem um ramo por construtor de List, com nil como base e cons como passo. As semanas 6 e 7 tratam a indução estrutural sobre tipos indutivos arbitrários.
namespace Backward
theorem append_nil {α : 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 Backward
Example 10. A prova terminada repousa sobre propext, que simp usa, e não sobre sorryAx, fechando o ciclo com o terceiro exemplo da seção de teoremas da Aula 3.
#print axioms Backward.add_comm