Replace nat_of_Z with Z.to_nat

Use Z.to_nat theorems from the standard Coq library in preference to
our theorems in lib/Coqlib.v.

Simplify lib/Coqlib.v accordingly.

5 files changed, 17 insertions, 17 deletions

diff --git a/backend/CSEproof.v b/backend/CSEproof.v
index d6bde348..a60c316b 100644
--- a/backend/CSEproof.v
+++ b/backend/CSEproof.v
@@ -544,7 +544,7 @@ Lemma kill_loads_after_storebytes_holds:
   bc sp = BCstack ->
   ematch bc rs ae ->
   approx = VA.State ae am ->
-  length bytes = nat_of_Z sz -> sz >= 0 ->
+  length bytes = Z.to_nat sz -> sz >= 0 ->
   numbering_holds valu ge (Vptr sp Ptrofs.zero) rs m'
                            (kill_loads_after_storebytes approx n dst sz).
 Proof.
@@ -557,7 +557,7 @@ Proof.
   simpl.
   rewrite negb_false_iff in H8.
   eapply Mem.load_storebytes_other. eauto.
-  rewrite H6. rewrite nat_of_Z_eq by auto.
+  rewrite H6. rewrite Z2Nat.id by omega.
   eapply pdisjoint_sound. eauto.
   unfold aaddressing. apply match_aptr_of_aval. eapply eval_static_addressing_sound; eauto.
   erewrite <- regs_valnums_sound by eauto. eauto with va.
@@ -598,9 +598,9 @@ Proof.
   exploit Mem.storebytes_split; eauto. intros (m2 & SB2 & SB3).
   clear SB23.
   assert (L1: Z.of_nat (length bytes1) = n1).
-  { erewrite Mem.loadbytes_length by eauto. apply nat_of_Z_eq. unfold n1; omega. }
+  { erewrite Mem.loadbytes_length by eauto. apply Z2Nat.id. unfold n1; omega. }
   assert (L2: Z.of_nat (length bytes2) = n2).
-  { erewrite Mem.loadbytes_length by eauto. apply nat_of_Z_eq. unfold n2; omega. }
+  { erewrite Mem.loadbytes_length by eauto. apply Z2Nat.id. unfold n2; omega. }
   rewrite L1 in *. rewrite L2 in *.
   assert (LB': Mem.loadbytes m2 b2 (ofs2 + n1) n2 = Some bytes2).
   { rewrite <- L2. eapply Mem.loadbytes_storebytes_same; eauto. }
diff --git a/backend/Deadcodeproof.v b/backend/Deadcodeproof.v
index 199ac922..2edc0395 100644
--- a/backend/Deadcodeproof.v
+++ b/backend/Deadcodeproof.v
@@ -106,7 +106,7 @@ Local Transparent Mem.loadbytes.
   unfold Mem.loadbytes; intros. destruct H.
   destruct (Mem.range_perm_dec m1 b ofs (ofs + n) Cur Readable); inv H0.
   rewrite pred_dec_true. econstructor; split; eauto.
-  apply GETN. intros. rewrite nat_of_Z_max in H.
+  apply GETN. intros. rewrite Z_to_nat_max in H.
   assert (ofs <= i < ofs + n) by xomega.
   apply ma_memval0; auto.
   red; intros; eauto.
@@ -966,7 +966,7 @@ Ltac UseTransfer :=
   intros. eapply nlive_remove; eauto.
   unfold adst, vanalyze; rewrite AN; eapply aaddr_arg_sound_1; eauto.
   erewrite Mem.loadbytes_length in H1 by eauto.
-  rewrite nat_of_Z_eq in H1 by omega. auto.
+  rewrite Z2Nat.id in H1 by omega. auto.
   eauto.
   intros (tm' & A & B).
   econstructor; split.
@@ -993,7 +993,7 @@ Ltac UseTransfer :=
   intros (bc & A & B & C).
   intros. eapply nlive_contains; eauto.
   erewrite Mem.loadbytes_length in H0 by eauto.
-  rewrite nat_of_Z_eq in H0 by omega. auto.
+  rewrite Z2Nat.id in H0 by omega. auto.
 + (* annot *)
   destruct (transfer_builtin_args (kill_builtin_res res ne, nm) _x2) as (ne1, nm1) eqn:TR.
   InvSoundState.
diff --git a/backend/NeedDomain.v b/backend/NeedDomain.v
index d431f3d8..692b4f9b 100644
--- a/backend/NeedDomain.v
+++ b/backend/NeedDomain.v
@@ -327,9 +327,9 @@ Lemma eqmod_iagree:
   Int.eqmod (two_p (Int.size m)) x y ->
   iagree (Int.repr x) (Int.repr y) m.
 Proof.
-  intros. set (p := nat_of_Z (Int.size m)).
+  intros. set (p := Z.to_nat (Int.size m)).
   generalize (Int.size_range m); intros RANGE.
-  assert (EQ: Int.size m = Z.of_nat p). { symmetry; apply nat_of_Z_eq. omega. }
+  assert (EQ: Int.size m = Z.of_nat p). { symmetry; apply Z2Nat.id. omega. }
   rewrite EQ in H; rewrite <- two_power_nat_two_p in H.
   red; intros. rewrite ! Int.testbit_repr by auto.
   destruct (zlt i (Int.size m)).
@@ -345,9 +345,9 @@ Lemma iagree_eqmod:
   iagree x y (complete_mask m) ->
   Int.eqmod (two_p (Int.size m)) (Int.unsigned x) (Int.unsigned y).
 Proof.
-  intros. set (p := nat_of_Z (Int.size m)).
+  intros. set (p := Z.to_nat (Int.size m)).
   generalize (Int.size_range m); intros RANGE.
-  assert (EQ: Int.size m = Z.of_nat p). { symmetry; apply nat_of_Z_eq. omega. }
+  assert (EQ: Int.size m = Z.of_nat p). { symmetry; apply Z2Nat.id. omega. }
   rewrite EQ; rewrite <- two_power_nat_two_p.
   apply Int.eqmod_same_bits. intros. apply H. omega.
   unfold complete_mask. rewrite Int.bits_zero_ext by omega.
diff --git a/backend/Unusedglobproof.v b/backend/Unusedglobproof.v
index d5f871a0..680daba7 100644
--- a/backend/Unusedglobproof.v
+++ b/backend/Unusedglobproof.v
@@ -1160,10 +1160,10 @@ Local Transparent Mem.loadbytes.
   generalize (S1 NO). unfold Mem.loadbytes. destruct Mem.range_perm_dec; intros E1; inv E1.
   generalize (S2 NO). unfold Mem.loadbytes. destruct Mem.range_perm_dec; intros E2; inv E2.
   rewrite Z.add_0_r.
-  apply Mem_getN_forall2 with (p := 0) (n := nat_of_Z (init_data_list_size (gvar_init v))).
+  apply Mem_getN_forall2 with (p := 0) (n := Z.to_nat (init_data_list_size (gvar_init v))).
   rewrite H3, H4. apply bytes_of_init_inject. auto.
   omega.
-  rewrite nat_of_Z_eq by (apply init_data_list_size_pos). omega.
+  rewrite Z2Nat.id by (apply Z.ge_le; apply init_data_list_size_pos). omega.
 Qed.
 
 Lemma init_mem_inj_2:
diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v
index e7e44e29..37a9ecf2 100644
--- a/backend/ValueDomain.v
+++ b/backend/ValueDomain.v
@@ -3134,7 +3134,7 @@ Proof.
     omega.
     intros (bytes1 & bytes2 & LOAD1 & LOAD2 & CONCAT).
     subst bytes.
-    exploit Mem.loadbytes_length. eexact LOAD1. change (nat_of_Z 1) with 1%nat. intros LENGTH1.
+    exploit Mem.loadbytes_length. eexact LOAD1. change (Z.to_nat 1) with 1%nat. intros LENGTH1.
     rewrite in_app_iff in IN. destruct IN.
   * destruct bytes1; try discriminate. destruct bytes1; try discriminate.
     simpl in H. destruct H; try contradiction. subst m0.
@@ -3492,7 +3492,7 @@ Qed.
 Lemma ablock_storebytes_sound:
   forall m b ofs bytes m' p ab sz,
   Mem.storebytes m b ofs bytes = Some m' ->
-  length bytes = nat_of_Z sz ->
+  length bytes = Z.to_nat sz ->
   (forall b' ofs' q i, In (Fragment (Vptr b' ofs') q i) bytes -> pmatch b' ofs' p) ->
   bmatch m b ab ->
   bmatch m' b (ablock_storebytes ab p ofs sz).
@@ -3509,7 +3509,7 @@ Proof.
   exploit ablock_storebytes_contents; eauto. intros [A B].
   assert (Mem.load chunk' m b ofs' = Some v').
   { rewrite <- LOAD'; symmetry. eapply Mem.load_storebytes_other; eauto.
-    rewrite U. rewrite LENGTH. rewrite nat_of_Z_max. right; omega. }
+    rewrite U. rewrite LENGTH. rewrite Z_to_nat_max. right; omega. }
   exploit BM2; eauto. unfold ablock_load. rewrite A. rewrite COMPAT. auto.
 Qed.
 
@@ -3992,7 +3992,7 @@ Theorem storebytes_sound:
   Mem.storebytes m b (Ptrofs.unsigned ofs) bytes = Some m' ->
   mmatch m am ->
   pmatch b ofs p ->
-  length bytes = nat_of_Z sz ->
+  length bytes = Z.to_nat sz ->
   (forall b' ofs' qt i, In (Fragment (Vptr b' ofs') qt i) bytes -> pmatch b' ofs' q) ->
   mmatch m' (storebytes am p sz q).
 Proof.