Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] subst tactic and parameters

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] subst tactic and parameters


Chronological Thread 
  • From: Denis Cousineau <cousineau AT lix.polytechnique.fr>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] subst tactic and parameters
  • Date: Mon, 9 Jul 2012 15:30:18 +0200


Le 9 juil. 2012 à 15:09, Adam Chlipala a écrit :

> On 07/09/2012 09:03 AM, Denis Cousineau wrote:
>> I've found that the tactic subst only works with equations in contexts
>> that concern variables that were quantified in the goal, and not global
>> parameters.
>>
>

Thanks for your very quick answer,

> I imagine this issue hasn't bothered others because use of global
> parameters is strongly discouraged; it's really against the spirit of
> constructive logic!

Sorry for the spirit, I'm actually certifying smt-solver results into Coq,
and the use of global parameters is very convenient.

>
> But, you can easily get [subst] to behave as you wish for parameter [x] by
> running:
> generalize dependent x; intros; subst.

Thanks, but that's a bypass for [subst x] and not for [subst].

Ok, I could write the ltac code to get all hypotheses of the form [x=y] then
generalize/intro all those x (or y), and then use [subst]...
But that's exactly what [subst] does (except the generalize/intro of course),
and that's a pity to have to re-implement it for global parameters.

Denis





Archive powered by MHonArc 2.6.18.

Top of Page