The Coq mailing list

[Robbert Krebbers <mailinglists AT robbertkrebbers.nl>]

Hello,

On 03/14/2013 06:52 PM, Ben Lerner wrote:
> Is there a way to write some form of Add Morphism (or Add Parametric
> Morphism) that would let me define the second instance above, allow me
> to "rewrite H", and generate the subgoal of proving "value t1"?
Not that I know of.

The problem in your example is that the premise "value t" of 
"Tm_plus_r2" is not a type class constraint. Hence, when type class 
search is invoked to derive the required morphism for your rewrite, it 
will block at it. Luckily, type class search is based on eauto, and uses 
a special eauto hint database called "typeclass_instances". This allows 
you to add Hints to the database yourself, for example a hint that 
invokes a tactic in case a "value ?x" constraint is encountered.

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