我可以告诉 Coq 从 n 到 n+2 进行归纳吗？

Question

我想看看是否有可能在不涉及奇数的情况下从https://softwarefoundations.cis.upenn.edu/lf-current/Logic.html 证明evenb n = true <-> exists k, n = double k。我尝试了类似以下的方法：

Theorem evenb_double_k : forall n,
  evenb n = true -> exists k, n = double k.
Proof.
  intros n H. induction n as [|n' IHn'].
  - exists 0. reflexivity.
  - (* stuck *)

但显然归纳法一次只对一个自然数起作用，exists k : nat, S n' = double k 显然无法证明。

n' : nat
H : evenb (S n') = true
IHn' : evenb n' = true -> exists k : nat, n' = double k
______________________________________(1/1)
exists k : nat, S n' = double k

有没有办法让归纳从 n 到 n+2？

Answer 1

有一种策略叫做fix。我将尝试在高层次上解释正在发生的事情，因为我认为这是一个很酷的 hack，但请注意 fix 是一把双刃剑，通常不建议使用：它取决于非常低级的细节Coq 的，这使得证明非常脆弱，当它们被破坏时，错误消息很难理解。

fix foo i，其中foo 是一个新变量，i 是一个整数，是一种适用于至少有i 参数的目标的策略（例如，forall n, evenb n = true -> ... 有两个：@ 987654328@ 和evenb n = true 的证明），并假设您要证明的目标，将新假设命名为foo。 （是的，你没看错。）

Theorem evenb_double_k : forall n,
  evenb n = true -> exists k, n = double k.
Proof.
  fix self 1.

(*

1 subgoal (ID 17)

  self : forall n : nat,
         evenb n = true -> exists k : nat, n = double k
  ============================
  forall n : nat, evenb n = true -> exists k : nat, n = double k

 *)

当然，有一个问题：必须将假设应用于n 的适当子项（这是目标的第一个参数，这就是fix self 1 的数字参数表示，我们说第一个参数是递减参数）。 n 的正确子项是什么？这是一个只有至少破坏一次n才能得到的值。

请注意，如果您仍然决定直接应用假设 self，Coq 不会立即抱怨（n 本身不是一个适当的子项）。 Coq 只检查Qed 上的“subterm”要求。 编辑：您也可以随时使用命令Guarded 进行检查。

  apply self. (* seems fine, all goals done. *)
Qed. (* ERROR! *)

您可以将fix 近似想象为一种强归纳形式，其中归纳假设 (self) 是针对所有小于当前项的项给出的，而不仅仅是直接的前项。然而这个“子项”关系实际上并没有出现在self 的语句中。 （这种特性使fix 成为一种低级、危险的策略。）

在fix 之后，您通常想要destruct 减少参数。这就是fix 允许你的证明遵循evenb 的结构的地方。下面，我们在S 的情况下再次立即销毁。所以我们得到了三种情况：n = O，n = S O，n = S (S n')，对于一些n' : nat。

第一种情况很简单，第二种是空洞的，第三种情况是你需要“归纳假设”selfn'。

Proof.
  fix self 1.
  intros n.
  destruct n as [| [| n']].
  - exists 0; reflexivity.
  - discriminate.
  - simpl. intro H.
    apply self in H.
    destruct H as [k Hk].
    exists (S k).
    rewrite Hk; reflexivity.
Qed.

其中的一些推理相当通用，甚至可以将其提取到自定义的归纳原理中，甚至是nats，具体来说是另一个Theorem。

Theorem even_ind :
  forall (P : nat -> Prop),
    P O ->
    (forall n, evenb n = true -> P n -> P (S (S n))) ->
    forall n, evenb n = true -> P n.

将其与nat 的标准归纳原理进行比较，这实际上也是一个定理，命名为nat_ind。这就是 induction 策略在后台使用的内容。

About nat_ind.

(* nat_ind :
     forall P : nat -> Prop,
       P 0 ->
       (forall n : nat, P n -> P (S n)) ->
       forall n : nat, P n
 *)

nat_ind 中的归纳步骤从n 变为S n，而even_ind 的归纳步骤从n 变为S (S n)，并有一个额外的假设，即我们的数字是偶数。

even_ind 的证明遵循与evenb_double_k 类似的结构，尽管它更抽象，因为它概括了P 上的所有谓词nat。

Proof.
  intros P HO HSS.
  fix self 1.
  intros n.
  destruct n as [| [| n']].
  - intro; apply HO.
  - discriminate.
  - intros H. apply HSS.
    + apply H.
    + apply self.
      apply H.
Qed.

这里的另一种方法是根本不使用fix（因为应该避免使用它），而是保留induction 作为原语来证明替代even_ind 原则。这对nat 来说很好，但是对于一些复杂的归纳类型，默认的归纳原理太弱了，手写fix 是唯一的方法。

最后，回到evenb_double_k，我们可以使用apply even_ind 的新归纳原理，而不是fix 或induction。我们现在只得到两个有意义的情况，O 和 S (S n')，其中n' 是偶数。

Theorem evenb_double_k' : forall n,
  evenb n = true -> exists k, n = double k.
Proof.
  apply even_ind.
  - exists 0. reflexivity.
  - intros n H [k Hk].
    exists (S k).
    rewrite Hk.
    reflexivity.
Qed.

---

此答案中使用的定义：

Fixpoint evenb n :=
  match n with
  | S (S n') => evenb n'
  | S O => false
  | O => true
  end.

Fixpoint double k :=
  match k with
  | O => O
  | S k' => S (S (double k'))
  end.

Answer 2

是的，绝对！让我们使用来自this answer的归纳原理。

From Coq Require Import Arith.

Lemma pair_induction (P : nat -> Prop) :
  P 0 -> P 1 ->
  (forall n, P n -> P (S n) -> P (S (S n))) ->
  forall n, P n.
Proof.
  intros H0 H1 Hstep n.
  enough (P n /\ P (S n)) by easy.
  induction n; intuition.
Qed.

现在我们可以像这样使用新原理（我将非标准函数与它们的 stdlib 对应项进行了切换，以便一切都编译）：

Theorem evenb_double_k : forall n,
  Nat.even n = true -> exists k, n = Nat.double k.
Proof.
  intros n Ev.
  induction n as [| |n IHn _] using pair_induction.
  (* the rest of the proof has been removed to not spoil the fun *)
Qed.