legacy/oldpacking/ky_packing/UPFZBZM_support_lemmas.hl

   1
   2 (* ========================================================================= *)
   3 (*                FLYSPECK - BOOK FORMALIZATION                              *)
   4 (*                                                                           *)
   5 (*      Authour   : VU KHAC KY                                               *)
   6 (*      Book lemma: UPFZBZM                                                  *)
   7 (*      Chaper    : Packing (Clusters)                                       *)
   8 (*      Date      : October 3, 2010                                          *)
   9 (*                                                                           *)
  10 (* ========================================================================= *)
  11
  12 (* ========================================================================= *)
  13 (*      Supporting lemmas for UPFZBZM                                        *)
  14 (*      Chaper    : Packing (Clusters)                                       *)
  15 (*                                                                           *)
  16 (* ========================================================================= *)
  17
  18 (* ========================================================================= *)
  19 (*                     FILES NEED TO BE LOADED                               *)
  20 (* ========================================================================= *)
  21
  22
  23 flyspeck_needs "nonlinear/vukhacky_tactics.hl";;
  24 flyspeck_needs "packing/pack_defs.hl";;
  25 flyspeck_needs "packing/pack_concl.hl";;
  26 flyspeck_needs "packing/beta_pair_thm.hl";;
  27 (* Loading the list of unproved lemmas *)
  28
  29 flyspeck_needs "packing/ky/UPFZBZM_axioms.hl";;
  30
  31 module UPFZBZM_support_lemmas.hl
  32
  33 open Pack_defs;;
  34 open Pack_concl;;
  35 open Vukhacky_tactics;;
  36
  37 (*-------------------------------------------------------------------------- *)
  38
  39  let UPFZBZM_concl =
  40    `!V.  saturated V /\ packing V /\ cell_cluster_estimate V /\
  41          marchal_inequality /\
  42          lmfun_inequality V ==>
  43     (?G. negligible_fun_0 G V /\ fcc_compatible G V)`;;
  44
  45 (* ------------------------------------------------------------------------- *)
  46
  47
  48 (* ========================================================================= *)
  49 (*                 SOME COMPLEMENTARY LEMMAS                                 *)
  50 (* ========================================================================= *)
  51 (* Lemma 1 *)
  52
  53  let john_harrison_lemma1 = prove
  54   (`(\(x,y). P x y) = (\p. P (FST p) (SND p))`,
  55    REWRITE_TAC[FUN_EQ_THM; FORALL_PAIR_THM]);;
  56
  57  let john_harrison_lemma2 = MESON[] `(?x. P x) /\ (@x. P x) = a ==> P a`;;
  58
  59  let JOHN_SELECT_THM = prove
  60   (`(?x y. P x /\ Q y /\ R x y) /\
  61     (@(x,y). P x /\ Q y /\ R x y) = (a,b)
  62     ==> P a /\ Q b /\ R a b`,
  63    REWRITE_TAC[GSYM EXISTS_PAIRED_THM] THEN
  64    REWRITE_TAC[john_harrison_lemma1] THEN
  65    DISCH_THEN(MP_TAC o MATCH_MP john_harrison_lemma2) THEN
  66    REWRITE_TAC[FST; SND]);;
  67
  68 (* ------------------------------------------------------------------------- *)
  69 (* Lemma 2 *)
  70
  71 let SQRT_RULE_Euler_lemma = prove
  72  (`!x y. x pow 2 = y /\ &0 <= x ==> x = sqrt y`,
  73  REPEAT STRIP_TAC THEN
  74  REWRITE_TAC[GSYM (ASSUME `x pow 2 = y`);REAL_POW_2] THEN
  75  ASM_SIMP_TAC[SQRT_MUL] THEN
  76  ASM_MESON_TAC[GSYM REAL_POW_2;SQRT_POW_2]);;
  77
  78 let  SQRT_OF_32_lemma = prove_by_refinement (
  79  `sqrt (&32) = &8 * sqrt (&1 / &2)`,
  80   [ (REWRITE_WITH `&8 = sqrt (&64)`);
  81    (MATCH_MP_TAC SQRT_RULE_Euler_lemma);
  82    (REAL_ARITH_TAC);
  83    (REWRITE_TAC[REAL_ARITH `&32 = &64 * (&1 / &2)`]);
  84    (MATCH_MP_TAC SQRT_MUL);
  85    (REAL_ARITH_TAC)]);;
  86
  87 (* ------------------------------------------------------------------------- *)
  88 (* Lemma 3 *)
  89
  90 let m1_minus_12m2 = prove_by_refinement (
  91  `mm1 - &12 * mm2 = sqrt (&1 / &2)`,
  92
  93 [ (REWRITE_TAC[mm1;mm2]);
  94  (REWRITE_TAC [REAL_ARITH `a * (b / c) = (a * b) / c`]);
  95  (REWRITE_WITH
  96  `&12 * (&6 * sol0 - pi) * sqrt (&2) = ((&6 * sol0 - pi) * sqrt (&8)) * &6`);
  97  (REWRITE_TAC[REAL_ARITH`&12 * a * b = (a * &2 * b) * &6`]);
  98  (MATCH_MP_TAC (MESON[REAL_EQ_MUL_RCANCEL] `a = b ==> a * x = b * x`));
  99  (MATCH_MP_TAC (MESON[REAL_EQ_MUL_LCANCEL] `a = b ==> x * a = x * b`));
 100
 101  (REWRITE_TAC[REAL_ARITH `&8 = &4 * &2`]);
 102  (REWRITE_WITH `sqrt (&4 * &2) = sqrt (&4) * sqrt (&2)`);
 103  (MATCH_MP_TAC SQRT_MUL);
 104  (REAL_ARITH_TAC);
 105  (MATCH_MP_TAC (MESON[REAL_EQ_MUL_RCANCEL] `a = b ==> a * x = b * x`));
 106  (MATCH_MP_TAC SQRT_RULE_Euler_lemma);
 107  (REAL_ARITH_TAC);
 108  (REWRITE_TAC[REAL_ARITH `(m * &6) / (&6 * tau0) = m * &6 / (tau0 * &6)`]);
 109  (REWRITE_WITH `((&6 * sol0 - pi) * sqrt (&8)) * &6 / (tau0 * &6) =
 110  ((&6 * sol0 - pi) * sqrt (&8)) / tau0`);
 111  (MATCH_MP_TAC REDUCE_WITH_DIV_Euler_lemma);
 112  (REWRITE_TAC[REAL_ARITH `~(&6 = &0)`;tau0_not_zero]);
 113
 114  (REWRITE_TAC[REAL_ARITH `a / b - c / b = (a - c) / b`]);
 115  (REWRITE_TAC[REAL_ARITH `a * x - b * x = (a - b) * x`]);
 116  (REWRITE_WITH `sol0 - (&6 * sol0 - pi) = tau0 / &4`);
 117  (REWRITE_TAC[tau0]);
 118  (REAL_ARITH_TAC);
 119
 120  (REWRITE_TAC[REAL_ARITH
 121   `(tau0 / &4 * x) / tau0 = (tau0 / tau0) * (x / &4)`]);
 122  (REWRITE_WITH `sqrt (&8) / &4 = sqrt (&1 / &2)`);
 123  (REWRITE_TAC[REAL_ARITH `&1 / &2 = &8 / &16`]);
 124  (REWRITE_WITH `sqrt (&8 / &16) = sqrt (&8) / sqrt (&16)`);
 125  (MATCH_MP_TAC SQRT_DIV THEN REAL_ARITH_TAC);
 126  (REWRITE_WITH `sqrt (&16) = &4`);
 127
 128  (MATCH_MP_TAC (MESON[] `a = b ==> b = a`));
 129  (MATCH_MP_TAC SQRT_RULE_Euler_lemma THEN REAL_ARITH_TAC);
 130  (MATCH_MP_TAC (MESON[REAL_MUL_LID] `x = &1 ==> x * y = y`));
 131  (MATCH_MP_TAC REAL_DIV_REFL);
 132  (REWRITE_TAC[tau0_not_zero])]);;
 133
 134
 135 (* ------------------------------------------------------------------------- *)
 136 (* Lemma 4 *)
 137
 138 let ZERO_LE_MM2_LEMMA =
 139    MATCH_MP (REAL_ARITH `&0 < x ==> &0 <= x`) ZERO_LT_MM2_LEMMA;;
 140
 141 (* ------------------------------------------------------------------------- *)
 142 (* Lemma 5 *)
 143
 144 let FINITE_edgeX = prove_by_refinement (
 145  `!V X. FINITE (edgeX V X)`,
 146 [(REPEAT GEN_TAC THEN REWRITE_TAC[edgeX;VX]);
 147  (COND_CASES_TAC);
 148 (* Break into 2 subgoal *)
 149
 150 (REWRITE_WITH `{{u:real^3, v} | {} u /\ {} v /\ ~(u = v)} = {}`);
 151 (* New Subgoal 1.1 *)
 152 (SET_TAC[]);  (*  End subgoal 1.1 *)
 153 (MESON_TAC[FINITE_CASES]);  (* End Subgoal 1 *)
 154 (REPEAT LET_TAC);
 155 (SUBGOAL_THEN
 156    `FINITE (set_of_list (truncate_simplex (k - 1) (ul:(real^3)list)))`
 157    ASSUME_TAC);
 158 (REWRITE_TAC[FINITE_SET_OF_LIST]);
 159 (ABBREV_TAC `S = set_of_list (truncate_simplex (k - 1) (ul:(real^3)list))`);
 160 (MATCH_MP_TAC FINITE_SUBSET);
 161 (EXISTS_TAC `{t:real^3->bool | t SUBSET S}`);
 162 (STRIP_TAC);
 163 (ASM_MESON_TAC[FINITE_POWERSET]);
 164 (REWRITE_TAC[SUBSET;IN_ELIM_THM]);
 165 (REPEAT STRIP_TAC);
 166 (REPLICATE_TAC 5 UP_ASM_TAC);
 167 (SET_TAC[])]);;
 168
 169
 170 (* ------------------------------------------------------------------------- *)
 171 (* Lemma 6 *)
 172
 173 let FINITE_critical_edgeX = prove_by_refinement (
 174  `!V X. FINITE (critical_edgeX V X)`,
 175 [(REPEAT STRIP_TAC);
 176  (REWRITE_TAC[critical_edgeX]);
 177  (REWRITE_WITH
 178   `{{u:real^3, v} | {u, v} IN edgeX V X /\ hminus <= hl [u; v] /\
 179                      hl [u; v] <= hplus} =
 180    {{u, v} | hminus <= hl [u; v] /\ hl [u; v] <= hplus} INTER (edgeX V X)`);
 181  (REPEAT GEN_TAC THEN SET_TAC[]);
 182  (MESON_TAC[FINITE_edgeX;FINITE_INTER])]);;
 183
 184
 185 (* ------------------------------------------------------------------------- *)
 186 (* Lemma 7 *)
 187
 188 let DIHV_LE_0 = prove_by_refinement (
 189  `!x:real^N y z t.  &0 <= dihV x y z t`,
 190 [ (REPEAT GEN_TAC THEN REWRITE_TAC[dihV]);
 191  (REPEAT LET_TAC THEN REWRITE_TAC[arcV]);
 192  (MATCH_MP_TAC (MESON[] `&0 <= acs y /\ acs y <= pi ==> &0 <= acs y`));
 193  (MATCH_MP_TAC ACS);
 194  (REWRITE_TAC[GSYM REAL_ABS_BOUNDS; NORM_CAUCHY_SCHWARZ_DIV])]);;
 195
 196
 197 (* ------------------------------------------------------------------------- *)
 198 (* Lemma 8 *)
 199
 200 let DIHV_SYM = prove_by_refinement (
 201  `!(x:real^N) y z t. dihV x y z t = dihV y x z t`,
 202 [ (REPEAT GEN_TAC);
 203  (REWRITE_TAC[dihV] THEN REPEAT LET_TAC);
 204  (MATCH_MP_TAC (MESON[]
 205   `!a b c d x. (a = b) /\ (c = d) ==> arcV x a c = arcV x b d`));
 206  (REPEAT STRIP_TAC);
 207   (* Break into 2 subgoals with similar proofs *)
 208
 209   (* Subgoal 1 *)
 210    (EXPAND_TAC "vap'" THEN EXPAND_TAC "vap");
 211
 212      (REWRITE_WITH `(va':real^N) = va - vc`);
 213      (EXPAND_TAC "va'" THEN EXPAND_TAC "va" THEN EXPAND_TAC "vc");
 214      (VECTOR_ARITH_TAC);
 215
 216      (REWRITE_WITH `(vc':real^N) = --vc`);
 217      (EXPAND_TAC "vc'" THEN EXPAND_TAC "vc");
 218      (VECTOR_ARITH_TAC);
 219
 220      (REWRITE_WITH
 221    `(--vc dot --vc) % (va:real^N - vc) = (vc dot vc) % va - (vc dot vc) % vc`);
 222     (REWRITE_TAC[DOT_RNEG;DOT_LNEG;REAL_ARITH `-- --x = x `]);
 223     (VECTOR_ARITH_TAC);
 224
 225   (MATCH_MP_TAC (VECTOR_ARITH `a = b + c ==> x:real^N - b - c = x - a `));
 226   (REWRITE_WITH `((va:real^N - vc) dot --vc) % --vc =
 227                  (va dot vc) % vc - (vc dot vc) % vc`);
 228  (REWRITE_TAC[DOT_RNEG;DOT_LNEG;VECTOR_MUL_LNEG; VECTOR_MUL_RNEG]);
 229  (REWRITE_TAC[VECTOR_NEG_MINUS1;VECTOR_MUL_ASSOC]);
 230  (REWRITE_TAC[REAL_ARITH `-- &1 * -- &1 * x = x`;
 231                DOT_LSUB;VECTOR_SUB_RDISTRIB]);
 232  (VECTOR_ARITH_TAC);
 233
 234    (* Subgoal 2 *)
 235  (EXPAND_TAC "vbp'" THEN EXPAND_TAC "vbp");
 236  (REWRITE_WITH `(vb':real^N) = vb - vc`);
 237  (EXPAND_TAC "vb'" THEN EXPAND_TAC "vb" THEN EXPAND_TAC "vc");
 238  (VECTOR_ARITH_TAC);
 239
 240    (REWRITE_WITH `(vc':real^N) = --vc`);
 241    (EXPAND_TAC "vc'" THEN EXPAND_TAC "vc");
 242    (VECTOR_ARITH_TAC);
 243
 244    (REWRITE_WITH
 245   `(--vc dot --vc) % (vb:real^N - vc) = (vc dot vc) % vb - (vc dot vc) % vc`);
 246    (REWRITE_TAC[DOT_RNEG;DOT_LNEG;REAL_ARITH `-- --x = x `]);
 247    (VECTOR_ARITH_TAC);
 248
 249    (MATCH_MP_TAC (VECTOR_ARITH `a = b + c ==> x:real^N - b - c = x - a `));
 250    (REWRITE_WITH `((vb:real^N - vc) dot --vc) % --vc =
 251                  (vb dot vc) % vc - (vc dot vc) % vc`);
 252    (REWRITE_TAC[DOT_RNEG;DOT_LNEG;VECTOR_MUL_LNEG; VECTOR_MUL_RNEG]);
 253    (REWRITE_TAC[VECTOR_NEG_MINUS1;VECTOR_MUL_ASSOC]);
 254    (REWRITE_TAC[REAL_ARITH `-- &1 * -- &1 * x = x`;
 255                DOT_LSUB;VECTOR_SUB_RDISTRIB]);
 256    (VECTOR_ARITH_TAC)]);;
 257
 258 (* ------------------------------------------------------------------------- *)
 259 (* Lemma 9 *)
 260
 261 let DIHX_POS = prove_by_refinement (
 262  `!u v V X. &0 <= dihX V X (u,v)`,
 263 [(REPEAT GEN_TAC THEN REWRITE_TAC[dihX]);
 264  (COND_CASES_TAC);
 265  REAL_ARITH_TAC;
 266  (LET_TAC THEN COND_CASES_TAC);
 267  (REWRITE_TAC[dihX2] THEN LET_TAC THEN REWRITE_TAC[DIHV_LE_0]);
 268  (COND_CASES_TAC);
 269  (REWRITE_TAC[dihX3] THEN LET_TAC THEN MATCH_MP_TAC (SUM_POS_LE));
 270  STRIP_TAC;
 271
 272  (REWRITE_TAC[left_action_list;TABLE]);
 273  (ABBREV_TAC `P = {p | p permutes {0, 1, 2}}`);
 274  (ABBREV_TAC
 275 `VL = {vl:(real^3)list | ?p. p permutes {0, 1, 2} /\
 276                 vl = REVERSE (REVERSE_TABLE (\i. EL (inverse p i) ul')
 277                     (LENGTH ul')) /\
 278                 u = EL 0 vl /\
 279                 v = EL 1 vl}`);
 280  (MATCH_MP_TAC FINITE_SUBSET);
 281  (EXISTS_TAC `(VL:(real^3)list->bool) CROSS (P: (num->num)->bool)`);
 282  STRIP_TAC;
 283  (MATCH_MP_TAC FINITE_CROSS);
 284  (NEW_GOAL `FINITE (P:(num->num)->bool)`);
 285  (EXPAND_TAC "P");
 286  (REWRITE_TAC[FINITE_PERMUTE_3]);
 287  (ASM_REWRITE_TAC[]);
 288  (EXPAND_TAC "VL");
 289  (MATCH_MP_TAC FINITE_SUBSET);
 290  (ABBREV_TAC
 291   `f = (\(p:num->num). REVERSE (REVERSE_TABLE (\i. EL (inverse p i)
 292                        (ul':(real^3)list)) (LENGTH ul')))`);
 293  (EXISTS_TAC `{vl:(real^3)list | ?p:num->num. p IN P /\ vl = f p}`);
 294  (STRIP_TAC);
 295  (MATCH_MP_TAC FINITE_IMAGE_EXPAND);
 296  (ASM_REWRITE_TAC[]);
 297  (EXPAND_TAC "P" THEN EXPAND_TAC "f");
 298  (REWRITE_TAC[SUBSET;IN;IN_ELIM_THM;BETA_THM]);
 299  (MESON_TAC[]);
 300
 301  (EXPAND_TAC "VL");
 302  (EXPAND_TAC "P");
 303  (REWRITE_TAC[CROSS;IN;IN_ELIM_THM;SUBSET]);
 304  (REPEAT STRIP_TAC);
 305  (EXISTS_TAC `vl:(real^3)list`);
 306  (EXISTS_TAC `p:(num->num)`);
 307  (REPEAT STRIP_TAC);
 308  (EXISTS_TAC `p:(num->num)`);
 309  (ASM_REWRITE_TAC[]);
 310  (ASM_REWRITE_TAC[]);
 311  (ASM_REWRITE_TAC[]);
 312
 313  GEN_TAC;
 314  (REWRITE_TAC[IN_ELIM_THM]);
 315  (DISCH_TAC);
 316  (CHOOSE_TAC (ASSUME `?vl p.
 317          (p permutes {0, 1, 2} /\
 318            vl = left_action_list p ul' /\
 319            u:real^3 = EL 0 vl /\
 320            v = EL 1 vl) /\
 321           x = vl,p`)) ;
 322  (CHOOSE_TAC (ASSUME `?p.
 323           (p permutes {0, 1, 2} /\
 324            vl = left_action_list p ul' /\
 325            u:real^3 = EL 0 vl /\
 326            v = EL 1 vl) /\
 327           x = vl,p`)) ;
 328  (UP_ASM_TAC THEN (REPEAT STRIP_TAC));
 329  (REWRITE_ONLY_TAC (ASSUME `x:(real^3)list#(num->num) = vl,p`));
 330  (REWRITE_TAC[DIHV_LE_0]);
 331  (COND_CASES_TAC);
 332  (REWRITE_TAC[dihX4]);
 333  LET_TAC;
 334  (MATCH_MP_TAC REAL_LE_MUL THEN REWRITE_TAC[REAL_ARITH `&0 <= &1 / &2`]);
 335  (MATCH_MP_TAC SUM_POS_LE);
 336  STRIP_TAC;
 337
 338  (ABBREV_TAC `P = {p | p permutes {0, 1, 2, 3}}`);
 339  (ABBREV_TAC
 340 `VL = {vl:(real^3)list | ?p. p permutes {0, 1, 2, 3} /\
 341                 vl = left_action_list p ul' /\
 342                 u = EL 0 vl /\
 343                 v = EL 1 vl}`);
 344  (MATCH_MP_TAC FINITE_SUBSET);
 345  (EXISTS_TAC `(VL:(real^3)list->bool) CROSS (P: (num->num)->bool)`);
 346  STRIP_TAC;
 347  (MATCH_MP_TAC FINITE_CROSS);
 348  (NEW_GOAL `FINITE (P:(num->num)->bool)`);
 349  (EXPAND_TAC "P");
 350  (REWRITE_TAC[FINITE_PERMUTE_4]);
 351  (ASM_REWRITE_TAC[]);
 352  (EXPAND_TAC "VL");
 353  (MATCH_MP_TAC FINITE_SUBSET);
 354  (ABBREV_TAC
 355   `f = (\(p:num->num). left_action_list p (ul':(real^3)list))`);
 356  (EXISTS_TAC `{vl:(real^3)list | ?p:num->num. p IN P /\ vl = f p}`);
 357  (STRIP_TAC);
 358  (MATCH_MP_TAC FINITE_IMAGE_EXPAND);
 359  (ASM_REWRITE_TAC[]);
 360  (EXPAND_TAC "P" THEN EXPAND_TAC "f");
 361  (REWRITE_TAC[SUBSET;IN;IN_ELIM_THM;BETA_THM]);
 362  (MESON_TAC[]);
 363
 364  (EXPAND_TAC "VL");
 365  (EXPAND_TAC "P");
 366  (REWRITE_TAC[CROSS;IN;IN_ELIM_THM;SUBSET]);
 367  (REPEAT STRIP_TAC);
 368  (EXISTS_TAC `vl:(real^3)list`);
 369  (EXISTS_TAC `p:(num->num)`);
 370  (REPEAT STRIP_TAC);
 371  (EXISTS_TAC `p:(num->num)`);
 372  (ASM_REWRITE_TAC[]);
 373  (ASM_REWRITE_TAC[]);
 374  (ASM_REWRITE_TAC[]);
 375
 376  GEN_TAC;
 377  (REWRITE_TAC[IN_ELIM_THM]);
 378  (DISCH_TAC);
 379  (CHOOSE_TAC (ASSUME `?vl p.
 380           (p permutes {0, 1, 2, 3} /\
 381            vl = left_action_list p ul' /\
 382            u:real^3 = EL 0 vl /\
 383            v = EL 1 vl) /\
 384           x = vl,p`)) ;
 385  (CHOOSE_TAC (ASSUME `?p.
 386           (p permutes {0, 1, 2, 3} /\
 387            vl = left_action_list p ul' /\
 388            u:real^3 = EL 0 vl /\
 389            v = EL 1 vl) /\
 390           x = vl,p`)) ;
 391  (UP_ASM_TAC THEN (REPEAT STRIP_TAC));
 392  (REWRITE_ONLY_TAC (ASSUME `x:(real^3)list#(num->num) = vl,p`));
 393  (REWRITE_TAC[DIHV_LE_0]);
 394  REAL_ARITH_TAC ]);;
 395
 396 (* ------------------------------------------------------------------------- *)
 397 (* Lemma 10 *)
 398
 399 let SUM_SET_OF_2_ELEMENTS = prove_by_refinement (
 400  `!s t f. ~(s = t) ==> sum {s:A,t} f = f s + f t`,
 401 [(REPEAT STRIP_TAC);
 402  (REWRITE_WITH `!s t f. f s = sum{s:A} f /\ f t = sum{t} f`);
 403  (MESON_TAC[SUM_SING]);
 404  (REWRITE_WITH `{s:A, t} = {s} UNION {t}`);
 405  (SET_TAC[]);
 406  (MATCH_MP_TAC SUM_UNION);
 407  (REWRITE_TAC[FINITE_SING]);
 408  (UP_ASM_TAC THEN SET_TAC[])]);;
 409
 410
 411 end;;