In `math-comp`

we have `Lemma modn0 m : m %% 0 = m.`

whereas in Coq we have `forall (m: nat), m mod 0 = 0`

. What is the rationale behind this design decision in `math-comp`

?

There are two definitions of division and modulo for `Z`

in the standard library (ones are called `Z.quot`

and `Z.rem`

), and MathComp has its own in `intdiv`

. They all behave differently. When I was implementing mczify, I found this is confusing.

IMO, `Lemma divz_eq m d : m = (m %/ d)%Z * d + (m %% d)%Z`

(and similar one for nat) without condition `d != 0`

make things a bit more uniform. But, I cannot really decide which one is better.

I see, this is also my reasoning for Coq PR #14086. Making it backward compatible is tricky though.

This is the commit where `divz`

and `modz`

are introduced, although it seems difficult to guess what was the point of this design decision. https://github.com/math-comp/mathcomp-history-before-github/commit/58e1b6f3fa8ce65a2f210a192cb19bc23cc44071

BTW, it is really good to know that `(1 mod 0)%N`

reduces to `1%N`

:joy:

Also, `modn m n`

of MathComp is structurally smaller than `m`

thanks to this, and it simplifies the definition of `gcdn`

, IIUC. https://github.com/math-comp/math-comp/blob/f4fb83f19cbe9503f7cfe03ba8217311744e33ac/mathcomp/ssreflect/div.v#L577-L581

Last updated: Jan 29 2023 at 18:03 UTC