From 8d5c6bb8f0cac1339dec7b730997ee30b1517073 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Fri, 22 Sep 2017 19:50:52 +0200 Subject: Remove coq warnings (#28) Replace deprecated functions and theorems from the Coq standard library (version 8.6) by their non-deprecated counterparts. --- common/Memdata.v | 50 +++++++++++++++++++++++++------------------------- 1 file changed, 25 insertions(+), 25 deletions(-) (limited to 'common/Memdata.v') diff --git a/common/Memdata.v b/common/Memdata.v index 0aed4644..a9ed48b4 100644 --- a/common/Memdata.v +++ b/common/Memdata.v @@ -53,7 +53,7 @@ Definition size_chunk_nat (chunk: memory_chunk) : nat := nat_of_Z(size_chunk chunk). Lemma size_chunk_conv: - forall chunk, size_chunk chunk = Z_of_nat (size_chunk_nat chunk). + forall chunk, size_chunk chunk = Z.of_nat (size_chunk_nat chunk). Proof. intros. destruct chunk; reflexivity. Qed. @@ -111,7 +111,7 @@ Qed. Lemma align_size_chunk_divides: forall chunk, (align_chunk chunk | size_chunk chunk). Proof. - intros. destruct chunk; simpl; try apply Zdivide_refl; exists 2; auto. + intros. destruct chunk; simpl; try apply Z.divide_refl; exists 2; auto. Qed. Lemma align_le_divides: @@ -120,7 +120,7 @@ Lemma align_le_divides: Proof. intros. destruct chunk1; destruct chunk2; simpl in *; solve [ omegaContradiction - | apply Zdivide_refl + | apply Z.divide_refl | exists 2; reflexivity | exists 4; reflexivity | exists 8; reflexivity ]. @@ -209,15 +209,15 @@ Qed. Lemma int_of_bytes_of_int: forall n x, - int_of_bytes (bytes_of_int n x) = x mod (two_p (Z_of_nat n * 8)). + int_of_bytes (bytes_of_int n x) = x mod (two_p (Z.of_nat n * 8)). Proof. induction n; intros. simpl. rewrite Zmod_1_r. auto. Opaque Byte.wordsize. - rewrite inj_S. simpl. - replace (Zsucc (Z_of_nat n) * 8) with (Z_of_nat n * 8 + 8) by omega. + rewrite Nat2Z.inj_succ. simpl. + replace (Z.succ (Z.of_nat n) * 8) with (Z.of_nat n * 8 + 8) by omega. rewrite two_p_is_exp; try omega. - rewrite Zmod_recombine. rewrite IHn. rewrite Zplus_comm. + rewrite Zmod_recombine. rewrite IHn. rewrite Z.add_comm. change (Byte.unsigned (Byte.repr x)) with (Byte.Z_mod_modulus x). rewrite Byte.Z_mod_modulus_eq. reflexivity. apply two_p_gt_ZERO. omega. apply two_p_gt_ZERO. omega. @@ -232,7 +232,7 @@ Proof. Qed. Lemma decode_encode_int: - forall n x, decode_int (encode_int n x) = x mod (two_p (Z_of_nat n * 8)). + forall n x, decode_int (encode_int n x) = x mod (two_p (Z.of_nat n * 8)). Proof. unfold decode_int, encode_int; intros. rewrite rev_if_be_involutive. apply int_of_bytes_of_int. @@ -272,19 +272,19 @@ Qed. Lemma bytes_of_int_mod: forall n x y, - Int.eqmod (two_p (Z_of_nat n * 8)) x y -> + Int.eqmod (two_p (Z.of_nat n * 8)) x y -> bytes_of_int n x = bytes_of_int n y. Proof. induction n. intros; simpl; auto. intros until y. - rewrite inj_S. - replace (Zsucc (Z_of_nat n) * 8) with (Z_of_nat n * 8 + 8) by omega. + rewrite Nat2Z.inj_succ. + replace (Z.succ (Z.of_nat n) * 8) with (Z.of_nat n * 8 + 8) by omega. rewrite two_p_is_exp; try omega. intro EQM. simpl; decEq. apply Byte.eqm_samerepr. red. - eapply Int.eqmod_divides; eauto. apply Zdivide_factor_l. + eapply Int.eqmod_divides; eauto. apply Z.divide_factor_r. apply IHn. destruct EQM as [k EQ]. exists k. rewrite EQ. rewrite <- Z_div_plus_full_l. decEq. change (two_p 8) with 256. ring. omega. @@ -354,7 +354,7 @@ Fixpoint check_value (n: nat) (v: val) (q: quantity) (vl: list memval) match n, vl with | O, nil => true | S m, Fragment v' q' m' :: vl' => - Val.eq v v' && quantity_eq q q' && beq_nat m m' && check_value m v q vl' + Val.eq v v' && quantity_eq q q' && Nat.eqb m m' && check_value m v q vl' | _, _ => false end. @@ -728,7 +728,7 @@ Proof. destruct (size_quantity_nat_pos q) as [sz EQ]. rewrite EQ. simpl. unfold proj_sumbool. rewrite dec_eq_true. destruct (quantity_eq q q0); auto. - destruct (beq_nat sz n) eqn:EQN; auto. + destruct (Nat.eqb sz n) eqn:EQN; auto. destruct (check_value sz v q mvl) eqn:CHECK; auto. simpl. apply beq_nat_true in EQN. subst n q0. constructor. auto. destruct H0 as [E|[E|[E|E]]]; subst chunk; destruct q; auto || discriminate. @@ -943,22 +943,22 @@ Qed. Lemma int_of_bytes_append: forall l2 l1, - int_of_bytes (l1 ++ l2) = int_of_bytes l1 + int_of_bytes l2 * two_p (Z_of_nat (length l1) * 8). + int_of_bytes (l1 ++ l2) = int_of_bytes l1 + int_of_bytes l2 * two_p (Z.of_nat (length l1) * 8). Proof. induction l1; simpl int_of_bytes; intros. simpl. ring. - simpl length. rewrite inj_S. - replace (Z.succ (Z.of_nat (length l1)) * 8) with (Z_of_nat (length l1) * 8 + 8) by omega. + simpl length. rewrite Nat2Z.inj_succ. + replace (Z.succ (Z.of_nat (length l1)) * 8) with (Z.of_nat (length l1) * 8 + 8) by omega. rewrite two_p_is_exp. change (two_p 8) with 256. rewrite IHl1. ring. omega. omega. Qed. Lemma int_of_bytes_range: - forall l, 0 <= int_of_bytes l < two_p (Z_of_nat (length l) * 8). + forall l, 0 <= int_of_bytes l < two_p (Z.of_nat (length l) * 8). Proof. induction l; intros. simpl. omega. - simpl length. rewrite inj_S. + simpl length. rewrite Nat2Z.inj_succ. replace (Z.succ (Z.of_nat (length l)) * 8) with (Z.of_nat (length l) * 8 + 8) by omega. rewrite two_p_is_exp. change (two_p 8) with 256. simpl int_of_bytes. generalize (Byte.unsigned_range a). @@ -1024,21 +1024,21 @@ Qed. Lemma bytes_of_int_append: forall n2 x2 n1 x1, - 0 <= x1 < two_p (Z_of_nat n1 * 8) -> - bytes_of_int (n1 + n2) (x1 + x2 * two_p (Z_of_nat n1 * 8)) = + 0 <= x1 < two_p (Z.of_nat n1 * 8) -> + bytes_of_int (n1 + n2) (x1 + x2 * two_p (Z.of_nat n1 * 8)) = bytes_of_int n1 x1 ++ bytes_of_int n2 x2. Proof. induction n1; intros. - simpl in *. f_equal. omega. - assert (E: two_p (Z.of_nat (S n1) * 8) = two_p (Z.of_nat n1 * 8) * 256). { - rewrite inj_S. change 256 with (two_p 8). rewrite <- two_p_is_exp. + rewrite Nat2Z.inj_succ. change 256 with (two_p 8). rewrite <- two_p_is_exp. f_equal. omega. omega. omega. } rewrite E in *. simpl. f_equal. apply Byte.eqm_samerepr. exists (x2 * two_p (Z.of_nat n1 * 8)). change Byte.modulus with 256. ring. - rewrite Zmult_assoc. rewrite Z_div_plus. apply IHn1. + rewrite Z.mul_assoc. rewrite Z_div_plus. apply IHn1. apply Zdiv_interval_1. omega. apply two_p_gt_ZERO; omega. omega. assumption. omega. Qed. @@ -1051,8 +1051,8 @@ Proof. intros. transitivity (bytes_of_int (4 + 4) (Int64.unsigned (Int64.ofwords (Int64.hiword i) (Int64.loword i)))). f_equal. f_equal. rewrite Int64.ofwords_recompose. auto. rewrite Int64.ofwords_add'. - change 32 with (Z_of_nat 4 * 8). - rewrite Zplus_comm. apply bytes_of_int_append. apply Int.unsigned_range. + change 32 with (Z.of_nat 4 * 8). + rewrite Z.add_comm. apply bytes_of_int_append. apply Int.unsigned_range. Qed. Lemma encode_val_int64: -- cgit