Andrej Dudenhefner (Apr 06 2021 at 12:46): Andrej Dudenhefner (Apr 06 2021 at 12:46):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 nat, N, (nonnegative) Z.
Andrej Dudenhefner (Apr 08 2021 at 08:29):@Enrico Tassi do you know the rationale behind math-comp's Lemma modn0 m : m %% 0 = m. (which breaks away from current Coq's m mod 0 = 0 design decision)?
Enrico Tassi (Apr 08 2021 at 08:30):I don't but this question may get a better in asnwer in math-comp users
Enrico Tassi (Apr 08 2021 at 08:31):Would you mind asking on that stream?
Andrej Dudenhefner (Apr 20 2021 at 07:21):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 div, mod lemmas for lia/nia (see follow up PR #14037).
Last updated: Sep 28 2023 at 11:01 UTC