text_formalization/packing/marchal_cells.hl

   1
   2 (* ========================================================================= *)
   3 (*                FLYSPECK - BOOK FORMALIZATION                              *)
   4 (*                                                                           *)
   5 (*      Authour   : VU KHAC KY                                               *)
   6 (*      Book lemma: Marchal cells                                            *)
   7 (*      Chaper    : Packing (Clusters)                                       *)
   8 (*      Date      : October 3, 2010                                          *)
   9 (*                                                                           *)
  10 (* ========================================================================= *)
  11
  12 (* ========================================================================== *)
  13 (* This file contains some lemmas that support for marchalcells part.         *)
  14 (* ========================================================================== *)
  15
  16
  17
  18 (* dmtcp *)
  19
  20 flyspeck_needs "nonlinear/vukhacky_tactics.hl";;
  21 flyspeck_needs "packing/pack_defs.hl";;
  22 flyspeck_needs "packing/pack_concl.hl";;
  23 flyspeck_needs "packing/pack1.hl";;
  24 flyspeck_needs "packing/Rogers.hl";;
  25
  26
  27 module Marchal_cells = struct
  28
  29   open Sphere;;
  30 open Pack_defs;;
  31 open Pack_concl;;
  32 open Vukhacky_tactics;;
  33 open Pack1;;
  34 open Rogers;;
  35
  36 (* ========================================================================== *)
  37
  38 let TRUNCATE_SIMPLEX_GENERAL_0 = prove_by_refinement (
  39  `!(xl:(real^3)list). ~(xl = []) ==> truncate_simplex 0 xl = [HD xl]`,
  40 [ (REPEAT STRIP_TAC);
  41  (REWRITE_TAC[TRUNCATE_SIMPLEX;INITIAL_SUBLIST]);
  42  (MATCH_MP_TAC SELECT_UNIQUE);
  43  (GEN_TAC THEN REWRITE_TAC[IN_ELIM_THM] THEN EQ_TAC);
  44  STRIP_TAC;
  45
  46  (NEW_GOAL `?x xl. (y:(real^3)list) = CONS x xl /\ LENGTH xl = 0`);
  47  (REWRITE_TAC[GSYM LENGTH_EQ_CONS]);
  48  (ASM_ARITH_TAC);
  49  (FIRST_X_ASSUM CHOOSE_TAC);
  50  (FIRST_X_ASSUM CHOOSE_TAC);
  51  (NEW_GOAL `(xl':(real^3)list) = []`);
  52  (ASM_MESON_TAC[LENGTH_EQ_NIL]);
  53  (ASM_REWRITE_TAC[]);
  54  (MATCH_MP_TAC (MESON[] `x = y ==> [x] = [y]`));
  55  (ASM_REWRITE_TAC[APPEND;HD]);
  56  STRIP_TAC;
  57
  58  (ASM_REWRITE_TAC[LENGTH;HD;ARITH_RULE `SUC 0 = 0 + 1`]);
  59
  60  (NEW_GOAL `?h:real^3 t. xl = CONS h t`);
  61  (ASM_MESON_TAC[list_CASES]);
  62  (FIRST_X_ASSUM CHOOSE_TAC);
  63  (FIRST_X_ASSUM CHOOSE_TAC);
  64  (EXISTS_TAC `t:(real^3)list`);
  65  (ASM_REWRITE_TAC[HD;APPEND])]);;
  66
  67
  68
  69 let TRUNCATE_SIMPLEX_EXPLICIT_0 = prove_by_refinement (
  70  `!u0 u1 u2 u3:real^3. truncate_simplex 0 [u0] = [u0] /\
  71                         truncate_simplex 0 [u0;u1] = [u0] /\
  72                         truncate_simplex 0 [u0;u1;u2] = [u0] /\
  73                         truncate_simplex 0 [u0;u1;u2;u3] = [u0]`,
  74 [ (REPEAT STRIP_TAC);
  75  (NEW_GOAL `~([u0:real^3] = [])`);
  76  (MESON_TAC[NOT_CONS_NIL]);
  77  (ASM_MESON_TAC[TRUNCATE_SIMPLEX_GENERAL_0;HD]);
  78  (NEW_GOAL `~([u0:real^3;u1] = [])`);
  79  (MESON_TAC[NOT_CONS_NIL]);
  80  (ASM_MESON_TAC[TRUNCATE_SIMPLEX_GENERAL_0;HD]);
  81  (NEW_GOAL `~([u0:real^3;u1;u2] = [])`);
  82  (MESON_TAC[NOT_CONS_NIL]);
  83  (ASM_MESON_TAC[TRUNCATE_SIMPLEX_GENERAL_0;HD]);
  84  (NEW_GOAL `~([u0:real^3;u1;u2;u3] = [])`);
  85  (MESON_TAC[NOT_CONS_NIL]);
  86  (ASM_MESON_TAC[TRUNCATE_SIMPLEX_GENERAL_0;HD])]);;
  87
  88
  89 (* -------------------------------------------------------------------------- *)
  90
  91
  92 let TRUNCATE_SIMPLEX_GENERAL_1 = prove_by_refinement (
  93  `!ul vl a b:real^3.
  94    (ul = APPEND [a;b] vl) ==> truncate_simplex 1 ul = [a;b]`,
  95 [ (REPEAT STRIP_TAC);
  96  (REWRITE_TAC[TRUNCATE_SIMPLEX;INITIAL_SUBLIST]);
  97  (MATCH_MP_TAC SELECT_UNIQUE);
  98  (GEN_TAC THEN REWRITE_TAC[IN_ELIM_THM] THEN EQ_TAC);
  99  STRIP_TAC;
 100
 101  (NEW_GOAL `?x xl. (y:(real^3)list) = CONS x xl /\ LENGTH xl = 1`);
 102  (REWRITE_TAC[GSYM LENGTH_EQ_CONS]);
 103  (ASM_ARITH_TAC);
 104  (FIRST_X_ASSUM CHOOSE_TAC);
 105  (FIRST_X_ASSUM CHOOSE_TAC);
 106
 107  (NEW_GOAL `?z zl. (xl:(real^3)list) = CONS z zl /\ LENGTH zl = 0`);
 108  (REWRITE_TAC[GSYM LENGTH_EQ_CONS]);
 109  (ASM_ARITH_TAC);
 110  (FIRST_X_ASSUM CHOOSE_TAC);
 111  (FIRST_X_ASSUM CHOOSE_TAC);
 112
 113  (NEW_GOAL `(zl:(real^3)list) = []`);
 114  (ASM_MESON_TAC[LENGTH_EQ_NIL]);
 115  (ASM_REWRITE_TAC[]);
 116  (MATCH_MP_TAC (MESON[] `x = y /\ z = t ==> [x;z] = [y;t]`));
 117  (UNDISCH_TAC `ul:(real^3)list = APPEND y yl`);
 118  (ASM_REWRITE_TAC[APPEND]);
 119  (MESON_TAC[CONS_11]);
 120  (REPEAT STRIP_TAC);
 121  (ASM_REWRITE_TAC[LENGTH;ARITH_RULE `SUC (SUC 0) = 1 + 1`]);
 122  (EXISTS_TAC `vl:(real^3)list`);
 123  (ASM_REWRITE_TAC[])]);;
 124
 125
 126 (* -------------------------------------------------------------------------- *)
 127
 128 let TRUNCATE_SIMPLEX_EXPLICIT_1 = prove_by_refinement (
 129  `!a b c (d:real^3). truncate_simplex 1 [a;b] = [a;b] /\
 130                       truncate_simplex 1 [a;b;c] = [a;b] /\
 131                       truncate_simplex 1 [a;b;c;d] = [a;b]`,
 132 [ (REPEAT STRIP_TAC);
 133  (NEW_GOAL `[a;b] = APPEND [a:real^3; b] []`);
 134  (MESON_TAC[APPEND_NIL]);
 135  (ASM_MESON_TAC[TRUNCATE_SIMPLEX_GENERAL_1]);
 136  (NEW_GOAL `[a;b;c] = APPEND [a:real^3; b] [c]`);
 137  (REWRITE_TAC[APPEND]);
 138  (ASM_MESON_TAC[TRUNCATE_SIMPLEX_GENERAL_1]);
 139  (NEW_GOAL `[a;b;c;d] = APPEND [a:real^3; b] [c;d]`);
 140  (REWRITE_TAC[APPEND]);
 141  (ASM_MESON_TAC[TRUNCATE_SIMPLEX_GENERAL_1])]);;
 142
 143
 144 (* -------------------------------------------------------------------------- *)
 145
 146 let TRUNCATE_SIMPLEX_GENERAL_2 = prove_by_refinement (
 147  `!a b c:real^3 ul vl.
 148     ul = APPEND [a;b;c] vl ==> truncate_simplex 2 ul = [a;b;c]`,
 149 [ (REPEAT STRIP_TAC);
 150  (REWRITE_TAC[TRUNCATE_SIMPLEX;INITIAL_SUBLIST]);
 151  (MATCH_MP_TAC SELECT_UNIQUE);
 152  (GEN_TAC THEN REWRITE_TAC[IN_ELIM_THM] THEN EQ_TAC);
 153  STRIP_TAC;
 154
 155  (NEW_GOAL `?x xl. (y:(real^3)list) = CONS x xl /\ LENGTH xl = 2`);
 156  (REWRITE_TAC[GSYM LENGTH_EQ_CONS]);
 157  (ASM_ARITH_TAC);
 158  (FIRST_X_ASSUM CHOOSE_TAC);
 159  (FIRST_X_ASSUM CHOOSE_TAC);
 160
 161  (NEW_GOAL `?z zl. (xl:(real^3)list) = CONS z zl /\ LENGTH zl = 1`);
 162  (REWRITE_TAC[GSYM LENGTH_EQ_CONS]);
 163  (ASM_ARITH_TAC);
 164  (FIRST_X_ASSUM CHOOSE_TAC);
 165  (FIRST_X_ASSUM CHOOSE_TAC);
 166
 167  (NEW_GOAL `?t tl. (zl:(real^3)list) = CONS t tl /\ LENGTH tl = 0`);
 168  (REWRITE_TAC[GSYM LENGTH_EQ_CONS]);
 169  (ASM_ARITH_TAC);
 170  (FIRST_X_ASSUM CHOOSE_TAC);
 171  (FIRST_X_ASSUM CHOOSE_TAC);
 172
 173  (NEW_GOAL `(tl:(real^3)list) = []`);
 174  (ASM_MESON_TAC[LENGTH_EQ_NIL]);
 175  (ASM_REWRITE_TAC[]);
 176  (MATCH_MP_TAC (MESON[] `x = y /\ z = t /\ s = r ==> [x;z;s] = [y;t;r]`));
 177  (UNDISCH_TAC `ul:(real^3)list = APPEND y yl`);
 178  (ASM_REWRITE_TAC[APPEND;CONS_11]);
 179  (MESON_TAC[]);
 180  (REPEAT STRIP_TAC);
 181  (ASM_REWRITE_TAC[LENGTH;ARITH_RULE
 182  `SUC (1 + 1) = 2 + 1 /\ SUC (SUC (SUC 0)) = 2 + 1`]);
 183  (EXISTS_TAC `vl:(real^3)list`);
 184  (ASM_REWRITE_TAC[])]);;
 185
 186
 187 (* -------------------------------------------------------------------------- *)
 188
 189 let TRUNCATE_SIMPLEX_EXPLICIT_2 = prove_by_refinement (
 190  `!a b c d:real^3.
 191          truncate_simplex 2 [a; b; c] = [a; b; c] /\
 192          truncate_simplex 2 [a; b; c; d] = [a; b; c]`,
 193 [ (REPEAT STRIP_TAC);
 194  (NEW_GOAL `[a;b;c] = APPEND [a:real^3; b; c] []`);
 195  (MESON_TAC[APPEND_NIL]);
 196  (ASM_MESON_TAC[TRUNCATE_SIMPLEX_GENERAL_2]);
 197  (NEW_GOAL `[a;b;c;d] = APPEND [a:real^3; b; c] [d]`);
 198  (REWRITE_TAC[APPEND]);
 199  (ASM_MESON_TAC[TRUNCATE_SIMPLEX_GENERAL_2])]);;
 200
 201
 202 (* -------------------------------------------------------------------------- *)
 203
 204 let TRUNCATE_SIMPLEX_EXPLICIT_3 = prove_by_refinement (
 205  `!a b c d:real^3.
 206          truncate_simplex 3 [a; b; c; d] = [a; b; c; d]`,
 207 [ (REPEAT STRIP_TAC);
 208  (REWRITE_TAC[TRUNCATE_SIMPLEX;INITIAL_SUBLIST]);
 209  (MATCH_MP_TAC SELECT_UNIQUE);
 210  (GEN_TAC THEN REWRITE_TAC[IN_ELIM_THM] THEN EQ_TAC);
 211  STRIP_TAC;
 212
 213  (NEW_GOAL `?x xl. (y:(real^3)list) = CONS x xl /\ LENGTH xl = 3`);
 214  (REWRITE_TAC[GSYM LENGTH_EQ_CONS]);
 215  (ASM_ARITH_TAC);
 216  (FIRST_X_ASSUM CHOOSE_TAC);
 217  (FIRST_X_ASSUM CHOOSE_TAC);
 218
 219  (NEW_GOAL `?z zl. (xl:(real^3)list) = CONS z zl /\ LENGTH zl = 2`);
 220  (REWRITE_TAC[GSYM LENGTH_EQ_CONS]);
 221  (ASM_ARITH_TAC);
 222  (FIRST_X_ASSUM CHOOSE_TAC);
 223  (FIRST_X_ASSUM CHOOSE_TAC);
 224
 225  (NEW_GOAL `?t tl. (zl:(real^3)list) = CONS t tl /\ LENGTH tl = 1`);
 226  (REWRITE_TAC[GSYM LENGTH_EQ_CONS]);
 227  (ASM_ARITH_TAC);
 228  (FIRST_X_ASSUM CHOOSE_TAC);
 229  (FIRST_X_ASSUM CHOOSE_TAC);
 230
 231  (NEW_GOAL `?w wl. (tl:(real^3)list) = CONS w wl /\ LENGTH wl = 0`);
 232  (REWRITE_TAC[GSYM LENGTH_EQ_CONS]);
 233  (ASM_ARITH_TAC);
 234  (FIRST_X_ASSUM CHOOSE_TAC);
 235  (FIRST_X_ASSUM CHOOSE_TAC);
 236
 237  (NEW_GOAL `(wl:(real^3)list) = []`);
 238  (ASM_MESON_TAC[LENGTH_EQ_NIL]);
 239  (ASM_REWRITE_TAC[]);
 240
 241  (NEW_GOAL `LENGTH [a;b;c;d:real^3] =
 242              LENGTH (y:(real^3)list) + LENGTH (yl:(real^3)list)`);
 243  (ASM_MESON_TAC[LENGTH_APPEND]);
 244  (UP_ASM_TAC THEN ASM_REWRITE_TAC[LENGTH] THEN DISCH_TAC);
 245  (NEW_GOAL `(yl:(real^3)list) = ([]:(real^3)list)`);
 246  (REWRITE_TAC[GSYM LENGTH_EQ_NIL]);
 247  (ASM_ARITH_TAC);
 248  (ASM_REWRITE_TAC[APPEND]);
 249
 250  (REPEAT STRIP_TAC);
 251  (ASM_REWRITE_TAC[LENGTH;ARITH_RULE
 252   `SUC (2 + 1) = 3 + 1 /\ SUC (SUC (SUC 0)) = 2 + 1`]);
 253
 254  (EXISTS_TAC `[]:(real^3)list`);
 255  (ASM_REWRITE_TAC[APPEND])]);;
 256
 257
 258 (* -------------------------------------------------------------------------- *)
 259
 260 let OMEGA_LIST_TRUNCATE_0 = prove_by_refinement (
 261  `!V u0:real^3 u1 u2 u3.
 262      omega_list_n V [u0;u1;u2;u3] 0 = omega_list V [u0] `,
 263 [ (REPEAT GEN_TAC);
 264  (REWRITE_TAC[OMEGA_LIST]);
 265  (REWRITE_WITH `LENGTH [u0:real^3] - 1 = 0`);
 266  (REWRITE_TAC[LENGTH; ARITH_RULE `SUC 0 - 1 = 0`]);
 267  (REWRITE_TAC[OMEGA_LIST_N]);
 268  (MESON_TAC[HD])]);;
 269
 270
 271 (* -------------------------------------------------------------------------- *)
 272
 273 let OMEGA_LIST_TRUNCATE_1 = prove_by_refinement (
 274  `!V u0:real^3 u1 u2 u3.
 275      omega_list_n V [u0;u1;u2;u3] 1 = omega_list V [u0;u1] `,
 276 [ (REPEAT GEN_TAC);
 277  (REWRITE_TAC[OMEGA_LIST]);
 278  (REWRITE_WITH `LENGTH [u0:real^3;u1] - 1 = 1`);
 279  (REWRITE_TAC[LENGTH; ARITH_RULE `SUC (SUC 0) - 1 = 1`]);
 280  (REWRITE_TAC[ARITH_RULE `1 = SUC 0`; OMEGA_LIST_N]);
 281  (REWRITE_TAC[ARITH_RULE `SUC 0 = 1`;TRUNCATE_SIMPLEX_EXPLICIT_1;HD])]);;
 282
 283
 284
 285 let OMEGA_LIST_TRUNCATE_2 = prove_by_refinement (
 286  `!V u0:real^3 u1 u2 u3.
 287      omega_list_n V [u0;u1;u2;u3] 2 = omega_list V [u0;u1;u2] `,
 288 [ (REPEAT GEN_TAC);
 289  (REWRITE_TAC[OMEGA_LIST]);
 290  (REWRITE_WITH `LENGTH [u0:real^3;u1;u2] - 1 = 2`);
 291  (REWRITE_TAC[LENGTH; ARITH_RULE `SUC (SUC (SUC 0)) - 1 = 2`]);
 292  (REWRITE_TAC[ARITH_RULE `2 = SUC 1`; OMEGA_LIST_N]);
 293  (REWRITE_TAC[ARITH_RULE `SUC 1 = 2`;TRUNCATE_SIMPLEX_EXPLICIT_2;HD]);
 294  (REPEAT AP_TERM_TAC);
 295  (REWRITE_TAC[ARITH_RULE `1 = SUC 0`; OMEGA_LIST_N;HD]);
 296  (REWRITE_TAC[ARITH_RULE `SUC 0 = 1`;TRUNCATE_SIMPLEX_EXPLICIT_1;HD])]);;
 297
 298
 299 (* -------------------------------------------------------------------------- *)
 300
 301 (* -------------------------------------------------------------------------- *)
 302 let OMEGA_LIST_0_EXPLICIT = prove_by_refinement (
 303  `!a:real^3 b c V ul.
 304      saturated V /\
 305      packing V /\
 306      ul IN barV V 3 /\
 307      hl ul < sqrt (&2) /\
 308      ul = [a; b; c; d]
 309      ==> omega_list_n V ul 0 = a`,
 310 [ (REPEAT STRIP_TAC);
 311  (REWRITE_TAC[OMEGA_LIST_N]);
 312  (ASM_MESON_TAC[HD])]);;
 313
 314
 315 (* -------------------------------------------------------------------------- *)
 316
 317 let OMEGA_LIST_1_EXPLICIT = prove_by_refinement (
 318  `!a:real^3 b c d V ul.
 319      saturated V /\
 320      packing V /\
 321      ul IN barV V 3 /\
 322      hl ul < sqrt (&2) /\
 323      ul = [a; b; c; d]
 324      ==> omega_list_n V ul 1 = circumcenter {a, b}`,
 325 [ (REPEAT STRIP_TAC);
 326  (REWRITE_WITH `{a,b} = set_of_list [a;(b:real^3)]`);
 327  (MESON_TAC[set_of_list]);
 328  (REWRITE_WITH `circumcenter (set_of_list [a; b:real^3]) = omega_list V [a:real^3; b]`);
 329  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 330  (MATCH_MP_TAC XNHPWAB1);
 331  (EXISTS_TAC `1`);
 332  (ASM_REWRITE_TAC[ARITH_RULE `1 <= 3`]);
 333  (MP_TAC (ASSUME `ul IN barV V 3`) THEN REWRITE_TAC[IN;BARV]);
 334
 335  (REPEAT STRIP_TAC);
 336  (REWRITE_TAC[LENGTH;ARITH_RULE `SUC (SUC 0) = 1 + 1`]);
 337  (NEW_GOAL `initial_sublist vl (ul:(real^3)list)`);
 338  (UNDISCH_TAC `initial_sublist vl [a:real^3; b]`);
 339  (REWRITE_TAC[INITIAL_SUBLIST] THEN STRIP_TAC);
 340  (EXISTS_TAC `APPEND yl [c;d:real^3]`);
 341  (REWRITE_TAC[APPEND_ASSOC; GSYM (ASSUME `[a:real^3; b] = APPEND vl yl`)]);
 342  (ASM_REWRITE_TAC[APPEND]);
 343  (ASM_MESON_TAC[]);
 344  (MATCH_MP_TAC (REAL_ARITH `hl (ul:(real^3)list) < b /\ a < hl ul ==> a < b`));
 345  (ASM_REWRITE_TAC[]);
 346  (REWRITE_WITH `[a;b:real^3] = truncate_simplex 1 ul`);
 347  (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);
 348  (REWRITE_WITH `[a;b;c;d:real^3] = truncate_simplex 3 ul`);
 349  (ASM_MESON_TAC[TRUNCATE_SIMPLEX_EXPLICIT_3]);
 350  (NEW_GOAL `!i j.  i < j /\ j <= 3
 351                      ==> hl (truncate_simplex i (ul:(real^3)list))
 352                        < hl (truncate_simplex j ul)`);
 353  (MATCH_MP_TAC XNHPWAB4);
 354  (EXISTS_TAC `V:real^3->bool`);
 355  (ASM_REWRITE_TAC[]);
 356  (FIRST_ASSUM MATCH_MP_TAC);
 357  (ARITH_TAC);
 358  (ASM_REWRITE_TAC[OMEGA_LIST_TRUNCATE_1])]);;
 359
 360 (* -------------------------------------------------------------------------- *)
 361
 362 let OMEGA_LIST_2_EXPLICIT = prove_by_refinement (
 363  `!a:real^3 b c d V ul.
 364      saturated V /\
 365      packing V /\
 366      ul IN barV V 3 /\
 367      hl ul < sqrt (&2) /\
 368      ul = [a; b; c; d]
 369      ==> omega_list_n V ul 2 = circumcenter {a, b , c}`,
 370 [ (REPEAT STRIP_TAC);
 371  (REWRITE_WITH `{a,b, c} = set_of_list [a;(b:real^3);c]`);
 372  (MESON_TAC[set_of_list]);
 373  (REWRITE_WITH `circumcenter (set_of_list [a; b:real^3;c]) = omega_list V [a;b;c]`);
 374  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 375  (MATCH_MP_TAC XNHPWAB1);
 376  (EXISTS_TAC `2`);
 377  (ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]);
 378  (MP_TAC (ASSUME `ul IN barV V 3`) THEN REWRITE_TAC[IN;BARV]);
 379  (REPEAT STRIP_TAC);
 380  (REWRITE_TAC[LENGTH;ARITH_RULE `SUC (SUC (SUC 0)) = 2 + 1`]);
 381  (NEW_GOAL `initial_sublist vl (ul:(real^3)list)`);
 382  (UNDISCH_TAC `initial_sublist vl [a:real^3; b;c]`);
 383  (REWRITE_TAC[INITIAL_SUBLIST] THEN STRIP_TAC);
 384  (EXISTS_TAC `APPEND yl [d:real^3]`);
 385  (REWRITE_TAC[APPEND_ASSOC; GSYM (ASSUME `[a:real^3; b; c] = APPEND vl yl`)]);
 386  (ASM_REWRITE_TAC[APPEND]);
 387  (ASM_MESON_TAC[]);
 388  (MATCH_MP_TAC (REAL_ARITH `hl (ul:(real^3)list) < b /\ a < hl ul ==> a < b`));
 389  (ASM_REWRITE_TAC[]);
 390  (REWRITE_WITH `[a;b:real^3;c] = truncate_simplex 2 ul`);
 391  (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
 392  (REWRITE_WITH `[a;b;c;d:real^3] = truncate_simplex 3 ul`);
 393  (ASM_MESON_TAC[TRUNCATE_SIMPLEX_EXPLICIT_3]);
 394
 395  (NEW_GOAL `!i j.  i < j /\ j <= 3
 396                      ==> hl (truncate_simplex i (ul:(real^3)list))
 397                        < hl (truncate_simplex j ul)`);
 398  (MATCH_MP_TAC XNHPWAB4);
 399  (EXISTS_TAC `V:real^3->bool`);
 400  (ASM_REWRITE_TAC[]);
 401  (FIRST_ASSUM MATCH_MP_TAC);
 402  (ARITH_TAC);
 403  (ASM_REWRITE_TAC[OMEGA_LIST_TRUNCATE_2])]);;
 404
 405
 406 (* -------------------------------------------------------------------------- *)
 407
 408
 409 let OMEGA_LIST_3_EXPLICIT = prove_by_refinement (
 410  `!a:real^3 b c d V ul.
 411      saturated V /\
 412      packing V /\
 413      ul IN barV V 3 /\
 414      hl ul < sqrt (&2) /\
 415      ul = [a; b; c; d]
 416      ==> omega_list_n V ul 3 = circumcenter {a, b , c, d}`,
 417 [ (REPEAT STRIP_TAC);
 418  (REWRITE_WITH `{a,b, c,d} = set_of_list [a;(b:real^3);c;d]`);
 419  (MESON_TAC[set_of_list]);
 420  (REWRITE_WITH `circumcenter (set_of_list [a; b:real^3;c;d]) = omega_list V [a;b;c;d]`);
 421  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 422  (MATCH_MP_TAC XNHPWAB1);
 423  (EXISTS_TAC `3`);
 424  (ASM_REWRITE_TAC[ARITH_RULE `3 <= 3`]);
 425  (ASM_MESON_TAC[]);
 426  (REWRITE_TAC[OMEGA_LIST]);
 427  (REWRITE_WITH `LENGTH [a:real^3; b; c; d] - 1 = 3`);
 428  (REWRITE_TAC[LENGTH]);
 429  (ARITH_TAC);
 430  (ASM_REWRITE_TAC[])]);;
 431
 432
 433 (* ------------------------------------------------------------------------- *)
 434
 435 let BARV_3_EXPLICIT = prove_by_refinement (
 436  `!V vl. barV V 3 vl ==> ? u0 u1 u2 u3. vl = [u0;u1;u2;u3]`,
 437 [(REPEAT GEN_TAC);
 438  (REWRITE_TAC[BARV]);
 439  (REPEAT STRIP_TAC);
 440  (NEW_GOAL `?x0 xl. (vl:(real^3)list) = CONS x0 xl /\ LENGTH xl = 3`);
 441  (REWRITE_TAC[GSYM LENGTH_EQ_CONS]);
 442  (ASM_ARITH_TAC);
 443  (FIRST_X_ASSUM CHOOSE_TAC);
 444  (FIRST_X_ASSUM CHOOSE_TAC);
 445  (EXISTS_TAC `x0:real^3`);
 446
 447  (NEW_GOAL `?x1 yl. (xl:(real^3)list) = CONS x1 yl /\ LENGTH yl = 2`);
 448  (REWRITE_TAC[GSYM LENGTH_EQ_CONS]);
 449  (ASM_ARITH_TAC);
 450  (FIRST_X_ASSUM CHOOSE_TAC);
 451  (FIRST_X_ASSUM CHOOSE_TAC);
 452  (EXISTS_TAC `x1:real^3`);
 453
 454  (NEW_GOAL `?x2 zl. (yl:(real^3)list) = CONS x2 zl /\ LENGTH zl = 1`);
 455  (REWRITE_TAC[GSYM LENGTH_EQ_CONS]);
 456  (ASM_ARITH_TAC);
 457  (FIRST_X_ASSUM CHOOSE_TAC);
 458  (FIRST_X_ASSUM CHOOSE_TAC);
 459  (EXISTS_TAC `x2:real^3`);
 460
 461  (NEW_GOAL `?x3 tl. (zl:(real^3)list) = CONS x3 tl /\ LENGTH tl = 0`);
 462  (REWRITE_TAC[GSYM LENGTH_EQ_CONS]);
 463  (ASM_ARITH_TAC);
 464  (FIRST_X_ASSUM CHOOSE_TAC);
 465  (FIRST_X_ASSUM CHOOSE_TAC);
 466  (EXISTS_TAC `x3:real^3`);
 467
 468  (NEW_GOAL `(tl:(real^3)list) = []`);
 469  (ASM_MESON_TAC[LENGTH_EQ_NIL]);
 470  (ASM_REWRITE_TAC[])]);;
 471
 472
 473 (* ------------------------------------------------------------------------- *)
 474
 475 let BARV_K_EXPLICIT = prove_by_refinement (
 476  `!V a b c d.
 477      barV V 3 [a; b; c; d]
 478      ==> barV V 2 [a; b; c] /\ barV V 1 [a; b] /\ barV V 0 [a]`,
 479 [ (REPEAT GEN_TAC);
 480  (REWRITE_TAC[BARV]);
 481  (REPEAT STRIP_TAC);
 482  (REWRITE_TAC[LENGTH;ARITH_RULE `SUC (SUC (SUC 0)) = 2 + 1`]);
 483  (MATCH_MP_TAC (ASSUME
 484   `!vl. initial_sublist vl [a:real^3; b; c; d] /\ 0 < LENGTH vl
 485            ==> voronoi_nondg V vl`));
 486  (ASM_REWRITE_TAC[]);
 487  (UNDISCH_TAC `initial_sublist vl [a; b; c:real^3]` THEN
 488    REWRITE_TAC[INITIAL_SUBLIST]);
 489  (STRIP_TAC);
 490  (EXISTS_TAC `APPEND yl [d:real^3]`);
 491  (REWRITE_TAC[APPEND_ASSOC; GSYM (ASSUME `[a; b; c:real^3] = APPEND vl yl`)]);
 492  (REWRITE_TAC[APPEND]);
 493  (REWRITE_TAC[LENGTH]);
 494  (ARITH_TAC);
 495
 496  (MATCH_MP_TAC (ASSUME
 497   `!vl. initial_sublist vl [a:real^3; b; c; d] /\ 0 < LENGTH vl
 498            ==> voronoi_nondg V vl`));
 499  (ASM_REWRITE_TAC[]);
 500  (UNDISCH_TAC `initial_sublist vl [a; b:real^3]` THEN
 501    REWRITE_TAC[INITIAL_SUBLIST]);
 502  (STRIP_TAC);
 503  (EXISTS_TAC `APPEND yl [c;d:real^3]`);
 504  (REWRITE_TAC[APPEND_ASSOC; GSYM (ASSUME `[a; b:real^3] = APPEND vl yl`)]);
 505  (REWRITE_TAC[APPEND]);
 506  (REWRITE_TAC[LENGTH]);
 507  (ARITH_TAC);
 508
 509  (MATCH_MP_TAC (ASSUME
 510   `!vl. initial_sublist vl [a:real^3; b; c; d] /\ 0 < LENGTH vl
 511            ==> voronoi_nondg V vl`));
 512  (ASM_REWRITE_TAC[]);
 513  (UNDISCH_TAC `initial_sublist vl [a:real^3]` THEN
 514    REWRITE_TAC[INITIAL_SUBLIST]);
 515  (STRIP_TAC);
 516  (EXISTS_TAC `APPEND yl [b;c;d:real^3]`);
 517  (REWRITE_TAC[APPEND_ASSOC; GSYM (ASSUME `[a:real^3] = APPEND vl yl`)]);
 518  (REWRITE_TAC[APPEND])]);;
 519
 520
 521 (* ------------------------------------------------------------------------- *)
 522
 523 let AFF_DIM_LE_LENGTH = prove_by_refinement (
 524  `!xl n. LENGTH xl = n ==> aff_dim (set_of_list (xl:(real^3)list)) < &n`,
 525 [ (REPEAT GEN_TAC THEN DISCH_TAC);
 526  (ABBREV_TAC `s = set_of_list (xl:(real^3)list)`);
 527  (NEW_GOAL `?b. ~affine_dependent b /\ b SUBSET (s:real^3->bool) /\
 528                  affine hull b = affine hull s`);
 529  (MESON_TAC[AFFINE_BASIS_EXISTS]);
 530  (FIRST_X_ASSUM CHOOSE_TAC);
 531  (NEW_GOAL `aff_dim (s:real^3->bool) = aff_dim (b:real^3->bool)`);
 532  (REWRITE_WITH `aff_dim (s:real^3->bool) = aff_dim (affine hull s) /\
 533                  aff_dim (b:real^3->bool) = aff_dim (affine hull b)`);
 534  (MESON_TAC[AFF_DIM_AFFINE_HULL]);
 535  (ASM_REWRITE_TAC[]);
 536  (NEW_GOAL `aff_dim (b:real^3->bool) = &(CARD b) - &1`);
 537  (ASM_SIMP_TAC[AFF_DIM_AFFINE_INDEPENDENT]);
 538  (NEW_GOAL `int_of_num (CARD (b:real^3->bool))
 539             <= int_of_num (CARD (s:real^3->bool))`);
 540  (MATCH_MP_TAC (ARITH_RULE `a <= b ==> int_of_num a <= int_of_num b`));
 541  (MATCH_MP_TAC CARD_SUBSET);
 542  (ASM_REWRITE_TAC[]);
 543  (EXPAND_TAC "s");
 544  (REWRITE_TAC[FINITE_SET_OF_LIST]);
 545
 546  (NEW_GOAL `int_of_num (CARD  (s:real^3->bool))
 547           <= int_of_num (LENGTH (xl:(real^3)list))`);
 548  (MATCH_MP_TAC (ARITH_RULE `a <= b ==> int_of_num a <= int_of_num b`));
 549  (EXPAND_TAC "s");
 550  (REWRITE_TAC[CARD_SET_OF_LIST_LE]);
 551  (ASM_ARITH_TAC) ]);;
 552
 553
 554 (* ------------------------------------------------------------------------ *)
 555
 556 let CONVEX_HULL_SUBSET = prove_by_refinement (
 557  `!S (S':real^N->bool).
 558      S SUBSET S' ==> (convex hull S) SUBSET (convex hull S')` ,
 559 [(REWRITE_TAC[SUBSET;convex;hull;IN;IN_ELIM_THM;INTERS]);
 560  (REPEAT STRIP_TAC);
 561  (NEW_GOAL `!x. S (x:real^N) ==> u x`);
 562  (ASM_MESON_TAC[]);
 563  (UP_ASM_TAC THEN DEL_TAC THEN UP_ASM_TAC THEN UP_ASM_TAC THEN DEL_TAC);
 564  (DISCH_THEN (LABEL_TAC "asm1"));
 565  (USE_THEN "asm1" (MP_TAC o SPEC `u:real^N->bool`) THEN DEL_TAC);
 566  (DISCH_TAC THEN DISCH_TAC THEN SWITCH_TAC THEN DISCH_TAC THEN SWITCH_TAC);
 567  (FIRST_X_ASSUM MATCH_MP_TAC);
 568  (ASM_REWRITE_TAC[])]);;
 569
 570
 571 (* ------------------------------------------------------------------------- *)
 572
 573 let BALL_CONVEX_HULL_LEMMA = prove_by_refinement (
 574  `!S s r x:real^N.
 575          (!x. S x ==> dist (s,x) < r)
 576          ==> (convex hull S) x
 577          ==> dist (s,x) < r`,
 578 [ (REPEAT STRIP_TAC);
 579  (NEW_GOAL `S SUBSET ball (s:real^N, r)`);
 580  (ASM_REWRITE_TAC[ball;SUBSET;IN;IN_ELIM_THM]);
 581  (NEW_GOAL `(convex hull S) SUBSET ball (s:real^N, r)`);
 582  (NEW_GOAL `convex hull ball(s:real^N,r) = ball (s,r)`);
 583  (REWRITE_TAC[CONVEX_HULL_EQ;CONVEX_BALL]);
 584  (ASM_MESON_TAC[CONVEX_HULL_SUBSET]);
 585  (REWRITE_WITH `!a x r. dist (a,x:real^N) < r <=> x IN ball(a,r)`);
 586  (REWRITE_TAC[IN;IN_ELIM_THM;ball] );
 587  (ASM_SET_TAC[])]);;
 588
 589
 590 (* ------------------------------------------------------------------------- *)
 591
 592 let CONVEX_RCONE_GT = prove_by_refinement (
 593  `!a:real^N b r. &0 <= r ==> convex (rcone_gt a b r)`,
 594 [ (REPEAT STRIP_TAC);
 595  (REWRITE_TAC[rcone_gt;convex;rconesgn;IN;IN_ELIM_THM]);
 596  (REPEAT STRIP_TAC);
 597  (REWRITE_WITH `(u % x + v % y) - a = u % (x - a) + v % (y - a:real^N)`);
 598  (ASM_REWRITE_TAC[VECTOR_SUB_LDISTRIB; VECTOR_MUL_LID;
 599   VECTOR_ARITH `a - x % b + c - y % b = (a + c) - (x + y) % b`]);
 600  (REWRITE_TAC[DOT_LADD;DOT_LMUL]);
 601  (ASM_CASES_TAC `&0 < u`);
 602
 603   (* 2 Subgoals *)
 604
 605  (NEW_GOAL
 606   `u * ((x:real^N - a) dot (b - a)) + v * ((y - a) dot (b - a)) >
 607    u * dist (x,a) * dist (b,a) * r + v *  dist (y,a) * dist (b,a) * r`);
 608    (* Subgoal 1.1 *)
 609
 610  (NEW_GOAL
 611   `u * ((x:real^N - a) dot (b - a)) > u * dist (x,a) * dist (b,a) * r`);
 612  (MATCH_MP_TAC (REAL_ARITH `&0 < a - b ==> a > b`));
 613  (REWRITE_TAC[REAL_ARITH `a * b * c * d = a * (b * c * d)`;
 614                REAL_ARITH `a * b - a * c = a * (b - c)`]);
 615  (MATCH_MP_TAC REAL_LT_MUL);
 616  (ASM_REAL_ARITH_TAC);
 617
 618  (NEW_GOAL
 619   `v * ((y:real^N - a) dot (b - a)) >= v * dist (y,a) * dist (b,a) * r`);
 620  (MATCH_MP_TAC (REAL_ARITH `&0 <= a - b ==> a >= b`));
 621  (REWRITE_TAC[REAL_ARITH `a * b * c * d = a * (b * c * d)`;
 622                REAL_ARITH `a * b - a * c = a * (b - c)`]);
 623  (MATCH_MP_TAC REAL_LE_MUL);
 624  (ASM_REAL_ARITH_TAC);
 625  (ASM_REAL_ARITH_TAC);
 626
 627  (NEW_GOAL
 628 `dist (u % x + v % y,a) * dist (b,a:real^N) * r <=
 629  u * dist (x,a) * dist (b,a) * r + v *  dist (y,a) * dist (b,a) * r`);
 630    (* Subgoal 1.2 *)
 631
 632  (MATCH_MP_TAC (REAL_ARITH `&0 <= a - b ==> b <= a`));
 633  (REWRITE_TAC[REAL_ARITH `(a * b * x + c * d * x) - e * x  =
 634                             (a * b + c * d - e) * x`]);
 635  (MATCH_MP_TAC REAL_LE_MUL);
 636  STRIP_TAC;
 637  (REWRITE_TAC[dist]);
 638  (REWRITE_WITH `(u % x + v % y) - a = u % (x - a) + v % (y - a:real^N)`);
 639  (ASM_REWRITE_TAC[VECTOR_SUB_LDISTRIB; VECTOR_MUL_LID;
 640    VECTOR_ARITH `a - x % b + c - y % b = (a + c) - (x + y) % b`]);
 641  (REWRITE_TAC[REAL_ARITH `&0 <= a + b - c <=> c <= a + b`]);
 642  (MATCH_MP_TAC (REAL_ARITH
 643   `m <= norm (u % (x - a:real^N)) + norm (v % (y - a)) /\
 644    norm (u % (x - a)) = b /\
 645    norm (v % (y - a)) = c ==> m <= b + c`));
 646  (REWRITE_TAC[NORM_TRIANGLE;NORM_MUL]);
 647  (REWRITE_WITH `abs u = u /\ abs v = v`);
 648  (ASM_SIMP_TAC[REAL_ABS_REFL]);
 649
 650  (MATCH_MP_TAC REAL_LE_MUL);
 651  (ASM_REWRITE_TAC[DIST_POS_LE]);
 652  (ASM_REAL_ARITH_TAC);
 653
 654 (* Subgoal 2 *)
 655
 656  (NEW_GOAL `u = &0`);
 657  (ASM_REAL_ARITH_TAC);
 658  (NEW_GOAL `v = &1`);
 659  (ASM_REAL_ARITH_TAC);
 660  (ASM_REWRITE_TAC[REAL_MUL_LZERO;REAL_ADD_LID;REAL_MUL_LID]);
 661  (ASM_REWRITE_TAC[VECTOR_MUL_LZERO;VECTOR_ADD_LID;VECTOR_MUL_LID])]);;
 662
 663
 664
 665 (* ------------------------------------------------------------------------- *)
 666
 667 let RCONE_GT_CONVEX_HULL_LEMMA = prove_by_refinement (
 668  `!a:real^N b r s.
 669  (s SUBSET rcone_gt a b r) /\ &0 <= r ==>
 670  (convex hull s SUBSET rcone_gt a b r)`,
 671 [ (REPEAT STRIP_TAC);
 672  (ASM_MESON_TAC[CONVEX_HULL_SUBSET;CONVEX_RCONE_GT; CONVEX_HULL_EQ])]);;
 673
 674
 675
 676 end;;