100/perfect.ml

   1 (* ========================================================================= *)
   2 (* Perfect number theorems.                                                  *)
   3 (* ========================================================================= *)
   4
   5 needs "Library/prime.ml";;
   6
   7 prioritize_num();;
   8
   9 (* ------------------------------------------------------------------------- *)
  10 (* The sum-of-divisors function.                                             *)
  11 (* ------------------------------------------------------------------------- *)
  12
  13 let sigma = new_definition
  14  `sigma(n) = if n = 0 then 0 else nsum {d | d divides n} (\i. i)`;;
  15
  16 (* ------------------------------------------------------------------------- *)
  17 (* Definition of perfection.                                                 *)
  18 (* ------------------------------------------------------------------------- *)
  19
  20 let perfect = new_definition
  21  `perfect n <=> ~(n = 0) /\ sigma(n) = 2 * n`;;
  22
  23 (* ------------------------------------------------------------------------- *)
  24 (* Various number-theoretic lemmas.                                          *)
  25 (* ------------------------------------------------------------------------- *)
  26
  27 let ODD_POW2_MINUS1 = prove
  28  (`!k. ~(k = 0) ==> ODD(2 EXP k - 1)`,
  29   REPEAT STRIP_TAC THEN
  30   SUBGOAL_THEN `EVEN(2 EXP k) <=> EVEN((2 EXP k - 1) + 1)` MP_TAC THENL
  31    [AP_TERM_TAC THEN REWRITE_TAC[ARITH_RULE `k = k - 1 + 1 <=> ~(k = 0)`] THEN
  32     REWRITE_TAC[EXP_EQ_0; ARITH];
  33     ASM_REWRITE_TAC[GSYM NOT_EVEN; EVEN_ADD; EVEN_EXP; ARITH]]);;
  34
  35 let EVEN_ODD_DECOMP = prove
  36  (`!n. ~(n = 0) ==> ?r s. ODD s /\ n = 2 EXP r * s`,
  37   MATCH_MP_TAC num_WF THEN X_GEN_TAC `n:num` THEN
  38   MP_TAC(SPEC `n:num` EVEN_OR_ODD) THEN
  39   REWRITE_TAC[EVEN_EXISTS; ODD_EXISTS] THEN
  40   DISCH_THEN(DISJ_CASES_THEN (X_CHOOSE_THEN `m:num` SUBST_ALL_TAC)) THENL
  41    [DISCH_THEN(MP_TAC o SPEC `m:num`) THEN
  42     REWRITE_TAC[MULT_EQ_0; ARITH; ARITH_RULE `m < 2 * m <=> ~(m = 0)`] THEN
  43     ASM_CASES_TAC `m = 0` THEN ASM_REWRITE_TAC[] THEN
  44     ONCE_REWRITE_TAC[SWAP_EXISTS_THM] THEN MATCH_MP_TAC MONO_EXISTS THEN
  45     X_GEN_TAC `s:num` THEN DISCH_THEN(X_CHOOSE_TAC `r:num`) THEN
  46     EXISTS_TAC `SUC r` THEN ASM_REWRITE_TAC[EXP; GSYM MULT_ASSOC];
  47     REPEAT(DISCH_THEN(K ALL_TAC)) THEN EXISTS_TAC `0` THEN
  48     REWRITE_TAC[EXP; MULT_CLAUSES] THEN MESON_TAC[]]);;
  49
  50 let FINITE_DIVISORS = prove
  51  (`!n. ~(n = 0) ==> FINITE {d | d divides n}`,
  52   REPEAT STRIP_TAC THEN MATCH_MP_TAC FINITE_SUBSET THEN
  53   EXISTS_TAC `{d | d <= n}` THEN REWRITE_TAC[FINITE_NUMSEG_LE] THEN
  54   REWRITE_TAC[SUBSET; IN_ELIM_THM] THEN ASM_MESON_TAC[DIVIDES_LE]);;
  55
  56 let MULT_EQ_COPRIME = prove
  57  (`!a b x y. a * b = x * y /\ coprime(a,x)
  58              ==> ?d. y = a * d /\ b = x * d`,
  59   REPEAT STRIP_TAC THEN
  60   MP_TAC(SPECL [`a:num`; `x:num`; `y:num`] COPRIME_DIVPROD) THEN
  61   MP_TAC(SPECL [`x:num`; `a:num`; `b:num`] COPRIME_DIVPROD) THEN
  62   REPEAT(ANTS_TAC THENL
  63    [ASM_MESON_TAC[DIVIDES_REFL; DIVIDES_RMUL; COPRIME_SYM];
  64     REWRITE_TAC[divides] THEN STRIP_TAC]) THEN
  65   UNDISCH_TAC `a * b = x * y` THEN ASM_REWRITE_TAC[] THEN
  66   REWRITE_TAC[ARITH_RULE
  67     `(a * x * u = x * a * v) <=> (a * x) * u = (a * x) * v`] THEN
  68   REWRITE_TAC[EQ_MULT_LCANCEL; MULT_EQ_0] THEN ASM_MESON_TAC[]);;
  69
  70 let COPRIME_ODD_POW2 = prove
  71  (`!k n. ODD(n) ==> coprime(2 EXP k,n)`,
  72   SIMP_TAC[coprime; PRIME_2; DIVIDES_PRIMEPOW] THEN REWRITE_TAC[divides] THEN
  73   REPEAT STRIP_TAC THEN UNDISCH_TAC `ODD n` THEN ASM_REWRITE_TAC[] THEN
  74   SIMP_TAC[ODD_MULT; ODD_EXP; ARITH]);;
  75
  76 let MULT_NSUM = prove
  77  (`!s t. FINITE s /\ FINITE t
  78          ==> nsum s f * nsum t g =
  79              nsum {(x:A,y:B) | x IN s /\ y IN t} (\(x,y). f(x) * g(y))`,
  80   SIMP_TAC[GSYM NSUM_NSUM_PRODUCT; NSUM_LMUL; NSUM_RMUL]);;
  81
  82 (* ------------------------------------------------------------------------- *)
  83 (* Some elementary properties of the sigma function.                         *)
  84 (* ------------------------------------------------------------------------- *)
  85
  86 let SIGMA_0 = prove
  87  (`sigma 0 = 0`,
  88   REWRITE_TAC[sigma]);;
  89
  90 let SIGMA_1 = prove
  91  (`sigma(1) = 1`,
  92   REWRITE_TAC[sigma; DIVIDES_ONE; SET_RULE `{d | d = 1} = {1}`] THEN
  93   REWRITE_TAC[ARITH; NSUM_SING]);;
  94
  95 let SIGMA_LBOUND = prove
  96  (`!n. 1 < n ==> n + 1 <= sigma(n)`,
  97   REPEAT STRIP_TAC THEN
  98   FIRST_ASSUM(ASSUME_TAC o MATCH_MP (ARITH_RULE `1 < n ==> ~(n = 0)`)) THEN
  99   ASM_REWRITE_TAC[sigma] THEN MATCH_MP_TAC LE_TRANS THEN
 100   EXISTS_TAC `nsum {1,n} (\i. i)` THEN CONJ_TAC THENL
 101    [SIMP_TAC[NSUM_CLAUSES; FINITE_RULES; IN_SING; NOT_IN_EMPTY] THEN
 102     ASM_ARITH_TAC;
 103     MATCH_MP_TAC NSUM_SUBSET_SIMPLE THEN ASM_SIMP_TAC[FINITE_DIVISORS] THEN
 104     REWRITE_TAC[SUBSET; IN_ELIM_THM; NOT_IN_EMPTY; IN_INSERT] THEN
 105     MESON_TAC[DIVIDES_1; DIVIDES_REFL]]);;
 106
 107 let SIGMA_MULT = prove
 108  (`!a b. 1 < a /\ 1 < b ==> 1 + b + a * b <= sigma(a * b)`,
 109   REPEAT STRIP_TAC THEN
 110   EVERY_ASSUM(ASSUME_TAC o MATCH_MP (ARITH_RULE `1 < n ==> ~(n = 0)`)) THEN
 111   ASM_REWRITE_TAC[sigma] THEN MATCH_MP_TAC LE_TRANS THEN
 112   EXISTS_TAC `nsum {1,b,a*b} (\i. i)` THEN CONJ_TAC THENL
 113    [SIMP_TAC[NSUM_CLAUSES; FINITE_RULES; IN_INSERT; NOT_IN_EMPTY] THEN
 114     ONCE_REWRITE_TAC[ARITH_RULE `x = a * b <=> a * b = 1 * x`] THEN
 115     ASM_REWRITE_TAC[EQ_MULT_RCANCEL] THEN
 116     REWRITE_TAC[MULT_CLAUSES; MULT_EQ_1] THEN
 117     ASM_ARITH_TAC;
 118     ASM_REWRITE_TAC[MULT_EQ_0] THEN
 119     MATCH_MP_TAC NSUM_SUBSET_SIMPLE THEN
 120     ASM_SIMP_TAC[FINITE_DIVISORS; MULT_EQ_0] THEN
 121     REWRITE_TAC[SUBSET; IN_ELIM_THM; NOT_IN_EMPTY; IN_INSERT] THEN
 122     MESON_TAC[DIVIDES_1; DIVIDES_REFL; DIVIDES_LMUL]]);;
 123
 124 let SIGMA_PRIME = prove
 125  (`!p. prime(p) ==> sigma(p) = p + 1`,
 126   GEN_TAC THEN
 127   ASM_CASES_TAC `p = 0` THEN ASM_REWRITE_TAC[PRIME_0; SIGMA_0; ARITH] THEN
 128   ASM_CASES_TAC `p = 1` THEN ASM_REWRITE_TAC[PRIME_1; SIGMA_1; ARITH] THEN
 129   DISCH_TAC THEN ASM_REWRITE_TAC[sigma] THEN
 130   MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC `nsum {1,p} (\i. i)` THEN
 131   CONJ_TAC THENL
 132    [AP_THM_TAC THEN AP_TERM_TAC THEN
 133     REWRITE_TAC[EXTENSION; IN_ELIM_THM; IN_INSERT; NOT_IN_EMPTY] THEN
 134     ASM_MESON_TAC[prime; DIVIDES_1; DIVIDES_REFL];
 135     ASM_SIMP_TAC[NSUM_CLAUSES; IN_SING; FINITE_RULES; NOT_IN_EMPTY] THEN
 136     ARITH_TAC]);;
 137
 138 let SIGMA_PRIME_EQ = prove
 139  (`!p. prime(p) <=> sigma(p) = p + 1`,
 140   GEN_TAC THEN EQ_TAC THEN REWRITE_TAC[SIGMA_PRIME] THEN
 141   ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN
 142   REWRITE_TAC[prime; DE_MORGAN_THM] THEN
 143   ASM_CASES_TAC `p = 1` THEN ASM_REWRITE_TAC[SIGMA_1; ARITH] THEN
 144   REWRITE_TAC[NOT_FORALL_THM; NOT_IMP; divides; DE_MORGAN_THM] THEN
 145   DISCH_THEN(X_CHOOSE_THEN `a:num` (CONJUNCTS_THEN2 MP_TAC ASSUME_TAC)) THEN
 146   DISCH_THEN(X_CHOOSE_THEN `b:num` SUBST_ALL_TAC) THEN
 147   MP_TAC(SPECL [`a:num`; `b:num`] SIGMA_MULT) THEN
 148   ASM_CASES_TAC `a = 0` THEN ASM_REWRITE_TAC[MULT_CLAUSES; SIGMA_0; ARITH] THEN
 149   ASM_CASES_TAC `b = 0` THEN ASM_REWRITE_TAC[MULT_CLAUSES; SIGMA_0; ARITH] THEN
 150   REPEAT(POP_ASSUM MP_TAC) THEN REWRITE_TAC[MULT_EQ_1] THEN
 151   ONCE_REWRITE_TAC[ARITH_RULE `a = a * b <=> a * b = a * 1`] THEN
 152   REWRITE_TAC[EQ_MULT_LCANCEL] THEN ARITH_TAC);;
 153
 154 let SIGMA_POW2 = prove
 155  (`!k. sigma(2 EXP k) = 2 EXP (k + 1) - 1`,
 156   GEN_TAC THEN REWRITE_TAC[sigma; EXP_EQ_0; ARITH] THEN
 157   MATCH_MP_TAC EQ_TRANS THEN
 158   EXISTS_TAC `nsum {2 EXP i | i <= k} (\i. i)` THEN CONJ_TAC THENL
 159    [AP_THM_TAC THEN AP_TERM_TAC THEN
 160     SIMP_TAC[DIVIDES_PRIMEPOW; PRIME_2; EXTENSION; IN_ELIM_THM];
 161     ALL_TAC] THEN
 162   MATCH_MP_TAC(ARITH_RULE `x + 1 = y ==> x = y - 1`) THEN
 163   SPEC_TAC(`k:num`,`k:num`) THEN INDUCT_TAC THEN REWRITE_TAC[LE] THENL
 164    [REWRITE_TAC[SET_RULE `{2 EXP i | i = 0} = {2 EXP 0}`] THEN
 165     REWRITE_TAC[ARITH; NSUM_SING];
 166     ALL_TAC] THEN
 167   REWRITE_TAC[SET_RULE
 168    `{2 EXP i | i = SUC k \/ i <= k} =
 169     (2 EXP (SUC k)) INSERT {2 EXP i | i <= k}`] THEN
 170   POP_ASSUM MP_TAC THEN
 171   REWRITE_TAC[SET_RULE
 172    `{2 EXP i | i <= k} = IMAGE (\i. 2 EXP i) {i | i <= k}`] THEN
 173   SIMP_TAC[NSUM_CLAUSES; FINITE_IMAGE; FINITE_NUMSEG_LE] THEN
 174   REWRITE_TAC[IN_IMAGE; GSYM LE_ANTISYM; LE_EXP; ARITH] THEN
 175   REWRITE_TAC[LE_ANTISYM; IN_ELIM_THM; UNWIND_THM1] THEN
 176   REWRITE_TAC[ARITH_RULE `~(SUC k <= k)`] THEN
 177   DISCH_TAC THEN ASM_REWRITE_TAC[GSYM ADD_ASSOC] THEN
 178   REWRITE_TAC[EXP; EXP_ADD; ARITH] THEN ARITH_TAC);;
 179
 180 (* ------------------------------------------------------------------------- *)
 181 (* Multiplicativity of sigma, the most interesting property.                 *)
 182 (* ------------------------------------------------------------------------- *)
 183
 184 let SIGMA_MULTIPLICATIVE = prove
 185  (`!a b. coprime(a,b) ==> sigma(a * b) = sigma(a) * sigma(b)`,
 186   REPEAT GEN_TAC THEN
 187   ASM_CASES_TAC `a = 0` THEN ASM_REWRITE_TAC[SIGMA_0; MULT_CLAUSES] THEN
 188   ASM_CASES_TAC `b = 0` THEN ASM_REWRITE_TAC[SIGMA_0; MULT_CLAUSES] THEN
 189   DISCH_TAC THEN ASM_REWRITE_TAC[sigma; MULT_EQ_0] THEN
 190   ASM_SIMP_TAC[FINITE_DIVISORS; MULT_NSUM] THEN
 191   REWRITE_TAC[IN_ELIM_THM] THEN MATCH_MP_TAC EQ_TRANS THEN
 192   EXISTS_TAC
 193    `nsum (IMAGE (\(x,y). x * y)
 194          {x,y | x divides a /\ y divides b}) (\i. i)` THEN
 195   CONJ_TAC THENL
 196    [AP_THM_TAC THEN AP_TERM_TAC THEN
 197     REWRITE_TAC[EXTENSION; IN_IMAGE; IN_ELIM_THM; EXISTS_PAIR_THM] THEN
 198     REWRITE_TAC[PAIR_EQ] THEN
 199     ONCE_REWRITE_TAC[TAUT `(a /\ b) /\ c <=> c /\ a /\ b`] THEN
 200     REWRITE_TAC[GSYM CONJ_ASSOC; RIGHT_EXISTS_AND_THM; UNWIND_THM1] THEN
 201     X_GEN_TAC `n:num` THEN EQ_TAC THEN REWRITE_TAC[DIVISION_DECOMP] THEN
 202     REWRITE_TAC[divides] THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
 203     MESON_TAC[MULT_AC];
 204     ALL_TAC] THEN
 205   W(fun (asl,w) -> MP_TAC(PART_MATCH (lhs o rand) NSUM_IMAGE (lhand w))) THEN
 206   REWRITE_TAC[o_DEF; ETA_AX] THEN DISCH_THEN MATCH_MP_TAC THEN
 207   REWRITE_TAC[FORALL_PAIR_THM; IN_ELIM_THM] THEN
 208   MAP_EVERY X_GEN_TAC [`w:num`; `x:num`; `y:num`; `z:num`] THEN
 209   REWRITE_TAC[PAIR_EQ] THEN STRIP_TAC THEN
 210   REPEAT(FIRST_X_ASSUM(SUBST_ALL_TAC o SYM o
 211     check (is_var o rand o concl))) THEN
 212   REWRITE_TAC[GSYM DIVIDES_ANTISYM] THEN
 213   ASM_MESON_TAC[COPRIME_DIVISORS; COPRIME_SYM; COPRIME_DIVPROD;
 214                 DIVIDES_RMUL; DIVIDES_REFL; MULT_SYM]);;
 215
 216 (* ------------------------------------------------------------------------- *)
 217 (* Hence the main theorems.                                                  *)
 218 (* ------------------------------------------------------------------------- *)
 219
 220 let PERFECT_EUCLID = prove
 221  (`!k. prime(2 EXP k - 1) ==> perfect(2 EXP (k - 1) * (2 EXP k - 1))`,
 222   GEN_TAC THEN ASM_CASES_TAC `k = 0` THEN ASM_REWRITE_TAC[ARITH; PRIME_0] THEN
 223   DISCH_TAC THEN
 224   SUBGOAL_THEN `coprime(2 EXP (k - 1),2 EXP k - 1)` ASSUME_TAC THENL
 225    [MATCH_MP_TAC COPRIME_ODD_POW2 THEN ASM_SIMP_TAC[ODD_POW2_MINUS1];
 226     ALL_TAC] THEN
 227   ASM_SIMP_TAC[perfect; SIGMA_MULTIPLICATIVE; SIGMA_PRIME; SIGMA_POW2] THEN
 228   ASM_SIMP_TAC[ARITH_RULE `~(k = 0) ==> k - 1 + 1 = k`; EXP_EQ_0;
 229                MULT_EQ_0; ARITH] THEN
 230   CONJ_TAC THENL [ASM_MESON_TAC[PRIME_0]; ALL_TAC] THEN
 231   REWRITE_TAC[MULT_ASSOC] THEN GEN_REWRITE_TAC RAND_CONV [MULT_SYM] THEN
 232   AP_TERM_TAC THEN REWRITE_TAC[GSYM(CONJUNCT2 EXP)] THEN
 233   AP_TERM_TAC THEN UNDISCH_TAC `~(k = 0)` THEN ARITH_TAC);;
 234
 235 let PERFECT_EULER = prove
 236  (`!n. EVEN(n) /\ perfect(n)
 237        ==> ?k. prime(2 EXP k - 1) /\ n = 2 EXP (k - 1) * (2 EXP k - 1)`,
 238   GEN_TAC THEN MP_TAC(SPEC `n:num` EVEN_ODD_DECOMP) THEN
 239   ASM_CASES_TAC `n = 0` THENL
 240    [ASM_REWRITE_TAC[perfect]; ASM_REWRITE_TAC[]] THEN
 241   REWRITE_TAC[LEFT_IMP_EXISTS_THM; GSYM NOT_EVEN] THEN
 242   MAP_EVERY X_GEN_TAC [`r:num`; `s:num`] THEN
 243   DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC SUBST_ALL_TAC) THEN
 244   ASM_REWRITE_TAC[EVEN_EXP; EVEN_MULT; ARITH] THEN
 245   DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
 246   REWRITE_TAC[perfect] THEN
 247   ASM_SIMP_TAC[SIGMA_MULTIPLICATIVE; SIGMA_POW2;
 248                COPRIME_ODD_POW2; GSYM NOT_EVEN] THEN
 249   DISCH_TAC THEN EXISTS_TAC `r + 1` THEN
 250   REWRITE_TAC[ADD_SUB; EQ_MULT_LCANCEL] THEN REWRITE_TAC[EXP_EQ_0; ARITH] THEN
 251   FIRST_X_ASSUM(MP_TAC o check(is_eq o concl)) THEN
 252   REWRITE_TAC[MULT_ASSOC; GSYM(CONJUNCT2 EXP); ADD1] THEN
 253   DISCH_THEN(MP_TAC o MATCH_MP
 254     (REWRITE_RULE[IMP_CONJ] MULT_EQ_COPRIME)) THEN
 255   ANTS_TAC THENL
 256    [ONCE_REWRITE_TAC[COPRIME_SYM] THEN MATCH_MP_TAC COPRIME_ODD_POW2 THEN
 257     SIMP_TAC[ODD_POW2_MINUS1; ADD_EQ_0; ARITH_EQ];
 258     ALL_TAC] THEN
 259   DISCH_THEN(X_CHOOSE_THEN `d:num` MP_TAC) THEN
 260   ASM_CASES_TAC `d = 0` THEN ASM_REWRITE_TAC[MULT_CLAUSES] THENL
 261    [ASM_MESON_TAC[EVEN]; ALL_TAC] THEN
 262   ASM_CASES_TAC `d = 1` THENL
 263    [ASM_REWRITE_TAC[MULT_CLAUSES; SIGMA_PRIME_EQ] THEN
 264     DISCH_THEN(CONJUNCTS_THEN2 (ASSUME_TAC o SYM) ASSUME_TAC) THEN
 265     ASM_REWRITE_TAC[] THEN EXPAND_TAC "s" THEN
 266     MATCH_MP_TAC(GSYM SUB_ADD) THEN
 267     REWRITE_TAC[ARITH_RULE `1 <= n <=> ~(n = 0)`; EXP_EQ_0; ARITH];
 268     ALL_TAC] THEN
 269   DISCH_THEN(CONJUNCTS_THEN2 (ASSUME_TAC o SYM) ASSUME_TAC) THEN
 270   MP_TAC(SPECL [`2 EXP (r + 1) - 1`; `d:num`] SIGMA_MULT) THEN
 271   ASM_REWRITE_TAC[] THEN
 272   MATCH_MP_TAC(TAUT `a /\ ~b ==> (a ==> b) ==> c`) THEN
 273   REPEAT CONJ_TAC THENL
 274    [MATCH_MP_TAC(ARITH_RULE `2 EXP 1 < a ==> 1 < a - 1`) THEN
 275     REWRITE_TAC[LT_EXP; ARITH] THEN
 276     UNDISCH_TAC `~(r = 0)` THEN ARITH_TAC;
 277     MAP_EVERY UNDISCH_TAC [`~(d = 0)`; `~(d = 1)`] THEN ARITH_TAC;
 278     REWRITE_TAC[NOT_LE] THEN EXPAND_TAC "s" THEN
 279     REWRITE_TAC[RIGHT_SUB_DISTRIB; MULT_CLAUSES] THEN
 280     MATCH_MP_TAC(ARITH_RULE `1 * d < x * d ==> x * d < 1 + d + x * d - d`) THEN
 281     ASM_REWRITE_TAC[LT_MULT_RCANCEL] THEN
 282     MATCH_MP_TAC(ARITH_RULE `2 EXP 0 < a ==> 1 < a`) THEN
 283     REWRITE_TAC[LT_EXP] THEN UNDISCH_TAC `~(r = 0)` THEN ARITH_TAC]);;