(* ========================================================================= *)
(* FLYSPECK - BOOK FORMALIZATION *)
(* *)
(* Authour : VU KHAC KY *)
(* Book lemma: SLTSTLO *)
(* Chaper : Packing (Marchal Cells) *)
(* Date : June - July 2011 *)
(* *)
(* ========================================================================= *)
module Sltstlo = struct
open Rogers;;
open Vukhacky_tactics;;
open Pack_defs;;
open Pack_concl;;
open Pack1;;
open Sphere;;
open Marchal_cells;;
open Marchal_cells_2_new;;
open Emnwuus;;
let seans_fn () =
let (tms,tm) = top_goal () in
let vss = map frees (tm::tms) in
let vs = setify (flat vss) in
map dest_var vs;;
(* =========================================================================== *)
let SLTSTLO1 = prove_by_refinement (
SLTSTLO1_concl,
[(REPEAT GEN_TAC THEN REPEAT STRIP_TAC);
(* =================== Case 1 ============================================== *)
(ASM_CASES_TAC `hl (ul:(real^3)list) < sqrt(&2)`);
(EXISTS_TAC `4`);
(REWRITE_TAC[ARITH_RULE `4 <= 4`]);
(* New subgoal *)
(SUBGOAL_THEN `mcell4 V ul = convex hull (set_of_list (ul:(real^3)list))`
ASSUME_TAC);
(REWRITE_TAC[mcell4]);
(COND_CASES_TAC);
(REFL_TAC);
(SUBGOAL_THEN `F` ASSUME_TAC);
(UP_ASM_TAC THEN UP_ASM_TAC THEN MESON_TAC[]);
(UP_ASM_TAC THEN MESON_TAC[]);
(SUBGOAL_THEN `mcell 4 V ul = mcell4 V (ul:(real^3)list)` ASSUME_TAC);
(REWRITE_TAC[mcell]);
(COND_CASES_TAC);
(SUBGOAL_THEN `F` ASSUME_TAC);
(MESON_TAC[ASSUME `4 = 0`;ARITH_RULE `~(4 = 0)`]);
(UP_ASM_TAC THEN MESON_TAC[]);
(COND_CASES_TAC);
(SUBGOAL_THEN `F` ASSUME_TAC);
(MESON_TAC[ASSUME `4 = 1`;ARITH_RULE `~(4 = 1)`]);
(UP_ASM_TAC THEN MESON_TAC[]);
(COND_CASES_TAC);
(SUBGOAL_THEN `F` ASSUME_TAC);
(MESON_TAC[ASSUME `4 = 2`;ARITH_RULE `~(4 = 2)`]);
(UP_ASM_TAC THEN MESON_TAC[]);
(COND_CASES_TAC);
(SUBGOAL_THEN `F` ASSUME_TAC);
(MESON_TAC[ASSUME `4 = 3`;ARITH_RULE `~(4 = 3)`]);
(UP_ASM_TAC THEN MESON_TAC[]);
(REFL_TAC);
(ASM_REWRITE_TAC[]);
(DEL_TAC THEN DEL_TAC);
(* New subgoal *)
(SUBGOAL_THEN `convex hull set_of_list (ul:(real^3)list) =
UNIONS {rogers V (left_action_list p ul) | p permutes 0..3}`
ASSUME_TAC);
(MATCH_MP_TAC WQPRRDY);
(ASM_REWRITE_TAC[IN]);
(* End subgoal *)
(PURE_ASM_REWRITE_TAC[]);
(REWRITE_TAC[IN_UNIONS]);
(EXISTS_TAC `rogers V (ul:(real^3)list)`);
(ASM_REWRITE_TAC[IN_ELIM_THM]);
(EXISTS_TAC `I:(num->num)`);
(STRIP_TAC);
(MESON_TAC[PERMUTES_I]);
(AP_TERM_TAC);
(REWRITE_TAC[Packing3.LEFT_ACTION_LIST_I]);
(* Finish case 1 *)
(* =================== Case 2 ============================================== *)
(NEW_GOAL `sqrt (&2) <= hl (ul:(real^3)list)`);
(UP_ASM_TAC THEN REAL_ARITH_TAC);
(SUBGOAL_THEN `? u0 u1 u2 u3. (ul:(real^3)list) = [u0:real^3;u1;u2;u3]` CHOOSE_TAC);
(MP_TAC (ASSUME `barV V 3 ul`));
(REWRITE_TAC[BARV_3_EXPLICIT]);
(FIRST_X_ASSUM CHOOSE_TAC);
(FIRST_X_ASSUM CHOOSE_TAC);
(FIRST_X_ASSUM CHOOSE_TAC);
(ASM_CASES_TAC `dist(u0:real^3, p) >= sqrt(&2)`);
(EXISTS_TAC `0`);
(REWRITE_TAC[ARITH_RULE `0 <= 4`]);
(SUBGOAL_THEN `mcell 0 V ul = mcell0 V (ul:(real^3)list)` ASSUME_TAC);
(REWRITE_TAC[mcell]);
(ONCE_ASM_REWRITE_TAC[]);
(REWRITE_TAC[mcell0]);
(REWRITE_TAC[DIFF; IN; IN_ELIM_THM]);
STRIP_TAC;
(ASM_MESON_TAC[IN]);
(REWRITE_TAC[ball;IN_ELIM_THM]);
(SUBGOAL_THEN `HD (ul:(real^3)list) = u0` ASSUME_TAC);
(ASM_REWRITE_TAC[HD]);
(ASM_REWRITE_TAC[]);
(ASM_REAL_ARITH_TAC);
(* Finish case 2 *)
(* =================== Case 3 ============================================== *)
(NEW_GOAL `dist (u0, p:real^3) < sqrt (&2)`);
(UP_ASM_TAC THEN REAL_ARITH_TAC);
(ASM_CASES_TAC `~(p IN rcone_gt (HD (ul:(real^3)list)) (HD (TL ul))
(hl (truncate_simplex 1 ul) / sqrt (&2))) `);
(EXISTS_TAC `1`);
(REWRITE_TAC[ARITH_RULE `1 <= 4`]);
(SUBGOAL_THEN `mcell 1 V ul = mcell1 V (ul:(real^3)list)` ASSUME_TAC);
(REWRITE_TAC[mcell]);
(COND_CASES_TAC);
(SUBGOAL_THEN `F` MP_TAC);
(UP_ASM_TAC THEN ARITH_TAC);
(MESON_TAC[]);
(REFL_TAC);
(ONCE_ASM_REWRITE_TAC[]);
(REWRITE_TAC[mcell1]);
(COND_CASES_TAC);
(REWRITE_TAC[IN_DIFF]);
(ASM_REWRITE_TAC[IN_INTER]);
(REWRITE_WITH `HD [u0;u1;u2;u3] = u0:real^3`);
(REWRITE_TAC[HD]);
(REWRITE_TAC[cball;IN;IN_ELIM_THM]);
(ASM_REAL_ARITH_TAC);
(NEW_GOAL `F`);
(ASM_MESON_TAC[]);
(UP_ASM_TAC THEN MESON_TAC[]);
(* Finish case 3 *)
(* =================== Case 4 ============================================== *)
(NEW_GOAL `p IN rcone_gt (HD (ul:(real^3)list)) (HD (TL ul))
(hl (truncate_simplex 1 ul) / sqrt (&2))`);
(UP_ASM_TAC THEN MESON_TAC[]);
(SWITCH_TAC THEN DEL_TAC);
(UP_ASM_TAC THEN ASM_REWRITE_TAC[HD;TL; TRUNCATE_SIMPLEX_EXPLICIT_1]);
(STRIP_TAC);
(ASM_CASES_TAC `p IN aff_ge {u0:real^3, u1} {mxi V ul, omega_list_n V ul 3}`);
(EXISTS_TAC `2`);
(REWRITE_TAC[ARITH_RULE `2 <= 4`]);
(REWRITE_TAC[MCELL_EXPLICIT; mcell2]);
(COND_CASES_TAC);
(LET_TAC);
(REWRITE_TAC[IN_INTER]);
(ASM_REWRITE_TAC[HD;TL]);
(REWRITE_TAC[GSYM (ASSUME `ul = [u0; u1; u2; u3:real^3]`)]);
(ASM_REWRITE_TAC[]);
(UP_ASM_TAC THEN UP_ASM_TAC THEN
ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);
(REPEAT STRIP_TAC);
(MATCH_MP_TAC (SET_RULE `(?s. p IN s /\ s SUBSET B) ==> p IN B`));
(EXISTS_TAC `rcone_gt (u0:real^3) u1 a`);
(REWRITE_TAC[RCONE_GT_SUBSET_RCONE_GE]);
(ASM_MESON_TAC[]);
(MATCH_MP_TAC RCONEGE_INTER_VORONOI_CLOSED_IMP_RCONEGE);
(EXISTS_TAC `V:real^3->bool`);
(ASM_REWRITE_TAC[]);
(NEW_GOAL `voronoi_nondg V (ul:(real^3)list)`);
(UNDISCH_TAC `barV V 3 (ul:(real^3)list)`);
(REWRITE_TAC[BARV]);
(STRIP_TAC THEN FIRST_ASSUM MATCH_MP_TAC);
(ASM_REWRITE_TAC[LENGTH; INITIAL_SUBLIST;ARITH_RULE `0 < 3 + 1`]);
(EXISTS_TAC `[]:(real^3)list`);
(REWRITE_TAC[APPEND]);
(UP_ASM_TAC THEN REWRITE_TAC[VORONOI_NONDG]);
(ASM_REWRITE_TAC[set_of_list]);
(REPEAT STRIP_TAC);
(* Break into 7 subgoals *)
(* Subgoal 1 & subgoal 2 *)
(ASM_SET_TAC[]);
(ASM_SET_TAC[]);
(NEW_GOAL `&0 < hl [u0; u1:real^3]`);
(REWRITE_WITH `hl [u0;u1:real^3] =
hl (truncate_simplex 1 (ul:(real^3)list))`);
(ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);
(MATCH_MP_TAC BARV_IMP_HL_1_POS_LT);
(EXISTS_TAC `V:real^3->bool`);
(ASM_REWRITE_TAC[]);
(NEW_GOAL `hl [u0;u1:real^3] = &0`);
(ASM_REWRITE_TAC[HL;set_of_list;SET_RULE `{a, a} = {a}`]);
(NEW_GOAL `radV {u1:real^3} = dist (circumcenter {u1},u1)`);
(NEW_GOAL `(!w. w IN {u1:real^3} ==> radV {u1} = dist (circumcenter {u1},w))`);
(MATCH_MP_TAC Rogers.OAPVION2);
(REWRITE_TAC[AFFINE_INDEPENDENT_1]);
(FIRST_X_ASSUM MATCH_MP_TAC);
(SET_TAC[]);
(ASM_REWRITE_TAC[Rogers.CIRCUMCENTER_1; dist]);
(NORM_ARITH_TAC);
(ASM_REAL_ARITH_TAC);
(EXPAND_TAC "a");
(MATCH_MP_TAC REAL_LT_DIV);
(STRIP_TAC);
(REWRITE_WITH `hl [u0;u1:real^3] =
hl (truncate_simplex 1 (ul:(real^3)list))`);
(ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);
(MATCH_MP_TAC BARV_IMP_HL_1_POS_LT);
(EXISTS_TAC `V:real^3->bool`);
(ASM_REWRITE_TAC[]);
(MATCH_MP_TAC SQRT_POS_LT);
(REAL_ARITH_TAC);
(EXPAND_TAC "a");
(NEW_GOAL `hl [u0; u1:real^3] / sqrt (&2) <= &1 <=>
hl [u0; u1] <= &1 * sqrt (&2)`);
(MATCH_MP_TAC REAL_LE_LDIV_EQ);
(MATCH_MP_TAC SQRT_POS_LT THEN REAL_ARITH_TAC);
(ASM_REWRITE_TAC[]);
(ASM_REAL_ARITH_TAC);
(MATCH_MP_TAC (SET_RULE `(?s. p IN s /\ s SUBSET B) ==> p IN B`));
(EXISTS_TAC `rcone_gt (u0:real^3) u1 a`);
(REWRITE_TAC[RCONE_GT_SUBSET_RCONE_GE]);
(ASM_MESON_TAC[]);
(REWRITE_WITH `p IN voronoi_closed V (u0:real^3) <=>
(?vl. vl IN barV V 3 /\
p IN rogers V vl /\
truncate_simplex 0 vl = [u0])`);
(MATCH_MP_TAC Rogers.GLTVHUM);
(ASM_REWRITE_TAC[]);
(ASM_SET_TAC[]);
(EXISTS_TAC `ul:(real^3)list`);
(ASM_REWRITE_TAC[IN; TRUNCATE_SIMPLEX_EXPLICIT_0]);
(UP_ASM_TAC THEN REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);
(REWRITE_TAC[MESON [] `~(a /\ b) <=> ~a \/ ~ b`]);
(DISCH_TAC);
(NEW_GOAL `~(hl [u0; u1:real^3] < sqrt (&2))`);
(ASM_MESON_TAC[]);
(NEW_GOAL `hl [u0; u1:real^3] >= sqrt (&2)`);
(ASM_REAL_ARITH_TAC);
(ABBREV_TAC `t = hl [u0; u1:real^3] / sqrt (&2)`);
(NEW_GOAL `&1 <= t`);
(EXPAND_TAC "t");
(NEW_GOAL `&1 <= hl [u0; u1:real^3] / sqrt (&2) <=>
&1 * sqrt (&2) <= hl [u0; u1]`);
(MATCH_MP_TAC REAL_LE_RDIV_EQ);
(MATCH_MP_TAC SQRT_POS_LT THEN REAL_ARITH_TAC);
(ASM_REWRITE_TAC[]);
(ASM_REAL_ARITH_TAC);
(UNDISCH_TAC `p IN rcone_gt (u0:real^3) u1 t`);
(REWRITE_TAC[rcone_gt;rconesgn; IN; IN_ELIM_THM; dist]);
(DISCH_TAC);
(NEW_GOAL `F`);
(NEW_GOAL `(p - u0) dot (u1 - u0) <= norm (p - u0) * norm (u1 - u0:real^3)`);
(REWRITE_TAC[NORM_CAUCHY_SCHWARZ]);
(NEW_GOAL `norm (p - u0) * norm (u1 - u0) * t >=
norm (p - u0) * norm (u1 - u0:real^3) `);
(REWRITE_TAC[REAL_ARITH `a * b * t >= a * b <=> &0 <= (t - &1) * (a * b)`]);
(MATCH_MP_TAC REAL_LE_MUL);
(STRIP_TAC);
(ASM_REAL_ARITH_TAC);
(MATCH_MP_TAC REAL_LE_MUL);
(REWRITE_TAC[NORM_POS_LE]);
(ASM_REAL_ARITH_TAC);
(UP_ASM_TAC THEN MESON_TAC[]);
(* Finish case 4 *)
(* =================== Case 5 ============================================== *)
(ASM_CASES_TAC `hl (truncate_simplex 2 (ul:(real^3)list)) >= sqrt (&2)`);
(NEW_GOAL `mxi V (ul:(real^3)list) = omega_list_n V ul 2`);
(REWRITE_TAC[mxi]);
(COND_CASES_TAC);
(REFL_TAC);
(NEW_GOAL `F`);
(ASM_REAL_ARITH_TAC);
(UP_ASM_TAC THEN MESON_TAC[]);
(NEW_GOAL `p IN aff_ge {u0, u1:real^3} {mxi V ul, omega_list_n V ul 3}`);
(MATCH_MP_TAC (SET_RULE `(?s. p IN s /\ s SUBSET B) ==> p IN B`));
(EXISTS_TAC `rogers V (ul:(real^3)list)`);
STRIP_TAC;
(ASM_REWRITE_TAC[]);
(MATCH_MP_TAC (SET_RULE `(?s. p SUBSET s /\ s SUBSET B) ==> p SUBSET B`));
(EXISTS_TAC `convex hull ({u0, u1:real^3} UNION {mxi V ul, omega_list_n V ul 3})`);
(STRIP_TAC);
(NEW_GOAL
`convex hull ({u0, u1:real^3} UNION {mxi V ul, omega_list_n V ul 3}) =
convex hull (convex hull ({u0, u1} UNION {mxi V ul, omega_list_n V ul 3}))`);
(ONCE_REWRITE_TAC[EQ_SYM_EQ]);
(REWRITE_TAC[CONVEX_HULL_EQ; CONVEX_CONVEX_HULL]);
(ONCE_ASM_REWRITE_TAC[]);
(REWRITE_TAC[ROGERS]);
(MATCH_MP_TAC CONVEX_HULL_SUBSET);
(ASM_REWRITE_TAC
[LENGTH; ARITH_RULE `SUC (SUC (SUC (SUC 0))) = 4` ; SET_OF_0_TO_3]);
(REWRITE_TAC[IMAGE;SUBSET;IN;IN_ELIM_THM]);
(REPEAT STRIP_TAC);
(ASM_CASES_TAC `x' = 0`);
(REWRITE_WITH `x = u0:real^3`);
(SWITCH_TAC THEN UP_ASM_TAC THEN ASM_REWRITE_TAC[OMEGA_LIST_N;HD]);
(ONCE_REWRITE_TAC[GSYM IN]);
(MATCH_MP_TAC IN_SET_IMP_IN_CONVEX_HULL_SET);
(SET_TAC[]);
(ASM_CASES_TAC `x' = 1`);
(REWRITE_WITH `x = circumcenter {u0,u1:real^3}`);
(ASM_REWRITE_TAC[]);
(MATCH_MP_TAC OMEGA_LIST_1_EXPLICIT_NEW);
(EXISTS_TAC `u2:real^3`);
(EXISTS_TAC `u3:real^3`);
(ASM_REWRITE_TAC[IN]);
(STRIP_TAC);
(ASM_MESON_TAC[IN]);
(ASM_CASES_TAC `hl [u0; u1:real^3] < sqrt (&2)`);
(ASM_REWRITE_TAC[]);
(NEW_GOAL `hl [u0; u1:real^3] >= sqrt (&2)`);
(ASM_REAL_ARITH_TAC);
(ABBREV_TAC `t = hl [u0; u1:real^3] / sqrt (&2)`);
(NEW_GOAL `&1 <= t`);
(EXPAND_TAC "t");
(NEW_GOAL `&1 <= hl [u0; u1:real^3] / sqrt (&2) <=>
&1 * sqrt (&2) <= hl [u0; u1]`);
(MATCH_MP_TAC REAL_LE_RDIV_EQ);
(MATCH_MP_TAC SQRT_POS_LT THEN REAL_ARITH_TAC);
(ASM_REWRITE_TAC[]);
(ASM_REAL_ARITH_TAC);
(UNDISCH_TAC `p IN rcone_gt (u0:real^3) u1 t`);
(REWRITE_TAC[rcone_gt;rconesgn; IN; IN_ELIM_THM; dist]);
(DISCH_TAC);
(NEW_GOAL `F`);
(NEW_GOAL `(p - u0) dot (u1 - u0) <= norm (p - u0) * norm (u1 - u0:real^3)`);
(REWRITE_TAC[NORM_CAUCHY_SCHWARZ]);
(NEW_GOAL `norm (p - u0) * norm (u1 - u0) * t >=
norm (p - u0) * norm (u1 - u0:real^3) `);
(REWRITE_TAC[REAL_ARITH `a * b * t >= a * b <=> &0 <= (t - &1) * (a * b)`]);
(MATCH_MP_TAC REAL_LE_MUL);
(STRIP_TAC);
(ASM_REAL_ARITH_TAC);
(MATCH_MP_TAC REAL_LE_MUL);
(REWRITE_TAC[NORM_POS_LE]);
(ASM_REAL_ARITH_TAC);
(UP_ASM_TAC THEN MESON_TAC[]);
(ONCE_REWRITE_TAC[GSYM IN]);
(MATCH_MP_TAC (SET_RULE `(?s. p IN s /\ s SUBSET B) ==> p IN B`));
(EXISTS_TAC `convex hull ({u0, u1:real^3})`);
(STRIP_TAC);
(REWRITE_TAC[Rogers.CIRCUMCENTER_2; midpoint;CONVEX_HULL_2;IN;IN_ELIM_THM]);
(EXISTS_TAC `&1 / (&2)`);
(EXISTS_TAC `&1 / (&2)`);
(ASM_SIMP_TAC[REAL_LE_DIV; REAL_ARITH `&0 <= &1 /\ &0 <= &2`]);
(STRIP_TAC);
(REAL_ARITH_TAC);
(VECTOR_ARITH_TAC);
(MATCH_MP_TAC CONVEX_HULL_SUBSET);
(SET_TAC[]);
(ASM_CASES_TAC `x' = 2`);
(ASM_REWRITE_TAC[]);
(ONCE_REWRITE_TAC[GSYM IN]);
(MATCH_MP_TAC IN_SET_IMP_IN_CONVEX_HULL_SET);
(SET_TAC[]);
(ASM_CASES_TAC `x' = 3`);
(ASM_REWRITE_TAC[]);
(ONCE_REWRITE_TAC[GSYM IN]);
(MATCH_MP_TAC IN_SET_IMP_IN_CONVEX_HULL_SET);
(SET_TAC[]);
(NEW_GOAL `F`);
(UP_ASM_TAC THEN UP_ASM_TAC THEN UP_ASM_TAC THEN UP_ASM_TAC THEN DEL_TAC);
(UP_ASM_TAC THEN TRUONG_SET_TAC[]);
(UP_ASM_TAC THEN MESON_TAC[]);
(ASM_REWRITE_TAC[SET_RULE `{a, b} UNION {c , d} = {a, b, c,d}`]);
(REWRITE_TAC[CONVEX_HULL_4_SUBSET_AFF_GE_2_2]);
(NEW_GOAL `F`);
(ASM_MESON_TAC[]);
(ASM_MESON_TAC[]);
(NEW_GOAL `hl (truncate_simplex 2 (ul:(real^3)list)) < sqrt (&2)`);
(ASM_REAL_ARITH_TAC);
(EXISTS_TAC `3`);
(REWRITE_TAC[ARITH_RULE `3 <= 4`]);
(REWRITE_TAC[MCELL_EXPLICIT; mcell3]);
(COND_CASES_TAC);
(ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2; set_of_list]);
(REWRITE_TAC[SET_RULE `{a, b ,c} UNION {d} = {a, b , c, d}`]);
(NEW_GOAL
`(?s. between s (omega_list_n V ul 2,omega_list_n V ul 3) /\
dist (u0,s:real^3) = sqrt (&2) /\
mxi V ul = s)`);
(MATCH_MP_TAC MXI_EXPLICIT_OLD);
(ASM_MESON_TAC[]);
(FIRST_X_ASSUM CHOOSE_TAC);
(REWRITE_WITH `mxi V [u0; u1; u2; u3] = s:real^3`);
(ASM_MESON_TAC[]);
(* ========================================================================= *)
(ABBREV_TAC `a = omega_list_n V ul 1`);
(ABBREV_TAC `b = omega_list_n V ul 2`);
(ABBREV_TAC `c = omega_list_n V ul 3`);
(NEW_GOAL `p IN convex hull {u0, a, b, c:real^3}`);
(EXPAND_TAC "a" THEN EXPAND_TAC "b" THEN EXPAND_TAC "c");
(REWRITE_WITH `u0:real^3 = HD ul`);
(ASM_REWRITE_TAC[HD]);
(REWRITE_WITH `convex hull
{HD ul, omega_list_n V ul 1, omega_list_n V ul 2, omega_list_n V ul 3} =
rogers V ul`);
(ONCE_REWRITE_TAC[EQ_SYM_EQ]);
(MATCH_MP_TAC ROGERS_EXPLICIT);
(ASM_REWRITE_TAC[]);
(ASM_REWRITE_TAC[]);
(NEW_GOAL `a = midpoint (u0, u1:real^3)`);
(REWRITE_TAC[GSYM Rogers.CIRCUMCENTER_2]);
(EXPAND_TAC "a");
(REWRITE_WITH `{u0,u1} = set_of_list [u0;(u1:real^3)]`);
(MESON_TAC[set_of_list]);
(REWRITE_TAC[ASSUME `ul = [u0; u1; u2; u3:real^3]`; OMEGA_LIST_TRUNCATE_1]);
(MATCH_MP_TAC XNHPWAB1);
(EXISTS_TAC `1`);
(ASM_REWRITE_TAC[ARITH_RULE `1 <= 3`]);
(MP_TAC (ASSUME `barV V 3 ul`) THEN REWRITE_TAC[IN;BARV]);
(REPEAT STRIP_TAC);
(REWRITE_TAC[LENGTH;ARITH_RULE `SUC (SUC 0) = 1 + 1`]);
(NEW_GOAL `initial_sublist vl (ul:(real^3)list)`);
(UNDISCH_TAC `initial_sublist vl [u0:real^3; u1]`);
(REWRITE_TAC[INITIAL_SUBLIST] THEN STRIP_TAC);
(EXISTS_TAC `APPEND yl [u2;u3:real^3]`);
(REWRITE_TAC[APPEND_ASSOC; GSYM (ASSUME `[u0:real^3; u1] = APPEND vl yl`)]);
(ASM_REWRITE_TAC[APPEND]);
(ASM_MESON_TAC[]);
(ABBREV_TAC `sl = truncate_simplex 2 (ul:(real^3)list)`);
(MATCH_MP_TAC (REAL_ARITH `hl (sl:(real^3)list) < b /\ a < hl sl ==> a < b`));
(ASM_REWRITE_TAC[]);
(REWRITE_WITH `[u0;u1:real^3] = truncate_simplex 1 sl`);
(EXPAND_TAC "sl" THEN DEL_TAC);
(ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2;TRUNCATE_SIMPLEX_EXPLICIT_1]);
(EXPAND_TAC "sl" THEN REWRITE_TAC[ASSUME
`ul = [u0;u1;u2:real^3;u3]`; TRUNCATE_SIMPLEX_EXPLICIT_2]);
(REWRITE_WITH `hl ([u0;u1;u2:real^3]) =
hl (truncate_simplex 2 (sl:(real^3)list))`);
(AP_TERM_TAC);
(ASM_MESON_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
(REWRITE_WITH `[u0;u1;u2:real^3] = sl`);
(ASM_MESON_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
(NEW_GOAL `!i j. i < j /\ j <= 2
==> hl (truncate_simplex i (sl:(real^3)list))
< hl (truncate_simplex j sl)`);
(MATCH_MP_TAC XNHPWAB4);
(EXISTS_TAC `V:real^3->bool`);
(ASM_REWRITE_TAC[]);
(EXPAND_TAC "sl" THEN REWRITE_TAC[IN]);
(MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
(EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]);
(FIRST_ASSUM MATCH_MP_TAC);
(ARITH_TAC);
(* ================================================================== *)
(NEW_GOAL `p IN convex hull {b, c, u0, u1:real^3}`);
(UP_ASM_TAC THEN UP_ASM_TAC);
(REWRITE_TAC[CONVEX_HULL_4; midpoint; IN; IN_ELIM_THM]);
(REPEAT STRIP_TAC);
(EXISTS_TAC `w:real` THEN EXISTS_TAC `z:real`);
(EXISTS_TAC `u + v * inv (&2)` THEN EXISTS_TAC `v * inv (&2)`);
(ASM_REWRITE_TAC[]);
(NEW_GOAL `&0 <= v * inv (&2)`);
(MATCH_MP_TAC REAL_LE_MUL);
(ASM_REAL_ARITH_TAC);
(ASM_REWRITE_TAC[REAL_ARITH `w + z + (u + v * inv (&2)) + v * inv (&2) =
u + v + w + z`]);
(STRIP_TAC);
(MATCH_MP_TAC REAL_LE_ADD);
(ASM_REWRITE_TAC[]);
(VECTOR_ARITH_TAC);
(NEW_GOAL `convex hull {b, c, u0, u1:real^3} =
convex hull {b, s, u0, u1} UNION convex hull {s, c, u0, u1}`);
(MATCH_MP_TAC CONVEX_HULL_BREAK_KY_LEMMA);
(ASM_REWRITE_TAC[]);
(SWITCH_TAC THEN UP_ASM_TAC THEN ASM_REWRITE_TAC[IN_UNION]);
(NEW_GOAL `~(p IN convex hull {s, c, u0, u1:real^3})`);
(STRIP_TAC);
(NEW_GOAL `p IN aff_ge {u0, u1} {mxi V ul, c:real^3}`);
(NEW_GOAL `convex hull {s, c, u0, u1} SUBSET aff_ge {u0, u1} {s, c:real^3}`);
(REWRITE_WITH `{s, c, u0, u1} = {u0,u1,s, c:real^3}`);
(SET_TAC[]);
(REWRITE_TAC[CONVEX_HULL_4_SUBSET_AFF_GE_2_2]);
(ASM_SET_TAC[]);
(ASM_MESON_TAC[]);
(DISCH_TAC);
(NEW_GOAL `p IN convex hull {b, s, u0, u1:real^3}`);
(ASM_MESON_TAC[]);
(NEW_GOAL `b IN convex hull {u0,u1,u2:real^3}`);
(EXPAND_TAC "b");
(REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`;OMEGA_LIST_TRUNCATE_2]);
(ABBREV_TAC `wl = [u0;u1;u2:real^3]`);
(REWRITE_WITH `{u0, u1, u2:real^3} = set_of_list wl`);
(EXPAND_TAC "wl" THEN REWRITE_TAC[set_of_list]);
(MATCH_MP_TAC XNHPWAB2);
(EXISTS_TAC `2`);
(REWRITE_WITH `wl = truncate_simplex 2 (ul:(real^3)list)`);
(EXPAND_TAC "wl" THEN REWRITE_TAC[ASSUME `ul = [u0; u1; u2; u3:real^3]`]);
(REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
(ASM_REWRITE_TAC[IN]);
(MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
(EXISTS_TAC `3` THEN ASM_MESON_TAC[ARITH_RULE `2 <= 3`]);
(UP_ASM_TAC THEN UP_ASM_TAC);
(REWRITE_TAC[CONVEX_HULL_3; CONVEX_HULL_4; IN; IN_ELIM_THM]);
(REPEAT STRIP_TAC);
(EXISTS_TAC `w + u * u'`);
(EXISTS_TAC `z + u * v'`);
(EXISTS_TAC `u * w'`);
(EXISTS_TAC `v:real`);
(ASM_SIMP_TAC[REAL_LE_ADD; REAL_LE_MUL]);
(STRIP_TAC);
(ASM_REWRITE_TAC[REAL_ARITH `(w + u * u') + (z + u * v') + u * w' + v =
u * (u' + v' + w') + v + w + z`; REAL_MUL_RID]);
(VECTOR_ARITH_TAC);
(NEW_GOAL `F`);
(ASM_MESON_TAC[]);
(ASM_MESON_TAC[])]);;let SLTSTLO2 = prove_by_refinement (
SLTSTLO2_concl,
[(REPEAT STRIP_TAC);
(ABBREV_TAC `B1 = frontier (rogers V (ul:(real^3)list))`);
(ABBREV_TAC `B2 = {w| norm ((w:real^3) - (HD ul)) = sqrt (&2)}`);
(ABBREV_TAC `B3 = rcone_eq (HD (ul:(real^3)list)) (HD (TL ul))
(hl (truncate_simplex 1 ul) / sqrt (&2))`);
(ABBREV_TAC `B4 = affine hull {(HD (ul:(real^3)list)), (HD (TL ul)),
mxi V ul}`);
(ABBREV_TAC `B5 = convex hull {omega_list_n V ul 2,
omega_list_n V (ul:(real^3)list) 3 }`);
(ABBREV_TAC `B6 = affine hull {(HD (ul:(real^3)list)), (HD (TL ul)),
(HD (TL (TL ul)))}`);
(ABBREV_TAC `B7 = affine hull {omega_list_n V ul 1, omega_list_n V ul 2,
omega_list_n V ul 3}`);
(ABBREV_TAC `Z = B1 UNION B2 UNION B3 UNION B4 UNION
(B5:real^3->bool) UNION B6 UNION B7`);
(EXISTS_TAC `Z:real^3->bool`);
(REPEAT STRIP_TAC);
(NEW_GOAL `?u0 u1 u2 u3. (ul:(real^3)list) = [u0:real^3;u1;u2;u3]`);
(MP_TAC (ASSUME `barV V 3 ul`));
(REWRITE_TAC[BARV_3_EXPLICIT]);
(FIRST_X_ASSUM CHOOSE_TAC);
(FIRST_X_ASSUM CHOOSE_TAC);
(FIRST_X_ASSUM CHOOSE_TAC);
(FIRST_X_ASSUM CHOOSE_TAC);
(EXPAND_TAC "Z");
(MATCH_MP_TAC NEGLIGIBLE_UNION);
(STRIP_TAC);
(EXPAND_TAC "B1" THEN MATCH_MP_TAC NEGLIGIBLE_CONVEX_FRONTIER);
(ASM_SIMP_TAC[ROGERS_EXPLICIT;CONVEX_CONVEX_HULL]);
(MATCH_MP_TAC NEGLIGIBLE_UNION);
(STRIP_TAC);
(* revised 2013-05-25: *)
(NEW_GOAL `(?(v:real^3)(r:real). (r> &0)/\ (B2 ={w:real^3 | norm (w-v)= r}))`);
(EXPAND_TAC "B2");
(EXISTS_TAC `(HD ul):real^3` THEN EXISTS_TAC `sqrt(&2)`);
(ASM_REWRITE_TAC[REAL_ARITH `a > &0 <=> &0 < a`]);
(MATCH_MP_TAC SQRT_POS_LT);
(REAL_ARITH_TAC);
(ASM_SIMP_TAC[NULLSET_SPHERE]);
(* end of revision *)
(MATCH_MP_TAC NEGLIGIBLE_UNION);
(STRIP_TAC);
(EXPAND_TAC "B3");
(MATCH_MP_TAC NEGLIGIBLE_RCONE_EQ);
(ASM_REWRITE_TAC[HD;TL]);
(STRIP_TAC);
(NEW_GOAL `aff_dim (set_of_list [u0;u1:real^3]) = &0`);
(ASM_REWRITE_TAC[set_of_list; SET_RULE `{x, x} = {x}`; AFF_DIM_SING]);
(NEW_GOAL `aff_dim (set_of_list [u0;u1:real^3]) = &1`);
(MATCH_MP_TAC MHFTTZN1);
(EXISTS_TAC `V:real^3->bool`);
(ASM_REWRITE_TAC[]);
(REWRITE_WITH `[u0; u0:real^3] = truncate_simplex 1 ul`);
(ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);
(MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
(EXISTS_TAC `3`);
(ASM_REWRITE_TAC[]);
(ARITH_TAC);
(NEW_GOAL `&0 = &1`);
(ASM_MESON_TAC[INT_OF_NUM_EQ;REAL_OF_NUM_EQ]);
(UP_ASM_TAC THEN REAL_ARITH_TAC);
(MATCH_MP_TAC NEGLIGIBLE_UNION);
(STRIP_TAC);
(EXPAND_TAC "B4");
(REWRITE_TAC[NEGLIGIBLE_AFFINE_HULL_3]);
(MATCH_MP_TAC NEGLIGIBLE_UNION);
(STRIP_TAC);
(EXPAND_TAC "B5");
(ONCE_REWRITE_TAC[SET_RULE `{a,b:real^3} = {a,a,b}`]);
(MESON_TAC[NEGLIGIBLE_CONVEX_HULL_3]);
(MATCH_MP_TAC NEGLIGIBLE_UNION);
(STRIP_TAC);
(EXPAND_TAC "B6");
(REWRITE_TAC[NEGLIGIBLE_AFFINE_HULL_3]);
(EXPAND_TAC "B7");
(REWRITE_TAC[NEGLIGIBLE_AFFINE_HULL_3]);
(* ========================================================================= *)
(NEW_GOAL `?u0 u1 u2 u3. (ul:(real^3)list) = [u0:real^3;u1;u2;u3]`);
(MP_TAC (ASSUME `barV V 3 ul`));
(REWRITE_TAC[BARV_3_EXPLICIT]);
(FIRST_X_ASSUM CHOOSE_TAC);
(FIRST_X_ASSUM CHOOSE_TAC);
(FIRST_X_ASSUM CHOOSE_TAC);
(FIRST_X_ASSUM CHOOSE_TAC);
(REWRITE_TAC[EXISTS_UNIQUE]);
(NEW_GOAL `?i. i <= 4 /\ p IN mcell i V ul`);
(MATCH_MP_TAC SLTSTLO1);
(ASM_REWRITE_TAC[]);
(ASM_SET_TAC[]);
(FIRST_X_ASSUM CHOOSE_TAC THEN EXISTS_TAC `i:num`);
(STRIP_TAC);
(ASM_REWRITE_TAC[]);
(* ========================================================================= *)
(ASM_CASES_TAC `hl (ul:(real^3)list) < sqrt(&2)`);
(NEW_GOAL ` mcell0 V ul = {} /\ mcell1 V ul = {} /\
mcell2 V ul = {} /\ mcell3 V ul = {}`);
(ASM_MESON_TAC[EMNWUUS2]);
(UP_ASM_TAC THEN ASM_REWRITE_TAC[] THEN DISCH_TAC);
(NEW_GOAL `!y. y <= 4 /\ p IN mcell y V ul ==>
~ (y = 0 \/ y = 1 \/ y = 2 \/ y = 3)`);
(REPEAT STRIP_TAC);
(UNDISCH_TAC `p IN mcell y V ul` THEN ASM_REWRITE_TAC[MCELL_EXPLICIT]);
(SET_TAC[]);
(UNDISCH_TAC `p IN mcell y V ul` THEN ASM_REWRITE_TAC[MCELL_EXPLICIT]);
(SET_TAC[]);
(UNDISCH_TAC `p IN mcell y V ul` THEN ASM_REWRITE_TAC[MCELL_EXPLICIT]);
(SET_TAC[]);
(UNDISCH_TAC `p IN mcell y V ul` THEN ASM_REWRITE_TAC[MCELL_EXPLICIT]);
(SET_TAC[]);
(NEW_GOAL `!y. y <= 4 /\ p IN mcell y V ul ==> y = 4`);
(GEN_TAC THEN DISCH_TAC);
(NEW_GOAL `~(y = 0 \/ y = 1 \/ y = 2 \/ y = 3)`);
(ASM_SIMP_TAC[]);
(ASM_ARITH_TAC);
(GEN_TAC THEN DISCH_TAC);
(NEW_GOAL `y = 4`);
(ASM_MESON_TAC[]);
(NEW_GOAL `i = 4`);
(ASM_MESON_TAC[]);
(ASM_MESON_TAC[]);
(NEW_GOAL `sqrt (&2) <= hl (ul:(real^3)list)`);
(UP_ASM_TAC THEN REAL_ARITH_TAC);
(* ========================================================================= *)
(ASM_CASES_TAC `dist(u0:real^3, p) >= sqrt(&2)`);
(NEW_GOAL `!y. y <= 4 /\ p IN mcell y V ul ==>
~ (y = 4 \/ y = 1 \/ y = 2 \/ y = 3)`);
(REPEAT STRIP_TAC);
(NEW_GOAL `mcell 4 V ul = {}`);
(SIMP_TAC[MCELL_EXPLICIT; ARITH_RULE `4 >= 4`;mcell4]);
(COND_CASES_TAC);
(NEW_GOAL `F`);
(ASM_MESON_TAC[]);
(ASM_MESON_TAC[]);
(REFL_TAC);
(UNDISCH_TAC `p IN mcell y V ul` THEN REWRITE_TAC[ASSUME `y = 4`]);
(REWRITE_TAC[ASSUME `mcell 4 V ul = {}`]);
(SET_TAC[]);
(UNDISCH_TAC `p IN mcell y V ul` THEN REWRITE_TAC[ASSUME `y = 1`;
MCELL_EXPLICIT;mcell1]);
(COND_CASES_TAC);
(STRIP_TAC);
(NEW_GOAL `~(p:real^3 IN B2)`);
(UNDISCH_TAC `p IN rogers V ul DIFF Z` THEN REWRITE_TAC[IN_DIFF]);
(EXPAND_TAC "Z" THEN REWRITE_TAC[IN_UNION]);
(SET_TAC[]);
(NEW_GOAL `p:real^3 IN cball (HD ul,sqrt (&2))`);
(ASM_SET_TAC[IN_DIFF;IN_INTER]);
(NEW_GOAL `~(p:real^3 IN B2 UNION ball (HD ul,sqrt (&2)))`);
(ASM_REWRITE_TAC[IN_UNION;HD;ball;IN;IN_ELIM_THM]);
(ASM_REAL_ARITH_TAC);
(UP_ASM_TAC THEN REWRITE_WITH `B2 UNION ball (HD ul,sqrt (&2)) =
cball (HD (ul:(real^3)list),sqrt (&2))`);
(EXPAND_TAC "B2");
(REWRITE_TAC[SET_EQ_LEMMA; IN_UNION; cball; ball;IN;IN_ELIM_THM]);
(ONCE_REWRITE_TAC[DIST_SYM]);
(REWRITE_TAC[dist] THEN REAL_ARITH_TAC);
(ASM_REWRITE_TAC[]);
(SET_TAC[]);
(UNDISCH_TAC `p IN mcell y V ul` THEN REWRITE_TAC[ASSUME `y = 2`;
MCELL_EXPLICIT;mcell2]);
(COND_CASES_TAC);
(LET_TAC);
(ASM_REWRITE_TAC[HD;TL] THEN STRIP_TAC);
(NEW_GOAL `p:real^3 IN (rcone_ge u0 u1 a INTER rcone_ge u1 u0 a)`);
(ASM_SET_TAC[IN_INTER]);
(UP_ASM_TAC THEN REWRITE_TAC[IN_INTER;rcone_ge;rconesgn;IN;IN_ELIM_THM]);
(REPEAT STRIP_TAC);
(NEW_GOAL `(p - u0) dot (u1 - u0:real^3) + (p - u1) dot (u0 - u1) >=
dist (p,u0) * dist (u1,u0) * a + dist (p,u1) * dist (u0,u1) * a`);
(ASM_REAL_ARITH_TAC);
(UP_ASM_TAC THEN REWRITE_TAC[DIST_SYM]);
(REWRITE_WITH `(p - u0) dot (u1 - u0:real^3) + (p - u1) dot (u0 - u1) =
(u0 - u1) dot (u0 - u1)`);
(VECTOR_ARITH_TAC);
(REWRITE_TAC[REAL_ARITH `x * a * b + y * a * b = (x + y) * a * b`;
GSYM NORM_POW_2; GSYM dist]);
(* ========================================================================== *)
(NEW_GOAL `dist (p,u0:real^3) <= dist (p,u1) /\ a = (inv(&2) * dist (u0,u1)) / sqrt (&2)`);
(REPEAT STRIP_TAC);
(NEW_GOAL `p IN rogers V ul`);
(ASM_SET_TAC[IN_DIFF]);
(NEW_GOAL `(p:real^3) IN voronoi_closed V u0`);
(NEW_GOAL `(p:real^3) IN voronoi_closed V u0 <=>
(?vl. vl IN barV V 3 /\
p IN rogers V vl /\
truncate_simplex 0 vl = [u0:real^3])`);
(MATCH_MP_TAC GLTVHUM);
(ASM_REWRITE_TAC[]);
(MATCH_MP_TAC BARV_IMP_u0_IN_V);
(EXISTS_TAC `ul:(real^3)list`);
(EXISTS_TAC `u1:real^3`);
(EXISTS_TAC `u2:real^3`);
(EXISTS_TAC `u3:real^3`);
(ASM_REWRITE_TAC[]);
(ASM_REWRITE_TAC[]);
(EXISTS_TAC `ul:(real^3)list`);
(ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_0]);
(ASM_SET_TAC[]);
(UP_ASM_TAC THEN REWRITE_TAC[voronoi_closed;IN;IN_ELIM_THM]);
(DISCH_TAC THEN FIRST_ASSUM MATCH_MP_TAC);
(NEW_GOAL `set_of_list (ul:(real^3)list) SUBSET V`);
(MATCH_MP_TAC Packing3.BARV_SUBSET);
(EXISTS_TAC `3` THEN ASM_MESON_TAC[]);
(UP_ASM_TAC THEN ASM_REWRITE_TAC[set_of_list]);
(SET_TAC[]);
(EXPAND_TAC "a");
(AP_THM_TAC);
(AP_TERM_TAC);
(REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`; TRUNCATE_SIMPLEX_EXPLICIT_1; HL;set_of_list]);
(NEW_GOAL `!w. w IN {u0,u1:real^3} ==>
radV {u0,u1} = dist (circumcenter {u0,u1},w)`);
(MATCH_MP_TAC Rogers.OAPVION2);
(REWRITE_TAC[AFFINE_INDEPENDENT_IFF_CARD]);
(STRIP_TAC);
(REWRITE_TAC[Geomdetail.FINITE6]);
(NEW_GOAL `aff_dim {u0, u1:real^3} = &1`);
(ABBREV_TAC `vl = [u0;u1:real^3]`);
(REWRITE_WITH `{u0, u1:real^3} = set_of_list vl`);
(EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]);
(MATCH_MP_TAC Rogers.MHFTTZN1);
(EXISTS_TAC `V:real^3->bool`);
(ASM_REWRITE_TAC[]);
(REWRITE_WITH `vl = truncate_simplex 1 ul:(real^3)list`);
(EXPAND_TAC "vl" THEN DEL_TAC);
(ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);
(MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
(EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]);
(ARITH_TAC);
(ASM_REWRITE_TAC[]);
(ONCE_REWRITE_TAC[ARITH_RULE
`&1 = &(CARD {u0, u1:real^3}) - (&1):int
<=> &(CARD {u0, u1:real^3}) = (&2):int`]);
(ONCE_REWRITE_TAC[INT_OF_NUM_EQ]);
(REWRITE_TAC[Geomdetail.CARD2]);
(REPEAT STRIP_TAC);
(NEW_GOAL `CARD {u0, u1:real^3} = 1`);
(REWRITE_WITH `{u0, u1} = {u1:real^3}`);
(ASM_SET_TAC[]);
(REWRITE_TAC[Geomdetail.CARD_SING]);
(NEW_GOAL `aff_dim {u0, u1} <= &(CARD {u0, u1:real^3}) - (&1):int`);
(MATCH_MP_TAC AFF_DIM_LE_CARD);
(REWRITE_TAC[Geomdetail.FINITE6]);
(NEW_GOAL `(&2):int <= &(CARD {u0, u1:real^3})`);
(ONCE_REWRITE_TAC[ARITH_RULE
`(&2):int <= &(CARD {u0, u1:real^3}) <=>
&1 <= &(CARD {u0, u1:real^3}) - (&1):int`]);
(ASM_MESON_TAC[]);
(NEW_GOAL `&(CARD {u0, u1:real^3}) <= (&2):int`);
(ONCE_REWRITE_TAC[INT_OF_NUM_LE]);
(REWRITE_TAC[Geomdetail.CARD2]);
(NEW_GOAL `CARD {u0, u1:real^3} = 2`);
(ONCE_REWRITE_TAC[GSYM INT_OF_NUM_EQ]);
(ASM_ARITH_TAC);
(ASM_ARITH_TAC);
(REWRITE_WITH `radV {u0, u1} = dist (circumcenter {u0, u1},u0:real^3)`);
(FIRST_X_ASSUM MATCH_MP_TAC);
(TRUONG_SET_TAC[]);
(REWRITE_TAC[CIRCUMCENTER_2;midpoint;dist;
VECTOR_ARITH `inv (&2) % (u0 + u1) - u0 = inv (&2) % (u1 - u0)`]);
(REWRITE_TAC[NORM_MUL]);
(REWRITE_WITH `abs (inv (&2)) = inv (&2)`);
(REWRITE_TAC[REAL_ABS_REFL]);
(REAL_ARITH_TAC);
(REWRITE_TAC[GSYM dist]);
(MESON_TAC[DIST_SYM]);
(UP_ASM_TAC THEN REPEAT STRIP_TAC);
(NEW_GOAL `(dist (p,u0) + dist (p,u1:real^3)) * dist (u0,u1) * a >=
(&2 * dist (p,u0)) * dist (u0,u1) * a`);
(REWRITE_TAC[REAL_ARITH `(x + y) * a * b >= (&2 * x) * a * b <=>
&0 <= (y - x) * a * b`]);
(MATCH_MP_TAC REAL_LE_MUL);
(STRIP_TAC);
(ASM_REAL_ARITH_TAC);
(MATCH_MP_TAC REAL_LE_MUL);
(STRIP_TAC);
(REWRITE_TAC[DIST_POS_LE]);
(ASM_REWRITE_TAC[]);
(MATCH_MP_TAC REAL_LE_DIV);
(STRIP_TAC);
(MATCH_MP_TAC REAL_LE_MUL);
(STRIP_TAC);
(REAL_ARITH_TAC);
(REWRITE_TAC[DIST_POS_LE]);
(MATCH_MP_TAC SQRT_POS_LE);
(REAL_ARITH_TAC);
(NEW_GOAL `dist (u0,u1:real^3) pow 2 >= (&2 * dist (p,u0)) * dist (u0,u1) * a `);
(ASM_REAL_ARITH_TAC);
(UP_ASM_TAC THEN ASM_REWRITE_TAC[]);
(REWRITE_TAC[REAL_ARITH `(&2 * x) * a * (inv(&2) * a) / b = (x / b) * a pow 2`]);
(REWRITE_TAC[REAL_ARITH `a >= x * a <=> &0 <= a * (&1 - x)`]);
(DISCH_TAC);
(NEW_GOAL `&0 <= dist (u0,u1) pow 2 * (&1 - dist (p,u0) / sqrt (&2))
<=> &0 <= (&1 - dist (p,u0:real^3) / sqrt (&2))`);
(NEW_GOAL `&0 < dist (u0,u1:real^3) pow 2`);
(REWRITE_TAC[GSYM Trigonometry2.NOT_ZERO_EQ_POW2_LT; DIST_EQ_0]);
(STRIP_TAC);
(NEW_GOAL `aff_dim {u0, u1:real^3} = &1`);
(ABBREV_TAC `vl = [u0;u1:real^3]`);
(REWRITE_WITH `{u0, u1:real^3} = set_of_list vl`);
(EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]);
(MATCH_MP_TAC Rogers.MHFTTZN1);
(EXISTS_TAC `V:real^3->bool`);
(ASM_REWRITE_TAC[]);
(REWRITE_WITH `vl = truncate_simplex 1 ul:(real^3)list`);
(EXPAND_TAC "vl" THEN DEL_TAC);
(ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);
(MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
(EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]);
(ARITH_TAC);
(NEW_GOAL `CARD {u0, u1:real^3} = 1`);
(REWRITE_WITH `{u0, u1} = {u1:real^3}`);
(ASM_SET_TAC[]);
(REWRITE_TAC[Geomdetail.CARD_SING]);
(NEW_GOAL `aff_dim {u0, u1} <= &(CARD {u0, u1:real^3}) - (&1):int`);
(MATCH_MP_TAC AFF_DIM_LE_CARD);
(REWRITE_TAC[Geomdetail.FINITE6]);
(UP_ASM_TAC THEN ASM_REWRITE_TAC[]);
(ASM_ARITH_TAC);
(ASM_MESON_TAC[REAL_LE_MUL_EQ]);
(NEW_GOAL `&0 <= &1 - dist (p,u0:real^3) / sqrt (&2)`);
(ASM_MESON_TAC[]);
(UP_ASM_TAC THEN REWRITE_TAC[REAL_ARITH `&0 <= a - b <=> b <= a`]);
(REWRITE_WITH `dist (p,u0:real^3) / sqrt (&2) <= &1
<=> dist (p,u0) <= &1 * sqrt (&2)`);
(MATCH_MP_TAC REAL_LE_LDIV_EQ);
(MATCH_MP_TAC SQRT_POS_LT);
(REAL_ARITH_TAC);
(REWRITE_TAC [REAL_MUL_LID]);
(STRIP_TAC);
(NEW_GOAL `dist (p, u0:real^3) = sqrt (&2)`);
(UP_ASM_TAC THEN ONCE_REWRITE_TAC[DIST_SYM]);
(ASM_REAL_ARITH_TAC);
(NEW_GOAL `~(p:real^3 IN B2)`);
(ASM_SET_TAC[IN_DIFF]);
(UP_ASM_TAC THEN EXPAND_TAC "B2" THEN REWRITE_TAC[IN;IN_ELIM_THM]);
(ASM_REWRITE_TAC[HD;GSYM dist]);
(SET_TAC[]);
(* ========================================================================= *)
(UNDISCH_TAC `p IN mcell y V ul` THEN REWRITE_TAC[ASSUME `y = 3`;
MCELL_EXPLICIT;mcell3]);
(COND_CASES_TAC);
(ASM_REWRITE_TAC[HD;TL;set_of_list]);
(NEW_GOAL `(?s. between s (omega_list_n V ul 2,omega_list_n V ul 3) /\
dist (u0,s) = sqrt (&2) /\
mxi V ul = s:real^3)`);
(MATCH_MP_TAC MXI_EXPLICIT_OLD);
(ASM_REWRITE_TAC[]);
(FIRST_X_ASSUM CHOOSE_TAC);
(UP_ASM_TAC THEN ASM_REWRITE_TAC[] THEN REPEAT STRIP_TAC);
(UP_ASM_TAC THEN ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2;set_of_list]);
(REWRITE_TAC[SET_RULE `{a,b,c} UNION {d} = {a,b,c,d}`]);
(STRIP_TAC);
(SUBGOAL_THEN `p:real^3 IN rogers V ul` MP_TAC);
(ASM_SET_TAC[IN_DIFF]);
(ASM_SIMP_TAC[ROGERS_EXPLICIT; HD]);
(ABBREV_TAC `s1 = omega_list_n V [u0; u1; u2; u3:real^3] 1`);
(ABBREV_TAC `s2 = omega_list_n V [u0; u1; u2; u3:real^3] 2`);
(ABBREV_TAC `s3 = omega_list_n V [u0; u1; u2; u3:real^3] 3`);
(STRIP_TAC);
(NEW_GOAL `?m n:real^3.
between p (m,n) /\ between m (u0,s1) /\ between n (s2,s3)`);
(ASM_SIMP_TAC[CONVEX_HULL_4_IMP_2_2]);
(UP_ASM_TAC THEN REPEAT STRIP_TAC);
(NEW_GOAL `between (p - m:real^3) (vec 0, n - m)`);
(UNDISCH_TAC `between p (m,n:real^3)` THEN REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;
CONVEX_HULL_2;IN;IN_ELIM_THM] THEN REPEAT STRIP_TAC);
(EXISTS_TAC `u:real` THEN EXISTS_TAC `v:real` THEN ASM_REWRITE_TAC[]);
(REWRITE_WITH `(u % m + v % n) - m:real^3 = (u % m + v % n) - (u + v) % m`);
(ASM_REWRITE_TAC[] THEN VECTOR_ARITH_TAC);
(VECTOR_ARITH_TAC);
(NEW_GOAL `between (proj_point (s2 - m) (p - m:real^3))
(vec 0, proj_point (s2 - m) (n - m))`);
(REWRITE_WITH `vec 0 = proj_point (s2 - m) (m - m:real^3)`);
(REWRITE_TAC[VECTOR_SUB_REFL; PRO_EXP; DOT_LZERO; REAL_ARITH `&0 / a = &0`]);
(VECTOR_ARITH_TAC);
(MATCH_MP_TAC BETWEEN_PROJ_POINT);
(ASM_REWRITE_TAC[VECTOR_SUB_REFL]);
(ABBREV_TAC `p' = proj_point (s2 - m) (p - m:real^3)`);
(ABBREV_TAC `n' = proj_point (s2 - m) (n - m:real^3)`);
(* ============================================================================ *)
(ABBREV_TAC `vl = [u0;u1;u2:real^3]`);
(NEW_GOAL `s2:real^3 = circumcenter (set_of_list vl)`);
(EXPAND_TAC "s2" THEN EXPAND_TAC "vl");
(REWRITE_TAC[OMEGA_LIST_TRUNCATE_2]);
(MATCH_MP_TAC XNHPWAB1);
(EXISTS_TAC `2`);
(REWRITE_WITH `[u0; u1; u2:real^3] = truncate_simplex 2 ul`);
(ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
(ASM_REWRITE_TAC[IN]);
(MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
(EXISTS_TAC `3`);
(ASM_MESON_TAC[ARITH_RULE `2 <= 3`]);
(NEW_GOAL `s3 IN voronoi_list V (truncate_simplex 2 (ul:(real^3)list))`);
(NEW_GOAL `s3 IN voronoi_list V (truncate_simplex (SUC 2)
[u0:real^3; u1; u2; u3])`);
(EXPAND_TAC "s3");
(REWRITE_TAC[OMEGA_LIST_N;ARITH_RULE `3 = SUC 2`]);
(MATCH_MP_TAC CLOSEST_POINT_IN_SET);
(REWRITE_TAC[Packing3.CLOSED_VORONOI_LIST]);
(MATCH_MP_TAC Packing3.BARV_IMP_VORONOI_LIST_NOT_EMPTY);
(EXISTS_TAC `3`);
(REWRITE_WITH `truncate_simplex (SUC 2) [u0; u1; u2; u3:real^3] = ul`);
(ASM_REWRITE_TAC[ARITH_RULE `SUC 2 = 3`; TRUNCATE_SIMPLEX_EXPLICIT_3]);
(ASM_MESON_TAC[]);
(UP_ASM_TAC);
(REWRITE_WITH `truncate_simplex (SUC 2) [u0; u1; u2; u3:real^3] = ul`);
(ASM_REWRITE_TAC[ARITH_RULE `SUC 2 = 3`; TRUNCATE_SIMPLEX_EXPLICIT_3]);
(STRIP_TAC);
(NEW_GOAL `voronoi_list V (ul:(real^3)list) SUBSET
voronoi_list V (truncate_simplex 2 ul)`);
(ASM_REWRITE_TAC[VORONOI_LIST;VORONOI_SET; SUBSET;
TRUNCATE_SIMPLEX_EXPLICIT_2; set_of_list; IN_INTERS]);
(EXPAND_TAC "vl" THEN REWRITE_TAC[IN; IN_ELIM_THM;set_of_list]
THEN REPEAT STRIP_TAC);
(FIRST_ASSUM MATCH_MP_TAC);
(EXISTS_TAC `v:real^3`);
(ASM_REWRITE_TAC[]);
(SWITCH_TAC THEN UP_ASM_TAC THEN TRUONG_SET_TAC[]);
(UP_ASM_TAC THEN UP_ASM_TAC THEN SET_TAC[SUBSET]);
(NEW_GOAL `n' = s2:real^3 - m`);
(EXPAND_TAC "n'");
(UNDISCH_TAC `between n (s2,s3:real^3)` THEN REWRITE_TAC[
BETWEEN_IN_CONVEX_HULL;CONVEX_HULL_2;IN;IN_ELIM_THM] THEN REPEAT STRIP_TAC);
(REWRITE_TAC[ASSUME `n:real^3 = u % s2 + v % s3`]);
(REWRITE_WITH `(u % s2 + v % s3) - m:real^3 = (s2 - m) + v % (s3 - s2)`);
(REWRITE_TAC[VECTOR_ARITH `(u % s2 + v % s3) - m = s2 - m + v % (s3 - s2)
<=> (u + v) % s2 = s2`]);
(ASM_REWRITE_TAC[VECTOR_MUL_LID]);
(REWRITE_TAC[PRO_EXP]);
(REWRITE_WITH `((s2 - m + v % (s3 - s2)) dot (s2 - m)) /
((s2 - m) dot (s2 - m:real^3)) = &1`);
(REWRITE_TAC[DOT_LADD; REAL_ARITH `(a + b) / c = a / c + b / c`]);
(REWRITE_WITH `((s2 - m) dot (s2 - m)) / ((s2 - m) dot (s2 - m:real^3)) = &1`);
(MATCH_MP_TAC REAL_DIV_REFL);
(REWRITE_TAC[GSYM NORM_POW_2; Trigonometry2.POW2_EQ_0;NORM_EQ_0]);
(REWRITE_TAC[VECTOR_ARITH `s2 - m = vec 0 <=> s2 = m`]);
(STRIP_TAC);
(NEW_GOAL `between s2 (u0, s1:real^3)`);
(ASM_MESON_TAC[]);
(NEW_GOAL `s2 IN affine hull {u0, s1:real^3}`);
(UP_ASM_TAC THEN REWRITE_TAC[BETWEEN_IN_CONVEX_HULL]);
(STRIP_TAC);
(NEW_GOAL `convex hull {u0,s1:real^3} SUBSET affine hull {u0,s1}`);
(REWRITE_TAC[CONVEX_HULL_SUBSET_AFFINE_HULL]);
(UP_ASM_TAC THEN UP_ASM_TAC THEN SET_TAC[]);
(NEW_GOAL `affine hull {u0,s1,s2} = affine hull {u0, s1:real^3}`);
(MATCH_MP_TAC AFFINE_HULLS_EQ);
(REWRITE_TAC[SUBSET; SET_RULE `x IN {a,b,c} <=> x = a \/ x = b \/ x = c`]);
(REPEAT STRIP_TAC);
(ASM_REWRITE_TAC[Trigonometry2.UV_IN_AFF2]);
(ASM_REWRITE_TAC[Trigonometry2.UV_IN_AFF2]);
(ASM_MESON_TAC[]);
(UP_ASM_TAC);
(REWRITE_TAC[SUBSET; SET_RULE `x IN {b,c} <=> x = b \/ x = c`]);
(REPEAT STRIP_TAC);
(ASM_REWRITE_TAC[AFFINE_HULL_3;IN;IN_ELIM_THM]);
(EXISTS_TAC `&1` THEN EXISTS_TAC `&0` THEN EXISTS_TAC `&0`);
(STRIP_TAC);
(REAL_ARITH_TAC);
(VECTOR_ARITH_TAC);
(ASM_REWRITE_TAC[AFFINE_HULL_3;IN;IN_ELIM_THM]);
(EXISTS_TAC `&0` THEN EXISTS_TAC `&1` THEN EXISTS_TAC `&0`);
(STRIP_TAC);
(REAL_ARITH_TAC);
(VECTOR_ARITH_TAC);
(NEW_GOAL `aff_dim {u0,s1,s2:real^3} <= &1`);
(ONCE_REWRITE_TAC[GSYM AFF_DIM_AFFINE_HULL]);
(ONCE_ASM_REWRITE_TAC[]);
(ONCE_REWRITE_TAC[AFF_DIM_AFFINE_HULL]);
(MATCH_MP_TAC (ARITH_RULE `(?x. x <= &1 /\ y <= x:int) ==> y <= &1`));
(EXISTS_TAC `&(CARD {u0,s1:real^3}):int - &1`);
(STRIP_TAC);
(REWRITE_TAC[ARITH_RULE `a:int - &1 <= &1 <=> a <= &2`; INT_OF_NUM_LE]);
(REWRITE_TAC[Geomdetail.CARD2]);
(MATCH_MP_TAC AFF_DIM_LE_CARD);
(REWRITE_TAC[Geomdetail.FINITE6]);
(NEW_GOAL `aff_dim {u0,s1,s2:real^3} = &2`);
(NEW_GOAL `vl:(real^3)list = truncate_simplex 2 ul`);
(EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
(REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
(REWRITE_WITH `aff_dim {u0,s1,s2:real^3} =
aff_dim {omega_list_n V vl j | j IN 0..2}`);
(AP_TERM_TAC);
(REWRITE_TAC[IN_NUMSEG_0]);
(REWRITE_TAC[SET_EQ_LEMMA;
SET_RULE `x IN {a,b,c} <=> (x = a \/ x = b \/ x = c)`; IN;IN_ELIM_THM]);
(REPEAT STRIP_TAC);
(EXISTS_TAC `0`);
(REWRITE_TAC[ARITH_RULE `0 <= 2`; OMEGA_LIST_N]);
(EXPAND_TAC "vl" THEN REWRITE_TAC[HD]);
(ASM_REWRITE_TAC[]);
(EXISTS_TAC `1`);
(ASM_REWRITE_TAC[ARITH_RULE `1 <= 2`]);
(EXPAND_TAC "vl");
(REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
(DEL_TAC);
(EXPAND_TAC "s1");
(REWRITE_TAC[OMEGA_LIST_TRUNCATE_1; OMEGA_LIST_TRUNCATE_1_NEW1]);
(EXISTS_TAC `2`);
(REWRITE_TAC[ARITH_RULE `2 <= 2`; ASSUME `x = s2:real^3`] THEN EXPAND_TAC "vl" THEN DEL_TAC);
(EXPAND_TAC "s2");
(REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2; HD]);
(REWRITE_TAC[set_of_list; OMEGA_LIST_TRUNCATE_2;
OMEGA_LIST_TRUNCATE_2_NEW1]);
(ASM_CASES_TAC `j = 0`);
(DISJ1_TAC);
(REWRITE_TAC[ASSUME `x:real^3 = omega_list_n V vl j`; OMEGA_LIST_N; HD]);
(EXPAND_TAC "vl");
(REWRITE_TAC[ASSUME `j = 0`]);
(REWRITE_TAC[OMEGA_LIST_N; HD]);
(ASM_CASES_TAC `j = 1`);
(DISJ2_TAC);
(DISJ1_TAC);
(ASM_REWRITE_TAC[]);
(REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2; HD]);
(EXPAND_TAC "s1");
(REWRITE_TAC[OMEGA_LIST_TRUNCATE_1; OMEGA_LIST_TRUNCATE_1_NEW1]);
(ASM_CASES_TAC `j = 2`);
(DISJ2_TAC);
(DISJ2_TAC);
(REWRITE_TAC[ASSUME `x:real^3 = omega_list_n V vl j`]);
(EXPAND_TAC "vl");
(EXPAND_TAC "s2");
(REWRITE_TAC[ASSUME `j = 2`; OMEGA_LIST_TRUNCATE_2; OMEGA_LIST_TRUNCATE_2_NEW1]);
(SUBGOAL_THEN `F` MP_TAC);
(ASM_ARITH_TAC);
(MESON_TAC[]);
(MATCH_MP_TAC XNHPWAB3);
(ASM_REWRITE_TAC[IN]);
STRIP_TAC;
(MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
(EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]);
(ASM_MESON_TAC[]);
(ASM_MESON_TAC[]);
(ASM_ARITH_TAC);
(* ========================================================================= *)
(* ========================================================================== *)
(MATCH_MP_TAC (REAL_ARITH `x = &0 ==> a + x = a`));
(REWRITE_TAC[DOT_LMUL]);
(REWRITE_WITH `(s3 - s2) dot (s2 - m:real^3) = &0`);
(ONCE_REWRITE_TAC[VECTOR_ARITH `a dot (b - c) = -- (a dot (c - b))`]);
(ONCE_REWRITE_TAC[REAL_ARITH `--a = &0 <=> a = &0`]);
(REWRITE_TAC[ASSUME `s2:real^3 = circumcenter (set_of_list vl)`]);
(MATCH_MP_TAC MHFTTZN4);
(EXISTS_TAC `V:real^3->bool`);
(EXISTS_TAC `2`);
(REWRITE_WITH `vl:(real^3)list = truncate_simplex 2 ul`);
(EXPAND_TAC "vl" THEN DEL_TAC);
(ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
(REPEAT STRIP_TAC);
(ASM_REWRITE_TAC[]);
(MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
(EXISTS_TAC `3`);
(ASM_MESON_TAC[ARITH_RULE `2 <= 3`]);
(* ========================================================================== *)
(MATCH_MP_TAC IN_AFFINE_KY_LEMMA1);
(ASM_REWRITE_TAC[]);
(ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2; set_of_list]);
(EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]);
(UNDISCH_TAC `between m (u0,s1:real^3)`);
(REWRITE_WITH `s1 = midpoint (u0,u1:real^3)`);
(EXPAND_TAC "s1");
(REWRITE_WITH `omega_list_n V [u0; u1; u2; u3] 1 =
omega_list_n V [u0; u1:real^3] 1`);
(REWRITE_TAC[OMEGA_LIST_TRUNCATE_1_NEW2;OMEGA_LIST_TRUNCATE_1]);
(REWRITE_TAC[OMEGA_LIST_TRUNCATE_1_NEW2]);
(REWRITE_WITH `omega_list V [u0; u1:real^3] =
circumcenter (set_of_list [u0;u1])`);
(MATCH_MP_TAC XNHPWAB1);
(EXISTS_TAC `1`);
(ASM_REWRITE_TAC[ARITH_RULE `1 <= 3`]);
(REWRITE_WITH `[u0;u1:real^3] = truncate_simplex 1 vl`);
(EXPAND_TAC "vl" THEN REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);
(REWRITE_TAC[IN] THEN STRIP_TAC);
(MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
(EXISTS_TAC `2` THEN REWRITE_TAC[ARITH_RULE `1 <= 2`]);
(REWRITE_WITH `vl = truncate_simplex 2 ul:(real^3)list`);
(EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
(REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
(MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
(EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]);
(NEW_GOAL `!i j. i < j /\ j <= 2
==> hl (truncate_simplex i (vl:(real^3)list))
< hl (truncate_simplex j vl)`);
(MATCH_MP_TAC XNHPWAB4);
(EXISTS_TAC `V:real^3->bool`);
(ASM_REWRITE_TAC[IN]);
(REWRITE_WITH `vl = truncate_simplex 2 ul:(real^3)list`);
(EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
(REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
(ASM_REWRITE_TAC[]);
(MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
(EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]);
(ASM_MESON_TAC[]);
(NEW_GOAL `hl (truncate_simplex 1 (vl:(real^3)list)) < hl (truncate_simplex 2 vl)`);
(FIRST_X_ASSUM MATCH_MP_TAC);
(ARITH_TAC);
(NEW_GOAL `truncate_simplex 2 vl = truncate_simplex 2 ul:(real^3)list`);
(EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
(REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
(MATCH_MP_TAC (REAL_ARITH `a < hl (truncate_simplex 2 (vl:(real^3)list)) /\
hl (truncate_simplex 2 vl) < b ==> a < b`));
(ASM_REWRITE_TAC[]);
(ASM_MESON_TAC[]);
(REWRITE_TAC[set_of_list;Rogers.CIRCUMCENTER_2]);
(REWRITE_TAC[BETWEEN_IN_CONVEX_HULL; CONVEX_HULL_2; midpoint; IN; IN_ELIM_THM; AFFINE_HULL_3]);
(REPEAT STRIP_TAC);
(EXISTS_TAC `u' + v' * inv (&2)`);
(EXISTS_TAC `v' * inv (&2)`);
(EXISTS_TAC `&0`);
(STRIP_TAC);
(REWRITE_TAC[REAL_ARITH `(u' + v' * inv (&2)) + v' * inv (&2) + &0 = u' + v'`]);
(ASM_REWRITE_TAC[]);
(ASM_REWRITE_TAC[]);
(VECTOR_ARITH_TAC);
(REWRITE_TAC[REAL_MUL_RZERO; REAL_ARITH `&0 / x = &0`]);
(VECTOR_ARITH_TAC);
(* ========================================================================== *)
(NEW_GOAL `norm (u0 - p:real^3) pow 2 =
norm ((p'+ m) - p) pow 2 + norm (u0 - (p' + m)) pow 2`);
(MATCH_MP_TAC PYTHAGORAS);
(REWRITE_WITH `p - (p'+ m) = projection (s2 - m) (p - m:real^3)`);
(REWRITE_TAC[VECTOR_ARITH `p - (a + b:real^3) = (p - b) - a`]);
(EXPAND_TAC "p'" THEN REWRITE_TAC[proj_point]);
(UNDISCH_TAC `between (p - m) (vec 0,n - m:real^3)`);
(REWRITE_TAC[BETWEEN_IN_CONVEX_HULL; CONVEX_HULL_2;IN;
IN_ELIM_THM; VECTOR_MUL_RZERO;VECTOR_ADD_LID]);
(REPEAT STRIP_TAC);
(VECTOR_ARITH_TAC);
(NEW_GOAL `(?k. k <= &1 /\ &0 <= k /\
projection (s2 - m) (p - m:real^3) = k % projection (s2 - m) (n - m))`);
(MATCH_MP_TAC PARALLEL_PROJECTION);
(ASM_REWRITE_TAC[]);
(STRIP_TAC);
(NEW_GOAL `s2 = m:real^3`);
(ASM_REWRITE_TAC[]);
(SWITCH_TAC THEN DEL_TAC);
(NEW_GOAL `between s2 (u0, s1:real^3)`);
(ASM_MESON_TAC[]);
(NEW_GOAL `s2 IN affine hull {u0, s1:real^3}`);
(UP_ASM_TAC THEN REWRITE_TAC[BETWEEN_IN_CONVEX_HULL]);
(STRIP_TAC);
(NEW_GOAL `convex hull {u0,s1:real^3} SUBSET affine hull {u0,s1}`);
(REWRITE_TAC[CONVEX_HULL_SUBSET_AFFINE_HULL]);
(UP_ASM_TAC THEN UP_ASM_TAC THEN SET_TAC[]);
(NEW_GOAL `affine hull {u0,s1,s2} = affine hull {u0, s1:real^3}`);
(MATCH_MP_TAC AFFINE_HULLS_EQ);
(REWRITE_TAC[SUBSET; SET_RULE `x IN {a,b,c} <=> x = a \/ x = b \/ x = c`]);
(REPEAT STRIP_TAC);
(ASM_REWRITE_TAC[Trigonometry2.UV_IN_AFF2]);
(ASM_REWRITE_TAC[Trigonometry2.UV_IN_AFF2]);
(ASM_MESON_TAC[]);
(UP_ASM_TAC);
(REWRITE_TAC[SUBSET; SET_RULE `x IN {b,c} <=> x = b \/ x = c`]);
(REPEAT STRIP_TAC);
(ASM_REWRITE_TAC[AFFINE_HULL_3;IN;IN_ELIM_THM]);
(EXISTS_TAC `&1` THEN EXISTS_TAC `&0` THEN EXISTS_TAC `&0`);
(STRIP_TAC);
(REAL_ARITH_TAC);
(VECTOR_ARITH_TAC);
(REWRITE_TAC[ASSUME `x = s1:real^3`;AFFINE_HULL_3;IN;IN_ELIM_THM]);
(EXISTS_TAC `&0` THEN EXISTS_TAC `&1` THEN EXISTS_TAC `&0`);
(STRIP_TAC);
(REAL_ARITH_TAC);
(VECTOR_ARITH_TAC);
(NEW_GOAL `aff_dim {u0,s1,s2:real^3} <= &1`);
(ONCE_REWRITE_TAC[GSYM AFF_DIM_AFFINE_HULL]);
(ONCE_ASM_REWRITE_TAC[]);
(ONCE_REWRITE_TAC[AFF_DIM_AFFINE_HULL]);
(MATCH_MP_TAC (ARITH_RULE `(?x. x <= &1 /\ y <= x:int) ==> y <= &1`));
(EXISTS_TAC `&(CARD {u0,s1:real^3}):int - &1`);
(STRIP_TAC);
(REWRITE_TAC[ARITH_RULE `a:int - &1 <= &1 <=> a <= &2`; INT_OF_NUM_LE]);
(REWRITE_TAC[Geomdetail.CARD2]);
(MATCH_MP_TAC AFF_DIM_LE_CARD);
(REWRITE_TAC[Geomdetail.FINITE6]);
(NEW_GOAL `aff_dim {u0,s1,s2:real^3} = &2`);
(NEW_GOAL `vl:(real^3)list = truncate_simplex 2 ul`);
(EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
(REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
(REWRITE_WITH `aff_dim {u0,s1,s2:real^3} =
aff_dim {omega_list_n V vl j | j IN 0..2}`);
(AP_TERM_TAC);
(REWRITE_TAC[IN_NUMSEG_0]);
(REWRITE_TAC[SET_EQ_LEMMA;
SET_RULE `x IN {a,b,c} <=> (x = a \/ x = b \/ x = c)`; IN;IN_ELIM_THM]);
(REPEAT STRIP_TAC);
(EXISTS_TAC `0`);
(REWRITE_TAC[ARITH_RULE `0 <= 2`; OMEGA_LIST_N]);
(EXPAND_TAC "vl" THEN REWRITE_TAC[HD]);
(ASM_REWRITE_TAC[]);
(EXISTS_TAC `1`);
(ASM_REWRITE_TAC[ARITH_RULE `1 <= 2`]);
(EXPAND_TAC "vl");
(REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
(DEL_TAC);
(EXPAND_TAC "s1");
(REWRITE_TAC[OMEGA_LIST_TRUNCATE_1; OMEGA_LIST_TRUNCATE_1_NEW1]);
(EXISTS_TAC `2`);
(REWRITE_TAC[ARITH_RULE `2 <= 2`; ASSUME `x = s2:real^3`] THEN EXPAND_TAC "vl" THEN DEL_TAC);
(EXPAND_TAC "s2");
(REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2; HD]);
(REWRITE_TAC[set_of_list; OMEGA_LIST_TRUNCATE_2;
OMEGA_LIST_TRUNCATE_2_NEW1]);
(ASM_CASES_TAC `j = 0`);
(DISJ1_TAC);
(REWRITE_TAC[ASSUME `x:real^3 = omega_list_n V vl j`; OMEGA_LIST_N; HD]);
(EXPAND_TAC "vl");
(REWRITE_TAC[ASSUME `j = 0`]);
(REWRITE_TAC[OMEGA_LIST_N; HD]);
(ASM_CASES_TAC `j = 1`);
(DISJ2_TAC);
(DISJ1_TAC);
(ASM_REWRITE_TAC[]);
(REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2; HD]);
(EXPAND_TAC "s1");
(REWRITE_TAC[OMEGA_LIST_TRUNCATE_1; OMEGA_LIST_TRUNCATE_1_NEW1]);
(ASM_CASES_TAC `j = 2`);
(DISJ2_TAC);
(DISJ2_TAC);
(REWRITE_TAC[ASSUME `x:real^3 = omega_list_n V vl j`]);
(EXPAND_TAC "vl");
(EXPAND_TAC "s2");
(REWRITE_TAC[ASSUME `j = 2`; OMEGA_LIST_TRUNCATE_2; OMEGA_LIST_TRUNCATE_2_NEW1]);
(SUBGOAL_THEN `F` MP_TAC);
(ASM_ARITH_TAC);
(MESON_TAC[]);
(MATCH_MP_TAC XNHPWAB3);
(ASM_REWRITE_TAC[IN]);
STRIP_TAC;
(MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
(EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]);
(ASM_MESON_TAC[]);
(ASM_MESON_TAC[]);
(ASM_ARITH_TAC);
(FIRST_X_ASSUM CHOOSE_TAC);
(UP_ASM_TAC THEN STRIP_TAC);
(REWRITE_TAC[ASSUME `projection (s2 - m) (p - m:real^3) =
k % projection (s2 - m) (n - m)`]);
(REWRITE_TAC[projection_proj_point; orthogonal]);
(REWRITE_TAC[ASSUME `proj_point (s2 - m) (n - m:real^3) = n'`]);
(REWRITE_TAC[ASSUME `n' = s2 - m:real^3`;
VECTOR_ARITH `n - m - (a - m:real^3) = n - a`]);
(UNDISCH_TAC `between n (s2,s3:real^3)`);
(REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;CONVEX_HULL_2;IN;IN_ELIM_THM] THEN
REPEAT STRIP_TAC);
(REWRITE_TAC[ASSUME `n = u % s2 + v % s3:real^3`]);
(REWRITE_WITH `(u % s2 + v % s3:real^3) - s2 = (u % s2 + v % s3) - (u + v) % s2`);
(ASM_REWRITE_TAC[VECTOR_MUL_LID]);
(REWRITE_TAC[VECTOR_ARITH
`(u % s2 + v % s3) - (u + v) % s2 = v % (s3 - s2:real^3)`]);
(ONCE_REWRITE_TAC[VECTOR_ARITH
`u0 - (p' + m) = ((u0:real^3) + s2 - (p' + m)) - s2`]);
(NEW_GOAL `(s3 - s2:real^3) dot ((u0 + s2 - (p' + m)) - s2) = &0`);
(ASM_REWRITE_TAC[]);
(MATCH_MP_TAC MHFTTZN4);
(EXISTS_TAC `V:real^3->bool`);
(EXISTS_TAC `2`);
(ASM_REWRITE_TAC[]);
(STRIP_TAC);
(REWRITE_WITH `vl:(real^3)list = truncate_simplex 2 ul`);
(ASM_REWRITE_TAC[]);
(EXPAND_TAC "vl");
(REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
(MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
(EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]);
(STRIP_TAC);
(MATCH_MP_TAC IN_AFFINE_KY_LEMMA1);
(REWRITE_WITH `vl:(real^3)list = truncate_simplex 2 ul`);
(ASM_REWRITE_TAC[]);
(EXPAND_TAC "vl");
(REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
(ASM_REWRITE_TAC[]);
(EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]);
(NEW_GOAL `!a b c m n p.
m IN affine hull {a,b,c:real^3} /\
n IN affine hull {a,b,c} /\
p IN affine hull {a,b,c}
==> m + n - p IN affine hull {a,b,c}`);
(REWRITE_TAC[AFFINE_HULL_3; IN;IN_ELIM_THM]);
(REPEAT STRIP_TAC);
(EXISTS_TAC `(u' + u'') - u'''`);
(EXISTS_TAC `(v' + v'') - v'''`);
(EXISTS_TAC `(w + w') - w''`);
STRIP_TAC;
(ASM_REAL_ARITH_TAC);
(ASM_REWRITE_TAC[]);
(VECTOR_ARITH_TAC);
(FIRST_X_ASSUM MATCH_MP_TAC);
(REPEAT STRIP_TAC);
(REWRITE_TAC[AFFINE_HULL_3; IN;IN_ELIM_THM]);
(EXISTS_TAC `&1` THEN EXISTS_TAC `&0` THEN EXISTS_TAC `&0`);
STRIP_TAC;
(ASM_REAL_ARITH_TAC);
(VECTOR_ARITH_TAC);
(MATCH_MP_TAC Rogers.OAPVION1);
(STRIP_TAC);
(SET_TAC[]);
(REWRITE_WITH `{u0, u1, u2:real^3} = set_of_list vl`);
(EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]);
(MATCH_MP_TAC Rogers.BARV_AFFINE_INDEPENDENT);
(EXISTS_TAC `V:real^3->bool`);
(EXISTS_TAC `2`);
(ASM_REWRITE_TAC[]);
(REWRITE_WITH `vl:(real^3)list = truncate_simplex 2 ul`);
(ASM_REWRITE_TAC[]);
(EXPAND_TAC "vl");
(REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
(MATCH_MP_TAC Packing3. TRUNCATE_SIMPLEX_BARV);
(EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]);
(EXPAND_TAC "p'");
(REWRITE_TAC[PRO_EXP]);
(ABBREV_TAC `h = ((p - m) dot (s2 - m)) / ((s2 - m) dot (s2 - m:real^3))`);
(NEW_GOAL `!a b c x y r.
x IN affine hull {a,b,c:real^3} /\
y IN affine hull {a,b,c}
==> r % (x - y) + y IN affine hull {a,b,c}`);
(REWRITE_TAC[AFFINE_HULL_3; IN;IN_ELIM_THM]);
(REPEAT STRIP_TAC);
(EXISTS_TAC `r * (u' - u'') + u''`);
(EXISTS_TAC `r * (v' - v'') + v''`);
(EXISTS_TAC `r * (w - w') + w'`);
STRIP_TAC;
(REWRITE_TAC[REAL_ARITH
`(r * (u' - u'') + u'') + (r * (v' - v'') + v'') + r * (w - w') + w' =
r * (u' + v' + w) - r * (u'' + v'' + w') + (u'' + v'' + w')`]);
(ASM_REWRITE_TAC[REAL_MUL_RID]);
(ASM_REAL_ARITH_TAC);
(ASM_REWRITE_TAC[]);
(VECTOR_ARITH_TAC);
(FIRST_X_ASSUM MATCH_MP_TAC);
(ASM_REWRITE_TAC[]);
(STRIP_TAC);
(REWRITE_WITH `{u0, u1, u2:real^3} = set_of_list vl`);
(EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]);
(MATCH_MP_TAC Rogers.OAPVION1);
(STRIP_TAC);
(REWRITE_WITH `set_of_list vl = {u0, u1, u2:real^3}`);
(EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]);
(SET_TAC[]);
(MATCH_MP_TAC Rogers.BARV_AFFINE_INDEPENDENT);
(EXISTS_TAC `V:real^3->bool`);
(EXISTS_TAC `2`);
(ASM_REWRITE_TAC[]);
(REWRITE_WITH `vl:(real^3)list = truncate_simplex 2 ul`);
(ASM_REWRITE_TAC[]);
(EXPAND_TAC "vl");
(REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
(MATCH_MP_TAC Packing3. TRUNCATE_SIMPLEX_BARV);
(EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]);
(UNDISCH_TAC `between m (u0,s1:real^3)`);
(REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;CONVEX_HULL_2;
AFFINE_HULL_3;IN;IN_ELIM_THM] THEN REPEAT STRIP_TAC);
(UP_ASM_TAC);
(REWRITE_WITH `s1 = midpoint (u0,u1:real^3)`);
(REWRITE_TAC[GSYM (ASSUME `omega_list_n V [u0; u1; u2; u3:real^3] 1 = s1`)]);
(REWRITE_WITH `omega_list_n V [u0; u1; u2; u3] 1 =
omega_list_n V [u0; u1:real^3] 1`);
(REWRITE_TAC[OMEGA_LIST_TRUNCATE_1_NEW2;OMEGA_LIST_TRUNCATE_1]);
(REWRITE_TAC[OMEGA_LIST_TRUNCATE_1_NEW2]);
(REWRITE_WITH `omega_list V [u0; u1:real^3] =
circumcenter (set_of_list [u0;u1])`);
(MATCH_MP_TAC XNHPWAB1);
(EXISTS_TAC `1`);
(ASM_REWRITE_TAC[ARITH_RULE `1 <= 3`]);
(REWRITE_WITH `[u0;u1:real^3] = truncate_simplex 1 vl`);
(EXPAND_TAC "vl" THEN REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);
(REWRITE_TAC[IN] THEN STRIP_TAC);
(MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
(EXISTS_TAC `2` THEN REWRITE_TAC[ARITH_RULE `1 <= 2`]);
(REWRITE_WITH `vl = truncate_simplex 2 ul:(real^3)list`);
(EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
(REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
(MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
(EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]);
(NEW_GOAL `!i j. i < j /\ j <= 2
==> hl (truncate_simplex i (vl:(real^3)list))
< hl (truncate_simplex j vl)`);
(MATCH_MP_TAC XNHPWAB4);
(EXISTS_TAC `V:real^3->bool`);
(ASM_REWRITE_TAC[IN]);
(REWRITE_WITH `vl = truncate_simplex 2 ul:(real^3)list`);
(EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
(REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
(ASM_REWRITE_TAC[]);
(MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
(EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]);
(ASM_MESON_TAC[]);
(NEW_GOAL `hl (truncate_simplex 1 (vl:(real^3)list)) < hl (truncate_simplex 2 vl)`);
(FIRST_X_ASSUM MATCH_MP_TAC);
(ARITH_TAC);
(NEW_GOAL `truncate_simplex 2 vl = truncate_simplex 2 ul:(real^3)list`);
(EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
(REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
(MATCH_MP_TAC (REAL_ARITH `a < hl (truncate_simplex 2 (vl:(real^3)list)) /\
hl (truncate_simplex 2 vl) < b ==> a < b`));
(ASM_REWRITE_TAC[]);
(ASM_MESON_TAC[]);
(REWRITE_TAC[set_of_list;Rogers.CIRCUMCENTER_2]);
(REWRITE_TAC[BETWEEN_IN_CONVEX_HULL; CONVEX_HULL_2; midpoint; IN; IN_ELIM_THM; AFFINE_HULL_3]);
(REPEAT STRIP_TAC);
(EXISTS_TAC `u' + v' * inv (&2)`);
(EXISTS_TAC `v' * inv (&2)`);
(EXISTS_TAC `&0`);
(STRIP_TAC);
(REWRITE_TAC[REAL_ARITH `(u' + v' * inv (&2)) + v' * inv (&2) + &0 = u' + v'`]);
(ASM_REWRITE_TAC[]);
(ASM_REWRITE_TAC[]);
(VECTOR_ARITH_TAC);
(REWRITE_TAC[VECTOR_ARITH `a % b % c dot d = a * b * (c dot d)`]);
(ASM_REWRITE_TAC[]);
(REWRITE_TAC[REAL_MUL_RZERO]);
(* ========================================================================= *)
(NEW_GOAL `norm (u0 - s:real^3) pow 2 =
norm (s2 - s) pow 2 + norm (u0 - s2) pow 2`);
(MATCH_MP_TAC PYTHAGORAS);
(ASM_REWRITE_TAC[orthogonal]);
(MATCH_MP_TAC MHFTTZN4);
(EXISTS_TAC `V:real^3->bool`);
(EXISTS_TAC `2`);
(REWRITE_WITH `vl:(real^3)list = truncate_simplex 2 ul`);
(EXPAND_TAC "vl" THEN DEL_TAC);
(ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
(REPEAT STRIP_TAC);
(ASM_REWRITE_TAC[]);
(MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
(EXISTS_TAC `3`);
(ASM_MESON_TAC[ARITH_RULE `2 <= 3`]);
(UNDISCH_TAC `between s (s2,s3:real^3)`);
(REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;CONVEX_HULL_2;IN;IN_ELIM_THM]);
(REPEAT STRIP_TAC);
(ONCE_REWRITE_TAC [GSYM IN]);
(ONCE_ASM_REWRITE_TAC[]);
(NEW_GOAL `convex (affine hull voronoi_list V
(truncate_simplex 2 [u0; u1; u2; u3:real^3]))`);
(MATCH_MP_TAC POLYHEDRON_IMP_CONVEX);
(REWRITE_TAC[POLYHEDRON_AFFINE_HULL]);
(UP_ASM_TAC THEN REWRITE_TAC[convex]);
(DISCH_TAC);
(FIRST_ASSUM MATCH_MP_TAC);
(ASM_REWRITE_TAC[]);
(REPEAT STRIP_TAC);
(REWRITE_WITH `truncate_simplex 2 [u0; u1; u2; u3:real^3] = vl`);
(EXPAND_TAC "vl" THEN REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
(NEW_GOAL `affine hull (voronoi_list V vl) INTER
affine hull (set_of_list vl) =
{circumcenter (set_of_list (vl:(real^3)list))}`);
(MATCH_MP_TAC Rogers.MHFTTZN3);
(EXISTS_TAC `2`);
(REWRITE_WITH `vl:(real^3)list = truncate_simplex 2 ul`);
(EXPAND_TAC "vl" THEN DEL_TAC);
(ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
(REPEAT STRIP_TAC);
(ASM_REWRITE_TAC[]);
(MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
(EXISTS_TAC `3`);
(ASM_MESON_TAC[ARITH_RULE `2 <= 3`]);
(UP_ASM_TAC THEN SET_TAC[]);
(MATCH_MP_TAC IN_AFFINE_KY_LEMMA1);
(ASM_MESON_TAC[]);
(ASM_REWRITE_TAC[]);
(REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2;set_of_list]);
(MATCH_MP_TAC IN_AFFINE_KY_LEMMA1);
(SET_TAC[]);
(* ======================================================================== *)
(NEW_GOAL `norm (u0 - (p' + m)) pow 2 <= norm (u0 - s2:real^3) pow 2`);
(REWRITE_TAC[GSYM REAL_LE_SQUARE_ABS; REAL_ABS_NORM;GSYM dist]);
(ONCE_REWRITE_TAC[DIST_SYM] THEN REWRITE_TAC[dist]);
(NEW_GOAL
`(?y. y IN {m, s2:real^3} /\
(!x. x IN convex hull {m,s2} ==> norm (x - u0) <= norm (y - u0 )))`);
(MATCH_MP_TAC SIMPLEX_FURTHEST_LE);
(STRIP_TAC);
(REWRITE_TAC[Geomdetail.FINITE6]);
(SET_TAC[]);
(UP_ASM_TAC THEN REWRITE_TAC[SET_RULE `x IN {a, b} <=> x = b \/ x = a`]
THEN REPEAT STRIP_TAC);
(UP_ASM_TAC THEN REWRITE_TAC[ASSUME `y' = s2:real^3`]);
(DISCH_TAC THEN FIRST_ASSUM MATCH_MP_TAC);
(UNDISCH_TAC `between p' (vec 0,n':real^3)`);
(REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;CONVEX_HULL_2;IN;IN_ELIM_THM]);
(REPEAT STRIP_TAC);
(EXISTS_TAC `u:real` THEN EXISTS_TAC `v:real` THEN ASM_REWRITE_TAC[]);
(REWRITE_TAC[VECTOR_MUL_RZERO; VECTOR_ADD_LID; VECTOR_ARITH
`a % (x - y) + y = b % y + a % x <=> ((b + a) - &1) % y = vec 0`]);
(ASM_REWRITE_TAC[REAL_SUB_REFL; VECTOR_MUL_LZERO]);
(MATCH_MP_TAC (REAL_ARITH `(?s. a <= s /\ s <= b) ==> a <= b`));
(EXISTS_TAC `norm (m - u0:real^3)`);
(STRIP_TAC);
(UP_ASM_TAC THEN REWRITE_TAC[ASSUME `y' = m:real^3`]);
(DISCH_TAC THEN FIRST_ASSUM MATCH_MP_TAC);
(UNDISCH_TAC `between p' (vec 0,n':real^3)`);
(REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;CONVEX_HULL_2;IN;IN_ELIM_THM]);
(REPEAT STRIP_TAC);
(EXISTS_TAC `u:real` THEN EXISTS_TAC `v:real` THEN ASM_REWRITE_TAC[]);
(REWRITE_TAC[VECTOR_MUL_RZERO; VECTOR_ADD_LID; VECTOR_ARITH
`a % (x - y) + y = b % y + a % x <=> ((b + a) - &1) % y = vec 0`]);
(ASM_REWRITE_TAC[REAL_SUB_REFL; VECTOR_MUL_LZERO]);
(MATCH_MP_TAC (REAL_ARITH `(?s. a <= s /\ s <= b) ==> a <= b`));
(EXISTS_TAC `norm (s1 - u0:real^3)`);
(STRIP_TAC);
(REWRITE_TAC[GSYM dist]);
(ONCE_REWRITE_TAC[DIST_SYM]);
(UNDISCH_TAC `between m (u0,s1:real^3)`);
(REWRITE_TAC[between]);
(STRIP_TAC);
(ASM_REWRITE_TAC[]);
(REWRITE_TAC[REAL_ARITH `a <= a + b <=> &0 <= b`; DIST_POS_LE]);
(NEW_GOAL `norm (s2 - u0:real^3) pow 2 =
norm (s1 - u0) pow 2 + norm (s2 - s1) pow 2`);
(MATCH_MP_TAC PYTHAGORAS);
(ABBREV_TAC `sl = [u0;u1:real^3]`);
(NEW_GOAL `s1:real^3 = circumcenter (set_of_list sl)`);
(EXPAND_TAC "s1" THEN EXPAND_TAC "sl");
(REWRITE_TAC[OMEGA_LIST_TRUNCATE_1]);
(MATCH_MP_TAC XNHPWAB1);
(EXISTS_TAC `1`);
(REWRITE_WITH `[u0; u1:real^3] = truncate_simplex 1 ul`);
(ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);
(ASM_REWRITE_TAC[IN]);
(STRIP_TAC);
(MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
(EXISTS_TAC `3`);
(ASM_MESON_TAC[ARITH_RULE `1 <= 3`]);
(DEL_TAC THEN ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);
(REWRITE_WITH `[u0;u1:real^3] = truncate_simplex 1 vl`);
(EXPAND_TAC "vl" THEN REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);
(NEW_GOAL `!i j. i < j /\ j <= 2
==> hl (truncate_simplex i (vl:(real^3)list))
< hl (truncate_simplex j vl)`);
(MATCH_MP_TAC XNHPWAB4);
(EXISTS_TAC `V:real^3->bool`);
(ASM_REWRITE_TAC[IN]);
(REWRITE_WITH `vl = truncate_simplex 2 ul:(real^3)list`);
(EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
(REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
(ASM_REWRITE_TAC[]);
(MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
(EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]);
(ASM_MESON_TAC[]);
(NEW_GOAL `hl (truncate_simplex 1 (vl:(real^3)list)) < hl (truncate_simplex 2 vl)`);
(FIRST_X_ASSUM MATCH_MP_TAC);
(ARITH_TAC);
(NEW_GOAL `truncate_simplex 2 vl = truncate_simplex 2 ul:(real^3)list`);
(EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
(REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
(MATCH_MP_TAC (REAL_ARITH `a < hl (truncate_simplex 2 (vl:(real^3)list)) /\
hl (truncate_simplex 2 vl) < b ==> a < b`));
(ASM_REWRITE_TAC[]);
(ASM_MESON_TAC[]);
(REWRITE_TAC [ASSUME `s1:real^3 = circumcenter (set_of_list sl)`;orthogonal]);
(ONCE_REWRITE_TAC[DOT_SYM]);
(MATCH_MP_TAC MHFTTZN4);
(EXISTS_TAC `V:real^3->bool`);
(EXISTS_TAC `1`);
(ASM_REWRITE_TAC[]);
(STRIP_TAC);
(REWRITE_WITH `sl:(real^3)list = truncate_simplex 1 ul`);
(ASM_REWRITE_TAC[]);
(EXPAND_TAC "sl");
(REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);
(MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
(EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `1 <= 3`]);
(STRIP_TAC);
(NEW_GOAL `affine hull (voronoi_list V vl) SUBSET
affine hull (voronoi_list V (sl:(real^3)list))`);
(MATCH_MP_TAC AFFINE_SUBSET_KY_LEMMA);
(EXPAND_TAC "sl" THEN EXPAND_TAC "vl" THEN REWRITE_TAC
[set_of_list; SET_RULE `x IN {a, b} <=> x = a \/ x = b`;
SET_RULE `x IN {a,b,c} <=> x = a \/ x = b \/ x = c`;
VORONOI_LIST; VORONOI_SET;voronoi_closed; SUBSET;IN_INTERS]);
(REWRITE_TAC[IN;IN_ELIM_THM] THEN REPEAT STRIP_TAC);
(FIRST_ASSUM MATCH_MP_TAC);
(EXISTS_TAC `v:real^3`);
(ASM_REWRITE_TAC[]);
(FIRST_ASSUM MATCH_MP_TAC);
(EXISTS_TAC `v:real^3`);
(ASM_REWRITE_TAC[]);
(MATCH_MP_TAC (SET_RULE `(?C. C SUBSET B /\ s IN C ) ==> s IN B`));
(EXISTS_TAC `affine hull voronoi_list V (vl:(real^3)list)`);
(ASM_REWRITE_TAC[]);
(NEW_GOAL `affine hull (voronoi_list V vl) INTER
affine hull (set_of_list vl) =
{circumcenter (set_of_list (vl:(real^3)list))}`);
(MATCH_MP_TAC Rogers.MHFTTZN3);
(EXISTS_TAC `2`);
(REWRITE_WITH `vl:(real^3)list = truncate_simplex 2 ul`);
(EXPAND_TAC "vl" THEN DEL_TAC);
(ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
(REPEAT STRIP_TAC);
(ASM_REWRITE_TAC[]);
(MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
(EXISTS_TAC `3`);
(ASM_MESON_TAC[ARITH_RULE `2 <= 3`]);
(UP_ASM_TAC THEN SET_TAC[]);
(EXPAND_TAC "sl" THEN REWRITE_TAC[set_of_list]);
(MATCH_MP_TAC IN_AFFINE_KY_LEMMA1);
(SET_TAC[IN]);
(REWRITE_WITH `norm (s1 - u0:real^3) <= norm (s2 - u0)
<=> norm (s1 - u0) pow 2 <= norm (s2 - u0) pow 2`);
(MATCH_MP_TAC Collect_geom.POW2_COND);
(REWRITE_TAC[NORM_POS_LE]);
(UP_ASM_TAC THEN MATCH_MP_TAC
(REAL_ARITH `(&0 <= c) ==> (a = b + c ==> b <= a)`));
(REWRITE_TAC[REAL_LE_POW_2]);
(* ==================================================================== *)
(NEW_GOAL `norm (u0 - s:real^3) < norm (u0 - p)`);
(MATCH_MP_TAC (REAL_ARITH `(?s. a <= s /\ s < b) ==> a < b`));
(EXISTS_TAC `sqrt (&2)`);
(STRIP_TAC);
(REWRITE_TAC[GSYM dist]);
(ASM_REAL_ARITH_TAC);
(REWRITE_TAC[GSYM dist]);
(UNDISCH_TAC `dist (u0,p:real^3) >= sqrt (&2)`);
(MATCH_MP_TAC (REAL_ARITH `~(a = b) ==> (a >= b ==> b < a)`));
(STRIP_TAC);
(NEW_GOAL `~(p:real^3 IN B2)`);
(ASM_SET_TAC[IN_DIFF]);
(UP_ASM_TAC THEN EXPAND_TAC "B2" THEN REWRITE_TAC[IN;IN_ELIM_THM]);
(ASM_REWRITE_TAC[HD; GSYM dist]);
(ONCE_REWRITE_TAC[DIST_SYM] THEN ASM_REWRITE_TAC[]);
(NEW_GOAL `norm (u0 - s:real^3) pow 2 < norm (u0 - p) pow 2`);
(REWRITE_TAC[GSYM REAL_LT_SQUARE_ABS; REAL_ABS_NORM]);
(ASM_REWRITE_TAC[]);
(NEW_GOAL `norm (s2 - s:real^3) pow 2 < norm ((p' + m) - p:real^3) pow 2`);
(REWRITE_WITH `norm (s2 - s) pow 2 =
norm (u0 - s:real^3) pow 2 - norm (u0 - s2) pow 2`);
(ASM_REAL_ARITH_TAC);
(REWRITE_WITH `norm ((p' + m) - p) pow 2 =
norm (u0 - p:real^3) pow 2 - norm (u0 - (p' + m)) pow 2`);
(ASM_REAL_ARITH_TAC);
(ASM_REAL_ARITH_TAC);
(* ======================================================================== *)
(UNDISCH_TAC `p IN convex hull {u0, u1, u2, s:real^3}`);
(REWRITE_TAC[CONVEX_HULL_4; IN; IN_ELIM_THM] THEN REPEAT STRIP_TAC);
(NEW_GOAL `(?m1. m1 IN convex hull {u0, u1, u2} /\
between p (m1, s:real^3))`);
(ASM_CASES_TAC `(u + v + w = &0)`);
(NEW_GOAL `p = s:real^3`);
(ASM_REWRITE_TAC[]);
(REWRITE_WITH `u = &0 /\ v = &0 /\ w = &0 /\ z = &1`);
(ASM_REAL_ARITH_TAC);
(VECTOR_ARITH_TAC);
(NEW_GOAL `F`);
(NEW_GOAL `~(p:real^3 IN B2)`);
(ASM_SET_TAC[IN_DIFF]);
(UP_ASM_TAC THEN EXPAND_TAC "B2" THEN REWRITE_TAC[IN;IN_ELIM_THM]);
(ASM_REWRITE_TAC[HD; GSYM dist]);
(REWRITE_WITH `u = &0 /\ v = &0 /\ w = &0 /\ z = &1`);
(ASM_REAL_ARITH_TAC);
(REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_MUL_LID; VECTOR_ADD_LID]);
(ONCE_REWRITE_TAC[DIST_SYM] THEN ASM_REWRITE_TAC[]);
(UP_ASM_TAC THEN MESON_TAC[]);
(EXISTS_TAC `(u / (u + v + w)) % u0 + (v / (u + v + w)) % u1 +
(w / (u + v + w)) % u2:real^3`);
(REWRITE_TAC[BETWEEN_IN_CONVEX_HULL; CONVEX_HULL_2;CONVEX_HULL_3; IN;
IN_ELIM_THM] THEN REPEAT STRIP_TAC);
(EXISTS_TAC `u / (u + v + w)`);
(EXISTS_TAC `v / (u + v + w)`);
(EXISTS_TAC `w / (u + v + w)`);
(ASM_REWRITE_TAC[REAL_ARITH `a / x + b / x + c / x = (a + b + c) / x`]);
(REPEAT STRIP_TAC);
(MATCH_MP_TAC REAL_LE_DIV);
(ASM_REAL_ARITH_TAC);
(MATCH_MP_TAC REAL_LE_DIV);
(ASM_REAL_ARITH_TAC);
(MATCH_MP_TAC REAL_LE_DIV);
(ASM_REAL_ARITH_TAC);
(MATCH_MP_TAC REAL_DIV_REFL);
(ASM_REAL_ARITH_TAC);
(EXISTS_TAC `u + v + w:real`);
(EXISTS_TAC `z:real`);
(REPEAT STRIP_TAC);
(ASM_REAL_ARITH_TAC);
(ASM_REAL_ARITH_TAC);
(ASM_REAL_ARITH_TAC);
(ASM_REWRITE_TAC[]);
(REWRITE_TAC[VECTOR_ARITH `a % (x/ a % u0 + y / a % u1 + z / a % u2) =
(a / a) % (x % u0) + (a / a) % (y % u1) + (a / a) % (z % u2)`]);
(REWRITE_WITH `(u + v + w) / (u + v + w) = &1`);
(ASM_SIMP_TAC [REAL_DIV_REFL]);
(REWRITE_TAC[VECTOR_MUL_LID]);
(VECTOR_ARITH_TAC);
(UP_ASM_TAC THEN REPEAT STRIP_TAC);
(* ======================================================================== *)
(NEW_GOAL `(?k. k <= &1 /\ &0 <= k /\
projection (s2 - m) (p - m:real^3) = k % projection (s2 - m) (n - m))`);
(MATCH_MP_TAC PARALLEL_PROJECTION);
(ASM_REWRITE_TAC[]);
(STRIP_TAC);
(NEW_GOAL `s2 = m:real^3`);
(ASM_REWRITE_TAC[]);
(SWITCH_TAC THEN DEL_TAC);
(NEW_GOAL `between s2 (u0, s1:real^3)`);
(ASM_MESON_TAC[]);
(NEW_GOAL `s2 IN affine hull {u0, s1:real^3}`);
(UP_ASM_TAC THEN REWRITE_TAC[BETWEEN_IN_CONVEX_HULL]);
(STRIP_TAC);
(NEW_GOAL `convex hull {u0,s1:real^3} SUBSET affine hull {u0,s1}`);
(REWRITE_TAC[CONVEX_HULL_SUBSET_AFFINE_HULL]);
(UP_ASM_TAC THEN UP_ASM_TAC THEN SET_TAC[]);
(NEW_GOAL `affine hull {u0,s1,s2} = affine hull {u0, s1:real^3}`);
(MATCH_MP_TAC AFFINE_HULLS_EQ);
(REWRITE_TAC[SUBSET; SET_RULE `x IN {a,b,c} <=> x = a \/ x = b \/ x = c`]);
(REPEAT STRIP_TAC);
(ASM_REWRITE_TAC[Trigonometry2.UV_IN_AFF2]);
(ASM_REWRITE_TAC[Trigonometry2.UV_IN_AFF2]);
(ASM_MESON_TAC[]);
(UP_ASM_TAC);
(REWRITE_TAC[SUBSET; SET_RULE `x IN {b,c} <=> x = b \/ x = c`]);
(REPEAT STRIP_TAC);
(ASM_REWRITE_TAC[AFFINE_HULL_3;IN;IN_ELIM_THM]);
(EXISTS_TAC `&1` THEN EXISTS_TAC `&0` THEN EXISTS_TAC `&0`);
(STRIP_TAC);
(REAL_ARITH_TAC);
(VECTOR_ARITH_TAC);
(REWRITE_TAC[ASSUME `x = s1:real^3`;AFFINE_HULL_3;IN;IN_ELIM_THM]);
(EXISTS_TAC `&0` THEN EXISTS_TAC `&1` THEN EXISTS_TAC `&0`);
(STRIP_TAC);
(REAL_ARITH_TAC);
(VECTOR_ARITH_TAC);
(NEW_GOAL `aff_dim {u0,s1,s2:real^3} <= &1`);
(ONCE_REWRITE_TAC[GSYM AFF_DIM_AFFINE_HULL]);
(ONCE_ASM_REWRITE_TAC[]);
(ONCE_REWRITE_TAC[AFF_DIM_AFFINE_HULL]);
(MATCH_MP_TAC (ARITH_RULE `(?x. x <= &1 /\ y <= x:int) ==> y <= &1`));
(EXISTS_TAC `&(CARD {u0,s1:real^3}):int - &1`);
(STRIP_TAC);
(REWRITE_TAC[ARITH_RULE `a:int - &1 <= &1 <=> a <= &2`; INT_OF_NUM_LE]);
(REWRITE_TAC[Geomdetail.CARD2]);
(MATCH_MP_TAC AFF_DIM_LE_CARD);
(REWRITE_TAC[Geomdetail.FINITE6]);
(NEW_GOAL `aff_dim {u0,s1,s2:real^3} = &2`);
(NEW_GOAL `vl:(real^3)list = truncate_simplex 2 ul`);
(EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
(REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
(REWRITE_WITH `aff_dim {u0,s1,s2:real^3} =
aff_dim {omega_list_n V vl j | j IN 0..2}`);
(AP_TERM_TAC);
(REWRITE_TAC[IN_NUMSEG_0]);
(REWRITE_TAC[SET_EQ_LEMMA;
SET_RULE `x IN {a,b,c} <=> (x = a \/ x = b \/ x = c)`; IN;IN_ELIM_THM]);
(REPEAT STRIP_TAC);
(EXISTS_TAC `0`);
(REWRITE_TAC[ARITH_RULE `0 <= 2`; OMEGA_LIST_N]);
(EXPAND_TAC "vl" THEN REWRITE_TAC[HD]);
(ASM_REWRITE_TAC[]);
(EXISTS_TAC `1`);
(ASM_REWRITE_TAC[ARITH_RULE `1 <= 2`]);
(EXPAND_TAC "vl");
(REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
(DEL_TAC);
(EXPAND_TAC "s1");
(REWRITE_TAC[OMEGA_LIST_TRUNCATE_1; OMEGA_LIST_TRUNCATE_1_NEW1]);
(EXISTS_TAC `2`);
(REWRITE_TAC[ARITH_RULE `2 <= 2`; ASSUME `x = s2:real^3`] THEN EXPAND_TAC "vl" THEN DEL_TAC);
(EXPAND_TAC "s2");
(REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2; HD]);
(REWRITE_TAC[set_of_list; OMEGA_LIST_TRUNCATE_2;
OMEGA_LIST_TRUNCATE_2_NEW1]);
(ASM_CASES_TAC `j = 0`);
(DISJ1_TAC);
(REWRITE_TAC[ASSUME `x:real^3 = omega_list_n V vl j`; OMEGA_LIST_N; HD]);
(EXPAND_TAC "vl");
(REWRITE_TAC[ASSUME `j = 0`]);
(REWRITE_TAC[OMEGA_LIST_N; HD]);
(ASM_CASES_TAC `j = 1`);
(DISJ2_TAC);
(DISJ1_TAC);
(ASM_REWRITE_TAC[]);
(REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2; HD]);
(EXPAND_TAC "s1");
(REWRITE_TAC[OMEGA_LIST_TRUNCATE_1; OMEGA_LIST_TRUNCATE_1_NEW1]);
(ASM_CASES_TAC `j = 2`);
(DISJ2_TAC);
(DISJ2_TAC);
(REWRITE_TAC[ASSUME `x:real^3 = omega_list_n V vl j`]);
(EXPAND_TAC "vl");
(EXPAND_TAC "s2");
(REWRITE_TAC[ASSUME `j = 2`; OMEGA_LIST_TRUNCATE_2; OMEGA_LIST_TRUNCATE_2_NEW1]);
(SUBGOAL_THEN `F` MP_TAC);
(ASM_ARITH_TAC);
(MESON_TAC[]);
(MATCH_MP_TAC XNHPWAB3);
(ASM_REWRITE_TAC[IN]);
STRIP_TAC;
(MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
(EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]);
(ASM_MESON_TAC[]);
(ASM_MESON_TAC[]);
(ASM_ARITH_TAC);
(NEW_GOAL `?h. h <= &1 /\ &0 <= h /\
projection (s2 - m1:real^3) (p - m1) = h % projection (s2 - m1) (s - m1)`);
(MATCH_MP_TAC PARALLEL_PROJECTION);
(ASM_REWRITE_TAC[]);
(STRIP_TAC);
(NEW_GOAL `s2 = m1:real^3`);
(ASM_REWRITE_TAC[]);
(SWITCH_TAC THEN DEL_TAC);
(NEW_GOAL `between p (s2, s:real^3)`);
(ASM_MESON_TAC[]);
(NEW_GOAL `between p (s3, s2:real^3)`);
(MATCH_MP_TAC BETWEEN_TRANS);
(EXISTS_TAC `s:real^3`);
(STRIP_TAC);
(ASM_MESON_TAC[BETWEEN_SYM]);
(ASM_MESON_TAC[BETWEEN_SYM]);
(NEW_GOAL `p:real^3 IN B5`);
(EXPAND_TAC "B5");
(UP_ASM_TAC THEN REWRITE_TAC[BETWEEN_IN_CONVEX_HULL]);
(EXPAND_TAC "s2");
(EXPAND_TAC "s3");
(REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
(MESON_TAC[SET_RULE `{a,b} = {b, a}`]);
(NEW_GOAL `~(p:real^3 IN B5)`);
(ASM_SET_TAC[IN_DIFF]);
(ASM_MESON_TAC[]);
(FIRST_X_ASSUM CHOOSE_TAC);
(FIRST_X_ASSUM CHOOSE_TAC);
(NEW_GOAL `projection (s2 - m1) (s - m1) = s - s2:real^3`);
(REWRITE_TAC[projection; VECTOR_ARITH `a - b - x % (d - b) = a - d
<=> (&1 - x) % (d - b:real^3) = vec 0`]);
(REWRITE_WITH `&1 - ((s - m1) dot (s2 - m1:real^3)) / ((s2 - m1) dot (s2 - m1)) = &0`);
(REWRITE_TAC[REAL_ARITH `&1 - a = &0 <=> a = &1`]);
(REWRITE_WITH `((s - m1) dot (s2 - m1)) / ((s2 - m1) dot (s2 - m1)) = &1
<=> ((s - m1) dot (s2 - m1)) = &1 * ((s2 - m1) dot (s2 - m1:real^3))`);
(MATCH_MP_TAC REAL_EQ_LDIV_EQ);
(REWRITE_TAC[GSYM NORM_POW_2; GSYM Trigonometry2.NOT_ZERO_EQ_POW2_LT;
NORM_EQ_0; VECTOR_ARITH `a - b = vec 0 <=> a = b`]);
(STRIP_TAC);
(NEW_GOAL `between p (s2, s:real^3)`);
(ASM_MESON_TAC[]);
(NEW_GOAL `between p (s3, s2:real^3)`);
(MATCH_MP_TAC BETWEEN_TRANS);
(EXISTS_TAC `s:real^3`);
(STRIP_TAC);
(ASM_MESON_TAC[BETWEEN_SYM]);
(ASM_MESON_TAC[BETWEEN_SYM]);
(NEW_GOAL `p:real^3 IN B5`);
(EXPAND_TAC "B5");
(UP_ASM_TAC THEN REWRITE_TAC[BETWEEN_IN_CONVEX_HULL]);
(EXPAND_TAC "s2");
(EXPAND_TAC "s3");
(REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
(MESON_TAC[SET_RULE `{a,b} = {b, a}`]);
(NEW_GOAL `~(p:real^3 IN B5)`);
(ASM_SET_TAC[IN_DIFF]);
(ASM_MESON_TAC[]);
(REWRITE_TAC[REAL_MUL_LID]);
(ONCE_REWRITE_TAC[REAL_ARITH `a = b <=> a - b = &0`]);
(REWRITE_TAC[VECTOR_ARITH
`(s - m1) dot r - (s2 - m1) dot r = (s - s2) dot r:real^3`]);
(REWRITE_WITH `(s - s2) dot (s2 - m1) = --((s - s2) dot (m1 - s2:real^3))`);
(VECTOR_ARITH_TAC);
(ONCE_REWRITE_TAC[REAL_ARITH `-- a = &0 <=> a = &0`]);
(UNDISCH_TAC `between s (s2,s3:real^3)`);
(REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;IN;IN_ELIM_THM; CONVEX_HULL_2]);
(REPEAT STRIP_TAC);
(REWRITE_TAC[ASSUME `s = u' % s2 + v' % s3:real^3`]);
(REWRITE_WITH `(u' % s2 + v' % s3) - s2:real^3 =
(u' % s2 + v' % s3) - (u' + v') % s2`);
(ASM_REWRITE_TAC[VECTOR_MUL_LID]);
(REWRITE_TAC[VECTOR_ARITH
`(u' % s2 + v' % s3) - (u' + v') % s2 = v' % (s3 - s2)`; DOT_LMUL]);
(REWRITE_WITH `(s3 - s2) dot (m1 - s2:real^3) = &0`);
(ASM_REWRITE_TAC[]);
(MATCH_MP_TAC MHFTTZN4);
(EXISTS_TAC `V:real^3->bool`);
(EXISTS_TAC `2`);
(REWRITE_WITH `vl:(real^3)list = truncate_simplex 2 ul`);
(EXPAND_TAC "vl" THEN DEL_TAC);
(ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
(REPEAT STRIP_TAC);
(ASM_REWRITE_TAC[]);
(MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
(EXISTS_TAC `3`);
(ASM_MESON_TAC[ARITH_RULE `2 <= 3`]);
(MATCH_MP_TAC IN_AFFINE_KY_LEMMA1);
(ONCE_ASM_REWRITE_TAC[]);
(REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`;
TRUNCATE_SIMPLEX_EXPLICIT_2;set_of_list]);
(UNDISCH_TAC `m1 IN convex hull {u0, u1, u2:real^3}`);
(NEW_GOAL `convex hull {u0, u1, u2:real^3} SUBSET
affine hull {u0, u1, u2:real^3}`);
(REWRITE_TAC[CONVEX_HULL_SUBSET_AFFINE_HULL]);
(UP_ASM_TAC THEN SET_TAC[]);
(REAL_ARITH_TAC);
(VECTOR_ARITH_TAC);
(ABBREV_TAC `M = projection (s2 - m1) (p - m1:real^3)`);
(ABBREV_TAC `N = projection (s2 - m) (p - m:real^3)`);
(NEW_GOAL `M = N:real^3`);
(NEW_GOAL `?r. N = r % M:real^3`);
(ASM_REWRITE_TAC[]);
(NEW_GOAL `projection (s2 - m) (n - m:real^3) = n - s2`);
(REWRITE_TAC[projection_proj_point; ASSUME `n' = s2 - m:real^3`;
ASSUME `proj_point (s2 - m) (n - m) = n':real^3`]);
(VECTOR_ARITH_TAC);
(REWRITE_WITH `circumcenter (set_of_list vl) = s2:real^3`);
(ASM_MESON_TAC[]);
(REWRITE_TAC[ASSUME `projection (s2 - m) (n - m) = n - s2:real^3`]);
(UNDISCH_TAC `between n (s2,s3:real^3)`);
(UNDISCH_TAC `between s (s2,s3:real^3)`);
(REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;CONVEX_HULL_2;IN;IN_ELIM_THM]);
(REPEAT STRIP_TAC);
(REWRITE_TAC[ASSUME `n = u'' % s2 + v'' % s3:real^3`;
ASSUME `s = u' % s2 + v' % s3:real^3`]);
(REWRITE_WITH `(u' % s2 + v' % s3) - s2:real^3
= (u' % s2 + v' % s3) - (u' + v') % s2 /\
(u'' % s2 + v'' % s3) - s2
= (u'' % s2 + v'' % s3) - (u'' + v'') % s2`);
(ASM_REWRITE_TAC[VECTOR_MUL_LID]);
(REWRITE_TAC[VECTOR_ARITH `(u % s + v % r) - (u + v) % s = v % (r - s)`]);
(REWRITE_TAC[VECTOR_MUL_ASSOC]);
(REWRITE_TAC[VECTOR_ARITH `a % x = b % x <=> (a - b) % x = vec 0`]);
(REWRITE_TAC[REAL_ARITH `(r * h) * v' = r * (h * v')`]);
(ASM_CASES_TAC `h * v' = &0`);
(NEW_GOAL `F`);
(ASM_CASES_TAC `h = &0`);
(NEW_GOAL `M:real^3 = vec 0`);
(ASM_REWRITE_TAC[VECTOR_MUL_LZERO]);
(UP_ASM_TAC THEN EXPAND_TAC "M" THEN REWRITE_TAC[projection]);
(ABBREV_TAC `kts = ((p - m1) dot (s2 - m1)) / ((s2 - m1) dot (s2 - m1:real^3))`);
(REWRITE_TAC [VECTOR_ARITH `a - p - c = vec 0 <=> a = p + c`]);
(STRIP_TAC);
(NEW_GOAL `p IN affine hull {u0,u1,u2:real^3}`);
(REWRITE_TAC[ASSUME `p = m1 + kts % (s2 - m1:real^3)`]);
(MATCH_MP_TAC TRANSLATE_AFFINE_KY_LEMMA1);
(REWRITE_TAC[MESON[] `A /\ B /\ A <=> A /\ B`]);
(STRIP_TAC);
(NEW_GOAL `convex hull {u0,u1,u2:real^3} SUBSET affine hull {u0, u1, u2}`);
(REWRITE_TAC[CONVEX_HULL_SUBSET_AFFINE_HULL]);
(UNDISCH_TAC `m1 IN convex hull {u0, u1, u2:real^3}`);
(UP_ASM_TAC THEN SET_TAC[]);
(ASM_REWRITE_TAC[]);
(EXPAND_TAC "vl");
(REWRITE_TAC[set_of_list]);
(MATCH_MP_TAC Rogers.OAPVION1);
(STRIP_TAC);
(SET_TAC[]);
(REWRITE_WITH `{u0, u1, u2:real^3} = set_of_list vl`);
(EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]);
(MATCH_MP_TAC Rogers.BARV_AFFINE_INDEPENDENT);
(EXISTS_TAC `V:real^3->bool`);
(EXISTS_TAC `2`);
(ASM_REWRITE_TAC[]);
(REWRITE_WITH `vl:(real^3)list = truncate_simplex 2 ul`);
(ASM_REWRITE_TAC[]);
(EXPAND_TAC "vl");
(REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
(MATCH_MP_TAC Packing3. TRUNCATE_SIMPLEX_BARV);
(EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]);
(NEW_GOAL `~(p:real^3 IN B6)`);
(ASM_SET_TAC[IN_DIFF]);
(UP_ASM_TAC THEN EXPAND_TAC "B6");
(REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`;HD;TL]);
(ASM_REWRITE_TAC[]);
(NEW_GOAL `v' = &0`);
(ASM_MESON_TAC[REAL_ENTIRE]);
(NEW_GOAL `s = s2:real^3`);
(ASM_REWRITE_TAC[]);
(REWRITE_WITH `u' = &1`);
(ASM_REAL_ARITH_TAC);
(REWRITE_TAC[VECTOR_MUL_LID]);
(VECTOR_ARITH_TAC);
(NEW_GOAL `!w. w IN {u0,u1,u2:real^3} ==>
radV {u0,u1,u2} = dist (circumcenter {u0,u1,u2},w)`);
(MATCH_MP_TAC Rogers.OAPVION2);
(REWRITE_WITH `{u0, u1, u2:real^3} = set_of_list vl`);
(EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]);
(MATCH_MP_TAC Rogers.BARV_AFFINE_INDEPENDENT);
(EXISTS_TAC `V:real^3->bool`);
(EXISTS_TAC `2`);
(ASM_REWRITE_TAC[]);
(REWRITE_WITH `vl:(real^3)list = truncate_simplex 2 ul`);
(ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
(MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
(EXISTS_TAC `3`);
(ASM_REWRITE_TAC[]);
(ARITH_TAC);
(NEW_GOAL `hl (truncate_simplex 2 (ul:(real^3)list)) = dist (s2, u0:real^3)`);
(REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`;
TRUNCATE_SIMPLEX_EXPLICIT_2; set_of_list; HL]);
(REWRITE_WITH `s2 = circumcenter {u0,u1,u2:real^3}`);
(ASM_REWRITE_TAC[]);
(EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]);
(FIRST_ASSUM MATCH_MP_TAC);
(SET_TAC[]);
(NEW_GOAL `hl (truncate_simplex 2 (ul:(real^3)list)) = sqrt (&2)`);
(ONCE_ASM_REWRITE_TAC[]);
(REWRITE_TAC[GSYM (ASSUME `s = s2:real^3`)]);
(ONCE_REWRITE_TAC[DIST_SYM]);
(ASM_REWRITE_TAC[]);
(ASM_REAL_ARITH_TAC);
(UP_ASM_TAC THEN MESON_TAC[]);
(EXISTS_TAC `(k * v'') / (h * v')`);
(REWRITE_TAC[REAL_ARITH `k * v'' - (k * v'') / (h * v') * h * v' =
(k * v'') * (&1 - (h * v') / (h * v'))`]);
(REWRITE_WITH `(h * v') / (h * v') = &1`);
(MATCH_MP_TAC REAL_DIV_REFL);
(ASM_REWRITE_TAC[]);
(REWRITE_TAC[REAL_SUB_REFL;REAL_MUL_RZERO; VECTOR_MUL_LZERO]);
(FIRST_X_ASSUM CHOOSE_TAC);
(NEW_GOAL `r = &1`);
(ASM_CASES_TAC `r = &1`);
(ASM_REWRITE_TAC[]);
(NEW_GOAL `p IN affine hull {u0,u1,u2:real^3}`);
(MATCH_MP_TAC IN_AFFINE_HULL_KY_LEMMA3_alt);
(EXISTS_TAC `M:real^3`);
(EXISTS_TAC `r:real`);
(REWRITE_WITH `p - M = (m1:real^3) + proj_point (s2 - m1) (p - m1)`);
(EXPAND_TAC "M" THEN REWRITE_TAC[proj_point]);
(VECTOR_ARITH_TAC);
(REWRITE_WITH `p - r % M =(m:real^3) + proj_point (s2 - m) (p - m)`);
(REWRITE_TAC[GSYM (ASSUME `N = r % M:real^3`)]);
(EXPAND_TAC "N" THEN REWRITE_TAC[proj_point]);
(VECTOR_ARITH_TAC);
(REWRITE_TAC[PRO_EXP]);
(REPEAT STRIP_TAC);
(MATCH_MP_TAC TRANSLATE_AFFINE_KY_LEMMA1 );
(REWRITE_TAC[MESON[] `A /\ B /\ A <=> A /\ B`]);
(REPEAT STRIP_TAC);
(NEW_GOAL `convex hull {u0,u1,u2} SUBSET affine hull {u0,u1,u2:real^3}`);
(REWRITE_TAC[CONVEX_HULL_SUBSET_AFFINE_HULL]);
(UP_ASM_TAC THEN UNDISCH_TAC `m1:real^3 IN convex hull {u0,u1,u2}` THEN
SET_TAC[]);
(ASM_REWRITE_TAC[]);
(REWRITE_WITH `{u0, u1, u2:real^3} = set_of_list vl`);
(EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]);
(MATCH_MP_TAC Rogers.BARV_CIRCUMCENTER_EXISTS);
(EXISTS_TAC `V:real^3->bool`);
(EXISTS_TAC `2`);
(ASM_REWRITE_TAC[]);
(REWRITE_WITH `vl:(real^3)list = truncate_simplex 2 ul`);
(ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
(MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
(EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]);
(MATCH_MP_TAC TRANSLATE_AFFINE_KY_LEMMA1);
(REWRITE_TAC[MESON[] `A/\B/\A <=> A/\B`]);
(STRIP_TAC);
(MATCH_MP_TAC IN_AFFINE_HULL_3_KY_LEMMA2);
(EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `s1:real^3`);
(REPEAT STRIP_TAC);
(MATCH_MP_TAC IN_AFFINE_KY_LEMMA1);
(SET_TAC[]);
(MATCH_MP_TAC (SET_RULE`(?s. s SUBSET b /\ a IN s) ==> a IN b`));
(EXISTS_TAC `convex hull {u0, u1,u2:real^3}`);
(REWRITE_TAC[CONVEX_HULL_SUBSET_AFFINE_HULL]);
(MATCH_MP_TAC (SET_RULE`(?s. s SUBSET b /\ a IN s) ==> a IN b`));
(EXISTS_TAC `convex hull {u0, u1:real^3}`);
(STRIP_TAC);
(MATCH_MP_TAC CONVEX_HULL_SUBSET);
(SET_TAC[]);
(REWRITE_WITH `{u0, u1:real^3} = set_of_list [u0;u1]`);
(REWRITE_TAC[set_of_list]);
(EXPAND_TAC "s1");
(REWRITE_WITH `omega_list_n V [u0; u1; u2; u3] 1 =
omega_list V [u0;u1:real^3]`);
(REWRITE_TAC[OMEGA_LIST_TRUNCATE_1]);
(MATCH_MP_TAC XNHPWAB2);
(EXISTS_TAC `1`);
(REPEAT STRIP_TAC);
(ASM_REWRITE_TAC[]);
(REWRITE_WITH `[u0;u1:real^3] = truncate_simplex 1 ul`);
(ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);
(REWRITE_TAC[IN]);
(MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
(EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `1 <= 3`]);
(REWRITE_WITH `[u0;u1:real^3] = truncate_simplex 1 vl`);
(EXPAND_TAC "vl");
(REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);
(MATCH_MP_TAC (REAL_ARITH `(?s. s < b /\ a <= s) ==> a < b`));
(EXISTS_TAC `hl (vl:(real^3)list)`);
(STRIP_TAC);
(REWRITE_WITH `vl = truncate_simplex 2 (ul:(real^3)list)`);
(ASM_REWRITE_TAC[]);
(EXPAND_TAC "vl");
(REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
(ASM_REWRITE_TAC[]);
(MATCH_MP_TAC Rogers.HL_DECREASE);
(EXISTS_TAC `V:real^3->bool`);
(EXISTS_TAC `2`);
(ASM_REWRITE_TAC[ARITH_RULE `1 <= 2`;IN]);
(REWRITE_WITH `vl = truncate_simplex 2 (ul:(real^3)list)`);
(ASM_REWRITE_TAC[]);
(EXPAND_TAC "vl");
(REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
(MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
(EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]);
(ASM_REWRITE_TAC[]);
(ASM_REWRITE_TAC[]);
(REWRITE_WITH `{u0, u1, u2:real^3} = set_of_list vl`);
(EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]);
(MATCH_MP_TAC Rogers.BARV_CIRCUMCENTER_EXISTS);
(EXISTS_TAC `V:real^3->bool`);
(EXISTS_TAC `2`);
(ASM_REWRITE_TAC[]);
(REWRITE_WITH `vl:(real^3)list = truncate_simplex 2 ul`);
(ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
(MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
(EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]);
(ASM_MESON_TAC[]);
(NEW_GOAL `~(p:real^3 IN B6)`);
(ASM_SET_TAC[IN_DIFF]);
(UP_ASM_TAC THEN EXPAND_TAC "B6");
(REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`;HD;TL]);
(STRIP_TAC);
(NEW_GOAL `F`);
(ASM_MESON_TAC[]);
(ASM_MESON_TAC[]);
(REWRITE_TAC[ASSUME `N = r % M:real^3`; ASSUME `r = &1`]);
(VECTOR_ARITH_TAC);
(NEW_GOAL `norm (M:real^3) <= norm (s2 - s:real^3)`);
(REWRITE_WITH `norm (s2 - s:real^3) = norm (projection (s2 - m1) (s - m1))`);
(REWRITE_WITH `norm (s2 - s:real^3) = norm (s - s2)`);
(NORM_ARITH_TAC);
(AP_TERM_TAC);
(ASM_MESON_TAC[]);
(REWRITE_TAC[ASSUME
`h <= &1 /\ &0 <= h /\ M = h % projection (s2 - m1) (s - m1:real^3)`]);
(REWRITE_TAC[NORM_MUL;REAL_ARITH `a * b <= b <=> &0 <= b * (&1 - a)`]);
(MATCH_MP_TAC REAL_LE_MUL);
(REWRITE_TAC[NORM_POS_LE; REAL_ARITH `&0 <= a - b <=> b <= a`]);
(REWRITE_WITH `abs h = h`);
(REWRITE_TAC[REAL_ABS_REFL]);
(ASM_REWRITE_TAC[]);
(ASM_REWRITE_TAC[]);
(NEW_GOAL `norm (s2 - s:real^3) < norm (N:real^3) `);
(REWRITE_WITH `norm (s2 - s:real^3) < norm (N:real^3) <=>
norm (s2 - s) pow 2 < norm (N:real^3) pow 2`);
(MATCH_MP_TAC Pack1.bp_bdt);
(REWRITE_TAC[NORM_POS_LE]);
(REWRITE_WITH `norm (N:real^3) = norm ((p' + m) - p:real^3)`);
(REWRITE_TAC[GSYM (ASSUME `projection (s2 - m) (p - m) = N:real^3`)]);
(REWRITE_TAC[projection_proj_point]);
(REWRITE_TAC[ASSUME `proj_point (s2 - m) (p - m) = p':real^3`]);
(NORM_ARITH_TAC);
(ASM_REWRITE_TAC[]);
(NEW_GOAL `norm (s2 - s:real^3) < norm (M:real^3)`);
(ASM_MESON_TAC[]);
(ASM_REAL_ARITH_TAC);
(SET_TAC[]);
(* ======================================================================= *)
(NEW_GOAL `!y. y <= 4 /\ p IN mcell y V ul ==> y = 0`);
(REPEAT STRIP_TAC);
(NEW_GOAL `~(y = 4 \/ y = 1 \/ y = 2 \/ y = 3)`);
(ASM_SIMP_TAC[]);
(ASM_ARITH_TAC);
(NEW_GOAL `i = 0`);
(FIRST_ASSUM MATCH_MP_TAC);
(ASM_SIMP_TAC[]);
(REWRITE_TAC[ASSUME `i = 0`]);
(ASM_REWRITE_TAC[]);
(* ====================================================================== *)
(NEW_GOAL `dist (u0, p:real^3) < sqrt (&2)`);
(UP_ASM_TAC THEN REAL_ARITH_TAC);
(ASM_CASES_TAC `~(p IN rcone_gt (HD (ul:(real^3)list)) (HD (TL ul))
(hl (truncate_simplex 1 ul) / sqrt (&2))) `);
(NEW_GOAL `!y. y <= 4 /\ p IN mcell y V ul ==>
~ (y = 4 \/ y = 0 \/ y = 2 \/ y = 3)`);
(REPEAT STRIP_TAC);
(NEW_GOAL `mcell 4 V ul = {}`);
(SIMP_TAC[MCELL_EXPLICIT; ARITH_RULE `4 >= 4`;mcell4]);
(COND_CASES_TAC);
(NEW_GOAL `F`);
(ASM_MESON_TAC[]);
(ASM_MESON_TAC[]);
(REFL_TAC);
(UNDISCH_TAC `p IN mcell y V ul` THEN REWRITE_TAC[ASSUME `y = 4`]);
(REWRITE_TAC[ASSUME `mcell 4 V ul = {}`]);
(SET_TAC[]);
(UNDISCH_TAC `p IN mcell y V ul` THEN REWRITE_TAC[ASSUME `y = 0`;
MCELL_EXPLICIT;mcell0]);
(STRIP_TAC);
(NEW_GOAL `~(p:real^3 IN ball (HD ul,sqrt (&2)))`);
(ASM_SET_TAC[IN_DIFF]);
(UP_ASM_TAC THEN ASM_REWRITE_TAC[HD;IN;ball;IN_ELIM_THM]);
(UNDISCH_TAC `p IN mcell y V ul` THEN REWRITE_TAC[ASSUME `y = 2`;
MCELL_EXPLICIT;mcell2]);
(COND_CASES_TAC);
(LET_TAC);
(REWRITE_TAC[IN_INTER]);
(REPEAT STRIP_TAC);
(NEW_GOAL `p:real^3 IN rcone_gt (HD ul) (HD (TL ul)) a`);
(REWRITE_TAC[RCONE_GT_GE;IN_DIFF]);
(ASM_REWRITE_TAC[]);
(REWRITE_TAC[HD;TL;IN;IN_ELIM_THM]);
(STRIP_TAC);
(NEW_GOAL `~(p:real^3 IN B3)`);
(ASM_SET_TAC[IN_DIFF]);
(UP_ASM_TAC THEN EXPAND_TAC "B3" THEN REWRITE_TAC[rcone_eq;rconesgn]);
(ASM_REWRITE_TAC[HD;TL;IN;IN_ELIM_THM;dist]);
(ASM_MESON_TAC[]);
(SET_TAC[]);
(* ======================================================================= *)
(UNDISCH_TAC `p IN mcell y V ul` THEN REWRITE_TAC[ASSUME `y = 3`;
MCELL_EXPLICIT;mcell3]);
(COND_CASES_TAC);
(NEW_GOAL `(?s. between s (omega_list_n V ul 2,omega_list_n V ul 3) /\
dist (u0,s) = sqrt (&2) /\
mxi V ul = s:real^3)`);
(MATCH_MP_TAC MXI_EXPLICIT_OLD);
(ASM_REWRITE_TAC[]);
(FIRST_X_ASSUM CHOOSE_TAC);
(UP_ASM_TAC THEN ASM_REWRITE_TAC[] THEN REPEAT STRIP_TAC);
(UP_ASM_TAC THEN ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2;set_of_list]);
(REWRITE_TAC[SET_RULE `{a,b,c} UNION {d} = {a,b,c,d}`]);
(STRIP_TAC);
(SUBGOAL_THEN `p:real^3 IN rogers V ul` MP_TAC);
(ASM_SET_TAC[IN_DIFF]);
(ASM_SIMP_TAC[ROGERS_EXPLICIT; HD]);
(ABBREV_TAC `s1 = omega_list_n V [u0; u1; u2; u3:real^3] 1`);
(ABBREV_TAC `s2 = omega_list_n V [u0; u1; u2; u3:real^3] 2`);
(ABBREV_TAC `s3 = omega_list_n V [u0; u1; u2; u3:real^3] 3`);
(STRIP_TAC);
(ABBREV_TAC `vl = [u0;u1;u2:real^3]`);
(NEW_GOAL `vl = truncate_simplex 2 ul:(real^3)list`);
(ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2] THEN EXPAND_TAC "vl");
(NEW_GOAL `barV V 2 vl`);
(ASM_REWRITE_TAC[] THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
(EXISTS_TAC `3` THEN ASM_MESON_TAC[ARITH_RULE `2 <= 3`]);
(NEW_GOAL `LENGTH (vl:(real^3)list) = 3 /\ CARD {u0,u1,u2:real^3} = 3`);
(REWRITE_WITH `{u0,u1,u2:real^3} = set_of_list vl`);
(EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]);
(REWRITE_TAC[ARITH_RULE `3 = 2 + 1`]);
(MATCH_MP_TAC Rogers.BARV_IMP_LENGTH_EQ_CARD);
(EXISTS_TAC `V:real^3->bool`);
(ASM_REWRITE_TAC[]);
(NEW_GOAL `s2:real^3 = omega_list V vl`);
(EXPAND_TAC "s2" THEN EXPAND_TAC "vl" THEN
REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
(MESON_TAC[OMEGA_LIST_TRUNCATE_2]);
(NEW_GOAL `s2 = circumcenter {u0,u1,u2:real^3}`);
(REWRITE_WITH `{u0,u1,u2:real^3} = set_of_list vl`);
(EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]);
(REWRITE_TAC[ASSUME `s2 = omega_list V vl`]);
(MATCH_MP_TAC Rogers.XNHPWAB1);
(EXISTS_TAC `2` THEN REWRITE_TAC[IN]);
(ASM_REWRITE_TAC[]);
(ASM_MESON_TAC[]);
(NEW_GOAL `dist (s2,u0:real^3) = hl (truncate_simplex 2 (ul:(real^3)list))`);
(ONCE_REWRITE_TAC[EQ_SYM_EQ]);
(REWRITE_TAC[GSYM (ASSUME `vl:(real^3)list = truncate_simplex 2 ul`)]);
(REWRITE_TAC[ASSUME `s2 = circumcenter {u0, u1, u2:real^3}`]);
(REWRITE_WITH `{u0, u1, u2:real^3} = set_of_list vl`);
(EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]);
(REWRITE_WITH `u0:real^3 = HD vl`);
(EXPAND_TAC "vl" THEN REWRITE_TAC[HD]);
(MATCH_MP_TAC Rogers.HL_EQ_DIST0);
(EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `2`);
(ASM_REWRITE_TAC[]);
(NEW_GOAL `~(s = s2:real^3)`);
(STRIP_TAC);
(NEW_GOAL `dist (u0,s:real^3) < sqrt (&2)`);
(ONCE_REWRITE_TAC[DIST_SYM]);
(REWRITE_TAC[ASSUME `s = s2:real^3`]);
(ASM_MESON_TAC[]);
(ASM_REAL_ARITH_TAC);
(NEW_GOAL `(s2:real^3) IN voronoi_list V vl`);
(SIMP_TAC[ASSUME `s2 = omega_list V vl`]);
(MATCH_MP_TAC Packing3.OMEGA_LIST_IN_VORONOI_LIST);
(EXISTS_TAC `2`);
(ASM_REWRITE_TAC[]);
(NEW_GOAL `(s3:real^3) IN voronoi_list V ul`);
(REWRITE_WITH `s3 = omega_list V ul`);
(EXPAND_TAC "s3" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`; OMEGA_LIST]);
(REWRITE_TAC[LENGTH; ARITH_RULE `SUC (SUC (SUC (SUC 0))) - 1 = 3`]);
(MATCH_MP_TAC Packing3.OMEGA_LIST_IN_VORONOI_LIST);
(EXISTS_TAC `3`);
(ASM_REWRITE_TAC[]);
(NEW_GOAL `(s3:real^3) IN voronoi_list V vl`);
(MATCH_MP_TAC (SET_RULE `(?s. a IN s /\ s SUBSET A) ==> a IN A`));
(EXISTS_TAC `voronoi_list V ul`);
(STRIP_TAC);
(ASM_REWRITE_TAC[]);
(EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
(REWRITE_TAC[VORONOI_LIST;VORONOI_SET;voronoi_closed;set_of_list;
SUBSET; IN_INTERS]);
(ONCE_REWRITE_TAC[IN]);
(REWRITE_TAC[IN_ELIM_THM]);
(REPEAT STRIP_TAC);
(FIRST_ASSUM MATCH_MP_TAC);
(EXISTS_TAC `v:real^3`);
(ASM_REWRITE_TAC[]);
(UNDISCH_TAC `v IN {u0, u1, u2:real^3}`);
(SET_TAC[]);
(NEW_GOAL `s IN voronoi_list V vl`);
(NEW_GOAL `convex (voronoi_list V vl)`);
(REWRITE_TAC[Packing3.CONVEX_VORONOI_LIST]);
(UP_ASM_TAC THEN REWRITE_TAC[convex] THEN STRIP_TAC);
(UNDISCH_TAC `between s (s2,s3:real^3)`);
(REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;CONVEX_HULL_2;IN;IN_ELIM_THM]);
(REPEAT STRIP_TAC);
(ONCE_REWRITE_TAC[GSYM IN]);
(REWRITE_TAC[ASSUME `s = u % s2 + v % s3:real^3`]);
(FIRST_ASSUM MATCH_MP_TAC);
(ASM_REWRITE_TAC[]);
(NEW_GOAL `~ (s IN affine hull {u0,u1,u2:real^3})`);
STRIP_TAC;
(NEW_GOAL `(s:real^3 - s2) dot (s - s2) = &0`);
(REWRITE_TAC[ASSUME `s2 = circumcenter {u0, u1, u2:real^3}`]);
(REWRITE_WITH `{u0, u1, u2:real^3} = set_of_list vl`);
(EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]);
(MATCH_MP_TAC MHFTTZN4);
(EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `2`);
(REPEAT STRIP_TAC);
(ASM_REWRITE_TAC[]);
(ASM_REWRITE_TAC[]);
(ASM_SIMP_TAC[IN_AFFINE_KY_LEMMA1]);
(EXPAND_TAC "vl" THEN ASM_MESON_TAC[set_of_list]);
(UP_ASM_TAC THEN REWRITE_TAC[GSYM NORM_POW_2; Trigonometry2.POW2_EQ_0;
NORM_EQ_0; VECTOR_ARITH `a - b = vec 0 <=> a = b`]);
(ASM_REWRITE_TAC[]);
(NEW_GOAL `CARD {u0, u1, u2, s:real^3} = 4`);
(ONCE_REWRITE_TAC[SET_RULE `{u0, u1, u2, s} = {s, u0, u1, u2}`]);
(REWRITE_WITH `4 = SUC (CARD {u0,u1,u2:real^3})`);
(ASM_REWRITE_TAC[]);
(ARITH_TAC);
(MATCH_MP_TAC (MESON[Geomdetail.CARD_CLAUSES_IMP]
`!s a. FINITE s /\ ~(a IN s) ==> CARD (a INSERT s) = SUC (CARD s)`));
(REWRITE_TAC[Geomdetail.FINITE6]);
(STRIP_TAC);
(NEW_GOAL `s IN affine hull {u0, u1, u2:real^3}`);
(UP_ASM_TAC THEN REWRITE_TAC[IN_AFFINE_KY_LEMMA1]);
(ASM_MESON_TAC[]);
(NEW_GOAL `~affine_dependent {u0, u1, u2, s:real^3}`);
(ONCE_REWRITE_TAC[SET_RULE `{a,b,c,d} = {d,a,b,c}`]);
(MATCH_MP_TAC AFFINE_INDEPENDENT_INSERT);
(ASM_REWRITE_TAC[]);
(REWRITE_WITH `{u0, u1, u2:real^3} = set_of_list vl`);
(EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]);
(MATCH_MP_TAC Rogers.BARV_AFFINE_INDEPENDENT);
(EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `2` THEN ASM_REWRITE_TAC[]);
(NEW_GOAL `s2 IN convex hull {u0, u1, u2:real^3}`);
(REWRITE_WITH `s2 = omega_list V vl /\ {u0, u1, u2:real^3} = set_of_list vl`);
(EXPAND_TAC "s2" THEN EXPAND_TAC "vl");
(REWRITE_TAC[OMEGA_LIST_TRUNCATE_2;set_of_list]);
(MATCH_MP_TAC Rogers.XNHPWAB2);
(EXISTS_TAC `2`);
(ASM_REWRITE_TAC[IN]);
(ASM_MESON_TAC[]);
(NEW_GOAL `s1 = inv (&2) % (u0 + u1:real^3)`);
(ONCE_REWRITE_TAC[GSYM midpoint]);
(EXPAND_TAC "s1");
(REWRITE_WITH `omega_list_n V [u0; u1; u2; u3] 1 =
omega_list_n V [u0; u1:real^3] 1`);
(REWRITE_TAC[OMEGA_LIST_TRUNCATE_1_NEW2;OMEGA_LIST_TRUNCATE_1]);
(REWRITE_TAC[OMEGA_LIST_TRUNCATE_1_NEW2]);
(REWRITE_WITH `omega_list V [u0; u1:real^3] =
circumcenter (set_of_list [u0;u1])`);
(MATCH_MP_TAC XNHPWAB1);
(EXISTS_TAC `1`);
(ASM_REWRITE_TAC[ARITH_RULE `1 <= 3`]);
(REWRITE_WITH `[u0;u1:real^3] = truncate_simplex 1 vl`);
(EXPAND_TAC "vl" THEN REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);
(REWRITE_TAC[IN] THEN STRIP_TAC);
(MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
(EXISTS_TAC `2` THEN REWRITE_TAC[ARITH_RULE `1 <= 2`]);
(ASM_REWRITE_TAC[]);
(NEW_GOAL `!i j. i < j /\ j <= 2
==> hl (truncate_simplex i (vl:(real^3)list))
< hl (truncate_simplex j vl)`);
(MATCH_MP_TAC XNHPWAB4);
(EXISTS_TAC `V:real^3->bool`);
(ASM_REWRITE_TAC[IN]);
(ASM_MESON_TAC[]);
(NEW_GOAL `hl (truncate_simplex 1 (vl:(real^3)list)) < hl (truncate_simplex 2 vl)`);
(FIRST_X_ASSUM MATCH_MP_TAC);
(ARITH_TAC);
(NEW_GOAL `truncate_simplex 2 vl = truncate_simplex 2 ul:(real^3)list`);
(EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
(REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
(MATCH_MP_TAC (REAL_ARITH `a < hl (truncate_simplex 2 (vl:(real^3)list)) /\
hl (truncate_simplex 2 vl) < b ==> a < b`));
(ASM_REWRITE_TAC[]);
(ASM_MESON_TAC[]);
(REWRITE_TAC[set_of_list;Rogers.CIRCUMCENTER_2]);
(NEW_GOAL `~(s3 IN affine hull {u0,u1,u2:real^3})`);
(STRIP_TAC);
(NEW_GOAL `(s3 - s2) dot (s3 - s2:real^3) = &0`);
(REWRITE_TAC[ASSUME `s2 = circumcenter {u0, u1, u2:real^3}`]);
(REWRITE_WITH `{u0, u1, u2:real^3} = set_of_list vl`);
(EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]);
(MATCH_MP_TAC MHFTTZN4);
(EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `2`);
(REPEAT STRIP_TAC);
(ASM_REWRITE_TAC[]);
(ASM_REWRITE_TAC[]);
(ASM_SIMP_TAC[IN_AFFINE_KY_LEMMA1]);
(EXPAND_TAC "vl" THEN ASM_MESON_TAC[set_of_list]);
(UP_ASM_TAC THEN REWRITE_TAC[GSYM NORM_POW_2; Trigonometry2.POW2_EQ_0;
NORM_EQ_0; VECTOR_ARITH `a - b = vec 0 <=> a = b`]);
(STRIP_TAC);
(UNDISCH_TAC `between s (s2,s3:real^3)`);
(REWRITE_TAC[ASSUME `s3= s2:real^3`; BETWEEN_REFL_EQ]);
(ASM_REWRITE_TAC[]);
(NEW_GOAL `p IN convex hull {u0, u1, s2, s:real^3}`);
(MATCH_MP_TAC CONVEX_HULL_KY_LEMMA_5);
(EXISTS_TAC `u2:real^3` THEN EXISTS_TAC `s3:real^3`);
(REPEAT STRIP_TAC);
(ASM_MESON_TAC[]);
(ASM_MESON_TAC[]);
(ASM_MESON_TAC[]);
(ASM_MESON_TAC[]);
(ASM_MESON_TAC[]);
(NEW_GOAL `~(p:real^3 IN B4)`);
(ASM_SET_TAC[IN_DIFF]);
(UP_ASM_TAC THEN EXPAND_TAC "B4" THEN REWRITE_TAC[ASSUME
`ul = [u0;u1;u2;u3:real^3]`; HD;TL;
ASSUME `mxi V [u0; u1; u2; u3] = s:real^3`]);
(ASM_MESON_TAC[]);
(REWRITE_TAC[IN_INTER; ASSUME `p IN convex hull {u0, u1, u2, s:real^3}`]);
(UNDISCH_TAC `p IN convex hull {u0, s1, s2, s3:real^3}`);
(REWRITE_TAC[ASSUME `s1 = inv (&2) % (u0 + u1:real^3)`;
CONVEX_HULL_4;IN;IN_ELIM_THM]);
(REPEAT STRIP_TAC);
(EXISTS_TAC `u + v * inv (&2)`);
(EXISTS_TAC `v * inv (&2)`);
(EXISTS_TAC `w:real` THEN EXISTS_TAC `z:real`);
(REPEAT STRIP_TAC);
(MATCH_MP_TAC REAL_LE_ADD);
(ASM_REWRITE_TAC[]);
(MATCH_MP_TAC REAL_LE_MUL);
(ASM_REWRITE_TAC[]);
(REAL_ARITH_TAC);
(MATCH_MP_TAC REAL_LE_MUL);
(ASM_REWRITE_TAC[]);
(REAL_ARITH_TAC);
(ASM_REWRITE_TAC[]);
(ASM_REWRITE_TAC[]);
(REWRITE_TAC[REAL_ARITH
`(u + v * inv (&2)) + v * inv (&2) + w + z = u + v + w + z`]);
(ASM_REWRITE_TAC[]);
(REWRITE_TAC[ASSUME
`p = u % u0 + v % inv (&2) % (u0 + u1) + w % s2 + z % s3:real^3`]);
(VECTOR_ARITH_TAC);
(* ========================================================================== *)
(NEW_GOAL `?m n. between p (m,n) /\ between m (u0,u1) /\ between n (s2,s:real^3)`);
(UP_ASM_TAC THEN REWRITE_TAC[CONVEX_HULL_4_IMP_2_2]);
(UP_ASM_TAC THEN REPEAT STRIP_TAC);
(NEW_GOAL `between m (u0, s1:real^3)`);
(ASM_CASES_TAC `between m (u0, s1:real^3)`);
(UP_ASM_TAC THEN MESON_TAC[]);
(NEW_GOAL `between m (s1, u1:real^3)`);
(NEW_GOAL `between m (u0, s1) \/ between m (s1, u1:real^3)`);
(MATCH_MP_TAC BETWEEN_TRANS_3_CASES);
(ASM_REWRITE_TAC[]);
(REWRITE_TAC[GSYM midpoint;BETWEEN_MIDPOINT]);
(ASM_MESON_TAC[]);
(NEW_GOAL `F`);
(NEW_GOAL `between n (s2,s3:real^3)`);
(ONCE_REWRITE_TAC[BETWEEN_SYM]);
(MATCH_MP_TAC BETWEEN_TRANS);
(EXISTS_TAC `s:real^3`);
(ONCE_REWRITE_TAC[BETWEEN_SYM]);
(ASM_MESON_TAC[]);
(UP_ASM_TAC THEN UP_ASM_TAC THEN UNDISCH_TAC `between p (m,n:real^3)`);
(REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;CONVEX_HULL_2;IN;IN_ELIM_THM]);
(REPEAT STRIP_TAC);
(UNDISCH_TAC `p = u % m + v % n:real^3`);
(REWRITE_TAC[ASSUME `m = u' % s1 + v' % u1:real^3`;
ASSUME `n = u'' % s2 + v'' % s3:real^3`]);
(REWRITE_WITH `u1 = &2 % s1 - u0:real^3`);
(REWRITE_TAC[ASSUME `s1 = inv (&2) % (u0 + u1:real^3)`]);
(VECTOR_ARITH_TAC);
(REWRITE_TAC[VECTOR_ADD_LDISTRIB;VECTOR_MUL_ASSOC]);
(REWRITE_TAC [VECTOR_ARITH
`((u * u') % s1 + (u * v') % (&2 % s1 - u0)) +
(v * u'') % s2 +
(v * v'') % s3 =
(u * (-- v')) % u0 + (u * u' + v' * &2 * u) % s1 + (v * u'') % s2 + (v * v'') % s3`]);
(STRIP_TAC);
(NEW_GOAL `u * --v' = &0`);
(MATCH_MP_TAC AFFINE_DEPENDENT_KY_LEMMA1);
(EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `s1:real^3`);
(EXISTS_TAC `s2:real^3` THEN EXISTS_TAC `s3:real^3`);
(EXISTS_TAC `p:real^3`);
(EXISTS_TAC `u * u' + v' * &2 * u`);
(EXISTS_TAC `v * u''`);
(EXISTS_TAC `v * v''`);
(NEW_GOAL `~(affine_dependent {u0,s1,s2:real^3})`);
(REWRITE_WITH `{u0,s1,s2:real^3} = {omega_list_n V vl i | i <= 2}`);
(EXPAND_TAC "s1" THEN EXPAND_TAC "s2");
(REWRITE_WITH `omega_list_n V [u0; u1; u2; u3] 1 = omega_list_n V vl 1`);
(EXPAND_TAC "vl" THEN REWRITE_TAC[OMEGA_LIST_TRUNCATE_1_NEW1; OMEGA_LIST_TRUNCATE_1]);
(REWRITE_WITH `omega_list_n V [u0; u1; u2; u3] 2 = omega_list_n V vl 2`);
(EXPAND_TAC "vl" THEN REWRITE_TAC[OMEGA_LIST_TRUNCATE_2_NEW1; OMEGA_LIST_TRUNCATE_2]);
(REWRITE_WITH `u0 = omega_list_n V vl 0`);
(REWRITE_TAC[OMEGA_LIST_N]);
(EXPAND_TAC "vl" THEN REWRITE_TAC[HD]);
(REWRITE_TAC[OMEGA_LIST_UP_TO_2]);
(MATCH_MP_TAC Rogers.AFFINE_INDEPENDENT_OMEGA_LIST_N);
(ASM_MESON_TAC[]);
(* ======================================================================== *)
(NEW_GOAL `~affine_dependent {u0, s1, s2, s3:real^3}`);
(ONCE_REWRITE_TAC[SET_RULE `{a,b,c,d} = {d,a,b,c}`]);
(MATCH_MP_TAC AFFINE_INDEPENDENT_INSERT);
STRIP_TAC;
(ASM_REWRITE_TAC[]);
(NEW_GOAL `~(s3 = s2:real^3)`);
(STRIP_TAC);
(UNDISCH_TAC `between s (s2,s3:real^3)`);
(REWRITE_TAC[ASSUME `s3= s2:real^3`; BETWEEN_REFL_EQ]);
(ASM_REWRITE_TAC[]);
(STRIP_TAC);
(NEW_GOAL `(s3 IN affine hull {u0,u1,u2:real^3})`);
(UNDISCH_TAC `s2 IN convex hull {u0,u1,u2:real^3}` THEN UP_ASM_TAC THEN
REWRITE_TAC[AFFINE_HULL_3; CONVEX_HULL_3; IN;IN_ELIM_THM;
ASSUME `s1 = inv (&2) % (u0 + u1:real^3)`]);
(REPEAT STRIP_TAC);
(REWRITE_TAC[ASSUME
`s3 = u''' % u0 + v''' % inv (&2) % (u0 + u1) + w % s2:real^3`;
ASSUME `s2 = u'''' % u0 + v'''' % u1 + w' % u2:real^3`]);
(EXISTS_TAC `u''' + v''' * inv (&2) + w * u''''`);
(EXISTS_TAC `v''' * inv (&2) + w * v''''`);
(EXISTS_TAC `w * w'`);
(STRIP_TAC);
(REWRITE_TAC[REAL_ARITH
`(u''' + v''' * inv (&2) + w * u'''') +
(v''' * inv (&2) + w * v'''') + w * w' =
(u''' + v''') + w * (u'''' + v'''' + w')`]);
(ASM_REWRITE_TAC[REAL_ARITH `(a + b) + c * &1 = a + b + c`]);
(VECTOR_ARITH_TAC);
(ASM_MESON_TAC[]);
(REPEAT STRIP_TAC);
(ASM_MESON_TAC[]);
(ONCE_REWRITE_TAC [SET_RULE `{u0, s1, s2, s3} = {s3,u0, s1, s2}`]);
(NEW_GOAL `CARD {u0,s1,s2:real^3} = 3`);
(REWRITE_WITH `{u0,s1,s2:real^3} = {omega_list_n V vl i | i <= 2}`);
(EXPAND_TAC "s1" THEN EXPAND_TAC "s2");
(REWRITE_WITH `omega_list_n V [u0; u1; u2; u3] 1 = omega_list_n V vl 1`);
(EXPAND_TAC "vl" THEN REWRITE_TAC[OMEGA_LIST_TRUNCATE_1_NEW1; OMEGA_LIST_TRUNCATE_1]);
(REWRITE_WITH `omega_list_n V [u0; u1; u2; u3] 2 = omega_list_n V vl 2`);
(EXPAND_TAC "vl" THEN REWRITE_TAC[OMEGA_LIST_TRUNCATE_2_NEW1; OMEGA_LIST_TRUNCATE_2]);
(REWRITE_WITH `u0 = omega_list_n V vl 0`);
(REWRITE_TAC[OMEGA_LIST_N]);
(EXPAND_TAC "vl" THEN REWRITE_TAC[HD]);
(REWRITE_TAC[OMEGA_LIST_UP_TO_2]);
(REWRITE_WITH `{omega_list_n V vl i | i <= 2} = IMAGE (omega_list_n V vl) {i | i <= 2}`);
(REWRITE_TAC[IMAGE]);
(SET_TAC[]);
(REWRITE_TAC[NUMSEG_LE]);
(REWRITE_WITH `IMAGE (omega_list_n V vl) (0..2) = {omega_list_n V vl i | i IN (0..2)}`);
(REWRITE_TAC[IMAGE]);
(SET_TAC[]);
(NEW_GOAL `aff_dim {omega_list_n V vl j | j IN 0..2} = &2`);
(MATCH_MP_TAC XNHPWAB3);
(ASM_MESON_TAC[IN]);
(NEW_GOAL `aff_dim {omega_list_n V vl i | i IN 0..2} <=
&(CARD {omega_list_n V vl i | i IN 0..2}) - &1`);
(MATCH_MP_TAC AFF_DIM_LE_CARD);
(REWRITE_WITH `{omega_list_n V vl i | i IN (0..2)} = IMAGE (omega_list_n V vl) (0..2)`);
(REWRITE_TAC[IMAGE]);
(SET_TAC[]);
(REWRITE_TAC[GSYM NUMSEG_LE]);
(REWRITE_WITH `IMAGE (omega_list_n V vl) {i | i <= 2} = {omega_list_n V vl i | i <= 2}`);
(REWRITE_TAC[IMAGE]);
(SET_TAC[]);
(REWRITE_TAC[OMEGA_LIST_UP_TO_2;Geomdetail.FINITE6]);
(UP_ASM_TAC THEN REWRITE_TAC[ARITH_RULE `a:int <= b - &1 <=> a + &1 <= b`]);
(REWRITE_TAC[ASSUME `aff_dim {omega_list_n V vl j | j IN 0..2} = &2`;
ARITH_RULE `&2 + &1 = &3:int`; INT_OF_NUM_LE]);
(STRIP_TAC);
(NEW_GOAL `CARD {omega_list_n V vl i | i IN 0..2} <= 3`);
(REWRITE_WITH `{omega_list_n V vl i | i IN (0..2)} = IMAGE (omega_list_n V vl) (0..2)`);
(REWRITE_TAC[IMAGE]);
(SET_TAC[]);
(REWRITE_TAC[GSYM NUMSEG_LE]);
(REWRITE_WITH `IMAGE (omega_list_n V vl) {i | i <= 2} = {omega_list_n V vl i | i <= 2}`);
(REWRITE_TAC[IMAGE]);
(SET_TAC[]);
(REWRITE_TAC[OMEGA_LIST_UP_TO_2; Geomdetail.CARD3]);
(ASM_ARITH_TAC);
(REWRITE_WITH `4 = SUC (CARD {u0, s1, s2:real^3})`);
(ASM_REWRITE_TAC[]);
(ARITH_TAC);
(MATCH_MP_TAC (MESON[Geomdetail.CARD_CLAUSES_IMP]
`!a s. FINITE s /\ ~(a IN s) ==> CARD (a INSERT s) = SUC (CARD s)`));
(REWRITE_TAC[Geomdetail.FINITE6]);
(STRIP_TAC);
(NEW_GOAL `~(s3 IN affine hull {u0,s1,s2:real^3})`);
(STRIP_TAC);
(NEW_GOAL `(s3 IN affine hull {u0,u1,u2:real^3})`);
(UNDISCH_TAC `s2 IN convex hull {u0,u1,u2:real^3}` THEN UP_ASM_TAC THEN
REWRITE_TAC[AFFINE_HULL_3; CONVEX_HULL_3; IN;IN_ELIM_THM;
ASSUME `s1 = inv (&2) % (u0 + u1:real^3)`]);
(REPEAT STRIP_TAC);
(REWRITE_TAC[ASSUME
`s3 = u''' % u0 + v''' % inv (&2) % (u0 + u1) + w % s2:real^3`;
ASSUME `s2 = u'''' % u0 + v'''' % u1 + w' % u2:real^3`]);
(EXISTS_TAC `u''' + v''' * inv (&2) + w * u''''`);
(EXISTS_TAC `v''' * inv (&2) + w * v''''`);
(EXISTS_TAC `w * w'`);
(STRIP_TAC);
(REWRITE_TAC[REAL_ARITH
`(u''' + v''' * inv (&2) + w * u'''') +
(v''' * inv (&2) + w * v'''') + w * w' =
(u''' + v''') + w * (u'''' + v'''' + w')`]);
(ASM_REWRITE_TAC[REAL_ARITH `(a + b) + c * &1 = a + b + c`]);
(VECTOR_ARITH_TAC);
(ASM_MESON_TAC[]);
(NEW_GOAL `s3 IN affine hull {u0, s1, s2:real^3}`);
(UNDISCH_TAC `s3 IN {u0, s1, s2:real^3}` THEN
REWRITE_TAC [IN_AFFINE_KY_LEMMA1]);
(ASM_MESON_TAC[]);
(ASM_MESON_TAC[]);
(REWRITE_TAC[REAL_ARITH
`u * --v' + (u * u' + v' * &2 * u) + v * u'' + v * v''
= u * (u' + v') + v * (u'' + v'')`]);
(ASM_REWRITE_TAC[REAL_MUL_RID]);
(ASM_REWRITE_TAC[]);
(REWRITE_TAC[REAL_ARITH `a * (-- b) <= &0 <=> &0 <= a * b`]);
(ASM_SIMP_TAC[REAL_LE_MUL]);
(NEW_GOAL `p IN affine hull {s1, s2, s3:real^3}`);
(REWRITE_TAC[AFFINE_HULL_3;IN;IN_ELIM_THM]);
(EXISTS_TAC `u * u' + v' * &2 * u`);
(EXISTS_TAC `v * u''`);
(EXISTS_TAC `v * v''`);
(STRIP_TAC);
(REWRITE_TAC[REAL_ARITH `(u * u' + v' * &2 * u) + v * u'' + v * v'' =
(u * (u' + v') + v * (u'' + v'')) - (u * -- v')`]);
(ASM_REWRITE_TAC[REAL_MUL_RID]);
(REAL_ARITH_TAC);
(ASM_REWRITE_TAC[]);
(VECTOR_ARITH_TAC);
(NEW_GOAL `~(p:real^3 IN B7)`);
(ASM_SET_TAC[IN_DIFF]);
(UP_ASM_TAC THEN EXPAND_TAC "B7");
(UP_ASM_TAC THEN EXPAND_TAC "s1" THEN EXPAND_TAC "s2" THEN EXPAND_TAC "s3");
(REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
(UP_ASM_TAC THEN MESON_TAC[]);
(* ========================================================================= *)
(NEW_GOAL `?q. between p (u0,q) /\ between q (n,s1:real^3)`);
(UNDISCH_TAC `between p (m,n:real^3)` THEN UP_ASM_TAC);
(REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;IN;IN_ELIM_THM; CONVEX_HULL_2]);
(REPEAT STRIP_TAC);
(EXISTS_TAC `((u' * v) / (u' * v + v')) % s1 +
(v' / (u' * v + v')) % n:real^3`);
(NEW_GOAL `~((u' * v + v') = &0)`);
(STRIP_TAC);
(NEW_GOAL `p = u0:real^3`);
(ASM_REWRITE_TAC[]);
(NEW_GOAL `u' * v = &0 /\ v' = &0`);
(NEW_GOAL `&0 <= u' * v /\ &0 <= v'`);
(ASM_SIMP_TAC [REAL_LE_MUL]);
(ASM_REAL_ARITH_TAC);
(NEW_GOAL `u' * u = &1`);
(NEW_GOAL `u' * u + (u' * v + v') = &1`);
(REWRITE_TAC[REAL_ARITH `u' * u + (u' * v + v') = u' * (u + v) + v'`]);
(ASM_MESON_TAC[REAL_MUL_RID]);
(ASM_REAL_ARITH_TAC);
(REWRITE_TAC[VECTOR_ADD_LDISTRIB;VECTOR_MUL_ASSOC]);
(ONCE_REWRITE_TAC[REAL_ARITH `a * b * c = (a * b) * c`]);
(ASM_REWRITE_TAC[]);
(VECTOR_ARITH_TAC);
(NEW_GOAL `~(p:real^3 IN B6)`);
(ASM_SET_TAC[IN_DIFF]);
(UP_ASM_TAC THEN EXPAND_TAC "B6" THEN REWRITE_TAC[
ASSUME `ul = [u0;u1;u2;u3:real^3]`; HD; TL]);
(REWRITE_TAC[ASSUME `p = u0:real^3`; AFFINE_HULL_3;IN;IN_ELIM_THM]);
(EXISTS_TAC `&1` THEN EXISTS_TAC `&0` THEN EXISTS_TAC `&0`);
(STRIP_TAC);
(REAL_ARITH_TAC);
(VECTOR_ARITH_TAC);
(STRIP_TAC);
(EXISTS_TAC `u' * u`);
(EXISTS_TAC `u' * v + v'`);
(REPEAT STRIP_TAC);
(ASM_SIMP_TAC[REAL_LE_MUL]);
(ASM_SIMP_TAC[REAL_LE_ADD;REAL_LE_MUL]);
(ASM_REWRITE_TAC[REAL_ARITH `u' * u + u' * v + v' = u' * (u + v) + v'`;
REAL_MUL_RID]);
(REWRITE_TAC[ASSUME `p = u' % m + v' % n:real^3`;
ASSUME `m = u % u0 + v % s1:real^3`;VECTOR_ADD_LDISTRIB;VECTOR_MUL_ASSOC]);
(REWRITE_TAC[VECTOR_ARITH `((u' * v + v') * (u' * v) / (u' * v + v')) % s1 =
((u' * v + v') / (u' * v + v')) % ((u' * v) % s1)`]);
(REWRITE_TAC[VECTOR_ARITH `((u' * v + v') * v' / (u' * v + v')) % n =
((u' * v + v') / (u' * v + v')) % (v' % n)`]);
(REWRITE_TAC[VECTOR_ARITH `(x + a % y) + b % z = x + m % a % y + m % b % z
<=> (m - &1) % (a % y + b % z )= vec 0`]);
(REWRITE_WITH `(u' * v + v') / (u' * v + v') = &1`);
(MATCH_MP_TAC REAL_DIV_REFL);
(ASM_REWRITE_TAC[]);
(VECTOR_ARITH_TAC);
(EXISTS_TAC `v' / (u' * v + v')`);
(EXISTS_TAC `(u' * v) / (u' * v + v')`);
(REPEAT STRIP_TAC);
(ASM_SIMP_TAC[REAL_LE_DIV;REAL_LE_ADD;REAL_LE_MUL]);
(ASM_SIMP_TAC[REAL_LE_DIV;REAL_LE_ADD;REAL_LE_MUL]);
(REWRITE_TAC[REAL_ARITH `a / x + b / x = (b + a) / x`]);
(MATCH_MP_TAC REAL_DIV_REFL);
(ASM_REWRITE_TAC[]);
(VECTOR_ARITH_TAC);
(UP_ASM_TAC THEN REPEAT STRIP_TAC);
(* ========================================================================= *)
(UNDISCH_TAC `~(p:real^3 IN
rcone_gt (HD ul) (HD (TL ul))
(hl (truncate_simplex 1 ul) / sqrt (&2)))`);
(ASM_REWRITE_TAC[HD;TL]);
(REWRITE_WITH `hl (truncate_simplex 1 [u0; u1; u2; u3:real^3]) = dist (s1, u0)`);
(REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);
(REWRITE_WITH `dist (s1,u0) = dist (circumcenter (set_of_list [u0;u1:real^3]), HD [u0;u1:real^3])`);
(REWRITE_TAC[HD; set_of_list; Rogers.CIRCUMCENTER_2]);
(ASM_REWRITE_TAC[midpoint]);
(MATCH_MP_TAC Rogers.HL_EQ_DIST0);
(EXISTS_TAC `V:real^3->bool`);
(EXISTS_TAC `1`);
(ASM_REWRITE_TAC[]);
(REWRITE_WITH `[u0;u1:real^3] = truncate_simplex 1 vl`);
(EXPAND_TAC "vl" THEN REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);
(MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
(EXISTS_TAC `2`);
(ASM_REWRITE_TAC[ARITH_RULE `1 <= 2`]);
(NEW_GOAL `q:real^3 IN rcone_ge u0 u1 (dist (s1,u0) / sqrt (&2))`);
(REWRITE_TAC[rcone_ge; rconesgn;IN;IN_ELIM_THM]);
(REWRITE_WITH `(q - u0) dot (u1 - u0) =
(q - s1) dot (u1 - u0) + (s1 - u0) dot (u1 - u0:real^3)`);
(VECTOR_ARITH_TAC);
(REWRITE_WITH `(q - s1) dot (u1 - u0:real^3) = &0`);
(REWRITE_WITH `u1 - u0 = (-- &2) % (u0:real^3 - s1)`);
(ASM_REWRITE_TAC[] THEN VECTOR_ARITH_TAC);
(REWRITE_TAC[DOT_RMUL]);
(REWRITE_WITH `(q - s1) dot (u0 - s1:real^3) = &0`);
(REWRITE_WITH `s1 = circumcenter (set_of_list [u0;u1:real^3])`);
(ASM_REWRITE_TAC[set_of_list; Rogers.CIRCUMCENTER_2; midpoint]);
(MATCH_MP_TAC MHFTTZN4);
(EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `1`);
(REPEAT STRIP_TAC);
(ASM_REWRITE_TAC[]);
(REWRITE_WITH `[u0;u1:real^3] = truncate_simplex 1 vl`);
(EXPAND_TAC "vl" THEN REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);
(MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
(EXISTS_TAC `2`);
(ASM_REWRITE_TAC[ARITH_RULE `1 <= 2`]);
(MATCH_MP_TAC IN_AFFINE_KY_LEMMA1);
(NEW_GOAL `n IN voronoi_list V [u0; u1:real^3]`);
(NEW_GOAL `s2 IN voronoi_list V [u0; u1:real^3]`);
(NEW_GOAL `(s2:real^3) IN voronoi_list V vl`);
(SIMP_TAC[ASSUME `s2 = omega_list V vl`]);
(MATCH_MP_TAC Packing3.OMEGA_LIST_IN_VORONOI_LIST);
(EXISTS_TAC `2`);
(ASM_REWRITE_TAC[]);
(MATCH_MP_TAC (SET_RULE `(?s. a IN s /\ s SUBSET A) ==> a IN A`));
(EXISTS_TAC `voronoi_list V vl`);
(STRIP_TAC);
(ASM_REWRITE_TAC[]);
(EXPAND_TAC "vl");
(REWRITE_TAC[VORONOI_LIST;VORONOI_SET;voronoi_closed;set_of_list;
SUBSET; IN_INTERS]);
(ONCE_REWRITE_TAC[IN]);
(REWRITE_TAC[IN_ELIM_THM]);
(REPEAT STRIP_TAC);
(FIRST_ASSUM MATCH_MP_TAC);
(EXISTS_TAC `v:real^3`);
(ASM_REWRITE_TAC[]);
(UNDISCH_TAC `v IN {u0, u1:real^3}`);
(SET_TAC[]);
(NEW_GOAL `s3 IN voronoi_list V [u0; u1]`);
(MATCH_MP_TAC (SET_RULE `(?s. a IN s /\ s SUBSET A) ==> a IN A`));
(EXISTS_TAC `voronoi_list V vl`);
(STRIP_TAC);
(ASM_REWRITE_TAC[]);
(EXPAND_TAC "vl");
(REWRITE_TAC[VORONOI_LIST;VORONOI_SET;voronoi_closed;set_of_list;
SUBSET; IN_INTERS]);
(ONCE_REWRITE_TAC[IN]);
(REWRITE_TAC[IN_ELIM_THM]);
(REPEAT STRIP_TAC);
(FIRST_ASSUM MATCH_MP_TAC);
(EXISTS_TAC `v:real^3`);
(ASM_REWRITE_TAC[]);
(UNDISCH_TAC `v IN {u0, u1:real^3}`);
(SET_TAC[]);
(NEW_GOAL `convex (voronoi_list V [u0;u1:real^3])`);
(REWRITE_TAC[Packing3.CONVEX_VORONOI_LIST]);
(UP_ASM_TAC THEN REWRITE_TAC[convex] THEN STRIP_TAC);
(SUBGOAL_THEN `between n (s2,s3:real^3)` MP_TAC);
(ONCE_REWRITE_TAC[BETWEEN_SYM]);
(MATCH_MP_TAC BETWEEN_TRANS);
(EXISTS_TAC `s:real^3`);
(ONCE_REWRITE_TAC[BETWEEN_SYM]);
(ASM_REWRITE_TAC[]);
(REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;CONVEX_HULL_2;IN;IN_ELIM_THM]);
(REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[GSYM IN]);
(REWRITE_TAC[ASSUME `n = u % s2 + v % s3:real^3`]);
(FIRST_ASSUM MATCH_MP_TAC);
(ASM_REWRITE_TAC[]);
(UNDISCH_TAC `between q (n,s1:real^3)`);
(REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;CONVEX_HULL_2;IN;IN_ELIM_THM]);
(REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[GSYM IN]);
(REWRITE_TAC[ASSUME `q = u % n + v % s1:real^3`]);
(NEW_GOAL `convex (voronoi_list V [u0;u1:real^3])`);
(REWRITE_TAC[Packing3.CONVEX_VORONOI_LIST]);
(UP_ASM_TAC THEN REWRITE_TAC[convex] THEN STRIP_TAC);
(FIRST_ASSUM MATCH_MP_TAC);
(ASM_REWRITE_TAC[]);
(REWRITE_TAC[GSYM (ASSUME `s1 = inv (&2) % (u0 + u1:real^3)`)]);
(REWRITE_WITH `s1 = omega_list V [u0;u1:real^3]`);
(EXPAND_TAC "s1");
(REWRITE_TAC[OMEGA_LIST_TRUNCATE_1]);
(MATCH_MP_TAC Packing3.OMEGA_LIST_IN_VORONOI_LIST);
(EXISTS_TAC `1`);
(REWRITE_WITH `[u0;u1:real^3] = truncate_simplex 1 ul`);
(ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);
(MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
(EXISTS_TAC `3`);
(ASM_REWRITE_TAC[ARITH_RULE `1 <= 3`]);
(MATCH_MP_TAC IN_AFFINE_KY_LEMMA1);
(REWRITE_TAC[set_of_list] THEN SET_TAC[]);
(REAL_ARITH_TAC);
(REWRITE_WITH `(s1 - u0) dot (u1 - u0:real^3) = dist (s1,u0) * dist (u1,u0)`);
(REWRITE_TAC[dist]);
(REWRITE_TAC [NORM_CAUCHY_SCHWARZ_EQ]);
(REWRITE_TAC[ASSUME `s1 = inv (&2) % (u0 + u1:real^3)`;
VECTOR_ARITH `inv (&2) % (u0 + u1) - u0 = inv (&2) % (u1 - u0)`]);
(REWRITE_TAC[NORM_MUL; VECTOR_MUL_ASSOC; REAL_ABS_MUL]);
(REWRITE_WITH `abs (inv (&2)) = inv (&2)`);
(REWRITE_TAC[REAL_ABS_REFL]);
(REAL_ARITH_TAC);
(VECTOR_ARITH_TAC);
(REWRITE_TAC[REAL_ADD_LID; REAL_ARITH `a * b >= x * b * a / t <=>
&0 <= a * b * (&1 - x / t)`]);
(MATCH_MP_TAC REAL_LE_MUL);
(STRIP_TAC);
(REWRITE_TAC[DIST_POS_LE]);
(MATCH_MP_TAC REAL_LE_MUL);
(STRIP_TAC);
(REWRITE_TAC[DIST_POS_LE]);
(REWRITE_TAC[REAL_ARITH `&0 <= a - b <=> b <= a`]);
(REWRITE_WITH `dist (q,u0:real^3) / sqrt (&2) <= &1
<=> dist (q,u0) <= &1 * sqrt (&2) `);
(MATCH_MP_TAC REAL_LE_LDIV_EQ);
(MATCH_MP_TAC SQRT_POS_LT THEN REAL_ARITH_TAC);
(ONCE_REWRITE_TAC[DIST_SYM]);
(ONCE_REWRITE_TAC[REAL_MUL_LID]);
(NEW_GOAL `dist (u0,s1:real^3) = hl (truncate_simplex 1 [u0;u1:real^3])`);
(REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);
(REWRITE_WITH `s1 = omega_list V [u0;u1:real^3]`);
(EXPAND_TAC "s1");
(REWRITE_TAC[OMEGA_LIST_TRUNCATE_1]);
(ONCE_REWRITE_TAC[EQ_SYM_EQ]);
(ONCE_REWRITE_TAC[DIST_SYM]);
(REWRITE_WITH ` dist (omega_list V [u0; u1],u0) =
dist (omega_list V [u0; u1],HD [u0;u1:real^3])`);
(REWRITE_TAC[HD]);
(MATCH_MP_TAC Rogers.WAUFCHE2);
(EXISTS_TAC `1`);
(REWRITE_WITH `[u0;u1:real^3] = truncate_simplex 1 vl`);
(EXPAND_TAC "vl");
(ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);
(REPEAT STRIP_TAC);
(ASM_REWRITE_TAC[]);
(REWRITE_TAC[IN]);
(MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
(EXISTS_TAC `2`);
(ASM_REWRITE_TAC[ARITH_RULE `1 <= 2`]);
(NEW_GOAL `hl (truncate_simplex 1 vl) <= hl (vl:(real^3)list)`);
(MATCH_MP_TAC Rogers.HL_DECREASE);
(EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `2`);
(ASM_REWRITE_TAC[IN; ARITH_RULE `1 <= 2`]);
(NEW_GOAL `hl (vl:(real^3)list) < sqrt (&2)`);
(ONCE_ASM_REWRITE_TAC[]);
(ASM_REAL_ARITH_TAC);
(ASM_REAL_ARITH_TAC);
(NEW_GOAL `hl (truncate_simplex 1 [u0;u1:real^3]) <= hl (vl:(real^3)list)`);
(REWRITE_WITH `truncate_simplex 1 [u0;u1:real^3] =
truncate_simplex 1 vl`);
(EXPAND_TAC "vl" THEN REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);
(MATCH_MP_TAC Rogers.HL_DECREASE);
(EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `2`);
(ASM_REWRITE_TAC[IN; ARITH_RULE `1 <= 2`]);
(NEW_GOAL `hl (vl:(real^3)list) < sqrt (&2)`);
(ONCE_ASM_REWRITE_TAC[]);
(ASM_REAL_ARITH_TAC);
(NEW_GOAL `dist (u0,s1:real^3) < sqrt (&2)`);
(ONCE_ASM_REWRITE_TAC[]);
(ASM_REAL_ARITH_TAC);
(NEW_GOAL `?y. y IN {n,s1:real^3} /\
(!x. x IN convex hull {n,s1} ==> norm (x - u0) <= norm (y - u0))`);
(MATCH_MP_TAC SIMPLEX_FURTHEST_LE);
(REWRITE_TAC[Geomdetail.FINITE6]);
(SET_TAC[]);
(UP_ASM_TAC THEN REWRITE_TAC [SET_RULE `a IN {x,y} <=> a = x \/ a = y`]
THEN REPEAT STRIP_TAC);
(NEW_GOAL `dist (u0,q) <= dist (u0, n:real^3)`);
(ONCE_REWRITE_TAC[DIST_SYM] THEN REWRITE_TAC
[dist; GSYM (ASSUME `y' = n:real^3`)]);
(POP_ASSUM MATCH_MP_TAC);
(REWRITE_TAC[GSYM BETWEEN_IN_CONVEX_HULL]);
(ASM_REWRITE_TAC[]);
(NEW_GOAL `dist (u0,n:real^3) <= sqrt (&2)`);
(NEW_GOAL `?y. y IN {s2,s:real^3} /\
(!x. x IN convex hull {s2,s} ==> norm (x - u0) <= norm (y - u0))`);
(MATCH_MP_TAC SIMPLEX_FURTHEST_LE);
(REWRITE_TAC[Geomdetail.FINITE6]);
(SET_TAC[]);
(UP_ASM_TAC THEN REWRITE_TAC [SET_RULE `a IN {x,y} <=> a = x \/ a = y`]
THEN REPEAT STRIP_TAC);
(NEW_GOAL `dist (u0,n) <= dist (u0, s2:real^3)`);
(ONCE_REWRITE_TAC[DIST_SYM] THEN REWRITE_TAC
[dist; GSYM (ASSUME `y'' = s2:real^3`)]);
(POP_ASSUM MATCH_MP_TAC);
(REWRITE_TAC[GSYM BETWEEN_IN_CONVEX_HULL]);
(ASM_REWRITE_TAC[]);
(NEW_GOAL `dist (u0,s2:real^3) < sqrt (&2)`);
(ONCE_REWRITE_TAC[DIST_SYM]);
(ONCE_ASM_REWRITE_TAC[]);
(ASM_REWRITE_TAC[]);
(ASM_REAL_ARITH_TAC);
(NEW_GOAL `dist (u0,n) <= dist (u0, s:real^3)`);
(ONCE_REWRITE_TAC[DIST_SYM] THEN REWRITE_TAC
[dist; GSYM (ASSUME `y'' = s:real^3`)]);
(POP_ASSUM MATCH_MP_TAC);
(REWRITE_TAC[GSYM BETWEEN_IN_CONVEX_HULL]);
(ASM_REWRITE_TAC[]);
(ASM_REAL_ARITH_TAC);
(ASM_REAL_ARITH_TAC);
(NEW_GOAL `dist (u0,q) <= dist (u0, s1:real^3)`);
(ONCE_REWRITE_TAC[DIST_SYM] THEN REWRITE_TAC
[dist; GSYM (ASSUME `y' = s1:real^3`)]);
(POP_ASSUM MATCH_MP_TAC);
(REWRITE_TAC[GSYM BETWEEN_IN_CONVEX_HULL]);
(ASM_REWRITE_TAC[]);
(ASM_REAL_ARITH_TAC);
(* ========================================================================== *)
(NEW_GOAL `p:real^3 IN rcone_ge u0 u1 (dist (s1,u0) / sqrt (&2))`);
(UNDISCH_TAC `between p (u0,q:real^3)`);
(REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;CONVEX_HULL_2;IN;IN_ELIM_THM]);
(REPEAT STRIP_TAC);
(ONCE_REWRITE_TAC[GSYM IN]);
(REWRITE_TAC[ASSUME `p = u % u0 + v % q:real^3`]);
(REWRITE_WITH `u % u0 + v % q = u0 + v % (q - u0:real^3)`);
(REWRITE_TAC[VECTOR_ARITH `u % u0 + v % q = u0 + v % (q - u0) <=>
((u + v) - &1) % u0 = vec 0`]);
(ASM_REWRITE_TAC[]);
(VECTOR_ARITH_TAC);
(MATCH_MP_TAC RCONE_GE_TRANS);
(REWRITE_TAC[VECTOR_ARITH `u0 + q - u0:real^3 = q`]);
(ASM_REWRITE_TAC[]);
(REWRITE_TAC[RCONE_GT_GE; IN_DIFF]);
(STRIP_TAC);
(ASM_REWRITE_TAC[]);
(REWRITE_TAC[IN;IN_ELIM_THM]);
(STRIP_TAC);
(NEW_GOAL `~(p:real^3 IN B3)`);
(ASM_SET_TAC[]);
(UP_ASM_TAC THEN EXPAND_TAC "B3" THEN REWRITE_TAC[ASSUME
`ul = [u0;u1;u2;u3:real^3]`; HD;TL]);
(REWRITE_WITH `hl (truncate_simplex 1 [u0; u1; u2; u3]) = dist (s1,u0:real^3)`);
(REWRITE_WITH `truncate_simplex 1 [u0; u1; u2; u3] =
truncate_simplex 1 [u0;u1:real^3]`);
(REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);
(REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);
(REWRITE_WITH `s1 = omega_list V [u0;u1:real^3]`);
(EXPAND_TAC "s1");
(REWRITE_TAC[OMEGA_LIST_TRUNCATE_1]);
(REWRITE_WITH ` dist (omega_list V [u0; u1],u0) =
dist (omega_list V [u0; u1],HD [u0;u1:real^3])`);
(REWRITE_TAC[HD]);
(MATCH_MP_TAC Rogers.WAUFCHE2);
(EXISTS_TAC `1`);
(REWRITE_WITH `[u0;u1:real^3] = truncate_simplex 1 vl`);
(EXPAND_TAC "vl");
(ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);
(REPEAT STRIP_TAC);
(ASM_REWRITE_TAC[]);
(REWRITE_TAC[IN]);
(MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
(EXISTS_TAC `2`);
(ASM_REWRITE_TAC[ARITH_RULE `1 <= 2`]);
(NEW_GOAL `hl (truncate_simplex 1 vl) <= hl (vl:(real^3)list)`);
(MATCH_MP_TAC Rogers.HL_DECREASE);
(EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `2`);
(ASM_REWRITE_TAC[IN; ARITH_RULE `1 <= 2`]);
(NEW_GOAL `hl (vl:(real^3)list) < sqrt (&2)`);
(ONCE_ASM_REWRITE_TAC[]);
(ASM_REAL_ARITH_TAC);
(ASM_REAL_ARITH_TAC);
(REWRITE_TAC[rcone_eq;rconesgn;IN;IN_ELIM_THM]);
(UP_ASM_TAC THEN REWRITE_TAC[dist] THEN MESON_TAC[]);
(SET_TAC[]);
(NEW_GOAL `!y. y <= 4 /\ p IN mcell y V ul ==> y = 1`);
(GEN_TAC THEN STRIP_TAC);
(NEW_GOAL `~(y = 4 \/ y = 0 \/ y = 2 \/ y = 3)`);
(ASM_SIMP_TAC[]);
(ASM_ARITH_TAC);
(NEW_GOAL `i = 1`);
(FIRST_ASSUM MATCH_MP_TAC);
(ASM_REWRITE_TAC[]);
(GEN_TAC THEN STRIP_TAC);
(ASM_REWRITE_TAC[]);
(FIRST_ASSUM MATCH_MP_TAC);
(ASM_REWRITE_TAC[]);
(UP_ASM_TAC THEN REWRITE_TAC[MESON[] `~ ~ A <=> A`] THEN DISCH_TAC);
(* ======================================================================== *)
(ASM_CASES_TAC
`p IN aff_ge {u0:real^3, u1} {mxi V ul, omega_list_n V ul 3}`);
(NEW_GOAL `!y. y <= 4 /\ p IN mcell y V ul ==>
~ (y = 4 \/ y = 0 \/ y = 1 \/ y = 3)`);
(REPEAT STRIP_TAC);
(NEW_GOAL `mcell 4 V ul = {}`);
(SIMP_TAC[MCELL_EXPLICIT; ARITH_RULE `4 >= 4`;mcell4]);
(COND_CASES_TAC);
(NEW_GOAL `F`);
(ASM_MESON_TAC[]);
(ASM_MESON_TAC[]);
(REFL_TAC);
(UNDISCH_TAC `p IN mcell y V ul` THEN REWRITE_TAC[ASSUME `y = 4`]);
(REWRITE_TAC[ASSUME `mcell 4 V ul = {}`]);
(SET_TAC[]);
(UNDISCH_TAC `p IN mcell y V ul` THEN REWRITE_TAC[ASSUME `y = 0`;
MCELL_EXPLICIT;mcell0]);
(STRIP_TAC);
(NEW_GOAL `~(p:real^3 IN ball (HD ul,sqrt (&2)))`);
(ASM_SET_TAC[IN_DIFF]);
(UP_ASM_TAC THEN ASM_REWRITE_TAC[HD;IN;ball;IN_ELIM_THM]);
(UNDISCH_TAC `p IN mcell y V ul` THEN REWRITE_TAC[ASSUME `y = 1`;
MCELL_EXPLICIT;mcell1]);
(COND_CASES_TAC);
(REWRITE_TAC[IN_DIFF]);
(STRIP_TAC);
(ASM_MESON_TAC[]);
(SET_TAC[]);
(* ======================================================================= *)
(UNDISCH_TAC `p IN mcell y V ul` THEN REWRITE_TAC[ASSUME `y = 3`;
MCELL_EXPLICIT;mcell3]);
(COND_CASES_TAC);
(NEW_GOAL `(?s. between s (omega_list_n V ul 2,omega_list_n V ul 3) /\
dist (u0,s) = sqrt (&2) /\
mxi V ul = s:real^3)`);
(MATCH_MP_TAC MXI_EXPLICIT_OLD);
(ASM_REWRITE_TAC[]);
(FIRST_X_ASSUM CHOOSE_TAC);
(UP_ASM_TAC THEN ASM_REWRITE_TAC[] THEN REPEAT STRIP_TAC);
(UP_ASM_TAC THEN ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2;set_of_list]);
(REWRITE_TAC[SET_RULE `{a,b,c} UNION {d} = {a,b,c,d}`]);
(STRIP_TAC);
(ABBREV_TAC `s2 = omega_list_n V [u0; u1; u2; u3:real^3] 2`);
(ABBREV_TAC `s3 = omega_list_n V [u0; u1; u2; u3:real^3] 3`);
(NEW_GOAL `p IN aff_ge {u0, u1} {s, s3:real^3}`);
(ASM_MESON_TAC[]);
(ABBREV_TAC `vl = [u0;u1;u2:real^3]`);
(NEW_GOAL `vl = truncate_simplex 2 ul:(real^3)list`);
(ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2] THEN EXPAND_TAC "vl");
(NEW_GOAL `barV V 2 vl`);
(ASM_REWRITE_TAC[] THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
(EXISTS_TAC `3` THEN ASM_MESON_TAC[ARITH_RULE `2 <= 3`]);
(NEW_GOAL `LENGTH (vl:(real^3)list) = 3 /\ CARD {u0,u1,u2:real^3} = 3`);
(REWRITE_WITH `{u0,u1,u2:real^3} = set_of_list vl`);
(EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]);
(REWRITE_TAC[ARITH_RULE `3 = 2 + 1`]);
(MATCH_MP_TAC Rogers.BARV_IMP_LENGTH_EQ_CARD);
(EXISTS_TAC `V:real^3->bool`);
(ASM_REWRITE_TAC[]);
(NEW_GOAL `s2:real^3 = omega_list V vl`);
(EXPAND_TAC "s2" THEN EXPAND_TAC "vl" THEN
REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
(MESON_TAC[OMEGA_LIST_TRUNCATE_2]);
(NEW_GOAL `s2 = circumcenter {u0,u1,u2:real^3}`);
(REWRITE_WITH `{u0,u1,u2:real^3} = set_of_list vl`);
(EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]);
(REWRITE_TAC[ASSUME `s2 = omega_list V vl`]);
(MATCH_MP_TAC Rogers.XNHPWAB1);
(EXISTS_TAC `2` THEN REWRITE_TAC[IN]);
(ASM_REWRITE_TAC[]);
(ASM_MESON_TAC[]);
(NEW_GOAL `dist (s2,u0:real^3) = hl (truncate_simplex 2 (ul:(real^3)list))`);
(ONCE_REWRITE_TAC[EQ_SYM_EQ]);
(REWRITE_TAC[GSYM (ASSUME `vl:(real^3)list = truncate_simplex 2 ul`)]);
(REWRITE_TAC[ASSUME `s2 = circumcenter {u0, u1, u2:real^3}`]);
(REWRITE_WITH `{u0, u1, u2:real^3} = set_of_list vl`);
(EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]);
(REWRITE_WITH `u0:real^3 = HD vl`);
(EXPAND_TAC "vl" THEN REWRITE_TAC[HD]);
(MATCH_MP_TAC Rogers.HL_EQ_DIST0);
(EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `2`);
(ASM_REWRITE_TAC[]);
(NEW_GOAL `~(s = s2:real^3)`);
(STRIP_TAC);
(NEW_GOAL `dist (u0,s:real^3) < sqrt (&2)`);
(ONCE_REWRITE_TAC[DIST_SYM]);
(REWRITE_TAC[ASSUME `s = s2:real^3`]);
(ASM_MESON_TAC[]);
(ASM_REAL_ARITH_TAC);
(NEW_GOAL `(s2:real^3) IN voronoi_list V vl`);
(SIMP_TAC[ASSUME `s2 = omega_list V vl`]);
(MATCH_MP_TAC Packing3.OMEGA_LIST_IN_VORONOI_LIST);
(EXISTS_TAC `2`);
(ASM_REWRITE_TAC[]);
(NEW_GOAL `(s3:real^3) IN voronoi_list V ul`);
(REWRITE_WITH `s3 = omega_list V ul`);
(EXPAND_TAC "s3" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`; OMEGA_LIST]);
(REWRITE_TAC[LENGTH; ARITH_RULE `SUC (SUC (SUC (SUC 0))) - 1 = 3`]);
(MATCH_MP_TAC Packing3.OMEGA_LIST_IN_VORONOI_LIST);
(EXISTS_TAC `3`);
(ASM_REWRITE_TAC[]);
(NEW_GOAL `(s3:real^3) IN voronoi_list V vl`);
(MATCH_MP_TAC (SET_RULE `(?s. a IN s /\ s SUBSET A) ==> a IN A`));
(EXISTS_TAC `voronoi_list V ul`);
(STRIP_TAC);
(ASM_REWRITE_TAC[]);
(EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
(REWRITE_TAC[VORONOI_LIST;VORONOI_SET;voronoi_closed;set_of_list;
SUBSET; IN_INTERS]);
(ONCE_REWRITE_TAC[IN]);
(REWRITE_TAC[IN_ELIM_THM]);
(REPEAT STRIP_TAC);
(FIRST_ASSUM MATCH_MP_TAC);
(EXISTS_TAC `v:real^3`);
(ASM_REWRITE_TAC[]);
(UNDISCH_TAC `v IN {u0, u1, u2:real^3}`);
(SET_TAC[]);
(NEW_GOAL `s IN voronoi_list V vl`);
(NEW_GOAL `convex (voronoi_list V vl)`);
(REWRITE_TAC[Packing3.CONVEX_VORONOI_LIST]);
(UP_ASM_TAC THEN REWRITE_TAC[convex] THEN STRIP_TAC);
(UNDISCH_TAC `between s (s2,s3:real^3)`);
(REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;CONVEX_HULL_2;IN;IN_ELIM_THM]);
(REPEAT STRIP_TAC);
(ONCE_REWRITE_TAC[GSYM IN]);
(REWRITE_TAC[ASSUME `s = u % s2 + v % s3:real^3`]);
(FIRST_ASSUM MATCH_MP_TAC);
(ASM_REWRITE_TAC[]);
(NEW_GOAL `~ (s IN affine hull {u0,u1,u2:real^3})`);
STRIP_TAC;
(NEW_GOAL `(s:real^3 - s2) dot (s - s2) = &0`);
(REWRITE_TAC[ASSUME `s2 = circumcenter {u0, u1, u2:real^3}`]);
(REWRITE_WITH `{u0, u1, u2:real^3} = set_of_list vl`);
(EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]);
(MATCH_MP_TAC MHFTTZN4);
(EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `2`);
(REPEAT STRIP_TAC);
(ASM_REWRITE_TAC[]);
(ASM_REWRITE_TAC[]);
(ASM_SIMP_TAC[IN_AFFINE_KY_LEMMA1]);
(EXPAND_TAC "vl" THEN ASM_MESON_TAC[set_of_list]);
(UP_ASM_TAC THEN REWRITE_TAC[GSYM NORM_POW_2; Trigonometry2.POW2_EQ_0;
NORM_EQ_0; VECTOR_ARITH `a - b = vec 0 <=> a = b`]);
(ASM_REWRITE_TAC[]);
(NEW_GOAL `~affine_dependent {u0, u1, u2, s:real^3}`);
(ONCE_REWRITE_TAC[SET_RULE `{a,b,c,d} = {d,a,b,c}`]);
(MATCH_MP_TAC AFFINE_INDEPENDENT_INSERT);
(ASM_REWRITE_TAC[]);
(REWRITE_WITH `{u0, u1, u2:real^3} = set_of_list vl`);
(EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]);
(MATCH_MP_TAC Rogers.BARV_AFFINE_INDEPENDENT);
(EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `2` THEN ASM_REWRITE_TAC[]);
(NEW_GOAL `s2 IN convex hull {u0, u1, u2:real^3}`);
(REWRITE_WITH `s2 = omega_list V vl /\ {u0, u1, u2:real^3} = set_of_list vl`);
(EXPAND_TAC "s2" THEN EXPAND_TAC "vl");
(REWRITE_TAC[OMEGA_LIST_TRUNCATE_2;set_of_list]);
(MATCH_MP_TAC Rogers.XNHPWAB2);
(EXISTS_TAC `2`);
(ASM_REWRITE_TAC[IN]);
(ASM_MESON_TAC[]);
(NEW_GOAL `~ (s3 IN affine hull {u0,u1,u2:real^3})`);
STRIP_TAC;
(NEW_GOAL `(s3:real^3 - s2) dot (s3 - s2) = &0`);
(REWRITE_TAC[ASSUME `s2 = circumcenter {u0, u1, u2:real^3}`]);
(REWRITE_WITH `{u0, u1, u2:real^3} = set_of_list vl`);
(EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]);
(MATCH_MP_TAC MHFTTZN4);
(EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `2`);
(REPEAT STRIP_TAC);
(ASM_REWRITE_TAC[]);
(ASM_REWRITE_TAC[]);
(ASM_SIMP_TAC[IN_AFFINE_KY_LEMMA1]);
(EXPAND_TAC "vl" THEN ASM_MESON_TAC[set_of_list]);
(UP_ASM_TAC THEN REWRITE_TAC[GSYM NORM_POW_2; Trigonometry2.POW2_EQ_0;
NORM_EQ_0; VECTOR_ARITH `a - b = vec 0 <=> a = b`]);
(REPEAT STRIP_TAC);
(UNDISCH_TAC `between s (s2,s3:real^3)`);
(REWRITE_TAC[ASSUME `s3 = s2:real^3`]);
(REWRITE_TAC[BETWEEN_REFL_EQ]);
(ASM_MESON_TAC[]);
(NEW_GOAL `DISJOINT {u0,u1} {s, s3:real^3}`);
(REWRITE_TAC[DISJOINT]);
(MATCH_MP_TAC (SET_RULE `~ (a IN s) /\ ~ (b IN s) ==> s INTER {a, b} = {}`));
(REPEAT STRIP_TAC);
(NEW_GOAL `s IN affine hull {u0, u1,u2:real^3}`);
(MATCH_MP_TAC IN_AFFINE_KY_LEMMA1);
(UP_ASM_TAC THEN SET_TAC[]);
(ASM_MESON_TAC[]);
(NEW_GOAL `s3 IN affine hull {u0, u1,u2:real^3}`);
(MATCH_MP_TAC IN_AFFINE_KY_LEMMA1);
(UP_ASM_TAC THEN SET_TAC[]);
(ASM_MESON_TAC[]);
(UNDISCH_TAC `p IN aff_ge {u0, u1} {s, s3:real^3}`);
(ASM_SIMP_TAC[AFF_GE_2_2]);
(REWRITE_TAC[IN;IN_ELIM_THM]);
(NEW_GOAL `?k1 k2. k1 + k2 = &1 /\ k2 <= &0 /\ k1 % s + k2 % s2 = s3:real^3`);
(UNDISCH_TAC `between s (s2,s3:real^3)`);
(REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;CONVEX_HULL_2;IN;IN_ELIM_THM]);
(REPEAT STRIP_TAC);
(EXISTS_TAC `&1 / v` THEN EXISTS_TAC ` -- u / v`);
(NEW_GOAL `~(v = &0)`);
(STRIP_TAC);
(NEW_GOAL `s = s2:real^3`);
(REWRITE_TAC[ASSUME `s = u % s2 + v % s3:real^3`]);
(REWRITE_WITH `v = &0 /\ u = &1`);
(ASM_REAL_ARITH_TAC);
(VECTOR_ARITH_TAC);
(ASM_MESON_TAC[]);
(REPEAT STRIP_TAC);
(REWRITE_TAC[REAL_ARITH `&1 / v + --u / v = (&1 - u) / v`]);
(REWRITE_WITH `&1 - u = v`);
(ASM_REAL_ARITH_TAC);
(ASM_SIMP_TAC[REAL_DIV_REFL]);
(REWRITE_TAC[REAL_ARITH `--u / v <= &0 <=> &0 <= u / v`]);
(ASM_SIMP_TAC[REAL_LE_DIV]);
(REWRITE_TAC[ASSUME `s = u % s2 + v % s3:real^3`]);
(REWRITE_TAC[VECTOR_ADD_LDISTRIB;VECTOR_MUL_ASSOC]);
(REWRITE_TAC[VECTOR_ARITH
`((&1 / v * u) % s2 + (&1 / v * v) % s3) + --u / v % s2 = s3 <=>
(v / v - &1) % s3 = vec 0`]);
(REWRITE_WITH `v / v = &1`);
(ASM_SIMP_TAC[REAL_DIV_REFL]);
(VECTOR_ARITH_TAC);
(FIRST_X_ASSUM CHOOSE_TAC THEN FIRST_X_ASSUM CHOOSE_TAC);
(REWRITE_WITH `s3 = k1 % s + k2 % s2:real^3`);
(ASM_REWRITE_TAC[]);
(UNDISCH_TAC `s2 IN convex hull {u0, u1, u2:real^3}`);
(REWRITE_TAC[CONVEX_HULL_3; IN_ELIM_THM; IN]);
(REPEAT STRIP_TAC);
(UP_ASM_TAC THEN REWRITE_TAC[ASSUME `s2 = u % u0 + v % u1 + w % u2:real^3`]);
(REWRITE_TAC [VECTOR_ADD_LDISTRIB;VECTOR_MUL_ASSOC]);
(REWRITE_TAC[VECTOR_ARITH `t1 % u0 + t2 % u1 + t3 % s + (t4 * k1) % s +
((t4 * k2) * u) % u0 + ((t4 * k2) * v) % u1 +
((t4 * k2) * w) % u2 = (t4 * k2 * w) % u2 +
(t1 + t4 * k2 * u) % u0 + (t2 + t4 * k2 * v) % u1 + (t3 + t4 * k1) % s`]);
(STRIP_TAC);
(NEW_GOAL `t4 * k2 * w = &0`);
(MATCH_MP_TAC AFFINE_DEPENDENT_KY_LEMMA1);
(EXISTS_TAC `u2:real^3` THEN EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `u1:real^3` THEN EXISTS_TAC `s:real^3` THEN EXISTS_TAC `p:real^3`);
(EXISTS_TAC `t1 + t4 * k2 * u`);
(EXISTS_TAC `t2 + t4 * k2 * v`);
(EXISTS_TAC `t3 + t4 * k1`);
(ASM_REWRITE_TAC[]);
(REPEAT STRIP_TAC);
(UP_ASM_TAC THEN REWRITE_TAC[] THEN ONCE_REWRITE_TAC[SET_RULE
`{u2, u0, u1, s} = {u0, u1, u2, s}`]);
(ASM_REWRITE_TAC[]);
(ONCE_REWRITE_TAC[SET_RULE
`{u2, u0, u1, s} = {s, u0, u1, u2}`]);
(REWRITE_WITH `4 = SUC (CARD {u0,u1,u2:real^3})`);
(ASM_REWRITE_TAC[]);
(ARITH_TAC);
(MATCH_MP_TAC (MESON[Geomdetail.CARD_CLAUSES_IMP]
`!s a. FINITE s /\ ~(a IN s) ==> CARD (a INSERT s) = SUC (CARD s)`));
(REWRITE_TAC[Geomdetail.FINITE6]);
(STRIP_TAC);
(NEW_GOAL `s IN affine hull {u0, u1, u2:real^3}`);
(UP_ASM_TAC THEN REWRITE_TAC[IN_AFFINE_KY_LEMMA1]);
(ASM_MESON_TAC[]);
(REWRITE_TAC[GSYM (ASSUME `p =
(t4 * k2 * w) % u2 +
(t1 + t4 * k2 * u) % u0 +
(t2 + t4 * k2 * v) % u1 +
(t3 + t4 * k1) % s:real^3`)]);
(ONCE_REWRITE_TAC[SET_RULE
`{u2, u0, u1, s} = {u0, u1, u2,s}`]);
(ASM_REWRITE_TAC[]);
(REWRITE_TAC[REAL_ARITH
`t4 * k2 * w + (t1 + t4 * k2 * u) + (t2 + t4 * k2 * v) + t3 + t4 * k1 =
t1 + t2 + t3 + t4 * (k1 + k2 * (u + v + w))`]);
(ASM_REWRITE_TAC[REAL_MUL_RID]);
(NEW_GOAL `&0 <= -- k2`);
(ASM_REAL_ARITH_TAC);
(REWRITE_TAC[REAL_ARITH `a * b * c <= &0 <=> &0 <= a * c * (-- b)`]);
(ASM_SIMP_TAC[REAL_LE_MUL]);
(NEW_GOAL `p IN affine hull {u0,u1,s:real^3}`);
(REWRITE_TAC[AFFINE_HULL_3;IN;IN_ELIM_THM]);
(EXISTS_TAC `t1 + t4 * k2 * u`);
(EXISTS_TAC `t2 + t4 * k2 * v`);
(EXISTS_TAC `t3 + t4 * k1`);
(ASM_REWRITE_TAC[VECTOR_MUL_LZERO;VECTOR_ADD_LID]);
(REWRITE_TAC[REAL_ARITH
`(t1 + t4 * k2 * u) + (t2 + t4 * k2 * v) + t3 + t4 * k1
= (t1 + t2 + t3 + t4 * (k1 + k2 * (u + v + w))) - (t4 * k2 * w)`]);
(ASM_REWRITE_TAC[REAL_MUL_RID]);
(REAL_ARITH_TAC);
(NEW_GOAL `~(p:real^3 IN B4)`);
(ASM_SET_TAC[]);
(UP_ASM_TAC THEN EXPAND_TAC "B4" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`; HD;TL]);
(REWRITE_WITH `mxi V [u0; u1; u2; u3] = s`);
(ASM_MESON_TAC[]);
(ASM_REWRITE_TAC[]);
(SET_TAC[]);
(NEW_GOAL `!y. y <= 4 /\ p IN mcell y V ul ==> y = 2`);
(GEN_TAC THEN STRIP_TAC);
(NEW_GOAL `~(y = 4 \/ y = 0 \/ y = 1 \/ y = 3)`);
(ASM_SIMP_TAC[]);
(ASM_ARITH_TAC);
(NEW_GOAL `i = 2`);
(FIRST_ASSUM MATCH_MP_TAC);
(ASM_REWRITE_TAC[]);
(GEN_TAC THEN STRIP_TAC);
(ASM_REWRITE_TAC[]);
(FIRST_ASSUM MATCH_MP_TAC);
(ASM_REWRITE_TAC[]);
(* ===================================================================== *)
(NEW_GOAL `!y. y <= 4 /\ p IN mcell y V ul ==>
~ (y = 4 \/ y = 0 \/ y = 1 \/ y = 2)`);
(REPEAT STRIP_TAC);
(NEW_GOAL `mcell 4 V ul = {}`);
(SIMP_TAC[MCELL_EXPLICIT; ARITH_RULE `4 >= 4`;mcell4]);
(COND_CASES_TAC);
(NEW_GOAL `F`);
(ASM_MESON_TAC[]);
(ASM_MESON_TAC[]);
(REFL_TAC);
(UNDISCH_TAC `p IN mcell y V ul` THEN REWRITE_TAC[ASSUME `y = 4`]);
(REWRITE_TAC[ASSUME `mcell 4 V ul = {}`]);
(SET_TAC[]);
(UNDISCH_TAC `p IN mcell y V ul` THEN REWRITE_TAC[ASSUME `y = 0`;
MCELL_EXPLICIT;mcell0]);
(STRIP_TAC);
(NEW_GOAL `~(p:real^3 IN ball (HD ul,sqrt (&2)))`);
(ASM_SET_TAC[IN_DIFF]);
(UP_ASM_TAC THEN ASM_REWRITE_TAC[HD;IN;ball;IN_ELIM_THM]);
(UNDISCH_TAC `p IN mcell y V ul` THEN REWRITE_TAC[ASSUME `y = 1`;
MCELL_EXPLICIT;mcell1]);
(COND_CASES_TAC);
(REWRITE_TAC[IN_DIFF]);
(STRIP_TAC);
(ASM_MESON_TAC[]);
(SET_TAC[]);
(UNDISCH_TAC `p IN mcell y V ul` THEN REWRITE_TAC[ASSUME `y = 2`;
MCELL_EXPLICIT;mcell2]);
(COND_CASES_TAC);
(LET_TAC);
(UNDISCH_TAC `~(p IN aff_ge {u0, u1} {mxi V ul, omega_list_n V ul 3})`);
(REWRITE_TAC[IN_INTER; ASSUME `ul = [u0;u1;u2;u3:real^3]`;HD;TL]);
(MESON_TAC[]);
(SET_TAC[]);
(NEW_GOAL `!y. y <= 4 /\ p IN mcell y V ul ==> y = 3`);
(GEN_TAC THEN STRIP_TAC);
(NEW_GOAL `~(y = 4 \/ y = 0 \/ y = 1 \/ y = 2)`);
(ASM_SIMP_TAC[]);
(ASM_ARITH_TAC);
(NEW_GOAL `i = 3`);
(FIRST_ASSUM MATCH_MP_TAC);
(ASM_REWRITE_TAC[]);
(GEN_TAC THEN STRIP_TAC);
(ASM_REWRITE_TAC[]);
(FIRST_ASSUM MATCH_MP_TAC);
(ASM_REWRITE_TAC[])]);;