From 6c4cb0b91468ac0f7bc95d79f89b88417628127a Mon Sep 17 00:00:00 2001 From: letouzey Date: Fri, 16 May 2008 12:21:36 +0000 Subject: Filename ZnZ (or Z_nZ in a later attempt) is neither pretty nor accurate (n _must_ in fact be a power of 2). Worse: Z_31Z is just plain wrong since it is Z/(2^31)Z and not Z/31Z (my fault). As a consequence, switch to CyclicAxioms, Cyclic31, DoubleCyclic, etc git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10940 85f007b7-540e-0410-9357-904b9bb8a0f7 --- Makefile.common | 6 +- theories/Numbers/Cyclic/Abstract/CyclicAxioms.v | 331 ++++++++ theories/Numbers/Cyclic/Abstract/NZCyclic.v | 11 +- theories/Numbers/Cyclic/Abstract/Z_nZ.v | 328 -------- .../Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v | 922 +++++++++++++++++++++ theories/Numbers/Cyclic/DoubleCyclic/Z_2nZ.v | 922 --------------------- theories/Numbers/Cyclic/Int31/Cyclic31.v | 114 +++ theories/Numbers/Cyclic/Int31/Z_31Z.v | 114 --- theories/Numbers/Natural/BigN/BigN.v | 6 +- theories/Numbers/Natural/BigN/NMake_gen.ml | 18 +- theories/Numbers/Natural/BigN/Nbasic.v | 4 +- 11 files changed, 1392 insertions(+), 1384 deletions(-) create mode 100644 theories/Numbers/Cyclic/Abstract/CyclicAxioms.v delete mode 100644 theories/Numbers/Cyclic/Abstract/Z_nZ.v create mode 100644 theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v delete mode 100644 theories/Numbers/Cyclic/DoubleCyclic/Z_2nZ.v create mode 100644 theories/Numbers/Cyclic/Int31/Cyclic31.v delete mode 100644 theories/Numbers/Cyclic/Int31/Z_31Z.v diff --git a/Makefile.common b/Makefile.common index 48e6dff14..a6596d59b 100644 --- a/Makefile.common +++ b/Makefile.common @@ -617,15 +617,15 @@ NUMBERSCOMMONVO:=$(addprefix theories/Numbers/, \ QRewrite.vo NumPrelude.vo BigNumPrelude.vo ) CYCLICABSTRACTVO:=$(addprefix theories/Numbers/Cyclic/Abstract/, \ - Z_nZ.vo NZCyclic.vo ) + CyclicAxioms.vo NZCyclic.vo ) CYCLICINT31VO:=$(addprefix theories/Numbers/Cyclic/Int31/, \ - Int31.vo Z_31Z.vo ) + Int31.vo Cyclic31.vo ) CYCLICDOUBLECYCLICVO:=$(addprefix theories/Numbers/Cyclic/DoubleCyclic/, \ DoubleType.vo DoubleBase.vo DoubleAdd.vo DoubleSub.vo \ DoubleMul.vo DoubleDivn1.vo DoubleDiv.vo DoubleSqrt.vo \ - DoubleLift.vo Z_2nZ.vo ) + DoubleLift.vo DoubleCyclic.vo ) CYCLICVO:=$(CYCLICABSTRACTVO) $(CYCLICINT31VO) $(CYCLICDOUBLECYCLICVO) diff --git a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v new file mode 100644 index 000000000..ed14cc799 --- /dev/null +++ b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v @@ -0,0 +1,331 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* Z; + znz_of_pos : positive -> N * znz; + znz_head0 : znz -> znz; + znz_tail0 : znz -> znz; + + (* Basic constructors *) + znz_0 : znz; + znz_1 : znz; + znz_Bm1 : znz; (* [2^digits-1], which is equivalent to [-1] *) + znz_WW : znz -> znz -> zn2z znz; + znz_W0 : znz -> zn2z znz; + znz_0W : znz -> zn2z znz; + + (* Comparison *) + znz_compare : znz -> znz -> comparison; + znz_eq0 : znz -> 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; + + (* Special divisions operations *) + 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; + + (* square root *) + znz_is_even : znz -> bool; + znz_sqrt2 : znz -> znz -> znz * carry znz; + znz_sqrt : znz -> znz }. + +End Z_nZ_Op. + +Section Z_nZ_Spec. + Variable w : Set. + 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 wWW := w_op.(znz_WW). + Let w0W := w_op.(znz_0W). + Let wW0 := w_op.(znz_W0). + + Let w_compare := w_op.(znz_compare). + Let w_eq0 := w_op.(znz_eq0). + + 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). + + 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_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_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. + + Notation "[+| c |]" := + (interp_carry 1 wB w_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). + + Notation "[|| x ||]" := + (zn2z_to_Z wB w_to_Z x) (at level 0, x at level 99). + + Record znz_spec : Set := mk_znz_spec { + + (* 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; + + (* Basic constructors *) + spec_0 : [|w0|] = 0; + spec_1 : [|w1|] = 1; + spec_Bm1 : [|wBm1|] = wB - 1; + spec_WW : forall h l, [||wWW h l||] = [|h|] * wB + [|l|]; + spec_0W : forall l, [||w0W l||] = [|l|]; + spec_W0 : forall h, [||wW0 h||] = [|h|]*wB; + + (* Comparison *) + spec_compare : + 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; + (* 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_add_carry : + forall x y, [|w_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_sub_carry : + forall x y, [|w_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|]; + + (* Special divisions operations *) + spec_div21 : forall a1 a2 b, + wB/2 <= [|b|] -> + [|a1|] < [|b|] -> + let (q,r) := w_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 + [|a|] = [|q|] * [|b|] + [|r|] /\ + 0 <= [|r|] < [|b|]; + spec_div : forall a b, 0 < [|b|] -> + let (q,r) := w_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_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|]; + + + (* shift operations *) + spec_head00: forall x, [|x|] = 0 -> [|w_head0 x|] = Zpos w_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; + spec_tail0 : forall x, 0 < [|x|] -> + exists y, 0 <= y /\ [|x|] = (2 * y + 1) * (2 ^ [|w_tail0 x|]) ; + spec_add_mul_div : forall x y p, + [|p|] <= Zpos w_digits -> + [| w_add_mul_div p x y |] = + ([|x|] * (2 ^ [|p|]) + + [|y|] / (2 ^ ((Zpos w_digits) - [|p|]))) mod wB; + spec_pos_mod : forall w p, + [|w_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; + spec_sqrt2 : forall x y, + wB/ 4 <= [|x|] -> + let (s,r) := w_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 + }. + +End Z_nZ_Spec. + + + +(** Injecting [Z] numbers into a cyclic structure *) + +Section znz_of_pos. + + Variable w : Set. + Variable w_op : znz_op w. + Variable op_spec : znz_spec w_op. + + Notation "[| x |]" := (znz_to_Z w_op x) (at level 0, x at level 99). + + Definition znz_of_Z (w:Set) (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. + intros p Hp. + generalize (spec_of_pos op_spec p). + case (znz_of_pos w_op 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. + case p1; simpl; intros; red; simpl; intros; discriminate. + unfold base; auto with zarith. + case (spec_to_Z op_spec 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. + intros p; case p; simpl; try rewrite spec_0; auto. + intros; rewrite znz_of_pos_correct; auto with zarith. + intros p1 (H1, _); contradict H1; apply Zlt_not_le; red; simpl; auto. + Qed. +End znz_of_pos. + + +(** A modular specification grouping the earlier records. *) + +Module Type CyclicType. + Parameter w : Set. + Parameter w_op : znz_op w. + Parameter w_spec : znz_spec w_op. +End CyclicType. diff --git a/theories/Numbers/Cyclic/Abstract/NZCyclic.v b/theories/Numbers/Cyclic/Abstract/NZCyclic.v index df3af4b63..2d23a12dd 100644 --- a/theories/Numbers/Cyclic/Abstract/NZCyclic.v +++ b/theories/Numbers/Cyclic/Abstract/NZCyclic.v @@ -13,10 +13,15 @@ Require Export NZAxioms. Require Import BigNumPrelude. Require Import DoubleType. -Require Import Z_nZ. +Require Import CyclicAxioms. -(** * A Z/nZ representation (module type [CyclicType]) implements - [NZAxiomsSig], e.g. the common properties between N and Z. *) +(** * From [CyclicType] to [NZAxiomsSig] *) + +(** A [Z/nZ] representation given by a module type [CyclicType] + implements [NZAxiomsSig], e.g. the common properties between + N and Z with no ordering. Notice that the [n] in [Z/nZ] is + a power of 2. +*) Module NZCyclicAxiomsMod (Import Cyclic : CyclicType) <: NZAxiomsSig. diff --git a/theories/Numbers/Cyclic/Abstract/Z_nZ.v b/theories/Numbers/Cyclic/Abstract/Z_nZ.v deleted file mode 100644 index 6d19e6613..000000000 --- a/theories/Numbers/Cyclic/Abstract/Z_nZ.v +++ /dev/null @@ -1,328 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* Z; - znz_of_pos : positive -> N * znz; - znz_head0 : znz -> znz; - znz_tail0 : znz -> znz; - - (* Basic constructors *) - znz_0 : znz; - znz_1 : znz; - znz_Bm1 : znz; - znz_WW : znz -> znz -> zn2z znz; - znz_W0 : znz -> zn2z znz; - znz_0W : znz -> zn2z znz; - - (* Comparison *) - znz_compare : znz -> znz -> comparison; - znz_eq0 : znz -> 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; - - (* Special divisions operations *) - 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; - - (* square root *) - znz_is_even : znz -> bool; - znz_sqrt2 : znz -> znz -> znz * carry znz; - znz_sqrt : znz -> znz }. - -End Z_nZ_Op. - -Section Z_nZ_Spec. - Variable w : Set. - 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 wWW := w_op.(znz_WW). - Let w0W := w_op.(znz_0W). - Let wW0 := w_op.(znz_W0). - - Let w_compare := w_op.(znz_compare). - Let w_eq0 := w_op.(znz_eq0). - - 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). - - 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_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_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. - - Notation "[+| c |]" := - (interp_carry 1 wB w_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). - - Notation "[|| x ||]" := - (zn2z_to_Z wB w_to_Z x) (at level 0, x at level 99). - - Record znz_spec : Set := mk_znz_spec { - - (* 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; - - (* Basic constructors *) - spec_0 : [|w0|] = 0; - spec_1 : [|w1|] = 1; - spec_Bm1 : [|wBm1|] = wB - 1; - spec_WW : forall h l, [||wWW h l||] = [|h|] * wB + [|l|]; - spec_0W : forall l, [||w0W l||] = [|l|]; - spec_W0 : forall h, [||wW0 h||] = [|h|]*wB; - - (* Comparison *) - spec_compare : - 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; - (* 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_add_carry : - forall x y, [|w_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_sub_carry : - forall x y, [|w_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|]; - - (* Special divisions operations *) - spec_div21 : forall a1 a2 b, - wB/2 <= [|b|] -> - [|a1|] < [|b|] -> - let (q,r) := w_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 - [|a|] = [|q|] * [|b|] + [|r|] /\ - 0 <= [|r|] < [|b|]; - spec_div : forall a b, 0 < [|b|] -> - let (q,r) := w_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_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|]; - - - (* shift operations *) - spec_head00: forall x, [|x|] = 0 -> [|w_head0 x|] = Zpos w_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; - spec_tail0 : forall x, 0 < [|x|] -> - exists y, 0 <= y /\ [|x|] = (2 * y + 1) * (2 ^ [|w_tail0 x|]) ; - spec_add_mul_div : forall x y p, - [|p|] <= Zpos w_digits -> - [| w_add_mul_div p x y |] = - ([|x|] * (2 ^ [|p|]) + - [|y|] / (2 ^ ((Zpos w_digits) - [|p|]))) mod wB; - spec_pos_mod : forall w p, - [|w_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; - spec_sqrt2 : forall x y, - wB/ 4 <= [|x|] -> - let (s,r) := w_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 - }. - -End Z_nZ_Spec. - - - -(** Injecting [Z] numbers into a cyclic structure *) - -Section znz_of_pos. - - Variable w : Set. - Variable w_op : znz_op w. - Variable op_spec : znz_spec w_op. - - Notation "[| x |]" := (znz_to_Z w_op x) (at level 0, x at level 99). - - Definition znz_of_Z (w:Set) (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. - intros p Hp. - generalize (spec_of_pos op_spec p). - case (znz_of_pos w_op 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. - case p1; simpl; intros; red; simpl; intros; discriminate. - unfold base; auto with zarith. - case (spec_to_Z op_spec 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. - intros p; case p; simpl; try rewrite spec_0; auto. - intros; rewrite znz_of_pos_correct; auto with zarith. - intros p1 (H1, _); contradict H1; apply Zlt_not_le; red; simpl; auto. - Qed. -End znz_of_pos. - - -(** A modular specification grouping the earlier records. *) - -Module Type CyclicType. - Parameter w : Set. - Parameter w_op : znz_op w. - Parameter w_spec : znz_spec w_op. -End CyclicType. diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v new file mode 100644 index 000000000..54ff3d354 --- /dev/null +++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v @@ -0,0 +1,922 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* WW w_0 p | C1 p => WW w_1 p end. + + Let _ww_digits := xO w_digits. + + Let _ww_zdigits := w_add2 w_zdigits w_zdigits. + + Let to_Z := zn2z_to_Z wB w_to_Z. + + Let ww_of_pos p := + match w_of_pos p with + | (N0, l) => (N0, WW w_0 l) + | (Npos ph,l) => + let (n,h) := w_of_pos ph in (n, w_WW h l) + end. + + + Let head0 := + Eval lazy beta delta [ww_head0] in + ww_head0 w_0 w_0W w_compare w_head0 w_add2 w_zdigits _ww_zdigits. + + Let tail0 := + 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). + + (* ** Comparison ** *) + Let compare := + Eval lazy beta delta[ww_compare] in ww_compare w_0 w_compare. + + Let eq0 (x:zn2z w) := + match x with + | W0 => true + | _ => false + end. + + (* ** Opposites ** *) + Let opp_c := + Eval lazy beta delta [ww_opp_c] in ww_opp_c w_0 w_opp_c w_opp_carry. + + Let opp := + Eval lazy beta delta [ww_opp] in ww_opp w_0 w_opp_c w_opp_carry w_opp. + + Let opp_carry := + Eval lazy beta delta [ww_opp_carry] in ww_opp_carry w_WW ww_Bm1 w_opp_carry. + + (* ** Additions ** *) + + Let succ_c := + Eval lazy beta delta [ww_succ_c] in ww_succ_c w_0 ww_1 w_succ_c. + + Let add_c := + Eval lazy beta delta [ww_add_c] in ww_add_c w_WW w_add_c w_add_carry_c. + + Let add_carry_c := + Eval lazy beta iota delta [ww_add_carry_c ww_succ_c] in + ww_add_carry_c w_0 w_WW ww_1 w_succ_c w_add_c w_add_carry_c. + + Let succ := + Eval lazy beta delta [ww_succ] in ww_succ w_W0 ww_1 w_succ_c w_succ. + + Let add := + Eval lazy beta delta [ww_add] in ww_add w_add_c w_add w_add_carry. + + Let add_carry := + Eval lazy beta iota delta [ww_add_carry ww_succ] in + ww_add_carry w_W0 ww_1 w_succ_c w_add_carry_c w_succ w_add w_add_carry. + + (* ** Subtractions ** *) + + Let pred_c := + Eval lazy beta delta [ww_pred_c] in ww_pred_c w_Bm1 w_WW ww_Bm1 w_pred_c. + + Let sub_c := + Eval lazy beta iota delta [ww_sub_c ww_opp_c] in + ww_sub_c w_0 w_WW w_opp_c w_opp_carry w_sub_c w_sub_carry_c. + + Let sub_carry_c := + Eval lazy beta iota delta [ww_sub_carry_c ww_pred_c ww_opp_carry] in + ww_sub_carry_c w_Bm1 w_WW ww_Bm1 w_opp_carry w_pred_c w_sub_c w_sub_carry_c. + + Let pred := + Eval lazy beta delta [ww_pred] in ww_pred w_Bm1 w_WW ww_Bm1 w_pred_c w_pred. + + Let sub := + Eval lazy beta iota delta [ww_sub ww_opp] in + ww_sub w_0 w_WW w_opp_c w_opp_carry w_sub_c w_opp w_sub w_sub_carry. + + Let sub_carry := + Eval lazy beta iota delta [ww_sub_carry ww_pred ww_opp_carry] in + ww_sub_carry w_Bm1 w_WW ww_Bm1 w_opp_carry w_pred_c w_sub_carry_c w_pred + w_sub w_sub_carry. + + + (* ** Multiplication ** *) + + Let mul_c := + Eval lazy beta iota delta [ww_mul_c double_mul_c] in + ww_mul_c w_0 w_1 w_WW w_W0 w_mul_c add_c add add_carry. + + Let karatsuba_c := + Eval lazy beta iota delta [ww_karatsuba_c double_mul_c kara_prod] in + ww_karatsuba_c w_0 w_1 w_WW w_W0 w_compare w_add w_sub w_mul_c + add_c add add_carry sub_c sub. + + Let mul := + Eval lazy beta delta [ww_mul] in + ww_mul w_W0 w_add w_mul_c w_mul add. + + Let square_c := + Eval lazy beta delta [ww_square_c] in + ww_square_c w_0 w_1 w_WW w_W0 w_mul_c w_square_c add_c add add_carry. + + (* Division operation *) + + Let div32 := + Eval lazy beta iota delta [w_div32] in + w_div32 w_0 w_Bm1 w_Bm2 w_WW w_compare w_add_c w_add_carry_c + w_add w_add_carry w_pred w_sub w_mul_c w_div21 sub_c. + + Let div21 := + 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 add_mul_div := + Eval lazy beta delta [ww_add_mul_div] in + ww_add_mul_div w_0 w_WW w_W0 w_0W compare w_add_mul_div sub w_zdigits low. + + Let div_gt := + Eval lazy beta delta [ww_div_gt] in + ww_div_gt 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. + + Let div := + Eval lazy beta delta [ww_div] in ww_div ww_1 compare div_gt. + + Let mod_gt := + Eval lazy beta delta [ww_mod_gt] in + ww_mod_gt 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_mod_gt w_add_mul_div w_head0 w_div21 div32 _ww_zdigits add_mul_div w_zdigits. + + Let mod_ := + Eval lazy beta delta [ww_mod] in ww_mod compare mod_gt. + + Let pos_mod := + Eval lazy beta delta [ww_pos_mod] in + ww_pos_mod w_0 w_zdigits w_WW w_pos_mod compare w_0W low sub _ww_zdigits. + + Let is_even := + Eval lazy beta delta [ww_is_even] in ww_is_even w_is_even. + + Let sqrt2 := + Eval lazy beta delta [ww_sqrt2] in + ww_sqrt2 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_zdigits w_add_c w_sqrt2 w_pred pred_c + pred add_c add sub_c add_mul_div. + + Let sqrt := + Eval lazy beta delta [ww_sqrt] in + ww_sqrt w_is_even w_0 w_sub w_add_mul_div w_zdigits + _ww_zdigits w_sqrt2 pred add_mul_div head0 compare low. + + Let gcd_gt_fix := + Eval cbv beta delta [ww_gcd_gt_aux ww_gcd_gt_body] in + ww_gcd_gt_aux 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 add_mul_div + w_zdigits. + + Let gcd_cont := + Eval lazy beta delta [gcd_cont] in gcd_cont ww_1 w_1 w_compare. + + Let gcd_gt := + Eval lazy beta delta [ww_gcd_gt] in + ww_gcd_gt w_0 w_eq0 w_gcd_gt _ww_digits gcd_gt_fix gcd_cont. + + Let gcd := + Eval lazy beta delta [ww_gcd] in + ww_gcd compare w_0 w_eq0 w_gcd_gt _ww_digits gcd_gt_fix gcd_cont. + + (* ** Record of operators on 2 words *) + + Definition mk_zn2z_op := + mk_znz_op _ww_digits _ww_zdigits + to_Z ww_of_pos head0 tail0 + W0 ww_1 ww_Bm1 + ww_WW ww_W0 ww_0W + compare eq0 + opp_c opp opp_carry + succ_c add_c add_carry_c + succ add add_carry + pred_c sub_c sub_carry_c + pred sub sub_carry + mul_c mul square_c + div21 div_gt div + mod_gt mod_ + gcd_gt gcd + add_mul_div + pos_mod + is_even + sqrt2 + sqrt. + + Definition mk_zn2z_op_karatsuba := + mk_znz_op _ww_digits _ww_zdigits + to_Z ww_of_pos head0 tail0 + W0 ww_1 ww_Bm1 + ww_WW ww_W0 ww_0W + compare eq0 + opp_c opp opp_carry + succ_c add_c add_carry_c + succ add add_carry + pred_c sub_c sub_carry_c + pred sub sub_carry + karatsuba_c mul square_c + div21 div_gt div + mod_gt mod_ + gcd_gt gcd + add_mul_div + pos_mod + is_even + sqrt2 + sqrt. + + (* Proof *) + Variable op_spec : znz_spec w_op. + + 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_WW op_spec) + (spec_0W op_spec) + (spec_W0 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). + + Let wwB := base _ww_digits. + + Notation "[| x |]" := (to_Z x) (at level 0, x at level 99). + + Notation "[+| c |]" := + (interp_carry 1 wwB to_Z c) (at level 0, x at level 99). + + Notation "[-| c |]" := + (interp_carry (-1) wwB to_Z c) (at level 0, x at level 99). + + Notation "[[ x ]]" := (zn2z_to_Z wwB to_Z x) (at level 0, x at level 99). + + Let spec_ww_to_Z : forall x, 0 <= [| x |] < wwB. + Proof. refine (spec_ww_to_Z w_digits w_to_Z _);auto. Qed. + + Let spec_ww_of_pos : forall p, + 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, w_WW, to_Z. + rewrite (spec_WW op_spec). replace wwB with (wB*wB). + unfold wB,w_digits;clear H;destruct n;ring. + symmetry. rewrite <- Zpower_2; exact (wwB_wBwB w_digits). + Qed. + + Let spec_ww_0 : [|W0|] = 0. + Proof. reflexivity. Qed. + + Let spec_ww_1 : [|ww_1|] = 1. + Proof. refine (spec_ww_1 w_0 w_1 w_digits w_to_Z _ _);auto. Qed. + + Let spec_ww_Bm1 : [|ww_Bm1|] = wwB - 1. + Proof. refine (spec_ww_Bm1 w_Bm1 w_digits w_to_Z _);auto. Qed. + + Let spec_ww_WW : forall h l, [[ww_WW h l]] = [|h|] * wwB + [|l|]. + Proof. + intros h l. replace wwB with (wB*wB). destruct h;simpl. + destruct l;simpl;ring. ring. + symmetry. rewrite <- Zpower_2; exact (wwB_wBwB w_digits). + Qed. + + Let spec_ww_0W : forall l, [[ww_0W l]] = [|l|]. + Proof. + intros l. replace wwB with (wB*wB). + destruct l;simpl;ring. + symmetry. ring_simplify; exact (wwB_wBwB w_digits). + Qed. + + Let spec_ww_W0 : forall h, [[ww_W0 h]] = [|h|]*wwB. + Proof. + intros h. replace wwB with (wB*wB). + destruct h;simpl;ring. + symmetry. ring_simplify; exact (wwB_wBwB w_digits). + Qed. + + Let spec_ww_compare : + forall x y, + match compare x y with + | Eq => [|x|] = [|y|] + | Lt => [|x|] < [|y|] + | Gt => [|x|] > [|y|] + end. + 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. + Proof. destruct x;simpl;intros;trivial;discriminate. Qed. + + Let spec_ww_opp_c : forall x, [-|opp_c x|] = -[|x|]. + Proof. + refine(spec_ww_opp_c w_0 w_0 W0 w_opp_c w_opp_carry w_digits w_to_Z _ _ _ _); + auto. + Qed. + + Let spec_ww_opp : forall x, [|opp x|] = (-[|x|]) mod wwB. + Proof. + refine(spec_ww_opp w_0 w_0 W0 w_opp_c w_opp_carry w_opp + w_digits w_to_Z _ _ _ _ _); + auto. + Qed. + + Let spec_ww_opp_carry : forall x, [|opp_carry x|] = wwB - [|x|] - 1. + Proof. + refine (spec_ww_opp_carry w_WW ww_Bm1 w_opp_carry w_digits w_to_Z _ _ _); + auto. exact (spec_WW op_spec). + Qed. + + Let spec_ww_succ_c : forall x, [+|succ_c x|] = [|x|] + 1. + Proof. + refine (spec_ww_succ_c w_0 w_0 ww_1 w_succ_c w_digits w_to_Z _ _ _ _);auto. + Qed. + + Let spec_ww_add_c : forall x y, [+|add_c x y|] = [|x|] + [|y|]. + Proof. + refine (spec_ww_add_c w_WW w_add_c w_add_carry_c w_digits w_to_Z _ _ _);auto. + exact (spec_WW op_spec). + Qed. + + Let spec_ww_add_carry_c : forall x y, [+|add_carry_c x y|] = [|x|]+[|y|]+1. + Proof. + refine (spec_ww_add_carry_c w_0 w_0 w_WW ww_1 w_succ_c w_add_c w_add_carry_c + w_digits w_to_Z _ _ _ _ _ _ _);auto. exact (spec_WW op_spec). + Qed. + + Let spec_ww_succ : forall x, [|succ x|] = ([|x|] + 1) mod wwB. + Proof. + refine (spec_ww_succ w_W0 ww_1 w_succ_c w_succ w_digits w_to_Z _ _ _ _ _); + auto. exact (spec_W0 op_spec). + Qed. + + Let spec_ww_add : forall x y, [|add x y|] = ([|x|] + [|y|]) mod wwB. + Proof. + refine (spec_ww_add w_add_c w_add w_add_carry w_digits w_to_Z _ _ _ _);auto. + Qed. + + Let spec_ww_add_carry : forall x y, [|add_carry x y|]=([|x|]+[|y|]+1)mod wwB. + Proof. + refine (spec_ww_add_carry w_W0 ww_1 w_succ_c w_add_carry_c w_succ + w_add w_add_carry w_digits w_to_Z _ _ _ _ _ _ _ _);auto. + exact (spec_W0 op_spec). + Qed. + + Let spec_ww_pred_c : forall x, [-|pred_c x|] = [|x|] - 1. + Proof. + refine (spec_ww_pred_c w_0 w_Bm1 w_WW ww_Bm1 w_pred_c w_digits w_to_Z + _ _ _ _ _);auto. exact (spec_WW op_spec). + Qed. + + Let spec_ww_sub_c : forall x y, [-|sub_c x y|] = [|x|] - [|y|]. + Proof. + refine (spec_ww_sub_c w_0 w_0 w_WW W0 w_opp_c w_opp_carry w_sub_c + w_sub_carry_c w_digits w_to_Z _ _ _ _ _ _ _);auto. exact (spec_WW op_spec). + Qed. + + Let spec_ww_sub_carry_c : forall x y, [-|sub_carry_c x y|] = [|x|]-[|y|]-1. + Proof. + refine (spec_ww_sub_carry_c w_0 w_Bm1 w_WW ww_Bm1 w_opp_carry w_pred_c + w_sub_c w_sub_carry_c w_digits w_to_Z _ _ _ _ _ _ _ _);auto. + exact (spec_WW op_spec). + Qed. + + Let spec_ww_pred : forall x, [|pred x|] = ([|x|] - 1) mod wwB. + Proof. + refine (spec_ww_pred w_0 w_Bm1 w_WW ww_Bm1 w_pred_c w_pred w_digits w_to_Z + _ _ _ _ _ _);auto. exact (spec_WW op_spec). + Qed. + + Let spec_ww_sub : forall x y, [|sub x y|] = ([|x|] - [|y|]) mod wwB. + Proof. + refine (spec_ww_sub w_0 w_0 w_WW W0 w_opp_c w_opp_carry w_sub_c w_opp + w_sub w_sub_carry w_digits w_to_Z _ _ _ _ _ _ _ _ _);auto. + exact (spec_WW op_spec). + Qed. + + Let spec_ww_sub_carry : forall x y, [|sub_carry x y|]=([|x|]-[|y|]-1) mod wwB. + Proof. + refine (spec_ww_sub_carry w_0 w_Bm1 w_WW ww_Bm1 w_opp_carry w_pred_c + w_sub_carry_c w_pred w_sub w_sub_carry w_digits w_to_Z _ _ _ _ _ _ _ _ _ _); + auto. exact (spec_WW op_spec). + Qed. + + Let spec_ww_mul_c : forall x y, [[mul_c x y ]] = [|x|] * [|y|]. + Proof. + refine (spec_ww_mul_c w_0 w_1 w_WW w_W0 w_mul_c add_c add add_carry w_digits + w_to_Z _ _ _ _ _ _ _ _ _);auto. exact (spec_WW op_spec). + exact (spec_W0 op_spec). exact (spec_mul_c op_spec). + Qed. + + Let spec_ww_karatsuba_c : forall x y, [[karatsuba_c x y ]] = [|x|] * [|y|]. + Proof. + refine (spec_ww_karatsuba_c _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ + _ _ _ _ _ _ _ _ _ _ _ _); auto. + unfold w_digits; apply spec_more_than_1_digit; auto. + exact (spec_WW op_spec). + exact (spec_W0 op_spec). + exact (spec_compare op_spec). + exact (spec_mul_c op_spec). + Qed. + + Let spec_ww_mul : forall x y, [|mul x y|] = ([|x|] * [|y|]) mod wwB. + Proof. + refine (spec_ww_mul w_W0 w_add w_mul_c w_mul add w_digits w_to_Z _ _ _ _ _); + auto. exact (spec_W0 op_spec). exact (spec_mul_c op_spec). + Qed. + + Let spec_ww_square_c : forall x, [[square_c x]] = [|x|] * [|x|]. + Proof. + refine (spec_ww_square_c w_0 w_1 w_WW w_W0 w_mul_c w_square_c add_c add + add_carry w_digits w_to_Z _ _ _ _ _ _ _ _ _ _);auto. + exact (spec_WW op_spec). exact (spec_W0 op_spec). + exact (spec_mul_c op_spec). exact (spec_square_c op_spec). + Qed. + + Let spec_w_div32 : forall a1 a2 a3 b1 b2, + wB / 2 <= (w_to_Z b1) -> + [|WW a1 a2|] < [|WW b1 b2|] -> + let (q, r) := div32 a1 a2 a3 b1 b2 in + (w_to_Z a1) * wwB + (w_to_Z a2) * wB + (w_to_Z a3) = + (w_to_Z q) * ((w_to_Z b1)*wB + (w_to_Z b2)) + [|r|] /\ + 0 <= [|r|] < (w_to_Z b1)*wB + w_to_Z b2. + Proof. + refine (spec_w_div32 w_0 w_Bm1 w_Bm2 w_WW w_compare w_add_c w_add_carry_c + w_add w_add_carry w_pred w_sub w_mul_c w_div21 sub_c w_digits w_to_Z + _ _ _ _ _ _ _ _ _ _ _ _ _ _ _);auto. + unfold w_Bm2, w_to_Z, w_pred, w_Bm1. + rewrite (spec_pred op_spec);rewrite (spec_Bm1 op_spec). + unfold w_digits;rewrite Zmod_small. ring. + assert (H:= wB_pos(znz_digits w_op)). omega. + exact (spec_WW op_spec). exact (spec_compare op_spec). + exact (spec_mul_c op_spec). exact (spec_div21 op_spec). + Qed. + + Let spec_ww_div21 : forall a1 a2 b, + wwB/2 <= [|b|] -> + [|a1|] < [|b|] -> + let (q,r) := div21 a1 a2 b in + [|a1|] *wwB+ [|a2|] = [|q|] * [|b|] + [|r|] /\ + 0 <= [|r|] < [|b|]. + Proof. + refine (spec_ww_div21 w_0 w_0W div32 ww_1 compare sub w_digits w_to_Z + _ _ _ _ _ _ _);auto. exact (spec_0W op_spec). + Qed. + + 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 w0 Hw0; simpl; unfold w_to_Z; rewrite Hw0. + unfold w_0; rewrite 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. + 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. + intros xh xl; simpl. + rewrite Zplus_comm; rewrite Z_mod_plus; auto with zarith. + rewrite Zmod_small; auto with zarith. + unfold wB, base; auto with zarith. + Qed. + + Let spec_ww_digits: + [|_ww_zdigits|] = Zpos (xO w_digits). + Proof. + unfold w_to_Z, _ww_zdigits. + rewrite spec_add2. + unfold w_to_Z, w_zdigits, w_digits. + rewrite spec_zdigits; auto. + rewrite Zpos_xO; auto with zarith. + Qed. + + + Let spec_ww_head00 : forall x, [|x|] = 0 -> [|head0 x|] = Zpos _ww_digits. + Proof. + 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). + Qed. + + Let spec_ww_head0 : forall x, 0 < [|x|] -> + wwB/ 2 <= 2 ^ [|head0 x|] * [|x|] < wwB. + Proof. + refine (spec_ww_head0 w_0 w_0W w_compare w_head0 + w_add2 w_zdigits _ww_zdigits + w_to_Z _ _ _ _ _ _ _);auto. + exact (spec_0W op_spec). + exact (spec_compare op_spec). + exact (spec_zdigits op_spec). + Qed. + + Let spec_ww_tail00 : forall x, [|x|] = 0 -> [|tail0 x|] = Zpos _ww_digits. + Proof. + refine (spec_ww_tail00 w_0 w_0W + w_compare w_tail0 w_add2 w_zdigits _ww_zdigits + w_to_Z _ _ _ (refl_equal _ww_digits) _ _ _ _); auto. + exact (spec_compare op_spec). + exact (spec_tail00 op_spec). + exact (spec_zdigits op_spec). + Qed. + + + Let spec_ww_tail0 : forall x, 0 < [|x|] -> + exists y, 0 <= y /\ [|x|] = (2 * y + 1) * 2 ^ [|tail0 x|]. + Proof. + refine (spec_ww_tail0 (w_digits := w_digits) w_0 w_0W w_compare w_tail0 + w_add2 w_zdigits _ww_zdigits w_to_Z _ _ _ _ _ _ _);auto. + exact (spec_0W op_spec). + exact (spec_compare op_spec). + exact (spec_zdigits op_spec). + Qed. + + Lemma spec_ww_add_mul_div : forall x y p, + [|p|] <= Zpos _ww_digits -> + [| add_mul_div p x y |] = + ([|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 + sub w_digits w_zdigits low w_to_Z + _ _ _ _ _ _ _ _ _ _ _);auto. + exact (spec_WW op_spec). + exact (spec_W0 op_spec). + exact (spec_0W op_spec). + exact (spec_zdigits op_spec). + Qed. + + Let spec_ww_div_gt : forall a b, + [|a|] > [|b|] -> 0 < [|b|] -> + let (q,r) := div_gt a b in + [|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 + 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 (spec_WW op_spec). + exact (spec_0W op_spec). + 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 spec_w_div32. + exact (spec_zdigits op_spec). + exact spec_ww_digits. + exact spec_ww_1. + exact spec_ww_add_mul_div. + Qed. + + Let spec_ww_div : forall a b, 0 < [|b|] -> + let (q,r) := div a b in + [|a|] = [|q|] * [|b|] + [|r|] /\ + 0 <= [|r|] < [|b|]. + Proof. + refine (spec_ww_div w_digits ww_1 compare div_gt w_to_Z _ _ _ _);auto. + Qed. + + Let spec_ww_mod_gt : forall a b, + [|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 + w_opp_c w_opp w_opp_carry w_sub_c w_sub w_sub_carry w_div_gt w_mod_gt + w_add_mul_div w_head0 w_div21 div32 _ww_zdigits ww_1 add_mul_div + w_zdigits w_to_Z + _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _);auto. + exact (spec_WW op_spec). + exact (spec_0W op_spec). + exact (spec_compare op_spec). + exact (spec_div_gt op_spec). + exact (spec_div21 op_spec). + exact (spec_zdigits op_spec). + exact spec_ww_add_mul_div. + Qed. + + Let spec_ww_mod : forall a b, 0 < [|b|] -> [|mod_ a b|] = [|a|] mod [|b|]. + Proof. + refine (spec_ww_mod w_digits W0 compare mod_gt w_to_Z _ _ _);auto. + Qed. + + 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 _ + 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 + w_opp_carry w_sub_c w_sub w_sub_carry w_gcd_gt w_add_mul_div w_head0 + w_div21 div32 _ww_zdigits ww_1 add_mul_div w_zdigits w_to_Z + _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _);auto. + exact (spec_WW op_spec). + exact (spec_0W op_spec). + exact (spec_compare op_spec). + exact (spec_div21 op_spec). + exact (spec_zdigits op_spec). + exact spec_ww_add_mul_div. + refine (@spec_gcd_cont w 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 + _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 + w_opp_carry w_sub_c w_sub w_sub_carry w_gcd_gt w_add_mul_div w_head0 + w_div21 div32 _ww_zdigits ww_1 add_mul_div w_zdigits w_to_Z + _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _);auto. + exact (spec_WW op_spec). + exact (spec_0W op_spec). + exact (spec_compare op_spec). + exact (spec_div21 op_spec). + exact (spec_zdigits op_spec). + exact spec_ww_add_mul_div. + refine (@spec_gcd_cont w 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, + match is_even x with + true => [|x|] mod 2 = 0 + | 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). + Qed. + + Let spec_ww_sqrt2 : forall x y, + wwB/ 4 <= [|x|] -> + let (s,r) := sqrt2 x y in + [[WW x y]] = [|s|] ^ 2 + [+|r|] /\ + [+|r|] <= 2 * [|s|]. + Proof. + intros x y H. + refine (@spec_ww_sqrt2 w 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 + _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _); auto. + exact (spec_zdigits op_spec). + exact (spec_more_than_1_digit op_spec). + exact (spec_0W op_spec). + exact (spec_is_even op_spec). + exact (spec_compare op_spec). + exact (spec_square_c op_spec). + exact (spec_div21 op_spec). + exact (spec_ww_add_mul_div). + exact (spec_sqrt2 op_spec). + 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 + w_sub w_add_mul_div w_digits w_zdigits _ww_zdigits + w_sqrt2 pred add_mul_div head0 compare + _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _); auto. + 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). + Qed. + + Lemma mk_znz2_spec : znz_spec mk_zn2z_op. + Proof. + apply mk_znz_spec;auto. + exact spec_ww_add_mul_div. + + refine (@spec_ww_pos_mod w w_0 w_digits w_zdigits w_WW + w_pos_mod compare w_0W low sub _ww_zdigits w_to_Z + _ _ _ _ _ _ _ _ _ _ _ _);auto. + exact (spec_WW op_spec). + exact (spec_pos_mod op_spec). + exact (spec_0W op_spec). + exact (spec_zdigits op_spec). + unfold w_to_Z, w_zdigits. + rewrite (spec_zdigits op_spec). + rewrite <- Zpos_xO; exact spec_ww_digits. + Qed. + + Lemma mk_znz2_karatsuba_spec : znz_spec mk_zn2z_op_karatsuba. + Proof. + apply mk_znz_spec;auto. + exact spec_ww_add_mul_div. + refine (@spec_ww_pos_mod w w_0 w_digits w_zdigits w_WW + w_pos_mod compare w_0W low sub _ww_zdigits w_to_Z + _ _ _ _ _ _ _ _ _ _ _ _);auto. + exact (spec_WW op_spec). + exact (spec_pos_mod op_spec). + exact (spec_0W op_spec). + exact (spec_zdigits op_spec). + unfold w_to_Z, w_zdigits. + rewrite (spec_zdigits op_spec). + rewrite <- Zpos_xO; exact spec_ww_digits. + Qed. + +End Z_2nZ. + +Section MulAdd. + + Variable w: Set. + Variable op: znz_op w. + Variable sop: znz_spec op. + + Definition mul_add:= w_mul_add (znz_0 op) (znz_succ op) (znz_add_c op) (znz_mul_c op). + + Notation "[| x |]" := (znz_to_Z op 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). + + + Lemma spec_mul_add: forall x y z, + let (zh, zl) := mul_add x y z in + [||WW zh zl||] = [|x|] * [|y|] + [|z|]. + 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). + Qed. + +End MulAdd. + + + + diff --git a/theories/Numbers/Cyclic/DoubleCyclic/Z_2nZ.v b/theories/Numbers/Cyclic/DoubleCyclic/Z_2nZ.v deleted file mode 100644 index 26d2393f9..000000000 --- a/theories/Numbers/Cyclic/DoubleCyclic/Z_2nZ.v +++ /dev/null @@ -1,922 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* WW w_0 p | C1 p => WW w_1 p end. - - Let _ww_digits := xO w_digits. - - Let _ww_zdigits := w_add2 w_zdigits w_zdigits. - - Let to_Z := zn2z_to_Z wB w_to_Z. - - Let ww_of_pos p := - match w_of_pos p with - | (N0, l) => (N0, WW w_0 l) - | (Npos ph,l) => - let (n,h) := w_of_pos ph in (n, w_WW h l) - end. - - - Let head0 := - Eval lazy beta delta [ww_head0] in - ww_head0 w_0 w_0W w_compare w_head0 w_add2 w_zdigits _ww_zdigits. - - Let tail0 := - 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). - - (* ** Comparison ** *) - Let compare := - Eval lazy beta delta[ww_compare] in ww_compare w_0 w_compare. - - Let eq0 (x:zn2z w) := - match x with - | W0 => true - | _ => false - end. - - (* ** Opposites ** *) - Let opp_c := - Eval lazy beta delta [ww_opp_c] in ww_opp_c w_0 w_opp_c w_opp_carry. - - Let opp := - Eval lazy beta delta [ww_opp] in ww_opp w_0 w_opp_c w_opp_carry w_opp. - - Let opp_carry := - Eval lazy beta delta [ww_opp_carry] in ww_opp_carry w_WW ww_Bm1 w_opp_carry. - - (* ** Additions ** *) - - Let succ_c := - Eval lazy beta delta [ww_succ_c] in ww_succ_c w_0 ww_1 w_succ_c. - - Let add_c := - Eval lazy beta delta [ww_add_c] in ww_add_c w_WW w_add_c w_add_carry_c. - - Let add_carry_c := - Eval lazy beta iota delta [ww_add_carry_c ww_succ_c] in - ww_add_carry_c w_0 w_WW ww_1 w_succ_c w_add_c w_add_carry_c. - - Let succ := - Eval lazy beta delta [ww_succ] in ww_succ w_W0 ww_1 w_succ_c w_succ. - - Let add := - Eval lazy beta delta [ww_add] in ww_add w_add_c w_add w_add_carry. - - Let add_carry := - Eval lazy beta iota delta [ww_add_carry ww_succ] in - ww_add_carry w_W0 ww_1 w_succ_c w_add_carry_c w_succ w_add w_add_carry. - - (* ** Subtractions ** *) - - Let pred_c := - Eval lazy beta delta [ww_pred_c] in ww_pred_c w_Bm1 w_WW ww_Bm1 w_pred_c. - - Let sub_c := - Eval lazy beta iota delta [ww_sub_c ww_opp_c] in - ww_sub_c w_0 w_WW w_opp_c w_opp_carry w_sub_c w_sub_carry_c. - - Let sub_carry_c := - Eval lazy beta iota delta [ww_sub_carry_c ww_pred_c ww_opp_carry] in - ww_sub_carry_c w_Bm1 w_WW ww_Bm1 w_opp_carry w_pred_c w_sub_c w_sub_carry_c. - - Let pred := - Eval lazy beta delta [ww_pred] in ww_pred w_Bm1 w_WW ww_Bm1 w_pred_c w_pred. - - Let sub := - Eval lazy beta iota delta [ww_sub ww_opp] in - ww_sub w_0 w_WW w_opp_c w_opp_carry w_sub_c w_opp w_sub w_sub_carry. - - Let sub_carry := - Eval lazy beta iota delta [ww_sub_carry ww_pred ww_opp_carry] in - ww_sub_carry w_Bm1 w_WW ww_Bm1 w_opp_carry w_pred_c w_sub_carry_c w_pred - w_sub w_sub_carry. - - - (* ** Multiplication ** *) - - Let mul_c := - Eval lazy beta iota delta [ww_mul_c double_mul_c] in - ww_mul_c w_0 w_1 w_WW w_W0 w_mul_c add_c add add_carry. - - Let karatsuba_c := - Eval lazy beta iota delta [ww_karatsuba_c double_mul_c kara_prod] in - ww_karatsuba_c w_0 w_1 w_WW w_W0 w_compare w_add w_sub w_mul_c - add_c add add_carry sub_c sub. - - Let mul := - Eval lazy beta delta [ww_mul] in - ww_mul w_W0 w_add w_mul_c w_mul add. - - Let square_c := - Eval lazy beta delta [ww_square_c] in - ww_square_c w_0 w_1 w_WW w_W0 w_mul_c w_square_c add_c add add_carry. - - (* Division operation *) - - Let div32 := - Eval lazy beta iota delta [w_div32] in - w_div32 w_0 w_Bm1 w_Bm2 w_WW w_compare w_add_c w_add_carry_c - w_add w_add_carry w_pred w_sub w_mul_c w_div21 sub_c. - - Let div21 := - 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 add_mul_div := - Eval lazy beta delta [ww_add_mul_div] in - ww_add_mul_div w_0 w_WW w_W0 w_0W compare w_add_mul_div sub w_zdigits low. - - Let div_gt := - Eval lazy beta delta [ww_div_gt] in - ww_div_gt 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. - - Let div := - Eval lazy beta delta [ww_div] in ww_div ww_1 compare div_gt. - - Let mod_gt := - Eval lazy beta delta [ww_mod_gt] in - ww_mod_gt 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_mod_gt w_add_mul_div w_head0 w_div21 div32 _ww_zdigits add_mul_div w_zdigits. - - Let mod_ := - Eval lazy beta delta [ww_mod] in ww_mod compare mod_gt. - - Let pos_mod := - Eval lazy beta delta [ww_pos_mod] in - ww_pos_mod w_0 w_zdigits w_WW w_pos_mod compare w_0W low sub _ww_zdigits. - - Let is_even := - Eval lazy beta delta [ww_is_even] in ww_is_even w_is_even. - - Let sqrt2 := - Eval lazy beta delta [ww_sqrt2] in - ww_sqrt2 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_zdigits w_add_c w_sqrt2 w_pred pred_c - pred add_c add sub_c add_mul_div. - - Let sqrt := - Eval lazy beta delta [ww_sqrt] in - ww_sqrt w_is_even w_0 w_sub w_add_mul_div w_zdigits - _ww_zdigits w_sqrt2 pred add_mul_div head0 compare low. - - Let gcd_gt_fix := - Eval cbv beta delta [ww_gcd_gt_aux ww_gcd_gt_body] in - ww_gcd_gt_aux 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 add_mul_div - w_zdigits. - - Let gcd_cont := - Eval lazy beta delta [gcd_cont] in gcd_cont ww_1 w_1 w_compare. - - Let gcd_gt := - Eval lazy beta delta [ww_gcd_gt] in - ww_gcd_gt w_0 w_eq0 w_gcd_gt _ww_digits gcd_gt_fix gcd_cont. - - Let gcd := - Eval lazy beta delta [ww_gcd] in - ww_gcd compare w_0 w_eq0 w_gcd_gt _ww_digits gcd_gt_fix gcd_cont. - - (* ** Record of operators on 2 words *) - - Definition mk_zn2z_op := - mk_znz_op _ww_digits _ww_zdigits - to_Z ww_of_pos head0 tail0 - W0 ww_1 ww_Bm1 - ww_WW ww_W0 ww_0W - compare eq0 - opp_c opp opp_carry - succ_c add_c add_carry_c - succ add add_carry - pred_c sub_c sub_carry_c - pred sub sub_carry - mul_c mul square_c - div21 div_gt div - mod_gt mod_ - gcd_gt gcd - add_mul_div - pos_mod - is_even - sqrt2 - sqrt. - - Definition mk_zn2z_op_karatsuba := - mk_znz_op _ww_digits _ww_zdigits - to_Z ww_of_pos head0 tail0 - W0 ww_1 ww_Bm1 - ww_WW ww_W0 ww_0W - compare eq0 - opp_c opp opp_carry - succ_c add_c add_carry_c - succ add add_carry - pred_c sub_c sub_carry_c - pred sub sub_carry - karatsuba_c mul square_c - div21 div_gt div - mod_gt mod_ - gcd_gt gcd - add_mul_div - pos_mod - is_even - sqrt2 - sqrt. - - (* Proof *) - Variable op_spec : znz_spec w_op. - - 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_WW op_spec) - (spec_0W op_spec) - (spec_W0 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). - - Let wwB := base _ww_digits. - - Notation "[| x |]" := (to_Z x) (at level 0, x at level 99). - - Notation "[+| c |]" := - (interp_carry 1 wwB to_Z c) (at level 0, x at level 99). - - Notation "[-| c |]" := - (interp_carry (-1) wwB to_Z c) (at level 0, x at level 99). - - Notation "[[ x ]]" := (zn2z_to_Z wwB to_Z x) (at level 0, x at level 99). - - Let spec_ww_to_Z : forall x, 0 <= [| x |] < wwB. - Proof. refine (spec_ww_to_Z w_digits w_to_Z _);auto. Qed. - - Let spec_ww_of_pos : forall p, - 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, w_WW, to_Z. - rewrite (spec_WW op_spec). replace wwB with (wB*wB). - unfold wB,w_digits;clear H;destruct n;ring. - symmetry. rewrite <- Zpower_2; exact (wwB_wBwB w_digits). - Qed. - - Let spec_ww_0 : [|W0|] = 0. - Proof. reflexivity. Qed. - - Let spec_ww_1 : [|ww_1|] = 1. - Proof. refine (spec_ww_1 w_0 w_1 w_digits w_to_Z _ _);auto. Qed. - - Let spec_ww_Bm1 : [|ww_Bm1|] = wwB - 1. - Proof. refine (spec_ww_Bm1 w_Bm1 w_digits w_to_Z _);auto. Qed. - - Let spec_ww_WW : forall h l, [[ww_WW h l]] = [|h|] * wwB + [|l|]. - Proof. - intros h l. replace wwB with (wB*wB). destruct h;simpl. - destruct l;simpl;ring. ring. - symmetry. rewrite <- Zpower_2; exact (wwB_wBwB w_digits). - Qed. - - Let spec_ww_0W : forall l, [[ww_0W l]] = [|l|]. - Proof. - intros l. replace wwB with (wB*wB). - destruct l;simpl;ring. - symmetry. ring_simplify; exact (wwB_wBwB w_digits). - Qed. - - Let spec_ww_W0 : forall h, [[ww_W0 h]] = [|h|]*wwB. - Proof. - intros h. replace wwB with (wB*wB). - destruct h;simpl;ring. - symmetry. ring_simplify; exact (wwB_wBwB w_digits). - Qed. - - Let spec_ww_compare : - forall x y, - match compare x y with - | Eq => [|x|] = [|y|] - | Lt => [|x|] < [|y|] - | Gt => [|x|] > [|y|] - end. - 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. - Proof. destruct x;simpl;intros;trivial;discriminate. Qed. - - Let spec_ww_opp_c : forall x, [-|opp_c x|] = -[|x|]. - Proof. - refine(spec_ww_opp_c w_0 w_0 W0 w_opp_c w_opp_carry w_digits w_to_Z _ _ _ _); - auto. - Qed. - - Let spec_ww_opp : forall x, [|opp x|] = (-[|x|]) mod wwB. - Proof. - refine(spec_ww_opp w_0 w_0 W0 w_opp_c w_opp_carry w_opp - w_digits w_to_Z _ _ _ _ _); - auto. - Qed. - - Let spec_ww_opp_carry : forall x, [|opp_carry x|] = wwB - [|x|] - 1. - Proof. - refine (spec_ww_opp_carry w_WW ww_Bm1 w_opp_carry w_digits w_to_Z _ _ _); - auto. exact (spec_WW op_spec). - Qed. - - Let spec_ww_succ_c : forall x, [+|succ_c x|] = [|x|] + 1. - Proof. - refine (spec_ww_succ_c w_0 w_0 ww_1 w_succ_c w_digits w_to_Z _ _ _ _);auto. - Qed. - - Let spec_ww_add_c : forall x y, [+|add_c x y|] = [|x|] + [|y|]. - Proof. - refine (spec_ww_add_c w_WW w_add_c w_add_carry_c w_digits w_to_Z _ _ _);auto. - exact (spec_WW op_spec). - Qed. - - Let spec_ww_add_carry_c : forall x y, [+|add_carry_c x y|] = [|x|]+[|y|]+1. - Proof. - refine (spec_ww_add_carry_c w_0 w_0 w_WW ww_1 w_succ_c w_add_c w_add_carry_c - w_digits w_to_Z _ _ _ _ _ _ _);auto. exact (spec_WW op_spec). - Qed. - - Let spec_ww_succ : forall x, [|succ x|] = ([|x|] + 1) mod wwB. - Proof. - refine (spec_ww_succ w_W0 ww_1 w_succ_c w_succ w_digits w_to_Z _ _ _ _ _); - auto. exact (spec_W0 op_spec). - Qed. - - Let spec_ww_add : forall x y, [|add x y|] = ([|x|] + [|y|]) mod wwB. - Proof. - refine (spec_ww_add w_add_c w_add w_add_carry w_digits w_to_Z _ _ _ _);auto. - Qed. - - Let spec_ww_add_carry : forall x y, [|add_carry x y|]=([|x|]+[|y|]+1)mod wwB. - Proof. - refine (spec_ww_add_carry w_W0 ww_1 w_succ_c w_add_carry_c w_succ - w_add w_add_carry w_digits w_to_Z _ _ _ _ _ _ _ _);auto. - exact (spec_W0 op_spec). - Qed. - - Let spec_ww_pred_c : forall x, [-|pred_c x|] = [|x|] - 1. - Proof. - refine (spec_ww_pred_c w_0 w_Bm1 w_WW ww_Bm1 w_pred_c w_digits w_to_Z - _ _ _ _ _);auto. exact (spec_WW op_spec). - Qed. - - Let spec_ww_sub_c : forall x y, [-|sub_c x y|] = [|x|] - [|y|]. - Proof. - refine (spec_ww_sub_c w_0 w_0 w_WW W0 w_opp_c w_opp_carry w_sub_c - w_sub_carry_c w_digits w_to_Z _ _ _ _ _ _ _);auto. exact (spec_WW op_spec). - Qed. - - Let spec_ww_sub_carry_c : forall x y, [-|sub_carry_c x y|] = [|x|]-[|y|]-1. - Proof. - refine (spec_ww_sub_carry_c w_0 w_Bm1 w_WW ww_Bm1 w_opp_carry w_pred_c - w_sub_c w_sub_carry_c w_digits w_to_Z _ _ _ _ _ _ _ _);auto. - exact (spec_WW op_spec). - Qed. - - Let spec_ww_pred : forall x, [|pred x|] = ([|x|] - 1) mod wwB. - Proof. - refine (spec_ww_pred w_0 w_Bm1 w_WW ww_Bm1 w_pred_c w_pred w_digits w_to_Z - _ _ _ _ _ _);auto. exact (spec_WW op_spec). - Qed. - - Let spec_ww_sub : forall x y, [|sub x y|] = ([|x|] - [|y|]) mod wwB. - Proof. - refine (spec_ww_sub w_0 w_0 w_WW W0 w_opp_c w_opp_carry w_sub_c w_opp - w_sub w_sub_carry w_digits w_to_Z _ _ _ _ _ _ _ _ _);auto. - exact (spec_WW op_spec). - Qed. - - Let spec_ww_sub_carry : forall x y, [|sub_carry x y|]=([|x|]-[|y|]-1) mod wwB. - Proof. - refine (spec_ww_sub_carry w_0 w_Bm1 w_WW ww_Bm1 w_opp_carry w_pred_c - w_sub_carry_c w_pred w_sub w_sub_carry w_digits w_to_Z _ _ _ _ _ _ _ _ _ _); - auto. exact (spec_WW op_spec). - Qed. - - Let spec_ww_mul_c : forall x y, [[mul_c x y ]] = [|x|] * [|y|]. - Proof. - refine (spec_ww_mul_c w_0 w_1 w_WW w_W0 w_mul_c add_c add add_carry w_digits - w_to_Z _ _ _ _ _ _ _ _ _);auto. exact (spec_WW op_spec). - exact (spec_W0 op_spec). exact (spec_mul_c op_spec). - Qed. - - Let spec_ww_karatsuba_c : forall x y, [[karatsuba_c x y ]] = [|x|] * [|y|]. - Proof. - refine (spec_ww_karatsuba_c _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ - _ _ _ _ _ _ _ _ _ _ _ _); auto. - unfold w_digits; apply spec_more_than_1_digit; auto. - exact (spec_WW op_spec). - exact (spec_W0 op_spec). - exact (spec_compare op_spec). - exact (spec_mul_c op_spec). - Qed. - - Let spec_ww_mul : forall x y, [|mul x y|] = ([|x|] * [|y|]) mod wwB. - Proof. - refine (spec_ww_mul w_W0 w_add w_mul_c w_mul add w_digits w_to_Z _ _ _ _ _); - auto. exact (spec_W0 op_spec). exact (spec_mul_c op_spec). - Qed. - - Let spec_ww_square_c : forall x, [[square_c x]] = [|x|] * [|x|]. - Proof. - refine (spec_ww_square_c w_0 w_1 w_WW w_W0 w_mul_c w_square_c add_c add - add_carry w_digits w_to_Z _ _ _ _ _ _ _ _ _ _);auto. - exact (spec_WW op_spec). exact (spec_W0 op_spec). - exact (spec_mul_c op_spec). exact (spec_square_c op_spec). - Qed. - - Let spec_w_div32 : forall a1 a2 a3 b1 b2, - wB / 2 <= (w_to_Z b1) -> - [|WW a1 a2|] < [|WW b1 b2|] -> - let (q, r) := div32 a1 a2 a3 b1 b2 in - (w_to_Z a1) * wwB + (w_to_Z a2) * wB + (w_to_Z a3) = - (w_to_Z q) * ((w_to_Z b1)*wB + (w_to_Z b2)) + [|r|] /\ - 0 <= [|r|] < (w_to_Z b1)*wB + w_to_Z b2. - Proof. - refine (spec_w_div32 w_0 w_Bm1 w_Bm2 w_WW w_compare w_add_c w_add_carry_c - w_add w_add_carry w_pred w_sub w_mul_c w_div21 sub_c w_digits w_to_Z - _ _ _ _ _ _ _ _ _ _ _ _ _ _ _);auto. - unfold w_Bm2, w_to_Z, w_pred, w_Bm1. - rewrite (spec_pred op_spec);rewrite (spec_Bm1 op_spec). - unfold w_digits;rewrite Zmod_small. ring. - assert (H:= wB_pos(znz_digits w_op)). omega. - exact (spec_WW op_spec). exact (spec_compare op_spec). - exact (spec_mul_c op_spec). exact (spec_div21 op_spec). - Qed. - - Let spec_ww_div21 : forall a1 a2 b, - wwB/2 <= [|b|] -> - [|a1|] < [|b|] -> - let (q,r) := div21 a1 a2 b in - [|a1|] *wwB+ [|a2|] = [|q|] * [|b|] + [|r|] /\ - 0 <= [|r|] < [|b|]. - Proof. - refine (spec_ww_div21 w_0 w_0W div32 ww_1 compare sub w_digits w_to_Z - _ _ _ _ _ _ _);auto. exact (spec_0W op_spec). - Qed. - - 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 w0 Hw0; simpl; unfold w_to_Z; rewrite Hw0. - unfold w_0; rewrite 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. - 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. - intros xh xl; simpl. - rewrite Zplus_comm; rewrite Z_mod_plus; auto with zarith. - rewrite Zmod_small; auto with zarith. - unfold wB, base; auto with zarith. - Qed. - - Let spec_ww_digits: - [|_ww_zdigits|] = Zpos (xO w_digits). - Proof. - unfold w_to_Z, _ww_zdigits. - rewrite spec_add2. - unfold w_to_Z, w_zdigits, w_digits. - rewrite spec_zdigits; auto. - rewrite Zpos_xO; auto with zarith. - Qed. - - - Let spec_ww_head00 : forall x, [|x|] = 0 -> [|head0 x|] = Zpos _ww_digits. - Proof. - 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). - Qed. - - Let spec_ww_head0 : forall x, 0 < [|x|] -> - wwB/ 2 <= 2 ^ [|head0 x|] * [|x|] < wwB. - Proof. - refine (spec_ww_head0 w_0 w_0W w_compare w_head0 - w_add2 w_zdigits _ww_zdigits - w_to_Z _ _ _ _ _ _ _);auto. - exact (spec_0W op_spec). - exact (spec_compare op_spec). - exact (spec_zdigits op_spec). - Qed. - - Let spec_ww_tail00 : forall x, [|x|] = 0 -> [|tail0 x|] = Zpos _ww_digits. - Proof. - refine (spec_ww_tail00 w_0 w_0W - w_compare w_tail0 w_add2 w_zdigits _ww_zdigits - w_to_Z _ _ _ (refl_equal _ww_digits) _ _ _ _); auto. - exact (spec_compare op_spec). - exact (spec_tail00 op_spec). - exact (spec_zdigits op_spec). - Qed. - - - Let spec_ww_tail0 : forall x, 0 < [|x|] -> - exists y, 0 <= y /\ [|x|] = (2 * y + 1) * 2 ^ [|tail0 x|]. - Proof. - refine (spec_ww_tail0 (w_digits := w_digits) w_0 w_0W w_compare w_tail0 - w_add2 w_zdigits _ww_zdigits w_to_Z _ _ _ _ _ _ _);auto. - exact (spec_0W op_spec). - exact (spec_compare op_spec). - exact (spec_zdigits op_spec). - Qed. - - Lemma spec_ww_add_mul_div : forall x y p, - [|p|] <= Zpos _ww_digits -> - [| add_mul_div p x y |] = - ([|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 - sub w_digits w_zdigits low w_to_Z - _ _ _ _ _ _ _ _ _ _ _);auto. - exact (spec_WW op_spec). - exact (spec_W0 op_spec). - exact (spec_0W op_spec). - exact (spec_zdigits op_spec). - Qed. - - Let spec_ww_div_gt : forall a b, - [|a|] > [|b|] -> 0 < [|b|] -> - let (q,r) := div_gt a b in - [|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 - 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 (spec_WW op_spec). - exact (spec_0W op_spec). - 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 spec_w_div32. - exact (spec_zdigits op_spec). - exact spec_ww_digits. - exact spec_ww_1. - exact spec_ww_add_mul_div. - Qed. - - Let spec_ww_div : forall a b, 0 < [|b|] -> - let (q,r) := div a b in - [|a|] = [|q|] * [|b|] + [|r|] /\ - 0 <= [|r|] < [|b|]. - Proof. - refine (spec_ww_div w_digits ww_1 compare div_gt w_to_Z _ _ _ _);auto. - Qed. - - Let spec_ww_mod_gt : forall a b, - [|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 - w_opp_c w_opp w_opp_carry w_sub_c w_sub w_sub_carry w_div_gt w_mod_gt - w_add_mul_div w_head0 w_div21 div32 _ww_zdigits ww_1 add_mul_div - w_zdigits w_to_Z - _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _);auto. - exact (spec_WW op_spec). - exact (spec_0W op_spec). - exact (spec_compare op_spec). - exact (spec_div_gt op_spec). - exact (spec_div21 op_spec). - exact (spec_zdigits op_spec). - exact spec_ww_add_mul_div. - Qed. - - Let spec_ww_mod : forall a b, 0 < [|b|] -> [|mod_ a b|] = [|a|] mod [|b|]. - Proof. - refine (spec_ww_mod w_digits W0 compare mod_gt w_to_Z _ _ _);auto. - Qed. - - 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 _ - 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 - w_opp_carry w_sub_c w_sub w_sub_carry w_gcd_gt w_add_mul_div w_head0 - w_div21 div32 _ww_zdigits ww_1 add_mul_div w_zdigits w_to_Z - _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _);auto. - exact (spec_WW op_spec). - exact (spec_0W op_spec). - exact (spec_compare op_spec). - exact (spec_div21 op_spec). - exact (spec_zdigits op_spec). - exact spec_ww_add_mul_div. - refine (@spec_gcd_cont w 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 - _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 - w_opp_carry w_sub_c w_sub w_sub_carry w_gcd_gt w_add_mul_div w_head0 - w_div21 div32 _ww_zdigits ww_1 add_mul_div w_zdigits w_to_Z - _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _);auto. - exact (spec_WW op_spec). - exact (spec_0W op_spec). - exact (spec_compare op_spec). - exact (spec_div21 op_spec). - exact (spec_zdigits op_spec). - exact spec_ww_add_mul_div. - refine (@spec_gcd_cont w 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, - match is_even x with - true => [|x|] mod 2 = 0 - | 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). - Qed. - - Let spec_ww_sqrt2 : forall x y, - wwB/ 4 <= [|x|] -> - let (s,r) := sqrt2 x y in - [[WW x y]] = [|s|] ^ 2 + [+|r|] /\ - [+|r|] <= 2 * [|s|]. - Proof. - intros x y H. - refine (@spec_ww_sqrt2 w 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 - _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _); auto. - exact (spec_zdigits op_spec). - exact (spec_more_than_1_digit op_spec). - exact (spec_0W op_spec). - exact (spec_is_even op_spec). - exact (spec_compare op_spec). - exact (spec_square_c op_spec). - exact (spec_div21 op_spec). - exact (spec_ww_add_mul_div). - exact (spec_sqrt2 op_spec). - 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 - w_sub w_add_mul_div w_digits w_zdigits _ww_zdigits - w_sqrt2 pred add_mul_div head0 compare - _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _); auto. - 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). - Qed. - - Lemma mk_znz2_spec : znz_spec mk_zn2z_op. - Proof. - apply mk_znz_spec;auto. - exact spec_ww_add_mul_div. - - refine (@spec_ww_pos_mod w w_0 w_digits w_zdigits w_WW - w_pos_mod compare w_0W low sub _ww_zdigits w_to_Z - _ _ _ _ _ _ _ _ _ _ _ _);auto. - exact (spec_WW op_spec). - exact (spec_pos_mod op_spec). - exact (spec_0W op_spec). - exact (spec_zdigits op_spec). - unfold w_to_Z, w_zdigits. - rewrite (spec_zdigits op_spec). - rewrite <- Zpos_xO; exact spec_ww_digits. - Qed. - - Lemma mk_znz2_karatsuba_spec : znz_spec mk_zn2z_op_karatsuba. - Proof. - apply mk_znz_spec;auto. - exact spec_ww_add_mul_div. - refine (@spec_ww_pos_mod w w_0 w_digits w_zdigits w_WW - w_pos_mod compare w_0W low sub _ww_zdigits w_to_Z - _ _ _ _ _ _ _ _ _ _ _ _);auto. - exact (spec_WW op_spec). - exact (spec_pos_mod op_spec). - exact (spec_0W op_spec). - exact (spec_zdigits op_spec). - unfold w_to_Z, w_zdigits. - rewrite (spec_zdigits op_spec). - rewrite <- Zpos_xO; exact spec_ww_digits. - Qed. - -End Z_2nZ. - -Section MulAdd. - - Variable w: Set. - Variable op: znz_op w. - Variable sop: znz_spec op. - - Definition mul_add:= w_mul_add (znz_0 op) (znz_succ op) (znz_add_c op) (znz_mul_c op). - - Notation "[| x |]" := (znz_to_Z op 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). - - - Lemma spec_mul_add: forall x y z, - let (zh, zl) := mul_add x y z in - [||WW zh zl||] = [|x|] * [|y|] + [|z|]. - 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). - Qed. - -End MulAdd. - - - - diff --git a/theories/Numbers/Cyclic/Int31/Cyclic31.v b/theories/Numbers/Cyclic/Int31/Cyclic31.v new file mode 100644 index 000000000..49a1a0b5b --- /dev/null +++ b/theories/Numbers/Cyclic/Int31/Cyclic31.v @@ -0,0 +1,114 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* N*int31 : p => N,i where p = N*2^31+phi i *) + exact head031. (* number of head 0 *) + exact tail031. (* number of tail 0 *) + + (* Basic constructors *) + exact 0. (* 0 *) + exact 1. (* 1 *) + exact Tn. (* 2^31 - 1 *) + (* A function which given two int31 i and j, returns a double word + which is worth i*2^31+j *) + exact (fun i j => match (match i ?= 0 with | Eq => j ?= 0 | not0 => not0 end) with | Eq => W0 | _ => WW i j end). + (* two special cases where i and j are respectively taken equal to 0 *) + exact (fun i => match i ?= 0 with | Eq => W0 | _ => WW i 0 end). + exact (fun j => match j ?= 0 with | Eq => W0 | _ => WW 0 j end). + + (* Comparison *) + exact compare31. + exact (fun i => match i ?= 0 with | Eq => true | _ => false end). + + (* Basic arithmetic operations *) + (* opposite functions *) + exact (fun i => 0 -c i). + exact (fun i => 0 - i). + exact (fun i => 0-i-1). (* the carry is always -1*) + (* successor and addition functions *) + exact (fun i => i +c 1). + exact add31c. + exact add31carryc. + exact (fun i => i + 1). + exact add31. + exact (fun i j => i + j + 1). + (* predecessor and subtraction functions *) + exact (fun i => i -c 1). + exact sub31c. + exact sub31carryc. + exact (fun i => i - 1). + exact sub31. + exact (fun i j => i - j - 1). + (* multiplication functions *) + exact mul31c. + exact mul31. + exact (fun x => x *c x). + + (* special (euclidian) division operations *) + exact div3121. + exact div31. (* this is supposed to be the special case of division a/b where a > b *) + exact div31. + (* euclidian division remainder *) + (* again special case for a > b *) + exact (fun i j => let (_,r) := i/j in r). + exact (fun i j => let (_,r) := i/j in r). + (* gcd functions *) + exact gcd31. (*gcd_gt*) + exact gcd31. (*gcd*) + + (* shift operations *) + exact addmuldiv31. (*add_mul_div *) +(*modulo 2^p *) + exact (fun p i => + match compare31 p 32 with + | Lt => addmuldiv31 p 0 (addmuldiv31 (31-p) i 0) + | _ => i + end). + + (* is i even ? *) + exact (fun i => let (_,r) := i/2 in + match r ?= 0 with + | Eq => true + | _ => false + end). + + (* square root operations *) + exact sqrt312. (* sqrt2 *) + exact sqrt31. (* sqr *) +Defined. + + +Definition int31_spec : znz_spec int31_op. +Admitted. + + +Module Int31Cyclic <: CyclicType. + Definition w := int31. + Definition w_op := int31_op. + Definition w_spec := int31_spec. +End Int31Cyclic. diff --git a/theories/Numbers/Cyclic/Int31/Z_31Z.v b/theories/Numbers/Cyclic/Int31/Z_31Z.v deleted file mode 100644 index 3b5944ed3..000000000 --- a/theories/Numbers/Cyclic/Int31/Z_31Z.v +++ /dev/null @@ -1,114 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* N*int31 : p => N,i where p = N*2^31+phi i *) - exact head031. (* number of head 0 *) - exact tail031. (* number of tail 0 *) - - (* Basic constructors *) - exact 0. (* 0 *) - exact 1. (* 1 *) - exact Tn. (* 2^31 - 1 *) - (* A function which given two int31 i and j, returns a double word - which is worth i*2^31+j *) - exact (fun i j => match (match i ?= 0 with | Eq => j ?= 0 | not0 => not0 end) with | Eq => W0 | _ => WW i j end). - (* two special cases where i and j are respectively taken equal to 0 *) - exact (fun i => match i ?= 0 with | Eq => W0 | _ => WW i 0 end). - exact (fun j => match j ?= 0 with | Eq => W0 | _ => WW 0 j end). - - (* Comparison *) - exact compare31. - exact (fun i => match i ?= 0 with | Eq => true | _ => false end). - - (* Basic arithmetic operations *) - (* opposite functions *) - exact (fun i => 0 -c i). - exact (fun i => 0 - i). - exact (fun i => 0-i-1). (* the carry is always -1*) - (* successor and addition functions *) - exact (fun i => i +c 1). - exact add31c. - exact add31carryc. - exact (fun i => i + 1). - exact add31. - exact (fun i j => i + j + 1). - (* predecessor and subtraction functions *) - exact (fun i => i -c 1). - exact sub31c. - exact sub31carryc. - exact (fun i => i - 1). - exact sub31. - exact (fun i j => i - j - 1). - (* multiplication functions *) - exact mul31c. - exact mul31. - exact (fun x => x *c x). - - (* special (euclidian) division operations *) - exact div3121. - exact div31. (* this is supposed to be the special case of division a/b where a > b *) - exact div31. - (* euclidian division remainder *) - (* again special case for a > b *) - exact (fun i j => let (_,r) := i/j in r). - exact (fun i j => let (_,r) := i/j in r). - (* gcd functions *) - exact gcd31. (*gcd_gt*) - exact gcd31. (*gcd*) - - (* shift operations *) - exact addmuldiv31. (*add_mul_div *) -(*modulo 2^p *) - exact (fun p i => - match compare31 p 32 with - | Lt => addmuldiv31 p 0 (addmuldiv31 (31-p) i 0) - | _ => i - end). - - (* is i even ? *) - exact (fun i => let (_,r) := i/2 in - match r ?= 0 with - | Eq => true - | _ => false - end). - - (* square root operations *) - exact sqrt312. (* sqrt2 *) - exact sqrt31. (* sqr *) -Defined. - - -Definition int31_spec : znz_spec int31_op. -Admitted. - - -Module Int31_words <: CyclicType. - Definition w := int31. - Definition w_op := int31_op. - Definition w_spec := int31_spec. -End Int31_words. diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v index 25a39aeba..033364f72 100644 --- a/theories/Numbers/Natural/BigN/BigN.v +++ b/theories/Numbers/Natural/BigN/BigN.v @@ -15,13 +15,13 @@ Author: Arnaud Spiwack *) Require Export Int31. -Require Import Z_nZ. -Require Import Z_31Z. +Require Import CyclicAxioms. +Require Import Cyclic31. Require Import NMake. Open Scope int31_scope. -Module BigN := NMake.Make Int31_words. +Module BigN := NMake.Make Int31Cyclic. Definition bigN := BigN.t. diff --git a/theories/Numbers/Natural/BigN/NMake_gen.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml index 3d098c755..d15006cb4 100644 --- a/theories/Numbers/Natural/BigN/NMake_gen.ml +++ b/theories/Numbers/Natural/BigN/NMake_gen.ml @@ -71,11 +71,11 @@ let _ = pr ""; pr "Require Import BigNumPrelude."; pr "Require Import ZArith."; + pr "Require Import CyclicAxioms."; pr "Require Import DoubleType."; pr "Require Import DoubleMul."; pr "Require Import DoubleDivn1."; - pr "Require Import Z_nZ."; - pr "Require Import Z_2nZ."; + pr "Require Import DoubleCyclic."; pr "Require Import Nbasic."; pr "Require Import Wf_nat."; pr "Require Import StreamMemo."; @@ -1776,7 +1776,7 @@ let _ = pp " (spec_zdigits ww_spec)"; pp " (spec_0 ww_spec) (spec_WW ww_spec) (spec_head0 ww_spec)"; pp " (spec_add_mul_div ww_spec) (spec_div21 ww_spec) "; - pp " (Z_nZ.spec_compare ww_spec) (Z_nZ.spec_sub ww_spec))."; + pp " (CyclicAxioms.spec_compare ww_spec) (CyclicAxioms.spec_sub ww_spec))."; pp ""; for i = 0 to size do @@ -2018,7 +2018,7 @@ let _ = pp " (spec_zdigits ww_spec)"; pp " (spec_0 ww_spec) (spec_WW ww_spec) (spec_head0 ww_spec)"; pp " (spec_add_mul_div ww_spec) (spec_div21 ww_spec) "; - pp " (Z_nZ.spec_compare ww_spec) (Z_nZ.spec_sub ww_spec))."; + pp " (CyclicAxioms.spec_compare ww_spec) (CyclicAxioms.spec_sub ww_spec))."; pp ""; pr " Theorem spec_mod_gt:"; @@ -2576,7 +2576,7 @@ let _ = pp " )."; pp " rewrite (spec_0 Hw)."; pp " rewrite Zmult_0_l; rewrite Zplus_0_l."; - pp " rewrite (Z_nZ.spec_sub Hw)."; + pp " rewrite (CyclicAxioms.spec_sub Hw)."; pp " rewrite Zmod_small; auto with zarith."; pp " rewrite (spec_zdigits Hw)."; pp " rewrite F0."; @@ -2754,7 +2754,7 @@ let _ = pp " assert (F1: znz_to_Z ww1_op (znz_head0 ww1_op xx) <= Zpos (znz_digits ww1_op))."; pp " case (Zle_lt_or_eq _ _ HH1); intros HH5."; pp " apply Zlt_le_weak."; - pp " case (Z_nZ.spec_head0 Hw1 xx)."; + pp " case (CyclicAxioms.spec_head0 Hw1 xx)."; pp " rewrite <- Hx; auto."; pp " intros _ Hu; unfold base in Hu."; pp " case (Zle_or_lt (Zpos (znz_digits ww1_op))"; @@ -2766,7 +2766,7 @@ let _ = pp " apply Zle_lt_trans with (2 := Hu)."; pp " apply Zmult_le_compat_l; auto with zarith."; pp " apply Zpower_le_monotone; auto with zarith."; - pp " rewrite (Z_nZ.spec_head00 Hw1 xx); auto with zarith."; + pp " rewrite (CyclicAxioms.spec_head00 Hw1 xx); auto with zarith."; pp " rewrite Zdiv_0_l; auto with zarith."; pp " rewrite Zplus_0_r."; pp " case (Zle_lt_or_eq _ _ HH1); intros HH5."; @@ -2779,7 +2779,7 @@ let _ = pp " split; auto with zarith ."; pp " apply Zlt_le_trans with (base (znz_digits ww1_op))."; pp " rewrite Hx."; - pp " case (Z_nZ.spec_head0 Hw1 xx); auto."; + pp " case (CyclicAxioms.spec_head0 Hw1 xx); auto."; pp " rewrite <- Hx; auto."; pp " intros _ Hu; rewrite Zmult_comm in Hu."; pp " apply Zle_lt_trans with (2 := Hu)."; @@ -2794,7 +2794,7 @@ let _ = pp " rewrite Zmod_small; auto with zarith."; pp " intros HH; apply HH."; pp " rewrite Hy; apply Zle_trans with (1 := Hl)."; - pp " rewrite (Z_nZ.spec_head00 Hw1 xx); auto with zarith."; + pp " rewrite (CyclicAxioms.spec_head00 Hw1 xx); auto with zarith."; pp " rewrite <- (spec_zdigits Hw); auto with zarith."; pp " rewrite <- (spec_zdigits Hw1); auto with zarith."; pp " assert (F5: forall n m, (n <= m)%snat ->" "%"; diff --git a/theories/Numbers/Natural/BigN/Nbasic.v b/theories/Numbers/Natural/BigN/Nbasic.v index ea472c860..ed7a7871f 100644 --- a/theories/Numbers/Natural/BigN/Nbasic.v +++ b/theories/Numbers/Natural/BigN/Nbasic.v @@ -15,8 +15,8 @@ Require Import BigNumPrelude. Require Import Max. Require Import DoubleType. Require Import DoubleBase. -Require Import Z_nZ. -Require Import Z_2nZ. +Require Import CyclicAxioms. +Require Import DoubleCyclic. (* To compute the necessary height *) -- cgit v1.2.3