legacy/oldtame/pishort.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* A bound for the number pi *)
   5 (* Chapter: Tame                                                           *)
   6 (* Author:  Vu Quang Thanh                                                  *)
   7 (* Date: 2010-02-13                                                          *)
   8 (* ========================================================================== *)
   9
  10
  11
  12 (* ========================================================================= *)
  13 (* Quick derivation of a pi approximation (could do this more nicely).       *)
  14 (* ========================================================================= *)
  15
  16
  17 module Pishort  = struct
  18
  19
  20 let TAYLOR_SIN = prove
  21  (`!n x. abs(sin x -
  22              sum(0..n) (\i. (if i MOD 4 = 0 then &0
  23                              else if i MOD 4 = 1 then &1
  24                              else if i MOD 4 = 2 then &0
  25                              else -- &1) * x pow i / &(FACT i)))
  26          <= abs x pow (n + 1) / &(FACT (n + 1))`,
  27   REPEAT STRIP_TAC THEN
  28   MP_TAC(ISPECL [`\n. if n MOD 4 = 0 then sin
  29                       else if n MOD 4 = 1 then cos
  30                       else if n MOD 4 = 2 then \x. --(sin x)
  31                       else \x. --(cos x)`;
  32                  `n:num`;
  33                  `real_interval[--(abs x),abs x]`; `&1`]
  34         REAL_TAYLOR) THEN
  35   REWRITE_TAC[] THEN ANTS_TAC THENL
  36    [REPEAT CONJ_TAC THENL
  37      [REWRITE_TAC[is_realinterval; IN_REAL_INTERVAL] THEN REAL_ARITH_TAC;
  38       ALL_TAC;
  39       MESON_TAC[REAL_ABS_NEG; SIN_BOUND; COS_BOUND]] THEN
  40     ONCE_REWRITE_TAC[GSYM(MATCH_MP MOD_ADD_MOD (ARITH_RULE `~(4 = 0)`))] THEN
  41     REPEAT STRIP_TAC THEN REPEAT_TCL DISJ_CASES_THEN SUBST1_TAC (ARITH_RULE
  42      `i MOD 4 = 0 \/ i MOD 4 = 1 \/ i MOD 4 = 2 \/ i MOD 4 = 3`) THEN
  43     CONV_TAC NUM_REDUCE_CONV THEN
  44     GEN_REWRITE_TAC (RATOR_CONV o LAND_CONV) [GSYM ETA_AX] THEN
  45     REWRITE_TAC[] THEN REAL_DIFF_TAC THEN REAL_ARITH_TAC;
  46     CONV_TAC NUM_REDUCE_CONV THEN REWRITE_TAC[COND_RATOR] THEN
  47     DISCH_THEN(MP_TAC o SPECL [`&0:real`; `x:real`]) THEN
  48     REWRITE_TAC[IN_REAL_INTERVAL] THEN ANTS_TAC THENL
  49      [REAL_ARITH_TAC; ALL_TAC] THEN
  50     REWRITE_TAC[REAL_SUB_RZERO; COS_0; SIN_0; REAL_NEG_0; REAL_MUL_LID]]);;
  51
  52 let PI_LOWERBOUND_WEAK = prove
  53  (`&627 / &256 <= pi`,
  54   SUBGOAL_THEN
  55    `!x. &0 < x /\ x < &627 / &256 ==> &0 < sin x` (MP_TAC o SPEC `pi`)
  56   THENL [ALL_TAC; SIMP_TAC[SIN_PI; REAL_LT_REFL; PI_POS; REAL_NOT_LT]] THEN
  57   REPEAT STRIP_TAC THEN MP_TAC(ISPECL [`2`; `x:real`] TAYLOR_SIN) THEN
  58   REWRITE_TAC[num_CONV `2`; num_CONV `1`; SUM_CLAUSES_NUMSEG] THEN
  59   CONV_TAC NUM_REDUCE_CONV THEN
  60   REWRITE_TAC[REAL_MUL_LZERO; REAL_ADD_LID; REAL_ADD_RID; REAL_MUL_LID] THEN
  61   ASM_SIMP_TAC[REAL_ARITH `&0 < x ==> abs x = x`] THEN MATCH_MP_TAC(REAL_ARITH
  62    `e + d < a ==> abs(s - a) <= d ==> e < s`) THEN
  63   REWRITE_TAC[REAL_ARITH
  64    `&0 + x pow 3 / &6 < x pow 1 / &1 <=> x * x pow 2 < x * &6`] THEN
  65   ASM_SIMP_TAC[REAL_LT_LMUL_EQ] THEN
  66   MATCH_MP_TAC REAL_LT_TRANS THEN EXISTS_TAC `(&627 / &256) pow 2` THEN
  67   ASM_SIMP_TAC[REAL_POW_LT2; ARITH_EQ; REAL_LT_IMP_LE] THEN
  68   CONV_TAC REAL_RAT_REDUCE_CONV);;
  69
  70 let COS_TREBLE_COS = prove
  71  (`!x. cos(&3 * x) = &4 * cos(x) pow 3 - &3 * cos x`,
  72   GEN_TAC THEN REWRITE_TAC[COS_ADD; REAL_ARITH `&3 * x = &2 * x + x`] THEN
  73   REWRITE_TAC[SIN_DOUBLE; COS_DOUBLE_COS] THEN
  74   MP_TAC(SPEC `x:real` SIN_CIRCLE) THEN CONV_TAC REAL_RING);;
  75
  76 let COS_PI6 = prove
  77  (`cos(pi / &6) = sqrt(&3) / &2`,
  78   MP_TAC(ISPEC `pi / &6` COS_TREBLE_COS) THEN
  79   REWRITE_TAC[REAL_ARITH `&3 * x / &6 = x / &2`; COS_PI2] THEN
  80   REWRITE_TAC[REAL_RING `&0 = &4 * c pow 3 - &3 * c <=>
  81                          c = &0 \/ (&2 * c) pow 2 = &3`] THEN
  82   SUBGOAL_THEN `&0 < cos(pi / &6)` ASSUME_TAC THENL
  83    [MATCH_MP_TAC COS_POS_PI THEN MP_TAC PI_POS THEN REAL_ARITH_TAC;
  84     DISCH_THEN(DISJ_CASES_THEN MP_TAC) THENL
  85      [ASM_MESON_TAC[REAL_LT_REFL]; ALL_TAC] THEN
  86     DISCH_THEN(MP_TAC o AP_TERM `sqrt`) THEN
  87     ASM_SIMP_TAC[POW_2_SQRT; REAL_LE_MUL; REAL_LT_IMP_LE; REAL_POS] THEN
  88     REAL_ARITH_TAC]);;
  89
  90 let SIN_PI6 = prove
  91  (`sin(pi / &6) = &1 / &2`,
  92   MP_TAC(SPEC `pi / &6` SIN_CIRCLE) THEN REWRITE_TAC[COS_PI6] THEN
  93   SIMP_TAC[REAL_POW_DIV; SQRT_POW_2; REAL_POS] THEN MATCH_MP_TAC(REAL_FIELD
  94    `~(s + &1 / &2 = &0) ==> s pow 2 + &3 / &2 pow 2 = &1 ==> s = &1 / &2`) THEN
  95   MATCH_MP_TAC(REAL_ARITH `&0 < x ==> ~(x + &1 / &2 = &0)`) THEN
  96   MATCH_MP_TAC SIN_POS_PI THEN MP_TAC PI_POS THEN REAL_ARITH_TAC);;
  97
  98 let SIN_PI6_STRADDLE = prove
  99  (`!a b. &0 <= a /\ a <= b /\ b <= &7 /\
 100          sin(a / &6) <= &1 / &2 /\ &1 / &2 <= sin(b / &6)
 101          ==> a <= pi /\ pi <= b`,
 102   REPEAT GEN_TAC THEN STRIP_TAC THEN
 103   MP_TAC(SPECL [`pi / &6`; `b / &6`] SIN_MONO_LE_EQ) THEN
 104   MP_TAC(SPECL [`a / &6`; `pi / &6`] SIN_MONO_LE_EQ) THEN
 105   ASM_REWRITE_TAC[SIN_PI6] THEN
 106   MP_TAC PI_LOWERBOUND_WEAK THEN ASM_REAL_ARITH_TAC);;
 107
 108 let PI_APPROX = prove
 109  (`abs(pi - &13493037705 / &4294967296) <= inv(&2 pow 32)`,
 110   REWRITE_TAC[REAL_ARITH `abs(x - a) <= e <=> a - e <= x /\ x <= a + e`] THEN
 111   MATCH_MP_TAC SIN_PI6_STRADDLE THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
 112   CONJ_TAC THENL
 113    [W(MP_TAC o PART_MATCH (lhand o rand o lhand) (SPEC `12` TAYLOR_SIN) o
 114         lhand o snd);
 115     W(MP_TAC o PART_MATCH (lhand o rand o lhand) (SPEC `12` TAYLOR_SIN) o
 116         rand o snd)] THEN
 117   REWRITE_TAC[TOP_DEPTH_CONV num_CONV `12`] THEN
 118   REPLICATE_TAC 13
 119    (ONCE_REWRITE_TAC[SUM_CLAUSES_NUMSEG] THEN REWRITE_TAC[LE_0]) THEN
 120   CONV_TAC NUM_REDUCE_CONV THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
 121   REAL_ARITH_TAC);;
 122
 123 let bound_for_pi = prove (`!n. &n * (&852 / &1000) <= &2 * pi ==> n <= 7`, REPEAT STRIP_TAC THEN ASSUME_TAC (PI_APPROX) THEN SUBGOAL_THEN `abs (pi - &13493037705 / &4294967296) < &1 / &128` ASSUME_TAC THENL[ASM_REAL_ARITH_TAC; MP_TAC (SPECL [`pi`; `&13493037705 / &4294967296`; `&1 / &128`] REAL_ABS_BOUND) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN SUBGOAL_THEN `&n < &8` ASSUME_TAC THENL[ASM_REAL_ARITH_TAC ; MP_TAC (SPECL [`n:num`; `8`] REAL_OF_NUM_LT) THEN ASM_REWRITE_TAC[] THEN ARITH_TAC]]);;
 124
 125
 126
 127 end;;