text_formalization/packing/URRPHBZ2.hl

   1 (* ========================================================================= *)
   2 (*                FLYSPECK - BOOK FORMALIZATION                              *)
   3 (*                                                                           *)
   4 (*      Authour   : VU KHAC KY                                               *)
   5 (*      Book lemma:  URRPHBZ2                                                *)
   6 (*      Chaper    : Packing (Marchal Cells)                                  *)
   7 (*      Date      : December 2011                                            *)
   8 (*      With special thanks to John Harrison for the lemma OPEN_RCONE_GT     *)
   9 (* ========================================================================= *)
  10 (*                     FILES NEED TO BE LOADED                               *)
  11
  12 (*  flyspeck_needs "packing/marchal_cells_2.hl";;                            *)
  13 (* flyspeck_needs "packing/LEPJBDJ.hl"                                       *)
  14
  15 (* ========================================================================= *)
  16
  17 module Urrphbz2 = struct
  18
  19 open Rogers;;
  20 open Vukhacky_tactics;;
  21 open Pack_defs;;
  22 open Pack_concl;;
  23 open Pack1;;
  24 open Sphere;;
  25 open Marchal_cells;;
  26 open Emnwuus;;
  27 open Marchal_cells_2_new;;
  28 open Lepjbdj;;
  29
  30 let EVENTUALLY_RADIAL_RCONE_GE_ABC_A = prove_by_refinement (
  31  `!a u0 u1:real^3. eventually_radial u0 (rcone_ge u0 u1 a)`,
  32 [(STRIP_TAC THEN REWRITE_TAC[eventually_radial; radial]);
  33  (REPEAT STRIP_TAC);
  34  (REWRITE_TAC[SET_RULE `a INTER b SUBSET b`]);
  35  (EXISTS_TAC `&1` THEN REWRITE_TAC[REAL_ARITH `&1 > &0`]);
  36  (REPEAT STRIP_TAC);
  37  (UNDISCH_TAC `u0 + u IN rcone_ge u0 u1 a INTER ball (u0:real^3,&1)`);
  38  (REWRITE_TAC[rcone_ge; rconesgn; IN_INTER; ball; IN; IN_ELIM_THM; dist;
  39    VECTOR_ARITH `(u + v) - u:real^3 = v /\ (u - (u + t % v)) = (--t % v)`;
  40    NORM_MUL; REAL_ABS_NEG]);
  41  (REWRITE_WITH `abs t = t`);
  42  (ASM_SIMP_TAC[REAL_ARITH `t > &0 ==> &0 <= t`; REAL_ABS_REFL]);
  43  (ASM_REWRITE_TAC[DOT_LMUL]);
  44  (STRIP_TAC);
  45  (REWRITE_TAC[REAL_ARITH `t * a >= (t * b) * c <=> &0 <= (a - b * c) * t`]);
  46  (MATCH_MP_TAC REAL_LE_MUL);
  47  (ASM_REAL_ARITH_TAC)]);;
  48
  49
  50 (* ========================================================================== *)
  51 (*      This lemma is in multivariate/flyspeck.hl                             *)
  52 (* ========================================================================== *)
  53
  54 let OPEN_RCONE_GT = prove
  55   (`!v0 v1:real^N a. open(rcone_gt v0 v1 a)`,
  56    REWRITE_TAC[rcone_gt; rconesgn] THEN
  57    GEOM_ORIGIN_TAC `v0:real^N` THEN REPEAT GEN_TAC THEN
  58    REWRITE_TAC[VECTOR_SUB_RZERO; DIST_0] THEN
  59    MP_TAC(ISPECL [`\x:real^N. lift(x dot v1 - norm x * norm v1 * a)`;
  60                   `{x:real^1 | x$1 > &0}`]
  61          CONTINUOUS_OPEN_PREIMAGE_UNIV) THEN
  62    REWRITE_TAC[OPEN_HALFSPACE_COMPONENT_GT] THEN REWRITE_TAC[GSYM drop] THEN
  63    REWRITE_TAC[IN_ELIM_THM; real_gt; REAL_SUB_LT; LIFT_DROP] THEN
  64    DISCH_THEN MATCH_MP_TAC THEN GEN_TAC THEN REWRITE_TAC[LIFT_SUB] THEN
  65    ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN REWRITE_TAC[LIFT_CMUL] THEN
  66    MATCH_MP_TAC CONTINUOUS_SUB THEN ONCE_REWRITE_TAC[DOT_SYM] THEN
  67    REWRITE_TAC[REWRITE_RULE[o_DEF] CONTINUOUS_AT_LIFT_DOT] THEN
  68    MATCH_MP_TAC CONTINUOUS_CMUL THEN
  69    REWRITE_TAC[REWRITE_RULE[o_DEF] CONTINUOUS_AT_LIFT_NORM]);;
  70
  71 let EVENTUALLY_RADIAL_RCONE_GE_ABC_B = prove_by_refinement (
  72  `!a u0 u1:real^3. ~(u0 = u1) /\ (&0 < a) /\ (a < &1) ==>
  73     eventually_radial u1 (rcone_ge u0 u1 a)`,
  74 [(STRIP_TAC THEN REWRITE_TAC[eventually_radial; radial]);
  75  (REPEAT STRIP_TAC);
  76  (REWRITE_TAC[SET_RULE `a INTER b SUBSET b`]);
  77
  78  (NEW_GOAL `u1:real^3 IN rcone_gt u0 u1 a`);
  79  (REWRITE_TAC[rcone_gt;rconesgn; IN; IN_ELIM_THM; GSYM NORM_POW_2; GSYM dist; REAL_POW_2; REAL_ARITH `x * x > x * x * a <=> &0 < (&1 - a) * x * x`]);
  80  (MATCH_MP_TAC REAL_LT_MUL);
  81  (ASM_SIMP_TAC[REAL_ARITH `&0 < a - b <=> b < a`]);
  82  (MATCH_MP_TAC REAL_LT_MUL);
  83  (ASM_SIMP_TAC[DIST_POS_LT]);
  84
  85  (NEW_GOAL `open (rcone_gt (u0:real^3) u1 a)`);
  86  (ASM_SIMP_TAC[OPEN_RCONE_GT]);
  87  (UP_ASM_TAC THEN REWRITE_TAC[open_def] THEN DISCH_TAC);
  88  (NEW_GOAL `?e. &0 < e /\
  89                    (!x'. dist (x',u1:real^3) < e ==> x' IN rcone_gt u0 u1 a)`);
  90
  91  (FIRST_ASSUM MATCH_MP_TAC);
  92  (ASM_REWRITE_TAC[]);
  93  (UP_ASM_TAC THEN STRIP_TAC THEN EXISTS_TAC `e:real`);
  94  (REPEAT STRIP_TAC);
  95  (ASM_REAL_ARITH_TAC);
  96  (REWRITE_TAC[IN_INTER] THEN STRIP_TAC);
  97  (MATCH_MP_TAC (SET_RULE `(?b. a IN b /\ b SUBSET c) ==> a IN c`));
  98  (EXISTS_TAC `rcone_gt (u0:real^3) u1 a`);
  99  (ASM_REWRITE_TAC[]);
 100  (STRIP_TAC);
 101  (FIRST_ASSUM MATCH_MP_TAC);
 102  (REWRITE_TAC[dist; VECTOR_ARITH `(a +b:real^3) - a = b`; NORM_MUL]);
 103  (REWRITE_WITH `abs t = t`);
 104  (ASM_SIMP_TAC[REAL_ABS_REFL; REAL_ARITH `t > &0 ==> &0 <= t`]);
 105  (ASM_REWRITE_TAC[]);
 106  (REWRITE_TAC[RCONE_GT_SUBSET_RCONE_GE]);
 107  (REWRITE_TAC[ball; IN; IN_ELIM_THM; dist; VECTOR_ARITH `a - (a + t % b) = (-- t) % b`; NORM_MUL; REAL_ABS_NEG]);
 108  (REWRITE_WITH `abs t = t`);
 109  (ASM_SIMP_TAC[REAL_ABS_REFL; REAL_ARITH `t > &0 ==> &0 <= t`]);
 110  (ASM_REWRITE_TAC[])]);;
 111
 112 (* ======================================================================= *)
 113
 114 let EVENTUALLY_RADIAL_AFF_GE = prove_by_refinement(
 115  `!a b c d:real^3. DISJOINT {a,b} {c, d}
 116    ==> eventually_radial a (aff_ge {a,b}{c,d})`,
 117 [(STRIP_TAC THEN REWRITE_TAC[eventually_radial; radial]);
 118  (REPEAT STRIP_TAC);
 119  (REWRITE_TAC[SET_RULE `a INTER b SUBSET b`]);
 120  (EXISTS_TAC `&1` THEN REWRITE_TAC[REAL_ARITH `&1 > &0`]);
 121  (ASM_SIMP_TAC[AFF_GE_2_2]);
 122  (REWRITE_TAC[IN_INTER; IN; IN_ELIM_THM] THEN REPEAT STRIP_TAC);
 123  (EXISTS_TAC `&1 - t * t2 - t * t3 - t * t4`);
 124  (EXISTS_TAC `t * t2` THEN EXISTS_TAC `t * t3` THEN EXISTS_TAC `t * t4`);
 125  (ASM_SIMP_TAC[REAL_LE_MUL; REAL_ARITH `t > &0 ==> &0 <= t`]);
 126  (STRIP_TAC);
 127  (REAL_ARITH_TAC);
 128  (REWRITE_WITH `u = t1 % a + t2 % b + t3 % c + t4 % d - a:real^3`);
 129  (UNDISCH_TAC `a + u:real^3 = t1 % a + t2 % b + t3 % c + t4 % d` THEN VECTOR_ARITH_TAC);
 130  (REWRITE_WITH
 131 `a + t % (t1 % a + t2 % b + t3 % c + t4 % d - a) =
 132  (&1 - t * t2 - t * t3 - t * t4) % a +
 133  (t * t2) % (b:real^3) + (t * t3) % c + (t * t4) % d
 134  <=> (t * t1 + t * t2 + t * t3 + t * t4 - t) % a = vec 0`);
 135  (VECTOR_ARITH_TAC);
 136  (ASM_REWRITE_TAC[REAL_ARITH `t * t1 + t * t2 + t * t3 + t * t4 - t = t * ((t1
 137   + t2 + t3 + t4) - &1)`; REAL_SUB_REFL; REAL_MUL_RZERO; VECTOR_MUL_LZERO]);
 138  (REWRITE_TAC[ball; IN_ELIM_THM; dist; VECTOR_ARITH `a - (a + t % s) =
 139   (-- t) % s`; NORM_MUL; REAL_ABS_NEG]);
 140  (REWRITE_WITH `abs t = t`);
 141  (ASM_SIMP_TAC[REAL_ABS_REFL; REAL_ARITH `t > &0 ==> &0 <= t`]);
 142  (ASM_REWRITE_TAC[])]);;
 143
 144 (* ======================================================================= *)
 145
 146 let FUN_AFFINE_KLEMMA = prove_by_refinement (
 147  `!a:real^3 b c d.
 148     aff_dim {a,b,c} = &2 /\ ~(d IN affine hull {a,b,c})
 149     ==> ~(a IN convex hull {b,c,d})`,
 150 [(REWRITE_TAC[CONVEX_HULL_3;AFFINE_HULL_3; IN; IN_ELIM_THM]);
 151  (REPEAT STRIP_TAC);
 152  (ASM_CASES_TAC `~(w = &0)`);
 153  (NEW_GOAL `?u v w. u + v + w = &1 /\ d = u % a + v % b + w % c:real^3`);
 154  (EXISTS_TAC `&1 / w` THEN EXISTS_TAC `-- u / w` THEN EXISTS_TAC `-- v/ w`);
 155  (STRIP_TAC);
 156  (REWRITE_TAC[REAL_ARITH `&1 / w + --u / w + --v / w = (&1 - u - v) / w`;
 157    GSYM (ASSUME `u + v + w = &1`); REAL_ARITH `(u + v + w) - u - v = w`]);
 158  (ASM_REWRITE_TAC[] THEN ASM_SIMP_TAC[REAL_DIV_REFL]);
 159  (REWRITE_TAC[VECTOR_ARITH `&1 / w % a + --u / w % b + --v / w % c =
 160    (&1 / w) % (a - u % b - v % c)`]);
 161  (ASM_REWRITE_TAC[VECTOR_ARITH `(a + b + c) - a - b = c:real^3`;   VECTOR_MUL_ASSOC]);
 162  (REWRITE_WITH `&1 / w * w = &1`);
 163  (ASM_REWRITE_TAC[GSYM Trigonometry2.NOT_0_INVERTABLE]);
 164  (VECTOR_ARITH_TAC);
 165  (ASM_MESON_TAC[]);
 166  (UP_ASM_TAC THEN REWRITE_TAC[]);
 167  (STRIP_TAC);
 168  (SWITCH_TAC THEN UP_ASM_TAC THEN ASM_REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_RID]);
 169  (STRIP_TAC);
 170  (UNDISCH_TAC `aff_dim {a, b, c:real^3} = &2`);
 171  (REWRITE_TAC[]);
 172  (ONCE_REWRITE_TAC[GSYM AFF_DIM_AFFINE_HULL]);
 173  (REWRITE_WITH `affine hull {a,b,c} = affine hull {b,c:real^3}`);
 174  (MATCH_MP_TAC AFFINE_HULLS_EQ);
 175  (REPEAT STRIP_TAC);
 176  (REWRITE_TAC[SUBSET;AFFINE_HULL_2;
 177    SET_RULE `x IN {a,b,c} <=> (x = a \/x = b \/ x = c)`; IN; IN_ELIM_THM]);
 178  (REPEAT STRIP_TAC);
 179  (EXISTS_TAC `u:real` THEN EXISTS_TAC `v:real` THEN ASM_REWRITE_TAC[]);
 180  (ASM_REAL_ARITH_TAC);
 181  (EXISTS_TAC `&1` THEN EXISTS_TAC `&0` THEN ASM_REWRITE_TAC[]);
 182  (STRIP_TAC);
 183  (ASM_REAL_ARITH_TAC);
 184  (VECTOR_ARITH_TAC);
 185  (EXISTS_TAC `&0` THEN EXISTS_TAC `&1` THEN ASM_REWRITE_TAC[]);
 186  (STRIP_TAC);
 187  (ASM_REAL_ARITH_TAC);
 188  (VECTOR_ARITH_TAC);
 189
 190  (REWRITE_TAC[SUBSET;AFFINE_HULL_3;
 191    SET_RULE `x IN {b,c} <=> (x = b \/ x = c)`; IN; IN_ELIM_THM]);
 192  (REPEAT STRIP_TAC);
 193  (EXISTS_TAC `&0` THEN EXISTS_TAC `&1` THEN EXISTS_TAC `&0` THEN ASM_REWRITE_TAC[]);
 194  (STRIP_TAC);
 195  (REAL_ARITH_TAC);
 196  (VECTOR_ARITH_TAC);
 197
 198  (EXISTS_TAC `&0` THEN EXISTS_TAC `&0` THEN EXISTS_TAC `&1` THEN ASM_REWRITE_TAC[]);
 199  (STRIP_TAC);
 200  (REAL_ARITH_TAC);
 201  (VECTOR_ARITH_TAC);
 202  (ONCE_REWRITE_TAC[AFF_DIM_AFFINE_HULL]);
 203  (REWRITE_TAC[AFF_DIM_2]);
 204  (COND_CASES_TAC);
 205  (ARITH_TAC);
 206  (ARITH_TAC)]);;
 207
 208 (* ========================================================================== *)
 209 (* ========================================================================== *)
 210 (*                  The main theorem                                          *)
 211 (* ========================================================================== *)
 212 (* ========================================================================== *)
 213
 214
 215 let URRPHBZ2 = prove_by_refinement (URRPHBZ2_concl,
 216 [(REPEAT STRIP_TAC);
 217  (SUBGOAL_THEN `? u0 u1 u2 u3. (ul:(real^3)list) = [u0:real^3;u1;u2;u3]` CHOOSE_TAC);
 218  (MP_TAC (ASSUME `barV V 3 ul`));
 219  (REWRITE_TAC[BARV_3_EXPLICIT]);
 220  (FIRST_X_ASSUM CHOOSE_TAC);
 221  (FIRST_X_ASSUM CHOOSE_TAC);
 222  (FIRST_X_ASSUM CHOOSE_TAC);
 223  (ASM_CASES_TAC `~ (mcell k V ul) (v:real^3)`);
 224  (MATCH_MP_TAC EVENTUALLY_RADIAL_NOT_IN_CLOSED_SET);
 225  (ASM_REWRITE_TAC[]);
 226  (ASM_MESON_TAC[CLOSED_MCELL]);
 227  (UP_ASM_TAC THEN REWRITE_TAC[MESON[] `~ ~A <=> A`] THEN DISCH_TAC);
 228
 229 (* ====Case 1:  k = 0 ====== *) (* FINISHED *)
 230
 231  (ASM_CASES_TAC `k = 0`);
 232  (NEW_GOAL `v = u0:real^3`);
 233  (REWRITE_WITH `u0:real^3 = HD ul`);
 234  (ASM_REWRITE_TAC[HD]);
 235  (MATCH_MP_TAC ROGERS_INTER_V_LEMMA);
 236  (EXISTS_TAC `V:real^3->bool`);
 237  (ASM_REWRITE_TAC[]);
 238  (SWITCH_TAC THEN UP_ASM_TAC THEN ASM_REWRITE_TAC[MCELL_EXPLICIT;mcell0]);
 239  (REWRITE_TAC[DIFF;IN_ELIM_THM]);
 240  (MESON_TAC[IN]);
 241  (ASM_REWRITE_TAC[]);
 242  (MATCH_MP_TAC EVENTUALLY_RADIAL_NOT_IN_CLOSED_SET );
 243  (STRIP_TAC);
 244  (REWRITE_TAC[MCELL_EXPLICIT; mcell0]);
 245  (REWRITE_TAC[DIFF;IN_ELIM_THM; MESON[] `!X Y. ~(X /\ ~Y) <=> (~X \/ Y) `]);
 246  (DISJ2_TAC);
 247  (REWRITE_TAC[HD;ball;IN;IN_ELIM_THM;DIST_REFL]);
 248  (MATCH_MP_TAC SQRT_POS_LT);
 249  (REAL_ARITH_TAC);
 250  (MATCH_MP_TAC CLOSED_MCELL);
 251  (ASM_MESON_TAC[]);
 252
 253 (* ====Case 2:  k = 1 ====== *)  (* Finished *)
 254
 255  (ASM_CASES_TAC `k = 1`);
 256  (ASM_REWRITE_TAC[MCELL_EXPLICIT; mcell1]);
 257  (COND_CASES_TAC);
 258  (REWRITE_TAC[HD;TL;TRUNCATE_SIMPLEX_EXPLICIT_1;rcone_gt;rconesgn]);
 259  (REWRITE_WITH
 260 ` rogers V [u0; u1; u2; u3:real^3] INTER cball (u0,sqrt (&2)) DIFF
 261   {x | (x - u0) dot (u1 - u0) >
 262        dist (x,u0) * dist (u1,u0) * hl [u0; u1] / sqrt (&2)} =
 263   rogers V [u0; u1; u2; u3] INTER cball (u0,sqrt (&2)) INTER
 264   {x | (x - u0) dot (u1 - u0) <=
 265        dist (x,u0) * dist (u1,u0) * hl [u0; u1] / sqrt (&2)}`);
 266  (REWRITE_TAC[Vol1.SET_EQ; IN_INTER; IN_DIFF; IN; IN_ELIM_THM]);
 267  (REPEAT STRIP_TAC);
 268  (ASM_REWRITE_TAC[]);
 269  (ASM_REWRITE_TAC[]);
 270  (ASM_REAL_ARITH_TAC);
 271  (ASM_REWRITE_TAC[]);
 272  (ASM_REWRITE_TAC[]);
 273  (ASM_REAL_ARITH_TAC);
 274
 275  (NEW_GOAL `v = u0:real^3`);
 276  (REWRITE_WITH `u0:real^3 = HD ul`);
 277  (ASM_REWRITE_TAC[HD]);
 278  (MATCH_MP_TAC ROGERS_INTER_V_LEMMA);
 279  (EXISTS_TAC `V:real^3->bool`);
 280  (ASM_REWRITE_TAC[IN]);
 281  (NEW_GOAL `mcell 1 V ul (v:real^3)`);
 282  (ASM_MESON_TAC[]);
 283  (UP_ASM_TAC THEN REWRITE_TAC[MCELL_EXPLICIT; mcell1]);
 284  (COND_CASES_TAC);
 285  (TRUONG_SET_TAC[]);
 286  (DISCH_TAC THEN NEW_GOAL `F`);
 287  (UP_ASM_TAC THEN ASM_MESON_TAC[GSYM IN; NOT_IN_EMPTY]);
 288  (UP_ASM_TAC THEN MESON_TAC[]);
 289
 290  (MATCH_MP_TAC EVENTUALLY_RADIAL_INTER);
 291  (STRIP_TAC);
 292   (* e_radial rogers *)
 293  (REWRITE_TAC[ROGERS; LENGTH; ARITH_RULE `SUC (SUC (SUC (SUC 0))) = 4`]);
 294  (REWRITE_TAC [SET_OF_0_TO_3]);
 295  (REWRITE_WITH `IMAGE (omega_list_n V [u0; u1; u2; u3:real^3]) {0, 1, 2, 3} =
 296    {omega_list_n V [u0; u1; u2; u3] 0, omega_list_n V [u0; u1; u2; u3] 1,
 297     omega_list_n V [u0; u1; u2; u3] 2, omega_list_n V [u0; u1; u2; u3] 3}`);
 298  (REWRITE_TAC[IMAGE]);
 299  (SET_TAC[]);
 300  (ABBREV_TAC `a = omega_list_n V [u0; u1; u2; u3:real^3] 0`);
 301  (REWRITE_WITH `a = u0:real^3`);
 302  (EXPAND_TAC "a" THEN REWRITE_TAC[OMEGA_LIST_N;HD]);
 303
 304  (ONCE_ASM_REWRITE_TAC[]);
 305  (MATCH_MP_TAC EVENTUALLY_RADIAL_CONVEX_HULL_4_sub1);
 306  (ABBREV_TAC `vl = [u0;u1;u2;u3:real^3]`);
 307
 308  (REWRITE_WITH `u0:real^3 = HD vl`);
 309  (EXPAND_TAC "vl" THEN ASM_REWRITE_TAC[HD]);
 310  (MATCH_MP_TAC U0_NOT_IN_CONVEX_HULL_FROM_ROGERS) ;
 311  (ASM_MESON_TAC[]);
 312
 313   (* e_radial cball *)
 314
 315  (MATCH_MP_TAC EVENTUALLY_RADIAL_INTER);
 316  (STRIP_TAC);
 317  (ASM_REWRITE_TAC[eventually_radial]);
 318  (EXISTS_TAC `&1`);
 319  (REWRITE_TAC[radial; REAL_ARITH `&1 > &0`; INTER_SUBSET]);
 320  (REPEAT STRIP_TAC);
 321  (REWRITE_WITH `cball (u0:real^3,sqrt (&2)) INTER ball (u0,&1) = ball (u0, &1)`);
 322  (MATCH_MP_TAC (SET_RULE `b SUBSET a ==> a INTER b = b`));
 323  (REWRITE_TAC[SUBSET; ball; cball; IN; IN_ELIM_THM]);
 324  (REPEAT STRIP_TAC);
 325  (NEW_GOAL `&1 < sqrt (&2)`);
 326  (REWRITE_TAC[ZERO_LT_SQRT_2]);
 327  (ASM_REAL_ARITH_TAC);
 328  (REWRITE_TAC[ball; IN; IN_ELIM_THM; dist; VECTOR_ARITH `a - (a + b:real^3) = --b`; NORM_NEG; NORM_MUL]);
 329  (REWRITE_WITH `abs t = t`);
 330  (REWRITE_TAC[REAL_ABS_REFL]);
 331  (ASM_REAL_ARITH_TAC);
 332  (ASM_REWRITE_TAC[]);
 333
 334 (* e_radial R^3 \ rcone_gt *)
 335
 336  (ASM_REWRITE_TAC[eventually_radial]);
 337  (EXISTS_TAC `&1`);
 338  (REWRITE_TAC[radial; REAL_ARITH `&1 > &0`; INTER_SUBSET; IN_INTER; IN; IN_ELIM_THM]);
 339  (REPEAT STRIP_TAC);
 340
 341  (REWRITE_WITH `((u0 + t % u) - u0) dot (u1 - u0:real^3) =
 342                   t * (((u0 + u) - u0) dot (u1 - u0))`);
 343  (VECTOR_ARITH_TAC);
 344  (REWRITE_WITH `dist (u0 + t % u,u0) = abs t * dist (u0 + u,u0:real^3)`);
 345  (REWRITE_TAC[dist; VECTOR_ARITH `(a + (b:real^3)) - a = b`; NORM_MUL]);
 346  (REWRITE_WITH `abs t = t`);
 347  (REWRITE_TAC[REAL_ABS_REFL]);
 348  (ASM_REAL_ARITH_TAC);
 349  (REWRITE_TAC [REAL_ARITH  `t * s <= (t * a) * b <=> &0 <= t * (a * b - s)`]);
 350  (MATCH_MP_TAC REAL_LE_MUL);
 351  (ASM_REAL_ARITH_TAC);
 352  (REWRITE_TAC[ball;IN_ELIM_THM]);
 353  (REWRITE_WITH `dist (u0,u0 + t % u) = abs t * norm (u:real^3)`);
 354  (REWRITE_TAC[dist; VECTOR_ARITH `(a + (b:real^3)) - a = b /\
 355                r:real^3 - (r + t) = -- t`; NORM_MUL; NORM_NEG]);
 356  (REWRITE_WITH `abs t = t`);
 357  (REWRITE_TAC[REAL_ABS_REFL]);
 358  (ASM_REAL_ARITH_TAC);
 359  (ASM_MESON_TAC[]);
 360  (REWRITE_TAC[EVENTUALLY_RADIAL_EMPTY]);
 361
 362 (* ======================================================================= *)
 363 (* ====Case 2:  k >= 4 ====== *)
 364
 365  (ASM_CASES_TAC `k >= 4`);
 366  (UNDISCH_TAC `mcell k V ul v`);
 367  (REWRITE_WITH `mcell k V ul = mcell4 V ul`);
 368  (MP_TAC MCELL_EXPLICIT THEN STRIP_TAC);
 369  (NEW_GOAL `mcell 0 V ul = mcell0 V ul /\
 370              mcell 1 V ul = mcell1 V ul /\
 371              mcell 2 V ul = mcell2 V ul /\
 372              mcell 3 V ul = mcell3 V ul /\
 373             (k >= 4 ==> mcell k V ul = mcell4 V ul)`);
 374  (ASM_REWRITE_TAC[]);
 375  (UP_ASM_TAC THEN STRIP_TAC);
 376  (FIRST_ASSUM MATCH_MP_TAC);
 377  (ASM_SIMP_TAC[]);
 378  (REWRITE_TAC[mcell4]);
 379  (COND_CASES_TAC);
 380  (ASM_REWRITE_TAC[set_of_list]);
 381  (STRIP_TAC);
 382  (ABBREV_TAC `S = {u0, u1,u2, u3:real^3}`);
 383  (ABBREV_TAC `s3 = omega_list V (ul:(real^3)list)`);
 384
 385  (NEW_GOAL `v IN {u0, u1 ,u2:real^3, u3}`);
 386  (ASM_CASES_TAC `(v:real^3) IN S`);
 387  (ASM_MESON_TAC[]);
 388  (NEW_GOAL `!x:real^3. x IN convex hull S /\ ~(x IN S)
 389                   ==> (?y. y IN S /\ norm (x - s3) < norm (y - s3))`);
 390  (MATCH_MP_TAC SIMPLEX_FURTHEST_LT_2);
 391  (EXPAND_TAC "S");
 392  (REWRITE_TAC[Geomdetail.FINITE6]);
 393  (NEW_GOAL `?y:real^3. y IN S /\ norm (v - s3) < norm (y - s3)`);
 394  (FIRST_ASSUM MATCH_MP_TAC);
 395  (ASM_REWRITE_TAC[IN]);
 396  (UP_ASM_TAC THEN EXPAND_TAC "S" THEN STRIP_TAC);
 397  (NEW_GOAL `s3 IN (voronoi_closed V (y:real^3))`);
 398  (EXPAND_TAC "s3");
 399  (MATCH_MP_TAC (SET_RULE `(?b. a IN b /\ b SUBSET c) ==> a IN c`));
 400  (EXISTS_TAC `voronoi_list V (ul:(real^3)list)`);
 401  (STRIP_TAC);
 402  (MATCH_MP_TAC Packing3.OMEGA_LIST_IN_VORONOI_LIST);
 403  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]);
 404  (ASM_REWRITE_TAC[VORONOI_LIST; VORONOI_SET; set_of_list]);
 405  (NEW_GOAL `y:real^3 IN S`);
 406  (ASM_MESON_TAC[]);
 407  (ASM_SET_TAC[]);
 408  (UP_ASM_TAC THEN REWRITE_TAC[voronoi_closed; IN; IN_ELIM_THM]);
 409  (ONCE_REWRITE_TAC[DIST_SYM]);
 410  (REWRITE_TAC[dist]);
 411  (STRIP_TAC);
 412  (NEW_GOAL `F`);
 413  (NEW_GOAL `norm (y - s3) <= norm (v - s3:real^3)`);
 414  (FIRST_ASSUM MATCH_MP_TAC);
 415  (UNDISCH_TAC `v:real^3 IN V` THEN MESON_TAC[IN]);
 416  (ASM_REAL_ARITH_TAC);
 417  (ASM_MESON_TAC[]);
 418
 419 (* Case v = u0 *)
 420  (ASM_CASES_TAC `v = u0:real^3`);
 421  (ASM_REWRITE_TAC[]);
 422  (EXPAND_TAC "S");
 423  (MATCH_MP_TAC EVENTUALLY_RADIAL_CONVEX_HULL_4_sub1);
 424  (NEW_GOAL `aff_dim {u0,u1,u2,u3:real^3} = &3`);
 425  (REWRITE_WITH `{u0,u1,u2,u3:real^3} = set_of_list ul`);
 426  (ASM_REWRITE_TAC[set_of_list]);
 427  (MATCH_MP_TAC Rogers.MHFTTZN1);
 428  (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]);
 429  (STRIP_TAC);
 430  (NEW_GOAL `aff_dim {u0,u1,u2,u3:real^3} <= &3 - &1`);
 431  (REWRITE_WITH `{u0,u1,u2,u3:real^3} = u0 INSERT {u1,u2,u3:real^3}`);
 432  (SET_TAC[]);
 433  (ONCE_REWRITE_TAC[AFF_DIM_INSERT]);
 434  (COND_CASES_TAC);
 435
 436  (NEW_GOAL `CARD {u1,u2,u3:real^3} <= 3`);
 437  (REWRITE_TAC[Geomdetail.CARD3]);
 438  (NEW_GOAL `aff_dim {u1, u2, u3} <= &(CARD{u1,u2,u3:real^3}) - &1`);
 439  (MATCH_MP_TAC AFF_DIM_LE_CARD);
 440  (REWRITE_TAC[Geomdetail.FINITE6]);
 441  (ASM_ARITH_TAC);
 442  (NEW_GOAL `F`);
 443  (NEW_GOAL `u0 IN affine hull {u1,u2,u3:real^3}`);
 444  (UNDISCH_TAC `u0 IN convex hull {u1, u2, u3:real^3}`);
 445  (MATCH_MP_TAC (SET_RULE `(b SUBSET c) ==> ((a IN b) ==> (a IN c))`));
 446  (REWRITE_TAC[CONVEX_HULL_SUBSET_AFFINE_HULL]);
 447  (ASM_MESON_TAC[]);
 448  (ASM_MESON_TAC[]);
 449  (ASM_ARITH_TAC);
 450
 451 (* Case v = u1 *)
 452  (ASM_CASES_TAC `v = u1:real^3`);
 453  (ASM_REWRITE_TAC[]);
 454  (EXPAND_TAC "S");
 455  (REWRITE_WITH `{u0, u1, u2, u3} = {u1, u0, u2, u3:real^3}`);
 456  (SET_TAC[]);
 457  (MATCH_MP_TAC EVENTUALLY_RADIAL_CONVEX_HULL_4_sub1);
 458  (NEW_GOAL `aff_dim {u1, u0, u2, u3:real^3} = &3`);
 459  (REWRITE_WITH `{u1, u0, u2, u3:real^3} = set_of_list ul`);
 460  (ASM_REWRITE_TAC[set_of_list]);
 461  (EXPAND_TAC "S" THEN SET_TAC[]);
 462  (MATCH_MP_TAC Rogers.MHFTTZN1);
 463  (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]);
 464  (STRIP_TAC);
 465  (NEW_GOAL `aff_dim {u1, u0, u2, u3:real^3} <= &3 - &1`);
 466  (REWRITE_WITH `{u1, u0, u2, u3:real^3} = u1 INSERT {u0,u2,u3:real^3}`);
 467  (SET_TAC[]);
 468  (ONCE_REWRITE_TAC[AFF_DIM_INSERT]);
 469  (COND_CASES_TAC);
 470
 471  (NEW_GOAL `CARD {u0,u2,u3:real^3} <= 3`);
 472  (REWRITE_TAC[Geomdetail.CARD3]);
 473  (NEW_GOAL `aff_dim {u0, u2, u3} <= &(CARD{u0,u2,u3:real^3}) - &1`);
 474  (MATCH_MP_TAC AFF_DIM_LE_CARD);
 475  (REWRITE_TAC[Geomdetail.FINITE6]);
 476  (ASM_ARITH_TAC);
 477  (NEW_GOAL `F`);
 478  (NEW_GOAL `u1 IN affine hull {u0,u2,u3:real^3}`);
 479  (UNDISCH_TAC `u1 IN convex hull {u0, u2, u3:real^3}`);
 480  (MATCH_MP_TAC (SET_RULE `(b SUBSET c) ==> ((a IN b) ==> (a IN c))`));
 481  (REWRITE_TAC[CONVEX_HULL_SUBSET_AFFINE_HULL]);
 482  (ASM_MESON_TAC[]);
 483  (ASM_MESON_TAC[]);
 484  (ASM_ARITH_TAC);
 485
 486 (* Case v = u2 *)
 487  (ASM_CASES_TAC `v = u2:real^3`);
 488  (ASM_REWRITE_TAC[]);
 489  (EXPAND_TAC "S");
 490  (REWRITE_WITH `{u0, u1, u2, u3} = {u2, u0, u1, u3:real^3}`);
 491  (SET_TAC[]);
 492  (MATCH_MP_TAC EVENTUALLY_RADIAL_CONVEX_HULL_4_sub1);
 493  (NEW_GOAL `aff_dim {u2, u0, u1, u3:real^3} = &3`);
 494  (REWRITE_WITH `{u2, u0, u1, u3:real^3} = set_of_list ul`);
 495  (ASM_REWRITE_TAC[set_of_list]);
 496  (EXPAND_TAC "S" THEN SET_TAC[]);
 497  (MATCH_MP_TAC Rogers.MHFTTZN1);
 498  (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]);
 499  (STRIP_TAC);
 500  (NEW_GOAL `aff_dim {u2, u0, u1, u3:real^3} <= &3 - &1`);
 501  (REWRITE_WITH `{u2, u0, u1, u3:real^3} = u2 INSERT {u0,u1,u3:real^3}`);
 502  (SET_TAC[]);
 503  (ONCE_REWRITE_TAC[AFF_DIM_INSERT]);
 504  (COND_CASES_TAC);
 505  (NEW_GOAL `CARD {u0,u1,u3:real^3} <= 3`);
 506  (REWRITE_TAC[Geomdetail.CARD3]);
 507  (NEW_GOAL `aff_dim {u0,u1,u3:real^3} <= &(CARD {u0,u1,u3:real^3}) - &1`);
 508  (MATCH_MP_TAC AFF_DIM_LE_CARD);
 509  (REWRITE_TAC[Geomdetail.FINITE6]);
 510  (ASM_ARITH_TAC);
 511  (NEW_GOAL `F`);
 512  (NEW_GOAL `u2 IN affine hull {u0,u1,u3:real^3}`);
 513  (UNDISCH_TAC `u2 IN convex hull {u0,u1,u3:real^3}`);
 514  (MATCH_MP_TAC (SET_RULE `(b SUBSET c) ==> ((a IN b) ==> (a IN c))`));
 515  (REWRITE_TAC[CONVEX_HULL_SUBSET_AFFINE_HULL]);
 516  (ASM_MESON_TAC[]);
 517  (ASM_MESON_TAC[]);
 518  (ASM_ARITH_TAC);
 519
 520 (* Case v = u2 *)
 521  (ASM_CASES_TAC `v = u3:real^3`);
 522  (ASM_REWRITE_TAC[]);
 523  (EXPAND_TAC "S");
 524  (REWRITE_WITH `{u0, u1, u2, u3} = {u3, u0, u1, u2:real^3}`);
 525  (SET_TAC[]);
 526  (MATCH_MP_TAC EVENTUALLY_RADIAL_CONVEX_HULL_4_sub1);
 527  (NEW_GOAL `aff_dim {u3, u0, u1, u2:real^3} = &3`);
 528  (REWRITE_WITH `{u3, u0, u1, u2:real^3} = set_of_list ul`);
 529  (ASM_REWRITE_TAC[set_of_list]);
 530  (EXPAND_TAC "S" THEN SET_TAC[]);
 531  (MATCH_MP_TAC Rogers.MHFTTZN1);
 532  (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]);
 533  (STRIP_TAC);
 534  (NEW_GOAL `aff_dim {u3, u0, u1, u2:real^3} <= &3 - &1`);
 535  (ONCE_REWRITE_TAC[AFF_DIM_INSERT]);
 536  (COND_CASES_TAC);
 537  (NEW_GOAL `CARD {u0,u1,u2:real^3} <= 3`);
 538  (REWRITE_TAC[Geomdetail.CARD3]);
 539  (NEW_GOAL `aff_dim {u0,u1,u2:real^3} <= &(CARD {u0,u1,u2:real^3}) - &1`);
 540  (MATCH_MP_TAC AFF_DIM_LE_CARD);
 541  (REWRITE_TAC[Geomdetail.FINITE6]);
 542  (ASM_ARITH_TAC);
 543  (NEW_GOAL `F`);
 544  (NEW_GOAL `u3 IN affine hull {u0,u1,u2:real^3}`);
 545  (UNDISCH_TAC `u3 IN convex hull {u0,u1,u2:real^3}`);
 546  (MATCH_MP_TAC (SET_RULE `(b SUBSET c) ==> ((a IN b) ==> (a IN c))`));
 547  (REWRITE_TAC[CONVEX_HULL_SUBSET_AFFINE_HULL]);
 548  (ASM_MESON_TAC[]);
 549  (ASM_MESON_TAC[]);
 550  (ASM_ARITH_TAC);
 551  (NEW_GOAL `F`);
 552  (ASM_SET_TAC[]);
 553  (ASM_MESON_TAC[]);
 554  (STRIP_TAC);
 555  (NEW_GOAL `v:real^3 IN {}`);
 556  (ASM_REWRITE_TAC[IN]);
 557  (NEW_GOAL `F`);
 558  (UP_ASM_TAC THEN REWRITE_TAC[NOT_IN_EMPTY]);
 559  (ASM_MESON_TAC[]);
 560
 561 (* ======================================================================= *)
 562 (* ====Case 4:  k = 3 ====== *)
 563
 564  (ASM_CASES_TAC `k = 3`);
 565  (ASM_REWRITE_TAC[MCELL_EXPLICIT; mcell3]);
 566  (COND_CASES_TAC);
 567  (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2; set_of_list]);
 568  (NEW_GOAL
 569  `V INTER mcell k V ul = set_of_list (truncate_simplex (k - 1) ul)`);
 570  (MATCH_MP_TAC LEPJBDJ);
 571  (ASM_REWRITE_TAC[ARITH_RULE `1 <= 3 /\ 3 <= 4`]);
 572  (STRIP_TAC);
 573  (NEW_GOAL `v IN mcell 3 V ul`);
 574  (ASM_SET_TAC[]);
 575  (ASM_SET_TAC[]);
 576  (UP_ASM_TAC THEN ASM_REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_2; ARITH_RULE `3 - 1 = 2`]);
 577  (STRIP_TAC);
 578
 579  (NEW_GOAL `v IN {u0, u1, u2:real^3}`);
 580  (ASM_SET_TAC[]);
 581  (ABBREV_TAC `m = mxi V [u0;u1;u2;u3:real^3]`);
 582  (REWRITE_TAC[SET_RULE `{a,b,c} UNION {d} = {a,b,c,d}`]);
 583  (NEW_GOAL `aff_dim {u0, u1, u2:real^3} = &2`);
 584  (REWRITE_WITH `{u0,u1,u2:real^3} = set_of_list (truncate_simplex 2 ul)`);
 585  (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2; set_of_list]);
 586  (MATCH_MP_TAC Rogers.MHFTTZN1);
 587  (EXISTS_TAC `V:real^3->bool`);
 588  (ASM_REWRITE_TAC[]);
 589  (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
 590  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]);
 591  (ASM_MESON_TAC[]);
 592  (NEW_GOAL `~(m IN affine hull {u0,u1,u2:real^3})`);
 593  (ABBREV_TAC `s2 = omega_list_n V [u0; u1; u2; u3] 2`);
 594  (ABBREV_TAC `s3 = omega_list_n V [u0; u1; u2; u3] 3`);
 595
 596  (NEW_GOAL `s2 IN voronoi_list V [u0;u1;u2:real^3]`);
 597  (EXPAND_TAC "s2");
 598  (REWRITE_TAC[OMEGA_LIST_N; ARITH_RULE `2 = SUC 1`]);
 599  (ASM_REWRITE_TAC[ARITH_RULE `SUC 1 = 2`; TRUNCATE_SIMPLEX_EXPLICIT_2]);
 600  (MATCH_MP_TAC CLOSEST_POINT_IN_SET);
 601  (REWRITE_TAC[Packing3.CLOSED_VORONOI_LIST]);
 602  (UNDISCH_TAC `barV V 3 ul` THEN REWRITE_TAC[BARV]);
 603  (REPEAT STRIP_TAC);
 604  (NEW_GOAL `voronoi_nondg V ([u0;u1;u2:real^3])`);
 605  (FIRST_ASSUM MATCH_MP_TAC);
 606  (REWRITE_TAC[Sphere.INITIAL_SUBLIST; LENGTH; ARITH_RULE `0 < SUC (SUC (SUC 0))`]);
 607  (EXISTS_TAC `[u3:real^3]` THEN ASM_REWRITE_TAC[APPEND]);
 608  (UP_ASM_TAC THEN ASM_REWRITE_TAC[VORONOI_NONDG; LENGTH;
 609    ARITH_RULE `SUC (SUC (SUC 0)) = 3`; AFF_DIM_EMPTY]);
 610  (REWRITE_TAC[ARITH_RULE `-- &1 + &3:int = &3 - &1`]);
 611  (REWRITE_TAC[MESON[INT_OF_NUM_SUB; ARITH_RULE `1 <= 3`] `&3:int - &1 = &(3 - 1)`]);
 612  (REWRITE_TAC[ARITH_RULE `3 - 1= 2 /\ ~(&2:int = &4)`]);
 613
 614
 615  (NEW_GOAL `s3 IN voronoi_list V [u0;u1;u2:real^3]`);
 616  (EXPAND_TAC "s3");
 617  (REWRITE_TAC[OMEGA_LIST_N; ARITH_RULE `3 = SUC 2`]);
 618  (ASM_REWRITE_TAC[ARITH_RULE `SUC 2 = 3`; TRUNCATE_SIMPLEX_EXPLICIT_3]);
 619  (MATCH_MP_TAC (SET_RULE `(?b. a IN b /\ b SUBSET c) ==> a IN c`));
 620  (EXISTS_TAC `voronoi_list V [u0; u1; u2; u3:real^3]`);
 621  (STRIP_TAC);
 622  (MATCH_MP_TAC CLOSEST_POINT_IN_SET);
 623  (REWRITE_TAC[Packing3.CLOSED_VORONOI_LIST]);
 624  (UNDISCH_TAC `barV V 3 ul` THEN REWRITE_TAC[BARV]);
 625  (REPEAT STRIP_TAC);
 626  (NEW_GOAL `voronoi_nondg V ([u0;u1;u2;u3:real^3])`);
 627  (FIRST_ASSUM MATCH_MP_TAC);
 628  (REWRITE_TAC[Sphere.INITIAL_SUBLIST; LENGTH; ARITH_RULE `0 < SUC (SUC (SUC (SUC 0)))`]);
 629  (EXISTS_TAC `[]:(real^3)list` THEN ASM_REWRITE_TAC[APPEND]);
 630  (UP_ASM_TAC THEN ASM_REWRITE_TAC[VORONOI_NONDG; LENGTH;
 631    ARITH_RULE `SUC(SUC (SUC (SUC 0))) = 4`; AFF_DIM_EMPTY]);
 632  (REWRITE_TAC[ARITH_RULE `-- &1 + &4:int = &4 - &1`]);
 633  (REWRITE_TAC[MESON[INT_OF_NUM_SUB; ARITH_RULE `1 <= 4`] `&4:int - &1 = &(4 - 1)`]);
 634  (REWRITE_TAC[ARITH_RULE `4 - 1= 3 /\ ~(&3:int = &4)`]);
 635  (REWRITE_TAC[VORONOI_LIST; set_of_list; VORONOI_SET]);
 636  (SET_TAC[]);
 637
 638  (NEW_GOAL `?s. between s (omega_list_n V ul 2,omega_list_n V ul 3) /\
 639                   dist (u0,s) = sqrt (&2) /\
 640                   mxi V ul = s`);
 641  (MATCH_MP_TAC MXI_EXPLICIT);
 642  (EXISTS_TAC `u1:real^3` THEN EXISTS_TAC `u2:real^3` THEN EXISTS_TAC `u3:real^3`);
 643  (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
 644  (REWRITE_WITH `[u0; u1; u2:real^3] = truncate_simplex 2 [u0; u1; u2; u3]`);
 645  (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
 646  (ASM_REWRITE_TAC[]);
 647
 648  (UP_ASM_TAC THEN ASM_REWRITE_TAC[] THEN STRIP_TAC);
 649  (NEW_GOAL `convex hull {s2,s3:real^3} SUBSET voronoi_list V [u0; u1; u2]`);
 650  (REWRITE_WITH `convex hull {s2, s3} SUBSET voronoi_list V [u0; u1; u2:real^3]    <=> convex hull {s2, s3} SUBSET convex hull (voronoi_list V [u0; u1; u2])`);
 651  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 652  (REWRITE_WITH `convex hull (voronoi_list V [u0; u1; u2]) = voronoi_list V [u0; u1; u2:real^3]`);
 653  (REWRITE_TAC[CONVEX_HULL_EQ; Packing3.CONVEX_VORONOI_LIST]);
 654  (MATCH_MP_TAC Marchal_cells.CONVEX_HULL_SUBSET);
 655  (ASM_SET_TAC[]);
 656
 657  (NEW_GOAL `s IN voronoi_list V [u0;u1;u2:real^3]`);
 658  (UNDISCH_TAC `between s (s2, s3:real^3)`);
 659  (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL]);
 660  (ASM_SET_TAC[]);
 661
 662  (NEW_GOAL `s2 = circumcenter (set_of_list [u0;u1;u2:real^3])`);
 663  (REWRITE_TAC[set_of_list]);
 664  (EXPAND_TAC "s2");
 665  (MATCH_MP_TAC OMEGA_LIST_2_EXPLICIT_NEW);
 666  (EXISTS_TAC `u3:(real^3)` THEN ASM_REWRITE_TAC[]);
 667  (REWRITE_TAC[GSYM (ASSUME `ul = [u0; u1; u2; u3:real^3]`); IN]);
 668  (ASM_REWRITE_TAC[]);
 669  (REWRITE_WITH `[u0; u1; u2:real^3] = truncate_simplex 2 [u0; u1; u2; u3]`);
 670  (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
 671  (ASM_REWRITE_TAC[]);
 672
 673  (STRIP_TAC);
 674  (NEW_GOAL `(m - s2:real^3) dot (m - s2) = &0`);
 675  (REWRITE_TAC[ASSUME `s2 = circumcenter (set_of_list [u0; u1; u2:real^3])`]);
 676  (MATCH_MP_TAC Rogers.MHFTTZN4);
 677  (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `2`);
 678  (REWRITE_TAC[set_of_list]);
 679  (ASM_REWRITE_TAC[]);
 680  (ASM_SIMP_TAC[IN_AFFINE_KY_LEMMA1]);
 681  (REWRITE_WITH `[u0; u1; u2:real^3] = truncate_simplex 2 ul`);
 682  (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
 683  (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
 684  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]);
 685  (UP_ASM_TAC THEN REWRITE_TAC[DOT_EQ_0; VECTOR_ARITH `a - b = vec 0 <=> a = b`]);
 686  (STRIP_TAC);
 687  (NEW_GOAL `hl (truncate_simplex 2 [u0;u1;u2;u3]) = dist (s, u0:real^3)`);
 688  (REWRITE_WITH `s = s2:real^3`);
 689  (ASM_MESON_TAC[]);
 690  (REWRITE_TAC[ASSUME `s2 = circumcenter (set_of_list [u0; u1; u2:real^3])`]);
 691  (REWRITE_WITH `dist (circumcenter (set_of_list [u0; u1; u2]),u0) = dist
 692   (circumcenter (set_of_list [u0; u1; u2]),HD [u0; u1; u2:real^3])`);
 693  (REWRITE_TAC[HD]);
 694  (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
 695  (MATCH_MP_TAC Rogers.HL_EQ_DIST0);
 696  (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `2`);
 697  (ASM_REWRITE_TAC[]);
 698  (REWRITE_WITH `[u0; u1; u2:real^3] = truncate_simplex 2 ul`);
 699  (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
 700  (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
 701  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]);
 702  (UP_ASM_TAC THEN REWRITE_TAC[] THEN ONCE_REWRITE_TAC[DIST_SYM]);
 703  (ASM_REAL_ARITH_TAC);
 704
 705
 706  (ASM_CASES_TAC `v = u0:real^3`);
 707  (ASM_REWRITE_TAC[]);
 708  (MATCH_MP_TAC EVENTUALLY_RADIAL_CONVEX_HULL_4_sub1);
 709  (MATCH_MP_TAC FUN_AFFINE_KLEMMA);
 710  (ASM_SET_TAC[]);
 711
 712  (ASM_CASES_TAC `v = u1:real^3`);
 713  (ASM_REWRITE_TAC[]);
 714  (REWRITE_WITH `{u0, u1, u2, m:real^3} = {u1, u0, u2, m}`);
 715  (SET_TAC[]);
 716  (MATCH_MP_TAC EVENTUALLY_RADIAL_CONVEX_HULL_4_sub1);
 717  (MATCH_MP_TAC FUN_AFFINE_KLEMMA);
 718  (REWRITE_WITH `{u1, u0, u2} = {u0, u1, u2:real^3}`);
 719  (SET_TAC[]);
 720  (ASM_SET_TAC[]);
 721
 722  (ASM_CASES_TAC `v = u2:real^3`);
 723  (ASM_REWRITE_TAC[]);
 724  (REWRITE_WITH `{u0, u1, u2, m:real^3} = {u2, u0, u1, m}`);
 725  (SET_TAC[]);
 726  (MATCH_MP_TAC EVENTUALLY_RADIAL_CONVEX_HULL_4_sub1);
 727  (MATCH_MP_TAC FUN_AFFINE_KLEMMA);
 728  (REWRITE_WITH `{u2, u0, u1} = {u0, u1, u2:real^3}`);
 729  (SET_TAC[]);
 730  (ASM_SET_TAC[]);
 731
 732  (NEW_GOAL `F`);
 733  (ASM_SET_TAC[]);
 734  (ASM_MESON_TAC[]);
 735  (REWRITE_TAC[EVENTUALLY_RADIAL_EMPTY]);
 736
 737 (* ======================================================================= *)
 738 (* ====Case 5:  k = 2 ====== *)
 739
 740  (ASM_CASES_TAC `k = 2`);
 741  (ASM_REWRITE_TAC[MCELL_EXPLICIT; mcell2]);
 742  (COND_CASES_TAC);
 743  (LET_TAC);
 744  (REWRITE_TAC[HD;TL]);
 745  (ABBREV_TAC `s3 = omega_list_n V [u0; u1; u2; u3] 3`);
 746  (ABBREV_TAC `m = mxi V [u0; u1; u2; u3]`);
 747
 748  (NEW_GOAL
 749  `V INTER mcell k V ul = set_of_list (truncate_simplex (k - 1) ul)`);
 750  (MATCH_MP_TAC LEPJBDJ);
 751  (ASM_REWRITE_TAC[ARITH_RULE `1 <= 2 /\ 2 <= 4`]);
 752  (STRIP_TAC);
 753  (NEW_GOAL `v IN mcell 3 V ul`);
 754  (ASM_SET_TAC[]);
 755  (ASM_SET_TAC[]);
 756  (UP_ASM_TAC THEN ASM_REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_1; ARITH_RULE `2 - 1 = 1`]);
 757  (STRIP_TAC);
 758
 759  (NEW_GOAL `v IN {u0, u1:real^3}`);
 760  (ASM_SET_TAC[]);
 761  (NEW_GOAL `~(u0 = u1:real^3)`);
 762  (STRIP_TAC);
 763  (NEW_GOAL `CARD {u0,u1,u2,u3:real^3} = 4`);
 764  (REWRITE_WITH `{u0,u1,u2,u3:real^3} = set_of_list ul`);
 765  (ASM_REWRITE_TAC[set_of_list]);
 766  (REWRITE_WITH `LENGTH (ul:(real^3)list) = 3 + 1 /\ CARD (set_of_list ul) = 3 + 1`);
 767  (MATCH_MP_TAC Rogers.BARV_IMP_LENGTH_EQ_CARD);
 768  (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]);
 769  (ARITH_TAC);
 770  (UP_ASM_TAC THEN ASM_REWRITE_TAC[SET_RULE `{a,a,b,c} = {a,b,c}`]);
 771  (NEW_GOAL `CARD {u1,u2,u3:real^3} <= 3`);
 772  (REWRITE_TAC[Geomdetail.CARD3]);
 773  (ASM_ARITH_TAC);
 774
 775
 776
 777  (NEW_GOAL `hl [u0;u1:real^3] = inv(&2) * dist (u1,u0)`);
 778  (REWRITE_WITH `hl [u0;u1:real^3] =
 779    dist (circumcenter (set_of_list [u0;u1]),HD [u0;u1])`);
 780  (MATCH_MP_TAC Rogers.HL_EQ_DIST0);
 781  (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `1`);
 782  (ASM_REWRITE_TAC[]);
 783  (REWRITE_WITH `[u0;u1:real^3] = truncate_simplex 1 ul`);
 784  (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);
 785  (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
 786  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `1 <= 3`]);
 787  (REWRITE_TAC[set_of_list; Rogers.CIRCUMCENTER_2; midpoint; HD; dist]);
 788  (NORM_ARITH_TAC);
 789
 790  (NEW_GOAL `&0 < a /\ a < &1`);
 791  (EXPAND_TAC "a");
 792  (REWRITE_TAC[]);
 793  (STRIP_TAC);
 794  (MATCH_MP_TAC REAL_LT_DIV);
 795  (SIMP_TAC[SQRT_POS_LT; ARITH_RULE `&0 < &2`]);
 796  (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);
 797  (ASM_REWRITE_TAC[]);
 798  (MATCH_MP_TAC REAL_LT_MUL);
 799  (ASM_SIMP_TAC[REAL_LT_INV; ARITH_RULE `&0 < &2`]);
 800  (MATCH_MP_TAC DIST_POS_LT THEN ASM_MESON_TAC[]);
 801  (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);
 802  (REWRITE_WITH `hl [u0; u1:real^3] / sqrt (&2) < &1 <=>
 803                  hl [u0; u1] < &1 * sqrt (&2)`);
 804  (MATCH_MP_TAC REAL_LT_LDIV_EQ);
 805  (SIMP_TAC[SQRT_POS_LT; ARITH_RULE `&0 < &2`]);
 806  (REWRITE_TAC[REAL_MUL_LID]);
 807  (REWRITE_WITH `[u0;u1:real^3] = truncate_simplex 1 [u0; u1; u2; u3]`);
 808  (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);
 809  (ASM_REWRITE_TAC[]);
 810
 811  (MATCH_MP_TAC EVENTUALLY_RADIAL_INTER);
 812  (STRIP_TAC);
 813  (ASM_CASES_TAC `v = u0:real^3`);
 814  (ASM_REWRITE_TAC[EVENTUALLY_RADIAL_RCONE_GE_ABC_A]);
 815  (ASM_CASES_TAC `v = u1:real^3`);
 816  (ASM_REWRITE_TAC[]);
 817  (MATCH_MP_TAC EVENTUALLY_RADIAL_RCONE_GE_ABC_B);
 818  (ASM_REWRITE_TAC[]);
 819  (NEW_GOAL `F`);
 820  (ASM_SET_TAC[]);
 821  (ASM_MESON_TAC[]);
 822
 823  (MATCH_MP_TAC EVENTUALLY_RADIAL_INTER);
 824  (STRIP_TAC);
 825  (ASM_CASES_TAC `v = u1:real^3`);
 826  (ASM_REWRITE_TAC[EVENTUALLY_RADIAL_RCONE_GE_ABC_A]);
 827  (ASM_CASES_TAC `v = u0:real^3`);
 828  (ASM_REWRITE_TAC[]);
 829  (MATCH_MP_TAC EVENTUALLY_RADIAL_RCONE_GE_ABC_B);
 830  (ASM_REWRITE_TAC[]);
 831  (NEW_GOAL `F`);
 832  (ASM_SET_TAC[]);
 833  (ASM_MESON_TAC[]);
 834
 835 (* ========================================================================== *)
 836  (NEW_GOAL `DISJOINT {u0, u1:real^3} {m, s3}`);
 837 (* ========================================================================== *)
 838
 839  (ABBREV_TAC `s2 = omega_list_n V ul 2`);
 840  (NEW_GOAL `s2 IN voronoi_list V [u0;u1]`);
 841  (REWRITE_WITH `[u0;u1:real^3] = truncate_simplex 1 ul`);
 842  (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);
 843  (EXPAND_TAC "s2");
 844  (MATCH_MP_TAC Rogers.OMEGA_LIST_N_IN_VORONOI_LIST_GEN);
 845  (EXISTS_TAC `3`);
 846  (ASM_REWRITE_TAC[ARITH_RULE `1 <= 2 /\ 2 <= 3`]);
 847
 848  (NEW_GOAL `s3 IN voronoi_list V [u0;u1]`);
 849  (REWRITE_WITH `[u0;u1:real^3] = truncate_simplex 1 ul`);
 850  (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);
 851  (EXPAND_TAC "s3");
 852  (REWRITE_TAC[GSYM (ASSUME `ul = [u0; u1; u2; u3:real^3]`)]);
 853  (MATCH_MP_TAC Rogers.OMEGA_LIST_N_IN_VORONOI_LIST_GEN);
 854  (EXISTS_TAC `3`);
 855  (ASM_REWRITE_TAC[ARITH_RULE `1 <= 3 /\ 3 <= 3`]);
 856  (NEW_GOAL `m IN voronoi_list V [u0; u1]`);
 857  (ASM_CASES_TAC `hl (truncate_simplex 2 (ul:(real^3)list)) < sqrt (&2)`);
 858  (NEW_GOAL `?s. between s (omega_list_n V ul 2,omega_list_n V ul 3) /\
 859                   dist (u0,s) = sqrt (&2) /\
 860                   m = s`);
 861  (EXPAND_TAC "m");
 862  (REWRITE_TAC[GSYM (ASSUME `ul = [u0; u1; u2; u3:real^3]`)]);
 863  (MATCH_MP_TAC MXI_EXPLICIT);
 864  (EXISTS_TAC `u1:real^3` THEN EXISTS_TAC `u2:real^3` THEN
 865    EXISTS_TAC `u3:real^3`);
 866  (ASM_REWRITE_TAC[]);
 867  (UP_ASM_TAC THEN ASM_REWRITE_TAC[] THEN STRIP_TAC);
 868
 869
 870  (NEW_GOAL `convex hull {s2,s3:real^3} SUBSET voronoi_list V [u0; u1]`);
 871  (REWRITE_WITH `convex hull {s2, s3} SUBSET voronoi_list V [u0; u1:real^3]    <=> convex hull {s2, s3} SUBSET convex hull (voronoi_list V [u0; u1])`);
 872  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 873  (REWRITE_WITH `convex hull (voronoi_list V [u0; u1]) = voronoi_list V [u0; u1:real^3]`);
 874  (REWRITE_TAC[CONVEX_HULL_EQ; Packing3.CONVEX_VORONOI_LIST]);
 875  (MATCH_MP_TAC Marchal_cells.CONVEX_HULL_SUBSET);
 876  (ASM_SET_TAC[]);
 877
 878  (ASM_REWRITE_TAC[]);
 879  (UNDISCH_TAC `between s (s2, s3:real^3)`);
 880  (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL]);
 881  (ASM_SET_TAC[]);
 882
 883  (EXPAND_TAC "m" THEN REWRITE_TAC[mxi]);
 884  (COND_CASES_TAC);
 885  (ASM_MESON_TAC[]);
 886  (NEW_GOAL `F`);
 887  (UP_ASM_TAC THEN UP_ASM_TAC THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);
 888  (ASM_MESON_TAC[]);
 889
 890  (NEW_GOAL `~(m IN {u0,u1:real^3})`);
 891  (REWRITE_TAC[SET_RULE `a IN {b,c} <=> a = b \/ a = c`] THEN STRIP_TAC);
 892  (NEW_GOAL `m:real^3 IN voronoi_closed V u1`);
 893  (UNDISCH_TAC `m IN voronoi_list V [u0; u1]` THEN REWRITE_TAC[VORONOI_LIST;
 894    VORONOI_SET; set_of_list]);
 895  (SET_TAC[]);
 896  (UP_ASM_TAC THEN ASM_REWRITE_TAC[voronoi_closed; IN; IN_ELIM_THM]);
 897  (STRIP_TAC);
 898  (NEW_GOAL `dist (u0, u1:real^3) <= dist (u0, u0)`);
 899  (FIRST_ASSUM MATCH_MP_TAC);
 900  (ASM_SET_TAC[]);
 901  (UP_ASM_TAC THEN REWRITE_TAC[DIST_REFL; REAL_ARITH `~(a <= b) <=> b < a`]);
 902  (ASM_SIMP_TAC[DIST_POS_LT]);
 903
 904  (NEW_GOAL `m:real^3 IN voronoi_closed V u0`);
 905  (UNDISCH_TAC `m IN voronoi_list V [u0; u1]` THEN REWRITE_TAC[VORONOI_LIST;
 906    VORONOI_SET; set_of_list]);
 907  (SET_TAC[]);
 908  (UP_ASM_TAC THEN ASM_REWRITE_TAC[voronoi_closed; IN; IN_ELIM_THM]);
 909  (STRIP_TAC);
 910  (NEW_GOAL `dist (u1, u0:real^3) <= dist (u1, u1)`);
 911  (FIRST_ASSUM MATCH_MP_TAC);
 912  (ASM_SET_TAC[]);
 913  (UP_ASM_TAC THEN REWRITE_TAC[DIST_REFL; REAL_ARITH `~(a <= b) <=> b < a`]);
 914  (ASM_SIMP_TAC[DIST_POS_LT]);
 915
 916  (NEW_GOAL `~(s3 IN {u0, u1:real^3})`);
 917  (REWRITE_TAC[SET_RULE `a IN {b,c} <=> a = b \/ a = c`] THEN STRIP_TAC);
 918  (NEW_GOAL `s3:real^3 IN voronoi_closed V u1`);
 919  (UNDISCH_TAC `s3 IN voronoi_list V [u0; u1]` THEN REWRITE_TAC[VORONOI_LIST;
 920    VORONOI_SET; set_of_list]);
 921  (SET_TAC[]);
 922  (UP_ASM_TAC THEN ASM_REWRITE_TAC[voronoi_closed; IN; IN_ELIM_THM]);
 923  (STRIP_TAC);
 924  (NEW_GOAL `dist (u0, u1:real^3) <= dist (u0, u0)`);
 925  (FIRST_ASSUM MATCH_MP_TAC);
 926  (ASM_SET_TAC[]);
 927  (UP_ASM_TAC THEN REWRITE_TAC[DIST_REFL; REAL_ARITH `~(a <= b) <=> b < a`]);
 928  (ASM_SIMP_TAC[DIST_POS_LT]);
 929
 930  (NEW_GOAL `s3:real^3 IN voronoi_closed V u0`);
 931  (UNDISCH_TAC `s3 IN voronoi_list V [u0; u1]` THEN REWRITE_TAC[VORONOI_LIST;
 932    VORONOI_SET; set_of_list]);
 933  (SET_TAC[]);
 934  (UP_ASM_TAC THEN ASM_REWRITE_TAC[voronoi_closed; IN; IN_ELIM_THM]);
 935  (STRIP_TAC);
 936  (NEW_GOAL `dist (u1, u0:real^3) <= dist (u1, u1)`);
 937  (FIRST_ASSUM MATCH_MP_TAC);
 938  (ASM_SET_TAC[]);
 939  (UP_ASM_TAC THEN REWRITE_TAC[DIST_REFL; REAL_ARITH `~(a <= b) <=> b < a`]);
 940  (ASM_SIMP_TAC[DIST_POS_LT]);
 941
 942  (REWRITE_TAC[DISJOINT]);
 943  (ASM_SET_TAC[]);
 944
 945 (* ========================================================================== *)
 946 (* ========================================================================== *)
 947
 948  (ASM_CASES_TAC `v = u0:real^3`);
 949  (ASM_REWRITE_TAC[]);
 950  (MATCH_MP_TAC EVENTUALLY_RADIAL_AFF_GE);
 951  (ASM_REWRITE_TAC[]);
 952
 953  (ASM_CASES_TAC `v = u1:real^3`);
 954  (ASM_REWRITE_TAC[]);
 955  (REWRITE_WITH `{u0,u1:real^3} = {u1,u0}`);
 956  (SET_TAC[]);
 957  (MATCH_MP_TAC EVENTUALLY_RADIAL_AFF_GE);
 958  (REWRITE_WITH `{u1,u0:real^3} = {u0,u1}`);
 959  (SET_TAC[]);
 960  (ASM_REWRITE_TAC[]);
 961
 962  (NEW_GOAL `F`);
 963  (ASM_SET_TAC[]);
 964  (ASM_MESON_TAC[]);
 965  (REWRITE_TAC[EVENTUALLY_RADIAL_EMPTY]);
 966
 967  (NEW_GOAL `F`);
 968  (ASM_ARITH_TAC);
 969  (ASM_MESON_TAC[])]);;
 970
 971
 972 end;;