# Structural induction

Structural induction is a generalization of mathematical induction.

To see how, consider the definition of naturals (which mathematical induction is based on):

Inductive nat : Set :=
| O => nat
| S => nat -> nat.

So, generally what we do is prove the base case $P(O)$, and then prove the recursive step $P(S (S n))$ by assuming $P(n)$.

Structural induction can be applied more generally, say lists.

Inductive natlist : Set :=
| nil  => natlist
| cons => nat -> natlist -> natlist.

In this case we prove the base case $P(nil)$, and then prove the recursive step $P(l')$ by assuming $P(l)$, where $l' = cons(x, l)$.

So as an example, let’s try to prove that $map(id) = id$.

First, let’s look at the definitions for map and id:

map _ []     = []
map f (x:xs) = f x : map f xs
id x         = x

We use induction on x.

Base case: $map(id, []) = [] = id([])$

Inductive step: Assume that $map(id, xs) = id(xs)$, and prove that $map(id, (x:xs)) = id(x:xs)$.

$map(id, (x:xs)) = id(x) : map(id, xs) = I.H. = id(x) : id(xs) = x : xs = id(x : xs)$.

Eta-reduction: $map(id) = id$.

Q.E.D.