## Tuesday, May 16, 2017

### Idris reverse proofs

Summary: I proved O(n) reverse is equivalent to O(n^2) reverse.

Following on from my previous post I left the goal of given two `reverse` implementations:

``````reverse1 : List a -> List a
reverse1 [] = []
reverse1 (x :: xs) = reverse1 xs ++ [x]

rev2 : List a -> List a -> List a
rev2 acc [] = acc
rev2 acc (x :: xs) = rev2 (x :: acc) xs

reverse2 : List a -> List a
reverse2 = rev2 []
``````

Proving the following laws hold:

``````proof_reverse1_reverse1 : (xs : List a) -> xs = reverse1 (reverse1 xs)
proof_reverse2_reverse2 : (xs : List a) -> xs = reverse2 (reverse2 xs)
proof_reverse1_reverse2 : (xs : List a) -> reverse1 xs = reverse2 xs
``````

The complete proofs are available in my Idris github repo, and if you want to get the most out of the code, it's probably best to step through the types in Idris. In this post I'll talk through a few of the details.

Directly proving the `reverse1 (reverse1 x) = x` by induction is hard, since the function doesn't really follow so directly. Instead we need to define a helper lemma.

``````proof_reverse1_append : (xs : List a) -> (ys : List a) ->
reverse1 (xs ++ ys) = reverse1 ys ++ reverse1 xs
``````

Coming up with these helper lemmas is the magic of writing proofs - and is part intuition, part thinking about what might be useful and part thinking about what invariants are obeyed. With that lemma, you can prove by induction on the first argument (which is the obvious one to chose since `++` evaluates the first argument first). Proving the base case is trivial:

``````proof_reverse1_append [] ys =
rewrite appendNilRightNeutral (reverse1 ys) in
Refl
``````

The proof immediately reduces to `reverse1 ys == reverse1 ys ++ []` and we can invoke the standard proof that if `++` has `[]` on the right we can ignore it. After applying that rewrite, we're straight back to `Refl`.

The `::` is not really any harder, we immediately get to `reverse1 ys ++ (reverse1 xs ++ [x])`, but bracketed the wrong way round, so have to apply `appendAssociative` to rebracket so it fits the inductive lemma. The proof looks like:

``````proof_reverse1_append (x :: xs) ys =
rewrite appendAssociative (reverse1 ys) (reverse1 xs) [x] in
rewrite proof_reverse1_append xs ys in Refl
``````

Once we have the proof of how to move `reverse1` over `++` we use it inductively to prove the original lemma:

``````proof_reverse1_reverse1 : (xs : List a) -> xs = reverse1 (reverse1 xs)
proof_reverse1_reverse1 [] = Refl
proof_reverse1_reverse1 (x :: xs) =
rewrite proof_reverse1_append (reverse1 xs) [x] in
rewrite proof_reverse1_reverse1 xs in
Refl
``````

For the remaining two proofs, I first decided to prove `reverse1 x = reverse2 x` and then prove the `reverse2 (reverse2 x) = x` in terms of that. To prove equivalence of the two functions I first needed information about the fundamental property that `rev2` obeys:

``````proof_rev : (xs : List a) -> (ys : List a) ->
rev2 xs ys = reverse2 ys ++ xs
``````

Namely that the accumulator can be tacked on the end. The proof itself isn't very complicated, although it does require two calls to the inductive hypothesis (you basically expand out `rev2` on both sides and show they are equivalent):

``````proof_rev xs [] = Refl
proof_rev xs (y :: ys) =
rewrite proof_rev [y] ys in
rewrite sym \$ appendAssociative (rev2 [] ys) [y] xs in
rewrite proof_rev (y :: xs) ys in
Refl
``````

The only slight complexity is that I needed to apply `sym` to switch the way the `appendAssocative` proof is applied. With that proof available, proving equivalence isn't that hard:

``````proof_reverse1_reverse2 : (xs : List a) -> reverse1 xs = reverse2 xs
proof_reverse1_reverse2 [] = Refl
proof_reverse1_reverse2 (x :: xs) =
rewrite proof_rev [x] xs in
rewrite proof_reverse1_reverse2 xs in
Refl
``````

In essence the `proof_rev` term shows that `rev` behaves like the O(n^2) reverse.

Finally, actually proving that `reverse2 (reverse2 x)` is true just involves replacing all the occurrences of `reverse2` with `reverse1`, then applying the proof that the property holds for `reverse1`. Nothing complicated at all:

``````proof_reverse2_reverse2 : (xs : List a) -> xs = reverse2 (reverse2 xs)
proof_reverse2_reverse2 xs =
rewrite sym \$ proof_reverse1_reverse2 xs in
rewrite sym \$ proof_reverse1_reverse2 (reverse1 xs) in
rewrite proof_reverse1_reverse1 xs in
Refl
``````

If you've got this far and are still hungry for more proof exercises I recommend Exercises on Generalizing the Induction Hypothesis which I have now worked through (solutions if you want to cheat).