Proof Assistants Stack Exchange is a question and answer site for mathematicians and computer scientists who develop and use proof assistants. It only takes a minute to sign up.
Sign up to join this community
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).
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 = nuniformly fornat,N,Z,int63,sint63,int31such thatm = (m / n) * n + (m mod n)holds (also forn = 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.
