1 (* ========================================================================= *)
2 (* Existence of primitive roots modulo certain numbers. *)
3 (* ========================================================================= *)
5 needs "Library/integer.ml";;
6 needs "Library/isum.ml";;
7 needs "Library/binomial.ml";;
8 needs "Library/pocklington.ml";;
9 needs "Library/multiplicative.ml";;
11 (* ------------------------------------------------------------------------- *)
12 (* Some lemmas connecting concepts in the various background theories. *)
13 (* ------------------------------------------------------------------------- *)
15 let DIVIDES_BINOM_PRIME = prove
16 (`!n p. prime p /\ 0 < n /\ n < p ==> p divides binom(p,n)`,
18 MP_TAC(AP_TERM `(divides) p` (SPECL [`p - n:num`; `n:num`] BINOM_FACT)) THEN
19 ASM_SIMP_TAC[DIVIDES_FACT_PRIME; PRIME_DIVPROD_EQ; SUB_ADD; LT_IMP_LE] THEN
20 ASM_REWRITE_TAC[GSYM NOT_LT; LT_REFL] THEN
21 ASM_SIMP_TAC[ARITH_RULE `0 < n /\ n < p ==> p - n < p`]);;
24 (`!p. int_prime(&p) <=> prime p`,
25 GEN_TAC THEN REWRITE_TAC[prime; int_prime] THEN
26 ONCE_REWRITE_TAC[GSYM INT_DIVIDES_LABS] THEN
27 REWRITE_TAC[GSYM INT_FORALL_ABS; GSYM num_divides; INT_ABS_NUM] THEN
28 REWRITE_TAC[INT_OF_NUM_GT; INT_OF_NUM_EQ] THEN ASM_CASES_TAC `p = 0` THENL
29 [ASM_REWRITE_TAC[ARITH; DIVIDES_0] THEN DISCH_THEN(MP_TAC o SPEC `2`);
30 AP_THM_TAC THEN AP_TERM_TAC] THEN
33 (* ------------------------------------------------------------------------- *)
34 (* Explicit formula for difference of real/integer polynomials. *)
35 (* ------------------------------------------------------------------------- *)
37 let REAL_POLY_DIFF_EXPLICIT = prove
39 sum(0..n) (\i. a(i) * x pow i) - sum(0..n) (\i. a(i) * y pow i) =
41 sum(0..n-1) (\i. sum(i+1..n) (\j. a j * y pow (j - 1 - i)) * x pow i)`,
43 REWRITE_TAC[GSYM SUM_SUB_NUMSEG; GSYM REAL_SUB_LDISTRIB] THEN
44 MP_TAC(ISPEC `n:num` LE_0) THEN SIMP_TAC[SUM_CLAUSES_LEFT; ADD_CLAUSES] THEN
45 DISCH_THEN(K ALL_TAC) THEN
46 REWRITE_TAC[REAL_SUB_REFL; REAL_MUL_RZERO; REAL_ADD_LID; real_pow] THEN
47 SIMP_TAC[REAL_SUB_POW] THEN
48 ONCE_REWRITE_TAC[REAL_ARITH `a * b * c:real = b * a * c`] THEN
49 REWRITE_TAC[SUM_LMUL] THEN AP_TERM_TAC THEN
50 SIMP_TAC[GSYM SUM_LMUL; GSYM SUM_RMUL; SUM_SUM_PRODUCT; FINITE_NUMSEG] THEN
51 MATCH_MP_TAC SUM_EQ_GENERAL_INVERSES THEN
52 REPEAT(EXISTS_TAC `\(a:num,b:num). (b,a)`) THEN
53 REWRITE_TAC[IN_ELIM_PAIR_THM; FORALL_PAIR_THM; REAL_MUL_AC] THEN
54 REWRITE_TAC[IN_NUMSEG] THEN ARITH_TAC);;
56 let INT_POLY_DIFF_EXPLICIT = INT_OF_REAL_THM REAL_POLY_DIFF_EXPLICIT;;
58 (* ------------------------------------------------------------------------- *)
59 (* Lagrange's theorem on number of roots modulo a prime. *)
60 (* ------------------------------------------------------------------------- *)
62 let FINITE_INTSEG_RESTRICT = prove
63 (`!P a b. FINITE {x:int | a <= x /\ x <= b /\ P x}`,
64 SIMP_TAC[FINITE_RESTRICT; FINITE_INTSEG; SET_RULE
65 `{x | P x /\ Q x /\ R x} = {x | x IN {x | P x /\ Q x} /\ R x}`]);;
67 let INT_POLY_LAGRANGE = prove
69 int_prime p /\ r - l < p
70 ==> !n a. ~(!i. i <= n ==> (a i == &0) (mod p))
71 ==> CARD {x | l <= x /\ x <= r /\
72 (isum(0..n) (\i. a(i) * x pow i) == &0) (mod p)}
74 REPEAT GEN_TAC THEN STRIP_TAC THEN REWRITE_TAC[INT_CONG_0_DIVIDES] THEN
75 MATCH_MP_TAC num_WF THEN REPEAT STRIP_TAC THEN MATCH_MP_TAC(MESON[]
76 `!a. (~(s = a) ==> CARD s <= n) /\ CARD a <= n ==> CARD s <= n`) THEN
77 EXISTS_TAC `{}:int->bool` THEN REWRITE_TAC[LE_0; CARD_CLAUSES] THEN
78 REWRITE_TAC[GSYM MEMBER_NOT_EMPTY; LEFT_IMP_EXISTS_THM; IN_ELIM_THM] THEN
79 X_GEN_TAC `c:int` THEN STRIP_TAC THEN ASM_CASES_TAC `n = 0` THENL
80 [MAP_EVERY UNDISCH_TAC
81 [`~(!i:num. i <= n ==> (p:int) divides (a i))`;
82 `p divides (isum (0..n) (\i. a i * c pow i))`] THEN
83 ASM_SIMP_TAC[CONJUNCT1 LE; ISUM_CLAUSES_NUMSEG] THEN
84 REWRITE_TAC[INT_POW; LEFT_FORALL_IMP_THM; EXISTS_REFL; INT_MUL_RID] THEN
87 ASM_CASES_TAC `p divides ((a:num->int) n)` THENL
88 [ASM_SIMP_TAC[ISUM_CLAUSES_RIGHT; LE_0; LE_1] THEN
89 ASM_SIMP_TAC[INTEGER_RULE
90 `(p:int) divides y ==> (p divides (x + y * z) <=> p divides x)`] THEN
91 MATCH_MP_TAC(ARITH_RULE `x <= n - 1 ==> x <= n`) THEN
92 FIRST_X_ASSUM(MP_TAC o SPEC `n - 1`) THEN
93 ASM_REWRITE_TAC[ARITH_RULE `n - 1 < n <=> ~(n = 0)`] THEN
94 DISCH_THEN MATCH_MP_TAC THEN
95 ASM_MESON_TAC[ARITH_RULE `i <= n <=> i <= n - 1 \/ i = n`]; ALL_TAC] THEN
96 MP_TAC(GEN `x:int` (MATCH_MP
98 `a - b:int = c ==> p divides b ==> (p divides a <=> p divides c)`)
99 (ISPECL [`n:num`; `a:num->int`; `x:int`; `c:int`]
100 INT_POLY_DIFF_EXPLICIT))) THEN
101 ASM_SIMP_TAC[INT_PRIME_DIVPROD_EQ] THEN DISCH_THEN(K ALL_TAC) THEN
102 ASM_REWRITE_TAC[LEFT_OR_DISTRIB; SET_RULE
103 `{x | q x \/ r x} = {x | q x} UNION {x | r x}`] THEN
105 `{x:int | l <= x /\ x <= r /\ p divides (x - c)} = {c}`
107 [MATCH_MP_TAC(SET_RULE `P c /\ (!x y. P x /\ P y ==> x = y)
108 ==> {x | P x} = {c}`) THEN
109 ASM_REWRITE_TAC[INT_SUB_REFL; INT_DIVIDES_0] THEN
110 MAP_EVERY X_GEN_TAC [`u:int`; `v:int`] THEN STRIP_TAC THEN
111 SUBGOAL_THEN `p divides (u - v:int)` MP_TAC THENL
112 [ASM_MESON_TAC[INT_CONG; INT_CONG_SYM; INT_CONG_TRANS]; ALL_TAC] THEN
113 DISCH_THEN(MP_TAC o MATCH_MP INT_DIVIDES_LE) THEN ASM_INT_ARITH_TAC;
115 REWRITE_TAC[SET_RULE `{a} UNION s = a INSERT s`] THEN
116 SIMP_TAC[CARD_CLAUSES; FINITE_INTSEG_RESTRICT] THEN
117 MATCH_MP_TAC(ARITH_RULE
118 `~(n = 0) /\ x <= n - 1 ==> (if p then x else SUC x) <= n`) THEN
119 ASM_REWRITE_TAC[] THEN
120 RULE_ASSUM_TAC(REWRITE_RULE[RIGHT_IMP_FORALL_THM; IMP_IMP]) THEN
121 FIRST_ASSUM MATCH_MP_TAC THEN
122 ASM_REWRITE_TAC[ARITH_RULE `n - 1 < n <=> ~(n = 0)`] THEN
123 DISCH_THEN(MP_TAC o SPEC `n - 1`) THEN
124 ASM_SIMP_TAC[LE_REFL; SUB_ADD; LE_1; ISUM_SING_NUMSEG; SUB_REFL] THEN
125 ASM_REWRITE_TAC[INT_POW; INT_MUL_RID]);;
127 (* ------------------------------------------------------------------------- *)
128 (* Laborious instantiation to (x^d == 1) (mod p) over natural numbers. *)
129 (* ------------------------------------------------------------------------- *)
131 let NUM_LAGRANGE_LEMMA = prove
132 (`!p d. prime p /\ 1 <= d
133 ==> CARD {x | x IN 1..p-1 /\ (x EXP d == 1) (mod p)} <= d`,
134 REPEAT STRIP_TAC THEN
135 MP_TAC(ISPECL [`&p:int`; `&1:int`; `&(p-1):int`] INT_POLY_LAGRANGE) THEN
137 [ASM_SIMP_TAC[INT_PRIME; INT_LT_SUB_RADD; INT_OF_NUM_ADD; INT_OF_NUM_LT] THEN
140 DISCH_THEN(MP_TAC o SPECL
141 [`d:num`; `\i. if i = d then &1 else if i = 0 then -- &1 else &0:int`]) THEN
142 REWRITE_TAC[] THEN ANTS_TAC THENL
143 [DISCH_THEN(MP_TAC o SPEC `d:num`) THEN REWRITE_TAC[LE_REFL] THEN
144 REWRITE_TAC[INT_CONG_0_DIVIDES; GSYM num_divides; DIVIDES_ONE] THEN
145 ASM_MESON_TAC[PRIME_1];
148 `(if p then x else y) * z:int = if p then x * z else y * z`] THEN
149 SIMP_TAC[ISUM_CASES; FINITE_NUMSEG; FINITE_RESTRICT] THEN
150 REWRITE_TAC[INT_POW; INT_MUL_LZERO; ISUM_0; INT_ADD_RID] THEN
151 MATCH_MP_TAC(ARITH_RULE `x:num <= y ==> y <= d ==> x <= d`) THEN
152 REWRITE_TAC[IN_ELIM_THM; IN_NUMSEG] THEN
153 ASM_SIMP_TAC[ARITH_RULE `(0 <= i /\ i <= d) /\ i = d <=> i = d`;
155 ==> (((0 <= i /\ i <= d) /\ ~(i = d)) /\ i = 0 <=>
157 REWRITE_TAC[SING_GSPEC; ISUM_SING] THEN
158 REWRITE_TAC[INT_ARITH `&1 * x + -- &1 * &1:int = x - &1`] THEN
159 REWRITE_TAC[INTEGER_RULE `(x - a:int == &0) (mod p) <=>
160 (x == a) (mod p)`] THEN
161 MATCH_MP_TAC CARD_SUBSET_IMAGE THEN EXISTS_TAC `num_of_int` THEN
162 REWRITE_TAC[FINITE_INTSEG_RESTRICT; SUBSET; IN_IMAGE; IN_ELIM_THM] THEN
163 X_GEN_TAC `n:num` THEN DISCH_TAC THEN EXISTS_TAC `&n:int` THEN
164 ASM_REWRITE_TAC[NUM_OF_INT_OF_NUM; INT_OF_NUM_LE; INT_OF_NUM_POW] THEN
165 ASM_REWRITE_TAC[GSYM num_congruent]);;
167 (* ------------------------------------------------------------------------- *)
168 (* Count of elements with a given order modulo a prime. *)
169 (* ------------------------------------------------------------------------- *)
171 let COUNT_ORDERS_MODULO_PRIME = prove
172 (`!p d. prime p /\ d divides (p - 1)
173 ==> CARD {x | x IN 1..p-1 /\ order p x = d} = phi(d)`,
176 FINITE s /\ (!x. x IN s ==> f(x) <= g(x)) /\ nsum s f = nsum s g
177 ==> !x. x IN s ==> f x = g x`,
178 REWRITE_TAC[GSYM LE_ANTISYM] THEN MESON_TAC[NSUM_LE; NSUM_LT; NOT_LE]) in
179 REWRITE_TAC[IMP_CONJ; RIGHT_FORALL_IMP_THM] THEN GEN_TAC THEN DISCH_TAC THEN
180 ONCE_REWRITE_TAC[SET_RULE
181 `(!x. p x ==> q x) <=> (!x. x IN {x | p x} ==> q x)`] THEN
182 MATCH_MP_TAC lemma THEN SUBGOAL_THEN `~(p - 1 = 0)` ASSUME_TAC THENL
183 [FIRST_ASSUM(MP_TAC o MATCH_MP PRIME_GE_2) THEN ARITH_TAC; ALL_TAC] THEN
184 ASM_SIMP_TAC[REWRITE_RULE[ETA_AX] PHI_DIVISORSUM; FINITE_DIVISORS] THEN
187 SIMP_TAC[CARD_EQ_NSUM; FINITE_RESTRICT; FINITE_NUMSEG] THEN
188 W(MP_TAC o PART_MATCH (lhs o rand) NSUM_GROUP o lhs o snd) THEN
189 REWRITE_TAC[NSUM_CONST_NUMSEG; FINITE_NUMSEG; ADD_SUB; MULT_CLAUSES] THEN
190 DISCH_THEN MATCH_MP_TAC THEN
191 REWRITE_TAC[SUBSET; FORALL_IN_IMAGE; IN_ELIM_THM; IN_NUMSEG] THEN
192 X_GEN_TAC `x:num` THEN STRIP_TAC THEN ASM_SIMP_TAC[GSYM PHI_PRIME] THEN
193 MATCH_MP_TAC ORDER_DIVIDES_PHI THEN ONCE_REWRITE_TAC[COPRIME_SYM] THEN
194 MATCH_MP_TAC PRIME_COPRIME_LT THEN ASM_REWRITE_TAC[] THEN
196 X_GEN_TAC `d:num` THEN REWRITE_TAC[IN_ELIM_THM] THEN DISCH_TAC THEN
197 ASM_CASES_TAC `{x | x IN 1..p-1 /\ order p x = d} = {}` THEN
198 ASM_REWRITE_TAC[CARD_CLAUSES; LE_0] THEN
199 FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [GSYM MEMBER_NOT_EMPTY]) THEN
200 REWRITE_TAC[IN_ELIM_THM; LEFT_IMP_EXISTS_THM] THEN X_GEN_TAC `a:num` THEN
201 REWRITE_TAC[IN_NUMSEG] THEN STRIP_TAC THEN REWRITE_TAC[PHI_ALT] THEN
202 MATCH_MP_TAC CARD_SUBSET_IMAGE THEN EXISTS_TAC `\m. (a EXP m) MOD p` THEN
203 REWRITE_TAC[PHI_FINITE_LEMMA] THEN
204 SUBGOAL_THEN `1 <= d` ASSUME_TAC THENL
205 [ASM_MESON_TAC[LE_1; DIVIDES_ZERO]; ALL_TAC] THEN
206 SUBGOAL_THEN `coprime(p,a)` ASSUME_TAC THENL
207 [ONCE_REWRITE_TAC[COPRIME_SYM] THEN
208 MATCH_MP_TAC PRIME_COPRIME_LT THEN ASM_REWRITE_TAC[] THEN
212 `{x | x IN 1..p-1 /\ (x EXP d == 1) (mod p)} =
213 IMAGE (\m. (a EXP m) MOD p) {m | m < d}`
215 [CONV_TAC SYM_CONV THEN MATCH_MP_TAC CARD_SUBSET_LE THEN
216 SIMP_TAC[FINITE_RESTRICT; FINITE_NUMSEG] THEN CONJ_TAC THENL
217 [REWRITE_TAC[SUBSET; FORALL_IN_IMAGE; IN_ELIM_THM] THEN
218 X_GEN_TAC `m:num` THEN DISCH_TAC THEN REWRITE_TAC[IN_NUMSEG] THEN
219 ASM_SIMP_TAC[ARITH_RULE `~(p - 1 = 0) ==> (x <= p - 1 <=> x < p)`] THEN
220 ASM_SIMP_TAC[DIVISION; PRIME_IMP_NZ] THEN CONJ_TAC THENL
221 [REWRITE_TAC[ARITH_RULE `1 <= x <=> ~(x = 0)`] THEN
222 ASM_SIMP_TAC[GSYM DIVIDES_MOD; PRIME_IMP_NZ] THEN
223 ASM_MESON_TAC[PRIME_DIVEXP; PRIME_COPRIME_EQ];
224 ASM_SIMP_TAC[CONG; PRIME_IMP_NZ; MOD_EXP_MOD] THEN
225 REWRITE_TAC[EXP_EXP] THEN ONCE_REWRITE_TAC[MULT_SYM] THEN
226 REWRITE_TAC[GSYM EXP_EXP] THEN
227 SUBST1_TAC(SYM(SPEC `m:num` EXP_ONE)) THEN
228 ASM_SIMP_TAC[GSYM CONG; PRIME_IMP_NZ] THEN
229 MATCH_MP_TAC CONG_EXP THEN ASM_MESON_TAC[ORDER]];
230 MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `d:num` THEN
231 ASM_SIMP_TAC[NUM_LAGRANGE_LEMMA] THEN
232 GEN_REWRITE_TAC LAND_CONV [GSYM CARD_NUMSEG_LT] THEN
233 MATCH_MP_TAC EQ_IMP_LE THEN CONV_TAC SYM_CONV THEN
234 MATCH_MP_TAC CARD_IMAGE_INJ THEN
235 ASM_SIMP_TAC[GSYM CONG; PRIME_IMP_NZ; FINITE_NUMSEG_LT; IN_ELIM_THM] THEN
236 ASM_SIMP_TAC[ORDER_DIVIDES_EXPDIFF] THEN REWRITE_TAC[CONG_IMP_EQ]];
237 MATCH_MP_TAC(SET_RULE
238 `s' SUBSET s /\ (!x. x IN t /\ f x IN s' ==> x IN t')
239 ==> s = IMAGE f t ==> s' SUBSET IMAGE f t'`) THEN
240 SIMP_TAC[SUBSET; IN_ELIM_THM; IN_NUMSEG] THEN
241 CONJ_TAC THENL [MESON_TAC[ORDER]; ALL_TAC] THEN
242 X_GEN_TAC `m:num` THEN ABBREV_TAC `b = (a EXP m) MOD p` THEN STRIP_TAC THEN
243 REWRITE_TAC[coprime; divides] THEN X_GEN_TAC `e:num` THEN
244 DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_THEN `m':num` (ASSUME_TAC o SYM))
245 (X_CHOOSE_THEN `d':num` (ASSUME_TAC o SYM))) THEN
246 MP_TAC(ISPECL [`p:num`; `b:num`] ORDER_WORKS) THEN
247 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC (MP_TAC o SPEC `d':num`)) THEN
248 ASM_REWRITE_TAC[] THEN
249 MATCH_MP_TAC(TAUT `a /\ c /\ (~b ==> d) ==> (a /\ b ==> ~c) ==> d`) THEN
250 REPEAT CONJ_TAC THENL
251 [UNDISCH_TAC `1 <= d` THEN EXPAND_TAC "d" THEN
252 REWRITE_TAC[ARITH_RULE `1 <= d <=> ~(d = 0)`; MULT_EQ_0] THEN
253 SIMP_TAC[DE_MORGAN_THM; ARITH_RULE `0 < d <=> ~(d = 0)`];
254 EXPAND_TAC "b" THEN ASM_SIMP_TAC[CONG; PRIME_IMP_NZ; MOD_EXP_MOD] THEN
255 EXPAND_TAC "m" THEN REWRITE_TAC[EXP_EXP] THEN
256 ONCE_REWRITE_TAC[ARITH_RULE `(e * m') * d':num = (e * d') * m'`] THEN
257 ASM_REWRITE_TAC[] THEN REWRITE_TAC[GSYM EXP_EXP] THEN
258 SUBST1_TAC(SYM(SPEC `m':num` EXP_ONE)) THEN
259 ASM_SIMP_TAC[GSYM CONG; PRIME_IMP_NZ] THEN
260 MATCH_MP_TAC CONG_EXP THEN ASM_MESON_TAC[ORDER];
262 REWRITE_TAC[ARITH_RULE `~(d < e * d) <=> e * d <= 1 * d`] THEN
263 REWRITE_TAC[LE_MULT_RCANCEL] THEN
264 REWRITE_TAC[ARITH_RULE `e <= 1 <=> e = 0 \/ e = 1`] THEN
265 STRIP_TAC THEN UNDISCH_TAC `e * d':num = d` THEN
266 ASM_REWRITE_TAC[] THEN ASM_ARITH_TAC]]);;
268 (* ------------------------------------------------------------------------- *)
269 (* In particular, primitive roots modulo a prime. *)
270 (* ------------------------------------------------------------------------- *)
272 let PRIMITIVE_ROOTS_MODULO_PRIME = prove
273 (`!p. prime p ==> CARD {x | x IN 1..p-1 /\ order p x = p - 1} = phi(p - 1)`,
274 REPEAT STRIP_TAC THEN
275 MP_TAC(ISPECL [`p:num`; `p - 1`] COUNT_ORDERS_MODULO_PRIME) THEN
276 ASM_REWRITE_TAC[DIVIDES_REFL]);;
278 let PRIMITIVE_ROOT_MODULO_PRIME = prove
279 (`!p. prime p ==> ?x. x IN 1..p-1 /\ order p x = p - 1`,
280 REPEAT STRIP_TAC THEN
281 FIRST_ASSUM(MP_TAC o MATCH_MP PRIMITIVE_ROOTS_MODULO_PRIME) THEN
282 ASM_CASES_TAC `{x | x IN 1..p-1 /\ order p x = p - 1} = {}` THENL
283 [ASM_REWRITE_TAC[CARD_CLAUSES]; ASM SET_TAC[]] THEN
284 ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN DISCH_THEN(K ALL_TAC) THEN
285 MATCH_MP_TAC(ARITH_RULE `1 <= p ==> ~(0 = p)`) THEN
286 MATCH_MP_TAC PHI_LOWERBOUND_1_STRONG THEN
287 FIRST_X_ASSUM(MP_TAC o MATCH_MP PRIME_GE_2) THEN ARITH_TAC);;
289 (* ------------------------------------------------------------------------- *)
290 (* Now primitive roots modulo odd prime powers. *)
291 (* ------------------------------------------------------------------------- *)
293 let COPRIME_1_PLUS_POWER_STEP = prove
294 (`!p z k. prime p /\ coprime(z,p) /\ 3 <= p /\ 1 <= k
295 ==> ?w. coprime(w,p) /\
296 (1 + z * p EXP k) EXP p = 1 + w * p EXP (k + 1)`,
297 REPEAT STRIP_TAC THEN
298 ONCE_REWRITE_TAC[ARITH_RULE `1 + a * b = a * b + 1`] THEN
299 REWRITE_TAC[BINOMIAL_THEOREM; EXP_ONE; MULT_CLAUSES] THEN
300 SIMP_TAC[NSUM_CLAUSES_LEFT; LE_0; EXP; binom; MULT_CLAUSES; ADD_CLAUSES] THEN
301 SUBGOAL_THEN `1 <= p` MP_TAC THENL [ASM_ARITH_TAC; ALL_TAC] THEN
302 SIMP_TAC[NSUM_CLAUSES_LEFT; BINOM_1; EXP_1; ARITH] THEN DISCH_TAC THEN
304 `(p EXP (k + 2)) divides (nsum(2..p) (\i. binom(p,i) * (z * p EXP k) EXP i))`
307 REWRITE_TAC[divides; LEFT_IMP_EXISTS_THM] THEN
308 X_GEN_TAC `d:num` THEN DISCH_THEN SUBST1_TAC THEN
309 EXISTS_TAC `z + p * d:num` THEN
310 ASM_REWRITE_TAC[NUMBER_RULE
311 `coprime(z + p * d:num,p) <=> coprime(z,p)`] THEN
312 REWRITE_TAC[EXP_ADD] THEN ARITH_TAC] THEN
313 MATCH_MP_TAC NSUM_CLOSED THEN
314 REWRITE_TAC[DIVIDES_0; DIVIDES_ADD; IN_NUMSEG] THEN
315 X_GEN_TAC `j:num` THEN STRIP_TAC THEN REWRITE_TAC[MULT_EXP] THEN
316 ONCE_REWRITE_TAC[ARITH_RULE `a * b * c:num = b * c * a`] THEN
317 REWRITE_TAC[EXP_EXP] THEN
318 MATCH_MP_TAC DIVIDES_LMUL THEN ASM_CASES_TAC `j:num = p` THENL
319 [MATCH_MP_TAC DIVIDES_RMUL THEN
320 ASM_SIMP_TAC[DIVIDES_EXP_LE; ARITH_RULE `3 <= p ==> 2 <= p`] THEN
321 MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `k * 3` THEN CONJ_TAC THENL
322 [ASM_ARITH_TAC; ASM_REWRITE_TAC[LE_MULT_LCANCEL]];
323 ONCE_REWRITE_TAC[MULT_SYM] THEN
324 REWRITE_TAC[EXP; ARITH_RULE `k + 2 = SUC(k + 1)`] THEN
325 MATCH_MP_TAC DIVIDES_MUL2 THEN CONJ_TAC THENL
326 [MATCH_MP_TAC DIVIDES_BINOM_PRIME THEN ASM_REWRITE_TAC[] THEN
328 ASM_SIMP_TAC[DIVIDES_EXP_LE; ARITH_RULE `3 <= p ==> 2 <= p`] THEN
329 MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `k * 2` THEN CONJ_TAC THENL
330 [ASM_ARITH_TAC; ASM_REWRITE_TAC[LE_MULT_LCANCEL]]]]);;
332 let COPRIME_1_PLUS_POWER = prove
333 (`!p z k. prime p /\ coprime(z,p) /\ 3 <= p
334 ==> ?w. coprime(w,p) /\
335 (1 + z * p) EXP (p EXP k) = 1 + w * p EXP (k + 1)`,
336 GEN_TAC THEN GEN_TAC THEN INDUCT_TAC THEN
337 REWRITE_TAC[ADD_CLAUSES; EXP_1; EXP] THENL [MESON_TAC[]; ALL_TAC] THEN
338 REWRITE_TAC[GSYM(ONCE_REWRITE_RULE[MULT_SYM] EXP_EXP)] THEN
339 DISCH_THEN(fun th -> POP_ASSUM MP_TAC THEN STRIP_ASSUME_TAC th) THEN
340 ASM_REWRITE_TAC[] THEN
341 DISCH_THEN(X_CHOOSE_THEN `w:num` STRIP_ASSUME_TAC) THEN
342 MP_TAC(ISPECL [`p:num`; `w:num`; `k + 1`] COPRIME_1_PLUS_POWER_STEP) THEN
343 ASM_REWRITE_TAC[ARITH_RULE `1 <= k + 1`] THEN
344 REWRITE_TAC[EXP_ADD; EXP_1; MULT_AC]);;
346 let PRIMITIVE_ROOT_MODULO_PRIMEPOWS = prove
347 (`!p. prime p /\ 3 <= p
348 ==> ?g. !j. 1 <= j ==> order(p EXP j) g = phi(p EXP j)`,
349 REPEAT STRIP_TAC THEN
350 FIRST_ASSUM(MP_TAC o MATCH_MP PRIMITIVE_ROOT_MODULO_PRIME) THEN
351 REWRITE_TAC[IN_NUMSEG] THEN
352 DISCH_THEN(X_CHOOSE_THEN `g:num` STRIP_ASSUME_TAC) THEN
353 MP_TAC(ISPECL [`p:num`; `g:num`] ORDER) THEN
354 ASM_SIMP_TAC[CONG_TO_1; EXP_EQ_0; LE_1] THEN
355 DISCH_THEN(X_CHOOSE_THEN `y:num` STRIP_ASSUME_TAC) THEN
356 SUBGOAL_THEN `?x. coprime(p,y + (p - 1) * g EXP (p - 2) * x)` CHOOSE_TAC THENL
357 [MP_TAC(ISPECL [`(&p - &1:int) * &g pow (p - 2)`; `&1 - &y:int`; `&p:int`]
358 INT_CONG_SOLVE_POS) THEN
360 [REWRITE_TAC[INT_COPRIME_LMUL; INT_COPRIME_LPOW] THEN
361 REWRITE_TAC[INTEGER_RULE `coprime(p - &1,p)`; GSYM num_coprime] THEN
362 ASM_SIMP_TAC[INT_OF_NUM_EQ; ARITH_RULE `3 <= p ==> ~(p = 0)`] THEN
363 DISJ1_TAC THEN MATCH_MP_TAC PRIME_COPRIME_LT THEN
364 ASM_REWRITE_TAC[] THEN ASM_ARITH_TAC;
365 REWRITE_TAC[GSYM INT_EXISTS_POS] THEN MATCH_MP_TAC MONO_EXISTS THEN
366 GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP (INTEGER_RULE
367 `(x:int == &1 - y) (mod n) ==> coprime(n,y + x)`)) THEN
368 ASM_SIMP_TAC[INT_OF_NUM_SUB; INT_OF_NUM_POW; INT_OF_NUM_MUL;
369 INT_OF_NUM_ADD; GSYM num_coprime;
370 ARITH_RULE `3 <= p ==> 1 <= p`] THEN
371 REWRITE_TAC[MULT_ASSOC]];
373 EXISTS_TAC `g + p * x:num` THEN X_GEN_TAC `j:num` THEN DISCH_TAC THEN
374 STRIP_ASSUME_TAC(ISPECL [`p EXP j`; `g + p * x:num`] ORDER_WORKS) THEN
375 MP_TAC(SPECL [`p:num`; `g + p * x:num`; `order (p EXP j) (g + p * x)`]
377 SUBGOAL_THEN `order p (g + p * x) = p - 1` SUBST1_TAC THENL
378 [ASM_MESON_TAC[ORDER_CONG; NUMBER_RULE `(g:num == g + p * x) (mod p)`];
380 MATCH_MP_TAC(TAUT `a /\ (b ==> c) ==> (a <=> b) ==> c`) THEN CONJ_TAC THENL
381 [MATCH_MP_TAC(NUMBER_RULE
382 `!y. (a == 1) (mod y) /\ x divides y ==> (a == 1) (mod x)`) THEN
383 EXISTS_TAC `p EXP j` THEN ASM_REWRITE_TAC[] THEN
384 ASM_SIMP_TAC[DIVIDES_REFL; DIVIDES_REXP; LE_1];
385 REWRITE_TAC[divides; LEFT_IMP_EXISTS_THM] THEN X_GEN_TAC `d:num` THEN
386 DISCH_THEN(fun th -> SUBST_ALL_TAC th THEN ASSUME_TAC th)] THEN
387 MP_TAC(ISPECL [`g + p * x:num`; `p EXP j`] ORDER_DIVIDES_PHI) THEN
388 ASM_SIMP_TAC[PHI_PRIMEPOW; LE_1; COPRIME_LEXP] THEN ANTS_TAC THENL
389 [REWRITE_TAC[NUMBER_RULE `coprime(p,g + p * x) <=> coprime(g,p)`] THEN
390 MATCH_MP_TAC PRIME_COPRIME_LT THEN
391 ASM_REWRITE_TAC[] THEN ASM_ARITH_TAC;
393 SUBGOAL_THEN `p EXP j - p EXP (j - 1) = (p - 1) * p EXP (j - 1)`
395 [UNDISCH_TAC `1 <= j` THEN SPEC_TAC(`j:num`,`j:num`) THEN
396 INDUCT_TAC THEN REWRITE_TAC[ARITH; SUC_SUB1] THEN
397 REWRITE_TAC[EXP; RIGHT_SUB_DISTRIB] THEN ARITH_TAC;
399 DISCH_THEN(MP_TAC o MATCH_MP (NUMBER_RULE
400 `(a * x:num) divides (a * y) ==> ~(a = 0) ==> x divides y`)) THEN
401 ASM_SIMP_TAC[DIVIDES_PRIMEPOW; ARITH_RULE `3 <= p ==> ~(p - 1 = 0)`] THEN
402 DISCH_THEN(X_CHOOSE_THEN `k:num`
403 (CONJUNCTS_THEN2 ASSUME_TAC SUBST_ALL_TAC)) THEN
404 AP_TERM_TAC THEN AP_TERM_TAC THEN
405 SUBGOAL_THEN `?z. (g + p * x) EXP (p - 1) = 1 + z * p /\ coprime(z,p)`
406 STRIP_ASSUME_TAC THENL
407 [REWRITE_TAC[BINOMIAL_THEOREM] THEN
408 ASM_SIMP_TAC[NSUM_CLAUSES_RIGHT; LE_0; ARITH_RULE
409 `3 <= p ==> 0 < p - 1`] THEN
410 REWRITE_TAC[BINOM_REFL; SUB_REFL; EXP; MULT_CLAUSES] THEN
412 `y + nsum(0..p-2) (\k. binom(p - 1,k) * g EXP k *
413 p EXP (p - 2 - k) * x EXP (p - 1 - k))` THEN
414 REWRITE_TAC[ARITH_RULE `n - 1 - 1 = n - 2`] THEN
415 SIMP_TAC[ARITH_RULE `s + 1 + y * p = 1 + (y + t) * p <=> s = p * t`] THEN
417 [REWRITE_TAC[GSYM NSUM_LMUL] THEN MATCH_MP_TAC NSUM_EQ THEN
418 X_GEN_TAC `i:num` THEN REWRITE_TAC[IN_NUMSEG] THEN STRIP_TAC THEN
419 SIMP_TAC[ARITH_RULE `p * b * g * pp * x:num = b * g * (p * pp) * x`] THEN
420 AP_TERM_TAC THEN AP_TERM_TAC THEN REWRITE_TAC[MULT_EXP] THEN
421 REWRITE_TAC[GSYM(CONJUNCT2 EXP)] THEN
422 AP_THM_TAC THEN AP_TERM_TAC THEN AP_TERM_TAC THEN ASM_ARITH_TAC;
424 ASM_SIMP_TAC[NSUM_CLAUSES_RIGHT; LE_0; ARITH_RULE
425 `3 <= p ==> 0 < p - 2`] THEN
426 REWRITE_TAC[BINOM_REFL; SUB_REFL; EXP; MULT_CLAUSES] THEN
427 ASM_SIMP_TAC[EXP_1; ARITH_RULE `3 <= p ==> p - 1 - (p - 2) = 1`] THEN
428 SUBGOAL_THEN `binom(p - 1,p - 2) = p - 1` SUBST1_TAC THENL
429 [SUBGOAL_THEN `p - 1 = SUC(p - 2)` SUBST1_TAC THENL
430 [ASM_ARITH_TAC; REWRITE_TAC[BINOM_PENULT]];
432 MATCH_MP_TAC(NUMBER_RULE
433 `coprime(p:num,y + x) /\ p divides z ==> coprime(y + z + x,p)`) THEN
434 ASM_REWRITE_TAC[] THEN MATCH_MP_TAC NSUM_CLOSED THEN
435 REWRITE_TAC[DIVIDES_0; DIVIDES_ADD; IN_NUMSEG] THEN
436 X_GEN_TAC `i:num` THEN STRIP_TAC THEN
437 REPLICATE_TAC 2 (MATCH_MP_TAC DIVIDES_LMUL) THEN
438 MATCH_MP_TAC DIVIDES_RMUL THEN MATCH_MP_TAC DIVIDES_REXP THEN
439 REWRITE_TAC[DIVIDES_REFL] THEN ASM_ARITH_TAC;
442 `?w. (g + p * x) EXP ((p - 1) * p EXP k) = 1 + p EXP (k + 1) * w /\
444 STRIP_ASSUME_TAC THENL
445 [ASM_REWRITE_TAC[GSYM EXP_EXP] THEN
446 ONCE_REWRITE_TAC[CONJ_SYM] THEN
447 GEN_REWRITE_TAC (BINDER_CONV o funpow 3 RAND_CONV) [MULT_SYM] THEN
448 MATCH_MP_TAC COPRIME_1_PLUS_POWER THEN ASM_REWRITE_TAC[];
450 `((g + p * x) EXP ((p - 1) * p EXP k) == 1) (mod (p EXP j))` THEN
451 ASM_REWRITE_TAC[NUMBER_RULE `(1 + x == 1) (mod n) <=> n divides x`] THEN
452 ONCE_REWRITE_TAC[MULT_SYM] THEN DISCH_TAC THEN
453 MP_TAC(SPECL [`p:num`; `j:num`; `w:num`; `p EXP (k + 1)`]
454 COPRIME_EXP_DIVPROD) THEN
455 ONCE_REWRITE_TAC[COPRIME_SYM] THEN ASM_REWRITE_TAC[] THEN
456 ASM_SIMP_TAC[DIVIDES_EXP_LE; ARITH_RULE `3 <= p ==> 2 <= p`] THEN
457 UNDISCH_TAC `k <= j - 1` THEN ARITH_TAC]);;
459 let PRIMITIVE_ROOT_MODULO_PRIMEPOW = prove
460 (`!p k. prime p /\ 3 <= p /\ 1 <= k
461 ==> ?x. x IN 1..(p EXP k - 1) /\ order (p EXP k) x = phi(p EXP k)`,
462 REPEAT STRIP_TAC THEN
463 MP_TAC(ISPEC `p:num` PRIMITIVE_ROOT_MODULO_PRIMEPOWS) THEN
464 ASM_REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
465 X_GEN_TAC `x:num` THEN DISCH_THEN(MP_TAC o SPEC `k:num`) THEN
466 ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
467 EXISTS_TAC `x MOD (p EXP k)` THEN CONJ_TAC THENL
468 [REWRITE_TAC[IN_NUMSEG; ARITH_RULE `1 <= x <=> ~(x = 0)`] THEN
470 [MP_TAC(ISPECL [`p EXP k`; `x:num`] DIVIDES_MOD) THEN
471 ASM_SIMP_TAC[EXP_EQ_0; ARITH_RULE `3 <= p ==> ~(p = 0)`] THEN
472 DISCH_THEN(SUBST1_TAC o SYM) THEN DISCH_TAC THEN
473 MP_TAC(ISPECL [`p EXP k`; `x:num`] ORDER) THEN
474 DISCH_THEN(MP_TAC o MATCH_MP (NUMBER_RULE
475 `(x == 1) (mod p) ==> p divides x ==> p divides 1`)) THEN
476 ASM_SIMP_TAC[EXP_EQ_1; DIVIDES_ONE; LE_1] THEN
477 ASM_SIMP_TAC[ARITH_RULE `3 <= p ==> ~(p = 1)`] THEN
478 MATCH_MP_TAC DIVIDES_REXP THEN ASM_REWRITE_TAC[] THEN
479 MATCH_MP_TAC(ARITH_RULE `1 <= p ==> ~(p = 0)`) THEN
480 MATCH_MP_TAC PHI_LOWERBOUND_1_STRONG THEN
481 MATCH_MP_TAC(ARITH_RULE `~(p = 0) ==> 1 <= p`) THEN
482 ASM_SIMP_TAC[EXP_EQ_0] THEN ASM_ARITH_TAC;
483 MATCH_MP_TAC(ARITH_RULE `a < b ==> a <= b - 1`) THEN
484 MP_TAC(ISPECL [`x:num`; `p EXP k`] DIVISION) THEN
485 ASM_SIMP_TAC[EXP_EQ_0; ARITH_RULE `3 <= p ==> ~(p = 0)`]];
486 MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC `order (p EXP k) x` THEN
487 CONJ_TAC THENL [ALL_TAC; ASM_REWRITE_TAC[]] THEN
488 MATCH_MP_TAC ORDER_CONG THEN MATCH_MP_TAC CONG_MOD THEN
489 ASM_SIMP_TAC[EXP_EQ_0; ARITH_RULE `3 <= p ==> ~(p = 0)`]]);;
491 (* ------------------------------------------------------------------------- *)
492 (* Double prime powers and the other remaining positive cases 2 and 4. *)
493 (* ------------------------------------------------------------------------- *)
495 let PRIMITIVE_ROOT_MODULO_2 = prove
496 (`?x. x IN 1..1 /\ order 2 x = phi(2)`,
497 EXISTS_TAC `1` THEN REWRITE_TAC[IN_NUMSEG; ARITH] THEN
498 SIMP_TAC[PHI_PRIME; PRIME_2] THEN CONV_TAC NUM_REDUCE_CONV THEN
499 MATCH_MP_TAC ORDER_UNIQUE THEN
500 REWRITE_TAC[ARITH_RULE `~(0 < m /\ m < 1)`] THEN
501 CONV_TAC NUM_REDUCE_CONV THEN CONV_TAC(ONCE_DEPTH_CONV CONG_CONV) THEN
504 let PRIMITIVE_ROOT_MODULO_4 = prove
505 (`?x. x IN 1..3 /\ order 4 x = phi(4)`,
506 EXISTS_TAC `3` THEN REWRITE_TAC[IN_NUMSEG; ARITH] THEN
507 SUBST1_TAC(ARITH_RULE `4 = 2 EXP 2`) THEN
508 SIMP_TAC[PHI_PRIMEPOW; PRIME_2] THEN CONV_TAC NUM_REDUCE_CONV THEN
509 MATCH_MP_TAC ORDER_UNIQUE THEN
510 REWRITE_TAC[FORALL_UNWIND_THM2; ARITH_RULE `0 < m /\ m < 2 <=> m = 1`] THEN
511 CONV_TAC NUM_REDUCE_CONV THEN CONV_TAC(ONCE_DEPTH_CONV CONG_CONV) THEN
514 let PRIMITIVE_ROOT_DOUBLE_LEMMA = prove
515 (`!n a. ODD n /\ ODD a /\ order n a = phi n
516 ==> order (2 * n) a = phi(2 * n)`,
517 REPEAT STRIP_TAC THEN MATCH_MP_TAC ORDER_UNIQUE THEN
518 ASM_SIMP_TAC[CONG_CHINESE_EQ; COPRIME_2; PHI_MULTIPLICATIVE] THEN
519 REWRITE_TAC[PHI_2; MULT_CLAUSES] THEN REPEAT CONJ_TAC THENL
520 [ASM_MESON_TAC[ODD; LE_1; PHI_LOWERBOUND_1_STRONG];
521 ASM_REWRITE_TAC[GSYM ODD_MOD_2; ODD_EXP];
522 ASM_MESON_TAC[ORDER_WORKS];
523 ASM_MESON_TAC[ORDER_WORKS]]);;
525 let PRIMITIVE_ROOT_MODULO_DOUBLE_PRIMEPOW = prove
526 (`!p k. prime p /\ 3 <= p /\ 1 <= k
527 ==> ?x. x IN 1..(2 * p EXP k - 1) /\
528 order (2 * p EXP k) x = phi(2 * p EXP k)`,
529 REPEAT GEN_TAC THEN DISCH_TAC THEN MP_TAC(SPEC `p:num` PRIME_ODD) THEN
530 ASM_SIMP_TAC[ARITH_RULE `3 <= p ==> ~(p = 2)`] THEN DISCH_TAC THEN
531 FIRST_ASSUM(MP_TAC o MATCH_MP PRIMITIVE_ROOT_MODULO_PRIMEPOW) THEN
532 DISCH_THEN(X_CHOOSE_THEN `g:num` MP_TAC) THEN REWRITE_TAC[IN_NUMSEG] THEN
533 STRIP_TAC THEN DISJ_CASES_TAC (SPEC `g:num` EVEN_OR_ODD) THENL
534 [EXISTS_TAC `g + p EXP k` THEN CONJ_TAC THENL
535 [CONJ_TAC THENL [ASM_ARITH_TAC; ALL_TAC] THEN
536 MATCH_MP_TAC(ARITH_RULE
537 `g <= x - 1 /\ p EXP 1 <= x ==> g + p <= 2 * x - 1`) THEN
538 ASM_REWRITE_TAC[LE_EXP] THEN ASM_ARITH_TAC;
540 EXISTS_TAC `g:num` THEN CONJ_TAC THENL [ASM_ARITH_TAC; ALL_TAC]] THEN
541 MATCH_MP_TAC PRIMITIVE_ROOT_DOUBLE_LEMMA THEN
542 ASM_REWRITE_TAC[ODD_ADD; ODD_EXP; NOT_ODD] THEN
543 FIRST_X_ASSUM(SUBST1_TAC o SYM) THEN MATCH_MP_TAC ORDER_CONG THEN
544 CONV_TAC NUMBER_RULE);;
546 (* ------------------------------------------------------------------------- *)
547 (* A couple of degenerate case not usually considered. *)
548 (* ------------------------------------------------------------------------- *)
550 let PRIMITIVE_ROOT_MODULO_0 = prove
551 (`(?x. order 0 x = phi(0))`,
552 EXISTS_TAC `2` THEN REWRITE_TAC[PHI_0; ORDER_EQ_0; COPRIME_2; ODD]);;
554 let PRIMITIVE_ROOT_MODULO_1 = prove
555 (`?x. order 1 x = phi(1)`,
556 EXISTS_TAC `1` THEN REWRITE_TAC[PHI_1] THEN MATCH_MP_TAC ORDER_UNIQUE THEN
557 REWRITE_TAC[ARITH_RULE `0 < m /\ m < 1 <=> F`; EXP_1; CONG_REFL] THEN
560 (* ------------------------------------------------------------------------- *)
561 (* The negative results. *)
562 (* ------------------------------------------------------------------------- *)
564 let CONG_TO_1_POW2 = prove
565 (`!k x. ODD x /\ 1 <= k ==> (x EXP (2 EXP k) == 1) (mod (2 EXP (k + 2)))`,
566 INDUCT_TAC THEN REWRITE_TAC[ADD_CLAUSES; EXP] THEN
567 CONV_TAC NUM_REDUCE_CONV THEN GEN_TAC THEN ASM_CASES_TAC `k = 0` THENL
568 [ASM_REWRITE_TAC[] THEN CONV_TAC NUM_REDUCE_CONV THEN
569 SIMP_TAC[ODD_EXISTS; LEFT_IMP_EXISTS_THM] THEN
570 REPEAT STRIP_TAC THEN REWRITE_TAC[CONG_TO_1] THEN DISJ2_TAC THEN
571 REWRITE_TAC[GSYM EVEN_EXISTS; ARITH_RULE
572 `SUC(2 * m) EXP 2 = 1 + q * 8 <=> m * (m + 1) = 2 * q`] THEN
573 REWRITE_TAC[EVEN_MULT; EVEN_ADD; ARITH] THEN CONV_TAC TAUT;
574 STRIP_TAC THEN FIRST_X_ASSUM(MP_TAC o SPEC `x:num`) THEN
575 ASM_SIMP_TAC[ONCE_REWRITE_RULE[MULT_SYM] EXP_MULT; LE_1] THEN
576 REWRITE_TAC[CONG_TO_1; EXP_EQ_1; ADD_EQ_0; MULT_EQ_1] THEN
577 CONV_TAC NUM_REDUCE_CONV THEN
578 DISCH_THEN(X_CHOOSE_THEN `m:num` SUBST1_TAC) THEN
579 REWRITE_TAC[EQ_MULT_LCANCEL; EXP_EQ_0; ARITH; GSYM EVEN_EXISTS; ARITH_RULE
580 `(1 + m * n) EXP 2 = 1 + q * 2 * n <=>
581 n * m * (2 + m * n) = n * 2 * q`] THEN
582 REWRITE_TAC[EVEN_MULT; EVEN_ADD; EVEN_EXP; ARITH] THEN ARITH_TAC]);;
584 let NO_PRIMITIVE_ROOT_MODULO_POW2 = prove
585 (`!k. 3 <= k ==> ~(?x. order (2 EXP k) x = phi(2 EXP k))`,
586 REPEAT STRIP_TAC THEN DISJ_CASES_TAC(SPEC `x:num` EVEN_OR_ODD) THENL
587 [FIRST_X_ASSUM(MP_TAC o MATCH_MP (ARITH_RULE
588 `a = b ==> 1 <= b /\ a = 0 ==> F`)) THEN
589 ASM_SIMP_TAC[ORDER_EQ_0; PHI_LOWERBOUND_1_STRONG; LE_1; EXP_EQ_0; ARITH;
590 COPRIME_LEXP; COPRIME_2; DE_MORGAN_THM; NOT_ODD] THEN
592 MP_TAC(CONJUNCT2(ISPECL [`2 EXP k`; `x:num`] ORDER_WORKS)) THEN
593 ASM_REWRITE_TAC[] THEN
594 DISCH_THEN(MP_TAC o SPEC `2 EXP (k - 2)`) THEN
595 ASM_SIMP_TAC[PHI_PRIMEPOW; PRIME_2; ARITH_RULE `3 <= k ==> ~(k = 0)`] THEN
596 ABBREV_TAC `j = k - 2` THEN
597 SUBGOAL_THEN `k - 1 = j + 1` SUBST1_TAC THENL [ASM_ARITH_TAC; ALL_TAC] THEN
598 SUBGOAL_THEN `k = j + 2` SUBST1_TAC THENL [ASM_ARITH_TAC; ALL_TAC] THEN
599 SUBGOAL_THEN `1 <= j` ASSUME_TAC THENL [ASM_ARITH_TAC; ALL_TAC] THEN
600 ASM_SIMP_TAC[CONG_TO_1_POW2; ARITH_RULE `0 < x <=> ~(x = 0)`] THEN
601 REWRITE_TAC[EXP_EQ_0; ARITH] THEN
602 MATCH_MP_TAC(ARITH_RULE `a + b:num < c ==> a < c - b`) THEN
603 REWRITE_TAC[EXP_ADD] THEN CONV_TAC NUM_REDUCE_CONV THEN
604 REWRITE_TAC[ARITH_RULE `x + x * 2 < x * 4 <=> ~(x = 0)`] THEN
605 REWRITE_TAC[EXP_EQ_0; ARITH]]);;
607 let NO_PRIMITIVE_ROOT_MODULO_COMPOSITE = prove
608 (`!a b. 3 <= a /\ 3 <= b /\ coprime(a,b)
609 ==> ~(?x. order (a * b) x = phi(a * b))`,
610 SIMP_TAC[PHI_MULTIPLICATIVE] THEN REPEAT STRIP_TAC THEN
611 MP_TAC(SPECL [`a * b:num`; `x:num`] ORDER_WORKS) THEN
612 ASM_SIMP_TAC[CONG_CHINESE_EQ] THEN STRIP_TAC THEN
613 FIRST_X_ASSUM(MP_TAC o SPEC `(phi a * phi b) DIV 2`) THEN
614 REWRITE_TAC[ARITH_RULE `0 < a DIV 2 /\ a DIV 2 < a <=> 2 <= a`; NOT_IMP] THEN
615 REPEAT CONJ_TAC THENL
616 [MATCH_MP_TAC(ARITH_RULE `2 * 2 <= x ==> 2 <= x`) THEN
617 MATCH_MP_TAC LE_MULT2 THEN ASM_SIMP_TAC[PHI_LOWERBOUND_2];
618 SUBGOAL_THEN `EVEN(phi b)` MP_TAC THENL
619 [ASM_SIMP_TAC[EVEN_PHI]; SIMP_TAC[EVEN_EXISTS; LEFT_IMP_EXISTS_THM]] THEN
620 REWRITE_TAC[ARITH_RULE `(a * 2 * b) DIV 2 = a * b`];
621 SUBGOAL_THEN `EVEN(phi a)` MP_TAC THENL
622 [ASM_SIMP_TAC[EVEN_PHI]; SIMP_TAC[EVEN_EXISTS; LEFT_IMP_EXISTS_THM]] THEN
623 REWRITE_TAC[ARITH_RULE `((2 * a) * b) DIV 2 = b * a`]] THEN
624 X_GEN_TAC `m:num` THEN DISCH_THEN SUBST1_TAC THEN
625 ASM_REWRITE_TAC[GSYM EXP_EXP] THEN SUBST1_TAC(SYM(SPEC `m:num` EXP_ONE)) THEN
626 MATCH_MP_TAC CONG_EXP THEN MATCH_MP_TAC FERMAT_LITTLE THEN
627 MP_TAC(ISPECL [`a * b:num`; `x:num`] ORDER_EQ_0) THEN
628 ASM_SIMP_TAC[MULT_EQ_0; LE_1; PHI_LOWERBOUND_1_STRONG;
629 ARITH_RULE `3 <= p ==> 1 <= p`] THEN
630 CONV_TAC NUMBER_RULE);;
632 (* ------------------------------------------------------------------------- *)
633 (* Equivalences, one with some degenerate cases, one more conventional. *)
634 (* ------------------------------------------------------------------------- *)
636 let PRIMITIVE_ROOT_EXISTS = prove
637 (`!n. (?x. order n x = phi n) <=>
638 n = 0 \/ n = 2 \/ n = 4 \/
639 ?p k. prime p /\ 3 <= p /\ (n = p EXP k \/ n = 2 * p EXP k)`,
641 ASM_CASES_TAC `n = 0` THEN ASM_REWRITE_TAC[PRIMITIVE_ROOT_MODULO_0] THEN
642 ASM_CASES_TAC `n = 2` THENL
643 [ASM_MESON_TAC[PRIMITIVE_ROOT_MODULO_2]; ALL_TAC] THEN
644 ASM_CASES_TAC `n = 4` THENL
645 [ASM_MESON_TAC[PRIMITIVE_ROOT_MODULO_4]; ALL_TAC] THEN
646 ASM_REWRITE_TAC[] THEN ASM_CASES_TAC `n = 1` THENL
647 [ASM_REWRITE_TAC[PRIMITIVE_ROOT_MODULO_1] THEN
648 MAP_EVERY EXISTS_TAC [`3`; `0`] THEN
649 CONV_TAC(ONCE_DEPTH_CONV PRIME_CONV) THEN CONV_TAC NUM_REDUCE_CONV;
653 REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
654 MAP_EVERY X_GEN_TAC [`p:num`; `k:num`] THEN
655 ASM_CASES_TAC `k = 0` THEN ASM_REWRITE_TAC[EXP; MULT_CLAUSES] THEN
656 STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
657 ASM_MESON_TAC[LE_1; PRIMITIVE_ROOT_MODULO_PRIMEPOW;
658 PRIMITIVE_ROOT_MODULO_DOUBLE_PRIMEPOW]] THEN
659 ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN
660 REWRITE_TAC[NOT_EXISTS_THM; TAUT `~(a /\ b /\ c) <=> a /\ b ==> ~c`] THEN
661 REWRITE_TAC[DE_MORGAN_THM] THEN STRIP_TAC THEN
662 MP_TAC(ISPEC `n:num` PRIMEPOW_FACTOR) THEN
663 ANTS_TAC THENL [ASM_ARITH_TAC; REWRITE_TAC[LEFT_IMP_EXISTS_THM]] THEN
664 MAP_EVERY X_GEN_TAC [`p:num`; `k:num`; `m:num`] THEN
665 ASM_CASES_TAC `m = 0` THEN ASM_REWRITE_TAC[MULT_CLAUSES] THEN
666 ASM_CASES_TAC `m = 1` THENL
667 [ASM_REWRITE_TAC[MULT_CLAUSES] THEN
668 REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
669 DISCH_THEN SUBST_ALL_TAC THEN
670 FIRST_X_ASSUM(MP_TAC o SPECL [`p:num`; `k:num`]) THEN
671 ASM_SIMP_TAC[PRIME_GE_2; ARITH_RULE
672 `2 <= p ==> (~(3 <= p) <=> p = 2)`] THEN
673 DISCH_THEN SUBST_ALL_TAC THEN ASM_CASES_TAC `3 <= k` THENL
674 [ASM_MESON_TAC[NO_PRIMITIVE_ROOT_MODULO_POW2]; ALL_TAC] THEN
675 FIRST_X_ASSUM(MP_TAC o MATCH_MP (ARITH_RULE
676 `~(3 <= k) ==> 1 <= k ==> k = 1 \/ k = 2`)) THEN
677 ASM_REWRITE_TAC[] THEN DISCH_THEN(DISJ_CASES_THEN SUBST_ALL_TAC) THEN
678 REPEAT(POP_ASSUM MP_TAC) THEN CONV_TAC NUM_REDUCE_CONV;
680 ASM_CASES_TAC `m = 2` THENL
681 [ASM_REWRITE_TAC[COPRIME_2] THEN
682 ASM_CASES_TAC `p = 2` THEN ASM_REWRITE_TAC[ARITH] THEN
683 STRIP_TAC THEN FIRST_ASSUM(ASSUME_TAC o MATCH_MP PRIME_GE_2) THEN
684 SUBGOAL_THEN `3 <= p` ASSUME_TAC THENL [ASM_ARITH_TAC; ALL_TAC] THEN
685 ASM_MESON_TAC[MULT_SYM];
687 STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
688 ASM_CASES_TAC `k = 1` THENL
689 [UNDISCH_THEN `k = 1` SUBST_ALL_TAC;
690 MP_TAC(SPECL [`p EXP k`; `m:num`] NO_PRIMITIVE_ROOT_MODULO_COMPOSITE) THEN
691 REWRITE_TAC[NOT_EXISTS_THM] THEN DISCH_THEN MATCH_MP_TAC THEN
692 ASM_REWRITE_TAC[COPRIME_LEXP] THEN
693 CONJ_TAC THENL [ALL_TAC; ASM_ARITH_TAC] THEN
694 MATCH_MP_TAC(ARITH_RULE `2 EXP 2 <= x ==> 3 <= x`) THEN
695 MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `p EXP 2` THEN
696 ASM_REWRITE_TAC[EXP_MONO_LE; LE_EXP] THEN
697 ASM_SIMP_TAC[PRIME_GE_2; PRIME_IMP_NZ] THEN ASM_ARITH_TAC] THEN
698 ASM_CASES_TAC `p = 2` THENL
699 [UNDISCH_THEN `p = 2` SUBST_ALL_TAC;
700 MP_TAC(SPECL [`p EXP 1`; `m:num`] NO_PRIMITIVE_ROOT_MODULO_COMPOSITE) THEN
701 REWRITE_TAC[NOT_EXISTS_THM] THEN DISCH_THEN MATCH_MP_TAC THEN
702 ASM_REWRITE_TAC[COPRIME_LEXP] THEN REWRITE_TAC[EXP_1] THEN
703 FIRST_ASSUM(MP_TAC o MATCH_MP PRIME_GE_2) THEN ASM_ARITH_TAC] THEN
704 RULE_ASSUM_TAC(REWRITE_RULE[EXP_1]) THEN REWRITE_TAC[EXP_1] THEN
705 MP_TAC(ISPEC `m:num` PRIMEPOW_FACTOR) THEN
706 ANTS_TAC THENL [ASM_ARITH_TAC; REWRITE_TAC[LEFT_IMP_EXISTS_THM]] THEN
707 MAP_EVERY X_GEN_TAC [`q:num`; `j:num`; `r:num`] THEN
708 ASM_CASES_TAC `r = 0` THEN ASM_REWRITE_TAC[MULT_CLAUSES] THEN
709 STRIP_TAC THEN UNDISCH_TAC `coprime(2,m)` THEN
710 ASM_SIMP_TAC[COPRIME_RMUL; COPRIME_REXP; LE_1] THEN
711 REWRITE_TAC[COPRIME_2] THEN STRIP_TAC THEN
712 SUBGOAL_THEN `3 <= q` ASSUME_TAC THENL
713 [MATCH_MP_TAC(ARITH_RULE `~(p = 2) /\ 2 <= p ==> 3 <= p`) THEN
714 ASM_SIMP_TAC[PRIME_GE_2] THEN DISCH_TAC THEN
715 UNDISCH_TAC `ODD q` THEN ASM_REWRITE_TAC[ARITH];
717 FIRST_X_ASSUM(MP_TAC o SPECL [`q:num`; `j:num`]) THEN
718 ASM_CASES_TAC `r = 1` THEN ASM_REWRITE_TAC[MULT_CLAUSES] THEN STRIP_TAC THEN
719 MP_TAC(SPECL [`2 * r`; `q EXP j`] NO_PRIMITIVE_ROOT_MODULO_COMPOSITE) THEN
720 REWRITE_TAC[COPRIME_LMUL; COPRIME_REXP] THEN ASM_REWRITE_TAC[COPRIME_2] THEN
721 ONCE_REWRITE_TAC[COPRIME_SYM] THEN ASM_REWRITE_TAC[] THEN
722 REWRITE_TAC[MULT_AC; NOT_EXISTS_THM] THEN DISCH_THEN MATCH_MP_TAC THEN
723 ASM_REWRITE_TAC[ARITH_RULE `3 <= r * 2 <=> ~(r = 0 \/ r = 1)`] THEN
724 MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `q EXP 1` THEN
725 ASM_REWRITE_TAC[LE_EXP; ARITH; COND_ID] THEN ASM_REWRITE_TAC[EXP_1]);;
727 let PRIMITIVE_ROOT_EXISTS_NONTRIVIAL = prove
728 (`!n. (?x. x IN 1..n-1 /\ order n x = phi n) <=>
730 ?p k. prime p /\ 3 <= p /\ 1 <= k /\ (n = p EXP k \/ n = 2 * p EXP k)`,
731 GEN_TAC THEN ASM_CASES_TAC `n = 0` THENL
732 [ASM_REWRITE_TAC[IN_NUMSEG] THEN CONV_TAC NUM_REDUCE_CONV THEN
733 MATCH_MP_TAC(TAUT `~a /\ ~b ==> (a <=> b)`) THEN
734 CONV_TAC(ONCE_DEPTH_CONV SYM_CONV) THEN
735 REWRITE_TAC[MULT_EQ_0; EXP_EQ_0] THEN ARITH_TAC;
737 ASM_CASES_TAC `n = 1` THENL
738 [ASM_REWRITE_TAC[IN_NUMSEG] THEN CONV_TAC NUM_REDUCE_CONV THEN
739 MATCH_MP_TAC(TAUT `~a /\ ~b ==> (a <=> b)`) THEN
740 CONV_TAC(ONCE_DEPTH_CONV SYM_CONV) THEN
741 REWRITE_TAC[MULT_EQ_1; EXP_EQ_1] THEN ARITH_TAC;
743 MATCH_MP_TAC EQ_TRANS THEN
744 EXISTS_TAC `?x. order n x = phi n` THEN CONJ_TAC THENL
745 [EQ_TAC THENL [MESON_TAC[]; ALL_TAC] THEN
746 DISCH_THEN(X_CHOOSE_TAC `x:num`) THEN EXISTS_TAC `x MOD n` THEN
747 ASM_SIMP_TAC[IN_NUMSEG; DIVISION; ARITH_RULE
748 `~(n = 0) /\ ~(n = 1) ==> (x <= n - 1 <=> x < n)`] THEN
750 [REWRITE_TAC[ARITH_RULE `1 <= x <=> ~(x = 0)`] THEN
751 ASM_SIMP_TAC[GSYM DIVIDES_MOD] THEN DISCH_TAC THEN
752 MP_TAC(SPECL [`n:num`; `x:num`] ORDER_EQ_0) THEN
753 ASM_SIMP_TAC[LE_1; PHI_LOWERBOUND_1_STRONG] THEN
754 REWRITE_TAC[coprime] THEN DISCH_THEN(MP_TAC o SPEC `n:num`) THEN
755 ASM_REWRITE_TAC[DIVIDES_REFL];
756 FIRST_ASSUM(SUBST1_TAC o SYM) THEN MATCH_MP_TAC ORDER_CONG THEN
757 ASM_SIMP_TAC[CONG_MOD]];
758 ASM_REWRITE_TAC[PRIMITIVE_ROOT_EXISTS] THEN
759 ASM_CASES_TAC `n = 2` THEN ASM_REWRITE_TAC[] THEN
760 ASM_CASES_TAC `n = 4` THEN ASM_REWRITE_TAC[] THEN
761 AP_TERM_TAC THEN REWRITE_TAC[FUN_EQ_THM] THEN X_GEN_TAC `p:num` THEN
762 AP_TERM_TAC THEN REWRITE_TAC[FUN_EQ_THM] THEN X_GEN_TAC `k:num` THEN
763 CONV_TAC(BINOP_CONV(ONCE_DEPTH_CONV SYM_CONV)) THEN
764 ASM_CASES_TAC `k = 0` THEN ASM_SIMP_TAC[LE_1] THEN
765 AP_TERM_TAC THEN ASM_ARITH_TAC]);;