The Coq mailing list

[Michael Shulman <mshulman AT ucsd.edu>]

Hi Matthieu,

Thank you very much!  I'm glad to hear at least that there is a
rational explanation.  (-:

Best,
Mike

On Fri, Nov 25, 2011 at 01:16, Matthieu Sozeau
<matthieu.sozeau AT gmail.com>
 wrote:
>
> 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