The following proof is a solution to the exercise I offered to readers in the blog post [A Great Old-Timey Game-Programming Hack](http://blog.moertel.com/posts/2013-12-14-great-old-timey-game-programming-hack.html).

gistfile1.txt

Tom Moertel <[email protected]>
2013-12-14

The following proof is a solution to the exercise I offered to readers
in the following blog post:

"A Great Old-Timey Game-Programming Hack"
http://blog.moertel.com/posts/2013-12-14-great-old-timey-game-programming-hack.html


Problem:

We want to prove that

    (reverse . concat) xs == (concat . reverse . map reverse) xs

for all finite sequences of finite sequences xs.


Solution:

We proceed by structural induction over lists.  There are two cases
to consider, [] and (x:xs).

First, case [].  Here we show that the left- and right-hand sides of
the equation reduce to the same value:

  From the left-hand side:

    reverse (concat [])
  =   { defn concat }
    reverse []
  =   { defn reverse }
    [].

  From the right:

    concat (reverse (map reverse []))
  =   { defn map }
    concat (reverse [])
  =   { defn reverse }
    concat []
  =   { defn concat }
    [].

Next, case (x:xs).  This time we convert the left-hand side into the
right.

    reverse (concat (x:xs))
  =   { defn concat }
    reverse (x ++ concat xs)
  =   { claim 1, see below }
    reverse (concat xs) ++ reverse x
  =   { induction hypothesis }
    concat (reverse (map reverse xs)) ++ reverse x
  =   { defn concat }
    concat (reverse (map reverse xs) ++ [reverse x])
  =   { defn reverse }
    concat (reverse (map reverse xs) ++ reverse [reverse x])
  =   { claim 1, backward }
    concat (reverse ([reverse x] ++ map reverse xs))
  =   { defn ++ when applied to single-elem list }
    concat (reverse ((reverse x) : map reverse xs))
  =   { defn map }
    concat (reverse (map reverse (x:xs)).

To complete the proof, we must show that the following supporting
claim also holds:

    (Claim 1)

    reverse (xs ++ ys) == reverse ys ++ reverse xs.

This claim we prove by induction on xs.

First, case [].  As before, we show that the left- and right-hand
sides reduce to the same expression:

  From the left:

    reverse ([] ++ ys)
  =   { defn ++ }
    reverse ys.

  From the right:

    reverse ys ++ reverse []
  =   { defn reverse }
    reverse ys ++ []
  =   { defn ++ }
    reverse ys.

Finally, case (x:xs).  We show that the left hand side translates into
the right.

    reverse ((x:xs) ++ ys)
  =   { defn ++ }
    reverse (x:(xs ++ ys))
  =   { defn reverse }
    reverse (xs ++ ys) ++ [x]
  =   { induction hypothesis }
    (reverse ys ++ reverse xs) ++ [x]
  =   { ++ associative }
    reverse ys ++ (reverse xs ++ [x])
  =   { defn reverse, backward }
    reverse ys ++ reverse (x:xs).

This completes the proof of Claim 1 and, by its support, our original
claim, as well.


Bonus proof!  Having proved

    (reverse . concat) xs == (concat . reverse . map reverse) xs,

we have also proved that

    (reverse . concat) xs == (concat . map reverse . reverse) xs.

This follows immediately from reverse being a natural transformation,
allowing the order of (reverse) and (map reverse) to be swapped on the
right hand side.  That is,

    (map f . reverse) xs == (reverse . map f) xs.

for all functions f :: a -> b.

The reverse of a single element, is the element. If you have a list with one element, that element is the first (and last) element. Reversing the list, produces a list which has the same element as the first (and last) element. In other words, while [1 2] reversed is 2 1  [1] reversed is 1.