diff options
Diffstat (limited to 'coqprime/num/W.v')
| -rw-r--r-- | coqprime/num/W.v | 200 |
1 files changed, 200 insertions, 0 deletions
diff --git a/coqprime/num/W.v b/coqprime/num/W.v new file mode 100644 index 000000000..d26e2657e --- /dev/null +++ b/coqprime/num/W.v @@ -0,0 +1,200 @@ + +(*************************************************************) +(* 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. |