text_formalization/packing/RDWKARC.hl

   1
   2 (* ========================================================================= *)
   3 (*                FLYSPECK - BOOK FORMALIZATION                              *)
   4 (*                                                                           *)
   5 (*      Authour   : VU KHAC KY                                               *)
   6 (*      Book lemma: RDWKARC                                                  *)
   7 (*      Chaper    : Packing (Clusters)                                       *)
   8 (*                                                                           *)
   9 (* ========================================================================= *)
  10 (*                     FILES NEED TO BE LOADED                               *)
  11 (*              UPFZBZM.hl                                                   *)
  12 (* ========================================================================= *)
  13
  14 module Rdwkarc = struct
  15
  16 (*
  17   open Sphere;;
  18   open Pack_defs;;
  19   open Pack_concl;;
  20   open Vukhacky_tactics;;
  21   open Pack1;;
  22 *)
  23
  24 open Sphere;;
  25 open Euler_main_theorem;;
  26 open Pack_defs;;
  27 open Pack_concl;;
  28 open Pack1;;
  29 open Pack2;;
  30 open Packing3;;
  31 open Rogers;;
  32 open Vukhacky_tactics;;
  33 open Marchal_cells;;
  34 open Emnwuus;;
  35 (* open Marchal_cells_2;; *)
  36 open Marchal_cells_2_new;;
  37 open Urrphbz1;;
  38 open Lepjbdj;;
  39 open Hdtfnfz;;
  40 open Rvfxzbu;;
  41 open Sltstlo;;
  42 open Urrphbz2;;
  43 open Urrphbz3;;
  44 open Ynhyjit;;
  45 open Njiutiu;;
  46 open Tezffsk;;
  47 open Qzksykg;;
  48 open Ddzuphj;;
  49 open Ajripqn;;
  50 open Qzyzmjc;;
  51 open Upfzbzm_support_lemmas;;
  52 open Marchal_cells_3;;
  53 open Grutoti;;
  54
  55 open Sum_gammax_lmfun_estimate;;
  56 open Kizhltl;;
  57 open Upfzbzm;;
  58
  59 (*-------------------------------------------------------------------------- *)
  60
  61 (*
  62 let RDWKARC_concl =
  63 `~kepler_conjecture /\ (!V. cell_cluster_estimate_v1 V) /\ TSKAJXY_statement
  64   ==> (?V. packing V /\ V SUBSET ball_annulus /\ ~lmfun_ineq_center V)`;;
  65 *)
  66
  67 (* ------------------------------------------------------------------------- *)
  68 (*   The following lemmas are necessary for the main theorem RDWKARC         *)
  69 (* ------------------------------------------------------------------------- *)
  70
  71 (* Lemma 1 *)
  72 let JGXZYGW_KY = prove_by_refinement (
  73  `!S.   packing S /\
  74          saturated S /\
  75          (?A. fcc_compatible A S /\ negligible_fun_0 A S)
  76          ==> (?c. !r. &1 <= r
  77                       ==> vol
  78                           (UNIONS {ball (v,&1) | v IN S} INTER ball (vec 0,r)) /
  79                           vol (ball (vec 0,r)) <=
  80                           pi / sqrt (&18) + c / r)`,
  81 [(MP_TAC JGXZYGW THEN DISCH_THEN (LABEL_TAC "asm1"));
  82  GEN_TAC;
  83  (REWRITE_TAC[negligible_fun_0]);
  84  (USE_THEN "asm1" (MP_TAC o SPEC `S:real^3->bool`));
  85  (DISCH_THEN (LABEL_TAC "asm2"));
  86  (USE_THEN "asm2" (MP_TAC o SPEC `(vec 0):real^3`));
  87  (MESON_TAC[])]);;
  88
  89 (* ------------------------------------------------------------------------- *)
  90 (*  Lemma 2 *)
  91 let PACKING_SUBSET = prove_by_refinement (
  92  `!V S. packing V /\ S SUBSET V ==> packing S`,
  93 [(REPEAT GEN_TAC THEN REWRITE_TAC[packing;SUBSET;IN_ELIM_THM]);
  94  (REPEAT STRIP_TAC);
  95  (MATCH_MP_TAC(ASSUME
  96     `!u:real^3 v. V u /\ V v /\ ~(u = v) ==> &2 <= dist (u,v)`) );
  97  (ASM_REWRITE_TAC[]);
  98  (REWRITE_WITH `V (u:real^3) /\ V v <=> u IN V /\ v IN V`);
  99  (REWRITE_TAC[IN]);
 100  STRIP_TAC;
 101    (* Break into smaller subgoals *)
 102
 103  (MATCH_MP_TAC(ASSUME `!(x:real^3). x IN S ==> x IN V`) );
 104  (ASM_REWRITE_TAC[IN]);
 105  (MATCH_MP_TAC(ASSUME `!(x:real^3). x IN S ==> x IN V`) );
 106  (ASM_REWRITE_TAC[IN])]);;
 107
 108
 109 (* ------------------------------------------------------------------------  *)
 110 (* Lemma 3 *)
 111 let PACKING_TRANS = prove_by_refinement (
 112  `! V (x:real^3). packing V ==> packing {u | (u + x) IN V}`,
 113
 114 [(REPEAT GEN_TAC THEN REWRITE_TAC[packing;IN_ELIM_THM]);
 115 (REPEAT STRIP_TAC);
 116 (ABBREV_TAC `u' = (u:real^3) + x`);
 117 (ABBREV_TAC `v' = (v:real^3) + x`);
 118   (NEW_GOAL `V (u':real^3) /\ V v' /\ ~(u' = v')`);
 119   (* New subgoal 1 *)
 120   (REPEAT STRIP_TAC);
 121   (ASM_REWRITE_TAC[GSYM IN]);
 122   (ASM_REWRITE_TAC[GSYM IN]);
 123   (NEW_GOAL `u = v:real^3`);
 124   (REPLICATE_TAC 3 UP_ASM_TAC );
 125   VECTOR_ARITH_TAC;
 126   (ASM_MESON_TAC[]);
 127   (* End subgoal 1 *)
 128
 129   (REWRITE_WITH `dist (u:real^3, v) = dist (u', v':real^3)`);
 130   (* Subgoal 2 *)
 131   (EXPAND_TAC "u'" THEN EXPAND_TAC "v'");
 132   (REWRITE_TAC[dist]);
 133   (NORM_ARITH_TAC);
 134   (* End subgoal 2 *)
 135
 136 (UP_ASM_TAC THEN ASM_REWRITE_TAC[])]);;
 137
 138
 139 (* ------------------------------------------------------------------------- *)
 140 (* Lemma 4 *)
 141
 142 let SATURATED_TRANS = prove_by_refinement (
 143 `!V (x:real^3). saturated V ==> saturated {u | u + x IN V}`,
 144
 145 [(REPEAT GEN_TAC THEN REWRITE_TAC[saturated]);
 146 (DISCH_THEN (LABEL_TAC "asm1"));
 147 (GEN_TAC);
 148 (USE_THEN "asm1" (MP_TAC  o SPEC `(x':real^3) + x`));
 149 (DEL_TAC THEN DISCH_TAC);
 150 (FIRST_X_ASSUM CHOOSE_TAC);
 151 (EXISTS_TAC `y - (x:real^3)`);
 152 (REWRITE_TAC[IN_ELIM_THM; VECTOR_ARITH `y - x + x = (y:real^3)`]);
 153 (ASM_REWRITE_TAC[]);
 154
 155   (NEW_GOAL `dist (x',y - x) = dist (x'+ x,y:real^3)`);
 156   (* Subgoal 1 *)
 157   (REWRITE_TAC[dist]);
 158   (NORM_ARITH_TAC);
 159   (* End subgoal 1 *)
 160
 161 (ASM_MESON_TAC[])]);;
 162
 163
 164 (* ------------------------------------------------------------------------- *)
 165 (* Lemma 5 *)
 166
 167 let RADV_TRANS_EQ = prove (
 168  `!u v:real^3 x. ~(u = v) ==> radV {u, v} = radV {u + x, v + x}`,
 169    REWRITE_TAC[GSYM set_of_list; GSYM HL; Marchal_cells_3.HL_2] THEN NORM_ARITH_TAC);;
 170
 171 (* ========================================================================= *)
 172 (*                             MAIN THEOREM RDWKARC                          *)
 173 (* ========================================================================= *)
 174
 175
 176 let RDWKARC = prove_by_refinement (Pack_concl.RDWKARC_concl,
 177 [
 178  (REWRITE_TAC[kepler_conjecture]);
 179  (REWRITE_WITH
 180  `~(!V. packing V /\ saturated V
 181         ==> (?c. !r. &1 <= r
 182                     ==> vol
 183                         (UNIONS {ball (v,&1) | v IN V} INTER ball (vec 0,r)) /
 184                         vol (ball (vec 0,r)) <=
 185                         pi / sqrt (&18) + c / r)) <=>
 186  (?V. packing V /\ saturated V
 187         /\ ~(?c. !r. &1 <= r
 188                     ==> vol
 189                         (UNIONS {ball (v,&1) | v IN V} INTER ball (vec 0,r)) /
 190                         vol (ball (vec 0,r)) <=
 191                         pi / sqrt (&18) + c / r))`);
 192
 193  (MESON_TAC[]);
 194  STRIP_TAC;
 195
 196  (NEW_GOAL `~(lmfun_inequality (V:real^3->bool))`);
 197  STRIP_TAC;
 198  (NEW_GOAL `(?G. negligible_fun_0 G V /\ fcc_compatible G V)`);
 199  (ASM_MESON_TAC[Upfzbzm.UPFZBZM]);
 200  (NEW_GOAL `(?c. !r. &1 <= r
 201                 ==> vol (UNIONS {ball (v,&1) | v IN V} INTER ball (vec 0,r)) /
 202                     vol (ball (vec 0,r)) <=
 203                     pi / sqrt (&18) + c / r)`);
 204  (MATCH_MP_TAC JGXZYGW_KY);
 205  (ASM_REWRITE_TAC[]);
 206  (CHOOSE_TAC (ASSUME `?G. negligible_fun_0 G V /\ fcc_compatible G V`));
 207  (EXISTS_TAC `G:real^3->real`);
 208  (ASM_REWRITE_TAC[]);
 209  (ASM_MESON_TAC[]);
 210
 211 (* ---------------------------------------------------------------------- *)
 212
 213  (UP_ASM_TAC THEN REWRITE_TAC[lmfun_inequality]);
 214  (REWRITE_WITH
 215  `~(!u:real^3. u IN V
 216        ==> sum {v | v IN V /\ ~(u = v) /\ dist (u,v) <= &2 * h0}
 217            (\v. lmfun (hl [u; v])) <=
 218            &12) <=>
 219  (?u. u IN V
 220        /\ ~(sum {v | v IN V /\ ~(u = v) /\ dist (u,v) <= &2 * h0}
 221            (\v. lmfun (hl [u; v])) <=
 222            &12))`);
 223  (MESON_TAC[]);
 224  (REWRITE_TAC[REAL_ARITH `~(a <= b) <=> b < a`]);
 225  (DISCH_TAC);
 226  (FIRST_X_ASSUM CHOOSE_TAC);
 227
 228
 229  (ABBREV_TAC `V' = {v:real^3 | v + u IN V}`);
 230  (EXISTS_TAC `V':real^3->bool INTER ball_annulus`);
 231  (ASM_REWRITE_TAC[INTER_SUBSET]);
 232
 233  (NEW_GOAL `packing (V':real^3->bool)`);
 234  (EXPAND_TAC "V'" THEN ASM_MESON_TAC[PACKING_TRANS]);
 235  STRIP_TAC;
 236  (ASM_MESON_TAC[PACKING_SUBSET;INTER_SUBSET]);
 237
 238 (* -------------------------------------------------------------------------- *)
 239
 240  (REWRITE_TAC[lmfun_ineq_center]);
 241  (REWRITE_TAC[REAL_ARITH `~(a <= b) <=> b < a`]);
 242  (EXPAND_TAC "V'" THEN REWRITE_TAC[ball_annulus]);
 243
 244  (REWRITE_WITH
 245 `sum ({v | v + u IN V} INTER (cball (vec 0,&2 * h0) DIFF ball (vec 0,&2)))
 246  (\v. lmfun (hl [vec 0; v])) =
 247  sum {v:real^3 | v IN V /\ ~(u = v) /\ dist (u,v) <= &2 * h0}
 248  (\v. lmfun (hl [u; v]))`);
 249  (MATCH_MP_TAC SUM_EQ_GENERAL_INVERSES);
 250  (REWRITE_TAC[IN_ELIM_THM]);
 251  (EXISTS_TAC `(\x:real^3. x + u)`);
 252  (EXISTS_TAC `(\x:real^3. x - u)`);
 253  (REPEAT STRIP_TAC);
 254  (REWRITE_TAC[IN_ELIM_THM;cball;INTER]);
 255  (CONJ_TAC);
 256  (ASM_REWRITE_TAC[VECTOR_ARITH `y:real^3 - u + u = y`]);
 257  (REWRITE_TAC[DIFF;IN_ELIM_THM;ball]);
 258  (UP_ASM_TAC THEN REWRITE_TAC[dist]);
 259  (DISCH_TAC THEN CONJ_TAC);
 260  (UP_ASM_TAC THEN NORM_ARITH_TAC);
 261  (REWRITE_WITH `norm (vec 0 - (y:real^3 - u)) = dist (u,y)`);
 262  (REWRITE_TAC[dist]);
 263  (NORM_ARITH_TAC);
 264  (REWRITE_TAC[REAL_ARITH `~(a < b) <=> b <= a`]);
 265  (NEW_GOAL `V u /\ V y /\ ~(u = (y:real^3))`);
 266  (ASM_REWRITE_TAC[]);
 267  STRIP_TAC;
 268  (ONCE_REWRITE_TAC[GSYM IN]);
 269  (ASM_REWRITE_TAC[]);
 270  (ONCE_REWRITE_TAC[GSYM IN]);
 271  (ASM_REWRITE_TAC[]);
 272  UP_ASM_TAC;
 273  (ASM_MESON_TAC[packing]);
 274  (REWRITE_TAC[BETA_THM]);
 275  VECTOR_ARITH_TAC;
 276  (REWRITE_TAC[BETA_THM]);
 277  (UP_ASM_TAC THEN REWRITE_TAC[INTER;IN_ELIM_THM]);
 278  (MESON_TAC[]);
 279  (UP_ASM_TAC THEN REWRITE_TAC[IN_ELIM_THM]);
 280  (REWRITE_TAC[VECTOR_ARITH `(u = x + u:real^3) <=> (x = vec 0)`]);
 281  (UP_ASM_TAC THEN REWRITE_TAC[INTER; DIFF;IN_ELIM_THM;ball]);
 282  (REPEAT STRIP_TAC);
 283  (NEW_GOAL `dist(vec 0, x:real^3) = &0`);
 284  (ASM_REWRITE_TAC[dist]);
 285  NORM_ARITH_TAC;
 286  (ASM_REAL_ARITH_TAC);
 287  (REWRITE_TAC[BETA_THM;dist]);
 288  (UP_ASM_TAC THEN REWRITE_TAC[INTER; DIFF;IN_ELIM_THM;ball]);
 289  (REWRITE_TAC[IN_ELIM_THM;cball]);
 290  NORM_ARITH_TAC;
 291  (REWRITE_TAC[BETA_THM]);
 292  (VECTOR_ARITH_TAC);
 293  (REWRITE_TAC[BETA_THM]);
 294  (AP_TERM_TAC);
 295  (REWRITE_TAC[HL]);
 296  (REWRITE_WITH `!u v:real^3. set_of_list [u; v] = {u , v}`);
 297  (REWRITE_TAC[set_of_list]);
 298  (UP_ASM_TAC THEN REWRITE_TAC[INTER; DIFF;IN_ELIM_THM;ball]);
 299  (REPEAT STRIP_TAC);
 300  (NEW_GOAL `~(x:real^3 = vec 0)`);
 301  (REPEAT STRIP_TAC);
 302  (NEW_GOAL `dist(vec 0, x:real^3) = &0`);
 303  (ASM_REWRITE_TAC[dist]);
 304  NORM_ARITH_TAC;
 305  (ASM_REAL_ARITH_TAC);
 306  (REWRITE_WITH `radV {u:real^3, x + u} = radV {vec 0 + u, x + u}`);
 307  (MESON_TAC[VECTOR_ARITH `!u. u = vec 0 + u`]);
 308  (ASM_MESON_TAC[RADV_TRANS_EQ]);
 309  (ASM_REWRITE_TAC[])
 310 ]);;
 311
 312
 313
 314 end;;