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.

11 files changed, 45 insertions, 68 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.
diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v
index 26d3d347..2dd34389 100644
--- a/cfrontend/SimplLocalsproof.v
+++ b/cfrontend/SimplLocalsproof.v
@@ -1055,7 +1055,7 @@ Proof.
   assert (RPDST: Mem.range_perm m bdst (Ptrofs.unsigned odst) (Ptrofs.unsigned odst + sizeof tge ty) Cur Nonempty).
     replace (sizeof tge ty) with (Z.of_nat (List.length bytes)).
     eapply Mem.range_perm_implies. eapply Mem.storebytes_range_perm; eauto. auto with mem.
-    rewrite LEN. apply nat_of_Z_eq. omega.
+    rewrite LEN. apply Z2Nat.id. omega.
   assert (PSRC: Mem.perm m bsrc (Ptrofs.unsigned osrc) Cur Nonempty).
     apply RPSRC. omega.
   assert (PDST: Mem.perm m bdst (Ptrofs.unsigned odst) Cur Nonempty).
diff --git a/common/Events.v b/common/Events.v
index b2335b96..26dd505f 100644
--- a/common/Events.v
+++ b/common/Events.v
@@ -1208,7 +1208,7 @@ Proof.
   assert (RPDST: Mem.range_perm m1 bdst (Ptrofs.unsigned odst) (Ptrofs.unsigned odst + sz) Cur Nonempty).
     replace sz with (Z.of_nat (length bytes)).
     eapply Mem.range_perm_implies. eapply Mem.storebytes_range_perm; eauto. auto with mem.
-    rewrite LEN. apply nat_of_Z_eq. omega.
+    rewrite LEN. apply Z2Nat.id. omega.
   assert (PSRC: Mem.perm m1 bsrc (Ptrofs.unsigned osrc) Cur Nonempty).
     apply RPSRC. omega.
   assert (PDST: Mem.perm m1 bdst (Ptrofs.unsigned odst) Cur Nonempty).
diff --git a/common/Memdata.v b/common/Memdata.v
index a9ed48b4..307a02db 100644
--- a/common/Memdata.v
+++ b/common/Memdata.v
@@ -50,7 +50,7 @@ Proof.
 Qed.
 
 Definition size_chunk_nat (chunk: memory_chunk) : nat :=
-  nat_of_Z(size_chunk chunk).
+  Z.to_nat(size_chunk chunk).
 
 Lemma size_chunk_conv:
   forall chunk, size_chunk chunk = Z.of_nat (size_chunk_nat chunk).
diff --git a/common/Memory.v b/common/Memory.v
index 2cf1c3ab..fed6c1d7 100644
--- a/common/Memory.v
+++ b/common/Memory.v
@@ -460,7 +460,7 @@ Definition loadv (chunk: memory_chunk) (m: mem) (addr: val) : option val :=
 
 Definition loadbytes (m: mem) (b: block) (ofs n: Z): option (list memval) :=
   if range_perm_dec m b ofs (ofs + n) Cur Readable
-  then Some (getN (nat_of_Z n) ofs (m.(mem_contents)#b))
+  then Some (getN (Z.to_nat n) ofs (m.(mem_contents)#b))
   else None.
 
 (** Memory stores. *)
@@ -780,7 +780,7 @@ Qed.
 Theorem loadbytes_length:
   forall m b ofs n bytes,
   loadbytes m b ofs n = Some bytes ->
-  length bytes = nat_of_Z n.
+  length bytes = Z.to_nat n.
 Proof.
   unfold loadbytes; intros.
   destruct (range_perm_dec m b ofs (ofs + n) Cur Readable); try congruence.
@@ -791,7 +791,7 @@ Theorem loadbytes_empty:
   forall m b ofs n,
   n <= 0 -> loadbytes m b ofs n = Some nil.
 Proof.
-  intros. unfold loadbytes. rewrite pred_dec_true. rewrite nat_of_Z_neg; auto.
+  intros. unfold loadbytes. rewrite pred_dec_true. rewrite Z_to_nat_neg; auto.
   red; intros. omegaContradiction.
 Qed.
 
@@ -816,8 +816,8 @@ Proof.
   unfold loadbytes; intros.
   destruct (range_perm_dec m b ofs (ofs + n1) Cur Readable); try congruence.
   destruct (range_perm_dec m b (ofs + n1) (ofs + n1 + n2) Cur Readable); try congruence.
-  rewrite pred_dec_true. rewrite nat_of_Z_plus; auto.
-  rewrite getN_concat. rewrite nat_of_Z_eq; auto.
+  rewrite pred_dec_true. rewrite Z2Nat.inj_add by omega.
+  rewrite getN_concat. rewrite Z2Nat.id by omega.
   congruence.
   red; intros.
   assert (ofs0 < ofs + n1 \/ ofs0 >= ofs + n1) by omega.
@@ -836,8 +836,8 @@ Proof.
   unfold loadbytes; intros.
   destruct (range_perm_dec m b ofs (ofs + (n1 + n2)) Cur Readable);
   try congruence.
-  rewrite nat_of_Z_plus in H; auto. rewrite getN_concat in H.
-  rewrite nat_of_Z_eq in H; auto.
+  rewrite Z2Nat.inj_add in H by omega. rewrite getN_concat in H.
+  rewrite Z2Nat.id in H by omega.
   repeat rewrite pred_dec_true.
   econstructor; econstructor.
   split. reflexivity. split. reflexivity. congruence.
@@ -1106,7 +1106,7 @@ Proof.
   assert (valid_access m2 chunk b ofs Readable) by eauto with mem.
   unfold loadbytes. rewrite pred_dec_true. rewrite store_mem_contents; simpl.
   rewrite PMap.gss.
-  replace (nat_of_Z (size_chunk chunk)) with (length (encode_val chunk v)).
+  replace (Z.to_nat (size_chunk chunk)) with (length (encode_val chunk v)).
   rewrite getN_setN_same. auto.
   rewrite encode_val_length. auto.
   apply H.
@@ -1127,10 +1127,10 @@ Proof.
   rewrite PMap.gsspec. destruct (peq b' b). subst b'.
   destruct H. congruence.
   destruct (zle n 0) as [z | n0].
-  rewrite (nat_of_Z_neg _ z). auto.
+  rewrite (Z_to_nat_neg _ z). auto.
   destruct H. omegaContradiction.
   apply getN_setN_outside. rewrite encode_val_length. rewrite <- size_chunk_conv.
-  rewrite nat_of_Z_eq. auto. omega.
+  rewrite Z2Nat.id. auto. omega.
   auto.
   red; intros. eauto with mem.
   rewrite pred_dec_false. auto.
@@ -1523,7 +1523,7 @@ Proof.
   destruct (range_perm_dec m1 b ofs (ofs + Z.of_nat (length bytes)) Cur Writable);
   try discriminate.
   rewrite pred_dec_true.
-  decEq. inv STORE2; simpl. rewrite PMap.gss. rewrite nat_of_Z_of_nat.
+  decEq. inv STORE2; simpl. rewrite PMap.gss. rewrite Nat2Z.id.
   apply getN_setN_same.
   red; eauto with mem.
 Qed.
@@ -1539,7 +1539,7 @@ Proof.
   rewrite pred_dec_true.
   rewrite storebytes_mem_contents. decEq.
   rewrite PMap.gsspec. destruct (peq b' b). subst b'.
-  apply getN_setN_disjoint. rewrite nat_of_Z_eq; auto. intuition congruence.
+  apply getN_setN_disjoint. rewrite Z2Nat.id by omega. intuition congruence.
   auto.
   red; auto with mem.
   apply pred_dec_false.
@@ -1867,7 +1867,7 @@ Proof.
   unfold loadbytes; intros. destruct (range_perm_dec m2 b ofs (ofs + n) Cur Readable); inv H.
   revert H0.
   injection ALLOC; intros A B. rewrite <- A; rewrite <- B; simpl. rewrite PMap.gss.
-  generalize (nat_of_Z n) ofs. induction n0; simpl; intros.
+  generalize (Z.to_nat n) ofs. induction n0; simpl; intros.
   contradiction.
   rewrite ZMap.gi in H0. destruct H0; eauto.
 Qed.
@@ -2342,13 +2342,13 @@ Lemma loadbytes_inj:
 Proof.
   intros. unfold loadbytes in *.
   destruct (range_perm_dec m1 b1 ofs (ofs + len) Cur Readable); inv H0.
-  exists (getN (nat_of_Z len) (ofs + delta) (m2.(mem_contents)#b2)).
+  exists (getN (Z.to_nat len) (ofs + delta) (m2.(mem_contents)#b2)).
   split. apply pred_dec_true.
   replace (ofs + delta + len) with ((ofs + len) + delta) by omega.
   eapply range_perm_inj; eauto with mem.
   apply getN_inj; auto.
-  destruct (zle 0 len). rewrite nat_of_Z_eq; auto. omega.
-  rewrite nat_of_Z_neg. simpl. red; intros; omegaContradiction. omega.
+  destruct (zle 0 len). rewrite Z2Nat.id by omega. auto.
+  rewrite Z_to_nat_neg by omega. simpl. red; intros; omegaContradiction.
 Qed.
 
 (** Preservation of stores. *)
@@ -4340,7 +4340,7 @@ Proof.
 + unfold loadbytes. destruct H.
   destruct (range_perm_dec m b ofs (ofs + n) Cur Readable).
   rewrite pred_dec_true. f_equal.
-  apply getN_exten. intros. rewrite nat_of_Z_eq in H by omega.
+  apply getN_exten. intros. rewrite Z2Nat.id in H by omega.
   apply unchanged_on_contents0; auto.
   red; intros. apply unchanged_on_perm0; auto.
   rewrite pred_dec_false. auto.
diff --git a/common/Memtype.v b/common/Memtype.v
index 03dc1499..53775d8b 100644
--- a/common/Memtype.v
+++ b/common/Memtype.v
@@ -358,7 +358,7 @@ Axiom load_loadbytes:
 Axiom loadbytes_length:
   forall m b ofs n bytes,
   loadbytes m b ofs n = Some bytes ->
-  length bytes = nat_of_Z n.
+  length bytes = Z.to_nat n.
 
 Axiom loadbytes_empty:
   forall m b ofs n,
diff --git a/lib/Coqlib.v b/lib/Coqlib.v
index 3b8e5b3b..90e0b89d 100644
--- a/lib/Coqlib.v
+++ b/lib/Coqlib.v
@@ -577,43 +577,20 @@ Qed.
 
 (** Conversion from [Z] to [nat]. *)
 
-Definition nat_of_Z: Z -> nat := Z.to_nat.
-
-Lemma nat_of_Z_of_nat:
-  forall n, nat_of_Z (Z.of_nat n) = n.
-Proof.
-  exact Nat2Z.id.
-Qed.
-
-Lemma nat_of_Z_max:
-  forall z, Z.of_nat (nat_of_Z z) = Z.max z 0.
-Proof.
-  intros. unfold Z.max. destruct z; simpl; auto.
-  change (Z.of_nat (Z.to_nat (Zpos p)) = Zpos p).
-  apply Z2Nat.id. compute; intuition congruence.
-Qed.
-
-Lemma nat_of_Z_eq:
-  forall z, z >= 0 -> Z.of_nat (nat_of_Z z) = z.
-Proof.
-  unfold nat_of_Z; intros. apply Z2Nat.id. omega.
-Qed.
-
-Lemma nat_of_Z_neg:
-  forall n, n <= 0 -> nat_of_Z n = O.
+Lemma Z_to_nat_neg:
+  forall n, n <= 0 -> Z.to_nat n = O.
 Proof.
   destruct n; unfold Z.le; simpl; auto. congruence.
 Qed.
 
-Lemma nat_of_Z_plus:
-  forall p q,
-  p >= 0 -> q >= 0 ->
-  nat_of_Z (p + q) = (nat_of_Z p + nat_of_Z q)%nat.
+Lemma Z_to_nat_max:
+  forall z, Z.of_nat (Z.to_nat z) = Z.max z 0.
 Proof.
-  unfold nat_of_Z; intros. apply Z2Nat.inj_add; omega.
+  intros. destruct (zle 0 z).
+- rewrite Z2Nat.id by auto. xomega.
+- rewrite Z_to_nat_neg by omega. xomega.
 Qed.
 
-
 (** Alignment: [align n amount] returns the smallest multiple of [amount]
   greater than or equal to [n]. *)