text_formalization/packing/TEZFFSK.hl

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