text_formalization/tame/Inequalities.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Chapter: Tame Hypermap                                                     *)
   5 (* Author: Alexey Solovyev                                                    *)
   6 (* Date: 2010-07-07                                                           *)
   7 (* Some nonlinear (polynomial) inequalities                                   *)
   8 (* ========================================================================== *)
   9
  10 flyspeck_needs "general/sphere.hl";;
  11 flyspeck_needs "trigonometry/trigonometry.hl";;
  12 flyspeck_needs "nonlinear/ineq.hl";;
  13
  14
  15 module Tame_inequalities = struct
  16
  17
  18 let let_RULE = fun th -> REWRITE_RULE[DEPTH_CONV let_CONV (concl th)] th;;
  19
  20 let REMOVE_ASSUM = POP_ASSUM (fun th -> ALL_TAC);;
  21
  22
  23
  24 (* Alternative form for ineq *)
  25 let INEQ_ALT = prove(`!A bounds. ineq bounds A <=> (ALL (\(a,x,b). a <= x /\ x <= b) bounds ==> A)`,
  26   GEN_TAC THEN
  27     MATCH_MP_TAC list_INDUCT THEN REPEAT STRIP_TAC THENL
  28     [
  29       REWRITE_TAC[Sphere.ineq; ALL];
  30       ALL_TAC
  31     ] THEN
  32     MP_TAC (ISPEC `a0:real#real#real` PAIR_SURJECTIVE) THEN
  33     DISCH_THEN (X_CHOOSE_THEN `a:real` MP_TAC) THEN
  34     DISCH_THEN (CHOOSE_THEN MP_TAC) THEN
  35     MP_TAC (ISPEC `y:real#real` PAIR_SURJECTIVE) THEN
  36     DISCH_THEN (X_CHOOSE_THEN `x:real` MP_TAC) THEN
  37     DISCH_THEN (X_CHOOSE_THEN `b:real` MP_TAC) THEN
  38     DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
  39     DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
  40     ASM_SIMP_TAC[Sphere.ineq; ALL; IMP_IMP]);;
  41
  42
  43
  44 (**************************************************)
  45
  46 let lemma = prove(`!a b c x x0 x1. a < &0 /\ x0 <= x /\ x <= x1 ==> a*x*x + b*x + c >= a*x0*x0 + b*x0 + c \/ a*x*x + b*x + c >= a*x1*x1 + b*x1 + c`,
  47    REPEAT STRIP_TAC THEN
  48      REWRITE_TAC[REAL_ARITH `a*x*x + b*x + c >= a*x0*x0 + b*x0 + c <=> &0 <= (x - x0) * (a * x0 + a * x + b)`] THEN
  49      DISJ_CASES_TAC (REAL_ARITH `&0 <= a * x0 + a * x + b \/ a * x0 + a * x + b < &0`) THENL
  50      [
  51        DISJ1_TAC THEN
  52          MATCH_MP_TAC REAL_LE_MUL THEN
  53          ASM_REWRITE_TAC[REAL_ARITH `&0 <= x - x0 <=> x0 <= x`];
  54        DISJ2_TAC THEN
  55          REWRITE_TAC[REAL_ARITH `(x - x1) * (a * x1 + a * x + b) = (x1 - x) * --(a * x1 + a * x + b)`] THEN
  56          MATCH_MP_TAC REAL_LE_MUL THEN
  57          ASM_REWRITE_TAC[REAL_ARITH `&0 <= x1 - x <=> x <= x1`; REAL_ARITH `&0 <= --a <=> a <= &0`] THEN
  58          MATCH_MP_TAC REAL_LE_TRANS THEN
  59          EXISTS_TAC `a * x0 + a * x + b:real` THEN
  60          ASM_SIMP_TAC[REAL_LT_IMP_LE] THEN
  61          REWRITE_TAC[REAL_ARITH `a + b <= c + b <=> a <= c`] THEN
  62          REWRITE_TAC[REAL_ARITH `a * x1 <= a * x0 <=> &0 <= --a * (x1 - x0)`] THEN
  63          MATCH_MP_TAC REAL_LE_MUL THEN
  64          REPEAT (POP_ASSUM MP_TAC) THEN
  65          REAL_ARITH_TAC
  66      ]);;
  67
  68
  69 let lemma' = prove(`!f a b c x x0 x1. f = (\x. a*x*x + b*x + c) /\ x0 <= x /\ x <= x1 /\ a < &0 ==> f x >= f x0 \/ f x >= f x1`,
  70    REPEAT STRIP_TAC THEN
  71      ASM_REWRITE_TAC[] THEN
  72      MATCH_MP_TAC lemma THEN
  73      ASM_REWRITE_TAC[]);;
  74
  75
  76 let lemma1 = prove(`!x1 x2 x3 x4 x5 x6. #4.0 <= x1 /\ x1 <= #6.3504 /\ #4.0 <= x4 ==> delta_x x1 x2 x3 x4 x5 x6 >= delta_x #4.0 x2 x3 x4 x5 x6 \/ delta_x x1 x2 x3 x4 x5 x6 >= delta_x #6.3504 x2 x3 x4 x5 x6`,
  77    REPEAT STRIP_TAC THEN
  78      SUBGOAL_THEN `!x1. delta_x x1 x2 x3 x4 x5 x6 = (\x. delta_x x x2 x3 x4 x5 x6) x1` (fun th -> ONCE_REWRITE_TAC[th]) THENL
  79      [
  80        REWRITE_TAC[];
  81        ALL_TAC
  82      ] THEN
  83
  84      MATCH_MP_TAC lemma' THEN
  85      ASM_REWRITE_TAC[Sphere.delta_x; FUN_EQ_THM] THEN
  86      MAP_EVERY EXISTS_TAC [`--x4`; `x4*(x2+x3-x4+x5+x6)+x2*x5+x3*x6-x3*x5-x2*x6`; `x2*x5*(x3-x2+x4-x5+x6) + x3*x6*(x2-x3+x4+x5-x6)-x2*x3*x4-x4*x5*x6`] THEN
  87      POP_ASSUM MP_TAC THEN REAL_ARITH_TAC);;
  88
  89
  90 let lemma2 = prove(`!x1 x2 x3 x4 x5 x6. #4.0 <= x2 /\ x2 <= #6.3504 /\ #4.0 <= x5 ==> delta_x x1 x2 x3 x4 x5 x6 >= delta_x x1 #4.0 x3 x4 x5 x6 \/ delta_x x1 x2 x3 x4 x5 x6 >= delta_x x1 #6.3504 x3 x4 x5 x6`,
  91    REPEAT STRIP_TAC THEN
  92      SUBGOAL_THEN `!x2. delta_x x1 x2 x3 x4 x5 x6 = (\x. delta_x x1 x x3 x4 x5 x6) x2` (fun th -> ONCE_REWRITE_TAC[th]) THENL
  93      [
  94        REWRITE_TAC[];
  95        ALL_TAC
  96      ] THEN
  97
  98      MATCH_MP_TAC lemma' THEN
  99      ASM_REWRITE_TAC[Sphere.delta_x; FUN_EQ_THM] THEN
 100      MAP_EVERY EXISTS_TAC [`--x5`; `x5*(x1+x3+x4-x5+x6)+x1*x4+x3*x6-x3*x4-x1*x6`; `x1*x4*(--x1+x3-x4+x5+x6) + x3*x6*(x1-x3+x4+x5-x6)-x1*x3*x5-x4*x5*x6`] THEN
 101      POP_ASSUM MP_TAC THEN REAL_ARITH_TAC);;
 102
 103
 104 let lemma3 = prove(`!x1 x2 x3 x4 x5 x6. #4.0 <= x3 /\ x3 <= #6.3504 /\ #4.0 <= x6 ==> delta_x x1 x2 x3 x4 x5 x6 >= delta_x x1 x2 #4.0 x4 x5 x6 \/ delta_x x1 x2 x3 x4 x5 x6 >= delta_x x1 x2 #6.3504 x4 x5 x6`,
 105    REPEAT STRIP_TAC THEN
 106      ONCE_REWRITE_TAC[SYM (BETA_CONV `(\x. delta_x x1 x2 x x4 x5 x6) x3`)] THEN
 107      MATCH_MP_TAC lemma' THEN
 108      ASM_REWRITE_TAC[Sphere.delta_x; FUN_EQ_THM] THEN
 109      MAP_EVERY EXISTS_TAC [`--x6`; `x6*(x1+x2-x6+x4+x5)+x1*x4+x2*x5-x2*x4-x1*x5`; `x2*x5*(x1-x2+x4-x5+x6) + x1*x4*(--x1+x2-x4+x5+x6)-x1*x2*x6-x4*x5*x6`] THEN
 110      POP_ASSUM MP_TAC THEN REAL_ARITH_TAC);;
 111
 112
 113 let lemma4 = prove(`!x1 x2 x3 x4 x5 x6. #4.0 <= x4 /\ x4 <= #6.3504 /\ #4.0 <= x1 ==> delta_x x1 x2 x3 x4 x5 x6 >= delta_x x1 x2 x3 #4.0 x5 x6 \/ delta_x x1 x2 x3 x4 x5 x6 >= delta_x x1 x2 x3 #6.3504 x5 x6`,
 114    REPEAT STRIP_TAC THEN
 115      ONCE_REWRITE_TAC[SYM (BETA_CONV `(\x. delta_x x1 x2 x3 x x5 x6) x4`)] THEN
 116      MATCH_MP_TAC lemma' THEN
 117      ASM_REWRITE_TAC[Sphere.delta_x; FUN_EQ_THM] THEN
 118      MAP_EVERY EXISTS_TAC [`--x1`; `x1*(--x1+x2+x3+x5+x6)+x2*x5+x3*x6-x2*x3-x5*x6`; `x2*x5*(x1-x2+x3-x5+x6) + x3*x6*(x1+x2-x3+x5-x6)-x1*x3*x5-x1*x2*x6`] THEN
 119      POP_ASSUM MP_TAC THEN REAL_ARITH_TAC);;
 120
 121
 122 let lemma5 = prove(`!x1 x2 x3 x4 x5 x6. #4.0 <= x5 /\ x5 <= #6.3504 /\ #4.0 <= x2 ==> delta_x x1 x2 x3 x4 x5 x6 >= delta_x x1 x2 x3 x4 #4.0 x6 \/ delta_x x1 x2 x3 x4 x5 x6 >= delta_x x1 x2 x3 x4 #6.3504 x6`,
 123    REPEAT STRIP_TAC THEN
 124      ONCE_REWRITE_TAC[SYM (BETA_CONV `(\x. delta_x x1 x2 x3 x4 x x6) x5`)] THEN
 125      MATCH_MP_TAC lemma' THEN
 126      ASM_REWRITE_TAC[Sphere.delta_x; FUN_EQ_THM] THEN
 127      MAP_EVERY EXISTS_TAC [`--x2`; `x2*(x1+x3-x2+x4+x6)+x1*x4+x3*x6-x1*x3-x4*x6`; `x1*x4*(--x1+x2+x3-x4+x6) + x3*x6*(x1+x2-x3+x4-x6)-x2*x3*x4-x1*x2*x6`] THEN
 128      POP_ASSUM MP_TAC THEN REAL_ARITH_TAC);;
 129
 130
 131 let lemma6 = prove(`!x1 x2 x3 x4 x5 x6. #4.0 <= x6 /\ x6 <= #6.3504 /\ #4.0 <= x3 ==> delta_x x1 x2 x3 x4 x5 x6 >= delta_x x1 x2 x3 x4 x5 #4.0 \/ delta_x x1 x2 x3 x4 x5 x6 >= delta_x x1 x2 x3 x4 x5 #6.3504`,
 132    REPEAT STRIP_TAC THEN
 133      ONCE_REWRITE_TAC[SYM (BETA_CONV `(\x. delta_x x1 x2 x3 x4 x5 x) x6`)] THEN
 134      MATCH_MP_TAC lemma' THEN
 135      ASM_REWRITE_TAC[Sphere.delta_x; FUN_EQ_THM] THEN
 136      MAP_EVERY EXISTS_TAC [`--x3`; `x3*(x1+x2-x3+x4+x5)+x1*x4+x2*x5-x1*x2-x4*x5`; `x2*x5*(x1-x2+x3+x4-x5) + x1*x4*(--x1+x2+x3-x4+x5)-x2*x3*x4-x1*x3*x5`] THEN
 137      POP_ASSUM MP_TAC THEN REAL_ARITH_TAC);;
 138
 139
 140
 141
 142
 143
 144 let main_lemma = prove(`!(f:real->real) x x0 x1 m. (f x >= f x0 \/ f x >= f x1) /\ f x0 >= m /\ f x1 >= m ==> f x >= m`,
 145    REWRITE_TAC[real_ge] THEN
 146      REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_LE_TRANS THENL
 147      [
 148        EXISTS_TAC `(f:real->real) x0` THEN
 149          ASM_REWRITE_TAC[];
 150        EXISTS_TAC `(f:real->real) x1` THEN
 151          ASM_REWRITE_TAC[]
 152      ]);;
 153
 154
 155 (* delta_x > 0 for x IN [4,4 h0^2] *)
 156
 157 let delta_x_pos = prove(`!x1 x2 x3 x4 x5 x6. ineq [#4.0,x1,#6.3504;
 158                                                    #4.0,x2,#6.3504;
 159                                                    #4.0,x3,#6.3504;
 160                                                    #4.0,x4,#6.3504;
 161                                                    #4.0,x5,#6.3504;
 162                                                    #4.0,x6,#6.3504] (delta_x x1 x2 x3 x4 x5 x6 >= #128.0)`,
 163    REPEAT STRIP_TAC THEN
 164      REWRITE_TAC[INEQ_ALT; ALL] THEN
 165      REPEAT STRIP_TAC THEN
 166      ASSUME_TAC (REAL_ARITH `#4.0 <= #4.0 /\ #4.0 <= #6.3504`) THEN
 167
 168      (* x1 *)
 169      ONCE_REWRITE_TAC[SYM (BETA_CONV `(\x. delta_x x x2 x3 x4 x5 x6) x1`)] THEN
 170      MATCH_MP_TAC main_lemma THEN
 171      MAP_EVERY EXISTS_TAC [`#4.0`; `#6.3504`] THEN
 172      ASM_SIMP_TAC[lemma1] THEN
 173      CONJ_TAC THEN
 174
 175      (* x2 *)
 176      ONCE_REWRITE_TAC[SYM (BETA_CONV `(\x. delta_x x1 x x3 x4 x5 x6) x2`)] THEN
 177      MATCH_MP_TAC main_lemma THEN
 178      MAP_EVERY EXISTS_TAC [`#4.0`; `#6.3504`] THEN
 179      ASM_SIMP_TAC[lemma2] THEN
 180      CONJ_TAC THEN
 181
 182      (* x3 *)
 183      ONCE_REWRITE_TAC[SYM (BETA_CONV `(\x. delta_x x1 x2 x x4 x5 x6) x3`)] THEN
 184      MATCH_MP_TAC main_lemma THEN
 185      MAP_EVERY EXISTS_TAC [`#4.0`; `#6.3504`] THEN
 186      ASM_SIMP_TAC[lemma3] THEN
 187      CONJ_TAC THEN
 188
 189      (* x4 *)
 190      ONCE_REWRITE_TAC[SYM (BETA_CONV `(\x. delta_x x1 x2 x3 x x5 x6) x4`)] THEN
 191      MATCH_MP_TAC main_lemma THEN
 192      MAP_EVERY EXISTS_TAC [`#4.0`; `#6.3504`] THEN
 193      ASM_SIMP_TAC[lemma4] THEN
 194      CONJ_TAC THEN
 195
 196      (* x5 *)
 197      ONCE_REWRITE_TAC[SYM (BETA_CONV `(\x. delta_x x1 x2 x3 x4 x x6) x5`)] THEN
 198      MATCH_MP_TAC main_lemma THEN
 199      MAP_EVERY EXISTS_TAC [`#4.0`; `#6.3504`] THEN
 200      ASM_SIMP_TAC[lemma5] THEN
 201      CONJ_TAC THEN
 202
 203      (* x6 *)
 204      ONCE_REWRITE_TAC[SYM (BETA_CONV `(\x. delta_x x1 x2 x3 x4 x5 x) x6`)] THEN
 205      MATCH_MP_TAC main_lemma THEN
 206      MAP_EVERY EXISTS_TAC [`#4.0`; `#6.3504`] THEN
 207      ASM_SIMP_TAC[lemma6] THEN
 208      CONJ_TAC THEN
 209
 210      (* Final stage *)
 211      REWRITE_TAC[Sphere.delta_x] THEN
 212      CONV_TAC REAL_RAT_REDUCE_CONV);;
 213
 214
 215 let lemma3 = prove(`!x1 x2 x3 x4 x5 x6. #4.0 <= x3 /\ x3 <= #6.3504 /\ #0.64 <= x6 ==> delta_x x1 x2 x3 x4 x5 x6 >= delta_x x1 x2 #4.0 x4 x5 x6 \/ delta_x x1 x2 x3 x4 x5 x6 >= delta_x x1 x2 #6.3504 x4 x5 x6`,
 216    REPEAT STRIP_TAC THEN
 217      ONCE_REWRITE_TAC[SYM (BETA_CONV `(\x. delta_x x1 x2 x x4 x5 x6) x3`)] THEN
 218      MATCH_MP_TAC lemma' THEN
 219      ASM_REWRITE_TAC[Sphere.delta_x; FUN_EQ_THM] THEN
 220      MAP_EVERY EXISTS_TAC [`--x6`; `x6*(x1+x2-x6+x4+x5)+x1*x4+x2*x5-x2*x4-x1*x5`; `x2*x5*(x1-x2+x4-x5+x6) + x1*x4*(--x1+x2-x4+x5+x6)-x1*x2*x6-x4*x5*x6`] THEN
 221      POP_ASSUM MP_TAC THEN REAL_ARITH_TAC);;
 222
 223
 224
 225 let lemma6 = prove(`!x1 x2 x3 x4 x5 x6. #0.64 <= x6 /\ x6 <= #6.3504 /\ #4.0 <= x3 ==> delta_x x1 x2 x3 x4 x5 x6 >= delta_x x1 x2 x3 x4 x5 #0.64 \/ delta_x x1 x2 x3 x4 x5 x6 >= delta_x x1 x2 x3 x4 x5 #6.3504`,
 226    REPEAT STRIP_TAC THEN
 227      ONCE_REWRITE_TAC[SYM (BETA_CONV `(\x. delta_x x1 x2 x3 x4 x5 x) x6`)] THEN
 228      MATCH_MP_TAC lemma' THEN
 229      ASM_REWRITE_TAC[Sphere.delta_x; FUN_EQ_THM] THEN
 230      MAP_EVERY EXISTS_TAC [`--x3`; `x3*(x1+x2-x3+x4+x5)+x1*x4+x2*x5-x1*x2-x4*x5`; `x2*x5*(x1-x2+x3+x4-x5) + x1*x4*(--x1+x2+x3-x4+x5)-x2*x3*x4-x1*x3*x5`] THEN
 231      POP_ASSUM MP_TAC THEN REAL_ARITH_TAC);;
 232
 233
 234
 235 (* delta_x > 0 for a special configuration of three points *)
 236
 237 let delta_x_3_points = prove(`!x1 x2 x3 x6. ineq [#4.0,x1,#6.3504;
 238                                                   #4.0,x2,#6.3504;
 239                                                   #4.0,x3,#6.3504;
 240                                                   #0.64,x6,#6.3504] (delta_x x1 x2 x3 (#4.0) (#4.0) x6 >= #13.0)`,
 241    REPEAT STRIP_TAC THEN
 242      REWRITE_TAC[INEQ_ALT; ALL] THEN
 243      REPEAT STRIP_TAC THEN
 244      ASSUME_TAC (REAL_ARITH `#4.0 <= #4.0 /\ #4.0 <= #6.3504`) THEN
 245
 246      (* x1 *)
 247      ONCE_REWRITE_TAC[SYM (BETA_CONV `(\x. delta_x x x2 x3 x4 x5 x6) x1`)] THEN
 248      MATCH_MP_TAC main_lemma THEN
 249      MAP_EVERY EXISTS_TAC [`#4.0`; `#6.3504`] THEN
 250      ASM_SIMP_TAC[lemma1] THEN
 251      CONJ_TAC THEN
 252
 253      (* x2 *)
 254      ONCE_REWRITE_TAC[SYM (BETA_CONV `(\x. delta_x x1 x x3 x4 x5 x6) x2`)] THEN
 255      MATCH_MP_TAC main_lemma THEN
 256      MAP_EVERY EXISTS_TAC [`#4.0`; `#6.3504`] THEN
 257      ASM_SIMP_TAC[lemma2] THEN
 258      CONJ_TAC THEN
 259
 260      (* x3 *)
 261      ONCE_REWRITE_TAC[SYM (BETA_CONV `(\x. delta_x x1 x2 x x4 x5 x6) x3`)] THEN
 262      MATCH_MP_TAC main_lemma THEN
 263      MAP_EVERY EXISTS_TAC [`#4.0`; `#6.3504`] THEN
 264      ASM_SIMP_TAC[lemma3] THEN
 265      CONJ_TAC THEN
 266
 267      (* x6 *)
 268      ONCE_REWRITE_TAC[SYM (BETA_CONV `(\x. delta_x x1 x2 x3 x4 x5 x) x6`)] THEN
 269      MATCH_MP_TAC main_lemma THEN
 270      MAP_EVERY EXISTS_TAC [`#0.64`; `#6.3504`] THEN
 271      ASM_SIMP_TAC[lemma6] THEN
 272      CONJ_TAC THEN
 273
 274      (* Final stage *)
 275      REWRITE_TAC[Sphere.delta_x] THEN
 276      CONV_TAC REAL_RAT_REDUCE_CONV);;
 277
 278
 279
 280 (************************************************************)
 281
 282
 283 (* eta_y pow 2 <= #2.2 *)
 284
 285
 286 let lemma1 = prove(`!x1 x2 x3. #4.0 <= x1 /\ x1 <= #6.3504 ==>
 287                      #2.2 * ups_x x1 x2 x3 - x1 * x2 * x3 >= #2.2 * ups_x #4.0 x2 x3 - #4.0 * x2 * x3 \/
 288                      #2.2 * ups_x x1 x2 x3 - x1 * x2 * x3 >= #2.2 * ups_x #6.3504 x2 x3 - #6.3504 * x2 * x3`,
 289    REPEAT STRIP_TAC THEN
 290      ONCE_REWRITE_TAC[SYM (BETA_CONV `(\x. #2.2 * ups_x x x2 x3 - x * x2 * x3) x1`)] THEN
 291      MATCH_MP_TAC lemma' THEN
 292      ASM_REWRITE_TAC[Sphere.ups_x; FUN_EQ_THM] THEN
 293      MAP_EVERY EXISTS_TAC [`-- #2.2`; `#2.2*(&2 * x3 + &2 * x2) - x2 * x3`; `#2.2 * (&2 * x2 * x3 - x2*x2 - x3*x3)`] THEN
 294      REAL_ARITH_TAC);;
 295
 296
 297 let lemma2 = prove(`!x1 x2 x3. #4.0 <= x2 /\ x2 <= #6.3504 ==>
 298                      #2.2 * ups_x x1 x2 x3 - x1 * x2 * x3 >= #2.2 * ups_x x1 #4.0 x3 - x1 * #4.0 * x3 \/
 299                      #2.2 * ups_x x1 x2 x3 - x1 * x2 * x3 >= #2.2 * ups_x x1 #6.3504 x3 - x1 * #6.3504 * x3`,
 300    REPEAT STRIP_TAC THEN
 301      ONCE_REWRITE_TAC[SYM (BETA_CONV `(\x. #2.2 * ups_x x1 x x3 - x1 * x * x3) x2`)] THEN
 302      MATCH_MP_TAC lemma' THEN
 303      ASM_REWRITE_TAC[Sphere.ups_x; FUN_EQ_THM] THEN
 304      MAP_EVERY EXISTS_TAC [`-- #2.2`; `#2.2*(&2 * x1 + &2 * x3) - x1 * x3`; `#2.2 * (&2 * x1 * x3 - x1*x1 - x3*x3)`] THEN
 305      REAL_ARITH_TAC);;
 306
 307
 308 let lemma3 = prove(`!x1 x2 x3. #4.0 <= x3 /\ x3 <= #6.3504 ==>
 309                      #2.2 * ups_x x1 x2 x3 - x1 * x2 * x3 >= #2.2 * ups_x x1 x2 #4.0 - x1 * x2 * #4.0 \/
 310                      #2.2 * ups_x x1 x2 x3 - x1 * x2 * x3 >= #2.2 * ups_x x1 x2 #6.3504 - x1 * x2 * #6.3504`,
 311    REPEAT STRIP_TAC THEN
 312      ONCE_REWRITE_TAC[SYM (BETA_CONV `(\x. #2.2 * ups_x x1 x2 x - x1 * x2 * x) x3`)] THEN
 313      MATCH_MP_TAC lemma' THEN
 314      ASM_REWRITE_TAC[Sphere.ups_x; FUN_EQ_THM] THEN
 315      MAP_EVERY EXISTS_TAC [`-- #2.2`; `#2.2*(&2 * x1 + &2 * x2) - x2 * x1`; `#2.2 * (&2 * x2 * x1 - x2*x2 - x1*x1)`] THEN
 316      REAL_ARITH_TAC);;
 317
 318
 319
 320 let eta_x_ineq_lemma = prove(`!x1 x2 x3. ineq [#4.0,x1,#6.3504;
 321                                                   #4.0,x2,#6.3504;
 322                                                   #4.0,x3,#6.3504]
 323                                                    (#2.2 * ups_x x1 x2 x3 - x1 * x2 * x3 >= &0)`,
 324    REPEAT STRIP_TAC THEN
 325      REWRITE_TAC[INEQ_ALT; ALL] THEN
 326      REPEAT STRIP_TAC THEN
 327      ASSUME_TAC (REAL_ARITH `#4.0 <= #4.0 /\ #4.0 <= #6.3504`) THEN
 328
 329      (* x1 *)
 330      ONCE_REWRITE_TAC[SYM (BETA_CONV `(\x. #2.2 * ups_x x x2 x3 - x * x2 * x3) x1`)] THEN
 331      MATCH_MP_TAC main_lemma THEN
 332      MAP_EVERY EXISTS_TAC [`#4.0`; `#6.3504`] THEN
 333      ASM_SIMP_TAC[lemma1] THEN
 334      CONJ_TAC THEN
 335
 336      (* x2 *)
 337      ONCE_REWRITE_TAC[SYM (BETA_CONV `(\x. #2.2 * ups_x x1 x x3 - x1 * x * x3) x2`)] THEN
 338      MATCH_MP_TAC main_lemma THEN
 339      MAP_EVERY EXISTS_TAC [`#4.0`; `#6.3504`] THEN
 340      ASM_SIMP_TAC[lemma2] THEN
 341      CONJ_TAC THEN
 342
 343      (* x3 *)
 344      ONCE_REWRITE_TAC[SYM (BETA_CONV `(\x. #2.2 * ups_x x1 x2 x - x1 * x2 * x) x3`)] THEN
 345      MATCH_MP_TAC main_lemma THEN
 346      MAP_EVERY EXISTS_TAC [`#4.0`; `#6.3504`] THEN
 347      ASM_SIMP_TAC[lemma3] THEN
 348      CONJ_TAC THEN
 349
 350      (* Final stage *)
 351      REWRITE_TAC[Sphere.ups_x] THEN
 352      CONV_TAC REAL_RAT_REDUCE_CONV);;
 353
 354
 355
 356 let ETA_Y_4_POINTS_INEQ = prove(`!y1 y2 y3. ineq[(&2, y1, &2 * h0); (&2, y2, &2 * h0); (&2, y3, &2 * h0)]
 357                                            (eta_y y1 y2 y3 pow 2 <= #2.2)`,
 358    REWRITE_TAC[INEQ_ALT; ALL; Sphere.h0; REAL_ARITH `&2 * #1.26 = #2.52`] THEN
 359      REPEAT GEN_TAC THEN DISCH_TAC THEN
 360      REWRITE_TAC[Sphere.eta_y; Sphere.eta_x] THEN
 361      CONV_TAC (DEPTH_CONV let_CONV) THEN
 362      MAP_EVERY ABBREV_TAC [`x1 = y1 * y1:real`; `x2 = y2 * y2:real`; `x3 = y3 * y3:real`] THEN
 363      SUBGOAL_THEN `!y. &2 <= y /\ y <= #2.52 ==> #4.0 <= y * y /\ y * y <= #6.3504` ASSUME_TAC THENL
 364      [
 365        GEN_TAC THEN
 366          REWRITE_TAC[REAL_ARITH `#4.0 = &2 * &2`; REAL_ARITH `#6.3504 = #2.52 * #2.52`] THEN
 367          REWRITE_TAC[GSYM REAL_POW_2] THEN
 368          REWRITE_TAC[GSYM REAL_LE_SQUARE_ABS] THEN
 369          REAL_ARITH_TAC;
 370        ALL_TAC
 371      ] THEN
 372      MAP_EVERY (fun tm -> FIRST_ASSUM (MP_TAC o SPEC tm)) [`y1:real`; `y2:real`; `y3:real`] THEN
 373      REMOVE_ASSUM THEN ASM_REWRITE_TAC[] THEN
 374      REPEAT DISCH_TAC THEN
 375      MP_TAC (SPEC_ALL eta_x_ineq_lemma) THEN
 376      ASM_REWRITE_TAC[INEQ_ALT; ALL] THEN
 377      DISCH_TAC THEN
 378
 379      SUBGOAL_THEN `&0 < x1 * x2 * x3` ASSUME_TAC THENL
 380      [
 381        ASSUME_TAC (REAL_ARITH `!x. #4.0 <= x ==> &0 < x`) THEN
 382          MATCH_MP_TAC REAL_LT_MUL THEN ASM_SIMP_TAC[] THEN
 383          MATCH_MP_TAC REAL_LT_MUL THEN ASM_SIMP_TAC[];
 384        ALL_TAC
 385      ] THEN
 386
 387      SUBGOAL_THEN `&0 < ups_x x1 x2 x3` ASSUME_TAC THENL
 388      [
 389        MATCH_MP_TAC (REAL_ARITH `#2.2 * u - x1 * x2 * x3 >= &0 /\ &0 < x1 * x2 * x3 ==> &0 < u`) THEN
 390          ASM_REWRITE_TAC[];
 391        ALL_TAC
 392      ] THEN
 393
 394      SUBGOAL_THEN `&0 <= (x1 * x2 * x3) / ups_x x1 x2 x3` ASSUME_TAC THENL
 395      [
 396        MATCH_MP_TAC REAL_LE_DIV THEN
 397          ASM_SIMP_TAC[REAL_LT_IMP_LE];
 398        ALL_TAC
 399      ] THEN
 400      ASM_SIMP_TAC[SQRT_POW_2] THEN
 401      ONCE_REWRITE_TAC[REAL_ARITH `#2.2 = #2.2 / &1`] THEN
 402      ASSUME_TAC (REAL_ARITH `&0 < &1`) THEN
 403      ASM_SIMP_TAC[RAT_LEMMA4] THEN
 404      REPLICATE_TAC 4 REMOVE_ASSUM THEN POP_ASSUM MP_TAC THEN
 405      REAL_ARITH_TAC);;
 406
 407
 408
 409
 410
 411
 412
 413
 414 (*************************************************************)
 415
 416
 417
 418
 419
 420
 421
 422 let DELTA_X4_MONO_LT_4 = prove(`!x1 x2 x3 a x5 x6 b. a < b /\ &0 < x1
 423                               ==> delta_x4 x1 x2 x3 b x5 x6 <
 424                                      delta_x4 x1 x2 x3 a x5 x6`,
 425   REPEAT STRIP_TAC THEN
 426     REWRITE_TAC[Sphere.delta_x4] THEN
 427     REWRITE_TAC[REAL_ARITH `a - b + c + d - e + f < a - g + c + d - e + h <=> f - b < h - g`] THEN
 428     REWRITE_TAC[REAL_ARITH `x1*(--x1+x2+x3-b+x5+x6)-x1*b = --(&2*x1*b) + x1*(--x1+x2+x3+x5+x6)`] THEN
 429     REWRITE_TAC[REAL_ARITH `--a + b < --c + b <=> c < a`] THEN
 430     MATCH_MP_TAC REAL_LT_LMUL THEN
 431     REWRITE_TAC[REAL_ARITH `&0 < &2`] THEN
 432     MATCH_MP_TAC REAL_LT_LMUL THEN
 433     ASM_REWRITE_TAC[]);;
 434
 435
 436
 437 let DELTA_X4_MONO_LE_4 = prove(`!x1 x2 x3 a x5 x6 b. a < b /\ &0 <= x1
 438                                  ==> delta_x4 x1 x2 x3 b x5 x6 <=
 439                                         delta_x4 x1 x2 x3 a x5 x6`,
 440    REPEAT STRIP_TAC THEN
 441      MP_TAC (REAL_ARITH `&0 <= x1 ==> x1 = &0 \/ &0 < x1`) THEN
 442      ASM_REWRITE_TAC[] THEN
 443      STRIP_TAC THENL
 444      [
 445        ASM_REWRITE_TAC[Sphere.delta_x4] THEN
 446          REAL_ARITH_TAC;
 447        MATCH_MP_TAC REAL_LT_IMP_LE THEN
 448          ASM_SIMP_TAC[DELTA_X4_MONO_LT_4]
 449      ]);;
 450
 451
 452
 453 let REAL_LT_SQUARE_POS = prove(`!x y. &0 < x /\ x < y ==> x pow 2 < y pow 2`,
 454    REPEAT STRIP_TAC THEN
 455      REWRITE_TAC[GSYM REAL_LT_SQUARE_ABS] THEN
 456      SUBGOAL_THEN `abs x = x` ASSUME_TAC THENL
 457      [
 458        ASM_SIMP_TAC[REAL_ABS_REFL; REAL_LT_IMP_LE];
 459        ALL_TAC
 460      ] THEN
 461      SUBGOAL_THEN `abs y = y` ASSUME_TAC THENL
 462      [
 463        ASM_REWRITE_TAC[REAL_ABS_REFL] THEN
 464          MATCH_MP_TAC REAL_LT_IMP_LE THEN
 465          MATCH_MP_TAC REAL_LT_TRANS THEN
 466          EXISTS_TAC `x:real` THEN
 467          ASM_REWRITE_TAC[];
 468        ALL_TAC
 469      ] THEN
 470      ASM_REWRITE_TAC[]);;
 471
 472
 473
 474 let ATN2_ACS_LEMMA = prove(`!a b. b * b < a ==>
 475                              pi / &2 + atn2(sqrt(a - b*b), --b) = acs(b/sqrt(a))`,
 476    REPEAT STRIP_TAC THEN
 477      SUBGOAL_THEN `&0 < a` ASSUME_TAC THENL
 478      [
 479        MATCH_MP_TAC REAL_LET_TRANS THEN
 480          EXISTS_TAC `b*b:real` THEN
 481          ASM_REWRITE_TAC[REAL_LE_SQUARE];
 482        ALL_TAC
 483      ] THEN
 484
 485      MP_TAC (REAL_ARITH `&0 < a ==> &0 <= a`) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
 486
 487      SUBGOAL_THEN `sqrt a pow 2 = a` ASSUME_TAC THENL
 488      [
 489        ASM_REWRITE_TAC[SQRT_POW2];
 490        ALL_TAC
 491      ]  THEN
 492
 493      SUBGOAL_THEN `atn2 (sqrt(a - b*b),--b) = --atn2(sqrt(a-b*b),b)` MP_TAC THENL
 494      [
 495        MATCH_MP_TAC Trigonometry1.ATN2_RNEG THEN
 496          DISJ2_TAC THEN
 497          MATCH_MP_TAC SQRT_POS_LT THEN
 498          ASM_REWRITE_TAC[REAL_ARITH `&0 < a - b <=> b < a`];
 499        ALL_TAC
 500      ] THEN
 501
 502      DISCH_THEN (fun th -> REWRITE_TAC[th; REAL_ARITH `a + --b = a - b`]) THEN
 503      SUBGOAL_THEN `atn2(sqrt(a - b*b), b) = atn2(sqrt(&1 - (b/sqrt a) pow 2),b/sqrt a)` MP_TAC THENL
 504      [
 505        MP_TAC (SPECL [`sqrt(&1 - (b/sqrt a) pow 2)`; `sqrt a`; `b/sqrt a`] (GEN_ALL Trigonometry2.POS_COMPATIBLE_WITH_ATN2)) THEN
 506          SUBGOAL_THEN `&0 < sqrt a` ASSUME_TAC THENL
 507          [
 508            MATCH_MP_TAC SQRT_POS_LT THEN
 509              ASM_REWRITE_TAC[];
 510            ALL_TAC
 511          ] THEN
 512          ASM_REWRITE_TAC[] THEN
 513          DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
 514          ASM_SIMP_TAC[REAL_FIELD `&0 < a ==> a * b / a = b`] THEN
 515
 516          SUBGOAL_THEN `a - b*b = (sqrt a) pow 2 * (&1 - (b/sqrt a) pow 2)` MP_TAC THENL
 517          [
 518            ASM_REWRITE_TAC[REAL_POW_DIV] THEN
 519              ASM_SIMP_TAC[REAL_FIELD `&0 < a ==> a * (&1 - b/a) = a - b`] THEN
 520              REWRITE_TAC[REAL_POW_2];
 521            ALL_TAC
 522          ] THEN
 523
 524          DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
 525          MP_TAC (SPECL [`sqrt a pow 2`; `&1 - (b/sqrt a) pow 2`] SQRT_MUL) THEN
 526          ANTS_TAC THENL
 527          [
 528            ASM_REWRITE_TAC[REAL_POW_DIV] THEN
 529              REWRITE_TAC[REAL_ARITH `&0 <= &1 - b <=> b <= &1`] THEN
 530              MATCH_MP_TAC Trigonometry2.REAL_LE_LDIV THEN
 531              ASM_SIMP_TAC[REAL_POW_2; REAL_ARITH `b < a ==> b <= a`];
 532            ALL_TAC
 533          ] THEN
 534
 535          DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
 536          ASM_REWRITE_TAC[];
 537        ALL_TAC
 538      ] THEN
 539
 540      DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
 541      MATCH_MP_TAC (GSYM Trigonometry2.acs_atn2) THEN
 542      REWRITE_TAC[REAL_ARITH `-- &1 <= x /\ x <= &1 <=> abs x <= &1`] THEN
 543      ONCE_REWRITE_TAC[REAL_ARITH `&1 = abs(&1)`] THEN
 544      REWRITE_TAC[REAL_LE_SQUARE_ABS] THEN
 545      REWRITE_TAC[REAL_POW_DIV] THEN
 546      ASM_REWRITE_TAC[REAL_POW_2; REAL_ARITH `&1 * &1 = &1`] THEN
 547      MATCH_MP_TAC Trigonometry2.REAL_LE_LDIV THEN
 548      ASM_SIMP_TAC[REAL_ARITH `b < a ==> b <= a`]);;
 549
 550
 551
 552 let DELTA_X_AND_DELTA_X4 = prove(`!x1 x2 x3 x4 x5 x6.
 553                                  (let d4 = delta_x4 x1 x2 x3 x4 x5 x6 in
 554                                  let d = delta_x x1 x2 x3 x4 x5 x6 in
 555                                  let v1 = ups_x x1 x2 x6 in
 556                                  let v2 = ups_x x1 x3 x5 in
 557                                  &4 * x1 * d = v1 * v2 - d4 * d4)`,
 558   REPEAT GEN_TAC THEN
 559     REPEAT (CONV_TAC let_CONV) THEN
 560     REWRITE_TAC[Sphere.delta_x4; Sphere.delta_x; Sphere.ups_x] THEN
 561     REAL_ARITH_TAC);;
 562
 563
 564 let DELTA_EQ_DELTA_X = prove(`!x1 x2 x3 x4 x5 x6.
 565                                delta x1 x2 x3 x6 x5 x4 = delta_x x1 x2 x3 x4 x5 x6`,
 566   REPEAT GEN_TAC THEN
 567     REWRITE_TAC[Sphere.delta_x; Collect_geom.delta] THEN
 568     REAL_ARITH_TAC);;
 569
 570
 571
 572
 573
 574 let DIH_X_MONO_LT_4 = prove(`!x1 x2 x3 a x5 x6 b. a < b /\
 575                            &0 < x1 /\
 576                            &0 < delta_x x1 x2 x3 a x5 x6 /\
 577                            &0 < delta_x x1 x2 x3 b x5 x6
 578                            ==> dih_x x1 x2 x3 a x5 x6 < dih_x x1 x2 x3 b x5 x6`,
 579    REPEAT STRIP_TAC THEN
 580      REWRITE_TAC[let_RULE Sphere.dih_x] THEN
 581      ABBREV_TAC `da = delta_x x1 x2 x3 a x5 x6` THEN
 582      ABBREV_TAC `db = delta_x x1 x2 x3 b x5 x6` THEN
 583      SUBGOAL_THEN `&0 < &4 * x1 * da /\ &0 < &4 * x1 * db` MP_TAC THENL
 584      [
 585        CONJ_TAC THEN
 586          MATCH_MP_TAC REAL_LT_MUL THEN
 587          REWRITE_TAC[REAL_ARITH `&0 < &4`] THEN
 588          MATCH_MP_TAC REAL_LT_MUL THEN
 589          ASM_REWRITE_TAC[];
 590        ALL_TAC
 591      ] THEN
 592
 593      EXPAND_TAC "da" THEN EXPAND_TAC "db" THEN
 594      REWRITE_TAC[let_RULE DELTA_X_AND_DELTA_X4] THEN
 595      REWRITE_TAC[REAL_ARITH `&0 < a - b <=> b < a`] THEN
 596      ABBREV_TAC `d4a = delta_x4 x1 x2 x3 a x5 x6` THEN
 597      ABBREV_TAC `d4b = delta_x4 x1 x2 x3 b x5 x6` THEN
 598      ABBREV_TAC `v1 = ups_x x1 x2 x6` THEN
 599      ABBREV_TAC `v2 = ups_x x1 x3 x5` THEN
 600
 601      STRIP_TAC THEN
 602      FIRST_ASSUM (MP_TAC o (fun th -> MATCH_MP ATN2_ACS_LEMMA th)) THEN
 603      POP_ASSUM MP_TAC THEN
 604      FIRST_ASSUM (MP_TAC o (fun th -> MATCH_MP ATN2_ACS_LEMMA th)) THEN
 605      DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
 606      DISCH_TAC THEN
 607      DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
 608
 609      MATCH_MP_TAC ACS_MONO_LT THEN
 610      SUBGOAL_THEN `!a b. b * b < a ==> -- &1 <= b / sqrt(a) /\ b / sqrt a <= &1` ASSUME_TAC THENL
 611      [
 612        REPEAT GEN_TAC THEN DISCH_TAC THEN
 613          REWRITE_TAC[REAL_ARITH `-- &1 <= x /\ x <= &1 <=> abs x <= &1`] THEN
 614          ONCE_REWRITE_TAC[REAL_ARITH `&1 = abs(&1)`] THEN
 615          REWRITE_TAC[REAL_LE_SQUARE_ABS] THEN
 616          REWRITE_TAC[REAL_POW_DIV] THEN
 617
 618          SUBGOAL_THEN `&0 < a'` ASSUME_TAC THENL
 619          [
 620            MATCH_MP_TAC REAL_LET_TRANS THEN
 621              EXISTS_TAC `b' * b':real` THEN
 622              ASM_SIMP_TAC[REAL_LE_SQUARE; REAL_ARITH `b < a ==> b <= a`];
 623            ALL_TAC
 624          ] THEN
 625
 626          SUBGOAL_THEN `sqrt a' pow 2 = a'` (fun th -> REWRITE_TAC[th]) THENL
 627          [
 628            REWRITE_TAC[SQRT_POW2] THEN
 629              ASM_SIMP_TAC[REAL_ARITH `&0 < a ==> &0 <= a`];
 630            ALL_TAC
 631          ] THEN
 632
 633          ASM_REWRITE_TAC[REAL_POW_2; REAL_ARITH `&1 * &1 = &1`] THEN
 634          MATCH_MP_TAC Trigonometry2.REAL_LE_LDIV THEN
 635          ASM_SIMP_TAC[REAL_ARITH `b < a ==> b <= a`];
 636        ALL_TAC
 637      ] THEN
 638
 639      POP_ASSUM (fun th -> ASM_SIMP_TAC[th]) THEN
 640      REWRITE_TAC[real_div] THEN
 641      MATCH_MP_TAC REAL_LT_RMUL THEN
 642      REWRITE_TAC[REAL_LT_INV_EQ] THEN
 643      CONJ_TAC THENL
 644      [
 645        MP_TAC (SPEC_ALL DELTA_X4_MONO_LT_4) THEN
 646          ASM_REWRITE_TAC[];
 647        MATCH_MP_TAC SQRT_POS_LT THEN
 648          MATCH_MP_TAC REAL_LET_TRANS THEN
 649          EXISTS_TAC `d4a * d4a:real` THEN
 650          ASM_REWRITE_TAC[REAL_LE_SQUARE]
 651      ]);;
 652
 653
 654
 655
 656
 657
 658 let DIH_Y_INEQ_concl = mk_imp ((hd (Ineq.getexact "2570626711")).ineq,
 659                                  `ineq [(#2.0,y1,#2.52);
 660                                         (#2.0,y2,#2.52);
 661                                         (#2.0,y3,#2.52);
 662                                         (#2.52,y4,#5.04);
 663                                         (#2.0,y5,#2.52);
 664                                         (#2.0,y6,#2.52)]
 665                                    (dih_y y1 y2 y3 y4 y5 y6 > #1.15 \/ delta_y y1 y2 y3 y4 y5 y6 <= &0)`);;
 666
 667
 668 g(DIH_Y_INEQ_concl);;
 669 let DIH_Y_INEQ = prove(DIH_Y_INEQ_concl,
 670    REWRITE_TAC[Pack_defs.h0; REAL_ARITH `&2 * #1.26 = #2.52`] THEN
 671      REWRITE_TAC[INEQ_ALT; ALL] THEN
 672      REPEAT STRIP_TAC THEN
 673      DISJ_CASES_TAC (REAL_ARITH `delta_y y1 y2 y3 y4 y5 y6 <= &0 \/ delta_y y1 y2 y3 y4 y5 y6 > &0`) THENL
 674      [
 675        ASM_REWRITE_TAC[];
 676        ALL_TAC
 677      ] THEN
 678      DISJ1_TAC THEN
 679      REWRITE_TAC[real_gt] THEN
 680      MATCH_MP_TAC REAL_LTE_TRANS THEN
 681      EXISTS_TAC `dih_y y1 y2 y3 #2.52 y5 y6` THEN
 682      FIRST_X_ASSUM (MP_TAC o SPECL [`y1:real`; `y2:real`; `y3:real`; `#2.52`; `y5:real`; `y6:real`]) THEN
 683      ASM_SIMP_TAC[REAL_LE_REFL; real_gt] THEN
 684      DISCH_THEN (fun th -> ALL_TAC) THEN
 685      POP_ASSUM MP_TAC THEN
 686
 687      REWRITE_TAC[let_RULE Sphere.dih_y; Sphere.delta_y] THEN
 688      MAP_EVERY ABBREV_TAC [`x1 = y1 * y1`; `x2 = y2 * y2`; `x3 = y3 * y3`; `x4 = y4 * y4`; `x5 = y5 * y5`; `x6 = y6 * y6`] THEN
 689      REWRITE_TAC[REAL_ARITH `a <= b <=> a < b \/ a = b`] THEN
 690      ASM_CASES_TAC `dih_x x1 x2 x3 (#2.52 * #2.52) x5 x6 = dih_x x1 x2 x3 x4 x5 x6` THEN ASM_REWRITE_TAC[] THEN
 691      REWRITE_TAC[real_gt] THEN
 692      DISCH_TAC THEN
 693      MATCH_MP_TAC DIH_X_MONO_LT_4 THEN
 694      POP_ASSUM (fun th -> REWRITE_TAC[th]) THEN
 695
 696      SUBGOAL_THEN `!y. #2.0 <= y /\ y <= #2.52 ==> #4.0 <= y * y /\ y * y <= #6.3504` ASSUME_TAC THENL
 697      [
 698        GEN_TAC THEN REWRITE_TAC[REAL_ARITH `#4.0 = #2.0 * #2.0`; REAL_ARITH `#6.3504 = #2.52 * #2.52`] THEN
 699          REWRITE_TAC[GSYM REAL_POW_2] THEN
 700          REWRITE_TAC[GSYM REAL_LE_SQUARE_ABS] THEN
 701          REAL_ARITH_TAC;
 702        ALL_TAC
 703      ] THEN
 704
 705      SUBGOAL_THEN `#2.52 * #2.52 < x4` (fun th -> REWRITE_TAC[th]) THENL
 706      [
 707        EXPAND_TAC "x4" THEN
 708          REWRITE_TAC[GSYM REAL_POW_2] THEN
 709          MATCH_MP_TAC REAL_LT_SQUARE_POS THEN
 710          ASM_REWRITE_TAC[REAL_ARITH `&0 < #2.52`; REAL_ARITH `a < b <=> a <= b /\ ~(a = b)`] THEN
 711          REMOVE_ASSUM THEN POP_ASSUM MP_TAC THEN
 712          REWRITE_TAC[CONTRAPOS_THM] THEN
 713          EXPAND_TAC "x4" THEN
 714          DISCH_THEN (fun th -> REWRITE_TAC[GSYM th]);
 715        ALL_TAC
 716      ] THEN
 717
 718      MAP_EVERY (fun tm -> FIRST_ASSUM (MP_TAC o SPEC tm)) [`y1:real`; `y2:real`; `y3:real`; `y5:real`; `y6:real`] THEN
 719      REMOVE_ASSUM THEN REMOVE_ASSUM THEN
 720      REPLICATE_TAC 6 (POP_ASSUM (fun th -> REWRITE_TAC[th])) THEN
 721      ASM_REWRITE_TAC[] THEN
 722      REPEAT REMOVE_ASSUM THEN REPEAT DISCH_TAC THEN
 723      ASM_SIMP_TAC[REAL_ARITH `#4.0 <= x1 ==> &0 < x1`] THEN
 724      MATCH_MP_TAC REAL_LTE_TRANS THEN
 725      EXISTS_TAC `#128.0` THEN
 726      REWRITE_TAC[REAL_ARITH `&0 < #128.0`; GSYM real_ge] THEN
 727
 728      MP_TAC delta_x_pos THEN
 729      REWRITE_TAC[INEQ_ALT; ALL] THEN
 730      DISCH_THEN MATCH_MP_TAC THEN
 731      ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);;
 732
 733
 734
 735
 736
 737
 738
 739
 740 end;;