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.

Published by Boro Sitnikovski