diff options
author | Stephane Glondu <steph@glondu.net> | 2013-05-08 18:03:54 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2013-05-08 18:03:54 +0200 |
commit | db38bb4ad9aff74576d3b7f00028d48f0447d5bd (patch) | |
tree | 09dafc3e5c7361d3a28e93677eadd2b7237d4f9f /theories/Numbers/Cyclic/DoubleCyclic | |
parent | 6e34b272d789455a9be589e27ad3a998cf25496b (diff) | |
parent | 499a11a45b5711d4eaabe84a80f0ad3ae539d500 (diff) |
Merge branch 'experimental/upstream' into upstream
Diffstat (limited to 'theories/Numbers/Cyclic/DoubleCyclic')
-rw-r--r-- | theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v | 52 | ||||
-rw-r--r-- | theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v | 173 | ||||
-rw-r--r-- | theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v | 445 | ||||
-rw-r--r-- | theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v | 350 | ||||
-rw-r--r-- | theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v | 198 | ||||
-rw-r--r-- | theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.v | 204 | ||||
-rw-r--r-- | theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.v | 95 | ||||
-rw-r--r-- | theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v | 410 | ||||
-rw-r--r-- | theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.v | 28 | ||||
-rw-r--r-- | theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v | 8 |
10 files changed, 923 insertions, 1040 deletions
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v index 305d77a9..35d8b595 100644 --- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v +++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <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 *) @@ -8,8 +8,6 @@ (* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) (************************************************************************) -(*i $Id: DoubleAdd.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - Set Implicit Arguments. Require Import ZArith. @@ -184,7 +182,7 @@ Section DoubleAdd. destruct x as [ |xh xl];simpl. apply spec_ww_1. generalize (spec_w_succ_c xl);destruct (w_succ_c xl) as [l|l]; intro H;unfold interp_carry in H. simpl;rewrite H;ring. - rewrite <- Zplus_assoc;rewrite <- H;rewrite Zmult_1_l. + rewrite <- Z.add_assoc;rewrite <- H;rewrite Z.mul_1_l. assert ([|l|] = 0). generalize (spec_to_Z xl)(spec_to_Z l);omega. rewrite H0;generalize (spec_w_succ_c xh);destruct (w_succ_c xh) as [h|h]; intro H1;unfold interp_carry in H1. @@ -197,19 +195,19 @@ Section DoubleAdd. Lemma spec_ww_add_c : forall x y, [+[ww_add_c x y]] = [[x]] + [[y]]. Proof. destruct x as [ |xh xl];simpl;trivial. - destruct y as [ |yh yl];simpl. rewrite Zplus_0_r;trivial. + destruct y as [ |yh yl];simpl. rewrite Z.add_0_r;trivial. replace ([|xh|] * wB + [|xl|] + ([|yh|] * wB + [|yl|])) with (([|xh|]+[|yh|])*wB + ([|xl|]+[|yl|])). 2:ring. generalize (spec_w_add_c xl yl);destruct (w_add_c xl yl) as [l|l]; intros H;unfold interp_carry in H;rewrite <- H. generalize (spec_w_add_c xh yh);destruct (w_add_c xh yh) as [h|h]; intros H1;unfold interp_carry in *;rewrite <- H1. trivial. - repeat rewrite Zmult_1_l;rewrite spec_w_WW;rewrite wwB_wBwB; ring. - rewrite Zplus_assoc;rewrite <- Zmult_plus_distr_l. + repeat rewrite Z.mul_1_l;rewrite spec_w_WW;rewrite wwB_wBwB; ring. + rewrite Z.add_assoc;rewrite <- Z.mul_add_distr_r. generalize (spec_w_add_carry_c xh yh);destruct (w_add_carry_c xh yh) as [h|h]; intros H1;unfold interp_carry in *;rewrite <- H1. simpl;ring. - repeat rewrite Zmult_1_l;rewrite wwB_wBwB;rewrite spec_w_WW;ring. + repeat rewrite Z.mul_1_l;rewrite wwB_wBwB;rewrite spec_w_WW;ring. Qed. Section Cont. @@ -223,23 +221,23 @@ Section DoubleAdd. destruct x as [ |xh xl];simpl;trivial. apply spec_f0;trivial. destruct y as [ |yh yl];simpl. - apply spec_f0;simpl;rewrite Zplus_0_r;trivial. + apply spec_f0;simpl;rewrite Z.add_0_r;trivial. generalize (spec_w_add_c xl yl);destruct (w_add_c xl yl) as [l|l]; intros H;unfold interp_carry in H. generalize (spec_w_add_c xh yh);destruct (w_add_c xh yh) as [h|h]; intros H1;unfold interp_carry in *. apply spec_f0. simpl;rewrite H;rewrite H1;ring. apply spec_f1. simpl;rewrite spec_w_WW;rewrite H. - rewrite Zplus_assoc;rewrite wwB_wBwB. rewrite Zpower_2; rewrite <- Zmult_plus_distr_l. - rewrite Zmult_1_l in H1;rewrite H1;ring. + rewrite Z.add_assoc;rewrite wwB_wBwB. rewrite Z.pow_2_r; rewrite <- Z.mul_add_distr_r. + rewrite Z.mul_1_l in H1;rewrite H1;ring. generalize (spec_w_add_carry_c xh yh);destruct (w_add_carry_c xh yh) as [h|h]; intros H1;unfold interp_carry in *. - apply spec_f0;simpl;rewrite H1. rewrite Zmult_plus_distr_l. - rewrite <- Zplus_assoc;rewrite H;ring. + apply spec_f0;simpl;rewrite H1. rewrite Z.mul_add_distr_r. + rewrite <- Z.add_assoc;rewrite H;ring. apply spec_f1. simpl;rewrite spec_w_WW;rewrite wwB_wBwB. - rewrite Zplus_assoc; rewrite Zpower_2; rewrite <- Zmult_plus_distr_l. - rewrite Zmult_1_l in H1;rewrite H1. rewrite Zmult_plus_distr_l. - rewrite <- Zplus_assoc;rewrite H;ring. + rewrite Z.add_assoc; rewrite Z.pow_2_r; rewrite <- Z.mul_add_distr_r. + rewrite Z.mul_1_l in H1;rewrite H1. rewrite Z.mul_add_distr_r. + rewrite <- Z.add_assoc;rewrite H;ring. Qed. End Cont. @@ -250,19 +248,19 @@ Section DoubleAdd. destruct x as [ |xh xl];intro y;simpl. exact (spec_ww_succ_c y). destruct y as [ |yh yl];simpl. - rewrite Zplus_0_r;exact (spec_ww_succ_c (WW xh xl)). + rewrite Z.add_0_r;exact (spec_ww_succ_c (WW xh xl)). replace ([|xh|] * wB + [|xl|] + ([|yh|] * wB + [|yl|]) + 1) with (([|xh|]+[|yh|])*wB + ([|xl|]+[|yl|]+1)). 2:ring. generalize (spec_w_add_carry_c xl yl);destruct (w_add_carry_c xl yl) as [l|l];intros H;unfold interp_carry in H;rewrite <- H. generalize (spec_w_add_c xh yh);destruct (w_add_c xh yh) as [h|h]; intros H1;unfold interp_carry in H1;rewrite <- H1. trivial. - unfold interp_carry;repeat rewrite Zmult_1_l;simpl;rewrite wwB_wBwB;ring. - rewrite Zplus_assoc;rewrite <- Zmult_plus_distr_l. + unfold interp_carry;repeat rewrite Z.mul_1_l;simpl;rewrite wwB_wBwB;ring. + rewrite Z.add_assoc;rewrite <- Z.mul_add_distr_r. generalize (spec_w_add_carry_c xh yh);destruct (w_add_carry_c xh yh) as [h|h];intros H1;unfold interp_carry in H1;rewrite <- H1. trivial. unfold interp_carry;rewrite spec_w_WW; - repeat rewrite Zmult_1_l;simpl;rewrite wwB_wBwB;ring. + repeat rewrite Z.mul_1_l;simpl;rewrite wwB_wBwB;ring. Qed. Lemma spec_ww_succ : forall x, [[ww_succ x]] = ([[x]] + 1) mod wwB. @@ -270,14 +268,14 @@ Section DoubleAdd. destruct x as [ |xh xl];simpl. rewrite spec_ww_1;rewrite Zmod_small;trivial. split;[intro;discriminate|apply wwB_pos]. - rewrite <- Zplus_assoc;generalize (spec_w_succ_c xl); + rewrite <- Z.add_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_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. - rewrite H0;rewrite Zplus_0_r;rewrite <- Zmult_plus_distr_l;rewrite wwB_wBwB. - rewrite Zpower_2; rewrite Zmult_mod_distr_r;try apply lt_0_wB. + rewrite H0;rewrite Z.add_0_r;rewrite <- Z.mul_add_distr_r;rewrite wwB_wBwB. + rewrite Z.pow_2_r; rewrite Zmult_mod_distr_r;try apply lt_0_wB. rewrite spec_w_W0;rewrite spec_w_succ;trivial. Qed. @@ -286,7 +284,7 @@ Section DoubleAdd. destruct x as [ |xh xl];intros y;simpl. rewrite Zmod_small;trivial. apply spec_ww_to_Z;trivial. destruct y as [ |yh yl]. - change [[W0]] with 0;rewrite Zplus_0_r. + change [[W0]] with 0;rewrite Z.add_0_r. 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|])) @@ -294,7 +292,7 @@ Section DoubleAdd. generalize (spec_w_add_c xl yl);destruct (w_add_c xl yl) as [l|l]; unfold interp_carry;intros H;simpl;rewrite <- H. rewrite (mod_wwB w_digits w_to_Z spec_to_Z);rewrite spec_w_add;trivial. - rewrite Zplus_assoc;rewrite <- Zmult_plus_distr_l. + rewrite Z.add_assoc;rewrite <- Z.mul_add_distr_r. rewrite(mod_wwB w_digits w_to_Z spec_to_Z);rewrite spec_w_add_carry;trivial. Qed. @@ -304,13 +302,13 @@ Section DoubleAdd. destruct x as [ |xh xl];intros y;simpl. exact (spec_ww_succ y). destruct y as [ |yh yl]. - change [[W0]] with 0;rewrite Zplus_0_r. exact (spec_ww_succ (WW xh xl)). + change [[W0]] with 0;rewrite Z.add_0_r. exact (spec_ww_succ (WW xh xl)). simpl;replace ([|xh|] * wB + [|xl|] + ([|yh|] * wB + [|yl|]) + 1) with (([|xh|]+[|yh|])*wB + ([|xl|]+[|yl|]+1)). 2:ring. generalize (spec_w_add_carry_c xl yl);destruct (w_add_carry_c xl yl) as [l|l];unfold interp_carry;intros H;rewrite <- H;simpl ww_to_Z. rewrite(mod_wwB w_digits w_to_Z spec_to_Z);rewrite spec_w_add;trivial. - rewrite Zplus_assoc;rewrite <- Zmult_plus_distr_l. + rewrite Z.add_assoc;rewrite <- Z.mul_add_distr_r. rewrite(mod_wwB w_digits w_to_Z spec_to_Z);rewrite spec_w_add_carry;trivial. Qed. diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v index 3d44f96b..ed69a8f5 100644 --- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v +++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <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 *) @@ -8,16 +8,16 @@ (* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) (************************************************************************) -(*i $Id: DoubleBase.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - Set Implicit Arguments. -Require Import ZArith. +Require Import ZArith Ndigits. Require Import BigNumPrelude. Require Import DoubleType. Local Open Scope Z_scope. +Local Infix "<<" := Pos.shiftl_nat (at level 30). + Section DoubleBase. Variable w : Type. Variable w_0 : w. @@ -70,13 +70,7 @@ Section DoubleBase. end end. - Fixpoint double_digits (n:nat) : positive := - match n with - | O => w_digits - | S n => xO (double_digits n) - end. - - Definition double_wB n := base (double_digits n). + Definition double_wB n := base (w_digits << n). Fixpoint double_to_Z (n:nat) : word w n -> Z := match n return word w n -> Z with @@ -167,17 +161,13 @@ Section DoubleBase. Variable spec_w_0W : forall l, [[w_0W l]] = [|l|]. Variable spec_to_Z : forall x, 0 <= [|x|] < wB. Variable spec_w_compare : forall x y, - match w_compare x y with - | Eq => [|x|] = [|y|] - | Lt => [|x|] < [|y|] - | Gt => [|x|] > [|y|] - end. + w_compare x y = Z.compare [|x|] [|y|]. Lemma wwB_wBwB : wwB = wB^2. Proof. - unfold base, ww_digits;rewrite Zpower_2; rewrite (Zpos_xO w_digits). + unfold base, ww_digits;rewrite Z.pow_2_r; rewrite (Pos2Z.inj_xO w_digits). replace (2 * Zpos w_digits) with (Zpos w_digits + Zpos w_digits). - apply Zpower_exp; unfold Zge;simpl;intros;discriminate. + apply Zpower_exp; unfold Z.ge;simpl;intros;discriminate. ring. Qed. @@ -189,28 +179,28 @@ Section DoubleBase. Lemma lt_0_wB : 0 < wB. Proof. - unfold base;apply Zpower_gt_0. unfold Zlt;reflexivity. - unfold Zle;intros H;discriminate H. + unfold base;apply Z.pow_pos_nonneg. unfold Z.lt;reflexivity. + unfold Z.le;intros H;discriminate H. Qed. Lemma lt_0_wwB : 0 < wwB. - Proof. rewrite wwB_wBwB; rewrite Zpower_2; apply Zmult_lt_0_compat;apply lt_0_wB. Qed. + Proof. rewrite wwB_wBwB; rewrite Z.pow_2_r; apply Z.mul_pos_pos;apply lt_0_wB. Qed. Lemma wB_pos: 1 < wB. Proof. - unfold base;apply Zlt_le_trans with (2^1). unfold Zlt;reflexivity. - apply Zpower_le_monotone. unfold Zlt;reflexivity. - split;unfold Zle;intros H. discriminate H. + unfold base;apply Z.lt_le_trans with (2^1). unfold Z.lt;reflexivity. + apply Zpower_le_monotone. unfold Z.lt;reflexivity. + split;unfold Z.le;intros H. discriminate H. clear spec_w_0W w_0W spec_w_Bm1 spec_to_Z spec_w_WW w_WW. destruct w_digits; discriminate H. Qed. Lemma wwB_pos: 1 < wwB. Proof. - assert (H:= wB_pos);rewrite wwB_wBwB;rewrite <-(Zmult_1_r 1). - rewrite Zpower_2. - apply Zmult_lt_compat2;(split;[unfold Zlt;reflexivity|trivial]). - apply Zlt_le_weak;trivial. + assert (H:= wB_pos);rewrite wwB_wBwB;rewrite <-(Z.mul_1_r 1). + rewrite Z.pow_2_r. + apply Zmult_lt_compat2;(split;[unfold Z.lt;reflexivity|trivial]). + apply Z.lt_le_incl;trivial. Qed. Theorem wB_div_2: 2 * (wB / 2) = wB. @@ -218,22 +208,22 @@ Section DoubleBase. 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_1_r. + pattern 2 at 2; rewrite <- Z.pow_1_r. rewrite <- Zpower_exp; auto with zarith. f_equal; auto with zarith. case w_digits; compute; intros; discriminate. rewrite H; f_equal; auto with zarith. - rewrite Zmult_comm; apply Z_div_mult; auto with zarith. + rewrite Z.mul_comm; apply Z_div_mult; auto with zarith. Qed. Theorem wwB_div_2 : wwB / 2 = wB / 2 * wB. Proof. 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. - rewrite wwB_wBwB; rewrite Zpower_2. + rewrite wwB_wBwB; rewrite Z.pow_2_r. pattern wB at 1; rewrite <- wB_div_2; auto. - rewrite <- Zmult_assoc. - repeat (rewrite (Zmult_comm 2); rewrite Z_div_mult); auto with zarith. + rewrite <- Z.mul_assoc. + repeat (rewrite (Z.mul_comm 2); rewrite Z_div_mult); auto with zarith. Qed. Lemma mod_wwB : forall z x, @@ -241,15 +231,15 @@ Section DoubleBase. Proof. intros z x. rewrite Zplus_mod. - pattern wwB at 1;rewrite wwB_wBwB; rewrite Zpower_2. + pattern wwB at 1;rewrite wwB_wBwB; rewrite Z.pow_2_r. rewrite Zmult_mod_distr_r;try apply lt_0_wB. 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. + apply Z_mod_lt;apply Z.lt_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]. + rewrite Z.pow_2_r;rewrite <- (Z.add_0_r (wB*wB));apply beta_lex_inv. + apply lt_0_wB. apply spec_to_Z. split;[apply Z.le_refl | apply lt_0_wB]. Qed. Lemma wB_div : forall x y, ([|x|] * wB + [|y|]) / wB = [|x|]. @@ -275,33 +265,32 @@ Section DoubleBase. clear spec_w_0 spec_w_1 spec_w_Bm1 w_0 w_1 w_Bm1. unfold base;apply Zpower_lt_monotone;auto with zarith. assert (0 < Zpos w_digits). compute;reflexivity. - unfold ww_digits;rewrite Zpos_xO;auto with zarith. + unfold ww_digits;rewrite Pos2Z.inj_xO;auto with zarith. Qed. Lemma w_to_Z_wwB : forall x, x < wB -> x < wwB. Proof. - intros x H;apply Zlt_trans with wB;trivial;apply lt_wB_wwB. + intros x H;apply Z.lt_trans with wB;trivial;apply lt_wB_wwB. Qed. Lemma spec_ww_to_Z : forall x, 0 <= [[x]] < wwB. Proof. clear spec_w_0 spec_w_1 spec_w_Bm1 w_0 w_1 w_Bm1. destruct x as [ |h l];simpl. - split;[apply Zle_refl|apply lt_0_wwB]. + split;[apply Z.le_refl|apply lt_0_wwB]. assert (H:=spec_to_Z h);assert (L:=spec_to_Z l);split. - apply Zplus_le_0_compat;auto with zarith. - rewrite <- (Zplus_0_r wwB);rewrite wwB_wBwB; rewrite Zpower_2; + apply Z.add_nonneg_nonneg;auto with zarith. + rewrite <- (Z.add_0_r wwB);rewrite wwB_wBwB; rewrite Z.pow_2_r; apply beta_lex_inv;auto with zarith. Qed. Lemma double_wB_wwB : forall n, double_wB n * double_wB n = double_wB (S n). Proof. intros n;unfold double_wB;simpl. - unfold base;rewrite (Zpos_xO (double_digits n)). - replace (2 * Zpos (double_digits n)) with - (Zpos (double_digits n) + Zpos (double_digits n)). + unfold base. rewrite Pshiftl_nat_S, (Pos2Z.inj_xO (_ << _)). + replace (2 * Zpos (w_digits << n)) with + (Zpos (w_digits << n) + Zpos (w_digits << n)) by ring. symmetry; apply Zpower_exp;intro;discriminate. - ring. Qed. Lemma double_wB_pos: @@ -315,16 +304,16 @@ Section DoubleBase. Proof. clear spec_w_0 spec_w_1 spec_w_Bm1 w_0 w_1 w_Bm1. intros n; elim n; clear n; auto. - unfold double_wB, double_digits; auto with zarith. + unfold double_wB, "<<"; auto with zarith. intros n H1; rewrite <- double_wB_wwB. - apply Zle_trans with (wB * 1). - rewrite Zmult_1_r; apply Zle_refl. - apply Zmult_le_compat; auto with zarith. - apply Zle_trans with wB; auto with zarith. - unfold base. - rewrite <- (Zpower_0_r 2). - apply Zpower_le_monotone2; auto with zarith. + apply Z.le_trans with (wB * 1). + rewrite Z.mul_1_r; apply Z.le_refl. unfold base; auto with zarith. + apply Z.mul_le_mono_nonneg; auto with zarith. + apply Z.le_trans with wB; auto with zarith. + unfold base. + rewrite <- (Z.pow_0_r 2). + apply Z.pow_le_mono_r; auto with zarith. Qed. Lemma spec_double_to_Z : @@ -337,9 +326,9 @@ Section DoubleBase. unfold double_wB,base;split;auto with zarith. assert (U0:= IHn w0);assert (U1:= IHn w1). split;auto with zarith. - apply Zlt_le_trans with ((double_wB n - 1) * double_wB n + double_wB n). + apply Z.lt_le_trans with ((double_wB n - 1) * double_wB n + double_wB n). assert (double_to_Z n w0*double_wB n <= (double_wB n - 1)*double_wB n). - apply Zmult_le_compat_r;auto with zarith. + apply Z.mul_le_mono_nonneg_r;auto with zarith. auto with zarith. rewrite <- double_wB_wwB. replace ((double_wB n - 1) * double_wB n + double_wB n) with (double_wB n * double_wB n); @@ -353,22 +342,19 @@ Section DoubleBase. clear spec_w_1 spec_w_Bm1. intros n; elim n; auto; clear n. intros n Hrec x; case x; clear x; auto. - intros xx yy H1; simpl in H1. - assert (F1: [!n | xx!] = 0). - case (Zle_lt_or_eq 0 ([!n | xx!])); auto. - case (spec_double_to_Z n xx); auto. - intros F2. - assert (F3 := double_wB_more_digits n). - assert (F4: 0 <= [!n | yy!]). - case (spec_double_to_Z n yy); auto. + intros xx yy; simpl. + destruct (spec_double_to_Z n xx) as [F1 _]. Z.le_elim F1. + - (* 0 < [!n | xx!] *) + intros; exfalso. + assert (F3 := double_wB_more_digits n). + destruct (spec_double_to_Z n yy) as [F4 _]. assert (F5: 1 * wB <= [!n | xx!] * double_wB n); auto with zarith. - apply Zmult_le_compat; auto with zarith. + apply Z.mul_le_mono_nonneg; auto with zarith. unfold base; auto with zarith. - simpl get_low; simpl double_to_Z. - generalize H1; clear H1. - rewrite F1; rewrite Zmult_0_l; rewrite Zplus_0_l. - intros H1; apply Hrec; auto. + - (* 0 = [!n | xx!] *) + rewrite <- F1; rewrite Z.mul_0_l, Z.add_0_l. + intros; apply Hrec; auto. Qed. Lemma spec_double_WW : forall n (h l : word w n), @@ -408,35 +394,40 @@ Section DoubleBase. intros a b c d H1; apply beta_lex_inv with (1 := H1); auto. Qed. + Ltac comp2ord := match goal with + | |- Lt = (?x ?= ?y) => symmetry; change (x < y) + | |- Gt = (?x ?= ?y) => symmetry; change (x > y); apply Z.lt_gt + end. + Lemma spec_ww_compare : forall x y, - match ww_compare x y with - | Eq => [[x]] = [[y]] - | Lt => [[x]] < [[y]] - | Gt => [[x]] > [[y]] - end. + ww_compare x y = Z.compare [[x]] [[y]]. Proof. destruct x as [ |xh xl];destruct y as [ |yh yl];simpl;trivial. - generalize (spec_w_compare w_0 yh);destruct (w_compare w_0 yh); - intros H;rewrite spec_w_0 in H. - rewrite <- H;simpl;rewrite <- spec_w_0;apply spec_w_compare. - change 0 with (0*wB+0);pattern 0 at 2;rewrite <- spec_w_0. + (* 1st case *) + rewrite 2 spec_w_compare, spec_w_0. + destruct (Z.compare_spec 0 [|yh|]) as [H|H|H]. + rewrite <- H;simpl. reflexivity. + symmetry. change (0 < [|yh|]*wB+[|yl|]). + change 0 with (0*wB+0). rewrite <- spec_w_0 at 2. apply wB_lex_inv;trivial. - absurd (0 <= [|yh|]). apply Zgt_not_le;trivial. + absurd (0 <= [|yh|]). apply Z.lt_nge; trivial. destruct (spec_to_Z yh);trivial. - generalize (spec_w_compare xh w_0);destruct (w_compare xh w_0); - intros H;rewrite spec_w_0 in H. - rewrite H;simpl;rewrite <- spec_w_0;apply spec_w_compare. - absurd (0 <= [|xh|]). apply Zgt_not_le;apply Zlt_gt;trivial. + (* 2nd case *) + rewrite 2 spec_w_compare, spec_w_0. + destruct (Z.compare_spec [|xh|] 0) as [H|H|H]. + rewrite H;simpl;reflexivity. + absurd (0 <= [|xh|]). apply Z.lt_nge; trivial. destruct (spec_to_Z xh);trivial. - apply Zlt_gt;change 0 with (0*wB+0);pattern 0 at 2;rewrite <- spec_w_0. - apply wB_lex_inv;apply Zgt_lt;trivial. - - generalize (spec_w_compare xh yh);destruct (w_compare xh yh);intros H. - rewrite H;generalize (spec_w_compare xl yl);destruct (w_compare xl yl); - intros H1;[rewrite H1|apply Zplus_lt_compat_l|apply Zplus_gt_compat_l]; - trivial. + comp2ord. + change 0 with (0*wB+0). rewrite <- spec_w_0 at 2. apply wB_lex_inv;trivial. - apply Zlt_gt;apply wB_lex_inv;apply Zgt_lt;trivial. + (* 3rd case *) + rewrite 2 spec_w_compare. + destruct (Z.compare_spec [|xh|] [|yh|]) as [H|H|H]. + rewrite H. + symmetry. apply Z.add_compare_mono_l. + comp2ord. apply wB_lex_inv;trivial. + comp2ord. apply wB_lex_inv;trivial. Qed. diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v index 006da1b3..35fe948e 100644 --- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v +++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <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 *) @@ -8,8 +8,6 @@ (* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) (************************************************************************) -(*i $Id: DoubleCyclic.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - Set Implicit Arguments. Require Import ZArith. @@ -30,65 +28,65 @@ Local Open Scope Z_scope. Section Z_2nZ. - Variable w : Type. - Variable w_op : znz_op w. - Let w_digits := w_op.(znz_digits). - Let w_zdigits := w_op.(znz_zdigits). + Context {t : Type}{ops : ZnZ.Ops t}. + + Let w_digits := ZnZ.digits. + Let w_zdigits := ZnZ.zdigits. - Let w_to_Z := w_op.(znz_to_Z). - Let w_of_pos := w_op.(znz_of_pos). - Let w_head0 := w_op.(znz_head0). - Let w_tail0 := w_op.(znz_tail0). + Let w_to_Z := ZnZ.to_Z. + Let w_of_pos := ZnZ.of_pos. + Let w_head0 := ZnZ.head0. + Let w_tail0 := ZnZ.tail0. - Let w_0 := w_op.(znz_0). - Let w_1 := w_op.(znz_1). - Let w_Bm1 := w_op.(znz_Bm1). + Let w_0 := ZnZ.zero. + Let w_1 := ZnZ.one. + Let w_Bm1 := ZnZ.minus_one. - Let w_compare := w_op.(znz_compare). - Let w_eq0 := w_op.(znz_eq0). + Let w_compare := ZnZ.compare. + Let w_eq0 := ZnZ.eq0. - Let w_opp_c := w_op.(znz_opp_c). - Let w_opp := w_op.(znz_opp). - Let w_opp_carry := w_op.(znz_opp_carry). + Let w_opp_c := ZnZ.opp_c. + Let w_opp := ZnZ.opp. + Let w_opp_carry := ZnZ.opp_carry. - Let w_succ_c := w_op.(znz_succ_c). - Let w_add_c := w_op.(znz_add_c). - Let w_add_carry_c := w_op.(znz_add_carry_c). - Let w_succ := w_op.(znz_succ). - Let w_add := w_op.(znz_add). - Let w_add_carry := w_op.(znz_add_carry). + Let w_succ_c := ZnZ.succ_c. + Let w_add_c := ZnZ.add_c. + Let w_add_carry_c := ZnZ.add_carry_c. + Let w_succ := ZnZ.succ. + Let w_add := ZnZ.add. + Let w_add_carry := ZnZ.add_carry. - Let w_pred_c := w_op.(znz_pred_c). - Let w_sub_c := w_op.(znz_sub_c). - Let w_sub_carry_c := w_op.(znz_sub_carry_c). - Let w_pred := w_op.(znz_pred). - Let w_sub := w_op.(znz_sub). - Let w_sub_carry := w_op.(znz_sub_carry). + Let w_pred_c := ZnZ.pred_c. + Let w_sub_c := ZnZ.sub_c. + Let w_sub_carry_c := ZnZ.sub_carry_c. + Let w_pred := ZnZ.pred. + Let w_sub := ZnZ.sub. + Let w_sub_carry := ZnZ.sub_carry. - Let w_mul_c := w_op.(znz_mul_c). - Let w_mul := w_op.(znz_mul). - Let w_square_c := w_op.(znz_square_c). + Let w_mul_c := ZnZ.mul_c. + Let w_mul := ZnZ.mul. + Let w_square_c := ZnZ.square_c. - Let w_div21 := w_op.(znz_div21). - Let w_div_gt := w_op.(znz_div_gt). - Let w_div := w_op.(znz_div). + Let w_div21 := ZnZ.div21. + Let w_div_gt := ZnZ.div_gt. + Let w_div := ZnZ.div. - Let w_mod_gt := w_op.(znz_mod_gt). - Let w_mod := w_op.(znz_mod). + Let w_mod_gt := ZnZ.modulo_gt. + Let w_mod := ZnZ.modulo. - Let w_gcd_gt := w_op.(znz_gcd_gt). - Let w_gcd := w_op.(znz_gcd). + Let w_gcd_gt := ZnZ.gcd_gt. + Let w_gcd := ZnZ.gcd. - Let w_add_mul_div := w_op.(znz_add_mul_div). + Let w_add_mul_div := ZnZ.add_mul_div. - Let w_pos_mod := w_op.(znz_pos_mod). + Let w_pos_mod := ZnZ.pos_mod. - Let w_is_even := w_op.(znz_is_even). - Let w_sqrt2 := w_op.(znz_sqrt2). - Let w_sqrt := w_op.(znz_sqrt). + Let w_is_even := ZnZ.is_even. + Let w_sqrt2 := ZnZ.sqrt2. + Let w_sqrt := ZnZ.sqrt. - Let _zn2z := zn2z w. + Let _zn2z := zn2z t. Let wB := base w_digits. @@ -105,9 +103,9 @@ Section Z_2nZ. Let to_Z := zn2z_to_Z wB w_to_Z. - Let w_W0 := znz_W0 w_op. - Let w_0W := znz_0W w_op. - Let w_WW := znz_WW w_op. + Let w_W0 := ZnZ.WO. + Let w_0W := ZnZ.OW. + Let w_WW := ZnZ.WW. Let ww_of_pos p := match w_of_pos p with @@ -124,15 +122,15 @@ Section Z_2nZ. Eval lazy beta delta [ww_tail0] in ww_tail0 w_0 w_0W w_compare w_tail0 w_add2 w_zdigits _ww_zdigits. - Let ww_WW := Eval lazy beta delta [ww_WW] in (@ww_WW w). - Let ww_0W := Eval lazy beta delta [ww_0W] in (@ww_0W w). - Let ww_W0 := Eval lazy beta delta [ww_W0] in (@ww_W0 w). + Let ww_WW := Eval lazy beta delta [ww_WW] in (@ww_WW t). + Let ww_0W := Eval lazy beta delta [ww_0W] in (@ww_0W t). + Let ww_W0 := Eval lazy beta delta [ww_W0] in (@ww_W0 t). (* ** Comparison ** *) Let compare := Eval lazy beta delta[ww_compare] in ww_compare w_0 w_compare. - Let eq0 (x:zn2z w) := + Let eq0 (x:zn2z t) := match x with | W0 => true | _ => false @@ -226,7 +224,7 @@ Section Z_2nZ. Eval lazy beta iota delta [ww_div21] in ww_div21 w_0 w_0W div32 ww_1 compare sub. - Let low (p: zn2z w) := match p with WW _ p1 => p1 | _ => w_0 end. + Let low (p: zn2z t) := match p with WW _ p1 => p1 | _ => w_0 end. Let add_mul_div := Eval lazy beta delta [ww_add_mul_div] in @@ -287,8 +285,8 @@ Section Z_2nZ. (* ** Record of operators on 2 words *) - Definition mk_zn2z_op := - mk_znz_op _ww_digits _ww_zdigits + Global Instance mk_zn2z_ops : ZnZ.Ops (zn2z t) | 1 := + ZnZ.MkOps _ww_digits _ww_zdigits to_Z ww_of_pos head0 tail0 W0 ww_1 ww_Bm1 compare eq0 @@ -307,8 +305,8 @@ Section Z_2nZ. sqrt2 sqrt. - Definition mk_zn2z_op_karatsuba := - mk_znz_op _ww_digits _ww_zdigits + Global Instance mk_zn2z_ops_karatsuba : ZnZ.Ops (zn2z t) | 2 := + ZnZ.MkOps _ww_digits _ww_zdigits to_Z ww_of_pos head0 tail0 W0 ww_1 ww_Bm1 compare eq0 @@ -328,51 +326,51 @@ Section Z_2nZ. sqrt. (* Proof *) - Variable op_spec : znz_spec w_op. + Context {specs : ZnZ.Specs ops}. Hint Resolve - (spec_to_Z op_spec) - (spec_of_pos op_spec) - (spec_0 op_spec) - (spec_1 op_spec) - (spec_Bm1 op_spec) - (spec_compare op_spec) - (spec_eq0 op_spec) - (spec_opp_c op_spec) - (spec_opp op_spec) - (spec_opp_carry op_spec) - (spec_succ_c op_spec) - (spec_add_c op_spec) - (spec_add_carry_c op_spec) - (spec_succ op_spec) - (spec_add op_spec) - (spec_add_carry op_spec) - (spec_pred_c op_spec) - (spec_sub_c op_spec) - (spec_sub_carry_c op_spec) - (spec_pred op_spec) - (spec_sub op_spec) - (spec_sub_carry op_spec) - (spec_mul_c op_spec) - (spec_mul op_spec) - (spec_square_c op_spec) - (spec_div21 op_spec) - (spec_div_gt op_spec) - (spec_div op_spec) - (spec_mod_gt op_spec) - (spec_mod op_spec) - (spec_gcd_gt op_spec) - (spec_gcd op_spec) - (spec_head0 op_spec) - (spec_tail0 op_spec) - (spec_add_mul_div op_spec) - (spec_pos_mod) - (spec_is_even) - (spec_sqrt2) - (spec_sqrt) - (spec_W0 op_spec) - (spec_0W op_spec) - (spec_WW op_spec). + ZnZ.spec_to_Z + ZnZ.spec_of_pos + ZnZ.spec_0 + ZnZ.spec_1 + ZnZ.spec_m1 + ZnZ.spec_compare + ZnZ.spec_eq0 + ZnZ.spec_opp_c + ZnZ.spec_opp + ZnZ.spec_opp_carry + ZnZ.spec_succ_c + ZnZ.spec_add_c + ZnZ.spec_add_carry_c + ZnZ.spec_succ + ZnZ.spec_add + ZnZ.spec_add_carry + ZnZ.spec_pred_c + ZnZ.spec_sub_c + ZnZ.spec_sub_carry_c + ZnZ.spec_pred + ZnZ.spec_sub + ZnZ.spec_sub_carry + ZnZ.spec_mul_c + ZnZ.spec_mul + ZnZ.spec_square_c + ZnZ.spec_div21 + ZnZ.spec_div_gt + ZnZ.spec_div + ZnZ.spec_modulo_gt + ZnZ.spec_modulo + ZnZ.spec_gcd_gt + ZnZ.spec_gcd + ZnZ.spec_head0 + ZnZ.spec_tail0 + ZnZ.spec_add_mul_div + ZnZ.spec_pos_mod + ZnZ.spec_is_even + ZnZ.spec_sqrt2 + ZnZ.spec_sqrt + ZnZ.spec_WO + ZnZ.spec_OW + ZnZ.spec_WW. Ltac wwauto := unfold ww_to_Z; auto. @@ -392,20 +390,21 @@ Section Z_2nZ. Proof. refine (spec_ww_to_Z w_digits w_to_Z _);auto. Qed. Let spec_ww_of_pos : forall p, - Zpos p = (Z_of_N (fst (ww_of_pos p)))*wwB + [|(snd (ww_of_pos p))|]. + Zpos p = (Z.of_N (fst (ww_of_pos p)))*wwB + [|(snd (ww_of_pos p))|]. Proof. unfold ww_of_pos;intros. - assert (H:= spec_of_pos op_spec p);unfold w_of_pos; - destruct (znz_of_pos w_op p). simpl in H. - rewrite H;clear H;destruct n;simpl to_Z. - simpl;unfold w_to_Z,w_0;rewrite (spec_0 op_spec);trivial. - unfold Z_of_N; assert (H:= spec_of_pos op_spec p0); - destruct (znz_of_pos w_op p0). simpl in H. - rewrite H;unfold fst, snd,Z_of_N, to_Z. - rewrite (spec_WW op_spec). + rewrite (ZnZ.spec_of_pos p). unfold w_of_pos. + case (ZnZ.of_pos p); intros. simpl. + destruct n; simpl ZnZ.to_Z. + simpl;unfold w_to_Z,w_0; rewrite ZnZ.spec_0;trivial. + unfold Z.of_N. + rewrite (ZnZ.spec_of_pos p0). + case (ZnZ.of_pos p0); intros. simpl. + unfold fst, snd,Z.of_N, to_Z, wB, w_digits, w_to_Z, w_WW. + rewrite ZnZ.spec_WW. replace wwB with (wB*wB). - unfold wB,w_to_Z,w_digits;clear H;destruct n;ring. - symmetry. rewrite <- Zpower_2; exact (wwB_wBwB w_digits). + unfold wB,w_to_Z,w_digits;destruct n;ring. + symmetry. rewrite <- Z.pow_2_r; exact (wwB_wBwB w_digits). Qed. Let spec_ww_0 : [|W0|] = 0. @@ -418,15 +417,9 @@ Section Z_2nZ. Proof. refine (spec_ww_Bm1 w_Bm1 w_digits w_to_Z _);auto. Qed. Let spec_ww_compare : - forall x y, - match compare x y with - | Eq => [|x|] = [|y|] - | Lt => [|x|] < [|y|] - | Gt => [|x|] > [|y|] - end. + forall x y, compare x y = Z.compare [|x|] [|y|]. Proof. refine (spec_ww_compare w_0 w_digits w_to_Z w_compare _ _ _);auto. - exact (spec_compare op_spec). Qed. Let spec_ww_eq0 : forall x, eq0 x = true -> [|x|] = 0. @@ -531,8 +524,7 @@ Section Z_2nZ. Proof. refine (spec_ww_karatsuba_c _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _); wwauto. - unfold w_digits; apply spec_more_than_1_digit; auto. - exact (spec_compare op_spec). + unfold w_digits; apply ZnZ.spec_more_than_1_digit; auto. Qed. Let spec_ww_mul : forall x y, [|mul x y|] = ([|x|] * [|y|]) mod wwB. @@ -559,11 +551,10 @@ Section Z_2nZ. w_add w_add_carry w_pred w_sub w_mul_c w_div21 sub_c w_digits w_to_Z _ _ _ _ _ _ _ _ _ _ _ _ _ _ _);wwauto. unfold w_Bm2, w_to_Z, w_pred, w_Bm1. - rewrite (spec_pred op_spec);rewrite (spec_Bm1 op_spec). + rewrite ZnZ.spec_pred, ZnZ.spec_m1. unfold w_digits;rewrite Zmod_small. ring. - assert (H:= wB_pos(znz_digits w_op)). omega. - exact (spec_compare op_spec). - exact (spec_div21 op_spec). + assert (H:= wB_pos(ZnZ.digits)). omega. + exact ZnZ.spec_div21. Qed. Let spec_ww_div21 : forall a1 a2 b, @@ -580,24 +571,21 @@ Section Z_2nZ. Let spec_add2: forall x y, [|w_add2 x y|] = w_to_Z x + w_to_Z y. unfold w_add2. - intros xh xl; generalize (spec_add_c op_spec xh xl). - unfold w_add_c; case znz_add_c; unfold interp_carry; simpl ww_to_Z. + intros xh xl; generalize (ZnZ.spec_add_c xh xl). + unfold w_add_c; case ZnZ.add_c; unfold interp_carry; simpl ww_to_Z. intros w0 Hw0; simpl; unfold w_to_Z; rewrite Hw0. - unfold w_0; rewrite spec_0; simpl; auto with zarith. - intros w0; rewrite Zmult_1_l; simpl. - unfold w_to_Z, w_1; rewrite spec_1; auto with zarith. - rewrite Zmult_1_l; auto. + unfold w_0; rewrite ZnZ.spec_0; simpl; auto with zarith. + intros w0; rewrite Z.mul_1_l; simpl. + unfold w_to_Z, w_1; rewrite ZnZ.spec_1; auto with zarith. + rewrite Z.mul_1_l; auto. Qed. Let spec_low: forall x, 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_small; auto with zarith. - split; auto with zarith. - unfold wB, base; auto with zarith. + unfold ww_to_Z, w_to_Z, w_0; rewrite ZnZ.spec_0; simpl; auto. intros xh xl; simpl. - rewrite Zplus_comm; rewrite Z_mod_plus; auto with zarith. + rewrite Z.add_comm; rewrite Z_mod_plus; auto with zarith. rewrite Zmod_small; auto with zarith. unfold wB, base; auto with zarith. Qed. @@ -608,8 +596,8 @@ Section Z_2nZ. unfold w_to_Z, _ww_zdigits. rewrite spec_add2. unfold w_to_Z, w_zdigits, w_digits. - rewrite spec_zdigits; auto. - rewrite Zpos_xO; auto with zarith. + rewrite ZnZ.spec_zdigits; auto. + rewrite Pos2Z.inj_xO; auto with zarith. Qed. @@ -617,10 +605,9 @@ Section Z_2nZ. Proof. refine (spec_ww_head00 w_0 w_0W w_compare w_head0 w_add2 w_zdigits _ww_zdigits - w_to_Z _ _ _ (refl_equal _ww_digits) _ _ _ _); auto. - exact (spec_compare op_spec). - exact (spec_head00 op_spec). - exact (spec_zdigits op_spec). + w_to_Z _ _ _ (eq_refl _ww_digits) _ _ _ _); auto. + exact ZnZ.spec_head00. + exact ZnZ.spec_zdigits. Qed. Let spec_ww_head0 : forall x, 0 < [|x|] -> @@ -629,18 +616,16 @@ Section Z_2nZ. refine (spec_ww_head0 w_0 w_0W w_compare w_head0 w_add2 w_zdigits _ww_zdigits w_to_Z _ _ _ _ _ _ _);wwauto. - exact (spec_compare op_spec). - exact (spec_zdigits op_spec). + exact ZnZ.spec_zdigits. Qed. Let spec_ww_tail00 : forall x, [|x|] = 0 -> [|tail0 x|] = Zpos _ww_digits. Proof. refine (spec_ww_tail00 w_0 w_0W w_compare w_tail0 w_add2 w_zdigits _ww_zdigits - w_to_Z _ _ _ (refl_equal _ww_digits) _ _ _ _); wwauto. - exact (spec_compare op_spec). - exact (spec_tail00 op_spec). - exact (spec_zdigits op_spec). + w_to_Z _ _ _ (eq_refl _ww_digits) _ _ _ _); wwauto. + exact ZnZ.spec_tail00. + exact ZnZ.spec_zdigits. Qed. @@ -649,8 +634,7 @@ Section Z_2nZ. Proof. refine (spec_ww_tail0 (w_digits := w_digits) w_0 w_0W w_compare w_tail0 w_add2 w_zdigits _ww_zdigits w_to_Z _ _ _ _ _ _ _);wwauto. - exact (spec_compare op_spec). - exact (spec_zdigits op_spec). + exact ZnZ.spec_zdigits. Qed. Lemma spec_ww_add_mul_div : forall x y p, @@ -659,10 +643,10 @@ Section Z_2nZ. ([|x|] * (2 ^ [|p|]) + [|y|] / (2 ^ ((Zpos _ww_digits) - [|p|]))) mod wwB. Proof. - refine (@spec_ww_add_mul_div w w_0 w_WW w_W0 w_0W compare w_add_mul_div + refine (@spec_ww_add_mul_div t w_0 w_WW w_W0 w_0W compare w_add_mul_div sub w_digits w_zdigits low w_to_Z _ _ _ _ _ _ _ _ _ _ _);wwauto. - exact (spec_zdigits op_spec). + exact ZnZ.spec_zdigits. Qed. Let spec_ww_div_gt : forall a b, @@ -671,29 +655,29 @@ Section Z_2nZ. [|a|] = [|q|] * [|b|] + [|r|] /\ 0 <= [|r|] < [|b|]. Proof. refine -(@spec_ww_div_gt w w_digits w_0 w_WW w_0W w_compare w_eq0 +(@spec_ww_div_gt t w_digits w_0 w_WW w_0W w_compare w_eq0 w_opp_c w_opp w_opp_carry w_sub_c w_sub w_sub_carry w_div_gt w_add_mul_div w_head0 w_div21 div32 _ww_zdigits ww_1 add_mul_div w_zdigits w_to_Z _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ). - exact (spec_0 op_spec). - exact (spec_to_Z op_spec). + exact ZnZ.spec_0. + exact ZnZ.spec_to_Z. wwauto. wwauto. - exact (spec_compare op_spec). - exact (spec_eq0 op_spec). - exact (spec_opp_c op_spec). - exact (spec_opp op_spec). - exact (spec_opp_carry op_spec). - exact (spec_sub_c op_spec). - exact (spec_sub op_spec). - exact (spec_sub_carry op_spec). - exact (spec_div_gt op_spec). - exact (spec_add_mul_div op_spec). - exact (spec_head0 op_spec). - exact (spec_div21 op_spec). + exact ZnZ.spec_compare. + exact ZnZ.spec_eq0. + exact ZnZ.spec_opp_c. + exact ZnZ.spec_opp. + exact ZnZ.spec_opp_carry. + exact ZnZ.spec_sub_c. + exact ZnZ.spec_sub. + exact ZnZ.spec_sub_carry. + exact ZnZ.spec_div_gt. + exact ZnZ.spec_add_mul_div. + exact ZnZ.spec_head0. + exact ZnZ.spec_div21. exact spec_w_div32. - exact (spec_zdigits op_spec). + exact ZnZ.spec_zdigits. exact spec_ww_digits. exact spec_ww_1. exact spec_ww_add_mul_div. @@ -711,15 +695,14 @@ refine [|a|] > [|b|] -> 0 < [|b|] -> [|mod_gt a b|] = [|a|] mod [|b|]. Proof. - refine (@spec_ww_mod_gt w w_digits w_0 w_WW w_0W w_compare w_eq0 + refine (@spec_ww_mod_gt t w_digits w_0 w_WW w_0W w_compare w_eq0 w_opp_c w_opp w_opp_carry w_sub_c w_sub w_sub_carry w_div_gt w_mod_gt w_add_mul_div w_head0 w_div21 div32 _ww_zdigits ww_1 add_mul_div w_zdigits w_to_Z _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _);wwauto. - exact (spec_compare op_spec). - exact (spec_div_gt op_spec). - exact (spec_div21 op_spec). - exact (spec_zdigits op_spec). + exact ZnZ.spec_div_gt. + exact ZnZ.spec_div21. + exact ZnZ.spec_zdigits. exact spec_ww_add_mul_div. Qed. @@ -731,37 +714,33 @@ refine Let spec_ww_gcd_gt : forall a b, [|a|] > [|b|] -> Zis_gcd [|a|] [|b|] [|gcd_gt a b|]. Proof. - refine (@spec_ww_gcd_gt w w_digits W0 w_to_Z _ + refine (@spec_ww_gcd_gt t w_digits W0 w_to_Z _ w_0 w_0 w_eq0 w_gcd_gt _ww_digits _ gcd_gt_fix _ _ _ _ gcd_cont _);auto. - refine (@spec_ww_gcd_gt_aux w w_digits w_0 w_WW w_0W w_compare w_opp_c w_opp + refine (@spec_ww_gcd_gt_aux t w_digits w_0 w_WW w_0W w_compare w_opp_c w_opp w_opp_carry w_sub_c w_sub w_sub_carry w_gcd_gt w_add_mul_div w_head0 w_div21 div32 _ww_zdigits ww_1 add_mul_div w_zdigits w_to_Z _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _);wwauto. - exact (spec_compare op_spec). - exact (spec_div21 op_spec). - exact (spec_zdigits op_spec). + exact ZnZ.spec_div21. + exact ZnZ.spec_zdigits. exact spec_ww_add_mul_div. - refine (@spec_gcd_cont w w_digits ww_1 w_to_Z _ _ w_0 w_1 w_compare + refine (@spec_gcd_cont t w_digits ww_1 w_to_Z _ _ w_0 w_1 w_compare _ _);auto. - exact (spec_compare op_spec). Qed. Let spec_ww_gcd : forall a b, Zis_gcd [|a|] [|b|] [|gcd a b|]. Proof. - refine (@spec_ww_gcd w w_digits W0 compare w_to_Z _ _ w_0 w_0 w_eq0 w_gcd_gt + refine (@spec_ww_gcd t w_digits W0 compare w_to_Z _ _ w_0 w_0 w_eq0 w_gcd_gt _ww_digits _ gcd_gt_fix _ _ _ _ gcd_cont _);auto. - refine (@spec_ww_gcd_gt_aux w w_digits w_0 w_WW w_0W w_compare w_opp_c w_opp + refine (@spec_ww_gcd_gt_aux t w_digits w_0 w_WW w_0W w_compare w_opp_c w_opp w_opp_carry w_sub_c w_sub w_sub_carry w_gcd_gt w_add_mul_div w_head0 w_div21 div32 _ww_zdigits ww_1 add_mul_div w_zdigits w_to_Z _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _);wwauto. - exact (spec_compare op_spec). - exact (spec_div21 op_spec). - exact (spec_zdigits op_spec). + exact ZnZ.spec_div21. + exact ZnZ.spec_zdigits. exact spec_ww_add_mul_div. - refine (@spec_gcd_cont w w_digits ww_1 w_to_Z _ _ w_0 w_1 w_compare + refine (@spec_gcd_cont t w_digits ww_1 w_to_Z _ _ w_0 w_1 w_compare _ _);auto. - exact (spec_compare op_spec). Qed. Let spec_ww_is_even : forall x, @@ -770,8 +749,8 @@ refine | false => [|x|] mod 2 = 1 end. Proof. - refine (@spec_ww_is_even w w_is_even w_0 w_1 w_Bm1 w_digits _ _ _ _ _); auto. - exact (spec_is_even op_spec). + refine (@spec_ww_is_even t w_is_even w_digits _ _ ). + exact ZnZ.spec_is_even. Qed. Let spec_ww_sqrt2 : forall x y, @@ -781,78 +760,72 @@ refine [+|r|] <= 2 * [|s|]. Proof. intros x y H. - refine (@spec_ww_sqrt2 w w_is_even w_compare w_0 w_1 w_Bm1 + refine (@spec_ww_sqrt2 t w_is_even w_compare w_0 w_1 w_Bm1 w_0W w_sub w_square_c w_div21 w_add_mul_div w_digits w_zdigits _ww_zdigits w_add_c w_sqrt2 w_pred pred_c pred add_c add sub_c add_mul_div _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _); wwauto. - exact (spec_zdigits op_spec). - exact (spec_more_than_1_digit op_spec). - exact (spec_is_even op_spec). - exact (spec_compare op_spec). - exact (spec_div21 op_spec). - exact (spec_ww_add_mul_div). - exact (spec_sqrt2 op_spec). + exact ZnZ.spec_zdigits. + exact ZnZ.spec_more_than_1_digit. + exact ZnZ.spec_is_even. + exact ZnZ.spec_div21. + exact spec_ww_add_mul_div. + exact ZnZ.spec_sqrt2. Qed. Let spec_ww_sqrt : forall x, [|sqrt x|] ^ 2 <= [|x|] < ([|sqrt x|] + 1) ^ 2. Proof. - refine (@spec_ww_sqrt w w_is_even w_0 w_1 w_Bm1 + refine (@spec_ww_sqrt t w_is_even w_0 w_1 w_Bm1 w_sub w_add_mul_div w_digits w_zdigits _ww_zdigits w_sqrt2 pred add_mul_div head0 compare _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _); wwauto. - exact (spec_zdigits op_spec). - exact (spec_more_than_1_digit op_spec). - exact (spec_is_even op_spec). - exact (spec_ww_add_mul_div). - exact (spec_sqrt2 op_spec). + exact ZnZ.spec_zdigits. + exact ZnZ.spec_more_than_1_digit. + exact ZnZ.spec_is_even. + exact spec_ww_add_mul_div. + exact ZnZ.spec_sqrt2. Qed. - Lemma mk_znz2_spec : znz_spec mk_zn2z_op. + Global Instance mk_zn2z_specs : ZnZ.Specs mk_zn2z_ops. Proof. - apply mk_znz_spec;auto. + apply ZnZ.MkSpecs; auto. exact spec_ww_add_mul_div. - refine (@spec_ww_pos_mod w w_0 w_digits w_zdigits w_WW + refine (@spec_ww_pos_mod t w_0 w_digits w_zdigits w_WW w_pos_mod compare w_0W low sub _ww_zdigits w_to_Z _ _ _ _ _ _ _ _ _ _ _ _);wwauto. - exact (spec_pos_mod op_spec). - exact (spec_zdigits op_spec). + exact ZnZ.spec_zdigits. unfold w_to_Z, w_zdigits. - rewrite (spec_zdigits op_spec). - rewrite <- Zpos_xO; exact spec_ww_digits. + rewrite ZnZ.spec_zdigits. + rewrite <- Pos2Z.inj_xO; exact spec_ww_digits. Qed. - Lemma mk_znz2_karatsuba_spec : znz_spec mk_zn2z_op_karatsuba. + Global Instance mk_zn2z_specs_karatsuba : ZnZ.Specs mk_zn2z_ops_karatsuba. Proof. - apply mk_znz_spec;auto. + apply ZnZ.MkSpecs; auto. exact spec_ww_add_mul_div. - refine (@spec_ww_pos_mod w w_0 w_digits w_zdigits w_WW + refine (@spec_ww_pos_mod t w_0 w_digits w_zdigits w_WW w_pos_mod compare w_0W low sub _ww_zdigits w_to_Z _ _ _ _ _ _ _ _ _ _ _ _);wwauto. - exact (spec_pos_mod op_spec). - exact (spec_zdigits op_spec). + exact ZnZ.spec_zdigits. unfold w_to_Z, w_zdigits. - rewrite (spec_zdigits op_spec). - rewrite <- Zpos_xO; exact spec_ww_digits. + rewrite ZnZ.spec_zdigits. + rewrite <- Pos2Z.inj_xO; exact spec_ww_digits. Qed. End Z_2nZ. Section MulAdd. - Variable w: Type. - Variable op: znz_op w. - Variable sop: znz_spec op. + Context {t : Type}{ops : ZnZ.Ops t}{specs : ZnZ.Specs ops}. - Definition mul_add:= w_mul_add (znz_0 op) (znz_succ op) (znz_add_c op) (znz_mul_c op). + Definition mul_add:= w_mul_add ZnZ.zero ZnZ.succ ZnZ.add_c ZnZ.mul_c. - Notation "[| x |]" := (znz_to_Z op x) (at level 0, x at level 99). + Notation "[| x |]" := (ZnZ.to_Z x) (at level 0, x at level 99). Notation "[|| x ||]" := - (zn2z_to_Z (base (znz_digits op)) (znz_to_Z op) x) (at level 0, x at level 99). - + (zn2z_to_Z (base ZnZ.digits) ZnZ.to_Z x) (at level 0, x at level 99). Lemma spec_mul_add: forall x y z, let (zh, zl) := mul_add x y z in @@ -860,11 +833,11 @@ Section MulAdd. Proof. intros x y z. refine (spec_w_mul_add _ _ _ _ _ _ _ _ _ _ _ _ x y z); auto. - exact (spec_0 sop). - exact (spec_to_Z sop). - exact (spec_succ sop). - exact (spec_add_c sop). - exact (spec_mul_c sop). + exact ZnZ.spec_0. + exact ZnZ.spec_to_Z. + exact ZnZ.spec_succ. + exact ZnZ.spec_add_c. + exact ZnZ.spec_mul_c. Qed. End MulAdd. @@ -873,13 +846,13 @@ End MulAdd. (** Modular versions of DoubleCyclic *) Module DoubleCyclic (C:CyclicType) <: CyclicType. - Definition w := zn2z C.w. - Definition w_op := mk_zn2z_op C.w_op. - Definition w_spec := mk_znz2_spec C.w_spec. + Definition t := zn2z C.t. + Instance ops : ZnZ.Ops t := mk_zn2z_ops. + Instance specs : ZnZ.Specs ops := mk_zn2z_specs. End DoubleCyclic. Module DoubleCyclicKaratsuba (C:CyclicType) <: CyclicType. - Definition w := zn2z C.w. - Definition w_op := mk_zn2z_op_karatsuba C.w_op. - Definition w_spec := mk_znz2_karatsuba_spec C.w_spec. + Definition t := zn2z C.t. + Definition ops : ZnZ.Ops t := mk_zn2z_ops_karatsuba. + Definition specs : ZnZ.Specs ops := mk_zn2z_specs_karatsuba. End DoubleCyclicKaratsuba. diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v index 4e6eccea..8525b0e1 100644 --- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v +++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <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 *) @@ -8,8 +8,6 @@ (* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) (************************************************************************) -(*i $Id: DoubleDiv.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - Set Implicit Arguments. Require Import ZArith. @@ -82,11 +80,7 @@ Section POS_MOD. Variable spec_w_0W : forall l, [[w_0W l]] = [|l|]. Variable spec_ww_compare : forall x y, - match ww_compare x y with - | Eq => [[x]] = [[y]] - | Lt => [[x]] < [[y]] - | Gt => [[x]] > [[y]] - end. + ww_compare x y = Z.compare [[x]] [[y]]. Variable spec_ww_sub: forall x y, [[ww_sub x y]] = ([[x]] - [[y]]) mod wwB. @@ -105,8 +99,8 @@ Section POS_MOD. intros w1 p; case (spec_to_w_Z p); intros HH1 HH2. unfold ww_pos_mod; case w1. simpl; rewrite Zmod_small; split; auto with zarith. - intros xh xl; generalize (spec_ww_compare p (w_0W w_zdigits)); - case ww_compare; + intros xh xl; rewrite spec_ww_compare. + case Z.compare_spec; rewrite spec_w_0W; rewrite spec_zdigits; fold wB; intros H1. rewrite H1; simpl ww_to_Z. @@ -123,19 +117,19 @@ Section POS_MOD. rewrite spec_low. 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). + apply Z.lt_le_trans with (1 := H1). unfold base; apply Zpower2_le_lin; auto with zarith. rewrite HH0. rewrite Zplus_mod; auto with zarith. unfold base. rewrite <- (F0 (Zpos w_digits) [[p]]). rewrite Zpower_exp; auto with zarith. - rewrite Zmult_assoc. + rewrite Z.mul_assoc. 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_ww_compare. + case Z.compare_spec; rewrite spec_ww_zdigits; rewrite spec_zdigits; intros H2. replace (2^[[p]]) with wwB. rewrite Zmod_small; auto with zarith. @@ -149,52 +143,52 @@ generalize (spec_ww_compare p ww_zdigits); rewrite <- Zmod_div_mod; auto with zarith. rewrite Zmod_small; auto with zarith. split; auto with zarith. - apply Zlt_le_trans with (Zpos w_digits); auto with zarith. + apply Z.lt_le_trans with (Zpos w_digits); auto with zarith. unfold base; apply Zpower2_le_lin; auto with zarith. exists wB; unfold base; rewrite <- Zpower_exp; auto with zarith. rewrite spec_ww_digits; - apply f_equal with (f := Zpower 2); rewrite Zpos_xO; auto with zarith. + apply f_equal with (f := Z.pow 2); rewrite Pos2Z.inj_xO; auto with zarith. simpl ww_to_Z; autorewrite with w_rewrite. rewrite spec_pos_mod; rewrite HH0. pattern [|xh|] at 2; rewrite Z_div_mod_eq with (b := 2 ^ ([[p]] - Zpos w_digits)); auto with zarith. - rewrite (fun x => (Zmult_comm (2 ^ x))); rewrite Zmult_plus_distr_l. - unfold base; rewrite <- Zmult_assoc; rewrite <- Zpower_exp; + rewrite (fun x => (Z.mul_comm (2 ^ x))); rewrite Z.mul_add_distr_r. + unfold base; rewrite <- Z.mul_assoc; rewrite <- Zpower_exp; auto with zarith. rewrite F0; auto with zarith. - rewrite <- Zplus_assoc; rewrite Zplus_mod; auto with zarith. + rewrite <- Z.add_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_small; auto with zarith. + symmetry; 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. - apply Zplus_le_0_compat; auto with zarith. - apply Zmult_le_0_compat; auto with zarith. + apply Z.add_nonneg_nonneg; auto with zarith. + apply Z.mul_nonneg_nonneg; auto with zarith. match goal with |- 0 <= ?X mod ?Y => case (Z_mod_lt X Y); auto with zarith end. match goal with |- ?X mod ?Y * ?U + ?Z < ?T => - apply Zle_lt_trans with ((Y - 1) * U + Z ); + apply Z.le_lt_trans with ((Y - 1) * U + Z ); [case (Z_mod_lt X Y); auto with zarith | idtac] end. match goal with |- ?X * ?U + ?Y < ?Z => - apply Zle_lt_trans with (X * U + (U - 1)) + apply Z.le_lt_trans with (X * U + (U - 1)) end. - apply Zplus_le_compat_l; auto with zarith. + apply Z.add_le_mono_l; auto with zarith. case (spec_to_Z xl); unfold base; auto with zarith. - rewrite Zmult_minus_distr_r; rewrite <- Zpower_exp; auto with zarith. + rewrite Z.mul_sub_distr_r; rewrite <- Zpower_exp; auto with zarith. rewrite F0; 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). + apply Z.lt_le_trans with (1:= U2). unfold base; rewrite spec_ww_digits. apply Zpower_le_monotone; auto with zarith. split; auto with zarith. - rewrite Zpos_xO; auto with zarith. + rewrite Pos2Z.inj_xO; auto with zarith. Qed. End POS_MOD. @@ -266,12 +260,7 @@ Section DoubleDiv32. Variable spec_w_WW : forall h l, [[w_WW h l]] = [|h|] * wB + [|l|]. Variable spec_compare : - forall x y, - match w_compare x y with - | Eq => [|x|] = [|y|] - | Lt => [|x|] < [|y|] - | Gt => [|x|] > [|y|] - end. + forall x y, w_compare x y = Z.compare [|x|] [|y|]. Variable spec_w_add_c : forall x y, [+|w_add_c x y|] = [|x|] + [|y|]. Variable spec_w_add_carry_c : forall x y, [+|w_add_carry_c x y|] = [|x|] + [|y|] + 1. @@ -301,14 +290,14 @@ Section DoubleDiv32. assert (H:= spec_ww_to_Z w_digits w_to_Z spec_to_Z x). Theorem wB_div2: forall x, wB/2 <= x -> wB <= 2 * x. - intros x H; rewrite <- wB_div_2; apply Zmult_le_compat_l; auto with zarith. + intros x H; rewrite <- wB_div_2; apply Z.mul_le_mono_nonneg_l; auto with zarith. Qed. Lemma Zmult_lt_0_reg_r_2 : forall n m : Z, 0 <= n -> 0 < m * n -> 0 < m. Proof. - intros n m H1 H2;apply Zmult_lt_0_reg_r with n;trivial. - destruct (Zle_lt_or_eq _ _ H1);trivial. - subst;rewrite Zmult_0_r in H2;discriminate H2. + intros n m H1 H2;apply Z.mul_pos_cancel_r with n;trivial. + Z.le_elim H1; trivial. + subst;rewrite Z.mul_0_r in H2;discriminate H2. Qed. Theorem spec_w_div32 : forall a1 a2 a3 b1 b2, @@ -322,7 +311,7 @@ Section DoubleDiv32. intros a1 a2 a3 b1 b2 Hle Hlt. assert (U:= lt_0_wB w_digits); assert (U1:= lt_0_wwB w_digits). Spec_w_to_Z a1;Spec_w_to_Z a2;Spec_w_to_Z a3;Spec_w_to_Z b1;Spec_w_to_Z b2. - rewrite wwB_wBwB; rewrite Zpower_2; rewrite Zmult_assoc;rewrite <- Zmult_plus_distr_l. + rewrite wwB_wBwB; rewrite Z.pow_2_r; rewrite Z.mul_assoc;rewrite <- Z.mul_add_distr_r. change (w_div32 a1 a2 a3 b1 b2) with match w_compare a1 b1 with | Lt => @@ -343,7 +332,7 @@ Section DoubleDiv32. (WW (w_sub a2 b2) a3) (WW b1 b2) | Gt => (w_0, W0) (* cas absurde *) end. - assert (Hcmp:=spec_compare a1 b1);destruct (w_compare a1 b1). + rewrite spec_compare. case Z.compare_spec; intro Hcmp. simpl in Hlt. rewrite Hcmp in Hlt;assert ([|a2|] < [|b2|]). omega. assert ([[WW (w_sub a2 b2) a3]] = ([|a2|]-[|b2|])*wB + [|a3|] + wwB). @@ -362,17 +351,17 @@ Section DoubleDiv32. rewrite H0;intros r. repeat (rewrite spec_ww_add;eauto || rewrite spec_w_Bm1 || rewrite spec_w_Bm2); - simpl ww_to_Z;try rewrite Zmult_1_l;intros H1. + simpl ww_to_Z;try rewrite Z.mul_1_l;intros H1. assert (0<= ([[r]] + ([|b1|] * wB + [|b2|])) - wwB < [|b1|] * wB + [|b2|]). Spec_ww_to_Z r;split;zarith. rewrite H1. assert (H12:= wB_div2 Hle). assert (wwB <= 2 * [|b1|] * wB). - rewrite wwB_wBwB; rewrite Zpower_2; zarith. + rewrite wwB_wBwB; rewrite Z.pow_2_r; zarith. assert (-wwB < ([|a2|] - [|b2|]) * wB + [|a3|] < 0). - split. apply Zlt_le_trans with (([|a2|] - [|b2|]) * wB);zarith. + split. apply Z.lt_le_trans with (([|a2|] - [|b2|]) * wB);zarith. rewrite wwB_wBwB;replace (-(wB^2)) with (-wB*wB);[zarith | ring]. - apply Zmult_lt_compat_r;zarith. - apply Zle_lt_trans with (([|a2|] - [|b2|]) * wB + (wB -1));zarith. + apply Z.mul_lt_mono_pos_r;zarith. + apply Z.le_lt_trans with (([|a2|] - [|b2|]) * wB + (wB -1));zarith. replace ( ([|a2|] - [|b2|]) * wB + (wB - 1)) with (([|a2|] - [|b2|] + 1) * wB + - 1);[zarith | ring]. assert (([|a2|] - [|b2|] + 1) * wB <= 0);zarith. @@ -387,13 +376,13 @@ Section DoubleDiv32. Spec_ww_to_Z (WW b1 b2). simpl in HH4;zarith. rewrite H0;intros r;repeat (rewrite spec_w_Bm1 || rewrite spec_w_Bm2); - simpl ww_to_Z;try rewrite Zmult_1_l;intros H1. + simpl ww_to_Z;try rewrite Z.mul_1_l;intros H1. assert ([[r]]=([|a2|]-[|b2|])*wB+[|a3|]+([|b1|]*wB+[|b2|])). zarith. split. rewrite H2;rewrite Hcmp;ring. split. Spec_ww_to_Z r;zarith. rewrite H2. assert (([|a2|] - [|b2|]) * wB + [|a3|] < 0);zarith. - apply Zle_lt_trans with (([|a2|] - [|b2|]) * wB + (wB -1));zarith. + apply Z.le_lt_trans with (([|a2|] - [|b2|]) * wB + (wB -1));zarith. replace ( ([|a2|] - [|b2|]) * wB + (wB - 1)) with (([|a2|] - [|b2|] + 1) * wB + - 1);[zarith|ring]. assert (([|a2|] - [|b2|] + 1) * wB <= 0);zarith. @@ -411,7 +400,7 @@ Section DoubleDiv32. rewrite H1. split. ring. split. rewrite <- H1;destruct (spec_ww_to_Z w_digits w_to_Z spec_to_Z r1);trivial. - apply Zle_lt_trans with ([|r|] * wB + [|a3|]). + apply Z.le_lt_trans with ([|r|] * wB + [|a3|]). assert ( 0 <= [|q|] * [|b2|]);zarith. apply beta_lex_inv;zarith. assert ([[r1]] = [|r|] * wB + [|a3|] - [|q|] * [|b2|] + wwB). @@ -429,10 +418,10 @@ Section DoubleDiv32. intros r2;repeat (rewrite spec_pred || rewrite spec_ww_add;eauto); simpl ww_to_Z;intros H7. assert (0 < [|q|] - 1). - assert (1 <= [|q|]). zarith. - destruct (Zle_lt_or_eq _ _ H6);zarith. - rewrite <- H8 in H2;rewrite H2 in H7. - assert (0 < [|b1|]*wB). apply Zmult_lt_0_compat;zarith. + assert (H6 : 1 <= [|q|]) by zarith. + Z.le_elim H6;zarith. + rewrite <- H6 in H2;rewrite H2 in H7. + assert (0 < [|b1|]*wB). apply Z.mul_pos_pos;zarith. Spec_ww_to_Z r2. zarith. rewrite (Zmod_small ([|q|] -1));zarith. rewrite (Zmod_small ([|q|] -1 -1));zarith. @@ -450,7 +439,7 @@ Section DoubleDiv32. < wwB). split;try omega. replace (2*([|b1|]*wB+[|b2|])) with ((2*[|b1|])*wB+2*[|b2|]). 2:ring. assert (H12:= wB_div2 Hle). assert (wwB <= 2 * [|b1|] * wB). - rewrite wwB_wBwB; rewrite Zpower_2; zarith. omega. + rewrite wwB_wBwB; rewrite Z.pow_2_r; zarith. omega. rewrite <- (Zmod_unique ([[r2]] + ([|b1|] * wB + [|b2|])) wwB @@ -545,17 +534,13 @@ Section DoubleDiv21. 0 <= [[r]] < [|b1|] * wB + [|b2|]. Variable spec_ww_1 : [[ww_1]] = 1. Variable spec_ww_compare : forall x y, - match ww_compare x y with - | Eq => [[x]] = [[y]] - | Lt => [[x]] < [[y]] - | Gt => [[x]] > [[y]] - end. + ww_compare x y = Z.compare [[x]] [[y]]. Variable spec_ww_sub : forall x y, [[ww_sub x y]] = ([[x]] - [[y]]) mod wwB. Theorem wwB_div: wwB = 2 * (wwB / 2). Proof. - rewrite wwB_div_2; rewrite Zmult_assoc; rewrite wB_div_2; auto. - rewrite <- Zpower_2; apply wwB_wBwB. + rewrite wwB_div_2; rewrite Z.mul_assoc; rewrite wB_div_2; auto. + rewrite <- Z.pow_2_r; apply wwB_wBwB. Qed. Ltac Spec_w_to_Z x := @@ -576,42 +561,41 @@ Section DoubleDiv21. intros a1 a2 b H Hlt; unfold ww_div21. Spec_ww_to_Z b; assert (Eq: 0 < [[b]]). Spec_ww_to_Z a1;omega. generalize Hlt H ;clear Hlt H;case a1. - intros H1 H2;simpl in H1;Spec_ww_to_Z a2; - 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. + intros H1 H2;simpl in H1;Spec_ww_to_Z a2. + rewrite spec_ww_compare. case Z.compare_spec; + simpl;try rewrite spec_ww_1;autorewrite with rm10; intros;zarith. rewrite spec_ww_sub;simpl. rewrite Zmod_small;zarith. split. ring. assert (wwB <= 2*[[b]]);zarith. rewrite wwB_div;zarith. intros a1h a1l. Spec_w_to_Z a1h;Spec_w_to_Z a1l. Spec_ww_to_Z a2. destruct a2 as [ |a3 a4]; - (destruct b as [ |b1 b2];[unfold Zle in Eq;discriminate Eq|idtac]); + (destruct b as [ |b1 b2];[unfold Z.le in Eq;discriminate Eq|idtac]); try (Spec_w_to_Z a3; Spec_w_to_Z a4); Spec_w_to_Z b1; Spec_w_to_Z b2; intros Hlt H; match goal with |-context [w_div32 ?X ?Y ?Z ?T ?U] => generalize (@spec_w_div32 X Y Z T U); case (w_div32 X Y Z T U); intros q1 r H0 end; (assert (Eq1: wB / 2 <= [|b1|]);[ apply (@beta_lex (wB / 2) 0 [|b1|] [|b2|] wB); auto with zarith; - autorewrite with rm10;repeat rewrite (Zmult_comm wB); + autorewrite with rm10;repeat rewrite (Z.mul_comm wB); rewrite <- wwB_div_2; trivial | generalize (H0 Eq1 Hlt);clear H0;destruct r as [ |r1 r2];simpl; - try rewrite spec_w_0; try rewrite spec_w_0W;repeat rewrite Zplus_0_r; + try rewrite spec_w_0; try rewrite spec_w_0W;repeat rewrite Z.add_0_r; intros (H1,H2) ]). - split;[rewrite wwB_wBwB; rewrite Zpower_2 | trivial]. - rewrite Zmult_assoc;rewrite Zmult_plus_distr_l;rewrite <- Zmult_assoc; - rewrite <- Zpower_2; rewrite <- wwB_wBwB;rewrite H1;ring. + split;[rewrite wwB_wBwB; rewrite Z.pow_2_r | trivial]. + rewrite Z.mul_assoc;rewrite Z.mul_add_distr_r;rewrite <- Z.mul_assoc; + rewrite <- Z.pow_2_r; rewrite <- wwB_wBwB;rewrite H1;ring. destruct H2 as (H2,H3);match goal with |-context [w_div32 ?X ?Y ?Z ?T ?U] => generalize (@spec_w_div32 X Y Z T U); case (w_div32 X Y Z T U); intros q r H0;generalize (H0 Eq1 H3);clear H0;intros (H4,H5) end. split;[rewrite wwB_wBwB | trivial]. - rewrite Zpower_2. - rewrite Zmult_assoc;rewrite Zmult_plus_distr_l;rewrite <- Zmult_assoc; - rewrite <- Zpower_2. + rewrite Z.pow_2_r. + rewrite Z.mul_assoc;rewrite Z.mul_add_distr_r;rewrite <- Z.mul_assoc; + rewrite <- Z.pow_2_r. rewrite <- wwB_wBwB;rewrite H1. - rewrite spec_w_0 in H4;rewrite Zplus_0_r in H4. - repeat rewrite Zmult_plus_distr_l. rewrite <- (Zmult_assoc [|r1|]). - rewrite <- Zpower_2; rewrite <- wwB_wBwB;rewrite H4;simpl;ring. + rewrite spec_w_0 in H4;rewrite Z.add_0_r in H4. + repeat rewrite Z.mul_add_distr_r. rewrite <- (Z.mul_assoc [|r1|]). + rewrite <- Z.pow_2_r; rewrite <- wwB_wBwB;rewrite H4;simpl;ring. split;[rewrite wwB_wBwB | split;zarith]. replace (([|a1h|] * wB + [|a1l|]) * wB^2 + ([|a3|] * wB + [|a4|])) with (([|a1h|] * wwB + [|a1l|] * wB + [|a3|])*wB+ [|a4|]). @@ -809,12 +793,7 @@ Section DoubleDivGt. Variable spec_w_WW : forall h l, [[w_WW h l]] = [|h|] * wB + [|l|]. Variable spec_w_0W : forall l, [[w_0W l]] = [|l|]. Variable spec_compare : - forall x y, - match w_compare x y with - | Eq => [|x|] = [|y|] - | Lt => [|x|] < [|y|] - | Gt => [|x|] > [|y|] - end. + forall x y, w_compare x y = Z.compare [|x|] [|y|]. Variable spec_eq0 : forall x, w_eq0 x = true -> [|x|] = 0. Variable spec_opp_c : forall x, [-|w_opp_c x|] = -[|x|]. @@ -914,42 +893,42 @@ Section DoubleDivGt. end in [[WW ah al]]=[[q]]*[[WW bh bl]]+[[r]] /\ 0 <=[[r]]< [[WW bh bl]]). assert (Hh := spec_head0 Hpos). lazy zeta. - generalize (spec_compare (w_head0 bh) w_0); case w_compare; + rewrite spec_compare; case Z.compare_spec; rewrite spec_w_0; intros HH. - generalize Hh; rewrite HH; simpl Zpower; - rewrite Zmult_1_l; intros (HH1, HH2); clear HH. + generalize Hh; rewrite HH; simpl Z.pow; + rewrite Z.mul_1_l; intros (HH1, HH2); clear HH. assert (wwB <= 2*[[WW bh bl]]). - apply Zle_trans with (2*[|bh|]*wB). - rewrite wwB_wBwB; rewrite Zpower_2; apply Zmult_le_compat_r; zarith. - rewrite <- wB_div_2; apply Zmult_le_compat_l; zarith. - simpl ww_to_Z;rewrite Zmult_plus_distr_r;rewrite Zmult_assoc. + apply Z.le_trans with (2*[|bh|]*wB). + rewrite wwB_wBwB; rewrite Z.pow_2_r; apply Z.mul_le_mono_nonneg_r; zarith. + rewrite <- wB_div_2; apply Z.mul_le_mono_nonneg_l; zarith. + simpl ww_to_Z;rewrite Z.mul_add_distr_l;rewrite Z.mul_assoc. Spec_w_to_Z bl;zarith. Spec_ww_to_Z (WW ah al). rewrite spec_ww_sub;eauto. - simpl;rewrite spec_ww_1;rewrite Zmult_1_l;simpl. + simpl;rewrite spec_ww_1;rewrite Z.mul_1_l;simpl. 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. exfalso. assert (2 ^ [|w_head0 bh|] * [|bh|] >= wB);auto with zarith. - apply Zle_ge; replace wB with (wB * 1);try ring. - Spec_w_to_Z bh;apply Zmult_le_compat;zarith. + apply Z.le_ge; replace wB with (wB * 1);try ring. + Spec_w_to_Z bh;apply Z.mul_le_mono_nonneg;zarith. unfold base;apply Zpower_le_monotone;zarith. assert (HHHH : 0 < [|w_head0 bh|] < Zpos w_digits); auto with zarith. - assert (Hb:= Zlt_le_weak _ _ H). + assert (Hb:= Z.lt_le_incl _ _ H). generalize (spec_add_mul_div w_0 ah Hb) (spec_add_mul_div ah al Hb) (spec_add_mul_div al w_0 Hb) (spec_add_mul_div bh bl Hb) (spec_add_mul_div bl w_0 Hb); - rewrite spec_w_0; repeat rewrite Zmult_0_l;repeat rewrite Zplus_0_l; - rewrite Zdiv_0_l;repeat rewrite Zplus_0_r. + rewrite spec_w_0; repeat rewrite Z.mul_0_l;repeat rewrite Z.add_0_l; + rewrite Zdiv_0_l;repeat rewrite Z.add_0_r. Spec_w_to_Z ah;Spec_w_to_Z bh. unfold base;repeat rewrite Zmod_shift_r;zarith. assert (H3:=to_Z_div_minus_p ah HHHH);assert(H4:=to_Z_div_minus_p al HHHH); assert (H5:=to_Z_div_minus_p bl HHHH). - rewrite Zmult_comm in Hh. + rewrite Z.mul_comm in Hh. assert (2^[|w_head0 bh|] < wB). unfold base;apply Zpower_lt_monotone;zarith. unfold base in H0;rewrite Zmod_small;zarith. fold wB; rewrite (Zmod_small ([|bh|] * 2 ^ [|w_head0 bh|]));zarith. @@ -964,15 +943,15 @@ Section DoubleDivGt. (w_add_mul_div (w_head0 bh) al w_0) (w_add_mul_div (w_head0 bh) bh bl) (w_add_mul_div (w_head0 bh) bl w_0)) as (q,r). - rewrite V1;rewrite V2. rewrite Zmult_plus_distr_l. - rewrite <- (Zplus_assoc ([|bh|] * 2 ^ [|w_head0 bh|] * wB)). + rewrite V1;rewrite V2. rewrite Z.mul_add_distr_r. + rewrite <- (Z.add_assoc ([|bh|] * 2 ^ [|w_head0 bh|] * wB)). unfold base;rewrite <- shift_unshift_mod;zarith. fold wB. replace ([|bh|] * 2 ^ [|w_head0 bh|] * wB + [|bl|] * 2 ^ [|w_head0 bh|]) with ([[WW bh bl]] * 2^[|w_head0 bh|]). 2:simpl;ring. - fold wwB. rewrite wwB_wBwB. rewrite Zpower_2. rewrite U1;rewrite U2;rewrite U3. - rewrite Zmult_assoc. rewrite Zmult_plus_distr_l. - rewrite (Zplus_assoc ([|ah|] / 2^(Zpos(w_digits) - [|w_head0 bh|])*wB * wB)). - rewrite <- Zmult_plus_distr_l. rewrite <- Zplus_assoc. + fold wwB. rewrite wwB_wBwB. rewrite Z.pow_2_r. rewrite U1;rewrite U2;rewrite U3. + rewrite Z.mul_assoc. rewrite Z.mul_add_distr_r. + rewrite (Z.add_assoc ([|ah|] / 2^(Zpos(w_digits) - [|w_head0 bh|])*wB * wB)). + rewrite <- Z.mul_add_distr_r. rewrite <- Z.add_assoc. unfold base;repeat rewrite <- shift_unshift_mod;zarith. fold wB. replace ([|ah|] * 2 ^ [|w_head0 bh|] * wB + [|al|] * 2 ^ [|w_head0 bh|]) with ([[WW ah al]] * 2^[|w_head0 bh|]). 2:simpl;ring. @@ -983,42 +962,42 @@ Section DoubleDivGt. unfold base. replace (2^Zpos (w_digits)) with (2^(Zpos (w_digits) - 1)*2). rewrite Z_div_mult;zarith. rewrite <- Zpower_exp;zarith. - apply Zlt_le_trans with wB;zarith. + apply Z.lt_le_trans with wB;zarith. unfold base;apply Zpower_le_monotone;zarith. pattern 2 at 2;replace 2 with (2^1);trivial. rewrite <- Zpower_exp;zarith. ring_simplify (Zpos (w_digits) - 1 + 1);trivial. change [[WW w_0 q]] with ([|w_0|]*wB+[|q|]);rewrite spec_w_0;rewrite - Zmult_0_l;rewrite Zplus_0_l. + Z.mul_0_l;rewrite Z.add_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_gt_0;zarith. + assert (0 < 2^[|w_head0 bh|]). apply Z.pow_pos_nonneg;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. + rewrite H1;rewrite Z.mul_assoc;apply Z_div_plus_l;trivial. split;[apply Zdiv_le_lower_bound| apply Zdiv_lt_upper_bound];zarith. rewrite spec_ww_add_mul_div. rewrite spec_ww_sub; auto with zarith. rewrite spec_ww_digits_. change (Zpos (xO (w_digits))) with (2*Zpos (w_digits));zarith. - simpl ww_to_Z;rewrite Zmult_0_l;rewrite Zplus_0_l. + simpl ww_to_Z;rewrite Z.mul_0_l;rewrite Z.add_0_l. rewrite spec_w_0W. 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_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. - rewrite <- (Zmult_1_r wwB);apply Zmult_le_compat;zarith. + apply Z.lt_le_trans with wwB;zarith. + rewrite <- (Z.mul_1_r wwB);apply Z.mul_le_mono_nonneg;zarith. 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). + apply Z.le_lt_trans with (2 * Zpos w_digits); auto with zarith. + unfold base, ww_digits; rewrite (Pos2Z.inj_xO w_digits). apply Zpower2_lt_lin; auto with zarith. rewrite spec_ww_sub; auto with zarith. rewrite spec_ww_digits_; rewrite spec_w_0W. 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). + rewrite Pos2Z.inj_xO; split; auto with zarith. + apply Z.le_lt_trans with (2 * Zpos w_digits); auto with zarith. + unfold base, ww_digits; rewrite (Pos2Z.inj_xO w_digits). apply Zpower2_lt_lin; auto with zarith. Qed. @@ -1058,14 +1037,13 @@ Section DoubleDivGt. assert (H2:=spec_div_gt Hgt Hpos);destruct (w_div_gt al bl). repeat rewrite spec_w_0W;simpl;rewrite spec_w_0;simpl;trivial. clear H. - assert (Hcmp := spec_compare w_0 bh); destruct (w_compare w_0 bh). + rewrite spec_compare; case Z.compare_spec; intros Hcmp. rewrite spec_w_0 in Hcmp. change [[WW bh bl]] with ([|bh|]*wB+[|bl|]). - rewrite <- Hcmp;rewrite Zmult_0_l;rewrite Zplus_0_l. + rewrite <- Hcmp;rewrite Z.mul_0_l;rewrite Z.add_0_l. simpl in Hpos;rewrite <- Hcmp in Hpos;simpl in Hpos. assert (H2:= @spec_double_divn1 w w_digits w_zdigits w_0 w_WW w_head0 w_add_mul_div w_div21 w_compare w_sub w_to_Z spec_to_Z spec_w_zdigits spec_w_0 spec_w_WW spec_head0 spec_add_mul_div spec_div21 spec_compare spec_sub 1 (WW ah al) bl Hpos). - unfold double_to_Z,double_wB,double_digits in H2. destruct (double_divn1 w_zdigits w_0 w_WW w_head0 w_add_mul_div w_div21 w_compare w_sub 1 (WW ah al) bl). @@ -1101,7 +1079,7 @@ Section DoubleDivGt. rewrite spec_mod_gt;trivial. assert (H:=spec_div_gt Hgt Hpos). destruct (w_div_gt a b) as (q,r);simpl. - rewrite Zmult_comm in H;destruct H. + rewrite Z.mul_comm in H;destruct H. symmetry;apply Zmod_unique with [|q|];trivial. Qed. @@ -1154,7 +1132,7 @@ Section DoubleDivGt. rewrite spec_w_0W;rewrite spec_w_mod_gt_eq;trivial. destruct (w_div_gt al bl);simpl;rewrite spec_w_0W;trivial. clear H. - assert (H2 := spec_compare w_0 bh);destruct (w_compare w_0 bh). + rewrite spec_compare; case Z.compare_spec; intros H2. rewrite (@spec_double_modn1_aux w w_zdigits w_0 w_WW w_head0 w_add_mul_div w_div21 w_compare w_sub w_to_Z spec_w_0 spec_compare 1 (WW ah al) bl). destruct (double_divn1 w_zdigits w_0 w_WW w_head0 w_add_mul_div w_div21 w_compare w_sub 1 @@ -1171,7 +1149,7 @@ Section DoubleDivGt. rewrite (spec_ww_mod_gt_eq a b Hgt Hpos). destruct (ww_div_gt a b)as(q,r);destruct H. apply Zmod_unique with[[q]];simpl;trivial. - rewrite Zmult_comm;trivial. + rewrite Z.mul_comm;trivial. Qed. Lemma Zis_gcd_mod : forall a b d, @@ -1227,13 +1205,14 @@ Section DoubleDivGt. end | Gt => W0 (* absurde *) end). - assert (Hbh := spec_compare w_0 bh);destruct (w_compare w_0 bh). - simpl ww_to_Z in *. rewrite spec_w_0 in Hbh;rewrite <- Hbh; - rewrite Zmult_0_l;rewrite Zplus_0_l. - assert (Hbl := spec_compare w_0 bl); destruct (w_compare w_0 bl). - rewrite spec_w_0 in Hbl;rewrite <- Hbl;apply Zis_gcd_0. - simpl;rewrite spec_w_0;rewrite Zmult_0_l;rewrite Zplus_0_l. - rewrite spec_w_0 in Hbl. + rewrite spec_compare, spec_w_0. + case Z.compare_spec; intros Hbh. + simpl ww_to_Z in *. rewrite <- Hbh. + rewrite Z.mul_0_l;rewrite Z.add_0_l. + rewrite spec_compare, spec_w_0. + case Z.compare_spec; intros Hbl. + rewrite <- Hbl;apply Zis_gcd_0. + simpl;rewrite spec_w_0;rewrite Z.mul_0_l;rewrite Z.add_0_l. apply Zis_gcd_mod;zarith. change ([|ah|] * wB + [|al|]) with (double_to_Z w_digits w_to_Z 1 (WW ah al)). rewrite <- (@spec_double_modn1 w w_digits w_zdigits w_0 w_WW w_head0 w_add_mul_div @@ -1241,67 +1220,67 @@ Section DoubleDivGt. spec_div21 spec_compare spec_sub 1 (WW ah al) bl Hbl). apply spec_gcd_gt. rewrite (@spec_double_modn1 w w_digits w_zdigits w_0 w_WW); trivial. - apply Zlt_gt;match goal with | |- ?x mod ?y < ?y => + apply Z.lt_gt;match goal with | |- ?x mod ?y < ?y => destruct (Z_mod_lt x y);zarith end. - rewrite spec_w_0 in Hbl;Spec_w_to_Z bl;exfalso;omega. - rewrite spec_w_0 in Hbh;assert (H:= spec_ww_mod_gt_aux _ _ _ Hgt Hbh). + Spec_w_to_Z bl;exfalso;omega. + assert (H:= spec_ww_mod_gt_aux _ _ _ Hgt Hbh). assert (H2 : 0 < [[WW bh bl]]). - simpl;Spec_w_to_Z bl. apply Zlt_le_trans with ([|bh|]*wB);zarith. - apply Zmult_lt_0_compat;zarith. + simpl;Spec_w_to_Z bl. apply Z.lt_le_trans with ([|bh|]*wB);zarith. + apply Z.mul_pos_pos;zarith. apply Zis_gcd_mod;trivial. rewrite <- H. simpl in *;destruct (ww_mod_gt_aux ah al bh bl) as [ |mh ml]. simpl;apply Zis_gcd_0;zarith. - assert (Hmh := spec_compare w_0 mh);destruct (w_compare w_0 mh). - simpl;rewrite spec_w_0 in Hmh; rewrite <- Hmh;simpl. - assert (Hml := spec_compare w_0 ml);destruct (w_compare w_0 ml). - rewrite <- Hml;rewrite spec_w_0;simpl;apply Zis_gcd_0. - simpl;rewrite spec_w_0;simpl. - rewrite spec_w_0 in Hml. apply Zis_gcd_mod;zarith. + rewrite spec_compare, spec_w_0; case Z.compare_spec; intros Hmh. + simpl;rewrite <- Hmh;simpl. + rewrite spec_compare, spec_w_0; case Z.compare_spec; intros Hml. + rewrite <- Hml;simpl;apply Zis_gcd_0. + simpl; rewrite spec_w_0; simpl. + apply Zis_gcd_mod;zarith. change ([|bh|] * wB + [|bl|]) with (double_to_Z w_digits w_to_Z 1 (WW bh bl)). rewrite <- (@spec_double_modn1 w w_digits w_zdigits w_0 w_WW w_head0 w_add_mul_div w_div21 w_compare w_sub w_to_Z spec_to_Z spec_w_zdigits spec_w_0 spec_w_WW spec_head0 spec_add_mul_div spec_div21 spec_compare spec_sub 1 (WW bh bl) ml Hml). apply spec_gcd_gt. rewrite (@spec_double_modn1 w w_digits w_zdigits w_0 w_WW); trivial. - apply Zlt_gt;match goal with | |- ?x mod ?y < ?y => + apply Z.lt_gt;match goal with | |- ?x mod ?y < ?y => destruct (Z_mod_lt x y);zarith end. - rewrite spec_w_0 in Hml;Spec_w_to_Z ml;exfalso;omega. - rewrite spec_w_0 in Hmh. assert ([[WW bh bl]] > [[WW mh ml]]). - rewrite H;simpl; apply Zlt_gt;match goal with | |- ?x mod ?y < ?y => + Spec_w_to_Z ml;exfalso;omega. + assert ([[WW bh bl]] > [[WW mh ml]]). + rewrite H;simpl; apply Z.lt_gt;match goal with | |- ?x mod ?y < ?y => destruct (Z_mod_lt x y);zarith end. assert (H1:= spec_ww_mod_gt_aux _ _ _ H0 Hmh). assert (H3 : 0 < [[WW mh ml]]). - simpl;Spec_w_to_Z ml. apply Zlt_le_trans with ([|mh|]*wB);zarith. - apply Zmult_lt_0_compat;zarith. + simpl;Spec_w_to_Z ml. apply Z.lt_le_trans with ([|mh|]*wB);zarith. + apply Z.mul_pos_pos;zarith. apply Zis_gcd_mod;zarith. simpl in *;rewrite <- H1. destruct (ww_mod_gt_aux bh bl mh ml) as [ |rh rl]. simpl; apply Zis_gcd_0. simpl;apply Hcont. simpl in H1;rewrite H1. - apply Zlt_gt;match goal with | |- ?x mod ?y < ?y => + apply Z.lt_gt;match goal with | |- ?x mod ?y < ?y => destruct (Z_mod_lt x y);zarith end. - apply Zle_trans with (2^n/2). + apply Z.le_trans with (2^n/2). apply Zdiv_le_lower_bound;zarith. - apply Zle_trans with ([|bh|] * wB + [|bl|]);zarith. - assert (H3' := Z_div_mod_eq [[WW bh bl]] [[WW mh ml]] (Zlt_gt _ _ H3)). - assert (H4' : 0 <= [[WW bh bl]]/[[WW mh ml]]). - apply Zge_le;apply Z_div_ge0;zarith. simpl in *;rewrite H1. + apply Z.le_trans with ([|bh|] * wB + [|bl|]);zarith. + assert (H3' := Z_div_mod_eq [[WW bh bl]] [[WW mh ml]] (Z.lt_gt _ _ H3)). + assert (H4 : 0 <= [[WW bh bl]]/[[WW mh ml]]). + apply Z.ge_le;apply Z_div_ge0;zarith. simpl in *;rewrite H1. pattern ([|bh|] * wB + [|bl|]) at 2;rewrite H3'. - destruct (Zle_lt_or_eq _ _ H4'). + Z.le_elim H4. assert (H6' : [[WW bh bl]] mod [[WW mh ml]] = [[WW bh bl]] - [[WW mh ml]] * ([[WW bh bl]]/[[WW mh ml]])). simpl;pattern ([|bh|] * wB + [|bl|]) at 2;rewrite H3';ring. simpl in H6'. assert ([[WW mh ml]] <= [[WW mh ml]] * ([[WW bh bl]]/[[WW mh ml]])). - simpl;pattern ([|mh|]*wB+[|ml|]) at 1;rewrite <- Zmult_1_r;zarith. + simpl;pattern ([|mh|]*wB+[|ml|]) at 1;rewrite <- Z.mul_1_r;zarith. simpl in *;assert (H8 := Z_mod_lt [[WW bh bl]] [[WW mh ml]]);simpl in H8; zarith. assert (H8 := Z_mod_lt [[WW bh bl]] [[WW mh ml]]);simpl in *;zarith. - rewrite <- H4 in H3';rewrite Zmult_0_r in H3';simpl in H3';zarith. + rewrite <- H4 in H3';rewrite Z.mul_0_r in H3';simpl in H3';zarith. pattern n at 1;replace n with (n-1+1);try ring. rewrite Zpower_exp;zarith. change (2^1) with 2. rewrite Z_div_mult;zarith. assert (2^1 <= 2^n). change (2^1) with 2;zarith. assert (H7 := @Zpower_le_monotone_inv 2 1 n);zarith. - rewrite spec_w_0 in Hmh;Spec_w_to_Z mh;exfalso;zarith. - rewrite spec_w_0 in Hbh;Spec_w_to_Z bh;exfalso;zarith. + Spec_w_to_Z mh;exfalso;zarith. + Spec_w_to_Z bh;exfalso;zarith. Qed. Lemma spec_ww_gcd_gt_aux : @@ -1316,27 +1295,27 @@ Section DoubleDivGt. [[ww_gcd_gt_aux p cont ah al bh bl]]. Proof. induction p;intros cont n Hcont ah al bh bl Hgt Hs;simpl ww_gcd_gt_aux. - assert (0 < Zpos p). unfold Zlt;reflexivity. + assert (0 < Zpos p). unfold Z.lt;reflexivity. apply spec_ww_gcd_gt_aux_body with (n := Zpos (xI p) + n); - trivial;rewrite Zpos_xI. + trivial;rewrite Pos2Z.inj_xI. intros. apply IHp with (n := Zpos p + n);zarith. intros. apply IHp with (n := n );zarith. - apply Zle_trans with (2 ^ (2* Zpos p + 1+ n -1));zarith. - apply Zpower_le_monotone2;zarith. - assert (0 < Zpos p). unfold Zlt;reflexivity. + apply Z.le_trans with (2 ^ (2* Zpos p + 1+ n -1));zarith. + apply Z.pow_le_mono_r;zarith. + assert (0 < Zpos p). unfold Z.lt;reflexivity. apply spec_ww_gcd_gt_aux_body with (n := Zpos (xO p) + n );trivial. - rewrite (Zpos_xO p). + rewrite (Pos2Z.inj_xO p). intros. apply IHp with (n := Zpos p + n - 1);zarith. intros. apply IHp with (n := n -1 );zarith. intros;apply Hcont;zarith. - apply Zle_trans with (2^(n-1));zarith. - apply Zpower_le_monotone2;zarith. - apply Zle_trans with (2 ^ (Zpos p + n -1));zarith. - apply Zpower_le_monotone2;zarith. - apply Zle_trans with (2 ^ (2*Zpos p + n -1));zarith. - apply Zpower_le_monotone2;zarith. + apply Z.le_trans with (2^(n-1));zarith. + apply Z.pow_le_mono_r;zarith. + apply Z.le_trans with (2 ^ (Zpos p + n -1));zarith. + apply Z.pow_le_mono_r;zarith. + apply Z.le_trans with (2 ^ (2*Zpos p + n -1));zarith. + apply Z.pow_le_mono_r;zarith. apply spec_ww_gcd_gt_aux_body with (n := n+1);trivial. - rewrite Zplus_comm;trivial. + rewrite Z.add_comm;trivial. ring_simplify (n + 1 - 1);trivial. Qed. @@ -1374,11 +1353,7 @@ Section DoubleDiv. Variable spec_to_Z : forall x, 0 <= [|x|] < wB. Variable spec_ww_1 : [[ww_1]] = 1. Variable spec_ww_compare : forall x y, - match ww_compare x y with - | Eq => [[x]] = [[y]] - | Lt => [[x]] < [[y]] - | Gt => [[x]] > [[y]] - end. + ww_compare x y = Z.compare [[x]] [[y]]. Variable spec_ww_div_gt : forall a b, [[a]] > [[b]] -> 0 < [[b]] -> let (q,r) := ww_div_gt a b in [[a]] = [[q]] * [[b]] + [[r]] /\ @@ -1400,20 +1375,20 @@ Section DoubleDiv. 0 <= [[r]] < [[b]]. Proof. intros a b Hpos;unfold ww_div. - assert (H:=spec_ww_compare a b);destruct (ww_compare a b). + rewrite spec_ww_compare; case Z.compare_spec; intros. simpl;rewrite spec_ww_1;split;zarith. simpl;split;[ring|Spec_ww_to_Z a;zarith]. - apply spec_ww_div_gt;trivial. + apply spec_ww_div_gt;auto with zarith. Qed. Lemma spec_ww_mod : forall a b, 0 < [[b]] -> [[ww_mod a b]] = [[a]] mod [[b]]. Proof. intros a b Hpos;unfold ww_mod. - assert (H := spec_ww_compare a b);destruct (ww_compare a b). + rewrite spec_ww_compare; case Z.compare_spec; intros. simpl;apply Zmod_unique with 1;try rewrite H;zarith. Spec_ww_to_Z a;symmetry;apply Zmod_small;zarith. - apply spec_ww_mod_gt;trivial. + apply spec_ww_mod_gt;auto with zarith. Qed. @@ -1431,12 +1406,7 @@ Section DoubleDiv. Variable spec_w_0 : [|w_0|] = 0. Variable spec_w_1 : [|w_1|] = 1. Variable spec_compare : - forall x y, - match w_compare x y with - | Eq => [|x|] = [|y|] - | Lt => [|x|] < [|y|] - | Gt => [|x|] > [|y|] - end. + forall x y, w_compare x y = Z.compare [|x|] [|y|]. Variable spec_eq0 : forall x, w_eq0 x = true -> [|x|] = 0. Variable spec_gcd_gt : forall a b, [|a|] > [|b|] -> Zis_gcd [|a|] [|b|] [|w_gcd_gt a b|]. @@ -1468,14 +1438,14 @@ Section DoubleDiv. assert (0 <= 1 < wB). split;zarith. apply wB_pos. assert (H1:= beta_lex _ _ _ _ _ Hle (spec_to_Z yl) H). Spec_w_to_Z yh;zarith. - unfold gcd_cont;assert (Hcmpy:=spec_compare w_1 yl); - rewrite spec_w_1 in Hcmpy. - simpl;rewrite H;simpl;destruct (w_compare w_1 yl). + unfold gcd_cont; rewrite spec_compare, spec_w_1. + case Z.compare_spec; intros Hcmpy. + simpl;rewrite H;simpl; rewrite spec_ww_1;rewrite <- Hcmpy;apply Zis_gcd_mod;zarith. rewrite <- (Zmod_unique ([|xh|]*wB+[|xl|]) 1 ([|xh|]*wB+[|xl|]) 0);zarith. rewrite H in Hle; exfalso;zarith. - assert ([|yl|] = 0). Spec_w_to_Z yl;zarith. - rewrite H0;simpl;apply Zis_gcd_0;trivial. + assert (H0 : [|yl|] = 0) by (Spec_w_to_Z yl;zarith). + simpl. rewrite H0, H;simpl;apply Zis_gcd_0;trivial. Qed. @@ -1515,7 +1485,7 @@ Section DoubleDiv. Spec_w_to_Z bh;assert ([|bh|] = 0);zarith. rewrite H1 in Hgt;simpl in Hgt. rewrite H1;simpl;auto. clear H. apply spec_gcd_gt_fix with (n:= 0);trivial. - rewrite Zplus_0_r;rewrite spec_ww_digits_. + rewrite Z.add_0_r;rewrite spec_ww_digits_. change (2 ^ Zpos (xO w_digits)) with wwB. Spec_ww_to_Z (WW bh bl);zarith. Qed. @@ -1528,7 +1498,7 @@ Section DoubleDiv. | Eq => a | Lt => ww_gcd_gt b a end). - assert (Hcmp := spec_ww_compare a b);destruct (ww_compare a b). + rewrite spec_ww_compare; case Z.compare_spec; intros Hcmp. Spec_ww_to_Z b;rewrite Hcmp. apply Zis_gcd_for_euclid with 1;zarith. ring_simplify ([[b]] - 1 * [[b]]). apply Zis_gcd_0;zarith. diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v index 4bdb75d6..5cb7405a 100644 --- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v +++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <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 *) @@ -8,17 +8,17 @@ (* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) (************************************************************************) -(*i $Id: DoubleDivn1.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - Set Implicit Arguments. -Require Import ZArith. +Require Import ZArith Ndigits. Require Import BigNumPrelude. Require Import DoubleType. Require Import DoubleBase. Local Open Scope Z_scope. +Local Infix "<<" := Pos.shiftl_nat (at level 30). + Section GENDIVN1. Variable w : Type. @@ -62,12 +62,7 @@ Section GENDIVN1. [|a1|] *wB+ [|a2|] = [|q|] * [|b|] + [|r|] /\ 0 <= [|r|] < [|b|]. Variable spec_compare : - forall x y, - match w_compare x y with - | Eq => [|x|] = [|y|] - | Lt => [|x|] < [|y|] - | Gt => [|x|] > [|y|] - end. + forall x y, w_compare x y = Z.compare [|x|] [|y|]. Variable spec_sub: forall x y, [|w_sub x y|] = ([|x|] - [|y|]) mod wB. @@ -112,8 +107,8 @@ Section GENDIVN1. destruct H4;split;trivial. rewrite spec_double_WW;trivial. rewrite <- double_wB_wwB. - rewrite Zmult_assoc;rewrite Zplus_assoc;rewrite <- Zmult_plus_distr_l. - rewrite H0;rewrite Zmult_plus_distr_l;rewrite <- Zplus_assoc. + rewrite Z.mul_assoc;rewrite Z.add_assoc;rewrite <- Z.mul_add_distr_r. + rewrite H0;rewrite Z.mul_add_distr_r;rewrite <- Z.add_assoc. rewrite H4;ring. Qed. @@ -162,14 +157,10 @@ Section GENDIVN1. | S n => double_divn1_p_aux n (double_divn1_p n) end. - Lemma p_lt_double_digits : forall n, [|p|] <= Zpos (double_digits w_digits n). + Lemma p_lt_double_digits : forall n, [|p|] <= Zpos (w_digits << n). Proof. -(* - induction n;simpl. destruct p_bounded;trivial. - case (spec_to_Z p); rewrite Zpos_xO;auto with zarith. -*) induction n;simpl. trivial. - case (spec_to_Z p); rewrite Zpos_xO;auto with zarith. + case (spec_to_Z p); rewrite Pshiftl_nat_S, Pos2Z.inj_xO;auto with zarith. Qed. Lemma spec_double_divn1_p : forall n r h l, @@ -177,14 +168,14 @@ Section GENDIVN1. let (q,r') := double_divn1_p n r h l in [|r|] * double_wB w_digits n + ([!n|h!]*2^[|p|] + - [!n|l!] / (2^(Zpos(double_digits w_digits n) - [|p|]))) + [!n|l!] / (2^(Zpos(w_digits << n) - [|p|]))) mod double_wB w_digits n = [!n|q!] * [|b2p|] + [|r'|] /\ 0 <= [|r'|] < [|b2p|]. Proof. case (spec_to_Z p); intros HH0 HH1. induction n;intros. simpl (double_divn1_p 0 r h l). - unfold double_to_Z, double_wB, double_digits. + unfold double_to_Z, double_wB, "<<". rewrite <- spec_add_mul_divp. exact (spec_div21 (w_add_mul_div p h l) b2p_le H). simpl (double_divn1_p (S n) r h l). @@ -196,24 +187,24 @@ Section GENDIVN1. replace ([|r|] * (double_wB w_digits n * double_wB w_digits n) + (([!n|hh!] * double_wB w_digits n + [!n|hl!]) * 2 ^ [|p|] + ([!n|lh!] * double_wB w_digits n + [!n|ll!]) / - 2^(Zpos (double_digits w_digits (S n)) - [|p|])) mod + 2^(Zpos (w_digits << (S n)) - [|p|])) mod (double_wB w_digits n * double_wB w_digits n)) with (([|r|] * double_wB w_digits n + ([!n|hh!] * 2^[|p|] + - [!n|hl!] / 2^(Zpos (double_digits w_digits n) - [|p|])) mod + [!n|hl!] / 2^(Zpos (w_digits << n) - [|p|])) mod double_wB w_digits n) * double_wB w_digits n + ([!n|hl!] * 2^[|p|] + - [!n|lh!] / 2^(Zpos (double_digits w_digits n) - [|p|])) mod + [!n|lh!] / 2^(Zpos (w_digits << n) - [|p|])) mod double_wB w_digits n). generalize (IHn r hh hl H);destruct (double_divn1_p n r hh hl) as (qh,rh); intros (H3,H4);rewrite H3. assert ([|rh|] < [|b2p|]). omega. replace (([!n|qh!] * [|b2p|] + [|rh|]) * double_wB w_digits n + ([!n|hl!] * 2 ^ [|p|] + - [!n|lh!] / 2 ^ (Zpos (double_digits w_digits n) - [|p|])) mod + [!n|lh!] / 2 ^ (Zpos (w_digits << n) - [|p|])) mod double_wB w_digits n) with ([!n|qh!] * [|b2p|] *double_wB w_digits n + ([|rh|]*double_wB w_digits n + ([!n|hl!] * 2 ^ [|p|] + - [!n|lh!] / 2 ^ (Zpos (double_digits w_digits n) - [|p|])) mod + [!n|lh!] / 2 ^ (Zpos (w_digits << n) - [|p|])) mod double_wB w_digits n)). 2:ring. generalize (IHn rh hl lh H0);destruct (double_divn1_p n rh hl lh) as (ql,rl); intros (H5,H6);rewrite H5. @@ -229,52 +220,52 @@ Section GENDIVN1. unfold double_wB,base. assert (UU:=p_lt_double_digits n). rewrite Zdiv_shift_r;auto with zarith. - 2:change (Zpos (double_digits w_digits (S n))) - with (2*Zpos (double_digits w_digits n));auto with zarith. - replace (2 ^ (Zpos (double_digits w_digits (S n)) - [|p|])) with - (2^(Zpos (double_digits w_digits n) - [|p|])*2^Zpos (double_digits w_digits n)). + 2:change (Zpos (w_digits << (S n))) + with (2*Zpos (w_digits << n));auto with zarith. + replace (2 ^ (Zpos (w_digits << (S n)) - [|p|])) with + (2^(Zpos (w_digits << n) - [|p|])*2^Zpos (w_digits << n)). rewrite Zdiv_mult_cancel_r;auto with zarith. - rewrite Zmult_plus_distr_l with (p:= 2^[|p|]). + rewrite Z.mul_add_distr_r with (p:= 2^[|p|]). pattern ([!n|hl!] * 2^[|p|]) at 2; - rewrite (shift_unshift_mod (Zpos(double_digits w_digits n))([|p|])([!n|hl!])); + rewrite (shift_unshift_mod (Zpos(w_digits << n))([|p|])([!n|hl!])); auto with zarith. - rewrite Zplus_assoc. + rewrite Z.add_assoc. replace - ([!n|hh!] * 2^Zpos (double_digits w_digits n)* 2^[|p|] + - ([!n|hl!] / 2^(Zpos (double_digits w_digits n)-[|p|])* - 2^Zpos(double_digits w_digits n))) + ([!n|hh!] * 2^Zpos (w_digits << n)* 2^[|p|] + + ([!n|hl!] / 2^(Zpos (w_digits << n)-[|p|])* + 2^Zpos(w_digits << n))) with (([!n|hh!] *2^[|p|] + double_to_Z w_digits w_to_Z n hl / - 2^(Zpos (double_digits w_digits n)-[|p|])) - * 2^Zpos(double_digits w_digits n));try (ring;fail). - rewrite <- Zplus_assoc. + 2^(Zpos (w_digits << n)-[|p|])) + * 2^Zpos(w_digits << n));try (ring;fail). + rewrite <- Z.add_assoc. rewrite <- (Zmod_shift_r ([|p|]));auto with zarith. replace - (2 ^ Zpos (double_digits w_digits n) * 2 ^ Zpos (double_digits w_digits n)) with - (2 ^ (Zpos (double_digits w_digits n) + Zpos (double_digits w_digits n))). - rewrite (Zmod_shift_r (Zpos (double_digits w_digits n)));auto with zarith. - replace (2 ^ (Zpos (double_digits w_digits n) + Zpos (double_digits w_digits n))) - with (2^Zpos(double_digits w_digits n) *2^Zpos(double_digits w_digits n)). - rewrite (Zmult_comm (([!n|hh!] * 2 ^ [|p|] + - [!n|hl!] / 2 ^ (Zpos (double_digits w_digits n) - [|p|])))). + (2 ^ Zpos (w_digits << n) * 2 ^ Zpos (w_digits << n)) with + (2 ^ (Zpos (w_digits << n) + Zpos (w_digits << n))). + rewrite (Zmod_shift_r (Zpos (w_digits << n)));auto with zarith. + replace (2 ^ (Zpos (w_digits << n) + Zpos (w_digits << n))) + with (2^Zpos(w_digits << n) *2^Zpos(w_digits << n)). + rewrite (Z.mul_comm (([!n|hh!] * 2 ^ [|p|] + + [!n|hl!] / 2 ^ (Zpos (w_digits << n) - [|p|])))). rewrite Zmult_mod_distr_l;auto with zarith. ring. rewrite Zpower_exp;auto with zarith. - assert (0 < Zpos (double_digits w_digits n)). unfold Zlt;reflexivity. + assert (0 < Zpos (w_digits << n)). unfold Z.lt;reflexivity. auto with zarith. apply Z_mod_lt;auto with zarith. rewrite Zpower_exp;auto with zarith. split;auto with zarith. apply Zdiv_lt_upper_bound;auto with zarith. rewrite <- Zpower_exp;auto with zarith. - replace ([|p|] + (Zpos (double_digits w_digits n) - [|p|])) with - (Zpos(double_digits w_digits n));auto with zarith. + replace ([|p|] + (Zpos (w_digits << n) - [|p|])) with + (Zpos(w_digits << n));auto with zarith. rewrite <- Zpower_exp;auto with zarith. - replace (Zpos (double_digits w_digits (S n)) - [|p|]) with - (Zpos (double_digits w_digits n) - [|p|] + - Zpos (double_digits w_digits n));trivial. - change (Zpos (double_digits w_digits (S n))) with - (2*Zpos (double_digits w_digits n)). ring. + replace (Zpos (w_digits << (S n)) - [|p|]) with + (Zpos (w_digits << n) - [|p|] + + Zpos (w_digits << n));trivial. + change (Zpos (w_digits << (S n))) with + (2*Zpos (w_digits << n)). ring. Qed. Definition double_modn1_p_aux n (modn1 : w -> word w n -> word w n -> w) r h l:= @@ -311,24 +302,25 @@ Section GENDIVN1. end end. - Lemma spec_double_digits:forall n, Zpos w_digits <= Zpos (double_digits w_digits n). + Lemma spec_double_digits:forall n, Zpos w_digits <= Zpos (w_digits << n). Proof. induction n;simpl;auto with zarith. - change (Zpos (xO (double_digits w_digits n))) with - (2*Zpos (double_digits w_digits n)). - assert (0 < Zpos w_digits);auto with zarith. - exact (refl_equal Lt). + rewrite Pshiftl_nat_S. + change (Zpos (xO (w_digits << n))) with + (2*Zpos (w_digits << n)). + assert (0 < Zpos w_digits) by reflexivity. + auto with zarith. Qed. Lemma spec_high : forall n (x:word w n), - [|high n x|] = [!n|x!] / 2^(Zpos (double_digits w_digits n) - Zpos w_digits). + [|high n x|] = [!n|x!] / 2^(Zpos (w_digits << n) - Zpos w_digits). Proof. induction n;intros. - unfold high,double_digits,double_to_Z. + unfold high,double_to_Z. rewrite Pshiftl_nat_0. replace (Zpos w_digits - Zpos w_digits) with 0;try ring. simpl. rewrite <- (Zdiv_unique [|x|] 1 [|x|] 0);auto with zarith. assert (U2 := spec_double_digits n). - assert (U3 : 0 < Zpos w_digits). exact (refl_equal Lt). + assert (U3 : 0 < Zpos w_digits). exact (eq_refl Lt). destruct x;unfold high;fold high. unfold double_to_Z,zn2z_to_Z;rewrite spec_0. rewrite Zdiv_0_l;trivial. @@ -336,18 +328,18 @@ Section GENDIVN1. assert (U1 := spec_double_to_Z w_digits w_to_Z spec_to_Z n w1). simpl [!S n|WW w0 w1!]. unfold double_wB,base;rewrite Zdiv_shift_r;auto with zarith. - replace (2 ^ (Zpos (double_digits w_digits (S n)) - Zpos w_digits)) with - (2^(Zpos (double_digits w_digits n) - Zpos w_digits) * - 2^Zpos (double_digits w_digits n)). + replace (2 ^ (Zpos (w_digits << (S n)) - Zpos w_digits)) with + (2^(Zpos (w_digits << n) - Zpos w_digits) * + 2^Zpos (w_digits << n)). rewrite Zdiv_mult_cancel_r;auto with zarith. rewrite <- Zpower_exp;auto with zarith. - replace (Zpos (double_digits w_digits n) - Zpos w_digits + - Zpos (double_digits w_digits n)) with - (Zpos (double_digits w_digits (S n)) - Zpos w_digits);trivial. - change (Zpos (double_digits w_digits (S n))) with - (2*Zpos (double_digits w_digits n));ring. - change (Zpos (double_digits w_digits (S n))) with - (2*Zpos (double_digits w_digits n)); auto with zarith. + replace (Zpos (w_digits << n) - Zpos w_digits + + Zpos (w_digits << n)) with + (Zpos (w_digits << (S n)) - Zpos w_digits);trivial. + change (Zpos (w_digits << (S n))) with + (2*Zpos (w_digits << n));ring. + change (Zpos (w_digits << (S n))) with + (2*Zpos (w_digits << n)); auto with zarith. Qed. Definition double_divn1 (n:nat) (a:word w n) (b:w) := @@ -373,30 +365,30 @@ Section GENDIVN1. intros n a b H. unfold double_divn1. case (spec_head0 H); intros H0 H1. case (spec_to_Z (w_head0 b)); intros HH1 HH2. - generalize (spec_compare (w_head0 b) w_0); case w_compare; + rewrite spec_compare; case Z.compare_spec; rewrite spec_0; intros H2; auto with zarith. assert (Hv1: wB/2 <= [|b|]). - generalize H0; rewrite H2; rewrite Zpower_0_r; - rewrite Zmult_1_l; auto. + generalize H0; rewrite H2; rewrite Z.pow_0_r; + rewrite Z.mul_1_l; auto. assert (Hv2: [|w_0|] < [|b|]). rewrite spec_0; auto. generalize (spec_double_divn1_0 Hv1 n a Hv2). - rewrite spec_0;rewrite Zmult_0_l; rewrite Zplus_0_l; auto. + rewrite spec_0;rewrite Z.mul_0_l; rewrite Z.add_0_l; auto. contradict H2; auto with zarith. assert (HHHH : 0 < [|w_head0 b|]); auto with zarith. assert ([|w_head0 b|] < Zpos w_digits). - case (Zle_or_lt (Zpos w_digits) [|w_head0 b|]); auto; intros HH. + case (Z.le_gt_cases (Zpos w_digits) [|w_head0 b|]); auto; intros HH. assert (2 ^ [|w_head0 b|] < wB). - apply Zle_lt_trans with (2 ^ [|w_head0 b|] * [|b|]);auto with zarith. + apply Z.le_lt_trans with (2 ^ [|w_head0 b|] * [|b|]);auto with zarith. replace (2 ^ [|w_head0 b|]) with (2^[|w_head0 b|] * 1);try (ring;fail). - apply Zmult_le_compat;auto with zarith. + apply Z.mul_le_mono_nonneg;auto with zarith. assert (wB <= 2^[|w_head0 b|]). unfold base;apply Zpower_le_monotone;auto with zarith. omega. assert ([|w_add_mul_div (w_head0 b) b w_0|] = 2 ^ [|w_head0 b|] * [|b|]). 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 Z.add_0_r; rewrite Z.mul_comm. rewrite Zmod_small; auto with zarith. assert (H5 := spec_to_Z (high n a)). assert @@ -404,21 +396,21 @@ Section GENDIVN1. <[|w_add_mul_div (w_head0 b) b w_0|]). rewrite H4. rewrite spec_add_mul_div;auto with zarith. - rewrite spec_0;rewrite Zmult_0_l;rewrite Zplus_0_l. + rewrite spec_0;rewrite Z.mul_0_l;rewrite Z.add_0_l. assert (([|high n a|]/2^(Zpos w_digits - [|w_head0 b|])) < wB). apply Zdiv_lt_upper_bound;auto with zarith. - apply Zlt_le_trans with wB;auto with zarith. + apply Z.lt_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_gt_0 2 (Zpos w_digits - [|w_head0 b|])); + apply Z.mul_le_mono_nonneg;auto with zarith. + assert (H6 := Z.pow_pos_nonneg 2 (Zpos w_digits - [|w_head0 b|])); 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). + apply Z.lt_le_trans with wB;auto with zarith. + apply Z.le_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_1_r. + apply Z.mul_le_mono_nonneg;auto with zarith. + pattern 2 at 1;rewrite <- Z.pow_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. @@ -428,40 +420,40 @@ Section GENDIVN1. (double_0 w_0 n)) as (q,r). assert (U:= spec_double_digits n). rewrite spec_double_0 in H7;trivial;rewrite Zdiv_0_l in H7. - rewrite Zplus_0_r in H7. + rewrite Z.add_0_r in H7. rewrite spec_add_mul_div in H7;auto with zarith. - rewrite spec_0 in H7;rewrite Zmult_0_l in H7;rewrite Zplus_0_l in H7. + rewrite spec_0 in H7;rewrite Z.mul_0_l in H7;rewrite Z.add_0_l in H7. assert (([|high n a|] / 2 ^ (Zpos w_digits - [|w_head0 b|])) mod wB - = [!n|a!] / 2^(Zpos (double_digits w_digits n) - [|w_head0 b|])). + = [!n|a!] / 2^(Zpos (w_digits << n) - [|w_head0 b|])). rewrite Zmod_small;auto with zarith. rewrite spec_high. rewrite Zdiv_Zdiv;auto with zarith. rewrite <- Zpower_exp;auto with zarith. - replace (Zpos (double_digits w_digits n) - Zpos w_digits + + replace (Zpos (w_digits << n) - Zpos w_digits + (Zpos w_digits - [|w_head0 b|])) - with (Zpos (double_digits w_digits n) - [|w_head0 b|]);trivial;ring. - assert (H8 := Zpower_gt_0 2 (Zpos w_digits - [|w_head0 b|]));auto with zarith. + with (Zpos (w_digits << n) - [|w_head0 b|]);trivial;ring. + assert (H8 := Z.pow_pos_nonneg 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 Z.le_lt_trans with ([|high n a|]);auto with zarith. apply Zdiv_le_upper_bound;auto with zarith. - pattern ([|high n a|]) at 1;rewrite <- Zmult_1_r. - apply Zmult_le_compat;auto with zarith. + pattern ([|high n a|]) at 1;rewrite <- Z.mul_1_r. + apply Z.mul_le_mono_nonneg;auto with zarith. rewrite H8 in H7;unfold double_wB,base in H7. rewrite <- shift_unshift_mod in H7;auto with zarith. rewrite H4 in H7. assert ([|w_add_mul_div (w_sub w_zdigits (w_head0 b)) w_0 r|] = [|r|]/2^[|w_head0 b|]). rewrite spec_add_mul_div. - rewrite spec_0;rewrite Zmult_0_l;rewrite Zplus_0_l. + rewrite spec_0;rewrite Z.mul_0_l;rewrite Z.add_0_l. replace (Zpos w_digits - [|w_sub w_zdigits (w_head0 b)|]) with ([|w_head0 b|]). 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 Z.le_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_gt_0 2 ([|w_head0 b|]));auto with zarith. + pattern ([|r|]) at 1;rewrite <- Z.mul_1_r. + apply Z.mul_le_mono_nonneg;auto with zarith. + assert (H10 := Z.pow_pos_nonneg 2 ([|w_head0 b|]));auto with zarith. rewrite spec_sub. rewrite Zmod_small; auto with zarith. split; auto with zarith. @@ -483,7 +475,7 @@ Section GENDIVN1. auto with zarith. rewrite H9. apply Zdiv_lt_upper_bound;auto with zarith. - rewrite Zmult_comm;auto with zarith. + rewrite Z.mul_comm;auto with zarith. exact (spec_double_to_Z w_digits w_to_Z spec_to_Z n a). Qed. @@ -506,7 +498,7 @@ Section GENDIVN1. double_modn1 n a b = snd (double_divn1 n a b). Proof. intros n a b;unfold double_divn1,double_modn1. - generalize (spec_compare (w_head0 b) w_0); case w_compare; + rewrite spec_compare; case Z.compare_spec; rewrite spec_0; intros H2; auto with zarith. apply spec_double_modn1_0. apply spec_double_modn1_0. diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.v index 36e3da9b..0a70dbf4 100644 --- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.v +++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <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 *) @@ -8,8 +8,6 @@ (* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) (************************************************************************) -(*i $Id: DoubleLift.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - Set Implicit Arguments. Require Import ZArith. @@ -106,17 +104,9 @@ Section DoubleLift. Variable spec_w_W0 : forall h, [[w_W0 h]] = [|h|] * wB. Variable spec_w_0W : forall l, [[w_0W l]] = [|l|]. Variable spec_compare : forall x y, - match w_compare x y with - | Eq => [|x|] = [|y|] - | Lt => [|x|] < [|y|] - | Gt => [|x|] > [|y|] - end. + w_compare x y = Z.compare [|x|] [|y|]. Variable spec_ww_compare : forall x y, - match ww_compare x y with - | Eq => [[x]] = [[y]] - | Lt => [[x]] < [[y]] - | Gt => [[x]] > [[y]] - end. + ww_compare x y = Z.compare [[x]] [[y]]. Variable spec_ww_digits : ww_Digits = xO w_digits. Variable spec_w_head00 : forall x, [|x|] = 0 -> [|w_head0 x|] = Zpos w_digits. Variable spec_w_head0 : forall x, 0 < [|x|] -> @@ -150,20 +140,20 @@ Section DoubleLift. case (spec_to_Z xh); intros Hx1 Hx2. case (spec_to_Z xl); intros Hy1 Hy2. assert (F1: [|xh|] = 0). - case (Zle_lt_or_eq _ _ Hy1); auto; intros Hy3. - absurd (0 < [|xh|] * wB + [|xl|]); auto with zarith. - apply Zlt_le_trans with (1 := Hy3); auto with zarith. - pattern [|xl|] at 1; rewrite <- (Zplus_0_l [|xl|]). - apply Zplus_le_compat_r; auto with zarith. - case (Zle_lt_or_eq _ _ Hx1); auto; intros Hx3. - absurd (0 < [|xh|] * wB + [|xl|]); auto with zarith. - rewrite <- Hy3; rewrite Zplus_0_r; auto with zarith. - apply Zmult_lt_0_compat; auto with zarith. - generalize (spec_compare w_0 xh); case w_compare. + { Z.le_elim Hy1; auto. + - absurd (0 < [|xh|] * wB + [|xl|]); auto with zarith. + apply Z.lt_le_trans with (1 := Hy1); auto with zarith. + pattern [|xl|] at 1; rewrite <- (Z.add_0_l [|xl|]). + apply Z.add_le_mono_r; auto with zarith. + - Z.le_elim Hx1; auto. + absurd (0 < [|xh|] * wB + [|xl|]); auto with zarith. + rewrite <- Hy1; rewrite Z.add_0_r; auto with zarith. + apply Z.mul_pos_pos; auto with zarith. } + rewrite spec_compare. case Z.compare_spec. intros H; simpl. rewrite spec_w_add; rewrite spec_w_head00. rewrite spec_zdigits; rewrite spec_ww_digits. - rewrite Zpos_xO; auto with zarith. + rewrite Pos2Z.inj_xO; auto with zarith. rewrite F1 in Hx; auto with zarith. rewrite spec_w_0; auto with zarith. rewrite spec_w_0; auto with zarith. @@ -173,44 +163,43 @@ Section DoubleLift. wwB/ 2 <= 2 ^ [[ww_head0 x]] * [[x]] < wwB. Proof. clear spec_ww_zdigits. - rewrite wwB_div_2;rewrite Zmult_comm;rewrite wwB_wBwB. + rewrite wwB_div_2;rewrite Z.mul_comm;rewrite wwB_wBwB. assert (U:= lt_0_wB w_digits); destruct x as [ |xh xl];simpl ww_to_Z;intros H. - unfold Zlt in H;discriminate H. - assert (H0 := spec_compare w_0 xh);rewrite spec_w_0 in H0. - destruct (w_compare w_0 xh). - rewrite <- H0. simpl Zplus. rewrite <- H0 in H;simpl in H. + unfold Z.lt in H;discriminate H. + rewrite spec_compare, spec_w_0. case Z.compare_spec; intros H0. + rewrite <- H0 in *. simpl Z.add. simpl in H. case (spec_to_Z w_zdigits); case (spec_to_Z (w_head0 xl)); intros HH1 HH2 HH3 HH4. rewrite spec_w_add. rewrite spec_zdigits; rewrite Zpower_exp; auto with zarith. case (spec_w_head0 H); intros H1 H2. - rewrite Zpower_2; fold wB; rewrite <- Zmult_assoc; split. - apply Zmult_le_compat_l; auto with zarith. - apply Zmult_lt_compat_l; auto with zarith. + rewrite Z.pow_2_r; fold wB; rewrite <- Z.mul_assoc; split. + apply Z.mul_le_mono_nonneg_l; auto with zarith. + apply Z.mul_lt_mono_pos_l; auto with zarith. assert (H1 := spec_w_head0 H0). rewrite spec_w_0W. split. - rewrite Zmult_plus_distr_r;rewrite Zmult_assoc. - apply Zle_trans with (2 ^ [|w_head0 xh|] * [|xh|] * wB). - rewrite Zmult_comm; zarith. + rewrite Z.mul_add_distr_l;rewrite Z.mul_assoc. + apply Z.le_trans with (2 ^ [|w_head0 xh|] * [|xh|] * wB). + rewrite Z.mul_comm; zarith. assert (0 <= 2 ^ [|w_head0 xh|] * [|xl|]);zarith. - assert (H2:=spec_to_Z xl);apply Zmult_le_0_compat;zarith. + assert (H2:=spec_to_Z xl);apply Z.mul_nonneg_nonneg;zarith. case (spec_to_Z (w_head0 xh)); intros H2 _. generalize ([|w_head0 xh|]) H1 H2;clear H1 H2; intros p H1 H2. assert (Eq1 : 2^p < wB). - rewrite <- (Zmult_1_r (2^p));apply Zle_lt_trans with (2^p*[|xh|]);zarith. + rewrite <- (Z.mul_1_r (2^p));apply Z.le_lt_trans with (2^p*[|xh|]);zarith. assert (Eq2: p < Zpos w_digits). - destruct (Zle_or_lt (Zpos w_digits) p);trivial;contradict Eq1. - apply Zle_not_lt;unfold base;apply Zpower_le_monotone;zarith. + destruct (Z.le_gt_cases (Zpos w_digits) p);trivial;contradict Eq1. + apply Z.le_ngt;unfold base;apply Zpower_le_monotone;zarith. assert (Zpos w_digits = p + (Zpos w_digits - p)). ring. - rewrite Zpower_2. + rewrite Z.pow_2_r. unfold base at 2;rewrite H3;rewrite Zpower_exp;zarith. - rewrite <- Zmult_assoc; apply Zmult_lt_compat_l; zarith. - rewrite <- (Zplus_0_r (2^(Zpos w_digits - p)*wB));apply beta_lex_inv;zarith. - apply Zmult_lt_reg_r with (2 ^ p); zarith. + rewrite <- Z.mul_assoc; apply Z.mul_lt_mono_pos_l; zarith. + rewrite <- (Z.add_0_r (2^(Zpos w_digits - p)*wB));apply beta_lex_inv;zarith. + apply Z.mul_lt_mono_pos_r with (2 ^ p); zarith. rewrite <- Zpower_exp;zarith. - rewrite Zmult_comm;ring_simplify (Zpos w_digits - p + p);fold wB;zarith. + rewrite Z.mul_comm;ring_simplify (Zpos w_digits - p + p);fold wB;zarith. assert (H1 := spec_to_Z xh);zarith. Qed. @@ -222,22 +211,22 @@ Section DoubleLift. case (spec_to_Z xh); intros Hx1 Hx2. case (spec_to_Z xl); intros Hy1 Hy2. assert (F1: [|xh|] = 0). - case (Zle_lt_or_eq _ _ Hy1); auto; intros Hy3. - absurd (0 < [|xh|] * wB + [|xl|]); auto with zarith. - apply Zlt_le_trans with (1 := Hy3); auto with zarith. - pattern [|xl|] at 1; rewrite <- (Zplus_0_l [|xl|]). - apply Zplus_le_compat_r; auto with zarith. - case (Zle_lt_or_eq _ _ Hx1); auto; intros Hx3. - absurd (0 < [|xh|] * wB + [|xl|]); auto with zarith. - rewrite <- Hy3; rewrite Zplus_0_r; auto with zarith. - apply Zmult_lt_0_compat; auto with zarith. + { Z.le_elim Hy1; auto. + - absurd (0 < [|xh|] * wB + [|xl|]); auto with zarith. + apply Z.lt_le_trans with (1 := Hy1); auto with zarith. + pattern [|xl|] at 1; rewrite <- (Z.add_0_l [|xl|]). + apply Z.add_le_mono_r; auto with zarith. + - Z.le_elim Hx1; auto. + absurd (0 < [|xh|] * wB + [|xl|]); auto with zarith. + rewrite <- Hy1; rewrite Z.add_0_r; auto with zarith. + apply Z.mul_pos_pos; auto with zarith. } assert (F2: [|xl|] = 0). rewrite F1 in Hx; auto with zarith. - generalize (spec_compare w_0 xl); case w_compare. + rewrite spec_compare; case Z.compare_spec. intros H; simpl. rewrite spec_w_add; rewrite spec_w_tail00; auto. rewrite spec_zdigits; rewrite spec_ww_digits. - rewrite Zpos_xO; auto with zarith. + rewrite Pos2Z.inj_xO; auto with zarith. rewrite spec_w_0; auto with zarith. rewrite spec_w_0; auto with zarith. Qed. @@ -247,52 +236,51 @@ Section DoubleLift. Proof. clear spec_ww_zdigits. destruct x as [ |xh xl];simpl ww_to_Z;intros H. - unfold Zlt in H;discriminate H. - assert (H0 := spec_compare w_0 xl);rewrite spec_w_0 in H0. - destruct (w_compare w_0 xl). - rewrite <- H0; rewrite Zplus_0_r. + unfold Z.lt in H;discriminate H. + rewrite spec_compare, spec_w_0. case Z.compare_spec; intros H0. + rewrite <- H0; rewrite Z.add_0_r. case (spec_to_Z (w_tail0 xh)); intros HH1 HH2. - generalize H; rewrite <- H0; rewrite Zplus_0_r; clear H; intros H. + generalize H; rewrite <- H0; rewrite Z.add_0_r; clear H; intros H. case (@spec_w_tail0 xh). - apply Zmult_lt_reg_r with wB; auto with zarith. + apply Z.mul_lt_mono_pos_r with wB; auto with zarith. unfold base; auto with zarith. intros z (Hz1, Hz2); exists z; split; auto. - rewrite spec_w_add; rewrite (fun x => Zplus_comm [|x|]). + rewrite spec_w_add; rewrite (fun x => Z.add_comm [|x|]). rewrite spec_zdigits; rewrite Zpower_exp; auto with zarith. - rewrite Zmult_assoc; rewrite <- Hz2; auto. + rewrite Z.mul_assoc; rewrite <- Hz2; auto. case (spec_to_Z (w_tail0 xh)); intros HH1 HH2. case (spec_w_tail0 H0); intros z (Hz1, Hz2). assert (Hp: [|w_tail0 xl|] < Zpos w_digits). - case (Zle_or_lt (Zpos w_digits) [|w_tail0 xl|]); auto; intros H1. + case (Z.le_gt_cases (Zpos w_digits) [|w_tail0 xl|]); auto; intros H1. absurd (2 ^ (Zpos w_digits) <= 2 ^ [|w_tail0 xl|]). - apply Zlt_not_le. + apply Z.lt_nge. case (spec_to_Z xl); intros HH3 HH4. - apply Zle_lt_trans with (2 := HH4). - apply Zle_trans with (1 * 2 ^ [|w_tail0 xl|]); auto with zarith. + apply Z.le_lt_trans with (2 := HH4). + apply Z.le_trans with (1 * 2 ^ [|w_tail0 xl|]); auto with zarith. rewrite Hz2. - apply Zmult_le_compat_r; auto with zarith. + apply Z.mul_le_mono_nonneg_r; auto with zarith. apply Zpower_le_monotone; auto with zarith. exists ([|xh|] * (2 ^ ((Zpos w_digits - [|w_tail0 xl|]) - 1)) + z); split. - apply Zplus_le_0_compat; auto. - apply Zmult_le_0_compat; auto with zarith. + apply Z.add_nonneg_nonneg; auto. + apply Z.mul_nonneg_nonneg; auto with zarith. case (spec_to_Z xh); auto. rewrite spec_w_0W. - rewrite (Zmult_plus_distr_r 2); rewrite <- Zplus_assoc. - rewrite Zmult_plus_distr_l; rewrite <- Hz2. - apply f_equal2 with (f := Zplus); auto. - rewrite (Zmult_comm 2). - repeat rewrite <- Zmult_assoc. - apply f_equal2 with (f := Zmult); auto. + rewrite (Z.mul_add_distr_l 2); rewrite <- Z.add_assoc. + rewrite Z.mul_add_distr_r; rewrite <- Hz2. + apply f_equal2 with (f := Z.add); auto. + rewrite (Z.mul_comm 2). + repeat rewrite <- Z.mul_assoc. + apply f_equal2 with (f := Z.mul); auto. case (spec_to_Z (w_tail0 xl)); intros HH3 HH4. - pattern 2 at 2; rewrite <- Zpower_1_r. + pattern 2 at 2; rewrite <- Z.pow_1_r. lazy beta; repeat rewrite <- Zpower_exp; auto with zarith. - unfold base; apply f_equal with (f := Zpower 2); auto with zarith. + unfold base; apply f_equal with (f := Z.pow 2); auto with zarith. contradict H0; case (spec_to_Z xl); auto with zarith. Qed. - Hint Rewrite Zdiv_0_l Zmult_0_l Zplus_0_l Zmult_0_r Zplus_0_r + Hint Rewrite Zdiv_0_l Z.mul_0_l Z.add_0_l Z.mul_0_r Z.add_0_r spec_w_W0 spec_w_0W spec_w_WW spec_w_0 (wB_div w_digits w_to_Z spec_to_Z) (wB_div_plus w_digits w_to_Z spec_to_Z) : w_rewrite. @@ -316,20 +304,20 @@ Section DoubleLift. intros xh xl yh yl p zdigits;assert (HwwB := wwB_pos w_digits). case (spec_to_w_Z p); intros Hv1 Hv2. replace (Zpos (xO w_digits)) with (Zpos w_digits + Zpos w_digits). - 2 : rewrite Zpos_xO;ring. + 2 : rewrite Pos2Z.inj_xO;ring. replace (Zpos w_digits + Zpos w_digits - [[p]]) with (Zpos w_digits + (Zpos w_digits - [[p]])). 2:ring. intros Hp; assert (Hxh := spec_to_Z xh);assert (Hxl:=spec_to_Z xl); assert (Hx := spec_ww_to_Z w_digits w_to_Z spec_to_Z (WW xh xl)); simpl in Hx;assert (Hyh := spec_to_Z yh);assert (Hyl:=spec_to_Z yl); assert (Hy:=spec_ww_to_Z w_digits w_to_Z spec_to_Z (WW yh yl));simpl in Hy. - generalize (spec_ww_compare p zdigits); case ww_compare; intros H1. + rewrite spec_ww_compare; case Z.compare_spec; intros H1. rewrite H1; unfold zdigits; rewrite spec_w_0W. - rewrite spec_zdigits; rewrite Zminus_diag; rewrite Zplus_0_r. + rewrite spec_zdigits; rewrite Z.sub_diag; rewrite Z.add_0_r. simpl ww_to_Z; w_rewrite;zarith. fold wB. - rewrite Zmult_plus_distr_l;rewrite <- Zmult_assoc;rewrite <- Zplus_assoc. - rewrite <- Zpower_2. + rewrite Z.mul_add_distr_r;rewrite <- Z.mul_assoc;rewrite <- Z.add_assoc. + rewrite <- Z.pow_2_r. 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. @@ -339,7 +327,7 @@ Section DoubleLift. case (spec_to_w_Z p); intros HH1 HH2; split; auto. generalize H1; unfold zdigits; rewrite spec_w_0W; rewrite spec_zdigits; intros tmp. - apply Zlt_le_trans with (1 := tmp). + apply Z.lt_le_trans with (1 := tmp). unfold base. apply Zpower2_le_lin; auto with zarith. 2: generalize H1; unfold zdigits; rewrite spec_w_0W; @@ -350,22 +338,22 @@ Section DoubleLift. rewrite HH0; auto with zarith. repeat rewrite spec_w_add_mul_div with (1 := HH). rewrite HH0. - rewrite Zmult_plus_distr_l. + rewrite Z.mul_add_distr_r. pattern ([|xl|] * 2 ^ [[p]]) at 2; rewrite shift_unshift_mod with (n:= Zpos w_digits);fold wB;zarith. replace ([|xh|] * wB * 2^[[p]]) with ([|xh|] * 2^[[p]] * wB). 2:ring. - rewrite Zplus_assoc;rewrite <- Zmult_plus_distr_l. rewrite <- Zplus_assoc. + rewrite Z.add_assoc;rewrite <- Z.mul_add_distr_r. rewrite <- Z.add_assoc. unfold base at 5;rewrite <- Zmod_shift_r;zarith. unfold base;rewrite Zmod_shift_r with (b:= Zpos (ww_digits w_digits)); fold wB;fold wwB;zarith. - rewrite wwB_wBwB;rewrite Zpower_2; rewrite Zmult_mod_distr_r;zarith. - unfold ww_digits;rewrite Zpos_xO;zarith. apply Z_mod_lt;zarith. + rewrite wwB_wBwB;rewrite Z.pow_2_r; rewrite Zmult_mod_distr_r;zarith. + unfold ww_digits;rewrite Pos2Z.inj_xO;zarith. apply Z_mod_lt;zarith. split;zarith. apply Zdiv_lt_upper_bound;zarith. rewrite <- Zpower_exp;zarith. ring_simplify ([[p]] + (Zpos w_digits - [[p]]));fold wB;zarith. assert (Hv: [[p]] > Zpos w_digits). generalize H1; clear H1. - unfold zdigits; rewrite spec_w_0W; rewrite spec_zdigits; auto. + unfold zdigits; rewrite spec_w_0W; rewrite spec_zdigits; auto with zarith. clear H1. assert (HH0: [|low (ww_sub p zdigits)|] = [[p]] - Zpos w_digits). rewrite spec_low. @@ -374,10 +362,10 @@ Section DoubleLift. rewrite <- Zmod_div_mod; auto with zarith. rewrite Zmod_small; auto with zarith. split; auto with zarith. - apply Zle_lt_trans with (Zpos w_digits); auto with zarith. + apply Z.le_lt_trans with (Zpos w_digits); auto with zarith. unfold base; apply Zpower2_lt_lin; auto with zarith. exists wB; unfold base. - unfold ww_digits; rewrite (Zpos_xO w_digits). + unfold ww_digits; rewrite (Pos2Z.inj_xO w_digits). rewrite <- Zpower_exp; auto with zarith. apply f_equal with (f := fun x => 2 ^ x); auto with zarith. assert (HH: [|low (ww_sub p zdigits)|] <= Zpos w_digits). @@ -390,25 +378,25 @@ Section DoubleLift. pattern wB at 5;replace wB with (2^(([[p]] - Zpos w_digits) + (Zpos w_digits - ([[p]] - Zpos w_digits)))). - rewrite Zpower_exp;zarith. rewrite Zmult_assoc. + rewrite Zpower_exp;zarith. rewrite Z.mul_assoc. rewrite Z_div_plus_l;zarith. rewrite shift_unshift_mod with (a:= [|yh|]) (p:= [[p]] - Zpos w_digits) (n := Zpos w_digits);zarith. fold wB. set (u := [[p]] - Zpos w_digits). replace [[p]] with (u + Zpos w_digits);zarith. - rewrite Zpower_exp;zarith. rewrite Zmult_assoc. fold wB. - repeat rewrite Zplus_assoc. rewrite <- Zmult_plus_distr_l. - repeat rewrite <- Zplus_assoc. + rewrite Zpower_exp;zarith. rewrite Z.mul_assoc. fold wB. + repeat rewrite Z.add_assoc. rewrite <- Z.mul_add_distr_r. + repeat rewrite <- Z.add_assoc. unfold base;rewrite Zmod_shift_r with (b:= Zpos (ww_digits w_digits)); fold wB;fold wwB;zarith. unfold base;rewrite Zmod_shift_r with (a:= Zpos w_digits) (b:= Zpos w_digits);fold wB;fold wwB;zarith. - rewrite wwB_wBwB; rewrite Zpower_2; rewrite Zmult_mod_distr_r;zarith. - rewrite Zmult_plus_distr_l. + rewrite wwB_wBwB; rewrite Z.pow_2_r; rewrite Zmult_mod_distr_r;zarith. + rewrite Z.mul_add_distr_r. replace ([|xh|] * wB * 2 ^ u) with ([|xh|]*2^u*wB). 2:ring. - repeat rewrite <- Zplus_assoc. - rewrite (Zplus_comm ([|xh|] * 2 ^ u * wB)). + repeat rewrite <- Z.add_assoc. + rewrite (Z.add_comm ([|xh|] * 2 ^ u * wB)). 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. @@ -416,7 +404,7 @@ Section DoubleLift. rewrite <- Zpower_exp;zarith. fold u. ring_simplify (u + (Zpos w_digits - u)); fold - wB;zarith. unfold ww_digits;rewrite Zpos_xO;zarith. + wB;zarith. unfold ww_digits;rewrite Pos2Z.inj_xO;zarith. unfold base;rewrite <- Zmod_shift_r;zarith. fold base;apply Z_mod_lt;zarith. unfold u; split;zarith. unfold u; split;zarith. @@ -446,15 +434,14 @@ Section DoubleLift. clear H1;w_rewrite);simpl ww_add_mul_div. replace [[WW w_0 w_0]] with 0;[w_rewrite|simpl;w_rewrite;trivial]. intros Heq;rewrite <- Heq;clear Heq; auto. - generalize (spec_ww_compare p (w_0W w_zdigits)); - case ww_compare; intros H1; w_rewrite. + rewrite spec_ww_compare. case Z.compare_spec; intros H1; w_rewrite. rewrite (spec_w_add_mul_div w_0 w_0);w_rewrite;zarith. generalize H1; w_rewrite; rewrite spec_zdigits; clear H1; intros H1. assert (HH0: [|low p|] = [[p]]). rewrite spec_low. apply Zmod_small. case (spec_to_w_Z p); intros HH1 HH2; split; auto. - apply Zlt_le_trans with (1 := H1). + apply Z.lt_le_trans with (1 := H1). unfold base; apply Zpower2_le_lin; auto with zarith. rewrite HH0; auto with zarith. replace [[WW w_0 w_0]] with 0;[w_rewrite|simpl;w_rewrite;trivial]. @@ -462,20 +449,21 @@ Section DoubleLift. generalize (spec_ww_compare p (w_0W w_zdigits)); case ww_compare; intros H1; w_rewrite. rewrite (spec_w_add_mul_div w_0 w_0);w_rewrite;zarith. - rewrite Zpos_xO in H;zarith. + rewrite Pos2Z.inj_xO in H;zarith. assert (HH: [|low (ww_sub p (w_0W w_zdigits)) |] = [[p]] - Zpos w_digits). - generalize H1; clear H1. + symmetry in H1; change ([[p]] > [[w_0W w_zdigits]]) in H1. + revert H1. rewrite spec_low. rewrite spec_ww_sub; w_rewrite; intros H1. rewrite <- Zmod_div_mod; auto with zarith. rewrite Zmod_small; auto with zarith. split; auto with zarith. - apply Zle_lt_trans with (Zpos w_digits); auto with zarith. + apply Z.le_lt_trans with (Zpos w_digits); auto with zarith. unfold base; apply Zpower2_lt_lin; auto with zarith. unfold base; auto with zarith. unfold base; auto with zarith. exists wB; unfold base. - unfold ww_digits; rewrite (Zpos_xO w_digits). + unfold ww_digits; rewrite (Pos2Z.inj_xO w_digits). rewrite <- Zpower_exp; auto with zarith. apply f_equal with (f := fun x => 2 ^ x); auto with zarith. case (spec_to_Z xh); auto with zarith. diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.v index 834e85d2..7a92ff0c 100644 --- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.v +++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <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 *) @@ -8,8 +8,6 @@ (* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) (************************************************************************) -(*i $Id: DoubleMul.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - Set Implicit Arguments. Require Import ZArith. @@ -248,12 +246,7 @@ Section DoubleMul. Variable spec_w_W0 : forall h, [[w_W0 h]] = [|h|] * wB. Variable spec_w_0W : forall l, [[w_0W l]] = [|l|]. Variable spec_w_compare : - forall x y, - match w_compare x y with - | Eq => [|x|] = [|y|] - | Lt => [|x|] < [|y|] - | Gt => [|x|] > [|y|] - end. + forall x y, w_compare x y = Z.compare [|x|] [|y|]. Variable spec_w_succ : forall x, [|w_succ x|] = ([|x|] + 1) mod wB. Variable spec_w_add_c : forall x y, [+|w_add_c x y|] = [|x|] + [|y|]. Variable spec_w_add : forall x y, [|w_add x y|] = ([|x|] + [|y|]) mod wB. @@ -332,7 +325,7 @@ Section DoubleMul. destruct cc as [ | cch ccl]; simpl zn2z_to_Z; simpl ww_to_Z. 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. + rewrite <- (Z.add_0_r ([|wc|]*wB));rewrite H;apply mult_add_ineq3;zarith. simpl ww_to_Z in H1. assert (U:=spec_to_Z cch). assert ([|wc|]*wB + [|cch|] <= 2*wB - 3). destruct (Z_le_gt_dec ([|wc|]*wB + [|cch|]) (2*wB - 3));trivial. @@ -342,21 +335,21 @@ Section DoubleMul. assert (H5 := Zmult_lt_b _ _ _ (spec_to_Z xl) (spec_to_Z yh)). omega. generalize H3;clear H3;rewrite <- H1. - rewrite Zplus_assoc; rewrite Zpower_2; rewrite Zmult_assoc; - rewrite <- Zmult_plus_distr_l. + rewrite Z.add_assoc; rewrite Z.pow_2_r; rewrite Z.mul_assoc; + rewrite <- Z.mul_add_distr_r. assert (((2 * wB - 4) + 2)*wB <= ([|wc|] * wB + [|cch|])*wB). - apply Zmult_le_compat;zarith. - rewrite Zmult_plus_distr_l in H3. + apply Z.mul_le_mono_nonneg;zarith. + rewrite Z.mul_add_distr_r in H3. intros. assert (U2 := spec_to_Z ccl);omega. generalize (spec_ww_add_c (w_W0 ccl) ll);destruct (ww_add_c (w_W0 ccl) ll) - as [l|l];unfold interp_carry;rewrite spec_w_W0;try rewrite Zmult_1_l; + as [l|l];unfold interp_carry;rewrite spec_w_W0;try rewrite Z.mul_1_l; simpl zn2z_to_Z; try rewrite spec_ww_add;try rewrite spec_ww_add_carry;rewrite spec_w_WW; 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. - repeat rewrite <- Zplus_assoc;rewrite H;apply mult_add_ineq2;zarith. + rewrite Z.add_assoc;rewrite Z.mul_add_distr_r. + rewrite Z.mul_1_l;rewrite <- Z.add_assoc;rewrite H4;ring. + repeat rewrite <- Z.add_assoc;rewrite H;apply mult_add_ineq2;zarith. Qed. Lemma spec_double_mul_c : forall cross:w->w->w->w->zn2z w -> zn2z w -> w*zn2z w, @@ -368,7 +361,7 @@ Section DoubleMul. forall x y, [||double_mul_c cross x y||] = [[x]] * [[y]]. Proof. intros cross Hcross x y;destruct x as [ |xh xl];simpl;trivial. - destruct y as [ |yh yl];simpl. rewrite Zmult_0_r;trivial. + destruct y as [ |yh yl];simpl. rewrite Z.mul_0_r;trivial. assert (H1:= spec_w_mul_c xh yh);assert (H2:= spec_w_mul_c xl yl). generalize (Hcross _ _ _ _ _ _ H1 H2). destruct (cross xh xl yh yl (w_mul_c xh yh) (w_mul_c xl yl)) as (wc,cc). @@ -389,7 +382,7 @@ Section DoubleMul. Lemma spec_w_2: [|w_2|] = 2. unfold w_2; rewrite spec_w_add; rewrite spec_w_1; simpl. apply Zmod_small; split; auto with zarith. - rewrite <- (Zpower_1_r 2); unfold base; apply Zpower_lt_monotone; auto with zarith. + rewrite <- (Z.pow_1_r 2); unfold base; apply Zpower_lt_monotone; auto with zarith. Qed. Lemma kara_prod_aux : forall xh xl yh yl, @@ -408,19 +401,19 @@ Section DoubleMul. assert (Hyh := (spec_to_Z yh)); assert (Hyl := (spec_to_Z yl)). generalize (spec_ww_add_c hh ll); case (ww_add_c hh ll); intros z Hz; rewrite <- Hz; unfold interp_carry; assert (Hz1 := (spec_ww_to_Z z)). - generalize (spec_w_compare xl xh); case (w_compare xl xh); intros Hxlh; + rewrite spec_w_compare; case Z.compare_spec; intros Hxlh; try rewrite Hxlh; try rewrite spec_w_0; try (ring; fail). - generalize (spec_w_compare yl yh); case (w_compare yl yh); intros Hylh. + rewrite spec_w_compare; case Z.compare_spec; intros Hylh. rewrite Hylh; rewrite spec_w_0; try (ring; fail). rewrite spec_w_0; try (ring; fail). repeat (rewrite spec_ww_sub || rewrite spec_w_sub || rewrite spec_w_mul_c). 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. - apply Zle_lt_trans with ([[z]]-0); auto with zarith. - unfold Zminus; apply Zplus_le_compat_l; apply Zle_left_rev; simpl; rewrite Zopp_involutive. - apply Zmult_le_0_compat; auto with zarith. + rewrite kara_prod_aux; apply Z.add_nonneg_nonneg; apply Z.mul_nonneg_nonneg; auto with zarith. + apply Z.le_lt_trans with ([[z]]-0); auto with zarith. + unfold Z.sub; apply Z.add_le_mono_l; apply Z.le_0_sub; simpl; rewrite Z.opp_involutive. + apply Z.mul_nonneg_nonneg; auto with zarith. 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_0; intros z1 Hz2 @@ -430,7 +423,7 @@ Section DoubleMul. rewrite spec_w_1; unfold interp_carry in Hz2; rewrite Hz2; repeat (rewrite spec_w_sub || rewrite spec_w_mul_c). repeat rewrite Zmod_small; auto with zarith; try (ring; fail). - generalize (spec_w_compare yl yh); case (w_compare yl yh); intros Hylh. + rewrite spec_w_compare; case Z.compare_spec; intros Hylh. rewrite Hylh; rewrite spec_w_0; 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_0; @@ -449,15 +442,15 @@ Section DoubleMul. replace ((x - y) * (z - t)) with ((y - x) * (t - z)); [idtac | ring] end. 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. - apply Zle_lt_trans with ([[z]]-0); auto with zarith. - unfold Zminus; apply Zplus_le_compat_l; apply Zle_left_rev; simpl; rewrite Zopp_involutive. - apply Zmult_le_0_compat; auto with zarith. + rewrite kara_prod_aux; apply Z.add_nonneg_nonneg; apply Z.mul_nonneg_nonneg; auto with zarith. + apply Z.le_lt_trans with ([[z]]-0); auto with zarith. + unfold Z.sub; apply Z.add_le_mono_l; apply Z.le_0_sub; simpl; rewrite Z.opp_involutive. + apply Z.mul_nonneg_nonneg; auto with zarith. (** there is a carry in hh + ll **) - rewrite Zmult_1_l. - generalize (spec_w_compare xl xh); case (w_compare xl xh); intros Hxlh; + rewrite Z.mul_1_l. + rewrite spec_w_compare; case Z.compare_spec; intros Hxlh; try rewrite Hxlh; try rewrite spec_w_1; try (ring; fail). - generalize (spec_w_compare yl yh); case (w_compare yl yh); intros Hylh; + rewrite spec_w_compare; case Z.compare_spec; intros Hylh; try rewrite Hylh; try rewrite spec_w_1; 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; @@ -465,7 +458,7 @@ Section DoubleMul. end. simpl in Hz2; rewrite Hz2; repeat (rewrite spec_w_sub || rewrite spec_w_mul_c). repeat rewrite Zmod_small; auto with zarith; try (ring; fail). - rewrite spec_w_0; rewrite Zmult_0_l; rewrite Zplus_0_l. + rewrite spec_w_0; rewrite Z.mul_0_l; rewrite Z.add_0_l. generalize Hz2; clear Hz2; unfold interp_carry. repeat (rewrite spec_w_sub || rewrite spec_w_mul_c). repeat rewrite Zmod_small; auto with zarith; try (ring; fail). @@ -476,11 +469,11 @@ Section DoubleMul. simpl in Hz2; rewrite Hz2; repeat (rewrite spec_w_sub || rewrite spec_w_mul_c). 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]])). + transitivity (wwB + (1 * wwB + [[z1]])). ring. rewrite Hz2; repeat (rewrite spec_w_sub || rewrite spec_w_mul_c). repeat rewrite Zmod_small; auto with zarith; try (ring; fail). - generalize (spec_w_compare yl yh); case (w_compare yl yh); intros Hylh; + rewrite spec_w_compare; case Z.compare_spec; intros Hylh; try rewrite Hylh; try rewrite spec_w_1; 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; @@ -489,7 +482,7 @@ Section DoubleMul. simpl in Hz2; rewrite Hz2; repeat (rewrite spec_w_sub || rewrite spec_w_mul_c). 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]])). + transitivity (wwB + (1 * wwB + [[z1]])). ring. rewrite Hz2; repeat (rewrite spec_w_sub || rewrite spec_w_mul_c). repeat rewrite Zmod_small; auto with zarith; try (ring; fail). @@ -499,7 +492,7 @@ Section DoubleMul. end. simpl in Hz2; rewrite Hz2; repeat (rewrite spec_w_sub || rewrite spec_w_mul_c). repeat rewrite Zmod_small; auto with zarith; try (ring; fail). - rewrite spec_w_0; rewrite Zmult_0_l; rewrite Zplus_0_l. + rewrite spec_w_0; rewrite Z.mul_0_l; rewrite Z.add_0_l. match goal with |- context[(?x - ?y) * (?z - ?t)] => replace ((x - y) * (z - t)) with ((y - x) * (t - z)); [idtac | ring] end. @@ -520,7 +513,7 @@ Section DoubleMul. rewrite <- wwB_wBwB;intros H1 H2. assert (H3 := wB_pos w_digits). assert (2*wB <= wwB). - rewrite wwB_wBwB; rewrite Zpower_2; apply Zmult_le_compat;zarith. + rewrite wwB_wBwB; rewrite Z.pow_2_r; apply Z.mul_le_mono_nonneg;zarith. omega. Qed. @@ -544,14 +537,14 @@ Section DoubleMul. 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_small; auto with zarith. + simpl; rewrite Z.mul_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 <- Zplus_mod; auto with zarith. - repeat (rewrite Zmult_plus_distr_l || rewrite Zmult_plus_distr_r). + repeat (rewrite Z.mul_add_distr_r || rewrite Z.mul_add_distr_l). rewrite <- Zmult_mod_distr_r; auto with zarith. - rewrite <- Zpower_2; rewrite <- wwB_wBwB; auto with zarith. + rewrite <- Z.pow_2_r; rewrite <- wwB_wBwB; auto with zarith. rewrite Zplus_mod; auto with zarith. rewrite Zmod_mod; auto with zarith. rewrite <- Zplus_mod; auto with zarith. @@ -571,10 +564,10 @@ Section DoubleMul. apply (spec_mul_aux xh xl xh xl wc cc);trivial. generalize Heq (spec_ww_add_c (w_mul_c xh xl) (w_mul_c xh xl));clear Heq. rewrite spec_w_mul_c;destruct (ww_add_c (w_mul_c xh xl) (w_mul_c xh xl)); - unfold interp_carry;try rewrite Zmult_1_l;intros Heq Heq';inversion Heq; - rewrite (Zmult_comm [|xl|]);subst. - rewrite spec_w_0;rewrite Zmult_0_l;rewrite Zplus_0_l;trivial. - rewrite spec_w_1;rewrite Zmult_1_l;rewrite <- wwB_wBwB;trivial. + unfold interp_carry;try rewrite Z.mul_1_l;intros Heq Heq';inversion Heq; + rewrite (Z.mul_comm [|xl|]);subst. + rewrite spec_w_0;rewrite Z.mul_0_l;rewrite Z.add_0_l;trivial. + rewrite spec_w_1;rewrite Z.mul_1_l;rewrite <- wwB_wBwB;trivial. Qed. Section DoubleMulAddn1Proof. @@ -596,8 +589,8 @@ Section DoubleMul. assert(H:=IHn xl y r);destruct (double_mul_add_n1 w_mul_add n xl y r)as(rl,l). assert(U:=IHn xh y rl);destruct(double_mul_add_n1 w_mul_add n xh y rl)as(rh,h). rewrite <- double_wB_wwB. rewrite spec_double_WW;simpl;trivial. - rewrite Zmult_plus_distr_l;rewrite <- Zplus_assoc;rewrite <- H. - rewrite Zmult_assoc;rewrite Zplus_assoc;rewrite <- Zmult_plus_distr_l. + rewrite Z.mul_add_distr_r;rewrite <- Z.add_assoc;rewrite <- H. + rewrite Z.mul_assoc;rewrite Z.add_assoc;rewrite <- Z.mul_add_distr_r. rewrite U;ring. Qed. @@ -611,9 +604,9 @@ Section DoubleMul. destruct (w_mul_c x y) as [ |h l];simpl;rewrite <- H. 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. + interp_carry in U;try rewrite Z.mul_1_l in H;simpl. rewrite U;ring. rewrite spec_w_succ. rewrite Zmod_small. - rewrite <- Zplus_assoc;rewrite <- U;ring. + rewrite <- Z.add_assoc;rewrite <- U;ring. simpl in H;assert (H1:= Zmult_lt_b _ _ _ (spec_to_Z x) (spec_to_Z y)). rewrite <- H in H1. assert (H2:=spec_to_Z h);split;zarith. diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v index 4394178f..40556c4a 100644 --- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v +++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <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 *) @@ -8,8 +8,6 @@ (* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) (************************************************************************) -(*i $Id: DoubleSqrt.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - Set Implicit Arguments. Require Import ZArith. @@ -220,12 +218,8 @@ Section DoubleSqrt. Variable spec_w_0W : forall l, [[w_0W l]] = [|l|]. Variable spec_w_is_even : forall x, if w_is_even x then [|x|] mod 2 = 0 else [|x|] mod 2 = 1. - Variable spec_w_compare : forall x y, - match w_compare x y with - | Eq => [|x|] = [|y|] - | Lt => [|x|] < [|y|] - | Gt => [|x|] > [|y|] - end. + Variable spec_w_compare : forall x y, + w_compare x y = Z.compare [|x|] [|y|]. Variable spec_w_sub : forall x y, [|w_sub x y|] = ([|x|] - [|y|]) mod wB. Variable spec_w_square_c : forall x, [[ w_square_c x]] = [|x|] * [|x|]. Variable spec_w_div21 : forall a1 a2 b, @@ -238,7 +232,7 @@ Section DoubleSqrt. [|p|] <= Zpos w_digits -> [| w_add_mul_div p x y |] = ([|x|] * (2 ^ [|p|]) + - [|y|] / (Zpower 2 ((Zpos w_digits) - [|p|]))) mod wB. + [|y|] / (Z.pow 2 ((Zpos w_digits) - [|p|]))) mod wB. Variable spec_ww_add_mul_div : forall x y p, [[p]] <= Zpos (xO w_digits) -> [[ ww_add_mul_div p x y ]] = @@ -257,11 +251,7 @@ Section DoubleSqrt. Variable spec_ww_pred : forall x, [[ww_pred x]] = ([[x]] - 1) mod wwB. Variable spec_ww_add_c : forall x y, [+[ww_add_c x y]] = [[x]] + [[y]]. Variable spec_ww_compare : forall x y, - match ww_compare x y with - | Eq => [[x]] = [[y]] - | Lt => [[x]] < [[y]] - | Gt => [[x]] > [[y]] - end. + ww_compare x y = Z.compare [[x]] [[y]]. Variable spec_ww_head0 : forall x, 0 < [[x]] -> wwB/ 2 <= 2 ^ [[ww_head0 x]] * [[x]] < wwB. Variable spec_low: forall x, [|low x|] = [[x]] mod wB. @@ -282,10 +272,9 @@ intros x; case x; simpl ww_is_even. unfold base. 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. + rewrite Z.add_0_l; rewrite Zmod_mod; auto with zarith. apply spec_w_is_even; auto with zarith. - apply Zdivide_mult_r; apply Zpower_divide; auto with zarith. - red; simpl; auto. + apply Z.divide_mul_r; apply Zpower_divide; auto with zarith. Qed. @@ -296,13 +285,10 @@ intros x; case x; simpl ww_is_even. intros a1 a2 b Hb; unfold w_div21c. assert (H: 0 < [|b|]); auto with zarith. assert (U := wB_pos w_digits). - apply Zlt_le_trans with (2 := Hb); auto with zarith. - apply Zlt_le_trans with 1; auto with zarith. + apply Z.lt_le_trans with (2 := Hb); auto with zarith. + apply Z.lt_le_trans with 1; auto with zarith. apply Zdiv_le_lower_bound; auto with zarith. - repeat match goal with |- context[w_compare ?y ?z] => - generalize (spec_w_compare y z); - case (w_compare y z) - end. + rewrite !spec_w_compare. repeat case Z.compare_spec. intros H1 H2; split. unfold interp_carry; autorewrite with w_rewrite rm10; auto with zarith. rewrite H1; rewrite H2; ring. @@ -321,7 +307,7 @@ intros x; case x; simpl ww_is_even. 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. + apply Z.lt_le_trans with (2 * (wB / 2)); auto with zarith. rewrite wB_div_2; auto. intros H1. match goal with |- context[w_div21 ?y ?z ?t] => @@ -334,7 +320,7 @@ intros x; case x; simpl ww_is_even. rewrite spec_w_sub; 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. + apply Z.lt_le_trans with (2 * (wB / 2)); auto with zarith. rewrite wB_div_2; auto. destruct (spec_to_Z a1);auto with zarith. destruct (spec_to_Z a1);auto with zarith. @@ -346,11 +332,11 @@ intros x; case x; simpl ww_is_even. intros w0 w1; replace [+|C1 w0|] with (wB + [|w0|]). rewrite Zmod_small; auto with zarith. intros (H3, H4); split; auto. - rewrite Zmult_plus_distr_l. - rewrite <- Zplus_assoc; rewrite <- H3; ring. + rewrite Z.mul_add_distr_r. + rewrite <- Z.add_assoc; rewrite <- H3; ring. split; auto with zarith. assert ([|a1|] < 2 * [|b|]); auto with zarith. - apply Zlt_le_trans with (2 * (wB / 2)); auto with zarith. + apply Z.lt_le_trans with (2 * (wB / 2)); auto with zarith. rewrite wB_div_2; auto. destruct (spec_to_Z a1);auto with zarith. destruct (spec_to_Z a1);auto with zarith. @@ -368,14 +354,14 @@ intros x; case x; simpl ww_is_even. rewrite spec_pred; rewrite spec_w_zdigits. rewrite Zmod_small; auto with zarith. split; auto with zarith. - apply Zlt_le_trans with (Zpos w_digits); auto with zarith. + apply Z.lt_le_trans with (Zpos w_digits); auto with zarith. unfold base; apply Zpower2_le_lin; auto with zarith. rewrite spec_w_add_mul_div; auto with zarith. autorewrite with w_rewrite rm10. match goal with |- context[?X - ?Y] => replace (X - Y) with 1 end. - rewrite Zpower_1_r; rewrite Zmod_small; auto with zarith. + rewrite Z.pow_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. @@ -390,15 +376,15 @@ intros x; case x; simpl ww_is_even. rewrite spec_pred; rewrite spec_w_zdigits. rewrite Zmod_small; auto with zarith. split; auto with zarith. - apply Zlt_le_trans with (Zpos w_digits); auto with zarith. + apply Z.lt_le_trans with (Zpos w_digits); auto with zarith. unfold base; apply Zpower2_le_lin; auto with zarith. autorewrite with w_rewrite rm10; auto with zarith. match goal with |- context[?X - ?Y] => replace (X - Y) with 1 end; rewrite Hp; try ring. - rewrite Zpos_minus; auto with zarith. - rewrite Zmax_right; auto with zarith. - rewrite Zpower_1_r; rewrite Zmod_small; auto with zarith. + rewrite Pos2Z.inj_sub_max; auto with zarith. + rewrite Z.max_r; auto with zarith. + rewrite Z.pow_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. @@ -406,14 +392,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_1_r; auto with zarith. + rewrite Zpower_exp; try rewrite Z.pow_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_1_r; rewrite <- Zpower_exp; + pattern 2 at 2; rewrite <- Z.pow_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. @@ -423,8 +409,8 @@ 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_1_r; auto with zarith. - rewrite Zmult_comm; auto. + rewrite Z.pow_1_r; auto with zarith. + rewrite Z.mul_comm; auto. Qed. Theorem ww_add_mult_mult_2: forall w, @@ -433,8 +419,8 @@ 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_1_r; auto with zarith. - rewrite Zmult_comm; auto. + rewrite Z.pow_1_r; auto with zarith. + rewrite Z.mul_comm; auto. rewrite spec_w_0W; rewrite spec_w_1; auto with zarith. red; simpl; intros; discriminate. Qed. @@ -445,18 +431,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_1_r; auto with zarith. + rewrite Z.pow_1_r; auto with zarith. f_equal; auto. - rewrite Zmult_comm; f_equal; auto. + rewrite Z.mul_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); + symmetry; apply Zdiv_unique with (r := 2 ^ (Zpos (ww_digits w_digits) - 1) -1); auto with zarith. unfold ww_digits; split; auto with zarith. match goal with |- 0 <= ?X - 1 => assert (0 < X); auto with zarith end. - apply Zpower_gt_0; auto with zarith. + apply Z.pow_pos_nonneg; auto with zarith. match goal with |- 0 <= ?X - 1 => assert (0 < X); auto with zarith; red; reflexivity end. @@ -466,7 +452,7 @@ intros x; case x; simpl ww_is_even. assert (tmp: forall p, p + p = 2 * p); auto with zarith; rewrite tmp; clear tmp. f_equal; auto. - pattern 2 at 2; rewrite <- Zpower_1_r; rewrite <- Zpower_exp; + pattern 2 at 2; rewrite <- Z.pow_1_r; rewrite <- Zpower_exp; auto with zarith. assert (tmp: forall p, 1 + (p - 1) = p); auto with zarith; rewrite tmp; clear tmp; auto. @@ -479,7 +465,7 @@ intros x; case x; simpl ww_is_even. 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. + rewrite Z_mod_same; try rewrite Z.add_0_r; auto with zarith. apply Zmod_mod; auto. Qed. @@ -494,8 +480,8 @@ intros x; case x; simpl ww_is_even. intros a1 a2 b H. assert (HH: 0 < [|b|]); auto with zarith. assert (U := wB_pos w_digits). - apply Zlt_le_trans with (2 := H); auto with zarith. - apply Zlt_le_trans with 1; auto with zarith. + apply Z.lt_le_trans with (2 := H); auto with zarith. + apply Z.lt_le_trans with 1; auto with zarith. apply Zdiv_le_lower_bound; auto with zarith. unfold w_div2s; case a1; intros w0 H0. match goal with |- context[w_div21c ?y ?z ?t] => @@ -541,10 +527,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_1_r; auto with zarith + try rewrite Z.pow_1_r; auto with zarith end. - rewrite Zpos_minus; auto with zarith. - rewrite Zmax_right; auto with zarith. + rewrite Pos2Z.inj_sub_max; auto with zarith. + rewrite Z.max_r; auto with zarith. ring. repeat rewrite C0_id. rewrite spec_w_add_c; auto with zarith. @@ -558,10 +544,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_1_r; auto with zarith + try rewrite Z.pow_1_r; auto with zarith end. - rewrite Zpos_minus; auto with zarith. - rewrite Zmax_right; auto with zarith. + rewrite Pos2Z.inj_sub_max; auto with zarith. + rewrite Z.max_r; auto with zarith. ring. repeat rewrite C1_plus_wB in H0. rewrite C1_plus_wB. @@ -583,7 +569,7 @@ intros x; case x; simpl ww_is_even. rewrite add_mult_div_2_plus_1. replace (wB + [|w0|]) with ([|b|] + ([|w0|] - [|b|] + wB)); auto with zarith. - rewrite Zmult_plus_distr_l; rewrite <- Zplus_assoc. + rewrite Z.mul_add_distr_r; rewrite <- Z.add_assoc. rewrite Hw1. pattern [|w2|] at 1; rewrite (Z_div_mod_eq [|w2|] 2); auto with zarith. @@ -591,10 +577,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_1_r; auto with zarith + try rewrite Z.pow_1_r; auto with zarith end. - rewrite Zpos_minus; auto with zarith. - rewrite Zmax_right; auto with zarith. + rewrite Pos2Z.inj_sub_max; auto with zarith. + rewrite Z.max_r; auto with zarith. ring. repeat rewrite C0_id. rewrite add_mult_div_2_plus_1. @@ -602,7 +588,7 @@ intros x; case x; simpl ww_is_even. intros H1; split; auto with zarith. replace (wB + [|w0|]) with ([|b|] + ([|w0|] - [|b|] + wB)); auto with zarith. - rewrite Zmult_plus_distr_l; rewrite <- Zplus_assoc. + rewrite Z.mul_add_distr_r; rewrite <- Z.add_assoc. rewrite Hw1. pattern [|w2|] at 1; rewrite (Z_div_mod_eq [|w2|] 2); auto with zarith. @@ -610,10 +596,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_1_r; auto with zarith + try rewrite Z.pow_1_r; auto with zarith end. - rewrite Zpos_minus; auto with zarith. - rewrite Zmax_right; auto with zarith. + rewrite Pos2Z.inj_sub_max; auto with zarith. + rewrite Z.max_r; auto with zarith. ring. split; auto with zarith. destruct (spec_to_Z b);auto with zarith. @@ -633,7 +619,7 @@ intros x; case x; simpl ww_is_even. rewrite add_mult_div_2. replace (wB + [|w0|]) with ([|b|] + ([|w0|] - [|b|] + wB)); auto with zarith. - rewrite Zmult_plus_distr_l; rewrite <- Zplus_assoc. + rewrite Z.mul_add_distr_r; rewrite <- Z.add_assoc. rewrite Hw1. pattern [|w2|] at 1; rewrite (Z_div_mod_eq [|w2|] 2); auto with zarith. @@ -644,7 +630,7 @@ intros x; case x; simpl ww_is_even. rewrite add_mult_div_2. replace (wB + [|w0|]) with ([|b|] + ([|w0|] - [|b|] + wB)); auto with zarith. - rewrite Zmult_plus_distr_l; rewrite <- Zplus_assoc. + rewrite Z.mul_add_distr_r; rewrite <- Z.add_assoc. rewrite Hw1. pattern [|w2|] at 1; rewrite (Z_div_mod_eq [|w2|] 2); auto with zarith. @@ -665,20 +651,20 @@ intros x; case x; simpl ww_is_even. rewrite <- Zpower_exp; auto with zarith. f_equal; auto with zarith. rewrite H. - rewrite (fun x => (Zmult_comm 4 (2 ^x))). + rewrite (fun x => (Z.mul_comm 4 (2 ^x))). rewrite Z_div_mult; auto with zarith. Qed. Theorem Zsquare_mult: forall p, p ^ 2 = p * p. intros p; change 2 with (1 + 1); rewrite Zpower_exp; - try rewrite Zpower_1_r; auto with zarith. + try rewrite Z.pow_1_r; auto with zarith. Qed. Theorem Zsquare_pos: forall p, 0 <= p ^ 2. - intros p; case (Zle_or_lt 0 p); intros H1. - rewrite Zsquare_mult; apply Zmult_le_0_compat; auto with zarith. + intros p; case (Z.le_gt_cases 0 p); intros H1. + rewrite Zsquare_mult; apply Z.mul_nonneg_nonneg; auto with zarith. rewrite Zsquare_mult; replace (p * p) with ((- p) * (- p)); try ring. - apply Zmult_le_0_compat; auto with zarith. + apply Z.mul_nonneg_nonneg; auto with zarith. Qed. Lemma spec_split: forall x, @@ -689,13 +675,12 @@ intros x; case x; simpl ww_is_even. Theorem mult_wwB: forall x y, [|x|] * [|y|] < wwB. Proof. - intros x y; rewrite wwB_wBwB; rewrite Zpower_2. + intros x y; rewrite wwB_wBwB; rewrite Z.pow_2_r. generalize (spec_to_Z x); intros U. generalize (spec_to_Z y); intros U1. - apply Zle_lt_trans with ((wB -1 ) * (wB - 1)); auto with zarith. - apply Zmult_le_compat; auto with zarith. - repeat (rewrite Zmult_minus_distr_r || rewrite Zmult_minus_distr_l); - auto with zarith. + apply Z.le_lt_trans with ((wB -1 ) * (wB - 1)); auto with zarith. + apply Z.mul_le_mono_nonneg; auto with zarith. + rewrite ?Z.mul_sub_distr_l, ?Z.mul_sub_distr_r; auto with zarith. Qed. Hint Resolve mult_wwB. @@ -710,22 +695,22 @@ intros x; case x; simpl ww_is_even. end; simpl fst; simpl snd. intros w0 w1 Hw0 w2 w3 Hw1. assert (U: wB/4 <= [|w2|]). - case (Zle_or_lt (wB / 4) [|w2|]); auto; intros H1. - contradict H; apply Zlt_not_le. - rewrite wwB_wBwB; rewrite Zpower_2. - pattern wB at 1; rewrite <- wB_div_4; rewrite <- Zmult_assoc; - rewrite Zmult_comm. + case (Z.le_gt_cases (wB / 4) [|w2|]); auto; intros H1. + contradict H; apply Z.lt_nge. + rewrite wwB_wBwB; rewrite Z.pow_2_r. + pattern wB at 1; rewrite <- wB_div_4; rewrite <- Z.mul_assoc; + rewrite Z.mul_comm. rewrite Z_div_mult; auto with zarith. rewrite <- Hw1. match goal with |- _ < ?X => - pattern X; rewrite <- Zplus_0_r; apply beta_lex_inv; + pattern X; rewrite <- Z.add_0_r; apply beta_lex_inv; auto with zarith end. destruct (spec_to_Z w3);auto with zarith. generalize (@spec_w_sqrt2 w2 w3 U); case (w_sqrt2 w2 w3). intros w4 c (H1, H2). assert (U1: wB/2 <= [|w4|]). - case (Zle_or_lt (wB/2) [|w4|]); auto with zarith. + case (Z.le_gt_cases (wB/2) [|w4|]); auto with zarith. intros U1. assert (U2 : [|w4|] <= wB/2 -1); auto with zarith. assert (U3 : [|w4|] ^ 2 <= wB/4 * wB - wB + 1); auto with zarith. @@ -733,19 +718,19 @@ intros x; case x; simpl ww_is_even. rewrite Zsquare_mult; replace Y with ((wB/2 - 1) * (wB/2 -1)) end. - apply Zmult_le_compat; auto with zarith. + apply Z.mul_le_mono_nonneg; auto with zarith. destruct (spec_to_Z w4);auto with zarith. destruct (spec_to_Z w4);auto with zarith. pattern wB at 4 5; rewrite <- wB_div_2. - rewrite Zmult_assoc. + rewrite Z.mul_assoc. replace ((wB / 4) * 2) with (wB / 2). ring. pattern wB at 1; rewrite <- wB_div_4. change 4 with (2 * 2). - rewrite <- Zmult_assoc; rewrite (Zmult_comm 2). + rewrite <- Z.mul_assoc; rewrite (Z.mul_comm 2). rewrite Z_div_mult; try ring; auto with zarith. assert (U4 : [+|c|] <= wB -2); auto with zarith. - apply Zle_trans with (1 := H2). + apply Z.le_trans with (1 := H2). match goal with |- ?X <= ?Y => replace Y with (2 * (wB/ 2 - 1)); auto with zarith end. @@ -754,10 +739,10 @@ intros x; case x; simpl ww_is_even. assert (U5: X < wB / 4 * wB) end. rewrite H1; auto with zarith. - contradict U; apply Zlt_not_le. - apply Zmult_lt_reg_r with wB; auto with zarith. + contradict U; apply Z.lt_nge. + apply Z.mul_lt_mono_pos_r with wB; auto with zarith. destruct (spec_to_Z w4);auto with zarith. - apply Zle_lt_trans with (2 := U5). + apply Z.le_lt_trans with (2 := U5). unfold ww_to_Z, zn2z_to_Z. destruct (spec_to_Z w3);auto with zarith. generalize (@spec_w_div2s c w0 w4 U1 H2). @@ -779,7 +764,7 @@ intros x; case x; simpl ww_is_even. unfold ww_to_Z, zn2z_to_Z in H1; rewrite H1. rewrite <- Hw0. match goal with |- (?X ^2 + ?Y) * wwB + (?Z * wB + ?T) = ?U => - apply trans_equal with ((X * wB) ^ 2 + (Y * wB + Z) * wB + T) + transitivity ((X * wB) ^ 2 + (Y * wB + Z) * wB + T) end. repeat rewrite Zsquare_mult. rewrite wwB_wBwB; ring. @@ -792,17 +777,17 @@ intros x; case x; simpl ww_is_even. match goal with |- ?X - ?Y * ?Y <= _ => assert (V := Zsquare_pos Y); rewrite Zsquare_mult in V; - apply Zle_trans with X; auto with zarith; + apply Z.le_trans with X; auto with zarith; clear V end. match goal with |- ?X * wB + ?Y <= 2 * (?Z * wB + ?T) => - apply Zle_trans with ((2 * Z - 1) * wB + wB); auto with zarith + apply Z.le_trans with ((2 * Z - 1) * wB + wB); auto with zarith end. destruct (spec_to_Z w1);auto with zarith. match goal with |- ?X <= _ => replace X with (2 * [|w4|] * wB); auto with zarith end. - rewrite Zmult_plus_distr_r; rewrite Zmult_assoc. + rewrite Z.mul_add_distr_l; rewrite Z.mul_assoc. destruct (spec_to_Z w5); auto with zarith. ring. intros z; replace [-[C1 z]] with (- wwB + [[z]]). @@ -828,7 +813,7 @@ intros x; case x; simpl ww_is_even. unfold ww_to_Z, zn2z_to_Z in H1; rewrite H1. rewrite <- Hw0. match goal with |- (?X ^2 + ?Y) * wwB + (?Z * wB + ?T) = ?U => - apply trans_equal with ((X * wB) ^ 2 + (Y * wB + Z) * wB + T) + transitivity ((X * wB) ^ 2 + (Y * wB + Z) * wB + T) end. repeat rewrite Zsquare_mult. rewrite wwB_wBwB; ring. @@ -841,11 +826,11 @@ intros x; case x; simpl ww_is_even. destruct (spec_ww_to_Z w_digits w_to_Z spec_to_Z z);auto with zarith. assert (V1 := spec_ww_to_Z w_digits w_to_Z spec_to_Z (WW w4 w5)). assert (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. - apply Zmult_lt_reg_r with 2; auto with zarith. + apply Z.lt_le_trans with (wB/ 2 * wB + 0); auto with zarith. + autorewrite with rm10; apply Z.mul_pos_pos; auto with zarith. + apply Z.mul_lt_mono_pos_r with 2; auto with zarith. autorewrite with rm10. - rewrite Zmult_comm; rewrite wB_div_2; auto with zarith. + rewrite Z.mul_comm; rewrite wB_div_2; auto with zarith. case (spec_to_Z w5);auto with zarith. case (spec_to_Z w5);auto with zarith. simpl. @@ -853,11 +838,11 @@ intros x; case x; simpl ww_is_even. assert (V1 := spec_ww_to_Z w_digits w_to_Z spec_to_Z (WW w4 w5)); auto with zarith. split; auto with zarith. assert (wwB <= 2 * [[WW w4 w5]]); auto with zarith. - apply Zle_trans with (2 * ([|w4|] * wB)). - rewrite wwB_wBwB; rewrite Zpower_2. - rewrite Zmult_assoc; apply Zmult_le_compat_r; auto with zarith. - rewrite <- wB_div_2; auto with zarith. + apply Z.le_trans with (2 * ([|w4|] * wB)). + rewrite wwB_wBwB; rewrite Z.pow_2_r. + rewrite Z.mul_assoc; apply Z.mul_le_mono_nonneg_r; auto with zarith. assert (V2 := spec_to_Z w5);auto with zarith. + rewrite <- wB_div_2; auto with zarith. simpl ww_to_Z; assert (V2 := spec_to_Z w5);auto with zarith. assert (V1 := spec_ww_to_Z w_digits w_to_Z spec_to_Z (WW w4 w5)); auto with zarith. intros z1; change [-[C1 z1]] with (-wwB + [[z1]]). @@ -869,21 +854,21 @@ intros x; case x; simpl ww_is_even. rewrite ww_add_mult_mult_2. 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. - apply Zmult_lt_reg_r with 2; auto with zarith. + apply Z.lt_le_trans with (wB/ 2 * wB + 0); auto with zarith. + autorewrite with rm10; apply Z.mul_pos_pos; auto with zarith. + apply Z.mul_lt_mono_pos_r with 2; auto with zarith. autorewrite with rm10. - rewrite Zmult_comm; rewrite wB_div_2; auto with zarith. + rewrite Z.mul_comm; rewrite wB_div_2; auto with zarith. assert (VV3 := spec_to_Z w5);auto with zarith. assert (VV3 := spec_to_Z w5);auto with zarith. simpl. assert (VV3 := spec_to_Z w5);auto with zarith. assert (VV3: wwB <= 2 * [[WW w4 w5]]); auto with zarith. - apply Zle_trans with (2 * ([|w4|] * wB)). - rewrite wwB_wBwB; rewrite Zpower_2. - rewrite Zmult_assoc; apply Zmult_le_compat_r; auto with zarith. - rewrite <- wB_div_2; auto with zarith. + apply Z.le_trans with (2 * ([|w4|] * wB)). + rewrite wwB_wBwB; rewrite Z.pow_2_r. + rewrite Z.mul_assoc; apply Z.mul_le_mono_nonneg_r; auto with zarith. case (spec_to_Z w5);auto with zarith. + rewrite <- wB_div_2; auto with zarith. 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. @@ -905,7 +890,7 @@ intros x; case x; simpl ww_is_even. rewrite <- Hw0. split. match goal with |- (?X ^2 + ?Y) * wwB + (?Z * wB + ?T) = ?U => - apply trans_equal with ((X * wB) ^ 2 + (Y * wB + Z) * wB + T) + transitivity ((X * wB) ^ 2 + (Y * wB + Z) * wB + T) end. repeat rewrite Zsquare_mult. rewrite wwB_wBwB; ring. @@ -918,17 +903,17 @@ intros x; case x; simpl ww_is_even. assert (V2 := spec_ww_to_Z w_digits w_to_Z spec_to_Z z);auto with zarith. assert (V3 := spec_ww_to_Z w_digits w_to_Z spec_to_Z z1);auto with zarith. split; auto with zarith. - rewrite (Zplus_comm (-wwB)); rewrite <- Zplus_assoc. + rewrite (Z.add_comm (-wwB)); rewrite <- Z.add_assoc. rewrite H5. match goal with |- 0 <= ?X + (?Y - ?Z) => - apply Zle_trans with (X - Z); auto with zarith + apply Z.le_trans with (X - Z); auto with zarith end. 2: generalize (spec_ww_to_Z w_digits w_to_Z spec_to_Z (WW w6 w1)); unfold ww_to_Z; auto with zarith. rewrite V1. match goal with |- 0 <= ?X - 1 - ?Y => assert (Y < X); auto with zarith end. - apply Zlt_le_trans with wwB; auto with zarith. + apply Z.lt_le_trans with wwB; auto with zarith. intros (H3, H4). match goal with |- context [ww_sub_c ?y ?z] => generalize (spec_ww_sub_c y z); case (ww_sub_c y z) @@ -946,7 +931,7 @@ intros x; case x; simpl ww_is_even. unfold ww_to_Z, zn2z_to_Z in H1; rewrite H1. rewrite <- Hw0. match goal with |- (?X ^2 + ?Y) * wwB + (?Z * wB + ?T) = ?U => - apply trans_equal with ((X * wB) ^ 2 + (Y * wB + Z) * wB + T) + transitivity ((X * wB) ^ 2 + (Y * wB + Z) * wB + T) end. repeat rewrite Zsquare_mult. rewrite wwB_wBwB; ring. @@ -958,27 +943,27 @@ intros x; case x; simpl ww_is_even. simpl ww_to_Z. rewrite H5. simpl ww_to_Z. - rewrite wwB_wBwB; rewrite Zpower_2. + rewrite wwB_wBwB; rewrite Z.pow_2_r. match goal with |- ?X * ?Y + (?Z * ?Y + ?T - ?U) <= _ => - apply Zle_trans with (X * Y + (Z * Y + T - 0)); + apply Z.le_trans with (X * Y + (Z * Y + T - 0)); auto with zarith end. assert (V := Zsquare_pos [|w5|]); rewrite Zsquare_mult in V; auto with zarith. autorewrite with rm10. match goal with |- _ <= 2 * (?U * ?V + ?W) => - apply Zle_trans with (2 * U * V + 0); + apply Z.le_trans with (2 * U * V + 0); auto with zarith end. match goal with |- ?X * ?Y + (?Z * ?Y + ?T) <= _ => replace (X * Y + (Z * Y + T)) with ((X + Z) * Y + T); try ring end. - apply Zlt_le_weak; apply beta_lex_inv; auto with zarith. + apply Z.lt_le_incl; apply beta_lex_inv; auto with zarith. destruct (spec_to_Z w1);auto with zarith. destruct (spec_to_Z w5);auto with zarith. - rewrite Zmult_plus_distr_r; auto with zarith. - rewrite Zmult_assoc; auto with zarith. + rewrite Z.mul_add_distr_l; auto with zarith. + rewrite Z.mul_assoc; auto with zarith. intros z; replace [-[C1 z]] with (- wwB + [[z]]). 2: simpl; case wwB; auto with zarith. intros H5; rewrite spec_w_square_c in H5; @@ -997,7 +982,7 @@ intros x; case x; simpl ww_is_even. rewrite <- Hw0. split. match goal with |- (?X ^2 + ?Y) * wwB + (?Z * wB + ?T) = ?U => - apply trans_equal with ((X * wB) ^ 2 + (Y * wB + Z) * wB + T) + transitivity ((X * wB) ^ 2 + (Y * wB + Z) * wB + T) end. repeat rewrite Zsquare_mult. rewrite wwB_wBwB; ring. @@ -1008,40 +993,38 @@ intros x; case x; simpl ww_is_even. repeat rewrite Zsquare_mult; ring. rewrite V. simpl ww_to_Z. - rewrite wwB_wBwB; rewrite Zpower_2. + rewrite wwB_wBwB; rewrite Z.pow_2_r. match goal with |- (?Z * ?Y + ?T - ?U) + ?X * ?Y <= _ => - apply Zle_trans with ((Z * Y + T - 0) + X * Y); + apply Z.le_trans with ((Z * Y + T - 0) + X * Y); auto with zarith end. assert (V1 := Zsquare_pos [|w5|]); rewrite Zsquare_mult in V1; auto with zarith. autorewrite with rm10. match goal with |- _ <= 2 * (?U * ?V + ?W) => - apply Zle_trans with (2 * U * V + 0); + apply Z.le_trans with (2 * U * V + 0); auto with zarith end. match goal with |- (?Z * ?Y + ?T) + ?X * ?Y <= _ => replace ((Z * Y + T) + X * Y) with ((X + Z) * Y + T); try ring end. - apply Zlt_le_weak; apply beta_lex_inv; auto with zarith. + apply Z.lt_le_incl; apply beta_lex_inv; auto with zarith. destruct (spec_to_Z w1);auto with zarith. destruct (spec_to_Z w5);auto with zarith. - rewrite Zmult_plus_distr_r; auto with zarith. - rewrite Zmult_assoc; auto with zarith. - case Zle_lt_or_eq with (1 := H2); clear H2; intros H2. + rewrite Z.mul_add_distr_l; auto with zarith. + rewrite Z.mul_assoc; auto with zarith. + Z.le_elim H2. intros c1 (H3, H4). - match type of H3 with ?X = ?Y => - absurd (X < Y) - end. - apply Zle_not_lt; rewrite <- H3; auto with zarith. - rewrite Zmult_plus_distr_l. - apply Zlt_le_trans with ((2 * [|w4|]) * wB + 0); + match type of H3 with ?X = ?Y => absurd (X < Y) end. + apply Z.le_ngt; rewrite <- H3; auto with zarith. + rewrite Z.mul_add_distr_r. + apply Z.lt_le_trans with ((2 * [|w4|]) * wB + 0); auto with zarith. apply beta_lex_inv; auto with zarith. destruct (spec_to_Z w0);auto with zarith. assert (V1 := spec_to_Z w5);auto with zarith. - rewrite (Zmult_comm wB); auto with zarith. + rewrite (Z.mul_comm wB); auto with zarith. assert (0 <= [|w5|] * (2 * [|w4|])); auto with zarith. intros c1 (H3, H4); rewrite H2 in H3. match type of H3 with ?X + ?Y = (?Z + ?T) * ?U + ?V => @@ -1051,20 +1034,19 @@ intros x; case x; simpl ww_is_even. end. assert (V1 := spec_to_Z w0);auto with zarith. assert (V2 := spec_to_Z w5);auto with zarith. - case (Zle_lt_or_eq 0 [|w5|]); auto with zarith; intros V3. - match type of VV with ?X = ?Y => - absurd (X < Y) - end. - apply Zle_not_lt; rewrite <- VV; auto with zarith. - apply Zlt_le_trans with wB; auto with zarith. + case V2; intros V3 _. + Z.le_elim V3; auto with zarith. + match type of VV with ?X = ?Y => absurd (X < Y) end. + apply Z.le_ngt; rewrite <- VV; auto with zarith. + apply Z.lt_le_trans with wB; auto with zarith. match goal with |- _ <= ?X + _ => - apply Zle_trans with X; auto with zarith + apply Z.le_trans with X; auto with zarith end. match goal with |- _ <= _ * ?X => - apply Zle_trans with (1 * X); auto with zarith + apply Z.le_trans with (1 * X); auto with zarith end. autorewrite with rm10. - rewrite <- wB_div_2; apply Zmult_le_compat_l; auto with zarith. + rewrite <- wB_div_2; apply Z.mul_le_mono_nonneg_l; auto with zarith. rewrite <- V3 in VV; generalize VV; autorewrite with rm10; clear VV; intros VV. rewrite spec_ww_add_c; auto with zarith. @@ -1080,7 +1062,7 @@ intros x; case x; simpl ww_is_even. simpl ww_to_Z in H1; rewrite H1. rewrite <- Hw0. match goal with |- (?X ^2 + ?Y) * wwB + (?Z * wB + ?T) = ?U => - apply trans_equal with ((X * wB) ^ 2 + (Y * wB + Z) * wB + T) + transitivity ((X * wB) ^ 2 + (Y * wB + Z) * wB + T) end. repeat rewrite Zsquare_mult. rewrite wwB_wBwB; ring. @@ -1092,41 +1074,41 @@ intros x; case x; simpl ww_is_even. simpl ww_to_Z; unfold ww_to_Z. rewrite spec_w_Bm1; auto with zarith. split. - rewrite wwB_wBwB; rewrite Zpower_2. + rewrite wwB_wBwB; rewrite Z.pow_2_r. match goal with |- _ <= -?X + (2 * (?Z * ?T + ?U) + ?V) => assert (X <= 2 * Z * T); auto with zarith end. - apply Zmult_le_compat_r; auto with zarith. - rewrite <- wB_div_2; apply Zmult_le_compat_l; auto with zarith. - rewrite Zmult_plus_distr_r; auto with zarith. - rewrite Zmult_assoc; auto with zarith. + apply Z.mul_le_mono_nonneg_r; auto with zarith. + rewrite <- wB_div_2; apply Z.mul_le_mono_nonneg_l; auto with zarith. + rewrite Z.mul_add_distr_l; auto with zarith. + rewrite Z.mul_assoc; auto with zarith. match goal with |- _ + ?X < _ => replace X with ((2 * (([|w4|]) + 1) * wB) - 1); try ring end. assert (2 * ([|w4|] + 1) * wB <= 2 * wwB); auto with zarith. - rewrite <- Zmult_assoc; apply Zmult_le_compat_l; auto with zarith. - rewrite wwB_wBwB; rewrite Zpower_2. - apply Zmult_le_compat_r; auto with zarith. + rewrite <- Z.mul_assoc; apply Z.mul_le_mono_nonneg_l; auto with zarith. + rewrite wwB_wBwB; rewrite Z.pow_2_r. + apply Z.mul_le_mono_nonneg_r; auto with zarith. case (spec_to_Z w4);auto with zarith. - Qed. +Qed. Lemma spec_ww_is_zero: forall x, if ww_is_zero x then [[x]] = 0 else 0 < [[x]]. intro x; unfold ww_is_zero. - generalize (spec_ww_compare W0 x); case (ww_compare W0 x); + rewrite spec_ww_compare. case Z.compare_spec; auto with zarith. simpl ww_to_Z. assert (V4 := spec_ww_to_Z w_digits w_to_Z spec_to_Z x);auto with zarith. Qed. Lemma wwB_4_2: 2 * (wwB / 4) = wwB/ 2. - pattern wwB at 1; rewrite wwB_wBwB; rewrite Zpower_2. + pattern wwB at 1; rewrite wwB_wBwB; rewrite Z.pow_2_r. rewrite <- wB_div_2. match goal with |- context[(2 * ?X) * (2 * ?Z)] => replace ((2 * X) * (2 * Z)) with ((X * Z) * 4); try ring end. rewrite Z_div_mult; auto with zarith. - rewrite Zmult_assoc; rewrite wB_div_2. + rewrite Z.mul_assoc; rewrite wB_div_2. rewrite wwB_div_2; ring. Qed. @@ -1142,10 +1124,10 @@ intros x; case x; simpl ww_is_even. intros H2. generalize (spec_ww_head0 x H2); case (ww_head0 x); autorewrite with rm10. intros (H3, H4); split; auto with zarith. - apply Zle_trans with (2 := H3). + apply Z.le_trans with (2 := H3). apply Zdiv_le_compat_l; auto with zarith. intros xh xl (H3, H4); split; auto with zarith. - apply Zle_trans with (2 := H3). + apply Z.le_trans with (2 := H3). apply Zdiv_le_compat_l; auto with zarith. intros H1. case (spec_to_w_Z (ww_head0 x)); intros Hv1 Hv2. @@ -1169,24 +1151,24 @@ intros x; case x; simpl ww_is_even. 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_1_r. + pattern 2 at 1; rewrite <- Z.pow_1_r. rewrite <- Zpower_exp; auto with zarith. ring_simplify (1 + (u - 1)); auto with zarith. split; auto with zarith. - apply Zmult_le_reg_r with 2; auto with zarith. - repeat rewrite (fun x => Zmult_comm x 2). + apply Z.mul_le_mono_pos_r with 2; auto with zarith. + repeat rewrite (fun x => Z.mul_comm x 2). rewrite wwB_4_2. - rewrite Zmult_assoc; rewrite Hu; auto with zarith. - apply Zle_lt_trans with (2 * 2 ^ ([[ww_head0 x]] - 1) * [[x]]); auto with zarith; + rewrite Z.mul_assoc; rewrite Hu; auto with zarith. + apply Z.le_lt_trans with (2 * 2 ^ ([[ww_head0 x]] - 1) * [[x]]); auto with zarith; rewrite Hu; auto with zarith. - apply Zmult_le_compat_r; auto with zarith. + apply Z.mul_le_mono_nonneg_r; auto with zarith. apply Zpower_le_monotone; auto with zarith. Qed. Theorem wwB_4_wB_4: wwB / 4 = wB / 4 * wB. - apply sym_equal; apply Zdiv_unique with 0; - auto with zarith. - rewrite Zmult_assoc; rewrite wB_div_4; auto with zarith. + Proof. + symmetry; apply Zdiv_unique with 0; auto with zarith. + rewrite Z.mul_assoc; rewrite wB_div_4; auto with zarith. rewrite wwB_wBwB; ring. Qed. @@ -1195,10 +1177,10 @@ intros x; case x; simpl ww_is_even. assert (U := wB_pos w_digits). intro x; unfold ww_sqrt. generalize (spec_ww_is_zero x); case (ww_is_zero x). - simpl ww_to_Z; simpl Zpower; unfold Zpower_pos; simpl; + simpl ww_to_Z; simpl Z.pow; unfold Z.pow_pos; simpl; auto with zarith. intros H1. - generalize (spec_ww_compare (ww_head1 x) W0); case ww_compare; + rewrite spec_ww_compare. case Z.compare_spec; simpl ww_to_Z; autorewrite with rm10. generalize H1; case x. intros HH; contradict HH; simpl ww_to_Z; auto with zarith. @@ -1216,7 +1198,7 @@ intros x; case x; simpl ww_is_even. intros w3 (H6, H7); rewrite H6. assert (V1 := spec_to_Z w3);auto with zarith. split; auto with zarith. - apply Zle_lt_trans with ([|w2|] ^2 + 2 * [|w2|]); auto with zarith. + apply Z.le_lt_trans with ([|w2|] ^2 + 2 * [|w2|]); auto with zarith. match goal with |- ?X < ?Z => replace Z with (X + 1); auto with zarith end. @@ -1224,7 +1206,7 @@ intros x; case x; simpl ww_is_even. intros w3 (H6, H7); rewrite H6. assert (V1 := spec_to_Z w3);auto with zarith. split; auto with zarith. - apply Zle_lt_trans with ([|w2|] ^2 + 2 * [|w2|]); auto with zarith. + apply Z.le_lt_trans with ([|w2|] ^2 + 2 * [|w2|]); auto with zarith. match goal with |- ?X < ?Z => replace Z with (X + 1); auto with zarith end. @@ -1234,42 +1216,42 @@ intros x; case x; simpl ww_is_even. case (spec_ww_head1 x); intros Hp1 Hp2. generalize (Hp2 H1); clear Hp2; intros Hp2. assert (Hv2: [[ww_head1 x]] <= Zpos (xO w_digits)). - case (Zle_or_lt (Zpos (xO w_digits)) [[ww_head1 x]]); auto with zarith; intros HH1. + case (Z.le_gt_cases (Zpos (xO w_digits)) [[ww_head1 x]]); auto with zarith; intros HH1. case Hp2; intros _ HH2; contradict HH2. - apply Zle_not_lt; unfold base. - apply Zle_trans with (2 ^ [[ww_head1 x]]). + apply Z.le_ngt; unfold base. + apply Z.le_trans with (2 ^ [[ww_head1 x]]). apply Zpower_le_monotone; auto with zarith. pattern (2 ^ [[ww_head1 x]]) at 1; - rewrite <- (Zmult_1_r (2 ^ [[ww_head1 x]])). - apply Zmult_le_compat_l; auto with zarith. + rewrite <- (Z.mul_1_r (2 ^ [[ww_head1 x]])). + apply Z.mul_le_mono_nonneg_l; auto with zarith. 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_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. + intros H2. symmetry in H2. rewrite Z.mul_eq_0 in H2. destruct H2 as [H2|H2]. + rewrite H2; unfold Z.pow, Z.pow_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_gt_0; auto with zarith. + apply Z.pow_pos_nonneg; auto with zarith. split; auto with zarith. - case Hp2; intros _ tmp; apply Zle_lt_trans with (2 := tmp); + case Hp2; intros _ tmp; apply Z.le_lt_trans with (2 := tmp); clear tmp. - rewrite Zmult_comm; apply Zmult_le_compat_r; auto with zarith. + rewrite Z.mul_comm; apply Z.mul_le_mono_nonneg_r; auto with zarith. assert (Hv0: [[ww_head1 x]] = 2 * ([[ww_head1 x]]/2)). pattern [[ww_head1 x]] at 1; rewrite (Z_div_mod_eq [[ww_head1 x]] 2); auto with zarith. generalize (spec_ww_is_even (ww_head1 x)); rewrite Hp1; - intros tmp; rewrite tmp; rewrite Zplus_0_r; auto. + intros tmp; rewrite tmp; rewrite Z.add_0_r; auto. intros w0 w1; autorewrite with w_rewrite rm10. rewrite Zmod_small; auto with zarith. - 2: rewrite Zmult_comm; auto with zarith. + 2: rewrite Z.mul_comm; auto with zarith. intros H2. assert (V: wB/4 <= [|w0|]). apply beta_lex with 0 [|w1|] wB; auto with zarith; autorewrite with rm10. simpl ww_to_Z in H2; rewrite H2. rewrite <- wwB_4_wB_4; auto with zarith. - rewrite Zmult_comm; auto with zarith. + rewrite Z.mul_comm; auto with zarith. assert (V1 := spec_to_Z w1);auto with zarith. generalize (@spec_w_sqrt2 w0 w1 V);auto with zarith. case (w_sqrt2 w0 w1); intros w2 c. @@ -1280,13 +1262,13 @@ intros x; case x; simpl ww_is_even. rewrite spec_ww_pred; rewrite spec_ww_zdigits. rewrite Zmod_small; auto with zarith. split; auto with zarith. - apply Zlt_le_trans with (Zpos (xO w_digits)); auto with zarith. + apply Z.lt_le_trans with (Zpos (xO w_digits)); auto with zarith. unfold base; apply Zpower2_le_lin; auto with zarith. assert (Hv4: [[ww_head1 x]]/2 < wB). - apply Zle_lt_trans with (Zpos w_digits). - apply Zmult_le_reg_r with 2; auto with zarith. - repeat rewrite (fun x => Zmult_comm x 2). - rewrite <- Hv0; rewrite <- Zpos_xO; auto. + apply Z.le_lt_trans with (Zpos w_digits). + apply Z.mul_le_mono_pos_r with 2; auto with zarith. + repeat rewrite (fun x => Z.mul_comm x 2). + rewrite <- Hv0; rewrite <- Pos2Z.inj_xO; auto. unfold base; apply Zpower2_lt_lin; auto with zarith. assert (Hv5: [[(ww_add_mul_div (ww_pred ww_zdigits) W0 (ww_head1 x))]] = [[ww_head1 x]]/2). @@ -1294,12 +1276,12 @@ 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_1_r. + rewrite Z.pow_1_r. rewrite Zmod_small; auto with zarith. split; auto with zarith. - apply Zlt_le_trans with (1 := Hv4); auto with zarith. + apply Z.lt_le_trans with (1 := Hv4); auto with zarith. unfold base; apply Zpower_le_monotone; auto with zarith. - split; unfold ww_digits; try rewrite Zpos_xO; auto with zarith. + split; unfold ww_digits; try rewrite Pos2Z.inj_xO; auto with zarith. rewrite Hv3; auto with zarith. assert (Hv6: [|low(ww_add_mul_div (ww_pred ww_zdigits) W0 (ww_head1 x))|] = [[ww_head1 x]]/2). @@ -1315,13 +1297,13 @@ intros x; case x; simpl ww_is_even. 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. + apply Z.mul_le_mono_pos_r with (2 ^ [[ww_head1 x]]); auto with zarith. rewrite H4. - apply Zle_trans with ([|w2|] ^ 2); auto with zarith. - rewrite Zmult_comm. + apply Z.le_trans with ([|w2|] ^ 2); auto with zarith. + rewrite Z.mul_comm. pattern [[ww_head1 x]] at 1; rewrite Hv0; auto with zarith. - rewrite (Zmult_comm 2); rewrite Zpower_mult; + rewrite (Z.mul_comm 2); rewrite Z.pow_mul_r; auto with zarith. assert (tmp: forall p q, p ^ 2 * q ^ 2 = (p * q) ^2); try (intros; repeat rewrite Zsquare_mult; ring); @@ -1337,17 +1319,17 @@ intros x; case x; simpl ww_is_even. case (Z_mod_lt [|w2|] (2 ^ ([[ww_head1 x]] / 2))); auto with zarith. case c; unfold interp_carry; autorewrite with rm10; intros w3; assert (V3 := spec_to_Z w3);auto with zarith. - apply Zmult_lt_reg_r with (2 ^ [[ww_head1 x]]); auto with zarith. + apply Z.mul_lt_mono_pos_r with (2 ^ [[ww_head1 x]]); auto with zarith. rewrite H4. - apply Zle_lt_trans with ([|w2|] ^ 2 + 2 * [|w2|]); auto with zarith. - apply Zlt_le_trans with (([|w2|] + 1) ^ 2); auto with zarith. + apply Z.le_lt_trans with ([|w2|] ^ 2 + 2 * [|w2|]); auto with zarith. + apply Z.lt_le_trans with (([|w2|] + 1) ^ 2); auto with zarith. match goal with |- ?X < ?Y => replace Y with (X + 1); auto with zarith end. repeat rewrite (Zsquare_mult); ring. - rewrite Zmult_comm. + rewrite Z.mul_comm. pattern [[ww_head1 x]] at 1; rewrite Hv0. - rewrite (Zmult_comm 2); rewrite Zpower_mult; + rewrite (Z.mul_comm 2); rewrite Z.pow_mul_r; auto with zarith. assert (tmp: forall p q, p ^ 2 * q ^ 2 = (p * q) ^2); try (intros; repeat rewrite Zsquare_mult; ring); @@ -1356,20 +1338,20 @@ intros x; case x; simpl ww_is_even. split; auto with zarith. pattern [|w2|] at 1; rewrite (Z_div_mod_eq [|w2|] (2 ^ ([[ww_head1 x]]/2))); auto with zarith. - rewrite <- Zplus_assoc; rewrite Zmult_plus_distr_r. - autorewrite with rm10; apply Zplus_le_compat_l; auto with zarith. + rewrite <- Z.add_assoc; rewrite Z.mul_add_distr_l. + autorewrite with rm10; apply Z.add_le_mono_l; auto with zarith. case (Z_mod_lt [|w2|] (2 ^ ([[ww_head1 x]]/2))); auto with zarith. split; auto with zarith. - apply Zle_lt_trans with ([|w2|]); auto with zarith. + apply Z.le_lt_trans with ([|w2|]); auto with zarith. apply Zdiv_le_upper_bound; auto with zarith. pattern [|w2|] at 1; replace [|w2|] with ([|w2|] * 2 ^0); auto with zarith. - apply Zmult_le_compat_l; auto with zarith. + apply Z.mul_le_mono_nonneg_l; auto with zarith. apply Zpower_le_monotone; auto with zarith. - rewrite Zpower_0_r; autorewrite with rm10; auto. + rewrite Z.pow_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. + rewrite Hv0 in Hv2; rewrite (Pos2Z.inj_xO w_digits) in Hv2; auto with zarith. + apply Z.le_lt_trans with (Zpos w_digits); auto with zarith. unfold base; apply Zpower2_lt_lin; auto with zarith. rewrite spec_w_sub; auto with zarith. rewrite Hv6; rewrite spec_w_zdigits; auto with zarith. @@ -1377,10 +1359,10 @@ intros x; case x; simpl ww_is_even. 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. - repeat rewrite (fun x => Zmult_comm x 2). - rewrite <- Hv0; rewrite <- Zpos_xO; auto with zarith. - apply Zle_lt_trans with (Zpos w_digits); auto with zarith. + apply Z.mul_le_mono_pos_r with 2; auto with zarith. + repeat rewrite (fun x => Z.mul_comm x 2). + rewrite <- Hv0; rewrite <- Pos2Z.inj_xO; auto with zarith. + apply Z.le_lt_trans with (Zpos w_digits); auto with zarith. unfold base; apply Zpower2_lt_lin; auto with zarith. Qed. diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.v index 3167f4c7..799c4e42 100644 --- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.v +++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <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 *) @@ -8,8 +8,6 @@ (* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) (************************************************************************) -(*i $Id: DoubleSub.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - Set Implicit Arguments. Require Import ZArith. @@ -197,9 +195,9 @@ Section DoubleSub. Lemma spec_ww_opp_c : forall x, [-[ww_opp_c x]] = -[[x]]. Proof. destruct x as [ |xh xl];simpl. reflexivity. - rewrite Zopp_plus_distr;generalize (spec_opp_c xl);destruct (w_opp_c xl) + rewrite Z.opp_add_distr;generalize (spec_opp_c xl);destruct (w_opp_c xl) as [l|l];intros H;unfold interp_carry in H;rewrite <- H; - rewrite Zopp_mult_distr_l. + rewrite <- Z.mul_opp_l. assert ([|l|] = 0). assert (H1:= spec_to_Z l);assert (H2 := spec_to_Z xl);omega. rewrite H0;generalize (spec_opp_c xh);destruct (w_opp_c xh) @@ -215,13 +213,13 @@ Section DoubleSub. Lemma spec_ww_opp : forall x, [[ww_opp x]] = (-[[x]]) mod wwB. Proof. destruct x as [ |xh xl];simpl. reflexivity. - rewrite Zopp_plus_distr;rewrite Zopp_mult_distr_l. + rewrite Z.opp_add_distr, <- Z.mul_opp_l. generalize (spec_opp_c xl);destruct (w_opp_c xl) as [l|l];intros H;unfold interp_carry in H;rewrite <- H;simpl ww_to_Z. - rewrite spec_w_0;rewrite Zplus_0_r;rewrite wwB_wBwB. + rewrite spec_w_0;rewrite Z.add_0_r;rewrite wwB_wBwB. assert ([|l|] = 0). assert (H1:= spec_to_Z l);assert (H2 := spec_to_Z xl);omega. - rewrite H0;rewrite Zplus_0_r; rewrite Zpower_2; + rewrite H0;rewrite Z.add_0_r; rewrite Z.pow_2_r; rewrite Zmult_mod_distr_r;try apply lt_0_wB. rewrite spec_opp;trivial. apply Zmod_unique with (q:= -1). @@ -242,7 +240,7 @@ Section DoubleSub. simpl ww_to_Z;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]; intros H;unfold interp_carry in H;rewrite <- H. simpl;apply spec_w_WW. - rewrite Zplus_assoc;rewrite <- Zmult_plus_distr_l. + rewrite Z.add_assoc;rewrite <- Z.mul_add_distr_r. assert ([|l|] = wB - 1). assert (H1:= spec_to_Z l);assert (H2 := spec_to_Z xl);omega. rewrite H0;change ([|xh|] + -1) with ([|xh|] - 1). @@ -265,7 +263,7 @@ Section DoubleSub. generalize (spec_sub_c xh yh);destruct (w_sub_c xh yh) as [h|h];intros H1; unfold interp_carry in H1;rewrite <- H1;unfold interp_carry; try rewrite spec_w_WW;simpl ww_to_Z;try rewrite wwB_wBwB;ring. - rewrite Zplus_assoc;rewrite <- Zmult_plus_distr_l. + rewrite Z.add_assoc;rewrite <- Z.mul_add_distr_r. change ([|xh|] - [|yh|] + -1) with ([|xh|] - [|yh|] - 1). generalize (spec_sub_carry_c xh yh);destruct (w_sub_carry_c xh yh) as [h|h]; intros H1;unfold interp_carry in *;rewrite <- H1;simpl ww_to_Z; @@ -276,7 +274,7 @@ Section DoubleSub. forall x y, [-[ww_sub_carry_c x y]] = [[x]] - [[y]] - 1. Proof. destruct y as [ |yh yl];simpl. - unfold Zminus;simpl;rewrite Zplus_0_r;exact (spec_ww_pred_c x). + unfold Z.sub;simpl;rewrite Z.add_0_r;exact (spec_ww_pred_c x). destruct x as [ |xh xl]. unfold interp_carry;rewrite spec_w_WW;simpl ww_to_Z;rewrite wwB_wBwB; repeat rewrite spec_opp_carry;ring. @@ -288,7 +286,7 @@ Section DoubleSub. generalize (spec_sub_c xh yh);destruct (w_sub_c xh yh) as [h|h];intros H1; unfold interp_carry in H1;rewrite <- H1;unfold interp_carry; try rewrite spec_w_WW;simpl ww_to_Z;try rewrite wwB_wBwB;ring. - rewrite Zplus_assoc;rewrite <- Zmult_plus_distr_l. + rewrite Z.add_assoc;rewrite <- Z.mul_add_distr_r. change ([|xh|] - [|yh|] + -1) with ([|xh|] - [|yh|] - 1). generalize (spec_sub_carry_c xh yh);destruct (w_sub_carry_c xh yh) as [h|h]; intros H1;unfold interp_carry in *;rewrite <- H1;try rewrite spec_w_WW; @@ -305,7 +303,7 @@ Section DoubleSub. unfold interp_carry in H;rewrite <- H;simpl ww_to_Z. 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. + rewrite Z.add_assoc;rewrite <- Z.mul_add_distr_r. change ([|xh|] + -1) with ([|xh|] - 1). assert ([|l|] = wB - 1). assert (H1:= spec_to_Z l);assert (H2:= spec_to_Z xl);omega. @@ -324,7 +322,7 @@ Section DoubleSub. unfold interp_carry in H;rewrite <- H. rewrite spec_w_WW;rewrite (mod_wwB w_digits w_to_Z spec_to_Z). rewrite spec_sub;trivial. - simpl ww_to_Z;rewrite Zplus_assoc;rewrite <- Zmult_plus_distr_l. + simpl ww_to_Z;rewrite Z.add_assoc;rewrite <- Z.mul_add_distr_r. rewrite (mod_wwB w_digits w_to_Z spec_to_Z);rewrite spec_sub_carry;trivial. Qed. @@ -343,7 +341,7 @@ Section DoubleSub. generalize (spec_sub_carry_c xl yl);destruct (w_sub_carry_c xl yl)as[l|l]; intros H;unfold interp_carry in H;rewrite <- H;rewrite spec_w_WW. rewrite (mod_wwB w_digits w_to_Z spec_to_Z);rewrite spec_sub;trivial. - rewrite Zplus_assoc;rewrite <- Zmult_plus_distr_l. + rewrite Z.add_assoc;rewrite <- Z.mul_add_distr_r. rewrite (mod_wwB w_digits w_to_Z spec_to_Z);rewrite spec_sub_carry;trivial. Qed. diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v index eb1132d4..ce1c0bef 100644 --- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v +++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <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 *) @@ -8,14 +8,12 @@ (* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) (************************************************************************) -(*i $Id: DoubleType.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - Set Implicit Arguments. Require Import ZArith. Local Open Scope Z_scope. -Definition base digits := Zpower 2 (Zpos digits). +Definition base digits := Z.pow 2 (Zpos digits). Section Carry. @@ -55,7 +53,7 @@ Section Zn2Z. End Zn2Z. -Implicit Arguments W0 [znz]. +Arguments W0 [znz]. (** From a cyclic representation [w], we iterate the [zn2z] construct [n] times, gaining the type of binary trees of depth at most [n], |