diff options
Diffstat (limited to 'theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v')
| -rw-r--r-- | theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v | 164 |
1 files changed, 136 insertions, 28 deletions
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}. |