summaryrefslogtreecommitdiff
path: root/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2013-05-08 18:03:54 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2013-05-08 18:03:54 +0200
commitdb38bb4ad9aff74576d3b7f00028d48f0447d5bd (patch)
tree09dafc3e5c7361d3a28e93677eadd2b7237d4f9f /theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v
parent6e34b272d789455a9be589e27ad3a998cf25496b (diff)
parent499a11a45b5711d4eaabe84a80f0ad3ae539d500 (diff)
Merge branch 'experimental/upstream' into upstream
Diffstat (limited to 'theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v')
-rw-r--r--theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v350
1 files changed, 160 insertions, 190 deletions
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.