coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Introduce existing variable

From: Thomas Braibant <thomas.braibant AT gmail.com>
To: Michael <michaelschausten AT googlemail.com>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] Introduce existing variable
Date: Mon, 19 Jul 2010 11:07:09 +0200
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:content-transfer-encoding; b=Kz1D/CQyZmFUWI2e1teSByz6KDaSZolOBMSIJEaANfyCAIdFV44OMY3m7p+/XYj4jy erRRManS0p+2Tpej8T0xUiax1qzT1O3/MKPg7V6LLQ1tBRSYvQmgQrDkccM6cx7su0M4 S9+WuQUgz6hHBxORmsVEjKsjfjt71Gx3SGWx8=

try destruct (Lem1 theyvariableyouwant) in the proof of your second lemma .

thomas

On Mon, Jul 19, 2010 at 11:04 AM, Michael
<michaelschausten AT googlemail.com>
wrote:
> Hello,
>
> I've got a Lemma, stating that for every y of myType there's a corresponding
> x:Z
>
> Lem1:
> �forall (y: myType),
> �exists x : Z,
> �(x = func1(y)),
> Admitted.
>
> Now in my proof, I've got some variables of myType in a formula, which I
> would
> like to be replaced, e.g.:
>
> func1(y0) * 3 <= func1(y0) * 4 + 3
>
> Since Coq doesn't know much about func1, this can't be solved at first.
> Therefore, I'd like to introduce a new variable according to Lem1, to
> change it
> to
>
> x0 * 3 <= x0 * 4 + 3.
>
> How can I "apply" my Lemma Lem1 to the proof here?
>
>
> Sincerely
>

[Coq-Club] Introduce existing variable, Michael
- Re: [Coq-Club] Introduce existing variable, Thomas Braibant
- Re: [Coq-Club] Introduce existing variable, Vincent Siles
- <Possible follow-ups>
- Re: Re: [Coq-Club] Introduce existing variable, Michael