(* ========================================================================== *) (* FLYSPECK - BOOK FORMALIZATION *) (* *) (* Lemma: NUHSVLM *) (* Chapter: leg *) (* Author: Nguyen Quang Truong *) (* Date: 2010-02-09 *) (* ========================================================================== *) (* second half of collect_geom.ml. It was split in half by thales Feb 2010. This file was edited by thales on 2012-5-15 to make it possible to load everything up through lemma GDRQXLG giving the formula for the circumradius of a simplex. Everything dependent on unproved axioms was commented out. Feb 2013, some excess material removed. *) flyspeck_needs "leg/cayleyR_def.hl";; flyspeck_needs "leg/collect_geom.hl";; module Collect_geom2 (* : Collect_geom2_type *) = struct open Sphere;; open Geomdetail;; open Collect_geom;; let cayleyR = Cayleyr.cayleyR;; let LET_TR = Collect_geom.LET_TR;; let DIST_POW2_DOT = Collect_geom.DIST_POW2_DOT;; let UPS_X_POS = Collect_geom.UPS_X_POS;; let DELTA_POS_4POINTS = Collect_geom.DELTA_POS_4POINTS;; let REAL_LDISTRIB = REAL_ADD_LDISTRIB;; let POW_2 = REAL_POW_2;; let REAL_POSSQ = REAL_LT_SQUARE;; let REAL_RDISTRIB = REAL_ARITH `!x y z. (x + y) * z = (x * z) + (y * z)`;; (* Tactics_jordan *) let BY = Hales_tactic.BY;; (* deprecated def from sphere.hl *) let mk_vec3 = new_definition `mk_vec3 a b c = vector[a; b; c]`;; let real3_of_triple = new_definition `real3_of_triple (a,b,c) = (mk_vec3 a b c):real^3`;; let triple_of_real3 = new_definition `triple_of_real3 (v:real^3) = (v$1, v$2, v$3)`;; (* deprecated def from sphere.hl *) (* this lemma is proved as below, but it take quite a long time to run it *) let CAYLEYR_5POINTS = prove(` !x1 x2 x3 x4 (x5 :real^3). let x12 = dist (x1,x2) pow 2 in let x13 = dist (x1,x3) pow 2 in let x14 = dist (x1,x4) pow 2 in let x15 = dist (x1,x5) pow 2 in let x23 = dist (x2,x3) pow 2 in let x24 = dist (x2,x4) pow 2 in let x25 = dist (x2,x5) pow 2 in let x34 = dist (x3,x4) pow 2 in let x35 = dist (x3,x5) pow 2 in let x45 = dist (x4,x5) pow 2 in cayleyR x12 x13 x14 x15 x23 x24 x25 x34 x35 x45 = &0 `, LET_TR THEN REWRITE_TAC[ DIST_POW2_DOT] THEN REPEAT GEN_TAC THEN REWRITE_TAC[ MESON[VECTOR_ARITH` (a:real^n) - b = a - x - ( b - x ) `]` AA ( (x1 - x5 ) dot ( x1 - x5)) ((x2 - x3) dot (x2 - x3)) ((x2 - x4) dot (x2 - x4)) ((x2 - x5) dot (x2 - x5)) ((x3 - x4) dot (x3 - x4)) ((x3 - x5) dot (x3 - x5)) ((x4 - x5) dot (x4 - x5)) = AA ( (x1 - x5 ) dot ( x1 - x5)) ((x2 - x1 - ( x3 - x1 )) dot (x2 - x1 - ( x3 - x1 ))) ((x2 - x1 - ( x4 - x1 )) dot (x2 - x1 - ( x4 - x1 ))) ((x2 - x1 - ( x5 - x1 )) dot (x2 - x1 - ( x5 - x1 ))) ((x3 - x1 - ( x4 - x1 )) dot (x3 - x1 - ( x4 - x1 ))) ((x3 - x1 - ( x5 - x1 )) dot (x3 - x1 - ( x5 - x1 ))) ((x4 - x1 - ( x5 - x1 )) dot (x4 - x1 - ( x5 - x1 ))) ` ] THEN SIMP_TAC[VECTOR_ARITH ` ((x4: real^N) - x1 - (x5 - x1)) = x1 - x5 - ( x1 - x4 ) `] THEN ABBREV_TAC ` x12 = (x1 - ( x2:real^3)) ` THEN ABBREV_TAC ` x13 = (x1 - ( x3:real^3)) ` THEN ABBREV_TAC ` x14 = (x1 - ( x4:real^3)) ` THEN ABBREV_TAC ` x15 = (x1 - ( x5:real^3)) ` THEN REWRITE_TAC[DOT_3] THEN REWRITE_TAC[lemma_cm3; cayleyR] THEN REAL_ARITH_TAC);; let LEMMA3 = prove(` !x1 x2 x3 x4 (x5 :real^3). let x12 = dist (x1,x2) pow 2 in let x13 = dist (x1,x3) pow 2 in let x14 = dist (x1,x4) pow 2 in let x15 = dist (x1,x5) pow 2 in let x23 = dist (x2,x3) pow 2 in let x24 = dist (x2,x4) pow 2 in let x25 = dist (x2,x5) pow 2 in let x34 = dist (x3,x4) pow 2 in let x35 = dist (x3,x5) pow 2 in let x45 = dist (x4,x5) pow 2 in &0 <= ups_x x12 x13 x23 /\ &0 <= delta x12 x13 x14 x23 x24 x34 /\ cayleyR x12 x13 x14 x15 x23 x24 x25 x34 x35 x45 = &0 `, MP_TAC CAYLEYR_5POINTS THEN LET_TR THEN SIMP_TAC[ dist; UPS_X_POS; DELTA_POS_4POINTS]);; (* LEMMA 3 *) let NUHSVLM = LEMMA3;; (* OLD END OF MODULE *) let LEMMA52 = prove( `! v1 v2 v3 v4 (v5:real^3). muy_v v1 v2 v3 v4 v5 ( (dist3 v4 v5) pow 2 ) = &0 `, REWRITE_TAC[muy_v; dist3] THEN MP_TAC LEMMA3 THEN LET_TR THEN SIMP_TAC[]);; let PFDFWWV = LEMMA52;; let PRE_VIET = REAL_ARITH `!x x1 x2. (x - x1) * (x - x2) = x pow 2 - (x1 + x2) * x + x1 * x2 /\ a * (x - x1) * (x - x2) = a * x pow 2 + ( -- a * (x1 + x2)) * x + a * x1 * x2 `;; let VIET_THEOREM = prove(`! x1 x2 a b c. (!x. a * x pow 2 + b * x + c = a * (x - x1) * (x - x2)) ==> -- b = a * ( x1 + x2 ) /\ c = a * x1 * x2 `, REWRITE_TAC[PRE_VIET; REAL_LDISTRIB;REAL_SUB_LDISTRIB; REAL_ARITH ` a - b * c = a + -- b * c `; REAL_ARITH` ( a + b ) + c = a + b + c `] THEN REWRITE_TAC[REAL_MUL_ASSOC; EQUATE_CONEFS_POLINOMIAL_POW2] THEN SIMP_TAC[] THEN REAL_ARITH_TAC);; let ADD_SUB_POW2_EX = REAL_RING ` ( a + b ) pow 2 = a pow 2 + &2 * a * b + b pow 2 /\ ( a - b ) pow 2 = a pow 2 - &2 * a * b + b pow 2 `;; let PRESENT_SUB_POW2 = REAL_RING` ! a b. ( a - b ) pow 2 = ( a + b ) pow 2 - &4 * a * b `;; let DIST_ROOT_AND_DISCRIMINANT = prove(` ! a b c x1 x2. ( ! x. a * x pow 2 + b * x + c = a * ( x - x1 ) * ( x - x2 ) ) ==> ( a pow 2 ) * ( x1 - x2 ) pow 2 = b pow 2 - &4 * a * c `, NHANH (SPEC_ALL VIET_THEOREM) THEN REWRITE_TAC[PRESENT_SUB_POW2] THEN SIMP_TAC[REAL_ARITH ` -- b = a <=> b = -- a `] THEN REAL_ARITH_TAC);; (* le 33. P 22 MARKED *) let REAL_EQ_TO_LE_LT = REAL_ARITH ` ( a = b <=> ~( a < b \/ b < a ) )`;; let FEBRUARY_13_09 = prove(` &0 < (u - v) dot (&2 % x - (u + v)) <=> &0 < (u - v) dot (x - &1 / &2 % (u + v)) `, ONCE_REWRITE_TAC[MESON[REAL_ARITH ` &0 < a <=> &0 < &2 * a `]` (a <=> &0 < b ) <=> ( a <=> &0 < &2 * b ) `] THEN ONCE_REWRITE_TAC[VECTOR_ARITH ` x * (a dot b) = a dot x % b `] THEN REWRITE_TAC[GSYM VECTOR_SUB_DISTRIBUTE; VECTOR_MUL_ASSOC] THEN REWRITE_TAC[REAL_ARITH ` &2 * &1 / &2 = &1 `; VECTOR_MUL_LID]);; let SUB_DOT_NEG_TO_POS = MESON[VECTOR_ARITH ` ( a - b ) dot x = -- (( b - a ) dot x ) `; REAL_ARITH ` -- a < &0 <=> &0 < a `] `! a b. ( a - b ) dot x < &0 <=> &0 < ( b - a ) dot x `;; let LEMMA6 = prove(` !(u:real^3) v. ~(u = v) ==> plane_norm (bis u v) `, REWRITE_TAC[plane_norm; bis] THEN REPEAT STRIP_TAC THEN EXISTS_TAC ` (u: real^3) - v ` THEN EXISTS_TAC ` &1 / &2 % ((u: real^3) + v )` THEN REWRITE_TAC[FUN_EQ_THM; IN_ELIM_THM] THEN ASM_SIMP_TAC[VECTOR_SUB_EQ] THEN REWRITE_TAC[REAL_EQ_TO_LE_LT; DIST_LT_HALF_PLANE;FEBRUARY_13_09; SUB_DOT_NEG_TO_POS] THEN SIMP_TAC[VECTOR_ADD_SYM] THEN MESON_TAC[]);; let BXVMKNF = LEMMA6;; let b_coef = BC_DEL_FOR;; let c_coef = b_coef ;; let DELTA_X34_B = prove(` ! x12 x13 x14 x23 x24 x. delta_x34 x12 x13 x14 x23 x24 x = -- &2 * x12 * x + b_coef x12 x13 x14 x23 x24 `, REWRITE_TAC[ delta_x34; b_coef]);; let EQ_POW2_COND = prove(`!a b. &0 <= a /\ &0 <= b ==> (a = b <=> a pow 2 = b pow 2)`, REWRITE_TAC[REAL_ARITH` a = b <=> a <= b /\ b <= a `] THEN SIMP_TAC[POW2_COND]);; let EQ_SQRT_POW2_EQ = prove(` &0 <= a /\ &0 <= b ==> ( a = sqrt b <=> a pow 2 = b ) `, SIMP_TAC[SQRT_WORKS; EQ_POW2_COND]);; (* let LEMMA33 = prove(` !x34 x12 x13 v1 x14 v3 x23 v2 v4 x24 x34' x34'' a. condA v1 v2 v3 v4 x12 x13 x14 x23 x24 x34 /\ (! x. muy_delta x12 x13 x14 x23 x24 x = a * ( x - x34' ) * ( x - x34'')) /\ x34' <= x34'' ==> delta_x34 x12 x13 x14 x23 x24 x34' = sqrt (ups_x x12 x13 x23 * ups_x x12 x14 x24) /\ delta_x34 x12 x13 x14 x23 x24 x34'' = --sqrt (ups_x x12 x13 x23 * ups_x x12 x14 x24) `, REWRITE_TAC[muy_delta; DELTA_X34_B; DELTA_COEFS] THEN SIMP_TAC[EQUATE_CONEFS_POLINOMIAL_POW2; PRE_VIET; REAL_ARITH ` -- a = b <=> b = -- a`] THEN SIMP_TAC[REAL_RING `-- &2 * x12 * x34' + -- --x12 * (x34' + x34'') = a <=> -- &2 * x12 * x34'' + -- --x12 * (x34' + x34'') = -- a `] THEN REWRITE_TAC[REAL_ARITH` -- &2 * x12 * x34'' + -- --x12 * (x34' + x34'') = x12 * ( x34' - x34'' ) `; condA] THEN REPEAT STRIP_TAC THEN EXPAND_TAC "x12" THEN EXPAND_TAC "x13" THEN EXPAND_TAC "x23" THEN EXPAND_TAC "x14" THEN EXPAND_TAC "x24" THEN UNDISCH_TAC ` x34' <= (x34'':real)` THEN ONCE_REWRITE_TAC[REAL_ARITH ` a <= b <=> &0 <= b - a `] THEN ONCE_REWRITE_TAC[ REAL_ARITH ` a * ( b - c ) = -- ( a * ( c - b ) ) `] THEN MP_TAC (GEN_ALL TROI_OI_DAT_HOI) THEN MP_TAC REAL_LE_POW_2 THEN REWRITE_TAC[REAL_ARITH` -- a = -- b <=> a = b `] THEN SIMP_TAC[UPS_X_SYM; REAL_LE_MUL; EQ_SQRT_POW2_EQ ] THEN ASM_SIMP_TAC[] THEN REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[ REAL_ARITH ` ( a * b ) pow 2 = a pow 2 * b pow 2 `] THEN REWRITE_TAC[PRESENT_SUB_POW2] THEN REWRITE_TAC[REAL_SUB_LDISTRIB; REAL_ARITH ` a pow 2 * b pow 2 = ( -- a * b ) pow 2 /\ a pow 2 * &4 * b = -- a * &4 * -- a * b `] THEN UNDISCH_TAC `b_coef x12 x13 x14 x23 x24 = --a * (x34' + x34'')` THEN UNDISCH_TAC `c_coef x12 x13 x14 x23 x24 = a * x34' * x34''` THEN UNDISCH_TAC `(a: real) = --x12` THEN ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN SIMP_TAC[] THEN SIMP_TAC[REAL_ARITH` -- -- a = a /\ ( -- a * b) pow 2 = ( a * b ) pow 2 /\ ( a * -- b) pow 2 = ( a * b ) pow 2 `; REAL_ADD_SYM; REAL_MUL_SYM] THEN SIMP_TAC[REAL_ADD_SYM; REAL_MUL_SYM] THEN ONCE_REWRITE_TAC[REAL_ARITH ` ( a * b ) pow 2 = ( b * -- a ) pow 2 `] THEN SIMP_TAC[] THEN REPEAT STRIP_TAC THEN EXPAND_TAC "a" THEN REWRITE_TAC[REAL_RING ` a - -- c * b * &4 = a + &4 * c * b `] THEN MESON_TAC[AGBWHRD; UPS_X_SYM]);; *) (* let CMUDPKT = LEMMA33;; *) (* ============= *) let LEMMA_OF_LE20 = prove(` ! x y z: real^3. &2 <= dist3 x y /\ dist3 x y <= #2.52 /\ &2 <= dist3 x z /\ dist3 x z <= #2.2 /\ &2 <= dist3 y z /\ dist3 y z <= #2.2 ==> ~collinear {x, y, z} `, MP_TAC JVUNDLC THEN SIMP_TAC[] THEN ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN REWRITE_TAC[MESON[]` (! a b c s. P a b c = s ==> Q a b c ) <=> (! a b c . Q a b c ) `] THEN SIMP_TAC[COL_EQ_UPS_0] THEN MATCH_MP_TAC (TAUT` a ==> b ==> a `) THEN REWRITE_TAC[GSYM dist3] THEN REWRITE_TAC[REAL_ENTIRE] THEN CONV_TAC REAL_FIELD);; let LT_POW2_EQ_LT = MESON[POW2_COND_LT; REAL_ARITH ` a <= b <=> ~ ( b < a ) `] `&0 < a /\ &0 < b ==> ( a < b <=> a pow 2 < b pow 2 ) `;; let ETA_Y_LT_SQRT2 = prove(`eta_y #2.2 #2.2 #2.52 < sqrt #2`, REWRITE_TAC[eta_y; eta_x; ups_x] THEN LET_TR THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN MP_TAC (REAL_FIELD ` &14641 / &8131< &2 `) THEN MP_TAC (REAL_FIELD ` &0 < &2 /\ &0 < &14641 / &8131 `) THEN NHANH (SPEC_ALL SQRT_POS_LT) THEN REWRITE_TAC[ REAL_ARITH ` #2 = &2 `] THEN SIMP_TAC[REAL_ARITH ` &0 < a ==> &0 <= a `;SQRT_POS_LT; LT_POW2_EQ_LT; SQRT_WORKS]);; let ETA_YY_LT_SQRT2 = MESON[ETA_Y_LT_SQRT2; REAL_ARITH ` #2 = &2 `]` eta_y #2.2 #2.2 #2.52 < sqrt ( &2 ) `;; let THANG_DEU = prove(` &2 <= x ==> &2 pow 2 <= x pow 2 `, NHANH (REAL_ARITH ` &2 <= x ==> &0 <= &2 /\ &0 <= x `) THEN MESON_TAC[POW2_COND]);; let NGAY23_THANG2_09 = prove(` &2 <= y /\ y <= sqrt (&8) ==> &2 pow 2 <= y * y /\ y * y <= &8 `, REWRITE_TAC[ GSYM REAL_POW_2] THEN DISCH_TAC THEN CONJ_TAC THENL [ASM_MESON_TAC[REAL_ARITH ` &2 <= a ==> &0 <= &2 /\ &0 <= a `;POW2_COND]; ASM_MESON_TAC[ SQRT_WORKS; REAL_ARITH ` &0 <= &8 `; POW2_COND; REAL_ARITH `&2 <= a /\ a <= b ==> &0 <= b /\ &0 <= a `]]);; let ETA_Y_SQRT8_2_251 = prove(` eta_y ( sqrt (&8) ) (&2) #2.51 < #1.453`, REWRITE_TAC[eta_y; eta_x; ups_x; GSYM POW_2] THEN LET_TR THEN REWRITE_TAC[MESON[SQRT_WORKS; REAL_ARITH ` &0 <= &8 `]` sqrt (&8) pow 2 = &8 `] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN MP_TAC (REAL_FIELD ` &0 < &20160320000 / &9551113999 /\ &0 < #1.453 `) THEN NHANH (SPEC_ALL SQRT_POS_LT) THEN SIMP_TAC[LT_POW2_EQ_LT; REAL_ARITH ` &0 < a ==> &0 <= a `; SQRT_POW_2] THEN DISCH_TAC THEN CONV_TAC REAL_FIELD );; let CDEUSDF_CHANGE = CDEUSDF;; let CIRCUMCENTER_FORMULAR = prove(` ! va vb vc. ~collinear {va, vb, vc} ==> circumcenter {va, vb, vc} = (dist3 vb vc pow 2 * (dist3 va vc pow 2 + dist3 va vb pow 2 - dist3 vb vc pow 2)) / (ups_x (dist3 vb vc pow 2) (dist3 va vc pow 2) (dist3 va vb pow 2)) % va + (dist3 va vc pow 2 * (dist3 vb vc pow 2 + dist3 va vb pow 2 - dist3 va vc pow 2)) / (ups_x (dist3 vb vc pow 2) (dist3 va vc pow 2) (dist3 va vb pow 2)) % vb + (dist3 va vb pow 2 * (dist3 vb vc pow 2 + dist3 va vc pow 2 - dist3 va vb pow 2)) / (ups_x (dist3 vb vc pow 2) (dist3 va vc pow 2) (dist3 va vb pow 2)) % vc `, ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN MP_TAC CDEUSDF_CHANGE THEN LET_TR THEN MESON_TAC[]);; let LE_EX = REAL_ARITH ` &0 <= a <=> a = &0 \/ &0 < a `;; let SUM_UPS_X_1 = prove(`!a b c. &0 < ups_x a b c ==> (c * (b + a - c)) / ups_x a b c + (a * (c + b - a)) / ups_x a b c + (b * (c + a - b)) / ups_x a b c = &1`, REWRITE_TAC[ups_x] THEN CONV_TAC REAL_FIELD);; MESON[POW2_COND; REAL_ARITH `&2 <= a /\ a <= b ==> &0 <= b /\ &0 <= a `]` &2 <= y /\ y <= b ==> y pow 2 <= b pow 2 `;; let FACTOR_OF_QUADRARTIC = prove(`! a b c x. ~(a = &0) /\ &0 <= b pow 2 - &4 * a * c ==> a * x pow 2 + b * x + c = a * (x - (--b + sqrt (b pow 2 - &4 * a * c)) / (&2 * a)) * (x - (--b - sqrt (b pow 2 - &4 * a * c)) / (&2 * a))` , REWRITE_TAC[PRE_VIET] THEN SIMP_TAC[REAL_FIELD ` ~( a = &0 ) ==> -- a * ( ( --b + del) / ( &2 * a ) + ( --b - del) / ( &2 * a )) = b `] THEN REWRITE_TAC[REAL_FIELD ` a / b * a' / b = ( a * a' ) / ( b pow 2 ) `] THEN REWRITE_TAC[REAL_FIELD ` a / b * a' / b = ( a * a' ) / ( b pow 2 ) `; REAL_DIFFSQ; GSYM REAL_POW_2] THEN SIMP_TAC[SQRT_WORKS] THEN SIMP_TAC[REAL_FIELD ` ~ ( a = &0 ) ==> a * (--b pow 2 - (b pow 2 - &4 * a * c)) / (&2 * a) pow 2 = c `]);; let COMPUTE_TO_QUA_POLY = prove(` #2.696 <= x /\ x <= sqrt8 ==> x pow 2 * ( &1 / eta_y x #2.45 #2.45 pow 2 - &1 / eta_y x ( &2 ) #2.51 pow 2 ) = &4331842500 / &363188227801 * x pow 4 + -- &45702201 / &302530802 * x pow 2 + &529046001 / &2520040000 `, REWRITE_TAC[eta_y; eta_x; ups_x] THEN LET_TR THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN NHANH (MESON[REAL_ARITH ` #2.696 <= x /\ x <= sqrt8 ==> &0 <= #2.696 /\ &0 <= x `; REAL_LE_MUL2] ` #2.696 <= x /\ x <= sqrt8 ==> #2.696 * #2.696 <= x * x /\ x * x <= sqrt8 * sqrt8 `) THEN NHANH (MESON[REAL_ARITH ` #2.696 * #2.696 <= x ==> &0 <= #2.696 * #2.696 /\ &0 <= x `; REAL_LE_MUL2] ` #2.696 * #2.696 <= x /\ x <= hh ==> (#2.696 * #2.696) * #2.696 * #2.696 <= x * x /\ x * x <= hh * hh `) THEN REWRITE_TAC[sqrt8] THEN REWRITE_TAC[REAL_POLY_CONV ` (--(x * x) * x * x - &16 - &3969126001 / &100000000 + &2 * (x * x) * &63001 / &10000 + &2 * (x * x) * &4 + &63001 / &1250) `] THEN REWRITE_TAC[REAL_POLY_CONV ` (--(x * x) * x * x - &5764801 / &160000 - &5764801 / &160000 + &2 * (x * x) * &2401 / &400 + &2 * (x * x) * &2401 / &400 + &5764801 / &80000) `] THEN REWRITE_TAC[REAL_ARITH ` x pow 4 = ( x pow 2 ) pow 2 `] THEN MP_TAC (REAL_ARITH ` ~ ( -- &1 = &0 ) /\ &0 <= ( &103001 / &5000 ) pow 2 - &4 * ( -- &1 ) * -- &529046001 / &100000000 `) THEN SIMP_TAC[FACTOR_OF_QUADRARTIC] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN REWRITE_TAC[REAL_ARITH ` (&252004 / &625) = ( &502 / &25 ) * ( &502 / &25 ) `] THEN REWRITE_TAC[MESON[REAL_ARITH ` &0 <= &502 / &25 /\ x * x = x pow 2 `; POW_2_SQRT]` sqrt ( ( &502 / &25 ) * ( &502 / &25 )) = ( &502 / &25 ) `] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN REWRITE_TAC[ GSYM POW_2] THEN REWRITE_TAC[REAL_ARITH ` a * x pow 2 + b * x = ( a * x + b ) * x `] THEN REWRITE_TAC[MESON[SQRT_WORKS; REAL_ARITH ` &0 <= &8`]` sqrt (&8) pow 2 = &8 `] THEN NHANH (REAL_FIELD ` (&113569 / &15625 <= x pow 2 /\ x pow 2 <= &8) ==> &0 <= (-- &1 * x pow 2 + &2401 / &100) /\ &0 <= (x pow 2 - &2601 / &10000 ) /\ &0 <= -- ((x pow 2 - &203401 / &10000) )/\ &0 <= &5764801 / &160000 /\ &0 <= &63001 / &2500`) THEN MP_TAC REAL_LE_POW_2 THEN REWRITE_TAC[REAL_ARITH ` -- &1 * a * b = a * -- b `] THEN REWRITE_TAC[REAL_FIELD ` ( &1 / a ) pow 2 = &1 / ( a pow 2 ) `] THEN MP_TAC REAL_LE_MUL THEN MP_TAC REAL_LE_DIV THEN SIMP_TAC[ SQRT_WORKS] THEN REWRITE_TAC[REAL_SUB_LDISTRIB] THEN REWRITE_TAC[REAL_FIELD ` &1 / ( a / b ) = b / a `] THEN SIMP_TAC[REAL_FIELD ` &113569 / &15625 <= a ==> a * ( b / ( a * c )) = b / c `] THEN REWRITE_TAC[REAL_POLY_CONV ` ((-- &1 * x pow 2 + &2401 / &100) * x pow 2) / (&5764801 / &160000) - ((x pow 2 - &2601 / &10000) * --(x pow 2 - &203401 / &10000)) / (&63001 / &2500) `] THEN REWRITE_TAC[REAL_ARITH ` a pow 4 = a pow 2 pow 2 `]);; (* REAL_ARITH ` &4650694416 = ( &68196 ) pow 2 `;; REAL_ARITH` &4650694416 / &363188227801 = ( &68196 / &602651 ) pow 2 `;; *) let PHAN_TICH = prove( `! x. &4331842500 / &363188227801 * (x pow 2 - &488365801 / &44090000) * (x pow 2 - &2081667 / &1310000) = &4331842500 / &363188227801 * x pow 4 + -- &45702201 / &302530802 * x pow 2 + &529046001 / &2520040000` , REAL_ARITH_TAC);; let Q_TR = prove(`! x. #2.696 <= x /\ x <= sqrt8 ==> x pow 2 * (&1 / eta_y x #2.45 #2.45 pow 2 - &1 / eta_y x (&2) #2.51 pow 2) <= &0 `, SIMP_TAC[COMPUTE_TO_QUA_POLY; GSYM PHAN_TICH ] THEN NHANH (MESON[REAL_ARITH ` #2.696 <= x /\ x <= hh ==> &0 <= #2.696 /\ &0 <= x` ; REAL_LE_MUL2] ` #2.696 <= x /\ x <= hh ==> #2.696 * #2.696 <= x * x /\ x * x <= hh * hh `) THEN REWRITE_TAC[REAL_ARITH ` &4331842500 / &363188227801 * a <= &0 <=> a <= &0 `] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN REWRITE_TAC[REAL_ARITH ` &0 <= &4331842500 / &363188227801 * a <=> &0 <= a `; sqrt8; GSYM POW_2; MESON[SQRT_WORKS; REAL_ARITH ` &0 <= &8 `]` sqrt (&8) pow 2 = &8 `] THEN NHANH (REAL_ARITH ` &113569 / &15625 <= x pow 2 /\ x pow 2 <= &8 ==> x pow 2 - &488365801 / &44090000 <= &0 /\ x pow 2 - &2081667 / &1310000 >= &0 `) THEN REWRITE_TAC[ REAL_ARITH ` ( a >= &0 <=> &0 <= a)/\ (a <= &0 <=> &0 <= -- a ) `] THEN REWRITE_TAC[REAL_ARITH ` -- ( a * b ) = -- a * b `] THEN MESON_TAC[REAL_LE_MUL]);; let SQRT8_LT = prove(` sqrt (&8) < &4 * #2.45 `, MP_TAC (REAL_ARITH ` &0 < &8 /\ &0 < &4 * #2.45`) THEN SIMP_TAC[SQRT_POS_LT; LT_POW2_EQ_LT] THEN SIMP_TAC[REAL_LT_IMP_LE; SQRT_WORKS] THEN REAL_ARITH_TAC);; let SQRT8_POW2 = MESON[SQRT_WORKS; REAL_ARITH ` &0 <= &8 `]` sqrt (&8) pow 2 = &8 `;; let IM_UP_POS = prove(`! x. #2.696 <= x /\ x <= sqrt8 ==> &0 < ups_x (x * x) (#2.45 * #2.45) (#2.45 * #2.45) /\ &0 < ups_x (x * x) (&2 * &2) (#2.51 * #2.51) `, REWRITE_TAC[ups_x] THEN REWRITE_TAC[REAL_IDEAL_CONV [` (x:real) pow 2 `]` --(x * x) * x * x - (#2.45 * #2.45) * #2.45 * #2.45 - (#2.45 * #2.45) * #2.45 * #2.45 + &2 * (x * x) * #2.45 * #2.45 + &2 * (x * x) * #2.45 * #2.45 + &2 * (#2.45 * #2.45) * #2.45 * #2.45 `] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN REWRITE_TAC[REAL_POLY_CONV ` --(x * x) * x * x - &16 - &3969126001 / &100000000 + &2 * (x * x) * &63001 / &10000 + &2 * (x * x) * &4 + &63001 / &1250 `] THEN NHANH (REAL_ARITH` #2.696 <= x /\ x <= s ==> &0 <= #2.696 /\ &0 <= x /\ &0 <= s `) THEN ONCE_REWRITE_TAC[MESON[]` a /\ b ==> c <=> b ==> a ==> c `] THEN SIMP_TAC[POW2_COND; sqrt8; SQRT8_POW2] THEN NHANH (REAL_ARITH` #2.696 pow 2 <= x /\ x <= &8 ==> &0 < &2401 / &100 + -- &1 * x /\ &0 < x /\ ~ ( -- &1 = &0 ) /\ &0 <= ( &103001 / &5000 ) pow 2 - &4 * -- &1 * -- &529046001 / &100000000 `) THEN SIMP_TAC[REAL_ARITH ` x pow 4 = x pow 2 pow 2 `; FACTOR_OF_QUADRARTIC] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN REWRITE_TAC[REAL_ARITH ` &252004 / &625 = ( &502 / &25) pow 2 `] THEN REWRITE_TAC[MESON[POW_2_SQRT; REAL_ARITH ` &0 <= &502 / &25 `]` sqrt ((&502 / &25) pow 2) = &502 / &25 `] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN NHANH (REAL_ARITH ` &113569 / &15625 <= x pow 2 /\ x pow 2 <= &8 ==> &0 < x pow 2 - &2601 / &10000 /\ &0 < -- (x pow 2 - &203401 / &10000) `) THEN REWRITE_TAC[REAL_ARITH ` -- &1 * a * b = a * --b `] THEN SIMP_TAC[REAL_LT_MUL]);; let IMP_ETAY_POS = prove( `! x. #2.696 <= x /\ x <= sqrt8 ==> &0 < eta_y x #2.45 #2.45 /\ &0 < eta_y x (&2) #2.51 `, REWRITE_TAC[eta_y; eta_x] THEN LET_TR THEN NHANH (MESON[REAL_ARITH ` &0 <= #2.696`; REAL_LE_MUL2]` #2.696 <= x ==> #2.696 * #2.696 <= x * x `) THEN NHANH (REAL_ARITH ` #2.696 * #2.696 <= x * x ==> &0 < ((x * x) * (#2.45 * #2.45) * #2.45 * #2.45) /\ &0 < ((x * x) * (&2 * &2) * #2.51 * #2.51) `) THEN MESON_TAC[IM_UP_POS; REAL_LT_DIV; SQRT_POS_LT]);; let REAL_LE_RDIV_0 = prove(` ! a b. &0 < b ==> ( &0 <= a / b <=> &0 <= a ) `, REWRITE_TAC[REAL_ARITH ` &0 <= a <=> &0 < a \/ a = &0 `] THEN SIMP_TAC[REAL_LT_RDIV_0] THEN SIMP_TAC[REAL_FIELD `&0 < b ==> ( a / b = &0 <=> a = &0 ) `]);; let NHSJMDH = prove(` ! y. #2.696 <= y /\ y <= sqrt8 ==> eta_y y (&2) (#2.51) <= eta_y y #2.45 (#2.45) `, NHANH (SPEC_ALL Q_TR) THEN ONCE_REWRITE_TAC[MESON[]` a /\ b ==> c <=> a ==> b ==> c `] THEN NHANH (MESON[REAL_ARITH ` &0 <= #2.696`; REAL_LE_MUL2]` #2.696 <= x ==> #2.696 * #2.696 <= x * x `) THEN REWRITE_TAC[POW_2] THEN NHANH (REAL_ARITH `#2.696 * #2.696 <= y ==> &0 < y `) THEN REWRITE_TAC[REAL_ARITH ` a * b <= &0 <=> &0 <= a * -- b `] THEN SIMP_TAC[REAL_LE_MUL_EQ] THEN ONCE_REWRITE_TAC[MESON[]`( a/\b ) /\ c <=> ( a /\ c ) /\ b `] THEN NHANH (SPEC_ALL IMP_ETAY_POS) THEN NHANH (REAL_ARITH ` &0 < eta_y a b c ==> ~(eta_y a b c = &0 ) `) THEN REWRITE_TAC[GSYM REAL_POSSQ] THEN SIMP_TAC[REAL_FIELD ` &0 < a /\ &0 < b ==> -- (&1 / a - &1 / b) = (a - b) / ( a * b ) `] THEN PHA THEN SIMP_TAC[REAL_LT_MUL; REAL_LE_RDIV_0] THEN REWRITE_TAC[GSYM REAL_DIFFSQ] THEN SIMP_TAC[REAL_LT_ADD; REAL_LE_MUL_EQ] THEN REAL_ARITH_TAC);; (* NEW WORKS *) let SQRT8_LE = MESON[ REAL_ARITH ` &0 <= &8`; SQRT_WORKS]` &0 <= sqrt (&8) `;; let RELATE_POW2 = prove(` ( a = &0 <=> a pow 2 = &0 ) /\ ( &0 < a pow 2 <=> &0 < a \/ ~( &0 <= a )) `, MP_TAC (REAL_FIELD ` a = &0 <=> a pow 2 = &0 `) THEN DISCH_TAC THEN CONJ_TAC THENL [ASM_SIMP_TAC[]; MP_TAC REAL_LE_POW_2] THEN MP_TAC (REAL_ARITH `( ! a. &0 < a \/ ~(&0 <= a) \/ a = &0 )`) THEN MP_TAC (REAL_FIELD ` a = &0 <=> a pow 2 = &0 `) THEN REWRITE_TAC[REAL_ARITH ` A <= b <=> A = b \/ A < b `] THEN MESON_TAC[REAL_ARITH ` ~ ( a = &0 /\ ( &0 < a \/ ~( &0 <= a ) )) `]);; let LT_POW2_COND = prove(`!a b. &0 <= a /\ &0 <= b ==> (a < b <=> a pow 2 < b pow 2)`, REPEAT GEN_TAC THEN ASM_CASES_TAC ` a = &0 ` THENL [ASM_SIMP_TAC[REAL_ARITH` &0 pow 2 = &0 `] THEN MESON_TAC[RELATE_POW2]; ASM_SIMP_TAC[REAL_LE_LT]] THEN STRIP_TAC THENL [ASM_MESON_TAC[LT_POW2_EQ_LT]; EXPAND_TAC "b"] THEN UNDISCH_TAC `&0 < a ` THEN REWRITE_TAC[REAL_ARITH ` &0 pow 2 = &0 /\ (a < &0 <=> ~(&0 <= a))`] THEN MP_TAC REAL_LE_POW_2 THEN MESON_TAC[REAL_LT_IMP_LE]);; let POS_IMP_POW2 = MESON[REAL_LE_TRANS; POW2_COND]` &0 <= a /\ a <= b ==> a pow 2 <= b pow 2 `;; let SQRT8_LE_EQ_8_LESS_POW2 = prove(` sqrt (&8 ) <= a ==> &8 <= a pow 2 `, MP_TAC SQRT8_LE THEN MESON_TAC[SQRT8_POW2; POS_IMP_POW2]);; let MINIMAL_QUADRATIC_POLY = prove(` ! b c (x:real). ( &4 * c - b pow 2 ) / &4 <= x pow 2 + b * x + c `, ONCE_REWRITE_TAC[REAL_ARITH ` a <= b <=> &0 <= b - a `] THEN REWRITE_TAC[REAL_ARITH ` (x pow 2 + b * x + c) - (&4 * c - b pow 2) / &4 = ( x + b / &2 ) pow 2 `; REAL_LE_POW_2]);; let GREATER_THAN_MID_QUADRATIC_PO = prove(` ! b c x x0. -- b / &2 <= x0 /\ x0 <= x ==> x0 pow 2 + b * x0 + c <= x pow 2 + b * x + c `, REWRITE_TAC[REAL_ARITH ` x0 pow 2 + b * x0 + c <= x pow 2 + b * x + c <=> &0 <= ( x - x0 ) * ( x + x0 + b ) `] THEN MESON_TAC[REAL_ARITH ` --b / &2 <= x0 /\ x0 <= x ==> &0 <= x - x0 /\ &0 <= x + x0 + b `; REAL_LE_MUL]);; (* PERMAINENCE *) (* MARCH WORKS *) let SQRT8_TWO_TWO = prove(` sqrt (&8) <= &2 + &2 `, MP_TAC SQRT8_LE THEN NHANH (MESON[REAL_ARITH ` &0 <= &2 + &2 `] `&0 <= sqrt (&8) ==> &0 <= &2 + &2 `) THEN SIMP_TAC[POW2_COND] THEN SIMP_TAC[REAL_ARITH ` &0 <= &8 `; SQRT_WORKS] THEN REAL_ARITH_TAC);; let A_POS_DELTA = prove(` &0 < delta (#3.2 pow 2 ) (sqrt8 pow 2 ) (&2 pow 2) (sqrt8 pow 2) (&2 pow 2) (&2 pow 2) `, REWRITE_TAC[delta; sqrt8; SQRT8_POW2] THEN REAL_ARITH_TAC);; let MET_LAM_ROI = prove(` #3.2 < sqrt8 + &2 /\ #3.2 < &2 + &2 /\ sqrt8 < sqrt8 + &2 /\ sqrt8 < &2 + &2 `, REWRITE_TAC[sqrt8; REAL_ARITH ` a < sqrt (&8) + b <=> a - b < sqrt (&8) `] THEN REWRITE_TAC[REAL_ARITH ` sqrt (&8) - &2 < sqrt (&8) `] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN MP_TAC SQRT8_LE THEN MP_TAC (REAL_ARITH` &0 <= &6 / &5 /\ &0 <= &4 `) THEN SIMP_TAC[LT_POW2_COND ] THEN SIMP_TAC[LT_POW2_COND; SQRT8_POW2 ] THEN REAL_ARITH_TAC);; let PROVE_POS_THINGS = prove(` ! x. x IN {#3.2 , sqrt8, &2 , sqrt8, &2, &2 } ==> &0 <= x `, REWRITE_TAC[SET_RULE `( !x. x IN {a,b,c,d,s,e} ==> p x ) <=> p a /\ p b /\ p c /\ p d /\ p s /\ p e `;sqrt8; SQRT8_LE] THEN REAL_ARITH_TAC);; let IMP_GT_THAN_TWO = prove(` ! v1 v2 w1 (w2:real^3). CARD {v1, w1,v2, w2} = 4 /\ packing {v1, w1,v2, w2} ==> &2 <= dist3 w1 v2 /\ &2 <= dist3 v2 w2 /\ &2 <= dist3 v1 w2 `, REWRITE_TAC[CARD4; packing; GSYM dist3; sqrt8] THEN SET_TAC[]);; (* THADGSB *) let LEMMA_FOR_PAHFWSI = prove(`! v1 v2 v3 v4. CARD {v1, v2, v3, v4} = 4 /\ packing {v1, v2, v3, v4} /\ dist (v1,v3) <= #3.2 /\ #2.51 <= dist (v1,v2) /\ dist (v2,v4) <= #2.51 ==> (!x. x IN {#3.2, #2.51, &2, #2.51, &2, &2} ==> &0 <= x) /\ #3.2 < #2.51 + &2 /\ #3.2 < &2 + &2 /\ #2.51 < #2.51 + &2 /\ #2.51 < &2 + &2 /\ &0 < delta (#3.2 pow 2) (#2.51 pow 2) (&2 pow 2) (#2.51 pow 2) (&2 pow 2) (&2 pow 2) /\ CARD {v1, v2, v3, v4} = 4 /\ #2.51 <= dist3 v1 v2 /\ &2 <= dist3 v2 v3 /\ &2 <= dist3 v3 v4 /\ &2 <= dist3 v1 v4 /\ dist3 v1 v3 <= #3.2 /\ dist3 v2 v4 <= #2.51 `, REWRITE_TAC[SET_RULE ` (!x. x IN {a,b,c,d,e,f} ==> P x ) <=> P a /\ P b /\ P c /\ P d /\ P e /\ P f `; REAL_ARITH ` &0 <= #2.51 /\ &0 <= &2 /\ &0 <= &2 /\ &0 <= #3.2 /\ &0 <= &2 /\ &0 <= #2.51 /\ #2.51 < &2 + #2.51 /\ #2.51 < &2 + &2 /\ #3.2 < &2 + &2 /\ #3.2 < #2.51 + &2 /\ #3.2 < &2 + #2.51 /\ #2.51 < #2.51 + &2 `] THEN SIMP_TAC[GSYM dist3] THEN REWRITE_TAC[CARD4; packing; delta; dist3] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN SET_TAC[]);; let LEMMA_OF_39 = prove(` ! (v1:real^3) v2 w1 w2. CARD {v1, v2, w1, w2} = 4 /\ packing {v1, v2, w1, w2} /\ dist (w1,w2) <= #2.51 /\ dist (v1,v2) <= #3.07 ==> (!x. x IN {#2.51, &2, &2, #3.07, &2, &2} ==> &0 <= x) /\ #2.51 < &2 + &2 /\ #2.51 < &2 + &2 /\ #3.07 < &2 + &2 /\ #3.07 < &2 + &2 /\ &0 < delta (#2.51 pow 2) (&2 pow 2) (&2 pow 2) (#3.07 pow 2) (&2 pow 2) (&2 pow 2) /\ CARD {w1, v1, w2, v2} = 4 /\ &2 <= dist3 w1 v1 /\ &2 <= dist3 v1 w2 /\ &2 <= dist3 w2 v2 /\ &2 <= dist3 w1 v2 /\ dist3 w1 w2 <= #2.51 /\ dist3 v1 v2 <= #3.07 `, REWRITE_TAC[SET_RULE ` (!x. x IN {a,b,c,d,e,f} ==> P x ) <=> P a /\ P b /\ P c /\ P d /\ P e /\ P f `; delta; GSYM dist3] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN REPEAT GEN_TAC THEN STRIP_TAC THEN CONJ_TAC THENL [ASM_MESON_TAC[SET_RULE ` {v1, v2, w1, w2} = {w1, v1, w2, v2}`];DOWN_TAC] THEN REWRITE_TAC[CARD4; packing; dist3] THEN SET_TAC[]);; let LEMMA_OF_LEMMA40 = prove(`! v1 v2 w1 (w2:real^3). CARD {v1, v2, w1, w2} = 4 /\ packing {v1, v2, w1, w2} /\ dist (v1,v2) <= #3.2 /\ dist (w1,w2) <= #2.51 /\ #2.2 <= dist (v1,w1) ==> (!x. x IN {#3.2, #2.2, &2, #2.51, &2, &2} ==> &0 <= x) /\ #3.2 < #2.2 + &2 /\ #3.2 < &2 + &2 /\ #2.51 < #2.2 + &2 /\ #2.51 < &2 + &2 /\ &0 < delta (#3.2 pow 2) (#2.2 pow 2) (&2 pow 2) (#2.51 pow 2) (&2 pow 2) (&2 pow 2) /\ CARD {v1, w1, v2, w2} = 4 /\ #2.2 <= dist3 v1 w1 /\ &2 <= dist3 w1 v2 /\ &2 <= dist3 v2 w2 /\ &2 <= dist3 v1 w2 /\ dist3 v1 v2 <= #3.2 /\ dist3 w1 w2 <= #2.51 `, REWRITE_TAC[SET_RULE ` (! x. x IN {a,b,c,d,e,f} ==> P x ) <=> P a /\ P b /\ P c /\ P d /\ P e /\ P f `; delta] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN SIMP_TAC[SET_RULE ` {v1, v2, w1, w2} = {v1, w1, v2, w2} `; packing] THEN SIMP_TAC[CARD4; GSYM dist3] THEN SET_TAC[]);; let LEOF41 = prove( `#3.114467 < x ==> delta (#2.51 pow 2) (&2 pow 2) (&2 pow 2) (&2 pow 2) (&2 pow 2) (x pow 2) < &0`, NHANH (MESON[REAL_ARITH ` #3.114467 < x ==> &0 < #3.114467 /\ &0 < x `; LT_POW2_EQ_LT]` #3.114467 < x ==> ( #3.114467 ) pow 2 < x pow 2 `) THEN REWRITE_TAC[delta] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN REWRITE_TAC[ REAL_POLY_CONV ` -- &126002 / &625 - &4 * &4 * x pow 2 - &4 * &4 * x pow 2 + &63001 / &10000 * x pow 2 * (-- &63001 / &10000 + &4 + &4 + &4 + &4 - x pow 2) + &4 * &4 * (&23001 / &10000 + &4 + &0 + x pow 2) + &4 * &4 * (&63001 / &10000 + -- &4 + &4 + x pow 2) `] THEN REWRITE_TAC[REAL_ARITH ` a pow 4 = a pow 2 pow 2 `] THEN REWRITE_TAC[REAL_ARITH ` a * x pow 2 + b * x = ( a * x + b ) * x `] THEN NHANH (REAL_ARITH `&9699904694089 / &1000000000000 < x pow 2 ==> -- &63001 / &10000 * x pow 2 + &6111033999 / &100000000 < &0` ) THEN NHANH (REAL_ARITH `&9699904694089 / &1000000000000 < x ==> &0 < x `) THEN REWRITE_TAC[REAL_ARITH ` a < &0 <=> &0 < -- a `; REAL_ARITH ` -- ( a * b ) = -- a * b `] THEN MESON_TAC[REAL_LT_MUL]);; let LEMMA41 = prove(`! v1 v2 v3 (v4:real^3). CARD {v1,v2,v3,v4} = 4 /\ dist3 v1 v2 = #2.51 /\ dist3 v1 v3 = &2 /\ dist3 v1 v4 = &2 /\ dist3 v2 v3 = &2 /\ dist3 v2 v4 = &2 ==> dist3 v3 v4 <= #3.114467 `, REPEAT GEN_TAC THEN MP_TAC LEMMA3 THEN LET_TR THEN REWRITE_TAC[REAL_ARITH ` x <= #3.114467 <=> ~ (#3.114467 < x ) `] THEN REWRITE_TAC[REAL_ARITH ` x <= #3.114467 <=> ~ (#3.114467 < x ) `; MESON[]` a ==> ~ b <=> a /\ b ==> F `] THEN PHA THEN NHANH (SPEC_ALL (prove(`! (v1:real^3) v2 v3 v4. dist3 v1 v2 = #2.51 /\ dist3 v1 v3 = &2 /\ dist3 v1 v4 = &2 /\ dist3 v2 v3 = &2 /\ dist3 v2 v4 = &2 /\ #3.114467 < dist3 v3 v4 ==> delta (dist (v1,v2) pow 2) (dist (v1,v3) pow 2) (dist (v1,v4) pow 2) (dist (v2,v3) pow 2) (dist (v2,v4) pow 2) (dist (v3,v4) pow 2) < &0 `, SIMP_TAC[dist3] THEN MESON_TAC[LEOF41]))) THEN REWRITE_TAC[REAL_ARITH ` a < &0 <=> ~( &0 <= a ) `; dist3] THEN MESON_TAC[]);; let YXWIPMH = LEMMA41;; let LEMMA_OF_L42 = prove(`sqrt8 <= dist3 v2 v4 /\ #3.488 <= x ==> -- &1 * x pow 2 * dist3 v2 v4 pow 2 + -- &1 * x pow 4 + &103001 / &5000 * x pow 2 + -- &529046001 / &100000000 < &0`, MP_TAC SQRT8_LE THEN IMP_IMP_TAC THEN NHANH (MESON[REAL_ARITH ` &0 <= a /\ a <= b /\ #3.488 <= x ==> &0 <= b /\ &0 <= #3.488 /\ &0 <= x `; POW2_COND]` &0 <= a /\ a <= b /\ #3.488 <= x ==> a pow 2 <= b pow 2 /\ #3.488 pow 2 <= x pow 2 `) THEN REWRITE_TAC[SQRT8_POW2; sqrt8] THEN NHANH (MESON[REAL_ARITH ` &0 <= a /\ a <= b /\ #3.488 <= x ==> &0 <= b /\ &0 <= #3.488 /\ &0 <= x `; POW2_COND]` &0 <= a /\ a <= b /\ #3.488 <= x ==> a pow 2 <= b pow 2 /\ #3.488 pow 2 <= x pow 2 `) THEN REWRITE_TAC[SQRT8_POW2] THEN NHANH (MESON[REAL_ARITH ` &0 <= &8 /\ &0 <= #3.488 pow 2 `; REAL_LE_MUL2]` &8 <= a /\ #3.488 pow 2 <= b ==> &8 * #3.488 pow 2 <= a * b `) THEN REWRITE_TAC[REAL_ARITH` a pow 4 = a pow 2 pow 2 `] THEN NHANH (MESON[REAL_ARITH ` #3.488 pow 2 <= x ==> &0 <= #3.488 pow 2 /\ &0 <= x `; POW2_COND]` #3.488 pow 2 <= x ==> #3.488 pow 2 pow 2 <= x pow 2 `) THEN REWRITE_TAC[REAL_ARITH ` a + -- &1 * x pow 2 + b * x + c = a + -- &1 * ( x pow 2 + -- b * x + -- c ) `] THEN NHANH (prove(` #3.488 pow 2 <= x pow 2 ==> #3.488 pow 2 pow 2 + --(&103001 / &5000) * #3.488 pow 2 + --(-- &529046001 / &100000000) <= x pow 2 pow 2 + --(&103001 / &5000) * x pow 2 + --(-- &529046001 / &100000000) `, MP_TAC (REAL_ARITH ` -- ( --(&103001 / &5000)) / &2 <= #3.488 pow 2 `) THEN MESON_TAC[GREATER_THAN_MID_QUADRATIC_PO ])) THEN REAL_ARITH_TAC);; let LEMMA_IN_LEMMA42_P25 = prove(` ! v1 v2 v3 v4 x. dist3 v1 v2 = #2.51 /\ dist3 v1 v4 = #2.51 /\ dist3 v2 v3 = &2 /\ dist3 v3 v4 = &2 /\ sqrt8 <= dist3 v2 v4 /\ #3.488 <= x ==> delta (dist3 v1 v2 pow 2) ( x pow 2) (dist3 v1 v4 pow 2) (dist3 v2 v3 pow 2) (dist3 v2 v4 pow 2) (dist3 v3 v4 pow 2) < &0 `, SIMP_TAC[] THEN NHANH (MESON[REAL_ARITH` #3.488 <= x ==> &0 <= #3.488 /\ &0 <= x `; POW2_COND]` #3.488 <= x ==> (#3.488 pow 2 <= x pow 2 ) `) THEN REWRITE_TAC[delta] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN REWRITE_TAC[REAL_POLY_CONV `--(&63001 / &10000 * x pow 2 * &4) - &63001 / &10000 * &63001 / &10000 * dist3 v2 v4 pow 2 - x pow 2 * &63001 / &2500 - &4 * dist3 v2 v4 pow 2 * &4 + &63001 / &10000 * &4 * (-- &63001 / &10000 + x pow 2 + &63001 / &10000 + &4 + dist3 v2 v4 pow 2 - &4) + x pow 2 * dist3 v2 v4 pow 2 * (&63001 / &10000 - x pow 2 + &63001 / &10000 + &4 - dist3 v2 v4 pow 2 + &4) + &63001 / &10000 * &4 * (&63001 / &10000 + x pow 2 - &63001 / &10000 - &4 + dist3 v2 v4 pow 2 + &4) `] THEN REWRITE_TAC[REAL_IDEAL_CONV [` y pow 2 `] `-- &1 * x pow 4 * y pow 2 + -- &1 * x pow 2 * y pow 4 + &103001 / &5000 * x pow 2 * y pow 2 + -- &529046001 / &100000000 * y pow 2 `] THEN REWRITE_TAC[MESON[]` a/\ #3.488 <= x /\ c <=> (a/\ #3.488 <= x )/\ c`] THEN NHANH (LEMMA_OF_L42) THEN REWRITE_TAC[sqrt8] THEN NHANH (SQRT8_LE_EQ_8_LESS_POW2) THEN REPEAT GEN_TAC THEN STRIP_TAC THEN UNDISCH_TAC ` &8 <= dist3 v2 v4 pow 2 ` THEN UNDISCH_TAC ` -- &1 * x pow 2 * dist3 v2 v4 pow 2 + -- &1 * x pow 4 + &103001 / &5000 * x pow 2 + -- &529046001 / &100000000 < &0 ` THEN ABBREV_TAC ` xx = (-- &1 * x pow 2 * dist3 v2 v4 pow 2 + -- &1 * x pow 4 + &103001 / &5000 * x pow 2 + -- &529046001 / &100000000)` THEN NHANH (REAL_ARITH ` &8 <= a ==> &0 < a `) THEN REWRITE_TAC[REAL_ARITH ` ( a * b < &0 <=> &0 < ( -- a ) * b )/\ ( a < &0 <=> &0 < -- a )`] THEN SIMP_TAC[REAL_LT_MUL]);; let PAATDXJ =prove(` ! v1 v2 v3 (v4:real^3). CARD {v1,v2,v3,v4} = 4 /\ dist3 v1 v2 = #2.51 /\ dist3 v1 v4 = #2.51 /\ dist3 v2 v3 = &2 /\ dist3 v3 v4 = &2 /\ sqrt8 <= dist3 v2 v4 ==> dist3 v1 v3 < #3.488 `, MP_TAC LEMMA3 THEN LET_TR THEN REWRITE_TAC[REAL_ARITH ` a < b <=> ~ ( b <= a )`] THEN REWRITE_TAC[MESON[]` a ==> ~ b <=> ~( a /\b)`] THEN PHA THEN NHANH (SPEC_ALL LEMMA_IN_LEMMA42_P25) THEN REWRITE_TAC[REAL_ARITH` a < b <=> ~(b <= a ) `] THEN SIMP_TAC[dist3]);; let CONVEX_NORMBALL = REWRITE_RULE[GSYM NORMBALL_BALL] CONVEX_BALL ;; let CONVEX_HULL4 = SPEC `{(v1:real^N),v2,v3,v4}` CONVEX_HULL_FINITE;; let CONVEX_HULL_4_EQUIV = prove(` ! v1 v2 v3 (v4:real^N). conv {v1,v2,v3,v4} = { x | ? a b c d. &0 <= a /\ &0 <= b /\ &0 <= c /\ &0 <= d /\ a + b + c + d = &1 /\ a % v1 + b % v2 + c % v3 + d % v4 = x } `, REWRITE_TAC[conv; FUN_EQ_THM; affsign; lin_combo; UNION_EMPTY; IN_ELIM_THM; sgn_ge] THEN REWRITE_TAC[MESON[]` x = vsum aa bb /\ a /\ b <=> a /\ b /\ vsum aa bb = x `] THEN ONCE_REWRITE_TAC[SET_RULE ` a s ==> b <=> s IN a ==> b `] THEN SIMP_TAC[CONVEX_HULL_FINITE_STEP; FINITE_INSERT; FINITE_RULES] THEN REWRITE_TAC[REAL_ARITH `x - y = z:real <=> x = y + z`; VECTOR_ARITH `x - y = z:real^N <=> x = y + z`] THEN REWRITE_TAC[VECTOR_ADD_RID; REAL_ADD_RID] THEN MESON_TAC[IN]);; let TXDIACY = prove(`! (a:real^3) b c d (v0: real^3) r. {a, b, c, d} SUBSET normball v0 r ==> convex hull {a, b, c, d} SUBSET normball v0 r `, REPEAT GEN_TAC THEN MP_TAC (MESON[CONVEX_NORMBALL]` convex (normball (v0:real^3) r)`) THEN NHANH (MESON[FINITE6] ` {a, b, c, d} SUBSET s ==> FINITE {(a:real^3),b,c,d} `) THEN REWRITE_TAC[CONVEX_HULL4; CONVEX_EXPLICIT] THEN IMP_IMP_TAC THEN REWRITE_TAC[SET_RULE ` {a | P a } SUBSET b <=> (! a. P a ==> a IN b)`] THEN REWRITE_TAC[MESON[]` (! y. ( ? u. P u y ) ==> Q y ) <=> (! y u. P u y ==> Q y ) `] THEN REWRITE_TAC[MESON[]`(!y u. P u /\ Q u /\ R u = y ==> Z y) <=> (!u. P u /\ Q u ==> Z (R u)) `] THEN MESON_TAC[]);; let LEMMA14 = TXDIACY;; let ECSEVNC = prove(`?t1 t2 t3 t4. !v1 v2 v3 v4 (v: real^3). ~coplanar_alt {v1, v2, v3, v4} ==> t1 v1 v2 v3 v4 v + t2 v1 v2 v3 v4 v + t3 v1 v2 v3 v4 v + t4 v1 v2 v3 v4 v = &1 /\ v = t1 v1 v2 v3 v4 v % v1 + t2 v1 v2 v3 v4 v % v2 + t3 v1 v2 v3 v4 v % v3 + t4 v1 v2 v3 v4 v % v4 /\ (!ta tb tc td. v = ta % v1 + tb % v2 + tc % v3 + td % v4 /\ ta + tb + tc + td = &1 ==> ta = t1 v1 v2 v3 v4 v /\ tb = t2 v1 v2 v3 v4 v /\ tc = t3 v1 v2 v3 v4 v /\ td = t4 v1 v2 v3 v4 v) `, REWRITE_TAC[GSYM SKOLEM_THM; RIGHT_EXISTS_IMP_THM] THEN REPEAT GEN_TAC THEN NHANH (SPEC_ALL (prove(`!v1 v2 v3 v0 v:real^3. ~coplanar_alt {v0, v1, v2, v3} ==> (?t1 t2 t3. v - v0 = t1 % (v1 - v0) + t2 % (v2 - v0) + t3 % (v3 - v0) /\ (!ta tb tc. v - v0 = ta % (v1 - v0) + tb % (v2 - v0) + tc % (v3 - v0) ==> ta = t1 /\ tb = t2 /\ tc = t3))`, SIMP_TAC[NONCOPLANAR_3_BASIS]))) THEN STRIP_TAC THEN EXISTS_TAC ` &1 - t1 - t2 - t3 ` THEN EXISTS_TAC ` t1:real ` THEN EXISTS_TAC ` t2:real ` THEN EXISTS_TAC ` t3:real ` THEN CONJ_TAC THENL [REAL_ARITH_TAC; CONJ_TAC] THENL [UNDISCH_TAC ` (v:real^3) - v1 = t1 % (v2 - v1) + t2 % (v3 - v1) + t3 % (v4 - v1)` THEN CONV_TAC VECTOR_ARITH; REPEAT GEN_TAC] THEN REWRITE_TAC[MESON[]` a /\ b ==> c <=> b ==> a ==> c `; REAL_ARITH ` ta + tb + tc + td = &1 <=> ta = &1 - tb - tc - td `] THEN SIMP_TAC[] THEN REWRITE_TAC[VECTOR_ARITH ` v = (&1 - tb - tc - td) % v1 + tb % v2 + tc % v3 + td % v4 <=> v - v1 = tb % ( v2 - v1 ) + tc % ( v3 - v1 ) + td % ( v4 - v1 ) `] THEN ASM_MESON_TAC[]);; let LEMMA76 = ECSEVNC;; let COEFS_4 = new_specification ["COEF4_1"; "COEF4_2"; "COEF4_3"; "COEF4_4"] ECSEVNC ;; let COEF_1_EQ_ZERO = prove(` ! v1 v2 v3 v4 (v:real^3). ~ coplanar_alt {v1,v2,v3,v4} ==> ( COEF4_1 v1 v2 v3 v4 v = &0 <=> v IN aff {v2,v3,v4} ) `, REWRITE_TAC[aff; AFFINE_HULL_3; IN_ELIM_THM] THEN NHANH (SPEC_ALL COEFS_4) THEN REPEAT GEN_TAC THEN STRIP_TAC THEN ONCE_REWRITE_TAC[REAL_ARITH` u + v + w = &0 + u + v + w `] THEN ONCE_REWRITE_TAC[VECTOR_ARITH` u + v + w = &0 % v1 + u + v + w `] THEN ASM_MESON_TAC[]);; let EQ_IMP_COPLANAR = prove(`! a b c (d:real^3). ( a = b \/ a = c \/ a = d ) ==> coplanar_alt {a,b,c,d} `, REPEAT STRIP_TAC THENL [ ASM_SIMP_TAC[SET_RULE ` a INSERT ( a INSERT s ) = a INSERT s `] THEN MP_TAC (DIMINDEX_3) THEN MESON_TAC[COPLANAR_3; ARITH_RULE` a = 3 ==> 2 <= a `]; ONCE_REWRITE_TAC[SET_RULE` {a,b,v,c} = {a,v,b,c} `] THEN ASM_SIMP_TAC[SET_RULE ` a INSERT ( a INSERT s ) = a INSERT s `] THEN MP_TAC (DIMINDEX_3) THEN MESON_TAC[COPLANAR_3; ARITH_RULE` a = 3 ==> 2 <= a `]; ONCE_REWRITE_TAC[SET_RULE` {a,b,v,c} = {a,c,v,b} `] THEN ASM_SIMP_TAC[SET_RULE ` a INSERT ( a INSERT s ) = a INSERT s `] THEN MP_TAC (DIMINDEX_3) THEN MESON_TAC[COPLANAR_3; ARITH_RULE` a = 3 ==> 2 <= a `]]);; let AFFINE_HULL_FINITE_STEP_GEN = prove (`!P:real^N->real->bool. ((?u. (!x. x IN {} ==> P x (u x)) /\ sum {} u = w /\ vsum {} (\x. u(x) % x) = y) <=> w = &0 /\ y = vec 0) /\ (FINITE(s:real^N->bool) /\ (!y. a IN s /\ P a y ==> P a (y / &2)) /\ (!x y. a IN s /\ P a x /\ P a y ==> P a (x + y)) ==> ((?u. (!x. x IN (a INSERT s) ==> P x (u x)) /\ sum (a INSERT s) u = w /\ vsum (a INSERT s) (\x. u(x) % x) = y) <=> ?v u. P a v /\ (!x. x IN s ==> P x (u x)) /\ sum s u = w - v /\ vsum s (\x. u(x) % x) = y - v % a))`, GEN_TAC THEN SIMP_TAC[SUM_CLAUSES; VSUM_CLAUSES; NOT_IN_EMPTY] THEN CONJ_TAC THENL [MESON_TAC[]; ALL_TAC] THEN DISCH_TAC THEN ASM_CASES_TAC `(a:real^N) IN s` THEN ASM_REWRITE_TAC[] THENL [ASM_SIMP_TAC[SET_RULE `a IN s ==> a INSERT s = s`] THEN EQ_TAC THEN REWRITE_TAC[LEFT_IMP_EXISTS_THM] THENL [X_GEN_TAC `u:real^N->real` THEN STRIP_TAC THEN EXISTS_TAC `(u:real^N->real) a / &2` THEN EXISTS_TAC `\x:real^N. if x = a then u x / &2 else u x`; MAP_EVERY X_GEN_TAC [`v:real`; `u:real^N->real`] THEN STRIP_TAC THEN EXISTS_TAC `\x:real^N. if x = a then u x + v else u x`] THEN ASM_SIMP_TAC[] THEN (CONJ_TAC THENL [ASM_MESON_TAC[]; ALL_TAC]) THEN ONCE_REWRITE_TAC[COND_RAND] THEN ONCE_REWRITE_TAC[COND_RATOR] THEN ASM_SIMP_TAC[VSUM_CASES; SUM_CASES] THEN ASM_SIMP_TAC[GSYM DELETE; SUM_DELETE; VSUM_DELETE] THEN ASM_SIMP_TAC[SET_RULE `a IN s ==> {x | x IN s /\ x = a} = {a}`] THEN REWRITE_TAC[SUM_SING; VSUM_SING] THEN (CONJ_TAC THENL [REAL_ARITH_TAC; VECTOR_ARITH_TAC]); EQ_TAC THEN REWRITE_TAC[LEFT_IMP_EXISTS_THM] THENL [X_GEN_TAC `u:real^N->real` THEN STRIP_TAC THEN EXISTS_TAC `(u:real^N->real) a` THEN EXISTS_TAC `u:real^N->real` THEN ASM_SIMP_TAC[IN_INSERT] THEN REPEAT(FIRST_X_ASSUM(SUBST1_TAC o SYM)) THEN CONJ_TAC THENL [REAL_ARITH_TAC; VECTOR_ARITH_TAC]; MAP_EVERY X_GEN_TAC [`v:real`; `u:real^N->real`] THEN STRIP_TAC THEN EXISTS_TAC `\x:real^N. if x = a then v:real else u x` THEN ASM_SIMP_TAC[IN_INSERT] THEN CONJ_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN ONCE_REWRITE_TAC[COND_RAND] THEN ONCE_REWRITE_TAC[COND_RATOR] THEN ASM_SIMP_TAC[VSUM_CASES; SUM_CASES] THEN ASM_SIMP_TAC[GSYM DELETE; SUM_DELETE; VSUM_DELETE] THEN ASM_SIMP_TAC[SET_RULE `~(a IN s) ==> {x | x IN s /\ x = a} = {}`] THEN ASM_SIMP_TAC[SET_RULE `~(a IN s) ==> s DELETE a = s`] THEN REWRITE_TAC[SUM_CLAUSES; VSUM_CLAUSES] THEN CONJ_TAC THENL [REAL_ARITH_TAC; VECTOR_ARITH_TAC]]]);; let THEOREM_RE_AFF_LT31 = prove (`!v1 v2 v3 vv x:real^N. ~(v1 = vv) /\ ~(v2 = vv) /\ ~(v3 = vv) ==> ((?f. f vv < &0 /\ sum {v1, v2, v3, vv} f = &1 /\ x = vsum {v1, v2, v3, vv} (\v. f v % v)) <=> {x | ?a b c t. a + b + c + t = &1 /\ x = a % v1 + b % v2 + c % v3 + t % vv /\ t < &0} x)`, REPEAT STRIP_TAC THEN MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC `?f. (!x:real^N. x IN {v1, v2, v3, vv} ==> vv = x ==> f x < &0) /\ sum {v1, v2, v3, vv} f = &1 /\ vsum {v1, v2, v3, vv} (\v. f v % v) = x` THEN CONJ_TAC THENL [ASM_REWRITE_TAC[FORALL_IN_INSERT; NOT_IN_EMPTY] THEN MESON_TAC[]; SIMP_TAC[AFFINE_HULL_FINITE_STEP_GEN; REAL_ARITH `x < &0 /\ y < &0 ==> x + y < &0`; REAL_ARITH `x < &0 ==> x / &2 < &0`; FINITE_INSERT; CONJUNCT1 FINITE_RULES; RIGHT_EXISTS_AND_THM] THEN ASM_REWRITE_TAC[IN_ELIM_THM; REAL_ARITH `x - y:real = z <=> x = y + z`; VECTOR_ARITH `x - y:real^N = z <=> x = y + z`] THEN REWRITE_TAC[VECTOR_ADD_RID; REAL_ADD_RID] THEN MESON_TAC[]]);; let AFF_LT31 = prove(` ! v1 v2 v3 (vv: real^N). ~ (vv IN {v1,v2,v3} ) ==> aff_lt {v1,v2,v3} {vv} = { x| ? a b c t. t < &0 /\ a + b + c + t = &1 /\ x = a % v1 + b % v2 + c % v3 + t % vv } `, REWRITE_TAC[IN_SET3; DE_MORGAN_THM; aff_lt_def;FUN_EQ_THM; affsign; lin_combo; sgn_lt] THEN REWRITE_TAC[SET_RULE` {v1, v2, v3} UNION {vv} = {v1, v2, v3, vv}`] THEN REWRITE_TAC[SET_RULE` a /\ (!w. {vv} w ==> f w < &0) /\ b <=> f vv < &0 /\ b /\ a `] THEN SIMP_TAC[THEOREM_RE_AFF_LT31; IN_ELIM_THM] THEN SET_TAC[]);; let AFF_LT21 = prove(`! a b (v0:real^N). ~ ( a = v0 ) /\ ~( b = v0 ) ==> aff_lt {a,b} {v0} = {x | ? ta tb t. ta + tb + t = &1 /\ t < &0 /\ x = ta % a + tb % b + t % v0} `, REWRITE_TAC[SET_RULE` ~(a = v0) /\ ~(b = v0) <=> ~ ( v0 IN {a,b} ) `] THEN ONCE_REWRITE_TAC[SET_RULE` {a,b} = {a,b,b} `] THEN SIMP_TAC[AFF_LT31] THEN SIMP_TAC[AFF_LT31; FUN_EQ_THM; IN_ELIM_THM] THEN REWRITE_TAC[VECTOR_ARITH` a % b + c % b + x = ( a + c ) % b + x `] THEN MESON_TAC[REAL_ARITH` a + b + c = ( a + b ) + c `; VECTOR_ARITH ` a % v = ( a + &0 ) % v `; REAL_ARITH ` a + b = a + &0 + b `]);; let INSET3 = SET_RULE` a IN {a,b,c} /\ b IN {a,b,c} /\ c IN {a,b,c} `;; let AFF_GT33 = prove(`! (v1:real^N) v2 v3 w1 w2 w3. {v1, v2, v3} INTER {w1, w2, w3} = {} ==> aff_gt {v1, v2, v3} {w1, w2, w3} = {x | ?a1 a2 a3 b1 b2 b3. &0 < b1 /\ &0 < b2 /\ &0 < b3 /\ a1 + a2 + a3 + b1 + b2 + b3 = &1 /\ x = a1 % v1 + a2 % v2 + a3 % v3 + b1 % w1 + b2 % w2 + b3 % w3}`, REWRITE_TAC[aff_gt_def; FUN_EQ_THM; affsign; lin_combo; sgn_gt] THEN REPEAT STRIP_TAC THEN MATCH_MP_TAC EQ_TRANS THEN REWRITE_TAC[SET_RULE ` ( a INSERT b ) UNION c = b UNION ( a INSERT c ) /\ {} UNION b = b `] THEN EXISTS_TAC ` (? f. x = vsum {v3, v2, v1, w1, w2, w3} (\v. f v % v) /\ (!(w:real^N). w IN {v3,v2,v1, w1, w2, w3} ==> w IN {w1,w2,w3} ==> &0 < f w) /\ sum {v3, v2, v1, w1, w2, w3} f = &1 ) ` THEN REWRITE_TAC[SET_RULE` (!x. ({v1, v2, v3} INTER {w1, w2, w3}) x <=> {} x) <=> {v1, v2, v3} INTER {w1, w2, w3} = {} `] THEN CONJ_TAC THENL [ FIRST_X_ASSUM MP_TAC THEN REWRITE_TAC[SET_RULE` (!x. ({v1, v2, v3} INTER {w1, w2, w3}) x <=> {} x) <=> {v1, v2, v3} INTER {w1, w2, w3} = {} `] THEN MESON_TAC[SET_RULE` {v1, v2, v3} INTER {w1, w2, w3} = {} ==> ( (!w. {w1, w2, w3} w ==> &0 < f w) <=> (!w. w IN {v3, v2, v1, w1, w2, w3} ==> w IN {w1, w2, w3} ==> &0 < f w) ) `]; REWRITE_TAC[MESON[]` a /\ (!z. P z ) /\ aa = &1 <=> (!z. P z ) /\ aa = &1 /\ a `]] THEN ONCE_REWRITE_TAC[MESON[]` a = vsum b c <=> vsum b c = a `] THEN SIMP_TAC[AFFINE_HULL_FINITE_STEP_GEN;FINITE_INSERT; CONJUNCT1 FINITE_RULES; RIGHT_EXISTS_AND_THM; REAL_ARITH `&0 < x /\ &0 < y ==> &0 < x + y`; REAL_ARITH `&0 < x ==> &0 < x / &2 `] THEN FIRST_X_ASSUM MP_TAC THEN REWRITE_TAC[SET_RULE` (!x. ({v1, v2, v3} INTER {w1, w2, w3}) x <=> {} x) <=> {v1, v2, v3} INTER {w1, w2, w3} = {} `; SET_RULE` ( a INSERT s ) INTER ss = {} <=> ~ ( a IN ss ) /\ s INTER ss = {} `] THEN SIMP_TAC[INSET3] THEN SIMP_TAC[INSET3; REAL_ARITH` a - b = c <=> a = b + c `; VECTOR_ARITH` a:real^N - b = c <=> a = b + c `] THEN REWRITE_TAC[ GSYM RIGHT_EXISTS_AND_THM; ZERO_NEUTRAL; IN_ELIM_THM; VECTOR_ARITH ` a + vec 0 = a `] THEN DISCH_TAC THEN MESON_TAC[REAL_ARITH` a + b + c + d = c + b + a + d `; VECTOR_ARITH` ( a:real^N ) + b + c + d = c + b + a + d `]);; let AFF_GE33 = prove_by_refinement( `! (v1:real^N) v2 v3 w1 w2 w3. {v1, v2, v3} INTER {w1, w2, w3} = {} ==> aff_ge {v1, v2, v3} {w1, w2, w3} = {x | ?a1 a2 a3 b1 b2 b3. &0 <= b1 /\ &0 <= b2 /\ &0 <= b3 /\ a1 + a2 + a3 + b1 + b2 + b3 = &1 /\ x = a1 % v1 + a2 % v2 + a3 % v3 + b1 % w1 + b2 % w2 + b3 % w3}`, (* {{{ proof *) [ (REWRITE_TAC[aff_gt_def; aff_ge_def; FUN_EQ_THM; affsign; lin_combo; sgn_gt; sgn_ge]); (REPEAT STRIP_TAC); (MATCH_MP_TAC EQ_TRANS ); (REWRITE_TAC[SET_RULE ` ( a INSERT b ) UNION c = b UNION ( a INSERT c ) /\ {} UNION b = b `]); (EXISTS_TAC ` (? f. x = vsum {v3, v2, v1, w1, w2, w3} (\v. f v % v) /\ (!(w:real^N). w IN {v3,v2,v1, w1, w2, w3} ==> w IN {w1,w2,w3} ==> &0 <= f w) /\ sum {v3, v2, v1, w1, w2, w3} f = &1 ) `); (CONJ_TAC); (FIRST_X_ASSUM MP_TAC); (REWRITE_TAC[SET_RULE` (!x. ({v1, v2, v3} INTER {w1, w2, w3}) x <=> {} x) <=> {v1, v2, v3} INTER {w1, w2, w3} = {} `]); BY((MESON_TAC[SET_RULE` {v1, v2, v3} INTER {w1, w2, w3} = {} ==> ( (!w. {w1, w2, w3} w ==> &0 <= f w) <=> (!w. w IN {v3, v2, v1, w1, w2, w3} ==> w IN {w1, w2, w3} ==> &0 <= f w) ) `])); (REWRITE_TAC[MESON[]` a /\ (!z. P z ) /\ aa = &1 <=> (!z. P z ) /\ aa = &1 /\ a `]); (ONCE_REWRITE_TAC[MESON[]` a = vsum b c <=> vsum b c = a `]); ( SIMP_TAC[AFFINE_HULL_FINITE_STEP_GEN;FINITE_INSERT; CONJUNCT1 FINITE_RULES; RIGHT_EXISTS_AND_THM; REAL_ARITH `&0 <= x /\ &0 <= y ==> &0 <= x + y`; REAL_ARITH `&0 <= x ==> &0 <= x / &2 `]); (FIRST_X_ASSUM MP_TAC); (REWRITE_TAC[SET_RULE` (!x. ({v1, v2, v3} INTER {w1, w2, w3}) x <=> {} x) <=> {v1, v2, v3} INTER {w1, w2, w3} = {} `; SET_RULE` ( a INSERT s ) INTER ss = {} <=> ~ ( a IN ss ) /\ s INTER ss = {} `]); (SIMP_TAC[INSET3]); (SIMP_TAC[INSET3; REAL_ARITH` a - b = c <=> a = b + c `; VECTOR_ARITH` a:real^N - b = c <=> a = b + c `]); (REWRITE_TAC[ GSYM RIGHT_EXISTS_AND_THM; ZERO_NEUTRAL; IN_ELIM_THM; VECTOR_ARITH ` a + vec 0 = a `]); (DISCH_TAC); BY( (MESON_TAC[REAL_ARITH` a + b + c + d = c + b + a + d `; VECTOR_ARITH` ( a:real^N ) + b + c + d = c + b + a + d `])) ]);; (* }}} *) let AFF_GE_12 = prove(`!v0 (a:real^N) b. ~(v0 = a \/ v0 = b) ==> aff_ge {v0} {a, b} = {x | ?tv ta tb. &0 <= ta /\ &0 <= tb /\ tv + ta + tb = &1 /\ x = tv % v0 + ta % a + tb % b}`, REWRITE_TAC[SET_RULE ` ~(v0 = a \/ v0 = b) <=> {v0} INTER {a,b} = {} `] THEN ONCE_REWRITE_TAC[SET_RULE` {a} = {a,a} `] THEN ONCE_REWRITE_TAC[SET_RULE` {a,a} = {a,a,a} `] THEN ONCE_REWRITE_TAC[SET_RULE` {a,b,b,b} = {a,b,b} `] THEN SIMP_TAC[AFF_GE33] THEN REWRITE_TAC[FUN_EQ_THM; IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN REWRITE_TAC[GSYM VECTOR_ADD_RDISTRIB; VECTOR_ARITH` a % v + b % v + y = ( a + b ) % v + y `] THEN GONTONG THEN EQ_TAC THENL [ MESON_TAC[REAL_ARITH` a1 + a2 + a3 + b1 + b2 + b3 = ( a1 + a2 + a3 ) + b1 + b2 + b3 `; REAL_ARITH ` &0 <= a /\ &0 <= b ==> &0 <= a + b `];STRIP_TAC] THEN EXISTS_TAC` tv: real ` THEN EXISTS_TAC` &0 ` THEN EXISTS_TAC` &0` THEN EXISTS_TAC` ta :real ` THEN EXISTS_TAC` &0` THEN EXISTS_TAC` tb:real ` THEN ASM_SIMP_TAC[REAL_ARITH ` a <= a `; ZERO_NEUTRAL]);; let INSET3 = SET_RULE` a IN {a, b, c} /\ b IN {a, b, c} /\ c IN {a, b, c} /\ {a, b, c} a /\ {a, b, c} b /\ {a, b, c} c `;; let AFF_LE_LT33 = prove(`! (v1:real^N) v2 v3 w1 w2 w3. {v1, v2, v3} INTER {w1, w2, w3} = {} ==> aff_le {v1, v2, v3} {w1, w2, w3} = {x | ?a1 a2 a3 b1 b2 b3. b1 <= &0 /\ b2 <= &0 /\ b3 <= &0 /\ a1 + a2 + a3 + b1 + b2 + b3 = &1 /\ x = a1 % v1 + a2 % v2 + a3 % v3 + b1 % w1 + b2 % w2 + b3 % w3} /\ aff_lt {v1, v2, v3} {w1, w2, w3} = {x | ?a1 a2 a3 b1 b2 b3. b1 < &0 /\ b2 < &0 /\ b3 < &0 /\ a1 + a2 + a3 + b1 + b2 + b3 = &1 /\ x = a1 % v1 + a2 % v2 + a3 % v3 + b1 % w1 + b2 % w2 + b3 % w3} `, REWRITE_TAC[IN_ELIM_THM; aff_le_def; FUN_EQ_THM; aff_lt_def; affsign; lin_combo; sgn_lt; sgn_le] THEN REWRITE_TAC[SET_RULE` {v1, v2, v3} UNION {w1, w2, w3} = {v1,v2,v3,w1,w2,w3} `] THEN ONCE_REWRITE_TAC[SET_RULE` {w1, w2, w3} w ==> P w <=> w IN {v1,v2,v3,w1,w2,w3} ==> {w1,w2,w3} w ==> P w `] THEN REWRITE_TAC[MESON[]` a = vsum aa bb /\ (! w. P w ) /\ b <=> (! w. P w ) /\ b /\ vsum aa bb = a `] THEN SIMP_TAC[AFFINE_HULL_FINITE_STEP_GEN; REAL_ARITH `( x < &0 /\ y < &0 ==> x + y < &0) /\ ( x <= &0 /\ y <= &0 ==> x + y <= &0)`; REAL_ARITH ` (x < &0 ==> x / &2 < &0 ) /\ (x <= &0 ==> x / &2 <= &0 )`; FINITE_INSERT; CONJUNCT1 FINITE_RULES ; RIGHT_EXISTS_AND_THM] THEN SIMP_TAC[ GSYM RIGHT_EXISTS_AND_THM; SET_RULE ` (!x. ({v1, v2, v3} INTER s ) x <=> {} x) <=> ~ ( s v1 ) /\ ~ ( s v2 ) /\ ~ ( s v3 ) `; INSET3] THEN REWRITE_TAC[REAL_ARITH` a - b = c <=> a = b + c`; REAL_ARITH ` a + &0 = a `; VECTOR_ARITH` (a:real^N) - b = c <=> a = b + c`; VECTOR_ARITH` a + vec 0 = a `] THEN MESON_TAC[]);; let AFF_GES_LTS = prove(` ! a b c (v0 :real^N). ~ ( a = v0 ) /\ ~( b = v0 ) /\ ~( c = v0 ) ==> aff_gt {a, b} {v0} = {x | ?ta tb t. ta + tb + t = &1 /\ &0 < t /\ x = ta % a + tb % b + t % v0} /\ aff_ge {a, b} {v0} = {x | ?ta tb t. ta + tb + t = &1 /\ &0 <= t /\ x = ta % a + tb % b + t % v0} /\ aff_lt {a,b,c} {v0} = { x| ? ta tb tc t. t < &0 /\ ta + tb + tc + t = &1 /\ x = ta % a + tb % b + tc % c + t % v0 } /\ aff_gt {a,b,c} {v0} = { x| ? ta tb tc t. &0 < t /\ ta + tb + tc + t = &1 /\ x = ta % a + tb % b + tc % c + t % v0 } `, ONCE_REWRITE_TAC[SET_RULE` {a} = {a,a,a} `] THEN ONCE_REWRITE_TAC[SET_RULE` {a,b,b,b} = {a,b,b} `] THEN ONCE_REWRITE_TAC[SET_RULE` {a,b,c,c} = {a,b,c} `] THEN NHANH (SET_RULE` ~(a = v0) /\ ~(b = v0) /\ ~(c = v0) ==> {a,b,b} INTER {v0,v0,v0} = {} /\ {a,b,c} INTER {v0,v0,v0} = {} `) THEN SIMP_TAC[AFF_LE_LT33; AFF_GE33; AFF_GT33] THEN REWRITE_TAC[GSYM VECTOR_ADD_RDISTRIB; VECTOR_ARITH` a % x + b % x + y = ( a + b ) % x + y `] THEN REWRITE_TAC[REAL_ARITH` (a + b ) + c = a + b + c `] THEN REPEAT STRIP_TAC THENL [ REWRITE_TAC[FUN_EQ_THM; IN_ELIM_THM] THEN GEN_TAC THEN EQ_TAC THENL [MESON_TAC[REAL_ARITH ` &0 < a /\ &0 < b ==> &0 < a + b `; REAL_ARITH ` a + b + c + d = a + ( b + c ) + d `]; MESON_TAC[REAL_ARITH ` a + b + c = a + b / &2 + b / &2 + c / &3 + c / &3 + c / &3 `; REAL_ARITH` &0 < a <=> &0 < a / &3 `; REAL_ARITH` a = a / &2 + a / &2 /\ b = b / &3 + b / &3 + b / &3 /\ b = ( b / &3 + b / &3 ) + b / &3 `]]; REPEAT STRIP_TAC THEN REWRITE_TAC[FUN_EQ_THM; IN_ELIM_THM] THEN GEN_TAC THEN EQ_TAC THENL [ MESON_TAC[REAL_ARITH ` ( &0 < a /\ &0 < b ==> &0 < a + b ) /\ ( &0 <= a /\ &0 <= b ==> &0 <= a + b ) `; REAL_ARITH ` a + b + c + d = a + ( b + c ) + d `] ; MESON_TAC[REAL_ARITH ` a + b + c = a + b / &2 + b / &2 + c / &3 + c / &3 + c / &3 `; REAL_ARITH` ( &0 < a <=> &0 < a / &3) /\ ( &0 <= a <=> &0 <= a / &3) `; REAL_ARITH` a = a / &2 + a / &2 /\ b = b / &3 + b / &3 + b / &3 /\ b = ( b / &3 + b / &3 ) + b / &3 `]]; REPEAT STRIP_TAC THEN REWRITE_TAC[FUN_EQ_THM; IN_ELIM_THM] THEN GEN_TAC THEN EQ_TAC THENL [MESON_TAC[REAL_ARITH ` ( &0 < a /\ &0 < b ==> &0 < a + b ) /\ ( &0 <= a /\ &0 <= b ==> &0 <= a + b ) `; REAL_ARITH ` ( a < &0 /\ b < &0 ==> a + b < &0 )`; REAL_ARITH ` a + b + c + d = a + ( b + c ) + d `]; STRIP_TAC] THEN EXISTS_TAC `ta :real` THEN EXISTS_TAC `tb :real` THEN EXISTS_TAC `tc :real` THEN REPEAT (EXISTS_TAC ` t / &3 `) THEN ASM_MESON_TAC[REAL_ARITH` a < &0 <=> a / &3 < &0 `; REAL_ARITH ` a = a / &3 + a / &3 + a / &3 `]; REPEAT STRIP_TAC THEN REWRITE_TAC[FUN_EQ_THM; IN_ELIM_THM] THEN GEN_TAC THEN EQ_TAC THENL [MESON_TAC[REAL_ARITH ` ( &0 < a /\ &0 < b ==> &0 < a + b ) /\ ( &0 <= a /\ &0 <= b ==> &0 <= a + b ) `; REAL_ARITH ` ( a < &0 /\ b < &0 ==> a + b < &0 )`; REAL_ARITH ` a + b + c + d = a + ( b + c ) + d `]; STRIP_TAC] THEN EXISTS_TAC `ta :real` THEN EXISTS_TAC `tb :real` THEN EXISTS_TAC `tc :real` THEN REPEAT (EXISTS_TAC ` t / &3 `) THEN ASM_MESON_TAC[REAL_ARITH ` a = a / &3 + a / &3 + a / &3 `; REAL_ARITH ` &0 < a <=> &0 < a / &3 `]]);; let AFF_GES_GTS = prove(` ! a b c (v0:real^N). ~(a = v0) /\ ~(b = v0) /\ ~(c = v0) ==> aff_gt {a, b} {v0} = {x | ?ta tb t. ta + tb + t = &1 /\ &0 < t /\ x = ta % a + tb % b + t % v0} /\ aff_ge {a, b} {v0} = {x | ?ta tb t. ta + tb + t = &1 /\ &0 <= t /\ x = ta % a + tb % b + t % v0} /\ aff_lt {a, b, c} {v0} = {x | ?ta tb tc t. t < &0 /\ ta + tb + tc + t = &1 /\ x = ta % a + tb % b + tc % c + t % v0} /\ aff_gt {a, b, c} {v0} = {x | ?ta tb tc t. &0 < t /\ ta + tb + tc + t = &1 /\ x = ta % a + tb % b + tc % c + t % v0} /\ aff_ge {a, b, c} {v0} = {x | ?ta tb tc t. &0 <= t /\ ta + tb + tc + t = &1 /\ x = ta % a + tb % b + tc % c + t % v0} `, REPEAT GEN_TAC THEN REWRITE_TAC[MESON[]` (a ==> a1 /\ a2 /\ a3 /\ a4 /\ a5) <=> ( a ==> a1 /\ a2 /\ a3 /\a4 ) /\ ( a ==> a5) `] THEN REWRITE_TAC[AFF_GES_LTS] THEN NHANH (SET_RULE` ~(a = v0) /\ ~(b = v0) /\ ~(c = v0) ==> {a,b,c} INTER {v0,v0,v0} = {} `) THEN ONCE_REWRITE_TAC[SET_RULE` {v} = {v,v,v} `] THEN ONCE_REWRITE_TAC[SET_RULE` {a, b, c, c, c} = {a,b,c} `] THEN SIMP_TAC[AFF_GE33] THEN REPEAT STRIP_TAC THEN REWRITE_TAC[FUN_EQ_THM; IN_ELIM_THM; GSYM VECTOR_ADD_RDISTRIB] THEN GEN_TAC THEN EQ_TAC THENL [ MESON_TAC[REAL_ARITH` &0 <= a /\ &0 <= b ==> &0 <= a + b `]; STRIP_TAC THEN EXISTS_TAC ` ta :real` THEN EXISTS_TAC ` tb :real` THEN EXISTS_TAC ` tc :real` THEN REPEAT ( EXISTS_TAC ` t / &3 `) THEN ASM_MESON_TAC[REAL_ARITH` a = a / &3 + a / &3 + a / &3 `; REAL_ARITH` &0 <= a <=> &0 <= a / &3 `]]);; let COEF_1_POS_NEG = prove(` ! v1 v2 v3 v4 (v:real^3). ~ coplanar_alt {v1,v2,v3,v4} ==> ( COEF4_1 v1 v2 v3 v4 v > &0 <=> v IN aff_gt {v2,v3,v4} {v1} ) /\ ( COEF4_1 v1 v2 v3 v4 v < &0 <=> v IN aff_lt {v2,v3, v4} {v1} ) `, NHANH (MESON[EQ_IMP_COPLANAR]`~coplanar_alt {v1, v2, v3, v4} ==> ~ ( v2 = v1 ) /\ ~ ((v3:real^3) = v1 ) /\ ~ (v4 = v1 ) `) THEN SIMP_TAC[AFF_GES_LTS] THEN NHANH (SPEC_ALL COEFS_4) THEN REWRITE_TAC[IN_ELIM_THM; REAL_ARITH ` a > b <=> b < a `] THEN REPEAT GEN_TAC THEN STRIP_TAC THEN ONCE_REWRITE_TAC[REAL_ARITH ` a + b + c + t = t + a + b + c `] THEN ONCE_REWRITE_TAC[VECTOR_ARITH ` (a:real^N) + b + c + t = t + a + b + c `] THEN ASM_MESON_TAC[]);; let ALL_ABOUT_COEF_1 = prove(` ! v1 v2 v3 v4 (v:real^3). ~ coplanar_alt {v1,v2,v3,v4} ==> ( COEF4_1 v1 v2 v3 v4 v < &0 <=> v IN aff_lt {v2,v3, v4} {v1} ) /\ ( COEF4_1 v1 v2 v3 v4 v = &0 <=> v IN aff {v2,v3,v4} ) /\ ( COEF4_1 v1 v2 v3 v4 v > &0 <=> v IN aff_gt {v2,v3,v4} {v1} )`, SIMP_TAC[COEF_1_EQ_ZERO ; COEF_1_POS_NEG ]);; let PER_COEF1_WITH_COEF2 = prove(`! v1 v2 v3 v4 (v:real^3). ~coplanar_alt {v1, v2, v3, v4} ==> COEF4_2 v1 v2 v3 v4 v = COEF4_1 v2 v3 v4 v1 v `, NHANH (SPEC_ALL COEFS_4) THEN REPEAT GEN_TAC THEN STRIP_TAC THEN MP_TAC (SPECL [` v2:real^3 `; `v3:real^3`; `v4:real^3`; ` v1:real^3`; `v:real^3 `] COEFS_4) THEN UNDISCH_TAC ` ~coplanar_alt {v1, v2, v3, (v4:real^3)}` THEN IMP_IMP_TAC THEN REWRITE_TAC[MESON[SET_RULE` {v1, v2, v3, v4} = {v2, v3, v4, v1}`]` ~coplanar_alt {v1, v2, v3, v4} /\ (~coplanar_alt {v2, v3, v4, v1} ==> l ) <=> ~coplanar_alt {v1, v2, v3, v4} /\ l `] THEN ONCE_REWRITE_TAC[GSYM (REAL_ARITH` a + b + c + d = b + c + d + a `)] THEN ONCE_REWRITE_TAC[GSYM (VECTOR_ARITH` (a:real^N) + b + c + d = b + c + d + a `)] THEN ASM_MESON_TAC[]);; let PER_COEF1_WITH_COEF3 = prove(`! v1 v2 v3 v4 (v:real^3). ~coplanar_alt {v1, v2, v3, v4} ==> COEF4_3 v1 v2 v3 v4 v = COEF4_1 v3 v4 v1 v2 v `, NHANH (SPEC_ALL COEFS_4) THEN REPEAT GEN_TAC THEN STRIP_TAC THEN MP_TAC (SPECL [`v3:real^3`; `v4:real^3`; ` v1:real^3`; ` v2:real^3`; `v:real^3 `] COEFS_4) THEN UNDISCH_TAC ` ~coplanar_alt {v1, v2, v3, (v4:real^3)}` THEN IMP_IMP_TAC THEN REWRITE_TAC[MESON[SET_RULE` {v1, v2, v3, v4} = {v3, v4, v1, v2}`]` ~coplanar_alt {v1, v2, v3, v4} /\ (~coplanar_alt {v3, v4, v1, v2} ==> l ) <=> ~coplanar_alt {v1, v2, v3, v4} /\ l `] THEN ONCE_REWRITE_TAC[GSYM (REAL_ARITH` a + b + c + d = c + d + a + b`)] THEN ONCE_REWRITE_TAC[GSYM (VECTOR_ARITH` (a:real^N) + b + c + d = c + d + a + b`)] THEN ASM_MESON_TAC[]);; let PER_COEF1_WITH_COEF4 = prove(`! v1 v2 v3 v4 (v:real^3). ~coplanar_alt {v1, v2, v3, v4} ==> COEF4_4 v1 v2 v3 v4 v = COEF4_1 v4 v1 v2 v3 v `, NHANH (SPEC_ALL COEFS_4) THEN REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[SET_RULE` {v1, v2, v3, v4} = {v4,v1, v2, v3}`] THEN NHANH (SPEC_ALL COEFS_4) THEN MESON_TAC[REAL_ARITH` ta + tb + tc + td = td + ta + tb + tc`; VECTOR_ARITH` ta + tb + tc + td = td + ta + tb + (tc:real^N)`]);; let ALL_ABOUT_COEF_2 = prove(` ! v1 v2 v3 v4 (v:real^3). ~ coplanar_alt {v1,v2,v3,v4} ==> ( COEF4_2 v1 v2 v3 v4 v < &0 <=> v IN aff_lt {v1,v3, v4} {v2} ) /\ ( COEF4_2 v1 v2 v3 v4 v = &0 <=> v IN aff {v1,v3,v4} ) /\ ( COEF4_2 v1 v2 v3 v4 v > &0 <=> v IN aff_gt {v1,v3,v4} {v2} )`, SIMP_TAC[PER_COEF1_WITH_COEF2] THEN MP_TAC ALL_ABOUT_COEF_1 THEN MESON_TAC[SET_RULE` {v1, v2, v3, v4} = {v2, v3, v4, v1}`; SET_RULE` {v1, v2, v3} = {v2, v3,v1}`]);; let ALL_ABOUT_COEF_3 = prove(` ! v1 v2 v3 v4 (v:real^3). ~ coplanar_alt {v1,v2,v3,v4} ==> ( COEF4_3 v1 v2 v3 v4 v < &0 <=> v IN aff_lt {v2,v1, v4} {v3} ) /\ ( COEF4_3 v1 v2 v3 v4 v = &0 <=> v IN aff {v2,v1,v4} ) /\ ( COEF4_3 v1 v2 v3 v4 v > &0 <=> v IN aff_gt {v2,v1,v4} {v3} ) `, SIMP_TAC[PER_COEF1_WITH_COEF3] THEN ONCE_REWRITE_TAC[SET_RULE` {v2, v1, v4} = {v4,v1,v2} `] THEN ONCE_REWRITE_TAC[SET_RULE` {v1, v4, v3, v2} = {v3,v4,v1,v2} `] THEN SIMP_TAC[ALL_ABOUT_COEF_1]);; let SRGTIHY = prove(` ! v1 v2 v3 v4 (v:real^3). ~ coplanar_alt {v1,v2,v3,v4} ==> ( COEF4_1 v1 v2 v3 v4 v < &0 <=> v IN aff_lt {v2,v3, v4} {v1} ) /\ ( COEF4_1 v1 v2 v3 v4 v = &0 <=> v IN aff {v2,v3,v4} ) /\ ( COEF4_1 v1 v2 v3 v4 v > &0 <=> v IN aff_gt {v2,v3,v4} {v1} ) /\ ( COEF4_2 v1 v2 v3 v4 v < &0 <=> v IN aff_lt {v1,v3, v4} {v2} ) /\ ( COEF4_2 v1 v2 v3 v4 v = &0 <=> v IN aff {v1,v3,v4} ) /\ ( COEF4_2 v1 v2 v3 v4 v > &0 <=> v IN aff_gt {v1,v3,v4} {v2} ) /\ ( COEF4_3 v1 v2 v3 v4 v < &0 <=> v IN aff_lt {v2,v1, v4} {v3} ) /\ ( COEF4_3 v1 v2 v3 v4 v = &0 <=> v IN aff {v2,v1,v4} ) /\ ( COEF4_3 v1 v2 v3 v4 v > &0 <=> v IN aff_gt {v2,v1,v4} {v3} )/\ ( COEF4_4 v1 v2 v3 v4 v < &0 <=> v IN aff_lt {v2,v1, v3} {v4} ) /\ ( COEF4_4 v1 v2 v3 v4 v = &0 <=> v IN aff {v2,v1,v3} ) /\ ( COEF4_4 v1 v2 v3 v4 v > &0 <=> v IN aff_gt {v2,v1,v3} {v4} )`, SIMP_TAC[ALL_ABOUT_COEF_1; ALL_ABOUT_COEF_2; ALL_ABOUT_COEF_3; PER_COEF1_WITH_COEF4] THEN ONCE_REWRITE_TAC[SET_RULE` {v2, v1, v3} = {v1,v2,v3}`] THEN ONCE_REWRITE_TAC[SET_RULE` {v1, v3, v2, v4} = {v4,v1,v2,v3}`] THEN SIMP_TAC[ALL_ABOUT_COEF_1]);; let LEMMA77 = SRGTIHY;; let CONV0_4 = prove (`conv0 {v1, v2, v3, v4} = {x:real^N | ?a b c d. &0 < a /\ &0 < b /\ &0 < c /\ &0 < d /\ a + b + c + d = &1 /\ a % v1 + b % v2 + c % v3 + d % v4 = x}`, REWRITE_TAC[FUN_EQ_THM; IN_ELIM_THM] THEN X_GEN_TAC `y:real^N` THEN REWRITE_TAC[conv0; affsign; sgn_gt; lin_combo; UNION_EMPTY] THEN MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC `?f. (!w:real^N. w IN {v1, v2, v3, v4} ==> &0 < f w) /\ sum {v1, v2, v3, v4} f = &1 /\ vsum {v1, v2, v3, v4} (\v. f v % v) = y` THEN CONJ_TAC THENL [REWRITE_TAC[IN] THEN MESON_TAC[]; ALL_TAC] THEN SIMP_TAC[AFFINE_HULL_FINITE_STEP_GEN; REAL_ARITH `&0 < x /\ &0 < y ==> &0 < x + y`; REAL_ARITH `&0 < x ==> &0 < x / &2`; FINITE_INSERT; CONJUNCT1 FINITE_RULES; RIGHT_EXISTS_AND_THM] THEN ASM_REWRITE_TAC[IN_ELIM_THM; REAL_ARITH `x - y:real = z <=> x = y + z`; VECTOR_ARITH `x - y:real^N = z <=> x = y + z`] THEN REWRITE_TAC[VECTOR_ADD_RID; REAL_ADD_RID] THEN MESON_TAC[]);; (* ======================= *) (* LEMMA 81 *) (* ======================= *) let ARIKWRQ = prove(`! v1 v2 v3 (v4:real^3). let s = {v1,v2,v3,v4} in CARD s = 4 /\ ~ coplanar_alt s ==> conv s = aff_ge ( s DIFF {v1} ) {v1} INTER aff_ge ( s DIFF {v2} ) {v2} INTER aff_ge ( s DIFF {v3} ) {v3} INTER aff_ge ( s DIFF {v4} ) {v4} `, LET_TR THEN SIMP_TAC[CARD4; SET_RULE ` ~(v1 IN {v2, v3, v4}) /\ ~(v2 = v3 \/ v3 = v4 \/ v4 = v2) ==> {v1, v2, v3, v4} DIFF {v1} = {v2,v3,v4} /\ {v1, v2, v3, v4} DIFF {v2} = {v3,v4,v1} /\ {v1, v2, v3, v4} DIFF {v3} = {v4,v1,v2} /\ {v1, v2, v3, v4} DIFF {v4} = {v1,v2,v3} `] THEN REWRITE_TAC[CARD4; IN_SET3;DE_MORGAN_THM] THEN SIMP_TAC[AFF_GES_GTS] THEN REWRITE_TAC[CONVEX_HULL_4_EQUIV] THEN REPEAT STRIP_TAC THEN REWRITE_TAC[SET_RULE ` a = b <=> (! x. x IN a <=> x IN b ) `; IN_INTER; IN_ELIM_THM] THEN GEN_TAC THEN EQ_TAC THENL [ ASM_MESON_TAC[REAL_ARITH` a + b + c + d = d + a + b + c `; VECTOR_ARITH` (a:real^N) + b + c + d = d + a + b + c `]; FIRST_X_ASSUM MP_TAC ] THEN NHANH (SPEC ` x: real^3` (GEN ` v:real^3` (SPEC_ALL COEFS_4))) THEN ABBREV_TAC ` aa = COEF4_1 v1 v2 v3 v4 x ` THEN ABBREV_TAC ` bb = COEF4_2 v1 v2 v3 v4 x ` THEN ABBREV_TAC ` cc = COEF4_3 v1 v2 v3 v4 x ` THEN ABBREV_TAC ` dd = COEF4_4 v1 v2 v3 v4 x ` THEN REWRITE_TAC[MESON[]` a ==> b ==> c <=> a /\ b ==> c `] THEN PHA THEN NHANH (MESON[REAL_ARITH` a + b + c + d = d + a + b + c `; VECTOR_ARITH` (a:real^N) + b + c + d = d + a + b + c `]` aa + bb + cc + dd = &1 /\ x = aa % v1 + bb % v2 + cc % v3 + dd % v4 /\ (!ta tb tc td. x = ta % v1 + tb % v2 + tc % v3 + td % v4 /\ ta + tb + tc + td = &1 ==> ta = aa /\ tb = bb /\ tc = cc /\ td = dd) /\ (?ta tb tc t. &0 <= t /\ ta + tb + tc + t = &1 /\ x = ta % v2 + tb % v3 + tc % v4 + t % v1) /\ (?ta tb tc t. &0 <= t /\ ta + tb + tc + t = &1 /\ x = ta % v3 + tb % v4 + tc % v1 + t % v2) /\ (?ta tb tc t. &0 <= t /\ ta + tb + tc + t = &1 /\ x = ta % v4 + tb % v1 + tc % v2 + t % v3) /\ (?ta tb tc t. &0 <= t /\ ta + tb + tc + t = &1 /\ x = ta % v1 + tb % v2 + tc % v3 + t % v4) ==> &0 <= aa /\ &0 <= bb /\ &0 <= cc /\ &0 <= dd`) THEN MATCH_MP_TAC (MESON[]` ( a1 /\ a2 /\ a3 ==> l) ==> aa /\ ( a1 /\ a2 /\ a4 ) /\ a3 ==> l `) THEN MESON_TAC[]);; (* ================ *) (* LEMMA 82 *) (* ================= *) let MXHKOXR = prove(`! v1 v2 v3 (v4:real^3). let s = {v1,v2,v3,v4} in CARD s = 4 /\ ~ coplanar_alt s ==> conv0 s = aff_gt ( s DIFF {v1} ) {v1} INTER aff_gt ( s DIFF {v2} ) {v2} INTER aff_gt ( s DIFF {v3} ) {v3} INTER aff_gt ( s DIFF {v4} ) {v4} `, LET_TR THEN SIMP_TAC[CARD4; SET_RULE ` ~(v1 IN {v2, v3, v4}) /\ ~(v2 = v3 \/ v3 = v4 \/ v4 = v2) ==> {v1, v2, v3, v4} DIFF {v1} = {v2,v3,v4} /\ {v1, v2, v3, v4} DIFF {v2} = {v3,v4,v1} /\ {v1, v2, v3, v4} DIFF {v3} = {v4,v1,v2} /\ {v1, v2, v3, v4} DIFF {v4} = {v1,v2,v3} `] THEN REWRITE_TAC[CARD4; IN_SET3;DE_MORGAN_THM] THEN SIMP_TAC[AFF_GES_GTS; CONV0_4 ] THEN REPEAT STRIP_TAC THEN REWRITE_TAC[SET_RULE ` a = b <=> (! x. x IN a <=> x IN b ) `; IN_INTER; IN_ELIM_THM] THEN GEN_TAC THEN EQ_TAC THENL [ ASM_MESON_TAC[REAL_ARITH` a + b + c + d = d + a + b + c `; VECTOR_ARITH` (a:real^N) + b + c + d = d + a + b + c `]; FIRST_X_ASSUM MP_TAC ] THEN NHANH (SPEC ` x: real^3` (GEN ` v:real^3` (SPEC_ALL COEFS_4))) THEN ABBREV_TAC ` aa = COEF4_1 v1 v2 v3 v4 x ` THEN ABBREV_TAC ` bb = COEF4_2 v1 v2 v3 v4 x ` THEN ABBREV_TAC ` cc = COEF4_3 v1 v2 v3 v4 x ` THEN ABBREV_TAC ` dd = COEF4_4 v1 v2 v3 v4 x ` THEN REWRITE_TAC[MESON[]` a ==> b ==> c <=> a /\ b ==> c `] THEN PHA THEN NHANH (MESON[REAL_ARITH` a + b + c + d = d + a + b + c `; VECTOR_ARITH` (a:real^N) + b + c + d = d + a + b + c `]` aa + bb + cc + dd = &1 /\ x = aa % v1 + bb % v2 + cc % v3 + dd % v4 /\ (!ta tb tc td. x = ta % v1 + tb % v2 + tc % v3 + td % v4 /\ ta + tb + tc + td = &1 ==> ta = aa /\ tb = bb /\ tc = cc /\ td = dd) /\ (?ta tb tc t. &0 < t /\ ta + tb + tc + t = &1 /\ x = ta % v2 + tb % v3 + tc % v4 + t % v1) /\ (?ta tb tc t. &0 < t /\ ta + tb + tc + t = &1 /\ x = ta % v3 + tb % v4 + tc % v1 + t % v2) /\ (?ta tb tc t. &0 < t /\ ta + tb + tc + t = &1 /\ x = ta % v4 + tb % v1 + tc % v2 + t % v3) /\ (?ta tb tc t. &0 < t /\ ta + tb + tc + t = &1 /\ x = ta % v1 + tb % v2 + tc % v3 + t % v4) ==> &0 < aa /\ &0 < bb /\ &0 < cc /\ &0 < dd `) THEN MATCH_MP_TAC (MESON[]` ( a1 /\ a2 /\ a3 ==> l) ==> aa /\ ( a1 /\ a2 /\ a4 ) /\ a3 ==> l `) THEN MESON_TAC[]);; let CONV0_4 = prove (`conv0 {v1, v2, v3, v4} = {x:real^N | ?a b c d. &0 < a /\ &0 < b /\ &0 < c /\ &0 < d /\ a + b + c + d = &1 /\ a % v1 + b % v2 + c % v3 + d % v4 = x}`, REWRITE_TAC[FUN_EQ_THM; IN_ELIM_THM] THEN X_GEN_TAC `y:real^N` THEN REWRITE_TAC[conv0; affsign; sgn_gt; lin_combo; UNION_EMPTY] THEN MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC `?f. (!w:real^N. w IN {v1, v2, v3, v4} ==> &0 < f w) /\ sum {v1, v2, v3, v4} f = &1 /\ vsum {v1, v2, v3, v4} (\v. f v % v) = y` THEN CONJ_TAC THENL [REWRITE_TAC[IN] THEN MESON_TAC[]; ALL_TAC] THEN SIMP_TAC[AFFINE_HULL_FINITE_STEP_GEN; REAL_ARITH `&0 < x /\ &0 < y ==> &0 < x + y`; REAL_ARITH `&0 < x ==> &0 < x / &2`; FINITE_INSERT; CONJUNCT1 FINITE_RULES; RIGHT_EXISTS_AND_THM] THEN ASM_REWRITE_TAC[IN_ELIM_THM; REAL_ARITH `x - y:real = z <=> x = y + z`; VECTOR_ARITH `x - y:real^N = z <=> x = y + z`] THEN REWRITE_TAC[VECTOR_ADD_RID; REAL_ADD_RID] THEN MESON_TAC[]);; let CONV0_4POINTS = CONV0_4;; (* ================== *) (* LEMMA 78 *) (* ================== *) let ZRFMKPY = prove(` ! v1 v2 v3 v4 (v:real^3). ~coplanar_alt {v1, v2, v3, v4} ==> (v IN conv {v1, v2, v3, v4} <=> &0 <= COEF4_1 v1 v2 v3 v4 v /\ &0 <= COEF4_2 v1 v2 v3 v4 v /\ &0 <= COEF4_3 v1 v2 v3 v4 v /\ &0 <= COEF4_4 v1 v2 v3 v4 v) /\ (v IN conv0 {v1, v2, v3, v4} <=> &0 < COEF4_1 v1 v2 v3 v4 v /\ &0 < COEF4_2 v1 v2 v3 v4 v /\ &0 < COEF4_3 v1 v2 v3 v4 v /\ &0 < COEF4_4 v1 v2 v3 v4 v) `, NHANH (SPEC_ALL COEFS_4) THEN REWRITE_TAC[CONVEX_HULL_4_EQUIV; CONV0_4POINTS; IN_ELIM_THM] THEN MESON_TAC[]);; let LEMMA78 = ZRFMKPY;; (* APRIL WORKS *) (* =========== *) (* NGUYEN QUANG TRUONG *) let IMP_TAC = IMP_IMP_TAC;; let QUAANG_TRUOONN = prove(` ! v0 v1 v2 v3 (v4:real^N). CARD {v0, v1, v2, v3, v4} = 5 /\ (?x. ~(x = v0) /\ x IN cone v0 {v1, v3} INTER cone v0 {v2, v4}) ==> ~(conv {v1, v3} INTER cone v0 {v2, v4} = {})`, REWRITE_TAC[CONV_SET2; cone; CARD5; SET_RULE ` a INTER b = {} <=> ~ (? x. a x /\ b x ) `; GSYM aff_ge_def; IN; IN_INTER] THEN NHANH (SET_RULE ` ~{v1, v2, v3, v4} v0 ==> ~ ( v0 = v1 \/ v0 = v3 ) /\ ~ ( v0 = v2 \/ v0 = v4 ) `) THEN ONCE_REWRITE_TAC[MESON[]` a /\ b ==> c <=> a ==> b ==> c `] THEN SIMP_TAC[AFF_GE_12] THEN REWRITE_TAC[DE_MORGAN_THM] THEN REWRITE_TAC[IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN UNDISCH_TAC ` (x:real^N) = tv % v0 + ta % v1 + tb % v3` THEN UNDISCH_TAC ` (x:real^N) = tv' % v0 + ta' % v2 + tb' % v4` THEN REWRITE_TAC[MESON[]` x = a ==> x = (b:real^N) ==> c <=> x = a /\ a = b ==> c `] THEN REWRITE_TAC[VECTOR_ARITH` a % v + d = b % v + e <=> ( a - b ) % v + d = e `] THEN ASM_CASES_TAC ` &0 < ta + tb ` THENL [DOWN_TAC THEN REWRITE_TAC[MESON[VECTOR_MUL_LCANCEL; REAL_FIELD ` &0 < a ==> ~ ( &1 / a = &0 )`]` &0 < ta + tb /\ aaa /\ aa = ta % v1 + tb % v3 <=> &0 < ta + tb /\ aaa /\ &1 / ( ta + tb ) % aa = &1 / ( ta + tb ) % ( ta % v1 + tb % v3) `] THEN REWRITE_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC; REAL_ARITH ` &1 / a * b = b / a `] THEN STRIP_TAC THEN DOWN_TAC THEN NHANH (MESON[REAL_LE_RDIV_0]`&0 <= ta /\ &0 <= tb /\ a1 /\ &0 <= ta' /\ &0 <= tb' /\ a2 /\ &0 < ta + tb /\ a3 ==> &0 <= ta / (ta + tb) /\ &0 <= tb / (ta + tb) /\ &0 <= ta' / (ta + tb) /\ &0 <= tb' / (ta + tb) `) THEN ASM_MESON_TAC[ REAL_FIELD` tv + ta + tb = &1 /\ tv' + ta' + tb' = &1 /\ &0 < ta + tb ==> (tv' - tv) / (ta + tb) + ta' / (ta + tb) + tb' / (ta + tb) = &1 /\ ta / ( ta + tb ) + tb / ( ta + tb ) = &1`]; DOWN_TAC THEN NHANH (MESON[REAL_ARITH` &0 <= a /\ &0 <= b /\ ~( &0 < a + b ) ==> a = &0 /\ b = &0 `]`&0 <= ta /\ &0 <= tb /\a1/\a2 /\a3/\a4 /\ ~(&0 < ta + tb) /\ a5 ==> ta = &0 /\ tb = &0`) THEN PURE_ONCE_REWRITE_TAC[MESON[]` P ta tb /\ ta = &0 /\ tb = &0 <=> P ( &0 ) ( &0 ) /\ ta = &0 /\ tb = &0 `] THEN REWRITE_TAC[ZERO_NEUTRAL; VECTOR_MUL_LZERO; VECTOR_ADD_LID] THEN REWRITE_TAC[VECTOR_ARITH` (tv' - tv) % v + a = vec 0 <=> tv' % v + a = tv % v `; MESON[]` a = b /\ b = c <=> a = c /\ b = c `] THEN MESON_TAC[VECTOR_ARITH ` &1 % v = v `]]);; (* le 80. p 51 *) (* ================ *) let JVDAFRS = prove(` ! v0 v1 v2 v3 (v4:real^N). CARD {v0, v1, v2, v3, v4} = 5 /\ (?x. ~(x = v0) /\ x IN cone v0 {v1, v3} INTER cone v0 {v2, v4}) ==> ~(conv {v1, v3} INTER cone v0 {v2, v4} = {} /\ conv {v2, v4} INTER cone v0 {v1, v3} = {})`, MESON_TAC[QUAANG_TRUOONN]);; (* LEMMA 22 *) (* =========================== *) let SQRT8_POS = MESON[REAL_ARITH ` &0 < &8 `; SQRT_POS_LT]` &0 < sqrt (&8) `;; let SQRT8_LT_4_45 = prove(` sqrt8 < #4.45 `, SIMP_TAC[sqrt8; REAL_ARITH ` &0 < #4.45 `; MESON[REAL_ARITH ` &0 < &8 `; SQRT_POS_LT]` &0 < sqrt (&8) `; LT_POW2_EQ_LT; SQRT8_POW2] THEN REAL_ARITH_TAC);; let PROVE_NOT_COLLINEAR = prove(` ! v0 v1 (v2:real^3). &2 <= dist3 v0 v1 /\ dist3 v0 v1 <= #2.51 /\ #2.45 <= dist3 v1 v2 /\ dist3 v1 v2 <= #2.51 /\ #2.77 <= dist3 v0 v2 /\ dist3 v0 v2 <= sqrt8 ==> ~ collinear {v0, v1, v2}`, REWRITE_TAC[COLLINEAR_AS_IN_CONV2; MID_COND; dist3; LENGTH_EQ_EX; DE_MORGAN_THM] THEN SIMP_TAC[DIST_SYM] THEN REPEAT GEN_TAC THEN ABBREV_TAC ` a = dist(v0,v1:real^3)` THEN ABBREV_TAC ` b = dist(v0,v2:real^3)` THEN ABBREV_TAC ` c = dist(v1,v2:real^3)` THEN MP_TAC SQRT8_LT_4_45 THEN REAL_ARITH_TAC);; let BPOW8APOW2CPOW2 = prove(`&2 <= a /\ a <= #2.51 /\ #2.45 <= c /\ c <= #2.51 /\ #2.77 <= b /\ b <= sqrt8 ==> b pow 2 <= &8 /\ a pow 2 <= #2.51 pow 2 /\ c pow 2 <= #2.51 pow 2 `, REWRITE_TAC[MESON[]` a1 /\ a2 /\a3 /\a4 /\a5 /\a6 ==> l <=> a1 /\a3 /\a5 ==> a2 /\a4 /\a6 ==> l `] THEN NHANH (REAL_ARITH`&2 <= a /\ #2.45 <= c /\ #2.77 <= b ==> &0 < a /\ &0 < b /\ &0 < c /\ &0 < #2.51 `) THEN SIMP_TAC[sqrt8; POW2_COND_LT; SQRT8_POS; SQRT8_POW2]);; let IMP_PRE_LE_19 = prove(`&2 <= a /\ a <= #2.51 /\ #2.45 <= c /\ c <= #2.51 /\ #2.77 <= b /\ b <= sqrt8 ==> &0 < &2 /\ &2 <= a /\ &0 < #2.77 /\ #2.77 <= b /\ &0 < #2.45 /\ #2.45 <= c /\ a pow 2 <= #2.77 pow 2 + #2.45 pow 2 /\ b pow 2 <= &2 pow 2 + #2.45 pow 2 /\ c pow 2 <= &2 pow 2 + #2.77 pow 2 `, CONV_TAC REAL_RAT_REDUCE_CONV THEN NHANH (BPOW8APOW2CPOW2 ) THEN REAL_ARITH_TAC);; (* ==================== *) let LT_SQ8_IMP_LT2 = prove_by_refinement( ` a < sqrt (&8) ==> ~ ( &2 <= &1 / &2 * a ) `, (* {{{ proof *) [ (ASM_CASES_TAC ` &0 <= a `); (UNDISCH_TAC `&0 <= a `); (SIMP_TAC[REAL_LT_IMP_LE; SQRT8_POS; LT_POW2_COND; REAL_ARITH ` &2 <= &1 / &2 * a <=> &4 <= a `; REAL_ARITH` &0 <= &4 `; POW2_COND; SQRT8_POW2]); BY((REAL_ARITH_TAC)); (FIRST_X_ASSUM MP_TAC); BY((REAL_ARITH_TAC)) ]);; (* }}} *) (* let condC = new_definition ` condC M13 m12 m14 M24 m34 (m23:real) = ((! x. x IN {M13, m12, m14, M24, m34, m23 } ==> &0 <= x ) /\ M13 <= m12 + m23 /\ M13 <= m14 + m34 /\ M24 < m12 + m14 /\ M24 < m23 + m34 /\ &0 <= delta (M13 pow 2) (m12 pow 2) (m14 pow 2) (M24 pow 2) (m34 pow 2 ) (m23 pow 2 ) )`;; let LE_FOR_LEMMA36 = prove(`(CARD {u, v, w} = 3 /\ packing {u, v, w} /\ dist (u,v) < sqrt8) /\ ~(dist (u,v) / &2 < dist (w,&1 / &2 % (u + v))) ==> condC (sqrt (&8)) (&2) (&2) (sqrt (&8)) (&2) (&2) /\ CARD {u, w, v, u + v - w} = 4 /\ &2 <= dist3 u w /\ &2 <= dist3 w v /\ &2 <= dist3 v (u + v - w) /\ &2 <= dist3 u (u + v - w) /\ dist3 u v < sqrt (&8) /\ dist3 w (u + v - w) <= sqrt (&8) `, REWRITE_TAC[condC; delta; SQRT8_POW2] THEN REWRITE_TAC[SET_RULE ` (! x. x IN ( a INSERT b ) ==> p x ) <=> p a /\ (! x. x IN b ==> p x ) `; NOT_IN_EMPTY] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN SIMP_TAC[SQRT8_POS; REAL_LT_IMP_LE; dist3; sqrt8; packing] THEN SIMP_TAC[REAL_LT_IMP_LE; SQRT8_POS; LT_POW2_COND; REAL_ARITH ` &0 <= &4 `; POW2_COND; SQRT8_POW2] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN REWRITE_TAC[NORM_ARITH` dist (v,u + v - w) = dist (u,w) /\ dist (u,u + v - w) = dist (v,w) /\ dist (w,u + v - w) = &2 * dist (w,&1 / &2 % (u + v)) `] THEN STRIP_TAC THEN CONJ_TAC THENL [ UNDISCH_TAC `CARD {(u:real^3), v, w} = 3` THEN REWRITE_TAC[CARD3; CARD4; IN_SET3] THEN REWRITE_TAC[DE_MORGAN_THM] THEN DAO THEN STRIP_TAC THEN CONJ_TAC THENL [ NHANH (NORM_ARITH`u + v - w = w ==> dist (w,u) = &1 / &2 * dist (u,v) `) THEN UNDISCH_TAC `dist ((u:real^3),v) < sqrt (&8)` THEN NHANH (LT_SQ8_IMP_LT2 ) THEN DOWN_TAC THEN SET_TAC[]; REWRITE_TAC[VECTOR_ARITH ` ((v:real^N) = u + v - w <=> u = w )`; VECTOR_ARITH ` ((u:real^N) = u + v - w <=> v = w ) `] THEN ASM_MESON_TAC[]]; DAO THEN CONJ_TAC THENL [REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC;DOWN_TAC THEN REWRITE_TAC[CARD3] THEN SET_TAC[]]]);; *) let MIDDLE_POINT_IN_CONV2 = prove(` &1 / &2 % ( u + v ) IN conv {u,v} `, REWRITE_TAC[CONV_SET2; IN_ELIM_THM; VECTOR_ADD_LDISTRIB] THEN MESON_TAC[REAL_ARITH ` &0 <= &1 / &2 `; REAL_ARITH` &1 / &2 + &1 / &2 = &1 `]);; let INTER_DISJONT_EX = SET_RULE ` ( a INTER b = {} ) <=> (! x. ~ (x IN a /\ x IN b )) `;; (* LEMMA36 *) (* ================== *) MATCH_MP (SPEC_ALL AFFINE_HULL_FINITE) (MESON[FINITE_RULES] ` FINITE {(a:real^N),b,c} `) ;; let PLANE_IMP_AFFINE = prove(`plane (p:real^N -> bool ) ==> affine p `, MESON_TAC[plane; AFFINE_AFFINE_HULL]);; let PLANE_IMP_AFFINE = prove(` plane (p:real^N -> bool ) ==> affine p `, REWRITE_TAC[plane; AFFINE_HULL_3; affine; FUN_EQ_THM; IN_ELIM_THM] THEN STRIP_TAC THEN ASM_SIMP_TAC[IN] THEN REPEAT STRIP_TAC THEN ASM_SIMP_TAC[] THEN SIMP_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC] THEN REWRITE_TAC[VECTOR_ARITH` (( a:real^N) + b + c ) + a' + b' + c' = ( a + a' ) + ( b + b') + c + c' `] THEN EXISTS_TAC ` u' * u'' + v' * u''' ` THEN EXISTS_TAC ` (u' * v'' + v' * v''')` THEN EXISTS_TAC ` (u' * w' + v' * w'')` THEN ASM_SIMP_TAC[prove(` u' + v' = &1 /\ u''' + v''' + w'' = &1 /\ u'' + v'' + w' = &1 ==> (u' * u'' + v' * u''') + (u' * v'' + v' * v''') + u' * w' + v' * w'' = &1 `, SIMP_TAC[REAL_ARITH` a + b = &1 <=> a = &1 - b `] THEN REAL_ARITH_TAC); GSYM VECTOR_ADD_RDISTRIB]);; let IMP_AFFINE_HULL_SUBSET = prove(` FINITE a /\ a SUBSET s /\ ~( a = {} )/\ affine s ==> ( affine hull a ) SUBSET s `, SIMP_TAC[AFFINE_HULL_FINITE; SUBSET; IN_ELIM_THM] THEN REWRITE_TAC[ GSYM SUBSET] THEN MESON_TAC[AFFINE]);; let SET_EQ_EX = SET_RULE `a = b <=> (! x. x IN a <=> x IN b ) `;; let SET_EQ_TO_SUBSET = SET_RULE ` a = b <=> a SUBSET b /\ b SUBSET a `;; let OTHORGONAL_QUATER_FOR = prove(` delta x12 ( x12 + x23 ) ( x12 + x24 ) x23 x24 x34 = x12 * ups_x x23 x24 x34 `, REWRITE_TAC[delta; ups_x] THEN REAL_ARITH_TAC);; let ORTHOGONAL_CROSS_PRODUCT = prove(` u dot ( u cross v ) = &0 /\ v dot ( u cross v ) = &0 `, REWRITE_TAC[cross; triple_of_real3; real3_of_triple; mk_vec3] THEN LET_TR THEN REWRITE_TAC[DOT_3; VECTOR_3] THEN REAL_ARITH_TAC);; let PITHAGOR_CROSS = prove(` dist (a + (b - a) cross (c - a),b) pow 2 = dist (b,a) pow 2 + norm ( (b - a) cross (c - a) ) pow 2 `, REWRITE_TAC[vector_norm; dist] THEN SIMP_TAC[DOT_POS_LE; SQRT_WORKS] THEN REWRITE_TAC[VECTOR_ARITH` ((a:real^N) + b) - c = b - (c - a ) `] THEN ABBREV_TAC ` ab = ( b - (a:real^3)) ` THEN ABBREV_TAC ` ac = ( c - (a:real^3)) ` THEN REWRITE_TAC[DOT_LSUB; DOT_RSUB] THEN SIMP_TAC[ORTHOGONAL_CROSS_PRODUCT; DOT_SYM] THEN REAL_ARITH_TAC);; let PITHAGOR_NORM = prove(` a dot b = &0 ==> dist (a,b) pow 2 = norm a pow 2 + norm b pow 2 `, SIMP_TAC[dist; vector_norm; DOT_POS_LE; SQRT_WORKS] THEN SIMP_TAC[DOT_LSUB; DOT_RSUB; DOT_SYM] THEN REAL_ARITH_TAC);; let VEC3_EQ_EX= prove(`! a (b:real^3). a = b <=> a$1 = b$1 /\ a$2 = b$2 /\ a$3 = b$3 `, SIMP_TAC[CART_EQ; DIMINDEX_3] THEN REWRITE_TAC[ARITH_RULE`1 <= i /\ i <= 3 <=> i = 1 \/ i = 2 \/ i = 3 `] THEN MESON_TAC[]);; let CROSS_CONVERT = prove_by_refinement( ` (b - a) cross (c - d) = (a - b) cross (d - c )`, (* {{{ proof *) [ (REWRITE_TAC[cross; triple_of_real3; real3_of_triple; mk_vec3]); (LET_TR); (REWRITE_TAC[lemma_cm3 ]); (REWRITE_TAC[VEC3_EQ_EX]); (REWRITE_TAC[VEC3_EQ_EX; VECTOR_3]); BY((REAL_ARITH_TAC)) ]);; (* }}} *) let lemma1 = MESON[prove(` dist(b,c) pow 2 = (a - c - (a - b)) dot (a - c - (a - b)) `, SIMP_TAC[dist; vector_norm; DOT_POS_LE; SQRT_WORKS] THEN MESON_TAC[VECTOR_ARITH ` b - (c:real^N) = (a - c) - ( a - b) `])]` ups_x aa bb (dist (b,c) pow 2 ) = ups_x aa bb (( a - c - (a - b)) dot (a - c - (a - b))) `;; let NORM_CROSS_PRODUCT_UPS_X = prove_by_refinement( `&4 * norm ( (b - a) cross (c - a)) pow 2 = ups_x (dist (a,b) pow 2) (dist (a,c) pow 2) (dist (b,c) pow 2)`, (* {{{ proof *) [ (REWRITE_TAC[lemma1 ]); (ONCE_REWRITE_TAC[CROSS_CONVERT]); (SIMP_TAC[ups_x;DIST_SYM; dist; vector_norm; DOT_POS_LE; SQRT_WORKS]); (REWRITE_TAC[cross; triple_of_real3; real3_of_triple; mk_vec3]); (LET_TR); (REWRITE_TAC[DOT_3; VECTOR_3]); (ABBREV_TAC ` ab = a - (b:real^3) `); (ABBREV_TAC ` cc = a - (c:real^3) `); BY((REWRITE_TAC[lemma_cm3 ] THEN REAL_ARITH_TAC)) ]);; (* }}} *) let lemma1 = prove( ` dist ( a cross b, a ) pow 2 = norm ( a cross b) pow 2 + norm a pow 2 /\dist ( a cross b, b ) pow 2 = norm ( a cross b) pow 2 + norm b pow 2 `, SIMP_TAC[DOT_SYM;ORTHOGONAL_CROSS_PRODUCT ; PITHAGOR_NORM; DIST_SYM] );; let NOT_COLLINEAR_IMP_CROSS_NOT_COPLANAR = prove_by_refinement( ` ! u v (w:real^3). ~ collinear {a,b,c} ==> ~ coplanar_alt { a + (b - a ) cross ( c - a ),a,b,c} `, (* {{{ proof *) [ (MP_TAC POLFLZY); (LET_TR); (SIMP_TAC[]); (DISCH_TAC); (REWRITE_TAC[NORM_ARITH` dist (a + b ,a) = norm (b ) `]); (REWRITE_TAC[NORM_ARITH`dist (a + c,b) = dist ( c, b - a ) `]); (SIMP_TAC[lemma1]); (REWRITE_TAC[GSYM dist]); (SIMP_TAC[DIST_SYM; OTHORGONAL_QUATER_FOR]); (ONCE_REWRITE_TAC[REAL_ARITH` a * b = &0 <=> ( &4 * a ) * b = &0 `]); (SIMP_TAC[NORM_CROSS_PRODUCT_UPS_X]); (REWRITE_TAC[REAL_ENTIRE]); BY((MESON_TAC[FHFMKIY])) ]);; (* }}} *) let ORTHOGONAL_IMP_PITHAGOR = prove(` (x:real^N) dot ((a:real^N) - b) = &0 ==> dist (a + x,b) pow 2 = norm x pow 2 + dist (a,b) pow 2`, SIMP_TAC[dist; vector_norm; DOT_POS_LE; SQRT_WORKS] THEN REWRITE_TAC[VECTOR_ARITH` (a + c) - b = c + a - (b:real^N)`] THEN ABBREV_TAC ` aa = ( a - (b:real^N)) ` THEN SIMP_TAC[DOT_LADD; DOT_RADD; DOT_SYM; ZERO_NEUTRAL]);; let NOT_COL_AND_ORTHO_IMP_NOT_COPL = prove(`! a b c (x:real^3). ~collinear {a, b, c} /\ x dot (a - b) = &0 /\ x dot (a - c) = &0 /\ ~(x = vec 0) ==> ~coplanar_alt {a + x, a, b, c}`, MP_TAC POLFLZY THEN LET_TR THEN SIMP_TAC[] THEN SIMP_TAC[ORTHOGONAL_IMP_PITHAGOR ] THEN SIMP_TAC[ORTHOGONAL_IMP_PITHAGOR; NORM_ARITH ` dist (a + x,a) = norm x `] THEN SIMP_TAC[ORTHOGONAL_IMP_PITHAGOR; NORM_ARITH ` dist (a + x,a) = norm x `; OTHORGONAL_QUATER_FOR] THEN SIMP_TAC[COL_EQ_UPS_0] THEN SIMP_TAC[COL_EQ_UPS_0; GSYM NORM_POS_LT; REAL_ENTIRE; MESON[RELATE_POW2]` a pow 2 = &0 <=> a = &0 `; REAL_ARITH ` &0 < a ==> ~( a = &0 ) `]);; let PLANE_NORM_IMP_AFFINE = prove(`! p. plane_norm p ==> affine p `, REWRITE_TAC[plane_norm; affine] THEN GEN_TAC THEN STRIP_TAC THEN ASM_SIMP_TAC[IN_ELIM_THM; MESON[]` a = &1 <=> &1 = a `] THEN ONCE_REWRITE_TAC[ VECTOR_ARITH ` ( a + b ) - c = ( a + b ) - &1 % c `] THEN ASM_SIMP_TAC[ VECTOR_ARITH` (u % x + v % y) - (u + v) % v0 = u % ( x - v0 ) + v % ( y - v0 ) `; DOT_RADD; DOT_RMUL; ZERO_NEUTRAL]);; let IN_PLANE_IMP_OTHORGONAL = prove(` n dot (x - v0) = &0 /\ n dot (y - v0) = &0 /\ n dot (z - v0) = &0 ==> n dot ( x - y ) = &0 /\ n dot ( x - z ) = &0 `, SIMP_TAC[DOT_RSUB] THEN REAL_ARITH_TAC);; let IMP_A1_EQ_0 = prove_by_refinement( `(n:real^N) dot (x - v0) = &0 /\ n dot (y - v0) = &0 /\ n dot (z - v0) = &0 /\ ~(n = vec 0) /\ x' = a1 % (x + n) + a2 % x + a3 % y + a4 % z /\ a1 + a2 + a3 + a4 = &1 /\ n dot (x' - v0) = &0 ==> a1 = &0`, (* {{{ proof *) [ (STRIP_TAC); (UNDISCH_TAC ` (n:real^N) dot (x' - v0) = &0`); (ASM_SIMP_TAC[VECTOR_ARITH`(a1 % x + y ) - v0 = a1 % ( x - v0 ) + y - v0 + a1 % v0 `]); (ONCE_REWRITE_TAC[ VECTOR_ARITH` a % x - y = a % ( x - y ) + a % y - y `]); (ASM_SIMP_TAC[DOT_RADD; VECTOR_ARITH` ( a + b ) - (c:real^N) = b + a - c `; DOT_RMUL; ZERO_NEUTRAL]); (ASM_SIMP_TAC[DOT_RADD; VECTOR_ARITH` ( a + b ) - (c:real^N) = b + a - c `; DOT_RMUL; ZERO_NEUTRAL; DOT_RSUB;REAL_ARITH` ((a4 * (n dot v0) - n dot v0 + a3 * (n dot v0)) + a2 * (n dot v0)) + a1 * (n dot v0) = ( a1 + a2 + a3 + a4 ) * ( n dot v0 ) - n dot v0 `; REAL_ARITH ` &1 * a - a = &0 `]); BY((ASM_MESON_TAC[REAL_ENTIRE; GSYM DOT_EQ_0])) ]);; (* }}} *) let LEMMA7 = prove(` !x y z (p:real^3 -> bool). plane_norm p /\ ~collinear {x, y, z} /\ {x, y, z} SUBSET p ==> p = aff {x, y, z}`, NHANH (PLANE_IMP_AFFINE) THEN REPEAT STRIP_TAC THEN REWRITE_TAC[aff; SET_EQ_TO_SUBSET] THEN CONJ_TAC THENL [ UNDISCH_TAC ` plane_norm (p:real^3 -> bool ) ` THEN REWRITE_TAC[plane_norm] THEN STRIP_TAC THEN UNDISCH_TAC ` {(x:real^3), y, z} SUBSET p` THEN ASM_SIMP_TAC[SET3_SUBSET; IN_ELIM_THM] THEN NHANH (IN_PLANE_IMP_OTHORGONAL ) THEN DOWN_TAC THEN NHANH (MESON[NOT_COL_AND_ORTHO_IMP_NOT_COPL]` ~collinear {(x:real^3), y, z} /\ ~(n = vec 0) /\a1 /\a2 /\a4 /\a3/\ n dot (x - y) = &0 /\ n dot (x - z) = &0 ==> ~coplanar_alt { x + n ,x,y,z} `) THEN REWRITE_TAC[SUBSET; IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN UNDISCH_TAC `~coplanar_alt {x + n, x, y, (z:real^3)} ` THEN NHANH (SPEC `x' :real^3` (GEN `v :real^3` ( SPEC_ALL COEFS_4 ))) THEN ABBREV_TAC ` a1 = COEF4_1 (x + n) x y z x'` THEN ABBREV_TAC ` a2 = COEF4_2 (x + n) x y z x'` THEN ABBREV_TAC ` a3 = COEF4_3 (x + n) x y z x'` THEN ABBREV_TAC ` a4 = COEF4_4 (x + n) x y z x'` THEN STRIP_TAC THEN DOWN_TAC THEN REWRITE_TAC[AFFINE_HULL_3; IN_ELIM_THM] THEN NHANH (MESON[IMP_A1_EQ_0]` ~(n = vec 0) /\ aa1 /\ n dot (x - v0) = &0 /\ n dot (y - v0) = &0 /\ n dot (z - v0) = &0 /\ aa2 /\aa3 /\ n dot (x' - v0) = &0 /\aa4/\aa5 /\aa6/\aa7/\ ~coplanar_alt {x + n, x, y, z} /\ a1 + a2 + a3 + a4 = &1 /\ x' = a1 % (x + n) + a2 % x + a3 % y + a4 % z /\ l ==> a1 = &0 `) THEN PURE_ONCE_REWRITE_TAC[MESON[]` P a1 /\ a1 = &0 <=> P (&0) /\ a1 = &0 `] THEN REWRITE_TAC[ZERO_NEUTRAL; VECTOR_ARITH` &0 % x + y = y `] THEN MESON_TAC[]; ASM_MESON_TAC[PLANE_NORM_IMP_AFFINE ; FINITE_RULES; SET_RULE` ~({(x:real^N), y, z} = {} )`; IMP_AFFINE_HULL_SUBSET]]);; let SMWTDMU = LEMMA7;; let DET_VEC3_AS_CROSS_DOT = prove_by_refinement( ` det_vec3 v1 v2 v3 = ( v1 cross v2 ) dot v3 `, (* {{{ proof *) [ (REWRITE_TAC[det_vec3; cross; triple_of_real3; real3_of_triple; mk_vec3; DOT_3; VECTOR_3]); (LET_TR); (REWRITE_TAC[det_vec3; cross; triple_of_real3; real3_of_triple; mk_vec3; DOT_3; VECTOR_3]); BY((REAL_ARITH_TAC)) ]);; (* }}} *) let COL_EQ_NORM_CROSS = prove_by_refinement( ` ! v1 v2 (v3:real^3). collinear {v1,v2,v3} <=> norm ( (v2 - v1) cross (v3 - v1)) pow 2 = &0 `, (* {{{ proof *) [ (REWRITE_TAC[COL_EQ_UPS_0]); (REWRITE_TAC[GSYM NORM_CROSS_PRODUCT_UPS_X]); BY((REAL_ARITH_TAC)) ]);; (* }}} *) let COLLINEAR_IMP_COPLANAR = prove(` ! v1 v2 v3 v3 (v:real^3). collinear {v1,v2,v3} ==> coplanar_alt {v1,v2,v3,v} `, REWRITE_TAC[COPLANAR_DET_VEC3_EQ_0; COL_EQ_NORM_CROSS; DET_VEC3_AS_CROSS_DOT ] THEN REWRITE_TAC[GSYM RELATE_POW2; NORM_EQ_0] THEN REPEAT GEN_TAC THEN SIMP_TAC[VECTOR_ARITH ` vec 0 dot x = &0 `]);; (* MAY WORKS, LEMMA 85 ; VBVYGGT *) let POS_EQ_NOT_COPLANANR = prove(` &0 < delta (dist ((x1:real^3),x2) pow 2) (dist (x1,x3) pow 2) (dist (x1,x4) pow 2) (dist (x2,x3) pow 2) (dist (x2,x4) pow 2) (dist (x3,x4) pow 2) <=> ~coplanar_alt {x1, x2, x3, x4} `, MP_TAC (DELTA_POS_4POINTS) THEN MP_TAC POLFLZY THEN LET_TR THEN REWRITE_TAC[REAL_ARITH` a <= b <=> a = b \/ a < b `] THEN MESON_TAC[REAL_ARITH` ~( a = b /\ a < b ) `]);; let SUM_CHI_EQ_2DELTA = prove(` let chi11 = chi x12 x13 x14 x23 x24 x34 in let chi22 = chi x12 x24 x23 x14 x13 x34 in let chi33 = chi x34 x13 x23 x14 x24 x12 in let chi44 = chi x34 x24 x14 x23 x13 x12 in &2 * delta x12 x13 x14 x23 x24 x34 = chi11 + chi22 + chi33 + chi44`, LET_TR THEN REWRITE_TAC[chi; delta] THEN REAL_ARITH_TAC);; let NOT_0_IMP_SUM_CHI_1 = prove(`~(delta x12 x13 x14 x23 x24 x34 = &0) ==> chi x12 x13 x14 x23 x24 x34 / (&2 * delta x12 x13 x14 x23 x24 x34) + chi x12 x24 x23 x14 x13 x34 / (&2 * delta x12 x13 x14 x23 x24 x34) + chi x34 x13 x23 x14 x24 x12 / (&2 * delta x12 x13 x14 x23 x24 x34) + chi x34 x24 x14 x23 x13 x12 / (&2 * delta x12 x13 x14 x23 x24 x34) = &1`, MP_TAC SUM_CHI_EQ_2DELTA THEN LET_TR THEN CONV_TAC REAL_FIELD);; (* MAY WORKS *) let PROVE_DIST_FROM_V1 = prove(` ~coplanar_alt {v1, v2, v3, v4} ==> let x12 = dist (v1,v2) pow 2 in let x13 = dist (v1,v3) pow 2 in let x14 = dist (v1,v4) pow 2 in let x23 = dist (v2,v3) pow 2 in let x24 = dist (v2,v4) pow 2 in let x34 = dist (v3,v4) pow 2 in let chi11 = chi x12 x13 x14 x23 x24 x34 in let chi22 = chi x12 x24 x23 x14 x13 x34 in let chi33 = chi x34 x13 x23 x14 x24 x12 in let chi44 = chi x34 x24 x14 x23 x13 x12 in p = &1 / (&2 * delta x12 x13 x14 x23 x24 x34) % (chi11 % v1 + chi22 % v2 + chi33 % v3 + chi44 % v4) ==> dist3 p v1 pow 2 = ( &1 / &2 ) * rho_ij' x12 x13 x14 x23 x24 x34 / (&2 * delta x12 x13 x14 x23 x24 x34) `, REWRITE_TAC[ GSYM POS_EQ_NOT_COPLANANR] THEN NHANH (REAL_ARITH` a < b ==> ~( b = a ) `) THEN NHANH NOT_0_IMP_SUM_CHI_1 THEN LET_TR THEN REWRITE_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC; REAL_ARITH` ( &1 / a ) * b = b / a `] THEN ABBREV_TAC ` a1 = chi (dist (v1,v2) pow 2) (dist (v1,v3) pow 2) (dist (v1,v4) pow 2) (dist (v2,v3) pow 2) (dist (v2,v4) pow 2) (dist (v3,v4) pow 2) / (&2 * delta (dist (v1,v2) pow 2) (dist (v1,v3) pow 2) (dist (v1,v4) pow 2) (dist (v2,v3) pow 2) (dist (v2,v4) pow 2) (dist (v3,(v4:real^3)) pow 2))` THEN ABBREV_TAC ` a2 = chi (dist (v1,v2) pow 2) (dist (v2,v4) pow 2) (dist (v2,v3) pow 2) (dist (v1,v4) pow 2) (dist (v1,v3) pow 2) (dist (v3,v4) pow 2) / (&2 * delta (dist (v1,v2) pow 2) (dist (v1,v3) pow 2) (dist (v1,v4) pow 2) (dist (v2,v3) pow 2) (dist (v2,v4) pow 2) (dist (v3,(v4:real^3)) pow 2)) ` THEN REWRITE_TAC[ GSYM dist3] THEN ABBREV_TAC ` a3 = chi (dist3 v3 v4 pow 2) (dist3 v1 v3 pow 2) (dist3 v2 v3 pow 2) (dist3 v1 v4 pow 2) (dist3 v2 v4 pow 2) (dist3 v1 v2 pow 2) / (&2 * delta (dist3 v1 v2 pow 2) (dist3 v1 v3 pow 2) (dist3 v1 v4 pow 2) (dist3 v2 v3 pow 2) (dist3 v2 v4 pow 2) (dist3 v3 v4 pow 2)) ` THEN ABBREV_TAC ` a4 = chi (dist3 v3 v4 pow 2) (dist3 v2 v4 pow 2) (dist3 v1 v4 pow 2) (dist3 v2 v3 pow 2) (dist3 v1 v3 pow 2) (dist3 v1 v2 pow 2) / (&2 * delta (dist3 v1 v2 pow 2) (dist3 v1 v3 pow 2) (dist3 v1 v4 pow 2) (dist3 v2 v3 pow 2) (dist3 v2 v4 pow 2) (dist3 v3 v4 pow 2)) ` THEN SIMP_TAC[REAL_ARITH` a + b = &1 <=> a = &1 - b `] THEN REPEAT STRIP_TAC THEN REWRITE_TAC[dist3; dist; NORM_POW_2; VECTOR_ARITH` (((&1 - (a2 + a3 + a4)) % v1 + a2 % v2 + a3 % v3 + a4 % v4) - v1) = a2 % ( v2 - v1 ) + a3 % (v3 - v1 ) + a4 % ( v4 - v1 ) `; VECTOR_ARITH` ( a + b ) dot ( a + b ) = a dot a + &2 * ( a dot b ) + b dot b `] THEN REWRITE_TAC[DOT_RADD; DOT_LMUL; DOT_RMUL] THEN REWRITE_TAC[X_DOT_X_EQ] THEN REWRITE_TAC[DOT_NORM_NEG; VECTOR_ARITH` v2 - v1 - (v4 - v1) = (v2:real^N) - v4 `] THEN SIMP_TAC[GSYM dist; DIST_SYM; GSYM dist3; D3_SYM] THEN EXPAND_TAC "a2" THEN EXPAND_TAC "a3" THEN EXPAND_TAC "a4" THEN REWRITE_TAC[GSYM dist3 ] THEN ABBREV_TAC ` x12 = dist3 v1 v2 pow 2 ` THEN ABBREV_TAC ` x13 = dist3 v1 v3 pow 2 ` THEN ABBREV_TAC ` x14 = dist3 v1 v4 pow 2 ` THEN ABBREV_TAC ` x23 = dist3 v2 v3 pow 2 ` THEN ABBREV_TAC ` x24 = dist3 v2 v4 pow 2 ` THEN ABBREV_TAC ` x34 = dist3 v3 v4 pow 2 ` THEN UNDISCH_TAC ` &0 < delta x12 x13 x14 x23 x24 x34 ` THEN ONCE_REWRITE_TAC[REAL_FIELD` &0 < a ==> b = c <=> &0 < a ==> b * ( &2 * a) pow 2 = c * ( &2 * a ) pow 2 `] THEN ONCE_REWRITE_TAC[REAL_ARITH` &0 < a <=> &0 < &2 * a `] THEN SIMP_TAC[REAL_FIELD` &0 < b ==> ( a / b ) * b pow 2 = a * b `; REAL_RDISTRIB; REAL_FIELD` &0 < b ==> ( a / b ) * ( aa / b ) * c * b pow 2 = a * aa * c `; REAL_ADD_LDISTRIB] THEN SIMP_TAC[REAL_LDISTRIB; REAL_ARITH` (a*b)*c = a *b * c `; REAL_FIELD` &0 < b ==> ( a / b ) * ( a / b ) * c * b pow 2 = a pow 2 * c `; REAL_ARITH` &2 * a * b * c / &2 * d = a * b * d * c `] THEN SIMP_TAC[REAL_FIELD` &0 < a ==> ( b / a ) * ( bb / a ) * a pow 2 * d = b * bb * d `] THEN SIMP_TAC[REAL_FIELD` &0 < a ==> b / a / &2 * a pow 2 = a * b / &2 `] THEN REWRITE_TAC[chi; rho_ij'; delta] THEN REAL_ARITH_TAC);; let PROVE_EQ_DIST_FROM4 = prove(` ~coplanar_alt {v1, v2, v3, v4} ==> let x12 = dist (v1,v2) pow 2 in let x13 = dist (v1,v3) pow 2 in let x14 = dist (v1,v4) pow 2 in let x23 = dist (v2,v3) pow 2 in let x24 = dist (v2,v4) pow 2 in let x34 = dist (v3,v4) pow 2 in let chi11 = chi x12 x13 x14 x23 x24 x34 in let chi22 = chi x12 x24 x23 x14 x13 x34 in let chi33 = chi x34 x13 x23 x14 x24 x12 in let chi44 = chi x34 x24 x14 x23 x13 x12 in p = &1 / (&2 * delta x12 x13 x14 x23 x24 x34) % (chi11 % v1 + chi22 % v2 + chi33 % v3 + chi44 % v4) ==> dist3 p v2 pow 2 = ( &1 / &2 ) * rho_ij' x12 x13 x14 x23 x24 x34 / (&2 * delta x12 x13 x14 x23 x24 x34) /\ dist3 p v3 pow 2 = ( &1 / &2 ) * rho_ij' x12 x13 x14 x23 x24 x34 / (&2 * delta x12 x13 x14 x23 x24 x34) /\ dist3 p v4 pow 2 = ( &1 / &2 ) * rho_ij' x12 x13 x14 x23 x24 x34 / (&2 * delta x12 x13 x14 x23 x24 x34) `, REWRITE_TAC[ GSYM POS_EQ_NOT_COPLANANR] THEN NHANH (REAL_ARITH` a < b ==> ~( b = a ) `) THEN NHANH NOT_0_IMP_SUM_CHI_1 THEN LET_TR THEN REWRITE_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC; REAL_ARITH` ( &1 / a ) * b = b / a `] THEN ABBREV_TAC ` a1 = chi (dist (v1,v2) pow 2) (dist (v1,v3) pow 2) (dist (v1,v4) pow 2) (dist (v2,v3) pow 2) (dist (v2,v4) pow 2) (dist (v3,v4) pow 2) / (&2 * delta (dist (v1,v2) pow 2) (dist (v1,v3) pow 2) (dist (v1,v4) pow 2) (dist (v2,v3) pow 2) (dist (v2,v4) pow 2) (dist (v3,(v4:real^3)) pow 2))` THEN ABBREV_TAC ` a2 = chi (dist (v1,v2) pow 2) (dist (v2,v4) pow 2) (dist (v2,v3) pow 2) (dist (v1,v4) pow 2) (dist (v1,v3) pow 2) (dist (v3,v4) pow 2) / (&2 * delta (dist (v1,v2) pow 2) (dist (v1,v3) pow 2) (dist (v1,v4) pow 2) (dist (v2,v3) pow 2) (dist (v2,v4) pow 2) (dist (v3,(v4:real^3)) pow 2)) ` THEN REWRITE_TAC[ GSYM dist3] THEN ABBREV_TAC ` a3 = chi (dist3 v3 v4 pow 2) (dist3 v1 v3 pow 2) (dist3 v2 v3 pow 2) (dist3 v1 v4 pow 2) (dist3 v2 v4 pow 2) (dist3 v1 v2 pow 2) / (&2 * delta (dist3 v1 v2 pow 2) (dist3 v1 v3 pow 2) (dist3 v1 v4 pow 2) (dist3 v2 v3 pow 2) (dist3 v2 v4 pow 2) (dist3 v3 v4 pow 2)) ` THEN ABBREV_TAC ` a4 = chi (dist3 v3 v4 pow 2) (dist3 v2 v4 pow 2) (dist3 v1 v4 pow 2) (dist3 v2 v3 pow 2) (dist3 v1 v3 pow 2) (dist3 v1 v2 pow 2) / (&2 * delta (dist3 v1 v2 pow 2) (dist3 v1 v3 pow 2) (dist3 v1 v4 pow 2) (dist3 v2 v3 pow 2) (dist3 v2 v4 pow 2) (dist3 v3 v4 pow 2)) ` THEN ONCE_REWRITE_TAC[MESON[VECTOR_ARITH` &1 % x = x `]` dist3 a b pow 2 = aa <=> dist3 a ( &1 % b ) pow 2 = aa `] THEN ONCE_REWRITE_TAC[MESON[]` a = &1 <=> &1 = a `] THEN SIMP_TAC[] THEN STRIP_TAC THEN STRIP_TAC THEN REWRITE_TAC[dist3; dist] THEN REWRITE_TAC[VECTOR_ARITH` (a1 % v1 + a2 % v2 + a3 % v3 + a4 % v4) - (a1 + a2 + a3 + a4) % v2 = a1 % ( v1 - v2 ) + a3 % ( v3 - v2 ) + a4 % (v4 - v2 ) `; VECTOR_ARITH` (a1 % v1 + a2 % v2 + a3 % v3 + a4 % v4) - (a1 + a2 + a3 + a4) % v3 = a1 % ( v1 - v3 ) + a2 % ( v2 - v3 ) + a4 % (v4 - v3 )`; VECTOR_ARITH` (a1 % v1 + a2 % v2 + a3 % v3 + a4 % v4) - (a1 + a2 + a3 + a4) % v4 = a1 % ( v1 - v4 ) + a2 % ( v2 - v4 ) + a3 % (v3 - v4 )`] THEN REWRITE_TAC[NORM_POW_2] THEN REWRITE_TAC[DOT_LADD; DOT_RADD; DOT_LMUL; DOT_RMUL; GSYM NORM_POW_2] THEN REWRITE_TAC[DOT_NORM_NEG; VECTOR_ARITH` v3 - v4 - (v2 - v4) = (v3:real^N) - v2 `; GSYM dist; GSYM dist3 ] THEN EXPAND_TAC "a1" THEN EXPAND_TAC "a2" THEN EXPAND_TAC "a3" THEN EXPAND_TAC "a4" THEN REWRITE_TAC[GSYM dist3 ] THEN REWRITE_TAC[prove(` dist3 (v4 - v3) (v1 - v3) = dist3 v1 v4 `, REWRITE_TAC[dist3] THEN CONV_TAC NORM_ARITH)] THEN SIMP_TAC[D3_SYM] THEN ABBREV_TAC ` x12 = dist3 v1 v2 pow 2 ` THEN ABBREV_TAC ` x13 = dist3 v1 v3 pow 2 ` THEN ABBREV_TAC ` x14 = dist3 v1 v4 pow 2 ` THEN ABBREV_TAC ` x23 = dist3 v2 v3 pow 2 ` THEN ABBREV_TAC ` x24 = dist3 v2 v4 pow 2 ` THEN ABBREV_TAC ` x34 = dist3 v3 v4 pow 2 ` THEN UNDISCH_TAC ` &0 < delta x12 x13 x14 x23 x24 x34 ` THEN ONCE_REWRITE_TAC[REAL_FIELD` &0 < a ==> ( b = c ) /\ ( bb = cc ) /\ ( bbb = ccc ) <=> &0 < a ==> ( b * ( &2 * a) pow 2 = c * ( &2 * a ) pow 2 ) /\ ( bb * ( &2 * a) pow 2 = cc * ( &2 * a ) pow 2 ) /\ ( bbb * ( &2 * a) pow 2 = ccc * ( &2 * a ) pow 2 ) `] THEN ONCE_REWRITE_TAC[REAL_ARITH` &0 < a <=> &0 < &2 * a `] THEN SIMP_TAC[REAL_FIELD` &0 < b ==> ( a / b ) * b pow 2 = a * b `; REAL_RDISTRIB; REAL_FIELD` &0 < b ==> ( a / b ) * ( aa / b ) * c * b pow 2 = a * aa * c `; REAL_ADD_LDISTRIB] THEN SIMP_TAC[REAL_LDISTRIB; REAL_ARITH` (a*b)*c = a *b * c `; REAL_FIELD` &0 < b ==> ( a / b ) * ( a / b ) * c * b pow 2 = a pow 2 * c `; REAL_ARITH` &2 * a * b * c / &2 * d = a * b * d * c `] THEN SIMP_TAC[REAL_FIELD` &0 < a ==> ( b / a ) * ( bb / a ) * a pow 2 * d = b * bb * d `] THEN SIMP_TAC[REAL_FIELD` &0 < a ==> b / a / &2 * a pow 2 = a * b / &2 `] THEN SIMP_TAC[REAL_FIELD` &0 < b ==> ( a / b ) * b pow 2 = a * b `; REAL_RDISTRIB; REAL_FIELD` &0 < b ==> ( a / b ) * ( aa / b ) * c * b pow 2 = a * aa * c `; REAL_ADD_LDISTRIB] THEN SIMP_TAC[REAL_LDISTRIB; REAL_ARITH` (a*b)*c = a *b * c `; REAL_FIELD` &0 < b ==> ( a / b ) * ( a / b ) * c * b pow 2 = a pow 2 * c `; REAL_ARITH` &2 * a * b * c / &2 * d = a * b * d * c `] THEN SIMP_TAC[REAL_FIELD` &0 < a ==> ( b / a ) * ( bb / a ) * a pow 2 * d = b * bb * d `] THEN SIMP_TAC[REAL_FIELD` &0 < a ==> b / a / &2 * a pow 2 = a * b / &2 `] THEN DISCH_TAC THEN REWRITE_TAC[chi; rho_ij'; delta] THEN REAL_ARITH_TAC);; let AFFINE_HULL_3 = prove (`affine hull {a,b,c} = { u % a + v % b + w % c | u + v + w = &1}`, SIMP_TAC[AFFINE_HULL_FINITE; FINITE_INSERT; FINITE_RULES] THEN SIMP_TAC[AFFINE_HULL_FINITE_STEP; FINITE_INSERT; FINITE_RULES] THEN REWRITE_TAC[REAL_ARITH `x - y = z:real <=> x = y + z`; VECTOR_ARITH `x - y = z:real^N <=> x = y + z`] THEN REWRITE_TAC[VECTOR_ADD_RID; REAL_ADD_RID] THEN SET_TAC[]);; let AFFINE_HULL_4 = prove (`affine hull {a,b,c,d} = { u % a + v % b + w % c + z % d | u + v + w + z = &1}`, SIMP_TAC[AFFINE_HULL_FINITE; FINITE_INSERT; FINITE_RULES] THEN SIMP_TAC[AFFINE_HULL_FINITE_STEP; FINITE_INSERT; FINITE_RULES] THEN REWRITE_TAC[REAL_ARITH `x - y = z:real <=> x = y + z`; VECTOR_ARITH `x - y = z:real^N <=> x = y + z`] THEN REWRITE_TAC[VECTOR_ADD_RID; REAL_ADD_RID] THEN SET_TAC[]);; let PROVE_EXISTS_CIR_OF_FOUR_POINTS = prove(`!(v1:real^3) v2 v3 v4. CARD {v1, v2, v3, v4} = 4 /\ ~coplanar_alt {v1, v2, v3, v4} ==> (? p. p IN affine hull {v1, v2, v3, v4} /\ (?r. !v. v IN {v1, v2, v3, v4} ==> r = dist (p, v))) `, NHANH (REWRITE_RULE[RIGHT_FORALL_IMP_THM] (GEN `p:real^3` PROVE_DIST_FROM_V1)) THEN NHANH (REWRITE_RULE[RIGHT_FORALL_IMP_THM] (GEN `p:real^3` PROVE_EQ_DIST_FROM4 )) THEN REPEAT GEN_TAC THEN REPEAT LET_TAC THEN ABBREV_TAC `rr = &1 / &2 * rho_ij' x12 x13 x14 x23 x24 x34 / (&2 * delta x12 x13 x14 x23 x24 x34) ` THEN REWRITE_TAC[GSYM POS_EQ_NOT_COPLANANR] THEN NHANH (SPEC_ALL REAL_POS_NZ) THEN ASM_SIMP_TAC[] THEN NHANH (NOT_0_IMP_SUM_CHI_1 ) THEN ASM_SIMP_TAC[] THEN REWRITE_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC; REAL_ARITH ` &1 / a * b = b / a `] THEN REWRITE_TAC[FORALL_IN_CLAUSES; MESON[]`(? r. (r:real) = a /\ r = b /\ r = c /\ r = d ) <=> a = b /\ a = c /\ a = d `] THEN REWRITE_TAC[MESON[]` (! x. x = a ==> P a ) <=> P a `] THEN DISCH_TAC THEN EXISTS_TAC ` chi11 / (&2 * delta x12 x13 x14 x23 x24 x34) % (v1:real^3) + chi22 / (&2 * delta x12 x13 x14 x23 x24 x34) % v2 + chi33 / (&2 * delta x12 x13 x14 x23 x24 x34) % v3 + chi44 / (&2 * delta x12 x13 x14 x23 x24 x34) % v4 ` THEN CONJ_TAC THENL [REWRITE_TAC[AFFINE_HULL_4; IN_ELIM_THM] THEN FIRST_X_ASSUM MP_TAC THEN MESON_TAC[NOT_0_IMP_SUM_CHI_1 ]; FIRST_X_ASSUM MP_TAC THEN SIMP_TAC[dist3; DIST_POS_LE; EQ_POW2_COND]]);; let IMP_PROPERTIES_OF_CIR4 = prove(`!(v1:real^3) v2 v3 v4. CARD {v1, v2, v3, v4} = 4 /\ ~coplanar_alt {v1, v2, v3, v4} ==> circumcenter {v1, v2, v3, v4} IN affine hull {v1, v2, v3, v4} /\ (?r. !v. v IN {v1, v2, v3, v4} ==> r = dist (circumcenter {v1, v2, v3, v4},v))`, NHANH (SPEC_ALL PROVE_EXISTS_CIR_OF_FOUR_POINTS ) THEN REWRITE_TAC[circumcenter; IN] THEN MESON_TAC[EXISTS_THM]);; let DIST_EQ_IMP_ORTHOGONAL = prove(` dist (pp,v2) = dist (pp,v1) /\ dist (p,v2) = dist (p,v1) ==> (pp - p ) dot (v2 - v1 ) = &0 `, REWRITE_TAC[MONG7_ROI; DOT_LSUB] THEN REAL_ARITH_TAC);; let IMP_OTHO4 = prove(` n dot (v2 - v1) = &0 /\ n dot (v3 - v1) = &0 /\ n dot (v4 - v1) = &0 /\ x IN affine hull {v1,v2,v3,v4} /\ y IN affine hull {v1,v2,v3,v4} ==> n dot (x - y ) = &0 `, REWRITE_TAC[AFFINE_HULL_4; IN_ELIM_THM] THEN STRIP_TAC THEN DOWN_TAC THEN IMP_TAC THEN SIMP_TAC[REAL_ARITH`a + b = c <=> a = c - b `] THEN PHA THEN REWRITE_TAC[VECTOR_ARITH` ((&1 - (v' + w' + z')) % v1 + v' % v2 + w' % v3 + z' % v4) - ((&1 - (v + w + z)) % v1 + v % v2 + w % v3 + z % v4) = ( v' - v ) % ( v2 - v1 ) + ( w' - w ) % ( v3 - v1 ) + ( z' - z ) % ( v4 - v1 ) `] THEN SIMP_TAC[DOT_RADD; DOT_RMUL; ZERO_NEUTRAL]);; let UNIQUE_EXISISTING_PROPERTY_C4 = prove(`!(v1:real^3) v2 v3 v4. CARD {v1, v2, v3, v4} = 4 /\ ~coplanar_alt {v1, v2, v3, v4} ==> (!p. p IN affine hull {v1, v2, v3, v4} /\ (?r. !v. v IN {v1, v2, v3, v4} ==> r = dist (p,v)) ==> p = circumcenter {v1, v2, v3, v4}) `, NHANH (SPEC_ALL IMP_PROPERTIES_OF_CIR4 ) THEN REPEAT GEN_TAC THEN ABBREV_TAC ` pp = circumcenter {(v1:real^3), v2, v3, v4}` THEN REPEAT STRIP_TAC THEN DOWN_TAC THEN REWRITE_TAC[FORALL_IN_CLAUSES] THEN REWRITE_TAC[MESON[]` r = a /\ r = b /\ r = c /\ r = d <=> r = a /\ b = a /\ c = a /\ d = a `] THEN PHA THEN NHANH (MESON[DIST_EQ_IMP_ORTHOGONAL ]`dist (pp,v2) = dist (pp,v1) /\ dist (pp,v3) = dist (pp,v1) /\ dist (pp,v4) = dist (pp,v1) /\a11/\a2/\ dist (p,v2) = dist (p,v1) /\ dist (p,v3) = dist (p,v1) /\ dist (p,v4) = dist (p,v1) ==> ( p - pp) dot ( v2 - v1 ) = &0 /\ ( p - pp ) dot ( v3 - v1 ) = &0 /\ ( p - pp ) dot ( v4 - v1 ) = &0 `) THEN ONCE_REWRITE_TAC[GSYM VECTOR_SUB_EQ] THEN REWRITE_TAC[GSYM DOT_EQ_0] THEN MESON_TAC[IMP_OTHO4 ]);; let PROVE_IN_AFFINE_HULL_4 = prove( `~(delta x12 x13 x14 x23 x24 x34 = &0) ==> &1 / (&2 * delta x12 x13 x14 x23 x24 x34) % (chi x12 x13 x14 x23 x24 x34 % v1 + chi x12 x24 x23 x14 x13 x34 % v2 + chi x34 x13 x23 x14 x24 x12 % v3 + chi x34 x24 x14 x23 x13 x12 % v4) IN affine hull {(v1:real^3), v2, v3, v4}`, REWRITE_TAC[AFFINE_HULL_4; IN_ELIM_THM; VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC; REAL_ARITH ` ( &1 / a ) * b = b/a `] THEN MESON_TAC[NOT_0_IMP_SUM_CHI_1]);; (* VBVYGGT , le 85 *) MESON[POW_2_SQRT; DIST_POS_LE]` dist (x,y) pow 2 = r ==> dist (x,y) = sqrt ( r ) `;; (* LEMMA 85 *) let VBVYGGT = prove(`!(v1:real^3) v2 v3 v4. CARD {v1, v2, v3, v4} = 4 /\ ~coplanar_alt {v1, v2, v3, v4} ==> circumcenter {v1, v2, v3, v4} IN affine hull {v1, v2, v3, v4} /\ (?r. !v. v IN {v1, v2, v3, v4} ==> r = dist (circumcenter {v1, v2, v3, v4},v)) /\ (!p. p IN affine hull {v1, v2, v3, v4} /\ (?r. !v. v IN {v1, v2, v3, v4} ==> r = dist (p,v)) ==> p = circumcenter {v1, v2, v3, v4}) /\ (let x12 = dist (v1,v2) pow 2 in let x13 = dist (v1,v3) pow 2 in let x14 = dist (v1,v4) pow 2 in let x23 = dist (v2,v3) pow 2 in let x24 = dist (v2,v4) pow 2 in let x34 = dist (v3,v4) pow 2 in let chi11 = chi x12 x13 x14 x23 x24 x34 in let chi22 = chi x12 x24 x23 x14 x13 x34 in let chi33 = chi x34 x13 x23 x14 x24 x12 in let chi44 = chi x34 x24 x14 x23 x13 x12 in circumcenter {v1, v2, v3, v4} = &1 / (&2 * delta x12 x13 x14 x23 x24 x34) % (chi11 % v1 + chi22 % v2 + chi33 % v3 + chi44 % v4)) `, NHANH (SPEC_ALL UNIQUE_EXISISTING_PROPERTY_C4 ) THEN NHANH (SPEC_ALL IMP_PROPERTIES_OF_CIR4 ) THEN REWRITE_TAC[MESON[]` (a /\ b1/\b2) /\ b ==> b1 /\b2/\ b/\ d <=> a /\ b1 /\b2/\b==>d `] THEN NHANH (REWRITE_RULE[RIGHT_FORALL_IMP_THM] ( GEN `p: real^3 `PROVE_DIST_FROM_V1)) THEN NHANH (REWRITE_RULE[RIGHT_FORALL_IMP_THM] ( GEN `p: real^3 ` PROVE_EQ_DIST_FROM4)) THEN REPEAT GEN_TAC THEN REPEAT LET_TAC THEN ABBREV_TAC `rr = &1 / &2 * rho_ij' x12 x13 x14 x23 x24 x34 / (&2 * delta x12 x13 x14 x23 x24 x34) ` THEN REWRITE_TAC[MESON[]` (! x. x = a ==> P x ) <=> P a `] THEN REWRITE_TAC[GSYM POS_EQ_NOT_COPLANANR] THEN NHANH (REAL_ARITH` &0 < a ==> ~( a = &0 )`) THEN NHANH (PROVE_IN_AFFINE_HULL_4 ) THEN UNDISCH_TAC ` dist ((v1:real^3),v2) pow 2 = x12` THEN UNDISCH_TAC ` dist ((v1:real^3),v3) pow 2 = x13` THEN UNDISCH_TAC ` dist ((v1:real^3),v4) pow 2 = x14` THEN UNDISCH_TAC ` dist ((v2:real^3),v3) pow 2 = x23` THEN UNDISCH_TAC ` dist ((v2:real^3),v4) pow 2 = x24` THEN UNDISCH_TAC ` dist ((v3:real^3),v4) pow 2 = x34` THEN UNDISCH_TAC ` chi x12 x13 x14 x23 x24 x34 = chi11 ` THEN UNDISCH_TAC ` chi x12 x24 x23 x14 x13 x34 = chi22 ` THEN UNDISCH_TAC ` chi x34 x13 x23 x14 x24 x12 = chi33` THEN UNDISCH_TAC ` chi x34 x24 x14 x23 x13 x12 = chi44` THEN REWRITE_TAC[MESON[]` a = b ==> P a <=> a = b ==> P b `] THEN ABBREV_TAC ` w = &1 / (&2 * delta x12 x13 x14 x23 x24 x34) % (chi11 % (v1:real^3) + chi22 % v2 + chi33 % v3 + chi44 % v4)` THEN REWRITE_TAC[MESON[]` a /\ b ==> c <=> a ==> b ==> c `] THEN REPLICATE_TAC 13 DISCH_TAC THEN REWRITE_TAC[FORALL_IN_CLAUSES;dist3] THEN PHA THEN NHANH (MESON[POW_2_SQRT; DIST_POS_LE]` dist (x,y) pow 2 = r ==> dist (x,y) = sqrt ( r ) `) THEN MESON_TAC[]);; let NOT_COPLANAR_IMP_EXISTS_CIR = prove(`! (v1:real^3) v2 v3 v4. CARD {v1, v2, v3, v4} = 4 /\ ~coplanar_alt {v1, v2, v3, v4} ==> circumcenter {v1, v2, v3, v4} IN affine hull {v1, v2, v3, v4} /\ (?r. !v. v IN {v1, v2, v3, v4} ==> r = dist (circumcenter {v1, v2, v3, v4},v)) `, MESON_TAC[VBVYGGT]);; let THREE_POINTS_COP = prove(` ! v1 v2 (v3:real^3). coplanar_alt {v1,v2,v3} `, MESON_TAC[DIMINDEX_3; ARITH_RULE` 2 <= 3 `; COPLANAR_3]);; let PER_SET4 = SET_RULE ` {a,b,c,d} = {b,a,c,d} /\ {a,b,c,d} = {c,b,a,d} /\ {a,b,c,d} = {d,b,c,a} `;; let NOT_COPLANAR_IMP_CARD4 = prove(` ~ coplanar_alt {(v1:real^3), v2, v3, v4} ==> CARD {v1, v2, v3, v4} = 4 `, REWRITE_TAC[CARD4; IN_SET3] THEN MP_TAC (GEN_ALL THREE_POINTS_COP ) THEN MESON_TAC[PER_SET4; SET_RULE` {a,a,b,c} = {a,b,c} `]);; let NOT_COPLANAR_IMP_EXISTS_CIR2 = MESON[NOT_COPLANAR_IMP_EXISTS_CIR ; NOT_COPLANAR_IMP_CARD4 ]` ! (v1:real^3) v2 v3 v4. ~ coplanar_alt {v1, v2, v3, v4} ==> circumcenter {v1, v2, v3, v4} IN affine hull {v1, v2, v3, v4} /\ (?r. !v. v IN {v1, v2, v3, v4} ==> r = dist (circumcenter {v1, v2, v3, v4},v)) `;; let NOT_COPLANAR_IMP_RADV_PROPERTIES = prove(` ~coplanar_alt {(v1:real^3), v2, v3, v4} ==> (! w. {v1, v2, v3, v4} w ==> radV {v1, v2, v3, v4} = dist (circumcenter {v1,v2,v3,v4} ,w) ) `, NHANH (SPEC_ALL NOT_COPLANAR_IMP_EXISTS_CIR2) THEN REWRITE_TAC[IN; radV] THEN MESON_TAC[EXISTS_THM]);; let ZJEWPAP = ` ! v1 v2 v3 (v4:real^3). let s = {v1, v2, v3, v4} in CARD s = 4 /\ ~ coplanar_alt s ==> radV {v1,v2,v3} <= radV s `;; let PHA = REWRITE_TAC[MESON[]` ( a ==> b ==> c <=> a /\ b ==> c ) /\ ( (a /\ b ) /\ c <=> a /\ b /\ c ) `];; let NOT_COL_EQ_UPS_X_POS = prove(`! v1 v2 v3. ~ collinear {(v1:real^3), v2, v3} <=> &0 < ups_x (dist (v1,v2) pow 2) (dist (v1,v3) pow 2) (dist (v2,v3) pow 2) `, MP_TAC (GEN_ALL ZERO_LE_UPS_X) THEN REWRITE_TAC[UPS_X_EQ_ZERO_COND] THEN REWRITE_TAC[UPS_X_EQ_ZERO_COND; REAL_ARITH` a <= b <=> a = b \/ a < b `] THEN REWRITE_TAC[dist3] THEN MESON_TAC[REAL_ARITH` ~( a = b /\ a < b ) `]);; let ETA_Y_POW2_EQ = prove(`(dist (v1,v2) pow 2 * dist (v1,v3) pow 2 * dist (v2,v3) pow 2) / ups_x (dist (v1,v2) pow 2) (dist (v1,v3) pow 2) (dist (v2,v3) pow 2) = ( eta_y (dist3 v2 v3) (dist3 v1 v3) (dist3 v1 v2)) pow 2 `, REWRITE_TAC[eta_y;dist3; eta_x] THEN LET_TR THEN REWRITE_TAC[GSYM REAL_POW_2; GSYM dist3 ] THEN SIMP_TAC[MESON[UPS_X_SYM]` ups_x a b c = ups_x c b a `; REAL_ARITH ` a * b * c = c * b * a `] THEN MESON_TAC[SQRT_WORKS; REAL_LE_SQUARE_POW; REAL_LE_MUL; REAL_LE_DIV; dist3 ; ZERO_LE_UPS_X; UPS_X_SYM]);; let ETA_Y_POS_LE = prove(` &0 <= eta_y (dist3 v1 v2) (dist3 v1 v3) (dist3 v2 v3) `, REWRITE_TAC[eta_y; eta_x] THEN LET_TR THEN REWRITE_TAC[GSYM REAL_POW_2] THEN MESON_TAC[REAL_LE_POW_2; REAL_LE_MUL; ZERO_LE_UPS_X; REAL_LE_DIV; SQRT_POS_LE]);; (* lemma 87 *) let ZJEWPAP = prove(` ! v1 v2 v3 (v4:real^3). let s = {v1, v2, v3, v4} in CARD s = 4 /\ ~ coplanar_alt s ==> radV {v1,v2,v3} <= radV s `, LET_TR THEN NHANH (MESON[COLLINEAR_IMP_COPLANAR ]`~coplanar_alt {v1, v2, v3, v4} ==> ~ collinear {(v1:real^3),v2,v3} `) THEN SIMP_TAC[NOT_COLL_IMP_RADV_EQ_ETA_Y] THEN REWRITE_TAC[MESON[]` a /\ b /\ c <=> (a/\b)/\c`] THEN NHANH (SPEC_ALL VBVYGGT) THEN REPEAT GEN_TAC THEN NHANH (NOT_COPLANAR_IMP_RADV_PROPERTIES) THEN ABBREV_TAC ` pp = circumcenter {(v1:real^3), v2, v3, v4}` THEN MP_TAC (SPECL [`pp :real^3`; ` v1: real^3`; `v2:real^3`; ` v3:real^3`] DELTA_POS_4POINTS ) THEN REWRITE_TAC[REWRITE_RULE[IN] FORALL_IN_CLAUSES; FORALL_IN_CLAUSES ] THEN REWRITE_TAC[MESON[]` ( a ==> b ==> c <=> a /\ b ==> c ) /\ ( (a /\ b ) /\ c <=> a /\ b /\ c ) `] THEN REPEAT STRIP_TAC THEN UNDISCH_TAC ` &0 <= delta (dist ((pp:real^3),v1) pow 2) (dist (pp,v2) pow 2) (dist (pp,v3) pow 2) (dist (v1,v2) pow 2) (dist (v1,v3) pow 2) (dist (v2,v3) pow 2)` THEN ABBREV_TAC `p1 = dist ((pp:real^3),v1)` THEN ABBREV_TAC `p2 = dist ((pp:real^3),v2)` THEN ABBREV_TAC `p3 = dist ((pp:real^3),v3)` THEN REPLICATE_TAC 3 (FIRST_X_ASSUM MP_TAC THEN MATCH_MP_TAC (MESON[]` a ==> b ==> a `)) THEN EXPAND_TAC "p1" THEN EXPAND_TAC "p2" THEN EXPAND_TAC "p3" THEN FIRST_X_ASSUM MP_TAC THEN REWRITE_TAC[NOT_COL_EQ_UPS_X_POS ] THEN REWRITE_TAC[NOT_COL_EQ_UPS_X_POS; DELTA_RRR_INTERPRETE] THEN SIMP_TAC[REAL_FIELD` &0 < a ==> -- b * c + r * a = a * ( r - ( b * c ) / a ) `] THEN SIMP_TAC[ETA_Y_POW2_EQ; REAL_LE_MUL_EQ] THEN UNDISCH_TAC ` radV {(v1:real^3), v2, v3, v4} = p1 ` THEN SIMP_TAC[] THEN EXPAND_TAC "p1" THEN UNDISCH_TAC `r = dist ((pp: real^3),v4)` THEN SIMP_TAC[] THEN REPLICATE_TAC 3 REMOVE_TAC THEN SIMP_TAC[ETA_Y_SYYM; REAL_ARITH` &0 <= a - b <=> b <= a `] THEN MESON_TAC[DIST_POS_LE; POW2_COND; ETA_Y_POS_LE ]);; let NOT_EQ_BASIS_IMP_OTHORGANAL = MESON[DOT_BASIS_BASIS_UNEQUAL] ` ! i j. ~( i = j ) ==> basis i dot basis j = &0 `;; let BASIS_DIS_OTHORGONAL = MESON[ARITH_RULE` ~( 1 = 2 \/ 1 = 3 \/ 2 = 3 ) `; NOT_EQ_BASIS_IMP_OTHORGANAL] ` basis 1 dot basis 2 = &0 /\ basis 1 dot basis 3 = &0 /\ basis 2 dot basis 3 = &0 ` ;; let NORM_BASIS_VEC3 = prove(` ! i. i = 1 \/ i = 2 \/ i = 3 ==> norm (( basis i ):real^3 ) = &1 `, MESON_TAC[DIMINDEX_3; ARITH_RULE` i = 1 \/ i = 2 \/ i = 3 <=> 1 <= i /\ i <= 3`; NORM_BASIS]);; let AAA_LEMMA = prove(` &0 < a /\ a <= b /\ b <= c /\ ll ==> &0 <= b pow 2 - a pow 2 /\ &0 <= c pow 2 - b pow 2 `, REWRITE_TAC[REAL_ARITH` &0 <= a - b <=> b <= a `] THEN MESON_TAC[REAL_LT_IMP_LE; POW2_COND; POS_IMP_POW2; REAL_LE_TRANS]);; let LLEEMAA = prove(` &0 < a /\ a <= b /\ b <= c /\ &0 < a' /\ a' <= b' /\ b' <= c' /\ a <= a' /\ b <= b' /\ c <= c' /\ l ==> &0 <= a' pow 2 - a pow 2 /\ &0 <= b' pow 2 - b pow 2 /\ &0 <= c' pow 2 - c pow 2 `, REWRITE_TAC[REAL_ARITH` &0 <= a - b <=> b <= a `] THEN MESON_TAC[POS_IMP_POW2; REAL_ARITH` a < b ==> a <= b `; REAL_LE_TRANS]);; let TYUNJLA = prove(` !(e1:real^3) e2 e3 a b c a' b' c' t1 t2 t3. e1 = basis 1 /\ e2 = basis 2 /\ e3 = basis 3 /\ &0 < a /\ a <= b /\ b <= c /\ &0 < a' /\ a' <= b' /\ b' <= c' /\ a <= a' /\ b <= b' /\ c <= c' /\ (!x. x IN {t1, t2, t3} ==> &0 < x) /\ t1 + t2 + t3 < &1 /\ v = ((t1 + t2 + t3) * a) % e1 + ((t2 + t3) * sqrt (b pow 2 - a pow 2)) % e2 + (t3 * sqrt (c pow 2 - b pow 2)) % e3 /\ v' = ((t1 + t2 + t3) * a') % e1 + ((t2 + t3) * sqrt (b' pow 2 - a' pow 2)) % e2 + (t3 * sqrt (c' pow 2 - b' pow 2)) % e3 ==> norm v <= norm v' `, REPEAT STRIP_TAC THEN FIRST_X_ASSUM MP_TAC THEN FIRST_X_ASSUM MP_TAC THEN SIMP_TAC[POW2_COND; NORM_POS_LE; NORM_POW_2; DOT_LADD; DOT_RADD; DOT_LMUL; DOT_RMUL] THEN ASM_SIMP_TAC[] THEN SIMP_TAC[GSYM NORM_POW_2; NORM_BASIS_VEC3 ] THEN SIMP_TAC[BASIS_DIS_OTHORGONAL; MESON[DOT_SYM; BASIS_DIS_OTHORGONAL] ` basis 2 dot basis 1 = &0 /\ basis 3 dot basis 1 = &0 /\ basis 3 dot basis 2 = &0 `; ZERO_NEUTRAL] THEN REWRITE_TAC[REAL_ARITH` (a * x ) * ( b * x ) * c = a * b * c * x pow 2 `] THEN REPEAT STRIP_TAC THEN DOWN_TAC THEN NHANH (AAA_LEMMA) THEN PHA THEN NHANH (MESON[AAA_LEMMA]` &0 < a /\ a <= b /\ b <= c /\ aa <= a /\ l ==> &0 <= b pow 2 - a pow 2 /\ &0 <= c pow 2 - b pow 2 `) THEN SIMP_TAC[SQRT_WORKS] THEN ONCE_REWRITE_TAC[REAL_ARITH` a <= b <=> &0 <= b - a `] THEN REWRITE_TAC[REAL_ARITH` ((t1 + t2 + t3) * (t1 + t2 + t3) * &1 pow 2 * a' pow 2 + (t2 + t3) * (t2 + t3) * &1 pow 2 * (b' pow 2 - a' pow 2) + t3 * t3 * &1 pow 2 * (c' pow 2 - b' pow 2)) - ((t1 + t2 + t3) * (t1 + t2 + t3) * &1 pow 2 * a pow 2 + (t2 + t3) * (t2 + t3) * &1 pow 2 * (b pow 2 - a pow 2) + t3 * t3 * &1 pow 2 * (c pow 2 - b pow 2)) = t1 * ( t1 + &2 * t2 + &2 * t3 ) * ( a' pow 2 - a pow 2 ) + t2 * (t2 + &2 * t3 ) * ( b' pow 2 - b pow 2 ) + t3 pow 2 * ( c' pow 2 - c pow 2 ) `] THEN REWRITE_TAC[REAL_ARITH` &0 <= a - b <=> b <= a `] THEN PHA THEN NHANH (LLEEMAA) THEN STRIP_TAC THEN UNDISCH_TAC ` (!x. x IN {t1, t2, t3} ==> &0 < x)` THEN REPLICATE_TAC 3 ( FIRST_X_ASSUM MP_TAC) THEN REWRITE_TAC[FORALL_IN_CLAUSES] THEN PHA THEN NHANH (REAL_ARITH` &0 < t1 /\ &0 < t2 /\ &0 < t3 ==> &0 <= t1 /\ &0 <= t2 /\ &0 <= t1 + &2 * t2 + &2 * t3 /\ &0 <= t2 + &2 * t3 `) THEN MESON_TAC[REAL_LE_ADD; REAL_LE_MUL; REAL_LE_POW_2]);; let LEMMA83 = TYUNJLA ;; let DELTA_TRIPLE_SUB_H_EXPAND = prove(` delta (a01 - h) (a02 - h) (a03 - h) x12 x13 x23 = delta a01 a02 a03 x12 x13 x23 - h * ups_x x12 x13 x23 `, REWRITE_TAC[delta;ups_x] THEN REAL_ARITH_TAC);; let PROVE_EXISTS_H_DELTA_0 = prove(`&0 < ups_x x12 x13 x23 /\ &0 <= delta a01 a02 a03 x12 x13 x23 ==> (?h. &0 <= h /\ h = ( delta a01 a02 a03 x12 x13 x23 ) / ups_x x12 x13 x23 /\ delta (a01 - h) (a02 - h) (a03 - h) x12 x13 x23 = &0 )`, REWRITE_TAC[DELTA_TRIPLE_SUB_H_EXPAND] THEN DISCH_TAC THEN EXISTS_TAC`( delta a01 a02 a03 x12 x13 x23 ) / ups_x x12 x13 x23` THEN ASM_SIMP_TAC[REAL_LT_IMP_LE; REAL_LE_DIV] THEN FIRST_X_ASSUM MP_TAC THEN CONV_TAC REAL_FIELD);; let FIRST_POINT_IN_AFF3 = prove(` ! w v1 v2. w IN aff {w,v1,v2} `, REWRITE_TAC[aff; AFFINE_HULL_3; IN_ELIM_THM] THEN REPEAT GEN_TAC THEN EXISTS_TAC ` &1 ` THEN EXISTS_TAC `&0` THEN EXISTS_TAC `&0` THEN REWRITE_TAC[ZERO_NEUTRAL] THEN CONV_TAC VECTOR_ARITH);; let THREE_GEN_POINTS_IN_AFF3 = MESON[PER_SET3; FIRST_POINT_IN_AFF3 ]` a IN aff {a,b,c} /\ b IN aff {a,b,c} /\ c IN aff {a,b,c} `;; let PROVE_THE_HYPOTHESI_FOR_74 = prove(` (let s = {v1, v2, v3, v4} in CARD s = 4 /\ ~coplanar_alt s /\ eta_y (dist3 v1 v2 ) (dist3 v1 v3) (dist3 v2 v3) <= r ) ==> ( let x12 = dist3 v1 v2 pow 2 in let x13 = dist3 v1 v3 pow 2 in let x23 = dist3 v2 v3 pow 2 in CARD {v1, v2, v3, v4} = 4 /\ ~coplanar_alt {v1, v2, v3, v4} /\ &0 <= r pow 2 /\ &0 <= r pow 2 /\ &0 <= r pow 2 /\ delta (r pow 2) (r pow 2) (r pow 2) x12 x13 x23 >= &0 ) `, REPEAT LET_TAC THEN SIMP_TAC[REAL_LE_POW_2] THEN REWRITE_TAC[DELTA_RRR_INTERPRETE] THEN EXPAND_TAC "s" THEN NHANH (MESON[COLLINEAR_IMP_COPLANAR]` ~ coplanar_alt {v1, v2, v3, v} ==> ~ collinear {v1, v2, (v3:real^3)} `) THEN REWRITE_TAC[NOT_COL_EQ_UPS_X_POS] THEN EXPAND_TAC "x12" THEN EXPAND_TAC "x13" THEN EXPAND_TAC "x23" THEN REWRITE_TAC[dist3] THEN SIMP_TAC[REAL_FIELD` &0 < a ==> -- x * y + r * a = a * ( r - (x * y ) / a )`] THEN SIMP_TAC[ETA_Y_POW2_EQ;dist3; ETA_Y_SYYM] THEN MP_TAC ETA_Y_POS_LE THEN DAO THEN PHA THEN REWRITE_TAC[dist3] THEN DAO THEN NHANH (MESON[POS_IMP_POW2]` a <= b /\ &0 <= a ==> a pow 2 <= b pow 2 `) THEN ONCE_REWRITE_TAC[REAL_ARITH` a <= b <=> &0 <= b - a `] THEN REWRITE_TAC[REAL_ARITH` a >= &0 <=> &0 <= a `] THEN SIMP_TAC[REAL_LT_IMP_LE; REAL_LE_MUL]);; let INSERT_SUBSET = SET_RULE` {} SUBSET s /\ ( ( a INSERT s ) SUBSET ss <=> a IN ss /\ s SUBSET ss ) `;; let IMP_TAC = REWRITE_TAC[MESON[]` a /\ b ==> c <=> a ==> b ==> c `];; let IMP_OTHORGONAL_AFF3 = prove(`!v1 v2 v3 u. u dot (v1 - v2) = &0 /\ u dot (v1 - v3) = &0 ==> (!x y. {x, y} SUBSET aff {v1, v2, v3} ==> u dot (x - y) = &0)`, REWRITE_TAC[aff; AFFINE_HULL_3; INSERT_SUBSET; IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN DOWN_TAC THEN REWRITE_TAC[MESON[]` a /\ b ==> c <=> a ==> b ==> c `] THEN SIMP_TAC[REAL_ARITH` a + b = &1 <=> a = &1 - b `] THEN REWRITE_TAC[VECTOR_ARITH` ((&1 - (v + w)) % v1 + v % v2 + w % v3) - ((&1 - (v' + w')) % v1 + v' % v2 + w' % v3) = ( v' - v ) % ( v1 - v2 ) + ( w' - w ) % ( v1 - v3 ) `] THEN REPEAT STRIP_TAC THEN ASM_SIMP_TAC[DOT_RADD; DOT_RMUL; ZERO_NEUTRAL]);; (* MONG7_ROI *) let DIST_EQ_IMP_OTHORGONAL = prove(` ! a b p q. dist (p,a) = dist (p,b) /\ dist (q,a) = dist(q,b) ==> ( p - q ) dot ( a - b ) = &0 `, REWRITE_TAC[MONG7_ROI; DOT_LSUB] THEN REAL_ARITH_TAC);; let NOT_COPLANAR_IMP_NOT_COLLINEAR = MATCH_MP (MESON[]` (a ==> b) ==> ~ b ==> ~ a `) (SPEC_ALL COLLINEAR_IMP_COPLANAR);; (* lemma 89 *) let PVLJZLA = prove( `! (v1:real^3) v2 v3 v4. let s = {v1, v2, v3, v4} in ~coplanar_alt s ==> (circumcenter s IN conv0 s <=> orientation s v1 (\x. &0 < x) /\ orientation s v2 (\x. &0 < x) /\ orientation s v3 (\x. &0 < x) /\ orientation s v4 (\x. &0 < x))`, REWRITE_TAC[orientation; affsign] THEN REPEAT GEN_TAC THEN LET_TR THEN REWRITE_TAC[lin_combo] THEN REWRITE_TAC[SET_RULE` s DIFF {a} UNION {a} = s UNION {a} `; SET_RULE` {a,b,c,d} UNION {a} = {a,b,c,d} /\ {a,b,c,d} UNION {b} = {a,b,c,d} /\ {a,b,c,d} UNION {c} = {a,b,c,d} /\ {a,b,c,d} UNION {d} = {a,b,c,d}`] THEN REWRITE_TAC[MESON[]`a = b /\ c /\ d <=> c /\ d /\ b = a `] THEN REWRITE_TAC[SET_RULE` (!w. {v1} w ==> &0 < f w) /\ sum {v1, v2, v3, v4} f = &1 /\ l <=> (!w. w IN {v1,v2,v3,v4} ==> {v1} w ==> &0 < f w) /\ sum {v1, v2, v3, v4} f = &1 /\ l `; SET_RULE` (!w. {v2} w ==> &0 < f w) /\ sum {v1, v2, v3, v4} f = &1 /\ l <=> (!w. w IN {v1,v2,v3,v4} ==> {v2} w ==> &0 < f w) /\ sum {v1, v2, v3, v4} f = &1 /\ l `; SET_RULE` (!w. {v2} w ==> &0 < f w) /\ sum {v1, v2, v3, v4} f = &1 /\ l <=> (!w. w IN {v1,v2,v3,v4} ==> {v2} w ==> &0 < f w) /\ sum {v1, v2, v3, v4} f = &1 /\ l `; SET_RULE` (!w. {v3} w ==> &0 < f w) /\ sum {v1, v2, v3, v4} f = &1 /\ l <=> (!w. w IN {v1,v2,v3,v4} ==> {v3} w ==> &0 < f w) /\ sum {v1, v2, v3, v4} f = &1 /\ l `; SET_RULE` (!w. {v4} w ==> &0 < f w) /\ sum {v1, v2, v3, v4} f = &1 /\ l <=> (!w. w IN {v1,v2,v3,v4} ==> {v4} w ==> &0 < f w) /\ sum {v1, v2, v3, v4} f = &1 /\ l `] THEN SIMP_TAC[AFFINE_HULL_FINITE_STEP_GEN; REAL_ARITH `&0 < x /\ &0 < y ==> &0 < x + y`; REAL_ARITH ` &0 < x ==> &0 < x / &2`; FINITE_INSERT; CONJUNCT1 FINITE_RULES ; RIGHT_EXISTS_AND_THM] THEN NHANH (NOT_COPLANAR_IMP_CARD4) THEN SIMP_TAC[IN_ACT_SING; CARD4; IN_SET3; DE_MORGAN_THM] THEN REWRITE_TAC[REAL_ARITH` a - b = c <=> a = b + c `; ZERO_NEUTRAL; VECTOR_ARITH`(a:real^N) - b = c <=> a = b + c `; VECTOR_ARITH` x + vec 0 = x `] THEN REWRITE_TAC[CONV0_4; IN_ELIM_THM] THEN NHANH (SPEC ` circumcenter {(v1:real^3), v2, v3, v4} ` ( GEN `v:real^3` (SPEC_ALL COEFS_4))) THEN STRIP_TAC THEN EQ_TAC THENL [ MESON_TAC[]; UNDISCH_TAC ` !ta tb tc td. circumcenter {v1, v2, v3, v4} = ta % v1 + tb % v2 + tc % v3 + td % v4 /\ ta + tb + tc + td = &1 ==> ta = COEF4_1 v1 v2 v3 v4 (circumcenter {v1, v2, v3, v4}) /\ tb = COEF4_2 v1 v2 v3 v4 (circumcenter {v1, v2, v3, v4}) /\ tc = COEF4_3 v1 v2 v3 v4 (circumcenter {v1, v2, v3, v4}) /\ td = COEF4_4 v1 v2 v3 v4 (circumcenter {v1, v2, v3, v4})` THEN REWRITE_TAC[MESON[]`&0 < v /\ ( ? b . P v b ) <=> (? b. &0 < v /\ P v b ) `] THEN REWRITE_TAC[MESON[]` &1 = a /\ aa = b <=> a = &1 /\ b = aa `] THEN ABBREV_TAC ` (vv:real^3) = circumcenter {v1, v2, v3, v4} ` THEN ABBREV_TAC ` a1 = COEF4_1 v1 v2 v3 v4 vv ` THEN ABBREV_TAC ` a2 = COEF4_2 v1 v2 v3 v4 vv ` THEN ABBREV_TAC ` a3 = COEF4_3 v1 v2 v3 v4 vv ` THEN ABBREV_TAC ` a4 = COEF4_4 v1 v2 v3 v4 vv ` THEN PHA THEN IMP_TAC THEN STRIP_TAC THEN STRIP_TAC THEN REPLICATE_TAC 4 (FIRST_X_ASSUM MP_TAC) THEN PHA THEN NHANH (MESON[]`(!ta tb tc td. vv = ta % v1 + tb % v2 + tc % v3 + td % v4 /\ ta + tb + tc + td = &1 ==> ta = a1 /\ tb = a2 /\ tc = a3 /\ td = a4) /\ a111 /\ v + v' + v'' + v''' = &1 /\ v % v1 + v' % v2 + v'' % v3 + v''' % v4 = vv /\ (?v v' v'' v'''. &0 < v' /\ v + v' + v'' + v''' = &1 /\ v % v1 + v' % v2 + v'' % v3 + v''' % v4 = vv) /\ (?v v' v'' v'''. &0 < v'' /\ v + v' + v'' + v''' = &1 /\ v % v1 + v' % v2 + v'' % v3 + v''' % v4 = vv) /\ (?v v' v'' v'''. &0 < v''' /\ v + v' + v'' + v''' = &1 /\ v % v1 + v' % v2 + v'' % v3 + v''' % v4 = vv) ==> &0 < v' /\ &0 < v'' /\ &0 < v''' `) THEN MESON_TAC[]]);; let IMP_IN_AFF_LT = prove(`CARD {v1, v2, v3, v4} = 4 ==> ( (?v v' v'' v'''. v < &0 /\ &1 = v + v' + v'' + v''' /\ vv = v % v1 + v' % v2 + v'' % v3 + v''' % v4) <=> vv IN aff_lt {v2,v3,v4} {v1} ) `, REWRITE_TAC[CARD4; IN_SET3; DE_MORGAN_THM] THEN SIMP_TAC[AFF_GES_GTS; IN_ELIM_THM] THEN REMOVE_TAC THEN MESON_TAC[REAL_ARITH` a + b + c + d = d + a + b + c `; VECTOR_ARITH` a + b + c + d = d + a + b + (c:real^N)`]);; let SQRT4_EQ2 = prove(` sqrt ( &4 ) = &2 `, REWRITE_TAC[REAL_ARITH` &4 = &2 pow 2 `] THEN MESON_TAC[POW_2_SQRT; REAL_ARITH` &0 <= &2 `]);; let RHUFIIB = prove( ` !x12 x13 x14 x23 x24 x34. rho_ij' x12 x13 x14 x23 x24 x34 * ups_x x34 x24 x23 = chi x12 x13 x14 x23 x24 x34 pow 2 + &4 * delta x12 x13 x14 x23 x24 x34 * x34 * x24 * x23 `, REWRITE_TAC[rho_ij'; chi; delta; ups_x] THEN REAL_ARITH_TAC);; (* lemma 84 *) let SHOGYBS = prove(` ! x1 x2 x3 (x4:real^3). ~coplanar_alt {x1,x2,x3,x4} ==> let x12 = dist (x1,x2) pow 2 in let x13 = dist (x1,x3) pow 2 in let x14 = dist (x1,x4) pow 2 in let x23 = dist (x2,x3) pow 2 in let x24 = dist (x2,x4) pow 2 in let x34 = dist (x3,x4) pow 2 in &0 <= rho_ij' x12 x13 x14 x23 x24 x34 `, ONCE_REWRITE_TAC[SET_RULE` {v1,v2,v3,v4} = {v2,v3,v4,v1} `] THEN NHANH (NOT_COPLANAR_IMP_NOT_COLLINEAR) THEN ONCE_REWRITE_TAC[GSYM (SET_RULE` {v1,v2,v3,v4} = {v2,v3,v4,v1} `)] THEN REWRITE_TAC[NOT_COL_EQ_UPS_X_POS] THEN REPEAT GEN_TAC THEN MP_TAC (SPEC_ALL DELTA_POS_4POINTS) THEN REPEAT LET_TAC THEN MP_TAC (SPEC_ALL RHUFIIB) THEN DOWN_TAC THEN NHANH (MESON[REAL_LE_POW_2]` a pow 2 = b ==> &0 <= b `) THEN DAO THEN SIMP_TAC[UPS_X_SYM] THEN REWRITE_TAC[MESON[REAL_FIELD` &0 < a ==> (b * a = c <=> b = c / a )`]` &0 < a /\a1 /\a2/\ b * a = c /\l <=> &0 < a /\a1 /\a2/\ b = c / a /\ l `] THEN MP_TAC (REAL_ARITH` &0 <= &4 `) THEN PHA THEN NHANH (MESON[REAL_LT_IMP_LE; REAL_LE_DIV; REAL_LE_MUL; REAL_LE_ADD; REAL_LE_POW_2]` &0 <= &4 /\ &0 < ups_x x23 x24 x34 /\a1/\ &0 <= delta x12 x13 x14 x23 x24 x34 /\ a2 /\ &0 <= x34 /\a3 /\ &0 <= x24 /\a4 /\ &0 <= x23 /\a5/\ &0 <= x14 /\a6 /\ &0 <= x13 /\a7 /\a8 /\ &0 <= x12 ==> &0 <= &4 * delta x12 x13 x14 x23 x24 x34 * x34 * x24 * x23 `) THEN ABBREV_TAC ` aaa = &4 * delta x12 x13 x14 x23 x24 x34 * x34 * x24 * x23 ` THEN STRIP_TAC THEN FIRST_X_ASSUM MP_TAC THEN UNDISCH_TAC ` rho_ij' x12 x13 x14 x23 x24 x34 = (chi x12 x13 x14 x23 x24 x34 pow 2 + aaa) / ups_x x23 x24 x34 ` THEN UNDISCH_TAC`&0 < ups_x x23 x24 x34` THEN MESON_TAC[REAL_LT_IMP_LE; REAL_LE_DIV; REAL_LE_MUL; REAL_LE_ADD; REAL_LE_POW_2]);; (* le 86 . GDRQXLG *) let GDRQXLG = prove(` ! v1 v2 v3 (v4:real^3). let s = {v1, v2, v3, v4} in let x12 = dist (v1,v2) pow 2 in let x13 = dist (v1,v3) pow 2 in let x14 = dist (v1,v4) pow 2 in let x23 = dist (v2,v3) pow 2 in let x24 = dist (v2,v4) pow 2 in let x34 = dist (v3,v4) pow 2 in CARD s = 4 /\ ~coplanar_alt s ==> radV s = sqrt ( rho_ij' x12 x13 x14 x23 x24 x34) / (&2 * sqrt (delta x12 x13 x14 x23 x24 x34))`, REPEAT GEN_TAC THEN REPEAT LET_TAC THEN EXPAND_TAC "s" THEN NHANH (NOT_COPLANAR_IMP_RADV_PROPERTIES) THEN NHANH (REWRITE_RULE[RIGHT_FORALL_IMP_THM] (GEN `p:real^3` PROVE_DIST_FROM_V1 )) THEN NHANH (REWRITE_RULE[RIGHT_FORALL_IMP_THM] (GEN `p:real^3` PROVE_EQ_DIST_FROM4 ) ) THEN REWRITE_TAC[GSYM POS_EQ_NOT_COPLANANR] THEN NHANH (REAL_ARITH` &0 < a ==> ~( a = &0 )`) THEN NHANH (PROVE_IN_AFFINE_HULL_4 ) THEN LET_TR THEN REWRITE_TAC[MESON[]`(!x. x = a ==> p x) <=> p a `] THEN ABBREV_TAC `taa = (&1 / (&2 * delta (dist (v1,v2) pow 2) (dist (v1,v3) pow 2) (dist (v1,v4) pow 2) (dist (v2,v3) pow 2) (dist (v2,v4) pow 2) (dist (v3,v4) pow 2)) % (chi (dist (v1,v2) pow 2) (dist (v1,v3) pow 2) (dist (v1,v4) pow 2) (dist (v2,v3) pow 2) (dist (v2,v4) pow 2) (dist (v3,v4) pow 2) % (v1:real^3) + chi (dist (v1,v2) pow 2) (dist (v2,v4) pow 2) (dist (v2,v3) pow 2) (dist (v1,v4) pow 2) (dist (v1,v3) pow 2) (dist (v3,v4) pow 2) % v2 + chi (dist (v3,v4) pow 2) (dist (v1,v3) pow 2) (dist (v2,v3) pow 2) (dist (v1,v4) pow 2) (dist (v2,v4) pow 2) (dist (v1,v2) pow 2) % v3 + chi (dist (v3,v4) pow 2) (dist (v2,v4) pow 2) (dist (v1,v4) pow 2) (dist (v2,v3) pow 2) (dist (v1,v3) pow 2) (dist (v1,v2) pow 2) % v4)) ` THEN REWRITE_TAC[ POS_EQ_NOT_COPLANANR] THEN NGOAC THEN NHANH (SPEC_ALL UNIQUE_EXISISTING_PROPERTY_C4 ) THEN REWRITE_TAC[FORALL_IN_CLAUSES] THEN ABBREV_TAC ` abc = &1 / &2 * rho_ij' (dist (v1,v2) pow 2) (dist (v1,v3) pow 2) (dist (v1,v4) pow 2) (dist (v2,v3) pow 2) (dist (v2,v4) pow 2) (dist (v3,v4) pow 2) / (&2 * delta (dist ((v1:real^3),v2) pow 2) (dist (v1,v3) pow 2) (dist (v1,v4) pow 2) (dist (v2,v3) pow 2) (dist (v2,v4) pow 2) (dist (v3,v4) pow 2)) ` THEN REWRITE_TAC[dist3] THEN NHANH (MESON[POW_2_SQRT; DIST_POS_LE]` dist (taa,v2) pow 2 = a ==> dist(taa,v2) = sqrt a `) THEN PHA THEN NHANH (MESON[]`(!p. p IN affine hull {v1, v2, v3, v4} /\ (?r. r = dist (p,v1) /\ r = dist (p,v2) /\ r = dist (p,v3) /\ r = dist (p,v4)) ==> p = circumcenter {v1, v2, v3, v4}) /\ a11 /\ taa IN affine hull {v1, v2, v3, v4} /\ dist (taa,v2) pow 2 = abc /\ dist (taa,v2) = sqrt abc /\ dist (taa,v3) pow 2 = abc /\ dist (taa,v3) = sqrt abc /\ dist (taa,v4) pow 2 = abc /\ dist (taa,v4) = sqrt abc /\ dist (taa,v1) pow 2 = abc /\ dist (taa,v1) = sqrt abc /\ lll ==> taa = circumcenter {v1, v2, v3, v4} `) THEN NHANH (SET_RULE ` (!w. {v1, v2, v3, v4} w ==> P w ) ==> P v1 `) THEN PHA THEN REWRITE_TAC[MESON[]` a = dist (aa,b) /\ ta = aa <=> ta = aa /\ a = dist (ta,b) `] THEN NHANH (MESON[]` a = b /\ a1 /\ a2 /\ c = a ==> c = b `) THEN NHANH (SPEC_ALL SHOGYBS) THEN MP_TAC (SPECL [`v1:real^3`;` v2:real^3`;`v3:real^3`;`v4:real^3`] DELTA_POS_4POINTS) THEN REPEAT LET_TAC THEN IMP_TAC THEN REPEAT (FIRST_X_ASSUM MP_TAC) THEN REWRITE_TAC[MESON[]` a = b ==> P a <=> a = b ==> P b `] THEN REWRITE_TAC[MESON[]` a = b ==> a = c <=> a = b ==> c = b `] THEN REPEAT STRIP_TAC THEN UNDISCH_TAC ` &1 / &2 * rho_ij' x12 x13 x14 x23 x24 x34 / (&2 * delta x12 x13 x14 x23 x24 x34) = abc ` THEN UNDISCH_TAC ` &0 <= rho_ij' x12 x13 x14 x23 x24 x34 ` THEN ABBREV_TAC ` edl = delta x12 x13 x14 x23 x24 x34 ` THEN UNDISCH_TAC` &0 <= edl ` THEN SIMP_TAC[REAL_ARITH` &0 <= &4 `; GSYM SQRT_MUL; GSYM SQRT4_EQ2] THEN SIMP_TAC[REAL_ARITH` &0 <= &4 `; REAL_LE_MUL; GSYM SQRT_DIV] THEN REWRITE_TAC[SQRT4_EQ2] THEN MESON_TAC[REAL_FIELD` &1 / &2 * x34 / (&2 * edl) = x34 / (&4 * edl)`]);; end;; (* end of module *)