Structural induction

Let’s try to prove that map id = id.

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

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

id x = x

Base case:
map id [] = [] = id []

Inductive step:
Assume that map id xs = id xs

Prove that map id (x:xs) = id (x:xs)

map id (x:xs) = id x : map id xs = by induction = id x : id xs = x : xs = id (x : xs)

Eta-reduction: map id = id Q.E.D.

Advertisements

Leave a Reply

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

WordPress.com Logo

You are commenting using your WordPress.com 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 )

Google+ photo

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

Connecting to %s