时间戳

首页 > 解决方案 > 证明两个 rev_append 实现的等价性

coq - 证明两个 rev_append 实现的等价性

问题描述

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

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

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？

标签： coqproofformal-verification

解决方案

您的定义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.

推荐阅读