The Coq mailing list

[Matthieu Sozeau <matthieu.sozeau AT gmail.com>]

Le 25 nov. 2011 à 05:34, Michael Shulman a écrit :

> I have managed to extract a fairly small example which exhibits the
> behavior I mentioned.  There are no typeclasses or coercions.
> 
> ~~~
> 
> Definition compose {A B C} (g : B -> C) (f : A -> B) (x : A) := g (f x).
> 
> Axiom reflect : Type -> Type.
> Axiom reflect_factor : forall {X Y}, (X -> Y) -> (reflect X -> Y).
> Axiom map_to_reflect : forall X, X -> reflect X.
> 
> Definition reflect_functor {X Y} (f : X -> Y) : reflect X -> reflect Y
>  := reflect_factor (compose (map_to_reflect Y) f).
> 
> Axiom reflect_factoriality : forall {X Y Z} (g : Y -> Z) (f : X -> Y)
> (rx : reflect X),
>  (reflect_factor g (reflect_functor f rx)) = (reflect_factor (compose g f) 
> rx).
> 
> Definition reflect_functoriality {X Y Z} (g : Y -> Z) (f : X -> Y) (rx
> : reflect X) :
>  (reflect_functor g (reflect_functor f rx)) = (reflect_functor
> (compose g f) rx).
> Proof.
>  apply @reflect_factoriality.
> Defined.
> 
> ~~~
> 
> In the proof above, "apply reflect_factoriality" fails with the
> message 'Error: Impossible to unify "Y" with "Z".' whereas "apply
> @reflect_factoriality" succeeds.  Can anyone explain the difference?

Hi Michael,

It's for a fairly bad reason due to the design of the unifier for tactics.
Here's the long technical explanation:

It has two kinds of metavariables: metas and existentials. When writing
[apply reflect_factoriality], the {X Y Z} are turned into existentials,
but when writing [apply @reflect_factoriality], they are turned into
metavariables. Coq tries first to unify the left-hand side of the equalities,
it succeeds in both cases, finding instances of X, Y and Z. However it
does not instantiate the existentials or metavariables just yet, it keeps
them as a substitution, to be merged later. 

In the first case, it unifies the right-hand side and finds different
instances for X, Y, and Z (unfolding reflect_functor and using first-order 
unification). Merging fails trying to equate Y and Z (and doesn't backtrack).
In the second case, it optimizes by substituting the meta substitution
and using the kernel conversion to equate the (now closed) right-hand sides:

  @reflect_factor X (reflect Z)
    (@compose X Y (reflect Z) (@compose Y Z (reflect Z) (map_to_reflect Z) g)
       f) rx
and

  @reflect_functor X Z (@compose X Y Z g f) rx

These are convertible, so the algorithm succeeds.

>> ?  I have encountered a few situations where the former fails but the
>> latter succeeds.  This confuses me, because in both cases all the
>> arguments of lemma (implicit or non-implicit) have to be deduced from
>> context.  Is the first one somehow trying to guess the implicit
>> arguments too soon or without enough information?

Rather the first one guesses too late, while the second one uses the current
unification information early enough. We're in the process of making this 
more 
uniform and also merge the unification algorithm used in tactics with
the one used for typechecking and [refine]:
[refine (reflect_factoriality _ _ _)] also works, and uses only existentials.

-- Matthieu