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

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

4 files changed, 11 insertions, 11 deletions

diff --git a/common/Memdata.v b/common/Memdata.v
index 307a02db..c53f0e5d 100644
--- a/common/Memdata.v
+++ b/common/Memdata.v
@@ -258,14 +258,14 @@ Lemma decode_encode_int_4:
   forall x, Int.repr (decode_int (encode_int 4 (Int.unsigned x))) = x.
 Proof.
   intros. rewrite decode_encode_int. transitivity (Int.repr (Int.unsigned x)).
-  decEq. apply Zmod_small. apply Int.unsigned_range. apply Int.repr_unsigned.
+  decEq. apply Z.mod_small. apply Int.unsigned_range. apply Int.repr_unsigned.
 Qed.
 
 Lemma decode_encode_int_8:
   forall x, Int64.repr (decode_int (encode_int 8 (Int64.unsigned x))) = x.
 Proof.
   intros. rewrite decode_encode_int. transitivity (Int64.repr (Int64.unsigned x)).
-  decEq. apply Zmod_small. apply Int64.unsigned_range. apply Int64.repr_unsigned.
+  decEq. apply Z.mod_small. apply Int64.unsigned_range. apply Int64.repr_unsigned.
 Qed.
 
 (** A length-[n] encoding depends only on the low [8*n] bits of the integer. *)
diff --git a/common/Memory.v b/common/Memory.v
index fed6c1d7..b68a5049 100644
--- a/common/Memory.v
+++ b/common/Memory.v
@@ -284,7 +284,7 @@ Lemma valid_access_dec:
 Proof.
   intros.
   destruct (range_perm_dec m b ofs (ofs + size_chunk chunk) Cur p).
-  destruct (Zdivide_dec (align_chunk chunk) ofs (align_chunk_pos chunk)).
+  destruct (Zdivide_dec (align_chunk chunk) ofs).
   left; constructor; auto.
   right; red; intro V; inv V; contradiction.
   right; red; intro V; inv V; contradiction.
@@ -887,11 +887,11 @@ Proof.
   intros (bytes1 & bytes2 & LB1 & LB2 & APP).
   change 4 with (size_chunk Mint32) in LB1.
   exploit loadbytes_load. eexact LB1.
-  simpl. apply Zdivides_trans with 8; auto. exists 2; auto.
+  simpl. apply Z.divide_trans with 8; auto. exists 2; auto.
   intros L1.
   change 4 with (size_chunk Mint32) in LB2.
   exploit loadbytes_load. eexact LB2.
-  simpl. apply Z.divide_add_r. apply Zdivides_trans with 8; auto. exists 2; auto. exists 1; auto.
+  simpl. apply Z.divide_add_r. apply Z.divide_trans with 8; auto. exists 2; auto. exists 1; auto.
   intros L2.
   exists (decode_val Mint32 (if Archi.big_endian then bytes1 else bytes2));
   exists (decode_val Mint32 (if Archi.big_endian then bytes2 else bytes1)).
@@ -1644,9 +1644,9 @@ Proof.
   rewrite encode_val_length in SB2. simpl in SB2.
   exists m1; split.
   apply storebytes_store. exact SB1.
-  simpl. apply Zdivides_trans with 8; auto. exists 2; auto.
+  simpl. apply Z.divide_trans with 8; auto. exists 2; auto.
   apply storebytes_store. exact SB2.
-  simpl. apply Z.divide_add_r. apply Zdivides_trans with 8; auto. exists 2; auto. exists 1; auto.
+  simpl. apply Z.divide_add_r. apply Z.divide_trans with 8; auto. exists 2; auto. exists 1; auto.
 Qed.
 
 Theorem storev_int64_split:
diff --git a/common/Separation.v b/common/Separation.v
index a9642d72..1493b535 100644
--- a/common/Separation.v
+++ b/common/Separation.v
@@ -702,7 +702,7 @@ Proof.
 - intros. assert (0 <= ofs < sz2) by (eapply Mem.perm_alloc_3; eauto). omega.
 - intros. apply Mem.perm_implies with Freeable; auto with mem.
   eapply Mem.perm_alloc_2; eauto. xomega.
-- red; intros. apply Zdivides_trans with 8; auto.
+- red; intros. apply Z.divide_trans with 8; auto.
   exists (8 / align_chunk chunk). destruct chunk; reflexivity.
 - intros. elim FRESH2. eapply Mem.valid_block_inject_2; eauto.
 - intros (j' & INJ' & J1 & J2 & J3).
diff --git a/common/Switch.v b/common/Switch.v
index 0ef91d60..5a6d4c63 100644
--- a/common/Switch.v
+++ b/common/Switch.v
@@ -288,10 +288,10 @@ Lemma validate_jumptable_correct:
 Proof.
   intros.
   rewrite (validate_jumptable_correct_rec cases tbl ofs); auto.
-- f_equal. f_equal. rewrite Zmod_small. omega.
+- f_equal. f_equal. rewrite Z.mod_small. omega.
   destruct (zle ofs v). omega.
   assert (M: ((v - ofs) + 1 * modulus) mod modulus = (v - ofs) + modulus).
-  { rewrite Zmod_small. omega. omega. }
+  { rewrite Z.mod_small. omega. omega. }
   rewrite Z_mod_plus in M by auto. rewrite M in H0. omega.
 - generalize (Z_mod_lt (v - ofs) modulus modulus_pos). omega.
 Qed.
@@ -331,7 +331,7 @@ Proof.
   rewrite (split_between_prop v _ _ _ _ _ _ EQ).
   assert (0 <= (v - ofs) mod modulus < modulus) by (apply Z_mod_lt; omega).
   destruct (zlt ((v - ofs) mod modulus) sz).
-  rewrite Zmod_small by omega. eapply validate_jumptable_correct; eauto.
+  rewrite Z.mod_small by omega. eapply validate_jumptable_correct; eauto.
   eapply IHt; eauto.
 Qed.