5

I'm trying to learn coq so please assume I know nothing about it.

If I have a lemma in coq that starts

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

And I want to proceed by induction on n. How do I start the induction at 1? Currently when I use the "induction n." tactic it starts at zero and this makes the base statement false which makes it hard to proceed.

Any hints?

4

1 回答 1

4

下面是一个证明，证明每个命题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.
于 2014-11-29T19:27:23.177 回答