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
There are two definitions of division and modulo for
Z in the standard library (ones are called
Z.rem), and MathComp has its own in
intdiv. They all behave differently. When I was implementing mczify, I found this is confusing.
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
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
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