Append ist assoziativ

data List a = Nil | Cons a ( List a ) 
    deriving (Show, Eq)
append :: List a -> List a -> List a 
append xs ys = case xs of
    Nil        -> ys
    Cons x xs' -> Cons x ( append xs' ys )

Behauptung:

forall a :: Type, forall xs, ys, zs :: List a
  append xs (append ys zs) 
    == append (append xs ys) zs

Beweis:

Fall 1: xs = Nil (Induktionsanfang) Fall 2: xs = Cons x xs' (Induktionsschritt)

Fall 1: xs = Nil (Induktionsanfang)

append Nil (append ys zs) 
   =?= append (append Nil ys) zs
(append ys zs) =?= append (append Nil ys) zs
(append ys zs) =?= append      ys zs

Terme sind identisch

Fall 2: xs = Cons x xs' (Induktionsschritt)

append (Cons x xs') (append ys zs) 
   =?= append (append (Cons x xs') ys) zs
Cons x (append xs' (append ys zs))
   =?= append (Cons x (append xs' ys)) zs
Cons x (append xs' (append ys zs))
   =?= Cons x (append (append xs' ys) zs)

Teilterme sind äquivalent nach Induktionsannahme