CODEWITHSUNDEEP
proofidris
0xd34df00d
0xd34df00d

Reputation: 1505

Equivalence of two ways of reversing a list

Let's say I have two different functions that reverse a list:

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

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

revAcc : List a -> List a
revAcc = revOnto []

and now I want to prove that these functions indeed do the same thing. This is the proof that I came up with:

mutual
  lemma1 : (acc, lst : List a) -> revOnto acc lst = revOnto [] lst ++ acc
  lemma1 acc [] = Refl
  lemma1 lst (y :: ys) = let rec1 = lemma1 (y :: lst) ys
                             rec2 = lemma2 y ys in
                         rewrite rec1 in
                         rewrite rec2 in
                         rewrite appendAssociative (revOnto [] ys) [y] lst in Refl

  lemma2 : (x0 : a) -> (xs : List a) -> revOnto [x0] xs = revOnto [] xs ++ [x0]
  lemma2 x0 [] = Refl
  lemma2 x0 (x :: xs) = let rec1 = lemma2 x xs
                            rec2 = lemma1 [x, x0] xs in
                        rewrite rec1 in
                        rewrite sym $ appendAssociative (revOnto [] xs) [x] [x0] in rec2

revsEq : (xs : List a) -> revAcc xs = revDumb xs
revsEq [] = Refl
revsEq (x :: xs) = let rec = revsEq xs in
                   rewrite sym rec in lemma2 x xs

This even type checks and is total (despite the mutual recursion):

*Reverse> :total revsEq
Reverse.revsEq is Total

Note that lemma1 is effectively a stronger version of the lemma2, yet I seemingly need lemma2 since it simplifies the recursive case in lemma1.

The question is: can I do any better? Mutually recursive lemmas with lots of rewrites seem to be overly opaque.

Upvotes: 1

Views: 321

Answers (1)

xash
xash

Reputation: 3722

If you do the recursion on a function that keeps revOnto's accumulator explicit, the proof can be quite short:

lemma1 : (acc, xs : List a) -> revOnto acc xs = revDumb xs ++ acc
lemma1 acc [] = Refl
lemma1 acc (y :: xs) =
    rewrite lemma1 (y :: acc) xs in
    appendAssociative (revDumb xs) [y] acc

revsEq : (xs : List a) -> revAcc xs = revDumb xs
revsEq [] = Refl
revsEq (x :: xs) = lemma1 [x] xs

Upvotes: 1

Related Questions