(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(*                                                                            *)
(* Chapter: Tame Hypermap                                                     *)
(* Author: Alexey Solovyev                                                    *)
(* Date: 2010-07-07                                                           *)
(* Some nonlinear (polynomial) inequalities                                   *)
(* ========================================================================== *)

flyspeck_needs "general/sphere.hl";;
flyspeck_needs "trigonometry/trigonometry.hl";;
flyspeck_needs "nonlinear/ineq.hl";;


module Tame_inequalities = struct


let let_RULE = fun th -> REWRITE_RULE[DEPTH_CONV let_CONV (concl th)] th;;

let REMOVE_ASSUM = POP_ASSUM (fun th -> ALL_TAC);;



(* Alternative form for ineq *)
let INEQ_ALT = 
prove(`!A bounds. ineq bounds A <=> (ALL (\(a,x,b). a <= x /\ x <= b) bounds ==> A)`,
GEN_TAC THEN MATCH_MP_TAC list_INDUCT THEN REPEAT STRIP_TAC THENL [ REWRITE_TAC[Sphere.ineq; ALL]; ALL_TAC ] THEN MP_TAC (ISPEC `a0:real#real#real` PAIR_SURJECTIVE) THEN DISCH_THEN (X_CHOOSE_THEN `a:real` MP_TAC) THEN DISCH_THEN (CHOOSE_THEN MP_TAC) THEN MP_TAC (ISPEC `y:real#real` PAIR_SURJECTIVE) THEN DISCH_THEN (X_CHOOSE_THEN `x:real` MP_TAC) THEN DISCH_THEN (X_CHOOSE_THEN `b:real` MP_TAC) THEN DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN ASM_SIMP_TAC[Sphere.ineq; ALL; IMP_IMP]);;
(**************************************************)
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`,
REPEAT STRIP_TAC THEN 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 DISJ_CASES_TAC (REAL_ARITH `&0 <= a * x0 + a * x + b \/ a * x0 + a * x + b < &0`) THENL [ DISJ1_TAC THEN MATCH_MP_TAC REAL_LE_MUL THEN ASM_REWRITE_TAC[REAL_ARITH `&0 <= x - x0 <=> x0 <= x`]; DISJ2_TAC THEN REWRITE_TAC[REAL_ARITH `(x - x1) * (a * x1 + a * x + b) = (x1 - x) * --(a * x1 + a * x + b)`] THEN MATCH_MP_TAC REAL_LE_MUL THEN ASM_REWRITE_TAC[REAL_ARITH `&0 <= x1 - x <=> x <= x1`; REAL_ARITH `&0 <= --a <=> a <= &0`] THEN MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `a * x0 + a * x + b:real` THEN ASM_SIMP_TAC[REAL_LT_IMP_LE] THEN REWRITE_TAC[REAL_ARITH `a + b <= c + b <=> a <= c`] THEN REWRITE_TAC[REAL_ARITH `a * x1 <= a * x0 <=> &0 <= --a * (x1 - x0)`] THEN MATCH_MP_TAC REAL_LE_MUL THEN REPEAT (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC ]);;
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`,
REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC lemma THEN ASM_REWRITE_TAC[]);;
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`,
REPEAT STRIP_TAC THEN 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 [ REWRITE_TAC[]; ALL_TAC ] THEN MATCH_MP_TAC lemma' THEN ASM_REWRITE_TAC[Sphere.delta_x; FUN_EQ_THM] THEN 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 POP_ASSUM MP_TAC THEN REAL_ARITH_TAC);;
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`,
REPEAT STRIP_TAC THEN 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 [ REWRITE_TAC[]; ALL_TAC ] THEN MATCH_MP_TAC lemma' THEN ASM_REWRITE_TAC[Sphere.delta_x; FUN_EQ_THM] THEN 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 POP_ASSUM MP_TAC THEN REAL_ARITH_TAC);;
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`,
REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[SYM (BETA_CONV `(\x. delta_x x1 x2 x x4 x5 x6) x3`)] THEN MATCH_MP_TAC lemma' THEN ASM_REWRITE_TAC[Sphere.delta_x; FUN_EQ_THM] THEN 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 POP_ASSUM MP_TAC THEN REAL_ARITH_TAC);;
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`,
REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[SYM (BETA_CONV `(\x. delta_x x1 x2 x3 x x5 x6) x4`)] THEN MATCH_MP_TAC lemma' THEN ASM_REWRITE_TAC[Sphere.delta_x; FUN_EQ_THM] THEN 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 POP_ASSUM MP_TAC THEN REAL_ARITH_TAC);;
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`,
REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[SYM (BETA_CONV `(\x. delta_x x1 x2 x3 x4 x x6) x5`)] THEN MATCH_MP_TAC lemma' THEN ASM_REWRITE_TAC[Sphere.delta_x; FUN_EQ_THM] THEN 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 POP_ASSUM MP_TAC THEN REAL_ARITH_TAC);;
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`,
REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[SYM (BETA_CONV `(\x. delta_x x1 x2 x3 x4 x5 x) x6`)] THEN MATCH_MP_TAC lemma' THEN ASM_REWRITE_TAC[Sphere.delta_x; FUN_EQ_THM] THEN 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 POP_ASSUM MP_TAC THEN REAL_ARITH_TAC);;
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`,
REWRITE_TAC[real_ge] THEN REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_LE_TRANS THENL [ EXISTS_TAC `(f:real->real) x0` THEN ASM_REWRITE_TAC[]; EXISTS_TAC `(f:real->real) x1` THEN ASM_REWRITE_TAC[] ]);;
(* delta_x > 0 for x IN [4,4 h0^2] *)
let delta_x_pos = 
prove(`!x1 x2 x3 x4 x5 x6. ineq [#4.0,x1,#6.3504; #4.0,x2,#6.3504; #4.0,x3,#6.3504; #4.0,x4,#6.3504; #4.0,x5,#6.3504; #4.0,x6,#6.3504] (delta_x x1 x2 x3 x4 x5 x6 >= #128.0)`,
REPEAT STRIP_TAC THEN REWRITE_TAC[INEQ_ALT; ALL] THEN REPEAT STRIP_TAC THEN ASSUME_TAC (REAL_ARITH `#4.0 <= #4.0 /\ #4.0 <= #6.3504`) THEN (* x1 *) ONCE_REWRITE_TAC[SYM (BETA_CONV `(\x. delta_x x x2 x3 x4 x5 x6) x1`)] THEN MATCH_MP_TAC main_lemma THEN MAP_EVERY EXISTS_TAC [`#4.0`; `#6.3504`] THEN ASM_SIMP_TAC[lemma1] THEN CONJ_TAC THEN (* x2 *) ONCE_REWRITE_TAC[SYM (BETA_CONV `(\x. delta_x x1 x x3 x4 x5 x6) x2`)] THEN MATCH_MP_TAC main_lemma THEN MAP_EVERY EXISTS_TAC [`#4.0`; `#6.3504`] THEN ASM_SIMP_TAC[lemma2] THEN CONJ_TAC THEN (* x3 *) ONCE_REWRITE_TAC[SYM (BETA_CONV `(\x. delta_x x1 x2 x x4 x5 x6) x3`)] THEN MATCH_MP_TAC main_lemma THEN MAP_EVERY EXISTS_TAC [`#4.0`; `#6.3504`] THEN ASM_SIMP_TAC[lemma3] THEN CONJ_TAC THEN (* x4 *) ONCE_REWRITE_TAC[SYM (BETA_CONV `(\x. delta_x x1 x2 x3 x x5 x6) x4`)] THEN MATCH_MP_TAC main_lemma THEN MAP_EVERY EXISTS_TAC [`#4.0`; `#6.3504`] THEN ASM_SIMP_TAC[lemma4] THEN CONJ_TAC THEN (* x5 *) ONCE_REWRITE_TAC[SYM (BETA_CONV `(\x. delta_x x1 x2 x3 x4 x x6) x5`)] THEN MATCH_MP_TAC main_lemma THEN MAP_EVERY EXISTS_TAC [`#4.0`; `#6.3504`] THEN ASM_SIMP_TAC[lemma5] THEN CONJ_TAC THEN (* x6 *) ONCE_REWRITE_TAC[SYM (BETA_CONV `(\x. delta_x x1 x2 x3 x4 x5 x) x6`)] THEN MATCH_MP_TAC main_lemma THEN MAP_EVERY EXISTS_TAC [`#4.0`; `#6.3504`] THEN ASM_SIMP_TAC[lemma6] THEN CONJ_TAC THEN (* Final stage *) REWRITE_TAC[Sphere.delta_x] THEN CONV_TAC REAL_RAT_REDUCE_CONV);;
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`,
REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[SYM (BETA_CONV `(\x. delta_x x1 x2 x x4 x5 x6) x3`)] THEN MATCH_MP_TAC lemma' THEN ASM_REWRITE_TAC[Sphere.delta_x; FUN_EQ_THM] THEN 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 POP_ASSUM MP_TAC THEN REAL_ARITH_TAC);;
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`,
REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[SYM (BETA_CONV `(\x. delta_x x1 x2 x3 x4 x5 x) x6`)] THEN MATCH_MP_TAC lemma' THEN ASM_REWRITE_TAC[Sphere.delta_x; FUN_EQ_THM] THEN 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 POP_ASSUM MP_TAC THEN REAL_ARITH_TAC);;
(* delta_x > 0 for a special configuration of three points *)
let delta_x_3_points = 
prove(`!x1 x2 x3 x6. ineq [#4.0,x1,#6.3504; #4.0,x2,#6.3504; #4.0,x3,#6.3504; #0.64,x6,#6.3504] (delta_x x1 x2 x3 (#4.0) (#4.0) x6 >= #13.0)`,
REPEAT STRIP_TAC THEN REWRITE_TAC[INEQ_ALT; ALL] THEN REPEAT STRIP_TAC THEN ASSUME_TAC (REAL_ARITH `#4.0 <= #4.0 /\ #4.0 <= #6.3504`) THEN (* x1 *) ONCE_REWRITE_TAC[SYM (BETA_CONV `(\x. delta_x x x2 x3 x4 x5 x6) x1`)] THEN MATCH_MP_TAC main_lemma THEN MAP_EVERY EXISTS_TAC [`#4.0`; `#6.3504`] THEN ASM_SIMP_TAC[lemma1] THEN CONJ_TAC THEN (* x2 *) ONCE_REWRITE_TAC[SYM (BETA_CONV `(\x. delta_x x1 x x3 x4 x5 x6) x2`)] THEN MATCH_MP_TAC main_lemma THEN MAP_EVERY EXISTS_TAC [`#4.0`; `#6.3504`] THEN ASM_SIMP_TAC[lemma2] THEN CONJ_TAC THEN (* x3 *) ONCE_REWRITE_TAC[SYM (BETA_CONV `(\x. delta_x x1 x2 x x4 x5 x6) x3`)] THEN MATCH_MP_TAC main_lemma THEN MAP_EVERY EXISTS_TAC [`#4.0`; `#6.3504`] THEN ASM_SIMP_TAC[lemma3] THEN CONJ_TAC THEN (* x6 *) ONCE_REWRITE_TAC[SYM (BETA_CONV `(\x. delta_x x1 x2 x3 x4 x5 x) x6`)] THEN MATCH_MP_TAC main_lemma THEN MAP_EVERY EXISTS_TAC [`#0.64`; `#6.3504`] THEN ASM_SIMP_TAC[lemma6] THEN CONJ_TAC THEN (* Final stage *) REWRITE_TAC[Sphere.delta_x] THEN CONV_TAC REAL_RAT_REDUCE_CONV);;
(************************************************************) (* eta_y pow 2 <= #2.2 *)
let lemma1 = 
prove(`!x1 x2 x3. #4.0 <= x1 /\ x1 <= #6.3504 ==> #2.2 * ups_x x1 x2 x3 - x1 * x2 * x3 >= #2.2 * ups_x #4.0 x2 x3 - #4.0 * x2 * x3 \/ #2.2 * ups_x x1 x2 x3 - x1 * x2 * x3 >= #2.2 * ups_x #6.3504 x2 x3 - #6.3504 * x2 * x3`,
REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[SYM (BETA_CONV `(\x. #2.2 * ups_x x x2 x3 - x * x2 * x3) x1`)] THEN MATCH_MP_TAC lemma' THEN ASM_REWRITE_TAC[Sphere.ups_x; FUN_EQ_THM] THEN MAP_EVERY EXISTS_TAC [`-- #2.2`; `#2.2*(&2 * x3 + &2 * x2) - x2 * x3`; `#2.2 * (&2 * x2 * x3 - x2*x2 - x3*x3)`] THEN REAL_ARITH_TAC);;
let lemma2 = 
prove(`!x1 x2 x3. #4.0 <= x2 /\ x2 <= #6.3504 ==> #2.2 * ups_x x1 x2 x3 - x1 * x2 * x3 >= #2.2 * ups_x x1 #4.0 x3 - x1 * #4.0 * x3 \/ #2.2 * ups_x x1 x2 x3 - x1 * x2 * x3 >= #2.2 * ups_x x1 #6.3504 x3 - x1 * #6.3504 * x3`,
REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[SYM (BETA_CONV `(\x. #2.2 * ups_x x1 x x3 - x1 * x * x3) x2`)] THEN MATCH_MP_TAC lemma' THEN ASM_REWRITE_TAC[Sphere.ups_x; FUN_EQ_THM] THEN MAP_EVERY EXISTS_TAC [`-- #2.2`; `#2.2*(&2 * x1 + &2 * x3) - x1 * x3`; `#2.2 * (&2 * x1 * x3 - x1*x1 - x3*x3)`] THEN REAL_ARITH_TAC);;
let lemma3 = 
prove(`!x1 x2 x3. #4.0 <= x3 /\ x3 <= #6.3504 ==> #2.2 * ups_x x1 x2 x3 - x1 * x2 * x3 >= #2.2 * ups_x x1 x2 #4.0 - x1 * x2 * #4.0 \/ #2.2 * ups_x x1 x2 x3 - x1 * x2 * x3 >= #2.2 * ups_x x1 x2 #6.3504 - x1 * x2 * #6.3504`,
REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[SYM (BETA_CONV `(\x. #2.2 * ups_x x1 x2 x - x1 * x2 * x) x3`)] THEN MATCH_MP_TAC lemma' THEN ASM_REWRITE_TAC[Sphere.ups_x; FUN_EQ_THM] THEN MAP_EVERY EXISTS_TAC [`-- #2.2`; `#2.2*(&2 * x1 + &2 * x2) - x2 * x1`; `#2.2 * (&2 * x2 * x1 - x2*x2 - x1*x1)`] THEN REAL_ARITH_TAC);;
let eta_x_ineq_lemma = 
prove(`!x1 x2 x3. ineq [#4.0,x1,#6.3504; #4.0,x2,#6.3504; #4.0,x3,#6.3504] (#2.2 * ups_x x1 x2 x3 - x1 * x2 * x3 >= &0)`,
REPEAT STRIP_TAC THEN REWRITE_TAC[INEQ_ALT; ALL] THEN REPEAT STRIP_TAC THEN ASSUME_TAC (REAL_ARITH `#4.0 <= #4.0 /\ #4.0 <= #6.3504`) THEN (* x1 *) ONCE_REWRITE_TAC[SYM (BETA_CONV `(\x. #2.2 * ups_x x x2 x3 - x * x2 * x3) x1`)] THEN MATCH_MP_TAC main_lemma THEN MAP_EVERY EXISTS_TAC [`#4.0`; `#6.3504`] THEN ASM_SIMP_TAC[lemma1] THEN CONJ_TAC THEN (* x2 *) ONCE_REWRITE_TAC[SYM (BETA_CONV `(\x. #2.2 * ups_x x1 x x3 - x1 * x * x3) x2`)] THEN MATCH_MP_TAC main_lemma THEN MAP_EVERY EXISTS_TAC [`#4.0`; `#6.3504`] THEN ASM_SIMP_TAC[lemma2] THEN CONJ_TAC THEN (* x3 *) ONCE_REWRITE_TAC[SYM (BETA_CONV `(\x. #2.2 * ups_x x1 x2 x - x1 * x2 * x) x3`)] THEN MATCH_MP_TAC main_lemma THEN MAP_EVERY EXISTS_TAC [`#4.0`; `#6.3504`] THEN ASM_SIMP_TAC[lemma3] THEN CONJ_TAC THEN (* Final stage *) REWRITE_TAC[Sphere.ups_x] THEN CONV_TAC REAL_RAT_REDUCE_CONV);;
let ETA_Y_4_POINTS_INEQ = 
prove(`!y1 y2 y3. ineq[(&2, y1, &2 * h0); (&2, y2, &2 * h0); (&2, y3, &2 * h0)] (eta_y y1 y2 y3 pow 2 <= #2.2)`,
REWRITE_TAC[INEQ_ALT; ALL; Sphere.h0; REAL_ARITH `&2 * #1.26 = #2.52`] THEN REPEAT GEN_TAC THEN DISCH_TAC THEN REWRITE_TAC[Sphere.eta_y; Sphere.eta_x] THEN CONV_TAC (DEPTH_CONV let_CONV) THEN MAP_EVERY ABBREV_TAC [`x1 = y1 * y1:real`; `x2 = y2 * y2:real`; `x3 = y3 * y3:real`] THEN SUBGOAL_THEN `!y. &2 <= y /\ y <= #2.52 ==> #4.0 <= y * y /\ y * y <= #6.3504` ASSUME_TAC THENL [ GEN_TAC THEN REWRITE_TAC[REAL_ARITH `#4.0 = &2 * &2`; REAL_ARITH `#6.3504 = #2.52 * #2.52`] THEN REWRITE_TAC[GSYM REAL_POW_2] THEN REWRITE_TAC[GSYM REAL_LE_SQUARE_ABS] THEN REAL_ARITH_TAC; ALL_TAC ] THEN MAP_EVERY (fun tm -> FIRST_ASSUM (MP_TAC o SPEC tm)) [`y1:real`; `y2:real`; `y3:real`] THEN REMOVE_ASSUM THEN ASM_REWRITE_TAC[] THEN REPEAT DISCH_TAC THEN MP_TAC (SPEC_ALL eta_x_ineq_lemma) THEN ASM_REWRITE_TAC[INEQ_ALT; ALL] THEN DISCH_TAC THEN SUBGOAL_THEN `&0 < x1 * x2 * x3` ASSUME_TAC THENL [ ASSUME_TAC (REAL_ARITH `!x. #4.0 <= x ==> &0 < x`) THEN MATCH_MP_TAC REAL_LT_MUL THEN ASM_SIMP_TAC[] THEN MATCH_MP_TAC REAL_LT_MUL THEN ASM_SIMP_TAC[]; ALL_TAC ] THEN SUBGOAL_THEN `&0 < ups_x x1 x2 x3` ASSUME_TAC THENL [ MATCH_MP_TAC (REAL_ARITH `#2.2 * u - x1 * x2 * x3 >= &0 /\ &0 < x1 * x2 * x3 ==> &0 < u`) THEN ASM_REWRITE_TAC[]; ALL_TAC ] THEN SUBGOAL_THEN `&0 <= (x1 * x2 * x3) / ups_x x1 x2 x3` ASSUME_TAC THENL [ MATCH_MP_TAC REAL_LE_DIV THEN ASM_SIMP_TAC[REAL_LT_IMP_LE]; ALL_TAC ] THEN ASM_SIMP_TAC[SQRT_POW_2] THEN ONCE_REWRITE_TAC[REAL_ARITH `#2.2 = #2.2 / &1`] THEN ASSUME_TAC (REAL_ARITH `&0 < &1`) THEN ASM_SIMP_TAC[RAT_LEMMA4] THEN REPLICATE_TAC 4 REMOVE_ASSUM THEN POP_ASSUM MP_TAC THEN REAL_ARITH_TAC);;
(*************************************************************)
let DELTA_X4_MONO_LT_4 = 
prove(`!x1 x2 x3 a x5 x6 b. a < b /\ &0 < x1 ==> delta_x4 x1 x2 x3 b x5 x6 < delta_x4 x1 x2 x3 a x5 x6`,
REPEAT STRIP_TAC THEN REWRITE_TAC[Sphere.delta_x4] THEN REWRITE_TAC[REAL_ARITH `a - b + c + d - e + f < a - g + c + d - e + h <=> f - b < h - g`] THEN REWRITE_TAC[REAL_ARITH `x1*(--x1+x2+x3-b+x5+x6)-x1*b = --(&2*x1*b) + x1*(--x1+x2+x3+x5+x6)`] THEN REWRITE_TAC[REAL_ARITH `--a + b < --c + b <=> c < a`] THEN MATCH_MP_TAC REAL_LT_LMUL THEN REWRITE_TAC[REAL_ARITH `&0 < &2`] THEN MATCH_MP_TAC REAL_LT_LMUL THEN ASM_REWRITE_TAC[]);;
let DELTA_X4_MONO_LE_4 = 
prove(`!x1 x2 x3 a x5 x6 b. a < b /\ &0 <= x1 ==> delta_x4 x1 x2 x3 b x5 x6 <= delta_x4 x1 x2 x3 a x5 x6`,
REPEAT STRIP_TAC THEN MP_TAC (REAL_ARITH `&0 <= x1 ==> x1 = &0 \/ &0 < x1`) THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THENL [ ASM_REWRITE_TAC[Sphere.delta_x4] THEN REAL_ARITH_TAC; MATCH_MP_TAC REAL_LT_IMP_LE THEN ASM_SIMP_TAC[DELTA_X4_MONO_LT_4] ]);;
let REAL_LT_SQUARE_POS = 
prove(`!x y. &0 < x /\ x < y ==> x pow 2 < y pow 2`,
REPEAT STRIP_TAC THEN REWRITE_TAC[GSYM REAL_LT_SQUARE_ABS] THEN SUBGOAL_THEN `abs x = x` ASSUME_TAC THENL [ ASM_SIMP_TAC[REAL_ABS_REFL; REAL_LT_IMP_LE]; ALL_TAC ] THEN SUBGOAL_THEN `abs y = y` ASSUME_TAC THENL [ ASM_REWRITE_TAC[REAL_ABS_REFL] THEN MATCH_MP_TAC REAL_LT_IMP_LE THEN MATCH_MP_TAC REAL_LT_TRANS THEN EXISTS_TAC `x:real` THEN ASM_REWRITE_TAC[]; ALL_TAC ] THEN ASM_REWRITE_TAC[]);;
let ATN2_ACS_LEMMA = 
prove(`!a b. b * b < a ==> pi / &2 + atn2(sqrt(a - b*b), --b) = acs(b/sqrt(a))`,
REPEAT STRIP_TAC THEN SUBGOAL_THEN `&0 < a` ASSUME_TAC THENL [ MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC `b*b:real` THEN ASM_REWRITE_TAC[REAL_LE_SQUARE]; ALL_TAC ] THEN MP_TAC (REAL_ARITH `&0 < a ==> &0 <= a`) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN SUBGOAL_THEN `sqrt a pow 2 = a` ASSUME_TAC THENL [ ASM_REWRITE_TAC[SQRT_POW2]; ALL_TAC ] THEN SUBGOAL_THEN `atn2 (sqrt(a - b*b),--b) = --atn2(sqrt(a-b*b),b)` MP_TAC THENL [ MATCH_MP_TAC Trigonometry1.ATN2_RNEG THEN DISJ2_TAC THEN MATCH_MP_TAC SQRT_POS_LT THEN ASM_REWRITE_TAC[REAL_ARITH `&0 < a - b <=> b < a`]; ALL_TAC ] THEN DISCH_THEN (fun th -> REWRITE_TAC[th; REAL_ARITH `a + --b = a - b`]) THEN SUBGOAL_THEN `atn2(sqrt(a - b*b), b) = atn2(sqrt(&1 - (b/sqrt a) pow 2),b/sqrt a)` MP_TAC THENL [ MP_TAC (SPECL [`sqrt(&1 - (b/sqrt a) pow 2)`; `sqrt a`; `b/sqrt a`] (GEN_ALL Trigonometry2.POS_COMPATIBLE_WITH_ATN2)) THEN SUBGOAL_THEN `&0 < sqrt a` ASSUME_TAC THENL [ MATCH_MP_TAC SQRT_POS_LT THEN ASM_REWRITE_TAC[]; ALL_TAC ] THEN ASM_REWRITE_TAC[] THEN DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN ASM_SIMP_TAC[REAL_FIELD `&0 < a ==> a * b / a = b`] THEN SUBGOAL_THEN `a - b*b = (sqrt a) pow 2 * (&1 - (b/sqrt a) pow 2)` MP_TAC THENL [ ASM_REWRITE_TAC[REAL_POW_DIV] THEN ASM_SIMP_TAC[REAL_FIELD `&0 < a ==> a * (&1 - b/a) = a - b`] THEN REWRITE_TAC[REAL_POW_2]; ALL_TAC ] THEN DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN MP_TAC (SPECL [`sqrt a pow 2`; `&1 - (b/sqrt a) pow 2`] SQRT_MUL) THEN ANTS_TAC THENL [ ASM_REWRITE_TAC[REAL_POW_DIV] THEN REWRITE_TAC[REAL_ARITH `&0 <= &1 - b <=> b <= &1`] THEN MATCH_MP_TAC Trigonometry2.REAL_LE_LDIV THEN ASM_SIMP_TAC[REAL_POW_2; REAL_ARITH `b < a ==> b <= a`]; ALL_TAC ] THEN DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN ASM_REWRITE_TAC[]; ALL_TAC ] THEN DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN MATCH_MP_TAC (GSYM Trigonometry2.acs_atn2) THEN REWRITE_TAC[REAL_ARITH `-- &1 <= x /\ x <= &1 <=> abs x <= &1`] THEN ONCE_REWRITE_TAC[REAL_ARITH `&1 = abs(&1)`] THEN REWRITE_TAC[REAL_LE_SQUARE_ABS] THEN REWRITE_TAC[REAL_POW_DIV] THEN ASM_REWRITE_TAC[REAL_POW_2; REAL_ARITH `&1 * &1 = &1`] THEN MATCH_MP_TAC Trigonometry2.REAL_LE_LDIV THEN ASM_SIMP_TAC[REAL_ARITH `b < a ==> b <= a`]);;
let DELTA_X_AND_DELTA_X4 = 
prove(`!x1 x2 x3 x4 x5 x6. (let d4 = delta_x4 x1 x2 x3 x4 x5 x6 in let d = delta_x x1 x2 x3 x4 x5 x6 in let v1 = ups_x x1 x2 x6 in let v2 = ups_x x1 x3 x5 in &4 * x1 * d = v1 * v2 - d4 * d4)`,
REPEAT GEN_TAC THEN REPEAT (CONV_TAC let_CONV) THEN REWRITE_TAC[Sphere.delta_x4; Sphere.delta_x; Sphere.ups_x] THEN REAL_ARITH_TAC);;
let DELTA_EQ_DELTA_X = 
prove(`!x1 x2 x3 x4 x5 x6. delta x1 x2 x3 x6 x5 x4 = delta_x x1 x2 x3 x4 x5 x6`,
REPEAT GEN_TAC THEN REWRITE_TAC[Sphere.delta_x; Collect_geom.delta] THEN REAL_ARITH_TAC);;
let DIH_X_MONO_LT_4 = 
prove(`!x1 x2 x3 a x5 x6 b. a < b /\ &0 < x1 /\ &0 < delta_x x1 x2 x3 a x5 x6 /\ &0 < delta_x x1 x2 x3 b x5 x6 ==> dih_x x1 x2 x3 a x5 x6 < dih_x x1 x2 x3 b x5 x6`,
REPEAT STRIP_TAC THEN REWRITE_TAC[let_RULE Sphere.dih_x] THEN ABBREV_TAC `da = delta_x x1 x2 x3 a x5 x6` THEN ABBREV_TAC `db = delta_x x1 x2 x3 b x5 x6` THEN SUBGOAL_THEN `&0 < &4 * x1 * da /\ &0 < &4 * x1 * db` MP_TAC THENL [ CONJ_TAC THEN MATCH_MP_TAC REAL_LT_MUL THEN REWRITE_TAC[REAL_ARITH `&0 < &4`] THEN MATCH_MP_TAC REAL_LT_MUL THEN ASM_REWRITE_TAC[]; ALL_TAC ] THEN EXPAND_TAC "da" THEN EXPAND_TAC "db" THEN REWRITE_TAC[let_RULE DELTA_X_AND_DELTA_X4] THEN REWRITE_TAC[REAL_ARITH `&0 < a - b <=> b < a`] THEN ABBREV_TAC `d4a = delta_x4 x1 x2 x3 a x5 x6` THEN ABBREV_TAC `d4b = delta_x4 x1 x2 x3 b x5 x6` THEN ABBREV_TAC `v1 = ups_x x1 x2 x6` THEN ABBREV_TAC `v2 = ups_x x1 x3 x5` THEN STRIP_TAC THEN FIRST_ASSUM (MP_TAC o (fun th -> MATCH_MP ATN2_ACS_LEMMA th)) THEN POP_ASSUM MP_TAC THEN FIRST_ASSUM (MP_TAC o (fun th -> MATCH_MP ATN2_ACS_LEMMA th)) THEN DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN DISCH_TAC THEN DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN MATCH_MP_TAC ACS_MONO_LT THEN SUBGOAL_THEN `!a b. b * b < a ==> -- &1 <= b / sqrt(a) /\ b / sqrt a <= &1` ASSUME_TAC THENL [ REPEAT GEN_TAC THEN DISCH_TAC THEN REWRITE_TAC[REAL_ARITH `-- &1 <= x /\ x <= &1 <=> abs x <= &1`] THEN ONCE_REWRITE_TAC[REAL_ARITH `&1 = abs(&1)`] THEN REWRITE_TAC[REAL_LE_SQUARE_ABS] THEN REWRITE_TAC[REAL_POW_DIV] THEN SUBGOAL_THEN `&0 < a'` ASSUME_TAC THENL [ MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC `b' * b':real` THEN ASM_SIMP_TAC[REAL_LE_SQUARE; REAL_ARITH `b < a ==> b <= a`]; ALL_TAC ] THEN SUBGOAL_THEN `sqrt a' pow 2 = a'` (fun th -> REWRITE_TAC[th]) THENL [ REWRITE_TAC[SQRT_POW2] THEN ASM_SIMP_TAC[REAL_ARITH `&0 < a ==> &0 <= a`]; ALL_TAC ] THEN ASM_REWRITE_TAC[REAL_POW_2; REAL_ARITH `&1 * &1 = &1`] THEN MATCH_MP_TAC Trigonometry2.REAL_LE_LDIV THEN ASM_SIMP_TAC[REAL_ARITH `b < a ==> b <= a`]; ALL_TAC ] THEN POP_ASSUM (fun th -> ASM_SIMP_TAC[th]) THEN REWRITE_TAC[real_div] THEN MATCH_MP_TAC REAL_LT_RMUL THEN REWRITE_TAC[REAL_LT_INV_EQ] THEN CONJ_TAC THENL [ MP_TAC (SPEC_ALL DELTA_X4_MONO_LT_4) THEN ASM_REWRITE_TAC[]; MATCH_MP_TAC SQRT_POS_LT THEN MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC `d4a * d4a:real` THEN ASM_REWRITE_TAC[REAL_LE_SQUARE] ]);;
let DIH_Y_INEQ_concl = mk_imp ((hd (Ineq.getexact "2570626711")).ineq, `ineq [(#2.0,y1,#2.52); (#2.0,y2,#2.52); (#2.0,y3,#2.52); (#2.52,y4,#5.04); (#2.0,y5,#2.52); (#2.0,y6,#2.52)] (dih_y y1 y2 y3 y4 y5 y6 > #1.15 \/ delta_y y1 y2 y3 y4 y5 y6 <= &0)`);; g(DIH_Y_INEQ_concl);;
let DIH_Y_INEQ = prove(DIH_Y_INEQ_concl,
   REWRITE_TAC[Pack_defs.h0; REAL_ARITH `&2 * #1.26 = #2.52`] THEN
     REWRITE_TAC[INEQ_ALT; ALL] THEN
     REPEAT STRIP_TAC THEN
     DISJ_CASES_TAC (REAL_ARITH `delta_y y1 y2 y3 y4 y5 y6 <= &0 \/ delta_y y1 y2 y3 y4 y5 y6 > &0`) THENL
     [
       ASM_REWRITE_TAC[];
       ALL_TAC
     ] THEN
     DISJ1_TAC THEN
     REWRITE_TAC[real_gt] THEN
     MATCH_MP_TAC REAL_LTE_TRANS THEN
     EXISTS_TAC `dih_y y1 y2 y3 #2.52 y5 y6` THEN
     FIRST_X_ASSUM (MP_TAC o SPECL [`y1:real`; `y2:real`; `y3:real`; `#2.52`; `y5:real`; `y6:real`]) THEN
     ASM_SIMP_TAC[REAL_LE_REFL; real_gt] THEN
     DISCH_THEN (fun th -> ALL_TAC) THEN
     POP_ASSUM MP_TAC THEN

     REWRITE_TAC[let_RULE Sphere.dih_y; Sphere.delta_y] THEN
     MAP_EVERY ABBREV_TAC [`x1 = y1 * y1`; `x2 = y2 * y2`; `x3 = y3 * y3`; `x4 = y4 * y4`; `x5 = y5 * y5`; `x6 = y6 * y6`] THEN
     REWRITE_TAC[REAL_ARITH `a <= b <=> a < b \/ a = b`] THEN
     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
     REWRITE_TAC[real_gt] THEN
     DISCH_TAC THEN
     MATCH_MP_TAC DIH_X_MONO_LT_4 THEN
     POP_ASSUM (fun th -> REWRITE_TAC[th]) THEN

     SUBGOAL_THEN `!y. #2.0 <= y /\ y <= #2.52 ==> #4.0 <= y * y /\ y * y <= #6.3504` ASSUME_TAC THENL
     [
       GEN_TAC THEN REWRITE_TAC[REAL_ARITH `#4.0 = #2.0 * #2.0`; REAL_ARITH `#6.3504 = #2.52 * #2.52`] THEN
	 REWRITE_TAC[GSYM REAL_POW_2] THEN
	 REWRITE_TAC[GSYM REAL_LE_SQUARE_ABS] THEN
	 REAL_ARITH_TAC;
       ALL_TAC
     ] THEN

     SUBGOAL_THEN `#2.52 * #2.52 < x4` (fun th -> REWRITE_TAC[th]) THENL
     [
       EXPAND_TAC "x4" THEN
	 REWRITE_TAC[GSYM REAL_POW_2] THEN
	 MATCH_MP_TAC REAL_LT_SQUARE_POS THEN
	 ASM_REWRITE_TAC[REAL_ARITH `&0 < #2.52`; REAL_ARITH `a < b <=> a <= b /\ ~(a = b)`] THEN
	 REMOVE_ASSUM THEN POP_ASSUM MP_TAC THEN
	 REWRITE_TAC[CONTRAPOS_THM] THEN
	 EXPAND_TAC "x4" THEN
	 DISCH_THEN (fun th -> REWRITE_TAC[GSYM th]);
       ALL_TAC
     ] THEN

     MAP_EVERY (fun tm -> FIRST_ASSUM (MP_TAC o SPEC tm)) [`y1:real`; `y2:real`; `y3:real`; `y5:real`; `y6:real`] THEN
     REMOVE_ASSUM THEN REMOVE_ASSUM THEN
     REPLICATE_TAC 6 (POP_ASSUM (fun th -> REWRITE_TAC[th])) THEN
     ASM_REWRITE_TAC[] THEN
     REPEAT REMOVE_ASSUM THEN REPEAT DISCH_TAC THEN
     ASM_SIMP_TAC[REAL_ARITH `#4.0 <= x1 ==> &0 < x1`] THEN
     MATCH_MP_TAC REAL_LTE_TRANS THEN
     EXISTS_TAC `#128.0` THEN
     REWRITE_TAC[REAL_ARITH `&0 < #128.0`; GSYM real_ge] THEN

     MP_TAC delta_x_pos THEN
     REWRITE_TAC[INEQ_ALT; ALL] THEN
     DISCH_THEN MATCH_MP_TAC THEN
     ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);;
end;;