The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

If you have your hands on an evar in Ltac, is there a way to get it as a goal?  For example, could I do something like:

match type of H with

  | _ /\ ?R => is_evar R; R: refine (_ : _ /\ _)

end

On Wed, Jul 23, 2014 at 2:16 PM, Jonathan <jonikelee AT gmail.com> wrote:

On 07/23/2014 04:44 AM, Arnaud Spiwack wrote:

Instantiate deprecated?  I thought that was the way to handle evars
manually.  How else?

Kinda sorta… ish.

Coq has a lot of backstory and stuff. So the treatment of existential
variables is not superbly uniform. In trunk, the [refine] tactic introduces
existential variable as goals. It is the preferred way to manipulate
existential variable explicitly.

For instance, instead of [evar (P:Prop)], you can use [refine (let P:Prop
:= _ in _)] and get two goals: one for your goal with a new binding [P :=
?x : Prop], and one (the first one actually) of type [Prop], whose solution
will instantiate [?x] (and vice-versa, if [?x] is partially instantiated,
the goal will be considered solved).

Now, it may not fit your needs. Since the new refine is new, and the
possibilities are largely unexplored and suffer from limited support, you
may still need [instantiate]. But hopefully, we can get rid of
[instantiate] eventually: it's not a very elegant solution.

OK for evar, but I still don't see how to get around using instantiate by using refine instead:

Consider a goal (consequent) that is a complex term containing evars - in order to use refine to solve one or more of those evars, doesn't one have to line up the underscores in the refine pattern with the evar occurrences in the goal?  That could be quite complicated.  It sounds like one would have to use match to construct the refine pattern specifically for the goal - or just recursively descend via a tactic into the goal doing has_evar/is_evar to find evars.

I'm not trying to suggest that instantiate is nice (it's quite nasty, actually).  I just don't see an easy way around it with refine.  But I also wouldn't want to hamper the progress made in the trunk with respect to coping with evars.

Since it's the 45'th anniversary of the moon landing, I am reminded of a classic Volkswagen advertisement showing a picture of the lunar module on the moon with the caption "It's ugly, but it gets you there".

-- Jonathan