Andrej Dudenhefner (Apr 08 2021 at 08:37): Andrej Dudenhefner (Apr 08 2021 at 08:37):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?
Kazuhiko Sakaguchi (Apr 08 2021 at 11:23):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.
Andrej Dudenhefner (Apr 08 2021 at 11:25):I see, this is also my reasoning for Coq PR #14086. Making it backward compatible is tricky though.
Kazuhiko Sakaguchi (Apr 08 2021 at 11:47):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:
Kazuhiko Sakaguchi (Apr 08 2021 at 14:54):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