回到5-8年后的Coq检验:如何证明(forall n，m: N，(n - (S ))= pred(n - m))？

Question

大约在5到8年前(可能是6到7年)，我用Coq写了一篇完整的泡泡类型的形式化文章。最早证实的一个词是标题中的那个，我称之为"sub_succ_r“(或者它可能是标准名称？)：

forall n m : nat, (n - (S m))%nat = pred(n - m)

那时候，这是那个引理的一个非常简单的证明：

intros n m.
induction n m using n_double_ind.
simpl.
auto.
apply sub_0_r.
Qed.

"sub__r“是断言

forall n : nat, (n - 0)%nat = n

现在，同样熟悉现代Coq的细心读者可能已经发现了旧证据的问题:第二行。

induction n m

也就是说，在两个术语上同时进行归纳，不再起作用，甚至在指定使用"n_double_ind“的情况下也是如此。我一直在绞尽脑汁如何用第一次对n的归纳和对m的归纳来证明这一点，但我就是搞不明白。

任何帮助，无论大小，都将不胜感激。

Answer 1

如果要同时对两个变量应用归纳，则需要使用逗号分隔符，或者Coq将f t识别为应用于t的f，因此当您编写n m时，这实际上意味着n是一个函数，您希望将它应用于m。相反，使用逗号如下：

induction n, m.

这会产生四个子目标。其中两个可以用auto来证明，因此您可以要求Coq在归纳生成的每个子目标上使用自动策略，使用分号如下：

induction n, m; auto.

剩下的子目标很容易用你提到的引理和归纳假设来证明。因此，整个脚本如下：

Lemma sub_0_r : forall n : nat, (n - 0) = n.
Admitted.

Theorem sub_succ_r: forall n m : nat, (n - (S m)) = pred(n - m).
Proof.
  induction n, m; auto.
  - apply sub_0_r.
  - apply IHn.
Qed.

还请注意，使用%nat是不必要的。

但是正如你所看到的，我们只使用IHn，这意味着我们没有对m使用归纳假设，所以我们不需要在m上使用induction，只有destruct策略才能起作用，一个更好的证据是：

induction n; destruct m; auto.
- apply sub_0_r.
- apply IHn.

这是最小的和优雅的。