The Coq mailing list

[Gregory Malecha <gmalecha AT cs.harvard.edu>]

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 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.
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).

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). 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.





On Fri, Jul 25, 2014 at 7:43 PM, Jonathan 
<jonikelee AT gmail.com>
 wrote:
> I've been thinking more about why evars can't always get instantiated with
> things that look like they should fit, at least in terms of their respective
> types - or, rather, how to avoid this problem (without judicious use of
> undo, or the mental equivalent).
>
> The exact rules by which Coq keeps evars consistent are very unclear to me -
> and it seems they are sometimes too conservative.  But, if one wants to keep
> an evar permanently solvable, could a trick from skolemization work?  That
> would involve changing an evar of type T into a function of type [types of
> all other hypotheses in the current goal] -> T that is in turn then applied
> to all other hypotheses in the current goal.  It's cumbersome, but wouldn't
> that keep the resulting evar invulnerable to changes in any of those
> hypotheses (as from inversion and the like)?
>
> As a rough example, consider a goal like:
>
>   a : A
>   b : B
>   c : C
>   d : D
>   e := ?42 : E
> ==========
> ....
>
> In this case, introduce a new evar f that is a function of type
> A->B->C->D->E, and instantiate e with its application:
>
>   a : A
>   b : B
>   c : C
>   d : D
>   f := ?57 : A -> B -> C -> D -> E
>   e := f a b c d : E
> ==========
> ....
>
> Then, as the goal evolves, and the hypotheses a b c d possibly change as per
> inversion and the like, f should still be instantiatable by something
> useful, I think - hopefully just some "glue logic" over the values of its
> arguments.
>
> Could any of the experts comment on whether this should work?  I think I
> could write the necessary tactic to automatically generate such an evar
> combo for a specific goal and target type (E in the above), but I don't have
> a clue how much testing or of what kinds I would have to run on that tactic
> to determine if it really does the job in all cases.
>
> I thought of this when trying to understand the ramifications of the new
> refine-induced evar behavior.  It looked to me almost as though refine was
> doing something like the above trick (f in the above is the "dependent
> subgoal").  If so, that's great, but there are many more sources of evars
> than just refine.
>
> -- Jonathan
>



-- 
gregory malecha
http://www.people.fas.harvard.edu/~gmalecha/