diff options
Diffstat (limited to 'theories/Ints/num')
| -rw-r--r-- | theories/Ints/num/GenAdd.v | 9 | ||||
| -rw-r--r-- | theories/Ints/num/GenBase.v | 22 | ||||
| -rw-r--r-- | theories/Ints/num/GenDiv.v | 58 | ||||
| -rw-r--r-- | theories/Ints/num/GenDivn1.v | 31 | ||||
| -rw-r--r-- | theories/Ints/num/GenLift.v | 16 | ||||
| -rw-r--r-- | theories/Ints/num/GenMul.v | 49 | ||||
| -rw-r--r-- | theories/Ints/num/GenSqrt.v | 119 | ||||
| -rw-r--r-- | theories/Ints/num/GenSub.v | 11 | ||||
| -rw-r--r-- | theories/Ints/num/Nbasic.v | 7 | ||||
| -rw-r--r-- | theories/Ints/num/Q0Make.v | 1 | ||||
| -rw-r--r-- | theories/Ints/num/QbiMake.v | 1 | ||||
| -rw-r--r-- | theories/Ints/num/QifMake.v | 1 | ||||
| -rw-r--r-- | theories/Ints/num/QpMake.v | 1 | ||||
| -rw-r--r-- | theories/Ints/num/QvMake.v | 1 | ||||
| -rw-r--r-- | theories/Ints/num/ZMake.v | 1 | ||||
| -rw-r--r-- | theories/Ints/num/Zn2Z.v | 7 | ||||
| -rw-r--r-- | theories/Ints/num/ZnZ.v | 1 |
17 files changed, 157 insertions, 179 deletions
diff --git a/theories/Ints/num/GenAdd.v b/theories/Ints/num/GenAdd.v index 9d4c579020..77f5e23016 100644 --- a/theories/Ints/num/GenAdd.v +++ b/theories/Ints/num/GenAdd.v @@ -10,7 +10,6 @@ Set Implicit Arguments. Require Import ZArith. Require Import ZAux. -Require Import ZDivModAux. Require Import Basic_type. Require Import GenBase. @@ -265,11 +264,11 @@ Section GenAdd. Lemma spec_ww_succ : forall x, [[ww_succ x]] = ([[x]] + 1) mod wwB. Proof. destruct x as [ |xh xl];simpl. - rewrite spec_ww_1;rewrite Zmod_def_small;trivial. + rewrite spec_ww_1;rewrite Zmod_small;trivial. split;[intro;discriminate|apply wwB_pos]. rewrite <- Zplus_assoc;generalize (spec_w_succ_c xl); destruct (w_succ_c xl) as[l|l];intro H;unfold interp_carry in H;rewrite <-H. - rewrite Zmod_def_small;trivial. + rewrite Zmod_small;trivial. rewrite wwB_wBwB;apply beta_mult;apply spec_to_Z. assert ([|l|] = 0). clear spec_ww_1 spec_w_1 spec_w_0. assert (H1:= spec_to_Z l); assert (H2:= spec_to_Z xl); omega. @@ -281,10 +280,10 @@ Section GenAdd. Lemma spec_ww_add : forall x y, [[ww_add x y]] = ([[x]] + [[y]]) mod wwB. Proof. destruct x as [ |xh xl];intros y;simpl. - rewrite Zmod_def_small;trivial. apply spec_ww_to_Z;trivial. + rewrite Zmod_small;trivial. apply spec_ww_to_Z;trivial. destruct y as [ |yh yl]. change [[W0]] with 0;rewrite Zplus_0_r. - rewrite Zmod_def_small;trivial. + rewrite Zmod_small;trivial. exact (spec_ww_to_Z w_digits w_to_Z spec_to_Z (WW xh xl)). simpl. replace ([|xh|] * wB + [|xl|] + ([|yh|] * wB + [|yl|])) with (([|xh|]+[|yh|])*wB + ([|xl|]+[|yl|])). 2:ring. diff --git a/theories/Ints/num/GenBase.v b/theories/Ints/num/GenBase.v index 6b6376b690..a9936f1dd0 100644 --- a/theories/Ints/num/GenBase.v +++ b/theories/Ints/num/GenBase.v @@ -10,8 +10,6 @@ Set Implicit Arguments. Require Import ZArith. Require Import ZAux. -Require Import ZDivModAux. -Require Import ZPowerAux. Require Import Basic_type. Require Import JMeq. @@ -188,7 +186,7 @@ Section GenBase. Lemma lt_0_wB : 0 < wB. Proof. - unfold base;apply Zpower_lt_0. unfold Zlt;reflexivity. + unfold base;apply Zpower_gt_0. unfold Zlt;reflexivity. unfold Zle;intros H;discriminate H. Qed. @@ -208,7 +206,7 @@ Section GenBase. Proof. assert (H:= wB_pos);rewrite wwB_wBwB;rewrite <-(Zmult_1_r 1). rewrite Zpower_2. - apply Zmult_lt_compat;(split;[unfold Zlt;reflexivity|trivial]). + apply Zmult_lt_compat2;(split;[unfold Zlt;reflexivity|trivial]). apply Zlt_le_weak;trivial. Qed. @@ -217,11 +215,11 @@ Section GenBase. clear spec_w_0 w_0 spec_w_1 w_1 spec_w_Bm1 w_Bm1 spec_w_WW spec_w_0W spec_to_Z;unfold base. assert (2 ^ Zpos w_digits = 2 * (2 ^ (Zpos w_digits - 1))). - pattern 2 at 2; rewrite <- Zpower_exp_1. + pattern 2 at 2; rewrite <- Zpower_1_r. rewrite <- Zpower_exp; auto with zarith. - eq_tac; auto with zarith. + f_equal; auto with zarith. case w_digits; compute; intros; discriminate. - rewrite H; eq_tac; auto with zarith. + rewrite H; f_equal; auto with zarith. rewrite Zmult_comm; apply Z_div_mult; auto with zarith. Qed. @@ -239,17 +237,17 @@ Section GenBase. (z*wB + [|x|]) mod wwB = (z mod wB)*wB + [|x|]. Proof. intros z x. - rewrite Zmod_plus. 2:apply lt_0_wwB. + rewrite Zplus_mod. pattern wwB at 1;rewrite wwB_wBwB; rewrite Zpower_2. rewrite Zmult_mod_distr_r;try apply lt_0_wB. - rewrite (Zmod_def_small [|x|]). - apply Zmod_def_small;rewrite wwB_wBwB;apply beta_mult;try apply spec_to_Z. + rewrite (Zmod_small [|x|]). + apply Zmod_small;rewrite wwB_wBwB;apply beta_mult;try apply spec_to_Z. apply Z_mod_lt;apply Zlt_gt;apply lt_0_wB. destruct (spec_to_Z x);split;trivial. change [|x|] with (0*wB+[|x|]). rewrite wwB_wBwB. rewrite Zpower_2;rewrite <- (Zplus_0_r (wB*wB));apply beta_lex_inv. apply lt_0_wB. apply spec_to_Z. split;[apply Zle_refl | apply lt_0_wB]. - Qed. + Qed. Lemma wB_div : forall x y, ([|x|] * wB + [|y|]) / wB = [|x|]. Proof. @@ -321,7 +319,7 @@ Section GenBase. apply Zmult_le_compat; auto with zarith. apply Zle_trans with wB; auto with zarith. unfold base. - rewrite <- (ZAux.Zpower_exp_0 2). + rewrite <- (Zpower_0_r 2). apply Zpower_le_monotone2; auto with zarith. unfold base; auto with zarith. Qed. diff --git a/theories/Ints/num/GenDiv.v b/theories/Ints/num/GenDiv.v index 6466c198ff..237adb48b0 100644 --- a/theories/Ints/num/GenDiv.v +++ b/theories/Ints/num/GenDiv.v @@ -10,8 +10,6 @@ Set Implicit Arguments. Require Import ZArith. Require Import ZAux. -Require Import ZDivModAux. -Require Import ZPowerAux. Require Import Basic_type. Require Import GenBase. Require Import GenDivn1. @@ -102,42 +100,41 @@ Section POS_MOD. assert (F0: forall x y, x - y + y = x); auto with zarith. intros w1 p; case (spec_to_w_Z p); intros HH1 HH2. unfold ww_pos_mod; case w1. - simpl; rewrite Zmod_def_small; split; auto with zarith. + simpl; rewrite Zmod_small; split; auto with zarith. intros xh xl; generalize (spec_ww_compare p (w_0W w_zdigits)); case ww_compare; rewrite spec_w_0W; rewrite spec_zdigits; fold wB; intros H1. rewrite H1; simpl ww_to_Z. autorewrite with w_rewrite rm10. - rewrite Zmod_plus; auto with zarith. - rewrite Zmod_mult_0; auto with zarith. + rewrite Zplus_mod; auto with zarith. + rewrite Z_mod_mult; auto with zarith. autorewrite with rm10. rewrite Zmod_mod; auto with zarith. - rewrite Zmod_def_small; auto with zarith. + rewrite Zmod_small; auto with zarith. autorewrite with w_rewrite rm10. simpl ww_to_Z. rewrite spec_pos_mod. assert (HH0: [|low p|] = [[p]]). rewrite spec_low. - apply Zmod_def_small; auto with zarith. + apply Zmod_small; auto with zarith. case (spec_to_w_Z p); intros HHH1 HHH2; split; auto with zarith. apply Zlt_le_trans with (1 := H1). - unfold base. - apply Zpower2_le_lin; auto with zarith. + unfold base; apply Zpower2_le_lin; auto with zarith. rewrite HH0. - rewrite Zmod_plus; auto with zarith. + rewrite Zplus_mod; auto with zarith. unfold base. rewrite <- (F0 (Zpos w_digits) [[p]]). rewrite Zpower_exp; auto with zarith. rewrite Zmult_assoc. - rewrite Zmod_mult_0; auto with zarith. + rewrite Z_mod_mult; auto with zarith. autorewrite with w_rewrite rm10. rewrite Zmod_mod; auto with zarith. generalize (spec_ww_compare p ww_zdigits); case ww_compare; rewrite spec_ww_zdigits; rewrite spec_zdigits; intros H2. replace (2^[[p]]) with wwB. - rewrite Zmod_def_small; auto with zarith. + rewrite Zmod_small; auto with zarith. unfold base; rewrite H2. rewrite spec_ww_digits; auto. assert (HH0: [|low (ww_sub p (w_0W w_zdigits))|] = @@ -146,7 +143,7 @@ generalize (spec_ww_compare p ww_zdigits); rewrite spec_ww_sub. rewrite spec_w_0W; rewrite spec_zdigits. rewrite <- Zmod_div_mod; auto with zarith. - rewrite Zmod_def_small; auto with zarith. + rewrite Zmod_small; auto with zarith. split; auto with zarith. apply Zlt_le_trans with (Zpos w_digits); auto with zarith. unfold base; apply Zpower2_le_lin; auto with zarith. @@ -162,11 +159,11 @@ generalize (spec_ww_compare p ww_zdigits); unfold base; rewrite <- Zmult_assoc; rewrite <- Zpower_exp; auto with zarith. rewrite F0; auto with zarith. - rewrite <- Zplus_assoc; rewrite Zmod_plus; auto with zarith. - rewrite Zmod_mult_0; auto with zarith. + rewrite <- Zplus_assoc; rewrite Zplus_mod; auto with zarith. + rewrite Z_mod_mult; auto with zarith. autorewrite with rm10. rewrite Zmod_mod; auto with zarith. - apply sym_equal; apply Zmod_def_small; auto with zarith. + apply sym_equal; apply Zmod_small; auto with zarith. case (spec_to_Z xh); intros U1 U2. case (spec_to_Z xl); intros U3 U4. split; auto with zarith. @@ -186,7 +183,7 @@ generalize (spec_ww_compare p ww_zdigits); case (spec_to_Z xl); unfold base; auto with zarith. rewrite Zmult_minus_distr_r; rewrite <- Zpower_exp; auto with zarith. rewrite F0; auto with zarith. - rewrite Zmod_def_small; auto with zarith. + rewrite Zmod_small; auto with zarith. case (spec_to_w_Z (WW xh xl)); intros U1 U2. split; auto with zarith. apply Zlt_le_trans with (1:= U2). @@ -349,7 +346,7 @@ Section GenDiv32. simpl;rewrite spec_sub. assert ([|a2|] - [|b2|] = wB*(-1) + ([|a2|] - [|b2|] + wB)). ring. assert (0 <= [|a2|] - [|b2|] + wB < wB). omega. - rewrite <-(Zmod_unique ([|a2|]-[|b2|]) wB (-1) ([|a2|]-[|b2|]+wB) U H1 H0). + rewrite <-(Zmod_unique ([|a2|]-[|b2|]) wB (-1) ([|a2|]-[|b2|]+wB) H1 H0). rewrite wwB_wBwB;ring. assert (U2 := wB_pos w_digits). eapply spec_ww_add_c_cont with (P := @@ -433,8 +430,8 @@ Section GenDiv32. rewrite <- H8 in H2;rewrite H2 in H7. assert (0 < [|b1|]*wB). apply Zmult_lt_0_compat;zarith. Spec_ww_to_Z r2. zarith. - rewrite (Zmod_def_small ([|q|] -1));zarith. - rewrite (Zmod_def_small ([|q|] -1 -1));zarith. + rewrite (Zmod_small ([|q|] -1));zarith. + rewrite (Zmod_small ([|q|] -1 -1));zarith. assert ([[r2]] + ([|b1|] * wB + [|b2|]) = wwB * 1 + ([|r|] * wB + [|a3|] - [|q|] * [|b2|] + 2 * ([|b1|] * wB + [|b2|]))). @@ -455,11 +452,10 @@ Section GenDiv32. wwB 1 ([|r|] * wB + [|a3|] - [|q|] * [|b2|] + 2*([|b1|] * wB + [|b2|])) - U1 H10 H8). split. ring. zarith. intros r2;repeat (rewrite spec_pred);simpl ww_to_Z;intros H7. - rewrite (Zmod_def_small ([|q|] -1));zarith. + rewrite (Zmod_small ([|q|] -1));zarith. split. replace [[r2]] with ([[r1]] + ([|b1|] * wB + [|b2|]) -wwB). rewrite H2; ring. rewrite <- H7; ring. @@ -580,7 +576,7 @@ Section GenDiv21. match goal with |-context [ww_compare ?Y ?Z] => generalize (spec_ww_compare Y Z); case (ww_compare Y Z) end; simpl;try rewrite spec_ww_1;autorewrite with rm10; intros;zarith. - rewrite spec_ww_sub;simpl. rewrite Zmod_def_small;zarith. + rewrite spec_ww_sub;simpl. rewrite Zmod_small;zarith. split. ring. assert (wwB <= 2*[[b]]);zarith. rewrite wwB_div;zarith. @@ -927,7 +923,7 @@ Section GenDivGt. Spec_ww_to_Z (WW ah al). rewrite spec_ww_sub;eauto. simpl;rewrite spec_ww_1;rewrite Zmult_1_l;simpl. - simpl ww_to_Z in Hgt, H, HH;rewrite Zmod_def_small;split;zarith. + simpl ww_to_Z in Hgt, H, HH;rewrite Zmod_small;split;zarith. case (spec_to_Z (w_head0 bh)); auto with zarith. assert ([|w_head0 bh|] < Zpos w_digits). destruct (Z_lt_ge_dec [|w_head0 bh|] (Zpos w_digits));trivial. @@ -951,8 +947,8 @@ Section GenDivGt. assert (H5:=to_Z_div_minus_p bl HHHH). rewrite Zmult_comm in Hh. assert (2^[|w_head0 bh|] < wB). unfold base;apply Zpower_lt_monotone;zarith. - unfold base in H0;rewrite Zmod_def_small;zarith. - fold wB; rewrite (Zmod_def_small ([|bh|] * 2 ^ [|w_head0 bh|]));zarith. + unfold base in H0;rewrite Zmod_small;zarith. + fold wB; rewrite (Zmod_small ([|bh|] * 2 ^ [|w_head0 bh|]));zarith. intros U1 U2 U3 V1 V2. generalize (@spec_w_div32 (w_add_mul_div (w_head0 bh) w_0 ah) (w_add_mul_div (w_head0 bh) ah al) @@ -991,7 +987,7 @@ Section GenDivGt. Zmult_0_l;rewrite Zplus_0_l. replace [[ww_add_mul_div (ww_sub w_0 w_WW w_opp_c w_opp_carry w_sub_c w_opp w_sub w_sub_carry _ww_zdigits (w_0W (w_head0 bh))) W0 r]] with ([[r]]/2^[|w_head0 bh|]). - assert (0 < 2^[|w_head0 bh|]). apply Zpower_lt_0;zarith. + assert (0 < 2^[|w_head0 bh|]). apply Zpower_gt_0;zarith. split. rewrite <- (Z_div_mult [[WW ah al]] (2^[|w_head0 bh|]));zarith. rewrite H1;rewrite Zmult_assoc;apply Z_div_plus_l;trivial. @@ -1002,9 +998,9 @@ Section GenDivGt. change (Zpos (xO (w_digits))) with (2*Zpos (w_digits));zarith. simpl ww_to_Z;rewrite Zmult_0_l;rewrite Zplus_0_l. rewrite spec_w_0W. - rewrite (fun x y => Zmod_def_small (x-y)); auto with zarith. + rewrite (fun x y => Zmod_small (x-y)); auto with zarith. ring_simplify (2 * Zpos w_digits - (2 * Zpos w_digits - [|w_head0 bh|])). - rewrite Zmod_def_small;zarith. + rewrite Zmod_small;zarith. split;[apply Zdiv_le_lower_bound| apply Zdiv_lt_upper_bound];zarith. Spec_ww_to_Z r. apply Zlt_le_trans with wwB;zarith. @@ -1015,7 +1011,7 @@ Section GenDivGt. apply Zpower2_lt_lin; auto with zarith. rewrite spec_ww_sub; auto with zarith. rewrite spec_ww_digits_; rewrite spec_w_0W. - rewrite Zmod_def_small;zarith. + rewrite Zmod_small;zarith. rewrite Zpos_xO; split; auto with zarith. apply Zle_lt_trans with (2 * Zpos w_digits); auto with zarith. unfold base, ww_digits; rewrite (Zpos_xO w_digits). @@ -1412,7 +1408,7 @@ Section GenDiv. intros a b Hpos;unfold ww_mod. assert (H := spec_ww_compare a b);destruct (ww_compare a b). simpl;apply Zmod_unique with 1;try rewrite H;zarith. - Spec_ww_to_Z a;symmetry;apply Zmod_def_small;zarith. + Spec_ww_to_Z a;symmetry;apply Zmod_small;zarith. apply spec_ww_mod_gt;trivial. Qed. diff --git a/theories/Ints/num/GenDivn1.v b/theories/Ints/num/GenDivn1.v index 84bf247f75..7987741dad 100644 --- a/theories/Ints/num/GenDivn1.v +++ b/theories/Ints/num/GenDivn1.v @@ -9,8 +9,7 @@ Set Implicit Arguments. Require Import ZArith. -Require Import ZDivModAux. -Require Import ZPowerAux. +Require Import ZAux. Require Import Basic_type. Require Import GenBase. @@ -230,7 +229,7 @@ Section GENDIVN1. with (2*Zpos (gen_digits w_digits n));auto with zarith. replace (2 ^ (Zpos (gen_digits w_digits (S n)) - [|p|])) with (2^(Zpos (gen_digits w_digits n) - [|p|])*2^Zpos (gen_digits w_digits n)). - rewrite Zdiv_Zmult_compat_r;auto with zarith. + rewrite Zdiv_mult_cancel_r;auto with zarith. rewrite Zmult_plus_distr_l with (p:= 2^[|p|]). pattern ([!n|hl!] * 2^[|p|]) at 2; rewrite (shift_unshift_mod (Zpos(gen_digits w_digits n))([|p|])([!n|hl!])); @@ -254,7 +253,7 @@ Section GENDIVN1. with (2^Zpos(gen_digits w_digits n) *2^Zpos(gen_digits w_digits n)). rewrite (Zmult_comm (([!n|hh!] * 2 ^ [|p|] + [!n|hl!] / 2 ^ (Zpos (gen_digits w_digits n) - [|p|])))). - rewrite Zmod_Zmult_compat_l;auto with zarith. + rewrite Zmult_mod_distr_l;auto with zarith. ring. rewrite Zpower_exp;auto with zarith. assert (0 < Zpos (gen_digits w_digits n)). unfold Zlt;reflexivity. @@ -336,7 +335,7 @@ Section GENDIVN1. replace (2 ^ (Zpos (gen_digits w_digits (S n)) - Zpos w_digits)) with (2^(Zpos (gen_digits w_digits n) - Zpos w_digits) * 2^Zpos (gen_digits w_digits n)). - rewrite Zdiv_Zmult_compat_r;auto with zarith. + rewrite Zdiv_mult_cancel_r;auto with zarith. rewrite <- Zpower_exp;auto with zarith. replace (Zpos (gen_digits w_digits n) - Zpos w_digits + Zpos (gen_digits w_digits n)) with @@ -373,7 +372,7 @@ Section GENDIVN1. generalize (spec_compare (w_head0 b) w_0); case w_compare; rewrite spec_0; intros H2; auto with zarith. assert (Hv1: wB/2 <= [|b|]). - generalize H0; rewrite H2; rewrite Zpower_exp_0; + generalize H0; rewrite H2; rewrite Zpower_0_r; rewrite Zmult_1_l; auto. assert (Hv2: [|w_0|] < [|b|]). rewrite spec_0; auto. @@ -394,7 +393,7 @@ Section GENDIVN1. rewrite (spec_add_mul_div b w_0); auto with zarith. rewrite spec_0;rewrite Zdiv_0_l; try omega. rewrite Zplus_0_r; rewrite Zmult_comm. - rewrite Zmod_def_small; auto with zarith. + rewrite Zmod_small; auto with zarith. assert (H5 := spec_to_Z (high n a)). assert ([|w_add_mul_div (w_head0 b) w_0 (high n a)|] @@ -407,15 +406,15 @@ Section GENDIVN1. apply Zlt_le_trans with wB;auto with zarith. pattern wB at 1;replace wB with (wB*1);try ring. apply Zmult_le_compat;auto with zarith. - assert (H6 := Zpower_lt_0 2 (Zpos w_digits - [|w_head0 b|])); + assert (H6 := Zpower_gt_0 2 (Zpos w_digits - [|w_head0 b|])); auto with zarith. - rewrite Zmod_def_small;auto with zarith. + rewrite Zmod_small;auto with zarith. apply Zdiv_lt_upper_bound;auto with zarith. apply Zlt_le_trans with wB;auto with zarith. apply Zle_trans with (2 ^ [|w_head0 b|] * [|b|] * 2). rewrite <- wB_div_2; try omega. apply Zmult_le_compat;auto with zarith. - pattern 2 at 1;rewrite <- Zpower_exp_1. + pattern 2 at 1;rewrite <- Zpower_1_r. apply Zpower_le_monotone;split;auto with zarith. rewrite <- H4 in H0. assert (Hb3: [|w_head0 b|] <= Zpos w_digits); auto with zarith. @@ -430,13 +429,13 @@ Section GENDIVN1. rewrite spec_0 in H7;rewrite Zmult_0_l in H7;rewrite Zplus_0_l in H7. assert (([|high n a|] / 2 ^ (Zpos w_digits - [|w_head0 b|])) mod wB = [!n|a!] / 2^(Zpos (gen_digits w_digits n) - [|w_head0 b|])). - rewrite Zmod_def_small;auto with zarith. + rewrite Zmod_small;auto with zarith. rewrite spec_high. rewrite Zdiv_Zdiv;auto with zarith. rewrite <- Zpower_exp;auto with zarith. replace (Zpos (gen_digits w_digits n) - Zpos w_digits + (Zpos w_digits - [|w_head0 b|])) with (Zpos (gen_digits w_digits n) - [|w_head0 b|]);trivial;ring. - assert (H8 := Zpower_lt_0 2 (Zpos w_digits - [|w_head0 b|]));auto with zarith. + assert (H8 := Zpower_gt_0 2 (Zpos w_digits - [|w_head0 b|]));auto with zarith. split;auto with zarith. apply Zle_lt_trans with ([|high n a|]);auto with zarith. apply Zdiv_le_upper_bound;auto with zarith. @@ -451,20 +450,20 @@ Section GENDIVN1. rewrite spec_0;rewrite Zmult_0_l;rewrite Zplus_0_l. replace (Zpos w_digits - [|w_sub w_zdigits (w_head0 b)|]) with ([|w_head0 b|]). - rewrite Zmod_def_small;auto with zarith. + rewrite Zmod_small;auto with zarith. assert (H9 := spec_to_Z r). split;auto with zarith. apply Zle_lt_trans with ([|r|]);auto with zarith. apply Zdiv_le_upper_bound;auto with zarith. pattern ([|r|]) at 1;rewrite <- Zmult_1_r. apply Zmult_le_compat;auto with zarith. - assert (H10 := Zpower_lt_0 2 ([|w_head0 b|]));auto with zarith. + assert (H10 := Zpower_gt_0 2 ([|w_head0 b|]));auto with zarith. rewrite spec_sub. - rewrite Zmod_def_small; auto with zarith. + rewrite Zmod_small; auto with zarith. split; auto with zarith. case (spec_to_Z w_zdigits); auto with zarith. rewrite spec_sub. - rewrite Zmod_def_small; auto with zarith. + rewrite Zmod_small; auto with zarith. split; auto with zarith. case (spec_to_Z w_zdigits); auto with zarith. case H7; intros H71 H72. diff --git a/theories/Ints/num/GenLift.v b/theories/Ints/num/GenLift.v index a7d8480ba6..06c76067eb 100644 --- a/theories/Ints/num/GenLift.v +++ b/theories/Ints/num/GenLift.v @@ -10,8 +10,6 @@ Set Implicit Arguments. Require Import ZArith. Require Import ZAux. -Require Import ZPowerAux. -Require Import ZDivModAux. Require Import Basic_type. Require Import GenBase. @@ -283,7 +281,7 @@ Section GenLift. repeat rewrite <- Zmult_assoc. apply f_equal2 with (f := Zmult); auto. case (spec_to_Z (w_tail0 xl)); intros HH3 HH4. - pattern 2 at 2; rewrite <- Zpower_exp_1. + pattern 2 at 2; rewrite <- Zpower_1_r. lazy beta; repeat rewrite <- Zpower_exp; auto with zarith. unfold base; apply f_equal with (f := Zpower 2); auto with zarith. @@ -328,12 +326,12 @@ Section GenLift. fold wB. rewrite Zmult_plus_distr_l;rewrite <- Zmult_assoc;rewrite <- Zplus_assoc. rewrite <- Zpower_2. - rewrite <- wwB_wBwB;apply Zmod_unique with [|xh|]. apply lt_0_wwB. + rewrite <- wwB_wBwB;apply Zmod_unique with [|xh|]. exact (spec_ww_to_Z w_digits w_to_Z spec_to_Z (WW xl yh)). ring. simpl ww_to_Z; w_rewrite;zarith. assert (HH0: [|low p|] = [[p]]). rewrite spec_low. - apply Zmod_def_small. + apply Zmod_small. case (spec_to_w_Z p); intros HH1 HH2; split; auto. generalize H1; unfold zdigits; rewrite spec_w_0W; rewrite spec_zdigits; intros tmp. @@ -370,7 +368,7 @@ Section GenLift. rewrite spec_ww_sub. unfold zdigits; rewrite spec_w_0W; rewrite spec_zdigits. rewrite <- Zmod_div_mod; auto with zarith. - rewrite Zmod_def_small; auto with zarith. + rewrite Zmod_small; auto with zarith. split; auto with zarith. apply Zle_lt_trans with (Zpos w_digits); auto with zarith. unfold base; apply Zpower2_lt_lin; auto with zarith. @@ -407,7 +405,7 @@ Section GenLift. ([|xh|]*2^u*wB). 2:ring. repeat rewrite <- Zplus_assoc. rewrite (Zplus_comm ([|xh|] * 2 ^ u * wB)). - rewrite Z_mod_plus;zarith. rewrite Zmod_mult_0;zarith. + rewrite Z_mod_plus;zarith. rewrite Z_mod_mult;zarith. unfold base;rewrite <- Zmod_shift_r;zarith. fold base;apply Z_mod_lt;zarith. unfold u; split;zarith. split;zarith. unfold u; apply Zdiv_lt_upper_bound;zarith. @@ -450,7 +448,7 @@ Section GenLift. generalize H1; w_rewrite; rewrite spec_zdigits; clear H1; intros H1. assert (HH0: [|low p|] = [[p]]). rewrite spec_low. - apply Zmod_def_small. + apply Zmod_small. case (spec_to_w_Z p); intros HH1 HH2; split; auto. apply Zlt_le_trans with (1 := H1). unfold base; apply Zpower2_le_lin; auto with zarith. @@ -466,7 +464,7 @@ Section GenLift. rewrite spec_low. rewrite spec_ww_sub; w_rewrite; intros H1. rewrite <- Zmod_div_mod; auto with zarith. - rewrite Zmod_def_small; auto with zarith. + rewrite Zmod_small; auto with zarith. split; auto with zarith. apply Zle_lt_trans with (Zpos w_digits); auto with zarith. unfold base; apply Zpower2_lt_lin; auto with zarith. diff --git a/theories/Ints/num/GenMul.v b/theories/Ints/num/GenMul.v index 7550781f16..5522e41bfc 100644 --- a/theories/Ints/num/GenMul.v +++ b/theories/Ints/num/GenMul.v @@ -10,7 +10,6 @@ Set Implicit Arguments. Require Import ZArith. Require Import ZAux. -Require Import ZDivModAux. Require Import Basic_type. Require Import GenBase. @@ -327,7 +326,7 @@ Section GenMul. 2:ring. rewrite <- H1;rewrite <- H;rewrite <- H0. assert (H2 := sum_mul_carry _ _ _ _ _ _ H1). destruct cc as [ | cch ccl]; simpl zn2z_to_Z; simpl ww_to_Z. - rewrite spec_ww_add;rewrite spec_w_W0;rewrite Zmod_def_small; + rewrite spec_ww_add;rewrite spec_w_W0;rewrite Zmod_small; rewrite wwB_wBwB. ring. rewrite <- (Zplus_0_r ([|wc|]*wB));rewrite H;apply mult_add_ineq3;zarith. simpl ww_to_Z in H1. assert (U:=spec_to_Z cch). @@ -349,7 +348,7 @@ Section GenMul. as [l|l];unfold interp_carry;rewrite spec_w_W0;try rewrite Zmult_1_l; simpl zn2z_to_Z; try rewrite spec_ww_add;try rewrite spec_ww_add_carry;rewrite spec_w_WW; - rewrite Zmod_def_small;rewrite wwB_wBwB;intros. + rewrite Zmod_small;rewrite wwB_wBwB;intros. rewrite H4;ring. rewrite H;apply mult_add_ineq2;zarith. rewrite Zplus_assoc;rewrite Zmult_plus_distr_l. rewrite Zmult_1_l;rewrite <- Zplus_assoc;rewrite H4;ring. @@ -385,8 +384,8 @@ Section GenMul. Lemma spec_w_2: [|w_2|] = 2. unfold w_2; rewrite spec_w_add; rewrite spec_w_1; simpl. - apply Zmod_def_small; split; auto with zarith. - rewrite <- (Zpower_exp_1 2); unfold base; apply Zpower_lt_monotone; auto with zarith. + apply Zmod_small; split; auto with zarith. + rewrite <- (Zpower_1_r 2); unfold base; apply Zpower_lt_monotone; auto with zarith. Qed. Lemma kara_prod_aux : forall xh xl yh yl, @@ -410,7 +409,7 @@ Section GenMul. generalize (spec_w_compare yl yh); case (w_compare yl yh); intros Hylh; try rewrite Hylh; try rewrite spec_w_0; try (ring; fail). repeat (rewrite spec_ww_sub || rewrite spec_w_sub || rewrite spec_w_mul_c). - repeat rewrite Zmod_def_small; auto with zarith; try (ring; fail). + repeat rewrite Zmod_small; auto with zarith; try (ring; fail). split; auto with zarith. simpl in Hz; rewrite Hz; rewrite H; rewrite H0. rewrite kara_prod_aux; apply Zplus_le_0_compat; apply Zmult_le_0_compat; auto with zarith. @@ -422,10 +421,10 @@ Section GenMul. intros z1 Hz2 end. simpl in Hz2; rewrite Hz2; repeat (rewrite spec_w_sub || rewrite spec_w_mul_c). - repeat rewrite Zmod_def_small; auto with zarith; try (ring; fail). + repeat rewrite Zmod_small; auto with zarith; try (ring; fail). rewrite spec_w_1; unfold interp_carry in Hz2; rewrite Hz2; repeat (rewrite spec_w_sub || rewrite spec_w_mul_c). - repeat rewrite Zmod_def_small; auto with zarith; try (ring; fail). + repeat rewrite Zmod_small; auto with zarith; try (ring; fail). generalize (spec_w_compare yl yh); case (w_compare yl yh); intros Hylh; try rewrite Hylh; try rewrite spec_w_0; try (ring; fail). match goal with |- context[ww_add_c ?x ?y] => @@ -433,12 +432,12 @@ Section GenMul. intros z1 Hz2 end. simpl in Hz2; rewrite Hz2; repeat (rewrite spec_w_sub || rewrite spec_w_mul_c). - repeat rewrite Zmod_def_small; auto with zarith; try (ring; fail). + repeat rewrite Zmod_small; auto with zarith; try (ring; fail). rewrite spec_w_1; unfold interp_carry in Hz2; rewrite Hz2; repeat (rewrite spec_w_sub || rewrite spec_w_mul_c). - repeat rewrite Zmod_def_small; auto with zarith; try (ring; fail). + repeat rewrite Zmod_small; auto with zarith; try (ring; fail). repeat (rewrite spec_ww_sub || rewrite spec_w_sub || rewrite spec_w_mul_c). - repeat rewrite Zmod_def_small; auto with zarith; try (ring; fail). + repeat rewrite Zmod_small; auto with zarith; try (ring; fail). split. match goal with |- context[(?x - ?y) * (?z - ?t)] => replace ((x - y) * (z - t)) with ((y - x) * (t - z)); [idtac | ring] @@ -459,22 +458,22 @@ Section GenMul. intros z1 Hz2 end. simpl in Hz2; rewrite Hz2; repeat (rewrite spec_w_sub || rewrite spec_w_mul_c). - repeat rewrite Zmod_def_small; auto with zarith; try (ring; fail). + repeat rewrite Zmod_small; auto with zarith; try (ring; fail). rewrite spec_w_0; rewrite Zmult_0_l; rewrite Zplus_0_l. generalize Hz2; clear Hz2; unfold interp_carry. repeat (rewrite spec_w_sub || rewrite spec_w_mul_c). - repeat rewrite Zmod_def_small; auto with zarith; try (ring; fail). + repeat rewrite Zmod_small; auto with zarith; try (ring; fail). match goal with |- context[ww_add_c ?x ?y] => generalize (spec_ww_add_c x y); case (ww_add_c x y); try rewrite spec_w_1; intros z1 Hz2 end. simpl in Hz2; rewrite Hz2; repeat (rewrite spec_w_sub || rewrite spec_w_mul_c). - repeat rewrite Zmod_def_small; auto with zarith; try (ring; fail). + repeat rewrite Zmod_small; auto with zarith; try (ring; fail). rewrite spec_w_2; unfold interp_carry in Hz2. apply trans_equal with (wwB + (1 * wwB + [[z1]])). ring. rewrite Hz2; repeat (rewrite spec_w_sub || rewrite spec_w_mul_c). - repeat rewrite Zmod_def_small; auto with zarith; try (ring; fail). + repeat rewrite Zmod_small; auto with zarith; try (ring; fail). generalize (spec_w_compare yl yh); case (w_compare yl yh); intros Hylh; try rewrite Hylh; try rewrite spec_w_1; try (ring; fail). match goal with |- context[ww_add_c ?x ?y] => @@ -482,25 +481,25 @@ Section GenMul. intros z1 Hz2 end. simpl in Hz2; rewrite Hz2; repeat (rewrite spec_w_sub || rewrite spec_w_mul_c). - repeat rewrite Zmod_def_small; auto with zarith; try (ring; fail). + repeat rewrite Zmod_small; auto with zarith; try (ring; fail). rewrite spec_w_2; unfold interp_carry in Hz2. apply trans_equal with (wwB + (1 * wwB + [[z1]])). ring. rewrite Hz2; repeat (rewrite spec_w_sub || rewrite spec_w_mul_c). - repeat rewrite Zmod_def_small; auto with zarith; try (ring; fail). + repeat rewrite Zmod_small; auto with zarith; try (ring; fail). match goal with |- context[ww_sub_c ?x ?y] => generalize (spec_ww_sub_c x y); case (ww_sub_c x y); try rewrite spec_w_1; intros z1 Hz2 end. simpl in Hz2; rewrite Hz2; repeat (rewrite spec_w_sub || rewrite spec_w_mul_c). - repeat rewrite Zmod_def_small; auto with zarith; try (ring; fail). + repeat rewrite Zmod_small; auto with zarith; try (ring; fail). rewrite spec_w_0; rewrite Zmult_0_l; rewrite Zplus_0_l. match goal with |- context[(?x - ?y) * (?z - ?t)] => replace ((x - y) * (z - t)) with ((y - x) * (t - z)); [idtac | ring] end. generalize Hz2; clear Hz2; unfold interp_carry. repeat (rewrite spec_w_sub || rewrite spec_w_mul_c). - repeat rewrite Zmod_def_small; auto with zarith; try (ring; fail). + repeat rewrite Zmod_small; auto with zarith; try (ring; fail). Qed. Lemma sub_carry : forall xh xl yh yl z, @@ -539,21 +538,21 @@ Section GenMul. assert (U1:= lt_0_wwB w_digits). intros x y; case x; auto; intros xh xl. case y; auto. - simpl; rewrite Zmult_0_r; rewrite Zmod_def_small; auto with zarith. + simpl; rewrite Zmult_0_r; rewrite Zmod_small; auto with zarith. intros yh yl;simpl. repeat (rewrite spec_ww_add || rewrite spec_w_W0 || rewrite spec_w_mul_c || rewrite spec_w_add || rewrite spec_w_mul). - rewrite <- Zmod_plus; auto with zarith. + rewrite <- Zplus_mod; auto with zarith. repeat (rewrite Zmult_plus_distr_l || rewrite Zmult_plus_distr_r). rewrite <- Zmult_mod_distr_r; auto with zarith. rewrite <- Zpower_2; rewrite <- wwB_wBwB; auto with zarith. - rewrite Zmod_plus; auto with zarith. + rewrite Zplus_mod; auto with zarith. rewrite Zmod_mod; auto with zarith. - rewrite <- Zmod_plus; auto with zarith. + rewrite <- Zplus_mod; auto with zarith. match goal with |- ?X mod _ = _ => rewrite <- Z_mod_plus with (a := X) (b := [|xh|] * [|yh|]) end; auto with zarith. - eq_tac; auto; rewrite wwB_wBwB; ring. + f_equal; auto; rewrite wwB_wBwB; ring. Qed. Lemma spec_ww_square_c : forall x, [||ww_square_c x||] = [[x]]*[[x]]. @@ -607,7 +606,7 @@ Section GenMul. rewrite spec_w_0;trivial. assert (U:=spec_w_add_c l r);destruct (w_add_c l r) as [lr|lr];unfold interp_carry in U;try rewrite Zmult_1_l in H;simpl. - rewrite U;ring. rewrite spec_w_succ. rewrite Zmod_def_small. + rewrite U;ring. rewrite spec_w_succ. rewrite Zmod_small. rewrite <- Zplus_assoc;rewrite <- U;ring. simpl in H;assert (H1:= Zmult_lt_b _ _ _ (spec_to_Z x) (spec_to_Z y)). rewrite <- H in H1. diff --git a/theories/Ints/num/GenSqrt.v b/theories/Ints/num/GenSqrt.v index 07b11ad749..3a5b59b6dc 100644 --- a/theories/Ints/num/GenSqrt.v +++ b/theories/Ints/num/GenSqrt.v @@ -10,8 +10,6 @@ Set Implicit Arguments. Require Import ZArith. Require Import ZAux. -Require Import ZDivModAux. -Require Import ZPowerAux. Require Import Basic_type. Require Import GenBase. @@ -277,10 +275,10 @@ Section GenSqrt. clear spec_more_than_1_digit. intros x; case x; simpl ww_is_even. simpl. - rewrite Zmod_def_small; auto with zarith. + rewrite Zmod_small; auto with zarith. intros w1 w2; simpl. unfold base. - rewrite Zmod_plus; auto with zarith. + rewrite Zplus_mod; auto with zarith. rewrite (fun x y => (Zdivide_mod (x * y))); auto with zarith. rewrite Zplus_0_l; rewrite Zmod_mod; auto with zarith. apply spec_w_is_even; auto with zarith. @@ -313,12 +311,12 @@ intros x; case x; simpl ww_is_even. destruct (spec_to_Z a2);auto with zarith. intros H1 H2; split. unfold interp_carry; autorewrite with w_rewrite rm10; auto with zarith. - rewrite H2; rewrite Zmod_def_small; auto with zarith. + rewrite H2; rewrite Zmod_small; auto with zarith. ring. destruct (spec_to_Z a2);auto with zarith. rewrite spec_w_sub; auto with zarith. destruct (spec_to_Z a2) as [H3 H4];auto with zarith. - rewrite Zmod_def_small; auto with zarith. + rewrite Zmod_small; auto with zarith. split; auto with zarith. assert ([|a2|] < 2 * [|b|]); auto with zarith. apply Zlt_le_trans with (2 * (wB / 2)); auto with zarith. @@ -332,7 +330,7 @@ intros x; case x; simpl ww_is_even. intros H1. assert (H2: [|w_sub a1 b|] < [|b|]). rewrite spec_w_sub; auto with zarith. - rewrite Zmod_def_small; auto with zarith. + rewrite Zmod_small; auto with zarith. assert ([|a1|] < 2 * [|b|]); auto with zarith. apply Zlt_le_trans with (2 * (wB / 2)); auto with zarith. rewrite wB_div_2; auto. @@ -344,7 +342,7 @@ intros x; case x; simpl ww_is_even. auto end. intros w0 w1; replace [+|C1 w0|] with (wB + [|w0|]). - rewrite Zmod_def_small; auto with zarith. + rewrite Zmod_small; auto with zarith. intros (H3, H4); split; auto. rewrite Zmult_plus_distr_l. rewrite <- Zplus_assoc; rewrite <- H3; ring. @@ -366,7 +364,7 @@ intros x; case x; simpl ww_is_even. intros w1. assert (Hp: [|w_pred w_zdigits|] = Zpos w_digits - 1). rewrite spec_pred; rewrite spec_w_zdigits. - rewrite Zmod_def_small; auto with zarith. + rewrite Zmod_small; auto with zarith. split; auto with zarith. apply Zlt_le_trans with (Zpos w_digits); auto with zarith. unfold base; apply Zpower2_le_lin; auto with zarith. @@ -375,7 +373,7 @@ intros x; case x; simpl ww_is_even. match goal with |- context[?X - ?Y] => replace (X - Y) with 1 end. - rewrite Zpower_exp_1; rewrite Zmod_def_small; auto with zarith. + rewrite Zpower_1_r; rewrite Zmod_small; auto with zarith. destruct (spec_to_Z w1) as [H1 H2];auto with zarith. split; auto with zarith. apply Zdiv_lt_upper_bound; auto with zarith. @@ -388,7 +386,7 @@ intros x; case x; simpl ww_is_even. intros w1. assert (Hp: [|w_pred w_zdigits|] = Zpos w_digits - 1). rewrite spec_pred; rewrite spec_w_zdigits. - rewrite Zmod_def_small; auto with zarith. + rewrite Zmod_small; auto with zarith. split; auto with zarith. apply Zlt_le_trans with (Zpos w_digits); auto with zarith. unfold base; apply Zpower2_le_lin; auto with zarith. @@ -397,7 +395,8 @@ intros x; case x; simpl ww_is_even. replace (X - Y) with 1 end; rewrite Hp; try ring. rewrite Zpos_minus; auto with zarith. - rewrite Zpower_exp_1; rewrite Zmod_def_small; auto with zarith. + rewrite Zmax_right; auto with zarith. + rewrite Zpower_1_r; rewrite Zmod_small; auto with zarith. destruct (spec_to_Z w1) as [H1 H2];auto with zarith. split; auto with zarith. unfold base. @@ -405,14 +404,14 @@ intros x; case x; simpl ww_is_even. assert (tmp: forall p, 1 + (p - 1) = p); auto with zarith; rewrite <- (tmp X); clear tmp end. - rewrite Zpower_exp; try rewrite Zpower_exp_1; auto with zarith. + rewrite Zpower_exp; try rewrite Zpower_1_r; auto with zarith. assert (tmp: forall p, 1 + (p -1) - 1 = p - 1); auto with zarith; rewrite tmp; clear tmp; auto with zarith. match goal with |- ?X + ?Y < _ => assert (Y < X); auto with zarith end. apply Zdiv_lt_upper_bound; auto with zarith. - pattern 2 at 2; rewrite <- Zpower_exp_1; rewrite <- Zpower_exp; + pattern 2 at 2; rewrite <- Zpower_1_r; rewrite <- Zpower_exp; auto with zarith. assert (tmp: forall p, (p - 1) + 1 = p); auto with zarith; rewrite tmp; clear tmp; auto with zarith. @@ -422,7 +421,7 @@ intros x; case x; simpl ww_is_even. [|w_add_mul_div w_1 w w_0|] = 2 * [|w|] mod wB. intros w1. autorewrite with w_rewrite rm10; auto with zarith. - rewrite Zpower_exp_1; auto with zarith. + rewrite Zpower_1_r; auto with zarith. rewrite Zmult_comm; auto. Qed. @@ -432,7 +431,7 @@ intros x; case x; simpl ww_is_even. rewrite spec_ww_add_mul_div; auto with zarith. autorewrite with w_rewrite rm10. rewrite spec_w_0W; rewrite spec_w_1. - rewrite Zpower_exp_1; auto with zarith. + rewrite Zpower_1_r; auto with zarith. rewrite Zmult_comm; auto. rewrite spec_w_0W; rewrite spec_w_1; auto with zarith. red; simpl; intros; discriminate. @@ -444,22 +443,18 @@ intros x; case x; simpl ww_is_even. intros w1. rewrite spec_ww_add_mul_div; auto with zarith. rewrite spec_w_0W; rewrite spec_w_1; auto with zarith. - rewrite Zpower_exp_1; auto with zarith. - eq_tac; auto. - rewrite Zmult_comm; eq_tac; auto. + rewrite Zpower_1_r; auto with zarith. + f_equal; auto. + rewrite Zmult_comm; f_equal; auto. autorewrite with w_rewrite rm10. unfold ww_digits, base. apply sym_equal; apply Zdiv_unique with (r := 2 ^ (Zpos (ww_digits w_digits) - 1) -1); auto with zarith. - apply Zpower_lt_0; auto with zarith. - match goal with |- 0 <= ?X - 1 => - assert (0 < X); auto with zarith; red; reflexivity - end. unfold ww_digits; split; auto with zarith. match goal with |- 0 <= ?X - 1 => assert (0 < X); auto with zarith end. - apply Zpower_lt_0; auto with zarith. + apply Zpower_gt_0; auto with zarith. match goal with |- 0 <= ?X - 1 => assert (0 < X); auto with zarith; red; reflexivity end. @@ -468,8 +463,8 @@ intros x; case x; simpl ww_is_even. rewrite tmp; clear tmp. assert (tmp: forall p, p + p = 2 * p); auto with zarith; rewrite tmp; clear tmp. - eq_tac; auto. - pattern 2 at 2; rewrite <- Zpower_exp_1; rewrite <- Zpower_exp; + f_equal; auto. + pattern 2 at 2; rewrite <- Zpower_1_r; rewrite <- Zpower_exp; auto with zarith. assert (tmp: forall p, 1 + (p - 1) = p); auto with zarith; rewrite tmp; clear tmp; auto. @@ -480,8 +475,8 @@ intros x; case x; simpl ww_is_even. red; simpl; intros; discriminate. Qed. - Theorem Zmod_plus_one: forall a1 b1, 0 < b1 -> (a1 + b1) mod b1 = a1 mod b1. - intros a1 b1 H; rewrite Zmod_plus; auto with zarith. + Theorem Zplus_mod_one: forall a1 b1, 0 < b1 -> (a1 + b1) mod b1 = a1 mod b1. + intros a1 b1 H; rewrite Zplus_mod; auto with zarith. rewrite Z_mod_same; try rewrite Zplus_0_r; auto with zarith. apply Zmod_mod; auto. Qed. @@ -544,9 +539,10 @@ intros x; case x; simpl ww_is_even. match goal with |- context[_ ^ ?X] => assert (tmp: forall p, 1 + (p - 1) = p); auto with zarith; rewrite <- (tmp X); clear tmp; rewrite Zpower_exp; - try rewrite Zpower_exp_1; auto with zarith + try rewrite Zpower_1_r; auto with zarith end. rewrite Zpos_minus; auto with zarith. + rewrite Zmax_right; auto with zarith. ring. repeat rewrite C0_id. rewrite spec_w_add_c; auto with zarith. @@ -560,9 +556,10 @@ intros x; case x; simpl ww_is_even. match goal with |- context[_ ^ ?X] => assert (tmp: forall p, 1 + (p - 1) = p); auto with zarith; rewrite <- (tmp X); clear tmp; rewrite Zpower_exp; - try rewrite Zpower_exp_1; auto with zarith + try rewrite Zpower_1_r; auto with zarith end. rewrite Zpos_minus; auto with zarith. + rewrite Zmax_right; auto with zarith. ring. repeat rewrite C1_plus_wB in H0. rewrite C1_plus_wB. @@ -573,8 +570,8 @@ intros x; case x; simpl ww_is_even. end. intros c w1; case c. intros w2 (Hw1, Hw2); rewrite C0_id in Hw1. - rewrite <- Zmod_plus_one in Hw1; auto with zarith. - rewrite Zmod_def_small in Hw1; auto with zarith. + rewrite <- Zplus_mod_one in Hw1; auto with zarith. + rewrite Zmod_small in Hw1; auto with zarith. match goal with |- context[w_is_even ?y] => generalize (spec_w_is_even y); case (w_is_even y) @@ -592,9 +589,10 @@ intros x; case x; simpl ww_is_even. match goal with |- context[_ ^ ?X] => assert (tmp: forall p, 1 + (p - 1) = p); auto with zarith; rewrite <- (tmp X); clear tmp; rewrite Zpower_exp; - try rewrite Zpower_exp_1; auto with zarith + try rewrite Zpower_1_r; auto with zarith end. rewrite Zpos_minus; auto with zarith. + rewrite Zmax_right; auto with zarith. ring. repeat rewrite C0_id. rewrite add_mult_div_2_plus_1. @@ -610,9 +608,10 @@ intros x; case x; simpl ww_is_even. match goal with |- context[_ ^ ?X] => assert (tmp: forall p, 1 + (p - 1) = p); auto with zarith; rewrite <- (tmp X); clear tmp; rewrite Zpower_exp; - try rewrite Zpower_exp_1; auto with zarith + try rewrite Zpower_1_r; auto with zarith end. rewrite Zpos_minus; auto with zarith. + rewrite Zmax_right; auto with zarith. ring. split; auto with zarith. destruct (spec_to_Z b);auto with zarith. @@ -620,8 +619,8 @@ intros x; case x; simpl ww_is_even. destruct (spec_to_Z b);auto with zarith. destruct (spec_to_Z b);auto with zarith. intros w2; rewrite C1_plus_wB. - rewrite <- Zmod_plus_one; auto with zarith. - rewrite Zmod_def_small; auto with zarith. + rewrite <- Zplus_mod_one; auto with zarith. + rewrite Zmod_small; auto with zarith. intros (Hw1, Hw2). match goal with |- context[w_is_even ?y] => generalize (spec_w_is_even y); @@ -662,7 +661,7 @@ intros x; case x; simpl ww_is_even. 4 * (2 ^ (Zpos w_digits - 2))). change 4 with (2 ^ 2). rewrite <- Zpower_exp; auto with zarith. - eq_tac; auto with zarith. + f_equal; auto with zarith. rewrite H. rewrite (fun x => (Zmult_comm 4 (2 ^x))). rewrite Z_div_mult; auto with zarith. @@ -670,7 +669,7 @@ intros x; case x; simpl ww_is_even. Theorem Zsquare_mult: forall p, p ^ 2 = p * p. intros p; change 2 with (1 + 1); rewrite Zpower_exp; - try rewrite Zpower_exp_1; auto with zarith. + try rewrite Zpower_1_r; auto with zarith. Qed. Theorem Zsquare_pos: forall p, 0 <= p ^ 2. @@ -817,7 +816,7 @@ intros x; case x; simpl ww_is_even. rewrite spec_ww_pred. rewrite <- Zmod_unique with (q := 1) (r := -wwB + 2 * [[WW w4 w5]]); auto with zarith. - intros Hz1; rewrite Zmod_def_small; auto with zarith. + intros Hz1; rewrite Zmod_small; auto with zarith. match type of H5 with -?X + ?Y = ?Z => assert (V: Y = Z + X); try (rewrite <- H5; ring) @@ -866,7 +865,7 @@ intros x; case x; simpl ww_is_even. rewrite spec_ww_add; auto with zarith. rewrite spec_ww_pred; auto with zarith. rewrite ww_add_mult_mult_2. - assert (VV1 := spec_ww_to_Z w_digits w_to_Z spec_to_Z (WW w4 w5)). + rename V1 into VV1. assert (VV2: 0 < [[WW w4 w5]]); auto with zarith. apply Zlt_le_trans with (wB/ 2 * wB + 0); auto with zarith. autorewrite with rm10; apply Zmult_lt_0_compat; auto with zarith. @@ -886,7 +885,7 @@ intros x; case x; simpl ww_is_even. simpl ww_to_Z; assert (V4 := spec_to_Z w5);auto with zarith. rewrite <- Zmod_unique with (q := 1) (r := -wwB + 2 * [[WW w4 w5]]); auto with zarith. - intros Hz1; rewrite Zmod_def_small; auto with zarith. + intros Hz1; rewrite Zmod_small; auto with zarith. match type of H5 with -?X + ?Y = ?Z => assert (V: Y = Z + X); try (rewrite <- H5; ring) @@ -895,7 +894,7 @@ intros x; case x; simpl ww_is_even. assert (V1: Y = Z - 1); [replace (Z - 1) with (X + (-X + Z -1)); [rewrite <- Hz1 | idtac]; ring - | idtac] + | idtac] end. rewrite <- Zmod_unique with (q := 1) (r := -wwB + [[z1]] + [[z]]); auto with zarith. @@ -1161,24 +1160,24 @@ intros x; case x; simpl ww_is_even. assert (Hp0: 0 < [[ww_head0 x]]). generalize (spec_ww_is_even (ww_head0 x)); rewrite H1. generalize Hv1; case [[ww_head0 x]]. - rewrite Zmod_def_small; auto with zarith. + rewrite Zmod_small; auto with zarith. intros; assert (0 < Zpos p); auto with zarith. red; simpl; auto. intros p H2; case H2; auto. assert (Hp: [[ww_pred (ww_head0 x)]] = [[ww_head0 x]] - 1). rewrite spec_ww_pred. - rewrite Zmod_def_small; auto with zarith. + rewrite Zmod_small; auto with zarith. intros H2; split. generalize (spec_ww_is_even (ww_pred (ww_head0 x))); case ww_is_even; auto. rewrite Hp. - rewrite Zmod_minus; auto with zarith. - rewrite H2; repeat rewrite Zmod_def_small; auto with zarith. + rewrite Zminus_mod; auto with zarith. + rewrite H2; repeat rewrite Zmod_small; auto with zarith. intros H3; rewrite Hp. case (spec_ww_head0 x); auto; intros Hv3 Hv4. assert (Hu: forall u, 0 < u -> 2 * 2 ^ (u - 1) = 2 ^u). intros u Hu. - pattern 2 at 1; rewrite <- Zpower_exp_1. + pattern 2 at 1; rewrite <- Zpower_1_r. rewrite <- Zpower_exp; auto with zarith. ring_simplify (1 + (u - 1)); auto with zarith. split; auto with zarith. @@ -1254,13 +1253,13 @@ intros x; case x; simpl ww_is_even. generalize (spec_ww_add_mul_div x W0 (ww_head1 x) Hv2); case ww_add_mul_div. simpl ww_to_Z; autorewrite with w_rewrite rm10. - rewrite Zmod_def_small; auto with zarith. + rewrite Zmod_small; auto with zarith. intros H2; case (Zmult_integral _ _ (sym_equal H2)); clear H2; intros H2. rewrite H2; unfold Zpower, Zpower_pos; simpl; auto with zarith. match type of H2 with ?X = ?Y => absurd (Y < X); try (rewrite H2; auto with zarith; fail) end. - apply Zpower_lt_0; auto with zarith. + apply Zpower_gt_0; auto with zarith. split; auto with zarith. case Hp2; intros _ tmp; apply Zle_lt_trans with (2 := tmp); clear tmp. @@ -1271,7 +1270,7 @@ intros x; case x; simpl ww_is_even. generalize (spec_ww_is_even (ww_head1 x)); rewrite Hp1; intros tmp; rewrite tmp; rewrite Zplus_0_r; auto. intros w0 w1; autorewrite with w_rewrite rm10. - rewrite Zmod_def_small; auto with zarith. + rewrite Zmod_small; auto with zarith. 2: rewrite Zmult_comm; auto with zarith. intros H2. assert (V: wB/4 <= [|w0|]). @@ -1287,7 +1286,7 @@ intros x; case x; simpl ww_is_even. assert (Hv3: [[ww_pred ww_zdigits]] = Zpos (xO w_digits) - 1). rewrite spec_ww_pred; rewrite spec_ww_zdigits. - rewrite Zmod_def_small; auto with zarith. + rewrite Zmod_small; auto with zarith. split; auto with zarith. apply Zlt_le_trans with (Zpos (xO w_digits)); auto with zarith. unfold base; apply Zpower2_le_lin; auto with zarith. @@ -1303,8 +1302,8 @@ intros x; case x; simpl ww_is_even. simpl ww_to_Z; autorewrite with rm10. rewrite Hv3. ring_simplify (Zpos (xO w_digits) - (Zpos (xO w_digits) - 1)). - rewrite Zpower_exp_1. - rewrite Zmod_def_small; auto with zarith. + rewrite Zpower_1_r. + rewrite Zmod_small; auto with zarith. split; auto with zarith. apply Zlt_le_trans with (1 := Hv4); auto with zarith. unfold base; apply Zpower_le_monotone; auto with zarith. @@ -1313,15 +1312,15 @@ intros x; case x; simpl ww_is_even. assert (Hv6: [|low(ww_add_mul_div (ww_pred ww_zdigits) W0 (ww_head1 x))|] = [[ww_head1 x]]/2). rewrite spec_low. - rewrite Hv5; rewrite Zmod_def_small; auto with zarith. + rewrite Hv5; rewrite Zmod_small; auto with zarith. rewrite spec_w_add_mul_div; auto with zarith. rewrite spec_w_sub; auto with zarith. rewrite spec_w_0. simpl ww_to_Z; autorewrite with rm10. rewrite Hv6; rewrite spec_w_zdigits. - rewrite (fun x y => Zmod_def_small (x - y)). + rewrite (fun x y => Zmod_small (x - y)). ring_simplify (Zpos w_digits - (Zpos w_digits - [[ww_head1 x]] / 2)). - rewrite Zmod_def_small. + rewrite Zmod_small. simpl ww_to_Z in H2; rewrite H2; auto with zarith. intros (H4, H5); split. apply Zmult_le_reg_r with (2 ^ [[ww_head1 x]]); auto with zarith. @@ -1335,7 +1334,7 @@ intros x; case x; simpl ww_is_even. assert (tmp: forall p q, p ^ 2 * q ^ 2 = (p * q) ^2); try (intros; repeat rewrite Zsquare_mult; ring); rewrite tmp; clear tmp. - apply ZPowerAux.Zpower_le_monotone_exp; auto with zarith. + apply Zpower_le_monotone3; auto with zarith. split; auto with zarith. pattern [|w2|] at 2; rewrite (Z_div_mod_eq [|w2|] (2 ^ ([[ww_head1 x]] / 2))); @@ -1361,7 +1360,7 @@ intros x; case x; simpl ww_is_even. assert (tmp: forall p q, p ^ 2 * q ^ 2 = (p * q) ^2); try (intros; repeat rewrite Zsquare_mult; ring); rewrite tmp; clear tmp. - apply ZPowerAux.Zpower_le_monotone_exp; auto with zarith. + apply Zpower_le_monotone3; auto with zarith. split; auto with zarith. pattern [|w2|] at 1; rewrite (Z_div_mod_eq [|w2|] (2 ^ ([[ww_head1 x]]/2))); auto with zarith. @@ -1375,7 +1374,7 @@ intros x; case x; simpl ww_is_even. auto with zarith. apply Zmult_le_compat_l; auto with zarith. apply Zpower_le_monotone; auto with zarith. - rewrite Zpower_exp_0; autorewrite with rm10; auto. + rewrite Zpower_0_r; autorewrite with rm10; auto. split; auto with zarith. rewrite Hv0 in Hv2; rewrite (Zpos_xO w_digits) in Hv2; auto with zarith. apply Zle_lt_trans with (Zpos w_digits); auto with zarith. @@ -1383,7 +1382,7 @@ intros x; case x; simpl ww_is_even. rewrite spec_w_sub; auto with zarith. rewrite Hv6; rewrite spec_w_zdigits; auto with zarith. assert (Hv7: 0 < [[ww_head1 x]]/2); auto with zarith. - rewrite Zmod_def_small; auto with zarith. + rewrite Zmod_small; auto with zarith. split; auto with zarith. assert ([[ww_head1 x]]/2 <= Zpos w_digits); auto with zarith. apply Zmult_le_reg_r with 2; auto with zarith. diff --git a/theories/Ints/num/GenSub.v b/theories/Ints/num/GenSub.v index 43661edd5b..9b09248532 100644 --- a/theories/Ints/num/GenSub.v +++ b/theories/Ints/num/GenSub.v @@ -10,7 +10,6 @@ Set Implicit Arguments. Require Import ZArith. Require Import ZAux. -Require Import ZDivModAux. Require Import Basic_type. Require Import GenBase. @@ -221,7 +220,7 @@ Section GenSub. rewrite H0;rewrite Zplus_0_r; rewrite Zpower_2; rewrite Zmult_mod_distr_r;try apply lt_0_wB. rewrite spec_opp;trivial. - apply Zmod_unique with (q:= -1). apply lt_0_wwB. + apply Zmod_unique with (q:= -1). exact (spec_ww_to_Z w_digits w_to_Z spec_to_Z (WW (w_opp_carry xh) l)). rewrite spec_opp_carry;rewrite wwB_wBwB;ring. Qed. @@ -295,12 +294,12 @@ Section GenSub. Lemma spec_ww_pred : forall x, [[ww_pred x]] = ([[x]] - 1) mod wwB. Proof. destruct x as [ |xh xl];simpl. - apply Zmod_unique with (-1). apply lt_0_wwB. apply spec_ww_to_Z;trivial. + apply Zmod_unique with (-1). apply spec_ww_to_Z;trivial. rewrite spec_ww_Bm1;ring. replace ([|xh|]*wB + [|xl|] - 1) with ([|xh|]*wB + ([|xl|] - 1)). 2:ring. generalize (spec_pred_c xl);destruct (w_pred_c xl) as [l|l];intro H; unfold interp_carry in H;rewrite <- H;simpl ww_to_Z. - rewrite Zmod_def_small. apply spec_w_WW. + rewrite Zmod_small. apply spec_w_WW. exact (spec_ww_to_Z w_digits w_to_Z spec_to_Z (WW xh l)). rewrite Zplus_assoc;rewrite <- Zmult_plus_distr_l. change ([|xh|] + -1) with ([|xh|] - 1). @@ -313,7 +312,7 @@ Section GenSub. Lemma spec_ww_sub : forall x y, [[ww_sub x y]] = ([[x]] - [[y]]) mod wwB. Proof. destruct y as [ |yh yl];simpl. - ring_simplify ([[x]] - 0);rewrite Zmod_def_small;trivial. apply spec_ww_to_Z;trivial. + ring_simplify ([[x]] - 0);rewrite Zmod_small;trivial. apply spec_ww_to_Z;trivial. destruct x as [ |xh xl];simpl. exact (spec_ww_opp (WW yh yl)). replace ([|xh|] * wB + [|xl|] - ([|yh|] * wB + [|yl|])) with (([|xh|] - [|yh|]) * wB + ([|xl|] - [|yl|])). 2:ring. @@ -331,7 +330,7 @@ Section GenSub. destruct y as [ |yh yl];simpl. ring_simplify ([[x]] - 0);exact (spec_ww_pred x). destruct x as [ |xh xl];simpl. - apply Zmod_unique with (-1). apply lt_0_wwB. + apply Zmod_unique with (-1). apply spec_ww_to_Z;trivial. fold (ww_opp_carry (WW yh yl)). rewrite (spec_ww_opp_carry (WW yh yl));simpl ww_to_Z;ring. diff --git a/theories/Ints/num/Nbasic.v b/theories/Ints/num/Nbasic.v index f7731ae6a6..0d85c92ed1 100644 --- a/theories/Ints/num/Nbasic.v +++ b/theories/Ints/num/Nbasic.v @@ -1,6 +1,5 @@ Require Import ZArith. Require Import ZAux. -Require Import ZDivModAux. Require Import Basic_type. Require Import Max. Require Import GenBase. @@ -28,13 +27,13 @@ assert (tmp: (forall p, 2 * p = p + p)%Z); intros p1 Hp1; rewrite F; rewrite (Zpos_xO p1). assert (tmp: (forall p, 2 * p = p + p)%Z); try repeat rewrite tmp; auto with zarith. -rewrite ZPowerAux.Zpower_exp_1; auto with zarith. +rewrite Zpower_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. subst; simpl plength. -rewrite ZPowerAux.Zpower_exp_1; auto with zarith. +rewrite Zpower_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. @@ -296,7 +295,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 ZAux.Zpower_mult; auto with zarith. + rewrite (Zpos_xO n1); rewrite Zmult_comm; rewrite Zpower_mult; auto with zarith. Qed. Let gen_to_Z_pos: forall n x, 0 <= gen_to_Z n x < gen_wB n := diff --git a/theories/Ints/num/Q0Make.v b/theories/Ints/num/Q0Make.v index 326e629024..c39a63301a 100644 --- a/theories/Ints/num/Q0Make.v +++ b/theories/Ints/num/Q0Make.v @@ -2,7 +2,6 @@ Require Import Bool. Require Import ZArith. Require Import Znumtheory. Require Import ZAux. -Require Import ZDivModAux. Require Import Arith. Require Export BigN. Require Export BigZ. diff --git a/theories/Ints/num/QbiMake.v b/theories/Ints/num/QbiMake.v index 53fb65b2a8..fdf8647079 100644 --- a/theories/Ints/num/QbiMake.v +++ b/theories/Ints/num/QbiMake.v @@ -2,7 +2,6 @@ Require Import Bool. Require Import ZArith. Require Import Znumtheory. Require Import ZAux. -Require Import ZDivModAux. Require Import Arith. Require Export BigN. Require Export BigZ. diff --git a/theories/Ints/num/QifMake.v b/theories/Ints/num/QifMake.v index add89898a8..5f461aa59b 100644 --- a/theories/Ints/num/QifMake.v +++ b/theories/Ints/num/QifMake.v @@ -2,7 +2,6 @@ Require Import Bool. Require Import ZArith. Require Import Znumtheory. Require Import ZAux. -Require Import ZDivModAux. Require Import Arith. Require Export BigN. Require Export BigZ. diff --git a/theories/Ints/num/QpMake.v b/theories/Ints/num/QpMake.v index 3c859d0f12..906cf8d159 100644 --- a/theories/Ints/num/QpMake.v +++ b/theories/Ints/num/QpMake.v @@ -2,7 +2,6 @@ Require Import Bool. Require Import ZArith. Require Import Znumtheory. Require Import ZAux. -Require Import ZDivModAux. Require Import Arith. Require Export BigN. Require Export BigZ. diff --git a/theories/Ints/num/QvMake.v b/theories/Ints/num/QvMake.v index eb97123da3..e51291a041 100644 --- a/theories/Ints/num/QvMake.v +++ b/theories/Ints/num/QvMake.v @@ -2,7 +2,6 @@ Require Import Bool. Require Import ZArith. Require Import Znumtheory. Require Import ZAux. -Require Import ZDivModAux. Require Import Arith. Require Export BigN. Require Export BigZ. diff --git a/theories/Ints/num/ZMake.v b/theories/Ints/num/ZMake.v index 0a2b5cd3fd..d00f14ec6c 100644 --- a/theories/Ints/num/ZMake.v +++ b/theories/Ints/num/ZMake.v @@ -1,6 +1,5 @@ Require Import ZArith. Require Import ZAux. -Require Import ZDivModAux. Open Scope Z_scope. diff --git a/theories/Ints/num/Zn2Z.v b/theories/Ints/num/Zn2Z.v index db3f28b418..a244635ea8 100644 --- a/theories/Ints/num/Zn2Z.v +++ b/theories/Ints/num/Zn2Z.v @@ -10,7 +10,6 @@ Set Implicit Arguments. Require Import ZArith. Require Import ZAux. -Require Import ZDivModAux. Require Import Basic_type. Require Import GenBase. Require Import GenAdd. @@ -588,7 +587,7 @@ Section Zn2Z. _ _ _ _ _ _ _ _ _ _ _ _ _ _ _);auto. unfold w_Bm2, w_to_Z, w_pred, w_Bm1. rewrite (spec_pred op_spec);rewrite (spec_Bm1 op_spec). - unfold w_digits;rewrite Zmod_def_small. ring. + unfold w_digits;rewrite Zmod_small. ring. assert (H:= wB_pos(znz_digits w_op)). omega. exact (spec_WW op_spec). exact (spec_compare op_spec). exact (spec_mul_c op_spec). exact (spec_div21 op_spec). @@ -621,12 +620,12 @@ Section Zn2Z. w_to_Z (low x) = [|x|] mod wB. intros x; case x; simpl low. unfold ww_to_Z, w_to_Z, w_0; rewrite (spec_0 op_spec); simpl. - rewrite Zmod_def_small; auto with zarith. + rewrite Zmod_small; auto with zarith. split; auto with zarith. unfold wB, base; auto with zarith. intros xh xl; simpl. rewrite Zplus_comm; rewrite Z_mod_plus; auto with zarith. - rewrite Zmod_def_small; auto with zarith. + rewrite Zmod_small; auto with zarith. unfold wB, base; auto with zarith. Qed. diff --git a/theories/Ints/num/ZnZ.v b/theories/Ints/num/ZnZ.v index 68f1092cdf..61d1ced604 100644 --- a/theories/Ints/num/ZnZ.v +++ b/theories/Ints/num/ZnZ.v @@ -8,7 +8,6 @@ Set Implicit Arguments. -Require Import Tactic. Require Import ZArith. Require Import Znumtheory. Require Import Basic_type. |