1 (* ========================================================================= *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
4 (* Authour : VU KHAC KY *)
5 (* Book lemma: LEPJBDJ *)
6 (* Chaper : Packing (Marchal cells) *)
8 (* ========================================================================= *)
10 (* ========================================================================= *)
11 (* FILES NEED TO BE LOADED *)
13 (* flyspeck_needs "packing/marchal_cells_2.hl";; *)
15 (* ========================================================================= *)
16 module Lepjbdj = struct
19 (* open Prove_by_refinement;; *)
20 open Vukhacky_tactics;;
27 open Marchal_cells_2_new;;
29 let LEPJBDJ_concl = `!V ul k.
30 saturated V /\ packing V /\ barV V 3 ul /\ (1 <= k) /\ (k <= 4) /\
31 ~(mcell k V ul = {})==>
32 (V INTER mcell k V ul = set_of_list (truncate_simplex (k-1) ul))`;;
39 ==> V INTER mcell 0 V ul = {}`;;
41 (* ========================================================================= *)
43 let LEPJBDJ = prove_by_refinement (
46 (NEW_GOAL `?u0 u1 u2 u3. ul = [u0;u1;u2;u3:real^3]`);
47 (MATCH_MP_TAC BARV_3_EXPLICIT);
48 (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]);
49 (UP_ASM_TAC THEN STRIP_TAC);
50 (NEW_GOAL `~(u0 = u1:real^3)`);
52 (NEW_GOAL `CARD {u0,u1,u2,u3:real^3} = 4`);
53 (REWRITE_WITH `{u0,u1,u2,u3:real^3} = set_of_list ul`);
54 (ASM_REWRITE_TAC[set_of_list]);
55 (REWRITE_WITH `LENGTH (ul:(real^3)list) = 3 + 1 /\ CARD (set_of_list ul) = 3 + 1`);
56 (MATCH_MP_TAC Rogers.BARV_IMP_LENGTH_EQ_CARD);
57 (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]);
59 (UP_ASM_TAC THEN ASM_REWRITE_TAC[SET_RULE `{a,a,b,c} = {a,b,c}`]);
60 (NEW_GOAL `CARD {u1,u2,u3:real^3} <= 3`);
61 (REWRITE_TAC[Geomdetail.CARD3]);
64 (*==== Next, we will consider 4 case of k = 1,2,3 and k >= 4 ======= *)
65 (* -------------------------------------------------------------------- *)
66 (ASM_CASES_TAC `k = 1`);
67 (ASM_REWRITE_TAC[ARITH_RULE `1 - 1 = 0`; TRUNCATE_SIMPLEX_EXPLICIT_0; set_of_list; MCELL_EXPLICIT; mcell1; HD;TL; TRUNCATE_SIMPLEX_EXPLICIT_1]);
69 (REWRITE_TAC[SET_EQ_LEMMA; IN_SING]);
71 (NEW_GOAL `x IN V INTER cball (u0:real^3,sqrt (&2))`);
72 (UP_ASM_TAC THEN SET_TAC[]);
73 (UP_ASM_TAC THEN REWRITE_TAC[IN_INTER; cball]);
74 (STRIP_TAC THEN UP_ASM_TAC THEN REWRITE_TAC[IN;IN_ELIM_THM] THEN STRIP_TAC);
75 (UNDISCH_TAC `packing (V:real^3->bool)` THEN REWRITE_TAC[packing]);
77 (ASM_CASES_TAC `x = u0:real^3`);
80 (NEW_GOAL `&2 <= dist (u0,x:real^3)`);
81 (FIRST_ASSUM MATCH_MP_TAC);
84 (ONCE_REWRITE_TAC[GSYM IN] THEN MATCH_MP_TAC (SET_RULE `(?b. a IN b /\ b SUBSET c) ==> a IN c`));
85 (EXISTS_TAC `set_of_list (ul:(real^3)list)`);
87 (ASM_REWRITE_TAC[set_of_list] THEN SET_TAC[]);
88 (MATCH_MP_TAC Packing3.BARV_SUBSET);
89 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]);
90 (UNDISCH_TAC `x:real^3 IN V` THEN REWRITE_TAC[IN]);
91 (NEW_GOAL `sqrt (&2) < &2`);
92 (REWRITE_TAC[SQRT2_LT_2]);
96 (REWRITE_TAC[IN_INTER; IN_DIFF]);
97 (REPEAT STRIP_TAC); (* break into 3 subgoals *)
100 (MATCH_MP_TAC (SET_RULE `(?b. a IN b /\ b SUBSET c) ==> a IN c`));
101 (EXISTS_TAC `set_of_list (ul:(real^3)list)`);
103 (ASM_REWRITE_TAC[set_of_list] THEN SET_TAC[]);
104 (MATCH_MP_TAC Packing3.BARV_SUBSET);
105 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]);
106 (REWRITE_TAC[GSYM (ASSUME `ul = [u0; u1; u2; u3:real^3]`)]);
107 (REWRITE_WITH `rogers V ul = convex hull
108 {HD ul, omega_list_n V ul 1, omega_list_n V ul 2, omega_list_n V ul 3}`);
109 (MATCH_MP_TAC ROGERS_EXPLICIT);
111 (ASM_REWRITE_TAC[HD]);
112 (MATCH_MP_TAC IN_SET_IMP_IN_CONVEX_HULL_SET);
114 (ASM_REWRITE_TAC[cball; IN; IN_ELIM_THM; DIST_REFL]);
115 (MATCH_MP_TAC SQRT_POS_LE);
117 (UP_ASM_TAC THEN ASM_REWRITE_TAC[rcone_gt; rconesgn; IN; IN_ELIM_THM;
118 VECTOR_SUB_REFL; DOT_LZERO; ARITH_RULE `~(a > b) <=> a <= b`; DIST_REFL;
119 REAL_MUL_LZERO; REAL_LE_REFL]);
121 (UNDISCH_TAC `~(mcell k V ul = {})`);
122 (ASM_REWRITE_TAC[MCELL_EXPLICIT; mcell1]);
125 (* -------------------------------------------------------------------- *)
126 (ASM_CASES_TAC `k = 2`);
127 (ASM_REWRITE_TAC[ARITH_RULE `2 - 1 = 1`; TRUNCATE_SIMPLEX_EXPLICIT_1;
128 MCELL_EXPLICIT; mcell2;HD;TL]);
131 (NEW_GOAL `hl [u0;u1:real^3] = inv(&2) * dist (u1,u0)`);
132 (REWRITE_WITH `hl [u0;u1:real^3] =
133 dist (circumcenter (set_of_list [u0;u1]),HD [u0;u1])`);
134 (MATCH_MP_TAC Rogers.HL_EQ_DIST0);
135 (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `1`);
137 (REWRITE_WITH `[u0;u1:real^3] = truncate_simplex 1 ul`);
138 (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);
139 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
140 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `1 <= 3`]);
141 (REWRITE_TAC[set_of_list; Rogers.CIRCUMCENTER_2; midpoint; HD; dist]);
144 (NEW_GOAL `&0 < a /\ a < &1`);
147 (MATCH_MP_TAC REAL_LT_DIV);
148 (SIMP_TAC[SQRT_POS_LT; ARITH_RULE `&0 < &2`]);
150 (MATCH_MP_TAC REAL_LT_MUL);
151 (ASM_SIMP_TAC[REAL_LT_INV; ARITH_RULE `&0 < &2`]);
152 (MATCH_MP_TAC DIST_POS_LT THEN ASM_MESON_TAC[]);
153 (REWRITE_WITH `hl [u0; u1:real^3] / sqrt (&2) < &1 <=>
154 hl [u0; u1] < &1 * sqrt (&2)`);
155 (MATCH_MP_TAC REAL_LT_LDIV_EQ);
156 (SIMP_TAC[SQRT_POS_LT; ARITH_RULE `&0 < &2`]);
157 (REWRITE_TAC[REAL_MUL_LID]);
161 (REWRITE_TAC[set_of_list; SET_EQ_LEMMA]);
163 (ASM_CASES_TAC `x IN {u0,u1:real^3}`);
166 (SWITCH_TAC THEN UP_ASM_TAC THEN REWRITE_TAC[IN_INTER] THEN STRIP_TAC);
169 (ABBREV_TAC `v = proj_point (u1 - u0:real^3) (x - u0) `);
170 (NEW_GOAL `(x - u0 - v:real^3) dot (u1 - u0) = &0`);
172 (REWRITE_TAC[GSYM projection_proj_point]);
173 (REWRITE_TAC[Packing3.PROJECTION_ORTHOGONAL]);
175 (NEW_GOAL `between (v+u0) (u0,u1:real^3)`);
176 (ASM_CASES_TAC `between (v+u0) (u0,u1:real^3)`);
178 (NEW_GOAL `between (v+u0) (u0,u1:real^3) \/ between u0 (u1,v+u0) \/ between u1 (v+u0,u0)`);
179 (REWRITE_TAC[GSYM COLLINEAR_BETWEEN_CASES]);
180 (MATCH_MP_TAC Collect_geom.IN_AFFINE_HULL_IMP_COLLINEAR);
181 (REWRITE_TAC[AFFINE_HULL_2; IN_ELIM_THM; IN]);
183 (REWRITE_TAC[PRO_EXP]);
184 (ABBREV_TAC `t = ((x - u0) dot (u1 - u0)) / ((u1 - u0) dot (u1 - u0):real^3)`);
185 (EXISTS_TAC `(&1 - t)` THEN EXISTS_TAC `t:real`);
186 (REWRITE_TAC[REAL_ARITH `(&1 - t) + t = &1`]);
189 (UP_ASM_TAC THEN ASM_REWRITE_TAC[] THEN STRIP_TAC);
191 (UNDISCH_TAC `x:real^3 IN rcone_ge u0 u1 a`);
192 (REWRITE_TAC[rcone_ge;rconesgn;IN;IN_ELIM_THM; ARITH_RULE `~(a >= b) <=> a < b`]);
193 (NEW_GOAL `(x - u0) dot (u1 - u0:real^3) <= &0`);
194 (UP_ASM_TAC THEN REWRITE_TAC[BETWEEN_IN_CONVEX_HULL; CONVEX_HULL_2;
195 IN;IN_ELIM_THM] THEN STRIP_TAC);
196 (REWRITE_WITH `(x - u0) dot (u1 - u0:real^3) = (x - u0 - v) dot (u1 - u0) +
199 (REWRITE_TAC[ASSUME `(x - u0 - v) dot (u1 - u0:real^3) = &0`; REAL_ADD_LID]);
200 (MP_TAC (ASSUME `u0 = u % u1 + v' % (v + u0:real^3)`) THEN
201 REWRITE_WITH `u0 = u % u1 + v' % (v + u0:real^3)
202 <=> (u + v') % u0 = u % u1 + v' % (v + u0)`);
205 (REWRITE_TAC[VECTOR_ARITH `(u + v') % u0 = u % u1 + v' % (v + u0)
206 <=> u % (u0 - u1) = v' % v`]);
209 (REWRITE_WITH `u % (u0 - u1) = v' % v <=> u / v' % (u0 - u1:real^3) = v`);
210 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
211 (MATCH_MP_TAC Trigonometry2.VEC_DIV_MOV);
213 (MP_TAC (ASSUME `u0 = u % u1 + v' % (v + u0:real^3)`));
214 (REWRITE_WITH `u = &1 /\ v' = &0`);
215 (ASM_REAL_ARITH_TAC);
216 (ASM_REWRITE_TAC[VECTOR_MUL_LID; VECTOR_MUL_LZERO; VECTOR_ADD_RID]);
217 (ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN STRIP_TAC);
219 (REWRITE_TAC[DOT_LMUL]);
220 (REWRITE_WITH `(u0 - u1) dot (u1 - u0) = --((u0 - u1:real^3) dot (u0 - u1))`);
222 (REWRITE_TAC[DOT_SQUARE_NORM]);
223 (REWRITE_TAC[REAL_ARITH `a * -- b <= &0 <=> &0 <= a * b`]);
224 (MATCH_MP_TAC REAL_LE_MUL);
225 (REWRITE_TAC[REAL_LE_POW_2]);
226 (MATCH_MP_TAC REAL_LE_DIV);
228 (NEW_GOAL `&0 < dist (x,u0) * dist (u1,u0:real^3) * a`);
229 (MATCH_MP_TAC REAL_LT_MUL);
231 (MATCH_MP_TAC DIST_POS_LT);
233 (MATCH_MP_TAC REAL_LT_MUL);
235 (MATCH_MP_TAC DIST_POS_LT);
238 (ASM_REAL_ARITH_TAC);
242 (UNDISCH_TAC `x:real^3 IN rcone_ge u1 u0 a`);
243 (REWRITE_TAC[rcone_ge;rconesgn;IN;IN_ELIM_THM; ARITH_RULE `~(a >= b) <=> a < b`]);
244 (NEW_GOAL `(x - u1) dot (u0 - u1:real^3) <= &0`);
245 (UP_ASM_TAC THEN REWRITE_TAC[BETWEEN_IN_CONVEX_HULL; CONVEX_HULL_2;
246 IN;IN_ELIM_THM] THEN STRIP_TAC);
247 (REWRITE_WITH `(x - u1) dot (u0 - u1:real^3) =
248 --((x - u0 - v) dot (u1 - u0)) + (v + u0 - u1) dot (u0 - u1)`);
250 (REWRITE_TAC[ASSUME `(x - u0 - v) dot (u1 - u0:real^3) = &0`;
251 REAL_NEG_0; REAL_ADD_LID]);
254 (MP_TAC (ASSUME `u1 = u % (v + u0) + v' % u0:real^3`) THEN
255 REWRITE_WITH `u1 = u % (v + u0) + v' % u0
256 <=> u1 = u % v + (u + v') % u0:real^3`);
258 (REWRITE_TAC[ASSUME `u + v' = &1`; VECTOR_ARITH `&1 % a = a`]);
259 (REWRITE_TAC[VECTOR_ARITH `u1 = u % v + u0 <=> &1 % (u1 - u0:real^3) = u % v`]);
260 (REWRITE_WITH `&1 % (u1 - u0) = u % v <=> &1 / u % (u1 - u0:real^3) = v`);
262 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
263 (MATCH_MP_TAC Trigonometry2.VEC_DIV_MOV);
265 (MP_TAC (ASSUME `u1 = u % (v + u0) + v' % u0:real^3`));
266 (REWRITE_WITH `u = &0 /\ v' = &1`);
267 (ASM_REAL_ARITH_TAC);
268 (REWRITE_TAC[VECTOR_MUL_LID; VECTOR_MUL_LZERO; VECTOR_ADD_LID]);
270 (ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN STRIP_TAC);
271 (REWRITE_WITH `v + u0 - u1 = (&1 / u - &1) % (u1 - u0:real^3)`);
273 (REWRITE_TAC[ASSUME `v = &1 / u % (u1 - u0:real^3)`]);
275 (REWRITE_TAC[DOT_LMUL]);
277 (REWRITE_WITH `(u1 - u0) dot (u0 - u1) = --((u0 - u1:real^3) dot (u0 - u1))`);
279 (REWRITE_TAC[DOT_SQUARE_NORM]);
281 (REWRITE_TAC[REAL_ARITH `a * -- b <= &0 <=> &0 <= a * b`]);
283 (MATCH_MP_TAC REAL_LE_MUL);
284 (REWRITE_TAC[REAL_LE_POW_2]);
286 (REWRITE_TAC[REAL_ARITH `&0 <= a - b <=> b <= a`]);
288 (REWRITE_WITH `&1 <= &1 / u <=> &1 * u <= &1`);
289 (MATCH_MP_TAC REAL_LE_RDIV_EQ);
290 (ASM_CASES_TAC `u = &0`);
292 (MP_TAC (ASSUME `u1 = u % (v + u0) + v' % u0:real^3`));
293 (REWRITE_WITH `u = &0 /\ v' = &1`);
294 (ASM_REAL_ARITH_TAC);
295 (REWRITE_TAC[VECTOR_MUL_LID; VECTOR_MUL_LZERO; VECTOR_ADD_LID]);
298 (ASM_REAL_ARITH_TAC);
299 (REWRITE_TAC[REAL_MUL_LID]);
300 (ASM_REAL_ARITH_TAC);
302 (NEW_GOAL `&0 < dist (x,u1) * dist (u0,u1:real^3) * a`);
303 (MATCH_MP_TAC REAL_LT_MUL);
305 (MATCH_MP_TAC DIST_POS_LT);
307 (MATCH_MP_TAC REAL_LT_MUL);
309 (MATCH_MP_TAC DIST_POS_LT);
312 (ASM_REAL_ARITH_TAC);
314 (* Finish proving that (v + u0) is between u0 and u1 *)
315 (* ================================================= *)
317 (NEW_GOAL `norm (x - u0) pow 2 = norm ((u0 + v) - u0) pow 2 + norm (x - (u0 + v):real^3) pow 2`);
318 (MATCH_MP_TAC PYTHAGORAS);
319 (REWRITE_TAC[orthogonal]);
320 (REWRITE_TAC[VECTOR_ARITH `a:real^3 - (a + b) = --b`]);
321 (REWRITE_TAC[VECTOR_ARITH `--v dot (x - (u0 + v)) = -- ((x - u0 - v) dot v)`]);
322 (REWRITE_WITH `(x - u0 - v) dot v = (x - u0 - v) dot proj_point (u1 - u0) (x - u0:real^3)`);
324 (REWRITE_TAC[PRO_EXP]);
325 (REWRITE_TAC[DOT_RMUL]);
326 (ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);
328 (NEW_GOAL `norm (x - u1) pow 2 = norm ((u0 + v) - u1) pow 2 + norm (x - (u0 + v):real^3) pow 2`);
329 (MATCH_MP_TAC PYTHAGORAS);
330 (REWRITE_TAC[orthogonal]);
331 (REWRITE_TAC[VECTOR_ARITH `(u1 - (u0 + v)) dot (x - (u0 + v)) = ((x - u0 - v) dot (u1 - (u0 + v)))`]);
332 (REWRITE_WITH `(x - u0 - v) dot (u1 - (u0 + v)) =
333 (x - u0 - v) dot (u1 - u0 - proj_point (u1 - u0) (x - u0:real^3))`);
336 (REWRITE_TAC[PRO_EXP]);
337 (ABBREV_TAC `t = ((x - u0) dot (u1 - u0)) / ((u1 - u0) dot (u1 - u0:real^3))`);
338 (REWRITE_TAC[VECTOR_ARITH `a - b - t% (a - b) = (&1 - t) % (a - b)`]);
339 (REWRITE_TAC[DOT_RMUL]);
340 (ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);
342 (* important lemma *)
343 (NEW_GOAL `sqrt (&2) <= dist (u0 + v,u0:real^3)`);
344 (UNDISCH_TAC `x:real^3 IN rcone_ge u0 u1 a`);
345 (REWRITE_TAC[rcone_ge; rconesgn; IN; IN_ELIM_THM]);
346 (REWRITE_WITH `(x - u0) dot (u1 - u0) = (x - u0 - v:real^3) dot (u1 - u0) + ((v+u0) - u0) dot (u1 - u0)`);
348 (ASM_REWRITE_TAC[REAL_ADD_LID]);
350 (REWRITE_TAC[ASSUME `hl [u0;u1:real^3] = inv (&2) * dist (u1,u0)`]);
352 (REWRITE_WITH `((v + u0) - u0) dot (u1 - u0) = dist (u0 + v, u0) * dist (u1,u0:real^3)`);
353 (REWRITE_WITH `v + u0 = u0 + v:real^3`);
355 (REWRITE_TAC[dist; NORM_CAUCHY_SCHWARZ_EQ]);
356 (UNDISCH_TAC `between (v + u0) (u0,u1:real^3)` THEN
357 REWRITE_TAC[BETWEEN_IN_CONVEX_HULL; CONVEX_HULL_2; IN;
358 IN_ELIM_THM] THEN STRIP_TAC);
359 (UP_ASM_TAC THEN REWRITE_WITH `v + u0 = u0 + v:real^3`);
363 (REWRITE_WITH `(u % u0 + v' % u1) - u0:real^3 = (u % u0 + v' % u1) - (u + v') % u0`);
364 (ASM_REWRITE_TAC[VECTOR_MUL_LID]);
365 (REWRITE_WITH `(u % u0 + v' % u1) - (u + v') % u0 = v' % (u1 - u0:real^3)`);
367 (REWRITE_TAC[NORM_MUL; VECTOR_MUL_ASSOC]);
368 (AP_THM_TAC THEN AP_TERM_TAC);
369 (REWRITE_WITH `abs v' = v'`);
370 (ASM_REWRITE_TAC[REAL_ABS_REFL]);
372 (REWRITE_TAC[REAL_ARITH `a * b >= c * b * d <=> &0 <= (a - c* d) * b`]);
373 (REWRITE_WITH `&0 <= (dist (u0 + v,u0) - dist (x,u0) * (inv (&2) * dist (u1,u0)) / sqrt (&2)) * dist (u1,u0) <=> &0 <= dist (u0 + v,u0:real^3) - dist (x,u0) * (inv (&2) * dist (u1,u0:real^3)) / sqrt (&2)`);
374 (MP_TAC REAL_LE_MUL_EQ);
376 (FIRST_ASSUM MATCH_MP_TAC);
377 (MATCH_MP_TAC DIST_POS_LT);
381 (NEW_GOAL `&0 <= dist (x,u0:real^3) * (inv (&2) * dist (u1,u0)) / sqrt (&2) - dist (u1,u0) / sqrt (&2)`);
382 (REWRITE_TAC[REAL_ARITH `a * (b * c)/d - c/d = (a * b - &1) * (c/d)`]);
383 (MATCH_MP_TAC REAL_LE_MUL);
384 (ASM_SIMP_TAC[REAL_LE_DIV; DIST_POS_LE; SQRT_POS_LE; REAL_ARITH `&0 <= &2`]);
385 (NEW_GOAL `&2 <= dist (x,u0:real^3)`);
386 (UNDISCH_TAC `packing (V:real^3->bool)` );
387 (REWRITE_TAC[packing]);
388 (STRIP_TAC THEN FIRST_ASSUM MATCH_MP_TAC);
390 (ONCE_REWRITE_TAC[GSYM IN]);
392 (ONCE_REWRITE_TAC[GSYM IN]);
393 (MATCH_MP_TAC (SET_RULE `(?b. a IN b /\ b SUBSET c) ==> a IN c`));
394 (EXISTS_TAC `set_of_list (ul:(real^3)list)`);
396 (ASM_REWRITE_TAC[set_of_list] THEN SET_TAC[]);
397 (MATCH_MP_TAC Packing3.BARV_SUBSET);
398 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]);
400 (NEW_GOAL `&0 <= dist (x,u0:real^3) * inv (&2) - &2 * inv (&2)`);
401 (REWRITE_TAC[REAL_ARITH `a * x - b * x = (a - b) * x`]);
402 (MATCH_MP_TAC REAL_LE_MUL);
404 (ASM_REAL_ARITH_TAC);
405 (ASM_SIMP_TAC[REAL_LE_INV; REAL_ARITH `&0 <= &2`]);
406 (NEW_GOAL `&2 * inv (&2) = &1`);
407 (ASM_SIMP_TAC [REAL_ARITH `~(&2 = &0)`; REAL_MUL_RINV]);
408 (ASM_REAL_ARITH_TAC);
409 (NEW_GOAL `dist (u1,u0) / sqrt (&2) <= dist (u0 + v,u0:real^3)`);
410 (ASM_REAL_ARITH_TAC);
411 (NEW_GOAL `sqrt (&2) <= dist (u1,u0:real^3) / sqrt (&2)`);
412 (REWRITE_WITH `sqrt (&2) <= dist (u1,u0:real^3) / sqrt (&2)
413 <=> sqrt (&2) * sqrt (&2) <= dist (u1,u0:real^3)`);
414 (MATCH_MP_TAC REAL_LE_RDIV_EQ);
415 (ASM_SIMP_TAC[SQRT_POS_LT; REAL_ARITH `&0 < &2`]);
416 (SIMP_TAC[GSYM REAL_POW_2; SQRT_POW_2; REAL_ARITH `&0 <= &2`]);
417 (UNDISCH_TAC `packing (V:real^3->bool)` );
418 (REWRITE_TAC[packing]);
419 (STRIP_TAC THEN FIRST_ASSUM MATCH_MP_TAC);
420 (NEW_GOAL `{u0,u1:real^3} SUBSET V`);
421 (MATCH_MP_TAC (SET_RULE `(?b. a SUBSET b /\ b SUBSET c) ==> a SUBSET c`));
422 (EXISTS_TAC `set_of_list (ul:(real^3)list)`);
424 (ASM_REWRITE_TAC[set_of_list] THEN SET_TAC[]);
425 (MATCH_MP_TAC Packing3.BARV_SUBSET);
426 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]);
428 (ASM_REAL_ARITH_TAC);
430 (* continue the next important lemma, similarly as above *)
432 (NEW_GOAL `sqrt (&2) <= dist (u0 + v,u1:real^3)`);
433 (UNDISCH_TAC `x:real^3 IN rcone_ge u1 u0 a`);
434 (REWRITE_TAC[rcone_ge; rconesgn; IN; IN_ELIM_THM]);
435 (REWRITE_WITH `(x - u1) dot (u0 - u1) = --((x - u0 - v:real^3) dot (u1 - u0)) + ((v+u0) - u1) dot (u0 - u1)`);
437 (ASM_REWRITE_TAC[REAL_ADD_LID;REAL_NEG_0]);
439 (REWRITE_TAC[ASSUME `hl [u0;u1:real^3] = inv (&2) * dist (u1,u0)`]);
441 (REWRITE_WITH `((v + u0) - u1) dot (u0 - u1) = dist (u0 + v, u1) * dist (u1,u0:real^3)`);
442 (REWRITE_WITH `v + u0 = u0 + v:real^3 /\ dist (u1,u0) = dist (u0,u1)`);
443 (REWRITE_TAC[DIST_SYM]);
445 (REWRITE_TAC[dist; NORM_CAUCHY_SCHWARZ_EQ]);
446 (UNDISCH_TAC `between (v + u0) (u0,u1:real^3)` THEN
447 REWRITE_TAC[BETWEEN_IN_CONVEX_HULL; CONVEX_HULL_2; IN;
448 IN_ELIM_THM] THEN STRIP_TAC);
449 (UP_ASM_TAC THEN REWRITE_WITH `v + u0 = u0 + v:real^3`);
454 (REWRITE_WITH `(u % u0 + v' % u1) - u1:real^3 = (u % u0 + v' % u1) - (u + v') % u1`);
455 (ASM_REWRITE_TAC[VECTOR_MUL_LID]);
456 (REWRITE_WITH `(u % u0 + v' % u1) - (u + v') % u1 = u % (u0 - u1:real^3)`);
458 (REWRITE_TAC[NORM_MUL; VECTOR_MUL_ASSOC]);
459 (AP_THM_TAC THEN AP_TERM_TAC);
460 (REWRITE_WITH `abs u = u`);
461 (ASM_REWRITE_TAC[REAL_ABS_REFL]);
463 (REWRITE_WITH `dist (u0,u1:real^3) = dist (u1,u0)`);
464 (REWRITE_TAC[DIST_SYM]);
465 (REWRITE_TAC[REAL_ARITH `a * b >= c * b * d <=> &0 <= (a - c* d) * b`]);
466 (REWRITE_WITH `&0 <= (dist (u0 + v,u1) - dist (x,u1) * (inv (&2) * dist (u1,u0)) / sqrt (&2)) * dist (u1,u0) <=> &0 <= dist (u0 + v,u1:real^3) - dist (x,u1) * (inv (&2) * dist (u1,u0:real^3)) / sqrt (&2)`);
467 (MP_TAC REAL_LE_MUL_EQ);
469 (FIRST_ASSUM MATCH_MP_TAC);
470 (MATCH_MP_TAC DIST_POS_LT);
474 (NEW_GOAL `&0 <= dist (x,u1:real^3) * (inv (&2) * dist (u1,u0)) / sqrt (&2) - dist (u1,u0) / sqrt (&2)`);
475 (REWRITE_TAC[REAL_ARITH `a * (b * c)/d - c/d = (a * b - &1) * (c/d)`]);
476 (MATCH_MP_TAC REAL_LE_MUL);
477 (ASM_SIMP_TAC[REAL_LE_DIV; DIST_POS_LE; SQRT_POS_LE; REAL_ARITH `&0 <= &2`]);
478 (NEW_GOAL `&2 <= dist (x,u1:real^3)`);
479 (UNDISCH_TAC `packing (V:real^3->bool)` );
480 (REWRITE_TAC[packing]);
481 (STRIP_TAC THEN FIRST_ASSUM MATCH_MP_TAC);
483 (ONCE_REWRITE_TAC[GSYM IN]);
485 (ONCE_REWRITE_TAC[GSYM IN]);
486 (MATCH_MP_TAC (SET_RULE `(?b. a IN b /\ b SUBSET c) ==> a IN c`));
487 (EXISTS_TAC `set_of_list (ul:(real^3)list)`);
489 (ASM_REWRITE_TAC[set_of_list] THEN SET_TAC[]);
490 (MATCH_MP_TAC Packing3.BARV_SUBSET);
491 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]);
493 (NEW_GOAL `&0 <= dist (x,u1:real^3) * inv (&2) - &2 * inv (&2)`);
494 (REWRITE_TAC[REAL_ARITH `a * x - b * x = (a - b) * x`]);
495 (MATCH_MP_TAC REAL_LE_MUL);
497 (ASM_REAL_ARITH_TAC);
498 (ASM_SIMP_TAC[REAL_LE_INV; REAL_ARITH `&0 <= &2`]);
499 (NEW_GOAL `&2 * inv (&2) = &1`);
500 (ASM_SIMP_TAC [REAL_ARITH `~(&2 = &0)`; REAL_MUL_RINV]);
501 (ASM_REAL_ARITH_TAC);
502 (NEW_GOAL `dist (u1,u0) / sqrt (&2) <= dist (u0 + v,u1:real^3)`);
503 (ASM_REAL_ARITH_TAC);
504 (NEW_GOAL `sqrt (&2) <= dist (u1,u0:real^3) / sqrt (&2)`);
505 (REWRITE_WITH `sqrt (&2) <= dist (u1,u0:real^3) / sqrt (&2)
506 <=> sqrt (&2) * sqrt (&2) <= dist (u1,u0:real^3)`);
507 (MATCH_MP_TAC REAL_LE_RDIV_EQ);
508 (ASM_SIMP_TAC[SQRT_POS_LT; REAL_ARITH `&0 < &2`]);
509 (SIMP_TAC[GSYM REAL_POW_2; SQRT_POW_2; REAL_ARITH `&0 <= &2`]);
510 (UNDISCH_TAC `packing (V:real^3->bool)` );
511 (REWRITE_TAC[packing]);
512 (STRIP_TAC THEN FIRST_ASSUM MATCH_MP_TAC);
513 (NEW_GOAL `{u0,u1:real^3} SUBSET V`);
514 (MATCH_MP_TAC (SET_RULE `(?b. a SUBSET b /\ b SUBSET c) ==> a SUBSET c`));
515 (EXISTS_TAC `set_of_list (ul:(real^3)list)`);
517 (ASM_REWRITE_TAC[set_of_list] THEN SET_TAC[]);
518 (MATCH_MP_TAC Packing3.BARV_SUBSET);
519 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]);
521 (ASM_REAL_ARITH_TAC);
522 (UNDISCH_TAC `between (v + u0) (u0,u1:real^3)`);
523 (REWRITE_WITH `v + u0 = u0 + v:real^3`);
525 (REWRITE_TAC[between] THEN STRIP_TAC);
526 (NEW_GOAL `dist (u0,u1:real^3) = dist (u0 + v,u0) + dist (u0 + v,u1)`);
527 (ASM_MESON_TAC[DIST_SYM]);
528 (NEW_GOAL `&2 * sqrt (&2) <= dist (u0,u1:real^3)`);
529 (NEW_GOAL `&2 * sqrt (&2) <= dist (u0 + v,u0) + dist (u0 + v,u1:real^3)`);
530 (ASM_REAL_ARITH_TAC);
531 (ASM_REAL_ARITH_TAC);
532 (UP_ASM_TAC THEN REWRITE_WITH `dist (u0,u1) = &2 * hl [u0; u1:real^3]`);
533 (REWRITE_TAC[ASSUME `hl [u0; u1] = inv (&2) * dist (u1,u0:real^3)`]);
534 (REWRITE_TAC[REAL_ARITH `a * b * c = (a * b) * c`]);
535 (REWRITE_WITH `&2 * inv (&2) = &1`);
536 (ASM_SIMP_TAC[REAL_MUL_RINV; REAL_ARITH `~(&2 = &0)`]);
537 (REWRITE_TAC[DIST_SYM;REAL_MUL_LID]);
538 (REWRITE_TAC[REAL_ARITH `~(a * b <= a * c) <=> &0 < a * (b - c)`]);
539 (MATCH_MP_TAC REAL_LT_MUL);
540 (ASM_REAL_ARITH_TAC);
542 (* Finish the most difficult part in case k = 2 *)
544 (REWRITE_TAC[IN_INTER]);
546 (NEW_GOAL `{u0,u1:real^3} SUBSET V`);
547 (MATCH_MP_TAC (SET_RULE `(?b. a SUBSET b /\ b SUBSET c) ==> a SUBSET c`));
548 (EXISTS_TAC `set_of_list (ul:(real^3)list)`);
550 (ASM_REWRITE_TAC[set_of_list] THEN SET_TAC[]);
551 (MATCH_MP_TAC Packing3.BARV_SUBSET);
552 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]);
555 (REWRITE_TAC[rcone_ge; rconesgn; IN; IN_ELIM_THM]);
556 (ASM_CASES_TAC `x = u0:real^3`);
557 (ASM_REWRITE_TAC[VECTOR_ARITH `(a - a) dot b = &0`; DIST_REFL; REAL_MUL_LZERO; REAL_ARITH `&0 >= &0`]);
558 (ASM_CASES_TAC `x = u1:real^3`);
559 (ASM_REWRITE_TAC[GSYM NORM_POW_2; GSYM dist; REAL_POW_2;
560 REAL_ARITH `a * a >= a * a * c <=> &0 <= a * a * (&1 - c)`]);
561 (MATCH_MP_TAC REAL_LE_MUL);
562 (ASM_SIMP_TAC[DIST_POS_LE]);
563 (MATCH_MP_TAC REAL_LE_MUL);
564 (ASM_SIMP_TAC[DIST_POS_LE]);
565 (ASM_REAL_ARITH_TAC);
570 (REWRITE_TAC[rcone_ge; rconesgn; IN; IN_ELIM_THM]);
571 (ASM_CASES_TAC `x = u1:real^3`);
572 (ASM_REWRITE_TAC[VECTOR_ARITH `(a - a) dot b = &0`; DIST_REFL; REAL_MUL_LZERO; REAL_ARITH `&0 >= &0`]);
573 (ASM_CASES_TAC `x = u0:real^3`);
574 (ASM_REWRITE_TAC[GSYM NORM_POW_2; GSYM dist; REAL_POW_2;
575 REAL_ARITH `a * a >= a * a * c <=> &0 <= a * a * (&1 - c)`]);
576 (MATCH_MP_TAC REAL_LE_MUL);
577 (ASM_SIMP_TAC[DIST_POS_LE]);
578 (MATCH_MP_TAC REAL_LE_MUL);
579 (ASM_SIMP_TAC[DIST_POS_LE]);
580 (ASM_REAL_ARITH_TAC);
585 (ABBREV_TAC `m = mxi V [u0;u1;u2;u3:real^3]`);
586 (ABBREV_TAC `s = omega_list_n V [u0;u1;u2;u3:real^3] 3`);
587 (REWRITE_TAC[aff_ge_def; IN_AFFSIGN; sgn_ge]);
589 (ABBREV_TAC `f = (\t:real^3. if t = x then &1 else &0)`);
590 (EXISTS_TAC `f:real^3->real`);
596 (REWRITE_WITH `{u0, u1} UNION {m, s} = {m,s} UNION {u0,u1:real^3}`);
598 (REWRITE_WITH `sum ({m, s} UNION {u0, u1}) f = sum ({u0, u1:real^3}) f`);
599 (MATCH_MP_TAC SUM_UNION_LZERO);
600 (REWRITE_TAC[Geomdetail.FINITE6]);
601 (REPEAT STRIP_TAC THEN EXPAND_TAC "f");
607 (ASM_SIMP_TAC[Collect_geom.SUM_DIS2]);
621 (REWRITE_WITH `{u0, u1} UNION {m, s} = {m,s} UNION {u0,u1:real^3}`);
623 (REWRITE_WITH `vsum ({m:real^3, s} UNION {u0, u1}) (\x. f x % x)
624 = vsum ({u0,u1}) (\x. f x % x)`);
625 (MATCH_MP_TAC VSUM_UNION_LZERO);
626 (REWRITE_TAC[Geomdetail.FINITE6]);
627 (REPEAT STRIP_TAC THEN EXPAND_TAC "f");
633 (ASM_SIMP_TAC[Collect_geom.VSUM_DIS2]);
640 (ASM_REWRITE_TAC[] THEN VECTOR_ARITH_TAC);
642 (ASM_REWRITE_TAC[] THEN VECTOR_ARITH_TAC);
648 (UNDISCH_TAC `~(mcell k V ul = {})`);
649 (ASM_REWRITE_TAC[MCELL_EXPLICIT;mcell2]);
653 (UP_ASM_TAC THEN ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);
658 (* ========================================================================= *)
659 (* -------------------- k = 4 --------------------------------------------*)
661 (ASM_CASES_TAC `k = 4`);
662 (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_3; ARITH_RULE `4 - 1 = 3`;
664 (ASM_SIMP_TAC[MCELL_EXPLICIT; ARITH_RULE `4 >= 4`]);
665 (REWRITE_TAC[SET_EQ_LEMMA; IN_INTER]);
666 (REWRITE_TAC[mcell4]);
668 (REWRITE_TAC[set_of_list]);
671 (ABBREV_TAC `S = {u0, u1,u2, u3:real^3}`);
672 (ABBREV_TAC `s3 = omega_list V (ul:(real^3)list)`);
674 (ASM_CASES_TAC `(x:real^3) IN S`);
676 (NEW_GOAL `!x:real^3. x IN convex hull S /\ ~(x IN S)
677 ==> (?y. y IN S /\ norm (x - s3) < norm (y - s3))`);
678 (MATCH_MP_TAC SIMPLEX_FURTHEST_LT_2);
680 (REWRITE_TAC[Geomdetail.FINITE6]);
681 (NEW_GOAL `?y:real^3. y IN S /\ norm (x - s3) < norm (y - s3)`);
682 (FIRST_ASSUM MATCH_MP_TAC);
683 (ASM_REWRITE_TAC[IN]);
684 (UP_ASM_TAC THEN EXPAND_TAC "S" THEN STRIP_TAC);
685 (NEW_GOAL `s3 IN (voronoi_closed V (y:real^3))`);
687 (MATCH_MP_TAC (SET_RULE `(?b. a IN b /\ b SUBSET c) ==> a IN c`));
688 (EXISTS_TAC `voronoi_list V (ul:(real^3)list)`);
690 (MATCH_MP_TAC Packing3.OMEGA_LIST_IN_VORONOI_LIST);
691 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]);
692 (ASM_REWRITE_TAC[VORONOI_LIST; VORONOI_SET; set_of_list]);
693 (NEW_GOAL `y:real^3 IN S`);
696 (UP_ASM_TAC THEN REWRITE_TAC[voronoi_closed; IN; IN_ELIM_THM]);
697 (ONCE_REWRITE_TAC[DIST_SYM]);
701 (NEW_GOAL `norm (y - s3) <= norm (x - s3:real^3)`);
702 (FIRST_ASSUM MATCH_MP_TAC);
703 (UNDISCH_TAC `x:real^3 IN V` THEN MESON_TAC[IN]);
704 (ASM_REAL_ARITH_TAC);
706 (MATCH_MP_TAC (SET_RULE `(?b. a IN b /\ b SUBSET c ) ==> a IN c`));
707 (EXISTS_TAC `set_of_list (ul:(real^3)list)`);
709 (ASM_REWRITE_TAC[set_of_list]);
710 (MATCH_MP_TAC Packing3.BARV_SUBSET);
711 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]);
712 (UP_ASM_TAC THEN REWRITE_TAC[IN_SET_IMP_IN_CONVEX_HULL_SET]);
714 (UNDISCH_TAC `~(mcell k V ul = {})`);
715 (ASM_SIMP_TAC[MCELL_EXPLICIT; ARITH_RULE `4 >= 4`]);
716 (REWRITE_TAC[mcell4]);
724 (* ========================================================================= *)
725 (* -------------------- k = 3 --------------------------------------------*)
728 (ASM_CASES_TAC `k = 3`);
729 (NEW_GOAL `{u0,u1,u2,u3:real^3} SUBSET V`);
730 (REWRITE_WITH `{u0,u1,u2,u3:real^3} = set_of_list ul`);
731 (ASM_REWRITE_TAC[set_of_list]);
732 (MATCH_MP_TAC Packing3.BARV_SUBSET);
733 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]);
734 (ASM_REWRITE_TAC[ARITH_RULE `3 - 1 = 2`; TRUNCATE_SIMPLEX_EXPLICIT_2;
735 MCELL_EXPLICIT; mcell3; set_of_list]);
736 (ABBREV_TAC `m = mxi V [u0; u1; u2; u3:real^3]`);
737 (REWRITE_TAC[SET_RULE `{a,b,c} UNION {d} = {a,b,c,d}`]);
740 (REWRITE_TAC[set_of_list; SET_EQ_LEMMA; IN_INTER]);
742 (ASM_CASES_TAC `x IN {u0,u1,u2:real^3}`);
745 (ABBREV_TAC `S = {u0, u1,u2, m:real^3}`);
746 (ABBREV_TAC `s2 = omega_list_n V (ul:(real^3)list) 2`);
747 (ABBREV_TAC `s3 = omega_list V (ul:(real^3)list)`);
749 (NEW_GOAL `s2 IN voronoi_list V [u0;u1;u2:real^3]`);
751 (REWRITE_TAC[OMEGA_LIST_TRUNCATE_2; ASSUME `ul = [u0; u1; u2; u3:real^3]`]);
752 (MATCH_MP_TAC Packing3.OMEGA_LIST_IN_VORONOI_LIST);
754 (REWRITE_WITH `[u0;u1;u2:real^3] = truncate_simplex 2 ul`);
755 (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
756 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
757 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]);
759 (NEW_GOAL `s3:real^3 IN voronoi_list V ul`);
761 (MATCH_MP_TAC Packing3.OMEGA_LIST_IN_VORONOI_LIST);
762 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]);
764 (NEW_GOAL `s3:real^3 IN voronoi_list V [u0;u1;u2:real^3]`);
765 (NEW_GOAL `voronoi_list V ul SUBSET voronoi_list V [u0;u1;u2:real^3]`);
766 (ASM_REWRITE_TAC[VORONOI_LIST; VORONOI_SET; set_of_list]);
770 (NEW_GOAL `?s. between s (omega_list_n V ul 2,omega_list_n V ul 3) /\
771 dist (u0,s) = sqrt (&2) /\
773 (MATCH_MP_TAC MXI_EXPLICIT);
774 (EXISTS_TAC `u1:real^3` THEN EXISTS_TAC `u2:real^3` THEN EXISTS_TAC `u3:real^3`);
775 (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
776 (UP_ASM_TAC THEN ASM_REWRITE_TAC[] THEN STRIP_TAC);
777 (NEW_GOAL `omega_list_n V [u0; u1; u2; u3] 3 = s3:real^3`);
778 (EXPAND_TAC "s3" THEN ONCE_REWRITE_TAC[EQ_SYM_EQ]);
779 (REWRITE_WITH `ul = truncate_simplex 3 [u0; u1; u2; u3:real^3]`);
780 (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_3]);
781 (MATCH_MP_TAC Packing3.OMEGA_LIST_LEMMA);
782 (REWRITE_TAC[LENGTH] THEN ARITH_TAC);
783 (MP_TAC (ASSUME `between s (s2,omega_list_n V [u0; u1; u2; u3:real^3] 3)`));
784 (REWRITE_TAC[ASSUME `omega_list_n V [u0; u1; u2; u3] 3 = s3:real^3`]);
785 (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL]);
787 (NEW_GOAL `convex hull {s2,s3:real^3} SUBSET voronoi_list V [u0; u1; u2]`);
788 (REWRITE_WITH `convex hull {s2, s3} SUBSET voronoi_list V [u0; u1; u2:real^3] <=> convex hull {s2, s3} SUBSET convex hull (voronoi_list V [u0; u1; u2])`);
789 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
790 (REWRITE_WITH `convex hull (voronoi_list V [u0; u1; u2]) = voronoi_list V [u0; u1; u2:real^3]`);
791 (REWRITE_TAC[CONVEX_HULL_EQ; Packing3.CONVEX_VORONOI_LIST]);
792 (MATCH_MP_TAC Marchal_cells.CONVEX_HULL_SUBSET);
794 (NEW_GOAL `s IN voronoi_list V [u0;u1;u2:real^3]`);
797 (NEW_GOAL `~(m:real^3 IN V)`);
798 (UP_ASM_TAC THEN ASM_REWRITE_TAC[VORONOI_LIST;VORONOI_SET;set_of_list]);
800 (NEW_GOAL `s IN voronoi_closed V (u0:real^3)`);
802 (UP_ASM_TAC THEN REWRITE_TAC[voronoi_closed; IN; IN_ELIM_THM]);
804 (NEW_GOAL `dist (s, u0:real^3) <= dist (s, s)`);
805 (FIRST_ASSUM MATCH_MP_TAC);
807 (UP_ASM_TAC THEN REWRITE_TAC[DIST_REFL] THEN ONCE_REWRITE_TAC[DIST_SYM]
808 THEN ASM_REWRITE_TAC[REAL_ARITH `~(a <= b) <=> b < a`]);
809 (ASM_SIMP_TAC[SQRT_POS_LT; REAL_ARITH `&0 < &2`]);
811 (NEW_GOAL `!x:real^3. x IN convex hull S /\ ~(x IN S)
812 ==> (?y. y IN S /\ norm (x - m) < norm (y - m))`);
813 (MATCH_MP_TAC SIMPLEX_FURTHEST_LT_2);
815 (REWRITE_TAC[Geomdetail.FINITE6]);
816 (NEW_GOAL `?y:real^3. y IN S /\ norm (x - m) < norm (y - m)`);
817 (FIRST_ASSUM MATCH_MP_TAC);
821 (NEW_GOAL `x = m:real^3`);
824 (UP_ASM_TAC THEN EXPAND_TAC "S" THEN STRIP_TAC);
826 (NEW_GOAL `norm (u0 - m:real^3) = sqrt (&2)`);
827 (ASM_REWRITE_TAC[GSYM dist]);
828 (UNDISCH_TAC `s IN voronoi_list V [u0;u1;u2:real^3]`);
829 (ASM_REWRITE_TAC[VORONOI_LIST;VORONOI_SET;set_of_list]);
832 (NEW_GOAL `s IN voronoi_closed V (u0:real^3)`);
834 (NEW_GOAL `s IN voronoi_closed V (u1:real^3)`);
836 (NEW_GOAL `s IN voronoi_closed V (u2:real^3)`);
838 (NEW_GOAL `norm (u0 - m:real^3) <= norm (u1 - m)`);
839 (REWRITE_TAC[GSYM dist] THEN ONCE_REWRITE_TAC[DIST_SYM]);
841 (UNDISCH_TAC `s IN voronoi_closed V (u0:real^3)` THEN
842 REWRITE_TAC[voronoi_closed; IN; IN_ELIM_THM]);
844 (FIRST_ASSUM MATCH_MP_TAC);
847 (NEW_GOAL `norm (u1 - m:real^3) <= norm (u2 - m)`);
848 (REWRITE_TAC[GSYM dist] THEN ONCE_REWRITE_TAC[DIST_SYM]);
850 (UNDISCH_TAC `s IN voronoi_closed V (u1:real^3)` THEN
851 REWRITE_TAC[voronoi_closed; IN; IN_ELIM_THM]);
853 (FIRST_ASSUM MATCH_MP_TAC);
856 (NEW_GOAL `norm (u2 - m:real^3) <= norm (u0 - m)`);
857 (REWRITE_TAC[GSYM dist] THEN ONCE_REWRITE_TAC[DIST_SYM]);
859 (UNDISCH_TAC `s IN voronoi_closed V (u2:real^3)` THEN
860 REWRITE_TAC[voronoi_closed; IN; IN_ELIM_THM]);
862 (FIRST_ASSUM MATCH_MP_TAC);
865 (NEW_GOAL `norm (m - m:real^3) = &0`);
867 (NEW_GOAL `norm (y - m:real^3) <= sqrt (&2)`);
868 (UNDISCH_TAC `y IN {u0,u1,u2,m:real^3}` THEN
869 REWRITE_TAC[SET_RULE `(y IN {u0,u1,u2,m:real^3})
870 <=> (y = u0 \/ y = u1 \/ y = u2 \/ y = m)`]);
871 (NEW_GOAL `&0 <= sqrt (&2)`);
872 (SIMP_TAC[REAL_ARITH `&0 <= &2`; SQRT_POS_LE]);
873 (NEW_GOAL `norm (u1 - m) = sqrt (&2) /\ norm (u2 - m:real^3) = sqrt (&2)`);
874 (ASM_REAL_ARITH_TAC);
876 (REWRITE_TAC[ASSUME `y = u0:real^3`; ASSUME `norm (u0 - m:real^3) = sqrt (&2)`] THEN REAL_ARITH_TAC);
877 (REWRITE_TAC[ASSUME `y = u1:real^3`; ASSUME `norm (u1 - m) = sqrt (&2) /\ norm (u2 - m:real^3) = sqrt (&2)`] THEN REAL_ARITH_TAC);
878 (REWRITE_TAC[ASSUME `y = u2:real^3`; ASSUME `norm (u1 - m) = sqrt (&2) /\ norm (u2 - m:real^3) = sqrt (&2)`] THEN REAL_ARITH_TAC);
879 (REWRITE_TAC[ASSUME `y = m:real^3`; ASSUME `norm (m - m:real^3) = &0`;
880 ASSUME `&0 <= sqrt (&2)`] THEN REAL_ARITH_TAC);
881 (NEW_GOAL `norm (x - m:real^3) < norm (u0 -m)`);
882 (ASM_REAL_ARITH_TAC);
883 (UP_ASM_TAC THEN REWRITE_TAC[ASSUME `m = s:real^3`; GSYM dist]);
885 (UNDISCH_TAC `s:real^3 IN voronoi_closed V u0`);
886 (REWRITE_TAC[voronoi_closed; IN; IN_ELIM_THM]);
887 (ONCE_REWRITE_TAC[DIST_SYM]);
889 (NEW_GOAL `dist (u0,s:real^3) <= dist (x,s)`);
890 (FIRST_ASSUM MATCH_MP_TAC);
892 (ASM_REAL_ARITH_TAC);
895 (MATCH_MP_TAC IN_SET_IMP_IN_CONVEX_HULL_SET);
898 (UNDISCH_TAC `~( mcell k V (ul:(real^3)list) = {})`);
899 (ASM_REWRITE_TAC[ARITH_RULE `3 - 1 = 2`; TRUNCATE_SIMPLEX_EXPLICIT_2;
900 MCELL_EXPLICIT; mcell3; set_of_list]);
903 (NEW_GOAL `k = 1 \/ k = 2 \/ k = 3 \/ k = 4`);
904 (UNDISCH_TAC `1 <= k` THEN UNDISCH_TAC `k <= 4`);
907 (ASM_MESON_TAC[])]);;
909 (* ========================================================================== *)
910 (* Lemma for the case mcell 0 *)
911 (* ========================================================================= *)
913 let LEPJBDJ_0 = prove_by_refinement
916 (REWRITE_TAC[MCELL_EXPLICIT; mcell0]);
917 (REWRITE_TAC[SET_RULE `a INTER b = {} <=> (!v. v IN a INTER b ==> F)`]);
918 (GEN_TAC THEN REWRITE_TAC[IN_INTER; IN_DIFF] THEN REPEAT STRIP_TAC );
919 (NEW_GOAL `v:real^3 = HD ul`);
920 (MATCH_MP_TAC ROGERS_INTER_V_LEMMA);
921 (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]);
923 (UNDISCH_TAC `~(v:real^3 IN ball (HD ul, sqrt (&2)))`);
924 (ASM_REWRITE_TAC[ball; IN; IN_ELIM_THM; DIST_REFL]);
925 (ASM_SIMP_TAC[SQRT_POS_LT; REAL_ARITH `&0 < &2`])]);;