Structural induction in Haskell

haskell, induction

Solution

You did not specify it, but I will assume `::` means list concatention and use `++`, since that is the operator used in Haskell. To prove this, we will perform induction on `xs`. First, we show that the statement holds for the base case (i.e. `xs = []`)

foldr f a (xs ++ ys) 
{- By definition of xs -}
= foldr f a ([] ++ ys)
{- By definition of ++ -}
= foldr f a ys

and

foldr f (foldr f a ys) xs
{- By definition of xs -}
= foldr f (foldr f a ys) []
{- By definition of foldr -}
= foldr f a ys

Now, we assume that the induction hypothesis `foldr f a (xs ++ ys) = foldr f (foldr f a ys) xs` holds for `xs` and show that it will hold for the list `x:xs` as well.

foldr f a (x:xs ++ ys)
{- By definition of ++ -}
= foldr f a (x:(xs ++ ys))
{- By definition of foldr -}
= x `f` foldr f a (xs ++ ys)
         ^------------------ call this k1
= x `f` k1

and

foldr f (foldr f a ys) (x:xs)
{- By definition of foldr -}
= x `f` foldr f (foldr f a ys) xs
         ^----------------------- call this k2
= x `f` k2

Now, by our induction hypothesis, we know that `k1` and `k2` are equal, therefore

x `f` k1 =  x `f` k2

Thus proving our hypothesis.

Problem

Original source