100/two_squares.ml

   1 (* ========================================================================= *)
   2 (* Representation of primes == 1 (mod 4) as sum of 2 squares.                *)
   3 (* ========================================================================= *)
   4
   5 needs "Library/prime.ml";;
   6
   7 prioritize_num();;
   8
   9 (* ------------------------------------------------------------------------- *)
  10 (* Definition of involution and various basic lemmas.                        *)
  11 (* ------------------------------------------------------------------------- *)
  12
  13 let involution = new_definition
  14   `involution f s = !x. x IN s ==> f(x) IN s /\ (f(f(x)) = x)`;;
  15
  16 let INVOLUTION_IMAGE = prove
  17  (`!f s. involution f s ==> (IMAGE f s = s)`,
  18   REWRITE_TAC[involution; EXTENSION; IN_IMAGE] THEN MESON_TAC[]);;
  19
  20 let INVOLUTION_DELETE = prove
  21  (`involution f s /\ a IN s /\ (f a = a) ==> involution f (s DELETE a)`,
  22   REWRITE_TAC[involution; IN_DELETE] THEN MESON_TAC[]);;
  23
  24 let INVOLUTION_STEPDOWN = prove
  25  (`involution f s /\ a IN s ==> involution f (s DIFF {a, (f a)})`,
  26   REWRITE_TAC[involution; IN_DIFF; IN_INSERT; NOT_IN_EMPTY] THEN MESON_TAC[]);;
  27
  28 let INVOLUTION_NOFIXES = prove
  29  (`involution f s ==> involution f {x | x IN s /\ ~(f x = x)}`,
  30   REWRITE_TAC[involution; IN_ELIM_THM] THEN MESON_TAC[]);;
  31
  32 let INVOLUTION_SUBSET = prove
  33  (`!f s t. involution f s /\ (!x. x IN t ==> f(x) IN t) /\ t SUBSET s
  34            ==> involution f t`,
  35   REWRITE_TAC[involution; SUBSET] THEN MESON_TAC[]);;
  36
  37 (* ------------------------------------------------------------------------- *)
  38 (* Involution with no fixpoints can only occur on finite set of even card    *)
  39 (* ------------------------------------------------------------------------- *)
  40
  41 let INVOLUTION_EVEN_STEP = prove
  42  (`FINITE(s) /\
  43    involution f s /\
  44    (!x:A. x IN s ==> ~(f x = x)) /\
  45    a IN s
  46    ==> FINITE(s DIFF {a, (f a)}) /\
  47        involution f (s DIFF {a, (f a)}) /\
  48        (!x:A. x IN (s DIFF {a, (f a)}) ==> ~(f x = x)) /\
  49        (CARD s = CARD(s DIFF {a, (f a)}) + 2)`,
  50   SIMP_TAC[FINITE_DIFF; INVOLUTION_STEPDOWN; IN_DIFF] THEN STRIP_TAC THEN
  51   SUBGOAL_THEN `s = (a:A) INSERT (f a) INSERT (s DIFF {a, (f a)})` MP_TAC THENL
  52    [REWRITE_TAC[EXTENSION; IN_INSERT; IN_DIFF; NOT_IN_EMPTY] THEN
  53     ASM_MESON_TAC[involution]; ALL_TAC] THEN
  54   DISCH_THEN(fun th -> GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [th]) THEN
  55   ASM_SIMP_TAC[CARD_CLAUSES; FINITE_DIFF; FINITE_INSERT] THEN
  56   ASM_SIMP_TAC[IN_INSERT; IN_DIFF; NOT_IN_EMPTY] THEN ARITH_TAC);;
  57
  58 let INVOLUTION_EVEN_INDUCT = prove
  59  (`!n s. FINITE(s) /\ (CARD s = n) /\ involution f s /\
  60          (!x:A. x IN s ==> ~(f x = x))
  61          ==> EVEN(CARD s)`,
  62   MATCH_MP_TAC num_WF THEN GEN_TAC THEN DISCH_TAC THEN GEN_TAC THEN
  63   ASM_CASES_TAC `s:A->bool = {}` THEN
  64   ASM_REWRITE_TAC[CARD_CLAUSES; ARITH] THEN
  65   FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE RAND_CONV [EXTENSION]) THEN
  66   REWRITE_TAC[NOT_IN_EMPTY; NOT_FORALL_THM] THEN
  67   DISCH_THEN(X_CHOOSE_THEN `a:A` STRIP_ASSUME_TAC) THEN STRIP_TAC THEN
  68   FIRST_X_ASSUM(MP_TAC o SPEC `CARD(s DIFF {a:A, (f a)})`) THEN
  69   REWRITE_TAC[RIGHT_IMP_FORALL_THM] THEN
  70   DISCH_THEN(MP_TAC o SPEC `s DIFF {a:A, (f a)}`) THEN
  71   MP_TAC INVOLUTION_EVEN_STEP THEN ASM_REWRITE_TAC[] THEN
  72   STRIP_TAC THEN ASM_REWRITE_TAC[ARITH_RULE `n < n + 2`] THEN
  73   SIMP_TAC[EVEN_ADD; ARITH]);;
  74
  75 let INVOLUTION_EVEN = prove
  76  (`!s. FINITE(s) /\ involution f s /\ (!x:A. x IN s ==> ~(f x = x))
  77        ==> EVEN(CARD s)`,
  78   MESON_TAC[INVOLUTION_EVEN_INDUCT]);;
  79
  80 (* ------------------------------------------------------------------------- *)
  81 (* So an involution with exactly one fixpoint has odd card domain.           *)
  82 (* ------------------------------------------------------------------------- *)
  83
  84 let INVOLUTION_FIX_ODD = prove
  85  (`FINITE(s) /\ involution f s /\ (?!a:A. a IN s /\ (f a = a))
  86    ==> ODD(CARD s)`,
  87   REWRITE_TAC[EXISTS_UNIQUE_DEF] THEN STRIP_TAC THEN
  88   SUBGOAL_THEN `s = (a:A) INSERT (s DELETE a)` SUBST1_TAC THENL
  89    [REWRITE_TAC[EXTENSION; IN_INSERT; IN_DELETE] THEN ASM_MESON_TAC[];
  90     ALL_TAC] THEN
  91   ASM_SIMP_TAC[CARD_CLAUSES; FINITE_DELETE; IN_DELETE; ODD; NOT_ODD] THEN
  92   MATCH_MP_TAC INVOLUTION_EVEN THEN
  93   ASM_SIMP_TAC[INVOLUTION_DELETE; FINITE_DELETE; IN_DELETE] THEN
  94   ASM_MESON_TAC[]);;
  95
  96 (* ------------------------------------------------------------------------- *)
  97 (* And an involution on a set of odd finite card must have a fixpoint.       *)
  98 (* ------------------------------------------------------------------------- *)
  99
 100 let INVOLUTION_ODD = prove
 101  (`!n s. FINITE(s) /\ involution f s /\ ODD(CARD s)
 102          ==> ?a. a IN s /\ (f a = a)`,
 103   REWRITE_TAC[GSYM NOT_EVEN] THEN MESON_TAC[INVOLUTION_EVEN]);;
 104
 105 (* ------------------------------------------------------------------------- *)
 106 (* Consequently, if one involution has a unique fixpoint, other has one.     *)
 107 (* ------------------------------------------------------------------------- *)
 108
 109 let INVOLUTION_FIX_FIX = prove
 110  (`!f g s. FINITE(s) /\ involution f s /\ involution g s /\
 111            (?!x. x IN s /\ (f x = x)) ==> ?x. x IN s /\ (g x = x)`,
 112   REPEAT STRIP_TAC THEN MATCH_MP_TAC INVOLUTION_ODD THEN
 113   ASM_REWRITE_TAC[] THEN MATCH_MP_TAC INVOLUTION_FIX_ODD THEN
 114   ASM_REWRITE_TAC[]);;
 115
 116 (* ------------------------------------------------------------------------- *)
 117 (* Formalization of Zagier's "one-sentence" proof over the natural numbers.  *)
 118 (* ------------------------------------------------------------------------- *)
 119
 120 let zset = new_definition
 121   `zset(a) = {(x,y,z) | x EXP 2 + 4 * y * z = a}`;;
 122
 123 let zag = new_definition
 124   `zag(x,y,z) =
 125         if x + z < y then (x + 2 * z,z,y - (x + z))
 126         else if x < 2 * y then (2 * y - x, y, (x + z) - y)
 127         else (x - 2 * y,(x + z) - y, y)`;;
 128
 129 let tag = new_definition
 130   `tag((x,y,z):num#num#num) = (x,z,y)`;;
 131
 132 let ZAG_INVOLUTION_GENERAL = prove
 133  (`0 < x /\ 0 < y /\ 0 < z ==> (zag(zag(x,y,z)) = (x,y,z))`,
 134   REWRITE_TAC[zag] THEN REPEAT(COND_CASES_TAC THEN ASM_REWRITE_TAC[]) THEN
 135   REWRITE_TAC[zag] THEN REPEAT(COND_CASES_TAC THEN ASM_REWRITE_TAC[]) THEN
 136   REWRITE_TAC[PAIR_EQ] THEN
 137   POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN ARITH_TAC);;
 138
 139 let IN_TRIPLE = prove
 140  (`(a,b,c) IN {(x,y,z) | P x y z} <=> P a b c`,
 141   REWRITE_TAC[IN_ELIM_THM; PAIR_EQ] THEN MESON_TAC[]);;
 142
 143 let PRIME_SQUARE = prove
 144  (`!n. ~prime(n * n)`,
 145   GEN_TAC THEN ASM_CASES_TAC `n = 0` THEN
 146   ASM_REWRITE_TAC[PRIME_0; MULT_CLAUSES] THEN
 147   REWRITE_TAC[prime; NOT_FORALL_THM; DE_MORGAN_THM] THEN
 148   ASM_CASES_TAC `n = 1` THEN ASM_REWRITE_TAC[ARITH] THEN
 149   DISJ2_TAC THEN EXISTS_TAC `n:num` THEN
 150   ASM_SIMP_TAC[DIVIDES_LMUL; DIVIDES_REFL] THEN
 151   GEN_REWRITE_TAC (RAND_CONV o LAND_CONV) [ARITH_RULE `n = n * 1`] THEN
 152   ASM_SIMP_TAC[EQ_MULT_LCANCEL]);;
 153
 154 let PRIME_4X = prove
 155  (`!n. ~prime(4 * n)`,
 156   GEN_TAC THEN REWRITE_TAC[prime; NOT_FORALL_THM; DE_MORGAN_THM] THEN
 157   DISJ2_TAC THEN EXISTS_TAC `2` THEN
 158   SUBST1_TAC(SYM(NUM_REDUCE_CONV `2 * 2`)) THEN
 159   ASM_SIMP_TAC[GSYM MULT_ASSOC; DIVIDES_RMUL; DIVIDES_REFL; ARITH_EQ] THEN
 160   ASM_CASES_TAC `n = 0` THEN POP_ASSUM MP_TAC THEN ARITH_TAC);;
 161
 162 let PRIME_XYZ_NONZERO = prove
 163  (`prime(x EXP 2 + 4 * y * z) ==> 0 < x /\ 0 < y /\ 0 < z`,
 164   CONV_TAC CONTRAPOS_CONV THEN
 165   REWRITE_TAC[DE_MORGAN_THM; ARITH_RULE `~(0 < x) = (x = 0)`] THEN
 166   DISCH_THEN(REPEAT_TCL DISJ_CASES_THEN SUBST1_TAC) THEN
 167   REWRITE_TAC[EXP_2; MULT_CLAUSES; ADD_CLAUSES; PRIME_SQUARE; PRIME_4X]);;
 168
 169 let ZAG_INVOLUTION = prove
 170  (`!p. prime(p) ==> involution zag (zset(p))`,
 171   REPEAT STRIP_TAC THEN REWRITE_TAC[involution; FORALL_PAIR_THM] THEN
 172   MAP_EVERY X_GEN_TAC [`x:num`; `y:num`; `z:num`] THEN
 173   REWRITE_TAC[zset; IN_TRIPLE] THEN DISCH_THEN(SUBST_ALL_TAC o SYM) THEN
 174   CONJ_TAC THENL
 175    [REWRITE_TAC[zag] THEN REPEAT COND_CASES_TAC THEN
 176     ASM_REWRITE_TAC[IN_TRIPLE] THEN
 177     RULE_ASSUM_TAC(REWRITE_RULE[NOT_LT]) THEN
 178     ASM_SIMP_TAC[GSYM INT_OF_NUM_EQ; GSYM INT_OF_NUM_ADD; EXP_2;
 179                  GSYM INT_OF_NUM_MUL; GSYM INT_OF_NUM_SUB; LT_IMP_LE] THEN
 180     INT_ARITH_TAC;
 181     MATCH_MP_TAC ZAG_INVOLUTION_GENERAL THEN
 182     ASM_MESON_TAC[PRIME_XYZ_NONZERO]]);;
 183
 184 let TAG_INVOLUTION = prove
 185  (`!a. involution tag (zset a)`,
 186   REWRITE_TAC[involution; tag; zset; FORALL_PAIR_THM] THEN
 187   REWRITE_TAC[IN_TRIPLE] THEN REWRITE_TAC[MULT_AC]);;
 188
 189 let ZAG_LEMMA = prove
 190  (`(zag(x,y,z) = (x,y,z)) ==> (y = x)`,
 191   REWRITE_TAC[zag; INT_POW_2] THEN
 192   REPEAT(COND_CASES_TAC THEN ASM_SIMP_TAC[PAIR_EQ]) THEN
 193   POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN ARITH_TAC);;
 194
 195 let ZSET_BOUND = prove
 196  (`0 < y /\ 0 < z /\ (x EXP 2 + 4 * y * z = p)
 197    ==> x <= p /\ y <= p /\ z <= p`,
 198   REPEAT GEN_TAC THEN STRIP_TAC THEN
 199   FIRST_X_ASSUM(SUBST1_TAC o SYM) THEN CONJ_TAC THENL
 200    [MESON_TAC[EXP_2; LE_SQUARE_REFL; ARITH_RULE `(a <= b ==> a <= b + c)`];
 201     CONJ_TAC THEN MATCH_MP_TAC(ARITH_RULE `y <= z ==> y <= x + z`) THENL
 202      [GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [MULT_SYM]; ALL_TAC] THEN
 203     REWRITE_TAC[ARITH_RULE `y <= 4 * a * y <=> 1 * y <= (4 * a) * y`] THEN
 204     ASM_REWRITE_TAC[LE_MULT_RCANCEL] THEN
 205     ASM_SIMP_TAC[ARITH_RULE `0 < a ==> 1 <= 4 * a`]]);;
 206
 207 let ZSET_FINITE = prove
 208  (`!p. prime(p) ==> FINITE(zset p)`,
 209   GEN_TAC THEN DISCH_TAC THEN
 210   MP_TAC(SPEC `p + 1` FINITE_NUMSEG_LT) THEN
 211   DISCH_THEN(fun th ->
 212     MP_TAC(funpow 2 (MATCH_MP FINITE_PRODUCT o CONJ th) th)) THEN
 213   MATCH_MP_TAC(REWRITE_RULE[TAUT `a /\ b ==> c <=> b ==> a ==> c`]
 214     FINITE_SUBSET) THEN
 215   REWRITE_TAC[zset; SUBSET; FORALL_PAIR_THM; IN_TRIPLE] THEN
 216   MAP_EVERY X_GEN_TAC [`x:num`; `y:num`; `z:num`] THEN
 217   REWRITE_TAC[IN_ELIM_THM; EXISTS_PAIR_THM; PAIR_EQ] THEN
 218   REWRITE_TAC[ARITH_RULE `x < p + 1 <=> x <= p`; PAIR_EQ] THEN
 219   DISCH_TAC THEN MAP_EVERY EXISTS_TAC [`x:num`; `y:num`; `z:num`] THEN
 220   ASM_REWRITE_TAC[] THEN REWRITE_TAC[RIGHT_AND_EXISTS_THM] THEN
 221   MAP_EVERY EXISTS_TAC [`y:num`; `z:num`] THEN REWRITE_TAC[] THEN
 222   ASM_MESON_TAC[ZSET_BOUND; PRIME_XYZ_NONZERO]);;
 223
 224 let SUM_OF_TWO_SQUARES = prove
 225  (`!p k. prime(p) /\ (p = 4 * k + 1) ==> ?x y. p = x EXP 2 + y EXP 2`,
 226   SIMP_TAC[] THEN REPEAT STRIP_TAC THEN
 227   SUBGOAL_THEN `?t. t IN zset(p) /\ (tag(t) = t)` MP_TAC THENL
 228    [ALL_TAC;
 229     REWRITE_TAC[LEFT_IMP_EXISTS_THM; FORALL_PAIR_THM; tag; PAIR_EQ] THEN
 230     REWRITE_TAC[zset; IN_TRIPLE; EXP_2] THEN
 231     ASM_MESON_TAC[ARITH_RULE `4 * x * y = (2 * x) * (2 * y)`]] THEN
 232   MATCH_MP_TAC INVOLUTION_FIX_FIX THEN EXISTS_TAC `zag` THEN
 233   ASM_SIMP_TAC[ZAG_INVOLUTION; TAG_INVOLUTION; ZSET_FINITE] THEN
 234   REWRITE_TAC[EXISTS_UNIQUE_ALT] THEN EXISTS_TAC `1,1,k:num` THEN
 235   REWRITE_TAC[FORALL_PAIR_THM] THEN
 236   MAP_EVERY X_GEN_TAC [`x:num`; `y:num`; `z:num`] THEN EQ_TAC THENL
 237    [ALL_TAC;
 238     DISCH_THEN(SUBST1_TAC o SYM) THEN
 239     REWRITE_TAC[zset; zag; IN_TRIPLE; ARITH] THEN
 240     REWRITE_TAC[MULT_CLAUSES; ARITH_RULE `~(1 + k < 1)`; PAIR_EQ] THEN
 241     ARITH_TAC] THEN
 242   REWRITE_TAC[zset; IN_TRIPLE] THEN STRIP_TAC THEN
 243   FIRST_ASSUM(SUBST_ALL_TAC o MATCH_MP ZAG_LEMMA) THEN
 244   UNDISCH_TAC `x EXP 2 + 4 * x * z = 4 * k + 1` THEN
 245   REWRITE_TAC[EXP_2; ARITH_RULE `x * x + 4 * x * z = x * (4 * z + x)`] THEN
 246   DISCH_THEN(ASSUME_TAC o SYM) THEN UNDISCH_TAC `prime p` THEN
 247   ASM_REWRITE_TAC[] THEN REWRITE_TAC[prime] THEN
 248   DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC (MP_TAC o SPEC `x:num`)) THEN
 249   SIMP_TAC[DIVIDES_RMUL; DIVIDES_REFL] THEN
 250   DISCH_THEN(DISJ_CASES_THEN2 SUBST_ALL_TAC MP_TAC) THENL
 251    [UNDISCH_TAC `4 * k + 1 = 1 * (4 * z + 1)` THEN
 252     REWRITE_TAC[MULT_CLAUSES; PAIR_EQ] THEN ARITH_TAC;
 253     ONCE_REWRITE_TAC[ARITH_RULE `(a = a * b) = (a * b = a * 1)`] THEN
 254     ASM_SIMP_TAC[EQ_MULT_LCANCEL] THEN STRIP_TAC THENL
 255      [UNDISCH_TAC `4 * k + 1 = x * (4 * z + x)` THEN
 256       ASM_REWRITE_TAC[MULT_CLAUSES; ADD_EQ_0; ARITH_EQ];
 257       UNDISCH_TAC `4 * z + x = 1` THEN REWRITE_TAC[PAIR_EQ] THEN
 258       ASM_CASES_TAC `z = 0` THENL
 259        [ALL_TAC; UNDISCH_TAC `~(z = 0)` THEN ARITH_TAC] THEN
 260       UNDISCH_TAC `4 * k + 1 = x * (4 * z + x)` THEN
 261       ASM_REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES] THEN
 262       ASM_CASES_TAC `x = 1` THEN ASM_REWRITE_TAC[] THEN
 263       REWRITE_TAC[MULT_CLAUSES] THEN ARITH_TAC]]);;