SF 第 1 卷：逻辑：如何证明 tr_rev <-> rev？

Question

从软件基础第 1 卷的逻辑一章中，我们看到了列表反转的尾递归定义。它是这样的：

Fixpoint rev_append {X} (l1 l2 : list X) : list X :=
  match l1 with
  | [] => l2
  | x :: l1' => rev_append l1' (x :: l2)
  end.

Definition tr_rev {X} (l : list X) : list X :=
  rev_append l [].

然后，我们被要求证明 tr_rev 和 rev 的等价性，很明显它们是相同的。不过，我很难完成入职培训。如果社区能就如何处理此案例提供任何提示，我们将不胜感激。

据我所知：

Theorem tr_rev_correct : forall X, @tr_rev X = @rev X.
Proof.
  intros X. (* Introduce the type *)
  apply functional_extensionality. (* Apply extensionality axiom *)
  intros l. (* Introduce the list *)
  induction l as [| x l']. (* start induction on the list *)
  - reflexivity. (* base case for the empty list is trivial *)
  - unfold tr_rev. (* inductive case seems simple too. We unfold the definition *)
    simpl. (* simplify it *)
    unfold tr_rev in IHl'. (* unfold definition in the Hypothesis *)
    rewrite <- IHl'. (* rewrite based on the hypothesis *)

至此，我有了这组假设和目标：

  X : Type
  x : X
  l' : list X
  IHl' : rev_append l' [ ] = rev l'
  ============================
  rev_append l' [x] = rev_append l' [ ] ++ [x]

现在，[] ++ [x] 显然与 [x] 相同，但 simpl 无法简化它，我无法想出一个 Lemma 来帮助我在这。我确实证明了app_nil_l（即forall (X : Type) (x : X) (l : list X), [] ++ [x] = [x].）但是当我尝试用app_nil_l重写时它会重写等式的两边。

我可以将其定义为公理，但我觉得那是作弊:-p

谢谢

Answer 1

用累加器证明有关定义的事情有一个特定的技巧。问题是，关于 tr_rev 的事实必然是关于 rev_append 的事实，但是 rev_append 定义在两个列表上，而 tr_rev 只定义在一个列表上。 rev_append 的计算依赖于这两个列表，因此归纳假设需要足够普遍以包含这两个列表。但是，如果您将 rev_append 的第二个输入固定为始终为空列表（您通过仅对 tr_rev 声明结果来隐含地做到这一点），那么归纳假设将始终太弱。

解决这个问题的方法是首先通过对 l1 的归纳（并在 l2 上进行归纳）来证明 rev_append 的一般结果，然后将这个结果专门用于tr_rev.

SF 第 1 卷：逻辑：如何证明 tr_rev <-> rev？

SF Volume 1: Logic: How to prove tr_rev <-> rev?

coq

proof-general

proof-of-correctness

coq-tactic