The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Hi, 

  Indeed, the unification problem is easy enough and falls into the pattern fragment. 

However, it looks like [apply]'s unification is buggy here indeed. The type inference 

unification algorithm is able to solve all of this:

Definition foo A B : (A -> B) = (A -> B) := eq_refl.

(** Due to the refine, we use [evarconv]'s algorithms (the one of type inference)

    instead of [apply]'s *)

Tactic Notation "unify'" open_constr(t) open_constr(u) :=

  assert(t = u); [refine eq_refl|].

Goal { T:_ & T }.

  refine (existT _ (forall (x:?[T1]) (y:?[T2]), ?T1) _).

  evar (Tnew:Type).

  unify (fun (x:?T1) => ?T2) (fun (x:?T1) => ?Tnew). Undo.

  unify' (fun (x:?T1) => ?Tnew) (fun (x:?T1) => ?T2). Undo.

  Fail unify (fun (x:?T1) => ?Tnew) (fun (x:?T1) => ?T2).

  unify (forall (x:?T1), ?T2) (forall (x:?T1), ?Tnew). Undo.

  Fail unify (forall (x:?T1), ?Tnew) (forall (x:?T1), ?T2).

  unify' (forall (x:?T1), ?T2) (forall (x:?T1), ?Tnew). Undo.

  unify' (forall (x:?T1), ?Tnew) (forall (x:?T1), ?T2). Undo.

  

  Fail unify (forall (x:?T1) (y:?T2), ?T1) (forall (x:?T1), ?Tnew).

  Fail unify (forall (x:?T1), ?Tnew) (forall (x:?T1) (y:?T2), ?T1).

  unify' (forall (x:?T1) (y:?T2), ?T1) (forall (x:?T1), ?Tnew). Undo.

  unify' (forall (x:?T1), ?Tnew) (forall (x:?T1) (y:?T2), ?T1).

Abort.

  

Goal { T:Type | T=T }.

  refine (exist _ (forall (x:?[T1]), ?[T2]) _).

  refine (foo _ _).

Best,

-- Matthieu

On Sat, Dec 3, 2016 at 7:20 AM Jason Gross <jasongross9 AT gmail.com> wrote:

Regarding the unification fragment this falls into, I believe that it falls into the pattern fragment (though I'm not completely sure), and Coq should be able to solve that fragment.

On Fri, Dec 2, 2016, 7:53 PM Eddy Westbrook <westbrook AT galois.com> wrote:

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
>