legacy/oldpacking/packing/development/Backup/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   open Sphere;;
  17   open Pack_defs;;
  18   open Pack_concl;;
  19   open Vukhacky_tactics;;
  20   open Pack1;;
  21
  22 (*-------------------------------------------------------------------------- *)
  23
  24 let RDWKARC_concl =
  25 `~kepler_conjecture /\ (!V. cell_cluster_estimate V) /\ TSKAJXY_statement
  26   ==> (?V. packing V /\ V SUBSET ball_annulus /\ ~lmfun_ineq_center V)`;;
  27
  28
  29 (* ------------------------------------------------------------------------- *)
  30 (*   The following lemmas are necessary for the main theorem RDWKARC         *)
  31 (* ------------------------------------------------------------------------- *)
  32
  33 (* Lemma 1 *)
  34 let JGXZYGW_KY = prove_by_refinement (
  35  `!S.   packing S /\
  36          saturated S /\
  37          (?A. fcc_compatible A S /\ negligible_fun_0 A S)
  38          ==> (?c. !r. &1 <= r
  39                       ==> vol
  40                           (UNIONS {ball (v,&1) | v IN S} INTER ball (vec 0,r)) /
  41                           vol (ball (vec 0,r)) <=
  42                           pi / sqrt (&18) + c / r)`,
  43 [(MP_TAC JGXZYGW THEN DISCH_THEN (LABEL_TAC "asm1"));
  44  GEN_TAC;
  45  (REWRITE_TAC[negligible_fun_0]);
  46  (USE_THEN "asm1" (MP_TAC o SPEC `S:real^3->bool`));
  47  (DISCH_THEN (LABEL_TAC "asm2"));
  48  (USE_THEN "asm2" (MP_TAC o SPEC `(vec 0):real^3`));
  49  (MESON_TAC[])]);;
  50
  51 (* ------------------------------------------------------------------------- *)
  52 (*  Lemma 2 *)
  53 let PACKING_SUBSET = prove_by_refinement (
  54  `!V S. packing V /\ S SUBSET V ==> packing S`,
  55 [(REPEAT GEN_TAC THEN REWRITE_TAC[packing;SUBSET;IN_ELIM_THM]);
  56  (REPEAT STRIP_TAC);
  57  (MATCH_MP_TAC(ASSUME
  58     `!u:real^3 v. V u /\ V v /\ ~(u = v) ==> &2 <= dist (u,v)`) );
  59  (ASM_REWRITE_TAC[]);
  60  (REWRITE_WITH `V (u:real^3) /\ V v <=> u IN V /\ v IN V`);
  61  (REWRITE_TAC[IN]);
  62  STRIP_TAC;
  63    (* Break into smaller subgoals *)
  64
  65  (MATCH_MP_TAC(ASSUME `!(x:real^3). x IN S ==> x IN V`) );
  66  (ASM_REWRITE_TAC[IN]);
  67  (MATCH_MP_TAC(ASSUME `!(x:real^3). x IN S ==> x IN V`) );
  68  (ASM_REWRITE_TAC[IN])]);;
  69
  70
  71 (* ------------------------------------------------------------------------  *)
  72 (* Lemma 3 *)
  73 let PACKING_TRANS = prove_by_refinement (
  74  `! V (x:real^3). packing V ==> packing {u | (u + x) IN V}`,
  75
  76 [(REPEAT GEN_TAC THEN REWRITE_TAC[packing;IN_ELIM_THM]);
  77 (REPEAT STRIP_TAC);
  78 (ABBREV_TAC `u' = (u:real^3) + x`);
  79 (ABBREV_TAC `v' = (v:real^3) + x`);
  80   (NEW_GOAL `V (u':real^3) /\ V v' /\ ~(u' = v')`);
  81   (* New subgoal 1 *)
  82   (REPEAT STRIP_TAC);
  83   (ASM_REWRITE_TAC[GSYM IN]);
  84   (ASM_REWRITE_TAC[GSYM IN]);
  85   (NEW_GOAL `u = v:real^3`);
  86   (REPLICATE_TAC 3 UP_ASM_TAC );
  87   VECTOR_ARITH_TAC;
  88   (ASM_MESON_TAC[]);
  89   (* End subgoal 1 *)
  90
  91   (REWRITE_WITH `dist (u:real^3, v) = dist (u', v':real^3)`);
  92   (* Subgoal 2 *)
  93   (EXPAND_TAC "u'" THEN EXPAND_TAC "v'");
  94   (REWRITE_TAC[dist]);
  95   (NORM_ARITH_TAC);
  96   (* End subgoal 2 *)
  97
  98 (UP_ASM_TAC THEN ASM_REWRITE_TAC[])]);;
  99
 100
 101 (* ------------------------------------------------------------------------- *)
 102 (* Lemma 4 *)
 103
 104 let SATURATED_TRANS = prove_by_refinement (
 105 `!V (x:real^3). saturated V ==> saturated {u | u + x IN V}`,
 106
 107 [(REPEAT GEN_TAC THEN REWRITE_TAC[saturated]);
 108 (DISCH_THEN (LABEL_TAC "asm1"));
 109 (GEN_TAC);
 110 (USE_THEN "asm1" (MP_TAC  o SPEC `(x':real^3) + x`));
 111 (DEL_TAC THEN DISCH_TAC);
 112 (FIRST_X_ASSUM CHOOSE_TAC);
 113 (EXISTS_TAC `y - (x:real^3)`);
 114 (REWRITE_TAC[IN_ELIM_THM; VECTOR_ARITH `y - x + x = (y:real^3)`]);
 115 (ASM_REWRITE_TAC[]);
 116
 117   (NEW_GOAL `dist (x',y - x) = dist (x'+ x,y:real^3)`);
 118   (* Subgoal 1 *)
 119   (REWRITE_TAC[dist]);
 120   (NORM_ARITH_TAC);
 121   (* End subgoal 1 *)
 122
 123 (ASM_MESON_TAC[])]);;
 124
 125
 126 (* ------------------------------------------------------------------------- *)
 127 (* Lemma 5 *)
 128
 129 let RADV_TRANS_EQ = prove (
 130  `!u v:real^3 x. ~(u = v) ==> radV {u, v} = radV {u + x, v + x}`,
 131    REWRITE_TAC[GSYM set_of_list; GSYM HL; HL_2] THEN NORM_ARITH_TAC);;
 132
 133 (* ========================================================================= *)
 134 (*                             MAIN THEOREM RDWKARC                          *)
 135 (* ========================================================================= *)
 136
 137 let RDWKARC = prove_by_refinement (RDWKARC_concl,
 138 [ (REWRITE_TAC[kepler_conjecture]);
 139  (REWRITE_WITH
 140  `~(!V. packing V /\ saturated V
 141         ==> (?c. !r. &1 <= r
 142                     ==> vol
 143                         (UNIONS {ball (v,&1) | v IN V} INTER ball (vec 0,r)) /
 144                         vol (ball (vec 0,r)) <=
 145                         pi / sqrt (&18) + c / r)) <=>
 146  (?V. packing V /\ saturated V
 147         /\ ~(?c. !r. &1 <= r
 148                     ==> vol
 149                         (UNIONS {ball (v,&1) | v IN V} INTER ball (vec 0,r)) /
 150                         vol (ball (vec 0,r)) <=
 151                         pi / sqrt (&18) + c / r))`);
 152
 153  (MESON_TAC[]);
 154  STRIP_TAC;
 155
 156  (NEW_GOAL `~(lmfun_inequality (V:real^3->bool))`);
 157  STRIP_TAC;
 158  (NEW_GOAL `(?G. negligible_fun_0 G V /\ fcc_compatible G V)`);
 159  (ASM_MESON_TAC[UPFZBZM]);
 160  (NEW_GOAL `(?c. !r. &1 <= r
 161                 ==> vol (UNIONS {ball (v,&1) | v IN V} INTER ball (vec 0,r)) /
 162                     vol (ball (vec 0,r)) <=
 163                     pi / sqrt (&18) + c / r)`);
 164  (MATCH_MP_TAC JGXZYGW_KY);
 165  (ASM_REWRITE_TAC[]);
 166  (CHOOSE_TAC (ASSUME `?G. negligible_fun_0 G V /\ fcc_compatible G V`));
 167  (EXISTS_TAC `G:real^3->real`);
 168  (ASM_REWRITE_TAC[]);
 169  (ASM_MESON_TAC[]);
 170
 171 (* ---------------------------------------------------------------------- *)
 172
 173  (UP_ASM_TAC THEN REWRITE_TAC[lmfun_inequality]);
 174  (REWRITE_WITH
 175  `~(!u:real^3. u IN V
 176        ==> sum {v | v IN V /\ ~(u = v) /\ dist (u,v) <= &2 * h0}
 177            (\v. lmfun (hl [u; v])) <=
 178            &12) <=>
 179  (?u. u IN V
 180        /\ ~(sum {v | v IN V /\ ~(u = v) /\ dist (u,v) <= &2 * h0}
 181            (\v. lmfun (hl [u; v])) <=
 182            &12))`);
 183  (MESON_TAC[]);
 184  (REWRITE_TAC[REAL_ARITH `~(a <= b) <=> b < a`]);
 185  (DISCH_TAC);
 186  (FIRST_X_ASSUM CHOOSE_TAC);
 187
 188
 189  (ABBREV_TAC `V' = {v:real^3 | v + u IN V}`);
 190  (EXISTS_TAC `V':real^3->bool INTER ball_annulus`);
 191  (ASM_REWRITE_TAC[INTER_SUBSET]);
 192
 193  (NEW_GOAL `packing (V':real^3->bool)`);
 194  (EXPAND_TAC "V'" THEN ASM_MESON_TAC[PACKING_TRANS]);
 195  STRIP_TAC;
 196  (ASM_MESON_TAC[PACKING_SUBSET;INTER_SUBSET]);
 197
 198 (* -------------------------------------------------------------------------- *)
 199
 200  (REWRITE_TAC[lmfun_ineq_center]);
 201  (REWRITE_TAC[REAL_ARITH `~(a <= b) <=> b < a`]);
 202  (EXPAND_TAC "V'" THEN REWRITE_TAC[ball_annulus]);
 203
 204  (REWRITE_WITH
 205 `sum ({v | v + u IN V} INTER (cball (vec 0,&2 * h0) DIFF ball (vec 0,&2)))
 206  (\v. lmfun (hl [vec 0; v])) =
 207  sum {v:real^3 | v IN V /\ ~(u = v) /\ dist (u,v) <= &2 * h0}
 208  (\v. lmfun (hl [u; v]))`);
 209  (MATCH_MP_TAC SUM_EQ_GENERAL_INVERSES);
 210  (REWRITE_TAC[IN_ELIM_THM]);
 211  (EXISTS_TAC `(\x:real^3. x + u)`);
 212  (EXISTS_TAC `(\x:real^3. x - u)`);
 213  (REPEAT STRIP_TAC);
 214  (REWRITE_TAC[IN_ELIM_THM;cball;INTER]);
 215  (CONJ_TAC);
 216  (ASM_REWRITE_TAC[VECTOR_ARITH `y:real^3 - u + u = y`]);
 217  (REWRITE_TAC[DIFF;IN_ELIM_THM;ball]);
 218  (UP_ASM_TAC THEN REWRITE_TAC[dist]);
 219  (DISCH_TAC THEN CONJ_TAC);
 220  (UP_ASM_TAC THEN NORM_ARITH_TAC);
 221  (REWRITE_WITH `norm (vec 0 - (y:real^3 - u)) = dist (u,y)`);
 222  (REWRITE_TAC[dist]);
 223  (NORM_ARITH_TAC);
 224  (REWRITE_TAC[REAL_ARITH `~(a < b) <=> b <= a`]);
 225  (NEW_GOAL `V u /\ V y /\ ~(u = (y:real^3))`);
 226  (ASM_REWRITE_TAC[]);
 227  STRIP_TAC;
 228  (ONCE_REWRITE_TAC[GSYM IN]);
 229  (ASM_REWRITE_TAC[]);
 230  (ONCE_REWRITE_TAC[GSYM IN]);
 231  (ASM_REWRITE_TAC[]);
 232  UP_ASM_TAC;
 233  (ASM_MESON_TAC[packing]);
 234  (REWRITE_TAC[BETA_THM]);
 235  VECTOR_ARITH_TAC;
 236  (REWRITE_TAC[BETA_THM]);
 237  (UP_ASM_TAC THEN REWRITE_TAC[INTER;IN_ELIM_THM]);
 238  (MESON_TAC[]);
 239  (UP_ASM_TAC THEN REWRITE_TAC[IN_ELIM_THM]);
 240  (REWRITE_TAC[VECTOR_ARITH `(u = x + u:real^3) <=> (x = vec 0)`]);
 241  (UP_ASM_TAC THEN REWRITE_TAC[INTER; DIFF;IN_ELIM_THM;ball]);
 242  (REPEAT STRIP_TAC);
 243  (NEW_GOAL `dist(vec 0, x:real^3) = &0`);
 244  (ASM_REWRITE_TAC[dist]);
 245  NORM_ARITH_TAC;
 246  (ASM_REAL_ARITH_TAC);
 247  (REWRITE_TAC[BETA_THM;dist]);
 248  (UP_ASM_TAC THEN REWRITE_TAC[INTER; DIFF;IN_ELIM_THM;ball]);
 249  (REWRITE_TAC[IN_ELIM_THM;cball]);
 250  NORM_ARITH_TAC;
 251  (REWRITE_TAC[BETA_THM]);
 252  (VECTOR_ARITH_TAC);
 253  (REWRITE_TAC[BETA_THM]);
 254  (AP_TERM_TAC);
 255  (REWRITE_TAC[HL]);
 256  (REWRITE_WITH `!u v:real^3. set_of_list [u; v] = {u , v}`);
 257  (REWRITE_TAC[set_of_list]);
 258  (UP_ASM_TAC THEN REWRITE_TAC[INTER; DIFF;IN_ELIM_THM;ball]);
 259  (REPEAT STRIP_TAC);
 260  (NEW_GOAL `~(x:real^3 = vec 0)`);
 261  (REPEAT STRIP_TAC);
 262  (NEW_GOAL `dist(vec 0, x:real^3) = &0`);
 263  (ASM_REWRITE_TAC[dist]);
 264  NORM_ARITH_TAC;
 265  (ASM_REAL_ARITH_TAC);
 266  (REWRITE_WITH `radV {u:real^3, x + u} = radV {vec 0 + u, x + u}`);
 267  (MESON_TAC[VECTOR_ARITH `!u. u = vec 0 + u`]);
 268  (ASM_MESON_TAC[RADV_TRANS_EQ]);
 269  (ASM_REWRITE_TAC[]) ]);;
 270
 271
 272 (* Finish the Lemma *)
 273 end;;