The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 08/01/2014 12:03 PM, Cedric Auger wrote:
> An example of how fragile evar instantiability is in Coq:
>
> Goal forall (n:nat), True.
> intros.
> evar (i:nat).
> instantiate (1:=n) in (Value of i). (*this works*)
> Abort.
>
> Goal forall (n:nat), True.
> intros.
> evar (i:nat).
> rename n into m. (*renaming blocks instantiation:*)
> Fail instantiate (1:=m) in (Value of i).
> Abort.
>
> Goal forall (n:nat), True.
> intros.
> evar (i:nat).
> revert n; intro n. (*even this blocks instantiation:*)
> Fail instantiate (1:=n) in (Value of i).
> Abort.
>
>
> In fact, when write "evar (i:nat).", that means that the evar "i" depends
> on the context in which it was introduced,
> that is: "n:nat". When you do "revert n.", "n" is removed from the
> dependencies of "i" (as it would have been with a "clear n"),
> meaning that evar "i" must be closed under the empty context.
> When you do "intro n.", you introduce a variable which cannot instantiate
> "i", as "n" is not a term closed in the empty context.

Having an operational explanation for the behavior unfortunately doesn't 
help one cope very well with its consequences.  The main consequence is 
that, once an evar shows up in a goal, the user must really think hard 
about every following proof step prior to the point when they are ready 
to instantiate that evar.  In fact, they have to think too hard - they 
have to know the inner workings of each tactic they will use between 
those times so that they can avoid those that alter the evar's context 
in ways that might impact the eventual instantiation, even if those 
tactics seemingly leave the goal intact.  Or, be prepared to do a lot of 
undos, head-scratching, and wild guesses.

The skolemization trick I mention in another thread helps somewhat. 
Perhaps the "refine-born" evars in the trunk will also help (they seem 
to be the dual of skolemization in a way - as going into a "dependent 
subgoal" and reverting all hypotheses there induces the corresponding 
evar to skolemize).  But I think any such tricks will come at their own 
usability cost.

> I cannot try it, but what is the result of:
>
> Goal forall (n:nat), True.
> intros.
> evar (i:nat).
> generalize n; intro m.
> Fail instantiate (1:=m) in (Value of i).
> Abort.

Yes - that fails as well.

> Here, I do not know if the link between "m" and "n" is established, and as
> "n" is still in the dependencies of "i", it could work.
>
> For your second case, I do not know how rename works internally. It could
> be implemented as something equivalent to a
> "revert all terms dependent on 'n', then revert 'n', then intro 'm', then
> intro all terms now dependent on 'm'".
> If this is the case, that could explain the error.
>
> To test it, one can do something like:
>
> Definition test : Type -> Type.
>    intros x.
>    rename x into y.
>    exact y.
> Defined.
>
> Print test.
>
> And see how y is introduced in the proof term.

The proof term doesn't mention y.  I wouldn't expect it to - it's just 
renaming a bound var, so Coq sees it as a no-op:

test = fun x : Type => x
     : Type -> Type

> Some remark:
>
> Goal forall m n, m<n -> False.
> Proof.
>    intros m n Hmn.
>    revert m. (* ← triggers an error for obvious reasons *)
> Abort.
>
> But with evars, no such thing is done (more or less thankfully, as it could
> be quite inconvenient not to be able to use tactics
> like clear in presence of evars introduced when these hypotheses were
> alive).
> Maybe a warning could be raised in these cases?
>
> Or more ideally, maybe that a "dependent reverse" could be defined (well,
> that may already be the case), and when calling it, all dependencies
> (including evars) could be generalized.
> This way, the link would not be lost.
>
> n : nat.
> i := ?(n) : nat (*evar*)
> m : nat
> H : P m i
> ========
> Q
>
> ------------
> "dependent revert n."
> would produce:
>
> m : nat
> ========
> forall n:nat, set i := ?(n) in P m i -> Q

That is a good point - because the following does work:

Goal forall (n:nat), True.
intros.
evar (i:nat).
revert i.
revert n.
intros n i.
instantiate (1:=n) in (Value of i).
Abort.

But note that this still doesn't:

Goal forall (n:nat), True.
intros.
evar (i:nat).
revert i.
rename n into m.
intro i.
Fail instantiate (1:=m) in (Value of i).
Abort.

Hmm - this must be bug:

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

Because, amazingly, i seems to recall m's past life as n:

Goal forall (n:nat), True.
intros.
evar (i:nat).
revert i.
revert n.
intros m i. (*no more n*)
instantiate (1:=n) in (Value of i). (*Note: n, not m!*)
Abort.

Even this works:

Goal forall (n:nat), True.
intros.
evar (i:nat).
rename n into m. (*Again, no more n*)
instantiate (1:=n) in (Value of i). (*Note: n, not m!*)
Abort.


So, maybe much of what I am complaining about are just bugs?

-- Jonathan