证明了两个rev_append实现的等价性

Question

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

我试图在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仍然不适用。

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

Answer 1

您的定义具有随归纳而变化的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.