The Coq mailing list

[Jan-Oliver Kaiser <janno AT mpi-sws.org>]

Hello Jonathan,

Thank you! This will prevent a lot of future headache. My preliminary 
tests indicate that it is not actually `id` which is unfolded here - it 
seems to work with all valid names. Am I right in assuming that you took 
`id` because it is a somewhat canonical choice of an existing name?

Best,
Jan-Oliver

On 11/24/2016 04:56 PM, Jonathan Leivent wrote:
> Hi Jan-Oliver,
>
> This will demonstrate the issue:
>
> exvar Type (fun t => unify t nat; idtac t; let t2 := eval lazy delta
> [id] in t in idtac t2).
>
> The first idtac will print something like "?X6", while the second will
> print "nat".  What type of reduction is done is not important
> (obviously, there is no id function to delta reduce here, so this
> reduction is a no-op).   Coq isn't always very good about noticing the
> instantiation of an evar through the raw evar itself, so this reduction
> step just prods it into doing so.
>
> -- Jonathan
>
>
> On 11/24/2016 09:59 AM, Jan-Oliver Kaiser wrote:
> > Hello,
> >
> > I am trying to find occurrences of an instantiated existential
> > variable in a bigger term. I have yet to find a way to make this work.
> > I have, however, identified a rather peculiar minimal failing example
> > of interaction between evars and match context:
> >
> > (* Some notation to hide a the overhead associated with evars *)
> > Tactic Notation "exvar" constr(type) tactic(cnt) :=
> >   let name := fresh in
> >   evar (name : type);
> >   let var := (eval unfold name in name) in
> >   clear name;
> >   cnt var.
> >
> > Goal True.
> >   exvar Type (fun t => unify t nat; match nat with context f [nat] =>
> > idtac "yay" end).
> >   Fail exvar Type (fun t => unify t nat; match nat with context f [t]
> > => idtac "yay" end).
> > Abort.
> >
> > The first call to exvar is just a sanity check to see if the evar
> > machinery works and the context pattern work as intended. The second
> > call is what really baffles me. t is successfully unified with nat -
> > but it cannot be found in the term nat. What is going on here?
> >
> > Thanks,
> > Jan-Oliver