diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-02-08 18:17:54 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-02-08 18:17:54 +0000 |
| commit | 911c50439abdedd0f75856d43ff12e9615ec9980 (patch) | |
| tree | 6dbe4453fab01358f42f99bc7cc831d0dc189f4b /theories/Numbers/Cyclic | |
| parent | c71e226db9a2cab3e73064d24e2020a0a11e2651 (diff) | |
DoubleCyclic + NMake : typeclasses, more genericity, less ML macro-generation
- Records of operations and specs in CyclicAxioms are now
type classes (under a module ZnZ for qualification).
We benefit from inference and from generic names:
(ZnZ.mul x y) instead of (znz_mul (some_ops...) x y).
- Beware of typeclasses unfolds: the line about
Typeclasses Opaque w1 w2 ... is critical for decent
compilation time (x2.5 without it).
- Functions defined via same_level are now obtained from a
generic version by (Eval ... in ...) during definition.
The code obtained this way should be just as before, apart
from some (minor?) details. Proofs for these functions
are _way_ simplier and lighter.
- The macro-generated NMake_gen.v contains only generic iterators
and compare, mul, div_gt, mod_gt. I hope to be able to adapt
these functions as well soon.
- Spec of comparison is now fully done with respect to Zcompare
- A log2 function has been added.
- No more unsafe_shiftr, we detect the underflow directly with sub_c
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12713 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Numbers/Cyclic')
| -rw-r--r-- | theories/Numbers/Cyclic/Abstract/CyclicAxioms.v | 464 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/Abstract/NZCyclic.v | 110 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v | 55 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v | 421 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v | 117 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v | 11 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.v | 34 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.v | 19 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v | 23 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/Int31/Cyclic31.v | 287 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/Int31/Ring31.v | 7 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/ZModulo/ZModulo.v | 448 |
12 files changed, 881 insertions, 1115 deletions
diff --git a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v index 51df2fa38..af30b0175 100644 --- a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v +++ b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v @@ -26,352 +26,284 @@ Local Open Scope Z_scope. (** First, a description via an operator record and a spec record. *) -Section Z_nZ_Op. +Module ZnZ. - Variable znz : Type. - - Record znz_op := mk_znz_op { + Class Ops (t:Type) := MkOps { (* Conversion functions with Z *) - znz_digits : positive; - znz_zdigits: znz; - znz_to_Z : znz -> Z; - znz_of_pos : positive -> N * znz; (* Euclidean division by [2^digits] *) - 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 *) + digits : positive; + zdigits: t; + to_Z : t -> Z; + of_pos : positive -> N * t; (* Euclidean division by [2^digits] *) + head0 : t -> t; (* number of digits 0 in front of the number *) + tail0 : t -> t; (* number of digits 0 at the bottom of the number *) (* Basic numbers *) - znz_0 : znz; - znz_1 : znz; - znz_Bm1 : znz; (* [2^digits-1], which is equivalent to [-1] *) + zero : t; + one : t; + minus_one : t; (* [2^digits-1], which is equivalent to [-1] *) (* Comparison *) - znz_compare : znz -> znz -> comparison; - znz_eq0 : znz -> bool; + compare : t -> t -> comparison; + eq0 : t -> bool; (* Basic arithmetic operations *) - znz_opp_c : znz -> carry znz; - znz_opp : znz -> znz; - znz_opp_carry : znz -> znz; (* the carry is known to be -1 *) - - znz_succ_c : znz -> carry znz; - znz_add_c : znz -> znz -> carry znz; - znz_add_carry_c : znz -> znz -> carry znz; - znz_succ : znz -> znz; - znz_add : znz -> znz -> znz; - znz_add_carry : znz -> znz -> znz; - - znz_pred_c : znz -> carry znz; - znz_sub_c : znz -> znz -> carry znz; - znz_sub_carry_c : znz -> znz -> carry znz; - znz_pred : znz -> znz; - znz_sub : znz -> znz -> znz; - znz_sub_carry : znz -> znz -> znz; - - znz_mul_c : znz -> znz -> zn2z znz; - znz_mul : znz -> znz -> znz; - znz_square_c : znz -> zn2z znz; + opp_c : t -> carry t; + opp : t -> t; + opp_carry : t -> t; (* the carry is known to be -1 *) + + succ_c : t -> carry t; + add_c : t -> t -> carry t; + add_carry_c : t -> t -> carry t; + succ : t -> t; + add : t -> t -> t; + add_carry : t -> t -> t; + + pred_c : t -> carry t; + sub_c : t -> t -> carry t; + sub_carry_c : t -> t -> carry t; + pred : t -> t; + sub : t -> t -> t; + sub_carry : t -> t -> t; + + mul_c : t -> t -> zn2z t; + mul : t -> t -> t; + square_c : t -> zn2z t; (* Special divisions operations *) - znz_div21 : znz -> znz -> znz -> znz*znz; - znz_div_gt : znz -> znz -> znz * znz; (* specialized version of [znz_div] *) - znz_div : znz -> znz -> znz * znz; + div21 : t -> t -> t -> t*t; + div_gt : t -> t -> t * t; (* specialized version of [div] *) + div : t -> t -> t * t; - znz_mod_gt : znz -> znz -> znz; (* specialized version of [znz_mod] *) - znz_mod : znz -> znz -> znz; + modulo_gt : t -> t -> t; (* specialized version of [mod] *) + modulo : t -> t -> t; - 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)] + gcd_gt : t -> t -> t; (* specialized version of [gcd] *) + gcd : t -> t -> t; + (* [add_mul_div p i j] is a combination of the [(digits-p)] low bits of [i] above the [p] high bits of [j]: - [znz_add_mul_div p i j = i*2^p+j/2^(digits-p)] *) - znz_add_mul_div : znz -> znz -> znz -> znz; - (* [znz_pos_mod p i] is [i mod 2^p] *) - znz_pos_mod : znz -> znz -> znz; + [add_mul_div p i j = i*2^p+j/2^(digits-p)] *) + add_mul_div : t -> t -> t -> t; + (* [pos_mod p i] is [i mod 2^p] *) + pos_mod : t -> t -> t; - znz_is_even : znz -> bool; + is_even : t -> bool; (* square root *) - znz_sqrt2 : znz -> znz -> znz * carry znz; - znz_sqrt : znz -> znz }. - -End Z_nZ_Op. - -Section Z_nZ_Spec. - Variable w : Type. - Variable w_op : znz_op w. - - Let w_digits := w_op.(znz_digits). - Let w_zdigits := w_op.(znz_zdigits). - Let w_to_Z := w_op.(znz_to_Z). - Let w_of_pos := w_op.(znz_of_pos). - Let w_head0 := w_op.(znz_head0). - Let w_tail0 := w_op.(znz_tail0). - - Let w0 := w_op.(znz_0). - Let w1 := w_op.(znz_1). - Let wBm1 := w_op.(znz_Bm1). - - Let w_compare := w_op.(znz_compare). - Let w_eq0 := w_op.(znz_eq0). - - Let w_opp_c := w_op.(znz_opp_c). - Let w_opp := w_op.(znz_opp). - Let w_opp_carry := w_op.(znz_opp_carry). - - Let w_succ_c := w_op.(znz_succ_c). - Let w_add_c := w_op.(znz_add_c). - Let w_add_carry_c := w_op.(znz_add_carry_c). - Let w_succ := w_op.(znz_succ). - Let w_add := w_op.(znz_add). - Let w_add_carry := w_op.(znz_add_carry). + sqrt2 : t -> t -> t * carry t; + sqrt : t -> t }. - Let w_pred_c := w_op.(znz_pred_c). - Let w_sub_c := w_op.(znz_sub_c). - Let w_sub_carry_c := w_op.(znz_sub_carry_c). - Let w_pred := w_op.(znz_pred). - Let w_sub := w_op.(znz_sub). - Let w_sub_carry := w_op.(znz_sub_carry). + Section Specs. + Context {t : Type}{ops : Ops t}. - Let w_mul_c := w_op.(znz_mul_c). - Let w_mul := w_op.(znz_mul). - Let w_square_c := w_op.(znz_square_c). + Notation "[| x |]" := (to_Z x) (at level 0, x at level 99). - Let w_div21 := w_op.(znz_div21). - Let w_div_gt := w_op.(znz_div_gt). - Let w_div := w_op.(znz_div). - - Let w_mod_gt := w_op.(znz_mod_gt). - Let w_mod := w_op.(znz_mod). - - Let w_gcd_gt := w_op.(znz_gcd_gt). - Let w_gcd := w_op.(znz_gcd). - - Let w_add_mul_div := w_op.(znz_add_mul_div). - - Let w_pos_mod := w_op.(znz_pos_mod). - - Let w_is_even := w_op.(znz_is_even). - Let w_sqrt2 := w_op.(znz_sqrt2). - Let w_sqrt := w_op.(znz_sqrt). - - Notation "[| x |]" := (w_to_Z x) (at level 0, x at level 99). - - Let wB := base w_digits. + Let wB := base digits. Notation "[+| c |]" := - (interp_carry 1 wB w_to_Z c) (at level 0, x at level 99). + (interp_carry 1 wB to_Z c) (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 to_Z c) (at level 0, x at level 99). Notation "[|| x ||]" := - (zn2z_to_Z wB w_to_Z x) (at level 0, x at level 99). + (zn2z_to_Z wB to_Z x) (at level 0, x at level 99). - Record znz_spec := mk_znz_spec { + Class Specs := MkSpecs { (* Conversion functions with Z *) spec_to_Z : forall x, 0 <= [| x |] < wB; spec_of_pos : forall p, - Zpos p = (Z_of_N (fst (w_of_pos p)))*wB + [|(snd (w_of_pos p))|]; - spec_zdigits : [| w_zdigits |] = Zpos w_digits; - spec_more_than_1_digit: 1 < Zpos w_digits; + Zpos p = (Z_of_N (fst (of_pos p)))*wB + [|(snd (of_pos p))|]; + spec_zdigits : [| zdigits |] = Zpos digits; + spec_more_than_1_digit: 1 < Zpos digits; (* Basic numbers *) - spec_0 : [|w0|] = 0; - spec_1 : [|w1|] = 1; - spec_Bm1 : [|wBm1|] = wB - 1; + spec_0 : [|zero|] = 0; + spec_1 : [|one|] = 1; + spec_m1 : [|minus_one|] = wB - 1; (* Comparison *) - spec_compare : - forall x y, - match w_compare x y with - | Eq => [|x|] = [|y|] - | Lt => [|x|] < [|y|] - | Gt => [|x|] > [|y|] - end; - spec_eq0 : forall x, w_eq0 x = true -> [|x|] = 0; + spec_compare : forall x y, compare x y = ([|x|] ?= [|y|]); + (* NB: the spec of [eq0] is deliberately partial, + see DoubleCyclic where [eq0 x = true <-> x = W0] *) + spec_eq0 : forall x, eq0 x = true -> [|x|] = 0; (* Basic arithmetic operations *) - spec_opp_c : forall x, [-|w_opp_c x|] = -[|x|]; - spec_opp : forall x, [|w_opp x|] = (-[|x|]) mod wB; - spec_opp_carry : forall x, [|w_opp_carry x|] = wB - [|x|] - 1; - - spec_succ_c : forall x, [+|w_succ_c x|] = [|x|] + 1; - spec_add_c : forall x y, [+|w_add_c x y|] = [|x|] + [|y|]; - spec_add_carry_c : forall x y, [+|w_add_carry_c x y|] = [|x|] + [|y|] + 1; - spec_succ : forall x, [|w_succ x|] = ([|x|] + 1) mod wB; - spec_add : forall x y, [|w_add x y|] = ([|x|] + [|y|]) mod wB; + spec_opp_c : forall x, [-|opp_c x|] = -[|x|]; + spec_opp : forall x, [|opp x|] = (-[|x|]) mod wB; + spec_opp_carry : forall x, [|opp_carry x|] = wB - [|x|] - 1; + + spec_succ_c : forall x, [+|succ_c x|] = [|x|] + 1; + spec_add_c : forall x y, [+|add_c x y|] = [|x|] + [|y|]; + spec_add_carry_c : forall x y, [+|add_carry_c x y|] = [|x|] + [|y|] + 1; + spec_succ : forall x, [|succ x|] = ([|x|] + 1) mod wB; + spec_add : forall x y, [|add x y|] = ([|x|] + [|y|]) mod wB; spec_add_carry : - forall x y, [|w_add_carry x y|] = ([|x|] + [|y|] + 1) mod wB; + forall x y, [|add_carry x y|] = ([|x|] + [|y|] + 1) mod wB; - spec_pred_c : forall x, [-|w_pred_c x|] = [|x|] - 1; - spec_sub_c : forall x y, [-|w_sub_c x y|] = [|x|] - [|y|]; - spec_sub_carry_c : forall x y, [-|w_sub_carry_c x y|] = [|x|] - [|y|] - 1; - spec_pred : forall x, [|w_pred x|] = ([|x|] - 1) mod wB; - spec_sub : forall x y, [|w_sub x y|] = ([|x|] - [|y|]) mod wB; + spec_pred_c : forall x, [-|pred_c x|] = [|x|] - 1; + spec_sub_c : forall x y, [-|sub_c x y|] = [|x|] - [|y|]; + spec_sub_carry_c : forall x y, [-|sub_carry_c x y|] = [|x|] - [|y|] - 1; + spec_pred : forall x, [|pred x|] = ([|x|] - 1) mod wB; + spec_sub : forall x y, [|sub x y|] = ([|x|] - [|y|]) mod wB; spec_sub_carry : - forall x y, [|w_sub_carry x y|] = ([|x|] - [|y|] - 1) mod wB; + forall x y, [|sub_carry x y|] = ([|x|] - [|y|] - 1) mod wB; - spec_mul_c : forall x y, [|| w_mul_c x y ||] = [|x|] * [|y|]; - spec_mul : forall x y, [|w_mul x y|] = ([|x|] * [|y|]) mod wB; - spec_square_c : forall x, [|| w_square_c x||] = [|x|] * [|x|]; + spec_mul_c : forall x y, [|| mul_c x y ||] = [|x|] * [|y|]; + spec_mul : forall x y, [|mul x y|] = ([|x|] * [|y|]) mod wB; + spec_square_c : forall x, [|| square_c x||] = [|x|] * [|x|]; (* Special divisions operations *) spec_div21 : forall a1 a2 b, wB/2 <= [|b|] -> [|a1|] < [|b|] -> - let (q,r) := w_div21 a1 a2 b in + let (q,r) := div21 a1 a2 b in [|a1|] *wB+ [|a2|] = [|q|] * [|b|] + [|r|] /\ 0 <= [|r|] < [|b|]; spec_div_gt : forall a b, [|a|] > [|b|] -> 0 < [|b|] -> - let (q,r) := w_div_gt a b in + let (q,r) := div_gt a b in [|a|] = [|q|] * [|b|] + [|r|] /\ 0 <= [|r|] < [|b|]; spec_div : forall a b, 0 < [|b|] -> - let (q,r) := w_div a b in + let (q,r) := div a b in [|a|] = [|q|] * [|b|] + [|r|] /\ 0 <= [|r|] < [|b|]; - spec_mod_gt : forall a b, [|a|] > [|b|] -> 0 < [|b|] -> - [|w_mod_gt a b|] = [|a|] mod [|b|]; - spec_mod : forall a b, 0 < [|b|] -> - [|w_mod a b|] = [|a|] mod [|b|]; + spec_modulo_gt : forall a b, [|a|] > [|b|] -> 0 < [|b|] -> + [|modulo_gt a b|] = [|a|] mod [|b|]; + spec_modulo : forall a b, 0 < [|b|] -> + [|modulo a b|] = [|a|] mod [|b|]; spec_gcd_gt : forall a b, [|a|] > [|b|] -> - Zis_gcd [|a|] [|b|] [|w_gcd_gt a b|]; - spec_gcd : forall a b, Zis_gcd [|a|] [|b|] [|w_gcd a b|]; + Zis_gcd [|a|] [|b|] [|gcd_gt a b|]; + spec_gcd : forall a b, Zis_gcd [|a|] [|b|] [|gcd a b|]; (* shift operations *) - spec_head00: forall x, [|x|] = 0 -> [|w_head0 x|] = Zpos w_digits; + spec_head00: forall x, [|x|] = 0 -> [|head0 x|] = Zpos digits; spec_head0 : forall x, 0 < [|x|] -> - wB/ 2 <= 2 ^ ([|w_head0 x|]) * [|x|] < wB; - spec_tail00: forall x, [|x|] = 0 -> [|w_tail0 x|] = Zpos w_digits; + wB/ 2 <= 2 ^ ([|head0 x|]) * [|x|] < wB; + spec_tail00: forall x, [|x|] = 0 -> [|tail0 x|] = Zpos digits; spec_tail0 : forall x, 0 < [|x|] -> - exists y, 0 <= y /\ [|x|] = (2 * y + 1) * (2 ^ [|w_tail0 x|]) ; + exists y, 0 <= y /\ [|x|] = (2 * y + 1) * (2 ^ [|tail0 x|]) ; spec_add_mul_div : forall x y p, - [|p|] <= Zpos w_digits -> - [| w_add_mul_div p x y |] = + [|p|] <= Zpos digits -> + [| add_mul_div p x y |] = ([|x|] * (2 ^ [|p|]) + - [|y|] / (2 ^ ((Zpos w_digits) - [|p|]))) mod wB; + [|y|] / (2 ^ ((Zpos digits) - [|p|]))) mod wB; spec_pos_mod : forall w p, - [|w_pos_mod p w|] = [|w|] mod (2 ^ [|p|]); + [|pos_mod p w|] = [|w|] mod (2 ^ [|p|]); (* sqrt *) spec_is_even : forall x, - if w_is_even x then [|x|] mod 2 = 0 else [|x|] mod 2 = 1; + if is_even x then [|x|] mod 2 = 0 else [|x|] mod 2 = 1; spec_sqrt2 : forall x y, wB/ 4 <= [|x|] -> - let (s,r) := w_sqrt2 x y in + let (s,r) := sqrt2 x y in [||WW x y||] = [|s|] ^ 2 + [+|r|] /\ [+|r|] <= 2 * [|s|]; spec_sqrt : forall x, - [|w_sqrt x|] ^ 2 <= [|x|] < ([|w_sqrt x|] + 1) ^ 2 + [|sqrt x|] ^ 2 <= [|x|] < ([|sqrt x|] + 1) ^ 2 }. -End Z_nZ_Spec. + End Specs. + + Implicit Arguments Specs [[t]]. -(** Generic construction of double words *) + (** Generic construction of double words *) -Section WW. + Section WW. - Variable w : Type. - Variable w_op : znz_op w. - Variable op_spec : znz_spec w_op. + Context {t : Type}{ops : Ops t}{specs : Specs ops}. - 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). + Let wB := base digits. - Definition znz_W0 h := - if w_eq0 h then W0 else WW h w_0. + Definition WO h := + if eq0 h then W0 else WW h zero. - Definition znz_0W l := - if w_eq0 l then W0 else WW w_0 l. + Definition OW l := + if eq0 l then W0 else WW zero l. - Definition znz_WW h l := - if w_eq0 h then znz_0W l else WW h l. + Definition WW h l := + if eq0 h then OW 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. + Lemma spec_WO : forall h, + zn2z_to_Z wB to_Z (WO h) = (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. + unfold zn2z_to_Z, WO; simpl; intros. + case_eq (eq0 h); intros. + rewrite (spec_eq0 _ H); auto. + rewrite 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. + Lemma spec_OW : forall l, + zn2z_to_Z wB to_Z (OW l) = 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. + unfold zn2z_to_Z, OW; simpl; intros. + case_eq (eq0 l); intros. + rewrite (spec_eq0 _ H); auto. + rewrite 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. + zn2z_to_Z wB to_Z (WW h l) = (to_Z h)*wB + 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. + unfold WW; simpl; intros. + case_eq (eq0 h); intros. + rewrite (spec_eq0 _ H); auto. + rewrite spec_OW; auto. simpl; auto. Qed. -End WW. + End WW. -(** Injecting [Z] numbers into a cyclic structure *) + (** Injecting [Z] numbers into a cyclic structure *) -Section znz_of_pos. + Section Of_Z. - Variable w : Type. - Variable w_op : znz_op w. - Variable op_spec : znz_spec w_op. + Context {t : Type}{ops : Ops t}{specs : Specs ops}. - Notation "[| x |]" := (znz_to_Z w_op x) (at level 0, x at level 99). + Notation "[| x |]" := (to_Z x) (at level 0, x at level 99). - Definition znz_of_Z (w:Type) (op:znz_op w) z := - match z with - | Zpos p => snd (op.(znz_of_pos) p) - | _ => op.(znz_0) - end. - - Theorem znz_of_pos_correct: - forall p, Zpos p < base (znz_digits w_op) -> [|(snd (znz_of_pos w_op p))|] = Zpos p. + Theorem of_pos_correct: + forall p, Zpos p < base digits -> [|(snd (of_pos p))|] = Zpos p. + Proof. intros p Hp. - generalize (spec_of_pos op_spec p). - case (znz_of_pos w_op p); intros n w1; simpl. + generalize (spec_of_pos p). + case (of_pos p); intros n w1; simpl. case n; simpl Npos; auto with zarith. intros p1 Hp1; contradict Hp; apply Zle_not_lt. - rewrite Hp1; auto with zarith. - match goal with |- _ <= ?X + ?Y => - apply Zle_trans with X; auto with zarith - end. - match goal with |- ?X <= _ => - pattern X at 1; rewrite <- (Zmult_1_l); - apply Zmult_le_compat_r; auto with zarith - end. + replace (base digits) with (1 * base digits + 0) by auto with zarith. + rewrite Hp1. + apply Zplus_le_compat. + apply Zmult_le_compat; auto with zarith. case p1; simpl; intros; red; simpl; intros; discriminate. unfold base; auto with zarith. - case (spec_to_Z op_spec w1); auto with zarith. + case (spec_to_Z w1); auto with zarith. Qed. - Theorem znz_of_Z_correct: - forall p, 0 <= p < base (znz_digits w_op) -> [|znz_of_Z w_op p|] = p. + Definition of_Z z := + match z with + | Zpos p => snd (of_pos p) + | _ => zero + end. + + Theorem of_Z_correct: + forall p, 0 <= p < base digits -> [|of_Z p|] = p. + Proof. intros p; case p; simpl; try rewrite spec_0; auto. - intros; rewrite znz_of_pos_correct; auto with zarith. + intros; rewrite of_pos_correct; auto with zarith. intros p1 (H1, _); contradict H1; apply Zlt_not_le; red; simpl; auto. Qed. -End znz_of_pos. + End Of_Z. + +End ZnZ. (** A modular specification grouping the earlier records. *) Module Type CyclicType. - Parameter w : Type. - Parameter w_op : znz_op w. - Parameter w_spec : znz_spec w_op. + Parameter t : Type. + Declare Instance ops : ZnZ.Ops t. + Declare Instance specs : ZnZ.Specs ops. End CyclicType. @@ -379,38 +311,29 @@ End CyclicType. Module CyclicRing (Import Cyclic : CyclicType). -Definition t := w. - -Local Notation "[| x |]" := (w_op.(znz_to_Z) x) (at level 0, x at level 99). +Local Notation "[| x |]" := (ZnZ.to_Z x) (at level 0, x at level 99). Definition eq (n m : t) := [| n |] = [| m |]. -Definition zero : t := w_op.(znz_0). -Definition one := w_op.(znz_1). -Definition add := w_op.(znz_add). -Definition sub := w_op.(znz_sub). -Definition mul := w_op.(znz_mul). -Definition opp := w_op.(znz_opp). Local Infix "==" := eq (at level 70). -Local Notation "0" := zero. -Local Notation "1" := one. -Local Infix "+" := add. -Local Infix "-" := sub. -Local Infix "*" := mul. -Local Notation "!!" := (base (znz_digits w_op)). - -Hint Rewrite - w_spec.(spec_0) w_spec.(spec_1) - w_spec.(spec_add) w_spec.(spec_mul) w_spec.(spec_opp) w_spec.(spec_sub) +Local Notation "0" := ZnZ.zero. +Local Notation "1" := ZnZ.one. +Local Infix "+" := ZnZ.add. +Local Infix "-" := ZnZ.sub. +Local Notation "- x" := (ZnZ.opp x). +Local Infix "*" := ZnZ.mul. +Local Notation wB := (base ZnZ.digits). + +Hint Rewrite ZnZ.spec_0 ZnZ.spec_1 ZnZ.spec_add ZnZ.spec_mul + ZnZ.spec_opp ZnZ.spec_sub : cyclic. -Ltac zify := - unfold eq, zero, one, add, sub, mul, opp in *; autorewrite with cyclic. +Ltac zify := unfold eq in *; autorewrite with cyclic. Lemma add_0_l : forall x, 0 + x == x. Proof. intros. zify. rewrite Zplus_0_l. -apply Zmod_small. apply w_spec.(spec_to_Z). +apply Zmod_small. apply ZnZ.spec_to_Z. Qed. Lemma add_comm : forall x y, x + y == y + x. @@ -426,7 +349,7 @@ Qed. Lemma mul_1_l : forall x, 1 * x == x. Proof. intros. zify. rewrite Zmult_1_l. -apply Zmod_small. apply w_spec.(spec_to_Z). +apply Zmod_small. apply ZnZ.spec_to_Z. Qed. Lemma mul_comm : forall x y, x * y == y * x. @@ -444,22 +367,22 @@ Proof. intros. zify. now rewrite <- Zplus_mod, Zmult_mod_idemp_l, Zmult_plus_distr_l. Qed. -Lemma add_opp_r : forall x y, x + opp y == x-y. +Lemma add_opp_r : forall x y, x + - y == x-y. Proof. intros. zify. rewrite <- Zminus_mod_idemp_r. unfold Zminus. -destruct (Z_eq_dec ([|y|] mod !!) 0) as [EQ|NEQ]. +destruct (Z_eq_dec ([|y|] mod wB) 0) as [EQ|NEQ]. rewrite Z_mod_zero_opp_full, EQ, 2 Zplus_0_r; auto. rewrite Z_mod_nz_opp_full by auto. rewrite <- Zplus_mod_idemp_r, <- Zminus_mod_idemp_l. rewrite Z_mod_same_full. simpl. now rewrite Zplus_mod_idemp_r. Qed. -Lemma add_opp_diag_r : forall x, x + opp x == 0. +Lemma add_opp_diag_r : forall x, x + - x == 0. Proof. intros. red. rewrite add_opp_r. zify. now rewrite Zminus_diag, Zmod_0_l. Qed. -Lemma CyclicRing : ring_theory 0 1 add mul sub opp eq. +Lemma CyclicRing : ring_theory 0 1 ZnZ.add ZnZ.mul ZnZ.sub ZnZ.opp eq. Proof. constructor. exact add_0_l. exact add_comm. exact add_assoc. @@ -470,13 +393,24 @@ exact add_opp_diag_r. Qed. Definition eqb x y := - match w_op.(znz_compare) x y with Eq => true | _ => false end. + match ZnZ.compare x y with Eq => true | _ => false end. + +Lemma eqb_eq : forall x y, eqb x y = true <-> x == y. +Proof. + intros. unfold eqb, eq. + rewrite ZnZ.spec_compare. + case Zcompare_spec; intuition; try discriminate. +Qed. +(* POUR HUGO: Lemma eqb_eq : forall x y, eqb x y = true <-> x == y. Proof. - intros. unfold eqb, eq. generalize (w_spec.(spec_compare) x y). - destruct (w_op.(znz_compare) x y); intuition; try discriminate. + intros. unfold eqb, eq. generalize (ZnZ.spec_compare x y). + case (ZnZ.compare x y); intuition; try discriminate. + (* BUG ?! using destruct instead of case won't work: + it gives 3 subcases, but ZnZ.compare x y is still there in them! *) Qed. +*) Lemma eqb_correct : forall x y, eqb x y = true -> x==y. Proof. now apply eqb_eq. Qed. diff --git a/theories/Numbers/Cyclic/Abstract/NZCyclic.v b/theories/Numbers/Cyclic/Abstract/NZCyclic.v index 517e48ad9..b68e89560 100644 --- a/theories/Numbers/Cyclic/Abstract/NZCyclic.v +++ b/theories/Numbers/Cyclic/Abstract/NZCyclic.v @@ -27,21 +27,17 @@ Module NZCyclicAxiomsMod (Import Cyclic : CyclicType) <: NZAxiomsSig. Local Open Scope Z_scope. -Definition t := w. +Local Notation wB := (base ZnZ.digits). -Definition NZ_to_Z : t -> Z := znz_to_Z w_op. -Definition Z_to_NZ : Z -> t := znz_of_Z w_op. -Local Notation wB := (base w_op.(znz_digits)). - -Local Notation "[| x |]" := (w_op.(znz_to_Z) x) (at level 0, x at level 99). +Local Notation "[| x |]" := (ZnZ.to_Z x) (at level 0, x at level 99). Definition eq (n m : t) := [| n |] = [| m |]. -Definition zero := w_op.(znz_0). -Definition succ := w_op.(znz_succ). -Definition pred := w_op.(znz_pred). -Definition add := w_op.(znz_add). -Definition sub := w_op.(znz_sub). -Definition mul := w_op.(znz_mul). +Definition zero := ZnZ.zero. +Definition succ := ZnZ.succ. +Definition pred := ZnZ.pred. +Definition add := ZnZ.add. +Definition sub := ZnZ.sub. +Definition mul := ZnZ.mul. Local Infix "==" := eq (at level 70). Local Notation "0" := zero. @@ -51,41 +47,25 @@ Local Infix "+" := add. Local Infix "-" := sub. Local Infix "*" := mul. -Hint Rewrite w_spec.(spec_0) w_spec.(spec_succ) w_spec.(spec_pred) - w_spec.(spec_add) w_spec.(spec_mul) w_spec.(spec_sub) : w. -Ltac wsimpl := - unfold eq, zero, succ, pred, add, sub, mul; autorewrite with w. -Ltac wcongruence := repeat red; intros; wsimpl; congruence. +Hint Rewrite ZnZ.spec_0 ZnZ.spec_succ ZnZ.spec_pred + ZnZ.spec_add ZnZ.spec_mul ZnZ.spec_sub : cyclic. +Ltac zify := + unfold eq, zero, succ, pred, add, sub, mul in *; + autorewrite with cyclic. +Ltac zcongruence := repeat red; intros; zify; congruence. Instance eq_equiv : Equivalence eq. Proof. unfold eq. firstorder. Qed. -Instance succ_wd : Proper (eq ==> eq) succ. -Proof. -wcongruence. -Qed. - -Instance pred_wd : Proper (eq ==> eq) pred. -Proof. -wcongruence. -Qed. +Local Obligation Tactic := zcongruence. -Instance add_wd : Proper (eq ==> eq ==> eq) add. -Proof. -wcongruence. -Qed. - -Instance sub_wd : Proper (eq ==> eq ==> eq) sub. -Proof. -wcongruence. -Qed. - -Instance mul_wd : Proper (eq ==> eq ==> eq) mul. -Proof. -wcongruence. -Qed. +Program Instance succ_wd : Proper (eq ==> eq) succ. +Program Instance pred_wd : Proper (eq ==> eq) pred. +Program Instance add_wd : Proper (eq ==> eq ==> eq) add. +Program Instance sub_wd : Proper (eq ==> eq ==> eq) sub. +Program Instance mul_wd : Proper (eq ==> eq ==> eq) mul. Theorem gt_wB_1 : 1 < wB. Proof. @@ -115,23 +95,16 @@ Qed. Lemma NZ_to_Z_mod : forall n, [| n |] mod wB = [| n |]. Proof. -intro n; rewrite Zmod_small. reflexivity. apply w_spec.(spec_to_Z). +intro n; rewrite Zmod_small. reflexivity. apply ZnZ.spec_to_Z. Qed. Theorem pred_succ : forall n, P (S n) == n. Proof. -intro n. wsimpl. +intro n. zify. rewrite <- pred_mod_wB. replace ([| n |] + 1 - 1)%Z with [| n |] by auto with zarith. apply NZ_to_Z_mod. Qed. -Lemma Z_to_NZ_0 : Z_to_NZ 0%Z == 0. -Proof. -unfold NZ_to_Z, Z_to_NZ. wsimpl. -rewrite znz_of_Z_correct; auto. -exact w_spec. split; [auto with zarith |apply gt_wB_0]. -Qed. - Section Induction. Variable A : t -> Prop. @@ -140,21 +113,22 @@ Hypothesis A0 : A 0. Hypothesis AS : forall n, A n <-> A (S n). (* Below, we use only -> direction *) -Let B (n : Z) := A (Z_to_NZ n). +Let B (n : Z) := A (ZnZ.of_Z n). Lemma B0 : B 0. Proof. -unfold B. now rewrite Z_to_NZ_0. +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. Qed. Lemma BS : forall n : Z, 0 <= n -> n < wB - 1 -> B n -> B (n + 1). Proof. intros n H1 H2 H3. unfold B in *. apply -> AS in H3. -setoid_replace (Z_to_NZ (n + 1)) with (S (Z_to_NZ n)). assumption. -wsimpl. -unfold NZ_to_Z, Z_to_NZ. -do 2 (rewrite znz_of_Z_correct; [ | exact w_spec | auto with zarith]). +setoid_replace (ZnZ.of_Z (n + 1)) with (S (ZnZ.of_Z n)). assumption. +zify. +rewrite 2 ZnZ.of_Z_correct; auto with zarith. symmetry; apply Zmod_small; auto with zarith. Qed. @@ -167,25 +141,23 @@ Qed. Theorem bi_induction : forall n, A n. Proof. -intro n. setoid_replace n with (Z_to_NZ (NZ_to_Z n)). -apply B_holds. apply w_spec.(spec_to_Z). -unfold eq, NZ_to_Z, Z_to_NZ; rewrite znz_of_Z_correct. -reflexivity. -exact w_spec. -apply w_spec.(spec_to_Z). +intro n. setoid_replace n with (ZnZ.of_Z (ZnZ.to_Z n)). +apply B_holds. apply ZnZ.spec_to_Z. +red. symmetry. apply ZnZ.of_Z_correct. +apply ZnZ.spec_to_Z. Qed. End Induction. Theorem add_0_l : forall n, 0 + n == n. Proof. -intro n. wsimpl. -rewrite Zplus_0_l. rewrite Zmod_small; [reflexivity | apply w_spec.(spec_to_Z)]. +intro n. zify. +rewrite Zplus_0_l. apply Zmod_small. apply ZnZ.spec_to_Z. Qed. Theorem add_succ_l : forall n m, (S n) + m == S (n + m). Proof. -intros n m. wsimpl. +intros n m. zify. rewrite succ_mod_wB. repeat rewrite Zplus_mod_idemp_l; try apply gt_wB_0. rewrite <- (Zplus_assoc ([| n |] mod wB) 1 [| m |]). rewrite Zplus_mod_idemp_l. rewrite (Zplus_comm 1 [| m |]); now rewrite Zplus_assoc. @@ -193,25 +165,27 @@ Qed. Theorem sub_0_r : forall n, n - 0 == n. Proof. -intro n. wsimpl. rewrite Zminus_0_r. apply NZ_to_Z_mod. +intro n. zify. rewrite Zminus_0_r. apply NZ_to_Z_mod. Qed. Theorem sub_succ_r : forall n m, n - (S m) == P (n - m). Proof. -intros n m. wsimpl. rewrite Zminus_mod_idemp_r, Zminus_mod_idemp_l. +intros n m. zify. rewrite Zminus_mod_idemp_r, Zminus_mod_idemp_l. now replace ([|n|] - ([|m|] + 1))%Z with ([|n|] - [|m|] - 1)%Z by auto with zarith. Qed. Theorem mul_0_l : forall n, 0 * n == 0. Proof. -intro n. wsimpl. now rewrite Zmult_0_l. +intro n. now zify. Qed. Theorem mul_succ_l : forall n m, (S n) * m == n * m + m. Proof. -intros n m. wsimpl. rewrite Zplus_mod_idemp_l, Zmult_mod_idemp_l. +intros n m. zify. rewrite Zplus_mod_idemp_l, Zmult_mod_idemp_l. now rewrite Zmult_plus_distr_l, Zmult_1_l. Qed. +Definition t := t. + End NZCyclicAxiomsMod. diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v index 88c34915d..23c62740c 100644 --- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v +++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v @@ -167,11 +167,7 @@ Section DoubleBase. Variable spec_w_0W : forall l, [[w_0W l]] = [|l|]. Variable spec_to_Z : forall x, 0 <= [|x|] < wB. Variable spec_w_compare : forall x y, - match w_compare x y with - | Eq => [|x|] = [|y|] - | Lt => [|x|] < [|y|] - | Gt => [|x|] > [|y|] - end. + w_compare x y = Zcompare [|x|] [|y|]. Lemma wwB_wBwB : wwB = wB^2. Proof. @@ -408,35 +404,40 @@ Section DoubleBase. intros a b c d H1; apply beta_lex_inv with (1 := H1); auto. Qed. + Ltac comp2ord := match goal with + | |- Lt = (?x ?= ?y) => symmetry; change (x < y) + | |- Gt = (?x ?= ?y) => symmetry; change (x > y); apply Zlt_gt + end. + Lemma spec_ww_compare : forall x y, - match ww_compare x y with - | Eq => [[x]] = [[y]] - | Lt => [[x]] < [[y]] - | Gt => [[x]] > [[y]] - end. + ww_compare x y = Zcompare [[x]] [[y]]. Proof. destruct x as [ |xh xl];destruct y as [ |yh yl];simpl;trivial. - generalize (spec_w_compare w_0 yh);destruct (w_compare w_0 yh); - intros H;rewrite spec_w_0 in H. - rewrite <- H;simpl;rewrite <- spec_w_0;apply spec_w_compare. - change 0 with (0*wB+0);pattern 0 at 2;rewrite <- spec_w_0. + (* 1st case *) + rewrite 2 spec_w_compare, spec_w_0. + destruct (Zcompare_spec 0 [|yh|]) as [H|H|H]. + rewrite <- H;simpl. reflexivity. + symmetry. change (0 < [|yh|]*wB+[|yl|]). + change 0 with (0*wB+0). rewrite <- spec_w_0 at 2. apply wB_lex_inv;trivial. - absurd (0 <= [|yh|]). apply Zgt_not_le;trivial. + absurd (0 <= [|yh|]). apply Zlt_not_le; trivial. destruct (spec_to_Z yh);trivial. - generalize (spec_w_compare xh w_0);destruct (w_compare xh w_0); - intros H;rewrite spec_w_0 in H. - rewrite H;simpl;rewrite <- spec_w_0;apply spec_w_compare. - absurd (0 <= [|xh|]). apply Zgt_not_le;apply Zlt_gt;trivial. + (* 2nd case *) + rewrite 2 spec_w_compare, spec_w_0. + destruct (Zcompare_spec [|xh|] 0) as [H|H|H]. + rewrite H;simpl;reflexivity. + absurd (0 <= [|xh|]). apply Zlt_not_le; trivial. destruct (spec_to_Z xh);trivial. - apply Zlt_gt;change 0 with (0*wB+0);pattern 0 at 2;rewrite <- spec_w_0. - apply wB_lex_inv;apply Zgt_lt;trivial. - - generalize (spec_w_compare xh yh);destruct (w_compare xh yh);intros H. - rewrite H;generalize (spec_w_compare xl yl);destruct (w_compare xl yl); - intros H1;[rewrite H1|apply Zplus_lt_compat_l|apply Zplus_gt_compat_l]; - trivial. + comp2ord. + change 0 with (0*wB+0). rewrite <- spec_w_0 at 2. apply wB_lex_inv;trivial. - apply Zlt_gt;apply wB_lex_inv;apply Zgt_lt;trivial. + (* 3rd case *) + rewrite 2 spec_w_compare. + destruct (Zcompare_spec [|xh|] [|yh|]) as [H|H|H]. + rewrite H. + symmetry. apply Zcompare_plus_compat. + comp2ord. apply wB_lex_inv;trivial. + comp2ord. apply wB_lex_inv;trivial. Qed. diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v index eea29e7ca..49a4f950a 100644 --- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v +++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v @@ -30,65 +30,65 @@ Local Open Scope Z_scope. Section Z_2nZ. - Variable w : Type. - Variable w_op : znz_op w. - Let w_digits := w_op.(znz_digits). - Let w_zdigits := w_op.(znz_zdigits). + Context {t : Type}{ops : ZnZ.Ops t}. - Let w_to_Z := w_op.(znz_to_Z). - Let w_of_pos := w_op.(znz_of_pos). - Let w_head0 := w_op.(znz_head0). - Let w_tail0 := w_op.(znz_tail0). + Let w_digits := ZnZ.digits. + Let w_zdigits := ZnZ.zdigits. - Let w_0 := w_op.(znz_0). - Let w_1 := w_op.(znz_1). - Let w_Bm1 := w_op.(znz_Bm1). + Let w_to_Z := ZnZ.to_Z. + Let w_of_pos := ZnZ.of_pos. + Let w_head0 := ZnZ.head0. + Let w_tail0 := ZnZ.tail0. - Let w_compare := w_op.(znz_compare). - Let w_eq0 := w_op.(znz_eq0). + Let w_0 := ZnZ.zero. + Let w_1 := ZnZ.one. + Let w_Bm1 := ZnZ.minus_one. - Let w_opp_c := w_op.(znz_opp_c). - Let w_opp := w_op.(znz_opp). - Let w_opp_carry := w_op.(znz_opp_carry). + Let w_compare := ZnZ.compare. + Let w_eq0 := ZnZ.eq0. - Let w_succ_c := w_op.(znz_succ_c). - Let w_add_c := w_op.(znz_add_c). - Let w_add_carry_c := w_op.(znz_add_carry_c). - Let w_succ := w_op.(znz_succ). - Let w_add := w_op.(znz_add). - Let w_add_carry := w_op.(znz_add_carry). + Let w_opp_c := ZnZ.opp_c. + Let w_opp := ZnZ.opp. + Let w_opp_carry := ZnZ.opp_carry. - Let w_pred_c := w_op.(znz_pred_c). - Let w_sub_c := w_op.(znz_sub_c). - Let w_sub_carry_c := w_op.(znz_sub_carry_c). - Let w_pred := w_op.(znz_pred). - Let w_sub := w_op.(znz_sub). - Let w_sub_carry := w_op.(znz_sub_carry). + Let w_succ_c := ZnZ.succ_c. + Let w_add_c := ZnZ.add_c. + Let w_add_carry_c := ZnZ.add_carry_c. + Let w_succ := ZnZ.succ. + Let w_add := ZnZ.add. + Let w_add_carry := ZnZ.add_carry. + Let w_pred_c := ZnZ.pred_c. + Let w_sub_c := ZnZ.sub_c. + Let w_sub_carry_c := ZnZ.sub_carry_c. + Let w_pred := ZnZ.pred. + Let w_sub := ZnZ.sub. + Let w_sub_carry := ZnZ.sub_carry. - Let w_mul_c := w_op.(znz_mul_c). - Let w_mul := w_op.(znz_mul). - Let w_square_c := w_op.(znz_square_c). - Let w_div21 := w_op.(znz_div21). - Let w_div_gt := w_op.(znz_div_gt). - Let w_div := w_op.(znz_div). + Let w_mul_c := ZnZ.mul_c. + Let w_mul := ZnZ.mul. + Let w_square_c := ZnZ.square_c. - Let w_mod_gt := w_op.(znz_mod_gt). - Let w_mod := w_op.(znz_mod). + Let w_div21 := ZnZ.div21. + Let w_div_gt := ZnZ.div_gt. + Let w_div := ZnZ.div. - Let w_gcd_gt := w_op.(znz_gcd_gt). - Let w_gcd := w_op.(znz_gcd). + Let w_mod_gt := ZnZ.modulo_gt. + Let w_mod := ZnZ.modulo. - Let w_add_mul_div := w_op.(znz_add_mul_div). + Let w_gcd_gt := ZnZ.gcd_gt. + Let w_gcd := ZnZ.gcd. - Let w_pos_mod := w_op.(znz_pos_mod). + Let w_add_mul_div := ZnZ.add_mul_div. - Let w_is_even := w_op.(znz_is_even). - Let w_sqrt2 := w_op.(znz_sqrt2). - Let w_sqrt := w_op.(znz_sqrt). + Let w_pos_mod := ZnZ.pos_mod. - Let _zn2z := zn2z w. + Let w_is_even := ZnZ.is_even. + Let w_sqrt2 := ZnZ.sqrt2. + Let w_sqrt := ZnZ.sqrt. + + Let _zn2z := zn2z t. Let wB := base w_digits. @@ -105,9 +105,9 @@ Section Z_2nZ. Let to_Z := zn2z_to_Z wB w_to_Z. - Let w_W0 := znz_W0 w_op. - Let w_0W := znz_0W w_op. - Let w_WW := znz_WW w_op. + Let w_W0 (x:t) := ZnZ.WO x. + Let w_0W (x:t) := ZnZ.OW x. + Let w_WW (x y:t) := ZnZ.WW x y. Let ww_of_pos p := match w_of_pos p with @@ -124,15 +124,15 @@ Section Z_2nZ. Eval lazy beta delta [ww_tail0] in ww_tail0 w_0 w_0W w_compare w_tail0 w_add2 w_zdigits _ww_zdigits. - Let ww_WW := Eval lazy beta delta [ww_WW] in (@ww_WW w). - Let ww_0W := Eval lazy beta delta [ww_0W] in (@ww_0W w). - Let ww_W0 := Eval lazy beta delta [ww_W0] in (@ww_W0 w). + Let ww_WW := Eval lazy beta delta [ww_WW] in (@ww_WW t). + Let ww_0W := Eval lazy beta delta [ww_0W] in (@ww_0W t). + Let ww_W0 := Eval lazy beta delta [ww_W0] in (@ww_W0 t). (* ** Comparison ** *) Let compare := Eval lazy beta delta[ww_compare] in ww_compare w_0 w_compare. - Let eq0 (x:zn2z w) := + Let eq0 (x:zn2z t) := match x with | W0 => true | _ => false @@ -226,7 +226,7 @@ Section Z_2nZ. Eval lazy beta iota delta [ww_div21] in ww_div21 w_0 w_0W div32 ww_1 compare sub. - Let low (p: zn2z w) := match p with WW _ p1 => p1 | _ => w_0 end. + Let low (p: zn2z t) := match p with WW _ p1 => p1 | _ => w_0 end. Let add_mul_div := Eval lazy beta delta [ww_add_mul_div] in @@ -287,8 +287,8 @@ Section Z_2nZ. (* ** Record of operators on 2 words *) - Definition mk_zn2z_op := - mk_znz_op _ww_digits _ww_zdigits + Global Instance mk_zn2z_ops : ZnZ.Ops (zn2z t) := + ZnZ.MkOps _ww_digits _ww_zdigits to_Z ww_of_pos head0 tail0 W0 ww_1 ww_Bm1 compare eq0 @@ -307,8 +307,8 @@ Section Z_2nZ. sqrt2 sqrt. - Definition mk_zn2z_op_karatsuba := - mk_znz_op _ww_digits _ww_zdigits + Global Instance mk_zn2z_ops_karatsuba : ZnZ.Ops (zn2z t) := + ZnZ.MkOps _ww_digits _ww_zdigits to_Z ww_of_pos head0 tail0 W0 ww_1 ww_Bm1 compare eq0 @@ -328,51 +328,51 @@ Section Z_2nZ. sqrt. (* Proof *) - Variable op_spec : znz_spec w_op. + Context {specs : ZnZ.Specs ops}. Hint Resolve - (spec_to_Z op_spec) - (spec_of_pos op_spec) - (spec_0 op_spec) - (spec_1 op_spec) - (spec_Bm1 op_spec) - (spec_compare op_spec) - (spec_eq0 op_spec) - (spec_opp_c op_spec) - (spec_opp op_spec) - (spec_opp_carry op_spec) - (spec_succ_c op_spec) - (spec_add_c op_spec) - (spec_add_carry_c op_spec) - (spec_succ op_spec) - (spec_add op_spec) - (spec_add_carry op_spec) - (spec_pred_c op_spec) - (spec_sub_c op_spec) - (spec_sub_carry_c op_spec) - (spec_pred op_spec) - (spec_sub op_spec) - (spec_sub_carry op_spec) - (spec_mul_c op_spec) - (spec_mul op_spec) - (spec_square_c op_spec) - (spec_div21 op_spec) - (spec_div_gt op_spec) - (spec_div op_spec) - (spec_mod_gt op_spec) - (spec_mod op_spec) - (spec_gcd_gt op_spec) - (spec_gcd op_spec) - (spec_head0 op_spec) - (spec_tail0 op_spec) - (spec_add_mul_div op_spec) - (spec_pos_mod) - (spec_is_even) - (spec_sqrt2) - (spec_sqrt) - (spec_W0 op_spec) - (spec_0W op_spec) - (spec_WW op_spec). + ZnZ.spec_to_Z + ZnZ.spec_of_pos + ZnZ.spec_0 + ZnZ.spec_1 + ZnZ.spec_m1 + ZnZ.spec_compare + ZnZ.spec_eq0 + ZnZ.spec_opp_c + ZnZ.spec_opp + ZnZ.spec_opp_carry + ZnZ.spec_succ_c + ZnZ.spec_add_c + ZnZ.spec_add_carry_c + ZnZ.spec_succ + ZnZ.spec_add + ZnZ.spec_add_carry + ZnZ.spec_pred_c + ZnZ.spec_sub_c + ZnZ.spec_sub_carry_c + ZnZ.spec_pred + ZnZ.spec_sub + ZnZ.spec_sub_carry + ZnZ.spec_mul_c + ZnZ.spec_mul + ZnZ.spec_square_c + ZnZ.spec_div21 + ZnZ.spec_div_gt + ZnZ.spec_div + ZnZ.spec_modulo_gt + ZnZ.spec_modulo + ZnZ.spec_gcd_gt + ZnZ.spec_gcd + ZnZ.spec_head0 + ZnZ.spec_tail0 + ZnZ.spec_add_mul_div + ZnZ.spec_pos_mod + ZnZ.spec_is_even + ZnZ.spec_sqrt2 + ZnZ.spec_sqrt + ZnZ.spec_WO + ZnZ.spec_OW + ZnZ.spec_WW. Ltac wwauto := unfold ww_to_Z; auto. @@ -395,16 +395,17 @@ Section Z_2nZ. Zpos p = (Z_of_N (fst (ww_of_pos p)))*wwB + [|(snd (ww_of_pos p))|]. Proof. unfold ww_of_pos;intros. - assert (H:= spec_of_pos op_spec p);unfold w_of_pos; - destruct (znz_of_pos w_op p). simpl in H. - rewrite H;clear H;destruct n;simpl to_Z. - simpl;unfold w_to_Z,w_0;rewrite (spec_0 op_spec);trivial. - unfold Z_of_N; assert (H:= spec_of_pos op_spec p0); - destruct (znz_of_pos w_op p0). simpl in H. - rewrite H;unfold fst, snd,Z_of_N, to_Z. - rewrite (spec_WW op_spec). + rewrite (ZnZ.spec_of_pos p). unfold w_of_pos. + case (ZnZ.of_pos p); intros. simpl. + destruct n; simpl ZnZ.to_Z. + simpl;unfold w_to_Z,w_0; rewrite ZnZ.spec_0;trivial. + unfold Z_of_N. + rewrite (ZnZ.spec_of_pos p0). + case (ZnZ.of_pos p0); intros. simpl. + unfold fst, snd,Z_of_N, to_Z, wB, w_digits, w_to_Z, w_WW. + rewrite ZnZ.spec_WW. replace wwB with (wB*wB). - unfold wB,w_to_Z,w_digits;clear H;destruct n;ring. + unfold wB,w_to_Z,w_digits;destruct n;ring. symmetry. rewrite <- Zpower_2; exact (wwB_wBwB w_digits). Qed. @@ -418,15 +419,9 @@ Section Z_2nZ. Proof. refine (spec_ww_Bm1 w_Bm1 w_digits w_to_Z _);auto. Qed. Let spec_ww_compare : - forall x y, - match compare x y with - | Eq => [|x|] = [|y|] - | Lt => [|x|] < [|y|] - | Gt => [|x|] > [|y|] - end. + forall x y, compare x y = Zcompare [|x|] [|y|]. Proof. refine (spec_ww_compare w_0 w_digits w_to_Z w_compare _ _ _);auto. - exact (spec_compare op_spec). Qed. Let spec_ww_eq0 : forall x, eq0 x = true -> [|x|] = 0. @@ -531,8 +526,7 @@ Section Z_2nZ. Proof. refine (spec_ww_karatsuba_c _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _); wwauto. - unfold w_digits; apply spec_more_than_1_digit; auto. - exact (spec_compare op_spec). + unfold w_digits; apply ZnZ.spec_more_than_1_digit; auto. Qed. Let spec_ww_mul : forall x y, [|mul x y|] = ([|x|] * [|y|]) mod wwB. @@ -559,11 +553,10 @@ Section Z_2nZ. w_add w_add_carry w_pred w_sub w_mul_c w_div21 sub_c w_digits w_to_Z _ _ _ _ _ _ _ _ _ _ _ _ _ _ _);wwauto. unfold w_Bm2, w_to_Z, w_pred, w_Bm1. - rewrite (spec_pred op_spec);rewrite (spec_Bm1 op_spec). + rewrite ZnZ.spec_pred, ZnZ.spec_m1. unfold w_digits;rewrite Zmod_small. ring. - assert (H:= wB_pos(znz_digits w_op)). omega. - exact (spec_compare op_spec). - exact (spec_div21 op_spec). + assert (H:= wB_pos(ZnZ.digits)). omega. + exact ZnZ.spec_div21. Qed. Let spec_ww_div21 : forall a1 a2 b, @@ -580,22 +573,19 @@ Section Z_2nZ. Let spec_add2: forall x y, [|w_add2 x y|] = w_to_Z x + w_to_Z y. unfold w_add2. - intros xh xl; generalize (spec_add_c op_spec xh xl). - unfold w_add_c; case znz_add_c; unfold interp_carry; simpl ww_to_Z. + intros xh xl; generalize (ZnZ.spec_add_c xh xl). + unfold w_add_c; case ZnZ.add_c; unfold interp_carry; simpl ww_to_Z. intros w0 Hw0; simpl; unfold w_to_Z; rewrite Hw0. - unfold w_0; rewrite spec_0; simpl; auto with zarith. + unfold w_0; rewrite ZnZ.spec_0; simpl; auto with zarith. intros w0; rewrite Zmult_1_l; simpl. - unfold w_to_Z, w_1; rewrite spec_1; auto with zarith. + unfold w_to_Z, w_1; rewrite ZnZ.spec_1; auto with zarith. rewrite Zmult_1_l; auto. Qed. Let spec_low: forall x, w_to_Z (low x) = [|x|] mod wB. intros x; case x; simpl low. - unfold ww_to_Z, w_to_Z, w_0; rewrite (spec_0 op_spec); simpl. - rewrite Zmod_small; auto with zarith. - split; auto with zarith. - unfold wB, base; auto with zarith. + unfold ww_to_Z, w_to_Z, w_0; rewrite ZnZ.spec_0; simpl; auto. intros xh xl; simpl. rewrite Zplus_comm; rewrite Z_mod_plus; auto with zarith. rewrite Zmod_small; auto with zarith. @@ -608,7 +598,7 @@ Section Z_2nZ. unfold w_to_Z, _ww_zdigits. rewrite spec_add2. unfold w_to_Z, w_zdigits, w_digits. - rewrite spec_zdigits; auto. + rewrite ZnZ.spec_zdigits; auto. rewrite Zpos_xO; auto with zarith. Qed. @@ -618,9 +608,8 @@ Section Z_2nZ. refine (spec_ww_head00 w_0 w_0W w_compare w_head0 w_add2 w_zdigits _ww_zdigits w_to_Z _ _ _ (refl_equal _ww_digits) _ _ _ _); auto. - exact (spec_compare op_spec). - exact (spec_head00 op_spec). - exact (spec_zdigits op_spec). + exact ZnZ.spec_head00. + exact ZnZ.spec_zdigits. Qed. Let spec_ww_head0 : forall x, 0 < [|x|] -> @@ -629,8 +618,7 @@ Section Z_2nZ. refine (spec_ww_head0 w_0 w_0W w_compare w_head0 w_add2 w_zdigits _ww_zdigits w_to_Z _ _ _ _ _ _ _);wwauto. - exact (spec_compare op_spec). - exact (spec_zdigits op_spec). + exact ZnZ.spec_zdigits. Qed. Let spec_ww_tail00 : forall x, [|x|] = 0 -> [|tail0 x|] = Zpos _ww_digits. @@ -638,9 +626,8 @@ Section Z_2nZ. refine (spec_ww_tail00 w_0 w_0W w_compare w_tail0 w_add2 w_zdigits _ww_zdigits w_to_Z _ _ _ (refl_equal _ww_digits) _ _ _ _); wwauto. - exact (spec_compare op_spec). - exact (spec_tail00 op_spec). - exact (spec_zdigits op_spec). + exact ZnZ.spec_tail00. + exact ZnZ.spec_zdigits. Qed. @@ -649,8 +636,7 @@ Section Z_2nZ. Proof. refine (spec_ww_tail0 (w_digits := w_digits) w_0 w_0W w_compare w_tail0 w_add2 w_zdigits _ww_zdigits w_to_Z _ _ _ _ _ _ _);wwauto. - exact (spec_compare op_spec). - exact (spec_zdigits op_spec). + exact ZnZ.spec_zdigits. Qed. Lemma spec_ww_add_mul_div : forall x y p, @@ -659,10 +645,10 @@ Section Z_2nZ. ([|x|] * (2 ^ [|p|]) + [|y|] / (2 ^ ((Zpos _ww_digits) - [|p|]))) mod wwB. Proof. - refine (@spec_ww_add_mul_div w w_0 w_WW w_W0 w_0W compare w_add_mul_div + refine (@spec_ww_add_mul_div t w_0 w_WW w_W0 w_0W compare w_add_mul_div sub w_digits w_zdigits low w_to_Z _ _ _ _ _ _ _ _ _ _ _);wwauto. - exact (spec_zdigits op_spec). + exact ZnZ.spec_zdigits. Qed. Let spec_ww_div_gt : forall a b, @@ -671,29 +657,29 @@ Section Z_2nZ. [|a|] = [|q|] * [|b|] + [|r|] /\ 0 <= [|r|] < [|b|]. Proof. refine -(@spec_ww_div_gt w w_digits w_0 w_WW w_0W w_compare w_eq0 +(@spec_ww_div_gt t w_digits w_0 w_WW w_0W w_compare w_eq0 w_opp_c w_opp w_opp_carry w_sub_c w_sub w_sub_carry w_div_gt w_add_mul_div w_head0 w_div21 div32 _ww_zdigits ww_1 add_mul_div w_zdigits w_to_Z _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ). - exact (spec_0 op_spec). - exact (spec_to_Z op_spec). + exact ZnZ.spec_0. + exact ZnZ.spec_to_Z. wwauto. wwauto. - exact (spec_compare op_spec). - exact (spec_eq0 op_spec). - exact (spec_opp_c op_spec). - exact (spec_opp op_spec). - exact (spec_opp_carry op_spec). - exact (spec_sub_c op_spec). - exact (spec_sub op_spec). - exact (spec_sub_carry op_spec). - exact (spec_div_gt op_spec). - exact (spec_add_mul_div op_spec). - exact (spec_head0 op_spec). - exact (spec_div21 op_spec). + exact ZnZ.spec_compare. + exact ZnZ.spec_eq0. + exact ZnZ.spec_opp_c. + exact ZnZ.spec_opp. + exact ZnZ.spec_opp_carry. + exact ZnZ.spec_sub_c. + exact ZnZ.spec_sub. + exact ZnZ.spec_sub_carry. + exact ZnZ.spec_div_gt. + exact ZnZ.spec_add_mul_div. + exact ZnZ.spec_head0. + exact ZnZ.spec_div21. exact spec_w_div32. - exact (spec_zdigits op_spec). + exact ZnZ.spec_zdigits. exact spec_ww_digits. exact spec_ww_1. exact spec_ww_add_mul_div. @@ -711,15 +697,14 @@ refine [|a|] > [|b|] -> 0 < [|b|] -> [|mod_gt a b|] = [|a|] mod [|b|]. Proof. - refine (@spec_ww_mod_gt w w_digits w_0 w_WW w_0W w_compare w_eq0 + refine (@spec_ww_mod_gt t w_digits w_0 w_WW w_0W w_compare w_eq0 w_opp_c w_opp w_opp_carry w_sub_c w_sub w_sub_carry w_div_gt w_mod_gt w_add_mul_div w_head0 w_div21 div32 _ww_zdigits ww_1 add_mul_div w_zdigits w_to_Z _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _);wwauto. - exact (spec_compare op_spec). - exact (spec_div_gt op_spec). - exact (spec_div21 op_spec). - exact (spec_zdigits op_spec). + exact ZnZ.spec_div_gt. + exact ZnZ.spec_div21. + exact ZnZ.spec_zdigits. exact spec_ww_add_mul_div. Qed. @@ -731,37 +716,33 @@ refine Let spec_ww_gcd_gt : forall a b, [|a|] > [|b|] -> Zis_gcd [|a|] [|b|] [|gcd_gt a b|]. Proof. - refine (@spec_ww_gcd_gt w w_digits W0 w_to_Z _ + refine (@spec_ww_gcd_gt t w_digits W0 w_to_Z _ w_0 w_0 w_eq0 w_gcd_gt _ww_digits _ gcd_gt_fix _ _ _ _ gcd_cont _);auto. - refine (@spec_ww_gcd_gt_aux w w_digits w_0 w_WW w_0W w_compare w_opp_c w_opp + refine (@spec_ww_gcd_gt_aux t w_digits w_0 w_WW w_0W w_compare w_opp_c w_opp w_opp_carry w_sub_c w_sub w_sub_carry w_gcd_gt w_add_mul_div w_head0 w_div21 div32 _ww_zdigits ww_1 add_mul_div w_zdigits w_to_Z _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _);wwauto. - exact (spec_compare op_spec). - exact (spec_div21 op_spec). - exact (spec_zdigits op_spec). + exact ZnZ.spec_div21. + exact ZnZ.spec_zdigits. exact spec_ww_add_mul_div. - refine (@spec_gcd_cont w w_digits ww_1 w_to_Z _ _ w_0 w_1 w_compare + refine (@spec_gcd_cont t w_digits ww_1 w_to_Z _ _ w_0 w_1 w_compare _ _);auto. - exact (spec_compare op_spec). Qed. Let spec_ww_gcd : forall a b, Zis_gcd [|a|] [|b|] [|gcd a b|]. Proof. - refine (@spec_ww_gcd w w_digits W0 compare w_to_Z _ _ w_0 w_0 w_eq0 w_gcd_gt + refine (@spec_ww_gcd t w_digits W0 compare w_to_Z _ _ w_0 w_0 w_eq0 w_gcd_gt _ww_digits _ gcd_gt_fix _ _ _ _ gcd_cont _);auto. - refine (@spec_ww_gcd_gt_aux w w_digits w_0 w_WW w_0W w_compare w_opp_c w_opp + refine (@spec_ww_gcd_gt_aux t w_digits w_0 w_WW w_0W w_compare w_opp_c w_opp w_opp_carry w_sub_c w_sub w_sub_carry w_gcd_gt w_add_mul_div w_head0 w_div21 div32 _ww_zdigits ww_1 add_mul_div w_zdigits w_to_Z _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _);wwauto. - exact (spec_compare op_spec). - exact (spec_div21 op_spec). - exact (spec_zdigits op_spec). + exact ZnZ.spec_div21. + exact ZnZ.spec_zdigits. exact spec_ww_add_mul_div. - refine (@spec_gcd_cont w w_digits ww_1 w_to_Z _ _ w_0 w_1 w_compare + refine (@spec_gcd_cont t w_digits ww_1 w_to_Z _ _ w_0 w_1 w_compare _ _);auto. - exact (spec_compare op_spec). Qed. Let spec_ww_is_even : forall x, @@ -770,8 +751,8 @@ refine | false => [|x|] mod 2 = 1 end. Proof. - refine (@spec_ww_is_even w w_is_even w_0 w_1 w_Bm1 w_digits _ _ _ _ _); auto. - exact (spec_is_even op_spec). + refine (@spec_ww_is_even t w_is_even w_0 w_1 w_Bm1 w_digits _ _ _ _ _); auto. + exact ZnZ.spec_is_even. Qed. Let spec_ww_sqrt2 : forall x y, @@ -781,60 +762,57 @@ refine [+|r|] <= 2 * [|s|]. Proof. intros x y H. - refine (@spec_ww_sqrt2 w w_is_even w_compare w_0 w_1 w_Bm1 + refine (@spec_ww_sqrt2 t w_is_even w_compare w_0 w_1 w_Bm1 w_0W w_sub w_square_c w_div21 w_add_mul_div w_digits w_zdigits _ww_zdigits w_add_c w_sqrt2 w_pred pred_c pred add_c add sub_c add_mul_div _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _); wwauto. - exact (spec_zdigits op_spec). - exact (spec_more_than_1_digit op_spec). - exact (spec_is_even op_spec). - exact (spec_compare op_spec). - exact (spec_div21 op_spec). - exact (spec_ww_add_mul_div). - exact (spec_sqrt2 op_spec). + exact ZnZ.spec_zdigits. + exact ZnZ.spec_more_than_1_digit. + exact ZnZ.spec_is_even. + exact ZnZ.spec_div21. + exact spec_ww_add_mul_div. + exact ZnZ.spec_sqrt2. Qed. Let spec_ww_sqrt : forall x, [|sqrt x|] ^ 2 <= [|x|] < ([|sqrt x|] + 1) ^ 2. Proof. - refine (@spec_ww_sqrt w w_is_even w_0 w_1 w_Bm1 + refine (@spec_ww_sqrt t w_is_even w_0 w_1 w_Bm1 w_sub w_add_mul_div w_digits w_zdigits _ww_zdigits w_sqrt2 pred add_mul_div head0 compare _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _); wwauto. - exact (spec_zdigits op_spec). - exact (spec_more_than_1_digit op_spec). - exact (spec_is_even op_spec). - exact (spec_ww_add_mul_div). - exact (spec_sqrt2 op_spec). + exact ZnZ.spec_zdigits. + exact ZnZ.spec_more_than_1_digit. + exact ZnZ.spec_is_even. + exact spec_ww_add_mul_div. + exact ZnZ.spec_sqrt2. Qed. - Lemma mk_znz2_spec : znz_spec mk_zn2z_op. + Global Instance mk_zn2z_specs : ZnZ.Specs mk_zn2z_ops. Proof. - apply mk_znz_spec;auto. + apply ZnZ.MkSpecs; auto. exact spec_ww_add_mul_div. - refine (@spec_ww_pos_mod w w_0 w_digits w_zdigits w_WW + refine (@spec_ww_pos_mod t w_0 w_digits w_zdigits w_WW w_pos_mod compare w_0W low sub _ww_zdigits w_to_Z _ _ _ _ _ _ _ _ _ _ _ _);wwauto. - exact (spec_pos_mod op_spec). - exact (spec_zdigits op_spec). + exact ZnZ.spec_zdigits. unfold w_to_Z, w_zdigits. - rewrite (spec_zdigits op_spec). + rewrite ZnZ.spec_zdigits. rewrite <- Zpos_xO; exact spec_ww_digits. Qed. - Lemma mk_znz2_karatsuba_spec : znz_spec mk_zn2z_op_karatsuba. + Global Instance mk_zn2z_specs_karatsuba : ZnZ.Specs mk_zn2z_ops_karatsuba. Proof. - apply mk_znz_spec;auto. + apply ZnZ.MkSpecs; auto. exact spec_ww_add_mul_div. - refine (@spec_ww_pos_mod w w_0 w_digits w_zdigits w_WW + refine (@spec_ww_pos_mod t w_0 w_digits w_zdigits w_WW w_pos_mod compare w_0W low sub _ww_zdigits w_to_Z _ _ _ _ _ _ _ _ _ _ _ _);wwauto. - exact (spec_pos_mod op_spec). - exact (spec_zdigits op_spec). + exact ZnZ.spec_zdigits. unfold w_to_Z, w_zdigits. - rewrite (spec_zdigits op_spec). + rewrite ZnZ.spec_zdigits. rewrite <- Zpos_xO; exact spec_ww_digits. Qed. @@ -842,17 +820,14 @@ End Z_2nZ. Section MulAdd. - Variable w: Type. - Variable op: znz_op w. - Variable sop: znz_spec op. + Context {t : Type}{ops : ZnZ.Ops t}{specs : ZnZ.Specs ops}. - Definition mul_add:= w_mul_add (znz_0 op) (znz_succ op) (znz_add_c op) (znz_mul_c op). + Definition mul_add:= w_mul_add ZnZ.zero ZnZ.succ ZnZ.add_c ZnZ.mul_c. - Notation "[| x |]" := (znz_to_Z op x) (at level 0, x at level 99). + Notation "[| x |]" := (ZnZ.to_Z x) (at level 0, x at level 99). Notation "[|| x ||]" := - (zn2z_to_Z (base (znz_digits op)) (znz_to_Z op) x) (at level 0, x at level 99). - + (zn2z_to_Z (base ZnZ.digits) ZnZ.to_Z x) (at level 0, x at level 99). Lemma spec_mul_add: forall x y z, let (zh, zl) := mul_add x y z in @@ -860,11 +835,11 @@ Section MulAdd. Proof. intros x y z. refine (spec_w_mul_add _ _ _ _ _ _ _ _ _ _ _ _ x y z); auto. - exact (spec_0 sop). - exact (spec_to_Z sop). - exact (spec_succ sop). - exact (spec_add_c sop). - exact (spec_mul_c sop). + exact ZnZ.spec_0. + exact ZnZ.spec_to_Z. + exact ZnZ.spec_succ. + exact ZnZ.spec_add_c. + exact ZnZ.spec_mul_c. Qed. End MulAdd. @@ -873,13 +848,13 @@ End MulAdd. (** Modular versions of DoubleCyclic *) Module DoubleCyclic (C:CyclicType) <: CyclicType. - Definition w := zn2z C.w. - Definition w_op := mk_zn2z_op C.w_op. - Definition w_spec := mk_znz2_spec C.w_spec. + Definition t := zn2z C.t. + Instance ops : ZnZ.Ops t := mk_zn2z_ops. + Instance specs : ZnZ.Specs ops := mk_zn2z_specs. End DoubleCyclic. Module DoubleCyclicKaratsuba (C:CyclicType) <: CyclicType. - Definition w := zn2z C.w. - Definition w_op := mk_zn2z_op_karatsuba C.w_op. - Definition w_spec := mk_znz2_karatsuba_spec C.w_spec. + Definition t := zn2z C.t. + Definition ops : ZnZ.Ops t := mk_zn2z_ops_karatsuba. + Definition specs : ZnZ.Specs ops := mk_zn2z_specs_karatsuba. End DoubleCyclicKaratsuba. diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v index 9204b4e05..1ce1e81b0 100644 --- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v +++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v @@ -82,11 +82,7 @@ Section POS_MOD. Variable spec_w_0W : forall l, [[w_0W l]] = [|l|]. Variable spec_ww_compare : forall x y, - match ww_compare x y with - | Eq => [[x]] = [[y]] - | Lt => [[x]] < [[y]] - | Gt => [[x]] > [[y]] - end. + ww_compare x y = Zcompare [[x]] [[y]]. Variable spec_ww_sub: forall x y, [[ww_sub x y]] = ([[x]] - [[y]]) mod wwB. @@ -105,8 +101,8 @@ Section POS_MOD. intros w1 p; case (spec_to_w_Z p); intros HH1 HH2. unfold ww_pos_mod; case w1. simpl; rewrite Zmod_small; split; auto with zarith. - intros xh xl; generalize (spec_ww_compare p (w_0W w_zdigits)); - case ww_compare; + intros xh xl; rewrite spec_ww_compare. + case Zcompare_spec; rewrite spec_w_0W; rewrite spec_zdigits; fold wB; intros H1. rewrite H1; simpl ww_to_Z. @@ -134,8 +130,8 @@ Section POS_MOD. rewrite Z_mod_mult; auto with zarith. autorewrite with w_rewrite rm10. rewrite Zmod_mod; auto with zarith. -generalize (spec_ww_compare p ww_zdigits); - case ww_compare; rewrite spec_ww_zdigits; + rewrite spec_ww_compare. + case Zcompare_spec; rewrite spec_ww_zdigits; rewrite spec_zdigits; intros H2. replace (2^[[p]]) with wwB. rewrite Zmod_small; auto with zarith. @@ -266,12 +262,7 @@ Section DoubleDiv32. Variable spec_w_WW : forall h l, [[w_WW h l]] = [|h|] * wB + [|l|]. Variable spec_compare : - forall x y, - match w_compare x y with - | Eq => [|x|] = [|y|] - | Lt => [|x|] < [|y|] - | Gt => [|x|] > [|y|] - end. + forall x y, w_compare x y = Zcompare [|x|] [|y|]. Variable spec_w_add_c : forall x y, [+|w_add_c x y|] = [|x|] + [|y|]. Variable spec_w_add_carry_c : forall x y, [+|w_add_carry_c x y|] = [|x|] + [|y|] + 1. @@ -343,7 +334,7 @@ Section DoubleDiv32. (WW (w_sub a2 b2) a3) (WW b1 b2) | Gt => (w_0, W0) (* cas absurde *) end. - assert (Hcmp:=spec_compare a1 b1);destruct (w_compare a1 b1). + rewrite spec_compare. case Zcompare_spec; intro Hcmp. simpl in Hlt. rewrite Hcmp in Hlt;assert ([|a2|] < [|b2|]). omega. assert ([[WW (w_sub a2 b2) a3]] = ([|a2|]-[|b2|])*wB + [|a3|] + wwB). @@ -545,11 +536,7 @@ Section DoubleDiv21. 0 <= [[r]] < [|b1|] * wB + [|b2|]. Variable spec_ww_1 : [[ww_1]] = 1. Variable spec_ww_compare : forall x y, - match ww_compare x y with - | Eq => [[x]] = [[y]] - | Lt => [[x]] < [[y]] - | Gt => [[x]] > [[y]] - end. + ww_compare x y = Zcompare [[x]] [[y]]. Variable spec_ww_sub : forall x y, [[ww_sub x y]] = ([[x]] - [[y]]) mod wwB. Theorem wwB_div: wwB = 2 * (wwB / 2). @@ -576,10 +563,9 @@ Section DoubleDiv21. intros a1 a2 b H Hlt; unfold ww_div21. Spec_ww_to_Z b; assert (Eq: 0 < [[b]]). Spec_ww_to_Z a1;omega. generalize Hlt H ;clear Hlt H;case a1. - intros H1 H2;simpl in H1;Spec_ww_to_Z a2; - match goal with |-context [ww_compare ?Y ?Z] => - generalize (spec_ww_compare Y Z); case (ww_compare Y Z) - end; simpl;try rewrite spec_ww_1;autorewrite with rm10; intros;zarith. + intros H1 H2;simpl in H1;Spec_ww_to_Z a2. + rewrite spec_ww_compare. case Zcompare_spec; + simpl;try rewrite spec_ww_1;autorewrite with rm10; intros;zarith. rewrite spec_ww_sub;simpl. rewrite Zmod_small;zarith. split. ring. assert (wwB <= 2*[[b]]);zarith. @@ -809,12 +795,7 @@ Section DoubleDivGt. Variable spec_w_WW : forall h l, [[w_WW h l]] = [|h|] * wB + [|l|]. Variable spec_w_0W : forall l, [[w_0W l]] = [|l|]. Variable spec_compare : - forall x y, - match w_compare x y with - | Eq => [|x|] = [|y|] - | Lt => [|x|] < [|y|] - | Gt => [|x|] > [|y|] - end. + forall x y, w_compare x y = Zcompare [|x|] [|y|]. Variable spec_eq0 : forall x, w_eq0 x = true -> [|x|] = 0. Variable spec_opp_c : forall x, [-|w_opp_c x|] = -[|x|]. @@ -914,7 +895,7 @@ Section DoubleDivGt. end in [[WW ah al]]=[[q]]*[[WW bh bl]]+[[r]] /\ 0 <=[[r]]< [[WW bh bl]]). assert (Hh := spec_head0 Hpos). lazy zeta. - generalize (spec_compare (w_head0 bh) w_0); case w_compare; + rewrite spec_compare; case Zcompare_spec; rewrite spec_w_0; intros HH. generalize Hh; rewrite HH; simpl Zpower; rewrite Zmult_1_l; intros (HH1, HH2); clear HH. @@ -1058,7 +1039,7 @@ Section DoubleDivGt. assert (H2:=spec_div_gt Hgt Hpos);destruct (w_div_gt al bl). repeat rewrite spec_w_0W;simpl;rewrite spec_w_0;simpl;trivial. clear H. - assert (Hcmp := spec_compare w_0 bh); destruct (w_compare w_0 bh). + rewrite spec_compare; case Zcompare_spec; intros Hcmp. rewrite spec_w_0 in Hcmp. change [[WW bh bl]] with ([|bh|]*wB+[|bl|]). rewrite <- Hcmp;rewrite Zmult_0_l;rewrite Zplus_0_l. simpl in Hpos;rewrite <- Hcmp in Hpos;simpl in Hpos. @@ -1154,7 +1135,7 @@ Section DoubleDivGt. rewrite spec_w_0W;rewrite spec_w_mod_gt_eq;trivial. destruct (w_div_gt al bl);simpl;rewrite spec_w_0W;trivial. clear H. - assert (H2 := spec_compare w_0 bh);destruct (w_compare w_0 bh). + rewrite spec_compare; case Zcompare_spec; intros H2. rewrite (@spec_double_modn1_aux w w_zdigits w_0 w_WW w_head0 w_add_mul_div w_div21 w_compare w_sub w_to_Z spec_w_0 spec_compare 1 (WW ah al) bl). destruct (double_divn1 w_zdigits w_0 w_WW w_head0 w_add_mul_div w_div21 w_compare w_sub 1 @@ -1227,13 +1208,14 @@ Section DoubleDivGt. end | Gt => W0 (* absurde *) end). - assert (Hbh := spec_compare w_0 bh);destruct (w_compare w_0 bh). - simpl ww_to_Z in *. rewrite spec_w_0 in Hbh;rewrite <- Hbh; + rewrite spec_compare, spec_w_0. + case Zcompare_spec; intros Hbh. + simpl ww_to_Z in *. rewrite <- Hbh. rewrite Zmult_0_l;rewrite Zplus_0_l. - assert (Hbl := spec_compare w_0 bl); destruct (w_compare w_0 bl). - rewrite spec_w_0 in Hbl;rewrite <- Hbl;apply Zis_gcd_0. + rewrite spec_compare, spec_w_0. + case Zcompare_spec; intros Hbl. + rewrite <- Hbl;apply Zis_gcd_0. simpl;rewrite spec_w_0;rewrite Zmult_0_l;rewrite Zplus_0_l. - rewrite spec_w_0 in Hbl. apply Zis_gcd_mod;zarith. change ([|ah|] * wB + [|al|]) with (double_to_Z w_digits w_to_Z 1 (WW ah al)). rewrite <- (@spec_double_modn1 w w_digits w_zdigits w_0 w_WW w_head0 w_add_mul_div @@ -1243,20 +1225,20 @@ Section DoubleDivGt. rewrite (@spec_double_modn1 w w_digits w_zdigits w_0 w_WW); trivial. apply Zlt_gt;match goal with | |- ?x mod ?y < ?y => destruct (Z_mod_lt x y);zarith end. - rewrite spec_w_0 in Hbl;Spec_w_to_Z bl;exfalso;omega. - rewrite spec_w_0 in Hbh;assert (H:= spec_ww_mod_gt_aux _ _ _ Hgt Hbh). + Spec_w_to_Z bl;exfalso;omega. + assert (H:= spec_ww_mod_gt_aux _ _ _ Hgt Hbh). assert (H2 : 0 < [[WW bh bl]]). simpl;Spec_w_to_Z bl. apply Zlt_le_trans with ([|bh|]*wB);zarith. apply Zmult_lt_0_compat;zarith. apply Zis_gcd_mod;trivial. rewrite <- H. simpl in *;destruct (ww_mod_gt_aux ah al bh bl) as [ |mh ml]. simpl;apply Zis_gcd_0;zarith. - assert (Hmh := spec_compare w_0 mh);destruct (w_compare w_0 mh). - simpl;rewrite spec_w_0 in Hmh; rewrite <- Hmh;simpl. - assert (Hml := spec_compare w_0 ml);destruct (w_compare w_0 ml). - rewrite <- Hml;rewrite spec_w_0;simpl;apply Zis_gcd_0. - simpl;rewrite spec_w_0;simpl. - rewrite spec_w_0 in Hml. apply Zis_gcd_mod;zarith. + rewrite spec_compare, spec_w_0; case Zcompare_spec; intros Hmh. + simpl;rewrite <- Hmh;simpl. + rewrite spec_compare, spec_w_0; case Zcompare_spec; intros Hml. + rewrite <- Hml;simpl;apply Zis_gcd_0. + simpl; rewrite spec_w_0; simpl. + apply Zis_gcd_mod;zarith. change ([|bh|] * wB + [|bl|]) with (double_to_Z w_digits w_to_Z 1 (WW bh bl)). rewrite <- (@spec_double_modn1 w w_digits w_zdigits w_0 w_WW w_head0 w_add_mul_div w_div21 w_compare w_sub w_to_Z spec_to_Z spec_w_zdigits spec_w_0 spec_w_WW spec_head0 spec_add_mul_div @@ -1265,8 +1247,8 @@ Section DoubleDivGt. rewrite (@spec_double_modn1 w w_digits w_zdigits w_0 w_WW); trivial. apply Zlt_gt;match goal with | |- ?x mod ?y < ?y => destruct (Z_mod_lt x y);zarith end. - rewrite spec_w_0 in Hml;Spec_w_to_Z ml;exfalso;omega. - rewrite spec_w_0 in Hmh. assert ([[WW bh bl]] > [[WW mh ml]]). + Spec_w_to_Z ml;exfalso;omega. + assert ([[WW bh bl]] > [[WW mh ml]]). rewrite H;simpl; apply Zlt_gt;match goal with | |- ?x mod ?y < ?y => destruct (Z_mod_lt x y);zarith end. assert (H1:= spec_ww_mod_gt_aux _ _ _ H0 Hmh). @@ -1300,8 +1282,8 @@ Section DoubleDivGt. rewrite Z_div_mult;zarith. assert (2^1 <= 2^n). change (2^1) with 2;zarith. assert (H7 := @Zpower_le_monotone_inv 2 1 n);zarith. - rewrite spec_w_0 in Hmh;Spec_w_to_Z mh;exfalso;zarith. - rewrite spec_w_0 in Hbh;Spec_w_to_Z bh;exfalso;zarith. + Spec_w_to_Z mh;exfalso;zarith. + Spec_w_to_Z bh;exfalso;zarith. Qed. Lemma spec_ww_gcd_gt_aux : @@ -1374,11 +1356,7 @@ Section DoubleDiv. Variable spec_to_Z : forall x, 0 <= [|x|] < wB. Variable spec_ww_1 : [[ww_1]] = 1. Variable spec_ww_compare : forall x y, - match ww_compare x y with - | Eq => [[x]] = [[y]] - | Lt => [[x]] < [[y]] - | Gt => [[x]] > [[y]] - end. + ww_compare x y = Zcompare [[x]] [[y]]. Variable spec_ww_div_gt : forall a b, [[a]] > [[b]] -> 0 < [[b]] -> let (q,r) := ww_div_gt a b in [[a]] = [[q]] * [[b]] + [[r]] /\ @@ -1400,20 +1378,20 @@ Section DoubleDiv. 0 <= [[r]] < [[b]]. Proof. intros a b Hpos;unfold ww_div. - assert (H:=spec_ww_compare a b);destruct (ww_compare a b). + rewrite spec_ww_compare; case Zcompare_spec; intros. simpl;rewrite spec_ww_1;split;zarith. simpl;split;[ring|Spec_ww_to_Z a;zarith]. - apply spec_ww_div_gt;trivial. + apply spec_ww_div_gt;auto with zarith. Qed. Lemma spec_ww_mod : forall a b, 0 < [[b]] -> [[ww_mod a b]] = [[a]] mod [[b]]. Proof. intros a b Hpos;unfold ww_mod. - assert (H := spec_ww_compare a b);destruct (ww_compare a b). + rewrite spec_ww_compare; case Zcompare_spec; intros. simpl;apply Zmod_unique with 1;try rewrite H;zarith. Spec_ww_to_Z a;symmetry;apply Zmod_small;zarith. - apply spec_ww_mod_gt;trivial. + apply spec_ww_mod_gt;auto with zarith. Qed. @@ -1431,12 +1409,7 @@ Section DoubleDiv. Variable spec_w_0 : [|w_0|] = 0. Variable spec_w_1 : [|w_1|] = 1. Variable spec_compare : - forall x y, - match w_compare x y with - | Eq => [|x|] = [|y|] - | Lt => [|x|] < [|y|] - | Gt => [|x|] > [|y|] - end. + forall x y, w_compare x y = Zcompare [|x|] [|y|]. Variable spec_eq0 : forall x, w_eq0 x = true -> [|x|] = 0. Variable spec_gcd_gt : forall a b, [|a|] > [|b|] -> Zis_gcd [|a|] [|b|] [|w_gcd_gt a b|]. @@ -1468,14 +1441,14 @@ Section DoubleDiv. assert (0 <= 1 < wB). split;zarith. apply wB_pos. assert (H1:= beta_lex _ _ _ _ _ Hle (spec_to_Z yl) H). Spec_w_to_Z yh;zarith. - unfold gcd_cont;assert (Hcmpy:=spec_compare w_1 yl); - rewrite spec_w_1 in Hcmpy. - simpl;rewrite H;simpl;destruct (w_compare w_1 yl). + unfold gcd_cont; rewrite spec_compare, spec_w_1. + case Zcompare_spec; intros Hcmpy. + simpl;rewrite H;simpl; rewrite spec_ww_1;rewrite <- Hcmpy;apply Zis_gcd_mod;zarith. rewrite <- (Zmod_unique ([|xh|]*wB+[|xl|]) 1 ([|xh|]*wB+[|xl|]) 0);zarith. rewrite H in Hle; exfalso;zarith. - assert ([|yl|] = 0). Spec_w_to_Z yl;zarith. - rewrite H0;simpl;apply Zis_gcd_0;trivial. + assert (H0 : [|yl|] = 0) by (Spec_w_to_Z yl;zarith). + simpl. rewrite H0, H;simpl;apply Zis_gcd_0;trivial. Qed. @@ -1528,7 +1501,7 @@ Section DoubleDiv. | Eq => a | Lt => ww_gcd_gt b a end). - assert (Hcmp := spec_ww_compare a b);destruct (ww_compare a b). + rewrite spec_ww_compare; case Zcompare_spec; intros Hcmp. Spec_ww_to_Z b;rewrite Hcmp. apply Zis_gcd_for_euclid with 1;zarith. ring_simplify ([[b]] - 1 * [[b]]). apply Zis_gcd_0;zarith. diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v index 386bbb9e5..136f96c04 100644 --- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v +++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v @@ -62,12 +62,7 @@ Section GENDIVN1. [|a1|] *wB+ [|a2|] = [|q|] * [|b|] + [|r|] /\ 0 <= [|r|] < [|b|]. Variable spec_compare : - forall x y, - match w_compare x y with - | Eq => [|x|] = [|y|] - | Lt => [|x|] < [|y|] - | Gt => [|x|] > [|y|] - end. + forall x y, w_compare x y = Zcompare [|x|] [|y|]. Variable spec_sub: forall x y, [|w_sub x y|] = ([|x|] - [|y|]) mod wB. @@ -373,7 +368,7 @@ Section GENDIVN1. intros n a b H. unfold double_divn1. case (spec_head0 H); intros H0 H1. case (spec_to_Z (w_head0 b)); intros HH1 HH2. - generalize (spec_compare (w_head0 b) w_0); case w_compare; + rewrite spec_compare; case Zcompare_spec; rewrite spec_0; intros H2; auto with zarith. assert (Hv1: wB/2 <= [|b|]). generalize H0; rewrite H2; rewrite Zpower_0_r; @@ -506,7 +501,7 @@ Section GENDIVN1. double_modn1 n a b = snd (double_divn1 n a b). Proof. intros n a b;unfold double_divn1,double_modn1. - generalize (spec_compare (w_head0 b) w_0); case w_compare; + rewrite spec_compare; case Zcompare_spec; rewrite spec_0; intros H2; auto with zarith. apply spec_double_modn1_0. apply spec_double_modn1_0. diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.v index 21e694e57..3405b6f4d 100644 --- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.v +++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.v @@ -106,17 +106,9 @@ Section DoubleLift. Variable spec_w_W0 : forall h, [[w_W0 h]] = [|h|] * wB. Variable spec_w_0W : forall l, [[w_0W l]] = [|l|]. Variable spec_compare : forall x y, - match w_compare x y with - | Eq => [|x|] = [|y|] - | Lt => [|x|] < [|y|] - | Gt => [|x|] > [|y|] - end. + w_compare x y = Zcompare [|x|] [|y|]. Variable spec_ww_compare : forall x y, - match ww_compare x y with - | Eq => [[x]] = [[y]] - | Lt => [[x]] < [[y]] - | Gt => [[x]] > [[y]] - end. + ww_compare x y = Zcompare [[x]] [[y]]. Variable spec_ww_digits : ww_Digits = xO w_digits. Variable spec_w_head00 : forall x, [|x|] = 0 -> [|w_head0 x|] = Zpos w_digits. Variable spec_w_head0 : forall x, 0 < [|x|] -> @@ -159,7 +151,7 @@ Section DoubleLift. absurd (0 < [|xh|] * wB + [|xl|]); auto with zarith. rewrite <- Hy3; rewrite Zplus_0_r; auto with zarith. apply Zmult_lt_0_compat; auto with zarith. - generalize (spec_compare w_0 xh); case w_compare. + rewrite spec_compare. case Zcompare_spec. intros H; simpl. rewrite spec_w_add; rewrite spec_w_head00. rewrite spec_zdigits; rewrite spec_ww_digits. @@ -176,9 +168,8 @@ Section DoubleLift. rewrite wwB_div_2;rewrite Zmult_comm;rewrite wwB_wBwB. assert (U:= lt_0_wB w_digits); destruct x as [ |xh xl];simpl ww_to_Z;intros H. unfold Zlt in H;discriminate H. - assert (H0 := spec_compare w_0 xh);rewrite spec_w_0 in H0. - destruct (w_compare w_0 xh). - rewrite <- H0. simpl Zplus. rewrite <- H0 in H;simpl in H. + rewrite spec_compare, spec_w_0. case Zcompare_spec; intros H0. + rewrite <- H0 in *. simpl Zplus. simpl in H. case (spec_to_Z w_zdigits); case (spec_to_Z (w_head0 xl)); intros HH1 HH2 HH3 HH4. rewrite spec_w_add. @@ -233,7 +224,7 @@ Section DoubleLift. apply Zmult_lt_0_compat; auto with zarith. assert (F2: [|xl|] = 0). rewrite F1 in Hx; auto with zarith. - generalize (spec_compare w_0 xl); case w_compare. + rewrite spec_compare; case Zcompare_spec. intros H; simpl. rewrite spec_w_add; rewrite spec_w_tail00; auto. rewrite spec_zdigits; rewrite spec_ww_digits. @@ -248,8 +239,7 @@ Section DoubleLift. clear spec_ww_zdigits. destruct x as [ |xh xl];simpl ww_to_Z;intros H. unfold Zlt in H;discriminate H. - assert (H0 := spec_compare w_0 xl);rewrite spec_w_0 in H0. - destruct (w_compare w_0 xl). + rewrite spec_compare, spec_w_0. case Zcompare_spec; intros H0. rewrite <- H0; rewrite Zplus_0_r. case (spec_to_Z (w_tail0 xh)); intros HH1 HH2. generalize H; rewrite <- H0; rewrite Zplus_0_r; clear H; intros H. @@ -323,7 +313,7 @@ Section DoubleLift. assert (Hx := spec_ww_to_Z w_digits w_to_Z spec_to_Z (WW xh xl)); simpl in Hx;assert (Hyh := spec_to_Z yh);assert (Hyl:=spec_to_Z yl); assert (Hy:=spec_ww_to_Z w_digits w_to_Z spec_to_Z (WW yh yl));simpl in Hy. - generalize (spec_ww_compare p zdigits); case ww_compare; intros H1. + rewrite spec_ww_compare; case Zcompare_spec; intros H1. rewrite H1; unfold zdigits; rewrite spec_w_0W. rewrite spec_zdigits; rewrite Zminus_diag; rewrite Zplus_0_r. simpl ww_to_Z; w_rewrite;zarith. @@ -365,7 +355,7 @@ Section DoubleLift. ring_simplify ([[p]] + (Zpos w_digits - [[p]]));fold wB;zarith. assert (Hv: [[p]] > Zpos w_digits). generalize H1; clear H1. - unfold zdigits; rewrite spec_w_0W; rewrite spec_zdigits; auto. + unfold zdigits; rewrite spec_w_0W; rewrite spec_zdigits; auto with zarith. clear H1. assert (HH0: [|low (ww_sub p zdigits)|] = [[p]] - Zpos w_digits). rewrite spec_low. @@ -446,8 +436,7 @@ Section DoubleLift. clear H1;w_rewrite);simpl ww_add_mul_div. replace [[WW w_0 w_0]] with 0;[w_rewrite|simpl;w_rewrite;trivial]. intros Heq;rewrite <- Heq;clear Heq; auto. - generalize (spec_ww_compare p (w_0W w_zdigits)); - case ww_compare; intros H1; w_rewrite. + rewrite spec_ww_compare. case Zcompare_spec; intros H1; w_rewrite. rewrite (spec_w_add_mul_div w_0 w_0);w_rewrite;zarith. generalize H1; w_rewrite; rewrite spec_zdigits; clear H1; intros H1. assert (HH0: [|low p|] = [[p]]). @@ -464,7 +453,8 @@ Section DoubleLift. rewrite (spec_w_add_mul_div w_0 w_0);w_rewrite;zarith. rewrite Zpos_xO in H;zarith. assert (HH: [|low (ww_sub p (w_0W w_zdigits)) |] = [[p]] - Zpos w_digits). - generalize H1; clear H1. + symmetry in H1; change ([[p]] > [[w_0W w_zdigits]]) in H1. + revert H1. rewrite spec_low. rewrite spec_ww_sub; w_rewrite; intros H1. rewrite <- Zmod_div_mod; auto with zarith. diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.v index 7090c76a8..6a2a34449 100644 --- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.v +++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.v @@ -248,12 +248,7 @@ Section DoubleMul. Variable spec_w_W0 : forall h, [[w_W0 h]] = [|h|] * wB. Variable spec_w_0W : forall l, [[w_0W l]] = [|l|]. Variable spec_w_compare : - forall x y, - match w_compare x y with - | Eq => [|x|] = [|y|] - | Lt => [|x|] < [|y|] - | Gt => [|x|] > [|y|] - end. + forall x y, w_compare x y = Zcompare [|x|] [|y|]. Variable spec_w_succ : forall x, [|w_succ x|] = ([|x|] + 1) mod wB. Variable spec_w_add_c : forall x y, [+|w_add_c x y|] = [|x|] + [|y|]. Variable spec_w_add : forall x y, [|w_add x y|] = ([|x|] + [|y|]) mod wB. @@ -408,9 +403,9 @@ Section DoubleMul. assert (Hyh := (spec_to_Z yh)); assert (Hyl := (spec_to_Z yl)). generalize (spec_ww_add_c hh ll); case (ww_add_c hh ll); intros z Hz; rewrite <- Hz; unfold interp_carry; assert (Hz1 := (spec_ww_to_Z z)). - generalize (spec_w_compare xl xh); case (w_compare xl xh); intros Hxlh; + rewrite spec_w_compare; case Zcompare_spec; intros Hxlh; try rewrite Hxlh; try rewrite spec_w_0; try (ring; fail). - generalize (spec_w_compare yl yh); case (w_compare yl yh); intros Hylh. + rewrite spec_w_compare; case Zcompare_spec; intros Hylh. rewrite Hylh; rewrite spec_w_0; try (ring; fail). rewrite spec_w_0; try (ring; fail). repeat (rewrite spec_ww_sub || rewrite spec_w_sub || rewrite spec_w_mul_c). @@ -430,7 +425,7 @@ Section DoubleMul. rewrite spec_w_1; unfold interp_carry in Hz2; rewrite Hz2; repeat (rewrite spec_w_sub || rewrite spec_w_mul_c). repeat rewrite Zmod_small; auto with zarith; try (ring; fail). - generalize (spec_w_compare yl yh); case (w_compare yl yh); intros Hylh. + rewrite spec_w_compare; case Zcompare_spec; intros Hylh. rewrite Hylh; rewrite spec_w_0; try (ring; fail). match goal with |- context[ww_add_c ?x ?y] => generalize (spec_ww_add_c x y); case (ww_add_c x y); try rewrite spec_w_0; @@ -455,9 +450,9 @@ Section DoubleMul. apply Zmult_le_0_compat; auto with zarith. (** there is a carry in hh + ll **) rewrite Zmult_1_l. - generalize (spec_w_compare xl xh); case (w_compare xl xh); intros Hxlh; + rewrite spec_w_compare; case Zcompare_spec; intros Hxlh; try rewrite Hxlh; try rewrite spec_w_1; try (ring; fail). - generalize (spec_w_compare yl yh); case (w_compare yl yh); intros Hylh; + rewrite spec_w_compare; case Zcompare_spec; intros Hylh; try rewrite Hylh; try rewrite spec_w_1; try (ring; fail). match goal with |- context[ww_sub_c ?x ?y] => generalize (spec_ww_sub_c x y); case (ww_sub_c x y); try rewrite spec_w_1; @@ -480,7 +475,7 @@ Section DoubleMul. ring. rewrite Hz2; repeat (rewrite spec_w_sub || rewrite spec_w_mul_c). repeat rewrite Zmod_small; auto with zarith; try (ring; fail). - generalize (spec_w_compare yl yh); case (w_compare yl yh); intros Hylh; + rewrite spec_w_compare; case Zcompare_spec; intros Hylh; try rewrite Hylh; try rewrite spec_w_1; try (ring; fail). match goal with |- context[ww_add_c ?x ?y] => generalize (spec_ww_add_c x y); case (ww_add_c x y); try rewrite spec_w_1; diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v index 83a2e7177..ee12c6a8d 100644 --- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v +++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v @@ -220,12 +220,8 @@ Section DoubleSqrt. Variable spec_w_0W : forall l, [[w_0W l]] = [|l|]. Variable spec_w_is_even : forall x, if w_is_even x then [|x|] mod 2 = 0 else [|x|] mod 2 = 1. - Variable spec_w_compare : forall x y, - match w_compare x y with - | Eq => [|x|] = [|y|] - | Lt => [|x|] < [|y|] - | Gt => [|x|] > [|y|] - end. + Variable spec_w_compare : forall x y, + w_compare x y = Zcompare [|x|] [|y|]. Variable spec_w_sub : forall x y, [|w_sub x y|] = ([|x|] - [|y|]) mod wB. Variable spec_w_square_c : forall x, [[ w_square_c x]] = [|x|] * [|x|]. Variable spec_w_div21 : forall a1 a2 b, @@ -257,11 +253,7 @@ Section DoubleSqrt. Variable spec_ww_pred : forall x, [[ww_pred x]] = ([[x]] - 1) mod wwB. Variable spec_ww_add_c : forall x y, [+[ww_add_c x y]] = [[x]] + [[y]]. Variable spec_ww_compare : forall x y, - match ww_compare x y with - | Eq => [[x]] = [[y]] - | Lt => [[x]] < [[y]] - | Gt => [[x]] > [[y]] - end. + ww_compare x y = Zcompare [[x]] [[y]]. Variable spec_ww_head0 : forall x, 0 < [[x]] -> wwB/ 2 <= 2 ^ [[ww_head0 x]] * [[x]] < wwB. Variable spec_low: forall x, [|low x|] = [[x]] mod wB. @@ -299,10 +291,7 @@ intros x; case x; simpl ww_is_even. apply Zlt_le_trans with (2 := Hb); auto with zarith. apply Zlt_le_trans with 1; auto with zarith. apply Zdiv_le_lower_bound; auto with zarith. - repeat match goal with |- context[w_compare ?y ?z] => - generalize (spec_w_compare y z); - case (w_compare y z) - end. + rewrite !spec_w_compare. repeat case Zcompare_spec. intros H1 H2; split. unfold interp_carry; autorewrite with w_rewrite rm10; auto with zarith. rewrite H1; rewrite H2; ring. @@ -1113,7 +1102,7 @@ intros x; case x; simpl ww_is_even. Lemma spec_ww_is_zero: forall x, if ww_is_zero x then [[x]] = 0 else 0 < [[x]]. intro x; unfold ww_is_zero. - generalize (spec_ww_compare W0 x); case (ww_compare W0 x); + rewrite spec_ww_compare. case Zcompare_spec; auto with zarith. simpl ww_to_Z. assert (V4 := spec_ww_to_Z w_digits w_to_Z spec_to_Z x);auto with zarith. @@ -1198,7 +1187,7 @@ intros x; case x; simpl ww_is_even. simpl ww_to_Z; simpl Zpower; unfold Zpower_pos; simpl; auto with zarith. intros H1. - generalize (spec_ww_compare (ww_head1 x) W0); case ww_compare; + rewrite spec_ww_compare. case Zcompare_spec; simpl ww_to_Z; autorewrite with rm10. generalize H1; case x. intros HH; contradict HH; simpl ww_to_Z; auto with zarith. diff --git a/theories/Numbers/Cyclic/Int31/Cyclic31.v b/theories/Numbers/Cyclic/Int31/Cyclic31.v index 744f2f47c..99bac5d7e 100644 --- a/theories/Numbers/Cyclic/Int31/Cyclic31.v +++ b/theories/Numbers/Cyclic/Int31/Cyclic31.v @@ -1106,81 +1106,61 @@ Section Basics. End Basics. - -Section Int31_Op. - -(** Nullity test *) -Let w_iszero i := match i ?= 0 with Eq => true | _ => false end. - -(** Modulo [2^p] *) -Let w_pos_mod p i := - match compare31 p 31 with +Instance int31_ops : ZnZ.Ops int31 := +{ + digits := 31%positive; (* number of digits *) + zdigits := 31; (* number of digits *) + to_Z := phi; (* conversion to Z *) + of_pos := positive_to_int31; (* positive -> N*int31 : p => N,i + where p = N*2^31+phi i *) + head0 := head031; (* number of head 0 *) + tail0 := tail031; (* number of tail 0 *) + zero := 0; + one := 1; + minus_one := Tn; (* 2^31 - 1 *) + compare := compare31; + eq0 := fun i => match i ?= 0 with Eq => true | _ => false end; + opp_c := fun i => 0 -c i; + opp := opp31; + opp_carry := fun i => 0-i-1; + succ_c := fun i => i +c 1; + add_c := add31c; + add_carry_c := add31carryc; + succ := fun i => i + 1; + add := add31; + add_carry := fun i j => i + j + 1; + pred_c := fun i => i -c 1; + sub_c := sub31c; + sub_carry_c := sub31carryc; + pred := fun i => i - 1; + sub := sub31; + sub_carry := fun i j => i - j - 1; + mul_c := mul31c; + mul := mul31; + square_c := fun x => x *c x; + div21 := div3121; + div_gt := div31; (* this is supposed to be the special case of + division a/b where a > b *) + div := div31; + modulo_gt := fun i j => let (_,r) := i/j in r; + modulo := fun i j => let (_,r) := i/j in r; + gcd_gt := gcd31; + gcd := gcd31; + add_mul_div := addmuldiv31; + pos_mod := (* modulo 2^p *) + fun p i => + match p ?= 31 with | Lt => addmuldiv31 p 0 (addmuldiv31 (31-p) i 0) | _ => i - end. + end; + is_even := + fun i => let (_,r) := i/2 in + match r ?= 0 with Eq => true | _ => false end; + sqrt2 := sqrt312; + sqrt := sqrt31 +}. -(** Parity test *) -Let w_iseven i := - let (_,r) := i/2 in - match r ?= 0 with Eq => true | _ => false end. - -Definition int31_op := (mk_znz_op - 31%positive (* number of digits *) - 31 (* number of digits *) - phi (* conversion to Z *) - positive_to_int31 (* positive -> N*int31 : p => N,i where p = N*2^31+phi i *) - head031 (* number of head 0 *) - tail031 (* number of tail 0 *) - (* Basic constructors *) - 0 - 1 - Tn (* 2^31 - 1 *) - (* Comparison *) - compare31 - w_iszero - (* Basic arithmetic operations *) - (fun i => 0 -c i) - opp31 - (fun i => 0-i-1) - (fun i => i +c 1) - add31c - add31carryc - (fun i => i + 1) - add31 - (fun i j => i + j + 1) - (fun i => i -c 1) - sub31c - sub31carryc - (fun i => i - 1) - sub31 - (fun i j => i - j - 1) - mul31c - mul31 - (fun x => x *c x) - (* special (euclidian) division operations *) - div3121 - div31 (* this is supposed to be the special case of division a/b where a > b *) - div31 - (* euclidian division remainder *) - (* again special case for a > b *) - (fun i j => let (_,r) := i/j in r) - (fun i j => let (_,r) := i/j in r) - gcd31 (*gcd_gt*) - gcd31 (*gcd*) - (* shift operations *) - addmuldiv31 (*add_mul_div *) - (* modulo 2^p *) - w_pos_mod - (* is i even ? *) - w_iseven - (* square root operations *) - sqrt312 (* sqrt2 *) - sqrt31 (* sqrt *) -). - -End Int31_Op. - -Section Int31_Spec. +Section Int31_Specs. Local Open Scope Z_scope. @@ -1222,22 +1202,14 @@ Section Int31_Spec. reflexivity. Qed. - Lemma spec_Bm1 : [| Tn |] = wB - 1. + Lemma spec_m1 : [| Tn |] = wB - 1. Proof. reflexivity. Qed. Lemma spec_compare : forall x y, - match (x ?= y)%int31 with - | Eq => [|x|] = [|y|] - | Lt => [|x|] < [|y|] - | Gt => [|x|] > [|y|] - end. - Proof. - clear; unfold compare31; simpl; intros. - case_eq ([|x|] ?= [|y|]); auto. - intros; apply Zcompare_Eq_eq; auto. - Qed. + (x ?= y)%int31 = ([|x|] ?= [|y|]). + Proof. reflexivity. Qed. (** Addition *) @@ -1654,12 +1626,10 @@ Section Int31_Spec. rewrite Zmult_comm, Z_div_mult; auto with zarith. Qed. - Let w_pos_mod := int31_op.(znz_pos_mod). - Lemma spec_pos_mod : forall w p, - [|w_pos_mod p w|] = [|w|] mod (2 ^ [|p|]). + [|ZnZ.pos_mod p w|] = [|w|] mod (2 ^ [|p|]). Proof. - unfold w_pos_mod, znz_pos_mod, int31_op, compare31. + unfold ZnZ.pos_mod, int31_ops, compare31. change [|31|] with 31%Z. assert (forall w p, 31<=p -> [|w|] = [|w|] mod 2^p). intros. @@ -2018,8 +1988,8 @@ Section Int31_Spec. Proof. assert (Hp2: 0 < [|2|]) by exact (refl_equal Lt). intros rec i j Hi Hj Hij H31 Hrec; rewrite sqrt31_step_def. - generalize (spec_compare (fst (i/j)%int31) j); case compare31; - rewrite div31_phi; auto; intros Hc; + rewrite spec_compare, div31_phi; auto. + case Zcompare_spec; auto; intros Hc; try (split; auto; apply sqrt_test_true; auto with zarith; fail). apply Hrec; repeat rewrite div31_phi; auto with zarith. replace [|(j + fst (i / j)%int31)|] with ([|j|] + [|i|] / [|j|]). @@ -2072,7 +2042,7 @@ Section Int31_Spec. [|sqrt31 x|] ^ 2 <= [|x|] < ([|sqrt31 x|] + 1) ^ 2. Proof. intros i; unfold sqrt31. - generalize (spec_compare 1 i); case compare31; change [|1|] with 1; + rewrite spec_compare. case Zcompare_spec; change [|1|] with 1; intros Hi; auto with zarith. repeat rewrite Zpower_2; auto with zarith. apply iter31_sqrt_correct; auto with zarith. @@ -2157,7 +2127,7 @@ Section Int31_Spec. unfold phi2; apply Zlt_le_trans with ([|ih|] * base)%Z; auto with zarith. apply Zmult_lt_0_compat; auto with zarith. apply Zlt_le_trans with (2:= Hih); auto with zarith. - generalize (spec_compare ih j); case compare31; intros Hc1. + rewrite spec_compare. case Zcompare_spec; intros Hc1. split; auto. apply sqrt_test_true; auto. unfold phi2, base; auto with zarith. @@ -2166,7 +2136,7 @@ Section Int31_Spec. rewrite Zmult_comm, Z_div_plus_full_l; unfold base; auto with zarith. unfold Zpower, Zpower_pos in Hj1; simpl in Hj1; auto with zarith. case (Zle_or_lt (2 ^ 30) [|j|]); intros Hjj. - generalize (spec_compare (fst (div3121 ih il j)) j); case compare31; + rewrite spec_compare; case Zcompare_spec; rewrite div312_phi; auto; intros Hc; try (split; auto; apply sqrt_test_true; auto with zarith; fail). apply Hrec. @@ -2300,7 +2270,7 @@ Section Int31_Spec. generalize (spec_sub_c il il1). case sub31c; intros il2 Hil2. simpl interp_carry in Hil2. - generalize (spec_compare ih ih1); case compare31. + rewrite spec_compare; case Zcompare_spec. unfold interp_carry. intros H1; split. rewrite Zpower_2, <- Hihl1. @@ -2347,7 +2317,7 @@ Section Int31_Spec. case (phi_bounded ih); intros H1 H2. generalize Hih; change (2 ^ Z_of_nat size / 4) with 536870912. split; auto with zarith. - generalize (spec_compare (ih - 1) ih1); case compare31. + rewrite spec_compare; case Zcompare_spec. rewrite Hsih. intros H1; split. rewrite Zpower_2, <- Hihl1. @@ -2418,11 +2388,9 @@ Section Int31_Spec. (** [iszero] *) - Let w_eq0 := int31_op.(znz_eq0). - - Lemma spec_eq0 : forall x, w_eq0 x = true -> [|x|] = 0. + Lemma spec_eq0 : forall x, ZnZ.eq0 x = true -> [|x|] = 0. Proof. - clear; unfold w_eq0, znz_eq0; simpl. + clear; unfold ZnZ.eq0; simpl. unfold compare31; simpl; intros. change [|0|] with 0 in H. apply Zcompare_Eq_eq. @@ -2431,12 +2399,10 @@ Section Int31_Spec. (* Even *) - Let w_is_even := int31_op.(znz_is_even). - Lemma spec_is_even : forall x, - if w_is_even x then [|x|] mod 2 = 0 else [|x|] mod 2 = 1. + if ZnZ.is_even x then [|x|] mod 2 = 0 else [|x|] mod 2 = 1. Proof. - unfold w_is_even; simpl; intros. + unfold ZnZ.is_even; simpl; intros. generalize (spec_div x 2). destruct (x/2)%int31 as (q,r); intros. unfold compare31. @@ -2445,77 +2411,60 @@ Section Int31_Spec. destruct H; auto with zarith. replace ([|x|] mod 2) with [|r|]. destruct H; auto with zarith. - case_eq ([|r|] ?= 0)%Z; intros. - apply Zcompare_Eq_eq; auto. - change ([|r|] < 0)%Z in H; auto with zarith. - change ([|r|] > 0)%Z in H; auto with zarith. + case Zcompare_spec; auto with zarith. apply Zmod_unique with [|q|]; auto with zarith. Qed. - Definition int31_spec : znz_spec int31_op. - split. - exact phi_bounded. - exact positive_to_int31_spec. - exact spec_zdigits. - exact spec_more_than_1_digit. - - exact spec_0. - exact spec_1. - exact spec_Bm1. - - exact spec_compare. - exact spec_eq0. - - exact spec_opp_c. - exact spec_opp. - exact spec_opp_carry. - - exact spec_succ_c. - exact spec_add_c. - exact spec_add_carry_c. - exact spec_succ. - exact spec_add. - exact spec_add_carry. - - exact spec_pred_c. - exact spec_sub_c. - exact spec_sub_carry_c. - exact spec_pred. - exact spec_sub. - exact spec_sub_carry. - - exact spec_mul_c. - exact spec_mul. - exact spec_square_c. - - exact spec_div21. - intros; apply spec_div; auto. - exact spec_div. - - intros; unfold int31_op; simpl; apply spec_mod; auto. - exact spec_mod. - - intros; apply spec_gcd; auto. - exact spec_gcd. - - exact spec_head00. - exact spec_head0. - exact spec_tail00. - exact spec_tail0. - - exact spec_add_mul_div. - exact spec_pos_mod. - - exact spec_is_even. - exact spec_sqrt2. - exact spec_sqrt. - Qed. - -End Int31_Spec. + Global Instance int31_specs : ZnZ.Specs int31_ops := { + spec_to_Z := phi_bounded; + spec_of_pos := positive_to_int31_spec; + spec_zdigits := spec_zdigits; + spec_more_than_1_digit := spec_more_than_1_digit; + spec_0 := spec_0; + spec_1 := spec_1; + spec_m1 := spec_m1; + spec_compare := spec_compare; + spec_eq0 := spec_eq0; + spec_opp_c := spec_opp_c; + spec_opp := spec_opp; + spec_opp_carry := spec_opp_carry; + spec_succ_c := spec_succ_c; + spec_add_c := spec_add_c; + spec_add_carry_c := spec_add_carry_c; + spec_succ := spec_succ; + spec_add := spec_add; + spec_add_carry := spec_add_carry; + spec_pred_c := spec_pred_c; + spec_sub_c := spec_sub_c; + spec_sub_carry_c := spec_sub_carry_c; + spec_pred := spec_pred; + spec_sub := spec_sub; + spec_sub_carry := spec_sub_carry; + spec_mul_c := spec_mul_c; + spec_mul := spec_mul; + spec_square_c := spec_square_c; + spec_div21 := spec_div21; + spec_div_gt := fun a b _ => spec_div a b; + spec_div := spec_div; + spec_modulo_gt := fun a b _ => spec_mod a b; + spec_modulo := spec_mod; + spec_gcd_gt := fun a b _ => spec_gcd a b; + spec_gcd := spec_gcd; + spec_head00 := spec_head00; + spec_head0 := spec_head0; + spec_tail00 := spec_tail00; + spec_tail0 := spec_tail0; + spec_add_mul_div := spec_add_mul_div; + spec_pos_mod := spec_pos_mod; + spec_is_even := spec_is_even; + spec_sqrt2 := spec_sqrt2; + spec_sqrt := spec_sqrt }. + +End Int31_Specs. Module Int31Cyclic <: CyclicType. - Definition w := int31. - Definition w_op := int31_op. - Definition w_spec := int31_spec. + Definition t := int31. + Definition ops := int31_ops. + Definition specs := int31_specs. End Int31Cyclic. diff --git a/theories/Numbers/Cyclic/Int31/Ring31.v b/theories/Numbers/Cyclic/Int31/Ring31.v index 2ec406b0f..a9c499fb9 100644 --- a/theories/Numbers/Cyclic/Int31/Ring31.v +++ b/theories/Numbers/Cyclic/Int31/Ring31.v @@ -83,9 +83,10 @@ Qed. Lemma eqb31_eq : forall x y, eqb31 x y = true <-> x=y. Proof. unfold eqb31. intros x y. -generalize (Cyclic31.spec_compare x y). -destruct (x ?= y); intuition; subst; auto with zarith; try discriminate. -apply Int31_canonic; auto. +rewrite Cyclic31.spec_compare. case Zcompare_spec. +intuition. apply Int31_canonic; auto. +intuition; subst; auto with zarith; try discriminate. +intuition; subst; auto with zarith; try discriminate. Qed. Lemma eqb31_correct : forall x y, eqb31 x y = true -> x=y. diff --git a/theories/Numbers/Cyclic/ZModulo/ZModulo.v b/theories/Numbers/Cyclic/ZModulo/ZModulo.v index 4f0f6c7c4..da0be5e2a 100644 --- a/theories/Numbers/Cyclic/ZModulo/ZModulo.v +++ b/theories/Numbers/Cyclic/ZModulo/ZModulo.v @@ -33,25 +33,23 @@ Section ZModulo. Definition wB := base digits. - Definition znz := Z. - Definition znz_digits := digits. - Definition znz_zdigits := Zpos digits. - Definition znz_to_Z x := x mod wB. + Definition t := Z. + Definition zdigits := Zpos digits. + Definition to_Z x := x mod wB. - Notation "[| x |]" := (znz_to_Z x) (at level 0, x at level 99). + Notation "[| x |]" := (to_Z x) (at level 0, x at level 99). Notation "[+| c |]" := - (interp_carry 1 wB znz_to_Z c) (at level 0, x at level 99). + (interp_carry 1 wB to_Z c) (at level 0, x at level 99). Notation "[-| c |]" := - (interp_carry (-1) wB znz_to_Z c) (at level 0, x at level 99). + (interp_carry (-1) wB to_Z c) (at level 0, x at level 99). Notation "[|| x ||]" := - (zn2z_to_Z wB znz_to_Z x) (at level 0, x at level 99). + (zn2z_to_Z wB to_Z x) (at level 0, x at level 99). Lemma spec_more_than_1_digit: 1 < Zpos digits. Proof. - unfold znz_digits. generalize digits_ne_1; destruct digits; auto. destruct 1; auto. Qed. @@ -65,12 +63,12 @@ Section ZModulo. Lemma spec_to_Z_1 : forall x, 0 <= [|x|]. Proof. - unfold znz_to_Z; intros; destruct (Z_mod_lt x wB wB_pos); auto. + unfold to_Z; intros; destruct (Z_mod_lt x wB wB_pos); auto. Qed. Lemma spec_to_Z_2 : forall x, [|x|] < wB. Proof. - unfold znz_to_Z; intros; destruct (Z_mod_lt x wB wB_pos); auto. + unfold to_Z; intros; destruct (Z_mod_lt x wB wB_pos); auto. Qed. Hint Resolve spec_to_Z_1 spec_to_Z_2. @@ -79,16 +77,16 @@ Section ZModulo. auto. Qed. - Definition znz_of_pos x := + Definition of_pos x := let (q,r) := Zdiv_eucl_POS x wB in (N_of_Z q, r). Lemma spec_of_pos : forall p, - Zpos p = (Z_of_N (fst (znz_of_pos p)))*wB + [|(snd (znz_of_pos p))|]. + Zpos p = (Z_of_N (fst (of_pos p)))*wB + [|(snd (of_pos p))|]. Proof. - intros; unfold znz_of_pos; simpl. + intros; unfold of_pos; simpl. generalize (Z_div_mod_POS wB wB_pos p). destruct (Zdiv_eucl_POS p wB); simpl; destruct 1. - unfold znz_to_Z; rewrite Zmod_small; auto. + unfold to_Z; rewrite Zmod_small; auto. assert (0 <= z). replace z with (Zpos p / wB) by (symmetry; apply Zdiv_unique with z0; auto). @@ -98,37 +96,37 @@ Section ZModulo. rewrite Zmult_comm; auto. Qed. - Lemma spec_zdigits : [|znz_zdigits|] = Zpos znz_digits. + Lemma spec_zdigits : [|zdigits|] = Zpos digits. Proof. - unfold znz_to_Z, znz_zdigits, znz_digits. + unfold to_Z, zdigits. apply Zmod_small. unfold wB, base. split; auto with zarith. apply Zpower2_lt_lin; auto with zarith. Qed. - Definition znz_0 := 0. - Definition znz_1 := 1. - Definition znz_Bm1 := wB - 1. + Definition zero := 0. + Definition one := 1. + Definition minus_one := wB - 1. - Lemma spec_0 : [|znz_0|] = 0. + Lemma spec_0 : [|zero|] = 0. Proof. - unfold znz_to_Z, znz_0. + unfold to_Z, zero. apply Zmod_small; generalize wB_pos; auto with zarith. Qed. - Lemma spec_1 : [|znz_1|] = 1. + Lemma spec_1 : [|one|] = 1. Proof. - unfold znz_to_Z, znz_1. + unfold to_Z, one. apply Zmod_small; split; auto with zarith. unfold wB, base. apply Zlt_trans with (Zpos digits); auto. apply Zpower2_lt_lin; auto with zarith. Qed. - Lemma spec_Bm1 : [|znz_Bm1|] = wB - 1. + Lemma spec_Bm1 : [|minus_one|] = wB - 1. Proof. - unfold znz_to_Z, znz_Bm1. + unfold to_Z, minus_one. apply Zmod_small; split; auto with zarith. unfold wB, base. cut (1 <= 2 ^ Zpos digits); auto with zarith. @@ -136,54 +134,46 @@ Section ZModulo. apply Zpower2_le_lin; auto with zarith. Qed. - Definition znz_compare x y := Zcompare [|x|] [|y|]. + Definition compare x y := Zcompare [|x|] [|y|]. Lemma spec_compare : forall x y, - match znz_compare x y with - | Eq => [|x|] = [|y|] - | Lt => [|x|] < [|y|] - | Gt => [|x|] > [|y|] - end. - Proof. - intros; unfold znz_compare, Zlt, Zgt. - case_eq (Zcompare [|x|] [|y|]); auto. - intros; apply Zcompare_Eq_eq; auto. - Qed. + compare x y = Zcompare [|x|] [|y|]. + Proof. reflexivity. Qed. - Definition znz_eq0 x := + Definition eq0 x := match [|x|] with Z0 => true | _ => false end. - Lemma spec_eq0 : forall x, znz_eq0 x = true -> [|x|] = 0. + Lemma spec_eq0 : forall x, eq0 x = true -> [|x|] = 0. Proof. - unfold znz_eq0; intros; now destruct [|x|]. + unfold eq0; intros; now destruct [|x|]. Qed. - Definition znz_opp_c x := - if znz_eq0 x then C0 0 else C1 (- x). - Definition znz_opp x := - x. - Definition znz_opp_carry x := - x - 1. + Definition opp_c x := + if eq0 x then C0 0 else C1 (- x). + Definition opp x := - x. + Definition opp_carry x := - x - 1. - Lemma spec_opp_c : forall x, [-|znz_opp_c x|] = -[|x|]. + Lemma spec_opp_c : forall x, [-|opp_c x|] = -[|x|]. Proof. - intros; unfold znz_opp_c, znz_to_Z; auto. - case_eq (znz_eq0 x); intros; unfold interp_carry. + intros; unfold opp_c, to_Z; auto. + case_eq (eq0 x); intros; unfold interp_carry. fold [|x|]; rewrite (spec_eq0 x H); auto. assert (x mod wB <> 0). - unfold znz_eq0, znz_to_Z in H. + unfold eq0, to_Z in H. intro H0; rewrite H0 in H; discriminate. rewrite Z_mod_nz_opp_full; auto with zarith. Qed. - Lemma spec_opp : forall x, [|znz_opp x|] = (-[|x|]) mod wB. + Lemma spec_opp : forall x, [|opp x|] = (-[|x|]) mod wB. Proof. - intros; unfold znz_opp, znz_to_Z; auto. + intros; unfold opp, to_Z; auto. change ((- x) mod wB = (0 - (x mod wB)) mod wB). rewrite Zminus_mod_idemp_r; simpl; auto. Qed. - Lemma spec_opp_carry : forall x, [|znz_opp_carry x|] = wB - [|x|] - 1. + Lemma spec_opp_carry : forall x, [|opp_carry x|] = wB - [|x|] - 1. Proof. - intros; unfold znz_opp_carry, znz_to_Z; auto. + intros; unfold opp_carry, to_Z; auto. replace (- x - 1) with (- 1 - x) by omega. rewrite <- Zminus_mod_idemp_r. replace ( -1 - x mod wB) with (0 + ( -1 - x mod wB)) by omega. @@ -194,21 +184,21 @@ Section ZModulo. generalize (Z_mod_lt x wB wB_pos); omega. Qed. - Definition znz_succ_c x := + Definition succ_c x := let y := Zsucc x in - if znz_eq0 y then C1 0 else C0 y. + if eq0 y then C1 0 else C0 y. - Definition znz_add_c x y := + Definition add_c x y := let z := [|x|] + [|y|] in if Z_lt_le_dec z wB then C0 z else C1 (z-wB). - Definition znz_add_carry_c x y := + Definition add_carry_c x y := let z := [|x|]+[|y|]+1 in if Z_lt_le_dec z wB then C0 z else C1 (z-wB). - Definition znz_succ := Zsucc. - Definition znz_add := Zplus. - Definition znz_add_carry x y := x + y + 1. + Definition succ := Zsucc. + Definition add := Zplus. + Definition add_carry x y := x + y + 1. Lemma Zmod_equal : forall x y z, z>0 -> (x-y) mod z = 0 -> x mod z = y mod z. @@ -221,10 +211,10 @@ Section ZModulo. rewrite Zplus_comm, Zmult_comm, Z_mod_plus; auto. Qed. - Lemma spec_succ_c : forall x, [+|znz_succ_c x|] = [|x|] + 1. + Lemma spec_succ_c : forall x, [+|succ_c x|] = [|x|] + 1. Proof. - intros; unfold znz_succ_c, znz_to_Z, Zsucc. - case_eq (znz_eq0 (x+1)); intros; unfold interp_carry. + intros; unfold succ_c, to_Z, Zsucc. + case_eq (eq0 (x+1)); intros; unfold interp_carry. rewrite Zmult_1_l. replace (wB + 0 mod wB) with wB by auto with zarith. @@ -236,7 +226,7 @@ Section ZModulo. apply Zmod_equal; auto. assert ((x+1) mod wB <> 0). - unfold znz_eq0, znz_to_Z in *; now destruct ((x+1) mod wB). + unfold eq0, to_Z in *; now destruct ((x+1) mod wB). assert (x mod wB + 1 <> wB). contradict H0. rewrite Zeq_plus_swap in H0; simpl in H0. @@ -247,9 +237,9 @@ Section ZModulo. generalize (Z_mod_lt x wB wB_pos); omega. Qed. - Lemma spec_add_c : forall x y, [+|znz_add_c x y|] = [|x|] + [|y|]. + Lemma spec_add_c : forall x y, [+|add_c x y|] = [|x|] + [|y|]. Proof. - intros; unfold znz_add_c, znz_to_Z, interp_carry. + intros; unfold add_c, to_Z, interp_carry. destruct Z_lt_le_dec. apply Zmod_small; generalize (Z_mod_lt x wB wB_pos) (Z_mod_lt y wB wB_pos); omega. @@ -258,9 +248,9 @@ Section ZModulo. generalize (Z_mod_lt x wB wB_pos) (Z_mod_lt y wB wB_pos); omega. Qed. - Lemma spec_add_carry_c : forall x y, [+|znz_add_carry_c x y|] = [|x|] + [|y|] + 1. + Lemma spec_add_carry_c : forall x y, [+|add_carry_c x y|] = [|x|] + [|y|] + 1. Proof. - intros; unfold znz_add_carry_c, znz_to_Z, interp_carry. + intros; unfold add_carry_c, to_Z, interp_carry. destruct Z_lt_le_dec. apply Zmod_small; generalize (Z_mod_lt x wB wB_pos) (Z_mod_lt y wB wB_pos); omega. @@ -269,59 +259,59 @@ Section ZModulo. generalize (Z_mod_lt x wB wB_pos) (Z_mod_lt y wB wB_pos); omega. Qed. - Lemma spec_succ : forall x, [|znz_succ x|] = ([|x|] + 1) mod wB. + Lemma spec_succ : forall x, [|succ x|] = ([|x|] + 1) mod wB. Proof. - intros; unfold znz_succ, znz_to_Z, Zsucc. + intros; unfold succ, to_Z, Zsucc. symmetry; apply Zplus_mod_idemp_l. Qed. - Lemma spec_add : forall x y, [|znz_add x y|] = ([|x|] + [|y|]) mod wB. + Lemma spec_add : forall x y, [|add x y|] = ([|x|] + [|y|]) mod wB. Proof. - intros; unfold znz_add, znz_to_Z; apply Zplus_mod. + intros; unfold add, to_Z; apply Zplus_mod. Qed. Lemma spec_add_carry : - forall x y, [|znz_add_carry x y|] = ([|x|] + [|y|] + 1) mod wB. + forall x y, [|add_carry x y|] = ([|x|] + [|y|] + 1) mod wB. Proof. - intros; unfold znz_add_carry, znz_to_Z. + intros; unfold add_carry, to_Z. rewrite <- Zplus_mod_idemp_l. rewrite (Zplus_mod x y). rewrite Zplus_mod_idemp_l; auto. Qed. - Definition znz_pred_c x := - if znz_eq0 x then C1 (wB-1) else C0 (x-1). + Definition pred_c x := + if eq0 x then C1 (wB-1) else C0 (x-1). - Definition znz_sub_c x y := + Definition sub_c x y := let z := [|x|]-[|y|] in if Z_lt_le_dec z 0 then C1 (wB+z) else C0 z. - Definition znz_sub_carry_c x y := + Definition sub_carry_c x y := let z := [|x|]-[|y|]-1 in if Z_lt_le_dec z 0 then C1 (wB+z) else C0 z. - Definition znz_pred := Zpred. - Definition znz_sub := Zminus. - Definition znz_sub_carry x y := x - y - 1. + Definition pred := Zpred. + Definition sub := Zminus. + Definition sub_carry x y := x - y - 1. - Lemma spec_pred_c : forall x, [-|znz_pred_c x|] = [|x|] - 1. + Lemma spec_pred_c : forall x, [-|pred_c x|] = [|x|] - 1. Proof. - intros; unfold znz_pred_c, znz_to_Z, interp_carry. - case_eq (znz_eq0 x); intros. + intros; unfold pred_c, to_Z, interp_carry. + case_eq (eq0 x); intros. fold [|x|]; rewrite spec_eq0; auto. replace ((wB-1) mod wB) with (wB-1); auto with zarith. symmetry; apply Zmod_small; generalize wB_pos; omega. assert (x mod wB <> 0). - unfold znz_eq0, znz_to_Z in *; now destruct (x mod wB). + unfold eq0, to_Z in *; now destruct (x mod wB). rewrite <- Zminus_mod_idemp_l. apply Zmod_small. generalize (Z_mod_lt x wB wB_pos); omega. Qed. - Lemma spec_sub_c : forall x y, [-|znz_sub_c x y|] = [|x|] - [|y|]. + Lemma spec_sub_c : forall x y, [-|sub_c x y|] = [|x|] - [|y|]. Proof. - intros; unfold znz_sub_c, znz_to_Z, interp_carry. + intros; unfold sub_c, to_Z, interp_carry. destruct Z_lt_le_dec. replace ((wB + (x mod wB - y mod wB)) mod wB) with (wB + (x mod wB - y mod wB)). @@ -333,9 +323,9 @@ Section ZModulo. generalize wB_pos (Z_mod_lt x wB wB_pos) (Z_mod_lt y wB wB_pos); omega. Qed. - Lemma spec_sub_carry_c : forall x y, [-|znz_sub_carry_c x y|] = [|x|] - [|y|] - 1. + Lemma spec_sub_carry_c : forall x y, [-|sub_carry_c x y|] = [|x|] - [|y|] - 1. Proof. - intros; unfold znz_sub_carry_c, znz_to_Z, interp_carry. + intros; unfold sub_carry_c, to_Z, interp_carry. destruct Z_lt_le_dec. replace ((wB + (x mod wB - y mod wB - 1)) mod wB) with (wB + (x mod wB - y mod wB -1)). @@ -347,38 +337,38 @@ Section ZModulo. generalize wB_pos (Z_mod_lt x wB wB_pos) (Z_mod_lt y wB wB_pos); omega. Qed. - Lemma spec_pred : forall x, [|znz_pred x|] = ([|x|] - 1) mod wB. + Lemma spec_pred : forall x, [|pred x|] = ([|x|] - 1) mod wB. Proof. - intros; unfold znz_pred, znz_to_Z, Zpred. + intros; unfold pred, to_Z, Zpred. rewrite <- Zplus_mod_idemp_l; auto. Qed. - Lemma spec_sub : forall x y, [|znz_sub x y|] = ([|x|] - [|y|]) mod wB. + Lemma spec_sub : forall x y, [|sub x y|] = ([|x|] - [|y|]) mod wB. Proof. - intros; unfold znz_sub, znz_to_Z; apply Zminus_mod. + intros; unfold sub, to_Z; apply Zminus_mod. Qed. Lemma spec_sub_carry : - forall x y, [|znz_sub_carry x y|] = ([|x|] - [|y|] - 1) mod wB. + forall x y, [|sub_carry x y|] = ([|x|] - [|y|] - 1) mod wB. Proof. - intros; unfold znz_sub_carry, znz_to_Z. + intros; unfold sub_carry, to_Z. rewrite <- Zminus_mod_idemp_l. rewrite (Zminus_mod x y). rewrite Zminus_mod_idemp_l. auto. Qed. - Definition znz_mul_c x y := + Definition mul_c x y := let (h,l) := Zdiv_eucl ([|x|]*[|y|]) wB in - if znz_eq0 h then if znz_eq0 l then W0 else WW h l else WW h l. + if eq0 h then if eq0 l then W0 else WW h l else WW h l. - Definition znz_mul := Zmult. + Definition mul := Zmult. - Definition znz_square_c x := znz_mul_c x x. + Definition square_c x := mul_c x x. - Lemma spec_mul_c : forall x y, [|| znz_mul_c x y ||] = [|x|] * [|y|]. + Lemma spec_mul_c : forall x y, [|| mul_c x y ||] = [|x|] * [|y|]. Proof. - intros; unfold znz_mul_c, zn2z_to_Z. + intros; unfold 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). @@ -394,31 +384,31 @@ Section ZModulo. apply Zdiv_lt_upper_bound; auto with zarith. apply Zmult_lt_compat; auto with zarith. clear H H0 H1 H2. - case_eq (znz_eq0 h); simpl; intros. - case_eq (znz_eq0 l); simpl; intros. + case_eq (eq0 h); simpl; intros. + case_eq (eq0 l); simpl; intros. rewrite <- H3, <- H4, (spec_eq0 h), (spec_eq0 l); auto with zarith. rewrite H3, H4; auto with zarith. rewrite H3, H4; auto with zarith. Qed. - Lemma spec_mul : forall x y, [|znz_mul x y|] = ([|x|] * [|y|]) mod wB. + Lemma spec_mul : forall x y, [|mul x y|] = ([|x|] * [|y|]) mod wB. Proof. - intros; unfold znz_mul, znz_to_Z; apply Zmult_mod. + intros; unfold mul, to_Z; apply Zmult_mod. Qed. - Lemma spec_square_c : forall x, [|| znz_square_c x||] = [|x|] * [|x|]. + Lemma spec_square_c : forall x, [|| square_c x||] = [|x|] * [|x|]. Proof. intros x; exact (spec_mul_c x x). Qed. - Definition znz_div x y := Zdiv_eucl [|x|] [|y|]. + Definition div x y := Zdiv_eucl [|x|] [|y|]. Lemma spec_div : forall a b, 0 < [|b|] -> - let (q,r) := znz_div a b in + let (q,r) := div a b in [|a|] = [|q|] * [|b|] + [|r|] /\ 0 <= [|r|] < [|b|]. Proof. - intros; unfold znz_div. + intros; unfold div. assert ([|b|]>0) by auto with zarith. assert (Zdiv_eucl [|a|] [|b|] = ([|a|]/[|b|], [|a|] mod [|b|])). unfold Zmod, Zdiv; destruct Zdiv_eucl; auto. @@ -440,10 +430,10 @@ Section ZModulo. rewrite H5, H6; rewrite Zmult_comm; auto with zarith. Qed. - Definition znz_div_gt := znz_div. + Definition div_gt := div. Lemma spec_div_gt : forall a b, [|a|] > [|b|] -> 0 < [|b|] -> - let (q,r) := znz_div_gt a b in + let (q,r) := div_gt a b in [|a|] = [|q|] * [|b|] + [|r|] /\ 0 <= [|r|] < [|b|]. Proof. @@ -451,27 +441,27 @@ Section ZModulo. apply spec_div; auto. Qed. - Definition znz_mod x y := [|x|] mod [|y|]. - Definition znz_mod_gt x y := [|x|] mod [|y|]. + Definition modulo x y := [|x|] mod [|y|]. + Definition modulo_gt x y := [|x|] mod [|y|]. - Lemma spec_mod : forall a b, 0 < [|b|] -> - [|znz_mod a b|] = [|a|] mod [|b|]. + Lemma spec_modulo : forall a b, 0 < [|b|] -> + [|modulo a b|] = [|a|] mod [|b|]. Proof. - intros; unfold znz_mod. + intros; unfold modulo. apply Zmod_small. assert ([|b|]>0) by auto with zarith. generalize (Z_mod_lt [|a|] [|b|] H0) (Z_mod_lt b wB wB_pos). fold [|b|]; omega. Qed. - Lemma spec_mod_gt : forall a b, [|a|] > [|b|] -> 0 < [|b|] -> - [|znz_mod_gt a b|] = [|a|] mod [|b|]. + Lemma spec_modulo_gt : forall a b, [|a|] > [|b|] -> 0 < [|b|] -> + [|modulo_gt a b|] = [|a|] mod [|b|]. Proof. - intros; apply spec_mod; auto. + intros; apply spec_modulo; auto. Qed. - Definition znz_gcd x y := Zgcd [|x|] [|y|]. - Definition znz_gcd_gt x y := Zgcd [|x|] [|y|]. + Definition gcd x y := Zgcd [|x|] [|y|]. + Definition gcd_gt x y := Zgcd [|x|] [|y|]. Lemma Zgcd_bound : forall a b, 0<=a -> 0<=b -> Zgcd a b <= Zmax a b. Proof. @@ -495,9 +485,9 @@ Section ZModulo. generalize (Zmax_spec a b); omega. Qed. - Lemma spec_gcd : forall a b, Zis_gcd [|a|] [|b|] [|znz_gcd a b|]. + Lemma spec_gcd : forall a b, Zis_gcd [|a|] [|b|] [|gcd a b|]. Proof. - intros; unfold znz_gcd. + intros; unfold gcd. generalize (Z_mod_lt a wB wB_pos)(Z_mod_lt b wB wB_pos); intros. fold [|a|] in *; fold [|b|] in *. replace ([|Zgcd [|a|] [|b|]|]) with (Zgcd [|a|] [|b|]). @@ -511,22 +501,22 @@ Section ZModulo. Qed. Lemma spec_gcd_gt : forall a b, [|a|] > [|b|] -> - Zis_gcd [|a|] [|b|] [|znz_gcd_gt a b|]. + Zis_gcd [|a|] [|b|] [|gcd_gt a b|]. Proof. intros. apply spec_gcd; auto. Qed. - Definition znz_div21 a1 a2 b := + Definition div21 a1 a2 b := Zdiv_eucl ([|a1|]*wB+[|a2|]) [|b|]. Lemma spec_div21 : forall a1 a2 b, wB/2 <= [|b|] -> [|a1|] < [|b|] -> - let (q,r) := znz_div21 a1 a2 b in + let (q,r) := div21 a1 a2 b in [|a1|] *wB+ [|a2|] = [|q|] * [|b|] + [|r|] /\ 0 <= [|r|] < [|b|]. Proof. - intros; unfold znz_div21. + intros; unfold div21. generalize (Z_mod_lt a1 wB wB_pos); fold [|a1|]; intros. generalize (Z_mod_lt a2 wB wB_pos); fold [|a2|]; intros. assert ([|b|]>0) by auto with zarith. @@ -552,22 +542,22 @@ Section ZModulo. rewrite H8, H9; rewrite Zmult_comm; auto with zarith. Qed. - Definition znz_add_mul_div p x y := - ([|x|] * (2 ^ [|p|]) + [|y|] / (2 ^ ((Zpos znz_digits) - [|p|]))). + Definition add_mul_div p x y := + ([|x|] * (2 ^ [|p|]) + [|y|] / (2 ^ ((Zpos digits) - [|p|]))). Lemma spec_add_mul_div : forall x y p, - [|p|] <= Zpos znz_digits -> - [| znz_add_mul_div p x y |] = + [|p|] <= Zpos digits -> + [| add_mul_div p x y |] = ([|x|] * (2 ^ [|p|]) + - [|y|] / (2 ^ ((Zpos znz_digits) - [|p|]))) mod wB. + [|y|] / (2 ^ ((Zpos digits) - [|p|]))) mod wB. Proof. - intros; unfold znz_add_mul_div; auto. + intros; unfold add_mul_div; auto. Qed. - Definition znz_pos_mod p w := [|w|] mod (2 ^ [|p|]). + Definition pos_mod p w := [|w|] mod (2 ^ [|p|]). Lemma spec_pos_mod : forall w p, - [|znz_pos_mod p w|] = [|w|] mod (2 ^ [|p|]). + [|pos_mod p w|] = [|w|] mod (2 ^ [|p|]). Proof. - intros; unfold znz_pos_mod. + intros; unfold pos_mod. apply Zmod_small. generalize (Z_mod_lt [|w|] (2 ^ [|p|])); intros. split. @@ -576,22 +566,22 @@ Section ZModulo. apply Zmod_le; auto with zarith. Qed. - Definition znz_is_even x := + Definition is_even x := if Z_eq_dec ([|x|] mod 2) 0 then true else false. Lemma spec_is_even : forall x, - if znz_is_even x then [|x|] mod 2 = 0 else [|x|] mod 2 = 1. + if is_even x then [|x|] mod 2 = 0 else [|x|] mod 2 = 1. Proof. - intros; unfold znz_is_even; destruct Z_eq_dec; auto. + intros; unfold is_even; destruct Z_eq_dec; auto. generalize (Z_mod_lt [|x|] 2); omega. Qed. - Definition znz_sqrt x := Zsqrt_plain [|x|]. + Definition sqrt x := Zsqrt_plain [|x|]. Lemma spec_sqrt : forall x, - [|znz_sqrt x|] ^ 2 <= [|x|] < ([|znz_sqrt x|] + 1) ^ 2. + [|sqrt x|] ^ 2 <= [|x|] < ([|sqrt x|] + 1) ^ 2. Proof. intros. - unfold znz_sqrt. + unfold sqrt. repeat rewrite Zpower_2. replace [|Zsqrt_plain [|x|]|] with (Zsqrt_plain [|x|]). apply Zsqrt_interval; auto with zarith. @@ -609,7 +599,7 @@ Section ZModulo. generalize wB_pos; auto with zarith. Qed. - Definition znz_sqrt2 x y := + Definition sqrt2 x y := let z := [|x|]*wB+[|y|] in match z with | Z0 => (0, C0 0) @@ -621,11 +611,11 @@ Section ZModulo. Lemma spec_sqrt2 : forall x y, wB/ 4 <= [|x|] -> - let (s,r) := znz_sqrt2 x y in + let (s,r) := sqrt2 x y in [||WW x y||] = [|s|] ^ 2 + [+|r|] /\ [+|r|] <= 2 * [|s|]. Proof. - intros; unfold znz_sqrt2. + intros; unfold sqrt2. simpl zn2z_to_Z. remember ([|x|]*wB+[|y|]) as z. destruct z. @@ -665,15 +655,15 @@ Section ZModulo. apply two_power_pos_correct. Qed. - Definition znz_head0 x := match [|x|] with - | Z0 => znz_zdigits - | Zpos p => znz_zdigits - log_inf p - 1 + Definition head0 x := match [|x|] with + | Z0 => zdigits + | Zpos p => zdigits - log_inf p - 1 | _ => 0 end. - Lemma spec_head00: forall x, [|x|] = 0 -> [|znz_head0 x|] = Zpos znz_digits. + Lemma spec_head00: forall x, [|x|] = 0 -> [|head0 x|] = Zpos digits. Proof. - unfold znz_head0; intros. + unfold head0; intros. rewrite H; simpl. apply spec_zdigits. Qed. @@ -701,43 +691,43 @@ Section ZModulo. Lemma spec_head0 : forall x, 0 < [|x|] -> - wB/ 2 <= 2 ^ ([|znz_head0 x|]) * [|x|] < wB. + wB/ 2 <= 2 ^ ([|head0 x|]) * [|x|] < wB. Proof. - intros; unfold znz_head0. + intros; unfold head0. generalize (spec_to_Z x). destruct [|x|]; try discriminate. intros. destruct (log_inf_correct p). rewrite 2 two_p_power2 in H2; auto with zarith. - assert (0 <= znz_zdigits - log_inf p - 1 < wB). + assert (0 <= zdigits - log_inf p - 1 < wB). split. - cut (log_inf p < znz_zdigits); try omega. - unfold znz_zdigits. + cut (log_inf p < zdigits); try omega. + unfold zdigits. unfold wB, base in *. apply log_inf_bounded; auto with zarith. - apply Zlt_trans with znz_zdigits. + apply Zlt_trans with zdigits. omega. - unfold znz_zdigits, wB, base; apply Zpower2_lt_lin; auto with zarith. + unfold zdigits, wB, base; apply Zpower2_lt_lin; auto with zarith. - unfold znz_to_Z; rewrite (Zmod_small _ _ H3). + unfold to_Z; rewrite (Zmod_small _ _ H3). destruct H2. split. - apply Zle_trans with (2^(znz_zdigits - log_inf p - 1)*(2^log_inf p)). + apply Zle_trans with (2^(zdigits - log_inf p - 1)*(2^log_inf p)). apply Zdiv_le_upper_bound; auto with zarith. rewrite <- Zpower_exp; auto with zarith. rewrite Zmult_comm; rewrite <- Zpower_Zsucc; auto with zarith. - replace (Zsucc (znz_zdigits - log_inf p -1 +log_inf p)) with znz_zdigits + replace (Zsucc (zdigits - log_inf p -1 +log_inf p)) with zdigits by ring. - unfold wB, base, znz_zdigits; auto with zarith. + unfold wB, base, zdigits; auto with zarith. apply Zmult_le_compat; auto with zarith. apply Zlt_le_trans - with (2^(znz_zdigits - log_inf p - 1)*(2^(Zsucc (log_inf p)))). + with (2^(zdigits - log_inf p - 1)*(2^(Zsucc (log_inf p)))). apply Zmult_lt_compat_l; auto with zarith. rewrite <- Zpower_exp; auto with zarith. - replace (znz_zdigits - log_inf p -1 +Zsucc (log_inf p)) with znz_zdigits + replace (zdigits - log_inf p -1 +Zsucc (log_inf p)) with zdigits by ring. - unfold wB, base, znz_zdigits; auto with zarith. + unfold wB, base, zdigits; auto with zarith. Qed. Fixpoint Ptail p := match p with @@ -774,24 +764,24 @@ Section ZModulo. rewrite <- H1; omega. Qed. - Definition znz_tail0 x := + Definition tail0 x := match [|x|] with - | Z0 => znz_zdigits + | Z0 => zdigits | Zpos p => Ptail p | Zneg _ => 0 end. - Lemma spec_tail00: forall x, [|x|] = 0 -> [|znz_tail0 x|] = Zpos znz_digits. + Lemma spec_tail00: forall x, [|x|] = 0 -> [|tail0 x|] = Zpos digits. Proof. - unfold znz_tail0; intros. + unfold tail0; intros. rewrite H; simpl. apply spec_zdigits. Qed. Lemma spec_tail0 : forall x, 0 < [|x|] -> - exists y, 0 <= y /\ [|x|] = (2 * y + 1) * (2 ^ [|znz_tail0 x|]). + exists y, 0 <= y /\ [|x|] = (2 * y + 1) * (2 ^ [|tail0 x|]). Proof. - intros; unfold znz_tail0. + intros; unfold tail0. generalize (spec_to_Z x). destruct [|x|]; try discriminate; intros. assert ([|Ptail p|] = Ptail p). @@ -818,60 +808,60 @@ Section ZModulo. (** Let's now group everything in two records *) - Definition zmod_op := mk_znz_op - (znz_digits : positive) - (znz_zdigits: znz) - (znz_to_Z : znz -> Z) - (znz_of_pos : positive -> N * znz) - (znz_head0 : znz -> znz) - (znz_tail0 : znz -> znz) - - (znz_0 : znz) - (znz_1 : znz) - (znz_Bm1 : znz) - - (znz_compare : znz -> znz -> comparison) - (znz_eq0 : znz -> bool) - - (znz_opp_c : znz -> carry znz) - (znz_opp : znz -> znz) - (znz_opp_carry : znz -> znz) - - (znz_succ_c : znz -> carry znz) - (znz_add_c : znz -> znz -> carry znz) - (znz_add_carry_c : znz -> znz -> carry znz) - (znz_succ : znz -> znz) - (znz_add : znz -> znz -> znz) - (znz_add_carry : znz -> znz -> znz) - - (znz_pred_c : znz -> carry znz) - (znz_sub_c : znz -> znz -> carry znz) - (znz_sub_carry_c : znz -> znz -> carry znz) - (znz_pred : znz -> znz) - (znz_sub : znz -> znz -> znz) - (znz_sub_carry : znz -> znz -> znz) - - (znz_mul_c : znz -> znz -> zn2z znz) - (znz_mul : znz -> znz -> znz) - (znz_square_c : znz -> zn2z znz) - - (znz_div21 : znz -> znz -> znz -> znz*znz) - (znz_div_gt : znz -> znz -> znz * znz) - (znz_div : znz -> znz -> znz * znz) - - (znz_mod_gt : znz -> znz -> znz) - (znz_mod : znz -> znz -> znz) - - (znz_gcd_gt : znz -> znz -> znz) - (znz_gcd : znz -> znz -> znz) - (znz_add_mul_div : znz -> znz -> znz -> znz) - (znz_pos_mod : znz -> znz -> znz) - - (znz_is_even : znz -> bool) - (znz_sqrt2 : znz -> znz -> znz * carry znz) - (znz_sqrt : znz -> znz). - - Definition zmod_spec := mk_znz_spec zmod_op + Instance zmod_ops : ZnZ.Ops Z := ZnZ.MkOps + (digits : positive) + (zdigits: t) + (to_Z : t -> Z) + (of_pos : positive -> N * t) + (head0 : t -> t) + (tail0 : t -> t) + + (zero : t) + (one : t) + (minus_one : t) + + (compare : t -> t -> comparison) + (eq0 : t -> bool) + + (opp_c : t -> carry t) + (opp : t -> t) + (opp_carry : t -> t) + + (succ_c : t -> carry t) + (add_c : t -> t -> carry t) + (add_carry_c : t -> t -> carry t) + (succ : t -> t) + (add : t -> t -> t) + (add_carry : t -> t -> t) + + (pred_c : t -> carry t) + (sub_c : t -> t -> carry t) + (sub_carry_c : t -> t -> carry t) + (pred : t -> t) + (sub : t -> t -> t) + (sub_carry : t -> t -> t) + + (mul_c : t -> t -> zn2z t) + (mul : t -> t -> t) + (square_c : t -> zn2z t) + + (div21 : t -> t -> t -> t*t) + (div_gt : t -> t -> t * t) + (div : t -> t -> t * t) + + (modulo_gt : t -> t -> t) + (modulo : t -> t -> t) + + (gcd_gt : t -> t -> t) + (gcd : t -> t -> t) + (add_mul_div : t -> t -> t -> t) + (pos_mod : t -> t -> t) + + (is_even : t -> bool) + (sqrt2 : t -> t -> t * carry t) + (sqrt : t -> t). + + Instance zmod_specs : ZnZ.Specs zmod_ops := ZnZ.MkSpecs spec_to_Z spec_of_pos spec_zdigits @@ -910,8 +900,8 @@ Section ZModulo. spec_div_gt spec_div - spec_mod_gt - spec_mod + spec_modulo_gt + spec_modulo spec_gcd_gt spec_gcd @@ -934,12 +924,12 @@ End ZModulo. Module Type PositiveNotOne. Parameter p : positive. - Axiom not_one : p<> 1%positive. + Axiom not_one : p <> 1%positive. End PositiveNotOne. Module ZModuloCyclicType (P:PositiveNotOne) <: CyclicType. - Definition w := Z. - Definition w_op := zmod_op P.p. - Definition w_spec := zmod_spec P.not_one. + Definition t := Z. + Instance ops : ZnZ.Ops t := zmod_ops P.p. + Instance specs : ZnZ.Specs ops := zmod_specs P.not_one. End ZModuloCyclicType. |