text_formalization/packing/LEPJBDJ.hl

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