Unification failure applying generic theorem

[RandomActsOfGrammar]

It seems there is a problem unifying the premises of generic theorems when those premises contain implications.

Suppose we have these definitions:

Kind pair   type -> type -> type.
Type pair   A -> B -> pair A B.

Kind ground   type. /*Just a basic type to use*/

Define append : list A -> list A -> list A -> prop by
append nil L L;
append (X::L1) L2 (X::L3) := append L1 L2 L3.

Define lookup : list (pair A B) -> A -> B -> prop by
lookup (pair A B::Rest) A B;
lookup (pair X Y::Rest) A B :=
  (X = A -> false) /\ lookup Rest A B.

We can prove a theorem about these for lists containing the ground type and use it fine:

Theorem vars_equiv_left :
  forall (G1 : list (pair ground ground)) G2 D D1 D2,
    (forall X U1 U2, member X D -> lookup G1 X U1 ->
                     lookup G2 X U2 -> U1 = U2) ->
    append D1 D2 D ->
    (forall X U1 U2, member X D1 -> lookup G1 X U1 ->
                     lookup G2 X U2 -> U1 = U2).
skip.

Theorem x :
  forall (G1 : list (pair ground ground)) G2 D D2 D3,
    (forall X U1 U2, member X D -> lookup G1 X U1 ->
                     lookup G2 X U2 -> U1 = U2) ->
    append D2 D3 D ->
    (forall X U1 U2, member X D2 -> lookup G1 X U1 ->
                     lookup G2 X U2 -> U1 = U2).
intros Equiv App Mem Lkp1 Lkp2.
apply vars_equiv_left to Equiv App.
apply H1 to Mem Lkp1 Lkp2. search.

However, if we prove a generic version of vars_equiv_left and try to use it in the same theorem, we have a problem:

Theorem vars_equiv_left [A, B] :
  forall (G1 : list (pair A B)) G2 D D1 D2,
    (forall X U1 U2, member X D -> lookup G1 X U1 ->
                     lookup G2 X U2 -> U1 = U2) ->
    append D1 D2 D ->
    (forall X U1 U2, member X D1 -> lookup G1 X U1 ->
                     lookup G2 X U2 -> U1 = U2).
skip.

Theorem x :
  forall (G1 : list (pair ground ground)) G2 D D2 D3,
    (forall X U1 U2, member X D -> lookup G1 X U1 ->
                     lookup G2 X U2 -> U1 = U2) ->
    append D2 D3 D ->
    (forall X U1 U2, member X D2 -> lookup G1 X U1 ->
                     lookup G2 X U2 -> U1 = U2).
intros Equiv App. apply vars_equiv_left to Equiv App.

This gives us the following error message:

Error: While matching argument #1:
Unification failure

[chaudhuri]

Not sure if this is a bug. Schematic theorems will have to be applied with explicit type instances as far as I recall. For instance, replacing your apply vars_equiv_left with this will not trigger the unification failure:

apply vars_equiv_left[ground, ground] to Equiv App.

Am I missing something? (Also, the schematic polymorphism code comes from @yvting, so he may have some insights.)

[RandomActsOfGrammar]

It seems to me that it should find the type instances from the application. In the Equiv hypothesis, G1 and G2 are known to have type list (pair ground ground). Then unifying the Equiv and the first premise of vars_equiv_left seems that it should work and fill the type instances.

In an example without an implication, it can find the type instances:

Theorem append_unique [A] : forall (L1 : list A) L2 L L',
  append L1 L2 L -> append L1 L2 L' -> L = L'.
skip.

Theorem append_ground : forall (L1 : list ground) L2 L L',
  append L1 L2 L -> append L1 L2 L' -> L = L'.
intros App1 App2. apply append_unique to App1 App2. search.

Even though we don't give the type instance for append_unique, it succeeds in the application.

[chaudhuri]

Interesting. Thanks for the report. Fixing now...

[chaudhuri]

Can you try this potential fix that I just committed? It addresses this particular corner case of unification of formulas but I'm not sure if it breaks other things. May back it out if there are regressions.

[RandomActsOfGrammar]

The fix seems to work for me.

[chaudhuri]

OK great. Holler if you discover anything broken and will reopen this issue.