The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 08/02/2014 02:56 AM, Cédric wrote:
> ...
>
> By the way, Jonathan asked if there was a bug in the variable renaming with
> respect to evars.
> I think it is the case as:
>
> *********************************************
> Hypothesis P : nat -> nat -> Prop.
> Hypothesis Q : Prop.
>
> Goal forall (n m : nat), Q.
>
> intros n.
> evar (i:nat).
> intros m.
> cut (P m i).
> intros H.
>
> revert H.
> revert i.
> revert n.
> intros p.
> intro i.
> ********************************************
> outputs:
>
> 2 subgoal
> m : nat
> p : nat
> i := ?7 (* [p] *) : nat
> ______________________________________(1/2)
> P m i -> Q
> ______________________________________(2/2)
> P m i
>
>
> and still "instantiace (1:=p) in (Value of i)" does not work, while the 
> display
> clearly prints that it can only depend on 'p', while the old name 'n' still
> works (and uses 'p' in fact).
>
> ---
> Cédric AUGER

Also note that "instantiate (1:=n) in (Value of i)" does work.  What may 
be happening (I'm straining to see into this black box) is perhaps made 
clearer using the "refine-born" evars in the trunk, with their dependent 
subgoals:

Hypothesis P : nat -> nat -> Prop.
Hypothesis Q : Prop.

Goal forall (n m : nat), Q.

intros n.
refine (let i:=_:nat in _). shelve.
intros m.
cut (P m i).
intros H.

revert H.
revert i.
revert n.
intros p.
intro i.

Unshelve.
Focus 3.

This dependent subgoal corresponding to the evar still has the 
hypothesis named n:

1 subgoal
n : nat
______________________________________(1/1)
nat

And, "exact n" works here.

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