The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Nope, that was frozen already. It might have a considerable impact so we'll need to evaluate it but I hope we'll have it in the following version.

Le jeu. 8 déc. 2016 à 18:34, Eddy Westbrook <westbrook AT galois.com> a écrit :

Matthieu,

Does this mean that the fix is in the new 8.6 rc1?

-Eddy

On Dec 6, 2016, at 11:23 PM, Matthieu Sozeau <mattam AT mattam.org> wrote:

Exactly. The fix is ready :) Thanks!

Le mar. 6 déc. 2016 à 20:21, Eddy Westbrook <westbrook AT galois.com> a écrit :

Matthieu,

Ok, I reported the bug.

It does certainly sound like a good idea to try to remove extra unification algorithms. :)  I imagine the apply unification algorithm is historical, from before Coq had evars?

-Eddy 

On Dec 6, 2016, at 6:27 AM, Matthieu Sozeau <mattam AT mattam.org> wrote:

Hi,

  Indeed, it seems to be a bug in unification somehow (it would be great if you could report it :). 8.6 will come with a mode where typeclass resolution relies on refine instead, alleviating the problem in this case. Note that the plan for 8.7 is to try and remove apply's unification entirely in favor of refine's (it's used in rewrite, destruct/induction as well as other tactics).

-- Matthieu

On Sat, Dec 3, 2016 at 5:26 PM Eddy Westbrook <westbrook AT galois.com> wrote:

All,

I figured Coq was supposed to solve pattern fragment unification problems. So what you are saying is that apply is buggy, and I should use the refine tactic instead?

I guess this explains why typeclass instantiation isn't working for me, since that mostly relies on the apply tactic, right?

Eddy

Sent from my iPhone

On Dec 3, 2016, at 2:37 AM, Matthieu Sozeau <mattam AT mattam.org> wrote:

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
>