proof - 反转列表的两种方法的等效性

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.

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

标签： proofidris

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