1 (* ========================================================================== *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
4 (* Chapter: Lemmas in Geometry *)
5 (* Author: NGUYEN QUANG TRUONG *)
7 (* ========================================================================== *)
12 Note: 2010-02-07. This file was written for the pre-2009 version of the proof of the Kepler
13 conjecture. Various things from this file are no longer needed. For now, we load it,
14 because some proofs from collect_geom.hl rely on this file.
16 Eventually this file should be pruned down to what is really needed.
18 voronoi_trg -> voronoi_
22 convex_trg -> (hull) convex
23 simplex -> geomdetail'simplex renamed.
24 deprecated: t0, voronoi2, voro2, center_pac, centered_pac, quasi_tri, quasi_reg_tet,
25 quarter, diagonal, strict_qua, strict_qua2, quartered_oct, ... (many others.)
30 Feb 18, 2013 some lemmas were deleted that were not needed, svn1626.
34 flyspeck_needs "general/sphere.hl";;
36 module Geomdetail (* : Geomdetail_type *) = struct
38 let packing = Sphere.packing;;
39 let voronoi_open = Sphere.voronoi_open;;
42 (* ================================ *)
43 (* ===== NGUYEN QUANG TRUONG ====== *)
49 Note: I have split the file into 2 pieces: geomdetail.ml and geomdetail_08.ml. Not everything in geomdetail_08.ml loads with the Multivariate directory, but these are the parts that are least likely to be used in the revision of the proof in 2009. Everything in this file now loads with Multivariate. --tch July 14, 2009
52 let near = new_definition ` near (v0:real^N) (r:real) s = { x | x IN s /\
56 let voronoi_trg = new_definition ` voronoi_trg v S = { x | !w. ((S w) /\ ~(w=v))
57 ==> (dist ( x , v ) < dist ( x , w )) }`;;
60 let conv0_2 = new_definition ` conv0_2 s = conv0 s `;;
62 let convex = new_definition `convex s <=> !x y u v. x IN s /\ y IN s /\ &0 <= u /\
63 &0 <= v /\ (u + v = &1) ==> (u % x + v % y) IN s`;;
65 let aff = new_definition `aff = ( hull ) affine`;;
67 let conv_trg = new_definition ` conv_trg s = convex hull s`;;
69 let border = new_definition ` border s = { x | ! ep. ep > &0 /\ ( ? a b. ~ (b IN s ) /\
70 dist (b, x) < ep /\ a IN s /\ dist (a, x) < ep ) }`;;
72 let packing_trg = new_definition `packing_trg (s:real^3 -> bool) = (! x y. s x /\ s y /\ ( ~(x=y))
73 ==> dist ( x, y) >= &2 ) `;;
75 let center_pac = new_definition ` center_pac s v = ( packing_trg s /\ s v )`;;
77 let centered_pac = new_definition ` centered_pac s v = ( packing s /\ v IN s )`;;
79 let dist3 = new_definition ` dist3 (x:real^3) y = dist (x,y)`;;
81 (* let voronoi2 = new_definition ` voronoi2 v S = {x| x IN voronoi_trg v S /\ dist3 x v < &2 }`;; *)
83 (* let voro2 = new_definition ` voro2 v s = {x| x IN voronoi_open s v /\ dist3 x v < &2 }`;; *)
87 let t0 = new_definition ` t0 = #1.255`;;
89 let quasi_tri = new_definition ` quasi_tri tri s = ( packing s /\
91 (? a b c. ~( a=b \/ b=c\/ c=a) /\ { a, b, c } = tri ) /\
92 (! x y. ( x IN tri /\ y IN tri /\ (~(x=y)) ) ==> ( dist3 x y <= &2 * t0 )))`;;
96 let simplex = new_definition ` geomdetail'simplex (d:real^3 -> bool) s = ( packing s /\
98 ( ? v1 v2 v3 v4. ~( v1 = v2 \/ v3 = v4 ) /\ {v1, v2 } INTER {v3, v4 } = {}/\ {v1,v2,v3,v4} = d )
102 let quarter = new_definition ` quarter (q:real^3 -> bool) s =
104 geomdetail'simplex q s /\
108 &2 * t0 <= dist3 v w /\
109 dist3 v w <= sqrt (&8) /\
111 x IN q /\ y IN q /\ ~({x, y} = {v, w})
112 ==> dist3 x y <= &2 * t0)))`;;
117 let quasi_reg_tet = new_definition ` quasi_reg_tet x s = ( geomdetail'simplex x s /\
118 (! v w. ( v IN x /\ w IN x /\
120 ==> ( dist3 v w <= &2 * t0 )) )`;;
123 let diagonal = new_definition ` diagonal d1 d2 q s = ( quarter q s /\
125 (!x y. x IN q /\ y IN q ==> dist3 x y <= dist3 d1 d2))`;;
128 let strict_qua = new_definition ` strict_qua d s = ( quarter d s /\
129 ( ? x y. x IN d /\ y IN d /\ &2 * t0 < dist3 x y /\ dist3 x y < sqrt( &8 ) ))`;;
131 let strict_qua2 = new_definition ` strict_qua2 d (ch:real^3 -> bool ) s = ( quarter d s /\ ch SUBSET d
132 /\ ( ? x y. ~( x = y ) /\ ch = {x,y} /\ &2 * t0 < dist3 x y /\ dist3 x y < sqrt ( &8 ) ) )`;;
137 let quartered_oct = new_definition `quartered_oct (v:real^3) (w:real^3) (v1:real^3) (v2:real^3) (v3:real^3) (v4:real^3) s =
139 ( &2 * t0 < dist (v,w) /\ dist (v,w) < sqrt (&8) ) /\
140 (!x. x IN {v1, v2, v3, v4}
141 ==> dist (x,v) <= &2 * t0 /\ dist (x,w) <= &2 * t0) /\
142 {v, w, v1, v2, v3, v4} SUBSET s /\
143 (&2 <= dist (v1,v2) /\ dist (v1,v2) <= &2 * t0) /\
144 (&2 <= dist (v2,v3) /\ dist (v2,v3) <= &2 * t0) /\
145 (&2 <= dist (v3,v4) /\ dist (v3,v4) <= &2 * t0) /\
146 &2 <= dist (v4,v1) /\
147 dist (v4,v1) <= &2 * t0 ) `;;
149 let adjacent_pai = new_definition ` adjacent_pai v v1 v3 v2 v4 s = ( strict_qua2 { v , v1 , v3 , v2 } { v1 , v3 } s
150 /\ strict_qua2 { v , v1 , v3 , v4 } { v1 , v3 } s /\
151 ( conv0 { v , v1 , v3 , v2 } INTER conv0 { v , v1 , v3 , v4 } = {} ) )`;;
154 let conflicting_dia = new_definition ` conflicting_dia v v1 v3 v2 v4 s = ( adjacent_pai v v1 v3 v2 v4 s
155 /\ adjacent_pai v v2 v4 v1 v3 s )`;;
158 let interior_pos = new_definition `interior_pos v v1 v3 v2 v4 s = ( conflicting_dia v v1 v3 v2 v4 s
159 /\ ~( conv0 { v1, v3 } INTER conv0 { v , v2 , v4 } = {} ))`;;
161 let isolated_qua = new_definition ` isolated_qua q s = ( quarter q s /\ ~( ? v v1 v2 v3 v4. q =
162 {v, v1, v2, v3} /\ adjacent_pai v v1 v2 v3 v4 s))`;;
164 let isolated_pai = new_definition ` isolated_pai q1 q2 s = ( isolated_qua q1 s /\ isolated_qua q2 s /\
165 ~ (conv0 q1 INTER conv0 q2 = {}))`;;
167 let anchor = new_definition ` anchor (v:real^3) v1 v2 s = ( {v, v1, v2} SUBSET s /\ dist3 v1 v2 <= sqrt ( &8 ) /\
168 dist3 v1 v2 >= &2 * t0 /\ dist3 v v1 <= &2 * t0 /\ dist3 v v2 <= &2 * t0 )`;;
171 let anchor_points = new_definition ` anchor_points v w s = { t | &2 * t0 <= dist3 v w /\
175 let Q_SYS = new_definition ` Q_SYS s = {q | quasi_reg_tet q s \/
180 dist3 c d > &2 * t0 /\
181 (quasi_reg_tet qq s \/ strict_qua qq s) /\
182 conv0 {c, d} INTER conv0 qq = {}) \/
186 v IN q /\ w IN q /\ &2 * t0 < dist3 v w /\ anchor t v w s} >
190 v IN q /\ w IN q /\ &2 * t0 < dist3 v w /\ anchor t v w s} =
192 ~(?v1 v2 v3 v4 v w. v IN q /\
194 {v1, v2, v3, v4} SUBSET anchor_points v w s
197 &2 * t0 < dist3 v w /\
198 quartered_oct v w v1 v2 v3 v4 s))
199 \/ (? v w v1 v2 v3 v4. q = { v, w, v1, v2} /\ quartered_oct v w v1 v2 v3 v4 s )
200 \/ (? v v1 v3 v2 v4. ( q = {v, v1, v2, v3} \/ q = {v, v1, v3, v4} ) /\
201 interior_pos v v1 v3 v2 v4 s /\ anchor_points v1 v3 s = { v, v2, v4} /\
202 anchor_points v2 v4 s = { v, v1, v3 } )}`;;
205 (* deprecated - thales *)
206 let conv = new_definition `conv S:real^A->bool = affsign sgn_ge {} S`;;
210 let barrier = new_definition ` barrier s = { { (v1 : real^3 ) , ( v2 :real^3 ) , (v3 :real^3) } |
211 quasi_tri { v1 , v2 , v3 } s \/
212 (? v4. ( { v1 , v2 , v3 } UNION { v4 }) IN Q_SYS s ) } `;;
214 let obstructed = new_definition ` obstructed x y s = ( ? bar. bar IN barrier s /\
215 ( ~ (conv0_2 { x , y } INTER conv_trg bar = {})))`;;
217 let obstruct = new_definition ` obstruct x y s = ( ? bar. bar IN barrier s /\
218 ( ~ (conv0 { x , y } INTER conv bar = {})))`;;
220 let unobstructed = new_definition ` unobstructed x y s = ( ~( obstructed x y s ))`;;
222 let VC_trg = new_definition ` VC_trg x s = { z | dist3 x z < &2 /\ ~obstructed x z s /\
223 (! y. y IN s /\ ~ ( x = y ) /\ ~(obstructed z y s) ==> dist3 x z < dist3 y z )} `;;
225 let VC_INFI_trg = new_definition ` VC_INFI_trg s = { z | ( ! x. x IN s /\
226 ~( z IN VC_trg x s ))}`;;
228 let VC = new_definition `VC v s = { x | v IN lambda_x x s /\
229 (!w. w IN lambda_x x s /\ ~(w = v) ==> dist3 x v < dist3 x w) }`;;
231 let VC_INFI = new_definition ` VC_INFI s = { z | ( ! x. ~( z IN VC x s ))}`;;
237 [NOT_IN_EMPTY; IN_UNIV; IN_UNION; IN_INTER; IN_DIFF; IN_INSERT;
238 IN_DELETE; IN_REST; IN_INTERS; IN_UNIONS; IN_IMAGE] in
239 let allthms = basicthms @ map (REWRITE_RULE[IN]) basicthms @
242 TRY(POP_ASSUM_LIST(MP_TAC o end_itlist CONJ)) THEN
243 REPEAT COND_CASES_TAC THEN
244 REWRITE_TAC[EXTENSION; SUBSET; PSUBSET; DISJOINT; SING] THEN
245 REWRITE_TAC allthms in
248 (if ths = [] then ALL_TAC else MP_TAC(end_itlist CONJ ths)) THEN
251 let SET_RULE tm = prove(tm,SET_TAC[]);;
253 (* some TRUONG TACTICS *)
255 let PHA = REWRITE_TAC[ MESON[] ` (a/\b)/\c <=> a/\ b /\ c `];;
257 let NGOAC = REWRITE_TAC[ MESON[] ` a/\b/\c <=> (a/\b)/\c `];;
259 let DAO = NGOAC THEN REWRITE_TAC[ MESON[]` a /\ b <=> b /\ a`];;
261 let PHAT = REWRITE_TAC[ MESON[] ` (a\/b)\/c <=> a\/b\/c `];;
263 let NGOACT = REWRITE_TAC[ GSYM (MESON[] ` (a\/b)\/c <=> a\/b\/c `)];;
265 let KHANANG = PHA THEN REWRITE_TAC[ MESON[]` ( a\/ b ) /\ c <=> a /\ c \/ b /\ c `] THEN
266 REWRITE_TAC[ MESON[]` a /\ ( b \/ c ) <=> a /\ b \/ a /\ c `];;
268 let ATTACH thm = MATCH_MP (MESON[]` ! a b. ( a ==> b ) ==> ( a <=> a /\ b )`) thm;;
270 let CUTHE1 th = MATCH_MP (MESON[]` ( ! a. P a ) ==> P a `) th ;;
272 let CUTHE2 th = MATCH_MP (MESON[]` ( ! a b. P a b ) ==> P a b`) th ;;
274 let CUTHE3 th = MATCH_MP (MESON[]` ( ! a b c. P a b c ) ==> P a b c`) th ;;
276 let CUTHE4 th = MATCH_MP (MESON[]` ( ! a b c d. P a b c d ) ==> P a b c d`) th ;;
278 let CUTHE5 th = MATCH_MP (MESON[]` ( ! a b c d e. P a b c d e) ==> P a b c d e`) th ;;
280 let CUTHE6 th = MATCH_MP (MESON[]` ( ! a b c d e f. P a b c d e f) ==> P a b c d e f`) th ;;
282 let CUTHE7 th = MATCH_MP (MESON[]` ( ! a b c d e f h. P a b c d e f h) ==> P a b c d e f h`) th ;;
284 let NHANH tm = ONCE_REWRITE_TAC[ ATTACH (tm)];;
287 let trg_sub_bo = prove ( `A SUBSET B <=> (!x. A x ==> B x)`, SET_TAC[] );;
289 let trg_sub_se = prove ( `A SUBSET B <=> (!x. x IN A ==> x IN B )`, SET_TAC[] );;
291 let trg_setbool = prove (`x IN A <=> A x `, SET_TAC[] );;
293 let trg_boolset = prove (` A x <=> x IN A `, SET_TAC[] );;
295 let trg_in_union = prove (` x IN ( A UNION B ) <=> x IN A \/ x IN B `, SET_TAC[]);;
297 let not_in_set3 = prove ( `~ ( x IN { z | A z /\ B z /\ C z } ) <=> ~ A x \/ ~ B x \/ ~ C x `,
300 let trg_dist3_sym = prove ( `! x y. dist3 x y = dist3 y x `, SIMP_TAC[dist3; DIST_SYM]);;
302 let affine_hull_e = prove (`affine hull {} = {}`,
303 REWRITE_TAC[AFFINE_EMPTY; AFFINE_HULL_EQ]);;
305 let wlog = MESON[]` (! a b. ( P a b = P b a ) /\ ( Q a b \/ Q b a ) ) ==> ((? a b . P a b ) <=> ( ? a b. P a b
308 let wlog_real = MESON[REAL_ARITH `( ! a b:real. a <= b \/ b <= a )`] `
309 (! a:real b:real . P a b = P b a ) ==> ((? a:real b . P a b ) <=> ( ? a b. P a b
312 let dkdx = MESON[REAL_ARITH ` ! a b:real. a <= b \/ b <= a `]`! P. (!a b u v m n p . P a b u v m n p <=> P b a v u m n p)
313 ==> ((?a b u v m n p. P a b u v m n p) <=> (?a b u v m n p. P a b u v m n p /\ a <= b))`;;
316 let AFFINE_HULL_SINGLE = prove(`!x. affine hull {x} = {x}`,
317 SIMP_TAC[AFFINE_SING; AFFINE_HULL_EQ]);;
319 let usefull = MESON[] ` (!x. a x ==> b x ) ==>(?x. a x ) ==> c ==> d <=>
320 (!x. a x ==> b x) ==> (?x. a x /\ b x ) ==> c ==> d `;;
322 let v1_in_convex3 = prove (` ! v1 v2 v3. v1 IN {t | ?a b c.
323 &0 <= a /\ &0 <= b /\ &0 <= c /\ a + b + c = &1 /\
324 t = a % v1 + b % v2 + c % v3}`, REPEAT GEN_TAC THEN REWRITE_TAC[ IN_ELIM_THM] THEN
325 EXISTS_TAC ` &1 ` THEN EXISTS_TAC ` &0 ` THEN EXISTS_TAC ` &0 ` THEN
326 REWRITE_TAC[ VECTOR_ARITH ` &1 % v1 + &0 % v2 + &0 % v3 = v1 `] THEN REAL_ARITH_TAC);;
329 let v3_in_convex3 = prove( `! v1 v2 v3. v3 IN
335 t = a % v1 + b % v2 + c % v3}`, REWRITE_TAC[IN_ELIM_THM] THEN REPEAT GEN_TAC
336 THEN REPLICATE_TAC 2 (EXISTS_TAC `&0`) THEN EXISTS_TAC ` &1` THEN REWRITE_TAC[VECTOR_MUL_LZERO;
337 VECTOR_ADD_LID; VECTOR_MUL_LID] THEN REAL_ARITH_TAC);;
340 let v1v2v3_in_convex3 = prove (` ! v1 v2 v3 . v1 IN {t | ?a b c. &0 <= a /\ &0 <= b /\ &0 <= c /\
341 a + b + c = &1 /\ t = a % v1 + b % v2 + c % v3}
342 /\ v2 IN {t | ?a b c. &0 <= a /\ &0 <= b /\ &0 <= c /\ a + b + c = &1 /\ t = a % v1 + b % v2 + c % v3}
343 /\ v3 IN {t | ?a b c. &0 <= a /\ &0 <= b /\ &0 <= c /\ a + b + c = &1 /\ t = a % v1 + b % v2 + c % v3}`,
344 REWRITE_TAC[v1_in_convex3; v3_in_convex3] THEN REPEAT GEN_TAC THEN REWRITE_TAC[IN_ELIM_THM] THEN
345 EXISTS_TAC ` &0` THEN EXISTS_TAC ` &1` THEN EXISTS_TAC ` &0` THEN
346 REWRITE_TAC[VECTOR_ARITH` v2 = &0 % v1 + &1 % v2 + &0 % v3`] THEN REAL_ARITH_TAC);;
349 let convex3 = prove( `!v1 v2 v3.
356 t = a % v1 + b % v2 + c % v3}`,
357 REWRITE_TAC[convex; IN_ELIM_THM] THEN
358 REPEAT GEN_TAC THEN STRIP_TAC THEN
359 EXISTS_TAC ` u * a + v * a'` THEN
360 EXISTS_TAC ` u * b + v * b'` THEN
361 EXISTS_TAC ` u * c + v * c'` THEN
362 REPEAT (FIRST_X_ASSUM MP_TAC) THEN
363 REWRITE_TAC[MESON[] ` a==> b==> c <=> a /\ b==> c`] THEN PHA THEN
364 REWRITE_TAC[ MESON[]` &0 <= a /\ l <=> l /\ &0 <= a `] THEN PHA THEN
365 NHANH (MESON[REAL_LE_MUL; REAL_ARITH ` &0 <= a /\ &0 <= b ==> &0 <= a +b `]` &0 <= v /\
372 &0 <= a ==> &0 <= u * c + v * c' /\
373 &0 <= u * b + v * b' /\
374 &0 <= u * a + v * a'`) THEN
375 REWRITE_TAC[REAL_ARITH` ( a + y ) + ( b + x ) + c + z = ( a + b + c) + (
377 REWRITE_TAC[REAL_ARITH ` a * b + a * c = a * ( b + c) `] THEN
379 REWRITE_TAC[ REAL_ARITH ` a * &1 = a `] THEN SIMP_TAC[] THEN
380 REWRITE_TAC[VECTOR_ARITH` u % (a % v1 + b % v2 + c % v3) + v % (a' % v1 + b' % v2 + c' % v3) =
381 (u * a + v * a') % v1 + (u * b + v * b') % v2 + (u * c + v * c') % v3`]);;
383 let INTERS_SUBSET = SET_RULE `! P t0. P t0 ==> INTERS { t| P t } SUBSET t0`;;
385 let SET3_SUBSET = SET_RULE`! a b c. {a,b,c} SUBSET s <=> a IN s /\ b IN s /\ c IN s `;;
387 let SUM_TWO_RATIO = REAL_FIELD ` ~(a + b = &0) <=> a / ( a + b) + b /(a+b) = &1`;;
389 let minconvex3 = prove(`!t v1 v2 v3.
390 convex t /\ {v1, v2, v3} SUBSET t
392 &0 <= a /\ &0 <= b /\ &0 <= c /\ a + b + c = &1
393 ==> a % v1 + b % v2 + c % v3 IN t)`,
395 REWRITE_TAC[convex; SET3_SUBSET] THEN
398 ONCE_REWRITE_TAC[ MESON[]` &0 <= a /\ &0 <= b /\ l<=> ( a + b = &0 \/
399 ~( a + b = &0)) /\ &0 <= a /\ &0 <= b /\ l`] THEN
400 REWRITE_TAC[RIGHT_OR_DISTRIB] THEN
401 REWRITE_TAC[ MESON[]` a \/ b ==> c <=> ( a ==> c ) /\ ( b ==> c )`] THEN
402 REWRITE_TAC[REAL_ARITH` a + b = &0 /\ &0 <= a /\ &0 <= b /\ &0 <= c /\ a + b + c = &1
403 <=> &0 = a /\ &0 = b /\ &1 = c `] THEN
404 ONCE_REWRITE_TAC[ EQ_SYM_EQ] THEN
406 ASM_REWRITE_TAC[ VECTOR_MUL_LZERO; VECTOR_MUL_LID; VECTOR_ADD_LID] THEN
407 REWRITE_TAC[MESON[]`&0 = a + b <=> a + b = &0`; SUM_TWO_RATIO] THEN
408 NHANH (MESON[REAL_ARITH ` &0 <= a /\ &0 <= b ==> &0 <= a + b `]`
409 dau /\ &0 <= a /\ &0 <= b /\ l ==> &0 <= a + b `) THEN
410 NHANH (MESON[REAL_LE_DIV]` (aa /\ &0 <= a /\ &0 <= b /\ bb) /\ &0 <= a + b
411 ==> &0 <= a / (a + b) /\ &0 <= b / (a + b)`) THEN
412 REWRITE_TAC[GSYM SUM_TWO_RATIO] THEN
414 NHANH (MESON[REAL_DIV_LMUL]` ~(a + b = &0) ==> a = (a+b) *(a/(a+b)) /\ b =
415 (a+b) *(b/(a+b))`) THEN
416 REWRITE_TAC[MESON[VECTOR_MUL_RCANCEL]` ( dau /\ a = (a + b) * a / (a + b) /\ b = (a + b) * b / (a + b))
417 /\ l ==> a % v1 + b % v2 + c % v3 IN t <=>
418 ( dau /\ a = (a + b) * a / (a + b) /\ b = (a + b) * b / (a + b))
419 /\ l ==> ((a + b) * a / (a + b)) % v1 + ((a + b) * b / (a + b)) % v2 + c % v3 IN t`] THEN
420 REWRITE_TAC[ VECTOR_ARITH ` ((a + b) * a / (a + b)) % v1 + ((a + b) * b / (a + b)) % v2 + c % v3
421 = (a + b) % ( (a / (a + b)) % v1 + (b / (a + b)) % v2) + c % v3 `] THEN
422 REWRITE_TAC[SUM_TWO_RATIO] THEN
423 ASM_MESON_TAC[ REAL_ARITH` a + b + c = (a + b ) + c`]);;
426 let EQ_EXPAND = MESON[] `(a <=> b) <=> ( a ==> b ) /\ ( b ==> a )` ;;
430 let OTHER_CONVEX_CONDI = prove(` ! s. convex s <=> (! a b c v1 v2 v3. {v1, v2, v3} SUBSET s /\
431 &0 <= a /\ &0 <= b /\ &0 <= c /\ a + b + c = &1
432 ==> a % v1 + b % v2 + c % v3 IN s)`,
433 REWRITE_TAC[EQ_EXPAND; MESON[minconvex3]`!s. (convex s
434 ==> (!a b c v1 v2 v3.
435 {v1, v2, v3} SUBSET s /\
440 ==> a % v1 + b % v2 + c % v3 IN s))`; convex] THEN STRIP_TAC THEN
441 REWRITE_TAC[SET3_SUBSET] THEN DISCH_TAC THEN
442 REWRITE_TAC[REAL_ARITH`&0 <= u /\ &0 <= v /\ u + v = &1 <=>
443 &0 <= u /\ &0 <= v / &2 /\ u + v/ &2 + v / &2 = &1`] THEN
444 ONCE_REWRITE_TAC[MESON[REAL_ARITH` a = a / &2 + a / &2`]` u % x + v % y =
445 u % x + ( v/ &2 + v/ &2 ) % y `] THEN REWRITE_TAC[ VECTOR_ADD_RDISTRIB] THEN
452 let convex3_in_inters = prove (` ! v1 v2 v3. {t | ?a b c.
457 t = a % v1 + b % v2 + c % v3} SUBSET
458 INTERS {t | convex t /\ {v1, v2, v3} SUBSET t} `,
460 MATCH_MP_TAC (SET_RULE ` ( ! x. x IN A ==> x IN B ) ==> A SUBSET B`) THEN
461 REWRITE_TAC[IN_ELIM_THM] THEN REWRITE_TAC[IN_INTERS] THEN
462 REWRITE_TAC[MESON[] `( !x. (?a b c.
467 x = a % v1 + b % v2 + c % v3)
468 ==> (!t. convex t /\ {v1, v2, v3} SUBSET t ==> x IN t))
474 x = a % v1 + b % v2 + c % v3)
475 ==> (!t. convex t /\ {v1, v2, v3} SUBSET t /\ (?a b c.
480 x = a % v1 + b % v2 + c % v3) ==> x IN t)) `] THEN
481 GEN_TAC THEN DISCH_TAC THEN GEN_TAC THEN FIRST_X_ASSUM MP_TAC THEN
482 REWRITE_TAC[ IN_ELIM_THM ; TAUT ` a ==> b ==> c <=> a /\ b ==> c `] THEN
483 MESON_TAC[minconvex3]);;
490 let simpl_conv3 =prove(` ! v1 v2 v3. conv_trg {v1 , v2 ,v3} = {t | ?a b c. &0 <= a /\ &0 <= b /\ &0 <= c /\ a + b + c = &1
491 /\ t = a % v1 + b % v2 + c % v3}`, REPEAT GEN_TAC THEN
492 REWRITE_TAC[conv; hull] THEN REPEAT GEN_TAC THEN
493 REWRITE_TAC[ SET_RULE` a = b <=> a SUBSET b /\ b SUBSET a `] THEN
494 REWRITE_TAC[conv_trg; hull] THEN
495 MATCH_MP_TAC (MATCH_MP ( MESON[] `(! a b. P a b) ==> P a b` ) (MESON[INTERS_SUBSET ]`
496 ! P t0 . ( P t0 /\ aa ) ==> INTERS {t | P t} SUBSET t0 /\ aa`)) THEN
497 REWRITE_TAC[convex3] THEN REWRITE_TAC[ SET_RULE `{v1 , v2, v3} SUBSET a <=>
498 v1 IN a /\ v2 IN a /\ v3 IN a`] THEN REWRITE_TAC [ v1v2v3_in_convex3] THEN
499 REWRITE_TAC[ SET_RULE` v1 IN t /\ v2 IN t /\ v3 IN t <=> {v1, v2, v3} SUBSET t`] THEN
500 REWRITE_TAC[convex3_in_inters]);;
503 (* =========== begining lemma 8.2 ========== *)
507 let near2t0 = new_definition ` near2t0 v0 s = { x | x IN s /\ dist(v0,x) < &2 * t0 }`;;
509 let e_plane = new_definition ` e_plane (a:real^N) (b:real^N) x = ( ~( a=b) /\ dist(a,x) = dist(b,x))`;;
512 let min_dist = new_definition ` min_dist (x:real^3) s = ((?u. u IN s /\
513 (!w. w IN s /\ ~(u = w) ==> dist (u,x) < dist (w,x))) \/
518 dist (u,x) = dist (v,x) /\
519 (!w. w IN s ==> dist (u,x) <= dist (w,x)))) `;;
521 (* ========== simplize.ml ============ *)
523 let SET3_SUBSET = SET_RULE`! a b c. {a,b,c} SUBSET s <=> a IN s /\ b IN s /\ c IN s `;;
525 let FINITE6 = MESON[ FINITE_RULES ] `! a b c d e f.
530 FINITE {a, b, c, d} /\
531 FINITE {a, b, c, d, e} /\
532 FINITE {a, b, c, d, e, f} `;;
534 (* ========= new simplizing ========== *)
536 let elimin = REWRITE_RULE[IN];;
538 let CONV_EM = prove(`conv {} = {}:real^A->bool`,
539 REWRITE_TAC[conv;sgn_ge;affsign;UNION_EMPTY;FUN_EQ_THM;elimin
540 NOT_IN_EMPTY;lin_combo;SUM_CLAUSES]
541 THEN REAL_ARITH_TAC);;
543 let CONV_SING = prove(`!u. conv {u:real^A} = {u}`,
544 REWRITE_TAC[conv;sgn_ge;affsign;FUN_EQ_THM;UNION_EMPTY;lin_combo;SUM_SING;VSUM_SING;
545 elimin IN_SING] THEN REPEAT GEN_TAC THEN
546 REWRITE_TAC[TAUT `(p <=> q) = ((p ==> q) /\ (q ==> p))`] THEN
547 REPEAT STRIP_TAC THENL [ASM_MESON_TAC[VECTOR_MUL_LID];
548 ASM_REWRITE_TAC[]] THEN EXISTS_TAC `\ (v:real^A). &1` THEN
549 MESON_TAC[VECTOR_MUL_LID;REAL_ARITH `&0 <= &1`] );;
552 let NOV9 = prove(`!x y z.(x = y /\ y = z
559 w = a % y + b % y + c % z})`,
560 SIMP_TAC[] THEN REWRITE_TAC[SET_RULE` {a,a} = {a}`] THEN
561 REWRITE_TAC[ CONV_SING; GSYM VECTOR_ADD_RDISTRIB] THEN
562 REWRITE_TAC[ MESON[]` a + b + c = &1 /\ w = (a + b + c) % z <=>a + b + c = &1 /\
563 w = &1 % z `; VECTOR_MUL_LID] THEN REWRITE_TAC[ FUN_EQ_THM] THEN
564 REWRITE_TAC[ SET_RULE ` {a} x <=> a = x `; IN_ELIM_THM] THEN
565 REPEAT GEN_TAC THEN DISCH_TAC THEN GEN_TAC THEN
566 NGOAC THEN REWRITE_TAC[ LEFT_EXISTS_AND_THM] THEN
567 MATCH_MP_TAC (MESON[] ` a ==> ( z = x <=> a /\ x = z )`) THEN
568 REPLICATE_TAC 2 (EXISTS_TAC `&0`) THEN EXISTS_TAC ` &1` THEN REAL_ARITH_TAC);;
570 let IN_ACT_SING = SET_RULE `! a x. ({a} x <=> a = x ) /\ ( x IN {a} <=> x = a) /\ {a} a`;;
572 let NOV10 = prove(` ! x y. (x = y
574 (?a b. &0 <= a /\ &0 <= b /\ a + b = &1 /\ x = a % y + b % y))) `,
575 REWRITE_TAC[GSYM VECTOR_ADD_RDISTRIB] THEN
576 REWRITE_TAC[ MESON[VECTOR_MUL_LID]` a + b = &1 /\ x = (a + b) % y <=> a + b = &1 /\
577 x = y`]THEN REPEAT GEN_TAC THEN DISCH_TAC THEN GEN_TAC THEN NGOAC THEN
578 REWRITE_TAC[LEFT_EXISTS_AND_THM] THEN MATCH_MP_TAC (MESON[]` a ==> ( x = y <=> a /\
579 y = x )`)THEN EXISTS_TAC `&0` THEN EXISTS_TAC ` &1` THEN REAL_ARITH_TAC);;
581 let IN_SET2 = SET_RULE `!a b x.
582 (x IN {a, b} <=> x = a \/ x = b) /\ ({a, b} x <=> x = a \/ x = b)`;;
585 let VSUM_DIS2 = prove(` ! x y f. ~(x=y) ==> vsum {x,y} f = f x + f y`, REWRITE_TAC[
587 <=> ~(x IN {y})`] THEN MESON_TAC[ FINITE_RULES; VSUM_CLAUSES; VSUM_SING]);;
589 let SUM_DIS2 = prove(`! x y f. ~(x=y) ==> sum {x,y} f = f x + f y `,REWRITE_TAC[
591 <=> ~(x IN {y})`] THEN MESON_TAC[ FINITE_RULES; SUM_CLAUSES; SUM_SING]);;
594 let TRUONG_LEMMA = prove
596 (?f. x' = f x % x + f y % y /\ (&0 <= f x /\ &0 <= f y) /\
598 (?a b. &0 <= a /\ &0 <= b /\ a + b = &1 /\ x' = a % x + b % y)` ,
599 REPEAT GEN_TAC THEN EQ_TAC
600 THENL [MESON_TAC[]; STRIP_TAC] THEN
601 ASM_CASES_TAC `y:real^N = x` THENL
602 [EXISTS_TAC `\x:real^N. &1 / &2`;
603 EXISTS_TAC `\u:real^N. if u = x then (a:real) else b`] THEN
604 ASM_REWRITE_TAC[GSYM VECTOR_ADD_RDISTRIB] THEN
605 CONV_TAC REAL_RAT_REDUCE_CONV);;
608 let NOV11 = prove(`! z. {z} =
614 w = a % z + b % z + c % z}`,
615 REWRITE_TAC[ FUN_EQ_THM; IN_ACT_SING; IN_ELIM_THM] THEN
616 REWRITE_TAC[GSYM VECTOR_ADD_RDISTRIB] THEN
617 REWRITE_TAC[ MESON[VECTOR_MUL_LID]`a + b + c = &1 /\
618 x = (a + b + c) % z <=> a + b + c = &1 /\ x = z`] THEN
619 NGOAC THEN MATCH_MP_TAC (MESON[]` (? a b c. P a b c) ==> (! z x. z = x <=>
620 (? a b c. P a b c /\ x = z))`) THEN
621 REPLICATE_TAC 2 (EXISTS_TAC `&0`) THEN
622 EXISTS_TAC `&1` THEN REAL_ARITH_TAC);;
626 let CONV2_CONV3 = prove(` !x' y z.
627 (?a b. &0 <= a /\ &0 <= b /\ a + b = &1 /\ x' = a % y + b % z)
633 x' = a % y + b % y + c % z)`,
634 REPEAT GEN_TAC THEN REWRITE_TAC[ VECTOR_ARITH` a % y + b % y + c % z = (a+b) %y + c%z`] THEN STRIP_TAC THEN
635 REPLICATE_TAC 2 (EXISTS_TAC `a/ &2`) THEN
636 EXISTS_TAC `b:real` THEN
637 REWRITE_TAC[ REAL_ARITH` a / &2 + a / &2 = a /\ a / &2 + a / &2 + b = a + b `] THEN
639 ASM_REAL_ARITH_TAC);;
642 let CONV3_CONV2 = prove(`! x' y z. (?a b c.
647 x' = a % y + b % y + c % z)
648 ==> (?a b. &0 <= a /\ &0 <= b /\ a + b = &1 /\ x' = a % y + b % z)`,
649 REPEAT GEN_TAC THEN STRIP_TAC THEN EXISTS_TAC ` a + b:real` THEN
650 EXISTS_TAC `c:real` THEN
651 REWRITE_TAC[VECTOR_ADD_RDISTRIB] THEN
652 REWRITE_TAC[VECTOR_ARITH` (a % y + b % y) + c % z = a % y + b % y + c % z `] THEN
653 ASM_SIMP_TAC[REAL_ARITH ` a + b + c = (a + b) + c`] THEN
654 ASM_REAL_ARITH_TAC);;
656 let CONV_SET2 = prove(` ! x y:real^A. conv {x,y} = {w | ? a b. &0 <= a /\ &0 <= b /\ a + b = &1 /\
658 ONCE_REWRITE_TAC[ MESON[] ` (! a b. P a b ) <=> ( ! a b. a = b \/ ~( a= b)
660 REWRITE_TAC[ MESON[]` a \/ b ==> c <=> ( a==> c) /\ ( b==> c)`] THEN
662 REWRITE_TAC[ SET_RULE ` {a,a} = {a}`; CONV_SING; FUN_EQ_THM; IN_ELIM_THM] THEN
663 REWRITE_TAC[ IN_ACT_SING] THEN
664 REWRITE_TAC[NOV10] THEN
665 REWRITE_TAC[conv; sgn_ge; affsign; lin_combo] THEN
666 REWRITE_TAC[UNION_EMPTY; IN_SET2] THEN
667 ONCE_REWRITE_TAC[ MESON[]` ~(x = y) ==> (!x'. (?f. P f x') <=> l x') <=>
668 ~(x = y) ==> (!x'. (?f. ~(x=y) /\ P f x') <=> l x')`] THEN
669 REWRITE_TAC[ MESON[VSUM_DIS2; SUM_DIS2]` ~(x = y) /\
670 x' = vsum {x, y} ff /\ l /\ sum {x, y} f = &1 <=> ~(x = y) /\
671 x' = ff x + ff y /\ l /\ f x + f y = &1 `] THEN
672 REWRITE_TAC[ MESON[]` (!w. w = x \/ w = y ==> &0 <= f w) <=> &0 <= f x /\ &0 <= f y`] THEN
673 ONCE_REWRITE_TAC[ GSYM (MESON[]` ~(x = y) ==> (!x'. (?f. P f x') <=> l x') <=>
674 ~(x = y) ==> (!x'. (?f. ~(x=y) /\ P f x') <=> l x')`)] THEN
675 REPEAT GEN_TAC THEN DISCH_TAC THEN GEN_TAC THEN
676 REWRITE_TAC[ TRUONG_LEMMA]);;
678 let CONV3_A_EQ = prove(`! x y z. (x = y \/ y = z \/ z = x
685 w = a % x + b % y + c % z})`,
686 MATCH_MP_TAC (MESON[] `(! a b c. P a b c <=> P b a c) /\ (! a b c. a = b \/ b = c ==> P a b c)
687 ==> (! a b c. a = b \/ b = c \/ c = a ==> P a b c )`) THEN
688 SIMP_TAC[ MESON[ SET_RULE ` {a,b,c} = {b,a,c} `]`conv {x, y, z} = conv {y,x,z}`] THEN
689 SIMP_TAC[ MESON[ REAL_ARITH` a + b + c = b + a + c`; VECTOR_ARITH` a % x + b % y + c % z
690 = b % y + a % x + c % z `]` (?a b c.
695 w = a % x + b % y + c % z)
701 w = a % y + b % x + c % z)`] THEN
702 MATCH_MP_TAC (MESON[]` (! a b c. P a b c <=> P c b a ) /\ (! a b c. a = b ==> P a b c)
703 ==> (! a b c. a = b \/ b = c ==> P a b c)`) THEN
704 SIMP_TAC[ MESON[SET_RULE `{a,b,c} ={c,b,a} `]` conv {a,b,c} = conv {c,b,a}`] THEN
705 SIMP_TAC[ MESON[REAL_ARITH` a + b + c = c + b + a`; VECTOR_ARITH` a % x + b % y + c % z
706 = c % z + b % y + a % x `]`(?a b c.
711 w = a % x + b % y + c % z) <=>
717 w = a % z + b % y + c % x)`] THEN
718 REWRITE_TAC[ SET_RULE`{a,a,b} = {a,b}`] THEN
719 ONCE_REWRITE_TAC[ MESON[]` x = y ==> conv {y,z} = s <=> x = y /\( y = z \/
720 ~(y=z))==> conv {y,z} = s `] THEN
721 KHANANG THEN REWRITE_TAC[ MESON[]` a \/ b ==> c <=> (a==> c) /\ (b==> c)`] THEN
722 SIMP_TAC[] THEN REWRITE_TAC[SET_RULE`{a,a} ={a}`; CONV_SING] THEN
723 SIMP_TAC[NOV11] THEN REWRITE_TAC [ GSYM NOV11] THEN
724 REWRITE_TAC[CONV_SET2] THEN
725 REPEAT GEN_TAC THEN STRIP_TAC THEN
726 REWRITE_TAC[ FUN_EQ_THM; IN_ELIM_THM] THEN
727 GEN_TAC THEN REWRITE_TAC[MESON[]` (a <=> b ) <=> ( a ==> b) /\ (b==> a)`] THEN
728 REWRITE_TAC[CONV2_CONV3; CONV3_CONV2]);;
731 let VSUM_DIS3 = prove( `! x y z f. ~(x=y\/y=z\/z=x) ==> vsum {x,y,z} f = f x + f y + f z `,
732 NHANH (SET_RULE` ~(x = y \/ y = z \/ z = x) ==> ({x} INTER {y,z} = {}) `) THEN
733 REWRITE_TAC[ GSYM DISJOINT; SET_RULE `{x, y, z} = {x} UNION {y,z}` ] THEN
734 REWRITE_TAC[MESON[FINITE6; VSUM_UNION]` aa /\ DISJOINT {x} {y, z}
735 ==> vsum ({x} UNION {y, z}) f = ab <=> aa /\ DISJOINT {x} {y, z} ==>
736 vsum {x} f + vsum {y,z} f = ab `] THEN
737 MESON_TAC[VSUM_SING; VSUM_DIS2]);;
740 let SUM_DIS3 = prove(` ! x y z f. ~(x = y \/ y = z \/ z = x) ==> sum {x, y, z} f =
742 NHANH (SET_RULE` ~(x = y \/ y = z \/ z = x) ==> ({x} INTER {y,z} = {}) `) THEN
743 REWRITE_TAC[ GSYM DISJOINT; SET_RULE `{x, y, z} = {x} UNION {y,z}` ] THEN
744 REWRITE_TAC[MESON[FINITE6; SUM_UNION]` aa /\ DISJOINT {x} {y, z}
745 ==> sum ({x} UNION {y, z}) f = ab <=> aa /\ DISJOINT {x} {y, z} ==>
746 sum {x} f + sum {y,z} f = ab `] THEN MESON_TAC[ SUM_SING; SUM_DIS2]);;
748 let EQ_EXPAND = MESON[] `(a <=> b) <=> ( a ==> b ) /\ ( b ==> a )` ;;
750 let CONV_SET3 = prove(`! x y z:real^A. conv {x,y,z} = { w | ? a b c. &0 <= a /\ &0 <= b /\ &0 <= c /\
751 a + b + c = &1 /\ w = a % x + b % y + c % z } `,
753 ONCE_REWRITE_TAC[ MESON[]` conv {x,y,z} = s <=> (x = y \/ y= z \/ z = x ) \/
754 ~(x = y \/ y= z \/ z = x ) ==> conv {x,y,z} = s`] THEN
755 ONCE_REWRITE_TAC[ MESON[]` a \/ b ==> c <=> ( a ==> c ) /\(b==>c)`] THEN
756 REWRITE_TAC[CONV3_A_EQ] THEN
757 REWRITE_TAC[conv; FUN_EQ_THM; affsign; IN_ELIM_THM; sgn_ge; lin_combo; UNION_EMPTY] THEN
758 DISCH_TAC THEN GEN_TAC THEN FIRST_X_ASSUM MP_TAC THEN
759 ONCE_REWRITE_TAC[ MESON[]` a ==> ((?f. P f ) <=> la ) <=>
760 a ==> ((?f. a /\ P f ) <=> la ) `] THEN REWRITE_TAC[MESON[VSUM_DIS3]` ~(x = y \/
761 y = z \/ z = x) /\ x' = vsum {x, y, z} f /\ l <=> ~(x = y \/ y = z \/ z = x) /\
762 x' = f x + f y + f z /\ l `] THEN
763 REWRITE_TAC[ MESON[SUM_DIS3]` ~(x = y \/ y = z \/ z = x) /\ P /\ Q /\ sum {x,y,z} f = &1
764 <=> ~(x = y \/ y = z \/ z = x) /\ P /\ Q /\ ( f x + f y + f z ) = &1`] THEN
765 REWRITE_TAC[SET_RULE ` (!w. {x, y, z} w ==> &0 <= f w) <=> &0 <= f x /\
766 &0 <= f y /\ &0 <= f z `] THEN
767 ONCE_REWRITE_TAC[ GSYM (MESON[]` a ==> ((?f. P f ) <=> la ) <=>
768 a ==> ((?f. a /\ P f ) <=> la ) `)] THEN DISCH_TAC THEN
769 REWRITE_TAC[ EQ_EXPAND] THEN
770 REWRITE_TAC[ MESON[]` (?f. x' = f x % x + f y % y + f z % z /\
771 (&0 <= f x /\ &0 <= f y /\ &0 <= f z) /\
772 f x + f y + f z = &1)
778 x' = a % x + b % y + c % z)`] THEN STRIP_TAC THEN
779 EXISTS_TAC ` (\d. if d = (x:real^A) then (a:real) else ( if d = (y:real^A) then
780 (b:real) else c ))` THEN REPEAT (FIRST_X_ASSUM MP_TAC) THEN
781 REWRITE_TAC[ MESON[]`~( a \/ b ) <=> ~a /\ ~b `] THEN SIMP_TAC[]);;
784 let CONV3_EQ = prove(` ! x y z. conv_trg {x,y,z} = conv {x,y,z} `, REWRITE_TAC[simpl_conv3;
788 (* ==== CARD ASSERTION ==== *)
791 let CARD_CLAUSES_IMP = prove(` !a s.
793 ==> CARD (a INSERT s) <= SUC (CARD s) /\
794 (a IN s ==> CARD (a INSERT s) = CARD s) /\
795 (~(a IN s) ==> CARD (a INSERT s) = SUC (CARD s))`,
796 ONCE_REWRITE_TAC[ MESON[] ` ( a ==> b /\ c ) <=> ( a ==> b ) /\ ( a ==> c )`] THEN
797 REWRITE_TAC[ MESON[CARD_CLAUSES] ` FINITE s ==> ( a IN s ==> CARD (a INSERT s) = CARD s ) /\
798 (~(a IN s) ==> CARD (a INSERT s) = SUC (CARD s))`] THEN
799 MESON_TAC[ CARD_CLAUSES; ARITH_RULE ` a <= SUC a /\ a <= a `]);;
801 (* =================== *)
803 let CARD_SING = prove( `! a: A. CARD {a} = 1`, REWRITE_TAC[ MESON[ FINITE6; CARD_EQ_NSUM ]
804 ` CARD {a} = nsum {a} (\x. 1)`] THEN REWRITE_TAC[ NSUM_SING ]);;
806 let CARD_SET2 = prove( ` ! a b . ( CARD {a, b} = 2 <=> ~(a = b)) /\ (CARD {a, b} = 1 <=> a = b ) `,
807 REWRITE_TAC[ MESON[ FINITE6; CARD_CLAUSES ] ` CARD {a,b} = (if a IN {b} then CARD {b} else SUC (CARD {b}))`]
808 THEN REWRITE_TAC[ MESON[ FINITE6; CARD_CLAUSES ] ` CARD {a} = (if a IN {} then CARD {} else SUC (CARD {}))`]
809 THEN REWRITE_TAC[ NOT_IN_EMPTY; IN_SING; CARD_CLAUSES; ADD1] THEN
810 MESON_TAC[ ARITH_RULE ` ~( 0+ 1 = 2 ) /\ (0 + 1) + 1 = 2 /\ ~((0 + 1) + 1 = 1 ) /\ 0 + 1 = 1 `]);;
814 let CARD_EQUATION = prove(`!(s: A -> bool) t.
816 ==> CARD (s UNION t) + CARD (s INTER t) = CARD s + CARD t `,
817 NHANH (MESON[FINITE_INTER; FINITE_UNION] `FINITE s /\ FINITE t ==> FINITE ( s UNION t ) /\
818 FINITE ( s INTER t ) `) THEN MESON_TAC[ CARD_EQ_NSUM; NSUM_INCL_EXCL]);;
821 let CARD_DISJOINT = prove(` ! s: A -> bool t. FINITE s /\ FINITE t ==>
822 ( CARD s + CARD t = CARD ( s UNION t ) <=> s INTER t ={} )`,
823 MESON_TAC[CARD_EQUATION; ARITH_RULE ` a + b = a <=> b = 0 `; FINITE_INTER; CARD_EQ_0]);;
826 let CARD2 = prove(` ! a b . CARD {a,b} <= 2 /\ ( CARD {a,b} = 2 <=> ~(a = b ) )`,
827 REWRITE_TAC[ MESON[ CARD_SET2] ` CARD {a, b} = 2 <=> ~(a = b)`] THEN MP_TAC CARD_SET2 THEN
828 ONCE_REWRITE_TAC[ MESON[] ` CARD {a, b} <= 2 <=>
829 ( a = b \/ ~( a = b)) /\ CARD {a, b} <= 2`] THEN KHANANG THEN
830 REWRITE_TAC[ MESON[CARD_SET2] `a = b /\ CARD {a, b} <= 2 \/ ~(a = b) /\ CARD {a, b} <= 2
831 <=> a = b /\ 1 <= 2 \/ ~(a = b) /\ 2 <= 2`] THEN
832 MESON_TAC[ARITH_RULE ` 1 <= 2 /\ 2 <= 2 `]);;
835 let CARD3 = prove(`! a b c . CARD {a,b,c} <= 3 /\
836 ( CARD {a,b,c} = 3 <=> ~( a =b \/ b= c\/ c= a ))`,
837 REWRITE_TAC[ SET_RULE ` {a,b,c} = {a} UNION {b,c}`] THEN
838 REWRITE_TAC[ ARITH_RULE ` CARD ({a} UNION {b, c}) <= 3 <=>
839 CARD ({a} UNION {b, c}) + CARD ({a} INTER {b, c}) <= 3 + CARD ({a} INTER {b, c})`] THEN
840 REWRITE_TAC[ ARITH_RULE ` CARD ({a} UNION {b, c}) = 3 <=>
841 CARD ({a} UNION {b, c}) + CARD ({a} INTER {b, c}) = 3 + CARD ({a} INTER {b, c})`] THEN
842 REWRITE_TAC[ MESON[ FINITE_RULES; CARD_EQUATION] ` CARD ({a} UNION {b, c}) + CARD ({a} INTER {b, c})
843 = CARD {a} + CARD {b,c} `] THEN REWRITE_TAC[ CARD_SING] THEN
844 REWRITE_TAC[ ARITH_RULE `! a b. (1 + a <= 3 + b <=> a <= 2 + b ) /\
845 (1 + a = 3 + b <=> a = 2 + b )`] THEN
846 REWRITE_TAC[ MESON[CARD2; ARITH_RULE ` a <= b ==> a <= b + c: num`] ` CARD {b, c} <= 2 + CARD ({a} INTER {b, c})`] THEN
847 ONCE_REWRITE_TAC[ MESON[CARD2]` CARD {b, c} = P b c <=> CARD {b, c} <= 2 /\ CARD {b, c} = P b c`] THEN
848 REWRITE_TAC[ ARITH_RULE ` a <= 2 /\ a = 2 + b <=> a = 2 /\ b = 0`] THEN
849 REWRITE_TAC[ MESON[FINITE_RULES; CARD2; FINITE_INTER; CARD_EQ_0] ` CARD {b, c} = 2 /\ CARD ({a} INTER {b, c}) = 0
850 <=> ~(b=c) /\ {a} INTER {b, c} = {}`] THEN SET_TAC[]);;
855 let CARD4 = prove(`!a b c d.
856 CARD {a, b, c, d} <= 4 /\
857 (CARD {a, b, c, d} = 4 <=>
858 ~(a IN {b, c, d}) /\ ~(b = c \/ c = d \/ d = b))`,
859 NHANH (MESON[FINITE6; CARD_CLAUSES_IMP]` CARD {a, b, c, d} <= 4 ==> CARD {a, b, c, d}
860 <= SUC (CARD {b,c,d})`) THEN
861 NHANH ( MESON[CARD3] ` aa <= SUC (CARD {b, c, d}) ==> CARD {b,c,d} <= 3 `) THEN
862 REWRITE_TAC[ ARITH_RULE ` CARD {a, b, c, d} <= 4 /\
863 CARD {a, b, c, d} <= SUC (CARD {b, c, d}) /\
864 CARD {b, c, d} <= 3 <=>
865 CARD {a, b, c, d} <= SUC (CARD {b, c, d}) /\ CARD {b, c, d} <= 3`] THEN
866 SIMP_TAC[MESON[FINITE_RULES; CARD_CLAUSES_IMP] ` CARD {a, b, c, d} <= SUC
867 (CARD {b, c, d})`; CARD3; CARD_CLAUSES_IMP] THEN
868 REWRITE_TAC[ ARITH_RULE ` CARD {a, b, c, d} = 4 <=> CARD {a, b, c, d} + CARD ( {a}
869 INTER {b,c,d} ) = 4 + CARD ({a} INTER {b,c,d})`] THEN
870 REWRITE_TAC[ SET_RULE ` {a,b,c,d} = {a} UNION {b,c,d} ` ] THEN
871 REWRITE_TAC[ MESON[FINITE_RULES; CARD_EQUATION; CARD_SING] ` CARD ({a} UNION {b, c, d}) + CARD ({a} INTER {b, c, d})
872 = 1 + CARD {b,c,d} `] THEN
873 NHANH (MESON[CARD3] ` 1 + CARD {b, c, d} = aa ==> CARD {b,c,d} <= 3 `) THEN
874 REWRITE_TAC[ ARITH_RULE `1 + CARD {b, c, d} = 4 + CARD ({a} INTER {b, c, d}) /\
875 CARD {b, c, d} <= 3 <=>
876 CARD {b, c, d} = 3 /\ CARD ({a} INTER {b, c, d}) = 0`] THEN
877 REWRITE_TAC[ CARD3] THEN
878 MESON_TAC[ FINITE_RULES; FINITE_INTER; CARD_EQ_0; SET_RULE `
879 {a} INTER {b, c, d} = {} <=> ~(a IN {b, c, d})` ]);;
882 let CARD5 = prove(` ! a b c d e. CARD {a,b,c,d,e} <= 5 /\
883 ( CARD {a,b,c,d,e} = 5 <=> ~( a IN {b,c,d,e}) /\
884 ~(b IN {c, d, e}) /\ ~(c = d \/ d = e \/ e = c))`,
885 ONCE_REWRITE_TAC[ MESON[ FINITE_RULES; CARD_CLAUSES_IMP] ` CARD {a, b, c, d, e} <= 5 <=>
886 CARD {a, b, c, d, e} <= SUC ( CARD {b,c,d,e} ) ==> CARD {a, b, c, d, e} <= 5`] THEN
887 ONCE_REWRITE_TAC[ MESON[CARD4] ` aa ==> CARD {a, b, c, d, e} <= 5 <=>
888 aa /\ CARD {b,c,d,e} <= 4 ==> CARD {a, b, c, d, e} <= 5`] THEN
889 REWRITE_TAC[ ARITH_RULE ` a <= SUC b /\ b <= 4 ==> a <= 5 `] THEN
890 REWRITE_TAC[ ARITH_RULE ` CARD {a, b, c, d, e} = 5 <=>
891 CARD {a, b, c, d, e} + CARD ({a} INTER {b,c,d,e} ) = 5 + CARD ({a} INTER {b,c,d,e} )`] THEN
892 REWRITE_TAC[ SET_RULE ` {a,b,c,d,e} = {a} UNION {b,c,d,e} `] THEN
893 REWRITE_TAC[ MESON[FINITE_RULES; CARD_EQUATION; CARD_SING ]` CARD ({a} UNION {b, c, d, e}) +
894 CARD ({a} INTER {b, c, d, e}) = 1 + CARD {b,c,d,e} `] THEN
895 ONCE_REWRITE_TAC[ MESON[ CARD4] ` 1 + CARD {b, c, d, e} = aa <=> CARD {b,c,d,e} <= 4 /\
896 1 + CARD {b, c, d, e} = aa `] THEN
897 REWRITE_TAC[ ARITH_RULE ` a <= 4 /\ 1 + a = 5 + b <=> a = 4 /\ b = 0`] THEN
898 REWRITE_TAC[ CARD4; MESON[FINITE_RULES; FINITE_INTER; CARD_EQ_0] `
899 CARD ({a} INTER {b, c, d, e}) = 0 <=> {a} INTER {b, c, d, e} ={} `] THEN SET_TAC[]);;
902 let set_3elements = prove(`(?a b c. ~(a = b \/ b = c \/ c = a) /\ {a, b, c} = {v1, v2, v3}) <=>
903 ~(v1 = v2 \/ v2 = v3 \/ v3 = v1)`, REWRITE_TAC[GSYM CARD3] THEN
908 let db_t0 = prove(`&2 * t0 = &2 * #1.255 /\ &2 * t0 = #2.51 /\ &2 * #1.255 = #2.51`,
909 REWRITE_TAC[t0] THEN REAL_ARITH_TAC);;
912 let without_lost = MESON[] ` ! P x. (!a b. P a b <=> P b a) /\ (?a b. P a b /\ x = a)
913 ==> (?a b. P a b /\ (x = a \/ x = b))`;;
915 let condi_of_wlofg = MESON[]` (!a b. P a b <=> P b a)
916 ==> ((?a b. P a b /\ (x = a \/ x = b)) <=> (?a b. P a b /\ x = a))`;;
919 let CARD_SET_OF_LIST_LE = prove
920 (`!l. CARD(set_of_list l) <= LENGTH l`,
922 SIMP_TAC[LENGTH; set_of_list; CARD_CLAUSES; FINITE_SET_OF_LIST] THEN
925 let HAS_SIZE_SET_OF_LIST = prove
926 (`!l. (set_of_list l) HAS_SIZE (LENGTH l) <=> PAIRWISE (\x y. ~(x = y)) l`,
927 REWRITE_TAC[HAS_SIZE; FINITE_SET_OF_LIST] THEN LIST_INDUCT_TAC THEN
928 ASM_SIMP_TAC[CARD_CLAUSES; LENGTH; set_of_list; PAIRWISE; ALL;
929 FINITE_SET_OF_LIST; GSYM ALL_MEM; IN_SET_OF_LIST] THEN
930 COND_CASES_TAC THEN ASM_REWRITE_TAC[SUC_INJ] THEN
931 ASM_MESON_TAC[CARD_SET_OF_LIST_LE; ARITH_RULE `~(SUC n <= n)`]);;
933 (* ====================In your theorem we want the n=4 case, so we instantiate it:
934 =========================== *)
936 let HAS_SIZE_SET_OF_LIST_4 = prove
937 (`!a b c d:A. {a,b,c,d} HAS_SIZE 4 <=> PAIRWISE (\x y. ~(x = y)) [a;b;c;d]`,
938 REPEAT GEN_TAC THEN MP_TAC(ISPEC `[a;b;c;d]:A list`HAS_SIZE_SET_OF_LIST) THEN
939 REWRITE_TAC[LENGTH; set_of_list; ARITH]) ;;
941 (* ============================================================================
942 Then finally, using this and a bit of straightforward rearrangement,
943 we can collapse the desired theorem to a lemma that MESON can prove
945 ===============================================================================*)
948 (`! a b c d. ( ? v1 v2 v3 v4:A. ~( v1 = v2 \/ v3 = v4 ) /\
949 {v1, v2 } INTER {v3, v4 } = {} /\
950 { a , b , c , d } = { v1 , v2, v3 ,v4}) <=>
951 ~ ( a = b \/ a = c \/ a = d \/ b = c \/ b = d \/ c = d )`,
953 REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY; INTER_EMPTY; SET_RULE
954 `(a INSERT s) INTER t = {} <=> ~(a IN t) /\ s INTER t = {}`] THEN
956 `(?v1 v2 v3 v4:A. {a,b,c,d} = {v1,v2,v3,v4} /\ {v1,v2,v3,v4} HAS_SIZE 4) <=>
957 {a,b,c,d} HAS_SIZE 4`) THEN
958 REWRITE_TAC[HAS_SIZE_SET_OF_LIST_4; PAIRWISE; ALL; DE_MORGAN_THM; CONJ_ACI]);;
961 let def_simplex = prove(`! s a b c d. geomdetail'simplex {a, b, c, d} s <=>
963 {a, b, c, d} SUBSET s /\
964 ~ ( a = b \/ a = c \/ a = d \/ b = c \/ b = d \/ c = d ) `, REWRITE_TAC[ simplex]
965 THEN REPEAT GEN_TAC THEN MATCH_MP_TAC (MESON[] ` ( x <=> y ) ==> ( a /\ b /\ x <=>
966 a /\ b /\ y ) `) THEN ONCE_REWRITE_TAC[MESON[]` {v1, v2, v3, v4} = {a, b, c, d} <=>
967 {a, b, c, d} = {v1, v2, v3, v4} ` ] THEN REWRITE_TAC[ SET_OF_4]);;
972 let PAIR_D3 = prove(` ! i j u w. {u,w} = {i,j} ==> dist3 i j = dist3 u w `,
973 REWRITE_TAC[ SET_RULE ` {u, w} = {i, j} <=> u= i /\ w = j \/ u = j /\ w = i `] THEN
974 MESON_TAC[ trg_dist3_sym]);;
976 let PAIR_DIST = prove(` ! i j u w. {u,w} = {i,j} ==> dist(i,j) = dist(u,w) `,
977 REWRITE_TAC[ SET_RULE ` {u, w} = {i, j} <=> u= i /\ w = j \/ u = j /\ w = i `] THEN
978 MESON_TAC[ DIST_SYM]);;
980 (* ================== *)
982 let DOT_SUB_ADD = VECTOR_ARITH `! a b. b dot b - a dot a = (b - a) dot (b + a)` ;;
984 let DIST_LT_HALF_PLANE = prove(`!x:real^A a:real^A b:real^A.
985 dist(x,a) < dist(x,b) <=> &0 < (a - b) dot (&2 % x - (a + b))`,
986 ABBREV_TAC ` an a b x = ((a:real^A) - b) dot (&2 % x - (a + b))` THEN
987 REWRITE_TAC[dist; vector_norm] THEN
988 REWRITE_TAC[MESON[DOT_POS_LE; SQRT_MONO_LT_EQ]` sqrt ( x dot x) < sqrt (y dot y) <=>
989 x dot x < y dot y `] THEN
990 REWRITE_TAC[DOT_LSUB; DOT_RSUB] THEN
991 SIMP_TAC[DOT_SYM] THEN
992 ONCE_REWRITE_TAC[ GSYM REAL_SUB_LT] THEN
993 REWRITE_TAC[ REAL_ARITH ` x dot x -
995 (b dot x - b dot b) -
996 (x dot x - a dot x - (a dot x - a dot a)) =
997 &2 * (a dot x - b dot x) + b dot b - a dot a`] THEN
998 REWRITE_TAC[GSYM DOT_LSUB; GSYM DOT_RMUL] THEN
999 REWRITE_TAC[DOT_SUB_ADD; VECTOR_ARITH `(b - a) dot (b + a) =
1000 ( -- ( a - b) ) dot ( a + b) `] THEN
1001 REWRITE_TAC[VECTOR_ARITH ` (a - b) dot &2 % x + --(a - b) dot (a + b) =
1002 (a-b) dot ( &2 % x - (a+b))`] THEN
1003 ASM_REWRITE_TAC[REAL_ARITH ` a - &0 = a` ]);;
1005 let OR_IMP_EX = MESON[]` ! a b c. a \/ b ==> c <=> (a ==> c) /\ ( b ==> c)` ;;
1007 let HALF_PLANE_CONV = prove(`! a b:real^N. convex { x| x | dist(x,a) < dist (x,b) }`,
1008 REWRITE_TAC[DIST_LT_HALF_PLANE; convex; IN_ELIM_THM] THEN
1009 REWRITE_TAC[VECTOR_ARITH ` &2 % (u % x + v % y) - (a + b)
1010 = u % ( &2 % x ) + v % ( &2 % y ) - &1 % (a + b )`] THEN
1011 ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN SIMP_TAC[] THEN
1012 REWRITE_TAC[VECTOR_ARITH ` (a - b) dot (u % &2 % x +
1013 v % &2 % y - (u + v) % (a + b)) = u * (a - b) dot (&2 % x - (a + b))
1014 + v * (a - b) dot (&2 % y - (a + b))`] THEN
1015 REWRITE_TAC[REAL_ARITH` &0 <= u /\ &0 <= v /\ &1 = u + v <=>
1016 &0 = u /\ &1 = v \/ &0 < u /\ &0 <= v /\ &1 = u + v`] THEN
1018 REWRITE_TAC[OR_IMP_EX] THEN
1019 ONCE_REWRITE_TAC[ EQ_SYM_EQ] THEN SIMP_TAC[] THEN
1020 REWRITE_TAC[REAL_POLY_CLAUSES] THEN
1021 SIMP_TAC[ REAL_ARITH ` a + &0 = a `] THEN
1022 NHANH (MESON[REAL_LT_MUL]` &0 < (a - b) dot (&2 % x - (a + b)) /\
1023 &0 < (a - b) dot (&2 % y - (a + b)) /\
1024 &0 < u /\ l ==> &0 < u * ((a - b) dot (&2 % x - (a + b)))`) THEN
1025 NHANH (MESON[REAL_ARITH` &0 < a ==> &0 <= a `; REAL_LE_MUL]`
1026 &0 < (a - b) dot (&2 % y - (a + b)) /\
1028 &0 <= v /\ l ==> &0 <= v * ((a - b) dot (&2 % y - (a + b)))`)
1029 THEN REAL_ARITH_TAC);;
1031 let HALF_PLANE_CONV_EP = REWRITE_RULE[convex; IN_ELIM_THM] HALF_PLANE_CONV;;
1033 let VORONOI_CONV = prove( ` ! (s:real^A -> bool) v. convex (voronoi_open s v)`,
1034 REWRITE_TAC[voronoi_open] THEN REPEAT GEN_TAC THEN
1035 REWRITE_TAC[convex; IN_ELIM_THM] THEN MESON_TAC[HALF_PLANE_CONV_EP]);;
1037 let CONVEX_IM_CONV2_SU = prove(`! s u v. convex s /\ u IN s /\ v IN s ==> conv {u,v} SUBSET s `,
1038 REWRITE_TAC[convex; CONV_SET2] THEN SET_TAC[]);;
1040 (* have not added *)
1042 let U_IN_CONV2 = prove(`! u v. u IN conv {u,v} `,
1043 REWRITE_TAC[ CONV_SET2; IN_ELIM_THM] THEN REPEAT GEN_TAC
1044 THEN EXISTS_TAC `&1` THEN EXISTS_TAC `&0 ` THEN
1045 REWRITE_TAC[VECTOR_MUL_LID; VECTOR_MUL_LZERO; VECTOR_ADD_RID] THEN
1048 let UV_IN_CONV2 = prove(` ! u v. u IN conv {u,v} /\ v IN conv {u,v} `,
1049 MESON_TAC[U_IN_CONV2; SET_RULE ` {u,v} = {v,u} `]);;
1051 let CONVEX_AS_CONV2 = prove(` ! s. convex s ==> ( ! u v. u IN s /\ v IN s <=>
1052 conv {u,v} SUBSET s )`, REWRITE_TAC[ EQ_EXPAND] THEN
1053 SIMP_TAC[CONVEX_IM_CONV2_SU ] THEN MESON_TAC[SUBSET; UV_IN_CONV2]);;
1055 let CONV0_SING = prove(`! x:real^A . conv0 {x} = {x} `,
1056 REWRITE_TAC[conv0; FUN_EQ_THM; affsign; lin_combo] THEN
1057 REWRITE_TAC[UNION_EMPTY; VSUM_SING; SUM_SING; IN_ACT_SING; sgn_gt] THEN
1058 REWRITE_TAC[MESON[REAL_ARITH` &0 < &1 `]` (!w. x = w ==> &0 < f w) /\
1059 f x = &1 <=> f x = &1 `] THEN
1060 REWRITE_TAC[MESON[VECTOR_MUL_LID]` (?f. x' = f x % x /\ f x = &1) <=>
1061 x' = x /\ (? f. f x = &1 ) `] THEN
1062 MESON_TAC[prove(`!x:real^A. ? f. f x = &1`, GEN_TAC THEN EXISTS_TAC
1063 `(\x:real^A. &1)` THEN MESON_TAC[])]);;
1065 let NOV10' = prove(`! x y. (x = y
1067 (?a b. &0 < a /\ &0 < b /\ a + b = &1 /\ x = a % y + b % y)))`,
1068 REWRITE_TAC[GSYM VECTOR_ADD_RDISTRIB] THEN
1069 REWRITE_TAC[MESON[VECTOR_MUL_LID]` a + b = &1 /\
1070 x = (a + b) % y <=> a + b = &1 /\ x = y `] THEN
1071 MESON_TAC[prove(` ?a b. &0 < a /\ &0 < b /\ a + b = &1`, REPEAT
1072 (EXISTS_TAC ` &1 / &2 `) THEN REAL_ARITH_TAC)]);;
1074 let CONV0_SET2 = prove(` ! x y:real^A. conv0 {x,y} = {w | ? a b. &0 < a /\ &0 < b /\ a + b = &1 /\
1076 ONCE_REWRITE_TAC[ MESON[] ` (! a b. P a b ) <=> ( ! a b. a = b \/ ~( a= b)
1078 REWRITE_TAC[ MESON[]` a \/ b ==> c <=> ( a==> c) /\ ( b==> c)`] THEN
1080 REWRITE_TAC[ SET_RULE ` {a,a} = {a}`; CONV0_SING; FUN_EQ_THM; IN_ELIM_THM] THEN
1081 REWRITE_TAC[ IN_ACT_SING; NOV10'] THEN
1082 REWRITE_TAC[conv0 ; sgn_gt; affsign; lin_combo] THEN
1083 REWRITE_TAC[UNION_EMPTY; IN_SET2] THEN
1084 ONCE_REWRITE_TAC[ MESON[]` ~(x = y) ==> (!x'. (?f. P f x') <=> l x') <=>
1085 ~(x = y) ==> (!x'. (?f. ~(x=y) /\ P f x') <=> l x')`] THEN
1086 REWRITE_TAC[ MESON[VSUM_DIS2; SUM_DIS2]` ~(x = y) /\
1087 x' = vsum {x, y} ff /\ l /\ sum {x, y} f = &1 <=> ~(x = y) /\
1088 x' = ff x + ff y /\ l /\ f x + f y = &1 `] THEN
1089 REWRITE_TAC[ MESON[]` (!w. w = x \/ w = y ==> &0 < f w) <=> &0 < f x /\ &0 < f y`] THEN
1090 ONCE_REWRITE_TAC[ GSYM (MESON[]` ~(x = y) ==> (!x'. (?f. P f x') <=> l x') <=>
1091 ~(x = y) ==> (!x'. (?f. ~(x=y) /\ P f x') <=> l x')`)] THEN
1092 REPEAT GEN_TAC THEN DISCH_TAC THEN GEN_TAC THEN
1093 REWRITE_TAC[ EQ_EXPAND] THEN
1094 SIMP_TAC[ MESON[]` ((?f. x' = f x % x + f y % y /\ (&0 < f x /\ &0 < f y) /\ f x + f y = &1)
1095 ==> (?a b. &0 < a /\ &0 < b /\ a + b = &1 /\ x' = a % x + b % y)) `] THEN
1096 STRIP_TAC THEN EXISTS_TAC ` (\(d:real^A). if d = x then (a:real) else b )` THEN
1099 let CONV02_SU_CONV2 = prove(` ! u v. conv0 {u,v} SUBSET conv {u,v} `,
1100 REWRITE_TAC[ CONV_SET2; CONV0_SET2] THEN
1101 MP_TAC (REAL_ARITH ` ! a . &0 < a ==> &0 <= a `) THEN SET_TAC[]);;
1104 let CONVEX_IM_CONV02_SU = prove(`! s u v. convex s /\ u IN s /\ v IN s ==>
1105 conv0 {u, v} SUBSET s`,
1106 MESON_TAC[CONV02_SU_CONV2; CONVEX_IM_CONV2_SU; SUBSET_TRANS]);;
1108 let PAIR_EQ_EXPAND =
1109 SET_RULE `{a,b} = {c,d} <=> a = c /\ b = d \/ a = d /\ b = c`;;
1111 let IN_SET3 = SET_RULE ` x IN {a,b,c} <=> x = a \/ x = b \/ x = c `;;
1113 let IN_SET4 = SET_RULE ` x IN {a,b,c,d} <=> x = a \/ x = b \/ x = c \/ x = d `;;
1115 let FOUR_IN = SET_RULE `!a b c d. a IN {a,b,c,d} /\ b IN {a,b,c,d} /\c IN {a,b,c,d} /\ d IN {a,b,c,d} ` ;;
1119 let D3_REFL = prove(` !x. dist3 x x = &0 ` , MESON_TAC[dist3; DIST_REFL]);;
1121 let db_t0_sq8 = MATCH_MP REAL_LT_RSQRT (REAL_ARITH ` #2.51 pow 2 < &8 `);;
1123 let SUB_PACKING = prove(`!sub s.
1124 packing s /\ sub SUBSET s
1125 ==> (!x y. x IN sub /\ y IN sub /\ ~(x = y) ==> &2 <= dist3 x y)`,
1126 REWRITE_TAC[ packing; GSYM dist3] THEN SET_TAC[]);;
1128 let DIST_PAIR_LEMMA = prove
1129 (`{a,b} = {c,d} ==> dist(a,b) = dist(c,d)`,
1130 REWRITE_TAC[PAIR_EQ_EXPAND] THEN MESON_TAC[DIST_SYM]);;