Examples/schnirelmann.ml

   1 (* ========================================================================= *)
   2 (* Schnirelmann density and its basic properties (not Mann's theorem yet).   *)
   3 (* ========================================================================= *)
   4
   5 needs "Multivariate/misc.ml";;
   6 needs "Library/products.ml";;
   7 prioritize_real();;
   8
   9 (* ------------------------------------------------------------------------- *)
  10 (* The basic definition.                                                     *)
  11 (* ------------------------------------------------------------------------- *)
  12
  13 let count = new_definition
  14  `count s n = CARD (s INTER (1..n))`;;
  15
  16 let schnirelmann = new_definition
  17  `schnirelmann s = inf { &(count s n) / &n | 1 <= n}`;;
  18
  19 (* ------------------------------------------------------------------------- *)
  20 (* Basic properties of the "count" function.                                 *)
  21 (* ------------------------------------------------------------------------- *)
  22
  23 let COUNT_BOUND = prove
  24  (`!s. count s n <= n`,
  25   GEN_TAC THEN REWRITE_TAC[count] THEN
  26   GEN_REWRITE_TAC RAND_CONV [GSYM CARD_NUMSEG_1] THEN
  27   MATCH_MP_TAC CARD_SUBSET THEN REWRITE_TAC[FINITE_NUMSEG] THEN SET_TAC[]);;
  28
  29 let COUNT_UNIV = prove
  30  (`!n. count (:num) n = n`,
  31   REWRITE_TAC[count; INTER_UNIV; CARD_NUMSEG_1]);;
  32
  33 let COUNT_MONO = prove
  34  (`!s t n. s SUBSET t ==> count s n <= count t n`,
  35   REPEAT STRIP_TAC THEN REWRITE_TAC[count] THEN
  36   MATCH_MP_TAC CARD_SUBSET THEN
  37   ASM_SIMP_TAC[FINITE_INTER; FINITE_NUMSEG] THEN ASM SET_TAC[]);;
  38
  39 let COUNT_INSENSITIVE = prove
  40  (`!s t n. (!m. 1 <= m ==> (m IN s <=> m IN t))
  41          ==> count s n = count t n`,
  42   REPEAT STRIP_TAC THEN REWRITE_TAC[count] THEN
  43   AP_TERM_TAC THEN REWRITE_TAC[EXTENSION; IN_INTER; IN_NUMSEG] THEN
  44   ASM_MESON_TAC[]);;
  45
  46 (* ------------------------------------------------------------------------- *)
  47 (* The straightforward properties of Schnirelmann density.                   *)
  48 (* ------------------------------------------------------------------------- *)
  49
  50 let SCHNIRELMANN_UBOUND,SCHNIRELMANN_LBOUND = (CONJ_PAIR o prove)
  51  (`(!n. 1 <= n ==> schnirelmann s <= &(count s n) / &n) /\
  52    (!b. (!n. 1 <= n ==> b <= &(count s n) / &n) ==> b <= schnirelmann s)`,
  53   MP_TAC(ISPEC `{ &(count s n) / &n | 1 <= n}` INF) THEN
  54   SIMP_TAC[SET_RULE `(!x. x IN {f x | P x} ==> Q x) <=> !x. P x ==> Q(f x)`;
  55            GSYM schnirelmann] THEN
  56   ANTS_TAC THENL
  57    [CONJ_TAC THENL [SET_TAC[LE_REFL]; ALL_TAC] THEN
  58     EXISTS_TAC `&0` THEN SIMP_TAC[REAL_LE_DIV; REAL_POS];
  59     MESON_TAC[]]);;
  60
  61 let SCHNIRELMANN_UBOUND_MUL = prove
  62  (`!n s. schnirelmann s * &n <= &(count s n)`,
  63   REPEAT GEN_TAC THEN
  64   DISJ_CASES_TAC(ARITH_RULE `n = 0 \/ 1 <= n`) THEN
  65   ASM_REWRITE_TAC[REAL_MUL_RZERO; REAL_POS] THEN
  66   ASM_SIMP_TAC[GSYM REAL_LE_RDIV_EQ; REAL_OF_NUM_LT; LE_1;
  67                SCHNIRELMANN_UBOUND]);;
  68
  69 let SCHNIRELMANN_BOUNDS = prove
  70  (`!s. &0 <= schnirelmann s /\ schnirelmann s <= &1`,
  71   GEN_TAC THEN REWRITE_TAC[schnirelmann] THEN
  72   MATCH_MP_TAC REAL_INF_BOUNDS THEN
  73   CONJ_TAC THENL [SET_TAC[LE_REFL]; ALL_TAC] THEN
  74   SIMP_TAC[SET_RULE `(!x. x IN {f x | P x} ==> Q x) <=> !x. P x ==> Q(f x)`;
  75            REAL_LE_DIV; REAL_POS; REAL_LE_LDIV_EQ; REAL_OF_NUM_LT; LE_1] THEN
  76   REWRITE_TAC[REAL_MUL_LID; REAL_OF_NUM_LE; COUNT_BOUND]);;
  77
  78 let SCHNIRELMANN_MONO = prove
  79  (`!s t. s SUBSET t ==> schnirelmann s <= schnirelmann t`,
  80   REPEAT STRIP_TAC THEN MATCH_MP_TAC SCHNIRELMANN_LBOUND THEN
  81   X_GEN_TAC `n:num` THEN DISCH_TAC THEN MATCH_MP_TAC REAL_LE_TRANS THEN
  82   EXISTS_TAC `&(count s n) / &n` THEN ASM_SIMP_TAC[SCHNIRELMANN_UBOUND] THEN
  83   ASM_SIMP_TAC[REAL_LE_DIV2_EQ; REAL_OF_NUM_LT; LE_1] THEN
  84   ASM_SIMP_TAC[REAL_OF_NUM_LE; COUNT_MONO]);;
  85
  86 let SCHNIRELMANN_INSENSITIVE = prove
  87  (`!s t. (!n. 1 <= n ==> (n IN s <=> n IN t))
  88          ==> schnirelmann s = schnirelmann t`,
  89   REPEAT GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP COUNT_INSENSITIVE) THEN
  90   SIMP_TAC[schnirelmann]);;
  91
  92 let SCHNIRELMANN_SENSITIVE = prove
  93  (`!s k. 1 <= k /\ ~(k IN s) ==> schnirelmann s <= &1 - &1 / &k`,
  94   REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_LE_TRANS THEN
  95   EXISTS_TAC `&(count s k) / &k` THEN
  96   ASM_SIMP_TAC[SCHNIRELMANN_UBOUND] THEN
  97   ASM_SIMP_TAC[REAL_FIELD `&1 <= x ==> (&1 - &1 / x) = (x - &1) / x`;
  98                REAL_OF_NUM_LE; REAL_LE_DIV2_EQ; REAL_OF_NUM_LT; LE_1] THEN
  99   ASM_SIMP_TAC[REAL_OF_NUM_SUB; REAL_OF_NUM_LE; count] THEN
 100   GEN_REWRITE_TAC RAND_CONV [GSYM CARD_NUMSEG_1] THEN
 101   MATCH_MP_TAC CARD_SUBSET THEN REWRITE_TAC[FINITE_NUMSEG] THEN
 102   REWRITE_TAC[SUBSET; IN_NUMSEG; IN_INTER] THEN
 103   ASM_MESON_TAC[ARITH_RULE `1 <= k ==> (x <= k - 1 <=> x <= k /\ ~(x = k))`]);;
 104
 105 let SCHNIRELMANN_SENSITIVE_1 = prove
 106  (`!s. ~(1 IN s) ==> schnirelmann s = &0`,
 107   REPEAT STRIP_TAC THEN
 108   MP_TAC(SPECL [`s:num->bool`; `1`] SCHNIRELMANN_SENSITIVE) THEN
 109   MP_TAC(SPEC `s:num->bool` SCHNIRELMANN_BOUNDS) THEN
 110   ASM_REWRITE_TAC[LE_REFL] THEN REAL_ARITH_TAC);;
 111
 112 let SCHNIRELMANN_UNIV = prove
 113  (`schnirelmann(:num) = &1`,
 114   REWRITE_TAC[GSYM REAL_LE_ANTISYM; SCHNIRELMANN_BOUNDS] THEN
 115   MATCH_MP_TAC SCHNIRELMANN_LBOUND THEN
 116   SIMP_TAC[COUNT_UNIV; REAL_DIV_REFL; REAL_OF_NUM_EQ; LE_1; REAL_LE_REFL]);;
 117
 118 let SCHNIRELMANN_EQ_1 = prove
 119  (`!s. schnirelmann s = &1 <=> !n. 1 <= n ==> n IN s`,
 120   GEN_TAC THEN EQ_TAC THENL
 121    [ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN
 122     REWRITE_TAC[EXTENSION; NOT_FORALL_THM; IN_UNIV; NOT_IMP] THEN
 123     DISCH_THEN(CHOOSE_THEN ASSUME_TAC) THEN
 124     FIRST_ASSUM(MP_TAC o MATCH_MP SCHNIRELMANN_SENSITIVE) THEN
 125     MATCH_MP_TAC(REAL_ARITH `&0 < x ==> s <= &1 - x ==> ~(s = &1)`) THEN
 126     ASM_SIMP_TAC[REAL_LT_DIV; REAL_OF_NUM_LT; LE_1; ARITH];
 127     REPEAT STRIP_TAC THEN
 128     GEN_REWRITE_TAC RAND_CONV [GSYM SCHNIRELMANN_UNIV] THEN
 129     MATCH_MP_TAC SCHNIRELMANN_INSENSITIVE THEN
 130     ASM_REWRITE_TAC[IN_UNIV]]);;
 131
 132 (* ------------------------------------------------------------------------- *)
 133 (* Sum-sets.                                                                 *)
 134 (* ------------------------------------------------------------------------- *)
 135
 136 parse_as_infix("+++",(16,"right"));;
 137
 138 let sumset = new_definition
 139  `s +++ t = {x + y:num | x IN s /\ y IN t}`;;
 140
 141 let SUMSET_0 = prove
 142  (`!s t. 0 IN s /\ 0 IN t ==> 0 IN (s +++ t)`,
 143   SIMP_TAC[sumset; IN_ELIM_THM] THEN MESON_TAC[ADD_CLAUSES]);;
 144
 145 let SUMSET_SUPERSET_LZERO = prove
 146  (`!s t. 0 IN s ==> t SUBSET (s +++ t)`,
 147   REPEAT STRIP_TAC THEN REWRITE_TAC[SUBSET; sumset; IN_ELIM_THM] THEN
 148   X_GEN_TAC `n:num` THEN DISCH_TAC THEN
 149   MAP_EVERY EXISTS_TAC [`0`; `n:num`] THEN ASM_REWRITE_TAC[ADD_CLAUSES]);;
 150
 151 let SUMSET_SUPERSET_RZERO = prove
 152  (`!s t. 0 IN t ==> s SUBSET (s +++ t)`,
 153   REPEAT STRIP_TAC THEN REWRITE_TAC[SUBSET; sumset; IN_ELIM_THM] THEN
 154   X_GEN_TAC `n:num` THEN DISCH_TAC THEN
 155   MAP_EVERY EXISTS_TAC [`n:num`; `0`] THEN ASM_REWRITE_TAC[ADD_CLAUSES]);;
 156
 157 let SUMSET_SYM = prove
 158  (`!s t. s +++ t = t +++ s`,
 159   REWRITE_TAC[EXTENSION; IN_ELIM_THM; sumset] THEN MESON_TAC[ADD_SYM]);;
 160
 161 let SUMSET_ASSOC = prove
 162  (`!s t u. s +++ (t +++ u) = (s +++ t) +++ u`,
 163   REWRITE_TAC[EXTENSION; IN_ELIM_THM; sumset] THEN MESON_TAC[ADD_ASSOC]);;
 164
 165 let NEUTRAL_SUMSET = prove
 166  (`neutral(+++) = {0}`,
 167   REWRITE_TAC[neutral] THEN MATCH_MP_TAC SELECT_UNIQUE THEN
 168   X_GEN_TAC `s:num->bool` THEN
 169   REWRITE_TAC[sumset; IN_ELIM_THM; EXTENSION; IN_SING] THEN EQ_TAC THENL
 170    [DISCH_THEN(MP_TAC o SPEC `{0}`) THEN REWRITE_TAC[IN_SING]; ALL_TAC] THEN
 171   MESON_TAC[ADD_CLAUSES]);;
 172
 173 let MONOIDAL_SUMSET = prove
 174  (`monoidal (+++)`,
 175   REWRITE_TAC[monoidal; NEUTRAL_SUMSET; SUMSET_ASSOC] THEN
 176   REWRITE_TAC[EQT_INTRO(SPEC_ALL SUMSET_SYM)] THEN
 177   REWRITE_TAC[EXTENSION; sumset; IN_ELIM_THM; IN_SING] THEN
 178   MESON_TAC[ADD_CLAUSES]);;
 179
 180 let SUMSET_0_ITER = prove
 181  (`!a s. FINITE s /\ (!k. k IN s ==> 0 IN a k) ==> 0 IN iterate(+++) s a`,
 182   GEN_TAC THEN REWRITE_TAC[IMP_CONJ] THEN
 183   MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
 184   SIMP_TAC[ITERATE_CLAUSES; MONOIDAL_SUMSET; NEUTRAL_SUMSET; IN_SING] THEN
 185   SIMP_TAC[IN_INSERT; SUMSET_0]);;
 186
 187 (* ------------------------------------------------------------------------- *)
 188 (* Basic Schnirelmann theorem.                                               *)
 189 (* ------------------------------------------------------------------------- *)
 190
 191 let SCHNIRELMAN_LEMMA = prove
 192  (`!s t n. 0 IN (s INTER t) /\ count s n + count t n >= n ==> n IN (s +++ t)`,
 193   REWRITE_TAC[IN_INTER] THEN REPEAT STRIP_TAC THEN
 194   MATCH_MP_TAC(TAUT `(~p ==> F) ==> p`) THEN DISCH_TAC THEN
 195   ASM_CASES_TAC `(n:num) IN s` THENL
 196    [ASM_MESON_TAC[SUMSET_SUPERSET_RZERO; SUBSET]; ALL_TAC] THEN
 197   ASM_CASES_TAC `(n:num) IN t` THENL
 198    [ASM_MESON_TAC[SUMSET_SUPERSET_LZERO; SUBSET]; ALL_TAC] THEN
 199   ASM_CASES_TAC `n = 0` THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
 200   SUBGOAL_THEN
 201    `~((s INTER (1..n-1)) INTER (IMAGE (\b. n - b) (t INTER (1..n-1))) = {})`
 202   MP_TAC THENL
 203    [MATCH_MP_TAC CARD_UNION_OVERLAP THEN
 204     SIMP_TAC[FINITE_IMAGE; FINITE_INTER; FINITE_NUMSEG; GT] THEN
 205     MATCH_MP_TAC LET_TRANS THEN EXISTS_TAC `CARD(1..n-1)` THEN CONJ_TAC THENL
 206      [MATCH_MP_TAC CARD_SUBSET THEN
 207       REWRITE_TAC[SUBSET; IN_UNION; FORALL_IN_IMAGE; FORALL_AND_THM;
 208                   TAUT `(a \/ b ==> c) <=> (a ==> c) /\ (b ==> c)`] THEN
 209       SIMP_TAC[FINITE_NUMSEG; IN_INTER; IN_NUMSEG] THEN ARITH_TAC;
 210       ALL_TAC] THEN
 211     REWRITE_TAC[CARD_NUMSEG_1] THEN
 212     MATCH_MP_TAC(ARITH_RULE `~(n = 0) /\ n <= x ==> n - 1 < x`) THEN
 213     ASM_REWRITE_TAC[] THEN FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (ARITH_RULE
 214      `s + t:num >= n ==> a = s /\ b = t ==> n <= a + b`)) THEN
 215     SUBGOAL_THEN `CARD(IMAGE (\b. n - b) (t INTER (1..n-1))) = count t (n - 1)`
 216     SUBST1_TAC THENL
 217      [REWRITE_TAC[count] THEN MATCH_MP_TAC CARD_IMAGE_INJ THEN
 218       SIMP_TAC[FINITE_INTER; FINITE_NUMSEG; IN_INTER; IN_NUMSEG] THEN
 219       ARITH_TAC;
 220       ALL_TAC] THEN
 221     REWRITE_TAC[count] THEN CONJ_TAC THEN AP_TERM_TAC THEN
 222     ASM_SIMP_TAC[EXTENSION; IN_INTER; IN_NUMSEG;
 223       ARITH_RULE `~(n = 0) ==> (x <= n - 1 <=> x <= n /\ ~(x = n))`] THEN
 224     ASM_MESON_TAC[];
 225     UNDISCH_TAC `~(n IN s +++ t)` THEN
 226     REWRITE_TAC[] THEN ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN
 227     REWRITE_TAC[EXTENSION; NOT_IN_EMPTY; IN_INTER; IN_IMAGE; IN_NUMSEG;
 228                 NOT_FORALL_THM; LEFT_IMP_EXISTS_THM] THEN
 229     X_GEN_TAC `a:num` THEN REWRITE_TAC[sumset; IN_ELIM_THM] THEN
 230     DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC (X_CHOOSE_TAC `b:num`)) THEN
 231     MAP_EVERY EXISTS_TAC [`a:num`; `b:num`] THEN ASM_REWRITE_TAC[] THEN
 232     ASM_ARITH_TAC]);;
 233
 234 let SCHNIRELMANN_THEOREM = prove
 235  (`!s t. 0 IN (s INTER t) /\ schnirelmann s + schnirelmann t >= &1
 236          ==> s +++ t = (:num)`,
 237   REWRITE_TAC[IN_INTER] THEN REPEAT STRIP_TAC THEN
 238   REWRITE_TAC[EXTENSION; IN_UNIV] THEN X_GEN_TAC `n:num` THEN
 239   ASM_CASES_TAC `n = 0` THENL
 240    [ASM_MESON_TAC[SUMSET_SUPERSET_LZERO; SUBSET; IN_INTER]; ALL_TAC] THEN
 241   MATCH_MP_TAC SCHNIRELMAN_LEMMA THEN ASM_REWRITE_TAC[IN_INTER] THEN
 242   REWRITE_TAC[GE; GSYM REAL_OF_NUM_LE; GSYM REAL_OF_NUM_ADD] THEN
 243   GEN_REWRITE_TAC LAND_CONV [GSYM REAL_MUL_LID] THEN
 244   ASM_SIMP_TAC[GSYM REAL_LE_RDIV_EQ; REAL_OF_NUM_LT; LE_1] THEN
 245   REWRITE_TAC[real_div; REAL_ADD_RDISTRIB] THEN REWRITE_TAC[GSYM real_div] THEN
 246   FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_ARITH
 247    `a + b >= &1 ==> a <= x /\ b <= y ==> &1 <= x + y`)) THEN
 248   CONJ_TAC THEN MATCH_MP_TAC SCHNIRELMANN_UBOUND THEN ASM_ARITH_TAC);;
 249
 250 let SCHNIRELMANN_THEOREM_2 = prove
 251  (`!s. 0 IN s /\ schnirelmann s >= &1 / &2 ==> s +++ s = (:num)`,
 252   REPEAT STRIP_TAC THEN MATCH_MP_TAC SCHNIRELMANN_THEOREM THEN
 253   ASM_REWRITE_TAC[IN_INTER] THEN ASM_REAL_ARITH_TAC);;
 254
 255 (* ------------------------------------------------------------------------- *)
 256 (* Additional additivity properties and full Schnirelmann theorem.           *)
 257 (* ------------------------------------------------------------------------- *)
 258
 259 let ENUMERATION_LEMMA = prove
 260  (`!n s p. s HAS_SIZE n /\ (!k. k IN s ==> 1 <= k /\ k <= p)
 261            ==> ?a:num->num.
 262                  a(0) = 0 /\
 263                  a(n + 1) = p + 1 /\
 264                  s = IMAGE a (1..n) /\
 265                  (!j k. j <= n /\ k <= n + 1 /\ j < k ==> a(j) < a(k)) /\
 266                  (!j k. j <= n /\ k <= n + 1 /\ j <= k ==> a(j) <= a(k))`,
 267   REPEAT STRIP_TAC THEN
 268   MP_TAC(ISPEC `(<=):num->num->bool` TOPOLOGICAL_SORT) THEN
 269   REWRITE_TAC[LE_TRANS; LE_ANTISYM] THEN
 270   DISCH_THEN(MP_TAC o SPECL [`n:num`; `s:num->bool`]) THEN
 271   ASM_REWRITE_TAC[NOT_LE; IN_NUMSEG] THEN
 272   DISCH_THEN(X_CHOOSE_THEN `f:num->num` STRIP_ASSUME_TAC) THEN
 273   EXISTS_TAC `\i. if 1 <= i then if i <= n then f i else p + 1 else 0` THEN
 274   ASM_REWRITE_TAC[ARITH; ARITH_RULE `1 <= n + 1 /\ ~(n + 1 <= n)`] THEN
 275   CONJ_TAC THENL
 276    [REWRITE_TAC[EXTENSION; IN_IMAGE; IN_NUMSEG] THEN MESON_TAC[]; ALL_TAC] THEN
 277   MATCH_MP_TAC(TAUT `(a ==> b) /\ a ==> a /\ b`) THEN
 278   CONJ_TAC THENL [MESON_TAC[LE_LT]; ALL_TAC] THEN
 279   SUBGOAL_THEN `!k. 1 <= k /\ k <= n ==> 1 <= f(k) /\ f(k) <= p`
 280   ASSUME_TAC THENL
 281    [GEN_TAC THEN STRIP_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
 282     ASM_REWRITE_TAC[IN_IMAGE; IN_NUMSEG] THEN ASM_MESON_TAC[];
 283     ALL_TAC] THEN
 284   MAP_EVERY X_GEN_TAC [`i:num`; `j:num`] THEN STRIP_TAC THEN
 285   FIRST_X_ASSUM(MP_TAC o SPECL [`i:num`; `j:num`]) THEN ASM_REWRITE_TAC[] THEN
 286   REPEAT(COND_CASES_TAC THEN ASM_SIMP_TAC[]) THEN
 287   FIRST_X_ASSUM(fun th ->
 288     MP_TAC(SPEC `i:num` th) THEN MP_TAC(SPEC `j:num` th)) THEN
 289   ASM_ARITH_TAC);;
 290
 291 let CARD_INTER_0_1 = prove
 292  (`!n s. 0 IN s ==> CARD(s INTER (0..n)) = SUC(CARD(s INTER (1..n)))`,
 293   REPEAT STRIP_TAC THEN
 294   SUBGOAL_THEN `s INTER (0..n) = 0 INSERT (s INTER (1..n))` SUBST1_TAC THENL
 295    [MATCH_MP_TAC(SET_RULE
 296      `a IN s /\ (t = a INSERT u)
 297       ==> (s INTER t = a INSERT (s INTER u))`) THEN
 298     ASM_REWRITE_TAC[EXTENSION; IN_INSERT; IN_NUMSEG] THEN ARITH_TAC;
 299     SIMP_TAC[CARD_CLAUSES; FINITE_INTER; FINITE_NUMSEG; IN_INTER; ARITH;
 300              IN_NUMSEG; GSYM REAL_OF_NUM_SUC]]);;
 301
 302 let SCHNIRELMANN_SUMSET = prove
 303  (`!s t. 0 IN (s INTER t)
 304          ==> schnirelmann(s +++ t)
 305                 >= (schnirelmann s + schnirelmann t) -
 306                    schnirelmann s * schnirelmann t`,
 307   REWRITE_TAC[IN_INTER] THEN REPEAT STRIP_TAC THEN REWRITE_TAC[real_ge] THEN
 308   MATCH_MP_TAC SCHNIRELMANN_LBOUND THEN X_GEN_TAC `n:num` THEN STRIP_TAC THEN
 309   ASM_SIMP_TAC[REAL_LE_RDIV_EQ; REAL_OF_NUM_LT; LE_1] THEN
 310   MP_TAC(SPECL [`count s n`; `s INTER (1..n)`; `n:num`] ENUMERATION_LEMMA) THEN
 311   SIMP_TAC[count; HAS_SIZE; FINITE_INTER; FINITE_NUMSEG] THEN
 312   SIMP_TAC[IN_INTER; IN_NUMSEG] THEN
 313   DISCH_THEN(X_CHOOSE_THEN `a:num->num` STRIP_ASSUME_TAC) THEN
 314   ABBREV_TAC `A = CARD(s INTER (1..n))` THEN
 315   SUBGOAL_THEN `!k. k <= A ==> (a:num->num)(k) IN s /\ a(k) <= n`
 316   ASSUME_TAC THENL
 317    [GEN_TAC THEN DISCH_TAC THEN
 318     FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [EXTENSION]) THEN
 319     DISCH_THEN(MP_TAC o SPEC `(a:num->num)(k)`) THEN
 320     DISJ_CASES_TAC(ARITH_RULE `k = 0 \/ 1 <= k`) THEN
 321     ASM_REWRITE_TAC[LE_0; IN_INTER; IN_NUMSEG] THEN
 322     MATCH_MP_TAC(TAUT `d ==> (a /\ b /\ c <=> d) ==> a /\ c`) THEN
 323     REWRITE_TAC[IN_IMAGE; IN_NUMSEG] THEN ASM_MESON_TAC[];
 324     ALL_TAC] THEN
 325   MATCH_MP_TAC REAL_LE_TRANS THEN
 326   EXISTS_TAC `&(CARD ((s +++ t) INTER (0..n))) - &1` THEN CONJ_TAC THENL
 327    [ALL_TAC;
 328     ASM_SIMP_TAC[CARD_INTER_0_1; SUMSET_0; GSYM REAL_OF_NUM_SUC] THEN
 329     REAL_ARITH_TAC] THEN
 330   REWRITE_TAC[REAL_LE_SUB_LADD] THEN MATCH_MP_TAC REAL_LE_TRANS THEN
 331   EXISTS_TAC
 332    `&(CARD(UNIONS(IMAGE (\i. (IMAGE (\b. a i + b)
 333                                     (t INTER (0..(a(i+1) - a(i) - 1)))))
 334                         (0..A))))` THEN
 335   CONJ_TAC THENL
 336    [ALL_TAC;
 337     REWRITE_TAC[REAL_OF_NUM_LE] THEN MATCH_MP_TAC CARD_SUBSET THEN
 338     SIMP_TAC[FINITE_INTER; FINITE_NUMSEG; UNIONS_SUBSET; FORALL_IN_IMAGE] THEN
 339     REWRITE_TAC[SUBSET; FORALL_IN_IMAGE] THEN
 340     X_GEN_TAC `k:num` THEN DISCH_TAC THEN X_GEN_TAC `l:num` THEN
 341     REWRITE_TAC[IN_INTER] THEN REPEAT STRIP_TAC THEN
 342     RULE_ASSUM_TAC(REWRITE_RULE[IN_NUMSEG]) THENL
 343      [REWRITE_TAC[sumset; IN_ELIM_THM] THEN ASM_MESON_TAC[]; ALL_TAC] THEN
 344     REWRITE_TAC[IN_NUMSEG; LE_0] THEN
 345     MATCH_MP_TAC(ARITH_RULE
 346      `a(k) < a(k + 1) /\ a(k + 1) <= n + 1 /\ l <= a(k + 1) - a(k) - 1
 347       ==> a(k) + l <= n`) THEN
 348     ASM_REWRITE_TAC[] THEN CONJ_TAC THENL
 349      [FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC; ALL_TAC] THEN
 350     ASM_CASES_TAC `k:num = A` THEN ASM_REWRITE_TAC[LE_REFL] THEN
 351     REPEAT(FIRST_X_ASSUM(MP_TAC o SPEC `k + 1`)) THEN ASM_ARITH_TAC] THEN
 352   W(MP_TAC o PART_MATCH (lhs o rand) CARD_UNIONS o rand o rand o snd) THEN
 353   REWRITE_TAC[FORALL_IN_IMAGE; IMP_CONJ; RIGHT_FORALL_IMP_THM] THEN
 354   SIMP_TAC[FINITE_IMAGE; FINITE_NUMSEG; FINITE_INTER] THEN
 355   SUBGOAL_THEN
 356    `!i j. i IN 0..A /\ j IN 0..A /\ ~(i = j)
 357                ==> IMAGE (\b. a i + b) (t INTER (0..a (i + 1) - a i - 1)) INTER
 358                    IMAGE (\b. a j + b) (t INTER (0..a (j + 1) - a j - 1)) = {}`
 359   (LABEL_TAC "*") THENL
 360    [MAP_EVERY X_GEN_TAC [`i:num`; `j:num`] THEN STRIP_TAC THEN
 361     REWRITE_TAC[SET_RULE
 362      `IMAGE f s INTER t = {} <=> !x. x IN s ==> ~(f x IN t)`] THEN
 363     X_GEN_TAC `k:num` THEN DISCH_TAC THEN REWRITE_TAC[IN_IMAGE] THEN
 364     DISCH_THEN(X_CHOOSE_THEN `l:num` STRIP_ASSUME_TAC) THEN
 365     RULE_ASSUM_TAC(REWRITE_RULE[IN_NUMSEG; IN_INTER]) THEN
 366     SUBGOAL_THEN `a(i + 1):num <= a(j) \/ a(j + 1) <= a(i)` MP_TAC THENL
 367      [FIRST_X_ASSUM(DISJ_CASES_TAC o MATCH_MP (ARITH_RULE
 368        `~(i = j) ==> i + 1 <= j \/ j + 1 <= i`))
 369       THENL [DISJ1_TAC; DISJ2_TAC] THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
 370       ASM_ARITH_TAC;
 371       ALL_TAC] THEN
 372     SUBGOAL_THEN `(a:num->num)(i) < a(i + 1) /\ a(j) < a(j + 1)`
 373     STRIP_ASSUME_TAC THENL
 374      [CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC; ALL_TAC] THEN
 375     ASM_ARITH_TAC;
 376     ALL_TAC] THEN
 377   ANTS_TAC THENL
 378    [X_GEN_TAC `i:num` THEN DISCH_TAC THEN
 379     X_GEN_TAC `j:num` THEN DISCH_TAC THEN
 380     ASM_CASES_TAC `i:num = j` THEN ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[];
 381     ALL_TAC] THEN
 382   DISCH_THEN SUBST1_TAC THEN
 383   W(MP_TAC o PART_MATCH (lhs o rand) NSUM_IMAGE_NONZERO o
 384     rand o rand o snd) THEN
 385   REWRITE_TAC[] THEN ANTS_TAC THENL
 386    [REWRITE_TAC[FINITE_NUMSEG] THEN MAP_EVERY X_GEN_TAC [`i:num`; `j:num`] THEN
 387     STRIP_TAC THEN REMOVE_THEN "*" (MP_TAC o SPECL [`i:num`; `j:num`]) THEN
 388     ASM_REWRITE_TAC[INTER_ACI] THEN SIMP_TAC[CARD_CLAUSES];
 389     ALL_TAC] THEN
 390   DISCH_THEN SUBST1_TAC THEN REWRITE_TAC[o_DEF] THEN
 391   SIMP_TAC[EQ_ADD_LCANCEL; CARD_IMAGE_INJ; FINITE_INTER; FINITE_NUMSEG] THEN
 392   SIMP_TAC[REAL_OF_NUM_SUM; FINITE_INTER; FINITE_NUMSEG] THEN
 393   MATCH_MP_TAC REAL_LE_TRANS THEN
 394   EXISTS_TAC
 395    `sum(0..A) (\i. schnirelmann t * &(a(i + 1) - a(i) - 1) + &1)` THEN
 396   CONJ_TAC THENL
 397    [ALL_TAC;
 398     MATCH_MP_TAC SUM_LE_NUMSEG THEN REWRITE_TAC[] THEN
 399     ASM_SIMP_TAC[CARD_INTER_0_1; SUMSET_0; GSYM REAL_OF_NUM_SUC] THEN
 400     SIMP_TAC[GSYM count; SCHNIRELMANN_UBOUND_MUL; REAL_LE_RADD]] THEN
 401   REWRITE_TAC[SUM_ADD_NUMSEG; SUM_CONST_NUMSEG] THEN
 402   REWRITE_TAC[SUB_0; GSYM REAL_OF_NUM_ADD; REAL_MUL_RID] THEN
 403   REWRITE_TAC[REAL_ADD_ASSOC; REAL_LE_RADD] THEN
 404   MATCH_MP_TAC REAL_LE_TRANS THEN
 405   EXISTS_TAC
 406    `sum(0..A) (\i. schnirelmann t * (&(a(i + 1)) - &(a i) - &1)) + &A` THEN
 407   CONJ_TAC THENL
 408    [ALL_TAC;
 409     REWRITE_TAC[REAL_LE_RADD] THEN MATCH_MP_TAC SUM_LE_NUMSEG THEN
 410     X_GEN_TAC `i:num` THEN STRIP_TAC THEN
 411     SUBGOAL_THEN `a(i):num < a(i + 1)` ASSUME_TAC THENL
 412      [FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC; ALL_TAC] THEN
 413     ASM_SIMP_TAC[REAL_OF_NUM_SUB; LT_IMP_LE; ARITH_RULE `a < b ==> 1 <= b - a`;
 414                  REAL_LE_REFL]] THEN
 415   REWRITE_TAC[SUM_LMUL] THEN
 416   ONCE_REWRITE_TAC[REAL_ARITH `a - b - c:real = --((b - a) + c)`] THEN
 417   REWRITE_TAC[SUM_NEG; SUM_ADD_NUMSEG; SUM_DIFFS; LE_0] THEN
 418   ASM_REWRITE_TAC[REAL_ARITH `--(&0 - a + b) = a - b`; SUM_CONST_NUMSEG] THEN
 419   REWRITE_TAC[SUB_0; GSYM REAL_OF_NUM_ADD; REAL_MUL_RID] THEN
 420   REWRITE_TAC[REAL_ARITH `(n + &1) - (a + &1) = n - a`] THEN
 421   MATCH_MP_TAC(REAL_ARITH
 422    `(&1 - t) * s * n <= (&1 - t) * a
 423     ==> ((s + t) - s * t) * n <= t * (n - a) + a`) THEN
 424   MATCH_MP_TAC REAL_LE_LMUL THEN EXPAND_TAC "A" THEN
 425   REWRITE_TAC[REAL_SUB_LE; SCHNIRELMANN_UBOUND_MUL; GSYM count] THEN
 426   REWRITE_TAC[SCHNIRELMANN_BOUNDS]);;
 427
 428 (* ------------------------------------------------------------------------- *)
 429 (* Now an iterative form.                                                    *)
 430 (* ------------------------------------------------------------------------- *)
 431
 432 let SCHNIRELMANN_SUMSET_GEN = prove
 433  (`!a s. FINITE s /\ (!i:A. i IN s ==> 0 IN a i)
 434          ==> schnirelmann(iterate(+++) s a)
 435              >= &1 - product s (\i. &1 - schnirelmann(a i))`,
 436   GEN_TAC THEN REWRITE_TAC[IMP_CONJ] THEN
 437   MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
 438   SIMP_TAC[PRODUCT_CLAUSES; real_ge; REAL_SUB_REFL; SCHNIRELMANN_BOUNDS] THEN
 439   MAP_EVERY X_GEN_TAC [`k:A`; `s:A->bool`] THEN STRIP_TAC THEN
 440   DISCH_TAC THEN FIRST_ASSUM(MP_TAC o check (is_imp o concl)) THEN
 441   ANTS_TAC THENL [ASM_MESON_TAC[IN_INSERT]; DISCH_TAC] THEN
 442   ASM_SIMP_TAC[ITERATE_CLAUSES; MONOIDAL_SUMSET] THEN
 443   MATCH_MP_TAC REAL_LE_TRANS THEN
 444   EXISTS_TAC `&1 - (&1 - schnirelmann(a(k:A))) *
 445                    (&1 - schnirelmann(iterate (+++) s a))` THEN
 446   CONJ_TAC THENL
 447    [MATCH_MP_TAC(REAL_ARITH `a <= b ==> &1 - b <= &1 - a`) THEN
 448     MATCH_MP_TAC REAL_LE_LMUL THEN
 449     ASM_REWRITE_TAC[REAL_SUB_LE; SCHNIRELMANN_BOUNDS] THEN
 450     ASM_REAL_ARITH_TAC;
 451     REWRITE_TAC[REAL_ARITH `&1 - (&1 - s) * (&1 - t) <= u <=>
 452                             u >= (s + t) - s * t`] THEN
 453     MATCH_MP_TAC SCHNIRELMANN_SUMSET THEN
 454     ASM_SIMP_TAC[IN_INTER; IN_INSERT; SUMSET_0_ITER]]);;
 455
 456 let SCHNIRELMANN_SUMSET_POW = prove
 457  (`!i s. FINITE i /\ 0 IN s
 458          ==> schnirelmann(iterate(+++) i (\k:A. s))
 459              >= &1 - (&1 - schnirelmann s) pow (CARD i)`,
 460   REPEAT STRIP_TAC THEN
 461   MP_TAC(ISPECL [`\i:A. (s:num->bool)`; `i:A->bool`]
 462     SCHNIRELMANN_SUMSET_GEN) THEN
 463   ASM_SIMP_TAC[PRODUCT_CONST]);;
 464
 465 let SCHNIRELMANN = prove
 466  (`!s. 0 IN s /\ schnirelmann s > &0
 467        ==> ?k. !i. i HAS_SIZE k ==> iterate(+++) i (\a:A. s) = (:num)`,
 468   REPEAT STRIP_TAC THEN REWRITE_TAC[HAS_SIZE] THEN
 469   MP_TAC(ISPECL [`&1 - schnirelmann s`; `&1 / &2`] REAL_ARCH_POW_INV) THEN
 470   ANTS_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC] THEN
 471   DISCH_THEN(X_CHOOSE_TAC `n:num`) THEN EXISTS_TAC `2 * n` THEN
 472   X_GEN_TAC `i:A->bool` THEN STRIP_TAC THEN
 473   SUBGOAL_THEN
 474    `?j k:A->bool. i = j UNION k /\ j INTER k = {} /\
 475                   j HAS_SIZE n /\ k HAS_SIZE n`
 476    (REPEAT_TCL CHOOSE_THEN (CONJUNCTS_THEN2 SUBST1_TAC STRIP_ASSUME_TAC))
 477   THENL
 478    [FIRST_ASSUM(MP_TAC o SPEC `n:num` o MATCH_MP CHOOSE_SUBSET) THEN
 479     ASM_REWRITE_TAC[ARITH_RULE `n <= 2 * n`] THEN
 480     MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `j:A->bool` THEN
 481     STRIP_TAC THEN EXISTS_TAC `i DIFF j:A->bool` THEN
 482     MATCH_MP_TAC(TAUT
 483      `(a /\ b /\ c) /\ (a /\ b /\ c ==> d) ==> a /\ b /\ c /\ d`) THEN
 484     CONJ_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN STRIP_TAC THEN
 485     GEN_REWRITE_TAC RAND_CONV [ARITH_RULE `n = 2 * n - n`] THEN
 486     MATCH_MP_TAC HAS_SIZE_DIFF THEN ASM_REWRITE_TAC[HAS_SIZE];
 487     ALL_TAC] THEN
 488   RULE_ASSUM_TAC(REWRITE_RULE[GSYM DISJOINT; HAS_SIZE]) THEN
 489   ASM_SIMP_TAC[MONOIDAL_SUMSET; ITERATE_UNION] THEN
 490   MATCH_MP_TAC SCHNIRELMANN_THEOREM THEN
 491   ASM_SIMP_TAC[SUMSET_0_ITER; IN_INTER] THEN
 492   MP_TAC(SPECL [`j:A->bool`; `s:num->bool`] SCHNIRELMANN_SUMSET_POW) THEN
 493   MP_TAC(SPECL [`k:A->bool`; `s:num->bool`] SCHNIRELMANN_SUMSET_POW) THEN
 494   ASM_SIMP_TAC[] THEN MATCH_MP_TAC(REAL_ARITH
 495    `a < &1 / &2 ==> y >= &1 - a ==> x >= &1 - a ==> x + y >= &1`) THEN
 496   ASM_REWRITE_TAC[]);;
 497
 498 (* ------------------------------------------------------------------------- *)
 499 (* A more direct version, without the techicality of 0 and sumsets.          *)
 500 (* ------------------------------------------------------------------------- *)
 501
 502 let SCHNIRELMANN_DIRECT = prove
 503  (`!s. schnirelmann s > &0
 504        ==> ?k. !n. ?m f. m <= k /\ (!i. i IN 1..m ==> f(i) IN s) /\
 505                          n = nsum (1..m) f`,
 506   GEN_TAC THEN STRIP_TAC THEN
 507   SUBGOAL_THEN
 508    `?k. !i:num->bool.
 509            i HAS_SIZE k ==> iterate (+++) i (\a. 0 INSERT s) = (:num)`
 510   MP_TAC THENL
 511    [MATCH_MP_TAC SCHNIRELMANN THEN REWRITE_TAC[IN_INSERT] THEN
 512     POP_ASSUM MP_TAC THEN MATCH_MP_TAC EQ_IMP THEN AP_THM_TAC THEN
 513     AP_TERM_TAC THEN MATCH_MP_TAC SCHNIRELMANN_INSENSITIVE THEN
 514     SIMP_TAC[IN_INSERT; LE_1];
 515     ALL_TAC] THEN
 516   MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `k:num` THEN
 517   DISCH_THEN(MP_TAC o SPEC `1..k`) THEN
 518   REWRITE_TAC[EXTENSION; HAS_SIZE_NUMSEG_1; IN_UNIV] THEN
 519   MATCH_MP_TAC MONO_FORALL THEN
 520   SPEC_TAC(`k:num`,`k:num`) THEN POP_ASSUM_LIST(K ALL_TAC) THEN
 521   INDUCT_TAC THEN SIMP_TAC[NUMSEG_CLAUSES; ARITH; ARITH_RULE `1 <= SUC k`] THEN
 522   SIMP_TAC[ITERATE_CLAUSES; MONOIDAL_SUMSET; FINITE_NUMSEG] THENL
 523    [REWRITE_TAC[NEUTRAL_SUMSET; IN_SING] THEN GEN_TAC THEN
 524     DISCH_THEN SUBST1_TAC THEN EXISTS_TAC `0` THEN
 525     SIMP_TAC[NSUM_CLAUSES_NUMSEG; CARD_CLAUSES; EMPTY_SUBSET; FINITE_RULES;
 526              IN_NUMSEG; LE_REFL; ARITH] THEN
 527     REWRITE_TAC[ARITH_RULE `~(1 <= i /\ i <= 0)`];
 528     ALL_TAC] THEN
 529   REWRITE_TAC[IN_NUMSEG; ARITH_RULE `~(SUC n <= n)`] THEN
 530   ONCE_REWRITE_TAC[sumset] THEN REWRITE_TAC[IN_ELIM_THM; IN_INSERT] THEN
 531   X_GEN_TAC `n:num` THEN DISCH_THEN(X_CHOOSE_THEN `x:num` MP_TAC) THEN
 532   ASM_CASES_TAC `x = 0` THEN ASM_REWRITE_TAC[ADD_CLAUSES] THENL
 533    [ASM_MESON_TAC[IN_NUMSEG; ARITH_RULE `x <= k ==> x <= SUC k`]; ALL_TAC] THEN
 534   DISCH_THEN(X_CHOOSE_THEN `y:num` STRIP_ASSUME_TAC) THEN
 535   FIRST_X_ASSUM(MP_TAC o SPEC `y:num`) THEN
 536   ASM_REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
 537   MAP_EVERY X_GEN_TAC [`m:num`; `f:num->num`] THEN STRIP_TAC THEN
 538   MAP_EVERY EXISTS_TAC [`SUC m`; `\i. if i = SUC m then x:num else f i`] THEN
 539   ASM_SIMP_TAC[LE_SUC; LE; NSUM_CLAUSES_NUMSEG] THEN CONJ_TAC THENL
 540    [ASM_MESON_TAC[ARITH_RULE `~(SUC n <= n)`; IN_NUMSEG]; ALL_TAC] THEN
 541   REWRITE_TAC[ARITH_RULE `1 = SUC m \/ 1 <= m`] THEN
 542   GEN_REWRITE_TAC RAND_CONV [ADD_SYM] THEN AP_TERM_TAC THEN
 543   MATCH_MP_TAC NSUM_EQ THEN
 544   ASM_MESON_TAC[ARITH_RULE `~(SUC n <= n)`; IN_NUMSEG]);;