(* split off from misc_defs_and_lemmas.ml *)


(* ------------------------------------------------------------------ *)
(* COMPUTING PI *)
(* ------------------------------------------------------------------ *)

Parse_ext_override_interface.unambiguous_interface();;
Parse_ext_override_interface.prioritize_real();;

(* ------------------------------------------------------------------ *)
(* general series approximations *)
(* ------------------------------------------------------------------ *)

let SER_APPROX1 = prove_by_refinement(
  `!s f g.  (f sums s) /\ (summable g) ==>
    (!k. ((!n. (||. (f (n+k)) <=. (g (n+k)))) ==>
    ( (s - (sum(0,k) f)) <=. (suminf (\n. (g (n +| k)))))))`,
  (* {{{ proof *)
  [
  REPEAT GEN_TAC;
  DISCH_ALL_TAC;
  GEN_TAC;
  DISCH_TAC;
  IMP_RES_THEN ASSUME_TAC SUM_SUMMABLE;
  IMP_RES_THEN (fun th -> (ASSUME_TAC (SPEC `k:num` th))) SER_OFFSET;
  IMP_RES_THEN ASSUME_TAC SUM_UNIQ;
  SUBGOAL_THEN `(\n. (f (n+ k))) sums (s - (sum(0,k) f))` ASSUME_TAC;
  ASM_MESON_TAC[];
  SUBGOAL_THEN `summable (\n. (f (n+k))) /\ (suminf (\n. (f (n+k))) <=. (suminf (\n. (g (n+k)))))` ASSUME_TAC;
  MATCH_MP_TAC SER_LE2;
  BETA_TAC;
  ASM_REWRITE_TAC[];
  IMP_RES_THEN ASSUME_TAC SER_OFFSET;
  FIRST_X_ASSUM (fun th -> ACCEPT_TAC (MATCH_MP SUM_SUMMABLE (((SPEC `k:num`) th))));
  ASM_MESON_TAC[SUM_UNIQ]
  ]);;
  (* }}} *)

let SER_APPROX = prove_by_refinement(
  `!s f g.  (f sums s) /\ (!n. (||. (f n) <=. (g n))) /\
       (summable g) ==>
    (!k. (abs (s - (sum(0,k) f)) <=. (suminf (\n. (g (n +| k))))))`,
  (* {{{ proof *)
  [
  REPEAT GEN_TAC;
  DISCH_ALL_TAC;
  GEN_TAC;
  REWRITE_TAC[REAL_ABS_BOUNDS];
  CONJ_TAC;
  SUBGOAL_THEN `(!k. ((!n. (||. ((\p. (--. (f p))) (n+k))) <=. (g (n+k)))) ==> ((--.s) - (sum(0,k) (\p. (--. (f p)))) <=. (suminf (\n. (g (n +k))))))` ASSUME_TAC;
  MATCH_MP_TAC SER_APPROX1;
  ASM_REWRITE_TAC[];
  MATCH_MP_TAC SER_NEG ;
  ASM_REWRITE_TAC[];
  MATCH_MP_TAC (REAL_ARITH (`(--. s -. (--. u) <=. x) ==> (--. x <=. (s -. u))`));
  ONCE_REWRITE_TAC[GSYM SUM_NEG];
  FIRST_X_ASSUM (fun th -> (MATCH_MP_TAC th));
  BETA_TAC;
  ASM_REWRITE_TAC[REAL_ABS_NEG];
  H_VAL2 CONJ (HYP "0") (HYP "2");
  IMP_RES_THEN MATCH_MP_TAC SER_APPROX1 ;
  GEN_TAC;
  ASM_MESON_TAC[];
  ]);;
  (* }}} *)

(* ------------------------------------------------------------------ *)
(* now for pi calculation stuff *)
(* ------------------------------------------------------------------ *)


let local_def = local_definition "trig";;


let PI_EST = prove_by_refinement(
               `!n. (1 <=| n) ==> (abs(&4 / &(8 * n + 1) -
            &2 / &(8 * n + 4) -
            &1 / &(8 * n + 5) -
            &1 / &(8 * n + 6)) <= &.622/(&.819))`,
  (* {{{ proof *)
   [
   GEN_TAC THEN DISCH_ALL_TAC;
   REWRITE_TAC[real_div];
   MATCH_MP_TAC (REWRITE_RULE[real_div] (REWRITE_RULE[REAL_RAT_REDUCE_CONV `(&.4/(&.9) +(&.2/(&.12)) + (&.1/(&.13))+ (&.1/(&.14)))`] (REAL_ARITH `(abs((&.4)*.u)<=. (&.4)/(&.9)) /\ (abs((&.2)*.v)<=. (&.2)/(&.12)) /\ (abs((&.1)*w) <=. (&.1)/(&.13)) /\ (abs((&.1)*x) <=. (&.1)/(&.14)) ==> (abs((&.4)*u -(&.2)*v - (&.1)*w - (&.1)*x) <= (&.4/(&.9) +(&.2/(&.12)) + (&.1/(&.13))+ (&.1/(&.14))))`)));
   IMP_RES_THEN ASSUME_TAC (ARITH_RULE `1 <=| n ==> (0 < n)`);
   FIRST_X_ASSUM (fun th -> ASSUME_TAC (REWRITE_RULE[GSYM REAL_OF_NUM_LT] th));
   ASSUME_TAC (prove(`(a<=.b) ==> (&.n*a <=. (&.n)*b)`,MESON_TAC[REAL_PROP_LE_LMUL;REAL_POS]));
   REWRITE_TAC[REAL_ABS_MUL;REAL_ABS_INV;prove(`||.(&.n) = (&.n)`,MESON_TAC[REAL_POS;REAL_ABS_REFL])];
   REPEAT CONJ_TAC THEN (POP_ASSUM (fun th -> MATCH_MP_TAC th)) THEN (MATCH_MP_TAC (prove(`((&.0 <. (&.n)) /\ (&.n <=. a)) ==> (inv(a)<=. (inv(&.n)))`,MESON_TAC[REAL_ABS_REFL;REAL_ABS_INV;REAL_LE_INV2]))) THEN
   REWRITE_TAC[REAL_LT;REAL_LE] THEN (H_UNDISCH_TAC (HYP"0")) THEN
   ARITH_TAC]);;
  (* }}} *)

let pi_fun = local_def `pi_fun n = inv (&.16 **. n) *.
          (&.4 / &.(8 *| n +| 1) -.
           &.2 / &.(8 *| n +| 4) -.
           &.1 / &.(8 *| n +| 5) -.
           &.1 / &.(8 *| n +| 6))`;;

let pi_bound_fun = local_def `pi_bound_fun n = if (n=0) then (&.8) else
    (((&.15)/(&.16))*(inv(&.16 **. n))) `;;

let PI_EST2 = prove_by_refinement(
    `!k. abs(pi_fun k) <=. (pi_bound_fun k)`,
  (* {{{ proof *)
   [
   GEN_TAC;
   REWRITE_TAC[pi_fun;pi_bound_fun];
   COND_CASES_TAC;
   ASM_REWRITE_TAC[];
   CONV_TAC (NUM_REDUCE_CONV);
   (CONV_TAC (REAL_RAT_REDUCE_CONV));
   CONV_TAC (RAND_CONV (REWR_CONV (REAL_ARITH `a*b = b*.a`)));
   REWRITE_TAC[REAL_ABS_MUL;REAL_ABS_INV;REAL_ABS_POW;prove(`||.(&.n) = (&.n)`,MESON_TAC[REAL_POS;REAL_ABS_REFL])];
   MATCH_MP_TAC (prove(`!x y z. (&.0 <. z /\ (y <=. x) ==> (z*y <=. (z*x)))`,MESON_TAC[REAL_LE_LMUL_EQ]));
   ASSUME_TAC (REWRITE_RULE[] (REAL_RAT_REDUCE_CONV `(&.622)/(&.819) <=. (&.15)/(&.16)`));
   IMP_RES_THEN ASSUME_TAC (ARITH_RULE `~(k=0) ==> (1<=| k)`);
   IMP_RES_THEN ASSUME_TAC (PI_EST);
   CONJ_TAC;
   SIMP_TAC[REAL_POW_LT;REAL_LT_INV;ARITH_RULE `&.0 < (&.16)`];
   ASM_MESON_TAC[REAL_LE_TRANS];
   ]);;
  (* }}} *)

let GP16 = prove_by_refinement(
  `!k. (\n. inv (&16 pow k) * inv (&16 pow n)) sums
         inv (&16 pow k) * &16 / &15`,
  (* {{{ proof *)
  [
  GEN_TAC;
  ASSUME_TAC (REWRITE_RULE[] (REAL_RAT_REDUCE_CONV `abs (&.1 / (&. 16)) <. (&.1)`));
  IMP_RES_THEN (fun th -> ASSUME_TAC (CONV_RULE REAL_RAT_REDUCE_CONV th)) GP;
  MATCH_MP_TAC SER_CMUL;
  ASM_REWRITE_TAC[GSYM REAL_POW_INV;REAL_INV_1OVER];
  ]);;
  (* }}} *)

let GP16a = prove_by_refinement(
   `!k. (0<|k) ==> (\n. (pi_bound_fun (n+k))) sums (inv(&.16 **. k))`,
  (* {{{ proof *)
   [
   GEN_TAC;
   DISCH_TAC;
   SUBGOAL_THEN `(\n. pi_bound_fun (n+k)) = (\n. ((&.15/(&.16))* (inv(&.16)**. k) *. inv(&.16 **. n)))` (fun th-> REWRITE_TAC[th]);
   MATCH_MP_TAC EQ_EXT;
   X_GEN_TAC `n:num` THEN BETA_TAC;
   REWRITE_TAC[pi_bound_fun];
   COND_CASES_TAC;
   ASM_MESON_TAC[ARITH_RULE `0<| k ==> (~(n+k = 0))`];
   REWRITE_TAC[GSYM REAL_MUL_ASSOC];
   AP_TERM_TAC;
   REWRITE_TAC[REAL_INV_MUL;REAL_POW_ADD;REAL_POW_INV;REAL_MUL_AC];
   SUBGOAL_THEN `(\n. (&.15/(&.16)) *. ((inv(&.16)**. k)*. inv(&.16 **. n))) sums ((&.15/(&.16)) *.(inv(&.16**. k)*. ((&.16)/(&.15))))` ASSUME_TAC;
   MATCH_MP_TAC SER_CMUL;
   REWRITE_TAC[REAL_POW_INV];
   ACCEPT_TAC (SPEC `k:num` GP16);
   FIRST_X_ASSUM MP_TAC;
   REWRITE_TAC[REAL_MUL_ASSOC];
   MATCH_MP_TAC (prove (`(x=y) ==> ((a sums x) ==> (a sums y))`,MESON_TAC[]));
   MATCH_MP_TAC (REAL_ARITH `(b*(a*c) = (b*(&.1))) ==> ((a*b)*c = b)`);
   AP_TERM_TAC;
   CONV_TAC (REAL_RAT_REDUCE_CONV);
   ]);;
  (* }}} *)

let PI_SER = prove_by_refinement(
  `!k. (0<|k) ==> (abs(pi - (sum(0,k) pi_fun)) <=. (inv(&.16 **. (k))))`,
  (* {{{ proof *)
   [
   GEN_TAC THEN DISCH_TAC;
   ASSUME_TAC (ONCE_REWRITE_RULE[ETA_AX] (REWRITE_RULE[GSYM pi_fun] POLYLOG_THM));
   ASSUME_TAC PI_EST2;
   IMP_RES_THEN (ASSUME_TAC) GP16a;
   IMP_RES_THEN (ASSUME_TAC) SUM_SUMMABLE;
   IMP_RES_THEN (ASSUME_TAC) SER_OFFSET_REV;
   IMP_RES_THEN (ASSUME_TAC) SUM_SUMMABLE;
   MP_TAC (SPECL [`pi`;`pi_fun`;`pi_bound_fun` ] SER_APPROX);
   ASM_REWRITE_TAC[];
   DISCH_THEN (fun th -> MP_TAC (SPEC `k:num` th));
   SUBGOAL_THEN `suminf (\n. pi_bound_fun (n + k)) = inv (&.16 **. k)` (fun th -> (MESON_TAC[th]));
   ASM_MESON_TAC[SUM_UNIQ];
   ]);;
  (* }}} *)

(* replace 3 by SUC (SUC (SUC 0)) *)
let SUC_EXPAND_CONV tm =
   let count = dest_numeral tm in
   let rec add_suc i r =
     if (i <=/ (Int 0)) then r
     else add_suc (i -/ (Int 1)) (mk_comb (`SUC`,r)) in
   let tm' = add_suc count `0` in
   REWRITE_RULE[] (ARITH_REWRITE_CONV[] (mk_eq (tm,tm')));;

let inv_twopow = prove(
  `!n. inv (&.16 **. n) = (twopow (--: (&:(4*n)))) `,
    REWRITE_TAC[TWOPOW_NEG;GSYM (NUM_RED_CONV `2 EXP 4`);
    REAL_OF_NUM_POW;EXP_MULT]);;

let PI_SERn n =
   let SUM_EXPAND_CONV =
           (ARITH_REWRITE_CONV[]) THENC
           (TOP_DEPTH_CONV SUC_EXPAND_CONV) THENC
           (REWRITE_CONV[sum]) THENC
           (ARITH_REWRITE_CONV[REAL_ADD_LID;GSYM REAL_ADD_ASSOC]) in
   let sum_thm = SUM_EXPAND_CONV (vsubst [n,`i:num`] `sum(0,i) f`) in
   let gt_thm = ARITH_RULE (vsubst [n,`i:num`] `0 <| i`) in
   ((* CONV_RULE REAL_RAT_REDUCE_CONV *)(CONV_RULE (ARITH_REWRITE_CONV[]) (BETA_RULE (REWRITE_RULE[sum_thm;pi_fun;inv_twopow] (MATCH_MP PI_SER gt_thm)))));;

(* abs(pi - u ) < e *)
let recompute_pi bprec =
   let n = (bprec /4) in
   let pi_ser = PI_SERn (mk_numeral (Int n)) in
   let _ = remove_real_constant `pi` in
   (add_real_constant pi_ser; INTERVAL_OF_TERM bprec `pi`);;

(* ------------------------------------------------------------------ *)
(* restore defaults *)
(* ------------------------------------------------------------------ *)

reduce_local_interface("trig");;