The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

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