Coq 归纳从特定的 nat 开始

Question

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

如果我在 coq 中有一个引理

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

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

任何提示？

Answer 1

以下证明了每个命题P对于all 都为真n>=1，ifP对于for 为真1，并且ifP归纳为真。

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.