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);;
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`,