text_formalization/packing/QZKSYKG.hl

   1 (* ========================================================================= *)
   2 (*                FLYSPECK - BOOK FORMALIZATION                              *)
   3 (*                                                                           *)
   4 (*      Authour   : VU KHAC KY                                               *)
   5 (*      Book lemma: QZKSYKG                                                  *)
   6 (*      Chaper    : Packing                                                  *)
   7 (*                                                                           *)
   8 (* ========================================================================= *)
   9
  10
  11 module Qzksykg = struct
  12
  13 open Rogers;;
  14 open Vukhacky_tactics;;
  15 open Pack_defs;;
  16 open Pack_concl;;
  17 open Pack1;;
  18 open Sphere;;
  19 open Marchal_cells;;
  20 open Emnwuus;;
  21 open Marchal_cells_2_new;;
  22 open Lepjbdj;;
  23 open Hdtfnfz;;
  24 open Ynhyjit;;
  25
  26 let CONVEX_HULL_4_IMP_3_1 = prove_by_refinement (
  27  `!a:real^3 b c d x.
  28     x IN convex hull {a,b,c,d} ==>
  29        (?x1 t1 t2.
  30            x1 IN convex hull {a,b,c} /\
  31            &0 <= t1 /\ &0 <= t2 /\ t1 + t2 = &1 /\
  32            x = t1 % x1 + t2 % d)`,
  33 [(REWRITE_TAC[CONVEX_HULL_4; CONVEX_HULL_3;IN;IN_ELIM_THM]);
  34  (REPEAT STRIP_TAC);
  35  (ASM_CASES_TAC `z < &1`);
  36
  37  (EXISTS_TAC `(u/ (u + v + w)) % a + (v/ (u+v+w)) % b + (w/(u+v+w)) % (c:real^3)`);
  38  (EXISTS_TAC `(u + v + w):real` THEN EXISTS_TAC `z:real`);
  39  (REPEAT STRIP_TAC);
  40  (EXISTS_TAC `u/(u+v+w)`);
  41  (EXISTS_TAC `v/(u+v+w)`);
  42  (EXISTS_TAC `w/(u+v+w)`);
  43  (REPEAT STRIP_TAC);
  44  (MATCH_MP_TAC REAL_LE_DIV);
  45  (ASM_REAL_ARITH_TAC);
  46  (MATCH_MP_TAC REAL_LE_DIV);
  47  (ASM_REAL_ARITH_TAC);
  48  (MATCH_MP_TAC REAL_LE_DIV);
  49  (ASM_REAL_ARITH_TAC);
  50  (REWRITE_TAC[REAL_ARITH `u / (u + v + w) + v / (u + v + w) + w / (u + v + w)=
  51   (u + v + w) / (u + v + w)`]);
  52  (MATCH_MP_TAC REAL_DIV_REFL);
  53  (ASM_REAL_ARITH_TAC);
  54  (REFL_TAC);
  55  (ASM_REAL_ARITH_TAC);
  56  (ASM_REAL_ARITH_TAC);
  57  (ASM_REAL_ARITH_TAC);
  58  (REWRITE_TAC[VECTOR_ARITH `s % (s1 /s % a + s2 / s % b + s3/ s % c) =
  59    (s * s1 / s) % a + (s * s2 / s) % b + (s * s3 / s) % c`]);
  60  (REWRITE_TAC[REAL_ARITH `s * s1 / s = s1 * (s / s)`]);
  61  (REWRITE_WITH `(u + v + w) / (u + v + w) = &1`);
  62  (MATCH_MP_TAC REAL_DIV_REFL);
  63  (ASM_REAL_ARITH_TAC);
  64  (ASM_REWRITE_TAC[REAL_MUL_RID] THEN VECTOR_ARITH_TAC);
  65
  66  (NEW_GOAL `z = &1 /\ u = &0 /\ v = &0 /\ w = &0`);
  67  (ASM_REAL_ARITH_TAC);
  68  (EXISTS_TAC `a:real^3`);
  69  (EXISTS_TAC `&0` THEN EXISTS_TAC `&1`);
  70  (ASM_REWRITE_TAC[ARITH_RULE `&0 <= &0 /\ &0 <= &1 /\ &0 + &1 = &1`]);
  71  (STRIP_TAC);
  72  (EXISTS_TAC `&1` THEN EXISTS_TAC `&0` THEN EXISTS_TAC `&0`);
  73  (ASM_REWRITE_TAC[ARITH_RULE `&0 <= &0 /\ &0 <= &1 /\ &1 + &0 + &0 = &1`]);
  74  (VECTOR_ARITH_TAC);
  75  (VECTOR_ARITH_TAC)]);;
  76
  77
  78 let BARV_2_EXPLICIT = prove_by_refinement (
  79  `!V vl. barV V 2 vl ==> ?u0 u1 u2. vl = [u0;u1;u2]`,
  80 [(REWRITE_TAC[BARV] THEN REPEAT STRIP_TAC);
  81  (NEW_GOAL `?x0 xl. (vl:(real^3)list) = CONS x0 xl /\ LENGTH xl = 2`);
  82  (REWRITE_TAC[GSYM LENGTH_EQ_CONS]);
  83  (ASM_ARITH_TAC);
  84  (UP_ASM_TAC THEN STRIP_TAC);
  85  (EXISTS_TAC `x0:real^3`);
  86  (NEW_GOAL `?x1 yl. (xl:(real^3)list) = CONS x1 yl /\ LENGTH yl = 1`);
  87  (REWRITE_TAC[GSYM LENGTH_EQ_CONS]);
  88  (ASM_ARITH_TAC);
  89  (UP_ASM_TAC THEN STRIP_TAC);
  90  (EXISTS_TAC `x1:real^3`);
  91  (NEW_GOAL `?x2 zl. (yl:(real^3)list) = CONS x2 zl /\ LENGTH zl = 0`);
  92  (REWRITE_TAC[GSYM LENGTH_EQ_CONS]);
  93  (ASM_ARITH_TAC);
  94  (UP_ASM_TAC THEN STRIP_TAC);
  95  (EXISTS_TAC `x2:real^3`);
  96  (NEW_GOAL `(zl:(real^3)list) = []`);
  97  (ASM_MESON_TAC[LENGTH_EQ_NIL]);
  98  (ASM_REWRITE_TAC[])]);;
  99
 100 let ROGERS_EXPLICIT_2 = prove_by_refinement (
 101  `!V ul.
 102   saturated V /\ packing V /\ barV V 2 ul ==>
 103   rogers V ul = convex hull
 104  {HD ul, omega_list_n V ul 1, omega_list_n V ul 2}`,
 105
 106 [(REPEAT STRIP_TAC THEN REWRITE_TAC[ROGERS]);
 107  (NEW_GOAL `?u0 u1 u2. (ul:(real^3)list) = [u0:real^3;u1;u2]`);
 108  (MATCH_MP_TAC BARV_2_EXPLICIT THEN EXISTS_TAC `V:real^3->bool`);
 109  (ASM_REWRITE_TAC[]);
 110  (UP_ASM_TAC THEN STRIP_TAC);
 111  (REWRITE_WITH `{j | j < LENGTH (ul:(real^3)list)} = {0, 1,2}`);
 112  (ASM_REWRITE_TAC[LENGTH; ARITH_RULE `SUC (SUC (SUC 0)) = 3`]);
 113  (SET_TAC[ARITH_RULE `0 < 3 /\ 1 < 3 /\ 2 < 3 /\
 114                       (!j. j < 3 ==> (j=0\/j=1\/j=2))`]);
 115  (REWRITE_TAC[IMAGE]);
 116  (AP_TERM_TAC);
 117  (REWRITE_TAC[SET_RULE `!x. x IN {0,1,2} <=> (x = 0 \/x = 1 \/x = 2)`]);
 118  (REWRITE_WITH
 119  `!y. (?x. (x = 0 \/ x = 1 \/ x = 2) /\ y = omega_list_n V ul x)
 120  <=> (y = omega_list_n V ul 0) \/ (y = omega_list_n V ul 1) \/
 121      (y = omega_list_n V ul 2)`);
 122  (SET_TAC[BETA_THM]);
 123  (REWRITE_WITH
 124    `{y | y = omega_list_n V ul 0 \/ y = omega_list_n V ul 1 \/
 125           y = omega_list_n V ul 2}
 126      =  {omega_list_n V ul 0, omega_list_n V ul 1, omega_list_n V ul 2}`);
 127  (SET_TAC[]);
 128  (REWRITE_WITH `omega_list_n V ul 0 = HD ul`);
 129  (REWRITE_TAC[OMEGA_LIST_N])]);;
 130
 131 let TWO_REARRANGEMENT_LEMMA = prove_by_refinement (
 132  `!V ul p u0 u1 u2 u3.
 133     packing V /\ saturated V /\ barV V 3 ul /\ ul = [u0;u1;u2;u3] ==>
 134     (?p. p permutes 0..1 /\ [u1;u0;u2;u3] = left_action_list p ul)`,
 135 [(REPEAT STRIP_TAC);
 136  (ABBREV_TAC `p = (\i. if i = 0 then 1 else if i = 1 then 0 else i)`);
 137  (EXISTS_TAC `p:num->num`);
 138
 139  (NEW_GOAL `p 0 = 1`);
 140  (EXPAND_TAC "p");
 141  (COND_CASES_TAC);
 142  (REFL_TAC);
 143  (ASM_MESON_TAC[]);
 144
 145  (NEW_GOAL `p 1 = 0`);
 146  (EXPAND_TAC "p");
 147  (COND_CASES_TAC);
 148  (COND_CASES_TAC);
 149  (REFL_TAC);
 150  (ASM_MESON_TAC[]);
 151
 152  (NEW_GOAL `!i. 1 < i ==> p i = i`);
 153  (EXPAND_TAC "p");
 154  (REPEAT STRIP_TAC);
 155  (COND_CASES_TAC);
 156  (NEW_GOAL `F`);
 157  (ASM_ARITH_TAC);
 158  (ASM_MESON_TAC[]);
 159  (COND_CASES_TAC);
 160  (NEW_GOAL `F`);
 161  (ASM_ARITH_TAC);
 162  (ASM_MESON_TAC[]);
 163  (REFL_TAC);
 164
 165  (NEW_GOAL `inverse p 0 = 1`);
 166  (REWRITE_TAC[inverse]);
 167  (MATCH_MP_TAC SELECT_UNIQUE);
 168  (GEN_TAC THEN EQ_TAC);
 169  (REWRITE_TAC[BETA_THM]);
 170  (ASM_CASES_TAC `y = 0`);
 171  (ASM_REWRITE_TAC[]);
 172  (ARITH_TAC);
 173  (ASM_CASES_TAC `1 < y`);
 174  (ASM_SIMP_TAC[]);
 175  (STRIP_TAC);
 176  (ASM_ARITH_TAC);
 177  (STRIP_TAC THEN ASM_REWRITE_TAC[BETA_THM]);
 178
 179  (NEW_GOAL `inverse p 1 = 0`);
 180  (REWRITE_TAC[inverse]);
 181  (MATCH_MP_TAC SELECT_UNIQUE);
 182  (GEN_TAC THEN EQ_TAC);
 183  (REWRITE_TAC[BETA_THM]);
 184  (ASM_CASES_TAC `y = 1`);
 185  (ASM_REWRITE_TAC[]);
 186  (ARITH_TAC);
 187  (ASM_CASES_TAC `1 < y`);
 188  (ASM_SIMP_TAC[]);
 189  (STRIP_TAC);
 190  (ASM_ARITH_TAC);
 191  (STRIP_TAC THEN ASM_REWRITE_TAC[BETA_THM]);
 192
 193  (NEW_GOAL `!i. 1 < i ==> inverse p i = i`);
 194  (REPEAT STRIP_TAC);
 195  (REWRITE_TAC[inverse]);
 196  (MATCH_MP_TAC SELECT_UNIQUE);
 197  (GEN_TAC THEN EQ_TAC);
 198  (REWRITE_TAC[BETA_THM]);
 199  (ASM_CASES_TAC `y = 0`);
 200  (ASM_SIMP_TAC[]);
 201  (STRIP_TAC);
 202  (NEW_GOAL `F`);
 203  (ASM_ARITH_TAC);
 204  (ASM_MESON_TAC[]);
 205  (ASM_CASES_TAC `y = 1`);
 206  (ASM_SIMP_TAC[]);
 207  (STRIP_TAC);
 208  (NEW_GOAL `F`);
 209  (ASM_ARITH_TAC);
 210  (ASM_MESON_TAC[]);
 211  (NEW_GOAL `1 < y`);
 212  (ASM_ARITH_TAC);
 213  (STRIP_TAC);
 214  (NEW_GOAL `(p:num->num) y = y`);
 215  (UNDISCH_TAC `1 < y` THEN ASM_REWRITE_TAC[]);
 216  (ASM_MESON_TAC[]);
 217  (STRIP_TAC THEN ASM_REWRITE_TAC[BETA_THM]);
 218  (ASM_MESON_TAC[]);
 219  (STRIP_TAC);
 220  (MATCH_MP_TAC Hypermap.lemma_permutes_via_surjetive);
 221  (REWRITE_WITH `0..1 = {0,1}`);
 222  (REWRITE_TAC[GSYM NUMSEG_LE; ARITH_RULE `x <= 1 <=> x = 0 \/ x = 1`]);
 223  (SET_TAC[]);
 224  (REWRITE_TAC[Geomdetail.FINITE6; SET_RULE `a IN {x,y} <=> a = x \/ a = y`]);
 225  (ASM_MESON_TAC[]);
 226
 227  (ASM_REWRITE_TAC[left_action_list;LENGTH; ARITH_RULE
 228   `SUC (SUC (SUC (SUC 0))) = 4`]);
 229  (ASM_REWRITE_TAC[TABLE_4]);
 230  (ASM_SIMP_TAC[TABLE_4; EL;HD;TL; ARITH_RULE `1 < 2 /\ 1 < 3`]);
 231  (REWRITE_TAC[EL; HD; TL; ARITH_RULE `1 = SUC 0 /\ 2 = SUC 1 /\ 3 = SUC 2`])]);;
 232
 233
 234 let SET_SUBSET_AFFINE_HULL = prove (
 235  `!S:real^3->bool. S SUBSET affine hull S`,
 236  STRIP_TAC THEN
 237  MATCH_MP_TAC (SET_RULE `(?C. A SUBSET C /\ C SUBSET B) ==> A SUBSET B`) THEN
 238  EXISTS_TAC `convex hull S:real^3->bool` THEN
 239  REWRITE_TAC[CONVEX_HULL_SUBSET_AFFINE_HULL; SUBSET] THEN
 240  REWRITE_TAC[IN_SET_IMP_IN_CONVEX_HULL_SET]);;
 241
 242 (* ========================================================================= *)
 243
 244 let QZKSYKG1_concl =
 245  `!V ul vl k p.
 246          saturated V /\
 247          packing V /\
 248          barV V 3 ul /\
 249          k IN {0,1,2,3,4} /\
 250          ~ (mcell k V ul = {}) /\
 251          p permutes 0..(k - 1) /\
 252          vl = left_action_list p ul
 253         ==> barV V 3 vl`;;
 254
 255 let QZKSYKG2_concl =
 256  `!V ul k.
 257          saturated V /\
 258          packing V /\
 259          barV V 3 ul /\
 260          k IN {0,1,2,3,4}
 261      ==> (mcell k V ul SUBSET
 262       UNIONS{rogers V (left_action_list p ul) | p permutes 0..(k-1)})`;;
 263
 264 (* ========================================================================= *)
 265
 266 let QZKSYKG1 = prove_by_refinement (QZKSYKG1_concl,
 267 [(REPEAT STRIP_TAC);
 268  (ASM_CASES_TAC `k = 0 \/ k = 1`);
 269  (UNDISCH_TAC `p permutes 0..(k-1)`);
 270  (REWRITE_WITH `k - 1 = 0`);
 271  (ASM_ARITH_TAC);
 272  (REWRITE_TAC[Packing3.PERMUTES_TRIVIAL]);
 273  (STRIP_TAC);
 274  (ASM_REWRITE_TAC[Packing3.LEFT_ACTION_LIST_I]);
 275  (NEW_GOAL `k IN {2,3,4}`);
 276  (ASM_SET_TAC[]);
 277
 278 (* Cases k = 4 *)
 279
 280  (ASM_CASES_TAC `k = 4`);
 281  (UNDISCH_TAC `~(mcell k V ul = {})`);
 282  (ASM_SIMP_TAC[MCELL_EXPLICIT; ARITH_RULE `4 >= 4`;mcell4]);
 283  (COND_CASES_TAC);
 284  (STRIP_TAC);
 285  (REWRITE_TAC[MESON[IN] `barV V 3 s <=> s IN barV V 3`]);
 286  (MATCH_MP_TAC Rogers.YIFVQDV_1);
 287  (ASM_REWRITE_TAC[IN]);
 288  (REWRITE_WITH `3 = k - 1`);
 289  (ASM_ARITH_TAC);
 290  (ASM_REWRITE_TAC[]);
 291  (MESON_TAC[]);
 292
 293 (* Cases k = 3, k = 2 *)
 294
 295  (REWRITE_WITH
 296   `barV V 3 vl /\
 297       (!j. k - 1 <= j /\ j <= 3
 298            ==> omega_list_n V vl j = omega_list_n V ul j)`);
 299  (MATCH_MP_TAC YNHYJIT);
 300  (EXISTS_TAC `p:num->num`);
 301  (ASM_REWRITE_TAC[]);
 302  (UNDISCH_TAC `~(mcell k V ul = {})`);
 303
 304  (ASM_CASES_TAC `k = 3`);
 305  (SIMP_TAC [ASSUME `k = 3`; MCELL_EXPLICIT; mcell3]);
 306  (COND_CASES_TAC);
 307  (REPEAT STRIP_TAC);
 308  (ASM_REWRITE_TAC[ARITH_RULE `3 - 1 = 2`]);
 309  (ASM_REWRITE_TAC[]);
 310  (MESON_TAC[]);
 311
 312  (NEW_GOAL `k = 2`);
 313  (ASM_SET_TAC[]);
 314  (SIMP_TAC [ASSUME `k = 2`; MCELL_EXPLICIT; mcell2]);
 315  (COND_CASES_TAC);
 316  (LET_TAC);
 317  (REPEAT STRIP_TAC);
 318  (ASM_REWRITE_TAC[ARITH_RULE `2 - 1 = 1`]);
 319  (ASM_REWRITE_TAC[]);
 320  (MESON_TAC[])]);;
 321
 322 (* ========================================================================= *)
 323
 324
 325 let QZKSYKG2 = prove_by_refinement ( QZKSYKG2_concl,
 326
 327 [(REPEAT STRIP_TAC);
 328  (ASM_CASES_TAC `k = 0 \/ k = 1`);
 329  (REWRITE_WITH `k - 1 = 0`);
 330  (ASM_ARITH_TAC);
 331  (REWRITE_TAC[Packing3.PERMUTES_TRIVIAL]);
 332  (REWRITE_TAC[Packing3.SING_GSPEC_APP; UNIONS_1;
 333    Packing3.LEFT_ACTION_LIST_I]);
 334  (UP_ASM_TAC THEN STRIP_TAC);
 335  (ASM_SIMP_TAC[MCELL_EXPLICIT; mcell0]);
 336  (SET_TAC[]);
 337  (ASM_SIMP_TAC[MCELL_EXPLICIT; mcell1]);
 338  (COND_CASES_TAC);
 339  (SET_TAC[]);
 340  (SET_TAC[]);
 341
 342 (* ======================================================================== *)
 343
 344  (ASM_CASES_TAC `k = 4`);
 345  (REWRITE_WITH `k - 1 = 3`);
 346  (ASM_ARITH_TAC);
 347  (ASM_SIMP_TAC[MCELL_EXPLICIT; ARITH_RULE `4 >= 4`; mcell4]);
 348  (COND_CASES_TAC);
 349  (REWRITE_WITH `convex hull set_of_list ul =
 350              UNIONS {rogers V (left_action_list p ul) | p permutes 0..3}`);
 351  (MATCH_MP_TAC Rogers.WQPRRDY);
 352  (ASM_REWRITE_TAC[IN]);
 353  (SET_TAC[]);
 354  (SET_TAC[]);
 355
 356 (* ======================================================================== *)
 357
 358  (ASM_CASES_TAC `k = 3`);
 359  (REWRITE_WITH `k - 1 = 2`);
 360  (ASM_ARITH_TAC);
 361  (ASM_SIMP_TAC[MCELL_EXPLICIT; mcell3]);
 362  (COND_CASES_TAC);
 363
 364  (ABBREV_TAC `m = mxi V ul`);
 365  (NEW_GOAL `?u0 u1 u2 u3. ul = [u0;u1;u2;u3:real^3]`);
 366  (MATCH_MP_TAC BARV_3_EXPLICIT THEN EXISTS_TAC `V:real^3->bool`);
 367  (ASM_REWRITE_TAC[]);
 368  (UP_ASM_TAC THEN STRIP_TAC);
 369  (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2;set_of_list;
 370    SET_RULE `{a,b,c} UNION {d} = {a,b,c,d}`]);
 371  (REWRITE_TAC[GSYM (ASSUME `ul = [u0;u1;u2;u3:real^3]`)]);
 372
 373  (REWRITE_TAC[SUBSET]);
 374  (GEN_TAC THEN DISCH_TAC);
 375  (NEW_GOAL `(?x1 t1 t2.
 376                   x1 IN convex hull {u0, u1, u2:real^3} /\
 377                   &0 <= t1 /\
 378                   &0 <= t2 /\
 379                   t1 + t2 = &1 /\
 380                   x = t1 % x1 + t2 % m)`);
 381  (ASM_SIMP_TAC[CONVEX_HULL_4_IMP_3_1]);
 382  (UP_ASM_TAC THEN STRIP_TAC);
 383  (REWRITE_TAC[ASSUME `x:real^3 = t1 % x1 + t2 % m`]);
 384
 385  (UNDISCH_TAC `x1 IN convex hull {u0, u1, u2:real^3}`);
 386  (REWRITE_WITH `convex hull {u0,u1,u2:real^3} =
 387    UNIONS {rogers V (left_action_list p (truncate_simplex 2 ul)) | p permutes 0..2}`);
 388  (REWRITE_WITH `{u0,u1,u2:real^3} = set_of_list (truncate_simplex 2 ul)`);
 389  (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2;set_of_list]);
 390  (MATCH_MP_TAC Rogers.WQPRRDY);
 391  (ASM_REWRITE_TAC[IN]);
 392  (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
 393  (EXISTS_TAC `3` THEN REWRITE_TAC[ARITH_RULE `2 <= 3`]);
 394  (ASM_MESON_TAC[]);
 395  (REWRITE_TAC[IN_UNIONS]);
 396  (REPEAT STRIP_TAC);
 397
 398  (NEW_GOAL `?p:num->num. p permutes 0..2 /\ t = rogers V (left_action_list p (truncate_simplex 2 ul))`);
 399  (ASM_SET_TAC[]);
 400  (UP_ASM_TAC THEN STRIP_TAC);
 401  (ABBREV_TAC `zl:(real^3)list = left_action_list p (truncate_simplex 2 ul)`);
 402  (EXISTS_TAC `rogers V (left_action_list p ul)`);
 403  (STRIP_TAC);
 404  (ASM_SET_TAC[]);
 405  (ABBREV_TAC `vl:(real^3)list = left_action_list p ul`);
 406  (NEW_GOAL
 407    `rogers V vl =
 408      convex hull
 409      {HD vl, omega_list_n V vl 1, omega_list_n V vl 2, omega_list_n V vl 3}`);
 410  (MATCH_MP_TAC ROGERS_EXPLICIT);
 411  (ASM_REWRITE_TAC[]);
 412  (REWRITE_TAC[MESON[IN] `barV V 3 vl <=> vl IN barV V 3`]);
 413  (REWRITE_WITH `vl IN barV V 3 /\
 414                omega_list_n V vl 2 = omega_list_n V ul 2 /\
 415                omega_list_n V vl 3 = omega_list_n V ul 3 /\
 416                mxi V vl = mxi V ul`);
 417  (MATCH_MP_TAC LEFT_ACTION_LIST_PROPERTIES);
 418  (EXISTS_TAC `p:num->num` THEN ASM_REWRITE_TAC[]);
 419
 420  (NEW_GOAL `zl = truncate_simplex 2 (vl:(real^3)list)`);
 421  (EXPAND_TAC "zl" THEN EXPAND_TAC "vl");
 422  (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2; LENGTH;
 423    ARITH_RULE `SUC (SUC (SUC 0)) = 3`; TABLE_4; ARITH_RULE `SUC 3 = 4`;
 424    ASSUME `ul = [u0;u1;u2;u3:real^3]`; left_action_list]);
 425
 426  (REWRITE_WITH `EL (inverse p 0) [u0; u1; u2:real^3] =
 427                  EL (inverse p 0) [u0; u1; u2; u3] /\
 428                  EL (inverse p 1) [u0; u1; u2:real^3] =
 429                  EL (inverse p 1) [u0; u1; u2; u3] /\
 430                  EL (inverse p 2) [u0; u1; u2:real^3] =
 431                  EL (inverse p 2) [u0; u1; u2; u3]`);
 432  (REWRITE_WITH `[u0; u1; u2:real^3] = truncate_simplex 2 [u0; u1; u2; u3]`);
 433  (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
 434
 435  (NEW_GOAL `!i. i IN 0..2 ==> inverse p i IN 0..2`);
 436  (REPEAT STRIP_TAC);
 437  (ABBREV_TAC `y = inverse (p:num->num) i`);
 438  (ASM_CASES_TAC `y IN 0..2`);
 439  (ASM_REWRITE_TAC[]);
 440  (NEW_GOAL `F`);
 441  (MP_TAC (ASSUME `p permutes 0..2`) THEN REWRITE_TAC[permutes; EXISTS_UNIQUE]);
 442  (STRIP_TAC);
 443  (NEW_GOAL `(p:num->num) y = y`);
 444  (ASM_SIMP_TAC[]);
 445  (UP_ASM_TAC THEN EXPAND_TAC "y");
 446  (REWRITE_WITH `(p:num->num) (inverse p i) = i`);
 447  (MESON_TAC[PERMUTES_INVERSES; ASSUME `p permutes 0..2`]);
 448  (ASM_REWRITE_TAC[]);
 449  (ASM_MESON_TAC[]);
 450  (ASM_MESON_TAC[]);
 451
 452  (REPEAT STRIP_TAC);
 453  (MATCH_MP_TAC Packing3.EL_TRUNCATE_SIMPLEX);
 454  (REWRITE_TAC[LENGTH; ARITH_RULE `2 + 1 <= SUC(SUC(SUC(SUC 0)))`]);
 455  (NEW_GOAL `inverse p 0 IN 0..2`);
 456  (FIRST_ASSUM MATCH_MP_TAC);
 457  (REWRITE_TAC[IN_NUMSEG_0] THEN ARITH_TAC);
 458  (UP_ASM_TAC THEN REWRITE_TAC[IN_NUMSEG_0]);
 459
 460
 461  (MATCH_MP_TAC Packing3.EL_TRUNCATE_SIMPLEX);
 462  (REWRITE_TAC[LENGTH; ARITH_RULE `2 + 1 <= SUC(SUC(SUC(SUC 0)))`]);
 463  (NEW_GOAL `inverse p 1 IN 0..2`);
 464  (FIRST_ASSUM MATCH_MP_TAC);
 465  (REWRITE_TAC[IN_NUMSEG_0] THEN ARITH_TAC);
 466  (UP_ASM_TAC THEN REWRITE_TAC[IN_NUMSEG_0]);
 467
 468  (MATCH_MP_TAC Packing3.EL_TRUNCATE_SIMPLEX);
 469  (REWRITE_TAC[LENGTH; ARITH_RULE `2 + 1 <= SUC(SUC(SUC(SUC 0)))`]);
 470  (NEW_GOAL `inverse p 2 IN 0..2`);
 471  (FIRST_ASSUM MATCH_MP_TAC);
 472  (REWRITE_TAC[IN_NUMSEG_0] THEN ARITH_TAC);
 473  (UP_ASM_TAC THEN REWRITE_TAC[IN_NUMSEG_0]);
 474
 475  (NEW_GOAL `rogers V zl =
 476       convex hull {HD zl, omega_list_n V zl 1, omega_list_n V zl 2}`);
 477  (MATCH_MP_TAC ROGERS_EXPLICIT_2);
 478  (ASM_REWRITE_TAC[]);
 479  (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
 480  (EXISTS_TAC `3` THEN REWRITE_TAC[ARITH_RULE `2 <= 3`]);
 481
 482  (REWRITE_TAC[MESON[IN] `barV V 3 vl <=> vl IN barV V 3`]);
 483  (REWRITE_WITH `vl IN barV V 3 /\
 484                omega_list_n V vl 2 = omega_list_n V ul 2 /\
 485                omega_list_n V vl 3 = omega_list_n V ul 3 /\
 486                mxi V vl = mxi V ul`);
 487  (MATCH_MP_TAC LEFT_ACTION_LIST_PROPERTIES);
 488  (EXISTS_TAC `p:num->num` THEN ASM_REWRITE_TAC[]);
 489
 490
 491 (* ------------------------------ *)
 492  (NEW_GOAL
 493   `x1 IN convex hull {HD zl, omega_list_n V zl 1, omega_list_n V zl 2}`);
 494  (ASM_MESON_TAC[]);
 495  (UP_ASM_TAC THEN REWRITE_TAC[CONVEX_HULL_3;IN;IN_ELIM_THM]);
 496  (STRIP_TAC);
 497  (ABBREV_TAC `q1 = omega_list_n V zl 1`);
 498  (ABBREV_TAC `q2 = omega_list_n V zl 2`);
 499  (ABBREV_TAC `s3 = omega_list_n V ul 3`);
 500  (ABBREV_TAC `q0 = HD (zl:(real^3)list)`);
 501
 502  (NEW_GOAL `vl IN barV V 3 /\
 503              omega_list_n V vl 2 = omega_list_n V ul 2 /\
 504              omega_list_n V vl 3 = omega_list_n V ul 3 /\
 505              mxi V vl = mxi V ul`);
 506  (MATCH_MP_TAC LEFT_ACTION_LIST_PROPERTIES);
 507  (EXISTS_TAC `p:num->num`);
 508  (ASM_REWRITE_TAC[]);
 509  (UP_ASM_TAC THEN REWRITE_TAC[IN] THEN STRIP_TAC);
 510  (NEW_GOAL `?v0 v1 v2 v3. vl = [v0;v1;v2;v3:real^3]`);
 511  (MATCH_MP_TAC BARV_3_EXPLICIT);
 512  (EXISTS_TAC `V:real^3->bool`);
 513  (ASM_REWRITE_TAC[]);
 514  (UP_ASM_TAC THEN STRIP_TAC);
 515
 516  (NEW_GOAL `HD vl = q0:real^3`);
 517  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 518  (EXPAND_TAC "q0" THEN
 519    REWRITE_TAC[ASSUME `zl:(real^3)list = truncate_simplex 2 vl`]);
 520  (MATCH_MP_TAC Packing3.HD_TRUNCATE_SIMPLEX);
 521  (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC);
 522
 523  (NEW_GOAL `omega_list_n V vl 1 = q1`);
 524  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 525  (EXPAND_TAC "q1" THEN
 526    REWRITE_TAC[ASSUME `zl:(real^3)list = truncate_simplex 2 vl`]);
 527  (REWRITE_TAC[ARITH_RULE `2 = 1 + 1`]);
 528  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 529  (MATCH_MP_TAC Packing3.OMEGA_LIST_N_LEMMA);
 530  (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC);
 531
 532  (NEW_GOAL `omega_list_n V vl 2 = q2`);
 533  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 534  (EXPAND_TAC "q2" THEN
 535    REWRITE_TAC[ASSUME `zl:(real^3)list = truncate_simplex 2 vl`]);
 536  (REWRITE_WITH `truncate_simplex 2 (vl:(real^3)list) =
 537                  truncate_simplex (2 + 0) vl`);
 538  (REWRITE_TAC[ARITH_RULE `2 + 0 = 2`]);
 539  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 540  (MATCH_MP_TAC Packing3.OMEGA_LIST_N_LEMMA);
 541  (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC);
 542
 543  (UNDISCH_TAC `omega_list_n V vl 2 = omega_list_n V ul 2` THEN
 544    ASM_REWRITE_TAC[]);
 545  (DISCH_TAC);
 546  (NEW_GOAL `between m (q2, s3:real^3)`);
 547  (NEW_GOAL `?s. between s (omega_list_n V ul 2,omega_list_n V ul 3) /\
 548                   dist (u0,s) = sqrt (&2) /\
 549                   mxi V ul = s`);
 550  (MATCH_MP_TAC MXI_EXPLICIT);
 551  (EXISTS_TAC `u1:real^3` THEN EXISTS_TAC `u2:real^3` THEN
 552    EXISTS_TAC `u3:real^3` THEN ASM_REWRITE_TAC[]);
 553  (UP_ASM_TAC THEN STRIP_TAC);
 554  (ASM_MESON_TAC[]);
 555  (UP_ASM_TAC THEN REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;IN;IN_ELIM_THM;
 556    CONVEX_HULL_2; CONVEX_HULL_4]);
 557  (REPEAT STRIP_TAC);
 558  (EXISTS_TAC `t1 * u` THEN EXISTS_TAC `t1 * v`);
 559  (EXISTS_TAC `t1 * w + t2 * u'` THEN EXISTS_TAC `t2 * v'`);
 560  (ASM_SIMP_TAC[REAL_LE_MUL; REAL_LE_ADD]);
 561  (STRIP_TAC);
 562  (REWRITE_WITH
 563    `t1 * u + t1 * v + (t1 * w + t2 * u') + t2 * v' =
 564     t1 * (u + v + w) + t2 * (u' + v')`);
 565  (REAL_ARITH_TAC);
 566  (ASM_REWRITE_TAC[REAL_MUL_RID]);
 567  (VECTOR_ARITH_TAC);
 568  (SET_TAC[]);
 569
 570 (* ========================================================================= *)
 571
 572  (NEW_GOAL `k = 2`);
 573  (ASM_SET_TAC[]);
 574  (NEW_GOAL `?u0 u1 u2 u3. ul = [u0;u1;u2;u3:real^3]`);
 575  (MATCH_MP_TAC BARV_3_EXPLICIT THEN EXISTS_TAC `V:real^3->bool`);
 576  (ASM_REWRITE_TAC[]);
 577  (UP_ASM_TAC THEN STRIP_TAC);
 578  (SIMP_TAC[ASSUME `k = 2`; MCELL_EXPLICIT; mcell2]);
 579  (COND_CASES_TAC);
 580  (LET_TAC);
 581
 582  (ABBREV_TAC `m = mxi V ul`);
 583  (ABBREV_TAC `s2 = omega_list_n V ul 2`);
 584  (ABBREV_TAC `s3 = omega_list_n V ul 3`);
 585  (ASM_REWRITE_TAC[HD;TL; ARITH_RULE `2 - 1 = 1`]);
 586  (MATCH_MP_TAC (SET_RULE `(?C. C SUBSET B /\ A SUBSET C) ==> A SUBSET B`));
 587  (EXISTS_TAC `convex hull {u0, u1, s2, s3:real^3}`);
 588  (REPEAT STRIP_TAC); (* Two subgoals *)
 589
 590 (* ------------------------------------------------------ *)
 591
 592  (MATCH_MP_TAC (SET_RULE `(?C. C SUBSET B /\ A SUBSET C) ==> A SUBSET B`));
 593  (EXISTS_TAC `rogers V ul UNION rogers V [u1;u0;u2;u3:real^3]`);
 594  (STRIP_TAC);
 595  (REWRITE_TAC[SUBSET; IN_UNIONS; IN_UNION]);
 596  (REPEAT STRIP_TAC);
 597  (REWRITE_TAC[IN;IN_ELIM_THM]);
 598  (EXISTS_TAC `rogers V ul`);
 599  (STRIP_TAC);
 600  (EXISTS_TAC `I:num->num`);
 601  (ASM_REWRITE_TAC[PERMUTES_I; Packing3.LEFT_ACTION_LIST_I]);
 602  (UP_ASM_TAC THEN REWRITE_TAC[IN]);
 603
 604  (REWRITE_TAC[IN;IN_ELIM_THM]);
 605  (EXISTS_TAC `rogers V [u1;u0;u2;u3]`);
 606  (STRIP_TAC);
 607  (NEW_GOAL `?p. p permutes 0..1 /\ [u1;u0;u2;u3:real^3] = left_action_list p ul`);
 608  (MATCH_MP_TAC TWO_REARRANGEMENT_LEMMA);
 609  (EXISTS_TAC `V:real^3->bool`);
 610  (ASM_REWRITE_TAC[]);
 611  (UP_ASM_TAC THEN STRIP_TAC);
 612  (EXISTS_TAC `p:num->num`);
 613  (ASM_REWRITE_TAC[]);
 614  (UP_ASM_TAC THEN REWRITE_TAC[IN]);
 615  (NEW_GOAL `?p. p permutes 0..1 /\ [u1;u0;u2;u3:real^3] = left_action_list p ul`);
 616  (MATCH_MP_TAC TWO_REARRANGEMENT_LEMMA);
 617  (EXISTS_TAC `V:real^3->bool`);
 618  (ASM_REWRITE_TAC[]);
 619  (UP_ASM_TAC THEN STRIP_TAC);
 620
 621
 622  (ABBREV_TAC `vl = [u1;u0;u2;u3:real^3]`);
 623  (NEW_GOAL `barV V 3 vl /\
 624              (!j. 1 <= j /\ j <= 3
 625                   ==> omega_list_n V vl j = omega_list_n V ul j)`);
 626  (ONCE_REWRITE_TAC[ARITH_RULE `1 = 2 - 1`]);
 627  (MATCH_MP_TAC YNHYJIT);
 628  (EXISTS_TAC `p:num->num` THEN REWRITE_TAC[ARITH_RULE `2 - 1 = 1`]);
 629  (ASM_REWRITE_TAC[SET_RULE `2 IN {2,3,4}`]);
 630  (UP_ASM_TAC THEN STRIP_TAC);
 631  (ABBREV_TAC `s1 = omega_list_n V ul 1`);
 632  (NEW_GOAL `rogers V ul = convex hull {HD ul, s1, s2, s3}`);
 633  (EXPAND_TAC "s1" THEN EXPAND_TAC "s2" THEN EXPAND_TAC "s3");
 634  (MATCH_MP_TAC ROGERS_EXPLICIT);
 635  (ASM_REWRITE_TAC[]);
 636
 637  (NEW_GOAL `rogers V vl = convex hull {HD vl, omega_list_n V vl 1,
 638              omega_list_n V vl 2, omega_list_n V vl 3}`);
 639  (MATCH_MP_TAC ROGERS_EXPLICIT);
 640  (ASM_REWRITE_TAC[]);
 641
 642  (NEW_GOAL `omega_list_n V vl 1 = s1`);
 643  (EXPAND_TAC "s1" THEN FIRST_ASSUM MATCH_MP_TAC THEN ARITH_TAC);
 644  (NEW_GOAL `omega_list_n V vl 2 = s2`);
 645  (EXPAND_TAC "s2" THEN FIRST_ASSUM MATCH_MP_TAC THEN ARITH_TAC);
 646  (NEW_GOAL `omega_list_n V vl 3 = s3`);
 647  (EXPAND_TAC "s3" THEN FIRST_ASSUM MATCH_MP_TAC THEN ARITH_TAC);
 648
 649  (ASM_REWRITE_TAC[HD]);
 650  (REWRITE_TAC[GSYM (ASSUME `vl = left_action_list p (ul:(real^3)list)`);
 651   GSYM (ASSUME `ul = [u0; u1; u2; u3:real^3]`)]);
 652  (EXPAND_TAC "vl" THEN REWRITE_TAC[HD]);
 653
 654  (NEW_GOAL `s1 = circumcenter {u1, u0:real^3}`);
 655  (EXPAND_TAC "s1" THEN MATCH_MP_TAC Marchal_cells_2_new.OMEGA_LIST_1_EXPLICIT_NEW);
 656  (EXISTS_TAC `u2:real^3` THEN EXISTS_TAC `u3:real^3` THEN REWRITE_TAC[IN]);
 657  (ASM_REWRITE_TAC[]);
 658  (REWRITE_WITH `hl [u1;u0:real^3] =
 659    hl (truncate_simplex 1 (ul:(real^3)list))`);
 660  (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1; HL]);
 661  (REWRITE_TAC[set_of_list; SET_RULE `{a,b} = {b,a}`]);
 662  (ASM_REWRITE_TAC[]);
 663  (UP_ASM_TAC THEN REWRITE_TAC[CIRCUMCENTER_2;midpoint] THEN STRIP_TAC);
 664  (ASM_REWRITE_TAC[]);
 665
 666  (REWRITE_TAC[SUBSET; CONVEX_HULL_4; IN; IN_ELIM_THM; IN_UNION]);
 667  (REPEAT STRIP_TAC);
 668
 669  (ASM_CASES_TAC `u <= v:real`);
 670  (DISJ2_TAC);
 671  (EXISTS_TAC `v - u:real` THEN EXISTS_TAC `&2 * u`);
 672  (EXISTS_TAC `w:real` THEN EXISTS_TAC `z:real`);
 673  (ASM_SIMP_TAC[REAL_ARITH `v - u + &2 * u + w + z = u + v + w + z`; REAL_LE_MUL; REAL_ARITH `&0 <= &2`; REAL_ARITH `&0 <= a - b <=> b <= a`]);
 674  (VECTOR_ARITH_TAC);
 675  (NEW_GOAL `v <= u:real`);
 676  (ASM_REAL_ARITH_TAC);
 677  (DISJ1_TAC);
 678  (EXISTS_TAC `u - v:real` THEN EXISTS_TAC `&2 * v`);
 679  (EXISTS_TAC `w:real` THEN EXISTS_TAC `z:real`);
 680  (ASM_SIMP_TAC[REAL_ARITH `u - v + &2 * v + w + z = u + v + w + z`;
 681    REAL_LE_MUL; REAL_ARITH `&0 <= &2`; REAL_ARITH `&0 <= a - b <=> b <= a`]);
 682  (VECTOR_ARITH_TAC);
 683
 684 (* ------------------------------------------------------ *)
 685
 686  (REWRITE_TAC[SUBSET; IN_INTER]);
 687  (REPEAT STRIP_TAC);
 688  (ABBREV_TAC `s1 = omega_list_n V ul 1`);
 689
 690  (NEW_GOAL `s1 = circumcenter {u0, u1:real^3}`);
 691  (EXPAND_TAC "s1" THEN MATCH_MP_TAC Marchal_cells_2_new.OMEGA_LIST_1_EXPLICIT_NEW);
 692  (EXISTS_TAC `u2:real^3` THEN EXISTS_TAC `u3:real^3` THEN REWRITE_TAC[IN]);
 693  (ASM_REWRITE_TAC[]);
 694  (REWRITE_WITH `hl [u0;u1:real^3] =
 695    hl (truncate_simplex 1 (ul:(real^3)list))`);
 696  (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1; HL;set_of_list]);
 697  (ASM_REWRITE_TAC[]);
 698
 699  (ABBREV_TAC `vl:(real^3)list = truncate_simplex 1 ul`);
 700
 701  (NEW_GOAL `s1:real^3 IN voronoi_list V vl`);
 702  (EXPAND_TAC "vl" THEN EXPAND_TAC "s1");
 703  (MATCH_MP_TAC Rogers.OMEGA_LIST_N_IN_VORONOI_LIST_GEN);
 704  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
 705  (NEW_GOAL `s2:real^3 IN voronoi_list V vl`);
 706  (EXPAND_TAC "vl" THEN EXPAND_TAC "s2");
 707  (MATCH_MP_TAC Rogers.OMEGA_LIST_N_IN_VORONOI_LIST_GEN);
 708  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
 709  (NEW_GOAL `s3:real^3 IN voronoi_list V vl`);
 710  (EXPAND_TAC "vl" THEN EXPAND_TAC "s3");
 711  (MATCH_MP_TAC Rogers.OMEGA_LIST_N_IN_VORONOI_LIST_GEN);
 712  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
 713
 714  (NEW_GOAL `m IN voronoi_list V vl`);
 715  (ASM_CASES_TAC `hl (truncate_simplex 2 (ul:(real^3)list)) >= sqrt (&2)`);
 716  (REWRITE_WITH `m = s2:real^3`);
 717  (EXPAND_TAC "m" THEN REWRITE_TAC[mxi]);
 718  (COND_CASES_TAC);
 719  (ASM_REWRITE_TAC[]);
 720  (NEW_GOAL `F`);
 721  (ASM_MESON_TAC[]);
 722  (ASM_MESON_TAC[]);
 723  (ASM_REWRITE_TAC[]);
 724  (NEW_GOAL `(?s. between s (omega_list_n V ul 2,omega_list_n V ul 3) /\
 725                   dist (u0,s) = sqrt (&2) /\
 726                   mxi V ul = s)`);
 727  (MATCH_MP_TAC MXI_EXPLICIT);
 728  (EXISTS_TAC `u1:real^3` THEN EXISTS_TAC `u2:real^3` THEN EXISTS_TAC `u3:real^3`);
 729  (ASM_REWRITE_TAC[]);
 730  (UP_ASM_TAC THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);
 731  (FIRST_X_ASSUM CHOOSE_TAC THEN UP_ASM_TAC THEN ASM_REWRITE_TAC[]);
 732  (STRIP_TAC);
 733  (ASM_REWRITE_TAC[]);
 734  (MATCH_MP_TAC (SET_RULE `(?C. x IN C /\ C SUBSET B) ==> x IN B`));
 735  (EXISTS_TAC `convex hull {s2, s3:real^3}`);
 736  (STRIP_TAC);
 737  (ASM_REWRITE_TAC[GSYM BETWEEN_IN_CONVEX_HULL]);
 738  (REWRITE_WITH `convex hull {s2, s3:real^3} SUBSET voronoi_list V vl <=>
 739    convex hull {s2, s3} SUBSET (convex hull (voronoi_list V vl))`);
 740  (REWRITE_WITH `convex hull (voronoi_list V vl) = voronoi_list V vl`);
 741  (REWRITE_TAC[CONVEX_HULL_EQ]);
 742  (REWRITE_TAC[Packing3.CONVEX_VORONOI_LIST]);
 743  (MATCH_MP_TAC Marchal_cells.CONVEX_HULL_SUBSET);
 744  (ASM_SET_TAC[]);
 745
 746  (NEW_GOAL `~(u0 = u1:real^3)`);
 747  (STRIP_TAC);
 748  (NEW_GOAL `LENGTH (ul:(real^3)list) = 3 + 1 /\
 749              CARD (set_of_list ul) = 3 + 1`);
 750  (MATCH_MP_TAC Rogers.BARV_IMP_LENGTH_EQ_CARD);
 751  (EXISTS_TAC `V:real^3->bool`);
 752  (ASM_REWRITE_TAC[]);
 753  (UP_ASM_TAC THEN ASM_REWRITE_TAC[set_of_list;
 754    SET_RULE `{u1, u1, u2, u3} = {u1,u2,u3}`]);
 755  (NEW_GOAL `CARD {u1,u2,u3:real^3} <= 3`);
 756  (REWRITE_TAC[Geomdetail.CARD3]);
 757  (ASM_ARITH_TAC);
 758
 759  (UNDISCH_TAC `x IN aff_ge {u0, u1} {m, s3:real^3}`);
 760  (REWRITE_WITH `aff_ge {u0, u1} {m, s3:real^3} =
 761              {y | ?t1 t2 t3 t4.
 762                       &0 <= t3 /\
 763                       &0 <= t4 /\
 764                       t1 + t2 + t3 + t4 = &1 /\
 765                       y = t1 % u0 + t2 % u1 + t3 % m + t4 % s3}`);
 766  (MATCH_MP_TAC AFF_GE_2_2);
 767
 768  (NEW_GOAL `~(m IN {u0, u1:real^3})`);
 769  (STRIP_TAC);
 770
 771  (ASM_CASES_TAC `m = u0:real^3`);
 772  (UNDISCH_TAC `m IN voronoi_list V vl`);
 773  (EXPAND_TAC "vl" THEN REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1;set_of_list;
 774    ASSUME `ul = [u0;u1;u2;u3:real^3]`; VORONOI_LIST; VORONOI_SET]);
 775  (STRIP_TAC);
 776  (NEW_GOAL `m:real^3 IN voronoi_closed V u1`);
 777  (UP_ASM_TAC THEN SET_TAC[]);
 778  (UP_ASM_TAC THEN ASM_REWRITE_TAC[voronoi_closed; IN; IN_ELIM_THM]);
 779  (REPEAT STRIP_TAC);
 780  (NEW_GOAL `dist (u0, u1:real^3) <= dist (u0, u0)`);
 781  (FIRST_ASSUM MATCH_MP_TAC);
 782  (NEW_GOAL `{u0, u1, u2, u3:real^3} SUBSET V`);
 783  (REWRITE_WITH `{u0, u1, u2, u3:real^3} = set_of_list ul`);
 784  (ASM_REWRITE_TAC[set_of_list]);
 785  (MATCH_MP_TAC Packing3.BARV_SUBSET);
 786  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]);
 787  (ONCE_REWRITE_TAC[MESON[IN] `V u0 <=> u0 IN V`]);
 788  (UP_ASM_TAC THEN SET_TAC[]);
 789  (UP_ASM_TAC THEN REWRITE_TAC[DIST_REFL]);
 790  (STRIP_TAC);
 791  (NEW_GOAL `dist (u0, u1:real^3) = &0`);
 792  (NEW_GOAL `&0 <= dist (u0, u1:real^3)`);
 793  (REWRITE_TAC[DIST_POS_LE]);
 794  (ASM_REAL_ARITH_TAC);
 795  (UP_ASM_TAC THEN REWRITE_TAC[DIST_EQ_0]);
 796  (ASM_REWRITE_TAC[]);
 797
 798  (ASM_CASES_TAC `m = u1:real^3`);
 799  (UNDISCH_TAC `m IN voronoi_list V vl`);
 800  (EXPAND_TAC "vl" THEN REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1;set_of_list;
 801    ASSUME `ul = [u0;u1;u2;u3:real^3]`; VORONOI_LIST; VORONOI_SET]);
 802  (STRIP_TAC);
 803  (NEW_GOAL `m:real^3 IN voronoi_closed V u0`);
 804  (UP_ASM_TAC THEN SET_TAC[]);
 805  (UP_ASM_TAC THEN ASM_REWRITE_TAC[voronoi_closed; IN; IN_ELIM_THM]);
 806  (REPEAT STRIP_TAC);
 807  (NEW_GOAL `dist (u1, u0:real^3) <= dist (u1, u1)`);
 808  (FIRST_ASSUM MATCH_MP_TAC);
 809  (NEW_GOAL `{u0, u1, u2, u3:real^3} SUBSET V`);
 810  (REWRITE_WITH `{u0, u1, u2, u3:real^3} = set_of_list ul`);
 811  (ASM_REWRITE_TAC[set_of_list]);
 812  (MATCH_MP_TAC Packing3.BARV_SUBSET);
 813  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]);
 814  (ONCE_REWRITE_TAC[MESON[IN] `V u0 <=> u0 IN V`]);
 815  (UP_ASM_TAC THEN SET_TAC[]);
 816  (UP_ASM_TAC THEN REWRITE_TAC[DIST_REFL]);
 817  (STRIP_TAC);
 818  (NEW_GOAL `dist (u1, u0:real^3) = &0`);
 819  (NEW_GOAL `&0 <= dist (u1, u0:real^3)`);
 820  (REWRITE_TAC[DIST_POS_LE]);
 821  (ASM_REAL_ARITH_TAC);
 822  (UP_ASM_TAC THEN REWRITE_TAC[DIST_EQ_0]);
 823  (ASM_MESON_TAC[]);
 824  (ASM_SET_TAC[]);
 825
 826
 827  (NEW_GOAL `~(s3 IN {u0, u1:real^3})`);
 828  (STRIP_TAC);
 829
 830  (ASM_CASES_TAC `s3 = u0:real^3`);
 831  (UNDISCH_TAC `s3 IN voronoi_list V vl`);
 832  (EXPAND_TAC "vl" THEN REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1;set_of_list;
 833    ASSUME `ul = [u0;u1;u2;u3:real^3]`; VORONOI_LIST; VORONOI_SET]);
 834  (STRIP_TAC);
 835  (NEW_GOAL `s3:real^3 IN voronoi_closed V u1`);
 836  (UP_ASM_TAC THEN SET_TAC[]);
 837  (UP_ASM_TAC THEN ASM_REWRITE_TAC[voronoi_closed; IN; IN_ELIM_THM]);
 838  (REPEAT STRIP_TAC);
 839  (NEW_GOAL `dist (u0, u1:real^3) <= dist (u0, u0)`);
 840  (FIRST_ASSUM MATCH_MP_TAC);
 841  (NEW_GOAL `{u0, u1, u2, u3:real^3} SUBSET V`);
 842  (REWRITE_WITH `{u0, u1, u2, u3:real^3} = set_of_list ul`);
 843  (ASM_REWRITE_TAC[set_of_list]);
 844  (MATCH_MP_TAC Packing3.BARV_SUBSET);
 845  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]);
 846  (ONCE_REWRITE_TAC[MESON[IN] `V u0 <=> u0 IN V`]);
 847  (UP_ASM_TAC THEN SET_TAC[]);
 848  (UP_ASM_TAC THEN REWRITE_TAC[DIST_REFL]);
 849  (STRIP_TAC);
 850  (NEW_GOAL `dist (u0, u1:real^3) = &0`);
 851  (NEW_GOAL `&0 <= dist (u0, u1:real^3)`);
 852  (REWRITE_TAC[DIST_POS_LE]);
 853  (ASM_REAL_ARITH_TAC);
 854  (UP_ASM_TAC THEN REWRITE_TAC[DIST_EQ_0]);
 855  (ASM_REWRITE_TAC[]);
 856
 857  (ASM_CASES_TAC `s3 = u1:real^3`);
 858  (UNDISCH_TAC `s3 IN voronoi_list V vl`);
 859  (EXPAND_TAC "vl" THEN REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1;set_of_list;
 860    ASSUME `ul = [u0;u1;u2;u3:real^3]`; VORONOI_LIST; VORONOI_SET]);
 861  (STRIP_TAC);
 862  (NEW_GOAL `s3:real^3 IN voronoi_closed V u0`);
 863  (UP_ASM_TAC THEN SET_TAC[]);
 864  (UP_ASM_TAC THEN ASM_REWRITE_TAC[voronoi_closed; IN; IN_ELIM_THM]);
 865  (REPEAT STRIP_TAC);
 866  (NEW_GOAL `dist (u1, u0:real^3) <= dist (u1, u1)`);
 867  (FIRST_ASSUM MATCH_MP_TAC);
 868  (NEW_GOAL `{u0, u1, u2, u3:real^3} SUBSET V`);
 869  (REWRITE_WITH `{u0, u1, u2, u3:real^3} = set_of_list ul`);
 870  (ASM_REWRITE_TAC[set_of_list]);
 871  (MATCH_MP_TAC Packing3.BARV_SUBSET);
 872  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]);
 873  (ONCE_REWRITE_TAC[MESON[IN] `V u0 <=> u0 IN V`]);
 874  (UP_ASM_TAC THEN SET_TAC[]);
 875  (UP_ASM_TAC THEN REWRITE_TAC[DIST_REFL]);
 876  (STRIP_TAC);
 877  (NEW_GOAL `dist (u1, u0:real^3) = &0`);
 878  (NEW_GOAL `&0 <= dist (u1, u0:real^3)`);
 879  (REWRITE_TAC[DIST_POS_LE]);
 880  (ASM_REAL_ARITH_TAC);
 881  (UP_ASM_TAC THEN REWRITE_TAC[DIST_EQ_0]);
 882  (ASM_MESON_TAC[]);
 883  (ASM_SET_TAC[]);
 884
 885  (REWRITE_TAC[DISJOINT]);
 886  (ASM_SET_TAC[]);
 887
 888 (*  ======================================================================== *)
 889 (* OK here *)
 890
 891  (REWRITE_TAC[IN; IN_ELIM_THM]);
 892  (REPEAT STRIP_TAC);
 893  (NEW_GOAL `&0 <= t1 /\ &0 <= t2`);
 894
 895  (ASM_CASES_TAC `&0 < t3 + t4`);
 896  (ABBREV_TAC `t5 = t3 + t4:real`);
 897  (ABBREV_TAC `z = t3 / t5 % m + t4 / t5 % (s3:real^3)`);
 898  (NEW_GOAL `between z (m, s3:real^3)`);
 899  (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;CONVEX_HULL_2;IN;IN_ELIM_THM]);
 900  (EXISTS_TAC `t3 / t5` THEN EXISTS_TAC `t4 / t5`);
 901  (ASM_SIMP_TAC[REAL_LE_DIV; REAL_ARITH `&0 < a ==> &0 <= a`]);
 902  (ASM_REWRITE_TAC[REAL_ARITH `a/b+c/b = (a+c)/b`]);
 903  (MATCH_MP_TAC REAL_DIV_REFL THEN ASM_REAL_ARITH_TAC);
 904
 905  (NEW_GOAL `z IN voronoi_list V vl`);
 906  (MATCH_MP_TAC (SET_RULE `(?C. x IN C /\ C SUBSET B) ==> x IN B`));
 907  (EXISTS_TAC `convex hull {m, s3:real^3}`);
 908  (STRIP_TAC);
 909  (ASM_REWRITE_TAC[GSYM BETWEEN_IN_CONVEX_HULL]);
 910  (REWRITE_WITH `convex hull {m, s3:real^3} SUBSET voronoi_list V vl <=>
 911    convex hull {m, s3} SUBSET (convex hull (voronoi_list V vl))`);
 912  (REWRITE_WITH `convex hull (voronoi_list V vl) = voronoi_list V vl`);
 913  (REWRITE_TAC[CONVEX_HULL_EQ]);
 914  (REWRITE_TAC[Packing3.CONVEX_VORONOI_LIST]);
 915  (MATCH_MP_TAC Marchal_cells.CONVEX_HULL_SUBSET);
 916  (ASM_SET_TAC[]);
 917
 918 (* ------------------------------------------------------------------------ *)
 919
 920  (ASM_CASES_TAC `t1 < &0`);
 921  (NEW_GOAL `F`);
 922  (UNDISCH_TAC `x:real^3 IN rcone_ge u1 u0 a`);
 923  (REWRITE_TAC[rcone_ge;rconesgn; IN; IN_ELIM_THM]);
 924  (REWRITE_TAC[REAL_ARITH `~(a >= b) <=> a < b`]);
 925  (NEW_GOAL `x = t1 % u0 + t2 % u1 + t5 % (z:real^3)`);
 926  (ASM_REWRITE_TAC[] THEN EXPAND_TAC "z" THEN EXPAND_TAC "t5");
 927  (REWRITE_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC]);
 928  (REWRITE_TAC[REAL_ARITH `a * b / a = b * (a / a)`]);
 929  (ASM_SIMP_TAC[REAL_DIV_REFL; REAL_ARITH `&0 < y ==> ~(y = &0)`;
 930   REAL_MUL_RID]);
 931  (REWRITE_TAC[dist]);
 932  (REWRITE_WITH `x - u1:real^3 = t1 % (u0 - u1) + t5 % (z - u1)`);
 933  (REWRITE_WITH `x - u1:real^3 = x - (t1 + t2 + t5) % u1`);
 934  (REWRITE_WITH `t1 + t2 + t5 = &1`);
 935  (ASM_REAL_ARITH_TAC);
 936  (VECTOR_ARITH_TAC);
 937  (REWRITE_TAC[ASSUME `x = t1 % u0 + t2 % u1 + t5 % z:real^3`]);
 938  (VECTOR_ARITH_TAC);
 939
 940  (REWRITE_TAC[DOT_LADD; DOT_LMUL; GSYM NORM_POW_2]);
 941  (NEW_GOAL `(z - u1) dot (u0 - u1:real^3) <=
 942              norm (z - u1:real^3) * norm (u0 - u1) * a`);
 943
 944  (ASM_CASES_TAC `hl (truncate_simplex 2 (ul:(real^3)list)) >= sqrt (&2)`);
 945  (NEW_GOAL `m = s2:real^3`);
 946  (EXPAND_TAC "m" THEN REWRITE_TAC[mxi] THEN COND_CASES_TAC);
 947  (ASM_REWRITE_TAC[]);
 948  (NEW_GOAL `F`);
 949  (ASM_MESON_TAC[]);
 950  (ASM_MESON_TAC[]);
 951
 952  (NEW_GOAL `u0 - u1 = &2 % (u0 - s1:real^3)`);
 953  (REWRITE_TAC[ASSUME `s1 = circumcenter {u0, u1:real^3}`; CIRCUMCENTER_2;
 954   midpoint; VECTOR_ARITH `u0 - inv (&2) % (u0 + u1) = inv (&2) % (u0 - u1)`]);
 955  (VECTOR_ARITH_TAC);
 956
 957  (NEW_GOAL `(z - s1) dot (u0 - s1:real^3) = &0`);
 958  (ASM_REWRITE_TAC[]);
 959  (REWRITE_WITH `{u0,u1:real^3} = set_of_list vl`);
 960  (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_1;
 961    ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
 962  (MATCH_MP_TAC Rogers.MHFTTZN4);
 963  (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `1`);
 964  (REPEAT STRIP_TAC);
 965  (ASM_REWRITE_TAC[]);
 966  (EXPAND_TAC "vl" THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
 967  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
 968  (MATCH_MP_TAC (SET_RULE `(?C. a IN C/\ C SUBSET B) ==> a IN B`));
 969  (EXISTS_TAC `voronoi_list V vl`);
 970  (ASM_REWRITE_TAC[SET_SUBSET_AFFINE_HULL]);
 971  (MATCH_MP_TAC (SET_RULE `(?C. a IN C/\ C SUBSET B) ==> a IN B`));
 972  (EXISTS_TAC `set_of_list (vl:(real^3)list)`);
 973  (ASM_REWRITE_TAC[SET_SUBSET_AFFINE_HULL]);
 974  (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_1;
 975    ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
 976  (SET_TAC[]);
 977
 978  (NEW_GOAL `norm (s2 - u1) <= norm (z - u1:real^3)`);
 979  (REWRITE_WITH `norm (s2 - u1) <= norm (z - u1:real^3) <=>
 980                  norm (s2 - u1) pow 2 <= norm (z - u1:real^3) pow 2`);
 981  (ASM_SIMP_TAC[Collect_geom.POW2_COND; NORM_POS_LE]);
 982  (REWRITE_WITH `s2 - u1 = (s2 - s1) + (s1 - u1:real^3) /\
 983                   z - u1 = (z - s1) + (s1 - u1:real^3)`);
 984  (VECTOR_ARITH_TAC);
 985  (REWRITE_WITH `norm (s2 - s1 + s1 - u1) pow 2 =
 986    norm (s2 - s1) pow 2 + norm (s1 - u1:real^3) pow 2`);
 987  (NEW_GOAL `(s2 - s1) dot (s1 - u1:real^3) = &0`);
 988  (REWRITE_WITH `s1 - u1 = u0 - s1:real^3`);
 989  (ASM_REWRITE_TAC[CIRCUMCENTER_2; midpoint] THEN VECTOR_ARITH_TAC);
 990  (ASM_REWRITE_TAC[]);
 991  (REWRITE_WITH `{u0,u1:real^3} = set_of_list vl`);
 992  (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_1;
 993    ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
 994  (MATCH_MP_TAC Rogers.MHFTTZN4);
 995  (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `1`);
 996  (REPEAT STRIP_TAC);
 997  (ASM_REWRITE_TAC[]);
 998  (EXPAND_TAC "vl" THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
 999  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
1000  (MATCH_MP_TAC (SET_RULE `(?C. a IN C/\ C SUBSET B) ==> a IN B`));
1001  (EXISTS_TAC `voronoi_list V vl`);
1002  (ASM_REWRITE_TAC[SET_SUBSET_AFFINE_HULL]);
1003  (MATCH_MP_TAC (SET_RULE `(?C. a IN C/\ C SUBSET B) ==> a IN B`));
1004  (EXISTS_TAC `set_of_list (vl:(real^3)list)`);
1005  (ASM_REWRITE_TAC[SET_SUBSET_AFFINE_HULL]);
1006  (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_1;
1007    ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
1008  (SET_TAC[]);
1009  (ASM_SIMP_TAC[Trigonometry2.PITHAGO_THEOREM]);
1010
1011  (REWRITE_WITH `norm (z - s1 + s1 - u1:real^3) pow 2 =
1012                  norm (z - s1) pow 2 + norm (s1 - u1) pow 2`);
1013  (NEW_GOAL `(z - s1) dot (s1 - u1:real^3) = &0`);
1014  (REWRITE_WITH `s1 - u1 = u0 - s1:real^3`);
1015  (ASM_REWRITE_TAC[CIRCUMCENTER_2; midpoint] THEN VECTOR_ARITH_TAC);
1016  (ASM_REWRITE_TAC[]);
1017  (ASM_SIMP_TAC[Trigonometry2.PITHAGO_THEOREM]);
1018  (REWRITE_TAC[REAL_ARITH `a + b <= c + b <=> a <= c`]);
1019  (REWRITE_TAC[GSYM (ASSUME `omega_list_n V ul 2 = s2`)] THEN
1020    REWRITE_TAC[OMEGA_LIST_N; ARITH_RULE `2 = SUC 1`]);
1021  (REWRITE_TAC[ARITH_RULE `SUC 1 = 2`]);
1022  (REWRITE_TAC[GSYM dist; DIST_SYM]);
1023  (ASM_REWRITE_TAC[]);
1024  (REWRITE_WITH `!a b c d:real^3.
1025    dist (a, b:real^3) pow 2 <= dist (c,d) pow 2 <=> dist (a,b) <= dist (c,d)`);
1026  (REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[EQ_SYM_EQ]);
1027  (SIMP_TAC[Collect_geom.POW2_COND; DIST_POS_LE]);
1028  (MATCH_MP_TAC CLOSEST_POINT_LE);
1029  (REWRITE_TAC[Packing3.CLOSED_VORONOI_LIST]);
1030  (REWRITE_TAC[GSYM (ASSUME `ul = [u0;u1;u2;u3:real^3]`)]);
1031  (ABBREV_TAC `zl:(real^3)list = truncate_simplex 2 ul`);
1032
1033  (NEW_GOAL `s2:real^3 IN voronoi_list V zl`);
1034  (EXPAND_TAC "zl" THEN REWRITE_TAC[GSYM (ASSUME `omega_list_n V ul 2 = s2`)]);
1035  (MATCH_MP_TAC Rogers.OMEGA_LIST_N_IN_VORONOI_LIST_GEN);
1036  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
1037  (NEW_GOAL `s3:real^3 IN voronoi_list V zl`);
1038  (EXPAND_TAC "zl" THEN EXPAND_TAC "s3");
1039  (MATCH_MP_TAC Rogers.OMEGA_LIST_N_IN_VORONOI_LIST_GEN);
1040  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
1041  (MATCH_MP_TAC (SET_RULE `(?C. x IN C /\ C SUBSET B) ==> x IN B`));
1042  (EXISTS_TAC `convex hull {s2, s3:real^3}`);
1043  (STRIP_TAC);
1044  (ASM_REWRITE_TAC[GSYM BETWEEN_IN_CONVEX_HULL]);
1045  (ASM_MESON_TAC[]);
1046  (REWRITE_WITH `convex hull {s2, s3:real^3} SUBSET voronoi_list V zl <=>
1047    convex hull {s2, s3} SUBSET (convex hull (voronoi_list V zl))`);
1048  (REWRITE_WITH `convex hull (voronoi_list V zl) = voronoi_list V zl`);
1049  (REWRITE_TAC[CONVEX_HULL_EQ]);
1050  (REWRITE_TAC[Packing3.CONVEX_VORONOI_LIST]);
1051  (MATCH_MP_TAC Marchal_cells.CONVEX_HULL_SUBSET);
1052  (ASM_SET_TAC[]);
1053
1054  (REWRITE_WITH `(z - u1) dot (u0 - u1:real^3) = &2 *  norm (u0 - s1) pow 2`);
1055  (REWRITE_WITH `(z - u1) dot (u0 - u1) = (z - s1) dot (u0 - u1) +
1056                  (s1 - u1) dot (u0 - u1:real^3)`);
1057  (VECTOR_ARITH_TAC);
1058  (REWRITE_TAC[ASSUME `u0 - u1 = &2 % (u0 - s1:real^3)`; DOT_RMUL]);
1059  (REWRITE_WITH `(s1 - u1) = (u0 - s1:real^3)`);
1060  (ASM_REWRITE_TAC[CIRCUMCENTER_2;midpoint] THEN VECTOR_ARITH_TAC);
1061  (ASM_REWRITE_TAC[NORM_POW_2] THEN REAL_ARITH_TAC);
1062
1063
1064  (NEW_GOAL `&2 * norm (u0 - s1:real^3) pow 2 <=
1065              norm (s2 - u1) * norm (u0 - u1) * a`);
1066  (NEW_GOAL `norm (s2 - u1:real^3) >= sqrt (&2)`);
1067  (NEW_GOAL `norm (s2 - u1:real^3) >=
1068              hl (truncate_simplex 2 (ul:(real^3)list))`);
1069  (REWRITE_TAC[GSYM dist]);
1070  (NEW_GOAL `?p. p permutes 0..1 /\
1071                     [u1; u0; u2; u3:real^3] = left_action_list p ul`);
1072  (MATCH_MP_TAC TWO_REARRANGEMENT_LEMMA);
1073  (EXISTS_TAC `V:real^3->bool`);
1074  (ASM_REWRITE_TAC[]);
1075  (UP_ASM_TAC THEN STRIP_TAC);
1076  (ABBREV_TAC `ul' = [u1;u0;u2;u3:real^3]`);
1077  (NEW_GOAL `barV V 3 ul' /\
1078              (!j. 1 <= j /\ j <= 3
1079                   ==> omega_list_n V ul' j = omega_list_n V ul j)`);
1080  (ONCE_REWRITE_TAC[ARITH_RULE `1 = 2 - 1`]);
1081  (MATCH_MP_TAC YNHYJIT);
1082  (EXISTS_TAC `p:num->num` THEN REWRITE_TAC[ARITH_RULE `2 - 1 = 1`;
1083    SET_RULE `2 IN {2,3,4}`]);
1084  (ASM_REWRITE_TAC[]);
1085  (UP_ASM_TAC THEN STRIP_TAC);
1086  (REWRITE_WITH `s2 = omega_list_n V ul' 2 /\ u1 = HD ul'`);
1087  (STRIP_TAC);
1088  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
1089  (REWRITE_TAC[GSYM (ASSUME `omega_list_n V ul 2 = s2`)] );
1090  (FIRST_ASSUM MATCH_MP_TAC THEN ARITH_TAC);
1091  (REWRITE_TAC[GSYM (ASSUME `[u1; u0; u2; u3:real^3] = ul'`); HD] );
1092  (REWRITE_TAC[REAL_ARITH `a >= b <=> b <= a`]);
1093  (ABBREV_TAC `xl:(real^3)list = truncate_simplex 2 ul'`);
1094  (REWRITE_WITH `hl (truncate_simplex 2 (ul:(real^3)list)) =
1095                  hl (xl:(real^3)list)`);
1096  (EXPAND_TAC "xl");
1097  (REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`;
1098    GSYM (ASSUME `[u1;u0;u2;u3:real^3] = ul'`); TRUNCATE_SIMPLEX_EXPLICIT_2]);
1099  (REWRITE_TAC[HL; set_of_list; SET_RULE `{u0, u1, u2} = {u1,u0,u2}`]);
1100  (REWRITE_WITH `omega_list_n V ul' 2 = omega_list V xl`);
1101  (REWRITE_WITH `omega_list V xl = omega_list_n V xl 2`);
1102  (REWRITE_TAC[OMEGA_LIST]);
1103  (EXPAND_TAC "xl" THEN REWRITE_TAC[GSYM
1104   (ASSUME `[u1; u0; u2; u3:real^3] = ul'`); TRUNCATE_SIMPLEX_EXPLICIT_2]);
1105  (REWRITE_TAC[LENGTH; ARITH_RULE `(SUC (SUC (SUC 0)) - 1) = 2`]);
1106  (EXPAND_TAC "xl");
1107  (REWRITE_WITH
1108   `truncate_simplex 2 (ul':(real^3)list) = truncate_simplex (2 + 0) ul'`);
1109  (REWRITE_TAC[ARITH_RULE `2 + 0 = 2`]);
1110  (MATCH_MP_TAC Packing3.OMEGA_LIST_N_LEMMA);
1111  (REWRITE_TAC[GSYM (ASSUME `[u1; u0; u2; u3:real^3] = ul'`); LENGTH]);
1112  (ARITH_TAC);
1113  (REWRITE_WITH `HD ul' = HD (xl:(real^3)list)`);
1114  (ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN EXPAND_TAC "xl");
1115  (MATCH_MP_TAC Packing3.HD_TRUNCATE_SIMPLEX);
1116  (REWRITE_TAC[GSYM (ASSUME `[u1; u0; u2; u3:real^3] = ul'`); LENGTH]);
1117  (ARITH_TAC);
1118  (MATCH_MP_TAC Rogers.WAUFCHE1);
1119  (EXISTS_TAC `2`);
1120  (REWRITE_TAC[IN] THEN EXPAND_TAC "xl");
1121  (STRIP_TAC);
1122  (ASM_REWRITE_TAC[]);
1123  (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
1124  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
1125  (ASM_REAL_ARITH_TAC);
1126
1127  (EXPAND_TAC "a");
1128  (REWRITE_WITH `hl (vl:(real^3)list) = dist (s1, u0:real^3)`);
1129  (REWRITE_WITH `s1:real^3 = circumcenter (set_of_list vl)`);
1130  (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`;
1131    TRUNCATE_SIMPLEX_EXPLICIT_1; set_of_list]);
1132  (ASM_REWRITE_TAC[]);
1133
1134  (REWRITE_WITH `u0:real^3 = HD vl`);
1135  (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`;
1136    TRUNCATE_SIMPLEX_EXPLICIT_1; set_of_list; HD]);
1137  (MATCH_MP_TAC Rogers.HL_EQ_DIST0);
1138  (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `1` THEN ASM_REWRITE_TAC[]);
1139  (EXPAND_TAC "vl");
1140  (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
1141  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
1142  (ONCE_REWRITE_TAC[DIST_SYM] THEN REWRITE_TAC[dist]);
1143  (REWRITE_TAC[ASSUME `u0 - u1 = &2 % (u0 - s1:real^3)`; NORM_MUL]);
1144  (REWRITE_WITH `abs (&2) = &2`);
1145  (REWRITE_TAC[REAL_ABS_REFL; REAL_ARITH `&0 <= &2`]);
1146  (REWRITE_TAC[REAL_ARITH `a * (&2 * b) * b / c = (&2 * b pow 2) * ( a / c)`]);
1147  (REWRITE_TAC[REAL_ARITH `a <= a * b <=> &0 <= a * (b - &1)`]);
1148  (MATCH_MP_TAC REAL_LE_MUL);
1149  (ASM_SIMP_TAC[REAL_LE_MUL; REAL_LE_POW_2; REAL_ARITH `&0 <= &2`]);
1150  (REWRITE_TAC[REAL_ARITH `&0 <= a - b <=> b <= a`]);
1151  (REWRITE_WITH `&1 <= norm (s2 - u1) / sqrt (&2) <=>
1152                  &1 * sqrt (&2) <= norm (s2 - u1:real^3)`);
1153  (MATCH_MP_TAC REAL_LE_RDIV_EQ);
1154  (MATCH_MP_TAC SQRT_POS_LT THEN REAL_ARITH_TAC);
1155  (ASM_REAL_ARITH_TAC);
1156  (NEW_GOAL `norm (s2 - u1) * norm (u0 - u1:real^3) * a <=
1157              norm (z - u1) * norm (u0 - u1) * a`);
1158  (REWRITE_TAC[REAL_ARITH `a * x * y <= b * x * y <=>
1159                            &0 <= (x * y) * (b - a)`]);
1160  (MATCH_MP_TAC REAL_LE_MUL);
1161  (STRIP_TAC);
1162  (MATCH_MP_TAC REAL_LE_MUL);
1163  (REWRITE_TAC[NORM_POS_LE]);
1164  (EXPAND_TAC "a" THEN MATCH_MP_TAC REAL_LE_DIV);
1165  (REWRITE_WITH `hl vl = dist (circumcenter (set_of_list vl),(HD vl):real^3)`);
1166  (MATCH_MP_TAC Rogers.HL_EQ_DIST0);
1167  (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `1` THEN ASM_REWRITE_TAC[]);
1168  (EXPAND_TAC "vl");
1169  (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
1170  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
1171  (REWRITE_TAC[DIST_POS_LE]);
1172  (SIMP_TAC[SQRT_POS_LE; REAL_ARITH `&0 <= &2`]);
1173  (ASM_REAL_ARITH_TAC);
1174  (ASM_REAL_ARITH_TAC);
1175
1176 (* ------------------------------------------------------------------------- *)
1177 (* OK here too *)
1178
1179 (* ----------------------------------------------------- *)
1180
1181  (NEW_GOAL `?s. between s (omega_list_n V ul 2,omega_list_n V ul 3) /\
1182                   dist (u0,s) = sqrt (&2) /\
1183                   mxi V ul = s`);
1184  (MATCH_MP_TAC MXI_EXPLICIT);
1185  (EXISTS_TAC `u1:real^3` THEN EXISTS_TAC `u2:real^3` THEN EXISTS_TAC `u3:real^3`);
1186  (REWRITE_TAC[REAL_ARITH `a < b <=> ~(a >= b)`]);
1187  (ASM_REWRITE_TAC[]);
1188  (FIRST_X_ASSUM CHOOSE_TAC);
1189  (UP_ASM_TAC THEN ONCE_ASM_REWRITE_TAC[] THEN STRIP_TAC);
1190
1191  (NEW_GOAL `u0 - u1 = &2 % (u0 - s1:real^3)`);
1192  (REWRITE_TAC[ASSUME `s1 = circumcenter {u0, u1:real^3}`; CIRCUMCENTER_2;
1193   midpoint; VECTOR_ARITH `u0 - inv (&2) % (u0 + u1) = inv (&2) % (u0 - u1)`]);
1194  (VECTOR_ARITH_TAC);
1195
1196  (NEW_GOAL `(z - s1) dot (u0 - s1:real^3) = &0`);
1197  (ASM_REWRITE_TAC[]);
1198  (REWRITE_WITH `{u0,u1:real^3} = set_of_list vl`);
1199  (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_1;
1200    ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
1201  (MATCH_MP_TAC Rogers.MHFTTZN4);
1202  (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `1`);
1203  (REPEAT STRIP_TAC);
1204  (ASM_REWRITE_TAC[]);
1205  (EXPAND_TAC "vl" THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
1206  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
1207  (MATCH_MP_TAC (SET_RULE `(?C. a IN C/\ C SUBSET B) ==> a IN B`));
1208  (EXISTS_TAC `voronoi_list V vl`);
1209  (ASM_REWRITE_TAC[SET_SUBSET_AFFINE_HULL]);
1210  (MATCH_MP_TAC (SET_RULE `(?C. a IN C/\ C SUBSET B) ==> a IN B`));
1211  (EXISTS_TAC `set_of_list (vl:(real^3)list)`);
1212  (ASM_REWRITE_TAC[SET_SUBSET_AFFINE_HULL]);
1213  (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_1;
1214    ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
1215  (SET_TAC[]);
1216
1217  (NEW_GOAL `between m (s2, z:real^3)`);
1218  (MATCH_MP_TAC BETWEEN_TRANS_2);
1219  (EXISTS_TAC `s3:real^3`);
1220  (STRIP_TAC);
1221  (ONCE_REWRITE_TAC[BETWEEN_SYM]);
1222  (ASM_REWRITE_TAC[]);
1223  (ASM_REWRITE_TAC[]);
1224  (ABBREV_TAC `zl:(real^3)list = truncate_simplex 2 ul`);
1225
1226  (NEW_GOAL `s2:real^3 IN voronoi_list V zl`);
1227  (EXPAND_TAC "s2" THEN EXPAND_TAC "zl");
1228  (MATCH_MP_TAC Rogers.OMEGA_LIST_N_IN_VORONOI_LIST_GEN);
1229  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
1230
1231  (NEW_GOAL `s3:real^3 IN voronoi_list V zl`);
1232  (EXPAND_TAC "s3" THEN EXPAND_TAC "zl");
1233  (MATCH_MP_TAC Rogers.OMEGA_LIST_N_IN_VORONOI_LIST_GEN);
1234  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
1235
1236  (NEW_GOAL `m:real^3 IN voronoi_list V zl`);
1237  (MATCH_MP_TAC (SET_RULE `(?C. x IN C /\ C SUBSET B) ==> x IN B`));
1238  (EXISTS_TAC `convex hull {s2, s3:real^3}`);
1239  (STRIP_TAC);
1240  (ASM_REWRITE_TAC[GSYM BETWEEN_IN_CONVEX_HULL]);
1241  (REWRITE_WITH `convex hull {s2, s3:real^3} SUBSET voronoi_list V zl <=>
1242    convex hull {s2, s3} SUBSET (convex hull (voronoi_list V zl))`);
1243  (REWRITE_WITH `convex hull (voronoi_list V zl) = voronoi_list V zl`);
1244  (REWRITE_TAC[CONVEX_HULL_EQ]);
1245  (REWRITE_TAC[Packing3.CONVEX_VORONOI_LIST]);
1246  (MATCH_MP_TAC Marchal_cells.CONVEX_HULL_SUBSET);
1247  (ASM_SET_TAC[]);
1248
1249  (NEW_GOAL `z:real^3 IN voronoi_list V zl`);
1250  (MATCH_MP_TAC (SET_RULE `(?C. x IN C /\ C SUBSET B) ==> x IN B`));
1251  (EXISTS_TAC `convex hull {m, s3:real^3}`);
1252  (STRIP_TAC);
1253  (ASM_REWRITE_TAC[GSYM BETWEEN_IN_CONVEX_HULL]);
1254  (REWRITE_WITH `convex hull {m, s3:real^3} SUBSET voronoi_list V zl <=>
1255    convex hull {m, s3} SUBSET (convex hull (voronoi_list V zl))`);
1256  (REWRITE_WITH `convex hull (voronoi_list V zl) = voronoi_list V zl`);
1257  (REWRITE_TAC[CONVEX_HULL_EQ]);
1258  (REWRITE_TAC[Packing3.CONVEX_VORONOI_LIST]);
1259  (MATCH_MP_TAC Marchal_cells.CONVEX_HULL_SUBSET);
1260  (ASM_SET_TAC[]);
1261
1262  (NEW_GOAL `norm (m - u1) <= norm (z - u1:real^3)`);
1263  (REWRITE_WITH `norm (m - u1) <= norm (z - u1:real^3) <=>
1264                  norm (m - u1) pow 2 <= norm (z - u1:real^3) pow 2`);
1265  (ASM_SIMP_TAC[Collect_geom.POW2_COND; NORM_POS_LE]);
1266  (REWRITE_WITH `m - u1 = (m - s2) + (s2 - u1:real^3) /\
1267                  z - u1 = (z - s2) + (s2 - u1:real^3)`);
1268  (VECTOR_ARITH_TAC);
1269  (REWRITE_WITH `norm (m - s2 + s2 - u1) pow 2 =
1270    norm (m - s2) pow 2 + norm (s2 - u1:real^3) pow 2`);
1271  (NEW_GOAL `(m - s2) dot (s2 - u1:real^3) = &0`);
1272  (ONCE_REWRITE_TAC[VECTOR_ARITH
1273    `(m - s2) dot (s2 - u1) = -- ((m - s2) dot (u1 - s2))`]);
1274  (REWRITE_TAC[REAL_ARITH `--a = &0 <=> a = &0`]);
1275  (REWRITE_WITH `s2:real^3 = circumcenter (set_of_list zl)`);
1276  (REWRITE_WITH `s2:real^3 = omega_list V zl`);
1277  (EXPAND_TAC "s2");
1278  (EXPAND_TAC "zl");
1279  (REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`; TRUNCATE_SIMPLEX_EXPLICIT_2;     LENGTH; ARITH_RULE `(SUC (SUC (SUC 0)) - 1) = 2`;
1280    Marchal_cells.OMEGA_LIST_TRUNCATE_2]);
1281  (MATCH_MP_TAC Rogers.XNHPWAB1);
1282  (EXISTS_TAC `2`);
1283  (REWRITE_TAC[IN; REAL_ARITH `a < b <=> ~(a >= b)`]);
1284  (ASM_REWRITE_TAC[]);
1285  (EXPAND_TAC "zl" THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
1286  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
1287  (MATCH_MP_TAC Rogers.MHFTTZN4);
1288  (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `2`);
1289  (REPEAT STRIP_TAC);
1290  (ASM_REWRITE_TAC[]);
1291  (EXPAND_TAC "zl" THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
1292  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
1293  (MATCH_MP_TAC (SET_RULE `(?C. a IN C/\ C SUBSET B) ==> a IN B`));
1294  (EXISTS_TAC `voronoi_list V zl`);
1295  (ASM_REWRITE_TAC[SET_SUBSET_AFFINE_HULL]);
1296  (MATCH_MP_TAC (SET_RULE `(?C. a IN C/\ C SUBSET B) ==> a IN B`));
1297  (EXISTS_TAC `set_of_list (zl:(real^3)list)`);
1298  (ASM_REWRITE_TAC[SET_SUBSET_AFFINE_HULL]);
1299  (EXPAND_TAC "zl" THEN REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_2;
1300    ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
1301  (SET_TAC[]);
1302  (ASM_SIMP_TAC[Trigonometry2.PITHAGO_THEOREM]);
1303
1304  (REWRITE_WITH
1305   `norm (z - s2 + s2 - u1) pow 2 =
1306    norm (z - s2) pow 2 + norm (s2 - u1:real^3) pow 2`);
1307  (NEW_GOAL `(z - s2) dot (s2 - u1:real^3) = &0`);
1308  (ONCE_REWRITE_TAC[VECTOR_ARITH
1309    `(z - s2) dot (s2 - u1) = -- ((z - s2) dot (u1 - s2))`]);
1310  (REWRITE_TAC[REAL_ARITH `--a = &0 <=> a = &0`]);
1311  (REWRITE_WITH `s2:real^3 = circumcenter (set_of_list zl)`);
1312  (REWRITE_WITH `s2:real^3 = omega_list V zl`);
1313  (EXPAND_TAC "s2");
1314  (EXPAND_TAC "zl");
1315  (REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`; TRUNCATE_SIMPLEX_EXPLICIT_2;     LENGTH; ARITH_RULE `(SUC (SUC (SUC 0)) - 1) = 2`;
1316    Marchal_cells.OMEGA_LIST_TRUNCATE_2]);
1317  (MATCH_MP_TAC Rogers.XNHPWAB1);
1318  (EXISTS_TAC `2`);
1319  (REWRITE_TAC[IN; REAL_ARITH `a < b <=> ~(a >= b)`]);
1320  (ASM_REWRITE_TAC[]);
1321  (EXPAND_TAC "zl" THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
1322  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
1323  (MATCH_MP_TAC Rogers.MHFTTZN4);
1324  (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `2`);
1325  (REPEAT STRIP_TAC);
1326  (ASM_REWRITE_TAC[]);
1327  (EXPAND_TAC "zl" THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
1328  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
1329  (MATCH_MP_TAC (SET_RULE `(?C. a IN C/\ C SUBSET B) ==> a IN B`));
1330  (EXISTS_TAC `voronoi_list V zl`);
1331  (ASM_REWRITE_TAC[SET_SUBSET_AFFINE_HULL]);
1332  (MATCH_MP_TAC (SET_RULE `(?C. a IN C/\ C SUBSET B) ==> a IN B`));
1333  (EXISTS_TAC `set_of_list (zl:(real^3)list)`);
1334  (ASM_REWRITE_TAC[SET_SUBSET_AFFINE_HULL]);
1335  (EXPAND_TAC "zl" THEN REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_2;
1336    ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
1337  (SET_TAC[]);
1338  (ASM_SIMP_TAC[Trigonometry2.PITHAGO_THEOREM]);
1339  (REWRITE_TAC[REAL_ARITH `a + b <= c + b <=> a <= c`]);
1340
1341  (MP_TAC (ASSUME `between m (s2,z:real^3)`));
1342  (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL; CONVEX_HULL_2;IN;IN_ELIM_THM] THEN STRIP_TAC);
1343  (REWRITE_TAC[ASSUME `m = u % s2 + v % z:real^3`]);
1344  (REWRITE_WITH
1345   `(u % s2 + v % z) - s2 = (u % s2 + v % z) - (u + v) % s2:real^3`);
1346  (ASM_REWRITE_TAC[VECTOR_MUL_LID]);
1347  (REWRITE_TAC[VECTOR_ARITH `(u % s2 + v % z) - (u + v) % s2 = v % (z - s2)`]);
1348  (REWRITE_TAC[NORM_MUL; REAL_ARITH `(a*b) pow 2 = a pow 2 * b pow 2`;
1349    REAL_ARITH `a * b <= b <=> &0 <= b * (&1 - a)`]);
1350  (MATCH_MP_TAC REAL_LE_MUL);
1351  (REWRITE_TAC[REAL_LE_POW_2]);
1352  (REWRITE_WITH `abs (v:real) = v`);
1353  (ASM_REWRITE_TAC[REAL_ABS_REFL]);
1354  (REWRITE_TAC[REAL_ARITH `&0 <= &1 - a <=> a <= &1 pow 2`]);
1355  (REWRITE_WITH ` v pow 2 <= &1 pow 2 <=> v <= &1`);
1356  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
1357  (MATCH_MP_TAC Collect_geom.POW2_COND);
1358  (ASM_REAL_ARITH_TAC);
1359  (ASM_REAL_ARITH_TAC);
1360
1361  (NEW_GOAL `norm (m - u1:real^3) = dist (u0, s:real^3)`);
1362  (ONCE_REWRITE_TAC[DIST_SYM]);
1363  (ASM_REWRITE_TAC[GSYM dist]);
1364  (UNDISCH_TAC `m IN voronoi_list V zl`);
1365  (ASM_REWRITE_TAC[VORONOI_LIST; VORONOI_SET]);
1366  (EXPAND_TAC "zl");
1367  (REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`; TRUNCATE_SIMPLEX_EXPLICIT_2;     set_of_list]);
1368  (STRIP_TAC);
1369  (NEW_GOAL `s:real^3 IN voronoi_closed V u0 /\ s IN voronoi_closed V u1`);
1370  (UP_ASM_TAC THEN SET_TAC[]);
1371  (UP_ASM_TAC THEN REWRITE_TAC[voronoi_closed; IN; IN_ELIM_THM]);
1372  (REPEAT STRIP_TAC);
1373  (NEW_GOAL `{u0,u1,u2,u3:real^3} SUBSET V`);
1374  (REWRITE_WITH `{u0,u1,u2,u3:real^3} = set_of_list ul`);
1375  (ASM_REWRITE_TAC[set_of_list]);
1376  (MATCH_MP_TAC Packing3.BARV_SUBSET);
1377  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]);
1378
1379
1380  (NEW_GOAL `dist (s,u0) <= dist (s,u1:real^3)`);
1381  (FIRST_ASSUM MATCH_MP_TAC);
1382  (ONCE_REWRITE_TAC[MESON[IN] `V s <=> s IN V`]);
1383  (ASM_SET_TAC[]);
1384  (NEW_GOAL `dist (s,u1) <= dist (s,u0:real^3)`);
1385  (FIRST_ASSUM MATCH_MP_TAC);
1386  (ONCE_REWRITE_TAC[MESON[IN] `V s <=> s IN V`]);
1387  (ASM_SET_TAC[]);
1388  (ASM_REAL_ARITH_TAC);
1389
1390  (NEW_GOAL `norm (m - u1:real^3) = sqrt (&2)`);
1391  (ASM_REAL_ARITH_TAC);
1392
1393  (REWRITE_WITH `(z - u1) dot (u0 - u1:real^3) = &2 *  norm (u0 - s1) pow 2`);
1394  (REWRITE_WITH `(z - u1) dot (u0 - u1) = (z - s1) dot (u0 - u1) +
1395                  (s1 - u1) dot (u0 - u1:real^3)`);
1396  (VECTOR_ARITH_TAC);
1397  (REWRITE_TAC[ASSUME `u0 - u1 = &2 % (u0 - s1:real^3)`; DOT_RMUL]);
1398  (REWRITE_WITH `(s1 - u1) = (u0 - s1:real^3)`);
1399  (ASM_REWRITE_TAC[CIRCUMCENTER_2;midpoint] THEN VECTOR_ARITH_TAC);
1400  (ASM_REWRITE_TAC[NORM_POW_2] THEN REAL_ARITH_TAC);
1401
1402  (NEW_GOAL `&2 * norm (u0 - s1:real^3) pow 2 <=
1403              norm (m - u1) * norm (u0 - u1) * a`);
1404  (EXPAND_TAC "a");
1405  (REWRITE_WITH `hl (vl:(real^3)list) = dist (s1, u0:real^3)`);
1406  (REWRITE_WITH `s1:real^3 = circumcenter (set_of_list vl)`);
1407  (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`;
1408    TRUNCATE_SIMPLEX_EXPLICIT_1; set_of_list]);
1409  (ASM_REWRITE_TAC[]);
1410
1411  (REWRITE_WITH `u0:real^3 = HD vl`);
1412  (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`;
1413    TRUNCATE_SIMPLEX_EXPLICIT_1; set_of_list; HD]);
1414  (MATCH_MP_TAC Rogers.HL_EQ_DIST0);
1415  (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `1` THEN ASM_REWRITE_TAC[]);
1416  (EXPAND_TAC "vl");
1417  (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
1418  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
1419  (ONCE_REWRITE_TAC[DIST_SYM] THEN REWRITE_TAC[dist]);
1420  (REWRITE_TAC[ASSUME `u0 - u1 = &2 % (u0 - s1:real^3)`; NORM_MUL]);
1421  (REWRITE_WITH `abs (&2) = &2`);
1422  (REWRITE_TAC[REAL_ABS_REFL; REAL_ARITH `&0 <= &2`]);
1423  (REWRITE_TAC[REAL_ARITH `a * (&2 * b) * b / c = (&2 * b pow 2) * ( a / c)`]);
1424  (REWRITE_TAC[REAL_ARITH `a <= a * b <=> &0 <= a * (b - &1)`]);
1425  (MATCH_MP_TAC REAL_LE_MUL);
1426  (ASM_SIMP_TAC[REAL_LE_MUL; REAL_LE_POW_2; REAL_ARITH `&0 <= &2`]);
1427  (REWRITE_TAC[REAL_ARITH `&0 <= a - b <=> b <= a`]);
1428  (REWRITE_WITH `sqrt (&2) / sqrt (&2) = &1`);
1429  (MATCH_MP_TAC REAL_DIV_REFL);
1430  (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~(a = &0)`));
1431  (SIMP_TAC[SQRT_POS_LT; REAL_ARITH `&0 < &2`]);
1432  (REAL_ARITH_TAC);
1433
1434  (NEW_GOAL `norm (m - u1) * norm (u0 - u1:real^3) * a <=
1435              norm (z - u1) * norm (u0 - u1) * a`);
1436  (REWRITE_TAC[REAL_ARITH `a * x * y <= b * x * y <=>
1437                            &0 <= (x * y) * (b - a)`]);
1438  (MATCH_MP_TAC REAL_LE_MUL);
1439  (STRIP_TAC);
1440  (MATCH_MP_TAC REAL_LE_MUL);
1441  (REWRITE_TAC[NORM_POS_LE]);
1442  (EXPAND_TAC "a" THEN MATCH_MP_TAC REAL_LE_DIV);
1443  (REWRITE_WITH `hl vl = dist (circumcenter (set_of_list vl),(HD vl):real^3)`);
1444  (MATCH_MP_TAC Rogers.HL_EQ_DIST0);
1445  (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `1` THEN ASM_REWRITE_TAC[]);
1446  (EXPAND_TAC "vl");
1447  (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
1448  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
1449  (REWRITE_TAC[DIST_POS_LE]);
1450  (SIMP_TAC[SQRT_POS_LE; REAL_ARITH `&0 <= &2`]);
1451  (ASM_REAL_ARITH_TAC);
1452  (ASM_REAL_ARITH_TAC);
1453
1454  (NEW_GOAL `t1 * norm (u0 - u1:real^3) pow 2 + t5 * ((z - u1) dot (u0 - u1))
1455   <= t1 * norm (u0 - u1) pow 2 + t5 * (norm (z - u1) * norm (u0 - u1) * a)`);
1456  (REWRITE_TAC[REAL_ARITH `a + b * c <= a + b * d <=> &0 <= b * (d - c)`]);
1457  (MATCH_MP_TAC REAL_LE_MUL);
1458  (ASM_REAL_ARITH_TAC);
1459
1460  (NEW_GOAL
1461  `t1 * norm (u0 - u1) pow 2 + t5 * norm (z - u1:real^3) * norm (u0 - u1) * a
1462  < norm (t1 % (u0 - u1) + t5 % (z - u1)) * norm (u0 - u1) * a`);
1463
1464  (REWRITE_TAC[REAL_ARITH
1465  `t1 * norm (u0 - u1) pow 2 + t5 * norm (z - u1:real^3) * norm (u0 - u1) * a
1466   < norm (t1 % (u0 - u1) + t5 % (z - u1)) * norm (u0 - u1) * a <=>
1467   &0 < (a * norm (t1 % (u0 - u1) + t5 % (z - u1)) - t1 * norm (u0 - u1) -
1468   t5 * a * norm (z - u1)) * norm (u0 - u1)`]);
1469  (MATCH_MP_TAC REAL_LT_MUL);
1470  (REPEAT STRIP_TAC);
1471  (REWRITE_TAC[REAL_ARITH `&0 < a - b - c <=> b + c < a`]);
1472
1473  (NEW_GOAL `t1 * norm (u0 - u1) < a * t1 * norm (u0 - u1:real^3)`);
1474  (REWRITE_TAC[REAL_ARITH `a * b < c * a * b <=> &0 < (--a) * b  * (&1 - c)`]);
1475  (MATCH_MP_TAC REAL_LT_MUL);
1476  (STRIP_TAC);
1477  (ASM_REAL_ARITH_TAC);
1478  (MATCH_MP_TAC REAL_LT_MUL);
1479  (STRIP_TAC);
1480  (REWRITE_TAC[NORM_POS_LT; VECTOR_ARITH `a - b = vec 0 <=> a = b`]);
1481  (ASM_REWRITE_TAC[]);
1482  (REWRITE_TAC[REAL_ARITH `&0 < a - b <=> b < a`] THEN EXPAND_TAC "a");
1483  (REWRITE_WITH `hl (vl:(real^3)list) / sqrt (&2) < &1 <=> hl vl < &1 * sqrt (&2) `);
1484  (MATCH_MP_TAC REAL_LT_LDIV_EQ);
1485  (MATCH_MP_TAC SQRT_POS_LT);
1486  (REAL_ARITH_TAC);
1487  (ASM_REWRITE_TAC[REAL_MUL_LID]);
1488
1489  (NEW_GOAL `a * t1 * norm (u0 - u1) + t5 * a * norm (z - u1) <=
1490  a * norm (t1 % (u0 - u1) + t5 % (z - u1:real^3))`);
1491  (REWRITE_TAC[REAL_ARITH
1492   `a * t1 * norm (u0 - u1) + t5 * a * norm (z - u1) <=
1493    a * norm (t1 % (u0 - u1) + t5 % (z - u1)) <=>
1494    &0 <= a * (norm (t1 % (u0 - u1) + t5 % (z - u1)) + (--t1 * norm (u0 - u1)) -     t5 * norm (z - u1))`]);
1495  (MATCH_MP_TAC REAL_LE_MUL);
1496  (STRIP_TAC);
1497  (EXPAND_TAC "a");
1498  (REWRITE_WITH `hl (vl:(real^3)list) = dist (s1, u0:real^3)`);
1499  (REWRITE_WITH `s1:real^3 = circumcenter (set_of_list vl)`);
1500  (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`;
1501    TRUNCATE_SIMPLEX_EXPLICIT_1; set_of_list]);
1502  (ASM_REWRITE_TAC[]);
1503
1504  (REWRITE_WITH `u0:real^3 = HD vl`);
1505  (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`;
1506    TRUNCATE_SIMPLEX_EXPLICIT_1; set_of_list; HD]);
1507  (MATCH_MP_TAC Rogers.HL_EQ_DIST0);
1508  (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `1` THEN ASM_REWRITE_TAC[]);
1509  (EXPAND_TAC "vl");
1510  (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
1511  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
1512  (MATCH_MP_TAC REAL_LE_DIV);
1513  (REWRITE_TAC[DIST_POS_LE]);
1514  (ASM_SIMP_TAC[SQRT_POS_LE; REAL_ARITH `&0 <= &2`]);
1515
1516  (ONCE_REWRITE_TAC[REAL_ARITH `&0 <= a + b - c <=> c <= a + b`]);
1517  (ABBREV_TAC `k1 = t1 % (u0 - u1) + t5 % (z - u1:real^3)`);
1518  (REWRITE_WITH `t5 * norm (z - u1) = norm (t5 % (z - u1:real^3))`);
1519  (REWRITE_TAC[NORM_MUL]);
1520  (REWRITE_WITH `abs t5 = t5`);
1521  (REWRITE_TAC[REAL_ABS_REFL]);
1522  (ASM_REAL_ARITH_TAC);
1523  (REWRITE_WITH `--t1 * norm (u0 - u1) = norm ((--t1) % (u0 - u1:real^3))`);
1524  (REWRITE_TAC[NORM_MUL]);
1525  (REWRITE_WITH `abs (--t1) = --t1`);
1526  (REWRITE_TAC[REAL_ABS_REFL]);
1527  (ASM_REAL_ARITH_TAC);
1528  (REWRITE_WITH `t5 % (z - u1) = k1 + --t1 % (u0 - u1:real^3)`);
1529  (EXPAND_TAC "k1" THEN VECTOR_ARITH_TAC);
1530  (REWRITE_TAC[NORM_TRIANGLE]);
1531  (ASM_REAL_ARITH_TAC);
1532  (REWRITE_TAC[NORM_POS_LT; VECTOR_ARITH `a - b = vec 0 <=> a = b`]);
1533  (ASM_REWRITE_TAC[]);
1534  (ASM_REAL_ARITH_TAC);
1535  (ASM_MESON_TAC[]);
1536
1537 (* ----------------------------------------------------------------------- *)
1538 (* Half of the proof *)
1539
1540
1541  (ASM_CASES_TAC `t2 < &0`);
1542  (NEW_GOAL `F`);
1543  (UNDISCH_TAC `x:real^3 IN rcone_ge u0 u1 a`);
1544  (REWRITE_TAC[rcone_ge;rconesgn; IN; IN_ELIM_THM]);
1545  (REWRITE_TAC[REAL_ARITH `~(a >= b) <=> a < b`]);
1546  (NEW_GOAL `x = t1 % u0 + t2 % u1 + t5 % (z:real^3)`);
1547  (ASM_REWRITE_TAC[] THEN EXPAND_TAC "z" THEN EXPAND_TAC "t5");
1548  (REWRITE_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC]);
1549  (REWRITE_TAC[REAL_ARITH `a * b / a = b * (a / a)`]);
1550  (ASM_SIMP_TAC[REAL_DIV_REFL; REAL_ARITH `&0 < y ==> ~(y = &0)`;
1551   REAL_MUL_RID]);
1552  (REWRITE_TAC[dist]);
1553  (REWRITE_WITH `x - u0:real^3 = t2 % (u1 - u0) + t5 % (z - u0)`);
1554  (REWRITE_WITH `x - u0:real^3 = x - (t1 + t2 + t5) % u0`);
1555  (REWRITE_WITH `t1 + t2 + t5 = &1`);
1556  (ASM_REAL_ARITH_TAC);
1557  (VECTOR_ARITH_TAC);
1558  (REWRITE_TAC[ASSUME `x = t1 % u0 + t2 % u1 + t5 % z:real^3`]);
1559  (VECTOR_ARITH_TAC);
1560
1561  (REWRITE_TAC[DOT_LADD; DOT_LMUL; GSYM NORM_POW_2]);
1562  (NEW_GOAL `(z - u0) dot (u1 - u0:real^3) <=
1563              norm (z - u0:real^3) * norm (u1 - u0) * a`);
1564
1565  (ASM_CASES_TAC `hl (truncate_simplex 2 (ul:(real^3)list)) >= sqrt (&2)`);
1566  (NEW_GOAL `m = s2:real^3`);
1567  (EXPAND_TAC "m" THEN REWRITE_TAC[mxi] THEN COND_CASES_TAC);
1568  (ASM_REWRITE_TAC[]);
1569  (NEW_GOAL `F`);
1570  (ASM_MESON_TAC[]);
1571  (ASM_MESON_TAC[]);
1572
1573  (NEW_GOAL `u1 - u0 = &2 % (u1 - s1:real^3)`);
1574  (REWRITE_TAC[ASSUME `s1 = circumcenter {u0, u1:real^3}`; CIRCUMCENTER_2;
1575   midpoint; VECTOR_ARITH `u1 - inv (&2) % (u0 + u1) = inv (&2) % (u1 - u0)`]);
1576  (VECTOR_ARITH_TAC);
1577
1578  (NEW_GOAL `(z - s1) dot (u1 - s1:real^3) = &0`);
1579  (ASM_REWRITE_TAC[]);
1580  (REWRITE_WITH `{u0,u1:real^3} = set_of_list vl`);
1581  (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_1;
1582    ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
1583  (MATCH_MP_TAC Rogers.MHFTTZN4);
1584  (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `1`);
1585  (REPEAT STRIP_TAC);
1586  (ASM_REWRITE_TAC[]);
1587  (EXPAND_TAC "vl" THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
1588  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
1589  (MATCH_MP_TAC (SET_RULE `(?C. a IN C/\ C SUBSET B) ==> a IN B`));
1590  (EXISTS_TAC `voronoi_list V vl`);
1591  (ASM_REWRITE_TAC[SET_SUBSET_AFFINE_HULL]);
1592  (MATCH_MP_TAC (SET_RULE `(?C. a IN C/\ C SUBSET B) ==> a IN B`));
1593  (EXISTS_TAC `set_of_list (vl:(real^3)list)`);
1594  (ASM_REWRITE_TAC[SET_SUBSET_AFFINE_HULL]);
1595  (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_1;
1596    ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
1597  (SET_TAC[]);
1598
1599  (NEW_GOAL `norm (s2 - u0) <= norm (z - u0:real^3)`);
1600  (REWRITE_WITH `norm (s2 - u0) <= norm (z - u0:real^3) <=>
1601                  norm (s2 - u0) pow 2 <= norm (z - u0:real^3) pow 2`);
1602  (ASM_SIMP_TAC[Collect_geom.POW2_COND; NORM_POS_LE]);
1603  (REWRITE_WITH `s2 - u0 = (s2 - s1) + (s1 - u0:real^3) /\
1604                   z - u0 = (z - s1) + (s1 - u0:real^3)`);
1605  (VECTOR_ARITH_TAC);
1606  (REWRITE_WITH `norm (s2 - s1 + s1 - u0) pow 2 =
1607    norm (s2 - s1) pow 2 + norm (s1 - u0:real^3) pow 2`);
1608  (NEW_GOAL `(s2 - s1) dot (s1 - u0:real^3) = &0`);
1609  (REWRITE_WITH `s1 - u0 = u1 - s1:real^3`);
1610  (ASM_REWRITE_TAC[CIRCUMCENTER_2; midpoint] THEN VECTOR_ARITH_TAC);
1611  (ASM_REWRITE_TAC[]);
1612  (REWRITE_WITH `{u0,u1:real^3} = set_of_list vl`);
1613  (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_1;
1614    ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
1615  (MATCH_MP_TAC Rogers.MHFTTZN4);
1616  (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `1`);
1617  (REPEAT STRIP_TAC);
1618  (ASM_REWRITE_TAC[]);
1619  (EXPAND_TAC "vl" THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
1620  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
1621  (MATCH_MP_TAC (SET_RULE `(?C. a IN C/\ C SUBSET B) ==> a IN B`));
1622  (EXISTS_TAC `voronoi_list V vl`);
1623  (ASM_REWRITE_TAC[SET_SUBSET_AFFINE_HULL]);
1624  (MATCH_MP_TAC (SET_RULE `(?C. a IN C/\ C SUBSET B) ==> a IN B`));
1625  (EXISTS_TAC `set_of_list (vl:(real^3)list)`);
1626  (ASM_REWRITE_TAC[SET_SUBSET_AFFINE_HULL]);
1627  (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_1;
1628    ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
1629  (SET_TAC[]);
1630  (ASM_SIMP_TAC[Trigonometry2.PITHAGO_THEOREM]);
1631
1632  (REWRITE_WITH `norm (z - s1 + s1 - u0:real^3) pow 2 =
1633                  norm (z - s1) pow 2 + norm (s1 - u0) pow 2`);
1634  (NEW_GOAL `(z - s1) dot (s1 - u0:real^3) = &0`);
1635  (REWRITE_WITH `s1 - u0 = u1 - s1:real^3`);
1636  (ASM_REWRITE_TAC[CIRCUMCENTER_2; midpoint] THEN VECTOR_ARITH_TAC);
1637  (ASM_REWRITE_TAC[]);
1638  (ASM_SIMP_TAC[Trigonometry2.PITHAGO_THEOREM]);
1639  (REWRITE_TAC[REAL_ARITH `a + b <= c + b <=> a <= c`]);
1640  (REWRITE_TAC[GSYM (ASSUME `omega_list_n V ul 2 = s2`)] THEN
1641    REWRITE_TAC[OMEGA_LIST_N; ARITH_RULE `2 = SUC 1`]);
1642  (REWRITE_TAC[ARITH_RULE `SUC 1 = 2`]);
1643  (REWRITE_TAC[GSYM dist; DIST_SYM]);
1644  (ASM_REWRITE_TAC[]);
1645  (REWRITE_WITH `!a b c d:real^3.
1646    dist (a, b:real^3) pow 2 <= dist (c,d) pow 2 <=> dist (a,b) <= dist (c,d)`);
1647  (REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[EQ_SYM_EQ]);
1648  (SIMP_TAC[Collect_geom.POW2_COND; DIST_POS_LE]);
1649  (MATCH_MP_TAC CLOSEST_POINT_LE);
1650  (REWRITE_TAC[Packing3.CLOSED_VORONOI_LIST]);
1651  (REWRITE_TAC[GSYM (ASSUME `ul = [u0;u1;u2;u3:real^3]`)]);
1652  (ABBREV_TAC `zl:(real^3)list = truncate_simplex 2 ul`);
1653
1654  (NEW_GOAL `s2:real^3 IN voronoi_list V zl`);
1655  (EXPAND_TAC "zl" THEN REWRITE_TAC[GSYM (ASSUME `omega_list_n V ul 2 = s2`)]);
1656  (MATCH_MP_TAC Rogers.OMEGA_LIST_N_IN_VORONOI_LIST_GEN);
1657  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
1658  (NEW_GOAL `s3:real^3 IN voronoi_list V zl`);
1659  (EXPAND_TAC "zl" THEN EXPAND_TAC "s3");
1660  (MATCH_MP_TAC Rogers.OMEGA_LIST_N_IN_VORONOI_LIST_GEN);
1661  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
1662  (MATCH_MP_TAC (SET_RULE `(?C. x IN C /\ C SUBSET B) ==> x IN B`));
1663  (EXISTS_TAC `convex hull {s2, s3:real^3}`);
1664  (STRIP_TAC);
1665  (ASM_REWRITE_TAC[GSYM BETWEEN_IN_CONVEX_HULL]);
1666  (ASM_MESON_TAC[]);
1667  (REWRITE_WITH `convex hull {s2, s3:real^3} SUBSET voronoi_list V zl <=>
1668    convex hull {s2, s3} SUBSET (convex hull (voronoi_list V zl))`);
1669  (REWRITE_WITH `convex hull (voronoi_list V zl) = voronoi_list V zl`);
1670  (REWRITE_TAC[CONVEX_HULL_EQ]);
1671  (REWRITE_TAC[Packing3.CONVEX_VORONOI_LIST]);
1672  (MATCH_MP_TAC Marchal_cells.CONVEX_HULL_SUBSET);
1673  (ASM_SET_TAC[]);
1674
1675  (REWRITE_WITH `(z - u0) dot (u1 - u0:real^3) = &2 *  norm (u1 - s1) pow 2`);
1676  (REWRITE_WITH `(z - u0) dot (u1 - u0) = (z - s1) dot (u1 - u0) +
1677                  (s1 - u0) dot (u1 - u0:real^3)`);
1678  (VECTOR_ARITH_TAC);
1679  (REWRITE_TAC[ASSUME `u1 - u0 = &2 % (u1 - s1:real^3)`; DOT_RMUL]);
1680  (REWRITE_WITH `(s1 - u0) = (u1 - s1:real^3)`);
1681  (ASM_REWRITE_TAC[CIRCUMCENTER_2;midpoint] THEN VECTOR_ARITH_TAC);
1682  (ASM_REWRITE_TAC[NORM_POW_2] THEN REAL_ARITH_TAC);
1683
1684
1685  (NEW_GOAL `&2 * norm (u1 - s1:real^3) pow 2 <=
1686              norm (s2 - u0) * norm (u1 - u0) * a`);
1687  (NEW_GOAL `norm (s2 - u0:real^3) >= sqrt (&2)`);
1688  (NEW_GOAL `norm (s2 - u0:real^3) >=
1689              hl (truncate_simplex 2 (ul:(real^3)list))`);
1690  (REWRITE_TAC[GSYM dist]);
1691  (ONCE_REWRITE_TAC[REAL_ARITH `a >= b <=> b <= a`]);
1692  (ABBREV_TAC `xl:(real^3)list = truncate_simplex 2 ul`);
1693
1694  (REWRITE_WITH `s2 = omega_list V xl`);
1695  (ONCE_REWRITE_TAC[GSYM (ASSUME `omega_list_n V ul 2 = s2`)]);
1696  (REWRITE_TAC[Marchal_cells.OMEGA_LIST_TRUNCATE_2;
1697    ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
1698  (EXPAND_TAC "xl" THEN REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2;
1699    ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
1700  (REWRITE_WITH `u0:real^3 = HD xl`);
1701  (EXPAND_TAC "xl");
1702  (REWRITE_TAC[ASSUME `ul = [u0; u1; u2; u3:real^3]`;
1703    TRUNCATE_SIMPLEX_EXPLICIT_2; HD]);
1704  (MATCH_MP_TAC Rogers.WAUFCHE1);
1705  (EXISTS_TAC `2`);
1706  (REWRITE_TAC[IN] THEN EXPAND_TAC "xl");
1707  (STRIP_TAC);
1708  (ASM_REWRITE_TAC[]);
1709  (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
1710  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
1711  (ASM_REAL_ARITH_TAC);
1712
1713  (EXPAND_TAC "a");
1714  (REWRITE_WITH `hl (vl:(real^3)list) = dist (s1, u1:real^3)`);
1715  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
1716  (REWRITE_WITH `s1:real^3 = circumcenter (set_of_list vl)`);
1717  (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`;
1718    TRUNCATE_SIMPLEX_EXPLICIT_1; set_of_list]);
1719  (ASM_REWRITE_TAC[]);
1720  (NEW_GOAL `!w:real^3. w IN set_of_list vl
1721                   ==> dist (circumcenter (set_of_list vl),w) = hl vl`);
1722  (MATCH_MP_TAC Rogers.HL_PROPERTIES);
1723  (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `1`);
1724  (ASM_REWRITE_TAC[] THEN EXPAND_TAC "vl");
1725  (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
1726  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
1727  (FIRST_ASSUM MATCH_MP_TAC);
1728  (EXPAND_TAC "vl");
1729  (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`;
1730    TRUNCATE_SIMPLEX_EXPLICIT_1; set_of_list]);
1731  (SET_TAC[]);
1732
1733  (ONCE_REWRITE_TAC[DIST_SYM] THEN REWRITE_TAC[dist]);
1734  (REWRITE_TAC[ASSUME `u1 - u0 = &2 % (u1 - s1:real^3)`; NORM_MUL]);
1735  (REWRITE_WITH `abs (&2) = &2`);
1736  (REWRITE_TAC[REAL_ABS_REFL; REAL_ARITH `&0 <= &2`]);
1737  (REWRITE_TAC[REAL_ARITH `a * (&2 * b) * b / c = (&2 * b pow 2) * ( a / c)`]);
1738  (REWRITE_TAC[REAL_ARITH `a <= a * b <=> &0 <= a * (b - &1)`]);
1739  (MATCH_MP_TAC REAL_LE_MUL);
1740  (ASM_SIMP_TAC[REAL_LE_MUL; REAL_LE_POW_2; REAL_ARITH `&0 <= &2`]);
1741  (REWRITE_TAC[REAL_ARITH `&0 <= a - b <=> b <= a`]);
1742  (REWRITE_WITH `&1 <= norm (s2 - u0) / sqrt (&2) <=>
1743                  &1 * sqrt (&2) <= norm (s2 - u0:real^3)`);
1744  (MATCH_MP_TAC REAL_LE_RDIV_EQ);
1745  (MATCH_MP_TAC SQRT_POS_LT THEN REAL_ARITH_TAC);
1746  (ASM_REAL_ARITH_TAC);
1747  (NEW_GOAL `norm (s2 - u0) * norm (u1 - u0:real^3) * a <=
1748              norm (z - u0) * norm (u1 - u0) * a`);
1749  (REWRITE_TAC[REAL_ARITH `a * x * y <= b * x * y <=>
1750                            &0 <= (x * y) * (b - a)`]);
1751  (MATCH_MP_TAC REAL_LE_MUL);
1752  (STRIP_TAC);
1753  (MATCH_MP_TAC REAL_LE_MUL);
1754  (REWRITE_TAC[NORM_POS_LE]);
1755  (EXPAND_TAC "a" THEN MATCH_MP_TAC REAL_LE_DIV);
1756  (REWRITE_WITH `hl vl = dist (circumcenter (set_of_list vl),(HD vl):real^3)`);
1757  (MATCH_MP_TAC Rogers.HL_EQ_DIST0);
1758  (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `1` THEN ASM_REWRITE_TAC[]);
1759  (EXPAND_TAC "vl");
1760  (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
1761  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
1762  (REWRITE_TAC[DIST_POS_LE]);
1763  (SIMP_TAC[SQRT_POS_LE; REAL_ARITH `&0 <= &2`]);
1764  (ASM_REAL_ARITH_TAC);
1765  (ASM_REAL_ARITH_TAC);
1766
1767 (* ------------------------------------------------------------------------- *)
1768 (* OK here too *)
1769
1770 (* ----------------------------------------------------- *)
1771
1772  (NEW_GOAL `?s. between s (omega_list_n V ul 2,omega_list_n V ul 3) /\
1773                   dist (u0,s) = sqrt (&2) /\
1774                   mxi V ul = s`);
1775  (MATCH_MP_TAC MXI_EXPLICIT);
1776  (EXISTS_TAC `u1:real^3` THEN EXISTS_TAC `u2:real^3` THEN EXISTS_TAC `u3:real^3`);
1777  (REWRITE_TAC[REAL_ARITH `a < b <=> ~(a >= b)`]);
1778  (ASM_REWRITE_TAC[]);
1779  (FIRST_X_ASSUM CHOOSE_TAC);
1780  (UP_ASM_TAC THEN ONCE_ASM_REWRITE_TAC[] THEN STRIP_TAC);
1781
1782  (NEW_GOAL `u1 - u0 = &2 % (u1 - s1:real^3)`);
1783  (REWRITE_TAC[ASSUME `s1 = circumcenter {u0, u1:real^3}`; CIRCUMCENTER_2;
1784   midpoint; VECTOR_ARITH `u1 - inv (&2) % (u0 + u1) = inv (&2) % (u1 - u0)`]);
1785  (VECTOR_ARITH_TAC);
1786
1787  (NEW_GOAL `(z - s1) dot (u1 - s1:real^3) = &0`);
1788  (ASM_REWRITE_TAC[]);
1789  (REWRITE_WITH `{u0,u1:real^3} = set_of_list vl`);
1790  (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_1;
1791    ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
1792  (MATCH_MP_TAC Rogers.MHFTTZN4);
1793  (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `1`);
1794  (REPEAT STRIP_TAC);
1795  (ASM_REWRITE_TAC[]);
1796  (EXPAND_TAC "vl" THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
1797  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
1798  (MATCH_MP_TAC (SET_RULE `(?C. a IN C/\ C SUBSET B) ==> a IN B`));
1799  (EXISTS_TAC `voronoi_list V vl`);
1800  (ASM_REWRITE_TAC[SET_SUBSET_AFFINE_HULL]);
1801  (MATCH_MP_TAC (SET_RULE `(?C. a IN C/\ C SUBSET B) ==> a IN B`));
1802  (EXISTS_TAC `set_of_list (vl:(real^3)list)`);
1803  (ASM_REWRITE_TAC[SET_SUBSET_AFFINE_HULL]);
1804  (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_1;
1805    ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
1806  (SET_TAC[]);
1807
1808  (NEW_GOAL `between m (s2, z:real^3)`);
1809  (MATCH_MP_TAC BETWEEN_TRANS_2);
1810  (EXISTS_TAC `s3:real^3`);
1811  (STRIP_TAC);
1812  (ONCE_REWRITE_TAC[BETWEEN_SYM]);
1813  (ASM_REWRITE_TAC[]);
1814  (ASM_REWRITE_TAC[]);
1815  (ABBREV_TAC `zl:(real^3)list = truncate_simplex 2 ul`);
1816
1817  (NEW_GOAL `s2:real^3 IN voronoi_list V zl`);
1818  (EXPAND_TAC "s2" THEN EXPAND_TAC "zl");
1819  (MATCH_MP_TAC Rogers.OMEGA_LIST_N_IN_VORONOI_LIST_GEN);
1820  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
1821
1822  (NEW_GOAL `s3:real^3 IN voronoi_list V zl`);
1823  (EXPAND_TAC "s3" THEN EXPAND_TAC "zl");
1824  (MATCH_MP_TAC Rogers.OMEGA_LIST_N_IN_VORONOI_LIST_GEN);
1825  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
1826
1827  (NEW_GOAL `m:real^3 IN voronoi_list V zl`);
1828  (MATCH_MP_TAC (SET_RULE `(?C. x IN C /\ C SUBSET B) ==> x IN B`));
1829  (EXISTS_TAC `convex hull {s2, s3:real^3}`);
1830  (STRIP_TAC);
1831  (ASM_REWRITE_TAC[GSYM BETWEEN_IN_CONVEX_HULL]);
1832  (REWRITE_WITH `convex hull {s2, s3:real^3} SUBSET voronoi_list V zl <=>
1833    convex hull {s2, s3} SUBSET (convex hull (voronoi_list V zl))`);
1834  (REWRITE_WITH `convex hull (voronoi_list V zl) = voronoi_list V zl`);
1835  (REWRITE_TAC[CONVEX_HULL_EQ]);
1836  (REWRITE_TAC[Packing3.CONVEX_VORONOI_LIST]);
1837  (MATCH_MP_TAC Marchal_cells.CONVEX_HULL_SUBSET);
1838  (ASM_SET_TAC[]);
1839
1840  (NEW_GOAL `z:real^3 IN voronoi_list V zl`);
1841  (MATCH_MP_TAC (SET_RULE `(?C. x IN C /\ C SUBSET B) ==> x IN B`));
1842  (EXISTS_TAC `convex hull {m, s3:real^3}`);
1843  (STRIP_TAC);
1844  (ASM_REWRITE_TAC[GSYM BETWEEN_IN_CONVEX_HULL]);
1845  (REWRITE_WITH `convex hull {m, s3:real^3} SUBSET voronoi_list V zl <=>
1846    convex hull {m, s3} SUBSET (convex hull (voronoi_list V zl))`);
1847  (REWRITE_WITH `convex hull (voronoi_list V zl) = voronoi_list V zl`);
1848  (REWRITE_TAC[CONVEX_HULL_EQ]);
1849  (REWRITE_TAC[Packing3.CONVEX_VORONOI_LIST]);
1850  (MATCH_MP_TAC Marchal_cells.CONVEX_HULL_SUBSET);
1851  (ASM_SET_TAC[]);
1852
1853  (NEW_GOAL `norm (m - u0) <= norm (z - u0:real^3)`);
1854  (REWRITE_WITH `norm (m - u0) <= norm (z - u0:real^3) <=>
1855                  norm (m - u0) pow 2 <= norm (z - u0:real^3) pow 2`);
1856  (ASM_SIMP_TAC[Collect_geom.POW2_COND; NORM_POS_LE]);
1857  (REWRITE_WITH `m - u0 = (m - s2) + (s2 - u0:real^3) /\
1858                  z - u0 = (z - s2) + (s2 - u0:real^3)`);
1859  (VECTOR_ARITH_TAC);
1860  (REWRITE_WITH `norm (m - s2 + s2 - u0) pow 2 =
1861    norm (m - s2) pow 2 + norm (s2 - u0:real^3) pow 2`);
1862  (NEW_GOAL `(m - s2) dot (s2 - u0:real^3) = &0`);
1863  (ONCE_REWRITE_TAC[VECTOR_ARITH
1864    `(m - s2) dot (s2 - u0) = -- ((m - s2) dot (u0 - s2))`]);
1865  (REWRITE_TAC[REAL_ARITH `--a = &0 <=> a = &0`]);
1866  (REWRITE_WITH `s2:real^3 = circumcenter (set_of_list zl)`);
1867  (REWRITE_WITH `s2:real^3 = omega_list V zl`);
1868  (EXPAND_TAC "s2");
1869  (EXPAND_TAC "zl");
1870  (REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`; TRUNCATE_SIMPLEX_EXPLICIT_2;     LENGTH; ARITH_RULE `(SUC (SUC (SUC 0)) - 1) = 2`;
1871    Marchal_cells.OMEGA_LIST_TRUNCATE_2]);
1872  (MATCH_MP_TAC Rogers.XNHPWAB1);
1873  (EXISTS_TAC `2`);
1874  (REWRITE_TAC[IN; REAL_ARITH `a < b <=> ~(a >= b)`]);
1875  (ASM_REWRITE_TAC[]);
1876  (EXPAND_TAC "zl" THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
1877  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
1878  (MATCH_MP_TAC Rogers.MHFTTZN4);
1879  (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `2`);
1880  (REPEAT STRIP_TAC);
1881  (ASM_REWRITE_TAC[]);
1882  (EXPAND_TAC "zl" THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
1883  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
1884  (MATCH_MP_TAC (SET_RULE `(?C. a IN C/\ C SUBSET B) ==> a IN B`));
1885  (EXISTS_TAC `voronoi_list V zl`);
1886  (ASM_REWRITE_TAC[SET_SUBSET_AFFINE_HULL]);
1887  (MATCH_MP_TAC (SET_RULE `(?C. a IN C/\ C SUBSET B) ==> a IN B`));
1888  (EXISTS_TAC `set_of_list (zl:(real^3)list)`);
1889  (ASM_REWRITE_TAC[SET_SUBSET_AFFINE_HULL]);
1890  (EXPAND_TAC "zl" THEN REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_2;
1891    ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
1892  (SET_TAC[]);
1893  (ASM_SIMP_TAC[Trigonometry2.PITHAGO_THEOREM]);
1894
1895  (REWRITE_WITH
1896   `norm (z - s2 + s2 - u0) pow 2 =
1897    norm (z - s2) pow 2 + norm (s2 - u0:real^3) pow 2`);
1898  (NEW_GOAL `(z - s2) dot (s2 - u0:real^3) = &0`);
1899  (ONCE_REWRITE_TAC[VECTOR_ARITH
1900    `(z - s2) dot (s2 - u0) = -- ((z - s2) dot (u0 - s2))`]);
1901  (REWRITE_TAC[REAL_ARITH `--a = &0 <=> a = &0`]);
1902  (REWRITE_WITH `s2:real^3 = circumcenter (set_of_list zl)`);
1903  (REWRITE_WITH `s2:real^3 = omega_list V zl`);
1904  (EXPAND_TAC "s2");
1905  (EXPAND_TAC "zl");
1906  (REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`; TRUNCATE_SIMPLEX_EXPLICIT_2;     LENGTH; ARITH_RULE `(SUC (SUC (SUC 0)) - 1) = 2`;
1907    Marchal_cells.OMEGA_LIST_TRUNCATE_2]);
1908  (MATCH_MP_TAC Rogers.XNHPWAB1);
1909  (EXISTS_TAC `2`);
1910  (REWRITE_TAC[IN; REAL_ARITH `a < b <=> ~(a >= b)`]);
1911  (ASM_REWRITE_TAC[]);
1912  (EXPAND_TAC "zl" THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
1913  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
1914  (MATCH_MP_TAC Rogers.MHFTTZN4);
1915  (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `2`);
1916  (REPEAT STRIP_TAC);
1917  (ASM_REWRITE_TAC[]);
1918  (EXPAND_TAC "zl" THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
1919  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
1920  (MATCH_MP_TAC (SET_RULE `(?C. a IN C/\ C SUBSET B) ==> a IN B`));
1921  (EXISTS_TAC `voronoi_list V zl`);
1922  (ASM_REWRITE_TAC[SET_SUBSET_AFFINE_HULL]);
1923  (MATCH_MP_TAC (SET_RULE `(?C. a IN C/\ C SUBSET B) ==> a IN B`));
1924  (EXISTS_TAC `set_of_list (zl:(real^3)list)`);
1925  (ASM_REWRITE_TAC[SET_SUBSET_AFFINE_HULL]);
1926  (EXPAND_TAC "zl" THEN REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_2;
1927    ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
1928  (SET_TAC[]);
1929  (ASM_SIMP_TAC[Trigonometry2.PITHAGO_THEOREM]);
1930  (REWRITE_TAC[REAL_ARITH `a + b <= c + b <=> a <= c`]);
1931
1932  (MP_TAC (ASSUME `between m (s2,z:real^3)`));
1933  (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL; CONVEX_HULL_2;IN;IN_ELIM_THM] THEN STRIP_TAC);
1934  (REWRITE_TAC[ASSUME `m = u % s2 + v % z:real^3`]);
1935  (REWRITE_WITH
1936   `(u % s2 + v % z) - s2 = (u % s2 + v % z) - (u + v) % s2:real^3`);
1937  (ASM_REWRITE_TAC[VECTOR_MUL_LID]);
1938  (REWRITE_TAC[VECTOR_ARITH `(u % s2 + v % z) - (u + v) % s2 = v % (z - s2)`]);
1939  (REWRITE_TAC[NORM_MUL; REAL_ARITH `(a*b) pow 2 = a pow 2 * b pow 2`;
1940    REAL_ARITH `a * b <= b <=> &0 <= b * (&1 - a)`]);
1941  (MATCH_MP_TAC REAL_LE_MUL);
1942  (REWRITE_TAC[REAL_LE_POW_2]);
1943  (REWRITE_WITH `abs (v:real) = v`);
1944  (ASM_REWRITE_TAC[REAL_ABS_REFL]);
1945  (REWRITE_TAC[REAL_ARITH `&0 <= &1 - a <=> a <= &1 pow 2`]);
1946  (REWRITE_WITH ` v pow 2 <= &1 pow 2 <=> v <= &1`);
1947  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
1948  (MATCH_MP_TAC Collect_geom.POW2_COND);
1949  (ASM_REAL_ARITH_TAC);
1950  (ASM_REAL_ARITH_TAC);
1951
1952  (NEW_GOAL `norm (m - u0:real^3) = dist (u0, s:real^3)`);
1953  (ONCE_REWRITE_TAC[DIST_SYM]);
1954  (ASM_REWRITE_TAC[GSYM dist]);
1955  (NEW_GOAL `norm (m - u0:real^3) = sqrt (&2)`);
1956  (ASM_REAL_ARITH_TAC);
1957
1958  (REWRITE_WITH `(z - u0) dot (u1 - u0:real^3) = &2 *  norm (u1 - s1) pow 2`);
1959  (REWRITE_WITH `(z - u0) dot (u1 - u0) = (z - s1) dot (u1 - u0) +
1960                  (s1 - u0) dot (u1 - u0:real^3)`);
1961  (VECTOR_ARITH_TAC);
1962  (REWRITE_TAC[ASSUME `u1 - u0 = &2 % (u1 - s1:real^3)`; DOT_RMUL]);
1963  (REWRITE_WITH `(s1 - u0) = (u1 - s1:real^3)`);
1964  (ASM_REWRITE_TAC[CIRCUMCENTER_2;midpoint] THEN VECTOR_ARITH_TAC);
1965  (ASM_REWRITE_TAC[NORM_POW_2] THEN REAL_ARITH_TAC);
1966
1967  (NEW_GOAL `&2 * norm (u1 - s1:real^3) pow 2 <=
1968              norm (m - u0) * norm (u1 - u0) * a`);
1969  (EXPAND_TAC "a");
1970  (REWRITE_WITH `hl (vl:(real^3)list) = dist (s1, u1:real^3)`);
1971  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
1972  (REWRITE_WITH `s1:real^3 = circumcenter (set_of_list vl)`);
1973  (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`;
1974    TRUNCATE_SIMPLEX_EXPLICIT_1; set_of_list]);
1975  (ASM_REWRITE_TAC[]);
1976  (NEW_GOAL `!w:real^3. w IN set_of_list vl
1977                   ==> dist (circumcenter (set_of_list vl),w) = hl vl`);
1978  (MATCH_MP_TAC Rogers.HL_PROPERTIES);
1979  (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `1`);
1980  (ASM_REWRITE_TAC[] THEN EXPAND_TAC "vl");
1981  (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
1982  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
1983  (FIRST_ASSUM MATCH_MP_TAC);
1984  (EXPAND_TAC "vl");
1985  (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`;
1986    TRUNCATE_SIMPLEX_EXPLICIT_1; set_of_list]);
1987  (SET_TAC[]);
1988
1989  (ONCE_REWRITE_TAC[DIST_SYM] THEN REWRITE_TAC[dist]);
1990  (REWRITE_TAC[ASSUME `u1 - u0 = &2 % (u1 - s1:real^3)`; NORM_MUL]);
1991  (REWRITE_WITH `abs (&2) = &2`);
1992  (REWRITE_TAC[REAL_ABS_REFL; REAL_ARITH `&0 <= &2`]);
1993  (REWRITE_TAC[REAL_ARITH `a * (&2 * b) * b / c = (&2 * b pow 2) * ( a / c)`]);
1994  (REWRITE_TAC[REAL_ARITH `a <= a * b <=> &0 <= a * (b - &1)`]);
1995  (MATCH_MP_TAC REAL_LE_MUL);
1996  (ASM_SIMP_TAC[REAL_LE_MUL; REAL_LE_POW_2; REAL_ARITH `&0 <= &2`]);
1997  (REWRITE_TAC[REAL_ARITH `&0 <= a - b <=> b <= a`]);
1998  (REWRITE_WITH `sqrt (&2) / sqrt (&2) = &1`);
1999  (MATCH_MP_TAC REAL_DIV_REFL);
2000  (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~(a = &0)`));
2001  (SIMP_TAC[SQRT_POS_LT; REAL_ARITH `&0 < &2`]);
2002  (REAL_ARITH_TAC);
2003
2004  (NEW_GOAL `norm (m - u0) * norm (u1 - u0:real^3) * a <=
2005              norm (z - u0) * norm (u1 - u0) * a`);
2006  (REWRITE_TAC[REAL_ARITH `a * x * y <= b * x * y <=>
2007                            &0 <= (x * y) * (b - a)`]);
2008  (MATCH_MP_TAC REAL_LE_MUL);
2009  (STRIP_TAC);
2010  (MATCH_MP_TAC REAL_LE_MUL);
2011  (REWRITE_TAC[NORM_POS_LE]);
2012  (EXPAND_TAC "a" THEN MATCH_MP_TAC REAL_LE_DIV);
2013  (REWRITE_WITH `hl (vl:(real^3)list) = dist (s1, u1:real^3)`);
2014  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
2015  (REWRITE_WITH `s1:real^3 = circumcenter (set_of_list vl)`);
2016  (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`;
2017    TRUNCATE_SIMPLEX_EXPLICIT_1; set_of_list]);
2018  (ASM_REWRITE_TAC[]);
2019  (NEW_GOAL `!w:real^3. w IN set_of_list vl
2020                   ==> dist (circumcenter (set_of_list vl),w) = hl vl`);
2021  (MATCH_MP_TAC Rogers.HL_PROPERTIES);
2022  (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `1`);
2023  (ASM_REWRITE_TAC[] THEN EXPAND_TAC "vl");
2024  (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
2025  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
2026  (FIRST_ASSUM MATCH_MP_TAC);
2027  (EXPAND_TAC "vl");
2028  (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`;
2029    TRUNCATE_SIMPLEX_EXPLICIT_1; set_of_list]);
2030  (SET_TAC[]);
2031  (REWRITE_TAC[DIST_POS_LE]);
2032  (SIMP_TAC[SQRT_POS_LE; REAL_ARITH `&0 <= &2`]);
2033  (ASM_REAL_ARITH_TAC);
2034  (ASM_REAL_ARITH_TAC);
2035
2036
2037  (NEW_GOAL `t2 * norm (u1 - u0:real^3) pow 2 + t5 * ((z - u0) dot (u1 - u0))
2038   <= t2 * norm (u1 - u0) pow 2 + t5 * (norm (z - u0) * norm (u1 - u0) * a)`);
2039  (REWRITE_TAC[REAL_ARITH `a + b * c <= a + b * d <=> &0 <= b * (d - c)`]);
2040  (MATCH_MP_TAC REAL_LE_MUL);
2041  (ASM_REAL_ARITH_TAC);
2042
2043  (NEW_GOAL
2044  `t2 * norm (u1 - u0) pow 2 + t5 * norm (z - u0:real^3) * norm (u1 - u0) * a
2045  < norm (t2 % (u1 - u0) + t5 % (z - u0)) * norm (u1 - u0) * a`);
2046
2047  (REWRITE_TAC[REAL_ARITH
2048  `t2 * norm (u1 - u0) pow 2 + t5 * norm (z - u0:real^3) * norm (u1 - u0) * a
2049   < norm (t2 % (u1 - u0) + t5 % (z - u0)) * norm (u1 - u0) * a <=>
2050   &0 < (a * norm (t2 % (u1 - u0) + t5 % (z - u0)) - t2 * norm (u1 - u0) -
2051   t5 * a * norm (z - u0)) * norm (u1 - u0)`]);
2052  (MATCH_MP_TAC REAL_LT_MUL);
2053  (REPEAT STRIP_TAC);
2054  (REWRITE_TAC[REAL_ARITH `&0 < a - b - c <=> b + c < a`]);
2055
2056  (NEW_GOAL `t2 * norm (u1 - u0) < a * t2 * norm (u1 - u0:real^3)`);
2057  (REWRITE_TAC[REAL_ARITH `a * b < c * a * b <=> &0 < (--a) * b  * (&1 - c)`]);
2058  (MATCH_MP_TAC REAL_LT_MUL);
2059  (STRIP_TAC);
2060  (ASM_REAL_ARITH_TAC);
2061  (MATCH_MP_TAC REAL_LT_MUL);
2062  (STRIP_TAC);
2063  (REWRITE_TAC[NORM_POS_LT; VECTOR_ARITH `a - b = vec 0 <=> b = a`]);
2064  (ASM_REWRITE_TAC[]);
2065  (REWRITE_TAC[REAL_ARITH `&0 < a - b <=> b < a`] THEN EXPAND_TAC "a");
2066  (REWRITE_WITH `hl (vl:(real^3)list) / sqrt (&2) < &1 <=> hl vl < &1 * sqrt (&2) `);
2067  (MATCH_MP_TAC REAL_LT_LDIV_EQ);
2068  (MATCH_MP_TAC SQRT_POS_LT);
2069  (REAL_ARITH_TAC);
2070  (ASM_REWRITE_TAC[REAL_MUL_LID]);
2071
2072  (NEW_GOAL `a * t2 * norm (u1 - u0) + t5 * a * norm (z - u0) <=
2073  a * norm (t2 % (u1 - u0) + t5 % (z - u0:real^3))`);
2074  (REWRITE_TAC[REAL_ARITH
2075   `a * t2 * norm (u1 - u0) + t5 * a * norm (z - u0) <=
2076    a * norm (t2 % (u1 - u0) + t5 % (z - u0)) <=>
2077    &0 <= a * (norm (t2 % (u1 - u0) + t5 % (z - u0)) + (--t2 * norm (u1 - u0)) -     t5 * norm (z - u0))`]);
2078  (MATCH_MP_TAC REAL_LE_MUL);
2079  (STRIP_TAC);
2080  (EXPAND_TAC "a");
2081  (REWRITE_WITH `hl (vl:(real^3)list) = dist (s1, u1:real^3)`);
2082  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
2083  (REWRITE_WITH `s1:real^3 = circumcenter (set_of_list vl)`);
2084  (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`;
2085    TRUNCATE_SIMPLEX_EXPLICIT_1; set_of_list]);
2086  (ASM_REWRITE_TAC[]);
2087  (NEW_GOAL `!w:real^3. w IN set_of_list vl
2088                   ==> dist (circumcenter (set_of_list vl),w) = hl vl`);
2089  (MATCH_MP_TAC Rogers.HL_PROPERTIES);
2090  (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `1`);
2091  (ASM_REWRITE_TAC[] THEN EXPAND_TAC "vl");
2092  (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
2093  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
2094  (FIRST_ASSUM MATCH_MP_TAC);
2095  (EXPAND_TAC "vl");
2096  (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`;
2097    TRUNCATE_SIMPLEX_EXPLICIT_1; set_of_list]);
2098  (SET_TAC[]);
2099
2100  (MATCH_MP_TAC REAL_LE_DIV);
2101  (REWRITE_TAC[DIST_POS_LE]);
2102  (ASM_SIMP_TAC[SQRT_POS_LE; REAL_ARITH `&0 <= &2`]);
2103
2104  (ONCE_REWRITE_TAC[REAL_ARITH `&0 <= a + b - c <=> c <= a + b`]);
2105  (ABBREV_TAC `k1 = t2 % (u1 - u0) + t5 % (z - u0:real^3)`);
2106  (REWRITE_WITH `t5 * norm (z - u0) = norm (t5 % (z - u0:real^3))`);
2107  (REWRITE_TAC[NORM_MUL]);
2108  (REWRITE_WITH `abs t5 = t5`);
2109  (REWRITE_TAC[REAL_ABS_REFL]);
2110  (ASM_REAL_ARITH_TAC);
2111  (REWRITE_WITH `--t2 * norm (u1 - u0) = norm ((--t2) % (u1 - u0:real^3))`);
2112  (REWRITE_TAC[NORM_MUL]);
2113  (REWRITE_WITH `abs (--t2) = --t2`);
2114  (REWRITE_TAC[REAL_ABS_REFL]);
2115  (ASM_REAL_ARITH_TAC);
2116  (REWRITE_WITH `t5 % (z - u0) = k1 + --t2 % (u1 - u0:real^3)`);
2117  (EXPAND_TAC "k1" THEN VECTOR_ARITH_TAC);
2118  (REWRITE_TAC[NORM_TRIANGLE]);
2119  (ASM_REAL_ARITH_TAC);
2120  (REWRITE_TAC[NORM_POS_LT; VECTOR_ARITH `a - b = vec 0 <=> a = b`]);
2121  (ASM_REWRITE_TAC[]);
2122  (ASM_REAL_ARITH_TAC);
2123  (ASM_MESON_TAC[]);
2124
2125  (ASM_REAL_ARITH_TAC);
2126
2127 (* ------------------------------------------------------------------------ *)
2128
2129  (NEW_GOAL `t3 = &0 /\ t4 = &0`);
2130  (ASM_REAL_ARITH_TAC);
2131
2132  (ASM_CASES_TAC `t1 < &0`);
2133  (NEW_GOAL `F`);
2134  (UNDISCH_TAC `x:real^3 IN rcone_ge u1 u0 a`);
2135  (REWRITE_TAC[rcone_ge;rconesgn; IN; IN_ELIM_THM]);
2136  (REWRITE_TAC[REAL_ARITH `~(a >= b) <=> a < b`]);
2137
2138  (REWRITE_TAC[dist]);
2139  (REWRITE_WITH `x - u1 = t1 % (u0 - u1:real^3)`);
2140  (REWRITE_WITH `x - u1 = x - (t1 + t2) % u1:real^3`);
2141  (REWRITE_WITH `t1 + t2 = &1`);
2142  (ASM_REAL_ARITH_TAC);
2143  (VECTOR_ARITH_TAC);
2144  (ASM_REWRITE_TAC[]);
2145  (VECTOR_ARITH_TAC);
2146
2147  (REWRITE_TAC[DOT_LMUL;GSYM NORM_POW_2]);
2148  (NEW_GOAL `t1 * norm (u0 - u1:real^3) pow 2 < &0`);
2149  (REWRITE_TAC[REAL_ARITH `a * b < &0 <=> &0 < (--a) * b`]);
2150  (MATCH_MP_TAC REAL_LT_MUL);
2151  (STRIP_TAC);
2152  (ASM_REAL_ARITH_TAC);
2153  (REWRITE_TAC[GSYM Trigonometry2.NOT_ZERO_EQ_POW2_LT; NORM_EQ_0]);
2154  (ASM_REWRITE_TAC[VECTOR_ARITH `a - b = vec 0 <=> a = b`]);
2155
2156  (NEW_GOAL `&0 <= norm (t1 % (u0 - u1:real^3)) * norm (u0 - u1) * a`);
2157  (MATCH_MP_TAC REAL_LE_MUL);
2158  (REWRITE_TAC[NORM_POS_LE]);
2159  (MATCH_MP_TAC REAL_LE_MUL);
2160  (REWRITE_TAC[NORM_POS_LE]);
2161  (EXPAND_TAC "a");
2162  (REWRITE_WITH `hl (vl:(real^3)list) =
2163    dist (circumcenter (set_of_list vl),HD vl)`);
2164  (MATCH_MP_TAC Rogers.HL_EQ_DIST0);
2165  (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `1`);
2166  (ASM_REWRITE_TAC[] THEN EXPAND_TAC "vl");
2167  (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
2168  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
2169  (MATCH_MP_TAC REAL_LE_DIV);
2170  (REWRITE_TAC[DIST_POS_LE]);
2171  (SIMP_TAC[SQRT_POS_LE; REAL_ARITH `&0 <= &2`]);
2172  (ASM_REAL_ARITH_TAC);
2173  (ASM_MESON_TAC[]);
2174
2175  (ASM_CASES_TAC `t2 < &0`);
2176  (NEW_GOAL `F`);
2177  (UNDISCH_TAC `x:real^3 IN rcone_ge u0 u1 a`);
2178  (REWRITE_TAC[rcone_ge;rconesgn; IN; IN_ELIM_THM]);
2179  (REWRITE_TAC[REAL_ARITH `~(a >= b) <=> a < b`]);
2180
2181  (REWRITE_TAC[dist]);
2182  (REWRITE_WITH `x - u0 = t2 % (u1 - u0:real^3)`);
2183  (REWRITE_WITH `x - u0 = x - (t1 + t2) % u0:real^3`);
2184  (REWRITE_WITH `t1 + t2 = &1`);
2185  (ASM_REAL_ARITH_TAC);
2186  (VECTOR_ARITH_TAC);
2187  (ASM_REWRITE_TAC[]);
2188  (VECTOR_ARITH_TAC);
2189
2190  (REWRITE_TAC[DOT_LMUL;GSYM NORM_POW_2]);
2191  (NEW_GOAL `t2 * norm (u1 - u0:real^3) pow 2 < &0`);
2192  (REWRITE_TAC[REAL_ARITH `a * b < &0 <=> &0 < (--a) * b`]);
2193  (MATCH_MP_TAC REAL_LT_MUL);
2194  (STRIP_TAC);
2195  (ASM_REAL_ARITH_TAC);
2196  (REWRITE_TAC[GSYM Trigonometry2.NOT_ZERO_EQ_POW2_LT; NORM_EQ_0]);
2197  (ASM_REWRITE_TAC[VECTOR_ARITH `a - b = vec 0 <=> a = b`]);
2198
2199  (NEW_GOAL `&0 <= norm (t2 % (u1 - u0:real^3)) * norm (u1 - u0) * a`);
2200  (MATCH_MP_TAC REAL_LE_MUL);
2201  (REWRITE_TAC[NORM_POS_LE]);
2202  (MATCH_MP_TAC REAL_LE_MUL);
2203  (REWRITE_TAC[NORM_POS_LE]);
2204  (EXPAND_TAC "a");
2205  (REWRITE_WITH `hl (vl:(real^3)list) =
2206    dist (circumcenter (set_of_list vl),HD vl)`);
2207  (MATCH_MP_TAC Rogers.HL_EQ_DIST0);
2208  (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `1`);
2209  (ASM_REWRITE_TAC[] THEN EXPAND_TAC "vl");
2210  (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
2211  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
2212  (MATCH_MP_TAC REAL_LE_DIV);
2213  (REWRITE_TAC[DIST_POS_LE]);
2214  (SIMP_TAC[SQRT_POS_LE; REAL_ARITH `&0 <= &2`]);
2215  (ASM_REAL_ARITH_TAC);
2216  (ASM_MESON_TAC[]);
2217
2218  (ASM_REAL_ARITH_TAC);
2219
2220  (REWRITE_TAC[CONVEX_HULL_4; IN; IN_ELIM_THM]);
2221  (NEW_GOAL `between m (s2, s3:real^3)`);
2222  (ASM_CASES_TAC `hl (truncate_simplex 2 (ul:(real^3)list)) >= sqrt (&2)`);
2223  (EXPAND_TAC "m");
2224  (REWRITE_TAC[mxi]);
2225  (COND_CASES_TAC);
2226  (ASM_REWRITE_TAC[BETWEEN_REFL]);
2227  (NEW_GOAL `F`);
2228  (ASM_MESON_TAC[]);
2229  (ASM_MESON_TAC[]);
2230  (NEW_GOAL `?s. between s (omega_list_n V ul 2,omega_list_n V ul 3) /\
2231                   dist (u0,s) = sqrt (&2) /\
2232                   mxi V ul = s`);
2233  (MATCH_MP_TAC MXI_EXPLICIT);
2234  (EXISTS_TAC `u1:real^3` THEN EXISTS_TAC `u2:real^3` THEN EXISTS_TAC `u3:real^3`);
2235  (REWRITE_TAC[REAL_ARITH `a < b <=> ~(a >= b)`]);
2236  (ASM_REWRITE_TAC[]);
2237  (FIRST_ASSUM CHOOSE_TAC THEN UP_ASM_TAC);
2238  (ASM_REWRITE_TAC[] THEN STRIP_TAC);
2239  (ASM_REWRITE_TAC[]);
2240
2241  (UP_ASM_TAC THEN REWRITE_TAC[BETWEEN_IN_CONVEX_HULL; CONVEX_HULL_2; IN; IN_ELIM_THM]);
2242  (REPEAT STRIP_TAC);
2243  (EXISTS_TAC `t1:real` THEN EXISTS_TAC `t2:real`);
2244  (EXISTS_TAC `t3 * u` THEN EXISTS_TAC `t3 * v + t4`);
2245  (ASM_SIMP_TAC[REAL_LE_MUL; REAL_LE_ADD]);
2246  (STRIP_TAC);
2247  (REWRITE_TAC[REAL_ARITH `t1 + t2 + t3 * u + t3 * v + t4 =
2248    t1 + t2 + t3 * (u + v) + t4`]);
2249  (ASM_REWRITE_TAC[REAL_MUL_RID]);
2250  (VECTOR_ARITH_TAC);
2251  (SET_TAC[])]);;
2252
2253 (* Finished *)
2254
2255 end;;