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.



Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Google+ photo

You are commenting using your Google+ account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )


Connecting to %s