diff options
Diffstat (limited to 'theories/Numbers/Natural/BigN/NMake.v')
| -rw-r--r-- | theories/Numbers/Natural/BigN/NMake.v | 364 |
1 files changed, 177 insertions, 187 deletions
diff --git a/theories/Numbers/Natural/BigN/NMake.v b/theories/Numbers/Natural/BigN/NMake.v index 952f6183..5012a1b9 100644 --- a/theories/Numbers/Natural/BigN/NMake.v +++ b/theories/Numbers/Natural/BigN/NMake.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -65,8 +65,8 @@ Module Make (W0:CyclicType) <: NType. intros. change (Zpos (ZnZ.digits (dom_op n)) <= Zpos (ZnZ.digits (dom_op m))). rewrite !digits_dom_op, !Pshiftl_nat_Zpower. - apply Zmult_le_compat_l; auto with zarith. - apply Zpower_le_monotone2; auto with zarith. + apply Z.mul_le_mono_nonneg_l; auto with zarith. + apply Z.pow_le_mono_r; auto with zarith. Qed. Definition to_N (x : t) := Z.to_N (to_Z x). @@ -186,12 +186,12 @@ Module Make (W0:CyclicType) <: NType. exact spec_0. Qed. - Lemma spec_pred : forall x, [pred x] = Zmax 0 ([x]-1). + Lemma spec_pred x : [pred x] = Z.max 0 ([x]-1). Proof. - intros. destruct (Zle_lt_or_eq _ _ (spec_pos x)). - rewrite Zmax_r; auto with zarith. - apply spec_pred_pos; auto. - rewrite <- H; apply spec_pred0; auto. + rewrite Z.max_comm. + destruct (Z.max_spec ([x]-1) 0) as [(H,->)|(H,->)]. + - apply spec_pred0; generalize (spec_pos x); auto with zarith. + - apply spec_pred_pos; auto with zarith. Qed. (** * Subtraction *) @@ -230,11 +230,11 @@ Module Make (W0:CyclicType) <: NType. exact spec_0. Qed. - Lemma spec_sub : forall x y, [sub x y] = Zmax 0 ([x]-[y]). + Lemma spec_sub : forall x y, [sub x y] = Z.max 0 ([x]-[y]). Proof. - intros. destruct (Zle_or_lt [y] [x]). - rewrite Zmax_r; auto with zarith. apply spec_sub_pos; auto. - rewrite Zmax_l; auto with zarith. apply spec_sub0; auto. + intros. destruct (Z.le_gt_cases [y] [x]). + rewrite Z.max_r; auto with zarith. apply spec_sub_pos; auto. + rewrite Z.max_l; auto with zarith. apply spec_sub0; auto. Qed. (** * Comparison *) @@ -249,7 +249,7 @@ Module Make (W0:CyclicType) <: NType. Let spec_comparen_m: forall n m (x : word (dom_t n) (S m)) (y : dom_t n), - comparen_m n m x y = Zcompare (eval n (S m) x) (ZnZ.to_Z y). + comparen_m n m x y = Z.compare (eval n (S m) x) (ZnZ.to_Z y). Proof. intros n m x y. unfold comparen_m, eval. @@ -287,10 +287,8 @@ Module Make (W0:CyclicType) <: NType. lazy beta iota delta [iter_sym dom_op dom_t comparen_m]. reflexivity. Qed. -(** TODO: no need for ZnZ.Spec_rect , Spec_ind, and so on... *) - Theorem spec_compare : forall x y, - compare x y = Zcompare [x] [y]. + compare x y = Z.compare [x] [y]. Proof. intros x y. rewrite compare_fold. apply spec_iter_sym; clear x y. intros. apply ZnZ.spec_compare. @@ -298,7 +296,7 @@ Module Make (W0:CyclicType) <: NType. intros n m x y; unfold comparenm. rewrite (spec_cast_l n m x), (spec_cast_r n m y). unfold to_Z; apply ZnZ.spec_compare. - intros. subst. apply Zcompare_antisym. + intros. subst. now rewrite <- Z.compare_antisym. Qed. Definition eqb (x y : t) : bool := @@ -346,14 +344,14 @@ Module Make (W0:CyclicType) <: NType. Definition min (n m : t) : t := match compare n m with Gt => m | _ => n end. Definition max (n m : t) : t := match compare n m with Lt => m | _ => n end. - Theorem spec_max : forall n m, [max n m] = Zmax [n] [m]. + Theorem spec_max : forall n m, [max n m] = Z.max [n] [m]. Proof. - intros. unfold max, Zmax. rewrite spec_compare; destruct Zcompare; reflexivity. + intros. unfold max, Z.max. rewrite spec_compare; destruct Z.compare; reflexivity. Qed. - Theorem spec_min : forall n m, [min n m] = Zmin [n] [m]. + Theorem spec_min : forall n m, [min n m] = Z.min [n] [m]. Proof. - intros. unfold min, Zmin. rewrite spec_compare; destruct Zcompare; reflexivity. + intros. unfold min, Z.min. rewrite spec_compare; destruct Z.compare; reflexivity. Qed. (** * Multiplication *) @@ -437,7 +435,7 @@ Module Make (W0:CyclicType) <: NType. intros; unfold wn_mul. generalize (spec_mul_add_n1 n m x y ZnZ.zero). case DoubleMul.double_mul_add_n1; intros q r Hqr. - rewrite ZnZ.spec_0, Zplus_0_r in Hqr. rewrite <- Hqr. + rewrite ZnZ.spec_0, Z.add_0_r in Hqr. rewrite <- Hqr. generalize (ZnZ.spec_eq0 q); case ZnZ.eq0; intros HH. rewrite HH; auto. simpl. apply spec_mk_t_w'. clear. @@ -458,7 +456,7 @@ Module Make (W0:CyclicType) <: NType. intros n m x y; unfold mulnm. rewrite spec_reduce_n. rewrite (spec_cast_l n m x), (spec_cast_r n m y). apply spec_muln. - intros. rewrite Zmult_comm; auto. + intros. rewrite Z.mul_comm; auto. Qed. (** * Division by a smaller number *) @@ -519,7 +517,7 @@ Module Make (W0:CyclicType) <: NType. apply DoubleBase.spec_get_low. apply spec_zeron. exact ZnZ.spec_to_Z. - apply Zle_lt_trans with (ZnZ.to_Z y); auto. + apply Z.le_lt_trans with (ZnZ.to_Z y); auto. rewrite <- nmake_double; auto. case (ZnZ.spec_to_Z y); auto. Qed. @@ -580,9 +578,9 @@ Module Make (W0:CyclicType) <: NType. intros x y H1 H2; generalize (spec_div_gt_aux x y H1 H2); case div_gt. intros q r (H3, H4); split. apply (Zdiv_unique [x] [y] [q] [r]); auto. - rewrite Zmult_comm; auto. + rewrite Z.mul_comm; auto. apply (Zmod_unique [x] [y] [q] [r]); auto. - rewrite Zmult_comm; auto. + rewrite Z.mul_comm; auto. Qed. (** * General Division *) @@ -597,7 +595,7 @@ Module Make (W0:CyclicType) <: NType. Theorem spec_div_eucl: forall x y, let (q,r) := div_eucl x y in - ([q], [r]) = Zdiv_eucl [x] [y]. + ([q], [r]) = Z.div_eucl [x] [y]. Proof. intros x y. unfold div_eucl. rewrite spec_eqb, spec_compare, spec_0. @@ -606,16 +604,16 @@ Module Make (W0:CyclicType) <: NType. intros H'. assert (H : 0 < [y]) by (generalize (spec_pos y); auto with zarith). clear H'. - case Zcompare_spec; intros Cmp; + case Z.compare_spec; intros Cmp; rewrite ?spec_0, ?spec_1; intros; auto with zarith. - rewrite Cmp; generalize (Z_div_same [y] (Zlt_gt _ _ H)) - (Z_mod_same [y] (Zlt_gt _ _ H)); - unfold Zdiv, Zmod; case Zdiv_eucl; intros; subst; auto. + rewrite Cmp; generalize (Z_div_same [y] (Z.lt_gt _ _ H)) + (Z_mod_same [y] (Z.lt_gt _ _ H)); + unfold Z.div, Z.modulo; case Z.div_eucl; intros; subst; auto. assert (LeLt: 0 <= [x] < [y]) by (generalize (spec_pos x); auto). generalize (Zdiv_small _ _ LeLt) (Zmod_small _ _ LeLt); - unfold Zdiv, Zmod; case Zdiv_eucl; intros; subst; auto. - generalize (spec_div_gt _ _ (Zlt_gt _ _ Cmp) H); auto. - unfold Zdiv, Zmod; case Zdiv_eucl; case div_gt. + unfold Z.div, Z.modulo; case Z.div_eucl; intros; subst; auto. + generalize (spec_div_gt _ _ (Z.lt_gt _ _ Cmp) H); auto. + unfold Z.div, Z.modulo; case Z.div_eucl; case div_gt. intros a b c d (H1, H2); subst; auto. Qed. @@ -626,7 +624,7 @@ Module Make (W0:CyclicType) <: NType. Proof. intros x y; unfold div; generalize (spec_div_eucl x y); case div_eucl; simpl fst. - intros xx yy; unfold Zdiv; case Zdiv_eucl; intros qq rr H; + intros xx yy; unfold Z.div; case Z.div_eucl; intros qq rr H; injection H; auto. Qed. @@ -730,10 +728,10 @@ Module Make (W0:CyclicType) <: NType. intro H'. assert (H : 0 < [y]) by (generalize (spec_pos y); auto with zarith). clear H'. - case Zcompare_spec; + case Z.compare_spec; rewrite ?spec_0, ?spec_1; intros; try split; auto with zarith. - rewrite H0; apply sym_equal; apply Z_mod_same; auto with zarith. - apply sym_equal; apply Zmod_small; auto with zarith. + rewrite H0; symmetry; apply Z_mod_same; auto with zarith. + symmetry; apply Zmod_small; auto with zarith. generalize (spec_pos x); auto with zarith. apply spec_mod_gt; auto with zarith. Qed. @@ -775,7 +773,7 @@ Module Make (W0:CyclicType) <: NType. Proof. intros x. symmetry. apply Z.sqrt_unique. - rewrite <- ! Zpower_2. apply spec_sqrt_aux. + rewrite <- ! Z.pow_2_r. apply spec_sqrt_aux. Qed. (** * Power *) @@ -791,14 +789,14 @@ Module Make (W0:CyclicType) <: NType. Proof. intros x n; generalize x; elim n; clear n x; simpl pow_pos. intros; rewrite spec_mul; rewrite spec_square; rewrite H. - rewrite Zpos_xI; rewrite Zpower_exp; auto with zarith. - rewrite (Zmult_comm 2); rewrite Zpower_mult; auto with zarith. - rewrite Zpower_2; rewrite Zpower_1_r; auto. + rewrite Pos2Z.inj_xI; rewrite Zpower_exp; auto with zarith. + rewrite (Z.mul_comm 2); rewrite Z.pow_mul_r; auto with zarith. + rewrite Z.pow_2_r; rewrite Z.pow_1_r; auto. intros; rewrite spec_square; rewrite H. - rewrite Zpos_xO; auto with zarith. - rewrite (Zmult_comm 2); rewrite Zpower_mult; auto with zarith. - rewrite Zpower_2; auto. - intros; rewrite Zpower_1_r; auto. + rewrite Pos2Z.inj_xO; auto with zarith. + rewrite (Z.mul_comm 2); rewrite Z.pow_mul_r; auto with zarith. + rewrite Z.pow_2_r; auto. + intros; rewrite Z.pow_1_r; auto. Qed. Definition pow_N (x:t)(n:N) : t := match n with @@ -806,7 +804,7 @@ Module Make (W0:CyclicType) <: NType. | BinNat.Npos p => pow_pos x p end. - Theorem spec_pow_N: forall x n, [pow_N x n] = [x] ^ Z_of_N n. + Theorem spec_pow_N: forall x n, [pow_N x n] = [x] ^ Z.of_N n. Proof. destruct n; simpl. apply spec_1. apply spec_pow_pos. @@ -867,15 +865,15 @@ Module Make (W0:CyclicType) <: NType. Zis_gcd [a] [b] [gcd_gt_body a b cont]. Proof. intros a b cont p H2 H3 H4; unfold gcd_gt_body. - rewrite ! spec_compare, spec_0. case Zcompare_spec. + rewrite ! spec_compare, spec_0. case Z.compare_spec. intros ->; apply Zis_gcd_0. intros HH; absurd (0 <= [b]); auto with zarith. case (spec_digits b); auto with zarith. - intros H5; case Zcompare_spec. - intros H6; rewrite <- (Zmult_1_r [b]). + intros H5; case Z.compare_spec. + intros H6; rewrite <- (Z.mul_1_r [b]). rewrite (Z_div_mod_eq [a] [b]); auto with zarith. rewrite <- spec_mod_gt; auto with zarith. - rewrite H6; rewrite Zplus_0_r. + rewrite H6; rewrite Z.add_0_r. apply Zis_gcd_mult; apply Zis_gcd_1. intros; apply False_ind. case (spec_digits (mod_gt a b)); auto with zarith. @@ -890,24 +888,19 @@ Module Make (W0:CyclicType) <: NType. rewrite <- spec_mod_gt; auto with zarith. repeat rewrite <- spec_mod_gt; auto with zarith. apply H4; auto with zarith. - apply Zmult_lt_reg_r with 2; auto with zarith. - apply Zle_lt_trans with ([b] + [mod_gt a b]); auto with zarith. - apply Zle_lt_trans with (([a]/[b]) * [b] + [mod_gt a b]); auto with zarith. - apply Zplus_le_compat_r. - pattern [b] at 1; rewrite <- (Zmult_1_l [b]). - apply Zmult_le_compat_r; auto with zarith. - case (Zle_lt_or_eq 0 ([a]/[b])); auto with zarith. - intros HH; rewrite (Z_div_mod_eq [a] [b]) in H2; - try rewrite <- HH in H2; auto with zarith. - case (Z_mod_lt [a] [b]); auto with zarith. - rewrite Zmult_comm; rewrite spec_mod_gt; auto with zarith. - rewrite <- Z_div_mod_eq; auto with zarith. - pattern 2 at 2; rewrite <- (Zpower_1_r 2). - rewrite <- Zpower_exp; auto with zarith. - ring_simplify (p - 1 + 1); auto. - case (Zle_lt_or_eq 0 p); auto with zarith. - generalize H3; case p; simpl Zpower; auto with zarith. - intros HH; generalize H3; rewrite <- HH; simpl Zpower; auto with zarith. + apply Z.mul_lt_mono_pos_r with 2; auto with zarith. + apply Z.le_lt_trans with ([b] + [mod_gt a b]); auto with zarith. + apply Z.le_lt_trans with (([a]/[b]) * [b] + [mod_gt a b]); auto with zarith. + - apply Z.add_le_mono_r. + rewrite <- (Z.mul_1_l [b]) at 1. + apply Z.mul_le_mono_nonneg_r; auto with zarith. + change 1 with (Z.succ 0). apply Z.le_succ_l. + apply Z.div_str_pos; auto with zarith. + - rewrite Z.mul_comm; rewrite spec_mod_gt; auto with zarith. + rewrite <- Z_div_mod_eq; auto with zarith. + rewrite Z.mul_comm, <- Z.pow_succ_r, Z.sub_1_r, Z.succ_pred; auto. + apply Z.le_0_sub. change 1 with (Z.succ 0). apply Z.le_succ_l. + destruct p; simpl in H3; auto with zarith. Qed. Fixpoint gcd_gt_aux (p:positive) (cont:t->t->t) (a b:t) : t := @@ -931,7 +924,7 @@ Module Make (W0:CyclicType) <: NType. apply Hrec with (Zpos p + n); auto. replace (Zpos p + (Zpos p + n)) with (Zpos (xI p) + n - 1); auto. - rewrite Zpos_xI; ring. + rewrite Pos2Z.inj_xI; ring. intros a2 b2 H9 H10. apply Hrec with n; auto. intros p Hrec n a b cont H2 H3 H4. @@ -940,18 +933,18 @@ Module Make (W0:CyclicType) <: NType. apply Hrec with (Zpos p + n - 1); auto. replace (Zpos p + (Zpos p + n - 1)) with (Zpos (xO p) + n - 1); auto. - rewrite Zpos_xO; ring. + rewrite Pos2Z.inj_xO; ring. intros a2 b2 H9 H10. apply Hrec with (n - 1); auto. replace (Zpos p + (n - 1)) with (Zpos p + n - 1); auto with zarith. intros a3 b3 H12 H13; apply H4; auto with zarith. - apply Zlt_le_trans with (1 := H12). - apply Zpower_le_monotone2; auto with zarith. + apply Z.lt_le_trans with (1 := H12). + apply Z.pow_le_mono_r; auto with zarith. intros n a b cont H H2 H3. simpl gcd_gt_aux. apply Zspec_gcd_gt_body with (n + 1); auto with zarith. - rewrite Zplus_comm; auto. + rewrite Z.add_comm; auto. intros a1 b1 H5 H6; apply H3; auto. replace n with (n + 1 - 1); auto; try ring. Qed. @@ -965,14 +958,14 @@ Module Make (W0:CyclicType) <: NType. Definition gcd_gt a b := gcd_gt_aux (digits a) gcd_cont a b. Theorem spec_gcd_gt: forall a b, - [a] > [b] -> [gcd_gt a b] = Zgcd [a] [b]. + [a] > [b] -> [gcd_gt a b] = Z.gcd [a] [b]. Proof. intros a b H2. case (spec_digits (gcd_gt a b)); intros H3 H4. case (spec_digits a); intros H5 H6. - apply sym_equal; apply Zis_gcd_gcd; auto with zarith. + symmetry; apply Zis_gcd_gcd; auto with zarith. unfold gcd_gt; apply Zspec_gcd_gt_aux with 0; auto with zarith. - intros a1 a2; rewrite Zpower_0_r. + intros a1 a2; rewrite Z.pow_0_r. case (spec_digits a2); intros H7 H8; intros; apply False_ind; auto with zarith. Qed. @@ -984,18 +977,18 @@ Module Make (W0:CyclicType) <: NType. | Gt => gcd_gt a b end. - Theorem spec_gcd: forall a b, [gcd a b] = Zgcd [a] [b]. + Theorem spec_gcd: forall a b, [gcd a b] = Z.gcd [a] [b]. Proof. intros a b. case (spec_digits a); intros H1 H2. case (spec_digits b); intros H3 H4. - unfold gcd. rewrite spec_compare. case Zcompare_spec. - intros HH; rewrite HH; apply sym_equal; apply Zis_gcd_gcd; auto. + unfold gcd. rewrite spec_compare. case Z.compare_spec. + intros HH; rewrite HH; symmetry; apply Zis_gcd_gcd; auto. apply Zis_gcd_refl. - intros; apply trans_equal with (Zgcd [b] [a]). + intros; transitivity (Z.gcd [b] [a]). apply spec_gcd_gt; auto with zarith. apply Zis_gcd_gcd; auto with zarith. - apply Zgcd_is_pos. + apply Z.gcd_nonneg. apply Zis_gcd_sym; apply Zgcd_is_gcd. intros; apply spec_gcd_gt; auto with zarith. Qed. @@ -1017,22 +1010,22 @@ Module Make (W0:CyclicType) <: NType. exact (ZnZ.spec_is_even x). Qed. - Theorem spec_even: forall x, even x = Zeven_bool [x]. + Theorem spec_even: forall x, even x = Z.even [x]. Proof. intros x. assert (H := spec_even_aux x). symmetry. - rewrite (Z_div_mod_eq_full [x] 2); auto with zarith. - destruct (even x); rewrite H, ?Zplus_0_r. + rewrite (Z.div_mod [x] 2); auto with zarith. + destruct (even x); rewrite H, ?Z.add_0_r. rewrite Zeven_bool_iff. apply Zeven_2p. apply not_true_is_false. rewrite Zeven_bool_iff. apply Zodd_not_Zeven. apply Zodd_2p_plus_1. Qed. - Theorem spec_odd: forall x, odd x = Zodd_bool [x]. + Theorem spec_odd: forall x, odd x = Z.odd [x]. Proof. intros x. unfold odd. assert (H := spec_even_aux x). symmetry. - rewrite (Z_div_mod_eq_full [x] 2); auto with zarith. - destruct (even x); rewrite H, ?Zplus_0_r; simpl negb. + rewrite (Z.div_mod [x] 2); auto with zarith. + destruct (even x); rewrite H, ?Z.add_0_r; simpl negb. apply not_true_is_false. rewrite Zodd_bool_iff. apply Zeven_not_Zodd. apply Zeven_2p. apply Zodd_bool_iff. apply Zodd_2p_plus_1. @@ -1041,27 +1034,21 @@ Module Make (W0:CyclicType) <: NType. (** * Conversion *) Definition pheight p := - Peano.pred (nat_of_P (get_height (ZnZ.digits (dom_op 0)) (plength p))). + Peano.pred (Pos.to_nat (get_height (ZnZ.digits (dom_op 0)) (plength p))). Theorem pheight_correct: forall p, - Zpos p < 2 ^ (Zpos (ZnZ.digits (dom_op 0)) * 2 ^ (Z_of_nat (pheight p))). + Zpos p < 2 ^ (Zpos (ZnZ.digits (dom_op 0)) * 2 ^ (Z.of_nat (pheight p))). Proof. intros p; unfold pheight. - assert (F1: forall x, Z_of_nat (Peano.pred (nat_of_P x)) = Zpos x - 1). - intros x. - assert (Zsucc (Z_of_nat (Peano.pred (nat_of_P x))) = Zpos x); auto with zarith. - rewrite <- inj_S. - rewrite <- (fun x => S_pred x 0); auto with zarith. - rewrite Zpos_eq_Z_of_nat_o_nat_of_P; auto. - apply lt_le_trans with 1%nat; auto with zarith. - exact (le_Pmult_nat x 1). - rewrite F1; clear F1. + rewrite Nat2Z.inj_pred by apply Pos2Nat.is_pos. + rewrite positive_nat_Z. + rewrite <- Z.sub_1_r. assert (F2:= (get_height_correct (ZnZ.digits (dom_op 0)) (plength p))). - apply Zlt_le_trans with (Zpos (Psucc p)). - rewrite Zpos_succ_morphism; auto with zarith. - apply Zle_trans with (1 := plength_pred_correct (Psucc p)). - rewrite Ppred_succ. - apply Zpower_le_monotone2; auto with zarith. + apply Z.lt_le_trans with (Zpos (Pos.succ p)). + rewrite Pos2Z.inj_succ; auto with zarith. + apply Z.le_trans with (1 := plength_pred_correct (Pos.succ p)). + rewrite Pos.pred_succ. + apply Z.pow_le_mono_r; auto with zarith. Qed. Definition of_pos (x:positive) : t := @@ -1076,8 +1063,8 @@ Module Make (W0:CyclicType) <: NType. simpl. apply ZnZ.of_pos_correct. unfold base. - apply Zlt_le_trans with (1 := pheight_correct x). - apply Zpower_le_monotone2; auto with zarith. + apply Z.lt_le_trans with (1 := pheight_correct x). + apply Z.pow_le_mono_r; auto with zarith. rewrite (digits_dom_op (_ _)), Pshiftl_nat_Zpower. auto with zarith. Qed. @@ -1088,7 +1075,7 @@ Module Make (W0:CyclicType) <: NType. end. Theorem spec_of_N: forall x, - [of_N x] = Z_of_N x. + [of_N x] = Z.of_N x. Proof. intros x; case x. simpl of_N. exact spec_0. @@ -1122,7 +1109,7 @@ Module Make (W0:CyclicType) <: NType. intros. apply Zdiv_unique with 0; auto with zarith. change 2 with (2^1) at 2. rewrite <- Zpower_exp; auto with zarith. - rewrite Zplus_0_r. f_equal. auto with zarith. + rewrite Z.add_0_r. f_equal. auto with zarith. Qed. Theorem spec_head0: forall x, 0 < [x] -> @@ -1212,9 +1199,9 @@ Module Make (W0:CyclicType) <: NType. set (d := ZnZ.digits (dom_op n)) in *; clearbody d. destruct (Z_lt_le_dec h (Zpos d)); auto. exfalso. assert (1 * 2^Zpos d <= ZnZ.to_Z x * 2^h). - apply Zmult_le_compat; auto with zarith. - apply Zpower_le_monotone2; auto with zarith. - rewrite Zmult_comm in H0. auto with zarith. + apply Z.mul_le_mono_nonneg; auto with zarith. + apply Z.pow_le_mono_r; auto with zarith. + rewrite Z.mul_comm in H0. auto with zarith. Qed. Lemma spec_log2_pos : forall x, [x]<>0 -> @@ -1232,13 +1219,13 @@ Module Make (W0:CyclicType) <: NType. assert (H2 := ZnZ.spec_to_Z (ZnZ.zdigits (dom_op n))). assert (H3 := head0_zdigits n x). rewrite Zmod_small by auto with zarith. + rewrite Z.sub_simpl_r. rewrite (Z.mul_lt_mono_pos_l (2^(ZnZ.to_Z (ZnZ.head0 x)))); auto with zarith. rewrite (Z.mul_le_mono_pos_l _ _ (2^(ZnZ.to_Z (ZnZ.head0 x)))); auto with zarith. rewrite <- 2 Zpower_exp; auto with zarith. - rewrite Z.add_sub_assoc, Zplus_minus. - rewrite Z.sub_simpl_r, Zplus_minus. + rewrite !Z.add_sub_assoc, !Z.add_simpl_l. rewrite ZnZ.spec_zdigits. rewrite pow2_pos_minus_1 by (red; auto). apply ZnZ.spec_head0; auto with zarith. @@ -1294,12 +1281,12 @@ Module Make (W0:CyclicType) <: NType. Proof. intros x y z HH HH1 HH2. split; auto with zarith. - apply Zle_lt_trans with (2 := HH2); auto with zarith. + apply Z.le_lt_trans with (2 := HH2); auto with zarith. apply Zdiv_le_upper_bound; auto with zarith. pattern x at 1; replace x with (x * 2 ^ 0); auto with zarith. - apply Zmult_le_compat_l; auto. - apply Zpower_le_monotone2; auto with zarith. - rewrite Zpower_0_r; ring. + apply Z.mul_le_mono_nonneg_l; auto. + apply Z.pow_le_mono_r; auto with zarith. + rewrite Z.pow_0_r; ring. Qed. Theorem spec_shiftr_pow2 : forall x n, @@ -1315,7 +1302,7 @@ Module Make (W0:CyclicType) <: NType. rewrite spec_reduce. rewrite ZnZ.spec_zdigits in H. rewrite ZnZ.spec_add_mul_div by auto with zarith. - rewrite ZnZ.spec_0, Zmult_0_l, Zplus_0_l. + rewrite ZnZ.spec_0, Z.mul_0_l, Z.add_0_l. rewrite Zmod_small. f_equal. f_equal. auto with zarith. split. auto with zarith. @@ -1324,8 +1311,8 @@ Module Make (W0:CyclicType) <: NType. rewrite ZnZ.spec_0. symmetry. apply Zdiv_small. split; auto with zarith. - apply Zlt_le_trans with (base (ZnZ.digits (dom_op n))); auto with zarith. - unfold base. apply Zpower_le_monotone2; auto with zarith. + apply Z.lt_le_trans with (base (ZnZ.digits (dom_op n))); auto with zarith. + unfold base. apply Z.pow_le_mono_r; auto with zarith. rewrite ZnZ.spec_zdigits in H. generalize (ZnZ.spec_to_Z d); auto with zarith. Qed. @@ -1370,21 +1357,21 @@ Module Make (W0:CyclicType) <: NType. destruct (ZnZ.spec_to_Z x). destruct (ZnZ.spec_to_Z p). rewrite ZnZ.spec_add_mul_div by (omega with *). - rewrite ZnZ.spec_0, Zdiv_0_l, Zplus_0_r. + rewrite ZnZ.spec_0, Zdiv_0_l, Z.add_0_r. apply Zmod_small. unfold base. split; auto with zarith. - rewrite Zmult_comm. - apply Zlt_le_trans with (2^(ZnZ.to_Z p + K)). + rewrite Z.mul_comm. + apply Z.lt_le_trans with (2^(ZnZ.to_Z p + K)). rewrite Zpower_exp; auto with zarith. - apply Zmult_lt_compat_l; auto with zarith. - apply Zpower_le_monotone2; auto with zarith. + apply Z.mul_lt_mono_pos_l; auto with zarith. + apply Z.pow_le_mono_r; auto with zarith. Qed. Theorem spec_unsafe_shiftl: forall x p, [p] <= [head0 x] -> [unsafe_shiftl x p] = [x] * 2 ^ [p]. Proof. intros. - destruct (Z_eq_dec [x] 0) as [EQ|NEQ]. + destruct (Z.eq_dec [x] 0) as [EQ|NEQ]. (* [x] = 0 *) apply spec_unsafe_shiftl_aux with 0; auto with zarith. now rewrite EQ. @@ -1421,7 +1408,7 @@ Module Make (W0:CyclicType) <: NType. Proof. intros x. rewrite ! digits_level, double_size_level. rewrite 2 digits_dom_op, 2 Pshiftl_nat_Zpower, - inj_S, Zpower_Zsucc; auto with zarith. + Nat2Z.inj_succ, Z.pow_succ_r; auto with zarith. ring. Qed. @@ -1438,46 +1425,47 @@ Module Make (W0:CyclicType) <: NType. assert (F1:= spec_pos (head0 x)). assert (F2: 0 < Zpos (digits x)). red; auto. - case (Zle_lt_or_eq _ _ (spec_pos x)); intros HH. + assert (HH := spec_pos x). Z.le_elim HH. generalize HH; rewrite <- (spec_double_size x); intros HH1. case (spec_head0 x HH); intros _ HH2. case (spec_head0 _ HH1). rewrite (spec_double_size x); rewrite (spec_double_size_digits x). intros HH3 _. - case (Zle_or_lt ([head0 (double_size x)]) (2 * [head0 x])); auto; intros HH4. + case (Z.le_gt_cases ([head0 (double_size x)]) (2 * [head0 x])); auto; intros HH4. absurd (2 ^ (2 * [head0 x] )* [x] < 2 ^ [head0 (double_size x)] * [x]); auto. - apply Zle_not_lt. - apply Zmult_le_compat_r; auto with zarith. - apply Zpower_le_monotone2; auto; auto with zarith. + apply Z.le_ngt. + apply Z.mul_le_mono_nonneg_r; auto with zarith. + apply Z.pow_le_mono_r; auto; auto with zarith. assert (HH5: 2 ^[head0 x] <= 2 ^(Zpos (digits x) - 1)). - case (Zle_lt_or_eq 1 [x]); auto with zarith; intros HH5. - apply Zmult_le_reg_r with (2 ^ 1); auto with zarith. - rewrite <- (fun x y z => Zpower_exp x (y - z)); auto with zarith. - assert (tmp: forall x, x - 1 + 1 = x); [intros; ring | rewrite tmp; clear tmp]. - apply Zle_trans with (2 := Zlt_le_weak _ _ HH2). - apply Zmult_le_compat_l; auto with zarith. - rewrite Zpower_1_r; auto with zarith. - apply Zpower_le_monotone2; auto with zarith. - case (Zle_or_lt (Zpos (digits x)) [head0 x]); auto with zarith; intros HH6. - absurd (2 ^ Zpos (digits x) <= 2 ^ [head0 x] * [x]); auto with zarith. - rewrite <- HH5; rewrite Zmult_1_r. - apply Zpower_le_monotone2; auto with zarith. - rewrite (Zmult_comm 2). - rewrite Zpower_mult; auto with zarith. - rewrite Zpower_2. - apply Zlt_le_trans with (2 := HH3). - rewrite <- Zmult_assoc. + { apply Z.le_succ_l in HH. change (1 <= [x]) in HH. + Z.le_elim HH. + - apply Z.mul_le_mono_pos_r with (2 ^ 1); auto with zarith. + rewrite <- (fun x y z => Z.pow_add_r x (y - z)); auto with zarith. + rewrite Z.sub_add. + apply Z.le_trans with (2 := Z.lt_le_incl _ _ HH2). + apply Z.mul_le_mono_nonneg_l; auto with zarith. + rewrite Z.pow_1_r; auto with zarith. + - apply Z.pow_le_mono_r; auto with zarith. + case (Z.le_gt_cases (Zpos (digits x)) [head0 x]); auto with zarith; intros HH6. + absurd (2 ^ Zpos (digits x) <= 2 ^ [head0 x] * [x]); auto with zarith. + rewrite <- HH; rewrite Z.mul_1_r. + apply Z.pow_le_mono_r; auto with zarith. } + rewrite (Z.mul_comm 2). + rewrite Z.pow_mul_r; auto with zarith. + rewrite Z.pow_2_r. + apply Z.lt_le_trans with (2 := HH3). + rewrite <- Z.mul_assoc. replace (2 * Zpos (digits x) - 1) with ((Zpos (digits x) - 1) + (Zpos (digits x))). rewrite Zpower_exp; auto with zarith. apply Zmult_lt_compat2; auto with zarith. split; auto with zarith. - apply Zmult_lt_0_compat; auto with zarith. - rewrite Zpos_xO; ring. - apply Zlt_le_weak; auto. + apply Z.mul_pos_pos; auto with zarith. + rewrite Pos2Z.inj_xO; ring. + apply Z.lt_le_incl; auto. repeat rewrite spec_head00; auto. rewrite spec_double_size_digits. - rewrite Zpos_xO; auto with zarith. + rewrite Pos2Z.inj_xO; auto with zarith. rewrite spec_double_size; auto. Qed. @@ -1485,24 +1473,26 @@ Module Make (W0:CyclicType) <: NType. forall x, 0 < [head0 (double_size x)]. Proof. intros x. - assert (F: 0 < Zpos (digits x)). - red; auto. - case (Zle_lt_or_eq _ _ (spec_pos (head0 (double_size x)))); auto; intros F0. - case (Zle_lt_or_eq _ _ (spec_pos (head0 x))); intros F1. - apply Zlt_le_trans with (2 := (spec_double_size_head0 x)); auto with zarith. - case (Zle_lt_or_eq _ _ (spec_pos x)); intros F3. + assert (F := Pos2Z.is_pos (digits x)). + assert (F0 := spec_pos (head0 (double_size x))). + Z.le_elim F0; auto. + assert (F1 := spec_pos (head0 x)). + Z.le_elim F1. + apply Z.lt_le_trans with (2 := (spec_double_size_head0 x)); auto with zarith. + assert (F3 := spec_pos x). + Z.le_elim F3. generalize F3; rewrite <- (spec_double_size x); intros F4. absurd (2 ^ (Zpos (xO (digits x)) - 1) < 2 ^ (Zpos (digits x))). - apply Zle_not_lt. - apply Zpower_le_monotone2; auto with zarith. - rewrite Zpos_xO; auto with zarith. + { apply Z.le_ngt. + apply Z.pow_le_mono_r; auto with zarith. + rewrite Pos2Z.inj_xO; auto with zarith. } case (spec_head0 x F3). - rewrite <- F1; rewrite Zpower_0_r; rewrite Zmult_1_l; intros _ HH. - apply Zle_lt_trans with (2 := HH). + rewrite <- F1; rewrite Z.pow_0_r; rewrite Z.mul_1_l; intros _ HH. + apply Z.le_lt_trans with (2 := HH). case (spec_head0 _ F4). rewrite (spec_double_size x); rewrite (spec_double_size_digits x). - rewrite <- F0; rewrite Zpower_0_r; rewrite Zmult_1_l; auto. - generalize F1; rewrite (spec_head00 _ (sym_equal F3)); auto with zarith. + rewrite <- F0; rewrite Z.pow_0_r; rewrite Z.mul_1_l; auto. + generalize F1; rewrite (spec_head00 _ (eq_sym F3)); auto with zarith. Qed. (** Finally we iterate [double_size] enough before [unsafe_shiftl] @@ -1521,14 +1511,14 @@ Module Make (W0:CyclicType) <: NType. [shiftl_aux_body cont x n] = [x] * 2 ^ [n]. Proof. intros n x p cont H1 H2; unfold shiftl_aux_body. - rewrite spec_compare; case Zcompare_spec; intros H. + rewrite spec_compare; case Z.compare_spec; intros H. apply spec_unsafe_shiftl; auto with zarith. apply spec_unsafe_shiftl; auto with zarith. rewrite H2. rewrite spec_double_size; auto. - rewrite Zplus_comm; rewrite Zpower_exp; auto with zarith. - apply Zle_trans with (2 := spec_double_size_head0 x). - rewrite Zpower_1_r; apply Zmult_le_compat_l; auto with zarith. + rewrite Z.add_comm; rewrite Zpower_exp; auto with zarith. + apply Z.le_trans with (2 := spec_double_size_head0 x). + rewrite Z.pow_1_r; apply Z.mul_le_mono_nonneg_l; auto with zarith. Qed. Fixpoint shiftl_aux p cont x n := @@ -1550,27 +1540,27 @@ Module Make (W0:CyclicType) <: NType. apply spec_shiftl_aux_body with (q); auto. intros x1 H3; apply Hrec with (q + 1)%positive; auto. intros x2 H4; apply Hrec with (p + q + 1)%positive; auto. - rewrite <- Pplus_assoc. - rewrite Zpos_plus_distr; auto. + rewrite <- Pos.add_assoc. + rewrite Pos2Z.inj_add; auto. intros x3 H5; apply H2. - rewrite Zpos_xI. + rewrite Pos2Z.inj_xI. replace (2 * Zpos p + 1 + Zpos q) with (Zpos p + Zpos (p + q + 1)); auto. - repeat rewrite Zpos_plus_distr; ring. + rewrite !Pos2Z.inj_add; ring. intros p Hrec q n x cont H1 H2. apply spec_shiftl_aux_body with (q); auto. intros x1 H3; apply Hrec with (q); auto. - apply Zle_trans with (2 := H3); auto with zarith. - apply Zpower_le_monotone2; auto with zarith. + apply Z.le_trans with (2 := H3); auto with zarith. + apply Z.pow_le_mono_r; auto with zarith. intros x2 H4; apply Hrec with (p + q)%positive; auto. intros x3 H5; apply H2. - rewrite (Zpos_xO p). + rewrite (Pos2Z.inj_xO p). replace (2 * Zpos p + Zpos q) with (Zpos p + Zpos (p + q)); auto. - repeat rewrite Zpos_plus_distr; ring. + rewrite Pos2Z.inj_add; ring. intros q n x cont H1 H2. apply spec_shiftl_aux_body with (q); auto. - rewrite Zplus_comm; auto. + rewrite Z.add_comm; auto. Qed. Definition shiftl x n := @@ -1582,25 +1572,25 @@ Module Make (W0:CyclicType) <: NType. [shiftl x n] = [x] * 2 ^ [n]. Proof. intros x n; unfold shiftl, shiftl_aux_body. - rewrite spec_compare; case Zcompare_spec; intros H. + rewrite spec_compare; case Z.compare_spec; intros H. apply spec_unsafe_shiftl; auto with zarith. apply spec_unsafe_shiftl; auto with zarith. rewrite <- (spec_double_size x). - rewrite spec_compare; case Zcompare_spec; intros H1. + rewrite spec_compare; case Z.compare_spec; intros H1. apply spec_unsafe_shiftl; auto with zarith. apply spec_unsafe_shiftl; auto with zarith. rewrite <- (spec_double_size (double_size x)). apply spec_shiftl_aux with 1%positive. - apply Zle_trans with (2 := spec_double_size_head0 (double_size x)). + apply Z.le_trans with (2 := spec_double_size_head0 (double_size x)). replace (2 ^ 1) with (2 * 1). - apply Zmult_le_compat_l; auto with zarith. + apply Z.mul_le_mono_nonneg_l; auto with zarith. generalize (spec_double_size_head0_pos x); auto with zarith. - rewrite Zpower_1_r; ring. + rewrite Z.pow_1_r; ring. intros x1 H2; apply spec_unsafe_shiftl. - apply Zle_trans with (2 := H2). - apply Zle_trans with (2 ^ Zpos (digits n)); auto with zarith. + apply Z.le_trans with (2 := H2). + apply Z.le_trans with (2 ^ Zpos (digits n)); auto with zarith. case (spec_digits n); auto with zarith. - apply Zpower_le_monotone2; auto with zarith. + apply Z.pow_le_mono_r; auto with zarith. Qed. Lemma spec_shiftl: forall x p, [shiftl x p] = Z.shiftl [x] [p]. |