CODEWITHSUNDEEP
haskellinduction
Rumen Hristov
Rumen Hristov

Reputation: 887

Proving foldr f st (xs++ys) = f (foldr f st xs) (foldr f st ys)

I am trying to prove the following statement by structural induction:

foldr f st (xs++yx) = f (foldr f st xs) (foldr f st ys)        (foldr.3)

However I am not even sure how to define foldr, so I am stuck as no definitions have been provided to me. I now believe that foldr can be defined as

foldr f st [] = st                                             (foldr.1)
foldr f st x:xs = f x (foldr f st xs)                          (foldr.2)

Now I want to start working on the base case passing the empty list to foldr. I have this, but I don't think it is correct.

foldr f st ([]++[]) = f (foldr f st []) (foldr f st [])
LHS:
    foldr f st ([]++[]) = foldr f st []                        by (++)
    foldr f st [] = st                                         by (foldr.1)
RHS:
    f (foldr f st []) (foldr f st []) = f st st                by (foldr.1)
    = st                                                       by definition of identity, st = 0

LHS = RHS, therefore base case holds

Now this is what I have for my inductive step:

Assume that:
  foldr f st (xs ++ ys) = f (foldr f st xs) (foldr f st ys)        (ind. hyp)

Show that:
  foldr f st (x:xs ++ ys) = f (foldr f st x:xs) (foldr f st ys)    (inductive step)

LHS:
    foldr f st (x:xs ++ ys) = f x (foldr f st xs) (foldr f st ys)  (by foldr.2)
RHS:
    f (foldr f st x:xs) (foldr f st ys) = 
  = f f x (foldr f st xs) (foldr f st ys)                          (by foldr.2)
  = f x (foldr f st xs) (foldr f st ys)

LHS = RHS, therefore inductive step holds. End of proof.

I am not sure if this proof is valid. I need some help in determining if it correct and if not - what part of it is not.

Upvotes: 2

Views: 301

Answers (1)

Christian Conkle
Christian Conkle

Reputation: 5992

First: you can find the definition for many basic Haskell functions via the API documentation, which is available on Hackage. The documentation for base is here. foldr is exported in Prelude, which has a link to its source code:

foldr :: (a -> b -> b) -> b -> [a] -> b
foldr k z = go
          where
            go []     = z
            go (y:ys) = y `k` go ys

It's defined like this for efficiency reasons; look up "worker-wrapper." It's equivalent to

foldr f st [] = st
foldr f st (y:ys) = f y (foldr f st ys)

Second: In your desired proof, the type of f must be a -> a -> a, which is less general than a -> b -> b.

Let's work through the base case (xs = ys = []).

foldr f st ([]++[]) = f (foldr f st []) (foldr f st [])
-- Definition of ++
foldr f st []       = f (foldr f st []) (foldr f st [])
-- Equation 1 of foldr
st                  = f st              st

This equation does not hold in general. To proceed with the proof, you'll have to assume that st is an identity for f.

You'll also have to assume, in the non-base case, that f is associative, I believe. These two assumptions, combined, indicate that f and st form a monoid. Are you trying to prove something about foldMap?

Upvotes: 2

Related Questions