lib/Coqlib.v: remove defns about multiplication, division, modulus

Instead, use definitions and lemmas from the Coq standard library
(ZArith, Znumtheory).

5 files changed, 22 insertions, 20 deletions

diff --git a/backend/Inliningproof.v b/backend/Inliningproof.v
index 2dcb8956..45051bcf 100644
--- a/backend/Inliningproof.v
+++ b/backend/Inliningproof.v
@@ -755,13 +755,13 @@ Proof.
   assert (2 <= sz -> (2 | n)). intros.
     destruct (zle sz 1). omegaContradiction.
     destruct (zle sz 2). auto.
-    destruct (zle sz 4). apply Zdivides_trans with 4; auto. exists 2; auto.
-    apply Zdivides_trans with 8; auto. exists 4; auto.
+    destruct (zle sz 4). apply Z.divide_trans with 4; auto. exists 2; auto.
+    apply Z.divide_trans with 8; auto. exists 4; auto.
   assert (4 <= sz -> (4 | n)). intros.
     destruct (zle sz 1). omegaContradiction.
     destruct (zle sz 2). omegaContradiction.
     destruct (zle sz 4). auto.
-    apply Zdivides_trans with 8; auto. exists 2; auto.
+    apply Z.divide_trans with 8; auto. exists 2; auto.
   assert (8 <= sz -> (8 | n)). intros.
     destruct (zle sz 1). omegaContradiction.
     destruct (zle sz 2). omegaContradiction.
diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v
index fc163719..55fa7a67 100644
--- a/backend/Lineartyping.v
+++ b/backend/Lineartyping.v
@@ -39,7 +39,7 @@ Definition slot_valid (sl: slot) (ofs: Z) (ty: typ): bool :=
   | Outgoing => zle 0 ofs
   | Incoming => In_dec Loc.eq (S Incoming ofs ty) (regs_of_rpairs (loc_parameters funct.(fn_sig)))
   end
-  && Zdivide_dec (typealign ty) ofs (typealign_pos ty).
+  && Zdivide_dec (typealign ty) ofs.
 
 Definition slot_writable (sl: slot) : bool :=
   match sl with
diff --git a/backend/SelectDivproof.v b/backend/SelectDivproof.v
index 9e24857a..e660677a 100644
--- a/backend/SelectDivproof.v
+++ b/backend/SelectDivproof.v
@@ -57,13 +57,13 @@ Proof.
     apply Z.mul_nonneg_nonneg; omega.
   assert (k * n <= two_p (N + l) - two_p l).
     apply Z.le_trans with (two_p l * n).
-    apply Zmult_le_compat_r. omega. omega.
+    apply Z.mul_le_mono_nonneg_r; omega.
     replace (N + l) with (l + N) by omega.
     rewrite two_p_is_exp.
     replace (two_p l * two_p N - two_p l)
        with (two_p l * (two_p N - 1))
          by ring.
-    apply Zmult_le_compat_l. omega. exploit (two_p_gt_ZERO l). omega. omega.
+    apply Z.mul_le_mono_nonneg_l. omega. exploit (two_p_gt_ZERO l). omega. omega.
     omega. omega.
   assert (0 <= two_p (N + l) * r).
     apply Z.mul_nonneg_nonneg.
@@ -72,7 +72,7 @@ Proof.
   assert (two_p (N + l) * r <= two_p (N + l) * d - two_p (N + l)).
     replace (two_p (N + l) * d - two_p (N + l))
        with (two_p (N + l) * (d - 1)) by ring.
-    apply Zmult_le_compat_l.
+    apply Z.mul_le_mono_nonneg_l. 
     omega.
     exploit (two_p_gt_ZERO (N + l)). omega. omega.
   assert (0 <= m * n - two_p (N + l) * q).
@@ -138,13 +138,13 @@ Proof.
   rewrite H2.
   assert (k * n <= two_p (N + l)).
     rewrite Z.add_comm. rewrite two_p_is_exp; try omega.
-    apply Z.le_trans with (two_p l * n). apply Zmult_le_compat_r. omega. omega.
-    apply Zmult_le_compat_l. omega. exploit (two_p_gt_ZERO l). omega. omega.
+    apply Z.le_trans with (two_p l * n). apply Z.mul_le_mono_nonneg_r; omega.
+    apply Z.mul_le_mono_nonneg_l. omega. exploit (two_p_gt_ZERO l). omega. omega.
   assert (two_p (N + l) * r <= two_p (N + l) * d - two_p (N + l)).
     replace (two_p (N + l) * d - two_p (N + l))
        with (two_p (N + l) * (d - 1))
          by ring.
-    apply Zmult_le_compat_l. omega. exploit (two_p_gt_ZERO (N + l)). omega. omega.
+    apply Z.mul_le_mono_nonneg_l. exploit (two_p_gt_ZERO (N + l)). omega. omega. omega.
   omega.
 Qed.
 
@@ -246,10 +246,11 @@ Proof.
   unfold Int.max_signed; omega.
   apply Zdiv_interval_1. generalize Int.min_signed_neg; omega. apply Int.half_modulus_pos.
   apply Int.modulus_pos.
-  split. apply Z.le_trans with (Int.min_signed * m). apply Zmult_le_compat_l_neg. omega. generalize Int.min_signed_neg; omega.
-  apply Zmult_le_compat_r. unfold n; generalize (Int.signed_range x); tauto. tauto.
+  split. apply Z.le_trans with (Int.min_signed * m). 
+  apply Z.mul_le_mono_nonpos_l. generalize Int.min_signed_neg; omega. omega.
+  apply Z.mul_le_mono_nonneg_r. omega. unfold n; generalize (Int.signed_range x); tauto.
   apply Z.le_lt_trans with (Int.half_modulus * m).
-  apply Zmult_le_compat_r. generalize (Int.signed_range x); unfold n, Int.max_signed; omega. tauto.
+  apply Z.mul_le_mono_nonneg_r. tauto. generalize (Int.signed_range x); unfold n, Int.max_signed; omega.
   apply Zmult_lt_compat_l. generalize Int.half_modulus_pos; omega. tauto.
   assert (32 < Int.max_unsigned) by (compute; auto). omega.
   unfold Int.lt; fold n. rewrite Int.signed_zero. destruct (zlt n 0); apply Int.eqm_unsigned_repr.
@@ -290,7 +291,7 @@ Proof.
   apply Int.eqm_sym. eapply Int.eqm_trans. apply Int.eqm_signed_unsigned.
   apply Int.eqm_unsigned_repr_l. apply Int.eqm_refl2.
   apply (f_equal (fun x => n * x / Int.modulus)).
-  rewrite Int.signed_repr_eq. rewrite Zmod_small by assumption.
+  rewrite Int.signed_repr_eq. rewrite Z.mod_small by assumption.
   apply zlt_false. assumption.
 Qed.
 
@@ -400,8 +401,9 @@ Proof.
   unfold Int64.max_signed; omega.
   apply Zdiv_interval_1. generalize Int64.min_signed_neg; omega. apply Int64.half_modulus_pos.
   apply Int64.modulus_pos.
-  split. apply Z.le_trans with (Int64.min_signed * m). apply Zmult_le_compat_l_neg. omega. generalize Int64.min_signed_neg; omega.
-  apply Zmult_le_compat_r. unfold n; generalize (Int64.signed_range x); tauto. tauto.
+  split. apply Z.le_trans with (Int64.min_signed * m).
+  apply Z.mul_le_mono_nonpos_l. generalize Int64.min_signed_neg; omega. omega.
+  apply Z.mul_le_mono_nonneg_r. tauto. unfold n; generalize (Int64.signed_range x); tauto.
   apply Z.le_lt_trans with (Int64.half_modulus * m).
   apply Zmult_le_compat_r. generalize (Int64.signed_range x); unfold n, Int64.max_signed; omega. tauto.
   apply Zmult_lt_compat_l. generalize Int64.half_modulus_pos; omega. tauto.
@@ -444,7 +446,7 @@ Proof.
   apply Int64.eqm_sym. eapply Int64.eqm_trans. apply Int64.eqm_signed_unsigned.
   apply Int64.eqm_unsigned_repr_l. apply Int64.eqm_refl2.
   apply (f_equal (fun x => n * x / Int64.modulus)).
-  rewrite Int64.signed_repr_eq. rewrite Zmod_small by assumption.
+  rewrite Int64.signed_repr_eq. rewrite Z.mod_small by assumption.
   apply zlt_false. assumption.
 Qed.
 
diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v
index afc470b3..621459d0 100644
--- a/backend/Selectionproof.v
+++ b/backend/Selectionproof.v
@@ -506,7 +506,7 @@ Proof.
   unfold Int.sub. rewrite Int.unsigned_repr_eq. f_equal. f_equal.
   apply Int.unsigned_repr. unfold Int.max_unsigned; omega.
 - intros until i0; intros EVAL R. exists v; split; auto.
-  inv R. rewrite Zmod_small by (apply Int.unsigned_range). constructor.
+  inv R. rewrite Z.mod_small by (apply Int.unsigned_range). constructor.
 - constructor.
 - apply Int.unsigned_range.
 Qed.
diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v
index 37a9ecf2..47b87bfb 100644
--- a/backend/ValueDomain.v
+++ b/backend/ValueDomain.v
@@ -1492,12 +1492,12 @@ Proof.
   inv H; auto with va.
 - apply vmatch_uns. red; intros. rewrite Int.bits_rol by auto.
   generalize (Int.unsigned_range n); intros.
-  rewrite Zmod_small by omega.
+  rewrite Z.mod_small by omega.
   apply H1. omega. omega.
 - destruct (zlt n0 Int.zwordsize); auto with va.
   apply vmatch_sgn. red; intros. rewrite ! Int.bits_rol by omega.
   generalize (Int.unsigned_range n); intros.
-  rewrite ! Zmod_small by omega.
+  rewrite ! Z.mod_small by omega.
   rewrite H1 by omega. symmetry. rewrite H1 by omega. auto.
 - destruct (zlt n0 Int.zwordsize); auto with va.
 Qed.