The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Samuel,

in general the purpose of ring is to solve goals by using the associativity 
and commutativity laws of one ring. The ring is selected by the type 
parameter of the equality. In your case you need additional lemmas to solve 
the goal, which have nothing to do with associativity or commutativity.
 
The Coq manual states, that the purpose of providing a ring morphism is to 
extend a generally non computational ring with a computational constant type, 
so that constant folding can be done. I would think this only works when the 
provided morphism is computational and not an axiom. It might also be that 
the ring tactic only tries to use the morphism if the respective terms are 
free of variables, which is not the case in your example. Add Ring has a 
"cnstants" option to provide a tactic to judge what a constant is, but I 
don't see how this would help you. So your usage of morphism seems to be a 
stretch.

But there is a way to do it: use the "preprocess" option to Add Ring to apply 
rewrites to convert all Z operators to mword operators like this:

  Add Ring mword_ring :
    (@regRing mword MW) (
       morphism (@ZToReg_morphism mword MW), 
       preprocess [repeat (rewrite ZToReg_morphism.(morph_add) || rewrite 
ZToReg_morphism.(morph_sub) || rewrite ZToReg_morphism.(morph_mul))]
    ).

Best regards,

Michael
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928