2
$\begingroup$

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
$\endgroup$
5
  • 2
    $\begingroup$ 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$. $\endgroup$
    – Henry Cohn
    Nov 29, 2011 at 14:41
  • 1
    $\begingroup$ 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". $\endgroup$ Nov 29, 2011 at 15:18
  • 1
    $\begingroup$ 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$? $\endgroup$
    – joro
    Nov 29, 2011 at 16:24
  • 2
    $\begingroup$ @joro: you're missing the point that Andreas made in his answer. "mod 0" does not have a generally accepted meaning. $\endgroup$ Nov 29, 2011 at 17:39
  • $\begingroup$ 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)). $\endgroup$ Dec 7, 2013 at 15:41

2 Answers 2

8
$\begingroup$

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

$\endgroup$
1
  • $\begingroup$ 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). $\endgroup$ Nov 30, 2011 at 2:39
5
$\begingroup$

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.

$\endgroup$
1
  • $\begingroup$ Even though Coq has dependent types, they are harder / more annoying to use than non-dependent types. Some use-cases really benefit from simply typed total functions. $\endgroup$
    – Ana Borges
    Nov 3, 2021 at 15:25

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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