1

从软件基础第 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

谢谢

4

1 回答 1

1

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

解决这个问题的方法是首先通过对rev_append的归纳l1（和对 的概括l2）证明 的一般结果，然后将这个结果专门用于 的情况tr_rev。

于 2021-09-28T13:36:31.890 回答