From 51c497b2e5a2b09788f2cf05f414634b037f52bf Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 23 Apr 2019 15:00:41 +0200 Subject: lib/Coqlib.v: remove defns about multiplication, division, modulus Instead, use definitions and lemmas from the Coq standard library (ZArith, Znumtheory). --- common/Memdata.v | 4 ++-- common/Memory.v | 10 +++++----- common/Separation.v | 2 +- common/Switch.v | 6 +++--- 4 files changed, 11 insertions(+), 11 deletions(-) (limited to 'common') diff --git a/common/Memdata.v b/common/Memdata.v index 307a02db..c53f0e5d 100644 --- a/common/Memdata.v +++ b/common/Memdata.v @@ -258,14 +258,14 @@ Lemma decode_encode_int_4: forall x, Int.repr (decode_int (encode_int 4 (Int.unsigned x))) = x. Proof. intros. rewrite decode_encode_int. transitivity (Int.repr (Int.unsigned x)). - decEq. apply Zmod_small. apply Int.unsigned_range. apply Int.repr_unsigned. + decEq. apply Z.mod_small. apply Int.unsigned_range. apply Int.repr_unsigned. Qed. Lemma decode_encode_int_8: forall x, Int64.repr (decode_int (encode_int 8 (Int64.unsigned x))) = x. Proof. intros. rewrite decode_encode_int. transitivity (Int64.repr (Int64.unsigned x)). - decEq. apply Zmod_small. apply Int64.unsigned_range. apply Int64.repr_unsigned. + decEq. apply Z.mod_small. apply Int64.unsigned_range. apply Int64.repr_unsigned. Qed. (** A length-[n] encoding depends only on the low [8*n] bits of the integer. *) diff --git a/common/Memory.v b/common/Memory.v index fed6c1d7..b68a5049 100644 --- a/common/Memory.v +++ b/common/Memory.v @@ -284,7 +284,7 @@ Lemma valid_access_dec: Proof. intros. destruct (range_perm_dec m b ofs (ofs + size_chunk chunk) Cur p). - destruct (Zdivide_dec (align_chunk chunk) ofs (align_chunk_pos chunk)). + destruct (Zdivide_dec (align_chunk chunk) ofs). left; constructor; auto. right; red; intro V; inv V; contradiction. right; red; intro V; inv V; contradiction. @@ -887,11 +887,11 @@ Proof. intros (bytes1 & bytes2 & LB1 & LB2 & APP). change 4 with (size_chunk Mint32) in LB1. exploit loadbytes_load. eexact LB1. - simpl. apply Zdivides_trans with 8; auto. exists 2; auto. + simpl. apply Z.divide_trans with 8; auto. exists 2; auto. intros L1. change 4 with (size_chunk Mint32) in LB2. exploit loadbytes_load. eexact LB2. - simpl. apply Z.divide_add_r. apply Zdivides_trans with 8; auto. exists 2; auto. exists 1; auto. + simpl. apply Z.divide_add_r. apply Z.divide_trans with 8; auto. exists 2; auto. exists 1; auto. intros L2. exists (decode_val Mint32 (if Archi.big_endian then bytes1 else bytes2)); exists (decode_val Mint32 (if Archi.big_endian then bytes2 else bytes1)). @@ -1644,9 +1644,9 @@ Proof. rewrite encode_val_length in SB2. simpl in SB2. exists m1; split. apply storebytes_store. exact SB1. - simpl. apply Zdivides_trans with 8; auto. exists 2; auto. + simpl. apply Z.divide_trans with 8; auto. exists 2; auto. apply storebytes_store. exact SB2. - simpl. apply Z.divide_add_r. apply Zdivides_trans with 8; auto. exists 2; auto. exists 1; auto. + simpl. apply Z.divide_add_r. apply Z.divide_trans with 8; auto. exists 2; auto. exists 1; auto. Qed. Theorem storev_int64_split: diff --git a/common/Separation.v b/common/Separation.v index a9642d72..1493b535 100644 --- a/common/Separation.v +++ b/common/Separation.v @@ -702,7 +702,7 @@ Proof. - intros. assert (0 <= ofs < sz2) by (eapply Mem.perm_alloc_3; eauto). omega. - intros. apply Mem.perm_implies with Freeable; auto with mem. eapply Mem.perm_alloc_2; eauto. xomega. -- red; intros. apply Zdivides_trans with 8; auto. +- red; intros. apply Z.divide_trans with 8; auto. exists (8 / align_chunk chunk). destruct chunk; reflexivity. - intros. elim FRESH2. eapply Mem.valid_block_inject_2; eauto. - intros (j' & INJ' & J1 & J2 & J3). diff --git a/common/Switch.v b/common/Switch.v index 0ef91d60..5a6d4c63 100644 --- a/common/Switch.v +++ b/common/Switch.v @@ -288,10 +288,10 @@ Lemma validate_jumptable_correct: Proof. intros. rewrite (validate_jumptable_correct_rec cases tbl ofs); auto. -- f_equal. f_equal. rewrite Zmod_small. omega. +- f_equal. f_equal. rewrite Z.mod_small. omega. destruct (zle ofs v). omega. assert (M: ((v - ofs) + 1 * modulus) mod modulus = (v - ofs) + modulus). - { rewrite Zmod_small. omega. omega. } + { rewrite Z.mod_small. omega. omega. } rewrite Z_mod_plus in M by auto. rewrite M in H0. omega. - generalize (Z_mod_lt (v - ofs) modulus modulus_pos). omega. Qed. @@ -331,7 +331,7 @@ Proof. rewrite (split_between_prop v _ _ _ _ _ _ EQ). assert (0 <= (v - ofs) mod modulus < modulus) by (apply Z_mod_lt; omega). destruct (zlt ((v - ofs) mod modulus) sz). - rewrite Zmod_small by omega. eapply validate_jumptable_correct; eauto. + rewrite Z.mod_small by omega. eapply validate_jumptable_correct; eauto. eapply IHt; eauto. Qed. -- cgit