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.

4 files changed, 20 insertions, 20 deletions

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,