Recursion and Induction on (Indexed) Inductive Types

We have been using match expressions to define functions on inductive types. In this file, we will see how to define functions using recursion and induction principles. These principles are automatically generated by Lean when an inductive type is defined, with functions like Nat.rec automatically introduced.

The function that allows us to define (dependent) functions by recursion and prove results by induction on the natural numbers is Nat.rec. It has the following type:

The motive should really be motif, i.e., a template. To define functions to say Nat, the motive is the constant function with value Nat. We will first focus on this case. The motive is constant for recursive definitions of (non dependent) functions.

What the above says is that to define a function f recusively, the data we need is:

1. The value of f at 0.
2. The function f at n + 1 given n and the value f n of f at n.

def fctrl : ℕ → ℕ

Equations

• fctrl t = Nat.rec 1 (fun (n fn : ℕ) => (n + 1) * fn) t

def fctrl' : ℕ → ℕ

Equations

• fctrl' = Nat.rec 1 fun (n fn : ℕ) => (n + 1) * fn

def stringFromNat (t : ℕ) : (fun (x : ℕ) => String) t

Equations

• stringFromNat = sorry

def even : ℕ → Bool

Equations

• even t = Nat.rec true (fun (n : ℕ) (p : Bool) => !p) t

When a function f is defined using Nat.rec, some definitional equalities are automatically generated. For example, the following is true by definition:

theorem fctrl_zero : fctrl 0 = 1

theorem fctrl_succ (n : ℕ) : fctrl (n + 1) = (n + 1) * fctrl n

We can write the definitional equalities in a general form.

theorem Nat.recFn_zero {α : Type u} (zeroData : α) (stepData : ℕ → α → α) : Nat.rec zeroData stepData 0 = zeroData

theorem Nat.recFn_succ {α : Type u} (zeroData : α) (stepData : ℕ → α → α) (n : ℕ) : Nat.rec zeroData stepData (n + 1) = stepData n (Nat.rec zeroData stepData n)

We see next recursive definitions of dependent functions. The motive is not constant in this case.

Concretely, we define:

• A family of types Tuple : ℕ → Type such that Tuple n is the type of n-tuples of natural numbers.
• The dependent function tuple : (n : ℕ) → Tuple (n + 1) such that tuple n is the n+1-tuple of natural numbers (n, ..., 1, 0).

def Tuple : ℕ → Type

Equations

• Tuple 0 = Unit
• Tuple n.succ = (ℕ × Tuple n)

theorem tuple1Type : Tuple 1 = (ℕ × Unit)

theorem tuple2Type : Tuple 2 = (ℕ × ℕ × Unit)

Note that × and → are right-associative. So, ℕ × ℕ × Unit is the same as ℕ × (ℕ × Unit).

theorem tuple2Type' : Tuple 2 = (ℕ × ℕ × Unit)

def tuple (n : ℕ) : Tuple (n + 1)

Equations

• tuple 0 = (0, ())
• tuple n.succ = (n + 1, tuple n)

def tuple' (n : ℕ) : Tuple (n + 1)

Equations

• tuple' t = Nat.rec (0, ()) (fun (n : ℕ) (tn : Tuple (n + 1)) => (n + 1, tn)) t

The recursive definition of tuple' satisfies the following definitional equalities.

theorem tuple'_zero : tuple' 0 = (0, ())

theorem tuple'_succ (n : ℕ) : tuple' (n + 1) = (n + 1, tuple' n)