1 (* ========================================================================== *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
3 (* Section: Conclusions *)
4 (* Chapter: Tame (Linear Programs) *)
5 (* Author: Thomas C. Hales *)
7 (* ========================================================================== *)
10 Treatment of two special inequalities for the linear programs.
14 LEMMA_8673686234 (uses inequalities "6170936724","8673686234 a","8673686234 b","8673686234 c")
15 see head.mod:yapex_sup_flat 'ID[8673686234]'
17 LEMMA_5691615370 (uses inequalities "5584033259","6170936724","5691615370")
18 see head.mod:perimZ 'ID[5691615370]'
22 module Lp_details = struct
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`,
32 REPEAT WEAKER_STRIP_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;
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;
43 GMATCH_SIMP_TAC REAL_LE_MUL;
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)
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)`,
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);
67 MATCH_MP_TAC (REWRITE_RULE[LET_DEF;LET_END_DEF] Tame_lemmas.quadratic_root_plus_works);
69 BY(ASM_TAC THEN REAL_ARITH_TAC);
71 BY(MESON_TAC[REAL_LE_TRANS;REAL_LE_POW_2]);
72 MATCH_MP_TAC (arith `&0 <= h ==> x <= x + h`);
74 REWRITE_TAC[Sphere.quadratic_root_plus];
75 GMATCH_SIMP_TAC REAL_LE_RDIV_EQ;
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))`;
80 GMATCH_SIMP_TAC SQRT_MONO_LE_EQ;
81 REWRITE_TAC[POW_2_SQRT_ABS];
86 BY(REWRITE_TAC[REAL_LE_POW_2]);
87 BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC)
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)`,
96 REPEAT WEAKER_STRIP_TAC;
97 INTRO_TAC quadratic_root_exists [`--a`;`--b`;`--c`;`x`];
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)
106 let delta_x_root_exists = prove_by_refinement(
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)`,
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);
118 REWRITE_TAC[Sphere.delta_x;Sphere.delta_x4];
121 MATCH_MP_TAC quadratic_root_pos_exists;
122 FIRST_X_ASSUM ((unlist REWRITE_TAC) o GSYM);
124 BY(ASM_TAC THEN REAL_ARITH_TAC)
128 let delta_y_root_exists = prove_by_refinement(
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)`,
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`];
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[]);
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)
163 let edge2_flatD_x1_quadratic_root_plus = prove_by_refinement(
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 )`,
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));
178 REWRITE_TAC[Sphere.delta_x;Nonlin_def.delta_x1];
180 ASM_REWRITE_TAC[Nonlinear_lemma.abc_quadratic];
184 let edge2_flatD_x1_expanded = prove_by_refinement(
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)
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);
199 REWRITE_TAC[Sphere.delta_x;Nonlin_def.delta_x1;Sphere.ups_x];
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)
211 (\q. edge2_flatD_x1 (&0) q x3 x4 x5 x6) f' x2 (:real))`,
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;
226 BY(ASM_TAC THEN REAL_ARITH_TAC)
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)`,
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])
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) /\
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))`,
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`];
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;
269 INTRO_TAC REAL_IVT_INCREASING [`(\q. edge2_flatD_x1 (&0) q x3 x4 x5 x6)`;`x2`;`x2M`;`x1m`];
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;
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;
285 FIRST_X_ASSUM MATCH_MP_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;
292 BY(ASM_TAC THEN REAL_ARITH_TAC)
296 let edge2_flatD_x1_works = prove_by_refinement(
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`,
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));
310 REWRITE_TAC[Sphere.delta_x;Nonlin_def.delta_x1];
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);
317 REWRITE_TAC[Sphere.delta_x;Nonlin_def.delta_x1;Sphere.ups_x];
320 GMATCH_SIMP_TAC REAL_LE_MUL;
321 BY(ASM_REWRITE_TAC[])
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`,
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;
338 GMATCH_SIMP_TAC REAL_LE_MUL;
339 BY(ASM_TAC THEN REAL_ARITH_TAC);
340 REWRITE_TAC[Nonlin_def.delta_x1];
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 /\
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)`,
360 REPEAT WEAKER_STRIP_TAC;
361 INTRO_TAC IVT_edge2_flatD_x1 [`x1m`;`x1M`;`x2m`;`x2M`;`x3`;`x4`;`x5`;`x6`];
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`]);
373 TYPIFY `x2` EXISTS_TAC;
376 MATCH_MP_TAC edge2_flatD_x1_works;
377 BY(ASM_SIMP_TAC[arith `x < y ==> x <= y`;arith `&0 < x ==> ~(x = &0)`]);
379 TYPIFY `edge2_flatD_x1 (&0) x2m x3 x4 x5 x6` EXISTS_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)
389 let delta_x1_sym = prove_by_refinement(
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`,
395 REWRITE_TAC[Nonlin_def.delta_x1];
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 /\
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)`,
415 REPEAT WEAKER_STRIP_TAC;
416 INTRO_TAC IVT_delta_x [`x1m`;`x1M`;`x3m`;`x3M`;`x2`;`x4`;`x6`;`x5`];
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[]);
425 FIRST_X_ASSUM_ST `ups_x` MP_TAC;
426 BY(MESON_TAC[Collect_geom.UPS_X_SYM]);
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])
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 /\
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)`,
449 REPEAT WEAKER_STRIP_TAC;
450 INTRO_TAC IVT_delta_x [`x1m`;`x1M`;`x5m`;`x5M`;`x6`;`x4`;`x2`;`x3`];
454 REPEAT WEAKER_STRIP_TAC;
455 BY(ASM_MESON_TAC[Collect_geom.UPS_X_SYM]);
457 BY(ASM_MESON_TAC[Collect_geom.UPS_X_SYM]);
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])
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 /\
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)`,
480 REPEAT WEAKER_STRIP_TAC;
481 INTRO_TAC IVT_delta_x [`x1m`;`x1M`;`x6m`;`x6M`;`x5`;`x4`;`x3`;`x2`];
485 REPEAT WEAKER_STRIP_TAC;
486 BY(ASM_MESON_TAC[Collect_geom.UPS_X_SYM]);
488 BY(ASM_MESON_TAC[Collect_geom.UPS_X_SYM]);
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])
496 let IVT_delta_x_full = prove_by_refinement(
497 `!x1m x1M x2m x2M x3m x3M x4 x5m x5M x6m x6M.
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 /\
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)
514 REPEAT WEAKER_STRIP_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`];
523 REPEAT WEAKER_STRIP_TAC;
524 FIRST_X_ASSUM MATCH_MP_TAC;
525 BY(ASM_REWRITE_TAC[arith `x <= x`]);
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`]);
533 FIRST_X_ASSUM MP_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`];
539 DISCH_THEN MP_TAC THEN ANTS_TAC;
541 REPEAT WEAKER_STRIP_TAC;
542 FIRST_X_ASSUM MATCH_MP_TAC;
543 BY(ASM_REWRITE_TAC[arith `x <= x`]);
545 FIRST_X_ASSUM MATCH_MP_TAC;
546 BY(ASM_REWRITE_TAC[arith `x <= x`]);
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`]);
553 FIRST_X_ASSUM MP_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`];
559 DISCH_THEN MP_TAC THEN ANTS_TAC;
561 REPEAT WEAKER_STRIP_TAC;
562 FIRST_X_ASSUM MATCH_MP_TAC;
563 BY(ASM_REWRITE_TAC[arith `x <= x`]);
565 FIRST_X_ASSUM MATCH_MP_TAC;
566 BY(ASM_REWRITE_TAC[arith `x <= x`]);
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`]);
573 FIRST_X_ASSUM MP_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`];
579 DISCH_THEN MP_TAC THEN ANTS_TAC;
581 REPEAT WEAKER_STRIP_TAC;
582 FIRST_X_ASSUM MATCH_MP_TAC;
583 BY(ASM_REWRITE_TAC[arith `x <= x`]);
585 FIRST_X_ASSUM MATCH_MP_TAC;
586 BY(ASM_REWRITE_TAC[arith `x <= x`]);
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`]);
593 FIRST_X_ASSUM MP_TAC;
595 FIRST_X_ASSUM MATCH_MP_TAC;
596 BY(ASM_REWRITE_TAC[arith `x <= x`]);
597 FIRST_X_ASSUM MP_TAC;
599 FIRST_X_ASSUM MATCH_MP_TAC;
600 BY(REPLICATE_TAC 4 (FIRST_X_ASSUM_ST `<` MP_TAC) THEN REAL_ARITH_TAC)
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)))`,
610 REPEAT WEAKER_STRIP_TAC;
611 MATCH_MP_TAC (TAUT `(a ==> b) /\ (b ==> a) ==> (a <=> b)`);
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);
631 GMATCH_SIMP_TAC SQRT_POS_LE;
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[])
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)))`,
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[])
655 let IVT_delta_y_full = prove_by_refinement(
656 `!y1m y1M y2m y2M y3m y3M y4 y5m y5M y6m y6M.
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 /\
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)
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`];
681 ASM_REWRITE_TAC[GSYM Sphere.delta_y];
683 GMATCH_SIMP_TAC REAL_LT_MUL_EQ;
684 BY(ASM_REWRITE_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;
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);
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;
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;
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);
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;
709 REWRITE_TAC[Sphere.delta_y];
710 GMATCH_SIMP_TAC (GSYM EXISTS_BIJ_SQUARE);
712 TYPIFY `x2` EXISTS_TAC;
714 GMATCH_SIMP_TAC (GSYM EXISTS_BIJ_SQUARE);
716 TYPIFY `x3` EXISTS_TAC;
718 GMATCH_SIMP_TAC (GSYM EXISTS_BIJ_SQUARE);
720 TYPIFY `x5` EXISTS_TAC;
722 GMATCH_SIMP_TAC (GSYM EXISTS_BIJ_SQUARE);
724 TYPIFY `x6` EXISTS_TAC;
725 BY(ASM_REWRITE_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;
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])
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)
744 P y1 y2 y3 y4 y5 y6) ==>
745 (!y1 y2 y3 y4 y5 y6. P y1 y2 y3 y4 y5 y6)`,
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[])
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) /\
767 P y1 y2 y3 y4 y5 y6) ==>
768 (!y1 y2 y3 y4 y5 y6. P y1 y2 y3 y4 y5 y6)`,
773 MATCH_MP_TAC REAL_WLOG_DS_LEMMA;
775 BY(ASM_MESON_TAC[arith `y3 <= y6 \/ y6 <= y3`;arith `y3 <= y3`])
780 let WLOG_8673686234 = prove_by_refinement(
781 `(!y1 y2 y3 y4 y5 y6.
782 y3 <= y2 /\ y5 <= y2 /\ y6 <= y2 ==>
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 [
801 ((y2 + y3 + y5 + y6 - #7.99 > #2.75 * (y1 - sqrt8)) \/
802 (delta_y y1 y2 y3 y4 y5 y6 < &0) \/
807 MATCH_MP_TAC REAL_WLOG_DS_LEMMA;
811 REPEAT WEAKER_STRIP_TAC;
812 REWRITE_TAC[Sphere.ineq];
813 REWRITE_TAC[Merge_ineq.delta_y_sym];
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]);
823 (* Prove "8673686234" using inequalities
824 "6170936724", "8673686234 a", "8673686234 b", "8673686234 c" *)
826 let LEMMA_8673686234 = prove_by_refinement(
828 (!y1 y2 y3 y4 y5 y6. ineq [
836 ( y_of_x delta_x1 y1 y2 y3 y4 y5 y6 < &0)) /\
838 (!y1 y2 y3 y4 y5 y6. ineq [
846 ((y2 + y3 + y5 + y6 - #7.99 - #0.00385 * delta_y y1 y2 y3 y4 y5 y6 > #2.75 * ((y1 + y4)/ &2 - sqrt8))
849 (!y1 y2 y3 y4 y5 y6. ineq [
857 ((y2 + y3 + y5 + y6 - #7.99 > #2.75 * (y1 - sqrt8)) \/
858 (delta_y y1 y2 y3 y4 y5 y6 < &0) ) ) /\
860 (!y1 y2 y3 y4 y5 y6. ineq [
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 [
879 ((y2 + y3 + y5 + y6 - #7.99 > #2.75 * (y1 - sqrt8)) \/
880 (delta_y y1 y2 y3 y4 y5 y6 < &0) \/
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;
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);
897 FIRST_X_ASSUM_ST `&2,y2,#2.07` kill;
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);
905 FIRST_X_ASSUM_ST `ineq` kill;
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]);
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;
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`];
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]);
946 FIRST_X_ASSUM_ST `ineq` kill;
948 BY(ASM_TAC THEN MP_TAC Flyspeck_constants.bounds THEN REAL_ARITH_TAC);
950 REPEAT WEAKER_STRIP_TAC;
951 MATCH_MP_TAC Merge_ineq.UPS_X_POS;
953 BY(MP_TAC Flyspeck_constants.bounds THEN ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
955 REPEAT WEAKER_STRIP_TAC;
956 MATCH_MP_TAC Merge_ineq.UPS_X_POS;
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]);
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";
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);
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);
992 TYPIFY_GOAL_THEN `!x. &0 <= x - &8 <=> sqrt8 * sqrt8 <= x` (unlist REWRITE_TAC);
993 REWRITE_TAC[Nonlinear_lemma.sqrt8_2];
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];
1002 MATCH_MP_TAC (arith `&0 < x /\ &0 <= y ==> &0 < x + y`);
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);
1014 let WLOG_5691615370 = prove_by_refinement(
1015 `(!y1 y2 y3 y4 y5 y6. ineq
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
1035 ((delta_y y1 y2 y3 y4 y5 y6 < &0) \/ (y2 + y3 + y5 + y6 > #8.472)))`,
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)`];
1040 MATCH_MP_TAC Terminal.REAL_WLOG_SQUARE2_LEMMA;
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];
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)`])
1056 (* Use 5584033259 and 6170936724 and 5691615370 to prove the lemma. *)
1058 let LEMMA_5691615370 = prove_by_refinement(
1060 (!y1 y2 y3 y4 y5 y6. ineq [
1068 ( y1 < &4 \/ delta_y y1 y2 y3 y4 y5 y6 < &0 )) /\
1070 (!y1 y2 y3 y4 y5 y6. ineq [
1078 ( y_of_x delta_x1 y1 y2 y3 y4 y5 y6 < &0)) /\
1080 (!y1 y2 y3 y4 y5 y6. ineq
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))) ==>
1092 (!y1 y2 y3 y4 y5 y6. ineq
1101 ((delta_y y1 y2 y3 y4 y5 y6 < &0) \/ (y2 + y3 + y5 + y6 > #8.472)))
1105 REWRITE_TAC[Sphere.y_of_x;Functional_equation.nonf_ups_126];
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[]);
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;
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";
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]);
1142 FIRST_X_ASSUM_ST `ineq` kill;
1144 BY(ASM_TAC THEN REAL_ARITH_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);
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);
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);
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];
1181 MATCH_MP_TAC (arith `&0 < x /\ &0 <= y ==> &0 < x + y`);
1184 REPEAT (GMATCH_SIMP_TAC (arith `&0 <= x /\ &0 <= y ==> &0 <= x + y`));
1185 REPEAT (GMATCH_SIMP_TAC REAL_LE_MUL);
1188 REWRITE_TAC[DE_MORGAN_THM;NOT_EXISTS_THM];
1191 FIRST_X_ASSUM (C INTRO_TAC [`y1'`;`y1`]);
1193 BY(ASM_TAC THEN REAL_ARITH_TAC);
1195 X_GEN_TAC `y6':real`;
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]);
1213 FIRST_X_ASSUM_ST `ineq` kill;
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];
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)