证明关于列表最后一个元素的定理

Question

我有两个函数

build_goal_aux

和

last

定义如下：

Fixpoint build_goal_aux (acc:list nat)(n:nat) : list nat :=
  match n with
  | O => acc
  | S n' => build_goal_aux (n::acc) n'
  end.
Fixpoint last (l:list nat) : option nat :=
  match l with
    | [] => None
    | a :: [] => Some a
    | _ :: l => last l
  end.

我想证明一些关于

build_goal_aux

的定理，例如：

Lemma build_goal_aux_last : forall n e, last (build_goal_aux [e] n) = Some e.
Lemma build_goal_aux_never_nil : forall (n:nat), build_goal_aux [0] n <> [].

但我不知道该怎么做。我尝试了对

n

的归纳，但我不知道如何完成证明。我仍然想尝试自己证明这一点，所以我不想要一个完整的解决方案，但一些线索就很好了。

Answer 1

你的两个引理都太具体了。让我们看看当我们尝试进行归纳时会发生什么：

Lemma build_goal_aux_last : forall n e, last (build_goal_aux [e] n) = Some e.
Proof.
  intros n.
  induction n.
  - easy.
  - intros e.
    simpl.
    (*
      n : nat
      IHn : forall e : nat, last (build_goal_aux [e] n) = Some e
      e : nat
      ============================
      last (build_goal_aux [S n; e] n) = Some e
    *)
Abort.

我们看到我们的归纳假设谈论的是

build_goal_aux [e] n

，而我们的目标谈论的是

build_goal_aux [S n; e] n

，所以归纳假设不可能有用。出路是概括引理，使其适用于给定

build_goal_aux

的每个列表，然后导出您想要的结果作为推论。

引理试图表达什么？只要

aux

列表非空，

build_goal_aux aux n

的最后一个元素就已经是预先确定的，无论

n

是什么。一种写法是：

Lemma build_goal_aux_last : forall n e w,
  last (build_goal_aux (e :: w) n) = last (e :: w).

（请注意，我选择将“

aux

非空”实现为

e :: w

而不是

aux <> []

，这最终是一个设计选择。我更喜欢这个版本，但YMMV。）

现在归纳假设实际上是有用的，你原来的引理显然是一个推论。

你的第二个引理的问题是相同的，并且有类似的解决方案。

当你有一个递减的递归定义（在本例中为

nat

）修改函数的某些其他参数（

list nat

）时，这种概括引理以使其可通过归纳法证明的模式会经常出现。在这种情况下）。为了获得足够强的归纳假设，您通常需要在非递减论证中完全通用的陈述。