text_formalization/tame/ArcProperties.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Author: Alexey Solovyev                                                    *)
   5 (* Date: 2010-06-17                                                           *)
   6 (* ===========================================================================*)
   7
   8
   9 (**********************************************)
  10 (* Properties of the function arc (arclegnth) *)
  11 (**********************************************)
  12
  13
  14 (* Some auxiliary results *)
  15 flyspeck_needs "trigonometry/trigonometry.hl";;
  16 (* lmfun, h0 definitions *)
  17 flyspeck_needs "packing/pack_defs.hl";;
  18
  19
  20 module Arc_properties = struct
  21
  22
  23 let REMOVE_ASSUM = POP_ASSUM (fun th -> ALL_TAC);;
  24
  25
  26 (* Some general results *)
  27
  28 (* Limit is a local notion *)
  29 let REALLIM_ATREAL_LOCAL = prove(`!f g x y. (g ---> y) (atreal x) /\
  30                                (?s. real_open s /\ x IN s /\ (!y. y IN s ==> f y = g y))
  31                                ==> (f ---> y) (atreal x)`,
  32    REWRITE_TAC[REALLIM_ATREAL; real_open] THEN
  33      REPEAT STRIP_TAC THEN
  34      POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN
  35      FIRST_X_ASSUM (MP_TAC o SPEC `x:real`) THEN
  36      ASM_REWRITE_TAC[] THEN
  37      STRIP_TAC THEN POP_ASSUM MP_TAC THEN
  38      FIRST_X_ASSUM (MP_TAC o SPEC `e:real`) THEN
  39      REPEAT STRIP_TAC THEN
  40      FIRST_X_ASSUM (MP_TAC o check (is_imp o concl)) THEN
  41      ASM_REWRITE_TAC[] THEN
  42      STRIP_TAC THEN
  43      EXISTS_TAC `min e' d` THEN
  44      CONJ_TAC THENL
  45      [
  46        REWRITE_TAC[real_min] THEN
  47          COND_CASES_TAC THEN ASM_REWRITE_TAC[];
  48        ALL_TAC
  49      ] THEN
  50      GEN_TAC THEN
  51      STRIP_TAC THEN
  52      SUBGOAL_THEN `(f:real->real) x' = (g:real->real) x'` (fun th -> REWRITE_TAC[th]) THENL
  53      [
  54        FIRST_X_ASSUM MATCH_MP_TAC THEN
  55          FIRST_X_ASSUM MATCH_MP_TAC THEN
  56          MATCH_MP_TAC REAL_LTE_TRANS THEN
  57          EXISTS_TAC `min e' d` THEN
  58          ASM_REWRITE_TAC[REAL_MIN_MIN];
  59        ALL_TAC;
  60      ] THEN
  61      FIRST_X_ASSUM MATCH_MP_TAC THEN
  62      ASM_REWRITE_TAC[] THEN
  63      MATCH_MP_TAC REAL_LTE_TRANS THEN
  64      EXISTS_TAC `min e' d` THEN
  65      ASM_REWRITE_TAC[REAL_MIN_MIN]);;
  66
  67
  68
  69
  70 (* Derivative is a local notion *)
  71 let HAS_REAL_DERIVATIVE_LOCAL = prove(`!f g x g'x. (g has_real_derivative g'x) (atreal x)
  72                                  /\ (?s. real_open s /\ x IN s /\ (!y. y IN s ==> f y = g y))
  73                                  ==> (f has_real_derivative g'x) (atreal x)`,
  74    REWRITE_TAC[HAS_REAL_DERIVATIVE_ATREAL] THEN
  75      REPEAT STRIP_TAC THEN
  76      MATCH_MP_TAC REALLIM_ATREAL_LOCAL THEN
  77      EXISTS_TAC `\y. (g y - (g:real->real) x) / (y - x)` THEN
  78      ASM_REWRITE_TAC[] THEN
  79      EXISTS_TAC `s:real->bool` THEN
  80      ASM_REWRITE_TAC[] THEN
  81      REPEAT STRIP_TAC THEN
  82      FIRST_ASSUM (MP_TAC o SPEC `x:real`) THEN
  83      FIRST_X_ASSUM (MP_TAC o SPEC `y:real`) THEN
  84      ASM_SIMP_TAC[]);;
  85
  86
  87
  88
  89 let REAL_LT_ONE_LDIV = prove(`!a b. &0 < b /\ a < b ==> a / b < &1`,
  90         REPEAT STRIP_TAC THEN
  91           ASM_SIMP_TAC[REAL_FIELD `&0 < b ==> (a / b < &1 <=> &0 < (b - a) / b)`] THEN
  92           ASM_SIMP_TAC[Trigonometry2.REAL_LT_DIV_0] THEN
  93           POP_ASSUM MP_TAC THEN REAL_ARITH_TAC);;
  94
  95
  96
  97 (****************************************************************)
  98
  99
 100 (* The derivative of arc (x, b, 2) *)
 101 let arc_derivative =
 102   let der0 = REAL_DIFF_CONV `((\x. acs ((x * x + b * b - &2 * &2) / (&2 * x * b))) has_real_derivative f) (atreal x)` in
 103   let der1 = REWRITE_RULE [REAL_ADD_RID; REAL_SUB_RZERO; REAL_MUL_RID; REAL_MUL_LID] der0 in
 104   let der2 = REWRITE_RULE [IMP_IMP] (DISCH_ALL der1) in
 105   let der_tm = (rand o rator) (concl der1) in
 106   let concl0 = list_mk_comb (`(has_real_derivative)`, [`\x. arclength x b (&2)`; der_tm; `atreal x within real_interval [&2,#2.52]`]) in
 107   let goal0 = list_mk_forall ([`x:real`; `b:real`], (mk_imp (`(&2 <= x /\ x <= #2.52) /\ (&2 <= b /\ b <= #2.52)`, concl0))) in
 108   prove(goal0,
 109    REPEAT STRIP_TAC THEN
 110      MATCH_MP_TAC HAS_REAL_DERIVATIVE_ATREAL_WITHIN THEN
 111      MATCH_MP_TAC HAS_REAL_DERIVATIVE_LOCAL THEN
 112      EXISTS_TAC `(\x. acs ((x * x + b * b - &2 * &2) / (&2 * x * b)))` THEN
 113      CONJ_TAC THENL
 114      [
 115        MATCH_MP_TAC der2 THEN
 116          CONJ_TAC THENL
 117          [
 118            MATCH_MP_TAC (REAL_ARITH `&0 <= a /\ a < &1 ==> abs a < &1`) THEN
 119              CONJ_TAC THENL
 120              [
 121                MATCH_MP_TAC REAL_LE_DIV THEN
 122                  SUBGOAL_THEN `&2 * &2 <= x * x /\ &2 * &2 <= b * b` ASSUME_TAC THENL
 123                  [
 124                    REWRITE_TAC[GSYM REAL_POW_2] THEN
 125                      CONJ_TAC THEN MATCH_MP_TAC REAL_POW_LE2 THEN ASM_REWRITE_TAC[REAL_ARITH `&0 <= &2`];
 126                    ALL_TAC
 127                  ] THEN
 128                  CONJ_TAC THENL
 129                  [
 130                    POP_ASSUM MP_TAC THEN
 131                      REAL_ARITH_TAC;
 132                    MATCH_MP_TAC REAL_LE_MUL THEN
 133                      REWRITE_TAC[REAL_ARITH `&0 <= &2`] THEN
 134                      MATCH_MP_TAC REAL_LE_MUL THEN
 135                      ASM_SIMP_TAC[REAL_ARITH `&2 <= x ==> &0 <= x`]
 136                  ];
 137                ALL_TAC
 138              ] THEN
 139
 140              MATCH_MP_TAC REAL_LT_ONE_LDIV THEN
 141              CONJ_TAC THENL
 142              [
 143                MATCH_MP_TAC REAL_LT_MUL THEN
 144                  REWRITE_TAC[REAL_ARITH `&0 < &2`] THEN
 145                  MATCH_MP_TAC REAL_LT_MUL THEN
 146                  ASM_SIMP_TAC[REAL_ARITH `&2 <= x ==> &0 < x`];
 147                ALL_TAC
 148              ] THEN
 149
 150              REWRITE_TAC[REAL_ARITH `x * x + b * b - &2 * &2 < &2 * x * b <=> (x - b) * (x - b) < &2 * &2`] THEN
 151              REWRITE_TAC[GSYM REAL_POW_2] THEN
 152              REWRITE_TAC[GSYM REAL_LT_SQUARE_ABS] THEN
 153              REPEAT (POP_ASSUM MP_TAC) THEN
 154              REAL_ARITH_TAC;
 155            ALL_TAC
 156          ] THEN
 157          REWRITE_TAC[Trigonometry2.NOT_MUL_EQ0_EQ] THEN
 158          REPEAT (POP_ASSUM MP_TAC) THEN
 159          REAL_ARITH_TAC;
 160        ALL_TAC
 161      ] THEN
 162
 163      EXISTS_TAC `real_interval (#1.9,#2.6)` THEN
 164      REWRITE_TAC[REAL_OPEN_REAL_INTERVAL; IN_REAL_INTERVAL] THEN
 165      CONJ_TAC THENL
 166      [
 167        REPEAT (POP_ASSUM MP_TAC) THEN
 168          REAL_ARITH_TAC;
 169        ALL_TAC
 170      ] THEN
 171      REPEAT STRIP_TAC THEN
 172      MATCH_MP_TAC Trigonometry1.ACS_ARCLENGTH THEN
 173      REPEAT (POP_ASSUM MP_TAC) THEN
 174      REAL_ARITH_TAC);;
 175
 176
 177
 178 (**************************************************************)
 179
 180
 181
 182 (* Numerical approximations for cos and acos *)
 183
 184
 185 let COS_EQ_NEG_SIN = prove(`!x. cos (x + pi / &2) = --sin x`,
 186      REWRITE_TAC[COS_SIN; REAL_ARITH `a - (b + a) = --b`; SIN_NEG]);;
 187
 188
 189
 190
 191 let COS_DERIVATIVES = prove(`!x n. ((\x. cos (x + &n * pi / &2)) has_real_derivative cos (x + &(n + 1) * pi / &2)) (atreal x)`,
 192    REPEAT GEN_TAC THEN REWRITE_TAC[] THEN
 193      MP_TAC (REAL_DIFF_CONV `((\x. cos (x + &n * pi / &2)) has_real_derivative f) (atreal x)`) THEN
 194      SUBGOAL_THEN `(&1 + &0) * --sin (x + &n * pi / &2) = cos (x + &(n + 1) * pi / &2)` (fun th -> REWRITE_TAC[th]) THEN
 195      REWRITE_TAC[REAL_ARITH `(&1 + &0) * --a = --a`] THEN
 196      REWRITE_TAC[GSYM REAL_OF_NUM_ADD] THEN
 197      REWRITE_TAC[REAL_ARITH `x + (a + &1) * t = (x + a * t) + t`] THEN
 198      REWRITE_TAC[COS_EQ_NEG_SIN]);;
 199
 200
 201
 202
 203 let REAL_TAYLOR_COS_RAW = prove(`!x n. abs (cos x - sum (0..n) (\k. if (EVEN k) then ((-- &1) pow (k DIV 2) * x pow k) / &(FACT k) else &0)) <=
 204                                   abs x pow (n + 1) / &(FACT (n + 1))`,
 205    REPEAT GEN_TAC THEN
 206      MP_TAC (SPECL [`(\i x. cos (x + &i * pi / &2))`; `n:num`; `UNIV:real->bool`; `&1`] REAL_TAYLOR) THEN
 207      ANTS_TAC THENL
 208      [
 209        REWRITE_TAC[is_realinterval; IN_UNIV; WITHINREAL_UNIV; COS_DERIVATIVES; COS_BOUND];
 210        ALL_TAC
 211      ] THEN
 212      REWRITE_TAC[IN_UNIV] THEN
 213      DISCH_THEN (MP_TAC o SPECL [`&0`; `x:real`]) THEN
 214      REWRITE_TAC[REAL_MUL_LZERO; REAL_ADD_RID; REAL_ADD_LID; REAL_SUB_RZERO; REAL_MUL_LID] THEN
 215      SUBGOAL_THEN `!i. cos (&i * pi / &2) * x pow i / &(FACT i) = if EVEN i then (-- &1 pow (i DIV 2) * x pow i) / &(FACT i) else &0` (fun th -> SIMP_TAC[th]) THEN
 216      GEN_TAC THEN
 217      ASM_CASES_TAC `EVEN i` THEN ASM_REWRITE_TAC[] THENL
 218      [
 219        POP_ASSUM MP_TAC THEN
 220          REWRITE_TAC[EVEN_EXISTS] THEN
 221          STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
 222          SUBGOAL_THEN `(2 * m) DIV 2 = m` (fun th -> REWRITE_TAC[th]) THENL
 223          [
 224            MATCH_MP_TAC DIV_MULT THEN
 225              ARITH_TAC;
 226            ALL_TAC
 227          ] THEN
 228          REWRITE_TAC[GSYM REAL_OF_NUM_MUL] THEN
 229          REWRITE_TAC[REAL_ARITH `(&2 * a) * b / &2 = a * b`] THEN
 230          REWRITE_TAC[COS_NPI] THEN
 231          REAL_ARITH_TAC;
 232        ALL_TAC
 233      ] THEN
 234      SUBGOAL_THEN `cos (&i * pi / &2) = &0` (fun th -> REWRITE_TAC[th]) THENL
 235      [
 236        REWRITE_TAC[COS_ZERO] THEN
 237          DISJ1_TAC THEN EXISTS_TAC `i:num` THEN
 238          ASM_REWRITE_TAC[];
 239        ALL_TAC
 240      ] THEN
 241      REWRITE_TAC[REAL_MUL_LZERO]);;
 242
 243
 244 let SUM_PAIR_0 = prove(`!f n. sum (0..2 * n + 1) f = sum(0..n) (\i. f (2 * i) + f (2 * i + 1))`,
 245    REPEAT GEN_TAC THEN
 246      MP_TAC (SPECL [`f:num->real`; `0`; `n:num`] SUM_PAIR) THEN
 247      REWRITE_TAC[ARITH_RULE `2 * 0 = 0`]);;
 248
 249
 250 let REAL_TAYLOR_COS = prove(`!x n. abs (cos x - sum (0..n) (\i. (-- &1) pow i * x pow (2 * i) / &(FACT (2 * i)))) <= abs x pow (2*n + 2) / &(FACT (2*n + 2))`,
 251    REPEAT GEN_TAC THEN
 252      MP_TAC (SPECL [`x:real`; `2 * n + 1`] REAL_TAYLOR_COS_RAW) THEN
 253      REWRITE_TAC[SUM_PAIR_0; EVEN_DOUBLE; ARITH_RULE `(2 * n + 1) + 1 = 2 *n + 2`] THEN
 254      SUBGOAL_THEN `!i. ~(EVEN (2 * i + 1))` MP_TAC THENL
 255      [
 256        GEN_TAC THEN REWRITE_TAC[NOT_EVEN] THEN
 257          REWRITE_TAC[ARITH_ODD; ODD_ADD; ODD_MULT];
 258        ALL_TAC
 259      ] THEN
 260      DISCH_THEN (fun th -> SIMP_TAC[th]) THEN
 261      SUBGOAL_THEN `!i. (2 * i) DIV 2 = i` MP_TAC THENL
 262      [
 263        GEN_TAC THEN
 264          MATCH_MP_TAC DIV_MULT THEN
 265          REWRITE_TAC[ARITH];
 266        ALL_TAC
 267      ] THEN
 268      DISCH_THEN (fun th -> REWRITE_TAC[th; REAL_ADD_RID]) THEN
 269      REWRITE_TAC[REAL_ARITH `(a * b) / c = a * b / c`]);;
 270
 271
 272
 273
 274
 275 let gen_sum_thm n =
 276   let SUM_lemma n =
 277     let tm = list_mk_comb (`sum:(num->bool)->(num->real)->real`, [mk_comb (`(..) 0`, mk_small_numeral n); `f:num->real`]) in
 278     let suc_th = REWRITE_RULE[EQ_CLAUSES] (REWRITE_CONV[ARITH] (mk_eq (mk_small_numeral n, mk_comb (`SUC`, mk_small_numeral (n - 1))))) in
 279     let th1 = REWRITE_CONV[suc_th] tm in
 280       REWRITE_RULE[SUM_CLAUSES_NUMSEG; ARITH] th1 in
 281   let rec rewriter th n =
 282     if n > 0 then
 283       rewriter (REWRITE_RULE[SUM_lemma n; GSYM REAL_ADD_ASSOC] th) (n - 1)
 284     else
 285       th in
 286     GEN_ALL (rewriter (SUM_lemma n) (n - 1));;
 287
 288
 289
 290 (* Evaluates cos at a given point using n terms from the cosine Taylor series *)
 291 let cos_eval x n =
 292   let th1 = (SPECL [x; mk_small_numeral n] REAL_TAYLOR_COS) in
 293   let th2 = REWRITE_RULE[gen_sum_thm n] th1 in
 294   let th4 = CONV_RULE (NUM_REDUCE_CONV) th2 in
 295   let th5 = CONV_RULE (DEPTH_CONV REAL_INT_POW_CONV) th4 in
 296     CONV_RULE (REAL_RAT_REDUCE_CONV) th5;;
 297
 298
 299
 300
 301 (************************************************************************)
 302
 303
 304
 305 (***************************)
 306 (* Properties of arc a b c *)
 307 (***************************)
 308
 309
 310 (* arc a b 2 <= arc a b c *)
 311 let arc_lemma1 = prove(`!a b c. &2 <= a /\ a <= #2.52 /\
 312                        &2 <= b /\ b <= #2.52 /\
 313                        &2 <= c /\ c <= #2.52
 314                        ==> arclength a b (&2) <= arclength a b c`,
 315    REPEAT STRIP_TAC THEN
 316      SUBGOAL_THEN `arclength a b (&2) = acs ((a * a + b * b - &2 * &2) / (&2 * a * b))` (fun th -> REWRITE_TAC[th]) THENL
 317      [
 318        MATCH_MP_TAC Trigonometry1.ACS_ARCLENGTH THEN
 319          REPEAT (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC;
 320        ALL_TAC
 321      ] THEN
 322      SUBGOAL_THEN `arclength a b c = acs ((a * a + b * b - c * c) / (&2 * a * b))` (fun th -> REWRITE_TAC[th]) THENL
 323      [
 324        MATCH_MP_TAC Trigonometry1.ACS_ARCLENGTH THEN
 325          REPEAT (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC;
 326        ALL_TAC
 327      ] THEN
 328      MATCH_MP_TAC ACS_MONO_LE THEN
 329
 330      ABBREV_TAC `a2:real = a * a` THEN
 331      ABBREV_TAC `b2:real = b * b` THEN
 332      ABBREV_TAC `c2:real = c * c` THEN
 333      ABBREV_TAC `ab2:real = &2 * a * b` THEN
 334
 335      SUBGOAL_THEN `&4 <= a2 /\ a2 <= #6.3504 /\ &4 <= b2 /\ b2 <= #6.3504 /\ &4 <= c2 /\ c2 <= #6.3504` ASSUME_TAC THENL
 336      [
 337        REMOVE_ASSUM THEN
 338          REPLICATE_TAC 3 (POP_ASSUM (fun th -> REWRITE_TAC[SYM th])) THEN
 339          REWRITE_TAC[REAL_ARITH `&4 = &2 * &2`; REAL_ARITH `#6.3504 = #2.52 * #2.52`] THEN
 340          REWRITE_TAC[GSYM REAL_POW_2; GSYM REAL_LE_SQUARE_ABS] THEN
 341          REPEAT (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC;
 342        ALL_TAC
 343      ] THEN
 344
 345      SUBGOAL_THEN `&8 <= ab2 /\ ab2 <= #12.7008` ASSUME_TAC THENL
 346      [
 347        EXPAND_TAC "ab2" THEN
 348          REWRITE_TAC[REAL_ARITH `&8 = &2 * &2 * &2`; REAL_ARITH `#12.7008 = &2 * #2.52 * #2.52`] THEN
 349          CONJ_TAC THEN MATCH_MP_TAC REAL_LE_LMUL THEN REWRITE_TAC[REAL_ARITH `&0 <= &2`] THENL
 350          [
 351            MATCH_MP_TAC REAL_LE_MUL2 THEN
 352              ASM_REWRITE_TAC[REAL_ARITH `&0 <= &2`];
 353            MATCH_MP_TAC REAL_LE_MUL2 THEN
 354              ASM_SIMP_TAC[REAL_ARITH `&2 <= a ==> &0 <= a`]
 355          ];
 356        ALL_TAC
 357      ] THEN
 358
 359      SUBGOAL_THEN `&0 < ab2` ASSUME_TAC THENL
 360      [
 361        MATCH_MP_TAC REAL_LTE_TRANS THEN
 362          EXISTS_TAC `&8` THEN ASM_REWRITE_TAC[REAL_ARITH `&0 < &8`];
 363        ALL_TAC
 364      ] THEN
 365
 366      REPEAT CONJ_TAC THENL
 367      [
 368        MATCH_MP_TAC REAL_LE_TRANS THEN
 369          EXISTS_TAC `&0` THEN
 370          REWRITE_TAC[REAL_ARITH `-- &1 <= &0`] THEN
 371          MATCH_MP_TAC REAL_LE_DIV THEN
 372          REPLICATE_TAC 3 (POP_ASSUM MP_TAC) THEN
 373          REAL_ARITH_TAC;
 374
 375        ASM_SIMP_TAC[REAL_LE_DIV2_EQ] THEN
 376          REMOVE_ASSUM THEN REMOVE_ASSUM THEN POP_ASSUM MP_TAC THEN
 377          REAL_ARITH_TAC;
 378
 379        MATCH_MP_TAC Trigonometry2.REAL_LE_LDIV THEN
 380          ASM_REWRITE_TAC[] THEN
 381
 382          MAP_EVERY EXPAND_TAC ["a2"; "b2"; "ab2"] THEN
 383          ONCE_REWRITE_TAC[REAL_ARITH `a + b - c <= d <=> a + b - d <= c`] THEN
 384          REWRITE_TAC[REAL_RING `a * a + b * b - &2 * a * b = (a - b) * (a - b)`] THEN
 385          REWRITE_TAC[GSYM REAL_POW_2; GSYM REAL_LE_SQUARE_ABS] THEN
 386          REPLICATE_TAC 9 REMOVE_ASSUM THEN
 387          REPEAT (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC
 388      ]);;
 389
 390
 391 (*************************************************************)
 392
 393
 394 (* arc a b c = arc b a c *)
 395 let ups_x_sym = prove(`!a b c. ups_x a b c = ups_x b a c`,
 396    REWRITE_TAC[Sphere.ups_x] THEN REAL_ARITH_TAC);;
 397
 398
 399 let arc_sym = prove(`!a b c. arclength a b c = arclength b a c`,
 400    REWRITE_TAC[Sphere.arclength; ups_x_sym] THEN
 401      REWRITE_TAC[REAL_ARITH `c - a - b = c - b - a`]);;
 402
 403
 404
 405 (*************************************************************)
 406
 407 (* arc x b 2 is concave *)
 408
 409
 410 (* A corrected version of the theorem from realanalysis.ml *)
 411 let REAL_CONVEX_ON_SECOND_DERIVATIVE = prove
 412  (`!f f' f'' s.
 413         is_realinterval s /\ ~(?a. s = {a}) /\
 414         (!x. x IN s ==> (f has_real_derivative f'(x)) (atreal x within s)) /\
 415         (!x. x IN s ==> (f' has_real_derivative f''(x)) (atreal x within s))
 416         ==> (f real_convex_on s <=> !x. x IN s ==> &0 <= f''(x))`,
 417   REPEAT STRIP_TAC THEN MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC
 418    `!x y. x IN s /\ y IN s /\ x <= y ==> (f':real->real)(x) <= f'(y)` THEN
 419   CONJ_TAC THENL
 420    [MATCH_MP_TAC REAL_CONVEX_ON_DERIVATIVE_INCREASING;
 421     CONV_TAC SYM_CONV THEN MATCH_MP_TAC HAS_REAL_DERIVATIVE_INCREASING] THEN
 422   ASM_REWRITE_TAC[]);;
 423
 424
 425
 426 (* arc is concave (-arc is convex) *)
 427
 428 let arc_concave = prove(`!b. &2 <= b /\ b <= #2.52 ==> (\x. -- arclength x b (&2)) real_convex_on (real_interval [&2, #2.52])`,
 429    REPEAT STRIP_TAC THEN
 430      MP_TAC (SPECL [`\x. --arclength x b (&2)`;
 431                     `\x. (x * x - (b * b - &4)) / x * inv (sqrt (&4 * (x * x) * (b * b) - (x * x + b * b - &4) pow 2))`;
 432                     `\x. inv (sqrt (&4 * (x * x) * (b * b) - (x * x + b * b - &4) pow 2)) * ((x * x + (b * b - &4)) / (x * x) - ((&2 * b * b - &2 * x * x + &8) * (x * x - (b * b - &4))) / (&4 * (x * x) * (b * b) - (x * x + b * b - &4) pow 2))`;
 433                     `real_interval [&2,#2.52]`
 434                    ] REAL_CONVEX_ON_SECOND_DERIVATIVE) THEN
 435      ANTS_TAC THENL
 436      [
 437        REWRITE_TAC[IS_REALINTERVAL_INTERVAL] THEN
 438          CONJ_TAC THENL
 439          [
 440            REWRITE_TAC[NOT_EXISTS_THM] THEN GEN_TAC THEN
 441              DISCH_TAC THEN
 442              SUBGOAL_THEN `&2 = a /\ #2.52 = a` MP_TAC THENL
 443              [
 444                REWRITE_TAC[GSYM IN_SING] THEN
 445                  POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN
 446                  REWRITE_TAC[IN_REAL_INTERVAL] THEN
 447                  REAL_ARITH_TAC;
 448                ALL_TAC
 449              ] THEN
 450              REAL_ARITH_TAC;
 451            ALL_TAC
 452          ] THEN
 453
 454          CONJ_TAC THENL
 455          [
 456            REWRITE_TAC[IN_REAL_INTERVAL] THEN
 457              GEN_TAC THEN DISCH_TAC THEN
 458              REWRITE_TAC[REAL_ARITH `a * inv(b) = --(a * --inv(b))`] THEN
 459              MATCH_MP_TAC HAS_REAL_DERIVATIVE_NEG THEN
 460              MP_TAC (SPEC_ALL arc_derivative) THEN
 461              ASM_REWRITE_TAC[] THEN
 462              REWRITE_TAC[REAL_ARITH `(x + x) * &2 * x * b - (x * x + b * b - &2 * &2) * &2 * b = &2 * b * (x * x - (b * b - &4))`] THEN
 463              SUBGOAL_THEN `&0 < &2 * x * b` ASSUME_TAC THENL
 464              [
 465                MATCH_MP_TAC REAL_LT_MUL THEN
 466                  REWRITE_TAC[REAL_ARITH `&0 < &2`] THEN
 467                  MATCH_MP_TAC REAL_LT_MUL THEN
 468                  ASM_SIMP_TAC[REAL_ARITH `&2 <= x ==> &0 < x`];
 469                ALL_TAC
 470              ] THEN
 471
 472              SUBGOAL_THEN `(&2 * b * (x * x - (b * b - &4))) / (&2 * x * b) pow 2 = (x * x - (b * b - &4)) / x * inv(&2 * x * b)` (fun th -> REWRITE_TAC[th]) THENL
 473              [
 474                POP_ASSUM MP_TAC THEN
 475                  CONV_TAC REAL_FIELD;
 476                ALL_TAC
 477              ] THEN
 478
 479              SUBGOAL_THEN `!a b c. (c * inv(a)) * --inv(b) = c * --inv(a * b)` (fun th -> ONCE_REWRITE_TAC[th]) THENL
 480              [
 481                REWRITE_TAC[REAL_INV_MUL] THEN
 482                  REAL_ARITH_TAC;
 483                ALL_TAC
 484              ] THEN
 485
 486              SUBGOAL_THEN `&0 <= &1 - ((x * x + b * b - &2 * &2) / (&2 * x * b)) pow 2` ASSUME_TAC THENL
 487              [
 488                REWRITE_TAC[REAL_POW_DIV] THEN
 489                  REWRITE_TAC[REAL_ARITH `&0 <= a - b <=> b <= a`] THEN
 490                  MATCH_MP_TAC Trigonometry2.REAL_LE_LDIV THEN
 491                  CONJ_TAC THENL
 492                  [
 493                    REWRITE_TAC[REAL_POW_2] THEN
 494                      MATCH_MP_TAC REAL_LT_MUL THEN
 495                      ASM_REWRITE_TAC[];
 496                    ALL_TAC
 497                  ] THEN
 498                  MATCH_MP_TAC REAL_POW_LE2 THEN
 499                  CONJ_TAC THENL
 500                  [
 501                    SUBGOAL_THEN `&2 * &2 <= x * x /\ &2 * &2 <= b * b` MP_TAC THENL
 502                      [
 503                        REWRITE_TAC[GSYM REAL_POW_2] THEN
 504                          REWRITE_TAC[GSYM REAL_LE_SQUARE_ABS] THEN
 505                          REPEAT (POP_ASSUM MP_TAC) THEN
 506                          REAL_ARITH_TAC;
 507                        ALL_TAC
 508                      ] THEN
 509                      REAL_ARITH_TAC;
 510                    ALL_TAC
 511                  ] THEN
 512                  REWRITE_TAC[REAL_ARITH `x * x + b * b - &2 * &2 <= &2 * x * b <=> (x - b) pow 2 <= &2 pow 2`] THEN
 513                  REWRITE_TAC[GSYM REAL_LE_SQUARE_ABS] THEN
 514                  REPEAT (POP_ASSUM MP_TAC) THEN
 515                  REAL_ARITH_TAC;
 516                ALL_TAC
 517              ] THEN
 518
 519              FIRST_ASSUM (ASSUME_TAC o MATCH_MP REAL_LT_IMP_LE) THEN
 520              ASM_SIMP_TAC[Trigonometry1.SQRT_MUL_L] THEN
 521              SUBGOAL_THEN `(&2 * x * b) pow 2 * (&1 - ((x * x + b * b - &2 * &2) / (&2 * x * b)) pow 2) = &4 * (x * x) * b * b - (x * x + b * b - &4) pow 2` MP_TAC THENL
 522              [
 523                REWRITE_TAC[REAL_POW_DIV; REAL_ARITH `a * (&1 - c) = a - a * c`] THEN
 524                  FIRST_ASSUM (ASSUME_TAC o MATCH_MP REAL_POW_LT) THEN
 525                  ASM_SIMP_TAC[REAL_FIELD `&0 < a ==> a * c / a = c`] THEN
 526                  REAL_ARITH_TAC;
 527                ALL_TAC
 528              ] THEN
 529              DISCH_THEN (fun th -> REWRITE_TAC[th]);
 530            ALL_TAC
 531          ] THEN
 532
 533          REWRITE_TAC[IN_REAL_INTERVAL] THEN
 534          GEN_TAC THEN DISCH_TAC THEN
 535          REAL_DIFF_TAC THEN
 536
 537          SUBGOAL_THEN `&0 < &4 * (x * x) * b * b - (x * x + b * b - &4) pow 2` ASSUME_TAC THENL
 538          [
 539            REWRITE_TAC[REAL_RING `&4 * (x * x) * b * b - (x * x + b * b - &4) pow 2 = (&2 pow 2 - (x - b) pow 2) * ((x + b) pow 2 - &2 pow 2)`] THEN
 540              MATCH_MP_TAC REAL_LT_MUL THEN
 541              ONCE_REWRITE_TAC[REAL_ARITH `&0 < a - b <=> b < a`] THEN
 542              REWRITE_TAC[GSYM REAL_LT_SQUARE_ABS] THEN
 543              REPEAT (POP_ASSUM MP_TAC) THEN
 544              REAL_ARITH_TAC;
 545            ALL_TAC
 546          ] THEN
 547
 548          CONJ_TAC THENL
 549          [
 550            ASM_SIMP_TAC[] THEN
 551              FIRST_X_ASSUM (ASSUME_TAC o MATCH_MP SQRT_POS_LT) THEN
 552              ASM_SIMP_TAC[REAL_POS_NZ; REAL_ARITH `&2 <= x ==> ~(x = &0)`];
 553            ALL_TAC
 554          ] THEN
 555
 556          REWRITE_TAC[REAL_MUL_LID; REAL_MUL_RID; REAL_ADD_RID; ARITH_RULE `2 - 1 = 1`; REAL_POW_1; REAL_SUB_RZERO] THEN
 557          REWRITE_TAC[REAL_INV_MUL] THEN
 558          FIRST_ASSUM (ASSUME_TAC o MATCH_MP REAL_LT_IMP_LE) THEN
 559          ASM_SIMP_TAC[SQRT_POW_2] THEN
 560          REPEAT (POP_ASSUM MP_TAC) THEN
 561          CONV_TAC REAL_FIELD;
 562        ALL_TAC
 563      ] THEN
 564
 565      DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
 566      REWRITE_TAC[IN_REAL_INTERVAL] THEN
 567      GEN_TAC THEN DISCH_TAC THEN
 568      MATCH_MP_TAC REAL_LE_MUL THEN
 569
 570      SUBGOAL_THEN `&0 < &4 * (x * x) * b * b - (x * x + b * b - &4) pow 2` ASSUME_TAC THENL
 571      [
 572        REWRITE_TAC[REAL_RING `&4 * (x * x) * b * b - (x * x + b * b - &4) pow 2 = (&2 pow 2 - (x - b) pow 2) * ((x + b) pow 2 - &2 pow 2)`] THEN
 573          MATCH_MP_TAC REAL_LT_MUL THEN
 574          ONCE_REWRITE_TAC[REAL_ARITH `&0 < a - b <=> b < a`] THEN
 575          REWRITE_TAC[GSYM REAL_LT_SQUARE_ABS] THEN
 576          REPEAT (POP_ASSUM MP_TAC) THEN
 577          REAL_ARITH_TAC;
 578        ALL_TAC
 579      ] THEN
 580
 581      CONJ_TAC THENL
 582      [
 583        MATCH_MP_TAC REAL_LE_INV THEN
 584          MATCH_MP_TAC SQRT_POS_LE THEN
 585          MATCH_MP_TAC REAL_LT_IMP_LE THEN
 586          ASM_REWRITE_TAC[];
 587        ALL_TAC
 588      ] THEN
 589
 590      ABBREV_TAC `t:real = x * x` THEN
 591      ABBREV_TAC `u:real = b * b` THEN
 592
 593      REWRITE_TAC[REAL_ARITH `&0 <= a - b <=> b <= a`] THEN
 594      SUBGOAL_THEN `&0 < t` ASSUME_TAC THENL
 595      [
 596        EXPAND_TAC "t" THEN
 597          MATCH_MP_TAC REAL_LT_MUL THEN
 598          ASM_SIMP_TAC[REAL_ARITH `&2 <= x ==> &0 < x`];
 599        ALL_TAC
 600      ] THEN
 601
 602      ASM_SIMP_TAC[RAT_LEMMA4] THEN
 603      ONCE_REWRITE_TAC[REAL_ARITH `a <= b <=> &0 <= b - a`] THEN
 604
 605      ABBREV_TAC `f = \t. (t + u - &4) * (&4 * t * u - (t + u - &4) pow 2) - ((&2 * u - &2 * t + &8) * (t - (u - &4))) * t` THEN
 606      FIRST_ASSUM (MP_TAC o (fun th -> AP_THM th `t:real`)) THEN
 607      BETA_TAC THEN
 608      DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
 609      ABBREV_TAC `f' = \t. &3 * (-- &2 * t * u + t * (t + &8) + u pow 2) + &8 * u - &80` THEN
 610      ABBREV_TAC `f'' = \t. &6 * (t - u + &4)` THEN
 611
 612      SUBGOAL_THEN `&4 <= t /\ &4 <= u /\ t <= #6.3504 /\ u <= #6.3504` ASSUME_TAC THENL
 613      [
 614        REWRITE_TAC[REAL_ARITH `&4 = &2 * &2`; REAL_ARITH `#6.3504 = #2.52 * #2.52`] THEN
 615          EXPAND_TAC "t" THEN EXPAND_TAC "u" THEN
 616          REWRITE_TAC[GSYM REAL_POW_2] THEN
 617          REWRITE_TAC[GSYM REAL_LE_SQUARE_ABS] THEN
 618          FIRST_X_ASSUM (MP_TAC o check (is_conj o concl)) THEN
 619          REPEAT (FIRST_X_ASSUM (MP_TAC o check (is_binop `(<=):real->real->bool` o concl))) THEN
 620          REAL_ARITH_TAC;
 621        ALL_TAC
 622      ] THEN
 623      SUBGOAL_THEN `&0 <= t /\ &0 <= u` ASSUME_TAC THENL
 624      [
 625        ASM_SIMP_TAC[REAL_ARITH `&4 <= t ==> &0 <= t`];
 626        ALL_TAC
 627      ] THEN
 628
 629      MATCH_MP_TAC REAL_LE_TRANS THEN
 630      EXISTS_TAC `(f:real->real) (&4)` THEN
 631      CONJ_TAC THENL
 632      [
 633        EXPAND_TAC "f" THEN
 634          REWRITE_TAC[REAL_ARITH `&4 + u - &4 = u`] THEN
 635          REWRITE_TAC[REAL_ARITH `a - &2 * &4 + &8 = a`] THEN
 636          REWRITE_TAC[REAL_ARITH `u * (&4 * &4 * u - u pow 2) - ((&2 * u) * (&4 - (u - &4))) * &4 = u * (&24 * u - u * u - &64)`] THEN
 637          MATCH_MP_TAC REAL_LE_MUL THEN
 638          ASM_REWRITE_TAC[] THEN
 639          ABBREV_TAC `g = \u. &24 * u - u * u - &64` THEN
 640          FIRST_ASSUM (MP_TAC o (fun th -> AP_THM th `u:real`)) THEN
 641          BETA_TAC THEN DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
 642          MATCH_MP_TAC REAL_LE_TRANS THEN
 643          EXISTS_TAC `(g:real->real) (&4)` THEN
 644          CONJ_TAC THENL
 645          [
 646            EXPAND_TAC "g" THEN
 647              REAL_ARITH_TAC;
 648            ALL_TAC
 649          ] THEN
 650          MATCH_MP_TAC HAS_REAL_DERIVATIVE_INCREASING_IMP THEN
 651          EXISTS_TAC `\u. &24 - &2 * u` THEN
 652          EXISTS_TAC `real_interval [&4,#6.3504]` THEN
 653          REWRITE_TAC[IS_REALINTERVAL_INTERVAL] THEN
 654          CONJ_TAC THENL
 655          [
 656            REPEAT STRIP_TAC THEN
 657              EXPAND_TAC "g" THEN
 658              REAL_DIFF_TAC THEN
 659              REAL_ARITH_TAC;
 660            ALL_TAC
 661          ] THEN
 662          ASM_REWRITE_TAC[IN_REAL_INTERVAL; REAL_ARITH `&4 <= &4 /\ &4 <= #6.3504`] THEN
 663          REAL_ARITH_TAC;
 664        ALL_TAC
 665      ] THEN
 666
 667      MATCH_MP_TAC HAS_REAL_DERIVATIVE_INCREASING_IMP THEN
 668      MAP_EVERY EXISTS_TAC [`f':real->real`; `real_interval [&4,#6.3504]`] THEN
 669      ASM_REWRITE_TAC[IN_REAL_INTERVAL; REAL_ARITH `&4 <= &4 /\ &4 <= #6.3504`] THEN
 670      REWRITE_TAC[IS_REALINTERVAL_INTERVAL] THEN
 671      CONJ_TAC THENL
 672      [
 673        REPEAT STRIP_TAC THEN
 674          EXPAND_TAC "f" THEN EXPAND_TAC "f'" THEN
 675          REAL_DIFF_TAC THEN
 676          REWRITE_TAC[ARITH_RULE `2 - 1 = 1`] THEN
 677          REAL_ARITH_TAC;
 678        ALL_TAC
 679      ] THEN
 680
 681      X_GEN_TAC `y:real` THEN DISCH_TAC THEN
 682      MATCH_MP_TAC REAL_LE_TRANS THEN
 683      EXISTS_TAC `(f':real->real) (&4)` THEN
 684      CONJ_TAC THENL
 685      [
 686        EXPAND_TAC "f'" THEN
 687          REWRITE_TAC[REAL_ARITH `&3 * (-- &2 * &4 * u + &4 * (&4 + &8) + u pow 2) + &8 * u - &80 = &3 * (u - &8 / &3) pow 2 + &128 / &3`] THEN
 688          MATCH_MP_TAC REAL_LE_ADD THEN
 689          CONJ_TAC THENL
 690          [
 691            MATCH_MP_TAC REAL_LE_MUL THEN
 692              REWRITE_TAC[REAL_POW_2; REAL_LE_SQUARE] THEN
 693              REAL_ARITH_TAC;
 694            REAL_ARITH_TAC
 695          ];
 696        ALL_TAC
 697      ] THEN
 698
 699      MATCH_MP_TAC HAS_REAL_DERIVATIVE_INCREASING_IMP THEN
 700      MAP_EVERY EXISTS_TAC [`f'':real->real`; `real_interval [&4,#6.3504]`] THEN
 701      ASM_REWRITE_TAC[IN_REAL_INTERVAL; REAL_ARITH `&4 <= &4 /\ &4 <= #6.3504`] THEN
 702      REWRITE_TAC[IS_REALINTERVAL_INTERVAL] THEN
 703      CONJ_TAC THENL
 704      [
 705        REPEAT STRIP_TAC THEN
 706          EXPAND_TAC "f'" THEN EXPAND_TAC "f''" THEN
 707          REAL_DIFF_TAC THEN
 708          REAL_ARITH_TAC;
 709        ALL_TAC
 710      ] THEN
 711
 712      EXPAND_TAC "f''" THEN
 713      REPLICATE_TAC 3 (POP_ASSUM MP_TAC) THEN
 714      REAL_ARITH_TAC);;
 715
 716
 717
 718 (* arc x b 2 >= arc (2 h0) b 2 + lmfun(x / 2) * (arc 2 b 2 - arc (2 h0) b 2) *)
 719
 720 let arc_lemma3 = prove(`!x b. (&2 <= x /\ x <= #2.52) /\ (&2 <= b /\ b <= #2.52)
 721                        ==> arclength x b (&2) >=
 722                               arclength (#2.52) b (&2) +
 723                                 lmfun(x / &2) * (arclength (&2) b (&2) - arclength (#2.52) b (&2))`,
 724    REPEAT STRIP_TAC THEN
 725      MP_TAC (SPEC_ALL arc_concave) THEN
 726      ASM_REWRITE_TAC[real_convex_on] THEN
 727      DISCH_THEN (MP_TAC o SPECL [`&2`; `#2.52`; `lmfun (x / &2)`; `&1 - lmfun (x / &2)`]) THEN
 728      REWRITE_TAC[IN_REAL_INTERVAL; REAL_LE_REFL; REAL_ARITH `&2 <= #2.52`; REAL_ARITH `a + &1 - a = &1`] THEN
 729      SUBGOAL_THEN `&0 <= lmfun (x / &2) /\ &0 <= &1 - lmfun (x / &2)` ASSUME_TAC THENL
 730      [
 731        REWRITE_TAC[Pack_defs.lmfun; Pack_defs.h0] THEN
 732          REPEAT (POP_ASSUM MP_TAC) THEN
 733          REAL_ARITH_TAC;
 734        ALL_TAC
 735      ] THEN
 736      ASM_REWRITE_TAC[] THEN
 737      SUBGOAL_THEN `lmfun (x / &2) * &2 + (&1 - lmfun (x / &2)) * #2.52 = x` (fun th -> REWRITE_TAC[th]) THENL
 738      [
 739        REWRITE_TAC[Pack_defs.lmfun; Pack_defs.h0] THEN
 740          REPEAT (POP_ASSUM MP_TAC) THEN
 741          REAL_ARITH_TAC;
 742        ALL_TAC
 743      ] THEN
 744      REAL_ARITH_TAC);;
 745
 746
 747
 748
 749 (********************************************************)
 750
 751
 752
 753
 754 let ABS_LE_BOUNDS = prove(`!x a e. abs (x - a) <= e <=> a - e <= x /\ x <= a + e`,
 755                           REAL_ARITH_TAC);;
 756
 757
 758
 759
 760 (* Estimates for the proof of arc_lemma4 *)
 761
 762 let estimate0 = prove(`arclength (&2) #2.52 (&2) - arclength #2.52 #2.52 (&2) >= #0.073`,
 763    SUBGOAL_THEN `arclength #2.52 #2.52 (&2) = acs ((#2.52 * #2.52 + #2.52 * #2.52 - (&2) * (&2)) / (&2 * #2.52 * #2.52))` (fun th -> REWRITE_TAC[th]) THENL
 764    [
 765      MATCH_MP_TAC Trigonometry1.ACS_ARCLENGTH THEN
 766        REAL_ARITH_TAC;
 767      ALL_TAC
 768    ] THEN
 769    SUBGOAL_THEN `arclength (&2) #2.52 (&2) = acs (((&2) * (&2) + #2.52 * #2.52 - (&2) * (&2)) / (&2 * (&2) * #2.52))` (fun th -> REWRITE_TAC[th]) THENL
 770    [
 771      MATCH_MP_TAC Trigonometry1.ACS_ARCLENGTH THEN
 772        REAL_ARITH_TAC;
 773      ALL_TAC
 774    ] THEN
 775    CONV_TAC REAL_RAT_REDUCE_CONV THEN
 776    REWRITE_TAC[REAL_ARITH `#0.073 = #0.8892 - #0.8162`] THEN
 777    MATCH_MP_TAC (REAL_ARITH `a >= b /\ c <= d ==> a - c >= b - d`) THEN
 778    CONJ_TAC THENL
 779    [
 780      SUBGOAL_THEN `#0.8892 = acs (cos #0.8892)` (fun th -> ONCE_REWRITE_TAC[th]) THENL
 781        [
 782          MATCH_MP_TAC (GSYM ACS_COS) THEN
 783            MP_TAC PI_APPROX_32 THEN
 784            REAL_ARITH_TAC;
 785          ALL_TAC
 786        ] THEN
 787        REWRITE_TAC[real_ge] THEN
 788        MATCH_MP_TAC ACS_MONO_LE THEN
 789        REWRITE_TAC[COS_BOUNDS] THEN
 790        CONJ_TAC THENL
 791        [
 792          CONV_TAC REAL_RAT_LE_CONV;
 793          MP_TAC (CONJUNCT1 (REWRITE_RULE[ABS_LE_BOUNDS] (cos_eval `#0.8892` 2))) THEN
 794            REAL_ARITH_TAC
 795        ];
 796
 797      SUBGOAL_THEN `#0.8162 = acs (cos #0.8162)` (fun th -> ONCE_REWRITE_TAC[th]) THENL
 798        [
 799          MATCH_MP_TAC (GSYM ACS_COS) THEN
 800            MP_TAC PI_APPROX_32 THEN
 801            REAL_ARITH_TAC;
 802          ALL_TAC
 803        ] THEN
 804        MATCH_MP_TAC ACS_MONO_LE THEN
 805        REWRITE_TAC[COS_BOUNDS] THEN
 806        CONJ_TAC THENL
 807        [
 808          MP_TAC ((CONJUNCT2 o REWRITE_RULE[ABS_LE_BOUNDS]) (cos_eval `#0.8162` 3)) THEN
 809            REAL_ARITH_TAC;
 810          CONV_TAC REAL_RAT_LE_CONV
 811        ]
 812    ]);;
 813
 814
 815 let estimate1 = prove(`!x. &2 <= x /\ x <= #2.52  ==> &1 / &4 * --inv (sqrt (&1 - (x / &4) pow 2)) <= -- #0.28`,
 816    REPEAT STRIP_TAC THEN
 817      REWRITE_TAC[REAL_ARITH `&1 / &4 * --a <= --b <=> &4 * b <= a`] THEN
 818      ONCE_REWRITE_TAC[REAL_ARITH `&4 * #0.28 = inv (inv (&4 * #0.28))`] THEN
 819      MATCH_MP_TAC REAL_LE_INV2 THEN
 820      SUBGOAL_THEN `&0 < &1 - (x / &4) pow 2` ASSUME_TAC THENL
 821      [
 822        REWRITE_TAC[REAL_ARITH `&0 < &1 - a <=> a < &1`] THEN
 823          ONCE_REWRITE_TAC[REAL_ARITH `&1 = &1 pow 2`] THEN
 824          MATCH_MP_TAC REAL_POW_LT2 THEN
 825          REWRITE_TAC[ARITH_RULE `~(2 = 0)`] THEN
 826          REPEAT (POP_ASSUM MP_TAC) THEN
 827          REAL_ARITH_TAC;
 828        ALL_TAC
 829      ] THEN
 830      CONJ_TAC THENL
 831      [
 832        MATCH_MP_TAC SQRT_POS_LT THEN
 833          ASM_REWRITE_TAC[];
 834        ALL_TAC
 835      ] THEN
 836      MATCH_MP_TAC REAL_LE_LSQRT THEN
 837      ASM_SIMP_TAC[REAL_LT_IMP_LE] THEN
 838      CONJ_TAC THENL
 839      [
 840        REAL_ARITH_TAC;
 841        ALL_TAC
 842      ] THEN
 843      ONCE_REWRITE_TAC[REAL_ARITH `&1 - a <= b <=> &1 - b <= a`] THEN
 844      REWRITE_TAC[REAL_POW_2] THEN
 845      REWRITE_TAC[REAL_ARITH `a <= x / &4 * x / &4 <=> &16 * a <= x * x`] THEN
 846      CONV_TAC REAL_RAT_REDUCE_CONV THEN
 847      MATCH_MP_TAC REAL_LE_TRANS THEN
 848      EXISTS_TAC `&2 * &2` THEN
 849      CONJ_TAC THENL
 850      [
 851        CONV_TAC REAL_RAT_REDUCE_CONV;
 852        REWRITE_TAC[GSYM REAL_POW_2] THEN
 853          MATCH_MP_TAC REAL_POW_LE2 THEN
 854          ASM_REWRITE_TAC[REAL_ARITH `&0 <= &2`]
 855      ]);;
 856
 857
 858
 859
 860 let estimate2 = prove(`!x. &2 <= x /\ x <= #2.52
 861         ==> (&2 * &2 * #2.52 * x * x - (&3969 / &625 + x * x - &4) * &126 / &25) / (&2 * #2.52 * x) pow 2 <= #0.13 /\
 862             &0 <= (&2 * &2 * #2.52 * x * x - (&3969 / &625 + x * x - &4) * &126 / &25) / (&2 * #2.52 * x) pow 2`,
 863    GEN_TAC THEN DISCH_TAC THEN
 864      SUBGOAL_THEN `&0 < (&2 * #2.52 * x) pow 2` ASSUME_TAC THENL
 865      [
 866        MATCH_MP_TAC REAL_POW_LT THEN
 867          POP_ASSUM MP_TAC THEN
 868          REAL_ARITH_TAC;
 869        ALL_TAC
 870      ] THEN
 871      ASM_SIMP_TAC[REAL_LE_LDIV_EQ; REAL_LE_RDIV_EQ; REAL_MUL_LZERO] THEN
 872      ABBREV_TAC `t:real = x * x` THEN
 873      SUBGOAL_THEN `&2 * &2 <= t /\ t <= #2.52 * #2.52` MP_TAC THENL
 874      [
 875        EXPAND_TAC "t" THEN
 876          REWRITE_TAC[GSYM REAL_POW_2] THEN
 877          CONJ_TAC THEN MATCH_MP_TAC REAL_POW_LE2 THEN ASM_REWRITE_TAC[] THENL
 878          [
 879            REAL_ARITH_TAC;
 880            MATCH_MP_TAC REAL_LE_TRANS THEN
 881              EXISTS_TAC `&2` THEN
 882              ASM_REWRITE_TAC[REAL_ARITH `&0 <= &2`]
 883          ];
 884        ALL_TAC
 885      ] THEN
 886
 887      REWRITE_TAC[REAL_POW_2] THEN
 888      ASM_REWRITE_TAC[REAL_ARITH `(a * b * x) * a * b * x = (a * b) * (a * b) * (x * x)`] THEN
 889      REAL_ARITH_TAC);;
 890
 891
 892
 893 let estimate3 = prove(`!x. &2 <= x /\ x <= #2.52 ==>
 894         inv (sqrt (&1 - ((&3969 / &625 + x * x - &4) / (&2 * #2.52 * x)) pow 2)) <= &2 /\
 895         &0 <= inv (sqrt (&1 - ((&3969 / &625 + x * x - &4) / (&2 * #2.52 * x)) pow 2))`,
 896    GEN_TAC THEN DISCH_TAC THEN
 897      SUBGOAL_THEN `inv (&2) <= sqrt (&1 - ((&3969 / &625 + x * x - &4) / (&2 * #2.52 * x)) pow 2)` ASSUME_TAC THENL
 898      [
 899        MATCH_MP_TAC REAL_LE_RSQRT THEN
 900          REWRITE_TAC[REAL_ARITH `a <= &1 - c <=> c <= &1 - a`; REAL_INV_INV] THEN
 901          REWRITE_TAC[REAL_POW_DIV; REAL_POW_2] THEN
 902          REWRITE_TAC[REAL_ARITH `(a * b * x) * a * b * x = (a * b * a * b) * x * x`] THEN
 903          ABBREV_TAC `t:real = x * x` THEN
 904          SUBGOAL_THEN `&4 <= t /\ t <= #6.3504` ASSUME_TAC THENL
 905          [
 906            REWRITE_TAC[REAL_ARITH `&4 = &2 * &2`; REAL_ARITH `#6.3504 = #2.52 * #2.52`] THEN
 907              EXPAND_TAC "t" THEN
 908              REWRITE_TAC[GSYM REAL_POW_2] THEN
 909              CONJ_TAC THEN MATCH_MP_TAC REAL_POW_LE2 THEN ASM_REWRITE_TAC[] THENL
 910              [
 911                REAL_ARITH_TAC;
 912                REPEAT (POP_ASSUM MP_TAC) THEN
 913                  REAL_ARITH_TAC
 914              ];
 915            ALL_TAC
 916          ] THEN
 917
 918          CONV_TAC (DEPTH_CONV REAL_RAT_MUL_CONV) THEN
 919          SUBGOAL_THEN `&0 < &15876 / &625 * t` ASSUME_TAC THENL
 920          [
 921            POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;
 922            ALL_TAC
 923          ] THEN
 924          ASM_SIMP_TAC[REAL_LE_LDIV_EQ] THEN
 925          REWRITE_TAC[REAL_ARITH `a + t - b = (a - b) + t`; REAL_ARITH `a * b * t = (a * b) * t`] THEN
 926          CONV_TAC REAL_RAT_REDUCE_CONV THEN
 927          REWRITE_TAC[REAL_ARITH `(a + t) * (a + t) <= b * t <=> (b / &2 - a - t) * (b / &2 - a - t) <= b * b / &4 - a * b`] THEN
 928          CONV_TAC REAL_RAT_REDUCE_CONV THEN
 929          MATCH_MP_TAC REAL_LE_TRANS THEN
 930          EXISTS_TAC `&4 * &4` THEN
 931          CONJ_TAC THENL
 932          [
 933            REWRITE_TAC[GSYM REAL_POW_2] THEN
 934              MATCH_MP_TAC REAL_POW_LE2 THEN
 935              FIRST_X_ASSUM (MP_TAC o check (is_conj o concl)) THEN
 936              REAL_ARITH_TAC;
 937            ALL_TAC
 938          ] THEN
 939          REAL_ARITH_TAC;
 940        ALL_TAC
 941      ] THEN
 942
 943      CONJ_TAC THENL
 944      [
 945        ONCE_REWRITE_TAC[REAL_ARITH `&2 = inv (inv (&2))`] THEN
 946          MATCH_MP_TAC REAL_LE_INV2 THEN
 947          ASM_REWRITE_TAC[REAL_ARITH `&0 < inv (&2)`; REAL_INV_INV];
 948        ALL_TAC
 949      ] THEN
 950
 951      MATCH_MP_TAC REAL_LE_INV THEN
 952      MATCH_MP_TAC REAL_LE_TRANS THEN
 953      EXISTS_TAC `inv (&2)` THEN
 954      ASM_REWRITE_TAC[REAL_ARITH `&0 <= inv (&2)`]);;
 955
 956
 957
 958 (* arc 2 x 2 - arc (2 h0) x 2 >= 0.073 *)
 959
 960 let arc_lemma4 = prove(`!x. &2 <= x /\ x <= #2.52
 961   ==> arclength (&2) x (&2) - arclength (#2.52) x (&2) >= #0.073`,
 962    REPEAT STRIP_TAC THEN
 963      REWRITE_TAC[REAL_ARITH `a - b >= c <=> b - a <= --c`] THEN
 964      MATCH_MP_TAC REAL_LE_TRANS THEN
 965      EXISTS_TAC `arclength #2.52 #2.52 (&2) - arclength (&2) #2.52 (&2)` THEN
 966      REWRITE_TAC[REWRITE_RULE [REAL_ARITH `a - b >= c <=> b - a <= --c`] estimate0] THEN
 967      ONCE_REWRITE_TAC[arc_sym] THEN
 968      MP_TAC (SPECL [`\x. arclength x #2.52 (&2) - arclength x (&2) (&2)`;
 969                     `\x. (&2 * &2 * #2.52 * x * x - (&3969 / &625 + x * x - &4) * &126 / &25) / (&2 * #2.52 * x) pow 2 *
 970                       --inv (sqrt (&1 - ((&3969 / &625 + x * x - &4) / (&2 * #2.52 * x)) pow 2)) -
 971                       &1 / &4 * --inv (sqrt (&1 - (x / &4) pow 2))`;
 972                     `real_interval [&2, #2.52]`]
 973                HAS_REAL_DERIVATIVE_INCREASING) THEN
 974
 975      ANTS_TAC THENL
 976      [
 977        REWRITE_TAC[IS_REALINTERVAL_INTERVAL] THEN
 978          CONJ_TAC THENL
 979          [
 980            REWRITE_TAC[NOT_EXISTS_THM] THEN GEN_TAC THEN
 981              DISCH_TAC THEN
 982              SUBGOAL_THEN `&2 = a /\ #2.52 = a` MP_TAC THENL
 983              [
 984                REWRITE_TAC[GSYM IN_SING] THEN
 985                  POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN
 986                  REWRITE_TAC[IN_REAL_INTERVAL] THEN
 987                  REAL_ARITH_TAC;
 988                ALL_TAC
 989              ] THEN
 990              REAL_ARITH_TAC;
 991            ALL_TAC
 992          ] THEN
 993
 994          REWRITE_TAC[IN_REAL_INTERVAL] THEN
 995          X_GEN_TAC `y:real` THEN DISCH_TAC THEN
 996          MATCH_MP_TAC HAS_REAL_DERIVATIVE_SUB THEN
 997          CONJ_TAC THENL
 998          [
 999            MP_TAC (SPECL [`y:real`; `#2.52`] arc_derivative) THEN
1000              ANTS_TAC THENL
1001              [
1002                ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC;
1003                ALL_TAC
1004              ] THEN
1005              REWRITE_TAC[REAL_ARITH `(y + y) * a * y * b = &2 * a * b * y * y`] THEN
1006              ONCE_REWRITE_TAC[REAL_ARITH `a + b - &4 = b + (a - &4)`] THEN
1007              CONV_TAC REAL_RAT_REDUCE_CONV THEN
1008              REWRITE_TAC[REAL_ARITH `&2 * y * #2.52 = &2 * #2.52 * y`];
1009            ALL_TAC
1010          ] THEN
1011          MP_TAC (SPECL [`y:real`; `&2`] arc_derivative) THEN
1012          ANTS_TAC THENL
1013          [
1014            ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC;
1015            ALL_TAC
1016          ] THEN
1017          CONV_TAC REAL_RAT_REDUCE_CONV THEN
1018          REWRITE_TAC[REAL_ARITH `(y + y) * &2 * y * &2 - (y * y + &0) * &4 = &4 * (y pow 2)`] THEN
1019          ASM_SIMP_TAC[REAL_FIELD `&2 <= y ==> ((y * y + &0) / (&2 * y * &2)) pow 2 = (y / &4) pow 2`] THEN
1020          ASM_SIMP_TAC[REAL_FIELD `&2 <= y ==> (&4 * y pow 2) / (&2 * y * &2) pow 2 = &1 / &4`];
1021        ALL_TAC
1022      ] THEN
1023
1024      BETA_TAC THEN
1025      DISCH_TAC THEN
1026
1027      FIRST_ASSUM (fun th -> SUBGOAL_THEN ((fst o dest_eq o concl) th) MP_TAC) THENL
1028      [
1029        REPEAT (POP_ASSUM (fun th -> ALL_TAC)) THEN
1030          REWRITE_TAC[IN_REAL_INTERVAL] THEN
1031          REPEAT STRIP_TAC THEN
1032          MATCH_MP_TAC (REAL_ARITH `(?c d. c <= a /\ b <= d /\ &0 <= c - d) ==> &0 <= a - b`) THEN
1033          MAP_EVERY EXISTS_TAC [`#0.13 * (-- &2)`; `-- #0.28`] THEN
1034          CONJ_TAC THENL
1035          [
1036            REWRITE_TAC[REAL_ARITH `a * --b <= c * --d <=> c * d <= a * b`] THEN
1037              MATCH_MP_TAC REAL_LE_MUL2 THEN
1038              ASM_SIMP_TAC[estimate2; estimate3];
1039            ALL_TAC
1040          ] THEN
1041
1042          ASM_SIMP_TAC[estimate1] THEN
1043          REAL_ARITH_TAC;
1044        ALL_TAC
1045      ] THEN
1046
1047      POP_ASSUM (fun th -> REWRITE_TAC[th]) THEN
1048      DISCH_THEN (MP_TAC o SPECL [`x:real`; `#2.52`]) THEN
1049      ASM_REWRITE_TAC[IN_REAL_INTERVAL; REAL_ARITH `&2 <= #2.52 /\ #2.52 <= #2.52`]
1050                       );;
1051
1052
1053
1054
1055
1056 (* arclength (2 h0) (2 h0) 2 >= 0.816 *)
1057
1058 let arc_lemma5 = prove(`arclength #2.52 #2.52 (&2) >= #0.816`,
1059    SUBGOAL_THEN `arclength #2.52 #2.52 (&2) = acs ((#2.52 * #2.52 + #2.52 * #2.52 - (&2) * (&2)) / (&2 * #2.52 * #2.52))` (fun th -> REWRITE_TAC[th]) THENL
1060    [
1061      MATCH_MP_TAC Trigonometry1.ACS_ARCLENGTH THEN
1062        REAL_ARITH_TAC;
1063      ALL_TAC
1064    ] THEN
1065
1066    CONV_TAC (REAL_RAT_REDUCE_CONV) THEN
1067    SUBGOAL_THEN `#0.816 = acs (cos (#0.816))` MP_TAC THENL
1068    [
1069      MATCH_MP_TAC (GSYM ACS_COS) THEN
1070        MP_TAC PI_APPROX_32 THEN
1071        REAL_ARITH_TAC;
1072      ALL_TAC
1073    ] THEN
1074    DISCH_THEN (fun th -> ONCE_REWRITE_TAC[th]) THEN
1075    REWRITE_TAC[real_ge] THEN
1076    MATCH_MP_TAC ACS_MONO_LE THEN
1077    REWRITE_TAC[COS_BOUNDS] THEN
1078    CONJ_TAC THENL
1079    [
1080      CONV_TAC REAL_RAT_LE_CONV;
1081      MP_TAC (CONJUNCT1 (REWRITE_RULE [ABS_LE_BOUNDS] (cos_eval `#0.816` 2))) THEN
1082        REAL_ARITH_TAC
1083    ]);;
1084
1085
1086
1087
1088
1089
1090 end;;
1091