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