3

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

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]

接下来做什么？

4

3 回答 3

5

正如您在尝试证明期间注意到的那样，当从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策略（请参阅逻辑基础的策略章节）。

于 2019-08-07T19:52:41.733 回答
2

您可以看到归纳假设IH不足以证明目标。在这里，您首先需要一个更一般的陈述来证明。您可以在此处找到更多专门针对此主题的练习。（实际上，尾递归反向是练习之一。）

在您的情况下，完全概括的陈述可能如下：

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.
于 2019-05-05T22:43:53.677 回答
0

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

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.
于 2019-08-22T05:06:35.093 回答