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

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

-
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 '11 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 '11 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 '11 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 '11 at 17:39
If you'd prefer, you can still define mod in a more traditional way: div_mod : forall n1 n2, n2 > 0 -> {p1 | p1 = (n3, n4) -> n1 = n3 * n2 + n4 /\ n4 < n2}. The difference between exists x1, p1 x1 and {x1 | p1 x1} is that the first is a Prop and the second is a Set or Type. Definition mod : forall n1 n2, n2 > 0 -> nat * nat := fun n1 n2 h1 => snd (proj1_sig (div_mod n1 n2 h1)). –  Rui Baptista Dec 7 '13 at 15:41

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

-
You don't really need to divide by 0. a and b are congruent mod n means b-a is a multiple of n. For n=0 this just means a and b are equal as Andreas has pointed out. This is is the generally accepted meaning of mod 0 and it is the meaning used in any ring. It makes no sense to interpret a mod 0 as 0 (unless a=0). –  David Wehlau Nov 30 '11 at 2:39

In the logic of Isabelle/HOL, nothing can be undefined. For a partial function such as division, the best we can do is complete the definitions in the most plausible manner, retaining as many well-known facts as possible (preferably unconditionally). Defining division such that x/0=0 (for integers, reals, etc.) works quite well. The Isabelle definitions also ensure that

"a div b * b + a mod b = a"

holds unconditionally.

Coq has dependent types, and in principle the type of div and mod could ensure that the second argument was nonzero. I don't know why this is not done.

-