Stream: Coq users

Topic: Consensus on division by zero


view this post on Zulip 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 *)

view this post on Zulip Andrej Dudenhefner (Apr 07 2021 at 12:20):

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.

view this post on Zulip 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)?

view this post on Zulip Enrico Tassi (Apr 08 2021 at 08:30):

I don't but this question may get a better in asnwer in math-comp users

view this post on Zulip Enrico Tassi (Apr 08 2021 at 08:31):

Would you mind asking on that stream?

view this post on Zulip 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: Feb 06 2023 at 13:03 UTC