diff options
Diffstat (limited to 'theories/Numbers/Cyclic')
| -rw-r--r-- | theories/Numbers/Cyclic/Abstract/CyclicAxioms.v | 21 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/Abstract/NZCyclic.v | 8 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v | 37 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v | 8 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v | 164 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v | 44 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v | 5 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.v | 2 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.v | 12 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v | 20 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.v | 11 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v | 5 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/Int31/Cyclic31.v | 270 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/Int31/Int31.v | 15 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/Int31/Ring31.v | 2 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/ZModulo/ZModulo.v | 55 |
16 files changed, 439 insertions, 240 deletions
diff --git a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v index 622ef225..8b84a484 100644 --- a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v +++ b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -88,8 +88,12 @@ Module ZnZ. is_even : t -> bool; (* square root *) sqrt2 : t -> t -> t * carry t; - sqrt : t -> t }. - + sqrt : t -> t; + (* bitwise operations *) + lor : t -> t -> t; + land : t -> t -> t; + lxor : t -> t -> t }. + Section Specs. Context {t : Type}{ops : Ops t}. @@ -98,10 +102,10 @@ Module ZnZ. Let wB := base digits. Notation "[+| c |]" := - (interp_carry 1 wB to_Z c) (at level 0, x at level 99). + (interp_carry 1 wB to_Z c) (at level 0, c at level 99). Notation "[-| c |]" := - (interp_carry (-1) wB to_Z c) (at level 0, x at level 99). + (interp_carry (-1) wB to_Z c) (at level 0, c at level 99). Notation "[|| x ||]" := (zn2z_to_Z wB to_Z x) (at level 0, x at level 99). @@ -199,7 +203,10 @@ Module ZnZ. [||WW x y||] = [|s|] ^ 2 + [+|r|] /\ [+|r|] <= 2 * [|s|]; spec_sqrt : forall x, - [|sqrt x|] ^ 2 <= [|x|] < ([|sqrt x|] + 1) ^ 2 + [|sqrt x|] ^ 2 <= [|x|] < ([|sqrt x|] + 1) ^ 2; + spec_lor : forall x y, [|lor x y|] = Z.lor [|x|] [|y|]; + spec_land : forall x y, [|land x y|] = Z.land [|x|] [|y|]; + spec_lxor : forall x y, [|lxor x y|] = Z.lxor [|x|] [|y|] }. End Specs. @@ -283,7 +290,7 @@ Module ZnZ. intros p Hp. generalize (spec_of_pos p). case (of_pos p); intros n w1; simpl. - case n; simpl Npos; auto with zarith. + case n; auto with zarith. intros p1 Hp1; contradict Hp; apply Z.le_ngt. replace (base digits) with (1 * base digits + 0) by ring. rewrite Hp1. diff --git a/theories/Numbers/Cyclic/Abstract/NZCyclic.v b/theories/Numbers/Cyclic/Abstract/NZCyclic.v index d9089e18..8adeda37 100644 --- a/theories/Numbers/Cyclic/Abstract/NZCyclic.v +++ b/theories/Numbers/Cyclic/Abstract/NZCyclic.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -106,7 +106,7 @@ Qed. Theorem one_succ : one == succ zero. Proof. -zify; simpl. now rewrite one_mod_wB. +zify; simpl Z.add. now rewrite one_mod_wB. Qed. Theorem two_succ : two == succ one. @@ -126,9 +126,7 @@ Let B (n : Z) := A (ZnZ.of_Z n). Lemma B0 : B 0. Proof. -unfold B. -setoid_replace (ZnZ.of_Z 0) with zero. assumption. -red; zify. apply ZnZ.of_Z_correct. auto using gt_wB_0 with zarith. +unfold B. apply A0. Qed. Lemma BS : forall n : Z, 0 <= n -> n < wB - 1 -> B n -> B (n + 1). diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v index 1b035948..a7c28862 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-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -150,17 +150,17 @@ Section DoubleAdd. Notation wwB := (base (ww_digits w_digits)). Notation "[| x |]" := (w_to_Z x) (at level 0, x at level 99). Notation "[+| c |]" := - (interp_carry 1 wB w_to_Z c) (at level 0, x at level 99). + (interp_carry 1 wB w_to_Z c) (at level 0, c at level 99). Notation "[-| c |]" := - (interp_carry (-1) wB w_to_Z c) (at level 0, x at level 99). + (interp_carry (-1) wB w_to_Z c) (at level 0, c at level 99). Notation "[[ x ]]" := (ww_to_Z w_digits w_to_Z x)(at level 0, x at level 99). Notation "[+[ c ]]" := (interp_carry 1 wwB (ww_to_Z w_digits w_to_Z) c) - (at level 0, x at level 99). + (at level 0, c at level 99). Notation "[-[ c ]]" := (interp_carry (-1) wwB (ww_to_Z w_digits w_to_Z) c) - (at level 0, x at level 99). + (at level 0, c at level 99). Variable spec_w_0 : [|w_0|] = 0. Variable spec_w_1 : [|w_1|] = 1. @@ -194,9 +194,9 @@ 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 Z.add_0_r;trivial. - replace ([|xh|] * wB + [|xl|] + ([|yh|] * wB + [|yl|])) + destruct x as [ |xh xl];trivial. + destruct y as [ |yh yl]. rewrite Z.add_0_r;trivial. + simpl. 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. @@ -218,10 +218,11 @@ Section DoubleAdd. Lemma spec_ww_add_c_cont : P x y (ww_add_c_cont x y). Proof. - destruct x as [ |xh xl];simpl;trivial. + destruct x as [ |xh xl];trivial. apply spec_f0;trivial. - destruct y as [ |yh yl];simpl. - apply spec_f0;simpl;rewrite Z.add_0_r;trivial. + destruct y as [ |yh yl]. + apply spec_f0;rewrite Z.add_0_r;trivial. + simpl. 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]; @@ -234,10 +235,10 @@ Section DoubleAdd. as [h|h]; intros H1;unfold interp_carry in *. 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. + apply spec_f1. rewrite spec_w_WW;rewrite wwB_wBwB. 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. + rewrite <- Z.add_assoc;rewrite H; simpl; ring. Qed. End Cont. @@ -245,11 +246,11 @@ Section DoubleAdd. Lemma spec_ww_add_carry_c : forall x y, [+[ww_add_carry_c x y]] = [[x]] + [[y]] + 1. Proof. - destruct x as [ |xh xl];intro y;simpl. + destruct x as [ |xh xl];intro y. exact (spec_ww_succ_c y). - destruct y as [ |yh yl];simpl. + destruct y as [ |yh yl]. rewrite Z.add_0_r;exact (spec_ww_succ_c (WW xh xl)). - replace ([|xh|] * wB + [|xl|] + ([|yh|] * wB + [|yl|]) + 1) + 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];intros H;unfold interp_carry in H;rewrite <- H. @@ -281,7 +282,7 @@ Section DoubleAdd. Lemma spec_ww_add : forall x y, [[ww_add x y]] = ([[x]] + [[y]]) mod wwB. Proof. - destruct x as [ |xh xl];intros y;simpl. + destruct x as [ |xh xl];intros y. rewrite Zmod_small;trivial. apply spec_ww_to_Z;trivial. destruct y as [ |yh yl]. change [[W0]] with 0;rewrite Z.add_0_r. @@ -299,7 +300,7 @@ Section DoubleAdd. Lemma spec_ww_add_carry : forall x y, [[ww_add_carry x y]] = ([[x]] + [[y]] + 1) mod wwB. Proof. - destruct x as [ |xh xl];intros y;simpl. + destruct x as [ |xh xl];intros y. exact (spec_ww_succ y). destruct y as [ |yh yl]. change [[W0]] with 0;rewrite Z.add_0_r. exact (spec_ww_succ (WW xh xl)). diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v index 41a1d8ba..e68cd033 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-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -149,9 +149,9 @@ Section DoubleBase. Notation "[| x |]" := (w_to_Z x) (at level 0, x at level 99). Notation "[[ x ]]" := (ww_to_Z x) (at level 0, x at level 99). Notation "[+[ c ]]" := - (interp_carry 1 wwB ww_to_Z c) (at level 0, x at level 99). + (interp_carry 1 wwB ww_to_Z c) (at level 0, c at level 99). Notation "[-[ c ]]" := - (interp_carry (-1) wwB ww_to_Z c) (at level 0, x at level 99). + (interp_carry (-1) wwB ww_to_Z c) (at level 0, c at level 99). Notation "[! n | x !]" := (double_to_Z n x) (at level 0, x at level 99). Variable spec_w_0 : [|w_0|] = 0. @@ -287,7 +287,7 @@ Section DoubleBase. 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 Pshiftl_nat_S, (Pos2Z.inj_xO (_ << _)). + unfold base. rewrite (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. diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v index e207d7eb..e137349e 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-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -283,6 +283,27 @@ Section Z_2nZ. Eval lazy beta delta [ww_gcd] in ww_gcd compare w_0 w_eq0 w_gcd_gt _ww_digits gcd_gt_fix gcd_cont. + Definition lor (x y : zn2z t) := + match x, y with + | W0, _ => y + | _, W0 => x + | WW hx lx, WW hy ly => WW (ZnZ.lor hx hy) (ZnZ.lor lx ly) + end. + + Definition land (x y : zn2z t) := + match x, y with + | W0, _ => W0 + | _, W0 => W0 + | WW hx lx, WW hy ly => WW (ZnZ.land hx hy) (ZnZ.land lx ly) + end. + + Definition lxor (x y : zn2z t) := + match x, y with + | W0, _ => y + | _, W0 => x + | WW hx lx, WW hy ly => WW (ZnZ.lxor hx hy) (ZnZ.lxor lx ly) + end. + (* ** Record of operators on 2 words *) Global Instance mk_zn2z_ops : ZnZ.Ops (zn2z t) | 1 := @@ -303,7 +324,10 @@ Section Z_2nZ. pos_mod is_even sqrt2 - sqrt. + sqrt + lor + land + lxor. Global Instance mk_zn2z_ops_karatsuba : ZnZ.Ops (zn2z t) | 2 := ZnZ.MkOps _ww_digits _ww_zdigits @@ -323,10 +347,15 @@ Section Z_2nZ. pos_mod is_even sqrt2 - sqrt. + sqrt + lor + land + lxor. (* Proof *) Context {specs : ZnZ.Specs ops}. + + Create HintDb ZnZ. Hint Resolve ZnZ.spec_to_Z @@ -370,24 +399,24 @@ Section Z_2nZ. ZnZ.spec_sqrt ZnZ.spec_WO ZnZ.spec_OW - ZnZ.spec_WW. - - Ltac wwauto := unfold ww_to_Z; auto. + ZnZ.spec_WW : ZnZ. + + Ltac wwauto := unfold ww_to_Z; eauto with ZnZ. Let wwB := base _ww_digits. Notation "[| x |]" := (to_Z x) (at level 0, x at level 99). Notation "[+| c |]" := - (interp_carry 1 wwB to_Z c) (at level 0, x at level 99). + (interp_carry 1 wwB to_Z c) (at level 0, c at level 99). Notation "[-| c |]" := - (interp_carry (-1) wwB to_Z c) (at level 0, x at level 99). + (interp_carry (-1) wwB to_Z c) (at level 0, c at level 99). Notation "[[ x ]]" := (zn2z_to_Z wwB to_Z x) (at level 0, x at level 99). Let spec_ww_to_Z : forall x, 0 <= [| x |] < wwB. - Proof. refine (spec_ww_to_Z w_digits w_to_Z _);auto. Qed. + Proof. refine (spec_ww_to_Z w_digits w_to_Z _); wwauto. Qed. Let spec_ww_of_pos : forall p, Zpos p = (Z.of_N (fst (ww_of_pos p)))*wwB + [|(snd (ww_of_pos p))|]. @@ -411,15 +440,15 @@ Section Z_2nZ. Proof. reflexivity. Qed. Let spec_ww_1 : [|ww_1|] = 1. - Proof. refine (spec_ww_1 w_0 w_1 w_digits w_to_Z _ _);auto. Qed. + Proof. refine (spec_ww_1 w_0 w_1 w_digits w_to_Z _ _);wwauto. Qed. Let spec_ww_Bm1 : [|ww_Bm1|] = wwB - 1. - Proof. refine (spec_ww_Bm1 w_Bm1 w_digits w_to_Z _);auto. Qed. + Proof. refine (spec_ww_Bm1 w_Bm1 w_digits w_to_Z _);wwauto. Qed. Let spec_ww_compare : 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. + refine (spec_ww_compare w_0 w_digits w_to_Z w_compare _ _ _);wwauto. Qed. Let spec_ww_eq0 : forall x, eq0 x = true -> [|x|] = 0. @@ -428,14 +457,14 @@ Section Z_2nZ. Let spec_ww_opp_c : forall x, [-|opp_c x|] = -[|x|]. Proof. refine(spec_ww_opp_c w_0 w_0 W0 w_opp_c w_opp_carry w_digits w_to_Z _ _ _ _); - auto. + wwauto. Qed. Let spec_ww_opp : forall x, [|opp x|] = (-[|x|]) mod wwB. Proof. refine(spec_ww_opp w_0 w_0 W0 w_opp_c w_opp_carry w_opp w_digits w_to_Z _ _ _ _ _); - auto. + wwauto. Qed. Let spec_ww_opp_carry : forall x, [|opp_carry x|] = wwB - [|x|] - 1. @@ -446,7 +475,7 @@ Section Z_2nZ. Let spec_ww_succ_c : forall x, [+|succ_c x|] = [|x|] + 1. Proof. - refine (spec_ww_succ_c w_0 w_0 ww_1 w_succ_c w_digits w_to_Z _ _ _ _);auto. + refine (spec_ww_succ_c w_0 w_0 ww_1 w_succ_c w_digits w_to_Z _ _ _ _);wwauto. Qed. Let spec_ww_add_c : forall x y, [+|add_c x y|] = [|x|] + [|y|]. @@ -468,7 +497,7 @@ Section Z_2nZ. Let spec_ww_add : forall x y, [|add x y|] = ([|x|] + [|y|]) mod wwB. Proof. - refine (spec_ww_add w_add_c w_add w_add_carry w_digits w_to_Z _ _ _ _);auto. + refine (spec_ww_add w_add_c w_add w_add_carry w_digits w_to_Z _ _ _ _);wwauto. Qed. Let spec_ww_add_carry : forall x y, [|add_carry x y|]=([|x|]+[|y|]+1)mod wwB. @@ -565,7 +594,7 @@ Section Z_2nZ. 0 <= [|r|] < [|b|]. Proof. refine (spec_ww_div21 w_0 w_0W div32 ww_1 compare sub w_digits w_to_Z - _ _ _ _ _ _ _);wwauto. + _ _ _ _ _ _ _);wwauto. Qed. Let spec_add2: forall x y, @@ -581,13 +610,14 @@ Section Z_2nZ. Qed. Let spec_low: forall x, - w_to_Z (low x) = [|x|] mod wB. + w_to_Z (low x) = [|x|] mod wB. intros x; case x; simpl low. - unfold ww_to_Z, w_to_Z, w_0; rewrite ZnZ.spec_0; simpl; auto. + unfold ww_to_Z, w_to_Z, w_0; rewrite ZnZ.spec_0; simpl; wwauto. intros xh xl; simpl. rewrite Z.add_comm; rewrite Z_mod_plus; auto with zarith. rewrite Zmod_small; auto with zarith. - unfold wB, base; auto with zarith. + unfold wB, base; eauto with ZnZ zarith. + unfold wB, base; eauto with ZnZ zarith. Qed. Let spec_ww_digits: @@ -605,7 +635,7 @@ 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 _ _ _ (eq_refl _ww_digits) _ _ _ _); auto. + w_to_Z _ _ _ (eq_refl _ww_digits) _ _ _ _); wwauto. exact ZnZ.spec_head00. exact ZnZ.spec_zdigits. Qed. @@ -688,7 +718,7 @@ refine [|a|] = [|q|] * [|b|] + [|r|] /\ 0 <= [|r|] < [|b|]. Proof. - refine (spec_ww_div w_digits ww_1 compare div_gt w_to_Z _ _ _ _);auto. + refine (spec_ww_div w_digits ww_1 compare div_gt w_to_Z _ _ _ _);wwauto. Qed. Let spec_ww_mod_gt : forall a b, @@ -708,7 +738,7 @@ refine Let spec_ww_mod : forall a b, 0 < [|b|] -> [|mod_ a b|] = [|a|] mod [|b|]. Proof. - refine (spec_ww_mod w_digits W0 compare mod_gt w_to_Z _ _ _);auto. + refine (spec_ww_mod w_digits W0 compare mod_gt w_to_Z _ _ _);wwauto. Qed. Let spec_ww_gcd_gt : forall a b, [|a|] > [|b|] -> @@ -716,7 +746,7 @@ refine Proof. 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. + _ gcd_gt_fix _ _ _ _ gcd_cont _);wwauto. 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 @@ -725,13 +755,13 @@ refine exact ZnZ.spec_zdigits. exact spec_ww_add_mul_div. refine (@spec_gcd_cont t w_digits ww_1 w_to_Z _ _ w_0 w_1 w_compare - _ _);auto. + _ _);wwauto. Qed. Let spec_ww_gcd : forall a b, Zis_gcd [|a|] [|b|] [|gcd a b|]. Proof. 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. + _ww_digits _ gcd_gt_fix _ _ _ _ gcd_cont _);wwauto. 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 @@ -740,7 +770,7 @@ refine exact ZnZ.spec_zdigits. exact spec_ww_add_mul_div. refine (@spec_gcd_cont t w_digits ww_1 w_to_Z _ _ w_0 w_1 w_compare - _ _);auto. + _ _);wwauto. Qed. Let spec_ww_is_even : forall x, @@ -779,7 +809,7 @@ refine 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. + _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _); wwauto. exact ZnZ.spec_zdigits. exact ZnZ.spec_more_than_1_digit. exact ZnZ.spec_is_even. @@ -787,6 +817,83 @@ refine exact ZnZ.spec_sqrt2. Qed. + Let wB_pos : 0 < wB. + Proof. + unfold wB, base; apply Z.pow_pos_nonneg; auto with zarith. + Qed. + + Hint Transparent ww_to_Z. + + Let ww_testbit_high n x y : Z.pos w_digits <= n -> + Z.testbit [|WW x y|] n = + Z.testbit (ZnZ.to_Z x) (n - Z.pos w_digits). + Proof. + intros Hn. + assert (E : ZnZ.to_Z x = [|WW x y|] / wB). + { simpl. + rewrite Z.div_add_l; eauto with ZnZ zarith. + now rewrite Z.div_small, Z.add_0_r; wwauto. } + rewrite E. + unfold wB, base. rewrite Z.div_pow2_bits. + - f_equal; auto with zarith. + - easy. + - auto with zarith. + Qed. + + Let ww_testbit_low n x y : 0 <= n < Z.pos w_digits -> + Z.testbit [|WW x y|] n = Z.testbit (ZnZ.to_Z y) n. + Proof. + intros (Hn,Hn'). + assert (E : ZnZ.to_Z y = [|WW x y|] mod wB). + { simpl; symmetry. + rewrite Z.add_comm, Z.mod_add; auto with zarith nocore. + apply Z.mod_small; eauto with ZnZ zarith. } + rewrite E. + unfold wB, base. symmetry. apply Z.mod_pow2_bits_low; auto. + Qed. + + Let spec_lor x y : [|lor x y|] = Z.lor [|x|] [|y|]. + Proof. + destruct x as [ |hx lx]. trivial. + destruct y as [ |hy ly]. now rewrite Z.lor_comm. + change ([|WW (ZnZ.lor hx hy) (ZnZ.lor lx ly)|] = + Z.lor [|WW hx lx|] [|WW hy ly|]). + apply Z.bits_inj'; intros n Hn. + rewrite Z.lor_spec. + destruct (Z.le_gt_cases (Z.pos w_digits) n) as [LE|GT]. + - now rewrite !ww_testbit_high, ZnZ.spec_lor, Z.lor_spec. + - rewrite !ww_testbit_low; auto. + now rewrite ZnZ.spec_lor, Z.lor_spec. + Qed. + + Let spec_land x y : [|land x y|] = Z.land [|x|] [|y|]. + Proof. + destruct x as [ |hx lx]. trivial. + destruct y as [ |hy ly]. now rewrite Z.land_comm. + change ([|WW (ZnZ.land hx hy) (ZnZ.land lx ly)|] = + Z.land [|WW hx lx|] [|WW hy ly|]). + apply Z.bits_inj'; intros n Hn. + rewrite Z.land_spec. + destruct (Z.le_gt_cases (Z.pos w_digits) n) as [LE|GT]. + - now rewrite !ww_testbit_high, ZnZ.spec_land, Z.land_spec. + - rewrite !ww_testbit_low; auto. + now rewrite ZnZ.spec_land, Z.land_spec. + Qed. + + Let spec_lxor x y : [|lxor x y|] = Z.lxor [|x|] [|y|]. + Proof. + destruct x as [ |hx lx]. trivial. + destruct y as [ |hy ly]. now rewrite Z.lxor_comm. + change ([|WW (ZnZ.lxor hx hy) (ZnZ.lxor lx ly)|] = + Z.lxor [|WW hx lx|] [|WW hy ly|]). + apply Z.bits_inj'; intros n Hn. + rewrite Z.lxor_spec. + destruct (Z.le_gt_cases (Z.pos w_digits) n) as [LE|GT]. + - now rewrite !ww_testbit_high, ZnZ.spec_lxor, Z.lxor_spec. + - rewrite !ww_testbit_low; auto. + now rewrite ZnZ.spec_lxor, Z.lxor_spec. + Qed. + Global Instance mk_zn2z_specs : ZnZ.Specs mk_zn2z_ops. Proof. apply ZnZ.MkSpecs; auto. @@ -816,6 +923,7 @@ refine End Z_2nZ. + Section MulAdd. Context {t : Type}{ops : ZnZ.Ops t}{specs : ZnZ.Specs ops}. diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v index 08f05bbf..cd55f9d8 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-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -97,8 +97,7 @@ Section POS_MOD. assert (HHHHH:= lt_0_wB w_digits). assert (F0: forall x y, x - y + y = x); auto with zarith. intros w1 p; case (spec_to_w_Z p); intros HH1 HH2. - unfold ww_pos_mod; case w1. - simpl; rewrite Zmod_small; split; auto with zarith. + unfold ww_pos_mod; case w1. reflexivity. intros xh xl; rewrite spec_ww_compare. case Z.compare_spec; rewrite spec_w_0W; rewrite spec_zdigits; fold wB; @@ -211,8 +210,7 @@ Section DoubleDiv32. Variable w_div21 : w -> w -> w -> w*w. Variable ww_sub_c : zn2z w -> zn2z w -> carry (zn2z w). - Definition w_div32 a1 a2 a3 b1 b2 := - Eval lazy beta iota delta [ww_add_c_cont ww_add] in + Definition w_div32_body a1 a2 a3 b1 b2 := match w_compare a1 b1 with | Lt => let (q,r) := w_div21 a1 a2 b1 in @@ -233,6 +231,10 @@ Section DoubleDiv32. | Gt => (w_0, W0) (* cas absurde *) end. + Definition w_div32 a1 a2 a3 b1 b2 := + Eval lazy beta iota delta [ww_add_c_cont ww_add w_div32_body] in + w_div32_body a1 a2 a3 b1 b2. + (* Proof *) Variable w_digits : positive. @@ -242,14 +244,14 @@ Section DoubleDiv32. Notation wwB := (base (ww_digits w_digits)). Notation "[| x |]" := (w_to_Z x) (at level 0, x at level 99). Notation "[+| c |]" := - (interp_carry 1 wB w_to_Z c) (at level 0, x at level 99). + (interp_carry 1 wB w_to_Z c) (at level 0, c at level 99). Notation "[-| c |]" := - (interp_carry (-1) wB w_to_Z c) (at level 0, x at level 99). + (interp_carry (-1) wB w_to_Z c) (at level 0, c at level 99). Notation "[[ x ]]" := (ww_to_Z w_digits w_to_Z x)(at level 0, x at level 99). Notation "[-[ c ]]" := (interp_carry (-1) wwB (ww_to_Z w_digits w_to_Z) c) - (at level 0, x at level 99). + (at level 0, c at level 99). Variable spec_w_0 : [|w_0|] = 0. @@ -312,26 +314,8 @@ Section DoubleDiv32. 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 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 => - let (q,r) := w_div21 a1 a2 b1 in - match ww_sub_c (w_WW r a3) (w_mul_c q b2) with - | C0 r1 => (q,r1) - | C1 r1 => - let q := w_pred q in - ww_add_c_cont w_WW w_add_c w_add_carry_c - (fun r2=>(w_pred q, ww_add w_add_c w_add w_add_carry r2 (WW b1 b2))) - (fun r2 => (q,r2)) - r1 (WW b1 b2) - end - | Eq => - ww_add_c_cont w_WW w_add_c w_add_carry_c - (fun r => (w_Bm2, ww_add w_add_c w_add w_add_carry r (WW b1 b2))) - (fun r => (w_Bm1,r)) - (WW (w_sub a2 b2) a3) (WW b1 b2) - | Gt => (w_0, W0) (* cas absurde *) - end. + change (w_div32 a1 a2 a3 b1 b2) with (w_div32_body a1 a2 a3 b1 b2). + unfold w_div32_body. rewrite spec_compare. case Z.compare_spec; intro Hcmp. simpl in Hlt. rewrite Hcmp in Hlt;assert ([|a2|] < [|b2|]). omega. @@ -520,7 +504,7 @@ Section DoubleDiv21. Notation "[[ x ]]" := (ww_to_Z w_digits w_to_Z x)(at level 0, x at level 99). Notation "[-[ c ]]" := (interp_carry (-1) wwB (ww_to_Z w_digits w_to_Z) c) - (at level 0, x at level 99). + (at level 0, c at level 99). Variable spec_w_0 : [|w_0|] = 0. Variable spec_to_Z : forall x, 0 <= [|x|] < wB. @@ -782,7 +766,7 @@ Section DoubleDivGt. Notation wwB := (base (ww_digits w_digits)). Notation "[| x |]" := (w_to_Z x) (at level 0, x at level 99). Notation "[-| c |]" := - (interp_carry (-1) wB w_to_Z c) (at level 0, x at level 99). + (interp_carry (-1) wB w_to_Z c) (at level 0, c at level 99). Notation "[[ x ]]" := (ww_to_Z w_digits w_to_Z x)(at level 0, x at level 99). diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v index 8e179ef6..6a1d741e 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-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -160,7 +160,7 @@ Section GENDIVN1. Lemma p_lt_double_digits : forall n, [|p|] <= Zpos (w_digits << n). Proof. induction n;simpl. trivial. - case (spec_to_Z p); rewrite Pshiftl_nat_S, Pos2Z.inj_xO;auto with zarith. + case (spec_to_Z p); rewrite Pos2Z.inj_xO;auto with zarith. Qed. Lemma spec_double_divn1_p : forall n r h l, @@ -305,7 +305,6 @@ Section GENDIVN1. Lemma spec_double_digits:forall n, Zpos w_digits <= Zpos (w_digits << n). Proof. induction n;simpl;auto with zarith. - rewrite Pshiftl_nat_S. change (Zpos (xO (w_digits << n))) with (2*Zpos (w_digits << n)). assert (0 < Zpos w_digits) by reflexivity. diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.v index 2d0cc0fb..ff9f50a5 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-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.v index 1c0fc68a..537f557d 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-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -218,17 +218,17 @@ Section DoubleMul. Notation wwB := (base (ww_digits w_digits)). Notation "[| x |]" := (w_to_Z x) (at level 0, x at level 99). Notation "[+| c |]" := - (interp_carry 1 wB w_to_Z c) (at level 0, x at level 99). + (interp_carry 1 wB w_to_Z c) (at level 0, c at level 99). Notation "[-| c |]" := - (interp_carry (-1) wB w_to_Z c) (at level 0, x at level 99). + (interp_carry (-1) wB w_to_Z c) (at level 0, c at level 99). Notation "[[ x ]]" := (ww_to_Z w_digits w_to_Z x)(at level 0, x at level 99). Notation "[+[ c ]]" := (interp_carry 1 wwB (ww_to_Z w_digits w_to_Z) c) - (at level 0, x at level 99). + (at level 0, c at level 99). Notation "[-[ c ]]" := (interp_carry (-1) wwB (ww_to_Z w_digits w_to_Z) c) - (at level 0, x at level 99). + (at level 0, c at level 99). Notation "[|| x ||]" := (zn2z_to_Z wwB (ww_to_Z w_digits w_to_Z) x) (at level 0, x at level 99). @@ -328,7 +328,7 @@ Section DoubleMul. 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. + destruct (Z_le_gt_dec ([|wc|]*wB + [|cch|]) (2*wB - 3)) as [Hle|Hgt];trivial. assert ([|xh|] * [|yl|] + [|xl|] * [|yh|] <= (2*wB - 4)*wB + 2). ring_simplify ((2*wB - 4)*wB + 2). assert (H4 := Zmult_lt_b _ _ _ (spec_to_Z xh) (spec_to_Z yl)). diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v index 149682f8..ab8c8617 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-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -185,17 +185,17 @@ Section DoubleSqrt. Notation wwB := (base (ww_digits w_digits)). Notation "[| x |]" := (w_to_Z x) (at level 0, x at level 99). Notation "[+| c |]" := - (interp_carry 1 wB w_to_Z c) (at level 0, x at level 99). + (interp_carry 1 wB w_to_Z c) (at level 0, c at level 99). Notation "[-| c |]" := - (interp_carry (-1) wB w_to_Z c) (at level 0, x at level 99). + (interp_carry (-1) wB w_to_Z c) (at level 0, c at level 99). Notation "[[ x ]]" := (ww_to_Z w_digits w_to_Z x)(at level 0, x at level 99). Notation "[+[ c ]]" := (interp_carry 1 wwB (ww_to_Z w_digits w_to_Z) c) - (at level 0, x at level 99). + (at level 0, c at level 99). Notation "[-[ c ]]" := (interp_carry (-1) wwB (ww_to_Z w_digits w_to_Z) c) - (at level 0, x at level 99). + (at level 0, c at level 99). Notation "[|| x ||]" := (zn2z_to_Z wwB (ww_to_Z w_digits w_to_Z) x) (at level 0, x at level 99). @@ -266,8 +266,8 @@ Section DoubleSqrt. if ww_is_even x then [[x]] mod 2 = 0 else [[x]] mod 2 = 1. clear spec_more_than_1_digit. intros x; case x; simpl ww_is_even. + reflexivity. simpl. - rewrite Zmod_small; auto with zarith. intros w1 w2; simpl. unfold base. rewrite Zplus_mod; auto with zarith. @@ -692,7 +692,7 @@ intros x; case x; simpl ww_is_even. intros x y H; unfold ww_sqrt2. repeat match goal with |- context[split ?x] => generalize (spec_split x); case (split x) - end; simpl fst; simpl snd. + end; simpl @fst; simpl @snd. intros w0 w1 Hw0 w2 w3 Hw1. assert (U: wB/4 <= [|w2|]). case (Z.le_gt_cases (wB / 4) [|w2|]); auto; intros H1. @@ -761,7 +761,7 @@ intros x; case x; simpl ww_is_even. auto. split. unfold zn2z_to_Z; rewrite <- Hw1. - unfold ww_to_Z, zn2z_to_Z in H1; rewrite H1. + unfold ww_to_Z, zn2z_to_Z in H1. rewrite H1. rewrite <- Hw0. match goal with |- (?X ^2 + ?Y) * wwB + (?Z * wB + ?T) = ?U => transitivity ((X * wB) ^ 2 + (Y * wB + Z) * wB + T) @@ -1193,7 +1193,7 @@ Qed. rewrite <- wwB_4_wB_4; auto. generalize (@spec_w_sqrt2 w0 w1 V);auto with zarith. case (w_sqrt2 w0 w1); intros w2 c. - simpl ww_to_Z; simpl fst. + simpl ww_to_Z; simpl @fst. case c; unfold interp_carry; autorewrite with rm10. intros w3 (H6, H7); rewrite H6. assert (V1 := spec_to_Z w3);auto with zarith. @@ -1256,7 +1256,7 @@ Qed. generalize (@spec_w_sqrt2 w0 w1 V);auto with zarith. case (w_sqrt2 w0 w1); intros w2 c. case (spec_to_Z w2); intros HH1 HH2. - simpl ww_to_Z; simpl fst. + simpl ww_to_Z; simpl @fst. assert (Hv3: [[ww_pred ww_zdigits]] = Zpos (xO w_digits) - 1). rewrite spec_ww_pred; rewrite spec_ww_zdigits. diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.v index aaa93a21..a2df2600 100644 --- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.v +++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.v @@ -1,6 +1,7 @@ + (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <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 *) @@ -159,17 +160,17 @@ Section DoubleSub. Notation wwB := (base (ww_digits w_digits)). Notation "[| x |]" := (w_to_Z x) (at level 0, x at level 99). Notation "[+| c |]" := - (interp_carry 1 wB w_to_Z c) (at level 0, x at level 99). + (interp_carry 1 wB w_to_Z c) (at level 0, c at level 99). Notation "[-| c |]" := - (interp_carry (-1) wB w_to_Z c) (at level 0, x at level 99). + (interp_carry (-1) wB w_to_Z c) (at level 0, c at level 99). Notation "[[ x ]]" := (ww_to_Z w_digits w_to_Z x)(at level 0, x at level 99). Notation "[+[ c ]]" := (interp_carry 1 wwB (ww_to_Z w_digits w_to_Z) c) - (at level 0, x at level 99). + (at level 0, c at level 99). Notation "[-[ c ]]" := (interp_carry (-1) wwB (ww_to_Z w_digits w_to_Z) c) - (at level 0, x at level 99). + (at level 0, c at level 99). Variable spec_w_0 : [|w_0|] = 0. Variable spec_w_Bm1 : [|w_Bm1|] = wB - 1. diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v index 1ab75307..c1f314e9 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-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -14,6 +14,7 @@ Require Import ZArith. Local Open Scope Z_scope. Definition base digits := Z.pow 2 (Zpos digits). +Arguments base digits: simpl never. Section Carry. @@ -53,7 +54,7 @@ Section Zn2Z. End Zn2Z. -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], diff --git a/theories/Numbers/Cyclic/Int31/Cyclic31.v b/theories/Numbers/Cyclic/Int31/Cyclic31.v index cef3ecae..aca57216 100644 --- a/theories/Numbers/Cyclic/Int31/Cyclic31.v +++ b/theories/Numbers/Cyclic/Int31/Cyclic31.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -75,88 +75,87 @@ Section Basics. (** * Iterated shift to the right *) - Definition nshiftr n x := iter_nat n _ shiftr x. + Definition nshiftr x := nat_rect _ x (fun _ => shiftr). Lemma nshiftr_S : - forall n x, nshiftr (S n) x = shiftr (nshiftr n x). + forall n x, nshiftr x (S n) = shiftr (nshiftr x n). Proof. reflexivity. Qed. Lemma nshiftr_S_tail : - forall n x, nshiftr (S n) x = nshiftr n (shiftr x). + forall n x, nshiftr x (S n) = nshiftr (shiftr x) n. Proof. - induction n; simpl; auto. - intros; rewrite nshiftr_S, IHn, nshiftr_S; auto. + intros n; elim n; simpl; auto. + intros; now f_equal. Qed. - Lemma nshiftr_n_0 : forall n, nshiftr n 0 = 0. + Lemma nshiftr_n_0 : forall n, nshiftr 0 n = 0. Proof. induction n; simpl; auto. - rewrite nshiftr_S, IHn; auto. + rewrite IHn; auto. Qed. - Lemma nshiftr_size : forall x, nshiftr size x = 0. + Lemma nshiftr_size : forall x, nshiftr x size = 0. Proof. destruct x; simpl; auto. Qed. Lemma nshiftr_above_size : forall k x, size<=k -> - nshiftr k x = 0. + nshiftr x k = 0. Proof. intros. replace k with ((k-size)+size)%nat by omega. induction (k-size)%nat; auto. rewrite nshiftr_size; auto. - simpl; rewrite nshiftr_S, IHn; auto. + simpl; rewrite IHn; auto. Qed. (** * Iterated shift to the left *) - Definition nshiftl n x := iter_nat n _ shiftl x. + Definition nshiftl x := nat_rect _ x (fun _ => shiftl). Lemma nshiftl_S : - forall n x, nshiftl (S n) x = shiftl (nshiftl n x). + forall n x, nshiftl x (S n) = shiftl (nshiftl x n). Proof. reflexivity. Qed. Lemma nshiftl_S_tail : - forall n x, nshiftl (S n) x = nshiftl n (shiftl x). - Proof. - induction n; simpl; auto. - intros; rewrite nshiftl_S, IHn, nshiftl_S; auto. + forall n x, nshiftl x (S n) = nshiftl (shiftl x) n. + Proof. + intros n; elim n; simpl; intros; now f_equal. Qed. - Lemma nshiftl_n_0 : forall n, nshiftl n 0 = 0. + Lemma nshiftl_n_0 : forall n, nshiftl 0 n = 0. Proof. induction n; simpl; auto. - rewrite nshiftl_S, IHn; auto. + rewrite IHn; auto. Qed. - Lemma nshiftl_size : forall x, nshiftl size x = 0. + Lemma nshiftl_size : forall x, nshiftl x size = 0. Proof. destruct x; simpl; auto. Qed. Lemma nshiftl_above_size : forall k x, size<=k -> - nshiftl k x = 0. + nshiftl x k = 0. Proof. intros. replace k with ((k-size)+size)%nat by omega. induction (k-size)%nat; auto. rewrite nshiftl_size; auto. - simpl; rewrite nshiftl_S, IHn; auto. + simpl; rewrite IHn; auto. Qed. Lemma firstr_firstl : - forall x, firstr x = firstl (nshiftl (pred size) x). + forall x, firstr x = firstl (nshiftl x (pred size)). Proof. destruct x; simpl; auto. Qed. Lemma firstl_firstr : - forall x, firstl x = firstr (nshiftr (pred size) x). + forall x, firstl x = firstr (nshiftr x (pred size)). Proof. destruct x; simpl; auto. Qed. @@ -164,23 +163,23 @@ Section Basics. (** More advanced results about [nshiftr] *) Lemma nshiftr_predsize_0_firstl : forall x, - nshiftr (pred size) x = 0 -> firstl x = D0. + nshiftr x (pred size) = 0 -> firstl x = D0. Proof. destruct x; compute; intros H; injection H; intros; subst; auto. Qed. Lemma nshiftr_0_propagates : forall n p x, n <= p -> - nshiftr n x = 0 -> nshiftr p x = 0. + nshiftr x n = 0 -> nshiftr x p = 0. Proof. intros. replace p with ((p-n)+n)%nat by omega. induction (p-n)%nat. simpl; auto. - simpl; rewrite nshiftr_S; rewrite IHn0; auto. + simpl; rewrite IHn0; auto. Qed. Lemma nshiftr_0_firstl : forall n x, n < size -> - nshiftr n x = 0 -> firstl x = D0. + nshiftr x n = 0 -> firstl x = D0. Proof. intros. apply nshiftr_predsize_0_firstl. @@ -197,15 +196,15 @@ Section Basics. forall x, P x. Proof. intros. - assert (forall n, n<=size -> P (nshiftr (size - n) x)). + assert (forall n, n<=size -> P (nshiftr x (size - n))). induction n; intros. rewrite nshiftr_size; auto. rewrite sneakl_shiftr. apply H0. - change (P (nshiftr (S (size - S n)) x)). + change (P (nshiftr x (S (size - S n)))). replace (S (size - S n))%nat with (size - n)%nat by omega. apply IHn; omega. - change x with (nshiftr (size-size) x); auto. + change x with (nshiftr x (size-size)); auto. Qed. Lemma int31_ind_twice : forall P : int31->Prop, @@ -236,19 +235,19 @@ Section Basics. Lemma recr_aux_converges : forall n p x, n <= size -> n <= p -> - recr_aux n A case0 caserec (nshiftr (size - n) x) = - recr_aux p A case0 caserec (nshiftr (size - n) x). + recr_aux n A case0 caserec (nshiftr x (size - n)) = + recr_aux p A case0 caserec (nshiftr x (size - n)). Proof. induction n. - simpl; intros. + simpl minus; intros. rewrite nshiftr_size; destruct p; simpl; auto. intros. destruct p. inversion H0. unfold recr_aux; fold recr_aux. - destruct (iszero (nshiftr (size - S n) x)); auto. + destruct (iszero (nshiftr x (size - S n))); auto. f_equal. - change (shiftr (nshiftr (size - S n) x)) with (nshiftr (S (size - S n)) x). + change (shiftr (nshiftr x (size - S n))) with (nshiftr x (S (size - S n))). replace (S (size - S n))%nat with (size - n)%nat by omega. apply IHn; auto with arith. Qed. @@ -259,7 +258,7 @@ Section Basics. Proof. intros. unfold recr. - change x with (nshiftr (size - size) x). + change x with (nshiftr x (size - size)). rewrite (recr_aux_converges size (S size)); auto with arith. rewrite recr_aux_eqn; auto. Qed. @@ -436,22 +435,22 @@ Section Basics. Lemma phibis_aux_bounded : forall n x, n <= size -> - (phibis_aux n (nshiftr (size-n) x) < 2 ^ (Z.of_nat n))%Z. + (phibis_aux n (nshiftr x (size-n)) < 2 ^ (Z.of_nat n))%Z. Proof. induction n. - simpl; unfold phibis_aux; simpl; auto with zarith. + simpl minus; unfold phibis_aux; simpl; auto with zarith. intros. unfold phibis_aux, recrbis_aux; fold recrbis_aux; - fold (phibis_aux n (shiftr (nshiftr (size - S n) x))). - assert (shiftr (nshiftr (size - S n) x) = nshiftr (size-n) x). + fold (phibis_aux n (shiftr (nshiftr x (size - S n)))). + assert (shiftr (nshiftr x (size - S n)) = nshiftr x (size-n)). replace (size - n)%nat with (S (size - (S n))) by omega. simpl; auto. rewrite H0. assert (H1 : n <= size) by omega. specialize (IHn x H1). - set (y:=phibis_aux n (nshiftr (size - n) x)) in *. + set (y:=phibis_aux n (nshiftr x (size - n))) in *. rewrite Nat2Z.inj_succ, Z.pow_succ_r; auto with zarith. - case_eq (firstr (nshiftr (size - S n) x)); intros. + case_eq (firstr (nshiftr x (size - S n))); intros. rewrite Z.double_spec; auto with zarith. rewrite Z.succ_double_spec; auto with zarith. Qed. @@ -462,12 +461,12 @@ Section Basics. rewrite <- phibis_aux_equiv. split. apply phibis_aux_pos. - change x with (nshiftr (size-size) x). + change x with (nshiftr x (size-size)). apply phibis_aux_bounded; auto. Qed. Lemma phibis_aux_lowerbound : - forall n x, firstr (nshiftr n x) = D1 -> + forall n x, firstr (nshiftr x n) = D1 -> (2 ^ Z.of_nat n <= phibis_aux (S n) x)%Z. Proof. induction n. @@ -509,7 +508,7 @@ Section Basics. (** After killing [n] bits at the left, are the numbers equal ?*) Definition EqShiftL n x y := - nshiftl n x = nshiftl n y. + nshiftl x n = nshiftl y n. Lemma EqShiftL_zero : forall x y, EqShiftL O x y <-> x = y. Proof. @@ -529,7 +528,7 @@ Section Basics. remember (k'-k)%nat as n. clear Heqn H k'. induction n; simpl; auto. - rewrite 2 nshiftl_S; f_equal; auto. + f_equal; auto. Qed. Lemma EqShiftL_firstr : forall k x y, k < size -> @@ -601,7 +600,7 @@ Section Basics. end. Lemma i2l_nshiftl : forall n x, n<=size -> - i2l (nshiftl n x) = cstlist _ D0 n ++ firstn (size-n) (i2l x). + i2l (nshiftl x n) = cstlist _ D0 n ++ firstn (size-n) (i2l x). Proof. induction n. intros. @@ -618,13 +617,13 @@ Section Basics. rewrite <- app_comm_cons; f_equal. rewrite IHn; [ | omega]. rewrite removelast_app. - f_equal. + apply f_equal. replace (size-n)%nat with (S (size - S n))%nat by omega. rewrite removelast_firstn; auto. rewrite i2l_length; omega. generalize (firstn_length (size-n) (i2l x)). rewrite i2l_length. - intros H0 H1; rewrite H1 in H0. + intros H0 H1. rewrite H1 in H0. rewrite min_l in H0 by omega. simpl length in H0. omega. @@ -636,7 +635,7 @@ Section Basics. EqShiftL k x y <-> firstn (size-k) (i2l x) = firstn (size-k) (i2l y). Proof. intros. - destruct (le_lt_dec size k). + destruct (le_lt_dec size k) as [Hle|Hlt]. split; intros. replace (size-k)%nat with O by omega. unfold firstn; auto. @@ -645,24 +644,24 @@ Section Basics. unfold EqShiftL. assert (k <= size) by omega. split; intros. - assert (i2l (nshiftl k x) = i2l (nshiftl k y)) by (f_equal; auto). + assert (i2l (nshiftl x k) = i2l (nshiftl y k)) by (f_equal; auto). rewrite 2 i2l_nshiftl in H1; auto. eapply app_inv_head; eauto. - assert (i2l (nshiftl k x) = i2l (nshiftl k y)). + assert (i2l (nshiftl x k) = i2l (nshiftl y k)). rewrite 2 i2l_nshiftl; auto. f_equal; auto. - rewrite <- (l2i_i2l (nshiftl k x)), <- (l2i_i2l (nshiftl k y)). + rewrite <- (l2i_i2l (nshiftl x k)), <- (l2i_i2l (nshiftl y k)). f_equal; auto. Qed. - (** This equivalence allows to prove easily the following delicate + (** This equivalence allows proving easily the following delicate result *) Lemma EqShiftL_twice_plus_one : forall k x y, EqShiftL k (twice_plus_one x) (twice_plus_one y) <-> EqShiftL (S k) x y. Proof. intros. - destruct (le_lt_dec size k). + destruct (le_lt_dec size k) as [Hle|Hlt]. split; intros; apply EqShiftL_size; auto. rewrite 2 EqShiftL_i2l. @@ -685,7 +684,7 @@ Section Basics. EqShiftL (S k) (shiftr x) (shiftr y). Proof. intros. - destruct (le_lt_dec size (S k)). + destruct (le_lt_dec size (S k)) as [Hle|Hlt]. apply EqShiftL_size; auto. case_eq (firstr x); intros. rewrite <- EqShiftL_twice. @@ -819,30 +818,30 @@ Section Basics. Lemma phi_inv_phi_aux : forall n x, n <= size -> - phi_inv (phibis_aux n (nshiftr (size-n) x)) = - nshiftr (size-n) x. + phi_inv (phibis_aux n (nshiftr x (size-n))) = + nshiftr x (size-n). Proof. induction n. - intros; simpl. + intros; simpl minus. rewrite nshiftr_size; auto. intros. unfold phibis_aux, recrbis_aux; fold recrbis_aux; - fold (phibis_aux n (shiftr (nshiftr (size-S n) x))). - assert (shiftr (nshiftr (size - S n) x) = nshiftr (size-n) x). + fold (phibis_aux n (shiftr (nshiftr x (size-S n)))). + assert (shiftr (nshiftr x (size - S n)) = nshiftr x (size-n)). replace (size - n)%nat with (S (size - (S n))); auto; omega. rewrite H0. - case_eq (firstr (nshiftr (size - S n) x)); intros. + case_eq (firstr (nshiftr x (size - S n))); intros. rewrite phi_inv_double. rewrite IHn by omega. rewrite <- H0. - remember (nshiftr (size - S n) x) as y. + remember (nshiftr x (size - S n)) as y. destruct y; simpl in H1; rewrite H1; auto. rewrite phi_inv_double_plus_one. rewrite IHn by omega. rewrite <- H0. - remember (nshiftr (size - S n) x) as y. + remember (nshiftr x (size - S n)) as y. destruct y; simpl in H1; rewrite H1; auto. Qed. @@ -850,7 +849,7 @@ Section Basics. Proof. intros. rewrite <- phibis_aux_equiv. - replace x with (nshiftr (size - size) x) by auto. + replace x with (nshiftr x (size - size)) by auto. apply phi_inv_phi_aux; auto. Qed. @@ -875,28 +874,28 @@ Section Basics. end. Lemma p2ibis_bounded : forall n p, - nshiftr n (snd (p2ibis n p)) = 0. + nshiftr (snd (p2ibis n p)) n = 0. Proof. induction n. simpl; intros; auto. - simpl; intros. - destruct p; simpl. + simpl p2ibis; intros. + destruct p; simpl snd. specialize IHn with p. - destruct (p2ibis n p); simpl in *. + destruct (p2ibis n p). simpl @snd in *. rewrite nshiftr_S_tail. - destruct (le_lt_dec size n). + destruct (le_lt_dec size n) as [Hle|Hlt]. rewrite nshiftr_above_size; auto. - assert (H:=nshiftr_0_firstl _ _ l IHn). + assert (H:=nshiftr_0_firstl _ _ Hlt IHn). replace (shiftr (twice_plus_one i)) with i; auto. - destruct i; simpl in *; rewrite H; auto. + destruct i; simpl in *. rewrite H; auto. specialize IHn with p. - destruct (p2ibis n p); simpl in *. + destruct (p2ibis n p); simpl @snd in *. rewrite nshiftr_S_tail. - destruct (le_lt_dec size n). + destruct (le_lt_dec size n) as [Hle|Hlt]. rewrite nshiftr_above_size; auto. - assert (H:=nshiftr_0_firstl _ _ l IHn). + assert (H:=nshiftr_0_firstl _ _ Hlt IHn). replace (shiftr (twice i)) with i; auto. destruct i; simpl in *; rewrite H; auto. @@ -946,7 +945,7 @@ Section Basics. intros. simpl p2ibis; destruct p; [ | | red; auto]; specialize IHn with p; - destruct (p2ibis n p); simpl snd in *; simpl phi_inv_positive; + destruct (p2ibis n p); simpl @snd in *; simpl phi_inv_positive; rewrite ?EqShiftL_twice_plus_one, ?EqShiftL_twice; replace (S (size - S n))%nat with (size - n)%nat by omega; apply IHn; omega. @@ -1158,7 +1157,10 @@ Instance int31_ops : ZnZ.Ops int31 := fun i => let (_,r) := i/2 in match r ?= 0 with Eq => true | _ => false end; sqrt2 := sqrt312; - sqrt := sqrt31 + sqrt := sqrt31; + lor := lor31; + land := land31; + lxor := lxor31 }. Section Int31_Specs. @@ -1175,10 +1177,10 @@ Section Int31_Specs. Qed. Notation "[+| c |]" := - (interp_carry 1 wB phi c) (at level 0, x at level 99). + (interp_carry 1 wB phi c) (at level 0, c at level 99). Notation "[-| c |]" := - (interp_carry (-1) wB phi c) (at level 0, x at level 99). + (interp_carry (-1) wB phi c) (at level 0, c at level 99). Notation "[|| x ||]" := (zn2z_to_Z wB phi x) (at level 0, x at level 99). @@ -1412,7 +1414,7 @@ Section Int31_Specs. generalize (phi_bounded a1)(phi_bounded a2)(phi_bounded b); intros. assert ([|b|]>0) by (auto with zarith). generalize (Z_div_mod (phi2 a1 a2) [|b|] H4) (Z_div_pos (phi2 a1 a2) [|b|] H4). - unfold Z.div; destruct (Z.div_eucl (phi2 a1 a2) [|b|]); simpl. + unfold Z.div; destruct (Z.div_eucl (phi2 a1 a2) [|b|]). rewrite ?phi_phi_inv. destruct 1; intros. unfold phi2 in *. @@ -1442,7 +1444,7 @@ Section Int31_Specs. unfold div31; intros. assert ([|b|]>0) by (auto with zarith). generalize (Z_div_mod [|a|] [|b|] H0) (Z_div_pos [|a|] [|b|] H0). - unfold Z.div; destruct (Z.div_eucl [|a|] [|b|]); simpl. + unfold Z.div; destruct (Z.div_eucl [|a|] [|b|]). rewrite ?phi_phi_inv. destruct 1; intros. rewrite H1, Z.mul_comm. @@ -1465,7 +1467,7 @@ Section Int31_Specs. assert ([|b|]>0) by (auto with zarith). unfold Z.modulo. generalize (Z_div_mod [|a|] [|b|] H0). - destruct (Z.div_eucl [|a|] [|b|]); simpl. + destruct (Z.div_eucl [|a|] [|b|]). rewrite ?phi_phi_inv. destruct 1; intros. generalize (phi_bounded b); intros. @@ -1478,15 +1480,14 @@ Section Int31_Specs. unfold gcd31. induction (2*size)%nat; intros. reflexivity. - simpl. + simpl euler. unfold compare31. change [|On|] with 0. generalize (phi_bounded j)(phi_bounded i); intros. case_eq [|j|]; intros. simpl; intros. generalize (Zabs_spec [|i|]); omega. - simpl. - rewrite IHn, H1; f_equal. + simpl. rewrite IHn, H1; f_equal. rewrite spec_mod, H1; auto. rewrite H1; compute; auto. rewrite H1 in H; destruct H as [H _]; compute in H; elim H; auto. @@ -1519,17 +1520,17 @@ Section Int31_Specs. simpl; auto. simpl; intros. case_eq (firstr i); intros H; rewrite 2 IHn; - unfold phibis_aux; simpl; rewrite H; fold (phibis_aux n (shiftr i)); + unfold phibis_aux; simpl; rewrite ?H; fold (phibis_aux n (shiftr i)); generalize (phibis_aux_pos n (shiftr i)); intros; set (z := phibis_aux n (shiftr i)) in *; clearbody z; - rewrite <- iter_nat_plus. + rewrite <- nat_rect_plus. f_equal. rewrite Z.double_spec, <- Z.add_diag. symmetry; apply Zabs2Nat.inj_add; auto with zarith. - change (iter_nat (S (Z.abs_nat z + Z.abs_nat z)) A f a = - iter_nat (Z.abs_nat (Z.succ_double z)) A f a); f_equal. + change (iter_nat (S (Z.abs_nat z) + (Z.abs_nat z))%nat A f a = + iter_nat (Z.abs_nat (Z.succ_double z)) A f a); f_equal. rewrite Z.succ_double_spec, <- Z.add_diag. rewrite Zabs2Nat.inj_add; auto with zarith. rewrite Zabs2Nat.inj_add; auto with zarith. @@ -1554,7 +1555,7 @@ Section Int31_Specs. intros. simpl addmuldiv31_alt. replace (S n) with (n+1)%nat by (rewrite plus_comm; auto). - rewrite iter_nat_plus; simpl; auto. + rewrite nat_rect_plus; simpl; auto. Qed. Lemma spec_add_mul_div : forall x y p, [|p|] <= Zpos 31 -> @@ -1573,10 +1574,9 @@ Section Int31_Specs. clear p H; revert x y. induction n. - simpl; intros. - change (Z.pow_pos 2 31) with (2^31). + simpl Z.of_nat; intros. rewrite Z.mul_1_r. - replace ([|y|] / 2^31) with 0. + replace ([|y|] / 2^(31-0)) with 0. rewrite Z.add_0_r. symmetry; apply Zmod_small; apply phi_bounded. symmetry; apply Zdiv_small; apply phi_bounded. @@ -1627,7 +1627,7 @@ Section Int31_Specs. Lemma spec_pos_mod : forall w p, [|ZnZ.pos_mod p w|] = [|w|] mod (2 ^ [|p|]). Proof. - unfold ZnZ.pos_mod, int31_ops, compare31. + unfold int31_ops, ZnZ.pos_mod, compare31. change [|31|] with 31%Z. assert (forall w p, 31<=p -> [|w|] = [|w|] mod 2^p). intros. @@ -1664,7 +1664,7 @@ Section Int31_Specs. Proof. intros. generalize (phi_inv_phi x). - rewrite H; simpl. + rewrite H; simpl phi_inv. intros H'; rewrite <- H'. simpl; auto. Qed. @@ -1739,7 +1739,7 @@ Section Int31_Specs. Proof. intros. rewrite head031_equiv. - assert (nshiftl size x = 0%int31). + assert (nshiftl x size = 0%int31). apply nshiftl_size. revert x H H0. unfold size at 2 5. @@ -1772,7 +1772,7 @@ Section Int31_Specs. Proof. intros. generalize (phi_inv_phi x). - rewrite H; simpl. + rewrite H; simpl phi_inv. intros H'; rewrite <- H'. simpl; auto. Qed. @@ -1837,7 +1837,7 @@ Section Int31_Specs. Proof. intros. rewrite tail031_equiv. - assert (nshiftr size x = 0%int31). + assert (nshiftr x size = 0%int31). apply nshiftr_size. revert x H H0. induction size. @@ -1957,7 +1957,7 @@ Section Int31_Specs. Lemma div31_phi i j: 0 < [|j|] -> [|fst (i/j)%int31|] = [|i|]/[|j|]. intros Hj; generalize (spec_div i j Hj). - case div31; intros q r; simpl fst. + case div31; intros q r; simpl @fst. intros (H1,H2); apply Zdiv_unique with [|r|]; auto with zarith. rewrite H1; ring. Qed. @@ -2092,7 +2092,7 @@ Section Int31_Specs. generalize (spec_div21 ih il j Hj Hj1). case div3121; intros q r (Hq, Hr). apply Zdiv_unique with (phi r); auto with zarith. - simpl fst; apply eq_trans with (1 := Hq); ring. + simpl @fst; apply eq_trans with (1 := Hq); ring. Qed. Lemma sqrt312_step_correct rec ih il j: @@ -2119,7 +2119,7 @@ Section Int31_Specs. unfold phi2; rewrite Hc1. assert (0 <= [|il|]/[|j|]) by (apply Z_div_pos; auto with zarith). rewrite Z.mul_comm, Z_div_plus_full_l; unfold base; auto with zarith. - unfold Z.pow, Z.pow_pos in Hj1; simpl in Hj1; auto with zarith. + simpl wB in Hj1. unfold Z.pow_pos in Hj1. simpl in Hj1. auto with zarith. case (Z.le_gt_cases (2 ^ 30) [|j|]); intros Hjj. rewrite spec_compare; case Z.compare_spec; rewrite div312_phi; auto; intros Hc; @@ -2213,6 +2213,9 @@ Section Int31_Specs. apply Nat2Z.is_nonneg. Qed. + (* Avoid expanding [iter312_sqrt] before variables in the context. *) + Strategy 1 [iter312_sqrt]. + Lemma spec_sqrt2 : forall x y, wB/ 4 <= [|x|] -> let (s,r) := sqrt312 x y in @@ -2230,7 +2233,7 @@ Section Int31_Specs. 2: simpl; unfold Z.pow_pos; simpl; auto with zarith. case (phi_bounded ih); case (phi_bounded il); intros H1 H2 H3 H4. unfold base, Z.pow, Z.pow_pos in H2,H4; simpl in H2,H4. - unfold phi2,Z.pow, Z.pow_pos. simpl Pos.iter; auto with zarith. } + unfold phi2. cbn [Z.pow Z.pow_pos Pos.iter]. auto with zarith. } case (iter312_sqrt_correct 31 (fun _ _ j => j) ih il Tn); auto with zarith. change [|Tn|] with 2147483647; auto with zarith. intros j1 _ HH; contradict HH. @@ -2255,9 +2258,8 @@ Section Int31_Specs. intros Hihl1. generalize (spec_sub_c il il1). case sub31c; intros il2 Hil2. - simpl interp_carry in Hil2. rewrite spec_compare; case Z.compare_spec. - unfold interp_carry. + unfold interp_carry in *. intros H1; split. rewrite Z.pow_2_r, <- Hihl1. unfold phi2; ring[Hil2 H1]. @@ -2274,7 +2276,7 @@ Section Int31_Specs. rewrite Z.mul_add_distr_r, Z.add_0_r; auto with zarith. case (phi_bounded il1); intros H3 _. apply Z.add_le_mono; auto with zarith. - unfold interp_carry; change (1 * 2 ^ Z.of_nat size) with base. + unfold interp_carry in *; change (1 * 2 ^ Z.of_nat size) with base. rewrite Z.pow_2_r, <- Hihl1, Hil2. intros H1. rewrite <- Z.le_succ_l, <- Z.add_1_r in H1. @@ -2378,8 +2380,8 @@ Qed. Lemma spec_eq0 : forall x, ZnZ.eq0 x = true -> [|x|] = 0. Proof. - clear; unfold ZnZ.eq0; simpl. - unfold compare31; simpl; intros. + clear; unfold ZnZ.eq0, int31_ops. + unfold compare31; intros. change [|0|] with 0 in H. apply Z.compare_eq. now destruct ([|x|] ?= 0). @@ -2390,7 +2392,7 @@ Qed. Lemma spec_is_even : forall x, if ZnZ.is_even x then [|x|] mod 2 = 0 else [|x|] mod 2 = 1. Proof. - unfold ZnZ.is_even; simpl; intros. + unfold ZnZ.is_even, int31_ops; intros. generalize (spec_div x 2). destruct (x/2)%int31 as (q,r); intros. unfold compare31. @@ -2403,6 +2405,51 @@ Qed. apply Zmod_unique with [|q|]; auto with zarith. Qed. + (* Bitwise *) + + Lemma log2_phi_bounded x : Z.log2 [|x|] < Z.of_nat size. + Proof. + destruct (phi_bounded x) as (H,H'). + Z.le_elim H. + - now apply Z.log2_lt_pow2. + - now rewrite <- H. + Qed. + + Lemma spec_lor x y : [| ZnZ.lor x y |] = Z.lor [|x|] [|y|]. + Proof. + unfold ZnZ.lor,int31_ops. unfold lor31. + rewrite phi_phi_inv. + apply Z.mod_small; split; trivial. + - apply Z.lor_nonneg; split; apply phi_bounded. + - apply Z.log2_lt_cancel. rewrite Z.log2_pow2 by easy. + rewrite Z.log2_lor; try apply phi_bounded. + apply Z.max_lub_lt; apply log2_phi_bounded. + Qed. + + Lemma spec_land x y : [| ZnZ.land x y |] = Z.land [|x|] [|y|]. + Proof. + unfold ZnZ.land, int31_ops. unfold land31. + rewrite phi_phi_inv. + apply Z.mod_small; split; trivial. + - apply Z.land_nonneg; left; apply phi_bounded. + - apply Z.log2_lt_cancel. rewrite Z.log2_pow2 by easy. + eapply Z.le_lt_trans. + apply Z.log2_land; try apply phi_bounded. + apply Z.min_lt_iff; left; apply log2_phi_bounded. + Qed. + + Lemma spec_lxor x y : [| ZnZ.lxor x y |] = Z.lxor [|x|] [|y|]. + Proof. + unfold ZnZ.lxor, int31_ops. unfold lxor31. + rewrite phi_phi_inv. + apply Z.mod_small; split; trivial. + - apply Z.lxor_nonneg; split; intros; apply phi_bounded. + - apply Z.log2_lt_cancel. rewrite Z.log2_pow2 by easy. + eapply Z.le_lt_trans. + apply Z.log2_lxor; try apply phi_bounded. + apply Z.max_lub_lt; apply log2_phi_bounded. + Qed. + Global Instance int31_specs : ZnZ.Specs int31_ops := { spec_to_Z := phi_bounded; spec_of_pos := positive_to_int31_spec; @@ -2446,7 +2493,10 @@ Qed. spec_pos_mod := spec_pos_mod; spec_is_even := spec_is_even; spec_sqrt2 := spec_sqrt2; - spec_sqrt := spec_sqrt }. + spec_sqrt := spec_sqrt; + spec_lor := spec_lor; + spec_land := spec_land; + spec_lxor := spec_lxor }. End Int31_Specs. diff --git a/theories/Numbers/Cyclic/Int31/Int31.v b/theories/Numbers/Cyclic/Int31/Int31.v index 73f2816a..4e28b5b9 100644 --- a/theories/Numbers/Cyclic/Int31/Int31.v +++ b/theories/Numbers/Cyclic/Int31/Int31.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -335,6 +335,11 @@ Definition addmuldiv31 p i j := in res. +(** Bitwise operations *) + +Definition lor31 n m := phi_inv (Z.lor (phi n) (phi m)). +Definition land31 n m := phi_inv (Z.land (phi n) (phi m)). +Definition lxor31 n m := phi_inv (Z.lxor (phi n) (phi m)). Register add31 as int31 plus in "coq_int31" by True. Register add31c as int31 plusc in "coq_int31" by True. @@ -345,9 +350,15 @@ Register sub31carryc as int31 minuscarryc in "coq_int31" by True. Register mul31 as int31 times in "coq_int31" by True. Register mul31c as int31 timesc in "coq_int31" by True. Register div3121 as int31 div21 in "coq_int31" by True. -Register div31 as int31 div in "coq_int31" by True. +Register div31 as int31 diveucl in "coq_int31" by True. Register compare31 as int31 compare in "coq_int31" by True. Register addmuldiv31 as int31 addmuldiv in "coq_int31" by True. +Register lor31 as int31 lor in "coq_int31" by True. +Register land31 as int31 land in "coq_int31" by True. +Register lxor31 as int31 lxor in "coq_int31" by True. + +Definition lnot31 n := lxor31 Tn n. +Definition ldiff31 n m := land31 n (lnot31 m). Fixpoint euler (guard:nat) (i j:int31) {struct guard} := match guard with diff --git a/theories/Numbers/Cyclic/Int31/Ring31.v b/theories/Numbers/Cyclic/Int31/Ring31.v index b2857256..4fde3f53 100644 --- a/theories/Numbers/Cyclic/Int31/Ring31.v +++ b/theories/Numbers/Cyclic/Int31/Ring31.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/theories/Numbers/Cyclic/ZModulo/ZModulo.v b/theories/Numbers/Cyclic/ZModulo/ZModulo.v index 673e4b1c..b93b4eb3 100644 --- a/theories/Numbers/Cyclic/ZModulo/ZModulo.v +++ b/theories/Numbers/Cyclic/ZModulo/ZModulo.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -38,10 +38,10 @@ Section ZModulo. Notation "[| x |]" := (to_Z x) (at level 0, x at level 99). Notation "[+| c |]" := - (interp_carry 1 wB to_Z c) (at level 0, x at level 99). + (interp_carry 1 wB to_Z c) (at level 0, c at level 99). Notation "[-| c |]" := - (interp_carry (-1) wB to_Z c) (at level 0, x at level 99). + (interp_carry (-1) wB to_Z c) (at level 0, c at level 99). Notation "[|| x ||]" := (zn2z_to_Z wB to_Z x) (at level 0, x at level 99). @@ -466,8 +466,8 @@ Section ZModulo. generalize (Zgcd_is_gcd a b); inversion_clear 1. destruct H2 as (q,H2); destruct H3 as (q',H3); clear H4. assert (H4:=Z.gcd_nonneg a b). - destruct (Z.eq_dec (Z.gcd a b) 0). - rewrite e; generalize (Zmax_spec a b); omega. + destruct (Z.eq_dec (Z.gcd a b) 0) as [->|Hneq]. + generalize (Zmax_spec a b); omega. assert (0 <= q). apply Z.mul_le_mono_pos_r with (Z.gcd a b); auto with zarith. destruct (Z.eq_dec q 0). @@ -796,6 +796,40 @@ Section ZModulo. exists 0; simpl; auto with zarith. Qed. + Definition lor := Z.lor. + Definition land := Z.land. + Definition lxor := Z.lxor. + + Lemma spec_lor x y : [|lor x y|] = Z.lor [|x|] [|y|]. + Proof. + unfold lor, to_Z. + apply Z.bits_inj'; intros n Hn. rewrite Z.lor_spec. + unfold wB, base. + destruct (Z.le_gt_cases (Z.pos digits) n). + - rewrite !Z.mod_pow2_bits_high; auto with zarith. + - rewrite !Z.mod_pow2_bits_low, Z.lor_spec; auto with zarith. + Qed. + + Lemma spec_land x y : [|land x y|] = Z.land [|x|] [|y|]. + Proof. + unfold land, to_Z. + apply Z.bits_inj'; intros n Hn. rewrite Z.land_spec. + unfold wB, base. + destruct (Z.le_gt_cases (Z.pos digits) n). + - rewrite !Z.mod_pow2_bits_high; auto with zarith. + - rewrite !Z.mod_pow2_bits_low, Z.land_spec; auto with zarith. + Qed. + + Lemma spec_lxor x y : [|lxor x y|] = Z.lxor [|x|] [|y|]. + Proof. + unfold lxor, to_Z. + apply Z.bits_inj'; intros n Hn. rewrite Z.lxor_spec. + unfold wB, base. + destruct (Z.le_gt_cases (Z.pos digits) n). + - rewrite !Z.mod_pow2_bits_high; auto with zarith. + - rewrite !Z.mod_pow2_bits_low, Z.lxor_spec; auto with zarith. + Qed. + (** Let's now group everything in two records *) Instance zmod_ops : ZnZ.Ops Z := ZnZ.MkOps @@ -849,7 +883,10 @@ Section ZModulo. (is_even : t -> bool) (sqrt2 : t -> t -> t * carry t) - (sqrt : t -> t). + (sqrt : t -> t) + (lor : t -> t -> t) + (land : t -> t -> t) + (lxor : t -> t -> t). Instance zmod_specs : ZnZ.Specs zmod_ops := ZnZ.MkSpecs spec_to_Z @@ -906,7 +943,10 @@ Section ZModulo. spec_is_even spec_sqrt2 - spec_sqrt. + spec_sqrt + spec_lor + spec_land + spec_lxor. End ZModulo. @@ -922,4 +962,3 @@ Module ZModuloCyclicType (P:PositiveNotOne) <: CyclicType. Instance ops : ZnZ.Ops t := zmod_ops P.p. Instance specs : ZnZ.Specs ops := zmod_specs P.not_one. End ZModuloCyclicType. - |