证明reverse=rev

Question

我有一些任务要做，但不知道怎么做：

reverse, rev :: [a] [a]

reverse [] = []
reverse (x:xs) = reverse xs ++ [x]

rev = aux [] where
    aux ys [] = ys
    aux ys (x:xs) = aux (x:ys) xs

“证明: reverse=rev”

您的帮助我们将不胜感激。谢谢。

PS。我可以用一些例子来做，但我认为那不专业。

Answer 1

我不会尝试直接证明等价性，而是(使用归纳)为每个函数证明它实际上颠倒了列表。如果它们都是反向列表，那么它们是等价的。

验证草图：

我们想要证明rev适用于所有列表：

长度为0的基本情况列表:证明rev []计算正确

归纳情形：证明对于任何n，rev可以颠倒任何长度为n的列表，假设rev可以颠倒任何长度为n-1的列表

Answer 2

你可以通过结构归纳来做一个草率的证明，但是如果你想要一个正确地处理底部的证明，它就不那么简单了。

Answer 3

归纳。基本情况是微不足道的。归纳的步骤应该不会太难。