blob: d26e2657e1ff27c94aafee5a2c4541bfdd27b7a2 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
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.
|
