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 ++++---- 5 files changed, 17 insertions(+), 17 deletions(-) (limited to 'backend') 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. -- cgit