(* ========================================================================= *)
(* #26: Leibniz's series for pi                                              *)
(* ========================================================================= *)

needs "Library/transc.ml";;

prioritize_real();;

(* ------------------------------------------------------------------------- *)
(* Summability of alternating series.                                        *)
(* ------------------------------------------------------------------------- *)

let ALTERNATING_SUM_BOUNDS = 
prove (`!a. (!n. a(2 * n + 1) <= &0 /\ &0 <= a(2 * n)) /\ (!n. abs(a(n + 1)) <= abs(a(n))) ==> !m n. (EVEN m ==> &0 <= sum(m,n) a /\ sum(m,n) a <= a(m)) /\ (ODD m ==> a(m) <= sum(m,n) a /\ sum(m,n) a <= &0)`,
GEN_TAC THEN STRIP_TAC THEN ONCE_REWRITE_TAC[SWAP_FORALL_THM] THEN INDUCT_TAC THEN REWRITE_TAC[ODD; EVEN] THENL [SIMP_TAC[sum; ODD_EXISTS; EVEN_EXISTS; LEFT_IMP_EXISTS_THM; ADD1] THEN ASM_SIMP_TAC[REAL_LE_REFL]; ALL_TAC] THEN X_GEN_TAC `m:num` THEN REWRITE_TAC[ARITH_RULE `SUC n = 1 + n`; GSYM SUM_SPLIT] THEN FIRST_X_ASSUM(MP_TAC o check (is_conj o concl) o SPEC `SUC m`) THEN REWRITE_TAC[ODD; EVEN; SUM_1] THEN REWRITE_TAC[ADD1; GSYM NOT_EVEN] THEN UNDISCH_THEN `!n. abs(a(n + 1)) <= abs(a n)` (MP_TAC o SPEC `m:num`) THEN ASM_CASES_TAC `EVEN m` THEN ASM_REWRITE_TAC[] THENL [FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [EVEN_EXISTS]) THEN DISCH_THEN(X_CHOOSE_THEN `p:num` SUBST_ALL_TAC) THEN FIRST_X_ASSUM(MP_TAC o SPEC `p:num`) THEN REAL_ARITH_TAC; FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [NOT_EVEN]) THEN REWRITE_TAC[ODD_EXISTS] THEN DISCH_THEN(X_CHOOSE_THEN `p:num` SUBST_ALL_TAC) THEN REWRITE_TAC[ADD1] THEN FIRST_X_ASSUM(MP_TAC o SPEC `p:num`) THEN REAL_ARITH_TAC]);;
let ALTERNATING_SUM_BOUND = 
prove (`!a. (!n. a(2 * n + 1) <= &0 /\ &0 <= a(2 * n)) /\ (!n. abs(a(n + 1)) <= abs(a(n))) ==> !m n. abs(sum(m,n) a) <= abs(a m)`,
GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP ALTERNATING_SUM_BOUNDS) THEN REPEAT(MATCH_MP_TAC MONO_FORALL THEN GEN_TAC) THEN REWRITE_TAC[GSYM NOT_EVEN] THEN ASM_CASES_TAC `EVEN m` THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);;
let SUMMABLE_ALTERNATING = 
prove (`!v. (!n. a(2 * n + 1) <= &0 /\ &0 <= a(2 * n)) /\ (!n. abs(a(n + 1)) <= abs(a(n))) /\ a tends_num_real &0 ==> summable a`,
REPEAT STRIP_TAC THEN REWRITE_TAC[SER_CAUCHY] THEN X_GEN_TAC `e:real` THEN STRIP_TAC THEN FIRST_X_ASSUM(MP_TAC o SPEC `e:real` o GEN_REWRITE_RULE I [SEQ]) THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `N:num` THEN REWRITE_TAC[REAL_SUB_RZERO] THEN ASM_MESON_TAC[ALTERNATING_SUM_BOUND; REAL_LET_TRANS]);;
(* ------------------------------------------------------------------------- *) (* Another version of the atan series. *) (* ------------------------------------------------------------------------- *)
let REAL_ATN_POWSER_ALT = 
prove (`!x. abs(x) < &1 ==> (\n. (-- &1) pow n / &(2 * n + 1) * x pow (2 * n + 1)) sums (atn x)`,
REPEAT STRIP_TAC THEN FIRST_ASSUM(ASSUME_TAC o MATCH_MP REAL_ATN_POWSER) THEN FIRST_ASSUM(MP_TAC o C CONJ (ARITH_RULE `0 < 2`) o MATCH_MP SUM_SUMMABLE) THEN DISCH_THEN(MP_TAC o MATCH_MP SER_GROUP) THEN FIRST_ASSUM(SUBST1_TAC o SYM o MATCH_MP SUM_UNIQ) THEN REWRITE_TAC[SUM_2; EVEN_MULT; EVEN_ADD; ARITH_EVEN; ADD_SUB] THEN ONCE_REWRITE_TAC[ARITH_RULE `n * 2 = 2 * n`] THEN SIMP_TAC[DIV_MULT; ARITH_EQ; REAL_MUL_LZERO; REAL_ADD_LID]);;
(* ------------------------------------------------------------------------- *) (* Summability of the same series for x = 1. *) (* ------------------------------------------------------------------------- *)
let SUMMABLE_LEIBNIZ = 
prove (`summable (\n. (-- &1) pow n / &(2 * n + 1))`,
MATCH_MP_TAC SUMMABLE_ALTERNATING THEN REWRITE_TAC[] THEN REPEAT CONJ_TAC THENL [REWRITE_TAC[REAL_POW_ADD; REAL_POW_MUL; GSYM REAL_POW_POW] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN REWRITE_TAC[REAL_POW_ONE; real_div; REAL_MUL_LID; REAL_MUL_LNEG] THEN REWRITE_TAC[REAL_LE_LNEG; REAL_ADD_RID; REAL_LE_INV_EQ; REAL_POS]; GEN_TAC THEN REWRITE_TAC[REAL_ABS_DIV; REAL_ABS_POW; REAL_ABS_NEG] THEN REWRITE_TAC[REAL_ABS_NUM; REAL_POW_ONE; real_div; REAL_MUL_LID] THEN MATCH_MP_TAC REAL_LE_INV2 THEN REWRITE_TAC[REAL_OF_NUM_LT; REAL_OF_NUM_LE] THEN ARITH_TAC; REWRITE_TAC[SEQ; REAL_SUB_RZERO; REAL_ABS_DIV; REAL_ABS_POW] THEN REWRITE_TAC[REAL_ABS_NEG; REAL_ABS_NUM; REAL_POW_ONE] THEN SIMP_TAC[REAL_LT_LDIV_EQ; REAL_OF_NUM_LT; ARITH_RULE `0 < n + 1`] THEN GEN_TAC THEN DISCH_TAC THEN FIRST_ASSUM(MP_TAC o SPEC `&1` o MATCH_MP REAL_ARCH) THEN MATCH_MP_TAC MONO_EXISTS THEN REWRITE_TAC[GE] THEN REPEAT STRIP_TAC THEN FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_ARITH `&1 < x * e ==> e * x <= y ==> &1 < y`)) THEN ASM_SIMP_TAC[REAL_LE_LMUL_EQ; REAL_OF_NUM_LE] THEN ASM_ARITH_TAC]);;
(* ------------------------------------------------------------------------- *) (* The tricky sum-bounding lemma. *) (* ------------------------------------------------------------------------- *)
let SUM_DIFFERENCES = 
prove (`!a m n. m <= n + 1 ==> sum(m..n) (\i. a(i) - a(i+1)) = a(m) - a(n + 1)`,
GEN_TAC THEN GEN_TAC THEN INDUCT_TAC THENL [REWRITE_TAC[ARITH_RULE `m <= 0 + 1 <=> m = 0 \/ m = 1`] THEN STRIP_TAC THEN ASM_REWRITE_TAC[SUM_SING_NUMSEG] THEN ASM_SIMP_TAC[SUM_TRIV_NUMSEG; ARITH; REAL_SUB_REFL]; ALL_TAC] THEN REWRITE_TAC[ARITH_RULE `m <= SUC n + 1 <=> m <= n + 1 \/ m = SUC n + 1`] THEN STRIP_TAC THEN ASM_SIMP_TAC[SUM_TRIV_NUMSEG; ARITH_RULE `n < n + 1`; REAL_SUB_REFL] THEN ASM_SIMP_TAC[SUM_CLAUSES_NUMSEG; ARITH_RULE `m <= n + 1 ==> m <= SUC n /\ m <= SUC n + 1`] THEN REWRITE_TAC[ADD1] THEN REAL_ARITH_TAC);;
let SUM_REARRANGE_LEMMA = 
prove (`!a v m n. m <= n + 1 ==> sum(m..n+1) (\i. a i * v i) = sum(m..n) (\k. sum(m..k) a * (v(k) - v(k+1))) + sum(m..n+1) a * v(n+1)`,
REPLICATE_TAC 3 GEN_TAC THEN INDUCT_TAC THENL [REWRITE_TAC[SUM_CLAUSES_NUMSEG; num_CONV `1`; ADD_CLAUSES] THEN ASM_CASES_TAC `m = 0` THEN ASM_REWRITE_TAC[ARITH] THEN REAL_ARITH_TAC; ALL_TAC] THEN REWRITE_TAC[ADD_CLAUSES; SUM_CLAUSES_NUMSEG] THEN DISCH_TAC THEN FIRST_X_ASSUM(MP_TAC o check (is_imp o concl)) THEN ASM_CASES_TAC `m = SUC(n + 1)` THENL [ASM_REWRITE_TAC[LE_SUC; ARITH_RULE `~(n + 1 <= n)`] THEN ASM_SIMP_TAC[SUM_TRIV_NUMSEG; ARITH_RULE `n < SUC n /\ n < SUC(n + 1)`] THEN REAL_ARITH_TAC; ALL_TAC] THEN ANTS_TAC THENL [ASM_ARITH_TAC; ALL_TAC] THEN DISCH_THEN SUBST1_TAC THEN ASM_REWRITE_TAC[] THEN ONCE_REWRITE_TAC[ARITH_RULE `m <= SUC n <=> m <= SUC(n + 1) /\ ~(m = SUC(n + 1))`] THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[GSYM REAL_ADD_ASSOC; REAL_EQ_ADD_LCANCEL] THEN REWRITE_TAC[REAL_ADD_ASSOC; REAL_ADD_RDISTRIB; REAL_EQ_ADD_RCANCEL] THEN REWRITE_TAC[GSYM ADD1; SUM_CLAUSES_NUMSEG] THEN ASM_SIMP_TAC[ARITH_RULE `m <= SUC(n + 1) /\ ~(m = SUC(n + 1)) ==> m <= SUC n`] THEN REWRITE_TAC[REAL_ARITH `(s1 * (v - w) + x) + (s2 + y) * w = (x + y * w) + (v - w) * s1 + w * s2`] THEN GEN_REWRITE_TAC LAND_CONV [REAL_MUL_SYM] THEN SIMP_TAC[REAL_ADD_LDISTRIB; GSYM SUM_CMUL; GSYM SUM_ADD_NUMSEG] THEN REWRITE_TAC[REAL_SUB_ADD; REAL_SUB_RDISTRIB] THEN REAL_ARITH_TAC);;
let SUM_BOUNDS_LEMMA = 
prove (`!a v l u m n. m <= n /\ (!i. m <= i /\ i <= n ==> &0 <= v(i) /\ v(i+1) <= v(i)) /\ (!k. m <= k /\ k <= n ==> l <= sum(m..k) a /\ sum(m..k) a <= u) ==> l * v(m) <= sum(m..n) (\i. a(i) * v(i)) /\ sum(m..n) (\i. a(i) * v(i)) <= u * v(m)`,
REPLICATE_TAC 5 GEN_TAC THEN INDUCT_TAC THENL [REWRITE_TAC[LE; SUM_CLAUSES_NUMSEG] THEN SIMP_TAC[ARITH_RULE `m <= i /\ i = 0 <=> m = 0 /\ i = 0`] THEN REWRITE_TAC[LEFT_FORALL_IMP_THM; RIGHT_EXISTS_AND_THM; EXISTS_REFL] THEN ASM_CASES_TAC `m = 0` THEN ASM_REWRITE_TAC[SUM_SING_NUMSEG] THEN SIMP_TAC[REAL_LE_RMUL]; POP_ASSUM(K ALL_TAC) THEN REWRITE_TAC[ADD1]] THEN SIMP_TAC[SUM_REARRANGE_LEMMA] THEN STRIP_TAC THEN CONJ_TAC THENL [MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `sum(m..n) (\k. l * (v(k) - v(k + 1))) + l * v(n+1)` THEN CONJ_TAC THENL [ASM_SIMP_TAC[SUM_LMUL; SUM_DIFFERENCES] THEN REAL_ARITH_TAC; ALL_TAC]; MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `sum(m..n) (\k. u * (v(k) - v(k + 1))) + u * v(n+1)` THEN CONJ_TAC THENL [ALL_TAC; ASM_SIMP_TAC[SUM_LMUL; SUM_DIFFERENCES] THEN REAL_ARITH_TAC]] THEN MATCH_MP_TAC REAL_LE_ADD2 THEN ASM_SIMP_TAC[REAL_LE_RMUL; LE_REFL] THEN MATCH_MP_TAC SUM_LE_NUMSEG THEN X_GEN_TAC `k:num` THEN STRIP_TAC THEN REWRITE_TAC[] THEN MATCH_MP_TAC REAL_LE_RMUL THEN ASM_SIMP_TAC[REAL_SUB_LE; ARITH_RULE `k <= n ==> k <= n + 1`]);;
let SUM_BOUND_LEMMA = 
prove (`!a v b m n. m <= n /\ (!i. m <= i /\ i <= n ==> &0 <= v(i) /\ v(i+1) <= v(i)) /\ (!k. m <= k /\ k <= n ==> abs(sum(m..k) a) <= b) ==> abs(sum(m..n) (\i. a(i) * v(i))) <= b * abs(v m)`,
REPEAT STRIP_TAC THEN MATCH_MP_TAC(REAL_ARITH `--b * k <= a /\ a <= b * k ==> abs(a) <= b * k`) THEN ASM_SIMP_TAC[LE_REFL; real_abs] THEN MATCH_MP_TAC SUM_BOUNDS_LEMMA THEN ASM_REWRITE_TAC[REAL_BOUNDS_LE]);;
(* ------------------------------------------------------------------------- *) (* Hence the final theorem. *) (* ------------------------------------------------------------------------- *)
let LEIBNIZ_PI = 
prove (`(\n. (-- &1) pow n / &(2 * n + 1)) sums (pi / &4)`,
REWRITE_TAC[GSYM ATN_1] THEN ASSUME_TAC(MATCH_MP SUMMABLE_SUM SUMMABLE_LEIBNIZ) THEN ABBREV_TAC `s = suminf(\n. (-- &1) pow n / &(2 * n + 1))` THEN SUBGOAL_THEN `s = atn(&1)` (fun th -> ASM_MESON_TAC[th]) THEN MATCH_MP_TAC(REAL_ARITH `~(&0 < abs(x - y)) ==> x = y`) THEN ABBREV_TAC `e = abs(s - atn(&1))` THEN DISCH_TAC THEN FIRST_ASSUM(MP_TAC o MATCH_MP SUM_SUMMABLE) THEN REWRITE_TAC[SER_CAUCHY] THEN DISCH_THEN(MP_TAC o SPEC `e / &7`) THEN ASM_SIMP_TAC[REAL_LT_DIV; REAL_OF_NUM_LT; ARITH] THEN DISCH_THEN(X_CHOOSE_THEN `N:num` STRIP_ASSUME_TAC) THEN SUBGOAL_THEN `(\x. sum(0,N) (\n. (-- &1) pow n / &(2 * n + 1) * x pow (2 * n + 1))) contl (&1)` MP_TAC THENL [MATCH_MP_TAC DIFF_CONT THEN EXISTS_TAC `sum(0,N) (\n. (-- &1) pow n * &1 pow (2 * n))` THEN MATCH_MP_TAC DIFF_SUM THEN X_GEN_TAC `k:num` THEN STRIP_TAC THEN REWRITE_TAC[real_div; GSYM REAL_MUL_ASSOC] THEN MATCH_MP_TAC DIFF_CMUL THEN MP_TAC(SPECL [`2 * k + 1`; `&1`] DIFF_POW) THEN DISCH_THEN(MP_TAC o SPEC `inv(&(2 * k + 1))` o MATCH_MP DIFF_CMUL) THEN MATCH_MP_TAC(TAUT `a = b ==> a ==> b`) THEN REWRITE_TAC[ADD_SUB] THEN AP_THM_TAC THEN AP_TERM_TAC THEN REWRITE_TAC[GSYM REAL_OF_NUM_ADD; GSYM REAL_OF_NUM_MUL] THEN REWRITE_TAC[REAL_POW_ONE] THEN CONV_TAC REAL_FIELD; ALL_TAC] THEN SUBGOAL_THEN `atn contl (&1)` MP_TAC THENL [MESON_TAC[DIFF_CONT; DIFF_ATN]; ALL_TAC] THEN REWRITE_TAC[CONTL_LIM; LIM] THEN REWRITE_TAC[TAUT `a ==> ~b <=> ~(a /\ b)`; AND_FORALL_THM] THEN DISCH_THEN(MP_TAC o SPEC `e / &6`) THEN ASM_SIMP_TAC[REAL_LT_DIV; REAL_OF_NUM_LT; ARITH; GSYM SUM_SUB] THEN ONCE_REWRITE_TAC[GSYM REAL_ABS_NEG] THEN REWRITE_TAC[GSYM SUM_NEG; REAL_NEG_SUB; GSYM REAL_MUL_RNEG] THEN REWRITE_TAC[REAL_POW_ONE; GSYM REAL_SUB_LDISTRIB] THEN DISCH_THEN (CONJUNCTS_THEN2 (X_CHOOSE_THEN `d1:real` STRIP_ASSUME_TAC) (X_CHOOSE_THEN `d2:real` STRIP_ASSUME_TAC)) THEN ABBREV_TAC `x = &1 - min (min (d1 / &2) (d2 / &2)) (&1 / &2)` THEN REPEAT(FIRST_X_ASSUM (MP_TAC o SPEC `x:real`) THEN ANTS_TAC THENL [ASM_REAL_ARITH_TAC; DISCH_TAC]) THEN SUBGOAL_THEN `&0 < x /\ x < &1 /\ abs x < &1` STRIP_ASSUME_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC] THEN FIRST_X_ASSUM(MP_TAC o MATCH_MP REAL_ATN_POWSER_ALT) THEN REWRITE_TAC[sums; SEQ] THEN DISCH_THEN(MP_TAC o SPEC `e / &6`) THEN ASM_SIMP_TAC[REAL_LT_DIV; REAL_OF_NUM_LT; ARITH] THEN DISCH_THEN(X_CHOOSE_TAC `N1:num`) THEN FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [sums]) THEN REWRITE_TAC[SEQ] THEN DISCH_THEN(MP_TAC o SPEC `e / &6`) THEN ASM_SIMP_TAC[REAL_LT_DIV; REAL_OF_NUM_LT; ARITH] THEN DISCH_THEN(X_CHOOSE_TAC `N2:num`) THEN REPEAT(FIRST_X_ASSUM(MP_TAC o SPEC `N + N1 + N2:num`) THEN ANTS_TAC THENL [ARITH_TAC; ALL_TAC]) THEN REWRITE_TAC[] THEN ONCE_REWRITE_TAC[GSYM SUM_SPLIT] THEN REWRITE_TAC[ADD_CLAUSES] THEN REPEAT STRIP_TAC THEN SUBGOAL_THEN `abs(sum(N,N1+N2) (\n. -- &1 pow n / &(2 * n + 1) * x pow (2 * n + 1))) < e / &6` ASSUME_TAC THENL [ASM_CASES_TAC `N1 + N2 = 0` THENL [ASM_SIMP_TAC[sum; REAL_LT_DIV; REAL_OF_NUM_LT; REAL_ABS_NUM; ARITH]; ALL_TAC] THEN MATCH_MP_TAC(REAL_ARITH `x <= e / &7 /\ &0 < e ==> x < e / &6`) THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `e / &7 * abs(x pow (2 * N + 1))` THEN CONJ_TAC THENL [ALL_TAC; GEN_REWRITE_TAC RAND_CONV [GSYM REAL_MUL_RID] THEN MATCH_MP_TAC REAL_LE_LMUL THEN REWRITE_TAC[REAL_ABS_POS] THEN ASM_SIMP_TAC[REAL_LT_IMP_LE; REAL_LT_DIV; REAL_OF_NUM_LT; ARITH] THEN REWRITE_TAC[REAL_ABS_POW; REAL_ABS_NUM] THEN MATCH_MP_TAC REAL_POW_1_LE THEN MAP_EVERY UNDISCH_TAC [`&0 < x`; `x < &1`] THEN REAL_ARITH_TAC] THEN ASM_SIMP_TAC[PSUM_SUM_NUMSEG] THEN MATCH_MP_TAC SUM_BOUND_LEMMA THEN CONJ_TAC THENL [UNDISCH_TAC `~(N1 + N2 = 0)` THEN ARITH_TAC; ALL_TAC] THEN REPEAT STRIP_TAC THENL [ASM_SIMP_TAC[REAL_LT_IMP_LE; REAL_POW_LT]; REWRITE_TAC[ARITH_RULE `2 * (m + 1) + 1 = (2 * m + 1) + 2`] THEN GEN_REWRITE_TAC LAND_CONV [REAL_POW_ADD] THEN GEN_REWRITE_TAC RAND_CONV [GSYM REAL_MUL_RID] THEN MATCH_MP_TAC REAL_LE_LMUL THEN ASM_SIMP_TAC[REAL_POW_LE; REAL_POW_1_LE; REAL_LT_IMP_LE]; MATCH_MP_TAC REAL_LT_IMP_LE THEN FIRST_X_ASSUM(MP_TAC o SPECL [`N:num`; `(k - N:num) + 1`]) THEN SIMP_TAC[PSUM_SUM_NUMSEG; ADD_EQ_0; ARITH_EQ] THEN ASM_SIMP_TAC[ARITH_RULE `N <= k ==> (N + (k - N) + 1) - 1 = k`] THEN REWRITE_TAC[GE; LE_REFL; REAL_LT_IMP_LE]]; ALL_TAC] THEN FIRST_X_ASSUM(MP_TAC o SPECL [`N:num`; `N1 + N2:num`]) THEN REWRITE_TAC[GE; LE_REFL] THEN FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_ARITH `abs((slo + shi) - s) < e / &6 ==> ~(abs(slo - s) < e / &3) ==> ~(abs(shi) < e / &7)`)) THEN RULE_ASSUM_TAC(REWRITE_RULE[REAL_SUB_LDISTRIB; SUM_SUB; REAL_MUL_RID]) THEN FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_ARITH `abs(s1 - sx) < e / &6 ==> ~(abs(sx - s) < e / &2) ==> ~(abs(s1 - s) < e / &3)`)) THEN ASM_REAL_ARITH_TAC);;