(* ========================================================================= *)
(* Existence of primitive roots modulo certain numbers.                      *)
(* ========================================================================= *)

needs "Library/integer.ml";;
needs "Library/isum.ml";;
needs "Library/binomial.ml";;
needs "Library/pocklington.ml";;
needs "Library/multiplicative.ml";;

(* ------------------------------------------------------------------------- *)
(* Some lemmas connecting concepts in the various background theories.       *)
(* ------------------------------------------------------------------------- *)

let DIVIDES_BINOM_PRIME = 
prove (`!n p. prime p /\ 0 < n /\ n < p ==> p divides binom(p,n)`,
REPEAT STRIP_TAC THEN MP_TAC(AP_TERM `(divides) p` (SPECL [`p - n:num`; `n:num`] BINOM_FACT)) THEN ASM_SIMP_TAC[DIVIDES_FACT_PRIME; PRIME_DIVPROD_EQ; SUB_ADD; LT_IMP_LE] THEN ASM_REWRITE_TAC[GSYM NOT_LT; LT_REFL] THEN ASM_SIMP_TAC[ARITH_RULE `0 < n /\ n < p ==> p - n < p`]);;
let INT_PRIME = 
prove (`!p. int_prime(&p) <=> prime p`,
GEN_TAC THEN REWRITE_TAC[prime; int_prime] THEN ONCE_REWRITE_TAC[GSYM INT_DIVIDES_LABS] THEN REWRITE_TAC[GSYM INT_FORALL_ABS; GSYM num_divides; INT_ABS_NUM] THEN REWRITE_TAC[INT_OF_NUM_GT; INT_OF_NUM_EQ] THEN ASM_CASES_TAC `p = 0` THENL [ASM_REWRITE_TAC[ARITH; DIVIDES_0] THEN DISCH_THEN(MP_TAC o SPEC `2`); AP_THM_TAC THEN AP_TERM_TAC] THEN ASM_ARITH_TAC);;
(* ------------------------------------------------------------------------- *) (* Explicit formula for difference of real/integer polynomials. *) (* ------------------------------------------------------------------------- *)
let REAL_POLY_DIFF_EXPLICIT = 
prove (`!n a x y. sum(0..n) (\i. a(i) * x pow i) - sum(0..n) (\i. a(i) * y pow i) = (x - y) * sum(0..n-1) (\i. sum(i+1..n) (\j. a j * y pow (j - 1 - i)) * x pow i)`,
REPEAT GEN_TAC THEN REWRITE_TAC[GSYM SUM_SUB_NUMSEG; GSYM REAL_SUB_LDISTRIB] THEN MP_TAC(ISPEC `n:num` LE_0) THEN SIMP_TAC[SUM_CLAUSES_LEFT; ADD_CLAUSES] THEN DISCH_THEN(K ALL_TAC) THEN REWRITE_TAC[REAL_SUB_REFL; REAL_MUL_RZERO; REAL_ADD_LID; real_pow] THEN SIMP_TAC[REAL_SUB_POW] THEN ONCE_REWRITE_TAC[REAL_ARITH `a * b * c:real = b * a * c`] THEN REWRITE_TAC[SUM_LMUL] THEN AP_TERM_TAC THEN SIMP_TAC[GSYM SUM_LMUL; GSYM SUM_RMUL; SUM_SUM_PRODUCT; FINITE_NUMSEG] THEN MATCH_MP_TAC SUM_EQ_GENERAL_INVERSES THEN REPEAT(EXISTS_TAC `\(a:num,b:num). (b,a)`) THEN REWRITE_TAC[IN_ELIM_PAIR_THM; FORALL_PAIR_THM; REAL_MUL_AC] THEN REWRITE_TAC[IN_NUMSEG] THEN ARITH_TAC);;
let INT_POLY_DIFF_EXPLICIT = INT_OF_REAL_THM REAL_POLY_DIFF_EXPLICIT;;
(* ------------------------------------------------------------------------- *) (* Lagrange's theorem on number of roots modulo a prime. *) (* ------------------------------------------------------------------------- *)
let FINITE_INTSEG_RESTRICT = 
prove (`!P a b. FINITE {x:int | a <= x /\ x <= b /\ P x}`,
SIMP_TAC[FINITE_RESTRICT; FINITE_INTSEG; SET_RULE `{x | P x /\ Q x /\ R x} = {x | x IN {x | P x /\ Q x} /\ R x}`]);;
let INT_POLY_LAGRANGE = 
prove (`!p l r. int_prime p /\ r - l < p ==> !n a. ~(!i. i <= n ==> (a i == &0) (mod p)) ==> CARD {x | l <= x /\ x <= r /\ (isum(0..n) (\i. a(i) * x pow i) == &0) (mod p)} <= n`,
REPEAT GEN_TAC THEN STRIP_TAC THEN REWRITE_TAC[INT_CONG_0_DIVIDES] THEN MATCH_MP_TAC num_WF THEN REPEAT STRIP_TAC THEN MATCH_MP_TAC(MESON[] `!a. (~(s = a) ==> CARD s <= n) /\ CARD a <= n ==> CARD s <= n`) THEN EXISTS_TAC `{}:int->bool` THEN REWRITE_TAC[LE_0; CARD_CLAUSES] THEN REWRITE_TAC[GSYM MEMBER_NOT_EMPTY; LEFT_IMP_EXISTS_THM; IN_ELIM_THM] THEN X_GEN_TAC `c:int` THEN STRIP_TAC THEN ASM_CASES_TAC `n = 0` THENL [MAP_EVERY UNDISCH_TAC [`~(!i:num. i <= n ==> (p:int) divides (a i))`; `p divides (isum (0..n) (\i. a i * c pow i))`] THEN ASM_SIMP_TAC[CONJUNCT1 LE; ISUM_CLAUSES_NUMSEG] THEN REWRITE_TAC[INT_POW; LEFT_FORALL_IMP_THM; EXISTS_REFL; INT_MUL_RID] THEN CONV_TAC TAUT; ALL_TAC] THEN ASM_CASES_TAC `p divides ((a:num->int) n)` THENL [ASM_SIMP_TAC[ISUM_CLAUSES_RIGHT; LE_0; LE_1] THEN ASM_SIMP_TAC[INTEGER_RULE `(p:int) divides y ==> (p divides (x + y * z) <=> p divides x)`] THEN MATCH_MP_TAC(ARITH_RULE `x <= n - 1 ==> x <= n`) THEN FIRST_X_ASSUM(MP_TAC o SPEC `n - 1`) THEN ASM_REWRITE_TAC[ARITH_RULE `n - 1 < n <=> ~(n = 0)`] THEN DISCH_THEN MATCH_MP_TAC THEN ASM_MESON_TAC[ARITH_RULE `i <= n <=> i <= n - 1 \/ i = n`]; ALL_TAC] THEN MP_TAC(GEN `x:int` (MATCH_MP (INTEGER_RULE `a - b:int = c ==> p divides b ==> (p divides a <=> p divides c)`) (ISPECL [`n:num`; `a:num->int`; `x:int`; `c:int`] INT_POLY_DIFF_EXPLICIT))) THEN ASM_SIMP_TAC[INT_PRIME_DIVPROD_EQ] THEN DISCH_THEN(K ALL_TAC) THEN ASM_REWRITE_TAC[LEFT_OR_DISTRIB; SET_RULE `{x | q x \/ r x} = {x | q x} UNION {x | r x}`] THEN SUBGOAL_THEN `{x:int | l <= x /\ x <= r /\ p divides (x - c)} = {c}` SUBST1_TAC THENL [MATCH_MP_TAC(SET_RULE `P c /\ (!x y. P x /\ P y ==> x = y) ==> {x | P x} = {c}`) THEN ASM_REWRITE_TAC[INT_SUB_REFL; INT_DIVIDES_0] THEN MAP_EVERY X_GEN_TAC [`u:int`; `v:int`] THEN STRIP_TAC THEN SUBGOAL_THEN `p divides (u - v:int)` MP_TAC THENL [ASM_MESON_TAC[INT_CONG; INT_CONG_SYM; INT_CONG_TRANS]; ALL_TAC] THEN DISCH_THEN(MP_TAC o MATCH_MP INT_DIVIDES_LE) THEN ASM_INT_ARITH_TAC; ALL_TAC] THEN REWRITE_TAC[SET_RULE `{a} UNION s = a INSERT s`] THEN SIMP_TAC[CARD_CLAUSES; FINITE_INTSEG_RESTRICT] THEN MATCH_MP_TAC(ARITH_RULE `~(n = 0) /\ x <= n - 1 ==> (if p then x else SUC x) <= n`) THEN ASM_REWRITE_TAC[] THEN RULE_ASSUM_TAC(REWRITE_RULE[RIGHT_IMP_FORALL_THM; IMP_IMP]) THEN FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[ARITH_RULE `n - 1 < n <=> ~(n = 0)`] THEN DISCH_THEN(MP_TAC o SPEC `n - 1`) THEN ASM_SIMP_TAC[LE_REFL; SUB_ADD; LE_1; ISUM_SING_NUMSEG; SUB_REFL] THEN ASM_REWRITE_TAC[INT_POW; INT_MUL_RID]);;
(* ------------------------------------------------------------------------- *) (* Laborious instantiation to (x^d == 1) (mod p) over natural numbers. *) (* ------------------------------------------------------------------------- *)
let NUM_LAGRANGE_LEMMA = 
prove (`!p d. prime p /\ 1 <= d ==> CARD {x | x IN 1..p-1 /\ (x EXP d == 1) (mod p)} <= d`,
REPEAT STRIP_TAC THEN MP_TAC(ISPECL [`&p:int`; `&1:int`; `&(p-1):int`] INT_POLY_LAGRANGE) THEN ANTS_TAC THENL [ASM_SIMP_TAC[INT_PRIME; INT_LT_SUB_RADD; INT_OF_NUM_ADD; INT_OF_NUM_LT] THEN ARITH_TAC; ALL_TAC] THEN DISCH_THEN(MP_TAC o SPECL [`d:num`; `\i. if i = d then &1 else if i = 0 then -- &1 else &0:int`]) THEN REWRITE_TAC[] THEN ANTS_TAC THENL [DISCH_THEN(MP_TAC o SPEC `d:num`) THEN REWRITE_TAC[LE_REFL] THEN REWRITE_TAC[INT_CONG_0_DIVIDES; GSYM num_divides; DIVIDES_ONE] THEN ASM_MESON_TAC[PRIME_1]; ALL_TAC] THEN REWRITE_TAC[MESON[] `(if p then x else y) * z:int = if p then x * z else y * z`] THEN SIMP_TAC[ISUM_CASES; FINITE_NUMSEG; FINITE_RESTRICT] THEN REWRITE_TAC[INT_POW; INT_MUL_LZERO; ISUM_0; INT_ADD_RID] THEN MATCH_MP_TAC(ARITH_RULE `x:num <= y ==> y <= d ==> x <= d`) THEN REWRITE_TAC[IN_ELIM_THM; IN_NUMSEG] THEN ASM_SIMP_TAC[ARITH_RULE `(0 <= i /\ i <= d) /\ i = d <=> i = d`; ARITH_RULE `1 <= d ==> (((0 <= i /\ i <= d) /\ ~(i = d)) /\ i = 0 <=> i = 0)`] THEN REWRITE_TAC[SING_GSPEC; ISUM_SING] THEN REWRITE_TAC[INT_ARITH `&1 * x + -- &1 * &1:int = x - &1`] THEN REWRITE_TAC[INTEGER_RULE `(x - a:int == &0) (mod p) <=> (x == a) (mod p)`] THEN MATCH_MP_TAC CARD_SUBSET_IMAGE THEN EXISTS_TAC `num_of_int` THEN REWRITE_TAC[FINITE_INTSEG_RESTRICT; SUBSET; IN_IMAGE; IN_ELIM_THM] THEN X_GEN_TAC `n:num` THEN DISCH_TAC THEN EXISTS_TAC `&n:int` THEN ASM_REWRITE_TAC[NUM_OF_INT_OF_NUM; INT_OF_NUM_LE; INT_OF_NUM_POW] THEN ASM_REWRITE_TAC[GSYM num_congruent]);;
(* ------------------------------------------------------------------------- *) (* Count of elements with a given order modulo a prime. *) (* ------------------------------------------------------------------------- *)
let COUNT_ORDERS_MODULO_PRIME = 
prove (`!p d. prime p /\ d divides (p - 1) ==> CARD {x | x IN 1..p-1 /\ order p x = d} = phi(d)`,
let lemma = prove
   (`!s f g:A->num.
          FINITE s /\ (!x. x IN s ==> f(x) <= g(x)) /\ nsum s f = nsum s g
          ==> !x. x IN s ==> f x = g x`,
    REWRITE_TAC[GSYM LE_ANTISYM] THEN MESON_TAC[NSUM_LE; NSUM_LT; NOT_LE]) in
  REWRITE_TAC[IMP_CONJ; RIGHT_FORALL_IMP_THM] THEN GEN_TAC THEN DISCH_TAC THEN
  ONCE_REWRITE_TAC[SET_RULE
   `(!x. p x ==> q x) <=> (!x. x IN {x | p x} ==> q x)`] THEN
  MATCH_MP_TAC lemma THEN SUBGOAL_THEN `~(p - 1 = 0)` ASSUME_TAC THENL
   [FIRST_ASSUM(MP_TAC o MATCH_MP PRIME_GE_2) THEN ARITH_TAC; ALL_TAC] THEN
  ASM_SIMP_TAC[REWRITE_RULE[ETA_AX] PHI_DIVISORSUM; FINITE_DIVISORS] THEN
  CONJ_TAC THENL
   [ALL_TAC;
    SIMP_TAC[CARD_EQ_NSUM; FINITE_RESTRICT; FINITE_NUMSEG] THEN
    W(MP_TAC o PART_MATCH (lhs o rand) NSUM_GROUP o lhs o snd) THEN
    REWRITE_TAC[NSUM_CONST_NUMSEG; FINITE_NUMSEG; ADD_SUB; MULT_CLAUSES] THEN
    DISCH_THEN MATCH_MP_TAC THEN
    REWRITE_TAC[SUBSET; FORALL_IN_IMAGE; IN_ELIM_THM; IN_NUMSEG] THEN
    X_GEN_TAC `x:num` THEN STRIP_TAC THEN ASM_SIMP_TAC[GSYM PHI_PRIME] THEN
    MATCH_MP_TAC ORDER_DIVIDES_PHI THEN ONCE_REWRITE_TAC[COPRIME_SYM] THEN
    MATCH_MP_TAC PRIME_COPRIME_LT THEN ASM_REWRITE_TAC[] THEN
    ASM_ARITH_TAC] THEN
  X_GEN_TAC `d:num` THEN REWRITE_TAC[IN_ELIM_THM] THEN DISCH_TAC THEN
  ASM_CASES_TAC `{x | x IN 1..p-1 /\ order p x = d} = {}` THEN
  ASM_REWRITE_TAC[CARD_CLAUSES; LE_0] THEN
  FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [GSYM MEMBER_NOT_EMPTY]) THEN
  REWRITE_TAC[IN_ELIM_THM; LEFT_IMP_EXISTS_THM] THEN X_GEN_TAC `a:num` THEN
  REWRITE_TAC[IN_NUMSEG] THEN STRIP_TAC THEN REWRITE_TAC[PHI_ALT] THEN
  MATCH_MP_TAC CARD_SUBSET_IMAGE THEN EXISTS_TAC `\m. (a EXP m) MOD p` THEN
  REWRITE_TAC[PHI_FINITE_LEMMA] THEN
  SUBGOAL_THEN `1 <= d` ASSUME_TAC THENL
   [ASM_MESON_TAC[LE_1; DIVIDES_ZERO]; ALL_TAC] THEN
  SUBGOAL_THEN `coprime(p,a)` ASSUME_TAC THENL
   [ONCE_REWRITE_TAC[COPRIME_SYM] THEN
    MATCH_MP_TAC PRIME_COPRIME_LT THEN ASM_REWRITE_TAC[] THEN
    ASM_ARITH_TAC;
    ALL_TAC] THEN
  SUBGOAL_THEN
   `{x | x IN 1..p-1 /\ (x EXP d == 1) (mod p)} =
    IMAGE (\m. (a EXP m) MOD p) {m | m < d}`
  MP_TAC THENL
   [CONV_TAC SYM_CONV THEN MATCH_MP_TAC CARD_SUBSET_LE THEN
    SIMP_TAC[FINITE_RESTRICT; FINITE_NUMSEG] THEN CONJ_TAC THENL
     [REWRITE_TAC[SUBSET; FORALL_IN_IMAGE; IN_ELIM_THM] THEN
      X_GEN_TAC `m:num` THEN DISCH_TAC THEN REWRITE_TAC[IN_NUMSEG] THEN
      ASM_SIMP_TAC[ARITH_RULE `~(p - 1 = 0) ==> (x <= p - 1 <=> x < p)`] THEN
      ASM_SIMP_TAC[DIVISION; PRIME_IMP_NZ] THEN CONJ_TAC THENL
       [REWRITE_TAC[ARITH_RULE `1 <= x <=> ~(x = 0)`] THEN
        ASM_SIMP_TAC[GSYM DIVIDES_MOD; PRIME_IMP_NZ] THEN
        ASM_MESON_TAC[PRIME_DIVEXP; PRIME_COPRIME_EQ];
        ASM_SIMP_TAC[CONG; PRIME_IMP_NZ; MOD_EXP_MOD] THEN
        REWRITE_TAC[EXP_EXP] THEN ONCE_REWRITE_TAC[MULT_SYM] THEN
        REWRITE_TAC[GSYM EXP_EXP] THEN
        SUBST1_TAC(SYM(SPEC `m:num` EXP_ONE)) THEN
        ASM_SIMP_TAC[GSYM CONG; PRIME_IMP_NZ] THEN
        MATCH_MP_TAC CONG_EXP THEN ASM_MESON_TAC[ORDER]];
      MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `d:num` THEN
      ASM_SIMP_TAC[NUM_LAGRANGE_LEMMA] THEN
      GEN_REWRITE_TAC LAND_CONV [GSYM CARD_NUMSEG_LT] THEN
      MATCH_MP_TAC EQ_IMP_LE THEN CONV_TAC SYM_CONV THEN
      MATCH_MP_TAC CARD_IMAGE_INJ THEN
      ASM_SIMP_TAC[GSYM CONG; PRIME_IMP_NZ; FINITE_NUMSEG_LT; IN_ELIM_THM] THEN
      ASM_SIMP_TAC[ORDER_DIVIDES_EXPDIFF] THEN REWRITE_TAC[CONG_IMP_EQ]];
    MATCH_MP_TAC(SET_RULE
     `s' SUBSET s /\ (!x. x IN t /\ f x IN s' ==> x IN t')
      ==> s = IMAGE f t ==> s' SUBSET IMAGE f t'`) THEN
    SIMP_TAC[SUBSET; IN_ELIM_THM; IN_NUMSEG] THEN
    CONJ_TAC THENL [MESON_TAC[ORDER]; ALL_TAC] THEN
    X_GEN_TAC `m:num` THEN ABBREV_TAC `b = (a EXP m) MOD p` THEN STRIP_TAC THEN
    REWRITE_TAC[coprime; divides] THEN X_GEN_TAC `e:num` THEN
    DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_THEN `m':num` (ASSUME_TAC o SYM))
                              (X_CHOOSE_THEN `d':num` (ASSUME_TAC o SYM))) THEN
    MP_TAC(ISPECL [`p:num`; `b:num`] ORDER_WORKS) THEN
    DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC (MP_TAC o SPEC `d':num`)) THEN
    ASM_REWRITE_TAC[] THEN
    MATCH_MP_TAC(TAUT `a /\ c /\ (~b ==> d) ==> (a /\ b ==> ~c) ==> d`) THEN
    REPEAT CONJ_TAC THENL
     [UNDISCH_TAC `1 <= d` THEN EXPAND_TAC "d" THEN
      REWRITE_TAC[ARITH_RULE `1 <= d <=> ~(d = 0)`; MULT_EQ_0] THEN
      SIMP_TAC[DE_MORGAN_THM; ARITH_RULE `0 < d <=> ~(d = 0)`];
      EXPAND_TAC "b" THEN ASM_SIMP_TAC[CONG; PRIME_IMP_NZ; MOD_EXP_MOD] THEN
      EXPAND_TAC "m" THEN REWRITE_TAC[EXP_EXP] THEN
      ONCE_REWRITE_TAC[ARITH_RULE `(e * m') * d':num = (e * d') * m'`] THEN
      ASM_REWRITE_TAC[] THEN REWRITE_TAC[GSYM EXP_EXP] THEN
      SUBST1_TAC(SYM(SPEC `m':num` EXP_ONE)) THEN
      ASM_SIMP_TAC[GSYM CONG; PRIME_IMP_NZ] THEN
      MATCH_MP_TAC CONG_EXP THEN ASM_MESON_TAC[ORDER];
      EXPAND_TAC "d" THEN
      REWRITE_TAC[ARITH_RULE `~(d < e * d) <=> e * d <= 1 * d`] THEN
      REWRITE_TAC[LE_MULT_RCANCEL] THEN
      REWRITE_TAC[ARITH_RULE `e <= 1 <=> e = 0 \/ e = 1`] THEN
      STRIP_TAC THEN UNDISCH_TAC `e * d':num = d` THEN
      ASM_REWRITE_TAC[] THEN ASM_ARITH_TAC]]);;
(* ------------------------------------------------------------------------- *) (* In particular, primitive roots modulo a prime. *) (* ------------------------------------------------------------------------- *)
let PRIMITIVE_ROOTS_MODULO_PRIME = 
prove (`!p. prime p ==> CARD {x | x IN 1..p-1 /\ order p x = p - 1} = phi(p - 1)`,
REPEAT STRIP_TAC THEN MP_TAC(ISPECL [`p:num`; `p - 1`] COUNT_ORDERS_MODULO_PRIME) THEN ASM_REWRITE_TAC[DIVIDES_REFL]);;
let PRIMITIVE_ROOT_MODULO_PRIME = 
prove (`!p. prime p ==> ?x. x IN 1..p-1 /\ order p x = p - 1`,
REPEAT STRIP_TAC THEN FIRST_ASSUM(MP_TAC o MATCH_MP PRIMITIVE_ROOTS_MODULO_PRIME) THEN ASM_CASES_TAC `{x | x IN 1..p-1 /\ order p x = p - 1} = {}` THENL [ASM_REWRITE_TAC[CARD_CLAUSES]; ASM SET_TAC[]] THEN ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN DISCH_THEN(K ALL_TAC) THEN MATCH_MP_TAC(ARITH_RULE `1 <= p ==> ~(0 = p)`) THEN MATCH_MP_TAC PHI_LOWERBOUND_1_STRONG THEN FIRST_X_ASSUM(MP_TAC o MATCH_MP PRIME_GE_2) THEN ARITH_TAC);;
(* ------------------------------------------------------------------------- *) (* Now primitive roots modulo odd prime powers. *) (* ------------------------------------------------------------------------- *)
let COPRIME_1_PLUS_POWER_STEP = 
prove (`!p z k. prime p /\ coprime(z,p) /\ 3 <= p /\ 1 <= k ==> ?w. coprime(w,p) /\ (1 + z * p EXP k) EXP p = 1 + w * p EXP (k + 1)`,
REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[ARITH_RULE `1 + a * b = a * b + 1`] THEN REWRITE_TAC[BINOMIAL_THEOREM; EXP_ONE; MULT_CLAUSES] THEN SIMP_TAC[NSUM_CLAUSES_LEFT; LE_0; EXP; binom; MULT_CLAUSES; ADD_CLAUSES] THEN SUBGOAL_THEN `1 <= p` MP_TAC THENL [ASM_ARITH_TAC; ALL_TAC] THEN SIMP_TAC[NSUM_CLAUSES_LEFT; BINOM_1; EXP_1; ARITH] THEN DISCH_TAC THEN SUBGOAL_THEN `(p EXP (k + 2)) divides (nsum(2..p) (\i. binom(p,i) * (z * p EXP k) EXP i))` MP_TAC THENL [ALL_TAC; REWRITE_TAC[divides; LEFT_IMP_EXISTS_THM] THEN X_GEN_TAC `d:num` THEN DISCH_THEN SUBST1_TAC THEN EXISTS_TAC `z + p * d:num` THEN ASM_REWRITE_TAC[NUMBER_RULE `coprime(z + p * d:num,p) <=> coprime(z,p)`] THEN REWRITE_TAC[EXP_ADD] THEN ARITH_TAC] THEN MATCH_MP_TAC NSUM_CLOSED THEN REWRITE_TAC[DIVIDES_0; DIVIDES_ADD; IN_NUMSEG] THEN X_GEN_TAC `j:num` THEN STRIP_TAC THEN REWRITE_TAC[MULT_EXP] THEN ONCE_REWRITE_TAC[ARITH_RULE `a * b * c:num = b * c * a`] THEN REWRITE_TAC[EXP_EXP] THEN MATCH_MP_TAC DIVIDES_LMUL THEN ASM_CASES_TAC `j:num = p` THENL [MATCH_MP_TAC DIVIDES_RMUL THEN ASM_SIMP_TAC[DIVIDES_EXP_LE; ARITH_RULE `3 <= p ==> 2 <= p`] THEN MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `k * 3` THEN CONJ_TAC THENL [ASM_ARITH_TAC; ASM_REWRITE_TAC[LE_MULT_LCANCEL]]; ONCE_REWRITE_TAC[MULT_SYM] THEN REWRITE_TAC[EXP; ARITH_RULE `k + 2 = SUC(k + 1)`] THEN MATCH_MP_TAC DIVIDES_MUL2 THEN CONJ_TAC THENL [MATCH_MP_TAC DIVIDES_BINOM_PRIME THEN ASM_REWRITE_TAC[] THEN ASM_ARITH_TAC; ASM_SIMP_TAC[DIVIDES_EXP_LE; ARITH_RULE `3 <= p ==> 2 <= p`] THEN MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `k * 2` THEN CONJ_TAC THENL [ASM_ARITH_TAC; ASM_REWRITE_TAC[LE_MULT_LCANCEL]]]]);;
let COPRIME_1_PLUS_POWER = 
prove (`!p z k. prime p /\ coprime(z,p) /\ 3 <= p ==> ?w. coprime(w,p) /\ (1 + z * p) EXP (p EXP k) = 1 + w * p EXP (k + 1)`,
GEN_TAC THEN GEN_TAC THEN INDUCT_TAC THEN REWRITE_TAC[ADD_CLAUSES; EXP_1; EXP] THENL [MESON_TAC[]; ALL_TAC] THEN REWRITE_TAC[GSYM(ONCE_REWRITE_RULE[MULT_SYM] EXP_EXP)] THEN DISCH_THEN(fun th -> POP_ASSUM MP_TAC THEN STRIP_ASSUME_TAC th) THEN ASM_REWRITE_TAC[] THEN DISCH_THEN(X_CHOOSE_THEN `w:num` STRIP_ASSUME_TAC) THEN MP_TAC(ISPECL [`p:num`; `w:num`; `k + 1`] COPRIME_1_PLUS_POWER_STEP) THEN ASM_REWRITE_TAC[ARITH_RULE `1 <= k + 1`] THEN REWRITE_TAC[EXP_ADD; EXP_1; MULT_AC]);;
let PRIMITIVE_ROOT_MODULO_PRIMEPOWS = 
prove (`!p. prime p /\ 3 <= p ==> ?g. !j. 1 <= j ==> order(p EXP j) g = phi(p EXP j)`,
REPEAT STRIP_TAC THEN FIRST_ASSUM(MP_TAC o MATCH_MP PRIMITIVE_ROOT_MODULO_PRIME) THEN REWRITE_TAC[IN_NUMSEG] THEN DISCH_THEN(X_CHOOSE_THEN `g:num` STRIP_ASSUME_TAC) THEN MP_TAC(ISPECL [`p:num`; `g:num`] ORDER) THEN ASM_SIMP_TAC[CONG_TO_1; EXP_EQ_0; LE_1] THEN DISCH_THEN(X_CHOOSE_THEN `y:num` STRIP_ASSUME_TAC) THEN SUBGOAL_THEN `?x. coprime(p,y + (p - 1) * g EXP (p - 2) * x)` CHOOSE_TAC THENL [MP_TAC(ISPECL [`(&p - &1:int) * &g pow (p - 2)`; `&1 - &y:int`; `&p:int`] INT_CONG_SOLVE_POS) THEN ANTS_TAC THENL [REWRITE_TAC[INT_COPRIME_LMUL; INT_COPRIME_LPOW] THEN REWRITE_TAC[INTEGER_RULE `coprime(p - &1,p)`; GSYM num_coprime] THEN ASM_SIMP_TAC[INT_OF_NUM_EQ; ARITH_RULE `3 <= p ==> ~(p = 0)`] THEN DISJ1_TAC THEN MATCH_MP_TAC PRIME_COPRIME_LT THEN ASM_REWRITE_TAC[] THEN ASM_ARITH_TAC; REWRITE_TAC[GSYM INT_EXISTS_POS] THEN MATCH_MP_TAC MONO_EXISTS THEN GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP (INTEGER_RULE `(x:int == &1 - y) (mod n) ==> coprime(n,y + x)`)) THEN ASM_SIMP_TAC[INT_OF_NUM_SUB; INT_OF_NUM_POW; INT_OF_NUM_MUL; INT_OF_NUM_ADD; GSYM num_coprime; ARITH_RULE `3 <= p ==> 1 <= p`] THEN REWRITE_TAC[MULT_ASSOC]]; ALL_TAC] THEN EXISTS_TAC `g + p * x:num` THEN X_GEN_TAC `j:num` THEN DISCH_TAC THEN STRIP_ASSUME_TAC(ISPECL [`p EXP j`; `g + p * x:num`] ORDER_WORKS) THEN MP_TAC(SPECL [`p:num`; `g + p * x:num`; `order (p EXP j) (g + p * x)`] ORDER_DIVIDES) THEN SUBGOAL_THEN `order p (g + p * x) = p - 1` SUBST1_TAC THENL [ASM_MESON_TAC[ORDER_CONG; NUMBER_RULE `(g:num == g + p * x) (mod p)`]; ALL_TAC] THEN MATCH_MP_TAC(TAUT `a /\ (b ==> c) ==> (a <=> b) ==> c`) THEN CONJ_TAC THENL [MATCH_MP_TAC(NUMBER_RULE `!y. (a == 1) (mod y) /\ x divides y ==> (a == 1) (mod x)`) THEN EXISTS_TAC `p EXP j` THEN ASM_REWRITE_TAC[] THEN ASM_SIMP_TAC[DIVIDES_REFL; DIVIDES_REXP; LE_1]; REWRITE_TAC[divides; LEFT_IMP_EXISTS_THM] THEN X_GEN_TAC `d:num` THEN DISCH_THEN(fun th -> SUBST_ALL_TAC th THEN ASSUME_TAC th)] THEN MP_TAC(ISPECL [`g + p * x:num`; `p EXP j`] ORDER_DIVIDES_PHI) THEN ASM_SIMP_TAC[PHI_PRIMEPOW; LE_1; COPRIME_LEXP] THEN ANTS_TAC THENL [REWRITE_TAC[NUMBER_RULE `coprime(p,g + p * x) <=> coprime(g,p)`] THEN MATCH_MP_TAC PRIME_COPRIME_LT THEN ASM_REWRITE_TAC[] THEN ASM_ARITH_TAC; ALL_TAC] THEN SUBGOAL_THEN `p EXP j - p EXP (j - 1) = (p - 1) * p EXP (j - 1)` SUBST1_TAC THENL [UNDISCH_TAC `1 <= j` THEN SPEC_TAC(`j:num`,`j:num`) THEN INDUCT_TAC THEN REWRITE_TAC[ARITH; SUC_SUB1] THEN REWRITE_TAC[EXP; RIGHT_SUB_DISTRIB] THEN ARITH_TAC; ALL_TAC] THEN DISCH_THEN(MP_TAC o MATCH_MP (NUMBER_RULE `(a * x:num) divides (a * y) ==> ~(a = 0) ==> x divides y`)) THEN ASM_SIMP_TAC[DIVIDES_PRIMEPOW; ARITH_RULE `3 <= p ==> ~(p - 1 = 0)`] THEN DISCH_THEN(X_CHOOSE_THEN `k:num` (CONJUNCTS_THEN2 ASSUME_TAC SUBST_ALL_TAC)) THEN AP_TERM_TAC THEN AP_TERM_TAC THEN SUBGOAL_THEN `?z. (g + p * x) EXP (p - 1) = 1 + z * p /\ coprime(z,p)` STRIP_ASSUME_TAC THENL [REWRITE_TAC[BINOMIAL_THEOREM] THEN ASM_SIMP_TAC[NSUM_CLAUSES_RIGHT; LE_0; ARITH_RULE `3 <= p ==> 0 < p - 1`] THEN REWRITE_TAC[BINOM_REFL; SUB_REFL; EXP; MULT_CLAUSES] THEN EXISTS_TAC `y + nsum(0..p-2) (\k. binom(p - 1,k) * g EXP k * p EXP (p - 2 - k) * x EXP (p - 1 - k))` THEN REWRITE_TAC[ARITH_RULE `n - 1 - 1 = n - 2`] THEN SIMP_TAC[ARITH_RULE `s + 1 + y * p = 1 + (y + t) * p <=> s = p * t`] THEN CONJ_TAC THENL [REWRITE_TAC[GSYM NSUM_LMUL] THEN MATCH_MP_TAC NSUM_EQ THEN X_GEN_TAC `i:num` THEN REWRITE_TAC[IN_NUMSEG] THEN STRIP_TAC THEN SIMP_TAC[ARITH_RULE `p * b * g * pp * x:num = b * g * (p * pp) * x`] THEN AP_TERM_TAC THEN AP_TERM_TAC THEN REWRITE_TAC[MULT_EXP] THEN REWRITE_TAC[GSYM(CONJUNCT2 EXP)] THEN AP_THM_TAC THEN AP_TERM_TAC THEN AP_TERM_TAC THEN ASM_ARITH_TAC; ALL_TAC] THEN ASM_SIMP_TAC[NSUM_CLAUSES_RIGHT; LE_0; ARITH_RULE `3 <= p ==> 0 < p - 2`] THEN REWRITE_TAC[BINOM_REFL; SUB_REFL; EXP; MULT_CLAUSES] THEN ASM_SIMP_TAC[EXP_1; ARITH_RULE `3 <= p ==> p - 1 - (p - 2) = 1`] THEN SUBGOAL_THEN `binom(p - 1,p - 2) = p - 1` SUBST1_TAC THENL [SUBGOAL_THEN `p - 1 = SUC(p - 2)` SUBST1_TAC THENL [ASM_ARITH_TAC; REWRITE_TAC[BINOM_PENULT]]; ALL_TAC] THEN MATCH_MP_TAC(NUMBER_RULE `coprime(p:num,y + x) /\ p divides z ==> coprime(y + z + x,p)`) THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC NSUM_CLOSED THEN REWRITE_TAC[DIVIDES_0; DIVIDES_ADD; IN_NUMSEG] THEN X_GEN_TAC `i:num` THEN STRIP_TAC THEN REPLICATE_TAC 2 (MATCH_MP_TAC DIVIDES_LMUL) THEN MATCH_MP_TAC DIVIDES_RMUL THEN MATCH_MP_TAC DIVIDES_REXP THEN REWRITE_TAC[DIVIDES_REFL] THEN ASM_ARITH_TAC; ALL_TAC] THEN SUBGOAL_THEN `?w. (g + p * x) EXP ((p - 1) * p EXP k) = 1 + p EXP (k + 1) * w /\ coprime(w,p)` STRIP_ASSUME_TAC THENL [ASM_REWRITE_TAC[GSYM EXP_EXP] THEN ONCE_REWRITE_TAC[CONJ_SYM] THEN GEN_REWRITE_TAC (BINDER_CONV o funpow 3 RAND_CONV) [MULT_SYM] THEN MATCH_MP_TAC COPRIME_1_PLUS_POWER THEN ASM_REWRITE_TAC[]; UNDISCH_TAC `((g + p * x) EXP ((p - 1) * p EXP k) == 1) (mod (p EXP j))` THEN ASM_REWRITE_TAC[NUMBER_RULE `(1 + x == 1) (mod n) <=> n divides x`] THEN ONCE_REWRITE_TAC[MULT_SYM] THEN DISCH_TAC THEN MP_TAC(SPECL [`p:num`; `j:num`; `w:num`; `p EXP (k + 1)`] COPRIME_EXP_DIVPROD) THEN ONCE_REWRITE_TAC[COPRIME_SYM] THEN ASM_REWRITE_TAC[] THEN ASM_SIMP_TAC[DIVIDES_EXP_LE; ARITH_RULE `3 <= p ==> 2 <= p`] THEN UNDISCH_TAC `k <= j - 1` THEN ARITH_TAC]);;
let PRIMITIVE_ROOT_MODULO_PRIMEPOW = 
prove (`!p k. prime p /\ 3 <= p /\ 1 <= k ==> ?x. x IN 1..(p EXP k - 1) /\ order (p EXP k) x = phi(p EXP k)`,
REPEAT STRIP_TAC THEN MP_TAC(ISPEC `p:num` PRIMITIVE_ROOT_MODULO_PRIMEPOWS) THEN ASM_REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN X_GEN_TAC `x:num` THEN DISCH_THEN(MP_TAC o SPEC `k:num`) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN EXISTS_TAC `x MOD (p EXP k)` THEN CONJ_TAC THENL [REWRITE_TAC[IN_NUMSEG; ARITH_RULE `1 <= x <=> ~(x = 0)`] THEN CONJ_TAC THENL [MP_TAC(ISPECL [`p EXP k`; `x:num`] DIVIDES_MOD) THEN ASM_SIMP_TAC[EXP_EQ_0; ARITH_RULE `3 <= p ==> ~(p = 0)`] THEN DISCH_THEN(SUBST1_TAC o SYM) THEN DISCH_TAC THEN MP_TAC(ISPECL [`p EXP k`; `x:num`] ORDER) THEN DISCH_THEN(MP_TAC o MATCH_MP (NUMBER_RULE `(x == 1) (mod p) ==> p divides x ==> p divides 1`)) THEN ASM_SIMP_TAC[EXP_EQ_1; DIVIDES_ONE; LE_1] THEN ASM_SIMP_TAC[ARITH_RULE `3 <= p ==> ~(p = 1)`] THEN MATCH_MP_TAC DIVIDES_REXP THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC(ARITH_RULE `1 <= p ==> ~(p = 0)`) THEN MATCH_MP_TAC PHI_LOWERBOUND_1_STRONG THEN MATCH_MP_TAC(ARITH_RULE `~(p = 0) ==> 1 <= p`) THEN ASM_SIMP_TAC[EXP_EQ_0] THEN ASM_ARITH_TAC; MATCH_MP_TAC(ARITH_RULE `a < b ==> a <= b - 1`) THEN MP_TAC(ISPECL [`x:num`; `p EXP k`] DIVISION) THEN ASM_SIMP_TAC[EXP_EQ_0; ARITH_RULE `3 <= p ==> ~(p = 0)`]]; MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC `order (p EXP k) x` THEN CONJ_TAC THENL [ALL_TAC; ASM_REWRITE_TAC[]] THEN MATCH_MP_TAC ORDER_CONG THEN MATCH_MP_TAC CONG_MOD THEN ASM_SIMP_TAC[EXP_EQ_0; ARITH_RULE `3 <= p ==> ~(p = 0)`]]);;
(* ------------------------------------------------------------------------- *) (* Double prime powers and the other remaining positive cases 2 and 4. *) (* ------------------------------------------------------------------------- *)
let PRIMITIVE_ROOT_MODULO_2 = 
prove (`?x. x IN 1..1 /\ order 2 x = phi(2)`,
EXISTS_TAC `1` THEN REWRITE_TAC[IN_NUMSEG; ARITH] THEN SIMP_TAC[PHI_PRIME; PRIME_2] THEN CONV_TAC NUM_REDUCE_CONV THEN MATCH_MP_TAC ORDER_UNIQUE THEN REWRITE_TAC[ARITH_RULE `~(0 < m /\ m < 1)`] THEN CONV_TAC NUM_REDUCE_CONV THEN CONV_TAC(ONCE_DEPTH_CONV CONG_CONV) THEN REWRITE_TAC[]);;
let PRIMITIVE_ROOT_MODULO_4 = 
prove (`?x. x IN 1..3 /\ order 4 x = phi(4)`,
EXISTS_TAC `3` THEN REWRITE_TAC[IN_NUMSEG; ARITH] THEN SUBST1_TAC(ARITH_RULE `4 = 2 EXP 2`) THEN SIMP_TAC[PHI_PRIMEPOW; PRIME_2] THEN CONV_TAC NUM_REDUCE_CONV THEN MATCH_MP_TAC ORDER_UNIQUE THEN REWRITE_TAC[FORALL_UNWIND_THM2; ARITH_RULE `0 < m /\ m < 2 <=> m = 1`] THEN CONV_TAC NUM_REDUCE_CONV THEN CONV_TAC(ONCE_DEPTH_CONV CONG_CONV) THEN REWRITE_TAC[]);;
let PRIMITIVE_ROOT_DOUBLE_LEMMA = 
prove (`!n a. ODD n /\ ODD a /\ order n a = phi n ==> order (2 * n) a = phi(2 * n)`,
REPEAT STRIP_TAC THEN MATCH_MP_TAC ORDER_UNIQUE THEN ASM_SIMP_TAC[CONG_CHINESE_EQ; COPRIME_2; PHI_MULTIPLICATIVE] THEN REWRITE_TAC[PHI_2; MULT_CLAUSES] THEN REPEAT CONJ_TAC THENL [ASM_MESON_TAC[ODD; LE_1; PHI_LOWERBOUND_1_STRONG]; ASM_REWRITE_TAC[GSYM ODD_MOD_2; ODD_EXP]; ASM_MESON_TAC[ORDER_WORKS]; ASM_MESON_TAC[ORDER_WORKS]]);;
let PRIMITIVE_ROOT_MODULO_DOUBLE_PRIMEPOW = 
prove (`!p k. prime p /\ 3 <= p /\ 1 <= k ==> ?x. x IN 1..(2 * p EXP k - 1) /\ order (2 * p EXP k) x = phi(2 * p EXP k)`,
REPEAT GEN_TAC THEN DISCH_TAC THEN MP_TAC(SPEC `p:num` PRIME_ODD) THEN ASM_SIMP_TAC[ARITH_RULE `3 <= p ==> ~(p = 2)`] THEN DISCH_TAC THEN FIRST_ASSUM(MP_TAC o MATCH_MP PRIMITIVE_ROOT_MODULO_PRIMEPOW) THEN DISCH_THEN(X_CHOOSE_THEN `g:num` MP_TAC) THEN REWRITE_TAC[IN_NUMSEG] THEN STRIP_TAC THEN DISJ_CASES_TAC (SPEC `g:num` EVEN_OR_ODD) THENL [EXISTS_TAC `g + p EXP k` THEN CONJ_TAC THENL [CONJ_TAC THENL [ASM_ARITH_TAC; ALL_TAC] THEN MATCH_MP_TAC(ARITH_RULE `g <= x - 1 /\ p EXP 1 <= x ==> g + p <= 2 * x - 1`) THEN ASM_REWRITE_TAC[LE_EXP] THEN ASM_ARITH_TAC; ALL_TAC]; EXISTS_TAC `g:num` THEN CONJ_TAC THENL [ASM_ARITH_TAC; ALL_TAC]] THEN MATCH_MP_TAC PRIMITIVE_ROOT_DOUBLE_LEMMA THEN ASM_REWRITE_TAC[ODD_ADD; ODD_EXP; NOT_ODD] THEN FIRST_X_ASSUM(SUBST1_TAC o SYM) THEN MATCH_MP_TAC ORDER_CONG THEN CONV_TAC NUMBER_RULE);;
(* ------------------------------------------------------------------------- *) (* A couple of degenerate case not usually considered. *) (* ------------------------------------------------------------------------- *)
let PRIMITIVE_ROOT_MODULO_0 = 
prove (`(?x. order 0 x = phi(0))`,
EXISTS_TAC `2` THEN REWRITE_TAC[PHI_0; ORDER_EQ_0; COPRIME_2; ODD]);;
let PRIMITIVE_ROOT_MODULO_1 = 
prove (`?x. order 1 x = phi(1)`,
EXISTS_TAC `1` THEN REWRITE_TAC[PHI_1] THEN MATCH_MP_TAC ORDER_UNIQUE THEN REWRITE_TAC[ARITH_RULE `0 < m /\ m < 1 <=> F`; EXP_1; CONG_REFL] THEN ARITH_TAC);;
(* ------------------------------------------------------------------------- *) (* The negative results. *) (* ------------------------------------------------------------------------- *)
let CONG_TO_1_POW2 = 
prove (`!k x. ODD x /\ 1 <= k ==> (x EXP (2 EXP k) == 1) (mod (2 EXP (k + 2)))`,
INDUCT_TAC THEN REWRITE_TAC[ADD_CLAUSES; EXP] THEN CONV_TAC NUM_REDUCE_CONV THEN GEN_TAC THEN ASM_CASES_TAC `k = 0` THENL [ASM_REWRITE_TAC[] THEN CONV_TAC NUM_REDUCE_CONV THEN SIMP_TAC[ODD_EXISTS; LEFT_IMP_EXISTS_THM] THEN REPEAT STRIP_TAC THEN REWRITE_TAC[CONG_TO_1] THEN DISJ2_TAC THEN REWRITE_TAC[GSYM EVEN_EXISTS; ARITH_RULE `SUC(2 * m) EXP 2 = 1 + q * 8 <=> m * (m + 1) = 2 * q`] THEN REWRITE_TAC[EVEN_MULT; EVEN_ADD; ARITH] THEN CONV_TAC TAUT; STRIP_TAC THEN FIRST_X_ASSUM(MP_TAC o SPEC `x:num`) THEN ASM_SIMP_TAC[ONCE_REWRITE_RULE[MULT_SYM] EXP_MULT; LE_1] THEN REWRITE_TAC[CONG_TO_1; EXP_EQ_1; ADD_EQ_0; MULT_EQ_1] THEN CONV_TAC NUM_REDUCE_CONV THEN DISCH_THEN(X_CHOOSE_THEN `m:num` SUBST1_TAC) THEN REWRITE_TAC[EQ_MULT_LCANCEL; EXP_EQ_0; ARITH; GSYM EVEN_EXISTS; ARITH_RULE `(1 + m * n) EXP 2 = 1 + q * 2 * n <=> n * m * (2 + m * n) = n * 2 * q`] THEN REWRITE_TAC[EVEN_MULT; EVEN_ADD; EVEN_EXP; ARITH] THEN ARITH_TAC]);;
let NO_PRIMITIVE_ROOT_MODULO_POW2 = 
prove (`!k. 3 <= k ==> ~(?x. order (2 EXP k) x = phi(2 EXP k))`,
REPEAT STRIP_TAC THEN DISJ_CASES_TAC(SPEC `x:num` EVEN_OR_ODD) THENL [FIRST_X_ASSUM(MP_TAC o MATCH_MP (ARITH_RULE `a = b ==> 1 <= b /\ a = 0 ==> F`)) THEN ASM_SIMP_TAC[ORDER_EQ_0; PHI_LOWERBOUND_1_STRONG; LE_1; EXP_EQ_0; ARITH; COPRIME_LEXP; COPRIME_2; DE_MORGAN_THM; NOT_ODD] THEN ASM_ARITH_TAC; MP_TAC(CONJUNCT2(ISPECL [`2 EXP k`; `x:num`] ORDER_WORKS)) THEN ASM_REWRITE_TAC[] THEN DISCH_THEN(MP_TAC o SPEC `2 EXP (k - 2)`) THEN ASM_SIMP_TAC[PHI_PRIMEPOW; PRIME_2; ARITH_RULE `3 <= k ==> ~(k = 0)`] THEN ABBREV_TAC `j = k - 2` THEN SUBGOAL_THEN `k - 1 = j + 1` SUBST1_TAC THENL [ASM_ARITH_TAC; ALL_TAC] THEN SUBGOAL_THEN `k = j + 2` SUBST1_TAC THENL [ASM_ARITH_TAC; ALL_TAC] THEN SUBGOAL_THEN `1 <= j` ASSUME_TAC THENL [ASM_ARITH_TAC; ALL_TAC] THEN ASM_SIMP_TAC[CONG_TO_1_POW2; ARITH_RULE `0 < x <=> ~(x = 0)`] THEN REWRITE_TAC[EXP_EQ_0; ARITH] THEN MATCH_MP_TAC(ARITH_RULE `a + b:num < c ==> a < c - b`) THEN REWRITE_TAC[EXP_ADD] THEN CONV_TAC NUM_REDUCE_CONV THEN REWRITE_TAC[ARITH_RULE `x + x * 2 < x * 4 <=> ~(x = 0)`] THEN REWRITE_TAC[EXP_EQ_0; ARITH]]);;
let NO_PRIMITIVE_ROOT_MODULO_COMPOSITE = 
prove (`!a b. 3 <= a /\ 3 <= b /\ coprime(a,b) ==> ~(?x. order (a * b) x = phi(a * b))`,
SIMP_TAC[PHI_MULTIPLICATIVE] THEN REPEAT STRIP_TAC THEN MP_TAC(SPECL [`a * b:num`; `x:num`] ORDER_WORKS) THEN ASM_SIMP_TAC[CONG_CHINESE_EQ] THEN STRIP_TAC THEN FIRST_X_ASSUM(MP_TAC o SPEC `(phi a * phi b) DIV 2`) THEN REWRITE_TAC[ARITH_RULE `0 < a DIV 2 /\ a DIV 2 < a <=> 2 <= a`; NOT_IMP] THEN REPEAT CONJ_TAC THENL [MATCH_MP_TAC(ARITH_RULE `2 * 2 <= x ==> 2 <= x`) THEN MATCH_MP_TAC LE_MULT2 THEN ASM_SIMP_TAC[PHI_LOWERBOUND_2]; SUBGOAL_THEN `EVEN(phi b)` MP_TAC THENL [ASM_SIMP_TAC[EVEN_PHI]; SIMP_TAC[EVEN_EXISTS; LEFT_IMP_EXISTS_THM]] THEN REWRITE_TAC[ARITH_RULE `(a * 2 * b) DIV 2 = a * b`]; SUBGOAL_THEN `EVEN(phi a)` MP_TAC THENL [ASM_SIMP_TAC[EVEN_PHI]; SIMP_TAC[EVEN_EXISTS; LEFT_IMP_EXISTS_THM]] THEN REWRITE_TAC[ARITH_RULE `((2 * a) * b) DIV 2 = b * a`]] THEN X_GEN_TAC `m:num` THEN DISCH_THEN SUBST1_TAC THEN ASM_REWRITE_TAC[GSYM EXP_EXP] THEN SUBST1_TAC(SYM(SPEC `m:num` EXP_ONE)) THEN MATCH_MP_TAC CONG_EXP THEN MATCH_MP_TAC FERMAT_LITTLE THEN MP_TAC(ISPECL [`a * b:num`; `x:num`] ORDER_EQ_0) THEN ASM_SIMP_TAC[MULT_EQ_0; LE_1; PHI_LOWERBOUND_1_STRONG; ARITH_RULE `3 <= p ==> 1 <= p`] THEN CONV_TAC NUMBER_RULE);;
(* ------------------------------------------------------------------------- *) (* Equivalences, one with some degenerate cases, one more conventional. *) (* ------------------------------------------------------------------------- *)
let PRIMITIVE_ROOT_EXISTS = 
prove (`!n. (?x. order n x = phi n) <=> n = 0 \/ n = 2 \/ n = 4 \/ ?p k. prime p /\ 3 <= p /\ (n = p EXP k \/ n = 2 * p EXP k)`,
GEN_TAC THEN ASM_CASES_TAC `n = 0` THEN ASM_REWRITE_TAC[PRIMITIVE_ROOT_MODULO_0] THEN ASM_CASES_TAC `n = 2` THENL [ASM_MESON_TAC[PRIMITIVE_ROOT_MODULO_2]; ALL_TAC] THEN ASM_CASES_TAC `n = 4` THENL [ASM_MESON_TAC[PRIMITIVE_ROOT_MODULO_4]; ALL_TAC] THEN ASM_REWRITE_TAC[] THEN ASM_CASES_TAC `n = 1` THENL [ASM_REWRITE_TAC[PRIMITIVE_ROOT_MODULO_1] THEN MAP_EVERY EXISTS_TAC [`3`; `0`] THEN CONV_TAC(ONCE_DEPTH_CONV PRIME_CONV) THEN CONV_TAC NUM_REDUCE_CONV; ALL_TAC] THEN EQ_TAC THENL [ALL_TAC; REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN MAP_EVERY X_GEN_TAC [`p:num`; `k:num`] THEN ASM_CASES_TAC `k = 0` THEN ASM_REWRITE_TAC[EXP; MULT_CLAUSES] THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[LE_1; PRIMITIVE_ROOT_MODULO_PRIMEPOW; PRIMITIVE_ROOT_MODULO_DOUBLE_PRIMEPOW]] THEN ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN REWRITE_TAC[NOT_EXISTS_THM; TAUT `~(a /\ b /\ c) <=> a /\ b ==> ~c`] THEN REWRITE_TAC[DE_MORGAN_THM] THEN STRIP_TAC THEN MP_TAC(ISPEC `n:num` PRIMEPOW_FACTOR) THEN ANTS_TAC THENL [ASM_ARITH_TAC; REWRITE_TAC[LEFT_IMP_EXISTS_THM]] THEN MAP_EVERY X_GEN_TAC [`p:num`; `k:num`; `m:num`] THEN ASM_CASES_TAC `m = 0` THEN ASM_REWRITE_TAC[MULT_CLAUSES] THEN ASM_CASES_TAC `m = 1` THENL [ASM_REWRITE_TAC[MULT_CLAUSES] THEN REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN DISCH_THEN SUBST_ALL_TAC THEN FIRST_X_ASSUM(MP_TAC o SPECL [`p:num`; `k:num`]) THEN ASM_SIMP_TAC[PRIME_GE_2; ARITH_RULE `2 <= p ==> (~(3 <= p) <=> p = 2)`] THEN DISCH_THEN SUBST_ALL_TAC THEN ASM_CASES_TAC `3 <= k` THENL [ASM_MESON_TAC[NO_PRIMITIVE_ROOT_MODULO_POW2]; ALL_TAC] THEN FIRST_X_ASSUM(MP_TAC o MATCH_MP (ARITH_RULE `~(3 <= k) ==> 1 <= k ==> k = 1 \/ k = 2`)) THEN ASM_REWRITE_TAC[] THEN DISCH_THEN(DISJ_CASES_THEN SUBST_ALL_TAC) THEN REPEAT(POP_ASSUM MP_TAC) THEN CONV_TAC NUM_REDUCE_CONV; ALL_TAC] THEN ASM_CASES_TAC `m = 2` THENL [ASM_REWRITE_TAC[COPRIME_2] THEN ASM_CASES_TAC `p = 2` THEN ASM_REWRITE_TAC[ARITH] THEN STRIP_TAC THEN FIRST_ASSUM(ASSUME_TAC o MATCH_MP PRIME_GE_2) THEN SUBGOAL_THEN `3 <= p` ASSUME_TAC THENL [ASM_ARITH_TAC; ALL_TAC] THEN ASM_MESON_TAC[MULT_SYM]; ALL_TAC] THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN ASM_CASES_TAC `k = 1` THENL [UNDISCH_THEN `k = 1` SUBST_ALL_TAC; MP_TAC(SPECL [`p EXP k`; `m:num`] NO_PRIMITIVE_ROOT_MODULO_COMPOSITE) THEN REWRITE_TAC[NOT_EXISTS_THM] THEN DISCH_THEN MATCH_MP_TAC THEN ASM_REWRITE_TAC[COPRIME_LEXP] THEN CONJ_TAC THENL [ALL_TAC; ASM_ARITH_TAC] THEN MATCH_MP_TAC(ARITH_RULE `2 EXP 2 <= x ==> 3 <= x`) THEN MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `p EXP 2` THEN ASM_REWRITE_TAC[EXP_MONO_LE; LE_EXP] THEN ASM_SIMP_TAC[PRIME_GE_2; PRIME_IMP_NZ] THEN ASM_ARITH_TAC] THEN ASM_CASES_TAC `p = 2` THENL [UNDISCH_THEN `p = 2` SUBST_ALL_TAC; MP_TAC(SPECL [`p EXP 1`; `m:num`] NO_PRIMITIVE_ROOT_MODULO_COMPOSITE) THEN REWRITE_TAC[NOT_EXISTS_THM] THEN DISCH_THEN MATCH_MP_TAC THEN ASM_REWRITE_TAC[COPRIME_LEXP] THEN REWRITE_TAC[EXP_1] THEN FIRST_ASSUM(MP_TAC o MATCH_MP PRIME_GE_2) THEN ASM_ARITH_TAC] THEN RULE_ASSUM_TAC(REWRITE_RULE[EXP_1]) THEN REWRITE_TAC[EXP_1] THEN MP_TAC(ISPEC `m:num` PRIMEPOW_FACTOR) THEN ANTS_TAC THENL [ASM_ARITH_TAC; REWRITE_TAC[LEFT_IMP_EXISTS_THM]] THEN MAP_EVERY X_GEN_TAC [`q:num`; `j:num`; `r:num`] THEN ASM_CASES_TAC `r = 0` THEN ASM_REWRITE_TAC[MULT_CLAUSES] THEN STRIP_TAC THEN UNDISCH_TAC `coprime(2,m)` THEN ASM_SIMP_TAC[COPRIME_RMUL; COPRIME_REXP; LE_1] THEN REWRITE_TAC[COPRIME_2] THEN STRIP_TAC THEN SUBGOAL_THEN `3 <= q` ASSUME_TAC THENL [MATCH_MP_TAC(ARITH_RULE `~(p = 2) /\ 2 <= p ==> 3 <= p`) THEN ASM_SIMP_TAC[PRIME_GE_2] THEN DISCH_TAC THEN UNDISCH_TAC `ODD q` THEN ASM_REWRITE_TAC[ARITH]; ALL_TAC] THEN FIRST_X_ASSUM(MP_TAC o SPECL [`q:num`; `j:num`]) THEN ASM_CASES_TAC `r = 1` THEN ASM_REWRITE_TAC[MULT_CLAUSES] THEN STRIP_TAC THEN MP_TAC(SPECL [`2 * r`; `q EXP j`] NO_PRIMITIVE_ROOT_MODULO_COMPOSITE) THEN REWRITE_TAC[COPRIME_LMUL; COPRIME_REXP] THEN ASM_REWRITE_TAC[COPRIME_2] THEN ONCE_REWRITE_TAC[COPRIME_SYM] THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[MULT_AC; NOT_EXISTS_THM] THEN DISCH_THEN MATCH_MP_TAC THEN ASM_REWRITE_TAC[ARITH_RULE `3 <= r * 2 <=> ~(r = 0 \/ r = 1)`] THEN MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `q EXP 1` THEN ASM_REWRITE_TAC[LE_EXP; ARITH; COND_ID] THEN ASM_REWRITE_TAC[EXP_1]);;
let PRIMITIVE_ROOT_EXISTS_NONTRIVIAL = 
prove (`!n. (?x. x IN 1..n-1 /\ order n x = phi n) <=> n = 2 \/ n = 4 \/ ?p k. prime p /\ 3 <= p /\ 1 <= k /\ (n = p EXP k \/ n = 2 * p EXP k)`,
GEN_TAC THEN ASM_CASES_TAC `n = 0` THENL [ASM_REWRITE_TAC[IN_NUMSEG] THEN CONV_TAC NUM_REDUCE_CONV THEN MATCH_MP_TAC(TAUT `~a /\ ~b ==> (a <=> b)`) THEN CONV_TAC(ONCE_DEPTH_CONV SYM_CONV) THEN REWRITE_TAC[MULT_EQ_0; EXP_EQ_0] THEN ARITH_TAC; ALL_TAC] THEN ASM_CASES_TAC `n = 1` THENL [ASM_REWRITE_TAC[IN_NUMSEG] THEN CONV_TAC NUM_REDUCE_CONV THEN MATCH_MP_TAC(TAUT `~a /\ ~b ==> (a <=> b)`) THEN CONV_TAC(ONCE_DEPTH_CONV SYM_CONV) THEN REWRITE_TAC[MULT_EQ_1; EXP_EQ_1] THEN ARITH_TAC; ALL_TAC] THEN MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC `?x. order n x = phi n` THEN CONJ_TAC THENL [EQ_TAC THENL [MESON_TAC[]; ALL_TAC] THEN DISCH_THEN(X_CHOOSE_TAC `x:num`) THEN EXISTS_TAC `x MOD n` THEN ASM_SIMP_TAC[IN_NUMSEG; DIVISION; ARITH_RULE `~(n = 0) /\ ~(n = 1) ==> (x <= n - 1 <=> x < n)`] THEN CONJ_TAC THENL [REWRITE_TAC[ARITH_RULE `1 <= x <=> ~(x = 0)`] THEN ASM_SIMP_TAC[GSYM DIVIDES_MOD] THEN DISCH_TAC THEN MP_TAC(SPECL [`n:num`; `x:num`] ORDER_EQ_0) THEN ASM_SIMP_TAC[LE_1; PHI_LOWERBOUND_1_STRONG] THEN REWRITE_TAC[coprime] THEN DISCH_THEN(MP_TAC o SPEC `n:num`) THEN ASM_REWRITE_TAC[DIVIDES_REFL]; FIRST_ASSUM(SUBST1_TAC o SYM) THEN MATCH_MP_TAC ORDER_CONG THEN ASM_SIMP_TAC[CONG_MOD]]; ASM_REWRITE_TAC[PRIMITIVE_ROOT_EXISTS] THEN ASM_CASES_TAC `n = 2` THEN ASM_REWRITE_TAC[] THEN ASM_CASES_TAC `n = 4` THEN ASM_REWRITE_TAC[] THEN AP_TERM_TAC THEN REWRITE_TAC[FUN_EQ_THM] THEN X_GEN_TAC `p:num` THEN AP_TERM_TAC THEN REWRITE_TAC[FUN_EQ_THM] THEN X_GEN_TAC `k:num` THEN CONV_TAC(BINOP_CONV(ONCE_DEPTH_CONV SYM_CONV)) THEN ASM_CASES_TAC `k = 0` THEN ASM_SIMP_TAC[LE_1] THEN AP_TERM_TAC THEN ASM_ARITH_TAC]);;