diff options
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Numbers/Cyclic/Abstract/NZCyclic.v | 4 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/Abstract/Z_nZ.v (renamed from theories/Numbers/Cyclic/Abstract/ZnZ.v) | 12 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v (renamed from theories/Numbers/Cyclic/DoubleCyclic/GenAdd.v) | 12 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v (renamed from theories/Numbers/Cyclic/DoubleCyclic/GenBase.v) | 90 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v (renamed from theories/Numbers/Cyclic/DoubleCyclic/GenDiv.v) | 84 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v (renamed from theories/Numbers/Cyclic/DoubleCyclic/GenDivn1.v) | 336 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.v (renamed from theories/Numbers/Cyclic/DoubleCyclic/GenLift.v) | 12 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.v (renamed from theories/Numbers/Cyclic/DoubleCyclic/GenMul.v) | 68 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v (renamed from theories/Numbers/Cyclic/DoubleCyclic/GenSqrt.v) | 10 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.v (renamed from theories/Numbers/Cyclic/DoubleCyclic/GenSub.v) | 12 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v (renamed from theories/Numbers/Cyclic/DoubleCyclic/Basic_type.v) | 0 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/DoubleCyclic/Z_2nZ.v (renamed from theories/Numbers/Cyclic/DoubleCyclic/Zn2Z.v) | 31 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/Int31/Int31.v | 2 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/Int31/Z_31Z.v (renamed from theories/Numbers/Cyclic/Int31/Z31Z.v) | 2 | ||||
| -rw-r--r-- | theories/Numbers/Natural/BigN/BigN.v | 4 | ||||
| -rw-r--r-- | theories/Numbers/Natural/BigN/NMake_gen.ml | 112 | ||||
| -rw-r--r-- | theories/Numbers/Natural/BigN/Nbasic.v | 64 |
17 files changed, 428 insertions, 427 deletions
diff --git a/theories/Numbers/Cyclic/Abstract/NZCyclic.v b/theories/Numbers/Cyclic/Abstract/NZCyclic.v index 7cc4e5434..df3af4b63 100644 --- a/theories/Numbers/Cyclic/Abstract/NZCyclic.v +++ b/theories/Numbers/Cyclic/Abstract/NZCyclic.v @@ -12,8 +12,8 @@ Require Export NZAxioms. Require Import BigNumPrelude. -Require Import Basic_type. -Require Import ZnZ. +Require Import DoubleType. +Require Import Z_nZ. (** * A Z/nZ representation (module type [CyclicType]) implements [NZAxiomsSig], e.g. the common properties between N and Z. *) diff --git a/theories/Numbers/Cyclic/Abstract/ZnZ.v b/theories/Numbers/Cyclic/Abstract/Z_nZ.v index 9ec7648e6..6d19e6613 100644 --- a/theories/Numbers/Cyclic/Abstract/ZnZ.v +++ b/theories/Numbers/Cyclic/Abstract/Z_nZ.v @@ -17,13 +17,13 @@ Set Implicit Arguments. Require Import ZArith. Require Import Znumtheory. Require Import BigNumPrelude. -Require Import Basic_type. +Require Import DoubleType. Open Local Scope Z_scope. -(** First, a description via operator records and spec records. *) +(** First, a description via an operator record and a spec record. *) -Section ZnZ_Op. +Section Z_nZ_Op. Variable znz : Set. @@ -90,9 +90,9 @@ Section ZnZ_Op. znz_sqrt2 : znz -> znz -> znz * carry znz; znz_sqrt : znz -> znz }. -End ZnZ_Op. +End Z_nZ_Op. -Section ZnZ_Spec. +Section Z_nZ_Spec. Variable w : Set. Variable w_op : znz_op w. @@ -270,7 +270,7 @@ Section ZnZ_Spec. [|w_sqrt x|] ^ 2 <= [|x|] < ([|w_sqrt x|] + 1) ^ 2 }. -End ZnZ_Spec. +End Z_nZ_Spec. diff --git a/theories/Numbers/Cyclic/DoubleCyclic/GenAdd.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v index 68703129b..d198361f1 100644 --- a/theories/Numbers/Cyclic/DoubleCyclic/GenAdd.v +++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v @@ -14,12 +14,12 @@ Set Implicit Arguments. Require Import ZArith. Require Import BigNumPrelude. -Require Import Basic_type. -Require Import GenBase. +Require Import DoubleType. +Require Import DoubleBase. Open Local Scope Z_scope. -Section GenAdd. +Section DoubleAdd. Variable w : Set. Variable w_0 : w. Variable w_1 : w. @@ -143,7 +143,7 @@ Section GenAdd. end end. - (*Section GenProof.*) + (*Section DoubleProof.*) Variable w_digits : positive. Variable w_to_Z : w -> Z. @@ -314,5 +314,5 @@ Section GenAdd. rewrite(mod_wwB w_digits w_to_Z spec_to_Z);rewrite spec_w_add_carry;trivial. Qed. -(* End GenProof. *) -End GenAdd. +(* End DoubleProof. *) +End DoubleAdd. diff --git a/theories/Numbers/Cyclic/DoubleCyclic/GenBase.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v index 8d07c6dee..3d1d1c235 100644 --- a/theories/Numbers/Cyclic/DoubleCyclic/GenBase.v +++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v @@ -14,11 +14,11 @@ Set Implicit Arguments. Require Import ZArith. Require Import BigNumPrelude. -Require Import Basic_type. +Require Import DoubleType. Open Local Scope Z_scope. -Section GenBase. +Section DoubleBase. Variable w : Set. Variable w_0 : w. Variable w_1 : w. @@ -59,7 +59,7 @@ Section GenBase. | _ => WW W0 l end. - Definition gen_WW (n:nat) := + Definition double_WW (n:nat) := match n return word w n -> word w n -> word w (S n) with | O => w_WW | S n => @@ -70,18 +70,18 @@ Section GenBase. end end. - Fixpoint gen_digits (n:nat) : positive := + Fixpoint double_digits (n:nat) : positive := match n with | O => w_digits - | S n => xO (gen_digits n) + | S n => xO (double_digits n) end. - Definition gen_wB n := base (gen_digits n). + Definition double_wB n := base (double_digits n). - Fixpoint gen_to_Z (n:nat) : word w n -> Z := + Fixpoint double_to_Z (n:nat) : word w n -> Z := match n return word w n -> Z with | O => w_to_Z - | S n => zn2z_to_Z (gen_wB n) (gen_to_Z n) + | S n => zn2z_to_Z (double_wB n) (double_to_Z n) end. Fixpoint extend_aux (n:nat) (x:zn2z w) {struct n}: word w (S n) := @@ -97,13 +97,13 @@ Section GenBase. | _ => extend_aux n r end. - Definition gen_0 n : word w n := + Definition double_0 n : word w n := match n return word w n with | O => w_0 | S _ => W0 end. - Definition gen_split (n:nat) (x:zn2z (word w n)) := + Definition double_split (n:nat) (x:zn2z (word w n)) := match x with | W0 => match n return word w n * word w n with @@ -149,7 +149,7 @@ Section GenBase. end. - Section GenProof. + Section DoubleProof. Notation wB := (base w_digits). Notation wwB := (base ww_digits). Notation "[| x |]" := (w_to_Z x) (at level 0, x at level 99). @@ -158,7 +158,7 @@ Section GenBase. (interp_carry 1 wwB ww_to_Z c) (at level 0, x at level 99). Notation "[-[ c ]]" := (interp_carry (-1) wwB ww_to_Z c) (at level 0, x at level 99). - Notation "[! n | x !]" := (gen_to_Z n x) (at level 0, x at level 99). + Notation "[! n | x !]" := (double_to_Z n x) (at level 0, x at level 99). Variable spec_w_0 : [|w_0|] = 0. Variable spec_w_1 : [|w_1|] = 1. @@ -294,29 +294,29 @@ Section GenBase. apply beta_lex_inv;auto with zarith. Qed. - Lemma gen_wB_wwB : forall n, gen_wB n * gen_wB n = gen_wB (S n). + Lemma double_wB_wwB : forall n, double_wB n * double_wB n = double_wB (S n). Proof. - intros n;unfold gen_wB;simpl. - unfold base;rewrite (Zpos_xO (gen_digits n)). - replace (2 * Zpos (gen_digits n)) with - (Zpos (gen_digits n) + Zpos (gen_digits n)). + intros n;unfold double_wB;simpl. + unfold base;rewrite (Zpos_xO (double_digits n)). + replace (2 * Zpos (double_digits n)) with + (Zpos (double_digits n) + Zpos (double_digits n)). symmetry; apply Zpower_exp;intro;discriminate. ring. Qed. - Lemma gen_wB_pos: - forall n, 0 <= gen_wB n. + Lemma double_wB_pos: + forall n, 0 <= double_wB n. Proof. - intros n; unfold gen_wB, base; auto with zarith. + intros n; unfold double_wB, base; auto with zarith. Qed. - Lemma gen_wB_more_digits: - forall n, wB <= gen_wB n. + Lemma double_wB_more_digits: + forall n, wB <= double_wB n. Proof. clear spec_w_0 spec_w_1 spec_w_Bm1 w_0 w_1 w_Bm1. intros n; elim n; clear n; auto. - unfold gen_wB, gen_digits; auto with zarith. - intros n H1; rewrite <- gen_wB_wwB. + unfold double_wB, double_digits; auto with zarith. + intros n H1; rewrite <- double_wB_wwB. apply Zle_trans with (wB * 1). rewrite Zmult_1_r; apply Zle_refl. apply Zmult_le_compat; auto with zarith. @@ -327,22 +327,22 @@ Section GenBase. unfold base; auto with zarith. Qed. - Lemma spec_gen_to_Z : - forall n (x:word w n), 0 <= [!n | x!] < gen_wB n. + Lemma spec_double_to_Z : + forall n (x:word w n), 0 <= [!n | x!] < double_wB n. Proof. clear spec_w_0 spec_w_1 spec_w_Bm1 w_0 w_1 w_Bm1. induction n;intros. exact (spec_to_Z x). - unfold gen_to_Z;fold gen_to_Z. + unfold double_to_Z;fold double_to_Z. destruct x;unfold zn2z_to_Z. - unfold gen_wB,base;split;auto with zarith. + unfold double_wB,base;split;auto with zarith. assert (U0:= IHn w0);assert (U1:= IHn w1). split;auto with zarith. - apply Zlt_le_trans with ((gen_wB n - 1) * gen_wB n + gen_wB n). - assert (gen_to_Z n w0*gen_wB n <= (gen_wB n - 1)*gen_wB n). + apply Zlt_le_trans with ((double_wB n - 1) * double_wB n + double_wB n). + assert (double_to_Z n w0*double_wB n <= (double_wB n - 1)*double_wB n). apply Zmult_le_compat_r;auto with zarith. auto with zarith. - rewrite <- gen_wB_wwB. - replace ((gen_wB n - 1) * gen_wB n + gen_wB n) with (gen_wB n * gen_wB n); + rewrite <- double_wB_wwB. + replace ((double_wB n - 1) * double_wB n + double_wB n) with (double_wB n * double_wB n); [auto with zarith | ring]. Qed. @@ -356,23 +356,23 @@ Section GenBase. intros xx yy H1; simpl in H1. assert (F1: [!n | xx!] = 0). case (Zle_lt_or_eq 0 ([!n | xx!])); auto. - case (spec_gen_to_Z n xx); auto. + case (spec_double_to_Z n xx); auto. intros F2. - assert (F3 := gen_wB_more_digits n). + assert (F3 := double_wB_more_digits n). assert (F4: 0 <= [!n | yy!]). - case (spec_gen_to_Z n yy); auto. - assert (F5: 1 * wB <= [!n | xx!] * gen_wB n); + case (spec_double_to_Z n yy); auto. + assert (F5: 1 * wB <= [!n | xx!] * double_wB n); auto with zarith. apply Zmult_le_compat; auto with zarith. unfold base; auto with zarith. - simpl get_low; simpl gen_to_Z. + simpl get_low; simpl double_to_Z. generalize H1; clear H1. rewrite F1; rewrite Zmult_0_l; rewrite Zplus_0_l. intros H1; apply Hrec; auto. Qed. - Lemma spec_gen_WW : forall n (h l : word w n), - [!S n|gen_WW n h l!] = [!n|h!] * gen_wB n + [!n|l!]. + Lemma spec_double_WW : forall n (h l : word w n), + [!S n|double_WW n h l!] = [!n|h!] * double_wB n + [!n|l!]. Proof. induction n;simpl;intros;trivial. destruct h;auto. @@ -389,12 +389,12 @@ Section GenBase. rewrite <- H;exact (spec_extend_aux n (WW w0 w1)). Qed. - Lemma spec_gen_0 : forall n, [!n|gen_0 n!] = 0. + Lemma spec_double_0 : forall n, [!n|double_0 n!] = 0. Proof. destruct n;trivial. Qed. - Lemma spec_gen_split : forall n x, - let (h,l) := gen_split n x in - [!S n|x!] = [!n|h!] * gen_wB n + [!n|l!]. + Lemma spec_double_split : forall n x, + let (h,l) := double_split n x in + [!S n|x!] = [!n|h!] * double_wB n + [!n|l!]. Proof. destruct x;simpl;auto. destruct n;simpl;trivial. @@ -440,7 +440,7 @@ Section GenBase. Qed. - End GenProof. + End DoubleProof. -End GenBase. +End DoubleBase. diff --git a/theories/Numbers/Cyclic/DoubleCyclic/GenDiv.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v index 057ad3c06..cac2cc5b5 100644 --- a/theories/Numbers/Cyclic/DoubleCyclic/GenDiv.v +++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v @@ -14,11 +14,11 @@ Set Implicit Arguments. Require Import ZArith. Require Import BigNumPrelude. -Require Import Basic_type. -Require Import GenBase. -Require Import GenDivn1. -Require Import GenAdd. -Require Import GenSub. +Require Import DoubleType. +Require Import DoubleBase. +Require Import DoubleDivn1. +Require Import DoubleAdd. +Require Import DoubleSub. Open Local Scope Z_scope. @@ -199,7 +199,7 @@ generalize (spec_ww_compare p ww_zdigits); End POS_MOD. -Section GenDiv32. +Section DoubleDiv32. Variable w : Set. Variable w_0 : w. @@ -470,9 +470,9 @@ Section GenDiv32. Qed. -End GenDiv32. +End DoubleDiv32. -Section GenDiv21. +Section DoubleDiv21. Variable w : Set. Variable w_0 : w. @@ -631,9 +631,9 @@ Section GenDiv21. [rewrite H4;simpl|rewrite wwB_wBwB];ring. Qed. -End GenDiv21. +End DoubleDiv21. -Section GenDivGt. +Section DoubleDivGt. Variable w : Set. Variable w_digits : positive. Variable w_0 : w. @@ -681,9 +681,9 @@ Section GenDivGt. end. Definition ww_div_gt a b := - Eval lazy beta iota delta [ww_div_gt_aux gen_divn1 - gen_divn1_p gen_divn1_p_aux gen_divn1_0 gen_divn1_0_aux - gen_split gen_0 gen_WW] in + Eval lazy beta iota delta [ww_div_gt_aux double_divn1 + double_divn1_p double_divn1_p_aux double_divn1_0 double_divn1_0_aux + double_split double_0 double_WW] in match a, b with | W0, _ => (W0,W0) | _, W0 => (W0,W0) @@ -695,7 +695,7 @@ Section GenDivGt. match w_compare w_0 bh with | Eq => let(q,r):= - gen_divn1 w_zdigits w_0 w_WW w_head0 w_add_mul_div w_div21 + double_divn1 w_zdigits w_0 w_WW w_head0 w_add_mul_div w_div21 w_compare w_sub 1 a bl in (q, w_0W r) | Lt => ww_div_gt_aux ah al bh bl @@ -722,9 +722,9 @@ Section GenDivGt. end. Definition ww_mod_gt a b := - Eval lazy beta iota delta [ww_mod_gt_aux gen_modn1 - gen_modn1_p gen_modn1_p_aux gen_modn1_0 gen_modn1_0_aux - gen_split gen_0 gen_WW snd] in + Eval lazy beta iota delta [ww_mod_gt_aux double_modn1 + double_modn1_p double_modn1_p_aux double_modn1_0 double_modn1_0_aux + double_split double_0 double_WW snd] in match a, b with | W0, _ => W0 | _, W0 => W0 @@ -733,7 +733,7 @@ Section GenDivGt. else match w_compare w_0 bh with | Eq => - w_0W (gen_modn1 w_zdigits w_0 w_head0 w_add_mul_div w_div21 + w_0W (double_modn1 w_zdigits w_0 w_head0 w_add_mul_div w_div21 w_compare w_sub 1 a bl) | Lt => ww_mod_gt_aux ah al bh bl | Gt => W0 (* cas absurde *) @@ -741,15 +741,15 @@ Section GenDivGt. end. Definition ww_gcd_gt_body (cont: w->w->w->w->zn2z w) (ah al bh bl: w) := - Eval lazy beta iota delta [ww_mod_gt_aux gen_modn1 - gen_modn1_p gen_modn1_p_aux gen_modn1_0 gen_modn1_0_aux - gen_split gen_0 gen_WW snd] in + Eval lazy beta iota delta [ww_mod_gt_aux double_modn1 + double_modn1_p double_modn1_p_aux double_modn1_0 double_modn1_0_aux + double_split double_0 double_WW snd] in match w_compare w_0 bh with | Eq => match w_compare w_0 bl with | Eq => WW ah al (* normalement n'arrive pas si forme normale *) | Lt => - let m := gen_modn1 w_zdigits w_0 w_head0 w_add_mul_div w_div21 + let m := double_modn1 w_zdigits w_0 w_head0 w_add_mul_div w_div21 w_compare w_sub 1 (WW ah al) bl in WW w_0 (w_gcd_gt bl m) | Gt => W0 (* absurde *) @@ -764,7 +764,7 @@ Section GenDivGt. match w_compare w_0 ml with | Eq => WW bh bl | _ => - let r := gen_modn1 w_zdigits w_0 w_head0 w_add_mul_div w_div21 + let r := double_modn1 w_zdigits w_0 w_head0 w_add_mul_div w_div21 w_compare w_sub 1 (WW bh bl) ml in WW w_0 (w_gcd_gt ml r) end @@ -1039,7 +1039,7 @@ Section GenDivGt. match w_compare w_0 bh with | Eq => let(q,r):= - gen_divn1 w_zdigits w_0 w_WW w_head0 w_add_mul_div w_div21 + double_divn1 w_zdigits w_0 w_WW w_head0 w_add_mul_div w_div21 w_compare w_sub 1 a bl in (q, w_0W r) | Lt => ww_div_gt_aux ah al bh bl @@ -1062,11 +1062,11 @@ Section GenDivGt. 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. - assert (H2:= @spec_gen_divn1 w w_digits w_zdigits w_0 w_WW w_head0 w_add_mul_div + assert (H2:= @spec_double_divn1 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 spec_div21 spec_compare spec_sub 1 (WW ah al) bl Hpos). - unfold gen_to_Z,gen_wB,gen_digits in H2. - destruct (gen_divn1 w_zdigits w_0 w_WW w_head0 w_add_mul_div w_div21 + unfold double_to_Z,double_wB,double_digits in H2. + destruct (double_divn1 w_zdigits w_0 w_WW w_head0 w_add_mul_div w_div21 w_compare w_sub 1 (WW ah al) bl). rewrite spec_w_0W;unfold ww_to_Z;trivial. @@ -1118,7 +1118,7 @@ Section GenDivGt. else match w_compare w_0 bh with | Eq => - w_0W (gen_modn1 w_zdigits w_0 w_head0 w_add_mul_div w_div21 + w_0W (double_modn1 w_zdigits w_0 w_head0 w_add_mul_div w_div21 w_compare w_sub 1 a bl) | Lt => ww_mod_gt_aux ah al bh bl | Gt => W0 (* cas absurde *) @@ -1135,7 +1135,7 @@ Section GenDivGt. match w_compare w_0 bh with | Eq => let(q,r):= - gen_divn1 w_zdigits w_0 w_WW w_head0 w_add_mul_div w_div21 + double_divn1 w_zdigits w_0 w_WW w_head0 w_add_mul_div w_div21 w_compare w_sub 1 a bl in (q, w_0W r) | Lt => ww_div_gt_aux ah al bh bl @@ -1155,9 +1155,9 @@ Section GenDivGt. 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_gen_modn1_aux w w_zdigits w_0 w_WW w_head0 w_add_mul_div + 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 (gen_divn1 w_zdigits w_0 w_WW w_head0 w_add_mul_div w_div21 w_compare w_sub 1 + destruct (double_divn1 w_zdigits w_0 w_WW w_head0 w_add_mul_div w_div21 w_compare w_sub 1 (WW ah al) bl);simpl;trivial. rewrite spec_ww_mod_gt_aux_eq;trivial;symmetry;trivial. trivial. @@ -1197,7 +1197,7 @@ Section GenDivGt. match w_compare w_0 bl with | Eq => WW ah al (* normalement n'arrive pas si forme normale *) | Lt => - let m := gen_modn1 w_zdigits w_0 w_head0 w_add_mul_div w_div21 + let m := double_modn1 w_zdigits w_0 w_head0 w_add_mul_div w_div21 w_compare w_sub 1 (WW ah al) bl in WW w_0 (w_gcd_gt bl m) | Gt => W0 (* absurde *) @@ -1212,7 +1212,7 @@ Section GenDivGt. match w_compare w_0 ml with | Eq => WW bh bl | _ => - let r := gen_modn1 w_zdigits w_0 w_head0 w_add_mul_div w_div21 + let r := double_modn1 w_zdigits w_0 w_head0 w_add_mul_div w_div21 w_compare w_sub 1 (WW bh bl) ml in WW w_0 (w_gcd_gt ml r) end @@ -1235,12 +1235,12 @@ Section GenDivGt. 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 (gen_to_Z w_digits w_to_Z 1 (WW ah al)). - rewrite <- (@spec_gen_modn1 w w_digits w_zdigits w_0 w_WW w_head0 w_add_mul_div + 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 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 spec_div21 spec_compare spec_sub 1 (WW ah al) bl Hbl). apply spec_gcd_gt. - rewrite (@spec_gen_modn1 w w_digits w_zdigits w_0 w_WW); trivial. + 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;elimtype False;omega. @@ -1257,12 +1257,12 @@ Section GenDivGt. 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. - change ([|bh|] * wB + [|bl|]) with (gen_to_Z w_digits w_to_Z 1 (WW bh bl)). - rewrite <- (@spec_gen_modn1 w w_digits w_zdigits w_0 w_WW w_head0 w_add_mul_div + 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 spec_div21 spec_compare spec_sub 1 (WW bh bl) ml Hml). apply spec_gcd_gt. - rewrite (@spec_gen_modn1 w w_digits w_zdigits w_0 w_WW); trivial. + 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;elimtype False;omega. @@ -1340,9 +1340,9 @@ Section GenDivGt. ring_simplify (n + 1 - 1);trivial. Qed. -End GenDivGt. +End DoubleDivGt. -Section GenDiv. +Section DoubleDiv. Variable w : Set. Variable w_digits : positive. @@ -1536,5 +1536,5 @@ Section GenDiv. apply spec_ww_gcd_gt;zarith. Qed. -End GenDiv. +End DoubleDiv. diff --git a/theories/Numbers/Cyclic/DoubleCyclic/GenDivn1.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v index cbf487f4b..00ba4e4ee 100644 --- a/theories/Numbers/Cyclic/DoubleCyclic/GenDivn1.v +++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v @@ -14,8 +14,8 @@ Set Implicit Arguments. Require Import ZArith. Require Import BigNumPrelude. -Require Import Basic_type. -Require Import GenBase. +Require Import DoubleType. +Require Import DoubleBase. Open Local Scope Z_scope. @@ -40,7 +40,7 @@ Section GENDIVN1. Notation wB := (base w_digits). Notation "[| x |]" := (w_to_Z x) (at level 0, x at level 99). - Notation "[! n | x !]" := (gen_to_Z w_digits w_to_Z n x) + Notation "[! n | x !]" := (double_to_Z w_digits w_to_Z n x) (at level 0, x at level 99). Notation "[[ x ]]" := (zn2z_to_Z wB w_to_Z x) (at level 0, x at level 99). @@ -77,64 +77,64 @@ Section GENDIVN1. Variable b2p : w. Variable b2p_le : wB/2 <= [|b2p|]. - Definition gen_divn1_0_aux n (divn1: w -> word w n -> word w n * w) r h := - let (hh,hl) := gen_split w_0 n h in + Definition double_divn1_0_aux n (divn1: w -> word w n -> word w n * w) r h := + let (hh,hl) := double_split w_0 n h in let (qh,rh) := divn1 r hh in let (ql,rl) := divn1 rh hl in - (gen_WW w_WW n qh ql, rl). + (double_WW w_WW n qh ql, rl). - Fixpoint gen_divn1_0 (n:nat) : w -> word w n -> word w n * w := + Fixpoint double_divn1_0 (n:nat) : w -> word w n -> word w n * w := match n return w -> word w n -> word w n * w with | O => fun r x => w_div21 r x b2p - | S n => gen_divn1_0_aux n (gen_divn1_0 n) + | S n => double_divn1_0_aux n (double_divn1_0 n) end. Lemma spec_split : forall (n : nat) (x : zn2z (word w n)), - let (h, l) := gen_split w_0 n x in - [!S n | x!] = [!n | h!] * gen_wB w_digits n + [!n | l!]. - Proof (spec_gen_split w_0 w_digits w_to_Z spec_0). + let (h, l) := double_split w_0 n x in + [!S n | x!] = [!n | h!] * double_wB w_digits n + [!n | l!]. + Proof (spec_double_split w_0 w_digits w_to_Z spec_0). - Lemma spec_gen_divn1_0 : forall n r a, + Lemma spec_double_divn1_0 : forall n r a, [|r|] < [|b2p|] -> - let (q,r') := gen_divn1_0 n r a in - [|r|] * gen_wB w_digits n + [!n|a!] = [!n|q!] * [|b2p|] + [|r'|] /\ + let (q,r') := double_divn1_0 n r a in + [|r|] * double_wB w_digits n + [!n|a!] = [!n|q!] * [|b2p|] + [|r'|] /\ 0 <= [|r'|] < [|b2p|]. Proof. induction n;intros. exact (spec_div21 a b2p_le H). - simpl (gen_divn1_0 (S n) r a); unfold gen_divn1_0_aux. - assert (H1 := spec_split n a);destruct (gen_split w_0 n a) as (hh,hl). + simpl (double_divn1_0 (S n) r a); unfold double_divn1_0_aux. + assert (H1 := spec_split n a);destruct (double_split w_0 n a) as (hh,hl). rewrite H1. - assert (H2 := IHn r hh H);destruct (gen_divn1_0 n r hh) as (qh,rh). + assert (H2 := IHn r hh H);destruct (double_divn1_0 n r hh) as (qh,rh). destruct H2. assert ([|rh|] < [|b2p|]). omega. - assert (H4 := IHn rh hl H3);destruct (gen_divn1_0 n rh hl) as (ql,rl). + assert (H4 := IHn rh hl H3);destruct (double_divn1_0 n rh hl) as (ql,rl). destruct H4;split;trivial. - rewrite spec_gen_WW;trivial. - rewrite <- gen_wB_wwB. + rewrite spec_double_WW;trivial. + rewrite <- double_wB_wwB. rewrite Zmult_assoc;rewrite Zplus_assoc;rewrite <- Zmult_plus_distr_l. rewrite H0;rewrite Zmult_plus_distr_l;rewrite <- Zplus_assoc. rewrite H4;ring. Qed. - Definition gen_modn1_0_aux n (modn1:w -> word w n -> w) r h := - let (hh,hl) := gen_split w_0 n h in modn1 (modn1 r hh) hl. + Definition double_modn1_0_aux n (modn1:w -> word w n -> w) r h := + let (hh,hl) := double_split w_0 n h in modn1 (modn1 r hh) hl. - Fixpoint gen_modn1_0 (n:nat) : w -> word w n -> w := + Fixpoint double_modn1_0 (n:nat) : w -> word w n -> w := match n return w -> word w n -> w with | O => fun r x => snd (w_div21 r x b2p) - | S n => gen_modn1_0_aux n (gen_modn1_0 n) + | S n => double_modn1_0_aux n (double_modn1_0 n) end. - Lemma spec_gen_modn1_0 : forall n r x, - gen_modn1_0 n r x = snd (gen_divn1_0 n r x). + Lemma spec_double_modn1_0 : forall n r x, + double_modn1_0 n r x = snd (double_divn1_0 n r x). Proof. induction n;simpl;intros;trivial. - unfold gen_modn1_0_aux, gen_divn1_0_aux. - destruct (gen_split w_0 n x) as (hh,hl). + unfold double_modn1_0_aux, double_divn1_0_aux. + destruct (double_split w_0 n x) as (hh,hl). rewrite (IHn r hh). - destruct (gen_divn1_0 n r hh) as (qh,rh);simpl. - rewrite IHn. destruct (gen_divn1_0 n rh hl);trivial. + destruct (double_divn1_0 n r hh) as (qh,rh);simpl. + rewrite IHn. destruct (double_divn1_0 n rh hl);trivial. Qed. Variable p : w. @@ -148,21 +148,21 @@ Section GENDIVN1. intros;apply spec_add_mul_div;auto. Qed. - Definition gen_divn1_p_aux n + Definition double_divn1_p_aux n (divn1 : w -> word w n -> word w n -> word w n * w) r h l := - let (hh,hl) := gen_split w_0 n h in - let (lh,ll) := gen_split w_0 n l in + let (hh,hl) := double_split w_0 n h in + let (lh,ll) := double_split w_0 n l in let (qh,rh) := divn1 r hh hl in let (ql,rl) := divn1 rh hl lh in - (gen_WW w_WW n qh ql, rl). + (double_WW w_WW n qh ql, rl). - Fixpoint gen_divn1_p (n:nat) : w -> word w n -> word w n -> word w n * w := + Fixpoint double_divn1_p (n:nat) : w -> word w n -> word w n -> word w n * w := match n return w -> word w n -> word w n -> word w n * w with | O => fun r h l => w_div21 r (w_add_mul_div p h l) b2p - | S n => gen_divn1_p_aux n (gen_divn1_p n) + | S n => double_divn1_p_aux n (double_divn1_p n) end. - Lemma p_lt_gen_digits : forall n, [|p|] <= Zpos (gen_digits w_digits n). + Lemma p_lt_double_digits : forall n, [|p|] <= Zpos (double_digits w_digits n). Proof. (* induction n;simpl. destruct p_bounded;trivial. @@ -172,130 +172,130 @@ Section GENDIVN1. case (spec_to_Z p); rewrite Zpos_xO;auto with zarith. Qed. - Lemma spec_gen_divn1_p : forall n r h l, + Lemma spec_double_divn1_p : forall n r h l, [|r|] < [|b2p|] -> - let (q,r') := gen_divn1_p n r h l in - [|r|] * gen_wB w_digits n + + let (q,r') := double_divn1_p n r h l in + [|r|] * double_wB w_digits n + ([!n|h!]*2^[|p|] + - [!n|l!] / (2^(Zpos(gen_digits w_digits n) - [|p|]))) - mod gen_wB w_digits n = [!n|q!] * [|b2p|] + [|r'|] /\ + [!n|l!] / (2^(Zpos(double_digits w_digits n) - [|p|]))) + mod double_wB w_digits n = [!n|q!] * [|b2p|] + [|r'|] /\ 0 <= [|r'|] < [|b2p|]. Proof. case (spec_to_Z p); intros HH0 HH1. induction n;intros. - simpl (gen_divn1_p 0 r h l). - unfold gen_to_Z, gen_wB, gen_digits. + simpl (double_divn1_p 0 r h l). + unfold double_to_Z, double_wB, double_digits. rewrite <- spec_add_mul_divp. exact (spec_div21 (w_add_mul_div p h l) b2p_le H). - simpl (gen_divn1_p (S n) r h l). - unfold gen_divn1_p_aux. - assert (H1 := spec_split n h);destruct (gen_split w_0 n h) as (hh,hl). - rewrite H1. rewrite <- gen_wB_wwB. - assert (H2 := spec_split n l);destruct (gen_split w_0 n l) as (lh,ll). + simpl (double_divn1_p (S n) r h l). + unfold double_divn1_p_aux. + assert (H1 := spec_split n h);destruct (double_split w_0 n h) as (hh,hl). + rewrite H1. rewrite <- double_wB_wwB. + assert (H2 := spec_split n l);destruct (double_split w_0 n l) as (lh,ll). rewrite H2. - replace ([|r|] * (gen_wB w_digits n * gen_wB w_digits n) + - (([!n|hh!] * gen_wB w_digits n + [!n|hl!]) * 2 ^ [|p|] + - ([!n|lh!] * gen_wB w_digits n + [!n|ll!]) / - 2^(Zpos (gen_digits w_digits (S n)) - [|p|])) mod - (gen_wB w_digits n * gen_wB w_digits n)) with - (([|r|] * gen_wB w_digits n + ([!n|hh!] * 2^[|p|] + - [!n|hl!] / 2^(Zpos (gen_digits w_digits n) - [|p|])) mod - gen_wB w_digits n) * gen_wB w_digits n + + replace ([|r|] * (double_wB w_digits n * double_wB w_digits n) + + (([!n|hh!] * double_wB w_digits n + [!n|hl!]) * 2 ^ [|p|] + + ([!n|lh!] * double_wB w_digits n + [!n|ll!]) / + 2^(Zpos (double_digits w_digits (S n)) - [|p|])) mod + (double_wB w_digits n * double_wB w_digits n)) with + (([|r|] * double_wB w_digits n + ([!n|hh!] * 2^[|p|] + + [!n|hl!] / 2^(Zpos (double_digits w_digits n) - [|p|])) mod + double_wB w_digits n) * double_wB w_digits n + ([!n|hl!] * 2^[|p|] + - [!n|lh!] / 2^(Zpos (gen_digits w_digits n) - [|p|])) mod - gen_wB w_digits n). - generalize (IHn r hh hl H);destruct (gen_divn1_p n r hh hl) as (qh,rh); + [!n|lh!] / 2^(Zpos (double_digits w_digits n) - [|p|])) mod + double_wB w_digits n). + generalize (IHn r hh hl H);destruct (double_divn1_p n r hh hl) as (qh,rh); intros (H3,H4);rewrite H3. assert ([|rh|] < [|b2p|]). omega. - replace (([!n|qh!] * [|b2p|] + [|rh|]) * gen_wB w_digits n + + replace (([!n|qh!] * [|b2p|] + [|rh|]) * double_wB w_digits n + ([!n|hl!] * 2 ^ [|p|] + - [!n|lh!] / 2 ^ (Zpos (gen_digits w_digits n) - [|p|])) mod - gen_wB w_digits n) with - ([!n|qh!] * [|b2p|] *gen_wB w_digits n + ([|rh|]*gen_wB w_digits n + + [!n|lh!] / 2 ^ (Zpos (double_digits w_digits n) - [|p|])) mod + double_wB w_digits n) with + ([!n|qh!] * [|b2p|] *double_wB w_digits n + ([|rh|]*double_wB w_digits n + ([!n|hl!] * 2 ^ [|p|] + - [!n|lh!] / 2 ^ (Zpos (gen_digits w_digits n) - [|p|])) mod - gen_wB w_digits n)). 2:ring. - generalize (IHn rh hl lh H0);destruct (gen_divn1_p n rh hl lh) as (ql,rl); + [!n|lh!] / 2 ^ (Zpos (double_digits w_digits n) - [|p|])) mod + double_wB w_digits n)). 2:ring. + generalize (IHn rh hl lh H0);destruct (double_divn1_p n rh hl lh) as (ql,rl); intros (H5,H6);rewrite H5. - split;[rewrite spec_gen_WW;trivial;ring|trivial]. - assert (Uhh := spec_gen_to_Z w_digits w_to_Z spec_to_Z n hh); - unfold gen_wB,base in Uhh. - assert (Uhl := spec_gen_to_Z w_digits w_to_Z spec_to_Z n hl); - unfold gen_wB,base in Uhl. - assert (Ulh := spec_gen_to_Z w_digits w_to_Z spec_to_Z n lh); - unfold gen_wB,base in Ulh. - assert (Ull := spec_gen_to_Z w_digits w_to_Z spec_to_Z n ll); - unfold gen_wB,base in Ull. - unfold gen_wB,base. - assert (UU:=p_lt_gen_digits n). + split;[rewrite spec_double_WW;trivial;ring|trivial]. + assert (Uhh := spec_double_to_Z w_digits w_to_Z spec_to_Z n hh); + unfold double_wB,base in Uhh. + assert (Uhl := spec_double_to_Z w_digits w_to_Z spec_to_Z n hl); + unfold double_wB,base in Uhl. + assert (Ulh := spec_double_to_Z w_digits w_to_Z spec_to_Z n lh); + unfold double_wB,base in Ulh. + assert (Ull := spec_double_to_Z w_digits w_to_Z spec_to_Z n ll); + unfold double_wB,base in Ull. + unfold double_wB,base. + assert (UU:=p_lt_double_digits n). rewrite Zdiv_shift_r;auto with zarith. - 2:change (Zpos (gen_digits w_digits (S n))) - with (2*Zpos (gen_digits w_digits n));auto with zarith. - replace (2 ^ (Zpos (gen_digits w_digits (S n)) - [|p|])) with - (2^(Zpos (gen_digits w_digits n) - [|p|])*2^Zpos (gen_digits w_digits n)). + 2:change (Zpos (double_digits w_digits (S n))) + with (2*Zpos (double_digits w_digits n));auto with zarith. + replace (2 ^ (Zpos (double_digits w_digits (S n)) - [|p|])) with + (2^(Zpos (double_digits w_digits n) - [|p|])*2^Zpos (double_digits w_digits n)). rewrite Zdiv_mult_cancel_r;auto with zarith. rewrite Zmult_plus_distr_l with (p:= 2^[|p|]). pattern ([!n|hl!] * 2^[|p|]) at 2; - rewrite (shift_unshift_mod (Zpos(gen_digits w_digits n))([|p|])([!n|hl!])); + rewrite (shift_unshift_mod (Zpos(double_digits w_digits n))([|p|])([!n|hl!])); auto with zarith. rewrite Zplus_assoc. replace - ([!n|hh!] * 2^Zpos (gen_digits w_digits n)* 2^[|p|] + - ([!n|hl!] / 2^(Zpos (gen_digits w_digits n)-[|p|])* - 2^Zpos(gen_digits w_digits n))) + ([!n|hh!] * 2^Zpos (double_digits w_digits n)* 2^[|p|] + + ([!n|hl!] / 2^(Zpos (double_digits w_digits n)-[|p|])* + 2^Zpos(double_digits w_digits n))) with - (([!n|hh!] *2^[|p|] + gen_to_Z w_digits w_to_Z n hl / - 2^(Zpos (gen_digits w_digits n)-[|p|])) - * 2^Zpos(gen_digits w_digits n));try (ring;fail). + (([!n|hh!] *2^[|p|] + double_to_Z w_digits w_to_Z n hl / + 2^(Zpos (double_digits w_digits n)-[|p|])) + * 2^Zpos(double_digits w_digits n));try (ring;fail). rewrite <- Zplus_assoc. rewrite <- (Zmod_shift_r ([|p|]));auto with zarith. replace - (2 ^ Zpos (gen_digits w_digits n) * 2 ^ Zpos (gen_digits w_digits n)) with - (2 ^ (Zpos (gen_digits w_digits n) + Zpos (gen_digits w_digits n))). - rewrite (Zmod_shift_r (Zpos (gen_digits w_digits n)));auto with zarith. - replace (2 ^ (Zpos (gen_digits w_digits n) + Zpos (gen_digits w_digits n))) - with (2^Zpos(gen_digits w_digits n) *2^Zpos(gen_digits w_digits n)). + (2 ^ Zpos (double_digits w_digits n) * 2 ^ Zpos (double_digits w_digits n)) with + (2 ^ (Zpos (double_digits w_digits n) + Zpos (double_digits w_digits n))). + rewrite (Zmod_shift_r (Zpos (double_digits w_digits n)));auto with zarith. + replace (2 ^ (Zpos (double_digits w_digits n) + Zpos (double_digits w_digits n))) + with (2^Zpos(double_digits w_digits n) *2^Zpos(double_digits w_digits n)). rewrite (Zmult_comm (([!n|hh!] * 2 ^ [|p|] + - [!n|hl!] / 2 ^ (Zpos (gen_digits w_digits n) - [|p|])))). + [!n|hl!] / 2 ^ (Zpos (double_digits w_digits n) - [|p|])))). rewrite Zmult_mod_distr_l;auto with zarith. ring. rewrite Zpower_exp;auto with zarith. - assert (0 < Zpos (gen_digits w_digits n)). unfold Zlt;reflexivity. + assert (0 < Zpos (double_digits w_digits n)). unfold Zlt;reflexivity. auto with zarith. apply Z_mod_lt;auto with zarith. rewrite Zpower_exp;auto with zarith. split;auto with zarith. apply Zdiv_lt_upper_bound;auto with zarith. rewrite <- Zpower_exp;auto with zarith. - replace ([|p|] + (Zpos (gen_digits w_digits n) - [|p|])) with - (Zpos(gen_digits w_digits n));auto with zarith. + replace ([|p|] + (Zpos (double_digits w_digits n) - [|p|])) with + (Zpos(double_digits w_digits n));auto with zarith. rewrite <- Zpower_exp;auto with zarith. - replace (Zpos (gen_digits w_digits (S n)) - [|p|]) with - (Zpos (gen_digits w_digits n) - [|p|] + - Zpos (gen_digits w_digits n));trivial. - change (Zpos (gen_digits w_digits (S n))) with - (2*Zpos (gen_digits w_digits n)). ring. + replace (Zpos (double_digits w_digits (S n)) - [|p|]) with + (Zpos (double_digits w_digits n) - [|p|] + + Zpos (double_digits w_digits n));trivial. + change (Zpos (double_digits w_digits (S n))) with + (2*Zpos (double_digits w_digits n)). ring. Qed. - Definition gen_modn1_p_aux n (modn1 : w -> word w n -> word w n -> w) r h l:= - let (hh,hl) := gen_split w_0 n h in - let (lh,ll) := gen_split w_0 n l in + Definition double_modn1_p_aux n (modn1 : w -> word w n -> word w n -> w) r h l:= + let (hh,hl) := double_split w_0 n h in + let (lh,ll) := double_split w_0 n l in modn1 (modn1 r hh hl) hl lh. - Fixpoint gen_modn1_p (n:nat) : w -> word w n -> word w n -> w := + Fixpoint double_modn1_p (n:nat) : w -> word w n -> word w n -> w := match n return w -> word w n -> word w n -> w with | O => fun r h l => snd (w_div21 r (w_add_mul_div p h l) b2p) - | S n => gen_modn1_p_aux n (gen_modn1_p n) + | S n => double_modn1_p_aux n (double_modn1_p n) end. - Lemma spec_gen_modn1_p : forall n r h l , - gen_modn1_p n r h l = snd (gen_divn1_p n r h l). + Lemma spec_double_modn1_p : forall n r h l , + double_modn1_p n r h l = snd (double_divn1_p n r h l). Proof. induction n;simpl;intros;trivial. - unfold gen_modn1_p_aux, gen_divn1_p_aux. - destruct(gen_split w_0 n h)as(hh,hl);destruct(gen_split w_0 n l) as (lh,ll). - rewrite (IHn r hh hl);destruct (gen_divn1_p n r hh hl) as (qh,rh). - rewrite IHn;simpl;destruct (gen_divn1_p n rh hl lh);trivial. + unfold double_modn1_p_aux, double_divn1_p_aux. + destruct(double_split w_0 n h)as(hh,hl);destruct(double_split w_0 n l) as (lh,ll). + rewrite (IHn r hh hl);destruct (double_divn1_p n r hh hl) as (qh,rh). + rewrite IHn;simpl;destruct (double_divn1_p n rh hl lh);trivial. Qed. End DIVAUX. @@ -311,46 +311,46 @@ Section GENDIVN1. end end. - Lemma spec_gen_digits:forall n, Zpos w_digits <= Zpos (gen_digits w_digits n). + Lemma spec_double_digits:forall n, Zpos w_digits <= Zpos (double_digits w_digits n). Proof. induction n;simpl;auto with zarith. - change (Zpos (xO (gen_digits w_digits n))) with - (2*Zpos (gen_digits w_digits n)). + change (Zpos (xO (double_digits w_digits n))) with + (2*Zpos (double_digits w_digits n)). assert (0 < Zpos w_digits);auto with zarith. exact (refl_equal Lt). Qed. Lemma spec_high : forall n (x:word w n), - [|high n x|] = [!n|x!] / 2^(Zpos (gen_digits w_digits n) - Zpos w_digits). + [|high n x|] = [!n|x!] / 2^(Zpos (double_digits w_digits n) - Zpos w_digits). Proof. induction n;intros. - unfold high,gen_digits,gen_to_Z. + unfold high,double_digits,double_to_Z. replace (Zpos w_digits - Zpos w_digits) with 0;try ring. simpl. rewrite <- (Zdiv_unique [|x|] 1 [|x|] 0);auto with zarith. - assert (U2 := spec_gen_digits n). + assert (U2 := spec_double_digits n). assert (U3 : 0 < Zpos w_digits). exact (refl_equal Lt). destruct x;unfold high;fold high. - unfold gen_to_Z,zn2z_to_Z;rewrite spec_0. + unfold double_to_Z,zn2z_to_Z;rewrite spec_0. rewrite Zdiv_0_l;trivial. - assert (U0 := spec_gen_to_Z w_digits w_to_Z spec_to_Z n w0); - assert (U1 := spec_gen_to_Z w_digits w_to_Z spec_to_Z n w1). + assert (U0 := spec_double_to_Z w_digits w_to_Z spec_to_Z n w0); + assert (U1 := spec_double_to_Z w_digits w_to_Z spec_to_Z n w1). simpl [!S n|WW w0 w1!]. - unfold gen_wB,base;rewrite Zdiv_shift_r;auto with zarith. - replace (2 ^ (Zpos (gen_digits w_digits (S n)) - Zpos w_digits)) with - (2^(Zpos (gen_digits w_digits n) - Zpos w_digits) * - 2^Zpos (gen_digits w_digits n)). + unfold double_wB,base;rewrite Zdiv_shift_r;auto with zarith. + replace (2 ^ (Zpos (double_digits w_digits (S n)) - Zpos w_digits)) with + (2^(Zpos (double_digits w_digits n) - Zpos w_digits) * + 2^Zpos (double_digits w_digits n)). rewrite Zdiv_mult_cancel_r;auto with zarith. rewrite <- Zpower_exp;auto with zarith. - replace (Zpos (gen_digits w_digits n) - Zpos w_digits + - Zpos (gen_digits w_digits n)) with - (Zpos (gen_digits w_digits (S n)) - Zpos w_digits);trivial. - change (Zpos (gen_digits w_digits (S n))) with - (2*Zpos (gen_digits w_digits n));ring. - change (Zpos (gen_digits w_digits (S n))) with - (2*Zpos (gen_digits w_digits n)); auto with zarith. + replace (Zpos (double_digits w_digits n) - Zpos w_digits + + Zpos (double_digits w_digits n)) with + (Zpos (double_digits w_digits (S n)) - Zpos w_digits);trivial. + change (Zpos (double_digits w_digits (S n))) with + (2*Zpos (double_digits w_digits n));ring. + change (Zpos (double_digits w_digits (S n))) with + (2*Zpos (double_digits w_digits n)); auto with zarith. Qed. - Definition gen_divn1 (n:nat) (a:word w n) (b:w) := + Definition double_divn1 (n:nat) (a:word w n) (b:w) := let p := w_head0 b in match w_compare p w_0 with | Gt => @@ -359,18 +359,18 @@ Section GENDIVN1. let k := w_sub w_zdigits p in let lsr_n := w_add_mul_div k w_0 in let r0 := w_add_mul_div p w_0 ha in - let (q,r) := gen_divn1_p b2p p n r0 a (gen_0 w_0 n) in + let (q,r) := double_divn1_p b2p p n r0 a (double_0 w_0 n) in (q, lsr_n r) - | _ => gen_divn1_0 b n w_0 a + | _ => double_divn1_0 b n w_0 a end. - Lemma spec_gen_divn1 : forall n a b, + Lemma spec_double_divn1 : forall n a b, 0 < [|b|] -> - let (q,r) := gen_divn1 n a b in + let (q,r) := double_divn1 n a b in [!n|a!] = [!n|q!] * [|b|] + [|r|] /\ 0 <= [|r|] < [|b|]. Proof. - intros n a b H. unfold gen_divn1. + 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; @@ -380,7 +380,7 @@ Section GENDIVN1. rewrite Zmult_1_l; auto. assert (Hv2: [|w_0|] < [|b|]). rewrite spec_0; auto. - generalize (spec_gen_divn1_0 Hv1 n a Hv2). + generalize (spec_double_divn1_0 Hv1 n a Hv2). rewrite spec_0;rewrite Zmult_0_l; rewrite Zplus_0_l; auto. contradict H2; auto with zarith. assert (HHHH : 0 < [|w_head0 b|]); auto with zarith. @@ -422,30 +422,30 @@ Section GENDIVN1. apply Zpower_le_monotone;split;auto with zarith. rewrite <- H4 in H0. assert (Hb3: [|w_head0 b|] <= Zpos w_digits); auto with zarith. - assert (H7:= spec_gen_divn1_p H0 Hb3 n a (gen_0 w_0 n) H6). - destruct (gen_divn1_p (w_add_mul_div (w_head0 b) b w_0) (w_head0 b) n + assert (H7:= spec_double_divn1_p H0 Hb3 n a (double_0 w_0 n) H6). + destruct (double_divn1_p (w_add_mul_div (w_head0 b) b w_0) (w_head0 b) n (w_add_mul_div (w_head0 b) w_0 (high n a)) a - (gen_0 w_0 n)) as (q,r). - assert (U:= spec_gen_digits n). - rewrite spec_gen_0 in H7;trivial;rewrite Zdiv_0_l in H7. + (double_0 w_0 n)) as (q,r). + assert (U:= spec_double_digits n). + rewrite spec_double_0 in H7;trivial;rewrite Zdiv_0_l in H7. rewrite Zplus_0_r in H7. rewrite spec_add_mul_div in H7;auto with zarith. rewrite spec_0 in H7;rewrite Zmult_0_l in H7;rewrite Zplus_0_l in H7. assert (([|high n a|] / 2 ^ (Zpos w_digits - [|w_head0 b|])) mod wB - = [!n|a!] / 2^(Zpos (gen_digits w_digits n) - [|w_head0 b|])). + = [!n|a!] / 2^(Zpos (double_digits w_digits n) - [|w_head0 b|])). rewrite Zmod_small;auto with zarith. rewrite spec_high. rewrite Zdiv_Zdiv;auto with zarith. rewrite <- Zpower_exp;auto with zarith. - replace (Zpos (gen_digits w_digits n) - Zpos w_digits + + replace (Zpos (double_digits w_digits n) - Zpos w_digits + (Zpos w_digits - [|w_head0 b|])) - with (Zpos (gen_digits w_digits n) - [|w_head0 b|]);trivial;ring. + with (Zpos (double_digits w_digits n) - [|w_head0 b|]);trivial;ring. assert (H8 := Zpower_gt_0 2 (Zpos w_digits - [|w_head0 b|]));auto with zarith. split;auto with zarith. apply Zle_lt_trans with ([|high n a|]);auto with zarith. apply Zdiv_le_upper_bound;auto with zarith. pattern ([|high n a|]) at 1;rewrite <- Zmult_1_r. apply Zmult_le_compat;auto with zarith. - rewrite H8 in H7;unfold gen_wB,base in H7. + rewrite H8 in H7;unfold double_wB,base in H7. rewrite <- shift_unshift_mod in H7;auto with zarith. rewrite H4 in H7. assert ([|w_add_mul_div (w_sub w_zdigits (w_head0 b)) w_0 r|] @@ -484,11 +484,11 @@ Section GENDIVN1. rewrite H9. apply Zdiv_lt_upper_bound;auto with zarith. rewrite Zmult_comm;auto with zarith. - exact (spec_gen_to_Z w_digits w_to_Z spec_to_Z n a). + exact (spec_double_to_Z w_digits w_to_Z spec_to_Z n a). Qed. - Definition gen_modn1 (n:nat) (a:word w n) (b:w) := + Definition double_modn1 (n:nat) (a:word w n) (b:w) := let p := w_head0 b in match w_compare p w_0 with | Gt => @@ -497,31 +497,31 @@ Section GENDIVN1. let k := w_sub w_zdigits p in let lsr_n := w_add_mul_div k w_0 in let r0 := w_add_mul_div p w_0 ha in - let r := gen_modn1_p b2p p n r0 a (gen_0 w_0 n) in + let r := double_modn1_p b2p p n r0 a (double_0 w_0 n) in lsr_n r - | _ => gen_modn1_0 b n w_0 a + | _ => double_modn1_0 b n w_0 a end. - Lemma spec_gen_modn1_aux : forall n a b, - gen_modn1 n a b = snd (gen_divn1 n a b). + Lemma spec_double_modn1_aux : forall n a b, + double_modn1 n a b = snd (double_divn1 n a b). Proof. - intros n a b;unfold gen_divn1,gen_modn1. + intros n a b;unfold double_divn1,double_modn1. generalize (spec_compare (w_head0 b) w_0); case w_compare; rewrite spec_0; intros H2; auto with zarith. - apply spec_gen_modn1_0. - apply spec_gen_modn1_0. - rewrite spec_gen_modn1_p. - destruct (gen_divn1_p (w_add_mul_div (w_head0 b) b w_0) (w_head0 b) n - (w_add_mul_div (w_head0 b) w_0 (high n a)) a (gen_0 w_0 n));simpl;trivial. + apply spec_double_modn1_0. + apply spec_double_modn1_0. + rewrite spec_double_modn1_p. + destruct (double_divn1_p (w_add_mul_div (w_head0 b) b w_0) (w_head0 b) n + (w_add_mul_div (w_head0 b) w_0 (high n a)) a (double_0 w_0 n));simpl;trivial. Qed. - Lemma spec_gen_modn1 : forall n a b, 0 < [|b|] -> - [|gen_modn1 n a b|] = [!n|a!] mod [|b|]. + Lemma spec_double_modn1 : forall n a b, 0 < [|b|] -> + [|double_modn1 n a b|] = [!n|a!] mod [|b|]. Proof. - intros n a b H;assert (H1 := spec_gen_divn1 n a H). - assert (H2 := spec_gen_modn1_aux n a b). - rewrite H2;destruct (gen_divn1 n a b) as (q,r). - simpl;apply Zmod_unique with (gen_to_Z w_digits w_to_Z n q);auto with zarith. + intros n a b H;assert (H1 := spec_double_divn1 n a H). + assert (H2 := spec_double_modn1_aux n a b). + rewrite H2;destruct (double_divn1 n a b) as (q,r). + simpl;apply Zmod_unique with (double_to_Z w_digits w_to_Z n q);auto with zarith. destruct H1 as (h1,h2);rewrite h1;ring. Qed. diff --git a/theories/Numbers/Cyclic/DoubleCyclic/GenLift.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.v index 6cc1ecad3..08f46aecd 100644 --- a/theories/Numbers/Cyclic/DoubleCyclic/GenLift.v +++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.v @@ -14,12 +14,12 @@ Set Implicit Arguments. Require Import ZArith. Require Import BigNumPrelude. -Require Import Basic_type. -Require Import GenBase. +Require Import DoubleType. +Require Import DoubleBase. Open Local Scope Z_scope. -Section GenLift. +Section DoubleLift. Variable w : Set. Variable w_0 : w. Variable w_WW : w -> w -> zn2z w. @@ -91,7 +91,7 @@ Section GenLift. end end. - Section GenProof. + Section DoubleProof. Variable w_to_Z : w -> Z. Notation wB := (base w_digits). @@ -481,7 +481,7 @@ Section GenLift. case (spec_to_Z xh); auto with zarith. Qed. - End GenProof. + End DoubleProof. -End GenLift. +End DoubleLift. diff --git a/theories/Numbers/Cyclic/DoubleCyclic/GenMul.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.v index f42946d6f..bc2508972 100644 --- a/theories/Numbers/Cyclic/DoubleCyclic/GenMul.v +++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.v @@ -14,12 +14,12 @@ Set Implicit Arguments. Require Import ZArith. Require Import BigNumPrelude. -Require Import Basic_type. -Require Import GenBase. +Require Import DoubleType. +Require Import DoubleBase. Open Local Scope Z_scope. -Section GenMul. +Section DoubleMul. Variable w : Set. Variable w_0 : w. Variable w_1 : w. @@ -48,7 +48,7 @@ Section GenMul. xl*yl = ll = |llh|lll *) - Definition gen_mul_c (cross:w->w->w->w->zn2z w -> zn2z w -> w*zn2z w) x y := + Definition double_mul_c (cross:w->w->w->w->zn2z w -> zn2z w -> w*zn2z w) x y := match x, y with | W0, _ => W0 | _, W0 => W0 @@ -67,7 +67,7 @@ Section GenMul. end. Definition ww_mul_c := - gen_mul_c + double_mul_c (fun xh xl yh yl hh ll=> match ww_add_c (w_mul_c xh yl) (w_mul_c xl yh) with | C0 cc => (w_0, cc) @@ -124,7 +124,7 @@ Section GenMul. end end. - Definition ww_karatsuba_c := gen_mul_c kara_prod. + Definition ww_karatsuba_c := double_mul_c kara_prod. Definition ww_mul x y := match x, y with @@ -157,49 +157,49 @@ Section GenMul. end end. - Section GenMulAddn1. + Section DoubleMulAddn1. Variable w_mul_add : w -> w -> w -> w * w. - Fixpoint gen_mul_add_n1 (n:nat) : word w n -> w -> w -> w * word w n := + Fixpoint double_mul_add_n1 (n:nat) : word w n -> w -> w -> w * word w n := match n return word w n -> w -> w -> w * word w n with | O => w_mul_add | S n1 => - let mul_add := gen_mul_add_n1 n1 in + let mul_add := double_mul_add_n1 n1 in fun x y r => match x with | W0 => (w_0,extend w_0W n1 r) | WW xh xl => let (rl,l) := mul_add xl y r in let (rh,h) := mul_add xh y rl in - (rh, gen_WW w_WW n1 h l) + (rh, double_WW w_WW n1 h l) end end. - End GenMulAddn1. + End DoubleMulAddn1. - Section GenMulAddmn1. + Section DoubleMulAddmn1. Variable wn: Set. Variable extend_n : w -> wn. Variable wn_0W : wn -> zn2z wn. Variable wn_WW : wn -> wn -> zn2z wn. Variable w_mul_add_n1 : wn -> w -> w -> w*wn. - Fixpoint gen_mul_add_mn1 (m:nat) : + Fixpoint double_mul_add_mn1 (m:nat) : word wn m -> w -> w -> w*word wn m := match m return word wn m -> w -> w -> w*word wn m with | O => w_mul_add_n1 | S m1 => - let mul_add := gen_mul_add_mn1 m1 in + let mul_add := double_mul_add_mn1 m1 in fun x y r => match x with | W0 => (w_0,extend wn_0W m1 (extend_n r)) | WW xh xl => let (rl,l) := mul_add xl y r in let (rh,h) := mul_add xh y rl in - (rh, gen_WW wn_WW m1 h l) + (rh, double_WW wn_WW m1 h l) end end. - End GenMulAddmn1. + End DoubleMulAddmn1. Definition w_mul_add x y r := match w_mul_c x y with @@ -212,7 +212,7 @@ Section GenMul. end. - (*Section GenProof. *) + (*Section DoubleProof. *) Variable w_digits : positive. Variable w_to_Z : w -> Z. @@ -235,7 +235,7 @@ Section GenMul. Notation "[|| x ||]" := (zn2z_to_Z wwB (ww_to_Z w_digits w_to_Z) x) (at level 0, x at level 99). - Notation "[! n | x !]" := (gen_to_Z w_digits w_to_Z n x) + Notation "[! n | x !]" := (double_to_Z w_digits w_to_Z n x) (at level 0, x at level 99). Variable spec_more_than_1_digit: 1 < Zpos w_digits. @@ -359,13 +359,13 @@ Section GenMul. repeat rewrite <- Zplus_assoc;rewrite H;apply mult_add_ineq2;zarith. Qed. - Lemma spec_gen_mul_c : forall cross:w->w->w->w->zn2z w -> zn2z w -> w*zn2z w, + Lemma spec_double_mul_c : forall cross:w->w->w->w->zn2z w -> zn2z w -> w*zn2z w, (forall xh xl yh yl hh ll, [[hh]] = [|xh|]*[|yh|] -> [[ll]] = [|xl|]*[|yl|] -> let (wc,cc) := cross xh xl yh yl hh ll in [|wc|]*wwB + [[cc]] = [|xh|]*[|yl|] + [|xl|]*[|yh|]) -> - forall x y, [||gen_mul_c cross x y||] = [[x]] * [[y]]. + forall x y, [||double_mul_c cross x y||] = [[x]] * [[y]]. Proof. intros cross Hcross x y;destruct x as [ |xh xl];simpl;trivial. destruct y as [ |yh yl];simpl. rewrite Zmult_0_r;trivial. @@ -378,7 +378,7 @@ Section GenMul. Lemma spec_ww_mul_c : forall x y, [||ww_mul_c x y||] = [[x]] * [[y]]. Proof. - intros x y;unfold ww_mul_c;apply spec_gen_mul_c. + intros x y;unfold ww_mul_c;apply spec_double_mul_c. intros xh xl yh yl hh ll H1 H2. generalize (spec_ww_add_c (w_mul_c xh yl) (w_mul_c xl yh)); destruct (ww_add_c (w_mul_c xh yl) (w_mul_c xl yh)) as [c|c]; @@ -534,7 +534,7 @@ Section GenMul. Lemma spec_ww_karatsuba_c : forall x y, [||ww_karatsuba_c x y||]=[[x]]*[[y]]. Proof. - intros x y; unfold ww_karatsuba_c;apply spec_gen_mul_c. + intros x y; unfold ww_karatsuba_c;apply spec_double_mul_c. intros; apply spec_kara_prod; auto. Qed. @@ -577,31 +577,31 @@ Section GenMul. rewrite spec_w_1;rewrite Zmult_1_l;rewrite <- wwB_wBwB;trivial. Qed. - Section GenMulAddn1Proof. + Section DoubleMulAddn1Proof. Variable w_mul_add : w -> w -> w -> w * w. Variable spec_w_mul_add : forall x y r, let (h,l):= w_mul_add x y r in [|h|]*wB+[|l|] = [|x|]*[|y|] + [|r|]. - Lemma spec_gen_mul_add_n1 : forall n x y r, - let (h,l) := gen_mul_add_n1 w_mul_add n x y r in - [|h|]*gen_wB w_digits n + [!n|l!] = [!n|x!]*[|y|]+[|r|]. + Lemma spec_double_mul_add_n1 : forall n x y r, + let (h,l) := double_mul_add_n1 w_mul_add n x y r in + [|h|]*double_wB w_digits n + [!n|l!] = [!n|x!]*[|y|]+[|r|]. Proof. induction n;intros x y r;trivial. exact (spec_w_mul_add x y r). - unfold gen_mul_add_n1;destruct x as[ |xh xl]; - fold(gen_mul_add_n1 w_mul_add). + unfold double_mul_add_n1;destruct x as[ |xh xl]; + fold(double_mul_add_n1 w_mul_add). rewrite spec_w_0;rewrite spec_extend;simpl;trivial. - assert(H:=IHn xl y r);destruct (gen_mul_add_n1 w_mul_add n xl y r)as(rl,l). - assert(U:=IHn xh y rl);destruct(gen_mul_add_n1 w_mul_add n xh y rl)as(rh,h). - rewrite <- gen_wB_wwB. rewrite spec_gen_WW;simpl;trivial. + assert(H:=IHn xl y r);destruct (double_mul_add_n1 w_mul_add n xl y r)as(rl,l). + assert(U:=IHn xh y rl);destruct(double_mul_add_n1 w_mul_add n xh y rl)as(rh,h). + rewrite <- double_wB_wwB. rewrite spec_double_WW;simpl;trivial. rewrite Zmult_plus_distr_l;rewrite <- Zplus_assoc;rewrite <- H. rewrite Zmult_assoc;rewrite Zplus_assoc;rewrite <- Zmult_plus_distr_l. rewrite U;ring. Qed. - End GenMulAddn1Proof. + End DoubleMulAddn1Proof. Lemma spec_w_mul_add : forall x y r, let (h,l):= w_mul_add x y r in @@ -623,6 +623,6 @@ Section GenMul. assert (H1 := beta_lex _ _ _ _ _ H0 (spec_to_Z l));zarith. Qed. -(* End GenProof. *) +(* End DoubleProof. *) -End GenMul. +End DoubleMul. diff --git a/theories/Numbers/Cyclic/DoubleCyclic/GenSqrt.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v index ce312aa62..01dd3055f 100644 --- a/theories/Numbers/Cyclic/DoubleCyclic/GenSqrt.v +++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v @@ -14,12 +14,12 @@ Set Implicit Arguments. Require Import ZArith. Require Import BigNumPrelude. -Require Import Basic_type. -Require Import GenBase. +Require Import DoubleType. +Require Import DoubleBase. Open Local Scope Z_scope. -Section GenSqrt. +Section DoubleSqrt. Variable w : Set. Variable w_is_even : w -> bool. Variable w_compare : w -> w -> comparison. @@ -202,7 +202,7 @@ Section GenSqrt. Notation "[|| x ||]" := (zn2z_to_Z wwB (ww_to_Z w_digits w_to_Z) x) (at level 0, x at level 99). - Notation "[! n | x !]" := (gen_to_Z w_digits w_to_Z n x) + Notation "[! n | x !]" := (double_to_Z w_digits w_to_Z n x) (at level 0, x at level 99). Variable spec_w_0 : [|w_0|] = 0. @@ -1386,4 +1386,4 @@ intros x; case x; simpl ww_is_even. unfold base; apply Zpower2_lt_lin; auto with zarith. Qed. -End GenSqrt. +End DoubleSqrt. diff --git a/theories/Numbers/Cyclic/DoubleCyclic/GenSub.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.v index 3babd7716..9dbfbb497 100644 --- a/theories/Numbers/Cyclic/DoubleCyclic/GenSub.v +++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.v @@ -14,12 +14,12 @@ Set Implicit Arguments. Require Import ZArith. Require Import BigNumPrelude. -Require Import Basic_type. -Require Import GenBase. +Require Import DoubleType. +Require Import DoubleBase. Open Local Scope Z_scope. -Section GenSub. +Section DoubleSub. Variable w : Set. Variable w_0 : w. Variable w_Bm1 : w. @@ -152,7 +152,7 @@ Section GenSub. end end. - (*Section GenProof.*) + (*Section DoubleProof.*) Variable w_digits : positive. Variable w_to_Z : w -> Z. @@ -347,9 +347,9 @@ Section GenSub. rewrite (mod_wwB w_digits w_to_Z spec_to_Z);rewrite spec_sub_carry;trivial. Qed. -(* End GenProof. *) +(* End DoubleProof. *) -End GenSub. +End DoubleSub. diff --git a/theories/Numbers/Cyclic/DoubleCyclic/Basic_type.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v index 95f3c88e6..95f3c88e6 100644 --- a/theories/Numbers/Cyclic/DoubleCyclic/Basic_type.v +++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v diff --git a/theories/Numbers/Cyclic/DoubleCyclic/Zn2Z.v b/theories/Numbers/Cyclic/DoubleCyclic/Z_2nZ.v index a70f3c8ec..26d2393f9 100644 --- a/theories/Numbers/Cyclic/DoubleCyclic/Zn2Z.v +++ b/theories/Numbers/Cyclic/DoubleCyclic/Z_2nZ.v @@ -14,22 +14,22 @@ Set Implicit Arguments. Require Import ZArith. Require Import BigNumPrelude. -Require Import Basic_type. -Require Import GenBase. -Require Import GenAdd. -Require Import GenSub. -Require Import GenMul. -Require Import GenSqrt. -Require Import GenLift. -Require Import GenDivn1. -Require Import GenDiv. -Require Import ZnZ. +Require Import DoubleType. +Require Import DoubleBase. +Require Import DoubleAdd. +Require Import DoubleSub. +Require Import DoubleMul. +Require Import DoubleSqrt. +Require Import DoubleLift. +Require Import DoubleDivn1. +Require Import DoubleDiv. +Require Import Z_nZ. Open Local Scope Z_scope. -Section Zn2Z. - +Section Z_2nZ. + Variable w : Set. Variable w_op : znz_op w. Let w_digits := w_op.(znz_digits). @@ -200,11 +200,11 @@ Section Zn2Z. (* ** Multiplication ** *) Let mul_c := - Eval lazy beta iota delta [ww_mul_c gen_mul_c] in + 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 gen_mul_c kara_prod] in + 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. @@ -885,7 +885,8 @@ refine rewrite (spec_zdigits op_spec). rewrite <- Zpos_xO; exact spec_ww_digits. Qed. -End Zn2Z. + +End Z_2nZ. Section MulAdd. diff --git a/theories/Numbers/Cyclic/Int31/Int31.v b/theories/Numbers/Cyclic/Int31/Int31.v index 5cd504a34..e5b5f0d86 100644 --- a/theories/Numbers/Cyclic/Int31/Int31.v +++ b/theories/Numbers/Cyclic/Int31/Int31.v @@ -12,7 +12,7 @@ (* Require Import Notations.*) Require Export ZArith. -Require Export Basic_type. +Require Export DoubleType. Unset Boxed Definitions. diff --git a/theories/Numbers/Cyclic/Int31/Z31Z.v b/theories/Numbers/Cyclic/Int31/Z_31Z.v index 1a0046f8f..3b5944ed3 100644 --- a/theories/Numbers/Cyclic/Int31/Z31Z.v +++ b/theories/Numbers/Cyclic/Int31/Z_31Z.v @@ -15,7 +15,7 @@ Author: Arnaud Spiwack *) Require Export Int31. -Require Import ZnZ. +Require Import Z_nZ. Open Scope int31_scope. diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v index db4cd8965..25a39aeba 100644 --- a/theories/Numbers/Natural/BigN/BigN.v +++ b/theories/Numbers/Natural/BigN/BigN.v @@ -15,9 +15,9 @@ Author: Arnaud Spiwack *) Require Export Int31. -Require Import Z31Z. +Require Import Z_nZ. +Require Import Z_31Z. Require Import NMake. -Require Import ZnZ. Open Scope int31_scope. diff --git a/theories/Numbers/Natural/BigN/NMake_gen.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml index 48e116564..3d098c755 100644 --- a/theories/Numbers/Natural/BigN/NMake_gen.ml +++ b/theories/Numbers/Natural/BigN/NMake_gen.ml @@ -71,12 +71,12 @@ let _ = pr ""; pr "Require Import BigNumPrelude."; pr "Require Import ZArith."; - pr "Require Import Basic_type."; - pr "Require Import ZnZ."; - pr "Require Import Zn2Z."; + 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 Nbasic."; - pr "Require Import GenMul."; - pr "Require Import GenDivn1."; pr "Require Import Wf_nat."; pr "Require Import StreamMemo."; pr ""; @@ -187,30 +187,30 @@ let _ = pp " Let nmake_op%i := nmake_op _ w%i_op." i i; pp " Let eval%in n := znz_to_Z (nmake_op%i n)." i i; if i == 0 then - pr " Let extend%i := GenBase.extend (WW w_0)." i + pr " Let extend%i := DoubleBase.extend (WW w_0)." i else - pr " Let extend%i := GenBase.extend (WW (W0: w%i))." i i; + pr " Let extend%i := DoubleBase.extend (WW (W0: w%i))." i i; done; pr ""; - pp " Theorem digits_gend:forall n ww (w_op: znz_op ww), "; + pp " Theorem digits_doubled:forall n ww (w_op: znz_op ww), "; pp " znz_digits (nmake_op _ w_op n) = "; - pp " GenBase.gen_digits (znz_digits w_op) n."; + pp " DoubleBase.double_digits (znz_digits w_op) n."; pp " Proof."; pp " intros n; elim n; auto; clear n."; - pp " intros n Hrec ww ww_op; simpl GenBase.gen_digits."; + pp " intros n Hrec ww ww_op; simpl DoubleBase.double_digits."; pp " rewrite <- Hrec; auto."; pp " Qed."; pp ""; - pp " Theorem nmake_gen: forall n ww (w_op: znz_op ww), "; + pp " Theorem nmake_double: forall n ww (w_op: znz_op ww), "; pp " znz_to_Z (nmake_op _ w_op n) ="; - pp " @GenBase.gen_to_Z _ (znz_digits w_op) (znz_to_Z w_op) n."; + pp " @DoubleBase.double_to_Z _ (znz_digits w_op) (znz_to_Z w_op) n."; pp " Proof."; pp " intros n; elim n; auto; clear n."; - pp " intros n Hrec ww ww_op; simpl GenBase.gen_to_Z; unfold zn2z_to_Z."; + pp " intros n Hrec ww ww_op; simpl DoubleBase.double_to_Z; unfold zn2z_to_Z."; pp " rewrite <- Hrec; auto."; - pp " unfold GenBase.gen_wB; rewrite <- digits_gend; auto."; + pp " unfold DoubleBase.double_wB; rewrite <- digits_doubled; auto."; pp " Qed."; pp ""; @@ -311,9 +311,9 @@ let _ = pp " rewrite digits_nmake; rewrite <- digits_w%i; auto." (i - 1); pp " Qed."; pp ""; - pp " Let spec_gen_eval%in: forall n, eval%in n = GenBase.gen_to_Z (znz_digits w%i_op) (znz_to_Z w%i_op) n." i i i i; + pp " Let spec_double_eval%in: forall n, eval%in n = DoubleBase.double_to_Z (znz_digits w%i_op) (znz_to_Z w%i_op) n." i i i i; pp " Proof."; - pp " intros n; exact (nmake_gen n w%i w%i_op)." i i; + pp " intros n; exact (nmake_double n w%i w%i_op)." i i; pp " Qed."; pp ""; done; @@ -344,7 +344,7 @@ let _ = pp " Let spec_eval%in%i: forall x, [%s%i x] = eval%in %i x." i j c (i + j) i j; pp " Proof."; if j == 0 then - pp " intros x; rewrite spec_gen_eval%in; unfold GenBase.gen_to_Z, to_Z; auto." i + pp " intros x; rewrite spec_double_eval%in; unfold DoubleBase.double_to_Z, to_Z; auto." i else begin pp " intros x; case x."; @@ -561,7 +561,7 @@ let _ = pr0 "extend%i " i; done; pr ""; - pr " GenBase.extend GenBase.extend_aux"; + pr " DoubleBase.extend DoubleBase.extend_aux"; pr " ] in"; pr " match x, y with"; for i = 0 to size do @@ -629,7 +629,7 @@ let _ = pr0 "extend%i " i; done; pr ""; - pr " GenBase.extend GenBase.extend_aux"; + pr " DoubleBase.extend DoubleBase.extend_aux"; pr " ] in"; pr " match x with"; for i = 0 to size do @@ -731,7 +731,7 @@ let _ = pr0 "extend%i " i; done; pr ""; - pr " GenBase.extend GenBase.extend_aux"; + pr " DoubleBase.extend DoubleBase.extend_aux"; pr " ] in"; pr " match x, y with"; for i = 0 to size do @@ -796,7 +796,7 @@ let _ = pr0 "extend%i " i; done; pr ""; - pr " GenBase.extend GenBase.extend_aux"; + pr " DoubleBase.extend DoubleBase.extend_aux"; pr " ] in"; pr " match x with"; for i = 0 to size do @@ -1335,7 +1335,7 @@ let _ = pp " | Gt => eval%in n x > [%s%i y]" i c i; pp " end."; pp " intros n x y."; - pp " unfold comparen_%i, to_Z; rewrite spec_gen_eval%in." i i; + pp " unfold comparen_%i, to_Z; rewrite spec_double_eval%in." i i; pp " apply spec_compare_mn_1."; pp " exact (spec_0 w%i_spec)." i; pp " intros x1; exact (spec_compare w%i_spec %s x1)." i (pz i); @@ -1436,7 +1436,7 @@ let _ = for i = 0 to size do pr " Definition w%i_mul_add_n1 :=" i; - pr " @gen_mul_add_n1 w%i %s w%i_op.(znz_WW) w%i_0W w%i_mul_add." i (pz i) i i i + pr " @double_mul_add_n1 w%i %s w%i_op.(znz_WW) w%i_0W w%i_mul_add." i (pz i) i i i done; pr ""; @@ -1528,11 +1528,11 @@ let _ = pp " znz_to_Z w%i_op z." i; pp " Proof."; pp " intros n x y z; unfold w%i_mul_add_n1." i; - pp " rewrite nmake_gen."; - pp " rewrite digits_gend."; - pp " change (base (GenBase.gen_digits (znz_digits w%i_op) n)) with" i; - pp " (GenBase.gen_wB (znz_digits w%i_op) n)." i; - pp " apply spec_gen_mul_add_n1; auto."; + pp " rewrite nmake_double."; + pp " rewrite digits_doubled."; + pp " change (base (DoubleBase.double_digits (znz_digits w%i_op) n)) with" i; + pp " (DoubleBase.double_wB (znz_digits w%i_op) n)." i; + pp " apply spec_double_mul_add_n1; auto."; if i == 0 then pp " exact (spec_0 w%i_spec)." i; pp " exact (spec_WW w%i_spec)." i; pp " exact (spec_0W w%i_spec)." i; @@ -1554,9 +1554,9 @@ let _ = pp " znz_to_Z (nmake_op _ w%i_op (S n)) (extend%i n x1) = " i i; pp " znz_to_Z w%i_op x1." i; pp " Proof."; - pp " intros n1 x2; rewrite nmake_gen."; + pp " intros n1 x2; rewrite nmake_double."; pp " unfold extend%i." i; - pp " rewrite GenBase.spec_extend; auto."; + pp " rewrite DoubleBase.spec_extend; auto."; if i == 0 then pp " intros l; simpl; unfold w_0; rewrite (spec_0 w0_spec); ring."; pp " Qed."; @@ -1767,7 +1767,7 @@ let _ = pr ""; pp " Let spec_divn1 ww (ww_op: znz_op ww) (ww_spec: znz_spec ww_op) := "; - pp " (spec_gen_divn1 "; + pp " (spec_double_divn1 "; pp " ww_op.(znz_zdigits) ww_op.(znz_0)"; pp " ww_op.(znz_WW) ww_op.(znz_head0)"; pp " ww_op.(znz_add_mul_div) ww_op.(znz_div21)"; @@ -1776,13 +1776,13 @@ 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 " (ZnZ.spec_compare ww_spec) (ZnZ.spec_sub ww_spec))."; + pp " (Z_nZ.spec_compare ww_spec) (Z_nZ.spec_sub ww_spec))."; pp ""; for i = 0 to size do pr " Definition w%i_divn1 n x y :=" i; pr " let (u, v) :="; - pr " gen_divn1 w%i_op.(znz_zdigits) w%i_op.(znz_0)" i i; + pr " double_divn1 w%i_op.(znz_zdigits) w%i_op.(znz_0)" i i; pr " w%i_op.(znz_WW) w%i_op.(znz_head0)" i i; pr " w%i_op.(znz_add_mul_div) w%i_op.(znz_div21)" i i; pr " w%i_op.(znz_compare) w%i_op.(znz_sub) (S n) x y in" i i; @@ -1796,15 +1796,15 @@ let _ = for i = 0 to size do pp " Lemma spec_get_end%i: forall n x y," i; pp " eval%in n x <= [%s%i y] -> " i c i; - pp " [%s%i (GenBase.get_low %s n x)] = eval%in n x." c i (pz i) i; + pp " [%s%i (DoubleBase.get_low %s n x)] = eval%in n x." c i (pz i) i; pp " Proof."; pp " intros n x y H."; - pp " rewrite spec_gen_eval%in; unfold to_Z." i; - pp " apply GenBase.spec_get_low."; + pp " rewrite spec_double_eval%in; unfold to_Z." i; + pp " apply DoubleBase.spec_get_low."; pp " exact (spec_0 w%i_spec)." i; pp " exact (spec_to_Z w%i_spec)." i; pp " apply Zle_lt_trans with [%s%i y]; auto." c i; - pp " rewrite <- spec_gen_eval%in; auto." i; + pp " rewrite <- spec_double_eval%in; auto." i; pp " unfold to_Z; case (spec_to_Z w%i_spec y); auto." i; pp " Qed."; pp ""; @@ -1830,7 +1830,7 @@ let _ = pr " (iter _ "; for i = 0 to size do pr " div_gt%i" i; - pr " (fun n x y => div_gt%i x (GenBase.get_low %s (S n) y))" i (pz i); + pr " (fun n x y => div_gt%i x (DoubleBase.get_low %s (S n) y))" i (pz i); pr " w%i_divn1" i; done; pr " div_gtnm)."; @@ -1851,7 +1851,7 @@ let _ = pp " x = [q] * y + [r] /\\ 0 <= [r] < y)"; for i = 0 to size do pp " div_gt%i" i; - pp " (fun n x y => div_gt%i x (GenBase.get_low %s (S n) y))" i (pz i); + pp " (fun n x y => div_gt%i x (DoubleBase.get_low %s (S n) y))" i (pz i); pp " w%i_divn1 _ _ _" i; done; pp " div_gtnm _)."; @@ -1864,7 +1864,7 @@ let _ = else pp " intros n x y H1 H2 H3; unfold div_gt%i, w%i_div_gt." i i; pp " generalize (spec_div_gt w%i_spec x " i; - pp " (GenBase.get_low %s (S n) y))." (pz i); + pp " (DoubleBase.get_low %s (S n) y))." (pz i); pp0 " "; for j = 0 to i do pp0 "unfold w%i; " (i-j); @@ -1883,17 +1883,17 @@ let _ = for j = 0 to i do pp0 "unfold w%i; " (i-j); done; - pp "case gen_divn1."; + pp "case double_divn1."; pp " intros xx yy H4."; if i == size then begin - pp " repeat rewrite <- spec_gen_eval%in in H4; auto." i; + pp " repeat rewrite <- spec_double_eval%in in H4; auto." i; pp " rewrite spec_eval%in; auto." i; end else begin pp " rewrite to_Z%i_spec; auto with zarith." i; - pp " repeat rewrite <- spec_gen_eval%in in H4; auto." i; + pp " repeat rewrite <- spec_double_eval%in in H4; auto." i; end; done; pp " intros n m x y H1 H2; unfold div_gtnm."; @@ -1983,7 +1983,7 @@ let _ = for i = 0 to size do pr " Definition w%i_modn1 :=" i; - pr " gen_modn1 w%i_op.(znz_zdigits) w%i_op.(znz_0)" i i; + pr " double_modn1 w%i_op.(znz_zdigits) w%i_op.(znz_0)" i i; pr " w%i_op.(znz_head0) w%i_op.(znz_add_mul_div) w%i_op.(znz_div21)" i i i; pr " w%i_op.(znz_compare) w%i_op.(znz_sub)." i i; done; @@ -2002,14 +2002,14 @@ let _ = pr " (iter _ "; for i = 0 to size do pr " (fun x y => reduce_%i (w%i_mod_gt x y))" i i; - pr " (fun n x y => reduce_%i (w%i_mod_gt x (GenBase.get_low %s (S n) y)))" i i (pz i); + pr " (fun n x y => reduce_%i (w%i_mod_gt x (DoubleBase.get_low %s (S n) y)))" i i (pz i); pr " (fun n x y => reduce_%i (w%i_modn1 (S n) x y))" i i; done; pr " mod_gtnm)."; pr ""; pp " Let spec_modn1 ww (ww_op: znz_op ww) (ww_spec: znz_spec ww_op) := "; - pp " (spec_gen_modn1 "; + pp " (spec_double_modn1 "; pp " ww_op.(znz_zdigits) ww_op.(znz_0)"; pp " ww_op.(znz_WW) ww_op.(znz_head0)"; pp " ww_op.(znz_add_mul_div) ww_op.(znz_div21)"; @@ -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 " (ZnZ.spec_compare ww_spec) (ZnZ.spec_sub ww_spec))."; + pp " (Z_nZ.spec_compare ww_spec) (Z_nZ.spec_sub ww_spec))."; pp ""; pr " Theorem spec_mod_gt:"; @@ -2029,7 +2029,7 @@ let _ = pp " [res] = x mod y)"; for i = 0 to size do pp " (fun x y => reduce_%i (w%i_mod_gt x y))" i i; - pp " (fun n x y => reduce_%i (w%i_mod_gt x (GenBase.get_low %s (S n) y)))" i i (pz i); + pp " (fun n x y => reduce_%i (w%i_mod_gt x (DoubleBase.get_low %s (S n) y)))" i i (pz i); pp " (fun n x y => reduce_%i (w%i_modn1 (S n) x y)) _ _ _" i i; done; pp " mod_gtnm _)."; @@ -2049,7 +2049,7 @@ let _ = pp " intros n x y H2 H3; rewrite spec_reduce_%i." i else pp " intros n x y H1 H2 H3; rewrite spec_reduce_%i." i; - pp " unfold w%i_modn1, to_Z; rewrite spec_gen_eval%in." i i; + pp " unfold w%i_modn1, to_Z; rewrite spec_double_eval%in." i i; pp " apply (spec_modn1 _ _ w%i_spec); auto." i; done; pp " intros n m x y H1 H2; unfold mod_gtnm."; @@ -2152,8 +2152,8 @@ let _ = pp " apply Zis_gcd_mult; apply Zis_gcd_1."; pp " intros; apply False_ind."; pp " case (spec_digits (mod_gt a b)); auto with zarith."; - pp " intros H6; apply GenDiv.Zis_gcd_mod; auto with zarith."; - pp " apply GenDiv.Zis_gcd_mod; auto with zarith."; + pp " intros H6; apply DoubleDiv.Zis_gcd_mod; auto with zarith."; + pp " apply DoubleDiv.Zis_gcd_mod; auto with zarith."; pp " rewrite <- spec_mod_gt; auto with zarith."; pp " assert (F2: [b] > [mod_gt a b])."; pp " case (Z_mod_lt [a] [b]); auto with zarith."; @@ -2576,7 +2576,7 @@ let _ = pp " )."; pp " rewrite (spec_0 Hw)."; pp " rewrite Zmult_0_l; rewrite Zplus_0_l."; - pp " rewrite (ZnZ.spec_sub Hw)."; + pp " rewrite (Z_nZ.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 (ZnZ.spec_head0 Hw1 xx)."; + pp " case (Z_nZ.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 (ZnZ.spec_head00 Hw1 xx); auto with zarith."; + pp " rewrite (Z_nZ.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 (ZnZ.spec_head0 Hw1 xx); auto."; + pp " case (Z_nZ.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 (ZnZ.spec_head00 Hw1 xx); auto with zarith."; + pp " rewrite (Z_nZ.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 9ca078053..ea472c860 100644 --- a/theories/Numbers/Natural/BigN/Nbasic.v +++ b/theories/Numbers/Natural/BigN/Nbasic.v @@ -12,11 +12,11 @@ Require Import ZArith. Require Import BigNumPrelude. -Require Import Basic_type. Require Import Max. -Require Import GenBase. -Require Import ZnZ. -Require Import Zn2Z. +Require Import DoubleType. +Require Import DoubleBase. +Require Import Z_nZ. +Require Import Z_2nZ. (* To compute the necessary height *) @@ -301,8 +301,8 @@ Section CompareRec. end. Variable wm_to_Z_pos: forall x, 0 <= wm_to_Z x < base wm_base. - Let gen_to_Z := gen_to_Z wm_base wm_to_Z. - Let gen_wB := gen_wB wm_base. + Let double_to_Z := double_to_Z wm_base wm_to_Z. + Let double_wB := double_wB wm_base. Lemma base_xO: forall n, base (xO n) = (base n)^2. Proof. @@ -310,15 +310,15 @@ Section CompareRec. rewrite (Zpos_xO n1); rewrite Zmult_comm; rewrite Zpower_mult; auto with zarith. Qed. - Let gen_to_Z_pos: forall n x, 0 <= gen_to_Z n x < gen_wB n := - (spec_gen_to_Z wm_base wm_to_Z wm_to_Z_pos). + Let double_to_Z_pos: forall n x, 0 <= double_to_Z n x < double_wB n := + (spec_double_to_Z wm_base wm_to_Z wm_to_Z_pos). Lemma spec_compare0_mn: forall n x, match compare0_mn n x with - Eq => 0 = gen_to_Z n x - | Lt => 0 < gen_to_Z n x - | Gt => 0 > gen_to_Z n x + Eq => 0 = double_to_Z n x + | Lt => 0 < double_to_Z n x + | Gt => 0 > double_to_Z n x end. Proof. intros n; elim n; clear n; auto. @@ -327,17 +327,17 @@ Section CompareRec. intros xh xl. generalize (Hrec xh); case compare0_mn; auto. generalize (Hrec xl); case compare0_mn; auto. - simpl gen_to_Z; intros H1 H2; rewrite H1; rewrite <- H2; auto. - simpl gen_to_Z; intros H1 H2; rewrite <- H2; auto. - case (gen_to_Z_pos n xl); auto with zarith. - intros H1; simpl gen_to_Z. - set (u := GenBase.gen_wB wm_base n). - case (gen_to_Z_pos n xl); intros H2 H3. + simpl double_to_Z; intros H1 H2; rewrite H1; rewrite <- H2; auto. + simpl double_to_Z; intros H1 H2; rewrite <- H2; auto. + case (double_to_Z_pos n xl); auto with zarith. + intros H1; simpl double_to_Z. + set (u := DoubleBase.double_wB wm_base n). + case (double_to_Z_pos n xl); intros H2 H3. assert (0 < u); auto with zarith. - unfold u, GenBase.gen_wB, base; auto with zarith. + unfold u, DoubleBase.double_wB, base; auto with zarith. change 0 with (0 + 0); apply Zplus_lt_le_compat; auto with zarith. apply Zmult_lt_0_compat; auto with zarith. - case (gen_to_Z_pos n xh); auto with zarith. + case (double_to_Z_pos n xh); auto with zarith. Qed. Fixpoint compare_mn_1 (n:nat) : word wm n -> w -> comparison := @@ -369,15 +369,15 @@ Section CompareRec. Variable wm_base_lt: forall x, 0 <= w_to_Z x < base (wm_base). - Let gen_wB_lt: forall n x, - 0 <= w_to_Z x < (gen_wB n). + Let double_wB_lt: forall n x, + 0 <= w_to_Z x < (double_wB n). Proof. intros n x; elim n; simpl; auto; clear n. intros n (H0, H); split; auto. apply Zlt_le_trans with (1:= H). - unfold gen_wB, GenBase.gen_wB; simpl. + unfold double_wB, DoubleBase.double_wB; simpl. rewrite base_xO. - set (u := base (gen_digits wm_base n)). + set (u := base (double_digits wm_base n)). assert (0 < u). unfold u, base; auto with zarith. replace (u^2) with (u * u); simpl; auto with zarith. @@ -388,9 +388,9 @@ Section CompareRec. Lemma spec_compare_mn_1: forall n x y, match compare_mn_1 n x y with - Eq => gen_to_Z n x = w_to_Z y - | Lt => gen_to_Z n x < w_to_Z y - | Gt => gen_to_Z n x > w_to_Z y + Eq => double_to_Z n x = w_to_Z y + | Lt => double_to_Z n x < w_to_Z y + | Gt => double_to_Z n x > w_to_Z y end. Proof. intros n; elim n; simpl; auto; clear n. @@ -400,13 +400,13 @@ Section CompareRec. rewrite <- H1b; rewrite Zmult_0_l; rewrite Zplus_0_l; auto. apply Hrec. apply Zlt_gt. - case (gen_wB_lt n y); intros _ H0. + case (double_wB_lt n y); intros _ H0. apply Zlt_le_trans with (1:= H0). - fold gen_wB. - case (gen_to_Z_pos n xl); intros H1 H2. - apply Zle_trans with (gen_to_Z n xh * gen_wB n); auto with zarith. - apply Zle_trans with (1 * gen_wB n); auto with zarith. - case (gen_to_Z_pos n xh); auto with zarith. + fold double_wB. + case (double_to_Z_pos n xl); intros H1 H2. + apply Zle_trans with (double_to_Z n xh * double_wB n); auto with zarith. + apply Zle_trans with (1 * double_wB n); auto with zarith. + case (double_to_Z_pos n xh); auto with zarith. Qed. End CompareRec. |