2 (* ========================================================================= *)
3 (* FLYSPECK - BOOK FORMALIZATION *)
5 (* Authour : VU KHAC KY *)
6 (* Book lemma: RDWKARC *)
7 (* Chaper : Packing (Clusters) *)
9 (* ========================================================================= *)
10 (* FILES NEED TO BE LOADED *)
12 (* ========================================================================= *)
14 module Rdwkarc = struct
20 open Vukhacky_tactics;;
25 open Euler_main_theorem;;
32 open Vukhacky_tactics;;
35 (* open Marchal_cells_2;; *)
36 open Marchal_cells_2_new;;
51 open Upfzbzm_support_lemmas;;
52 open Marchal_cells_3;;
55 open Sum_gammax_lmfun_estimate;;
59 (*-------------------------------------------------------------------------- *)
63 `~kepler_conjecture /\ (!V. cell_cluster_estimate_v1 V) /\ TSKAJXY_statement
64 ==> (?V. packing V /\ V SUBSET ball_annulus /\ ~lmfun_ineq_center V)`;;
67 (* ------------------------------------------------------------------------- *)
68 (* The following lemmas are necessary for the main theorem RDWKARC *)
69 (* ------------------------------------------------------------------------- *)
72 let JGXZYGW_KY = prove_by_refinement (
75 (?A. fcc_compatible A S /\ negligible_fun_0 A S)
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"));
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`));
89 (* ------------------------------------------------------------------------- *)
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]);
96 `!u:real^3 v. V u /\ V v /\ ~(u = v) ==> &2 <= dist (u,v)`) );
98 (REWRITE_WITH `V (u:real^3) /\ V v <=> u IN V /\ v IN V`);
101 (* Break into smaller subgoals *)
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])]);;
109 (* ------------------------------------------------------------------------ *)
111 let PACKING_TRANS = prove_by_refinement (
112 `! V (x:real^3). packing V ==> packing {u | (u + x) IN V}`,
114 [(REPEAT GEN_TAC THEN REWRITE_TAC[packing;IN_ELIM_THM]);
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')`);
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 );
129 (REWRITE_WITH `dist (u:real^3, v) = dist (u', v':real^3)`);
131 (EXPAND_TAC "u'" THEN EXPAND_TAC "v'");
136 (UP_ASM_TAC THEN ASM_REWRITE_TAC[])]);;
139 (* ------------------------------------------------------------------------- *)
142 let SATURATED_TRANS = prove_by_refinement (
143 `!V (x:real^3). saturated V ==> saturated {u | u + x IN V}`,
145 [(REPEAT GEN_TAC THEN REWRITE_TAC[saturated]);
146 (DISCH_THEN (LABEL_TAC "asm1"));
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)`]);
155 (NEW_GOAL `dist (x',y - x) = dist (x'+ x,y:real^3)`);
161 (ASM_MESON_TAC[])]);;
164 (* ------------------------------------------------------------------------- *)
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);;
171 (* ========================================================================= *)
172 (* MAIN THEOREM RDWKARC *)
173 (* ========================================================================= *)
176 let RDWKARC = prove_by_refinement (Pack_concl.RDWKARC_concl,
178 (REWRITE_TAC[kepler_conjecture]);
180 `~(!V. packing V /\ saturated V
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
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))`);
196 (NEW_GOAL `~(lmfun_inequality (V:real^3->bool))`);
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);
206 (CHOOSE_TAC (ASSUME `?G. negligible_fun_0 G V /\ fcc_compatible G V`));
207 (EXISTS_TAC `G:real^3->real`);
211 (* ---------------------------------------------------------------------- *)
213 (UP_ASM_TAC THEN REWRITE_TAC[lmfun_inequality]);
216 ==> sum {v | v IN V /\ ~(u = v) /\ dist (u,v) <= &2 * h0}
217 (\v. lmfun (hl [u; v])) <=
220 /\ ~(sum {v | v IN V /\ ~(u = v) /\ dist (u,v) <= &2 * h0}
221 (\v. lmfun (hl [u; v])) <=
224 (REWRITE_TAC[REAL_ARITH `~(a <= b) <=> b < a`]);
226 (FIRST_X_ASSUM CHOOSE_TAC);
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]);
233 (NEW_GOAL `packing (V':real^3->bool)`);
234 (EXPAND_TAC "V'" THEN ASM_MESON_TAC[PACKING_TRANS]);
236 (ASM_MESON_TAC[PACKING_SUBSET;INTER_SUBSET]);
238 (* -------------------------------------------------------------------------- *)
240 (REWRITE_TAC[lmfun_ineq_center]);
241 (REWRITE_TAC[REAL_ARITH `~(a <= b) <=> b < a`]);
242 (EXPAND_TAC "V'" THEN REWRITE_TAC[ball_annulus]);
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)`);
254 (REWRITE_TAC[IN_ELIM_THM;cball;INTER]);
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)`);
264 (REWRITE_TAC[REAL_ARITH `~(a < b) <=> b <= a`]);
265 (NEW_GOAL `V u /\ V y /\ ~(u = (y:real^3))`);
268 (ONCE_REWRITE_TAC[GSYM IN]);
270 (ONCE_REWRITE_TAC[GSYM IN]);
273 (ASM_MESON_TAC[packing]);
274 (REWRITE_TAC[BETA_THM]);
276 (REWRITE_TAC[BETA_THM]);
277 (UP_ASM_TAC THEN REWRITE_TAC[INTER;IN_ELIM_THM]);
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]);
283 (NEW_GOAL `dist(vec 0, x:real^3) = &0`);
284 (ASM_REWRITE_TAC[dist]);
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]);
291 (REWRITE_TAC[BETA_THM]);
293 (REWRITE_TAC[BETA_THM]);
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]);
300 (NEW_GOAL `~(x:real^3 = vec 0)`);
302 (NEW_GOAL `dist(vec 0, x:real^3) = &0`);
303 (ASM_REWRITE_TAC[dist]);
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]);