Welcome to MathOverflow

Question

1

The proof assistants Coq and Isabelle give conflicting formal proofs about $a \mod 0 \qquad \forall a \in \mathbb{Z}$.

According to Coq $$ a \mod 0 = 0$$ and Isabelle proves $$ a \mod = a$$

mod is the function, not a congruence.

Which way is it?

All the computer algebra systems I tried give an error in this case.

Can one derive a counter intuitive statement from the above results?

Both agree that integer division by $0$ is $0$ forall $\mathbb{Z}$.

Coq proof:

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.

Isabelle proof:

theory mod0
imports Main 
begin
lemma mod0: " \<forall> n \<in> \<int>. n mod (0::int) = n" 
by auto

flag	asked Nov 29 2011 at 14:28 joro 4,230●1●10●31

	In there any other interpretation for these conflicting formal proofs than conflicting formal definitions? I don't think there's a standard definition for what the mod function means. I'd be inclined to define $a \mod 0$ as $a$, on the grounds that $a \mod b$ should be a representative for the image of $a$ in $\mathbb{Z}/b\mathbb{Z}$. I don't know if there's an equally compelling reason to define it as $0$. – Henry Cohn Nov 29 2011 at 14:41
	What Henry said. It is a matter of definition, so different proof systems (and different textbooks, different CASs) may have different definitions. It is nothing to do with "conflicting formal proofs". – Gerald Edgar Nov 29 2011 at 15:18
	Henry, Gerald, I see your point. But "mod" has more or less generally accepted meaning (there is an answer to the question). Should I wonder what the provers mean by $\mathbb{Z}$ or `int` or $2+2$? – joro Nov 29 2011 at 16:24
	@joro: you're missing the point that Andreas made in his answer. "mod 0" does not have a generally accepted meaning. – Thierry Zell Nov 29 2011 at 17:39

Andreas Blass · Accepted Answer · 2011-11-29 14:51:49Z UTC

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.)

How to interpret conflicting formal proofs about “a mod 0 = ? ”

Remember to vote up questions/answers you find interesting or helpful (requires 15 reputation points)

1 Answer

You can accept an answer to one of your own questions by clicking the check mark next to it. This awards 15 reputation points to the person who answered and 2 reputation points to you.