我可以告诉 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

是的，绝对！让我们使用来自 .

的归纳原理

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.

Answer 2

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

fix foo i，其中 foo 是一个新变量，i 是一个整数，是一种适用于至少有 i 个参数的目标的策略（例如，forall n, evenb n = true -> ... 有两个：n 和 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（n 本身不是一个适当的子项），Coq 不会立即抱怨。 Coq 仅检查 Qed 上的 "subterm" 要求。编辑：您也可以随时使用命令Guarded来检查。

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

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

在 fix 之后，您通常希望 destruct 递减参数。这是 fix 允许您的证明遵循 evenb 结构的地方。下面，我们在 S 的情况下立即再次析构。所以我们得到三种情况：n = O、n = S O、n = S (S n') 对于某些 n' : nat。

第一种情况很简单，第二种是空洞的，第三种是你需要 "induction hypothesis" self at n'.

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 相似的结构，尽管它更抽象，因为它概括了 nat 上的所有谓词 P。

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.

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

Can I tell Coq to do induction from n to n+2?

coq

induction