text_formalization/packing/DDZUPHJ.hl

   1 (* ========================================================================= *)
   2 (*                FLYSPECK - BOOK FORMALIZATION                              *)
   3 (*                                                                           *)
   4 (*      Authour   : VU KHAC KY                                               *)
   5 (*      Book lemma: DDZUPHJ                                                  *)
   6 (*      Chaper    : Packing                                                  *)
   7 (*                                                                           *)
   8 (* ========================================================================= *)
   9
  10
  11 module Ddzuphj = 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 Tezffsk;;
  25 open Njiutiu;;
  26
  27 (* ========================================================================= *)
  28
  29 let DDZUPHJ_concl =
  30 `!V ul vl k.
  31   saturated V /\ packing V /\ k IN {0,1,2,3,4} /\
  32   barV V 3 ul /\ barV  V 3 vl /\ rogers V ul = rogers V vl /\
  33   aff_dim (rogers V ul) = &3 /\ ~ (mcell k V ul = {})
  34   ==> (mcell k V ul = mcell k V vl)`;;
  35
  36 (* ========================================================================= *)
  37
  38 let RCONE_GT_EQ_EMPTY_LEMMA = prove_by_refinement (
  39  `!a:real^3 b r. r >= &1 ==> rcone_gt a b r = {}`,
  40 [(REPEAT STRIP_TAC);
  41  (REWRITE_TAC[rcone_gt;rconesgn;
  42    SET_RULE `{x | P x} = {} <=> (!x. P x ==> F)`]);
  43  (REWRITE_TAC[dist] THEN REPEAT STRIP_TAC);
  44  (NEW_GOAL `(x - a) dot (b - a) <= norm(x - a) * norm (b - a:real^3)`);
  45  (REWRITE_TAC[NORM_CAUCHY_SCHWARZ]);
  46  (NEW_GOAL`norm (x - a) * norm (b:real^3 -a) * r >= norm (x-a) * norm (b-a)`);
  47  (REWRITE_TAC[REAL_ARITH `(a*b*c >= a * b) <=> &0 <= (a * b) * (c - &1)`]);
  48  (MATCH_MP_TAC REAL_LE_MUL);
  49  (STRIP_TAC);
  50  (MATCH_MP_TAC REAL_LE_MUL THEN REWRITE_TAC[NORM_POS_LE]);
  51  (ASM_REAL_ARITH_TAC);
  52  (ASM_REAL_ARITH_TAC)]);;
  53
  54 (* ========================================================================= *)
  55 (*         Main theorem                                                      *)
  56 (* ========================================================================= *)
  57
  58
  59 let DDZUPHJ = prove_by_refinement (DDZUPHJ_concl,
  60 [(REPEAT STRIP_TAC);
  61  (NEW_GOAL `?u0 u1 u2 u3. ul = [u0;u1;u2;u3:real^3]`);
  62  (MATCH_MP_TAC BARV_3_EXPLICIT);
  63  (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]);
  64  (NEW_GOAL `?v0 v1 v2 v3. vl = [v0;v1;v2;v3:real^3]`);
  65  (MATCH_MP_TAC BARV_3_EXPLICIT);
  66  (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]);
  67  (UP_ASM_TAC THEN UP_ASM_TAC THEN REPEAT STRIP_TAC);
  68
  69 (* ========================================================================= *)
  70 (* Case k = 4 *)
  71
  72  (ASM_CASES_TAC `k = 4`);
  73  (NEW_GOAL `hl (ul:(real^3)list) < sqrt (&2)`);
  74  (UNDISCH_TAC `~(mcell k V ul = {})` THEN
  75   SIMP_TAC[ASSUME `k = 4`; MCELL_EXPLICIT; ARITH_RULE `4 >= 4`;mcell4]);
  76  (MESON_TAC[]);
  77
  78  (NEW_GOAL `truncate_simplex 3 (ul:(real^3)list) = truncate_simplex 3 vl`);
  79  (MATCH_MP_TAC TEZFFSK);
  80  (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[ARITH_RULE `3 <= 3`]);
  81  (REWRITE_WITH `truncate_simplex 3 [u0; u1; u2; u3:real^3] = ul`);
  82  (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_3]);
  83  (ASM_REWRITE_TAC[]);
  84  (UP_ASM_TAC THEN REWRITE_WITH `truncate_simplex 3 (ul:(real^3)list) = ul`);
  85  (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_3]);
  86  (REWRITE_WITH `truncate_simplex 3 (vl:(real^3)list) = vl`);
  87  (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_3]);
  88  (STRIP_TAC);
  89  (REWRITE_TAC[ASSUME `ul = (vl:(real^3)list)`]);
  90
  91 (* ========================================================================= *)
  92 (* Case k = 3 *)
  93  (ASM_CASES_TAC `k = 3`);
  94  (NEW_GOAL `hl (truncate_simplex 2 ul) < sqrt (&2) /\
  95              sqrt (&2) <= hl (ul:(real^3)list)`);
  96  (UNDISCH_TAC `~(mcell k V ul = {})` THEN
  97   SIMP_TAC[ASSUME `k = 3`; MCELL_EXPLICIT;mcell3]);
  98  (MESON_TAC[]);
  99
 100  (NEW_GOAL `truncate_simplex 2 (ul:(real^3)list) = truncate_simplex 2 vl`);
 101  (MATCH_MP_TAC TEZFFSK);
 102  (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]);
 103
 104  (NEW_GOAL `!i. 0 <= i /\ i <= 3
 105                   ==> omega_list_n V ul i = omega_list_n V vl i`);
 106  (MATCH_MP_TAC NJIUTIU);
 107  (ASM_REWRITE_TAC[]);
 108
 109  (NEW_GOAL `sqrt (&2) <= hl (vl:(real^3)list)`);
 110  (REWRITE_TAC[ARITH_RULE `a <= b <=> (b < a ==> F)`]);
 111  (STRIP_TAC);
 112  (NEW_GOAL `hl vl = dist (omega_list V vl,HD vl)`);
 113  (MATCH_MP_TAC WAUFCHE2);
 114  (EXISTS_TAC `3` THEN REWRITE_TAC[IN] THEN ASM_REWRITE_TAC[]);
 115  (NEW_GOAL `hl ul <= dist (omega_list V ul,HD ul)`);
 116  (MATCH_MP_TAC WAUFCHE1);
 117  (EXISTS_TAC `3` THEN REWRITE_TAC[IN] THEN ASM_REWRITE_TAC[]);
 118  (UP_ASM_TAC THEN
 119    REWRITE_WITH `omega_list V ul = omega_list V vl /\ HD ul = HD vl`);
 120  (STRIP_TAC);
 121  (ASM_REWRITE_TAC[OMEGA_LIST; LENGTH]);
 122  (REWRITE_TAC[GSYM (ASSUME `ul = [u0;u1;u2;u3:real^3]`);
 123                GSYM (ASSUME `vl = [v0;v1;v2;v3:real^3]`)]);
 124  (FIRST_ASSUM MATCH_MP_TAC);
 125  (ARITH_TAC);
 126  (REWRITE_WITH `HD (ul:(real^3)list) = HD (truncate_simplex 2 ul)`);
 127  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 128  (MATCH_MP_TAC Packing3.HD_TRUNCATE_SIMPLEX);
 129  (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC);
 130  (REWRITE_WITH `HD (vl:(real^3)list) = HD (truncate_simplex 2 vl)`);
 131  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 132  (MATCH_MP_TAC Packing3.HD_TRUNCATE_SIMPLEX);
 133  (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC);
 134  (ASM_REWRITE_TAC[]);
 135  (ASM_REAL_ARITH_TAC);
 136
 137  (NEW_GOAL `mxi V ul = mxi V vl`);
 138  (REWRITE_TAC[mxi]);
 139  (COND_CASES_TAC);
 140  (COND_CASES_TAC);
 141  (FIRST_ASSUM MATCH_MP_TAC);
 142  (ARITH_TAC);
 143  (NEW_GOAL `F`);
 144  (ASM_REAL_ARITH_TAC);
 145  (ASM_MESON_TAC[]);
 146  (COND_CASES_TAC);
 147  (NEW_GOAL `F`);
 148  (ASM_MESON_TAC[]);
 149  (ASM_MESON_TAC[]);
 150
 151  (REWRITE_WITH `omega_list_n V ul 2 = omega_list_n V vl 2`);
 152  (FIRST_ASSUM MATCH_MP_TAC THEN ARITH_TAC);
 153  (REWRITE_WITH `omega_list_n V ul 3 = omega_list_n V vl 3`);
 154  (FIRST_ASSUM MATCH_MP_TAC THEN ARITH_TAC);
 155  (REWRITE_WITH `HD (ul:(real^3)list) = HD (truncate_simplex 2 ul)`);
 156  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 157  (MATCH_MP_TAC Packing3.HD_TRUNCATE_SIMPLEX);
 158  (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC);
 159  (REWRITE_WITH `HD (vl:(real^3)list) = HD (truncate_simplex 2 vl)`);
 160  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 161  (MATCH_MP_TAC Packing3.HD_TRUNCATE_SIMPLEX);
 162  (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC);
 163  (ASM_REWRITE_TAC[]);
 164
 165  (SIMP_TAC[ASSUME `k = 3`; MCELL_EXPLICIT; mcell3]);
 166  (COND_CASES_TAC);
 167  (COND_CASES_TAC);
 168  (ASM_REWRITE_TAC[]);
 169  (NEW_GOAL `F`);
 170  (UP_ASM_TAC THEN REWRITE_TAC[GSYM (ASSUME
 171   `truncate_simplex 2 ul = truncate_simplex 2 (vl:(real^3)list)`)]);
 172  (ASM_REWRITE_TAC[]);
 173  (ASM_MESON_TAC[]);
 174  (NEW_GOAL `F`);
 175  (ASM_MESON_TAC[]);
 176  (ASM_MESON_TAC[]);
 177
 178 (* ========================================================================= *)
 179 (* Case k = 2 *)
 180
 181  (ASM_CASES_TAC `k = 2`);
 182  (NEW_GOAL `hl (truncate_simplex 1 ul) < sqrt (&2) /\
 183              sqrt (&2) <= hl (ul:(real^3)list)`);
 184  (UNDISCH_TAC `~(mcell k V ul = {})` THEN
 185   SIMP_TAC[ASSUME `k = 2`; MCELL_EXPLICIT;mcell2]);
 186  (MESON_TAC[]);
 187
 188  (NEW_GOAL `truncate_simplex 1 (ul:(real^3)list) = truncate_simplex 1 vl`);
 189  (MATCH_MP_TAC TEZFFSK);
 190  (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[ARITH_RULE `1 <= 3`]);
 191
 192  (NEW_GOAL `!i. 0 <= i /\ i <= 3
 193                   ==> omega_list_n V ul i = omega_list_n V vl i`);
 194  (MATCH_MP_TAC NJIUTIU);
 195  (ASM_REWRITE_TAC[]);
 196
 197  (NEW_GOAL `sqrt (&2) <= hl (vl:(real^3)list)`);
 198  (REWRITE_TAC[ARITH_RULE `a <= b <=> (b < a ==> F)`]);
 199  (STRIP_TAC);
 200  (NEW_GOAL `hl vl = dist (omega_list V vl,HD vl)`);
 201  (MATCH_MP_TAC WAUFCHE2);
 202  (EXISTS_TAC `3` THEN REWRITE_TAC[IN] THEN ASM_REWRITE_TAC[]);
 203  (NEW_GOAL `hl ul <= dist (omega_list V ul,HD ul)`);
 204  (MATCH_MP_TAC WAUFCHE1);
 205  (EXISTS_TAC `3` THEN REWRITE_TAC[IN] THEN ASM_REWRITE_TAC[]);
 206  (UP_ASM_TAC THEN
 207    REWRITE_WITH `omega_list V ul = omega_list V vl /\ HD ul = HD vl`);
 208  (STRIP_TAC);
 209  (ASM_REWRITE_TAC[OMEGA_LIST; LENGTH]);
 210  (REWRITE_TAC[GSYM (ASSUME `ul = [u0;u1;u2;u3:real^3]`);
 211                GSYM (ASSUME `vl = [v0;v1;v2;v3:real^3]`)]);
 212  (FIRST_ASSUM MATCH_MP_TAC);
 213  (ARITH_TAC);
 214  (REWRITE_WITH `HD (ul:(real^3)list) = HD (truncate_simplex 1 ul)`);
 215  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 216  (MATCH_MP_TAC Packing3.HD_TRUNCATE_SIMPLEX);
 217  (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC);
 218  (REWRITE_WITH `HD (vl:(real^3)list) = HD (truncate_simplex 1 vl)`);
 219  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 220  (MATCH_MP_TAC Packing3.HD_TRUNCATE_SIMPLEX);
 221  (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC);
 222  (ASM_REWRITE_TAC[]);
 223  (ASM_REAL_ARITH_TAC);
 224
 225  (NEW_GOAL `mxi V ul = mxi V vl`);
 226  (REWRITE_TAC[mxi]);
 227  (COND_CASES_TAC);
 228  (COND_CASES_TAC);
 229  (FIRST_ASSUM MATCH_MP_TAC);
 230  (ARITH_TAC);
 231  (NEW_GOAL `F`);
 232
 233  (ABBREV_TAC `zl:(real^3)list = truncate_simplex 2 vl`);
 234  (NEW_GOAL `hl zl = dist (omega_list V zl,HD zl)`);
 235  (MATCH_MP_TAC WAUFCHE2);
 236  (EXISTS_TAC `2` THEN REWRITE_TAC[IN] THEN ASM_REWRITE_TAC[]);
 237  (STRIP_TAC);
 238  (EXPAND_TAC "zl" THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
 239  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]);
 240  (ASM_REAL_ARITH_TAC);
 241
 242  (ABBREV_TAC `wl:(real^3)list = truncate_simplex 2 ul`);
 243  (NEW_GOAL `hl wl <= dist (omega_list V wl,HD wl)`);
 244  (MATCH_MP_TAC WAUFCHE1);
 245  (EXISTS_TAC `2` THEN REWRITE_TAC[IN] THEN ASM_REWRITE_TAC[]);
 246  (EXPAND_TAC "wl" THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
 247  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]);
 248  (UP_ASM_TAC THEN
 249    REWRITE_WITH `omega_list V wl = omega_list_n V ul 2/\ HD wl = HD ul`);
 250  (EXPAND_TAC "wl");
 251  (STRIP_TAC);
 252  (MATCH_MP_TAC Packing3.OMEGA_LIST_LEMMA);
 253  (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC);
 254  (REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`;
 255    TRUNCATE_SIMPLEX_EXPLICIT_2; HD]);
 256
 257  (UNDISCH_TAC `hl zl = dist (omega_list V zl,HD zl)`);
 258  (REWRITE_WITH `omega_list V zl = omega_list_n V vl 2/\ HD zl = HD vl`);
 259  (EXPAND_TAC "zl");
 260  (STRIP_TAC);
 261  (MATCH_MP_TAC Packing3.OMEGA_LIST_LEMMA);
 262  (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC);
 263  (REWRITE_TAC[ASSUME `vl = [v0;v1;v2;v3:real^3]`;
 264    TRUNCATE_SIMPLEX_EXPLICIT_2; HD]);
 265  (REWRITE_WITH `omega_list_n V ul 2 = omega_list_n V vl 2/\ HD ul = HD vl`);
 266  (STRIP_TAC);
 267  (FIRST_ASSUM MATCH_MP_TAC THEN ARITH_TAC);
 268
 269  (REWRITE_WITH `HD (ul:(real^3)list) = HD (truncate_simplex 1 ul)`);
 270  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 271  (MATCH_MP_TAC Packing3.HD_TRUNCATE_SIMPLEX);
 272  (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC);
 273  (REWRITE_WITH `HD (vl:(real^3)list) = HD (truncate_simplex 1 vl)`);
 274  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 275  (MATCH_MP_TAC Packing3.HD_TRUNCATE_SIMPLEX);
 276  (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC);
 277  (ASM_REWRITE_TAC[]);
 278  (ASM_REAL_ARITH_TAC);
 279  (ASM_MESON_TAC[]);
 280
 281  (COND_CASES_TAC);
 282  (NEW_GOAL `F`);
 283
 284  (ABBREV_TAC `zl:(real^3)list = truncate_simplex 2 ul`);
 285  (NEW_GOAL `hl zl = dist (omega_list V zl,HD zl)`);
 286  (MATCH_MP_TAC WAUFCHE2);
 287  (EXISTS_TAC `2` THEN REWRITE_TAC[IN] THEN ASM_REWRITE_TAC[]);
 288  (STRIP_TAC);
 289  (EXPAND_TAC "zl" THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
 290  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]);
 291  (ASM_REAL_ARITH_TAC);
 292
 293  (ABBREV_TAC `wl:(real^3)list = truncate_simplex 2 vl`);
 294  (NEW_GOAL `hl wl <= dist (omega_list V wl,HD wl)`);
 295  (MATCH_MP_TAC WAUFCHE1);
 296  (EXISTS_TAC `2` THEN REWRITE_TAC[IN] THEN ASM_REWRITE_TAC[]);
 297  (EXPAND_TAC "wl" THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
 298  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]);
 299  (UP_ASM_TAC THEN
 300    REWRITE_WITH `omega_list V wl = omega_list_n V vl 2/\ HD wl = HD vl`);
 301  (EXPAND_TAC "wl");
 302  (STRIP_TAC);
 303  (MATCH_MP_TAC Packing3.OMEGA_LIST_LEMMA);
 304  (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC);
 305  (REWRITE_TAC[ASSUME `vl = [v0;v1;v2;v3:real^3]`;
 306    TRUNCATE_SIMPLEX_EXPLICIT_2; HD]);
 307
 308  (UNDISCH_TAC `hl zl = dist (omega_list V zl,HD zl)`);
 309  (REWRITE_WITH `omega_list V zl = omega_list_n V ul 2/\ HD zl = HD ul`);
 310  (EXPAND_TAC "zl");
 311  (STRIP_TAC);
 312  (MATCH_MP_TAC Packing3.OMEGA_LIST_LEMMA);
 313  (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC);
 314  (REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`;
 315    TRUNCATE_SIMPLEX_EXPLICIT_2; HD]);
 316  (REWRITE_WITH `omega_list_n V ul 2 = omega_list_n V vl 2/\ HD ul = HD vl`);
 317  (STRIP_TAC);
 318  (FIRST_ASSUM MATCH_MP_TAC THEN ARITH_TAC);
 319
 320  (REWRITE_WITH `HD (ul:(real^3)list) = HD (truncate_simplex 1 ul)`);
 321  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 322  (MATCH_MP_TAC Packing3.HD_TRUNCATE_SIMPLEX);
 323  (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC);
 324  (REWRITE_WITH `HD (vl:(real^3)list) = HD (truncate_simplex 1 vl)`);
 325  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 326  (MATCH_MP_TAC Packing3.HD_TRUNCATE_SIMPLEX);
 327  (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC);
 328  (ASM_REWRITE_TAC[]);
 329  (ASM_REAL_ARITH_TAC);
 330  (ASM_MESON_TAC[]);
 331
 332  (REWRITE_WITH `omega_list_n V ul 2 = omega_list_n V vl 2`);
 333  (FIRST_ASSUM MATCH_MP_TAC THEN ARITH_TAC);
 334  (REWRITE_WITH `omega_list_n V ul 3 = omega_list_n V vl 3`);
 335  (FIRST_ASSUM MATCH_MP_TAC THEN ARITH_TAC);
 336
 337  (REWRITE_WITH `HD (ul:(real^3)list) = HD (truncate_simplex 1 ul)`);
 338  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 339  (MATCH_MP_TAC Packing3.HD_TRUNCATE_SIMPLEX);
 340  (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC);
 341  (REWRITE_WITH `HD (vl:(real^3)list) = HD (truncate_simplex 1 vl)`);
 342  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 343  (MATCH_MP_TAC Packing3.HD_TRUNCATE_SIMPLEX);
 344  (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC);
 345  (REWRITE_TAC[ASSUME
 346    `truncate_simplex 1 (ul:(real^3)list) = truncate_simplex 1 vl`]);
 347
 348  (SIMP_TAC[ASSUME `k = 2`; MCELL_EXPLICIT; mcell2]);
 349  (COND_CASES_TAC);
 350  (COND_CASES_TAC);
 351  (REWRITE_TAC[ASSUME
 352    `truncate_simplex 1 (ul:(real^3)list) = truncate_simplex 1 vl`]);
 353  (REPEAT LET_TAC);
 354  (REWRITE_TAC[ASSUME `mxi V ul = mxi V vl`]);
 355  (REWRITE_WITH `omega_list_n V ul 3 = omega_list_n V vl 3`);
 356  (FIRST_ASSUM MATCH_MP_TAC THEN ARITH_TAC);
 357  (ASM_REWRITE_TAC[HD;TL]);
 358
 359  (NEW_GOAL `{u0, u1} = {v0, v1:real^3}`);
 360  (REWRITE_WITH `{u0,u1:real^3} = set_of_list(truncate_simplex 1 ul)`);
 361  (REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_1;
 362                ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
 363  (REWRITE_WITH `{v0,v1:real^3} = set_of_list(truncate_simplex 1 vl)`);
 364  (ASM_REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_1]);
 365  (ASM_REWRITE_TAC[]);
 366
 367  (ASM_CASES_TAC `u0 = v0:real^3`);
 368  (NEW_GOAL `u1 = v1:real^3`);
 369  (NEW_GOAL `~(u0 = u1:real^3)`);
 370  (STRIP_TAC);
 371  (NEW_GOAL `LENGTH (truncate_simplex 1 (ul:(real^3)list)) = 1 + 1 /\
 372              CARD (set_of_list (truncate_simplex 1 ul)) = 1 + 1`);
 373  (MATCH_MP_TAC Rogers.BARV_IMP_LENGTH_EQ_CARD);
 374  (EXISTS_TAC `V:real^3->bool` THEN STRIP_TAC);
 375  (ASM_REWRITE_TAC[]);
 376  (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
 377  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `1 <= 3`]);
 378  (UP_ASM_TAC THEN REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_1;
 379    ASSUME `ul = [u0;u1;u2;u3:real^3]`; ASSUME `u0 = u1:real^3`;
 380    SET_RULE `{a,a} = {a}`; Geomdetail.CARD_SING; ARITH_RULE `~(1 = 1 + 1)`]);
 381  (UP_ASM_TAC THEN UP_ASM_TAC THEN UP_ASM_TAC THEN SET_TAC[]);
 382  (ASM_REWRITE_TAC[]);
 383
 384  (NEW_GOAL `u0 = v1:real^3`);
 385  (UP_ASM_TAC THEN UP_ASM_TAC THEN SET_TAC[]);
 386  (NEW_GOAL `u1 = v0:real^3`);
 387  (DEL_TAC THEN UP_ASM_TAC THEN UP_ASM_TAC THEN SET_TAC[]);
 388  (ASM_REWRITE_TAC[]);
 389  (SET_TAC[]);
 390
 391  (NEW_GOAL `F`);
 392  (UP_ASM_TAC THEN REWRITE_TAC[GSYM (ASSUME
 393   `truncate_simplex 1 ul = truncate_simplex 1 (vl:(real^3)list)`)]);
 394  (ASM_REWRITE_TAC[]);
 395  (ASM_MESON_TAC[]);
 396  (NEW_GOAL `F`);
 397  (ASM_MESON_TAC[]);
 398  (ASM_MESON_TAC[]);
 399
 400 (* ========================================================================= *)
 401 (* Case k = 1 *)
 402
 403  (ASM_CASES_TAC `k = 1`);
 404  (NEW_GOAL `sqrt (&2) <= hl (ul:(real^3)list)`);
 405  (UNDISCH_TAC `~(mcell k V ul = {})` THEN
 406   SIMP_TAC[ASSUME `k = 1`; MCELL_EXPLICIT;mcell1]);
 407  (MESON_TAC[]);
 408
 409  (NEW_GOAL `!i. 0 <= i /\ i <= 3
 410                   ==> omega_list_n V ul i = omega_list_n V vl i`);
 411  (MATCH_MP_TAC NJIUTIU);
 412  (ASM_REWRITE_TAC[]);
 413
 414  (NEW_GOAL `HD ul = HD (vl:(real^3)list)`);
 415  (MATCH_MP_TAC ROGERS_INTER_V_LEMMA);
 416  (EXISTS_TAC `V:real^3->bool`);
 417  (REPEAT STRIP_TAC);
 418  (ASM_REWRITE_TAC[]);
 419  (ASM_REWRITE_TAC[]);
 420  (ASM_REWRITE_TAC[]);
 421
 422  (NEW_GOAL `HD ul IN set_of_list (ul:(real^3)list)`);
 423  (MATCH_MP_TAC Packing3.BARV_IMP_HD_IN_SET_OF_LIST);
 424  (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]);
 425  (NEW_GOAL `set_of_list (ul:(real^3)list) SUBSET V`);
 426  (MATCH_MP_TAC Packing3.BARV_SUBSET);
 427  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]);
 428  (ASM_SET_TAC[]);
 429  (REWRITE_WITH `rogers V vl (HD ul) <=> HD ul IN rogers V vl`);
 430  (REWRITE_TAC[IN]);
 431  (REWRITE_TAC[GSYM (ASSUME `rogers V ul = rogers V vl`)]);
 432  (REWRITE_WITH
 433   `rogers V ul =
 434       convex hull
 435      {HD ul, omega_list_n V ul 1, omega_list_n V ul 2, omega_list_n V ul 3}`);
 436  (MATCH_MP_TAC ROGERS_EXPLICIT);
 437  (ASM_REWRITE_TAC[]);
 438  (MATCH_MP_TAC IN_SET_IMP_IN_CONVEX_HULL_SET);
 439  (SET_TAC[]);
 440
 441  (NEW_GOAL `sqrt (&2) <= hl (vl:(real^3)list)`);
 442  (REWRITE_TAC[ARITH_RULE `a <= b <=> (b < a ==> F)`]);
 443  (STRIP_TAC);
 444  (NEW_GOAL `hl vl = dist (omega_list V vl,HD vl)`);
 445  (MATCH_MP_TAC WAUFCHE2);
 446  (EXISTS_TAC `3` THEN REWRITE_TAC[IN] THEN ASM_REWRITE_TAC[]);
 447  (NEW_GOAL `hl ul <= dist (omega_list V ul,HD ul)`);
 448  (MATCH_MP_TAC WAUFCHE1);
 449  (EXISTS_TAC `3` THEN REWRITE_TAC[IN] THEN ASM_REWRITE_TAC[]);
 450  (UP_ASM_TAC THEN
 451    REWRITE_WITH `omega_list V ul = omega_list V vl /\ HD ul = HD vl`);
 452  (STRIP_TAC);
 453  (ASM_REWRITE_TAC[OMEGA_LIST; LENGTH]);
 454  (REWRITE_TAC[GSYM (ASSUME `ul = [u0;u1;u2;u3:real^3]`);
 455                GSYM (ASSUME `vl = [v0;v1;v2;v3:real^3]`)]);
 456  (FIRST_ASSUM MATCH_MP_TAC);
 457  (ARITH_TAC);
 458  (ASM_REWRITE_TAC[]);
 459  (ASM_REAL_ARITH_TAC);
 460
 461  (ASM_CASES_TAC `hl (truncate_simplex 1 (ul:(real^3)list)) < sqrt (&2)`);
 462  (NEW_GOAL `truncate_simplex 1 (ul:(real^3)list) = truncate_simplex 1 vl`);
 463  (MATCH_MP_TAC TEZFFSK);
 464  (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[ARITH_RULE `1 <= 3`]);
 465
 466  (SIMP_TAC[ASSUME `k = 1`; MCELL_EXPLICIT; mcell1]);
 467  (COND_CASES_TAC);
 468  (COND_CASES_TAC);
 469  (REWRITE_TAC[ASSUME
 470    `truncate_simplex 1 (ul:(real^3)list) = truncate_simplex 1 vl`;
 471    ASSUME `HD ul = HD (vl:(real^3)list)`; ASSUME `rogers V ul = rogers V vl`]);
 472  (REWRITE_WITH `HD (TL ul) = EL 1 (truncate_simplex 1 (ul:(real^3)list))`);
 473  (REWRITE_TAC[ASSUME
 474   `ul = [u0;u1;u2;u3:real^3]`;TRUNCATE_SIMPLEX_EXPLICIT_1]);
 475  (REWRITE_TAC[EL; HD; TL; ARITH_RULE `1 = SUC 0`]);
 476  (REWRITE_WITH `HD (TL vl) = EL 1 (truncate_simplex 1 (vl:(real^3)list))`);
 477  (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);
 478  (REWRITE_TAC[EL; HD; TL; ARITH_RULE `1 = SUC 0`]);
 479  (ASM_REWRITE_TAC[]);
 480  (NEW_GOAL `F`);
 481  (ASM_MESON_TAC[]);
 482  (ASM_MESON_TAC[]);
 483  (NEW_GOAL `F`);
 484  (ASM_MESON_TAC[]);
 485  (ASM_MESON_TAC[]);
 486
 487
 488  (NEW_GOAL `sqrt (&2) <= hl (truncate_simplex 1 (ul:(real^3)list))`);
 489  (ASM_REAL_ARITH_TAC);
 490
 491  (NEW_GOAL `sqrt (&2) <= hl (truncate_simplex 1 (vl:(real^3)list))`);
 492  (REWRITE_TAC[ARITH_RULE `a <= b <=> (b < a ==> F)`]);
 493  (STRIP_TAC);
 494  (ABBREV_TAC `zl = truncate_simplex 1 (vl:(real^3)list)`);
 495  (NEW_GOAL `hl zl = dist (omega_list V zl,HD zl)`);
 496  (MATCH_MP_TAC WAUFCHE2);
 497  (EXISTS_TAC `1` THEN REWRITE_TAC[IN] THEN ASM_REWRITE_TAC[]);
 498  (EXPAND_TAC "zl" THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
 499  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `1 <= 3`]);
 500
 501  (ABBREV_TAC `wl = truncate_simplex 1 (ul:(real^3)list)`);
 502  (NEW_GOAL `hl wl <= dist (omega_list V wl,HD wl)`);
 503  (MATCH_MP_TAC WAUFCHE1);
 504  (EXISTS_TAC `1` THEN REWRITE_TAC[IN] THEN ASM_REWRITE_TAC[]);
 505  (EXPAND_TAC "wl" THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
 506  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `1 <= 3`]);
 507
 508  (UP_ASM_TAC THEN
 509    REWRITE_WITH `omega_list V wl = omega_list_n V ul 1 /\ HD wl = HD ul`);
 510  (STRIP_TAC);
 511  (EXPAND_TAC "wl");
 512  (MATCH_MP_TAC Packing3.OMEGA_LIST_LEMMA);
 513  (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC);
 514  (EXPAND_TAC "wl");
 515  (MATCH_MP_TAC Packing3.HD_TRUNCATE_SIMPLEX);
 516  (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC);
 517
 518  (UNDISCH_TAC `hl zl = dist (omega_list V zl,HD zl)` THEN
 519    REWRITE_WITH `omega_list V zl = omega_list_n V vl 1 /\ HD zl = HD vl`);
 520  (STRIP_TAC);
 521  (EXPAND_TAC "zl");
 522  (MATCH_MP_TAC Packing3.OMEGA_LIST_LEMMA);
 523  (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC);
 524  (EXPAND_TAC "zl");
 525  (MATCH_MP_TAC Packing3.HD_TRUNCATE_SIMPLEX);
 526  (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC);
 527
 528  (REWRITE_WITH `omega_list_n V ul 1 = omega_list_n V  vl 1`);
 529  (FIRST_ASSUM MATCH_MP_TAC);
 530  (ARITH_TAC);
 531  (REWRITE_TAC[ASSUME `HD (ul:(real^3)list) = HD (vl:(real^3)list)`]);
 532  (ASM_REAL_ARITH_TAC);
 533
 534  (SIMP_TAC[ASSUME `k = 1`; MCELL_EXPLICIT; mcell1]);
 535  (COND_CASES_TAC);
 536  (COND_CASES_TAC);
 537
 538  (REWRITE_WITH
 539  `rcone_gt (HD (ul:(real^3)list)) (HD (TL ul))
 540   (hl (truncate_simplex 1 ul) / sqrt (&2)) = {}`);
 541  (MATCH_MP_TAC RCONE_GT_EQ_EMPTY_LEMMA);
 542  (ONCE_REWRITE_TAC[REAL_ARITH `a >= b <=> b <= a`]);
 543  (REWRITE_WITH `&1 <= hl (truncate_simplex 1 (ul:(real^3)list)) / sqrt (&2)
 544     <=> &1 * sqrt (&2) <= hl (truncate_simplex 1 ul)`);
 545  (MATCH_MP_TAC REAL_LE_RDIV_EQ);
 546  (MATCH_MP_TAC SQRT_POS_LT);
 547  (ARITH_TAC);
 548  (REWRITE_TAC[REAL_MUL_LID] THEN ASM_REAL_ARITH_TAC);
 549
 550  (REWRITE_WITH
 551  `rcone_gt (HD (vl:(real^3)list)) (HD (TL vl))
 552   (hl (truncate_simplex 1 vl) / sqrt (&2)) = {}`);
 553  (MATCH_MP_TAC RCONE_GT_EQ_EMPTY_LEMMA);
 554  (ONCE_REWRITE_TAC[REAL_ARITH `a >= b <=> b <= a`]);
 555  (REWRITE_WITH `&1 <= hl (truncate_simplex 1 (vl:(real^3)list)) / sqrt (&2)
 556     <=> &1 * sqrt (&2) <= hl (truncate_simplex 1 vl)`);
 557  (MATCH_MP_TAC REAL_LE_RDIV_EQ);
 558  (MATCH_MP_TAC SQRT_POS_LT);
 559  (ARITH_TAC);
 560  (REWRITE_TAC[REAL_MUL_LID] THEN ASM_REAL_ARITH_TAC);
 561  (ASM_REWRITE_TAC[]);
 562
 563  (NEW_GOAL `F`);
 564  (ASM_MESON_TAC[]);
 565  (ASM_MESON_TAC[]);
 566  (NEW_GOAL `F`);
 567  (ASM_MESON_TAC[]);
 568  (ASM_MESON_TAC[]);
 569
 570 (* ========================================================================= *)
 571 (* Case k = 0 *)
 572
 573  (NEW_GOAL `k = 0`);
 574  (ASM_SET_TAC[]);
 575  (SIMP_TAC[ASSUME `k = 0`; MCELL_EXPLICIT; mcell0]);
 576  (REWRITE_TAC[ASSUME `rogers V ul = rogers V vl`]);
 577
 578  (NEW_GOAL `!i. 0 <= i /\ i <= 3
 579                   ==> omega_list_n V ul i = omega_list_n V vl i`);
 580  (MATCH_MP_TAC NJIUTIU);
 581  (ASM_REWRITE_TAC[]);
 582
 583  (REWRITE_WITH `HD ul = HD (vl:(real^3)list)`);
 584  (MATCH_MP_TAC ROGERS_INTER_V_LEMMA);
 585  (EXISTS_TAC `V:real^3->bool`);
 586  (REPEAT STRIP_TAC);
 587  (ASM_REWRITE_TAC[]);
 588  (ASM_REWRITE_TAC[]);
 589  (ASM_REWRITE_TAC[]);
 590
 591  (NEW_GOAL `HD ul IN set_of_list (ul:(real^3)list)`);
 592  (MATCH_MP_TAC Packing3.BARV_IMP_HD_IN_SET_OF_LIST);
 593  (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]);
 594  (NEW_GOAL `set_of_list (ul:(real^3)list) SUBSET V`);
 595  (MATCH_MP_TAC Packing3.BARV_SUBSET);
 596  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]);
 597  (ASM_SET_TAC[]);
 598  (REWRITE_WITH `rogers V vl (HD ul) <=> HD ul IN rogers V vl`);
 599  (REWRITE_TAC[IN]);
 600  (REWRITE_TAC[GSYM (ASSUME `rogers V ul = rogers V vl`)]);
 601  (REWRITE_WITH
 602   `rogers V ul =
 603       convex hull
 604      {HD ul, omega_list_n V ul 1, omega_list_n V ul 2, omega_list_n V ul 3}`);
 605  (MATCH_MP_TAC ROGERS_EXPLICIT);
 606  (ASM_REWRITE_TAC[]);
 607  (MATCH_MP_TAC IN_SET_IMP_IN_CONVEX_HULL_SET);
 608  (SET_TAC[])]);;
 609
 610
 611 end;;