coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Howto instantiate forall in the assumptions?

From: Matthieu Sozeau <matthieu.sozeau AT gmail.com>
To: Hendrik Tews <tews AT os.inf.tu-dresden.de>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] Howto instantiate forall in the assumptions?
Date: Tue, 30 Nov 2010 11:25:12 +0100
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=subject:mime-version:content-type:from:in-reply-to:date:cc :content-transfer-encoding:message-id:references:to:x-mailer; b=n35BcuYQHf56TxzFk7aEvHOji+OOcyjUB3mri1A9XKMThp+epb62Efy3AFNcKLfuQd KzqDcy4OH8ptnHyyg+SbE1CqZTcIS6fYkgVmRXdUdguAHNk2gtTGg1ZuOac0fELCZ+1X BzXxkXNfRV809MEV++FpQzLYYneag4FsgSAzA=

Le 30 nov. 2010 � 11:15, Hendrik Tews a �crit :

> Hi,
>
> I have a goal with "forall c : C, ... " in the assumptions, for
> which apply fails for various reasons. I was not able to
> instantiate it and finally solved the problem with cut. IMO this
> use of cut is a bad workaround, because it requires to copy the
> complete body of the forall and to perform the substitution
> manually.
>
> How can I manually instantiate a universal
> quantification/dependent product in the assumptions?

Hi Hendrik,

you can use the [specialize] tactic to do that, e.g [specialize (H t u)].

-- Matthieu

[Coq-Club] Howto instantiate forall in the assumptions?, Hendrik Tews
- Re: [Coq-Club] Howto instantiate forall in the assumptions?, Matthieu Sozeau
- Re: [Coq-Club] Howto instantiate forall in the assumptions?, St�phane Lescuyer