reverse - Agda - 反向助手

Question

我试图证明这个引理

reverse-++ : ∀{ℓ}{A : Set ℓ}(l1 l2 :  A) → reverse (l1 ++ l2) ≡ (reverse l2) ++ (reverse l1)     
reverse-++ [] [] = refl
reverse-++ l1  [] rewrite ++[] l1 = refl
reverse-++ l1 (x :: xs) =  {!!}

但是另一个功能 reverse-helper 不断出现在我的目标中，我不知道如何摆脱它。有什么指导或建议吗？

Answer 1

我假设在 的实现中reverse，您调用reverse-helper. 在这种情况下，您可能想要证明一个引理reverse-helper，您可以在引理 about 中调用它reverse。这是一个普遍的事情：如果你用辅助函数来证明某个函数，你通常需要一个带辅助证明的证明，因为证明的归纳结构通常与函数的递归结构相匹配。

Answer 2

我认为你应该从不同的论点开始。

因为++可能用 定义[] ++ a = a，reverse (x :: xs) = (reverse xs) ++ (x :: nil)最好证明reverse-++ (x :: xs) ys = cong (\xs -> xs ++ (x :: nil)) (reverse-++ xs ys)