Skip to Content.
Sympa Menu

coq-club - RE: [Coq-Club] how to proof in Z modulo?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

RE: [Coq-Club] how to proof in Z modulo?


Chronological Thread 
  • From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
  • To: "coq-club AT inria.fr" <coq-club AT inria.fr>
  • Subject: RE: [Coq-Club] how to proof in Z modulo?
  • Date: Tue, 9 Aug 2016 11:53:49 +0000
  • Accept-language: de-DE, en-US
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=michael.soegtrop AT intel.com; spf=Pass smtp.mailfrom=michael.soegtrop AT intel.com; spf=None smtp.helo=postmaster AT mga14.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



Archive powered by MHonArc 2.6.18.

Top of Page