coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] subst tactic and parameters, Denis Cousineau, 07/09/2012
- Re: [Coq-Club] subst tactic and parameters, Adam Chlipala, 07/09/2012
- Re: [Coq-Club] subst tactic and parameters, Denis Cousineau, 07/09/2012
- Re: [Coq-Club] subst tactic and parameters, AUGER Cédric, 07/09/2012
- Re: [Coq-Club] subst tactic and parameters, Adam Chlipala, 07/09/2012
Archive powered by MHonArc 2.6.18.