3.3. Funções por Casamento de Padrões e Recursão
Uma função sobre um tipo indutivo se define por casamento de padrões, uma equação por forma de construtor. A recursão é estrutural quando cada chamada recursiva descasca um construtor, e Lean aceita essas definições, já que elas terminam. As definições abaixo trabalham sobre o ℕ do núcleo, cujos construtores são Nat.zero e Nat.succ.
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)
def power : ℕ → ℕ → ℕ
| _, Nat.zero => 1
| m, Nat.succ n => mul m (power m n)
Os padrões são mais ricos que construtores nus. A função de Fibonacci casa zero, um e todo número da forma n + 2, que abrevia duas aplicações de succ.
def fib : ℕ → ℕ
| 0 => 0
| 1 => 1
| n + 2 => fib (n + 1) + fib n
Um argumento que nenhuma equação inspeciona pode ir para a esquerda dos dois-pontos, onde se torna um parâmetro fixo ao longo da recursão.
def powerParam (m : ℕ) : ℕ → ℕ
| Nat.zero => 1
| Nat.succ n => mul m (powerParam m n)
3.3.1. Exemplos
Os exemplos abaixo definem funções por casamento de padrões e recursão estrutural sobre ℕ e sobre Bool.
Exemplo 1. A metade descarta um de cada par, casando a forma n + 2.
def half : ℕ → ℕ
| 0 => 0
| 1 => 0
| n + 2 => half n + 1
Exemplo 2. Uma definição não recursiva dispensa o casamento de padrões. O quadrado reaproveita mul.
def square (n : ℕ) : ℕ := mul n n
Exemplo 3. O teste de zero devolve um Bool, e as duas equações cobrem os dois construtores.
def isZero : ℕ → Bool
| Nat.zero => true
| Nat.succ _ => false
Exemplo 4. O fatorial recursa sobre a forma n + 1, e a forma com parâmetro mantém a multiplicação explícita.
def factorial : ℕ → ℕ
| 0 => 1
| n + 1 => mul (n + 1) (factorial n)
Exemplo 5. Casamento de padrões em dois argumentos ao mesmo tempo. O menor de dois números desce em ambos.
def smaller : ℕ → ℕ → ℕ
| _, 0 => 0
| 0, _ => 0
| m + 1, n + 1 => smaller m n + 1
Exemplo 6. Os números de Lucas seguem a recursão de Fibonacci a partir de valores iniciais diferentes.
def lucas : ℕ → ℕ
| 0 => 2
| 1 => 1
| n + 2 => lucas (n + 1) + lucas n
Exemplo 7. A conjunção sobre Bool casa apenas o seu primeiro argumento.
def conj : Bool → Bool → Bool
| true, b => b
| false, _ => false
Exemplo 8. A paridade recursa de dois em dois, então a chamada recursiva descasca dois construtores.
def evenb : ℕ → Bool
| 0 => true
| 1 => false
| n + 2 => evenb n
Exemplo 9. A soma dos n primeiros números recursa sobre n + 1.
def sumTo : ℕ → ℕ
| 0 => 0
| n + 1 => (n + 1) + sumTo n
Exemplo 10. As potências de dois como uma instância da recursão de power, com a base fixa.
def twoPow : ℕ → ℕ
| 0 => 1
| n + 1 => mul 2 (twoPow n)