needs "tame/Inequalities.hl";;

module Delta_ineq = struct

open Tame_inequalities;;

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 <= &9 /\ #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 (&9) 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 <= &9 /\ #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 (&9) 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 <= &9 /\ #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 (&9)`,
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 apex darts *)
let delta_x_pos_apex = 
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,&9; #4.0,x5,&9; #4.0,x6,&9] (delta_x x1 x2 x3 x4 x5 x6 >= &1)`,
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`; `&9`] 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`; `&9`] 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`; `&9`] THEN ASM_SIMP_TAC[lemma6] THEN CONJ_TAC THEN (* Final stage *) REWRITE_TAC[Sphere.delta_x] THEN CONV_TAC REAL_RAT_REDUCE_CONV);;
let aux_lemma1 = 
prove(`!a. &2 <= a /\ a <= #2.52 ==> #4.0 <= a * a /\ a * a <= #6.3504`,
REWRITE_TAC[ARITH_RULE `#4.0 = &2 * &2 /\ #6.3504 = #2.52 * #2.52`] THEN REWRITE_TAC[GSYM REAL_POW_2; GSYM REAL_LE_SQUARE_ABS] THEN ARITH_TAC);;
let aux_lemma2 = 
prove(`!a. &2 <= a /\ a <= &3 ==> #4.0 <= a * a /\ a * a <= &9`,
REWRITE_TAC[ARITH_RULE `#4.0 = &2 * &2 /\ &9 = &3 * &3`] THEN REWRITE_TAC[GSYM REAL_POW_2; GSYM REAL_LE_SQUARE_ABS] THEN ARITH_TAC);;
let delta_y_pos_apex = 
prove(`!y1 y2 y3 y4 y5 y6. &2 <= y1 /\ y1 <= #2.52 /\ &2 <= y2 /\ y2 <= #2.52 /\ &2 <= y3 /\ y3 <= #2.52 /\ &2 <= y4 /\ y4 <= &3 /\ &2 <= y5 /\ y5 <= &3 /\ &2 <= y6 /\ y6 <= &3 ==> &0 <= delta_y y1 y2 y3 y4 y5 y6`,
REPEAT STRIP_TAC THEN REWRITE_TAC[Sphere.delta_y] THEN MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `&1` THEN REWRITE_TAC[ARITH_RULE `&0 <= &1`; GSYM real_ge] THEN MP_TAC delta_x_pos_apex THEN REWRITE_TAC[INEQ_ALT; ALL] THEN DISCH_THEN MATCH_MP_TAC THEN ASM_SIMP_TAC[aux_lemma1; aux_lemma2]);;
end;;