How to interpret conflicting formal proofs about "a mod 0 = ? " - MathOverflow most recent 30 from http://mathoverflow.net 2013-05-19T15:05:02Z http://mathoverflow.net/feeds/question/82181 http://www.creativecommons.org/licenses/by-nc/2.5/rdf http://mathoverflow.net/questions/82181/how-to-interpret-conflicting-formal-proofs-about-a-mod-0 How to interpret conflicting formal proofs about "a mod 0 = ? " joro 2011-11-29T14:28:06Z 2011-11-29T14:51:49Z <p>The proof assistants Coq and Isabelle give conflicting formal proofs about $a \mod 0 \qquad \forall a \in \mathbb{Z}$.</p> <p>According to Coq $$a \mod 0 = 0$$ and Isabelle proves $$a \mod = a$$</p> <p><code>mod</code> is the function, not a congruence.</p> <blockquote> <p>Which way is it?</p> </blockquote> <p>All the computer algebra systems I tried give an error in this case.</p> <p>Can one derive a counter intuitive statement from the above results?</p> <p>Both agree that integer division by $0$ is $0$ forall $\mathbb{Z}$.</p> <p>Coq proof:</p> <pre><code>Require Import ZArith. Require Import Coq.ZArith.Znumtheory. Open Scope Z_scope. Lemma mod0: forall n:Z, n mod 0 = 0. apply Zmod_0_r. Qed. </code></pre> <p>Isabelle proof:</p> <pre><code>theory mod0 imports Main begin lemma mod0: " \&lt;forall&gt; n \&lt;in&gt; \&lt;int&gt;. n mod (0::int) = n" by auto </code></pre> http://mathoverflow.net/questions/82181/how-to-interpret-conflicting-formal-proofs-about-a-mod-0/82182#82182 Answer by Andreas Blass for How to interpret conflicting formal proofs about "a mod 0 = ? " Andreas Blass 2011-11-29T14:51:49Z 2011-11-29T14:51:49Z <p>If $a$ mod 0 is to be defined at all (and I'm not entirely convinced that it should be), then it ought to differ from $a$ by a multiple of 0, which means to me that it ought to be $a$. But it's asserted in the question that the computer systems have a strange notion of division by 0, so they might think that everything is a multiple of 0. In this alternative "reality", everything is congruent to everything else modulo 0; so if you define $a$ mod $b$ as the smallest non-negative integer congruent to $a$ modulo $b$, then $a$ mod 0 would be 0. Personally, I refuse to buy into this alternative reality; congruence modulo 0 should mean equality. (Fortunately, I rarely use computer algebra systems, and I have never yet asked one about divisibility by 0.)</p>