diff options
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Numbers/Cyclic/Abstract/CyclicAxioms.v | 70 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v | 140 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/Int31/Cyclic31.v | 54 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/ZModulo/ZModulo.v | 39 | ||||
| -rw-r--r-- | theories/Numbers/Natural/BigN/NMake_gen.ml | 15 |
5 files changed, 113 insertions, 205 deletions
diff --git a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v index ed099a1fd..b7a427532 100644 --- a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v +++ b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v @@ -40,13 +40,10 @@ Section Z_nZ_Op. znz_head0 : znz -> znz; (* number of digits 0 in front of the number *) znz_tail0 : znz -> znz; (* number of digits 0 at the bottom of the number *) - (* Basic constructors *) + (* Basic numbers *) znz_0 : znz; znz_1 : znz; znz_Bm1 : znz; (* [2^digits-1], which is equivalent to [-1] *) - znz_WW : znz -> znz -> zn2z znz; (* from high and low words to a double word *) - znz_W0 : znz -> zn2z znz; (* same, with null low word *) - znz_0W : znz -> zn2z znz; (* same, with null high word *) (* Comparison *) znz_compare : znz -> znz -> comparison; @@ -77,13 +74,13 @@ Section Z_nZ_Op. (* Special divisions operations *) znz_div21 : znz -> znz -> znz -> znz*znz; - znz_div_gt : znz -> znz -> znz * znz; (* why this one ? *) + znz_div_gt : znz -> znz -> znz * znz; (* specialized version of [znz_div] *) znz_div : znz -> znz -> znz * znz; - znz_mod_gt : znz -> znz -> znz; (* why this one ? *) + znz_mod_gt : znz -> znz -> znz; (* specialized version of [znz_mod] *) znz_mod : znz -> znz -> znz; - znz_gcd_gt : znz -> znz -> znz; (* why this one ? *) + znz_gcd_gt : znz -> znz -> znz; (* specialized version of [znz_gcd] *) znz_gcd : znz -> znz -> znz; (* [znz_add_mul_div p i j] is a combination of the [(digits-p)] low bits of [i] above the [p] high bits of [j]: @@ -114,10 +111,6 @@ Section Z_nZ_Spec. Let w1 := w_op.(znz_1). Let wBm1 := w_op.(znz_Bm1). - Let wWW := w_op.(znz_WW). - Let w0W := w_op.(znz_0W). - Let wW0 := w_op.(znz_W0). - Let w_compare := w_op.(znz_compare). Let w_eq0 := w_op.(znz_eq0). @@ -183,13 +176,10 @@ Section Z_nZ_Spec. spec_zdigits : [| w_zdigits |] = Zpos w_digits; spec_more_than_1_digit: 1 < Zpos w_digits; - (* Basic constructors *) + (* Basic numbers *) spec_0 : [|w0|] = 0; spec_1 : [|w1|] = 1; spec_Bm1 : [|wBm1|] = wB - 1; - spec_WW : forall h l, [||wWW h l||] = [|h|] * wB + [|l|]; - spec_0W : forall l, [||w0W l||] = [|l|]; - spec_W0 : forall h, [||wW0 h||] = [|h|]*wB; (* Comparison *) spec_compare : @@ -279,7 +269,57 @@ Section Z_nZ_Spec. End Z_nZ_Spec. +(** Generic construction of double words *) + +Section WW. + + Variable w : Type. + Variable w_op : znz_op w. + Variable op_spec : znz_spec w_op. + + Let wB := base w_op.(znz_digits). + Let w_to_Z := w_op.(znz_to_Z). + Let w_eq0 := w_op.(znz_eq0). + Let w_0 := w_op.(znz_0). + + Definition znz_W0 h := + if w_eq0 h then W0 else WW h w_0. + + Definition znz_0W l := + if w_eq0 l then W0 else WW w_0 l. + + Definition znz_WW h l := + if w_eq0 h then znz_0W l else WW h l. + + Lemma spec_W0 : forall h, + zn2z_to_Z wB w_to_Z (znz_W0 h) = (w_to_Z h)*wB. + Proof. + unfold zn2z_to_Z, znz_W0, w_to_Z; simpl; intros. + case_eq (w_eq0 h); intros. + rewrite (op_spec.(spec_eq0) _ H); auto. + unfold w_0; rewrite op_spec.(spec_0); auto with zarith. + Qed. + + Lemma spec_0W : forall l, + zn2z_to_Z wB w_to_Z (znz_0W l) = w_to_Z l. + Proof. + unfold zn2z_to_Z, znz_0W, w_to_Z; simpl; intros. + case_eq (w_eq0 l); intros. + rewrite (op_spec.(spec_eq0) _ H); auto. + unfold w_0; rewrite op_spec.(spec_0); auto with zarith. + Qed. + + Lemma spec_WW : forall h l, + zn2z_to_Z wB w_to_Z (znz_WW h l) = (w_to_Z h)*wB + w_to_Z l. + Proof. + unfold znz_WW, w_to_Z; simpl; intros. + case_eq (w_eq0 h); intros. + rewrite (op_spec.(spec_eq0) _ H); auto. + rewrite spec_0W; auto. + simpl; auto. + Qed. +End WW. (** Injecting [Z] numbers into a cyclic structure *) diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v index 0a8b281fb..b590e9b3c 100644 --- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v +++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v @@ -44,10 +44,6 @@ Section Z_2nZ. Let w_1 := w_op.(znz_1). Let w_Bm1 := w_op.(znz_Bm1). - Let w_WW := w_op.(znz_WW). - Let w_W0 := w_op.(znz_W0). - Let w_0W := w_op.(znz_0W). - Let w_compare := w_op.(znz_compare). Let w_eq0 := w_op.(znz_eq0). @@ -109,6 +105,10 @@ Section Z_2nZ. Let to_Z := zn2z_to_Z wB w_to_Z. + Let w_W0 := znz_W0 w_op. + Let w_0W := znz_0W w_op. + Let w_WW := znz_WW w_op. + Let ww_of_pos p := match w_of_pos p with | (N0, l) => (N0, WW w_0 l) @@ -116,7 +116,6 @@ Section Z_2nZ. let (n,h) := w_of_pos ph in (n, w_WW h l) end. - Let head0 := Eval lazy beta delta [ww_head0] in ww_head0 w_0 w_0W w_compare w_head0 w_add2 w_zdigits _ww_zdigits. @@ -292,7 +291,6 @@ Section Z_2nZ. mk_znz_op _ww_digits _ww_zdigits to_Z ww_of_pos head0 tail0 W0 ww_1 ww_Bm1 - ww_WW ww_W0 ww_0W compare eq0 opp_c opp opp_carry succ_c add_c add_carry_c @@ -313,7 +311,6 @@ Section Z_2nZ. mk_znz_op _ww_digits _ww_zdigits to_Z ww_of_pos head0 tail0 W0 ww_1 ww_Bm1 - ww_WW ww_W0 ww_0W compare eq0 opp_c opp opp_carry succ_c add_c add_carry_c @@ -339,9 +336,6 @@ Section Z_2nZ. (spec_0 op_spec) (spec_1 op_spec) (spec_Bm1 op_spec) - (spec_WW op_spec) - (spec_0W op_spec) - (spec_W0 op_spec) (spec_compare op_spec) (spec_eq0 op_spec) (spec_opp_c op_spec) @@ -375,7 +369,12 @@ Section Z_2nZ. (spec_pos_mod) (spec_is_even) (spec_sqrt2) - (spec_sqrt). + (spec_sqrt) + (spec_W0 op_spec) + (spec_0W op_spec) + (spec_WW op_spec). + + Ltac wwauto := unfold ww_to_Z; auto. Let wwB := base _ww_digits. @@ -402,9 +401,10 @@ Section Z_2nZ. simpl;unfold w_to_Z,w_0;rewrite (spec_0 op_spec);trivial. unfold Z_of_N; assert (H:= spec_of_pos op_spec p0); destruct (znz_of_pos w_op p0). simpl in H. - rewrite H;unfold fst, snd,Z_of_N, w_WW, to_Z. - rewrite (spec_WW op_spec). replace wwB with (wB*wB). - unfold wB,w_digits;clear H;destruct n;ring. + rewrite H;unfold fst, snd,Z_of_N, to_Z. + rewrite (spec_WW op_spec). + replace wwB with (wB*wB). + unfold wB,w_to_Z,w_digits;clear H;destruct n;ring. symmetry. rewrite <- Zpower_2; exact (wwB_wBwB w_digits). Qed. @@ -417,27 +417,6 @@ Section Z_2nZ. Let spec_ww_Bm1 : [|ww_Bm1|] = wwB - 1. Proof. refine (spec_ww_Bm1 w_Bm1 w_digits w_to_Z _);auto. Qed. - Let spec_ww_WW : forall h l, [[ww_WW h l]] = [|h|] * wwB + [|l|]. - Proof. - intros h l. replace wwB with (wB*wB). destruct h;simpl. - destruct l;simpl;ring. ring. - symmetry. rewrite <- Zpower_2; exact (wwB_wBwB w_digits). - Qed. - - Let spec_ww_0W : forall l, [[ww_0W l]] = [|l|]. - Proof. - intros l. replace wwB with (wB*wB). - destruct l;simpl;ring. - symmetry. ring_simplify; exact (wwB_wBwB w_digits). - Qed. - - Let spec_ww_W0 : forall h, [[ww_W0 h]] = [|h|]*wwB. - Proof. - intros h. replace wwB with (wB*wB). - destruct h;simpl;ring. - symmetry. ring_simplify; exact (wwB_wBwB w_digits). - Qed. - Let spec_ww_compare : forall x y, match compare x y with @@ -469,7 +448,7 @@ Section Z_2nZ. Let spec_ww_opp_carry : forall x, [|opp_carry x|] = wwB - [|x|] - 1. Proof. refine (spec_ww_opp_carry w_WW ww_Bm1 w_opp_carry w_digits w_to_Z _ _ _); - auto. exact (spec_WW op_spec). + wwauto. Qed. Let spec_ww_succ_c : forall x, [+|succ_c x|] = [|x|] + 1. @@ -479,20 +458,19 @@ Section Z_2nZ. Let spec_ww_add_c : forall x y, [+|add_c x y|] = [|x|] + [|y|]. Proof. - refine (spec_ww_add_c w_WW w_add_c w_add_carry_c w_digits w_to_Z _ _ _);auto. - exact (spec_WW op_spec). + refine (spec_ww_add_c w_WW w_add_c w_add_carry_c w_digits w_to_Z _ _ _);wwauto. Qed. Let spec_ww_add_carry_c : forall x y, [+|add_carry_c x y|] = [|x|]+[|y|]+1. Proof. refine (spec_ww_add_carry_c w_0 w_0 w_WW ww_1 w_succ_c w_add_c w_add_carry_c - w_digits w_to_Z _ _ _ _ _ _ _);auto. exact (spec_WW op_spec). + w_digits w_to_Z _ _ _ _ _ _ _);wwauto. Qed. Let spec_ww_succ : forall x, [|succ x|] = ([|x|] + 1) mod wwB. Proof. refine (spec_ww_succ w_W0 ww_1 w_succ_c w_succ w_digits w_to_Z _ _ _ _ _); - auto. exact (spec_W0 op_spec). + wwauto. Qed. Let spec_ww_add : forall x y, [|add x y|] = ([|x|] + [|y|]) mod wwB. @@ -503,79 +481,70 @@ Section Z_2nZ. Let spec_ww_add_carry : forall x y, [|add_carry x y|]=([|x|]+[|y|]+1)mod wwB. Proof. refine (spec_ww_add_carry w_W0 ww_1 w_succ_c w_add_carry_c w_succ - w_add w_add_carry w_digits w_to_Z _ _ _ _ _ _ _ _);auto. - exact (spec_W0 op_spec). + w_add w_add_carry w_digits w_to_Z _ _ _ _ _ _ _ _);wwauto. Qed. Let spec_ww_pred_c : forall x, [-|pred_c x|] = [|x|] - 1. Proof. refine (spec_ww_pred_c w_0 w_Bm1 w_WW ww_Bm1 w_pred_c w_digits w_to_Z - _ _ _ _ _);auto. exact (spec_WW op_spec). + _ _ _ _ _);wwauto. Qed. Let spec_ww_sub_c : forall x y, [-|sub_c x y|] = [|x|] - [|y|]. Proof. refine (spec_ww_sub_c w_0 w_0 w_WW W0 w_opp_c w_opp_carry w_sub_c - w_sub_carry_c w_digits w_to_Z _ _ _ _ _ _ _);auto. exact (spec_WW op_spec). + w_sub_carry_c w_digits w_to_Z _ _ _ _ _ _ _);wwauto. Qed. Let spec_ww_sub_carry_c : forall x y, [-|sub_carry_c x y|] = [|x|]-[|y|]-1. Proof. refine (spec_ww_sub_carry_c w_0 w_Bm1 w_WW ww_Bm1 w_opp_carry w_pred_c - w_sub_c w_sub_carry_c w_digits w_to_Z _ _ _ _ _ _ _ _);auto. - exact (spec_WW op_spec). + w_sub_c w_sub_carry_c w_digits w_to_Z _ _ _ _ _ _ _ _);wwauto. Qed. Let spec_ww_pred : forall x, [|pred x|] = ([|x|] - 1) mod wwB. Proof. refine (spec_ww_pred w_0 w_Bm1 w_WW ww_Bm1 w_pred_c w_pred w_digits w_to_Z - _ _ _ _ _ _);auto. exact (spec_WW op_spec). + _ _ _ _ _ _);wwauto. Qed. Let spec_ww_sub : forall x y, [|sub x y|] = ([|x|] - [|y|]) mod wwB. Proof. refine (spec_ww_sub w_0 w_0 w_WW W0 w_opp_c w_opp_carry w_sub_c w_opp - w_sub w_sub_carry w_digits w_to_Z _ _ _ _ _ _ _ _ _);auto. - exact (spec_WW op_spec). + w_sub w_sub_carry w_digits w_to_Z _ _ _ _ _ _ _ _ _);wwauto. Qed. Let spec_ww_sub_carry : forall x y, [|sub_carry x y|]=([|x|]-[|y|]-1) mod wwB. Proof. refine (spec_ww_sub_carry w_0 w_Bm1 w_WW ww_Bm1 w_opp_carry w_pred_c w_sub_carry_c w_pred w_sub w_sub_carry w_digits w_to_Z _ _ _ _ _ _ _ _ _ _); - auto. exact (spec_WW op_spec). + wwauto. Qed. Let spec_ww_mul_c : forall x y, [[mul_c x y ]] = [|x|] * [|y|]. Proof. refine (spec_ww_mul_c w_0 w_1 w_WW w_W0 w_mul_c add_c add add_carry w_digits - w_to_Z _ _ _ _ _ _ _ _ _);auto. exact (spec_WW op_spec). - exact (spec_W0 op_spec). exact (spec_mul_c op_spec). + w_to_Z _ _ _ _ _ _ _ _ _);wwauto. Qed. Let spec_ww_karatsuba_c : forall x y, [[karatsuba_c x y ]] = [|x|] * [|y|]. Proof. refine (spec_ww_karatsuba_c _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ - _ _ _ _ _ _ _ _ _ _ _ _); auto. + _ _ _ _ _ _ _ _ _ _ _ _); wwauto. unfold w_digits; apply spec_more_than_1_digit; auto. - exact (spec_WW op_spec). - exact (spec_W0 op_spec). exact (spec_compare op_spec). - exact (spec_mul_c op_spec). Qed. Let spec_ww_mul : forall x y, [|mul x y|] = ([|x|] * [|y|]) mod wwB. Proof. refine (spec_ww_mul w_W0 w_add w_mul_c w_mul add w_digits w_to_Z _ _ _ _ _); - auto. exact (spec_W0 op_spec). exact (spec_mul_c op_spec). + wwauto. Qed. Let spec_ww_square_c : forall x, [[square_c x]] = [|x|] * [|x|]. Proof. refine (spec_ww_square_c w_0 w_1 w_WW w_W0 w_mul_c w_square_c add_c add - add_carry w_digits w_to_Z _ _ _ _ _ _ _ _ _ _);auto. - exact (spec_WW op_spec). exact (spec_W0 op_spec). - exact (spec_mul_c op_spec). exact (spec_square_c op_spec). + add_carry w_digits w_to_Z _ _ _ _ _ _ _ _ _ _);wwauto. Qed. Let spec_w_div32 : forall a1 a2 a3 b1 b2, @@ -588,13 +557,13 @@ Section Z_2nZ. Proof. refine (spec_w_div32 w_0 w_Bm1 w_Bm2 w_WW w_compare w_add_c w_add_carry_c w_add w_add_carry w_pred w_sub w_mul_c w_div21 sub_c w_digits w_to_Z - _ _ _ _ _ _ _ _ _ _ _ _ _ _ _);auto. + _ _ _ _ _ _ _ _ _ _ _ _ _ _ _);wwauto. unfold w_Bm2, w_to_Z, w_pred, w_Bm1. rewrite (spec_pred op_spec);rewrite (spec_Bm1 op_spec). unfold w_digits;rewrite Zmod_small. ring. assert (H:= wB_pos(znz_digits w_op)). omega. - exact (spec_WW op_spec). exact (spec_compare op_spec). - exact (spec_mul_c op_spec). exact (spec_div21 op_spec). + exact (spec_compare op_spec). + exact (spec_div21 op_spec). Qed. Let spec_ww_div21 : forall a1 a2 b, @@ -605,7 +574,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 - _ _ _ _ _ _ _);auto. exact (spec_0W op_spec). + _ _ _ _ _ _ _);wwauto. Qed. Let spec_add2: forall x y, @@ -659,8 +628,7 @@ Section Z_2nZ. Proof. refine (spec_ww_head0 w_0 w_0W w_compare w_head0 w_add2 w_zdigits _ww_zdigits - w_to_Z _ _ _ _ _ _ _);auto. - exact (spec_0W op_spec). + w_to_Z _ _ _ _ _ _ _);wwauto. exact (spec_compare op_spec). exact (spec_zdigits op_spec). Qed. @@ -669,7 +637,7 @@ Section Z_2nZ. Proof. refine (spec_ww_tail00 w_0 w_0W w_compare w_tail0 w_add2 w_zdigits _ww_zdigits - w_to_Z _ _ _ (refl_equal _ww_digits) _ _ _ _); auto. + w_to_Z _ _ _ (refl_equal _ww_digits) _ _ _ _); wwauto. exact (spec_compare op_spec). exact (spec_tail00 op_spec). exact (spec_zdigits op_spec). @@ -680,8 +648,7 @@ Section Z_2nZ. exists y, 0 <= y /\ [|x|] = (2 * y + 1) * 2 ^ [|tail0 x|]. Proof. refine (spec_ww_tail0 (w_digits := w_digits) w_0 w_0W w_compare w_tail0 - w_add2 w_zdigits _ww_zdigits w_to_Z _ _ _ _ _ _ _);auto. - exact (spec_0W op_spec). + w_add2 w_zdigits _ww_zdigits w_to_Z _ _ _ _ _ _ _);wwauto. exact (spec_compare op_spec). exact (spec_zdigits op_spec). Qed. @@ -694,10 +661,7 @@ Section Z_2nZ. Proof. refine (@spec_ww_add_mul_div w w_0 w_WW w_W0 w_0W compare w_add_mul_div sub w_digits w_zdigits low w_to_Z - _ _ _ _ _ _ _ _ _ _ _);auto. - exact (spec_WW op_spec). - exact (spec_W0 op_spec). - exact (spec_0W op_spec). + _ _ _ _ _ _ _ _ _ _ _);wwauto. exact (spec_zdigits op_spec). Qed. @@ -714,8 +678,8 @@ refine ). exact (spec_0 op_spec). exact (spec_to_Z op_spec). - exact (spec_WW op_spec). - exact (spec_0W op_spec). + wwauto. + wwauto. exact (spec_compare op_spec). exact (spec_eq0 op_spec). exact (spec_opp_c op_spec). @@ -751,9 +715,7 @@ refine w_opp_c w_opp w_opp_carry w_sub_c w_sub w_sub_carry w_div_gt w_mod_gt w_add_mul_div w_head0 w_div21 div32 _ww_zdigits ww_1 add_mul_div w_zdigits w_to_Z - _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _);auto. - exact (spec_WW op_spec). - exact (spec_0W op_spec). + _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _);wwauto. exact (spec_compare op_spec). exact (spec_div_gt op_spec). exact (spec_div21 op_spec). @@ -775,9 +737,7 @@ refine refine (@spec_ww_gcd_gt_aux w 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 - _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _);auto. - exact (spec_WW op_spec). - exact (spec_0W op_spec). + _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _);wwauto. exact (spec_compare op_spec). exact (spec_div21 op_spec). exact (spec_zdigits op_spec). @@ -794,9 +754,7 @@ refine refine (@spec_ww_gcd_gt_aux w 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 - _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _);auto. - exact (spec_WW op_spec). - exact (spec_0W op_spec). + _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _);wwauto. exact (spec_compare op_spec). exact (spec_div21 op_spec). exact (spec_zdigits op_spec). @@ -827,13 +785,11 @@ refine w_0W w_sub w_square_c w_div21 w_add_mul_div w_digits w_zdigits _ww_zdigits w_add_c w_sqrt2 w_pred pred_c pred add_c add sub_c add_mul_div - _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _); auto. + _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _); wwauto. exact (spec_zdigits op_spec). exact (spec_more_than_1_digit op_spec). - exact (spec_0W op_spec). exact (spec_is_even op_spec). exact (spec_compare op_spec). - exact (spec_square_c op_spec). exact (spec_div21 op_spec). exact (spec_ww_add_mul_div). exact (spec_sqrt2 op_spec). @@ -845,7 +801,7 @@ refine refine (@spec_ww_sqrt w 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 - _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _); auto. + _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _); wwauto. exact (spec_zdigits op_spec). exact (spec_more_than_1_digit op_spec). exact (spec_is_even op_spec). @@ -860,10 +816,8 @@ refine refine (@spec_ww_pos_mod w w_0 w_digits w_zdigits w_WW w_pos_mod compare w_0W low sub _ww_zdigits w_to_Z - _ _ _ _ _ _ _ _ _ _ _ _);auto. - exact (spec_WW op_spec). + _ _ _ _ _ _ _ _ _ _ _ _);wwauto. exact (spec_pos_mod op_spec). - exact (spec_0W op_spec). exact (spec_zdigits op_spec). unfold w_to_Z, w_zdigits. rewrite (spec_zdigits op_spec). @@ -876,10 +830,8 @@ refine exact spec_ww_add_mul_div. refine (@spec_ww_pos_mod w w_0 w_digits w_zdigits w_WW w_pos_mod compare w_0W low sub _ww_zdigits w_to_Z - _ _ _ _ _ _ _ _ _ _ _ _);auto. - exact (spec_WW op_spec). + _ _ _ _ _ _ _ _ _ _ _ _);wwauto. exact (spec_pos_mod op_spec). - exact (spec_0W op_spec). exact (spec_zdigits op_spec). unfold w_to_Z, w_zdigits. rewrite (spec_zdigits op_spec). diff --git a/theories/Numbers/Cyclic/Int31/Cyclic31.v b/theories/Numbers/Cyclic/Int31/Cyclic31.v index c1e444fb7..a0f3a253a 100644 --- a/theories/Numbers/Cyclic/Int31/Cyclic31.v +++ b/theories/Numbers/Cyclic/Int31/Cyclic31.v @@ -1109,18 +1109,6 @@ End Basics. Section Int31_Op. -(** A function which given two int31 i and j, returns a double word - which is worth i*2^31+j *) -Let w_WW i j := - match (match i ?= 0 with Eq => j ?= 0 | not0 => not0 end) with - | Eq => W0 - | _ => WW i j - end. - -(** Two special cases where i and j are respectively taken equal to 0 *) -Let w_W0 i := match i ?= 0 with Eq => W0 | _ => WW i 0 end. -Let w_0W j := match j ?= 0 with Eq => W0 | _ => WW 0 j end. - (** Nullity test *) Let w_iszero i := match i ?= 0 with Eq => true | _ => false end. @@ -1147,9 +1135,6 @@ Definition int31_op := (mk_znz_op 0 1 Tn (* 2^31 - 1 *) - w_WW - w_W0 - w_0W (* Comparison *) compare31 w_iszero @@ -1933,42 +1918,6 @@ Section Int31_Spec. apply Zcompare_Eq_eq. now destruct ([|x|] ?= 0). Qed. - - (** [WW] and variants *) - - Let wWW := int31_op.(znz_WW). - Let w0W := int31_op.(znz_0W). - Let wW0 := int31_op.(znz_W0). - - Lemma spec_WW : forall h l, [||wWW h l||] = [|h|] * wB + [|l|]. - Proof. - clear; unfold wWW; simpl; intros. - unfold compare31 in *. - change [|0|] with 0. - case_eq ([|h|] ?= 0); simpl; auto. - case_eq ([|l|] ?= 0); simpl; auto. - intros. - rewrite (Zcompare_Eq_eq _ _ H); simpl. - rewrite (Zcompare_Eq_eq _ _ H0); simpl; auto. - Qed. - - Lemma spec_0W : forall l, [||w0W l||] = [|l|]. - Proof. - clear; unfold w0W; simpl; intros. - unfold compare31 in *. - change [|0|] with 0. - case_eq ([|l|] ?= 0); simpl; auto. - intros; symmetry; apply Zcompare_Eq_eq; auto. - Qed. - - Lemma spec_W0 : forall h, [||wW0 h||] = [|h|]*wB. - Proof. - clear; unfold wW0; simpl; intros. - unfold compare31 in *. - change [|0|] with 0. - case_eq ([|h|] ?= 0); simpl; auto with zarith. - intro H; rewrite (Zcompare_Eq_eq _ _ H); auto. - Qed. (* Even *) @@ -2003,9 +1952,6 @@ Section Int31_Spec. exact spec_0. exact spec_1. exact spec_Bm1. - exact spec_WW. - exact spec_0W. - exact spec_W0. exact spec_compare. exact spec_eq0. diff --git a/theories/Numbers/Cyclic/ZModulo/ZModulo.v b/theories/Numbers/Cyclic/ZModulo/ZModulo.v index c3f3eed08..77f1a57b4 100644 --- a/theories/Numbers/Cyclic/ZModulo/ZModulo.v +++ b/theories/Numbers/Cyclic/ZModulo/ZModulo.v @@ -158,35 +158,6 @@ Section ZModulo. unfold znz_eq0; intros; now destruct [|x|]. Qed. - Definition znz_WW h l := - if znz_eq0 h && znz_eq0 l then W0 else WW h l. - - Lemma spec_WW : forall h l, [||znz_WW h l||] = [|h|] * wB + [|l|]. - Proof. - intros; unfold znz_WW. - case_eq (znz_eq0 h); intros; simpl; auto. - case_eq (znz_eq0 l); intros; simpl; auto. - rewrite 2 spec_eq0; auto. - Qed. - - Definition znz_0W l := if znz_eq0 l then W0 else WW 0 l. - - Lemma spec_0W : forall l, [||znz_0W l||] = [|l|]. - Proof. - intros; unfold znz_0W. - case_eq (znz_eq0 l); intros; simpl; auto. - rewrite spec_eq0; auto. - Qed. - - Definition znz_W0 h := if znz_eq0 h then W0 else WW h 0. - - Lemma spec_W0 : forall h, [||znz_W0 h||] = [|h|]*wB. - Proof. - intros; unfold znz_W0. - case_eq (znz_eq0 h); intros; simpl; auto with zarith. - rewrite spec_eq0; auto with zarith. - Qed. - Definition znz_opp_c x := if znz_eq0 x then C0 0 else C1 (- x). Definition znz_opp x := - x. @@ -399,7 +370,7 @@ Section ZModulo. Definition znz_mul_c x y := let (h,l) := Zdiv_eucl ([|x|]*[|y|]) wB in - znz_WW h l. + if znz_eq0 h then if znz_eq0 l then W0 else WW h l else WW h l. Definition znz_mul := Zmult. @@ -407,7 +378,7 @@ Section ZModulo. Lemma spec_mul_c : forall x y, [|| znz_mul_c x y ||] = [|x|] * [|y|]. Proof. - intros; unfold znz_mul_c, zn2z_to_Z, znz_WW. + intros; unfold znz_mul_c, zn2z_to_Z. assert (Zdiv_eucl ([|x|]*[|y|]) wB = (([|x|]*[|y|])/wB,([|x|]*[|y|]) mod wB)). unfold Zmod, Zdiv; destruct Zdiv_eucl; auto. generalize (Z_div_mod ([|x|]*[|y|]) wB wB_pos); destruct Zdiv_eucl as (h,l). @@ -870,9 +841,6 @@ Section ZModulo. (znz_0 : znz) (znz_1 : znz) (znz_Bm1 : znz) - (znz_WW : znz -> znz -> zn2z znz) - (znz_W0 : znz -> zn2z znz) - (znz_0W : znz -> zn2z znz) (znz_compare : znz -> znz -> comparison) (znz_eq0 : znz -> bool) @@ -924,9 +892,6 @@ Section ZModulo. spec_0 spec_1 spec_Bm1 - spec_WW - spec_0W - spec_W0 spec_compare spec_eq0 diff --git a/theories/Numbers/Natural/BigN/NMake_gen.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml index ad0bf445c..22a4b200a 100644 --- a/theories/Numbers/Natural/BigN/NMake_gen.ml +++ b/theories/Numbers/Natural/BigN/NMake_gen.ml @@ -1430,13 +1430,18 @@ let _ = pr ""; for i = 0 to size do - pr " Definition w%i_0W := w%i_op.(znz_0W)." i i + pr " Definition w%i_0W := znz_0W w%i_op." i i + done; + pr ""; + + for i = 0 to size do + pr " Definition w%i_WW := znz_WW w%i_op." i i done; pr ""; for i = 0 to size do pr " Definition w%i_mul_add_n1 :=" i; - pr " @double_mul_add_n1 w%i %s w%i_op.(znz_WW) w%i_0W w%i_mul_add." i (pz i) i i i + pr " @double_mul_add_n1 w%i %s w%i_WW w%i_0W w%i_mul_add." i (pz i) i i i done; pr ""; @@ -1769,7 +1774,7 @@ let _ = pp " Let spec_divn1 ww (ww_op: znz_op ww) (ww_spec: znz_spec ww_op) := "; pp " (spec_double_divn1 "; pp " ww_op.(znz_zdigits) ww_op.(znz_0)"; - pp " ww_op.(znz_WW) ww_op.(znz_head0)"; + pp " (znz_WW ww_op) ww_op.(znz_head0)"; pp " ww_op.(znz_add_mul_div) ww_op.(znz_div21)"; pp " ww_op.(znz_compare) ww_op.(znz_sub) (znz_to_Z ww_op)"; pp " (spec_to_Z ww_spec) "; @@ -1783,7 +1788,7 @@ let _ = pr " Definition w%i_divn1 n x y :=" i; pr " let (u, v) :="; pr " double_divn1 w%i_op.(znz_zdigits) w%i_op.(znz_0)" i i; - pr " w%i_op.(znz_WW) w%i_op.(znz_head0)" i i; + pr " (znz_WW w%i_op) w%i_op.(znz_head0)" i i; pr " w%i_op.(znz_add_mul_div) w%i_op.(znz_div21)" i i; pr " w%i_op.(znz_compare) w%i_op.(znz_sub) (S n) x y in" i i; if i == size then @@ -2011,7 +2016,7 @@ let _ = pp " Let spec_modn1 ww (ww_op: znz_op ww) (ww_spec: znz_spec ww_op) := "; pp " (spec_double_modn1 "; pp " ww_op.(znz_zdigits) ww_op.(znz_0)"; - pp " ww_op.(znz_WW) ww_op.(znz_head0)"; + pp " (znz_WW ww_op) ww_op.(znz_head0)"; pp " ww_op.(znz_add_mul_div) ww_op.(znz_div21)"; pp " ww_op.(znz_compare) ww_op.(znz_sub) (znz_to_Z ww_op)"; pp " (spec_to_Z ww_spec) "; |