证明两个 rev_append 实现的等效性

问题描述

免责声明：这不是家庭作业问题。

我正在尝试在 Coq 中实现我自己的 rev_append 版本，然后证明它与内置版本等效。以下是我的实现。

Fixpoint my_rev_append (l1 l2 : list nat) : (list nat) * (list nat) :=
  match l1 with
  | nil => (l1,l2)
  | hd :: tl => my_rev_append tl (hd :: l2)
  end.

然后我试图证明它等价于rev_append

Theorem my_rev_append_correct : forall (l1 l2 : list nat),my_rev_append l1 l2 = (nil,(rev_append l1 l2)).
Proof.
  intros l1 l2.
  induction l1.
  reflexivity.

然后我达到了以下目标，我看不到前进的道路。

  IHl1 : my_rev_append l1 l2 = (nil,rev_append l1 l2)
  ============================
  my_rev_append (a :: l1) l2 = (nil,rev_append (a :: l1) l2)

不能使用IHl1，因为当前子目标的RHS是(nil,rev_append (a :: l1) l2)，不包含(nil,rev_append l1 l2)。我尝试对其运行 simpl 策略，但没有奏效，因为 IHl1 仍然不适用。

我完全明白我可以通过将 | nil => (l1,l2) 中的 my_rev_append 行更改为 | nil => l2 来证明这一点。然而，是否有可能在不改变 my_rev_append 的定义的情况下证明这个定理？

解决方法

你的定义有 l2 通过归纳而变化。因此，定理的证明也应该有 l2 通过归纳而变化。为此，在开始归纳之前不要intro归纳l2，将其留在目标中。归纳假设的类型以该目标为模型，然后允许您在递归情况下为其传递不同的值。

Theorem my_rev_append_correct : forall (l1 l2 : list nat),my_rev_append l1 l2 = (nil,rev_append l1 l2).
Proof.
  induction l1 as [ | x l1 rec]; intros l2.
  - reflexivity.
  - apply rec.
Qed.

coq formal-verification proof