coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Taral <taralx AT gmail.com>
To: Jean-Francois Monin <jean-francois.monin AT imag.fr>
Cc: Sidi <Sidi.Ould_Biha AT inria.fr>, catty wang <catty.wang AT gmail.com>, coq-club AT inria.fr
Subject: Re: [Coq-Club] how to prove this?
Date: Wed, 30 Jun 2010 18:56:29 -0700
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type; b=Z3z7DI+VKnk2BLm9e1jIfvy3YD8nri6BBrVHp9cqfG9s9KBzcU4RHNPRVjJuHVTYkv mmun1Dy4n5+efiFhElRA/Hng/mgToDx0JItJDP4HcU1lYHXGChi/pVPopzX9MXP4AQ99 foiIeNPnD6P+6Uxcf++qoWuluLjSk8V+drKWg=

On Mon, Jun 28, 2010 at 11:34 PM, Jean-Francois Monin
<jean-francois.monin AT imag.fr>
wrote:
> 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.

Too much work.

Goal forall x, exists y, y = x + 2.
eauto.
Qed.

--
Taral
<taralx AT gmail.com>
"Please let me know if there's any further trouble I can give you."
-- Unknown

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