在 Coq 中使用从 1 开始的归纳法

Question

我正在尝试在 Coq 证明中使用从 1 开始的归纳法。从this question得到了我需要的归纳原理证明：

Section induction_at_1.
  Variable P : nat -> Prop.
  Hypothesis p1 : P 1.
  Hypothesis pS : forall n, P n -> P (S n).

  Theorem induction_at_1:
    forall n, n > 0 -> P n.

    induction n; intro.
    - exfalso; omega.
    - destruct n.
      + apply p1.
      + assert (S n >= 1) by omega.
        intuition.
  Qed.
End induction_at_1.

我得到的结果在结构上与标准归纳法非常相似。事实上，Check nat_ind 产生

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

而 Check induction_at_1 产生

induction_at_1:
  forall P : nat -> Prop,
  P 1 ->
  (forall n : nat, P n -> P (S n)) ->
  forall n : nat, n > 0 -> P n

当我尝试应用这个归纳原理时，问题出现了。比如我想用归纳法证明

Lemma cancellation:
  forall a b c: nat, a > 0 -> a * b = a * c -> b = c.

这似乎完全适合我上面的那种归纳，但是当我这样开始我的证明时

  intros a b c H0 H1.
  induction a using induction_at_1.

我收到以下无法解释的错误：

Not the right number of induction arguments (expected 2 arguments).

由于这两个归纳原理对我来说看起来几乎相同，所以我不确定为什么这不起作用。有什么想法吗？

Answer 1

我也觉得这种行为令人费解，但有几种解决方法。一种是使用 ssreflect 归纳策略，称为 elim:

From Coq Require Import ssreflect.

Lemma cancellation:
  forall a b c: nat, a > 0 -> a * b = a * c -> b = c.
Proof.
intros a b c H.
elim/induction_at_1: a / H.
(* ... *)
Abort.

第二行告诉 Coq 对 H（不是 a）进行归纳，同时泛化 a 并使用归纳原理 induction_at_1。我无法使用常规 Coq induction.

获得类似于工作的东西

另一种方法是使用简单的自然数归纳法。在这种情况下，我相信引理遵循 b 的归纳，同时概括 c（我不确定 a 的归纳是否有效）。如果您确实需要为所有 n 显示 m <= n -> P n 形式的内容，您可以将 n 替换为 n - m + m（这在 m <= n 假设下应该是可能的), 然后通过对 n - m.

的归纳来证明 P (n - m + m)

在 Coq 中使用从 1 开始的归纳法

Using induction starting from 1 in Coq

formal-verification

coq

coq-tactic