The Coq mailing list

[Eddy Westbrook <westbrook AT galois.com>]

Hi Jonathan,

I actually just figured out the following trick, where I can write my own 
unification algorithm using the typeclass mechanism:

Class MyUnify A (x y : A) : Prop := { my_unify : x = y }.

Instance MyUnify_refl A x : MyUnify A x x := ltac:(repeat econstructor).

Instance MyUnify_app A B fl fr argl argr :
  MyUnify (A -> B) fl fr -> MyUnify A argl argr -> MyUnify B (fl argl) (fr 
argr).
...

Instance MyUnify_lam A B fl fr (pf:forall x, MyUnify B (fl x) (fr x))
  : MyUnify (A -> B) fl fr.
...

Then, instead of unifying my dependent and non-dependent functions f1 and f2, 
I was able to assert (Unify f1 f2), and use the typeclass resolution 
mechanism to instantiate the necessary evars for me.

If you do get your implementation done, definitely let me know, but please 
don’t get too far into on my account. :)

Thanks again for all your help,
-Eddy


> On Dec 2, 2016, at 2:39 PM, Jonathan Leivent 
> <jonikelee AT gmail.com>
>  wrote:
> 
> 
> 
> 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
>