6.1. Tipos Indutivos e Seus Princípios
Um tipo indutivo é definido listando os seus construtores. Todo valor do tipo é construído aplicando esses construtores, e cada valor é construído de uma única maneira. A Aula 3 usou isso para construir ℕ a partir de Nat.zero e Nat.succ e List a partir de List.nil e List.cons. Para um tipo de dados como ℕ, Lean gera dos construtores quatro princípios, e nomeá-los explica de onde vêm as ferramentas das aulas anteriores.
O recursor T.rec é o princípio primitivo do tipo. É a forma bruta da recursão estrutural e, lido sobre um motivo que devolve uma proposição, a forma bruta da indução estrutural. O seu tipo para ℕ mostra os dois casos que uma função sobre ℕ deve fornecer, um para Nat.zero e um para Nat.succ, e o segundo caso recebe o valor no predecessor, que é o resultado recursivo.
#check @Nat.rec
#check @Nat.succ.injEq
O princípio casesOn é o caso especial não recursivo do recursor, aquele em que a tática cases da Aula 1 se traduz. O casamento de padrões e o compilador de equações transformam a sintaxe de superfície da Aula 3 em aplicações do recursor. A definição abaixo computa com Nat.rec diretamente, e a mesma função por casamento de padrões é a que a Aula 3 teria escrito; as duas são iguais.
namespace Func
def usingRec (n : ℕ) : ℕ :=
Nat.rec (motive := fun _ => ℕ) 0 (fun _ ih => ih + 2) n
example : usingRec 3 = 6 := rfl
end Func
Os dois princípios restantes dizem respeito aos próprios construtores. Cada construtor é injetivo, então aplicações iguais de construtores têm argumentos iguais, e Lean gera a equação Nat.succ.injEq que registra isso. Construtores distintos são disjuntos, então nenhuma aplicação de Nat.succ é igual a Nat.zero. A injetividade e a disjunção valem para um tipo de dados como ℕ; para um tipo de provas, onde todas as provas de uma proposição são iguais, elas não valem. A segunda saída acima é a equação de injetividade, e os dois exemplos abaixo usam a injetividade e a disjunção.
namespace Func
example (m n : ℕ) (h : Nat.succ m = Nat.succ n) :
m = n := m:ℕn:ℕh:m.succ = n.succ⊢ m = n
All goals completed! 🐙
example (n : ℕ) : Nat.succ n ≠ 0 :=
Nat.succ_ne_zero n
end Func
A tática induction da Aula 4 é o recursor lido sobre uma proposição, e a Aula 7 o deriva em geral e prova as leis que esta aula enuncia. Aqui o recursor é apenas nomeado, como a origem da recursão e da análise de casos já em uso.
Notas de margem. O Guia, capítulo 5. Avigad, de Moura, Kong, Ullrich, Theorem Proving in Lean 4, o capítulo sobre tipos indutivos. A referência da linguagem Lean sobre o comando inductive.