1 (* ========================================================================== *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
6 (* Author: Nguyen Quang Truong *)
8 (* ========================================================================== *)
11 (* second half of collect_geom.ml.
12 It was split in half by thales Feb 2010.
14 This file was edited by thales on 2012-5-15
15 to make it possible to load everything up through lemma GDRQXLG
16 giving the formula for the circumradius of a simplex.
18 Everything dependent on unproved axioms was commented out.
20 Feb 2013, some excess material removed.
23 flyspeck_needs "leg/cayleyR_def.hl";;
24 flyspeck_needs "leg/collect_geom.hl";;
26 module Collect_geom2 (* : Collect_geom2_type *) = struct
34 let cayleyR = Cayleyr.cayleyR;;
36 let LET_TR = Collect_geom.LET_TR;;
37 let DIST_POW2_DOT = Collect_geom.DIST_POW2_DOT;;
38 let UPS_X_POS = Collect_geom.UPS_X_POS;;
39 let DELTA_POS_4POINTS = Collect_geom.DELTA_POS_4POINTS;;
40 let REAL_LDISTRIB = REAL_ADD_LDISTRIB;;
41 let POW_2 = REAL_POW_2;;
42 let REAL_POSSQ = REAL_LT_SQUARE;;
43 let REAL_RDISTRIB = REAL_ARITH
44 `!x y z. (x + y) * z = (x * z) + (y * z)`;; (* Tactics_jordan *)
46 let BY = Hales_tactic.BY;;
48 (* deprecated def from sphere.hl *)
49 let mk_vec3 = new_definition
50 `mk_vec3 a b c = vector[a; b; c]`;;
51 let real3_of_triple = new_definition
52 `real3_of_triple (a,b,c) = (mk_vec3 a b c):real^3`;;
53 let triple_of_real3 = new_definition
54 `triple_of_real3 (v:real^3) =
56 (* deprecated def from sphere.hl *)
59 (* this lemma is proved as below, but it take quite a long time to run it *)
61 let CAYLEYR_5POINTS = prove(` !x1 x2 x3 x4 (x5 :real^3).
62 let x12 = dist (x1,x2) pow 2 in
63 let x13 = dist (x1,x3) pow 2 in
64 let x14 = dist (x1,x4) pow 2 in
65 let x15 = dist (x1,x5) pow 2 in
66 let x23 = dist (x2,x3) pow 2 in
67 let x24 = dist (x2,x4) pow 2 in
68 let x25 = dist (x2,x5) pow 2 in
69 let x34 = dist (x3,x4) pow 2 in
70 let x35 = dist (x3,x5) pow 2 in
71 let x45 = dist (x4,x5) pow 2 in
72 cayleyR x12 x13 x14 x15 x23 x24 x25 x34 x35 x45 = &0 `,
73 LET_TR THEN REWRITE_TAC[ DIST_POW2_DOT] THEN REPEAT GEN_TAC THEN
74 REWRITE_TAC[ MESON[VECTOR_ARITH` (a:real^n) - b = a - x - ( b - x ) `]`
75 AA ( (x1 - x5 ) dot ( x1 - x5)) ((x2 - x3) dot (x2 - x3))
76 ((x2 - x4) dot (x2 - x4))
77 ((x2 - x5) dot (x2 - x5))
78 ((x3 - x4) dot (x3 - x4))
79 ((x3 - x5) dot (x3 - x5))
80 ((x4 - x5) dot (x4 - x5)) =
81 AA ( (x1 - x5 ) dot ( x1 - x5)) ((x2 - x1 - ( x3 - x1 )) dot (x2 - x1 - ( x3 - x1 )))
82 ((x2 - x1 - ( x4 - x1 )) dot (x2 - x1 - ( x4 - x1 )))
83 ((x2 - x1 - ( x5 - x1 )) dot (x2 - x1 - ( x5 - x1 )))
84 ((x3 - x1 - ( x4 - x1 )) dot (x3 - x1 - ( x4 - x1 )))
85 ((x3 - x1 - ( x5 - x1 )) dot (x3 - x1 - ( x5 - x1 )))
86 ((x4 - x1 - ( x5 - x1 )) dot (x4 - x1 - ( x5 - x1 ))) ` ] THEN
87 SIMP_TAC[VECTOR_ARITH ` ((x4: real^N) - x1 - (x5 - x1)) = x1 - x5 - ( x1 - x4 ) `] THEN
88 ABBREV_TAC ` x12 = (x1 - ( x2:real^3)) ` THEN
89 ABBREV_TAC ` x13 = (x1 - ( x3:real^3)) ` THEN
90 ABBREV_TAC ` x14 = (x1 - ( x4:real^3)) ` THEN
91 ABBREV_TAC ` x15 = (x1 - ( x5:real^3)) ` THEN
92 REWRITE_TAC[DOT_3] THEN REWRITE_TAC[lemma_cm3; cayleyR] THEN REAL_ARITH_TAC);;
97 let LEMMA3 = prove(` !x1 x2 x3 x4 (x5 :real^3).
98 let x12 = dist (x1,x2) pow 2 in
99 let x13 = dist (x1,x3) pow 2 in
100 let x14 = dist (x1,x4) pow 2 in
101 let x15 = dist (x1,x5) pow 2 in
102 let x23 = dist (x2,x3) pow 2 in
103 let x24 = dist (x2,x4) pow 2 in
104 let x25 = dist (x2,x5) pow 2 in
105 let x34 = dist (x3,x4) pow 2 in
106 let x35 = dist (x3,x5) pow 2 in
107 let x45 = dist (x4,x5) pow 2 in
108 &0 <= ups_x x12 x13 x23 /\
109 &0 <= delta x12 x13 x14 x23 x24 x34 /\
110 cayleyR x12 x13 x14 x15 x23 x24 x25 x34 x35 x45 = &0 `, MP_TAC
111 CAYLEYR_5POINTS THEN LET_TR THEN
112 SIMP_TAC[ dist; UPS_X_POS; DELTA_POS_4POINTS]);;
116 let NUHSVLM = LEMMA3;;
119 (* OLD END OF MODULE *)
122 let LEMMA52 = prove( `! v1 v2 v3 v4 (v5:real^3).
123 muy_v v1 v2 v3 v4 v5 ( (dist3 v4 v5) pow 2 ) = &0 `,
124 REWRITE_TAC[muy_v; dist3] THEN MP_TAC LEMMA3 THEN
125 LET_TR THEN SIMP_TAC[]);;
127 let PFDFWWV = LEMMA52;;
130 REAL_ARITH `!x x1 x2. (x - x1) * (x - x2) = x pow 2 - (x1 + x2) * x + x1 * x2 /\
131 a * (x - x1) * (x - x2) = a * x pow 2 + ( -- a * (x1 + x2)) * x + a * x1 * x2 `;;
134 let VIET_THEOREM = prove(`! x1 x2 a b c. (!x. a * x pow 2 + b * x + c =
135 a * (x - x1) * (x - x2)) ==> -- b = a * ( x1 + x2 ) /\ c = a * x1 * x2 `,
136 REWRITE_TAC[PRE_VIET; REAL_LDISTRIB;REAL_SUB_LDISTRIB;
137 REAL_ARITH ` a - b * c = a + -- b * c `; REAL_ARITH` ( a + b ) + c =
139 REWRITE_TAC[REAL_MUL_ASSOC; EQUATE_CONEFS_POLINOMIAL_POW2] THEN
140 SIMP_TAC[] THEN REAL_ARITH_TAC);;
142 let ADD_SUB_POW2_EX = REAL_RING ` ( a + b ) pow 2 = a pow 2 + &2 * a * b + b pow 2 /\
143 ( a - b ) pow 2 = a pow 2 - &2 * a * b + b pow 2 `;;
145 let PRESENT_SUB_POW2 = REAL_RING` ! a b. ( a - b ) pow 2 = ( a + b ) pow 2
148 let DIST_ROOT_AND_DISCRIMINANT = prove(` ! a b c x1 x2. ( ! x. a * x pow 2 + b * x + c =
149 a * ( x - x1 ) * ( x - x2 ) )
150 ==> ( a pow 2 ) * ( x1 - x2 ) pow 2 = b pow 2 - &4 * a * c `,
151 NHANH (SPEC_ALL VIET_THEOREM) THEN REWRITE_TAC[PRESENT_SUB_POW2] THEN
152 SIMP_TAC[REAL_ARITH ` -- b = a <=> b = -- a `] THEN REAL_ARITH_TAC);;
154 (* le 33. P 22 MARKED *)
156 let REAL_EQ_TO_LE_LT = REAL_ARITH `
157 ( a = b <=> ~( a < b \/ b < a ) )`;;
159 let FEBRUARY_13_09 = prove(` &0 < (u - v) dot (&2 % x - (u + v)) <=>
160 &0 < (u - v) dot (x - &1 / &2 % (u + v)) `,
161 ONCE_REWRITE_TAC[MESON[REAL_ARITH ` &0 < a <=> &0 < &2 * a `]` (a <=> &0 < b ) <=>
162 ( a <=> &0 < &2 * b ) `] THEN ONCE_REWRITE_TAC[VECTOR_ARITH ` x * (a dot b) =
164 REWRITE_TAC[GSYM VECTOR_SUB_DISTRIBUTE; VECTOR_MUL_ASSOC] THEN
165 REWRITE_TAC[REAL_ARITH ` &2 * &1 / &2 = &1 `; VECTOR_MUL_LID]);;
167 let SUB_DOT_NEG_TO_POS = MESON[VECTOR_ARITH ` ( a - b ) dot x =
168 -- (( b - a ) dot x ) `; REAL_ARITH ` -- a < &0 <=> &0 < a `]
169 `! a b. ( a - b ) dot x < &0 <=> &0 < ( b - a ) dot x `;;
172 let LEMMA6 = prove(` !(u:real^3) v. ~(u = v) ==> plane_norm (bis u v) `,
173 REWRITE_TAC[plane_norm; bis] THEN REPEAT STRIP_TAC THEN
174 EXISTS_TAC ` (u: real^3) - v ` THEN
175 EXISTS_TAC ` &1 / &2 % ((u: real^3) + v )` THEN
176 REWRITE_TAC[FUN_EQ_THM; IN_ELIM_THM] THEN ASM_SIMP_TAC[VECTOR_SUB_EQ] THEN
177 REWRITE_TAC[REAL_EQ_TO_LE_LT; DIST_LT_HALF_PLANE;FEBRUARY_13_09;
178 SUB_DOT_NEG_TO_POS] THEN SIMP_TAC[VECTOR_ADD_SYM] THEN MESON_TAC[]);;
180 let BXVMKNF = LEMMA6;;
183 let b_coef = BC_DEL_FOR;;
184 let c_coef = b_coef ;;
186 let DELTA_X34_B = prove(` ! x12 x13 x14 x23 x24 x. delta_x34 x12 x13 x14 x23 x24 x =
187 -- &2 * x12 * x + b_coef x12 x13 x14 x23 x24 `, REWRITE_TAC[ delta_x34; b_coef]);;
192 let EQ_POW2_COND = prove(`!a b. &0 <= a /\ &0 <= b ==> (a = b <=> a pow 2 = b pow 2)`,
193 REWRITE_TAC[REAL_ARITH` a = b <=> a <= b /\ b <= a `] THEN SIMP_TAC[POW2_COND]);;
196 let EQ_SQRT_POW2_EQ = prove(` &0 <= a /\ &0 <= b ==> ( a = sqrt b <=> a pow 2 = b ) `,
197 SIMP_TAC[SQRT_WORKS; EQ_POW2_COND]);;
201 let LEMMA33 = prove(` !x34 x12 x13 v1 x14 v3 x23 v2 v4 x24 x34' x34'' a.
202 condA v1 v2 v3 v4 x12 x13 x14 x23 x24 x34 /\
203 (! x. muy_delta x12 x13 x14 x23 x24 x = a * ( x - x34' ) * ( x - x34''))
205 ==> delta_x34 x12 x13 x14 x23 x24 x34' =
206 sqrt (ups_x x12 x13 x23 * ups_x x12 x14 x24) /\
207 delta_x34 x12 x13 x14 x23 x24 x34'' =
208 --sqrt (ups_x x12 x13 x23 * ups_x x12 x14 x24) `,
209 REWRITE_TAC[muy_delta; DELTA_X34_B; DELTA_COEFS] THEN
210 SIMP_TAC[EQUATE_CONEFS_POLINOMIAL_POW2; PRE_VIET;
211 REAL_ARITH ` -- a = b <=> b = -- a`] THEN
212 SIMP_TAC[REAL_RING `-- &2 * x12 * x34' + -- --x12 * (x34' + x34'') = a <=>
213 -- &2 * x12 * x34'' + -- --x12 * (x34' + x34'') = -- a `] THEN
214 REWRITE_TAC[REAL_ARITH` -- &2 * x12 * x34'' + -- --x12 * (x34' + x34'')
215 = x12 * ( x34' - x34'' ) `; condA] THEN REPEAT STRIP_TAC THEN
216 EXPAND_TAC "x12" THEN EXPAND_TAC "x13" THEN EXPAND_TAC "x23" THEN
217 EXPAND_TAC "x14" THEN EXPAND_TAC "x24" THEN
218 UNDISCH_TAC ` x34' <= (x34'':real)` THEN
219 ONCE_REWRITE_TAC[REAL_ARITH ` a <= b <=> &0 <= b - a `] THEN
220 ONCE_REWRITE_TAC[ REAL_ARITH ` a * ( b - c ) = -- ( a * ( c - b ) ) `] THEN
221 MP_TAC (GEN_ALL TROI_OI_DAT_HOI) THEN MP_TAC REAL_LE_POW_2 THEN
222 REWRITE_TAC[REAL_ARITH` -- a = -- b <=> a = b `] THEN
223 SIMP_TAC[UPS_X_SYM; REAL_LE_MUL; EQ_SQRT_POW2_EQ ] THEN
224 ASM_SIMP_TAC[] THEN REPEAT STRIP_TAC THEN
225 ONCE_REWRITE_TAC[ REAL_ARITH ` ( a * b ) pow 2 = a pow 2 * b pow 2 `] THEN
226 REWRITE_TAC[PRESENT_SUB_POW2] THEN
227 REWRITE_TAC[REAL_SUB_LDISTRIB; REAL_ARITH ` a pow 2 * b pow 2 =
228 ( -- a * b ) pow 2 /\ a pow 2 * &4 * b = -- a * &4 * -- a * b `] THEN
229 UNDISCH_TAC `b_coef x12 x13 x14 x23 x24 = --a * (x34' + x34'')` THEN
230 UNDISCH_TAC `c_coef x12 x13 x14 x23 x24 = a * x34' * x34''` THEN
231 UNDISCH_TAC `(a: real) = --x12` THEN ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN
232 SIMP_TAC[] THEN SIMP_TAC[REAL_ARITH` -- -- a = a /\ ( -- a * b) pow 2 =
233 ( a * b ) pow 2 /\ ( a * -- b) pow 2 = ( a * b ) pow 2 `; REAL_ADD_SYM;
234 REAL_MUL_SYM] THEN SIMP_TAC[REAL_ADD_SYM; REAL_MUL_SYM] THEN
235 ONCE_REWRITE_TAC[REAL_ARITH ` ( a * b ) pow 2 = ( b * -- a ) pow 2 `] THEN
236 SIMP_TAC[] THEN REPEAT STRIP_TAC THEN EXPAND_TAC "a" THEN
237 REWRITE_TAC[REAL_RING ` a - -- c * b * &4 = a + &4 * c * b `] THEN
238 MESON_TAC[AGBWHRD; UPS_X_SYM]);;
241 (* let CMUDPKT = LEMMA33;; *)
246 let LEMMA_OF_LE20 = prove(` ! x y z: real^3.
248 dist3 x y <= #2.52 /\
253 ==> ~collinear {x, y, z} `,
256 ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN
257 REWRITE_TAC[MESON[]` (! a b c s. P a b c = s ==> Q a b c ) <=>
258 (! a b c . Q a b c ) `] THEN
259 SIMP_TAC[COL_EQ_UPS_0] THEN
260 MATCH_MP_TAC (TAUT` a ==> b ==> a `) THEN
261 REWRITE_TAC[GSYM dist3] THEN
262 REWRITE_TAC[REAL_ENTIRE] THEN
263 CONV_TAC REAL_FIELD);;
267 let LT_POW2_EQ_LT = MESON[POW2_COND_LT; REAL_ARITH ` a <= b <=> ~ ( b < a ) `]
268 `&0 < a /\ &0 < b ==> ( a < b <=> a pow 2 < b pow 2 ) `;;
270 let ETA_Y_LT_SQRT2 = prove(`eta_y #2.2 #2.2 #2.52 < sqrt #2`,
271 REWRITE_TAC[eta_y; eta_x; ups_x] THEN LET_TR THEN
272 CONV_TAC REAL_RAT_REDUCE_CONV THEN MP_TAC (REAL_FIELD ` &14641 / &8131< &2 `)
273 THEN MP_TAC (REAL_FIELD ` &0 < &2 /\ &0 < &14641 / &8131 `) THEN
274 NHANH (SPEC_ALL SQRT_POS_LT) THEN REWRITE_TAC[ REAL_ARITH ` #2 = &2 `] THEN
275 SIMP_TAC[REAL_ARITH ` &0 < a ==> &0 <= a `;SQRT_POS_LT; LT_POW2_EQ_LT; SQRT_WORKS]);;
277 let ETA_YY_LT_SQRT2 = MESON[ETA_Y_LT_SQRT2; REAL_ARITH ` #2 = &2 `]`
278 eta_y #2.2 #2.2 #2.52 < sqrt ( &2 ) `;;
280 let THANG_DEU = prove(` &2 <= x ==> &2 pow 2 <= x pow 2 `,
281 NHANH (REAL_ARITH ` &2 <= x ==> &0 <= &2 /\ &0 <= x `)
282 THEN MESON_TAC[POW2_COND]);;
284 let NGAY23_THANG2_09 = prove(` &2 <= y /\ y <= sqrt (&8) ==>
285 &2 pow 2 <= y * y /\ y * y <= &8 `,
286 REWRITE_TAC[ GSYM REAL_POW_2] THEN DISCH_TAC THEN CONJ_TAC THENL
287 [ASM_MESON_TAC[REAL_ARITH ` &2 <= a ==> &0 <= &2 /\ &0 <= a `;POW2_COND];
288 ASM_MESON_TAC[ SQRT_WORKS; REAL_ARITH ` &0 <= &8 `;
289 POW2_COND; REAL_ARITH `&2 <= a /\ a <= b ==> &0 <= b /\ &0 <= a `]]);;
293 let ETA_Y_SQRT8_2_251 = prove(` eta_y ( sqrt (&8) ) (&2) #2.51 < #1.453`,
294 REWRITE_TAC[eta_y; eta_x; ups_x; GSYM POW_2] THEN
296 REWRITE_TAC[MESON[SQRT_WORKS; REAL_ARITH ` &0 <= &8 `]` sqrt (&8) pow 2 = &8 `] THEN
297 CONV_TAC REAL_RAT_REDUCE_CONV THEN
298 MP_TAC (REAL_FIELD ` &0 < &20160320000 / &9551113999 /\ &0 < #1.453 `) THEN
299 NHANH (SPEC_ALL SQRT_POS_LT) THEN
300 SIMP_TAC[LT_POW2_EQ_LT; REAL_ARITH ` &0 < a ==> &0 <= a `; SQRT_POW_2] THEN
302 CONV_TAC REAL_FIELD );;
304 let CDEUSDF_CHANGE = CDEUSDF;;
307 let CIRCUMCENTER_FORMULAR = prove(` ! va vb vc. ~collinear {va, vb, vc}
308 ==> circumcenter {va, vb, vc} =
310 (dist3 va vc pow 2 + dist3 va vb pow 2 - dist3 vb vc pow 2)) /
311 (ups_x (dist3 vb vc pow 2) (dist3 va vc pow 2) (dist3 va vb pow 2)) %
314 (dist3 vb vc pow 2 + dist3 va vb pow 2 - dist3 va vc pow 2)) /
315 (ups_x (dist3 vb vc pow 2) (dist3 va vc pow 2) (dist3 va vb pow 2)) %
318 (dist3 vb vc pow 2 + dist3 va vc pow 2 - dist3 va vb pow 2)) /
319 (ups_x (dist3 vb vc pow 2) (dist3 va vc pow 2) (dist3 va vb pow 2)) %
321 ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN
322 MP_TAC CDEUSDF_CHANGE THEN LET_TR THEN MESON_TAC[]);;
324 let LE_EX = REAL_ARITH ` &0 <= a <=> a = &0 \/ &0 < a `;;
326 let SUM_UPS_X_1 = prove(`!a b c.
328 ==> (c * (b + a - c)) / ups_x a b c +
329 (a * (c + b - a)) / ups_x a b c +
330 (b * (c + a - b)) / ups_x a b c =
331 &1`, REWRITE_TAC[ups_x] THEN CONV_TAC REAL_FIELD);;
334 MESON[POW2_COND; REAL_ARITH `&2 <= a /\ a <= b ==> &0 <= b /\ &0 <= a `]`
335 &2 <= y /\ y <= b ==> y pow 2 <= b pow 2 `;;
338 let FACTOR_OF_QUADRARTIC = prove(`! a b c x. ~(a = &0) /\
339 &0 <= b pow 2 - &4 * a * c ==> a * x pow 2 + b * x + c =
341 (x - (--b + sqrt (b pow 2 - &4 * a * c)) / (&2 * a)) *
342 (x - (--b - sqrt (b pow 2 - &4 * a * c)) / (&2 * a))` ,
343 REWRITE_TAC[PRE_VIET] THEN SIMP_TAC[REAL_FIELD ` ~( a = &0 ) ==>
344 -- a * ( ( --b + del) / ( &2 * a ) + ( --b - del) / ( &2 * a )) = b `] THEN
345 REWRITE_TAC[REAL_FIELD ` a / b * a' / b = ( a * a' ) / ( b pow 2 ) `] THEN
346 REWRITE_TAC[REAL_FIELD ` a / b * a' / b = ( a * a' ) / ( b pow 2 ) `;
347 REAL_DIFFSQ; GSYM REAL_POW_2] THEN SIMP_TAC[SQRT_WORKS] THEN
348 SIMP_TAC[REAL_FIELD ` ~ ( a = &0 ) ==> a * (--b pow 2 -
349 (b pow 2 - &4 * a * c)) / (&2 * a) pow 2 = c `]);;
352 let COMPUTE_TO_QUA_POLY = prove(` #2.696 <= x /\ x <= sqrt8 ==>
353 x pow 2 * ( &1 / eta_y x #2.45 #2.45 pow 2 -
354 &1 / eta_y x ( &2 ) #2.51 pow 2 ) = &4331842500 / &363188227801 * x pow 4 +
355 -- &45702201 / &302530802 * x pow 2 +
356 &529046001 / &2520040000 `, REWRITE_TAC[eta_y; eta_x; ups_x] THEN
358 CONV_TAC REAL_RAT_REDUCE_CONV THEN
359 NHANH (MESON[REAL_ARITH ` #2.696 <= x /\ x <= sqrt8 ==>
360 &0 <= #2.696 /\ &0 <= x `; REAL_LE_MUL2] ` #2.696 <= x /\ x <= sqrt8 ==>
361 #2.696 * #2.696 <= x * x /\ x * x <= sqrt8 * sqrt8 `) THEN
362 NHANH (MESON[REAL_ARITH ` #2.696 * #2.696 <= x ==> &0 <= #2.696 * #2.696 /\ &0 <= x `; REAL_LE_MUL2] `
363 #2.696 * #2.696 <= x /\ x <= hh ==> (#2.696 * #2.696) * #2.696 * #2.696 <= x * x /\
364 x * x <= hh * hh `) THEN
365 REWRITE_TAC[sqrt8] THEN
366 REWRITE_TAC[REAL_POLY_CONV ` (--(x * x) * x * x - &16 - &3969126001 / &100000000 +
367 &2 * (x * x) * &63001 / &10000 +
369 &63001 / &1250) `] THEN
370 REWRITE_TAC[REAL_POLY_CONV `
371 (--(x * x) * x * x - &5764801 / &160000 - &5764801 / &160000 +
372 &2 * (x * x) * &2401 / &400 +
373 &2 * (x * x) * &2401 / &400 +
374 &5764801 / &80000) `] THEN
375 REWRITE_TAC[REAL_ARITH ` x pow 4 = ( x pow 2 ) pow 2 `] THEN
376 MP_TAC (REAL_ARITH ` ~ ( -- &1 = &0 ) /\ &0 <= ( &103001 / &5000 ) pow 2 - &4 * ( -- &1 ) * -- &529046001 / &100000000 `) THEN
377 SIMP_TAC[FACTOR_OF_QUADRARTIC] THEN
378 CONV_TAC REAL_RAT_REDUCE_CONV THEN
379 REWRITE_TAC[REAL_ARITH ` (&252004 / &625) = ( &502 / &25 ) * ( &502 / &25 ) `] THEN
380 REWRITE_TAC[MESON[REAL_ARITH ` &0 <= &502 / &25 /\ x * x = x pow 2 `; POW_2_SQRT]`
381 sqrt ( ( &502 / &25 ) * ( &502 / &25 )) = ( &502 / &25 ) `] THEN
382 CONV_TAC REAL_RAT_REDUCE_CONV THEN
383 REWRITE_TAC[ GSYM POW_2] THEN
384 REWRITE_TAC[REAL_ARITH ` a * x pow 2 + b * x = ( a * x + b ) * x `] THEN
385 REWRITE_TAC[MESON[SQRT_WORKS; REAL_ARITH ` &0 <= &8`]` sqrt (&8) pow 2 = &8 `] THEN
386 NHANH (REAL_FIELD ` (&113569 / &15625 <= x pow 2 /\ x pow 2 <= &8)
387 ==> &0 <= (-- &1 * x pow 2 + &2401 / &100) /\
388 &0 <= (x pow 2 - &2601 / &10000 ) /\
389 &0 <= -- ((x pow 2 - &203401 / &10000) )/\ &0 <= &5764801 / &160000 /\
390 &0 <= &63001 / &2500`) THEN
391 MP_TAC REAL_LE_POW_2 THEN
392 REWRITE_TAC[REAL_ARITH ` -- &1 * a * b = a * -- b `] THEN
393 REWRITE_TAC[REAL_FIELD ` ( &1 / a ) pow 2 = &1 / ( a pow 2 ) `] THEN
394 MP_TAC REAL_LE_MUL THEN
395 MP_TAC REAL_LE_DIV THEN
396 SIMP_TAC[ SQRT_WORKS] THEN
397 REWRITE_TAC[REAL_SUB_LDISTRIB] THEN
398 REWRITE_TAC[REAL_FIELD ` &1 / ( a / b ) = b / a `] THEN
399 SIMP_TAC[REAL_FIELD ` &113569 / &15625 <= a ==> a * ( b / ( a * c )) = b / c `] THEN
400 REWRITE_TAC[REAL_POLY_CONV ` ((-- &1 * x pow 2 + &2401 / &100) * x pow 2) / (&5764801 / &160000) -
401 ((x pow 2 - &2601 / &10000) * --(x pow 2 - &203401 / &10000)) /
402 (&63001 / &2500) `] THEN
403 REWRITE_TAC[REAL_ARITH ` a pow 4 = a pow 2 pow 2 `]);;
406 REAL_ARITH ` &4650694416 = ( &68196 ) pow 2 `;;
407 REAL_ARITH` &4650694416 / &363188227801 = ( &68196 / &602651 ) pow 2 `;;
410 let PHAN_TICH = prove( `! x. &4331842500 / &363188227801 *
411 (x pow 2 - &488365801 / &44090000) *
412 (x pow 2 - &2081667 / &1310000) =
413 &4331842500 / &363188227801 * x pow 4 +
414 -- &45702201 / &302530802 * x pow 2 +
415 &529046001 / &2520040000` , REAL_ARITH_TAC);;
417 let Q_TR = prove(`! x. #2.696 <= x /\ x <= sqrt8 ==>
419 (&1 / eta_y x #2.45 #2.45 pow 2 - &1 / eta_y x (&2) #2.51 pow 2) <= &0 `,
420 SIMP_TAC[COMPUTE_TO_QUA_POLY; GSYM PHAN_TICH ] THEN
421 NHANH (MESON[REAL_ARITH ` #2.696 <= x /\ x <= hh ==> &0 <= #2.696 /\ &0 <= x`
422 ; REAL_LE_MUL2] ` #2.696 <= x /\ x <= hh ==>
423 #2.696 * #2.696 <= x * x /\ x * x <= hh * hh `) THEN
424 REWRITE_TAC[REAL_ARITH `
425 &4331842500 / &363188227801 * a <= &0 <=> a <= &0 `] THEN
426 CONV_TAC REAL_RAT_REDUCE_CONV THEN
427 REWRITE_TAC[REAL_ARITH ` &0 <=
428 &4331842500 / &363188227801 * a <=> &0 <= a `; sqrt8; GSYM POW_2;
429 MESON[SQRT_WORKS; REAL_ARITH ` &0 <= &8 `]` sqrt (&8) pow 2 = &8 `] THEN
430 NHANH (REAL_ARITH ` &113569 / &15625 <= x pow 2 /\
431 x pow 2 <= &8 ==> x pow 2 - &488365801 / &44090000 <= &0 /\
432 x pow 2 - &2081667 / &1310000 >= &0 `) THEN
433 REWRITE_TAC[ REAL_ARITH ` ( a >= &0 <=> &0 <= a)/\ (a <= &0 <=> &0 <= -- a ) `] THEN
434 REWRITE_TAC[REAL_ARITH ` -- ( a * b ) = -- a * b `] THEN
435 MESON_TAC[REAL_LE_MUL]);;
437 let SQRT8_LT = prove(` sqrt (&8) < &4 * #2.45 `,
438 MP_TAC (REAL_ARITH ` &0 < &8 /\ &0 < &4 * #2.45`) THEN
439 SIMP_TAC[SQRT_POS_LT; LT_POW2_EQ_LT] THEN
440 SIMP_TAC[REAL_LT_IMP_LE; SQRT_WORKS] THEN REAL_ARITH_TAC);;
444 let SQRT8_POW2 = MESON[SQRT_WORKS; REAL_ARITH ` &0 <= &8 `]` sqrt (&8) pow 2 = &8 `;;
447 let IM_UP_POS = prove(`! x. #2.696 <= x /\ x <= sqrt8 ==>
448 &0 < ups_x (x * x) (#2.45 * #2.45) (#2.45 * #2.45) /\
449 &0 < ups_x (x * x) (&2 * &2) (#2.51 * #2.51) `,
450 REWRITE_TAC[ups_x] THEN
451 REWRITE_TAC[REAL_IDEAL_CONV [` (x:real) pow 2 `]`
453 (#2.45 * #2.45) * #2.45 * #2.45 -
454 (#2.45 * #2.45) * #2.45 * #2.45 +
455 &2 * (x * x) * #2.45 * #2.45 +
456 &2 * (x * x) * #2.45 * #2.45 +
457 &2 * (#2.45 * #2.45) * #2.45 * #2.45 `] THEN
458 CONV_TAC REAL_RAT_REDUCE_CONV THEN
459 REWRITE_TAC[REAL_POLY_CONV ` --(x * x) * x * x - &16 - &3969126001 / &100000000 +
460 &2 * (x * x) * &63001 / &10000 +
462 &63001 / &1250 `] THEN
463 NHANH (REAL_ARITH` #2.696 <= x /\ x <= s ==> &0 <= #2.696 /\
464 &0 <= x /\ &0 <= s `) THEN
465 ONCE_REWRITE_TAC[MESON[]` a /\ b ==> c <=> b ==> a ==> c `] THEN
466 SIMP_TAC[POW2_COND; sqrt8; SQRT8_POW2] THEN
467 NHANH (REAL_ARITH` #2.696 pow 2 <= x /\ x <= &8 ==>
468 &0 < &2401 / &100 + -- &1 * x /\ &0 < x /\
469 ~ ( -- &1 = &0 ) /\ &0 <= ( &103001 / &5000 ) pow 2 - &4 * -- &1 *
470 -- &529046001 / &100000000 `) THEN
471 SIMP_TAC[REAL_ARITH ` x pow 4 = x pow 2 pow 2 `; FACTOR_OF_QUADRARTIC] THEN
472 CONV_TAC REAL_RAT_REDUCE_CONV THEN
473 REWRITE_TAC[REAL_ARITH ` &252004 / &625 = ( &502 / &25) pow 2 `] THEN
474 REWRITE_TAC[MESON[POW_2_SQRT; REAL_ARITH ` &0 <= &502 / &25 `]`
475 sqrt ((&502 / &25) pow 2) = &502 / &25 `] THEN
476 CONV_TAC REAL_RAT_REDUCE_CONV THEN
477 NHANH (REAL_ARITH ` &113569 / &15625 <= x pow 2 /\ x pow 2 <= &8 ==>
478 &0 < x pow 2 - &2601 / &10000 /\ &0 < -- (x pow 2 - &203401 / &10000) `) THEN
479 REWRITE_TAC[REAL_ARITH ` -- &1 * a * b = a * --b `] THEN
480 SIMP_TAC[REAL_LT_MUL]);;
483 let IMP_ETAY_POS = prove( `! x. #2.696 <= x /\ x <= sqrt8 ==>
484 &0 < eta_y x #2.45 #2.45 /\ &0 < eta_y x (&2) #2.51 `,
485 REWRITE_TAC[eta_y; eta_x] THEN
487 NHANH (MESON[REAL_ARITH ` &0 <= #2.696`; REAL_LE_MUL2]`
488 #2.696 <= x ==> #2.696 * #2.696 <= x * x `) THEN
489 NHANH (REAL_ARITH ` #2.696 * #2.696 <= x * x ==>
490 &0 < ((x * x) * (#2.45 * #2.45) * #2.45 * #2.45) /\
491 &0 < ((x * x) * (&2 * &2) * #2.51 * #2.51) `) THEN
492 MESON_TAC[IM_UP_POS; REAL_LT_DIV; SQRT_POS_LT]);;
495 let REAL_LE_RDIV_0 = prove(` ! a b. &0 < b ==> ( &0 <= a / b <=> &0 <= a ) `,
496 REWRITE_TAC[REAL_ARITH ` &0 <= a <=> &0 < a \/ a = &0 `] THEN
497 SIMP_TAC[REAL_LT_RDIV_0] THEN
498 SIMP_TAC[REAL_FIELD `&0 < b ==> ( a / b = &0 <=> a = &0 ) `]);;
501 let NHSJMDH = prove(` ! y. #2.696 <= y /\ y <= sqrt8 ==>
502 eta_y y (&2) (#2.51) <= eta_y y #2.45 (#2.45) `,
503 NHANH (SPEC_ALL Q_TR) THEN
504 ONCE_REWRITE_TAC[MESON[]` a /\ b ==> c <=> a ==> b ==> c `] THEN
505 NHANH (MESON[REAL_ARITH ` &0 <= #2.696`; REAL_LE_MUL2]`
506 #2.696 <= x ==> #2.696 * #2.696 <= x * x `) THEN
507 REWRITE_TAC[POW_2] THEN
508 NHANH (REAL_ARITH `#2.696 * #2.696 <= y ==> &0 < y `) THEN
509 REWRITE_TAC[REAL_ARITH ` a * b <= &0 <=> &0 <= a * -- b `] THEN
510 SIMP_TAC[REAL_LE_MUL_EQ] THEN
511 ONCE_REWRITE_TAC[MESON[]`( a/\b ) /\ c <=> ( a /\ c ) /\ b `] THEN
512 NHANH (SPEC_ALL IMP_ETAY_POS) THEN
513 NHANH (REAL_ARITH ` &0 < eta_y a b c ==> ~(eta_y a b c = &0 ) `) THEN
514 REWRITE_TAC[GSYM REAL_POSSQ] THEN SIMP_TAC[REAL_FIELD ` &0 < a /\
515 &0 < b ==> -- (&1 / a - &1 / b) = (a - b) / ( a * b ) `] THEN
516 PHA THEN SIMP_TAC[REAL_LT_MUL; REAL_LE_RDIV_0] THEN
517 REWRITE_TAC[GSYM REAL_DIFFSQ] THEN
518 SIMP_TAC[REAL_LT_ADD; REAL_LE_MUL_EQ] THEN REAL_ARITH_TAC);;
521 let SQRT8_LE = MESON[ REAL_ARITH ` &0 <= &8`; SQRT_WORKS]` &0 <= sqrt (&8) `;;
523 let RELATE_POW2 = prove(` ( a = &0 <=> a pow 2 = &0 ) /\
524 ( &0 < a pow 2 <=> &0 < a \/ ~( &0 <= a )) `,
525 MP_TAC (REAL_FIELD ` a = &0 <=> a pow 2 = &0 `) THEN DISCH_TAC THEN
526 CONJ_TAC THENL [ASM_SIMP_TAC[]; MP_TAC REAL_LE_POW_2] THEN
527 MP_TAC (REAL_ARITH `( ! a. &0 < a \/ ~(&0 <= a) \/ a = &0 )`) THEN
528 MP_TAC (REAL_FIELD ` a = &0 <=> a pow 2 = &0 `) THEN
529 REWRITE_TAC[REAL_ARITH ` A <= b <=> A = b \/ A < b `] THEN
530 MESON_TAC[REAL_ARITH ` ~ ( a = &0 /\ ( &0 < a \/ ~( &0 <= a ) )) `]);;
532 let LT_POW2_COND = prove(`!a b. &0 <= a /\ &0 <= b ==> (a < b <=> a pow 2 < b pow 2)`,
533 REPEAT GEN_TAC THEN ASM_CASES_TAC ` a = &0 ` THENL
534 [ASM_SIMP_TAC[REAL_ARITH` &0 pow 2 = &0 `] THEN MESON_TAC[RELATE_POW2];
535 ASM_SIMP_TAC[REAL_LE_LT]] THEN STRIP_TAC THENL [ASM_MESON_TAC[LT_POW2_EQ_LT];
536 EXPAND_TAC "b"] THEN UNDISCH_TAC `&0 < a ` THEN REWRITE_TAC[REAL_ARITH `
537 &0 pow 2 = &0 /\ (a < &0 <=> ~(&0 <= a))`] THEN MP_TAC REAL_LE_POW_2 THEN
538 MESON_TAC[REAL_LT_IMP_LE]);;
541 let POS_IMP_POW2 = MESON[REAL_LE_TRANS; POW2_COND]` &0 <= a /\ a <= b ==> a pow 2
545 let SQRT8_LE_EQ_8_LESS_POW2 = prove(` sqrt (&8 ) <= a ==> &8 <= a pow 2 `,
546 MP_TAC SQRT8_LE THEN MESON_TAC[SQRT8_POW2; POS_IMP_POW2]);;
549 let MINIMAL_QUADRATIC_POLY = prove(`
550 ! b c (x:real). ( &4 * c - b pow 2 ) / &4 <= x pow 2 + b * x + c `,
551 ONCE_REWRITE_TAC[REAL_ARITH ` a <= b <=> &0 <= b - a `] THEN
552 REWRITE_TAC[REAL_ARITH ` (x pow 2 + b * x + c) - (&4 * c - b pow 2) / &4
553 = ( x + b / &2 ) pow 2 `; REAL_LE_POW_2]);;
555 let GREATER_THAN_MID_QUADRATIC_PO = prove(` ! b c x x0. -- b / &2 <= x0 /\ x0 <= x ==>
556 x0 pow 2 + b * x0 + c <= x pow 2 + b * x + c `,
557 REWRITE_TAC[REAL_ARITH ` x0 pow 2 + b * x0 + c <= x pow 2 + b * x + c
558 <=> &0 <= ( x - x0 ) * ( x + x0 + b ) `] THEN
559 MESON_TAC[REAL_ARITH ` --b / &2 <= x0 /\ x0 <= x ==>
560 &0 <= x - x0 /\ &0 <= x + x0 + b `; REAL_LE_MUL]);;
565 let SQRT8_TWO_TWO = prove(` sqrt (&8) <= &2 + &2 `,
566 MP_TAC SQRT8_LE THEN NHANH (MESON[REAL_ARITH ` &0 <= &2 + &2 `]
567 `&0 <= sqrt (&8) ==> &0 <= &2 + &2 `) THEN SIMP_TAC[POW2_COND] THEN
568 SIMP_TAC[REAL_ARITH ` &0 <= &8 `; SQRT_WORKS] THEN REAL_ARITH_TAC);;
571 let A_POS_DELTA = prove(` &0 < delta (#3.2 pow 2 ) (sqrt8 pow 2 ) (&2 pow 2) (sqrt8 pow 2)
572 (&2 pow 2) (&2 pow 2) `, REWRITE_TAC[delta; sqrt8; SQRT8_POW2] THEN REAL_ARITH_TAC);;
574 let MET_LAM_ROI = prove(` #3.2 < sqrt8 + &2 /\ #3.2 < &2 + &2 /\ sqrt8 < sqrt8 + &2 /\
576 REWRITE_TAC[sqrt8; REAL_ARITH ` a < sqrt (&8) + b <=> a - b < sqrt (&8) `] THEN
577 REWRITE_TAC[REAL_ARITH ` sqrt (&8) - &2 < sqrt (&8) `] THEN
578 CONV_TAC REAL_RAT_REDUCE_CONV THEN MP_TAC SQRT8_LE THEN
579 MP_TAC (REAL_ARITH` &0 <= &6 / &5 /\ &0 <= &4 `) THEN
580 SIMP_TAC[LT_POW2_COND ] THEN SIMP_TAC[LT_POW2_COND; SQRT8_POW2 ] THEN
584 let PROVE_POS_THINGS = prove(` ! x. x IN {#3.2 , sqrt8, &2 , sqrt8, &2, &2 } ==> &0 <= x `,
585 REWRITE_TAC[SET_RULE `( !x. x IN {a,b,c,d,s,e} ==> p x ) <=>
586 p a /\ p b /\ p c /\ p d /\ p s /\ p e `;sqrt8; SQRT8_LE] THEN REAL_ARITH_TAC);;
590 let IMP_GT_THAN_TWO = prove(` ! v1 v2 w1 (w2:real^3).
591 CARD {v1, w1,v2, w2} = 4 /\
592 packing {v1, w1,v2, w2}
593 ==> &2 <= dist3 w1 v2 /\
596 REWRITE_TAC[CARD4; packing; GSYM dist3; sqrt8] THEN SET_TAC[]);;
601 let LEMMA_FOR_PAHFWSI = prove(`! v1 v2 v3 v4. CARD {v1, v2, v3, v4} = 4 /\
602 packing {v1, v2, v3, v4} /\
603 dist (v1,v3) <= #3.2 /\
604 #2.51 <= dist (v1,v2) /\
605 dist (v2,v4) <= #2.51
606 ==> (!x. x IN {#3.2, #2.51, &2, #2.51, &2, &2} ==> &0 <= x) /\
609 #2.51 < #2.51 + &2 /\
612 delta (#3.2 pow 2) (#2.51 pow 2) (&2 pow 2) (#2.51 pow 2) (&2 pow 2)
614 CARD {v1, v2, v3, v4} = 4 /\
615 #2.51 <= dist3 v1 v2 /\
619 dist3 v1 v3 <= #3.2 /\
620 dist3 v2 v4 <= #2.51 `,
621 REWRITE_TAC[SET_RULE ` (!x. x IN {a,b,c,d,e,f} ==> P x ) <=>
622 P a /\ P b /\ P c /\ P d /\ P e /\ P f `; REAL_ARITH `
628 &0 <= #2.51 /\ #2.51 < &2 + #2.51 /\
631 #3.2 < #2.51 + &2 /\ #3.2 < &2 + #2.51 /\
632 #2.51 < #2.51 + &2 `] THEN SIMP_TAC[GSYM dist3] THEN
633 REWRITE_TAC[CARD4; packing; delta; dist3] THEN CONV_TAC REAL_RAT_REDUCE_CONV
636 let LEMMA_OF_39 = prove(` ! (v1:real^3) v2 w1 w2.
637 CARD {v1, v2, w1, w2} = 4 /\
638 packing {v1, v2, w1, w2} /\
639 dist (w1,w2) <= #2.51 /\
640 dist (v1,v2) <= #3.07
641 ==> (!x. x IN {#2.51, &2, &2, #3.07, &2, &2} ==> &0 <= x) /\
647 delta (#2.51 pow 2) (&2 pow 2) (&2 pow 2) (#3.07 pow 2) (&2 pow 2)
649 CARD {w1, v1, w2, v2} = 4 /\
654 dist3 w1 w2 <= #2.51 /\
655 dist3 v1 v2 <= #3.07 `,
656 REWRITE_TAC[SET_RULE ` (!x. x IN {a,b,c,d,e,f} ==> P x ) <=>
657 P a /\ P b /\ P c /\ P d /\ P e /\ P f `; delta; GSYM dist3] THEN CONV_TAC
658 REAL_RAT_REDUCE_CONV THEN REPEAT GEN_TAC THEN STRIP_TAC THEN CONJ_TAC THENL
659 [ASM_MESON_TAC[SET_RULE ` {v1, v2, w1, w2} = {w1, v1, w2, v2}`];DOWN_TAC]
660 THEN REWRITE_TAC[CARD4; packing; dist3] THEN SET_TAC[]);;
662 let LEMMA_OF_LEMMA40 = prove(`! v1 v2 w1 (w2:real^3). CARD {v1, v2, w1, w2} = 4 /\
663 packing {v1, v2, w1, w2} /\
664 dist (v1,v2) <= #3.2 /\
665 dist (w1,w2) <= #2.51 /\
667 ==> (!x. x IN {#3.2, #2.2, &2, #2.51, &2, &2} ==> &0 <= x) /\
673 delta (#3.2 pow 2) (#2.2 pow 2) (&2 pow 2) (#2.51 pow 2) (&2 pow 2)
675 CARD {v1, w1, v2, w2} = 4 /\
676 #2.2 <= dist3 v1 w1 /\
680 dist3 v1 v2 <= #3.2 /\
681 dist3 w1 w2 <= #2.51 `,
682 REWRITE_TAC[SET_RULE ` (! x. x IN {a,b,c,d,e,f} ==> P x ) <=>
683 P a /\ P b /\ P c /\ P d /\ P e /\ P f `; delta] THEN
684 CONV_TAC REAL_RAT_REDUCE_CONV THEN SIMP_TAC[SET_RULE `
685 {v1, v2, w1, w2} = {v1, w1, v2, w2} `; packing] THEN
686 SIMP_TAC[CARD4; GSYM dist3] THEN SET_TAC[]);;
689 `#3.114467 < x ==> delta (#2.51 pow 2) (&2 pow 2) (&2 pow 2) (&2 pow 2)
690 (&2 pow 2) (x pow 2) < &0`,
691 NHANH (MESON[REAL_ARITH ` #3.114467 < x ==> &0 < #3.114467 /\ &0 < x `;
692 LT_POW2_EQ_LT]` #3.114467 < x ==> ( #3.114467 ) pow 2 < x pow 2 `) THEN
693 REWRITE_TAC[delta] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
694 REWRITE_TAC[ REAL_POLY_CONV ` -- &126002 / &625 - &4 * &4 * x pow 2 - &4 * &4 * x pow 2 +
695 &63001 / &10000 * x pow 2 *
696 (-- &63001 / &10000 + &4 + &4 + &4 + &4 - x pow 2) +
697 &4 * &4 * (&23001 / &10000 + &4 + &0 + x pow 2) +
698 &4 * &4 * (&63001 / &10000 + -- &4 + &4 + x pow 2) `] THEN
699 REWRITE_TAC[REAL_ARITH ` a pow 4 = a pow 2 pow 2 `] THEN
700 REWRITE_TAC[REAL_ARITH ` a * x pow 2 + b * x = ( a * x + b ) * x `] THEN
701 NHANH (REAL_ARITH `&9699904694089 / &1000000000000 < x pow 2
702 ==> -- &63001 / &10000 * x pow 2 + &6111033999 / &100000000 < &0` ) THEN
703 NHANH (REAL_ARITH `&9699904694089 / &1000000000000 < x ==> &0 < x `) THEN
704 REWRITE_TAC[REAL_ARITH ` a < &0 <=> &0 < -- a `;
705 REAL_ARITH ` -- ( a * b ) = -- a * b `] THEN MESON_TAC[REAL_LT_MUL]);;
708 let LEMMA41 = prove(`! v1 v2 v3 (v4:real^3).
709 CARD {v1,v2,v3,v4} = 4 /\
710 dist3 v1 v2 = #2.51 /\
715 ==> dist3 v3 v4 <= #3.114467 `,
716 REPEAT GEN_TAC THEN MP_TAC LEMMA3 THEN LET_TR THEN
717 REWRITE_TAC[REAL_ARITH ` x <= #3.114467 <=> ~ (#3.114467 < x ) `] THEN
718 REWRITE_TAC[REAL_ARITH ` x <= #3.114467 <=> ~ (#3.114467 < x ) `;
719 MESON[]` a ==> ~ b <=> a /\ b ==> F `] THEN PHA THEN
720 NHANH (SPEC_ALL (prove(`! (v1:real^3) v2 v3 v4. dist3 v1 v2 = #2.51 /\
721 dist3 v1 v3 = &2 /\ dist3 v1 v4 = &2 /\ dist3 v2 v3 = &2 /\ dist3 v2 v4 = &2 /\
722 #3.114467 < dist3 v3 v4 ==> delta (dist (v1,v2) pow 2) (dist (v1,v3) pow 2)
723 (dist (v1,v4) pow 2) (dist (v2,v3) pow 2) (dist (v2,v4) pow 2)
724 (dist (v3,v4) pow 2) < &0 `, SIMP_TAC[dist3] THEN MESON_TAC[LEOF41]))) THEN
725 REWRITE_TAC[REAL_ARITH ` a < &0 <=> ~( &0 <= a ) `; dist3] THEN MESON_TAC[]);;
727 let YXWIPMH = LEMMA41;;
729 let LEMMA_OF_L42 = prove(`sqrt8 <= dist3 v2 v4 /\ #3.488 <= x
730 ==> -- &1 * x pow 2 * dist3 v2 v4 pow 2 +
732 &103001 / &5000 * x pow 2 +
733 -- &529046001 / &100000000 <
737 NHANH (MESON[REAL_ARITH ` &0 <= a /\ a <= b /\ #3.488 <= x ==> &0 <= b /\
738 &0 <= #3.488 /\ &0 <= x `; POW2_COND]`
739 &0 <= a /\ a <= b /\ #3.488 <= x ==> a pow 2 <= b pow 2 /\
740 #3.488 pow 2 <= x pow 2 `) THEN
741 REWRITE_TAC[SQRT8_POW2; sqrt8] THEN
742 NHANH (MESON[REAL_ARITH ` &0 <= a /\ a <= b /\ #3.488 <= x ==> &0 <= b /\
743 &0 <= #3.488 /\ &0 <= x `; POW2_COND]`
744 &0 <= a /\ a <= b /\ #3.488 <= x ==> a pow 2 <= b pow 2 /\
745 #3.488 pow 2 <= x pow 2 `) THEN
746 REWRITE_TAC[SQRT8_POW2] THEN
747 NHANH (MESON[REAL_ARITH ` &0 <= &8 /\ &0 <= #3.488 pow 2 `; REAL_LE_MUL2]` &8 <= a /\
748 #3.488 pow 2 <= b ==> &8 * #3.488 pow 2 <= a * b `) THEN
749 REWRITE_TAC[REAL_ARITH` a pow 4 = a pow 2 pow 2 `] THEN
750 NHANH (MESON[REAL_ARITH ` #3.488 pow 2 <= x ==> &0 <= #3.488 pow 2 /\
751 &0 <= x `; POW2_COND]` #3.488 pow 2 <= x ==> #3.488 pow 2 pow 2 <= x pow 2 `) THEN
752 REWRITE_TAC[REAL_ARITH ` a + -- &1 * x pow 2 + b * x + c =
753 a + -- &1 * ( x pow 2 + -- b * x + -- c ) `] THEN
754 NHANH (prove(` #3.488 pow 2 <= x pow 2 ==>
756 --(&103001 / &5000) * #3.488 pow 2 +
757 --(-- &529046001 / &100000000) <= x pow 2 pow 2 +
758 --(&103001 / &5000) * x pow 2 +
759 --(-- &529046001 / &100000000) `,
760 MP_TAC (REAL_ARITH ` -- ( --(&103001 / &5000)) / &2 <= #3.488 pow 2 `) THEN
761 MESON_TAC[GREATER_THAN_MID_QUADRATIC_PO ])) THEN
766 let LEMMA_IN_LEMMA42_P25 = prove(` ! v1 v2 v3 v4 x.
767 dist3 v1 v2 = #2.51 /\
768 dist3 v1 v4 = #2.51 /\
771 sqrt8 <= dist3 v2 v4 /\
773 ==> delta (dist3 v1 v2 pow 2) ( x pow 2) (dist3 v1 v4 pow 2)
776 (dist3 v3 v4 pow 2) < &0 `,
778 NHANH (MESON[REAL_ARITH` #3.488 <= x ==> &0 <= #3.488 /\ &0 <= x `; POW2_COND]`
779 #3.488 <= x ==> (#3.488 pow 2 <= x pow 2 ) `) THEN
780 REWRITE_TAC[delta] THEN
781 CONV_TAC REAL_RAT_REDUCE_CONV THEN
782 REWRITE_TAC[REAL_POLY_CONV `--(&63001 / &10000 * x pow 2 * &4) -
783 &63001 / &10000 * &63001 / &10000 * dist3 v2 v4 pow 2 -
784 x pow 2 * &63001 / &2500 -
785 &4 * dist3 v2 v4 pow 2 * &4 +
788 (-- &63001 / &10000 +
792 dist3 v2 v4 pow 2 - &4) +
795 (&63001 / &10000 - x pow 2 +
797 &4 - dist3 v2 v4 pow 2 +
802 x pow 2 - &63001 / &10000 - &4 +
805 REWRITE_TAC[REAL_IDEAL_CONV [` y pow 2 `] `-- &1 * x pow 4 * y pow 2 +
806 -- &1 * x pow 2 * y pow 4 +
807 &103001 / &5000 * x pow 2 * y pow 2 +
808 -- &529046001 / &100000000 * y pow 2 `] THEN
809 REWRITE_TAC[MESON[]` a/\ #3.488 <= x /\ c <=> (a/\ #3.488 <= x )/\ c`] THEN
810 NHANH (LEMMA_OF_L42) THEN
811 REWRITE_TAC[sqrt8] THEN
812 NHANH (SQRT8_LE_EQ_8_LESS_POW2) THEN
815 UNDISCH_TAC ` &8 <= dist3 v2 v4 pow 2 ` THEN
816 UNDISCH_TAC ` -- &1 * x pow 2 * dist3 v2 v4 pow 2 +
818 &103001 / &5000 * x pow 2 +
819 -- &529046001 / &100000000 <
821 ABBREV_TAC ` xx = (-- &1 * x pow 2 * dist3 v2 v4 pow 2 +
823 &103001 / &5000 * x pow 2 +
824 -- &529046001 / &100000000)` THEN
825 NHANH (REAL_ARITH ` &8 <= a ==> &0 < a `) THEN
826 REWRITE_TAC[REAL_ARITH ` ( a * b < &0 <=> &0 < ( -- a ) * b )/\
827 ( a < &0 <=> &0 < -- a )`] THEN
828 SIMP_TAC[REAL_LT_MUL]);;
830 let PAATDXJ =prove(` ! v1 v2 v3 (v4:real^3).
831 CARD {v1,v2,v3,v4} = 4 /\
832 dist3 v1 v2 = #2.51 /\
833 dist3 v1 v4 = #2.51 /\
837 ==> dist3 v1 v3 < #3.488 `,
838 MP_TAC LEMMA3 THEN LET_TR THEN REWRITE_TAC[REAL_ARITH ` a < b <=> ~ ( b <= a )`]
839 THEN REWRITE_TAC[MESON[]` a ==> ~ b <=> ~( a /\b)`] THEN
840 PHA THEN NHANH (SPEC_ALL LEMMA_IN_LEMMA42_P25) THEN
841 REWRITE_TAC[REAL_ARITH` a < b <=> ~(b <= a ) `] THEN SIMP_TAC[dist3]);;
844 let CONVEX_NORMBALL = REWRITE_RULE[GSYM NORMBALL_BALL] CONVEX_BALL ;;
847 SPEC `{(v1:real^N),v2,v3,v4}` CONVEX_HULL_FINITE;;
849 let CONVEX_HULL_4_EQUIV = prove(` ! v1 v2 v3 (v4:real^N).
850 conv {v1,v2,v3,v4} = { x | ? a b c d.
855 a + b + c + d = &1 /\
856 a % v1 + b % v2 + c % v3 + d % v4 = x } `,
857 REWRITE_TAC[conv; FUN_EQ_THM; affsign; lin_combo; UNION_EMPTY;
858 IN_ELIM_THM; sgn_ge] THEN
859 REWRITE_TAC[MESON[]` x = vsum aa bb /\ a /\ b <=>
860 a /\ b /\ vsum aa bb = x `] THEN
861 ONCE_REWRITE_TAC[SET_RULE ` a s ==> b <=> s IN a ==> b `] THEN
862 SIMP_TAC[CONVEX_HULL_FINITE_STEP; FINITE_INSERT; FINITE_RULES] THEN
863 REWRITE_TAC[REAL_ARITH `x - y = z:real <=> x = y + z`;
864 VECTOR_ARITH `x - y = z:real^N <=> x = y + z`] THEN
865 REWRITE_TAC[VECTOR_ADD_RID; REAL_ADD_RID] THEN MESON_TAC[IN]);;
868 let TXDIACY = prove(`! (a:real^3) b c d (v0: real^3) r.
869 {a, b, c, d} SUBSET normball v0 r
870 ==> convex hull {a, b, c, d} SUBSET normball v0 r `,
871 REPEAT GEN_TAC THEN MP_TAC (MESON[CONVEX_NORMBALL]` convex (normball (v0:real^3) r)`) THEN
872 NHANH (MESON[FINITE6] ` {a, b, c, d} SUBSET s ==> FINITE {(a:real^3),b,c,d} `) THEN
873 REWRITE_TAC[CONVEX_HULL4; CONVEX_EXPLICIT] THEN
875 REWRITE_TAC[SET_RULE ` {a | P a } SUBSET b <=> (! a. P a ==> a IN b)`] THEN
876 REWRITE_TAC[MESON[]` (! y. ( ? u. P u y ) ==> Q y ) <=>
877 (! y u. P u y ==> Q y ) `] THEN
878 REWRITE_TAC[MESON[]`(!y u. P u /\ Q u /\ R u = y ==> Z y) <=>
879 (!u. P u /\ Q u ==> Z (R u)) `] THEN MESON_TAC[]);;
880 let LEMMA14 = TXDIACY;;
883 let ECSEVNC = prove(`?t1 t2 t3 t4.
884 !v1 v2 v3 v4 (v: real^3).
885 ~coplanar_alt {v1, v2, v3, v4}
886 ==> t1 v1 v2 v3 v4 v +
892 t1 v1 v2 v3 v4 v % v1 +
893 t2 v1 v2 v3 v4 v % v2 +
894 t3 v1 v2 v3 v4 v % v3 +
895 t4 v1 v2 v3 v4 v % v4 /\
897 v = ta % v1 + tb % v2 + tc % v3 + td % v4 /\
898 ta + tb + tc + td = &1
899 ==> ta = t1 v1 v2 v3 v4 v /\
900 tb = t2 v1 v2 v3 v4 v /\
901 tc = t3 v1 v2 v3 v4 v /\
902 td = t4 v1 v2 v3 v4 v) `,
903 REWRITE_TAC[GSYM SKOLEM_THM; RIGHT_EXISTS_IMP_THM] THEN REPEAT
904 GEN_TAC THEN NHANH (SPEC_ALL (prove(`!v1 v2 v3 v0 v:real^3.
905 ~coplanar_alt {v0, v1, v2, v3} ==> (?t1 t2 t3. v - v0 = t1 % (v1 - v0)
906 + t2 % (v2 - v0) + t3 % (v3 - v0) /\ (!ta tb tc. v - v0 = ta % (v1 - v0)
907 + tb % (v2 - v0) + tc % (v3 - v0) ==> ta = t1 /\
908 tb = t2 /\ tc = t3))`, SIMP_TAC[NONCOPLANAR_3_BASIS]))) THEN
909 STRIP_TAC THEN EXISTS_TAC ` &1 - t1 - t2 - t3 ` THEN
910 EXISTS_TAC ` t1:real ` THEN EXISTS_TAC ` t2:real ` THEN
911 EXISTS_TAC ` t3:real ` THEN CONJ_TAC THENL [REAL_ARITH_TAC;
912 CONJ_TAC] THENL [UNDISCH_TAC ` (v:real^3) - v1 = t1 % (v2 - v1) +
913 t2 % (v3 - v1) + t3 % (v4 - v1)` THEN
914 CONV_TAC VECTOR_ARITH; REPEAT GEN_TAC] THEN
915 REWRITE_TAC[MESON[]` a /\ b ==> c <=> b ==> a ==> c `;
916 REAL_ARITH ` ta + tb + tc + td = &1 <=> ta = &1 - tb - tc - td `] THEN
917 SIMP_TAC[] THEN REWRITE_TAC[VECTOR_ARITH ` v = (&1 - tb - tc - td) % v1
918 + tb % v2 + tc % v3 + td % v4 <=> v - v1 = tb % ( v2 - v1 ) +
919 tc % ( v3 - v1 ) + td % ( v4 - v1 ) `] THEN ASM_MESON_TAC[]);;
921 let LEMMA76 = ECSEVNC;;
923 let COEFS_4 = new_specification ["COEF4_1"; "COEF4_2"; "COEF4_3"; "COEF4_4"] ECSEVNC ;;
925 let COEF_1_EQ_ZERO = prove(` ! v1 v2 v3 v4 (v:real^3).
926 ~ coplanar_alt {v1,v2,v3,v4} ==>
927 ( COEF4_1 v1 v2 v3 v4 v = &0 <=> v IN aff {v2,v3,v4} ) `,
928 REWRITE_TAC[aff; AFFINE_HULL_3; IN_ELIM_THM] THEN
929 NHANH (SPEC_ALL COEFS_4) THEN
930 REPEAT GEN_TAC THEN STRIP_TAC THEN
931 ONCE_REWRITE_TAC[REAL_ARITH` u + v + w = &0 + u + v + w `] THEN
932 ONCE_REWRITE_TAC[VECTOR_ARITH` u + v + w = &0 % v1 + u + v + w `] THEN
935 let EQ_IMP_COPLANAR = prove(`! a b c (d:real^3). ( a = b \/ a = c \/ a = d )
936 ==> coplanar_alt {a,b,c,d} `,
937 REPEAT STRIP_TAC THENL [
938 ASM_SIMP_TAC[SET_RULE ` a INSERT ( a INSERT s ) = a INSERT s `] THEN
939 MP_TAC (DIMINDEX_3) THEN MESON_TAC[COPLANAR_3; ARITH_RULE` a = 3 ==> 2 <= a `];
940 ONCE_REWRITE_TAC[SET_RULE` {a,b,v,c} = {a,v,b,c} `] THEN
941 ASM_SIMP_TAC[SET_RULE ` a INSERT ( a INSERT s ) = a INSERT s `] THEN
942 MP_TAC (DIMINDEX_3) THEN MESON_TAC[COPLANAR_3; ARITH_RULE` a = 3 ==> 2 <= a `];
943 ONCE_REWRITE_TAC[SET_RULE` {a,b,v,c} = {a,c,v,b} `] THEN
944 ASM_SIMP_TAC[SET_RULE ` a INSERT ( a INSERT s ) = a INSERT s `] THEN
945 MP_TAC (DIMINDEX_3) THEN MESON_TAC[COPLANAR_3; ARITH_RULE` a = 3 ==> 2 <= a `]]);;
947 let AFFINE_HULL_FINITE_STEP_GEN = prove
948 (`!P:real^N->real->bool.
949 ((?u. (!x. x IN {} ==> P x (u x)) /\
950 sum {} u = w /\ vsum {} (\x. u(x) % x) = y) <=>
951 w = &0 /\ y = vec 0) /\
952 (FINITE(s:real^N->bool) /\
953 (!y. a IN s /\ P a y ==> P a (y / &2)) /\
954 (!x y. a IN s /\ P a x /\ P a y ==> P a (x + y))
955 ==> ((?u. (!x. x IN (a INSERT s) ==> P x (u x)) /\
956 sum (a INSERT s) u = w /\
957 vsum (a INSERT s) (\x. u(x) % x) = y) <=>
958 ?v u. P a v /\ (!x. x IN s ==> P x (u x)) /\
960 vsum s (\x. u(x) % x) = y - v % a))`,
961 GEN_TAC THEN SIMP_TAC[SUM_CLAUSES; VSUM_CLAUSES; NOT_IN_EMPTY] THEN
962 CONJ_TAC THENL [MESON_TAC[]; ALL_TAC] THEN DISCH_TAC THEN
963 ASM_CASES_TAC `(a:real^N) IN s` THEN ASM_REWRITE_TAC[] THENL
964 [ASM_SIMP_TAC[SET_RULE `a IN s ==> a INSERT s = s`] THEN EQ_TAC THEN
965 REWRITE_TAC[LEFT_IMP_EXISTS_THM] THENL
966 [X_GEN_TAC `u:real^N->real` THEN STRIP_TAC THEN
967 EXISTS_TAC `(u:real^N->real) a / &2` THEN
968 EXISTS_TAC `\x:real^N. if x = a then u x / &2 else u x`;
969 MAP_EVERY X_GEN_TAC [`v:real`; `u:real^N->real`] THEN
971 EXISTS_TAC `\x:real^N. if x = a then u x + v else u x`] THEN
972 ASM_SIMP_TAC[] THEN (CONJ_TAC THENL [ASM_MESON_TAC[]; ALL_TAC]) THEN
973 ONCE_REWRITE_TAC[COND_RAND] THEN ONCE_REWRITE_TAC[COND_RATOR] THEN
974 ASM_SIMP_TAC[VSUM_CASES; SUM_CASES] THEN
975 ASM_SIMP_TAC[GSYM DELETE; SUM_DELETE; VSUM_DELETE] THEN
976 ASM_SIMP_TAC[SET_RULE `a IN s ==> {x | x IN s /\ x = a} = {a}`] THEN
977 REWRITE_TAC[SUM_SING; VSUM_SING] THEN
978 (CONJ_TAC THENL [REAL_ARITH_TAC; VECTOR_ARITH_TAC]);
979 EQ_TAC THEN REWRITE_TAC[LEFT_IMP_EXISTS_THM] THENL
980 [X_GEN_TAC `u:real^N->real` THEN STRIP_TAC THEN
981 EXISTS_TAC `(u:real^N->real) a` THEN
982 EXISTS_TAC `u:real^N->real` THEN ASM_SIMP_TAC[IN_INSERT] THEN
983 REPEAT(FIRST_X_ASSUM(SUBST1_TAC o SYM)) THEN
984 CONJ_TAC THENL [REAL_ARITH_TAC; VECTOR_ARITH_TAC];
985 MAP_EVERY X_GEN_TAC [`v:real`; `u:real^N->real`] THEN
987 EXISTS_TAC `\x:real^N. if x = a then v:real else u x` THEN
988 ASM_SIMP_TAC[IN_INSERT] THEN CONJ_TAC THENL
989 [ASM_MESON_TAC[]; ALL_TAC] THEN
990 ONCE_REWRITE_TAC[COND_RAND] THEN ONCE_REWRITE_TAC[COND_RATOR] THEN
991 ASM_SIMP_TAC[VSUM_CASES; SUM_CASES] THEN
992 ASM_SIMP_TAC[GSYM DELETE; SUM_DELETE; VSUM_DELETE] THEN
993 ASM_SIMP_TAC[SET_RULE `~(a IN s) ==> {x | x IN s /\ x = a} = {}`] THEN
994 ASM_SIMP_TAC[SET_RULE `~(a IN s) ==> s DELETE a = s`] THEN
995 REWRITE_TAC[SUM_CLAUSES; VSUM_CLAUSES] THEN
996 CONJ_TAC THENL [REAL_ARITH_TAC; VECTOR_ARITH_TAC]]]);;
1000 let THEOREM_RE_AFF_LT31 = prove
1001 (`!v1 v2 v3 vv x:real^N.
1002 ~(v1 = vv) /\ ~(v2 = vv) /\ ~(v3 = vv)
1003 ==> ((?f. f vv < &0 /\
1004 sum {v1, v2, v3, vv} f = &1 /\
1005 x = vsum {v1, v2, v3, vv} (\v. f v % v)) <=>
1007 a + b + c + t = &1 /\
1008 x = a % v1 + b % v2 + c % v3 + t % vv /\
1011 REPEAT STRIP_TAC THEN MATCH_MP_TAC EQ_TRANS THEN
1013 `?f. (!x:real^N. x IN {v1, v2, v3, vv} ==> vv = x ==> f x < &0) /\
1014 sum {v1, v2, v3, vv} f = &1 /\
1015 vsum {v1, v2, v3, vv} (\v. f v % v) = x` THEN
1017 [ASM_REWRITE_TAC[FORALL_IN_INSERT; NOT_IN_EMPTY] THEN MESON_TAC[];
1018 SIMP_TAC[AFFINE_HULL_FINITE_STEP_GEN;
1019 REAL_ARITH `x < &0 /\ y < &0 ==> x + y < &0`;
1020 REAL_ARITH `x < &0 ==> x / &2 < &0`;
1021 FINITE_INSERT; CONJUNCT1 FINITE_RULES; RIGHT_EXISTS_AND_THM] THEN
1022 ASM_REWRITE_TAC[IN_ELIM_THM;
1023 REAL_ARITH `x - y:real = z <=> x = y + z`;
1024 VECTOR_ARITH `x - y:real^N = z <=> x = y + z`] THEN
1025 REWRITE_TAC[VECTOR_ADD_RID; REAL_ADD_RID] THEN MESON_TAC[]]);;
1027 let AFF_LT31 = prove(` ! v1 v2 v3 (vv: real^N). ~ (vv IN {v1,v2,v3} ) ==>
1028 aff_lt {v1,v2,v3} {vv} =
1029 { x| ? a b c t. t < &0 /\ a + b + c + t = &1 /\
1030 x = a % v1 + b % v2 + c % v3 + t % vv } `,
1031 REWRITE_TAC[IN_SET3; DE_MORGAN_THM; aff_lt_def;FUN_EQ_THM;
1032 affsign; lin_combo; sgn_lt] THEN
1033 REWRITE_TAC[SET_RULE` {v1, v2, v3} UNION {vv} = {v1, v2, v3, vv}`] THEN
1034 REWRITE_TAC[SET_RULE` a /\ (!w. {vv} w ==> f w < &0) /\ b
1035 <=> f vv < &0 /\ b /\ a `] THEN
1036 SIMP_TAC[THEOREM_RE_AFF_LT31; IN_ELIM_THM] THEN SET_TAC[]);;
1038 let AFF_LT21 = prove(`! a b (v0:real^N). ~ ( a = v0 ) /\ ~( b = v0 ) ==>
1043 x = ta % a + tb % b + t % v0} `,
1044 REWRITE_TAC[SET_RULE` ~(a = v0) /\ ~(b = v0) <=>
1045 ~ ( v0 IN {a,b} ) `] THEN
1046 ONCE_REWRITE_TAC[SET_RULE` {a,b} = {a,b,b} `] THEN SIMP_TAC[AFF_LT31] THEN
1047 SIMP_TAC[AFF_LT31; FUN_EQ_THM; IN_ELIM_THM] THEN
1048 REWRITE_TAC[VECTOR_ARITH` a % b + c % b + x = ( a + c ) % b + x `] THEN
1049 MESON_TAC[REAL_ARITH` a + b + c = ( a + b ) + c `;
1050 VECTOR_ARITH ` a % v = ( a + &0 ) % v `; REAL_ARITH `
1051 a + b = a + &0 + b `]);;
1054 let INSET3 = SET_RULE` a IN {a,b,c} /\ b IN {a,b,c} /\ c IN {a,b,c} `;;
1056 let AFF_GT33 = prove(`! (v1:real^N) v2 v3 w1 w2 w3.
1057 {v1, v2, v3} INTER {w1, w2, w3} = {}
1058 ==> aff_gt {v1, v2, v3} {w1, w2, w3} =
1059 {x | ?a1 a2 a3 b1 b2 b3.
1063 a1 + a2 + a3 + b1 + b2 + b3 = &1 /\
1065 a1 % v1 + a2 % v2 + a3 % v3 + b1 % w1 + b2 % w2 + b3 % w3}`,
1066 REWRITE_TAC[aff_gt_def; FUN_EQ_THM; affsign; lin_combo; sgn_gt] THEN
1067 REPEAT STRIP_TAC THEN
1068 MATCH_MP_TAC EQ_TRANS THEN
1069 REWRITE_TAC[SET_RULE ` ( a INSERT b ) UNION c =
1070 b UNION ( a INSERT c ) /\ {} UNION b = b `] THEN
1071 EXISTS_TAC ` (? f. x = vsum {v3, v2, v1, w1, w2, w3} (\v. f v % v) /\
1072 (!(w:real^N). w IN {v3,v2,v1, w1, w2, w3} ==> w IN {w1,w2,w3} ==> &0 < f w) /\
1073 sum {v3, v2, v1, w1, w2, w3} f = &1 ) ` THEN
1074 REWRITE_TAC[SET_RULE` (!x. ({v1, v2, v3} INTER {w1, w2, w3}) x <=> {} x)
1075 <=> {v1, v2, v3} INTER {w1, w2, w3} = {} `] THEN
1077 FIRST_X_ASSUM MP_TAC THEN
1078 REWRITE_TAC[SET_RULE` (!x. ({v1, v2, v3} INTER {w1, w2, w3}) x <=> {} x)
1079 <=> {v1, v2, v3} INTER {w1, w2, w3} = {} `] THEN
1080 MESON_TAC[SET_RULE` {v1, v2, v3} INTER {w1, w2, w3} = {} ==>
1081 ( (!w. {w1, w2, w3} w ==> &0 < f w) <=>
1082 (!w. w IN {v3, v2, v1, w1, w2, w3}
1083 ==> w IN {w1, w2, w3}
1085 REWRITE_TAC[MESON[]` a /\ (!z. P z ) /\ aa = &1 <=>
1086 (!z. P z ) /\ aa = &1 /\ a `]] THEN
1087 ONCE_REWRITE_TAC[MESON[]` a = vsum b c <=> vsum b c = a `] THEN
1088 SIMP_TAC[AFFINE_HULL_FINITE_STEP_GEN;FINITE_INSERT; CONJUNCT1 FINITE_RULES;
1089 RIGHT_EXISTS_AND_THM;
1090 REAL_ARITH `&0 < x /\ &0 < y ==> &0 < x + y`;
1091 REAL_ARITH `&0 < x ==> &0 < x / &2 `] THEN
1092 FIRST_X_ASSUM MP_TAC THEN
1093 REWRITE_TAC[SET_RULE` (!x. ({v1, v2, v3} INTER {w1, w2, w3}) x <=> {} x)
1094 <=> {v1, v2, v3} INTER {w1, w2, w3} = {} `; SET_RULE` ( a INSERT s ) INTER ss = {} <=>
1095 ~ ( a IN ss ) /\ s INTER ss = {} `] THEN
1096 SIMP_TAC[INSET3] THEN
1097 SIMP_TAC[INSET3; REAL_ARITH` a - b = c <=> a = b + c `;
1098 VECTOR_ARITH` a:real^N - b = c <=> a = b + c `] THEN
1099 REWRITE_TAC[ GSYM RIGHT_EXISTS_AND_THM; ZERO_NEUTRAL;
1100 IN_ELIM_THM; VECTOR_ARITH ` a + vec 0 = a `] THEN
1102 MESON_TAC[REAL_ARITH` a + b + c + d = c + b + a + d `;
1103 VECTOR_ARITH` ( a:real^N ) + b + c + d = c + b + a + d `]);;
1105 let AFF_GE33 = prove_by_refinement(
1106 `! (v1:real^N) v2 v3 w1 w2 w3.
1107 {v1, v2, v3} INTER {w1, w2, w3} = {}
1108 ==> aff_ge {v1, v2, v3} {w1, w2, w3} =
1109 {x | ?a1 a2 a3 b1 b2 b3.
1113 a1 + a2 + a3 + b1 + b2 + b3 = &1 /\
1115 a1 % v1 + a2 % v2 + a3 % v3 + b1 % w1 + b2 % w2 + b3 % w3}`,
1118 (REWRITE_TAC[aff_gt_def; aff_ge_def; FUN_EQ_THM; affsign; lin_combo; sgn_gt; sgn_ge]);
1120 (MATCH_MP_TAC EQ_TRANS );
1121 (REWRITE_TAC[SET_RULE ` ( a INSERT b ) UNION c = b UNION ( a INSERT c ) /\ {} UNION b = b `]);
1122 (EXISTS_TAC ` (? f. x = vsum {v3, v2, v1, w1, w2, w3} (\v. f v % v) /\ (!(w:real^N). w IN {v3,v2,v1, w1, w2, w3} ==> w IN {w1,w2,w3} ==> &0 <= f w) /\ sum {v3, v2, v1, w1, w2, w3} f = &1 ) `);
1124 (FIRST_X_ASSUM MP_TAC);
1125 (REWRITE_TAC[SET_RULE` (!x. ({v1, v2, v3} INTER {w1, w2, w3}) x <=> {} x) <=> {v1, v2, v3} INTER {w1, w2, w3} = {} `]);
1126 BY((MESON_TAC[SET_RULE` {v1, v2, v3} INTER {w1, w2, w3} = {} ==> ( (!w. {w1, w2, w3} w ==> &0 <= f w) <=> (!w. w IN {v3, v2, v1, w1, w2, w3} ==> w IN {w1, w2, w3} ==> &0 <= f w) ) `]));
1127 (REWRITE_TAC[MESON[]` a /\ (!z. P z ) /\ aa = &1 <=> (!z. P z ) /\ aa = &1 /\ a `]);
1128 (ONCE_REWRITE_TAC[MESON[]` a = vsum b c <=> vsum b c = a `]);
1129 ( SIMP_TAC[AFFINE_HULL_FINITE_STEP_GEN;FINITE_INSERT; CONJUNCT1 FINITE_RULES; RIGHT_EXISTS_AND_THM; REAL_ARITH `&0 <= x /\ &0 <= y ==> &0 <= x + y`; REAL_ARITH `&0 <= x ==> &0 <= x / &2 `]);
1130 (FIRST_X_ASSUM MP_TAC);
1131 (REWRITE_TAC[SET_RULE` (!x. ({v1, v2, v3} INTER {w1, w2, w3}) x <=> {} x) <=> {v1, v2, v3} INTER {w1, w2, w3} = {} `; SET_RULE` ( a INSERT s ) INTER ss = {} <=> ~ ( a IN ss ) /\ s INTER ss = {} `]);
1133 (SIMP_TAC[INSET3; REAL_ARITH` a - b = c <=> a = b + c `; VECTOR_ARITH` a:real^N - b = c <=> a = b + c `]);
1134 (REWRITE_TAC[ GSYM RIGHT_EXISTS_AND_THM; ZERO_NEUTRAL; IN_ELIM_THM; VECTOR_ARITH ` a + vec 0 = a `]);
1136 BY( (MESON_TAC[REAL_ARITH` a + b + c + d = c + b + a + d `; VECTOR_ARITH` ( a:real^N ) + b + c + d = c + b + a + d `]))
1141 let AFF_GE_12 = prove(`!v0 (a:real^N) b.
1143 ==> aff_ge {v0} {a, b} =
1147 tv + ta + tb = &1 /\
1148 x = tv % v0 + ta % a + tb % b}`,
1149 REWRITE_TAC[SET_RULE ` ~(v0 = a \/ v0 = b) <=> {v0} INTER {a,b} = {} `] THEN
1150 ONCE_REWRITE_TAC[SET_RULE` {a} = {a,a} `] THEN
1151 ONCE_REWRITE_TAC[SET_RULE` {a,a} = {a,a,a} `] THEN
1152 ONCE_REWRITE_TAC[SET_RULE` {a,b,b,b} = {a,b,b} `] THEN
1153 SIMP_TAC[AFF_GE33] THEN REWRITE_TAC[FUN_EQ_THM; IN_ELIM_THM] THEN
1154 REPEAT STRIP_TAC THEN
1155 REWRITE_TAC[GSYM VECTOR_ADD_RDISTRIB; VECTOR_ARITH` a % v +
1156 b % v + y = ( a + b ) % v + y `] THEN GONTONG THEN EQ_TAC THENL [
1157 MESON_TAC[REAL_ARITH` a1 + a2 + a3 + b1 + b2 + b3 =
1158 ( a1 + a2 + a3 ) + b1 + b2 + b3 `; REAL_ARITH ` &0 <= a
1159 /\ &0 <= b ==> &0 <= a + b `];STRIP_TAC] THEN EXISTS_TAC` tv: real `
1160 THEN EXISTS_TAC` &0 ` THEN EXISTS_TAC` &0` THEN EXISTS_TAC` ta :real `
1161 THEN EXISTS_TAC` &0` THEN EXISTS_TAC` tb:real ` THEN
1162 ASM_SIMP_TAC[REAL_ARITH ` a <= a `; ZERO_NEUTRAL]);;
1165 let INSET3 = SET_RULE` a IN {a, b, c} /\ b IN {a, b, c} /\ c IN {a, b, c}
1166 /\ {a, b, c} a /\ {a, b, c} b /\ {a, b, c} c `;;
1170 let AFF_LE_LT33 = prove(`! (v1:real^N) v2 v3 w1 w2 w3.
1171 {v1, v2, v3} INTER {w1, w2, w3} = {}
1172 ==> aff_le {v1, v2, v3} {w1, w2, w3} =
1173 {x | ?a1 a2 a3 b1 b2 b3.
1177 a1 + a2 + a3 + b1 + b2 + b3 = &1 /\
1179 a1 % v1 + a2 % v2 + a3 % v3 + b1 % w1 + b2 % w2 + b3 % w3} /\
1180 aff_lt {v1, v2, v3} {w1, w2, w3} =
1181 {x | ?a1 a2 a3 b1 b2 b3.
1185 a1 + a2 + a3 + b1 + b2 + b3 = &1 /\
1187 a1 % v1 + a2 % v2 + a3 % v3 + b1 % w1 + b2 % w2 + b3 % w3} `,
1188 REWRITE_TAC[IN_ELIM_THM; aff_le_def; FUN_EQ_THM; aff_lt_def;
1189 affsign; lin_combo; sgn_lt; sgn_le] THEN
1190 REWRITE_TAC[SET_RULE` {v1, v2, v3} UNION {w1, w2, w3} =
1191 {v1,v2,v3,w1,w2,w3} `] THEN
1192 ONCE_REWRITE_TAC[SET_RULE` {w1, w2, w3} w ==> P w <=>
1193 w IN {v1,v2,v3,w1,w2,w3} ==> {w1,w2,w3} w ==> P w `] THEN
1194 REWRITE_TAC[MESON[]` a = vsum aa bb /\
1195 (! w. P w ) /\ b <=> (! w. P w ) /\ b /\ vsum aa bb = a `] THEN
1196 SIMP_TAC[AFFINE_HULL_FINITE_STEP_GEN;
1197 REAL_ARITH `( x < &0 /\ y < &0 ==> x + y < &0) /\ ( x <= &0 /\ y <= &0 ==> x + y <= &0)`;
1198 REAL_ARITH ` (x < &0 ==> x / &2 < &0 ) /\ (x <= &0 ==> x / &2 <= &0 )`;
1199 FINITE_INSERT; CONJUNCT1 FINITE_RULES
1200 ; RIGHT_EXISTS_AND_THM] THEN
1201 SIMP_TAC[ GSYM RIGHT_EXISTS_AND_THM; SET_RULE `
1202 (!x. ({v1, v2, v3} INTER s ) x <=> {} x) <=>
1203 ~ ( s v1 ) /\ ~ ( s v2 ) /\ ~ ( s v3 ) `; INSET3] THEN
1204 REWRITE_TAC[REAL_ARITH` a - b = c <=> a = b + c`; REAL_ARITH `
1205 a + &0 = a `; VECTOR_ARITH` (a:real^N) - b = c <=> a = b + c`;
1206 VECTOR_ARITH` a + vec 0 = a `] THEN
1212 let AFF_GES_LTS = prove(` ! a b c (v0 :real^N).
1213 ~ ( a = v0 ) /\ ~( b = v0 ) /\ ~( c = v0 ) ==>
1214 aff_gt {a, b} {v0} =
1216 ta + tb + t = &1 /\ &0 < t /\ x = ta % a + tb % b + t % v0} /\
1217 aff_ge {a, b} {v0} =
1221 x = ta % a + tb % b + t % v0} /\
1222 aff_lt {a,b,c} {v0} =
1223 { x| ? ta tb tc t. t < &0 /\ ta + tb + tc + t = &1 /\
1224 x = ta % a + tb % b + tc % c + t % v0 } /\
1225 aff_gt {a,b,c} {v0} =
1226 { x| ? ta tb tc t. &0 < t /\ ta + tb + tc + t = &1 /\
1227 x = ta % a + tb % b + tc % c + t % v0 } `,
1228 ONCE_REWRITE_TAC[SET_RULE` {a} = {a,a,a} `] THEN
1229 ONCE_REWRITE_TAC[SET_RULE` {a,b,b,b} = {a,b,b} `] THEN
1230 ONCE_REWRITE_TAC[SET_RULE` {a,b,c,c} = {a,b,c} `] THEN
1231 NHANH (SET_RULE` ~(a = v0) /\ ~(b = v0) /\ ~(c = v0) ==>
1232 {a,b,b} INTER {v0,v0,v0} = {} /\ {a,b,c} INTER {v0,v0,v0} = {} `) THEN
1233 SIMP_TAC[AFF_LE_LT33; AFF_GE33; AFF_GT33] THEN
1234 REWRITE_TAC[GSYM VECTOR_ADD_RDISTRIB; VECTOR_ARITH` a % x + b % x + y
1235 = ( a + b ) % x + y `] THEN
1236 REWRITE_TAC[REAL_ARITH` (a + b ) + c = a + b + c `] THEN
1237 REPEAT STRIP_TAC THENL [
1238 REWRITE_TAC[FUN_EQ_THM; IN_ELIM_THM] THEN GEN_TAC THEN
1239 EQ_TAC THENL [MESON_TAC[REAL_ARITH ` &0 < a /\ &0 < b ==> &0 < a + b `;
1240 REAL_ARITH ` a + b + c + d = a + ( b + c ) + d `];
1241 MESON_TAC[REAL_ARITH ` a + b + c = a + b / &2 + b / &2 + c / &3 +
1242 c / &3 + c / &3 `; REAL_ARITH` &0 < a <=> &0 < a / &3 `;
1243 REAL_ARITH` a = a / &2 + a / &2 /\ b = b / &3 + b / &3 + b / &3 /\ b =
1244 ( b / &3 + b / &3 ) + b / &3 `]];
1245 REPEAT STRIP_TAC THEN
1246 REWRITE_TAC[FUN_EQ_THM; IN_ELIM_THM] THEN GEN_TAC THEN
1248 MESON_TAC[REAL_ARITH ` ( &0 < a /\ &0 < b ==> &0 < a + b ) /\ ( &0 <= a /\ &0 <= b ==> &0 <= a + b ) `;
1249 REAL_ARITH ` a + b + c + d = a + ( b + c ) + d `] ;
1250 MESON_TAC[REAL_ARITH ` a + b + c = a + b / &2 + b / &2 + c / &3 +
1251 c / &3 + c / &3 `; REAL_ARITH` ( &0 < a <=> &0 < a / &3) /\ ( &0 <= a <=> &0 <= a / &3) `;
1252 REAL_ARITH` a = a / &2 + a / &2 /\ b = b / &3 + b / &3 + b / &3 /\ b = ( b / &3 + b / &3 ) + b / &3 `]];
1253 REPEAT STRIP_TAC THEN
1254 REWRITE_TAC[FUN_EQ_THM; IN_ELIM_THM] THEN GEN_TAC THEN
1255 EQ_TAC THENL [MESON_TAC[REAL_ARITH ` ( &0 < a /\ &0 < b ==> &0 < a + b )
1256 /\ ( &0 <= a /\ &0 <= b ==> &0 <= a + b ) `; REAL_ARITH ` ( a < &0 /\ b < &0
1257 ==> a + b < &0 )`; REAL_ARITH ` a + b + c + d = a + ( b + c ) + d `]; STRIP_TAC] THEN
1258 EXISTS_TAC `ta :real` THEN
1259 EXISTS_TAC `tb :real` THEN
1260 EXISTS_TAC `tc :real` THEN
1261 REPEAT (EXISTS_TAC ` t / &3 `) THEN
1262 ASM_MESON_TAC[REAL_ARITH` a < &0 <=> a / &3 < &0 `;
1263 REAL_ARITH ` a = a / &3 + a / &3 + a / &3 `];
1264 REPEAT STRIP_TAC THEN
1265 REWRITE_TAC[FUN_EQ_THM; IN_ELIM_THM] THEN GEN_TAC THEN
1266 EQ_TAC THENL [MESON_TAC[REAL_ARITH ` ( &0 < a /\ &0 < b ==> &0 < a + b ) /\ ( &0 <= a /\ &0 <= b
1267 ==> &0 <= a + b ) `; REAL_ARITH ` ( a < &0 /\ b < &0 ==> a + b < &0 )`;
1268 REAL_ARITH ` a + b + c + d = a + ( b + c ) + d `]; STRIP_TAC] THEN
1269 EXISTS_TAC `ta :real` THEN
1270 EXISTS_TAC `tb :real` THEN
1271 EXISTS_TAC `tc :real` THEN
1272 REPEAT (EXISTS_TAC ` t / &3 `) THEN
1273 ASM_MESON_TAC[REAL_ARITH ` a = a / &3 + a / &3 + a / &3 `;
1274 REAL_ARITH ` &0 < a <=> &0 < a / &3 `]]);;
1277 let AFF_GES_GTS = prove(` ! a b c (v0:real^N).
1278 ~(a = v0) /\ ~(b = v0) /\ ~(c = v0)
1279 ==> aff_gt {a, b} {v0} =
1283 x = ta % a + tb % b + t % v0} /\
1284 aff_ge {a, b} {v0} =
1288 x = ta % a + tb % b + t % v0} /\
1289 aff_lt {a, b, c} {v0} =
1292 ta + tb + tc + t = &1 /\
1293 x = ta % a + tb % b + tc % c + t % v0} /\
1294 aff_gt {a, b, c} {v0} =
1297 ta + tb + tc + t = &1 /\
1298 x = ta % a + tb % b + tc % c + t % v0} /\
1299 aff_ge {a, b, c} {v0} =
1302 ta + tb + tc + t = &1 /\
1303 x = ta % a + tb % b + tc % c + t % v0} `,
1305 REWRITE_TAC[MESON[]` (a ==> a1 /\ a2 /\ a3 /\ a4 /\ a5) <=>
1306 ( a ==> a1 /\ a2 /\ a3 /\a4 ) /\ ( a ==> a5) `] THEN
1307 REWRITE_TAC[AFF_GES_LTS] THEN
1308 NHANH (SET_RULE` ~(a = v0) /\ ~(b = v0) /\ ~(c = v0)
1309 ==> {a,b,c} INTER {v0,v0,v0} = {} `) THEN
1310 ONCE_REWRITE_TAC[SET_RULE` {v} = {v,v,v} `] THEN
1311 ONCE_REWRITE_TAC[SET_RULE` {a, b, c, c, c} = {a,b,c} `] THEN
1312 SIMP_TAC[AFF_GE33] THEN
1313 REPEAT STRIP_TAC THEN
1314 REWRITE_TAC[FUN_EQ_THM; IN_ELIM_THM; GSYM VECTOR_ADD_RDISTRIB] THEN
1315 GEN_TAC THEN EQ_TAC THENL [
1316 MESON_TAC[REAL_ARITH` &0 <= a /\ &0 <= b ==> &0 <= a + b `];
1318 EXISTS_TAC ` ta :real` THEN
1319 EXISTS_TAC ` tb :real` THEN
1320 EXISTS_TAC ` tc :real` THEN
1321 REPEAT ( EXISTS_TAC ` t / &3 `) THEN
1322 ASM_MESON_TAC[REAL_ARITH` a = a / &3 + a / &3 + a / &3 `;
1323 REAL_ARITH` &0 <= a <=> &0 <= a / &3 `]]);;
1326 let COEF_1_POS_NEG = prove(` ! v1 v2 v3 v4 (v:real^3).
1327 ~ coplanar_alt {v1,v2,v3,v4} ==>
1328 ( COEF4_1 v1 v2 v3 v4 v > &0 <=> v IN aff_gt {v2,v3,v4} {v1} ) /\
1329 ( COEF4_1 v1 v2 v3 v4 v < &0 <=> v IN aff_lt {v2,v3, v4} {v1} ) `,
1330 NHANH (MESON[EQ_IMP_COPLANAR]`~coplanar_alt {v1, v2, v3, v4} ==>
1331 ~ ( v2 = v1 ) /\ ~ ((v3:real^3) = v1 ) /\ ~ (v4 = v1 ) `) THEN
1332 SIMP_TAC[AFF_GES_LTS] THEN NHANH (SPEC_ALL COEFS_4) THEN
1333 REWRITE_TAC[IN_ELIM_THM; REAL_ARITH ` a > b <=> b < a `] THEN
1334 REPEAT GEN_TAC THEN STRIP_TAC THEN
1335 ONCE_REWRITE_TAC[REAL_ARITH ` a + b + c + t = t + a + b + c `] THEN
1336 ONCE_REWRITE_TAC[VECTOR_ARITH ` (a:real^N) + b + c + t = t + a + b + c `] THEN
1340 let ALL_ABOUT_COEF_1 = prove(` ! v1 v2 v3 v4 (v:real^3).
1341 ~ coplanar_alt {v1,v2,v3,v4} ==>
1342 ( COEF4_1 v1 v2 v3 v4 v < &0 <=> v IN aff_lt {v2,v3, v4} {v1} ) /\
1343 ( COEF4_1 v1 v2 v3 v4 v = &0 <=> v IN aff {v2,v3,v4} ) /\
1344 ( COEF4_1 v1 v2 v3 v4 v > &0 <=> v IN aff_gt {v2,v3,v4} {v1} )`,
1345 SIMP_TAC[COEF_1_EQ_ZERO ; COEF_1_POS_NEG ]);;
1347 let PER_COEF1_WITH_COEF2 = prove(`! v1 v2 v3 v4 (v:real^3).
1348 ~coplanar_alt {v1, v2, v3, v4} ==>
1349 COEF4_2 v1 v2 v3 v4 v = COEF4_1 v2 v3 v4 v1 v `,
1350 NHANH (SPEC_ALL COEFS_4) THEN
1351 REPEAT GEN_TAC THEN STRIP_TAC THEN
1352 MP_TAC (SPECL [` v2:real^3 `; `v3:real^3`; `v4:real^3`; ` v1:real^3`;
1353 `v:real^3 `] COEFS_4) THEN
1354 UNDISCH_TAC ` ~coplanar_alt {v1, v2, v3, (v4:real^3)}` THEN
1356 REWRITE_TAC[MESON[SET_RULE` {v1, v2, v3, v4} = {v2, v3, v4, v1}`]`
1357 ~coplanar_alt {v1, v2, v3, v4} /\
1358 (~coplanar_alt {v2, v3, v4, v1} ==> l ) <=> ~coplanar_alt {v1, v2, v3, v4}
1360 ONCE_REWRITE_TAC[GSYM (REAL_ARITH` a + b + c + d = b + c + d + a `)] THEN
1361 ONCE_REWRITE_TAC[GSYM (VECTOR_ARITH` (a:real^N) + b + c + d = b + c + d + a `)] THEN
1364 let PER_COEF1_WITH_COEF3 = prove(`! v1 v2 v3 v4 (v:real^3).
1365 ~coplanar_alt {v1, v2, v3, v4} ==>
1366 COEF4_3 v1 v2 v3 v4 v = COEF4_1 v3 v4 v1 v2 v `,
1367 NHANH (SPEC_ALL COEFS_4) THEN
1368 REPEAT GEN_TAC THEN STRIP_TAC THEN
1369 MP_TAC (SPECL [`v3:real^3`; `v4:real^3`; ` v1:real^3`; ` v2:real^3`;
1370 `v:real^3 `] COEFS_4) THEN
1371 UNDISCH_TAC ` ~coplanar_alt {v1, v2, v3, (v4:real^3)}` THEN
1373 REWRITE_TAC[MESON[SET_RULE` {v1, v2, v3, v4} = {v3, v4, v1, v2}`]`
1374 ~coplanar_alt {v1, v2, v3, v4} /\
1375 (~coplanar_alt {v3, v4, v1, v2} ==> l ) <=> ~coplanar_alt {v1, v2, v3, v4}
1377 ONCE_REWRITE_TAC[GSYM (REAL_ARITH` a + b + c + d = c + d + a + b`)] THEN
1378 ONCE_REWRITE_TAC[GSYM (VECTOR_ARITH` (a:real^N) + b + c + d = c + d + a + b`)]
1379 THEN ASM_MESON_TAC[]);;
1381 let PER_COEF1_WITH_COEF4 = prove(`! v1 v2 v3 v4 (v:real^3).
1382 ~coplanar_alt {v1, v2, v3, v4} ==>
1383 COEF4_4 v1 v2 v3 v4 v = COEF4_1 v4 v1 v2 v3 v `,
1384 NHANH (SPEC_ALL COEFS_4) THEN
1386 ONCE_REWRITE_TAC[SET_RULE` {v1, v2, v3, v4} = {v4,v1, v2, v3}`] THEN
1387 NHANH (SPEC_ALL COEFS_4) THEN
1388 MESON_TAC[REAL_ARITH` ta + tb + tc + td = td + ta + tb + tc`;
1389 VECTOR_ARITH` ta + tb + tc + td = td + ta + tb + (tc:real^N)`]);;
1391 let ALL_ABOUT_COEF_2 = prove(` ! v1 v2 v3 v4 (v:real^3).
1392 ~ coplanar_alt {v1,v2,v3,v4} ==>
1393 ( COEF4_2 v1 v2 v3 v4 v < &0 <=> v IN aff_lt {v1,v3, v4} {v2} ) /\
1394 ( COEF4_2 v1 v2 v3 v4 v = &0 <=> v IN aff {v1,v3,v4} ) /\
1395 ( COEF4_2 v1 v2 v3 v4 v > &0 <=> v IN aff_gt {v1,v3,v4} {v2} )`,
1396 SIMP_TAC[PER_COEF1_WITH_COEF2] THEN MP_TAC ALL_ABOUT_COEF_1 THEN
1397 MESON_TAC[SET_RULE` {v1, v2, v3, v4} = {v2, v3, v4, v1}`;
1398 SET_RULE` {v1, v2, v3} = {v2, v3,v1}`]);;
1403 let ALL_ABOUT_COEF_3 = prove(` ! v1 v2 v3 v4 (v:real^3).
1404 ~ coplanar_alt {v1,v2,v3,v4} ==>
1405 ( COEF4_3 v1 v2 v3 v4 v < &0 <=> v IN aff_lt {v2,v1, v4} {v3} ) /\
1406 ( COEF4_3 v1 v2 v3 v4 v = &0 <=> v IN aff {v2,v1,v4} ) /\
1407 ( COEF4_3 v1 v2 v3 v4 v > &0 <=> v IN aff_gt {v2,v1,v4} {v3} ) `,
1408 SIMP_TAC[PER_COEF1_WITH_COEF3] THEN
1409 ONCE_REWRITE_TAC[SET_RULE` {v2, v1, v4} = {v4,v1,v2} `] THEN
1410 ONCE_REWRITE_TAC[SET_RULE` {v1, v4, v3, v2} = {v3,v4,v1,v2} `] THEN
1411 SIMP_TAC[ALL_ABOUT_COEF_1]);;
1413 let SRGTIHY = prove(` ! v1 v2 v3 v4 (v:real^3).
1414 ~ coplanar_alt {v1,v2,v3,v4} ==>
1415 ( COEF4_1 v1 v2 v3 v4 v < &0 <=> v IN aff_lt {v2,v3, v4} {v1} ) /\
1416 ( COEF4_1 v1 v2 v3 v4 v = &0 <=> v IN aff {v2,v3,v4} ) /\
1417 ( COEF4_1 v1 v2 v3 v4 v > &0 <=> v IN aff_gt {v2,v3,v4} {v1} ) /\
1418 ( COEF4_2 v1 v2 v3 v4 v < &0 <=> v IN aff_lt {v1,v3, v4} {v2} ) /\
1419 ( COEF4_2 v1 v2 v3 v4 v = &0 <=> v IN aff {v1,v3,v4} ) /\
1420 ( COEF4_2 v1 v2 v3 v4 v > &0 <=> v IN aff_gt {v1,v3,v4} {v2} ) /\
1421 ( COEF4_3 v1 v2 v3 v4 v < &0 <=> v IN aff_lt {v2,v1, v4} {v3} ) /\
1422 ( COEF4_3 v1 v2 v3 v4 v = &0 <=> v IN aff {v2,v1,v4} ) /\
1423 ( COEF4_3 v1 v2 v3 v4 v > &0 <=> v IN aff_gt {v2,v1,v4} {v3} )/\
1424 ( COEF4_4 v1 v2 v3 v4 v < &0 <=> v IN aff_lt {v2,v1, v3} {v4} ) /\
1425 ( COEF4_4 v1 v2 v3 v4 v = &0 <=> v IN aff {v2,v1,v3} ) /\
1426 ( COEF4_4 v1 v2 v3 v4 v > &0 <=> v IN aff_gt {v2,v1,v3} {v4} )`,
1427 SIMP_TAC[ALL_ABOUT_COEF_1; ALL_ABOUT_COEF_2; ALL_ABOUT_COEF_3;
1428 PER_COEF1_WITH_COEF4] THEN
1429 ONCE_REWRITE_TAC[SET_RULE` {v2, v1, v3} = {v1,v2,v3}`] THEN
1430 ONCE_REWRITE_TAC[SET_RULE` {v1, v3, v2, v4} = {v4,v1,v2,v3}`] THEN
1431 SIMP_TAC[ALL_ABOUT_COEF_1]);;
1432 let LEMMA77 = SRGTIHY;;
1436 (`conv0 {v1, v2, v3, v4} =
1437 {x:real^N | ?a b c d.
1442 a + b + c + d = &1 /\
1443 a % v1 + b % v2 + c % v3 + d % v4 = x}`,
1444 REWRITE_TAC[FUN_EQ_THM; IN_ELIM_THM] THEN X_GEN_TAC `y:real^N` THEN
1445 REWRITE_TAC[conv0; affsign; sgn_gt; lin_combo; UNION_EMPTY] THEN
1446 MATCH_MP_TAC EQ_TRANS THEN
1448 `?f. (!w:real^N. w IN {v1, v2, v3, v4} ==> &0 < f w) /\
1449 sum {v1, v2, v3, v4} f = &1 /\
1450 vsum {v1, v2, v3, v4} (\v. f v % v) = y` THEN
1451 CONJ_TAC THENL [REWRITE_TAC[IN] THEN MESON_TAC[]; ALL_TAC] THEN
1452 SIMP_TAC[AFFINE_HULL_FINITE_STEP_GEN;
1453 REAL_ARITH `&0 < x /\ &0 < y ==> &0 < x + y`;
1454 REAL_ARITH `&0 < x ==> &0 < x / &2`;
1455 FINITE_INSERT; CONJUNCT1 FINITE_RULES; RIGHT_EXISTS_AND_THM] THEN
1456 ASM_REWRITE_TAC[IN_ELIM_THM;
1457 REAL_ARITH `x - y:real = z <=> x = y + z`;
1458 VECTOR_ARITH `x - y:real^N = z <=> x = y + z`] THEN
1459 REWRITE_TAC[VECTOR_ADD_RID; REAL_ADD_RID] THEN MESON_TAC[]);;
1461 (* ======================= *)
1463 (* ======================= *)
1465 let ARIKWRQ = prove(`! v1 v2 v3 (v4:real^3).
1466 let s = {v1,v2,v3,v4} in
1467 CARD s = 4 /\ ~ coplanar_alt s ==>
1468 conv s = aff_ge ( s DIFF {v1} ) {v1} INTER
1469 aff_ge ( s DIFF {v2} ) {v2} INTER
1470 aff_ge ( s DIFF {v3} ) {v3} INTER
1471 aff_ge ( s DIFF {v4} ) {v4} `, LET_TR THEN
1472 SIMP_TAC[CARD4; SET_RULE ` ~(v1 IN {v2, v3, v4}) /\ ~(v2 = v3 \/ v3 = v4 \/ v4 = v2)
1473 ==> {v1, v2, v3, v4} DIFF {v1} = {v2,v3,v4} /\
1474 {v1, v2, v3, v4} DIFF {v2} = {v3,v4,v1} /\
1475 {v1, v2, v3, v4} DIFF {v3} = {v4,v1,v2} /\
1476 {v1, v2, v3, v4} DIFF {v4} = {v1,v2,v3} `] THEN
1477 REWRITE_TAC[CARD4; IN_SET3;DE_MORGAN_THM] THEN
1478 SIMP_TAC[AFF_GES_GTS] THEN
1479 REWRITE_TAC[CONVEX_HULL_4_EQUIV] THEN
1480 REPEAT STRIP_TAC THEN
1481 REWRITE_TAC[SET_RULE ` a = b <=> (! x. x IN a <=> x IN b ) `;
1482 IN_INTER; IN_ELIM_THM] THEN
1483 GEN_TAC THEN EQ_TAC THENL [
1484 ASM_MESON_TAC[REAL_ARITH` a + b + c + d = d + a + b + c `;
1485 VECTOR_ARITH` (a:real^N) + b + c + d = d + a + b + c `];
1486 FIRST_X_ASSUM MP_TAC ] THEN
1487 NHANH (SPEC ` x: real^3` (GEN ` v:real^3` (SPEC_ALL COEFS_4))) THEN
1488 ABBREV_TAC ` aa = COEF4_1 v1 v2 v3 v4 x ` THEN
1489 ABBREV_TAC ` bb = COEF4_2 v1 v2 v3 v4 x ` THEN
1490 ABBREV_TAC ` cc = COEF4_3 v1 v2 v3 v4 x ` THEN
1491 ABBREV_TAC ` dd = COEF4_4 v1 v2 v3 v4 x ` THEN
1492 REWRITE_TAC[MESON[]` a ==> b ==> c <=> a /\ b ==> c `] THEN PHA THEN
1493 NHANH (MESON[REAL_ARITH` a + b + c + d = d + a + b + c `;
1494 VECTOR_ARITH` (a:real^N) + b + c + d = d + a + b + c `]`
1495 aa + bb + cc + dd = &1 /\
1496 x = aa % v1 + bb % v2 + cc % v3 + dd % v4 /\
1498 x = ta % v1 + tb % v2 + tc % v3 + td % v4 /\ ta + tb + tc + td = &1
1499 ==> ta = aa /\ tb = bb /\ tc = cc /\ td = dd) /\
1502 ta + tb + tc + t = &1 /\
1503 x = ta % v2 + tb % v3 + tc % v4 + t % v1) /\
1506 ta + tb + tc + t = &1 /\
1507 x = ta % v3 + tb % v4 + tc % v1 + t % v2) /\
1510 ta + tb + tc + t = &1 /\
1511 x = ta % v4 + tb % v1 + tc % v2 + t % v3) /\
1514 ta + tb + tc + t = &1 /\
1515 x = ta % v1 + tb % v2 + tc % v3 + t % v4)
1516 ==> &0 <= aa /\ &0 <= bb /\ &0 <= cc /\ &0 <= dd`) THEN
1517 MATCH_MP_TAC (MESON[]` ( a1 /\ a2 /\ a3 ==> l) ==>
1518 aa /\ ( a1 /\ a2 /\ a4 ) /\ a3 ==> l `) THEN MESON_TAC[]);;
1524 (* ================ *)
1526 (* ================= *)
1531 let MXHKOXR = prove(`! v1 v2 v3 (v4:real^3). let s = {v1,v2,v3,v4} in
1532 CARD s = 4 /\ ~ coplanar_alt s ==>
1533 conv0 s = aff_gt ( s DIFF {v1} ) {v1} INTER
1534 aff_gt ( s DIFF {v2} ) {v2} INTER
1535 aff_gt ( s DIFF {v3} ) {v3} INTER
1536 aff_gt ( s DIFF {v4} ) {v4} `, LET_TR THEN
1537 SIMP_TAC[CARD4; SET_RULE ` ~(v1 IN {v2, v3, v4}) /\ ~(v2 = v3 \/ v3 = v4 \/ v4 = v2)
1538 ==> {v1, v2, v3, v4} DIFF {v1} = {v2,v3,v4} /\
1539 {v1, v2, v3, v4} DIFF {v2} = {v3,v4,v1} /\
1540 {v1, v2, v3, v4} DIFF {v3} = {v4,v1,v2} /\
1541 {v1, v2, v3, v4} DIFF {v4} = {v1,v2,v3} `] THEN
1542 REWRITE_TAC[CARD4; IN_SET3;DE_MORGAN_THM] THEN
1543 SIMP_TAC[AFF_GES_GTS; CONV0_4 ] THEN
1544 REPEAT STRIP_TAC THEN
1545 REWRITE_TAC[SET_RULE ` a = b <=> (! x. x IN a <=> x IN b ) `;
1546 IN_INTER; IN_ELIM_THM] THEN
1547 GEN_TAC THEN EQ_TAC THENL [
1548 ASM_MESON_TAC[REAL_ARITH` a + b + c + d = d + a + b + c `;
1549 VECTOR_ARITH` (a:real^N) + b + c + d = d + a + b + c `];
1550 FIRST_X_ASSUM MP_TAC ] THEN
1551 NHANH (SPEC ` x: real^3` (GEN ` v:real^3` (SPEC_ALL COEFS_4))) THEN
1552 ABBREV_TAC ` aa = COEF4_1 v1 v2 v3 v4 x ` THEN
1553 ABBREV_TAC ` bb = COEF4_2 v1 v2 v3 v4 x ` THEN
1554 ABBREV_TAC ` cc = COEF4_3 v1 v2 v3 v4 x ` THEN
1555 ABBREV_TAC ` dd = COEF4_4 v1 v2 v3 v4 x ` THEN
1556 REWRITE_TAC[MESON[]` a ==> b ==> c <=> a /\ b ==> c `] THEN PHA THEN
1557 NHANH (MESON[REAL_ARITH` a + b + c + d = d + a + b + c `;
1558 VECTOR_ARITH` (a:real^N) + b + c + d = d + a + b + c `]`
1559 aa + bb + cc + dd = &1 /\
1560 x = aa % v1 + bb % v2 + cc % v3 + dd % v4 /\
1562 x = ta % v1 + tb % v2 + tc % v3 + td % v4 /\ ta + tb + tc + td = &1
1563 ==> ta = aa /\ tb = bb /\ tc = cc /\ td = dd) /\
1566 ta + tb + tc + t = &1 /\
1567 x = ta % v2 + tb % v3 + tc % v4 + t % v1) /\
1570 ta + tb + tc + t = &1 /\
1571 x = ta % v3 + tb % v4 + tc % v1 + t % v2) /\
1574 ta + tb + tc + t = &1 /\
1575 x = ta % v4 + tb % v1 + tc % v2 + t % v3) /\
1578 ta + tb + tc + t = &1 /\
1579 x = ta % v1 + tb % v2 + tc % v3 + t % v4)
1580 ==> &0 < aa /\ &0 < bb /\ &0 < cc /\ &0 < dd `) THEN
1581 MATCH_MP_TAC (MESON[]` ( a1 /\ a2 /\ a3 ==> l) ==>
1582 aa /\ ( a1 /\ a2 /\ a4 ) /\ a3 ==> l `) THEN MESON_TAC[]);;
1586 (`conv0 {v1, v2, v3, v4} =
1587 {x:real^N | ?a b c d.
1592 a + b + c + d = &1 /\
1593 a % v1 + b % v2 + c % v3 + d % v4 = x}`,
1594 REWRITE_TAC[FUN_EQ_THM; IN_ELIM_THM] THEN X_GEN_TAC `y:real^N` THEN
1595 REWRITE_TAC[conv0; affsign; sgn_gt; lin_combo; UNION_EMPTY] THEN
1596 MATCH_MP_TAC EQ_TRANS THEN
1598 `?f. (!w:real^N. w IN {v1, v2, v3, v4} ==> &0 < f w) /\
1599 sum {v1, v2, v3, v4} f = &1 /\
1600 vsum {v1, v2, v3, v4} (\v. f v % v) = y` THEN
1601 CONJ_TAC THENL [REWRITE_TAC[IN] THEN MESON_TAC[]; ALL_TAC] THEN
1602 SIMP_TAC[AFFINE_HULL_FINITE_STEP_GEN;
1603 REAL_ARITH `&0 < x /\ &0 < y ==> &0 < x + y`;
1604 REAL_ARITH `&0 < x ==> &0 < x / &2`;
1605 FINITE_INSERT; CONJUNCT1 FINITE_RULES; RIGHT_EXISTS_AND_THM] THEN
1606 ASM_REWRITE_TAC[IN_ELIM_THM;
1607 REAL_ARITH `x - y:real = z <=> x = y + z`;
1608 VECTOR_ARITH `x - y:real^N = z <=> x = y + z`] THEN
1609 REWRITE_TAC[VECTOR_ADD_RID; REAL_ADD_RID] THEN MESON_TAC[]);;
1612 let CONV0_4POINTS = CONV0_4;;
1616 (* ================== *)
1619 (* ================== *)
1622 let ZRFMKPY = prove(` ! v1 v2 v3 v4 (v:real^3).
1623 ~coplanar_alt {v1, v2, v3, v4}
1624 ==> (v IN conv {v1, v2, v3, v4} <=>
1625 &0 <= COEF4_1 v1 v2 v3 v4 v /\
1626 &0 <= COEF4_2 v1 v2 v3 v4 v /\
1627 &0 <= COEF4_3 v1 v2 v3 v4 v /\
1628 &0 <= COEF4_4 v1 v2 v3 v4 v) /\
1629 (v IN conv0 {v1, v2, v3, v4} <=>
1630 &0 < COEF4_1 v1 v2 v3 v4 v /\
1631 &0 < COEF4_2 v1 v2 v3 v4 v /\
1632 &0 < COEF4_3 v1 v2 v3 v4 v /\
1633 &0 < COEF4_4 v1 v2 v3 v4 v) `,
1634 NHANH (SPEC_ALL COEFS_4) THEN REWRITE_TAC[CONVEX_HULL_4_EQUIV;
1635 CONV0_4POINTS; IN_ELIM_THM] THEN MESON_TAC[]);;
1637 let LEMMA78 = ZRFMKPY;;
1643 (* NGUYEN QUANG TRUONG *)
1644 let IMP_TAC = IMP_IMP_TAC;;
1648 let QUAANG_TRUOONN = prove(` ! v0 v1 v2 v3 (v4:real^N).
1649 CARD {v0, v1, v2, v3, v4} = 5 /\
1650 (?x. ~(x = v0) /\ x IN cone v0 {v1, v3} INTER cone v0 {v2, v4})
1651 ==> ~(conv {v1, v3} INTER cone v0 {v2, v4} = {})`,
1652 REWRITE_TAC[CONV_SET2; cone; CARD5; SET_RULE ` a INTER b = {} <=>
1653 ~ (? x. a x /\ b x ) `; GSYM aff_ge_def; IN; IN_INTER] THEN
1654 NHANH (SET_RULE ` ~{v1, v2, v3, v4} v0 ==>
1655 ~ ( v0 = v1 \/ v0 = v3 ) /\ ~ ( v0 = v2 \/ v0 = v4 ) `) THEN
1656 ONCE_REWRITE_TAC[MESON[]` a /\ b ==> c <=> a ==> b ==> c `] THEN
1657 SIMP_TAC[AFF_GE_12] THEN REWRITE_TAC[DE_MORGAN_THM] THEN
1658 REWRITE_TAC[IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN
1659 UNDISCH_TAC ` (x:real^N) = tv % v0 + ta % v1 + tb % v3` THEN
1660 UNDISCH_TAC ` (x:real^N) = tv' % v0 + ta' % v2 + tb' % v4` THEN
1661 REWRITE_TAC[MESON[]` x = a
1662 ==> x = (b:real^N) ==> c <=> x = a /\ a = b ==> c `] THEN
1663 REWRITE_TAC[VECTOR_ARITH` a % v + d = b % v + e <=>
1664 ( a - b ) % v + d = e `] THEN
1665 ASM_CASES_TAC ` &0 < ta + tb ` THENL [DOWN_TAC THEN
1666 REWRITE_TAC[MESON[VECTOR_MUL_LCANCEL; REAL_FIELD ` &0 < a ==> ~ ( &1 / a = &0 )`]`
1667 &0 < ta + tb /\ aaa /\
1668 aa = ta % v1 + tb % v3 <=> &0 < ta + tb /\ aaa /\
1669 &1 / ( ta + tb ) % aa = &1 / ( ta + tb ) % ( ta % v1 + tb % v3) `] THEN
1670 REWRITE_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC; REAL_ARITH `
1671 &1 / a * b = b / a `] THEN STRIP_TAC THEN DOWN_TAC THEN
1672 NHANH (MESON[REAL_LE_RDIV_0]`&0 <= ta /\ &0 <= tb /\ a1 /\ &0 <= ta' /\
1674 &0 < ta + tb /\ a3 ==> &0 <= ta / (ta + tb) /\ &0 <= tb / (ta + tb) /\
1675 &0 <= ta' / (ta + tb) /\ &0 <= tb' / (ta + tb) `) THEN ASM_MESON_TAC[
1676 REAL_FIELD` tv + ta + tb = &1 /\ tv' + ta' + tb' = &1 /\
1677 &0 < ta + tb ==> (tv' - tv) / (ta + tb) + ta' / (ta + tb) +
1678 tb' / (ta + tb) = &1 /\ ta / ( ta + tb ) + tb / ( ta + tb ) = &1`];
1680 NHANH (MESON[REAL_ARITH` &0 <= a /\ &0 <= b /\ ~( &0 < a + b )
1681 ==> a = &0 /\ b = &0 `]`&0 <= ta /\ &0 <= tb /\a1/\a2 /\a3/\a4 /\
1682 ~(&0 < ta + tb) /\ a5 ==> ta = &0 /\ tb = &0`) THEN
1683 PURE_ONCE_REWRITE_TAC[MESON[]` P ta tb /\ ta = &0 /\ tb = &0
1684 <=> P ( &0 ) ( &0 ) /\ ta = &0 /\ tb = &0 `] THEN
1685 REWRITE_TAC[ZERO_NEUTRAL; VECTOR_MUL_LZERO; VECTOR_ADD_LID] THEN
1686 REWRITE_TAC[VECTOR_ARITH` (tv' - tv) % v + a = vec 0 <=> tv' % v + a
1687 = tv % v `; MESON[]` a = b /\ b = c <=> a = c /\ b = c `] THEN
1688 MESON_TAC[VECTOR_ARITH ` &1 % v = v `]]);;
1691 (* ================ *)
1693 let JVDAFRS = prove(` ! v0 v1 v2 v3 (v4:real^N).
1694 CARD {v0, v1, v2, v3, v4} = 5 /\
1695 (?x. ~(x = v0) /\ x IN cone v0 {v1, v3} INTER cone v0 {v2, v4})
1696 ==> ~(conv {v1, v3} INTER cone v0 {v2, v4} = {} /\
1697 conv {v2, v4} INTER cone v0 {v1, v3} = {})`, MESON_TAC[QUAANG_TRUOONN]);;
1700 (* =========================== *)
1702 let SQRT8_POS = MESON[REAL_ARITH ` &0 < &8 `; SQRT_POS_LT]` &0 < sqrt (&8) `;;
1704 let SQRT8_LT_4_45 = prove(` sqrt8 < #4.45 `,
1705 SIMP_TAC[sqrt8; REAL_ARITH ` &0 < #4.45 `; MESON[REAL_ARITH ` &0 < &8 `;
1706 SQRT_POS_LT]` &0 < sqrt (&8) `; LT_POW2_EQ_LT; SQRT8_POW2] THEN REAL_ARITH_TAC);;
1709 let PROVE_NOT_COLLINEAR = prove(` ! v0 v1 (v2:real^3).
1710 &2 <= dist3 v0 v1 /\
1711 dist3 v0 v1 <= #2.51 /\
1712 #2.45 <= dist3 v1 v2 /\
1713 dist3 v1 v2 <= #2.51 /\
1714 #2.77 <= dist3 v0 v2 /\
1715 dist3 v0 v2 <= sqrt8
1716 ==> ~ collinear {v0, v1, v2}`,
1717 REWRITE_TAC[COLLINEAR_AS_IN_CONV2; MID_COND; dist3; LENGTH_EQ_EX; DE_MORGAN_THM] THEN
1718 SIMP_TAC[DIST_SYM] THEN
1720 ABBREV_TAC ` a = dist(v0,v1:real^3)` THEN
1721 ABBREV_TAC ` b = dist(v0,v2:real^3)` THEN
1722 ABBREV_TAC ` c = dist(v1,v2:real^3)` THEN
1723 MP_TAC SQRT8_LT_4_45 THEN
1726 let BPOW8APOW2CPOW2 = prove(`&2 <= a /\
1732 ==> b pow 2 <= &8 /\ a pow 2 <= #2.51 pow 2 /\ c pow 2 <= #2.51 pow 2 `,
1733 REWRITE_TAC[MESON[]` a1 /\ a2 /\a3 /\a4 /\a5 /\a6 ==> l <=>
1734 a1 /\a3 /\a5 ==> a2 /\a4 /\a6 ==> l `] THEN
1735 NHANH (REAL_ARITH`&2 <= a /\ #2.45 <= c /\ #2.77 <= b ==>
1736 &0 < a /\ &0 < b /\ &0 < c /\ &0 < #2.51 `) THEN
1737 SIMP_TAC[sqrt8; POW2_COND_LT; SQRT8_POS; SQRT8_POW2]);;
1739 let IMP_PRE_LE_19 = prove(`&2 <= a /\
1751 a pow 2 <= #2.77 pow 2 + #2.45 pow 2 /\
1752 b pow 2 <= &2 pow 2 + #2.45 pow 2 /\
1753 c pow 2 <= &2 pow 2 + #2.77 pow 2 `,
1754 CONV_TAC REAL_RAT_REDUCE_CONV THEN NHANH (BPOW8APOW2CPOW2 ) THEN REAL_ARITH_TAC);;
1756 (* ==================== *)
1758 let LT_SQ8_IMP_LT2 = prove_by_refinement(
1759 ` a < sqrt (&8) ==> ~ ( &2 <= &1 / &2 * a ) `,
1762 (ASM_CASES_TAC ` &0 <= a `);
1763 (UNDISCH_TAC `&0 <= a `);
1764 (SIMP_TAC[REAL_LT_IMP_LE; SQRT8_POS; LT_POW2_COND; REAL_ARITH ` &2 <= &1 / &2 * a <=> &4 <= a `; REAL_ARITH` &0 <= &4 `; POW2_COND; SQRT8_POW2]);
1765 BY((REAL_ARITH_TAC));
1766 (FIRST_X_ASSUM MP_TAC);
1767 BY((REAL_ARITH_TAC))
1772 let condC = new_definition ` condC M13 m12 m14 M24 m34 (m23:real) =
1773 ((! x. x IN {M13, m12, m14, M24, m34, m23 } ==> &0 <= x ) /\
1778 &0 <= delta (M13 pow 2) (m12 pow 2) (m14 pow 2) (M24 pow 2) (m34 pow 2 )
1781 let LE_FOR_LEMMA36 = prove(`(CARD {u, v, w} = 3 /\ packing {u, v, w} /\ dist (u,v) < sqrt8) /\
1782 ~(dist (u,v) / &2 < dist (w,&1 / &2 % (u + v))) ==>
1783 condC (sqrt (&8)) (&2) (&2) (sqrt (&8)) (&2) (&2) /\
1784 CARD {u, w, v, u + v - w} = 4 /\
1787 &2 <= dist3 v (u + v - w) /\
1788 &2 <= dist3 u (u + v - w) /\
1789 dist3 u v < sqrt (&8) /\
1790 dist3 w (u + v - w) <= sqrt (&8) `,
1791 REWRITE_TAC[condC; delta; SQRT8_POW2] THEN
1792 REWRITE_TAC[SET_RULE ` (! x. x IN ( a INSERT b ) ==> p x ) <=>
1793 p a /\ (! x. x IN b ==> p x ) `; NOT_IN_EMPTY] THEN
1794 CONV_TAC REAL_RAT_REDUCE_CONV THEN
1795 SIMP_TAC[SQRT8_POS; REAL_LT_IMP_LE; dist3; sqrt8; packing] THEN
1796 SIMP_TAC[REAL_LT_IMP_LE; SQRT8_POS; LT_POW2_COND;
1797 REAL_ARITH ` &0 <= &4 `; POW2_COND; SQRT8_POW2] THEN
1798 CONV_TAC REAL_RAT_REDUCE_CONV THEN
1799 REWRITE_TAC[NORM_ARITH` dist (v,u + v - w) = dist (u,w) /\
1800 dist (u,u + v - w) = dist (v,w) /\
1801 dist (w,u + v - w) = &2 * dist (w,&1 / &2 % (u + v)) `] THEN
1802 STRIP_TAC THEN CONJ_TAC THENL [
1803 UNDISCH_TAC `CARD {(u:real^3), v, w} = 3` THEN
1804 REWRITE_TAC[CARD3; CARD4; IN_SET3] THEN
1805 REWRITE_TAC[DE_MORGAN_THM] THEN DAO THEN
1806 STRIP_TAC THEN CONJ_TAC THENL [
1807 NHANH (NORM_ARITH`u + v - w = w ==> dist (w,u) = &1 / &2 * dist (u,v) `) THEN
1808 UNDISCH_TAC `dist ((u:real^3),v) < sqrt (&8)` THEN
1809 NHANH (LT_SQ8_IMP_LT2 ) THEN DOWN_TAC THEN SET_TAC[];
1810 REWRITE_TAC[VECTOR_ARITH ` ((v:real^N) = u + v - w <=> u = w )`;
1811 VECTOR_ARITH ` ((u:real^N) = u + v - w <=> v = w ) `] THEN ASM_MESON_TAC[]];
1812 DAO THEN CONJ_TAC THENL [REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN
1813 REAL_ARITH_TAC;DOWN_TAC THEN REWRITE_TAC[CARD3] THEN SET_TAC[]]]);;
1817 let MIDDLE_POINT_IN_CONV2 = prove(` &1 / &2 % ( u + v ) IN conv {u,v} `,
1818 REWRITE_TAC[CONV_SET2; IN_ELIM_THM; VECTOR_ADD_LDISTRIB] THEN
1819 MESON_TAC[REAL_ARITH ` &0 <= &1 / &2 `; REAL_ARITH` &1 / &2 + &1 / &2 = &1 `]);;
1821 let INTER_DISJONT_EX =
1822 SET_RULE ` ( a INTER b = {} ) <=> (! x. ~ (x IN a /\ x IN b )) `;;
1827 (* ================== *)
1829 MATCH_MP (SPEC_ALL AFFINE_HULL_FINITE) (MESON[FINITE_RULES] ` FINITE {(a:real^N),b,c} `) ;;
1833 let PLANE_IMP_AFFINE = prove(`plane (p:real^N -> bool ) ==> affine p `,
1834 MESON_TAC[plane; AFFINE_AFFINE_HULL]);;
1838 let PLANE_IMP_AFFINE = prove(` plane (p:real^N -> bool ) ==> affine p `,
1839 REWRITE_TAC[plane; AFFINE_HULL_3; affine; FUN_EQ_THM; IN_ELIM_THM] THEN
1840 STRIP_TAC THEN ASM_SIMP_TAC[IN] THEN REPEAT STRIP_TAC THEN ASM_SIMP_TAC[] THEN
1841 SIMP_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC] THEN
1842 REWRITE_TAC[VECTOR_ARITH` (( a:real^N) + b + c ) + a' + b' + c'
1843 = ( a + a' ) + ( b + b') + c + c' `] THEN EXISTS_TAC ` u' * u'' + v' * u''' ` THEN
1844 EXISTS_TAC ` (u' * v'' + v' * v''')` THEN EXISTS_TAC ` (u' * w' + v' * w'')` THEN
1845 ASM_SIMP_TAC[prove(` u' + v' = &1 /\
1846 u''' + v''' + w'' = &1 /\
1847 u'' + v'' + w' = &1 ==>
1848 (u' * u'' + v' * u''') + (u' * v'' + v' * v''') + u' * w' + v' * w'' = &1 `,
1849 SIMP_TAC[REAL_ARITH` a + b = &1 <=> a = &1 - b `] THEN REAL_ARITH_TAC);
1850 GSYM VECTOR_ADD_RDISTRIB]);;
1855 let IMP_AFFINE_HULL_SUBSET = prove(` FINITE a /\ a SUBSET s /\
1856 ~( a = {} )/\ affine s ==> ( affine hull a ) SUBSET s `,
1857 SIMP_TAC[AFFINE_HULL_FINITE; SUBSET; IN_ELIM_THM] THEN
1858 REWRITE_TAC[ GSYM SUBSET] THEN MESON_TAC[AFFINE]);;
1862 let SET_EQ_EX = SET_RULE `a = b <=> (! x. x IN a <=> x IN b ) `;;
1864 let SET_EQ_TO_SUBSET = SET_RULE ` a = b <=> a SUBSET b /\ b SUBSET a `;;
1869 let OTHORGONAL_QUATER_FOR = prove(` delta x12 ( x12 + x23 ) ( x12 + x24 ) x23 x24 x34 =
1870 x12 * ups_x x23 x24 x34 `, REWRITE_TAC[delta; ups_x] THEN REAL_ARITH_TAC);;
1873 let ORTHOGONAL_CROSS_PRODUCT = prove(` u dot ( u cross v ) = &0 /\
1874 v dot ( u cross v ) = &0 `,
1875 REWRITE_TAC[cross; triple_of_real3; real3_of_triple; mk_vec3] THEN
1876 LET_TR THEN REWRITE_TAC[DOT_3; VECTOR_3] THEN REAL_ARITH_TAC);;
1878 let PITHAGOR_CROSS = prove(` dist (a + (b - a) cross (c - a),b) pow 2 =
1879 dist (b,a) pow 2 + norm ( (b - a) cross (c - a) ) pow 2 `,
1880 REWRITE_TAC[vector_norm; dist] THEN
1881 SIMP_TAC[DOT_POS_LE; SQRT_WORKS] THEN
1882 REWRITE_TAC[VECTOR_ARITH` ((a:real^N) + b) - c = b - (c - a ) `] THEN
1883 ABBREV_TAC ` ab = ( b - (a:real^3)) ` THEN
1884 ABBREV_TAC ` ac = ( c - (a:real^3)) ` THEN
1885 REWRITE_TAC[DOT_LSUB; DOT_RSUB] THEN
1886 SIMP_TAC[ORTHOGONAL_CROSS_PRODUCT; DOT_SYM] THEN
1889 let PITHAGOR_NORM = prove(` a dot b = &0 ==> dist (a,b) pow 2 = norm a pow 2 +
1891 SIMP_TAC[dist; vector_norm; DOT_POS_LE; SQRT_WORKS] THEN
1892 SIMP_TAC[DOT_LSUB; DOT_RSUB; DOT_SYM] THEN REAL_ARITH_TAC);;
1894 let VEC3_EQ_EX= prove(`! a (b:real^3). a = b <=> a$1 = b$1 /\ a$2 = b$2 /\ a$3 = b$3 `,
1895 SIMP_TAC[CART_EQ; DIMINDEX_3] THEN
1896 REWRITE_TAC[ARITH_RULE`1 <= i /\ i <= 3 <=>
1897 i = 1 \/ i = 2 \/ i = 3 `] THEN MESON_TAC[]);;
1899 let CROSS_CONVERT = prove_by_refinement(
1900 ` (b - a) cross (c - d) = (a - b) cross (d - c )`,
1903 (REWRITE_TAC[cross; triple_of_real3; real3_of_triple; mk_vec3]);
1905 (REWRITE_TAC[lemma_cm3 ]);
1906 (REWRITE_TAC[VEC3_EQ_EX]);
1907 (REWRITE_TAC[VEC3_EQ_EX; VECTOR_3]);
1908 BY((REAL_ARITH_TAC))
1913 let lemma1 = MESON[prove(` dist(b,c) pow 2 = (a - c - (a - b)) dot (a - c - (a - b)) `,
1914 SIMP_TAC[dist; vector_norm; DOT_POS_LE; SQRT_WORKS] THEN
1915 MESON_TAC[VECTOR_ARITH
1916 ` b - (c:real^N) = (a - c) - ( a - b) `])]`
1917 ups_x aa bb (dist (b,c) pow 2 ) =
1918 ups_x aa bb (( a - c - (a - b)) dot (a - c - (a - b))) `;;
1920 let NORM_CROSS_PRODUCT_UPS_X = prove_by_refinement(
1921 `&4 * norm ( (b - a) cross (c - a)) pow 2 =
1922 ups_x (dist (a,b) pow 2) (dist (a,c) pow 2) (dist (b,c) pow 2)`,
1925 (REWRITE_TAC[lemma1 ]);
1926 (ONCE_REWRITE_TAC[CROSS_CONVERT]);
1927 (SIMP_TAC[ups_x;DIST_SYM; dist; vector_norm; DOT_POS_LE; SQRT_WORKS]);
1928 (REWRITE_TAC[cross; triple_of_real3; real3_of_triple; mk_vec3]);
1930 (REWRITE_TAC[DOT_3; VECTOR_3]);
1931 (ABBREV_TAC ` ab = a - (b:real^3) `);
1932 (ABBREV_TAC ` cc = a - (c:real^3) `);
1933 BY((REWRITE_TAC[lemma_cm3 ] THEN REAL_ARITH_TAC))
1938 ` dist ( a cross b, a ) pow 2 = norm ( a cross b) pow 2 +
1939 norm a pow 2 /\dist ( a cross b, b ) pow 2 = norm ( a cross b) pow 2 +
1941 SIMP_TAC[DOT_SYM;ORTHOGONAL_CROSS_PRODUCT ; PITHAGOR_NORM; DIST_SYM]
1944 let NOT_COLLINEAR_IMP_CROSS_NOT_COPLANAR = prove_by_refinement(
1945 ` ! u v (w:real^3). ~ collinear {a,b,c} ==> ~ coplanar_alt {
1946 a + (b - a ) cross ( c - a ),a,b,c} `,
1953 (REWRITE_TAC[NORM_ARITH` dist (a + b ,a) = norm (b ) `]);
1954 (REWRITE_TAC[NORM_ARITH`dist (a + c,b) = dist ( c, b - a ) `]);
1956 (REWRITE_TAC[GSYM dist]);
1957 (SIMP_TAC[DIST_SYM; OTHORGONAL_QUATER_FOR]);
1958 (ONCE_REWRITE_TAC[REAL_ARITH` a * b = &0 <=> ( &4 * a ) * b = &0 `]);
1959 (SIMP_TAC[NORM_CROSS_PRODUCT_UPS_X]);
1960 (REWRITE_TAC[REAL_ENTIRE]);
1961 BY((MESON_TAC[FHFMKIY]))
1965 let ORTHOGONAL_IMP_PITHAGOR = prove(` (x:real^N) dot ((a:real^N) - b) = &0 ==>
1966 dist (a + x,b) pow 2 = norm x pow 2 + dist (a,b) pow 2`,
1967 SIMP_TAC[dist; vector_norm; DOT_POS_LE; SQRT_WORKS] THEN
1968 REWRITE_TAC[VECTOR_ARITH` (a + c) - b = c + a - (b:real^N)`] THEN
1969 ABBREV_TAC ` aa = ( a - (b:real^N)) ` THEN
1970 SIMP_TAC[DOT_LADD; DOT_RADD; DOT_SYM; ZERO_NEUTRAL]);;
1972 let NOT_COL_AND_ORTHO_IMP_NOT_COPL = prove(`! a b c (x:real^3).
1973 ~collinear {a, b, c} /\ x dot (a - b) = &0 /\
1974 x dot (a - c) = &0 /\ ~(x = vec 0)
1975 ==> ~coplanar_alt {a + x, a, b, c}`,
1976 MP_TAC POLFLZY THEN LET_TR THEN SIMP_TAC[] THEN
1977 SIMP_TAC[ORTHOGONAL_IMP_PITHAGOR ] THEN
1978 SIMP_TAC[ORTHOGONAL_IMP_PITHAGOR; NORM_ARITH ` dist (a + x,a) = norm x `] THEN
1979 SIMP_TAC[ORTHOGONAL_IMP_PITHAGOR; NORM_ARITH ` dist (a + x,a) = norm x `;
1980 OTHORGONAL_QUATER_FOR] THEN SIMP_TAC[COL_EQ_UPS_0] THEN
1981 SIMP_TAC[COL_EQ_UPS_0; GSYM NORM_POS_LT; REAL_ENTIRE; MESON[RELATE_POW2]`
1982 a pow 2 = &0 <=> a = &0 `; REAL_ARITH ` &0 < a ==> ~( a = &0 ) `]);;
1984 let PLANE_NORM_IMP_AFFINE = prove(`! p. plane_norm p ==> affine p `,
1985 REWRITE_TAC[plane_norm; affine] THEN GEN_TAC THEN STRIP_TAC THEN
1986 ASM_SIMP_TAC[IN_ELIM_THM; MESON[]` a = &1 <=> &1 = a `] THEN
1987 ONCE_REWRITE_TAC[ VECTOR_ARITH ` ( a + b ) - c = ( a + b ) - &1 % c `] THEN
1988 ASM_SIMP_TAC[ VECTOR_ARITH` (u % x + v % y) - (u + v) % v0 =
1989 u % ( x - v0 ) + v % ( y - v0 ) `; DOT_RADD; DOT_RMUL; ZERO_NEUTRAL]);;
1991 let IN_PLANE_IMP_OTHORGONAL = prove(`
1992 n dot (x - v0) = &0 /\ n dot (y - v0) = &0 /\ n dot (z - v0) = &0 ==>
1993 n dot ( x - y ) = &0 /\ n dot ( x - z ) = &0 `,
1994 SIMP_TAC[DOT_RSUB] THEN REAL_ARITH_TAC);;
1996 let IMP_A1_EQ_0 = prove_by_refinement(
1997 `(n:real^N) dot (x - v0) = &0 /\
1998 n dot (y - v0) = &0 /\
1999 n dot (z - v0) = &0 /\
2001 x' = a1 % (x + n) + a2 % x + a3 % y + a4 % z /\
2002 a1 + a2 + a3 + a4 = &1 /\
2003 n dot (x' - v0) = &0
2008 (UNDISCH_TAC ` (n:real^N) dot (x' - v0) = &0`);
2009 (ASM_SIMP_TAC[VECTOR_ARITH`(a1 % x + y ) - v0 = a1 % ( x - v0 ) + y - v0 + a1 % v0 `]);
2010 (ONCE_REWRITE_TAC[ VECTOR_ARITH` a % x - y = a % ( x - y ) + a % y - y `]);
2011 (ASM_SIMP_TAC[DOT_RADD; VECTOR_ARITH` ( a + b ) - (c:real^N) = b + a - c `; DOT_RMUL; ZERO_NEUTRAL]);
2012 (ASM_SIMP_TAC[DOT_RADD; VECTOR_ARITH` ( a + b ) - (c:real^N) = b + a - c `; DOT_RMUL; ZERO_NEUTRAL; DOT_RSUB;REAL_ARITH` ((a4 * (n dot v0) - n dot v0 + a3 * (n dot v0)) + a2 * (n dot v0)) + a1 * (n dot v0) = ( a1 + a2 + a3 + a4 ) * ( n dot v0 ) - n dot v0 `; REAL_ARITH ` &1 * a - a = &0 `]);
2013 BY((ASM_MESON_TAC[REAL_ENTIRE; GSYM DOT_EQ_0]))
2017 let LEMMA7 = prove(` !x y z (p:real^3 -> bool).
2018 plane_norm p /\ ~collinear {x, y, z} /\ {x, y, z} SUBSET p
2019 ==> p = aff {x, y, z}`,
2020 NHANH (PLANE_IMP_AFFINE) THEN
2021 REPEAT STRIP_TAC THEN
2022 REWRITE_TAC[aff; SET_EQ_TO_SUBSET] THEN CONJ_TAC THENL [
2023 UNDISCH_TAC ` plane_norm (p:real^3 -> bool ) ` THEN
2024 REWRITE_TAC[plane_norm] THEN
2026 UNDISCH_TAC ` {(x:real^3), y, z} SUBSET p` THEN
2027 ASM_SIMP_TAC[SET3_SUBSET; IN_ELIM_THM] THEN
2028 NHANH (IN_PLANE_IMP_OTHORGONAL ) THEN
2030 NHANH (MESON[NOT_COL_AND_ORTHO_IMP_NOT_COPL]`
2031 ~collinear {(x:real^3), y, z} /\
2032 ~(n = vec 0) /\a1 /\a2 /\a4 /\a3/\
2033 n dot (x - y) = &0 /\
2034 n dot (x - z) = &0 ==> ~coplanar_alt { x + n ,x,y,z} `) THEN
2035 REWRITE_TAC[SUBSET; IN_ELIM_THM] THEN
2036 REPEAT STRIP_TAC THEN
2037 UNDISCH_TAC `~coplanar_alt {x + n, x, y, (z:real^3)} ` THEN
2038 NHANH (SPEC `x' :real^3` (GEN `v :real^3` ( SPEC_ALL COEFS_4 ))) THEN
2039 ABBREV_TAC ` a1 = COEF4_1 (x + n) x y z x'` THEN
2040 ABBREV_TAC ` a2 = COEF4_2 (x + n) x y z x'` THEN
2041 ABBREV_TAC ` a3 = COEF4_3 (x + n) x y z x'` THEN
2042 ABBREV_TAC ` a4 = COEF4_4 (x + n) x y z x'` THEN
2045 REWRITE_TAC[AFFINE_HULL_3; IN_ELIM_THM] THEN
2046 NHANH (MESON[IMP_A1_EQ_0]` ~(n = vec 0) /\
2048 n dot (x - v0) = &0 /\
2049 n dot (y - v0) = &0 /\
2050 n dot (z - v0) = &0 /\
2052 n dot (x' - v0) = &0 /\aa4/\aa5 /\aa6/\aa7/\
2053 ~coplanar_alt {x + n, x, y, z} /\
2054 a1 + a2 + a3 + a4 = &1 /\
2055 x' = a1 % (x + n) + a2 % x + a3 % y + a4 % z /\ l ==>
2057 PURE_ONCE_REWRITE_TAC[MESON[]` P a1 /\ a1 = &0 <=> P (&0) /\
2059 REWRITE_TAC[ZERO_NEUTRAL; VECTOR_ARITH` &0 % x + y = y `] THEN
2061 ASM_MESON_TAC[PLANE_NORM_IMP_AFFINE ; FINITE_RULES;
2062 SET_RULE` ~({(x:real^N), y, z} = {} )`; IMP_AFFINE_HULL_SUBSET]]);;
2064 let SMWTDMU = LEMMA7;;
2066 let DET_VEC3_AS_CROSS_DOT = prove_by_refinement(
2067 ` det_vec3 v1 v2 v3 = ( v1 cross v2 ) dot v3 `,
2070 (REWRITE_TAC[det_vec3; cross; triple_of_real3; real3_of_triple; mk_vec3; DOT_3; VECTOR_3]);
2072 (REWRITE_TAC[det_vec3; cross; triple_of_real3; real3_of_triple; mk_vec3; DOT_3; VECTOR_3]);
2073 BY((REAL_ARITH_TAC))
2077 let COL_EQ_NORM_CROSS = prove_by_refinement(
2078 ` ! v1 v2 (v3:real^3). collinear {v1,v2,v3} <=>
2079 norm ( (v2 - v1) cross (v3 - v1)) pow 2 = &0 `,
2082 (REWRITE_TAC[COL_EQ_UPS_0]);
2083 (REWRITE_TAC[GSYM NORM_CROSS_PRODUCT_UPS_X]);
2084 BY((REAL_ARITH_TAC))
2091 let COLLINEAR_IMP_COPLANAR = prove(` ! v1 v2 v3 v3 (v:real^3). collinear {v1,v2,v3} ==>
2092 coplanar_alt {v1,v2,v3,v} `,
2093 REWRITE_TAC[COPLANAR_DET_VEC3_EQ_0; COL_EQ_NORM_CROSS; DET_VEC3_AS_CROSS_DOT ] THEN
2094 REWRITE_TAC[GSYM RELATE_POW2; NORM_EQ_0] THEN REPEAT GEN_TAC THEN
2095 SIMP_TAC[VECTOR_ARITH ` vec 0 dot x = &0 `]);;
2097 (* MAY WORKS, LEMMA 85 ; VBVYGGT *)
2102 let POS_EQ_NOT_COPLANANR = prove(` &0 < delta (dist ((x1:real^3),x2) pow 2) (dist (x1,x3) pow 2)
2103 (dist (x1,x4) pow 2)
2104 (dist (x2,x3) pow 2)
2105 (dist (x2,x4) pow 2)
2106 (dist (x3,x4) pow 2) <=> ~coplanar_alt {x1, x2, x3, x4} `,
2107 MP_TAC (DELTA_POS_4POINTS) THEN MP_TAC POLFLZY THEN LET_TR THEN
2108 REWRITE_TAC[REAL_ARITH` a <= b <=> a = b \/ a < b `] THEN
2109 MESON_TAC[REAL_ARITH` ~( a = b /\ a < b ) `]);;
2111 let SUM_CHI_EQ_2DELTA = prove(` let chi11 = chi x12 x13 x14 x23 x24 x34 in
2112 let chi22 = chi x12 x24 x23 x14 x13 x34 in
2113 let chi33 = chi x34 x13 x23 x14 x24 x12 in
2114 let chi44 = chi x34 x24 x14 x23 x13 x12 in
2115 &2 * delta x12 x13 x14 x23 x24 x34 = chi11 + chi22 + chi33 + chi44`, LET_TR THEN
2116 REWRITE_TAC[chi; delta] THEN REAL_ARITH_TAC);;
2118 let NOT_0_IMP_SUM_CHI_1 = prove(`~(delta x12 x13 x14 x23 x24 x34 = &0)
2119 ==> chi x12 x13 x14 x23 x24 x34 / (&2 * delta x12 x13 x14 x23 x24 x34) +
2120 chi x12 x24 x23 x14 x13 x34 / (&2 * delta x12 x13 x14 x23 x24 x34) +
2121 chi x34 x13 x23 x14 x24 x12 / (&2 * delta x12 x13 x14 x23 x24 x34) +
2122 chi x34 x24 x14 x23 x13 x12 / (&2 * delta x12 x13 x14 x23 x24 x34) =
2123 &1`, MP_TAC SUM_CHI_EQ_2DELTA THEN
2124 LET_TR THEN CONV_TAC REAL_FIELD);;
2128 let PROVE_DIST_FROM_V1 = prove(` ~coplanar_alt {v1, v2, v3, v4} ==>
2129 let x12 = dist (v1,v2) pow 2 in
2130 let x13 = dist (v1,v3) pow 2 in
2131 let x14 = dist (v1,v4) pow 2 in
2132 let x23 = dist (v2,v3) pow 2 in
2133 let x24 = dist (v2,v4) pow 2 in
2134 let x34 = dist (v3,v4) pow 2 in
2135 let chi11 = chi x12 x13 x14 x23 x24 x34 in
2136 let chi22 = chi x12 x24 x23 x14 x13 x34 in
2137 let chi33 = chi x34 x13 x23 x14 x24 x12 in
2138 let chi44 = chi x34 x24 x14 x23 x13 x12 in
2140 &1 / (&2 * delta x12 x13 x14 x23 x24 x34) %
2141 (chi11 % v1 + chi22 % v2 + chi33 % v3 + chi44 % v4)
2142 ==> dist3 p v1 pow 2 =
2143 ( &1 / &2 ) * rho_ij' x12 x13 x14 x23 x24 x34 / (&2 * delta x12 x13 x14 x23 x24 x34) `,
2144 REWRITE_TAC[ GSYM POS_EQ_NOT_COPLANANR] THEN
2145 NHANH (REAL_ARITH` a < b ==> ~( b = a ) `) THEN
2146 NHANH NOT_0_IMP_SUM_CHI_1 THEN
2147 LET_TR THEN REWRITE_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC;
2148 REAL_ARITH` ( &1 / a ) * b = b / a `] THEN
2149 ABBREV_TAC ` a1 = chi (dist (v1,v2) pow 2) (dist (v1,v3) pow 2) (dist (v1,v4) pow 2)
2150 (dist (v2,v3) pow 2)
2151 (dist (v2,v4) pow 2)
2152 (dist (v3,v4) pow 2) /
2154 delta (dist (v1,v2) pow 2) (dist (v1,v3) pow 2) (dist (v1,v4) pow 2)
2155 (dist (v2,v3) pow 2)
2156 (dist (v2,v4) pow 2)
2157 (dist (v3,(v4:real^3)) pow 2))` THEN
2158 ABBREV_TAC ` a2 = chi (dist (v1,v2) pow 2) (dist (v2,v4) pow 2) (dist (v2,v3) pow 2)
2159 (dist (v1,v4) pow 2)
2160 (dist (v1,v3) pow 2)
2161 (dist (v3,v4) pow 2) /
2163 delta (dist (v1,v2) pow 2) (dist (v1,v3) pow 2) (dist (v1,v4) pow 2)
2164 (dist (v2,v3) pow 2)
2165 (dist (v2,v4) pow 2)
2166 (dist (v3,(v4:real^3)) pow 2)) ` THEN
2167 REWRITE_TAC[ GSYM dist3] THEN
2168 ABBREV_TAC ` a3 = chi (dist3 v3 v4 pow 2) (dist3 v1 v3 pow 2) (dist3 v2 v3 pow 2) (dist3 v1 v4 pow 2)
2170 (dist3 v1 v2 pow 2) /
2172 delta (dist3 v1 v2 pow 2) (dist3 v1 v3 pow 2) (dist3 v1 v4 pow 2)
2175 (dist3 v3 v4 pow 2)) ` THEN
2176 ABBREV_TAC ` a4 = chi (dist3 v3 v4 pow 2) (dist3 v2 v4 pow 2) (dist3 v1 v4 pow 2) (dist3 v2 v3 pow 2)
2178 (dist3 v1 v2 pow 2) /
2180 delta (dist3 v1 v2 pow 2) (dist3 v1 v3 pow 2) (dist3 v1 v4 pow 2)
2183 (dist3 v3 v4 pow 2)) ` THEN
2184 SIMP_TAC[REAL_ARITH` a + b = &1 <=> a = &1 - b `] THEN
2185 REPEAT STRIP_TAC THEN
2186 REWRITE_TAC[dist3; dist; NORM_POW_2; VECTOR_ARITH`
2187 (((&1 - (a2 + a3 + a4)) % v1 + a2 % v2 + a3 % v3 + a4 % v4) - v1) =
2188 a2 % ( v2 - v1 ) + a3 % (v3 - v1 ) + a4 % ( v4 - v1 ) `;
2189 VECTOR_ARITH` ( a + b ) dot ( a + b ) = a dot a + &2 * ( a dot b )
2191 REWRITE_TAC[DOT_RADD; DOT_LMUL; DOT_RMUL] THEN
2192 REWRITE_TAC[X_DOT_X_EQ] THEN
2193 REWRITE_TAC[DOT_NORM_NEG; VECTOR_ARITH` v2 - v1 - (v4 - v1)
2194 = (v2:real^N) - v4 `] THEN
2195 SIMP_TAC[GSYM dist; DIST_SYM; GSYM dist3; D3_SYM] THEN
2196 EXPAND_TAC "a2" THEN
2197 EXPAND_TAC "a3" THEN
2198 EXPAND_TAC "a4" THEN
2199 REWRITE_TAC[GSYM dist3 ] THEN
2200 ABBREV_TAC ` x12 = dist3 v1 v2 pow 2 ` THEN
2201 ABBREV_TAC ` x13 = dist3 v1 v3 pow 2 ` THEN
2202 ABBREV_TAC ` x14 = dist3 v1 v4 pow 2 ` THEN
2203 ABBREV_TAC ` x23 = dist3 v2 v3 pow 2 ` THEN
2204 ABBREV_TAC ` x24 = dist3 v2 v4 pow 2 ` THEN
2205 ABBREV_TAC ` x34 = dist3 v3 v4 pow 2 ` THEN
2206 UNDISCH_TAC ` &0 < delta x12 x13 x14 x23 x24 x34 ` THEN
2207 ONCE_REWRITE_TAC[REAL_FIELD` &0 < a ==> b = c <=> &0 < a
2208 ==> b * ( &2 * a) pow 2 = c * ( &2 * a ) pow 2 `] THEN
2209 ONCE_REWRITE_TAC[REAL_ARITH` &0 < a <=> &0 < &2 * a `] THEN
2210 SIMP_TAC[REAL_FIELD` &0 < b ==> ( a / b ) * b pow 2 = a * b `;
2211 REAL_RDISTRIB; REAL_FIELD` &0 < b ==> ( a / b ) * ( aa / b ) * c *
2212 b pow 2 = a * aa * c `; REAL_ADD_LDISTRIB] THEN
2213 SIMP_TAC[REAL_LDISTRIB; REAL_ARITH` (a*b)*c = a *b * c `;
2214 REAL_FIELD` &0 < b ==> ( a / b ) * ( a / b ) * c * b pow 2 = a pow 2 * c `;
2215 REAL_ARITH` &2 * a * b * c / &2 * d = a * b * d * c `] THEN
2216 SIMP_TAC[REAL_FIELD` &0 < a ==> ( b / a ) * ( bb / a ) * a pow 2
2217 * d = b * bb * d `] THEN
2218 SIMP_TAC[REAL_FIELD` &0 < a ==> b / a / &2 * a pow 2 =
2220 REWRITE_TAC[chi; rho_ij'; delta] THEN
2223 let PROVE_EQ_DIST_FROM4 = prove(` ~coplanar_alt {v1, v2, v3, v4} ==>
2224 let x12 = dist (v1,v2) pow 2 in
2225 let x13 = dist (v1,v3) pow 2 in
2226 let x14 = dist (v1,v4) pow 2 in
2227 let x23 = dist (v2,v3) pow 2 in
2228 let x24 = dist (v2,v4) pow 2 in
2229 let x34 = dist (v3,v4) pow 2 in
2230 let chi11 = chi x12 x13 x14 x23 x24 x34 in
2231 let chi22 = chi x12 x24 x23 x14 x13 x34 in
2232 let chi33 = chi x34 x13 x23 x14 x24 x12 in
2233 let chi44 = chi x34 x24 x14 x23 x13 x12 in
2235 &1 / (&2 * delta x12 x13 x14 x23 x24 x34) %
2236 (chi11 % v1 + chi22 % v2 + chi33 % v3 + chi44 % v4)
2238 dist3 p v2 pow 2 = ( &1 / &2 ) * rho_ij' x12 x13 x14 x23 x24 x34 / (&2 * delta x12 x13 x14 x23 x24 x34) /\
2239 dist3 p v3 pow 2 = ( &1 / &2 ) * rho_ij' x12 x13 x14 x23 x24 x34 / (&2 * delta x12 x13 x14 x23 x24 x34) /\
2241 ( &1 / &2 ) * rho_ij' x12 x13 x14 x23 x24 x34 / (&2 * delta x12 x13 x14 x23 x24 x34) `,
2242 REWRITE_TAC[ GSYM POS_EQ_NOT_COPLANANR] THEN
2243 NHANH (REAL_ARITH` a < b ==> ~( b = a ) `) THEN
2244 NHANH NOT_0_IMP_SUM_CHI_1 THEN
2245 LET_TR THEN REWRITE_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC;
2246 REAL_ARITH` ( &1 / a ) * b = b / a `] THEN
2247 ABBREV_TAC ` a1 = chi (dist (v1,v2) pow 2) (dist (v1,v3) pow 2) (dist (v1,v4) pow 2)
2248 (dist (v2,v3) pow 2)
2249 (dist (v2,v4) pow 2)
2250 (dist (v3,v4) pow 2) /
2252 delta (dist (v1,v2) pow 2) (dist (v1,v3) pow 2) (dist (v1,v4) pow 2)
2253 (dist (v2,v3) pow 2)
2254 (dist (v2,v4) pow 2)
2255 (dist (v3,(v4:real^3)) pow 2))` THEN
2256 ABBREV_TAC ` a2 = chi (dist (v1,v2) pow 2) (dist (v2,v4) pow 2) (dist (v2,v3) pow 2)
2257 (dist (v1,v4) pow 2)
2258 (dist (v1,v3) pow 2)
2259 (dist (v3,v4) pow 2) /
2261 delta (dist (v1,v2) pow 2) (dist (v1,v3) pow 2) (dist (v1,v4) pow 2)
2262 (dist (v2,v3) pow 2)
2263 (dist (v2,v4) pow 2)
2264 (dist (v3,(v4:real^3)) pow 2)) ` THEN
2265 REWRITE_TAC[ GSYM dist3] THEN
2266 ABBREV_TAC ` a3 = chi (dist3 v3 v4 pow 2) (dist3 v1 v3 pow 2) (dist3 v2 v3 pow 2) (dist3 v1 v4 pow 2)
2268 (dist3 v1 v2 pow 2) /
2270 delta (dist3 v1 v2 pow 2) (dist3 v1 v3 pow 2) (dist3 v1 v4 pow 2)
2273 (dist3 v3 v4 pow 2)) ` THEN
2274 ABBREV_TAC ` a4 = chi (dist3 v3 v4 pow 2) (dist3 v2 v4 pow 2) (dist3 v1 v4 pow 2) (dist3 v2 v3 pow 2)
2276 (dist3 v1 v2 pow 2) /
2278 delta (dist3 v1 v2 pow 2) (dist3 v1 v3 pow 2) (dist3 v1 v4 pow 2)
2281 (dist3 v3 v4 pow 2)) ` THEN
2282 ONCE_REWRITE_TAC[MESON[VECTOR_ARITH` &1 % x = x `]` dist3 a b pow 2 =
2283 aa <=> dist3 a ( &1 % b ) pow 2 = aa `] THEN
2284 ONCE_REWRITE_TAC[MESON[]` a = &1 <=> &1 = a `] THEN
2286 STRIP_TAC THEN STRIP_TAC THEN
2287 REWRITE_TAC[dist3; dist] THEN
2288 REWRITE_TAC[VECTOR_ARITH` (a1 % v1 + a2 % v2 + a3 % v3 + a4 % v4) - (a1 + a2 + a3 + a4) % v2
2289 = a1 % ( v1 - v2 ) + a3 % ( v3 - v2 ) + a4 % (v4 - v2 ) `;
2290 VECTOR_ARITH` (a1 % v1 + a2 % v2 + a3 % v3 + a4 % v4) - (a1 + a2 + a3 + a4) % v3
2291 = a1 % ( v1 - v3 ) + a2 % ( v2 - v3 ) + a4 % (v4 - v3 )`;
2292 VECTOR_ARITH` (a1 % v1 + a2 % v2 + a3 % v3 + a4 % v4) - (a1 + a2 + a3 + a4) % v4 =
2293 a1 % ( v1 - v4 ) + a2 % ( v2 - v4 ) + a3 % (v3 - v4 )`] THEN
2294 REWRITE_TAC[NORM_POW_2] THEN
2295 REWRITE_TAC[DOT_LADD; DOT_RADD; DOT_LMUL; DOT_RMUL; GSYM NORM_POW_2] THEN
2296 REWRITE_TAC[DOT_NORM_NEG; VECTOR_ARITH` v3 - v4 - (v2 - v4) =
2297 (v3:real^N) - v2 `; GSYM dist; GSYM dist3 ] THEN
2298 EXPAND_TAC "a1" THEN
2299 EXPAND_TAC "a2" THEN
2300 EXPAND_TAC "a3" THEN
2301 EXPAND_TAC "a4" THEN
2302 REWRITE_TAC[GSYM dist3 ] THEN
2303 REWRITE_TAC[prove(` dist3 (v4 - v3) (v1 - v3) = dist3 v1 v4 `,
2304 REWRITE_TAC[dist3] THEN CONV_TAC NORM_ARITH)] THEN
2305 SIMP_TAC[D3_SYM] THEN
2306 ABBREV_TAC ` x12 = dist3 v1 v2 pow 2 ` THEN
2307 ABBREV_TAC ` x13 = dist3 v1 v3 pow 2 ` THEN
2308 ABBREV_TAC ` x14 = dist3 v1 v4 pow 2 ` THEN
2309 ABBREV_TAC ` x23 = dist3 v2 v3 pow 2 ` THEN
2310 ABBREV_TAC ` x24 = dist3 v2 v4 pow 2 ` THEN
2311 ABBREV_TAC ` x34 = dist3 v3 v4 pow 2 ` THEN
2312 UNDISCH_TAC ` &0 < delta x12 x13 x14 x23 x24 x34 ` THEN
2313 ONCE_REWRITE_TAC[REAL_FIELD` &0 < a ==> ( b = c ) /\ ( bb = cc ) /\ ( bbb = ccc )
2315 ==> ( b * ( &2 * a) pow 2 = c * ( &2 * a ) pow 2 ) /\
2316 ( bb * ( &2 * a) pow 2 = cc * ( &2 * a ) pow 2 ) /\
2317 ( bbb * ( &2 * a) pow 2 = ccc * ( &2 * a ) pow 2 ) `] THEN
2318 ONCE_REWRITE_TAC[REAL_ARITH` &0 < a <=> &0 < &2 * a `] THEN
2319 SIMP_TAC[REAL_FIELD` &0 < b ==> ( a / b ) * b pow 2 = a * b `;
2320 REAL_RDISTRIB; REAL_FIELD` &0 < b ==> ( a / b ) * ( aa / b ) * c *
2321 b pow 2 = a * aa * c `; REAL_ADD_LDISTRIB] THEN
2322 SIMP_TAC[REAL_LDISTRIB; REAL_ARITH` (a*b)*c = a *b * c `;
2323 REAL_FIELD` &0 < b ==> ( a / b ) * ( a / b ) * c * b pow 2 = a pow 2 * c `;
2324 REAL_ARITH` &2 * a * b * c / &2 * d = a * b * d * c `] THEN
2325 SIMP_TAC[REAL_FIELD` &0 < a ==> ( b / a ) * ( bb / a ) * a pow 2
2326 * d = b * bb * d `] THEN
2327 SIMP_TAC[REAL_FIELD` &0 < a ==> b / a / &2 * a pow 2 =
2328 a * b / &2 `] THEN SIMP_TAC[REAL_FIELD` &0 < b ==> ( a / b ) * b pow 2 = a * b `;
2329 REAL_RDISTRIB; REAL_FIELD` &0 < b ==> ( a / b ) * ( aa / b ) * c *
2330 b pow 2 = a * aa * c `; REAL_ADD_LDISTRIB] THEN
2331 SIMP_TAC[REAL_LDISTRIB; REAL_ARITH` (a*b)*c = a *b * c `;
2332 REAL_FIELD` &0 < b ==> ( a / b ) * ( a / b ) * c * b pow 2 = a pow 2 * c `;
2333 REAL_ARITH` &2 * a * b * c / &2 * d = a * b * d * c `] THEN
2334 SIMP_TAC[REAL_FIELD` &0 < a ==> ( b / a ) * ( bb / a ) * a pow 2
2335 * d = b * bb * d `] THEN
2336 SIMP_TAC[REAL_FIELD` &0 < a ==> b / a / &2 * a pow 2 =
2338 DISCH_TAC THEN REWRITE_TAC[chi; rho_ij'; delta] THEN
2341 let AFFINE_HULL_3 = prove
2342 (`affine hull {a,b,c} =
2343 { u % a + v % b + w % c | u + v + w = &1}`,
2344 SIMP_TAC[AFFINE_HULL_FINITE; FINITE_INSERT; FINITE_RULES] THEN
2345 SIMP_TAC[AFFINE_HULL_FINITE_STEP; FINITE_INSERT; FINITE_RULES] THEN
2346 REWRITE_TAC[REAL_ARITH `x - y = z:real <=> x = y + z`;
2347 VECTOR_ARITH `x - y = z:real^N <=> x = y + z`] THEN
2348 REWRITE_TAC[VECTOR_ADD_RID; REAL_ADD_RID] THEN SET_TAC[]);;
2350 let AFFINE_HULL_4 = prove
2351 (`affine hull {a,b,c,d} =
2352 { u % a + v % b + w % c + z % d | u + v + w + z = &1}`,
2353 SIMP_TAC[AFFINE_HULL_FINITE; FINITE_INSERT; FINITE_RULES] THEN
2354 SIMP_TAC[AFFINE_HULL_FINITE_STEP; FINITE_INSERT; FINITE_RULES] THEN
2355 REWRITE_TAC[REAL_ARITH `x - y = z:real <=> x = y + z`;
2356 VECTOR_ARITH `x - y = z:real^N <=> x = y + z`] THEN
2357 REWRITE_TAC[VECTOR_ADD_RID; REAL_ADD_RID] THEN SET_TAC[]);;
2360 let PROVE_EXISTS_CIR_OF_FOUR_POINTS = prove(`!(v1:real^3) v2 v3 v4.
2361 CARD {v1, v2, v3, v4} = 4 /\ ~coplanar_alt {v1, v2, v3, v4}
2362 ==> (? p. p IN affine hull {v1, v2, v3, v4} /\
2363 (?r. !v. v IN {v1, v2, v3, v4}
2364 ==> r = dist (p, v))) `,
2365 NHANH (REWRITE_RULE[RIGHT_FORALL_IMP_THM] (GEN `p:real^3` PROVE_DIST_FROM_V1)) THEN
2366 NHANH (REWRITE_RULE[RIGHT_FORALL_IMP_THM] (GEN `p:real^3` PROVE_EQ_DIST_FROM4 )) THEN
2367 REPEAT GEN_TAC THEN REPEAT LET_TAC THEN ABBREV_TAC `rr = &1 / &2 *
2368 rho_ij' x12 x13 x14 x23 x24 x34 / (&2 * delta x12 x13 x14 x23 x24 x34) ` THEN
2369 REWRITE_TAC[GSYM POS_EQ_NOT_COPLANANR] THEN
2370 NHANH (SPEC_ALL REAL_POS_NZ) THEN ASM_SIMP_TAC[] THEN
2371 NHANH (NOT_0_IMP_SUM_CHI_1 ) THEN ASM_SIMP_TAC[] THEN
2372 REWRITE_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC;
2373 REAL_ARITH ` &1 / a * b = b / a `] THEN
2374 REWRITE_TAC[FORALL_IN_CLAUSES; MESON[]`(? r. (r:real) = a /\
2375 r = b /\ r = c /\ r = d ) <=> a = b /\ a = c /\ a = d `] THEN
2376 REWRITE_TAC[MESON[]` (! x. x = a ==> P a ) <=> P a `] THEN DISCH_TAC THEN
2377 EXISTS_TAC ` chi11 / (&2 * delta x12 x13 x14 x23 x24 x34) % (v1:real^3) +
2378 chi22 / (&2 * delta x12 x13 x14 x23 x24 x34) % v2 +
2379 chi33 / (&2 * delta x12 x13 x14 x23 x24 x34) % v3 +
2380 chi44 / (&2 * delta x12 x13 x14 x23 x24 x34) % v4 ` THEN
2381 CONJ_TAC THENL [REWRITE_TAC[AFFINE_HULL_4; IN_ELIM_THM] THEN
2382 FIRST_X_ASSUM MP_TAC THEN MESON_TAC[NOT_0_IMP_SUM_CHI_1 ];
2383 FIRST_X_ASSUM MP_TAC THEN SIMP_TAC[dist3; DIST_POS_LE; EQ_POW2_COND]]);;
2396 let IMP_PROPERTIES_OF_CIR4 = prove(`!(v1:real^3) v2 v3 v4.
2397 CARD {v1, v2, v3, v4} = 4 /\ ~coplanar_alt {v1, v2, v3, v4}
2398 ==> circumcenter {v1, v2, v3, v4} IN affine hull {v1, v2, v3, v4} /\
2399 (?r. !v. v IN {v1, v2, v3, v4}
2400 ==> r = dist (circumcenter {v1, v2, v3, v4},v))`,
2401 NHANH (SPEC_ALL PROVE_EXISTS_CIR_OF_FOUR_POINTS ) THEN REWRITE_TAC[circumcenter; IN]
2402 THEN MESON_TAC[EXISTS_THM]);;
2407 let DIST_EQ_IMP_ORTHOGONAL = prove(` dist (pp,v2) = dist (pp,v1) /\
2408 dist (p,v2) = dist (p,v1) ==>
2409 (pp - p ) dot (v2 - v1 ) = &0 `,
2410 REWRITE_TAC[MONG7_ROI; DOT_LSUB] THEN REAL_ARITH_TAC);;
2414 let IMP_OTHO4 = prove(` n dot (v2 - v1) = &0 /\
2415 n dot (v3 - v1) = &0 /\
2416 n dot (v4 - v1) = &0 /\
2417 x IN affine hull {v1,v2,v3,v4} /\
2418 y IN affine hull {v1,v2,v3,v4} ==>
2419 n dot (x - y ) = &0 `,
2420 REWRITE_TAC[AFFINE_HULL_4; IN_ELIM_THM] THEN STRIP_TAC THEN
2421 DOWN_TAC THEN IMP_TAC THEN SIMP_TAC[REAL_ARITH`a + b = c <=> a = c - b `] THEN
2422 PHA THEN REWRITE_TAC[VECTOR_ARITH` ((&1 - (v' + w' + z')) % v1 + v' % v2 +
2423 w' % v3 + z' % v4) - ((&1 - (v + w + z)) % v1 + v % v2 + w % v3 + z % v4) =
2424 ( v' - v ) % ( v2 - v1 ) + ( w' - w ) % ( v3 - v1 ) +
2425 ( z' - z ) % ( v4 - v1 ) `] THEN
2426 SIMP_TAC[DOT_RADD; DOT_RMUL; ZERO_NEUTRAL]);;
2432 let UNIQUE_EXISISTING_PROPERTY_C4 = prove(`!(v1:real^3) v2 v3 v4.
2433 CARD {v1, v2, v3, v4} = 4 /\ ~coplanar_alt {v1, v2, v3, v4}
2434 ==> (!p. p IN affine hull {v1, v2, v3, v4} /\
2435 (?r. !v. v IN {v1, v2, v3, v4} ==> r = dist (p,v))
2436 ==> p = circumcenter {v1, v2, v3, v4}) `,
2437 NHANH (SPEC_ALL IMP_PROPERTIES_OF_CIR4 ) THEN
2439 ABBREV_TAC ` pp = circumcenter {(v1:real^3), v2, v3, v4}` THEN
2440 REPEAT STRIP_TAC THEN
2442 REWRITE_TAC[FORALL_IN_CLAUSES] THEN
2443 REWRITE_TAC[MESON[]` r = a /\ r = b /\ r = c /\ r = d <=> r = a /\ b = a /\ c = a
2446 NHANH (MESON[DIST_EQ_IMP_ORTHOGONAL ]`dist (pp,v2) = dist (pp,v1) /\
2447 dist (pp,v3) = dist (pp,v1) /\
2448 dist (pp,v4) = dist (pp,v1) /\a11/\a2/\
2449 dist (p,v2) = dist (p,v1) /\
2450 dist (p,v3) = dist (p,v1) /\
2451 dist (p,v4) = dist (p,v1) ==>
2452 ( p - pp) dot ( v2 - v1 ) = &0 /\
2453 ( p - pp ) dot ( v3 - v1 ) = &0 /\
2454 ( p - pp ) dot ( v4 - v1 ) = &0 `) THEN
2455 ONCE_REWRITE_TAC[GSYM VECTOR_SUB_EQ] THEN
2456 REWRITE_TAC[GSYM DOT_EQ_0] THEN MESON_TAC[IMP_OTHO4 ]);;
2461 let PROVE_IN_AFFINE_HULL_4 = prove(
2462 `~(delta x12 x13 x14 x23 x24 x34 = &0)
2463 ==> &1 / (&2 * delta x12 x13 x14 x23 x24 x34) %
2464 (chi x12 x13 x14 x23 x24 x34 % v1 +
2465 chi x12 x24 x23 x14 x13 x34 % v2 +
2466 chi x34 x13 x23 x14 x24 x12 % v3 +
2467 chi x34 x24 x14 x23 x13 x12 % v4) IN
2468 affine hull {(v1:real^3), v2, v3, v4}`,
2469 REWRITE_TAC[AFFINE_HULL_4; IN_ELIM_THM; VECTOR_ADD_LDISTRIB;
2470 VECTOR_MUL_ASSOC; REAL_ARITH ` ( &1 / a ) * b = b/a `]
2471 THEN MESON_TAC[NOT_0_IMP_SUM_CHI_1]);;
2475 (* VBVYGGT , le 85 *)
2479 MESON[POW_2_SQRT; DIST_POS_LE]` dist (x,y) pow 2 = r ==> dist (x,y) = sqrt ( r ) `;;
2482 let VBVYGGT = prove(`!(v1:real^3) v2 v3 v4.
2483 CARD {v1, v2, v3, v4} = 4 /\ ~coplanar_alt {v1, v2, v3, v4}
2484 ==> circumcenter {v1, v2, v3, v4} IN affine hull {v1, v2, v3, v4} /\
2485 (?r. !v. v IN {v1, v2, v3, v4}
2486 ==> r = dist (circumcenter {v1, v2, v3, v4},v)) /\
2487 (!p. p IN affine hull {v1, v2, v3, v4} /\
2488 (?r. !v. v IN {v1, v2, v3, v4} ==> r = dist (p,v))
2489 ==> p = circumcenter {v1, v2, v3, v4}) /\
2490 (let x12 = dist (v1,v2) pow 2 in
2491 let x13 = dist (v1,v3) pow 2 in
2492 let x14 = dist (v1,v4) pow 2 in
2493 let x23 = dist (v2,v3) pow 2 in
2494 let x24 = dist (v2,v4) pow 2 in
2495 let x34 = dist (v3,v4) pow 2 in
2496 let chi11 = chi x12 x13 x14 x23 x24 x34 in
2497 let chi22 = chi x12 x24 x23 x14 x13 x34 in
2498 let chi33 = chi x34 x13 x23 x14 x24 x12 in
2499 let chi44 = chi x34 x24 x14 x23 x13 x12 in
2500 circumcenter {v1, v2, v3, v4} =
2501 &1 / (&2 * delta x12 x13 x14 x23 x24 x34) %
2502 (chi11 % v1 + chi22 % v2 + chi33 % v3 + chi44 % v4)) `,
2503 NHANH (SPEC_ALL UNIQUE_EXISISTING_PROPERTY_C4 ) THEN
2504 NHANH (SPEC_ALL IMP_PROPERTIES_OF_CIR4 ) THEN
2505 REWRITE_TAC[MESON[]` (a /\ b1/\b2) /\ b ==> b1 /\b2/\ b/\ d <=> a /\ b1 /\b2/\b==>d `] THEN
2506 NHANH (REWRITE_RULE[RIGHT_FORALL_IMP_THM] ( GEN `p: real^3 `PROVE_DIST_FROM_V1)) THEN
2507 NHANH (REWRITE_RULE[RIGHT_FORALL_IMP_THM] ( GEN `p: real^3 ` PROVE_EQ_DIST_FROM4)) THEN
2508 REPEAT GEN_TAC THEN REPEAT LET_TAC THEN ABBREV_TAC `rr = &1 / &2 *
2509 rho_ij' x12 x13 x14 x23 x24 x34 / (&2 * delta x12 x13 x14 x23 x24 x34) ` THEN
2510 REWRITE_TAC[MESON[]` (! x. x = a ==> P x ) <=> P a `] THEN
2511 REWRITE_TAC[GSYM POS_EQ_NOT_COPLANANR] THEN
2512 NHANH (REAL_ARITH` &0 < a ==> ~( a = &0 )`) THEN
2513 NHANH (PROVE_IN_AFFINE_HULL_4 ) THEN
2514 UNDISCH_TAC ` dist ((v1:real^3),v2) pow 2 = x12` THEN
2515 UNDISCH_TAC ` dist ((v1:real^3),v3) pow 2 = x13` THEN
2516 UNDISCH_TAC ` dist ((v1:real^3),v4) pow 2 = x14` THEN
2517 UNDISCH_TAC ` dist ((v2:real^3),v3) pow 2 = x23` THEN
2518 UNDISCH_TAC ` dist ((v2:real^3),v4) pow 2 = x24` THEN
2519 UNDISCH_TAC ` dist ((v3:real^3),v4) pow 2 = x34` THEN
2520 UNDISCH_TAC ` chi x12 x13 x14 x23 x24 x34 = chi11 ` THEN
2521 UNDISCH_TAC ` chi x12 x24 x23 x14 x13 x34 = chi22 ` THEN
2522 UNDISCH_TAC ` chi x34 x13 x23 x14 x24 x12 = chi33` THEN
2523 UNDISCH_TAC ` chi x34 x24 x14 x23 x13 x12 = chi44` THEN
2524 REWRITE_TAC[MESON[]` a = b ==> P a <=> a = b ==> P b `] THEN
2525 ABBREV_TAC ` w = &1 / (&2 * delta x12 x13 x14 x23 x24 x34) %
2526 (chi11 % (v1:real^3) + chi22 % v2 + chi33 % v3 + chi44 % v4)` THEN
2527 REWRITE_TAC[MESON[]` a /\ b ==> c <=> a ==> b ==> c `]
2528 THEN REPLICATE_TAC 13 DISCH_TAC THEN
2529 REWRITE_TAC[FORALL_IN_CLAUSES;dist3] THEN PHA THEN
2530 NHANH (MESON[POW_2_SQRT; DIST_POS_LE]` dist (x,y) pow 2 = r
2531 ==> dist (x,y) = sqrt ( r ) `) THEN MESON_TAC[]);;
2533 let NOT_COPLANAR_IMP_EXISTS_CIR = prove(`! (v1:real^3) v2 v3 v4.
2534 CARD {v1, v2, v3, v4} = 4 /\ ~coplanar_alt {v1, v2, v3, v4}
2535 ==> circumcenter {v1, v2, v3, v4} IN affine hull {v1, v2, v3, v4} /\
2536 (?r. !v. v IN {v1, v2, v3, v4}
2537 ==> r = dist (circumcenter {v1, v2, v3, v4},v)) `,
2538 MESON_TAC[VBVYGGT]);;
2540 let THREE_POINTS_COP = prove(` ! v1 v2 (v3:real^3). coplanar_alt {v1,v2,v3} `,
2541 MESON_TAC[DIMINDEX_3; ARITH_RULE` 2 <= 3 `; COPLANAR_3]);;
2543 let PER_SET4 = SET_RULE ` {a,b,c,d} = {b,a,c,d} /\
2544 {a,b,c,d} = {c,b,a,d} /\
2545 {a,b,c,d} = {d,b,c,a} `;;
2547 let NOT_COPLANAR_IMP_CARD4 = prove(` ~ coplanar_alt {(v1:real^3), v2, v3, v4}
2548 ==> CARD {v1, v2, v3, v4} = 4 `, REWRITE_TAC[CARD4; IN_SET3] THEN
2549 MP_TAC (GEN_ALL THREE_POINTS_COP ) THEN
2550 MESON_TAC[PER_SET4; SET_RULE` {a,a,b,c} = {a,b,c} `]);;
2553 let NOT_COPLANAR_IMP_EXISTS_CIR2 = MESON[NOT_COPLANAR_IMP_EXISTS_CIR ;
2554 NOT_COPLANAR_IMP_CARD4 ]` ! (v1:real^3) v2 v3 v4. ~ coplanar_alt {v1, v2, v3, v4}
2555 ==> circumcenter {v1, v2, v3, v4} IN affine hull {v1, v2, v3, v4} /\
2556 (?r. !v. v IN {v1, v2, v3, v4}
2557 ==> r = dist (circumcenter {v1, v2, v3, v4},v)) `;;
2559 let NOT_COPLANAR_IMP_RADV_PROPERTIES = prove(` ~coplanar_alt {(v1:real^3), v2, v3, v4} ==>
2560 (! w. {v1, v2, v3, v4} w ==> radV {v1, v2, v3, v4}
2561 = dist (circumcenter {v1,v2,v3,v4} ,w) ) `,
2562 NHANH (SPEC_ALL NOT_COPLANAR_IMP_EXISTS_CIR2) THEN
2563 REWRITE_TAC[IN; radV] THEN MESON_TAC[EXISTS_THM]);;
2565 let ZJEWPAP = ` ! v1 v2 v3 (v4:real^3).
2566 let s = {v1, v2, v3, v4} in CARD s = 4 /\ ~ coplanar_alt s
2567 ==> radV {v1,v2,v3} <= radV s `;;
2569 let PHA = REWRITE_TAC[MESON[]` ( a ==> b ==> c <=> a /\ b ==> c ) /\
2570 ( (a /\ b ) /\ c <=> a /\ b /\ c ) `];;
2572 let NOT_COL_EQ_UPS_X_POS = prove(`! v1 v2 v3. ~ collinear {(v1:real^3), v2, v3} <=>
2573 &0 < ups_x (dist (v1,v2) pow 2) (dist (v1,v3) pow 2)
2574 (dist (v2,v3) pow 2) `,
2575 MP_TAC (GEN_ALL ZERO_LE_UPS_X) THEN REWRITE_TAC[UPS_X_EQ_ZERO_COND] THEN
2576 REWRITE_TAC[UPS_X_EQ_ZERO_COND; REAL_ARITH` a <= b <=> a = b \/ a < b `] THEN
2577 REWRITE_TAC[dist3] THEN MESON_TAC[REAL_ARITH` ~( a = b /\ a < b ) `]);;
2580 let ETA_Y_POW2_EQ = prove(`(dist (v1,v2) pow 2 * dist (v1,v3) pow 2 * dist (v2,v3) pow 2) /
2581 ups_x (dist (v1,v2) pow 2) (dist (v1,v3) pow 2) (dist (v2,v3) pow 2) =
2582 ( eta_y (dist3 v2 v3) (dist3 v1 v3) (dist3 v1 v2)) pow 2 `,
2583 REWRITE_TAC[eta_y;dist3; eta_x] THEN LET_TR THEN
2584 REWRITE_TAC[GSYM REAL_POW_2; GSYM dist3 ] THEN
2585 SIMP_TAC[MESON[UPS_X_SYM]` ups_x a b c = ups_x c b a `;
2586 REAL_ARITH ` a * b * c = c * b * a `] THEN
2587 MESON_TAC[SQRT_WORKS; REAL_LE_SQUARE_POW; REAL_LE_MUL;
2588 REAL_LE_DIV; dist3 ; ZERO_LE_UPS_X; UPS_X_SYM]);;
2591 let ETA_Y_POS_LE = prove(` &0 <= eta_y (dist3 v1 v2) (dist3 v1 v3) (dist3 v2 v3) `,
2592 REWRITE_TAC[eta_y; eta_x] THEN LET_TR THEN REWRITE_TAC[GSYM REAL_POW_2] THEN
2593 MESON_TAC[REAL_LE_POW_2; REAL_LE_MUL; ZERO_LE_UPS_X; REAL_LE_DIV;
2598 let ZJEWPAP = prove(` ! v1 v2 v3 (v4:real^3).
2599 let s = {v1, v2, v3, v4} in CARD s = 4 /\ ~ coplanar_alt s
2600 ==> radV {v1,v2,v3} <= radV s `,
2602 NHANH (MESON[COLLINEAR_IMP_COPLANAR ]`~coplanar_alt {v1, v2, v3, v4}
2603 ==> ~ collinear {(v1:real^3),v2,v3} `) THEN
2604 SIMP_TAC[NOT_COLL_IMP_RADV_EQ_ETA_Y] THEN
2605 REWRITE_TAC[MESON[]` a /\ b /\ c <=> (a/\b)/\c`] THEN
2606 NHANH (SPEC_ALL VBVYGGT) THEN
2608 NHANH (NOT_COPLANAR_IMP_RADV_PROPERTIES) THEN
2609 ABBREV_TAC ` pp = circumcenter {(v1:real^3), v2, v3, v4}` THEN
2610 MP_TAC (SPECL [`pp :real^3`; ` v1: real^3`; `v2:real^3`; ` v3:real^3`] DELTA_POS_4POINTS ) THEN
2611 REWRITE_TAC[REWRITE_RULE[IN] FORALL_IN_CLAUSES;
2612 FORALL_IN_CLAUSES ] THEN
2613 REWRITE_TAC[MESON[]` ( a ==> b ==> c <=> a /\ b ==> c ) /\
2614 ( (a /\ b ) /\ c <=> a /\ b /\ c ) `] THEN
2615 REPEAT STRIP_TAC THEN
2617 delta (dist ((pp:real^3),v1) pow 2) (dist (pp,v2) pow 2) (dist (pp,v3) pow 2)
2618 (dist (v1,v2) pow 2)
2619 (dist (v1,v3) pow 2)
2620 (dist (v2,v3) pow 2)` THEN
2621 ABBREV_TAC `p1 = dist ((pp:real^3),v1)` THEN
2622 ABBREV_TAC `p2 = dist ((pp:real^3),v2)` THEN
2623 ABBREV_TAC `p3 = dist ((pp:real^3),v3)` THEN
2624 REPLICATE_TAC 3 (FIRST_X_ASSUM MP_TAC THEN MATCH_MP_TAC
2625 (MESON[]` a ==> b ==> a `)) THEN
2626 EXPAND_TAC "p1" THEN
2627 EXPAND_TAC "p2" THEN
2628 EXPAND_TAC "p3" THEN
2629 FIRST_X_ASSUM MP_TAC THEN
2630 REWRITE_TAC[NOT_COL_EQ_UPS_X_POS ] THEN
2631 REWRITE_TAC[NOT_COL_EQ_UPS_X_POS; DELTA_RRR_INTERPRETE] THEN
2632 SIMP_TAC[REAL_FIELD` &0 < a ==> -- b * c + r * a = a * ( r - ( b * c ) / a ) `] THEN
2633 SIMP_TAC[ETA_Y_POW2_EQ; REAL_LE_MUL_EQ] THEN
2634 UNDISCH_TAC ` radV {(v1:real^3), v2, v3, v4} = p1 ` THEN
2636 EXPAND_TAC "p1" THEN
2637 UNDISCH_TAC `r = dist ((pp: real^3),v4)` THEN
2639 REPLICATE_TAC 3 REMOVE_TAC THEN
2640 SIMP_TAC[ETA_Y_SYYM; REAL_ARITH` &0 <= a - b <=> b <= a `] THEN
2641 MESON_TAC[DIST_POS_LE; POW2_COND; ETA_Y_POS_LE ]);;
2647 let NOT_EQ_BASIS_IMP_OTHORGANAL = MESON[DOT_BASIS_BASIS_UNEQUAL]
2648 ` ! i j. ~( i = j ) ==> basis i dot basis j = &0 `;;
2650 let BASIS_DIS_OTHORGONAL =
2651 MESON[ARITH_RULE` ~( 1 = 2 \/ 1 = 3 \/ 2 = 3 ) `; NOT_EQ_BASIS_IMP_OTHORGANAL]
2652 ` basis 1 dot basis 2 = &0 /\
2653 basis 1 dot basis 3 = &0 /\
2654 basis 2 dot basis 3 = &0 ` ;;
2656 let NORM_BASIS_VEC3 = prove(` ! i. i = 1 \/ i = 2 \/ i = 3 ==>
2657 norm (( basis i ):real^3 ) = &1 `,
2658 MESON_TAC[DIMINDEX_3; ARITH_RULE` i = 1 \/ i = 2 \/ i = 3 <=>
2659 1 <= i /\ i <= 3`; NORM_BASIS]);;
2661 let AAA_LEMMA = prove(` &0 < a /\
2663 b <= c /\ ll ==> &0 <= b pow 2 - a pow 2 /\ &0 <= c pow 2 - b pow 2 `,
2664 REWRITE_TAC[REAL_ARITH` &0 <= a - b <=> b <= a `] THEN
2665 MESON_TAC[REAL_LT_IMP_LE; POW2_COND; POS_IMP_POW2; REAL_LE_TRANS]);;
2667 let LLEEMAA = prove(` &0 < a /\
2675 c <= c' /\ l ==> &0 <= a' pow 2 - a pow 2 /\
2676 &0 <= b' pow 2 - b pow 2 /\
2677 &0 <= c' pow 2 - c pow 2 `,
2678 REWRITE_TAC[REAL_ARITH` &0 <= a - b <=> b <= a `] THEN
2679 MESON_TAC[POS_IMP_POW2; REAL_ARITH` a < b ==> a <= b `;
2682 let TYUNJLA = prove(` !(e1:real^3) e2 e3 a b c a' b' c' t1 t2 t3.
2695 (!x. x IN {t1, t2, t3} ==> &0 < x) /\
2696 t1 + t2 + t3 < &1 /\
2698 ((t1 + t2 + t3) * a) % e1 +
2699 ((t2 + t3) * sqrt (b pow 2 - a pow 2)) % e2 +
2700 (t3 * sqrt (c pow 2 - b pow 2)) % e3 /\
2701 v' = ((t1 + t2 + t3) * a') % e1 +
2702 ((t2 + t3) * sqrt (b' pow 2 - a' pow 2)) % e2 +
2703 (t3 * sqrt (c' pow 2 - b' pow 2)) % e3 ==>
2704 norm v <= norm v' `,
2705 REPEAT STRIP_TAC THEN FIRST_X_ASSUM MP_TAC THEN
2706 FIRST_X_ASSUM MP_TAC THEN
2707 SIMP_TAC[POW2_COND; NORM_POS_LE; NORM_POW_2; DOT_LADD; DOT_RADD;
2708 DOT_LMUL; DOT_RMUL] THEN ASM_SIMP_TAC[] THEN
2709 SIMP_TAC[GSYM NORM_POW_2; NORM_BASIS_VEC3 ] THEN
2710 SIMP_TAC[BASIS_DIS_OTHORGONAL; MESON[DOT_SYM; BASIS_DIS_OTHORGONAL]
2711 ` basis 2 dot basis 1 = &0 /\ basis 3 dot basis 1 = &0 /\
2712 basis 3 dot basis 2 = &0 `; ZERO_NEUTRAL] THEN
2713 REWRITE_TAC[REAL_ARITH` (a * x ) * ( b * x ) * c = a * b * c * x pow 2 `] THEN
2714 REPEAT STRIP_TAC THEN DOWN_TAC THEN
2715 NHANH (AAA_LEMMA) THEN PHA THEN
2716 NHANH (MESON[AAA_LEMMA]` &0 < a /\ a <= b /\ b <= c /\ aa <= a /\ l ==>
2717 &0 <= b pow 2 - a pow 2 /\ &0 <= c pow 2 - b pow 2 `) THEN
2718 SIMP_TAC[SQRT_WORKS] THEN
2719 ONCE_REWRITE_TAC[REAL_ARITH` a <= b <=> &0 <= b - a `] THEN
2720 REWRITE_TAC[REAL_ARITH` ((t1 + t2 + t3) * (t1 + t2 + t3) * &1 pow 2 * a' pow 2 +
2721 (t2 + t3) * (t2 + t3) * &1 pow 2 * (b' pow 2 - a' pow 2) +
2722 t3 * t3 * &1 pow 2 * (c' pow 2 - b' pow 2)) -
2723 ((t1 + t2 + t3) * (t1 + t2 + t3) * &1 pow 2 * a pow 2 +
2724 (t2 + t3) * (t2 + t3) * &1 pow 2 * (b pow 2 - a pow 2) +
2725 t3 * t3 * &1 pow 2 * (c pow 2 - b pow 2)) =
2726 t1 * ( t1 + &2 * t2 + &2 * t3 ) * ( a' pow 2 - a pow 2 ) +
2727 t2 * (t2 + &2 * t3 ) * ( b' pow 2 - b pow 2 ) +
2728 t3 pow 2 * ( c' pow 2 - c pow 2 ) `] THEN
2729 REWRITE_TAC[REAL_ARITH` &0 <= a - b <=> b <= a `] THEN
2730 PHA THEN NHANH (LLEEMAA) THEN STRIP_TAC THEN
2731 UNDISCH_TAC ` (!x. x IN {t1, t2, t3} ==> &0 < x)` THEN
2732 REPLICATE_TAC 3 ( FIRST_X_ASSUM MP_TAC) THEN
2733 REWRITE_TAC[FORALL_IN_CLAUSES] THEN PHA THEN
2734 NHANH (REAL_ARITH` &0 < t1 /\ &0 < t2 /\ &0 < t3 ==>
2735 &0 <= t1 /\ &0 <= t2 /\ &0 <= t1 + &2 * t2 + &2 * t3 /\
2736 &0 <= t2 + &2 * t3 `) THEN
2737 MESON_TAC[REAL_LE_ADD; REAL_LE_MUL; REAL_LE_POW_2]);;
2739 let LEMMA83 = TYUNJLA ;;
2741 let DELTA_TRIPLE_SUB_H_EXPAND = prove(`
2742 delta (a01 - h) (a02 - h) (a03 - h) x12 x13 x23 =
2743 delta a01 a02 a03 x12 x13 x23 - h * ups_x x12 x13 x23 `,
2744 REWRITE_TAC[delta;ups_x] THEN REAL_ARITH_TAC);;
2746 let PROVE_EXISTS_H_DELTA_0 = prove(`&0 < ups_x x12 x13 x23 /\ &0 <= delta a01 a02 a03 x12 x13 x23
2747 ==> (?h. &0 <= h /\ h = ( delta a01 a02 a03 x12 x13 x23 ) / ups_x x12 x13 x23 /\
2748 delta (a01 - h) (a02 - h) (a03 - h) x12 x13 x23 = &0 )`,
2749 REWRITE_TAC[DELTA_TRIPLE_SUB_H_EXPAND] THEN
2751 EXISTS_TAC`( delta a01 a02 a03 x12 x13 x23 ) / ups_x x12 x13 x23` THEN
2752 ASM_SIMP_TAC[REAL_LT_IMP_LE; REAL_LE_DIV] THEN
2753 FIRST_X_ASSUM MP_TAC THEN CONV_TAC REAL_FIELD);;
2755 let FIRST_POINT_IN_AFF3 = prove(` ! w v1 v2. w IN aff {w,v1,v2} `,
2756 REWRITE_TAC[aff; AFFINE_HULL_3; IN_ELIM_THM] THEN REPEAT GEN_TAC THEN
2757 EXISTS_TAC ` &1 ` THEN EXISTS_TAC `&0` THEN EXISTS_TAC `&0` THEN
2758 REWRITE_TAC[ZERO_NEUTRAL] THEN CONV_TAC VECTOR_ARITH);;
2760 let THREE_GEN_POINTS_IN_AFF3 = MESON[PER_SET3; FIRST_POINT_IN_AFF3 ]` a IN aff {a,b,c} /\
2761 b IN aff {a,b,c} /\ c IN aff {a,b,c} `;;
2763 let PROVE_THE_HYPOTHESI_FOR_74 = prove(` (let s = {v1, v2, v3, v4} in
2767 eta_y (dist3 v1 v2 ) (dist3 v1 v3) (dist3 v2 v3) <= r )
2768 ==> ( let x12 = dist3 v1 v2 pow 2 in
2769 let x13 = dist3 v1 v3 pow 2 in
2770 let x23 = dist3 v2 v3 pow 2 in
2771 CARD {v1, v2, v3, v4} = 4 /\
2773 ~coplanar_alt {v1, v2, v3, v4} /\
2777 delta (r pow 2) (r pow 2) (r pow 2) x12 x13 x23 >= &0 ) `,
2779 SIMP_TAC[REAL_LE_POW_2] THEN
2780 REWRITE_TAC[DELTA_RRR_INTERPRETE] THEN
2782 NHANH (MESON[COLLINEAR_IMP_COPLANAR]` ~ coplanar_alt {v1, v2, v3, v} ==>
2783 ~ collinear {v1, v2, (v3:real^3)} `) THEN
2784 REWRITE_TAC[NOT_COL_EQ_UPS_X_POS] THEN
2785 EXPAND_TAC "x12" THEN
2786 EXPAND_TAC "x13" THEN
2787 EXPAND_TAC "x23" THEN
2788 REWRITE_TAC[dist3] THEN
2789 SIMP_TAC[REAL_FIELD` &0 < a ==> -- x * y + r * a = a * ( r - (x * y ) / a )`] THEN
2790 SIMP_TAC[ETA_Y_POW2_EQ;dist3; ETA_Y_SYYM] THEN
2791 MP_TAC ETA_Y_POS_LE THEN
2793 REWRITE_TAC[dist3] THEN DAO THEN
2794 NHANH (MESON[POS_IMP_POW2]` a <= b /\ &0 <= a ==>
2795 a pow 2 <= b pow 2 `) THEN
2796 ONCE_REWRITE_TAC[REAL_ARITH` a <= b <=> &0 <= b - a `] THEN
2797 REWRITE_TAC[REAL_ARITH` a >= &0 <=> &0 <= a `] THEN
2798 SIMP_TAC[REAL_LT_IMP_LE; REAL_LE_MUL]);;
2801 let INSERT_SUBSET = SET_RULE` {} SUBSET s /\
2802 ( ( a INSERT s ) SUBSET ss <=> a IN ss /\ s SUBSET ss ) `;;
2805 let IMP_TAC = REWRITE_TAC[MESON[]` a /\ b ==> c <=> a ==> b ==> c `];;
2807 let IMP_OTHORGONAL_AFF3 = prove(`!v1 v2 v3 u.
2808 u dot (v1 - v2) = &0 /\ u dot (v1 - v3) = &0
2809 ==> (!x y. {x, y} SUBSET aff {v1, v2, v3} ==> u dot (x - y) = &0)`,
2810 REWRITE_TAC[aff; AFFINE_HULL_3; INSERT_SUBSET; IN_ELIM_THM] THEN
2811 REPEAT STRIP_TAC THEN DOWN_TAC THEN
2812 REWRITE_TAC[MESON[]` a /\ b ==> c <=> a ==> b ==> c `] THEN
2813 SIMP_TAC[REAL_ARITH` a + b = &1 <=> a = &1 - b `] THEN
2814 REWRITE_TAC[VECTOR_ARITH` ((&1 - (v + w)) % v1 + v % v2 + w % v3) -
2815 ((&1 - (v' + w')) % v1 + v' % v2 + w' % v3) =
2816 ( v' - v ) % ( v1 - v2 ) + ( w' - w ) % ( v1 - v3 ) `] THEN REPEAT STRIP_TAC
2817 THEN ASM_SIMP_TAC[DOT_RADD; DOT_RMUL; ZERO_NEUTRAL]);;
2822 let DIST_EQ_IMP_OTHORGONAL = prove(` ! a b p q. dist (p,a) = dist (p,b) /\ dist (q,a) = dist(q,b)
2823 ==> ( p - q ) dot ( a - b ) = &0 `,
2824 REWRITE_TAC[MONG7_ROI; DOT_LSUB] THEN REAL_ARITH_TAC);;
2826 let NOT_COPLANAR_IMP_NOT_COLLINEAR =
2827 MATCH_MP (MESON[]` (a ==> b) ==> ~ b ==> ~ a `) (SPEC_ALL COLLINEAR_IMP_COPLANAR);;
2830 let PVLJZLA = prove( `! (v1:real^3) v2 v3 v4.
2831 let s = {v1, v2, v3, v4} in
2833 ==> (circumcenter s IN conv0 s <=>
2834 orientation s v1 (\x. &0 < x) /\
2835 orientation s v2 (\x. &0 < x) /\
2836 orientation s v3 (\x. &0 < x) /\
2837 orientation s v4 (\x. &0 < x))`,
2838 REWRITE_TAC[orientation; affsign] THEN
2841 REWRITE_TAC[lin_combo] THEN
2842 REWRITE_TAC[SET_RULE` s DIFF {a} UNION {a} = s UNION {a} `;
2843 SET_RULE` {a,b,c,d} UNION {a} = {a,b,c,d} /\
2844 {a,b,c,d} UNION {b} = {a,b,c,d} /\
2845 {a,b,c,d} UNION {c} = {a,b,c,d} /\
2846 {a,b,c,d} UNION {d} = {a,b,c,d}`] THEN
2847 REWRITE_TAC[MESON[]`a = b /\ c /\ d <=> c /\ d /\ b = a `] THEN
2848 REWRITE_TAC[SET_RULE` (!w. {v1} w ==> &0 < f w) /\
2849 sum {v1, v2, v3, v4} f = &1 /\ l
2850 <=> (!w. w IN {v1,v2,v3,v4} ==> {v1} w ==> &0 < f w) /\
2851 sum {v1, v2, v3, v4} f = &1 /\ l `;
2852 SET_RULE` (!w. {v2} w ==> &0 < f w) /\
2853 sum {v1, v2, v3, v4} f = &1 /\ l
2854 <=> (!w. w IN {v1,v2,v3,v4} ==> {v2} w ==> &0 < f w) /\
2855 sum {v1, v2, v3, v4} f = &1 /\ l `;
2856 SET_RULE` (!w. {v2} w ==> &0 < f w) /\
2857 sum {v1, v2, v3, v4} f = &1 /\ l
2858 <=> (!w. w IN {v1,v2,v3,v4} ==> {v2} w ==> &0 < f w) /\
2859 sum {v1, v2, v3, v4} f = &1 /\ l `;
2860 SET_RULE` (!w. {v3} w ==> &0 < f w) /\
2861 sum {v1, v2, v3, v4} f = &1 /\ l
2862 <=> (!w. w IN {v1,v2,v3,v4} ==> {v3} w ==> &0 < f w) /\
2863 sum {v1, v2, v3, v4} f = &1 /\ l `;
2864 SET_RULE` (!w. {v4} w ==> &0 < f w) /\
2865 sum {v1, v2, v3, v4} f = &1 /\ l
2866 <=> (!w. w IN {v1,v2,v3,v4} ==> {v4} w ==> &0 < f w) /\
2867 sum {v1, v2, v3, v4} f = &1 /\ l `] THEN
2868 SIMP_TAC[AFFINE_HULL_FINITE_STEP_GEN;
2869 REAL_ARITH `&0 < x /\ &0 < y ==> &0 < x + y`;
2870 REAL_ARITH ` &0 < x ==> &0 < x / &2`;
2871 FINITE_INSERT; CONJUNCT1 FINITE_RULES
2872 ; RIGHT_EXISTS_AND_THM] THEN
2873 NHANH (NOT_COPLANAR_IMP_CARD4) THEN
2874 SIMP_TAC[IN_ACT_SING; CARD4; IN_SET3; DE_MORGAN_THM] THEN
2875 REWRITE_TAC[REAL_ARITH` a - b = c <=> a = b + c `; ZERO_NEUTRAL;
2876 VECTOR_ARITH`(a:real^N) - b = c <=> a = b + c `; VECTOR_ARITH` x +
2878 REWRITE_TAC[CONV0_4; IN_ELIM_THM] THEN
2879 NHANH (SPEC ` circumcenter {(v1:real^3), v2, v3, v4} ` ( GEN `v:real^3` (SPEC_ALL COEFS_4))) THEN
2883 UNDISCH_TAC ` !ta tb tc td.
2884 circumcenter {v1, v2, v3, v4} =
2885 ta % v1 + tb % v2 + tc % v3 + td % v4 /\
2886 ta + tb + tc + td = &1
2887 ==> ta = COEF4_1 v1 v2 v3 v4 (circumcenter {v1, v2, v3, v4}) /\
2888 tb = COEF4_2 v1 v2 v3 v4 (circumcenter {v1, v2, v3, v4}) /\
2889 tc = COEF4_3 v1 v2 v3 v4 (circumcenter {v1, v2, v3, v4}) /\
2890 td = COEF4_4 v1 v2 v3 v4 (circumcenter {v1, v2, v3, v4})` THEN
2891 REWRITE_TAC[MESON[]`&0 < v /\ ( ? b . P v b ) <=>
2892 (? b. &0 < v /\ P v b ) `] THEN
2893 REWRITE_TAC[MESON[]` &1 = a /\ aa = b <=> a = &1 /\ b = aa `] THEN
2894 ABBREV_TAC ` (vv:real^3) = circumcenter {v1, v2, v3, v4} ` THEN
2895 ABBREV_TAC ` a1 = COEF4_1 v1 v2 v3 v4 vv ` THEN
2896 ABBREV_TAC ` a2 = COEF4_2 v1 v2 v3 v4 vv ` THEN
2897 ABBREV_TAC ` a3 = COEF4_3 v1 v2 v3 v4 vv ` THEN
2898 ABBREV_TAC ` a4 = COEF4_4 v1 v2 v3 v4 vv ` THEN PHA THEN
2899 IMP_TAC THEN STRIP_TAC THEN STRIP_TAC THEN
2900 REPLICATE_TAC 4 (FIRST_X_ASSUM MP_TAC) THEN PHA THEN
2901 NHANH (MESON[]`(!ta tb tc td.
2902 vv = ta % v1 + tb % v2 + tc % v3 + td % v4 /\ ta + tb + tc + td = &1
2903 ==> ta = a1 /\ tb = a2 /\ tc = a3 /\ td = a4) /\
2905 v + v' + v'' + v''' = &1 /\
2906 v % v1 + v' % v2 + v'' % v3 + v''' % v4 = vv /\
2909 v + v' + v'' + v''' = &1 /\
2910 v % v1 + v' % v2 + v'' % v3 + v''' % v4 = vv) /\
2913 v + v' + v'' + v''' = &1 /\
2914 v % v1 + v' % v2 + v'' % v3 + v''' % v4 = vv) /\
2917 v + v' + v'' + v''' = &1 /\
2918 v % v1 + v' % v2 + v'' % v3 + v''' % v4 = vv) ==>
2919 &0 < v' /\ &0 < v'' /\ &0 < v''' `) THEN MESON_TAC[]]);;
2924 let IMP_IN_AFF_LT = prove(`CARD {v1, v2, v3, v4} = 4 ==> ( (?v v' v'' v'''.
2926 &1 = v + v' + v'' + v''' /\ vv =
2927 v % v1 + v' % v2 + v'' % v3 + v''' % v4) <=>
2928 vv IN aff_lt {v2,v3,v4} {v1} ) `,
2929 REWRITE_TAC[CARD4; IN_SET3; DE_MORGAN_THM] THEN SIMP_TAC[AFF_GES_GTS; IN_ELIM_THM]
2930 THEN REMOVE_TAC THEN
2931 MESON_TAC[REAL_ARITH` a + b + c + d = d + a + b + c `;
2932 VECTOR_ARITH` a + b + c + d = d + a + b + (c:real^N)`]);;
2935 let SQRT4_EQ2 = prove(` sqrt ( &4 ) = &2 `,
2936 REWRITE_TAC[REAL_ARITH` &4 = &2 pow 2 `] THEN
2937 MESON_TAC[POW_2_SQRT; REAL_ARITH` &0 <= &2 `]);;
2940 let RHUFIIB = prove( ` !x12 x13 x14 x23 x24 x34.
2941 rho_ij' x12 x13 x14 x23 x24 x34 * ups_x x34 x24 x23 =
2942 chi x12 x13 x14 x23 x24 x34 pow 2 +
2943 &4 * delta x12 x13 x14 x23 x24 x34 * x34 * x24 * x23 `,
2944 REWRITE_TAC[rho_ij'; chi; delta; ups_x] THEN REAL_ARITH_TAC);;
2948 let SHOGYBS = prove(` ! x1 x2 x3 (x4:real^3).
2949 ~coplanar_alt {x1,x2,x3,x4} ==>
2950 let x12 = dist (x1,x2) pow 2 in
2951 let x13 = dist (x1,x3) pow 2 in
2952 let x14 = dist (x1,x4) pow 2 in
2953 let x23 = dist (x2,x3) pow 2 in
2954 let x24 = dist (x2,x4) pow 2 in
2955 let x34 = dist (x3,x4) pow 2 in
2956 &0 <= rho_ij' x12 x13 x14 x23 x24 x34 `,
2957 ONCE_REWRITE_TAC[SET_RULE` {v1,v2,v3,v4} = {v2,v3,v4,v1} `] THEN
2958 NHANH (NOT_COPLANAR_IMP_NOT_COLLINEAR) THEN
2959 ONCE_REWRITE_TAC[GSYM (SET_RULE` {v1,v2,v3,v4} = {v2,v3,v4,v1} `)] THEN
2960 REWRITE_TAC[NOT_COL_EQ_UPS_X_POS] THEN REPEAT GEN_TAC THEN
2961 MP_TAC (SPEC_ALL DELTA_POS_4POINTS) THEN
2962 REPEAT LET_TAC THEN MP_TAC (SPEC_ALL RHUFIIB) THEN DOWN_TAC THEN
2963 NHANH (MESON[REAL_LE_POW_2]` a pow 2 = b ==> &0 <= b `) THEN DAO THEN
2964 SIMP_TAC[UPS_X_SYM] THEN
2965 REWRITE_TAC[MESON[REAL_FIELD` &0 < a ==> (b * a = c <=> b = c / a )`]`
2966 &0 < a /\a1 /\a2/\ b * a = c /\l <=> &0 < a /\a1 /\a2/\ b = c / a /\ l `] THEN
2967 MP_TAC (REAL_ARITH` &0 <= &4 `) THEN PHA THEN
2968 NHANH (MESON[REAL_LT_IMP_LE; REAL_LE_DIV;
2969 REAL_LE_MUL; REAL_LE_ADD; REAL_LE_POW_2]` &0 <= &4 /\
2970 &0 < ups_x x23 x24 x34 /\a1/\
2971 &0 <= delta x12 x13 x14 x23 x24 x34 /\ a2 /\
2972 &0 <= x34 /\a3 /\ &0 <= x24 /\a4 /\ &0 <= x23 /\a5/\
2973 &0 <= x14 /\a6 /\ &0 <= x13 /\a7 /\a8 /\ &0 <= x12 ==>
2974 &0 <= &4 * delta x12 x13 x14 x23 x24 x34 * x34 * x24 * x23 `) THEN
2975 ABBREV_TAC ` aaa = &4 * delta x12 x13 x14 x23 x24 x34 * x34 * x24 * x23 ` THEN STRIP_TAC THEN
2976 FIRST_X_ASSUM MP_TAC THEN UNDISCH_TAC ` rho_ij' x12 x13 x14 x23 x24 x34 =
2977 (chi x12 x13 x14 x23 x24 x34 pow 2 + aaa) / ups_x x23 x24 x34 ` THEN
2978 UNDISCH_TAC`&0 < ups_x x23 x24 x34` THEN MESON_TAC[REAL_LT_IMP_LE; REAL_LE_DIV;
2979 REAL_LE_MUL; REAL_LE_ADD; REAL_LE_POW_2]);;
2982 (* le 86 . GDRQXLG *)
2985 let GDRQXLG = prove(` ! v1 v2 v3 (v4:real^3).
2986 let s = {v1, v2, v3, v4} in
2987 let x12 = dist (v1,v2) pow 2 in
2988 let x13 = dist (v1,v3) pow 2 in
2989 let x14 = dist (v1,v4) pow 2 in
2990 let x23 = dist (v2,v3) pow 2 in
2991 let x24 = dist (v2,v4) pow 2 in
2992 let x34 = dist (v3,v4) pow 2 in
2993 CARD s = 4 /\ ~coplanar_alt s
2995 sqrt ( rho_ij' x12 x13 x14 x23 x24 x34) /
2996 (&2 * sqrt (delta x12 x13 x14 x23 x24 x34))`,
2997 REPEAT GEN_TAC THEN REPEAT LET_TAC THEN EXPAND_TAC "s" THEN
2998 NHANH (NOT_COPLANAR_IMP_RADV_PROPERTIES) THEN
2999 NHANH (REWRITE_RULE[RIGHT_FORALL_IMP_THM] (GEN `p:real^3` PROVE_DIST_FROM_V1 )) THEN
3000 NHANH (REWRITE_RULE[RIGHT_FORALL_IMP_THM] (GEN `p:real^3` PROVE_EQ_DIST_FROM4 ) ) THEN
3001 REWRITE_TAC[GSYM POS_EQ_NOT_COPLANANR] THEN
3002 NHANH (REAL_ARITH` &0 < a ==> ~( a = &0 )`) THEN
3003 NHANH (PROVE_IN_AFFINE_HULL_4 ) THEN LET_TR THEN
3004 REWRITE_TAC[MESON[]`(!x. x = a ==> p x) <=> p a `] THEN
3005 ABBREV_TAC `taa = (&1 / (&2 *
3006 delta (dist (v1,v2) pow 2) (dist (v1,v3) pow 2) (dist (v1,v4) pow 2)
3007 (dist (v2,v3) pow 2)
3008 (dist (v2,v4) pow 2)
3009 (dist (v3,v4) pow 2)) %
3010 (chi (dist (v1,v2) pow 2) (dist (v1,v3) pow 2) (dist (v1,v4) pow 2)
3011 (dist (v2,v3) pow 2)
3012 (dist (v2,v4) pow 2)
3013 (dist (v3,v4) pow 2) %
3015 chi (dist (v1,v2) pow 2) (dist (v2,v4) pow 2) (dist (v2,v3) pow 2)
3016 (dist (v1,v4) pow 2)
3017 (dist (v1,v3) pow 2)
3018 (dist (v3,v4) pow 2) %
3020 chi (dist (v3,v4) pow 2) (dist (v1,v3) pow 2) (dist (v2,v3) pow 2)
3021 (dist (v1,v4) pow 2)
3022 (dist (v2,v4) pow 2)
3023 (dist (v1,v2) pow 2) %
3025 chi (dist (v3,v4) pow 2) (dist (v2,v4) pow 2) (dist (v1,v4) pow 2)
3026 (dist (v2,v3) pow 2)
3027 (dist (v1,v3) pow 2)
3028 (dist (v1,v2) pow 2) %
3030 REWRITE_TAC[ POS_EQ_NOT_COPLANANR] THEN NGOAC THEN
3031 NHANH (SPEC_ALL UNIQUE_EXISISTING_PROPERTY_C4 ) THEN
3032 REWRITE_TAC[FORALL_IN_CLAUSES] THEN ABBREV_TAC ` abc = &1 / &2 *
3033 rho_ij' (dist (v1,v2) pow 2) (dist (v1,v3) pow 2) (dist (v1,v4) pow 2)
3034 (dist (v2,v3) pow 2) (dist (v2,v4) pow 2) (dist (v3,v4) pow 2) /
3036 delta (dist ((v1:real^3),v2) pow 2) (dist (v1,v3) pow 2) (dist (v1,v4) pow 2)
3037 (dist (v2,v3) pow 2)
3038 (dist (v2,v4) pow 2)
3039 (dist (v3,v4) pow 2)) ` THEN REWRITE_TAC[dist3] THEN
3040 NHANH (MESON[POW_2_SQRT; DIST_POS_LE]` dist (taa,v2) pow 2 = a ==>
3041 dist(taa,v2) = sqrt a `) THEN PHA THEN
3042 NHANH (MESON[]`(!p. p IN affine hull {v1, v2, v3, v4} /\
3043 (?r. r = dist (p,v1) /\
3047 ==> p = circumcenter {v1, v2, v3, v4}) /\ a11 /\
3048 taa IN affine hull {v1, v2, v3, v4} /\
3049 dist (taa,v2) pow 2 = abc /\
3050 dist (taa,v2) = sqrt abc /\
3051 dist (taa,v3) pow 2 = abc /\
3052 dist (taa,v3) = sqrt abc /\
3053 dist (taa,v4) pow 2 = abc /\
3054 dist (taa,v4) = sqrt abc /\
3055 dist (taa,v1) pow 2 = abc /\
3056 dist (taa,v1) = sqrt abc /\ lll ==> taa = circumcenter {v1, v2, v3, v4} `) THEN
3057 NHANH (SET_RULE ` (!w. {v1, v2, v3, v4} w ==> P w ) ==> P v1 `) THEN PHA THEN
3058 REWRITE_TAC[MESON[]` a = dist (aa,b) /\ ta = aa <=> ta = aa /\ a = dist (ta,b) `] THEN
3059 NHANH (MESON[]` a = b /\ a1 /\ a2 /\ c = a ==> c = b `) THEN NHANH (SPEC_ALL SHOGYBS) THEN
3060 MP_TAC (SPECL [`v1:real^3`;` v2:real^3`;`v3:real^3`;`v4:real^3`]
3061 DELTA_POS_4POINTS) THEN REPEAT LET_TAC THEN IMP_TAC THEN REPEAT (FIRST_X_ASSUM MP_TAC) THEN
3062 REWRITE_TAC[MESON[]` a = b ==> P a <=> a = b ==> P b `] THEN
3063 REWRITE_TAC[MESON[]` a = b ==> a = c <=> a = b ==> c = b `] THEN REPEAT STRIP_TAC THEN
3064 UNDISCH_TAC ` &1 / &2 * rho_ij' x12 x13 x14 x23 x24 x34 / (&2 * delta x12 x13 x14 x23 x24 x34) =
3065 abc ` THEN UNDISCH_TAC ` &0 <= rho_ij' x12 x13 x14 x23 x24 x34 ` THEN
3066 ABBREV_TAC ` edl = delta x12 x13 x14 x23 x24 x34 ` THEN UNDISCH_TAC` &0 <= edl ` THEN
3067 SIMP_TAC[REAL_ARITH` &0 <= &4 `; GSYM SQRT_MUL; GSYM SQRT4_EQ2] THEN
3068 SIMP_TAC[REAL_ARITH` &0 <= &4 `; REAL_LE_MUL; GSYM SQRT_DIV] THEN
3069 REWRITE_TAC[SQRT4_EQ2] THEN MESON_TAC[REAL_FIELD` &1 / &2 * x34 / (&2 * edl) = x34 / (&4 * edl)`]);;
3073 end;; (* end of module *)