1 (* ========================================================================== *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
4 (* A bound for the number pi *)
6 (* Author: Vu Quang Thanh *)
8 (* ========================================================================== *)
12 (* ========================================================================= *)
13 (* Quick derivation of a pi approximation (could do this more nicely). *)
14 (* ========================================================================= *)
17 module Pishort = struct
20 let TAYLOR_SIN = prove
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))`,
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)
33 `real_interval[--(abs x),abs x]`; `&1`]
35 REWRITE_TAC[] THEN ANTS_TAC THENL
36 [REPEAT CONJ_TAC THENL
37 [REWRITE_TAC[is_realinterval; IN_REAL_INTERVAL] THEN REAL_ARITH_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]]);;
52 let PI_LOWERBOUND_WEAK = prove
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);;
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);;
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
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);;
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);;
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
113 [W(MP_TAC o PART_MATCH (lhand o rand o lhand) (SPEC `12` TAYLOR_SIN) o
115 W(MP_TAC o PART_MATCH (lhand o rand o lhand) (SPEC `12` TAYLOR_SIN) o
117 REWRITE_TAC[TOP_DEPTH_CONV num_CONV `12`] THEN
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
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]]);;