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 , and then prove the recursive step by assuming .

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 , and then prove the recursive step by assuming , where .

So as an example, let’s try to prove that .

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:

Inductive step: Assume that , and prove that .

.

Eta-reduction: .

Q.E.D.

Advertisements