Hi everyone, pardon me if it sounds stupid, but I am curious about use case of these two lemmas .
Lemma Zmod_0_r: forall a, a mod 0 = 0.
Lemma Zdiv_0_r: forall a, a/0 = 0.
My question is why do we have these lemma in first place ? Are not these operations undefined when divisor is 0. According to me, it would make more sense when performing these operations we should have a precondition to make sure that divisor in not zero.
On the choice of having set the value of
a mod 0 and
a / 0 to
0, there is some related discussion here: https://discourse.elm-lang.org/t/integer-division-by-zero/2923
I agree with you that I don’t like to see these lemmas in the standard library. I would prefer if we could make it like these values are undefined, but this is actually useful to have some lemmas that apply for all values, and not just for non-null values, because it will be easier for automation to use them. The file that you mentioned uses this heavily.
Here is some rationalization.
it is not possible to construct a partially defined function in Coq. So when defining the division and
mod function with type
Z -> Z -> Z, you need to cover the case when the second argument is 0. The simplest choice was to say that in this case both division and
mod return 0, even though in conventional mathematics they would be undefined.
Once you ave chosen this behaviour, the two lemmas above are provable and therefore they are included among the results.
So in fact the division and mod function that are used in the library are “extended division” and “extended modulo”. The two statements you are citing actually are statements about “extended division” and “extended mod”.
Coming from conventional mathematics, the cost of having a slightly different definition of division and modulo is low, because when you write a formula that contains division and modulo in conventional mathematics it is your responsibility to check that no division by 0 occurs in the formula. But if no division by 0 occurs, then the value of the “extended division” and the “extended mod” coincide with their conventional counterparts, so that your formula has the same meaning. So the meaning of every formula that would be admissible in conventional mathematics is preserved.
If you write a formula that does not contain any division or modulo, the meaning of this formula is the same in Coq and in conventional mathematics. If you prove this formula using a division and a modulo operation, the validity of your proof is not compromised, because “division” and “modulo” are only conventional names. The proof verification by Coq is not compromised, because the exact definition is used at every step of the proof (not the conventional definition with its more limited range). So if your proof is a conventional proof, everywhere a division is used, you needed to check that the division was licit. In Coq, the check was not made, but the value is used consistently with the definition of “extended division”, which happens to the same as the “conventional division” and the same value is used so nothing is compromised.
You might think that the proof obtained is weaker, but it is not the case, because the check whether division by zero occurs is actually made in the definition of “extended division” and the Coq system check that in this case whatever formula you prove about the result of division is also provable when the second input is zero and the output is also zero. So in fact, more information has been formally verified.
The same occurs with natural number and subtraction.
The theory of wheels is a possible solution to the problem of division by zero: