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.

5 files changed, 18 insertions, 13 deletions

diff --git a/cfrontend/SimplExprproof.v b/cfrontend/SimplExprproof.v
index 2aed0cdf..04afe4da 100644
--- a/cfrontend/SimplExprproof.v
+++ b/cfrontend/SimplExprproof.v
@@ -1974,7 +1974,7 @@ Ltac NOTIN :=
   exploit tr_simple_rvalue; eauto. simpl; intro SL1.
   subst sl0; simpl Kseqlist.
   econstructor; split.
-  right; split. apply star_refl. simpl. apply plus_lt_compat_r.
+  right; split. apply star_refl. simpl. apply Nat.add_lt_mono_r.
   apply (leftcontext_size _ _ _ H). simpl. lia.
   econstructor; eauto. apply S.
   eapply tr_expr_monotone; eauto.
@@ -1996,7 +1996,7 @@ Ltac NOTIN :=
   auto.
 + (* for effects *)
   econstructor; split.
-  right; split. apply star_refl. simpl. apply plus_lt_compat_r.
+  right; split. apply star_refl. simpl. apply Nat.add_lt_mono_r.
   apply (leftcontext_size _ _ _ H). simpl. lia.
   econstructor; eauto.
   exploit tr_simple_rvalue; eauto. simpl. intros A. subst sl1.
diff --git a/common/Memdata.v b/common/Memdata.v
index 1bd87169..7622cab3 100644
--- a/common/Memdata.v
+++ b/common/Memdata.v
@@ -426,7 +426,7 @@ Lemma check_inj_value:
 Proof.
   induction n; simpl. auto.
   unfold proj_sumbool. rewrite dec_eq_true. rewrite dec_eq_true.
-  rewrite <- beq_nat_refl. simpl; auto.
+  rewrite Nat.eqb_refl. simpl; auto.
 Qed.
 
 Lemma proj_inj_value:
@@ -719,7 +719,7 @@ Proof.
   {
     induction n; destruct mvs; simpl; intros; try discriminate.
     contradiction.
-    destruct m; try discriminate. InvBooleans. apply beq_nat_true in H4. subst.
+    destruct m; try discriminate. InvBooleans. apply Nat.eqb_eq in H4. subst.
     destruct H0. subst mv. exists n0; split; auto. lia.
     eapply IHn; eauto. lia.
   }
@@ -738,7 +738,7 @@ Proof.
     destruct (quantity_eq q q0); auto.
     destruct (Nat.eqb sz n) eqn:EQN; auto.
     destruct (check_value sz v q mvl) eqn:CHECK; auto.
-    simpl. apply beq_nat_true in EQN. subst n q0. constructor. auto.
+    simpl. apply Nat.eqb_eq in EQN. subst n q0. constructor. auto.
     destruct H0 as [E|[E|[E|E]]]; subst chunk; destruct q; auto || discriminate.
     congruence.
     intros. eapply B; eauto. lia.
@@ -797,9 +797,9 @@ Lemma check_value_inject:
 Proof.
   induction 1; intros; destruct n; simpl in *; auto.
   inv H; auto.
-  InvBooleans. assert (n = n0) by (apply beq_nat_true; auto). subst v1 q0 n0.
+  InvBooleans. assert (n = n0) by (apply Nat.eqb_eq; auto). subst v1 q0 n0.
   replace v2 with v'.
-  unfold proj_sumbool; rewrite ! dec_eq_true. rewrite <- beq_nat_refl. simpl; eauto.
+  unfold proj_sumbool; rewrite ! dec_eq_true. rewrite Nat.eqb_refl. simpl; eauto.
   inv H2; try discriminate; inv H4; congruence.
   discriminate.
 Qed.
diff --git a/common/Switch.v b/common/Switch.v
index 70d1da15..23f9dd3e 100644
--- a/common/Switch.v
+++ b/common/Switch.v
@@ -271,7 +271,7 @@ Lemma validate_jumptable_correct_rec:
 Proof.
   induction tbl; simpl; intros.
 - unfold list_length_z in H0. simpl in H0. extlia.
-- InvBooleans. rewrite list_length_z_cons in H0. apply beq_nat_true in H1.
+- InvBooleans. rewrite list_length_z_cons in H0. apply Nat.eqb_eq in H1.
   destruct (zeq v 0).
   + replace (base + v) with base by lia. congruence.
   + replace (base + v) with (Z.succ base + Z.pred v) by lia.
@@ -308,13 +308,13 @@ Proof.
   intros default v VRANGE. induction t; simpl; intros until hi.
 - (* base case *)
   destruct cases as [ | [key1 act1] cases1]; intros.
-+ apply beq_nat_true in H. subst act. reflexivity.
-+ InvBooleans. apply beq_nat_true in H2. subst. simpl.
++ apply Nat.eqb_eq in H. subst act. reflexivity.
++ InvBooleans. apply Nat.eqb_eq in H2. subst. simpl.
   destruct (zeq v hi). auto. extlia.
 - (* eq node *)
   destruct (split_eq key cases) as [optact others] eqn:EQ. intros.
   destruct optact as [act1|]; InvBooleans; try discriminate.
-  apply beq_nat_true in H.
+  apply Nat.eqb_eq in H.
   rewrite (split_eq_prop v default _ _ _ _ EQ).
   destruct (zeq v key).
   + congruence.
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.
diff --git a/lib/Iteration.v b/lib/Iteration.v
index 34471826..50672069 100644
--- a/lib/Iteration.v
+++ b/lib/Iteration.v
@@ -204,7 +204,6 @@ End PrimIter.
 
 Require Import Classical.
 Require Import ClassicalDescription.
-Require Import Max.
 
 Module GenIter.
 
@@ -280,7 +279,7 @@ Lemma converges_to_unique:
 Proof.
   intros a b [n C] b' [n' C'].
   rewrite <- (C (max n n')). rewrite <- (C' (max n n')). auto.
-  apply le_max_r. apply le_max_l.
+  apply Nat.le_max_r. apply Nat.le_max_l.
 Qed.
 
 Lemma converges_to_exists_uniquely: