1 (* ========================================================================= *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
4 (* Authour : VU KHAC KY *)
5 (* Book lemma: DDZUPHJ *)
8 (* ========================================================================= *)
11 module Ddzuphj = struct
14 open Vukhacky_tactics;;
21 open Marchal_cells_2_new;;
27 (* ========================================================================= *)
31 saturated V /\ packing V /\ k IN {0,1,2,3,4} /\
32 barV V 3 ul /\ barV V 3 vl /\ rogers V ul = rogers V vl /\
33 aff_dim (rogers V ul) = &3 /\ ~ (mcell k V ul = {})
34 ==> (mcell k V ul = mcell k V vl)`;;
36 (* ========================================================================= *)
38 let RCONE_GT_EQ_EMPTY_LEMMA = prove_by_refinement (
39 `!a:real^3 b r. r >= &1 ==> rcone_gt a b r = {}`,
41 (REWRITE_TAC[rcone_gt;rconesgn;
42 SET_RULE `{x | P x} = {} <=> (!x. P x ==> F)`]);
43 (REWRITE_TAC[dist] THEN REPEAT STRIP_TAC);
44 (NEW_GOAL `(x - a) dot (b - a) <= norm(x - a) * norm (b - a:real^3)`);
45 (REWRITE_TAC[NORM_CAUCHY_SCHWARZ]);
46 (NEW_GOAL`norm (x - a) * norm (b:real^3 -a) * r >= norm (x-a) * norm (b-a)`);
47 (REWRITE_TAC[REAL_ARITH `(a*b*c >= a * b) <=> &0 <= (a * b) * (c - &1)`]);
48 (MATCH_MP_TAC REAL_LE_MUL);
50 (MATCH_MP_TAC REAL_LE_MUL THEN REWRITE_TAC[NORM_POS_LE]);
52 (ASM_REAL_ARITH_TAC)]);;
54 (* ========================================================================= *)
56 (* ========================================================================= *)
59 let DDZUPHJ = prove_by_refinement (DDZUPHJ_concl,
61 (NEW_GOAL `?u0 u1 u2 u3. ul = [u0;u1;u2;u3:real^3]`);
62 (MATCH_MP_TAC BARV_3_EXPLICIT);
63 (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]);
64 (NEW_GOAL `?v0 v1 v2 v3. vl = [v0;v1;v2;v3:real^3]`);
65 (MATCH_MP_TAC BARV_3_EXPLICIT);
66 (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]);
67 (UP_ASM_TAC THEN UP_ASM_TAC THEN REPEAT STRIP_TAC);
69 (* ========================================================================= *)
72 (ASM_CASES_TAC `k = 4`);
73 (NEW_GOAL `hl (ul:(real^3)list) < sqrt (&2)`);
74 (UNDISCH_TAC `~(mcell k V ul = {})` THEN
75 SIMP_TAC[ASSUME `k = 4`; MCELL_EXPLICIT; ARITH_RULE `4 >= 4`;mcell4]);
78 (NEW_GOAL `truncate_simplex 3 (ul:(real^3)list) = truncate_simplex 3 vl`);
79 (MATCH_MP_TAC TEZFFSK);
80 (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[ARITH_RULE `3 <= 3`]);
81 (REWRITE_WITH `truncate_simplex 3 [u0; u1; u2; u3:real^3] = ul`);
82 (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_3]);
84 (UP_ASM_TAC THEN REWRITE_WITH `truncate_simplex 3 (ul:(real^3)list) = ul`);
85 (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_3]);
86 (REWRITE_WITH `truncate_simplex 3 (vl:(real^3)list) = vl`);
87 (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_3]);
89 (REWRITE_TAC[ASSUME `ul = (vl:(real^3)list)`]);
91 (* ========================================================================= *)
93 (ASM_CASES_TAC `k = 3`);
94 (NEW_GOAL `hl (truncate_simplex 2 ul) < sqrt (&2) /\
95 sqrt (&2) <= hl (ul:(real^3)list)`);
96 (UNDISCH_TAC `~(mcell k V ul = {})` THEN
97 SIMP_TAC[ASSUME `k = 3`; MCELL_EXPLICIT;mcell3]);
100 (NEW_GOAL `truncate_simplex 2 (ul:(real^3)list) = truncate_simplex 2 vl`);
101 (MATCH_MP_TAC TEZFFSK);
102 (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]);
104 (NEW_GOAL `!i. 0 <= i /\ i <= 3
105 ==> omega_list_n V ul i = omega_list_n V vl i`);
106 (MATCH_MP_TAC NJIUTIU);
109 (NEW_GOAL `sqrt (&2) <= hl (vl:(real^3)list)`);
110 (REWRITE_TAC[ARITH_RULE `a <= b <=> (b < a ==> F)`]);
112 (NEW_GOAL `hl vl = dist (omega_list V vl,HD vl)`);
113 (MATCH_MP_TAC WAUFCHE2);
114 (EXISTS_TAC `3` THEN REWRITE_TAC[IN] THEN ASM_REWRITE_TAC[]);
115 (NEW_GOAL `hl ul <= dist (omega_list V ul,HD ul)`);
116 (MATCH_MP_TAC WAUFCHE1);
117 (EXISTS_TAC `3` THEN REWRITE_TAC[IN] THEN ASM_REWRITE_TAC[]);
119 REWRITE_WITH `omega_list V ul = omega_list V vl /\ HD ul = HD vl`);
121 (ASM_REWRITE_TAC[OMEGA_LIST; LENGTH]);
122 (REWRITE_TAC[GSYM (ASSUME `ul = [u0;u1;u2;u3:real^3]`);
123 GSYM (ASSUME `vl = [v0;v1;v2;v3:real^3]`)]);
124 (FIRST_ASSUM MATCH_MP_TAC);
126 (REWRITE_WITH `HD (ul:(real^3)list) = HD (truncate_simplex 2 ul)`);
127 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
128 (MATCH_MP_TAC Packing3.HD_TRUNCATE_SIMPLEX);
129 (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC);
130 (REWRITE_WITH `HD (vl:(real^3)list) = HD (truncate_simplex 2 vl)`);
131 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
132 (MATCH_MP_TAC Packing3.HD_TRUNCATE_SIMPLEX);
133 (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC);
135 (ASM_REAL_ARITH_TAC);
137 (NEW_GOAL `mxi V ul = mxi V vl`);
141 (FIRST_ASSUM MATCH_MP_TAC);
144 (ASM_REAL_ARITH_TAC);
151 (REWRITE_WITH `omega_list_n V ul 2 = omega_list_n V vl 2`);
152 (FIRST_ASSUM MATCH_MP_TAC THEN ARITH_TAC);
153 (REWRITE_WITH `omega_list_n V ul 3 = omega_list_n V vl 3`);
154 (FIRST_ASSUM MATCH_MP_TAC THEN ARITH_TAC);
155 (REWRITE_WITH `HD (ul:(real^3)list) = HD (truncate_simplex 2 ul)`);
156 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
157 (MATCH_MP_TAC Packing3.HD_TRUNCATE_SIMPLEX);
158 (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC);
159 (REWRITE_WITH `HD (vl:(real^3)list) = HD (truncate_simplex 2 vl)`);
160 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
161 (MATCH_MP_TAC Packing3.HD_TRUNCATE_SIMPLEX);
162 (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC);
165 (SIMP_TAC[ASSUME `k = 3`; MCELL_EXPLICIT; mcell3]);
170 (UP_ASM_TAC THEN REWRITE_TAC[GSYM (ASSUME
171 `truncate_simplex 2 ul = truncate_simplex 2 (vl:(real^3)list)`)]);
178 (* ========================================================================= *)
181 (ASM_CASES_TAC `k = 2`);
182 (NEW_GOAL `hl (truncate_simplex 1 ul) < sqrt (&2) /\
183 sqrt (&2) <= hl (ul:(real^3)list)`);
184 (UNDISCH_TAC `~(mcell k V ul = {})` THEN
185 SIMP_TAC[ASSUME `k = 2`; MCELL_EXPLICIT;mcell2]);
188 (NEW_GOAL `truncate_simplex 1 (ul:(real^3)list) = truncate_simplex 1 vl`);
189 (MATCH_MP_TAC TEZFFSK);
190 (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[ARITH_RULE `1 <= 3`]);
192 (NEW_GOAL `!i. 0 <= i /\ i <= 3
193 ==> omega_list_n V ul i = omega_list_n V vl i`);
194 (MATCH_MP_TAC NJIUTIU);
197 (NEW_GOAL `sqrt (&2) <= hl (vl:(real^3)list)`);
198 (REWRITE_TAC[ARITH_RULE `a <= b <=> (b < a ==> F)`]);
200 (NEW_GOAL `hl vl = dist (omega_list V vl,HD vl)`);
201 (MATCH_MP_TAC WAUFCHE2);
202 (EXISTS_TAC `3` THEN REWRITE_TAC[IN] THEN ASM_REWRITE_TAC[]);
203 (NEW_GOAL `hl ul <= dist (omega_list V ul,HD ul)`);
204 (MATCH_MP_TAC WAUFCHE1);
205 (EXISTS_TAC `3` THEN REWRITE_TAC[IN] THEN ASM_REWRITE_TAC[]);
207 REWRITE_WITH `omega_list V ul = omega_list V vl /\ HD ul = HD vl`);
209 (ASM_REWRITE_TAC[OMEGA_LIST; LENGTH]);
210 (REWRITE_TAC[GSYM (ASSUME `ul = [u0;u1;u2;u3:real^3]`);
211 GSYM (ASSUME `vl = [v0;v1;v2;v3:real^3]`)]);
212 (FIRST_ASSUM MATCH_MP_TAC);
214 (REWRITE_WITH `HD (ul:(real^3)list) = HD (truncate_simplex 1 ul)`);
215 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
216 (MATCH_MP_TAC Packing3.HD_TRUNCATE_SIMPLEX);
217 (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC);
218 (REWRITE_WITH `HD (vl:(real^3)list) = HD (truncate_simplex 1 vl)`);
219 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
220 (MATCH_MP_TAC Packing3.HD_TRUNCATE_SIMPLEX);
221 (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC);
223 (ASM_REAL_ARITH_TAC);
225 (NEW_GOAL `mxi V ul = mxi V vl`);
229 (FIRST_ASSUM MATCH_MP_TAC);
233 (ABBREV_TAC `zl:(real^3)list = truncate_simplex 2 vl`);
234 (NEW_GOAL `hl zl = dist (omega_list V zl,HD zl)`);
235 (MATCH_MP_TAC WAUFCHE2);
236 (EXISTS_TAC `2` THEN REWRITE_TAC[IN] THEN ASM_REWRITE_TAC[]);
238 (EXPAND_TAC "zl" THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
239 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]);
240 (ASM_REAL_ARITH_TAC);
242 (ABBREV_TAC `wl:(real^3)list = truncate_simplex 2 ul`);
243 (NEW_GOAL `hl wl <= dist (omega_list V wl,HD wl)`);
244 (MATCH_MP_TAC WAUFCHE1);
245 (EXISTS_TAC `2` THEN REWRITE_TAC[IN] THEN ASM_REWRITE_TAC[]);
246 (EXPAND_TAC "wl" THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
247 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]);
249 REWRITE_WITH `omega_list V wl = omega_list_n V ul 2/\ HD wl = HD ul`);
252 (MATCH_MP_TAC Packing3.OMEGA_LIST_LEMMA);
253 (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC);
254 (REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`;
255 TRUNCATE_SIMPLEX_EXPLICIT_2; HD]);
257 (UNDISCH_TAC `hl zl = dist (omega_list V zl,HD zl)`);
258 (REWRITE_WITH `omega_list V zl = omega_list_n V vl 2/\ HD zl = HD vl`);
261 (MATCH_MP_TAC Packing3.OMEGA_LIST_LEMMA);
262 (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC);
263 (REWRITE_TAC[ASSUME `vl = [v0;v1;v2;v3:real^3]`;
264 TRUNCATE_SIMPLEX_EXPLICIT_2; HD]);
265 (REWRITE_WITH `omega_list_n V ul 2 = omega_list_n V vl 2/\ HD ul = HD vl`);
267 (FIRST_ASSUM MATCH_MP_TAC THEN ARITH_TAC);
269 (REWRITE_WITH `HD (ul:(real^3)list) = HD (truncate_simplex 1 ul)`);
270 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
271 (MATCH_MP_TAC Packing3.HD_TRUNCATE_SIMPLEX);
272 (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC);
273 (REWRITE_WITH `HD (vl:(real^3)list) = HD (truncate_simplex 1 vl)`);
274 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
275 (MATCH_MP_TAC Packing3.HD_TRUNCATE_SIMPLEX);
276 (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC);
278 (ASM_REAL_ARITH_TAC);
284 (ABBREV_TAC `zl:(real^3)list = truncate_simplex 2 ul`);
285 (NEW_GOAL `hl zl = dist (omega_list V zl,HD zl)`);
286 (MATCH_MP_TAC WAUFCHE2);
287 (EXISTS_TAC `2` THEN REWRITE_TAC[IN] THEN ASM_REWRITE_TAC[]);
289 (EXPAND_TAC "zl" THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
290 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]);
291 (ASM_REAL_ARITH_TAC);
293 (ABBREV_TAC `wl:(real^3)list = truncate_simplex 2 vl`);
294 (NEW_GOAL `hl wl <= dist (omega_list V wl,HD wl)`);
295 (MATCH_MP_TAC WAUFCHE1);
296 (EXISTS_TAC `2` THEN REWRITE_TAC[IN] THEN ASM_REWRITE_TAC[]);
297 (EXPAND_TAC "wl" THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
298 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]);
300 REWRITE_WITH `omega_list V wl = omega_list_n V vl 2/\ HD wl = HD vl`);
303 (MATCH_MP_TAC Packing3.OMEGA_LIST_LEMMA);
304 (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC);
305 (REWRITE_TAC[ASSUME `vl = [v0;v1;v2;v3:real^3]`;
306 TRUNCATE_SIMPLEX_EXPLICIT_2; HD]);
308 (UNDISCH_TAC `hl zl = dist (omega_list V zl,HD zl)`);
309 (REWRITE_WITH `omega_list V zl = omega_list_n V ul 2/\ HD zl = HD ul`);
312 (MATCH_MP_TAC Packing3.OMEGA_LIST_LEMMA);
313 (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC);
314 (REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`;
315 TRUNCATE_SIMPLEX_EXPLICIT_2; HD]);
316 (REWRITE_WITH `omega_list_n V ul 2 = omega_list_n V vl 2/\ HD ul = HD vl`);
318 (FIRST_ASSUM MATCH_MP_TAC THEN ARITH_TAC);
320 (REWRITE_WITH `HD (ul:(real^3)list) = HD (truncate_simplex 1 ul)`);
321 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
322 (MATCH_MP_TAC Packing3.HD_TRUNCATE_SIMPLEX);
323 (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC);
324 (REWRITE_WITH `HD (vl:(real^3)list) = HD (truncate_simplex 1 vl)`);
325 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
326 (MATCH_MP_TAC Packing3.HD_TRUNCATE_SIMPLEX);
327 (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC);
329 (ASM_REAL_ARITH_TAC);
332 (REWRITE_WITH `omega_list_n V ul 2 = omega_list_n V vl 2`);
333 (FIRST_ASSUM MATCH_MP_TAC THEN ARITH_TAC);
334 (REWRITE_WITH `omega_list_n V ul 3 = omega_list_n V vl 3`);
335 (FIRST_ASSUM MATCH_MP_TAC THEN ARITH_TAC);
337 (REWRITE_WITH `HD (ul:(real^3)list) = HD (truncate_simplex 1 ul)`);
338 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
339 (MATCH_MP_TAC Packing3.HD_TRUNCATE_SIMPLEX);
340 (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC);
341 (REWRITE_WITH `HD (vl:(real^3)list) = HD (truncate_simplex 1 vl)`);
342 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
343 (MATCH_MP_TAC Packing3.HD_TRUNCATE_SIMPLEX);
344 (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC);
346 `truncate_simplex 1 (ul:(real^3)list) = truncate_simplex 1 vl`]);
348 (SIMP_TAC[ASSUME `k = 2`; MCELL_EXPLICIT; mcell2]);
352 `truncate_simplex 1 (ul:(real^3)list) = truncate_simplex 1 vl`]);
354 (REWRITE_TAC[ASSUME `mxi V ul = mxi V vl`]);
355 (REWRITE_WITH `omega_list_n V ul 3 = omega_list_n V vl 3`);
356 (FIRST_ASSUM MATCH_MP_TAC THEN ARITH_TAC);
357 (ASM_REWRITE_TAC[HD;TL]);
359 (NEW_GOAL `{u0, u1} = {v0, v1:real^3}`);
360 (REWRITE_WITH `{u0,u1:real^3} = set_of_list(truncate_simplex 1 ul)`);
361 (REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_1;
362 ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
363 (REWRITE_WITH `{v0,v1:real^3} = set_of_list(truncate_simplex 1 vl)`);
364 (ASM_REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_1]);
367 (ASM_CASES_TAC `u0 = v0:real^3`);
368 (NEW_GOAL `u1 = v1:real^3`);
369 (NEW_GOAL `~(u0 = u1:real^3)`);
371 (NEW_GOAL `LENGTH (truncate_simplex 1 (ul:(real^3)list)) = 1 + 1 /\
372 CARD (set_of_list (truncate_simplex 1 ul)) = 1 + 1`);
373 (MATCH_MP_TAC Rogers.BARV_IMP_LENGTH_EQ_CARD);
374 (EXISTS_TAC `V:real^3->bool` THEN STRIP_TAC);
376 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
377 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `1 <= 3`]);
378 (UP_ASM_TAC THEN REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_1;
379 ASSUME `ul = [u0;u1;u2;u3:real^3]`; ASSUME `u0 = u1:real^3`;
380 SET_RULE `{a,a} = {a}`; Geomdetail.CARD_SING; ARITH_RULE `~(1 = 1 + 1)`]);
381 (UP_ASM_TAC THEN UP_ASM_TAC THEN UP_ASM_TAC THEN SET_TAC[]);
384 (NEW_GOAL `u0 = v1:real^3`);
385 (UP_ASM_TAC THEN UP_ASM_TAC THEN SET_TAC[]);
386 (NEW_GOAL `u1 = v0:real^3`);
387 (DEL_TAC THEN UP_ASM_TAC THEN UP_ASM_TAC THEN SET_TAC[]);
392 (UP_ASM_TAC THEN REWRITE_TAC[GSYM (ASSUME
393 `truncate_simplex 1 ul = truncate_simplex 1 (vl:(real^3)list)`)]);
400 (* ========================================================================= *)
403 (ASM_CASES_TAC `k = 1`);
404 (NEW_GOAL `sqrt (&2) <= hl (ul:(real^3)list)`);
405 (UNDISCH_TAC `~(mcell k V ul = {})` THEN
406 SIMP_TAC[ASSUME `k = 1`; MCELL_EXPLICIT;mcell1]);
409 (NEW_GOAL `!i. 0 <= i /\ i <= 3
410 ==> omega_list_n V ul i = omega_list_n V vl i`);
411 (MATCH_MP_TAC NJIUTIU);
414 (NEW_GOAL `HD ul = HD (vl:(real^3)list)`);
415 (MATCH_MP_TAC ROGERS_INTER_V_LEMMA);
416 (EXISTS_TAC `V:real^3->bool`);
422 (NEW_GOAL `HD ul IN set_of_list (ul:(real^3)list)`);
423 (MATCH_MP_TAC Packing3.BARV_IMP_HD_IN_SET_OF_LIST);
424 (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]);
425 (NEW_GOAL `set_of_list (ul:(real^3)list) SUBSET V`);
426 (MATCH_MP_TAC Packing3.BARV_SUBSET);
427 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]);
429 (REWRITE_WITH `rogers V vl (HD ul) <=> HD ul IN rogers V vl`);
431 (REWRITE_TAC[GSYM (ASSUME `rogers V ul = rogers V vl`)]);
435 {HD ul, omega_list_n V ul 1, omega_list_n V ul 2, omega_list_n V ul 3}`);
436 (MATCH_MP_TAC ROGERS_EXPLICIT);
438 (MATCH_MP_TAC IN_SET_IMP_IN_CONVEX_HULL_SET);
441 (NEW_GOAL `sqrt (&2) <= hl (vl:(real^3)list)`);
442 (REWRITE_TAC[ARITH_RULE `a <= b <=> (b < a ==> F)`]);
444 (NEW_GOAL `hl vl = dist (omega_list V vl,HD vl)`);
445 (MATCH_MP_TAC WAUFCHE2);
446 (EXISTS_TAC `3` THEN REWRITE_TAC[IN] THEN ASM_REWRITE_TAC[]);
447 (NEW_GOAL `hl ul <= dist (omega_list V ul,HD ul)`);
448 (MATCH_MP_TAC WAUFCHE1);
449 (EXISTS_TAC `3` THEN REWRITE_TAC[IN] THEN ASM_REWRITE_TAC[]);
451 REWRITE_WITH `omega_list V ul = omega_list V vl /\ HD ul = HD vl`);
453 (ASM_REWRITE_TAC[OMEGA_LIST; LENGTH]);
454 (REWRITE_TAC[GSYM (ASSUME `ul = [u0;u1;u2;u3:real^3]`);
455 GSYM (ASSUME `vl = [v0;v1;v2;v3:real^3]`)]);
456 (FIRST_ASSUM MATCH_MP_TAC);
459 (ASM_REAL_ARITH_TAC);
461 (ASM_CASES_TAC `hl (truncate_simplex 1 (ul:(real^3)list)) < sqrt (&2)`);
462 (NEW_GOAL `truncate_simplex 1 (ul:(real^3)list) = truncate_simplex 1 vl`);
463 (MATCH_MP_TAC TEZFFSK);
464 (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[ARITH_RULE `1 <= 3`]);
466 (SIMP_TAC[ASSUME `k = 1`; MCELL_EXPLICIT; mcell1]);
470 `truncate_simplex 1 (ul:(real^3)list) = truncate_simplex 1 vl`;
471 ASSUME `HD ul = HD (vl:(real^3)list)`; ASSUME `rogers V ul = rogers V vl`]);
472 (REWRITE_WITH `HD (TL ul) = EL 1 (truncate_simplex 1 (ul:(real^3)list))`);
474 `ul = [u0;u1;u2;u3:real^3]`;TRUNCATE_SIMPLEX_EXPLICIT_1]);
475 (REWRITE_TAC[EL; HD; TL; ARITH_RULE `1 = SUC 0`]);
476 (REWRITE_WITH `HD (TL vl) = EL 1 (truncate_simplex 1 (vl:(real^3)list))`);
477 (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);
478 (REWRITE_TAC[EL; HD; TL; ARITH_RULE `1 = SUC 0`]);
488 (NEW_GOAL `sqrt (&2) <= hl (truncate_simplex 1 (ul:(real^3)list))`);
489 (ASM_REAL_ARITH_TAC);
491 (NEW_GOAL `sqrt (&2) <= hl (truncate_simplex 1 (vl:(real^3)list))`);
492 (REWRITE_TAC[ARITH_RULE `a <= b <=> (b < a ==> F)`]);
494 (ABBREV_TAC `zl = truncate_simplex 1 (vl:(real^3)list)`);
495 (NEW_GOAL `hl zl = dist (omega_list V zl,HD zl)`);
496 (MATCH_MP_TAC WAUFCHE2);
497 (EXISTS_TAC `1` THEN REWRITE_TAC[IN] THEN ASM_REWRITE_TAC[]);
498 (EXPAND_TAC "zl" THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
499 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `1 <= 3`]);
501 (ABBREV_TAC `wl = truncate_simplex 1 (ul:(real^3)list)`);
502 (NEW_GOAL `hl wl <= dist (omega_list V wl,HD wl)`);
503 (MATCH_MP_TAC WAUFCHE1);
504 (EXISTS_TAC `1` THEN REWRITE_TAC[IN] THEN ASM_REWRITE_TAC[]);
505 (EXPAND_TAC "wl" THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
506 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `1 <= 3`]);
509 REWRITE_WITH `omega_list V wl = omega_list_n V ul 1 /\ HD wl = HD ul`);
512 (MATCH_MP_TAC Packing3.OMEGA_LIST_LEMMA);
513 (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC);
515 (MATCH_MP_TAC Packing3.HD_TRUNCATE_SIMPLEX);
516 (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC);
518 (UNDISCH_TAC `hl zl = dist (omega_list V zl,HD zl)` THEN
519 REWRITE_WITH `omega_list V zl = omega_list_n V vl 1 /\ HD zl = HD vl`);
522 (MATCH_MP_TAC Packing3.OMEGA_LIST_LEMMA);
523 (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC);
525 (MATCH_MP_TAC Packing3.HD_TRUNCATE_SIMPLEX);
526 (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC);
528 (REWRITE_WITH `omega_list_n V ul 1 = omega_list_n V vl 1`);
529 (FIRST_ASSUM MATCH_MP_TAC);
531 (REWRITE_TAC[ASSUME `HD (ul:(real^3)list) = HD (vl:(real^3)list)`]);
532 (ASM_REAL_ARITH_TAC);
534 (SIMP_TAC[ASSUME `k = 1`; MCELL_EXPLICIT; mcell1]);
539 `rcone_gt (HD (ul:(real^3)list)) (HD (TL ul))
540 (hl (truncate_simplex 1 ul) / sqrt (&2)) = {}`);
541 (MATCH_MP_TAC RCONE_GT_EQ_EMPTY_LEMMA);
542 (ONCE_REWRITE_TAC[REAL_ARITH `a >= b <=> b <= a`]);
543 (REWRITE_WITH `&1 <= hl (truncate_simplex 1 (ul:(real^3)list)) / sqrt (&2)
544 <=> &1 * sqrt (&2) <= hl (truncate_simplex 1 ul)`);
545 (MATCH_MP_TAC REAL_LE_RDIV_EQ);
546 (MATCH_MP_TAC SQRT_POS_LT);
548 (REWRITE_TAC[REAL_MUL_LID] THEN ASM_REAL_ARITH_TAC);
551 `rcone_gt (HD (vl:(real^3)list)) (HD (TL vl))
552 (hl (truncate_simplex 1 vl) / sqrt (&2)) = {}`);
553 (MATCH_MP_TAC RCONE_GT_EQ_EMPTY_LEMMA);
554 (ONCE_REWRITE_TAC[REAL_ARITH `a >= b <=> b <= a`]);
555 (REWRITE_WITH `&1 <= hl (truncate_simplex 1 (vl:(real^3)list)) / sqrt (&2)
556 <=> &1 * sqrt (&2) <= hl (truncate_simplex 1 vl)`);
557 (MATCH_MP_TAC REAL_LE_RDIV_EQ);
558 (MATCH_MP_TAC SQRT_POS_LT);
560 (REWRITE_TAC[REAL_MUL_LID] THEN ASM_REAL_ARITH_TAC);
570 (* ========================================================================= *)
575 (SIMP_TAC[ASSUME `k = 0`; MCELL_EXPLICIT; mcell0]);
576 (REWRITE_TAC[ASSUME `rogers V ul = rogers V vl`]);
578 (NEW_GOAL `!i. 0 <= i /\ i <= 3
579 ==> omega_list_n V ul i = omega_list_n V vl i`);
580 (MATCH_MP_TAC NJIUTIU);
583 (REWRITE_WITH `HD ul = HD (vl:(real^3)list)`);
584 (MATCH_MP_TAC ROGERS_INTER_V_LEMMA);
585 (EXISTS_TAC `V:real^3->bool`);
591 (NEW_GOAL `HD ul IN set_of_list (ul:(real^3)list)`);
592 (MATCH_MP_TAC Packing3.BARV_IMP_HD_IN_SET_OF_LIST);
593 (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]);
594 (NEW_GOAL `set_of_list (ul:(real^3)list) SUBSET V`);
595 (MATCH_MP_TAC Packing3.BARV_SUBSET);
596 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]);
598 (REWRITE_WITH `rogers V vl (HD ul) <=> HD ul IN rogers V vl`);
600 (REWRITE_TAC[GSYM (ASSUME `rogers V ul = rogers V vl`)]);
604 {HD ul, omega_list_n V ul 1, omega_list_n V ul 2, omega_list_n V ul 3}`);
605 (MATCH_MP_TAC ROGERS_EXPLICIT);
607 (MATCH_MP_TAC IN_SET_IMP_IN_CONVEX_HULL_SET);