《软件基础》卷1Logic章节：如何证明tr_rev与rev等价？

你遇到的阻碍本质是归纳假设的泛化程度不足，当前的归纳命题仅覆盖了rev_append第二个参数为空列表的情况，无法适配归纳步中出现的第二个参数为[x]的场景，需要先证明一个更通用的辅助引理来打通rev_append和标准rev+列表拼接的关系。

具体解题步骤 #

1. 先证明通用辅助引理，建立rev_append的通用性质

Lemma rev_append_general : forall X (l1 l2 : list X),
  rev_append l1 l2 = rev l1 ++ l2.
Proof.
  intros X l1 l2.
  induction l1 as [| x l1' IH].
  - simpl. apply app_nil_l. (* 基例直接用空列表左拼接引理即可 *)
  - simpl. rewrite IH. rewrite app_assoc. reflexivity.
Qed.

这里用到的app_assoc是列表拼接的结合律，属于Coq列表标准库的基础引理，你也可以自行通过归纳证明，逻辑非常简单。

2. 用辅助引理直接完成原定理证明，不需要沿用你走到一半的归纳路径就能快速得证：

Theorem tr_rev_correct : forall X, @tr_rev X = @rev X.
Proof.
  intros X.
  apply functional_extensionality.
  intros l.
  unfold tr_rev.
  rewrite rev_append_general.
  apply app_nil_r. (* 空列表右拼接引理：任何列表拼接空列表等于自身 *)
Qed.

如果你一定要沿着你之前的证明路径走，在你卡住的目标下，直接对目标应用rev_append_general就可以将等式两边都转化为拼接形式：

rev l' ++ [x] = (rev l' ++ []) ++ [x]

接下来只需要用app_nil_r把rev l' ++ []简化为rev l'，等式两边就完全相等了。

内容的提问来源于stack exchange，提问作者Felipe Balbi