逻辑：tr_rev_correct 的辅助引理

Question

逻辑章节介绍了反向列表函数的尾递归版本。我们需要证明它能正常工作：

Fixpoint rev_append {X} (l1 l2 : list X) : list X :=
  match l1 with
  | [] => l2
  | x :: l1' => rev_append l1' (x :: l2)
  end.

(* Tail recursion rev *)
Definition tr_rev {X} (l : list X) : list X :=
  rev_append l [].

但在证明之前我想证明一个引理：

Lemma rev_append_app: forall (X: Type) (x: X) (l : list X),
    rev_append l [x] = rev_append l [] ++ [x].
Proof.
  intros X x l. induction l as [| h t IH].
  - simpl. reflexivity.
  - simpl.

我卡在这里了：

X : Type
x, h : X
t : list X
IH : rev_append t [x] = rev_append t [ ] ++ [x]
============================
rev_append t [h; x] = rev_append t [h] ++ [x]

下一步做什么？

Answer 1

可以看出，归纳假设IH不足以证明目标。这里你需要的是首先要证明的更一般的陈述。您可以找到更多专门针对该主题的练习 here。（其实尾递归逆向也是练习之一。）

对于您的情况，完全概括的陈述可以如下：

Lemma rev_append_app': forall (X: Type) (l l1 l2 : list X),
    rev_append l (l1 ++ l2) = rev_append l l1 ++ l2.

用归纳法证明这一点很简单。然后你可以证明你自己的说法是这个的推论：

Corollary rev_append_app: forall (X: Type) (x: X) (l : list X),
    rev_append l [x] = rev_append l [] ++ [x].
Proof. intros. apply (rev_append_app _ _ [] [x]). Qed.

Answer 2

正如您在尝试证明过程中注意到的那样，当从 rev_append l [x] 到 rev_append (h :: t) [x] 进行归纳步骤时，您在简化后得到项 rev_append t [h; x]。归纳步骤不会导致 rev_append 函数的基本情况，而是导致无法简化的另一个递归调用。

请注意您想要应用的归纳假设如何针对某些固定的 x 做出关于 rev_append t [x] 的陈述，但在您的目标中，它之前的额外 h 列表元素碍事，归纳假设也没用

这就是 Bubbler 的回答在指出您的归纳假设不够强大时所指的内容：它只说明了第二个参数是具有 单个[=36 的列表的情况=] 元素。但即使在归纳步骤（一个递归应用程序）之后，该列表也已经至少有两个元素！

正如Bubbler所建议的那样，辅助引理rev_append l (l1 ++ l2) = rev_append l l1 ++ l2更强并且没有这个问题：当用作归纳假设时，它也可以应用于rev_append t [h; x]，让你用 rev_append t [h] ++ [x].
证明相等
当试图证明辅助引理时，您可能会像证明 rev_append_app 本身一样陷入困境（就像我一样）。帮助我继续进行的关键建议是 在开始归纳 之前要小心引入哪些普遍量化的变量。如果过早地专门化其中任何一个，您可能会削弱归纳假设并再次陷入困境。您可能需要更改这些量化变量的顺序或使用 generalize dependent 策略（请参阅 逻辑基础 的 Tactics 章节）。

Answer 3

像这样使用泛化依赖策略：

Lemma rev_append_app: forall (X: Type) (l l1: list X) (x : X),
    rev_append l (l1 ++ [x]) = rev_append l l1 ++ [x].
  intros.
  generalize dependent l1.
  induction l as [| h t IH].
  - intros.
    easy.
  - intros.
    apply (IH (h::l1)).
Qed.

逻辑：tr_rev_correct 的辅助引理

Logic: auxilliry lemma for tr_rev_correct

coq

logical-foundations