I'm trying to find the discussion on division by zero mentioned in #11447.
My main concern is the design decision leading to the incoherence
Compute (1 mod 0)%nat. (* = 0%nat : nat *) Compute (1 mod 0)%Z. (* = 0%Z : Z *) Compute (1 mod 0)%N. (* = 1%N : N *)
Annoyed by the glue code / superfluous assumptions I created PR #14086 to address the described issue. Now computation is uniform and we have
n = (n / m) * m + (n mod m) in
@Enrico Tassi do you know the rationale behind
Lemma modn0 m : m %% 0 = m. (which breaks away from current Coq's
m mod 0 = 0 design decision)?
I don't but this question may get a better in asnwer in math-comp users
Would you mind asking on that stream?
For those who are interested: the PR #14086 (for uniform modulo treatment) is ready, requiring maintainers review/approval. Once accepted, we can have a uniform
mod lemmas for
nia (see follow up PR #14037).
Last updated: Sep 28 2023 at 11:01 UTC