coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] how to prove this?

From: Jean-Francois Monin <jean-francois.monin AT imag.fr>
To: Sidi <Sidi.Ould_Biha AT inria.fr>
Cc: catty wang <catty.wang AT gmail.com>, coq-club AT inria.fr
Subject: Re: [Coq-Club] how to prove this?
Date: Tue, 29 Jun 2010 14:34:36 +0800
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=sender:date:from:to:cc:subject:message-id:references:mime-version :content-type:content-disposition:in-reply-to:user-agent; b=ZQ9CdDS5y9KwvnvjhYcly37kMXOLbCQrKYw+1BE2bUsRinlQtoyHR1Oem9890CvQ4q dpZgnFA7dg3i2G9aMB7ZmSxZPuq/WIZZo4bJw43xjdIM1HsHDGU22ssITCoKk/udc+xs 11bjcMCPnFBn2FyDCnT1N83OkDNfqc+/tQykA=

Well, since + is already there, you don't need induction anymore!

Goal forall x, exists y, y = x + 2.
intro x. exists (x+2). reflexivity.

JF

On Tue, Jun 29, 2010 at 02:23:05PM +0800, Sidi wrote:
> On Tue, 2010-06-29 at 13:52 +0800, catty wang wrote:
> > hi,all:
> >
> >        I wondering how to prove this :
> >                        forall x:nat, exists y:nat,y=x+2.
> >        please help me,thanks .
> >
> >                                         catty.
> >
> Hi,
> You can prove this lemma by induction x.
>
> Goal forall x, exists y, y = x + 2.
> induction x. exists 2; auto.
> destruct IHx as [x' Exx']. exists (S x'). simpl. auto.

[Coq-Club] how to prove this?, catty wang
- Re: [Coq-Club] how to prove this?, Sidi
  - Re: [Coq-Club] how to prove this?, Jean-Francois Monin