The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 12/02/2016 04:54 PM, Eddy Westbrook wrote:
> Thanks for your help, Jonathan.
>
> Is there any way to search a term to find all the evars in it, so I can 
> skolemize all of them? I would like to do something like this, where R is a 
> typeclass that only has an instance for non-dependent function types:
>
> Ltac prove_R :=
>    lazymatch goal with
>    | |- R (forall x:?A, ?B) => skolemize_all_evars B; apply 
> R_nondep_fun_instance
>    end.
>
> Thanks again,
> -Eddy

It should be possible to write a tactic that skolemizes every 
evar-under-binders in a term with respect to just those binders it is 
under.  But, if you want to apply a non-dependent lemma, then you have 
to clear the dependent vars, not revert them, right?
However, the same tactic mechanism could probably do either, subbing 
clear for revert...

Part of the trick to doing this is to understand that instantiate can 
reach evars under binders, while match contexts cannot - hence one can 
remove top-level evars by something like:

  repeat match goal with
  |- context[?E] => is_evar E; set E
  end.

The next part of the trick is harder, as one has to descend under 
binders to accumulate the variables that one wants to skolemize 
remaining evars with respect to, then call instantiate (1:=ltac:(revert 
V)) for each of those, in the right order.  Then when the next evar is 
skolemized, do the above match again to factor it out of the goal, and 
repeat...

If a brute-force skolemization (all vars, even if not a binder) is OK, 
one can just do instantiate (1:=ltac:(revert_all)) instead, where 
revert_all is:

  Ltac revert_all := repeat lazymatch goal with H:_ |- _ => revert H end.

in which case, there is no need to descend under binders.

I've written versions of the brute-force tactic, but not the careful 
one.  I guess I could give it a try....

-- Jonathan