在逻辑章节中，介绍了反向列表函数的尾递归版本。我们需要证明它可以正确工作：
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]
接下来做什么？
正如您在尝试证明期间注意到的那样，当从rev_append l [x] to rev_append (h :: t) [x]，你最终会得到这个词rev_append t [h; x]简化后。归纳步骤不会导致基本情况rev_append函数，而是另一个无法简化的递归调用。
请注意您想要应用的归纳假设如何陈述rev_append t [x]对于一些固定的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策略（参见Tactics https://softwarefoundations.cis.upenn.edu/lf-current/Tactics.html的章节逻辑基础).
本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)
