2 (* ========================================================================= *)
3 (* FLYSPECK - BOOK FORMALIZATION *)
5 (* Authour : VU KHAC KY *)
6 (* Book lemma: UPFZBZM *)
7 (* Chaper : Packing (Clusters) *)
8 (* Date : October 3, 2010 *)
10 (* ========================================================================= *)
12 (* ========================================================================= *)
13 (* Supporting lemmas for UPFZBZM *)
14 (* Chaper : Packing (Clusters) *)
16 (* ========================================================================= *)
18 (* ========================================================================= *)
19 (* FILES NEED TO BE LOADED *)
20 (* ========================================================================= *)
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 *)
29 flyspeck_needs "packing/ky/UPFZBZM_axioms.hl";;
31 module UPFZBZM_support_lemmas.hl
35 open Vukhacky_tactics;;
37 (*-------------------------------------------------------------------------- *)
40 `!V. saturated V /\ packing V /\ cell_cluster_estimate V /\
42 lmfun_inequality V ==>
43 (?G. negligible_fun_0 G V /\ fcc_compatible G V)`;;
45 (* ------------------------------------------------------------------------- *)
48 (* ========================================================================= *)
49 (* SOME COMPLEMENTARY LEMMAS *)
50 (* ========================================================================= *)
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]);;
57 let john_harrison_lemma2 = MESON[] `(?x. P x) /\ (@x. P x) = a ==> P a`;;
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]);;
68 (* ------------------------------------------------------------------------- *)
71 let SQRT_RULE_Euler_lemma = prove
72 (`!x y. x pow 2 = y /\ &0 <= x ==> x = sqrt y`,
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]);;
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);
83 (REWRITE_TAC[REAL_ARITH `&32 = &64 * (&1 / &2)`]);
84 (MATCH_MP_TAC SQRT_MUL);
87 (* ------------------------------------------------------------------------- *)
90 let m1_minus_12m2 = prove_by_refinement (
91 `mm1 - &12 * mm2 = sqrt (&1 / &2)`,
93 [ (REWRITE_TAC[mm1;mm2]);
94 (REWRITE_TAC [REAL_ARITH `a * (b / c) = (a * b) / c`]);
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`));
101 (REWRITE_TAC[REAL_ARITH `&8 = &4 * &2`]);
102 (REWRITE_WITH `sqrt (&4 * &2) = sqrt (&4) * sqrt (&2)`);
103 (MATCH_MP_TAC SQRT_MUL);
105 (MATCH_MP_TAC (MESON[REAL_EQ_MUL_RCANCEL] `a = b ==> a * x = b * x`));
106 (MATCH_MP_TAC SQRT_RULE_Euler_lemma);
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]);
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`);
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`);
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])]);;
135 (* ------------------------------------------------------------------------- *)
138 let ZERO_LE_MM2_LEMMA =
139 MATCH_MP (REAL_ARITH `&0 < x ==> &0 <= x`) ZERO_LT_MM2_LEMMA;;
141 (* ------------------------------------------------------------------------- *)
144 let FINITE_edgeX = prove_by_refinement (
145 `!V X. FINITE (edgeX V X)`,
146 [(REPEAT GEN_TAC THEN REWRITE_TAC[edgeX;VX]);
148 (* Break into 2 subgoal *)
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 *)
156 `FINITE (set_of_list (truncate_simplex (k - 1) (ul:(real^3)list)))`
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}`);
163 (ASM_MESON_TAC[FINITE_POWERSET]);
164 (REWRITE_TAC[SUBSET;IN_ELIM_THM]);
166 (REPLICATE_TAC 5 UP_ASM_TAC);
170 (* ------------------------------------------------------------------------- *)
173 let FINITE_critical_edgeX = prove_by_refinement (
174 `!V X. FINITE (critical_edgeX V X)`,
176 (REWRITE_TAC[critical_edgeX]);
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])]);;
185 (* ------------------------------------------------------------------------- *)
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`));
194 (REWRITE_TAC[GSYM REAL_ABS_BOUNDS; NORM_CAUCHY_SCHWARZ_DIV])]);;
197 (* ------------------------------------------------------------------------- *)
200 let DIHV_SYM = prove_by_refinement (
201 `!(x:real^N) y z t. dihV x y z t = dihV y x z t`,
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`));
207 (* Break into 2 subgoals with similar proofs *)
210 (EXPAND_TAC "vap'" THEN EXPAND_TAC "vap");
212 (REWRITE_WITH `(va':real^N) = va - vc`);
213 (EXPAND_TAC "va'" THEN EXPAND_TAC "va" THEN EXPAND_TAC "vc");
216 (REWRITE_WITH `(vc':real^N) = --vc`);
217 (EXPAND_TAC "vc'" THEN EXPAND_TAC "vc");
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 `]);
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]);
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");
240 (REWRITE_WITH `(vc':real^N) = --vc`);
241 (EXPAND_TAC "vc'" THEN EXPAND_TAC "vc");
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 `]);
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)]);;
258 (* ------------------------------------------------------------------------- *)
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]);
266 (LET_TAC THEN COND_CASES_TAC);
267 (REWRITE_TAC[dihX2] THEN LET_TAC THEN REWRITE_TAC[DIHV_LE_0]);
269 (REWRITE_TAC[dihX3] THEN LET_TAC THEN MATCH_MP_TAC (SUM_POS_LE));
272 (REWRITE_TAC[left_action_list;TABLE]);
273 (ABBREV_TAC `P = {p | p permutes {0, 1, 2}}`);
275 `VL = {vl:(real^3)list | ?p. p permutes {0, 1, 2} /\
276 vl = REVERSE (REVERSE_TABLE (\i. EL (inverse p i) ul')
280 (MATCH_MP_TAC FINITE_SUBSET);
281 (EXISTS_TAC `(VL:(real^3)list->bool) CROSS (P: (num->num)->bool)`);
283 (MATCH_MP_TAC FINITE_CROSS);
284 (NEW_GOAL `FINITE (P:(num->num)->bool)`);
286 (REWRITE_TAC[FINITE_PERMUTE_3]);
289 (MATCH_MP_TAC FINITE_SUBSET);
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}`);
295 (MATCH_MP_TAC FINITE_IMAGE_EXPAND);
297 (EXPAND_TAC "P" THEN EXPAND_TAC "f");
298 (REWRITE_TAC[SUBSET;IN;IN_ELIM_THM;BETA_THM]);
303 (REWRITE_TAC[CROSS;IN;IN_ELIM_THM;SUBSET]);
305 (EXISTS_TAC `vl:(real^3)list`);
306 (EXISTS_TAC `p:(num->num)`);
308 (EXISTS_TAC `p:(num->num)`);
314 (REWRITE_TAC[IN_ELIM_THM]);
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 /\
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 /\
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]);
332 (REWRITE_TAC[dihX4]);
334 (MATCH_MP_TAC REAL_LE_MUL THEN REWRITE_TAC[REAL_ARITH `&0 <= &1 / &2`]);
335 (MATCH_MP_TAC SUM_POS_LE);
338 (ABBREV_TAC `P = {p | p permutes {0, 1, 2, 3}}`);
340 `VL = {vl:(real^3)list | ?p. p permutes {0, 1, 2, 3} /\
341 vl = left_action_list p ul' /\
344 (MATCH_MP_TAC FINITE_SUBSET);
345 (EXISTS_TAC `(VL:(real^3)list->bool) CROSS (P: (num->num)->bool)`);
347 (MATCH_MP_TAC FINITE_CROSS);
348 (NEW_GOAL `FINITE (P:(num->num)->bool)`);
350 (REWRITE_TAC[FINITE_PERMUTE_4]);
353 (MATCH_MP_TAC FINITE_SUBSET);
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}`);
358 (MATCH_MP_TAC FINITE_IMAGE_EXPAND);
360 (EXPAND_TAC "P" THEN EXPAND_TAC "f");
361 (REWRITE_TAC[SUBSET;IN;IN_ELIM_THM;BETA_THM]);
366 (REWRITE_TAC[CROSS;IN;IN_ELIM_THM;SUBSET]);
368 (EXISTS_TAC `vl:(real^3)list`);
369 (EXISTS_TAC `p:(num->num)`);
371 (EXISTS_TAC `p:(num->num)`);
377 (REWRITE_TAC[IN_ELIM_THM]);
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 /\
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 /\
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]);
396 (* ------------------------------------------------------------------------- *)
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`,
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}`);
406 (MATCH_MP_TAC SUM_UNION);
407 (REWRITE_TAC[FINITE_SING]);
408 (UP_ASM_TAC THEN SET_TAC[])]);;