The Coq mailing list

[Michael Shulman <mshulman AT ucsd.edu>]

Ah, thanks!  Yes, I can see that that might be a useful feature.  But
it is certainly surprising to me!  Is this explained in the reference
manual?

On Thu, Apr 28, 2011 at 1:14 AM, Hugo Herbelin 
<Hugo.Herbelin AT inria.fr>
 wrote:
> Hi,
>
> On Mon, Apr 25, 2011 at 08:25:11PM -0700, Michael Shulman wrote:
>> I am confused by some behavior of metavariable binding in Ltac.  This
>> works as I would expect:
>>
>> Lemma test {A B} (f : forall x:A, B x) (a : A) : B a.
>> Proof.
>>   match goal with
>>     | |- B ?y => apply f with (x := y)
>>   end.
>> Qed.
>>
>> But this doesn't (just replace both y's with x):
>>
>> Lemma test {A B} (f : forall x:A, B x) (a : A) : B a.
>> Proof.
>>   match goal with
>>     | |- B ?x => apply f with (x := x)
>>   end.
>> Qed.
>>
>> It seems to me that there should be no difference; isn't the latter
>> just an alpha-conversion of the first?  Surely the 'x' on the
>> left-hand side of the := exists in a different scope (the dependent
>> arguments of f) and shouldn't be affected by the name of a local
>> metavariable?  Or is there some other subtlety I'm missing?
>
> The choice to allow the x on the left-hand side of := to be possibly
> given as a parameter of the ltac expression goes back to the initial
> design of Ltac. As soon as it is always possible to alpha-convert the
> code as you did in the first example, I do not see any real problem
> in keeping this feature, even if it might be a bit surprising when we
> experiment your second example.
>
> Hugo Herbelin
>