The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 08/02/2014 11:38 AM, Jonathan wrote:
> ...
>
> So, I would guess that what instantiate is doing is reaching into the 
> dependent subgoal to do its work - ignoring whatever is going on (such 
> as name changing and the like) in the other subgoals.  If that is the 
> correct behavior, might expect "Display Existential Variable 
> Instances" to do the same, but it doesn't.  Alternately, perhaps the 
> dependent subgoal should undergo renamings as they occur in the other 
> subgoals?  But, how could you do this, as there could be multiple 
> other subgoals in which the evar exists, and they can all name the 
> same things differently?  Or, keep track of a renaming map between the 
> dependent subgoal and each of the others?  Or, always skolemize - 
> which is equivalent to reverting all in the dependent subgoal as soon 
> as it is introduced, so that they have no names to confuse?
>
> -- Jonathan

A further note to whomever might consider fixing evars - please keep in 
mind that it's not just renaming that is the problem.  Renaming might be 
the least of the problem, as illustrated here:

Goal forall (n:nat), True.
intros.
evar (i:nat).
apply id in n.
Fail instantiate (1:=n) in (Value of i).

If Coq is to allow true backward chaining, then it has to give evars 
more freedom than this.

-- Jonathan