The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

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