Given:
data Nat = Zero | Succ Nat
data List a = Nil | Cons a (List a)
length Nil = Zero
length (Cons x xs) = Succ (length xs)
map f Nil = Nil
map f (Cons x xs) = Cons (f x) (map f xs)
prove that:
length (map f xs) = length xs
Proof by induction on structure of xs :: List a
case xs = Nil:
length (map f Nil) = length Nil
length Nil = length Nil
QED { ... }
case xs = Cons y ys:
Assume: length (map f ys) = length ys
length (map f (Cons y ys)) = length (Cons y ys)
length (Cons (f y) (map f ys)) = ...
Succ (length (map f ys)) = length (Cons y ys)
Succ (length (map f ys)) = Succ (length ys)
length (map f ys) = length ys
QED