coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Yannick <yannick.zakowski AT irisa.fr>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Shadowing binders abusively renamed?
- Date: Wed, 27 Jul 2016 16:29:42 +0200
Oh thanks Jonathan! You are right that I did not specify but am still on
8.5, I should switch.
That would solve the issue indeed. Out of curiosity, if anyone knows why
wrapping a tactic into a Ltac definition and chaining rather that using
a dot changes the behavior, I would still be interested.
Best,
Yannick
Le 27/07/2016 à 16:15, Jonathan Leivent a écrit :
> Yannick,
>
> I think this misbehavior of subst is fixed in 8.5pl2.
>
> -- Jonathan
>
>
> On 07/27/2016 09:50 AM, Yannick wrote:
>> Dear Coq Club,
>>
>> I am a bit confused with Coq's behavior towards hypotheses whose name
>> collude with a definition in its context. Please consider the following
>> minimal example, also enclosed with the mail:
>>
>> Ltac inv H := inversion H; try subst; clear H.
>>
>> Definition bar := False.
>>
>> Inductive Eq: nat -> nat -> Prop :=
>> | Eq_def: forall n m, n = m -> Eq n m.
>>
>> Lemma foo: forall (n:nat) (m:nat) (bar: Eq n m), False.
>> intros n m bar.
>>
>> A first observation here: 'intros' would rename bar as bar0, but 'intros
>> n m bar' will indeed name it bar. I guess it makes sense, we do not want
>> to shadow unless explicitly required.
>>
>> What confuses me more is the behavior of subst:
>>
>> inversion bar. (* Context: bar: Eq n m and a bunch of equalities named
>> H, H0, H1 *)
>> subst. (* Context: bar0: Eq m m *)
>>
>> Here subst actually renamed "abusively" my hypothesis.
>>
>> Finally, I am at total lost with the following:
>> Restart.
>> Fail (intros n m bar; inv bar).
>> (*
>> The command has indeed failed with message:
>> In nested Ltac calls to "inv" and "clear H", last call failed.
>> Error: Ltac variable H is bound to a value of type var which cannot be
>> coerced to a variable.
>> *)
>> intros n m bar.
>> inv bar. (** Succeed, by renaming on the way my hypothesis from bar to
>> bar0 **)
>> Restart.
>> intros n m bar.
>> Fail (inversion bar; subst; clear bar).
>> (*
>> The command has indeed failed with message:
>> No such hypothesis: bar
>> *)
>>
>> Given the previous observation on the behaviour of subst, the third case
>> failing is to be expected. However I do not quite grasp why wrapping it
>> in a Ltac call allows it to succeed, and even more so why it does not
>> when chained with a semi-colon.
>>
>>
>> Naturally, I would agree at any rate that using pre-existing names for
>> hypotheses is not quite a good policy. However I happened to do it
>> accidentally and had quite a hard time figuring what was going on. Any
>> explanation or pointers as to what is really going on in each case, and
>> confirmation that these behaviours are indeed desired, would be awesome.
>>
>> Thanks a lot in advance,
>> Best,
>> Yannick
>
- [Coq-Club] Difference between uconstr and open_constr, Robbert Krebbers, 07/27/2016
- Re: [Coq-Club] Difference between uconstr and open_constr, Jonathan Leivent, 07/27/2016
- Re: [Coq-Club] Difference between uconstr and open_constr, Jonathan Leivent, 07/27/2016
- [Coq-Club] Shadowing binders abusively renamed?, Yannick, 07/27/2016
- Re: [Coq-Club] Shadowing binders abusively renamed?, Jonathan Leivent, 07/27/2016
- Re: [Coq-Club] Shadowing binders abusively renamed?, Yannick, 07/27/2016
- Re: [Coq-Club] Shadowing binders abusively renamed?, Jonathan Leivent, 07/27/2016
- Re: [Coq-Club] Shadowing binders abusively renamed?, Yannick, 07/27/2016
- Re: [Coq-Club] Shadowing binders abusively renamed?, Jonathan Leivent, 07/27/2016
- [Coq-Club] Shadowing binders abusively renamed?, Yannick, 07/27/2016
- Re: [Coq-Club] Difference between uconstr and open_constr, Pierre-Marie Pédrot, 07/27/2016
- Re: [Coq-Club] Difference between uconstr and open_constr, Jonathan Leivent, 07/27/2016
- Re: [Coq-Club] Difference between uconstr and open_constr, Jonathan Leivent, 07/27/2016
Archive powered by MHonArc 2.6.18.