(* ========================================================================== *) (* FLYSPECK - BOOK FORMALIZATION *) (* Section: Conclusions *) (* Chapter: Tame (Linear Programs) *) (* Author: Thomas C. Hales *) (* Date: 2013-06-19 *) (* ========================================================================== *) (* Treatment of two special inequalities for the linear programs. The main results are LEMMA_8673686234 (uses inequalities "6170936724","8673686234 a","8673686234 b","8673686234 c") see head.mod:yapex_sup_flat 'ID[8673686234]' LEMMA_5691615370 (uses inequalities "5584033259","6170936724","5691615370") see head.mod:perimZ 'ID[5691615370]' *) module Lp_details = struct open Hales_tactic;; (* start 867 *) let quadratic_root_plus_disc = prove_by_refinement( `!a b c x. &0 < a /\ a * x pow 2 + b * x + c <= &0 ==> &0 <= b pow 2 - &4 * a * c`, (* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM MP_TAC; 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); Calc_derivative.CALC_ID_TAC; BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC); ONCE_REWRITE_TAC[arith `u - v <= &0 <=> u <= v`]; GMATCH_SIMP_TAC REAL_LE_RDIV_EQ; CONJ_TAC; BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC); TYPIFY `&0 <= (a * (x + b / (&2 * a)) pow 2) * &4 * a` ENOUGH_TO_SHOW_TAC; BY(REAL_ARITH_TAC); GMATCH_SIMP_TAC REAL_LE_MUL; CONJ_TAC; GMATCH_SIMP_TAC REAL_LE_MUL; ASM_REWRITE_TAC[REAL_LE_POW_2]; BY(ASM_TAC THEN REAL_ARITH_TAC); BY(ASM_TAC THEN REAL_ARITH_TAC) ]);; (* }}} *) let quadratic_root_exists = prove_by_refinement( `!a b c x. &0 < a /\ a * x pow 2 + b * x + c <= &0 ==> (?y. x <= y /\ a * y pow 2 + b *y + c = &0)`, (* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; TYPED_ABBREV_TAC `(h:real) = quadratic_root_plus (a, b + &2 * a *x, a * x pow 2 + b * x + c)`; TYPIFY `x + h` EXISTS_TAC; 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)`]; 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); ONCE_REWRITE_TAC[arith `v <= v - &4 * a * x <=> &0 <= a * (-- x)`]; GMATCH_SIMP_TAC REAL_LE_MUL; BY(ASM_TAC THEN REAL_ARITH_TAC); CONJ2_TAC; EXPAND_TAC "h"; MATCH_MP_TAC (REWRITE_RULE[LET_DEF;LET_END_DEF] Tame_lemmas.quadratic_root_plus_works); CONJ_TAC; BY(ASM_TAC THEN REAL_ARITH_TAC); FIRST_X_ASSUM MP_TAC; BY(MESON_TAC[REAL_LE_TRANS;REAL_LE_POW_2]); MATCH_MP_TAC (arith `&0 <= h ==> x <= x + h`); EXPAND_TAC "h"; REWRITE_TAC[Sphere.quadratic_root_plus]; GMATCH_SIMP_TAC REAL_LE_RDIV_EQ; CONJ_TAC; BY(ASM_TAC THEN REAL_ARITH_TAC); 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))`; BY(REAL_ARITH_TAC); GMATCH_SIMP_TAC SQRT_MONO_LE_EQ; REWRITE_TAC[POW_2_SQRT_ABS]; ASM_REWRITE_TAC[]; CONJ2_TAC; BY(REAL_ARITH_TAC); SUBCONJ_TAC; BY(REWRITE_TAC[REAL_LE_POW_2]); BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC) ]);; (* }}} *) let quadratic_root_pos_exists = prove_by_refinement( `!a b c x. a < &0 /\ &0 <= a * x pow 2 + b * x + c ==> (?y. x <= y /\ a * y pow 2 + b *y + c = &0)`, (* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; INTRO_TAC quadratic_root_exists [`--a`;`--b`;`--c`;`x`]; ANTS_TAC; BY(ASM_TAC THEN REAL_ARITH_TAC); REPEAT WEAKER_STRIP_TAC; TYPIFY `y` EXISTS_TAC; BY(ASM_TAC THEN REAL_ARITH_TAC) ]);; (* }}} *) let delta_x_root_exists = prove_by_refinement( `!x1 x2 x3 x4 x5 x6. &0 <= delta_x x1 x2 x3 x4 x5 x6 /\ &0 < x1 ==> (?x4'. x4 <= x4' /\ delta_x x1 x2 x3 x4' x5 x6 = &0)`, (* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; TYPED_ABBREV_TAC `b = ( delta_x4 x1 x2 x3 (&0) x5 x6)` ; TYPED_ABBREV_TAC `c = delta_x x1 x2 x3 (&0) x5 x6` ; TYPIFY `!z. delta_x x1 x2 x3 z x5 x6 = (-- x1) * z pow 2 + b * z + c` (C SUBGOAL_THEN ASSUME_TAC); EXPAND_TAC "c"; EXPAND_TAC "b"; REWRITE_TAC[Sphere.delta_x;Sphere.delta_x4]; BY(REAL_ARITH_TAC); ASM_REWRITE_TAC[]; MATCH_MP_TAC quadratic_root_pos_exists; FIRST_X_ASSUM ((unlist REWRITE_TAC) o GSYM); ASM_REWRITE_TAC[]; BY(ASM_TAC THEN REAL_ARITH_TAC) ]);; (* }}} *) let delta_y_root_exists = prove_by_refinement( `!y1 y2 y3 y4 y5 y6. &0 <= delta_y y1 y2 y3 y4 y5 y6 /\ &0 < y1 /\ &0 < y4 ==> (?y4'. y4 <= y4' /\ delta_y y1 y2 y3 y4' y5 y6 = &0)`, (* {{{ proof *) [ REWRITE_TAC[Sphere.delta_y]; REPEAT WEAKER_STRIP_TAC; INTRO_TAC delta_x_root_exists [`y1*y1`;`y2*y2`;`y3*y3`;`y4*y4`;`y5*y5`;`y6*y6`]; ANTS_TAC; ASM_REWRITE_TAC[]; GMATCH_SIMP_TAC REAL_LT_MUL_EQ; BY(ASM_REWRITE_TAC[]); REPEAT WEAKER_STRIP_TAC; TYPIFY `sqrt(x4')` EXISTS_TAC; TYPIFY `&0 <= x4'` (C SUBGOAL_THEN ASSUME_TAC); FIRST_X_ASSUM_ST `<=` MP_TAC; BY(MESON_TAC[REAL_LE_POW_2;REAL_LE_TRANS;arith `x*x = x pow 2`]); TYPIFY `sqrt(x4') * sqrt(x4') = x4'` (C SUBGOAL_THEN ASSUME_TAC); GMATCH_SIMP_TAC (GSYM SQRT_MUL); GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx; BY(ASM_REWRITE_TAC[]); ASM_REWRITE_TAC[]; PROOF_BY_CONTR_TAC; FIRST_X_ASSUM_ST `y4 * y4 <= x4'` MP_TAC; FIRST_ASSUM_ST `(=)` (SUBST1_TAC o GSYM); REWRITE_TAC[arith `~(x <= y) <=> y < x`]; MATCH_MP_TAC Misc_defs_and_lemmas.ABS_SQUARE; TYPIFY `&0 <= sqrt x4'` (C SUBGOAL_THEN ASSUME_TAC); GMATCH_SIMP_TAC SQRT_POS_LE; BY(ASM_REWRITE_TAC[]); BY(ASM_TAC THEN REAL_ARITH_TAC) ]);; (* }}} *) let edge2_flatD_x1_quadratic_root_plus = prove_by_refinement( `!d x2 x3 x4 x5 x6. edge2_flatD_x1 d x2 x3 x4 x5 x6 = quadratic_root_plus(x4, -- delta_x1 (&0) x2 x3 x4 x5 x6, d - delta_x (&0) x2 x3 x4 x5 x6 )`, (* {{{ proof *) [ REWRITE_TAC[Nonlin_def.edge2_flatD_x1]; REPEAT WEAKER_STRIP_TAC; TYPED_ABBREV_TAC `b = (-- delta_x1 (&0) x2 x3 x4 x5 x6)`; TYPED_ABBREV_TAC `c = (d - delta_x (&0) x2 x3 x4 x5 x6)`; TYPIFY `!z. d - delta_x z x2 x3 x4 x5 x6 = x4 * z pow 2 + b * z + c` ((C SUBGOAL_THEN ASSUME_TAC)); EXPAND_TAC "c"; EXPAND_TAC "b"; REWRITE_TAC[Sphere.delta_x;Nonlin_def.delta_x1]; BY(REAL_ARITH_TAC); ASM_REWRITE_TAC[Nonlinear_lemma.abc_quadratic]; ]);; (* }}} *) let edge2_flatD_x1_expanded = prove_by_refinement( `!d x2 x3 x4 x5 x6. edge2_flatD_x1 d x2 x3 x4 x5 x6 = (delta_x1 (&0) x2 x3 x4 x5 x6 + sqrt (ups_x x2 x3 x4 * ups_x x4 x5 x6 - &4 * x4 * d)) / (&2 * x4) `, (* {{{ proof *) [ REWRITE_TAC[edge2_flatD_x1_quadratic_root_plus]; REPEAT WEAKER_STRIP_TAC; TYPED_ABBREV_TAC `b = (-- delta_x1 (&0) x2 x3 x4 x5 x6)`; TYPED_ABBREV_TAC `c = (d - delta_x (&0) x2 x3 x4 x5 x6)`; REWRITE_TAC[Sphere.quadratic_root_plus]; 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); EXPAND_TAC "b"; EXPAND_TAC "c"; REWRITE_TAC[Sphere.delta_x;Nonlin_def.delta_x1;Sphere.ups_x]; BY(REAL_ARITH_TAC); ASM_REWRITE_TAC[]; EXPAND_TAC "b"; BY(REAL_ARITH_TAC) ]);; (* }}} *) let derived_form_edge2_flatD_x1 = prove_by_refinement( `!x2 x3 x4 x5 x6. (&0 < ups_x x2 x3 x4 /\ &0 < ups_x x4 x5 x6 /\ &0 < x4) ==> (?f'. derived_form T (\q. edge2_flatD_x1 (&0) q x3 x4 x5 x6) f' x2 (:real))`, (* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; REWRITE_TAC[edge2_flatD_x1_expanded]; REWRITE_TAC[Nonlin_def.delta_x1;Sphere.ups_x;arith `x - &4 * x4 * &0 = x`]; 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; Pent_hex.DERIVED_TAC MP_TAC; REWRITE_TAC[GSYM Sphere.ups_x]; TYPIFY_GOAL_THEN `(&0 < ups_x x2 x3 x4 * ups_x x4 x5 x6 /\ ~(&2 = &0) /\ ~(x4 = &0))` (unlist REWRITE_TAC); REWRITE_TAC[REAL_OF_NUM_EQ]; GMATCH_SIMP_TAC REAL_LT_MUL_EQ; ASM_REWRITE_TAC[]; CONJ_TAC; BY(ARITH_TAC); BY(ASM_TAC THEN REAL_ARITH_TAC) ]);; (* }}} *) let edge2_flatD_x1_continuous = prove_by_refinement( `!x2 x3 x4 x5 x6. (&0 < ups_x x2 x3 x4 /\ &0 < ups_x x4 x5 x6 /\ &0 < x4 ==> (\q. edge2_flatD_x1 (&0) q x3 x4 x5 x6) real_continuous atreal x2)`, (* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; MATCH_MP_TAC HAS_REAL_DERIVATIVE_IMP_CONTINUOUS_ATREAL; INTRO_TAC derived_form_edge2_flatD_x1 [`x2`;`x3`;`x4`;`x5`;`x6`]; BY(ASM_REWRITE_TAC[Calc_derivative.derived_form;WITHINREAL_UNIV]) ]);; (* }}} *) let IVT_edge2_flatD_x1 = prove_by_refinement( `!x1m x1M x2m x2M x3 x4 x5 x6. (!x2. x2m <= x2 /\ x2 <= x2M ==> &0 < ups_x x2 x3 x4) /\ (&0 < ups_x x4 x5 x6) /\ (&0 < x4) /\ (x1m <= x1M) /\ (x2m <= x2M) /\ (delta_x x1M x2M x3 x4 x5 x6 = &0) /\ (!x1 x2. x1m <= x1 /\ x1 <= x1M /\ x2m <= x2 /\ x2 <= x2M ==> delta_x1 x1 x2 x3 x4 x5 x6 < &0) ==> ((?x2. x2m <= x2 /\ x2 <= x2M /\ edge2_flatD_x1 (&0) x2 x3 x4 x5 x6 = x1m) \/ (x1m < edge2_flatD_x1 (&0) x2m x3 x4 x5 x6))`, (* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; TYPIFY `!x2. x2m <= x2 /\ x2 <= x2M ==> x1m < edge2_flatD_x1 (&0) x2 x3 x4 x5 x6` ASM_CASES_TAC; FIRST_X_ASSUM (C INTRO_TAC [`x2m`]); ASM_REWRITE_TAC[arith `x <= x`]; BY(MESON_TAC[]); FIRST_X_ASSUM MP_TAC; REWRITE_TAC[NOT_FORALL_THM]; REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM MP_TAC; REWRITE_TAC[TAUT `~(a ==> b) <=> (a /\ ~b)`]; REWRITE_TAC[arith `~(x < b) <=> b <= x`]; REPEAT WEAKER_STRIP_TAC; DISJ1_TAC; INTRO_TAC REAL_IVT_INCREASING [`(\q. edge2_flatD_x1 (&0) q x3 x4 x5 x6)`;`x2`;`x2M`;`x1m`]; ANTS_TAC; ASM_REWRITE_TAC[]; CONJ2_TAC; ENOUGH_TO_SHOW_TAC `edge2_flatD_x1 (&0) x2M x3 x4 x5 x6 = x1M`; BY(ASM_TAC THEN REAL_ARITH_TAC); MATCH_MP_TAC Pent_hex.edge2_flatD_x1_delta_lemma2; ASM_REWRITE_TAC[]; FIRST_X_ASSUM MATCH_MP_TAC; BY(ASM_TAC THEN REAL_ARITH_TAC); REWRITE_TAC[REAL_CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN]; REWRITE_TAC[IN_REAL_INTERVAL]; REPEAT WEAKER_STRIP_TAC; MATCH_MP_TAC REAL_CONTINUOUS_ATREAL_WITHINREAL; MATCH_MP_TAC edge2_flatD_x1_continuous; ASM_REWRITE_TAC[]; FIRST_X_ASSUM MATCH_MP_TAC; ASM_REWRITE_TAC[]; BY(ASM_TAC THEN REAL_ARITH_TAC); REWRITE_TAC[IN_REAL_INTERVAL]; REPEAT WEAKER_STRIP_TAC; TYPIFY `x` EXISTS_TAC; ASM_REWRITE_TAC[]; BY(ASM_TAC THEN REAL_ARITH_TAC) ]);; (* }}} *) let edge2_flatD_x1_works = prove_by_refinement( `!x2 x3 x4 x5 x6. &0 <= ups_x x2 x3 x4 /\ &0 <= ups_x x4 x5 x6 /\ ~(x4 = &0) ==> delta_x (edge2_flatD_x1 (&0) x2 x3 x4 x5 x6) x2 x3 x4 x5 x6 = &0`, (* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; REWRITE_TAC[edge2_flatD_x1_quadratic_root_plus]; TYPED_ABBREV_TAC `b = (-- delta_x1 (&0) x2 x3 x4 x5 x6)`; TYPED_ABBREV_TAC `c = (&0 - delta_x (&0) x2 x3 x4 x5 x6)`; ONCE_REWRITE_TAC[arith `d = &0 <=> &0 - d = &0`]; TYPIFY `!z. &0 - delta_x z x2 x3 x4 x5 x6 = x4 * z pow 2 + b * z + c` ((C SUBGOAL_THEN ASSUME_TAC)); EXPAND_TAC "c"; EXPAND_TAC "b"; REWRITE_TAC[Sphere.delta_x;Nonlin_def.delta_x1]; BY(REAL_ARITH_TAC); ASM_REWRITE_TAC[]; MATCH_MP_TAC (REWRITE_RULE[LET_DEF;LET_END_DEF] Tame_lemmas.quadratic_root_plus_works); TYPIFY `b pow 2 - &4 * x4 * c = ups_x x2 x3 x4 * ups_x x4 x5 x6 ` (C SUBGOAL_THEN ASSUME_TAC); EXPAND_TAC "b"; EXPAND_TAC "c"; REWRITE_TAC[Sphere.delta_x;Nonlin_def.delta_x1;Sphere.ups_x]; BY(REAL_ARITH_TAC); ASM_REWRITE_TAC[]; GMATCH_SIMP_TAC REAL_LE_MUL; BY(ASM_REWRITE_TAC[]) ]);; (* }}} *) let delta_x1_decreasing = prove_by_refinement( `!x1 x2 x3 x4 x5 x6 x1'. x1 <= x1' /\ &0 <= x4 ==> delta_x1 x1' x2 x3 x4 x5 x6 <= delta_x1 x1 x2 x3 x4 x5 x6`, (* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; ENOUGH_TO_SHOW_TAC `delta_x1 x1 x2 x3 x4 x5 x6 - delta_x1 x1' x2 x3 x4 x5 x6 = &2 * x4 * (x1' - x1)`; ONCE_REWRITE_TAC[arith `d' <= d <=> &0 <= d - d'`]; DISCH_THEN SUBST1_TAC; GMATCH_SIMP_TAC REAL_LE_MUL; CONJ_TAC; BY(REAL_ARITH_TAC); GMATCH_SIMP_TAC REAL_LE_MUL; BY(ASM_TAC THEN REAL_ARITH_TAC); REWRITE_TAC[Nonlin_def.delta_x1]; BY(REAL_ARITH_TAC) ]);; (* }}} *) let IVT_delta_x = prove_by_refinement( `!x1m x1M x2m x2M x3 x4 x5 x6. (!x2. x2m <= x2 /\ x2 <= x2M ==> &0 < ups_x x2 x3 x4) /\ &0 < ups_x x4 x5 x6 /\ &0 < x4 /\ x1m <= x1M /\ x2m <= x2M /\ delta_x x1M x2M x3 x4 x5 x6 = &0 /\ (!x2. x2m <= x2 /\ x2 <= x2M ==> delta_x1 x1m x2 x3 x4 x5 x6 < &0) ==> (?x2. x2m <= x2 /\ x2 <= x2M /\ delta_x x1m x2 x3 x4 x5 x6 = &0) \/ (?x1. x1m < x1 /\ delta_x x1 x2m x3 x4 x5 x6 = &0)`, (* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; INTRO_TAC IVT_edge2_flatD_x1 [`x1m`;`x1M`;`x2m`;`x2M`;`x3`;`x4`;`x5`;`x6`]; ANTS_TAC; (ASM_REWRITE_TAC[]); REPEAT WEAKER_STRIP_TAC; ENOUGH_TO_SHOW_TAC `delta_x1 x1 x2 x3 x4 x5 x6 <= delta_x1 x1m x2 x3 x4 x5 x6`; MATCH_MP_TAC (arith `x < &0 ==> (y <= x ==> y< &0)`); FIRST_X_ASSUM MATCH_MP_TAC; BY(ASM_REWRITE_TAC[]); MATCH_MP_TAC delta_x1_decreasing; BY(ASM_SIMP_TAC[arith `&0 < x ==> &0 <= x`]); STRIP_TAC; DISJ1_TAC; TYPIFY `x2` EXISTS_TAC; ASM_REWRITE_TAC[]; EXPAND_TAC "x1m"; MATCH_MP_TAC edge2_flatD_x1_works; BY(ASM_SIMP_TAC[arith `x < y ==> x <= y`;arith `&0 < x ==> ~(x = &0)`]); DISJ2_TAC; TYPIFY `edge2_flatD_x1 (&0) x2m x3 x4 x5 x6` EXISTS_TAC; ASM_REWRITE_TAC[]; MATCH_MP_TAC edge2_flatD_x1_works; ASM_SIMP_TAC[arith `x < y ==> x <= y`;arith `&0 < x ==> ~(x = &0)`]; MATCH_MP_TAC (arith `x < y ==> x <= y`); FIRST_X_ASSUM MATCH_MP_TAC; BY(ASM_TAC THEN REAL_ARITH_TAC) ]);; (* }}} *) let delta_x1_sym = prove_by_refinement( `!x1 x2 x3 x4 x5 x6. delta_x1 x1 x3 x2 x4 x6 x5 = delta_x1 x1 x2 x3 x4 x5 x6 /\ delta_x1 x1 x5 x6 x4 x2 x3 = delta_x1 x1 x2 x3 x4 x5 x6`, (* {{{ proof *) [ REWRITE_TAC[Nonlin_def.delta_x1]; BY(REAL_ARITH_TAC) ]);; (* }}} *) let IVT_delta_x_3 = prove_by_refinement( `!x1m x1M x2 x3m x3M x4 x5 x6. (!x3. x3m <= x3 /\ x3 <= x3M ==> &0 < ups_x x2 x3 x4) /\ &0 < ups_x x4 x5 x6 /\ &0 < x4 /\ x1m <= x1M /\ x3m <= x3M /\ delta_x x1M x2 x3M x4 x5 x6 = &0 /\ (!x3. x3m <= x3 /\ x3 <= x3M ==> delta_x1 x1m x2 x3 x4 x5 x6 < &0) ==> (?x3. x3m <= x3 /\ x3 <= x3M /\ delta_x x1m x2 x3 x4 x5 x6 = &0) \/ (?x1. x1m < x1 /\ delta_x x1 x2 x3m x4 x5 x6 = &0)`, (* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; INTRO_TAC IVT_delta_x [`x1m`;`x1M`;`x3m`;`x3M`;`x2`;`x4`;`x6`;`x5`]; ASM_REWRITE_TAC[]; ANTS_TAC; CONJ_TAC; REPEAT WEAKER_STRIP_TAC; ONCE_REWRITE_TAC[Merge_ineq.ups_x_sym]; FIRST_X_ASSUM MATCH_MP_TAC; BY(ASM_REWRITE_TAC[]); CONJ_TAC; FIRST_X_ASSUM_ST `ups_x` MP_TAC; BY(MESON_TAC[Collect_geom.UPS_X_SYM]); CONJ_TAC; BY(ASM_MESON_TAC[Merge_ineq.delta_x_sym]); BY(ASM_MESON_TAC[delta_x1_sym]); BY(MESON_TAC[Merge_ineq.delta_x_sym]) ]);; (* }}} *) let IVT_delta_x_5 = prove_by_refinement( `!x1m x1M x2 x3 x4 x5m x5M x6. (!x5. x5m <= x5 /\ x5 <= x5M ==> &0 < ups_x x4 x5 x6) /\ &0 < ups_x x2 x3 x4 /\ &0 < x4 /\ x1m <= x1M /\ x5m <= x5M /\ delta_x x1M x2 x3 x4 x5M x6 = &0 /\ (!x5. x5m <= x5 /\ x5 <= x5M ==> delta_x1 x1m x2 x3 x4 x5 x6 < &0) ==> (?x5. x5m <= x5 /\ x5 <= x5M /\ delta_x x1m x2 x3 x4 x5 x6 = &0) \/ (?x1. x1m < x1 /\ delta_x x1 x2 x3 x4 x5m x6 = &0)`, (* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; INTRO_TAC IVT_delta_x [`x1m`;`x1M`;`x5m`;`x5M`;`x6`;`x4`;`x2`;`x3`]; ASM_REWRITE_TAC[]; ANTS_TAC; CONJ_TAC; REPEAT WEAKER_STRIP_TAC; BY(ASM_MESON_TAC[Collect_geom.UPS_X_SYM]); CONJ_TAC; BY(ASM_MESON_TAC[Collect_geom.UPS_X_SYM]); CONJ_TAC; BY(ASM_MESON_TAC[Merge_ineq.delta_x_sym]); BY(ASM_MESON_TAC[delta_x1_sym]); BY(MESON_TAC[Merge_ineq.delta_x_sym]) ]);; (* }}} *) let IVT_delta_x_6 = prove_by_refinement( `!x1m x1M x2 x3 x4 x5 x6m x6M. (!x6. x6m <= x6 /\ x6 <= x6M ==> &0 < ups_x x4 x5 x6) /\ &0 < ups_x x2 x3 x4 /\ &0 < x4 /\ x1m <= x1M /\ x6m <= x6M /\ delta_x x1M x2 x3 x4 x5 x6M = &0 /\ (!x6. x6m <= x6 /\ x6 <= x6M ==> delta_x1 x1m x2 x3 x4 x5 x6 < &0) ==> (?x6. x6m <= x6 /\ x6 <= x6M /\ delta_x x1m x2 x3 x4 x5 x6 = &0) \/ (?x1. x1m < x1 /\ delta_x x1 x2 x3 x4 x5 x6m = &0)`, (* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; INTRO_TAC IVT_delta_x [`x1m`;`x1M`;`x6m`;`x6M`;`x5`;`x4`;`x3`;`x2`]; ASM_REWRITE_TAC[]; ANTS_TAC; CONJ_TAC; REPEAT WEAKER_STRIP_TAC; BY(ASM_MESON_TAC[Collect_geom.UPS_X_SYM]); CONJ_TAC; BY(ASM_MESON_TAC[Collect_geom.UPS_X_SYM]); CONJ_TAC; BY(ASM_MESON_TAC[Merge_ineq.delta_x_sym]); BY(ASM_MESON_TAC[delta_x1_sym]); BY(MESON_TAC[Merge_ineq.delta_x_sym]) ]);; (* }}} *) let IVT_delta_x_full = prove_by_refinement( `!x1m x1M x2m x2M x3m x3M x4 x5m x5M x6m x6M. &0 < x4 /\ (!x2 x3. x2m <= x2 /\ x2 <= x2M /\ x3m <= x3 /\ x3 <= x3M ==> &0 < ups_x x2 x3 x4) /\ (!x5 x6. x5m <= x5 /\ x5 <= x5M /\ x6m <= x6 /\ x6 <= x6M ==> &0 < ups_x x4 x5 x6) /\ x1m <= x1M /\ x2m <= x2M /\ x3m <= x3M /\ x5m <= x5M /\ x6m <= x6M /\ delta_x x1M x2M x3M x4 x5M x6M = &0 /\ (! x2 x3 x5 x6. x2m <= x2 /\ x2 <= x2M /\ x3m <= x3 /\ x3 <= x3M /\ x5m <= x5 /\ x5 <= x5M /\ x6m <= x6 /\ x6 <= x6M ==> delta_x1 x1m x2 x3 x4 x5 x6 < &0) ==> (?x2 x3 x5 x6. x2m <= x2 /\ x2 <= x2M /\ x3m <= x3 /\ x3 <= x3M /\ x5m <= x5 /\ x5 <= x5M /\ x6m <= x6 /\ x6 <= x6M /\ delta_x x1m x2 x3 x4 x5 x6 = &0) \/ (?x1. x1m < x1 /\ delta_x x1 x2m x3m x4 x5m x6m = &0) `, (* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; PROOF_BY_CONTR_TAC; RULE_ASSUM_TAC (REWRITE_RULE[DE_MORGAN_THM;NOT_EXISTS_THM;TAUT `~(a /\ b) <=> a ==> ~b`;TAUT `a ==> b ==> c <=> (a /\ b) ==> c`]); FIRST_X_ASSUM MP_TAC; REPEAT WEAKER_STRIP_TAC; INTRO_TAC IVT_delta_x [`x1m`;`x1M`;`x2m`;`x2M`;`x3M`;`x4`;`x5M`;`x6M`]; ANTS_TAC; ASM_REWRITE_TAC[]; CONJ_TAC; REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM MATCH_MP_TAC; BY(ASM_REWRITE_TAC[arith `x <= x`]); CONJ_TAC; FIRST_X_ASSUM MATCH_MP_TAC; BY(ASM_REWRITE_TAC[arith `x <= x`]); REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM MATCH_MP_TAC; BY(ASM_REWRITE_TAC[arith `x <= x`]); STRIP_TAC; FIRST_X_ASSUM MP_TAC; REWRITE_TAC[]; FIRST_X_ASSUM MATCH_MP_TAC; BY(ASM_REWRITE_TAC[arith `x <= x`]); INTRO_TAC IVT_delta_x_3 [`x1m`;`x1`;`x2m`;`x3m`;`x3M`;`x4`;`x5M`;`x6M`]; ASM_REWRITE_TAC[]; DISCH_THEN MP_TAC THEN ANTS_TAC; CONJ_TAC; REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM MATCH_MP_TAC; BY(ASM_REWRITE_TAC[arith `x <= x`]); CONJ_TAC; FIRST_X_ASSUM MATCH_MP_TAC; BY(ASM_REWRITE_TAC[arith `x <= x`]); CONJ_TAC; BY(FIRST_X_ASSUM_ST `<` MP_TAC THEN REAL_ARITH_TAC); REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM MATCH_MP_TAC; BY(ASM_REWRITE_TAC[arith `x <= x`]); STRIP_TAC; FIRST_X_ASSUM MP_TAC; REWRITE_TAC[]; FIRST_X_ASSUM MATCH_MP_TAC; BY(ASM_REWRITE_TAC[arith `x <= x`]); INTRO_TAC IVT_delta_x_5 [`x1m`;`x1'`;`x2m`;`x3m`;`x4`;`x5m`;`x5M`;`x6M`]; ASM_REWRITE_TAC[]; DISCH_THEN MP_TAC THEN ANTS_TAC; CONJ_TAC; REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM MATCH_MP_TAC; BY(ASM_REWRITE_TAC[arith `x <= x`]); CONJ_TAC; FIRST_X_ASSUM MATCH_MP_TAC; BY(ASM_REWRITE_TAC[arith `x <= x`]); CONJ_TAC; BY(REPLICATE_TAC 2 (FIRST_X_ASSUM_ST `<` MP_TAC) THEN REAL_ARITH_TAC); REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM MATCH_MP_TAC; BY(ASM_REWRITE_TAC[arith `x <= x`]); STRIP_TAC; FIRST_X_ASSUM MP_TAC; REWRITE_TAC[]; FIRST_X_ASSUM MATCH_MP_TAC; BY(ASM_REWRITE_TAC[arith `x <= x`]); INTRO_TAC IVT_delta_x_6 [`x1m`;`x1''`;`x2m`;`x3m`;`x4`;`x5m`;`x6m`;`x6M`]; ASM_REWRITE_TAC[]; DISCH_THEN MP_TAC THEN ANTS_TAC; CONJ_TAC; REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM MATCH_MP_TAC; BY(ASM_REWRITE_TAC[arith `x <= x`]); CONJ_TAC; FIRST_X_ASSUM MATCH_MP_TAC; BY(ASM_REWRITE_TAC[arith `x <= x`]); CONJ_TAC; BY(REPLICATE_TAC 3 (FIRST_X_ASSUM_ST `<` MP_TAC) THEN REAL_ARITH_TAC); REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM MATCH_MP_TAC; BY(ASM_REWRITE_TAC[arith `x <= x`]); STRIP_TAC; FIRST_X_ASSUM MP_TAC; REWRITE_TAC[]; FIRST_X_ASSUM MATCH_MP_TAC; BY(ASM_REWRITE_TAC[arith `x <= x`]); FIRST_X_ASSUM MP_TAC; REWRITE_TAC[]; FIRST_X_ASSUM MATCH_MP_TAC; BY(REPLICATE_TAC 4 (FIRST_X_ASSUM_ST `<` MP_TAC) THEN REAL_ARITH_TAC) ]);; (* }}} *) let FORALL_BIJ_SQUARE = prove_by_refinement( `!P ym yM. &0 <= ym /\ &0 <= yM ==> ((!x. ym*ym <= x /\ x <= yM*yM ==> P x) <=> (!y. ym <= y /\ y <= yM ==> P (y*y)))`, (* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; MATCH_MP_TAC (TAUT `(a ==> b) /\ (b ==> a) ==> (a <=> b)`); CONJ_TAC; REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM MATCH_MP_TAC; GMATCH_SIMP_TAC Misc_defs_and_lemmas.ABS_SQUARE_LE; GMATCH_SIMP_TAC Misc_defs_and_lemmas.ABS_SQUARE_LE; BY(ASM_TAC THEN REAL_ARITH_TAC); REPEAT WEAKER_STRIP_TAC; TYPIFY `&0 <= x` (C SUBGOAL_THEN ASSUME_TAC); FIRST_X_ASSUM_ST `y*y <= x` MP_TAC; BY(MESON_TAC[REAL_LE_POW_2;arith `x*x = x pow 2`;REAL_LE_TRANS]); REPLICATE_TAC 2 (FIRST_X_ASSUM_ST `*` MP_TAC); TYPIFY_GOAL_THEN `x = sqrt x * sqrt x` (unlist ONCE_REWRITE_TAC); GMATCH_SIMP_TAC (GSYM SQRT_MUL); GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx; BY(ASM_REWRITE_TAC[]); ASM_REWRITE_TAC[arith `x * x = x pow 2`]; GMATCH_SIMP_TAC (GSYM Trigonometry2.POW2_COND); GMATCH_SIMP_TAC (GSYM Trigonometry2.POW2_COND); ASM_REWRITE_TAC[]; GMATCH_SIMP_TAC SQRT_POS_LE; ASM_REWRITE_TAC[]; REWRITE_TAC[arith `x pow 2 = x*x`]; REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM MATCH_MP_TAC; BY(ASM_REWRITE_TAC[]) ]);; (* }}} *) let EXISTS_BIJ_SQUARE = prove_by_refinement( `!P ym yM. &0 <= ym /\ &0 <= yM ==> ((?x. ym*ym <= x /\ x <= yM*yM /\ P x) <=> (?y. ym <= y /\ y <= yM /\ P (y*y)))`, (* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; ONCE_REWRITE_TAC[TAUT `(a <=> b) <=> (~a <=> ~b)`]; REWRITE_TAC[NOT_EXISTS_THM;DE_MORGAN_THM]; REWRITE_TAC[TAUT `~a \/ ~b \/ ~c <=> (a /\ b ==> ~c)`]; MATCH_MP_TAC FORALL_BIJ_SQUARE; BY(ASM_REWRITE_TAC[]) ]);; (* }}} *) let IVT_delta_y_full = prove_by_refinement( `!y1m y1M y2m y2M y3m y3M y4 y5m y5M y6m y6M. &0 < y4 /\ &0 <= y1m /\ &0 <= y2m /\ &0 <= y3m /\ &0 <= y5m /\ &0 <= y6m /\ (!y2 y3. y2m <= y2 /\ y2 <= y2M /\ y3m <= y3 /\ y3 <= y3M ==> &0 < ups_x (y2*y2) (y3*y3) (y4*y4)) /\ (!y5 y6. y5m <= y5 /\ y5 <= y5M /\ y6m <= y6 /\ y6 <= y6M ==> &0 < ups_x (y4*y4) (y5*y5) (y6*y6)) /\ y1m <= y1M /\ y2m <= y2M /\ y3m <= y3M /\ y5m <= y5M /\ y6m <= y6M /\ delta_y y1M y2M y3M y4 y5M y6M = &0 /\ (! y2 y3 y5 y6. y2m <= y2 /\ y2 <= y2M /\ y3m <= y3 /\ y3 <= y3M /\ y5m <= y5 /\ y5 <= y5M /\ y6m <= y6 /\ y6 <= y6M ==> y_of_x delta_x1 y1m y2 y3 y4 y5 y6 < &0) ==> (?y2 y3 y5 y6. y2m <= y2 /\ y2 <= y2M /\ y3m <= y3 /\ y3 <= y3M /\ y5m <= y5 /\ y5 <= y5M /\ y6m <= y6 /\ y6 <= y6M /\ delta_y y1m y2 y3 y4 y5 y6 = &0) \/ (?y1. y1m < y1 /\ delta_y y1 y2m y3m y4 y5m y6m = &0) `, (* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; TYPIFY `&0 <= y2M /\ &0 <= y3M /\ &0 <= y5M /\ &0 <= y6M` (C SUBGOAL_THEN ASSUME_TAC); REPEAT (FIRST_X_ASSUM_ST `!` kill); BY(ASM_TAC THEN REAL_ARITH_TAC); 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`]; ANTS_TAC; ASM_REWRITE_TAC[GSYM Sphere.delta_y]; CONJ_TAC; GMATCH_SIMP_TAC REAL_LT_MUL_EQ; BY(ASM_REWRITE_TAC[]); CONJ_TAC; 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; BY(MESON_TAC[]); REPEAT (GMATCH_SIMP_TAC FORALL_BIJ_SQUARE THEN ASM_REWRITE_TAC[] THEN REPEAT GEN_TAC THEN DISCH_TAC); FIRST_X_ASSUM MATCH_MP_TAC; BY(ASM_TAC THEN REAL_ARITH_TAC); CONJ_TAC; 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; BY(MESON_TAC[]); REPEAT (GMATCH_SIMP_TAC FORALL_BIJ_SQUARE THEN ASM_REWRITE_TAC[] THEN REPEAT GEN_TAC THEN DISCH_TAC); FIRST_X_ASSUM MATCH_MP_TAC; BY(ASM_TAC THEN REAL_ARITH_TAC); REPEAT (GMATCH_SIMP_TAC Misc_defs_and_lemmas.ABS_SQUARE_LE); ASM_SIMP_TAC[arith `&0 <= y ==> abs y = y`]; 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; BY(MESON_TAC[]); REPEAT (GMATCH_SIMP_TAC FORALL_BIJ_SQUARE THEN ASM_REWRITE_TAC[] THEN REPEAT GEN_TAC THEN DISCH_TAC); REWRITE_TAC[GSYM Sphere.y_of_x]; FIRST_X_ASSUM MATCH_MP_TAC; BY(ASM_TAC THEN REAL_ARITH_TAC); STRIP_TAC; DISJ1_TAC; 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; BY(MESON_TAC[]); REWRITE_TAC[Sphere.delta_y]; GMATCH_SIMP_TAC (GSYM EXISTS_BIJ_SQUARE); ASM_REWRITE_TAC[]; TYPIFY `x2` EXISTS_TAC; ASM_REWRITE_TAC[]; GMATCH_SIMP_TAC (GSYM EXISTS_BIJ_SQUARE); ASM_REWRITE_TAC[]; TYPIFY `x3` EXISTS_TAC; ASM_REWRITE_TAC[]; GMATCH_SIMP_TAC (GSYM EXISTS_BIJ_SQUARE); ASM_REWRITE_TAC[]; TYPIFY `x5` EXISTS_TAC; ASM_REWRITE_TAC[]; GMATCH_SIMP_TAC (GSYM EXISTS_BIJ_SQUARE); ASM_REWRITE_TAC[]; TYPIFY `x6` EXISTS_TAC; BY(ASM_REWRITE_TAC[]); DISJ2_TAC; REWRITE_TAC[Sphere.delta_y]; TYPIFY `sqrt x1` EXISTS_TAC; GMATCH_SIMP_TAC (GSYM SQRT_MUL); GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx; ASM_REWRITE_TAC[]; GMATCH_SIMP_TAC REAL_LT_RSQRT; ASM_REWRITE_TAC[arith `y pow 2 = y*y`]; FIRST_X_ASSUM_ST `<` MP_TAC; BY(MESON_TAC[arith `a < y ==> a <= y`;arith `y*y = y pow 2`;REAL_LE_POW_2;REAL_LE_TRANS]) ]);; (* }}} *) let REAL_WLOG_DS_LEMMA = prove_by_refinement( `!P. (!(y1:A) y2 y3 (y4:A) y5 y6. P y1 y2 y3 y4 y5 y6 = P y1 y3 y2 y4 y6 y5) /\ (!y1 y2 y3 y4 y5 y6. P y1 y2 y3 y4 y5 y6 = P y1 y5 y6 y4 y2 y3) /\ (!y1 y2 y3 y4 y5 y6. (y3 <= y2) /\ (y5 <= y2) /\ (y6 <= y2) ==> P y1 y2 y3 y4 y5 y6) ==> (!y1 y2 y3 y4 y5 y6. P y1 y2 y3 y4 y5 y6)`, (* {{{ proof *) [ REPEAT WEAK_STRIP_TAC; SUBGOAL_THEN `?a. a IN {y2,y3,y5,y6} /\ (!x. x IN {y2,y3,y5,y6} ==> x <= a)` MP_TAC; MATCH_MP_TAC Merge_ineq.REAL_FINITE_MAX_EXISTS; BY(REWRITE_TAC[ FINITE_INSERT ; FINITE_EMPTY;NOT_INSERT_EMPTY]); REPEAT WEAK_STRIP_TAC; REPEAT (FIRST_X_ASSUM_ST `IN` MP_TAC); REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY]; REWRITE_TAC[MESON[] `(!x. x = y2 \/ x = y3 \/ x = y5 \/ x = y6 ==> x <= a) = (y2 <= a /\ y3 <= a /\ y5 <= a /\ y6 <= a)`]; BY(DISCH_THEN STRIP_ASSUME_TAC THEN ASM_MESON_TAC[]) ]);; (* }}} *) (* let REAL_WLOG_DS2_LEMMA = prove_by_refinement( `!P. (!(y1:A) y2 y3 (y4:A) y5 y6. P y1 y2 y3 y4 y5 y6 = P y1 y3 y2 y4 y6 y5) /\ (!y1 y2 y3 y4 y5 y6. P y1 y2 y3 y4 y5 y6 = P y1 y5 y6 y4 y2 y3) /\ (!y1 y2 y3 y4 y5 y6. (y3 <= y2) /\ (y5 <= y2) /\ (y6 <= y2) /\ (y6 <= y3) ==> P y1 y2 y3 y4 y5 y6) ==> (!y1 y2 y3 y4 y5 y6. P y1 y2 y3 y4 y5 y6)`, (* {{{ proof *) [ GEN_TAC; DISCH_TAC; MATCH_MP_TAC REAL_WLOG_DS_LEMMA; ASM_REWRITE_TAC[]; BY(ASM_MESON_TAC[arith `y3 <= y6 \/ y6 <= y3`;arith `y3 <= y3`]) ]);; (* }}} *) *) let WLOG_8673686234 = prove_by_refinement( `(!y1 y2 y3 y4 y5 y6. y3 <= y2 /\ y5 <= y2 /\ y6 <= y2 ==> ineq [ (sqrt8,y1,#3.0); (&2,y2,&2 * h0); (&2,y3,&2 * h0); (sqrt8,y4,&4 * h0); (&2,y5,&2 * h0); (&2,y6,&2 * h0) ] ((y2 + y3 + y5 + y6 - #7.99 > #2.75 * (y1 - sqrt8)) \/ (delta_y y1 y2 y3 y4 y5 y6 < &0) \/ (y4 < y1))) ==> (!y1 y2 y3 y4 y5 y6. ineq [ (sqrt8,y1,#3.0); (&2,y2,&2 * h0); (&2,y3,&2 * h0); (sqrt8,y4,&4 * h0); (&2,y5,&2 * h0); (&2,y6,&2 * h0) ] ((y2 + y3 + y5 + y6 - #7.99 > #2.75 * (y1 - sqrt8)) \/ (delta_y y1 y2 y3 y4 y5 y6 < &0) \/ (y4 < y1)))`, (* {{{ proof *) [ DISCH_TAC; MATCH_MP_TAC REAL_WLOG_DS_LEMMA; ASM_REWRITE_TAC[]; FIRST_X_ASSUM kill; CONJ_TAC; REPEAT WEAKER_STRIP_TAC; REWRITE_TAC[Sphere.ineq]; REWRITE_TAC[Merge_ineq.delta_y_sym]; BY(REAL_ARITH_TAC); REPEAT WEAKER_STRIP_TAC; REWRITE_TAC[Sphere.ineq]; TYPIFY `delta_y y1 y5 y6 y4 y2 y3 = delta_y y1 y2 y3 y4 y5 y6` (C SUBGOAL_THEN SUBST1_TAC); BY(MESON_TAC[Merge_ineq.delta_y_sym]); BY(REAL_ARITH_TAC) ]);; (* }}} *) (* Prove "8673686234" using inequalities "6170936724", "8673686234 a", "8673686234 b", "8673686234 c" *) let LEMMA_8673686234 = prove_by_refinement( ` (!y1 y2 y3 y4 y5 y6. ineq [ (&3,y1,&3); (&2,y2,#2.52); (&2,y3,#2.52); (sqrt8,y4,&4 * h0); (&2,y5,#2.52); (&2,y6,#2.52) ] ( y_of_x delta_x1 y1 y2 y3 y4 y5 y6 < &0)) /\ (!y1 y2 y3 y4 y5 y6. ineq [ (sqrt8,y1,#3.0); (&2,y2,#2.07); (&2,y3,#2.07); (sqrt8,y4,&4 * h0); (&2,y5,#2.07); (&2,y6,#2.07) ] ((y2 + y3 + y5 + y6 - #7.99 - #0.00385 * delta_y y1 y2 y3 y4 y5 y6 > #2.75 * ((y1 + y4)/ &2 - sqrt8)) ) ) /\ (!y1 y2 y3 y4 y5 y6. ineq [ (sqrt8,y1,#3.0); (#2.07,y2,&2 * h0); (&2,y3,&2 * h0); (#3.0,y4,#3.0); (&2,y5,&2 * h0); (&2,y6,&2 * h0) ] ((y2 + y3 + y5 + y6 - #7.99 > #2.75 * (y1 - sqrt8)) \/ (delta_y y1 y2 y3 y4 y5 y6 < &0) ) ) /\ (!y1 y2 y3 y4 y5 y6. ineq [ (sqrt8,y1,#3.0); (#2.07,y2,&2 * h0); (&2,y3,&2 * h0); (sqrt8,y4,#3.0); (&2,y5,&2 * h0); (&2,y6,&2 * h0) ] ((y2 + y3 + y5 + y6 - #7.99 > #2.75 * ((y1 + y4)/ &2 - sqrt8)) \/ (y2 + y3 + y5 + y6 - #7.99 - #0.00385 * delta_y y1 y2 y3 y4 y5 y6 > #2.75 * ((y1 + y4)/ &2 - sqrt8)) \/ (delta_y y1 y2 y3 y4 y5 y6 < &0) ) ) ==> (!y1 y2 y3 y4 y5 y6. ineq [ (sqrt8,y1,#3.0); (&2,y2,&2 * h0); (&2,y3,&2 * h0); (sqrt8,y4,&4 * h0); (&2,y5,&2 * h0); (&2,y6,&2 * h0) ] ((y2 + y3 + y5 + y6 - #7.99 > #2.75 * (y1 - sqrt8)) \/ (delta_y y1 y2 y3 y4 y5 y6 < &0) \/ (y4 < y1)) ) `, (* {{{ proof *) [ DISCH_TAC; MATCH_MP_TAC WLOG_8673686234; REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM_ST `delta_y` MP_TAC THEN REPEAT WEAKER_STRIP_TAC; COMMENT "case a"; ASM_CASES_TAC `y2 <= #2.07`; FIRST_X_ASSUM_ST `&2,y2,#2.07` MP_TAC; DISCH_THEN (C INTRO_TAC [`y1`;`y2`;`y3`;`y4`;`y5`;`y6`]); REWRITE_TAC[Sphere.ineq]; REPEAT (FIRST_X_ASSUM_ST `y <= y2` MP_TAC); BY(REAL_ARITH_TAC); FIRST_X_ASSUM_ST `&2,y2,#2.07` kill; COMMENT "case c"; ASM_CASES_TAC `y4 <= #3.0`; FIRST_X_ASSUM_ST `ineq` MP_TAC; DISCH_THEN (C INTRO_TAC [`y1`;`y2`;`y3`;`y4`;`y5`;`y6`]); REWRITE_TAC[Sphere.ineq]; REPEAT (FIRST_X_ASSUM_ST `y <= y2` MP_TAC); BY(REAL_ARITH_TAC); FIRST_X_ASSUM_ST `ineq` kill; COMMENT "case b"; ASM_CASES_TAC `delta_y y1 y2 y3 y4 y5 y6 < &0`; BY(ASM_REWRITE_TAC[Sphere.ineq]); ASM_CASES_TAC `y4 < y1`; BY(ASM_REWRITE_TAC[Sphere.ineq]); ASM_REWRITE_TAC[]; COMMENT "ups"; REWRITE_TAC[Sphere.ineq]; REPEAT WEAKER_STRIP_TAC; TYPIFY `&0 < ups_x (y1*y1) (y2*y2) (y6*y6)` (C SUBGOAL_THEN ASSUME_TAC); MATCH_MP_TAC Merge_ineq.UPS_X_POS; REPLICATE_TAC 14 (FIRST_X_ASSUM MP_TAC); MP_TAC Flyspeck_constants.bounds; BY(REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC); TYPIFY `&0 < ups_x (y1*y1) (y3*y3) (y5*y5)` (C SUBGOAL_THEN ASSUME_TAC); MATCH_MP_TAC Merge_ineq.UPS_X_POS; REPLICATE_TAC 14 (FIRST_X_ASSUM MP_TAC); MP_TAC Flyspeck_constants.bounds; BY(REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC); COMMENT "construct y4'"; TYPIFY `?y4'. y4 <= y4' /\ delta_y y1 y2 y3 y4' y5 y6 = &0` (C SUBGOAL_THEN MP_TAC); MATCH_MP_TAC delta_y_root_exists; CONJ_TAC; BY(ASM_TAC THEN REAL_ARITH_TAC); MP_TAC Flyspeck_constants.bounds; BY(ASM_TAC THEN REAL_ARITH_TAC); REPEAT WEAKER_STRIP_TAC; INTRO_TAC IVT_delta_y_full [`#3.0`;`y4'`;`#2.07`;`y2`;`&2`;`y6`;`y1`;`&2`;`y5`;`&2`;`y3`]; ASM_REWRITE_TAC[arith `&0 <= #3.0 /\ &0 <= #2.07 /\ &0 <= &2`]; ANTS_TAC; FIRST_X_ASSUM_ST `ineq` kill; 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); REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM (C INTRO_TAC [`#3.0`;`y2'`;`y3'`;`y1`;`y5'`;`y6'`]); REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`]; DISCH_THEN MATCH_MP_TAC; BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC); TYPIFY `delta_y y4' y2 y6 y1 y5 y3 = delta_y y1 y2 y3 y4' y5 y6` (C SUBGOAL_THEN SUBST1_TAC); BY(MESON_TAC[Merge_ineq.delta_y_sym]); ASM_REWRITE_TAC[]; FIRST_X_ASSUM_ST `ineq` kill; CONJ_TAC; BY(ASM_TAC THEN MP_TAC Flyspeck_constants.bounds THEN REAL_ARITH_TAC); CONJ_TAC; REPEAT WEAKER_STRIP_TAC; MATCH_MP_TAC Merge_ineq.UPS_X_POS; ASM_REWRITE_TAC[]; BY(MP_TAC Flyspeck_constants.bounds THEN ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC); CONJ_TAC; REPEAT WEAKER_STRIP_TAC; MATCH_MP_TAC Merge_ineq.UPS_X_POS; ASM_REWRITE_TAC[]; BY(MP_TAC Flyspeck_constants.bounds THEN ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC); BY(ASM_TAC THEN REAL_ARITH_TAC); DISCH_THEN DISJ_CASES_TAC; FIRST_X_ASSUM (X_CHOOSE_THEN `y2':real` ASSUME_TAC); FIRST_X_ASSUM (X_CHOOSE_THEN `y6':real` ASSUME_TAC); FIRST_X_ASSUM (X_CHOOSE_THEN `y5':real` ASSUME_TAC); FIRST_X_ASSUM (X_CHOOSE_THEN `y3':real` ASSUME_TAC); FIRST_X_ASSUM (C INTRO_TAC [`y1`;`y2'`;`y3'`;`#3.0`;`y5'`;`y6'`]); ASM_REWRITE_TAC[Sphere.ineq;arith `~(&0 < &0)`;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`]; TYPIFY `delta_y y1 y2' y3' #3.0 y5' y6' = delta_y #3.0 y2' y6' y1 y5' y3'` (C SUBGOAL_THEN SUBST1_TAC); BY(MESON_TAC[Merge_ineq.delta_y_sym]); ASM_REWRITE_TAC[]; ANTS_TAC; BY(MP_TAC Flyspeck_constants.bounds THEN ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC); BY(ASM_TAC THEN REAL_ARITH_TAC); COMMENT "second case: long diags"; PROOF_BY_CONTR_TAC; FIRST_X_ASSUM_ST `delta_y` MP_TAC; REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM MP_TAC; REWRITE_TAC[Sphere.delta_y;arith `&2 * &2 = &4`]; TYPED_ABBREV_TAC `u = y1' * y1' - &9` ; TYPIFY `y1' * y1' = &9 + u` (C SUBGOAL_THEN SUBST1_TAC); BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC); TYPED_ABBREV_TAC `v = y1 * y1 - &8` ; TYPIFY `y1 * y1 = &8 + v` (C SUBGOAL_THEN SUBST1_TAC); BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC); TYPIFY `&0 <= u` (C SUBGOAL_THEN ASSUME_TAC); EXPAND_TAC "u"; REWRITE_TAC[arith `&0 <= x - &9 <=> &3 * &3 <= x`]; GMATCH_SIMP_TAC Misc_defs_and_lemmas.ABS_SQUARE_LE; BY(FIRST_X_ASSUM_ST `#3.0` MP_TAC THEN REAL_ARITH_TAC); TYPIFY `&0 <= v` (C SUBGOAL_THEN ASSUME_TAC); EXPAND_TAC "v"; TYPIFY_GOAL_THEN `!x. &0 <= x - &8 <=> sqrt8 * sqrt8 <= x` (unlist REWRITE_TAC); REWRITE_TAC[Nonlinear_lemma.sqrt8_2]; BY(REAL_ARITH_TAC); GMATCH_SIMP_TAC Misc_defs_and_lemmas.ABS_SQUARE_LE; REPLICATE_TAC 3 (FIRST_X_ASSUM_ST `sqrt8` MP_TAC); BY(MP_TAC Flyspeck_constants.bounds THEN REAL_ARITH_TAC); MATCH_MP_TAC (arith `&0 < -- x ==> ~(x = &0)`); 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); REWRITE_TAC[Sphere.delta_x]; BY(REAL_ARITH_TAC); MATCH_MP_TAC (arith `&0 < x /\ &0 <= y ==> &0 < x + y`); CONJ_TAC; BY(REAL_ARITH_TAC); REWRITE_TAC[arith `v pow 2 = v*v`]; REPEAT (GMATCH_SIMP_TAC (arith `&0 <= x /\ &0 <= y ==> &0 <= x + y`)); GMATCH_SIMP_TAC REAL_LE_MUL; REPEAT (GMATCH_SIMP_TAC REAL_LE_MUL); ASM_REWRITE_TAC[]; BY(REAL_ARITH_TAC) ]);; (* }}} *) let WLOG_5691615370 = prove_by_refinement( `(!y1 y2 y3 y4 y5 y6. ineq [ (#3.0,y1,#3.0); (&2,y2,#2.52); (&2,y3,#2.52); (#3.0,y4,#3.0); (&2,y5,#2.52); (&2,y6,#2.52) ] ((delta_y y1 y2 y3 y4 y5 y6 < &0) \/ (y2 + y3 + y5 + y6 > #8.472) \/ (y2 < y3) \/ (y2 < y5) \/ (y2 < y6 ) \/ (y3 < y6))) ==> (!y1 y2 y3 y4 y5 y6. ineq [ (#3.0,y1,#3.0); (&2,y2,#2.52); (&2,y3,#2.52); (#3.0,y4,#3.0); (&2,y5,#2.52); (&2,y6,#2.52) ] ((delta_y y1 y2 y3 y4 y5 y6 < &0) \/ (y2 + y3 + y5 + y6 > #8.472)))`, (* {{{ proof *) [ 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)`]; DISCH_TAC; MATCH_MP_TAC Terminal.REAL_WLOG_SQUARE2_LEMMA; CONJ_TAC; REPEAT GEN_TAC; REWRITE_TAC[Sphere.ineq;Merge_ineq.delta_y_sym]; TYPIFY `delta_y y1 y5 y6 y4 y2 y2' = delta_y y1 y2 y2' y4 y5 y6` (C SUBGOAL_THEN SUBST1_TAC); BY(MESON_TAC[Merge_ineq.delta_y_sym]); REWRITE_TAC[REAL_ADD_AC]; BY(MESON_TAC[]); REPEAT WEAKER_STRIP_TAC; REWRITE_TAC[Sphere.ineq]; RULE_ASSUM_TAC (REWRITE_RULE[Sphere.ineq]); BY(ASM_MESON_TAC[arith `x <= y ==> ~(y < x)`]) ]);; (* }}} *) (* Use 5584033259 and 6170936724 and 5691615370 to prove the lemma. *) let LEMMA_5691615370 = prove_by_refinement( ` (!y1 y2 y3 y4 y5 y6. ineq [ (&3,y1,&4 * h0); (&2,y2,#2.472); (&2,y3,#2.472); (&3,y4,&4 * h0); (&2,y5,#2.472); (&2,y6,#2.472) ] ( y1 < &4 \/ delta_y y1 y2 y3 y4 y5 y6 < &0 )) /\ (!y1 y2 y3 y4 y5 y6. ineq [ (&3,y1,&3); (&2,y2,#2.52); (&2,y3,#2.52); (sqrt8,y4,&4 * h0); (&2,y5,#2.52); (&2,y6,#2.52) ] ( y_of_x delta_x1 y1 y2 y3 y4 y5 y6 < &0)) /\ (!y1 y2 y3 y4 y5 y6. ineq [ (#3.0,y1,#3.0); (&2,y2,#2.52); (&2,y3,#2.52); (#3.0,y4,#3.0); (&2,y5,#2.52); (&2,y6,#2.52) ] ((delta_y y1 y2 y3 y4 y5 y6 < &0) \/ (y2 + y3 + y5 + y6 > #8.472) \/ (y2 < y3) \/ (y2 < y5) \/ (y2 < y6 ) \/ (y3 < y6))) ==> (!y1 y2 y3 y4 y5 y6. ineq [ (#3.0,y1,&4 * h0); (&2,y2,#2.52); (&2,y3,#2.52); (#3.0,y4,&4 * h0); (&2,y5,#2.52); (&2,y6,#2.52) ] ((delta_y y1 y2 y3 y4 y5 y6 < &0) \/ (y2 + y3 + y5 + y6 > #8.472))) `, (* {{{ proof *) [ REWRITE_TAC[Sphere.y_of_x;Functional_equation.nonf_ups_126]; STRIP_TAC; FIRST_X_ASSUM (ASSUME_TAC o (MATCH_MP WLOG_5691615370)); REWRITE_TAC[Sphere.ineq]; REPEAT WEAKER_STRIP_TAC; ASM_CASES_TAC `delta_y y1 y2 y3 y4 y5 y6 < &0`; BY(ASM_REWRITE_TAC[]); ASM_REWRITE_TAC[]; COMMENT "construct y4'"; TYPIFY `?y4'. y4 <= y4' /\ delta_y y1 y2 y3 y4' y5 y6 = &0` (C SUBGOAL_THEN MP_TAC); MATCH_MP_TAC delta_y_root_exists; CONJ_TAC; BY(ASM_TAC THEN REAL_ARITH_TAC); BY(ASM_TAC THEN REAL_ARITH_TAC); REPEAT WEAKER_STRIP_TAC; COMMENT "bound 4 on diagonal"; PROOF_BY_CONTR_TAC; TYPIFY `y2 <= #2.472 /\ y3 <= #2.472 /\ y5 <= #2.472 /\ y6 <= #2.472` (C SUBGOAL_THEN ASSUME_TAC); BY(REPLICATE_TAC 14 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC); TYPIFY `y1 < &4` (C SUBGOAL_THEN ASSUME_TAC); FIRST_X_ASSUM_ST `y1 < &4` (C INTRO_TAC [`y1`;`y2`;`y3`;`y4`;`y5`;`y6`]); ASM_REWRITE_TAC[Sphere.y_of_x;Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`]; DISCH_THEN MATCH_MP_TAC; BY(REPLICATE_TAC 17 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC); INTRO_TAC IVT_delta_y_full [`#3.0`;`y4'`;`&2`;`y2`;`&2`;`y6`;`y1`;`&2`;`y5`;`&2`;`y3`]; ASM_REWRITE_TAC[arith `&0 <= #3.0 /\ &0 <= &2`]; DISCH_THEN MP_TAC THEN ANTS_TAC; FIRST_X_ASSUM_ST `ineq` kill; 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); REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM (C INTRO_TAC [`#3.0`;`y2'`;`y3'`;`y1`;`y5'`;`y6'`]); REWRITE_TAC[Sphere.y_of_x;Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`]; DISCH_THEN MATCH_MP_TAC; BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN MP_TAC Flyspeck_constants.bounds THEN REAL_ARITH_TAC); TYPIFY `delta_y y4' y2 y6 y1 y5 y3 = delta_y y1 y2 y3 y4' y5 y6` (C SUBGOAL_THEN SUBST1_TAC); BY(MESON_TAC[Merge_ineq.delta_y_sym]); ASM_REWRITE_TAC[]; FIRST_X_ASSUM_ST `ineq` kill; CONJ_TAC; BY(ASM_TAC THEN REAL_ARITH_TAC); CONJ_TAC; GEN_TAC; X_GEN_TAC `y6':real`; REPEAT WEAKER_STRIP_TAC; MATCH_MP_TAC Merge_ineq.UPS_X_POS; BY(REPLICATE_TAC 22 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC); CONJ_TAC; GEN_TAC; X_GEN_TAC `y3':real`; REPEAT WEAKER_STRIP_TAC; MATCH_MP_TAC Merge_ineq.UPS_X_POS; BY(REPLICATE_TAC 22 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC); BY(REPLICATE_TAC 15 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC); TYPIFY `!z1 z4. #3.0 <= z1 /\ #3.0 <= z4 ==> delta_y z1 (&2) (&2) z4 (&2) (&2) < &0` (C SUBGOAL_THEN ASSUME_TAC); REWRITE_TAC[Sphere.delta_y;arith `&2 * &2 = &4`]; REPEAT WEAKER_STRIP_TAC; TYPED_ABBREV_TAC `u = z1 * z1 - &9` ; TYPIFY `z1 * z1 = &9 + u` (C SUBGOAL_THEN SUBST1_TAC); BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC); TYPED_ABBREV_TAC `v = z4 * z4 - &9` ; TYPIFY `z4 * z4 = &9 + v` (C SUBGOAL_THEN SUBST1_TAC); BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC); TYPIFY `&0 <= u` (C SUBGOAL_THEN ASSUME_TAC); EXPAND_TAC "u"; REWRITE_TAC[arith `&0 <= x - &9 <=> &3 * &3 <= x`]; GMATCH_SIMP_TAC Misc_defs_and_lemmas.ABS_SQUARE_LE; BY(REPLICATE_TAC 2 (FIRST_X_ASSUM_ST `#3.0` MP_TAC) THEN REAL_ARITH_TAC); TYPIFY `&0 <= v` (C SUBGOAL_THEN ASSUME_TAC); EXPAND_TAC "v"; REWRITE_TAC[arith `&0 <= x - &9 <=> &3 * &3 <= x`]; GMATCH_SIMP_TAC Misc_defs_and_lemmas.ABS_SQUARE_LE; BY(REPLICATE_TAC 2 (FIRST_X_ASSUM_ST `#3.0` MP_TAC) THEN REAL_ARITH_TAC); MATCH_MP_TAC (arith `&0 < -- x ==> x < &0`); 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); REWRITE_TAC[Sphere.delta_x]; BY(REAL_ARITH_TAC); MATCH_MP_TAC (arith `&0 < x /\ &0 <= y ==> &0 < x + y`); CONJ_TAC; BY(REAL_ARITH_TAC); REPEAT (GMATCH_SIMP_TAC (arith `&0 <= x /\ &0 <= y ==> &0 <= x + y`)); REPEAT (GMATCH_SIMP_TAC REAL_LE_MUL); ASM_REWRITE_TAC[]; BY(REAL_ARITH_TAC); REWRITE_TAC[DE_MORGAN_THM;NOT_EXISTS_THM]; CONJ2_TAC; GEN_TAC; FIRST_X_ASSUM (C INTRO_TAC [`y1'`;`y1`]); ASM_REWRITE_TAC[]; BY(ASM_TAC THEN REAL_ARITH_TAC); GEN_TAC; X_GEN_TAC `y6':real`; GEN_TAC; X_GEN_TAC `y3':real`; REWRITE_TAC[GSYM DE_MORGAN_THM]; REPEAT WEAKER_STRIP_TAC; INTRO_TAC IVT_delta_y_full [`#3.0`;`y1`;`&2`;`y2'`;`&2`;`y3'`;`#3.0`;`&2`;`y5'`;`&2`;`y6'`]; ASM_REWRITE_TAC[arith `&0 <= #3.0 /\ &0 <= &2 /\ &0 < #3.0`]; DISCH_THEN MP_TAC THEN ANTS_TAC; FIRST_X_ASSUM_ST `ineq` kill; 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); REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM (C INTRO_TAC [`#3.0`;`y2''`;`y3''`;`#3.0`;`y5''`;`y6''`]); REWRITE_TAC[Sphere.y_of_x;Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`]; DISCH_THEN MATCH_MP_TAC; BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN MP_TAC Flyspeck_constants.bounds THEN REAL_ARITH_TAC); TYPIFY `delta_y y1 y2' y3' #3.0 y5' y6' = delta_y #3.0 y2' y6' y1 y5' y3'` (C SUBGOAL_THEN SUBST1_TAC); BY(MESON_TAC[Merge_ineq.delta_y_sym]); ASM_REWRITE_TAC[]; FIRST_X_ASSUM_ST `ineq` kill; CONJ_TAC; REPEAT WEAKER_STRIP_TAC; MATCH_MP_TAC Merge_ineq.UPS_X_POS; BY(REPLICATE_TAC 22 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC); REPEAT WEAKER_STRIP_TAC; MATCH_MP_TAC Merge_ineq.UPS_X_POS; BY(REPLICATE_TAC 22 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC); TYPIFY_GOAL_THEN `~(?y1. #3.0 < y1 /\ delta_y y1 (&2) (&2) #3.0 (&2) (&2) = &0)` (unlist REWRITE_TAC); REWRITE_TAC[NOT_EXISTS_THM]; GEN_TAC; FIRST_X_ASSUM (C INTRO_TAC [`y1'`;`#3.0`]); BY(REPLICATE_TAC 22 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC); REWRITE_TAC[NOT_EXISTS_THM]; REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM (C INTRO_TAC [`#3.0`;`y2''`;`y3''`;`#3.0`;`y5''`;`y6''`]); ASM_REWRITE_TAC[Sphere.y_of_x;Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`]; BY(REPLICATE_TAC 37 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC) ]);; (* }}} *) end;;