Coq 归纳从特定的 nat 开始

Question

我正在尝试学习 coq，所以请假设我对此一无所知。

如果我在 coq 中有一个引理

forall n m:nat, n>=1 -> m>=1 ...

我想通过对 n 进行归纳。我如何从 1 开始归纳？目前当我使用“归纳n”。战术它从零开始，这使得基本语句为假，从而难以继续。

任何提示？

Answer 1

以下是每个命题P的证明是真的n>=1 , 如果 P对 1 是正确的如果 P归纳为真。

Require Import Omega.

Parameter P : nat -> Prop.
Parameter p1 : P 1.
Parameter pS : forall n, P n -> P (S n).

Goal forall n, n>=1 -> P n.

我们通过归纳法开始证明。

  induction n; intro.

如果您有一个错误的假设，那么错误的基本案例是没有问题的。在这种情况下 0>=1 .

  - exfalso. omega.

归纳案例很棘手，因为要访问 P n 的证明，我们首先要证明n>=1 .诀窍是在n上做一个案例分析。 .如 n=0 ，那么我们可以简单地证明目标 P 1 .如 n>=1 ，我们可以访问P n ，然后证明其余的。

  - destruct n.
    + apply p1.
    + assert (S n >= 1) by omega.
      intuition.
      apply pS.
      trivial.
Qed.