逻辑：tr_rev_correct 的辅助引理答案

【问题标题】：Logic: auxilliry lemma for tr_rev_correct逻辑：tr_rev_correct 的辅助引理
【发布时间】：2019-05-05 12:27:01
【问题描述】：

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

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]

接下来要做什么？

【问题讨论】：

简短的回答是，这个引理并不比原始引理更容易证明。
@Li-yaoXia 请给点提示。

标签： coq logical-foundations

【解决方案1】：

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

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

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

正如 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 策略（参见Logic Foundations 的Tactics 章节）。

【讨论】：

【解决方案2】：

您可以看到归纳假设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.

【讨论】：

【解决方案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.

【讨论】：