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). --- lib/Coqlib.v | 94 ++++------------------------------------------------------ lib/Floats.v | 4 +-- lib/Integers.v | 20 ++++++------- 3 files changed, 17 insertions(+), 101 deletions(-) (limited to 'lib') diff --git a/lib/Coqlib.v b/lib/Coqlib.v index 90e0b89d..02c5d07f 100644 --- a/lib/Coqlib.v +++ b/lib/Coqlib.v @@ -411,42 +411,12 @@ Qed. (** Properties of Euclidean division and modulus. *) -Lemma Zdiv_small: - forall x y, 0 <= x < y -> x / y = 0. -Proof. - intros. assert (y > 0). omega. - assert (forall a b, - 0 <= a < y -> - 0 <= y * b + a < y -> - b = 0). - intros. - assert (b = 0 \/ b > 0 \/ (-b) > 0). omega. - elim H3; intro. - auto. - elim H4; intro. - assert (y * b >= y * 1). apply Zmult_ge_compat_l. omega. omega. - omegaContradiction. - assert (y * (-b) >= y * 1). apply Zmult_ge_compat_l. omega. omega. - rewrite <- Zopp_mult_distr_r in H6. omegaContradiction. - apply H1 with (x mod y). - apply Z_mod_lt. auto. - rewrite <- Z_div_mod_eq. auto. auto. -Qed. - -Lemma Zmod_small: - forall x y, 0 <= x < y -> x mod y = x. -Proof. - intros. assert (y > 0). omega. - generalize (Z_div_mod_eq x y H0). - rewrite (Zdiv_small x y H). omega. -Qed. - Lemma Zmod_unique: forall x y a b, x = a * y + b -> 0 <= b < y -> x mod y = b. Proof. intros. subst x. rewrite Z.add_comm. - rewrite Z_mod_plus. apply Zmod_small. auto. omega. + rewrite Z_mod_plus. apply Z.mod_small. auto. omega. Qed. Lemma Zdiv_unique: @@ -461,30 +431,7 @@ Lemma Zdiv_Zdiv: forall a b c, b > 0 -> c > 0 -> (a / b) / c = a / (b * c). Proof. - intros. - generalize (Z_div_mod_eq a b H). generalize (Z_mod_lt a b H). intros. - generalize (Z_div_mod_eq (a/b) c H0). generalize (Z_mod_lt (a/b) c H0). intros. - set (q1 := a / b) in *. set (r1 := a mod b) in *. - set (q2 := q1 / c) in *. set (r2 := q1 mod c) in *. - symmetry. apply Zdiv_unique with (r2 * b + r1). - rewrite H2. rewrite H4. ring. - split. - assert (0 <= r2 * b). apply Z.mul_nonneg_nonneg. omega. omega. omega. - assert ((r2 + 1) * b <= c * b). - apply Zmult_le_compat_r. omega. omega. - replace ((r2 + 1) * b) with (r2 * b + b) in H5 by ring. - replace (c * b) with (b * c) in H5 by ring. - omega. -Qed. - -Lemma Zmult_le_compat_l_neg : - forall n m p:Z, n >= m -> p <= 0 -> p * n <= p * m. -Proof. - intros. - assert ((-p) * n >= (-p) * m). apply Zmult_ge_compat_l. auto. omega. - replace (p * n) with (- ((-p) * n)) by ring. - replace (p * m) with (- ((-p) * m)) by ring. - omega. + intros. apply Z.div_div; omega. Qed. Lemma Zdiv_interval_1: @@ -516,9 +463,9 @@ Proof. intros. assert (lo <= a / b < hi+1). apply Zdiv_interval_1. omega. omega. auto. - assert (lo * b <= lo * 1). apply Zmult_le_compat_l_neg. omega. omega. + assert (lo * b <= lo * 1) by (apply Z.mul_le_mono_nonpos_l; omega). replace (lo * 1) with lo in H3 by ring. - assert ((hi + 1) * 1 <= (hi + 1) * b). apply Zmult_le_compat_l. omega. omega. + assert ((hi + 1) * 1 <= (hi + 1) * b) by (apply Z.mul_le_mono_nonneg_l; omega). replace ((hi + 1) * 1) with (hi + 1) in H4 by ring. omega. omega. @@ -529,42 +476,11 @@ Lemma Zmod_recombine: a > 0 -> b > 0 -> x mod (a * b) = ((x/b) mod a) * b + (x mod b). Proof. - intros. - set (xb := x/b). - apply Zmod_unique with (xb/a). - generalize (Z_div_mod_eq x b H0); fold xb; intro EQ1. - generalize (Z_div_mod_eq xb a H); intro EQ2. - rewrite EQ2 in EQ1. - eapply eq_trans. eexact EQ1. ring. - generalize (Z_mod_lt x b H0). intro. - generalize (Z_mod_lt xb a H). intro. - assert (0 <= xb mod a * b <= a * b - b). - split. apply Z.mul_nonneg_nonneg; omega. - replace (a * b - b) with ((a - 1) * b) by ring. - apply Zmult_le_compat; omega. - omega. + intros. rewrite (Z.mul_comm a b). rewrite Z.rem_mul_r by omega. ring. Qed. (** Properties of divisibility. *) -Lemma Zdivides_trans: - forall x y z, (x | y) -> (y | z) -> (x | z). -Proof. - intros x y z [a A] [b B]; subst. exists (a*b); ring. -Qed. - -Definition Zdivide_dec: - forall (p q: Z), p > 0 -> { (p|q) } + { ~(p|q) }. -Proof. - intros. destruct (zeq (Z.modulo q p) 0). - left. exists (q / p). - transitivity (p * (q / p) + (q mod p)). apply Z_div_mod_eq; auto. - transitivity (p * (q / p)). omega. ring. - right; red; intros. elim n. apply Z_div_exact_1; auto. - inv H0. rewrite Z_div_mult; auto. ring. -Defined. -Global Opaque Zdivide_dec. - Lemma Zdivide_interval: forall a b c, 0 < c -> 0 <= a < b -> (c | a) -> (c | b) -> 0 <= a <= b - c. diff --git a/lib/Floats.v b/lib/Floats.v index 3ce8f4b4..f93505fc 100644 --- a/lib/Floats.v +++ b/lib/Floats.v @@ -1218,7 +1218,7 @@ Proof. set (m := n mod 2^p + (2^p-1)) in *. assert (C: m / 2^p = if zeq (n mod 2^p) 0 then 0 else 1). { unfold m. destruct (zeq (n mod 2^p) 0). - rewrite e. apply Zdiv_small. omega. + rewrite e. apply Z.div_small. omega. eapply Zdiv_unique with (n mod 2^p - 1). ring. omega. } assert (D: Z.testbit m p = if zeq (n mod 2^p) 0 then false else true). { destruct (zeq (n mod 2^p) 0). @@ -1226,7 +1226,7 @@ Proof. apply Z.testbit_true; auto. rewrite C; auto. } assert (E: forall i, p < i -> Z.testbit m i = false). { intros. apply Z.testbit_false. omega. - replace (m / 2^i) with 0. auto. symmetry. apply Zdiv_small. + replace (m / 2^i) with 0. auto. symmetry. apply Z.div_small. unfold m. split. omega. apply Z.lt_le_trans with (2 * 2^p). omega. change 2 with (2^1) at 1. rewrite <- (Zpower_plus radix2) by omega. apply Zpower_le. omega. } diff --git a/lib/Integers.v b/lib/Integers.v index 4b75e71e..64263b97 100644 --- a/lib/Integers.v +++ b/lib/Integers.v @@ -539,7 +539,7 @@ Lemma eqmod_small_eq: Proof. intros x y [k EQ] I1 I2. generalize (Zdiv_unique _ _ _ _ EQ I2). intro. - rewrite (Zdiv_small x modul I1) in H. subst k. omega. + rewrite (Z.div_small x modul I1) in H. subst k. omega. Qed. Lemma eqmod_mod_eq: @@ -712,7 +712,7 @@ Theorem repr_unsigned: forall i, repr (unsigned i) = i. Proof. destruct i; simpl. unfold repr. apply mkint_eq. - rewrite Z_mod_modulus_eq. apply Zmod_small; omega. + rewrite Z_mod_modulus_eq. apply Z.mod_small; omega. Qed. Hint Resolve repr_unsigned: ints. @@ -735,7 +735,7 @@ Theorem unsigned_repr: forall z, 0 <= z <= max_unsigned -> unsigned (repr z) = z. Proof. intros. rewrite unsigned_repr_eq. - apply Zmod_small. unfold max_unsigned in H. omega. + apply Z.mod_small. unfold max_unsigned in H. omega. Qed. Hint Resolve unsigned_repr: ints. @@ -782,7 +782,7 @@ Qed. Theorem unsigned_one: unsigned one = 1. Proof. - unfold one; rewrite unsigned_repr_eq. apply Zmod_small. split. omega. + unfold one; rewrite unsigned_repr_eq. apply Z.mod_small. split. omega. unfold modulus. replace wordsize with (S(Init.Nat.pred wordsize)). rewrite two_power_nat_S. generalize (two_power_nat_pos (Init.Nat.pred wordsize)). omega. @@ -793,7 +793,7 @@ Theorem unsigned_mone: unsigned mone = modulus - 1. Proof. unfold mone; rewrite unsigned_repr_eq. replace (-1) with ((modulus - 1) + (-1) * modulus). - rewrite Z_mod_plus_full. apply Zmod_small. + rewrite Z_mod_plus_full. apply Z.mod_small. generalize modulus_pos. omega. omega. Qed. @@ -825,7 +825,7 @@ Qed. Theorem unsigned_repr_wordsize: unsigned iwordsize = zwordsize. Proof. - unfold iwordsize; rewrite unsigned_repr_eq. apply Zmod_small. + unfold iwordsize; rewrite unsigned_repr_eq. apply Z.mod_small. generalize wordsize_pos wordsize_max_unsigned; unfold max_unsigned; omega. Qed. @@ -2464,7 +2464,7 @@ Proof. - rewrite andb_false_r; auto. - generalize (unsigned_range n); intros. rewrite bits_mone. rewrite andb_true_r. f_equal. - symmetry. apply Zmod_small. omega. + symmetry. apply Z.mod_small. omega. omega. Qed. @@ -2491,7 +2491,7 @@ Theorem rol_zero: rol x zero = x. Proof. bit_solve. f_equal. rewrite unsigned_zero. rewrite Z.sub_0_r. - apply Zmod_small; auto. + apply Z.mod_small; auto. Qed. Lemma bitwise_binop_rol: @@ -2616,14 +2616,14 @@ Proof. rewrite !testbit_repr; auto. rewrite !Z.lor_spec. rewrite orb_comm. f_equal; apply same_bits_eqm; auto. - apply eqm_unsigned_repr_r. apply eqm_refl2. f_equal. - rewrite Zmod_small; auto. + rewrite Z.mod_small; auto. assert (unsigned (add y z) = zwordsize). rewrite H1. apply unsigned_repr_wordsize. unfold add in H5. rewrite unsigned_repr in H5. omega. generalize two_wordsize_max_unsigned; omega. - apply eqm_unsigned_repr_r. apply eqm_refl2. f_equal. - apply Zmod_small; auto. + apply Z.mod_small; auto. Qed. (** ** Properties of [Z_one_bits] and [is_power2]. *) -- cgit