逻辑：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

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

请注意，您要应用的归纳假设如何rev_append t [x]对某些固定的进行声明x，但在您的目标中，h在它妨碍之前的额外列表元素，并且归纳假设是没有用的。

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

正如 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策略（请参阅逻辑基础的策略章节）。