Given:
data List a = Nil | Cons a (List a)
map f Nil = Nil
map f (Cons x xs) = Cons (f x) (map f xs)
(f . g) x = f ( g x)
prove that:
map (f . g) = map f . map g
That is: for all xs :: List a,
map (f . g) xs = (map f . map g) xs { by function equality }
Proof by induction on structure of xs :: List a
case xs = Nil:
map (f . g) Nil = (map f . map g) Nil
Nil = ...
Nil = (map f . map g) Nil
Nil = map f (map g Nil)
Nil = map f Nil
Nil = Nil
QED { ... }
case xs = Cons y ys:
Assume: map (f . g) ys = (map f . map g) ys
Prove: map (f . g) (Cons y ys) = (map f . map g) (Cons y ys)
Cons ((f . g) y) (map (f . g) ys) = ...
Cons (f (g y)) (map (f . g) ys) = ...
Cons (f (g y)) (map (f . g) ys) = (map f . map g) (Cons y ys)
Cons (f (g y)) (map (f . g) ys) = map f (map g (Cons y ys))
Cons (f (g y)) (map (f . g) ys) = map f (Cons (g y) (map g ys))
Cons (f (g y)) (map (f . g) ys) = Cons (f (g y)) (map f (map g ys))
map (f . g) ys = map f (map g ys)
map (f . g) ys = (map f . map g) ys
QED