证明反转=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”，

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

附言。我可以用一些例子来做到这一点，但我认为这不专业

Answer 1

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

Answer 2

就职。基本情况很简单。归纳步骤不应该太难。

Answer 3

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

证明草图：

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

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

归纳情况：
证明对于任何 n，rev 可以反转任何长度为 n 的列表，假设 rev 可以反转任何长度最多为 n-1 的列表

Answer 4

由于任何列表反转函数只能在给定有限列表的情况下产生任何输出，因此我们可以将此代码转换为 Coq（其中列表始终是有限的）并在那里证明所需的语句（忽略底部）。

这个证明不是我自己的 - 它是标准库中的证明的稍微修改版本。

Open Scope list_scope.

Require List.
Require Import FunctionalExtensionality.

Section equivalence.

  Variable A : Type.

  (* The reverse function is already defined in the standard library as List.rev. *)
  Notation reverse := (@List.rev A).

  Fixpoint aux (ys l2 : list A) :=
    match l2 with
      nil => ys
      | x :: xs => aux (x :: ys) xs
    end.

  Definition rev : list A -> list A
    := aux nil.

  Lemma aux_rev : forall l l', aux l' l = reverse l ++ l'.
  Proof.
    induction l; simpl; auto; intros.
    rewrite <- List.app_assoc; firstorder.
  Qed.

  Theorem both_equal : reverse = rev.
    extensionality xs.
    unfold rev.
    rewrite aux_rev.
    now rewrite List.app_nil_r.
  Qed.

End equivalence.