The Coq mailing list

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

Dear Laurent,

> It works but your ring somewhat misses the fact that 3 mod 3 = 0 but 
> applying it twice makes the trick

Indeed, this is the reason why ring doesn't work as I expected. If all the 
mod's are removed we have:

x = x - (- x) - ((- x) - x)
x  = x + x + x + x

which is not true in arbitrary rings, only in this specific ring.

It might help to define the multiply operator as ((a mod m) * (b mod m)) mod 
m. I think ring simplifies x+x+x+x to 4*x which then should be trivially 
simplified to 1*x. With the operators defined as is, this is less trivial to 
see. I ask Valentin to try this. 

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