text_formalization/local/lp_details.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (* Section: Conclusions                                                       *)
   4 (* Chapter: Tame (Linear Programs)                                            *)
   5 (* Author: Thomas C. Hales                                                    *)
   6 (* Date: 2013-06-19                                                           *)
   7 (* ========================================================================== *)
   8
   9 (*
  10 Treatment of two special inequalities for the linear programs.
  11
  12 The main results are
  13
  14 LEMMA_8673686234 (uses inequalities "6170936724","8673686234 a","8673686234 b","8673686234 c")
  15 see head.mod:yapex_sup_flat 'ID[8673686234]'
  16
  17 LEMMA_5691615370 (uses inequalities "5584033259","6170936724","5691615370")
  18 see head.mod:perimZ 'ID[5691615370]'
  19
  20 *)
  21
  22 module Lp_details = struct
  23
  24   open Hales_tactic;;
  25 (* start 867 *)
  26
  27 let quadratic_root_plus_disc = prove_by_refinement(
  28   `!a b c x. &0 < a /\ a * x pow 2 + b * x + c <= &0 ==>
  29    &0 <= b pow 2 - &4 * a * c`,
  30   (* {{{ proof *)
  31   [
  32   REPEAT WEAKER_STRIP_TAC;
  33   FIRST_X_ASSUM MP_TAC;
  34   TYPIFY `a * x pow 2 + b * x + c = a * (x + b /(&2 * a)) pow 2 - (b pow 2 - &4 * a*c)/(&4 * a)` (C SUBGOAL_THEN SUBST1_TAC);
  35     Calc_derivative.CALC_ID_TAC;
  36     BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC);
  37   ONCE_REWRITE_TAC[arith `u - v <= &0 <=> u <= v`];
  38   GMATCH_SIMP_TAC REAL_LE_RDIV_EQ;
  39   CONJ_TAC;
  40     BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC);
  41   TYPIFY `&0 <= (a * (x + b / (&2 * a)) pow 2) * &4 * a` ENOUGH_TO_SHOW_TAC;
  42     BY(REAL_ARITH_TAC);
  43   GMATCH_SIMP_TAC REAL_LE_MUL;
  44   CONJ_TAC;
  45     GMATCH_SIMP_TAC REAL_LE_MUL;
  46     ASM_REWRITE_TAC[REAL_LE_POW_2];
  47     BY(ASM_TAC THEN REAL_ARITH_TAC);
  48   BY(ASM_TAC THEN REAL_ARITH_TAC)
  49   ]);;
  50   (* }}} *)
  51
  52 let quadratic_root_exists = prove_by_refinement(
  53   `!a b c x. &0 < a /\  a * x pow 2 + b * x + c <= &0 ==>
  54     (?y. x <= y /\ a * y pow 2 + b *y + c = &0)`,
  55   (* {{{ proof *)
  56   [
  57   REPEAT WEAKER_STRIP_TAC;
  58   TYPED_ABBREV_TAC `(h:real) = quadratic_root_plus (a, b + &2 * a *x, a * x pow 2 + b * x + c)`;
  59   TYPIFY `x + h` EXISTS_TAC;
  60   REWRITE_TAC[arith `a * (x + h) pow 2 + b * (x + h) +c = a * h pow 2 + (b + &2 * a *x) * h + (a * x pow 2 + b * x + c)`];
  61   TYPIFY `(b + &2 * a * x) pow 2 <= (b + &2 * a * x) pow 2 - &4 * a * (a * x pow 2 + b * x + c)` (C SUBGOAL_THEN ASSUME_TAC);
  62     ONCE_REWRITE_TAC[arith `v <= v - &4 * a * x <=> &0 <= a * (-- x)`];
  63     GMATCH_SIMP_TAC REAL_LE_MUL;
  64     BY(ASM_TAC THEN REAL_ARITH_TAC);
  65   CONJ2_TAC;
  66     EXPAND_TAC "h";
  67     MATCH_MP_TAC (REWRITE_RULE[LET_DEF;LET_END_DEF] Tame_lemmas.quadratic_root_plus_works);
  68     CONJ_TAC;
  69       BY(ASM_TAC THEN REAL_ARITH_TAC);
  70     FIRST_X_ASSUM MP_TAC;
  71     BY(MESON_TAC[REAL_LE_TRANS;REAL_LE_POW_2]);
  72   MATCH_MP_TAC (arith `&0 <= h ==> x <= x + h`);
  73   EXPAND_TAC "h";
  74   REWRITE_TAC[Sphere.quadratic_root_plus];
  75   GMATCH_SIMP_TAC REAL_LE_RDIV_EQ;
  76   CONJ_TAC;
  77     BY(ASM_TAC THEN REAL_ARITH_TAC);
  78   ENOUGH_TO_SHOW_TAC `(b + &2 * a * x) <= sqrt((b + &2 * a*x) pow 2) /\ sqrt((b+ &2 * a*x) pow 2) <= sqrt((b + &2 * a * x) pow 2 - &4 * a * (a * x pow 2 + b * x + c))`;
  79     BY(REAL_ARITH_TAC);
  80   GMATCH_SIMP_TAC SQRT_MONO_LE_EQ;
  81   REWRITE_TAC[POW_2_SQRT_ABS];
  82   ASM_REWRITE_TAC[];
  83   CONJ2_TAC;
  84     BY(REAL_ARITH_TAC);
  85   SUBCONJ_TAC;
  86     BY(REWRITE_TAC[REAL_LE_POW_2]);
  87   BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC)
  88   ]);;
  89   (* }}} *)
  90
  91 let quadratic_root_pos_exists = prove_by_refinement(
  92   `!a b c x.  a < &0 /\  &0 <= a * x pow 2 + b * x + c ==>
  93     (?y. x <= y /\ a * y pow 2 + b *y + c = &0)`,
  94   (* {{{ proof *)
  95   [
  96   REPEAT WEAKER_STRIP_TAC;
  97   INTRO_TAC quadratic_root_exists [`--a`;`--b`;`--c`;`x`];
  98   ANTS_TAC;
  99     BY(ASM_TAC THEN REAL_ARITH_TAC);
 100   REPEAT WEAKER_STRIP_TAC;
 101   TYPIFY `y` EXISTS_TAC;
 102   BY(ASM_TAC THEN REAL_ARITH_TAC)
 103   ]);;
 104   (* }}} *)
 105
 106 let delta_x_root_exists = prove_by_refinement(
 107   `!x1 x2 x3 x4 x5 x6.
 108     &0 <= delta_x x1 x2 x3 x4 x5 x6 /\ &0 < x1 ==>
 109      (?x4'. x4 <= x4' /\ delta_x x1 x2 x3 x4' x5 x6 = &0)`,
 110   (* {{{ proof *)
 111   [
 112  REPEAT WEAKER_STRIP_TAC;
 113   TYPED_ABBREV_TAC  `b = ( delta_x4 x1 x2 x3 (&0) x5 x6)` ;
 114   TYPED_ABBREV_TAC  `c =  delta_x x1 x2 x3 (&0) x5 x6` ;
 115   TYPIFY `!z. delta_x x1 x2 x3 z x5 x6 = (-- x1) * z pow 2 + b * z + c` (C SUBGOAL_THEN ASSUME_TAC);
 116     EXPAND_TAC "c";
 117     EXPAND_TAC "b";
 118     REWRITE_TAC[Sphere.delta_x;Sphere.delta_x4];
 119     BY(REAL_ARITH_TAC);
 120   ASM_REWRITE_TAC[];
 121   MATCH_MP_TAC quadratic_root_pos_exists;
 122   FIRST_X_ASSUM ((unlist REWRITE_TAC) o GSYM);
 123   ASM_REWRITE_TAC[];
 124   BY(ASM_TAC THEN REAL_ARITH_TAC)
 125   ]);;
 126   (* }}} *)
 127
 128 let delta_y_root_exists = prove_by_refinement(
 129   `!y1 y2 y3 y4 y5 y6.
 130     &0 <= delta_y y1 y2 y3 y4 y5 y6 /\ &0 < y1 /\ &0 < y4 ==>
 131     (?y4'. y4 <= y4' /\ delta_y y1 y2 y3 y4' y5 y6 = &0)`,
 132   (* {{{ proof *)
 133   [
 134   REWRITE_TAC[Sphere.delta_y];
 135   REPEAT WEAKER_STRIP_TAC;
 136   INTRO_TAC delta_x_root_exists [`y1*y1`;`y2*y2`;`y3*y3`;`y4*y4`;`y5*y5`;`y6*y6`];
 137   ANTS_TAC;
 138     ASM_REWRITE_TAC[];
 139     GMATCH_SIMP_TAC REAL_LT_MUL_EQ;
 140     BY(ASM_REWRITE_TAC[]);
 141   REPEAT WEAKER_STRIP_TAC;
 142   TYPIFY `sqrt(x4')` EXISTS_TAC;
 143   TYPIFY `&0 <= x4'` (C SUBGOAL_THEN ASSUME_TAC);
 144     FIRST_X_ASSUM_ST `<=` MP_TAC;
 145     BY(MESON_TAC[REAL_LE_POW_2;REAL_LE_TRANS;arith `x*x = x pow 2`]);
 146   TYPIFY `sqrt(x4') * sqrt(x4') = x4'` (C SUBGOAL_THEN ASSUME_TAC);
 147     GMATCH_SIMP_TAC (GSYM SQRT_MUL);
 148     GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx;
 149     BY(ASM_REWRITE_TAC[]);
 150   ASM_REWRITE_TAC[];
 151   PROOF_BY_CONTR_TAC;
 152   FIRST_X_ASSUM_ST `y4 * y4 <= x4'` MP_TAC;
 153   FIRST_ASSUM_ST `(=)` (SUBST1_TAC o GSYM);
 154   REWRITE_TAC[arith `~(x <= y) <=> y < x`];
 155   MATCH_MP_TAC Misc_defs_and_lemmas.ABS_SQUARE;
 156   TYPIFY `&0 <= sqrt x4'` (C SUBGOAL_THEN ASSUME_TAC);
 157     GMATCH_SIMP_TAC SQRT_POS_LE;
 158     BY(ASM_REWRITE_TAC[]);
 159   BY(ASM_TAC THEN REAL_ARITH_TAC)
 160   ]);;
 161   (* }}} *)
 162
 163 let edge2_flatD_x1_quadratic_root_plus = prove_by_refinement(
 164   `!d x2 x3 x4 x5 x6.
 165     edge2_flatD_x1 d x2 x3 x4 x5 x6 =
 166     quadratic_root_plus(x4,
 167                         -- delta_x1 (&0) x2 x3 x4 x5 x6,
 168    d - delta_x (&0) x2 x3 x4 x5 x6 )`,
 169   (* {{{ proof *)
 170   [
 171   REWRITE_TAC[Nonlin_def.edge2_flatD_x1];
 172   REPEAT WEAKER_STRIP_TAC;
 173   TYPED_ABBREV_TAC `b = (-- delta_x1 (&0) x2 x3 x4 x5 x6)`;
 174   TYPED_ABBREV_TAC `c = (d - delta_x (&0) x2 x3 x4 x5 x6)`;
 175   TYPIFY `!z. d - delta_x z x2 x3 x4 x5 x6 = x4 * z pow 2 + b * z + c` ((C SUBGOAL_THEN ASSUME_TAC));
 176     EXPAND_TAC "c";
 177     EXPAND_TAC "b";
 178     REWRITE_TAC[Sphere.delta_x;Nonlin_def.delta_x1];
 179     BY(REAL_ARITH_TAC);
 180   ASM_REWRITE_TAC[Nonlinear_lemma.abc_quadratic];
 181   ]);;
 182   (* }}} *)
 183
 184 let edge2_flatD_x1_expanded = prove_by_refinement(
 185   `!d x2 x3 x4 x5 x6.
 186     edge2_flatD_x1 d x2 x3 x4 x5 x6 = (delta_x1 (&0) x2 x3 x4 x5 x6
 187     + sqrt (ups_x x2 x3 x4 * ups_x x4 x5 x6 - &4 * x4 * d)) / (&2 * x4)
 188     `,
 189   (* {{{ proof *)
 190   [
 191   REWRITE_TAC[edge2_flatD_x1_quadratic_root_plus];
 192   REPEAT WEAKER_STRIP_TAC;
 193   TYPED_ABBREV_TAC `b = (-- delta_x1 (&0) x2 x3 x4 x5 x6)`;
 194   TYPED_ABBREV_TAC `c = (d - delta_x (&0) x2 x3 x4 x5 x6)`;
 195   REWRITE_TAC[Sphere.quadratic_root_plus];
 196   TYPIFY `b pow 2 - &4 * x4 * c = ups_x x2 x3 x4 * ups_x x4 x5 x6 - &4 * x4 * d` (C SUBGOAL_THEN ASSUME_TAC);
 197     EXPAND_TAC "b";
 198     EXPAND_TAC "c";
 199     REWRITE_TAC[Sphere.delta_x;Nonlin_def.delta_x1;Sphere.ups_x];
 200     BY(REAL_ARITH_TAC);
 201   ASM_REWRITE_TAC[];
 202   EXPAND_TAC "b";
 203   BY(REAL_ARITH_TAC)
 204   ]);;
 205   (* }}} *)
 206
 207 let derived_form_edge2_flatD_x1 = prove_by_refinement(
 208   `!x2 x3 x4 x5 x6. (&0 < ups_x x2 x3 x4 /\ &0 < ups_x x4 x5 x6 /\ &0 < x4)
 209      ==> (?f'.
 210     derived_form T
 211     (\q. edge2_flatD_x1 (&0) q x3 x4 x5 x6) f' x2 (:real))`,
 212   (* {{{ proof *)
 213   [
 214   REPEAT WEAKER_STRIP_TAC;
 215   REWRITE_TAC[edge2_flatD_x1_expanded];
 216   REWRITE_TAC[Nonlin_def.delta_x1;Sphere.ups_x;arith `x - &4 * x4 * &0 = x`];
 217   TYPIFY `((((x5 - x6 + x4) +    (((--x2 + -- &1 * x2) + &2 * x4 + &2 * x3) *     (--x4 * x4 - x5 * x5 - x6 * x6 +      &2 * x4 * x6 +      &2 * x4 * x5 +      &2 * x5 * x6)) *    inv    (&2 *     sqrt     ((--x2 * x2 - x3 * x3 - x4 * x4 +       &2 * x2 * x4 +       &2 * x2 * x3 +       &2 * x3 * x4) *      (--x4 * x4 - x5 * x5 - x6 * x6 +       &2 * x4 * x6 +       &2 * x4 * x5 +       &2 * x5 * x6)))) *   &2 *   x4) /  (&2 * x4) pow 2)` EXISTS_TAC;
 218   Pent_hex.DERIVED_TAC MP_TAC;
 219   REWRITE_TAC[GSYM Sphere.ups_x];
 220   TYPIFY_GOAL_THEN `(&0 < ups_x x2 x3 x4 * ups_x x4 x5 x6 /\ ~(&2 = &0) /\ ~(x4 = &0))` (unlist REWRITE_TAC);
 221   REWRITE_TAC[REAL_OF_NUM_EQ];
 222   GMATCH_SIMP_TAC REAL_LT_MUL_EQ;
 223   ASM_REWRITE_TAC[];
 224   CONJ_TAC;
 225     BY(ARITH_TAC);
 226   BY(ASM_TAC THEN REAL_ARITH_TAC)
 227   ]);;
 228   (* }}} *)
 229
 230 let edge2_flatD_x1_continuous = prove_by_refinement(
 231   `!x2 x3 x4 x5 x6. (&0 < ups_x x2 x3 x4 /\ &0 < ups_x x4 x5 x6 /\ &0 < x4 ==>
 232    (\q. edge2_flatD_x1 (&0) q x3 x4 x5 x6) real_continuous atreal x2)`,
 233   (* {{{ proof *)
 234   [
 235   REPEAT WEAKER_STRIP_TAC;
 236   MATCH_MP_TAC HAS_REAL_DERIVATIVE_IMP_CONTINUOUS_ATREAL;
 237   INTRO_TAC derived_form_edge2_flatD_x1 [`x2`;`x3`;`x4`;`x5`;`x6`];
 238   BY(ASM_REWRITE_TAC[Calc_derivative.derived_form;WITHINREAL_UNIV])
 239   ]);;
 240   (* }}} *)
 241
 242 let IVT_edge2_flatD_x1 = prove_by_refinement(
 243   `!x1m x1M x2m x2M x3 x4 x5 x6.
 244     (!x2. x2m <= x2 /\ x2 <= x2M ==> &0 < ups_x x2 x3 x4) /\
 245     (&0 < ups_x x4 x5 x6) /\
 246     (&0 < x4) /\
 247     (x1m <= x1M) /\
 248     (x2m <= x2M) /\
 249     (delta_x x1M x2M x3 x4 x5 x6 = &0) /\
 250     (!x1 x2. x1m <= x1 /\ x1 <= x1M /\ x2m <= x2 /\ x2 <= x2M ==>
 251        delta_x1 x1 x2 x3 x4 x5 x6 < &0) ==>
 252     ((?x2. x2m <= x2 /\ x2 <= x2M /\ edge2_flatD_x1 (&0) x2 x3 x4 x5 x6 = x1m) \/
 253        (x1m < edge2_flatD_x1 (&0) x2m x3 x4 x5 x6))`,
 254   (* {{{ proof *)
 255   [
 256   REPEAT WEAKER_STRIP_TAC;
 257   TYPIFY `!x2. x2m <= x2 /\ x2 <= x2M ==> x1m < edge2_flatD_x1 (&0) x2 x3 x4 x5 x6` ASM_CASES_TAC;
 258     FIRST_X_ASSUM (C INTRO_TAC [`x2m`]);
 259     ASM_REWRITE_TAC[arith `x <= x`];
 260     BY(MESON_TAC[]);
 261   FIRST_X_ASSUM MP_TAC;
 262   REWRITE_TAC[NOT_FORALL_THM];
 263   REPEAT WEAKER_STRIP_TAC;
 264   FIRST_X_ASSUM MP_TAC;
 265   REWRITE_TAC[TAUT `~(a ==> b) <=> (a /\ ~b)`];
 266   REWRITE_TAC[arith `~(x < b) <=> b <= x`];
 267   REPEAT WEAKER_STRIP_TAC;
 268   DISJ1_TAC;
 269   INTRO_TAC REAL_IVT_INCREASING [`(\q. edge2_flatD_x1 (&0) q x3 x4 x5 x6)`;`x2`;`x2M`;`x1m`];
 270   ANTS_TAC;
 271     ASM_REWRITE_TAC[];
 272     CONJ2_TAC;
 273       ENOUGH_TO_SHOW_TAC `edge2_flatD_x1 (&0) x2M x3 x4 x5 x6 = x1M`;
 274         BY(ASM_TAC THEN REAL_ARITH_TAC);
 275       MATCH_MP_TAC Pent_hex.edge2_flatD_x1_delta_lemma2;
 276       ASM_REWRITE_TAC[];
 277       FIRST_X_ASSUM MATCH_MP_TAC;
 278       BY(ASM_TAC THEN REAL_ARITH_TAC);
 279     REWRITE_TAC[REAL_CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN];
 280     REWRITE_TAC[IN_REAL_INTERVAL];
 281     REPEAT WEAKER_STRIP_TAC;
 282     MATCH_MP_TAC REAL_CONTINUOUS_ATREAL_WITHINREAL;
 283     MATCH_MP_TAC edge2_flatD_x1_continuous;
 284     ASM_REWRITE_TAC[];
 285     FIRST_X_ASSUM MATCH_MP_TAC;
 286     ASM_REWRITE_TAC[];
 287     BY(ASM_TAC THEN REAL_ARITH_TAC);
 288   REWRITE_TAC[IN_REAL_INTERVAL];
 289   REPEAT WEAKER_STRIP_TAC;
 290   TYPIFY `x` EXISTS_TAC;
 291   ASM_REWRITE_TAC[];
 292   BY(ASM_TAC THEN REAL_ARITH_TAC)
 293   ]);;
 294   (* }}} *)
 295
 296 let edge2_flatD_x1_works = prove_by_refinement(
 297   `!x2 x3 x4 x5 x6.
 298   &0 <= ups_x x2 x3 x4 /\ &0 <= ups_x x4 x5 x6 /\ ~(x4 = &0) ==>
 299     delta_x (edge2_flatD_x1 (&0) x2 x3 x4 x5 x6) x2 x3 x4 x5 x6 = &0`,
 300   (* {{{ proof *)
 301   [
 302   REPEAT WEAKER_STRIP_TAC;
 303   REWRITE_TAC[edge2_flatD_x1_quadratic_root_plus];
 304   TYPED_ABBREV_TAC `b = (-- delta_x1 (&0) x2 x3 x4 x5 x6)`;
 305   TYPED_ABBREV_TAC `c = (&0 - delta_x (&0) x2 x3 x4 x5 x6)`;
 306   ONCE_REWRITE_TAC[arith `d = &0 <=> &0 - d = &0`];
 307   TYPIFY `!z. &0 - delta_x z x2 x3 x4 x5 x6 = x4 * z pow 2 + b * z + c` ((C SUBGOAL_THEN ASSUME_TAC));
 308     EXPAND_TAC "c";
 309     EXPAND_TAC "b";
 310     REWRITE_TAC[Sphere.delta_x;Nonlin_def.delta_x1];
 311     BY(REAL_ARITH_TAC);
 312   ASM_REWRITE_TAC[];
 313   MATCH_MP_TAC (REWRITE_RULE[LET_DEF;LET_END_DEF] Tame_lemmas.quadratic_root_plus_works);
 314   TYPIFY `b pow 2 - &4 * x4 * c = ups_x x2 x3 x4 * ups_x x4 x5 x6 ` (C SUBGOAL_THEN ASSUME_TAC);
 315     EXPAND_TAC "b";
 316     EXPAND_TAC "c";
 317     REWRITE_TAC[Sphere.delta_x;Nonlin_def.delta_x1;Sphere.ups_x];
 318     BY(REAL_ARITH_TAC);
 319   ASM_REWRITE_TAC[];
 320   GMATCH_SIMP_TAC REAL_LE_MUL;
 321   BY(ASM_REWRITE_TAC[])
 322   ]);;
 323   (* }}} *)
 324
 325 let delta_x1_decreasing = prove_by_refinement(
 326   `!x1 x2 x3 x4 x5 x6 x1'.
 327     x1 <= x1' /\ &0 <= x4 ==>
 328     delta_x1 x1' x2 x3 x4 x5 x6 <= delta_x1 x1 x2 x3 x4 x5 x6`,
 329   (* {{{ proof *)
 330   [
 331   REPEAT WEAKER_STRIP_TAC;
 332   ENOUGH_TO_SHOW_TAC `delta_x1 x1 x2 x3 x4 x5 x6 - delta_x1 x1' x2 x3 x4 x5 x6 = &2 * x4 * (x1' - x1)`;
 333     ONCE_REWRITE_TAC[arith `d' <= d <=> &0 <= d - d'`];
 334     DISCH_THEN SUBST1_TAC;
 335     GMATCH_SIMP_TAC REAL_LE_MUL;
 336     CONJ_TAC;
 337       BY(REAL_ARITH_TAC);
 338     GMATCH_SIMP_TAC REAL_LE_MUL;
 339     BY(ASM_TAC THEN REAL_ARITH_TAC);
 340   REWRITE_TAC[Nonlin_def.delta_x1];
 341   BY(REAL_ARITH_TAC)
 342   ]);;
 343   (* }}} *)
 344
 345 let IVT_delta_x = prove_by_refinement(
 346   `!x1m x1M x2m x2M x3 x4 x5 x6.
 347          (!x2. x2m <= x2 /\ x2 <= x2M ==> &0 < ups_x x2 x3 x4) /\
 348          &0 < ups_x x4 x5 x6 /\
 349          &0 < x4 /\
 350          x1m <= x1M /\
 351          x2m <= x2M /\
 352          delta_x x1M x2M x3 x4 x5 x6 = &0 /\
 353          (!x2. x2m <= x2 /\ x2 <= x2M
 354               ==> delta_x1 x1m x2 x3 x4 x5 x6 < &0)
 355          ==> (?x2. x2m <= x2 /\
 356                    x2 <= x2M /\ delta_x x1m x2 x3 x4 x5 x6 = &0) \/
 357              (?x1. x1m < x1 /\ delta_x x1 x2m x3 x4 x5 x6 = &0)`,
 358   (* {{{ proof *)
 359   [
 360   REPEAT WEAKER_STRIP_TAC;
 361   INTRO_TAC IVT_edge2_flatD_x1 [`x1m`;`x1M`;`x2m`;`x2M`;`x3`;`x4`;`x5`;`x6`];
 362   ANTS_TAC;
 363     (ASM_REWRITE_TAC[]);
 364     REPEAT WEAKER_STRIP_TAC;
 365     ENOUGH_TO_SHOW_TAC `delta_x1 x1 x2 x3 x4 x5 x6 <= delta_x1 x1m x2 x3 x4 x5 x6`;
 366       MATCH_MP_TAC (arith `x < &0 ==> (y <= x ==> y< &0)`);
 367       FIRST_X_ASSUM MATCH_MP_TAC;
 368       BY(ASM_REWRITE_TAC[]);
 369     MATCH_MP_TAC delta_x1_decreasing;
 370     BY(ASM_SIMP_TAC[arith `&0 < x ==> &0 <= x`]);
 371   STRIP_TAC;
 372     DISJ1_TAC;
 373     TYPIFY `x2` EXISTS_TAC;
 374     ASM_REWRITE_TAC[];
 375     EXPAND_TAC "x1m";
 376     MATCH_MP_TAC edge2_flatD_x1_works;
 377     BY(ASM_SIMP_TAC[arith `x < y ==> x <= y`;arith `&0 < x ==> ~(x = &0)`]);
 378   DISJ2_TAC;
 379   TYPIFY `edge2_flatD_x1 (&0) x2m x3 x4 x5 x6` EXISTS_TAC;
 380   ASM_REWRITE_TAC[];
 381   MATCH_MP_TAC edge2_flatD_x1_works;
 382   ASM_SIMP_TAC[arith `x < y ==> x <= y`;arith `&0 < x ==> ~(x = &0)`];
 383   MATCH_MP_TAC (arith `x < y ==> x <= y`);
 384   FIRST_X_ASSUM MATCH_MP_TAC;
 385   BY(ASM_TAC THEN REAL_ARITH_TAC)
 386   ]);;
 387   (* }}} *)
 388
 389 let delta_x1_sym = prove_by_refinement(
 390   `!x1 x2 x3 x4 x5 x6.
 391      delta_x1 x1 x3 x2 x4 x6 x5 = delta_x1 x1 x2 x3 x4 x5 x6 /\
 392     delta_x1 x1 x5 x6 x4 x2 x3 = delta_x1 x1 x2 x3 x4 x5 x6`,
 393   (* {{{ proof *)
 394   [
 395   REWRITE_TAC[Nonlin_def.delta_x1];
 396   BY(REAL_ARITH_TAC)
 397   ]);;
 398   (* }}} *)
 399
 400 let IVT_delta_x_3 = prove_by_refinement(
 401   `!x1m x1M x2 x3m x3M x4 x5 x6.
 402          (!x3. x3m <= x3 /\ x3 <= x3M ==> &0 < ups_x x2 x3 x4) /\
 403          &0 < ups_x x4 x5 x6 /\
 404          &0 < x4 /\
 405          x1m <= x1M /\
 406          x3m <= x3M /\
 407          delta_x x1M x2 x3M x4 x5 x6 = &0 /\
 408          (!x3. x3m <= x3 /\ x3 <= x3M
 409               ==> delta_x1 x1m x2 x3 x4 x5 x6 < &0)
 410          ==> (?x3. x3m <= x3 /\
 411                    x3 <= x3M /\ delta_x x1m x2 x3 x4 x5 x6 = &0) \/
 412              (?x1. x1m < x1 /\ delta_x x1 x2 x3m x4 x5 x6 = &0)`,
 413   (* {{{ proof *)
 414   [
 415   REPEAT WEAKER_STRIP_TAC;
 416   INTRO_TAC IVT_delta_x [`x1m`;`x1M`;`x3m`;`x3M`;`x2`;`x4`;`x6`;`x5`];
 417   ASM_REWRITE_TAC[];
 418   ANTS_TAC;
 419     CONJ_TAC;
 420       REPEAT WEAKER_STRIP_TAC;
 421       ONCE_REWRITE_TAC[Merge_ineq.ups_x_sym];
 422       FIRST_X_ASSUM MATCH_MP_TAC;
 423       BY(ASM_REWRITE_TAC[]);
 424     CONJ_TAC;
 425       FIRST_X_ASSUM_ST `ups_x` MP_TAC;
 426       BY(MESON_TAC[Collect_geom.UPS_X_SYM]);
 427     CONJ_TAC;
 428       BY(ASM_MESON_TAC[Merge_ineq.delta_x_sym]);
 429     BY(ASM_MESON_TAC[delta_x1_sym]);
 430   BY(MESON_TAC[Merge_ineq.delta_x_sym])
 431   ]);;
 432   (* }}} *)
 433
 434 let IVT_delta_x_5 = prove_by_refinement(
 435   `!x1m x1M x2 x3 x4 x5m x5M x6.
 436          (!x5. x5m <= x5 /\ x5 <= x5M ==> &0 < ups_x x4 x5 x6) /\
 437          &0 < ups_x x2 x3 x4 /\
 438          &0 < x4 /\
 439          x1m <= x1M /\
 440          x5m <= x5M /\
 441          delta_x x1M x2 x3 x4 x5M x6 = &0 /\
 442          (!x5. x5m <= x5 /\ x5 <= x5M
 443               ==> delta_x1 x1m x2 x3 x4 x5 x6 < &0)
 444          ==> (?x5. x5m <= x5 /\
 445                    x5 <= x5M /\ delta_x x1m x2 x3 x4 x5 x6 = &0) \/
 446              (?x1. x1m < x1 /\ delta_x x1 x2 x3 x4 x5m x6 = &0)`,
 447   (* {{{ proof *)
 448   [
 449   REPEAT WEAKER_STRIP_TAC;
 450   INTRO_TAC IVT_delta_x [`x1m`;`x1M`;`x5m`;`x5M`;`x6`;`x4`;`x2`;`x3`];
 451   ASM_REWRITE_TAC[];
 452   ANTS_TAC;
 453     CONJ_TAC;
 454       REPEAT WEAKER_STRIP_TAC;
 455       BY(ASM_MESON_TAC[Collect_geom.UPS_X_SYM]);
 456     CONJ_TAC;
 457       BY(ASM_MESON_TAC[Collect_geom.UPS_X_SYM]);
 458     CONJ_TAC;
 459       BY(ASM_MESON_TAC[Merge_ineq.delta_x_sym]);
 460     BY(ASM_MESON_TAC[delta_x1_sym]);
 461   BY(MESON_TAC[Merge_ineq.delta_x_sym])
 462   ]);;
 463   (* }}} *)
 464
 465 let IVT_delta_x_6 = prove_by_refinement(
 466   `!x1m x1M x2 x3 x4 x5 x6m x6M.
 467          (!x6. x6m <= x6 /\ x6 <= x6M ==> &0 < ups_x x4 x5 x6) /\
 468          &0 < ups_x x2 x3 x4 /\
 469          &0 < x4 /\
 470          x1m <= x1M /\
 471          x6m <= x6M /\
 472          delta_x x1M x2 x3 x4 x5 x6M = &0 /\
 473          (!x6. x6m <= x6 /\ x6 <= x6M
 474               ==> delta_x1 x1m x2 x3 x4 x5 x6 < &0)
 475          ==> (?x6. x6m <= x6 /\
 476                    x6 <= x6M /\ delta_x x1m x2 x3 x4 x5 x6 = &0) \/
 477              (?x1. x1m < x1 /\ delta_x x1 x2 x3 x4 x5 x6m = &0)`,
 478   (* {{{ proof *)
 479   [
 480   REPEAT WEAKER_STRIP_TAC;
 481   INTRO_TAC IVT_delta_x [`x1m`;`x1M`;`x6m`;`x6M`;`x5`;`x4`;`x3`;`x2`];
 482   ASM_REWRITE_TAC[];
 483   ANTS_TAC;
 484     CONJ_TAC;
 485       REPEAT WEAKER_STRIP_TAC;
 486       BY(ASM_MESON_TAC[Collect_geom.UPS_X_SYM]);
 487     CONJ_TAC;
 488       BY(ASM_MESON_TAC[Collect_geom.UPS_X_SYM]);
 489     CONJ_TAC;
 490       BY(ASM_MESON_TAC[Merge_ineq.delta_x_sym]);
 491     BY(ASM_MESON_TAC[delta_x1_sym]);
 492   BY(MESON_TAC[Merge_ineq.delta_x_sym])
 493   ]);;
 494   (* }}} *)
 495
 496 let IVT_delta_x_full = prove_by_refinement(
 497   `!x1m x1M x2m x2M x3m x3M x4 x5m x5M x6m x6M.
 498     &0 < x4 /\
 499     (!x2 x3. x2m <= x2 /\ x2 <= x2M /\ x3m <= x3 /\ x3 <= x3M ==> &0 < ups_x x2 x3 x4) /\
 500     (!x5 x6. x5m <= x5 /\ x5 <= x5M /\ x6m <= x6 /\ x6 <= x6M ==> &0 < ups_x x4 x5 x6) /\
 501     x1m <= x1M /\ x2m <= x2M /\ x3m <= x3M /\ x5m <= x5M /\ x6m <= x6M /\
 502     delta_x x1M x2M x3M x4 x5M x6M = &0 /\
 503     (! x2 x3 x5 x6.
 504        x2m <= x2 /\ x2 <= x2M /\ x3m <= x3 /\ x3 <= x3M /\
 505        x5m <= x5 /\ x5 <= x5M /\ x6m <= x6 /\ x6 <= x6M ==>
 506        delta_x1 x1m x2 x3 x4 x5 x6 < &0) ==>
 507     (?x2 x3 x5 x6. x2m <= x2 /\ x2 <= x2M /\ x3m <= x3 /\ x3 <= x3M /\
 508        x5m <= x5 /\ x5 <= x5M /\ x6m <= x6 /\ x6 <= x6M /\
 509        delta_x x1m x2 x3 x4 x5 x6 = &0) \/
 510     (?x1. x1m < x1 /\ delta_x x1 x2m x3m x4 x5m x6m = &0)
 511 `,
 512   (* {{{ proof *)
 513   [
 514   REPEAT WEAKER_STRIP_TAC;
 515   PROOF_BY_CONTR_TAC;
 516   RULE_ASSUM_TAC (REWRITE_RULE[DE_MORGAN_THM;NOT_EXISTS_THM;TAUT `~(a /\ b) <=> a ==> ~b`;TAUT `a ==> b ==> c <=> (a /\ b) ==> c`]);
 517   FIRST_X_ASSUM MP_TAC;
 518   REPEAT WEAKER_STRIP_TAC;
 519   INTRO_TAC IVT_delta_x [`x1m`;`x1M`;`x2m`;`x2M`;`x3M`;`x4`;`x5M`;`x6M`];
 520   ANTS_TAC;
 521     ASM_REWRITE_TAC[];
 522     CONJ_TAC;
 523       REPEAT WEAKER_STRIP_TAC;
 524       FIRST_X_ASSUM MATCH_MP_TAC;
 525       BY(ASM_REWRITE_TAC[arith `x <= x`]);
 526     CONJ_TAC;
 527       FIRST_X_ASSUM MATCH_MP_TAC;
 528       BY(ASM_REWRITE_TAC[arith `x <= x`]);
 529     REPEAT WEAKER_STRIP_TAC;
 530     FIRST_X_ASSUM MATCH_MP_TAC;
 531     BY(ASM_REWRITE_TAC[arith `x <= x`]);
 532   STRIP_TAC;
 533     FIRST_X_ASSUM MP_TAC;
 534     REWRITE_TAC[];
 535     FIRST_X_ASSUM MATCH_MP_TAC;
 536     BY(ASM_REWRITE_TAC[arith `x <= x`]);
 537   INTRO_TAC IVT_delta_x_3 [`x1m`;`x1`;`x2m`;`x3m`;`x3M`;`x4`;`x5M`;`x6M`];
 538   ASM_REWRITE_TAC[];
 539   DISCH_THEN MP_TAC THEN ANTS_TAC;
 540     CONJ_TAC;
 541       REPEAT WEAKER_STRIP_TAC;
 542       FIRST_X_ASSUM MATCH_MP_TAC;
 543       BY(ASM_REWRITE_TAC[arith `x <= x`]);
 544     CONJ_TAC;
 545       FIRST_X_ASSUM MATCH_MP_TAC;
 546       BY(ASM_REWRITE_TAC[arith `x <= x`]);
 547     CONJ_TAC;
 548       BY(FIRST_X_ASSUM_ST `<` MP_TAC THEN REAL_ARITH_TAC);
 549     REPEAT WEAKER_STRIP_TAC;
 550     FIRST_X_ASSUM MATCH_MP_TAC;
 551     BY(ASM_REWRITE_TAC[arith `x <= x`]);
 552   STRIP_TAC;
 553     FIRST_X_ASSUM MP_TAC;
 554     REWRITE_TAC[];
 555     FIRST_X_ASSUM MATCH_MP_TAC;
 556     BY(ASM_REWRITE_TAC[arith `x <= x`]);
 557   INTRO_TAC IVT_delta_x_5 [`x1m`;`x1'`;`x2m`;`x3m`;`x4`;`x5m`;`x5M`;`x6M`];
 558   ASM_REWRITE_TAC[];
 559   DISCH_THEN MP_TAC THEN ANTS_TAC;
 560     CONJ_TAC;
 561       REPEAT WEAKER_STRIP_TAC;
 562       FIRST_X_ASSUM MATCH_MP_TAC;
 563       BY(ASM_REWRITE_TAC[arith `x <= x`]);
 564     CONJ_TAC;
 565       FIRST_X_ASSUM MATCH_MP_TAC;
 566       BY(ASM_REWRITE_TAC[arith `x <= x`]);
 567     CONJ_TAC;
 568       BY(REPLICATE_TAC 2 (FIRST_X_ASSUM_ST `<` MP_TAC) THEN REAL_ARITH_TAC);
 569     REPEAT WEAKER_STRIP_TAC;
 570     FIRST_X_ASSUM MATCH_MP_TAC;
 571     BY(ASM_REWRITE_TAC[arith `x <= x`]);
 572   STRIP_TAC;
 573     FIRST_X_ASSUM MP_TAC;
 574     REWRITE_TAC[];
 575     FIRST_X_ASSUM MATCH_MP_TAC;
 576     BY(ASM_REWRITE_TAC[arith `x <= x`]);
 577   INTRO_TAC IVT_delta_x_6 [`x1m`;`x1''`;`x2m`;`x3m`;`x4`;`x5m`;`x6m`;`x6M`];
 578   ASM_REWRITE_TAC[];
 579   DISCH_THEN MP_TAC THEN ANTS_TAC;
 580     CONJ_TAC;
 581       REPEAT WEAKER_STRIP_TAC;
 582       FIRST_X_ASSUM MATCH_MP_TAC;
 583       BY(ASM_REWRITE_TAC[arith `x <= x`]);
 584     CONJ_TAC;
 585       FIRST_X_ASSUM MATCH_MP_TAC;
 586       BY(ASM_REWRITE_TAC[arith `x <= x`]);
 587     CONJ_TAC;
 588       BY(REPLICATE_TAC 3 (FIRST_X_ASSUM_ST `<` MP_TAC) THEN REAL_ARITH_TAC);
 589     REPEAT WEAKER_STRIP_TAC;
 590     FIRST_X_ASSUM MATCH_MP_TAC;
 591     BY(ASM_REWRITE_TAC[arith `x <= x`]);
 592   STRIP_TAC;
 593     FIRST_X_ASSUM MP_TAC;
 594     REWRITE_TAC[];
 595     FIRST_X_ASSUM MATCH_MP_TAC;
 596     BY(ASM_REWRITE_TAC[arith `x <= x`]);
 597   FIRST_X_ASSUM MP_TAC;
 598   REWRITE_TAC[];
 599   FIRST_X_ASSUM MATCH_MP_TAC;
 600   BY(REPLICATE_TAC 4 (FIRST_X_ASSUM_ST `<` MP_TAC) THEN REAL_ARITH_TAC)
 601   ]);;
 602   (* }}} *)
 603
 604 let FORALL_BIJ_SQUARE = prove_by_refinement(
 605   `!P ym yM. &0 <= ym /\ &0 <= yM ==>
 606     ((!x. ym*ym <= x /\ x <= yM*yM ==> P x) <=>
 607     (!y. ym <= y /\ y <= yM ==> P (y*y)))`,
 608   (* {{{ proof *)
 609   [
 610   REPEAT WEAKER_STRIP_TAC;
 611   MATCH_MP_TAC (TAUT `(a ==> b) /\ (b ==> a) ==> (a <=> b)`);
 612   CONJ_TAC;
 613     REPEAT WEAKER_STRIP_TAC;
 614     FIRST_X_ASSUM MATCH_MP_TAC;
 615     GMATCH_SIMP_TAC Misc_defs_and_lemmas.ABS_SQUARE_LE;
 616     GMATCH_SIMP_TAC Misc_defs_and_lemmas.ABS_SQUARE_LE;
 617     BY(ASM_TAC THEN REAL_ARITH_TAC);
 618   REPEAT WEAKER_STRIP_TAC;
 619   TYPIFY `&0 <= x` (C SUBGOAL_THEN ASSUME_TAC);
 620     FIRST_X_ASSUM_ST `y*y <= x` MP_TAC;
 621     BY(MESON_TAC[REAL_LE_POW_2;arith `x*x = x pow 2`;REAL_LE_TRANS]);
 622   REPLICATE_TAC 2 (FIRST_X_ASSUM_ST `*` MP_TAC);
 623   TYPIFY_GOAL_THEN `x = sqrt x * sqrt x` (unlist ONCE_REWRITE_TAC);
 624     GMATCH_SIMP_TAC (GSYM SQRT_MUL);
 625     GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx;
 626     BY(ASM_REWRITE_TAC[]);
 627   ASM_REWRITE_TAC[arith `x * x = x pow 2`];
 628   GMATCH_SIMP_TAC (GSYM Trigonometry2.POW2_COND);
 629   GMATCH_SIMP_TAC (GSYM Trigonometry2.POW2_COND);
 630   ASM_REWRITE_TAC[];
 631   GMATCH_SIMP_TAC SQRT_POS_LE;
 632   ASM_REWRITE_TAC[];
 633   REWRITE_TAC[arith `x pow 2 = x*x`];
 634   REPEAT WEAKER_STRIP_TAC;
 635   FIRST_X_ASSUM MATCH_MP_TAC;
 636   BY(ASM_REWRITE_TAC[])
 637   ]);;
 638   (* }}} *)
 639
 640 let EXISTS_BIJ_SQUARE = prove_by_refinement(
 641   `!P ym yM. &0 <= ym /\ &0 <= yM ==>
 642     ((?x. ym*ym <= x /\ x <= yM*yM /\ P x) <=>
 643     (?y. ym <= y /\ y <= yM /\ P (y*y)))`,
 644   (* {{{ proof *)
 645   [
 646   REPEAT WEAKER_STRIP_TAC;
 647   ONCE_REWRITE_TAC[TAUT `(a <=> b) <=> (~a <=> ~b)`];
 648   REWRITE_TAC[NOT_EXISTS_THM;DE_MORGAN_THM];
 649   REWRITE_TAC[TAUT `~a \/ ~b \/ ~c <=> (a /\ b ==> ~c)`];
 650   MATCH_MP_TAC FORALL_BIJ_SQUARE;
 651   BY(ASM_REWRITE_TAC[])
 652   ]);;
 653   (* }}} *)
 654
 655 let IVT_delta_y_full = prove_by_refinement(
 656   `!y1m y1M y2m y2M y3m y3M y4 y5m y5M y6m y6M.
 657     &0 < y4 /\
 658     &0 <= y1m /\ &0 <= y2m /\ &0 <= y3m /\ &0 <= y5m /\ &0 <= y6m /\
 659     (!y2 y3. y2m <= y2 /\ y2 <= y2M /\ y3m <= y3 /\ y3 <= y3M ==> &0 < ups_x (y2*y2) (y3*y3) (y4*y4)) /\
 660     (!y5 y6. y5m <= y5 /\ y5 <= y5M /\ y6m <= y6 /\ y6 <= y6M ==> &0 < ups_x (y4*y4) (y5*y5) (y6*y6)) /\
 661     y1m <= y1M /\ y2m <= y2M /\ y3m <= y3M /\ y5m <= y5M /\ y6m <= y6M /\
 662     delta_y y1M y2M y3M y4 y5M y6M = &0 /\
 663     (! y2 y3 y5 y6.
 664        y2m <= y2 /\ y2 <= y2M /\ y3m <= y3 /\ y3 <= y3M /\
 665        y5m <= y5 /\ y5 <= y5M /\ y6m <= y6 /\ y6 <= y6M ==>
 666        y_of_x delta_x1 y1m y2 y3 y4 y5 y6 < &0) ==>
 667     (?y2 y3 y5 y6. y2m <= y2 /\ y2 <= y2M /\ y3m <= y3 /\ y3 <= y3M /\
 668        y5m <= y5 /\ y5 <= y5M /\ y6m <= y6 /\ y6 <= y6M /\
 669        delta_y y1m y2 y3 y4 y5 y6 = &0) \/
 670     (?y1. y1m < y1 /\ delta_y y1 y2m y3m y4 y5m y6m = &0)
 671 `,
 672   (* {{{ proof *)
 673   [
 674
 675   REPEAT WEAKER_STRIP_TAC;
 676   TYPIFY `&0 <= y2M /\ &0 <= y3M /\ &0 <= y5M /\ &0 <= y6M` (C SUBGOAL_THEN ASSUME_TAC);
 677     REPEAT (FIRST_X_ASSUM_ST `!` kill);
 678     BY(ASM_TAC THEN REAL_ARITH_TAC);
 679   INTRO_TAC IVT_delta_x_full [`y1m * y1m`;`y1M * y1M`;`y2m*y2m`;`y2M*y2M`;`y3m*y3m`;`y3M*y3M`;`y4*y4`;`y5m*y5m`;`y5M*y5M`;`y6m*y6m`;`y6M*y6M`];
 680   ANTS_TAC;
 681     ASM_REWRITE_TAC[GSYM Sphere.delta_y];
 682     CONJ_TAC;
 683       GMATCH_SIMP_TAC REAL_LT_MUL_EQ;
 684       BY(ASM_REWRITE_TAC[]);
 685     CONJ_TAC;
 686       TYPIFY `!x2. y2m * y2m <= x2 /\ x2 <= y2M * y2M ==> !x3. y3m * y3m <= x3 /\ x3 <= y3M * y3M  ==> &0 < ups_x x2 x3 (y4 * y4)` ENOUGH_TO_SHOW_TAC;
 687         BY(MESON_TAC[]);
 688       REPEAT (GMATCH_SIMP_TAC FORALL_BIJ_SQUARE THEN ASM_REWRITE_TAC[] THEN REPEAT GEN_TAC THEN DISCH_TAC);
 689       FIRST_X_ASSUM MATCH_MP_TAC;
 690       BY(ASM_TAC THEN REAL_ARITH_TAC);
 691     CONJ_TAC;
 692       TYPIFY `!x5.     y5m * y5m <= x5 /\ x5 <= y5M * y5M ==> !x6. y6m * y6m <= x6 /\ x6 <= y6M * y6M     ==> &0 < ups_x (y4 * y4) x5 x6` ENOUGH_TO_SHOW_TAC;
 693         BY(MESON_TAC[]);
 694       REPEAT (GMATCH_SIMP_TAC FORALL_BIJ_SQUARE THEN ASM_REWRITE_TAC[] THEN REPEAT GEN_TAC THEN DISCH_TAC);
 695       FIRST_X_ASSUM MATCH_MP_TAC;
 696       BY(ASM_TAC THEN REAL_ARITH_TAC);
 697     REPEAT (GMATCH_SIMP_TAC Misc_defs_and_lemmas.ABS_SQUARE_LE);
 698     ASM_SIMP_TAC[arith `&0 <= y ==> abs y = y`];
 699     TYPIFY `!x2 .     y2m * y2m <= x2 /\     x2 <= y2M * y2M ==> !x3.     y3m * y3m <= x3 /\     x3 <= y3M * y3M ==> !x5.     y5m * y5m <= x5 /\     x5 <= y5M * y5M ==> !x6.     y6m * y6m <= x6 /\     x6 <= y6M * y6M     ==> delta_x1 (y1m * y1m) x2 x3 (y4 * y4) x5 x6 < &0` ENOUGH_TO_SHOW_TAC;
 700       BY(MESON_TAC[]);
 701     REPEAT (GMATCH_SIMP_TAC FORALL_BIJ_SQUARE THEN ASM_REWRITE_TAC[] THEN REPEAT GEN_TAC THEN DISCH_TAC);
 702     REWRITE_TAC[GSYM Sphere.y_of_x];
 703     FIRST_X_ASSUM MATCH_MP_TAC;
 704     BY(ASM_TAC THEN REAL_ARITH_TAC);
 705   STRIP_TAC;
 706     DISJ1_TAC;
 707     TYPIFY `?y2.     y2m <= y2 /\     y2 <= y2M /\ ?y3.     y3m <= y3 /\     y3 <= y3M /\ ?y5.     y5m <= y5 /\     y5 <= y5M /\ ?y6.     y6m <= y6 /\     y6 <= y6M /\     delta_y y1m y2 y3 y4 y5 y6 = &0` ENOUGH_TO_SHOW_TAC;
 708       BY(MESON_TAC[]);
 709     REWRITE_TAC[Sphere.delta_y];
 710     GMATCH_SIMP_TAC (GSYM EXISTS_BIJ_SQUARE);
 711     ASM_REWRITE_TAC[];
 712     TYPIFY `x2` EXISTS_TAC;
 713     ASM_REWRITE_TAC[];
 714     GMATCH_SIMP_TAC (GSYM EXISTS_BIJ_SQUARE);
 715     ASM_REWRITE_TAC[];
 716     TYPIFY `x3` EXISTS_TAC;
 717     ASM_REWRITE_TAC[];
 718     GMATCH_SIMP_TAC (GSYM EXISTS_BIJ_SQUARE);
 719     ASM_REWRITE_TAC[];
 720     TYPIFY `x5` EXISTS_TAC;
 721     ASM_REWRITE_TAC[];
 722     GMATCH_SIMP_TAC (GSYM EXISTS_BIJ_SQUARE);
 723     ASM_REWRITE_TAC[];
 724     TYPIFY `x6` EXISTS_TAC;
 725     BY(ASM_REWRITE_TAC[]);
 726   DISJ2_TAC;
 727   REWRITE_TAC[Sphere.delta_y];
 728   TYPIFY `sqrt x1` EXISTS_TAC;
 729   GMATCH_SIMP_TAC (GSYM SQRT_MUL);
 730   GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx;
 731   ASM_REWRITE_TAC[];
 732   GMATCH_SIMP_TAC REAL_LT_RSQRT;
 733   ASM_REWRITE_TAC[arith `y pow 2 = y*y`];
 734   FIRST_X_ASSUM_ST `<` MP_TAC;
 735   BY(MESON_TAC[arith `a < y ==> a <= y`;arith `y*y = y pow 2`;REAL_LE_POW_2;REAL_LE_TRANS])
 736   ]);;
 737   (* }}} *)
 738
 739 let REAL_WLOG_DS_LEMMA = prove_by_refinement(
 740   `!P. (!(y1:A) y2 y3 (y4:A) y5 y6. P y1 y2 y3 y4 y5 y6 = P y1 y3 y2 y4 y6 y5) /\
 741     (!y1 y2 y3 y4 y5 y6. P y1 y2 y3 y4 y5 y6 = P y1 y5 y6 y4 y2 y3) /\
 742     (!y1 y2 y3 y4 y5 y6. (y3 <= y2) /\ (y5 <= y2) /\ (y6 <= y2)
 743          ==>
 744        P y1 y2 y3 y4 y5 y6) ==>
 745     (!y1 y2 y3 y4 y5 y6. P y1 y2 y3 y4 y5 y6)`,
 746   (* {{{ proof *)
 747   [
 748   REPEAT WEAK_STRIP_TAC;
 749   SUBGOAL_THEN `?a.  a IN {y2,y3,y5,y6} /\ (!x. x IN {y2,y3,y5,y6} ==> x <= a)` MP_TAC;
 750     MATCH_MP_TAC Merge_ineq.REAL_FINITE_MAX_EXISTS;
 751     BY(REWRITE_TAC[ FINITE_INSERT ; FINITE_EMPTY;NOT_INSERT_EMPTY]);
 752   REPEAT WEAK_STRIP_TAC;
 753   REPEAT (FIRST_X_ASSUM_ST `IN` MP_TAC);
 754   REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY];
 755   REWRITE_TAC[MESON[] `(!x. x = y2 \/ x = y3 \/ x = y5 \/ x = y6 ==> x <= a) = (y2 <= a /\ y3 <= a /\ y5 <= a /\ y6 <= a)`];
 756   BY(DISCH_THEN STRIP_ASSUME_TAC THEN ASM_MESON_TAC[])
 757   ]);;
 758   (* }}} *)
 759
 760 (*
 761 let REAL_WLOG_DS2_LEMMA = prove_by_refinement(
 762 `!P. (!(y1:A) y2 y3 (y4:A) y5 y6. P y1 y2 y3 y4 y5 y6 = P y1 y3 y2 y4 y6 y5) /\
 763     (!y1 y2 y3 y4 y5 y6. P y1 y2 y3 y4 y5 y6 = P y1 y5 y6 y4 y2 y3) /\
 764     (!y1 y2 y3 y4 y5 y6. (y3 <= y2) /\ (y5 <= y2) /\ (y6 <= y2) /\
 765        (y6 <= y3)
 766          ==>
 767        P y1 y2 y3 y4 y5 y6) ==>
 768     (!y1 y2 y3 y4 y5 y6. P y1 y2 y3 y4 y5 y6)`,
 769   (* {{{ proof *)
 770   [
 771   GEN_TAC;
 772   DISCH_TAC;
 773   MATCH_MP_TAC REAL_WLOG_DS_LEMMA;
 774   ASM_REWRITE_TAC[];
 775   BY(ASM_MESON_TAC[arith `y3 <= y6 \/ y6 <= y3`;arith `y3 <= y3`])
 776   ]);;
 777   (* }}} *)
 778 *)
 779
 780 let WLOG_8673686234 = prove_by_refinement(
 781   `(!y1 y2 y3 y4 y5 y6.
 782       y3 <= y2 /\ y5 <= y2 /\ y6 <= y2 ==>
 783       ineq [
 784   (sqrt8,y1,#3.0);
 785     (&2,y2,&2 * h0);
 786     (&2,y3,&2 * h0);
 787     (sqrt8,y4,&4 * h0);
 788     (&2,y5,&2 * h0);
 789     (&2,y6,&2 * h0)
 790   ]
 791     ((y2 + y3 + y5 + y6 - #7.99 > #2.75 * (y1 - sqrt8)) \/
 792      (delta_y y1 y2 y3 y4 y5 y6 < &0) \/
 793      (y4 < y1))) ==> (!y1 y2 y3 y4 y5 y6. ineq [
 794   (sqrt8,y1,#3.0);
 795     (&2,y2,&2 * h0);
 796     (&2,y3,&2 * h0);
 797     (sqrt8,y4,&4 * h0);
 798     (&2,y5,&2 * h0);
 799     (&2,y6,&2 * h0)
 800   ]
 801     ((y2 + y3 + y5 + y6 - #7.99 > #2.75 * (y1 - sqrt8)) \/
 802      (delta_y y1 y2 y3 y4 y5 y6 < &0) \/
 803      (y4 < y1)))`,
 804   (* {{{ proof *)
 805   [
 806   DISCH_TAC;
 807   MATCH_MP_TAC REAL_WLOG_DS_LEMMA;
 808   ASM_REWRITE_TAC[];
 809   FIRST_X_ASSUM kill;
 810   CONJ_TAC;
 811     REPEAT WEAKER_STRIP_TAC;
 812     REWRITE_TAC[Sphere.ineq];
 813     REWRITE_TAC[Merge_ineq.delta_y_sym];
 814     BY(REAL_ARITH_TAC);
 815   REPEAT WEAKER_STRIP_TAC;
 816   REWRITE_TAC[Sphere.ineq];
 817   TYPIFY `delta_y y1 y5 y6 y4 y2 y3 = delta_y y1 y2 y3 y4 y5 y6` (C SUBGOAL_THEN SUBST1_TAC);
 818     BY(MESON_TAC[Merge_ineq.delta_y_sym]);
 819   BY(REAL_ARITH_TAC)
 820   ]);;
 821   (* }}} *)
 822
 823 (* Prove "8673686234" using inequalities
 824 "6170936724", "8673686234 a", "8673686234 b", "8673686234 c" *)
 825
 826 let LEMMA_8673686234 = prove_by_refinement(
 827   `
 828 (!y1 y2 y3 y4 y5 y6. ineq [
 829     (&3,y1,&3);
 830     (&2,y2,#2.52);
 831     (&2,y3,#2.52);
 832     (sqrt8,y4,&4 * h0);
 833     (&2,y5,#2.52);
 834       (&2,y6,#2.52)
 835   ]
 836   ( y_of_x delta_x1 y1 y2 y3 y4 y5 y6 < &0)) /\
 837
 838 (!y1 y2 y3 y4 y5 y6. ineq [
 839   (sqrt8,y1,#3.0);
 840     (&2,y2,#2.07);
 841     (&2,y3,#2.07);
 842     (sqrt8,y4,&4 * h0);
 843     (&2,y5,#2.07);
 844     (&2,y6,#2.07)
 845   ]
 846     ((y2 + y3 + y5 + y6 - #7.99 - #0.00385 * delta_y y1 y2 y3 y4 y5 y6 >   #2.75 * ((y1 + y4)/ &2 - sqrt8))
 847     )  ) /\
 848
 849 (!y1 y2 y3 y4 y5 y6. ineq [
 850   (sqrt8,y1,#3.0);
 851     (#2.07,y2,&2 * h0);
 852     (&2,y3,&2 * h0);
 853     (#3.0,y4,#3.0);
 854     (&2,y5,&2 * h0);
 855     (&2,y6,&2 * h0)
 856   ]
 857     ((y2 + y3 + y5 + y6 - #7.99 > #2.75 * (y1 - sqrt8)) \/
 858      (delta_y y1 y2 y3 y4 y5 y6 < &0)  )  ) /\
 859
 860 (!y1 y2 y3 y4 y5 y6. ineq [
 861   (sqrt8,y1,#3.0);
 862     (#2.07,y2,&2 * h0);
 863     (&2,y3,&2 * h0);
 864     (sqrt8,y4,#3.0);
 865     (&2,y5,&2 * h0);
 866     (&2,y6,&2 * h0)
 867   ]
 868     ((y2 + y3 + y5 + y6 - #7.99 >   #2.75 * ((y1 + y4)/ &2 - sqrt8)) \/
 869    (y2 + y3 + y5 + y6 - #7.99 - #0.00385 * delta_y y1 y2 y3 y4 y5 y6 >   #2.75 * ((y1 + y4)/ &2 - sqrt8)) \/
 870      (delta_y y1 y2 y3 y4 y5 y6 < &0)  )  )
 871 ==> (!y1 y2 y3 y4 y5 y6. ineq [
 872   (sqrt8,y1,#3.0);
 873     (&2,y2,&2 * h0);
 874     (&2,y3,&2 * h0);
 875     (sqrt8,y4,&4 * h0);
 876     (&2,y5,&2 * h0);
 877     (&2,y6,&2 * h0)
 878   ]
 879     ((y2 + y3 + y5 + y6 - #7.99 > #2.75 * (y1 - sqrt8)) \/
 880      (delta_y y1 y2 y3 y4 y5 y6 < &0) \/
 881      (y4 < y1))  )
 882
 883 `,
 884   (* {{{ proof *)
 885   [
 886   DISCH_TAC;
 887   MATCH_MP_TAC WLOG_8673686234;
 888   REPEAT WEAKER_STRIP_TAC;
 889   FIRST_X_ASSUM_ST `delta_y` MP_TAC THEN REPEAT WEAKER_STRIP_TAC;
 890   COMMENT "case a";
 891   ASM_CASES_TAC `y2 <= #2.07`;
 892     FIRST_X_ASSUM_ST `&2,y2,#2.07` MP_TAC;
 893     DISCH_THEN (C INTRO_TAC [`y1`;`y2`;`y3`;`y4`;`y5`;`y6`]);
 894     REWRITE_TAC[Sphere.ineq];
 895     REPEAT (FIRST_X_ASSUM_ST `y <= y2` MP_TAC);
 896     BY(REAL_ARITH_TAC);
 897   FIRST_X_ASSUM_ST `&2,y2,#2.07` kill;
 898   COMMENT "case c";
 899   ASM_CASES_TAC `y4 <= #3.0`;
 900     FIRST_X_ASSUM_ST `ineq` MP_TAC;
 901     DISCH_THEN (C INTRO_TAC [`y1`;`y2`;`y3`;`y4`;`y5`;`y6`]);
 902     REWRITE_TAC[Sphere.ineq];
 903     REPEAT (FIRST_X_ASSUM_ST `y <= y2` MP_TAC);
 904     BY(REAL_ARITH_TAC);
 905   FIRST_X_ASSUM_ST `ineq` kill;
 906   COMMENT "case b";
 907   ASM_CASES_TAC `delta_y y1 y2 y3 y4 y5 y6 < &0`;
 908     BY(ASM_REWRITE_TAC[Sphere.ineq]);
 909   ASM_CASES_TAC `y4 < y1`;
 910     BY(ASM_REWRITE_TAC[Sphere.ineq]);
 911   ASM_REWRITE_TAC[];
 912   COMMENT "ups";
 913   REWRITE_TAC[Sphere.ineq];
 914   REPEAT WEAKER_STRIP_TAC;
 915   TYPIFY `&0 < ups_x (y1*y1) (y2*y2) (y6*y6)` (C SUBGOAL_THEN ASSUME_TAC);
 916     MATCH_MP_TAC Merge_ineq.UPS_X_POS;
 917     REPLICATE_TAC 14 (FIRST_X_ASSUM MP_TAC);
 918     MP_TAC Flyspeck_constants.bounds;
 919     BY(REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
 920   TYPIFY `&0 < ups_x (y1*y1) (y3*y3) (y5*y5)` (C SUBGOAL_THEN ASSUME_TAC);
 921     MATCH_MP_TAC Merge_ineq.UPS_X_POS;
 922     REPLICATE_TAC 14 (FIRST_X_ASSUM MP_TAC);
 923     MP_TAC Flyspeck_constants.bounds;
 924     BY(REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
 925   COMMENT "construct y4'";
 926   TYPIFY `?y4'. y4 <= y4' /\ delta_y y1 y2 y3 y4' y5 y6 = &0` (C SUBGOAL_THEN MP_TAC);
 927     MATCH_MP_TAC delta_y_root_exists;
 928     CONJ_TAC;
 929       BY(ASM_TAC THEN REAL_ARITH_TAC);
 930     MP_TAC Flyspeck_constants.bounds;
 931     BY(ASM_TAC THEN REAL_ARITH_TAC);
 932   REPEAT WEAKER_STRIP_TAC;
 933   INTRO_TAC IVT_delta_y_full [`#3.0`;`y4'`;`#2.07`;`y2`;`&2`;`y6`;`y1`;`&2`;`y5`;`&2`;`y3`];
 934   ASM_REWRITE_TAC[arith `&0 <= #3.0 /\ &0 <= #2.07 /\ &0 <= &2`];
 935   ANTS_TAC;
 936     FIRST_X_ASSUM_ST `ineq` kill;
 937     TYPIFY_GOAL_THEN `(!y2' y3' y5' y6'.       #2.07 <= y2' /\      y2' <= y2 /\      &2 <= y3' /\      y3' <= y6 /\      &2 <= y5' /\      y5' <= y5 /\      &2 <= y6' /\      y6' <= y3      ==> y_of_x delta_x1  #3.0 y2' y3' y1 y5' y6' < &0)` (unlist REWRITE_TAC);
 938       REPEAT WEAKER_STRIP_TAC;
 939       FIRST_X_ASSUM (C INTRO_TAC [`#3.0`;`y2'`;`y3'`;`y1`;`y5'`;`y6'`]);
 940       REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
 941       DISCH_THEN MATCH_MP_TAC;
 942       BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
 943     TYPIFY `delta_y y4' y2 y6 y1 y5 y3 = delta_y y1 y2 y3 y4' y5 y6` (C SUBGOAL_THEN SUBST1_TAC);
 944       BY(MESON_TAC[Merge_ineq.delta_y_sym]);
 945     ASM_REWRITE_TAC[];
 946     FIRST_X_ASSUM_ST `ineq` kill;
 947     CONJ_TAC;
 948       BY(ASM_TAC THEN MP_TAC Flyspeck_constants.bounds THEN REAL_ARITH_TAC);
 949     CONJ_TAC;
 950       REPEAT WEAKER_STRIP_TAC;
 951       MATCH_MP_TAC Merge_ineq.UPS_X_POS;
 952       ASM_REWRITE_TAC[];
 953       BY(MP_TAC Flyspeck_constants.bounds THEN ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
 954     CONJ_TAC;
 955       REPEAT WEAKER_STRIP_TAC;
 956       MATCH_MP_TAC Merge_ineq.UPS_X_POS;
 957       ASM_REWRITE_TAC[];
 958       BY(MP_TAC Flyspeck_constants.bounds THEN ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
 959     BY(ASM_TAC THEN REAL_ARITH_TAC);
 960   DISCH_THEN DISJ_CASES_TAC;
 961     FIRST_X_ASSUM (X_CHOOSE_THEN `y2':real` ASSUME_TAC);
 962     FIRST_X_ASSUM (X_CHOOSE_THEN `y6':real` ASSUME_TAC);
 963     FIRST_X_ASSUM (X_CHOOSE_THEN `y5':real` ASSUME_TAC);
 964     FIRST_X_ASSUM (X_CHOOSE_THEN `y3':real` ASSUME_TAC);
 965     FIRST_X_ASSUM (C INTRO_TAC [`y1`;`y2'`;`y3'`;`#3.0`;`y5'`;`y6'`]);
 966     ASM_REWRITE_TAC[Sphere.ineq;arith `~(&0 < &0)`;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
 967     TYPIFY `delta_y y1 y2' y3' #3.0 y5' y6' = delta_y #3.0 y2' y6' y1 y5' y3'` (C SUBGOAL_THEN SUBST1_TAC);
 968       BY(MESON_TAC[Merge_ineq.delta_y_sym]);
 969     ASM_REWRITE_TAC[];
 970     ANTS_TAC;
 971       BY(MP_TAC Flyspeck_constants.bounds THEN ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
 972     BY(ASM_TAC THEN REAL_ARITH_TAC);
 973   COMMENT "second case: long diags";
 974   PROOF_BY_CONTR_TAC;
 975   FIRST_X_ASSUM_ST `delta_y` MP_TAC;
 976   REPEAT WEAKER_STRIP_TAC;
 977   FIRST_X_ASSUM MP_TAC;
 978   REWRITE_TAC[Sphere.delta_y;arith `&2 * &2 = &4`];
 979   TYPED_ABBREV_TAC  `u = y1' * y1' - &9` ;
 980   TYPIFY `y1' * y1' = &9 + u` (C SUBGOAL_THEN SUBST1_TAC);
 981     BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC);
 982   TYPED_ABBREV_TAC  `v = y1 * y1 - &8` ;
 983   TYPIFY `y1 * y1 = &8 + v` (C SUBGOAL_THEN SUBST1_TAC);
 984     BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC);
 985   TYPIFY `&0 <= u` (C SUBGOAL_THEN ASSUME_TAC);
 986     EXPAND_TAC "u";
 987     REWRITE_TAC[arith `&0 <= x - &9 <=> &3 * &3 <= x`];
 988     GMATCH_SIMP_TAC Misc_defs_and_lemmas.ABS_SQUARE_LE;
 989     BY(FIRST_X_ASSUM_ST `#3.0` MP_TAC THEN REAL_ARITH_TAC);
 990   TYPIFY `&0 <= v` (C SUBGOAL_THEN ASSUME_TAC);
 991     EXPAND_TAC "v";
 992     TYPIFY_GOAL_THEN `!x. &0 <= x - &8 <=> sqrt8 * sqrt8 <= x` (unlist REWRITE_TAC);
 993       REWRITE_TAC[Nonlinear_lemma.sqrt8_2];
 994       BY(REAL_ARITH_TAC);
 995     GMATCH_SIMP_TAC Misc_defs_and_lemmas.ABS_SQUARE_LE;
 996     REPLICATE_TAC 3 (FIRST_X_ASSUM_ST `sqrt8` MP_TAC);
 997     BY(MP_TAC Flyspeck_constants.bounds THEN REAL_ARITH_TAC);
 998   MATCH_MP_TAC (arith `&0 < -- x ==> ~(x = &0)`);
 999   TYPIFY `-- delta_x (&9 + u) (#2.07 * #2.07) (&4) (&8 + v) (&4) (&4)  = #51.81187204 +  #77.7208*u + &8* u pow 2 +  #78.4359*v + #17.7151*u*v +  u pow 2 *v + &9*v pow 2 + u* v pow 2` (C SUBGOAL_THEN SUBST1_TAC);
1000     REWRITE_TAC[Sphere.delta_x];
1001     BY(REAL_ARITH_TAC);
1002   MATCH_MP_TAC (arith `&0 < x /\ &0 <= y ==> &0 < x + y`);
1003   CONJ_TAC;
1004     BY(REAL_ARITH_TAC);
1005   REWRITE_TAC[arith `v pow 2 = v*v`];
1006   REPEAT (GMATCH_SIMP_TAC (arith `&0 <= x /\ &0 <= y ==> &0 <= x + y`));
1007   GMATCH_SIMP_TAC REAL_LE_MUL;
1008   REPEAT (GMATCH_SIMP_TAC REAL_LE_MUL);
1009   ASM_REWRITE_TAC[];
1010   BY(REAL_ARITH_TAC)
1011   ]);;
1012   (* }}} *)
1013
1014 let WLOG_5691615370 = prove_by_refinement(
1015   `(!y1 y2 y3 y4 y5 y6. ineq
1016   [
1017   (#3.0,y1,#3.0);
1018   (&2,y2,#2.52);
1019   (&2,y3,#2.52);
1020   (#3.0,y4,#3.0);
1021   (&2,y5,#2.52);
1022   (&2,y6,#2.52)
1023   ]
1024   ((delta_y y1 y2 y3 y4 y5 y6 < &0) \/ (y2 + y3 + y5 + y6 > #8.472) \/
1025    (y2 < y3) \/ (y2 < y5) \/ (y2 < y6 ) \/ (y3 < y6))) ==>
1026   (!y1 y2 y3 y4 y5 y6. ineq
1027   [
1028   (#3.0,y1,#3.0);
1029   (&2,y2,#2.52);
1030   (&2,y3,#2.52);
1031   (#3.0,y4,#3.0);
1032   (&2,y5,#2.52);
1033   (&2,y6,#2.52)
1034   ]
1035   ((delta_y y1 y2 y3 y4 y5 y6 < &0) \/ (y2 + y3 + y5 + y6 > #8.472)))`,
1036   (* {{{ proof *)
1037   [
1038   ONCE_REWRITE_TAC[MESON[] `!P. (!y1 y2 y3 y4 y5 y6. P y1 y2 y3 y4 y5 y6) <=> (!y2 y3 y5 y6 y1 y4. P y1 y2 y3 y4 y5 y6)`];
1039   DISCH_TAC;
1040   MATCH_MP_TAC Terminal.REAL_WLOG_SQUARE2_LEMMA;
1041   CONJ_TAC;
1042     REPEAT GEN_TAC;
1043     REWRITE_TAC[Sphere.ineq;Merge_ineq.delta_y_sym];
1044     TYPIFY `delta_y y1 y5 y6 y4 y2 y2' = delta_y y1 y2 y2' y4 y5 y6` (C SUBGOAL_THEN SUBST1_TAC);
1045       BY(MESON_TAC[Merge_ineq.delta_y_sym]);
1046     REWRITE_TAC[REAL_ADD_AC];
1047     BY(MESON_TAC[]);
1048   REPEAT WEAKER_STRIP_TAC;
1049   REWRITE_TAC[Sphere.ineq];
1050   RULE_ASSUM_TAC (REWRITE_RULE[Sphere.ineq]);
1051   BY(ASM_MESON_TAC[arith `x <= y ==> ~(y < x)`])
1052   ]);;
1053   (* }}} *)
1054
1055
1056 (* Use 5584033259 and 6170936724 and 5691615370  to prove the lemma. *)
1057
1058 let LEMMA_5691615370 = prove_by_refinement(
1059   `
1060 (!y1 y2 y3 y4 y5 y6. ineq [
1061     (&3,y1,&4 * h0);
1062     (&2,y2,#2.472);
1063     (&2,y3,#2.472);
1064     (&3,y4,&4 * h0);
1065     (&2,y5,#2.472);
1066       (&2,y6,#2.472)
1067   ]
1068   ( y1 < &4 \/ delta_y y1 y2 y3 y4 y5 y6 < &0 )) /\
1069
1070  (!y1 y2 y3 y4 y5 y6. ineq [
1071     (&3,y1,&3);
1072     (&2,y2,#2.52);
1073     (&2,y3,#2.52);
1074     (sqrt8,y4,&4 * h0);
1075     (&2,y5,#2.52);
1076       (&2,y6,#2.52)
1077   ]
1078   ( y_of_x delta_x1 y1 y2 y3 y4 y5 y6 < &0)) /\
1079
1080 (!y1 y2 y3 y4 y5 y6. ineq
1081   [
1082   (#3.0,y1,#3.0);
1083   (&2,y2,#2.52);
1084   (&2,y3,#2.52);
1085   (#3.0,y4,#3.0);
1086   (&2,y5,#2.52);
1087   (&2,y6,#2.52)
1088   ]
1089   ((delta_y y1 y2 y3 y4 y5 y6 < &0) \/ (y2 + y3 + y5 + y6 > #8.472) \/
1090    (y2 < y3) \/ (y2 < y5) \/ (y2 < y6 ) \/ (y3 < y6))) ==>
1091
1092 (!y1 y2 y3 y4 y5 y6. ineq
1093   [
1094   (#3.0,y1,&4 * h0);
1095   (&2,y2,#2.52);
1096   (&2,y3,#2.52);
1097   (#3.0,y4,&4 * h0);
1098   (&2,y5,#2.52);
1099   (&2,y6,#2.52)
1100   ]
1101   ((delta_y y1 y2 y3 y4 y5 y6 < &0) \/ (y2 + y3 + y5 + y6 > #8.472)))
1102   `,
1103   (* {{{ proof *)
1104   [
1105   REWRITE_TAC[Sphere.y_of_x;Functional_equation.nonf_ups_126];
1106   STRIP_TAC;
1107   FIRST_X_ASSUM (ASSUME_TAC o (MATCH_MP WLOG_5691615370));
1108   REWRITE_TAC[Sphere.ineq];
1109   REPEAT WEAKER_STRIP_TAC;
1110   ASM_CASES_TAC `delta_y y1 y2 y3 y4 y5 y6 < &0`;
1111     BY(ASM_REWRITE_TAC[]);
1112   ASM_REWRITE_TAC[];
1113   COMMENT "construct y4'";
1114   TYPIFY `?y4'. y4 <= y4' /\ delta_y y1 y2 y3 y4' y5 y6 = &0` (C SUBGOAL_THEN MP_TAC);
1115     MATCH_MP_TAC delta_y_root_exists;
1116     CONJ_TAC;
1117       BY(ASM_TAC THEN REAL_ARITH_TAC);
1118     BY(ASM_TAC THEN REAL_ARITH_TAC);
1119   REPEAT WEAKER_STRIP_TAC;
1120   COMMENT "bound 4 on diagonal";
1121   PROOF_BY_CONTR_TAC;
1122   TYPIFY `y2 <= #2.472 /\ y3 <= #2.472 /\ y5 <= #2.472 /\ y6 <= #2.472` (C SUBGOAL_THEN ASSUME_TAC);
1123     BY(REPLICATE_TAC 14 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
1124   TYPIFY `y1 < &4` (C SUBGOAL_THEN ASSUME_TAC);
1125     FIRST_X_ASSUM_ST `y1 < &4` (C INTRO_TAC [`y1`;`y2`;`y3`;`y4`;`y5`;`y6`]);
1126     ASM_REWRITE_TAC[Sphere.y_of_x;Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
1127     DISCH_THEN MATCH_MP_TAC;
1128     BY(REPLICATE_TAC 17 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
1129   INTRO_TAC IVT_delta_y_full [`#3.0`;`y4'`;`&2`;`y2`;`&2`;`y6`;`y1`;`&2`;`y5`;`&2`;`y3`];
1130   ASM_REWRITE_TAC[arith `&0 <= #3.0 /\ &0 <= &2`];
1131   DISCH_THEN MP_TAC THEN ANTS_TAC;
1132     FIRST_X_ASSUM_ST `ineq` kill;
1133     TYPIFY_GOAL_THEN `(!y2' y3' y5' y6'.      &2 <= y2' /\      y2' <= y2 /\      &2 <= y3' /\      y3' <= y6 /\      &2 <= y5' /\      y5' <= y5 /\      &2 <= y6' /\      y6' <= y3      ==> y_of_x delta_x1  #3.0 y2' y3' y1 y5' y6' < &0)` (unlist REWRITE_TAC);
1134       REPEAT WEAKER_STRIP_TAC;
1135       FIRST_X_ASSUM (C INTRO_TAC [`#3.0`;`y2'`;`y3'`;`y1`;`y5'`;`y6'`]);
1136       REWRITE_TAC[Sphere.y_of_x;Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
1137       DISCH_THEN MATCH_MP_TAC;
1138       BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN MP_TAC Flyspeck_constants.bounds THEN REAL_ARITH_TAC);
1139     TYPIFY `delta_y y4' y2 y6 y1 y5 y3 = delta_y y1 y2 y3 y4' y5 y6` (C SUBGOAL_THEN SUBST1_TAC);
1140       BY(MESON_TAC[Merge_ineq.delta_y_sym]);
1141     ASM_REWRITE_TAC[];
1142     FIRST_X_ASSUM_ST `ineq` kill;
1143     CONJ_TAC;
1144       BY(ASM_TAC THEN REAL_ARITH_TAC);
1145     CONJ_TAC;
1146       GEN_TAC;
1147       X_GEN_TAC `y6':real`;
1148       REPEAT WEAKER_STRIP_TAC;
1149       MATCH_MP_TAC Merge_ineq.UPS_X_POS;
1150       BY(REPLICATE_TAC 22 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
1151     CONJ_TAC;
1152       GEN_TAC;
1153       X_GEN_TAC `y3':real`;
1154       REPEAT WEAKER_STRIP_TAC;
1155       MATCH_MP_TAC Merge_ineq.UPS_X_POS;
1156       BY(REPLICATE_TAC 22 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
1157     BY(REPLICATE_TAC 15 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
1158   TYPIFY `!z1 z4.  #3.0 <= z1 /\ #3.0 <= z4 ==> delta_y z1 (&2) (&2) z4 (&2) (&2) < &0` (C SUBGOAL_THEN ASSUME_TAC);
1159     REWRITE_TAC[Sphere.delta_y;arith `&2 * &2 = &4`];
1160     REPEAT WEAKER_STRIP_TAC;
1161     TYPED_ABBREV_TAC  `u = z1 * z1 - &9` ;
1162     TYPIFY `z1 * z1 = &9 + u` (C SUBGOAL_THEN SUBST1_TAC);
1163       BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC);
1164     TYPED_ABBREV_TAC  `v = z4 * z4 - &9` ;
1165     TYPIFY `z4 * z4 = &9 + v` (C SUBGOAL_THEN SUBST1_TAC);
1166       BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC);
1167     TYPIFY `&0 <= u` (C SUBGOAL_THEN ASSUME_TAC);
1168       EXPAND_TAC "u";
1169       REWRITE_TAC[arith `&0 <= x - &9 <=> &3 * &3 <= x`];
1170       GMATCH_SIMP_TAC Misc_defs_and_lemmas.ABS_SQUARE_LE;
1171       BY(REPLICATE_TAC 2 (FIRST_X_ASSUM_ST `#3.0` MP_TAC) THEN REAL_ARITH_TAC);
1172     TYPIFY `&0 <= v` (C SUBGOAL_THEN ASSUME_TAC);
1173       EXPAND_TAC "v";
1174       REWRITE_TAC[arith `&0 <= x - &9 <=> &3 * &3 <= x`];
1175       GMATCH_SIMP_TAC Misc_defs_and_lemmas.ABS_SQUARE_LE;
1176       BY(REPLICATE_TAC 2 (FIRST_X_ASSUM_ST `#3.0` MP_TAC) THEN REAL_ARITH_TAC);
1177     MATCH_MP_TAC (arith `&0 < -- x ==> x < &0`);
1178     TYPIFY `-- delta_x (&9 + u) (&4) (&4) (&9 + v) (&4) (&4)  = &162 + &99*u + &9*u*u + &99*v +  &20*u*v + u*u*v + &9*v*v +  u*v*v` (C SUBGOAL_THEN SUBST1_TAC);
1179       REWRITE_TAC[Sphere.delta_x];
1180       BY(REAL_ARITH_TAC);
1181     MATCH_MP_TAC (arith `&0 < x /\ &0 <= y ==> &0 < x + y`);
1182     CONJ_TAC;
1183       BY(REAL_ARITH_TAC);
1184     REPEAT (GMATCH_SIMP_TAC (arith `&0 <= x /\ &0 <= y ==> &0 <= x + y`));
1185     REPEAT (GMATCH_SIMP_TAC REAL_LE_MUL);
1186     ASM_REWRITE_TAC[];
1187     BY(REAL_ARITH_TAC);
1188   REWRITE_TAC[DE_MORGAN_THM;NOT_EXISTS_THM];
1189   CONJ2_TAC;
1190     GEN_TAC;
1191     FIRST_X_ASSUM (C INTRO_TAC [`y1'`;`y1`]);
1192     ASM_REWRITE_TAC[];
1193     BY(ASM_TAC THEN REAL_ARITH_TAC);
1194   GEN_TAC;
1195   X_GEN_TAC `y6':real`;
1196   GEN_TAC;
1197   X_GEN_TAC `y3':real`;
1198   REWRITE_TAC[GSYM DE_MORGAN_THM];
1199   REPEAT WEAKER_STRIP_TAC;
1200   INTRO_TAC IVT_delta_y_full [`#3.0`;`y1`;`&2`;`y2'`;`&2`;`y3'`;`#3.0`;`&2`;`y5'`;`&2`;`y6'`];
1201   ASM_REWRITE_TAC[arith `&0 <= #3.0 /\ &0 <= &2 /\ &0 < #3.0`];
1202   DISCH_THEN MP_TAC THEN ANTS_TAC;
1203     FIRST_X_ASSUM_ST `ineq` kill;
1204     TYPIFY_GOAL_THEN `(!y2 y3 y5 y6.      &2 <= y2 /\      y2 <= y2' /\      &2 <= y3 /\      y3 <= y3' /\      &2 <= y5 /\      y5 <= y5' /\      &2 <= y6 /\      y6 <= y6'      ==> y_of_x delta_x1  #3.0 y2 y3  #3.0 y5 y6 < &0)` (unlist REWRITE_TAC);
1205       REPEAT WEAKER_STRIP_TAC;
1206       FIRST_X_ASSUM (C INTRO_TAC [`#3.0`;`y2''`;`y3''`;`#3.0`;`y5''`;`y6''`]);
1207       REWRITE_TAC[Sphere.y_of_x;Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
1208       DISCH_THEN MATCH_MP_TAC;
1209       BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN MP_TAC Flyspeck_constants.bounds THEN REAL_ARITH_TAC);
1210     TYPIFY `delta_y y1 y2' y3' #3.0 y5' y6' = delta_y #3.0 y2' y6' y1 y5' y3'` (C SUBGOAL_THEN SUBST1_TAC);
1211       BY(MESON_TAC[Merge_ineq.delta_y_sym]);
1212     ASM_REWRITE_TAC[];
1213     FIRST_X_ASSUM_ST `ineq` kill;
1214     CONJ_TAC;
1215       REPEAT WEAKER_STRIP_TAC;
1216       MATCH_MP_TAC Merge_ineq.UPS_X_POS;
1217       BY(REPLICATE_TAC 22 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
1218     REPEAT WEAKER_STRIP_TAC;
1219     MATCH_MP_TAC Merge_ineq.UPS_X_POS;
1220     BY(REPLICATE_TAC 22 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
1221   TYPIFY_GOAL_THEN `~(?y1.  #3.0 < y1 /\ delta_y y1 (&2) (&2)  #3.0 (&2) (&2) = &0)` (unlist REWRITE_TAC);
1222     REWRITE_TAC[NOT_EXISTS_THM];
1223     GEN_TAC;
1224     FIRST_X_ASSUM (C INTRO_TAC [`y1'`;`#3.0`]);
1225     BY(REPLICATE_TAC 22 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
1226   REWRITE_TAC[NOT_EXISTS_THM];
1227   REPEAT WEAKER_STRIP_TAC;
1228   FIRST_X_ASSUM (C INTRO_TAC [`#3.0`;`y2''`;`y3''`;`#3.0`;`y5''`;`y6''`]);
1229   ASM_REWRITE_TAC[Sphere.y_of_x;Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
1230   BY(REPLICATE_TAC 37 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC)
1231   ]);;
1232   (* }}} *)
1233
1234
1235 end;;