The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 12/02/2016 03:50 PM, Eddy Westbrook wrote:
> Hi Jonathan,
>
> Thanks for the reply, and for the suggested workaround. I’ll see if I can get 
> something like that to work.
>
> The reason this looks like a bug to me, though, is that I think, if I’m not 
> mistaken, that what I am actually trying solve is the problem
>
> ?T2 x = ?B

FYI - You can "skolemize" ?T2 with respect to x in the goal by doing this:

Goal { T:Type | T=T }.
  refine (exist _ (forall (x:?[T1]), ?[T2]) _).
  instantiate (T2:=ltac:(revert x)). (*skolemize ?T2 wrt x*)

> (Technically, I think Coq writes the left-hand side as something like 
> ?T2@{__:=x}, but it’s the same thing.) This problem has the solution ?T2 = (fun 
> _ => ?B). It falls into the higher-order pattern fragment, since ?T2 is fully 
> applied to distinct bound variables, and I thought Coq would solve this fragment.

I don't think Coq can solve such fragments.

> Also, either way, the fact that the unify tactic is not commutative also 
> seems like a bug...

I think the problems with commutativity of unification with evars is a 
known issue that Hugo has attempted to (and is continuing to attempt to) 
deal with.

-- Jonathan