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. --- backend/CSEproof.v | 8 ++++---- backend/Deadcodeproof.v | 6 +++--- backend/NeedDomain.v | 8 ++++---- backend/Unusedglobproof.v | 4 ++-- backend/ValueDomain.v | 8 ++++---- cfrontend/SimplLocalsproof.v | 2 +- common/Events.v | 2 +- common/Memdata.v | 2 +- common/Memory.v | 34 +++++++++++++++++----------------- common/Memtype.v | 2 +- lib/Coqlib.v | 37 +++++++------------------------------ 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]. *) -- cgit