Hi everyone, pardon me if it sounds stupid, but I am curious about use case of these two lemmas [1].

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.

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.

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.