diff options
Diffstat (limited to 'theories/Numbers/Natural/BigN')
| -rw-r--r-- | theories/Numbers/Natural/BigN/BigN.v | 4 | ||||
| -rw-r--r-- | theories/Numbers/Natural/BigN/NMake.v | 364 | ||||
| -rw-r--r-- | theories/Numbers/Natural/BigN/NMake_gen.ml | 2 | ||||
| -rw-r--r-- | theories/Numbers/Natural/BigN/Nbasic.v | 120 |
4 files changed, 240 insertions, 250 deletions
diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v index 7f205b38..072b75f7 100644 --- a/theories/Numbers/Natural/BigN/BigN.v +++ b/theories/Numbers/Natural/BigN/BigN.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 *) @@ -119,7 +119,7 @@ BigN.zify. auto with zarith. intros NEQ. generalize (BigN.spec_div_eucl a b). generalize (Z_div_mod_full [a] [b] NEQ). -destruct BigN.div_eucl as (q,r), Zdiv_eucl as (q',r'). +destruct BigN.div_eucl as (q,r), Z.div_eucl as (q',r'). intros (EQ,_). injection 1. intros EQr EQq. BigN.zify. rewrite EQr, EQq; auto. Qed. 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]. diff --git a/theories/Numbers/Natural/BigN/NMake_gen.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml index 59d440c3..278cc8bf 100644 --- a/theories/Numbers/Natural/BigN/NMake_gen.ml +++ b/theories/Numbers/Natural/BigN/NMake_gen.ml @@ -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 *) diff --git a/theories/Numbers/Natural/BigN/Nbasic.v b/theories/Numbers/Natural/BigN/Nbasic.v index 4717d0b2..5bde1008 100644 --- a/theories/Numbers/Natural/BigN/Nbasic.v +++ b/theories/Numbers/Natural/BigN/Nbasic.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 *) @@ -32,7 +32,7 @@ Proof. transitivity (2 * (2 ^ Z.of_nat n * Zpos p)). rewrite <- IHn. auto. rewrite Z.mul_assoc. - rewrite inj_S. + rewrite Nat2Z.inj_succ. rewrite <- Z.pow_succ_r; auto with zarith. Qed. @@ -41,39 +41,39 @@ Qed. Fixpoint plength (p: positive) : positive := match p with xH => xH - | xO p1 => Psucc (plength p1) - | xI p1 => Psucc (plength p1) + | xO p1 => Pos.succ (plength p1) + | xI p1 => Pos.succ (plength p1) end. Theorem plength_correct: forall p, (Zpos p < 2 ^ Zpos (plength p))%Z. -assert (F: (forall p, 2 ^ (Zpos (Psucc p)) = 2 * 2 ^ Zpos p)%Z). -intros p; replace (Zpos (Psucc p)) with (1 + Zpos p)%Z. +assert (F: (forall p, 2 ^ (Zpos (Pos.succ p)) = 2 * 2 ^ Zpos p)%Z). +intros p; replace (Zpos (Pos.succ p)) with (1 + Zpos p)%Z. rewrite Zpower_exp; auto with zarith. -rewrite Zpos_succ_morphism; unfold Zsucc; auto with zarith. +rewrite Pos2Z.inj_succ; unfold Z.succ; auto with zarith. intros p; elim p; simpl plength; auto. -intros p1 Hp1; rewrite F; repeat rewrite Zpos_xI. +intros p1 Hp1; rewrite F; repeat rewrite Pos2Z.inj_xI. assert (tmp: (forall p, 2 * p = p + p)%Z); try repeat rewrite tmp; auto with zarith. -intros p1 Hp1; rewrite F; rewrite (Zpos_xO p1). +intros p1 Hp1; rewrite F; rewrite (Pos2Z.inj_xO p1). assert (tmp: (forall p, 2 * p = p + p)%Z); try repeat rewrite tmp; auto with zarith. -rewrite Zpower_1_r; auto with zarith. +rewrite Z.pow_1_r; auto with zarith. Qed. -Theorem plength_pred_correct: forall p, (Zpos p <= 2 ^ Zpos (plength (Ppred p)))%Z. -intros p; case (Psucc_pred p); intros H1. +Theorem plength_pred_correct: forall p, (Zpos p <= 2 ^ Zpos (plength (Pos.pred p)))%Z. +intros p; case (Pos.succ_pred_or p); intros H1. subst; simpl plength. -rewrite Zpower_1_r; auto with zarith. +rewrite Z.pow_1_r; auto with zarith. pattern p at 1; rewrite <- H1. -rewrite Zpos_succ_morphism; unfold Zsucc; auto with zarith. -generalize (plength_correct (Ppred p)); auto with zarith. +rewrite Pos2Z.inj_succ; unfold Z.succ; auto with zarith. +generalize (plength_correct (Pos.pred p)); auto with zarith. Qed. Definition Pdiv p q := - match Zdiv (Zpos p) (Zpos q) with + match Z.div (Zpos p) (Zpos q) with Zpos q1 => match (Zpos p) - (Zpos q) * (Zpos q1) with Z0 => q1 - | _ => (Psucc q1) + | _ => (Pos.succ q1) end | _ => xH end. @@ -85,20 +85,20 @@ unfold Pdiv. assert (H1: Zpos q > 0); auto with zarith. assert (H1b: Zpos p >= 0); auto with zarith. generalize (Z_div_ge0 (Zpos p) (Zpos q) H1 H1b). -generalize (Z_div_mod_eq (Zpos p) (Zpos q) H1); case Zdiv. - intros HH _; rewrite HH; rewrite Zmult_0_r; rewrite Zmult_1_r; simpl. +generalize (Z_div_mod_eq (Zpos p) (Zpos q) H1); case Z.div. + intros HH _; rewrite HH; rewrite Z.mul_0_r; rewrite Z.mul_1_r; simpl. case (Z_mod_lt (Zpos p) (Zpos q) H1); auto with zarith. intros q1 H2. replace (Zpos p - Zpos q * Zpos q1) with (Zpos p mod Zpos q). 2: pattern (Zpos p) at 2; rewrite H2; auto with zarith. generalize H2 (Z_mod_lt (Zpos p) (Zpos q) H1); clear H2; - case Zmod. + case Z.modulo. intros HH _; rewrite HH; auto with zarith. - intros r1 HH (_,HH1); rewrite HH; rewrite Zpos_succ_morphism. - unfold Zsucc; rewrite Zmult_plus_distr_r; auto with zarith. + intros r1 HH (_,HH1); rewrite HH; rewrite Pos2Z.inj_succ. + unfold Z.succ; rewrite Z.mul_add_distr_l; auto with zarith. intros r1 _ (HH,_); case HH; auto. intros q1 HH; rewrite HH. -unfold Zge; simpl Zcompare; intros HH1; case HH1; auto. +unfold Z.ge; simpl Z.compare; intros HH1; case HH1; auto. Qed. Definition is_one p := match p with xH => true | _ => false end. @@ -109,7 +109,7 @@ Qed. Definition get_height digits p := let r := Pdiv p digits in - if is_one r then xH else Psucc (plength (Ppred r)). + if is_one r then xH else Pos.succ (plength (Pos.pred r)). Theorem get_height_correct: forall digits N, @@ -119,13 +119,13 @@ unfold get_height. assert (H1 := Pdiv_le N digits). case_eq (is_one (Pdiv N digits)); intros H2. rewrite (is_one_one _ H2) in H1. -rewrite Zmult_1_r in H1. -change (2^(1-1))%Z with 1; rewrite Zmult_1_r; auto. +rewrite Z.mul_1_r in H1. +change (2^(1-1))%Z with 1; rewrite Z.mul_1_r; auto. clear H2. -apply Zle_trans with (1 := H1). -apply Zmult_le_compat_l; auto with zarith. -rewrite Zpos_succ_morphism; unfold Zsucc. -rewrite Zplus_comm; rewrite Zminus_plus. +apply Z.le_trans with (1 := H1). +apply Z.mul_le_mono_nonneg_l; auto with zarith. +rewrite Pos2Z.inj_succ; unfold Z.succ. +rewrite Z.add_comm; rewrite Z.add_simpl_l. apply plength_pred_correct. Qed. @@ -152,18 +152,18 @@ Open Scope nat_scope. Fixpoint plusnS (n m: nat) {struct n} : (n + S m = S (n + m))%nat := match n return (n + S m = S (n + m))%nat with - | 0 => refl_equal (S m) + | 0 => eq_refl (S m) | S n1 => let v := S (S n1 + m) in - eq_ind_r (fun n => S n = v) (refl_equal v) (plusnS n1 m) + eq_ind_r (fun n => S n = v) (eq_refl v) (plusnS n1 m) end. Fixpoint plusn0 n : n + 0 = n := match n return (n + 0 = n) with - | 0 => refl_equal 0 + | 0 => eq_refl 0 | S n1 => let v := S n1 in - eq_ind_r (fun n : nat => S n = v) (refl_equal v) (plusn0 n1) + eq_ind_r (fun n : nat => S n = v) (eq_refl v) (plusn0 n1) end. Fixpoint diff (m n: nat) {struct m}: nat * nat := @@ -177,8 +177,8 @@ Fixpoint diff_l (m n : nat) {struct m} : fst (diff m n) + n = max m n := match m return fst (diff m n) + n = max m n with | 0 => match n return (n = max 0 n) with - | 0 => refl_equal _ - | S n0 => refl_equal _ + | 0 => eq_refl _ + | S n0 => eq_refl _ end | S m1 => match n return (fst (diff (S m1) n) + n = max (S m1) n) @@ -188,7 +188,7 @@ Fixpoint diff_l (m n : nat) {struct m} : fst (diff m n) + n = max m n := let v := fst (diff m1 n1) + n1 in let v1 := fst (diff m1 n1) + S n1 in eq_ind v (fun n => v1 = S n) - (eq_ind v1 (fun n => v1 = n) (refl_equal v1) (S v) (plusnS _ _)) + (eq_ind v1 (fun n => v1 = n) (eq_refl v1) (S v) (plusnS _ _)) _ (diff_l _ _) end end. @@ -197,17 +197,17 @@ Fixpoint diff_r (m n: nat) {struct m}: snd (diff m n) + m = max m n := match m return (snd (diff m n) + m = max m n) with | 0 => match n return (snd (diff 0 n) + 0 = max 0 n) with - | 0 => refl_equal _ + | 0 => eq_refl _ | S _ => plusn0 _ end | S m => match n return (snd (diff (S m) n) + S m = max (S m) n) with - | 0 => refl_equal (snd (diff (S m) 0) + S m) + | 0 => eq_refl (snd (diff (S m) 0) + S m) | S n1 => let v := S (max m n1) in eq_ind_r (fun n => n = v) (eq_ind_r (fun n => S n = v) - (refl_equal v) (diff_r _ _)) (plusnS _ _) + (eq_refl v) (diff_r _ _)) (plusnS _ _) end end. @@ -216,7 +216,7 @@ Fixpoint diff_r (m n: nat) {struct m}: snd (diff m n) + m = max m n := Definition castm (m n: nat) (H: m = n) (x: word w (S m)): (word w (S n)) := match H in (_ = y) return (word w (S y)) with - | refl_equal => x + | eq_refl => x end. Variable m: nat. @@ -314,7 +314,7 @@ Section CompareRec. Lemma base_xO: forall n, base (xO n) = (base n)^2. Proof. intros n1; unfold base. - rewrite (Zpos_xO n1); rewrite Zmult_comm; rewrite Zpower_mult; auto with zarith. + rewrite (Pos2Z.inj_xO n1); rewrite Z.mul_comm; rewrite Z.pow_mul_r; auto with zarith. Qed. Let double_to_Z_pos: forall n x, 0 <= double_to_Z n x < double_wB n := @@ -332,13 +332,13 @@ Section CompareRec. rewrite 2 Hrec. simpl double_to_Z. set (wB := DoubleBase.double_wB wm_base n). - case Zcompare_spec; intros Cmp. + case Z.compare_spec; intros Cmp. rewrite <- Cmp. reflexivity. - symmetry. apply Zgt_lt, Zlt_gt. (* ;-) *) + symmetry. apply Z.gt_lt, Z.lt_gt. (* ;-) *) assert (0 < wB). unfold wB, DoubleBase.double_wB, base; auto with zarith. - change 0 with (0 + 0); apply Zplus_lt_le_compat; auto with zarith. - apply Zmult_lt_0_compat; auto with zarith. + change 0 with (0 + 0); apply Z.add_lt_le_mono; auto with zarith. + apply Z.mul_pos_pos; auto with zarith. case (double_to_Z_pos n xl); auto with zarith. case (double_to_Z_pos n xh); intros; exfalso; omega. Qed. @@ -358,9 +358,9 @@ Section CompareRec. end. Variable spec_compare: forall x y, - compare x y = Zcompare (w_to_Z x) (w_to_Z y). + compare x y = Z.compare (w_to_Z x) (w_to_Z y). Variable spec_compare_m: forall x y, - compare_m x y = Zcompare (wm_to_Z x) (w_to_Z y). + compare_m x y = Z.compare (wm_to_Z x) (w_to_Z y). Variable wm_base_lt: forall x, 0 <= w_to_Z x < base (wm_base). @@ -369,35 +369,35 @@ Section CompareRec. Proof. intros n x; elim n; simpl; auto; clear n. intros n (H0, H); split; auto. - apply Zlt_le_trans with (1:= H). + apply Z.lt_le_trans with (1:= H). unfold double_wB, DoubleBase.double_wB; simpl. rewrite Pshiftl_nat_S, base_xO. set (u := base (Pos.shiftl_nat wm_base n)). assert (0 < u). unfold u, base; auto with zarith. replace (u^2) with (u * u); simpl; auto with zarith. - apply Zle_trans with (1 * u); auto with zarith. - unfold Zpower_pos; simpl; ring. + apply Z.le_trans with (1 * u); auto with zarith. + unfold Z.pow_pos; simpl; ring. Qed. Lemma spec_compare_mn_1: forall n x y, - compare_mn_1 n x y = Zcompare (double_to_Z n x) (w_to_Z y). + compare_mn_1 n x y = Z.compare (double_to_Z n x) (w_to_Z y). Proof. intros n; elim n; simpl; auto; clear n. intros n Hrec x; case x; clear x; auto. intros y; rewrite spec_compare; rewrite w_to_Z_0. reflexivity. intros xh xl y; simpl; - rewrite spec_compare0_mn, Hrec. case Zcompare_spec. + rewrite spec_compare0_mn, Hrec. case Z.compare_spec. intros H1b. - rewrite <- H1b; rewrite Zmult_0_l; rewrite Zplus_0_l; auto. - symmetry. apply Zlt_gt. + rewrite <- H1b; rewrite Z.mul_0_l; rewrite Z.add_0_l; auto. + symmetry. apply Z.lt_gt. case (double_wB_lt n y); intros _ H0. - apply Zlt_le_trans with (1:= H0). + apply Z.lt_le_trans with (1:= H0). fold double_wB. case (double_to_Z_pos n xl); intros H1 H2. - apply Zle_trans with (double_to_Z n xh * double_wB n); auto with zarith. - apply Zle_trans with (1 * double_wB n); auto with zarith. + apply Z.le_trans with (double_to_Z n xh * double_wB n); auto with zarith. + apply Z.le_trans with (1 * double_wB n); auto with zarith. case (double_to_Z_pos n xh); intros; exfalso; omega. Qed. @@ -440,8 +440,8 @@ End AddS. Proof. intros x; elim x; clear x; [intros x1 Hrec | intros x1 Hrec | idtac]; intros y; case y; clear y; intros y1 H || intros H; simpl length_pos; - try (rewrite (Zpos_xI x1) || rewrite (Zpos_xO x1)); - try (rewrite (Zpos_xI y1) || rewrite (Zpos_xO y1)); + try (rewrite (Pos2Z.inj_xI x1) || rewrite (Pos2Z.inj_xO x1)); + try (rewrite (Pos2Z.inj_xI y1) || rewrite (Pos2Z.inj_xO y1)); try (inversion H; fail); try (assert (Zpos x1 < Zpos y1); [apply Hrec; apply lt_S_n | idtac]; auto with zarith); assert (0 < Zpos y1); auto with zarith; red; auto. |