Library/primitive.ml

   1 (* ========================================================================= *)
   2 (* Existence of primitive roots modulo certain numbers.                      *)
   3 (* ========================================================================= *)
   4
   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";;
  10
  11 (* ------------------------------------------------------------------------- *)
  12 (* Some lemmas connecting concepts in the various background theories.       *)
  13 (* ------------------------------------------------------------------------- *)
  14
  15 let DIVIDES_BINOM_PRIME = prove
  16  (`!n p. prime p /\ 0 < n /\ n < p ==> p divides binom(p,n)`,
  17   REPEAT STRIP_TAC THEN
  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`]);;
  22
  23 let INT_PRIME = prove
  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
  31   ASM_ARITH_TAC);;
  32
  33 (* ------------------------------------------------------------------------- *)
  34 (* Explicit formula for difference of real/integer polynomials.              *)
  35 (* ------------------------------------------------------------------------- *)
  36
  37 let REAL_POLY_DIFF_EXPLICIT = prove
  38  (`!n a x y.
  39         sum(0..n) (\i. a(i) * x pow i) - sum(0..n) (\i. a(i) * y pow i) =
  40         (x - y) *
  41         sum(0..n-1) (\i. sum(i+1..n) (\j. a j * y pow (j - 1 - i)) * x pow i)`,
  42   REPEAT GEN_TAC THEN
  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);;
  55
  56 let INT_POLY_DIFF_EXPLICIT = INT_OF_REAL_THM REAL_POLY_DIFF_EXPLICIT;;
  57
  58 (* ------------------------------------------------------------------------- *)
  59 (* Lagrange's theorem on number of roots modulo a prime.                     *)
  60 (* ------------------------------------------------------------------------- *)
  61
  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}`]);;
  66
  67 let INT_POLY_LAGRANGE = prove
  68  (`!p l r.
  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)}
  73                   <= n`,
  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
  85     CONV_TAC TAUT;
  86     ALL_TAC] 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
  97      (INTEGER_RULE
  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
 104   SUBGOAL_THEN
 105    `{x:int | l <= x /\ x <= r /\ p divides (x - c)} = {c}`
 106   SUBST1_TAC THENL
 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;
 114     ALL_TAC] THEN
 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]);;
 126
 127 (* ------------------------------------------------------------------------- *)
 128 (* Laborious instantiation to (x^d == 1) (mod p) over natural numbers.       *)
 129 (* ------------------------------------------------------------------------- *)
 130
 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
 136   ANTS_TAC THENL
 137    [ASM_SIMP_TAC[INT_PRIME; INT_LT_SUB_RADD; INT_OF_NUM_ADD; INT_OF_NUM_LT] THEN
 138     ARITH_TAC;
 139     ALL_TAC] 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];
 146     ALL_TAC] THEN
 147   REWRITE_TAC[MESON[]
 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`;
 154                ARITH_RULE `1 <= d
 155                            ==> (((0 <= i /\ i <= d) /\ ~(i = d)) /\ i = 0 <=>
 156                                 i = 0)`] THEN
 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]);;
 166
 167 (* ------------------------------------------------------------------------- *)
 168 (* Count of elements with a given order modulo a prime.                      *)
 169 (* ------------------------------------------------------------------------- *)
 170
 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)`,
 174   let lemma = prove
 175    (`!s f g:A->num.
 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
 185   CONJ_TAC THENL
 186    [ALL_TAC;
 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
 195     ASM_ARITH_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
 209     ASM_ARITH_TAC;
 210     ALL_TAC] THEN
 211   SUBGOAL_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}`
 214   MP_TAC THENL
 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];
 261       EXPAND_TAC "d" THEN
 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]]);;
 267
 268 (* ------------------------------------------------------------------------- *)
 269 (* In particular, primitive roots modulo a prime.                            *)
 270 (* ------------------------------------------------------------------------- *)
 271
 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]);;
 277
 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);;
 288
 289 (* ------------------------------------------------------------------------- *)
 290 (* Now primitive roots modulo odd prime powers.                              *)
 291 (* ------------------------------------------------------------------------- *)
 292
 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
 303   SUBGOAL_THEN
 304    `(p EXP (k + 2)) divides (nsum(2..p) (\i. binom(p,i) * (z * p EXP k) EXP i))`
 305   MP_TAC THENL
 306    [ALL_TAC;
 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
 327       ASM_ARITH_TAC;
 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]]]]);;
 331
 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]);;
 345
 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
 359     ANTS_TAC THENL
 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]];
 372     ALL_TAC] THEN
 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)`]
 376       ORDER_DIVIDES) THEN
 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)`];
 379     ALL_TAC] THEN
 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;
 392     ALL_TAC] THEN
 393   SUBGOAL_THEN `p EXP j - p EXP (j - 1) = (p - 1) * p EXP (j - 1)`
 394   SUBST1_TAC THENL
 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;
 398     ALL_TAC] THEN
 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
 411     EXISTS_TAC
 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
 416     CONJ_TAC THENL
 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;
 423       ALL_TAC] THEN
 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]];
 431       ALL_TAC] THEN
 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;
 440     ALL_TAC] THEN
 441   SUBGOAL_THEN
 442    `?w. (g + p * x) EXP ((p - 1) * p EXP k) = 1 + p EXP (k + 1) * w /\
 443         coprime(w,p)`
 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[];
 449     UNDISCH_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]);;
 458
 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
 469     CONJ_TAC THENL
 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)`]]);;
 490
 491 (* ------------------------------------------------------------------------- *)
 492 (* Double prime powers and the other remaining positive cases 2 and 4.       *)
 493 (* ------------------------------------------------------------------------- *)
 494
 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
 502   REWRITE_TAC[]);;
 503
 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
 512   REWRITE_TAC[]);;
 513
 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]]);;
 524
 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;
 539       ALL_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);;
 545
 546 (* ------------------------------------------------------------------------- *)
 547 (* A couple of degenerate case not usually considered.                       *)
 548 (* ------------------------------------------------------------------------- *)
 549
 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]);;
 553
 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
 558   ARITH_TAC);;
 559
 560 (* ------------------------------------------------------------------------- *)
 561 (* The negative results.                                                     *)
 562 (* ------------------------------------------------------------------------- *)
 563
 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]);;
 583
 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
 591     ASM_ARITH_TAC;
 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]]);;
 606
 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);;
 631
 632 (* ------------------------------------------------------------------------- *)
 633 (* Equivalences, one with some degenerate cases, one more conventional.      *)
 634 (* ------------------------------------------------------------------------- *)
 635
 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)`,
 640   GEN_TAC THEN
 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;
 650     ALL_TAC] THEN
 651   EQ_TAC THENL
 652    [ALL_TAC;
 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;
 679     ALL_TAC] THEN
 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];
 686     ALL_TAC] THEN
 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];
 716     ALL_TAC] THEN
 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]);;
 726
 727 let PRIMITIVE_ROOT_EXISTS_NONTRIVIAL = prove
 728  (`!n. (?x. x IN 1..n-1 /\ order n x = phi n) <=>
 729        n = 2 \/ n = 4 \/
 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;
 736     ALL_TAC] THEN
 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;
 742     ALL_TAC] THEN
 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
 749     CONJ_TAC THENL
 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]);;