coq - 逻辑 : auxilliry lemma for 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策略(请参阅逻辑基础的 Tactics 一章)。