I noticed that Coq 8.15 (possibly 8.14) made some significant changes to divmod. In particular, Nat.divmod_0q0 seems to have been removed and the div_mod lemma with signature y<>0 -> x = y*(x/y) + x mod y has effectively been replaced with div_mod_eq which drops the y<>0 precondition.

Does divmod (and hence div and mod) now behave differently? Could somebody summarize the changes? It looks like some 8.15 theorems simply don't hold in 8.13 and vice-versa (with Nat.divmod_0q0).


1 Answer 1


This was changed in Coq 8.14 (MR: https://github.com/coq/coq/pull/14086), and the changes are summarized in https://coq.inria.fr/refman/changes.html#id310. Quoting:

Changed: set n mod 0 = n uniformly for nat, N, Z, int63, sint63, int31 such that m = (m / n) * n + (m mod n) holds (also for n = 0)

As you can see, in many cases this gives stronger theorems with fewer side conditions — but in any case they're more uniform across nat, N and Z.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.