Given:
data Nat = Zero | Succ Nat
data List a = Nil | Cons a (List a)
add Zero m = m
add (Succ n) m = Succ (add n m)
length Nil = Zero
length (Cons x xs) = Succ (length xs)
append Nil ys = ys
append (Cons x xs) ys = Cons x (append xs ys)
prove that:
length (append as bs) = add (length as) (length bs)
Proof by induction on structure of as :: List a
case as = Nil:
length (append Nil bs) = add (length Nil) (length bs)
length bs = add (length Nil) (length bs)
length bs = add Zero (length bs)
length bs = length bs
QED { ... }
case as = Cons c cs:
Assume: length (append cs bs) = add (length cs) (length bs)
Prove: length (append (Cons c cs) bs) = add (length (Cons c cs)) (length bs)
length (Cons c (append cs bs)) = ...
Succ (length (append cs bs)) = ...
... = add (length (Cons c cs)) (length bs)
... = add (Succ (length cs)) (length bs)
Succ (length (append cs bs)) = Succ (add (length cs) (length bs))
length (append cs bs) = add (length cs) (length bs)
QED