Examples/harmonicsum.ml

   1 (* ========================================================================= *)
   2 (* Nice little result that harmonic sum never gives an integer.              *)
   3 (* ========================================================================= *)
   4
   5 needs "Library/prime.ml";;
   6 needs "Library/products.ml";;
   7 needs "Library/floor.ml";;
   8
   9 (* ------------------------------------------------------------------------- *)
  10 (* In any contiguous range, index (order) of 2 has a strict maximum.         *)
  11 (* ------------------------------------------------------------------------- *)
  12
  13 let NUMSEG_MAXIMAL_INDEX_2 = prove
  14  (`!m n. 1 <= m /\ m <= n
  15          ==> ?k. k IN m..n /\
  16                  !l. l IN m..n /\ ~(l = k) ==> index 2 l < index 2 k`,
  17   REPEAT STRIP_TAC THEN
  18   MP_TAC(ISPEC `\x. x IN IMAGE (index 2) (m..n)` num_MAX) THEN
  19   REWRITE_TAC[FORALL_IN_IMAGE; EXISTS_IN_IMAGE; IN_NUMSEG] THEN
  20   ASM_REWRITE_TAC[MEMBER_NOT_EMPTY; IMAGE_EQ_EMPTY; NUMSEG_EMPTY; NOT_LT] THEN
  21   MATCH_MP_TAC(TAUT `p /\ (q ==> r) ==> (p <=> q) ==> r`) THEN
  22   CONJ_TAC THENL [MESON_TAC[INDEX_TRIVIAL_BOUND; LE_TRANS]; ALL_TAC] THEN
  23   MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `k:num` THEN
  24   STRIP_TAC THEN ASM_SIMP_TAC[LT_LE] THEN X_GEN_TAC `l:num` THEN STRIP_TAC THEN
  25   MP_TAC(SPECL [`l:num`; `2`] INDEX_DECOMPOSITION_PRIME) THEN
  26   MP_TAC(SPECL [`k:num`; `2`] INDEX_DECOMPOSITION_PRIME) THEN
  27   REWRITE_TAC[PRIME_2; LEFT_IMP_EXISTS_THM; COPRIME_2] THEN
  28   ASM_CASES_TAC `k = 0` THENL [ASM_ARITH_TAC; ASM_REWRITE_TAC[]] THEN
  29   ASM_CASES_TAC `l = 0` THENL [ASM_ARITH_TAC; ASM_REWRITE_TAC[]] THEN
  30   X_GEN_TAC `p:num` THEN STRIP_TAC THEN X_GEN_TAC `q:num` THEN STRIP_TAC THEN
  31   DISCH_THEN SUBST_ALL_TAC THEN
  32   MP_TAC(ARITH_RULE `~(l:num = k) ==> l < k \/ k < l`) THEN
  33   ASM_REWRITE_TAC[] THEN DISCH_THEN(DISJ_CASES_THEN MP_TAC) THEN
  34   MAP_EVERY EXPAND_TAC ["k"; "l"] THEN
  35   REWRITE_TAC[LT_MULT_LCANCEL; EXP_EQ_0; ARITH_EQ] THEN DISCH_TAC THENL
  36    [FIRST_X_ASSUM(MP_TAC o SPEC `2 EXP index 2 k * (q + 1)`);
  37     FIRST_X_ASSUM(MP_TAC o SPEC `2 EXP index 2 k * (p + 1)`)] THEN
  38   ASM_SIMP_TAC[INDEX_MUL; PRIME_2; EXP_EQ_0; ADD_EQ_0; ARITH; NOT_IMP;
  39                INDEX_EXP; INDEX_REFL] THEN
  40   REWRITE_TAC[ARITH_RULE `n * 1 + k <= n <=> k = 0`; INDEX_EQ_0] THEN
  41   ASM_REWRITE_TAC[ADD_EQ_0; ARITH; DIVIDES_2; EVEN_ADD; NOT_EVEN] THEN
  42   MATCH_MP_TAC(ARITH_RULE
  43    `!p. m <= e * q /\ e * (q + 1) <= e * p /\ e * p <= n
  44          ==> m <= e * (q + 1) /\ e * (q + 1) <= n`)
  45   THENL [EXISTS_TAC `p:num`; EXISTS_TAC `q:num`] THEN
  46   REWRITE_TAC[LE_MULT_LCANCEL] THEN ASM_REWRITE_TAC[] THEN
  47   ASM_ARITH_TAC);;
  48
  49 (* ------------------------------------------------------------------------- *)
  50 (* Hence the result.                                                         *)
  51 (* ------------------------------------------------------------------------- *)
  52
  53 let NONINTEGER_HARMONIC = prove
  54  (`!m n. 1 <= m /\ 1 < n /\ m <= n ==> ~(integer (sum(m..n) (\k. inv(&k))))`,
  55   let lemma = prove
  56    (`!m n. 1 <= m
  57            ==> sum(m..n) (\k. inv(&k)) =
  58                (sum(m..n) (\k. product ((m..n) DELETE k) (\i. &i))) /
  59                product(m..n) (\i. &i)`,
  60     REPEAT STRIP_TAC THEN REWRITE_TAC[real_div; GSYM SUM_RMUL] THEN
  61     MATCH_MP_TAC SUM_EQ_NUMSEG THEN X_GEN_TAC `k:num` THEN STRIP_TAC THEN
  62     REWRITE_TAC[] THEN MATCH_MP_TAC(REAL_FIELD
  63      `~(x = &0) /\ ~(z = &0) /\ x * y = z
  64       ==> inv x = y * inv z`) THEN
  65     ASM_SIMP_TAC[PRODUCT_EQ_0; FINITE_NUMSEG; IN_NUMSEG; REAL_OF_NUM_EQ] THEN
  66     REPEAT(CONJ_TAC THENL [ASM_ARITH_TAC; ALL_TAC]) THEN
  67     MP_TAC(ISPECL [`\i. &i`; `m..n`; `k:num`] PRODUCT_DELETE) THEN
  68     ASM_REWRITE_TAC[FINITE_NUMSEG; IN_NUMSEG]) in
  69   REPEAT GEN_TAC THEN STRIP_TAC THEN ASM_CASES_TAC `n:num = m` THENL
  70    [ASM_REWRITE_TAC[SUM_SING_NUMSEG] THEN
  71     REWRITE_TAC[REAL_ARITH `inv x = &1 / x`; INTEGER_DIV; DIVIDES_ONE] THEN
  72     ASM_ARITH_TAC;
  73     ALL_TAC] THEN
  74   ASM_SIMP_TAC[lemma] THEN
  75   SIMP_TAC[GSYM REAL_OF_NUM_NPRODUCT; FINITE_NUMSEG; GSYM REAL_OF_NUM_SUM;
  76            FINITE_DELETE; INTEGER_DIV] THEN
  77   SIMP_TAC[NPRODUCT_EQ_0; FINITE_NUMSEG; IN_NUMSEG; DE_MORGAN_THM] THEN
  78   CONJ_TAC THENL [ASM_ARITH_TAC; ALL_TAC] THEN
  79   MP_TAC(SPECL [`m:num`; `n:num`] NUMSEG_MAXIMAL_INDEX_2) THEN
  80   ASM_REWRITE_TAC[IN_NUMSEG] THEN
  81   DISCH_THEN(X_CHOOSE_THEN `k:num` STRIP_ASSUME_TAC) THEN
  82   MP_TAC(ISPECL [`\i. nproduct((m..n) DELETE i) (\j. j)`; `m..n`; `k:num`]
  83      NSUM_DELETE) THEN
  84   ASM_REWRITE_TAC[IN_NUMSEG; FINITE_NUMSEG] THEN
  85   DISCH_THEN(SUBST1_TAC o SYM) THEN
  86   ABBREV_TAC `i = index 2 (nproduct ((m..n) DELETE k) (\j. j))` THEN
  87   MATCH_MP_TAC(EQT_ELIM(
  88    (REWRITE_CONV[IMP_CONJ; CONTRAPOS_THM] THENC (EQT_INTRO o NUMBER_RULE))
  89    `!p. p divides r /\ p divides n /\ ~(p divides m)
  90        ==> ~(r divides (m + n))`)) THEN
  91   EXISTS_TAC `2 EXP (i + 1)` THEN REPEAT CONJ_TAC THENL
  92    [ALL_TAC;
  93     MATCH_MP_TAC DIVIDES_NSUM THEN
  94     REWRITE_TAC[FINITE_NUMSEG; FINITE_DELETE; IN_NUMSEG; IN_DELETE] THEN
  95     X_GEN_TAC `l:num` THEN STRIP_TAC;
  96     ALL_TAC] THEN
  97   REWRITE_TAC[PRIMEPOW_DIVIDES_INDEX] THEN
  98   SIMP_TAC[ARITH; DE_MORGAN_THM; NPRODUCT_EQ_0; FINITE_NUMSEG; FINITE_DELETE;
  99            IN_NUMSEG; IN_DELETE]
 100   THENL
 101    [DISJ2_TAC THEN
 102     MP_TAC(ISPECL [`\i:num. i`; `m..n`; `k:num`] NPRODUCT_DELETE) THEN
 103     ASM_REWRITE_TAC[FINITE_NUMSEG; IN_NUMSEG] THEN
 104     DISCH_THEN(MP_TAC o AP_TERM `index 2`) THEN IMP_REWRITE_TAC[INDEX_MUL] THEN
 105     SIMP_TAC[NPRODUCT_EQ_0; FINITE_NUMSEG; FINITE_DELETE; PRIME_2] THEN
 106     REWRITE_TAC[IN_DELETE; IN_NUMSEG] THEN
 107     ANTS_TAC THENL [ASM_ARITH_TAC; DISCH_THEN(SUBST1_TAC o SYM)] THEN
 108     FIRST_X_ASSUM(fun th ->
 109      MP_TAC(SPEC `m:num` th) THEN MP_TAC(SPEC `n:num` th)) THEN
 110     ASM_ARITH_TAC;
 111     DISJ2_TAC THEN
 112     MP_TAC(ISPECL [`\i:num. i`; `m..n`; `l:num`] NPRODUCT_DELETE) THEN
 113     MP_TAC(ISPECL [`\i:num. i`; `m..n`; `k:num`] NPRODUCT_DELETE) THEN
 114     ASM_REWRITE_TAC[FINITE_NUMSEG; IN_NUMSEG; IMP_IMP] THEN
 115     DISCH_THEN(CONJUNCTS_THEN (MP_TAC o AP_TERM `index 2`)) THEN
 116     IMP_REWRITE_TAC[INDEX_MUL] THEN
 117     SIMP_TAC[NPRODUCT_EQ_0; FINITE_NUMSEG; FINITE_DELETE; PRIME_2] THEN
 118     REWRITE_TAC[IN_DELETE; IN_NUMSEG] THEN
 119     ANTS_TAC THENL [ASM_ARITH_TAC; DISCH_TAC] THEN
 120     ANTS_TAC THENL [ASM_ARITH_TAC; ALL_TAC] THEN
 121     FIRST_X_ASSUM(SUBST1_TAC o SYM) THEN ASM_REWRITE_TAC[] THEN
 122     FIRST_X_ASSUM(MP_TAC o SPEC `l:num`) THEN ASM_ARITH_TAC;
 123     ASM_REWRITE_TAC[] THEN ASM_ARITH_TAC]);;