Search code examples
haskellequivalentproof

Prove that reverse=rev

I have some task to do, but don't know how to do it:

reverse, rev :: [a] [a]

reverse [] = []
reverse (x:xs) = reverse xs ++ [x]

rev = aux [] where
    aux ys [] = ys
    aux ys (x:xs) = aux (x:ys) xs

"Prove that : reverse=rev"

Your help would be appreciated. Thank you.

PS. I can do it using some example but i think thats not professional

Solution

  • Instead of trying to prove equivalence directly, I would for each function prove (using induction) that it actually reverses the list. If both of them reverse lists, then they are equivalent.

    Proof sketch:

    We want to prove that rev works for all lists:

    base case lists of length 0: prove that rev [] computes correctly

    inductive case: prove that for any n, rev can reverses any list of length n, assuming rev can reverse any list of length up to n-1