The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 11/24/2016 11:09 AM, Jan-Oliver Kaiser wrote:
> 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?

Any reduction will work (except for "red" which will fail because there 
is no head constant).  I just used "id" to illustrate that.

Also, on "lazy" vs. "cbv" - there is a bug in Coq that seems to make 
"cbv" style reductions a bit fragile on evars (see 
https://coq.inria.fr/bugs/show_bug.cgi?id=3906), while "lazy" reductions 
continue to work.

-- Jonathan

> 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