(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION *)
(* Section: Conclusions *)
(* Chapter: Local Fan *)
(* Lemma: OCBICBY *)
(* Author: Thomas C. Hales *)
(* Date: 2013-06-27 *)
(* ========================================================================== *)
module Ocbicby = struct
open Hales_tactic;;
let LET_THM = CONJ LET_DEF LET_END_DEF;;
let diff = Pent_hex.diff;;
let DERIVED_TAC = Pent_hex.DERIVED_TAC;;
(*
Functional_equation.functional_overload();;
*)
(* }}} *)
(* }}} *)
(* }}} *)
let euler_p_eulerA_x = prove_by_refinement(
`!(v0:real^A) v1 v2 v3.
(let x1 =
dist(v0,v1) pow 2 in
let x2 =
dist(v0,v2) pow 2 in
let x3 =
dist(v0,v3) pow 2 in
let x4 =
dist(v2,v3) pow 2 in
let x5 =
dist(v1,v3) pow 2 in
let x6 =
dist(v1,v2) pow 2 in
(
euler_p v0 v1 v2 v3 =
eulerA_x x1 x2 x3 x4 x5 x6))`,
(* {{{ proof *)
[
REWRITE_TAC[
LET_DEF;
LET_END_DEF;Sphere.euler_p;Sphere.eulerA_x;Sphere.ylist];
REPEAT WEAKER_STRIP_TAC;
REPEAT (GMATCH_SIMP_TAC
POW_2_SQRT);
REWRITE_TAC[
DIST_POS_LE];
MATCH_MP_TAC (arith `b = b' ==> a + b = a + b'`);
MATCH_MP_TAC (arith `a = a' /\ b = b' /\ c = c' ==> ra * a + rb * b + rc * c = ra * a' + rb * b' + rc * c'`);
REWRITE_TAC[Collect_geom2.DIST_POW2_DOT];
REWRITE_TAC[
DOT_LSUB;
DOT_RSUB];
REWRITE_TAC[
DOT_SYM];
BY(REAL_ARITH_TAC)
]);;
let COPLANAR_IMP_DIH_PI = prove_by_refinement(
`!(v0:real^3) v1 v2 v3. (let y1 =
dist(v0,v1) in
let y2 =
dist(v0,v2) in
let y3 =
dist(v0,v3) in
let y4 =
dist(v2,v3) in
let y5 =
dist(v1,v3) in
let y6 =
dist(v1,v2) in
(~collinear {v0, v1, v2} /\ ~collinear {v0, v1, v3} /\
coplanar {v0,v1,v2,v3} /\
y_of_x delta_x4 y1 y2 y3 y4 y5 y6 < &0 ==>
dihV v0 v1 v2 v3 =
pi))`,
(* {{{ proof *)
[
REWRITE_TAC[
LET_DEF;
LET_END_DEF];
REPEAT WEAKER_STRIP_TAC;
FIRST_X_ASSUM_ST `
coplanar` MP_TAC;
GMATCH_SIMP_TAC (GSYM
DIHV_EQ_0_PI_EQ_COPLANAR);
ASM_REWRITE_TAC[];
TYPIFY `(&0 <
dihV v0 v1 v2 v3 )` ENOUGH_TO_SHOW_TAC;
BY(REAL_ARITH_TAC);
INTRO_TAC Euler_complement.OJEKOJF2 [`v0`;`v1`;`v2`;`v3`];
REWRITE_TAC[
LET_DEF;
LET_END_DEF];
ASM_REWRITE_TAC[];
DISCH_THEN SUBST1_TAC;
FIRST_X_ASSUM MP_TAC;
REWRITE_TAC[Sphere.y_of_x;arith `x*x = x pow 2`];
TYPED_ABBREV_TAC `d4 =
delta_x4 (
dist (v0,v1) pow 2) (
dist (v0,v2) pow 2) (
dist (v0,v3) pow 2) (
dist (v2,v3) pow 2) (
dist (v1,v3) pow 2) (
dist (v1,v2) pow 2)` ;
DISCH_TAC;
TYPIFY `!x y. (y < &0 ==> atn2 (x,y) = --(
pi / &2) -
atn (x / y))` (C SUBGOAL_THEN ASSUME_TAC);
BY(MESON_TAC[Trigonometry1.ATN2_BREAKDOWN]);
FIRST_X_ASSUM (unlist ASM_SIMP_TAC);
MATCH_MP_TAC (arith `&0 <
pi /\ -- (
pi / &2) < a ==> &0 < pi/ &2 - ( -- (pi/ &2) - a)`);
REWRITE_TAC[
PI_POS];
BY(REWRITE_TAC[
ATN_BOUNDS])
]);;
let DIH_IMP_EULER_A_POS = prove_by_refinement(
`main_nonlinear_terminal_v11 ==> (!(v0:real^3) v1 v2 v3. (let y1 =
dist(v0,v1) in
let y2 =
dist(v0,v2) in
let y3 =
dist(v0,v3) in
let y4 =
dist(v2,v3) in
let y5 =
dist(v1,v3) in
let y6 =
dist(v1,v2) in
(~collinear {v0,v1,v2} /\ ~collinear {v0,v2,v3} /\ ~collinear{v0,v1,v3} /\
dihV v0 v1 v2 v3 +
dihV v0 v2 v3 v1 +
dihV v0 v3 v1 v2 < &2 *
pi /\
&2 <= y1 /\ y1 <= &2 * h0 /\
&2 <= y2 /\ y2 <= &2 * h0 /\
&2 <= y3 /\ y3 <= &2 * h0 /\
#3.01 <= y4 /\ y4 <= #3.915 /\
#3.01 <= y5 /\ y5 <= #3.915 /\
#3.01 <= y6 /\ y6 <= #3.915 ==>
y_of_x eulerA_x y1 y2 y3 y4 y5 y6 > &0)))`,
(* {{{ proof *)
[
REWRITE_TAC[
LET_DEF;
LET_END_DEF];
REPEAT WEAKER_STRIP_TAC;
TYPIFY `&0 <
delta_y (
dist(v0,v1)) (
dist(v0,v2)) (
dist(v0,v3)) (
dist(v2,v3)) (
dist(v1,v3)) (
dist(v1,v2))` ASM_CASES_TAC;
INTRO_TAC Euler_main_theorem.EULER_TRIANGLE [`v0`;`v1`;`v2`;`v3`];
REWRITE_TAC[
LET_DEF;
LET_END_DEF;Sphere.xlist;Sphere.ylist];
ANTS_TAC;
BY(ASM_REWRITE_TAC[arith `x pow 2 = x * x`;GSYM Sphere.delta_y]);
DISCH_TAC;
FIRST_X_ASSUM_ST `&2 *
pi` MP_TAC;
REWRITE_TAC[arith `dd < &2 *
pi <=> dd -
pi <
pi`];
ASM_REWRITE_TAC[arith `(a + b+c) -pi = a + b + c -
pi`];
ASM_REWRITE_TAC[arith `x pow 2 = x * x`;GSYM Sphere.delta_y;arith `
pi - u <
pi <=> &0 < u`];
REWRITE_TAC[ (REWRITE_RULE[
LET_DEF;
LET_END_DEF]
euler_p_eulerA_x)];
REWRITE_TAC[arith `x pow 2 = x * x`;GSYM Sphere.y_of_x];
TYPED_ABBREV_TAC `p =
y_of_x eulerA_x (
dist (v0,v1)) (
dist (v0,v2)) (
dist (v0,v3)) (
dist (v2,v3)) (
dist (v1,v3)) (
dist (v1,v2))` ;
REWRITE_TAC[arith `&0 < &2 * x <=> &0 < x`];
GMATCH_SIMP_TAC Merge_ineq.ATN2_POS;
CONJ_TAC;
GMATCH_SIMP_TAC
REAL_LT_RSQRT;
BY(ASM_TAC THEN REAL_ARITH_TAC);
BY(REAL_ARITH_TAC);
COMMENT "case delta=0";
let derived_form_delta_x_wrt_x4 = prove_by_refinement(
`!x1 x2 x3 x4 x5 x6.
derived_form T (\q.
delta_x x1 x2 x3 q x5 x6) (
delta_x4 x1 x2 x3 x4 x5 x6) (x4) (:real)`,
(* {{{ proof *)
[
REPEAT WEAKER_STRIP_TAC;
REWRITE_TAC[Sphere.delta_x4;Sphere.delta_x];
DERIVED_TAC (MP_TAC);
MATCH_MP_TAC (TAUT `(x <=> y) ==> (x ==> y)`);
REPEAT (AP_THM_TAC ORELSE AP_TERM_TAC);
BY(REAL_ARITH_TAC)
]);;
let derived_form_delta_x_wrt_x5 = prove_by_refinement(
`!x1 x2 x3 x4 x5 x6.
derived_form T (\q.
delta_x x1 x2 x3 x4 q x6) (
delta_x5 x1 x2 x3 x4 x5 x6) (x5) (:real)`,
(* {{{ proof *)
[
REPEAT WEAKER_STRIP_TAC;
REWRITE_TAC[Nonlin_def.delta_x5;Sphere.delta_x];
DERIVED_TAC (MP_TAC);
MATCH_MP_TAC (TAUT `(x <=> y) ==> (x ==> y)`);
REPEAT (AP_THM_TAC ORELSE AP_TERM_TAC);
BY(REAL_ARITH_TAC)
]);;
let derived_form_delta_x_wrt_x6 = prove_by_refinement(
`!x1 x2 x3 x4 x5 x6.
derived_form T (\q.
delta_x x1 x2 x3 x4 x5 q) (
delta_x6 x1 x2 x3 x4 x5 x6) (x6) (:real)`,
(* {{{ proof *)
[
REPEAT WEAKER_STRIP_TAC;
REWRITE_TAC[Nonlin_def.delta_x6;Sphere.delta_x];
DERIVED_TAC (MP_TAC);
MATCH_MP_TAC (TAUT `(x <=> y) ==> (x ==> y)`);
REPEAT (AP_THM_TAC ORELSE AP_TERM_TAC);
BY(REAL_ARITH_TAC)
]);;
let derived_form_delta_x4_wrt_x4 = prove_by_refinement(
`!x1 x2 x3 x4 x5 x6.
derived_form T (\q.
delta_x4 x1 x2 x3 q x5 x6) (-- &2 * x1) (x4) (:real)`,
(* {{{ proof *)
[
REPEAT WEAKER_STRIP_TAC;
REWRITE_TAC[Sphere.delta_x4];
DERIVED_TAC (MP_TAC);
MATCH_MP_TAC (TAUT `(x <=> y) ==> (x ==> y)`);
REPEAT (AP_THM_TAC ORELSE AP_TERM_TAC);
BY(REAL_ARITH_TAC)
]);;
let derived_form_delta_x4_wrt_x5 = prove_by_refinement(
`!x1 x2 x3 x4 x5 x6.
derived_form T (\q.
delta_x4 x1 x2 x3 x4 q x6) (x1 + x2 - x6) (x5) (:real)`,
(* {{{ proof *)
[
REPEAT WEAKER_STRIP_TAC;
REWRITE_TAC[Sphere.delta_x4];
DERIVED_TAC (MP_TAC);
MATCH_MP_TAC (TAUT `(x <=> y) ==> (x ==> y)`);
REPEAT (AP_THM_TAC ORELSE AP_TERM_TAC);
BY(REAL_ARITH_TAC)
]);;
let derived_form_delta_x4_wrt_x6 = prove_by_refinement(
`!x1 x2 x3 x4 x5 x6.
derived_form T (\q.
delta_x4 x1 x2 x3 x4 x5 q) (x1 + x3 - x5) (x6) (:real)`,
(* {{{ proof *)
[
REPEAT WEAKER_STRIP_TAC;
REWRITE_TAC[Sphere.delta_x4];
DERIVED_TAC (MP_TAC);
MATCH_MP_TAC (TAUT `(x <=> y) ==> (x ==> y)`);
REPEAT (AP_THM_TAC ORELSE AP_TERM_TAC);
BY(REAL_ARITH_TAC)
]);;
let derived_form_dih_x_wrt_x4 = prove_by_refinement(
`!x1 x2 x3 x4 x5 x6.
&0 < x1 /\
&0 <
delta_x x1 x2 x3 x4 x5 x6 /\
&0 <
ups_x x1 x2 x6 /\
&0 <
ups_x x1 x3 x5 ==>
derived_form T (\q.
dih_x x1 x2 x3 q x5 x6) (
sqrt x1 /
sqrt (
delta_x x1 x2 x3 x4 x5 x6)) (x4) (:real)`,
(* {{{ proof *)
[
REPEAT WEAKER_STRIP_TAC;
TYPED_ABBREV_TAC `w = (
sqrt x1 /
sqrt (
delta_x x1 x2 x3 x4 x5 x6))`;
REWRITE_TAC[Sphere.dih_x;LET_THM];
DERIVED_TAC (MP_TAC o GEN_ALL o (GENL [`x1:real`;`x2:real`;`x3:real`;`x4:real`;`x5:real`;`x6:real`]));
DISCH_THEN (C INTRO_TAC [`(-- &2 * x1)`;`(
delta_x4 x1 x2 x3 x4 x5 x6)`;`x1`;`x2`;`x3`;`x4`;`x5`;`x6`]);
TYPIFY `&0 < &4 * x1 *
delta_x x1 x2 x3 x4 x5 x6` (C SUBGOAL_THEN ASSUME_TAC);
GMATCH_SIMP_TAC
REAL_LT_MUL_EQ;
REWRITE_TAC[arith `&0 < &4`];
GMATCH_SIMP_TAC
REAL_LT_MUL_EQ;
BY(ASM_REWRITE_TAC[]);
TYPIFY `&0 <
sqrt(&4 * x1 *
delta_x x1 x2 x3 x4 x5 x6)` (C SUBGOAL_THEN ASSUME_TAC);
GMATCH_SIMP_TAC
REAL_LT_RSQRT;
BY(ASM_TAC THEN REAL_ARITH_TAC);
ONCE_REWRITE_TAC[
derived_form_b];
ANTS_TAC;
ASM_REWRITE_TAC[
derived_form_delta_x4_wrt_x4;
derived_form_delta_x_wrt_x4;
IN_UNIV;DE_MORGAN_THM];
BY(ASM_TAC THEN REAL_ARITH_TAC);
REWRITE_TAC[];
MATCH_MP_TAC (TAUT `(x <=> y) ==> (x ==> y)`);
REPEAT (AP_THM_TAC ORELSE AP_TERM_TAC);
TYPIFY `(
sqrt (&4 * x1 *
delta_x x1 x2 x3 x4 x5 x6) pow 2 + --delta_x4 x1 x2 x3 x4 x5 x6 pow 2) =
ups_x x1 x3 x5 *
ups_x x1 x2 x6 ` (C SUBGOAL_THEN ASSUME_TAC);
GMATCH_SIMP_TAC
SQRT_POW_2;
ASM_SIMP_TAC[arith `&0 < x ==> &0 <= x`];
REWRITE_TAC[arith `(-- x) pow 2 = x pow 2`;GSYM
ups_x_delta_x];
BY(REAL_ARITH_TAC);
ASM_REWRITE_TAC[];
TYPIFY `(((-- &2 * x1) * -- &1) *
sqrt (&4 * x1 *
delta_x x1 x2 x3 x4 x5 x6) - --delta_x4 x1 x2 x3 x4 x5 x6 * (&4 * x1 *
delta_x4 x1 x2 x3 x4 x5 x6) * inv (&2 *
sqrt (&4 * x1 *
delta_x x1 x2 x3 x4 x5 x6))) = (&2 * x1) * (
ups_x x1 x3 x5 *
ups_x x1 x2 x6) /
sqrt(&4 * x1 *
delta_x x1 x2 x3 x4 x5 x6)` (C SUBGOAL_THEN SUBST1_TAC);
FIRST_ASSUM ( SUBST1_TAC o GSYM);
Calc_derivative.CALC_ID_TAC;
BY(ASM_TAC THEN REAL_ARITH_TAC);
TYPIFY `((&2 * x1) * (
ups_x x1 x3 x5 *
ups_x x1 x2 x6) /
sqrt (&4 * x1 *
delta_x x1 x2 x3 x4 x5 x6)) / (
ups_x x1 x3 x5 *
ups_x x1 x2 x6) =
sqrt(x1) /
sqrt(
delta_x x1 x2 x3 x4 x5 x6)` (C SUBGOAL_THEN SUBST1_TAC);
Calc_derivative.CALC_ID_TAC;
TYPIFY `&0 <
sqrt(
delta_x x1 x2 x3 x4 x5 x6)` (C SUBGOAL_THEN ASSUME_TAC);
GMATCH_SIMP_TAC
REAL_LT_RSQRT;
BY(ASM_TAC THEN REAL_ARITH_TAC);
CONJ_TAC;
BY(ASM_TAC THEN REAL_ARITH_TAC);
TYPIFY `
sqrt(&4 * x1 *
delta_x x1 x2 x3 x4 x5 x6) = &2 *
sqrt(x1) *
sqrt(
delta_x x1 x2 x3 x4 x5 x6)` (C SUBGOAL_THEN SUBST1_TAC);
GMATCH_SIMP_TAC (GSYM
SQRT_MUL);
TYPIFY `&2 =
sqrt(&4)` (C SUBGOAL_THEN SUBST1_TAC);
MATCH_MP_TAC Upfzbzm_support_lemmas.SQRT_RULE_Euler_lemma;
BY(REAL_ARITH_TAC);
CONJ_TAC;
BY(ASM_TAC THEN REAL_ARITH_TAC);
GMATCH_SIMP_TAC (GSYM
SQRT_MUL);
REWRITE_TAC[arith `&0 <= &4`];
GMATCH_SIMP_TAC
REAL_LE_MUL;
BY(ASM_TAC THEN REAL_ARITH_TAC);
TYPIFY `
sqrt x1 *
sqrt x1 = x1` (C SUBGOAL_THEN MP_TAC);
GMATCH_SIMP_TAC (GSYM
SQRT_MUL);
GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx;
BY(ASM_TAC THEN REAL_ARITH_TAC);
TYPED_ABBREV_TAC `s =
sqrt(
delta_x x1 x2 x3 x4 x5 x6)` ;
REWRITE_TAC[arith `((&2 * sx * s) * u) * sx = &2 * (sx * sx) * s * u`];
DISCH_THEN SUBST1_TAC;
BY(REAL_ARITH_TAC);
EXPAND_TAC "w";
let derived_form_dih_x_wrt_x5 = prove_by_refinement(
`!x1 x2 x3 x4 x5 x6.
&0 < x1 /\
&0 <
delta_x x1 x2 x3 x4 x5 x6 /\
&0 <
ups_x x1 x2 x6 /\
&0 <
ups_x x1 x3 x5 ==>
derived_form T (\q.
dih_x x1 x2 x3 x4 q x6) (--sqrt x1 *
delta_x6 x1 x2 x3 x4 x5 x6 /
(
ups_x x1 x3 x5 *
sqrt (
delta_x x1 x2 x3 x4 x5 x6))) (x5) (:real)`,
(* {{{ proof *)
[
REPEAT WEAKER_STRIP_TAC;
TYPED_ABBREV_TAC `w = (--sqrt x1 *
delta_x6 x1 x2 x3 x4 x5 x6 / (
ups_x x1 x3 x5 *
sqrt (
delta_x x1 x2 x3 x4 x5 x6)))`;
REWRITE_TAC[Sphere.dih_x;LET_THM];
DERIVED_TAC (MP_TAC o GEN_ALL o (GENL [`x1:real`;`x2:real`;`x3:real`;`x4:real`;`x5:real`;`x6:real`]));
DISCH_THEN (C INTRO_TAC [`x1 + x2 - x6`;`(
delta_x5 x1 x2 x3 x4 x5 x6)`;`x1`;`x2`;`x3`;`x4`;`x5`;`x6`]);
TYPIFY `&0 < &4 * x1 *
delta_x x1 x2 x3 x4 x5 x6` (C SUBGOAL_THEN ASSUME_TAC);
GMATCH_SIMP_TAC
REAL_LT_MUL_EQ;
REWRITE_TAC[arith `&0 < &4`];
GMATCH_SIMP_TAC
REAL_LT_MUL_EQ;
BY(ASM_REWRITE_TAC[]);
TYPIFY `&0 <
sqrt(&4 * x1 *
delta_x x1 x2 x3 x4 x5 x6)` (C SUBGOAL_THEN ASSUME_TAC);
GMATCH_SIMP_TAC
REAL_LT_RSQRT;
BY(ASM_TAC THEN REAL_ARITH_TAC);
ONCE_REWRITE_TAC[
derived_form_b];
ANTS_TAC;
ASM_REWRITE_TAC[
derived_form_delta_x4_wrt_x5;
derived_form_delta_x_wrt_x5;
IN_UNIV;DE_MORGAN_THM];
BY(ASM_TAC THEN REAL_ARITH_TAC);
REWRITE_TAC[];
MATCH_MP_TAC (TAUT `(x <=> y) ==> (x ==> y)`);
REPEAT (AP_THM_TAC ORELSE AP_TERM_TAC);
TYPIFY `(
sqrt (&4 * x1 *
delta_x x1 x2 x3 x4 x5 x6) pow 2 + --delta_x4 x1 x2 x3 x4 x5 x6 pow 2) =
ups_x x1 x3 x5 *
ups_x x1 x2 x6 ` (C SUBGOAL_THEN ASSUME_TAC);
GMATCH_SIMP_TAC
SQRT_POW_2;
ASM_SIMP_TAC[arith `&0 < x ==> &0 <= x`];
REWRITE_TAC[arith `(-- x) pow 2 = x pow 2`;GSYM
ups_x_delta_x];
BY(REAL_ARITH_TAC);
ASM_REWRITE_TAC[];
TYPIFY `(((x1 + x2 - x6) * -- &1) *
sqrt (&4 * x1 *
delta_x x1 x2 x3 x4 x5 x6) - --delta_x4 x1 x2 x3 x4 x5 x6 * (&4 * x1 *
delta_x5 x1 x2 x3 x4 x5 x6) * inv (&2 *
sqrt (&4 * x1 *
delta_x x1 x2 x3 x4 x5 x6))) = (-- &4 * x1 *
ups_x x1 x2 x6 *
delta_x6 x1 x2 x3 x4 x5 x6) / (&2 *
sqrt(&4 * x1 *
delta_x x1 x2 x3 x4 x5 x6))` (C SUBGOAL_THEN SUBST1_TAC);
Calc_derivative.CALC_ID_TAC;
CONJ_TAC;
BY(ASM_TAC THEN REAL_ARITH_TAC);
REWRITE_TAC[arith `(xx * s) * &2 * s = (s * s) * xx * &2`];
GMATCH_SIMP_TAC (GSYM
SQRT_MUL);
ASM_SIMP_TAC[arith `&0 <x ==> &0 <= x`];
GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx;
ASM_SIMP_TAC[arith `&0 <x ==> &0 <= x`];
TYPED_ABBREV_TAC `sq =
sqrt (&4 * x1 *
delta_x x1 x2 x3 x4 x5 x6)`;
REWRITE_TAC[Sphere.delta_x;Nonlin_def.delta_x4;Nonlin_def.delta_x5;Nonlin_def.delta_x6;Sphere.ups_x];
BY(REAL_ARITH_TAC);
TYPIFY `(-- &4 * x1 *
ups_x x1 x2 x6 *
delta_x6 x1 x2 x3 x4 x5 x6) / (&2 *
sqrt (&4 * x1 *
delta_x x1 x2 x3 x4 x5 x6)) / (
ups_x x1 x3 x5 *
ups_x x1 x2 x6) = --
sqrt x1 *
delta_x6 x1 x2 x3 x4 x5 x6 / (
ups_x x1 x3 x5 *
sqrt(
delta_x x1 x2 x3 x4 x5 x6))` (C SUBGOAL_THEN SUBST1_TAC);
Calc_derivative.CALC_ID_TAC;
TYPIFY `&0 <
sqrt(
delta_x x1 x2 x3 x4 x5 x6)` (C SUBGOAL_THEN ASSUME_TAC);
GMATCH_SIMP_TAC
REAL_LT_RSQRT;
BY(ASM_TAC THEN REAL_ARITH_TAC);
CONJ_TAC;
BY(ASM_TAC THEN REAL_ARITH_TAC);
TYPIFY `
sqrt(&4 * x1 *
delta_x x1 x2 x3 x4 x5 x6) = &2 *
sqrt(x1) *
sqrt(
delta_x x1 x2 x3 x4 x5 x6)` (C SUBGOAL_THEN SUBST1_TAC);
GMATCH_SIMP_TAC (GSYM
SQRT_MUL);
TYPIFY `&2 =
sqrt(&4)` (C SUBGOAL_THEN SUBST1_TAC);
MATCH_MP_TAC Upfzbzm_support_lemmas.SQRT_RULE_Euler_lemma;
BY(REAL_ARITH_TAC);
CONJ_TAC;
BY(ASM_TAC THEN REAL_ARITH_TAC);
GMATCH_SIMP_TAC (GSYM
SQRT_MUL);
REWRITE_TAC[arith `&0 <= &4`];
GMATCH_SIMP_TAC
REAL_LE_MUL;
BY(ASM_TAC THEN REAL_ARITH_TAC);
TYPIFY `
sqrt x1 *
sqrt x1 = x1` (C SUBGOAL_THEN MP_TAC);
GMATCH_SIMP_TAC (GSYM
SQRT_MUL);
GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx;
BY(ASM_TAC THEN REAL_ARITH_TAC);
TYPED_ABBREV_TAC `s =
sqrt(
delta_x x1 x2 x3 x4 x5 x6)` ;
REWRITE_TAC[arith `((&2 * sx * s) * u) * sx = &2 * (sx * sx) * s * u`];
BY(CONV_TAC REAL_RING);
EXPAND_TAC "w";
let derived_form_dih_x_wrt_x6 = prove_by_refinement(
`!x1 x2 x3 x4 x5 x6.
&0 < x1 /\
&0 <
delta_x x1 x2 x3 x4 x5 x6 /\
&0 <
ups_x x1 x2 x6 /\
&0 <
ups_x x1 x3 x5 ==>
derived_form T (\q.
dih_x x1 x2 x3 x4 x5 q) (--sqrt x1 *
delta_x5 x1 x2 x3 x4 x5 x6 /
(
ups_x x1 x2 x6 *
sqrt (
delta_x x1 x2 x3 x4 x5 x6))) (x6) (:real)`,
(* {{{ proof *)
[
REPEAT WEAKER_STRIP_TAC;
TYPIFY_GOAL_THEN `!q.
dih_x x1 x2 x3 x4 x5 q =
dih_x x1 x3 x2 x4 q x5` (unlist REWRITE_TAC);
BY(REWRITE_TAC[Nonlinear_lemma.dih_x_sym]);
INTRO_TAC
derived_form_dih_x_wrt_x5 [`x1`;`x3`;`x2`;`x4`;`x6`;`x5`];
TYPIFY `
delta_x x1 x3 x2 x4 x6 x5 =
delta_x x1 x2 x3 x4 x5 x6` (C SUBGOAL_THEN SUBST1_TAC);
BY(ASM_TAC THEN MESON_TAC[Merge_ineq.delta_x_sym]);
ASM_REWRITE_TAC[];
MATCH_MP_TAC (TAUT `(x <=> y) ==> (x ==> y)`);
REPEAT (AP_THM_TAC ORELSE AP_TERM_TAC);
REWRITE_TAC[Nonlin_def.delta_x6;Nonlin_def.delta_x5];
BY(REAL_ARITH_TAC)
]);;
let derived_form_num1 = prove_by_refinement(
`!x4 x5 x6 e1 e2 e3.
derived_form T (\q. num1 e1 e2 e3 q x5 x6) (&4 * ((&16 - &2 * x4) * e1 + (x5 - &8) * e2 + (x6 - &8) * e3))
(x4) (:real)`,
(* {{{ proof *)
[
REPEAT WEAKER_STRIP_TAC;
REWRITE_TAC[Sphere.num1];
DERIVED_TAC MP_TAC;
MATCH_MP_TAC (TAUT `(x <=> y) ==> (x ==> y)`);
REPEAT (AP_THM_TAC ORELSE AP_TERM_TAC);
BY(REAL_ARITH_TAC)
]);;
let derived_form_sum_dih = prove_by_refinement(
`!x1 x2 x3 x4 x5 x6 e1 e2 e3.
&0 < x1 /\ &0 < x2 /\ &0 < x3 /\
&0 <
delta_x x1 x2 x3 x4 x5 x6 /\
&0 <
ups_x x1 x2 x6 /\
&0 <
ups_x x1 x3 x5 /\
&0 <
ups_x x2 x3 x4 ==>
derived_form T (\q. e1 *
dih_x x1 x2 x3 q x5 x6
+ e2 *
dih_x x2 x3 x1 x5 x6 q
+ e3 *
dih_x x3 x1 x2 x6 q x5) ((e1 *
sqrt x1 *
ups_x x2 x3 x4 -
e2 *
sqrt x2 *
delta_x6 x1 x2 x3 x4 x5 x6 -
e3 *
sqrt x3 *
delta_x5 x1 x2 x3 x4 x5 x6) /
(
ups_x x2 x3 x4 *
sqrt (
delta_x x1 x2 x3 x4 x5 x6))) (x4) (:real)`,
(* {{{ proof *)
[
REPEAT WEAKER_STRIP_TAC;
TYPED_ABBREV_TAC `w = (e1 *
sqrt x1 *
ups_x x2 x3 x4 - e2 *
sqrt x2 *
delta_x6 x1 x2 x3 x4 x5 x6 - e3 *
sqrt x3 *
delta_x5 x1 x2 x3 x4 x5 x6) / (
ups_x x2 x3 x4 *
sqrt (
delta_x x1 x2 x3 x4 x5 x6))`;
TYPIFY_GOAL_THEN `!q. e1 *
dih_x x1 x2 x3 q x5 x6 + e2 *
dih_x x2 x3 x1 x5 x6 q + e3 *
dih_x x3 x1 x2 x6 q x5 = e1 * (\q.
dih_x x1 x2 x3 q x5 x6) q + e2 * (\q.
dih_x x2 x3 x1 x5 x6 q) q + e3 * (\q.
dih_x x3 x1 x2 x6 q x5) q` (unlist PURE_REWRITE_TAC);
BY(REWRITE_TAC[]);
TYPED_ABBREV_TAC `f1 = (\q.
dih_x x1 x2 x3 q x5 x6)` ;
TYPED_ABBREV_TAC `f2 = (\q.
dih_x x2 x3 x1 x5 x6 q)` ;
TYPED_ABBREV_TAC `f3 = (\q.
dih_x x3 x1 x2 x6 q x5)` ;
DERIVED_TAC (MP_TAC o GEN_ALL o (GENL [`x1:real`;`x2:real`;`x3:real`;`x4:real`;`x5:real`;`x6:real`;`e1:real`;`e2:real`;`e3:real`]));
DISCH_THEN (C INTRO_TAC [`f1`;`f2`;`f3`]);
EXPAND_TAC "f1";
let derived_form_sum_dih444 = prove_by_refinement(
`!x4 x5 x6 e1 e2 e3.
&0 < x4 /\ x4 < &16 /\
&0 < x5 /\ x5 < &16 /\
&0 < x6 /\ x6 < &16 /\
&0 <
delta_x (&4) (&4) (&4) x4 x5 x6 ==>
derived_form T (\q. e1 *
dih_x (&4) (&4) (&4) q x5 x6
+ e2 *
dih_x (&4) (&4) (&4) x5 x6 q
+ e3 *
dih_x (&4) (&4) (&4) x6 q x5)
(( num1 e1 e2 e3 x4 x5 x6 ) / (&2 * x4 * (&16 - x4) *
sqrt(
delta_x (&4) (&4) (&4) x4 x5 x6))) (x4) (:real)`,
(* {{{ proof *)
[
REPEAT WEAKER_STRIP_TAC;
ONCE_REWRITE_TAC[arith `a / (&2 * b) = (a/ &2) / b`];
INTRO_TAC
derived_form_sum_dih [`&4`;`&4`;`&4`;`x4`;`x5`;`x6`;`e1`;`e2`;`e3`];
TYPIFY_GOAL_THEN `!x.
ups_x (&4) (&4) (x) = x * (&16 - x)` (unlist REWRITE_TAC);
ASM_REWRITE_TAC[Sphere.ups_x;arith `&0 < &4`];
TYPIFY_GOAL_THEN `!x6. -- &4 * &4 - &4 * &4 - x6 * x6 + &2 * &4 * x6 + &2 * &4 * &4 + &2 * &4 * x6 = x6 * (&16- x6)` (unlist REWRITE_TAC);
BY(REAL_ARITH_TAC);
ANTS_TAC;
REPEAT (GMATCH_SIMP_TAC
REAL_LT_MUL_EQ);
BY(ASM_TAC THEN REAL_ARITH_TAC);
MATCH_MP_TAC (TAUT `(x <=> y) ==> (x ==> y)`);
REWRITE_TAC[
REAL_MUL_AC;Collect_geom2.SQRT4_EQ2];
REPEAT (AP_THM_TAC ORELSE AP_TERM_TAC);
REWRITE_TAC[Sphere.num1;Nonlin_def.delta_x6;Nonlin_def.delta_x5];
BY(REAL_ARITH_TAC)
]);;
let derived_form_sum_dih444sub = prove_by_refinement(
`!x4 x5 x6 e1 e2 e3.
&0 < x4 /\ x4 < &16 /\
&0 < x5 /\ x5 < &16 /\
&0 < x6 /\ x6 < &16 /\
&0 <
delta_x (&4) (&4) (&4) x4 x5 x6 ==>
derived_form T (\q. e1 *
dih_x (&4) (&4) (&4) q x5 x6
+ e2 *
dih_x (&4) (&4) (&4) x5 x6 q
+ e3 *
dih_x (&4) (&4) (&4) x6 q x5 - (&1 + const1) *
pi)
(( num1 e1 e2 e3 x4 x5 x6 ) / (&2 * x4 * (&16 - x4) *
sqrt(
delta_x (&4) (&4) (&4) x4 x5 x6))) (x4) (:real)`,
(* {{{ proof *)
[
REPEAT WEAKER_STRIP_TAC;
TYPED_ABBREV_TAC `f' = (num1 e1 e2 e3 x4 x5 x6 / (&2 * x4 * (&16 - x4) *
sqrt (
delta_x (&4) (&4) (&4) x4 x5 x6)))`;
INTRO_TAC (GEN_ALL Calc_derivative.derived_form_sub) [`T`;`T`;`(\q. e1 *
dih_x (&4) (&4) (&4) q x5 x6 + e2 *
dih_x (&4) (&4) (&4) x5 x6 q + e3 *
dih_x (&4) (&4) (&4) x6 q x5)`;`\ (q:real). (&1 + const1)*pi`;`f'`;`&0`;`x4`;`(:real)`];
ASM_REWRITE_TAC[arith `f' - &0 = f'`;arith `(a + b) - c = a + b - c`];
DISCH_THEN MATCH_MP_TAC;
EXPAND_TAC "f'";
let derived_form_tau2D = prove_by_refinement(
`!x4 x5 x6 e1 e2 e3.
&0 < x4 /\ x4 < &16 /\
&0 < x5 /\ x5 < &16 /\
&0 < x6 /\ x6 < &16 /\
&0 <
delta_x (&4) (&4) (&4) x4 x5 x6 /\
num1 e1 e2 e3 x4 x5 x6 = &0 ==>
derived_form T
(\q. ( num1 e1 e2 e3 q x5 x6) / (&2 * q * (&16 - q) *
sqrt(
delta_x (&4) (&4) (&4) q x5 x6)))
((&4 * dnum1 e1 e2 e3 x4 x5 x6) /
(&2 * x4 * (&16 - x4) *
sqrt(
delta_x (&4) (&4) (&4) x4 x5 x6)))
(x4) (:real)`,
(* {{{ proof *)
[
REPEAT WEAKER_STRIP_TAC;
TYPIFY ` (\q. ( num1 e1 e2 e3 q x5 x6) / (&2 * q * (&16 - q) *
sqrt(
delta_x (&4) (&4) (&4) q x5 x6))) = (\q. (\q. num1 e1 e2 e3 q x5 x6) q / (\q. &2 * q * (&16 - q) *
sqrt(
delta_x (&4) (&4) (&4) q x5 x6)) q) ` (C SUBGOAL_THEN SUBST1_TAC);
BY(REWRITE_TAC[
FUN_EQ_THM]);
TYPED_ABBREV_TAC `(f:real->
real) = (\q. num1 e1 e2 e3 q x5 x6 )` ;
TYPED_ABBREV_TAC `(g:real->
real) = (\q. &2 * q * (&16 - q) *
sqrt (
delta_x (&4) (&4) (&4) q x5 x6))` ;
DERIVED_TAC (MP_TAC o GEN_ALL);
MP_TAC (diff `(\q. &2 * q * (&16 - q) *
sqrt (
delta_x (&4) (&4) (&4) q x5 x6))` [Sphere.delta_x] `x4:real` `(:real)`);
ASM_REWRITE_TAC[];
DISCH_TAC;
TYPED_ABBREV_TAC `(g':real) = (&2 * (x4 * ((&16 - x4) * (&4 * (x4 * -- &1 + -- &4 + &4 + &4 - x4 + x5 + x6) + &4 * x5 + &4 * x6 - &4 * &4 - x5 * x6) * inv (&2 *
sqrt (
delta_x (&4) (&4) (&4) x4 x5 x6)) + -- &1 *
sqrt (
delta_x (&4) (&4) (&4) x4 x5 x6)) + (&16 - x4) *
sqrt (
delta_x (&4) (&4) (&4) x4 x5 x6)))` ;
DISCH_THEN (C INTRO_TAC [`&4 * dnum1 e1 e2 e3 x4 x5 x6`;`f`;`g'`;`g`;`x4`]);
ASM_REWRITE_TAC[];
EXPAND_TAC "f";
let derived_form_taum_d3_exists = prove_by_refinement(
`!x4 x5 x6 e1 e2 e3. ?f'' f'''.
&0 < x4 /\ x4 < &16 /\
&0 < x5 /\ x5 < &16 /\
&0 < x6 /\ x6 < &16 /\
&0 <
delta_x (&4) (&4) (&4) x4 x5 x6 ==>
(!x4. &0 < x4 /\ x4 < &16 /\ &0 <
delta_x (&4) (&4) (&4) x4 x5 x6 ==>
derived_form T
(\q. ( num1 e1 e2 e3 q x5 x6 ) / (&2 * q * (&16 - q) *
sqrt(
delta_x (&4) (&4) (&4) q x5 x6))) (f'' x4) (x4) (:real)) /\
(
derived_form T f'' f''' x4 (:real))`,
(* {{{ proof *)
[
REPEAT WEAKER_STRIP_TAC;
TYPIFY `\q. (((&4 * dnum1 e1 e2 e3 q x5 x6) * &2 * q * (&16 - q) *
sqrt (
delta_x (&4) (&4) (&4) q x5 x6) - num1 e1 e2 e3 q x5 x6 * &2 * (q * ((&16 - q) *
delta_x4 (&4) (&4) (&4) q x5 x6 * inv (&2 *
sqrt (
delta_x (&4) (&4) (&4) q x5 x6)) + -- &1 *
sqrt (
delta_x (&4) (&4) (&4) q x5 x6)) + (&16 - q) *
sqrt (
delta_x (&4) (&4) (&4) q x5 x6))) / (&2 * q * (&16 - q) *
sqrt (
delta_x (&4) (&4) (&4) q x5 x6)) pow 2)` EXISTS_TAC;
TYPIFY `(((((&4 * ((&16 - &2 * x4) * e1 + (x5 - &8) * e2 + (x6 - &8) * e3)) * &2 * (x4 * ((&16 - x4) *
delta_x4 (&4) (&4) (&4) x4 x5 x6 * inv (&2 *
sqrt (
delta_x (&4) (&4) (&4) x4 x5 x6)) + -- &1 *
sqrt (
delta_x (&4) (&4) (&4) x4 x5 x6)) + (&16 - x4) *
sqrt (
delta_x (&4) (&4) (&4) x4 x5 x6)) + (&4 * -- &2 * e1) * &2 * x4 * (&16 - x4) *
sqrt (
delta_x (&4) (&4) (&4) x4 x5 x6)) - (num1 e1 e2 e3 x4 x5 x6 * &2 * ((x4 * (((&16 - x4) * (
delta_x4 (&4) (&4) (&4) x4 x5 x6 * (&2 *
delta_x4 (&4) (&4) (&4) x4 x5 x6 * inv (&2 *
sqrt (
delta_x (&4) (&4) (&4) x4 x5 x6))) * --inv ((&2 *
sqrt (
delta_x (&4) (&4) (&4) x4 x5 x6)) pow 2) + (-- &2 * &4) * inv (&2 *
sqrt (
delta_x (&4) (&4) (&4) x4 x5 x6))) + -- &1 *
delta_x4 (&4) (&4) (&4) x4 x5 x6 * inv (&2 *
sqrt (
delta_x (&4) (&4) (&4) x4 x5 x6))) + -- &1 *
delta_x4 (&4) (&4) (&4) x4 x5 x6 * inv (&2 *
sqrt (
delta_x (&4) (&4) (&4) x4 x5 x6))) + (&16 - x4) *
delta_x4 (&4) (&4) (&4) x4 x5 x6 * inv (&2 *
sqrt (
delta_x (&4) (&4) (&4) x4 x5 x6)) + -- &1 *
sqrt (
delta_x (&4) (&4) (&4) x4 x5 x6)) + (&16 - x4) *
delta_x4 (&4) (&4) (&4) x4 x5 x6 * inv (&2 *
sqrt (
delta_x (&4) (&4) (&4) x4 x5 x6)) + -- &1 *
sqrt (
delta_x (&4) (&4) (&4) x4 x5 x6)) + (&4 * dnum1 e1 e2 e3 x4 x5 x6) * &2 * (x4 * ((&16 - x4) *
delta_x4 (&4) (&4) (&4) x4 x5 x6 * inv (&2 *
sqrt (
delta_x (&4) (&4) (&4) x4 x5 x6)) + -- &1 *
sqrt (
delta_x (&4) (&4) (&4) x4 x5 x6)) + (&16 - x4) *
sqrt (
delta_x (&4) (&4) (&4) x4 x5 x6)))) * (&2 * x4 * (&16 - x4) *
sqrt (
delta_x (&4) (&4) (&4) x4 x5 x6)) pow 2 - ((&4 * ((&16 - &2 * x4) * e1 + (x5 - &8) * e2 + (x6 - &8) * e3)) * &2 * x4 * (&16 - x4) *
sqrt (
delta_x (&4) (&4) (&4) x4 x5 x6) - num1 e1 e2 e3 x4 x5 x6 * &2 * (x4 * ((&16 - x4) *
delta_x4 (&4) (&4) (&4) x4 x5 x6 * inv (&2 *
sqrt (
delta_x (&4) (&4) (&4) x4 x5 x6)) + -- &1 *
sqrt (
delta_x (&4) (&4) (&4) x4 x5 x6)) + (&16 - x4) *
sqrt (
delta_x (&4) (&4) (&4) x4 x5 x6))) * &2 * (&2 * x4 * (&16 - x4) *
sqrt (
delta_x (&4) (&4) (&4) x4 x5 x6)) pow 1 * &2 * (x4 * ((&16 - x4) *
delta_x4 (&4) (&4) (&4) x4 x5 x6 * inv (&2 *
sqrt (
delta_x (&4) (&4) (&4) x4 x5 x6)) + -- &1 *
sqrt (
delta_x (&4) (&4) (&4) x4 x5 x6)) + (&16 - x4) *
sqrt (
delta_x (&4) (&4) (&4) x4 x5 x6))) / (&2 * x4 * (&16 - x4) *
sqrt (
delta_x (&4) (&4) (&4) x4 x5 x6)) pow 4)` EXISTS_TAC;
REPEAT WEAKER_STRIP_TAC;
CONJ_TAC;
REPEAT WEAKER_STRIP_TAC;
REWRITE_TAC[];
DERIVED_TAC (MP_TAC o GEN_ALL);
DISCH_THEN (C INTRO_TAC [`(&4 * dnum1 e1 e2 e3 x4' x5 x6)`;`e1`;`e2`;`e3`;`
delta_x4 (&4) (&4) (&4) x4' x5 x6`;`x5`;`x6`;`x4'`]);
REWRITE_TAC[
derived_form_dnum1;
derived_form_delta_x_wrt_x4];
ONCE_REWRITE_TAC[
derived_form_b];
ANTS_TAC;
GMATCH_SIMP_TAC
SQRT_EQ_0;
BY(ASM_TAC THEN REAL_ARITH_TAC);
BY(REWRITE_TAC[]);
REWRITE_TAC[Nonlin_def.dnum1];
DERIVED_TAC (MP_TAC o GEN_ALL);
DISCH_THEN (C INTRO_TAC [`
delta_x4 (&4) (&4) (&4) x4 x5 x6`;`
delta_x4 (&4) (&4) (&4) x4 x5 x6`;`-- &2 * &4`;`
delta_x4 (&4) (&4) (&4) x4 x5 x6`;`
delta_x4 (&4) (&4) (&4) x4 x5 x6`;`(&4 * dnum1 e1 e2 e3 x4 x5 x6)`;`e1`;`e2`;`e3`;`
delta_x4 (&4) (&4) (&4) x4 x5 x6`;`x5`;`x6`;`x4`]);
REWRITE_TAC[
derived_form_dnum1;
derived_form_delta_x_wrt_x4;
derived_form_delta_x4_wrt_x4];
ONCE_REWRITE_TAC[
derived_form_b];
ANTS_TAC;
GMATCH_SIMP_TAC
SQRT_EQ_0;
BY(ASM_TAC THEN REAL_ARITH_TAC);
REWRITE_TAC[];
MATCH_MP_TAC (TAUT `(x <=> y) ==> (x ==> y)`);
REPEAT (AP_THM_TAC ORELSE AP_TERM_TAC);
BY(REWRITE_TAC[Nonlin_def.dnum1])
]);;
let delta_y_dim_reduction = prove_by_refinement(
`!y1 y2 y3 y4 y5 y6.
(let x6' = &8 * (&1 - (y1 * y1 + y2*y2 - y6*y6)/(&2* y1 * y2)) in
let x5' = &8 * (&1 - (y1*y1 + y3*y3 - y5*y5)/(&2 * y1 * y3)) in
let x4' = &8 * (&1 - (y2*y2 + y3*y3 - y4*y4)/(&2*y2*y3)) in
(~(y1 = &0) /\ ~(y2 = &0) /\ ~(y3 = &0) ==>
delta_x (&4) (&4) (&4) x4' x5' x6' = &64 *
delta_y y1 y2 y3 y4 y5 y6 / ((y1 * y2 * y3) pow 2)))
`,
(* {{{ proof *)
[
REWRITE_TAC[LET_THM];
REWRITE_TAC[Sphere.delta_x;Sphere.delta_y];
BY(CONV_TAC REAL_FIELD)
]);;
let delta_x_xrr = prove_by_refinement(
`!y1 y2 y3 y4 y5 y6.
(~(y1 = &0) /\ ~(y2 = &0) /\ ~(y3 = &0) ==>
delta_x (&4) (&4) (&4) (xrr y2 y3 y4) (xrr y1 y3 y5) (xrr y1 y2 y6) =
&64 *
delta_y y1 y2 y3 y4 y5 y6 / ((y1 *y2 * y3) pow 2))`,
(* {{{ proof *)
[
REWRITE_TAC[Appendix.xrr];
REPEAT WEAKER_STRIP_TAC;
BY(ASM_SIMP_TAC[GSYM (REWRITE_RULE[LET_THM]
delta_y_dim_reduction)])
]);;
let delta_x4_dim_reduction = prove_by_refinement(
`!y1 y2 y3 y4 y5 y6.
(let x6' = &8 * (&1 - (y1 * y1 + y2*y2 - y6*y6)/(&2* y1 * y2)) in
let x5' = &8 * (&1 - (y1*y1 + y3*y3 - y5*y5)/(&2 * y1 * y3)) in
let x4' = &8 * (&1 - (y2*y2 + y3*y3 - y4*y4)/(&2*y2*y3)) in
(~(y1 = &0) /\ ~(y2 = &0) /\ ~(y3 = &0) ==>
delta_x4 (&4) (&4) (&4) x4' x5' x6' = &16 *
y_of_x delta_x4 y1 y2 y3 y4 y5 y6 / (y1 * y1 * y2 * y3)))
`,
(* {{{ proof *)
[
REWRITE_TAC[LET_THM];
REWRITE_TAC[Sphere.delta_x4;Sphere.y_of_x];
BY(CONV_TAC REAL_FIELD)
]);;
let dih_x_dim_reduction = prove_by_refinement(
`!y1 y2 y3 y4 y5 y6.
(let x6' = &8 * (&1 - (y1 * y1 + y2*y2 - y6*y6)/(&2* y1 * y2)) in
let x5' = &8 * (&1 - (y1*y1 + y3*y3 - y5*y5)/(&2 * y1 * y3)) in
let x4' = &8 * (&1 - (y2*y2 + y3*y3 - y4*y4)/(&2*y2*y3)) in
((&0 < y1) /\ (&0 < y2) /\ (&0 < y3) /\ &0 <
delta_y y1 y2 y3 y4 y5 y6 ==>
dih_x (&4) (&4) (&4) x4' x5' x6' =
dih_y y1 y2 y3 y4 y5 y6))
`,
(* {{{ proof *)
[
REWRITE_TAC[Sphere.dih_x;Sphere.dih_y;LET_THM];
REPEAT WEAKER_STRIP_TAC;
TYPIFY `~(y1 = &0) /\ ~(y2 = &0) /\ ~(y3 = &0)` (C SUBGOAL_THEN ASSUME_TAC);
BY(ASM_TAC THEN REAL_ARITH_TAC);
ASM_SIMP_TAC[REWRITE_RULE[LET_THM]
delta_x4_dim_reduction;REWRITE_RULE[LET_THM]
delta_y_dim_reduction];
REWRITE_TAC[GSYM Sphere.y_of_x];
TYPIFY `
sqrt (&4 * &4 * &64 *
delta_y y1 y2 y3 y4 y5 y6 / (y1 * y2 * y3) pow 2) = &16 *
sqrt (&4 * (y1 * y1) *
y_of_x delta_x y1 y2 y3 y4 y5 y6) / (y1 * y1 * y2 * y3)` (C SUBGOAL_THEN SUBST1_TAC);
Calc_derivative.CALC_ID_TAC;
ASM_REWRITE_TAC[];
TYPIFY `&0 < y1 * y1 * y2 * y3` (C SUBGOAL_THEN ASSUME_TAC);
REPEAT (GMATCH_SIMP_TAC
REAL_LT_MUL);
BY(ASM_TAC THEN REAL_ARITH_TAC);
TYPIFY `y1 * y1 * y2 * y3 =
sqrt((y1 * y1 * y2 * y3) pow 2)` (C SUBGOAL_THEN SUBST1_TAC);
GMATCH_SIMP_TAC
POW_2_SQRT;
BY(ASM_SIMP_TAC[arith `&0 < x ==> &0 <= x`]);
GMATCH_SIMP_TAC (GSYM
SQRT_MUL);
REWRITE_TAC[
REAL_LE_POW_2];
GMATCH_SIMP_TAC (arith `&0 <= d/ y ==> &0 <= &4 * &4 * &64 * d / y`);
GMATCH_SIMP_TAC
REAL_LE_RDIV_EQ;
CONJ_TAC;
REPEAT (GMATCH_SIMP_TAC
REAL_LT_MUL);
REWRITE_TAC[GSYM Trigonometry2.NOT_ZERO_EQ_POW2_LT];
REWRITE_TAC[
REAL_ENTIRE];
BY(ASM_TAC THEN REAL_ARITH_TAC);
CONJ_TAC;
BY(ASM_TAC THEN REAL_ARITH_TAC);
TYPIFY `&16 *
sqrt (&4 * (y1 * y1) *
y_of_x delta_x y1 y2 y3 y4 y5 y6) =
sqrt (&16 pow 2 * &4 * (y1 * y1) *
y_of_x delta_x y1 y2 y3 y4 y5 y6)` (C SUBGOAL_THEN SUBST1_TAC);
TYPIFY `&16 =
sqrt(&16 pow 2)` (C SUBGOAL_THEN SUBST1_TAC);
REWRITE_TAC[
POW_2_SQRT_ABS];
BY(REAL_ARITH_TAC);
GMATCH_SIMP_TAC (GSYM
SQRT_MUL);
CONJ_TAC;
CONJ_TAC;
BY(REAL_ARITH_TAC);
GMATCH_SIMP_TAC (arith `&0 <= x ==> &0 <= &4 * x`);
GMATCH_SIMP_TAC
REAL_LE_MUL;
REWRITE_TAC[
REAL_LE_SQUARE];
REWRITE_TAC[Sphere.y_of_x;Sphere.delta_x;GSYM Sphere.delta_y];
BY(ASM_TAC THEN REAL_ARITH_TAC);
AP_TERM_TAC;
REWRITE_TAC[
POW_2_SQRT_ABS];
BY(REAL_ARITH_TAC);
REWRITE_TAC[arith `s - s' = &0 <=> s = s'`];
AP_TERM_TAC;
REWRITE_TAC[Sphere.y_of_x;Sphere.delta_x;GSYM Sphere.delta_y];
Calc_derivative.CALC_ID_TAC;
BY(ASM_REWRITE_TAC[]);
TYPED_ABBREV_TAC `dx =
y_of_x delta_x y1 y2 y3 y4 y5 y6` ;
TYPED_ABBREV_TAC `d4 =
y_of_x delta_x4 y1 y2 y3 y4 y5 y6 ` ;
TYPED_ABBREV_TAC `s =
sqrt(&4 * (y1 * y1) * dx)` ;
REWRITE_TAC[arith `&16 * s / y = (&16 / y) * s`];
REWRITE_TAC[arith `-- (a * d4) = a * -- d4`];
GMATCH_SIMP_TAC Trigonometry1.ATN2_LMUL_EQ;
GMATCH_SIMP_TAC
REAL_LT_DIV;
REPEAT (GMATCH_SIMP_TAC
REAL_LT_MUL);
BY(ASM_TAC THEN REAL_ARITH_TAC)
]);;
let derived_form_xrr = prove_by_refinement(
`!y1 y2 y6.
derived_form (&0 < y1 /\ &0 < y2)
(\q. xrr y1 y2 q) ((&8 * y6) / (y1 * y2)) y6 (:real)`,
(* {{{ proof *)
[
REPEAT WEAKER_STRIP_TAC;
ASM_CASES_TAC `~(&0 < y1 /\ &0 < y2)`;
BY(ASM_REWRITE_TAC[Pent_hex.derived_form_F]);
RULE_ASSUM_TAC (REWRITE_RULE[]);
ASM_REWRITE_TAC[Appendix.xrr];
DERIVED_TAC MP_TAC;
TYPIFY `~(y1 = &0) /\ ~(y2 = &0) /\ ~(&2 = &0)` (C SUBGOAL_THEN ASSUME_TAC);
BY(ASM_TAC THEN REAL_ARITH_TAC);
ASM_REWRITE_TAC[];
MATCH_MP_TAC (TAUT `(x <=> y) ==> (x ==> y)`);
REPEAT (AP_THM_TAC ORELSE AP_TERM_TAC);
Calc_derivative.CALC_ID_TAC;
BY(ASM_REWRITE_TAC[])
]);;
let derived_form_xrr_wrt_y1 = prove_by_refinement(
`!y1 y2 y6.
derived_form (&0 < y1 /\ &0 < y2)
(\q. xrr q y2 y6) ( -- &4 * ((y1*y1 + y6*y6 - y2*y2)/ (y1 pow 2 * y2))) y1 (:real)`,
(* {{{ proof *)
[
REPEAT WEAKER_STRIP_TAC;
ASM_CASES_TAC `~(&0 < y1 /\ &0 < y2)`;
BY(ASM_REWRITE_TAC[Pent_hex.derived_form_F]);
RULE_ASSUM_TAC (REWRITE_RULE[]);
ASM_REWRITE_TAC[Appendix.xrr];
DERIVED_TAC MP_TAC;
TYPIFY `~(y1 = &0) /\ ~(y2 = &0) /\ ~(&2 = &0)` (C SUBGOAL_THEN ASSUME_TAC);
BY(ASM_TAC THEN REAL_ARITH_TAC);
ASM_REWRITE_TAC[];
MATCH_MP_TAC (TAUT `(x <=> y) ==> (x ==> y)`);
REPEAT (AP_THM_TAC ORELSE AP_TERM_TAC);
Calc_derivative.CALC_ID_TAC;
(ASM_REWRITE_TAC[])
]);;
let derived_form_xrr_D2 = prove_by_refinement(
`!y1 y2 y6.
derived_form (&0 < y1 /\ &0 < y2)
(\q. (&8* q) / (y1 *y2)) (&8 / (y1 * y2)) y6 (:real)`,
(* {{{ proof *)
[
REPEAT WEAKER_STRIP_TAC;
ASM_CASES_TAC `~(&0 < y1 /\ &0 < y2)`;
BY(ASM_REWRITE_TAC[Pent_hex.derived_form_F]);
RULE_ASSUM_TAC (REWRITE_RULE[]);
ASM_REWRITE_TAC[];
DERIVED_TAC MP_TAC;
ONCE_REWRITE_TAC[
derived_form_b];
ANTS_TAC;
BY(ASM_TAC THEN REAL_ARITH_TAC);
ASM_REWRITE_TAC[];
MATCH_MP_TAC (TAUT `(x <=> y) ==> (x ==> y)`);
REPEAT (AP_THM_TAC ORELSE AP_TERM_TAC);
Calc_derivative.CALC_ID_TAC;
BY(ASM_TAC THEN REAL_ARITH_TAC)
]);;
let derived_form_xrr_D3 = prove_by_refinement(
`!y1 y2 y6.
derived_form (&0 < y1 /\ &0 < y2)
(\q. (&8) / (y1 *y2)) (&0) y6 (:real)`,
(* {{{ proof *)
[
REPEAT WEAKER_STRIP_TAC;
ASM_CASES_TAC `~(&0 < y1 /\ &0 < y2)`;
BY(ASM_REWRITE_TAC[Pent_hex.derived_form_F]);
RULE_ASSUM_TAC (REWRITE_RULE[]);
ASM_REWRITE_TAC[];
DERIVED_TAC MP_TAC;
BY(REWRITE_TAC[])
]);;
let derived_form_chain = prove_by_refinement(
`!f f' g g' x y.
f x = y /\
derived_form T f f' x (:real) /\
derived_form T g g' y (:real) ==>
derived_form T (g o f) (g' * f') x (:real)
`,
(* {{{ proof *)
[
REPEAT GEN_TAC;
TYPIFY `g o f = \q. g(f(q))` (C SUBGOAL_THEN SUBST1_TAC);
BY(REWRITE_TAC[
FUN_EQ_THM;
o_THM]);
REPEAT WEAKER_STRIP_TAC;
MP_TAC (GEN_ALL (Calc_derivative.differentiate `(\(q:real). (g:real->
real) (f q))` `x:real` `(:real)`));
DISCH_THEN (C INTRO_TAC [`g`;`f`;`f'`;`g'`;`x`]);
ASM_REWRITE_TAC[];
BY(REWRITE_TAC[
REAL_MUL_AC])
]);;
let derived_form_chain_old = prove_by_refinement(
`!f f' g g' h' x y.
f x = y /\
derived_form T f f' x (:real) /\
derived_form T g g' y (:real) /\
derived_form T (g o f) h' x (:real) ==>
h' = g' * f'
`,
(* {{{ proof *)
[
REPEAT GEN_TAC;
TYPIFY `g o f = \q. g(f(q))` (C SUBGOAL_THEN SUBST1_TAC);
BY(REWRITE_TAC[
FUN_EQ_THM;
o_THM]);
REPEAT WEAKER_STRIP_TAC;
MP_TAC (GEN_ALL (Calc_derivative.differentiate `(\(q:real). (g:real->
real) (f q))` `x:real` `(:real)`));
DISCH_THEN (C INTRO_TAC [`g`;`f`;`f'`;`g'`;`x`]);
ASM_REWRITE_TAC[];
DISCH_TAC;
TYPIFY `h' = f' * g'` (C SUBGOAL_THEN SUBST1_TAC);
INTRO_TAC
derived_form_unique [`(\q. g (f q))`;`h'`;`f'*g'`;`x`];
DISCH_THEN MATCH_MP_TAC;
BY(ASM_REWRITE_TAC[]);
BY(REAL_ARITH_TAC)
]);;
let taum_compose_xrr = prove_by_refinement(
`!y1 y2 y3 y4 y5 y6.
(let e1 = rho y1 in
let e2 = rho y2 in
let e3 = rho y3 in
let x5 = xrr y1 y3 y5 in
let x6 = xrr y1 y2 y6 in
( &0 < y1 /\ &0 < y2 /\ &0 < y3 /\ &0 <
delta_y y1 y2 y3 y4 y5 y6 ==>
(\q. taum y1 y2 y3 q y5 y6) y4 =
((\q. e1 *
dih_x (&4) (&4) (&4) q x5 x6
+ e2 *
dih_x (&4) (&4) (&4) x5 x6 q
+ e3 *
dih_x (&4) (&4) (&4) x6 q x5 - (&1 + const1) *
pi) o
(\q. xrr y2 y3 q)) y4))`,
(* {{{ proof *)
[
REWRITE_TAC[
LET_DEF;
LET_END_DEF];
REWRITE_TAC[
o_THM;Nonlinear_lemma.taum_123];
REWRITE_TAC[Sphere.rhazim;Sphere.rhazim2;Sphere.rhazim3;Sphere.node2_y;Sphere.node3_y];
REPEAT WEAKER_STRIP_TAC;
TYPIFY `
dih_x (&4) (&4) (&4) (xrr y1 y3 y5) (xrr y1 y2 y6) (xrr y2 y3 y4) =
dih_x (&4) (&4) (&4) (xrr y1 y3 y5) (xrr y2 y3 y4) (xrr y2 y1 y6)` (C SUBGOAL_THEN SUBST1_TAC);
BY(MESON_TAC[
xrr_sym;Nonlinear_lemma.dih_x_sym]);
TYPIFY `
dih_x (&4) (&4) (&4) (xrr y1 y2 y6) (xrr y2 y3 y4) (xrr y1 y3 y5) =
dih_x (&4) (&4) (&4) (xrr y1 y2 y6) (xrr y3 y2 y4) (xrr y3 y1 y5)` (C SUBGOAL_THEN SUBST1_TAC);
BY(MESON_TAC[
xrr_sym]);
REWRITE_TAC[Appendix.xrr];
REPEAT (GMATCH_SIMP_TAC (REWRITE_RULE[LET_THM]
dih_x_dim_reduction));
ASM_REWRITE_TAC[];
REWRITE_TAC[Nonlinear_lemma.dih_y_sym];
FIRST_X_ASSUM MP_TAC;
BY(REWRITE_TAC[Merge_ineq.delta_y_sym;])
]);;
let xrr_factor = prove_by_refinement(
`!y1 y2 y6.
&0 < y1 /\ &0 < y2 ==> (xrr y1 y2 y6 = &4 * ((y6 + y2 - y1) * (y6 - y2 + y1))/(y1 * y2))`,
(* {{{ proof *)
[
REPEAT WEAKER_STRIP_TAC;
REWRITE_TAC[Appendix.xrr];
Calc_derivative.CALC_ID_TAC;
BY(ASM_TAC THEN REAL_ARITH_TAC)
]);;
let xrr_factor_8 = prove_by_refinement(
`!y1 y2 y6.
&0 < y1 /\ &0 < y2 ==> (&16 - xrr y1 y2 y6 = &4* ((y6 + y2 + y1) * ( y2 + y1- y6))/(y1 * y2))`,
(* {{{ proof *)
[
REPEAT WEAKER_STRIP_TAC;
REWRITE_TAC[Appendix.xrr];
Calc_derivative.CALC_ID_TAC;
BY(ASM_TAC THEN REAL_ARITH_TAC)
]);;
let xrr_pos = prove_by_refinement(
`!y1 y2 y6.
&0 < y1 /\ &0 < y2 /\ y1 < y2 + y6 /\ y2 < y1 + y6 ==> &0 < xrr y1 y2 y6`,
(* {{{ proof *)
[
REPEAT WEAKER_STRIP_TAC;
REWRITE_TAC[Appendix.xrr];
MATCH_MP_TAC (arith `&0 < x ==> &0 < &8 * x`);
TYPIFY `&1 - (y1 * y1 + y2 * y2 - y6 * y6) / (&2 * y1 * y2) = ((y6 + y2 - y1) * (y6 - y2 + y1))/(&2 * y1 * y2)` (C SUBGOAL_THEN SUBST1_TAC);
Calc_derivative.CALC_ID_TAC;
BY(ASM_TAC THEN REAL_ARITH_TAC);
GMATCH_SIMP_TAC
REAL_LT_RDIV_EQ;
REWRITE_TAC[arith `&0 * x = &0`];
GMATCH_SIMP_TAC
REAL_LT_MUL_EQ;
REPEAT (GMATCH_SIMP_TAC
REAL_LT_MUL_EQ);
BY(ASM_TAC THEN REAL_ARITH_TAC)
]);;
let xrr_lt_16 = prove_by_refinement(
`!y1 y2 y6. &0 < y1 /\ &0 < y2 /\ y6 < y1 + y2 /\ &0 < y6 ==> xrr y1 y2 y6 < &16`,
(* {{{ proof *)
[
REPEAT WEAKER_STRIP_TAC;
REWRITE_TAC[Appendix.xrr];
MATCH_MP_TAC (arith `&0 < &1 + u ==> &8 * (&1 - u) < &16`);
TYPIFY `&1 + (y1 * y1 + y2 * y2 - y6 * y6) / (&2 * y1 * y2) = ((y6 + y2 + y1) * ( y2 + y1- y6))/(&2 * y1 * y2)` (C SUBGOAL_THEN SUBST1_TAC);
Calc_derivative.CALC_ID_TAC;
BY(ASM_TAC THEN REAL_ARITH_TAC);
GMATCH_SIMP_TAC
REAL_LT_RDIV_EQ;
REWRITE_TAC[arith `&0 * x = &0`];
REPEAT (GMATCH_SIMP_TAC
REAL_LT_MUL_EQ);
BY(ASM_TAC THEN REAL_ARITH_TAC)
]);;
let ups_x_triangle_ineq = prove_by_refinement(
`!y1 y2 y6. &0 < y1 /\ &0 < y2 /\ &0 < y6 ==> (&0 <
ups_x (y1*y1) (y2*y2) (y6*y6) <=>
(y1 < y2 + y6 /\ y2 < y1 + y6 /\ y6 < y1 + y2))`,
(* {{{ proof *)
[
REPEAT WEAKER_STRIP_TAC;
TYPIFY `
ups_x (y1*y1) (y2*y2) (y6*y6) = (y1 - y2 + y6) * (y1 + y2 - y6) * (-- y1 + y2 + y6) * (y1 + y2 + y6) ` (C SUBGOAL_THEN SUBST1_TAC);
REWRITE_TAC[Sphere.ups_x];
BY(REAL_ARITH_TAC);
REPEAT WEAKER_STRIP_TAC;
REWRITE_TAC[
REAL_MUL_POS_LT;arith `x * y < &0 <=> &0 < (--x ) * y`];
ASM_CASES_TAC `y2 < y1 + y6`;
BY(ASM_TAC THEN REAL_ARITH_TAC);
BY(ASM_TAC THEN REAL_ARITH_TAC)
]);;
let xrr_bounds = prove_by_refinement(
`!y1 y2 y6. &0 < y1 /\ &0 < y2 /\ &0 < y6 /\ &0 <
ups_x (y1*y1) (y2*y2) (y6*y6) ==>
(&0 < xrr y1 y2 y6 /\ xrr y1 y2 y6 < &16)`,
(* {{{ proof *)
[
REPEAT WEAKER_STRIP_TAC;
INTRO_TAC
ups_x_triangle_ineq [`y1`;`y2`;`y6`];
ANTS_TAC;
BY(ASM_REWRITE_TAC[]);
DISCH_THEN (RULE_ASSUM_TAC o (unlist REWRITE_RULE));
CONJ_TAC;
MATCH_MP_TAC
xrr_pos;
BY(ASM_REWRITE_TAC[]);
MATCH_MP_TAC
xrr_lt_16;
BY(ASM_REWRITE_TAC[])
]);;
let xrr_bounds_2 = prove_by_refinement(
`!y1 y2 y6. &0 < y1 /\ &0 < y2 /\ &0 < y6 ==> (&0 <
ups_x (y1*y1) (y2*y2) (y6*y6) <=>
&0 < xrr y1 y2 y6 /\ xrr y1 y2 y6 < &16)`,
(* {{{ proof *)
[
REPEAT WEAKER_STRIP_TAC;
REWRITE_TAC[ (TAUT `(a <=>b) <=> ((a ==> b) /\ (b ==> a) )`)];
CONJ_TAC;
BY(ASM_MESON_TAC[
xrr_bounds]);
ASM_SIMP_TAC[
ups_x_triangle_ineq];
ONCE_REWRITE_TAC[arith `x < &16 <=> &0 < &16- x`];
ASM_SIMP_TAC[
xrr_factor_8];
ASM_SIMP_TAC[
xrr_factor];
ONCE_REWRITE_TAC[arith `&0 < &4 * x <=> &0 < x`];
REPEAT (GMATCH_SIMP_TAC Trigonometry2.REAL_LT_DIV_0);
TYPIFY_GOAL_THEN `&0 < y1 * y2` (unlist REWRITE_TAC);
GMATCH_SIMP_TAC
REAL_LT_MUL_EQ;
BY(ASM_REWRITE_TAC[]);
REWRITE_TAC[
REAL_MUL_POS_LT];
BY(ASM_TAC THEN REAL_ARITH_TAC)
]);;
let xrr_le_16 = prove_by_refinement(
`!y1 y2 y6. &0 < y1 /\ &0 < y2 /\ &0 < y6 /\ &0 <
ups_x (y1*y1) (y2*y2) (y6*y6) ==>
xrr y1 y2 y6 <= &16`,
(* {{{ proof *)
[
REPEAT WEAKER_STRIP_TAC;
MATCH_MP_TAC (arith `x < y ==> x <= y`);
BY(ASM_MESON_TAC[
xrr_bounds_2])
]);;
let arclength_xrr = prove_by_refinement(
`!y1 y2 y6. &0 < y1 /\ &0 < y2 /\ &0 < y6 /\ &0 <
ups_x (y1*y1) (y2*y2) (y6*y6) ==>
arclength y1 y2 y6 =
acs(&1 - xrr y1 y2 y6 / &8)`,
(* {{{ proof *)
[
REPEAT WEAKER_STRIP_TAC;
INTRO_TAC
ups_x_triangle_ineq [`y1`;`y2`;`y6`];
ANTS_TAC;
BY(ASM_REWRITE_TAC[]);
DISCH_THEN (RULE_ASSUM_TAC o (unlist REWRITE_RULE));
REWRITE_TAC[Appendix.xrr];
GMATCH_SIMP_TAC Trigonometry.PQQDENV;
ASM_SIMP_TAC[arith `a < b ==> a <= b`];
CONJ_TAC;
BY(ASM_TAC THEN REAL_ARITH_TAC);
AP_TERM_TAC;
Calc_derivative.CALC_ID_TAC;
BY(ASM_TAC THEN REAL_ARITH_TAC)
]);;
let TBRMXRZ2 = prove_by_refinement(
`!P Q f f' f'' g g' g'' h' h'' x y.
(P x) /\ (Q (f x)) /\ (y = f x) /\ &0 < f' x /\ h' x = &0 /\
real_open {x | P x /\ Q (f x) } /\
(!x.
derived_form (P x) f (f' x) x (:real)) /\
(!y.
derived_form (Q( y)) g (g' y) y (:real)) /\
(!x.
derived_form (P x /\ Q (f x)) (g o f) (h' x) x (:real)) /\
derived_form T f' f'' x (:real) /\
derived_form T g' g'' y (:real) /\
derived_form T h' h'' x (:real) ==>
re_eqvl h'' g''`,
(* {{{ proof *)
[
REPEAT WEAKER_STRIP_TAC;
TYPIFY `!x. P x /\ Q (f x) ==> h' x = g' (f x) * f' x` (C SUBGOAL_THEN ASSUME_TAC);
REPEAT WEAKER_STRIP_TAC;
INTRO_TAC
derived_form_chain_old [`f`;`f' x'`;`g`;`g' (f x')`;`h' x'`;`x'`;`f x'`];
DISCH_THEN MATCH_MP_TAC;
ASM_REWRITE_TAC[];
RULE_ASSUM_TAC(ONCE_REWRITE_RULE[
derived_form_b]);
BY(ASM_SIMP_TAC[]);
TYPIFY `
derived_form T (\q. g' (f q) * f' q) h'' x (:real)` (C SUBGOAL_THEN ASSUME_TAC);
REWRITE_TAC[Calc_derivative.derived_form;
WITHINREAL_UNIV];
MATCH_MP_TAC Arc_properties.HAS_REAL_DERIVATIVE_LOCAL;
TYPIFY `h'` EXISTS_TAC;
CONJ_TAC;
FIRST_X_ASSUM_ST `
derived_form` MP_TAC;
BY(REWRITE_TAC[Calc_derivative.derived_form;
WITHINREAL_UNIV]);
TYPIFY `{ x | P x /\ Q (f x)}` EXISTS_TAC;
ASM_REWRITE_TAC[
IN_ELIM_THM];
BY(FIRST_X_ASSUM MP_TAC THEN MESON_TAC[]);
MP_TAC (GEN_ALL (Calc_derivative.differentiate `(\(q:real). (g':real->
real) (f q) * f' q)` `x:real` `(:real)`));
DISCH_THEN (C INTRO_TAC [`g'`;`f`;`f''`;`f' x`;`g''`;`f'`;`x`]);
ASM_REWRITE_TAC[];
TYPIFY_GOAL_THEN `(
derived_form T g' g'' (f x) (:real) /\
derived_form T f (f' x) x (:real))` (unlist REWRITE_TAC);
CONJ_TAC;
BY(ASM_MESON_TAC[]);
RULE_ASSUM_TAC (ONCE_REWRITE_RULE[
derived_form_b]);
FIRST_X_ASSUM MATCH_MP_TAC;
BY(ASM_REWRITE_TAC[]);
DISCH_TAC;
INTRO_TAC
derived_form_unique [`(\q. g' (f q) * f' q)`;`h''`;`(g' (f x) * f'' + (f' x * g'') * f' x)`;`x`];
ASM_REWRITE_TAC[];
DISCH_THEN SUBST1_TAC;
INTRO_TAC
TBRMXRZ1 [`f`;`f' x`;`g`;`g' y`;`h' x`;`x`;`y`];
ANTS_TAC;
RULE_ASSUM_TAC (ONCE_REWRITE_RULE[
derived_form_b]);
BY(ASM_MESON_TAC[]);
DISCH_TAC;
RULE_ASSUM_TAC(ONCE_REWRITE_RULE[Leaf_cell.RE_EQVL_SYM]);
FIRST_X_ASSUM MP_TAC;
ASM_REWRITE_TAC[Trigonometry2.re_eqvl];
REPEAT WEAKER_STRIP_TAC;
ASM_REWRITE_TAC[];
TYPIFY `f' x * f' x` EXISTS_TAC;
GMATCH_SIMP_TAC
REAL_LT_MUL_EQ;
ASM_REWRITE_TAC[];
BY(REAL_ARITH_TAC)
]);;
let SECOND_CHAIN_GENERAL = prove_by_refinement(
`!P Q f f' f'' g g' g'' x y.
(P x) /\ (Q (f x)) /\ (f x = y) /\
real_open {x | P x /\ Q (f x) } /\
(!x.
derived_form (P x) f (f' x) x (:real)) /\
(!y.
derived_form (Q( y)) g (g' y) y (:real)) /\
derived_form T f' f'' x (:real) /\
derived_form T g' g'' y (:real) ==>
derived_form T (\q. g' (f q) * f' q) (g' y * f'' + g'' * f' x pow 2 ) x (:real)`,
(* {{{ proof *)
[
REPEAT WEAKER_STRIP_TAC;
MP_TAC (GEN_ALL (Calc_derivative.differentiate `(\(q:real). (g':real->
real) (f q) * f' q)` `x:real` `(:real)`));
DISCH_THEN (C INTRO_TAC [`g'`;`f`;`f''`;`f' x`;`g''`;`f'`;`x`]);
ASM_REWRITE_TAC[];
ONCE_REWRITE_TAC[
derived_form_b];
ANTS_TAC;
RULE_ASSUM_TAC (ONCE_REWRITE_RULE[
derived_form_b]);
BY(ASM_MESON_TAC[]);
ASM_REWRITE_TAC[];
MATCH_MP_TAC (TAUT `(x <=> y) ==> (x ==> y)`);
REPEAT (AP_THM_TAC ORELSE AP_TERM_TAC);
BY(REAL_ARITH_TAC)
]);;
let SECOND_CHAIN_CRITICAL = prove_by_refinement(
`!P Q f f' f'' g g' g'' x y.
(P x) /\ (Q (f x)) /\ (f x = y) /\ g' y = &0 /\
real_open {x | P x /\ Q (f x) } /\
(!x.
derived_form (P x) f (f' x) x (:real)) /\
(!y.
derived_form (Q( y)) g (g' y) y (:real)) /\
derived_form T f' f'' x (:real) /\
derived_form T g' g'' y (:real) ==>
derived_form T (\q. g' (f q) * f' q) (g'' * (f' x) pow 2) x (:real)`,
(* {{{ proof *)
[
REPEAT WEAKER_STRIP_TAC;
MP_TAC (GEN_ALL (Calc_derivative.differentiate `(\(q:real). (g':real->
real) (f q) * f' q)` `x:real` `(:real)`));
DISCH_THEN (C INTRO_TAC [`g'`;`f`;`f''`;`f' x`;`g''`;`f'`;`x`]);
ASM_REWRITE_TAC[];
ONCE_REWRITE_TAC[
derived_form_b];
ANTS_TAC;
RULE_ASSUM_TAC (ONCE_REWRITE_RULE[
derived_form_b]);
BY(ASM_MESON_TAC[]);
ASM_REWRITE_TAC[];
MATCH_MP_TAC (TAUT `(x <=> y) ==> (x ==> y)`);
REPEAT (AP_THM_TAC ORELSE AP_TERM_TAC);
BY(REAL_ARITH_TAC)
]);;
let THIRD_CHAIN_GENERAL = prove_by_refinement(
`!P Q f f' f'' f''' g g' g'' g''' x y.
(P x) /\ (Q (f x)) /\ (f x = y) /\
real_open {x | P x /\ Q (f x) } /\
(!x.
derived_form (P x) f (f' x) x (:real)) /\
(!y.
derived_form (Q( y)) g (g' y) y (:real)) /\
(!x.
derived_form (P x) f' (f'' x) x (:real)) /\
(!y.
derived_form (Q y) g' (g'' y) y (:real)) /\
derived_form (P x) f'' f''' x (:real) /\
derived_form (Q y) g'' g''' y (:real)
==>
(?h'''.
derived_form T (\ (q:real). (g' (f q) * f'' q + g'' (f q) * f' q pow 2 )) h''' x (:real))`,
(* {{{ proof *)
[
REPEAT WEAKER_STRIP_TAC;
TYPIFY `(g' y * f''' + (f' x * g'' y) * f'' x) + g'' y * &2 * f' x pow 1 * f'' x + (f' x * g''') * f' x pow 2` EXISTS_TAC;
MP_TAC (GEN_ALL (Calc_derivative.differentiate `(\ (q:real). (g' ((f:real->
real) q) * f'' q + g'' (f q) * f' q pow 2 ))` `x:real` `(:real)`));
DISCH_THEN (C INTRO_TAC [`g'`; `f'''`;`f' x`;`g'' y`; `f''`;`g''`;`f`; `f'' x`;`f' x`;`g'''`;`f'`;`x`]);
ASM_REWRITE_TAC[];
ONCE_REWRITE_TAC[
derived_form_b];
ANTS_TAC;
RULE_ASSUM_TAC (ONCE_REWRITE_RULE[
derived_form_b]);
BY(ASM_MESON_TAC[]);
BY(ASM_REWRITE_TAC[])
]);;
let SECOND_DERIVATIVE_TEST_COMPOSE = prove_by_refinement(
`!P Q x y s f f' f'' f''' g g' g'' g'''.
P x /\ Q (f x) /\ (f x = y) /\ &0 < f' x /\
s
SUBSET {x | P x /\ Q (f x)} /\
real_open {x | P x /\ Q (f x) } /\
real_open s /\ x
IN s /\
(!x'. x'
IN s ==> g(f x) <= g(f x') ) /\
(!x.
derived_form (P x) f (f' x) x (:real)) /\
(!x.
derived_form (P x) f' (f'' x) x (:real)) /\
derived_form (P x) f'' f''' x (:real) /\
(!y.
derived_form (Q( y)) g (g' y) y (:real)) /\
(!y.
derived_form (Q y) g' (g'' y) y (:real)) /\
derived_form (Q y) g'' g''' y (:real) ==>
(g' y = &0 /\ &0 <= g'' y)
`,
(* {{{ proof *)
[
REPEAT WEAKER_STRIP_TAC;
INTRO_TAC Pent_hex.SECOND_DERIVATIVE_TEST [`g o f`;`(\q. g' (f q) * f' q)`;`(\ (q:real). (g' (f q) * f'' q + g'' (f q) * f' q pow 2 ))`;`x`;`s`];
ANTS_TAC;
ASM_REWRITE_TAC[];
TYPIFY_GOAL_THEN `(\q. g' (f q) * f'' q + g'' (f q) * f' q pow 2)
real_continuous atreal x` (unlist REWRITE_TAC);
MATCH_MP_TAC
SECOND_CHAIN_CONTINUOUS;
BY(ASM_MESON_TAC[]);
TYPIFY_GOAL_THEN `(!x'. x'
IN s ==> (g o f) x <= (g o f) x')` (unlist REWRITE_TAC);
BY(ASM_MESON_TAC[
o_THM]);
CONJ_TAC;
REPEAT WEAKER_STRIP_TAC;
INTRO_TAC
derived_form_chain [`f`;`f' x'`;`g`;`g' (f x')`;`x'`;`f x'`];
RULE_ASSUM_TAC (ONCE_REWRITE_RULE[
derived_form_b]);
ANTS_TAC;
TYPIFY `P x' /\ Q(f x')` (C SUBGOAL_THEN ASSUME_TAC);
BY(ASM_TAC THEN SET_TAC[]);
BY(ASM_MESON_TAC[]);
BY(REWRITE_TAC[Calc_derivative.derived_form;
WITHINREAL_UNIV]);
REPEAT WEAKER_STRIP_TAC;
TYPIFY `P x' /\ Q(f x')` (C SUBGOAL_THEN ASSUME_TAC);
BY(ASM_TAC THEN SET_TAC[]);
INTRO_TAC
SECOND_CHAIN_GENERAL [`P`;`Q`;`f`;`f'`;`f'' x'`;`g`;`g'`;`g'' (f x')`;`x'`;`f x'`];
ANTS_TAC;
ASM_REWRITE_TAC[];
RULE_ASSUM_TAC(ONCE_REWRITE_RULE[
derived_form_b]);
BY(ASM_MESON_TAC[]);
BY(ASM_REWRITE_TAC[Calc_derivative.derived_form;
WITHINREAL_UNIV]);
ASM_REWRITE_TAC[];
REPEAT WEAKER_STRIP_TAC;
SUBCONJ_TAC;
FIRST_X_ASSUM_ST `gf = &0` MP_TAC;
REWRITE_TAC[
REAL_ENTIRE];
BY(ASM_SIMP_TAC[arith `&0 < f' ==> ~(f' = &0)`]);
DISCH_TAC;
FIRST_X_ASSUM_ST `&0 <= stuff` MP_TAC;
ASM_REWRITE_TAC[];
ASM_REWRITE_TAC[arith `&0 * x + u = u`];
REPEAT WEAKER_STRIP_TAC;
MATCH_MP_TAC Real_ext.REAL_PROP_NN_RCANCEL;
TYPIFY `f' x pow 2` EXISTS_TAC;
ASM_REWRITE_TAC[];
REWRITE_TAC[arith `x pow 2 = x * x`];
GMATCH_SIMP_TAC
REAL_LT_MUL_EQ;
BY(ASM_REWRITE_TAC[])
]);;
let delta_y_pos_xrr = prove_by_refinement(
`!y1 y2 y3 y4 y5 y6. &0 < y1 /\ &0 < y2 /\ &0 < y3 ==>
(&0 <
delta_y y1 y2 y3 y4 y5 y6 <=>
&0 <
delta_x (&4) (&4) (&4) (xrr y2 y3 y4) (xrr y1 y3 y5) (xrr y1 y2 y6)) `,
(* {{{ proof *)
[
REPEAT WEAKER_STRIP_TAC;
GMATCH_SIMP_TAC
delta_x_xrr;
ASM_SIMP_TAC[arith `&0 < y ==> ~(y= &0)`];
REWRITE_TAC[arith `&0 < &64 * x <=> &0 < x`];
GMATCH_SIMP_TAC Trigonometry2.REAL_LT_DIV_0;
REWRITE_TAC[GSYM Trigonometry2.NOT_ZERO_EQ_POW2_LT];
REWRITE_TAC[
REAL_ENTIRE];
BY(ASM_TAC THEN REAL_ARITH_TAC)
]);;
let xrr_convert = prove_by_refinement(
`!y1 y2 y3 y5 y6. &0 < y1 /\ &0 < y2 /\ &0 < y3 /\ &0 < y5 /\ &0 < y6 /\
&0 <
ups_x (y1*y1) (y3*y3) (y5*y5) /\ &0 <
ups_x (y1*y1) (y2*y2) (y6*y6) ==>
{ y | &0 < y /\ &0 < xrr y2 y3 y /\ xrr y2 y3 y < &16 /\
&0 <
delta_x (&4) (&4) (&4) (xrr y2 y3 y) (xrr y1 y3 y5) (xrr y1 y2 y6)} =
{ y | &0 < y /\ &0 <
ups_x (y2*y2) (y3*y3) (y*y) /\ &0 <
delta_y y1 y2 y3 y y5 y6 }`,
(* {{{ proof *)
[
REPEAT WEAKER_STRIP_TAC;
REWRITE_TAC[
FUN_EQ_THM;
IN_ELIM_THM];
GEN_TAC;
ASM_CASES_TAC `~(&0<x)`;
BY(ASM_REWRITE_TAC[]);
RULE_ASSUM_TAC (REWRITE_RULE[]);
ASM_REWRITE_TAC[];
GMATCH_SIMP_TAC (GSYM
delta_y_pos_xrr);
ASM_REWRITE_TAC[];
ASM_SIMP_TAC[
xrr_bounds_2];
BY(MESON_TAC[])
]);;
let SECOND_DERIVATIVE_TEST_TAUM = prove_by_refinement(
`!a b y1 y2 y3 y4 y5 y6.
y4
IN real_interval (a,b) /\
real_interval (a,b)
SUBSET
{y4 | &0 <
delta_y y1 y2 y3 y4 y5 y6 /\ &0 < y4 /\ &0 <
ups_x (y2*y2) (y3*y3) (y4*y4)} /\
&0 < y1 /\ &0 < y2 /\ &0 < y3 /\ &0 < y5 /\ &0 < y6 /\
&0 <
ups_x (y1*y1) (y2*y2) (y6*y6) /\
&0 <
ups_x (y1*y1) (y3*y3) (y5*y5) /\
(num1 (rho y1) (rho y2) (rho y3) (xrr y2 y3 y4) (xrr y1 y3 y5) (xrr y1 y2 y6) = &0 ==>
dnum1 (rho y1) (rho y2) (rho y3) (xrr y2 y3 y4) (xrr y1 y3 y5) (xrr y1 y2 y6) < &0) ==>
(?y4'. y4'
IN real_interval(a,b) /\ taum y1 y2 y3 y4' y5 y6 < taum y1 y2 y3 y4 y5 y6)`,
(* {{{ proof *)
[
REPEAT WEAKER_STRIP_TAC;
PROOF_BY_CONTR_TAC;
RULE_ASSUM_TAC (REWRITE_RULE[
NOT_EXISTS_THM;TAUT `~(a /\ b) <=> (a ==> ~b)`]);
RULE_ASSUM_TAC (REWRITE_RULE[arith `~(x < y) <=> y <= x`]);
COMMENT "
set up second derivative";
let FIRST_DERIVATIVE_TEST_TAUM = prove_by_refinement(
`!y1 y2 y3 y4 y5 y6.
&0 <
delta_y y1 y2 y3 y4 y5 y6 /\
&0 < y1 /\
&0 < y2 /\
&0 < y3 /\
&0 < y5 /\
&0 < y6 /\
&0 < y4 /\
&0 <
ups_x (y1 * y1) (y2 * y2) (y6 * y6) /\
&0 <
ups_x (y1 * y1) (y3 * y3) (y5 * y5) /\
&0 <
ups_x (y2 * y2) (y3 * y3) (y4* y4) /\
&0 < num1 (rho y1) (rho y2) (rho y3) (xrr y2 y3 y4) (xrr y1 y3 y5) (xrr y1 y2 y6) ==>
(?a b. y4
IN real_interval (a,b) /\
(!y4' y4''. (y4'
IN real_interval(a,b) /\ y4''
IN real_interval(a,b) /\ y4' < y4'' ==>
taum y1 y2 y3 y4' y5 y6 < taum y1 y2 y3 y4'' y5 y6)))
`,
(* {{{ proof *)
[
REPEAT WEAKER_STRIP_TAC;
REPEAT WEAKER_STRIP_TAC;
PROOF_BY_CONTR_TAC;
RULE_ASSUM_TAC (REWRITE_RULE[
NOT_EXISTS_THM;TAUT `!a b. ~(a ==> b) <=> (a /\ ~b)`]);
COMMENT "
set up first derivative";
let rho_bounds = prove_by_refinement(
`!y. &2 <= y /\ y <= &2 * h0 ==> &1 <= rho y /\ rho y <= &1 + sol0 /
pi`,
(* {{{ proof *)
[
REWRITE_TAC[Nonlinear_lemma.rho_alt;Nonlinear_lemma.sol0_over_pi_EQ_const1];
REPEAT WEAKER_STRIP_TAC;
ASSUME_TAC
const1_pos;
REWRITE_TAC[arith `&1 <= &1 + x <=> &0 <= x`;arith `&1 + c* x <= &1 + c <=> &0 <= c *(&1 - x)`];
GMATCH_SIMP_TAC
REAL_LE_MUL;
GMATCH_SIMP_TAC
REAL_LE_MUL;
BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC)
]);;
let LEMMA_1834976363 = prove_by_refinement(
`main_nonlinear_terminal_v11 ==> (!y1 y2 y3 y4 y5 y6 a b.
&2 <= y1 /\ y1 <= &2 * h0 /\
&2 <= y2 /\ y2 <= &2 * h0 /\
&2 <= y3 /\ y3 <= &2 * h0 /\
(&2 / h0) pow 2 <= xrr y2 y3 y4 /\ xrr y2 y3 y4 <= #15.53 /\
(&2 / h0) pow 2 <= xrr y1 y3 y5 /\
(&2 / h0) pow 2 <= xrr y1 y2 y6 /\
y4
IN real_interval (a,b) /\
real_interval (a,b)
SUBSET
{y4 | &0 <
delta_y y1 y2 y3 y4 y5 y6 /\ &0 < y4 /\ &0 <
ups_x (y2*y2) (y3*y3) (y4*y4)} /\
&0 < y5 /\ &0 < y6 /\
&0 <
ups_x (y1*y1) (y2*y2) (y6*y6) /\
&0 <
ups_x (y1*y1) (y3*y3) (y5*y5) ==>
(?y4'. y4'
IN real_interval(a,b) /\ taum y1 y2 y3 y4' y5 y6 < taum y1 y2 y3 y4 y5 y6))`,
(* {{{ proof *)
[
REPEAT WEAKER_STRIP_TAC;
MATCH_MP_TAC
SECOND_DERIVATIVE_TEST_TAUM;
ASM_REWRITE_TAC[];
ASM_SIMP_TAC[arith `&2 <= y ==> &0 < y`];
DISCH_TAC;
PROOF_BY_CONTR_TAC;
INTRO_TAC (Terminal.get_main_nonlinear "1834976363") [`rho y1`;`rho y2`;`rho y3`;`xrr y2 y3 y4`;`xrr y1 y3 y5`;`xrr y1 y2 y6`];
ASM_REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> a /\ b ==> c`];
REWRITE_TAC[arith `~(&0 > &0) /\ ~(&0 < &0)`;arith `&4 pow 2 = &16`;
rho_bounds];
ASM_SIMP_TAC[
rho_bounds];
REPEAT (GMATCH_SIMP_TAC (arith `x < y ==> x <= y`));
BY(ASM_MESON_TAC[arith `&2 <= y ==> &0 < y`;
xrr_bounds])
]);;
let xrr_increasing = prove_by_refinement(
`!y1 y2 y6 y6'. &0 < y1 /\ &0 < y2 /\ &0 <= y6 /\ y6 < y6' ==> xrr y1 y2 y6 < xrr y1 y2 y6'`,
(* {{{ proof *)
[
REPEAT WEAKER_STRIP_TAC;
ONCE_REWRITE_TAC[arith `x < y <=> &0 < y - x`];
TYPIFY `xrr y1 y2 y6' - xrr y1 y2 y6 = (&4 / (y1 * y2)) * (y6' * y6' - y6 * y6)` (C SUBGOAL_THEN SUBST1_TAC);
REWRITE_TAC[Appendix.xrr];
Calc_derivative.CALC_ID_TAC;
BY(ASM_TAC THEN REAL_ARITH_TAC);
GMATCH_SIMP_TAC
REAL_LT_MUL_EQ;
GMATCH_SIMP_TAC
REAL_LT_DIV;
GMATCH_SIMP_TAC
REAL_LT_MUL_EQ;
ONCE_REWRITE_TAC[arith `&0 < y - x <=> x < y`];
GMATCH_SIMP_TAC Misc_defs_and_lemmas.ABS_SQUARE;
BY(ASM_TAC THEN REAL_ARITH_TAC)
]);;
let xrr_decreasing = prove_by_refinement(
`!y1 y1' y2 y6. &2 <= y1 /\ &2 <= y1' /\ &2 <= y2 /\ &2 <= y6 /\ y2 <= &2 * h0 /\ y1 <= y1' ==>
xrr y1' y2 y6 <= xrr y1 y2 y6`,
(* {{{ proof *)
[
REPEAT WEAKER_STRIP_TAC;
TYPIFY `y1 = y1'` ASM_CASES_TAC;
BY(ASM_REWRITE_TAC[arith `x <= x`]);
INTRO_TAC
REAL_MVT_SIMPLE [`(\q. xrr q y2 y6)`;`\q. ( -- &4 * ((q*q + y6*y6 - y2*y2)/ (q pow 2 * y2)))`;`y1`;`y1'`];
REWRITE_TAC[
IN_REAL_INTERVAL];
ANTS_TAC;
CONJ_TAC;
BY(ASM_TAC THEN REAL_ARITH_TAC);
REPEAT WEAKER_STRIP_TAC;
MATCH_MP_TAC
HAS_REAL_DERIVATIVE_ATREAL_WITHIN;
INTRO_TAC
derived_form_xrr_wrt_y1 [`x`;`y2`;`y6`];
REWRITE_TAC[Calc_derivative.derived_form;
WITHINREAL_UNIV];
DISCH_THEN MATCH_MP_TAC;
BY(ASM_TAC THEN REAL_ARITH_TAC);
REPEAT WEAKER_STRIP_TAC;
ONCE_REWRITE_TAC [arith `x <= y <=> &0 <= y - x`];
RULE_ASSUM_TAC(ONCE_REWRITE_RULE[arith `x' - x = (-- &4 * u/v) * z <=> x - x' = &4 * u/ v * z`]);
ASM_REWRITE_TAC[];
GMATCH_SIMP_TAC
REAL_LE_MUL;
GMATCH_SIMP_TAC
REAL_LE_MUL;
GMATCH_SIMP_TAC
REAL_LE_DIV;
GMATCH_SIMP_TAC
REAL_LE_MUL;
REWRITE_TAC[
REAL_LE_POW_2];
ENOUGH_TO_SHOW_TAC ` &0 <= x * x + y6 * y6 - y2 * y2`;
BY(ASM_TAC THEN REAL_ARITH_TAC);
MATCH_MP_TAC
REAL_LE_TRANS;
TYPIFY `&2 * &2 + &2 * &2 - (&2 * h0) * (&2 * h0)` EXISTS_TAC;
CONJ_TAC;
BY(REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
MATCH_MP_TAC (arith `x <= x' /\ y <= y' /\ z' <= z ==> x + y - z <= x' + y' - z'`);
GMATCH_SIMP_TAC Misc_defs_and_lemmas.ABS_SQUARE_LE;
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)
]);;
let xrr_simple_lower_bound = prove_by_refinement(
`!y1 y2 y6 y6inf. &2 <= y1 /\ y1 <= &2 * h0 /\ &2 <= y2 /\ y2 <= &2 * h0 /\
&2 <= y6inf /\ y6inf <= y6 ==> (y6inf/ h0) pow 2 <= xrr y1 y2 y6`,
(* {{{ proof *)
[
REPEAT WEAKER_STRIP_TAC;
MATCH_MP_TAC
REAL_LE_TRANS;
TYPIFY `xrr (&2 * h0) y2 y6` EXISTS_TAC;
CONJ2_TAC;
MATCH_MP_TAC
xrr_decreasing;
BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
MATCH_MP_TAC
REAL_LE_TRANS;
TYPIFY `xrr (&2 * h0) (&2 * h0) y6` EXISTS_TAC;
CONJ2_TAC;
ONCE_REWRITE_TAC[
xrr_sym];
MATCH_MP_TAC
xrr_decreasing;
BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
MATCH_MP_TAC
REAL_LE_TRANS;
TYPIFY `xrr (&2 * h0) (&2 * h0) y6inf` EXISTS_TAC;
CONJ2_TAC;
TYPIFY `y6inf = y6` ASM_CASES_TAC;
BY(ASM_REWRITE_TAC[arith `x <= x`]);
MATCH_MP_TAC (arith (`x < y ==> x <= y`));
MATCH_MP_TAC
xrr_increasing;
BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
REWRITE_TAC[Appendix.xrr];
MATCH_MP_TAC (arith `x = y ==> x <= y`);
Calc_derivative.CALC_ID_TAC;
BY(REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC)
]);;
let xrr_simple_upper_bound = prove_by_refinement(
`!y1 y2 y6 y6sup. &2 <= y1 /\ y1 <= &2 * h0 /\ &2 <= y2 /\ y2 <= &2 * h0 /\
&2 <= y6 /\ y6 <= y6sup /\ y6sup < &4 ==> xrr y1 y2 y6 <= y6sup pow 2`,
(* {{{ proof *)
[
REPEAT WEAKER_STRIP_TAC;
MATCH_MP_TAC
REAL_LE_TRANS;
TYPIFY `xrr (&2) y2 y6` EXISTS_TAC;
CONJ_TAC;
MATCH_MP_TAC
xrr_decreasing;
BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
MATCH_MP_TAC
REAL_LE_TRANS;
TYPIFY `xrr (&2) (&2) y6` EXISTS_TAC;
CONJ_TAC;
ONCE_REWRITE_TAC[
xrr_sym];
MATCH_MP_TAC
xrr_decreasing;
BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
MATCH_MP_TAC
REAL_LE_TRANS;
TYPIFY `xrr (&2) (&2) y6sup` EXISTS_TAC;
CONJ_TAC;
TYPIFY `y6sup = y6` ASM_CASES_TAC;
BY(ASM_REWRITE_TAC[arith `x <= x`]);
MATCH_MP_TAC (arith (`x < y ==> x <= y`));
MATCH_MP_TAC
xrr_increasing;
BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
REWRITE_TAC[Appendix.xrr];
MATCH_MP_TAC (arith `x = y ==> x <= y`);
Calc_derivative.CALC_ID_TAC;
BY(REAL_ARITH_TAC)
]);;
let NUM1_GENERIC = prove_by_refinement(
` (!x4inf x4sup x5inf x5sup x6inf x6sup y1 y2 y3 y4 y5 y6.
ineq
[
(&1 , rho y1, &1 + sol0/
pi);
(&1 , rho y2, &1 + sol0/
pi);
(&1 , rho y3, &1 + sol0/
pi);
(x4inf, xrr y2 y3 y4, x4sup);
(x5inf, xrr y1 y3 y5, x5sup);
(x6inf, xrr y1 y2 y6, x6sup)
]
((num1 (rho y1) (rho y2) (rho y3) (xrr y2 y3 y4) (xrr y1 y3 y5) (xrr y1 y2 y6) ) > &0) /\
&2 <= y1 /\ y1 <= &2 * h0 /\
&2 <= y2 /\ y2 <= &2 * h0 /\
&2 <= y3 /\ y3 <= &2 * h0 /\
x4inf <= xrr y2 y3 y4 /\ xrr y2 y3 y4 <= x4sup /\
x5inf <= xrr y1 y3 y5 /\ xrr y1 y3 y5 <= x5sup /\
x6inf <= xrr y1 y2 y6 /\ xrr y1 y2 y6 <= x6sup /\
&0 < y4 /\ &0 < y5 /\ &0 < y6 /\
&0 <
delta_y y1 y2 y3 y4 y5 y6 /\
&0 <
ups_x (y2 * y2) (y3 * y3) (y4* y4) /\
&0 <
ups_x (y1*y1) (y2*y2) (y6*y6) /\
&0 <
ups_x (y1*y1) (y3*y3) (y5*y5) ==>
(?a b. y4
IN real_interval (a,b) /\
(!y4' y4''. (y4'
IN real_interval(a,b) /\ y4''
IN real_interval(a,b) /\ y4' < y4'' ==>
taum y1 y2 y3 y4' y5 y6 < taum y1 y2 y3 y4'' y5 y6))))`,
(* {{{ proof *)
[
ASM_REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> a /\ b ==> c`];
REPEAT WEAKER_STRIP_TAC;
FIRST_X_ASSUM_ST `num1` MP_TAC;
ANTS_TAC;
ASM_REWRITE_TAC[];
BY(ASM_MESON_TAC[
rho_bounds]);
DISCH_TAC;
MATCH_MP_TAC
FIRST_DERIVATIVE_TEST_TAUM;
ASM_REWRITE_TAC[];
BY(ASM_SIMP_TAC[arith `n > &0 ==> &0 < n`;arith `&2 <= y ==> &0 < y`])
]);;
let LEMMA_4828966562 = prove_by_refinement(
`main_nonlinear_terminal_v11 ==>
(!y1 y2 y3 y4 y5 y6.
&2 <= y1 /\ y1 <= &2 * h0 /\
&2 <= y2 /\ y2 <= &2 * h0 /\
&2 <= y3 /\ y3 <= &2 * h0 /\
&2 <= y4 /\ y4 <= &2 * h0 /\
&2 <= y5 /\ y5 <= #3.01 /\
(&3 <= y6) /\
&0 <
delta_y y1 y2 y3 y4 y5 y6 /\
// &0 <
ups_x (y2 * y2) (y3 * y3) (y4* y4) /\
// &0 <
ups_x (y1*y1) (y3*y3) (y5*y5) /\
&0 <
ups_x (y1*y1) (y2*y2) (y6*y6) ==>
(?a b. y4
IN real_interval (a,b) /\
(!y4' y4''. (y4'
IN real_interval(a,b) /\ y4''
IN real_interval(a,b) /\ y4' < y4'' ==>
taum y1 y2 y3 y4' y5 y6 < taum y1 y2 y3 y4'' y5 y6))))`,
(* {{{ proof *)
[
REPEAT WEAKER_STRIP_TAC;
MATCH_MP_TAC
NUM1_GENERIC;
GEXISTL_TAC [ `(&2/h0) pow 2`;`(&2 * h0) pow 2`;`(&2/h0) pow 2 `;`#3.01 pow 2`;`#2.38 pow 2`;`#16.0`];
INTRO_TAC (Terminal.get_main_nonlinear "4828966562") [`xrr y2 y3 y4`;`xrr y1 y3 y5`;`xrr y1 y2 y6`;`rho y1`;`rho y2`;`rho y3`];
DISCH_THEN (unlist REWRITE_TAC);
ASM_REWRITE_TAC[];
TYPIFY `&0 <
ups_x (y2 * y2) (y3 * y3) (y4 * y4) /\ &0 <
ups_x (y1 * y1) (y3 * y3) (y5 * y5)` (C SUBGOAL_THEN ASSUME_TAC);
REPEAT (GMATCH_SIMP_TAC Ysskqoy.TRI_UPS_X_STRICT_POS);
BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
ASM_REWRITE_TAC[];
REPEAT (GMATCH_SIMP_TAC
xrr_simple_lower_bound);
ASM_REWRITE_TAC[];
REPEAT (GMATCH_SIMP_TAC
xrr_simple_upper_bound);
ASM_REWRITE_TAC[arith `#16.0 = &16`];
GMATCH_SIMP_TAC
xrr_le_16;
TYPIFY_GOAL_THEN `#2.38 pow 2 <= xrr y1 y2 y6` (unlist REWRITE_TAC);
MATCH_MP_TAC
REAL_LE_TRANS;
TYPIFY `(&3 / h0) pow 2` EXISTS_TAC;
CONJ_TAC;
BY(REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
GMATCH_SIMP_TAC
xrr_simple_lower_bound;
BY(ASM_TAC THEN REAL_ARITH_TAC);
ASM_REWRITE_TAC[];
BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC)
]);;
let LEMMA_6843920790 = prove_by_refinement(
`main_nonlinear_terminal_v11 ==>
(!y1 y2 y3 y4 y5 y6.
&2 <= y1 /\ y1 <= &2 * h0 /\
&2 <= y2 /\ y2 <= &2 * h0 /\
&2 <= y3 /\ y3 <= &2 * h0 /\
&2 <= y4 /\ y4 <= #3.01 /\
&3 <= y5 /\ xrr y1 y3 y5 <= #15.53 /\
&3 <= y6 /\ xrr y1 y2 y6 <= #15.53 /\
&0 <
delta_y y1 y2 y3 y4 y5 y6
==>
(?a b. y4
IN real_interval (a,b) /\
(!y4' y4''. (y4'
IN real_interval(a,b) /\ y4''
IN real_interval(a,b) /\ y4' < y4'' ==>
taum y1 y2 y3 y4' y5 y6 < taum y1 y2 y3 y4'' y5 y6))))`,
(* {{{ proof *)
[
REPEAT WEAKER_STRIP_TAC;
MATCH_MP_TAC
NUM1_GENERIC;
GEXISTL_TAC [ `(&2/h0) pow 2`;`#3.01 pow 2`;`(#2.38) pow 2 `;`#15.53`;`#2.38 pow 2`;`#15.53`];
INTRO_TAC (Terminal.get_main_nonlinear "6843920790") [`xrr y2 y3 y4`;`xrr y1 y3 y5`;`xrr y1 y2 y6`;`rho y1`;`rho y2`;`rho y3`];
DISCH_THEN (unlist REWRITE_TAC);
ASM_REWRITE_TAC[];
REPEAT (GMATCH_SIMP_TAC
xrr_simple_lower_bound);
ASM_REWRITE_TAC[];
REPEAT (GMATCH_SIMP_TAC
xrr_simple_upper_bound);
ASM_REWRITE_TAC[];
TYPIFY_GOAL_THEN `#2.38 pow 2 <= xrr y1 y2 y6` (ASSUME_TAC);
MATCH_MP_TAC
REAL_LE_TRANS;
TYPIFY `(&3 / h0) pow 2` EXISTS_TAC;
CONJ_TAC;
BY(REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
GMATCH_SIMP_TAC
xrr_simple_lower_bound;
BY(ASM_TAC THEN REAL_ARITH_TAC);
TYPIFY_GOAL_THEN `#2.38 pow 2 <= xrr y1 y3 y5` (ASSUME_TAC);
MATCH_MP_TAC
REAL_LE_TRANS;
TYPIFY `(&3 / h0) pow 2` EXISTS_TAC;
CONJ_TAC;
BY(REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
GMATCH_SIMP_TAC
xrr_simple_lower_bound;
BY(ASM_TAC THEN REAL_ARITH_TAC);
TYPIFY `&0 <
ups_x (y2 * y2) (y3 * y3) (y4 * y4) ` (C SUBGOAL_THEN ASSUME_TAC);
REPEAT (GMATCH_SIMP_TAC Ysskqoy.TRI_UPS_X_STRICT_POS);
BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
ASM_REWRITE_TAC[];
REPEAT (GMATCH_SIMP_TAC
xrr_bounds_2);
BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC)
]);;
let is_scs_funlist_basic = prove_by_refinement(
`!k d a0 b0 a b . d < #0.9 /\ 3 <= k /\ k <= 6 /\
(!i j. i < j /\ j < k ==>
funlist_v39 a a0 k i j <=
funlist_v39 b b0 k i j) /\
(!i j. i < j /\ j < k ==> &2 <=
funlist_v39 a a0 k i j) /\
(!i. i < 3 /\ k = 3 ==>
funlist_v39 b b0 k i (SUC i) < &4) /\
(!i. i < k /\ 3 < k ==>
funlist_v39 b b0 k i (SUC i) <= cstab) /\
CARD
{i | i < k /\
(&2 * h0 <
funlist_v39 b b0 k i (SUC i) \/
&2 <
funlist_v39 a a0 k i (SUC i))} +
k <= 6 ==>
is_scs_v39 (scs_v39 (k,d,
funlist_v39 a a0 k,
funlist_v39 a a0 k,
funlist_v39 b b0 k,
funlist_v39 b b0 k,
(\i j. F),{},{},{}))`,
(* {{{ proof *)
[
REPEAT WEAKER_STRIP_TAC;
ONCE_REWRITE_TAC[GSYM Terminal.funlistA_empty];
MATCH_MP_TAC Terminal.is_scs_funlist;
ASM_REWRITE_TAC[Appendix.periodic_empty];
BY(REWRITE_TAC[Terminal.funlistA_empty])
]);;
let periodic2_cs_adj = prove_by_refinement(
`!k r r'. periodic2(
cs_adj k r r') k`,
(* {{{ proof *)
[
REPEAT WEAKER_STRIP_TAC;
REWRITE_TAC[
LET_DEF;
LET_END_DEF;Appendix.periodic2;Appendix.cs_adj];
TYPIFY `!i. (i + k) MOD k = i MOD k` (C SUBGOAL_THEN ASSUME_TAC);
GEN_TAC;
ONCE_REWRITE_TAC[arith `i + (k:num) = 1 * k + i`];
BY(REWRITE_TAC[
MOD_MULT_ADD]);
REPEAT WEAKER_STRIP_TAC;
BY(ASM_REWRITE_TAC[arith `SUC (i + k) = (SUC i + k)`])
]);;
let is_scs_adj = prove_by_refinement(
`!k d r r' s s'. d < #0.9 /\ 3 <= k /\ k <= 6 /\ (k = 3 ==> s < &4) /\ (3 < k ==> s <= cstab) /\
(&2 <= r ) /\ (&2 <= r') /\ (r <= s) /\ (r' <= s') /\ (3 < k ==> s <= &2 * h0 /\ r = &2) ==>
is_scs_v39 (
mk_unadorned_v39 k d (
cs_adj k r r') (
cs_adj k s s'))`,
(* {{{ proof *)
[
REPEAT WEAKER_STRIP_TAC;
ASM_REWRITE_TAC[Appendix.is_scs_v39;Terminal.scs_unadorned_explicit;Appendix.scs_v39_explicit;arith `x <= x`;Appendix.periodic_empty;
periodic2_cs_adj];
CONJ_TAC;
BY(REWRITE_TAC[Appendix.periodic2]);
CONJ_TAC;
REPEAT WEAKER_STRIP_TAC;
REWRITE_TAC[Appendix.cs_adj];
CONJ_TAC;
BY(MESON_TAC[]);
CONJ_TAC;
BY(MESON_TAC[]);
BY(MESON_TAC[]);
CONJ_TAC;
REPEAT WEAKER_STRIP_TAC;
REWRITE_TAC[Appendix.cs_adj];
COND_CASES_TAC THEN ASM_REWRITE_TAC[];
BY(REAL_ARITH_TAC);
COND_CASES_TAC;
BY(ASM_TAC THEN REAL_ARITH_TAC);
BY(ASM_TAC THEN REAL_ARITH_TAC);
CONJ_TAC;
REPEAT WEAKER_STRIP_TAC;
BY(REWRITE_TAC[Appendix.cs_adj]);
CONJ_TAC;
REPEAT WEAKER_STRIP_TAC;
REWRITE_TAC[Appendix.cs_adj];
COND_CASES_TAC;
BY(ASM_MESON_TAC[
MOD_LT;arith `3 <= k ==> 0 < k`]);
BY(ASM_TAC THEN REAL_ARITH_TAC);
CONJ_TAC;
REPEAT WEAKER_STRIP_TAC;
REWRITE_TAC[Appendix.cs_adj];
ASM_REWRITE_TAC[];
FIRST_X_ASSUM (RULE_ASSUM_TAC o (unlist REWRITE_RULE));
BY(ASM_TAC THEN REAL_ARITH_TAC);
CONJ_TAC;
REPEAT WEAKER_STRIP_TAC;
REWRITE_TAC[Appendix.cs_adj];
FIRST_X_ASSUM (RULE_ASSUM_TAC o (unlist REWRITE_RULE));
BY(ASM_TAC THEN REAL_ARITH_TAC);
ASM_CASES_TAC `k=3`;
ASM_REWRITE_TAC[arith `x + 3 <= 6 <=> x <= 3`];
INTRO_TAC
HAS_SIZE_NUMSEG_LT [`3`];
REWRITE_TAC[
HAS_SIZE];
TYPIFY `{i | i < 3 /\ (&2 * h0 <
cs_adj 3 s s' i (SUC i) \/ &2 <
cs_adj 3 r r' i (SUC i))}
SUBSET {i | i < 3}` (C SUBGOAL_THEN MP_TAC);
BY(SET_TAC[]);
BY(MESON_TAC[
CARD_SUBSET]);
TYPIFY `{i | i < k /\ (&2 * h0 <
cs_adj k s s' i (SUC i) \/ &2 <
cs_adj k r r' i (SUC i))} = {}` ENOUGH_TO_SHOW_TAC;
DISCH_THEN SUBST1_TAC;
REWRITE_TAC[
CARD_CLAUSES];
BY(ASM_TAC THEN ARITH_TAC);
REWRITE_TAC[
EXTENSION;
IN_ELIM_THM;
NOT_IN_EMPTY];
REWRITE_TAC[Appendix.cs_adj];
GEN_TAC;
REWRITE_TAC[DE_MORGAN_THM];
REWRITE_TAC[TAUT `~a \/ b <=> a ==> b`];
DISCH_TAC;
ASM_SIMP_TAC[Qknvmlb.SUC_MOD_NOT_EQ;arith `3 <= k==> 1 < k`];
TYPIFY `3 < k` (C SUBGOAL_THEN ASSUME_TAC);
BY(ASM_TAC THEN ARITH_TAC);
FIRST_X_ASSUM_ST `h0` MP_TAC;
ASM_REWRITE_TAC[];
BY(REAL_ARITH_TAC)
]);;
let azim_in_fan_azim = prove_by_refinement(
`!vv E k i.
periodic vv k /\ 3 <= k /\ (!i j. i < k /\ j < k /\ vv i = vv j ==> i =j ) /\
E =
IMAGE (\i. {vv i, vv (SUC i)}) (:num)
==>
azim_in_fan (vv i,vv (SUC i)) E =
azim (
vec 0) (vv i) (vv (SUC i)) (vv (i + k -1))`,
(* {{{ proof *)
[
REPEAT WEAKER_STRIP_TAC;
ASM_REWRITE_TAC[Localization.azim_in_fan;
LET_DEF;
LET_END_DEF];
GMATCH_SIMP_TAC Terminal.EE_vv;
TYPIFY `k` EXISTS_TAC;
ASM_REWRITE_TAC[];
COND_CASES_TAC;
BY(REWRITE_TAC[GEN_ALL Local_lemmas.AZIM_CYCLE_TWO_POINT_SET]);
PROOF_BY_CONTR_TAC;
FIRST_X_ASSUM_ST `
CARD` MP_TAC;
TYPIFY `~(k = 0)` (C SUBGOAL_THEN ASSUME_TAC);
BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
REWRITE_TAC[];
MATCH_MP_TAC (arith `c = 2 ==> c > 1`);
MATCH_MP_TAC Hypermap.CARD_TWO_ELEMENTS;
INTRO_TAC Oxl_def.periodic_mod [`vv`;`k`];
ASM_REWRITE_TAC[];
DISCH_THEN (unlist ONCE_REWRITE_TAC);
DISCH_TAC;
TYPIFY `SUC i MOD k = (i + k - 1) MOD k` (C SUBGOAL_THEN ASSUME_TAC);
BY(ASM_MESON_TAC[
DIVISION]);
INTRO_TAC Oxlzlez.MOD_INJ1_ALT [`k-2`;`k`];
ANTS_TAC;
BY(REPEAT (FIRST_X_ASSUM_ST `3 <= k` MP_TAC) THEN ARITH_TAC);
DISCH_TAC;
FIRST_X_ASSUM (C INTRO_TAC [`SUC i`]);
ASM_REWRITE_TAC[];
BY(ASM_SIMP_TAC[arith `3 <= k ==> SUC x + k - 2 = x + k - 1`])
]);;
let sol_local_azim = prove_by_refinement(
`!vv k .
(
let E =
IMAGE (\i. {vv i, vv (SUC i)}) (:num) in
let f =
IMAGE (\i. vv i,vv (SUC i)) (:num) in
(periodic vv k /\ 3 <= k /\
(!i j. i < k /\ j < k /\ vv i = vv j ==> (i = j)) ==>
sol_local E f =
sum {i | i < k} (\i.
azim (
vec 0) (vv i) (vv (i+1)) (vv (i + (k-1)))) -
pi * (&k - &2)))`,
let vv_inj_lemma = prove_by_refinement(
`!s v k.
is_scs_v39 s /\ v
IN BBs_v39 s /\
scs_k_v39 s = k ==>
(!i j. i < k /\ j < k /\ v i = v j ==> i = j)`,
(* {{{ proof *)
[
REPEAT WEAKER_STRIP_TAC;
RULE_ASSUM_TAC(REWRITE_RULE[Appendix.is_scs_v39;
IN;Appendix.BBs_v39;LET_THM]);
ASM_TAC THEN REPEAT WEAKER_STRIP_TAC;
FIRST_X_ASSUM (C INTRO_TAC [`i`;`j`]);
REPEAT WEAKER_STRIP_TAC;
PROOF_BY_CONTR_TAC;
FIRST_X_ASSUM_ST `&2 <= x` (C INTRO_TAC [`i`;`j`]);
ASM_REWRITE_TAC[arith `~(x <= y) <=> y < x`];
FIRST_X_ASSUM_ST `a <=
dist(u,v)` MP_TAC;
ASM_REWRITE_TAC[
DIST_REFL];
BY(REAL_ARITH_TAC)
]);;
let delta_x4_imp_obtuse = prove_by_refinement(
`!x1 x2 x3 x4 x5 x6.
&0 < x1 /\ &0 <=
delta_x x1 x2 x3 x4 x5 x6 /\
delta_x4 x1 x2 x3 x4 x5 x6 < &0 ==>
pi/ &2 <
dih_x x1 x2 x3 x4 x5 x6`,
(* {{{ proof *)
[
REPEAT WEAKER_STRIP_TAC;
REWRITE_TAC[Sphere.dih_x;LET_THM];
REWRITE_TAC[arith `x < x + y <=> &0 < y`];
TYPED_ABBREV_TAC `s =
sqrt(&4 * x1 *
delta_x x1 x2 x3 x4 x5 x6)`;
TYPIFY `&0 <= s` (C SUBGOAL_THEN ASSUME_TAC);
EXPAND_TAC "s";
let scs_vv_MOD = prove_by_refinement(
`!s vv i.
is_scs_v39 s /\
BBs_v39 s vv ==> vv(i MOD
scs_k_v39 s) = vv i`,
(* {{{ proof *)
[
REWRITE_TAC[Appendix.is_scs_v39;Appendix.BBs_v39;LET_THM];
REPEAT WEAKER_STRIP_TAC;
SPEC_TAC (`i:num`,`i:num`);
MATCH_MP_TAC Xwitccn.PERIODIC_PROPERTY;
ASM_REWRITE_TAC[];
BY(FIRST_X_ASSUM_ST `3 <= k` MP_TAC THEN ARITH_TAC)
]);;
let scs_lb_2 = prove_by_refinement(
`!s vv i j.
is_scs_v39 s /\
BBs_v39 s vv /\ ~(i MOD
scs_k_v39 s = j MOD
scs_k_v39 s) ==>
&2 <=
dist(vv i,vv j)`,
(* {{{ proof *)
[
REPEAT WEAKER_STRIP_TAC;
TYPIFY_GOAL_THEN `!i. vv(i MOD
scs_k_v39 s) = vv (i)` (unlist ONCE_REWRITE_TAC o GSYM);
BY(ASM_MESON_TAC[
scs_vv_MOD]);
RULE_ASSUM_TAC(REWRITE_RULE[Appendix.is_scs_v39;Appendix.BBs_v39;LET_THM]);
TYPED_ABBREV_TAC `k =
scs_k_v39 s`;
ASM_TAC THEN REPEAT WEAKER_STRIP_TAC;
FIRST_X_ASSUM_ST `&2 <= x` (C INTRO_TAC [`i MOD k`;`j MOD k`]);
FIRST_X_ASSUM_ST `
scs_a_v39` (C INTRO_TAC [`i MOD k`;`j MOD k`]);
ASM_SIMP_TAC[arith `3 <= k ==> ~(k = 0)`;
DIVISION];
BY(REAL_ARITH_TAC)
]);;
let delta_x4_decreasing = prove_by_refinement(
`!x1 x2 x3 x4 x5 x6 x4'.
x4 <= x4' /\ &0 <= x1 ==>
delta_x4 x1 x2 x3 x4' x5 x6 <=
delta_x4 x1 x2 x3 x4 x5 x6`,
(* {{{ proof *)
[
REPEAT WEAKER_STRIP_TAC;
ENOUGH_TO_SHOW_TAC `
delta_x4 x1 x2 x3 x4 x5 x6 -
delta_x4 x1 x2 x3 x4' x5 x6 = &2 * x1 * (x4' - x4)`;
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_x4];
BY(REAL_ARITH_TAC)
]);;
let SYNQIWN = prove_by_refinement(
`main_nonlinear_terminal_v11 ==> (!s v i k.
is_scs_v39 s /\
BBs_v39 s v /\
scs_k_v39 s =k /\ 3 < k /\
((
norm (v (SUC i)) = &2 /\
dist(v i,v (i+k-1)) = &2) \/
(
norm (v (i+k-1)) = &2 /\
dist(v i,v (SUC i)) = &2) \/
(
norm (v (SUC i)) = &2 /\
norm (v(i+k-1)) = &2) \/
(
dist(v i,v(SUC i)) = &2 /\
dist(v i,v(i + k - 1)) = &2) \/
(
norm (v (SUC i)) = &2 /\
dist(v i,v (SUC i)) = &2) \/
(
norm (v (i+k-1)) = &2 /\
dist(v i,v (i+k-1)) = &2)) /\
(
dist(v i,v (SUC i)) <= &2 * h0) /\
(
dist(v (i),v(i+k-1)) <= &2 * h0) /\
cstab <=
dist(v (SUC i),v(i+k - 1)) ==>
pi/ &2 <
azim (
vec 0) (v (i)) (v (SUC i)) (v (i + k - 1)))
`,
(* {{{ proof *)
[
REPEAT WEAKER_STRIP_TAC;
REWRITE_TAC[arith `x < y <=> ~(y <= x)`];
DISCH_TAC;
TYPED_ABBREV_TAC `E =
IMAGE (\i. {v i, v (SUC i)}) (:num) `;
INTRO_TAC
vv_inj_lemma [`s`;`v`;`k`];
ASM_REWRITE_TAC[
IN];
COMMENT "noncollinearity";
let scs_diag_2 = prove_by_refinement(
`!k i. 3 < k ==>
scs_diag k (SUC i) (i + k - 1)`,
(* {{{ proof *)
[
REPEAT GEN_TAC;
REWRITE_TAC[Appendix.scs_diag];
DISCH_TAC;
TYPIFY_GOAL_THEN `~(SUC (SUC i) MOD k = (i + k - 1) MOD k)` (unlist REWRITE_TAC);
TYPIFY_GOAL_THEN `i + k - 1 = SUC(SUC i) + (k - 3)` (unlist REWRITE_TAC);
BY(ASM_TAC THEN ARITH_TAC);
BY(ASM_MESON_TAC[Oxl_2012.MOD_INJ1;arith `3 < k ==> ~(k = 0) /\ ~(k - 3 = 0) /\ (k - 3 < k)`]);
TYPIFY_GOAL_THEN `SUC (i + k - 1) = SUC i + (k-1)` (unlist REWRITE_TAC);
BY(ASM_TAC THEN ARITH_TAC);
CONJ2_TAC;
BY(ASM_MESON_TAC[Oxl_2012.MOD_INJ1;arith `3 < k ==> ~(k = 0) /\ ~(k - 1 = 0) /\ (k - 1 < k)`]);
TYPIFY_GOAL_THEN `i + k - 1 = SUC i + k - 2` (unlist REWRITE_TAC);
BY(ASM_TAC THEN ARITH_TAC);
BY(ASM_MESON_TAC[Oxl_2012.MOD_INJ1;arith `3 < k ==> ~(k = 0) /\ ~(k - 2 = 0) /\ (k - 2 < k)`])
]);;
let RRCWNS_WEAK = prove_by_refinement(
`main_nonlinear_terminal_v11 ==> (!s vv.
(let V =
IMAGE vv (:num) in
let E =
IMAGE (\i. {vv i, vv (SUC i)}) (:num) in
let k =
scs_k_v39 s in
(
BBs_v39 s vv /\ 3 < k /\
taustar_v39 s vv < &0 /\
is_scs_v39 s /\ scs_basic_v39 s /\
(!i j.
scs_diag (
scs_k_v39 s) i j ==> cstab <=
dist(vv i,vv j)) /\
(!i w. lunar(vv i,w) V E ==>
dist(vv i,vv(SUC i)) <= &2*h0 /\
dist(vv i,vv(i + k - 1)) <= &2*h0 /\
((
norm (vv (SUC i)) = &2 \/
dist(vv i, vv(SUC i)) = &2)) /\
((
norm (vv (i + k - 1)) = &2 \/
dist(vv i, vv(i + k - 1)) = &2)))
==>
scs_generic vv)))`,
(* {{{ proof *)
[
DISCH_TAC;
REWRITE_TAC[LET_THM;Appendix.scs_generic];
REPEAT WEAKER_STRIP_TAC;
INTRO_TAC Jkqewgv.JKQEWGV2 [`s`;`vv`];
ASM_REWRITE_TAC[LET_THM];
DISCH_TAC;
TYPED_ABBREV_TAC `V =
IMAGE vv (:num)`;
TYPED_ABBREV_TAC `E =
IMAGE (\i. {vv i, vv (SUC i)}) (:num)`;
TYPED_ABBREV_TAC `f =
IMAGE (\i. (vv i,vv (SUC i))) (:num)`;
TYPIFY `
convex_local_fan(V,E,f)` (C SUBGOAL_THEN ASSUME_TAC);
RULE_ASSUM_TAC (REWRITE_RULE[Appendix.BBs_v39;LET_THM]);
BY(ASM_MESON_TAC[arith `3 < k ==> ~(k <= 3)`;LET_THM]);
TYPIFY `~(?v w. lunar (v,w) V E)` ENOUGH_TO_SHOW_TAC;
FIRST_X_ASSUM (MP_TAC o (MATCH_MP Local_lemmas.CVX_LO_IMP_LO));
FIRST_X_ASSUM_ST `circular` MP_TAC;
BY(MESON_TAC[Wrgcvdr_cizmrrh.CIZMRRH]);
REPEAT WEAKER_STRIP_TAC;
INTRO_TAC Jkqewgv.JKQEWGV3 [`s`;`vv`;`v`;`w`];
ASM_REWRITE_TAC[LET_THM];
TYPIFY `v
IN V /\ w
IN V` (C SUBGOAL_THEN ASSUME_TAC);
RULE_ASSUM_TAC(REWRITE_RULE[Wrgcvdr_cizmrrh.lunar]);
BY(FIRST_X_ASSUM MP_TAC THEN SET_TAC[]);
TYPIFY `!v. v
IN V ==> ?i. v = vv i` (C SUBGOAL_THEN ASSUME_TAC);
GEN_TAC;
EXPAND_TAC "V";
let EAR_SOL_NN = prove_by_refinement(
`main_nonlinear_terminal_v11 ==> ( !y1 y2 y3 y4 y5 y6.
&2 <= y1 /\ y1 <= &2 * h0 /\
&2 <= y2 /\ y2 <= &2 * h0 /\
&2 <= y3 /\ y3 <= &2 * h0 /\
cstab <= y4 /\ y4 <= #3.915 /\
y5 = &2 /\
y6 = &2 /\
&0 <=
delta_y y1 y2 y3 y4 y5 y6 ==>
&0 <=
sol_y y1 y2 y3 y4 y5 y6)`,
(* {{{ proof *)
[
REPEAT WEAKER_STRIP_TAC;
COMMENT "delta=0";
let cs_adj_SUC = prove_by_refinement(
`!k a b i j. 1 < k ==>
cs_adj k a b i (SUC i) = a`,
(* {{{ proof *)
[
REWRITE_TAC[Appendix.scs_diag;Appendix.cs_adj];
BY(MESON_TAC[Qknvmlb.SUC_MOD_NOT_EQ])
]);;
let scs_6T1_props = prove_by_refinement(
`
scs_k_v39 scs_6T1 = 6 /\
scs_basic_v39
scs_6T1 /\
(!vv i j.
BBs_v39 scs_6T1 vv /\
scs_diag 6 i j ==> cstab <=
dist(vv i,vv j)) /\
(!vv i.
BBs_v39 scs_6T1 vv ==>
dist(vv i, vv(SUC i)) = &2)`,
(* {{{ proof *)
[
SUBCONJ_TAC;
BY(REWRITE_TAC[Appendix.scs_6T1;Terminal.scs_unadorned_explicit;]);
DISCH_TAC;
SUBCONJ_TAC;
BY(REWRITE_TAC[Appendix.scs_6T1;
scs_basic_unadorned]);
DISCH_TAC;
MP_TAC (REWRITE_RULE[Appendix.scs_6T1]
is_scs_6T1);
REWRITE_TAC[Appendix.scs_6T1;Appendix.BBs_v39;Terminal.scs_unadorned_explicit;LET_THM;Appendix.is_scs_v39];
REPEAT WEAKER_STRIP_TAC;
CONJ_TAC;
REPEAT WEAKER_STRIP_TAC;
FIRST_X_ASSUM (MP_TAC o (MATCH_MP
scs_diag_cs_adj));
BY(FIRST_X_ASSUM_ST `
cs_adj` MP_TAC THEN MESON_TAC[]);
REPEAT WEAKER_STRIP_TAC;
BY(FIRST_X_ASSUM_ST `
cs_adj` MP_TAC THEN MESON_TAC[
cs_adj_SUC;arith `&2 <= x /\ x <= &2 ==> x = &2`;arith `1 < 6`])
]);;
let scs_6T1_generic = prove_by_refinement(
`main_nonlinear_terminal_v11 ==> (!vv.
(let V =
IMAGE vv (:num) in
let E =
IMAGE (\i. {vv i, vv (SUC i)}) (:num) in
BBs_v39 scs_6T1 vv /\
taustar_v39 scs_6T1 vv < &0 ==>
scs_generic vv))`,
(* {{{ proof *)
[
REWRITE_TAC[LET_THM];
REPEAT WEAKER_STRIP_TAC;
MATCH_MP_TAC (UNDISCH (REWRITE_RULE[LET_THM]
RRCWNS_WEAK));
TYPIFY `
scs_6T1` EXISTS_TAC;
ASM_REWRITE_TAC[
is_scs_6T1];
ASSUME_TAC
scs_6T1_props;
ASM_REWRITE_TAC[];
REWRITE_TAC[arith `3 < 6`;(REWRITE_RULE[GSYM Appendix.scs_6T1]
is_scs_6T1)];
CONJ_TAC;
BY(ASM_MESON_TAC[]);
REPEAT WEAKER_STRIP_TAC;
REWRITE_TAC[arith `i+6 - 1 = i+5`];
TYPIFY `
dist(vv i,vv(i+5)) =
dist(vv(i+5),vv(SUC(i+5)))` (C SUBGOAL_THEN SUBST1_TAC);
TYPIFY `vv (SUC (i+5)) = vv(i)` ENOUGH_TO_SHOW_TAC;
BY(DISCH_THEN SUBST1_TAC THEN REWRITE_TAC[
DIST_SYM]);
RULE_ASSUM_TAC(REWRITE_RULE[Appendix.BBs_v39;LET_THM;
scs_6T1_props;Sphere.periodic]);
BY(ASM_REWRITE_TAC[arith `SUC (i+5) = i + 6`]);
ASM_SIMP_TAC[];
BY(REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC)
]);;
let is_scs_5T1 = prove_by_refinement(
`
is_scs_v39 (
scs_5T1)`,
(* {{{ proof *)
[
REWRITE_TAC[Appendix.scs_5T1];
MATCH_MP_TAC
is_scs_adj;
REWRITE_TAC[Appendix.d_tame;Sphere.cstab];
REWRITE_TAC[arith `~(5 = 3) /\ (3 <= 5) /\ (5 <= 6) /\ (3 < 5)`];
BY(REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC)
]);;
let scs_5T1_props = prove_by_refinement(
`
scs_k_v39 scs_5T1 = 5 /\
scs_basic_v39
scs_5T1 /\
(!vv i j.
BBs_v39 scs_5T1 vv /\
scs_diag 5 i j ==> cstab <=
dist(vv i,vv j)) /\
(!vv i.
BBs_v39 scs_5T1 vv ==>
dist(vv i, vv(SUC i)) = &2)`,
(* {{{ proof *)
[
SUBCONJ_TAC;
BY(REWRITE_TAC[Appendix.scs_5T1;Terminal.scs_unadorned_explicit;]);
DISCH_TAC;
SUBCONJ_TAC;
BY(REWRITE_TAC[Appendix.scs_5T1;
scs_basic_unadorned]);
DISCH_TAC;
MP_TAC
is_scs_5T1;
REWRITE_TAC[Appendix.scs_5T1;Appendix.BBs_v39;Terminal.scs_unadorned_explicit;LET_THM;Appendix.is_scs_v39];
REPEAT WEAKER_STRIP_TAC;
CONJ_TAC;
REPEAT WEAKER_STRIP_TAC;
FIRST_X_ASSUM (MP_TAC o (MATCH_MP
scs_diag_cs_adj));
BY(FIRST_X_ASSUM_ST `
cs_adj` MP_TAC THEN MESON_TAC[]);
REPEAT WEAKER_STRIP_TAC;
BY(FIRST_X_ASSUM_ST `
cs_adj` MP_TAC THEN MESON_TAC[
cs_adj_SUC;arith `&2 <= x /\ x <= &2 ==> x = &2`;arith `1 < 5`])
]);;
let scs_5T1_generic = prove_by_refinement(
`main_nonlinear_terminal_v11 ==> (!vv.
(let V =
IMAGE vv (:num) in
let E =
IMAGE (\i. {vv i, vv (SUC i)}) (:num) in
BBs_v39 scs_5T1 vv /\
taustar_v39 scs_5T1 vv < &0 ==>
scs_generic vv))`,
(* {{{ proof *)
[
REWRITE_TAC[LET_THM];
REPEAT WEAKER_STRIP_TAC;
MATCH_MP_TAC (UNDISCH (REWRITE_RULE[LET_THM]
RRCWNS_WEAK));
TYPIFY `
scs_5T1` EXISTS_TAC;
ASM_REWRITE_TAC[
is_scs_5T1];
ASSUME_TAC
scs_5T1_props;
ASM_REWRITE_TAC[];
REWRITE_TAC[arith `3 < 5`;(
is_scs_5T1)];
CONJ_TAC;
BY(ASM_MESON_TAC[]);
REPEAT WEAKER_STRIP_TAC;
REWRITE_TAC[arith `i+5 - 1 = i+4`];
TYPIFY `
dist(vv i,vv(i+4)) =
dist(vv(i+4),vv(SUC(i+4)))` (C SUBGOAL_THEN SUBST1_TAC);
TYPIFY `vv (SUC (i+4)) = vv(i)` ENOUGH_TO_SHOW_TAC;
BY(DISCH_THEN SUBST1_TAC THEN REWRITE_TAC[
DIST_SYM]);
RULE_ASSUM_TAC(REWRITE_RULE[Appendix.BBs_v39;LET_THM;
scs_5T1_props;Sphere.periodic]);
BY(ASM_REWRITE_TAC[arith `SUC (i+4) = i + 5`]);
ASM_SIMP_TAC[];
BY(REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC)
]);;
let periodic_sum_shift = prove_by_refinement(
`!j f n.
periodic f n /\ ~(n = 0) ==>
sum { i | i < n} f =
sum {i | i < n } (\i. f (j+i))`,
(* {{{ proof *)
[
REPEAT WEAKER_STRIP_TAC;
INTRO_TAC Oxl_def.periodic_sum [`f`;`n`];
ASM_REWRITE_TAC[];
DISCH_THEN (C INTRO_TAC [`j`]);
TYPIFY `(0.. n - 1) = {i | i < n}` (C SUBGOAL_THEN SUBST1_TAC);
REWRITE_TAC[
EXTENSION;
IN_NUMSEG;
IN_ELIM_THM];
GEN_TAC;
BY(ASM_TAC THEN ARITH_TAC);
DISCH_THEN (SUBST1_TAC o GSYM);
INTRO_TAC Oxl_def.BIJ_SUM [`{i | (i:num) < n}`;`j..n - 1 + j`;`f`;`(\i. j+(i:num))`];
ANTS_TAC;
REWRITE_TAC[
BIJ;
INJ;
SURJ];
SUBCONJ_TAC;
REWRITE_TAC[
IN_NUMSEG;
IN_ELIM_THM];
BY(ASM_TAC THEN ARITH_TAC);
DISCH_THEN (unlist REWRITE_TAC);
REWRITE_TAC[
IN_NUMSEG;
IN_ELIM_THM];
REPEAT WEAKER_STRIP_TAC;
TYPIFY `x - (j:num)` EXISTS_TAC;
BY(ASM_TAC THEN ARITH_TAC);
DISCH_THEN (SUBST1_TAC o GSYM);
MATCH_MP_TAC
SUM_EQ;
BY(REWRITE_TAC[
o_THM])
]);;
let LEMMA_7175074394 = prove_by_refinement(
`main_nonlinear_terminal_v11 ==> (!y1 y2 y3 y4 y5 y6. ineq [
(&2,y1,#2.52);
(&2,y2,#2.52);
(&2,y3,#2.52);
(&2,y4,&2);
(#3.01,y5,#3.237);
(&2,y6,&2)
]
(
(
delta_y y1 y2 y3 y4 y5 y6 <= &20) /\ (&0 <=
delta_y y1 y2 y3 y4 y5 y6) ==>
(
dih_y y1 y2 y3 y4 y5 y6 < #0.3205)
))`,
(* {{{ proof *)
[
ASM_REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> a /\ b ==> c`;LET_THM];
REPEAT WEAKER_STRIP_TAC;
INTRO_TAC (Terminal.get_main_nonlinear "2485876245a") [`y1`;`y2`;`y3`;`y4`;`y5`;`y6`];
ASM_REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> a /\ b ==> c`;LET_THM];
ANTS_TAC;
BY(ASM_TAC THEN REAL_ARITH_TAC);
REWRITE_TAC[Sphere.delta4_y;Sphere.y_of_x];
DISCH_TAC;
INTRO_TAC (Terminal.get_main_nonlinear "7175074394") [`y1`;`y2`;`y3`;`y4`;`y5`;`y6`];
ASM_REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> a /\ b ==> c`;LET_THM];
ASM_SIMP_TAC [arith `x <= &20 ==> ~(x > &20)`];
DISCH_TAC;
REWRITE_TAC[Sphere.dih_y;LET_THM];
GMATCH_SIMP_TAC Merge_ineq.lindih_lt;
GMATCH_SIMP_TAC
REAL_LT_MUL_EQ;
CONJ_TAC;
BY(ASM_TAC THEN REAL_ARITH_TAC);
CONJ_TAC;
CONJ_TAC;
BY(MP_TAC Flyspeck_constants.bounds THEN REAL_ARITH_TAC);
CONJ_TAC;
BY(ASM_TAC THEN REAL_ARITH_TAC);
BY(ASM_TAC THEN REAL_ARITH_TAC);
TYPIFY `&0 <= (&4 * (y1 * y1) *
delta_x (y1 * y1) (y2 * y2) (y3 * y3) (y4 * y4) (y5 * y5) (y6 * y6))` (C SUBGOAL_THEN ASSUME_TAC);
REPEAT (GMATCH_SIMP_TAC
REAL_LE_MUL);
REWRITE_TAC[GSYM Sphere.delta_y];
BY(ASM_TAC THEN REAL_ARITH_TAC);
GMATCH_SIMP_TAC Pack1.bp_bdt;
GMATCH_SIMP_TAC
SQRT_POS_LE;
ASM_REWRITE_TAC[];
CONJ_TAC;
GMATCH_SIMP_TAC
REAL_LE_MUL;
GMATCH_SIMP_TAC
TAN_POS_PI2_LE;
BY(MP_TAC Flyspeck_constants.bounds THEN ASM_TAC THEN REAL_ARITH_TAC);
GMATCH_SIMP_TAC
SQRT_POW_2;
ASM_REWRITE_TAC[];
MATCH_MP_TAC
REAL_LT_TRANS;
TYPIFY `#0.110186 *
delta4_squared_y y1 y2 y3 y4 y5 y6` EXISTS_TAC;
CONJ_TAC;
FIRST_X_ASSUM_ST `
x1_delta_y` MP_TAC;
BY(REWRITE_TAC[Sphere.x1_delta_y;Sphere.delta4_squared_y;Sphere.y_of_x;Sphere.x1_delta_x]);
REWRITE_TAC[Sphere.delta4_squared_y;Sphere.y_of_x;Sphere.delta4_squared_x];
REWRITE_TAC[arith `(x * y) pow 2 = x pow 2 * y pow 2`];
GMATCH_SIMP_TAC
REAL_LT_RMUL_EQ;
REWRITE_TAC[GSYM Trigonometry2.NOT_ZERO_EQ_POW2_LT];
CONJ_TAC;
BY(ASM_TAC THEN REAL_ARITH_TAC);
TYPIFY `#0.110186 =
sqrt(#0.110186) pow 2` (C SUBGOAL_THEN SUBST1_TAC);
GMATCH_SIMP_TAC
SQRT_POW_2;
BY(REAL_ARITH_TAC);
MATCH_MP_TAC Tame_inequalities.REAL_LT_SQUARE_POS;
GMATCH_SIMP_TAC
SQRT_POS_LT;
CONJ_TAC;
BY(REAL_ARITH_TAC);
TYPIFY `
atn(
sqrt #0.110186) <
atn(
tan #0.3205)` ENOUGH_TO_SHOW_TAC;
BY(REWRITE_TAC[
ATN_MONO_LT_EQ]);
GMATCH_SIMP_TAC
TAN_ATN;
CONJ_TAC;
BY(MP_TAC Flyspeck_constants.bounds THEN REAL_ARITH_TAC);
BY(REWRITE_TAC[c110186])
]);;
let angle_sum_5T1 = prove_by_refinement(
`main_nonlinear_terminal_v11 ==> (!y1 y2 y3 y4 y5 y6 y126 y135.
ineq [&2,y1,&2*h0;
&2,y2,&2*h0;
&2,y3,&2*h0;
&2,y126,&2*h0;
&2,y135,&2*h0;
&2,y4,&2;
cstab,y5,#3.237;
cstab,y6,#3.237]
(
dih_y y1 y126 y135 cstab (&2) (&2) <=
dih_y y1 y2 y3 y4 y5 y6 +
dih_y y1 y2 y126 (&2) (&2) y6 +
dih_y y1 y3 y135 (&2) (&2) y5 /\
&0 <=
delta_y y1 y2 y126 (&2) (&2) y6 /\ &0 <=
delta_y y1 y3 y135 (&2) (&2) y5 ==>
(&20 <=
delta_y y1 y2 y126 (&2) (&2) y6 \/ &20 <=
delta_y y1 y3 y135 (&2) (&2) y5)))
`,
(* {{{ proof *)
[
ASM_REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> a /\ b ==> c`];
REPEAT WEAKER_STRIP_TAC;
PROOF_BY_CONTR_TAC;
RULE_ASSUM_TAC(REWRITE_RULE[DE_MORGAN_THM;arith `~(x <= y) <=> y < x`]);
TYPIFY `#2.52 = &2 * h0` (C SUBGOAL_THEN ASSUME_TAC);
BY(REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
INTRO_TAC (Terminal.get_main_nonlinear "6789182745") [`y1`;`y2`;`y3`;`y4`;`y5`;`y6`];
ASM_REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> a /\ b ==> c`;GSYM Sphere.cstab];
DISCH_TAC;
INTRO_TAC (Terminal.get_main_nonlinear "4887115291") [`y1`;`y126`;`y135`;`cstab`;`(&2)`;`(&2)`];
ASM_REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> a /\ b ==> c`;GSYM Sphere.cstab];
REWRITE_TAC[arith `x <= x`];
DISCH_TAC;
INTRO_TAC (UNDISCH
LEMMA_7175074394) [`y1`;`y126`;`y2`;`(&2)`;`y6`;`(&2)`];
ASM_REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> a /\ b ==> c`;GSYM Sphere.cstab;LET_THM];
INTRO_TAC (UNDISCH
LEMMA_7175074394) [`y1`;`y135`;`y3`;`(&2)`;`y5`;`(&2)`];
ASM_REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> a /\ b ==> c`;GSYM Sphere.cstab;LET_THM];
ONCE_REWRITE_TAC[Nonlinear_lemma.dih_y_sym];
REPEAT (FIRST_X_ASSUM_ST `
delta_y` MP_TAC) THEN REWRITE_TAC[Pent_hex.delta_y_hex_cases] THEN REPEAT WEAKER_STRIP_TAC;
BY(ASM_TAC THEN REAL_ARITH_TAC)
]);;
let terminal_pent_taum2 = prove_by_refinement(
`main_nonlinear_terminal_v11 ==> (!y1 y2 y3 y4 y5 y6 y126 y135.
&0 <=
delta_y y126 y1 y2 y6 (&2) (&2) /\
&0 <=
delta_y y135 y1 y3 y5 (&2) (&2) /\
dih_y y1 y126 y135 cstab (&2) (&2) <=
dih_y y1 y2 y3 y4 y5 y6 +
dih_y y1 y2 y126 (&2) (&2) y6 +
dih_y y1 y3 y135 (&2) (&2) y5
==>
(ineq [
(&2,y1,&2 * h0);
(&2,y2,&2 * h0);
(&2,y3,&2 * h0);
(&2,y4,&2);
(#3.01,y5,#3.237);
(#3.01,y6,#3.237);
(&2,y126,&2 * h0);
(&2,y135,&2 * h0)
]
(#0.616 < taum y126 y1 y2 y6 (&2) (&2) + taum y1 y2 y3 y4 y5 y6 + taum y135 y1 y3 y5 (&2) (&2))))
`,
(* {{{ proof *)
[
ASM_REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> a /\ b ==> c`];
REPEAT WEAKER_STRIP_TAC;
INTRO_TAC (UNDISCH
angle_sum_5T1) [`y1`;`y2`;`y3`;`y4`;`y5`;`y6`;`y126`;`y135`];
ASM_REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> a /\ b ==> c`];
ASM_REWRITE_TAC[Pent_hex.delta_y_hex_cases;Sphere.cstab];
STRIP_TAC;
INTRO_TAC (UNDISCH Pent_hex.terminal_pent_taum) [`y1`;`y2`;`y3`;`y4`;`y5`;`y6`;`y126`;`y135`];
BY(ASM_REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> a /\ b ==> c`]);
INTRO_TAC (UNDISCH Pent_hex.terminal_pent_taum) [`y1`;`y3`;`y2`;`y4`;`y6`;`y5`;`y135`;`y126`];
ASM_REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> a /\ b ==> c`];
TYPIFY `taum y1 y3 y2 y4 y6 y5 = taum y1 y2 y3 y4 y5 y6` ENOUGH_TO_SHOW_TAC;
BY(REAL_ARITH_TAC);
BY(MESON_TAC[Terminal.taum_sym])
]);;
let dih_y_mono = prove_by_refinement(
`!y1 y2 y3 y4 y5 y6 y4'.
y4 <= y4' /\ &0 < y1 /\ &0 < y4 /\
&0 <
delta_y y1 y2 y3 y4 y5 y6 /\
&0 <=
delta_y y1 y2 y3 y4' y5 y6 ==>
dih_y y1 y2 y3 y4 y5 y6 <=
dih_y y1 y2 y3 y4' y5 y6`,
(* {{{ proof *)
[
REPEAT WEAKER_STRIP_TAC;
TYPIFY `y4 = y4'` ASM_CASES_TAC;
BY(ASM_REWRITE_TAC[arith `x <= x`]);
ASM_CASES_TAC `&0 <
delta_y y1 y2 y3 y4' y5 y6`;
REWRITE_TAC[Sphere.dih_y;LET_THM];
MATCH_MP_TAC (arith `x < y ==> x <= y`);
MATCH_MP_TAC Tame_inequalities.DIH_X_MONO_LT_4;
GMATCH_SIMP_TAC Misc_defs_and_lemmas.ABS_SQUARE;
GMATCH_SIMP_TAC
REAL_LT_MUL_EQ;
ASM_REWRITE_TAC[GSYM Sphere.delta_y];
BY(ASM_TAC THEN REAL_ARITH_TAC);
TYPIFY `
delta_y y1 y2 y3 y4' y5 y6 = &0` (C SUBGOAL_THEN ASSUME_TAC);
BY(ASM_TAC THEN REAL_ARITH_TAC);
ASM_CASES_TAC `
delta4_y y1 y2 y3 y4' y5 y6 <= &0`;
MATCH_MP_TAC
REAL_LE_TRANS;
TYPIFY `
pi` EXISTS_TAC;
CONJ_TAC;
REWRITE_TAC[Sphere.dih_y;LET_THM];
MATCH_MP_TAC (arith (`x < y ==> x <= y`));
MATCH_MP_TAC Oxlzlez.DIH_X_LT_PI;
GMATCH_SIMP_TAC
REAL_LT_MUL_EQ;
BY(ASM_REWRITE_TAC[GSYM Sphere.delta_y]);
ASM_REWRITE_TAC[Sphere.dih_y;LET_THM;Sphere.dih_x;GSYM Sphere.delta_y];
REWRITE_TAC[arith `x * &0 = &0`;
SQRT_0];
ASM_CASES_TAC `
delta4_y y1 y2 y3 y4' y5 y6 = &0`;
RULE_ASSUM_TAC(REWRITE_RULE[Sphere.y_of_x;Sphere.delta4_y]);
ASM_REWRITE_TAC[];
BY(MESON_TAC[arith `-- &0 = &0`;Merge_ineq.atn2_0;
PI_POS;arith `&0 < x ==> x <= x / &2 + x`]);
TYPIFY `
delta4_y y1 y2 y3 y4' y5 y6 < &0` (C SUBGOAL_THEN MP_TAC);
BY(ASM_TAC THEN REAL_ARITH_TAC);
REWRITE_TAC[Sphere.y_of_x;Sphere.delta4_y];
TYPED_ABBREV_TAC `u =
delta_x4 (y1 * y1) (y2 * y2) (y3 * y3) (y4' * y4') (y5 * y5) (y6 * y6)`;
BY(MESON_TAC[arith `u < &0 ==> &0 < -- u`;Merge_ineq.atn2_0;arith `x <= x / &2 + x / &2`]);
INTRO_TAC
delta_diff4 [`y1*y1`;`y2*y2`;`y3*y3`;`y4'*y4'`;`y5*y5`;`y6*y6`;`y4*y4`];
RULE_ASSUM_TAC(REWRITE_RULE[Sphere.delta_y;Sphere.delta4_y;Sphere.y_of_x]);
ASM_REWRITE_TAC[];
ENOUGH_TO_SHOW_TAC `&0 <
delta_x (y1 * y1) (y2 * y2) (y3 * y3) (y4 * y4) (y5 * y5) (y6 * y6) /\ &0 <=
delta_x4 (y1 * y1) (y2 * y2) (y3 * y3) (y4' * y4') (y5 * y5) (y6 * y6) * (y4' * y4' - y4 * y4) /\ &0 <= (y1 * y1) * (y4' * y4' - y4 * y4) pow 2`;
BY(REAL_ARITH_TAC);
ASM_REWRITE_TAC[];
CONJ_TAC;
GMATCH_SIMP_TAC
REAL_LE_MUL;
REWRITE_TAC[arith `&0 <= a - b <=> b <= a`];
GMATCH_SIMP_TAC Misc_defs_and_lemmas.ABS_SQUARE_LE;
BY(ASM_TAC THEN REAL_ARITH_TAC);
GMATCH_SIMP_TAC
REAL_LE_MUL;
REWRITE_TAC[
REAL_LE_POW_2];
BY(REWRITE_TAC[
REAL_LE_SQUARE])
]);;
let MOD_EQ_MOD_SHIFT = prove_by_refinement(
`!n x1 x2 y. ~(n=0) ==> (((y + x1) MOD n = (y + x2) MOD n) <=> (x1 MOD n = x2 MOD n))`,
(* {{{ proof *)
[
REPEAT WEAKER_STRIP_TAC;
MATCH_MP_TAC (TAUT `((a ==> b) /\ (b ==> a)) ==> (a <=> b)`);
CONJ_TAC;
BY(ASM_MESON_TAC[Hdplygy.MOD_EQ_MOD]);
BY(ASM_MESON_TAC[
MOD_ADD_MOD])
]);;
let psort_4 = prove_by_refinement(
`!i. psort 4(i,4) = psort 4(i,0) /\ psort 4 (4,i)=psort 4 (0,i)`,
(* {{{ proof *)
[
REWRITE_TAC[Appendix.psort;LET_THM;Uxckfpe.ARITH_4_TAC]
]);;
let I_LT_J_LT_5_EXPLICIT = prove_by_refinement(
`!i j. (i < j /\ j < 5) <=> ((i = 0 /\ j = 1) \/ (i = 0 /\ j = 2) \/ (i = 0 /\ j = 3) \/ (i = 1 /\ j = 2) \/
(i = 1 /\ j = 3) \/ (i = 2 /\ j = 3) \/
(i=0 /\ j=4) \/ (i=1 /\ j=4) \/ (i=2 /\ j=4) \/ (i=3 /\ j=4))`,
(* {{{ proof *)
[
REPEAT WEAKER_STRIP_TAC;
REWRITE_TAC[Geomdetail.EQ_EXPAND];
CONJ2_TAC;
BY(ARITH_TAC);
REPEAT WEAKER_STRIP_TAC;
TYPIFY `j = 1 \/ j = 2 \/ j = 3 \/ j= 4` (C SUBGOAL_THEN ASSUME_TAC);
BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
REPEAT (FIRST_X_ASSUM DISJ_CASES_TAC) THEN ASM_REWRITE_TAC[] THEN REPEAT (FIRST_X_ASSUM MP_TAC);
BY(ARITH_TAC);
BY(ARITH_TAC);
BY(ARITH_TAC);
BY(ARITH_TAC)
]);;
let MOD_5_EXPLICIT = prove_by_refinement(
`0 MOD 5 = 0 /\ 1 MOD 5 = 1 /\ 2 MOD 5 = 2 /\ 3 MOD 5 = 3 /\ 4 MOD 5 = 4 /\
5 MOD 5 = 0 /\ 6 MOD 5 = 1 /\ 7 MOD 5 = 2`,
(* {{{ proof *)
[
ASM_SIMP_TAC[
MOD_LT;
MOD_MULT_ADD;arith `0 < 5 /\ 1 < 5 /\ 2 < 5 /\ 3 < 5 /\ 4 < 5 /\ 6 = 1*5 + 1 /\ 7 = 1*5 + 2`];
BY(ASM_SIMP_TAC[Oxlzlez.MOD_REFL_ALT;arith `~(5 =0)`])
]);;
let psort_5 = prove_by_refinement(
`
psort 5 (0,1) = (0,1) /\ psort 5 (0,2) = (0,2) /\ psort 5(0,3) = (0,3) /\ psort 5 (0,4)=(0,4) /\
psort 5 (1,1) = (1,1) /\ psort 5 (1,2) = (1,2) /\ psort 5(1,3) = (1,3) /\ psort 5 (1,4)=(1,4) /\
psort 5 (2,1) = (1,2) /\ psort 5 (2,2) = (2,2) /\ psort 5(2,3) = (2,3) /\ psort 5 (2,4)=(2,4) /\
psort 5 (3,1) = (1,3) /\ psort 5 (3,2) = (2,3) /\ psort 5(3,3) = (3,3) /\ psort 5 (3,4)=(3,4) /\
psort 5 (4,1) = (1,4) /\ psort 5 (4,2) = (2,4) /\ psort 5(4,3) = (3,4) /\ psort 5 (4,4)=(4,4) /\
psort 5 (4,5) = (0,4) /\ psort 5 (5,4) = (0,4)
`,
let is_scs_4T3 = prove_by_refinement(
`
is_scs_v39 scs_4T3`,
(* {{{ proof *)
[
REWRITE_TAC[Appendix.scs_4T3];
REWRITE_TAC[Appendix.mk_unadorned_v39];
MATCH_MP_TAC
is_scs_funlist_basic;
REWRITE_TAC[Appendix.d_tame;Sphere.cstab;Sphere.h0;Terminal.I_LT_J_LT_4_EXPLICIT];
TYPED_ABBREV_TAC `s = {i | i < 4 /\ (&2 * #1.26 <
funlist_v39 [(0,1), #3.01; (0,2),&6; (1,3),&6] (&2) 4 i (SUC i) \/ &2 <
funlist_v39 [(0,1), #3.01; (0,2), #3.01; (1,3), #3.01] (&2) 4 i (SUC i))}`;
REWRITE_TAC[arith `i < 4 <=> i=0 \/ i=1 \/ i=2 \/ i=3`];
NUM_REDUCE_TAC;
REPEAT CONJ_TAC THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[Terminal.FUNLIST_EXPLICIT;Uxckfpe.ARITH_4_TAC;
psort_4] THEN TRY (REAL_ARITH_TAC);
TYPIFY `
CARD s = 1` ENOUGH_TO_SHOW_TAC;
BY(ARITH_TAC);
MATCH_MP_TAC Misc_defs_and_lemmas.CARD_SING;
REWRITE_TAC[
SING];
TYPIFY `0` EXISTS_TAC;
EXPAND_TAC "s";
let is_scs_4T4 = prove_by_refinement(
`
is_scs_v39 scs_4T4`,
(* {{{ proof *)
[
REWRITE_TAC[Appendix.scs_4T4];
REWRITE_TAC[Appendix.mk_unadorned_v39];
MATCH_MP_TAC
is_scs_funlist_basic;
REWRITE_TAC[Appendix.d_tame;Sphere.cstab;Sphere.h0;Terminal.I_LT_J_LT_4_EXPLICIT];
TYPED_ABBREV_TAC `s = {i | i < 4 /\ (&2 * #1.26 <
funlist_v39 [(0,1),sqrt8; (0,2),&6; (1,3), #3.01] (&2 * #1.26) 4 i (SUC i) \/ &2 <
funlist_v39 [(0,1),&2 * #1.26; (0,2),sqrt8; (1,3),sqrt8] (&2) 4 i (SUC i))}`;
REWRITE_TAC[arith `i < 4 <=> i=0 \/ i=1 \/ i=2 \/ i=3`];
NUM_REDUCE_TAC;
REPEAT CONJ_TAC THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[Terminal.FUNLIST_EXPLICIT;Uxckfpe.ARITH_4_TAC;
psort_4] THEN MP_TAC
sqrt8_flyspeck (* Flyspeck_constants.bounds *) THEN TRY (REAL_ARITH_TAC);
DISCH_THEN kill;
TYPIFY `
CARD s = 1` ENOUGH_TO_SHOW_TAC;
BY(ARITH_TAC);
MATCH_MP_TAC Misc_defs_and_lemmas.CARD_SING;
REWRITE_TAC[
SING];
TYPIFY `0` EXISTS_TAC;
EXPAND_TAC "s";
let is_scs_4T5 = prove_by_refinement(
`
is_scs_v39 scs_4T5`,
(* {{{ proof *)
[
REWRITE_TAC[Appendix.scs_4T5];
REWRITE_TAC[Appendix.mk_unadorned_v39];
MATCH_MP_TAC
is_scs_funlist_basic;
REWRITE_TAC[Appendix.d_tame;Sphere.cstab;Sphere.h0;Terminal.I_LT_J_LT_4_EXPLICIT];
TYPED_ABBREV_TAC `s = {i | i < 4 /\ (&2 * #1.26 <
funlist_v39 [(0,1), #3.01; (0,2),&6; (1,3), #3.01] (&2 * #1.26) 4 i (SUC i) \/ &2 <
funlist_v39 [(0,1),&2 * #1.26; (0,2), #3.01; (1,3), #3.01] (&2) 4 i (SUC i))}`;
REWRITE_TAC[arith `i < 4 <=> i=0 \/ i=1 \/ i=2 \/ i=3`];
NUM_REDUCE_TAC;
REPEAT CONJ_TAC THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[Terminal.FUNLIST_EXPLICIT;Uxckfpe.ARITH_4_TAC;
psort_4] THEN TRY (REAL_ARITH_TAC);
TYPIFY `
CARD s = 1` ENOUGH_TO_SHOW_TAC;
BY(ARITH_TAC);
MATCH_MP_TAC Misc_defs_and_lemmas.CARD_SING;
REWRITE_TAC[
SING];
TYPIFY `0` EXISTS_TAC;
EXPAND_TAC "s";
let is_scs_3T1 = prove_by_refinement(
`
is_scs_v39 scs_3T1`,
(* {{{ proof *)
[
REWRITE_TAC[Appendix.scs_3T1];
REWRITE_TAC[Appendix.mk_unadorned_v39];
MATCH_MP_TAC
is_scs_funlist_basic;
REWRITE_TAC[Appendix.d_tame;Sphere.cstab;Sphere.h0;Terminal.I_LT_J_LT_3_EXPLICIT;arith `x + 3 <= 6 <=> x <= 3`;
CARD_3_SUBSET];
REWRITE_TAC[arith `i < 3 <=> i=0 \/ i=1 \/ i=2`];
NUM_REDUCE_TAC;
BY(REPEAT CONJ_TAC THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[Terminal.FUNLIST_EXPLICIT;Uxckfpe.ARITH_3_TAC] THEN MP_TAC
sqrt8_flyspeck (* 1 *) THEN TRY (REAL_ARITH_TAC))
]);;
let is_scs_3M1 = prove_by_refinement(
`
is_scs_v39 scs_3M1`,
(* {{{ proof *)
[
REWRITE_TAC[Appendix.scs_3M1];
REWRITE_TAC[Appendix.mk_unadorned_v39];
MATCH_MP_TAC
is_scs_funlist_basic;
REWRITE_TAC[Appendix.d_tame;Sphere.cstab;Sphere.h0;Terminal.I_LT_J_LT_3_EXPLICIT;arith `x + 3 <= 6 <=> x <= 3`;
CARD_3_SUBSET];
REWRITE_TAC[arith `i < 3 <=> i=0 \/ i=1 \/ i=2`];
NUM_REDUCE_TAC;
BY(REPEAT CONJ_TAC THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[Terminal.FUNLIST_EXPLICIT;Uxckfpe.ARITH_3_TAC] THEN MP_TAC
sqrt8_flyspeck (* 1 *) THEN TRY (REAL_ARITH_TAC))
]);;
let is_scs_3T2 = prove_by_refinement(
`
is_scs_v39 scs_3T2`,
(* {{{ proof *)
[
REWRITE_TAC[Appendix.scs_3T2];
REWRITE_TAC[Appendix.mk_unadorned_v39];
MATCH_MP_TAC
is_scs_funlist_basic;
REWRITE_TAC[Appendix.d_tame;Sphere.cstab;Sphere.h0;Terminal.I_LT_J_LT_3_EXPLICIT;arith `x + 3 <= 6 <=> x <= 3`;
CARD_3_SUBSET];
REWRITE_TAC[arith `i < 3 <=> i=0 \/ i=1 \/ i=2`];
NUM_REDUCE_TAC;
BY(REPEAT CONJ_TAC THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[Terminal.FUNLIST_EXPLICIT;Uxckfpe.ARITH_3_TAC] THEN MP_TAC
sqrt8_flyspeck (* 1 *) THEN TRY (REAL_ARITH_TAC))
]);;
let is_scs_3T3 = prove_by_refinement(
`
is_scs_v39 scs_3T3`,
(* {{{ proof *)
[
REWRITE_TAC[Appendix.scs_3T3];
REWRITE_TAC[Appendix.mk_unadorned_v39];
MATCH_MP_TAC
is_scs_funlist_basic;
REWRITE_TAC[Appendix.d_tame;Sphere.cstab;Sphere.h0;Terminal.I_LT_J_LT_3_EXPLICIT;arith `x + 3 <= 6 <=> x <= 3`;
CARD_3_SUBSET];
REWRITE_TAC[arith `i < 3 <=> i=0 \/ i=1 \/ i=2`];
NUM_REDUCE_TAC;
BY(REPEAT CONJ_TAC THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[Terminal.FUNLIST_EXPLICIT;Uxckfpe.ARITH_3_TAC] THEN MP_TAC
sqrt8_flyspeck (* 1 *) THEN TRY (REAL_ARITH_TAC))
]);;
let is_scs_3T4 = prove_by_refinement(
`
is_scs_v39 scs_3T4`,
(* {{{ proof *)
[
REWRITE_TAC[Appendix.scs_3T4];
REWRITE_TAC[Appendix.mk_unadorned_v39];
MATCH_MP_TAC
is_scs_funlist_basic;
REWRITE_TAC[Appendix.d_tame;Sphere.cstab;Sphere.h0;Terminal.I_LT_J_LT_3_EXPLICIT;arith `x + 3 <= 6 <=> x <= 3`;
CARD_3_SUBSET];
REWRITE_TAC[arith `i < 3 <=> i=0 \/ i=1 \/ i=2`];
NUM_REDUCE_TAC;
BY(REPEAT CONJ_TAC THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[Terminal.FUNLIST_EXPLICIT;Uxckfpe.ARITH_3_TAC] THEN MP_TAC
sqrt8_flyspeck (* 1 *) THEN TRY (REAL_ARITH_TAC))
]);;
let is_scs_3T5 = prove_by_refinement(
`
is_scs_v39 scs_3T5`,
(* {{{ proof *)
[
REWRITE_TAC[Appendix.scs_3T5];
REWRITE_TAC[Appendix.mk_unadorned_v39];
MATCH_MP_TAC
is_scs_funlist_basic;
REWRITE_TAC[Appendix.d_tame;Sphere.cstab;Sphere.h0;Terminal.I_LT_J_LT_3_EXPLICIT;arith `x + 3 <= 6 <=> x <= 3`;
CARD_3_SUBSET];
REWRITE_TAC[arith `i < 3 <=> i=0 \/ i=1 \/ i=2`];
NUM_REDUCE_TAC;
BY(REPEAT CONJ_TAC THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[Terminal.FUNLIST_EXPLICIT;Uxckfpe.ARITH_3_TAC] THEN MP_TAC
sqrt8_flyspeck (* 1 *) THEN TRY (REAL_ARITH_TAC))
]);;
let is_scs_3T6 = prove_by_refinement(
`
is_scs_v39 scs_3T6'`,
(* {{{ proof *)
[
REWRITE_TAC[Appendix.scs_3T6];
REWRITE_TAC[Appendix.mk_unadorned_v39];
MATCH_MP_TAC
is_scs_funlist_basic;
REWRITE_TAC[Appendix.d_tame;Sphere.cstab;Sphere.h0;Terminal.I_LT_J_LT_3_EXPLICIT;arith `x + 3 <= 6 <=> x <= 3`;
CARD_3_SUBSET];
REWRITE_TAC[arith `i < 3 <=> i=0 \/ i=1 \/ i=2`];
NUM_REDUCE_TAC;
BY(REPEAT CONJ_TAC THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[Terminal.FUNLIST_EXPLICIT;Uxckfpe.ARITH_3_TAC] THEN MP_TAC
sqrt8_flyspeck (* 1 *) THEN TRY (REAL_ARITH_TAC))
]);;
let is_scs_3T7 = prove_by_refinement(
`
is_scs_v39 scs_3T7`,
(* {{{ proof *)
[
REWRITE_TAC[Appendix.scs_3T7];
REWRITE_TAC[Appendix.mk_unadorned_v39];
MATCH_MP_TAC
is_scs_funlist_basic;
REWRITE_TAC[Appendix.d_tame;Sphere.cstab;Sphere.h0;Terminal.I_LT_J_LT_3_EXPLICIT;arith `x + 3 <= 6 <=> x <= 3`;
CARD_3_SUBSET];
REWRITE_TAC[arith `i < 3 <=> i=0 \/ i=1 \/ i=2`];
NUM_REDUCE_TAC;
BY(REPEAT CONJ_TAC THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[Terminal.FUNLIST_EXPLICIT;Uxckfpe.ARITH_3_TAC] THEN MP_TAC
sqrt8_flyspeck (* 1 *) THEN TRY (REAL_ARITH_TAC))
]);;
let is_scs_5I3 = prove_by_refinement(
`
is_scs_v39 scs_5I3`,
(* {{{ proof *)
[
REWRITE_TAC[Appendix.scs_5I3];
REWRITE_TAC[Appendix.mk_unadorned_v39];
MATCH_MP_TAC
is_scs_funlist_basic;
REWRITE_TAC[Appendix.d_tame;Sphere.cstab;Sphere.h0;
I_LT_J_LT_5_EXPLICIT];
TYPED_ABBREV_TAC `s = {i | i < 5 /\ (&2 * #1.26 <
funlist_v39 [(0,1),sqrt8; (0,2),&6; (0,3),&6; (1,3),&6; (1,4),&6; (2,4),&6] (&2 * #1.26) 5 i (SUC i) \/ &2 <
funlist_v39 [(0,1),&2 * #1.26; (0,2),&2 * #1.26; (0,3),&2 * #1.26; (1,3), &2 * #1.26; (1,4), &2 * #1.26; (2,4),&2 * #1.26] (&2) 5 i (SUC i))}`;
REWRITE_TAC[arith `i < 5 <=> i=0 \/ i=1 \/ i=2 \/ i=3 \/ i=4`];
NUM_REDUCE_TAC;
REPEAT CONJ_TAC THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[Terminal.FUNLIST_EXPLICIT;Uxckfpe.ARITH_5_TAC;
psort_5] THEN MP_TAC
sqrt8_flyspeck (* 1 *) THEN TRY (REAL_ARITH_TAC);
DISCH_THEN kill;
TYPIFY `
CARD s = 1` ENOUGH_TO_SHOW_TAC;
BY(ARITH_TAC);
MATCH_MP_TAC Misc_defs_and_lemmas.CARD_SING;
REWRITE_TAC[
SING];
TYPIFY `0` EXISTS_TAC;
EXPAND_TAC "s";
let is_scs_4I3 = prove_by_refinement(
`
is_scs_v39 scs_4I3`,
(* {{{ proof *)
[
REWRITE_TAC[Appendix.scs_4I3];
REWRITE_TAC[Appendix.mk_unadorned_v39];
MATCH_MP_TAC
is_scs_funlist_basic;
REWRITE_TAC[Appendix.d_tame;Sphere.cstab;Sphere.h0;Terminal.I_LT_J_LT_4_EXPLICIT];
TYPED_ABBREV_TAC `s = {i | i < 4 /\ (&2 * #1.26 <
funlist_v39 [(0,1),sqrt8; (0,2),&6; (1,3),&6] (&2 * #1.26) 4 i (SUC i) \/ &2 <
funlist_v39 [(0,1),&2 * #1.26; (0,2),sqrt8; (1,3),sqrt8] (&2) 4 i (SUC i))}`;
REWRITE_TAC[arith `i < 4 <=> i=0 \/ i=1 \/ i=2 \/ i=3`];
NUM_REDUCE_TAC;
REPEAT CONJ_TAC THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[Terminal.FUNLIST_EXPLICIT;Uxckfpe.ARITH_4_TAC;
psort_4] THEN TRY (MP_TAC
sqrt8_flyspeck (* 1 *) THEN REAL_ARITH_TAC);
TYPIFY `
CARD s = 1` ENOUGH_TO_SHOW_TAC;
BY(ARITH_TAC);
MATCH_MP_TAC Misc_defs_and_lemmas.CARD_SING;
REWRITE_TAC[
SING];
TYPIFY `0` EXISTS_TAC;
EXPAND_TAC "s";
let is_scs_5M1 = prove_by_refinement(
`
is_scs_v39 scs_5M1`,
(* {{{ proof *)
[
REWRITE_TAC[Appendix.scs_5M1];
REWRITE_TAC[Appendix.mk_unadorned_v39];
MATCH_MP_TAC
is_scs_funlist_basic;
REWRITE_TAC[Appendix.d_tame;Sphere.cstab;Sphere.h0;
I_LT_J_LT_5_EXPLICIT];
TYPED_ABBREV_TAC `s = {i | i < 5 /\ (&2 * #1.26 <
funlist_v39 [(0,1), #3.01; (0,2),&6; (0,3),&6; (1,3),&6; (1,4),&6; (2,4),&6] (&2 * #1.26) 5 i (SUC i) \/ &2 <
funlist_v39 [(0,1),&2 * #1.26; (0,2),&2 * #1.26; (0,3),&2 * #1.26; (1,3), &2 * #1.26; (1,4), &2 * #1.26; (2,4),&2 * #1.26] (&2) 5 i (SUC i))}`;
REWRITE_TAC[arith `i < 5 <=> i=0 \/ i=1 \/ i=2 \/ i=3 \/ i=4`];
NUM_REDUCE_TAC;
REPEAT CONJ_TAC THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[Terminal.FUNLIST_EXPLICIT;Uxckfpe.ARITH_5_TAC;
psort_5] THEN TRY (REAL_ARITH_TAC);
TYPIFY `
CARD s = 1` ENOUGH_TO_SHOW_TAC;
BY(ARITH_TAC);
MATCH_MP_TAC Misc_defs_and_lemmas.CARD_SING;
REWRITE_TAC[
SING];
TYPIFY `0` EXISTS_TAC;
EXPAND_TAC "s";
let is_scs_5M2 = prove_by_refinement(
`
is_scs_v39 scs_5M2`,
(* {{{ proof *)
[
REWRITE_TAC[Appendix.scs_5M2];
REWRITE_TAC[Appendix.mk_unadorned_v39];
MATCH_MP_TAC
is_scs_funlist_basic;
REWRITE_TAC[Appendix.d_tame;Sphere.cstab;Sphere.h0;
I_LT_J_LT_5_EXPLICIT];
TYPED_ABBREV_TAC `s = {i | i < 5 /\ (&2 * #1.26 <
funlist_v39 [(0,1), #3.01; (0,2),&6; (0,3),&6; (1,3),&6; (1,4),&6; (2,4),&6] (&2 * #1.26) 5 i (SUC i) \/ &2 <
funlist_v39 [(0,1),&2; (0,2), #3.01; (0,3), #3.01; (1,3), #3.01; (1,4), #3.01; (2,4), #3.01] (&2) 5 i (SUC i))}`;
REWRITE_TAC[arith `i < 5 <=> i=0 \/ i=1 \/ i=2 \/ i=3 \/ i=4`];
NUM_REDUCE_TAC;
REPEAT CONJ_TAC THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[Terminal.FUNLIST_EXPLICIT;Uxckfpe.ARITH_5_TAC;
psort_5] THEN TRY (REAL_ARITH_TAC);
TYPIFY `
CARD s = 1` ENOUGH_TO_SHOW_TAC;
BY(ARITH_TAC);
MATCH_MP_TAC Misc_defs_and_lemmas.CARD_SING;
REWRITE_TAC[
SING];
TYPIFY `0` EXISTS_TAC;
EXPAND_TAC "s";
let is_scs_4M1 = prove_by_refinement(
`
is_scs_v39 scs_4M1`,
(* {{{ proof *)
[
REWRITE_TAC[Appendix.scs_4M1];
REWRITE_TAC[Appendix.mk_unadorned_v39];
MATCH_MP_TAC
is_scs_funlist_basic;
REWRITE_TAC[Appendix.d_tame;Sphere.cstab;Sphere.h0;Terminal.I_LT_J_LT_4_EXPLICIT];
TYPED_ABBREV_TAC `s = {i | i < 4 /\ (&2 * #1.26 <
funlist_v39 [(0,1), #3.01; (0,2),&6; (1,3),&6] (&2 * #1.26) 4 i (SUC i) \/ &2 <
funlist_v39 [(0,1),&2 * #1.26; (0,2),&2 * #1.26; (1,3),&2 * #1.26] (&2) 4 i (SUC i))}`;
REWRITE_TAC[arith `i < 4 <=> i=0 \/ i=1 \/ i=2 \/ i=3`];
NUM_REDUCE_TAC;
REPEAT CONJ_TAC THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[Terminal.FUNLIST_EXPLICIT;Uxckfpe.ARITH_4_TAC;
psort_4] THEN TRY (MP_TAC
sqrt8_flyspeck (* 1 *) THEN REAL_ARITH_TAC);
TYPIFY `
CARD s = 1` ENOUGH_TO_SHOW_TAC;
BY(ARITH_TAC);
MATCH_MP_TAC Misc_defs_and_lemmas.CARD_SING;
REWRITE_TAC[
SING];
TYPIFY `0` EXISTS_TAC;
EXPAND_TAC "s";
let is_scs_4M2 = prove_by_refinement(
`
is_scs_v39 scs_4M2`,
(* {{{ proof *)
[
REWRITE_TAC[Appendix.scs_4M2];
REWRITE_TAC[Appendix.mk_unadorned_v39];
MATCH_MP_TAC
is_scs_funlist_basic;
REWRITE_TAC[Appendix.d_tame;Sphere.cstab;Sphere.h0;Terminal.I_LT_J_LT_4_EXPLICIT];
TYPED_ABBREV_TAC `s = {i | i < 4 /\ (&2 * #1.26 <
funlist_v39 [(0,1), #3.01; (0,2),&6; (1,3),&6] (&2 * #1.26) 4 i (SUC i) \/ &2 <
funlist_v39 [(0,1),&2 * #1.26; (0,2),&2 * #1.26; (1,3),&2 * #1.26] (&2) 4 i (SUC i))}`;
REWRITE_TAC[arith `i < 4 <=> i=0 \/ i=1 \/ i=2 \/ i=3`];
NUM_REDUCE_TAC;
REPEAT CONJ_TAC THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[Terminal.FUNLIST_EXPLICIT;Uxckfpe.ARITH_4_TAC;
psort_4] THEN TRY (MP_TAC
sqrt8_flyspeck (* 1 *) THEN REAL_ARITH_TAC);
TYPIFY `
CARD s = 1` ENOUGH_TO_SHOW_TAC;
BY(ARITH_TAC);
MATCH_MP_TAC Misc_defs_and_lemmas.CARD_SING;
REWRITE_TAC[
SING];
TYPIFY `0` EXISTS_TAC;
EXPAND_TAC "s";
let is_scs_4M3 = prove_by_refinement(
`
is_scs_v39 scs_4M3'`,
(* {{{ proof *)
[
REWRITE_TAC[Appendix.scs_4M3];
REWRITE_TAC[Appendix.mk_unadorned_v39];
MATCH_MP_TAC
is_scs_funlist_basic;
REWRITE_TAC[Appendix.d_tame;Sphere.cstab;Sphere.h0;Terminal.I_LT_J_LT_4_EXPLICIT];
TYPED_ABBREV_TAC `s = {i | i < 4 /\ (&2 * #1.26 <
funlist_v39 [(0,1), #3.01; (0,2),&6; (1,3),&6] (&2 * #1.26) 4 i (SUC i) \/ &2 <
funlist_v39 [(0,1),sqrt8; (0,2),sqrt8; (1,3),sqrt8] (&2) 4 i (SUC i))}`;
REWRITE_TAC[arith `i < 4 <=> i=0 \/ i=1 \/ i=2 \/ i=3`];
NUM_REDUCE_TAC;
REPEAT CONJ_TAC THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[Terminal.FUNLIST_EXPLICIT;Uxckfpe.ARITH_4_TAC;
psort_4] THEN TRY (MP_TAC
sqrt8_flyspeck (* 1 *) THEN REAL_ARITH_TAC);
TYPIFY `
CARD s = 1` ENOUGH_TO_SHOW_TAC;
BY(ARITH_TAC);
MATCH_MP_TAC Misc_defs_and_lemmas.CARD_SING;
REWRITE_TAC[
SING];
TYPIFY `0` EXISTS_TAC;
EXPAND_TAC "s";
let is_scs_4M4 = prove_by_refinement(
`
is_scs_v39 scs_4M4'`,
(* {{{ proof *)
[
REWRITE_TAC[Appendix.scs_4M4];
REWRITE_TAC[Appendix.mk_unadorned_v39];
MATCH_MP_TAC
is_scs_funlist_basic;
REWRITE_TAC[Appendix.d_tame;Sphere.cstab;Sphere.h0;Terminal.I_LT_J_LT_4_EXPLICIT];
TYPED_ABBREV_TAC `s = {i | i < 4 /\ (&2 * #1.26 <
funlist_v39 [(0,1), #3.01; (1,2), #3.01; (0,2),&6; (1,3),&6] (&2 * #1.26) 4 i (SUC i) \/ &2 <
funlist_v39 [(0,1),&2 * #1.26; (1,2),&2 * #1.26; (0,2),&2 * #1.26; (1,3), &2 * #1.26] (&2) 4 i (SUC i))}`;
REWRITE_TAC[arith `i < 4 <=> i=0 \/ i=1 \/ i=2 \/ i=3`];
NUM_REDUCE_TAC;
REPEAT CONJ_TAC THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[Terminal.FUNLIST_EXPLICIT;Uxckfpe.ARITH_4_TAC;
psort_4] THEN TRY (REAL_ARITH_TAC);
TYPIFY `s = {0,1}` ENOUGH_TO_SHOW_TAC;
DISCH_THEN SUBST1_TAC;
BY(MESON_TAC[Geomdetail.CARD2;arith `x <= 2 ==> x + 4 <= 6`]);
EXPAND_TAC "s";
let is_scs_4M5 = prove_by_refinement(
`
is_scs_v39 scs_4M5'`,
(* {{{ proof *)
[
REWRITE_TAC[Appendix.scs_4M5];
REWRITE_TAC[Appendix.mk_unadorned_v39];
MATCH_MP_TAC
is_scs_funlist_basic;
REWRITE_TAC[Appendix.d_tame;Sphere.cstab;Sphere.h0;Terminal.I_LT_J_LT_4_EXPLICIT];
TYPED_ABBREV_TAC `s = {i | i < 4 /\ (&2 * #1.26 <
funlist_v39 [(0,1), #3.01; (2,3), #3.01; (0,2),&6; (1,3),&6] (&2 * #1.26) 4 i (SUC i) \/ &2 <
funlist_v39 [(0,1),&2 * #1.26; (2,3),&2 * #1.26; (0,2),&2 * #1.26; (1,3), &2 * #1.26] (&2) 4 i (SUC i))}`;
REWRITE_TAC[arith `i < 4 <=> i=0 \/ i=1 \/ i=2 \/ i=3`];
NUM_REDUCE_TAC;
REPEAT CONJ_TAC THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[Terminal.FUNLIST_EXPLICIT;Uxckfpe.ARITH_4_TAC;
psort_4] THEN TRY (REAL_ARITH_TAC);
TYPIFY `s = {0,2}` ENOUGH_TO_SHOW_TAC;
DISCH_THEN SUBST1_TAC;
BY(MESON_TAC[Geomdetail.CARD2;arith `x <= 2 ==> x + 4 <= 6`]);
EXPAND_TAC "s";
let is_scs_4M6 = prove_by_refinement(
`
is_scs_v39 scs_4M6'`,
(* {{{ proof *)
[
REWRITE_TAC[Appendix.scs_4M6];
REWRITE_TAC[Appendix.mk_unadorned_v39];
MATCH_MP_TAC
is_scs_funlist_basic;
REWRITE_TAC[Appendix.d_tame;Sphere.cstab;Sphere.h0;Terminal.I_LT_J_LT_4_EXPLICIT];
TYPED_ABBREV_TAC `s = {i | i < 4 /\ (&2 * #1.26 <
funlist_v39 [(0,1), #3.01; (0,2),&6; (1,3),&6] (&2 * #1.26) 4 i (SUC i) \/ &2 <
funlist_v39 [(0,1),&2 * #1.26; (0,2), #3.01; (1,3), #3.01] (&2) 4 i (SUC i))}`;
REWRITE_TAC[arith `i < 4 <=> i=0 \/ i=1 \/ i=2 \/ i=3`];
NUM_REDUCE_TAC;
REPEAT CONJ_TAC THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[Terminal.FUNLIST_EXPLICIT;Uxckfpe.ARITH_4_TAC;
psort_4] THEN TRY (MP_TAC
sqrt8_flyspeck (* 1 *) THEN REAL_ARITH_TAC);
TYPIFY `
CARD s = 1` ENOUGH_TO_SHOW_TAC;
BY(ARITH_TAC);
MATCH_MP_TAC Misc_defs_and_lemmas.CARD_SING;
REWRITE_TAC[
SING];
TYPIFY `0` EXISTS_TAC;
EXPAND_TAC "s";
let is_scs_4M7 = prove_by_refinement(
`
is_scs_v39 scs_4M7`,
(* {{{ proof *)
[
REWRITE_TAC[Appendix.scs_4M7];
REWRITE_TAC[Appendix.mk_unadorned_v39];
MATCH_MP_TAC
is_scs_funlist_basic;
REWRITE_TAC[Appendix.d_tame;Sphere.cstab;Sphere.h0;Terminal.I_LT_J_LT_4_EXPLICIT];
TYPED_ABBREV_TAC `s = {i | i < 4 /\ (&2 * #1.26 <
funlist_v39 [(0,1), #3.01; (1,2), #3.01; (0,2),&6; (1,3),&6; (1,3),&6] (&2 * #1.26) 4 i (SUC i) \/ &2 <
funlist_v39 [(0,1),&2 * #1.26; (1,2),&2 * #1.26; (0,2), #3.01; (1,3), #3.01] (&2) 4 i (SUC i))}`;
REWRITE_TAC[arith `i < 4 <=> i=0 \/ i=1 \/ i=2 \/ i=3`];
NUM_REDUCE_TAC;
REPEAT CONJ_TAC THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[Terminal.FUNLIST_EXPLICIT;Uxckfpe.ARITH_4_TAC;
psort_4] THEN TRY (REAL_ARITH_TAC);
TYPIFY `s = {0,1}` ENOUGH_TO_SHOW_TAC;
DISCH_THEN SUBST1_TAC;
BY(MESON_TAC[Geomdetail.CARD2;arith `x <= 2 ==> x + 4 <= 6`]);
EXPAND_TAC "s";
let is_scs_4M8 = prove_by_refinement(
`
is_scs_v39 scs_4M8`,
(* {{{ proof *)
[
REWRITE_TAC[Appendix.scs_4M8];
REWRITE_TAC[Appendix.mk_unadorned_v39];
MATCH_MP_TAC
is_scs_funlist_basic;
REWRITE_TAC[Appendix.d_tame;Sphere.cstab;Sphere.h0;Terminal.I_LT_J_LT_4_EXPLICIT];
TYPED_ABBREV_TAC `s = {i | i < 4 /\ (&2 * #1.26 <
funlist_v39 [(0,1), #3.01; (2,3), #3.01; (0,2),&6; (1,3),&6; (1,3),&6] (&2 * #1.26) 4 i (SUC i) \/ &2 <
funlist_v39 [(0,1),&2 * #1.26; (2,3),&2 * #1.26; (0,2), #3.01; (1,3), #3.01] (&2) 4 i (SUC i))} `;
REWRITE_TAC[arith `i < 4 <=> i=0 \/ i=1 \/ i=2 \/ i=3`];
NUM_REDUCE_TAC;
REPEAT CONJ_TAC THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[Terminal.FUNLIST_EXPLICIT;Uxckfpe.ARITH_4_TAC;
psort_4] THEN TRY (REAL_ARITH_TAC);
TYPIFY `s = {0,2}` ENOUGH_TO_SHOW_TAC;
DISCH_THEN SUBST1_TAC;
BY(MESON_TAC[Geomdetail.CARD2;arith `x <= 2 ==> x + 4 <= 6`]);
EXPAND_TAC "s";
let basic_examples = prove_by_refinement(
`scs_basic_v39
scs_6I1 /\
scs_basic_v39
scs_5I1 /\
scs_basic_v39
scs_5I2 /\
scs_basic_v39
scs_5I3 /\
scs_basic_v39
scs_4I1 /\
scs_basic_v39
scs_4I2 /\
scs_basic_v39
scs_4I3 /\
scs_basic_v39
scs_3I1 /\
scs_basic_v39
scs_6T1 /\
scs_basic_v39
scs_5T1 /\
scs_basic_v39 scs_4T1 /\
scs_basic_v39 scs_4T2 /\
scs_basic_v39 scs_4T3 /\
scs_basic_v39
scs_4T4 /\
scs_basic_v39
scs_4T5 /\
scs_basic_v39
scs_3T1 /\
scs_basic_v39 scs_3T2 /\
scs_basic_v39 scs_3T3 /\
scs_basic_v39 scs_3T4 /\
scs_basic_v39 scs_3T5 /\
scs_basic_v39 scs_3T6' /\
scs_basic_v39 scs_3T7 /\
scs_basic_v39
scs_6M1 /\
scs_basic_v39
scs_5M1 /\
scs_basic_v39
scs_5M2 /\
scs_basic_v39
scs_4M1 /\
scs_basic_v39
scs_4M2 /\
scs_basic_v39 scs_4M3' /\
scs_basic_v39 scs_4M4' /\
scs_basic_v39 scs_4M5' /\
scs_basic_v39 scs_4M6' /\
scs_basic_v39
scs_4M7 /\
scs_basic_v39
scs_4M8 /\
scs_basic_v39
scs_3M1
`,
(* {{{ proof *)
[
REWRITE_TAC[Appendix.scs_basic];
REWRITE_TAC[
is_scs_examples;
unadorned_examples];
REWRITE_TAC scs_example_list;
BY(REWRITE_TAC[Terminal.scs_unadorned_explicit])
]);;