The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 07/26/2014 06:13 PM, Gregory Malecha wrote:
> Hi, Jonathan --
>
> There are things that could be done related to this, but I'm not sure
> that your proposal really changes much.
>
> You can achieve it by creating a new evar (say ?2) and
> instantiate the old evar (say ?1) with the application that you are
> proposing. If you revert all of your hypotheses first then this new
> evar will have an empty environment and you should get exactly what
> you are proposing.

The impression I get is that an empty environment is not as important as 
access to all the necessary components of the eventual instantiation 
such that those components aren't lost and don't change.  But, I have 
never attempted a full revert before creating an evar - I would think 
that results in an evar that can't use any of the hypotheses that are 
then intro'ed.  I will have to try that to see what happens...

> The main issue that I run up against when I have problems like this
> come from trying to instantiate a unification variable with an
> expression that came from a destruct. For example.
>
> x : nat * nat
> ============
> ....
> evar nat.
> destruct x as [fst_x snd_x].
> instantiate (1 := fst_x).
>
> The final instantiate doesn't work because [fst_x] is not in scope.

Right  - that's one type of instantiate problem - the not-in-scope 
variety.  Another is the not well-typed one that occurs when the type of 
something in the evar's environment changes due usually to type index 
effects following inversions.  Another is when the evar was created in 
the root of a subgoal tree, and you have to solve the one evar such that 
it satisfies disparate constraints in different subgoals.

> You could make it in scope by performing the same destruct in the
> unification variable which essentially does:
>
> instantiate (1 := match x with (fst_x,snd_x) => fst_x end).

Yes - so long as x stays accessible, its type doesn't change, etc.

> Of course you can still run into the problem when you are introducing
> new variables in other ways. I've thought about this feature before
> and it might make a lot of sense, but I have found that usually, you
> should just make evars as late as possible (for the most part).

Sure, when possible, and when it doesn't require me to attempt to 
predict what's needed well in advance.  I have tried to use Coq in the 
style of always posing things I will (or might) need in advance.  I 
don't like that style - it requires too much mental heavy lifting.  I 
would rather Coq be more of a proof assistant than merely a proof 
checker - so it should help me find the necessary instantiation terms, 
and not merely congratulate me when I'm good at predicting them myself.

>   Doing
> something like the above trick makes proof terms quite large because
> you'll be duplicating parts of the proof term in the unification
> variable. You also need to be careful about it because you don't want
> o introduce case splits when they don't matter.

You're right about duplicating proof parts - but I'm not nearly as 
worried about that as I am frustrated by not being able to instantiate 
an evar with the right term once I get far enough into a proof to 
determine what the right term is.   If the extracted OCaml doesn't 
suffer - then the duplication doesn't phase me.

-- Jonathan