Take the 2-minute tour ×
MathOverflow is a question and answer site for professional mathematicians. It's 100% free, no registration required.

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
share|improve this question
2  
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
1  
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
1  
@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

2 Answers 2

up vote 9 down vote accepted

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

share|improve this answer
    
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.

share|improve this answer

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.