The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 07/28/2014 09:08 AM, Gregory Malecha wrote:

...

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.

Here's an example of how to use this skolemization trick in a case like the above one:

Ltac assign name term :=
  match goal with
      H := ?V : _ |- _ => match H with name => unify V term end
  end.

Goal forall (x : nat * nat), True.
intro x.
evar (n:nat).
assert (n=fst x). (*the actual goal*)
(*skolemize n over everything else in the goal (just x in this case):*)
evar (f:nat*nat->nat). assign n (f x). subst f.
(*Now proceed with the proof search*)
destruct x as [fst_x snd_x].
(*solve for the skolemizing function:*)
subst n. reflexivity.

This works in the trunk.  I don't have a version of 8.4 handy to try it in. 

Note that the assign tactic, by using unify directly on the evar, seems to work in more cases than instantiate - but still not enough to eliminate the need for skolemization in a case like this.  Maybe that's a feature only available in the trunk.  If so, you might have to introduce the skolemizing function evar f prior to the evar n.

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.

I assume that you want to use the hypothesis at the type produced by
the inversion rather than the initial one. Ultimately the issue is
that Coq is punning the context of the unification variable and the
current goal.

You're elaborating the proof to find out what you need to solve the evar - maybe somethings that were from earlier than the evar, maybe some that were introduced later.  The purpose of the skolemization trick is to make it so that the evar remains receptive to its eventually determined contents, even if they are not in scope or not well-typed in the original environment of the evar.

It might be possible to do this kind of thing with the new tactic
engine in 8.5 (though I don't know much about its internals).
Essentially, you would need to say "in all the evars in this goal, do
the following tactic". That would manipulate the types/contexts of
those evars appropriately. This is essentially what I mentioned in my
previous email. With dependency this might get trickier though.

That may be possible with the refine-born evars in 8.5.  I still don't know enough about them.

I don't know a way to do it in the 8.4 tactic engine though that
doesn't mean it isn't possible, at the very least, you could write a
plugin that does it. I would doubt that something like this makes it
into the main tactic code to be done automatically because it seems
pretty heavy and would probably mess up proofs of people that are not
expecting it.

I never intended to suggest that all evars get skolemized automatically.  A tactic to do so would be preferrable.  I am working on a tactic to skolemize an arbitrary evar, and one to solve skolem-function equalities (which aren't always solvable just by reflexivity).  I have seemingly-working versions of both, and am testing them.

-- Jonathan