The Coq mailing list

[Ben Lerner <blerner AT cs.brown.edu>]

On 3/14/2013 2:13 PM, Robbert Krebbers wrote:
> ...
>
> I think the following will make your "Tm_plus_r2" instance work.
>
> Hint Extern 100 (value _) => constructor : typeclass_instances.
>
> Of course, instead of "constructor", you could write arbitrary tactics.
> But keep in mind that if you are not careful, it may make things quite 
> slow (or even loop).
>
> Cheers,
>
> Robbert

That hint indeed works in this case, thanks!  Small variants on it work 
in a few more cases: (assumption || (econstructor; eauto) || eauto).  
This certainly suffices for the case where I have an assumption H : 
value t1, instead of knowing it's (C n) and hence constructor is 
enough...  So the recipe here seems to be, know in advance what the 
preconditions of your morphisms are, get them into the context, and add 
a Hint ... => assumption to resolve them. That's not too bad, but it is 
forward-only reasoning, though.

So now I'm curious: could there be a backward-reasoning friendly way to 
do this?  Searching a bit for information about the typeclass_instances 
hint database, I found out I could I could turn on debug-printing of the 
search done by typeclass resolution.  In this case, I get

1.1: apply Tm_plus_2_Proper on
(Proper (stepmany ==> ?5332) (P t1))
1.1.1.1: (*external*) assumption   on
(value t1)
no backtrack on (value t1) after normevars
no backtrack on (value t1) after apply Tm_plus_2_Proper
2.1: apply trans_co_eq_inv_impl_morphism on
(Proper (stepmany ==> ?5335 ==> Basics.flip Basics.impl) stepmany)
.......

Looking at that first line, though, is intriguing: it uses apply, rather 
than eapply.  It seems like rewriting would work if it used eapply, even 
if I *didn't* have the Hint suggested above.  Would using eapply, 
though, cause too many spurious matches of candidate morphisms to 
succeed?  Or might there be a Hint form that typeclass resolution could 
take, to tell it that it's ok to leave some goals unproven after normevars?