1 (* ========================================================================== *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
5 (* Author: Nguyen Quang Truong *)
7 (* ========================================================================== *)
11 flyspeck_needs "general/sphere.hl";;
12 flyspeck_needs "leg/geomdetail.hl";;
13 flyspeck_needs "leg/affprops.hl";;
14 flyspeck_needs "leg/cayleyR_def.hl";;
16 module Collect_geom = struct
21 global replace rho->rho_x
23 This file gives an alternative def of rho_ij, delta, chi.
24 These should be reconciled with main flyspeck library
29 let packing = Sphere.packing;;
30 let eta_x = Sphere.eta_x;;
31 let eta_y = Sphere.eta_y;;
32 let aff = Sphere.aff;; (* also appears in Geomdetail *)
33 let line = Sphere.line;;
34 let circumcenter = Sphere.circumcenter;;
35 let radV = Sphere.radV;;
37 let conv = Geomdetail.conv;;
38 let CONV0_SET2 = Geomdetail.CONV0_SET2;;
39 let OR_IMP_EX = Geomdetail.OR_IMP_EX;;
40 let CONV_SET3 = Geomdetail.CONV_SET3;;
41 let INTERS_SUBSET = Geomdetail.INTERS_SUBSET;;
42 let DOT_SUB_ADD = Geomdetail.DOT_SUB_ADD;;
43 let trg_dist3_sym = Geomdetail.trg_dist3_sym;;
44 let DIST_LT_HALF_PLANE = Geomdetail.DIST_LT_HALF_PLANE;;
46 let simp_def2 = Affprops.affprops;;
48 let cayleyR = Cayleyr.cayleyR;;
50 let BY = Hales_tactic.BY;;
54 (* dist3 is deprecated *)
55 let dist3 = new_definition `dist3 (v:real^3) w = dist(v,w)`;;
57 let ups_x = new_definition ` ups_x x1 x2 x6 =
58 --x1 * x1 - x2 * x2 - x6 * x6 +
64 let rho_ij = new_definition ` rho_ij (x12 :real) x13 x14 x23 x24 x34 =
65 --(x14 * x14 * x23 * x23) -
66 x13 * x13 * x24 * x24 -
67 x12 * x12 * x34 * x34 +
69 (x12 * x14 * x23 * x34 +
70 x12 * x13 * x24 * x34 +
71 x13 * x14 * x23 * x24) `;;
74 let rho_ij'_rho_x = new_definition `rho_ij' x1 x2 x3 x6 x5 x4 = rho_x x1 x2 x3 x4 x5 x6`;;
76 let rho_ij' = prove_by_refinement(
77 `!x12 x34 x13 x14 x23 x24. rho_ij' (x12 :real) x13 x14 x23 x24 x34 =
78 --(x14 * x14 * x23 * x23) -
79 x13 * x13 * x24 * x24 -
80 x12 * x12 * x34 * x34 +
82 (x12 * x14 * x23 * x34 +
83 x12 * x13 * x24 * x34 +
84 x13 * x14 * x23 * x24)`,
87 (REWRITE_TAC[rho_ij'_rho_x;Sphere.rho_x]);
92 let chi = new_definition ` chi x12 x13 x14 x23 x24 x34 =
99 &2 * x23 * x24 * x34 -
104 let delta = new_definition ` delta x12 x13 x14 x23 x24 x34 =
105 --(x12 * x13 * x23) -
109 x12 * x34 * (--x12 + x13 + x14 + x23 + x24 - x34) +
110 x13 * x24 * (x12 - x13 + x14 + x23 - x24 + x34 ) +
111 x14 * x23 * ( x12 + x13 - x14 - x23 + x24 + x34 ) `;;
113 let eta_v = new_definition ` eta_v v1 v2 (v3: real^N) =
114 let e1 = dist (v2, v3) in
115 let e2 = dist (v1, v3) in
116 let e3 = dist (v2, v1) in
117 e1 * e2 * e3 / sqrt ( ups_x (e1 pow 2 ) ( e2 pow 2) ( e3 pow 2 ) ) `;;
119 let max_real = new_definition(`max_real x y =
120 if (y < x) then x else y`);;
122 let max_real3 = new_definition ` max_real3 x y z = max_real (max_real x y ) z `;;
124 let ups_x_pow2 = new_definition` ups_x_pow2 x y z = ups_x ( x*x ) ( y * y) ( z * z)`;;
126 let plane_norm = new_definition `
128 (?n v0. ~(n = vec 0) /\ p = {v | n dot (v - v0) = &0}) `;;
131 let delta_x34 = new_definition ` delta_x34 x12 x13 x14 x23 x24 x34 =
145 let plane_3p = new_definition `plane_3p (a:real^3) b c =
146 {x | ~collinear {a, b, c} /\
147 (?ta tb tc. ta + tb + tc = &1 /\ x = ta % a + tb % b + tc % c)}`;;
150 (* end new_definition *)
152 (* NGUYEN DUC PHUONG *)
153 (* Definition of Cayley Menger square cm3 *)
156 let cm3_ups_x = new_definition `!(v1:real^3) (v2:real^3) (v3:real^3).
158 (((v2 - v1)$2 * (v3 - v1)$3 ) - ((v2 - v1)$3 * (v3 - v1)$2)) pow 2 +
159 (((v2 - v1)$3 * (v3 - v1)$1 ) - ((v2 - v1)$1 * (v3 - v1)$3)) pow 2 +
160 (((v2 - v1)$1 * (v3 - v1)$2 ) - ((v2 - v1)$2 * (v3 - v1)$1)) pow 2 `;;
163 (* Nguyen Tuyen Hoang, Nguyen Duc Phuong *)
165 (* The polynomial ups can be expressed as a Cayley- Menger square *)
167 let lemma_cm3 = prove (`!(x:real^3) y.
168 (x-y)$1 = x$1 - y$1 /\ (x-y)$2 = x$2 - y$2 /\ (x-y)$3 = x$3 - y$3`,
170 (REPEAT GEN_TAC) THEN (REPEAT CONJ_TAC) THENL
171 [(MESON_TAC[VECTOR_SUB_COMPONENT;DIMINDEX_3;ARITH_RULE `1 <= 1 /\ 1 <= 3`]);
172 (MESON_TAC[VECTOR_SUB_COMPONENT;DIMINDEX_3;ARITH_RULE `1 <= 2 /\ 2 <= 3`]);
173 (MESON_TAC[VECTOR_SUB_COMPONENT;DIMINDEX_3;ARITH_RULE `1 <= 3 /\ 3 <= 3`])]);;
175 let lemma7 = prove ( `! (v1 : real ^3)(v2: real^3)(v3:real^3).
177 ups_x (norm (v1 -v2) pow 2) (norm (v2 -v3) pow 2) (norm (v3 -v1) pow 2) / &4`,
179 (REPEAT GEN_TAC) THEN
180 (REWRITE_TAC[cm3_ups_x; ups_x]) THEN
181 (REWRITE_TAC[GSYM DOT_SQUARE_NORM;DOT_3;REAL_POW_2]) THEN
182 (REWRITE_TAC[lemma_cm3]) THEN
185 let pow_g = prove ( `! (x:real). &0 <= x pow 2`,
186 GEN_TAC THEN REWRITE_TAC[REAL_POW_2; REAL_LE_SQUARE]);;
188 let lemma8 = prove ( `! (v1:real^3)(v2:real^3)(v3:real^3).
189 &0 <= ups_x (norm (v1 - v2) pow 2)(norm (v2 - v3) pow 2)(norm (v3 - v1) pow 2)`,
191 THEN (MATCH_MP_TAC (REAL_ARITH `&0 <= a/ &4 ==> &0 <= a `))
192 THEN (REWRITE_TAC[GSYM lemma7])
193 THEN (REWRITE_TAC[cm3_ups_x])
195 THEN (ABBREV_TAC `(a:real) = (((v2:real^3) - v1)$2 * (v3 - v1)$3 - (v2 - v1)$3 * (v3 - v1)$2) pow 2`)
196 THEN (FIRST_X_ASSUM ((LABEL_TAC "1") o GSYM))
197 THEN (ABBREV_TAC `(b:real) = (((v2:real^3) - v1)$3 * (v3 - v1)$1 - (v2 - v1)$1 * (v3 - v1)$3) pow 2`)
198 THEN (FIRST_X_ASSUM((LABEL_TAC "2") o GSYM))
199 THEN (ABBREV_TAC `(c:real) = (((v2:real^3) - v1)$1 * (v3 - v1)$2 - (v2 - v1)$2 * (v3 - v1)$1) pow 2`)
200 THEN (FIRST_X_ASSUM((LABEL_TAC "3") o GSYM))
202 THEN (MATCH_MP_TAC (SPEC_ALL REAL_LE_ADD))
204 THEN (ASM_REWRITE_TAC[pow_g])
205 THEN (MATCH_MP_TAC (SPEC_ALL REAL_LE_ADD))
207 THEN (ASM_REWRITE_TAC[pow_g]));;
212 let GONTONG = REAL_RING ` ((a + b) + c = a + b + c ) `;;
214 let SUB_SUM_SUB = REAL_RING ` (a - ( b + c ) = a - b - c )/\( a - (b- c) = a - b + c )` ;;
217 let JVUNDLC = prove(`!a b c s.
219 ==> &16 * s * (s - a) * (s - b) * (s - c) =
220 ups_x (a pow 2) (b pow 2) (c pow 2)`, SIMP_TAC [ ups_x] THEN
221 REWRITE_TAC[REAL_FIELD` a / &2 - b = ( a - &2 * b ) / &2 `] THEN
222 REWRITE_TAC[REAL_FIELD ` &16 * ( a / &2 ) * ( b / &2 ) * (c / &2 ) *
223 ( d / &2 ) = a * b * c * d `] THEN REAL_ARITH_TAC);;
227 [NOT_IN_EMPTY; IN_UNIV; IN_UNION; IN_INTER; IN_DIFF; IN_INSERT;
228 IN_DELETE; IN_REST; IN_INTERS; IN_UNIONS; IN_IMAGE] in
229 let allthms = basicthms @ map (REWRITE_RULE[IN]) basicthms @
232 TRY(POP_ASSUM_LIST(MP_TAC o end_itlist CONJ)) THEN
233 REPEAT COND_CASES_TAC THEN
234 REWRITE_TAC[EXTENSION; SUBSET; PSUBSET; DISJOINT; SING] THEN
235 REWRITE_TAC allthms in
238 (if ths = [] then ALL_TAC else MP_TAC(end_itlist CONJ ths)) THEN
241 let SET_RULE tm = prove(tm,SET_TAC[]);;
243 (* some TRUONG TACTICS *)
245 let PHA = REWRITE_TAC[ MESON[] ` (a/\b)/\c <=> a/\ b /\ c `];;
247 let NGOAC = REWRITE_TAC[ MESON[] ` a/\b/\c <=> (a/\b)/\c `];;
249 let DAO = NGOAC THEN REWRITE_TAC[ MESON[]` a /\ b <=> b /\ a`];;
251 let PHAT = REWRITE_TAC[ MESON[] ` (a\/b)\/c <=> a\/b\/c `];;
253 let NGOACT = REWRITE_TAC[ GSYM (MESON[] ` (a\/b)\/c <=> a\/b\/c `)];;
255 let KHANANG = PHA THEN REWRITE_TAC[ MESON[]` ( a\/ b ) /\ c <=> a /\ c \/ b /\ c `] THEN
256 REWRITE_TAC[ MESON[]` a /\ ( b \/ c ) <=> a /\ b \/ a /\ c `];;
258 let ATTACH thm = MATCH_MP (MESON[]` ! a b. ( a ==> b ) ==> ( a <=> a /\ b )`) thm;;
260 let NHANH tm = ONCE_REWRITE_TAC[ ATTACH (tm)];;
261 let STRIP_TR = REPEAT STRIP_TAC THEN REPEAT (FIRST_X_ASSUM MP_TAC)
262 THEN REWRITE_TAC[IMP_IMP] THEN PHA;;
265 let elimin = REWRITE_RULE[IN];;
267 let CONV_EM = prove(`conv {} = {}:real^A->bool`,
268 REWRITE_TAC[conv;sgn_ge;affsign;UNION_EMPTY;FUN_EQ_THM;elimin
269 NOT_IN_EMPTY;lin_combo;SUM_CLAUSES]
270 THEN REAL_ARITH_TAC);;
272 let CONV_SING = prove(`!u. conv {u:real^A} = {u}`,
273 REWRITE_TAC[conv;sgn_ge;affsign;FUN_EQ_THM;UNION_EMPTY;lin_combo;SUM_SING;VSUM_SING;
274 elimin IN_SING] THEN REPEAT GEN_TAC THEN
275 REWRITE_TAC[TAUT `(p <=> q) = ((p ==> q) /\ (q ==> p))`] THEN
276 REPEAT STRIP_TAC THENL [ASM_MESON_TAC[VECTOR_MUL_LID];
277 ASM_REWRITE_TAC[]] THEN EXISTS_TAC `\ (v:real^A). &1` THEN
278 MESON_TAC[VECTOR_MUL_LID;REAL_ARITH `&0 <= &1`] );;
280 let IN_ACT_SING = SET_RULE `! a x. ({a} x <=> a = x ) /\ ( x IN {a} <=> x = a) /\ {a} a`;;
282 let IN_SET2 = SET_RULE `!a b x.
283 (x IN {a, b} <=> x = a \/ x = b) /\ ({a, b} x <=> x = a \/ x = b)`;;
285 let SUM_DIS2 = prove(`! x y f. ~(x=y) ==> sum {x,y} f = f x + f y `,REWRITE_TAC[
287 <=> ~(x IN {y})`] THEN MESON_TAC[ FINITE_RULES; SUM_CLAUSES; SUM_SING]);;
290 let VSUM_DIS2 = prove(` ! x y f. ~(x=y) ==> vsum {x,y} f = f x + f y`, REWRITE_TAC[
292 <=> ~(x IN {y})`] THEN MESON_TAC[ FINITE_RULES; VSUM_CLAUSES; VSUM_SING]);;
294 let NOV10 = prove(` ! x y. (x = y
296 (?a b. &0 <= a /\ &0 <= b /\ a + b = &1 /\ x = a % y + b % y))) `,
297 REWRITE_TAC[GSYM VECTOR_ADD_RDISTRIB] THEN
298 REWRITE_TAC[ MESON[VECTOR_MUL_LID]` a + b = &1 /\ x = (a + b) % y <=> a + b = &1 /\
299 x = y`]THEN REPEAT GEN_TAC THEN DISCH_TAC THEN GEN_TAC THEN NGOAC THEN
300 REWRITE_TAC[LEFT_EXISTS_AND_THM] THEN MATCH_MP_TAC (MESON[]` a ==> ( x = y <=> a /\
301 y = x )`)THEN EXISTS_TAC `&0` THEN EXISTS_TAC ` &1` THEN REAL_ARITH_TAC);;
304 let TRUONG_LEMMA = prove
306 (?f. x' = f x % x + f y % y /\ (&0 <= f x /\ &0 <= f y) /\
308 (?a b. &0 <= a /\ &0 <= b /\ a + b = &1 /\ x' = a % x + b % y)` ,
309 REPEAT GEN_TAC THEN EQ_TAC
310 THENL [MESON_TAC[]; STRIP_TAC] THEN
311 ASM_CASES_TAC `y:real^N = x` THENL
312 [EXISTS_TAC `\x:real^N. &1 / &2`;
313 EXISTS_TAC `\u:real^N. if u = x then (a:real) else b`] THEN
314 ASM_REWRITE_TAC[GSYM VECTOR_ADD_RDISTRIB] THEN
315 CONV_TAC REAL_RAT_REDUCE_CONV);;
317 let CONV_SET2 = prove(` ! x y:real^A. conv {x,y} = {w | ? a b. &0 <= a /\ &0 <= b /\ a + b = &1 /\
319 ONCE_REWRITE_TAC[ MESON[] ` (! a b. P a b ) <=> ( ! a b. a = b \/ ~( a= b)
321 REWRITE_TAC[ MESON[]` a \/ b ==> c <=> ( a==> c) /\ ( b==> c)`] THEN
322 SIMP_TAC[] THEN REWRITE_TAC[ SET_RULE ` {a,a} = {a}`; CONV_SING; FUN_EQ_THM;
323 IN_ELIM_THM] THEN REWRITE_TAC[ IN_ACT_SING] THEN REWRITE_TAC[NOV10] THEN
324 REWRITE_TAC[conv; sgn_ge; affsign; lin_combo] THEN
325 REWRITE_TAC[UNION_EMPTY; IN_SET2] THEN
326 ONCE_REWRITE_TAC[ MESON[]` ~(x = y) ==> (!x'. (?f. P f x') <=> l x') <=>
327 ~(x = y) ==> (!x'. (?f. ~(x=y) /\ P f x') <=> l x')`] THEN
328 REWRITE_TAC[ MESON[VSUM_DIS2; SUM_DIS2]` ~(x = y) /\x' = vsum {x, y} ff /\ l /\
329 sum {x, y} f = &1 <=> ~(x = y) /\ x' = ff x + ff y /\ l /\ f x + f y = &1 `] THEN
330 REWRITE_TAC[ MESON[]` (!w. w = x \/ w = y ==> &0 <= f w) <=> &0 <= f x /\ &0 <= f y`]
331 THEN ONCE_REWRITE_TAC[ GSYM (MESON[]` ~(x = y) ==> (!x'. (?f. P f x') <=> l x') <=>
332 ~(x = y) ==> (!x'. (?f. ~(x=y) /\ P f x') <=> l x')`)] THEN
333 REPEAT GEN_TAC THEN DISCH_TAC THEN GEN_TAC THEN REWRITE_TAC[ TRUONG_LEMMA]);;
335 let LE_OF_ZPGPXNN = prove(` ! a b v v1 v2 . &0 <= a /\ &0 <= b /\ a + b = &1 /\
336 v = a % v1 + b % v2 ==> dist ( v,v1) + dist (v,v2) = dist(v1,v2)`,
337 SIMP_TAC[dist; REAL_ARITH ` a + b = &1 <=> b = &1 - a `] THEN
338 REWRITE_TAC[VECTOR_ARITH ` (a % v1 + (&1 - a) % v2) - v1 = ( a - &1 )%( v1 - v2)`] THEN
339 REWRITE_TAC[VECTOR_ARITH` (a % v1 + (&1 - a) % v2) - v2 = a % ( v1 - v2) `] THEN
340 SIMP_TAC[NORM_MUL; GSYM REAL_ABS_REFL] THEN REWRITE_TAC[ REAL_ARITH ` abs ( a - &1 )
341 = abs ( &1 - a ) `] THEN REAL_ARITH_TAC);;
343 let LENGTH_EQUA = prove(` ! v v1 v2. v IN conv {v1,v2} ==> dist (v,v1) +
344 dist (v,v2) = dist (v1,v2) `,REWRITE_TAC[CONV_SET2; IN_ELIM_THM] THEN
345 MESON_TAC[LE_OF_ZPGPXNN]);;
348 let ZPGPXNN = prove(`!v1 v2 v. dist (v1,v2) < dist (v,v1) + dist (v,v2) ==>
349 ~(v IN conv {v1, v2})`,
350 REWRITE_TAC[MESON[] `a ==> ~ b <=> ~(a /\ b )`] THEN REWRITE_TAC[CONV_SET2; IN_ELIM_THM]
351 THEN MESON_TAC[LE_OF_ZPGPXNN; REAL_ARITH ` a < b ==> ~ ( a = b ) `]);;
353 let REDUCE_T2 = MESON[]` !P Q.
354 (!v1 v2 v3 t1 t2 t3. P v1 t1 v2 t2 v3 t3 <=> P v2 t2 v1 t1 v3 t3) /\
355 (!v1 v2 v3. Q v1 v2 v3 <=> Q v2 v1 v3) /\
357 ~(t1 = &0 /\ t3 = &0) /\ P v1 t1 v2 t2 v3 t3 ==> Q v1 v2 v3)
358 ==> (!v1 v2 v3 t1 t2 t3.
359 ~(t1 = &0 /\ t2 = &0 /\ t3 = &0) /\ P v1 t1 v2 t2 v3 t3
362 let VEC_PER2_3 = VECTOR_ARITH `((a:real^N ) + b + c = b + a + c)/\
363 ( (a:real^N ) + b + c = c + b + a )`;;
364 let PER2_IN3 = SET_RULE ` {a,b,c} = {b,a,c} /\ {a,b,c} = {c,b,a}`;;
366 let REDUCE_T3 = MESON[]`!P Q.
367 (!v1 v2 v3 t1 t2 t3. P v1 t1 v2 t2 v3 t3 <=> P v3 t3 v2 t2 v1 t1) /\
368 (!v1 v2 v3. Q v1 v2 v3 <=> Q v3 v2 v1) /\
369 (!v1 v2 v3 t1 t2 t3. ~(t1 = &0) /\ P v1 t1 v2 t2 v3 t3 ==> Q v1 v2 v3)
370 ==> (!v1 v2 v3 t1 t2 t3.
371 ~(t1 = &0 /\ t3 = &0) /\ P v1 t1 v2 t2 v3 t3 ==> Q v1 v2 v3)`;;
373 let SUB_PACKING = prove(`!sub s.
374 packing s /\ sub SUBSET s
375 ==> (!x y. x IN sub /\ y IN sub /\ ~(x = y) ==> &2 <= dist3 x y)`,
376 REWRITE_TAC[ packing; GSYM dist3] THEN SET_TAC[]);;
380 SET_RULE `{a,b} = {c,d} <=> a = c /\ b = d \/ a = d /\ b = c`;;
382 let IN_SET3 = SET_RULE ` x IN {a,b,c} <=> x = a \/ x = b \/ x = c `;;
383 let IN_SET4 = SET_RULE ` x IN {a,b,c,d} <=> x = a \/ x = b \/ x = c \/ x = d `;;
386 let SGFCDZO = prove(`! (v1:real^3) v2 v3 t1 t2 t3.
387 t1 % v1 + t2 % v2 + t3 % v3 = vec 0 /\
389 ~(t1 = &0 /\ t2 = &0 /\ t3 = &0)
390 ==> collinear {v1, v2, v3}`,
391 ONCE_REWRITE_TAC[MESON[]` a /\ b/\c <=> c /\ a /\ b `] THEN
392 MATCH_MP_TAC REDUCE_T2 THEN
393 CONJ_TAC THENL [SIMP_TAC[VEC_PER2_3; REAL_ADD_AC]; CONJ_TAC THENL
394 [SIMP_TAC[PER2_IN3]; MATCH_MP_TAC REDUCE_T3]] THEN
395 CONJ_TAC THENL [SIMP_TAC[REAL_ADD_AC; VEC_PER2_3];
396 CONJ_TAC THENL [SIMP_TAC[PER2_IN3]; REWRITE_TAC[]]] THEN
397 REPEAT GEN_TAC THEN REWRITE_TAC[collinear] THEN
398 STRIP_TAC THEN EXISTS_TAC `v2 - (v3:real^3)` THEN
399 ONCE_REWRITE_TAC[MESON[]` x IN s /\ y IN s <=>
400 ( x = y \/ ~ ( x = y))/\ x IN s /\ y IN s `] THEN
401 REWRITE_TAC[IN_SET3] THEN REPEAT GEN_TAC THEN
402 REWRITE_TAC[MESON[]` (a \/ b) /\ c ==> d <=> (a /\ c ==> d) /\ (b /\ c ==> d)`]
403 THEN CONJ_TAC THENL [DISCH_TAC THEN EXISTS_TAC `&0` THEN
404 FIRST_X_ASSUM MP_TAC THEN MATCH_MP_TAC (MESON[]` (a ==> c) ==> a /\ b ==> c `) THEN
405 MESON_TAC[VECTOR_MUL_LZERO; VECTOR_SUB_EQ]; STRIP_TAC] THENL [
409 EXISTS_TAC ` t3 / t1 ` THEN ASM_SIMP_TAC[] THEN STRIP_TR THEN
410 ONCE_REWRITE_TAC[MESON[VECTOR_MUL_LCANCEL]`
411 ~(t1 = &0) /\ a ==> x = y <=> ~(t1 = &0) /\ a ==> t1 % x = t1 % y`] THEN
412 REWRITE_TAC[VECTOR_MUL_ASSOC] THEN SIMP_TAC[REAL_DIV_LMUL] THEN
413 ONCE_REWRITE_TAC[GSYM VECTOR_SUB_EQ] THEN
414 REWRITE_TAC[ VECTOR_ARITH ` ( a + b + (c:real^N) ) - vec 0 = vec 0 <=>
415 a = -- ( b + c ) `; REAL_ARITH` a + b + c = &0 <=> a = -- ( b + c ) `] THEN
416 SIMP_TAC[VECTOR_SUB_LDISTRIB] THEN
417 MESON_TAC[VECTOR_ARITH ` --(t2 % v2 + t3 % v3) - --(t2 + t3) % v2 -
418 (t3 % v2 - t3 % v3) = vec 0`];
420 EXISTS_TAC ` ( -- t2 ) / t1 ` THEN ASM_SIMP_TAC[] THEN STRIP_TR THEN
421 ONCE_REWRITE_TAC[MESON[VECTOR_MUL_LCANCEL]`
422 ~(t1 = &0) /\ a ==> x = y <=> ~(t1 = &0) /\ a ==> t1 % x = t1 % y`] THEN
423 REWRITE_TAC[VECTOR_MUL_ASSOC] THEN SIMP_TAC[REAL_DIV_LMUL] THEN
424 ONCE_REWRITE_TAC[GSYM VECTOR_SUB_EQ] THEN
425 REWRITE_TAC[ VECTOR_ARITH ` ( a + b + (c:real^N) ) - vec 0 = vec 0 <=>
426 a = -- ( b + c ) `; REAL_ARITH` a + b + c = &0 <=> a = -- ( b + c ) `] THEN
427 SIMP_TAC[VECTOR_SUB_LDISTRIB] THEN
428 MESON_TAC[VECTOR_ARITH ` --(t2 % v2 + t3 % v3) - --(t2 + t3) % v3 -
429 (--t2 % v2 - --t2 % v3) = vec 0`];
432 EXISTS_TAC ` ( -- t3) / t1 ` THEN ASM_SIMP_TAC[] THEN STRIP_TR THEN
433 ONCE_REWRITE_TAC[MESON[VECTOR_MUL_LCANCEL]`
434 ~(t1 = &0) /\ a ==> x = y <=> ~(t1 = &0) /\ a ==> t1 % x = t1 % y`] THEN
435 REWRITE_TAC[VECTOR_MUL_ASSOC] THEN SIMP_TAC[REAL_DIV_LMUL] THEN
436 ONCE_REWRITE_TAC[GSYM VECTOR_SUB_EQ] THEN
437 REWRITE_TAC[ VECTOR_ARITH ` ( a + b + (c:real^N) ) - vec 0 = vec 0 <=>
438 a = -- ( b + c ) `; REAL_ARITH` a + b + c = &0 <=> a = -- ( b + c ) `] THEN
439 SIMP_TAC[VECTOR_SUB_LDISTRIB] THEN MESON_TAC[VECTOR_ARITH ` --(t2 + t3) % v2
440 - --(t2 % v2 + t3 % v3) - (--t3 % v2 - --t3 % v3) = vec 0`];
446 EXISTS_TAC ` &1 ` THEN ASM_SIMP_TAC[VECTOR_MUL_LID];
449 EXISTS_TAC ` t2 / t1 ` THEN ASM_SIMP_TAC[] THEN STRIP_TR THEN
450 ONCE_REWRITE_TAC[MESON[VECTOR_MUL_LCANCEL]`
451 ~(t1 = &0) /\ a ==> x = y <=> ~(t1 = &0) /\ a ==> t1 % x = t1 % y`] THEN
452 REWRITE_TAC[VECTOR_MUL_ASSOC] THEN SIMP_TAC[REAL_DIV_LMUL] THEN
453 ONCE_REWRITE_TAC[GSYM VECTOR_SUB_EQ] THEN
454 REWRITE_TAC[ VECTOR_ARITH ` ( a + b + (c:real^N) ) - vec 0 = vec 0 <=>
455 a = -- ( b + c ) `; REAL_ARITH` a + b + c = &0 <=> a = -- ( b + c ) `] THEN
456 SIMP_TAC[VECTOR_SUB_LDISTRIB] THEN
457 MESON_TAC[VECTOR_ARITH ` --(t2 + t3) % v3 - --(t2 % v2 + t3 % v3) -
458 (t2 % v2 - t2 % v3) = vec 0`];
460 EXISTS_TAC ` -- &1 ` THEN ASM_MESON_TAC[VECTOR_ARITH ` v3 - v2 = -- &1 % (v2 - v3)`];
467 let RHUFIIB = prove( ` !x12 x13 x14 x23 x24 x34.
468 rho_ij' x12 x13 x14 x23 x24 x34 * ups_x x34 x24 x23 =
469 chi x12 x13 x14 x23 x24 x34 pow 2 +
470 &4 * delta x12 x13 x14 x23 x24 x34 * x34 * x24 * x23 `,
471 REWRITE_TAC[rho_ij'; chi; delta; ups_x] THEN REAL_ARITH_TAC);;
474 let RIGHT_END_POINT = prove( `!x aa bb.
475 (?a b. &0 < a /\ b = &0 /\ a + b = &1 /\ x = a % aa + b % bb) <=> x = aa`,
476 REPEAT GEN_TAC THEN EQ_TAC THENL [STRIP_TR THEN
477 REWRITE_TAC[ MESON[REAL_ARITH `b = &0 /\ a + b = &1 <=> b= &0 /\ a = &1 `]`
478 b = &0 /\ a + b = &1 /\ P a b <=> b = &0 /\ a = &1 /\ P (&1 ) ( &0 ) `] THEN
479 MESON_TAC[VECTOR_ARITH ` &1 % aa + &0 % bb = aa `];
480 DISCH_TAC THEN EXISTS_TAC ` &1 ` THEN EXISTS_TAC ` &0 ` THEN
481 REWRITE_TAC[REAL_ARITH ` &0 < &1 /\ &1 + &0 = &1 `] THEN
482 ASM_MESON_TAC[VECTOR_ARITH ` &1 % aa + &0 % bb = aa `]]);;
484 let LEFT_END_POINT = prove(` !x aa bb.
485 (?a b. a = &0 /\ &0 < b /\ a + b = &1 /\ x = &0 % aa + &1 % bb)
487 REWRITE_TAC[VECTOR_ARITH ` &0 % aa + &1 % bb = bb `] THEN
488 MESON_TAC[REAL_ARITH ` &0 = &0 /\ &0 < &1 /\ &0 + &1 = &1 `]);;
491 let CONV_CONV0 = prove(`! x a b. x IN conv {a,b} <=> x = a \/ x = b \/ x IN conv0 {a,b} `,
492 REWRITE_TAC[CONV_SET2; CONV0_SET2; IN_ELIM_THM] THEN
493 REWRITE_TAC[REAL_ARITH ` &0 <= a <=> a = &0 \/ &0 < a `] THEN
494 KHANANG THEN REWRITE_TAC[EXISTS_OR_THM] THEN
495 SIMP_TAC[MESON[REAL_ARITH ` ~(a = &0 /\ b = &0 /\ a + b = &1)`]`
496 ~(a = &0 /\ b = &0 /\ a + b = &1 /\ las )` ] THEN
497 REWRITE_TAC[MESON[REAL_ARITH ` a = &0 /\ a + b = &1 <=> a = &0 /\ b = &1 `]`
498 a = &0 /\ &0 < b /\ a + b = &1 /\ x = a % aa + b % ba <=>
499 a = &0 /\ &0 < b /\ a + b = &1 /\ x = &0 % aa + &1 % ba`] THEN
500 MESON_TAC[ RIGHT_END_POINT; LEFT_END_POINT]);;
503 let GONTONG = REWRITE_TAC[REAL_ARITH ` ( a + b ) + c = a + b + c `];;
506 let MAEWNPU = prove(` ?b c.
507 !x12 x13 x14 x23 x24 x34.
508 delta x12 x13 x14 x23 x24 x34 =
510 b x12 x13 x14 x23 x24 * x34 +
511 c x12 x13 x14 x23 x24 `,
512 REWRITE_TAC[delta; REAL_ARITH ` a - b = a + -- b `;
513 REAL_ARITH ` a * (b + c )= a * b + a * c ` ] THEN
514 REWRITE_TAC[REAL_ARITH ` a * b * -- c = -- a * b * c /\ -- ( a * b ) = -- a * b `] THEN
515 REWRITE_TAC[REAL_ARITH` x12 * x34 * x23 + x12 * x34 * x24 +
516 --x12 * x34 * x34 = x12 * x34 * x23 + x12 * x34 * x24 +
517 -- x12 * ( x34 pow 2 ) `] THEN
518 REWRITE_TAC[REAL_ARITH ` ( a + b ) + c = a + b + c `] THEN
519 REWRITE_TAC[REAL_ARITH ` a + b * c pow 2 + d = b * c pow 2 + a + d `] THEN
520 ONCE_REWRITE_TAC[REAL_ARITH `a + b + c + d + e = a + d + b + c + e `] THEN
521 REWRITE_TAC[REAL_ARITH ` a * b * c = ( a * b ) * c `] THEN
522 REPLICATE_TAC 30 ( ONCE_REWRITE_TAC[REAL_ARITH ` a * x pow 2 + b * x + d + e
523 = a * x pow 2 + b * x + e + d `] THEN GONTONG THEN REWRITE_TAC[ REAL_ARITH
524 ` a * x pow 2 + b * x + d * x + e = a * x pow 2 + ( b + d) * x + e`]) THEN
525 REPLICATE_TAC 50 ( ONCE_REWRITE_TAC[REAL_ARITH ` a * x pow 2 + b * x + d + e
526 = a * x pow 2 + b * x + e + d `] THEN GONTONG THEN ONCE_REWRITE_TAC[ REAL_ARITH ` a * x pow 2 + b * x + (d * x) * h + e
527 = a * x pow 2 + ( b + d * h ) * x + e`]) THEN
528 EXISTS_TAC ` (\ x12 x13 x14 x23 x24. --x13 * x14 +
537 EXISTS_TAC ` (\ x12 x13 x14 x23 x24. (x14 * x23) * x12 +
539 (--x14 * x23) * x14 +
540 (--x14 * x23) * x23 +
542 (--x12 * x13) * x23 +
543 (--x12 * x14) * x24 +
545 (--x13 * x24) * x13 +
548 (--x13 * x24) * x24 ) ` THEN
551 (* ----new ------- *)
553 let DELTA_COEFS = new_specification ["b_coef"; "c_coef"] MAEWNPU;;
556 let DELTA_X34 = prove(` !x12 x13 x14 x23 x24 x34.
557 delta x12 x13 x14 x23 x24 x34 =
571 (--x14 * x23) * x14 +
572 (--x14 * x23) * x23 +
574 (--x12 * x13) * x23 +
575 (--x12 * x14) * x24 +
577 (--x13 * x24) * x13 +
580 (--x13 * x24) * x24`, REWRITE_TAC[delta] THEN REAL_ARITH_TAC);;
582 let C_COEF_FORMULA = prove(`! x12 x13 x14 x23 x24. c_coef x12 x13 x14 x23 x24
583 = (x14 * x23) * x12 +
585 (--x14 * x23) * x14 +
586 (--x14 * x23) * x23 +
588 (--x12 * x13) * x23 +
589 (--x12 * x14) * x24 +
591 (--x13 * x24) * x13 +
594 (--x13 * x24) * x24`, MP_TAC DELTA_COEFS THEN
595 NHANH (MESON[]` (!x12 x13 x14 x23 x24 x34. p x12 x13 x14 x23 x24 x34)
596 ==> (! x12 x13 x14 x23 x24. p x12 x13 x14 x23 x24 (&0) ) `) THEN
597 REWRITE_TAC[DELTA_X34] THEN
598 REWRITE_TAC[REAL_ARITH ` &0 pow 2 = &0 `; REAL_MUL_RZERO; REAL_ADD_LID] THEN
601 let BC_DEL_FOR = prove(` ! x12 x13 x14 x23 x24. b_coef x12 x13 x14 x23 x24 =
611 c_coef x12 x13 x14 x23 x24 =
614 (--x14 * x23) * x14 +
615 (--x14 * x23) * x23 +
617 (--x12 * x13) * x23 +
618 (--x12 * x14) * x24 +
620 (--x13 * x24) * x13 +
623 (--x13 * x24) * x24 `, REWRITE_TAC[C_COEF_FORMULA] THEN
624 MP_TAC DELTA_COEFS THEN NHANH (MESON[]` (!x12 x13 x14 x23 x24 x34.
625 p x12 x13 x14 x23 x24 x34)
626 ==> (! x12 x13 x14 x23 x24. p x12 x13 x14 x23 x24 (&1) ) `) THEN
627 REWRITE_TAC[DELTA_X34; C_COEF_FORMULA] THEN
628 REWRITE_TAC[REAL_ARITH ` a + b + c = a + b' + c <=> b = b' `] THEN
629 SIMP_TAC[REAL_RING` a * &1 = a `]);;
632 let AGBWHRD = prove(` !x12 x13 x14 x23 x24 x12 x13 x14 x23 x24.
633 b_coef x12 x13 x14 x23 x24 pow 2 +
634 &4 * x12 * c_coef x12 x13 x14 x23 x24 =
635 ups_x x12 x23 x13 * ups_x x12 x24 x14`, REWRITE_TAC[BC_DEL_FOR; ups_x] THEN
639 let COLLINEAR_EX = prove(` ! x y (z:real^3) . collinear {x,y,z} <=> ( ? a b c. a + b + c = &0 /\ ~ ( a = &0 /\
640 b = &0 /\ c = &0 ) /\ a % x + b % y + c % z = vec 0 ) `,
641 REWRITE_TAC[collinear] THEN
645 NHANH (SET_RULE` (!x' y'. x' IN {x, y, z} /\ y' IN {x, y, z} ==> P x' y' )
646 ==> P x y /\ P x z `) THEN
648 DISJ_CASES_TAC (MESON[]` c = &0 /\ c' = &0 \/ ~( c = &0 /\ c' = &0 ) `) THENL [
649 ASM_SIMP_TAC[VECTOR_ARITH ` x - y = &0 % t <=> y = x`] THEN
651 EXISTS_TAC ` &1 ` THEN EXISTS_TAC ` &1 ` THEN
652 EXISTS_TAC ` -- &2 ` THEN
653 REWRITE_TAC[REAL_ARITH ` &1 + &1 + -- &2 = &0 /\
654 ~(&1 = &0 /\ &1 = &0 /\ -- &2 = &0)`; VECTOR_ARITH` &1 % x + &1 % x +
659 NHANH (MESON[VECTOR_MUL_LCANCEL]` x = c % u /\
660 y = c' % u ==> c' % x = c' % (c % u) /\ c % y = c % c' % u `) THEN
661 REWRITE_TAC[VECTOR_ARITH ` x = c' % c % u /\ y = c % c' % u <=>
662 x = y /\ y = c % c' % u`] THEN
663 REWRITE_TAC[VECTOR_ARITH ` c' % (x - y) = c % (x - z) <=> (c - c' ) % x + c' % y +
664 -- c % z = vec 0 `] THEN
665 ASM_MESON_TAC[REAL_ARITH ` (( c - b ) + b + -- c = &0 ) /\ (~( c = &0 )
666 <=> ~( -- c = &0 ))`]];REWRITE_TAC[GSYM collinear] THEN MESON_TAC[SGFCDZO]]);;
669 let MAX_REAL_LESS_EX = prove(`!x y a. max_real x y <= a <=> x <= a /\ y <= a`,
670 REWRITE_TAC[max_real; COND_EXPAND; COND_ELIM_THM;COND_RAND; COND_RATOR] THEN
672 MESON_TAC[REAL_ARITH ` (~ ( b < a ) /\ b <= c ==> a <= c)`; REAL_ARITH ` a < b /\ b <= c ==> a <= c `]);;
675 let MAX_REAL3_LESS_EX = prove(`! x y z a. max_real3 x y z <= a <=> x <= a /\
676 y <= a /\ z <= a `, REWRITE_TAC[max_real3; MAX_REAL_LESS_EX] THEN MESON_TAC[]);;
680 (P x y z <=> P y x z) /\
681 (P x y z <=> P x z y) /\
682 (Q x y z <=> Q y x z) /\
683 (Q x y z <=> Q x z y)) /\
684 (!x y z. P x y z ==> Q x y z)
685 ==> (!x y z. P x y z ==> Q x y z /\ Q y x z /\ Q z x y)`;;
688 let UPS_X_SYM = prove(` ! x y z. ups_x x y z = ups_x y x z /\
689 ups_x x y z = ups_x x z y `, REWRITE_TAC[ups_x] THEN REAL_ARITH_TAC);;
691 let PER_MUL3 = REAL_ARITH ` a*b*c = b * a * c /\ a *b *c = a * c * b `;;
693 let ETA_X_SYM = prove(` ! x y z. &0 <= x /\ &0 <= y /\ &0 <= z /\ &0 <= ups_x x y z ==>
694 eta_x x y z = eta_x y x z /\ eta_x x y z = eta_x x z y `,
695 REWRITE_TAC[eta_x] THEN
696 NHANH (MESON[UPS_X_SYM]` &0 <= ups_x x y z ==> &0 <= ups_x y x z
697 /\ &0 <= ups_x x z y `) THEN
698 NHANH (MESON[REAL_LE_MUL]`&0 <= x /\ &0 <= y /\ &0 <= z /\ las ==>
699 &0 <= x * y * z`) THEN
700 PHA THEN NHANH (MESON[REAL_LE_DIV; REAL_ARITH ` a * b * c = b * a * c
701 /\ a * b * c = a * c * b `]`
702 &0 <= ups_x x y z /\ &0 <= aa /\ &0 <= bb /\ &0 <= x * y * z
703 ==> &0 <= (x * y * z) / ups_x x y z /\
704 &0 <= (y * x * z) / aa /\
705 &0 <= (x * z * y) / bb`) THEN
706 SIMP_TAC[SQRT_INJ] THEN
707 MESON_TAC[UPS_X_SYM; PER_MUL3]);;
709 let ETA_Y_SYM = prove(` ! x y z. &0 <= ups_x (x * x) (y * y) (z * z) ==>
710 eta_y x y z = eta_y y x z /\ eta_y x y z = eta_y x z y `,
711 REWRITE_TAC[eta_y] THEN REPEAT LET_TAC THEN MESON_TAC[ETA_X_SYM; REAL_LE_SQUARE]);;
715 let ETA_Y_SYMM = MESON[UPS_X_SYM; ETA_Y_SYM]` ! x y z. &0 <= ups_x (x * x) (y * y) (z * z)
716 ==> eta_y x y z = eta_y x z y /\
717 eta_y x y z = eta_y y x z /\
718 eta_y x y z = eta_y z x y /\
719 eta_y x y z = eta_y y z x /\
720 eta_y x y z = eta_y z y x`;;
723 let IMPLY_POS = prove(`! x y z . &0 <= ups_x (x * x) (y * y) (z * z) ==>
724 &0 <= ((z * z) * (x * x) * y * y) / ups_x (z * z) (x * x) (y * y) /\
725 &0 <= ((x * x) * (y * y) * z * z) / ups_x (x * x) (y * y) (z * z) /\
726 &0 <= ((y * y) * (z * z) * x * x) / ups_x (y * y) (z * z) (x * x) `, MP_TAC
727 REAL_LE_SQUARE THEN MP_TAC REAL_LE_MUL THEN MESON_TAC[UPS_X_SYM; REAL_LE_DIV]);;
729 let POW2_COND = MESON[REAL_ABS_REFL; REAL_LE_SQUARE_ABS]` ! a b. &0 <= a /\ &0 <= b ==>
730 ( a <= b <=> a pow 2 <= b pow 2 ) `;;
733 let TRUONGG = prove(`! x y z. &0 < ups_x_pow2 z x y ==>
734 ((z * z) * (x * x) * y * y) / ups_x (z * z) (x * x) (y * y) -
735 z pow 2 / &4 = ( z pow 2 * (( z pow 2 - x pow 2 - y pow 2 ) pow 2 ))
736 / (&4 * ups_x_pow2 z x y )`,
737 REWRITE_TAC[ups_x; ups_x_pow2] THEN CONV_TAC REAL_FIELD);;
739 let RE_TRUONGG = REWRITE_RULE[GSYM ups_x_pow2] TRUONGG;;
741 let HVXIKHW = prove(` !x y z.
742 &0 <= x /\ &0 <= y /\ &0 <= z /\ &0 < ups_x_pow2 x y z
743 ==> max_real3 x y z / &2 <= eta_y x y z`,
744 REWRITE_TAC[REAL_ARITH` a / &2 <= b <=> a <= &2 * b `; MAX_REAL3_LESS_EX] THEN
745 REWRITE_TAC[eta_x; ups_x_pow2] THEN
746 NHANH (REAL_ARITH` &0 < a ==> &0 <= a `) THEN
747 DAO THEN REPEAT GEN_TAC THEN
748 REWRITE_TAC[MESON[ETA_Y_SYMM]` &0 <= ups_x (x * x) (y * y) (z * z) /\ las
749 ==> z <= &2 * eta_y x y z /\ x <= &2 * eta_y x y z /\ y <= &2 * eta_y x y z
750 <=> &0 <= ups_x (x * x) (y * y) (z * z) /\ las
751 ==> z <= &2 * eta_y z x y /\ x <= &2 * eta_y x y z /\ y <= &2 * eta_y y z x`] THEN
752 REWRITE_TAC[eta_y] THEN CONV_TAC (TOP_DEPTH_CONV let_CONV) THEN REWRITE_TAC[eta_x]
753 THEN NHANH (SPEC_ALL IMPLY_POS) THEN
754 NHANH (SPEC_ALL (prove(` ! a b x y. &0 <= a / b /\ &0 <= x /\ &0 <= y ==>
755 &0 <= &2 * sqrt ( a/b) /\ &0 <= &2 * sqrt x /\ &0 <= &2 * sqrt y `,
756 REWRITE_TAC[REAL_ARITH ` &0 <= &2 * a <=> &0 <= a `] THEN
757 SIMP_TAC[SQRT_WORKS]))) THEN SIMP_TAC[POW2_COND] THEN
758 REWRITE_TAC[REAL_ARITH ` x <= ( &2 * y ) pow 2 <=> x / &4 <= y pow 2 `] THEN
759 SIMP_TAC[ SQRT_POW_2] THEN REWRITE_TAC[ GSYM ups_x_pow2] THEN
760 REWRITE_TAC[REAL_FIELD` a / b <= c <=> &0 <= c - a / b `] THEN
761 SIMP_TAC[ups_x_pow2; UPS_X_SYM; RE_TRUONGG] THEN DAO THEN
762 MATCH_MP_TAC (MESON[]` (a4 ==> l) ==> (a1/\a2/\a3/\a4/\a5) ==> l `) THEN
763 MP_TAC REAL_LE_SQUARE THEN MP_TAC REAL_LE_MUL THEN MP_TAC REAL_LE_DIV THEN
764 REWRITE_TAC[GSYM REAL_POW_2] THEN MESON_TAC[REAL_ARITH ` &0 < a ==> &0 <= &4 * a `]);;
767 let EXISTS_INV = REAL_FIELD` ~( a = &0 ) <=> a * &1 / a = &1 /\ &1 / a * a = &1 `;;
770 let REAL_LT_RDIV_0 = prove( `!y z. &0 < z ==> (&0 < (y / z) <=> &0 < y)`,
771 MESON_TAC[REAL_LT_DIV;REAL_LT_MUL;REAL_DIV_RMUL;REAL_ARITH `&0 < x==> ~(x= &0)`]);;
773 let POS_EQ_INV_POS = prove(`!x. &0 < x <=> &0 < &1 / x`, GEN_TAC THEN EQ_TAC
774 THENL [REWRITE_TAC[MESON[REAL_LT_RDIV_0; REAL_ARITH ` &0 < &1 `]`! b. &0 < b
775 ==> &0 < &1 / b `];REWRITE_TAC[] THEN
776 MESON_TAC[MESON[REAL_LT_RDIV_0; REAL_ARITH ` &0 < &1 `]` &0 < b
777 ==> &0 < &1 / b `; REAL_FIELD ` &1 / ( &1 / x ) = x ` ]]);;
780 let MIDDLE_POINT = prove(` ! x y (z:real^3) . collinear {x,y,z} ==> x IN conv {y,z} \/
781 y IN conv {x,z} \/ z IN conv {x,y} `, REWRITE_TAC[COLLINEAR_EX] THEN REPEAT
783 MATCH_MP_TAC (prove(`(!(a:real) (b:real) (c:real). P a b c <=> P (--a) (--b) (--c)) /\
784 ((?a b c. &0 <= a /\ P a b c) ==> l) ==> ( ? a b c. P a b c ) ==> l `,
785 DISCH_TAC THEN ASM_MESON_TAC[REAL_ARITH ` ! a. a <= &0 \/ &0 <= a`;
786 REAL_ARITH ` a <= &0 <=> &0 <= -- a `])) THEN
787 CONJ_TAC THENL [MESON_TAC[REAL_ARITH` a = &0 <=> -- a = &0 `; REAL_ARITH ` a + b + c = &0
788 <=> --a + --b + --c = &0`; VECTOR_ARITH ` a % x + b % y + c % z = vec 0
789 <=> --a % x + --b % y + --c % z = vec 0 `]; STRIP_TAC] THEN
790 DISJ_CASES_TAC (REAL_ARITH ` &0 < b \/ b <= &0`) THENL
791 [STRIP_TR THEN REWRITE_TAC[VECTOR_ARITH ` a + b + c % z = vec 0 <=>
792 --c % z = a + b `] THEN
793 NHANH (MESON[VECTOR_MUL_LCANCEL]` a % x = y ==> (&1 / a) % a % x = &1 / a % y `) THEN
794 REWRITE_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC] THEN
795 REWRITE_TAC[MESON[]` a1/\a2/\a3/\a4/\a5 ==> l <=> a1 /\ a5 /\ a2 ==>
797 NHANH (REAL_FIELD ` &0 <= a /\ &0 < b /\ a + b + c = &0 ==>
798 a / ( -- c ) + b /( -- c ) = &1 /\ ~ ( -- c = &0 )/\ &0 < -- c `) THEN
799 SIMP_TAC[EXISTS_INV] THEN
800 ONCE_REWRITE_TAC[MESON[POS_EQ_INV_POS]` a /\ &0 < c <=> a /\ &0 < &1 / c `] THEN
801 REWRITE_TAC[VECTOR_MUL_LID; CONV_SET2; IN_ELIM_THM; GSYM (REAL_ARITH` a / b =
803 ONCE_REWRITE_TAC[REAL_ARITH` a / b = &1 / b * a `] THEN
804 MP_TAC (GEN_ALL (MESON[REAL_ARITH`( a * &1 = a ) /\ ( &0 < a ==> &0 <= a )`;
805 REAL_LE_MUL]` &0 < &1 / c * &1 /\ ( &0 <= a \/ &0 < a ) ==> &0 <= &1 / c * a `)) THEN
806 MESON_TAC[]; STRIP_TR THEN
807 NHANH (MESON[REAL_ARITH` &0 <= c \/ c <= &0`]` a + b + v = &0 ==>
808 &0 <= v \/ v <= &0 `) THEN
809 REWRITE_TAC[MESON[]` a1/\(a2 /\ (aa\/ bb))/\ dd <=>
810 (aa\/bb) /\ a1/\a2/\dd`] THEN SPEC_TAC (`a:real`, `a:real`) THEN
811 SPEC_TAC (`b:real`, `b:real`) THEN SPEC_TAC (`c:real`, `c:real`) THEN
812 KHANANG THEN REWRITE_TAC[(prove( `&0 <= c /\ &0 <= a /\ a + b + c = &0 /\
813 ~(a = &0 /\ b = &0 /\ c = &0) /\ a % x + b % y + c % z = vec 0 /\
814 b <= &0 <=> --a <= &0 /\ &0 <= --b /\ --b + --c + --a = &0 /\
815 ~(--b = &0 /\ --c = &0 /\ --a = &0) /\ --b % y + --c % z + -- a % x = vec 0 /\
816 --c <= &0`, MESON_TAC[
817 REAL_ARITH ` (a = &0 <=> --a = &0) /\ ( b <= &0 <=> &0 <= -- b ) /\
818 (&0 <= a <=> --a <= &0) /\
819 (a + b + c = &0 <=> --b + --c + -- a = &0)`;
820 VECTOR_ARITH` a % x + b % y + c % z = vec 0 <=>
821 --b % y + --c % z + --a % x = vec 0 `]))] THEN
822 REWRITE_TAC[MESON[]` a \/ b ==> c <=> (a ==> c) /\(b==>c)`] THEN
823 REWRITE_TAC[MESON[REAL_ARITH `&0 <= a <=> a = &0 \/ &0 < a `]`
824 c <= &0 /\ &0 <= a /\ l <=> ( a = &0 \/ &0 < a ) /\ c <= &0 /\ l`] THEN
826 REWRITE_TAC[MESON[REAL_ARITH `a = &0 /\ c <= &0 /\ a + b + c = &0 /\ b <= &0
827 ==> a = &0 /\ b = &0 /\ c = &0`]`a = &0 /\ c <= &0 /\
828 a + b + c = &0 /\ ~(a = &0 /\ b = &0 /\ c = &0) /\a2/\ b <= &0 <=> F `] THEN
829 NHANH (MESON[REAL_FIELD ` &0 < a /\
830 a + b + c = &0 ==> -- b / a + -- c / a = &1 `]`&0 < a /\ c <= &0 /\
831 a + b + c = &0 /\ l ==> --b / a + --c / a = &1 `) THEN
832 REWRITE_TAC[VECTOR_ARITH ` a % x + b % y + c % z = vec 0 <=>
833 a % x = -- b % y + -- c % z `] THEN
834 NHANH (MESON[VECTOR_MUL_LCANCEL]` a % x = y ==> &1 / a % a % x = &1 / a % y `) THEN
835 REWRITE_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC; REAL_ARITH ` &1 / a * b
836 = b / a `;VECTOR_MUL_LID ] THEN PHA THEN
837 PURE_ONCE_REWRITE_TAC[MESON[REAL_FIELD ` &0 < a ==> a / a = &1`]`
838 &0 < a /\ P ( a / a) <=> &0 < a /\ P ( &1 ) `] THEN
839 REWRITE_TAC[VECTOR_MUL_LID ] THEN
840 REWRITE_TAC[MESON[SET_RULE ` {a,b} = {b,a}`]` y IN conv {x, z} \/ z IN conv {x, y}
841 <=> y IN conv {z,x} \/ z IN conv {x,y} `] THEN
842 REWRITE_TAC[CONV_SET2; IN_ELIM_THM] THEN
843 REWRITE_TAC[ REAL_ARITH ` a <= &0 <=> &0 <= -- a `] THEN
844 MESON_TAC[REAL_LE_DIV; REAL_ARITH ` &0 < a ==> &0 <= a `]]);;
846 let IN_CONV_COLLINEAR = prove(` ! (v:real^3) v1 v2. v IN conv {v1,v2} ==>
847 collinear {v,v1,v2} `, REWRITE_TAC[COLLINEAR_EX] THEN
848 REWRITE_TAC[COLLINEAR_EX; CONV_SET2; IN_ELIM_THM] THEN
849 REWRITE_TAC[VECTOR_ARITH ` v = a % v1 + b % v2 <=>
850 &1 % v + -- a % v1 + -- b % v2 = vec 0 `] THEN
851 MESON_TAC[REAL_ARITH `~ ( &1 = &0 ) /\ (a + b = &1 <=> &1 + --a + --b = &0 )`]);;
853 let PER_SET3 = SET_RULE ` {a,b,c} = {a,c,b} /\ {a,b,c} = {b,a,c} /\
854 {a,b,c} = {c,a,b} /\ {a,b,c} = {b,c,a} /\ {a,b,c} = {c,b,a} `;;
856 let COLLINERA_AS_IN_CONV2 = prove(` ! x y (z:real^3) . collinear {x,y,z} <=>
858 y IN conv {x,z} \/ z IN conv {x,y}`,
859 MESON_TAC[PER_SET3; IN_CONV_COLLINEAR; MIDDLE_POINT]);;
861 let LENGTH_EQ_EX = prove(`!v v1 v2.
862 dist (v1,v) + dist (v,v2) = dist (v1,v2) <=>
863 ~(dist (v1,v2) < dist (v1,v) + dist (v,v2))`,
865 REWRITE_TAC[REAL_ARITH ` ~( a < b) <=> b <= a `] THEN
866 EQ_TAC THENL [REAL_ARITH_TAC;
867 NHANH (MESON[DIST_TRIANGLE]` dist (v1,v) + dist (v,v2) <= dist (v1,v2)
868 ==> dist(v1,v2) <= dist (v1,v) + dist (v,v2)`) THEN
872 (* HARRISON have proved this lemma as following, but it must be loaded after convex.ml *)
874 let BETWEEN_IFF_IN_CONVEX_HULL = prove
876 dist(v1,v) + dist(v,v2) = dist(v1,v2) <=> v IN convex hull {v1,v2}`,
877 REPEAT GEN_TAC THEN ASM_CASES_TAC `v1:real^N = v2` THENL
878 [ASM_REWRITE_TAC[INSERT_AC; CONVEX_HULL_SING; IN_SING] THEN NORM_ARITH_TAC;
879 REWRITE_TAC[CONVEX_HULL_2_ALT; IN_ELIM_THM] THEN EQ_TAC THENL
880 [DISCH_TAC THEN EXISTS_TAC `dist(v1:real^N,v) / dist(v1,v2)` THEN
881 ASM_SIMP_TAC[REAL_LE_LDIV_EQ; REAL_LE_RDIV_EQ; DIST_POS_LT] THEN CONJ_TAC
882 THENL [FIRST_ASSUM(SUBST1_TAC o SYM) THEN NORM_ARITH_TAC; ALL_TAC] THEN
883 MATCH_MP_TAC VECTOR_MUL_LCANCEL_IMP THEN
884 EXISTS_TAC `dist(v1:real^N,v2)` THEN
885 ASM_SIMP_TAC[VECTOR_MUL_ASSOC; VECTOR_ADD_LDISTRIB; REAL_SUB_LDISTRIB;
886 REAL_DIV_LMUL; DIST_EQ_0] THEN
887 FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [DIST_TRIANGLE_EQ] o SYM) THEN
888 FIRST_ASSUM(SUBST1_TAC o SYM) THEN
889 REWRITE_TAC[dist; REAL_ARITH `(a + b) * &1 - a = b`] THEN
891 STRIP_TAC THEN ASM_REWRITE_TAC[dist] THEN
892 REWRITE_TAC[VECTOR_ARITH `a - (a + b:real^N) = --b`;
893 VECTOR_ARITH `(a + u % (b - a)) - b = (&1 - u) % (a - b)`;
894 NORM_NEG; NORM_MUL; GSYM REAL_ADD_LDISTRIB] THEN
895 REWRITE_TAC[NORM_SUB] THEN REPEAT(POP_ASSUM MP_TAC) THEN
896 CONV_TAC REAL_FIELD]]);;
898 (* From this, your version follows easily: *)
900 let BETWEEN_IMP_IN_CONVEX_HULL = prove
901 (`!v v1 v2. dist(v1,v) + dist(v,v2) = dist(v1,v2)
902 ==> (?a b. &0 <= a /\ &0 <= b /\ a + b = &1 /\
903 v = a % v1 + b % v2)`,
904 REWRITE_TAC[BETWEEN_IFF_IN_CONVEX_HULL; CONVEX_HULL_2; IN_ELIM_THM] THEN
905 REWRITE_TAC[CONJ_ASSOC]);;
909 let PRE_HE = prove(` ! x y z. let p = ( x + y + z ) / &2 in
910 ups_x_pow2 x y z = &16 * p * ( p - x ) * ( p - y ) * ( p - z ) `,
911 CONV_TAC (TOP_DEPTH_CONV let_CONV) THEN
912 REWRITE_TAC[ups_x_pow2; ups_x] THEN REAL_ARITH_TAC);;
914 let PRE_HER = prove(`!x y z.
918 ((x + y + z) / &2 - x) *
919 ((x + y + z) / &2 - y) *
920 ((x + y + z) / &2 - z)`,
921 REWRITE_TAC[ups_x_pow2; ups_x] THEN REAL_ARITH_TAC);;
924 let TRIVIVAL_LE = prove(`!v1 v2 v3.
925 ~(v2 = v3 /\ v1 = v2)
926 ==> ~(dist (v1,v2) + dist (v1,v3) + dist (v2,v3) = &0)`,
927 SIMP_TAC[DE_MORGAN_THM; DIST_NZ] THEN
928 NHANH (MESON[DIST_POS_LE]`&0 < dist (v2,v3) \/ &0 < dist (v1,v2) ==>
929 &0 <= dist(v1,v3) `) THEN MP_TAC DIST_POS_LE THEN KHANANG THEN
930 REWRITE_TAC[OR_IMP_EX] THEN
931 NHANH (MESON[DIST_POS_LE]`&0 < dist (v2,v3) /\ &0 <= dist (v1,v3)
932 ==> &0 <= dist(v1,v2) `) THEN
933 SIMP_TAC[REAL_ARITH`( &0 < a /\ &0 <= b ) /\ &0 <= c ==> ~(c + b + a = &0 ) `] THEN
934 NHANH (MESON[DIST_POS_LE]`&0 < dist (v1,v2) /\ &0 <= dist (v1,v3) ==>
935 &0 <= dist(v2,v3) `) THEN
936 MESON_TAC[REAL_ARITH ` &0 < a /\ &0 <= b /\ &0 <= c ==> ~( a + b + c = &0 ) `]);;
940 let MID_COND = prove(` ! v v1 v2. v IN conv {v1,v2} <=> dist(v1,v) + dist(v,v2)
941 = dist(v1,v2) `, REPEAT GEN_TAC THEN EQ_TAC THENL [MESON_TAC[LENGTH_EQUA; DIST_SYM];
942 REWRITE_TAC[CONV_SET2; IN_ELIM_THM] THEN
943 MESON_TAC[DIST_SYM; BETWEEN_IMP_IN_CONVEX_HULL]]);;
947 let FHFMKIY = prove(`!(v1:real^3) v2 v3 x12 x13 x23.
948 x12 = dist (v1,v2) pow 2 /\
949 x13 = dist (v1,v3) pow 2 /\
950 x23 = dist (v2,v3) pow 2
951 ==> (collinear {v1, v2, v3} <=> ups_x x12 x13 x23 = &0)`,
952 REPEAT STRIP_TAC THEN ASM_SIMP_TAC[] THEN REWRITE_TAC[COLLINERA_AS_IN_CONV2]
953 THEN REWRITE_TAC[REAL_ARITH ` x pow 2 = x * x `; GSYM ups_x_pow2] THEN
954 REWRITE_TAC[PRE_HER] THEN REWRITE_TAC[REAL_ENTIRE] THEN
955 ONCE_REWRITE_TAC[MESON[]`( v1 IN conv {v2, v3} \/ a \/ b <=> l ) <=>
956 (v1 = v2 /\ v1 = v3 ) \/ ~(v1 = v2 /\ v1 = v3) ==> ( v1 IN conv {v2, v3}
957 \/ a \/ b <=> l )`] THEN REWRITE_TAC[OR_IMP_EX] THEN
958 SIMP_TAC[DIST_SYM; DIST_REFL; MESON[]` a= b/\ a= c <=> b = c /\ a= b`] THEN
959 SIMP_TAC[SET_RULE ` {a,a} = {a} /\ a IN {a} `; CONV_SING;
960 REAL_ARITH ` (&0 + &0 + &0)/ &2 = &0 `] THEN SIMP_TAC[ TRIVIVAL_LE;
961 REAL_ARITH `~( &16 = &0) /\(~( a = &0) ==> ~( a / &2 = &0))`] THEN
962 REWRITE_TAC[REAL_ARITH ` (a+ b + c ) / &2 - a = &0 <=> b + c = a `] THEN
963 REWRITE_TAC[REAL_ARITH ` (a+ b + c ) / &2 - b = &0 <=> c + a = b `] THEN
964 REWRITE_TAC[REAL_ARITH ` (a+ b + c ) / &2 - c = &0 <=> a + b = c `] THEN
965 REWRITE_TAC[MESON[SET_RULE `{a,b} = {b,a} `]`v2 IN conv {v1, v3} \/ v3 IN
966 conv {v1, v2} <=> v2 IN conv {v3,v1} \/ v3 IN conv {v1, v2}`] THEN
967 REWRITE_TAC[MID_COND] THEN MESON_TAC[DIST_SYM]);;
970 (* NGUYEN QUANG TRUONG *)
973 (* These following lemma are Multivariate/convex.ml *)
976 let affine_dependent = new_definition
977 `affine_dependent (s:real^N -> bool) <=>
978 ?x. x IN s /\ x IN (affine hull (s DELETE x))`;;
980 let AFFINE_HULL_FINITE = prove
983 ==> affine hull s = {y | ?u. sum s u = &1 /\ vsum s (\v. u v % v) = y}`,
984 GEN_TAC THEN DISCH_TAC THEN
985 REWRITE_TAC[EXTENSION; AFFINE_HULL_EXPLICIT; IN_ELIM_THM] THEN
986 X_GEN_TAC `x:real^N` THEN EQ_TAC THEN REWRITE_TAC[LEFT_IMP_EXISTS_THM] THENL
987 [MAP_EVERY X_GEN_TAC [`t:real^N->bool`; `f:real^N->real`] THEN
989 EXISTS_TAC `\x:real^N. if x IN t then f x else &0` THEN
990 REWRITE_TAC[] THEN ONCE_REWRITE_TAC[COND_RAND] THEN
991 ONCE_REWRITE_TAC[COND_RATOR] THEN REWRITE_TAC[VECTOR_MUL_LZERO] THEN
992 ASM_SIMP_TAC[GSYM VSUM_RESTRICT_SET; GSYM SUM_RESTRICT_SET] THEN
993 ASM_SIMP_TAC[SET_RULE `t SUBSET s ==> {x | x IN s /\ x IN t} = t`];
994 X_GEN_TAC `f:real^N->real` THEN
995 ASM_CASES_TAC `s:real^N->bool = {}` THEN
996 ASM_REWRITE_TAC[SUM_CLAUSES; REAL_OF_NUM_EQ; ARITH] THEN STRIP_TAC THEN
997 MAP_EVERY EXISTS_TAC [`s:real^N->bool`; `f:real^N->real`] THEN
998 ASM_REWRITE_TAC[GSYM EXTENSION; SUBSET_REFL]]);;
1000 let IN_AFFINE_HULL_IMP_COLLINEAR = prove
1001 (`!a b c:real^N. a IN (affine hull {b,c}) ==> collinear {a,b,c}`,
1002 REPEAT GEN_TAC THEN MAP_EVERY ASM_CASES_TAC
1003 [`a:real^N = b`; `a:real^N = c`; `b:real^N = c`] THEN
1004 TRY(ASM_REWRITE_TAC[INSERT_AC; COLLINEAR_SING; COLLINEAR_2] THEN NO_TAC) THEN
1005 SIMP_TAC[AFFINE_HULL_FINITE; FINITE_INSERT; FINITE_SING] THEN
1006 SIMP_TAC[SUM_CLAUSES; VSUM_CLAUSES; FINITE_RULES; REAL_ADD_RID] THEN
1007 ASM_REWRITE_TAC[IN_INSERT; IN_ELIM_THM; NOT_IN_EMPTY; VECTOR_ADD_RID] THEN
1008 DISCH_THEN(X_CHOOSE_THEN `f:real^N->real` STRIP_ASSUME_TAC) THEN
1009 ONCE_REWRITE_TAC[SET_RULE `{a,b,c} = {c,b,a}`] THEN
1010 ASM_REWRITE_TAC[COLLINEAR_3; COLLINEAR_LEMMA; VECTOR_SUB_EQ] THEN
1011 EXISTS_TAC `(f:real^N->real) c` THEN EXPAND_TAC "a" THEN
1012 FIRST_X_ASSUM(SUBST1_TAC o MATCH_MP (REAL_ARITH
1013 `b + c = &1 ==> b = &1 - c`)) THEN VECTOR_ARITH_TAC);;
1016 let AFFINE_DEPENDENT_3_IMP_COLLINEAR = prove
1017 (`!a b c:real^N. affine_dependent{a,b,c} ==> collinear{a,b,c}`,
1019 MAP_EVERY ASM_CASES_TAC
1020 [`a:real^N = b`; `a:real^N = c`; `b:real^N = c`] THEN
1021 TRY(ASM_REWRITE_TAC[INSERT_AC; COLLINEAR_SING; COLLINEAR_2] THEN NO_TAC) THEN
1022 REWRITE_TAC[affine_dependent; IN_INSERT; NOT_IN_EMPTY] THEN STRIP_TAC THEN
1023 FIRST_X_ASSUM SUBST_ALL_TAC THENL
1025 ONCE_REWRITE_TAC[SET_RULE `{a,b,c} = {b,a,c}`];
1026 ONCE_REWRITE_TAC[SET_RULE `{a,b,c} = {c,b,a}`]] THEN
1027 MATCH_MP_TAC IN_AFFINE_HULL_IMP_COLLINEAR THEN
1028 FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (MESON[]
1029 `x IN s ==> s = t ==> x IN t`)) THEN
1030 AP_TERM_TAC THEN ASM SET_TAC[]);;
1034 (`!v1 v2 v3 v:real^N.
1035 ~collinear{v1,v2,v3} /\ v IN (affine hull {v1,v2,v3})
1037 ==> ?t1 t2 t3. v = t1 % v1 + t2 % v2 + t3 % v3 /\
1038 t1 + t2 + t3 = &1 /\
1039 !ta tb tc. v = ta % v1 + tb % v2 + tc % v3 /\
1042 ==> ta = t1 /\ tb = t2 /\ tc = t3`,
1044 MAP_EVERY ASM_CASES_TAC
1045 [`v1:real^N = v2`; `v2:real^N = v3`; `v1:real^N = v3`] THEN
1046 TRY(ASM_REWRITE_TAC[INSERT_AC; COLLINEAR_SING; COLLINEAR_2] THEN NO_TAC) THEN
1047 SIMP_TAC[AFFINE_HULL_FINITE; FINITE_INSERT; FINITE_SING; IN_ELIM_THM] THEN
1048 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
1049 SIMP_TAC[SUM_CLAUSES; VSUM_CLAUSES; FINITE_INSERT; FINITE_SING;
1050 SUM_SING; VSUM_SING] THEN
1051 ASM_REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY; LEFT_IMP_EXISTS_THM] THEN
1052 X_GEN_TAC `f:real^N->real` THEN STRIP_TAC THEN
1053 MAP_EVERY EXISTS_TAC
1054 [`(f:real^N->real) v1`; `(f:real^N->real) v2`; `(f:real^N->real) v3`] THEN
1055 ASM_REWRITE_TAC[] THEN REPEAT GEN_TAC THEN EXPAND_TAC "v" THEN
1056 DISCH_TAC THEN MATCH_MP_TAC(TAUT `(~p ==> F) ==> p`) THEN DISCH_TAC THEN
1057 UNDISCH_TAC `~collinear{v1:real^N,v2,v3}` THEN REWRITE_TAC[] THEN
1058 MATCH_MP_TAC AFFINE_DEPENDENT_3_IMP_COLLINEAR THEN
1059 SIMP_TAC[AFFINE_DEPENDENT_EXPLICIT_FINITE; FINITE_INSERT; FINITE_RULES;
1060 SUM_CLAUSES; VSUM_CLAUSES] THEN
1061 ASM_REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY] THEN
1062 EXISTS_TAC `\x. if x = v1 then f v1 - ta
1063 else if x = v2 then f v2 - tb
1064 else (f:real^N->real) v3 - tc` THEN
1065 ASM_REWRITE_TAC[REAL_ADD_RID; VECTOR_ADD_RID] THEN REPEAT CONJ_TAC THENL
1066 [ASM_REAL_ARITH_TAC;
1067 ASM_REWRITE_TAC[EXISTS_OR_THM; RIGHT_OR_DISTRIB; UNWIND_THM2] THEN
1068 ASM_REWRITE_TAC[REAL_SUB_0] THEN ASM_MESON_TAC[];
1069 ASM_REWRITE_TAC[VECTOR_ARITH
1070 `(a - a') % x + (b - b') % y + (c - c') % z = vec 0 <=>
1071 a % x + b % y + c % z = a' % x + b' % y + c' % z`] THEN
1076 let FAFKVLR_ALT = prove
1077 (`!v1 v2 v3 v:real^N.
1078 ~collinear{v1,v2,v3} /\ v IN (affine hull {v1,v2,v3})
1079 ==> ?!(t1,t2,t3). v = t1 % v1 + t2 % v2 + t3 % v3 /\
1081 REWRITE_TAC(map(REWRITE_RULE[ETA_AX])
1082 [EXISTS_UNIQUE; FORALL_PAIR_THM; EXISTS_PAIR_THM]) THEN
1083 REWRITE_TAC[PAIR_EQ; GSYM CONJ_ASSOC; FAFKVLR]);;
1086 let equivalent_lemma = prove(` (?t1 t2 t3.
1087 !v1 v2 v3 (v:real^N).
1088 v IN affine hull {v1, v2, v3} /\ ~collinear {v1, v2, v3}
1090 t1 v1 v2 v3 v % v1 + t2 v1 v2 v3 v % v2 + t3 v1 v2 v3 v % v3 /\
1091 t1 v1 v2 v3 v + t2 v1 v2 v3 v + t3 v1 v2 v3 v = &1 /\
1093 v = ta % v1 + tb % v2 + tc % v3 /\ ta + tb + tc = &1
1094 ==> ta = t1 v1 v2 v3 v /\
1095 tb = t2 v1 v2 v3 v /\
1096 tc = t3 v1 v2 v3 v)) <=>
1098 ( !v1 v2 v3 (v:real^N).
1099 v IN affine hull {v1, v2, v3} /\ ~collinear {v1, v2, v3}
1101 v = t1 % v1 + t2 % v2 + t3 % v3 /\
1102 t1 + t2 + t3 = &1 /\
1104 v = ta % v1 + tb % v2 + tc % v3 /\ ta + tb + tc = &1
1105 ==> ta = t1 /\ tb = t2 /\ tc = t3))) `,
1106 REWRITE_TAC[GSYM SKOLEM_THM; LEFT_FORALL_IMP_THM; RIGHT_EXISTS_IMP_THM]);;
1109 let LAMBDA_TRIPLED_THM = prove
1110 (`!t. (\(x,y,z). t x y z) = (\p. t (FST p) (FST(SND p)) (SND(SND p)))`,
1111 REWRITE_TAC[FUN_EQ_THM; FORALL_PAIR_THM]);;
1113 let FORALL_TRIPLED_THM = prove
1114 (`!P. (!(x,y,z). P x y z) <=> (!x y z. P x y z)`,
1115 REWRITE_TAC[LAMBDA_TRIPLED_THM] THEN REWRITE_TAC[FORALL_PAIR_THM]);;
1117 let EXISTS_TRIPLED_THM = prove
1118 (`!P. (?(x,y,z). P x y z) <=> (?x y z. P x y z)`,
1119 REWRITE_TAC[LAMBDA_TRIPLED_THM] THEN REWRITE_TAC[EXISTS_PAIR_THM]);;
1121 let EXISTS_UNIQUE_TRIPLED_THM = prove
1122 (`!P. (?!(x,y,z). P x y z) <=>
1124 (!x' y' z'. P x' y' z' ==> x' = x /\ y' = y /\ z' = z))`,
1125 REWRITE_TAC[REWRITE_RULE[ETA_AX] EXISTS_UNIQUE] THEN
1126 REWRITE_TAC[FORALL_TRIPLED_THM; EXISTS_TRIPLED_THM] THEN
1127 REWRITE_TAC[EXISTS_PAIR_THM; FORALL_PAIR_THM; PAIR_EQ]);;
1130 let theoremmm = prove
1131 (`( !v1 v2 v3 v:real^N.
1132 v IN affine hull {v1, v2, v3} /\ ~collinear {v1, v2, v3}
1134 v = t1 % v1 + t2 % v2 + t3 % v3 /\
1135 t1 + t2 + t3 = &1 /\
1137 v = ta % v1 + tb % v2 + tc % v3 /\
1139 ==> ta = t1 /\ tb = t2 /\ tc = t3)) )
1141 ( !v1 v2 v3 v:real^N.
1142 ~collinear {v1, v2, v3} /\ v IN affine hull {v1, v2, v3}
1143 ==> (?!(t1,t2,t3). v = t1 % v1 + t2 % v2 + t3 % v3 /\
1144 t1 + t2 + t3 = &1))`,
1145 REWRITE_TAC[EXISTS_UNIQUE_TRIPLED_THM] THEN REWRITE_TAC[CONJ_ACI]);;
1150 let FAFKVLR = prove(` (?t1 t2 t3.
1151 !v1 v2 v3 (v:real^N).
1152 v IN affine hull {v1, v2, v3} /\ ~collinear {v1, v2, v3}
1154 t1 v1 v2 v3 v % v1 + t2 v1 v2 v3 v % v2 + t3 v1 v2 v3 v % v3 /\
1155 t1 v1 v2 v3 v + t2 v1 v2 v3 v + t3 v1 v2 v3 v = &1 /\
1157 v = ta % v1 + tb % v2 + tc % v3 /\ ta + tb + tc = &1
1158 ==> ta = t1 v1 v2 v3 v /\
1159 tb = t2 v1 v2 v3 v /\
1160 tc = t3 v1 v2 v3 v)) `,
1161 SIMP_TAC[equivalent_lemma; FAFKVLR]);;
1162 let LEMMA11 = FAFKVLR;;
1163 let lemma11 = REWRITE_RULE[equivalent_lemma] FAFKVLR;;
1164 let COEFS = new_specification ["coef1"; "coef2"; "coef3"] FAFKVLR;;
1166 let lem11 = REWRITE_RULE[simp_def2; IN_ELIM_THM] lemma11;;
1168 let REAL_PER3 = REAL_ARITH `!a b c. a + b + c = b + a + c /\ a + b + c = c + b + a `;;
1171 MESON[VEC_PER2_3]` (!ta tb tc.
1172 v = ta % v1 + tb % v2 + tc % v3 ==> ta = t1 /\ tb = t2 /\ tc = t3) /\bbb/\
1173 v = ta''' % v1 + tb''' % v2 + t''' % v3 /\
1174 v = ta'' % v3 + tb'' % v1 + t'' % v2 /\
1175 v = ta' % v2 + tb' % v3 + t' % v1 /\
1176 aa ==> t' = t1 /\ t'' = t2 /\ t''' = t3 `;;
1178 let NOT_COLLINEAR_IMP_2_UNEQUAL = MESON[INSERT_INSERT; COLLINEAR_2; INSERT_AC]
1179 `~collinear {v0, va, vb} ==> ~(v0 = va) /\ ~(v0 = vb) `;;
1181 let COLLINEAR_DISJOINT3 = prove(`!v1:real^A v2 v3. ~collinear {v1,v2,v3} ==>
1182 DISJOINT {v2,v3} {v1}`,
1183 REWRITE_TAC[DISJOINT_INSERT;DISJOINT_EMPTY;IN_INSERT;NOT_IN_EMPTY] THEN
1184 MESON_TAC[NOT_COLLINEAR_IMP_2_UNEQUAL]
1187 let COLLINEAR_DISJOINT_PERM3 = prove(`!v1:real^A v2 v3. (~collinear {v1,v2,v3} ==>
1188 DISJOINT {v1,v2} {v3}) /\ (~collinear {v1,v2,v3} ==> DISJOINT {v2,v3} {v1}) /\
1189 (~collinear {v1,v2,v3} ==> DISJOINT {v3,v1} {v2})`,
1191 SUBGOAL_THEN `{v3:real^A,v1,v2} = {v1,v2,v3} /\ {v2,v3,v1}={v1,v2,v3}` MP_TAC THENL
1192 [SET_TAC[] ; ASM_MESON_TAC[COLLINEAR_DISJOINT3]]);;
1194 let simp_def_ge = prove(` !a:real^A b v0.
1195 DISJOINT {a, b} {v0}
1197 aff_ge {a, b} {v0} =
1201 x = ta % a + tb % b + t % v0} `,
1202 MESON_TAC[simp_def2]);;
1205 let IN_CONV3_EQ = prove(`! (v:real^3) v1 v2 v3. ~collinear {v1,v2,v3} ==> (v IN conv {v1, v2, v3} <=>
1206 v IN aff_ge {v1,v2} {v3} /\
1207 v IN aff_ge {v2,v3} {v1} /\ v IN aff_ge {v3,v1} {v2} )`,
1208 SIMP_TAC[CONV_SET3; COLLINEAR_DISJOINT_PERM3;simp_def_ge; IN_ELIM_THM] THEN
1209 REPEAT GEN_TAC THEN DISCH_TAC THEN EQ_TAC THENL [
1210 MESON_TAC[REAL_ARITH` a + b + c = b + a + c /\ a + b + c = c + b + a `;
1211 VECTOR_ARITH `(a:real^N) + b + c = b + a + c /\ a + b + c = c + b + a `; lem11];
1212 NHANH (MESON[]` (? a b c. P a b c /\ Q c /\ R a b c) /\ aa /\ bb ==>
1213 (? a b c. P a b c /\ R a b c) `) THEN
1214 FIRST_X_ASSUM MP_TAC THEN
1215 REWRITE_TAC[IMP_IMP] THEN
1216 REWRITE_TAC[MESON[]` ~a/\ b <=> b /\ ~ a `] THEN
1218 NHANH (SPEC_ALL lem11) THEN
1219 STRIP_TR THEN REWRITE_TAC[MESON[]` (v = w:real^N) /\ a <=> a /\ v = w `] THEN PHA] THEN
1220 NHANH (MESON[VEC_PER2_3; REAL_PER3]` ta + tb + t = &1 /\
1222 ta' + tb' + t' = &1 /\
1224 ta'' + tb'' + t'' = &1 /\
1228 t1 + t2 + t3 = &1 /\
1230 ta + tb + tc = &1 /\ v = ta % v1 + tb % v2 + tc % v3
1231 ==> ta = t1 /\ tb = t2 /\ tc = t3) /\
1232 v = t1 % v1 + t2 % v2 + t3 % v3 /\
1234 v = ta'' % v3 + tb'' % v1 + t'' % v2 /\
1235 v = ta' % v2 + tb' % v3 + t' % v1 /\
1236 v = ta % v1 + tb % v2 + t % v3 ==> t1 = t' /\ t2 = t'' /\ t3 = t`) THEN
1240 let IN_CONV03_EQ = prove(
1241 `! (v:real^3) v1 v2 v3. ~collinear {v1,v2,v3} ==>
1242 (v IN conv0 {v1, v2, v3} <=> v IN aff_gt {v1,v2} {v3} /\
1243 v IN aff_gt {v2,v3} {v1} /\ v IN aff_gt {v3,v1} {v2} )`,
1244 SIMP_TAC[CONV_SET3; COLLINEAR_DISJOINT_PERM3;simp_def2; IN_ELIM_THM] THEN
1245 REPEAT GEN_TAC THEN DISCH_TAC THEN EQ_TAC THENL [
1246 MESON_TAC[REAL_ARITH` a + b + c = b + a + c /\ a + b + c = c + b + a `;
1247 VECTOR_ARITH `(a:real^N) + b + c = b + a + c /\ a + b + c = c + b + a `; lem11];
1248 NHANH (MESON[]` (? a b c. P a b c /\ Q c /\ R a b c) /\ aa /\ bb ==>
1249 (? a b c. P a b c /\ R a b c) `) THEN
1250 FIRST_X_ASSUM MP_TAC THEN
1251 REWRITE_TAC[IMP_IMP] THEN
1252 REWRITE_TAC[MESON[]` ~a/\ b <=> b /\ ~ a `] THEN
1254 NHANH (SPEC_ALL lem11) THEN
1255 STRIP_TR THEN REWRITE_TAC[MESON[]` (v = w:real^N) /\ a <=> a /\ v = w `]]
1256 THEN PHA THEN NHANH (MESON[VEC_PER2_3; REAL_PER3]`
1259 ta' + tb' + t' = &1 /\
1261 ta'' + tb'' + t'' = &1 /\
1262 &0 < t'' /\ a33 /\ a22 /\
1263 t1 + t2 + t3 = &1 /\
1265 ta + tb + tc = &1 /\ v = ta % v1 + tb % v2 + tc % v3
1266 ==> ta = t1 /\ tb = t2 /\ tc = t3) /\
1267 v = t1 % v1 + t2 % v2 + t3 % v3 /\ a11 /\
1268 v = ta'' % v3 + tb'' % v1 + t'' % v2 /\
1269 v = ta' % v2 + tb' % v3 + t' % v1 /\
1270 v = ta % v1 + tb % v2 + t % v3 ==>
1271 t1 = t' /\ t2 = t'' /\ t3 = t `) THEN MESON_TAC[]);;
1274 let AFFINE_SET_GEN_BY_TWO_POINTS =
1275 prove(`! a b. affine {x | ?ta tb. ta + tb = &1 /\ x = ta % a + tb % b}`,
1276 REWRITE_TAC[affine; IN_ELIM_THM] THEN
1279 EXISTS_TAC ` u * ta + v * ta' ` THEN
1280 EXISTS_TAC ` u * tb + v * tb' ` THEN
1281 REWRITE_TAC[REAL_ARITH ` (u * ta + v * ta') + u * tb + v * tb' =
1282 u * (ta + tb) + v * (ta' + tb' ) `] THEN
1283 ASM_SIMP_TAC[REAL_ARITH ` a * &1 = a `] THEN
1284 CONV_TAC VECTOR_ARITH);;
1286 let SET2_SU_EX = SET_RULE` {(a:A),b} SUBSET s <=> a IN s /\ b IN s `;;
1288 let GENERATING_POINT_IN_SET_AFF = prove(` ! a b. {a,b} SUBSET {x | ?ta tb.
1289 ta + tb = &1 /\ x = ta % a + tb % b}`,REWRITE_TAC[SET2_SU_EX; IN_ELIM_THM]
1290 THEN REPEAT GEN_TAC THEN
1291 MESON_TAC[REAL_ARITH` &0 + &1 = &1 /\ a + b = b + a`; VECTOR_ARITH `
1292 a = &0 % b + &1 % a /\ a = &1 % a + &0 % b `]);;
1295 let AFF_2POINTS_INTERPRET = prove(`!a b. aff {a, b} = {x | ?ta tb. ta + tb = &1 /\ x = ta % a + tb % b}`,
1296 REWRITE_TAC[aff; hull] THEN
1298 REWRITE_TAC[GSYM SUBSET_ANTISYM_EQ] THEN
1299 SIMP_TAC[INTERS_SUBSET; AFFINE_SET_GEN_BY_TWO_POINTS;
1300 GENERATING_POINT_IN_SET_AFF] THEN
1301 REWRITE_TAC[SUBSET; IN_ELIM_THM] THEN
1302 REWRITE_TAC[SUBSET; IN_ELIM_THM; IN_INTERS; affine] THEN
1306 (* corrected with DISJOINT by thales *)
1308 let IN_AFF_GE_INTERPRET_TO_AFF_GT_AND_AFF = prove(` ! v v1 v2 v3 .
1309 DISJOINT{v1,v2} {v3} ==>
1310 (v IN aff_ge {v1,v2} {v3} <=> v IN aff_gt {v1,v2} {v3} \/
1311 v IN aff {v1,v2}) `,
1312 REPEAT STRIP_TAC THEN
1313 ASM_SIMP_TAC[simp_def2; AFF_2POINTS_INTERPRET; IN_ELIM_THM ] THEN
1314 REWRITE_TAC [REAL_ARITH ` &0 <= a <=> &0 < a \/ a = &0 `] THEN
1315 MESON_TAC[REAL_ARITH ` (&0 <= a <=> &0 < a \/ a = &0 )/\( a + &0 = a ) `;
1316 VECTOR_ARITH ` a + &0 % c = a `]);;
1318 let DOWN_TAC = REPEAT (FIRST_X_ASSUM MP_TAC) THEN REWRITE_TAC[IMP_IMP] THEN PHA;;
1319 let IMP_IMP_TAC = REWRITE_TAC[IMP_IMP] THEN PHA;;
1322 let AFFINE_AFF_HULL = prove(` ! s. affine ( aff s ) `,
1323 REWRITE_TAC[aff; AFFINE_AFFINE_HULL]);;
1326 let AFFINE_CONTAIN_LINE = prove(`! a b s. affine s /\ {a,b} SUBSET s ==>
1327 aff {a,b} SUBSET s `,
1328 REWRITE_TAC[affine ; AFF_2POINTS_INTERPRET; IN_ELIM_THM] THEN SET_TAC[]);;
1330 let VECTOR_SUB_DISTRIBUTE = VECTOR_ARITH ` ! a x y. a % x - a % y = a % ( x - y ) `;;
1333 let CHANGE_SIDE = prove(` ~( a = &0 ) ==> ( x = a % y <=> ( &1 / a) % x = y )`,
1334 MESON_TAC[ VECTOR_ARITH ` ( a * b ) % x = a % b % x `; VECTOR_MUL_LID;
1335 REAL_FIELD `~( a = &0 ) ==> a * &1 / a = &1 `; VECTOR_MUL_LCANCEL]);;
1338 let PRE_INVERSE_SUB = prove(` ! a b v w. {a, b} SUBSET aff {v, w} /\ ~(a = b)
1339 ==> {v, w} SUBSET aff {a, b}`,
1340 REWRITE_TAC[AFF_2POINTS_INTERPRET; SET2_SU_EX; IN_ELIM_THM] THEN
1341 REPEAT GEN_TAC THEN STRIP_TAC THEN REPEAT (FIRST_X_ASSUM MP_TAC) THEN
1342 REWRITE_TAC[IMP_IMP] THEN PHA THEN
1343 NHANH (MESON[]` (a:real^N) = b /\ gg /\ a' = b' /\ ll ==> a - a' = b - b' `) THEN
1344 REWRITE_TAC[VECTOR_ARITH` (ta % v + tb % w) - (ta' % v + tb' % w) =
1345 ( ta - ta') % v + ( tb - tb' ) % w `] THEN
1346 PHA THEN REWRITE_TAC[MESON[]` a = &1 /\ b <=> b /\ a = &1 `] THEN PHA THEN
1347 NHANH (REAL_ARITH ` ta + tb = &1 /\ ta' + tb' = &1 ==> ta' - ta = tb - tb' `) THEN
1348 REWRITE_TAC[VECTOR_ARITH ` a + ( x - y ) % b = a - ( y - x) % b `] THEN
1349 REWRITE_TAC[MESON[]` a - b = ta % v - tb % w /\aa/\
1350 ta = tb <=> a - b = ta % v - ta % w /\ aa /\ ta = tb `] THEN
1351 ASM_CASES_TAC `(ta:real) = ta' ` THENL [ASM_SIMP_TAC[REAL_SUB_REFL;
1352 VECTOR_MUL_LZERO; VECTOR_SUB_RZERO; VECTOR_SUB_EQ] THEN MESON_TAC[]; ALL_TAC] THEN
1353 REWRITE_TAC[VECTOR_SUB_DISTRIBUTE] THEN FIRST_X_ASSUM MP_TAC THEN
1354 ONCE_REWRITE_TAC[REAL_ARITH` ~( a = b) <=> ~( a - b = &0 )`] THEN IMP_IMP_TAC THEN
1355 REWRITE_TAC[MESON[]` ~( a = b:real) /\ l <=> l /\ ~(a = b) `; MESON[]`
1356 a = d % b /\ l <=> l /\ a = d % b `] THEN PHA THEN
1357 REWRITE_TAC[MESON[CHANGE_SIDE]` x = a % y /\ ~( a = &0 ) <=> &1 / a % x = y /\
1358 ~( a = &0 )`] THEN NHANH (MESON[VECTOR_MUL_LCANCEL]` ta - ta' = tb' - tb /\
1359 a = b /\ l ==> tb % a = tb % b /\ ta % a = ta % b `) THEN
1360 ONCE_REWRITE_TAC[MESON[]` a = (b:real^n) /\ l <=> l /\ a = b `] THEN PHA
1361 THEN REWRITE_TAC[GSYM VECTOR_SUB_DISTRIBUTE] THEN
1362 ONCE_REWRITE_TAC[VECTOR_ARITH` a = (b:real^N) /\ a1 = (b1:real^N) /\ a2 =
1363 (b2:real^N) <=> a2 = b2 /\ a + a2 = b + b2 /\ a2 - a1 = b2 - b1 `] THEN
1364 REWRITE_TAC[VECTOR_ARITH` (ta % v + tb % w) - (ta % v - ta % w) = ( ta + tb ) % w `;
1365 VECTOR_ARITH` tb % v - tb % w + ta % v + tb % w = ( ta + tb ) % v `] THEN
1366 REWRITE_TAC[VECTOR_MUL_ASSOC; VECTOR_ARITH` a - ( x % a - y % b ) =
1367 (&1 - x ) % a + y % b `] THEN REWRITE_TAC[VECTOR_ARITH` a % x - b % y + x =
1368 (a + &1 ) % x + --b % y `] THEN
1369 REWRITE_TAC[MESON[]` a = &1 /\ b = &1 /\ l <=> a = &1 /\ l /\b = &1 `] THEN
1370 DAO THEN MATCH_MP_TAC (MESON[]`( a1 /\a2/\a3/\a5 ==> l) ==>
1371 (a1/\a2/\a3/\a4/\a5/\a6 ==> l ) `) THEN PURE_ONCE_REWRITE_TAC[ MESON[]`
1372 a + b = &1 /\ P ( a + b ) <=> a + b = &1 /\ P (&1) `] THEN
1373 REWRITE_TAC[VECTOR_MUL_LID] THEN MESON_TAC[REAL_FIELD ` ~(ta - ta' = &0)
1374 ==> (tb * &1 / (ta - ta') + &1) + --(tb * &1 / (ta - ta')) = &1 /\
1375 &1 - ta * &1 / (ta - ta') + ta * &1 / (ta - ta') = &1 `]);;
1380 `!(a:real^N) b x. line x /\ {a, b} SUBSET x /\ ~(a = b) ==> x = aff {a, b}`,
1381 REWRITE_TAC[line; GSYM aff] THEN REPEAT GEN_TAC THEN STRIP_TAC THEN
1382 REWRITE_TAC[GSYM SUBSET_ANTISYM_EQ] THEN ASM_SIMP_TAC[AFFINE_AFF_HULL;
1383 AFFINE_CONTAIN_LINE] THEN STRIP_TR THEN
1384 ABBREV_TAC ` (ki : bool ) = aff {(v:real^N), (w:real^N)}
1385 SUBSET aff {(a:real^N), (b:real^N)}` THEN
1386 REWRITE_TAC[MESON[]` a/\b/\c ==> d <=> b ==> a/\c ==> d `] THEN SIMP_TAC[]
1387 THEN DISCH_TAC THEN IMP_IMP_TAC THEN
1388 NHANH (MESON[PRE_INVERSE_SUB]`{a, b} SUBSET aff {v, w} /\ aa /\ ~(a = b)
1389 ==> {v, w} SUBSET aff {a, b} `) THEN
1390 NHANH (MESON[AFFINE_AFF_HULL]` aa /\ v SUBSET aff {a, b} ==> affine (aff {a,b})`)
1391 THEN DOWN_TAC THEN MESON_TAC[AFFINE_CONTAIN_LINE]);;
1393 let RCEABUJ = LEMMA5;;
1396 let COL_EQ_UPS_0 = GEN_ALL (MESON[FHFMKIY]` collinear {(v1:real^3), v2, v3} <=>
1397 ups_x (dist (v1,v2) pow 2) (dist (v1,v3) pow 2) (dist (v2,v3) pow 2) = &0`);;
1401 let EQ_POW2_COND = prove(`!a b. &0 <= a /\ &0 <= b ==> (a = b <=> a pow 2 = b pow 2)`,
1402 REWRITE_TAC[REAL_ARITH` a = b <=> a <= b /\ b <= a `] THEN SIMP_TAC[POW2_COND]);;
1405 let D3_POS_LE = MESON[dist3; DIST_POS_LE]` ! x y. &0 <= dist3 x y `;;
1408 let delta_x12 = new_definition ` delta_x12 x12 x13 x14 x23 x24 x34 =
1409 -- x13 * x23 + -- x14 * x24 + x34 * ( -- x12 + x13 + x14 + x23 + x24 + -- x34 )
1410 + -- x12 * x34 + x13 * x24 + x14 * x23 `;;
1412 let delta_x13 = new_definition` delta_x13 x12 x13 x14 x23 x24 x34 =
1413 -- x12 * x23 + -- x14 * x34 + x12 * x34 + x24 * ( x12 + -- x13 + x14 + x23 +
1414 -- x24 + x34 ) + -- x13 * x24 + x14 * x23 `;;
1416 let delta_x14 = new_definition`delta_x14 x12 x13 x14 x23 x24 x34 =
1421 x23 * (x12 + x13 + --x14 + --x23 + x24 + x34) +
1427 prove(` ! a (b:real^N) . dist (a,b) pow 2 = ( a - b ) dot ( a- b) `,
1428 SIMP_TAC[dist; vector_norm; DOT_POS_LE; SQRT_WORKS]);;
1432 (* the following lemma is in Multivariate/convex.ml *)
1433 let AFFINE_HULL_3 = new_axiom_removed` affine hull {a,b,c} =
1434 { u % a + v % b + w % c | u + v + w = &1}`;;
1437 let LET_TR = CONV_TAC (TOP_DEPTH_CONV let_CONV);;
1441 (* lemma 16 SDIHJZK *)
1443 let TO_UYCH = prove(` &0 < ups_x a12 a13 a23 ==>
1444 delta_x12 a01 a02 a03 a12 a13 a23 / ups_x a12 a13 a23 +
1445 delta_x13 a01 a02 a03 a12 a13 a23 / ups_x a12 a13 a23 +
1446 delta_x14 a01 a02 a03 a12 a13 a23 / ups_x a12 a13 a23 =
1448 REWRITE_TAC[ups_x; delta_x12; delta_x13; delta_x14] THEN CONV_TAC REAL_FIELD);;
1453 let NOT_UPS_X_ZERO_IMP_SMT = prove(`~(ups_x a12 a13 a23 = &0)
1454 ==> (delta_x13 a01 a02 a03 a12 a13 a23 / ups_x a12 a13 a23) pow 2 * a12 +
1455 delta_x13 a01 a02 a03 a12 a13 a23 / ups_x a12 a13 a23 *
1456 delta_x14 a01 a02 a03 a12 a13 a23 / ups_x a12 a13 a23 *
1458 (delta_x14 a01 a02 a03 a12 a13 a23 / ups_x a12 a13 a23) pow 2 * a13
1460 a01 - delta a01 a02 a03 a12 a13 a23 / ups_x a12 a13 a23 /\
1462 (delta_x14 a01 a02 a03 a12 a13 a23 / ups_x a12 a13 a23) pow 2 * a23 +
1463 delta_x14 a01 a02 a03 a12 a13 a23 / ups_x a12 a13 a23 *
1464 delta_x12 a01 a02 a03 a12 a13 a23 / ups_x a12 a13 a23 *
1466 (delta_x12 a01 a02 a03 a12 a13 a23 / ups_x a12 a13 a23) pow 2 * a12
1468 a02 - delta a01 a02 a03 a12 a13 a23 / ups_x a12 a13 a23 /\
1470 (delta_x12 a01 a02 a03 a12 a13 a23 / ups_x a12 a13 a23) pow 2 * a13 +
1471 delta_x12 a01 a02 a03 a12 a13 a23 / ups_x a12 a13 a23 *
1472 delta_x13 a01 a02 a03 a12 a13 a23 / ups_x a12 a13 a23 *
1474 (delta_x13 a01 a02 a03 a12 a13 a23 / ups_x a12 a13 a23) pow 2 * a23 =
1475 a03 - delta a01 a02 a03 a12 a13 a23 / ups_x a12 a13 a23`,
1476 ONCE_REWRITE_TAC[REAL_FIELD` ~( a = &0 ) ==> ( x = y ) /\ ( xx = yy ) /\ ( xxx = yyy)
1477 <=> ~( a = &0 ) ==> ( x * a pow 2 = y * a pow 2 ) /\
1478 ( xx * a pow 2 = yy * a pow 2 ) /\
1479 ( xxx * a pow 2 = yyy * a pow 2 ) `] THEN
1480 SIMP_TAC[REAL_FIELD` ~( a = &0 ) ==> ( b - c / a ) * a pow 2 = b * a pow 2 - c * a `
1481 ; REAL_ADD_RDISTRIB] THEN
1482 SIMP_TAC[REAL_ARITH` ( a * b ) * c = a * b * c `;
1483 REAL_FIELD` ~ ( a = &0 ) ==> ( b / a ) pow 2 * c * a pow 2 =
1484 b pow 2 * c `; REAL_FIELD ` ~ ( a = &0 ) ==> b / a * c / a * d *
1485 a pow 2 = b * c * d `] THEN DISCH_TAC THEN
1486 REWRITE_TAC[delta_x12; delta_x13; delta_x14; delta; ups_x] THEN REAL_ARITH_TAC);;
1489 let TROI_OI_DAT_HOI = MESON[ lemma8; dist; DIST_SYM]` &0 <=
1490 ups_x ( dist((v1:real^3),v2) pow 2) (dist(v2,v3) pow 2)
1491 (dist(v1,v3) pow 2)`;;
1495 let ZERO_LE_UPS_X = MESON[TROI_OI_DAT_HOI; dist3; DIST_SYM]`
1496 &0 <= ups_x (dist3 x y pow 2) (dist3 x z pow 2) (dist3 y z pow 2) `;;
1499 let UPS_X_EQ_ZERO_COND = prove(` ! v1 v2 (v3: real^3). (collinear {v1, v2, v3} <=>
1500 ups_x (dist (v1,v2) pow 2) (dist (v1,v3) pow 2)
1501 (dist (v2,v3) pow 2) =
1503 MP_TAC FHFMKIY THEN MESON_TAC[]);;
1507 let NORM_POW2_SUM2 = prove(` norm ( a % x + b % y ) pow 2 =
1508 a pow 2 * norm x pow 2 + &2 * ( a * b ) * ( x dot y ) +
1509 b pow 2 * norm y pow 2 `, REWRITE_TAC[vector_norm] THEN
1510 SIMP_TAC[DOT_POS_LE; SQRT_WORKS] THEN CONV_TAC VECTOR_ARITH);;
1514 let X_DOT_X_EQ = prove( ` x dot x = norm x pow 2 `,
1515 SIMP_TAC[vector_norm; DOT_POS_LE; SQRT_WORKS]);;
1519 let SUB_DIST_POW2_INTERPRETE = prove(`! x y (v:real^N) c.
1520 dist(x,v) pow 2 - dist(y,v) pow 2 = c <=>
1521 ( &2 % v - ( x + y )) dot ( y - x ) = c `,
1522 SIMP_TAC[DIST_POW2_DOT; DOT_SUB_ADD; VECTOR_ARITH`
1523 (x - v - (y - v)) dot (x - v + y - v) = (&2 % v - (x + y)) dot (y - x) `]);;
1525 let D3_SYM = MESON[trg_dist3_sym]` ! x y. dist3 x y = dist3 y x `;;
1527 let REAL_DIV_LZERO = prove(
1529 REPEAT GEN_TAC THEN REWRITE_TAC[real_div; REAL_MUL_LZERO]);;
1531 let SDIHJZK = prove(`! (v1:real^3) v2 v3 (a01: real) a02 a03.
1532 ~collinear {v1, v2, v3} /\
1533 (let x12 = dist3 v1 v2 pow 2 in
1534 let x13 = dist3 v1 v3 pow 2 in
1535 let x23 = dist3 v2 v3 pow 2 in delta a01 a02 a03 x12 x13 x23 = &0)
1536 ==> (?!v0. a01 = dist3 v0 v1 pow 2 /\
1537 a02 = dist3 v0 v2 pow 2 /\
1538 a03 = dist3 v0 v3 pow 2 /\
1539 (let x12 = dist3 v1 v2 pow 2 in
1540 let x13 = dist3 v1 v3 pow 2 in
1541 let x23 = dist3 v2 v3 pow 2 in
1542 let vv = ups_x x12 x13 x23 in
1543 let t1 = delta_x12 a01 a02 a03 x12 x13 x23 / vv in
1544 let t2 = delta_x13 a01 a02 a03 x12 x13 x23 / vv in
1545 let t3 = delta_x14 a01 a02 a03 x12 x13 x23 / vv in
1546 v0 = t1 % v1 + t2 % v2 + t3 % v3 /\ t1 + t2 + t3 = &1 ))`,
1550 REWRITE_TAC[EXISTS_UNIQUE] THEN
1551 EXISTS_TAC ` delta_x12 a01 a02 a03 (dist3 v1 v2 pow 2) (dist3 v1 v3 pow 2)
1552 (dist3 v2 v3 pow 2) /
1553 ups_x (dist3 v1 v2 pow 2) (dist3 v1 v3 pow 2) (dist3 v2 v3 pow 2) %
1555 delta_x13 a01 a02 a03 (dist3 v1 v2 pow 2) (dist3 v1 v3 pow 2)
1556 (dist3 v2 v3 pow 2) /
1557 ups_x (dist3 v1 v2 pow 2) (dist3 v1 v3 pow 2) (dist3 v2 v3 pow 2) %
1559 delta_x14 a01 a02 a03 (dist3 v1 v2 pow 2) (dist3 v1 v3 pow 2)
1560 (dist3 v2 v3 pow 2) /
1561 ups_x (dist3 v1 v2 pow 2) (dist3 v1 v3 pow 2) (dist3 v2 v3 pow 2) %
1563 UNDISCH_TAC `~collinear {(v1:real^3), v2, v3}` THEN
1564 MP_TAC (GEN_ALL ZERO_LE_UPS_X) THEN
1565 REWRITE_TAC[UPS_X_EQ_ZERO_COND] THEN
1566 REWRITE_TAC[MESON[]` a ==> b ==> c <=> a /\ b ==> c `; dist3] THEN
1567 NHANH (MESON[REAL_ARITH ` &0 <= a <=> &0 < a \/ a = &0 `]`
1569 &0 <= ups_x (dist (x,y) pow 2) (dist (x,z) pow 2) (dist (y,z) pow 2)) /\
1570 ~(ups_x (dist (v1,v2) pow 2) (dist (v1,v3) pow 2) (dist (v2,v3) pow 2) = &0)
1571 ==> &0 < ups_x (dist ((v1:real^3),v2) pow 2) (dist (v1,v3) pow 2) (dist (v2,v3) pow 2) `) THEN
1572 REWRITE_TAC[ GSYM dist3] THEN
1576 UNDISCH_TAC ` &0 < ups_x (dist3 v1 v2 pow 2) (dist3 v1 v3 pow 2) (dist3 v2 v3 pow 2)` THEN
1577 ABBREV_TAC ` a12 = dist3 v1 v2 pow 2 ` THEN ABBREV_TAC ` a13 = dist3 v1 v3 pow 2 ` THEN
1578 ABBREV_TAC ` a23 = dist3 v2 v3 pow 2 ` THEN SIMP_TAC[TO_UYCH] THEN
1579 REWRITE_TAC[MESON[dist3; dist] ` aa = dist3 a b pow 2 <=> aa = norm ( a- b ) pow 2 `] THEN
1580 ONCE_REWRITE_TAC[VECTOR_ARITH ` a - b = a - &1 % b `] THEN
1581 NHANH (GSYM TO_UYCH) THEN SIMP_TAC[] THEN
1582 SIMP_TAC[VECTOR_ARITH ` (a % v1 + b % v2 + c % v3) - (a + b + c) % v2 =
1583 (b % v2 + c % v3 + a % v1) - (b + c + a) % v2 /\
1584 (a % v1 + b % v2 + c % v3) - (a + b + c) % v3 =
1585 (c % v3 + a % v1 + b % v2 ) - ( c + a + b ) % v3 `] THEN
1586 REWRITE_TAC[VECTOR_ARITH` ( a % v1 + b % v2 + c % v3) -
1587 ( a + b + c ) % v1 = b % ( v2 - v1 ) + c % ( v3 - v1 ) `] THEN
1588 REWRITE_TAC[NORM_POW2_SUM2 ; REAL_ARITH ` &2 * ( a * b ) * c = a * b * &2 * c `] THEN
1589 REWRITE_TAC[VECTOR_ARITH ` &2 * ( x dot y ) = x dot x + y dot y - ( x - y ) dot ( x - y ) `] THEN
1590 REWRITE_TAC[VECTOR_ARITH` v1 - v3 - (v2 - v3) = (v1:real^3) - v2 `] THEN
1591 REWRITE_TAC[X_DOT_X_EQ; GSYM dist; GSYM dist3] THEN
1592 SIMP_TAC[D3_SYM] THEN ASM_SIMP_TAC[] THEN STRIP_TAC THEN
1593 UNDISCH_TAC ` ~(ups_x a12 a13 a23 = &0)` THEN NHANH NOT_UPS_X_ZERO_IMP_SMT THEN
1594 ASM_SIMP_TAC[REAL_DIV_LZERO; REAL_SUB_RZERO];
1599 let HALF_OF_LE16 = prove(` ! (v1:real^3) v2 v3 (a01: real) a02 a03.
1600 ~collinear {v1, v2, v3} /\
1601 (let x12 = dist3 v1 v2 pow 2 in
1602 let x13 = dist3 v1 v3 pow 2 in
1603 let x23 = dist3 v2 v3 pow 2 in delta a01 a02 a03 x12 x13 x23 = &0)
1604 ==> ?v0. (v0 IN aff {v1, v2, v3} /\
1605 a01 = dist3 v0 v1 pow 2 /\
1606 a02 = dist3 v0 v2 pow 2 /\
1607 a03 = dist3 v0 v3 pow 2 /\
1608 (let x12 = dist3 v1 v2 pow 2 in
1609 let x13 = dist3 v1 v3 pow 2 in
1610 let x23 = dist3 v2 v3 pow 2 in
1611 let vv = ups_x x12 x13 x23 in
1612 let t1 = delta_x12 a01 a02 a03 x12 x13 x23 / vv in
1613 let t2 = delta_x13 a01 a02 a03 x12 x13 x23 / vv in
1614 let t3 = delta_x14 a01 a02 a03 x12 x13 x23 / vv in
1615 v0 = t1 % v1 + t2 % v2 + t3 % v3)) `,
1616 REPEAT GEN_TAC THEN LET_TR THEN STRIP_TAC THEN REWRITE_TAC[EXISTS_UNIQUE] THEN
1617 EXISTS_TAC ` delta_x12 a01 a02 a03 (dist3 v1 v2 pow 2) (dist3 v1 v3 pow 2)
1618 (dist3 v2 v3 pow 2) /
1619 ups_x (dist3 v1 v2 pow 2) (dist3 v1 v3 pow 2) (dist3 v2 v3 pow 2) %
1621 delta_x13 a01 a02 a03 (dist3 v1 v2 pow 2) (dist3 v1 v3 pow 2)
1622 (dist3 v2 v3 pow 2) /
1623 ups_x (dist3 v1 v2 pow 2) (dist3 v1 v3 pow 2) (dist3 v2 v3 pow 2) %
1625 delta_x14 a01 a02 a03 (dist3 v1 v2 pow 2) (dist3 v1 v3 pow 2)
1626 (dist3 v2 v3 pow 2) /
1627 ups_x (dist3 v1 v2 pow 2) (dist3 v1 v3 pow 2) (dist3 v2 v3 pow 2) %
1629 UNDISCH_TAC `~collinear {(v1:real^3), v2, v3}` THEN
1630 MP_TAC (GEN_ALL ZERO_LE_UPS_X) THEN
1631 REWRITE_TAC[UPS_X_EQ_ZERO_COND] THEN
1632 REWRITE_TAC[MESON[]` a ==> b ==> c <=> a /\ b ==> c `; dist3] THEN
1633 NHANH (MESON[REAL_ARITH ` &0 <= a <=> &0 < a \/ a = &0 `]`
1635 &0 <= ups_x (dist (x,y) pow 2) (dist (x,z) pow 2) (dist (y,z) pow 2)) /\
1636 ~(ups_x (dist (v1,v2) pow 2) (dist (v1,v3) pow 2) (dist (v2,v3) pow 2) = &0)
1637 ==> &0 < ups_x (dist ((v1:real^3),v2) pow 2) (dist (v1,v3) pow 2) (dist (v2,v3) pow 2) `) THEN
1638 REWRITE_TAC[ GSYM dist3] THEN
1640 UNDISCH_TAC ` &0 < ups_x (dist3 v1 v2 pow 2) (dist3 v1 v3 pow 2) (dist3 v2 v3 pow 2)` THEN
1641 ABBREV_TAC ` a12 = dist3 v1 v2 pow 2 ` THEN ABBREV_TAC ` a13 = dist3 v1 v3 pow 2 ` THEN
1642 ABBREV_TAC ` a23 = dist3 v2 v3 pow 2 ` THEN SIMP_TAC[TO_UYCH] THEN
1643 REWRITE_TAC[MESON[dist3; dist] ` aa = dist3 a b pow 2 <=> aa = norm ( a- b ) pow 2 `] THEN
1644 ONCE_REWRITE_TAC[VECTOR_ARITH ` a - b = a - &1 % b `] THEN
1645 NHANH (GSYM TO_UYCH) THEN SIMP_TAC[] THEN
1646 SIMP_TAC[VECTOR_ARITH ` (a % v1 + b % v2 + c % v3) - (a + b + c) % v2 =
1647 (b % v2 + c % v3 + a % v1) - (b + c + a) % v2 /\
1648 (a % v1 + b % v2 + c % v3) - (a + b + c) % v3 =
1649 (c % v3 + a % v1 + b % v2 ) - ( c + a + b ) % v3 `] THEN
1650 REWRITE_TAC[VECTOR_ARITH` ( a % v1 + b % v2 + c % v3) -
1651 ( a + b + c ) % v1 = b % ( v2 - v1 ) + c % ( v3 - v1 ) `] THEN
1652 REWRITE_TAC[NORM_POW2_SUM2 ; REAL_ARITH ` &2 * ( a * b ) * c = a * b * &2 * c `] THEN
1653 REWRITE_TAC[VECTOR_ARITH ` &2 * ( x dot y ) = x dot x + y dot y - ( x - y ) dot ( x - y ) `] THEN
1654 REWRITE_TAC[VECTOR_ARITH` v1 - v3 - (v2 - v3) = (v1:real^3) - v2 `] THEN
1655 REWRITE_TAC[X_DOT_X_EQ; GSYM dist; GSYM dist3] THEN
1656 SIMP_TAC[D3_SYM] THEN ASM_SIMP_TAC[] THEN STRIP_TAC THEN
1657 UNDISCH_TAC ` ~(ups_x a12 a13 a23 = &0)` THEN NHANH NOT_UPS_X_ZERO_IMP_SMT THEN
1658 ASM_SIMP_TAC[REAL_DIV_LZERO; REAL_SUB_RZERO] THEN
1659 REWRITE_TAC[aff; AFFINE_HULL_3; IN_ELIM_THM] THEN ASM_MESON_TAC[]);;
1664 let EQ_SUB_DIST_POW2_IMP_IDENTIFIED = prove(` ! v1 v2 v3 (u:real^N) w.
1665 {u,w} SUBSET affine hull {v1,v2,v3} /\
1666 dist (u,v2) pow 2 - dist (u,v1) pow 2 = dist (w,v2) pow 2 - dist (w,v1) pow 2 /\
1667 dist (u,v3) pow 2 - dist (u,v1) pow 2 = dist (w,v3) pow 2 - dist (w,v1) pow 2 ==>
1669 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[DIST_SYM] THEN
1670 SIMP_TAC[SUB_DIST_POW2_INTERPRETE ] THEN ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN
1671 SIMP_TAC[SUB_DIST_POW2_INTERPRETE ] THEN
1672 ONCE_REWRITE_TAC[REAL_ARITH` a = b <=> a - b = &0 `] THEN
1673 SIMP_TAC[GSYM DOT_LSUB] THEN
1674 SIMP_TAC[GSYM DOT_LSUB; VECTOR_ARITH` a - b - ( aa - b ) =
1675 (a:real^N) - aa `; GSYM VECTOR_SUB_LDISTRIB; AFFINE_HULL_3;
1676 SET2_SU_EX; IN_ELIM_THM] THEN STRIP_TAC THEN
1677 REPEAT (FIRST_X_ASSUM MP_TAC ) THEN
1678 REWRITE_TAC[MESON[]` a ==> b ==> c <=> b /\ a ==> c `] THEN
1679 NHANH (MESON[]` a = (aa:real^N) /\ la /\ b = bb /\ lb ==>
1680 a - b = aa - bb `) THEN
1681 REWRITE_TAC[REAL_ARITH` a + b = &1 <=> a = &1 - b `] THEN PHA THEN
1682 STRIP_TAC THEN FIRST_X_ASSUM MP_TAC THEN UNDISCH_TAC`u' = &1 - (v + w')` THEN
1683 UNDISCH_TAC`u'' = &1 - (v' + w'')` THEN SIMP_TAC[] THEN
1684 SIMP_TAC[VECTOR_ARITH` ((&1 - (v' + w'')) % v1 + v' % v2 + w'' % v3) -
1685 ((&1 - (v + w')) % v1 + v % v2 + w' % v3) =
1686 ( v - v' ) % ( v1 - v2 ) + (w' - w'' ) % ( v1 - v3 ) `] THEN
1687 REPEAT STRIP_TAC THEN
1688 ONCE_REWRITE_TAC[VECTOR_ARITH ` a = b <=> b - a = vec 0` ] THEN
1689 REWRITE_TAC[GSYM DOT_EQ_0] THEN FIRST_X_ASSUM MP_TAC THEN
1690 REWRITE_TAC[MESON[]` a = b ==> a dot a = &0 <=> a = b ==>
1691 a dot b = &0 `] THEN
1692 REWRITE_TAC[DOT_RADD; DOT_RMUL; REAL_ARITH ` a * ( b dot c ) + aa * bb = &0
1693 <=> a * &2 * ( b dot c ) + aa * &2 * bb = &0 `] THEN
1694 ONCE_REWRITE_TAC[GSYM DOT_LMUL] THEN
1695 ABBREV_TAC ` as = &2 % ((w:real^N) - u) dot (v1 - v2)` THEN
1696 ABBREV_TAC ` bs = &2 % ((w:real^N) - u) dot (v1 - v3)` THEN
1697 DISCH_TAC THEN ASM_SIMP_TAC[] THEN REAL_ARITH_TAC);;
1699 (* lemma 16 SDIHJZK *)
1701 let SDIHJZK = prove(`! (v1:real^3) v2 v3 (a01: real) a02 a03.
1702 ~collinear {v1, v2, v3} /\
1703 (let x12 = dist3 v1 v2 pow 2 in
1704 let x13 = dist3 v1 v3 pow 2 in
1705 let x23 = dist3 v2 v3 pow 2 in delta a01 a02 a03 x12 x13 x23 = &0)
1706 ==> (?v0. v0 IN aff {v1,v2,v3} /\
1707 a01 = dist3 v0 v1 pow 2 /\
1708 a02 = dist3 v0 v2 pow 2 /\
1709 a03 = dist3 v0 v3 pow 2 /\
1710 (! vv0. vv0 IN aff {v1,v2,v3} /\
1711 a01 = dist3 vv0 v1 pow 2 /\
1712 a02 = dist3 vv0 v2 pow 2 /\
1713 a03 = dist3 vv0 v3 pow 2 ==> vv0 = v0 ) /\
1714 (let x12 = dist3 v1 v2 pow 2 in
1715 let x13 = dist3 v1 v3 pow 2 in
1716 let x23 = dist3 v2 v3 pow 2 in
1717 let vv = ups_x x12 x13 x23 in
1718 let t1 = delta_x12 a01 a02 a03 x12 x13 x23 / vv in
1719 let t2 = delta_x13 a01 a02 a03 x12 x13 x23 / vv in
1720 let t3 = delta_x14 a01 a02 a03 x12 x13 x23 / vv in
1721 v0 = t1 % v1 + t2 % v2 + t3 % v3))`,
1722 REPEAT GEN_TAC THEN NHANH (SPEC_ALL HALF_OF_LE16 ) THEN STRIP_TAC THEN
1723 EXISTS_TAC `v0:real^3` THEN ASM_SIMP_TAC[] THEN
1724 GEN_TAC THEN UNDISCH_TAC ` (v0:real^3) IN aff {v1, v2, v3}` THEN
1725 ONCE_REWRITE_TAC[REAL_ARITH ` a1 = b1 /\ a2 = b2 /\ a3 = b3 <=>
1726 a2 - a1 = b2 - b1 /\ a3 - a1 = b3 - b1 /\ a1 = b1 `] THEN
1727 REWRITE_TAC[aff; SET2_SU_EX] THEN REWRITE_TAC[dist3] THEN
1728 PHA THEN MESON_TAC[SET2_SU_EX; EQ_SUB_DIST_POW2_IMP_IDENTIFIED]);;
1732 let SDIHJZK_INTERPRETE = prove(`!(v1:real^3) v2 v3 a01 a02 a03.
1733 ~collinear {v1, v2, v3} /\
1734 delta a01 a02 a03 (dist3 v1 v2 pow 2) (dist3 v1 v3 pow 2) (dist3 v2 v3 pow 2) =
1736 ==> (?v0. v0 IN aff {v1, v2, v3} /\
1737 a01 = dist3 v0 v1 pow 2 /\
1738 a02 = dist3 v0 v2 pow 2 /\
1739 a03 = dist3 v0 v3 pow 2 /\
1740 (!vv0. vv0 IN aff {v1, v2, v3} /\
1741 a01 = dist3 vv0 v1 pow 2 /\
1742 a02 = dist3 vv0 v2 pow 2 /\
1743 a03 = dist3 vv0 v3 pow 2
1746 delta_x12 a01 a02 a03 (dist3 v1 v2 pow 2) (dist3 v1 v3 pow 2)
1747 (dist3 v2 v3 pow 2) /
1748 ups_x (dist3 v1 v2 pow 2) (dist3 v1 v3 pow 2) (dist3 v2 v3 pow 2) %
1750 delta_x13 a01 a02 a03 (dist3 v1 v2 pow 2) (dist3 v1 v3 pow 2)
1751 (dist3 v2 v3 pow 2) /
1752 ups_x (dist3 v1 v2 pow 2) (dist3 v1 v3 pow 2) (dist3 v2 v3 pow 2) %
1754 delta_x14 a01 a02 a03 (dist3 v1 v2 pow 2) (dist3 v1 v3 pow 2)
1755 (dist3 v2 v3 pow 2) /
1756 ups_x (dist3 v1 v2 pow 2) (dist3 v1 v3 pow 2) (dist3 v2 v3 pow 2) %
1757 v3)`, MP_TAC SDIHJZK THEN LET_TR THEN SIMP_TAC[]);;
1761 let DELTA_RRR_INTERPRETE = prove(` delta r r r a b c = -- a * b * c + r * ups_x a b c `,
1762 REWRITE_TAC[delta; ups_x] THEN REAL_ARITH_TAC);;
1765 let NOT_UPS_X_EQ_0_IMP = prove(` ~( ups_x a b c = &0 )
1766 ==> delta ( ( a * b * c ) / ups_x a b c ) ( ( a * b * c ) / ups_x a b c )
1767 ( ( a * b * c ) / ups_x a b c ) a b c = &0 `,
1768 REWRITE_TAC[DELTA_RRR_INTERPRETE ] THEN CONV_TAC REAL_FIELD);;
1773 let COL_EQ_UPS_0 = GEN_ALL (MESON[FHFMKIY]` collinear {(v1:real^3), v2, v3} <=>
1774 ups_x (dist (v1,v2) pow 2) (dist (v1,v3) pow 2) (dist (v2,v3) pow 2) = &0`);;
1777 (* CDEUSDF POST ZERO_LE_UPS_X *)
1780 let REAL_LE_SQUARE_POW =
1781 MESON[REAL_POW_2; REAL_LE_SQUARE]`! x. &0 <= x pow 2 `;;
1784 let PROVE_EXISTS_RADV = prove(`!(va:real^3) vb vc.
1785 ~collinear {va, vb, vc}
1786 ==> (?p. p IN affine hull {va, vb, vc} /\
1787 (?c. ( !w. w IN {va, vb, vc} ==> c = dist (p,w)) /\
1788 (!p'. p' IN affine hull {va, vb, vc} /\
1789 ( !w. w IN {va, vb, vc} ==> c = dist (p',w))
1791 REWRITE_TAC[COL_EQ_UPS_0] THEN
1792 NHANH (NOT_UPS_X_EQ_0_IMP ) THEN
1793 REWRITE_TAC[GSYM COL_EQ_UPS_0] THEN
1794 REWRITE_TAC[GSYM dist3] THEN
1795 NHANH (SPEC_ALL SDIHJZK_INTERPRETE) THEN
1796 REWRITE_TAC[EXISTS_UNIQUE] THEN
1797 REPEAT STRIP_TAC THEN
1798 ABBREV_TAC ` r = (dist3 va vb pow 2 * dist3 va vc pow 2 * dist3 vb vc pow 2) /
1799 ups_x (dist3 va vb pow 2) (dist3 va vc pow 2) (dist3 vb vc pow 2) ` THEN
1800 EXISTS_TAC ` v0 :real^3` THEN
1801 UNDISCH_TAC ` (v0:real^3) IN aff {va, vb, vc}` THEN
1802 SIMP_TAC[aff; SET_RULE ` (! x. x IN {a,b,c} ==> P x ) <=>
1803 P a /\ P b /\ P c `] THEN
1804 DISCH_TAC THEN EXISTS_TAC ` sqrt ( r ) ` THEN
1805 UNDISCH_TAC ` (dist3 va vb pow 2 * dist3 va vc pow 2 * dist3 vb vc pow 2) /
1806 ups_x (dist3 va vb pow 2) (dist3 va vc pow 2) (dist3 vb vc pow 2) = r` THEN
1807 NHANH (MESON[REAL_LE_SQUARE_POW; REAL_LE_DIV; REAL_LE_MUL;
1808 ZERO_LE_UPS_X ]` (dist3 va vb pow 2 * dist3 va vc pow 2 * dist3 vb vc pow 2) /
1809 ups_x (dist3 va vb pow 2) (dist3 va vc pow 2) (dist3 vb vc pow 2) =
1810 r ==> &0 <= r `) THEN
1811 SIMP_TAC[SQRT_WORKS; EQ_POW2_COND; D3_POS_LE] THEN
1812 ASM_MESON_TAC[aff]);;
1817 let COND_FOR_CIRCUMCENTER_PROPERTIESS = prove(`~collinear {(v1:real^3), v2, v3}
1818 ==> circumcenter {v1, v2, v3} IN affine hull {v1, v2, v3} /\
1819 (?c. !v. v IN {v1, v2, v3} ==> c = dist (circumcenter {v1, v2, v3}, v))`,
1820 NHANH (MESON[PROVE_EXISTS_RADV]`~collinear {(va:real^3), vb, vc}
1821 ==> (?p. p IN affine hull {va, vb, vc} /\
1822 (?c. (!w. w IN {va, vb, vc} ==> c = dist (p,w)))) `) THEN
1823 REWRITE_TAC[IN; circumcenter] THEN MESON_TAC[EXISTS_THM]);;
1826 let DELTA_X14_RRR = prove(` delta_x14 r r r a b c = a * ( b + c - a ) `,
1827 REWRITE_TAC[delta_x14] THEN REAL_ARITH_TAC);;
1830 let DELTA_X1I_RRR = prove(` delta_x12 r r r a b c = c * ( b + a - c ) /\
1831 delta_x13 r r r a b c = b * ( c + a - b ) /\
1832 delta_x14 r r r a b c = a * (c + b - a) `,
1833 REWRITE_TAC[delta_x12; delta_x13; delta_x14] THEN REAL_ARITH_TAC);;
1839 let PRE_RADV_COND = prove(` ~ collinear {va,vb,vc} ==>
1840 (? c. ! w. {va,vb,(vc:real^3)} w ==> c = dist(circumcenter {va,vb,vc} , w )) `,
1841 NHANH (COND_FOR_CIRCUMCENTER_PROPERTIESS ) THEN MESON_TAC[IN]);;
1844 let NOT_COL_IMP_RADV_PROPERTIY = prove(` ~collinear {(va:real^3), vb, vc}
1845 ==> ( ! w. {va, vb, vc} w ==>
1846 radV {va, vb, vc} = dist (circumcenter {va, vb, vc},w)) `,
1847 NHANH (PRE_RADV_COND ) THEN SIMP_TAC[EXISTS_THM; radV]);;
1852 let CIRCUMCENTER_FORMULAR2 = prove(`! (va:real^3) vb vc a b c.
1853 a = dist3 vb vc /\ b = dist3 va vc /\ c = dist3 va vb /\ ~collinear {va, vb, vc}
1856 (a pow 2 * (b pow 2 + c pow 2 - a pow 2)) /
1857 (ups_x (a pow 2) (b pow 2) (c pow 2)) in
1859 (b pow 2 * (a pow 2 + c pow 2 - b pow 2)) /
1860 (ups_x (a pow 2) (b pow 2) (c pow 2)) in
1862 (c pow 2 * (a pow 2 + b pow 2 - c pow 2)) /
1863 (ups_x (a pow 2) (b pow 2) (c pow 2)) in
1864 al_a % va + al_b % vb + al_c % vc = circumcenter {va, vb, vc})`,
1865 REWRITE_TAC[COL_EQ_UPS_0] THEN
1866 NHANH (NOT_UPS_X_EQ_0_IMP) THEN
1867 REWRITE_TAC[GSYM COL_EQ_UPS_0; GSYM dist3] THEN
1868 NHANH (SPEC_ALL SDIHJZK_INTERPRETE ) THEN
1869 REPEAT STRIP_TAC THEN
1870 ABBREV_TAC ` r = (dist3 va vb pow 2 * dist3 va vc pow 2 * dist3 vb vc pow 2) /
1871 ups_x (dist3 va vb pow 2) (dist3 va vc pow 2) (dist3 vb vc pow 2) ` THEN
1873 delta_x12 r r r (dist3 va vb pow 2) (dist3 va vc pow 2) (dist3 vb vc pow 2) /
1874 ups_x (dist3 va vb pow 2) (dist3 va vc pow 2) (dist3 vb vc pow 2) %
1876 delta_x13 r r r (dist3 va vb pow 2) (dist3 va vc pow 2) (dist3 vb vc pow 2) /
1877 ups_x (dist3 va vb pow 2) (dist3 va vc pow 2) (dist3 vb vc pow 2) %
1879 delta_x14 r r r (dist3 va vb pow 2) (dist3 va vc pow 2) (dist3 vb vc pow 2) /
1880 ups_x (dist3 va vb pow 2) (dist3 va vc pow 2) (dist3 vb vc pow 2) %
1883 UNDISCH_TAC ` a = dist3 vb vc ` THEN
1884 UNDISCH_TAC ` b = dist3 va vc ` THEN
1885 UNDISCH_TAC ` c = dist3 va vb ` THEN
1886 SIMP_TAC[DELTA_X1I_RRR] THEN
1887 SIMP_TAC[MESON[UPS_X_SYM]` ups_x a b c = ups_x c b a `] THEN
1888 ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN
1890 REPEAT STRIP_TAC THEN
1891 UNDISCH_TAC ` ~collinear {(va:real^3), vb, vc} ` THEN
1892 NHANH (COND_FOR_CIRCUMCENTER_PROPERTIESS) THEN
1893 REWRITE_TAC[SET_RULE ` (! x. x IN {a,b,c} ==> P x )
1894 <=> P a /\ P b /\ P c `] THEN
1895 REWRITE_TAC[SET_RULE ` (! x. x IN {a,b,c} ==> P x )
1896 <=> P a /\ P b /\ P c `; MESON[]` (? cc. cc = a /\ cc = b /\ cc = c)
1897 <=> a = b /\ a = c `] THEN
1898 UNDISCH_TAC ` v0 IN aff {va, vb, (vc:real^3)}` THEN
1899 REWRITE_TAC[aff; SET_RULE ` a IN s ==> b /\ aa IN s /\ l ==>
1900 ll <=> b ==> {a,aa} SUBSET s /\ l ==> ll `] THEN
1902 UNDISCH_TAC` r = dist3 v0 va pow 2 ` THEN
1903 UNDISCH_TAC` r = dist3 v0 vb pow 2 ` THEN
1904 UNDISCH_TAC` r = dist3 v0 vc pow 2 ` THEN
1905 REWRITE_TAC[MESON[]` r = a1 ==> r = a2 ==> r = a3 ==> l ==> ll <=>
1906 r = a1 /\ l /\ a2 = a3 /\ a1 = a3 ==> ll `;dist3] THEN
1907 ONCE_REWRITE_TAC[MESON[]` dist(a,b) = s <=> s = dist(a,b) `] THEN
1908 SIMP_TAC[DIST_POS_LE; EQ_POW2_COND] THEN
1909 ONCE_REWRITE_TAC[REAL_ARITH` a = b <=> a - b = &0 `] THEN
1910 MESON_TAC[EQ_SUB_DIST_POW2_IMP_IDENTIFIED ]);;
1912 let REAL_LE_POW_2 = prove(` ! x. &0 <= x pow 2 `,
1913 REWRITE_TAC[REAL_POW_2; REAL_LE_SQUARE]);;
1917 let NOT_COLL_IMP_RADV_FORMULAR = prove(`! (va:real^3) vb vc a b c.
1918 a = dist3 vb vc /\ b = dist3 va vc /\ c = dist3 va vb /\ ~collinear {va, vb, vc}
1919 ==> radV {va, vb, vc} = eta_y a b c`,
1920 REWRITE_TAC[COL_EQ_UPS_0] THEN
1921 NHANH (NOT_UPS_X_EQ_0_IMP) THEN
1922 REWRITE_TAC[GSYM COL_EQ_UPS_0; GSYM dist3] THEN
1923 NHANH (SPEC_ALL SDIHJZK_INTERPRETE ) THEN
1924 REPEAT STRIP_TAC THEN
1925 ABBREV_TAC ` r = (dist3 va vb pow 2 * dist3 va vc pow 2 * dist3 vb vc pow 2) /
1926 ups_x (dist3 va vb pow 2) (dist3 va vc pow 2) (dist3 vb vc pow 2) ` THEN
1928 UNDISCH_TAC ` a = dist3 vb vc ` THEN
1929 UNDISCH_TAC ` b = dist3 va vc ` THEN
1930 UNDISCH_TAC ` c = dist3 va vb ` THEN
1931 SIMP_TAC[DELTA_X1I_RRR] THEN
1932 SIMP_TAC[MESON[UPS_X_SYM]` ups_x a b c = ups_x c b a `] THEN
1933 ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN
1935 REPEAT STRIP_TAC THEN
1936 UNDISCH_TAC ` ~collinear {(va:real^3), vb, vc} ` THEN
1937 NHANH (COND_FOR_CIRCUMCENTER_PROPERTIESS) THEN
1938 REWRITE_TAC[SET_RULE ` (! x. x IN {a,b,c} ==> P x )
1939 <=> P a /\ P b /\ P c `] THEN
1940 REWRITE_TAC[SET_RULE ` (! x. x IN {a,b,c} ==> P x )
1941 <=> P a /\ P b /\ P c `; MESON[]` (? cc. cc = a /\ cc = b /\ cc = c)
1942 <=> a = b /\ a = c `] THEN
1943 UNDISCH_TAC ` v0 IN aff {va, vb, (vc:real^3)}` THEN
1944 REWRITE_TAC[aff; SET_RULE ` a IN s ==> b /\ aa IN s /\ l ==>
1945 ll <=> b ==> {a,aa} SUBSET s /\ l ==> ll `] THEN
1947 UNDISCH_TAC` r = dist3 v0 va pow 2 ` THEN
1948 UNDISCH_TAC` r = dist3 v0 vb pow 2 ` THEN
1949 UNDISCH_TAC` r = dist3 v0 vc pow 2 ` THEN
1950 REWRITE_TAC[MESON[]` r = a1 ==> r = a2 ==> r = a3 ==> l ==> ll <=>
1951 r = a1 /\ l /\ a2 = a3 /\ a1 = a3 ==> ll `;dist3] THEN
1952 ONCE_REWRITE_TAC[MESON[]` dist(a,b) = s <=> s = dist(a,b) `] THEN
1953 SIMP_TAC[DIST_POS_LE; EQ_POW2_COND] THEN
1954 ONCE_REWRITE_TAC[REAL_ARITH` a = b <=> a - b = &0 `] THEN
1955 REWRITE_TAC[MESON[]` ( a /\ a1 = &0 /\ a2 = &0 ) /\ b1 = &0 /\ b2 = &0 <=>
1956 b1 = &0 /\ b2 = &0 /\ a /\ b1 = a1 /\ b2 = a2 `] THEN
1957 NHANH (SPEC_ALL EQ_SUB_DIST_POW2_IMP_IDENTIFIED ) THEN
1959 UNDISCH_TAC ` ~collinear {(va:real^3), vb, vc}` THEN
1960 NHANH (NOT_COL_IMP_RADV_PROPERTIY ) THEN
1961 FIRST_X_ASSUM MP_TAC THEN
1963 SIMP_TAC[SET_RULE ` (!w. {va, vb, vc} w ==> P w ) <=>
1964 P va /\ P vb /\ P vc `] THEN
1965 REPEAT STRIP_TAC THEN
1969 UNDISCH_TAC ` r - dist ((v0:real^3),vc) pow 2 = &0 ` THEN
1970 SIMP_TAC[REAL_ARITH` a - b = &0 <=> b = a `] THEN
1972 REWRITE_TAC[eta_y; eta_x] THEN
1974 MP_TAC (GEN_ALL ZERO_LE_UPS_X) THEN
1975 SIMP_TAC[GSYM REAL_POW_2] THEN
1976 SIMP_TAC[REAL_ARITH` a * b * c = c * b * a `;
1977 UPS_X_SYM; dist3] THEN
1978 MP_TAC (MESON[dist3; DIST_POS_LE]` &0 <= dist3 v0 vc `) THEN
1979 MP_TAC (MESON[REAL_LE_DIV; REAL_LE_MUL_EQ; REAL_LE_POW_2;REAL_LE_MUL; ZERO_LE_UPS_X;
1980 SQRT_WORKS]` &0 <= ((dist3 va vb pow 2 * dist3 va vc pow 2 * dist3 vb vc pow 2) /
1981 ups_x (dist3 va vb pow 2) (dist3 va vc pow 2) (dist3 vb vc pow 2)) /\
1982 &0 <= sqrt ((dist3 va vb pow 2 * dist3 va vc pow 2 * dist3 vb vc pow 2) /
1983 ups_x (dist3 va vb pow 2) (dist3 va vc pow 2) (dist3 vb vc pow 2)) `) THEN
1984 REWRITE_TAC[MESON[]` a ==> b ==> c <=> b /\ a ==> c `] THEN
1985 MATCH_MP_TAC (MESON[]` (a1 /\ a3 ==> l) ==> a1 /\a2 /\a3 ==> l`) THEN
1986 SIMP_TAC[dist3; EQ_POW2_COND; SQRT_WORKS]);;
1989 let CDEUSDF = prove(`!(va:real^3) vb vc a b c.
1990 a = dist3 vb vc /\ b = dist3 va vc /\ c = dist3 va vb /\ ~collinear {va, vb, vc}
1991 ==> (?p. p IN affine hull {va, vb, vc} /\
1992 (?c. ( !w. w IN {va, vb, vc} ==> c = dist (p,w)) /\
1993 (!p'. p' IN affine hull {va, vb, vc} /\
1994 ( !w. w IN {va, vb, vc} ==> c = dist (p',w))
1997 (a pow 2 * (b pow 2 + c pow 2 - a pow 2)) /
1998 (ups_x (a pow 2) (b pow 2) (c pow 2)) in
2000 (b pow 2 * (a pow 2 + c pow 2 - b pow 2)) /
2001 (ups_x (a pow 2) (b pow 2) (c pow 2)) in
2003 (c pow 2 * (a pow 2 + b pow 2 - c pow 2)) /
2004 (ups_x (a pow 2) (b pow 2) (c pow 2)) in
2005 al_a % va + al_b % vb + al_c % vc = circumcenter {va, vb, vc}) /\
2006 radV {va, vb, vc} = eta_y a b c`,
2007 SIMP_TAC[PROVE_EXISTS_RADV; CIRCUMCENTER_FORMULAR2; NOT_COLL_IMP_RADV_FORMULAR ]);;
2009 let LEMMA17 = CDEUSDF;;
2011 let DIST_EQ_IS_UNIQUE = prove(` {u, w} SUBSET affine hull {v1, v2, v3} /\
2012 dist (u,v2) = dist (u,v1) /\ dist (u,v3) = dist (u,v1) /\
2013 dist (w,v2) = dist (w,v1) /\ dist (w,v3) = dist (w,v1) ==>
2015 SIMP_TAC[EQ_POW2_COND; DIST_POS_LE] THEN ONCE_REWRITE_TAC[REAL_ARITH`
2016 a = b <=> a - b = &0 `] THEN MESON_TAC[EQ_SUB_DIST_POW2_IMP_IDENTIFIED]);;
2019 let NEVER_USED_AGAIN = prove(` p IN affine hull {va, vb, vc} /\ c = dist (p,va)
2020 /\ c = dist (p,vb) /\ c = dist (p,vc) ==>
2021 (! p'. p' IN affine hull {va, vb, vc} /\
2022 dist (p',vb) = dist (p',va) /\
2023 dist (p',vc) = dist (p',va) <=>
2024 p' IN affine hull {va, vb, vc} /\
2027 c = dist (p',vc) )`,
2028 MESON_TAC[DIST_EQ_IS_UNIQUE; SET2_SU_EX]);;
2032 let TRUONG_WELL = prove(`! (va:real^3) vb vc. ~collinear {va, vb, vc}
2033 ==> (?p. p IN affine hull {va, vb, vc} /\
2034 (?c. !w. w IN {va, vb, vc} ==> c = dist (p,w)) /\
2035 (!p'. p' IN affine hull {va, vb, vc} /\
2036 (?c. !w. w IN {va, vb, vc} ==> c = dist (p',w))
2038 NHANH (SPEC_ALL PROVE_EXISTS_RADV) THEN REPEAT STRIP_TAC THEN EXISTS_TAC `p:real^3`
2039 THEN CONJ_TAC THENL [ASM_SIMP_TAC[]; CONJ_TAC] THENL [ASM_MESON_TAC[];
2040 REPLICATE_TAC 3 (FIRST_X_ASSUM MP_TAC) THEN
2041 REWRITE_TAC[SET_RULE` (!a. a IN {x,y,z} ==> p a)
2042 <=> p x /\ p y /\ p z `] THEN
2043 REWRITE_TAC[MESON[]` (?c. c = a /\ c = b /\ c = cc ) <=>
2044 b = a /\ cc = a `]] THEN
2045 REWRITE_TAC[MESON[]` a ==> b ==> c <=> a /\b ==> c `] THEN
2046 PHA THEN MESON_TAC[NEVER_USED_AGAIN ]);;
2051 let NGAY_MONG6 = MESON[TRUONG_WELL] `! va vb (vc:real^3).
2052 ~collinear {va, vb, vc} ==> (?p. p IN affine hull {va, vb, vc} /\
2053 (?c. !w. w IN {va, vb, vc} ==> c = dist (p,w)) ) `;;
2056 let CIRCUMCENTER_PROPTIES = prove(`!va vb (vc:real^3).
2057 ~collinear {va, vb, vc}
2058 ==> circumcenter {va, vb, vc} IN affine hull {va, vb, vc} /\
2059 (?c. !w. w IN {va, vb, vc}
2060 ==> c = dist (circumcenter {va, vb, vc},w))`,
2061 NHANH (SPEC_ALL NGAY_MONG6) THEN REWRITE_TAC[IN;
2062 circumcenter; EXISTS_THM] THEN SIMP_TAC[]);;
2069 let SIMP_DOT_ALEM = prove( `&0 < (b - a) dot x <=> x dot (a - b) < &0`,
2070 SIMP_TAC[DOT_SYM] THEN
2071 REWRITE_TAC[ REAL_ARITH ` a < &0 <=> &0 < -- a `; GSYM DOT_RNEG] THEN
2072 REWRITE_TAC[VECTOR_ARITH ` -- ((a:real^N) - b) = b - a `]);;
2077 let MONG7_ROI = prove(` ! p a (b:real^A). dist (p,a) = dist (p,b) <=>
2078 (p - &1 / &2 % ( a + b )) dot ( a - b) = &0 `,
2079 REWRITE_TAC[ REAL_ARITH ` a = b <=> ~ ( a < b) /\ ~( b < a ) `;
2080 DIST_LT_HALF_PLANE] THEN
2081 REWRITE_TAC[VECTOR_ARITH` (p - &1 / &2 % (a + b)) dot (a - b)
2082 = &1 / &2 * ( (&2 % p - (a + b ) ) dot ( a- b ) ) `] THEN
2083 REWRITE_TAC[REAL_ARITH `( &1 / &2 * a < &0 <=> a < &0) /\
2084 (&0 < &1 / &2 * a <=> &0 < a )`] THEN
2085 REWRITE_TAC[SIMP_DOT_ALEM] THEN
2086 SIMP_TAC[VECTOR_ARITH` (a - b) dot (c - d) = (b - a) dot (d - c)`; DOT_SYM;
2087 VECTOR_ADD_SYM] THEN MESON_TAC[]);;
2089 let LEMMA26 = prove(`!v1 v2 (v3:real^3) p.
2090 ~collinear {v1, v2, v3} /\ p = circumcenter {v1, v2, v3}
2091 ==> (p - &1 / &2 % (v1 + v2)) dot (v1 - v2) = &0 /\
2092 (p - &1 / &2 % (v2 + v3)) dot (v2 - v3) = &0 /\
2093 (p - &1 / &2 % (v3 + v1)) dot (v3 - v1) = &0`,
2094 NHANH (SPEC_ALL CIRCUMCENTER_PROPTIES) THEN
2095 NHANH (SET_RULE` (?c. !w. w IN {v1, v2, v3} ==> c = P w) ==> P v1 = P v2
2096 /\ P v2 = P v3 /\ P v3 = P v1 `) THEN
2097 SIMP_TAC[MONG7_ROI]);;
2099 let POXDVXO = LEMMA26;;
2103 let NOT_COLL_IMP_RADV_EQ_ETA_Y = MESON[prove(`!va vb vc a b c.
2104 a = dist3 vb vc /\ b = dist3 va vc /\ c = dist3 va vb /\ ~collinear {va, vb, vc}
2105 ==> radV {va, vb, vc} = eta_y (dist3 vb vc) (dist3 va vc) (dist3 va vb)`,
2106 SIMP_TAC[CDEUSDF])]`
2107 !va vb vc . ~collinear {va, vb, vc}
2108 ==> radV {va, vb, vc} = eta_y (dist3 vb vc) (dist3 va vc) (dist3 va vb)`;;
2110 let COLLINEAR2 = prove(` ! x (y:real^N). collinear {x,y} `,
2111 REPEAT GEN_TAC THEN REWRITE_TAC[collinear] THEN
2112 EXISTS_TAC ` x -(y: real^N)` THEN
2113 ASM_SIMP_TAC[SET_RULE` a = b ==> {a,b,c} = {a,c} `] THEN
2114 REWRITE_TAC[IN_SET2] THEN
2117 [ASM_SIMP_TAC[] THEN EXISTS_TAC ` &0 ` THEN CONV_TAC VECTOR_ARITH;
2118 ASM_SIMP_TAC[] THEN EXISTS_TAC ` &1 ` THEN CONV_TAC VECTOR_ARITH;
2119 ASM_SIMP_TAC[] THEN EXISTS_TAC ` -- &1 ` THEN CONV_TAC VECTOR_ARITH;
2120 ASM_SIMP_TAC[] THEN EXISTS_TAC ` &0 ` THEN CONV_TAC VECTOR_ARITH]
2123 let TWO_EQ_IMP_COL3 = prove(` ! (x:real^N) y z . x = y ==> collinear {x, y, z} `,
2124 STRIP_TR THEN SIMP_TAC[SET_RULE` a = b ==> {a,b,c} = {a,c} `; COLLINEAR2]);;
2127 let NOT_CO_IMP_DIST_POS = prove(`! x y z. ~ collinear {x,y,z} ==> &0 < dist (x,y) `,
2128 NHANH (MESON[TWO_EQ_IMP_COL3]` ~collinear {x, y, z} ==> ~( x= y) `) THEN
2129 SIMP_TAC[DIST_POS_LT]);;
2132 let NOT_COLL_IMP_POS_SUM = prove( ` !x y z.
2133 ~collinear {x, y, z} ==> &0 < ( dist3 x y + dist3 y z + dist3 z x) / &2 `,
2134 NHANH (SPEC_ALL NOT_CO_IMP_DIST_POS) THEN
2135 NHANH (MESON[DIST_POS_LE]` ~collinear {x, y, z} ==>
2136 &0 <= dist (y,z) /\ &0 <= dist (z,x) `) THEN
2137 SIMP_TAC[dist3] THEN REAL_ARITH_TAC);;
2139 let PER_SET2 = SET_RULE ` {a,b} = {b,a} `;;
2142 let COLLINEAR_AS_IN_CONV2 = MESON[PER_SET2; COLLINERA_AS_IN_CONV2]`! x y (z:real^3). collinear {x, y, z} <=>
2143 x IN conv {y, z} \/ y IN conv {z, x} \/ z IN conv {x, y}`;;
2145 let COLLINEAR_IMP_POS_UPS2 = prove(` ! x y (z:real^3). ~ collinear {x,y,z} ==>
2146 &0 < ups_x_pow2 ( dist3 x y ) ( dist3 y z ) ( dist3 z x ) `,
2147 REWRITE_TAC[PRE_HER] THEN NHANH (SPEC_ALL NOT_COLL_IMP_POS_SUM ) THEN
2148 REWRITE_TAC[COLLINEAR_AS_IN_CONV2] THEN REWRITE_TAC[MID_COND] THEN
2149 REWRITE_TAC[LENGTH_EQ_EX] THEN REWRITE_TAC[DE_MORGAN_THM] THEN
2150 SIMP_TAC[dist3] THEN REPEAT GEN_TAC THEN SIMP_TAC[
2151 prove(` &0 < a ==> ( &0 < &16 * a * b <=> &0 < b ) `,
2152 REWRITE_TAC[REAL_ARITH ` &0 < &16 * a <=> &0 < a `] THEN
2153 REWRITE_TAC[REAL_LT_MUL_EQ])] THEN
2154 REWRITE_TAC[REAL_ARITH ` (a + b + c ) / &2 - a = ( b + c - a ) / &2 `] THEN
2155 REWRITE_TAC[REAL_ARITH ` (a + b + c ) / &2 - b = ( c + a - b ) / &2 `] THEN
2156 REWRITE_TAC[REAL_ARITH ` (a + b + c ) / &2 - c = ( a + b - c ) / &2 `] THEN
2157 REWRITE_TAC[REAL_ARITH ` a < b + c <=> &0 < ( b + c - a ) / &2 `] THEN
2158 SIMP_TAC[DIST_SYM] THEN SIMP_TAC[REAL_ARITH ` a + b - c = b + a - c `] THEN
2159 SIMP_TAC[REAL_LT_MUL]);;
2163 let RADV_FORMULAR = MESON[CDEUSDF]` !(va:real^3) vb vc.
2164 ~collinear {va, vb, vc}
2165 ==> radV {va, vb, vc} = eta_y (dist3 vb vc) (dist3 va vc) (dist3 va vb)`;;
2169 let MUL3_SYM = REAL_ARITH ` ! a b c. a * b * c = b * a * c /\
2170 a * b * c = c * b * a `;;
2172 let ETA_X_SYMM = prove(` ! a b c. eta_x a b c = eta_x b a c /\
2173 eta_x a b c = eta_x c b a `,SIMP_TAC[eta_x; MUL3_SYM; UPS_X_SYM]);;
2175 let ETA_Y_SYYM = prove(` ! x y z. eta_y x y z = eta_y y x z /\
2176 eta_y x y z = eta_y z y x `, REWRITE_TAC[eta_y] THEN
2177 CONV_TAC (TOP_DEPTH_CONV let_CONV) THEN MESON_TAC[ETA_X_SYMM]);;
2181 let NOT_COL3_IMP_DIFF = MESON[PER_SET3; TWO_EQ_IMP_COL3]`!a b c.
2182 ~collinear {a, b, c} ==> ~(a = b \/ a = c \/ b = c)`;;
2184 let LET_TR = CONV_TAC (TOP_DEPTH_CONV let_CONV);;
2187 let POW2_COND_LT = MESON[POW2_COND; REAL_ARITH ` &0 < a ==> &0 <= a `]`
2188 !a b. &0 < a /\ &0 < b ==> (a <= b <=> a pow 2 <= b pow 2)`;;
2191 let ETA_Y_2 = prove(` eta_y (&2) (&2) (&2) = &2 / sqrt (&3) `,
2192 REWRITE_TAC[eta_y; eta_x; ups_x] THEN
2194 REWRITE_TAC[REAL_ARITH ` ((&2 * &2) * (&2 * &2) * &2 * &2) /
2195 (--(&2 * &2) * &2 * &2 - (&2 * &2) * &2 * &2 - (&2 * &2) * &2 * &2 +
2196 &2 * (&2 * &2) * &2 * &2 +
2197 &2 * (&2 * &2) * &2 * &2 +
2198 &2 * (&2 * &2) * &2 * &2) = &4 / &3 `] THEN
2199 MP_TAC (MESON[REAL_LT_DIV; MESON[SQRT_POS_LT; REAL_ARITH` &0 < &3 `] `
2200 &0 < sqrt (&3) `; REAL_ARITH ` &0 < &2 /\ &0 < &4 /\ &0 < &3 `] ` &0 < &4 / &3
2201 /\ &0 < &2 / sqrt (&3) `) THEN
2202 REWRITE_TAC[REAL_ARITH` a = b <=> a <= b /\ b <= a `] THEN
2203 SIMP_TAC[SQRT_POS_LT; POW2_COND_LT] THEN
2204 REWRITE_TAC[GSYM (REAL_ARITH` a = b <=> a <= b /\ b <= a `)] THEN
2205 SIMP_TAC[REAL_LT_IMP_LE; SQRT_POW_2] THEN
2206 REWRITE_TAC[REAL_FIELD` (a/ b) pow 2 = a pow 2 / ( b pow 2 ) `] THEN
2207 SIMP_TAC[REAL_ARITH ` &0 <= &3 `; SQRT_POW_2] THEN
2210 let D3_POS_LE = MESON[dist3; DIST_POS_LE]` ! x y. &0 <= dist3 x y `;;
2217 let cayleytr = new_definition `
2218 cayleytr x12 x13 x14 x15 x23 x24 x25 x34 x35 x45 =
2219 &2 * x23 * x25 * x34 +
2220 &2 * x23 * x24 * x35 +
2221 -- &1 * x23 pow 2 * x45 +
2222 -- &2 * x15 * x23 * x34 +
2223 -- &2 * x15 * x23 * x24 +
2224 &2 * x15 * x23 pow 2 +
2225 -- &2 * x14 * x23 * x35 +
2226 -- &2 * x14 * x23 * x25 +
2227 &2 * x14 * x23 pow 2 +
2228 &4 * x14 * x15 * x23 +
2229 -- &2 * x13 * x25 * x34 +
2230 -- &2 * x13 * x24 * x35 +
2231 &4 * x13 * x24 * x25 +
2232 &2 * x13 * x23 * x45 +
2233 -- &2 * x13 * x23 * x25 +
2234 -- &2 * x13 * x23 * x24 +
2235 &2 * x13 * x15 * x34 +
2236 -- &2 * x13 * x15 * x24 +
2237 -- &2 * x13 * x15 * x23 +
2238 &2 * x13 * x14 * x35 +
2239 -- &2 * x13 * x14 * x25 +
2240 -- &2 * x13 * x14 * x23 +
2241 -- &1 * x13 pow 2 * x45 +
2242 &2 * x13 pow 2 * x25 +
2243 &2 * x13 pow 2 * x24 +
2244 &4 * x12 * x34 * x35 +
2245 -- &2 * x12 * x25 * x34 +
2246 -- &2 * x12 * x24 * x35 +
2247 &2 * x12 * x23 * x45 +
2248 -- &2 * x12 * x23 * x35 +
2249 -- &2 * x12 * x23 * x34 +
2250 -- &2 * x12 * x15 * x34 +
2251 &2 * x12 * x15 * x24 +
2252 -- &2 * x12 * x15 * x23 +
2253 -- &2 * x12 * x14 * x35 +
2254 &2 * x12 * x14 * x25 +
2255 -- &2 * x12 * x14 * x23 +
2256 &2 * x12 * x13 * x45 +
2257 -- &2 * x12 * x13 * x35 +
2258 -- &2 * x12 * x13 * x34 +
2259 -- &2 * x12 * x13 * x25 +
2260 -- &2 * x12 * x13 * x24 +
2261 &4 * x12 * x13 * x23 +
2262 -- &1 * x12 pow 2 * x45 +
2263 &2 * x12 pow 2 * x35 +
2264 &2 * x12 pow 2 * x34 `;;
2267 let LTCTBAN = prove(` cayleyR x12 x13 x14 x15 x23 x24 x25 x34 x35 x45 =
2268 ups_x x12 x13 x23 * x45 pow 2 + cayleytr x12 x13 x14 x15 x23 x24 x25 x34 x35 ( &0 )
2269 * x45 + cayleyR x12 x13 x14 x15 x23 x24 x25 x34 x35 ( &0 ) `,
2270 REWRITE_TAC[ups_x; cayleyR;cayleytr] THEN REAL_ARITH_TAC);;
2274 (* ------------------------------------------------------------------------- *)
2275 (* Flyspeck definitions we use. *)
2276 (* ------------------------------------------------------------------------- *)
2278 let plane = new_definition
2279 `plane x = (?u v w. ~(collinear {u,v,w}) /\ (x = affine hull {u,v,w}))`;;
2281 (* renamed from coplanar, because j. harrison changed the def. -thales *)
2283 let coplanar_alt = new_definition `coplanar_alt S = (?x. plane x /\ S SUBSET x)`;;
2286 (* renamed condA to condA, thales *)
2289 let condA = new_definition `condA (v1:real^3) v2 v3 v4 x12 x13 x14 x23 x24 x34 =
2290 ( ~ ( v1 = v2 ) /\ coplanar_alt {v1,v2,v3,v4} /\
2291 ( dist ( v1, v2) pow 2 ) = x12 /\
2292 dist (v1,v3) pow 2 = x13 /\
2293 dist (v1,v4) pow 2 = x14 /\
2294 dist (v2,v3) pow 2 = x23 /\ dist (v2,v4) pow 2 = x24 )`;;
2297 let det_vec3 = new_definition ` det_vec3 (a:real^3) (b:real^3) (c:real^3) =
2298 a$1 * b$2 * c$3 + b$1 * c$2 * a$3 + c$1 * a$2 * b$3 -
2299 ( a$1 * c$2 * b$3 + b$1 * a$2 * c$3 + c$1 * b$2 * a$3 ) `;;
2301 let COPLANAR_DET_EQ_0 = prove
2302 (`!v0 v1 (v2: real^3) v3.
2303 coplanar_alt {v0,v1,v2,v3} <=>
2304 det(vector[v1 - v0; v2 - v0; v3 - v0]) = &0`,
2305 REPEAT GEN_TAC THEN REWRITE_TAC[DET_EQ_0_RANK; RANK_ROW] THEN
2306 REWRITE_TAC[rows; row; LAMBDA_ETA] THEN
2307 ONCE_REWRITE_TAC[SIMPLE_IMAGE_GEN] THEN
2308 REWRITE_TAC[GSYM numseg; DIMINDEX_3] THEN
2309 CONV_TAC(ONCE_DEPTH_CONV NUMSEG_CONV) THEN
2310 SIMP_TAC[IMAGE_CLAUSES; VECTOR_3] THEN EQ_TAC THENL
2311 [REWRITE_TAC[coplanar_alt; plane; LEFT_AND_EXISTS_THM; LEFT_IMP_EXISTS_THM] THEN
2313 [`p:real^3->bool`; `a:real^3`; `b:real^3`; `c:real^3`] THEN
2314 DISCH_THEN(CONJUNCTS_THEN2 STRIP_ASSUME_TAC MP_TAC) THEN
2315 FIRST_X_ASSUM SUBST1_TAC THEN
2316 W(MP_TAC o PART_MATCH lhand AFFINE_HULL_INSERT_SUBSET_SPAN o
2317 rand o lhand o goal_concl) THEN
2318 REWRITE_TAC[GSYM IMP_CONJ_ALT] THEN
2319 DISCH_THEN(MP_TAC o MATCH_MP SUBSET_TRANS) THEN
2320 DISCH_THEN(MP_TAC o ISPEC `\x:real^3. x - a` o MATCH_MP IMAGE_SUBSET) THEN
2321 ONCE_REWRITE_TAC[SIMPLE_IMAGE_GEN] THEN
2322 REWRITE_TAC[IMAGE_CLAUSES; GSYM IMAGE_o; o_DEF; VECTOR_ADD_SUB; IMAGE_ID;
2324 REWRITE_TAC[INSERT_SUBSET] THEN STRIP_TAC THEN
2325 GEN_REWRITE_TAC LAND_CONV [GSYM DIM_SPAN] THEN MATCH_MP_TAC LET_TRANS THEN
2326 EXISTS_TAC `CARD {b - a:real^3,c - a}` THEN
2328 [MATCH_MP_TAC SPAN_CARD_GE_DIM;
2329 SIMP_TAC[CARD_CLAUSES; FINITE_RULES] THEN ARITH_TAC] THEN
2330 REWRITE_TAC[FINITE_INSERT; FINITE_RULES] THEN
2331 GEN_REWRITE_TAC RAND_CONV [GSYM SPAN_SPAN] THEN
2332 MATCH_MP_TAC SPAN_MONO THEN REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET] THEN
2333 MP_TAC(VECTOR_ARITH `!x y:real^3. x - y = (x - a) - (y - a)`) THEN
2334 DISCH_THEN(fun th -> REPEAT CONJ_TAC THEN
2335 GEN_REWRITE_TAC LAND_CONV [th]) THEN
2336 MATCH_MP_TAC SPAN_SUB THEN ASM_REWRITE_TAC[];
2339 MP_TAC(ISPECL [`{v1 - v0,v2 - v0,v3 - v0}:real^3->bool`; `2`]
2340 LOWDIM_EXPAND_BASIS) THEN
2341 ASM_REWRITE_TAC[ARITH_RULE `n <= 2 <=> n < 3`; DIMINDEX_3; ARITH] THEN
2342 DISCH_THEN(X_CHOOSE_THEN `t:real^3->bool`
2343 (CONJUNCTS_THEN2 MP_TAC STRIP_ASSUME_TAC)) THEN
2344 CONV_TAC(LAND_CONV HAS_SIZE_CONV) THEN
2345 REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
2346 MAP_EVERY X_GEN_TAC [`a:real^3`; `b:real^3`] THEN
2347 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC SUBST_ALL_TAC) THEN
2348 REWRITE_TAC[coplanar_alt; plane] THEN
2349 EXISTS_TAC `affine hull {v0,v0 + a,v0 + b}:real^3->bool` THEN
2351 [MAP_EVERY EXISTS_TAC [`v0:real^3`; `v0 + a:real^3`; `v0 + b:real^3`] THEN
2352 REWRITE_TAC[COLLINEAR_3; COLLINEAR_LEMMA;
2353 VECTOR_ARITH `--x = vec 0 <=> x = vec 0`;
2354 VECTOR_ARITH `u - (u + a):real^3 = --a`;
2355 VECTOR_ARITH `(u + b) - (u + a):real^3 = b - a`] THEN
2356 REWRITE_TAC[DE_MORGAN_THM; VECTOR_SUB_EQ;
2357 VECTOR_ARITH `b - a = c % -- a <=> (c - &1) % a + &1 % b = vec 0`] THEN
2358 ASM_REWRITE_TAC[] THEN CONJ_TAC THENL
2359 [ASM_MESON_TAC[IN_INSERT; INDEPENDENT_NONZERO]; ALL_TAC] THEN
2360 DISCH_THEN(X_CHOOSE_TAC `u:real`) THEN
2361 FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [independent]) THEN
2362 REWRITE_TAC[DEPENDENT_EXPLICIT] THEN
2363 MAP_EVERY EXISTS_TAC [`{a:real^3,b}`;
2364 `\x:real^3. if x = a then u - &1 else &1`] THEN
2365 REWRITE_TAC[FINITE_INSERT; FINITE_RULES; SUBSET_REFL] THEN
2367 [EXISTS_TAC `b:real^3` THEN ASM_REWRITE_TAC[IN_INSERT] THEN
2370 SIMP_TAC[VSUM_CLAUSES; FINITE_RULES] THEN
2371 ASM_REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY; VECTOR_ADD_RID];
2373 W(MP_TAC o PART_MATCH (lhs o rand) AFFINE_HULL_INSERT_SPAN o
2374 rand o goal_concl) THEN
2376 [REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY] THEN
2377 REWRITE_TAC[VECTOR_ARITH `u = u + a <=> a = vec 0`] THEN
2378 ASM_MESON_TAC[INDEPENDENT_NONZERO; IN_INSERT];
2380 DISCH_THEN SUBST1_TAC THEN
2381 ONCE_REWRITE_TAC[SIMPLE_IMAGE_GEN] THEN
2382 REWRITE_TAC[SIMPLE_IMAGE; IMAGE_CLAUSES; IMAGE_ID; VECTOR_ADD_SUB] THEN
2383 MATCH_MP_TAC SUBSET_TRANS THEN EXISTS_TAC
2384 `IMAGE (\v:real^3. v0 + v) (span{v1 - v0, v2 - v0, v3 - v0})` THEN
2385 ASM_SIMP_TAC[IMAGE_SUBSET] THEN
2386 REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET; IN_IMAGE] THEN CONJ_TAC THENL
2387 [EXISTS_TAC `vec 0:real^3` THEN REWRITE_TAC[SPAN_0] THEN VECTOR_ARITH_TAC;
2388 REWRITE_TAC[VECTOR_ARITH `v1:real^N = v0 + x <=> x = v1 - v0`] THEN
2389 REWRITE_TAC[UNWIND_THM2] THEN REPEAT CONJ_TAC THEN
2390 MATCH_MP_TAC SPAN_SUPERSET THEN REWRITE_TAC[IN_INSERT]]]);;
2393 (* renamed from COPLANAR Jan 2013, to avoid clash with hol-light/Multivariate/Flyspeck.ml thm *)
2395 let COPLANAR_ALT = prove
2397 ==> !s:real^N->bool. coplanar_alt s <=> ?u v w. s SUBSET affine hull {u,v,w}`,
2398 DISCH_TAC THEN GEN_TAC THEN REWRITE_TAC[coplanar_alt; plane] THEN
2399 REWRITE_TAC[LEFT_AND_EXISTS_THM] THEN
2400 ONCE_REWRITE_TAC[MESON[]
2401 `(?x u v w. p x u v w) <=> (?u v w x. p x u v w)`] THEN
2402 REWRITE_TAC[GSYM CONJ_ASSOC; RIGHT_EXISTS_AND_THM; UNWIND_THM2] THEN
2403 EQ_TAC THENL [MESON_TAC[]; REWRITE_TAC[LEFT_IMP_EXISTS_THM]] THEN
2404 MAP_EVERY X_GEN_TAC [`u:real^N`; `v:real^N`; `w:real^N`] THEN DISCH_TAC THEN
2406 `s SUBSET {u + x:real^N | x | x IN span {y - u | y IN {v,w}}}`
2408 [FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP
2409 (REWRITE_RULE[IMP_CONJ] SUBSET_TRANS)) THEN
2410 REWRITE_TAC[AFFINE_HULL_INSERT_SUBSET_SPAN];
2412 ONCE_REWRITE_TAC[SIMPLE_IMAGE_GEN] THEN
2413 DISCH_THEN(MP_TAC o ISPEC `\x:real^N. x - u` o MATCH_MP IMAGE_SUBSET) THEN
2414 REWRITE_TAC[GSYM IMAGE_o; o_DEF; VECTOR_ADD_SUB; IMAGE_ID; SIMPLE_IMAGE] THEN
2415 REWRITE_TAC[IMAGE_CLAUSES] THEN
2416 MP_TAC(ISPECL [`{v - u:real^N,w - u}`; `2`] LOWDIM_EXPAND_BASIS) THEN
2418 [ASM_REWRITE_TAC[] THEN MATCH_MP_TAC LE_TRANS THEN
2419 EXISTS_TAC `CARD{v - u:real^N,w - u}` THEN
2420 SIMP_TAC[DIM_LE_CARD; FINITE_INSERT; FINITE_RULES] THEN
2421 SIMP_TAC[CARD_CLAUSES; FINITE_RULES] THEN ARITH_TAC;
2423 DISCH_THEN(X_CHOOSE_THEN `t:real^N->bool`
2424 (CONJUNCTS_THEN2 MP_TAC STRIP_ASSUME_TAC)) THEN
2425 CONV_TAC(LAND_CONV HAS_SIZE_CONV) THEN
2426 REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
2427 MAP_EVERY X_GEN_TAC [`a:real^N`; `b:real^N`] THEN
2428 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC SUBST_ALL_TAC) THEN
2429 UNDISCH_TAC `span {v - u, w - u} SUBSET span {a:real^N, b}` THEN
2430 REWRITE_TAC[GSYM IMP_CONJ_ALT] THEN
2431 DISCH_THEN(ASSUME_TAC o MATCH_MP SUBSET_TRANS) THEN
2432 MAP_EVERY EXISTS_TAC [`u:real^N`; `u + a:real^N`; `u + b:real^N`] THEN
2434 [REWRITE_TAC[COLLINEAR_3; COLLINEAR_LEMMA;
2435 VECTOR_ARITH `--x = vec 0 <=> x = vec 0`;
2436 VECTOR_ARITH `u - (u + a):real^N = --a`;
2437 VECTOR_ARITH `(u + b) - (u + a):real^N = b - a`] THEN
2438 REWRITE_TAC[DE_MORGAN_THM; VECTOR_SUB_EQ;
2439 VECTOR_ARITH `b - a = c % -- a <=> (c - &1) % a + &1 % b = vec 0`] THEN
2440 ASM_REWRITE_TAC[] THEN CONJ_TAC THENL
2441 [ASM_MESON_TAC[IN_INSERT; INDEPENDENT_NONZERO]; ALL_TAC] THEN
2442 DISCH_THEN(X_CHOOSE_TAC `u:real`) THEN
2443 FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [independent]) THEN
2444 REWRITE_TAC[DEPENDENT_EXPLICIT] THEN
2445 MAP_EVERY EXISTS_TAC [`{a:real^N,b}`;
2446 `\x:real^N. if x = a then u - &1 else &1`] THEN
2447 REWRITE_TAC[FINITE_INSERT; FINITE_RULES; SUBSET_REFL] THEN
2449 [EXISTS_TAC `b:real^N` THEN ASM_REWRITE_TAC[IN_INSERT] THEN
2452 SIMP_TAC[VSUM_CLAUSES; FINITE_RULES] THEN
2453 ASM_REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY; VECTOR_ADD_RID];
2455 W(MP_TAC o PART_MATCH (lhs o rand) AFFINE_HULL_INSERT_SPAN o rand o goal_concl) THEN
2457 [REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY] THEN
2458 REWRITE_TAC[VECTOR_ARITH `u = u + a <=> a = vec 0`] THEN
2459 ASM_MESON_TAC[INDEPENDENT_NONZERO; IN_INSERT];
2461 DISCH_THEN SUBST1_TAC THEN
2462 FIRST_ASSUM(MP_TAC o ISPEC `\x:real^N. u + x` o MATCH_MP IMAGE_SUBSET) THEN
2463 REWRITE_TAC[GSYM IMAGE_o; o_DEF; IMAGE_ID;
2464 ONCE_REWRITE_RULE[VECTOR_ADD_SYM] VECTOR_SUB_ADD] THEN
2465 MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ_ALT] SUBSET_TRANS) THEN
2466 REWRITE_TAC[SUBSET; FORALL_IN_IMAGE] THEN
2467 REWRITE_TAC[SIMPLE_IMAGE; IMAGE_CLAUSES; VECTOR_ADD_SUB] THEN
2470 (* this LEMMA in determinants.ml
2471 let DET_3 = new_axiom_removed`!A:real^3^3.
2472 det(A) = A$1$1 * A$2$2 * A$3$3 +
2473 A$1$2 * A$2$3 * A$3$1 +
2474 A$1$3 * A$2$1 * A$3$2 -
2475 A$1$1 * A$2$3 * A$3$2 -
2476 A$1$2 * A$2$1 * A$3$3 -
2477 A$1$3 * A$2$2 * A$3$1`;;
2480 let det_vec3 = new_definition ` det_vec3 (a:real^3) (b:real^3) (c:real^3) =
2481 a$1 * b$2 * c$3 + b$1 * c$2 * a$3 + c$1 * a$2 * b$3 -
2482 ( a$1 * c$2 * b$3 + b$1 * a$2 * c$3 + c$1 * b$2 * a$3 ) `;;
2485 let DET_VEC3_EXPAND = prove
2486 (`det (vector [a; b; (c:real^3)] ) = det_vec3 a b c`,
2487 REWRITE_TAC[det_vec3; DET_3; VECTOR_3] THEN REAL_ARITH_TAC);;
2489 let COPLANAR_DET_VEC3_EQ_0 = prove( `!v0 v1 (v2: real^3) v3.
2490 coplanar_alt {v0,v1,v2,v3} <=>
2491 det_vec3 ( v1 - v0 ) ( v2 - v0 ) ( v3 - v0 ) = &0`, REWRITE_TAC[COPLANAR_DET_EQ_0; DET_VEC3_EXPAND]);;
2495 let COPLANAR_3 = prove
2496 (`!a b c:real^N. 2 <= dimindex(:N) ==> coplanar_alt {a,b,c}`,
2497 SIMP_TAC[COPLANAR_ALT; SUBSET] THEN MESON_TAC[HULL_INC]);;
2499 let NONCOPLANAR_4_DISTINCT = prove
2501 ~(coplanar_alt{a,b,c,d}) /\ 2 <= dimindex(:N)
2502 ==> ~(a = b) /\ ~(a = c) /\ ~(a = d) /\
2503 ~(b = c) /\ ~(b = d) /\ ~(c = d)`,
2504 REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
2505 ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN REWRITE_TAC[DE_MORGAN_THM] THEN
2506 STRIP_TAC THEN ASM_SIMP_TAC[INSERT_AC; COPLANAR_3]);;
2510 let NONCOPLANAR_3_BASIS = prove
2511 (`!v1 v2 v3 v0 v:real^3.
2512 ~coplanar_alt {v0, v1, v2, v3}
2514 v = t1 % (v1 - v0) + t2 % (v2 - v0) + t3 % (v3 - v0) /\
2516 v = ta % (v1 - v0) + tb % (v2 - v0) + tc % (v3 - v0)
2517 ==> ta = t1 /\ tb = t2 /\ tc = t3))`,
2518 REPEAT STRIP_TAC THEN
2519 FIRST_ASSUM(MP_TAC o MATCH_MP (REWRITE_RULE[IMP_CONJ]
2520 NONCOPLANAR_4_DISTINCT)) THEN
2521 REWRITE_TAC[DIMINDEX_3; ARITH] THEN STRIP_TAC THEN
2522 SUBGOAL_THEN `independent {v1 - v0:real^3,v2 - v0,v3 - v0}` ASSUME_TAC THENL
2523 [FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE RAND_CONV [COPLANAR_DET_EQ_0]) THEN
2524 ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN REWRITE_TAC[independent] THEN
2525 DISCH_TAC THEN MATCH_MP_TAC DET_DEPENDENT_ROWS THEN
2526 REWRITE_TAC[rows; row; LAMBDA_ETA; GSYM IN_NUMSEG; DIMINDEX_3] THEN
2527 ONCE_REWRITE_TAC[SIMPLE_IMAGE] THEN
2528 CONV_TAC(ONCE_DEPTH_CONV NUMSEG_CONV) THEN
2529 ASM_REWRITE_TAC[IMAGE_CLAUSES; VECTOR_3];
2531 MP_TAC(ISPECL [`(:real^3)`; `{v1 - v0:real^3,v2 - v0,v3 - v0}`]
2532 CARD_GE_DIM_INDEPENDENT) THEN
2533 ASM_REWRITE_TAC[DIM_UNIV; SUBSET_UNIV] THEN ANTS_TAC THENL
2534 [SIMP_TAC[CARD_CLAUSES; FINITE_INSERT; FINITE_RULES] THEN
2535 ASM_REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY; DIMINDEX_3; ARITH;
2536 VECTOR_ARITH `x - a:real^N = y - a <=> x = y`];
2538 REWRITE_TAC[SUBSET; IN_UNIV; SPAN_BREAKDOWN_EQ; SPAN_EMPTY] THEN
2539 DISCH_THEN(MP_TAC o SPEC `v:real^3`) THEN
2540 MAP_EVERY (fun t -> MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC t)
2541 [`t1:real`; `t2:real`; `t3:real`] THEN
2542 REWRITE_TAC[IN_SING; VECTOR_ARITH
2543 `a - b - c - d:real^N = vec 0 <=> a = b + c + d`] THEN
2544 DISCH_THEN SUBST1_TAC THEN REWRITE_TAC[] THEN
2545 MAP_EVERY X_GEN_TAC [`ta:real`; `tb:real`; `tc:real`] THEN
2546 REWRITE_TAC[VECTOR_ARITH
2547 `t1 % x + t2 % y + t3 % z = ta % x + tb % y + tc % z <=>
2548 (t1 - ta) % x + (t2 - tb) % y + (t3 - tc) % z = vec 0`] THEN
2549 STRIP_TAC THEN FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [independent]) THEN
2550 REWRITE_TAC[DEPENDENT_EXPLICIT; NOT_EXISTS_THM] THEN
2551 DISCH_THEN(MP_TAC o SPECL
2552 [`{v1 - v0:real^3,v2 - v0,v3 - v0}`;
2553 `\v:real^3. if v = v1 - v0 then t1 - ta
2554 else if v = v2 - v0 then t2 - tb
2555 else t3 - tc`]) THEN
2556 SIMP_TAC[FINITE_INSERT; FINITE_RULES; SUBSET_REFL; VSUM_CLAUSES] THEN
2557 ASM_REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY; VECTOR_ADD_RID;
2558 RIGHT_OR_DISTRIB; EXISTS_OR_THM; UNWIND_THM2;
2559 VECTOR_ARITH `x - a:real^N = y - a <=> x = y`] THEN
2560 SIMP_TAC[DE_MORGAN_THM; REAL_SUB_0]);;
2564 let DET_VEC3_AND_DELTA = prove(`!(a:real^3) b c d.
2565 &4 * ( det_vec3 (a - d) (b - d) (c - d) ) pow 2 =
2566 delta ( dist3 a d pow 2)
2568 (dist3 c d pow 2) (dist3 a b pow 2) (dist3 a c pow 2) (dist3 b c pow 2) `,
2569 SIMP_TAC[dist3; dist] THEN
2570 REWRITE_TAC[GSYM (MESON[VECTOR_ARITH ` (a :real^N) - b = ( a - x ) - ( b - x ) `]`
2571 delta (norm (a - d) pow 2) (norm (b - d) pow 2)
2572 (norm (c - d) pow 2) (norm ((a - d) - (b - d )) pow 2)
2573 (norm ((a - d) - ( c - d )) pow 2) (norm ((b - d ) - ( c - d )) pow 2) =
2574 delta (norm (a - d) pow 2) (norm (b - d) pow 2) (norm (c - d) pow 2)
2575 (norm (a - b) pow 2) (norm (a - c) pow 2) (norm (b - c) pow 2) `)] THEN
2576 SIMP_TAC[ vector_norm; DOT_POS_LE; SQRT_WORKS] THEN
2577 REWRITE_TAC[DOT_3] THEN
2578 REWRITE_TAC[MESON[lemma_cm3]`((a:real^3) - d - (b - d))$1 = (a - d)$1 - (b - d)$1 /\
2579 (a - d - (b - d))$2 = (a - d)$2 - (b - d)$2 /\
2580 (a - d - (b - d))$3 = (a - d)$3 - (b - d)$3 `] THEN
2581 REWRITE_TAC[delta; det_vec3] THEN
2586 let POLFLZY = prove(` !(x1:real^3) x2 x3 x4.
2587 let x12 = dist (x1,x2) pow 2 in
2588 let x13 = dist (x1,x3) pow 2 in
2589 let x14 = dist (x1,x4) pow 2 in
2590 let x23 = dist (x2,x3) pow 2 in
2591 let x24 = dist (x2,x4) pow 2 in
2592 let x34 = dist (x3,x4) pow 2 in
2593 coplanar_alt {x1, x2, x3, x4} <=> delta x12 x13 x14 x23 x24 x34 = &0 `,
2594 LET_TR THEN REPEAT GEN_TAC THEN MP_TAC (GSYM (SPECL [` x2 :real^3`;
2595 ` x3:real^3`;` x4:real^3`; ` x1 :real^3`] DET_VEC3_AND_DELTA)) THEN
2596 SIMP_TAC[dist3; DIST_SYM] THEN REWRITE_TAC[REAL_ARITH ` &4 * a = &0 <=> a = &0 `]
2597 THEN SIMP_TAC[GSYM ( REAL_FIELD ` x = &0 <=> x pow 2 = &0 `);
2598 COPLANAR_DET_VEC3_EQ_0]);;
2601 let LEMMA15 = POLFLZY;;
2603 let muy_delta = new_definition ` muy_delta = delta `;;
2608 let VCRJIHC = prove(`!(v1:real^3) v2 v3 v4 x34 x12 x13 x14 x23 x24.
2609 condA v1 v2 v3 v4 x12 x13 x14 x23 x24 x34
2610 ==> muy_delta x12 x13 x14 x23 x24 (dist (v3,v4) pow 2) = &0`,
2611 REWRITE_TAC[condA; muy_delta] THEN MP_TAC POLFLZY THEN LET_TR THEN MESON_TAC[]);;
2614 let ZERO_NEUTRAL = REAL_ARITH ` ! x. &0 * x = &0 /\ x * &0 = &0 /\ &0 + x = x /\ x + &0 = x /\ x - &0 = x /\
2617 let EQUATE_CONEFS_POLINOMIAL_POW2 = prove( `!a b c aa bb cc. ( ! x.
2618 a * x pow 2 + b * x + c = aa * x pow 2 + bb * x + cc ) <=>
2619 a = aa /\ b = bb /\ c = cc`, REPEAT GEN_TAC THEN EQ_TAC THENL [
2620 NHANH (MESON[]` (! (x:real). P x ) ==> P ( &0 ) /\ P ( &1 ) /\ P ( -- &1 )`) THEN
2621 REAL_ARITH_TAC THEN REAL_ARITH_TAC; SIMP_TAC[]]);;
2623 let GJWYYPS = prove(`!x12 x13 x14 x15 x23 x24 x25 x34 x35 a b c.
2624 (! x45. cayleyR x12 x13 x14 x15 x23 x24 x25 x34 x35 x45 =
2625 a * x45 pow 2 + b * x45 + c )
2626 ==> b pow 2 - &4 * a * c =
2627 &16 * delta x12 x13 x14 x23 x24 x34 * delta x12 x13 x15 x23 x25 x35`,
2628 ONCE_REWRITE_TAC[LTCTBAN] THEN REPEAT GEN_TAC THEN
2629 REWRITE_TAC[EQUATE_CONEFS_POLINOMIAL_POW2] THEN ONCE_REWRITE_TAC[EQ_SYM_EQ]
2630 THEN SIMP_TAC[] THEN DISCH_TAC THEN REWRITE_TAC[ups_x; cayleytr; cayleyR;
2631 delta; ZERO_NEUTRAL] THEN REAL_ARITH_TAC);;
2633 let LEMMA51 = GJWYYPS ;;
2635 let NOT_TOW_EQ_IMP_COL_EQUAVALENT = prove_by_refinement(
2636 `!v1 v2 (v:real^3). ~(v1 = v2) ==> (collinear {v, v1, v2} <=> v IN aff {v1, v2})`,
2639 (REWRITE_TAC[COLLINEAR_EX]);
2640 (NHANH (MESON[]` a % b + c = vec 0 ==> ( a = &0 \/ ~(a = &0 ))`));
2642 (NGOAC THEN PURE_ONCE_REWRITE_TAC[MESON[]` P a /\ a = &0 <=> P ( &0 ) /\ a = &0 `]);
2643 (REWRITE_TAC[REAL_ADD_LID; VECTOR_MUL_LZERO; VECTOR_ADD_LID]);
2644 (REWRITE_TAC[REAL_ARITH ` a + b= &0 <=> a = -- b `; VECTOR_ARITH` a % x + b % y = vec 0 <=> a % x = ( -- b) % y`]);
2645 (NHANH (MESON[REAL_ARITH ` a = &0 <=> -- a = &0 `; VECTOR_MUL_LCANCEL]` (b = --c /\ ~(b = &0 /\ c = &0)) /\ b % v1 = --c % v2 ==> v1 = v2 `));
2647 (REWRITE_TAC[AFF_2POINTS_INTERPRET; IN_ELIM_THM]);
2648 (REPEAT GEN_TAC THEN DISCH_TAC THEN EQ_TAC);
2649 (REWRITE_TAC[VECTOR_ARITH ` a % v + b % v1 + c % v2 = vec 0 <=> a % v = ( -- b) % v1 + ( --c ) % v2 `]);
2650 (PHA THEN REWRITE_TAC[MESON[CHANGE_SIDE]` a % v = v1 /\ ~(a = &0) <=> v = &1 / a % v1 /\ ~( a = &0 ) `]);
2651 (REWRITE_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC; REAL_ARITH `&1 / a * b = b / a`]);
2652 (REWRITE_TAC[AFF_2POINTS_INTERPRET; IN_ELIM_THM]);
2653 BY( (MESON_TAC[REAL_FIELD ` ~ ( a = &0 ) /\ a = -- (b + c) ==> ( -- b) / a + ( -- c) / a = &1 `]));
2655 (EXISTS_TAC ` &1 `);
2656 (EXISTS_TAC ` -- ta`);
2657 (EXISTS_TAC ` -- tb`);
2659 (ASM_SIMP_TAC[REAL_ARITH` ~(&1 = &0 ) /\ -- ( -- a + -- b ) = a + b `]);
2660 BY( (CONV_TAC VECTOR_ARITH))
2666 let LEMMA30 = prove(`!v1 v2 v3 v4 x12 x13 x14 x23 x24 x34 a b c.
2667 condA v1 v2 v3 v4 x12 x13 x14 x23 x24 x34 /\
2668 (!x12 x13 x14 x23 x24 x34.
2669 muy_delta x12 x13 x14 x23 x24 x34 =
2670 a x12 x13 x14 x23 x24 * x34 pow 2 +
2671 b x12 x13 x14 x23 x24 * x34 +
2672 c x12 x13 x14 x23 x24 )
2673 ==> (v3 IN aff {v1, v2} \/ v4 IN aff {v1, v2} <=>
2674 b x12 x13 x14 x23 x24 pow 2 -
2675 &4 * a x12 x13 x14 x23 x24 * c x12 x13 x14 x23 x24 =
2677 REWRITE_TAC[muy_delta; DELTA_COEFS; EQUATE_CONEFS_POLINOMIAL_POW2 ] THEN
2678 ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN SIMP_TAC[] THEN REPEAT GEN_TAC THEN
2679 DISCH_TAC THEN REWRITE_TAC[REAL_ARITH` a - b * -- c * d = a + b * c * d `;
2680 AGBWHRD] THEN DOWN_TAC THEN SIMP_TAC[condA; REAL_ENTIRE;
2681 GSYM NOT_TOW_EQ_IMP_COL_EQUAVALENT] THEN ONCE_REWRITE_TAC[MESON[PER_SET3]`
2682 p {v3, v1, v2} \/ p {v4, v1, v2} <=> p {v1,v2,v3} \/ p {v1,v2,v4} `] THEN
2683 ONCE_REWRITE_TAC[MESON[UPS_X_SYM]` ups_x x12 x23 x13 = &0 \/
2684 ups_x x12 x24 x14 = &0 <=> ups_x x12 x13 x23 = &0 \/
2685 ups_x x12 x14 x24 = &0 `] THEN MESON_TAC[UPS_X_SYM; PER_SET3; FHFMKIY]);;
2688 (* let EWVIFXW = LEMMA30;; *)
2691 let LEMMA51 = GJWYYPS;;
2692 let LEMMA50 = LTCTBAN;;
2693 let muy_v = new_definition ` muy_v (x1: real^N ) (x2:real^N) (x3:real^N) (x4:real^N)
2695 (let x12 = dist (x1,x2) pow 2 in
2696 let x13 = dist (x1,x3) pow 2 in
2697 let x14 = dist (x1,x4) pow 2 in
2698 let x15 = dist (x1,x5) pow 2 in
2699 let x23 = dist (x2,x3) pow 2 in
2700 let x24 = dist (x2,x4) pow 2 in
2701 let x25 = dist (x2,x5) pow 2 in
2702 let x34 = dist (x3,x4) pow 2 in
2703 let x35 = dist (x3,x5) pow 2 in
2704 cayleyR x12 x13 x14 x15 x23 x24 x25 x34 x35 x45) `;;
2706 let REMOVE_TAC = MATCH_MP_TAC (MESON[]` a ==> b ==> a `);;
2708 let ALE = MESON[LTCTBAN]`!x12 x13 x14 x15 x23 x24 x25 x34 x35.
2710 cayleyR x12 x13 x14 x15 x23 x24 x25 x34 x35 x =
2711 a * x pow 2 + b * x + c )
2712 ==> b pow 2 - &4 * a * c = &0)
2713 ==> cayleytr x12 x13 x14 x15 x23 x24 x25 x34 x35 (&0) pow 2 -
2716 cayleyR x12 x13 x14 x15 x23 x24 x25 x34 x35 (&0) =
2719 let DISCRIMINANT_OF_CAY = MESON[LTCTBAN; GJWYYPS]`cayleytr x12 x13 x14 x15 x23 x24 x25 x34 x35 (&0) pow 2 -
2720 &4 * ups_x x12 x13 x23 * cayleyR x12 x13 x14 x15 x23 x24 x25 x34 x35 (&0) =
2721 &16 * delta x12 x13 x14 x23 x24 x34 * delta x12 x13 x15 x23 x25 x35`;;
2723 let NOT_TWO_EQ_IMP_COL_EQUAVALENT = NOT_TOW_EQ_IMP_COL_EQUAVALENT;;
2725 let GDLRUZB = prove(` ! (v1:real^3) (v2:real^3) (v3:real^3) (v4:real^3) (v5:real^3) a b c.
2726 coplanar_alt {v1, v2, v3, v4} \/ coplanar_alt {v1, v2, v3, v5} <=>
2727 (! a b c. (! x. muy_v v1 v2 v3 v4 v5 x = a * x pow 2 + b * x + c )
2728 ==> b pow 2 - &4 * a * c = &0) `,REWRITE_TAC[muy_v] THEN LET_TR THEN
2729 REPEAT GEN_TAC THEN EQ_TAC THENL [DISCH_TAC THEN
2730 NHANH (MESON[GJWYYPS]` (!x45. cayleyR x12 x13 x14 x15 x23 x24 x25 x34 x35 x45 =
2731 a * x45 pow 2 + b * x45 + c)
2732 ==> b pow 2 - &4 * a * c =
2734 delta x12 x13 x14 x23 x24 x34 *
2735 delta x12 x13 x15 x23 x25 x35`) THEN SIMP_TAC[] THEN
2736 UNDISCH_TAC ` coplanar_alt {(v1:real^3), v2, v3, v4}\/ coplanar_alt {v1, v2, v3, v5}` THEN
2737 MP_TAC LEMMA15 THEN LET_TR THEN REWRITE_TAC[REAL_FIELD` &16 * a * b = &0
2738 <=> a = &0 \/ b = &0 `] THEN SIMP_TAC[]; NHANH (SPEC_ALL ALE) THEN
2739 REWRITE_TAC[DISCRIMINANT_OF_CAY ] THEN MP_TAC POLFLZY THEN LET_TR THEN
2740 REWRITE_TAC[REAL_FIELD` &16 * a * b = &0 <=> a = &0 \/ b = &0 `] THEN
2744 let DET_VECC3_AND_DELTA = prove(` (! d a b c .
2745 delta (dist3 d a pow 2) (dist3 d b pow 2) (dist3 d c pow 2) (dist3 a b pow 2)
2748 &4 * det_vec3 (a - d) (b - d) (c - d) pow 2) `, MESON_TAC[D3_SYM;
2749 DET_VEC3_AND_DELTA]);;
2752 let DELTA_POS_4POINTS = prove(`!x1 x2 x3 (x4:real^3).
2754 delta (dist (x1,x2) pow 2) (dist (x1,x3) pow 2) (dist (x1,x4) pow 2)
2755 (dist (x2,x3) pow 2)
2756 (dist (x2,x4) pow 2)
2757 (dist (x3,x4) pow 2)`, REWRITE_TAC[GSYM dist3] THEN SIMP_TAC[D3_SYM] THEN
2758 MP_TAC (DET_VECC3_AND_DELTA) THEN SIMP_TAC[] THEN DISCH_TAC THEN MP_TAC
2759 REAL_LE_SQUARE_POW THEN MESON_TAC[REAL_ARITH` &0 <= x <=> &0 <= &4 * x `]);;
2764 prove(` ! a (b:real^N) . dist (a,b) pow 2 = ( a - b ) dot ( a- b) `,
2765 SIMP_TAC[dist; vector_norm; DOT_POS_LE; SQRT_WORKS]);;
2767 let UPS_X_POS = MESON[lemma8; UPS_X_SYM; NORM_SUB]` &0 <=
2768 ups_x (norm ((x1 : real^3) - x2) pow 2) (norm (x1 - x3) pow 2)
2769 (norm (x2 - x3) pow 2) `;;
2771 let UPS_X_SYM = MESON[UPS_X_SYM]` !x y z. ups_x x y z = ups_x y x z /\ ups_x x y z = ups_x x z y
2772 /\ ups_x x y z = ups_x x z y `;;