diff options
Diffstat (limited to 'coqprime/num/W.v')
| -rw-r--r-- | coqprime/num/W.v | 200 |
1 files changed, 0 insertions, 200 deletions
diff --git a/coqprime/num/W.v b/coqprime/num/W.v deleted file mode 100644 index d26e2657e..000000000 --- a/coqprime/num/W.v +++ /dev/null @@ -1,200 +0,0 @@ - -(*************************************************************) -(* This file is distributed under the terms of the *) -(* GNU Lesser General Public License Version 2.1 *) -(*************************************************************) -(* Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr *) -(*************************************************************) - -Set Implicit Arguments. -Require Import CyclicAxioms DoubleCyclic BigN Cyclic31 Int31. -Require Import ZArith ZCAux. - -(* ** Type of words ** *) - - -(* Make the words *) - -Definition mk_word: forall (w: Type) (n:nat), Type. -fix 2. -intros w n; case n; simpl. -exact int31. -intros n1; exact (zn2z (mk_word w n1)). -Defined. - -(* Make the op *) -Fixpoint mk_op (w : Type) (op : ZnZ.Ops w) (n : nat) {struct n} : - ZnZ.Ops (word w n) := - match n return (ZnZ.Ops (word w n)) with - | O => op - | S n1 => mk_zn2z_ops_karatsuba (mk_op op n1) - end. - -Theorem mk_op_digits: forall w (op: ZnZ.Ops w) n, - (Zpos (ZnZ.digits (mk_op op n)) = 2 ^ Z_of_nat n * Zpos (ZnZ.digits op))%Z. -intros w op n; elim n; simpl mk_op; auto; clear n. -intros n Rec; simpl ZnZ.digits. -rewrite Zpos_xO; rewrite Rec. -rewrite Zmult_assoc; apply f_equal2 with (f := Zmult); auto. -rewrite inj_S; unfold Zsucc; rewrite Zplus_comm. -rewrite Zpower_exp; auto with zarith. -Qed. - -Theorem digits_pos: forall w (op: ZnZ.Ops w) n, - (1 < Zpos (ZnZ.digits op) -> 1 < Zpos (ZnZ.digits (mk_op op n)))%Z. -intros w op n H. -rewrite mk_op_digits. -rewrite <- (Zmult_1_r 1). -apply Zle_lt_trans with (2 ^ (Z_of_nat n) * 1)%Z. -apply Zmult_le_compat_r; auto with zarith. -rewrite <- (Zpower_0_r 2). -apply Zpower_le_monotone; auto with zarith. -apply Zmult_lt_compat_l; auto with zarith. -Qed. - -Fixpoint mk_spec (w : Type) (op : ZnZ.Ops w) (op_spec : ZnZ.Specs op) - (H: (1 < Zpos (ZnZ.digits op))%Z) (n : nat) - {struct n} : ZnZ.Specs (mk_op op n) := - match n return (ZnZ.Specs (mk_op op n)) with - | O => op_spec - | S n1 => - @mk_zn2z_specs_karatsuba (word w n1) (mk_op op n1) - (* (digits_pos op n1 H) *) (mk_spec op_spec H n1) - end. - -(* ** Operators ** *) -Definition w31_1_op := mk_zn2z_ops int31_ops. -Definition w31_2_op := mk_zn2z_ops w31_1_op. -Definition w31_3_op := mk_zn2z_ops w31_2_op. -Definition w31_4_op := mk_zn2z_ops_karatsuba w31_3_op. -Definition w31_5_op := mk_zn2z_ops_karatsuba w31_4_op. -Definition w31_6_op := mk_zn2z_ops_karatsuba w31_5_op. -Definition w31_7_op := mk_zn2z_ops_karatsuba w31_6_op. -Definition w31_8_op := mk_zn2z_ops_karatsuba w31_7_op. -Definition w31_9_op := mk_zn2z_ops_karatsuba w31_8_op. -Definition w31_10_op := mk_zn2z_ops_karatsuba w31_9_op. -Definition w31_11_op := mk_zn2z_ops_karatsuba w31_10_op. -Definition w31_12_op := mk_zn2z_ops_karatsuba w31_11_op. -Definition w31_13_op := mk_zn2z_ops_karatsuba w31_12_op. -Definition w31_14_op := mk_zn2z_ops_karatsuba w31_13_op. - -Definition cmk_op: forall (n: nat), ZnZ.Ops (word int31 n). -intros n; case n; clear n. -exact int31_ops. -intros n; case n; clear n. -exact w31_1_op. -intros n; case n; clear n. -exact w31_2_op. -intros n; case n; clear n. -exact w31_3_op. -intros n; case n; clear n. -exact w31_4_op. -intros n; case n; clear n. -exact w31_5_op. -intros n; case n; clear n. -exact w31_6_op. -intros n; case n; clear n. -exact w31_7_op. -intros n; case n; clear n. -exact w31_8_op. -intros n; case n; clear n. -exact w31_9_op. -intros n; case n; clear n. -exact w31_10_op. -intros n; case n; clear n. -exact w31_11_op. -intros n; case n; clear n. -exact w31_12_op. -intros n; case n; clear n. -exact w31_13_op. -intros n; case n; clear n. -exact w31_14_op. -intros n. -match goal with |- context[S ?X] => - exact (mk_op int31_ops (S X)) -end. -Defined. - -Definition cmk_spec: forall n, ZnZ.Specs (cmk_op n). -assert (S1: ZnZ.Specs w31_1_op). -unfold w31_1_op; apply mk_zn2z_specs; auto with zarith. -exact int31_specs. -assert (S2: ZnZ.Specs w31_2_op). -unfold w31_2_op; apply mk_zn2z_specs; auto with zarith. -assert (S3: ZnZ.Specs w31_3_op). -unfold w31_3_op; apply mk_zn2z_specs; auto with zarith. -assert (S4: ZnZ.Specs w31_4_op). -unfold w31_4_op; apply mk_zn2z_specs_karatsuba; auto with zarith. -assert (S5: ZnZ.Specs w31_5_op). -unfold w31_5_op; apply mk_zn2z_specs_karatsuba; auto with zarith. -assert (S6: ZnZ.Specs w31_6_op). -unfold w31_6_op; apply mk_zn2z_specs_karatsuba; auto with zarith. -assert (S7: ZnZ.Specs w31_7_op). -unfold w31_7_op; apply mk_zn2z_specs_karatsuba; auto with zarith. -assert (S8: ZnZ.Specs w31_8_op). -unfold w31_8_op; apply mk_zn2z_specs_karatsuba; auto with zarith. -assert (S9: ZnZ.Specs w31_9_op). -unfold w31_9_op; apply mk_zn2z_specs_karatsuba; auto with zarith. -assert (S10: ZnZ.Specs w31_10_op). -unfold w31_10_op; apply mk_zn2z_specs_karatsuba; auto with zarith. -assert (S11: ZnZ.Specs w31_11_op). -unfold w31_11_op; apply mk_zn2z_specs_karatsuba; auto with zarith. -assert (S12: ZnZ.Specs w31_12_op). -unfold w31_12_op; apply mk_zn2z_specs_karatsuba; auto with zarith. -assert (S13: ZnZ.Specs w31_13_op). -unfold w31_13_op; apply mk_zn2z_specs_karatsuba; auto with zarith. -assert (S14: ZnZ.Specs w31_14_op). -unfold w31_14_op; apply mk_zn2z_specs_karatsuba; auto with zarith. -intros n; case n; clear n. -exact int31_specs. -intros n; case n; clear n. -exact S1. -intros n; case n; clear n. -exact S2. -intros n; case n; clear n. -exact S3. -intros n; case n; clear n. -exact S4. -intros n; case n; clear n. -exact S5. -intros n; case n; clear n. -exact S6. -intros n; case n; clear n. -exact S7. -intros n; case n; clear n. -exact S8. -intros n; case n; clear n. -exact S9. -intros n; case n; clear n. -exact S10. -intros n; case n; clear n. -exact S11. -intros n; case n; clear n. -exact S12. -intros n; case n; clear n. -exact S13. -intros n; case n; clear n. -exact S14. -intro n. -simpl cmk_op. -repeat match goal with |- ZnZ.Specs - (mk_zn2z_ops_karatsuba ?X) => - generalize (@mk_zn2z_specs_karatsuba _ X); intros tmp; - apply tmp; clear tmp; auto with zarith -end. -(* -apply digits_pos. -*) -auto with zarith. -apply mk_spec. -exact int31_specs. -auto with zarith. -Defined. - - -Theorem cmk_op_digits: forall n, - (Zpos (ZnZ.digits (cmk_op n)) = 2 ^ (Z_of_nat n) * 31)%Z. -do 15 (intros n; case n; clear n; [try reflexivity | idtac]). -intros n; unfold cmk_op; lazy beta. -rewrite mk_op_digits; auto. -Qed. |