Coq诱导从特定的nat开始 [英] Coq induction start at specific nat

问题描述

我正在尝试学习普通话，所以请假设我对此一无所知.

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

如果我在coq中有一个引理，

If I have a lemma in coq that starts

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

我想对n进行归纳.如何从1开始感应?目前，当我使用归纳n"时.策略从零开始，这会使基本语句为假，从而使其难以执行.

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.

有任何提示吗?

推荐答案

以下证明每个命题P对于所有n>=1都是正确的，如果P对于1是true且如果P归纳地是真的.

The following is a proof that every proposition P is true forall n>=1, if P is true for 1 and if P is inductively true.

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.

我们通过归纳开始证明.

We begin the proof by induction.

  induction n; intro.

如果存在错误的假设，那么错误的基本情况就没有问题.在这种情况下，0>=1.

A false base case is no problem, if you have a false hypothesis laying around. In this case 0>=1.

  - exfalso. omega.

归纳式的情况很棘手，因为要访问P n的证明，我们首先必须证明n>=1.诀窍是对n进行案例分析.如果是n=0，那么我们可以简单地证明目标P 1.如果是n>=1，我们可以访问P n，然后验证其余部分.

The inductive case is tricky, because to access a proof of P n, we first have to proof that n>=1. The trick is to do a case analysis on n. If n=0, then we can trivially proof the goal P 1. If n>=1, we can access P n, and then proof the rest.

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

这篇关于Coq诱导从特定的nat开始的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！