## Stream: math-comp users

### Topic: m %% 0 = m

#### 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