(* ========================================================================= *)
(* Schnirelmann density and its basic properties (not Mann's theorem yet).   *)
(* ========================================================================= *)

needs "Multivariate/misc.ml";;
needs "Library/products.ml";;
prioritize_real();;

(* ------------------------------------------------------------------------- *)
(* The basic definition.                                                     *)
(* ------------------------------------------------------------------------- *)

let count = new_definition
 `count s n = CARD (s INTER (1..n))`;;
let schnirelmann = new_definition
 `schnirelmann s = inf { &(count s n) / &n | 1 <= n}`;;
(* ------------------------------------------------------------------------- *) (* Basic properties of the "count" function. *) (* ------------------------------------------------------------------------- *)
let COUNT_BOUND = 
prove (`!s. count s n <= n`,
GEN_TAC THEN REWRITE_TAC[count] THEN GEN_REWRITE_TAC RAND_CONV [GSYM CARD_NUMSEG_1] THEN MATCH_MP_TAC CARD_SUBSET THEN REWRITE_TAC[FINITE_NUMSEG] THEN SET_TAC[]);;
let COUNT_UNIV = 
prove (`!n. count (:num) n = n`,
REWRITE_TAC[count; INTER_UNIV; CARD_NUMSEG_1]);;
let COUNT_MONO = 
prove (`!s t n. s SUBSET t ==> count s n <= count t n`,
REPEAT STRIP_TAC THEN REWRITE_TAC[count] THEN MATCH_MP_TAC CARD_SUBSET THEN ASM_SIMP_TAC[FINITE_INTER; FINITE_NUMSEG] THEN ASM SET_TAC[]);;
let COUNT_INSENSITIVE = 
prove (`!s t n. (!m. 1 <= m ==> (m IN s <=> m IN t)) ==> count s n = count t n`,
REPEAT STRIP_TAC THEN REWRITE_TAC[count] THEN AP_TERM_TAC THEN REWRITE_TAC[EXTENSION; IN_INTER; IN_NUMSEG] THEN ASM_MESON_TAC[]);;
(* ------------------------------------------------------------------------- *) (* The straightforward properties of Schnirelmann density. *) (* ------------------------------------------------------------------------- *) let SCHNIRELMANN_UBOUND,SCHNIRELMANN_LBOUND = (CONJ_PAIR o prove) (`(!n. 1 <= n ==> schnirelmann s <= &(count s n) / &n) /\ (!b. (!n. 1 <= n ==> b <= &(count s n) / &n) ==> b <= schnirelmann s)`, MP_TAC(ISPEC `{ &(count s n) / &n | 1 <= n}` INF) THEN SIMP_TAC[SET_RULE `(!x. x IN {f x | P x} ==> Q x) <=> !x. P x ==> Q(f x)`; GSYM schnirelmann] THEN ANTS_TAC THENL [CONJ_TAC THENL [SET_TAC[LE_REFL]; ALL_TAC] THEN EXISTS_TAC `&0` THEN SIMP_TAC[REAL_LE_DIV; REAL_POS]; MESON_TAC[]]);;
let SCHNIRELMANN_UBOUND_MUL = 
prove (`!n s. schnirelmann s * &n <= &(count s n)`,
REPEAT GEN_TAC THEN DISJ_CASES_TAC(ARITH_RULE `n = 0 \/ 1 <= n`) THEN ASM_REWRITE_TAC[REAL_MUL_RZERO; REAL_POS] THEN ASM_SIMP_TAC[GSYM REAL_LE_RDIV_EQ; REAL_OF_NUM_LT; LE_1; SCHNIRELMANN_UBOUND]);;
let SCHNIRELMANN_BOUNDS = 
prove (`!s. &0 <= schnirelmann s /\ schnirelmann s <= &1`,
GEN_TAC THEN REWRITE_TAC[schnirelmann] THEN MATCH_MP_TAC REAL_INF_BOUNDS THEN CONJ_TAC THENL [SET_TAC[LE_REFL]; ALL_TAC] THEN SIMP_TAC[SET_RULE `(!x. x IN {f x | P x} ==> Q x) <=> !x. P x ==> Q(f x)`; REAL_LE_DIV; REAL_POS; REAL_LE_LDIV_EQ; REAL_OF_NUM_LT; LE_1] THEN REWRITE_TAC[REAL_MUL_LID; REAL_OF_NUM_LE; COUNT_BOUND]);;
let SCHNIRELMANN_MONO = 
prove (`!s t. s SUBSET t ==> schnirelmann s <= schnirelmann t`,
REPEAT STRIP_TAC THEN MATCH_MP_TAC SCHNIRELMANN_LBOUND THEN X_GEN_TAC `n:num` THEN DISCH_TAC THEN MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `&(count s n) / &n` THEN ASM_SIMP_TAC[SCHNIRELMANN_UBOUND] THEN ASM_SIMP_TAC[REAL_LE_DIV2_EQ; REAL_OF_NUM_LT; LE_1] THEN ASM_SIMP_TAC[REAL_OF_NUM_LE; COUNT_MONO]);;
let SCHNIRELMANN_INSENSITIVE = 
prove (`!s t. (!n. 1 <= n ==> (n IN s <=> n IN t)) ==> schnirelmann s = schnirelmann t`,
REPEAT GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP COUNT_INSENSITIVE) THEN SIMP_TAC[schnirelmann]);;
let SCHNIRELMANN_SENSITIVE = 
prove (`!s k. 1 <= k /\ ~(k IN s) ==> schnirelmann s <= &1 - &1 / &k`,
REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `&(count s k) / &k` THEN ASM_SIMP_TAC[SCHNIRELMANN_UBOUND] THEN ASM_SIMP_TAC[REAL_FIELD `&1 <= x ==> (&1 - &1 / x) = (x - &1) / x`; REAL_OF_NUM_LE; REAL_LE_DIV2_EQ; REAL_OF_NUM_LT; LE_1] THEN ASM_SIMP_TAC[REAL_OF_NUM_SUB; REAL_OF_NUM_LE; count] THEN GEN_REWRITE_TAC RAND_CONV [GSYM CARD_NUMSEG_1] THEN MATCH_MP_TAC CARD_SUBSET THEN REWRITE_TAC[FINITE_NUMSEG] THEN REWRITE_TAC[SUBSET; IN_NUMSEG; IN_INTER] THEN ASM_MESON_TAC[ARITH_RULE `1 <= k ==> (x <= k - 1 <=> x <= k /\ ~(x = k))`]);;
let SCHNIRELMANN_SENSITIVE_1 = 
prove (`!s. ~(1 IN s) ==> schnirelmann s = &0`,
REPEAT STRIP_TAC THEN MP_TAC(SPECL [`s:num->bool`; `1`] SCHNIRELMANN_SENSITIVE) THEN MP_TAC(SPEC `s:num->bool` SCHNIRELMANN_BOUNDS) THEN ASM_REWRITE_TAC[LE_REFL] THEN REAL_ARITH_TAC);;
let SCHNIRELMANN_UNIV = 
prove (`schnirelmann(:num) = &1`,
REWRITE_TAC[GSYM REAL_LE_ANTISYM; SCHNIRELMANN_BOUNDS] THEN MATCH_MP_TAC SCHNIRELMANN_LBOUND THEN SIMP_TAC[COUNT_UNIV; REAL_DIV_REFL; REAL_OF_NUM_EQ; LE_1; REAL_LE_REFL]);;
let SCHNIRELMANN_EQ_1 = 
prove (`!s. schnirelmann s = &1 <=> !n. 1 <= n ==> n IN s`,
GEN_TAC THEN EQ_TAC THENL [ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN REWRITE_TAC[EXTENSION; NOT_FORALL_THM; IN_UNIV; NOT_IMP] THEN DISCH_THEN(CHOOSE_THEN ASSUME_TAC) THEN FIRST_ASSUM(MP_TAC o MATCH_MP SCHNIRELMANN_SENSITIVE) THEN MATCH_MP_TAC(REAL_ARITH `&0 < x ==> s <= &1 - x ==> ~(s = &1)`) THEN ASM_SIMP_TAC[REAL_LT_DIV; REAL_OF_NUM_LT; LE_1; ARITH]; REPEAT STRIP_TAC THEN GEN_REWRITE_TAC RAND_CONV [GSYM SCHNIRELMANN_UNIV] THEN MATCH_MP_TAC SCHNIRELMANN_INSENSITIVE THEN ASM_REWRITE_TAC[IN_UNIV]]);;
(* ------------------------------------------------------------------------- *) (* Sum-sets. *) (* ------------------------------------------------------------------------- *) parse_as_infix("+++",(16,"right"));;
let sumset = new_definition
 `s +++ t = {x + y:num | x IN s /\ y IN t}`;;
let SUMSET_0 = 
prove (`!s t. 0 IN s /\ 0 IN t ==> 0 IN (s +++ t)`,
SIMP_TAC[sumset; IN_ELIM_THM] THEN MESON_TAC[ADD_CLAUSES]);;
let SUMSET_SUPERSET_LZERO = 
prove (`!s t. 0 IN s ==> t SUBSET (s +++ t)`,
REPEAT STRIP_TAC THEN REWRITE_TAC[SUBSET; sumset; IN_ELIM_THM] THEN X_GEN_TAC `n:num` THEN DISCH_TAC THEN MAP_EVERY EXISTS_TAC [`0`; `n:num`] THEN ASM_REWRITE_TAC[ADD_CLAUSES]);;
let SUMSET_SUPERSET_RZERO = 
prove (`!s t. 0 IN t ==> s SUBSET (s +++ t)`,
REPEAT STRIP_TAC THEN REWRITE_TAC[SUBSET; sumset; IN_ELIM_THM] THEN X_GEN_TAC `n:num` THEN DISCH_TAC THEN MAP_EVERY EXISTS_TAC [`n:num`; `0`] THEN ASM_REWRITE_TAC[ADD_CLAUSES]);;
let SUMSET_SYM = 
prove (`!s t. s +++ t = t +++ s`,
REWRITE_TAC[EXTENSION; IN_ELIM_THM; sumset] THEN MESON_TAC[ADD_SYM]);;
let SUMSET_ASSOC = 
prove (`!s t u. s +++ (t +++ u) = (s +++ t) +++ u`,
REWRITE_TAC[EXTENSION; IN_ELIM_THM; sumset] THEN MESON_TAC[ADD_ASSOC]);;
let NEUTRAL_SUMSET = 
prove (`neutral(+++) = {0}`,
REWRITE_TAC[neutral] THEN MATCH_MP_TAC SELECT_UNIQUE THEN X_GEN_TAC `s:num->bool` THEN REWRITE_TAC[sumset; IN_ELIM_THM; EXTENSION; IN_SING] THEN EQ_TAC THENL [DISCH_THEN(MP_TAC o SPEC `{0}`) THEN REWRITE_TAC[IN_SING]; ALL_TAC] THEN MESON_TAC[ADD_CLAUSES]);;
let MONOIDAL_SUMSET = 
prove (`monoidal (+++)`,
REWRITE_TAC[monoidal; NEUTRAL_SUMSET; SUMSET_ASSOC] THEN REWRITE_TAC[EQT_INTRO(SPEC_ALL SUMSET_SYM)] THEN REWRITE_TAC[EXTENSION; sumset; IN_ELIM_THM; IN_SING] THEN MESON_TAC[ADD_CLAUSES]);;
let SUMSET_0_ITER = 
prove (`!a s. FINITE s /\ (!k. k IN s ==> 0 IN a k) ==> 0 IN iterate(+++) s a`,
GEN_TAC THEN REWRITE_TAC[IMP_CONJ] THEN MATCH_MP_TAC FINITE_INDUCT_STRONG THEN SIMP_TAC[ITERATE_CLAUSES; MONOIDAL_SUMSET; NEUTRAL_SUMSET; IN_SING] THEN SIMP_TAC[IN_INSERT; SUMSET_0]);;
(* ------------------------------------------------------------------------- *) (* Basic Schnirelmann theorem. *) (* ------------------------------------------------------------------------- *)
let SCHNIRELMAN_LEMMA = 
prove (`!s t n. 0 IN (s INTER t) /\ count s n + count t n >= n ==> n IN (s +++ t)`,
REWRITE_TAC[IN_INTER] THEN REPEAT STRIP_TAC THEN MATCH_MP_TAC(TAUT `(~p ==> F) ==> p`) THEN DISCH_TAC THEN ASM_CASES_TAC `(n:num) IN s` THENL [ASM_MESON_TAC[SUMSET_SUPERSET_RZERO; SUBSET]; ALL_TAC] THEN ASM_CASES_TAC `(n:num) IN t` THENL [ASM_MESON_TAC[SUMSET_SUPERSET_LZERO; SUBSET]; ALL_TAC] THEN ASM_CASES_TAC `n = 0` THENL [ASM_MESON_TAC[]; ALL_TAC] THEN SUBGOAL_THEN `~((s INTER (1..n-1)) INTER (IMAGE (\b. n - b) (t INTER (1..n-1))) = {})` MP_TAC THENL [MATCH_MP_TAC CARD_UNION_OVERLAP THEN SIMP_TAC[FINITE_IMAGE; FINITE_INTER; FINITE_NUMSEG; GT] THEN MATCH_MP_TAC LET_TRANS THEN EXISTS_TAC `CARD(1..n-1)` THEN CONJ_TAC THENL [MATCH_MP_TAC CARD_SUBSET THEN REWRITE_TAC[SUBSET; IN_UNION; FORALL_IN_IMAGE; FORALL_AND_THM; TAUT `(a \/ b ==> c) <=> (a ==> c) /\ (b ==> c)`] THEN SIMP_TAC[FINITE_NUMSEG; IN_INTER; IN_NUMSEG] THEN ARITH_TAC; ALL_TAC] THEN REWRITE_TAC[CARD_NUMSEG_1] THEN MATCH_MP_TAC(ARITH_RULE `~(n = 0) /\ n <= x ==> n - 1 < x`) THEN ASM_REWRITE_TAC[] THEN FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (ARITH_RULE `s + t:num >= n ==> a = s /\ b = t ==> n <= a + b`)) THEN SUBGOAL_THEN `CARD(IMAGE (\b. n - b) (t INTER (1..n-1))) = count t (n - 1)` SUBST1_TAC THENL [REWRITE_TAC[count] THEN MATCH_MP_TAC CARD_IMAGE_INJ THEN SIMP_TAC[FINITE_INTER; FINITE_NUMSEG; IN_INTER; IN_NUMSEG] THEN ARITH_TAC; ALL_TAC] THEN REWRITE_TAC[count] THEN CONJ_TAC THEN AP_TERM_TAC THEN ASM_SIMP_TAC[EXTENSION; IN_INTER; IN_NUMSEG; ARITH_RULE `~(n = 0) ==> (x <= n - 1 <=> x <= n /\ ~(x = n))`] THEN ASM_MESON_TAC[]; UNDISCH_TAC `~(n IN s +++ t)` THEN REWRITE_TAC[] THEN ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN REWRITE_TAC[EXTENSION; NOT_IN_EMPTY; IN_INTER; IN_IMAGE; IN_NUMSEG; NOT_FORALL_THM; LEFT_IMP_EXISTS_THM] THEN X_GEN_TAC `a:num` THEN REWRITE_TAC[sumset; IN_ELIM_THM] THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC (X_CHOOSE_TAC `b:num`)) THEN MAP_EVERY EXISTS_TAC [`a:num`; `b:num`] THEN ASM_REWRITE_TAC[] THEN ASM_ARITH_TAC]);;
let SCHNIRELMANN_THEOREM = 
prove (`!s t. 0 IN (s INTER t) /\ schnirelmann s + schnirelmann t >= &1 ==> s +++ t = (:num)`,
REWRITE_TAC[IN_INTER] THEN REPEAT STRIP_TAC THEN REWRITE_TAC[EXTENSION; IN_UNIV] THEN X_GEN_TAC `n:num` THEN ASM_CASES_TAC `n = 0` THENL [ASM_MESON_TAC[SUMSET_SUPERSET_LZERO; SUBSET; IN_INTER]; ALL_TAC] THEN MATCH_MP_TAC SCHNIRELMAN_LEMMA THEN ASM_REWRITE_TAC[IN_INTER] THEN REWRITE_TAC[GE; GSYM REAL_OF_NUM_LE; GSYM REAL_OF_NUM_ADD] THEN GEN_REWRITE_TAC LAND_CONV [GSYM REAL_MUL_LID] THEN ASM_SIMP_TAC[GSYM REAL_LE_RDIV_EQ; REAL_OF_NUM_LT; LE_1] THEN REWRITE_TAC[real_div; REAL_ADD_RDISTRIB] THEN REWRITE_TAC[GSYM real_div] THEN FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_ARITH `a + b >= &1 ==> a <= x /\ b <= y ==> &1 <= x + y`)) THEN CONJ_TAC THEN MATCH_MP_TAC SCHNIRELMANN_UBOUND THEN ASM_ARITH_TAC);;
let SCHNIRELMANN_THEOREM_2 = 
prove (`!s. 0 IN s /\ schnirelmann s >= &1 / &2 ==> s +++ s = (:num)`,
REPEAT STRIP_TAC THEN MATCH_MP_TAC SCHNIRELMANN_THEOREM THEN ASM_REWRITE_TAC[IN_INTER] THEN ASM_REAL_ARITH_TAC);;
(* ------------------------------------------------------------------------- *) (* Additional additivity properties and full Schnirelmann theorem. *) (* ------------------------------------------------------------------------- *)
let ENUMERATION_LEMMA = 
prove (`!n s p. s HAS_SIZE n /\ (!k. k IN s ==> 1 <= k /\ k <= p) ==> ?a:num->num. a(0) = 0 /\ a(n + 1) = p + 1 /\ s = IMAGE a (1..n) /\ (!j k. j <= n /\ k <= n + 1 /\ j < k ==> a(j) < a(k)) /\ (!j k. j <= n /\ k <= n + 1 /\ j <= k ==> a(j) <= a(k))`,
REPEAT STRIP_TAC THEN MP_TAC(ISPEC `(<=):num->num->bool` TOPOLOGICAL_SORT) THEN REWRITE_TAC[LE_TRANS; LE_ANTISYM] THEN DISCH_THEN(MP_TAC o SPECL [`n:num`; `s:num->bool`]) THEN ASM_REWRITE_TAC[NOT_LE; IN_NUMSEG] THEN DISCH_THEN(X_CHOOSE_THEN `f:num->num` STRIP_ASSUME_TAC) THEN EXISTS_TAC `\i. if 1 <= i then if i <= n then f i else p + 1 else 0` THEN ASM_REWRITE_TAC[ARITH; ARITH_RULE `1 <= n + 1 /\ ~(n + 1 <= n)`] THEN CONJ_TAC THENL [REWRITE_TAC[EXTENSION; IN_IMAGE; IN_NUMSEG] THEN MESON_TAC[]; ALL_TAC] THEN MATCH_MP_TAC(TAUT `(a ==> b) /\ a ==> a /\ b`) THEN CONJ_TAC THENL [MESON_TAC[LE_LT]; ALL_TAC] THEN SUBGOAL_THEN `!k. 1 <= k /\ k <= n ==> 1 <= f(k) /\ f(k) <= p` ASSUME_TAC THENL [GEN_TAC THEN STRIP_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[IN_IMAGE; IN_NUMSEG] THEN ASM_MESON_TAC[]; ALL_TAC] THEN MAP_EVERY X_GEN_TAC [`i:num`; `j:num`] THEN STRIP_TAC THEN FIRST_X_ASSUM(MP_TAC o SPECL [`i:num`; `j:num`]) THEN ASM_REWRITE_TAC[] THEN REPEAT(COND_CASES_TAC THEN ASM_SIMP_TAC[]) THEN FIRST_X_ASSUM(fun th -> MP_TAC(SPEC `i:num` th) THEN MP_TAC(SPEC `j:num` th)) THEN ASM_ARITH_TAC);;
let CARD_INTER_0_1 = 
prove (`!n s. 0 IN s ==> CARD(s INTER (0..n)) = SUC(CARD(s INTER (1..n)))`,
REPEAT STRIP_TAC THEN SUBGOAL_THEN `s INTER (0..n) = 0 INSERT (s INTER (1..n))` SUBST1_TAC THENL [MATCH_MP_TAC(SET_RULE `a IN s /\ (t = a INSERT u) ==> (s INTER t = a INSERT (s INTER u))`) THEN ASM_REWRITE_TAC[EXTENSION; IN_INSERT; IN_NUMSEG] THEN ARITH_TAC; SIMP_TAC[CARD_CLAUSES; FINITE_INTER; FINITE_NUMSEG; IN_INTER; ARITH; IN_NUMSEG; GSYM REAL_OF_NUM_SUC]]);;
let SCHNIRELMANN_SUMSET = 
prove (`!s t. 0 IN (s INTER t) ==> schnirelmann(s +++ t) >= (schnirelmann s + schnirelmann t) - schnirelmann s * schnirelmann t`,
REWRITE_TAC[IN_INTER] THEN REPEAT STRIP_TAC THEN REWRITE_TAC[real_ge] THEN MATCH_MP_TAC SCHNIRELMANN_LBOUND THEN X_GEN_TAC `n:num` THEN STRIP_TAC THEN ASM_SIMP_TAC[REAL_LE_RDIV_EQ; REAL_OF_NUM_LT; LE_1] THEN MP_TAC(SPECL [`count s n`; `s INTER (1..n)`; `n:num`] ENUMERATION_LEMMA) THEN SIMP_TAC[count; HAS_SIZE; FINITE_INTER; FINITE_NUMSEG] THEN SIMP_TAC[IN_INTER; IN_NUMSEG] THEN DISCH_THEN(X_CHOOSE_THEN `a:num->num` STRIP_ASSUME_TAC) THEN ABBREV_TAC `A = CARD(s INTER (1..n))` THEN SUBGOAL_THEN `!k. k <= A ==> (a:num->num)(k) IN s /\ a(k) <= n` ASSUME_TAC THENL [GEN_TAC THEN DISCH_TAC THEN FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [EXTENSION]) THEN DISCH_THEN(MP_TAC o SPEC `(a:num->num)(k)`) THEN DISJ_CASES_TAC(ARITH_RULE `k = 0 \/ 1 <= k`) THEN ASM_REWRITE_TAC[LE_0; IN_INTER; IN_NUMSEG] THEN MATCH_MP_TAC(TAUT `d ==> (a /\ b /\ c <=> d) ==> a /\ c`) THEN REWRITE_TAC[IN_IMAGE; IN_NUMSEG] THEN ASM_MESON_TAC[]; ALL_TAC] THEN MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `&(CARD ((s +++ t) INTER (0..n))) - &1` THEN CONJ_TAC THENL [ALL_TAC; ASM_SIMP_TAC[CARD_INTER_0_1; SUMSET_0; GSYM REAL_OF_NUM_SUC] THEN REAL_ARITH_TAC] THEN REWRITE_TAC[REAL_LE_SUB_LADD] THEN MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `&(CARD(UNIONS(IMAGE (\i. (IMAGE (\b. a i + b) (t INTER (0..(a(i+1) - a(i) - 1))))) (0..A))))` THEN CONJ_TAC THENL [ALL_TAC; REWRITE_TAC[REAL_OF_NUM_LE] THEN MATCH_MP_TAC CARD_SUBSET THEN SIMP_TAC[FINITE_INTER; FINITE_NUMSEG; UNIONS_SUBSET; FORALL_IN_IMAGE] THEN REWRITE_TAC[SUBSET; FORALL_IN_IMAGE] THEN X_GEN_TAC `k:num` THEN DISCH_TAC THEN X_GEN_TAC `l:num` THEN REWRITE_TAC[IN_INTER] THEN REPEAT STRIP_TAC THEN RULE_ASSUM_TAC(REWRITE_RULE[IN_NUMSEG]) THENL [REWRITE_TAC[sumset; IN_ELIM_THM] THEN ASM_MESON_TAC[]; ALL_TAC] THEN REWRITE_TAC[IN_NUMSEG; LE_0] THEN MATCH_MP_TAC(ARITH_RULE `a(k) < a(k + 1) /\ a(k + 1) <= n + 1 /\ l <= a(k + 1) - a(k) - 1 ==> a(k) + l <= n`) THEN ASM_REWRITE_TAC[] THEN CONJ_TAC THENL [FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC; ALL_TAC] THEN ASM_CASES_TAC `k:num = A` THEN ASM_REWRITE_TAC[LE_REFL] THEN REPEAT(FIRST_X_ASSUM(MP_TAC o SPEC `k + 1`)) THEN ASM_ARITH_TAC] THEN W(MP_TAC o PART_MATCH (lhs o rand) CARD_UNIONS o rand o rand o snd) THEN REWRITE_TAC[FORALL_IN_IMAGE; IMP_CONJ; RIGHT_FORALL_IMP_THM] THEN SIMP_TAC[FINITE_IMAGE; FINITE_NUMSEG; FINITE_INTER] THEN SUBGOAL_THEN `!i j. i IN 0..A /\ j IN 0..A /\ ~(i = j) ==> IMAGE (\b. a i + b) (t INTER (0..a (i + 1) - a i - 1)) INTER IMAGE (\b. a j + b) (t INTER (0..a (j + 1) - a j - 1)) = {}` (LABEL_TAC "*") THENL [MAP_EVERY X_GEN_TAC [`i:num`; `j:num`] THEN STRIP_TAC THEN REWRITE_TAC[SET_RULE `IMAGE f s INTER t = {} <=> !x. x IN s ==> ~(f x IN t)`] THEN X_GEN_TAC `k:num` THEN DISCH_TAC THEN REWRITE_TAC[IN_IMAGE] THEN DISCH_THEN(X_CHOOSE_THEN `l:num` STRIP_ASSUME_TAC) THEN RULE_ASSUM_TAC(REWRITE_RULE[IN_NUMSEG; IN_INTER]) THEN SUBGOAL_THEN `a(i + 1):num <= a(j) \/ a(j + 1) <= a(i)` MP_TAC THENL [FIRST_X_ASSUM(DISJ_CASES_TAC o MATCH_MP (ARITH_RULE `~(i = j) ==> i + 1 <= j \/ j + 1 <= i`)) THENL [DISJ1_TAC; DISJ2_TAC] THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC; ALL_TAC] THEN SUBGOAL_THEN `(a:num->num)(i) < a(i + 1) /\ a(j) < a(j + 1)` STRIP_ASSUME_TAC THENL [CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC; ALL_TAC] THEN ASM_ARITH_TAC; ALL_TAC] THEN ANTS_TAC THENL [X_GEN_TAC `i:num` THEN DISCH_TAC THEN X_GEN_TAC `j:num` THEN DISCH_TAC THEN ASM_CASES_TAC `i:num = j` THEN ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[]; ALL_TAC] THEN DISCH_THEN SUBST1_TAC THEN W(MP_TAC o PART_MATCH (lhs o rand) NSUM_IMAGE_NONZERO o rand o rand o snd) THEN REWRITE_TAC[] THEN ANTS_TAC THENL [REWRITE_TAC[FINITE_NUMSEG] THEN MAP_EVERY X_GEN_TAC [`i:num`; `j:num`] THEN STRIP_TAC THEN REMOVE_THEN "*" (MP_TAC o SPECL [`i:num`; `j:num`]) THEN ASM_REWRITE_TAC[INTER_ACI] THEN SIMP_TAC[CARD_CLAUSES]; ALL_TAC] THEN DISCH_THEN SUBST1_TAC THEN REWRITE_TAC[o_DEF] THEN SIMP_TAC[EQ_ADD_LCANCEL; CARD_IMAGE_INJ; FINITE_INTER; FINITE_NUMSEG] THEN SIMP_TAC[REAL_OF_NUM_SUM; FINITE_INTER; FINITE_NUMSEG] THEN MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `sum(0..A) (\i. schnirelmann t * &(a(i + 1) - a(i) - 1) + &1)` THEN CONJ_TAC THENL [ALL_TAC; MATCH_MP_TAC SUM_LE_NUMSEG THEN REWRITE_TAC[] THEN ASM_SIMP_TAC[CARD_INTER_0_1; SUMSET_0; GSYM REAL_OF_NUM_SUC] THEN SIMP_TAC[GSYM count; SCHNIRELMANN_UBOUND_MUL; REAL_LE_RADD]] THEN REWRITE_TAC[SUM_ADD_NUMSEG; SUM_CONST_NUMSEG] THEN REWRITE_TAC[SUB_0; GSYM REAL_OF_NUM_ADD; REAL_MUL_RID] THEN REWRITE_TAC[REAL_ADD_ASSOC; REAL_LE_RADD] THEN MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `sum(0..A) (\i. schnirelmann t * (&(a(i + 1)) - &(a i) - &1)) + &A` THEN CONJ_TAC THENL [ALL_TAC; REWRITE_TAC[REAL_LE_RADD] THEN MATCH_MP_TAC SUM_LE_NUMSEG THEN X_GEN_TAC `i:num` THEN STRIP_TAC THEN SUBGOAL_THEN `a(i):num < a(i + 1)` ASSUME_TAC THENL [FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC; ALL_TAC] THEN ASM_SIMP_TAC[REAL_OF_NUM_SUB; LT_IMP_LE; ARITH_RULE `a < b ==> 1 <= b - a`; REAL_LE_REFL]] THEN REWRITE_TAC[SUM_LMUL] THEN ONCE_REWRITE_TAC[REAL_ARITH `a - b - c:real = --((b - a) + c)`] THEN REWRITE_TAC[SUM_NEG; SUM_ADD_NUMSEG; SUM_DIFFS; LE_0] THEN ASM_REWRITE_TAC[REAL_ARITH `--(&0 - a + b) = a - b`; SUM_CONST_NUMSEG] THEN REWRITE_TAC[SUB_0; GSYM REAL_OF_NUM_ADD; REAL_MUL_RID] THEN REWRITE_TAC[REAL_ARITH `(n + &1) - (a + &1) = n - a`] THEN MATCH_MP_TAC(REAL_ARITH `(&1 - t) * s * n <= (&1 - t) * a ==> ((s + t) - s * t) * n <= t * (n - a) + a`) THEN MATCH_MP_TAC REAL_LE_LMUL THEN EXPAND_TAC "A" THEN REWRITE_TAC[REAL_SUB_LE; SCHNIRELMANN_UBOUND_MUL; GSYM count] THEN REWRITE_TAC[SCHNIRELMANN_BOUNDS]);;
(* ------------------------------------------------------------------------- *) (* Now an iterative form. *) (* ------------------------------------------------------------------------- *)
let SCHNIRELMANN_SUMSET_GEN = 
prove (`!a s. FINITE s /\ (!i:A. i IN s ==> 0 IN a i) ==> schnirelmann(iterate(+++) s a) >= &1 - product s (\i. &1 - schnirelmann(a i))`,
GEN_TAC THEN REWRITE_TAC[IMP_CONJ] THEN MATCH_MP_TAC FINITE_INDUCT_STRONG THEN SIMP_TAC[PRODUCT_CLAUSES; real_ge; REAL_SUB_REFL; SCHNIRELMANN_BOUNDS] THEN MAP_EVERY X_GEN_TAC [`k:A`; `s:A->bool`] THEN STRIP_TAC THEN DISCH_TAC THEN FIRST_ASSUM(MP_TAC o check (is_imp o concl)) THEN ANTS_TAC THENL [ASM_MESON_TAC[IN_INSERT]; DISCH_TAC] THEN ASM_SIMP_TAC[ITERATE_CLAUSES; MONOIDAL_SUMSET] THEN MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `&1 - (&1 - schnirelmann(a(k:A))) * (&1 - schnirelmann(iterate (+++) s a))` THEN CONJ_TAC THENL [MATCH_MP_TAC(REAL_ARITH `a <= b ==> &1 - b <= &1 - a`) THEN MATCH_MP_TAC REAL_LE_LMUL THEN ASM_REWRITE_TAC[REAL_SUB_LE; SCHNIRELMANN_BOUNDS] THEN ASM_REAL_ARITH_TAC; REWRITE_TAC[REAL_ARITH `&1 - (&1 - s) * (&1 - t) <= u <=> u >= (s + t) - s * t`] THEN MATCH_MP_TAC SCHNIRELMANN_SUMSET THEN ASM_SIMP_TAC[IN_INTER; IN_INSERT; SUMSET_0_ITER]]);;
let SCHNIRELMANN_SUMSET_POW = 
prove (`!i s. FINITE i /\ 0 IN s ==> schnirelmann(iterate(+++) i (\k:A. s)) >= &1 - (&1 - schnirelmann s) pow (CARD i)`,
REPEAT STRIP_TAC THEN MP_TAC(ISPECL [`\i:A. (s:num->bool)`; `i:A->bool`] SCHNIRELMANN_SUMSET_GEN) THEN ASM_SIMP_TAC[PRODUCT_CONST]);;
let SCHNIRELMANN = 
prove (`!s. 0 IN s /\ schnirelmann s > &0 ==> ?k. !i. i HAS_SIZE k ==> iterate(+++) i (\a:A. s) = (:num)`,
REPEAT STRIP_TAC THEN REWRITE_TAC[HAS_SIZE] THEN MP_TAC(ISPECL [`&1 - schnirelmann s`; `&1 / &2`] REAL_ARCH_POW_INV) THEN ANTS_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC] THEN DISCH_THEN(X_CHOOSE_TAC `n:num`) THEN EXISTS_TAC `2 * n` THEN X_GEN_TAC `i:A->bool` THEN STRIP_TAC THEN SUBGOAL_THEN `?j k:A->bool. i = j UNION k /\ j INTER k = {} /\ j HAS_SIZE n /\ k HAS_SIZE n` (REPEAT_TCL CHOOSE_THEN (CONJUNCTS_THEN2 SUBST1_TAC STRIP_ASSUME_TAC)) THENL [FIRST_ASSUM(MP_TAC o SPEC `n:num` o MATCH_MP CHOOSE_SUBSET) THEN ASM_REWRITE_TAC[ARITH_RULE `n <= 2 * n`] THEN MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `j:A->bool` THEN STRIP_TAC THEN EXISTS_TAC `i DIFF j:A->bool` THEN MATCH_MP_TAC(TAUT `(a /\ b /\ c) /\ (a /\ b /\ c ==> d) ==> a /\ b /\ c /\ d`) THEN CONJ_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN STRIP_TAC THEN GEN_REWRITE_TAC RAND_CONV [ARITH_RULE `n = 2 * n - n`] THEN MATCH_MP_TAC HAS_SIZE_DIFF THEN ASM_REWRITE_TAC[HAS_SIZE]; ALL_TAC] THEN RULE_ASSUM_TAC(REWRITE_RULE[GSYM DISJOINT; HAS_SIZE]) THEN ASM_SIMP_TAC[MONOIDAL_SUMSET; ITERATE_UNION] THEN MATCH_MP_TAC SCHNIRELMANN_THEOREM THEN ASM_SIMP_TAC[SUMSET_0_ITER; IN_INTER] THEN MP_TAC(SPECL [`j:A->bool`; `s:num->bool`] SCHNIRELMANN_SUMSET_POW) THEN MP_TAC(SPECL [`k:A->bool`; `s:num->bool`] SCHNIRELMANN_SUMSET_POW) THEN ASM_SIMP_TAC[] THEN MATCH_MP_TAC(REAL_ARITH `a < &1 / &2 ==> y >= &1 - a ==> x >= &1 - a ==> x + y >= &1`) THEN ASM_REWRITE_TAC[]);;
(* ------------------------------------------------------------------------- *) (* A more direct version, without the techicality of 0 and sumsets. *) (* ------------------------------------------------------------------------- *)
let SCHNIRELMANN_DIRECT = 
prove (`!s. schnirelmann s > &0 ==> ?k. !n. ?m f. m <= k /\ (!i. i IN 1..m ==> f(i) IN s) /\ n = nsum (1..m) f`,
GEN_TAC THEN STRIP_TAC THEN SUBGOAL_THEN `?k. !i:num->bool. i HAS_SIZE k ==> iterate (+++) i (\a. 0 INSERT s) = (:num)` MP_TAC THENL [MATCH_MP_TAC SCHNIRELMANN THEN REWRITE_TAC[IN_INSERT] THEN POP_ASSUM MP_TAC THEN MATCH_MP_TAC EQ_IMP THEN AP_THM_TAC THEN AP_TERM_TAC THEN MATCH_MP_TAC SCHNIRELMANN_INSENSITIVE THEN SIMP_TAC[IN_INSERT; LE_1]; ALL_TAC] THEN MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `k:num` THEN DISCH_THEN(MP_TAC o SPEC `1..k`) THEN REWRITE_TAC[EXTENSION; HAS_SIZE_NUMSEG_1; IN_UNIV] THEN MATCH_MP_TAC MONO_FORALL THEN SPEC_TAC(`k:num`,`k:num`) THEN POP_ASSUM_LIST(K ALL_TAC) THEN INDUCT_TAC THEN SIMP_TAC[NUMSEG_CLAUSES; ARITH; ARITH_RULE `1 <= SUC k`] THEN SIMP_TAC[ITERATE_CLAUSES; MONOIDAL_SUMSET; FINITE_NUMSEG] THENL [REWRITE_TAC[NEUTRAL_SUMSET; IN_SING] THEN GEN_TAC THEN DISCH_THEN SUBST1_TAC THEN EXISTS_TAC `0` THEN SIMP_TAC[NSUM_CLAUSES_NUMSEG; CARD_CLAUSES; EMPTY_SUBSET; FINITE_RULES; IN_NUMSEG; LE_REFL; ARITH] THEN REWRITE_TAC[ARITH_RULE `~(1 <= i /\ i <= 0)`]; ALL_TAC] THEN REWRITE_TAC[IN_NUMSEG; ARITH_RULE `~(SUC n <= n)`] THEN ONCE_REWRITE_TAC[sumset] THEN REWRITE_TAC[IN_ELIM_THM; IN_INSERT] THEN X_GEN_TAC `n:num` THEN DISCH_THEN(X_CHOOSE_THEN `x:num` MP_TAC) THEN ASM_CASES_TAC `x = 0` THEN ASM_REWRITE_TAC[ADD_CLAUSES] THENL [ASM_MESON_TAC[IN_NUMSEG; ARITH_RULE `x <= k ==> x <= SUC k`]; ALL_TAC] THEN DISCH_THEN(X_CHOOSE_THEN `y:num` STRIP_ASSUME_TAC) THEN FIRST_X_ASSUM(MP_TAC o SPEC `y:num`) THEN ASM_REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN MAP_EVERY X_GEN_TAC [`m:num`; `f:num->num`] THEN STRIP_TAC THEN MAP_EVERY EXISTS_TAC [`SUC m`; `\i. if i = SUC m then x:num else f i`] THEN ASM_SIMP_TAC[LE_SUC; LE; NSUM_CLAUSES_NUMSEG] THEN CONJ_TAC THENL [ASM_MESON_TAC[ARITH_RULE `~(SUC n <= n)`; IN_NUMSEG]; ALL_TAC] THEN REWRITE_TAC[ARITH_RULE `1 = SUC m \/ 1 <= m`] THEN GEN_REWRITE_TAC RAND_CONV [ADD_SYM] THEN AP_TERM_TAC THEN MATCH_MP_TAC NSUM_EQ THEN ASM_MESON_TAC[ARITH_RULE `~(SUC n <= n)`; IN_NUMSEG]);;