text_formalization/packing/YSSKQOY.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (* Section: Counting Spheres                                                  *)
   4 (* Chapter: packing                                                           *)
   5 (* Author: Thomas C. Hales                                                    *)
   6 (* Date: 2011-06-18                                                           *)
   7 (* ========================================================================== *)
   8
   9
  10
  11 flyspeck_needs "usr/thales/hales_tactic.hl";;
  12
  13 module Ysskqoy = struct
  14
  15   open Tactics_jordan;;
  16 open Hales_tactic;;
  17
  18
  19 (* ========================================================================== *)
  20 (* Nonlinear inequality hypotheses *)
  21 (* ========================================================================== *)
  22
  23
  24 let pack_ineq_tml =
  25   let has_packid = (fun t -> not(intersect ["UKBRPFE";"WAZLDCD";"BIEFJHU"] (Ineq.flypaper_ids t) = [])) in
  26   let idl = (filter has_packid !Ineq.ineqs) in
  27   let tml = map (fun t -> t.ineq) idl in
  28     end_itlist (curry mk_conj) tml;;
  29
  30 let pack_ineq_def_a =
  31   new_definition (mk_eq (`pack_ineq_def_a:bool`,pack_ineq_tml));;
  32
  33
  34 (* ========================================================================== *)
  35 (* some general lemmas *)
  36 (* ========================================================================== *)
  37
  38
  39 let selectd = new_definition `selectd P d =
  40   if (?r. P r) then (@) P else (d:A)`;;
  41
  42 let selectd_cases = prove_by_refinement(
  43   `!P (d:A). P(selectd P d) \/ (selectd P d  = d)`,
  44   (* {{{ proof *)
  45   [
  46   REWRITE_TAC [selectd];
  47   REPEAT WEAK_STRIP_TAC;
  48   COND_CASES_TAC THEN (ASM_REWRITE_TAC []);
  49   DISJ1_TAC;
  50   MATCH_MP_TAC SELECT_AX;
  51   BY(ASM_REWRITE_TAC [])
  52   ]);;
  53   (* }}} *)
  54
  55 let selectd_exists = prove_by_refinement(
  56   `!P (d:A). (?r. P r) ==> P(selectd P d)`,
  57   (* {{{ proof *)
  58   [
  59   REWRITE_TAC[selectd];
  60   REPEAT GEN_TAC;
  61   SIMP_TAC[SELECT_AX]
  62   ]);;
  63   (* }}} *)
  64
  65
  66 let DOT_COMPLEX = prove_by_refinement(
  67   `!x y x' y'. (complex (x,y)) dot (complex (x',y')) = x * x' + y * y'`,
  68   (* {{{ proof *)
  69   [
  70   SIMP_TAC [ complex;dot; DIMINDEX_2; SUM_2; VECTOR_2 ]
  71   ]);;
  72   (* }}} *)
  73
  74 let DOT_RE = prove_by_refinement(
  75   `!z1 z2. z1 dot z2 = Re (z1 * cnj z2)`,
  76   (* {{{ proof *)
  77   [
  78   REWRITE_TAC [ FORALL_COMPLEX;DOT_COMPLEX;complex_mul;RE;IM;RE_CNJ;IM_CNJ ];
  79   REAL_ARITH_TAC
  80   ]);;
  81   (* }}} *)
  82
  83 let ARG_CNJ = prove_by_refinement(
  84   `!z w. ~(w = Cx (&0)) ==> Arg (z / w) = Arg (z * cnj w)`,
  85   (* {{{ proof *)
  86   [
  87   ONCE_REWRITE_TAC [ COMPLEX_DIV_CNJ ];
  88   REPEAT WEAK_STRIP_TAC;
  89   REWRITE_TAC [ complex_div; GSYM CX_INV ; COMPLEX_POW_2;COMPLEX_INV_MUL ];
  90   TYPIFY `&0 < inv (norm w)` (C SUBGOAL_THEN ASSUME_TAC);
  91   MATCH_MP_TAC REAL_LT_INV;
  92   REWRITE_TAC [ NORM_POS_LT ];
  93   BY(ASM_MESON_TAC [COMPLEX_VEC_0]);
  94   ONCE_REWRITE_TAC [ COMPLEX_MUL_ASSOC ];
  95   ASM_SIMP_TAC [ ONCE_REWRITE_RULE [ COMPLEX_MUL_SYM ] ARG_MUL_CX ]
  96   ]);;
  97   (* }}} *)
  98
  99 let ARG_0_DIV = prove_by_refinement(
 100   `!u v. ( (u/v) = Cx (&0)) <=> (u = Cx (&0) \/ v = Cx (&0))`,
 101   (* {{{ proof *)
 102   [
 103   BY(REWRITE_TAC [ COMPLEX_ENTIRE;complex_div;COMPLEX_INV_EQ_0 ]);
 104   ]);;
 105   (* }}} *)
 106
 107 let CARD_UNION_EQ = prove
 108  (`!(s:B->bool) t u. FINITE u /\ (s INTER t = {}) /\ (s UNION t = u)
 109            ==> (CARD s + CARD t = CARD u)`,
 110   MESON_TAC[CARD_UNION; FINITE_SUBSET; SUBSET_UNION]);;
 111
 112 let INJ_SURJ = prove_by_refinement(
 113   `!a b (f:A->B).  FINITE a /\ FINITE b /\ (CARD a = CARD b) ==>
 114     (INJ f a b ==> SURJ f a b)`,
 115   (* {{{ proof *)
 116   [
 117   REPEAT WEAK_STRIP_TAC;
 118   ABBREV_TAC `s = IMAGE (f:A->B) a`;
 119   ABBREV_TAC `t = { r | b r /\ ~(?k. a k /\ r = (f:A->B) k) }`;
 120   INTRO_TAC  CARD_UNION_EQ [`s`;`t`;`b`];
 121   ANTS_TAC;
 122   ASM_REWRITE_TAC [];
 123   ONCE_REWRITE_TAC [ FUN_EQ_THM ];
 124   EXPAND_TAC "s";
 125   EXPAND_TAC "t";
 126   HASH_UNDISCH_TAC 4678;
 127   REWRITE_TAC [IMAGE;INTER;UNION;IN_ELIM_THM;INJ];
 128   REWRITE_TAC [ IN;IN_ELIM_THM;X_IN NOT_IN_EMPTY ];
 129   BY(MESON_TAC []);
 130   SUBGOAL_THEN `BIJ (f:A->B) a (IMAGE f a)` ASSUME_TAC;
 131   REWRITE_TAC [ BIJ ; Misc_defs_and_lemmas.IMAGE_SURJ ];
 132   HASH_UNDISCH_TAC 4678;
 133   REWRITE_TAC [ INJ;IMAGE;IN_ELIM_THM ];
 134   BY(MESON_TAC []);
 135   SUBGOAL_THEN `CARD (a:A->bool) = CARD (s:B->bool)` ASSUME_TAC;
 136   ASM_MESON_TAC [ Misc_defs_and_lemmas.BIJ_CARD ];
 137   DISCH_TAC;
 138   SUBGOAL_THEN ` (t:B->bool) HAS_SIZE 0` ASSUME_TAC;
 139   REWRITE_TAC [HAS_SIZE];
 140   CONJ_TAC;
 141   MATCH_MP_TAC FINITE_SUBSET;
 142   EXISTSv_TAC "b";
 143   ASM_REWRITE_TAC [];
 144   EXPAND_TAC "t";
 145   SET_TAC[];
 146   BY(ASM_MESON_TAC [ ARITH_RULE `x + (t:num) = x ==> (t = 0)` ]);
 147   HASH_RULE_TAC 526 (REWRITE_RULE [ HAS_SIZE_0 ]);
 148   EXPAND_TAC "t";
 149   HASH_UNDISCH_TAC 4678;
 150   REWRITE_TAC [ SURJ;INJ;IN_ELIM_THM;IN ];
 151   ONCE_REWRITE_TAC [ FUN_EQ_THM ];
 152   REWRITE_TAC [ SURJ;INJ;IN_ELIM_THM;IN;X_IN NOT_IN_EMPTY ];
 153   BY(MESON_TAC [])
 154   ]);;
 155   (* }}} *)
 156
 157 let INJ_IFF_SURJ = prove_by_refinement(
 158   `!a b (f:A->B).  FINITE a /\ FINITE b /\ (CARD a = CARD b) ==>
 159     (INJ f a b <=> SURJ f a b)`,
 160   (* {{{ proof *)
 161   [
 162   REPEAT WEAK_STRIP_TAC;
 163   EQ_TAC;
 164   MATCH_MP_TAC INJ_SURJ;
 165   BY(ASM_MESON_TAC []);
 166   DISCH_TAC;
 167   HASH_COPY_TAC 6181;
 168   HASH_UNDISCH_TAC 6181;
 169   DISCH_THEN (MP_TAC o (MATCH_MP Misc_defs_and_lemmas.INVERSE_DEF));
 170   REPEAT WEAK_STRIP_TAC;
 171   TYPIFY `SURJ (INVERSE f a b) b a` (C SUBGOAL_THEN MP_TAC);
 172   HASH_UNDISCH_TAC 7518;
 173   MATCH_MP_TAC INJ_SURJ;
 174   BY(ASM_REWRITE_TAC []);
 175   DISCH_TAC;
 176   REWRITE_TAC [ INJ ];
 177   SUBCONJ_TAC;
 178   ASM_MESON_TAC [ SURJ ];
 179   DISCH_TAC;
 180   REPEAT WEAK_STRIP_TAC;
 181   SUBGOAL_THEN `(?r1 r2. r1 IN b /\ r2 IN b /\ x = (INVERSE (f:A->B) a b r1) /\ (y = (INVERSE f a b r2)))` MP_TAC;
 182   ASM_MESON_TAC [SURJ];
 183   REPEAT WEAK_STRIP_TAC;
 184   ASM_MESON_TAC []
 185   ]);;
 186   (* }}} *)
 187
 188 let NORM1_NZ = prove_by_refinement(
 189   `!(a:real^N). norm a = &1 ==> ~(a = vec 0)`,
 190   (* {{{ proof *)
 191   [
 192 MESON_TAC [NORM_0;REAL_ARITH `~(&1 = &0)`]
 193   ]);;
 194   (* }}} *)
 195
 196 (* from tame *)
 197
 198 let normalize = new_definition `!(v:real^N). normalize v = inv (norm v) % v`;;
 199
 200 let norm_normalize = prove_by_refinement(
 201  `! (v:real^N). ~(v = vec 0) ==> norm (normalize v) = &1 `,
 202 [
 203 (GEN_TAC THEN STRIP_TAC);
 204 (PURE_REWRITE_TAC[normalize;NORM_MUL;REAL_ABS_INV;REAL_ABS_NORM]);
 205 (MATCH_MP_TAC REAL_MUL_LINV);
 206 (ASM_MESON_TAC[NORM_EQ_0]);
 207 ]);;
 208
 209 let NZ_IMP_NORM1 = prove_by_refinement(
 210   `!(a:real^N) b. ~(a = vec 0) ==>
 211    (?a' b'. (norm a' = &1) /\
 212       (!x. (a dot x <= b) <=>  (a' dot x <= b') ) /\
 213       (!x. (a dot x = b) <=> (a' dot x = b') ))`,
 214   (* {{{ proof *)
 215   [
 216 REPEAT STRIP_TAC ;
 217 EXISTS_TAC `normalize (a:real^N)`;
 218 EXISTS_TAC `inv(norm (a:real^N)) * b`;
 219 ASM_SIMP_TAC [norm_normalize];
 220 ASM_SIMP_TAC [norm_normalize];
 221 REWRITE_TAC [normalize;DOT_LMUL];
 222 FIRST_X_ASSUM (ASSUME_TAC o (REWRITE_RULE[GSYM NORM_POS_LT]));
 223 FIRST_X_ASSUM (ASSUME_TAC o (ONCE_REWRITE_RULE[GSYM REAL_LT_INV_EQ]));
 224 ASM_SIMP_TAC [REAL_LE_LMUL_EQ];
 225 ASM_MESON_TAC [REAL_EQ_MUL_LCANCEL;REAL_ARITH `&0 < u ==> ~(u= &0)`]
 226   ]);;
 227   (* }}} *)
 228
 229
 230
 231 let RE_CEXP_CX = prove_by_refinement(
 232   `!x. Re( cexp (ii * Cx x)) = cos x`,
 233   (* {{{ proof *)
 234   [
 235   REWRITE_TAC [ RE_CEXP; RE_MUL_II; IM_CX; IM_MUL_II; RE_CX ; REAL_ARITH `-- &0 = &0`; REAL_EXP_0; REAL_ARITH `&1 * x = x` ]
 236   ]);;
 237   (* }}} *)
 238
 239 let norm_normalize = prove_by_refinement(
 240  `! (v:real^N). ~(v = vec 0) ==> norm (normalize v) = &1 `,
 241 [
 242 (GEN_TAC THEN STRIP_TAC);
 243 (PURE_REWRITE_TAC[normalize;NORM_MUL;REAL_ABS_INV;REAL_ABS_NORM]);
 244 (MATCH_MP_TAC REAL_MUL_LINV);
 245 (ASM_MESON_TAC[NORM_EQ_0]);
 246 ]);;
 247
 248
 249 let RE_NORM_1 = prove_by_refinement(
 250   `!z. norm z = &1 ==> Re ( z ) = cos (Arg z)`,
 251   (* {{{ proof *)
 252   [
 253   REPEAT WEAK_STRIP_TAC;
 254   CONV_TAC (PATH_CONV "l" (ONCE_REWRITE_CONV[ARG]));
 255   ASM_REWRITE_TAC [ COMPLEX_MUL_LID ; RE_CEXP_CX]
 256   ]);;
 257   (* }}} *)
 258
 259 let COS_ARG_VECTOR_ANGLE = prove_by_refinement(
 260   `! u v. ~(u = Cx (&0)) /\ ~(v = Cx (&0)) ==> cos (Arg (u/v)) = cos (vector_angle u v)`,
 261   (* {{{ proof *)
 262   [
 263   REWRITE_TAC [ GSYM COMPLEX_VEC_0 ];
 264   REPEAT WEAK_STRIP_TAC;
 265   REWRITE_TAC [ COS_VECTOR_ANGLE];
 266   ASM_SIMP_TAC [ ];
 267   TYPIFY `(u dot v) / (norm u * norm v) = (normalize u dot normalize v)` (C SUBGOAL_THEN SUBST1_TAC);
 268     REWRITE_TAC [ normalize; DOT_LMUL; DOT_RMUL; real_div; REAL_INV_MUL ];
 269     BY(REAL_ARITH_TAC);
 270   SUBGOAL_THEN `~(u/v = Cx (&0))` ASSUME_TAC;
 271     BY(ASM_MESON_TAC [ COMPLEX_VEC_0; ARG_0_DIV ]);
 272   REWRITE_TAC [ DOT_RE ];
 273   TYPIFY `norm (normalize u) = &1 /\ norm (normalize v) = &1` (C SUBGOAL_THEN MP_TAC);
 274     BY(ASM_SIMP_TAC [norm_normalize]);
 275   REPEAT WEAK_STRIP_TAC;
 276   SUBGOAL_THEN ( `normalize u * cnj (normalize v) = normalize u/ normalize v`) SUBST1_TAC;
 277     ONCE_REWRITE_TAC [ COMPLEX_DIV_CNJ ];
 278     BY(ASM_REWRITE_TAC [ COMPLEX_DIV_1 ; COMPLEX_POW_ONE ]);
 279   TYPIFY `norm (normalize u / normalize v) = &1` (C SUBGOAL_THEN ASSUME_TAC);
 280     BY(ASM_REWRITE_TAC [ COMPLEX_NORM_DIV ; REAL_ARITH `&1 / &1 = &1`]);
 281   ASM_SIMP_TAC [RE_NORM_1];
 282   AP_TERM_TAC;
 283   REWRITE_TAC [ normalize; COMPLEX_CMUL ; complex_div ; REAL_INV_MUL; COMPLEX_INV_MUL; CX_INV; COMPLEX_INV_INV; GSYM COMPLEX_MUL_ASSOC];
 284   REWRITE_TAC [ GSYM CX_INV ];
 285   TYPIFY `&0 < inv (norm u) /\ &0 < norm v` (C SUBGOAL_THEN ASSUME_TAC);
 286     BY(CONJ_TAC THEN (TRY (MATCH_MP_TAC REAL_LT_INV)) THEN (ASM_SIMP_TAC [NORM_POS_LT]));
 287   ASM_SIMP_TAC [ ARG_MUL_CX ];
 288   CONV_TAC (PATH_CONV "rrl" (ONCE_REWRITE_CONV[ COMPLEX_MUL_SYM ]));
 289   ONCE_REWRITE_TAC [ COMPLEX_MUL_ASSOC ];
 290   CONV_TAC (PATH_CONV "rrl" (ONCE_REWRITE_CONV[ COMPLEX_MUL_SYM ]));
 291   REWRITE_TAC [ GSYM COMPLEX_MUL_ASSOC ];
 292   BY(ASM_SIMP_TAC [ ARG_MUL_CX ])
 293   ]);;
 294   (* }}} *)
 295
 296 let SEC_DOT = prove_by_refinement(
 297   `!u v r psi.
 298     &0 < r /\
 299     &0 <= psi /\ psi < pi / &2 /\
 300     norm (v) = r * inv(cos psi) /\
 301         norm (u) = r /\
 302     cos (vector_angle u v) = cos psi ==> (u dot (v - u) = &0)`  ,
 303   (* {{{ proof *)
 304   [
 305   REPEAT WEAK_STRIP_TAC;
 306   REWRITE_TAC [ DOT_RSUB];
 307   ASM_SIMP_TAC [ DOT_SQUARE_NORM ];
 308   ASM_SIMP_TAC [ VECTOR_ANGLE ];
 309   REWRITE_TAC [ GSYM REAL_MUL_ASSOC ];
 310   SUBGOAL_THEN `inv(cos psi) * cos psi = &1` SUBST1_TAC;
 311     MATCH_MP_TAC REAL_MUL_LINV;
 312     MATCH_MP_TAC (REAL_ARITH `&0 < x ==> ~(x = &0)`);
 313     MATCH_MP_TAC COS_POS_PI;
 314     MP_TAC PI_POS;
 315     BY (ASM_REAL_ARITH_TAC);
 316   BY (REAL_ARITH_TAC)
 317   ]);;
 318   (* }}} *)
 319
 320
 321
 322
 323
 324 (* YSSKQOY *)
 325
 326
 327 (* great study example. It is an obvious conseq. of
 328   Trigonometry1.ACS_ARCLENGTH, but a direct match doesn't work *)
 329
 330 let arclength2 = prove_by_refinement(
 331   `!h.  (&1 <= h /\ h <= h0) ==> arclength (&2) (&2 * h) (&2) = acs(h / &2)`,
 332   (* {{{ proof *)
 333   [
 334   REPEAT STRIP_TAC;
 335   MP_TAC (SPECL [`&2`;`&2 * h`;`&2`] Trigonometry1.ACS_ARCLENGTH);
 336   BRANCH_A [
 337     ANTS_TAC ;
 338     MP_TAC Sphere.h0;
 339     ASM_REAL_ARITH_TAC;
 340   ];
 341   DISCH_THEN SUBST1_TAC;
 342   AP_TERM_TAC;
 343   UNDISCH_TAC `&1 <= h`;
 344   BY (CONV_TAC REAL_FIELD);
 345   ]);;
 346   (* }}} *)
 347
 348
 349 let yssk_reduction = prove_by_refinement(
 350   `(!a1 a2 b1 b2. (&2 <= a1) /\ (a1 <= a2) /\ (a2 <= &2 * h0) /\
 351       (&2 <= b1 /\ b1 <= b2 /\ b2 <= &2 * h0) ==>
 352      (&0 <= arclength a2 b2 (&2) - arclength a1 b2 (&2) - arclength a2 b1 (&2) +
 353      arclength a1 b1 (&2))) ==>
 354     (!h h'. (&1 <= h) /\ (h <= h0) /\ (&1 <= h') /\ (h' <= h0) ==>
 355     acs (h/ &2) + acs (h'/ &2) - pi/ &3 <= arclength (&2 * h) (&2 * h') (&2))`,
 356   (* {{{ proof *)
 357   [
 358     REPEAT STRIP_TAC;
 359     FIRST_X_ASSUM (fun t -> MP_TAC(SPECL[`&2`;`&2 * h`;`&2`;`&2 * h'`] t));
 360     BRANCH_A [
 361       ANTS_TAC ;
 362       MP_TAC Sphere.h0;
 363       ASM_REAL_ARITH_TAC;
 364     ];
 365     MATCH_MP_TAC (REAL_ARITH ` (b = b') /\ (c = c') /\ (d = d') ==> ((&0 <= a - b - c +d) ==> c' + b' - d' <= a)`);
 366     SUBST1_TAC (SPECL[`&2 * h`;`&2`;`&2`] Arc_properties.arc_sym);
 367     ASM_SIMP_TAC [arclength2;Arc_properties.arc_sym;];
 368     MP_TAC (SPEC `&1` arclength2);
 369     BY(REWRITE_TAC[REAL_ARITH `&2 * &1 = &2`;Nonlinear_lemma.ACS_2;Sphere.h0;REAL_ARITH `&1 <= &1 /\ &1 <= #1.26`]);
 370 ]);;
 371   (* }}} *)
 372
 373  let TRI_UPS_X_STRICT_POS = prove
 374    (`!a b c. (&0 < a) /\ (&0 < b) /\ (&0 <= c) /\ (c < a + b) /\ (a < b + c) /\ (b < c + a) ==>
 375      &0 < ups_x (a * a) (b * b) (c * c)`,
 376     REPEAT STRIP_TAC THEN
 377       REWRITE_TAC [Trigonometry1.UPS_X_SQUARES] THEN
 378       BY(REPEAT (MATCH_MP_TAC REAL_LT_MUL ORELSE CONJ_TAC ORELSE
 379                 ASM_REAL_ARITH_TAC)));;
 380
 381  let ups_x_pos = prove_by_refinement(
 382   `!a b. &2 <= a /\ a <= #2.52 /\ &2 <= b /\ b <= #2.52 ==> &0 < ups_x (a pow 2) (b pow 2) (&4)`,
 383   (* {{{ proof *)
 384   [
 385     REPEAT STRIP_TAC;
 386     REWRITE_TAC[REAL_ARITH `&4 = &2 * &2 /\ a pow 2 = a*a`];
 387     MATCH_MP_TAC TRI_UPS_X_STRICT_POS;
 388     BY(ASM_REAL_ARITH_TAC);
 389   ]);;
 390   (* }}} *)
 391
 392 (*
 393   let expand_poly_tac = REWRITE_TAC[REAL_ADD_LDISTRIB;REAL_ADD_RDISTRIB;REAL_ARITH `-- -- x = x /\ -- (x + y ) = -- x - y /\ -- (x - y) = y - x /\ (a * b) * c = a * b * c /\ x - (u - v) = x + v - u /\ (x - y) - z = x - y - z /\ (x - y) * z = x * z - y * z /\ (-- (a * b) = (-- a) * b) /\ (a + b) + c = a + b + c /\ x*(y-z) = x * y - x * z `;REAL_POW_MUL];;
 394 *)
 395
 396
 397
 398 let arc_derivative = prove_by_refinement(
 399   `!a b.  (&2 <= a /\ a <= #2.52) /\ &2 <= b /\ b <= #2.52
 400          ==>( ((\x. arclength x b (&2)) has_real_derivative
 401               (-- (&4 + a pow 2 - b pow 2) / (a * sqrt(ups_x (a pow 2) (b pow 2) (&4)) )))
 402              (atreal a within real_interval [&2,#2.52]))`,
 403   (* {{{ proof *)
 404   [
 405     REPEAT STRIP_TAC;
 406     MP_TAC (SPECL [`a:real`;`b:real`] Arc_properties.arc_derivative);
 407     ASM_REWRITE_TAC[];
 408     FORCE_MATCH;
 409     BRANCH_A [
 410       (   SUBGOAL_THEN `(&0 < a) /\ (&0 < b) /\ &0 < ups_x (a pow 2) (b pow 2) (&4)` ASSUME_TAC) ;
 411       (   REPEAT (CONJ_TAC ORELSE MATCH_MP_TAC ups_x_pos ORELSE ASM_REAL_ARITH_TAC));
 412     ];
 413     SUBGOAL_THEN `(&1 - ((a * a + b * b - &2 * &2) / (&2 * a * b)) pow 2) = (inv (&2 * a * b)) pow 2 * (ups_x (a pow 2) (b pow 2) (&4)) ` SUBST1_TAC;
 414     REWRITE_TAC[Sphere.ups_x];
 415     FIRST_X_ASSUM MP_TAC;
 416     BY(CONV_TAC REAL_FIELD);
 417     BRANCH_A [
 418       SUBGOAL_THEN `((a + a) * &2 * a * b - (a * a + b * b - &2 * &2) * &2 * b) = ( &2 * b * (&4 + a pow 2 - b pow 2))` SUBST1_TAC;
 419       BY (   CONV_TAC REAL_FIELD);
 420     ];
 421     MP_TAC (SPECL[`inv(&2 * a * b)`;`ups_x (a pow 2) (b pow 2) (&4)`] (GSYM Trigonometry1.SQRT_MUL_L));
 422     BRANCH_A [
 423       ANTS_TAC;
 424       REWRITE_TAC[REAL_LE_INV_EQ] THEN
 425            BY(REPEAT (CONJ_TAC ORELSE MATCH_MP_TAC REAL_LE_MUL ORELSE ASM_REAL_ARITH_TAC));
 426     ];
 427     DISCH_THEN SUBST1_TAC;
 428     FIRST_X_ASSUM MP_TAC;
 429     BY(CONV_TAC REAL_FIELD);
 430   ]);;
 431   (* }}} *)
 432
 433 let arc_derivative2 = prove_by_refinement(
 434   `!a b.  (&2 <= a /\ a <= #2.52) /\ &2 <= b /\ b <= #2.52
 435   ==>( ((\x. -- (&4 + a pow 2 - x pow 2)/(a * sqrt(ups_x (a pow 2) (x pow 2) (&4))))
 436           has_real_derivative
 437               (&32 * a * b /( (sqrt (ups_x (a pow 2) (b pow 2) (&4))) pow 3)))
 438              (atreal b within real_interval [&2,#2.52]))`,
 439   (* {{{ proof *)
 440   [
 441     REPEAT STRIP_TAC;
 442     REWRITE_TAC[Sphere.ups_x];
 443     MP_TAC (REWRITE_RULE[Calc_derivative.derived_form] (Calc_derivative.differentiate `(\x. --(&4 + a pow 2 - x pow 2) /       (a *        sqrt        (--(a pow 2) * a pow 2 - x pow 2 * x pow 2 - &4 * &4 +         &2 * a pow 2 * &4 +         &2 * a pow 2 * x pow 2 +         &2 * x pow 2 * &4)))` `b:real` `real_interval [&2,#2.52]`));
 444     REWRITE_TAC[GSYM Sphere.ups_x];
 445     BRANCH_A [
 446       SUBGOAL_THEN `&0 < ups_x (a pow 2) (b pow 2) (&4) ` ASSUME_TAC;
 447       REWRITE_TAC[REAL_ARITH `a pow 2 = a * a /\ &4 = &2 * &2`];
 448       MATCH_MP_TAC TRI_UPS_X_STRICT_POS;
 449       BY(ASM_REAL_ARITH_TAC);
 450     ];
 451     ASM_REWRITE_TAC[REAL_ENTIRE;TAUT `~(a\/b) <=> ~a /\ ~b`];
 452     BRANCH_A [
 453       SUBGOAL_THEN `~(sqrt( ups_x (a pow 2) (b pow 2) (&4)) = &0) ` ASSUME_TAC;
 454       ASM_SIMP_TAC[SQRT_EQ_0;REAL_ARITH `&0 < u ==> &0 <= u`];
 455       BY(ASM_REAL_ARITH_TAC);
 456     ];
 457     ASM_REWRITE_TAC[];
 458     BRANCH_A [
 459       ANTS_TAC;
 460       (FIRST_X_ASSUM (fun t -> MP_TAC t THEN REAL_ARITH_TAC));
 461     ];
 462     FORCE_MATCH;
 463     ABBREV_TAC `c = ups_x (a pow 2) (b pow 2) (&4)`;
 464     Calc_derivative.CALC_ID_TAC;
 465     ASM_SIMP_TAC[REAL_ARITH `~(&2 = &0) /\ (&2 <= a ==> ~(a = &0))`];
 466     BRANCH_A [
 467       SUBGOAL_THEN `sqrt c pow 2 = ups_x (a pow 2) (b pow 2) (&4)` MP_TAC;
 468       EXPAND_TAC "c";
 469       MATCH_MP_TAC SQRT_POW_2;
 470       BY(ASM_MESON_TAC[REAL_ARITH `&0 < c ==> &0 <= c`])
 471     ];
 472     ABBREV_TAC `d = sqrt c`;
 473     REWRITE_TAC[Sphere.ups_x];
 474     BY(CONV_TAC REAL_RING);
 475   ]);;
 476   (* }}} *)
 477
 478 (* This is a good candidate for automation, long but trivial *)
 479
 480 let arc_length2_increasing = prove_by_refinement(
 481   `!a b1 b2.   (&2 <= a /\ a <= #2.52) /\ &2 <= b1 /\ b1 <= #2.52 /\ &2 <= b2 /\ b2 <= #2.52 /\ b1 <= b2 ==>
 482   let fa = (\x. -- (&4 + a pow 2 - x pow 2)/(a * sqrt(ups_x (a pow 2) (x pow 2) (&4))))  in
 483     (
 484       fa b1 <= fa b2
 485     )`,
 486   (* {{{ proof *)
 487   [
 488   REPEAT STRIP_TAC;
 489     LET_TAC;
 490     ABBREV_TAC `fa' =  \x. (&32 * a * x /( (sqrt (ups_x (a pow 2) (x pow 2) (&4))) pow 3))`;
 491   MP_TAC (SPECL[`fa:real->real`;`fa':real->real`;`b1:real`;`b2:real`] REAL_MVT_VERY_SIMPLE);
 492   ASM_REWRITE_TAC[IN_ELIM_THM;IN;];
 493   ANTS_TAC;
 494   REPEAT STRIP_TAC;
 495   MATCH_MP_TAC HAS_REAL_DERIVATIVE_WITHIN_SUBSET;
 496   EXISTS_TAC `real_interval [&2, #2.52]`;
 497   CONJ_TAC;
 498   EXPAND_TAC "fa";
 499   EXPAND_TAC "fa'";
 500   MATCH_MP_TAC arc_derivative2;
 501   REPEAT (POP_ASSUM MP_TAC) THEN REWRITE_TAC[real_interval;IN_ELIM_THM];
 502   REAL_ARITH_TAC;
 503   REWRITE_TAC[real_interval;SUBSET;IN_ELIM_THM];
 504   GEN_TAC;
 505   ASM_REAL_ARITH_TAC;
 506   REWRITE_TAC[real_interval;IN_ELIM_THM];
 507   REPEAT STRIP_TAC;
 508   ONCE_REWRITE_TAC[REAL_ARITH `(x <= y) = (&0 <= y - x)`];
 509   ASM_REWRITE_TAC[];
 510   MATCH_MP_TAC REAL_LE_MUL;
 511   CONJ_TAC THENL [ALL_TAC;ASM_MESON_TAC[REAL_ARITH `x <= y ==> &0 <= y -x`]];
 512   EXPAND_TAC "fa'";
 513   REWRITE_TAC [real_div];
 514   REPEAT ((MATCH_MP_TAC REAL_LE_MUL) ORELSE CONJ_TAC ORELSE ASM_REAL_ARITH_TAC);
 515   REWRITE_TAC[REAL_LE_INV_EQ];
 516   MATCH_MP_TAC REAL_POW_LE;
 517   MATCH_MP_TAC SQRT_POS_LE;
 518   REWRITE_TAC[REAL_ARITH `a pow 2 = a*a /\ &4 = &2 * &2`];
 519   MATCH_MP_TAC Trigonometry1.TRI_UPS_X_POS;
 520   ASM_REAL_ARITH_TAC;
 521   ]);;
 522   (* }}} *)
 523
 524 let arc_length1_increasing = prove_by_refinement(
 525   `!a1 a2 b1 b2. (&2 <= a1) /\ (a1 <= a2) /\ (a2 <= #2.52) /\
 526       (&2 <= b1 /\ b1 <= b2 /\ b2 <= #2.52) ==>
 527     (let f = \x. arclength x b2 (&2) - arclength x b1 (&2) in
 528     (f a1 <= f a2))`,
 529   (* {{{ proof *)
 530   [
 531   REPEAT STRIP_TAC;
 532     LET_TAC;
 533     ABBREV_TAC `fa = \b a.  (-- (&4 + a pow 2 - b pow 2) / (a * sqrt(ups_x (a pow 2) (b pow 2) (&4)) ))`;
 534     MP_TAC (SPECL [`f:real->real`;`\(a:real). (((fa:real->real->real) b2 a - fa b1 a):real)`;`a1:real`;`a2:real`] REAL_MVT_VERY_SIMPLE);
 535     ASM_REWRITE_TAC[IN;IN_ELIM_THM];
 536     (* BRANCH will go 3 deep *)
 537     ANTS_TAC;
 538     REPEAT STRIP_TAC;
 539   MATCH_MP_TAC HAS_REAL_DERIVATIVE_WITHIN_SUBSET;
 540   EXISTS_TAC `real_interval [&2, #2.52]`;
 541   CONJ_TAC;
 542   EXPAND_TAC "f";
 543     MATCH_MP_TAC HAS_REAL_DERIVATIVE_SUB;
 544     EXPAND_TAC "fa";
 545     CONJ_TAC THEN MATCH_MP_TAC arc_derivative THEN FIRST_X_ASSUM MP_TAC THEN REWRITE_TAC[IN_ELIM_THM;real_interval] THEN (ASM_REAL_ARITH_TAC);
 546     REWRITE_TAC[SUBSET;real_interval;IN_ELIM_THM];
 547     ASM_REAL_ARITH_TAC;
 548    REWRITE_TAC[SUBSET;real_interval;IN_ELIM_THM];
 549    REPEAT STRIP_TAC;
 550    ONCE_REWRITE_TAC[REAL_ARITH `x <= y <=> &0 <= y - x`];
 551    ASM_REWRITE_TAC[];
 552   MATCH_MP_TAC REAL_LE_MUL;
 553   CONJ_TAC THENL[ALL_TAC;UNDISCH_TAC `a1 <= a2` THEN REAL_ARITH_TAC];
 554   MP_TAC (SPECL[`x:real`;`b1:real`;`b2:real`] arc_length2_increasing);
 555   LET_TAC;
 556   EXPAND_TAC "fa'";
 557   EXPAND_TAC "fa";
 558   ANTS_TAC;
 559   ASM_REAL_ARITH_TAC;
 560  REAL_ARITH_TAC;
 561   ]);;
 562   (* }}} *)
 563
 564 let YSSKQOY= prove_by_refinement(
 565   `  (!h h'. (&1 <= h) /\ (h <= h0) /\ (&1 <= h') /\ (h' <= h0) ==>
 566     acs (h/ &2) + acs (h'/ &2) - pi/ &3 <= arclength (&2 * h) (&2 * h') (&2))`,
 567   (* {{{ proof *)
 568   [
 569     MATCH_MP_TAC yssk_reduction;
 570     REPEAT STRIP_TAC;
 571     MP_TAC (SPECL[`a1:real`;`a2:real`;`b1:real`;`b2:real` ] arc_length1_increasing);
 572     LET_TAC;
 573     EXPAND_TAC "f";
 574     ASM_REWRITE_TAC[];
 575     BRANCH_A [
 576       ANTS_TAC;
 577       MP_TAC Sphere.h0;
 578       ASM_REAL_ARITH_TAC;
 579     ];
 580     REAL_ARITH_TAC;
 581   ]);;
 582   (* }}} *)
 583
 584  end;;