From 2c2dabd4f7b7f330cc8e6c9cf879618a422316e8 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 6 Mar 2023 16:37:07 +0100 Subject: Address most deprecation warnings from Coq 8.16 * Define our own `Z_div_mod_eq` lemma The one in the Coq standard library is deprecated since 8.14, but its replacement changed type between 8.13 and 8.14. So the only way to remain compatible from 8.12 to 8.16 is to define our own lemma. Phew. * Do not use `Arith.Max`, deprecated. * Do not use `plus_lt_compat_r`, deprecated. * Do not use `beq_nat_refl` and `beq_nat_true`, deprecated. --- lib/Coqlib.v | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'lib/Coqlib.v') diff --git a/lib/Coqlib.v b/lib/Coqlib.v index 045fb03a..9b8f2abb 100644 --- a/lib/Coqlib.v +++ b/lib/Coqlib.v @@ -406,6 +406,12 @@ Qed. (** Properties of Euclidean division and modulus. *) +Lemma Z_div_mod_eq: forall a b, + b > 0 -> a = (b * (a / b) + a mod b). +Proof. + intros. apply Z.div_mod. lia. +Qed. + Lemma Zmod_unique: forall x y a b, x = a * y + b -> 0 <= b < y -> x mod y = b. -- cgit