text_formalization/packing/UPFZBZM_support_lemmas.hl

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