100/reciprocity.ml

   1 (* ========================================================================= *)
   2 (* Quadratic reciprocity.                                                    *)
   3 (* ========================================================================= *)
   4
   5 needs "Library/prime.ml";;
   6 needs "Library/pocklington.ml";;
   7
   8 prioritize_num();;
   9
  10 (* ------------------------------------------------------------------------- *)
  11 (* Misc. lemmas.                                                             *)
  12 (* ------------------------------------------------------------------------- *)
  13
  14 let IN_NUMSEG_1 = prove
  15  (`!p i. i IN 1..p - 1 <=> 0 < i /\ i < p`,
  16   REWRITE_TAC[IN_NUMSEG] THEN ARITH_TAC);;
  17
  18 let EVEN_DIV = prove
  19  (`!n. EVEN n <=> n = 2 * (n DIV 2)`,
  20   GEN_TAC THEN REWRITE_TAC[EVEN_MOD] THEN
  21   MP_TAC(SPEC `n:num` (MATCH_MP DIVISION (ARITH_RULE `~(2 = 0)`))) THEN
  22   ARITH_TAC);;
  23
  24 let CONG_MINUS1_SQUARE = prove
  25  (`2 <= p ==> ((p - 1) * (p - 1) == 1) (mod p)`,
  26   SIMP_TAC[LE_EXISTS; LEFT_IMP_EXISTS_THM] THEN REPEAT STRIP_TAC THEN
  27   REWRITE_TAC[cong; nat_mod; ARITH_RULE `(2 + x) - 1 = x + 1`] THEN
  28   MAP_EVERY EXISTS_TAC [`0`; `d:num`] THEN ARITH_TAC);;
  29
  30 let CONG_EXP_MINUS1 = prove
  31  (`!p n. 2 <= p ==> ((p - 1) EXP n == if EVEN n then 1 else p - 1) (mod p)`,
  32   REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN GEN_TAC THEN DISCH_TAC THEN
  33   INDUCT_TAC THEN REWRITE_TAC[EXP; ARITH; CONG_REFL] THEN
  34   MATCH_MP_TAC CONG_TRANS THEN
  35   EXISTS_TAC `(p - 1) * (if EVEN n then 1 else p - 1)` THEN
  36   ASM_SIMP_TAC[CONG_MULT; CONG_REFL; EVEN] THEN
  37   ASM_CASES_TAC `EVEN n` THEN
  38   ASM_SIMP_TAC[MULT_CLAUSES; CONG_REFL; CONG_MINUS1_SQUARE]);;
  39
  40 let NOT_CONG_MINUS1 = prove
  41  (`!p. 3 <= p ==> ~(p - 1 == 1) (mod p)`,
  42   REPEAT STRIP_TAC THEN SUBGOAL_THEN `(2 == 0) (mod p)` MP_TAC THENL
  43    [MATCH_MP_TAC CONG_ADD_LCANCEL THEN EXISTS_TAC `p - 1` THEN
  44     ONCE_REWRITE_TAC[CONG_SYM] THEN
  45     ASM_SIMP_TAC[ADD_CLAUSES; ARITH_RULE `3 <= p ==> (p - 1) + 2 = p + 1`] THEN
  46     MATCH_MP_TAC CONG_TRANS THEN EXISTS_TAC `0 + 1` THEN CONJ_TAC THENL
  47      [ASM_MESON_TAC[ADD_CLAUSES]; ALL_TAC] THEN
  48     MATCH_MP_TAC CONG_ADD THEN
  49     MESON_TAC[CONG_0; CONG_SYM; DIVIDES_REFL; CONG_REFL];
  50     REWRITE_TAC[CONG_0] THEN DISCH_THEN(MP_TAC o MATCH_MP DIVIDES_LE) THEN
  51     ASM_ARITH_TAC]);;
  52
  53 let CONG_COND_LEMMA = prove
  54  (`!p x y. 3 <= p /\
  55            ((if x then 1 else p - 1) == (if y then 1 else p - 1)) (mod p)
  56            ==> (x <=> y)`,
  57   REPEAT GEN_TAC THEN REPEAT(COND_CASES_TAC THEN ASM_REWRITE_TAC[]) THEN
  58   ASM_MESON_TAC[CONG_SYM; NOT_CONG_MINUS1]);;
  59
  60 let FINITE_SUBCROSS = prove
  61  (`!s:A->bool t:B->bool.
  62        FINITE s /\ FINITE t ==> FINITE {x,y | x IN s /\ y IN t /\ P x y}`,
  63   REPEAT STRIP_TAC THEN MATCH_MP_TAC FINITE_SUBSET THEN
  64   EXISTS_TAC `(s:A->bool) CROSS (t:B->bool)` THEN
  65   ASM_SIMP_TAC[FINITE_CROSS; SUBSET; IN_CROSS; FORALL_PAIR_THM;
  66                IN_ELIM_PAIR_THM]);;
  67
  68 let CARD_SUBCROSS_DETERMINATE = prove
  69  (`FINITE s /\ FINITE t /\ (!x. x IN s /\ p(x) ==> f(x) IN t)
  70    ==> CARD {(x:A),(y:B) | x IN s /\ y IN t /\ y = f x /\ p x} =
  71        CARD {x | x IN s /\ p(x)}`,
  72   REPEAT STRIP_TAC THEN CONV_TAC SYM_CONV THEN
  73   MATCH_MP_TAC CARD_IMAGE_INJ_EQ THEN EXISTS_TAC `\(x:A,y:B). x` THEN
  74   ASM_SIMP_TAC[FINITE_SUBCROSS; FORALL_PAIR_THM; EXISTS_UNIQUE_THM] THEN
  75   REWRITE_TAC[EXISTS_PAIR_THM; IN_ELIM_PAIR_THM] THEN
  76   SIMP_TAC[IN_ELIM_THM; PAIR_EQ] THEN ASM_MESON_TAC[]);;
  77
  78 let CARD_SUBCROSS_SWAP = prove
  79  (`CARD {y,x | y IN 1..m /\ x IN 1..n /\ P x y} =
  80    CARD {x,y | x IN 1..n /\ y IN 1..m /\ P x y}`,
  81   REPEAT STRIP_TAC THEN MATCH_MP_TAC CARD_IMAGE_INJ_EQ THEN
  82   EXISTS_TAC `\(x:num,y:num). (y,x)` THEN
  83   ASM_SIMP_TAC[FINITE_SUBCROSS; FINITE_NUMSEG] THEN
  84   REWRITE_TAC[EXISTS_UNIQUE_THM; FORALL_PAIR_THM; EXISTS_PAIR_THM] THEN
  85   SIMP_TAC[IN_ELIM_PAIR_THM; PAIR_EQ] THEN MESON_TAC[]);;
  86
  87 (* ------------------------------------------------------------------------- *)
  88 (* What it means to be a quadratic residue. I keep in the "mod p" as what    *)
  89 (* I think is a more intuitive notation.                                     *)
  90 (*                                                                           *)
  91 (* We might explicitly assume that the two numbers are coprime, ruling out   *)
  92 (* the degenerate case of 0 as a quadratic residue. But this seems simpler.  *)
  93 (* ------------------------------------------------------------------------- *)
  94
  95 parse_as_infix("is_quadratic_residue",(12,"right"));;
  96
  97 let is_quadratic_residue = new_definition
  98  `y is_quadratic_residue rel <=> ?x. (x EXP 2 == y) (rel)`;;
  99
 100 (* ------------------------------------------------------------------------- *)
 101 (* Alternative formulation for special cases.                                *)
 102 (* ------------------------------------------------------------------------- *)
 103
 104 let IS_QUADRATIC_RESIDUE = prove
 105  (`!a p. ~(p = 0) /\ ~(p divides a)
 106          ==> (a is_quadratic_residue (mod p) <=>
 107                  ?x. 0 < x /\ x < p /\ (x EXP 2 == a) (mod p))`,
 108   REPEAT GEN_TAC THEN REWRITE_TAC[is_quadratic_residue; EXP_2] THEN
 109   DISCH_TAC THEN EQ_TAC THENL [ALL_TAC; MESON_TAC[]] THEN
 110   DISCH_THEN(X_CHOOSE_TAC `x:num`) THEN EXISTS_TAC `x MOD p` THEN
 111   ASM_SIMP_TAC[DIVISION] THEN CONJ_TAC THENL
 112    [ASM_MESON_TAC[LT_NZ; GSYM DIVIDES_MOD; CONG_DIVIDES; DIVIDES_LMUL];
 113     UNDISCH_TAC `(x * x == a) (mod p)` THEN
 114     ASM_SIMP_TAC[CONG; MOD_MULT_MOD2]]);;
 115
 116 let IS_QUADRATIC_RESIDUE_COMMON = prove
 117  (`!a p. prime p /\ coprime(a,p)
 118          ==> (a is_quadratic_residue (mod p) <=>
 119                  ?x. 0 < x /\ x < p /\ (x EXP 2 == a) (mod p))`,
 120   REPEAT STRIP_TAC THEN MATCH_MP_TAC IS_QUADRATIC_RESIDUE THEN
 121   ASM_MESON_TAC[COPRIME_PRIME; DIVIDES_REFL; PRIME_0]);;
 122
 123 (* ------------------------------------------------------------------------- *)
 124 (* Some lemmas about dual pairs; these would be more natural over Z.         *)
 125 (* ------------------------------------------------------------------------- *)
 126
 127 let QUADRATIC_RESIDUE_PAIR_ADD = prove
 128  (`!p x y. prime p
 129            ==> (((x + y) EXP 2 == x EXP 2) (mod p) <=>
 130                  p divides y \/ p divides (2 * x + y))`,
 131   REWRITE_TAC[NUM_RING `(x + y) EXP 2 = y * (y + 2 * x) + x EXP 2`] THEN
 132   SIMP_TAC[CONG_ADD_RCANCEL_EQ_0; CONG_0; PRIME_DIVPROD_EQ; ADD_SYM]);;
 133
 134 let QUADRATIC_RESIDUE_PAIR = prove
 135  (`!p x y. prime p
 136            ==> ((x EXP 2 == y EXP 2) (mod p) <=>
 137                  p divides (x + y) \/ p divides (dist(x,y)))`,
 138   GEN_TAC THEN MATCH_MP_TAC WLOG_LE THEN CONJ_TAC THENL
 139    [MESON_TAC[DIST_SYM; CONG_SYM; ADD_SYM]; ALL_TAC] THEN
 140   REWRITE_TAC[LE_EXISTS] THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
 141   ONCE_REWRITE_TAC[CONG_SYM] THEN ASM_SIMP_TAC[QUADRATIC_RESIDUE_PAIR_ADD] THEN
 142   REWRITE_TAC[DIST_RADD_0; ARITH_RULE `x + x + d = 2 * x + d`; DISJ_ACI]);;
 143
 144 let IS_QUADRATIC_RESIDUE_PAIR = prove
 145  (`!a p. prime p /\ coprime(a,p)
 146          ==> (a is_quadratic_residue (mod p) <=>
 147                  ?x y. 0 < x /\ x < p /\ 0 < y /\ y < p /\ x + y = p /\
 148                        (x EXP 2 == a) (mod p) /\ (y EXP 2 == a) (mod p) /\
 149                        !z. 0 < z /\ z < p /\ (z EXP 2 == a) (mod p)
 150                            ==> z = x \/ z = y)`,
 151   SIMP_TAC[IS_QUADRATIC_RESIDUE_COMMON] THEN REPEAT STRIP_TAC THEN
 152   EQ_TAC THENL [ALL_TAC; MESON_TAC[]] THEN
 153   DISCH_THEN(X_CHOOSE_THEN `x:num` STRIP_ASSUME_TAC) THEN
 154   MAP_EVERY EXISTS_TAC [`x:num`; `p - x:num`] THEN
 155   ASM_SIMP_TAC[ARITH_RULE
 156    `0 < x /\ x < p ==> 0 < p - x /\ p - x < p /\ x + (p - x) = p`] THEN
 157   REPEAT STRIP_TAC THEN
 158   FIRST_X_ASSUM(MP_TAC o MATCH_MP QUADRATIC_RESIDUE_PAIR) THENL
 159    [DISCH_THEN(MP_TAC o SPECL [`x:num`; `p - x:num`]) THEN
 160     ASM_SIMP_TAC[ARITH_RULE `x < p ==> x + (p - x) = p`; DIVIDES_REFL] THEN
 161     ASM_MESON_TAC[CONG_TRANS; CONG_SYM];
 162     DISCH_THEN(MP_TAC o SPECL [`x:num`; `z:num`]) THEN
 163     SUBGOAL_THEN `(x EXP 2 == z EXP 2) (mod p)` (fun th -> SIMP_TAC[th]) THENL
 164      [ASM_MESON_TAC[CONG_TRANS; CONG_SYM]; ALL_TAC] THEN
 165     DISCH_THEN(DISJ_CASES_THEN (MP_TAC o MATCH_MP DIVIDES_CASES)) THEN
 166     REWRITE_TAC[ADD_EQ_0; DIST_EQ_0] THEN REWRITE_TAC[dist] THEN
 167     ASM_ARITH_TAC]);;
 168
 169 let QUADRATIC_RESIDUE_PAIR_PRODUCT = prove
 170  (`!p x. 0 < x /\ x < p /\ (x EXP 2 == a) (mod p)
 171          ==> (x * (p - x) == (p - 1) * a) (mod p)`,
 172   REPEAT STRIP_TAC THEN
 173   FIRST_ASSUM(ASSUME_TAC o MP (ARITH_RULE `x < p ==> 1 <= p`)) THEN
 174   SUBGOAL_THEN `(x * (p - x) + x EXP 2 == a * (p - 1) + a * 1) (mod p)`
 175   MP_TAC THENL
 176    [ASM_SIMP_TAC[LEFT_SUB_DISTRIB; EXP_2; SUB_ADD;
 177                  LE_MULT_LCANCEL; LT_IMP_LE] THEN
 178     REWRITE_TAC[cong; nat_mod] THEN ASM_MESON_TAC[ADD_SYM; MULT_SYM];
 179     REWRITE_TAC[MULT_CLAUSES] THEN
 180     ASM_MESON_TAC[CONG_ADD; CONG_TRANS; CONG_SYM; CONG_REFL; MULT_SYM;
 181                   CONG_ADD_RCANCEL]]);;
 182
 183 (* ------------------------------------------------------------------------- *)
 184 (* Define the Legendre symbol.                                               *)
 185 (* ------------------------------------------------------------------------- *)
 186
 187 let legendre = new_definition
 188  `(legendre:num#num->int)(a,p) =
 189         if ~(coprime(a,p)) then &0
 190         else if a is_quadratic_residue (mod p) then &1
 191         else --(&1)`;;
 192
 193 (* ------------------------------------------------------------------------- *)
 194 (* Definition of iterated product.                                           *)
 195 (* ------------------------------------------------------------------------- *)
 196
 197 let nproduct = new_definition `nproduct = iterate ( * )`;;
 198
 199 let NPRODUCT_CLAUSES = prove
 200  (`(!f. nproduct {} f = 1) /\
 201    (!x f s. FINITE(s)
 202             ==> (nproduct (x INSERT s) f =
 203                  if x IN s then nproduct s f else f(x) * nproduct s f))`,
 204   REWRITE_TAC[nproduct; GSYM NEUTRAL_MUL] THEN
 205   ONCE_REWRITE_TAC[SWAP_FORALL_THM] THEN
 206   MATCH_MP_TAC ITERATE_CLAUSES THEN REWRITE_TAC[MONOIDAL_MUL]);;
 207
 208 let NPRODUCT_DELETE = prove
 209  (`!s. FINITE s /\ a IN s
 210        ==> f(a) * nproduct(s DELETE a) f = nproduct s f`,
 211   SIMP_TAC[nproduct; ITERATE_DELETE; MONOIDAL_MUL]);;
 212
 213 let CONG_NPRODUCT = prove
 214  (`!f g s. FINITE s /\ (!x. x IN s ==> (f x == g x) (mod n))
 215            ==> (nproduct s f == nproduct s g) (mod n)`,
 216   REWRITE_TAC[nproduct] THEN
 217   MATCH_MP_TAC(MATCH_MP ITERATE_RELATED MONOIDAL_MUL) THEN
 218   SIMP_TAC[CONG_REFL; CONG_MULT]);;
 219
 220 let NPRODUCT_MULT = prove
 221  (`!f g s. FINITE s
 222            ==> nproduct s (\x. f x * g x) = nproduct s f * nproduct s g`,
 223   GEN_TAC THEN GEN_TAC THEN MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
 224   SIMP_TAC[NPRODUCT_CLAUSES; MULT_AC; MULT_CLAUSES]);;
 225
 226 let NPRODUCT_INJECTION = prove
 227  (`!f p s. FINITE s /\
 228            (!x. x IN s ==> p x IN s) /\
 229            (!x y. x IN s /\ y IN s /\ p x = p y ==> x = y)
 230            ==> nproduct s (f o p) = nproduct s f`,
 231   REWRITE_TAC[nproduct] THEN MATCH_MP_TAC ITERATE_INJECTION THEN
 232   REWRITE_TAC[MONOIDAL_MUL]);;
 233
 234 let NPRODUCT_CONST = prove
 235  (`!c s. FINITE s ==> nproduct s (\x. c) = c EXP (CARD s)`,
 236   GEN_TAC THEN MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
 237   SIMP_TAC[NPRODUCT_CLAUSES; CARD_CLAUSES; EXP]);;
 238
 239 let NPRODUCT_DELTA_CONST = prove
 240  (`!c s. FINITE s
 241          ==> nproduct s (\x. if p(x) then c else 1) =
 242              c EXP (CARD {x | x IN s /\ p(x)})`,
 243   let lemma1 = prove
 244    (`{x | x IN a INSERT s /\ p(x)} =
 245      if p(a) then a INSERT {x | x IN s /\ p(x)}
 246      else {x | x IN s /\ p(x)}`,
 247     COND_CASES_TAC THEN ASM_REWRITE_TAC[EXTENSION; IN_INSERT; IN_ELIM_THM] THEN
 248     ASM_MESON_TAC[])
 249   and lemma2 = prove
 250    (`FINITE s ==> FINITE {x | x IN s /\ p(x)}`,
 251     MATCH_MP_TAC(ONCE_REWRITE_RULE[TAUT `a /\ b ==> c <=> b ==> a ==> c`]
 252                 FINITE_SUBSET) THEN
 253     SIMP_TAC[SUBSET; IN_ELIM_THM]) in
 254   GEN_TAC THEN MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
 255   SIMP_TAC[NPRODUCT_CLAUSES; CARD_CLAUSES; EXP; NOT_IN_EMPTY;
 256            SET_RULE `{x | F} = {}`; lemma1] THEN
 257   REPEAT STRIP_TAC THEN COND_CASES_TAC THEN
 258   ASM_SIMP_TAC[CARD_CLAUSES; IN_ELIM_THM; lemma2; EXP; MULT_CLAUSES]);;
 259
 260 let COPRIME_NPRODUCT = prove
 261  (`!f p s. FINITE s /\ (!x. x IN s ==> coprime(p,f x))
 262            ==> coprime(p,nproduct s f)`,
 263   GEN_TAC THEN GEN_TAC THEN REWRITE_TAC[IMP_CONJ] THEN
 264   MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
 265   SIMP_TAC[NPRODUCT_CLAUSES; COPRIME_1; IN_INSERT; COPRIME_MUL]);;
 266
 267 (* ------------------------------------------------------------------------- *)
 268 (* Factorial in terms of products.                                           *)
 269 (* ------------------------------------------------------------------------- *)
 270
 271 let FACT_NPRODUCT = prove
 272  (`!n. FACT(n) = nproduct(1..n) (\i. i)`,
 273   INDUCT_TAC THEN
 274   REWRITE_TAC[FACT; NUMSEG_CLAUSES; ARITH; NPRODUCT_CLAUSES] THEN
 275   ASM_SIMP_TAC[ARITH_RULE `1 <= SUC n`; NPRODUCT_CLAUSES; FINITE_NUMSEG] THEN
 276   REWRITE_TAC[IN_NUMSEG] THEN ARITH_TAC);;
 277
 278 (* ------------------------------------------------------------------------- *)
 279 (* General "pairing up" theorem for products.                                *)
 280 (* ------------------------------------------------------------------------- *)
 281
 282 let NPRODUCT_PAIRUP_INDUCT = prove
 283  (`!f r n s k. s HAS_SIZE (2 * n) /\
 284                (!x:A. x IN s ==> ?!y. y IN s /\ ~(y = x) /\
 285                                       (f(x) * f(y) == k) (mod r))
 286                ==> (nproduct s f == k EXP n) (mod r)`,
 287   GEN_TAC THEN GEN_TAC THEN
 288   MATCH_MP_TAC num_WF THEN X_GEN_TAC `n:num` THEN DISCH_TAC THEN
 289   X_GEN_TAC `s:A->bool` THEN GEN_TAC THEN ASM_CASES_TAC `n = 0` THENL
 290    [ASM_SIMP_TAC[MULT_CLAUSES; HAS_SIZE_0; NPRODUCT_CLAUSES; EXP; CONG_REFL];
 291     ALL_TAC] THEN
 292   ASM_CASES_TAC `s:A->bool = {}` THENL
 293    [ASM_MESON_TAC[HAS_SIZE_0; ARITH_RULE `2 * n = 0 <=> n = 0`; HAS_SIZE];
 294     ALL_TAC] THEN
 295   STRIP_TAC THEN FIRST_X_ASSUM(X_CHOOSE_TAC `a:A` o
 296     GEN_REWRITE_RULE I [GSYM MEMBER_NOT_EMPTY]) THEN
 297   FIRST_X_ASSUM(MP_TAC o SPEC `n - 1`) THEN
 298   ASM_SIMP_TAC[ARITH_RULE `~(n = 0) ==> n - 1 < n`] THEN
 299   FIRST_ASSUM(MP_TAC o SPEC `a:A`) THEN REWRITE_TAC[ASSUME `(a:A) IN s`] THEN
 300   REWRITE_TAC[EXISTS_UNIQUE] THEN
 301   DISCH_THEN(X_CHOOSE_THEN `b:A` STRIP_ASSUME_TAC) THEN
 302   DISCH_THEN(MP_TAC o SPECL [`(s DELETE a) DELETE (b:A)`; `k:num`]) THEN
 303   SUBGOAL_THEN `s = (a:A) INSERT (b INSERT (s DELETE a DELETE b))`
 304    (ASSUME_TAC o SYM) THENL [ASM SET_TAC[]; ALL_TAC] THEN ANTS_TAC THENL
 305    [CONJ_TAC THENL
 306      [UNDISCH_TAC `(s:A->bool) HAS_SIZE 2 * n` THEN
 307       FIRST_X_ASSUM(fun th -> GEN_REWRITE_TAC (LAND_CONV o LAND_CONV)
 308         [SYM th]) THEN
 309       SIMP_TAC[HAS_SIZE; FINITE_INSERT; CARD_CLAUSES; FINITE_DELETE;
 310                IMP_CONJ; IN_DELETE; IN_INSERT] THEN
 311       ASM_REWRITE_TAC[] THEN ARITH_TAC;
 312       ALL_TAC] THEN
 313     X_GEN_TAC `x:A` THEN ASM_REWRITE_TAC[IN_DELETE] THEN STRIP_TAC THEN
 314     FIRST_ASSUM(MP_TAC o C MATCH_MP (ASSUME `(x:A) IN s`)) THEN
 315     REWRITE_TAC[EXISTS_UNIQUE] THEN MATCH_MP_TAC MONO_EXISTS THEN
 316     X_GEN_TAC `y:A` THEN STRIP_TAC THEN CONJ_TAC THENL
 317      [ALL_TAC; ASM_MESON_TAC[]] THEN
 318     ASM_REWRITE_TAC[] THEN CONJ_TAC THEN DISCH_THEN SUBST_ALL_TAC THENL
 319      [ASM_MESON_TAC[MULT_SYM]; ALL_TAC] THEN
 320     FIRST_X_ASSUM(MP_TAC o C MATCH_MP (ASSUME `(b:A) IN s`)) THEN
 321     REWRITE_TAC[EXISTS_UNIQUE_THM] THEN
 322     DISCH_THEN(MP_TAC o SPECL [`a:A`; `x:A`] o CONJUNCT2) THEN
 323     ASM_MESON_TAC[MULT_SYM];
 324     ALL_TAC] THEN
 325   DISCH_TAC THEN EXPAND_TAC "s" THEN
 326   FIRST_X_ASSUM(MP_TAC o CONJUNCT1 o REWRITE_RULE[HAS_SIZE]) THEN
 327   SIMP_TAC[NPRODUCT_CLAUSES; FINITE_INSERT; FINITE_DELETE] THEN
 328   REWRITE_TAC[IN_INSERT; IN_DELETE; MULT_CLAUSES] THEN
 329   FIRST_ASSUM(SUBST1_TAC o MATCH_MP
 330    (ARITH_RULE `~(n = 0) ==> n = SUC(n - 1)`)) THEN
 331   ASM_REWRITE_TAC[MULT_ASSOC; EXP] THEN DISCH_TAC THEN
 332   MATCH_MP_TAC CONG_MULT THEN ASM_REWRITE_TAC[]);;
 333
 334 (* ------------------------------------------------------------------------- *)
 335 (* The two cases.                                                            *)
 336 (* ------------------------------------------------------------------------- *)
 337
 338 let QUADRATIC_NONRESIDUE_FACT = prove
 339  (`!a p. prime p /\ ODD(p) /\
 340          coprime(a,p) /\ ~(a is_quadratic_residue (mod p))
 341          ==> (a EXP ((p - 1) DIV 2) == FACT(p - 1)) (mod p)`,
 342   REPEAT STRIP_TAC THEN REWRITE_TAC[FACT_NPRODUCT] THEN
 343   ONCE_REWRITE_TAC[CONG_SYM] THEN MATCH_MP_TAC NPRODUCT_PAIRUP_INDUCT THEN
 344   CONJ_TAC THENL
 345    [FIRST_X_ASSUM(CHOOSE_THEN SUBST1_TAC o
 346       GEN_REWRITE_RULE I [ODD_EXISTS]) THEN
 347     SIMP_TAC[SUC_SUB1; DIV_MULT; ARITH] THEN
 348     REWRITE_TAC[HAS_SIZE; FINITE_NUMSEG; CARD_NUMSEG; ADD_SUB];
 349     ALL_TAC] THEN
 350   ASM_CASES_TAC `p = 0` THENL [ASM_MESON_TAC[PRIME_0]; ALL_TAC] THEN
 351   ASM_SIMP_TAC[IN_NUMSEG; ARITH_RULE `1 <= x <=> 0 < x`;
 352                ARITH_RULE `~(p = 0) ==> (x <= p - 1 <=> x < p)`] THEN
 353   REPEAT STRIP_TAC THEN
 354   MP_TAC(SPECL [`a:num`; `p:num`; `x:num`] CONG_SOLVE_UNIQUE_NONTRIVIAL) THEN
 355   ONCE_REWRITE_TAC[COPRIME_SYM] THEN ASM_REWRITE_TAC[] THEN
 356   MATCH_MP_TAC EQ_IMP THEN AP_TERM_TAC THEN
 357   REWRITE_TAC[FUN_EQ_THM] THEN ASM_MESON_TAC[is_quadratic_residue; EXP_2]);;
 358
 359 let QUADRATIC_RESIDUE_FACT = prove
 360  (`!a p. prime p /\ ODD(p) /\
 361          coprime(a,p) /\ a is_quadratic_residue (mod p)
 362          ==> (a EXP ((p - 1) DIV 2) == FACT(p - 2)) (mod p)`,
 363   REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[CONG_SYM] THEN
 364   SUBGOAL_THEN `3 <= p /\ ~(p = 0)` STRIP_ASSUME_TAC THENL
 365    [FIRST_ASSUM(MP_TAC o MATCH_MP PRIME_GE_2) THEN UNDISCH_TAC `ODD(p)` THEN
 366     ASM_CASES_TAC `p = 2` THEN ASM_REWRITE_TAC[ARITH] THEN
 367     UNDISCH_TAC `~(p = 2)` THEN ARITH_TAC;
 368     ALL_TAC] THEN
 369   UNDISCH_TAC `a is_quadratic_residue (mod p)` THEN
 370   ASM_SIMP_TAC[EXP_2; IS_QUADRATIC_RESIDUE_PAIR; LEFT_IMP_EXISTS_THM] THEN
 371   MAP_EVERY X_GEN_TAC [`x:num`; `y:num`] THEN STRIP_TAC THEN
 372   SUBGOAL_THEN `~(x:num = y)` ASSUME_TAC THENL
 373    [ASM_MESON_TAC[ODD_ADD]; ALL_TAC] THEN
 374   MP_TAC(ISPECL [`\i:num. i`; `p:num`; `(p - 3) DIV 2`;
 375    `(1..p-1) DELETE x DELETE y`; `a:num`] NPRODUCT_PAIRUP_INDUCT) THEN
 376   ANTS_TAC THENL
 377    [ASM_SIMP_TAC[HAS_SIZE; FINITE_DELETE; FINITE_NUMSEG; IN_NUMSEG_1;
 378                  CARD_DELETE; IN_DELETE; CARD_NUMSEG_1] THEN
 379     SIMP_TAC[ARITH_RULE `p - 1 - 1 - 1 = p - 3`] THEN
 380     ASM_SIMP_TAC[GSYM EVEN_DIV; EVEN_SUB; ARITH; NOT_EVEN] THEN
 381     X_GEN_TAC `u:num` THEN REPEAT STRIP_TAC THEN
 382     MP_TAC(SPECL [`a:num`; `p:num`; `u:num`] CONG_SOLVE_UNIQUE_NONTRIVIAL) THEN
 383     ONCE_REWRITE_TAC[COPRIME_SYM] THEN ASM_REWRITE_TAC[] THEN
 384     MATCH_MP_TAC EQ_IMP THEN AP_TERM_TAC THEN ABS_TAC THEN EQ_TAC THEN
 385     STRIP_TAC THEN ASM_REWRITE_TAC[] THEN REPEAT CONJ_TAC THEN
 386     DISCH_THEN SUBST_ALL_TAC THEN
 387     RULE_ASSUM_TAC(ONCE_REWRITE_RULE[MULT_SYM]) THEN
 388     ASM_MESON_TAC[CONG_SOLVE_UNIQUE; PRIME_0; PRIME_COPRIME_LT];
 389     ALL_TAC] THEN
 390   MP_TAC(SPECL [`p:num`; `x:num`] QUADRATIC_RESIDUE_PAIR_PRODUCT) THEN
 391   ASM_SIMP_TAC[EXP_2; IMP_IMP; ARITH_RULE `x + y = p ==> p - x = y`] THEN
 392   DISCH_THEN(MP_TAC o MATCH_MP CONG_MULT) THEN
 393   ASM_SIMP_TAC[NPRODUCT_DELETE; GSYM MULT_ASSOC; IN_DELETE;
 394                FINITE_DELETE; IN_NUMSEG_1; FINITE_NUMSEG] THEN
 395   ASM_SIMP_TAC[GSYM(CONJUNCT2 EXP); GSYM FACT_NPRODUCT; ARITH_RULE
 396    `3 <= p ==> SUC((p - 3) DIV 2) = (p - 1) DIV 2`] THEN
 397   ASM_SIMP_TAC[FACT; ARITH_RULE `3 <= p ==> p - 1 = SUC(p - 2)`] THEN
 398   ASM_SIMP_TAC[ARITH_RULE `3 <= p ==> SUC(p - 2) = p - 1`] THEN
 399   ASM_MESON_TAC[COPRIME_MINUS1; CONG_MULT_LCANCEL; CONG_SYM]);;
 400
 401 (* ------------------------------------------------------------------------- *)
 402 (* We immediately get one part of Wilson's theorem.                          *)
 403 (* ------------------------------------------------------------------------- *)
 404
 405 let WILSON_LEMMA = prove
 406  (`!p. prime(p) ==> (FACT(p - 2) == 1) (mod p)`,
 407   REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[CONG_SYM] THEN
 408   FIRST_ASSUM(DISJ_CASES_THEN2 SUBST_ALL_TAC ASSUME_TAC o MATCH_MP PRIME_ODD)
 409   THENL [CONV_TAC NUM_REDUCE_CONV THEN CONV_TAC CONG_CONV; ALL_TAC] THEN
 410   MP_TAC(SPECL [`1`; `p:num`] QUADRATIC_RESIDUE_FACT) THEN
 411   ASM_MESON_TAC[is_quadratic_residue; COPRIME_SYM; COPRIME_1; CONG_REFL;
 412                 EXP_ONE; CONG_SYM]);;
 413
 414 let WILSON_IMP = prove
 415  (`!p. prime(p) ==> (FACT(p - 1) == p - 1) (mod p)`,
 416   SIMP_TAC[FACT; PRIME_GE_2; ARITH_RULE `2 <= p ==> p - 1 = SUC(p - 2)`] THEN
 417   MESON_TAC[CONG_MULT; MULT_CLAUSES; WILSON_LEMMA; CONG_REFL]);;
 418
 419 let WILSON = prove
 420  (`!p. ~(p = 1) ==> (prime p <=> (FACT(p - 1) == p - 1) (mod p))`,
 421   X_GEN_TAC `n:num` THEN DISCH_TAC THEN EQ_TAC THEN SIMP_TAC[WILSON_IMP] THEN
 422   FIRST_X_ASSUM(MP_TAC o MATCH_MP PRIME_FACTOR) THEN
 423   DISCH_THEN(X_CHOOSE_THEN `p:num` STRIP_ASSUME_TAC) THEN
 424   FIRST_ASSUM(MP_TAC o MATCH_MP DIVIDES_LE) THEN
 425   ASM_CASES_TAC `n = 0` THEN ASM_REWRITE_TAC[] THENL
 426    [ASM_REWRITE_TAC[CONG_MOD_0] THEN CONV_TAC NUM_REDUCE_CONV; ALL_TAC] THEN
 427   REWRITE_TAC[LE_LT] THEN ASM_CASES_TAC `n:num = p` THEN ASM_REWRITE_TAC[] THEN
 428   DISCH_THEN(MP_TAC o MATCH_MP (ARITH_RULE `x < y ==> x <= y - 1`)) THEN
 429   ASM_SIMP_TAC[GSYM DIVIDES_FACT_PRIME] THEN
 430   DISCH_THEN(fun th -> DISCH_TAC THEN MP_TAC th) THEN
 431   SUBGOAL_THEN `p divides FACT(n - 1) <=> p divides (n - 1)` SUBST1_TAC THENL
 432    [MATCH_MP_TAC CONG_DIVIDES THEN
 433     MATCH_MP_TAC CONG_MOD_MULT THEN EXISTS_TAC `n:num` THEN
 434     ASM_REWRITE_TAC[];
 435     ALL_TAC] THEN
 436   DISCH_TAC THEN SUBGOAL_THEN `p divides 1` MP_TAC THENL
 437    [MATCH_MP_TAC DIVIDES_ADD_REVR THEN EXISTS_TAC `n - 1` THEN
 438     ASM_SIMP_TAC[ARITH_RULE `~(n = 0) ==> n - 1 + 1 = n`];
 439     REWRITE_TAC[DIVIDES_ONE] THEN ASM_MESON_TAC[PRIME_1]]);;
 440
 441 (* ------------------------------------------------------------------------- *)
 442 (* Using Wilson's theorem we can get the Euler criterion.                    *)
 443 (* ------------------------------------------------------------------------- *)
 444
 445 let EULER_CRITERION = prove
 446  (`!a p. prime p /\ coprime(a,p)
 447          ==> (a EXP ((p - 1) DIV 2) ==
 448               (if a is_quadratic_residue (mod p) then 1 else p - 1)) (mod p)`,
 449   REPEAT STRIP_TAC THEN FIRST_ASSUM(DISJ_CASES_THEN2 SUBST_ALL_TAC ASSUME_TAC o
 450     MATCH_MP PRIME_ODD) THEN CONV_TAC NUM_REDUCE_CONV THEN
 451   REWRITE_TAC[COND_ID; EXP; CONG_REFL] THEN
 452   ASM_MESON_TAC[WILSON_LEMMA; WILSON_IMP; CONG_TRANS; CONG_SYM;
 453                 QUADRATIC_RESIDUE_FACT; QUADRATIC_NONRESIDUE_FACT]);;
 454
 455 (* ------------------------------------------------------------------------- *)
 456 (* Gauss's Lemma.                                                            *)
 457 (* ------------------------------------------------------------------------- *)
 458
 459 let GAUSS_LEMMA_1 = prove
 460  (`prime p /\ coprime(a,p) /\ 2 * r + 1 = p
 461    ==> nproduct(1..r) (\x. let b = (a * x) MOD p in
 462                            if b <= r then b else p - b) =
 463        nproduct(1..r) (\x. x)`,
 464   REPEAT STRIP_TAC THEN FIRST_ASSUM(ASSUME_TAC o MATCH_MP PRIME_IMP_NZ) THEN
 465   GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [SYM(CONJUNCT1(SPEC_ALL I_O_ID))] THEN
 466   REWRITE_TAC[I_DEF] THEN MATCH_MP_TAC NPRODUCT_INJECTION THEN
 467   REWRITE_TAC[FINITE_NUMSEG] THEN
 468   ABBREV_TAC `f = \x. let b = (a * x) MOD p in
 469                       if b <= r then b else p - b` THEN
 470   MATCH_MP_TAC(TAUT `a /\ (a ==> b) ==> a /\ b`) THEN CONJ_TAC THENL
 471    [GEN_TAC THEN EXPAND_TAC "f" THEN REWRITE_TAC[IN_NUMSEG] THEN
 472     LET_TAC THEN REWRITE_TAC[LET_DEF; LET_END_DEF] THEN REPEAT STRIP_TAC THENL
 473      [ALL_TAC; EXPAND_TAC "p" THEN ARITH_TAC] THEN
 474     REWRITE_TAC[ARITH_RULE `1 <= x <=> ~(x = 0)`] THEN COND_CASES_TAC THENL
 475      [ALL_TAC; ASM_MESON_TAC[DIVISION; NOT_LE; SUB_EQ_0; PRIME_0]] THEN
 476     EXPAND_TAC "b" THEN ASM_SIMP_TAC[GSYM DIVIDES_MOD; PRIME_IMP_NZ] THEN
 477     ASM_SIMP_TAC[PRIME_DIVPROD_EQ] THEN STRIP_TAC THENL
 478      [ASM_MESON_TAC[coprime; DIVIDES_REFL; PRIME_1];
 479       ASM_MESON_TAC[DIVIDES_LE; ARITH_RULE `~(1 <= 0)`;
 480                     ARITH_RULE `~(2 * r + 1 <= i /\ i <= r)`]];
 481     REWRITE_TAC[LET_DEF; LET_END_DEF] THEN DISCH_TAC] THEN
 482   MAP_EVERY X_GEN_TAC [`i:num`; `j:num`] THEN REWRITE_TAC[IN_NUMSEG] THEN
 483   REPEAT STRIP_TAC THEN MATCH_MP_TAC CONG_IMP_EQ THEN EXISTS_TAC `p:num` THEN
 484   REPEAT(CONJ_TAC THENL
 485    [ASM_MESON_TAC[ARITH_RULE `i <= r ==> i < 2 * r + 1`] ; ALL_TAC]) THEN
 486   MATCH_MP_TAC CONG_MULT_LCANCEL THEN EXISTS_TAC `a:num` THEN
 487   FIRST_X_ASSUM(MP_TAC o MATCH_MP (ARITH_RULE
 488    `(if a then x else p - x) = (if b then y else p - y) ==> x < p /\ y < p
 489     ==> x = y \/ x + y = p`)) THEN ASM_SIMP_TAC[DIVISION] THEN
 490   DISCH_THEN(DISJ_CASES_THEN MP_TAC) THENL [ASM_MESON_TAC[CONG]; ALL_TAC] THEN
 491   DISCH_THEN(MP_TAC o C AP_THM `p:num` o AP_TERM `(MOD)`) THEN
 492   ASM_SIMP_TAC[MOD_ADD_MOD] THEN ASM_SIMP_TAC[GSYM CONG] THEN
 493   DISCH_THEN(MP_TAC o MATCH_MP CONG_DIVIDES) THEN
 494   ASM_SIMP_TAC[GSYM LEFT_ADD_DISTRIB; PRIME_DIVPROD_EQ; DIVIDES_REFL] THEN
 495   STRIP_TAC THENL
 496    [ASM_MESON_TAC[coprime; DIVIDES_REFL; PRIME_1]; ALL_TAC] THEN
 497   FIRST_ASSUM(MP_TAC o MATCH_MP DIVIDES_LE) THEN
 498   ASM_SIMP_TAC[ARITH_RULE `1 <= i ==> ~(i + j = 0)`] THEN
 499   MAP_EVERY UNDISCH_TAC [`i <= r`; `j <= r`; `2 * r + 1 = p`] THEN ARITH_TAC);;
 500
 501 let GAUSS_LEMMA_2 = prove
 502  (`prime p /\ coprime(a,p) /\ 2 * r + 1 = p
 503    ==> (nproduct(1..r) (\x. let b = (a * x) MOD p in
 504                             if b <= r then b else p - b) ==
 505         (p - 1) EXP (CARD {x | x IN 1..r /\ r < (a * x) MOD p}) *
 506         a EXP r * nproduct(1..r) (\x. x)) (mod p)`,
 507   REPEAT STRIP_TAC THEN
 508   ABBREV_TAC `s = {x | x IN 1..r /\ (a * x) MOD p <= r}` THEN
 509   MATCH_MP_TAC CONG_TRANS THEN
 510   EXISTS_TAC
 511    `nproduct(1..r) (\x. (if x IN s then 1 else p - 1) * (a * x) MOD p)` THEN
 512   CONJ_TAC THENL
 513    [MATCH_MP_TAC CONG_NPRODUCT THEN REWRITE_TAC[FINITE_NUMSEG; IN_NUMSEG] THEN
 514     X_GEN_TAC `i:num` THEN STRIP_TAC THEN LET_TAC THEN
 515     EXPAND_TAC "s" THEN REWRITE_TAC[IN_ELIM_THM] THEN
 516     ASM_REWRITE_TAC[IN_NUMSEG] THEN
 517     COND_CASES_TAC THEN ASM_REWRITE_TAC[MULT_CLAUSES; CONG_REFL] THEN
 518     REWRITE_TAC[RIGHT_SUB_DISTRIB] THEN MATCH_MP_TAC CONG_SUB THEN
 519     ASM_REWRITE_TAC[LE_MULT_RCANCEL; MULT_CLAUSES; CONG_REFL] THEN
 520     REWRITE_TAC[ARITH_RULE `b <= p /\ (1 <= p \/ b = 0) <=> b <= p`] THEN
 521     FIRST_ASSUM(MP_TAC o MATCH_MP PRIME_GE_2) THEN
 522     DISCH_THEN(MP_TAC o SPEC `a * i:num` o MATCH_MP DIVISION o
 523      MATCH_MP (ARITH_RULE `2 <= p ==> ~(p = 0)`)) THEN
 524     ASM_SIMP_TAC[LT_IMP_LE; cong; nat_mod] THEN DISCH_THEN(K ALL_TAC) THEN
 525     MAP_EVERY EXISTS_TAC [`b:num`; `1`] THEN ARITH_TAC;
 526     ALL_TAC] THEN
 527   ASM_SIMP_TAC[NPRODUCT_MULT; FINITE_NUMSEG] THEN
 528   MATCH_MP_TAC CONG_MULT THEN CONJ_TAC THENL
 529    [ONCE_REWRITE_TAC[TAUT `(if p then x else y) = (if ~p then y else x)`] THEN
 530     SIMP_TAC[NPRODUCT_DELTA_CONST; FINITE_NUMSEG] THEN
 531     MATCH_MP_TAC EQ_IMP_CONG THEN AP_TERM_TAC THEN AP_TERM_TAC THEN
 532     EXPAND_TAC "s" THEN REWRITE_TAC[EXTENSION; IN_ELIM_THM] THEN
 533     MESON_TAC[NOT_LT];
 534     ALL_TAC] THEN
 535   MATCH_MP_TAC CONG_TRANS THEN EXISTS_TAC `nproduct(1..r) (\x. a * x)` THEN
 536   CONJ_TAC THENL
 537    [ASM_SIMP_TAC[CONG_MOD; PRIME_IMP_NZ; CONG_NPRODUCT; FINITE_NUMSEG];
 538     SIMP_TAC[NPRODUCT_MULT; FINITE_NUMSEG; NPRODUCT_CONST; CARD_NUMSEG_1] THEN
 539     REWRITE_TAC[CONG_REFL]]);;
 540
 541 let GAUSS_LEMMA_3 = prove
 542  (`prime p /\ coprime(a,p) /\ 2 * r + 1 = p
 543    ==> ((p - 1) EXP CARD {x | x IN 1..r /\ r < (a * x) MOD p} *
 544         (if a is_quadratic_residue mod p then 1 else p - 1) == 1) (mod p)`,
 545   REPEAT STRIP_TAC THEN MATCH_MP_TAC CONG_TRANS THEN EXISTS_TAC
 546    `(p - 1) EXP CARD {x | x IN 1..r /\ r < (a * x) MOD p} * a EXP r` THEN
 547   ONCE_REWRITE_TAC[CONG_SYM] THEN CONJ_TAC THENL
 548    [MATCH_MP_TAC CONG_MULT THEN REWRITE_TAC[CONG_REFL] THEN
 549     SUBGOAL_THEN `r = (p - 1) DIV 2`
 550      (fun th -> ASM_SIMP_TAC[th; EULER_CRITERION]) THEN
 551     EXPAND_TAC "p" THEN ARITH_TAC;
 552     ALL_TAC] THEN
 553   MATCH_MP_TAC CONG_MULT_RCANCEL THEN
 554   EXISTS_TAC `nproduct (1..r) (\x. x)` THEN
 555   ASM_SIMP_TAC[MULT_CLAUSES; GSYM MULT_ASSOC;
 556                SIMP_RULE[GAUSS_LEMMA_1] GAUSS_LEMMA_2] THEN
 557   ONCE_REWRITE_TAC[COPRIME_SYM] THEN MATCH_MP_TAC COPRIME_NPRODUCT THEN
 558   REWRITE_TAC[IN_NUMSEG; FINITE_NUMSEG] THEN REPEAT STRIP_TAC THEN
 559   ONCE_REWRITE_TAC[COPRIME_SYM] THEN MATCH_MP_TAC PRIME_COPRIME_LT THEN
 560   ASM_REWRITE_TAC[] THEN ASM_ARITH_TAC);;
 561
 562 let GAUSS_LEMMA_4 = prove
 563  (`prime p /\ coprime(a,p) /\ 2 * r + 1 = p
 564    ==> ((if EVEN(CARD{x | x IN 1..r /\ r < (a * x) MOD p}) then 1 else p - 1) *
 565         (if a is_quadratic_residue mod p then 1 else p - 1) == 1) (mod p)`,
 566   REPEAT STRIP_TAC THEN MATCH_MP_TAC CONG_TRANS THEN
 567   EXISTS_TAC `(p - 1) EXP CARD {x | x IN 1..r /\ r < (a * x) MOD p} *
 568               (if a is_quadratic_residue mod p then 1 else p - 1)` THEN
 569   ASM_SIMP_TAC[GAUSS_LEMMA_3] THEN ONCE_REWRITE_TAC[CONG_SYM] THEN
 570   ASM_SIMP_TAC[CONG_EXP_MINUS1; CONG_MULT; CONG_REFL; PRIME_GE_2]);;
 571
 572 let GAUSS_LEMMA = prove
 573  (`!a p r. prime p /\ coprime(a,p) /\ 2 * r + 1 = p
 574            ==> (a is_quadratic_residue (mod p) <=>
 575                 EVEN(CARD {x | x IN 1..r /\ r < (a * x) MOD p}))`,
 576   REPEAT GEN_TAC THEN DISCH_TAC THEN
 577   MATCH_MP_TAC CONG_COND_LEMMA THEN EXISTS_TAC `p:num` THEN CONJ_TAC THENL
 578    [FIRST_X_ASSUM(CONJUNCTS_THEN2 MP_TAC STRIP_ASSUME_TAC) THEN
 579     EXPAND_TAC "p" THEN ASM_CASES_TAC `r = 0` THENL
 580      [REWRITE_TAC[ASSUME `r = 0`; ARITH; PRIME_1];
 581       UNDISCH_TAC `~(r = 0)` THEN ARITH_TAC];
 582     FIRST_ASSUM(MP_TAC o MATCH_MP GAUSS_LEMMA_4) THEN
 583     REPEAT(COND_CASES_TAC THEN ASM_SIMP_TAC[CONG_REFL]) THEN
 584     REWRITE_TAC[MULT_CLAUSES] THEN MESON_TAC[CONG_SYM]]);;
 585
 586 (* ------------------------------------------------------------------------- *)
 587 (* A more symmetrical version.                                               *)
 588 (* ------------------------------------------------------------------------- *)
 589
 590 let GAUSS_LEMMA_SYM = prove
 591  (`!p q r s. prime p /\ prime q /\ coprime(p,q) /\
 592              2 * r + 1 = p /\ 2 * s + 1 = q
 593              ==> (q is_quadratic_residue (mod p) <=>
 594                   EVEN(CARD {x,y | x IN 1..r /\ y IN 1..s /\
 595                                    q * x < p * y /\ p * y <= q * x + r}))`,
 596   ONCE_REWRITE_TAC[COPRIME_SYM] THEN REPEAT STRIP_TAC THEN
 597   MP_TAC(SPECL [`q:num`; `p:num`; `r:num`] GAUSS_LEMMA) THEN
 598   ASM_SIMP_TAC[] THEN DISCH_THEN(K ALL_TAC) THEN AP_TERM_TAC THEN
 599   MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC
 600    `CARD {x,y | x IN 1..r /\ y IN 1..s /\
 601                 y = (q * x) DIV p + 1 /\ r < (q * x) MOD p}` THEN
 602   CONJ_TAC THENL
 603    [CONV_TAC SYM_CONV THEN MATCH_MP_TAC CARD_SUBCROSS_DETERMINATE THEN
 604     REWRITE_TAC[FINITE_NUMSEG; IN_NUMSEG; ARITH_RULE `1 <= x + 1`] THEN
 605     X_GEN_TAC `x:num` THEN STRIP_TAC THEN
 606     SUBGOAL_THEN `p * (q * x) DIV p + r < q * r` MP_TAC THENL
 607      [MATCH_MP_TAC LTE_TRANS THEN EXISTS_TAC `q * x` THEN
 608       ASM_REWRITE_TAC[LE_MULT_LCANCEL] THEN
 609       GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [MULT_SYM] THEN
 610       ASM_MESON_TAC[PRIME_IMP_NZ; LT_ADD_LCANCEL; DIVISION];
 611       MAP_EVERY EXPAND_TAC ["p"; "q"] THEN DISCH_THEN(MP_TAC o MATCH_MP
 612        (ARITH_RULE `(2 * r + 1) * d + r < (2 * s + 1) * r
 613                     ==> (2 * r) * d < (2 * r) * s`)) THEN
 614       SIMP_TAC[LT_MULT_LCANCEL; ARITH_RULE `x < y ==> x + 1 <= y`]];
 615     AP_TERM_TAC THEN
 616     REWRITE_TAC[EXTENSION; IN_ELIM_PAIR_THM; FORALL_PAIR_THM] THEN
 617     MAP_EVERY X_GEN_TAC [`x:num`; `y:num`] THEN
 618     AP_TERM_TAC THEN AP_TERM_TAC THEN EQ_TAC THEN DISCH_TAC THENL
 619      [MP_TAC(MATCH_MP PRIME_IMP_NZ (ASSUME `prime p`)) THEN
 620       DISCH_THEN(MP_TAC o SPEC `q * x` o MATCH_MP DIVISION) THEN
 621       FIRST_ASSUM(CONJUNCTS_THEN2 SUBST1_TAC MP_TAC) THEN
 622       UNDISCH_TAC `2 * r + 1 = p` THEN ARITH_TAC;
 623       MATCH_MP_TAC(TAUT `a /\ (a ==> b) ==> a /\ b`) THEN CONJ_TAC THENL
 624        [ALL_TAC;
 625         DISCH_THEN SUBST_ALL_TAC THEN
 626         MATCH_MP_TAC(ARITH_RULE
 627          `!p d. 2 * r + 1 = p /\ p * (d + 1) <= (d * p + m) + r ==> r < m`) THEN
 628         MAP_EVERY EXISTS_TAC [`p:num`; `(q * x) DIV p`] THEN
 629         ASM_MESON_TAC[DIVISION; PRIME_IMP_NZ]] THEN
 630       MATCH_MP_TAC(ARITH_RULE `~(x <= y) /\ ~(y + 2 <= x) ==> x = y + 1`) THEN
 631       REPEAT STRIP_TAC THENL
 632        [SUBGOAL_THEN `y * p <= ((q * x) DIV p) * p` MP_TAC THENL
 633          [ASM_SIMP_TAC[LE_MULT_RCANCEL; PRIME_IMP_NZ]; ALL_TAC];
 634         SUBGOAL_THEN `((q * x) DIV p + 2) * p <= y * p` MP_TAC THENL
 635          [ASM_SIMP_TAC[LE_MULT_RCANCEL; PRIME_IMP_NZ]; ALL_TAC]] THEN
 636       MP_TAC(MATCH_MP PRIME_IMP_NZ (ASSUME `prime p`)) THEN
 637       DISCH_THEN(MP_TAC o SPEC `q * x` o MATCH_MP DIVISION) THEN
 638       ASM_ARITH_TAC]]);;
 639
 640 let GAUSS_LEMMA_SYM' = prove
 641  (`!p q r s. prime p /\ prime q /\ coprime(p,q) /\
 642              2 * r + 1 = p /\ 2 * s + 1 = q
 643              ==> (p is_quadratic_residue (mod q) <=>
 644                   EVEN(CARD {x,y | x IN 1..r /\ y IN 1..s /\
 645                                    p * y < q * x /\ q * x <= p * y + s}))`,
 646   REPEAT STRIP_TAC THEN
 647   MP_TAC(SPECL [`q:num`; `p:num`; `s:num`; `r:num`] GAUSS_LEMMA_SYM) THEN
 648   ONCE_REWRITE_TAC[COPRIME_SYM] THEN ASM_REWRITE_TAC[] THEN
 649   DISCH_THEN SUBST1_TAC THEN AP_TERM_TAC THEN
 650   GEN_REWRITE_TAC LAND_CONV [CARD_SUBCROSS_SWAP] THEN
 651   AP_TERM_TAC THEN REWRITE_TAC[EXTENSION; FORALL_PAIR_THM] THEN
 652   REWRITE_TAC[IN_ELIM_PAIR_THM; CONJ_ACI]);;
 653
 654 (* ------------------------------------------------------------------------- *)
 655 (* The main result.                                                          *)
 656 (* ------------------------------------------------------------------------- *)
 657
 658 let RECIPROCITY_SET_LEMMA = prove
 659  (`!a b c d r s.
 660         a UNION b UNION c UNION d = (1..r) CROSS (1..s) /\
 661         PAIRWISE DISJOINT [a;b;c;d] /\ CARD b = CARD c
 662         ==> ((EVEN(CARD a) <=> EVEN(CARD d)) <=> ~(ODD r /\ ODD s))`,
 663   REPEAT STRIP_TAC THEN
 664   SUBGOAL_THEN `CARD(a:num#num->bool) + CARD(b:num#num->bool) +
 665                 CARD(c:num#num->bool) + CARD(d:num#num->bool) = r * s`
 666    (fun th -> MP_TAC(AP_TERM `EVEN` th) THEN
 667               ASM_REWRITE_TAC[EVEN_ADD; GSYM NOT_EVEN; EVEN_MULT] THEN
 668               CONV_TAC TAUT) THEN
 669   SUBGOAL_THEN
 670    `FINITE(a:num#num->bool) /\ FINITE(b:num#num->bool) /\
 671     FINITE(c:num#num->bool) /\ FINITE(d:num#num->bool)`
 672   STRIP_ASSUME_TAC THENL
 673    [REPEAT STRIP_TAC THEN MATCH_MP_TAC FINITE_SUBSET THEN
 674     EXISTS_TAC `(1..r) CROSS (1..s)` THEN
 675     SIMP_TAC[FINITE_CROSS; FINITE_NUMSEG] THEN
 676     FIRST_X_ASSUM(SUBST_ALL_TAC o SYM) THEN ASM SET_TAC[];
 677     ALL_TAC] THEN
 678   FIRST_X_ASSUM(MP_TAC o AP_TERM `CARD:(num#num->bool)->num`) THEN
 679   SIMP_TAC[CARD_CROSS; CARD_NUMSEG_1; FINITE_NUMSEG] THEN
 680   DISCH_THEN(SUBST1_TAC o SYM) THEN
 681   FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [PAIRWISE]) THEN
 682   REWRITE_TAC[PAIRWISE; DISJOINT; ALL] THEN
 683   ASM_SIMP_TAC[CARD_UNION; FINITE_UNION; SET_RULE
 684     `a INTER (b UNION c) = {} <=> a INTER b = {} /\ a INTER c = {}`]);;
 685
 686 let RECIPROCITY_SIMPLE = prove
 687  (`!p q r s.
 688         prime p /\
 689         prime q /\
 690         coprime (p,q) /\
 691         2 * r + 1 = p /\
 692         2 * s + 1 = q
 693         ==> ((q is_quadratic_residue (mod p) <=>
 694               p is_quadratic_residue (mod q)) <=>
 695              ~(ODD r /\ ODD s))`,
 696   REPEAT STRIP_TAC THEN
 697   MP_TAC(SPECL [`p:num`; `q:num`; `r:num`; `s:num`] GAUSS_LEMMA_SYM) THEN
 698   MP_TAC(SPECL [`p:num`; `q:num`; `r:num`; `s:num`] GAUSS_LEMMA_SYM') THEN
 699   ASM_REWRITE_TAC[] THEN
 700   ONCE_REWRITE_TAC[COPRIME_SYM] THEN ASM_REWRITE_TAC[] THEN
 701   REPEAT(DISCH_THEN SUBST1_TAC) THEN MATCH_MP_TAC RECIPROCITY_SET_LEMMA THEN
 702   EXISTS_TAC `{x,y | x IN 1..r /\ y IN 1..s /\ q * x + r < p * y}` THEN
 703   EXISTS_TAC `{x,y | x IN 1..r /\ y IN 1..s /\ p * y + s < q * x}` THEN
 704   REPEAT CONJ_TAC THEN
 705   REWRITE_TAC[PAIRWISE; DISJOINT; EXTENSION; NOT_IN_EMPTY; FORALL_PAIR_THM;
 706               ALL; IN_UNION; IN_CROSS; IN_ELIM_PAIR_THM; IN_INTER]
 707   THENL
 708    [MAP_EVERY X_GEN_TAC [`x:num`; `y:num`] THEN
 709     MAP_EVERY ASM_CASES_TAC [`x IN 1..r`; `y IN 1..s`] THEN ASM_SIMP_TAC[] THEN
 710     SUBGOAL_THEN `~(q * x = p * y)` (fun th -> MP_TAC th THEN ARITH_TAC) THEN
 711     DISCH_THEN(MP_TAC o AP_TERM `(divides) p`) THEN
 712     ASM_SIMP_TAC[PRIME_DIVPROD_EQ; DIVIDES_REFL] THEN STRIP_TAC THENL
 713      [ASM_MESON_TAC[DIVIDES_REFL; PRIME_1; coprime]; ALL_TAC] THEN
 714     FIRST_X_ASSUM(MP_TAC o MATCH_MP DIVIDES_LE) THEN
 715     UNDISCH_TAC `x IN 1..r` THEN REWRITE_TAC[IN_NUMSEG] THEN
 716     EXPAND_TAC "p" THEN ARITH_TAC;
 717     ARITH_TAC;
 718     MATCH_MP_TAC BIJECTIONS_CARD_EQ THEN
 719     REPEAT(EXISTS_TAC `\(x,y). (r + 1) - x,(s + 1) - y`) THEN
 720     SIMP_TAC[FINITE_SUBCROSS; FINITE_NUMSEG] THEN
 721     REWRITE_TAC[FORALL_PAIR_THM; IN_ELIM_PAIR_THM; IN_NUMSEG; PAIR_EQ] THEN
 722     CONJ_TAC THEN MAP_EVERY X_GEN_TAC [`x:num`; `y:num`] THEN
 723     SIMP_TAC[ARITH_RULE `x <= y ==> (y + 1) - ((y + 1) - x) = x`] THEN
 724     SIMP_TAC[ARITH_RULE
 725      `1 <= x /\ x <= y ==> 1 <= (y + 1) - x /\ (y + 1) - x <= y`] THEN
 726     REWRITE_TAC[LEFT_SUB_DISTRIB] THEN REPEAT STRIP_TAC THEN
 727     MATCH_MP_TAC(ARITH_RULE
 728      `x <= y /\ v + y + z < x + u ==> (y - x) + z < u - v`) THEN
 729     ASM_SIMP_TAC[LE_MULT_LCANCEL; ARITH_RULE `x <= r ==> x <= r + 1`] THEN
 730     REWRITE_TAC[ARITH_RULE `a + x < y + a <=> x < y`] THEN
 731     REPEAT(FIRST_X_ASSUM(SUBST_ALL_TAC o SYM)) THEN
 732     ASM_ARITH_TAC]);;
 733
 734 (* ------------------------------------------------------------------------- *)
 735 (* In terms of the Legendre symbol.                                          *)
 736 (* ------------------------------------------------------------------------- *)
 737
 738 let RECIPROCITY_LEGENDRE = prove
 739  (`!p q. prime p /\ prime q /\ ODD p /\ ODD q /\ ~(p = q)
 740          ==> legendre(p,q) * legendre(q,p) =
 741              --(&1) pow ((p - 1) DIV 2 * (q - 1) DIV 2)`,
 742   REPEAT STRIP_TAC THEN MAP_EVERY UNDISCH_TAC [`ODD q`; `ODD p`] THEN
 743   REWRITE_TAC[ODD_EXISTS; LEFT_IMP_EXISTS_THM; RIGHT_IMP_FORALL_THM] THEN
 744   MAP_EVERY X_GEN_TAC [`r:num`; `s:num`] THEN REWRITE_TAC[ADD1] THEN
 745   REPEAT(DISCH_THEN (fun th -> SUBST1_TAC th THEN ASSUME_TAC(SYM th))) THEN
 746   REWRITE_TAC[ARITH_RULE `((2 * s + 1) - 1) DIV 2 = s`] THEN
 747   MP_TAC(SPECL [`p:num`; `q:num`; `r:num`; `s:num`] RECIPROCITY_SIMPLE) THEN
 748   ASM_SIMP_TAC[DISTINCT_PRIME_COPRIME; INT_POW_NEG; EVEN_MULT; legendre] THEN
 749   REWRITE_TAC[DE_MORGAN_THM; NOT_ODD; INT_POW_ONE] THEN
 750   MAP_EVERY ASM_CASES_TAC [`EVEN r`; `EVEN s`] THEN ASM_REWRITE_TAC[] THEN
 751   SIMP_TAC[TAUT `~(a <=> b) <=> (a <=> ~b)`] THEN DISCH_THEN(K ALL_TAC) THEN
 752   ASM_CASES_TAC `p is_quadratic_residue (mod q)` THEN
 753   ASM_REWRITE_TAC[INT_MUL_LNEG; INT_MUL_RNEG; INT_NEG_NEG; INT_MUL_LID]);;