From b66ddea9b0304d390b56afadda80fa4d2f2184d6 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 23 Apr 2019 14:12:04 +0200 Subject: 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. --- common/Memory.v | 34 +++++++++++++++++----------------- 1 file changed, 17 insertions(+), 17 deletions(-) (limited to 'common/Memory.v') 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. -- cgit