text_formalization/leg/collect_geom2.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Lemma: NUHSVLM                                                      *)
   5 (* Chapter: leg                                                               *)
   6 (* Author:  Nguyen Quang Truong                                              *)
   7 (* Date: 2010-02-09                                                           *)
   8 (* ========================================================================== *)
   9
  10
  11 (* second half of collect_geom.ml.
  12 It was split in half by thales Feb 2010.
  13
  14 This file was edited by thales on 2012-5-15
  15 to make it possible to load everything up through lemma GDRQXLG
  16 giving the formula for the circumradius of a simplex.
  17
  18 Everything dependent on unproved axioms was commented out.
  19
  20 Feb 2013, some excess material removed.
  21  *)
  22
  23 flyspeck_needs "leg/cayleyR_def.hl";;
  24 flyspeck_needs "leg/collect_geom.hl";;
  25
  26 module Collect_geom2 (* : Collect_geom2_type *)  = struct
  27
  28   open Sphere;;
  29   open Geomdetail;;
  30   open Collect_geom;;
  31
  32
  33
  34   let cayleyR = Cayleyr.cayleyR;;
  35
  36   let LET_TR = Collect_geom.LET_TR;;
  37   let DIST_POW2_DOT = Collect_geom.DIST_POW2_DOT;;
  38   let UPS_X_POS = Collect_geom.UPS_X_POS;;
  39   let DELTA_POS_4POINTS = Collect_geom.DELTA_POS_4POINTS;;
  40   let REAL_LDISTRIB = REAL_ADD_LDISTRIB;;
  41   let POW_2 = REAL_POW_2;;
  42   let REAL_POSSQ = REAL_LT_SQUARE;;
  43   let REAL_RDISTRIB = REAL_ARITH
  44     `!x y z. (x + y) * z = (x * z) + (y * z)`;;  (* Tactics_jordan *)
  45
  46   let BY = Hales_tactic.BY;;
  47
  48 (* deprecated def from sphere.hl *)
  49   let mk_vec3 = new_definition
  50   `mk_vec3 a b c = vector[a; b; c]`;;
  51   let real3_of_triple = new_definition
  52     `real3_of_triple (a,b,c) = (mk_vec3 a b c):real^3`;;
  53   let triple_of_real3 = new_definition
  54     `triple_of_real3 (v:real^3) =
  55     (v$1, v$2, v$3)`;;
  56 (* deprecated def from sphere.hl *)
  57
  58
  59 (* this lemma is proved as below, but it take quite a long time to run it *)
  60
  61 let CAYLEYR_5POINTS = prove(`  !x1 x2 x3 x4 (x5 :real^3).
  62          let x12 = dist (x1,x2) pow 2 in
  63          let x13 = dist (x1,x3) pow 2 in
  64          let x14 = dist (x1,x4) pow 2 in
  65          let x15 = dist (x1,x5) pow 2 in
  66          let x23 = dist (x2,x3) pow 2 in
  67          let x24 = dist (x2,x4) pow 2 in
  68          let x25 = dist (x2,x5) pow 2 in
  69          let x34 = dist (x3,x4) pow 2 in
  70          let x35 = dist (x3,x5) pow 2 in
  71          let x45 = dist (x4,x5) pow 2 in
  72          cayleyR x12 x13 x14 x15 x23 x24 x25 x34 x35 x45 = &0 `,
  73 LET_TR THEN REWRITE_TAC[ DIST_POW2_DOT] THEN REPEAT GEN_TAC THEN
  74 REWRITE_TAC[ MESON[VECTOR_ARITH` (a:real^n) - b = a - x - ( b - x ) `]`
  75   AA ( (x1 - x5 ) dot ( x1 - x5)) ((x2 - x3) dot (x2 - x3))
  76  ((x2 - x4) dot (x2 - x4))
  77  ((x2 - x5) dot (x2 - x5))
  78  ((x3 - x4) dot (x3 - x4))
  79  ((x3 - x5) dot (x3 - x5))
  80  ((x4 - x5) dot (x4 - x5)) =
  81   AA ( (x1 - x5 ) dot ( x1 - x5)) ((x2 - x1 - ( x3 - x1 )) dot (x2 - x1 - ( x3 - x1 )))
  82   ((x2 - x1 - ( x4 - x1 )) dot (x2 - x1 - ( x4 - x1 )))
  83   ((x2 - x1 - ( x5 - x1 )) dot (x2 - x1 - ( x5 - x1 )))
  84   ((x3 - x1 - ( x4 - x1 )) dot (x3 - x1 - ( x4 - x1 )))
  85   ((x3 - x1 - ( x5 - x1 )) dot (x3 - x1 - ( x5 - x1 )))
  86     ((x4 - x1 - ( x5 - x1 )) dot (x4 - x1 - ( x5 - x1 ))) ` ] THEN
  87 SIMP_TAC[VECTOR_ARITH ` ((x4: real^N) - x1 - (x5 - x1)) = x1 - x5 - ( x1 - x4 ) `] THEN
  88 ABBREV_TAC ` x12 = (x1 - ( x2:real^3)) ` THEN
  89 ABBREV_TAC ` x13 = (x1 - ( x3:real^3)) ` THEN
  90 ABBREV_TAC ` x14 = (x1 - ( x4:real^3)) ` THEN
  91 ABBREV_TAC ` x15 = (x1 - ( x5:real^3)) ` THEN
  92 REWRITE_TAC[DOT_3] THEN REWRITE_TAC[lemma_cm3; cayleyR] THEN REAL_ARITH_TAC);;
  93
  94
  95
  96
  97 let LEMMA3 = prove(` !x1 x2 x3 x4 (x5 :real^3).
  98                  let x12 = dist (x1,x2) pow 2 in
  99          let x13 = dist (x1,x3) pow 2 in
 100          let x14 = dist (x1,x4) pow 2 in
 101          let x15 = dist (x1,x5) pow 2 in
 102          let x23 = dist (x2,x3) pow 2 in
 103          let x24 = dist (x2,x4) pow 2 in
 104          let x25 = dist (x2,x5) pow 2 in
 105          let x34 = dist (x3,x4) pow 2 in
 106          let x35 = dist (x3,x5) pow 2 in
 107          let x45 = dist (x4,x5) pow 2 in
 108          &0 <= ups_x x12 x13 x23 /\
 109          &0 <= delta x12 x13 x14 x23 x24 x34 /\
 110          cayleyR x12 x13 x14 x15 x23 x24 x25 x34 x35 x45 = &0 `, MP_TAC
 111 CAYLEYR_5POINTS THEN LET_TR THEN
 112 SIMP_TAC[ dist; UPS_X_POS; DELTA_POS_4POINTS]);;
 113
 114
 115 (* LEMMA 3 *)
 116 let NUHSVLM = LEMMA3;;
 117
 118
 119 (* OLD END OF MODULE *)
 120
 121
 122 let LEMMA52 = prove( `! v1 v2 v3 v4 (v5:real^3).
 123   muy_v v1 v2 v3 v4 v5 ( (dist3 v4 v5) pow 2 ) = &0 `,
 124 REWRITE_TAC[muy_v; dist3] THEN MP_TAC LEMMA3 THEN
 125 LET_TR THEN SIMP_TAC[]);;
 126
 127 let PFDFWWV = LEMMA52;;
 128
 129 let PRE_VIET =
 130 REAL_ARITH `!x x1 x2. (x - x1) * (x - x2) = x pow 2 - (x1 + x2) * x + x1 * x2 /\
 131  a * (x - x1) * (x - x2) = a * x pow 2 + ( -- a * (x1 + x2)) * x + a * x1 * x2 `;;
 132
 133
 134 let VIET_THEOREM = prove(`! x1 x2 a b c. (!x. a * x pow 2 + b * x + c =
 135 a * (x - x1) * (x - x2)) ==>  -- b = a * ( x1 + x2 ) /\ c = a * x1 * x2 `,
 136 REWRITE_TAC[PRE_VIET; REAL_LDISTRIB;REAL_SUB_LDISTRIB;
 137 REAL_ARITH ` a - b * c = a + -- b * c `; REAL_ARITH` ( a + b ) + c =
 138 a + b + c `] THEN
 139 REWRITE_TAC[REAL_MUL_ASSOC; EQUATE_CONEFS_POLINOMIAL_POW2] THEN
 140 SIMP_TAC[] THEN REAL_ARITH_TAC);;
 141
 142 let ADD_SUB_POW2_EX = REAL_RING ` ( a + b ) pow 2 = a pow 2 + &2 * a * b + b pow 2 /\
 143 ( a - b ) pow 2 = a pow 2 - &2 * a * b + b pow 2 `;;
 144
 145 let PRESENT_SUB_POW2 = REAL_RING` ! a b. ( a - b ) pow 2 = ( a + b ) pow 2
 146   - &4 * a * b `;;
 147
 148 let DIST_ROOT_AND_DISCRIMINANT = prove(` ! a b c x1 x2. ( ! x. a * x pow 2 + b * x + c =
 149  a * ( x - x1 ) * ( x - x2 ) )
 150   ==> ( a pow 2 ) * ( x1 - x2 ) pow 2 = b pow 2 - &4 * a * c `,
 151 NHANH (SPEC_ALL VIET_THEOREM) THEN REWRITE_TAC[PRESENT_SUB_POW2] THEN
 152 SIMP_TAC[REAL_ARITH ` -- b = a <=> b = -- a `] THEN REAL_ARITH_TAC);;
 153
 154 (* le 33. P 22 MARKED *)
 155
 156 let REAL_EQ_TO_LE_LT = REAL_ARITH `
 157   ( a = b <=> ~( a < b \/ b < a ) )`;;
 158
 159 let FEBRUARY_13_09 = prove(` &0 < (u - v) dot (&2 % x - (u + v)) <=>
 160   &0 < (u - v) dot (x - &1 / &2 % (u + v)) `,
 161 ONCE_REWRITE_TAC[MESON[REAL_ARITH ` &0 < a <=> &0 < &2 * a `]` (a <=> &0 < b ) <=>
 162   ( a <=> &0 < &2 * b ) `] THEN ONCE_REWRITE_TAC[VECTOR_ARITH ` x * (a dot b) =
 163   a dot x % b `] THEN
 164 REWRITE_TAC[GSYM VECTOR_SUB_DISTRIBUTE; VECTOR_MUL_ASSOC] THEN
 165 REWRITE_TAC[REAL_ARITH ` &2 * &1 / &2 = &1 `; VECTOR_MUL_LID]);;
 166
 167 let SUB_DOT_NEG_TO_POS = MESON[VECTOR_ARITH ` ( a - b ) dot x =
 168 --  (( b - a ) dot x ) `;  REAL_ARITH ` -- a < &0 <=> &0 < a `]
 169 `! a b.  ( a - b ) dot x < &0 <=> &0 < ( b - a ) dot x `;;
 170
 171
 172 let LEMMA6 = prove(` !(u:real^3) v. ~(u = v) ==> plane_norm (bis u v) `,
 173 REWRITE_TAC[plane_norm; bis] THEN REPEAT STRIP_TAC THEN
 174 EXISTS_TAC ` (u: real^3) - v ` THEN
 175 EXISTS_TAC ` &1 / &2 % ((u: real^3) + v )` THEN
 176 REWRITE_TAC[FUN_EQ_THM; IN_ELIM_THM] THEN ASM_SIMP_TAC[VECTOR_SUB_EQ] THEN
 177 REWRITE_TAC[REAL_EQ_TO_LE_LT; DIST_LT_HALF_PLANE;FEBRUARY_13_09;
 178  SUB_DOT_NEG_TO_POS] THEN SIMP_TAC[VECTOR_ADD_SYM] THEN MESON_TAC[]);;
 179
 180 let BXVMKNF = LEMMA6;;
 181
 182
 183 let b_coef = BC_DEL_FOR;;
 184 let c_coef = b_coef ;;
 185
 186 let DELTA_X34_B = prove(` ! x12 x13 x14 x23 x24 x. delta_x34 x12 x13 x14 x23 x24 x =
 187   -- &2 * x12 * x + b_coef x12 x13 x14 x23 x24 `, REWRITE_TAC[ delta_x34; b_coef]);;
 188
 189
 190
 191
 192 let EQ_POW2_COND = prove(`!a b. &0 <= a /\ &0 <= b ==> (a = b <=> a pow 2 = b pow 2)`,
 193 REWRITE_TAC[REAL_ARITH` a = b <=> a <= b /\ b <= a `] THEN SIMP_TAC[POW2_COND]);;
 194
 195
 196 let EQ_SQRT_POW2_EQ = prove(` &0 <= a /\ &0 <= b ==> ( a = sqrt b <=> a pow 2 = b ) `,
 197 SIMP_TAC[SQRT_WORKS; EQ_POW2_COND]);;
 198
 199
 200 (*
 201 let LEMMA33 = prove(` !x34 x12 x13 v1 x14 v3 x23 v2 v4 x24 x34' x34'' a.
 202  condA v1 v2 v3 v4 x12 x13 x14 x23 x24 x34 /\
 203           (! x. muy_delta x12 x13 x14 x23 x24 x = a * ( x - x34' ) * ( x - x34''))
 204 /\ x34' <= x34''
 205   ==> delta_x34 x12 x13 x14 x23 x24 x34' =
 206              sqrt (ups_x x12 x13 x23 * ups_x x12 x14 x24) /\
 207              delta_x34 x12 x13 x14 x23 x24 x34'' =
 208              --sqrt (ups_x x12 x13 x23 * ups_x x12 x14 x24) `,
 209 REWRITE_TAC[muy_delta; DELTA_X34_B; DELTA_COEFS] THEN
 210 SIMP_TAC[EQUATE_CONEFS_POLINOMIAL_POW2; PRE_VIET;
 211 REAL_ARITH ` -- a = b <=> b = -- a`] THEN
 212 SIMP_TAC[REAL_RING `-- &2 * x12 * x34' + -- --x12 * (x34' + x34'') = a <=>
 213   -- &2 * x12 * x34'' + -- --x12 * (x34' + x34'') = -- a `] THEN
 214 REWRITE_TAC[REAL_ARITH` -- &2 * x12 * x34'' + -- --x12 * (x34' + x34'')
 215   = x12 * ( x34' - x34'' ) `; condA] THEN REPEAT STRIP_TAC THEN
 216 EXPAND_TAC "x12"  THEN EXPAND_TAC "x13" THEN EXPAND_TAC "x23" THEN
 217 EXPAND_TAC "x14" THEN EXPAND_TAC "x24" THEN
 218 UNDISCH_TAC ` x34' <= (x34'':real)` THEN
 219 ONCE_REWRITE_TAC[REAL_ARITH ` a <= b <=> &0 <= b - a `] THEN
 220 ONCE_REWRITE_TAC[ REAL_ARITH ` a * ( b - c ) = -- ( a * ( c - b ) ) `] THEN
 221 MP_TAC (GEN_ALL TROI_OI_DAT_HOI) THEN MP_TAC REAL_LE_POW_2 THEN
 222 REWRITE_TAC[REAL_ARITH` -- a = -- b <=> a = b `] THEN
 223 SIMP_TAC[UPS_X_SYM; REAL_LE_MUL; EQ_SQRT_POW2_EQ ] THEN
 224 ASM_SIMP_TAC[] THEN REPEAT STRIP_TAC THEN
 225 ONCE_REWRITE_TAC[ REAL_ARITH ` ( a * b ) pow 2 = a pow 2 * b pow 2 `] THEN
 226 REWRITE_TAC[PRESENT_SUB_POW2] THEN
 227 REWRITE_TAC[REAL_SUB_LDISTRIB; REAL_ARITH ` a pow 2 * b pow 2 =
 228 ( -- a * b ) pow 2   /\ a pow 2 * &4 * b = -- a * &4 * -- a * b `] THEN
 229 UNDISCH_TAC `b_coef x12 x13 x14 x23 x24 = --a * (x34' + x34'')` THEN
 230 UNDISCH_TAC `c_coef x12 x13 x14 x23 x24 = a * x34' * x34''` THEN
 231 UNDISCH_TAC `(a: real) = --x12` THEN ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN
 232 SIMP_TAC[] THEN SIMP_TAC[REAL_ARITH` -- -- a = a /\ ( -- a * b) pow 2 =
 233   ( a * b ) pow 2 /\ ( a * -- b) pow 2 = ( a * b ) pow 2  `; REAL_ADD_SYM;
 234  REAL_MUL_SYM] THEN SIMP_TAC[REAL_ADD_SYM; REAL_MUL_SYM] THEN
 235 ONCE_REWRITE_TAC[REAL_ARITH ` ( a * b ) pow 2 = ( b * -- a ) pow 2 `] THEN
 236 SIMP_TAC[] THEN REPEAT STRIP_TAC THEN EXPAND_TAC "a" THEN
 237 REWRITE_TAC[REAL_RING ` a - -- c * b * &4 = a + &4 * c * b `] THEN
 238 MESON_TAC[AGBWHRD; UPS_X_SYM]);;
 239 *)
 240
 241 (* let CMUDPKT = LEMMA33;; *)
 242
 243 (* ============= *)
 244
 245
 246 let LEMMA_OF_LE20 = prove(` ! x y z: real^3.
 247    &2 <= dist3 x y /\
 248          dist3 x y <= #2.52 /\
 249          &2 <= dist3 x z /\
 250          dist3 x z <= #2.2 /\
 251          &2 <= dist3 y z /\
 252          dist3 y z <= #2.2
 253          ==> ~collinear {x, y, z}  `,
 254 MP_TAC JVUNDLC THEN
 255 SIMP_TAC[] THEN
 256 ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN
 257 REWRITE_TAC[MESON[]` (! a b c s. P a b c = s ==> Q a b c ) <=>
 258   (! a b c . Q a b c ) `] THEN
 259 SIMP_TAC[COL_EQ_UPS_0] THEN
 260 MATCH_MP_TAC (TAUT` a ==> b ==> a `) THEN
 261 REWRITE_TAC[GSYM dist3] THEN
 262 REWRITE_TAC[REAL_ENTIRE] THEN
 263 CONV_TAC REAL_FIELD);;
 264
 265
 266
 267 let LT_POW2_EQ_LT = MESON[POW2_COND_LT; REAL_ARITH ` a <= b <=> ~ ( b < a ) `]
 268 `&0 < a /\ &0 < b ==> ( a < b <=> a pow 2 < b pow 2 ) `;;
 269
 270 let ETA_Y_LT_SQRT2 = prove(`eta_y #2.2 #2.2 #2.52 < sqrt #2`,
 271 REWRITE_TAC[eta_y; eta_x; ups_x] THEN LET_TR THEN
 272 CONV_TAC REAL_RAT_REDUCE_CONV THEN MP_TAC (REAL_FIELD ` &14641 / &8131< &2 `)
 273  THEN MP_TAC (REAL_FIELD ` &0 < &2 /\ &0 < &14641 / &8131 `) THEN
 274 NHANH (SPEC_ALL SQRT_POS_LT) THEN REWRITE_TAC[ REAL_ARITH ` #2 = &2 `] THEN
 275 SIMP_TAC[REAL_ARITH ` &0 < a ==> &0 <= a `;SQRT_POS_LT; LT_POW2_EQ_LT; SQRT_WORKS]);;
 276
 277 let ETA_YY_LT_SQRT2 = MESON[ETA_Y_LT_SQRT2; REAL_ARITH ` #2 = &2 `]`
 278   eta_y #2.2 #2.2 #2.52 < sqrt ( &2 ) `;;
 279
 280 let THANG_DEU = prove(` &2 <= x ==> &2 pow 2 <= x pow 2 `,
 281 NHANH (REAL_ARITH ` &2 <= x ==> &0 <= &2 /\ &0 <= x `)
 282 THEN MESON_TAC[POW2_COND]);;
 283
 284 let NGAY23_THANG2_09 = prove(` &2 <= y /\ y <= sqrt (&8) ==>
 285   &2 pow 2 <= y * y /\ y * y <= &8 `,
 286 REWRITE_TAC[ GSYM REAL_POW_2] THEN DISCH_TAC THEN CONJ_TAC THENL
 287 [ASM_MESON_TAC[REAL_ARITH ` &2 <= a ==> &0 <= &2 /\ &0 <= a `;POW2_COND];
 288 ASM_MESON_TAC[ SQRT_WORKS; REAL_ARITH ` &0 <= &8 `;
 289   POW2_COND; REAL_ARITH `&2 <= a /\ a <= b ==> &0 <= b /\ &0 <= a `]]);;
 290
 291
 292
 293 let ETA_Y_SQRT8_2_251 = prove(` eta_y ( sqrt (&8) ) (&2) #2.51 < #1.453`,
 294 REWRITE_TAC[eta_y; eta_x; ups_x; GSYM POW_2] THEN
 295 LET_TR THEN
 296 REWRITE_TAC[MESON[SQRT_WORKS; REAL_ARITH ` &0 <= &8 `]` sqrt (&8) pow 2 = &8 `] THEN
 297 CONV_TAC REAL_RAT_REDUCE_CONV THEN
 298 MP_TAC (REAL_FIELD ` &0 < &20160320000 / &9551113999 /\ &0 < #1.453 `) THEN
 299 NHANH (SPEC_ALL SQRT_POS_LT) THEN
 300 SIMP_TAC[LT_POW2_EQ_LT; REAL_ARITH ` &0 < a ==> &0 <= a `; SQRT_POW_2] THEN
 301 DISCH_TAC THEN
 302 CONV_TAC REAL_FIELD );;
 303
 304 let CDEUSDF_CHANGE = CDEUSDF;;
 305
 306
 307 let CIRCUMCENTER_FORMULAR = prove(` ! va vb vc.  ~collinear {va, vb, vc}
 308  ==> circumcenter {va, vb, vc} =
 309   (dist3 vb vc pow 2 *
 310            (dist3 va vc pow 2 + dist3 va vb pow 2 - dist3 vb vc pow 2)) /
 311           (ups_x (dist3 vb vc pow 2) (dist3 va vc pow 2) (dist3 va vb pow 2)) %
 312           va +
 313           (dist3 va vc pow 2 *
 314            (dist3 vb vc pow 2 + dist3 va vb pow 2 - dist3 va vc pow 2)) /
 315           (ups_x (dist3 vb vc pow 2) (dist3 va vc pow 2) (dist3 va vb pow 2)) %
 316           vb +
 317           (dist3 va vb pow 2 *
 318            (dist3 vb vc pow 2 + dist3 va vc pow 2 - dist3 va vb pow 2)) /
 319           (ups_x (dist3 vb vc pow 2) (dist3 va vc pow 2) (dist3 va vb pow 2)) %
 320           vc `,
 321 ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN
 322 MP_TAC CDEUSDF_CHANGE THEN LET_TR THEN MESON_TAC[]);;
 323
 324 let LE_EX = REAL_ARITH ` &0 <= a <=> a = &0 \/ &0 < a `;;
 325
 326 let SUM_UPS_X_1 = prove(`!a b c.
 327      &0 < ups_x a b c
 328      ==> (c * (b + a - c)) / ups_x a b c +
 329          (a * (c + b - a)) / ups_x a b c +
 330          (b * (c + a - b)) / ups_x a b c =
 331          &1`, REWRITE_TAC[ups_x] THEN CONV_TAC REAL_FIELD);;
 332
 333
 334 MESON[POW2_COND; REAL_ARITH `&2 <= a /\ a <= b ==> &0 <= b /\ &0 <= a `]`
 335   &2 <= y /\ y <= b ==> y pow 2 <= b pow 2 `;;
 336
 337
 338 let FACTOR_OF_QUADRARTIC = prove(`! a b c x. ~(a = &0) /\
 339 &0 <= b pow 2 - &4 * a * c ==> a * x pow 2 + b * x + c =
 340      a *
 341      (x - (--b + sqrt (b pow 2 - &4 * a * c)) / (&2 * a)) *
 342      (x - (--b - sqrt (b pow 2 - &4 * a * c)) / (&2 * a))`   ,
 343 REWRITE_TAC[PRE_VIET] THEN SIMP_TAC[REAL_FIELD ` ~( a = &0 ) ==>
 344 -- a * ( ( --b + del) / ( &2 * a ) + ( --b - del) / ( &2 * a )) = b `] THEN
 345 REWRITE_TAC[REAL_FIELD ` a / b * a' / b = ( a * a' ) / ( b pow 2 ) `] THEN
 346 REWRITE_TAC[REAL_FIELD ` a / b * a' / b = ( a * a' ) / ( b pow 2 ) `;
 347   REAL_DIFFSQ; GSYM REAL_POW_2] THEN SIMP_TAC[SQRT_WORKS] THEN
 348 SIMP_TAC[REAL_FIELD ` ~ ( a = &0 ) ==> a * (--b pow 2 -
 349  (b pow 2 - &4 * a * c)) / (&2 * a) pow 2 = c `]);;
 350
 351
 352 let COMPUTE_TO_QUA_POLY = prove(` #2.696 <= x /\ x <= sqrt8  ==>
 353 x pow 2  * ( &1 / eta_y x #2.45 #2.45 pow 2 -
 354   &1 / eta_y x ( &2 ) #2.51 pow 2 ) = &4331842500 / &363188227801 * x pow 4 +
 355      -- &45702201 / &302530802 * x pow 2 +
 356      &529046001 / &2520040000 `, REWRITE_TAC[eta_y; eta_x; ups_x] THEN
 357 LET_TR THEN
 358 CONV_TAC REAL_RAT_REDUCE_CONV THEN
 359 NHANH (MESON[REAL_ARITH ` #2.696 <= x /\ x <= sqrt8 ==>
 360   &0 <= #2.696 /\ &0 <= x `; REAL_LE_MUL2] ` #2.696 <= x /\ x <= sqrt8 ==>
 361    #2.696 * #2.696 <= x * x /\ x * x <= sqrt8 * sqrt8 `) THEN
 362 NHANH (MESON[REAL_ARITH ` #2.696 * #2.696 <= x ==> &0 <= #2.696 * #2.696 /\ &0 <= x `; REAL_LE_MUL2] `
 363   #2.696 * #2.696 <= x /\ x <= hh ==> (#2.696 * #2.696) * #2.696 * #2.696 <= x * x /\
 364   x * x <= hh * hh `) THEN
 365 REWRITE_TAC[sqrt8] THEN
 366 REWRITE_TAC[REAL_POLY_CONV ` (--(x * x) * x * x - &16 - &3969126001 / &100000000 +
 367         &2 * (x * x) * &63001 / &10000 +
 368         &2 * (x * x) * &4 +
 369         &63001 / &1250) `] THEN
 370 REWRITE_TAC[REAL_POLY_CONV `
 371   (--(x * x) * x * x - &5764801 / &160000 - &5764801 / &160000 +
 372         &2 * (x * x) * &2401 / &400 +
 373         &2 * (x * x) * &2401 / &400 +
 374         &5764801 / &80000) `] THEN
 375 REWRITE_TAC[REAL_ARITH ` x pow 4 = ( x pow 2 ) pow 2 `] THEN
 376 MP_TAC (REAL_ARITH ` ~ ( -- &1 = &0 ) /\ &0 <= ( &103001 / &5000 ) pow 2 - &4 * ( -- &1 ) * -- &529046001 / &100000000 `) THEN
 377 SIMP_TAC[FACTOR_OF_QUADRARTIC] THEN
 378 CONV_TAC REAL_RAT_REDUCE_CONV THEN
 379 REWRITE_TAC[REAL_ARITH ` (&252004 / &625) = ( &502 / &25 ) * ( &502 / &25 ) `] THEN
 380 REWRITE_TAC[MESON[REAL_ARITH ` &0 <= &502 / &25 /\ x * x = x pow 2 `; POW_2_SQRT]`
 381   sqrt ( ( &502 / &25 ) * ( &502 / &25 )) = ( &502 / &25 ) `] THEN
 382 CONV_TAC REAL_RAT_REDUCE_CONV THEN
 383 REWRITE_TAC[ GSYM POW_2] THEN
 384 REWRITE_TAC[REAL_ARITH `  a * x pow 2 + b * x = ( a * x + b ) * x `] THEN
 385 REWRITE_TAC[MESON[SQRT_WORKS; REAL_ARITH ` &0 <= &8`]` sqrt (&8) pow 2 = &8 `] THEN
 386 NHANH (REAL_FIELD ` (&113569 / &15625 <= x pow 2 /\ x pow 2 <= &8)
 387   ==> &0 <= (-- &1 * x pow 2 + &2401 / &100) /\
 388   &0 <= (x pow 2 - &2601 / &10000 ) /\
 389   &0 <= -- ((x pow 2 - &203401 / &10000) )/\ &0 <= &5764801 / &160000 /\
 390 &0 <= &63001 / &2500`) THEN
 391 MP_TAC REAL_LE_POW_2 THEN
 392 REWRITE_TAC[REAL_ARITH ` -- &1 * a * b = a * -- b `] THEN
 393 REWRITE_TAC[REAL_FIELD ` ( &1 / a ) pow 2  = &1 / ( a pow 2 ) `] THEN
 394 MP_TAC REAL_LE_MUL THEN
 395 MP_TAC REAL_LE_DIV THEN
 396 SIMP_TAC[ SQRT_WORKS] THEN
 397 REWRITE_TAC[REAL_SUB_LDISTRIB] THEN
 398 REWRITE_TAC[REAL_FIELD ` &1 / ( a / b ) = b / a `] THEN
 399 SIMP_TAC[REAL_FIELD ` &113569 / &15625 <= a ==> a * ( b / ( a * c )) = b / c `] THEN
 400 REWRITE_TAC[REAL_POLY_CONV ` ((-- &1 * x pow 2 + &2401 / &100) * x pow 2) / (&5764801 / &160000) -
 401      ((x pow 2 - &2601 / &10000) * --(x pow 2 - &203401 / &10000)) /
 402      (&63001 / &2500) `] THEN
 403 REWRITE_TAC[REAL_ARITH ` a pow 4 = a pow 2 pow 2 `]);;
 404
 405 (*
 406 REAL_ARITH ` &4650694416 = ( &68196 ) pow 2 `;;
 407 REAL_ARITH` &4650694416 / &363188227801 = ( &68196 / &602651 ) pow 2 `;;
 408 *)
 409
 410 let PHAN_TICH = prove(  `! x. &4331842500 / &363188227801 *
 411      (x pow 2 - &488365801 / &44090000) *
 412      (x pow 2 - &2081667 / &1310000) =
 413      &4331842500 / &363188227801 * x pow 4 +
 414      -- &45702201 / &302530802 * x pow 2 +
 415      &529046001 / &2520040000`   , REAL_ARITH_TAC);;
 416
 417 let Q_TR = prove(`! x. #2.696 <= x /\ x <= sqrt8 ==>
 418   x pow 2 *
 419          (&1 / eta_y x #2.45 #2.45 pow 2 - &1 / eta_y x (&2) #2.51 pow 2) <= &0 `,
 420 SIMP_TAC[COMPUTE_TO_QUA_POLY; GSYM PHAN_TICH ] THEN
 421 NHANH (MESON[REAL_ARITH ` #2.696 <= x /\ x <= hh ==> &0 <= #2.696 /\ &0 <= x`
 422   ; REAL_LE_MUL2] ` #2.696 <= x /\ x <= hh ==>
 423    #2.696 * #2.696 <= x * x /\ x * x <= hh * hh `) THEN
 424 REWRITE_TAC[REAL_ARITH `
 425          &4331842500 / &363188227801 * a <= &0 <=> a <= &0 `] THEN
 426 CONV_TAC REAL_RAT_REDUCE_CONV THEN
 427 REWRITE_TAC[REAL_ARITH ` &0 <=
 428          &4331842500 / &363188227801 * a <=> &0 <= a `; sqrt8; GSYM POW_2;
 429   MESON[SQRT_WORKS; REAL_ARITH ` &0 <= &8 `]` sqrt (&8) pow 2 = &8 `] THEN
 430 NHANH (REAL_ARITH ` &113569 / &15625 <= x pow 2 /\
 431      x pow 2 <= &8 ==> x pow 2 - &488365801 / &44090000 <= &0 /\
 432   x pow 2 - &2081667 / &1310000 >= &0 `) THEN
 433 REWRITE_TAC[ REAL_ARITH ` ( a >= &0 <=> &0 <= a)/\ (a <= &0 <=> &0 <= -- a ) `] THEN
 434 REWRITE_TAC[REAL_ARITH ` -- ( a * b ) = -- a * b `] THEN
 435 MESON_TAC[REAL_LE_MUL]);;
 436
 437 let SQRT8_LT = prove(` sqrt (&8) < &4 * #2.45 `,
 438 MP_TAC (REAL_ARITH ` &0 < &8 /\ &0 <  &4 * #2.45`) THEN
 439 SIMP_TAC[SQRT_POS_LT; LT_POW2_EQ_LT] THEN
 440 SIMP_TAC[REAL_LT_IMP_LE; SQRT_WORKS] THEN REAL_ARITH_TAC);;
 441
 442
 443
 444 let SQRT8_POW2 = MESON[SQRT_WORKS; REAL_ARITH ` &0 <= &8 `]` sqrt (&8) pow 2 = &8 `;;
 445
 446
 447 let IM_UP_POS = prove(`! x. #2.696 <= x /\ x <= sqrt8 ==>
 448 &0 < ups_x (x * x) (#2.45 * #2.45) (#2.45 * #2.45) /\
 449 &0 < ups_x (x * x) (&2 * &2) (#2.51 * #2.51) `,
 450 REWRITE_TAC[ups_x] THEN
 451 REWRITE_TAC[REAL_IDEAL_CONV [` (x:real) pow 2 `]`
 452          --(x * x) * x * x -
 453          (#2.45 * #2.45) * #2.45 * #2.45 -
 454          (#2.45 * #2.45) * #2.45 * #2.45 +
 455          &2 * (x * x) * #2.45 * #2.45 +
 456          &2 * (x * x) * #2.45 * #2.45 +
 457          &2 * (#2.45 * #2.45) * #2.45 * #2.45 `] THEN
 458 CONV_TAC REAL_RAT_REDUCE_CONV THEN
 459 REWRITE_TAC[REAL_POLY_CONV ` --(x * x) * x * x - &16 - &3969126001 / &100000000 +
 460          &2 * (x * x) * &63001 / &10000 +
 461          &2 * (x * x) * &4 +
 462          &63001 / &1250 `] THEN
 463 NHANH (REAL_ARITH` #2.696 <= x /\ x <= s ==> &0 <= #2.696 /\
 464   &0 <= x /\ &0 <= s `) THEN
 465 ONCE_REWRITE_TAC[MESON[]` a /\ b ==> c <=> b ==> a ==> c `] THEN
 466 SIMP_TAC[POW2_COND; sqrt8; SQRT8_POW2] THEN
 467 NHANH (REAL_ARITH` #2.696 pow 2 <= x /\ x <= &8 ==>
 468   &0 < &2401 / &100 + -- &1 * x /\ &0 < x /\
 469   ~ ( -- &1 = &0 ) /\ &0 <= ( &103001 / &5000 ) pow 2 - &4 * -- &1 *
 470   -- &529046001 / &100000000 `) THEN
 471 SIMP_TAC[REAL_ARITH ` x pow 4 = x pow 2 pow 2 `; FACTOR_OF_QUADRARTIC] THEN
 472 CONV_TAC REAL_RAT_REDUCE_CONV THEN
 473 REWRITE_TAC[REAL_ARITH ` &252004 / &625 = ( &502 / &25) pow 2 `] THEN
 474 REWRITE_TAC[MESON[POW_2_SQRT; REAL_ARITH ` &0 <= &502 / &25 `]`
 475   sqrt ((&502 / &25) pow 2) = &502 / &25 `] THEN
 476 CONV_TAC REAL_RAT_REDUCE_CONV THEN
 477 NHANH (REAL_ARITH ` &113569 / &15625 <= x pow 2 /\ x pow 2 <= &8 ==>
 478   &0 < x pow 2 - &2601 / &10000 /\ &0 < -- (x pow 2 - &203401 / &10000) `) THEN
 479 REWRITE_TAC[REAL_ARITH ` -- &1 * a * b = a * --b `] THEN
 480 SIMP_TAC[REAL_LT_MUL]);;
 481
 482
 483 let IMP_ETAY_POS = prove( `! x. #2.696 <= x /\ x <= sqrt8 ==>
 484 &0 < eta_y x #2.45 #2.45 /\ &0 < eta_y x (&2) #2.51 `,
 485 REWRITE_TAC[eta_y; eta_x] THEN
 486 LET_TR THEN
 487 NHANH (MESON[REAL_ARITH ` &0 <= #2.696`; REAL_LE_MUL2]`
 488   #2.696 <= x ==> #2.696 * #2.696 <= x * x `) THEN
 489 NHANH (REAL_ARITH ` #2.696 * #2.696 <= x * x ==>
 490   &0 < ((x * x) * (#2.45 * #2.45) * #2.45 * #2.45) /\
 491   &0 < ((x * x) * (&2 * &2) * #2.51 * #2.51) `) THEN
 492 MESON_TAC[IM_UP_POS; REAL_LT_DIV; SQRT_POS_LT]);;
 493
 494
 495 let REAL_LE_RDIV_0 = prove(` ! a b. &0 < b ==> ( &0 <= a / b <=> &0 <= a ) `,
 496 REWRITE_TAC[REAL_ARITH ` &0 <= a <=> &0 < a \/ a = &0 `] THEN
 497 SIMP_TAC[REAL_LT_RDIV_0] THEN
 498 SIMP_TAC[REAL_FIELD `&0 < b ==> ( a / b = &0 <=> a = &0 ) `]);;
 499
 500
 501 let NHSJMDH = prove(` ! y. #2.696 <= y /\ y <= sqrt8 ==>
 502      eta_y y (&2) (#2.51) <= eta_y y #2.45 (#2.45) `,
 503 NHANH (SPEC_ALL Q_TR) THEN
 504 ONCE_REWRITE_TAC[MESON[]` a /\ b ==> c <=> a ==> b ==> c `] THEN
 505 NHANH (MESON[REAL_ARITH ` &0 <= #2.696`; REAL_LE_MUL2]`
 506   #2.696 <= x ==> #2.696 * #2.696 <= x * x `)  THEN
 507 REWRITE_TAC[POW_2] THEN
 508 NHANH (REAL_ARITH `#2.696 * #2.696 <= y ==> &0 < y `) THEN
 509 REWRITE_TAC[REAL_ARITH ` a * b <= &0 <=> &0 <= a * -- b `] THEN
 510 SIMP_TAC[REAL_LE_MUL_EQ] THEN
 511 ONCE_REWRITE_TAC[MESON[]`( a/\b ) /\ c <=> ( a /\ c ) /\ b `] THEN
 512 NHANH (SPEC_ALL IMP_ETAY_POS) THEN
 513 NHANH (REAL_ARITH ` &0 < eta_y a b c ==> ~(eta_y a b c = &0 ) `) THEN
 514 REWRITE_TAC[GSYM REAL_POSSQ] THEN SIMP_TAC[REAL_FIELD ` &0 < a /\
 515  &0 < b ==>  -- (&1 / a - &1 / b) = (a - b) / ( a * b ) `] THEN
 516 PHA THEN SIMP_TAC[REAL_LT_MUL; REAL_LE_RDIV_0] THEN
 517 REWRITE_TAC[GSYM REAL_DIFFSQ] THEN
 518 SIMP_TAC[REAL_LT_ADD; REAL_LE_MUL_EQ] THEN REAL_ARITH_TAC);;
 519
 520 (* NEW WORKS *)
 521 let SQRT8_LE = MESON[ REAL_ARITH ` &0 <= &8`; SQRT_WORKS]` &0 <= sqrt (&8) `;;
 522
 523 let RELATE_POW2 = prove(` ( a = &0 <=> a pow 2 = &0 ) /\
 524   ( &0 < a pow 2 <=> &0 < a \/ ~( &0 <= a )) `,
 525 MP_TAC (REAL_FIELD ` a = &0 <=> a pow 2 = &0 `) THEN DISCH_TAC THEN
 526 CONJ_TAC THENL [ASM_SIMP_TAC[]; MP_TAC REAL_LE_POW_2] THEN
 527 MP_TAC (REAL_ARITH `( ! a. &0 < a \/ ~(&0 <= a) \/ a = &0 )`) THEN
 528 MP_TAC (REAL_FIELD ` a = &0 <=> a pow 2 = &0 `) THEN
 529 REWRITE_TAC[REAL_ARITH ` A <= b <=> A = b \/ A < b `] THEN
 530 MESON_TAC[REAL_ARITH ` ~ ( a = &0 /\ ( &0 < a \/ ~( &0 <= a ) )) `]);;
 531
 532 let LT_POW2_COND = prove(`!a b. &0 <= a /\ &0 <= b ==> (a < b <=> a pow 2 < b pow 2)`,
 533 REPEAT GEN_TAC THEN ASM_CASES_TAC ` a = &0 ` THENL
 534 [ASM_SIMP_TAC[REAL_ARITH` &0 pow 2 = &0 `] THEN MESON_TAC[RELATE_POW2];
 535 ASM_SIMP_TAC[REAL_LE_LT]] THEN STRIP_TAC THENL [ASM_MESON_TAC[LT_POW2_EQ_LT];
 536 EXPAND_TAC "b"] THEN UNDISCH_TAC `&0 < a ` THEN REWRITE_TAC[REAL_ARITH `
 537  &0 pow 2 = &0 /\ (a < &0 <=> ~(&0 <= a))`] THEN MP_TAC REAL_LE_POW_2 THEN
 538 MESON_TAC[REAL_LT_IMP_LE]);;
 539
 540
 541 let POS_IMP_POW2 = MESON[REAL_LE_TRANS; POW2_COND]` &0 <= a /\ a <= b ==> a pow 2
 542   <= b pow 2 `;;
 543
 544
 545 let SQRT8_LE_EQ_8_LESS_POW2 = prove(` sqrt (&8 ) <= a ==> &8 <= a pow 2 `,
 546 MP_TAC SQRT8_LE THEN MESON_TAC[SQRT8_POW2; POS_IMP_POW2]);;
 547
 548
 549 let MINIMAL_QUADRATIC_POLY =  prove(`
 550 ! b c (x:real). ( &4 * c - b pow 2 ) / &4 <= x pow 2 + b * x + c `,
 551 ONCE_REWRITE_TAC[REAL_ARITH ` a <= b <=> &0 <= b - a `] THEN
 552 REWRITE_TAC[REAL_ARITH ` (x pow 2 + b * x + c) - (&4 * c - b pow 2) / &4
 553   = ( x + b / &2 ) pow 2 `; REAL_LE_POW_2]);;
 554
 555 let GREATER_THAN_MID_QUADRATIC_PO = prove(` ! b c x x0. -- b / &2 <= x0 /\ x0 <= x ==>
 556   x0 pow 2 + b * x0 + c <= x pow 2 + b * x + c `,
 557 REWRITE_TAC[REAL_ARITH ` x0 pow 2 + b * x0 + c <= x pow 2 + b * x + c
 558   <=> &0 <= ( x - x0 ) * ( x + x0 + b ) `] THEN
 559 MESON_TAC[REAL_ARITH ` --b / &2 <= x0 /\ x0 <= x ==>
 560   &0 <= x - x0 /\ &0 <= x + x0 + b `; REAL_LE_MUL]);;
 561
 562 (* PERMAINENCE *)
 563 (* MARCH WORKS *)
 564
 565 let SQRT8_TWO_TWO = prove(` sqrt (&8) <= &2 + &2 `,
 566 MP_TAC SQRT8_LE THEN NHANH (MESON[REAL_ARITH ` &0 <= &2 + &2 `]
 567 `&0 <= sqrt (&8) ==> &0 <= &2 + &2 `) THEN SIMP_TAC[POW2_COND] THEN
 568 SIMP_TAC[REAL_ARITH ` &0 <= &8 `; SQRT_WORKS] THEN REAL_ARITH_TAC);;
 569
 570
 571 let A_POS_DELTA = prove(` &0 < delta (#3.2 pow 2 ) (sqrt8 pow 2 ) (&2 pow 2) (sqrt8 pow 2)
 572 (&2 pow 2) (&2 pow 2) `, REWRITE_TAC[delta; sqrt8; SQRT8_POW2] THEN REAL_ARITH_TAC);;
 573
 574 let MET_LAM_ROI = prove(` #3.2 < sqrt8 + &2 /\ #3.2 < &2 + &2 /\ sqrt8 < sqrt8 + &2 /\
 575 sqrt8 < &2 + &2 `,
 576 REWRITE_TAC[sqrt8; REAL_ARITH ` a < sqrt (&8) + b <=> a - b < sqrt (&8) `] THEN
 577 REWRITE_TAC[REAL_ARITH ` sqrt (&8) - &2 < sqrt (&8) `] THEN
 578 CONV_TAC REAL_RAT_REDUCE_CONV THEN MP_TAC SQRT8_LE  THEN
 579 MP_TAC (REAL_ARITH` &0 <= &6 / &5 /\ &0 <= &4 `) THEN
 580 SIMP_TAC[LT_POW2_COND ] THEN SIMP_TAC[LT_POW2_COND; SQRT8_POW2 ] THEN
 581 REAL_ARITH_TAC);;
 582
 583
 584 let PROVE_POS_THINGS = prove(` ! x. x IN {#3.2 , sqrt8, &2 , sqrt8, &2, &2 } ==> &0 <= x `,
 585 REWRITE_TAC[SET_RULE `( !x. x IN {a,b,c,d,s,e} ==> p x ) <=>
 586   p a /\ p b /\ p c /\ p d /\ p s /\ p e `;sqrt8;  SQRT8_LE] THEN REAL_ARITH_TAC);;
 587
 588
 589
 590 let IMP_GT_THAN_TWO = prove(` ! v1 v2 w1 (w2:real^3).
 591            CARD {v1, w1,v2, w2} = 4 /\
 592            packing {v1, w1,v2, w2}
 593 ==>       &2 <= dist3 w1 v2 /\
 594          &2 <= dist3 v2 w2 /\
 595          &2 <= dist3 v1 w2  `,
 596 REWRITE_TAC[CARD4; packing; GSYM dist3; sqrt8] THEN SET_TAC[]);;
 597
 598 (*       THADGSB         *)
 599
 600
 601 let LEMMA_FOR_PAHFWSI = prove(`! v1 v2 v3 v4. CARD {v1, v2, v3, v4} = 4 /\
 602          packing {v1, v2, v3, v4} /\
 603          dist (v1,v3) <= #3.2 /\
 604          #2.51 <= dist (v1,v2) /\
 605          dist (v2,v4) <= #2.51
 606 ==>     (!x. x IN {#3.2, #2.51, &2, #2.51, &2, &2} ==> &0 <= x) /\
 607          #3.2 < #2.51 + &2 /\
 608          #3.2 < &2 + &2 /\
 609          #2.51 < #2.51 + &2 /\
 610          #2.51 < &2 + &2 /\
 611          &0 <
 612          delta (#3.2 pow 2) (#2.51 pow 2) (&2 pow 2) (#2.51 pow 2) (&2 pow 2)
 613          (&2 pow 2) /\
 614          CARD {v1, v2, v3, v4} = 4 /\
 615          #2.51 <= dist3 v1 v2 /\
 616          &2 <= dist3 v2 v3 /\
 617          &2 <= dist3 v3 v4 /\
 618          &2 <= dist3 v1 v4 /\
 619          dist3 v1 v3 <= #3.2 /\
 620          dist3 v2 v4 <= #2.51 `,
 621 REWRITE_TAC[SET_RULE ` (!x. x IN {a,b,c,d,e,f} ==> P x ) <=>
 622   P a /\ P b /\ P c /\ P d /\ P e /\ P f `; REAL_ARITH `
 623   &0 <= #2.51 /\
 624           &0 <= &2 /\
 625           &0 <= &2 /\
 626           &0 <= #3.2 /\
 627           &0 <= &2 /\
 628           &0 <= #2.51 /\ #2.51 < &2 + #2.51 /\
 629          #2.51 < &2 + &2 /\
 630          #3.2 < &2 + &2 /\
 631          #3.2 < #2.51 + &2 /\ #3.2 < &2 + #2.51 /\
 632          #2.51 < #2.51 + &2  `] THEN SIMP_TAC[GSYM dist3] THEN
 633 REWRITE_TAC[CARD4; packing; delta; dist3] THEN CONV_TAC REAL_RAT_REDUCE_CONV
 634 THEN SET_TAC[]);;
 635
 636 let LEMMA_OF_39 = prove(` ! (v1:real^3) v2 w1 w2.
 637          CARD {v1, v2, w1, w2} = 4 /\
 638          packing {v1, v2, w1, w2} /\
 639          dist (w1,w2) <= #2.51 /\
 640          dist (v1,v2) <= #3.07
 641 ==> (!x. x IN {#2.51, &2, &2, #3.07, &2, &2} ==> &0 <= x) /\
 642      #2.51 < &2 + &2 /\
 643      #2.51 < &2 + &2 /\
 644      #3.07 < &2 + &2 /\
 645      #3.07 < &2 + &2 /\
 646      &0 <
 647      delta (#2.51 pow 2) (&2 pow 2) (&2 pow 2) (#3.07 pow 2) (&2 pow 2)
 648      (&2 pow 2) /\
 649      CARD {w1, v1, w2, v2} = 4 /\
 650      &2 <= dist3 w1 v1 /\
 651      &2 <= dist3 v1 w2 /\
 652      &2 <= dist3 w2 v2 /\
 653      &2 <= dist3 w1 v2 /\
 654      dist3 w1 w2 <= #2.51 /\
 655      dist3 v1 v2 <= #3.07 `,
 656 REWRITE_TAC[SET_RULE ` (!x. x IN {a,b,c,d,e,f} ==> P x ) <=>
 657   P a /\ P b /\ P c /\ P d /\ P e /\ P f `; delta; GSYM dist3] THEN CONV_TAC
 658 REAL_RAT_REDUCE_CONV THEN REPEAT GEN_TAC THEN STRIP_TAC THEN CONJ_TAC THENL
 659 [ASM_MESON_TAC[SET_RULE ` {v1, v2, w1, w2} = {w1, v1, w2, v2}`];DOWN_TAC]
 660  THEN REWRITE_TAC[CARD4; packing; dist3] THEN SET_TAC[]);;
 661
 662 let LEMMA_OF_LEMMA40 = prove(`! v1 v2 w1 (w2:real^3).  CARD {v1, v2, w1, w2} = 4 /\
 663          packing {v1, v2, w1, w2} /\
 664          dist (v1,v2) <= #3.2 /\
 665          dist (w1,w2) <= #2.51 /\
 666          #2.2 <= dist (v1,w1)
 667 ==> (!x. x IN {#3.2, #2.2, &2, #2.51, &2, &2} ==> &0 <= x) /\
 668      #3.2 < #2.2 + &2 /\
 669      #3.2 < &2 + &2 /\
 670      #2.51 < #2.2 + &2 /\
 671      #2.51 < &2 + &2 /\
 672      &0 <
 673      delta (#3.2 pow 2) (#2.2 pow 2) (&2 pow 2) (#2.51 pow 2) (&2 pow 2)
 674      (&2 pow 2) /\
 675      CARD {v1, w1, v2, w2} = 4 /\
 676      #2.2 <= dist3 v1 w1 /\
 677      &2 <= dist3 w1 v2 /\
 678      &2 <= dist3 v2 w2 /\
 679      &2 <= dist3 v1 w2 /\
 680      dist3 v1 v2 <= #3.2 /\
 681      dist3 w1 w2 <= #2.51 `,
 682 REWRITE_TAC[SET_RULE ` (! x. x IN {a,b,c,d,e,f} ==> P x ) <=>
 683   P a /\ P b /\ P c /\ P d /\ P e /\ P f `; delta] THEN
 684 CONV_TAC REAL_RAT_REDUCE_CONV THEN SIMP_TAC[SET_RULE `
 685 {v1, v2, w1, w2} = {v1, w1, v2, w2} `; packing] THEN
 686 SIMP_TAC[CARD4; GSYM dist3] THEN SET_TAC[]);;
 687
 688 let LEOF41 = prove(
 689 `#3.114467 < x ==> delta (#2.51 pow 2) (&2 pow 2) (&2 pow 2) (&2 pow 2)
 690  (&2 pow 2) (x pow 2) < &0`,
 691 NHANH (MESON[REAL_ARITH ` #3.114467 < x ==> &0 < #3.114467 /\ &0 < x `;
 692   LT_POW2_EQ_LT]` #3.114467 < x ==> ( #3.114467 ) pow 2 < x pow 2 `) THEN
 693 REWRITE_TAC[delta] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
 694 REWRITE_TAC[ REAL_POLY_CONV ` -- &126002 / &625 - &4 * &4 * x pow 2 - &4 * &4 * x pow 2 +
 695      &63001 / &10000 *     x pow 2 *
 696      (-- &63001 / &10000 + &4 + &4 + &4 + &4 - x pow 2) +
 697      &4 * &4 * (&23001 / &10000 + &4 + &0 + x pow 2) +
 698      &4 * &4 * (&63001 / &10000 + -- &4 + &4 + x pow 2) `] THEN
 699 REWRITE_TAC[REAL_ARITH ` a pow 4 = a pow 2 pow 2 `] THEN
 700 REWRITE_TAC[REAL_ARITH ` a * x pow 2 + b * x = ( a * x + b ) * x `] THEN
 701 NHANH (REAL_ARITH `&9699904694089 / &1000000000000 < x pow 2
 702      ==> -- &63001 / &10000 * x pow 2 + &6111033999 / &100000000 < &0` ) THEN
 703 NHANH (REAL_ARITH `&9699904694089 / &1000000000000 < x ==> &0 < x `) THEN
 704 REWRITE_TAC[REAL_ARITH ` a < &0 <=> &0 < -- a `;
 705   REAL_ARITH ` -- ( a * b ) = -- a * b `] THEN MESON_TAC[REAL_LT_MUL]);;
 706
 707
 708 let LEMMA41 = prove(`! v1 v2 v3 (v4:real^3).
 709  CARD {v1,v2,v3,v4} = 4 /\
 710  dist3 v1 v2 = #2.51 /\
 711          dist3 v1 v3 = &2 /\
 712          dist3 v1 v4 = &2 /\
 713          dist3 v2 v3 = &2 /\
 714          dist3 v2 v4 = &2
 715          ==> dist3 v3 v4 <= #3.114467 `,
 716 REPEAT GEN_TAC THEN MP_TAC LEMMA3 THEN LET_TR THEN
 717 REWRITE_TAC[REAL_ARITH ` x <= #3.114467 <=> ~ (#3.114467 < x ) `] THEN
 718 REWRITE_TAC[REAL_ARITH ` x <= #3.114467 <=> ~ (#3.114467 < x ) `;
 719    MESON[]` a ==> ~ b <=> a /\ b ==> F `] THEN PHA THEN
 720 NHANH (SPEC_ALL (prove(`! (v1:real^3) v2 v3 v4. dist3 v1 v2 = #2.51 /\
 721 dist3 v1 v3 = &2 /\ dist3 v1 v4 = &2 /\ dist3 v2 v3 = &2 /\ dist3 v2 v4 = &2 /\
 722 #3.114467 < dist3 v3 v4 ==> delta (dist (v1,v2) pow 2) (dist (v1,v3) pow 2)
 723 (dist (v1,v4) pow 2) (dist (v2,v3) pow 2) (dist (v2,v4) pow 2)
 724  (dist (v3,v4) pow 2) < &0 `, SIMP_TAC[dist3] THEN MESON_TAC[LEOF41]))) THEN
 725 REWRITE_TAC[REAL_ARITH ` a < &0 <=> ~( &0 <= a ) `; dist3] THEN MESON_TAC[]);;
 726
 727 let YXWIPMH = LEMMA41;;
 728
 729 let LEMMA_OF_L42 = prove(`sqrt8 <= dist3 v2 v4 /\ #3.488 <= x
 730  ==> -- &1 * x pow 2 * dist3 v2 v4 pow 2 +
 731      -- &1 * x pow 4 +
 732      &103001 / &5000 * x pow 2 +
 733      -- &529046001 / &100000000 <
 734      &0`,
 735 MP_TAC SQRT8_LE THEN
 736 IMP_IMP_TAC THEN
 737 NHANH (MESON[REAL_ARITH ` &0 <= a /\ a <= b /\ #3.488 <= x ==> &0 <= b /\
 738   &0 <= #3.488 /\ &0 <= x `; POW2_COND]`
 739   &0 <= a /\ a <= b /\ #3.488 <= x ==> a pow 2 <= b pow 2 /\
 740   #3.488 pow 2 <= x pow 2 `) THEN
 741 REWRITE_TAC[SQRT8_POW2; sqrt8] THEN
 742 NHANH (MESON[REAL_ARITH ` &0 <= a /\ a <= b /\ #3.488 <= x ==> &0 <= b /\
 743   &0 <= #3.488 /\ &0 <= x `; POW2_COND]`
 744   &0 <= a /\ a <= b /\ #3.488 <= x ==> a pow 2 <= b pow 2 /\
 745   #3.488 pow 2 <= x pow 2 `) THEN
 746 REWRITE_TAC[SQRT8_POW2] THEN
 747 NHANH (MESON[REAL_ARITH ` &0 <= &8 /\ &0 <= #3.488 pow 2 `; REAL_LE_MUL2]` &8 <= a /\
 748  #3.488 pow 2 <= b ==> &8 * #3.488 pow 2 <= a * b `) THEN
 749 REWRITE_TAC[REAL_ARITH` a pow 4 = a pow 2 pow 2 `] THEN
 750 NHANH (MESON[REAL_ARITH ` #3.488 pow 2 <= x ==> &0 <= #3.488 pow 2 /\
 751   &0 <= x `; POW2_COND]` #3.488 pow 2 <= x ==> #3.488 pow 2 pow 2 <= x pow 2 `) THEN
 752 REWRITE_TAC[REAL_ARITH ` a + -- &1 * x pow 2 + b * x + c =
 753   a + -- &1 * ( x pow 2 + -- b * x + -- c ) `] THEN
 754 NHANH (prove(` #3.488 pow 2 <= x pow 2 ==>
 755   #3.488 pow 2 pow 2 +
 756       --(&103001 / &5000) * #3.488 pow 2 +
 757       --(-- &529046001 / &100000000) <= x pow 2 pow 2 +
 758       --(&103001 / &5000) * x pow 2 +
 759       --(-- &529046001 / &100000000) `,
 760 MP_TAC (REAL_ARITH ` -- (  --(&103001 / &5000))  / &2 <= #3.488 pow 2 `) THEN
 761 MESON_TAC[GREATER_THAN_MID_QUADRATIC_PO ])) THEN
 762 REAL_ARITH_TAC);;
 763
 764
 765
 766 let LEMMA_IN_LEMMA42_P25 = prove(` ! v1 v2 v3 v4 x.
 767             dist3 v1 v2 = #2.51 /\
 768             dist3 v1 v4 = #2.51 /\
 769             dist3 v2 v3 = &2 /\
 770             dist3 v3 v4 = &2 /\
 771             sqrt8 <= dist3 v2 v4 /\
 772             #3.488 <= x
 773 ==>   delta (dist3 v1 v2 pow 2) ( x pow 2) (dist3 v1 v4 pow 2)
 774       (dist3 v2 v3 pow 2)
 775       (dist3 v2 v4 pow 2)
 776       (dist3 v3 v4 pow 2) < &0 `,
 777 SIMP_TAC[] THEN
 778 NHANH (MESON[REAL_ARITH` #3.488 <= x ==> &0 <= #3.488 /\ &0 <= x `; POW2_COND]`
 779   #3.488 <= x ==> (#3.488 pow 2 <= x pow 2 ) `) THEN
 780 REWRITE_TAC[delta] THEN
 781 CONV_TAC REAL_RAT_REDUCE_CONV THEN
 782 REWRITE_TAC[REAL_POLY_CONV `--(&63001 / &10000 * x pow 2 * &4) -
 783          &63001 / &10000 * &63001 / &10000 * dist3 v2 v4 pow 2 -
 784          x pow 2 * &63001 / &2500 -
 785          &4 * dist3 v2 v4 pow 2 * &4 +
 786          &63001 / &10000 *
 787          &4 *
 788          (-- &63001 / &10000 +
 789           x pow 2 +
 790           &63001 / &10000 +
 791           &4 +
 792           dist3 v2 v4 pow 2 - &4) +
 793          x pow 2 *
 794          dist3 v2 v4 pow 2 *
 795          (&63001 / &10000 - x pow 2 +
 796           &63001 / &10000 +
 797           &4 - dist3 v2 v4 pow 2 +
 798           &4) +
 799          &63001 / &10000 *
 800          &4 *
 801          (&63001 / &10000 +
 802           x pow 2 - &63001 / &10000 - &4 +
 803           dist3 v2 v4 pow 2 +
 804           &4) `] THEN
 805 REWRITE_TAC[REAL_IDEAL_CONV [` y pow 2 `] `-- &1 * x pow 4 * y pow 2 +
 806          -- &1 * x pow 2 * y pow 4 +
 807          &103001 / &5000 * x pow 2 * y pow 2 +
 808          -- &529046001 / &100000000 * y pow 2 `] THEN
 809 REWRITE_TAC[MESON[]` a/\ #3.488 <= x /\ c <=> (a/\ #3.488 <= x )/\ c`] THEN
 810 NHANH (LEMMA_OF_L42) THEN
 811 REWRITE_TAC[sqrt8] THEN
 812 NHANH (SQRT8_LE_EQ_8_LESS_POW2) THEN
 813 REPEAT GEN_TAC THEN
 814 STRIP_TAC THEN
 815 UNDISCH_TAC ` &8 <= dist3 v2 v4 pow 2 ` THEN
 816 UNDISCH_TAC ` -- &1 * x pow 2 * dist3 v2 v4 pow 2 +
 817       -- &1 * x pow 4 +
 818       &103001 / &5000 * x pow 2 +
 819       -- &529046001 / &100000000 <
 820       &0 ` THEN
 821 ABBREV_TAC ` xx = (-- &1 * x pow 2 * dist3 v2 v4 pow 2 +
 822       -- &1 * x pow 4 +
 823       &103001 / &5000 * x pow 2 +
 824       -- &529046001 / &100000000)` THEN
 825 NHANH (REAL_ARITH ` &8 <= a ==> &0 < a `) THEN
 826 REWRITE_TAC[REAL_ARITH ` ( a * b < &0 <=> &0 < ( -- a ) * b )/\
 827   ( a < &0 <=> &0 < -- a )`] THEN
 828 SIMP_TAC[REAL_LT_MUL]);;
 829
 830 let PAATDXJ =prove(` ! v1 v2 v3 (v4:real^3).
 831          CARD {v1,v2,v3,v4} = 4 /\
 832          dist3 v1 v2 = #2.51 /\
 833          dist3 v1 v4 = #2.51 /\
 834          dist3 v2 v3 = &2 /\
 835          dist3 v3 v4 = &2 /\
 836          sqrt8 <= dist3 v2 v4
 837          ==> dist3 v1 v3 < #3.488 `,
 838 MP_TAC LEMMA3 THEN LET_TR THEN REWRITE_TAC[REAL_ARITH ` a < b <=> ~ ( b <= a )`]
 839 THEN REWRITE_TAC[MESON[]` a ==> ~ b <=> ~( a /\b)`] THEN
 840 PHA THEN NHANH (SPEC_ALL LEMMA_IN_LEMMA42_P25) THEN
 841 REWRITE_TAC[REAL_ARITH` a < b <=> ~(b <= a ) `] THEN SIMP_TAC[dist3]);;
 842
 843
 844 let CONVEX_NORMBALL = REWRITE_RULE[GSYM NORMBALL_BALL] CONVEX_BALL ;;
 845
 846 let CONVEX_HULL4 =
 847 SPEC `{(v1:real^N),v2,v3,v4}` CONVEX_HULL_FINITE;;
 848
 849 let CONVEX_HULL_4_EQUIV = prove(` ! v1 v2 v3 (v4:real^N).
 850   conv {v1,v2,v3,v4} = { x | ? a b c d.
 851   &0 <= a /\
 852           &0 <= b /\
 853           &0 <= c /\
 854           &0 <= d /\
 855           a + b + c + d = &1 /\
 856           a % v1 + b % v2 + c % v3 + d % v4 = x } `,
 857 REWRITE_TAC[conv; FUN_EQ_THM; affsign; lin_combo; UNION_EMPTY;
 858  IN_ELIM_THM; sgn_ge] THEN
 859 REWRITE_TAC[MESON[]` x = vsum aa bb /\ a /\ b <=>
 860   a /\ b /\ vsum aa bb = x `] THEN
 861 ONCE_REWRITE_TAC[SET_RULE ` a s ==> b <=> s IN a ==> b `] THEN
 862  SIMP_TAC[CONVEX_HULL_FINITE_STEP; FINITE_INSERT; FINITE_RULES] THEN
 863  REWRITE_TAC[REAL_ARITH `x - y = z:real <=> x = y + z`;
 864              VECTOR_ARITH `x - y = z:real^N <=> x = y + z`] THEN
 865  REWRITE_TAC[VECTOR_ADD_RID; REAL_ADD_RID] THEN MESON_TAC[IN]);;
 866
 867
 868 let TXDIACY = prove(`! (a:real^3) b c d (v0: real^3) r.
 869  {a, b, c, d} SUBSET normball v0 r
 870          ==> convex hull {a, b, c, d} SUBSET normball v0 r `,
 871 REPEAT GEN_TAC THEN MP_TAC (MESON[CONVEX_NORMBALL]` convex (normball (v0:real^3) r)`) THEN
 872 NHANH (MESON[FINITE6] ` {a, b, c, d} SUBSET s ==> FINITE {(a:real^3),b,c,d} `) THEN
 873 REWRITE_TAC[CONVEX_HULL4; CONVEX_EXPLICIT] THEN
 874 IMP_IMP_TAC THEN
 875 REWRITE_TAC[SET_RULE ` {a | P a } SUBSET b <=> (! a. P a ==> a IN b)`] THEN
 876 REWRITE_TAC[MESON[]` (! y. ( ? u. P u y ) ==> Q y ) <=>
 877   (! y u. P u y ==> Q y ) `] THEN
 878 REWRITE_TAC[MESON[]`(!y u. P u /\ Q u /\ R u = y ==> Z y) <=>
 879   (!u. P u /\ Q u ==> Z (R u)) `] THEN MESON_TAC[]);;
 880 let LEMMA14 = TXDIACY;;
 881
 882
 883 let ECSEVNC = prove(`?t1 t2 t3 t4.
 884      !v1 v2 v3 v4 (v: real^3).
 885          ~coplanar_alt {v1, v2, v3, v4}
 886          ==> t1 v1 v2 v3 v4 v +
 887              t2 v1 v2 v3 v4 v +
 888              t3 v1 v2 v3 v4 v +
 889              t4 v1 v2 v3 v4 v =
 890              &1 /\
 891              v =
 892              t1 v1 v2 v3 v4 v % v1 +
 893              t2 v1 v2 v3 v4 v % v2 +
 894              t3 v1 v2 v3 v4 v % v3 +
 895              t4 v1 v2 v3 v4 v % v4 /\
 896              (!ta tb tc td.
 897                   v = ta % v1 + tb % v2 + tc % v3 + td % v4 /\
 898                   ta + tb + tc + td = &1
 899                   ==> ta = t1 v1 v2 v3 v4 v /\
 900                       tb = t2 v1 v2 v3 v4 v /\
 901                       tc = t3 v1 v2 v3 v4 v /\
 902                       td = t4 v1 v2 v3 v4 v) `,
 903 REWRITE_TAC[GSYM SKOLEM_THM; RIGHT_EXISTS_IMP_THM] THEN REPEAT
 904 GEN_TAC THEN NHANH (SPEC_ALL (prove(`!v1 v2 v3 v0 v:real^3.
 905     ~coplanar_alt {v0, v1, v2, v3} ==> (?t1 t2 t3. v - v0 = t1 % (v1 - v0)
 906  + t2 % (v2 - v0) + t3 % (v3 - v0) /\ (!ta tb tc. v - v0 = ta % (v1 - v0)
 907  + tb % (v2 - v0) + tc % (v3 - v0)   ==> ta = t1 /\
 908  tb = t2 /\ tc = t3))`, SIMP_TAC[NONCOPLANAR_3_BASIS]))) THEN
 909 STRIP_TAC THEN EXISTS_TAC ` &1 - t1 - t2 - t3 ` THEN
 910 EXISTS_TAC ` t1:real ` THEN EXISTS_TAC ` t2:real ` THEN
 911 EXISTS_TAC ` t3:real ` THEN CONJ_TAC THENL [REAL_ARITH_TAC;
 912  CONJ_TAC] THENL [UNDISCH_TAC ` (v:real^3) - v1 = t1 % (v2 - v1) +
 913 t2 % (v3 - v1) + t3 % (v4 - v1)` THEN
 914 CONV_TAC VECTOR_ARITH; REPEAT GEN_TAC] THEN
 915 REWRITE_TAC[MESON[]` a /\ b ==> c <=> b ==> a ==> c `;
 916   REAL_ARITH ` ta + tb + tc + td = &1 <=> ta = &1 - tb - tc - td `] THEN
 917 SIMP_TAC[] THEN REWRITE_TAC[VECTOR_ARITH `   v = (&1 - tb - tc - td) % v1
 918  + tb % v2 + tc % v3 + td % v4 <=>  v - v1 = tb % ( v2 - v1 ) +
 919 tc % ( v3 - v1 ) + td % ( v4 - v1 ) `] THEN ASM_MESON_TAC[]);;
 920
 921 let LEMMA76 = ECSEVNC;;
 922
 923 let COEFS_4 = new_specification ["COEF4_1"; "COEF4_2"; "COEF4_3"; "COEF4_4"] ECSEVNC ;;
 924
 925 let COEF_1_EQ_ZERO = prove(` ! v1 v2 v3 v4 (v:real^3).
 926   ~ coplanar_alt {v1,v2,v3,v4} ==>
 927   ( COEF4_1 v1 v2 v3 v4 v = &0 <=> v IN aff {v2,v3,v4} ) `,
 928 REWRITE_TAC[aff; AFFINE_HULL_3; IN_ELIM_THM] THEN
 929 NHANH (SPEC_ALL COEFS_4) THEN
 930 REPEAT GEN_TAC THEN STRIP_TAC THEN
 931 ONCE_REWRITE_TAC[REAL_ARITH` u + v + w = &0 + u + v + w `] THEN
 932 ONCE_REWRITE_TAC[VECTOR_ARITH` u + v + w = &0 % v1 + u + v + w `] THEN
 933 ASM_MESON_TAC[]);;
 934
 935 let EQ_IMP_COPLANAR = prove(`! a b c (d:real^3). ( a = b \/ a = c \/ a = d )
 936  ==> coplanar_alt {a,b,c,d} `,
 937 REPEAT STRIP_TAC THENL [
 938 ASM_SIMP_TAC[SET_RULE ` a INSERT ( a INSERT s ) = a INSERT s `] THEN
 939 MP_TAC (DIMINDEX_3) THEN MESON_TAC[COPLANAR_3;  ARITH_RULE` a = 3 ==> 2 <= a `];
 940 ONCE_REWRITE_TAC[SET_RULE` {a,b,v,c} = {a,v,b,c} `] THEN
 941 ASM_SIMP_TAC[SET_RULE ` a INSERT ( a INSERT s ) = a INSERT s `] THEN
 942 MP_TAC (DIMINDEX_3) THEN MESON_TAC[COPLANAR_3;  ARITH_RULE` a = 3 ==> 2 <= a `];
 943 ONCE_REWRITE_TAC[SET_RULE` {a,b,v,c} = {a,c,v,b} `] THEN
 944 ASM_SIMP_TAC[SET_RULE ` a INSERT ( a INSERT s ) = a INSERT s `] THEN
 945 MP_TAC (DIMINDEX_3) THEN MESON_TAC[COPLANAR_3;  ARITH_RULE` a = 3 ==> 2 <= a `]]);;
 946
 947 let AFFINE_HULL_FINITE_STEP_GEN = prove
 948  (`!P:real^N->real->bool.
 949        ((?u. (!x. x IN {} ==> P x (u x)) /\
 950              sum {} u = w /\ vsum {} (\x. u(x) % x) = y) <=>
 951         w = &0 /\ y = vec 0) /\
 952        (FINITE(s:real^N->bool) /\
 953         (!y. a IN s /\ P a y ==> P a (y / &2)) /\
 954         (!x y. a IN s /\ P a x /\ P a y ==> P a (x + y))
 955         ==> ((?u. (!x. x IN (a INSERT s) ==> P x (u x)) /\
 956                   sum (a INSERT s) u = w /\
 957                   vsum (a INSERT s) (\x. u(x) % x) = y) <=>
 958              ?v u. P a v /\ (!x. x IN s ==> P x (u x)) /\
 959                    sum s u = w - v /\
 960                    vsum s (\x. u(x) % x) = y - v % a))`,
 961  GEN_TAC THEN SIMP_TAC[SUM_CLAUSES; VSUM_CLAUSES; NOT_IN_EMPTY] THEN
 962  CONJ_TAC THENL [MESON_TAC[]; ALL_TAC] THEN DISCH_TAC THEN
 963  ASM_CASES_TAC `(a:real^N) IN s` THEN ASM_REWRITE_TAC[] THENL
 964   [ASM_SIMP_TAC[SET_RULE `a IN s ==> a INSERT s = s`] THEN EQ_TAC THEN
 965    REWRITE_TAC[LEFT_IMP_EXISTS_THM] THENL
 966     [X_GEN_TAC `u:real^N->real` THEN STRIP_TAC THEN
 967      EXISTS_TAC `(u:real^N->real) a / &2` THEN
 968      EXISTS_TAC `\x:real^N. if x = a then u x / &2 else u x`;
 969      MAP_EVERY X_GEN_TAC [`v:real`; `u:real^N->real`] THEN
 970      STRIP_TAC THEN
 971      EXISTS_TAC `\x:real^N. if x = a then u x + v else u x`] THEN
 972    ASM_SIMP_TAC[] THEN (CONJ_TAC THENL [ASM_MESON_TAC[]; ALL_TAC]) THEN
 973    ONCE_REWRITE_TAC[COND_RAND] THEN ONCE_REWRITE_TAC[COND_RATOR] THEN
 974    ASM_SIMP_TAC[VSUM_CASES; SUM_CASES] THEN
 975    ASM_SIMP_TAC[GSYM DELETE; SUM_DELETE; VSUM_DELETE] THEN
 976    ASM_SIMP_TAC[SET_RULE `a IN s ==> {x | x IN s /\ x = a} = {a}`] THEN
 977    REWRITE_TAC[SUM_SING; VSUM_SING] THEN
 978    (CONJ_TAC THENL [REAL_ARITH_TAC; VECTOR_ARITH_TAC]);
 979    EQ_TAC THEN REWRITE_TAC[LEFT_IMP_EXISTS_THM] THENL
 980     [X_GEN_TAC `u:real^N->real` THEN STRIP_TAC THEN
 981      EXISTS_TAC `(u:real^N->real) a` THEN
 982      EXISTS_TAC `u:real^N->real` THEN ASM_SIMP_TAC[IN_INSERT] THEN
 983      REPEAT(FIRST_X_ASSUM(SUBST1_TAC o SYM)) THEN
 984      CONJ_TAC THENL [REAL_ARITH_TAC; VECTOR_ARITH_TAC];
 985      MAP_EVERY X_GEN_TAC [`v:real`; `u:real^N->real`] THEN
 986      STRIP_TAC THEN
 987      EXISTS_TAC `\x:real^N. if x = a then v:real else u x` THEN
 988      ASM_SIMP_TAC[IN_INSERT] THEN CONJ_TAC THENL
 989       [ASM_MESON_TAC[]; ALL_TAC] THEN
 990      ONCE_REWRITE_TAC[COND_RAND] THEN ONCE_REWRITE_TAC[COND_RATOR] THEN
 991      ASM_SIMP_TAC[VSUM_CASES; SUM_CASES] THEN
 992      ASM_SIMP_TAC[GSYM DELETE; SUM_DELETE; VSUM_DELETE] THEN
 993      ASM_SIMP_TAC[SET_RULE `~(a IN s) ==> {x | x IN s /\ x = a} = {}`] THEN
 994      ASM_SIMP_TAC[SET_RULE `~(a IN s) ==> s DELETE a = s`] THEN
 995      REWRITE_TAC[SUM_CLAUSES; VSUM_CLAUSES] THEN
 996      CONJ_TAC THENL [REAL_ARITH_TAC; VECTOR_ARITH_TAC]]]);;
 997
 998
 999
1000 let THEOREM_RE_AFF_LT31 = prove
1001  (`!v1 v2 v3 vv x:real^N.
1002        ~(v1 = vv) /\ ~(v2 = vv) /\ ~(v3 = vv)
1003        ==> ((?f. f vv < &0 /\
1004                  sum {v1, v2, v3, vv} f = &1 /\
1005                  x = vsum {v1, v2, v3, vv} (\v. f v % v)) <=>
1006             {x | ?a b c t.
1007                      a + b + c + t = &1 /\
1008                      x = a % v1 + b % v2 + c % v3 + t % vv /\
1009                      t < &0}
1010             x)`,
1011  REPEAT STRIP_TAC THEN MATCH_MP_TAC EQ_TRANS THEN
1012  EXISTS_TAC
1013   `?f. (!x:real^N. x IN {v1, v2, v3, vv} ==> vv = x ==> f x < &0) /\
1014        sum {v1, v2, v3, vv} f = &1 /\
1015        vsum {v1, v2, v3, vv} (\v. f v % v) = x` THEN
1016  CONJ_TAC THENL
1017   [ASM_REWRITE_TAC[FORALL_IN_INSERT; NOT_IN_EMPTY] THEN MESON_TAC[];
1018    SIMP_TAC[AFFINE_HULL_FINITE_STEP_GEN;
1019             REAL_ARITH `x < &0 /\ y < &0 ==> x + y < &0`;
1020             REAL_ARITH `x < &0 ==> x / &2 < &0`;
1021             FINITE_INSERT; CONJUNCT1 FINITE_RULES; RIGHT_EXISTS_AND_THM] THEN
1022    ASM_REWRITE_TAC[IN_ELIM_THM;
1023                    REAL_ARITH `x - y:real = z <=> x = y + z`;
1024                    VECTOR_ARITH `x - y:real^N = z <=> x = y + z`] THEN
1025    REWRITE_TAC[VECTOR_ADD_RID; REAL_ADD_RID] THEN MESON_TAC[]]);;
1026
1027 let AFF_LT31 = prove(` ! v1 v2 v3 (vv: real^N). ~ (vv IN {v1,v2,v3} ) ==>
1028 aff_lt {v1,v2,v3} {vv} =
1029    { x| ? a b c t. t < &0 /\ a + b + c + t = &1 /\
1030            x = a % v1 + b % v2 + c % v3 + t % vv } `,
1031 REWRITE_TAC[IN_SET3; DE_MORGAN_THM; aff_lt_def;FUN_EQ_THM;
1032  affsign; lin_combo; sgn_lt] THEN
1033 REWRITE_TAC[SET_RULE` {v1, v2, v3} UNION {vv} = {v1, v2, v3, vv}`] THEN
1034 REWRITE_TAC[SET_RULE` a /\ (!w. {vv} w ==> f w < &0) /\ b
1035   <=> f vv < &0 /\ b /\ a `] THEN
1036 SIMP_TAC[THEOREM_RE_AFF_LT31; IN_ELIM_THM] THEN SET_TAC[]);;
1037
1038 let AFF_LT21 = prove(`! a b (v0:real^N). ~ ( a = v0 ) /\ ~( b = v0 ) ==>
1039 aff_lt {a,b} {v0} =
1040           {x | ? ta tb t.
1041                    ta + tb + t = &1 /\
1042                    t < &0 /\
1043                    x = ta % a + tb % b + t % v0} `,
1044 REWRITE_TAC[SET_RULE` ~(a = v0) /\ ~(b = v0) <=>
1045   ~ ( v0 IN {a,b} ) `] THEN
1046 ONCE_REWRITE_TAC[SET_RULE` {a,b} = {a,b,b} `] THEN SIMP_TAC[AFF_LT31] THEN
1047 SIMP_TAC[AFF_LT31; FUN_EQ_THM; IN_ELIM_THM] THEN
1048 REWRITE_TAC[VECTOR_ARITH` a % b + c % b + x = ( a + c ) % b + x `] THEN
1049 MESON_TAC[REAL_ARITH` a + b + c = ( a + b ) + c `;
1050 VECTOR_ARITH ` a % v = ( a + &0 ) % v `; REAL_ARITH `
1051    a + b = a + &0 + b `]);;
1052
1053
1054 let INSET3 = SET_RULE` a IN {a,b,c} /\ b IN {a,b,c} /\ c IN {a,b,c} `;;
1055
1056 let AFF_GT33 = prove(`! (v1:real^N) v2 v3 w1 w2 w3.
1057      {v1, v2, v3} INTER {w1, w2, w3} = {}
1058      ==> aff_gt {v1, v2, v3} {w1, w2, w3} =
1059          {x | ?a1 a2 a3 b1 b2 b3.
1060                   &0 < b1 /\
1061                   &0 < b2 /\
1062                   &0 < b3 /\
1063                   a1 + a2 + a3 + b1 + b2 + b3 = &1 /\
1064                   x =
1065                   a1 % v1 + a2 % v2 + a3 % v3 + b1 % w1 + b2 % w2 + b3 % w3}`,
1066 REWRITE_TAC[aff_gt_def; FUN_EQ_THM; affsign; lin_combo; sgn_gt] THEN
1067 REPEAT STRIP_TAC THEN
1068 MATCH_MP_TAC EQ_TRANS  THEN
1069 REWRITE_TAC[SET_RULE ` ( a INSERT b ) UNION c =
1070    b UNION ( a INSERT c ) /\ {} UNION b = b `] THEN
1071 EXISTS_TAC ` (? f. x = vsum {v3, v2, v1, w1, w2, w3} (\v. f v % v) /\
1072            (!(w:real^N). w IN {v3,v2,v1, w1, w2, w3} ==> w IN {w1,w2,w3} ==>  &0 < f w) /\
1073            sum {v3, v2, v1, w1, w2, w3} f = &1 ) ` THEN
1074 REWRITE_TAC[SET_RULE` (!x. ({v1, v2, v3} INTER {w1, w2, w3}) x <=> {} x)
1075   <=> {v1, v2, v3} INTER {w1, w2, w3} = {} `] THEN
1076 CONJ_TAC THENL [
1077 FIRST_X_ASSUM MP_TAC THEN
1078 REWRITE_TAC[SET_RULE` (!x. ({v1, v2, v3} INTER {w1, w2, w3}) x <=> {} x)
1079   <=> {v1, v2, v3} INTER {w1, w2, w3} = {} `] THEN
1080 MESON_TAC[SET_RULE` {v1, v2, v3} INTER {w1, w2, w3} = {} ==>
1081   ( (!w. {w1, w2, w3} w ==> &0 < f w) <=>
1082   (!w. w IN {v3, v2, v1, w1, w2, w3}
1083                 ==> w IN {w1, w2, w3}
1084                 ==> &0 < f w) ) `];
1085 REWRITE_TAC[MESON[]` a /\ (!z. P z ) /\ aa = &1 <=>
1086   (!z. P z ) /\ aa = &1 /\ a `]] THEN
1087 ONCE_REWRITE_TAC[MESON[]` a = vsum b c <=> vsum b c = a `] THEN
1088  SIMP_TAC[AFFINE_HULL_FINITE_STEP_GEN;FINITE_INSERT; CONJUNCT1 FINITE_RULES;
1089             RIGHT_EXISTS_AND_THM;
1090             REAL_ARITH `&0 < x /\ &0 < y ==> &0 < x + y`;
1091             REAL_ARITH `&0 < x  ==> &0 < x / &2 `] THEN
1092 FIRST_X_ASSUM MP_TAC THEN
1093 REWRITE_TAC[SET_RULE` (!x. ({v1, v2, v3} INTER {w1, w2, w3}) x <=> {} x)
1094   <=> {v1, v2, v3} INTER {w1, w2, w3} = {} `; SET_RULE` ( a INSERT s ) INTER ss = {} <=>
1095 ~ ( a IN ss ) /\ s INTER ss = {} `] THEN
1096 SIMP_TAC[INSET3] THEN
1097 SIMP_TAC[INSET3; REAL_ARITH` a - b = c <=> a = b + c `;
1098   VECTOR_ARITH` a:real^N - b = c <=> a = b + c `] THEN
1099 REWRITE_TAC[ GSYM  RIGHT_EXISTS_AND_THM; ZERO_NEUTRAL;
1100  IN_ELIM_THM; VECTOR_ARITH ` a + vec 0 = a `] THEN
1101 DISCH_TAC THEN
1102 MESON_TAC[REAL_ARITH` a + b + c + d = c + b + a + d `;
1103   VECTOR_ARITH` ( a:real^N ) + b + c + d = c + b + a + d `]);;
1104
1105 let AFF_GE33 = prove_by_refinement(
1106 `! (v1:real^N) v2 v3 w1 w2 w3.
1107      {v1, v2, v3} INTER {w1, w2, w3} = {}
1108      ==> aff_ge {v1, v2, v3} {w1, w2, w3} =
1109          {x | ?a1 a2 a3 b1 b2 b3.
1110                   &0 <= b1 /\
1111                   &0 <= b2 /\
1112                   &0 <= b3 /\
1113                   a1 + a2 + a3 + b1 + b2 + b3 = &1 /\
1114                   x =
1115                   a1 % v1 + a2 % v2 + a3 % v3 + b1 % w1 + b2 % w2 + b3 % w3}`,
1116   (* {{{ proof *)
1117   [
1118   (REWRITE_TAC[aff_gt_def; aff_ge_def; FUN_EQ_THM; affsign; lin_combo; sgn_gt; sgn_ge]);
1119   (REPEAT STRIP_TAC);
1120   (MATCH_MP_TAC EQ_TRANS );
1121   (REWRITE_TAC[SET_RULE ` ( a INSERT b ) UNION c =   b UNION ( a INSERT c ) /\ {} UNION b = b `]);
1122   (EXISTS_TAC ` (? f. x = vsum {v3, v2, v1, w1, w2, w3} (\v. f v % v) /\           (!(w:real^N). w IN {v3,v2,v1, w1, w2, w3} ==> w IN {w1,w2,w3} ==>  &0 <= f w) /\           sum {v3, v2, v1, w1, w2, w3} f = &1 ) `);
1123   (CONJ_TAC);
1124     (FIRST_X_ASSUM MP_TAC);
1125     (REWRITE_TAC[SET_RULE` (!x. ({v1, v2, v3} INTER {w1, w2, w3}) x <=> {} x)  <=> {v1, v2, v3} INTER {w1, w2, w3} = {} `]);
1126     BY((MESON_TAC[SET_RULE` {v1, v2, v3} INTER {w1, w2, w3} = {} ==>  ( (!w. {w1, w2, w3} w ==> &0 <= f w) <=>  (!w. w IN {v3, v2, v1, w1, w2, w3}                ==> w IN {w1, w2, w3}                ==> &0 <= f w) ) `]));
1127   (REWRITE_TAC[MESON[]` a /\ (!z. P z ) /\ aa = &1 <=>  (!z. P z ) /\ aa = &1 /\ a `]);
1128   (ONCE_REWRITE_TAC[MESON[]` a = vsum b c <=> vsum b c = a `]);
1129   ( SIMP_TAC[AFFINE_HULL_FINITE_STEP_GEN;FINITE_INSERT; CONJUNCT1 FINITE_RULES; RIGHT_EXISTS_AND_THM; REAL_ARITH `&0 <= x /\ &0 <= y ==> &0 <= x + y`; REAL_ARITH `&0 <= x  ==> &0 <= x / &2 `]);
1130   (FIRST_X_ASSUM MP_TAC);
1131   (REWRITE_TAC[SET_RULE` (!x. ({v1, v2, v3} INTER {w1, w2, w3}) x <=> {} x)  <=> {v1, v2, v3} INTER {w1, w2, w3} = {} `; SET_RULE` ( a INSERT s ) INTER ss = {} <=> ~ ( a IN ss ) /\ s INTER ss = {} `]);
1132    (SIMP_TAC[INSET3]);
1133    (SIMP_TAC[INSET3; REAL_ARITH` a - b = c <=> a = b + c `; VECTOR_ARITH` a:real^N - b = c <=> a = b + c `]);
1134    (REWRITE_TAC[ GSYM RIGHT_EXISTS_AND_THM; ZERO_NEUTRAL; IN_ELIM_THM; VECTOR_ARITH ` a + vec 0 = a `]);
1135    (DISCH_TAC);
1136   BY( (MESON_TAC[REAL_ARITH` a + b + c + d = c + b + a + d `; VECTOR_ARITH` ( a:real^N ) + b + c + d = c + b + a + d `]))
1137   ]);;
1138   (* }}} *)
1139
1140
1141 let AFF_GE_12 = prove(`!v0 (a:real^N) b.
1142      ~(v0 = a \/ v0 = b)
1143      ==> aff_ge {v0} {a, b} =
1144          {x | ?tv ta tb.
1145                   &0 <= ta /\
1146                   &0 <= tb /\
1147                   tv + ta + tb = &1 /\
1148                   x = tv % v0 + ta % a + tb % b}`,
1149 REWRITE_TAC[SET_RULE ` ~(v0 = a \/ v0 = b) <=> {v0} INTER {a,b} = {} `] THEN
1150 ONCE_REWRITE_TAC[SET_RULE` {a} = {a,a} `] THEN
1151 ONCE_REWRITE_TAC[SET_RULE` {a,a} = {a,a,a} `] THEN
1152 ONCE_REWRITE_TAC[SET_RULE` {a,b,b,b} = {a,b,b} `] THEN
1153 SIMP_TAC[AFF_GE33] THEN REWRITE_TAC[FUN_EQ_THM; IN_ELIM_THM] THEN
1154 REPEAT STRIP_TAC THEN
1155 REWRITE_TAC[GSYM VECTOR_ADD_RDISTRIB; VECTOR_ARITH` a % v +
1156   b % v + y = ( a + b ) % v + y `] THEN GONTONG THEN EQ_TAC THENL [
1157 MESON_TAC[REAL_ARITH` a1 + a2 + a3 + b1 + b2 + b3 =
1158   ( a1 + a2 + a3 ) + b1 + b2 + b3 `; REAL_ARITH ` &0 <= a
1159 /\ &0 <= b ==> &0 <= a + b `];STRIP_TAC] THEN EXISTS_TAC` tv: real `
1160 THEN EXISTS_TAC` &0 ` THEN EXISTS_TAC` &0` THEN EXISTS_TAC` ta :real `
1161  THEN EXISTS_TAC` &0` THEN EXISTS_TAC` tb:real ` THEN
1162 ASM_SIMP_TAC[REAL_ARITH ` a <= a `; ZERO_NEUTRAL]);;
1163
1164
1165 let INSET3 = SET_RULE` a IN {a, b, c} /\ b IN {a, b, c} /\ c IN {a, b, c}
1166  /\ {a, b, c} a /\ {a, b, c} b /\ {a, b, c} c `;;
1167
1168
1169
1170 let AFF_LE_LT33 = prove(`! (v1:real^N) v2 v3 w1 w2 w3.
1171      {v1, v2, v3} INTER {w1, w2, w3} = {}
1172      ==> aff_le {v1, v2, v3} {w1, w2, w3} =
1173          {x | ?a1 a2 a3 b1 b2 b3.
1174                   b1 <= &0 /\
1175                   b2 <= &0  /\
1176                   b3 <= &0  /\
1177                   a1 + a2 + a3 + b1 + b2 + b3 = &1 /\
1178                   x =
1179                   a1 % v1 + a2 % v2 + a3 % v3 + b1 % w1 + b2 % w2 + b3 % w3} /\
1180    aff_lt {v1, v2, v3} {w1, w2, w3} =
1181          {x | ?a1 a2 a3 b1 b2 b3.
1182                   b1 < &0 /\
1183                   b2 < &0  /\
1184                   b3 < &0  /\
1185                   a1 + a2 + a3 + b1 + b2 + b3 = &1 /\
1186                   x =
1187                   a1 % v1 + a2 % v2 + a3 % v3 + b1 % w1 + b2 % w2 + b3 % w3} `,
1188 REWRITE_TAC[IN_ELIM_THM; aff_le_def; FUN_EQ_THM; aff_lt_def;
1189  affsign; lin_combo; sgn_lt; sgn_le] THEN
1190 REWRITE_TAC[SET_RULE` {v1, v2, v3} UNION {w1, w2, w3} =
1191   {v1,v2,v3,w1,w2,w3} `] THEN
1192 ONCE_REWRITE_TAC[SET_RULE` {w1, w2, w3} w ==> P w <=>
1193   w IN {v1,v2,v3,w1,w2,w3} ==> {w1,w2,w3} w ==> P w `] THEN
1194 REWRITE_TAC[MESON[]` a = vsum aa bb /\
1195   (! w. P w ) /\ b <=> (! w. P w ) /\ b /\ vsum aa bb = a `] THEN
1196  SIMP_TAC[AFFINE_HULL_FINITE_STEP_GEN;
1197             REAL_ARITH `( x < &0 /\ y < &0 ==> x + y < &0) /\ ( x <= &0 /\ y <= &0 ==> x + y <= &0)`;
1198             REAL_ARITH ` (x < &0 ==> x / &2 < &0 ) /\ (x <= &0 ==> x / &2 <= &0 )`;
1199             FINITE_INSERT; CONJUNCT1 FINITE_RULES
1200 ; RIGHT_EXISTS_AND_THM]  THEN
1201 SIMP_TAC[ GSYM RIGHT_EXISTS_AND_THM; SET_RULE `
1202   (!x. ({v1, v2, v3} INTER s ) x <=> {} x) <=>
1203   ~ ( s v1 ) /\ ~ ( s v2 ) /\ ~ ( s v3 ) `; INSET3] THEN
1204 REWRITE_TAC[REAL_ARITH` a - b = c <=> a = b + c`; REAL_ARITH `
1205   a + &0 = a `; VECTOR_ARITH` (a:real^N) - b = c <=> a = b + c`;
1206   VECTOR_ARITH` a + vec 0 = a `] THEN
1207 MESON_TAC[]);;
1208
1209
1210
1211
1212 let AFF_GES_LTS = prove(` ! a b c (v0 :real^N).
1213  ~ ( a = v0 ) /\ ~( b = v0 ) /\ ~( c = v0 ) ==>
1214 aff_gt {a, b} {v0} =
1215           {x | ?ta tb t.
1216                    ta + tb + t = &1 /\ &0 < t /\ x = ta % a + tb % b + t % v0} /\
1217 aff_ge {a, b} {v0} =
1218           {x | ?ta tb t.
1219                    ta + tb + t = &1 /\
1220                    &0 <= t /\
1221                    x = ta % a + tb % b + t % v0} /\
1222 aff_lt {a,b,c} {v0} =
1223    { x| ? ta tb tc t. t < &0 /\ ta + tb + tc + t = &1 /\
1224            x = ta % a + tb % b + tc % c + t % v0 }  /\
1225 aff_gt {a,b,c} {v0} =
1226    { x| ? ta tb tc t. &0 < t /\ ta + tb + tc + t = &1 /\
1227      x = ta % a + tb % b + tc % c + t % v0 } `,
1228 ONCE_REWRITE_TAC[SET_RULE` {a} = {a,a,a} `] THEN
1229 ONCE_REWRITE_TAC[SET_RULE` {a,b,b,b} = {a,b,b} `] THEN
1230 ONCE_REWRITE_TAC[SET_RULE` {a,b,c,c} = {a,b,c} `] THEN
1231 NHANH (SET_RULE` ~(a = v0) /\ ~(b = v0) /\ ~(c = v0) ==>
1232   {a,b,b} INTER {v0,v0,v0} = {} /\ {a,b,c} INTER {v0,v0,v0} = {} `) THEN
1233 SIMP_TAC[AFF_LE_LT33; AFF_GE33; AFF_GT33] THEN
1234 REWRITE_TAC[GSYM VECTOR_ADD_RDISTRIB; VECTOR_ARITH` a % x + b % x + y
1235   = ( a + b ) % x + y `] THEN
1236 REWRITE_TAC[REAL_ARITH` (a + b ) + c = a + b + c `] THEN
1237 REPEAT STRIP_TAC THENL [
1238 REWRITE_TAC[FUN_EQ_THM; IN_ELIM_THM] THEN GEN_TAC THEN
1239 EQ_TAC THENL [MESON_TAC[REAL_ARITH ` &0 < a /\ &0 < b ==> &0 < a + b `;
1240   REAL_ARITH ` a + b + c + d = a + ( b + c ) + d `];
1241 MESON_TAC[REAL_ARITH ` a + b + c = a + b / &2 + b / &2 + c / &3 +
1242   c / &3 + c / &3 `; REAL_ARITH` &0 < a <=> &0 < a / &3 `;
1243   REAL_ARITH` a = a / &2 + a / &2 /\ b = b / &3 + b / &3 + b / &3 /\ b =
1244  ( b / &3 + b / &3 ) + b / &3  `]];
1245 REPEAT STRIP_TAC THEN
1246 REWRITE_TAC[FUN_EQ_THM; IN_ELIM_THM] THEN GEN_TAC THEN
1247 EQ_TAC THENL [
1248 MESON_TAC[REAL_ARITH ` ( &0 < a /\ &0 < b ==> &0 < a + b ) /\ ( &0 <= a /\ &0 <= b ==> &0 <= a + b )  `;
1249   REAL_ARITH ` a + b + c + d = a + ( b + c ) + d `] ;
1250 MESON_TAC[REAL_ARITH ` a + b + c = a + b / &2 + b / &2 + c / &3 +
1251   c / &3 + c / &3 `; REAL_ARITH` ( &0 < a <=> &0 < a / &3) /\ ( &0 <= a <=> &0 <= a / &3) `;
1252   REAL_ARITH` a = a / &2 + a / &2 /\ b = b / &3 + b / &3 + b / &3 /\ b = ( b / &3 + b / &3 ) + b / &3  `]];
1253 REPEAT STRIP_TAC THEN
1254 REWRITE_TAC[FUN_EQ_THM; IN_ELIM_THM] THEN GEN_TAC THEN
1255 EQ_TAC THENL [MESON_TAC[REAL_ARITH ` ( &0 < a /\ &0 < b ==> &0 < a + b )
1256 /\ ( &0 <= a /\ &0 <= b ==> &0 <= a + b )  `; REAL_ARITH ` ( a < &0 /\ b < &0
1257 ==> a + b < &0 )`; REAL_ARITH ` a + b + c + d = a + ( b + c ) + d `]; STRIP_TAC] THEN
1258 EXISTS_TAC `ta :real` THEN
1259 EXISTS_TAC `tb :real` THEN
1260 EXISTS_TAC `tc :real` THEN
1261 REPEAT (EXISTS_TAC ` t / &3 `) THEN
1262 ASM_MESON_TAC[REAL_ARITH` a < &0 <=> a / &3 < &0 `;
1263   REAL_ARITH ` a = a / &3 + a / &3 + a / &3 `];
1264 REPEAT STRIP_TAC THEN
1265 REWRITE_TAC[FUN_EQ_THM; IN_ELIM_THM] THEN GEN_TAC THEN
1266 EQ_TAC THENL [MESON_TAC[REAL_ARITH ` ( &0 < a /\ &0 < b ==> &0 < a + b ) /\ ( &0 <= a /\ &0 <= b
1267  ==> &0 <= a + b )  `; REAL_ARITH ` ( a < &0 /\ b < &0 ==> a + b < &0 )`;
1268   REAL_ARITH ` a + b + c + d = a + ( b + c ) + d `]; STRIP_TAC] THEN
1269 EXISTS_TAC `ta :real` THEN
1270 EXISTS_TAC `tb :real` THEN
1271 EXISTS_TAC `tc :real` THEN
1272 REPEAT (EXISTS_TAC ` t / &3 `) THEN
1273 ASM_MESON_TAC[REAL_ARITH ` a = a / &3 + a / &3 + a / &3 `;
1274   REAL_ARITH ` &0 < a <=> &0 < a / &3 `]]);;
1275
1276
1277 let AFF_GES_GTS = prove(` ! a b c (v0:real^N).
1278 ~(a = v0) /\ ~(b = v0) /\ ~(c = v0)
1279      ==> aff_gt {a, b} {v0} =
1280                {x | ?ta tb t.
1281                         ta + tb + t = &1 /\
1282                         &0 < t /\
1283                         x = ta % a + tb % b + t % v0} /\
1284                aff_ge {a, b} {v0} =
1285                {x | ?ta tb t.
1286                         ta + tb + t = &1 /\
1287                         &0 <= t /\
1288                         x = ta % a + tb % b + t % v0} /\
1289                aff_lt {a, b, c} {v0} =
1290                {x | ?ta tb tc t.
1291                         t < &0 /\
1292                         ta + tb + tc + t = &1 /\
1293                         x = ta % a + tb % b + tc % c + t % v0} /\
1294                aff_gt {a, b, c} {v0} =
1295                {x | ?ta tb tc t.
1296                         &0 < t /\
1297                         ta + tb + tc + t = &1 /\
1298                         x = ta % a + tb % b + tc % c + t % v0} /\
1299          aff_ge {a, b, c} {v0} =
1300          {x | ?ta tb tc t.
1301                   &0 <= t /\
1302                   ta + tb + tc + t = &1 /\
1303                   x = ta % a + tb % b + tc % c + t % v0} `,
1304 REPEAT GEN_TAC THEN
1305 REWRITE_TAC[MESON[]` (a ==> a1 /\ a2 /\ a3 /\ a4 /\ a5) <=>
1306   ( a ==> a1 /\ a2 /\ a3 /\a4 ) /\ ( a ==> a5) `] THEN
1307 REWRITE_TAC[AFF_GES_LTS] THEN
1308 NHANH (SET_RULE` ~(a = v0) /\ ~(b = v0) /\ ~(c = v0)
1309   ==> {a,b,c} INTER {v0,v0,v0} = {} `) THEN
1310 ONCE_REWRITE_TAC[SET_RULE` {v} = {v,v,v} `] THEN
1311 ONCE_REWRITE_TAC[SET_RULE` {a, b, c, c, c} = {a,b,c} `] THEN
1312 SIMP_TAC[AFF_GE33] THEN
1313 REPEAT STRIP_TAC THEN
1314 REWRITE_TAC[FUN_EQ_THM; IN_ELIM_THM; GSYM VECTOR_ADD_RDISTRIB] THEN
1315 GEN_TAC THEN EQ_TAC THENL [
1316 MESON_TAC[REAL_ARITH` &0 <= a /\ &0 <= b ==> &0 <= a + b `];
1317 STRIP_TAC THEN
1318 EXISTS_TAC ` ta :real` THEN
1319 EXISTS_TAC ` tb :real` THEN
1320 EXISTS_TAC ` tc :real` THEN
1321 REPEAT ( EXISTS_TAC ` t / &3 `) THEN
1322 ASM_MESON_TAC[REAL_ARITH` a = a / &3 + a / &3 + a / &3 `;
1323   REAL_ARITH` &0 <= a <=> &0 <= a / &3 `]]);;
1324
1325
1326 let COEF_1_POS_NEG = prove(` ! v1 v2 v3 v4 (v:real^3).
1327   ~ coplanar_alt {v1,v2,v3,v4} ==>
1328   ( COEF4_1 v1 v2 v3 v4 v > &0 <=> v IN aff_gt {v2,v3,v4} {v1} ) /\
1329 ( COEF4_1 v1 v2 v3 v4 v < &0 <=> v IN aff_lt {v2,v3, v4} {v1} ) `,
1330 NHANH (MESON[EQ_IMP_COPLANAR]`~coplanar_alt {v1, v2, v3, v4} ==>
1331   ~ ( v2 = v1 ) /\ ~ ((v3:real^3) = v1 ) /\ ~ (v4 = v1 ) `) THEN
1332 SIMP_TAC[AFF_GES_LTS] THEN NHANH (SPEC_ALL COEFS_4) THEN
1333 REWRITE_TAC[IN_ELIM_THM; REAL_ARITH ` a > b <=> b < a `] THEN
1334 REPEAT GEN_TAC THEN STRIP_TAC THEN
1335 ONCE_REWRITE_TAC[REAL_ARITH ` a + b + c + t = t + a + b + c `] THEN
1336 ONCE_REWRITE_TAC[VECTOR_ARITH ` (a:real^N) + b + c + t = t + a + b + c `] THEN
1337 ASM_MESON_TAC[]);;
1338
1339
1340 let ALL_ABOUT_COEF_1 = prove(` ! v1 v2 v3 v4 (v:real^3).
1341   ~ coplanar_alt {v1,v2,v3,v4} ==>
1342   ( COEF4_1 v1 v2 v3 v4 v < &0 <=> v IN aff_lt {v2,v3, v4} {v1} ) /\
1343   ( COEF4_1 v1 v2 v3 v4 v = &0 <=> v IN aff {v2,v3,v4} ) /\
1344   ( COEF4_1 v1 v2 v3 v4 v > &0 <=> v IN aff_gt {v2,v3,v4} {v1} )`,
1345 SIMP_TAC[COEF_1_EQ_ZERO ; COEF_1_POS_NEG ]);;
1346
1347 let PER_COEF1_WITH_COEF2 = prove(`! v1 v2 v3 v4 (v:real^3).
1348  ~coplanar_alt {v1, v2, v3, v4} ==>
1349    COEF4_2 v1 v2 v3 v4 v = COEF4_1 v2 v3 v4 v1 v `,
1350 NHANH (SPEC_ALL COEFS_4) THEN
1351 REPEAT GEN_TAC THEN STRIP_TAC THEN
1352 MP_TAC (SPECL [` v2:real^3 `; `v3:real^3`; `v4:real^3`; ` v1:real^3`;
1353  `v:real^3 `] COEFS_4) THEN
1354 UNDISCH_TAC ` ~coplanar_alt {v1, v2, v3, (v4:real^3)}` THEN
1355 IMP_IMP_TAC THEN
1356 REWRITE_TAC[MESON[SET_RULE` {v1, v2, v3, v4} = {v2, v3, v4, v1}`]`
1357   ~coplanar_alt {v1, v2, v3, v4} /\
1358  (~coplanar_alt {v2, v3, v4, v1} ==> l ) <=> ~coplanar_alt {v1, v2, v3, v4}
1359   /\ l `] THEN
1360 ONCE_REWRITE_TAC[GSYM (REAL_ARITH` a + b + c + d = b + c + d + a `)] THEN
1361 ONCE_REWRITE_TAC[GSYM (VECTOR_ARITH` (a:real^N) + b + c + d = b + c + d + a `)] THEN
1362 ASM_MESON_TAC[]);;
1363
1364 let PER_COEF1_WITH_COEF3 = prove(`! v1 v2 v3 v4 (v:real^3).
1365  ~coplanar_alt {v1, v2, v3, v4} ==>
1366    COEF4_3 v1 v2 v3 v4 v = COEF4_1 v3 v4 v1 v2 v `,
1367 NHANH (SPEC_ALL COEFS_4) THEN
1368 REPEAT GEN_TAC THEN STRIP_TAC THEN
1369 MP_TAC (SPECL [`v3:real^3`; `v4:real^3`; ` v1:real^3`; ` v2:real^3`;
1370  `v:real^3 `] COEFS_4) THEN
1371 UNDISCH_TAC ` ~coplanar_alt {v1, v2, v3, (v4:real^3)}` THEN
1372 IMP_IMP_TAC THEN
1373 REWRITE_TAC[MESON[SET_RULE` {v1, v2, v3, v4} = {v3, v4, v1, v2}`]`
1374   ~coplanar_alt {v1, v2, v3, v4} /\
1375  (~coplanar_alt {v3, v4, v1, v2} ==> l ) <=> ~coplanar_alt {v1, v2, v3, v4}
1376   /\ l `] THEN
1377 ONCE_REWRITE_TAC[GSYM (REAL_ARITH` a + b + c + d = c + d + a + b`)] THEN
1378 ONCE_REWRITE_TAC[GSYM (VECTOR_ARITH` (a:real^N) + b + c + d = c + d + a + b`)]
1379  THEN ASM_MESON_TAC[]);;
1380
1381 let PER_COEF1_WITH_COEF4 = prove(`! v1 v2 v3 v4 (v:real^3).
1382  ~coplanar_alt {v1, v2, v3, v4} ==>
1383    COEF4_4 v1 v2 v3 v4 v = COEF4_1 v4 v1 v2 v3 v `,
1384 NHANH (SPEC_ALL COEFS_4) THEN
1385 REPEAT GEN_TAC THEN
1386 ONCE_REWRITE_TAC[SET_RULE` {v1, v2, v3, v4} = {v4,v1, v2, v3}`] THEN
1387 NHANH (SPEC_ALL COEFS_4) THEN
1388 MESON_TAC[REAL_ARITH` ta + tb + tc + td = td + ta + tb + tc`;
1389   VECTOR_ARITH` ta + tb + tc + td = td + ta + tb + (tc:real^N)`]);;
1390
1391 let ALL_ABOUT_COEF_2 = prove(` ! v1 v2 v3 v4 (v:real^3).
1392   ~ coplanar_alt {v1,v2,v3,v4} ==>
1393   ( COEF4_2 v1 v2 v3 v4 v < &0 <=> v IN aff_lt {v1,v3, v4} {v2} ) /\
1394   ( COEF4_2 v1 v2 v3 v4 v = &0 <=> v IN aff {v1,v3,v4} ) /\
1395   ( COEF4_2 v1 v2 v3 v4 v > &0 <=> v IN aff_gt {v1,v3,v4} {v2} )`,
1396 SIMP_TAC[PER_COEF1_WITH_COEF2] THEN MP_TAC ALL_ABOUT_COEF_1 THEN
1397 MESON_TAC[SET_RULE` {v1, v2, v3, v4} = {v2, v3, v4, v1}`;
1398 SET_RULE` {v1, v2, v3} = {v2, v3,v1}`]);;
1399
1400
1401
1402
1403 let ALL_ABOUT_COEF_3 = prove(` ! v1 v2 v3 v4 (v:real^3).
1404   ~ coplanar_alt {v1,v2,v3,v4} ==>
1405   ( COEF4_3 v1 v2 v3 v4 v < &0 <=> v IN aff_lt {v2,v1, v4} {v3} ) /\
1406   ( COEF4_3 v1 v2 v3 v4 v = &0 <=> v IN aff {v2,v1,v4} ) /\
1407   ( COEF4_3 v1 v2 v3 v4 v > &0 <=> v IN aff_gt {v2,v1,v4} {v3} ) `,
1408 SIMP_TAC[PER_COEF1_WITH_COEF3] THEN
1409 ONCE_REWRITE_TAC[SET_RULE` {v2, v1, v4} = {v4,v1,v2} `] THEN
1410 ONCE_REWRITE_TAC[SET_RULE` {v1, v4, v3, v2} = {v3,v4,v1,v2} `] THEN
1411 SIMP_TAC[ALL_ABOUT_COEF_1]);;
1412
1413 let SRGTIHY = prove(` ! v1 v2 v3 v4 (v:real^3).
1414   ~ coplanar_alt {v1,v2,v3,v4} ==>
1415   ( COEF4_1 v1 v2 v3 v4 v < &0 <=> v IN aff_lt {v2,v3, v4} {v1} ) /\
1416   ( COEF4_1 v1 v2 v3 v4 v = &0 <=> v IN aff {v2,v3,v4} ) /\
1417   ( COEF4_1 v1 v2 v3 v4 v > &0 <=> v IN aff_gt {v2,v3,v4} {v1} ) /\
1418   ( COEF4_2 v1 v2 v3 v4 v < &0 <=> v IN aff_lt {v1,v3, v4} {v2} ) /\
1419   ( COEF4_2 v1 v2 v3 v4 v = &0 <=> v IN aff {v1,v3,v4} ) /\
1420   ( COEF4_2 v1 v2 v3 v4 v > &0 <=> v IN aff_gt {v1,v3,v4} {v2} ) /\
1421   ( COEF4_3 v1 v2 v3 v4 v < &0 <=> v IN aff_lt {v2,v1, v4} {v3} ) /\
1422   ( COEF4_3 v1 v2 v3 v4 v = &0 <=> v IN aff {v2,v1,v4} ) /\
1423   ( COEF4_3 v1 v2 v3 v4 v > &0 <=> v IN aff_gt {v2,v1,v4} {v3} )/\
1424   ( COEF4_4 v1 v2 v3 v4 v < &0 <=> v IN aff_lt {v2,v1, v3} {v4} ) /\
1425   ( COEF4_4 v1 v2 v3 v4 v = &0 <=> v IN aff {v2,v1,v3} ) /\
1426   ( COEF4_4 v1 v2 v3 v4 v > &0 <=> v IN aff_gt {v2,v1,v3} {v4} )`,
1427 SIMP_TAC[ALL_ABOUT_COEF_1; ALL_ABOUT_COEF_2; ALL_ABOUT_COEF_3;
1428   PER_COEF1_WITH_COEF4] THEN
1429 ONCE_REWRITE_TAC[SET_RULE` {v2, v1, v3} = {v1,v2,v3}`] THEN
1430 ONCE_REWRITE_TAC[SET_RULE` {v1, v3, v2, v4} = {v4,v1,v2,v3}`] THEN
1431 SIMP_TAC[ALL_ABOUT_COEF_1]);;
1432 let LEMMA77 = SRGTIHY;;
1433
1434
1435  let CONV0_4 = prove
1436   (`conv0 {v1, v2, v3, v4} =
1437          {x:real^N | ?a b c d.
1438          &0 < a /\
1439          &0 < b /\
1440          &0 < c /\
1441          &0 < d /\
1442          a + b + c + d = &1 /\
1443          a % v1 + b % v2 + c % v3 + d % v4 = x}`,
1444    REWRITE_TAC[FUN_EQ_THM; IN_ELIM_THM] THEN X_GEN_TAC `y:real^N` THEN
1445    REWRITE_TAC[conv0; affsign; sgn_gt; lin_combo; UNION_EMPTY] THEN
1446    MATCH_MP_TAC EQ_TRANS THEN
1447    EXISTS_TAC
1448     `?f. (!w:real^N. w IN {v1, v2, v3, v4} ==> &0 < f w) /\
1449          sum {v1, v2, v3, v4} f = &1 /\
1450          vsum {v1, v2, v3, v4} (\v. f v % v) = y` THEN
1451    CONJ_TAC THENL [REWRITE_TAC[IN] THEN MESON_TAC[]; ALL_TAC] THEN
1452    SIMP_TAC[AFFINE_HULL_FINITE_STEP_GEN;
1453             REAL_ARITH `&0 < x /\ &0 < y ==> &0 < x + y`;
1454             REAL_ARITH `&0 < x ==> &0 < x / &2`;
1455             FINITE_INSERT; CONJUNCT1 FINITE_RULES; RIGHT_EXISTS_AND_THM] THEN
1456    ASM_REWRITE_TAC[IN_ELIM_THM;
1457                    REAL_ARITH `x - y:real = z <=> x = y + z`;
1458                    VECTOR_ARITH `x - y:real^N = z <=> x = y + z`] THEN
1459    REWRITE_TAC[VECTOR_ADD_RID; REAL_ADD_RID] THEN MESON_TAC[]);;
1460
1461 (* ======================= *)
1462 (* LEMMA 81 *)
1463 (* ======================= *)
1464
1465 let ARIKWRQ = prove(`! v1 v2 v3 (v4:real^3).
1466   let s = {v1,v2,v3,v4} in
1467   CARD s = 4 /\ ~ coplanar_alt s ==>
1468   conv s = aff_ge ( s DIFF {v1} ) {v1} INTER
1469   aff_ge ( s DIFF {v2} ) {v2} INTER
1470   aff_ge ( s DIFF {v3} ) {v3} INTER
1471   aff_ge ( s DIFF {v4} ) {v4} `, LET_TR THEN
1472 SIMP_TAC[CARD4; SET_RULE ` ~(v1 IN {v2, v3, v4}) /\ ~(v2 = v3 \/ v3 = v4 \/ v4 = v2)
1473   ==> {v1, v2, v3, v4} DIFF {v1} = {v2,v3,v4} /\
1474   {v1, v2, v3, v4} DIFF {v2} = {v3,v4,v1} /\
1475   {v1, v2, v3, v4} DIFF {v3} = {v4,v1,v2} /\
1476   {v1, v2, v3, v4} DIFF {v4} = {v1,v2,v3} `] THEN
1477 REWRITE_TAC[CARD4; IN_SET3;DE_MORGAN_THM] THEN
1478 SIMP_TAC[AFF_GES_GTS] THEN
1479 REWRITE_TAC[CONVEX_HULL_4_EQUIV] THEN
1480 REPEAT STRIP_TAC THEN
1481 REWRITE_TAC[SET_RULE ` a = b <=> (! x. x IN a <=> x IN b ) `;
1482   IN_INTER; IN_ELIM_THM] THEN
1483 GEN_TAC THEN EQ_TAC THENL [
1484 ASM_MESON_TAC[REAL_ARITH` a + b + c + d = d + a + b + c `;
1485   VECTOR_ARITH` (a:real^N) + b + c + d = d + a + b + c `];
1486 FIRST_X_ASSUM MP_TAC ] THEN
1487 NHANH (SPEC ` x: real^3` (GEN ` v:real^3` (SPEC_ALL COEFS_4))) THEN
1488 ABBREV_TAC ` aa = COEF4_1 v1 v2 v3 v4 x ` THEN
1489 ABBREV_TAC ` bb = COEF4_2 v1 v2 v3 v4 x ` THEN
1490 ABBREV_TAC ` cc = COEF4_3 v1 v2 v3 v4 x ` THEN
1491 ABBREV_TAC ` dd = COEF4_4 v1 v2 v3 v4 x ` THEN
1492 REWRITE_TAC[MESON[]` a ==> b ==> c <=> a /\ b ==> c `] THEN PHA THEN
1493 NHANH (MESON[REAL_ARITH` a + b + c + d = d + a + b + c `;
1494   VECTOR_ARITH` (a:real^N) + b + c + d = d + a + b + c `]`
1495 aa + bb + cc + dd = &1 /\
1496  x = aa % v1 + bb % v2 + cc % v3 + dd % v4 /\
1497  (!ta tb tc td.
1498       x = ta % v1 + tb % v2 + tc % v3 + td % v4 /\ ta + tb + tc + td = &1
1499       ==> ta = aa /\ tb = bb /\ tc = cc /\ td = dd) /\
1500  (?ta tb tc t.
1501       &0 <= t /\
1502       ta + tb + tc + t = &1 /\
1503       x = ta % v2 + tb % v3 + tc % v4 + t % v1) /\
1504  (?ta tb tc t.
1505       &0 <= t /\
1506       ta + tb + tc + t = &1 /\
1507       x = ta % v3 + tb % v4 + tc % v1 + t % v2) /\
1508  (?ta tb tc t.
1509       &0 <= t /\
1510       ta + tb + tc + t = &1 /\
1511       x = ta % v4 + tb % v1 + tc % v2 + t % v3) /\
1512  (?ta tb tc t.
1513       &0 <= t /\
1514       ta + tb + tc + t = &1 /\
1515       x = ta % v1 + tb % v2 + tc % v3 + t % v4)
1516  ==> &0 <= aa /\ &0 <= bb /\ &0 <= cc /\ &0 <= dd`) THEN
1517 MATCH_MP_TAC (MESON[]` ( a1 /\ a2 /\ a3 ==> l) ==>
1518   aa /\ ( a1 /\ a2 /\ a4 ) /\ a3 ==> l `) THEN MESON_TAC[]);;
1519
1520
1521
1522
1523
1524 (* ================ *)
1525 (* LEMMA 82 *)
1526 (* ================= *)
1527
1528
1529
1530
1531 let MXHKOXR = prove(`! v1 v2 v3 (v4:real^3). let s = {v1,v2,v3,v4} in
1532   CARD s = 4 /\ ~ coplanar_alt s ==>
1533   conv0 s = aff_gt ( s DIFF {v1} ) {v1} INTER
1534   aff_gt ( s DIFF {v2} ) {v2} INTER
1535   aff_gt ( s DIFF {v3} ) {v3} INTER
1536   aff_gt ( s DIFF {v4} ) {v4} `, LET_TR THEN
1537 SIMP_TAC[CARD4; SET_RULE ` ~(v1 IN {v2, v3, v4}) /\ ~(v2 = v3 \/ v3 = v4 \/ v4 = v2)
1538   ==> {v1, v2, v3, v4} DIFF {v1} = {v2,v3,v4} /\
1539   {v1, v2, v3, v4} DIFF {v2} = {v3,v4,v1} /\
1540   {v1, v2, v3, v4} DIFF {v3} = {v4,v1,v2} /\
1541   {v1, v2, v3, v4} DIFF {v4} = {v1,v2,v3} `] THEN
1542 REWRITE_TAC[CARD4; IN_SET3;DE_MORGAN_THM] THEN
1543 SIMP_TAC[AFF_GES_GTS; CONV0_4 ] THEN
1544 REPEAT STRIP_TAC THEN
1545 REWRITE_TAC[SET_RULE ` a = b <=> (! x. x IN a <=> x IN b ) `;
1546   IN_INTER; IN_ELIM_THM] THEN
1547 GEN_TAC THEN EQ_TAC THENL [
1548 ASM_MESON_TAC[REAL_ARITH` a + b + c + d = d + a + b + c `;
1549   VECTOR_ARITH` (a:real^N) + b + c + d = d + a + b + c `];
1550 FIRST_X_ASSUM MP_TAC ] THEN
1551 NHANH (SPEC ` x: real^3` (GEN ` v:real^3` (SPEC_ALL COEFS_4))) THEN
1552 ABBREV_TAC ` aa = COEF4_1 v1 v2 v3 v4 x ` THEN
1553 ABBREV_TAC ` bb = COEF4_2 v1 v2 v3 v4 x ` THEN
1554 ABBREV_TAC ` cc = COEF4_3 v1 v2 v3 v4 x ` THEN
1555 ABBREV_TAC ` dd = COEF4_4 v1 v2 v3 v4 x ` THEN
1556 REWRITE_TAC[MESON[]` a ==> b ==> c <=> a /\ b ==> c `] THEN PHA THEN
1557 NHANH (MESON[REAL_ARITH` a + b + c + d = d + a + b + c `;
1558   VECTOR_ARITH` (a:real^N) + b + c + d = d + a + b + c `]`
1559 aa + bb + cc + dd = &1 /\
1560  x = aa % v1 + bb % v2 + cc % v3 + dd % v4 /\
1561  (!ta tb tc td.
1562       x = ta % v1 + tb % v2 + tc % v3 + td % v4 /\ ta + tb + tc + td = &1
1563       ==> ta = aa /\ tb = bb /\ tc = cc /\ td = dd) /\
1564  (?ta tb tc t.
1565       &0 < t /\
1566       ta + tb + tc + t = &1 /\
1567       x = ta % v2 + tb % v3 + tc % v4 + t % v1) /\
1568  (?ta tb tc t.
1569       &0 < t /\
1570       ta + tb + tc + t = &1 /\
1571       x = ta % v3 + tb % v4 + tc % v1 + t % v2) /\
1572  (?ta tb tc t.
1573       &0 < t /\
1574       ta + tb + tc + t = &1 /\
1575       x = ta % v4 + tb % v1 + tc % v2 + t % v3) /\
1576  (?ta tb tc t.
1577       &0 < t /\
1578       ta + tb + tc + t = &1 /\
1579       x = ta % v1 + tb % v2 + tc % v3 + t % v4)
1580 ==> &0 < aa /\ &0 < bb /\ &0 < cc /\ &0 < dd `) THEN
1581 MATCH_MP_TAC (MESON[]` ( a1 /\ a2 /\ a3 ==> l) ==>
1582   aa /\ ( a1 /\ a2 /\ a4 ) /\ a3 ==> l `) THEN MESON_TAC[]);;
1583
1584
1585  let CONV0_4 = prove
1586   (`conv0 {v1, v2, v3, v4} =
1587          {x:real^N | ?a b c d.
1588          &0 < a /\
1589          &0 < b /\
1590          &0 < c /\
1591          &0 < d /\
1592          a + b + c + d = &1 /\
1593          a % v1 + b % v2 + c % v3 + d % v4 = x}`,
1594    REWRITE_TAC[FUN_EQ_THM; IN_ELIM_THM] THEN X_GEN_TAC `y:real^N` THEN
1595    REWRITE_TAC[conv0; affsign; sgn_gt; lin_combo; UNION_EMPTY] THEN
1596    MATCH_MP_TAC EQ_TRANS THEN
1597    EXISTS_TAC
1598     `?f. (!w:real^N. w IN {v1, v2, v3, v4} ==> &0 < f w) /\
1599          sum {v1, v2, v3, v4} f = &1 /\
1600          vsum {v1, v2, v3, v4} (\v. f v % v) = y` THEN
1601    CONJ_TAC THENL [REWRITE_TAC[IN] THEN MESON_TAC[]; ALL_TAC] THEN
1602    SIMP_TAC[AFFINE_HULL_FINITE_STEP_GEN;
1603             REAL_ARITH `&0 < x /\ &0 < y ==> &0 < x + y`;
1604             REAL_ARITH `&0 < x ==> &0 < x / &2`;
1605             FINITE_INSERT; CONJUNCT1 FINITE_RULES; RIGHT_EXISTS_AND_THM] THEN
1606    ASM_REWRITE_TAC[IN_ELIM_THM;
1607                    REAL_ARITH `x - y:real = z <=> x = y + z`;
1608                    VECTOR_ARITH `x - y:real^N = z <=> x = y + z`] THEN
1609    REWRITE_TAC[VECTOR_ADD_RID; REAL_ADD_RID] THEN MESON_TAC[]);;
1610
1611
1612 let CONV0_4POINTS = CONV0_4;;
1613
1614
1615
1616 (* ================== *)
1617 (* LEMMA 78 *)
1618
1619 (* ================== *)
1620
1621
1622 let ZRFMKPY = prove(` ! v1 v2 v3 v4 (v:real^3).
1623   ~coplanar_alt {v1, v2, v3, v4}
1624          ==> (v IN conv {v1, v2, v3, v4} <=>
1625               &0 <= COEF4_1 v1 v2 v3 v4 v /\
1626               &0 <= COEF4_2 v1 v2 v3 v4 v /\
1627               &0 <= COEF4_3 v1 v2 v3 v4 v /\
1628               &0 <= COEF4_4 v1 v2 v3 v4 v) /\
1629              (v IN conv0 {v1, v2, v3, v4} <=>
1630               &0 < COEF4_1 v1 v2 v3 v4 v /\
1631               &0 < COEF4_2 v1 v2 v3 v4 v /\
1632               &0 < COEF4_3 v1 v2 v3 v4 v /\
1633               &0 < COEF4_4 v1 v2 v3 v4 v) `,
1634 NHANH (SPEC_ALL COEFS_4) THEN REWRITE_TAC[CONVEX_HULL_4_EQUIV;
1635 CONV0_4POINTS; IN_ELIM_THM] THEN MESON_TAC[]);;
1636
1637 let LEMMA78 = ZRFMKPY;;
1638
1639
1640
1641 (* APRIL WORKS *)
1642 (* =========== *)
1643 (* NGUYEN QUANG TRUONG *)
1644 let IMP_TAC = IMP_IMP_TAC;;
1645
1646
1647
1648 let QUAANG_TRUOONN = prove(` ! v0 v1 v2 v3 (v4:real^N).
1649    CARD {v0, v1, v2, v3, v4} = 5 /\
1650          (?x. ~(x = v0) /\ x IN cone v0 {v1, v3} INTER cone v0 {v2, v4})
1651          ==> ~(conv {v1, v3} INTER cone v0 {v2, v4} = {})`,
1652 REWRITE_TAC[CONV_SET2; cone; CARD5; SET_RULE ` a INTER b = {} <=>
1653   ~ (? x. a x /\ b x ) `; GSYM aff_ge_def; IN; IN_INTER] THEN
1654 NHANH (SET_RULE ` ~{v1, v2, v3, v4} v0 ==>
1655   ~ ( v0 = v1 \/ v0 = v3 ) /\ ~ ( v0 = v2 \/ v0 = v4 ) `) THEN
1656 ONCE_REWRITE_TAC[MESON[]` a /\ b ==> c <=> a ==> b ==> c `] THEN
1657 SIMP_TAC[AFF_GE_12] THEN REWRITE_TAC[DE_MORGAN_THM] THEN
1658 REWRITE_TAC[IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN
1659 UNDISCH_TAC ` (x:real^N) = tv % v0 + ta % v1 + tb % v3` THEN
1660 UNDISCH_TAC ` (x:real^N) = tv' % v0 + ta' % v2 + tb' % v4` THEN
1661 REWRITE_TAC[MESON[]` x = a
1662  ==> x = (b:real^N) ==> c <=> x = a /\ a = b ==> c `] THEN
1663 REWRITE_TAC[VECTOR_ARITH` a % v + d = b % v + e <=>
1664   ( a - b ) % v + d = e `] THEN
1665 ASM_CASES_TAC ` &0 < ta + tb ` THENL [DOWN_TAC THEN
1666 REWRITE_TAC[MESON[VECTOR_MUL_LCANCEL; REAL_FIELD ` &0 < a ==> ~ ( &1 / a = &0 )`]`
1667   &0 < ta + tb /\ aaa /\
1668  aa = ta % v1 + tb % v3 <=> &0 < ta + tb /\ aaa /\
1669   &1 / ( ta + tb ) % aa = &1 / ( ta + tb ) % ( ta % v1 + tb % v3) `] THEN
1670 REWRITE_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC; REAL_ARITH `
1671   &1 / a * b = b / a `] THEN STRIP_TAC THEN DOWN_TAC THEN
1672 NHANH (MESON[REAL_LE_RDIV_0]`&0 <= ta /\ &0 <= tb /\ a1 /\ &0 <= ta' /\
1673  &0 <= tb' /\ a2 /\
1674  &0 < ta + tb /\ a3 ==> &0 <= ta / (ta + tb) /\ &0 <= tb / (ta + tb) /\
1675   &0 <= ta' / (ta + tb) /\ &0 <= tb' / (ta + tb) `) THEN ASM_MESON_TAC[
1676 REAL_FIELD` tv + ta + tb = &1 /\ tv' + ta' + tb' = &1 /\
1677   &0 < ta + tb ==> (tv' - tv) / (ta + tb) + ta' / (ta + tb) +
1678   tb' / (ta + tb) = &1 /\ ta / ( ta + tb ) + tb / ( ta + tb ) = &1`];
1679 DOWN_TAC THEN
1680 NHANH (MESON[REAL_ARITH` &0 <= a /\ &0 <= b /\ ~( &0 < a + b )
1681 ==> a = &0 /\ b = &0 `]`&0 <= ta /\ &0 <= tb /\a1/\a2 /\a3/\a4 /\
1682  ~(&0 < ta + tb) /\ a5 ==> ta = &0 /\ tb = &0`) THEN
1683 PURE_ONCE_REWRITE_TAC[MESON[]` P ta tb /\ ta = &0 /\ tb = &0
1684   <=> P ( &0 ) ( &0 ) /\ ta = &0 /\ tb = &0 `] THEN
1685 REWRITE_TAC[ZERO_NEUTRAL; VECTOR_MUL_LZERO; VECTOR_ADD_LID] THEN
1686 REWRITE_TAC[VECTOR_ARITH` (tv' - tv) % v + a = vec 0 <=> tv' % v + a
1687   = tv % v `; MESON[]` a = b /\ b = c <=> a = c /\ b = c `] THEN
1688 MESON_TAC[VECTOR_ARITH ` &1 % v = v `]]);;
1689
1690 (* le 80. p 51 *)
1691 (* ================ *)
1692
1693 let JVDAFRS = prove(` ! v0 v1 v2 v3 (v4:real^N).
1694    CARD {v0, v1, v2, v3, v4} = 5 /\
1695          (?x. ~(x = v0) /\ x IN cone v0 {v1, v3} INTER cone v0 {v2, v4})
1696          ==> ~(conv {v1, v3} INTER cone v0 {v2, v4} = {} /\
1697                conv {v2, v4} INTER cone v0 {v1, v3} = {})`, MESON_TAC[QUAANG_TRUOONN]);;
1698
1699 (* LEMMA 22 *)
1700 (* =========================== *)
1701
1702 let SQRT8_POS = MESON[REAL_ARITH ` &0 < &8 `; SQRT_POS_LT]` &0 < sqrt (&8) `;;
1703
1704 let SQRT8_LT_4_45 = prove(` sqrt8 < #4.45 `,
1705 SIMP_TAC[sqrt8; REAL_ARITH ` &0 < #4.45 `; MESON[REAL_ARITH ` &0 < &8 `;
1706 SQRT_POS_LT]` &0 < sqrt (&8) `; LT_POW2_EQ_LT; SQRT8_POW2] THEN REAL_ARITH_TAC);;
1707
1708
1709 let PROVE_NOT_COLLINEAR = prove(` ! v0 v1 (v2:real^3).
1710          &2 <= dist3 v0 v1 /\
1711          dist3 v0 v1 <= #2.51 /\
1712          #2.45 <= dist3 v1 v2 /\
1713          dist3 v1 v2 <= #2.51 /\
1714          #2.77 <= dist3 v0 v2 /\
1715          dist3 v0 v2 <= sqrt8
1716          ==> ~ collinear {v0, v1, v2}`,
1717 REWRITE_TAC[COLLINEAR_AS_IN_CONV2; MID_COND; dist3; LENGTH_EQ_EX; DE_MORGAN_THM] THEN
1718 SIMP_TAC[DIST_SYM] THEN
1719 REPEAT GEN_TAC THEN
1720 ABBREV_TAC ` a = dist(v0,v1:real^3)` THEN
1721 ABBREV_TAC ` b = dist(v0,v2:real^3)` THEN
1722 ABBREV_TAC ` c = dist(v1,v2:real^3)` THEN
1723 MP_TAC SQRT8_LT_4_45  THEN
1724 REAL_ARITH_TAC);;
1725
1726 let BPOW8APOW2CPOW2 = prove(`&2 <= a /\
1727  a <= #2.51 /\
1728  #2.45 <= c /\
1729  c <= #2.51 /\
1730  #2.77 <= b /\
1731  b <= sqrt8
1732 ==> b pow 2 <= &8 /\ a pow 2 <= #2.51 pow 2 /\ c pow 2 <= #2.51 pow 2 `,
1733 REWRITE_TAC[MESON[]` a1 /\ a2 /\a3 /\a4 /\a5 /\a6 ==> l <=>
1734   a1 /\a3 /\a5 ==> a2 /\a4 /\a6 ==> l `] THEN
1735 NHANH (REAL_ARITH`&2 <= a /\ #2.45 <= c /\ #2.77 <= b ==>
1736  &0 < a /\ &0 < b /\ &0 < c /\ &0 < #2.51 `) THEN
1737 SIMP_TAC[sqrt8; POW2_COND_LT; SQRT8_POS; SQRT8_POW2]);;
1738
1739 let IMP_PRE_LE_19 = prove(`&2 <= a /\
1740  a <= #2.51 /\
1741  #2.45 <= c /\
1742  c <= #2.51 /\
1743  #2.77 <= b /\
1744  b <= sqrt8
1745  ==> &0 < &2 /\
1746      &2 <= a /\
1747      &0 < #2.77 /\
1748      #2.77 <= b /\
1749      &0 < #2.45 /\
1750      #2.45 <= c /\
1751      a pow 2 <= #2.77 pow 2 + #2.45 pow 2 /\
1752      b pow 2 <= &2 pow 2 + #2.45 pow 2 /\
1753      c pow 2 <= &2 pow 2 + #2.77 pow 2 `,
1754 CONV_TAC REAL_RAT_REDUCE_CONV THEN NHANH (BPOW8APOW2CPOW2 ) THEN REAL_ARITH_TAC);;
1755
1756 (* ==================== *)
1757
1758 let LT_SQ8_IMP_LT2 = prove_by_refinement(
1759 ` a < sqrt (&8) ==> ~ ( &2 <= &1 / &2 * a ) `,
1760   (* {{{ proof *)
1761   [
1762   (ASM_CASES_TAC ` &0 <= a `);
1763     (UNDISCH_TAC `&0 <= a `);
1764     (SIMP_TAC[REAL_LT_IMP_LE; SQRT8_POS; LT_POW2_COND; REAL_ARITH `  &2 <= &1 / &2 * a <=> &4 <= a `; REAL_ARITH` &0 <= &4 `; POW2_COND; SQRT8_POW2]);
1765     BY((REAL_ARITH_TAC));
1766   (FIRST_X_ASSUM MP_TAC);
1767   BY((REAL_ARITH_TAC))
1768   ]);;
1769   (* }}} *)
1770
1771 (*
1772 let condC = new_definition ` condC M13 m12 m14 M24 m34 (m23:real) =
1773   ((! x. x IN {M13, m12, m14, M24, m34, m23 } ==> &0 <= x ) /\
1774   M13 <= m12 + m23 /\
1775   M13 <= m14 + m34 /\
1776   M24 < m12 + m14 /\
1777   M24 < m23 + m34 /\
1778   &0 <= delta (M13 pow 2) (m12 pow 2) (m14 pow 2) (M24 pow 2) (m34 pow 2 )
1779    (m23 pow 2 ) )`;;
1780
1781 let LE_FOR_LEMMA36 = prove(`(CARD {u, v, w} = 3 /\ packing {u, v, w} /\ dist (u,v) < sqrt8) /\
1782        ~(dist (u,v) / &2 < dist (w,&1 / &2 % (u + v))) ==>
1783   condC (sqrt (&8)) (&2) (&2) (sqrt (&8)) (&2) (&2) /\
1784      CARD {u, w, v, u + v - w} = 4 /\
1785      &2 <= dist3 u w /\
1786      &2 <= dist3 w v /\
1787      &2 <= dist3 v (u + v - w) /\
1788      &2 <= dist3 u (u + v - w) /\
1789      dist3 u v < sqrt (&8) /\
1790      dist3 w (u + v - w) <= sqrt (&8) `,
1791 REWRITE_TAC[condC; delta; SQRT8_POW2] THEN
1792 REWRITE_TAC[SET_RULE ` (! x. x IN ( a INSERT b ) ==> p x ) <=>
1793   p a /\ (! x. x IN b  ==> p x ) `; NOT_IN_EMPTY] THEN
1794 CONV_TAC REAL_RAT_REDUCE_CONV THEN
1795 SIMP_TAC[SQRT8_POS; REAL_LT_IMP_LE; dist3; sqrt8; packing] THEN
1796 SIMP_TAC[REAL_LT_IMP_LE; SQRT8_POS; LT_POW2_COND;
1797   REAL_ARITH ` &0 <= &4 `; POW2_COND; SQRT8_POW2] THEN
1798 CONV_TAC REAL_RAT_REDUCE_CONV THEN
1799 REWRITE_TAC[NORM_ARITH` dist (v,u + v - w) = dist (u,w) /\
1800   dist (u,u + v - w) = dist (v,w) /\
1801   dist (w,u + v - w) = &2 * dist (w,&1 / &2 % (u + v)) `] THEN
1802 STRIP_TAC THEN CONJ_TAC THENL [
1803 UNDISCH_TAC `CARD {(u:real^3), v, w} = 3` THEN
1804 REWRITE_TAC[CARD3; CARD4; IN_SET3] THEN
1805 REWRITE_TAC[DE_MORGAN_THM] THEN DAO THEN
1806 STRIP_TAC THEN CONJ_TAC THENL [
1807 NHANH (NORM_ARITH`u + v - w = w ==> dist (w,u) = &1 / &2 *  dist (u,v) `) THEN
1808 UNDISCH_TAC `dist ((u:real^3),v) < sqrt (&8)` THEN
1809  NHANH (LT_SQ8_IMP_LT2 ) THEN DOWN_TAC THEN SET_TAC[];
1810 REWRITE_TAC[VECTOR_ARITH ` ((v:real^N) = u + v - w <=> u = w )`;
1811   VECTOR_ARITH ` ((u:real^N) = u + v - w <=> v = w ) `] THEN ASM_MESON_TAC[]];
1812 DAO THEN CONJ_TAC THENL [REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN
1813 REAL_ARITH_TAC;DOWN_TAC THEN REWRITE_TAC[CARD3] THEN SET_TAC[]]]);;
1814 *)
1815
1816
1817 let MIDDLE_POINT_IN_CONV2 = prove(` &1 / &2 % ( u + v ) IN conv {u,v} `,
1818 REWRITE_TAC[CONV_SET2; IN_ELIM_THM; VECTOR_ADD_LDISTRIB] THEN
1819 MESON_TAC[REAL_ARITH ` &0 <= &1 / &2 `; REAL_ARITH` &1 / &2 + &1 / &2 = &1 `]);;
1820
1821 let INTER_DISJONT_EX =
1822 SET_RULE ` ( a INTER b = {} ) <=> (! x. ~ (x IN a /\ x IN b )) `;;
1823
1824
1825 (* LEMMA36 *)
1826
1827 (* ================== *)
1828
1829 MATCH_MP (SPEC_ALL AFFINE_HULL_FINITE) (MESON[FINITE_RULES] ` FINITE {(a:real^N),b,c} `) ;;
1830
1831
1832
1833 let PLANE_IMP_AFFINE = prove(`plane (p:real^N -> bool ) ==> affine p `,
1834 MESON_TAC[plane; AFFINE_AFFINE_HULL]);;
1835
1836
1837
1838 let PLANE_IMP_AFFINE = prove(` plane (p:real^N -> bool ) ==> affine p `,
1839 REWRITE_TAC[plane; AFFINE_HULL_3; affine; FUN_EQ_THM; IN_ELIM_THM] THEN
1840 STRIP_TAC THEN ASM_SIMP_TAC[IN] THEN REPEAT STRIP_TAC THEN ASM_SIMP_TAC[] THEN
1841 SIMP_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC] THEN
1842 REWRITE_TAC[VECTOR_ARITH` (( a:real^N) + b + c ) + a' + b' + c'
1843   = ( a + a' ) + ( b + b') + c + c' `] THEN EXISTS_TAC ` u' * u'' + v' * u''' ` THEN
1844 EXISTS_TAC ` (u' * v'' + v' * v''')` THEN EXISTS_TAC ` (u' * w' + v' * w'')` THEN
1845 ASM_SIMP_TAC[prove(` u' + v' = &1 /\
1846   u''' + v''' + w'' = &1 /\
1847   u'' + v'' + w' = &1 ==>
1848   (u' * u'' + v' * u''') + (u' * v'' + v' * v''') + u' * w' + v' * w'' = &1 `,
1849 SIMP_TAC[REAL_ARITH` a + b = &1 <=> a = &1 - b `] THEN REAL_ARITH_TAC);
1850   GSYM VECTOR_ADD_RDISTRIB]);;
1851
1852
1853
1854
1855 let IMP_AFFINE_HULL_SUBSET = prove(` FINITE a /\ a SUBSET s /\
1856 ~( a = {} )/\ affine s  ==> ( affine hull a ) SUBSET s `,
1857 SIMP_TAC[AFFINE_HULL_FINITE; SUBSET; IN_ELIM_THM] THEN
1858 REWRITE_TAC[ GSYM SUBSET] THEN MESON_TAC[AFFINE]);;
1859
1860
1861
1862 let SET_EQ_EX = SET_RULE `a = b <=> (! x. x IN a <=> x IN b ) `;;
1863
1864 let SET_EQ_TO_SUBSET = SET_RULE ` a = b <=>  a SUBSET b /\ b SUBSET a `;;
1865
1866
1867
1868
1869 let OTHORGONAL_QUATER_FOR = prove(` delta x12 ( x12 + x23 ) ( x12 + x24 )  x23 x24 x34 =
1870   x12 * ups_x x23 x24 x34 `, REWRITE_TAC[delta; ups_x] THEN REAL_ARITH_TAC);;
1871
1872
1873 let ORTHOGONAL_CROSS_PRODUCT = prove(` u dot ( u cross v ) = &0 /\
1874   v dot ( u cross v ) = &0 `,
1875 REWRITE_TAC[cross; triple_of_real3; real3_of_triple; mk_vec3] THEN
1876 LET_TR THEN REWRITE_TAC[DOT_3; VECTOR_3] THEN REAL_ARITH_TAC);;
1877
1878 let PITHAGOR_CROSS = prove(` dist (a +  (b - a) cross (c - a),b) pow 2 =
1879 dist (b,a) pow 2 +  norm (  (b - a) cross (c - a) ) pow 2 `,
1880 REWRITE_TAC[vector_norm; dist] THEN
1881 SIMP_TAC[DOT_POS_LE; SQRT_WORKS] THEN
1882 REWRITE_TAC[VECTOR_ARITH` ((a:real^N) + b) - c = b - (c - a ) `] THEN
1883 ABBREV_TAC ` ab = ( b - (a:real^3)) ` THEN
1884 ABBREV_TAC ` ac = ( c - (a:real^3)) ` THEN
1885 REWRITE_TAC[DOT_LSUB; DOT_RSUB] THEN
1886 SIMP_TAC[ORTHOGONAL_CROSS_PRODUCT; DOT_SYM] THEN
1887 REAL_ARITH_TAC);;
1888
1889 let PITHAGOR_NORM = prove(` a dot b = &0 ==> dist (a,b) pow 2 = norm a pow 2 +
1890   norm b pow 2 `,
1891 SIMP_TAC[dist; vector_norm; DOT_POS_LE; SQRT_WORKS] THEN
1892 SIMP_TAC[DOT_LSUB; DOT_RSUB; DOT_SYM] THEN REAL_ARITH_TAC);;
1893
1894 let VEC3_EQ_EX= prove(`! a (b:real^3). a = b <=> a$1 = b$1 /\ a$2 = b$2 /\ a$3 = b$3 `,
1895 SIMP_TAC[CART_EQ; DIMINDEX_3] THEN
1896 REWRITE_TAC[ARITH_RULE`1 <= i /\ i <= 3 <=>
1897   i = 1 \/ i = 2 \/ i = 3 `] THEN MESON_TAC[]);;
1898
1899 let CROSS_CONVERT = prove_by_refinement(
1900 `  (b - a) cross (c - d) =  (a - b) cross (d - c )`,
1901   (* {{{ proof *)
1902   [
1903   (REWRITE_TAC[cross; triple_of_real3; real3_of_triple; mk_vec3]);
1904   (LET_TR);
1905   (REWRITE_TAC[lemma_cm3 ]);
1906   (REWRITE_TAC[VEC3_EQ_EX]);
1907   (REWRITE_TAC[VEC3_EQ_EX; VECTOR_3]);
1908   BY((REAL_ARITH_TAC))
1909   ]);;
1910   (* }}} *)
1911
1912
1913 let lemma1 = MESON[prove(` dist(b,c) pow 2 = (a - c - (a - b)) dot (a - c - (a - b)) `,
1914                          SIMP_TAC[dist; vector_norm; DOT_POS_LE; SQRT_WORKS] THEN
1915                            MESON_TAC[VECTOR_ARITH
1916                 ` b - (c:real^N) = (a - c) - ( a - b) `])]`
1917   ups_x  aa bb (dist (b,c) pow 2 ) =
1918   ups_x aa bb (( a - c - (a - b)) dot (a - c - (a - b))) `;;
1919
1920 let NORM_CROSS_PRODUCT_UPS_X  = prove_by_refinement(
1921   `&4 * norm ( (b - a) cross (c - a)) pow 2 =
1922     ups_x (dist (a,b) pow 2) (dist (a,c) pow 2) (dist (b,c) pow 2)`,
1923   (* {{{ proof *)
1924   [
1925   (REWRITE_TAC[lemma1 ]);
1926   (ONCE_REWRITE_TAC[CROSS_CONVERT]);
1927   (SIMP_TAC[ups_x;DIST_SYM; dist; vector_norm; DOT_POS_LE; SQRT_WORKS]);
1928   (REWRITE_TAC[cross; triple_of_real3; real3_of_triple; mk_vec3]);
1929   (LET_TR);
1930   (REWRITE_TAC[DOT_3; VECTOR_3]);
1931   (ABBREV_TAC ` ab = a - (b:real^3) `);
1932   (ABBREV_TAC ` cc = a - (c:real^3) `);
1933   BY((REWRITE_TAC[lemma_cm3 ] THEN REAL_ARITH_TAC))
1934   ]);;
1935   (* }}} *)
1936
1937 let lemma1 = prove(
1938   ` dist (  a cross b, a ) pow 2  = norm ( a cross b) pow 2 +
1939     norm a pow 2 /\dist (  a cross b, b ) pow 2  = norm ( a cross b) pow 2 +
1940     norm b pow 2 `,
1941   SIMP_TAC[DOT_SYM;ORTHOGONAL_CROSS_PRODUCT ; PITHAGOR_NORM; DIST_SYM]
1942 );;
1943
1944 let NOT_COLLINEAR_IMP_CROSS_NOT_COPLANAR = prove_by_refinement(
1945  ` ! u v (w:real^3). ~ collinear {a,b,c} ==> ~ coplanar_alt {
1946   a +  (b - a ) cross ( c - a ),a,b,c} `,
1947   (* {{{ proof *)
1948   [
1949   (MP_TAC POLFLZY);
1950   (LET_TR);
1951   (SIMP_TAC[]);
1952   (DISCH_TAC);
1953   (REWRITE_TAC[NORM_ARITH` dist (a + b ,a) = norm (b ) `]);
1954   (REWRITE_TAC[NORM_ARITH`dist (a + c,b) =  dist ( c, b - a ) `]);
1955   (SIMP_TAC[lemma1]);
1956   (REWRITE_TAC[GSYM dist]);
1957   (SIMP_TAC[DIST_SYM; OTHORGONAL_QUATER_FOR]);
1958   (ONCE_REWRITE_TAC[REAL_ARITH` a * b = &0 <=> ( &4 * a ) * b = &0 `]);
1959   (SIMP_TAC[NORM_CROSS_PRODUCT_UPS_X]);
1960   (REWRITE_TAC[REAL_ENTIRE]);
1961   BY((MESON_TAC[FHFMKIY]))
1962   ]);;
1963   (* }}} *)
1964
1965 let ORTHOGONAL_IMP_PITHAGOR = prove(` (x:real^N) dot ((a:real^N) - b) = &0 ==>
1966   dist (a + x,b) pow 2 = norm x pow 2 + dist (a,b) pow 2`,
1967 SIMP_TAC[dist; vector_norm; DOT_POS_LE; SQRT_WORKS] THEN
1968 REWRITE_TAC[VECTOR_ARITH` (a + c) - b = c + a - (b:real^N)`] THEN
1969 ABBREV_TAC ` aa = ( a - (b:real^N)) ` THEN
1970 SIMP_TAC[DOT_LADD; DOT_RADD; DOT_SYM; ZERO_NEUTRAL]);;
1971
1972 let NOT_COL_AND_ORTHO_IMP_NOT_COPL = prove(`! a b c (x:real^3).
1973  ~collinear {a, b, c} /\ x dot (a - b) = &0 /\
1974  x dot (a - c) = &0 /\ ~(x = vec 0)
1975  ==> ~coplanar_alt {a + x, a, b, c}`,
1976 MP_TAC POLFLZY THEN LET_TR THEN SIMP_TAC[] THEN
1977 SIMP_TAC[ORTHOGONAL_IMP_PITHAGOR ] THEN
1978 SIMP_TAC[ORTHOGONAL_IMP_PITHAGOR; NORM_ARITH ` dist (a + x,a) = norm x `] THEN
1979 SIMP_TAC[ORTHOGONAL_IMP_PITHAGOR; NORM_ARITH ` dist (a + x,a) = norm x `;
1980 OTHORGONAL_QUATER_FOR] THEN SIMP_TAC[COL_EQ_UPS_0] THEN
1981 SIMP_TAC[COL_EQ_UPS_0; GSYM NORM_POS_LT; REAL_ENTIRE; MESON[RELATE_POW2]`
1982   a pow 2 = &0 <=> a = &0 `; REAL_ARITH ` &0 < a ==> ~( a = &0 ) `]);;
1983
1984 let PLANE_NORM_IMP_AFFINE = prove(`! p. plane_norm p ==> affine p `,
1985 REWRITE_TAC[plane_norm; affine] THEN GEN_TAC THEN STRIP_TAC THEN
1986 ASM_SIMP_TAC[IN_ELIM_THM;  MESON[]` a = &1 <=> &1 = a `] THEN
1987 ONCE_REWRITE_TAC[ VECTOR_ARITH ` ( a + b ) - c = ( a + b ) - &1 % c `] THEN
1988 ASM_SIMP_TAC[ VECTOR_ARITH` (u % x + v % y) - (u + v) % v0 =
1989 u % ( x - v0 ) +  v % ( y - v0 ) `; DOT_RADD; DOT_RMUL; ZERO_NEUTRAL]);;
1990
1991 let IN_PLANE_IMP_OTHORGONAL = prove(`
1992  n dot (x - v0) = &0 /\ n dot (y - v0) = &0 /\ n dot (z - v0) = &0 ==>
1993   n dot ( x - y ) = &0 /\ n dot ( x - z ) = &0 `,
1994 SIMP_TAC[DOT_RSUB] THEN REAL_ARITH_TAC);;
1995
1996 let IMP_A1_EQ_0 = prove_by_refinement(
1997 `(n:real^N) dot (x - v0) = &0 /\
1998  n dot (y - v0) = &0 /\
1999  n dot (z - v0) = &0 /\
2000  ~(n = vec 0) /\
2001  x' = a1 % (x + n) + a2 % x + a3 % y + a4 % z /\
2002  a1 + a2 + a3 + a4 = &1 /\
2003  n dot (x' - v0) = &0
2004  ==> a1 = &0`,
2005   (* {{{ proof *)
2006   [
2007    (STRIP_TAC);
2008    (UNDISCH_TAC ` (n:real^N) dot (x' - v0) = &0`);
2009   (ASM_SIMP_TAC[VECTOR_ARITH`(a1 % x + y ) - v0 = a1 % ( x - v0 ) + y - v0 + a1 % v0 `]);
2010   (ONCE_REWRITE_TAC[ VECTOR_ARITH` a % x - y =  a % ( x - y ) + a % y - y `]);
2011   (ASM_SIMP_TAC[DOT_RADD; VECTOR_ARITH` ( a + b ) - (c:real^N)   = b + a - c `; DOT_RMUL; ZERO_NEUTRAL]);
2012   (ASM_SIMP_TAC[DOT_RADD; VECTOR_ARITH` ( a + b ) - (c:real^N)   = b + a - c `; DOT_RMUL; ZERO_NEUTRAL; DOT_RSUB;REAL_ARITH` ((a4 * (n dot v0) - n dot v0 + a3 * (n dot v0)) + a2 * (n dot v0)) + a1 * (n dot v0) = ( a1 + a2 + a3 + a4 ) * ( n dot v0 ) - n dot v0 `; REAL_ARITH ` &1 * a - a = &0 `]);
2013   BY((ASM_MESON_TAC[REAL_ENTIRE; GSYM DOT_EQ_0]))
2014   ]);;
2015   (* }}} *)
2016
2017 let LEMMA7 = prove(` !x y z (p:real^3 -> bool).
2018          plane_norm p /\ ~collinear {x, y, z} /\ {x, y, z} SUBSET p
2019          ==> p = aff {x, y, z}`,
2020 NHANH (PLANE_IMP_AFFINE) THEN
2021 REPEAT STRIP_TAC THEN
2022 REWRITE_TAC[aff; SET_EQ_TO_SUBSET] THEN CONJ_TAC THENL [
2023 UNDISCH_TAC ` plane_norm (p:real^3 -> bool ) ` THEN
2024 REWRITE_TAC[plane_norm] THEN
2025 STRIP_TAC THEN
2026 UNDISCH_TAC ` {(x:real^3), y, z} SUBSET p` THEN
2027 ASM_SIMP_TAC[SET3_SUBSET; IN_ELIM_THM] THEN
2028 NHANH (IN_PLANE_IMP_OTHORGONAL ) THEN
2029 DOWN_TAC THEN
2030 NHANH (MESON[NOT_COL_AND_ORTHO_IMP_NOT_COPL]`
2031   ~collinear {(x:real^3), y, z} /\
2032  ~(n = vec 0) /\a1 /\a2 /\a4 /\a3/\
2033  n dot (x - y) = &0 /\
2034  n dot (x - z) = &0 ==> ~coplanar_alt { x + n ,x,y,z} `) THEN
2035 REWRITE_TAC[SUBSET; IN_ELIM_THM] THEN
2036 REPEAT STRIP_TAC THEN
2037 UNDISCH_TAC `~coplanar_alt {x + n, x, y, (z:real^3)} ` THEN
2038 NHANH (SPEC `x' :real^3` (GEN `v :real^3` ( SPEC_ALL COEFS_4 ))) THEN
2039 ABBREV_TAC ` a1 = COEF4_1 (x + n) x y z x'` THEN
2040 ABBREV_TAC ` a2 = COEF4_2 (x + n) x y z x'` THEN
2041 ABBREV_TAC ` a3 = COEF4_3 (x + n) x y z x'` THEN
2042 ABBREV_TAC ` a4 = COEF4_4 (x + n) x y z x'` THEN
2043 STRIP_TAC THEN
2044 DOWN_TAC THEN
2045 REWRITE_TAC[AFFINE_HULL_3; IN_ELIM_THM] THEN
2046 NHANH (MESON[IMP_A1_EQ_0]` ~(n = vec 0) /\
2047  aa1 /\
2048  n dot (x - v0) = &0 /\
2049  n dot (y - v0) = &0 /\
2050  n dot (z - v0) = &0 /\
2051  aa2 /\aa3 /\
2052  n dot (x' - v0) = &0 /\aa4/\aa5 /\aa6/\aa7/\
2053  ~coplanar_alt {x + n, x, y, z} /\
2054  a1 + a2 + a3 + a4 = &1 /\
2055  x' = a1 % (x + n) + a2 % x + a3 % y + a4 % z /\ l ==>
2056   a1 = &0 `) THEN
2057 PURE_ONCE_REWRITE_TAC[MESON[]` P a1 /\ a1 = &0 <=> P (&0) /\
2058   a1 = &0 `] THEN
2059 REWRITE_TAC[ZERO_NEUTRAL; VECTOR_ARITH` &0 % x + y = y `] THEN
2060 MESON_TAC[];
2061 ASM_MESON_TAC[PLANE_NORM_IMP_AFFINE ; FINITE_RULES;
2062 SET_RULE` ~({(x:real^N), y, z} = {} )`;  IMP_AFFINE_HULL_SUBSET]]);;
2063
2064 let SMWTDMU = LEMMA7;;
2065
2066 let DET_VEC3_AS_CROSS_DOT = prove_by_refinement(
2067 ` det_vec3 v1 v2 v3 = (  v1 cross v2 ) dot v3 `,
2068   (* {{{ proof *)
2069   [
2070   (REWRITE_TAC[det_vec3; cross; triple_of_real3; real3_of_triple; mk_vec3; DOT_3; VECTOR_3]);
2071   (LET_TR);
2072   (REWRITE_TAC[det_vec3; cross; triple_of_real3; real3_of_triple; mk_vec3; DOT_3; VECTOR_3]);
2073   BY((REAL_ARITH_TAC))
2074   ]);;
2075   (* }}} *)
2076
2077 let COL_EQ_NORM_CROSS = prove_by_refinement(
2078 ` ! v1 v2 (v3:real^3). collinear {v1,v2,v3} <=>
2079  norm ( (v2 - v1) cross (v3 - v1)) pow 2 = &0 `,
2080   (* {{{ proof *)
2081   [
2082   (REWRITE_TAC[COL_EQ_UPS_0]);
2083   (REWRITE_TAC[GSYM NORM_CROSS_PRODUCT_UPS_X]);
2084   BY((REAL_ARITH_TAC))
2085   ]);;
2086   (* }}} *)
2087
2088
2089
2090
2091 let COLLINEAR_IMP_COPLANAR = prove(` ! v1 v2 v3 v3 (v:real^3). collinear {v1,v2,v3} ==>
2092 coplanar_alt {v1,v2,v3,v} `,
2093 REWRITE_TAC[COPLANAR_DET_VEC3_EQ_0; COL_EQ_NORM_CROSS; DET_VEC3_AS_CROSS_DOT ] THEN
2094 REWRITE_TAC[GSYM RELATE_POW2; NORM_EQ_0] THEN REPEAT GEN_TAC THEN
2095 SIMP_TAC[VECTOR_ARITH ` vec 0 dot x = &0 `]);;
2096
2097 (* MAY WORKS, LEMMA 85 ; VBVYGGT *)
2098
2099
2100
2101
2102 let POS_EQ_NOT_COPLANANR = prove(` &0 <   delta (dist ((x1:real^3),x2) pow 2) (dist (x1,x3) pow 2)
2103            (dist (x1,x4) pow 2)
2104            (dist (x2,x3) pow 2)
2105            (dist (x2,x4) pow 2)
2106            (dist (x3,x4) pow 2) <=> ~coplanar_alt {x1, x2, x3, x4} `,
2107 MP_TAC (DELTA_POS_4POINTS) THEN MP_TAC POLFLZY THEN LET_TR THEN
2108 REWRITE_TAC[REAL_ARITH` a <= b <=> a = b \/ a < b `] THEN
2109 MESON_TAC[REAL_ARITH` ~( a = b /\ a < b ) `]);;
2110
2111 let SUM_CHI_EQ_2DELTA = prove(` let chi11 = chi x12 x13 x14 x23 x24 x34 in
2112  let chi22 = chi x12 x24 x23 x14 x13 x34 in
2113  let chi33 = chi x34 x13 x23 x14 x24 x12 in
2114  let chi44 = chi x34 x24 x14 x23 x13 x12 in
2115  &2 * delta x12 x13 x14 x23 x24 x34 = chi11 + chi22 + chi33 + chi44`, LET_TR THEN
2116 REWRITE_TAC[chi; delta] THEN REAL_ARITH_TAC);;
2117
2118 let NOT_0_IMP_SUM_CHI_1 = prove(`~(delta x12 x13 x14 x23 x24 x34 = &0)
2119  ==> chi x12 x13 x14 x23 x24 x34 / (&2 * delta x12 x13 x14 x23 x24 x34) +
2120      chi x12 x24 x23 x14 x13 x34 / (&2 * delta x12 x13 x14 x23 x24 x34) +
2121      chi x34 x13 x23 x14 x24 x12 / (&2 * delta x12 x13 x14 x23 x24 x34) +
2122      chi x34 x24 x14 x23 x13 x12 / (&2 * delta x12 x13 x14 x23 x24 x34) =
2123      &1`, MP_TAC SUM_CHI_EQ_2DELTA THEN
2124 LET_TR THEN CONV_TAC REAL_FIELD);;
2125
2126 (* MAY WORKS *)
2127
2128 let PROVE_DIST_FROM_V1 = prove(` ~coplanar_alt {v1, v2, v3, v4} ==>
2129 let x12 = dist (v1,v2) pow 2 in
2130  let x13 = dist (v1,v3) pow 2 in
2131  let x14 = dist (v1,v4) pow 2 in
2132  let x23 = dist (v2,v3) pow 2 in
2133  let x24 = dist (v2,v4) pow 2 in
2134  let x34 = dist (v3,v4) pow 2 in
2135  let chi11 = chi x12 x13 x14 x23 x24 x34 in
2136  let chi22 = chi x12 x24 x23 x14 x13 x34 in
2137  let chi33 = chi x34 x13 x23 x14 x24 x12 in
2138  let chi44 = chi x34 x24 x14 x23 x13 x12 in
2139  p =
2140  &1 / (&2 * delta x12 x13 x14 x23 x24 x34) %
2141  (chi11 % v1 + chi22 % v2 + chi33 % v3 + chi44 % v4)
2142  ==> dist3 p v1 pow 2 =
2143     ( &1 / &2 ) * rho_ij' x12 x13 x14 x23 x24 x34 / (&2 * delta x12 x13 x14 x23 x24 x34) `,
2144 REWRITE_TAC[ GSYM POS_EQ_NOT_COPLANANR] THEN
2145 NHANH (REAL_ARITH` a < b ==> ~( b = a ) `) THEN
2146 NHANH NOT_0_IMP_SUM_CHI_1  THEN
2147 LET_TR THEN REWRITE_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC;
2148   REAL_ARITH` ( &1 / a ) * b = b / a `] THEN
2149 ABBREV_TAC ` a1 = chi (dist (v1,v2) pow 2) (dist (v1,v3) pow 2) (dist (v1,v4) pow 2)
2150      (dist (v2,v3) pow 2)
2151      (dist (v2,v4) pow 2)
2152      (dist (v3,v4) pow 2) /
2153      (&2 *
2154       delta (dist (v1,v2) pow 2) (dist (v1,v3) pow 2) (dist (v1,v4) pow 2)
2155       (dist (v2,v3) pow 2)
2156       (dist (v2,v4) pow 2)
2157       (dist (v3,(v4:real^3)) pow 2))` THEN
2158 ABBREV_TAC ` a2 = chi (dist (v1,v2) pow 2) (dist (v2,v4) pow 2) (dist (v2,v3) pow 2)
2159      (dist (v1,v4) pow 2)
2160      (dist (v1,v3) pow 2)
2161      (dist (v3,v4) pow 2) /
2162      (&2 *
2163       delta (dist (v1,v2) pow 2) (dist (v1,v3) pow 2) (dist (v1,v4) pow 2)
2164       (dist (v2,v3) pow 2)
2165       (dist (v2,v4) pow 2)
2166       (dist (v3,(v4:real^3)) pow 2)) ` THEN
2167 REWRITE_TAC[ GSYM dist3] THEN
2168 ABBREV_TAC ` a3 = chi (dist3 v3 v4 pow 2) (dist3 v1 v3 pow 2) (dist3 v2 v3 pow 2) (dist3 v1 v4 pow 2)
2169      (dist3 v2 v4 pow 2)
2170      (dist3 v1 v2 pow 2) /
2171      (&2 *
2172       delta (dist3 v1 v2 pow 2) (dist3 v1 v3 pow 2) (dist3 v1 v4 pow 2)
2173       (dist3 v2 v3 pow 2)
2174       (dist3 v2 v4 pow 2)
2175       (dist3 v3 v4 pow 2)) ` THEN
2176 ABBREV_TAC ` a4 = chi (dist3 v3 v4 pow 2) (dist3 v2 v4 pow 2) (dist3 v1 v4 pow 2) (dist3 v2 v3 pow 2)
2177      (dist3 v1 v3 pow 2)
2178      (dist3 v1 v2 pow 2) /
2179      (&2 *
2180       delta (dist3 v1 v2 pow 2) (dist3 v1 v3 pow 2) (dist3 v1 v4 pow 2)
2181       (dist3 v2 v3 pow 2)
2182       (dist3 v2 v4 pow 2)
2183       (dist3 v3 v4 pow 2)) ` THEN
2184 SIMP_TAC[REAL_ARITH` a + b = &1 <=> a = &1 - b `] THEN
2185 REPEAT STRIP_TAC THEN
2186 REWRITE_TAC[dist3; dist; NORM_POW_2; VECTOR_ARITH`
2187   (((&1 - (a2 + a3 + a4)) % v1 + a2 % v2 + a3 % v3 + a4 % v4) - v1) =
2188   a2 % ( v2 - v1 ) + a3 % (v3 - v1 ) + a4 % ( v4 - v1 ) `;
2189   VECTOR_ARITH` ( a + b ) dot ( a + b ) = a dot a + &2 * ( a dot b )
2190   + b dot b `] THEN
2191 REWRITE_TAC[DOT_RADD; DOT_LMUL; DOT_RMUL] THEN
2192 REWRITE_TAC[X_DOT_X_EQ] THEN
2193 REWRITE_TAC[DOT_NORM_NEG; VECTOR_ARITH` v2 - v1 - (v4 - v1)
2194   = (v2:real^N) - v4 `] THEN
2195 SIMP_TAC[GSYM dist; DIST_SYM; GSYM dist3; D3_SYM] THEN
2196 EXPAND_TAC "a2" THEN
2197 EXPAND_TAC "a3" THEN
2198 EXPAND_TAC "a4" THEN
2199 REWRITE_TAC[GSYM dist3 ] THEN
2200 ABBREV_TAC ` x12 = dist3 v1 v2 pow 2 ` THEN
2201 ABBREV_TAC ` x13 = dist3 v1 v3 pow 2 ` THEN
2202 ABBREV_TAC ` x14 = dist3 v1 v4 pow 2 ` THEN
2203 ABBREV_TAC ` x23 = dist3 v2 v3 pow 2 ` THEN
2204 ABBREV_TAC ` x24 = dist3 v2 v4 pow 2 ` THEN
2205 ABBREV_TAC ` x34 = dist3 v3 v4 pow 2 ` THEN
2206 UNDISCH_TAC ` &0 < delta x12 x13 x14 x23 x24 x34 ` THEN
2207 ONCE_REWRITE_TAC[REAL_FIELD` &0 < a ==> b = c <=> &0 < a
2208  ==> b * ( &2 * a) pow 2 = c * ( &2 * a ) pow 2 `] THEN
2209 ONCE_REWRITE_TAC[REAL_ARITH` &0 < a <=> &0 < &2 * a `] THEN
2210 SIMP_TAC[REAL_FIELD` &0 < b ==> ( a / b ) * b pow 2 = a * b `;
2211   REAL_RDISTRIB; REAL_FIELD` &0 < b ==> ( a / b ) * ( aa / b ) * c *
2212 b pow 2 = a * aa * c `; REAL_ADD_LDISTRIB] THEN
2213 SIMP_TAC[REAL_LDISTRIB; REAL_ARITH` (a*b)*c = a *b * c `;
2214   REAL_FIELD` &0 < b ==> ( a / b ) * ( a / b ) * c * b pow 2 = a pow 2 * c `;
2215   REAL_ARITH` &2 * a * b * c / &2 * d = a * b * d * c `] THEN
2216 SIMP_TAC[REAL_FIELD` &0 < a ==> ( b / a ) * ( bb / a ) * a pow 2
2217   * d = b * bb * d `] THEN
2218 SIMP_TAC[REAL_FIELD` &0 < a ==> b / a / &2 * a pow 2 =
2219   a * b / &2 `] THEN
2220 REWRITE_TAC[chi; rho_ij'; delta] THEN
2221 REAL_ARITH_TAC);;
2222
2223 let PROVE_EQ_DIST_FROM4 = prove(` ~coplanar_alt {v1, v2, v3, v4} ==>
2224 let x12 = dist (v1,v2) pow 2 in
2225  let x13 = dist (v1,v3) pow 2 in
2226  let x14 = dist (v1,v4) pow 2 in
2227  let x23 = dist (v2,v3) pow 2 in
2228  let x24 = dist (v2,v4) pow 2 in
2229  let x34 = dist (v3,v4) pow 2 in
2230  let chi11 = chi x12 x13 x14 x23 x24 x34 in
2231  let chi22 = chi x12 x24 x23 x14 x13 x34 in
2232  let chi33 = chi x34 x13 x23 x14 x24 x12 in
2233  let chi44 = chi x34 x24 x14 x23 x13 x12 in
2234  p =
2235  &1 / (&2 * delta x12 x13 x14 x23 x24 x34) %
2236  (chi11 % v1 + chi22 % v2 + chi33 % v3 + chi44 % v4)
2237 ==>
2238 dist3 p v2 pow 2 = ( &1 / &2 ) * rho_ij' x12 x13 x14 x23 x24 x34 / (&2 * delta x12 x13 x14 x23 x24 x34) /\
2239 dist3 p v3 pow 2 = ( &1 / &2 ) * rho_ij' x12 x13 x14 x23 x24 x34 / (&2 * delta x12 x13 x14 x23 x24 x34) /\
2240 dist3 p v4 pow 2 =
2241  ( &1 / &2 ) * rho_ij' x12 x13 x14 x23 x24 x34 / (&2 * delta x12 x13 x14 x23 x24 x34)  `,
2242 REWRITE_TAC[ GSYM POS_EQ_NOT_COPLANANR] THEN
2243 NHANH (REAL_ARITH` a < b ==> ~( b = a ) `) THEN
2244 NHANH NOT_0_IMP_SUM_CHI_1  THEN
2245 LET_TR THEN REWRITE_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC;
2246   REAL_ARITH` ( &1 / a ) * b = b / a `] THEN
2247 ABBREV_TAC ` a1 = chi (dist (v1,v2) pow 2) (dist (v1,v3) pow 2) (dist (v1,v4) pow 2)
2248      (dist (v2,v3) pow 2)
2249      (dist (v2,v4) pow 2)
2250      (dist (v3,v4) pow 2) /
2251      (&2 *
2252       delta (dist (v1,v2) pow 2) (dist (v1,v3) pow 2) (dist (v1,v4) pow 2)
2253       (dist (v2,v3) pow 2)
2254       (dist (v2,v4) pow 2)
2255       (dist (v3,(v4:real^3)) pow 2))` THEN
2256 ABBREV_TAC ` a2 = chi (dist (v1,v2) pow 2) (dist (v2,v4) pow 2) (dist (v2,v3) pow 2)
2257      (dist (v1,v4) pow 2)
2258      (dist (v1,v3) pow 2)
2259      (dist (v3,v4) pow 2) /
2260      (&2 *
2261       delta (dist (v1,v2) pow 2) (dist (v1,v3) pow 2) (dist (v1,v4) pow 2)
2262       (dist (v2,v3) pow 2)
2263       (dist (v2,v4) pow 2)
2264       (dist (v3,(v4:real^3)) pow 2)) ` THEN
2265 REWRITE_TAC[ GSYM dist3] THEN
2266 ABBREV_TAC ` a3 = chi (dist3 v3 v4 pow 2) (dist3 v1 v3 pow 2) (dist3 v2 v3 pow 2) (dist3 v1 v4 pow 2)
2267      (dist3 v2 v4 pow 2)
2268      (dist3 v1 v2 pow 2) /
2269      (&2 *
2270       delta (dist3 v1 v2 pow 2) (dist3 v1 v3 pow 2) (dist3 v1 v4 pow 2)
2271       (dist3 v2 v3 pow 2)
2272       (dist3 v2 v4 pow 2)
2273       (dist3 v3 v4 pow 2)) ` THEN
2274 ABBREV_TAC ` a4 = chi (dist3 v3 v4 pow 2) (dist3 v2 v4 pow 2) (dist3 v1 v4 pow 2) (dist3 v2 v3 pow 2)
2275      (dist3 v1 v3 pow 2)
2276      (dist3 v1 v2 pow 2) /
2277      (&2 *
2278       delta (dist3 v1 v2 pow 2) (dist3 v1 v3 pow 2) (dist3 v1 v4 pow 2)
2279       (dist3 v2 v3 pow 2)
2280       (dist3 v2 v4 pow 2)
2281       (dist3 v3 v4 pow 2)) ` THEN
2282 ONCE_REWRITE_TAC[MESON[VECTOR_ARITH` &1 % x = x `]` dist3 a b pow 2 =
2283   aa <=> dist3 a ( &1 % b ) pow 2 = aa `] THEN
2284 ONCE_REWRITE_TAC[MESON[]` a = &1 <=> &1 = a `] THEN
2285 SIMP_TAC[] THEN
2286 STRIP_TAC THEN STRIP_TAC THEN
2287 REWRITE_TAC[dist3; dist] THEN
2288 REWRITE_TAC[VECTOR_ARITH` (a1 % v1 + a2 % v2 + a3 % v3 + a4 % v4) - (a1 + a2 + a3 + a4) % v2
2289   = a1 % ( v1 - v2 ) + a3 % ( v3 - v2 ) + a4 % (v4 - v2 ) `;
2290   VECTOR_ARITH` (a1 % v1 + a2 % v2 + a3 % v3 + a4 % v4) - (a1 + a2 + a3 + a4) % v3
2291   = a1 % ( v1 - v3 ) + a2 % ( v2 - v3 ) + a4 % (v4 - v3 )`;
2292   VECTOR_ARITH` (a1 % v1 + a2 % v2 + a3 % v3 + a4 % v4) - (a1 + a2 + a3 + a4) % v4 =
2293   a1 % ( v1 - v4 ) + a2 % ( v2 - v4 ) + a3 % (v3 - v4 )`] THEN
2294 REWRITE_TAC[NORM_POW_2] THEN
2295 REWRITE_TAC[DOT_LADD; DOT_RADD; DOT_LMUL; DOT_RMUL; GSYM NORM_POW_2] THEN
2296 REWRITE_TAC[DOT_NORM_NEG; VECTOR_ARITH` v3 - v4 - (v2 - v4) =
2297   (v3:real^N) - v2 `; GSYM dist; GSYM dist3 ] THEN
2298 EXPAND_TAC "a1" THEN
2299 EXPAND_TAC "a2" THEN
2300 EXPAND_TAC "a3" THEN
2301 EXPAND_TAC "a4" THEN
2302 REWRITE_TAC[GSYM dist3 ] THEN
2303 REWRITE_TAC[prove(` dist3 (v4 - v3) (v1 - v3) = dist3 v1 v4 `,
2304 REWRITE_TAC[dist3] THEN CONV_TAC NORM_ARITH)] THEN
2305 SIMP_TAC[D3_SYM] THEN
2306 ABBREV_TAC ` x12 = dist3 v1 v2 pow 2 ` THEN
2307 ABBREV_TAC ` x13 = dist3 v1 v3 pow 2 ` THEN
2308 ABBREV_TAC ` x14 = dist3 v1 v4 pow 2 ` THEN
2309 ABBREV_TAC ` x23 = dist3 v2 v3 pow 2 ` THEN
2310 ABBREV_TAC ` x24 = dist3 v2 v4 pow 2 ` THEN
2311 ABBREV_TAC ` x34 = dist3 v3 v4 pow 2 ` THEN
2312 UNDISCH_TAC ` &0 < delta x12 x13 x14 x23 x24 x34 ` THEN
2313 ONCE_REWRITE_TAC[REAL_FIELD` &0 < a ==> ( b = c ) /\ ( bb = cc ) /\ ( bbb = ccc )
2314 <=> &0 < a
2315  ==> ( b * ( &2 * a) pow 2 = c * ( &2 * a ) pow 2 ) /\
2316 ( bb * ( &2 * a) pow 2 = cc * ( &2 * a ) pow 2 ) /\
2317 ( bbb * ( &2 * a) pow 2 = ccc * ( &2 * a ) pow 2 ) `] THEN
2318 ONCE_REWRITE_TAC[REAL_ARITH` &0 < a <=> &0 < &2 * a `] THEN
2319 SIMP_TAC[REAL_FIELD` &0 < b ==> ( a / b ) * b pow 2 = a * b `;
2320   REAL_RDISTRIB; REAL_FIELD` &0 < b ==> ( a / b ) * ( aa / b ) * c *
2321 b pow 2 = a * aa * c `; REAL_ADD_LDISTRIB] THEN
2322 SIMP_TAC[REAL_LDISTRIB; REAL_ARITH` (a*b)*c = a *b * c `;
2323   REAL_FIELD` &0 < b ==> ( a / b ) * ( a / b ) * c * b pow 2 = a pow 2 * c `;
2324   REAL_ARITH` &2 * a * b * c / &2 * d = a * b * d * c `] THEN
2325 SIMP_TAC[REAL_FIELD` &0 < a ==> ( b / a ) * ( bb / a ) * a pow 2
2326   * d = b * bb * d `] THEN
2327 SIMP_TAC[REAL_FIELD` &0 < a ==> b / a / &2 * a pow 2 =
2328   a * b / &2 `] THEN SIMP_TAC[REAL_FIELD` &0 < b ==> ( a / b ) * b pow 2 = a * b `;
2329   REAL_RDISTRIB; REAL_FIELD` &0 < b ==> ( a / b ) * ( aa / b ) * c *
2330 b pow 2 = a * aa * c `; REAL_ADD_LDISTRIB] THEN
2331 SIMP_TAC[REAL_LDISTRIB; REAL_ARITH` (a*b)*c = a *b * c `;
2332   REAL_FIELD` &0 < b ==> ( a / b ) * ( a / b ) * c * b pow 2 = a pow 2 * c `;
2333   REAL_ARITH` &2 * a * b * c / &2 * d = a * b * d * c `] THEN
2334 SIMP_TAC[REAL_FIELD` &0 < a ==> ( b / a ) * ( bb / a ) * a pow 2
2335   * d = b * bb * d `] THEN
2336 SIMP_TAC[REAL_FIELD` &0 < a ==> b / a / &2 * a pow 2 =
2337   a * b / &2 `] THEN
2338 DISCH_TAC THEN REWRITE_TAC[chi; rho_ij'; delta] THEN
2339 REAL_ARITH_TAC);;
2340
2341 let AFFINE_HULL_3 = prove
2342  (`affine hull {a,b,c} =
2343     { u % a + v % b + w % c | u + v + w = &1}`,
2344   SIMP_TAC[AFFINE_HULL_FINITE; FINITE_INSERT; FINITE_RULES] THEN
2345   SIMP_TAC[AFFINE_HULL_FINITE_STEP; FINITE_INSERT; FINITE_RULES] THEN
2346   REWRITE_TAC[REAL_ARITH `x - y = z:real <=> x = y + z`;
2347               VECTOR_ARITH `x - y = z:real^N <=> x = y + z`] THEN
2348   REWRITE_TAC[VECTOR_ADD_RID; REAL_ADD_RID] THEN SET_TAC[]);;
2349
2350 let AFFINE_HULL_4 = prove
2351  (`affine hull {a,b,c,d} =
2352     { u % a + v % b + w % c + z % d | u + v + w + z = &1}`,
2353   SIMP_TAC[AFFINE_HULL_FINITE; FINITE_INSERT; FINITE_RULES] THEN
2354   SIMP_TAC[AFFINE_HULL_FINITE_STEP; FINITE_INSERT; FINITE_RULES] THEN
2355   REWRITE_TAC[REAL_ARITH `x - y = z:real <=> x = y + z`;
2356               VECTOR_ARITH `x - y = z:real^N <=> x = y + z`] THEN
2357   REWRITE_TAC[VECTOR_ADD_RID; REAL_ADD_RID] THEN SET_TAC[]);;
2358
2359
2360 let PROVE_EXISTS_CIR_OF_FOUR_POINTS = prove(`!(v1:real^3) v2 v3 v4.
2361          CARD {v1, v2, v3, v4} = 4 /\ ~coplanar_alt {v1, v2, v3, v4}
2362          ==> (? p. p IN affine hull {v1, v2, v3, v4} /\
2363              (?r. !v. v IN {v1, v2, v3, v4}
2364                       ==> r = dist (p, v))) `,
2365 NHANH (REWRITE_RULE[RIGHT_FORALL_IMP_THM]  (GEN `p:real^3` PROVE_DIST_FROM_V1)) THEN
2366 NHANH (REWRITE_RULE[RIGHT_FORALL_IMP_THM]  (GEN `p:real^3` PROVE_EQ_DIST_FROM4 )) THEN
2367 REPEAT GEN_TAC THEN REPEAT LET_TAC THEN ABBREV_TAC `rr = &1 / &2 *
2368        rho_ij' x12 x13 x14 x23 x24 x34 / (&2 * delta x12 x13 x14 x23 x24 x34) ` THEN
2369 REWRITE_TAC[GSYM POS_EQ_NOT_COPLANANR] THEN
2370 NHANH (SPEC_ALL REAL_POS_NZ) THEN ASM_SIMP_TAC[] THEN
2371 NHANH (NOT_0_IMP_SUM_CHI_1 ) THEN ASM_SIMP_TAC[] THEN
2372 REWRITE_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC;
2373   REAL_ARITH ` &1 / a * b = b / a `] THEN
2374 REWRITE_TAC[FORALL_IN_CLAUSES; MESON[]`(? r. (r:real) = a /\
2375   r = b /\ r = c /\ r = d ) <=> a = b /\ a = c /\ a = d `] THEN
2376 REWRITE_TAC[MESON[]` (! x. x = a ==> P a ) <=> P a `] THEN DISCH_TAC THEN
2377 EXISTS_TAC ` chi11 / (&2 * delta x12 x13 x14 x23 x24 x34) % (v1:real^3) +
2378       chi22 / (&2 * delta x12 x13 x14 x23 x24 x34) % v2 +
2379       chi33 / (&2 * delta x12 x13 x14 x23 x24 x34) % v3 +
2380       chi44 / (&2 * delta x12 x13 x14 x23 x24 x34) % v4 ` THEN
2381 CONJ_TAC THENL [REWRITE_TAC[AFFINE_HULL_4; IN_ELIM_THM] THEN
2382 FIRST_X_ASSUM MP_TAC THEN MESON_TAC[NOT_0_IMP_SUM_CHI_1 ];
2383 FIRST_X_ASSUM MP_TAC THEN SIMP_TAC[dist3; DIST_POS_LE; EQ_POW2_COND]]);;
2384
2385
2386
2387
2388
2389
2390
2391
2392
2393
2394
2395
2396 let IMP_PROPERTIES_OF_CIR4 = prove(`!(v1:real^3) v2 v3 v4.
2397          CARD {v1, v2, v3, v4} = 4 /\ ~coplanar_alt {v1, v2, v3, v4}
2398          ==> circumcenter {v1, v2, v3, v4} IN affine hull {v1, v2, v3, v4} /\
2399              (?r. !v. v IN {v1, v2, v3, v4}
2400                       ==> r = dist (circumcenter {v1, v2, v3, v4},v))`,
2401 NHANH (SPEC_ALL PROVE_EXISTS_CIR_OF_FOUR_POINTS ) THEN REWRITE_TAC[circumcenter; IN]
2402 THEN MESON_TAC[EXISTS_THM]);;
2403
2404
2405
2406
2407 let DIST_EQ_IMP_ORTHOGONAL = prove(` dist (pp,v2) = dist (pp,v1) /\
2408   dist (p,v2) = dist (p,v1) ==>
2409   (pp - p ) dot (v2 - v1 ) = &0 `,
2410 REWRITE_TAC[MONG7_ROI; DOT_LSUB] THEN REAL_ARITH_TAC);;
2411
2412
2413
2414 let IMP_OTHO4 = prove(` n dot (v2 - v1) = &0 /\
2415   n dot (v3 - v1) = &0 /\
2416   n dot (v4 - v1) = &0 /\
2417   x IN affine hull {v1,v2,v3,v4} /\
2418   y IN affine hull {v1,v2,v3,v4} ==>
2419   n dot (x - y ) = &0 `,
2420 REWRITE_TAC[AFFINE_HULL_4; IN_ELIM_THM] THEN STRIP_TAC THEN
2421 DOWN_TAC THEN IMP_TAC THEN SIMP_TAC[REAL_ARITH`a + b = c <=> a = c - b `] THEN
2422 PHA THEN REWRITE_TAC[VECTOR_ARITH` ((&1 - (v' + w' + z')) % v1 + v' % v2 +
2423  w' % v3 + z' % v4) - ((&1 - (v + w + z)) % v1 + v % v2 + w % v3 + z % v4)  =
2424   ( v' - v ) % ( v2 - v1 ) + ( w' - w ) % ( v3 - v1 ) +
2425   ( z' - z ) % ( v4 - v1 ) `] THEN
2426 SIMP_TAC[DOT_RADD; DOT_RMUL; ZERO_NEUTRAL]);;
2427
2428
2429
2430
2431
2432 let UNIQUE_EXISISTING_PROPERTY_C4 = prove(`!(v1:real^3) v2 v3 v4.
2433          CARD {v1, v2, v3, v4} = 4 /\ ~coplanar_alt {v1, v2, v3, v4}
2434          ==>   (!p. p IN affine hull {v1, v2, v3, v4} /\
2435                   (?r. !v. v IN {v1, v2, v3, v4} ==> r = dist (p,v))
2436                   ==> p = circumcenter {v1, v2, v3, v4}) `,
2437 NHANH (SPEC_ALL IMP_PROPERTIES_OF_CIR4 ) THEN
2438 REPEAT GEN_TAC THEN
2439 ABBREV_TAC ` pp = circumcenter {(v1:real^3), v2, v3, v4}` THEN
2440 REPEAT STRIP_TAC THEN
2441 DOWN_TAC THEN
2442 REWRITE_TAC[FORALL_IN_CLAUSES] THEN
2443 REWRITE_TAC[MESON[]` r = a /\ r = b /\ r = c /\ r = d <=> r = a /\ b = a /\ c = a
2444   /\ d = a `] THEN
2445 PHA THEN
2446 NHANH (MESON[DIST_EQ_IMP_ORTHOGONAL ]`dist (pp,v2) = dist (pp,v1) /\
2447  dist (pp,v3) = dist (pp,v1) /\
2448  dist (pp,v4) = dist (pp,v1) /\a11/\a2/\
2449  dist (p,v2) = dist (p,v1) /\
2450  dist (p,v3) = dist (p,v1) /\
2451  dist (p,v4) = dist (p,v1) ==>
2452   ( p - pp) dot ( v2 - v1 ) = &0 /\
2453   ( p - pp ) dot ( v3 - v1 ) = &0 /\
2454   ( p - pp ) dot ( v4 - v1 ) = &0 `) THEN
2455 ONCE_REWRITE_TAC[GSYM VECTOR_SUB_EQ] THEN
2456 REWRITE_TAC[GSYM DOT_EQ_0] THEN MESON_TAC[IMP_OTHO4 ]);;
2457
2458
2459
2460
2461 let PROVE_IN_AFFINE_HULL_4 = prove(
2462 `~(delta x12 x13 x14 x23 x24 x34 = &0)
2463  ==> &1 / (&2 * delta x12 x13 x14 x23 x24 x34) %
2464      (chi x12 x13 x14 x23 x24 x34 % v1 +
2465       chi x12 x24 x23 x14 x13 x34 % v2 +
2466       chi x34 x13 x23 x14 x24 x12 % v3 +
2467       chi x34 x24 x14 x23 x13 x12 % v4) IN
2468      affine hull {(v1:real^3), v2, v3, v4}`,
2469 REWRITE_TAC[AFFINE_HULL_4; IN_ELIM_THM; VECTOR_ADD_LDISTRIB;
2470   VECTOR_MUL_ASSOC; REAL_ARITH ` ( &1 / a ) * b = b/a `]
2471  THEN MESON_TAC[NOT_0_IMP_SUM_CHI_1]);;
2472
2473
2474
2475 (* VBVYGGT , le 85 *)
2476
2477
2478
2479 MESON[POW_2_SQRT; DIST_POS_LE]` dist (x,y) pow 2 = r ==> dist (x,y) = sqrt ( r ) `;;
2480
2481 (* LEMMA 85 *)
2482 let VBVYGGT = prove(`!(v1:real^3) v2 v3 v4.
2483          CARD {v1, v2, v3, v4} = 4 /\ ~coplanar_alt {v1, v2, v3, v4}
2484          ==> circumcenter {v1, v2, v3, v4} IN affine hull {v1, v2, v3, v4} /\
2485              (?r. !v. v IN {v1, v2, v3, v4}
2486                       ==> r = dist (circumcenter {v1, v2, v3, v4},v)) /\
2487              (!p. p IN affine hull {v1, v2, v3, v4} /\
2488                   (?r. !v. v IN {v1, v2, v3, v4} ==> r = dist (p,v))
2489                   ==> p = circumcenter {v1, v2, v3, v4}) /\
2490              (let x12 = dist (v1,v2) pow 2 in
2491               let x13 = dist (v1,v3) pow 2 in
2492               let x14 = dist (v1,v4) pow 2 in
2493               let x23 = dist (v2,v3) pow 2 in
2494               let x24 = dist (v2,v4) pow 2 in
2495               let x34 = dist (v3,v4) pow 2 in
2496               let chi11 = chi x12 x13 x14 x23 x24 x34 in
2497               let chi22 = chi x12 x24 x23 x14 x13 x34 in
2498               let chi33 = chi x34 x13 x23 x14 x24 x12 in
2499               let chi44 = chi x34 x24 x14 x23 x13 x12 in
2500               circumcenter {v1, v2, v3, v4} =
2501               &1 / (&2 * delta x12 x13 x14 x23 x24 x34) %
2502               (chi11 % v1 + chi22 % v2 + chi33 % v3 + chi44 % v4)) `,
2503 NHANH (SPEC_ALL UNIQUE_EXISISTING_PROPERTY_C4 ) THEN
2504 NHANH (SPEC_ALL IMP_PROPERTIES_OF_CIR4 ) THEN
2505 REWRITE_TAC[MESON[]` (a /\ b1/\b2) /\ b ==> b1 /\b2/\ b/\ d <=> a /\ b1 /\b2/\b==>d `] THEN
2506 NHANH (REWRITE_RULE[RIGHT_FORALL_IMP_THM] ( GEN `p: real^3 `PROVE_DIST_FROM_V1)) THEN
2507 NHANH (REWRITE_RULE[RIGHT_FORALL_IMP_THM] ( GEN `p: real^3 ` PROVE_EQ_DIST_FROM4)) THEN
2508 REPEAT GEN_TAC THEN REPEAT LET_TAC THEN ABBREV_TAC `rr = &1 / &2 *
2509        rho_ij' x12 x13 x14 x23 x24 x34 / (&2 * delta x12 x13 x14 x23 x24 x34) ` THEN
2510 REWRITE_TAC[MESON[]` (! x. x = a ==> P x ) <=> P a `] THEN
2511 REWRITE_TAC[GSYM POS_EQ_NOT_COPLANANR] THEN
2512 NHANH (REAL_ARITH` &0 < a ==> ~( a = &0 )`) THEN
2513 NHANH (PROVE_IN_AFFINE_HULL_4 ) THEN
2514 UNDISCH_TAC ` dist ((v1:real^3),v2) pow 2 = x12` THEN
2515 UNDISCH_TAC ` dist ((v1:real^3),v3) pow 2 = x13` THEN
2516 UNDISCH_TAC ` dist ((v1:real^3),v4) pow 2 = x14` THEN
2517 UNDISCH_TAC ` dist ((v2:real^3),v3) pow 2 = x23` THEN
2518 UNDISCH_TAC ` dist ((v2:real^3),v4) pow 2 = x24` THEN
2519 UNDISCH_TAC ` dist ((v3:real^3),v4) pow 2 = x34` THEN
2520 UNDISCH_TAC ` chi x12 x13 x14 x23 x24 x34 = chi11 ` THEN
2521 UNDISCH_TAC ` chi x12 x24 x23 x14 x13 x34 = chi22 ` THEN
2522 UNDISCH_TAC ` chi x34 x13 x23 x14 x24 x12 = chi33` THEN
2523 UNDISCH_TAC ` chi x34 x24 x14 x23 x13 x12 = chi44` THEN
2524 REWRITE_TAC[MESON[]` a = b ==> P a <=> a = b ==> P b `] THEN
2525 ABBREV_TAC ` w =  &1 / (&2 * delta x12 x13 x14 x23 x24 x34) %
2526      (chi11 % (v1:real^3) + chi22 % v2 + chi33 % v3 + chi44 % v4)` THEN
2527 REWRITE_TAC[MESON[]` a /\ b ==> c <=> a ==> b ==> c `]
2528 THEN REPLICATE_TAC 13 DISCH_TAC THEN
2529 REWRITE_TAC[FORALL_IN_CLAUSES;dist3] THEN PHA THEN
2530 NHANH (MESON[POW_2_SQRT; DIST_POS_LE]` dist (x,y) pow 2 = r
2531  ==> dist (x,y) = sqrt ( r ) `) THEN MESON_TAC[]);;
2532
2533 let NOT_COPLANAR_IMP_EXISTS_CIR = prove(`! (v1:real^3) v2 v3 v4.
2534        CARD {v1, v2, v3, v4} = 4 /\ ~coplanar_alt {v1, v2, v3, v4}
2535        ==> circumcenter {v1, v2, v3, v4} IN affine hull {v1, v2, v3, v4} /\
2536            (?r. !v. v IN {v1, v2, v3, v4}
2537                     ==> r = dist (circumcenter {v1, v2, v3, v4},v)) `,
2538 MESON_TAC[VBVYGGT]);;
2539
2540 let THREE_POINTS_COP = prove(` ! v1 v2 (v3:real^3). coplanar_alt {v1,v2,v3} `,
2541 MESON_TAC[DIMINDEX_3; ARITH_RULE` 2 <= 3 `; COPLANAR_3]);;
2542
2543 let PER_SET4 = SET_RULE ` {a,b,c,d} = {b,a,c,d} /\
2544   {a,b,c,d} = {c,b,a,d} /\
2545   {a,b,c,d} = {d,b,c,a} `;;
2546
2547 let NOT_COPLANAR_IMP_CARD4 = prove(` ~ coplanar_alt {(v1:real^3), v2, v3, v4}
2548 ==> CARD {v1, v2, v3, v4} = 4 `, REWRITE_TAC[CARD4; IN_SET3] THEN
2549 MP_TAC (GEN_ALL THREE_POINTS_COP ) THEN
2550 MESON_TAC[PER_SET4; SET_RULE` {a,a,b,c} = {a,b,c} `]);;
2551
2552
2553 let NOT_COPLANAR_IMP_EXISTS_CIR2 = MESON[NOT_COPLANAR_IMP_EXISTS_CIR ;
2554 NOT_COPLANAR_IMP_CARD4 ]` ! (v1:real^3) v2 v3 v4. ~ coplanar_alt {v1, v2, v3, v4}
2555        ==> circumcenter {v1, v2, v3, v4} IN affine hull {v1, v2, v3, v4} /\
2556            (?r. !v. v IN {v1, v2, v3, v4}
2557                     ==> r = dist (circumcenter {v1, v2, v3, v4},v)) `;;
2558
2559 let NOT_COPLANAR_IMP_RADV_PROPERTIES = prove(` ~coplanar_alt {(v1:real^3), v2, v3, v4} ==>
2560   (! w. {v1, v2, v3, v4} w ==> radV {v1, v2, v3, v4}
2561     = dist (circumcenter {v1,v2,v3,v4} ,w) ) `,
2562 NHANH (SPEC_ALL NOT_COPLANAR_IMP_EXISTS_CIR2) THEN
2563 REWRITE_TAC[IN; radV] THEN MESON_TAC[EXISTS_THM]);;
2564
2565 let ZJEWPAP = ` ! v1 v2 v3 (v4:real^3).
2566   let s = {v1, v2, v3, v4} in CARD s = 4 /\ ~ coplanar_alt s
2567   ==> radV {v1,v2,v3}  <= radV s  `;;
2568
2569 let PHA = REWRITE_TAC[MESON[]` ( a ==> b ==> c <=> a /\ b ==> c ) /\
2570   ( (a /\ b ) /\ c <=> a /\ b /\ c ) `];;
2571
2572 let NOT_COL_EQ_UPS_X_POS = prove(`! v1 v2 v3.  ~ collinear {(v1:real^3), v2, v3} <=>
2573            &0 < ups_x (dist (v1,v2) pow 2) (dist (v1,v3) pow 2)
2574            (dist (v2,v3) pow 2) `,
2575 MP_TAC (GEN_ALL ZERO_LE_UPS_X) THEN REWRITE_TAC[UPS_X_EQ_ZERO_COND] THEN
2576 REWRITE_TAC[UPS_X_EQ_ZERO_COND; REAL_ARITH` a <= b <=> a = b \/ a < b `] THEN
2577 REWRITE_TAC[dist3] THEN MESON_TAC[REAL_ARITH` ~( a = b /\ a < b ) `]);;
2578
2579
2580 let ETA_Y_POW2_EQ = prove(`(dist (v1,v2) pow 2 * dist (v1,v3) pow 2 * dist (v2,v3) pow 2) /
2581       ups_x (dist (v1,v2) pow 2) (dist (v1,v3) pow 2) (dist (v2,v3) pow 2) =
2582 ( eta_y (dist3 v2 v3) (dist3 v1 v3) (dist3 v1 v2)) pow 2 `,
2583 REWRITE_TAC[eta_y;dist3; eta_x] THEN LET_TR THEN
2584 REWRITE_TAC[GSYM REAL_POW_2; GSYM dist3 ] THEN
2585 SIMP_TAC[MESON[UPS_X_SYM]` ups_x a b c = ups_x c b a `;
2586 REAL_ARITH ` a * b * c = c * b * a `] THEN
2587 MESON_TAC[SQRT_WORKS; REAL_LE_SQUARE_POW; REAL_LE_MUL;
2588   REAL_LE_DIV; dist3 ; ZERO_LE_UPS_X; UPS_X_SYM]);;
2589
2590
2591 let ETA_Y_POS_LE = prove(` &0 <= eta_y (dist3 v1 v2) (dist3 v1 v3) (dist3 v2 v3) `,
2592 REWRITE_TAC[eta_y; eta_x] THEN LET_TR THEN REWRITE_TAC[GSYM REAL_POW_2] THEN
2593 MESON_TAC[REAL_LE_POW_2; REAL_LE_MUL; ZERO_LE_UPS_X; REAL_LE_DIV;
2594   SQRT_POS_LE]);;
2595
2596
2597 (* lemma 87 *)
2598 let ZJEWPAP = prove(` ! v1 v2 v3 (v4:real^3).
2599   let s = {v1, v2, v3, v4} in CARD s = 4 /\ ~ coplanar_alt s
2600   ==> radV {v1,v2,v3}  <= radV s  `,
2601 LET_TR THEN
2602 NHANH (MESON[COLLINEAR_IMP_COPLANAR ]`~coplanar_alt {v1, v2, v3, v4}
2603   ==> ~ collinear {(v1:real^3),v2,v3} `) THEN
2604 SIMP_TAC[NOT_COLL_IMP_RADV_EQ_ETA_Y] THEN
2605 REWRITE_TAC[MESON[]` a /\ b /\ c <=> (a/\b)/\c`] THEN
2606 NHANH (SPEC_ALL VBVYGGT) THEN
2607 REPEAT GEN_TAC THEN
2608 NHANH (NOT_COPLANAR_IMP_RADV_PROPERTIES) THEN
2609 ABBREV_TAC ` pp = circumcenter {(v1:real^3), v2, v3, v4}` THEN
2610 MP_TAC (SPECL [`pp :real^3`; ` v1: real^3`; `v2:real^3`; ` v3:real^3`] DELTA_POS_4POINTS ) THEN
2611 REWRITE_TAC[REWRITE_RULE[IN] FORALL_IN_CLAUSES;
2612    FORALL_IN_CLAUSES ] THEN
2613 REWRITE_TAC[MESON[]` ( a ==> b ==> c <=> a /\ b ==> c ) /\
2614   ( (a /\ b ) /\ c <=> a /\ b /\ c ) `] THEN
2615 REPEAT STRIP_TAC THEN
2616 UNDISCH_TAC ` &0 <=
2617       delta (dist ((pp:real^3),v1) pow 2) (dist (pp,v2) pow 2) (dist (pp,v3) pow 2)
2618       (dist (v1,v2) pow 2)
2619       (dist (v1,v3) pow 2)
2620       (dist (v2,v3) pow 2)` THEN
2621 ABBREV_TAC `p1 = dist ((pp:real^3),v1)` THEN
2622 ABBREV_TAC `p2 = dist ((pp:real^3),v2)` THEN
2623 ABBREV_TAC `p3 = dist ((pp:real^3),v3)` THEN
2624  REPLICATE_TAC 3 (FIRST_X_ASSUM MP_TAC THEN MATCH_MP_TAC
2625 (MESON[]` a ==> b ==> a `)) THEN
2626 EXPAND_TAC "p1" THEN
2627 EXPAND_TAC "p2" THEN
2628 EXPAND_TAC "p3" THEN
2629 FIRST_X_ASSUM MP_TAC THEN
2630 REWRITE_TAC[NOT_COL_EQ_UPS_X_POS ] THEN
2631 REWRITE_TAC[NOT_COL_EQ_UPS_X_POS; DELTA_RRR_INTERPRETE] THEN
2632 SIMP_TAC[REAL_FIELD` &0 < a ==> -- b * c + r * a = a * ( r - ( b * c )  / a ) `] THEN
2633 SIMP_TAC[ETA_Y_POW2_EQ; REAL_LE_MUL_EQ] THEN
2634 UNDISCH_TAC ` radV {(v1:real^3), v2, v3, v4} = p1 ` THEN
2635 SIMP_TAC[] THEN
2636 EXPAND_TAC "p1" THEN
2637 UNDISCH_TAC `r = dist ((pp: real^3),v4)` THEN
2638 SIMP_TAC[] THEN
2639 REPLICATE_TAC 3 REMOVE_TAC THEN
2640 SIMP_TAC[ETA_Y_SYYM; REAL_ARITH` &0 <= a - b <=> b <= a `] THEN
2641 MESON_TAC[DIST_POS_LE; POW2_COND; ETA_Y_POS_LE ]);;
2642
2643
2644
2645
2646
2647 let NOT_EQ_BASIS_IMP_OTHORGANAL = MESON[DOT_BASIS_BASIS_UNEQUAL]
2648 ` ! i j. ~( i = j ) ==> basis i dot basis j = &0 `;;
2649
2650 let BASIS_DIS_OTHORGONAL =
2651 MESON[ARITH_RULE` ~( 1 = 2 \/ 1 = 3 \/ 2 = 3 ) `; NOT_EQ_BASIS_IMP_OTHORGANAL]
2652 ` basis 1 dot basis 2 = &0 /\
2653   basis 1 dot basis 3 = &0 /\
2654   basis 2 dot basis 3 = &0 ` ;;
2655
2656 let NORM_BASIS_VEC3 = prove(` ! i. i = 1 \/ i = 2 \/ i = 3 ==>
2657 norm (( basis i ):real^3 ) = &1 `,
2658 MESON_TAC[DIMINDEX_3; ARITH_RULE` i = 1 \/ i = 2 \/ i = 3 <=>
2659   1 <= i /\ i <= 3`; NORM_BASIS]);;
2660
2661 let AAA_LEMMA = prove(` &0 < a /\
2662  a <= b /\
2663  b <= c /\ ll ==> &0 <= b pow 2 - a pow 2 /\ &0 <= c pow 2 - b pow 2 `,
2664 REWRITE_TAC[REAL_ARITH` &0 <= a - b <=> b <= a `] THEN
2665 MESON_TAC[REAL_LT_IMP_LE; POW2_COND; POS_IMP_POW2; REAL_LE_TRANS]);;
2666
2667 let LLEEMAA = prove(` &0 < a /\
2668      a <= b /\
2669      b <= c /\
2670      &0 < a' /\
2671      a' <= b' /\
2672      b' <= c' /\
2673      a <= a' /\
2674      b <= b' /\
2675      c <= c' /\ l ==> &0 <= a' pow 2 - a pow 2 /\
2676   &0 <= b' pow 2 - b pow 2 /\
2677   &0 <= c' pow 2 - c pow 2 `,
2678 REWRITE_TAC[REAL_ARITH` &0 <= a - b <=> b <= a `] THEN
2679 MESON_TAC[POS_IMP_POW2; REAL_ARITH` a < b ==> a <= b `;
2680   REAL_LE_TRANS]);;
2681
2682 let TYUNJLA = prove(` !(e1:real^3) e2 e3 a b c a' b' c' t1 t2 t3.
2683   e1 = basis 1 /\
2684      e2 = basis 2 /\
2685      e3 = basis 3 /\
2686      &0 < a /\
2687      a <= b /\
2688      b <= c /\
2689      &0 < a' /\
2690      a' <= b' /\
2691      b' <= c' /\
2692      a <= a' /\
2693      b <= b' /\
2694      c <= c' /\
2695      (!x. x IN {t1, t2, t3} ==> &0 < x) /\
2696      t1 + t2 + t3 < &1 /\
2697      v =
2698      ((t1 + t2 + t3) * a) % e1 +
2699      ((t2 + t3) * sqrt (b pow 2 - a pow 2)) % e2 +
2700      (t3 * sqrt (c pow 2 - b pow 2)) % e3 /\
2701   v' = ((t1 + t2 + t3) * a') % e1 +
2702      ((t2 + t3) * sqrt (b' pow 2 - a' pow 2)) % e2 +
2703      (t3 * sqrt (c' pow 2 - b' pow 2)) % e3 ==>
2704   norm v <= norm v' `,
2705 REPEAT STRIP_TAC THEN FIRST_X_ASSUM MP_TAC THEN
2706 FIRST_X_ASSUM MP_TAC THEN
2707 SIMP_TAC[POW2_COND; NORM_POS_LE; NORM_POW_2; DOT_LADD; DOT_RADD;
2708 DOT_LMUL; DOT_RMUL] THEN ASM_SIMP_TAC[] THEN
2709 SIMP_TAC[GSYM NORM_POW_2; NORM_BASIS_VEC3 ] THEN
2710 SIMP_TAC[BASIS_DIS_OTHORGONAL; MESON[DOT_SYM; BASIS_DIS_OTHORGONAL]
2711   ` basis 2 dot basis 1 = &0 /\ basis 3 dot basis 1 = &0 /\
2712   basis 3 dot basis 2 = &0 `; ZERO_NEUTRAL] THEN
2713 REWRITE_TAC[REAL_ARITH` (a * x ) * ( b * x ) * c = a * b * c * x pow 2 `] THEN
2714 REPEAT STRIP_TAC THEN DOWN_TAC THEN
2715 NHANH (AAA_LEMMA) THEN PHA THEN
2716 NHANH (MESON[AAA_LEMMA]` &0 < a /\ a <= b /\ b <= c /\ aa <= a /\ l ==>
2717   &0 <= b pow 2 - a pow 2 /\ &0 <= c pow 2 - b pow 2 `) THEN
2718 SIMP_TAC[SQRT_WORKS] THEN
2719 ONCE_REWRITE_TAC[REAL_ARITH` a <= b <=> &0 <= b - a `] THEN
2720 REWRITE_TAC[REAL_ARITH` ((t1 + t2 + t3) * (t1 + t2 + t3) * &1 pow 2 * a' pow 2 +
2721       (t2 + t3) * (t2 + t3) * &1 pow 2 * (b' pow 2 - a' pow 2) +
2722       t3 * t3 * &1 pow 2 * (c' pow 2 - b' pow 2)) -
2723      ((t1 + t2 + t3) * (t1 + t2 + t3) * &1 pow 2 * a pow 2 +
2724       (t2 + t3) * (t2 + t3) * &1 pow 2 * (b pow 2 - a pow 2) +
2725       t3 * t3 * &1 pow 2 * (c pow 2 - b pow 2)) =
2726   t1 * ( t1 + &2 * t2 + &2 * t3 ) * ( a' pow 2 - a pow 2 ) +
2727   t2 * (t2 + &2 * t3 ) * ( b' pow 2 - b pow 2 ) +
2728   t3 pow 2 * ( c' pow 2 - c pow 2 ) `] THEN
2729 REWRITE_TAC[REAL_ARITH` &0 <= a - b <=> b <= a `] THEN
2730 PHA THEN NHANH (LLEEMAA) THEN STRIP_TAC THEN
2731 UNDISCH_TAC ` (!x. x IN {t1, t2, t3} ==> &0 < x)` THEN
2732 REPLICATE_TAC 3 ( FIRST_X_ASSUM MP_TAC) THEN
2733 REWRITE_TAC[FORALL_IN_CLAUSES] THEN PHA THEN
2734 NHANH (REAL_ARITH` &0 < t1 /\ &0 < t2 /\ &0 < t3 ==>
2735   &0 <= t1 /\ &0 <= t2 /\ &0 <= t1 + &2 * t2 + &2 * t3 /\
2736   &0 <= t2 + &2 * t3 `) THEN
2737 MESON_TAC[REAL_LE_ADD; REAL_LE_MUL; REAL_LE_POW_2]);;
2738
2739 let LEMMA83 = TYUNJLA ;;
2740
2741 let DELTA_TRIPLE_SUB_H_EXPAND = prove(`
2742 delta (a01 - h) (a02 - h) (a03 - h) x12 x13 x23 =
2743   delta a01 a02 a03 x12 x13 x23 - h * ups_x x12 x13 x23 `,
2744 REWRITE_TAC[delta;ups_x] THEN REAL_ARITH_TAC);;
2745
2746 let PROVE_EXISTS_H_DELTA_0 = prove(`&0 < ups_x x12 x13 x23 /\ &0 <= delta a01 a02 a03 x12 x13 x23
2747  ==> (?h. &0 <= h /\ h = ( delta a01 a02 a03 x12 x13 x23 ) / ups_x x12 x13 x23 /\
2748  delta (a01 - h) (a02 - h) (a03 - h) x12 x13 x23 = &0 )`,
2749 REWRITE_TAC[DELTA_TRIPLE_SUB_H_EXPAND] THEN
2750 DISCH_TAC THEN
2751 EXISTS_TAC`( delta a01 a02 a03 x12 x13 x23 ) / ups_x x12 x13 x23` THEN
2752 ASM_SIMP_TAC[REAL_LT_IMP_LE; REAL_LE_DIV] THEN
2753 FIRST_X_ASSUM MP_TAC THEN CONV_TAC REAL_FIELD);;
2754
2755 let FIRST_POINT_IN_AFF3 = prove(` ! w v1 v2. w IN aff {w,v1,v2} `,
2756 REWRITE_TAC[aff; AFFINE_HULL_3; IN_ELIM_THM] THEN REPEAT GEN_TAC THEN
2757 EXISTS_TAC ` &1 ` THEN EXISTS_TAC `&0` THEN EXISTS_TAC `&0` THEN
2758 REWRITE_TAC[ZERO_NEUTRAL] THEN CONV_TAC VECTOR_ARITH);;
2759
2760 let THREE_GEN_POINTS_IN_AFF3 = MESON[PER_SET3; FIRST_POINT_IN_AFF3 ]` a IN aff {a,b,c} /\
2761   b IN aff {a,b,c} /\ c IN aff {a,b,c} `;;
2762
2763 let PROVE_THE_HYPOTHESI_FOR_74 = prove(` (let s = {v1, v2, v3, v4} in
2764          CARD s = 4 /\
2765
2766          ~coplanar_alt s /\
2767          eta_y (dist3 v1 v2 ) (dist3 v1 v3) (dist3 v2 v3) <= r )
2768 ==> ( let x12 = dist3 v1 v2 pow 2 in
2769      let x13 = dist3 v1 v3 pow 2 in
2770      let x23 = dist3 v2 v3 pow 2 in
2771      CARD {v1, v2, v3, v4} = 4 /\
2772
2773      ~coplanar_alt {v1, v2, v3, v4} /\
2774      &0 <= r pow 2 /\
2775      &0 <= r pow 2 /\
2776      &0 <= r pow 2 /\
2777      delta (r pow 2) (r pow 2) (r pow 2) x12 x13 x23 >= &0 ) `,
2778 REPEAT LET_TAC THEN
2779 SIMP_TAC[REAL_LE_POW_2] THEN
2780 REWRITE_TAC[DELTA_RRR_INTERPRETE] THEN
2781 EXPAND_TAC "s" THEN
2782 NHANH (MESON[COLLINEAR_IMP_COPLANAR]` ~ coplanar_alt {v1, v2, v3, v} ==>
2783   ~ collinear {v1, v2, (v3:real^3)} `) THEN
2784 REWRITE_TAC[NOT_COL_EQ_UPS_X_POS] THEN
2785 EXPAND_TAC "x12" THEN
2786 EXPAND_TAC "x13" THEN
2787 EXPAND_TAC "x23" THEN
2788 REWRITE_TAC[dist3] THEN
2789 SIMP_TAC[REAL_FIELD` &0 < a ==> -- x * y + r * a = a * ( r - (x * y ) / a )`] THEN
2790 SIMP_TAC[ETA_Y_POW2_EQ;dist3; ETA_Y_SYYM] THEN
2791 MP_TAC ETA_Y_POS_LE THEN
2792 DAO THEN PHA THEN
2793 REWRITE_TAC[dist3] THEN DAO THEN
2794 NHANH (MESON[POS_IMP_POW2]` a <= b /\ &0 <= a ==>
2795   a pow 2 <= b pow 2 `) THEN
2796 ONCE_REWRITE_TAC[REAL_ARITH` a <= b <=> &0 <= b - a `] THEN
2797 REWRITE_TAC[REAL_ARITH` a >= &0 <=> &0 <= a `] THEN
2798 SIMP_TAC[REAL_LT_IMP_LE; REAL_LE_MUL]);;
2799
2800
2801 let INSERT_SUBSET = SET_RULE` {} SUBSET s /\
2802   ( ( a INSERT s ) SUBSET ss <=> a IN ss /\ s SUBSET  ss ) `;;
2803
2804
2805 let IMP_TAC = REWRITE_TAC[MESON[]` a /\ b ==> c <=> a ==> b ==> c `];;
2806
2807 let IMP_OTHORGONAL_AFF3 = prove(`!v1 v2 v3 u.
2808      u dot (v1 - v2) = &0 /\ u dot (v1 - v3) = &0
2809      ==> (!x y. {x, y} SUBSET aff {v1, v2, v3} ==> u dot (x - y) = &0)`,
2810 REWRITE_TAC[aff; AFFINE_HULL_3; INSERT_SUBSET; IN_ELIM_THM] THEN
2811 REPEAT STRIP_TAC THEN DOWN_TAC THEN
2812 REWRITE_TAC[MESON[]` a /\ b ==> c <=> a ==> b ==> c `] THEN
2813 SIMP_TAC[REAL_ARITH` a + b = &1 <=> a = &1 - b `] THEN
2814 REWRITE_TAC[VECTOR_ARITH` ((&1 - (v + w)) % v1 + v % v2 + w % v3) -
2815       ((&1 - (v' + w')) % v1 + v' % v2 + w' % v3) =
2816   ( v' - v ) % ( v1 - v2 ) + ( w' - w ) % ( v1 - v3 ) `] THEN REPEAT STRIP_TAC
2817  THEN ASM_SIMP_TAC[DOT_RADD; DOT_RMUL; ZERO_NEUTRAL]);;
2818
2819
2820 (* MONG7_ROI *)
2821
2822 let DIST_EQ_IMP_OTHORGONAL = prove(` ! a b p q. dist (p,a) = dist (p,b) /\ dist (q,a) = dist(q,b)
2823 ==> ( p - q ) dot ( a - b ) = &0 `,
2824 REWRITE_TAC[MONG7_ROI; DOT_LSUB] THEN REAL_ARITH_TAC);;
2825
2826 let NOT_COPLANAR_IMP_NOT_COLLINEAR =
2827   MATCH_MP (MESON[]` (a ==> b) ==> ~ b ==> ~ a `) (SPEC_ALL COLLINEAR_IMP_COPLANAR);;
2828
2829 (* lemma 89 *)
2830 let PVLJZLA = prove( `! (v1:real^3) v2 v3 v4.
2831      let s = {v1, v2, v3, v4} in
2832      ~coplanar_alt s
2833      ==> (circumcenter s IN conv0 s <=>
2834           orientation s v1 (\x. &0 < x) /\
2835           orientation s v2 (\x. &0 < x) /\
2836           orientation s v3 (\x. &0 < x) /\
2837           orientation s v4 (\x. &0 < x))`,
2838 REWRITE_TAC[orientation; affsign] THEN
2839 REPEAT GEN_TAC THEN
2840 LET_TR THEN
2841 REWRITE_TAC[lin_combo] THEN
2842 REWRITE_TAC[SET_RULE` s DIFF {a} UNION {a} = s UNION {a} `;
2843   SET_RULE` {a,b,c,d} UNION {a} = {a,b,c,d} /\
2844   {a,b,c,d} UNION {b} = {a,b,c,d} /\
2845   {a,b,c,d} UNION {c} = {a,b,c,d} /\
2846   {a,b,c,d} UNION {d} = {a,b,c,d}`] THEN
2847 REWRITE_TAC[MESON[]`a = b /\ c /\ d <=> c /\ d /\ b = a `] THEN
2848 REWRITE_TAC[SET_RULE` (!w. {v1} w ==> &0 < f w) /\
2849            sum {v1, v2, v3, v4} f = &1 /\ l
2850   <=> (!w. w IN {v1,v2,v3,v4} ==> {v1} w ==> &0 < f w) /\
2851   sum {v1, v2, v3, v4} f = &1 /\ l `;
2852   SET_RULE` (!w. {v2} w ==> &0 < f w) /\
2853            sum {v1, v2, v3, v4} f = &1 /\ l
2854   <=> (!w. w IN {v1,v2,v3,v4} ==> {v2} w ==> &0 < f w) /\
2855   sum {v1, v2, v3, v4} f = &1 /\ l `;
2856   SET_RULE` (!w. {v2} w ==> &0 < f w) /\
2857            sum {v1, v2, v3, v4} f = &1 /\ l
2858   <=> (!w. w IN {v1,v2,v3,v4} ==> {v2} w ==> &0 < f w) /\
2859   sum {v1, v2, v3, v4} f = &1 /\ l `;
2860   SET_RULE` (!w. {v3} w ==> &0 < f w) /\
2861            sum {v1, v2, v3, v4} f = &1 /\ l
2862   <=> (!w. w IN {v1,v2,v3,v4} ==> {v3} w ==> &0 < f w) /\
2863   sum {v1, v2, v3, v4} f = &1 /\ l `;
2864   SET_RULE` (!w. {v4} w ==> &0 < f w) /\
2865            sum {v1, v2, v3, v4} f = &1 /\ l
2866   <=> (!w. w IN {v1,v2,v3,v4} ==> {v4} w ==> &0 < f w) /\
2867   sum {v1, v2, v3, v4} f = &1 /\ l `] THEN
2868  SIMP_TAC[AFFINE_HULL_FINITE_STEP_GEN;
2869             REAL_ARITH `&0 < x /\ &0 < y  ==> &0 < x + y`;
2870             REAL_ARITH ` &0 < x ==> &0 < x / &2`;
2871             FINITE_INSERT; CONJUNCT1 FINITE_RULES
2872 ; RIGHT_EXISTS_AND_THM]  THEN
2873 NHANH (NOT_COPLANAR_IMP_CARD4) THEN
2874 SIMP_TAC[IN_ACT_SING; CARD4; IN_SET3; DE_MORGAN_THM] THEN
2875 REWRITE_TAC[REAL_ARITH` a - b = c <=> a = b + c `; ZERO_NEUTRAL;
2876   VECTOR_ARITH`(a:real^N) - b = c <=> a = b + c `; VECTOR_ARITH` x +
2877   vec 0 = x `] THEN
2878 REWRITE_TAC[CONV0_4; IN_ELIM_THM] THEN
2879 NHANH (SPEC ` circumcenter {(v1:real^3), v2, v3, v4} ` ( GEN `v:real^3` (SPEC_ALL COEFS_4))) THEN
2880 STRIP_TAC THEN
2881 EQ_TAC THENL [
2882 MESON_TAC[];
2883 UNDISCH_TAC ` !ta tb tc td.
2884           circumcenter {v1, v2, v3, v4} =
2885           ta % v1 + tb % v2 + tc % v3 + td % v4 /\
2886           ta + tb + tc + td = &1
2887           ==> ta = COEF4_1 v1 v2 v3 v4 (circumcenter {v1, v2, v3, v4}) /\
2888               tb = COEF4_2 v1 v2 v3 v4 (circumcenter {v1, v2, v3, v4}) /\
2889               tc = COEF4_3 v1 v2 v3 v4 (circumcenter {v1, v2, v3, v4}) /\
2890               td = COEF4_4 v1 v2 v3 v4 (circumcenter {v1, v2, v3, v4})` THEN
2891 REWRITE_TAC[MESON[]`&0 < v /\ ( ? b . P v b ) <=>
2892   (? b. &0 < v /\ P v b ) `] THEN
2893 REWRITE_TAC[MESON[]` &1 = a /\ aa = b <=> a = &1 /\ b = aa `] THEN
2894 ABBREV_TAC ` (vv:real^3) = circumcenter {v1, v2, v3, v4} ` THEN
2895 ABBREV_TAC ` a1 = COEF4_1 v1 v2 v3 v4 vv ` THEN
2896 ABBREV_TAC ` a2 = COEF4_2 v1 v2 v3 v4 vv ` THEN
2897 ABBREV_TAC ` a3 = COEF4_3 v1 v2 v3 v4 vv ` THEN
2898 ABBREV_TAC ` a4 = COEF4_4 v1 v2 v3 v4 vv ` THEN PHA THEN
2899 IMP_TAC THEN STRIP_TAC THEN STRIP_TAC THEN
2900 REPLICATE_TAC 4 (FIRST_X_ASSUM MP_TAC) THEN PHA THEN
2901 NHANH (MESON[]`(!ta tb tc td.
2902       vv = ta % v1 + tb % v2 + tc % v3 + td % v4 /\ ta + tb + tc + td = &1
2903       ==> ta = a1 /\ tb = a2 /\ tc = a3 /\ td = a4) /\
2904  a111  /\
2905  v + v' + v'' + v''' = &1 /\
2906  v % v1 + v' % v2 + v'' % v3 + v''' % v4 = vv /\
2907  (?v v' v'' v'''.
2908       &0 < v' /\
2909       v + v' + v'' + v''' = &1 /\
2910       v % v1 + v' % v2 + v'' % v3 + v''' % v4 = vv) /\
2911  (?v v' v'' v'''.
2912       &0 < v'' /\
2913       v + v' + v'' + v''' = &1 /\
2914       v % v1 + v' % v2 + v'' % v3 + v''' % v4 = vv) /\
2915  (?v v' v'' v'''.
2916       &0 < v''' /\
2917       v + v' + v'' + v''' = &1 /\
2918       v % v1 + v' % v2 + v'' % v3 + v''' % v4 = vv) ==>
2919   &0 < v' /\ &0 < v'' /\ &0 < v''' `) THEN MESON_TAC[]]);;
2920
2921
2922
2923
2924 let IMP_IN_AFF_LT = prove(`CARD {v1, v2, v3, v4} = 4 ==> ( (?v v' v'' v'''.
2925            v < &0 /\
2926            &1 = v + v' + v'' + v''' /\ vv =
2927            v % v1 + v' % v2 + v'' % v3 + v''' % v4) <=>
2928   vv IN aff_lt {v2,v3,v4} {v1} ) `,
2929 REWRITE_TAC[CARD4; IN_SET3; DE_MORGAN_THM] THEN SIMP_TAC[AFF_GES_GTS; IN_ELIM_THM]
2930 THEN REMOVE_TAC THEN
2931 MESON_TAC[REAL_ARITH` a + b + c + d = d + a + b + c `;
2932   VECTOR_ARITH` a + b + c + d = d + a + b + (c:real^N)`]);;
2933
2934
2935 let SQRT4_EQ2 = prove(` sqrt ( &4 ) = &2 `,
2936 REWRITE_TAC[REAL_ARITH` &4 = &2 pow 2 `] THEN
2937 MESON_TAC[POW_2_SQRT; REAL_ARITH` &0 <= &2 `]);;
2938
2939
2940 let RHUFIIB = prove( ` !x12 x13 x14 x23 x24 x34.
2941          rho_ij' x12 x13 x14 x23 x24 x34 * ups_x x34 x24 x23 =
2942          chi x12 x13 x14 x23 x24 x34 pow 2 +
2943          &4 * delta x12 x13 x14 x23 x24 x34 * x34 * x24 * x23 `,
2944 REWRITE_TAC[rho_ij'; chi; delta; ups_x] THEN REAL_ARITH_TAC);;
2945
2946
2947 (* lemma 84 *)
2948 let SHOGYBS = prove(` ! x1 x2 x3 (x4:real^3).
2949   ~coplanar_alt {x1,x2,x3,x4} ==>
2950          let x12 = dist (x1,x2) pow 2 in
2951          let x13 = dist (x1,x3) pow 2 in
2952          let x14 = dist (x1,x4) pow 2 in
2953          let x23 = dist (x2,x3) pow 2 in
2954          let x24 = dist (x2,x4) pow 2 in
2955          let x34 = dist (x3,x4) pow 2 in
2956   &0 <= rho_ij' x12 x13 x14 x23 x24 x34  `,
2957 ONCE_REWRITE_TAC[SET_RULE` {v1,v2,v3,v4} =  {v2,v3,v4,v1} `] THEN
2958 NHANH (NOT_COPLANAR_IMP_NOT_COLLINEAR) THEN
2959 ONCE_REWRITE_TAC[GSYM (SET_RULE` {v1,v2,v3,v4} =  {v2,v3,v4,v1} `)] THEN
2960 REWRITE_TAC[NOT_COL_EQ_UPS_X_POS] THEN REPEAT GEN_TAC THEN
2961 MP_TAC (SPEC_ALL DELTA_POS_4POINTS) THEN
2962 REPEAT LET_TAC THEN MP_TAC (SPEC_ALL RHUFIIB) THEN DOWN_TAC THEN
2963 NHANH (MESON[REAL_LE_POW_2]` a pow 2 = b   ==> &0 <= b `) THEN DAO THEN
2964 SIMP_TAC[UPS_X_SYM] THEN
2965 REWRITE_TAC[MESON[REAL_FIELD` &0 < a ==> (b * a = c <=> b = c / a )`]`
2966   &0 < a /\a1 /\a2/\ b * a = c /\l <=>  &0 < a /\a1 /\a2/\ b = c / a /\ l `] THEN
2967 MP_TAC (REAL_ARITH` &0 <= &4 `) THEN PHA THEN
2968 NHANH (MESON[REAL_LT_IMP_LE; REAL_LE_DIV;
2969   REAL_LE_MUL; REAL_LE_ADD; REAL_LE_POW_2]`  &0 <= &4 /\
2970  &0 < ups_x x23 x24 x34 /\a1/\
2971  &0 <= delta x12 x13 x14 x23 x24 x34 /\ a2 /\
2972  &0 <= x34 /\a3 /\ &0 <= x24 /\a4 /\ &0 <= x23 /\a5/\
2973  &0 <= x14 /\a6 /\ &0 <= x13 /\a7 /\a8 /\ &0 <= x12 ==>
2974   &0 <= &4 * delta x12 x13 x14 x23 x24 x34 * x34 * x24 * x23 `) THEN
2975 ABBREV_TAC ` aaa = &4 * delta x12 x13 x14 x23 x24 x34 * x34 * x24 * x23 ` THEN STRIP_TAC THEN
2976 FIRST_X_ASSUM MP_TAC THEN UNDISCH_TAC ` rho_ij' x12 x13 x14 x23 x24 x34 =
2977       (chi x12 x13 x14 x23 x24 x34 pow 2 + aaa) / ups_x x23 x24 x34 ` THEN
2978 UNDISCH_TAC`&0 < ups_x x23 x24 x34` THEN MESON_TAC[REAL_LT_IMP_LE; REAL_LE_DIV;
2979   REAL_LE_MUL; REAL_LE_ADD; REAL_LE_POW_2]);;
2980
2981
2982 (* le 86 . GDRQXLG *)
2983
2984
2985 let GDRQXLG = prove(` ! v1 v2 v3 (v4:real^3).
2986   let s = {v1, v2, v3, v4} in
2987 let x12 = dist (v1,v2) pow 2 in
2988                     let x13 = dist (v1,v3) pow 2 in
2989                     let x14 = dist (v1,v4) pow 2 in
2990                     let x23 = dist (v2,v3) pow 2 in
2991                     let x24 = dist (v2,v4) pow 2 in
2992                     let x34 = dist (v3,v4) pow 2 in
2993      CARD s = 4 /\ ~coplanar_alt s
2994      ==> radV s =
2995         sqrt ( rho_ij' x12 x13 x14 x23 x24 x34) /
2996          (&2 * sqrt (delta x12 x13 x14 x23 x24 x34))`,
2997 REPEAT GEN_TAC THEN REPEAT LET_TAC THEN EXPAND_TAC "s" THEN
2998 NHANH (NOT_COPLANAR_IMP_RADV_PROPERTIES) THEN
2999 NHANH (REWRITE_RULE[RIGHT_FORALL_IMP_THM] (GEN `p:real^3` PROVE_DIST_FROM_V1  )) THEN
3000 NHANH (REWRITE_RULE[RIGHT_FORALL_IMP_THM] (GEN `p:real^3` PROVE_EQ_DIST_FROM4 ) ) THEN
3001 REWRITE_TAC[GSYM POS_EQ_NOT_COPLANANR] THEN
3002 NHANH (REAL_ARITH` &0 < a ==> ~( a = &0 )`) THEN
3003 NHANH (PROVE_IN_AFFINE_HULL_4 ) THEN LET_TR THEN
3004 REWRITE_TAC[MESON[]`(!x. x = a ==> p x) <=> p a `] THEN
3005 ABBREV_TAC `taa = (&1 /    (&2 *
3006      delta (dist (v1,v2) pow 2) (dist (v1,v3) pow 2) (dist (v1,v4) pow 2)
3007      (dist (v2,v3) pow 2)
3008      (dist (v2,v4) pow 2)
3009      (dist (v3,v4) pow 2)) %
3010     (chi (dist (v1,v2) pow 2) (dist (v1,v3) pow 2) (dist (v1,v4) pow 2)
3011      (dist (v2,v3) pow 2)
3012      (dist (v2,v4) pow 2)
3013      (dist (v3,v4) pow 2) %
3014      (v1:real^3) +
3015      chi (dist (v1,v2) pow 2) (dist (v2,v4) pow 2) (dist (v2,v3) pow 2)
3016      (dist (v1,v4) pow 2)
3017      (dist (v1,v3) pow 2)
3018      (dist (v3,v4) pow 2) %
3019      v2 +
3020      chi (dist (v3,v4) pow 2) (dist (v1,v3) pow 2) (dist (v2,v3) pow 2)
3021      (dist (v1,v4) pow 2)
3022      (dist (v2,v4) pow 2)
3023      (dist (v1,v2) pow 2) %
3024      v3 +
3025      chi (dist (v3,v4) pow 2) (dist (v2,v4) pow 2) (dist (v1,v4) pow 2)
3026      (dist (v2,v3) pow 2)
3027      (dist (v1,v3) pow 2)
3028      (dist (v1,v2) pow 2) %
3029      v4)) ` THEN
3030 REWRITE_TAC[ POS_EQ_NOT_COPLANANR] THEN NGOAC THEN
3031 NHANH (SPEC_ALL UNIQUE_EXISISTING_PROPERTY_C4 ) THEN
3032 REWRITE_TAC[FORALL_IN_CLAUSES] THEN ABBREV_TAC ` abc = &1 / &2 *
3033  rho_ij' (dist (v1,v2) pow 2) (dist (v1,v3) pow 2) (dist (v1,v4) pow 2)
3034  (dist (v2,v3) pow 2) (dist (v2,v4) pow 2) (dist (v3,v4) pow 2) /
3035  (&2 *
3036   delta (dist ((v1:real^3),v2) pow 2) (dist (v1,v3) pow 2) (dist (v1,v4) pow 2)
3037   (dist (v2,v3) pow 2)
3038   (dist (v2,v4) pow 2)
3039   (dist (v3,v4) pow 2)) ` THEN REWRITE_TAC[dist3] THEN
3040 NHANH (MESON[POW_2_SQRT; DIST_POS_LE]` dist (taa,v2) pow 2 = a ==>
3041   dist(taa,v2) = sqrt a `) THEN PHA THEN
3042 NHANH (MESON[]`(!p. p IN affine hull {v1, v2, v3, v4} /\
3043       (?r. r = dist (p,v1) /\
3044            r = dist (p,v2) /\
3045            r = dist (p,v3) /\
3046            r = dist (p,v4))
3047       ==> p = circumcenter {v1, v2, v3, v4}) /\ a11 /\
3048  taa IN affine hull {v1, v2, v3, v4} /\
3049  dist (taa,v2) pow 2 = abc /\
3050  dist (taa,v2) = sqrt abc /\
3051  dist (taa,v3) pow 2 = abc /\
3052  dist (taa,v3) = sqrt abc /\
3053  dist (taa,v4) pow 2 = abc /\
3054  dist (taa,v4) = sqrt abc /\
3055  dist (taa,v1) pow 2 = abc /\
3056  dist (taa,v1) = sqrt abc /\ lll ==> taa = circumcenter {v1, v2, v3, v4} `) THEN
3057 NHANH (SET_RULE ` (!w. {v1, v2, v3, v4} w ==> P w ) ==> P v1 `) THEN PHA THEN
3058 REWRITE_TAC[MESON[]` a = dist (aa,b) /\ ta = aa <=> ta = aa  /\ a = dist (ta,b) `] THEN
3059 NHANH (MESON[]` a = b /\ a1 /\ a2 /\ c = a ==> c = b `) THEN NHANH (SPEC_ALL SHOGYBS) THEN
3060 MP_TAC (SPECL [`v1:real^3`;` v2:real^3`;`v3:real^3`;`v4:real^3`]
3061 DELTA_POS_4POINTS) THEN REPEAT LET_TAC THEN IMP_TAC THEN REPEAT (FIRST_X_ASSUM MP_TAC) THEN
3062 REWRITE_TAC[MESON[]` a = b ==> P a <=> a = b ==> P b `] THEN
3063 REWRITE_TAC[MESON[]` a = b ==> a = c <=> a = b ==> c = b `] THEN REPEAT STRIP_TAC THEN
3064 UNDISCH_TAC ` &1 / &2 *      rho_ij' x12 x13 x14 x23 x24 x34 / (&2 * delta x12 x13 x14 x23 x24 x34) =
3065       abc ` THEN UNDISCH_TAC ` &0 <= rho_ij' x12 x13 x14 x23 x24 x34 ` THEN
3066 ABBREV_TAC ` edl = delta x12 x13 x14 x23 x24 x34 ` THEN UNDISCH_TAC` &0 <= edl ` THEN
3067 SIMP_TAC[REAL_ARITH` &0 <= &4 `; GSYM SQRT_MUL; GSYM SQRT4_EQ2] THEN
3068 SIMP_TAC[REAL_ARITH` &0 <= &4 `; REAL_LE_MUL;  GSYM SQRT_DIV] THEN
3069 REWRITE_TAC[SQRT4_EQ2] THEN MESON_TAC[REAL_FIELD` &1 / &2 * x34 / (&2 * edl) =  x34 / (&4 * edl)`]);;
3070
3071
3072
3073 end;;  (* end of module *)
3074