两种反转列表的方法的等价性

Question

假设我有两个不同的函数来反转列表：

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 []

现在我想证明这些函数确实做同样的事情。这是我提出的证明：

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

这个偶数类型检查并且是总的（尽管相互递归）：

*Reverse> :total revsEq
Reverse.revsEq is Total

请注意 lemma1 实际上是 lemma2 的更强版本，但我似乎需要 lemma2 因为它简化了 lemma1.[=17 中的递归情况=]

问题是：我能做得更好吗？具有大量重写的相互递归引理似乎过于不透明。

Answer 1

如果你对一个使revOnto的累加器保持显式的函数进行递归，证明可以很短：

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

两种反转列表的方法的等价性

Equivalence of two ways of reversing a list

proof

idris