The Coq mailing list

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

Hi,

> 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?

I'm afraid that several such isolated peculiar features of Ltac are
not documented...

Hugo

> 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
> >
>