text_formalization/tame/CKQOWSA_4.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Chapter: Tame Hypermap                                                     *)
   5 (* Author: Alexey Solovyev                                                    *)
   6 (* Date: 2010-07-07                                                           *)
   7 (* (V,ESTD V) is a fan (4-point case)                                         *)
   8 (* ========================================================================== *)
   9
  10 flyspeck_needs "tame/CKQOWSA_3.hl";;
  11
  12
  13 module Ckqowsa_4_points = struct
  14
  15
  16 open Ckqowsa_3_points;;
  17
  18
  19
  20 (* General *)
  21
  22 let IN_INTERVAL_1 = prove(`!a b c. lift c IN interval [lift a, lift b] <=> a <= c /\ c <= b`,
  23    REPEAT STRIP_TAC THEN
  24      SIMP_TAC[IN_INTERVAL; DIMINDEX_1; ARITH_RULE `1 <= i /\ i <= 1 <=> i = 1`] THEN
  25      REWRITE_TAC[GSYM drop; LIFT_DROP] THEN
  26      EQ_TAC THEN SIMP_TAC[] THEN
  27      DISCH_THEN (MP_TAC o SPEC `1`) THEN
  28      SIMP_TAC[]);;
  29
  30
  31 let DIST_SQR = prove(`!v (w:real^N) d. dist(v,w) = d <=> dist(v,w) pow 2 = d pow 2 /\ &0 <= d`,
  32                      REPEAT STRIP_TAC THEN EQ_TAC THEN STRIP_TAC THENL
  33                        [
  34                          FIRST_X_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN
  35                            REWRITE_TAC[DIST_POS_LE];
  36                          ASSUME_TAC (REAL_ARITH `!d. &0 <= d ==> d = abs(d)`) THEN
  37                            FIRST_ASSUM (MP_TAC o SPEC `d:real`) THEN
  38                            FIRST_X_ASSUM (MP_TAC o SPEC `dist(v:real^N,w)`) THEN
  39                            ASM_REWRITE_TAC[DIST_POS_LE] THEN
  40                            REPLICATE_TAC 2 (DISCH_THEN (fun th -> ONCE_REWRITE_TAC[th])) THEN
  41                            ASM_REWRITE_TAC[REAL_EQ_SQUARE_ABS]
  42                        ]);;
  43
  44
  45 let estd_non_collinear_lemma = prove(`!v w. v IN ball_annulus /\ w IN ball_annulus /\
  46                                        &2 <= dist (v,w) /\ dist (v,w) <= &2 * h0
  47                                        ==> ~collinear {vec 0, v, w}`,
  48    REWRITE_TAC[in_ball_annulus] THEN
  49      REWRITE_TAC[COLLINEAR_BETWEEN_CASES; between; DIST_0; DIST_SYM] THEN
  50      REWRITE_TAC[Sphere.h0] THEN
  51      REAL_ARITH_TAC);;
  52
  53
  54
  55 let zero_not_between = prove(`!v w:real^N. ~between (vec 0) (v, w) ==> ~(v = vec 0) /\ ~(w = vec 0) /\
  56                                                        (!a b. a < &0 /\ &0 < b ==> ~(a % w = b % v))`,
  57    REPEAT GEN_TAC THEN DISCH_TAC THEN
  58      SUBGOAL_THEN `~(v = vec 0:real^N) /\ ~(w = vec 0:real^N)` ASSUME_TAC THENL
  59      [
  60        POP_ASSUM MP_TAC THEN
  61          REWRITE_TAC[GSYM NORM_EQ_0] THEN
  62          REWRITE_TAC[between; DIST_0] THEN
  63          ASM_CASES_TAC `norm (v:real^N) = &0` THEN ASM_REWRITE_TAC[] THENL
  64          [
  65            POP_ASSUM MP_TAC THEN REWRITE_TAC[NORM_EQ_0] THEN
  66              DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
  67              REWRITE_TAC[DIST_0; REAL_ADD_LID];
  68            ALL_TAC
  69          ] THEN
  70          ASM_CASES_TAC `norm (w:real^N) = &0` THEN ASM_REWRITE_TAC[] THEN
  71          POP_ASSUM MP_TAC THEN REWRITE_TAC[NORM_EQ_0] THEN
  72          DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
  73          REWRITE_TAC[DIST_0; REAL_ADD_RID];
  74        ALL_TAC
  75      ] THEN
  76      ASM_REWRITE_TAC[] THEN
  77
  78      REPEAT STRIP_TAC THEN
  79      UNDISCH_TAC `~between (vec 0:real^N) (v,w)` THEN
  80      REWRITE_TAC[between; DIST_0] THEN
  81      POP_ASSUM (MP_TAC o AP_TERM `\v:real^N. inv(a) % v`) THEN
  82      REWRITE_TAC[VECTOR_MUL_ASSOC] THEN
  83      ASM_SIMP_TAC[REAL_ARITH `a < &0 ==> ~(a = &0)`; REAL_MUL_LINV; VECTOR_MUL_LID] THEN
  84      DISCH_TAC THEN
  85      REWRITE_TAC[dist; VECTOR_ARITH `v - a % v = (&1 - a) % v:real^N`] THEN
  86      REWRITE_TAC[NORM_MUL] THEN
  87
  88      SUBGOAL_THEN `&0 <= --(inv a * b)` ASSUME_TAC THENL
  89      [
  90        REWRITE_TAC[REAL_ARITH `&0 <= --(a * b) <=> &0 <= --a * b`] THEN
  91          MATCH_MP_TAC REAL_LE_MUL THEN
  92          ASM_SIMP_TAC[REAL_LT_IMP_LE] THEN
  93          REWRITE_TAC[GSYM REAL_INV_NEG] THEN
  94          MATCH_MP_TAC REAL_LE_INV THEN
  95          ASM_SIMP_TAC[REAL_ARITH `a < &0 ==> &0 <= --a`];
  96        ALL_TAC
  97      ] THEN
  98
  99      SUBGOAL_THEN `abs (&1 - inv a * b) = &1 - inv a * b` (fun th -> REWRITE_TAC[th]) THENL
 100      [
 101        REWRITE_TAC[REAL_ABS_REFL] THEN
 102          REWRITE_TAC[REAL_ARITH `&1 - a = &1 + (--a)`] THEN
 103          MATCH_MP_TAC REAL_LE_ADD THEN
 104          ASM_REWRITE_TAC[REAL_LE_01];
 105        ALL_TAC
 106      ] THEN
 107
 108      SUBGOAL_THEN `abs (inv a * b) = --(inv a * b)` (fun th -> REWRITE_TAC[th]) THENL
 109      [
 110        POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;
 111        ALL_TAC
 112      ] THEN
 113
 114      REAL_ARITH_TAC);;
 115
 116
 117 let zero_not_between_estd = prove(`!v w. v IN ball_annulus /\ w IN ball_annulus /\ dist (v,w) <= &2 * h0
 118                                     ==> ~between (vec 0) (v,w)`,
 119    REWRITE_TAC[in_ball_annulus; between; DIST_0; Sphere.h0] THEN
 120      REAL_ARITH_TAC);;
 121
 122
 123
 124 (******************************************************************)
 125
 126 (* Some properties of projections *)
 127
 128 let projection = Sphere.projection;;
 129
 130
 131 let PROJECTION_ORTHOGONAL = prove(`!d v:real^N. projection d v dot d = &0`,
 132    REWRITE_TAC[DOT_SYM; projection; VECTOR_SUB_PROJECT_ORTHOGONAL]);;
 133
 134
 135 let VECTOR_PROJECTION = prove(`!d v:real^N. v = projection d v + (v dot d) / (d dot d) % d`,
 136    REWRITE_TAC[projection] THEN VECTOR_ARITH_TAC);;
 137
 138
 139
 140 let PROJECTION_0 = prove(`!d:real^N. projection d (vec 0) = vec 0`,
 141    REWRITE_TAC[projection; DOT_LZERO; real_div; REAL_MUL_LZERO] THEN
 142      VECTOR_ARITH_TAC);;
 143
 144
 145 let PROJECTION_ZERO = prove(`!d:real^N. ~(d = vec 0) ==> projection d d = vec 0`,
 146    REWRITE_TAC[GSYM NORM_EQ_0] THEN GEN_TAC THEN DISCH_TAC THEN
 147      REWRITE_TAC[NORM_EQ_0; projection; DOT_SQUARE_NORM] THEN
 148      SUBGOAL_THEN `norm d pow 2 / norm (d:real^N) pow 2 = &1` (fun th -> REWRITE_TAC[th]) THENL
 149      [
 150        REWRITE_TAC[real_div; REAL_POW_2; REAL_INV_MUL] THEN
 151          REWRITE_TAC[REAL_ARITH `(d * d) * id * id = d * (d * id) * id`] THEN
 152          ASM_SIMP_TAC[REAL_MUL_RINV; REAL_MUL_LID];
 153        ALL_TAC
 154      ] THEN
 155      VECTOR_ARITH_TAC);;
 156
 157
 158 let PROJECTION_LINEAR = prove(`!(d:real^N) v w a. projection d (v + w) = projection d v + projection d w /\
 159                                          projection d (a % v) = a % projection d v`,
 160    REPEAT GEN_TAC THEN
 161      REWRITE_TAC[projection; DOT_LMUL; DOT_LADD; real_div; REAL_ADD_RDISTRIB; VECTOR_SUB_LDISTRIB; VECTOR_MUL_ASSOC; REAL_MUL_ASSOC] THEN
 162      REWRITE_TAC[VECTOR_ADD_RDISTRIB] THEN
 163      VECTOR_ARITH_TAC);;
 164
 165
 166 let PROJECTION_NEG = prove(`!(d:real^N) v. projection d (--v) = --projection d v`,
 167                            REWRITE_TAC[VECTOR_ARITH `--v:real^N = -- &1 % v`; PROJECTION_LINEAR]);;
 168
 169
 170 let PROJECTION_SUB = prove(`!(d:real^N) v w. projection d (v - w) = projection d v - projection d w`,
 171     REWRITE_TAC[VECTOR_ARITH `a - b:real^N = a + (--b)`; PROJECTION_LINEAR; PROJECTION_NEG]);;
 172
 173
 174
 175 let PROJECTION_DIST2 = prove(`!d v w:real^N. ~(d = vec 0) ==>
 176                                dist (projection d v, projection d w) pow 2 = dist (v,w) pow 2 - ((v - w) dot d) pow 2 / (norm d pow 2)`,
 177    REWRITE_TAC[GSYM NORM_EQ_0] THEN REPEAT STRIP_TAC THEN
 178      REWRITE_TAC[dist; projection] THEN
 179      REWRITE_TAC[VECTOR_ARITH `v - a % d - (w - b % d) = (v - w) - (a - b) % d:real^N`] THEN
 180
 181      ABBREV_TAC `x = v - w:real^N` THEN
 182      ABBREV_TAC `y = ((v dot d) / (d dot d) - (w dot d) / (d dot d)) % d:real^N` THEN
 183
 184      SUBGOAL_THEN `!a. a / (d dot d) * (d dot d:real^N) = a` ASSUME_TAC THENL
 185      [
 186        REWRITE_TAC[real_div; DOT_SQUARE_NORM; REAL_POW_2; REAL_INV_MUL] THEN
 187          REWRITE_TAC[REAL_ARITH `(a * id * id) * d * d = a * (id * (id * d) * d)`] THEN
 188          ASM_SIMP_TAC[REAL_MUL_LINV; REAL_MUL_LID; REAL_MUL_RID];
 189        ALL_TAC
 190      ] THEN
 191
 192      SUBGOAL_THEN `x:real^N dot y = y dot y` ASSUME_TAC THENL
 193      [
 194        EXPAND_TAC "y" THEN
 195          REWRITE_TAC[real_div] THEN
 196          REWRITE_TAC[GSYM REAL_SUB_RDISTRIB; GSYM DOT_LSUB] THEN
 197          EXPAND_TAC "x" THEN
 198          REWRITE_TAC[DOT_LMUL; DOT_RMUL; DOT_SYM] THEN
 199          REWRITE_TAC[REAL_ARITH `(dv * id) * (dv * id) * d = ((dv * dv * id) * id) * d`] THEN
 200          ASM_REWRITE_TAC[GSYM real_div] THEN
 201          REAL_ARITH_TAC;
 202        ALL_TAC
 203      ] THEN
 204
 205      ASM_REWRITE_TAC[NORM_POW_2; DOT_LSUB; DOT_RSUB; DOT_SYM] THEN
 206      REWRITE_TAC[REAL_ARITH `x - y - (y - y) = x - z <=> y = z`] THEN
 207      EXPAND_TAC "y" THEN
 208      REWRITE_TAC[real_div] THEN
 209      ASM_REWRITE_TAC[GSYM REAL_SUB_RDISTRIB; GSYM DOT_LSUB] THEN
 210      REWRITE_TAC[DOT_LMUL; DOT_RMUL] THEN
 211      ASM_REWRITE_TAC[GSYM real_div; DOT_SYM] THEN
 212      REAL_ARITH_TAC);;
 213
 214
 215
 216 let PROJECTION_SUM_DIST = prove(`!(d:real^N) x y a b. x dot d = &0 /\ y dot d = &0
 217                      ==> dist (x + a % d, y + b % d) pow 2 = dist (x, y) pow 2 + (a - b) pow 2 * (d dot d)`,
 218    REPEAT STRIP_TAC THEN
 219      GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [dist] THEN
 220      REWRITE_TAC[VECTOR_ARITH `(x + a % d) - (y + b % d) = (x - y) + (a - b) % d:real^N`] THEN
 221      SUBGOAL_THEN `(x - y:real^N) dot ((a - b) % d) = &0` ASSUME_TAC THENL
 222      [
 223        ASM_REWRITE_TAC[DOT_RMUL; DOT_LSUB; REAL_MUL_RZERO; REAL_SUB_RZERO];
 224        ALL_TAC
 225      ] THEN
 226      ASM_SIMP_TAC[Trigonometry2.PITHAGO_THEOREM] THEN
 227      REWRITE_TAC[GSYM dist] THEN
 228      REWRITE_TAC[NORM_MUL; REAL_POW_MUL; REAL_POW2_ABS; DOT_SQUARE_NORM]);;
 229
 230
 231
 232 let PROJECTION_DIST_SPECIAL_EQ = prove(`!d x v w:real^N. ~(d = vec 0) /\ x dot d = &0
 233                                     ==> dist (x + (v - projection d v), w) pow 2 = dist (x, projection d w) pow 2 - dist (projection d v, projection d w) pow 2 + dist (v, w) pow 2`,
 234    REWRITE_TAC[GSYM NORM_EQ_0] THEN
 235      REPEAT STRIP_TAC THEN
 236      SUBGOAL_THEN `!a. a / (d dot d) * (d dot d:real^N) = a` ASSUME_TAC THENL
 237      [
 238        REWRITE_TAC[real_div; DOT_SQUARE_NORM; REAL_POW_2; REAL_INV_MUL] THEN
 239          REWRITE_TAC[REAL_ARITH `(a * id * id) * d * d = a * (id * (id * d) * d)`] THEN
 240          ASM_SIMP_TAC[REAL_MUL_LINV; REAL_MUL_LID; REAL_MUL_RID];
 241        ALL_TAC
 242      ] THEN
 243
 244      SUBGOAL_THEN `dist (x + v - projection d v, w) pow 2 = dist (x, projection d w) pow 2 + ((v - w) dot d:real^N) pow 2 / norm d pow 2` (fun th -> REWRITE_TAC[th]) THENL
 245      [
 246        MP_TAC (SPECL [`d:real^N`; `w:real^N`] VECTOR_PROJECTION) THEN
 247          DISCH_THEN (fun th -> GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [th]) THEN
 248          SUBGOAL_THEN `v - projection d (v:real^N) = (v dot d) / (d dot d) % d` (fun th -> REWRITE_TAC[th]) THENL
 249          [
 250            REWRITE_TAC[projection] THEN
 251              VECTOR_ARITH_TAC;
 252            ALL_TAC
 253          ] THEN
 254          ASM_SIMP_TAC[PROJECTION_ORTHOGONAL; PROJECTION_SUM_DIST] THEN
 255          REWRITE_TAC[real_div] THEN
 256          REWRITE_TAC[GSYM REAL_SUB_RDISTRIB; GSYM DOT_LSUB] THEN
 257          REWRITE_TAC[REAL_ARITH `(a * b) pow 2 * c = ((a pow 2 * b) * b) * c`] THEN
 258          ASM_REWRITE_TAC[GSYM real_div; NORM_POW_2];
 259        ALL_TAC
 260      ] THEN
 261      MP_TAC (SPECL [`d:real^N`; `v:real^N`; `w:real^N`] PROJECTION_DIST2) THEN
 262      ASM_REWRITE_TAC[GSYM NORM_EQ_0] THEN
 263      REAL_ARITH_TAC);;
 264
 265
 266
 267 let PROJECTION_DIST_SPECIAL_LE = prove(`!d x v w:real^N. ~(d = vec 0) /\ x dot d = &0 /\ dist (x, projection d w) <= dist (projection d v, projection d w)
 268                                         ==> dist (x + v - projection d v, w) <= dist (v, w)`,
 269    REPEAT STRIP_TAC THEN
 270      POP_ASSUM MP_TAC THEN
 271      REWRITE_TAC[dist] THEN ONCE_REWRITE_TAC[GSYM REAL_ABS_NORM] THEN
 272      REWRITE_TAC[REAL_LE_SQUARE_ABS] THEN
 273      REWRITE_TAC[GSYM dist] THEN
 274      ASM_SIMP_TAC[PROJECTION_DIST_SPECIAL_EQ] THEN
 275      REAL_ARITH_TAC);;
 276
 277
 278
 279 (***********************************************)
 280
 281
 282 (* General properties of affine hull and aff_ge *)
 283
 284 let aff_ge_0_2_eq_segment = prove(`!v:real^N. aff_ge {vec 0} {vec 0,v} = segment [vec 0,v] /\ aff_ge {vec 0} {v,vec 0} = segment [vec 0,v]`,
 285    GEN_TAC THEN
 286      REWRITE_TAC[SET_RULE `{v:real^N, vec 0} = {vec 0,v}`] THEN
 287      ONCE_REWRITE_TAC[AFF_GE_DISJOINT_DIFF] THEN
 288      REWRITE_TAC[SET_RULE `{vec 0} DIFF {vec 0,v:real^N} = {}`] THEN
 289      REWRITE_TAC[GSYM CONVEX_HULL_AFF_GE; SEGMENT_CONVEX_HULL]);;
 290
 291
 292 let in_segment_imp_in_aff_ge_0_2 = prove(`!v v1 v2:real^N. v IN segment [v1,v2] ==> v IN aff_ge {vec 0} {v1,v2}`,
 293    REPEAT GEN_TAC THEN
 294      ASM_CASES_TAC `v1:real^N = vec 0` THENL
 295      [
 296        ASM_SIMP_TAC[aff_ge_0_2_eq_segment];
 297        ALL_TAC
 298      ] THEN
 299      ASM_CASES_TAC `v2:real^N = vec 0` THENL
 300      [
 301        ASM_REWRITE_TAC[aff_ge_0_2_eq_segment; SEGMENT_SYM];
 302        ALL_TAC
 303      ] THEN
 304      ASM_SIMP_TAC[aff_ge_0_2] THEN
 305      REWRITE_TAC[IN_SEGMENT; IN_ELIM_THM] THEN
 306      STRIP_TAC THEN
 307      MAP_EVERY EXISTS_TAC [`&1 - u`; `u:real`] THEN
 308      ASM_REWRITE_TAC[] THEN
 309      UNDISCH_TAC `u <= &1` THEN REAL_ARITH_TAC);;
 310
 311
 312
 313 let points_in_aff_ge_0_2 = prove(`!v1 v2:real^N. vec 0 IN aff_ge {vec 0} {v1, v2} /\
 314                                                  v1 IN aff_ge {vec 0} {v1, v2} /\
 315                                                  v2 IN aff_ge {vec 0} {v1, v2}`,
 316    REPEAT GEN_TAC THEN
 317      ASM_CASES_TAC `v1:real^N = vec 0` THENL
 318      [
 319        ASM_REWRITE_TAC[aff_ge_0_2_eq_segment; ENDS_IN_SEGMENT];
 320        ALL_TAC
 321      ] THEN
 322      ASM_CASES_TAC `v2:real^N = vec 0` THENL
 323      [
 324        ASM_REWRITE_TAC[aff_ge_0_2_eq_segment; ENDS_IN_SEGMENT];
 325        ALL_TAC
 326      ] THEN
 327      ASM_SIMP_TAC[aff_ge_0_2; IN_ELIM_THM] THEN
 328      REPEAT CONJ_TAC THENL
 329      [
 330        MAP_EVERY EXISTS_TAC [`&0`; `&0`];
 331        MAP_EVERY EXISTS_TAC [`&1`; `&0`];
 332        MAP_EVERY EXISTS_TAC [`&0`; `&1`]
 333      ] THEN
 334      REWRITE_TAC[REAL_LE_REFL; REAL_LE_01; VECTOR_MUL_LZERO; VECTOR_ADD_LID; VECTOR_MUL_LID; VECTOR_ADD_RID]);;
 335
 336
 337
 338 let aff_ge_0_2_SUBSET = prove(`!v1 v2 v w:real^N. ~(v1 = vec 0) /\ ~(v2 = vec 0) /\
 339                                 v IN aff_ge {vec 0} {v1,v2} /\ w IN aff_ge {vec 0} {v1,v2}
 340                                 ==> aff_ge {vec 0} {v,w} SUBSET aff_ge {vec 0} {v1,v2}`,
 341    REPEAT STRIP_TAC THEN
 342      MP_TAC (ISPECL [`{vec 0:real^N}`; `{v1:real^N,v2}`] CONVEX_AFF_GE) THEN
 343      REWRITE_TAC[CONVEX_CONTAINS_SEGMENT] THEN DISCH_TAC THEN
 344      ASM_CASES_TAC `v:real^N = vec 0` THENL
 345      [
 346        ASM_REWRITE_TAC[aff_ge_0_2_eq_segment] THEN
 347          FIRST_X_ASSUM MATCH_MP_TAC THEN
 348          ASM_REWRITE_TAC[points_in_aff_ge_0_2];
 349        ALL_TAC
 350      ] THEN
 351      ASM_CASES_TAC `w:real^N = vec 0` THENL
 352      [
 353        ASM_REWRITE_TAC[aff_ge_0_2_eq_segment] THEN
 354          FIRST_X_ASSUM MATCH_MP_TAC THEN
 355          ASM_REWRITE_TAC[points_in_aff_ge_0_2];
 356        ALL_TAC
 357      ] THEN
 358      REPEAT (FIRST_X_ASSUM (MP_TAC o check (is_binary "IN" o concl))) THEN
 359      ASM_SIMP_TAC[aff_ge_0_2; IN_ELIM_THM; SUBSET] THEN
 360      REPEAT STRIP_TAC THEN
 361      MAP_EVERY EXISTS_TAC [`t1'' * t1 + t2'' * t1'`; `t1'' * t2 + t2'' * t2'`] THEN
 362      REWRITE_TAC[CONJ_ASSOC] THEN
 363      CONJ_TAC THENL
 364      [
 365        CONJ_TAC THEN MATCH_MP_TAC REAL_LE_ADD THEN CONJ_TAC THEN MATCH_MP_TAC REAL_LE_MUL THEN ASM_REWRITE_TAC[];
 366        ALL_TAC
 367      ] THEN
 368      ASM_REWRITE_TAC[] THEN
 369      VECTOR_ARITH_TAC);;
 370
 371
 372
 373 let segment_inter_aff_ge_ends = prove(`!v1 v2 v w n:real^N. ~(v1 = vec 0) /\ ~(v2 = vec 0) /\
 374                                                             v1 dot n = &0 /\ v2 dot n = &0 /\
 375                                                             v dot n = &0 /\ ~(w dot n = &0) /\
 376                                                             ~(segment [v,w] INTER aff_ge {vec 0} {v1,v2} = {})
 377                                                             ==> v IN aff_ge {vec 0} {v1,v2}`,
 378    REPEAT STRIP_TAC THEN
 379      POP_ASSUM MP_TAC THEN
 380      REWRITE_TAC[GSYM MEMBER_NOT_EMPTY] THEN
 381      REWRITE_TAC[IN_INTER; IN_SEGMENT] THEN
 382      REPEAT STRIP_TAC THEN
 383      FIRST_ASSUM MP_TAC THEN
 384      SUBGOAL_THEN `?t1 t2. &0 <= t1 /\ &0 <= t2 /\ x = t1 % v1 + t2 % v2:real^N` MP_TAC THENL
 385      [
 386        POP_ASSUM MP_TAC THEN
 387          ASM_SIMP_TAC[aff_ge_0_2; IN_ELIM_THM];
 388        ALL_TAC
 389      ] THEN
 390      STRIP_TAC THEN
 391      SUBGOAL_THEN `u = &0` ASSUME_TAC THENL
 392      [
 393        POP_ASSUM (MP_TAC o AP_TERM `\v:real^N. v dot n`) THEN
 394          FIRST_X_ASSUM (MP_TAC o AP_TERM `\v:real^N. v dot n`) THEN
 395          DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
 396          ASM_REWRITE_TAC[DOT_LADD; DOT_LMUL; REAL_MUL_RZERO; REAL_ADD_LID] THEN
 397          UNDISCH_TAC `~(w dot n:real^N = &0)` THEN
 398          CONV_TAC REAL_FIELD;
 399        ALL_TAC
 400      ] THEN
 401      UNDISCH_TAC `x = (&1 - u) % v + u % w:real^N` THEN
 402      POP_ASSUM (fun th -> REWRITE_TAC[th]) THEN
 403      REMOVE_ASSUM THEN
 404      REWRITE_TAC[REAL_SUB_RZERO; VECTOR_MUL_LZERO; VECTOR_MUL_LID; VECTOR_ADD_RID] THEN
 405      DISCH_THEN (fun th -> ASM_REWRITE_TAC[SYM th]));;
 406
 407
 408
 409
 410 let in_affine_hull_lemma = prove(`!v1 v2 v:real^N. ~collinear {vec 0,v1,v2} /\ v IN affine hull {vec 0,v1,v2}
 411                                    ==> ?t1 t2. v = t1 % v1 + t2 % v2 /\
 412                                        (!t1' t2'. v = t1' % v1 + t2' % v2 ==> t1' = t1 /\ t2' = t2)`,
 413    REWRITE_TAC[AFFINE_HULL_3; IN_ELIM_THM] THEN
 414      REWRITE_TAC[VECTOR_MUL_RZERO; VECTOR_ADD_LID] THEN
 415      REPEAT STRIP_TAC THEN
 416      UNDISCH_TAC `~collinear {vec 0,v1,v2:real^N}` THEN DISCH_TAC THEN
 417      FIRST_ASSUM MP_TAC THEN REWRITE_TAC[COLLINEAR_LEMMA] THEN
 418      FIRST_X_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[SET_RULE `{vec 0:real^N,v1,v2} = {vec 0,v2,v1}`] THEN
 419      REWRITE_TAC[COLLINEAR_LEMMA; DE_MORGAN_THM; NOT_EXISTS_THM] THEN
 420      REPEAT STRIP_TAC THEN
 421
 422      MAP_EVERY EXISTS_TAC [`v':real`; `w:real`] THEN
 423      ASM_REWRITE_TAC[] THEN
 424      REPEAT STRIP_TAC THENL
 425      [
 426        ASM_CASES_TAC `t1' = v':real` THEN ASM_REWRITE_TAC[] THEN
 427          SUBGOAL_TAC "A" `~(v' - t1' = &0)` [ POP_ASSUM MP_TAC THEN REAL_ARITH_TAC ] THEN
 428          FIRST_X_ASSUM (MP_TAC o check (is_eq o concl)) THEN
 429          REWRITE_TAC[VECTOR_ARITH `t1 % v1 + t2 % v2 = t1' % v1 + t2' % v2 <=> (t1 - t1') % v1 = (t2' - t2) % v2:real^N`] THEN
 430          DISCH_THEN (MP_TAC o AP_TERM `(\v:real^N. inv(v' - t1') % v)`) THEN BETA_TAC THEN
 431          REWRITE_TAC[VECTOR_MUL_ASSOC] THEN
 432          ASM_SIMP_TAC[REAL_MUL_LINV; VECTOR_MUL_LID];
 433        ASM_CASES_TAC `t2' = w:real` THEN ASM_REWRITE_TAC[] THEN
 434          SUBGOAL_TAC "A" `~(w - t2' = &0)` [ POP_ASSUM MP_TAC THEN REAL_ARITH_TAC ] THEN
 435          FIRST_X_ASSUM (MP_TAC o check (is_eq o concl)) THEN
 436          REWRITE_TAC[VECTOR_ARITH `t1 % v1 + t2 % v2 = t1' % v1 + t2' % v2 <=> (t2 - t2') % v2 = (t1' - t1) % v1:real^N`] THEN
 437          DISCH_THEN (MP_TAC o AP_TERM `(\v:real^N. inv(w - t2') % v)`) THEN BETA_TAC THEN
 438          REWRITE_TAC[VECTOR_MUL_ASSOC] THEN
 439          ASM_SIMP_TAC[REAL_MUL_LINV; VECTOR_MUL_LID]
 440      ]);;
 441
 442
 443
 444
 445 let affine_hull_3_plane = prove(`!v1 v2 n:real^3. ~collinear {vec 0,v1,v2} /\ ~(n = vec 0) /\
 446                                   v1 dot n = &0 /\ v2 dot n = &0
 447                                   ==> affine hull {vec 0,v1,v2} = {v | v dot n = &0}`,
 448    REPEAT STRIP_TAC THEN
 449      SUBGOAL_THEN `dim {n,v1,v2:real^3} = 3` ASSUME_TAC THENL
 450      [
 451        ONCE_REWRITE_TAC[DIM_INSERT] THEN
 452          SUBGOAL_THEN `~(n IN span {v1,v2:real^3})` (fun th -> REWRITE_TAC[th]) THENL
 453          [
 454            REWRITE_TAC[SPAN_2; IN_UNIV; IN_ELIM_THM] THEN
 455              STRIP_TAC THEN
 456              POP_ASSUM (MP_TAC o AP_TERM `(dot) (n:real^3)`) THEN
 457              POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN
 458              SIMP_TAC[DOT_RADD; DOT_RMUL; DOT_SYM] THEN
 459              ASM_REWRITE_TAC[REAL_MUL_RZERO; REAL_ADD_LID; DOT_EQ_0];
 460            ALL_TAC
 461          ] THEN
 462
 463          ONCE_REWRITE_TAC[DIM_INSERT] THEN
 464          SUBGOAL_THEN `~(v1:real^3 IN span {v2})` (fun th -> REWRITE_TAC[th]) THENL
 465          [
 466            REWRITE_TAC[SPAN_SING; IN_ELIM_THM; IN_UNIV] THEN
 467              UNDISCH_TAC `~collinear {vec 0:real^3,v1,v2}` THEN
 468              ONCE_REWRITE_TAC[SET_RULE `{vec 0:real^3,v1,v2} = {vec 0,v2,v1}`] THEN
 469              SIMP_TAC[COLLINEAR_LEMMA; DE_MORGAN_THM];
 470            ALL_TAC
 471          ] THEN
 472          REWRITE_TAC[DIM_SING] THEN
 473          UNDISCH_TAC `~collinear {vec 0:real^3,v1,v2}` THEN
 474          SIMP_TAC[COLLINEAR_LEMMA; DE_MORGAN_THM] THEN
 475          ARITH_TAC;
 476        ALL_TAC
 477      ] THEN
 478      MP_TAC (ISPEC `{n:real^3,v1,v2}` DIM_EQ_FULL) THEN
 479      ASM_REWRITE_TAC[AFFINE_HULL_3; DIMINDEX_3; SPAN_3; IN_UNIV; EXTENSION; IN_ELIM_THM] THEN DISCH_TAC THEN
 480      REWRITE_TAC[VECTOR_MUL_RZERO; VECTOR_ADD_LID] THEN
 481      GEN_TAC THEN
 482      EQ_TAC THENL
 483      [
 484        STRIP_TAC THEN ASM_REWRITE_TAC[DOT_LADD; DOT_LMUL; REAL_MUL_RZERO; REAL_ADD_RID];
 485        ALL_TAC
 486      ] THEN
 487      POP_ASSUM (MP_TAC o SPEC `x:real^3`) THEN
 488      STRIP_TAC THEN ASM_REWRITE_TAC[DOT_LADD; DOT_LMUL; REAL_MUL_RZERO; REAL_ADD_RID] THEN
 489      ASM_REWRITE_TAC[REAL_ENTIRE; DOT_EQ_0] THEN
 490      DISCH_TAC THEN
 491      MAP_EVERY EXISTS_TAC [`&1 - v - w`; `v:real`; `w:real`] THEN
 492      CONJ_TAC THENL [ REAL_ARITH_TAC; ALL_TAC ] THEN
 493      ASM_REWRITE_TAC[] THEN VECTOR_ARITH_TAC);;
 494
 495
 496
 497
 498 let intersection_point_exists = prove(`!v1 v2 n v w:real^3.
 499                                         ~collinear {vec 0,v1,v2} /\ ~(n = vec 0) /\
 500                                         v1 dot n = &0 /\ v2 dot n = &0 /\
 501                                         v dot n <= &0 /\
 502                                         &0 <= w dot n
 503                                         ==> ?p. p IN segment [v,w] INTER affine hull {vec 0,v1,v2}`,
 504    REPEAT STRIP_TAC THEN
 505      ASM_SIMP_TAC[IN_INTER; IN_SEGMENT; affine_hull_3_plane; IN_ELIM_THM] THEN
 506      ABBREV_TAC `d = (\u. ((&1 - u) % v + u % w) dot n:real^3)` THEN
 507      SUBGOAL_THEN `?u. (&0 <= u /\ u <= &1) /\ d u = &0` ASSUME_TAC THENL
 508      [
 509        REWRITE_TAC[GSYM IN_REAL_INTERVAL] THEN
 510          MATCH_MP_TAC REAL_IVT_INCREASING THEN
 511          REWRITE_TAC[REAL_LE_01] THEN
 512          EXPAND_TAC "d" THEN
 513          ASM_REWRITE_TAC[REAL_SUB_RZERO; VECTOR_MUL_LZERO; VECTOR_ADD_RID; VECTOR_MUL_LID; REAL_SUB_REFL] THEN
 514          ASM_REWRITE_TAC[VECTOR_ADD_LID] THEN
 515          EXPAND_TAC "d" THEN
 516          REWRITE_TAC[VECTOR_ARITH `((&1 - u) % v + u % w:real^3) dot n = v dot n + u * ((w - v) dot n)`] THEN
 517          MATCH_MP_TAC REAL_CONTINUOUS_ON_ADD THEN
 518          REWRITE_TAC[REAL_CONTINUOUS_ON_CONST] THEN
 519          MATCH_MP_TAC REAL_CONTINUOUS_ON_MUL THEN
 520          REWRITE_TAC[REAL_CONTINUOUS_ON_CONST; REAL_CONTINUOUS_ON_ID];
 521        ALL_TAC
 522      ] THEN
 523      POP_ASSUM MP_TAC THEN STRIP_TAC THEN
 524      EXISTS_TAC `(&1 - u) % v + u % w:real^3` THEN
 525      POP_ASSUM MP_TAC THEN EXPAND_TAC "d" THEN SIMP_TAC[] THEN
 526      DISCH_TAC THEN
 527      EXISTS_TAC `u:real` THEN ASM_REWRITE_TAC[]);;
 528
 529
 530
 531
 532
 533 let aux_ineq = prove(`!a b x. &0 < a /\ &0 < b /\ x = (&1 - a * a - b * b) / (&2 * a * b) /\ -- &1 <= x /\ x <= &1
 534                        ==> x * (&1 - a) <= b`,
 535    REPEAT GEN_TAC THEN
 536      REWRITE_TAC[GSYM IMP_IMP] THEN
 537      DISCH_TAC THEN DISCH_TAC THEN
 538      DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
 539      REPEAT DISCH_TAC THEN
 540
 541      SUBGOAL_THEN `&0 < &2 * a * b` ASSUME_TAC THENL
 542      [
 543        MATCH_MP_TAC REAL_LT_MUL THEN
 544          REWRITE_TAC[REAL_ARITH `&0 < &2`] THEN
 545          MATCH_MP_TAC REAL_LT_MUL THEN ASM_REWRITE_TAC[];
 546        ALL_TAC
 547      ] THEN
 548      SUBGOAL_THEN `&1 <= (a + b) pow 2` ASSUME_TAC THENL
 549      [
 550        FIRST_X_ASSUM (MP_TAC o check (is_binop `(<=):real->real->bool` o concl)) THEN
 551          MP_TAC (GEN_ALL RAT_LEMMA4) THEN
 552          DISCH_THEN (MP_TAC o SPECL [`&1 - a * a - b * b`; `&1`; `&1`; `&2 * a * b`]) THEN
 553          ASM_REWRITE_TAC[REAL_ARITH `&0 < &1`; REAL_ARITH `&1 / &1 = &1`] THEN
 554          DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
 555          REAL_ARITH_TAC;
 556        ALL_TAC
 557      ] THEN
 558      SUBGOAL_THEN `(a - b) pow 2 <= &1` ASSUME_TAC THENL
 559      [
 560        UNDISCH_TAC `-- &1 <= (&1 - a * a - b * b) / (&2 * a * b)` THEN
 561          MP_TAC (GEN_ALL RAT_LEMMA4) THEN
 562          DISCH_THEN (MP_TAC o SPECL [`-- &1`; `&2 * a * b`; `&1 - a * a - b * b`; `&1`]) THEN
 563          ASM_REWRITE_TAC[REAL_ARITH `&0 < &1`; REAL_ARITH `-- &1 / &1 = -- &1`] THEN
 564          DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
 565          REAL_ARITH_TAC;
 566        ALL_TAC
 567      ] THEN
 568      DISJ_CASES_TAC (REAL_ARITH `&0 < &1 - a \/ &1 - a = &0 \/ &1 - a < &0`) THENL
 569      [
 570        ASM_CASES_TAC `(&1 - a * a - b * b) / (&2 * a * b) < &0` THENL
 571          [
 572            MATCH_MP_TAC REAL_LE_TRANS THEN
 573              EXISTS_TAC `&0` THEN
 574              ASM_SIMP_TAC[REAL_LT_IMP_LE] THEN
 575              REWRITE_TAC[REAL_ARITH `a * b <= &0 <=> &0 <= (--a) * b`] THEN
 576              MATCH_MP_TAC REAL_LE_MUL THEN
 577              ASM_SIMP_TAC[REAL_LT_IMP_LE; REAL_ARITH `x < &0 ==> &0 <= --x`];
 578            ALL_TAC
 579          ] THEN
 580          POP_ASSUM MP_TAC THEN
 581          REWRITE_TAC[REAL_NOT_LT] THEN DISCH_TAC THEN
 582          ONCE_REWRITE_TAC[REAL_ARITH `x <= b <=> x <= &1 * b`] THEN
 583          MATCH_MP_TAC REAL_LE_MUL2 THEN
 584          ASM_SIMP_TAC[REAL_LT_IMP_LE] THEN
 585          REWRITE_TAC[REAL_ARITH `&1 - a <= b <=> &1 <= a + b`] THEN
 586          SUBGOAL_THEN `&0 <= a + b` MP_TAC THENL
 587          [
 588            MATCH_MP_TAC REAL_LE_ADD THEN ASM_SIMP_TAC[REAL_LT_IMP_LE];
 589            ALL_TAC
 590          ] THEN
 591          ONCE_REWRITE_TAC[GSYM REAL_ABS_REFL] THEN
 592          DISCH_THEN (fun th -> ONCE_REWRITE_TAC[SYM th]) THEN
 593          ONCE_REWRITE_TAC[REAL_ARITH `&1 = abs(&1)`] THEN
 594          ASM_REWRITE_TAC[REAL_LE_SQUARE_ABS; REAL_ARITH `&1 pow 2 = &1`];
 595        ALL_TAC
 596      ] THEN
 597      POP_ASSUM DISJ_CASES_TAC THENL
 598      [
 599        ASM_SIMP_TAC[REAL_MUL_RZERO; REAL_LT_IMP_LE];
 600        ALL_TAC
 601      ] THEN
 602      ASM_CASES_TAC `&0 < (&1 - a * a - b * b) / (&2 * a * b)` THENL
 603      [
 604        MATCH_MP_TAC REAL_LE_TRANS THEN
 605          EXISTS_TAC `&0` THEN
 606          ASM_SIMP_TAC[REAL_LT_IMP_LE] THEN
 607          REWRITE_TAC[REAL_ARITH `a * b <= &0 <=> &0 <= a * (--b)`] THEN
 608          MATCH_MP_TAC REAL_LE_MUL THEN
 609          ASM_SIMP_TAC[REAL_LT_IMP_LE; REAL_ARITH `x < &0 ==> &0 <= --x`];
 610        ALL_TAC
 611      ] THEN
 612      POP_ASSUM MP_TAC THEN
 613      REWRITE_TAC[REAL_NOT_LT] THEN DISCH_TAC THEN
 614      ONCE_REWRITE_TAC[REAL_ARITH `x * y <= b <=> (--x) * (--y) <= &1 * b`] THEN
 615      MATCH_MP_TAC REAL_LE_MUL2 THEN
 616      ASM_SIMP_TAC[REAL_ARITH `x <= &0 ==> &0 <= --x`; REAL_ARITH `&1 - a < &0 ==> &0 <= --(&1 - a)`] THEN
 617      ASM_REWRITE_TAC[REAL_ARITH `-- x <= &1 <=> -- &1 <= x`] THEN
 618      REMOVE_ASSUM THEN REMOVE_ASSUM THEN POP_ASSUM MP_TAC THEN
 619      REWRITE_TAC[ABS_SQUARE_LE_1] THEN
 620      REAL_ARITH_TAC);;
 621
 622
 623
 624 let rotation_dist_decrease_lemma = prove(`!v w u:real^N. u IN aff_ge {vec 0} {v,w} /\ norm u = norm v
 625                                    ==> dist (u,w) <= dist (v,w)`,
 626    REPEAT STRIP_TAC THEN
 627      ASM_CASES_TAC `v:real^N = vec 0` THENL
 628      [
 629        UNDISCH_TAC `norm (u:real^N) = norm (v:real^N)` THEN
 630          ASM_REWRITE_TAC[NORM_0; NORM_EQ_0] THEN
 631          SIMP_TAC[REAL_LE_REFL];
 632        ALL_TAC
 633      ] THEN
 634      ASM_CASES_TAC `w:real^N = vec 0` THENL
 635      [
 636        ASM_REWRITE_TAC[DIST_0; REAL_LE_REFL];
 637        ALL_TAC
 638      ] THEN
 639      REWRITE_TAC[dist] THEN
 640      ONCE_REWRITE_TAC[GSYM REAL_ABS_NORM] THEN
 641      REWRITE_TAC[REAL_LE_SQUARE_ABS] THEN
 642      REWRITE_TAC[NORM_POW_2; DOT_LSUB; DOT_RSUB] THEN
 643      ASM_REWRITE_TAC[DOT_SYM; DOT_SQUARE_NORM] THEN
 644      REWRITE_TAC[REAL_ARITH `v - uw - (uw - w) <= v - vw - (vw - w) <=> vw <= uw`] THEN
 645      SUBGOAL_THEN `~(u = vec 0:real^N)` ASSUME_TAC THENL
 646      [
 647        ASM_REWRITE_TAC[GSYM NORM_EQ_0] THEN
 648          ASM_REWRITE_TAC[NORM_EQ_0];
 649        ALL_TAC
 650      ] THEN
 651
 652      MAP_EVERY ABBREV_TAC [`v':real^N = inv (norm v) % v`; `w':real^N = inv (norm w) % w`; `u':real^N = inv (norm u) % u`] THEN
 653      SUBGOAL_THEN `norm (v':real^N) = &1 /\ norm (w':real^N) = &1 /\ norm (u':real^N) = &1` ASSUME_TAC THENL
 654      [
 655        REPLICATE_TAC 3 (POP_ASSUM (fun th -> REWRITE_TAC[SYM th])) THEN
 656          REPLICATE_TAC 3 (POP_ASSUM MP_TAC) THEN
 657          REWRITE_TAC[GSYM NORM_EQ_0; NORM_MUL] THEN
 658          SUBGOAL_THEN `!v:real^N. abs (inv (norm v)) = inv (norm v)` (fun th -> REWRITE_TAC[th]) THENL
 659          [
 660            REWRITE_TAC[REAL_ABS_REFL] THEN
 661              GEN_TAC THEN MATCH_MP_TAC REAL_LE_INV THEN
 662              REWRITE_TAC[NORM_POS_LE];
 663            ALL_TAC
 664          ] THEN
 665          SIMP_TAC[REAL_MUL_LINV];
 666        ALL_TAC
 667      ] THEN
 668      SUBGOAL_THEN `v:real^N = norm v % v' /\ w:real^N = norm w % w' /\ u:real^N = norm u % u'` ASSUME_TAC THENL
 669      [
 670        REMOVE_ASSUM THEN
 671          REPLICATE_TAC 3 (POP_ASSUM (fun th -> REWRITE_TAC[SYM th])) THEN
 672          REPLICATE_TAC 3 (POP_ASSUM MP_TAC) THEN
 673          REWRITE_TAC[VECTOR_ARITH `a % b % v = (a * b) % v:real^N`; GSYM NORM_EQ_0] THEN
 674          SIMP_TAC[REAL_MUL_RINV] THEN
 675          REWRITE_TAC[VECTOR_MUL_LID];
 676        ALL_TAC
 677      ] THEN
 678      SUBGOAL_THEN `?a b. &0 <= a /\ &0 <= b /\ u':real^N = a % v' + b % w'` ASSUME_TAC THENL
 679      [
 680        REMOVE_ASSUM THEN REMOVE_ASSUM THEN
 681          REPLICATE_TAC 3 (POP_ASSUM (fun th -> REWRITE_TAC[SYM th])) THEN
 682          FIRST_X_ASSUM (MP_TAC o check (is_binary "IN" o concl)) THEN
 683          ASM_SIMP_TAC[aff_ge_0_2] THEN
 684          REWRITE_TAC[IN_ELIM_THM] THEN
 685          REPLICATE_TAC 3 (POP_ASSUM MP_TAC) THEN
 686          REWRITE_TAC[GSYM NORM_EQ_0] THEN REPEAT STRIP_TAC THEN
 687          MAP_EVERY EXISTS_TAC [`t1:real`; `inv (norm (v:real^N)) * t2 * norm (w:real^N)`] THEN
 688          CONJ_TAC THEN ASM_REWRITE_TAC[] THEN
 689          CONJ_TAC THENL
 690          [
 691            MATCH_MP_TAC REAL_LE_MUL THEN
 692              CONJ_TAC THENL [ MATCH_MP_TAC REAL_LE_INV THEN REWRITE_TAC[NORM_POS_LE]; ALL_TAC ] THEN
 693              MATCH_MP_TAC REAL_LE_MUL THEN
 694              ASM_REWRITE_TAC[NORM_POS_LE];
 695            ALL_TAC
 696          ] THEN
 697          REWRITE_TAC[VECTOR_ARITH `(vv * t2 * ww) % iw % w = (vv * t2 * (ww * iw)) % (w:real^N)`] THEN
 698          ASM_SIMP_TAC[REAL_MUL_RINV; REAL_MUL_RID] THEN
 699          VECTOR_ARITH_TAC;
 700        ALL_TAC
 701      ] THEN
 702
 703      POP_ASSUM MP_TAC THEN
 704      POP_ASSUM (fun th -> ONCE_REWRITE_TAC[th]) THEN
 705      REPLICATE_TAC 3 (FIRST_X_ASSUM ((fun th -> ALL_TAC) o check (is_eq o concl))) THEN
 706      STRIP_TAC THEN
 707      ASM_REWRITE_TAC[DOT_LMUL; DOT_RMUL] THEN
 708      MATCH_MP_TAC REAL_LE_LMUL THEN ASM_REWRITE_TAC[NORM_POS_LE] THEN
 709      MATCH_MP_TAC REAL_LE_LMUL THEN ASM_REWRITE_TAC[NORM_POS_LE] THEN
 710
 711      ASM_CASES_TAC `a = &0` THENL
 712      [
 713        UNDISCH_TAC `u':real^N = a % v' + b % w'` THEN
 714          ASM_REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_LID] THEN
 715          DISCH_THEN (MP_TAC o AP_TERM `norm:real^N->real`) THEN
 716          ASM_REWRITE_TAC[NORM_MUL; REAL_MUL_LZERO; REAL_ADD_LID] THEN
 717          ASM_SIMP_TAC[REAL_ARITH `&0 <= b ==> abs b = b`; REAL_MUL_RID] THEN
 718          DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN
 719          REWRITE_TAC[DOT_LMUL; DOT_SQUARE_NORM; REAL_MUL_LID] THEN
 720          ASM_REWRITE_TAC[VECTOR_ANGLE; REAL_POW_2; REAL_MUL_LID] THEN
 721          REWRITE_TAC[COS_BOUNDS];
 722        ALL_TAC
 723      ] THEN
 724
 725      ASM_CASES_TAC `b = &0` THENL
 726      [
 727        UNDISCH_TAC `u':real^N = a % v' + b % w'` THEN
 728          ASM_REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_RID] THEN
 729          DISCH_THEN (MP_TAC o AP_TERM `norm:real^N -> real`) THEN
 730          ASM_SIMP_TAC[NORM_MUL; REAL_ARITH `&0 <= t1 ==> abs t1 = t1`; REAL_MUL_RID] THEN
 731          DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN
 732          REWRITE_TAC[DOT_LMUL; REAL_MUL_LID; REAL_LE_REFL];
 733        ALL_TAC
 734      ] THEN
 735
 736      ASM_REWRITE_TAC[DOT_LADD; DOT_LMUL; DOT_SQUARE_NORM; REAL_POW_2; REAL_MUL_RID] THEN
 737      REWRITE_TAC[REAL_ARITH `vw <= a * vw + b <=> vw * (&1 - a) <= b`] THEN
 738      MATCH_MP_TAC aux_ineq THEN
 739      ASM_REWRITE_TAC[REAL_ARITH `&0 < a <=> &0 <= a /\ ~(a = &0)`] THEN
 740      CONJ_TAC THENL
 741      [
 742        UNDISCH_TAC `u':real^N = a % v' + b % w'` THEN
 743          DISCH_THEN (MP_TAC o AP_TERM `norm:real^N->real`) THEN
 744          ASM_REWRITE_TAC[] THEN
 745          ONCE_REWRITE_TAC[GSYM REAL_ABS_NORM] THEN
 746          ONCE_REWRITE_TAC[REAL_ARITH `&1 = abs(&1)`] THEN
 747          REWRITE_TAC[REAL_EQ_SQUARE_ABS; NORM_POW_2; DOT_LADD; DOT_RADD; DOT_SYM; DOT_LMUL; DOT_RMUL] THEN
 748          ASM_REWRITE_TAC[DOT_SQUARE_NORM; REAL_MUL_RID; REAL_POW_2; REAL_MUL_RID] THEN
 749          REWRITE_TAC[REAL_ARITH `abs(&1) = &1`] THEN
 750          POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN
 751          CONV_TAC REAL_FIELD;
 752        ALL_TAC
 753      ] THEN
 754      ASM_REWRITE_TAC[VECTOR_ANGLE; REAL_MUL_LID; COS_BOUNDS]);;
 755
 756
 757
 758 let rotation_dist_decrease_special_case = prove(`!(v:real^N) w u a. &0 <= a /\ w = --a % v /\ norm u = norm v ==> dist (u,w) <= dist (v,w)`,
 759     REPEAT STRIP_TAC THEN
 760       REWRITE_TAC[dist] THEN ONCE_REWRITE_TAC[GSYM REAL_ABS_NORM] THEN
 761       REWRITE_TAC[REAL_LE_SQUARE_ABS] THEN
 762       REWRITE_TAC[NORM_POW_2; DOT_LSUB; DOT_RSUB] THEN
 763       REWRITE_TAC[DOT_SYM; DOT_SQUARE_NORM] THEN
 764       ASM_REWRITE_TAC[DOT_RMUL] THEN
 765       REWRITE_TAC[REAL_ARITH `vv - uv - (uv - ww) <= vv - v2 - (v2 - ww) <=> --uv <= --v2`] THEN
 766       REWRITE_TAC[REAL_NEG_LMUL; REAL_NEG_NEG] THEN
 767       MATCH_MP_TAC REAL_LE_LMUL THEN ASM_REWRITE_TAC[] THEN
 768       ASM_REWRITE_TAC[VECTOR_ANGLE] THEN
 769       REPEAT (MATCH_MP_TAC REAL_LE_LMUL THEN REWRITE_TAC[NORM_POS_LE]) THEN
 770       REWRITE_TAC[VECTOR_ANGLE_REFL] THEN
 771       ASM_CASES_TAC `v:real^N = vec 0` THEN ASM_REWRITE_TAC[] THENL
 772       [
 773         REWRITE_TAC[vector_angle; REAL_LE_REFL];
 774         REWRITE_TAC[COS_0; COS_BOUNDS]
 775       ]);;
 776
 777
 778
 779
 780 (******************************************************************)
 781
 782 (* Lemmas about continuous functions *)
 783
 784
 785 let continuous_lemma_inc = prove(`!f c t1. &0 <= t1 /\
 786                                 f real_continuous_on real_interval [&0,t1] /\
 787                                 f (&0) <= c /\ c <= f t1
 788                                 ==> ?x. &0 <= x /\ x <= t1 /\ f x = c /\
 789                                         (!t. &0 <= t /\ t < x ==> f t < c)`,
 790    REPEAT STRIP_TAC THEN
 791      ABBREV_TAC `s = {t | &0 <= t /\ t <= t1 /\ c <= f t}` THEN
 792      SUBGOAL_THEN `t1:real IN s` ASSUME_TAC THENL
 793      [
 794        EXPAND_TAC "s" THEN ASM_REWRITE_TAC[IN_ELIM_THM; REAL_LE_REFL];
 795        ALL_TAC
 796      ] THEN
 797      EXISTS_TAC `inf s` THEN
 798      MP_TAC (SPEC `s:real->bool` INF) THEN
 799      ANTS_TAC THENL
 800      [
 801        ASM_REWRITE_TAC[GSYM MEMBER_NOT_EMPTY] THEN
 802          CONJ_TAC THENL [ EXISTS_TAC `t1:real` THEN ASM_REWRITE_TAC[]; EXISTS_TAC `&0` ] THEN
 803          GEN_TAC THEN EXPAND_TAC "s" THEN
 804          SIMP_TAC[IN_ELIM_THM];
 805        ALL_TAC
 806      ] THEN
 807      STRIP_TAC THEN
 808
 809      (* 0 <= inf s *)
 810      SUBGOAL_THEN `&0 <= inf s` ASSUME_TAC THENL
 811      [
 812        POP_ASSUM (MP_TAC o SPEC `&0`) THEN
 813          ANTS_TAC THEN SIMP_TAC[] THEN
 814          GEN_TAC THEN EXPAND_TAC "s" THEN
 815          SIMP_TAC[IN_ELIM_THM];
 816        ALL_TAC
 817      ] THEN
 818
 819      (* inf s <= t1 *)
 820      SUBGOAL_THEN `inf s <= t1` ASSUME_TAC THENL
 821      [
 822        REMOVE_ASSUM THEN POP_ASSUM (MP_TAC o SPEC `t1:real`) THEN
 823          ASM_SIMP_TAC[];
 824        ALL_TAC
 825      ] THEN
 826
 827      (* f t < c for all t IN [0,inf s) *)
 828      SUBGOAL_THEN `!t. &0 <= t /\ t < inf s ==> f t < c` ASSUME_TAC THENL
 829      [
 830        GEN_TAC THEN
 831          DISCH_THEN (LABEL_TAC "A") THEN
 832          SUBGOAL_THEN `&0 <= t /\ t <= t1` ASSUME_TAC THENL
 833          [
 834            ASM_REWRITE_TAC[] THEN
 835              MATCH_MP_TAC REAL_LT_IMP_LE THEN
 836              MATCH_MP_TAC REAL_LTE_TRANS THEN
 837              EXISTS_TAC `inf s` THEN
 838              ASM_REWRITE_TAC[];
 839            ALL_TAC
 840          ] THEN
 841          USE_THEN "A" MP_TAC THEN
 842          ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN
 843          REWRITE_TAC[REAL_NOT_LT; DE_MORGAN_THM] THEN
 844          DISCH_TAC THEN DISJ2_TAC THEN
 845          FIRST_X_ASSUM MATCH_MP_TAC THEN
 846          EXPAND_TAC "s" THEN ASM_REWRITE_TAC[IN_ELIM_THM];
 847        ALL_TAC
 848      ] THEN
 849
 850      ASM_REWRITE_TAC[] THEN
 851
 852      (* f(inf s) = c *)
 853      DISJ_CASES_TAC (REAL_ARITH `c < f (inf s) \/ f (inf s) = c \/ f (inf s) < c`) THENL
 854      [
 855        (* f(inf s) > c *)
 856        MP_TAC (SPECL [`f:real->real`; `&0`; `inf s`; `c:real`] REAL_IVT_INCREASING) THEN
 857          ANTS_TAC THENL
 858          [
 859            ASM_SIMP_TAC[REAL_LT_IMP_LE] THEN
 860              MATCH_MP_TAC REAL_CONTINUOUS_ON_SUBSET THEN
 861              EXISTS_TAC `real_interval [&0,t1]` THEN
 862              ASM_REWRITE_TAC[] THEN
 863              ASM_REWRITE_TAC[SUBSET_REAL_INTERVAL; REAL_LE_REFL];
 864            ALL_TAC
 865          ] THEN
 866          REWRITE_TAC[IN_REAL_INTERVAL] THEN
 867          STRIP_TAC THEN
 868          ASM_CASES_TAC `x = inf s` THENL
 869          [
 870            UNDISCH_TAC `f (x:real) = c:real` THEN
 871              ASM_SIMP_TAC[];
 872            ALL_TAC
 873          ] THEN
 874          FIRST_X_ASSUM (MP_TAC o SPEC `x:real`) THEN
 875          ASM_REWRITE_TAC[REAL_ARITH `x < inf s <=> x <= inf s /\ ~(x = inf s)`] THEN
 876          REWRITE_TAC[REAL_LT_REFL];
 877        ALL_TAC
 878      ] THEN
 879      POP_ASSUM DISJ_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
 880
 881      (* f(inf s) < c *)
 882      UNDISCH_TAC `f real_continuous_on real_interval [&0,t1]` THEN
 883      REWRITE_TAC[real_continuous_on] THEN
 884      DISCH_THEN (MP_TAC o SPEC `inf s`) THEN
 885      ASM_REWRITE_TAC[IN_REAL_INTERVAL] THEN
 886      DISCH_THEN (MP_TAC o SPEC `c - f (inf s)`) THEN
 887      ANTS_TAC THENL
 888      [
 889        POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;
 890        ALL_TAC
 891      ] THEN
 892      STRIP_TAC THEN
 893      ABBREV_TAC `p = inf s + min (d / &2) (t1 - inf s)` THEN
 894      SUBGOAL_THEN `!t. &0 <= t /\ t <= p ==> f t < c` ASSUME_TAC THENL
 895      [
 896        GEN_TAC THEN
 897          ASM_CASES_TAC `t < inf s` THENL
 898          [
 899            DISCH_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
 900              ASM_REWRITE_TAC[];
 901            ALL_TAC
 902          ] THEN
 903          POP_ASSUM MP_TAC THEN REWRITE_TAC[REAL_NOT_LT] THEN
 904          REPEAT STRIP_TAC THEN
 905          FIRST_X_ASSUM (MP_TAC o SPEC `t:real`) THEN
 906          ANTS_TAC THENL
 907          [
 908            ASM_REWRITE_TAC[] THEN
 909              CONJ_TAC THENL
 910              [
 911                MATCH_MP_TAC REAL_LE_TRANS THEN
 912                  EXISTS_TAC `p:real` THEN
 913                  ASM_REWRITE_TAC[] THEN
 914                  EXPAND_TAC "p" THEN
 915                  REWRITE_TAC[REAL_ARITH `a + b <= t1 <=> b <= t1 - a`] THEN
 916                  REWRITE_TAC[REAL_MIN_MIN];
 917                ALL_TAC
 918              ] THEN
 919              MATCH_MP_TAC (REAL_ARITH `!a. &0 < d /\ a < d /\ &0 <= a ==> abs a < d`) THEN
 920              ASM_REWRITE_TAC[REAL_ARITH `&0 <= a - b <=> b <= a`] THEN
 921              MATCH_MP_TAC REAL_LET_TRANS THEN
 922              EXISTS_TAC `p - inf s` THEN
 923              ASM_REWRITE_TAC[REAL_ARITH `a - b <= c - b <=> a <= c`] THEN
 924              EXPAND_TAC "p" THEN
 925              REWRITE_TAC[REAL_ARITH `(a + b) - a = b`] THEN
 926              MATCH_MP_TAC REAL_LET_TRANS THEN
 927              EXISTS_TAC `d / &2` THEN
 928              ASM_SIMP_TAC[REAL_MIN_MIN; REAL_ARITH `&0 < d ==> d / &2 < d`];
 929            ALL_TAC
 930          ] THEN
 931          REAL_ARITH_TAC;
 932        ALL_TAC
 933      ] THEN
 934      SUBGOAL_THEN `p <= inf s` MP_TAC THENL
 935      [
 936        FIRST_X_ASSUM MATCH_MP_TAC THEN
 937          GEN_TAC THEN
 938          ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN
 939          REWRITE_TAC[REAL_NOT_LE] THEN
 940          DISCH_TAC THEN FIRST_X_ASSUM (MP_TAC o SPEC `x:real`) THEN
 941          EXPAND_TAC "s" THEN REWRITE_TAC[IN_ELIM_THM; DE_MORGAN_THM] THEN
 942          ASM_SIMP_TAC[REAL_LT_IMP_LE] THEN
 943          ASM_CASES_TAC `&0 <= x` THEN ASM_REWRITE_TAC[] THEN
 944          SIMP_TAC[REAL_NOT_LE];
 945        ALL_TAC
 946      ] THEN
 947      SUBGOAL_THEN `inf s < p` MP_TAC THENL
 948      [
 949        EXPAND_TAC "p" THEN
 950          REWRITE_TAC[REAL_ARITH `a < a + b <=> &0 < b`] THEN
 951          ASM_SIMP_TAC[REAL_LT_MIN; REAL_ARITH `&0 < d ==> &0 < d / &2`] THEN
 952          ASM_CASES_TAC `inf s = t1` THENL
 953          [
 954            UNDISCH_TAC `f (inf s) < c` THEN
 955              POP_ASSUM (fun th -> REWRITE_TAC[th]) THEN
 956              UNDISCH_TAC `c <= f (t1:real)` THEN
 957              REAL_ARITH_TAC;
 958            ALL_TAC
 959          ] THEN
 960          ASM_REWRITE_TAC[REAL_ARITH `&0 < t1 - inf s <=> inf s <= t1 /\ ~(inf s = t1)`];
 961        ALL_TAC
 962      ] THEN
 963      REAL_ARITH_TAC);;
 964
 965
 966
 967 let continuous_lemma_dec = prove(`!f c t1. &0 <= t1 /\
 968                                    f real_continuous_on real_interval [&0,t1] /\
 969                                    c <= f (&0) /\ f t1 <= c
 970                                    ==> ?x. &0 <= x /\ x <= t1 /\ f x = c /\
 971                                         (!t. &0 <= t /\ t < x ==> c < f t)`,
 972    REPEAT STRIP_TAC THEN
 973      MP_TAC (SPECL [`\t. --(f:real->real) t`; `--c:real`; `t1:real`] continuous_lemma_inc) THEN
 974      ASM_REWRITE_TAC[] THEN
 975      ANTS_TAC THENL
 976      [
 977        CONJ_TAC THENL
 978          [
 979            MATCH_MP_TAC REAL_CONTINUOUS_ON_NEG THEN
 980              ASM_REWRITE_TAC[];
 981            ALL_TAC
 982          ] THEN
 983          ASM_REWRITE_TAC[REAL_LE_NEG];
 984        ALL_TAC
 985      ] THEN
 986      STRIP_TAC THEN
 987      EXISTS_TAC `x:real` THEN
 988      ASM_REWRITE_TAC[] THEN
 989      CONJ_TAC THENL
 990      [
 991        ONCE_REWRITE_TAC[REAL_ARITH `a = b <=> --a = --b`] THEN
 992          ASM_REWRITE_TAC[];
 993        ALL_TAC
 994      ] THEN
 995      GEN_TAC THEN STRIP_TAC THEN
 996      FIRST_X_ASSUM (MP_TAC o SPEC `t:real`) THEN
 997      ASM_REWRITE_TAC[REAL_LT_NEG]);;
 998
 999
1000
1001
1002
1003
1004
1005
1006
1007 (******************************************************)
1008
1009 (* Rotation lemmas *)
1010
1011
1012 let rotation_lemma_special = prove(`!v w n:real^N. ~(v = vec 0) /\ ~(w = vec 0) /\
1013                                      (v dot n = &0) /\ (w dot n = &0) /\
1014                                      3 <= dimindex(:N) ==>
1015                                      ?f:real^1->real^N. f continuous_on UNIV /\
1016                                                         f(lift (&0)) = v /\ f(lift (&1)) = norm v / norm w % w /\
1017                                                         (!t. norm (f t) = norm v /\ f t dot n = &0) /\
1018                                                         (!t. &0 <= t /\ t <= &1 ==> dist (f (lift t), w) <= dist (v, w)) /\
1019                                                         (~collinear {vec 0, v, w} ==> (!t. &0 <= t /\ t <= &1 ==> f (lift t) IN aff_ge {vec 0} {v, w}))`,
1020    REPEAT GEN_TAC THEN STRIP_TAC THEN
1021      SUBGOAL_THEN `~(norm (v:real^N) = &0) /\ ~(norm (w:real^N) = &0)` ASSUME_TAC THENL
1022      [
1023        ASM_REWRITE_TAC[NORM_EQ_0];
1024        ALL_TAC
1025      ] THEN
1026
1027      ABBREV_TAC `u = norm (v:real^N) / norm w % w:real^N` THEN
1028      SUBGOAL_THEN `norm (u:real^N) = norm (v:real^N)` ASSUME_TAC THENL
1029      [
1030        POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN
1031          REWRITE_TAC[NORM_MUL; REAL_ABS_DIV; REAL_ABS_NORM; real_div] THEN
1032          ASM_SIMP_TAC[GSYM REAL_MUL_ASSOC; REAL_MUL_LINV; REAL_MUL_RID];
1033        ALL_TAC
1034      ] THEN
1035      SUBGOAL_THEN `~(u = vec 0:real^N)` ASSUME_TAC THENL
1036      [
1037        ASM_REWRITE_TAC[GSYM NORM_EQ_0];
1038        ALL_TAC
1039      ] THEN
1040      SUBGOAL_THEN `aff_ge {vec 0} {v,w} = aff_ge {vec 0:real^N} {v,u}` ASSUME_TAC THENL
1041      [
1042        MATCH_MP_TAC aff_ge_eq_lemma THEN
1043          EXISTS_TAC `norm (v:real^N) / norm (w:real^N)` THEN
1044          ASM_REWRITE_TAC[] THEN
1045          MATCH_MP_TAC REAL_LT_DIV THEN
1046          ASM_REWRITE_TAC[NORM_POS_LE; REAL_ARITH `&0 < a <=> &0 <= a /\ ~(a = &0)`];
1047        ALL_TAC
1048      ] THEN
1049      SUBGOAL_THEN `collinear {vec 0, v, w:real^N} <=> collinear {vec 0, v, u}` (fun th -> REWRITE_TAC[th]) THENL
1050      [
1051        MP_TAC (ISPECL [`&1`; `norm (v:real^N) / norm (w:real^N)`; `v:real^N`; `w:real^N`] COLLINEAR_SCALE_ALL) THEN
1052          ANTS_TAC THENL
1053          [
1054            REWRITE_TAC[REAL_ARITH `~(&1 = &0)`] THEN
1055              MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~(a = &0)`) THEN
1056              MATCH_MP_TAC REAL_LT_DIV THEN
1057              ASM_REWRITE_TAC[NORM_POS_LT];
1058            ALL_TAC
1059          ] THEN
1060          DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN
1061          ASM_REWRITE_TAC[VECTOR_MUL_LID];
1062        ALL_TAC
1063      ] THEN
1064
1065      ASM_CASES_TAC `~collinear {vec 0,v,u:real^N}` THENL
1066      [
1067        MP_TAC (SPECL [`v:real^N`; `u:real^N`] rotation_lemma) THEN
1068          ASM_REWRITE_TAC[] THEN
1069          STRIP_TAC THEN
1070          EXISTS_TAC `f:real^1->real^N` THEN
1071          ASM_REWRITE_TAC[] THEN
1072          CONJ_TAC THENL
1073          [
1074            GEN_TAC THEN
1075              UNDISCH_TAC `!t:real^1. ?a b. f t = a % v + b % u:real^N` THEN
1076              DISCH_THEN (MP_TAC o SPEC `t:real^1`) THEN STRIP_TAC THEN
1077              ASM_REWRITE_TAC[] THEN
1078              UNDISCH_TAC `f (lift (&1)) = u:real^N` THEN
1079              DISCH_THEN (fun th -> ALL_TAC) THEN
1080              EXPAND_TAC "u" THEN
1081              REWRITE_TAC[DOT_LADD; DOT_LMUL] THEN
1082              ASM_REWRITE_TAC[REAL_MUL_RZERO; REAL_ADD_LID];
1083            ALL_TAC
1084          ] THEN
1085          CONJ_TAC THENL
1086          [
1087            REPEAT STRIP_TAC THEN
1088              MATCH_MP_TAC rotation_dist_decrease_lemma THEN
1089              ASM_REWRITE_TAC[] THEN
1090              FIRST_X_ASSUM MATCH_MP_TAC THEN
1091              ASM_REWRITE_TAC[IN_INTERVAL_1];
1092            ALL_TAC
1093          ] THEN
1094          REPEAT STRIP_TAC THEN
1095          FIRST_X_ASSUM MATCH_MP_TAC THEN
1096          ASM_REWRITE_TAC[IN_INTERVAL_1];
1097        ALL_TAC
1098      ] THEN
1099
1100      ASM_REWRITE_TAC[] THEN
1101      POP_ASSUM MP_TAC THEN
1102      ASM_REWRITE_TAC[COLLINEAR_LEMMA_ALT] THEN
1103      STRIP_TAC THEN
1104      FIRST_ASSUM (MP_TAC o AP_TERM `norm:real^N->real`) THEN
1105      ASM_REWRITE_TAC[NORM_MUL] THEN
1106      ASM_REWRITE_TAC[REAL_ARITH `v = c * v <=> v * (c - &1) = &0`; REAL_ENTIRE; REAL_ARITH `abs c - &1 = &0 <=> c = &1 \/ c = -- &1`] THEN
1107      DISCH_THEN DISJ_CASES_TAC THENL
1108      [
1109        EXISTS_TAC `(\t:real^1. v:real^N)` THEN
1110          ASM_REWRITE_TAC[CONTINUOUS_ON_CONST; VECTOR_MUL_LID; REAL_LE_REFL];
1111        ALL_TAC
1112      ] THEN
1113
1114      SUBGOAL_THEN `?e:real^N. e dot v = &0 /\ norm e = norm v /\ e dot n = &0` ASSUME_TAC THENL
1115      [
1116        SUBGOAL_THEN `dim {v:real^N,n} < dimindex (:N)` ASSUME_TAC THENL
1117          [
1118            MATCH_MP_TAC LET_TRANS THEN
1119              EXISTS_TAC `2` THEN
1120              ASM_SIMP_TAC[ARITH_RULE `3 <= a ==> 2 < a`] THEN
1121              MATCH_MP_TAC LE_TRANS THEN
1122              EXISTS_TAC `CARD {v:real^N,n}` THEN
1123              SUBGOAL_THEN `FINITE {v:real^N,n}` ASSUME_TAC THENL
1124              [
1125                REWRITE_TAC[FINITE_INSERT; FINITE_EMPTY];
1126                ALL_TAC
1127              ] THEN
1128              ASM_SIMP_TAC[DIM_LE_CARD] THEN
1129              REWRITE_TAC[Geomdetail.CARD2];
1130            ALL_TAC
1131          ] THEN
1132          MP_TAC (SPEC `{v:real^N,n}` ORTHOGONAL_TO_SUBSPACE_EXISTS) THEN
1133          ASM_REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY; orthogonal] THEN
1134          STRIP_TAC THEN
1135          EXISTS_TAC `norm (v:real^N) / norm (x:real^N) % x:real^N` THEN
1136          FIRST_ASSUM (MP_TAC o SPEC `v:real^N`) THEN
1137          FIRST_X_ASSUM (MP_TAC o SPEC `n:real^N`) THEN
1138          REWRITE_TAC[] THEN REPEAT DISCH_TAC THEN
1139          ASM_REWRITE_TAC[NORM_MUL; REAL_ABS_DIV; REAL_ABS_NORM; real_div; GSYM REAL_MUL_ASSOC; DOT_LMUL; REAL_MUL_RZERO] THEN
1140          UNDISCH_TAC `~(x:real^N = vec 0)` THEN
1141          SIMP_TAC[GSYM NORM_EQ_0; REAL_MUL_LINV; REAL_MUL_RID];
1142        ALL_TAC
1143      ] THEN
1144
1145      POP_ASSUM MP_TAC THEN STRIP_TAC THEN
1146
1147      ABBREV_TAC `f = (\t:real^1. cos (pi * drop t) % v + sin (pi * drop t) % e:real^N)` THEN
1148      EXISTS_TAC `f:real^1->real^N` THEN
1149
1150      CONJ_TAC THENL
1151      [
1152        EXPAND_TAC "f" THEN
1153          MATCH_MP_TAC CONTINUOUS_ON_ADD THEN
1154          CONJ_TAC THEN MATCH_MP_TAC CONTINUOUS_ON_VMUL THENL
1155          [
1156            SUBGOAL_THEN `lift o (\t:real^1. cos (pi * drop t)) = (lift o cos o drop) o (\t:real^1. pi % t)` (fun th -> REWRITE_TAC[th]) THENL
1157              [
1158                REWRITE_TAC[FUN_EQ_THM; o_THM; DROP_CMUL];
1159                ALL_TAC
1160              ] THEN
1161              MATCH_MP_TAC CONTINUOUS_ON_COMPOSE THEN
1162              CONJ_TAC THENL [ MATCH_MP_TAC CONTINUOUS_ON_CMUL THEN REWRITE_TAC [CONTINUOUS_ON_ID]; ALL_TAC ] THEN
1163              MATCH_MP_TAC CONTINUOUS_AT_IMP_CONTINUOUS_ON THEN
1164              GEN_TAC THEN DISCH_TAC THEN
1165              MP_TAC (SPEC `drop (x:real^1)` REAL_CONTINUOUS_AT_COS) THEN
1166              REWRITE_TAC[REAL_CONTINUOUS_CONTINUOUS_ATREAL; LIFT_DROP];
1167
1168            SUBGOAL_THEN `lift o (\t:real^1. sin (pi * drop t)) = (lift o sin o drop) o (\t:real^1. pi % t)` (fun th -> REWRITE_TAC[th]) THENL
1169              [
1170                REWRITE_TAC[FUN_EQ_THM; o_THM; DROP_CMUL];
1171                ALL_TAC
1172              ] THEN
1173              MATCH_MP_TAC CONTINUOUS_ON_COMPOSE THEN
1174              CONJ_TAC THENL [ MATCH_MP_TAC CONTINUOUS_ON_CMUL THEN REWRITE_TAC [CONTINUOUS_ON_ID]; ALL_TAC ] THEN
1175              MATCH_MP_TAC CONTINUOUS_AT_IMP_CONTINUOUS_ON THEN
1176              GEN_TAC THEN DISCH_TAC THEN
1177              MP_TAC (SPEC `drop (x:real^1)` REAL_CONTINUOUS_AT_SIN) THEN
1178              REWRITE_TAC[REAL_CONTINUOUS_CONTINUOUS_ATREAL; LIFT_DROP];
1179          ];
1180        ALL_TAC
1181      ] THEN
1182
1183      CONJ_TAC THENL
1184      [
1185        EXPAND_TAC "f" THEN
1186          REWRITE_TAC[LIFT_DROP; REAL_MUL_RZERO; COS_0; SIN_0; VECTOR_MUL_LID; VECTOR_MUL_LZERO; VECTOR_ADD_RID];
1187        ALL_TAC
1188      ] THEN
1189
1190      CONJ_TAC THENL
1191      [
1192        EXPAND_TAC "f" THEN
1193          ASM_REWRITE_TAC[LIFT_DROP; REAL_MUL_RID; COS_PI; SIN_PI; VECTOR_MUL_LZERO; VECTOR_ADD_RID];
1194        ALL_TAC
1195      ] THEN
1196
1197      SUBGOAL_THEN `!t:real^1. norm ((f:real^1->real^N) t) = norm (v:real^N)` ASSUME_TAC THENL
1198      [
1199        EXPAND_TAC "f" THEN
1200          GEN_TAC THEN
1201          ONCE_REWRITE_TAC[GSYM REAL_ABS_NORM] THEN
1202          REWRITE_TAC[REAL_EQ_SQUARE_ABS] THEN
1203          ASM_REWRITE_TAC[NORM_POW_2; DOT_LADD; DOT_RADD; DOT_LMUL; DOT_RMUL; DOT_SYM; REAL_MUL_RZERO; REAL_ADD_LID; REAL_ADD_RID] THEN
1204          ASM_REWRITE_TAC[DOT_SQUARE_NORM] THEN
1205          REWRITE_TAC[REAL_ARITH `c * c * n + s * s * n = (s pow 2 + c pow 2) * n`] THEN
1206          REWRITE_TAC[SIN_CIRCLE; REAL_MUL_LID];
1207        ALL_TAC
1208      ] THEN
1209
1210      ASM_REWRITE_TAC[] THEN
1211      CONJ_TAC THENL
1212      [
1213        GEN_TAC THEN EXPAND_TAC "f" THEN
1214          ASM_REWRITE_TAC[DOT_LADD; DOT_LMUL; REAL_MUL_RZERO; REAL_ADD_RID];
1215        ALL_TAC
1216      ] THEN
1217
1218      GEN_TAC THEN DISCH_TAC THEN
1219      MATCH_MP_TAC rotation_dist_decrease_special_case THEN
1220      ASM_REWRITE_TAC[] THEN
1221      EXISTS_TAC `norm(w:real^N) / norm(v:real^N)` THEN
1222      CONJ_TAC THENL
1223      [
1224        MATCH_MP_TAC REAL_LE_DIV THEN
1225          REWRITE_TAC[NORM_POS_LE];
1226        ALL_TAC
1227      ] THEN
1228      UNDISCH_TAC `norm (v:real^N) / norm (w:real^N) % w = u` THEN
1229      DISCH_THEN (MP_TAC o AP_TERM `\x:real^N. norm (w:real^N) / norm (v:real^N) % x`) THEN
1230      REWRITE_TAC[VECTOR_MUL_ASSOC; real_div] THEN
1231      ONCE_REWRITE_TAC[REAL_ARITH `(w * iv) * v * iw = (w * iw) * (v * iv)`] THEN
1232      ASM_SIMP_TAC[REAL_MUL_RINV; REAL_MUL_LID; VECTOR_MUL_LID] THEN
1233      VECTOR_ARITH_TAC);;
1234
1235
1236
1237 (* Consider properties of intersecting segments *)
1238 let aff_ge_inter_segments = prove(`!v w u p:real^N. ~collinear {vec 0, v, u} /\ p IN aff_ge {vec 0} {v, u} /\
1239                                            ~(segment [v, w] INTER aff_ge {vec 0} {u} = {})
1240                                            ==> ~(segment [p, w] INTER aff_ge {vec 0} {u} = {})`,
1241    REPEAT STRIP_TAC THEN
1242      SUBGOAL_THEN `(?x y. &0 <= x /\ x <= &1 /\ &0 <= y /\ (&1 - x) % p + x % w:real^N = y % u) ==> ~(segment [p,w] INTER aff_ge {vec 0} {u} = {})` MP_TAC THENL
1243      [
1244        STRIP_TAC THEN
1245          REWRITE_TAC[GSYM MEMBER_NOT_EMPTY] THEN
1246          REWRITE_TAC[IN_INTER; IN_SEGMENT; HALFLINE; VECTOR_MUL_RZERO; VECTOR_ADD_LID] THEN
1247          EXISTS_TAC `(&1 - x) % p + x % w:real^N` THEN
1248          CONJ_TAC THENL
1249          [
1250            REMOVE_ASSUM THEN
1251              EXISTS_TAC `x:real` THEN
1252              ASM_REWRITE_TAC[];
1253            ALL_TAC
1254          ] THEN
1255          ASM_REWRITE_TAC[IN_ELIM_THM] THEN
1256          EXISTS_TAC `y:real` THEN
1257          ASM_REWRITE_TAC[];
1258        ALL_TAC
1259      ] THEN
1260      ASM_REWRITE_TAC[TAUT `~(A ==> ~B) <=> A /\ B`] THEN
1261      REMOVE_ASSUM THEN
1262
1263      SUBGOAL_THEN `~(v = vec 0:real^N) /\ ~(u = vec 0:real^N)` ASSUME_TAC THENL
1264      [
1265        UNDISCH_TAC `~collinear {vec 0, v, u:real^N}` THEN
1266          SIMP_TAC[COLLINEAR_LEMMA; DE_MORGAN_THM];
1267        ALL_TAC
1268      ] THEN
1269
1270      UNDISCH_TAC `p IN aff_ge {vec 0:real^N} {v, u}` THEN
1271      ASM_SIMP_TAC[aff_ge_0_2; IN_ELIM_THM] THEN
1272      STRIP_TAC THEN
1273
1274      SUBGOAL_THEN `?a c. &0 <= a /\ a <= &1 /\ &0 <= c /\ (&1 - a) % v + a % w = c % u:real^N` MP_TAC THENL
1275      [
1276        UNDISCH_TAC `~(segment [v,w] INTER aff_ge {vec 0} {u:real^N} = {})` THEN
1277          REWRITE_TAC[GSYM MEMBER_NOT_EMPTY; IN_INTER; IN_SEGMENT; HALFLINE; IN_ELIM_THM] THEN
1278          REWRITE_TAC[VECTOR_MUL_RZERO; VECTOR_ADD_LID] THEN
1279          STRIP_TAC THEN
1280          MAP_EVERY EXISTS_TAC [`u':real`; `t:real`] THEN
1281          ASM_REWRITE_TAC[] THEN
1282          POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN
1283          ASM_REWRITE_TAC[];
1284        ALL_TAC
1285      ] THEN
1286      STRIP_TAC THEN
1287
1288      ASM_CASES_TAC `a = &0` THENL
1289      [
1290        MAP_EVERY EXISTS_TAC [`&0`; `t1 * c + t2:real`] THEN
1291          REWRITE_TAC[REAL_LE_REFL; REAL_LE_01; VECTOR_MUL_LZERO; VECTOR_ADD_RID; REAL_SUB_RZERO; VECTOR_MUL_LID] THEN
1292          CONJ_TAC THENL
1293          [
1294            MATCH_MP_TAC REAL_LE_ADD THEN
1295              ASM_REWRITE_TAC[] THEN
1296              MATCH_MP_TAC REAL_LE_MUL THEN
1297              ASM_REWRITE_TAC[];
1298            ALL_TAC
1299          ] THEN
1300
1301          ASM_REWRITE_TAC[] THEN
1302          UNDISCH_TAC `(&1 - a) % v + a % w = c % u:real^N` THEN
1303          ASM_REWRITE_TAC[REAL_SUB_RZERO; VECTOR_MUL_LID; VECTOR_MUL_LZERO; VECTOR_ADD_RID] THEN
1304          DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
1305          VECTOR_ARITH_TAC;
1306        ALL_TAC
1307      ] THEN
1308
1309      FIRST_X_ASSUM (MP_TAC o AP_TERM `\x:real^N. inv a % x` o check (is_eq o concl)) THEN
1310      ASM_REWRITE_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC] THEN
1311      ASM_SIMP_TAC[REAL_MUL_LINV; VECTOR_MUL_LID] THEN
1312      REWRITE_TAC[VECTOR_ARITH `v + w = z <=> w = z - v:real^N`] THEN
1313      DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
1314      REWRITE_TAC[VECTOR_ARITH `x % (a % u - b % v) = (x * a) % u + (--x * b) % v:real^N`] THEN
1315      REWRITE_TAC[VECTOR_ARITH `y % u - (a % v + b % u) = (y - b) % u + (--a) % v:real^N`] THEN
1316
1317      ABBREV_TAC `b = inv a * (&1 - a)` THEN
1318      ABBREV_TAC `d = inv a * c` THEN
1319
1320      ASM_CASES_TAC `t1 = &0` THENL
1321      [
1322        MAP_EVERY EXISTS_TAC [`&0`; `t2:real`] THEN
1323          ASM_REWRITE_TAC[REAL_LE_REFL; REAL_LE_01; REAL_MUL_LZERO; VECTOR_MUL_LZERO; REAL_MUL_LNEG; VECTOR_MUL_LNEG; REAL_SUB_RZERO; REAL_SUB_REFL; REAL_MUL_LID];
1324        ALL_TAC
1325      ] THEN
1326
1327      SUBGOAL_THEN `&0 <= b /\ &0 <= d` ASSUME_TAC THENL
1328      [
1329        SUBGOAL_THEN `&0 <= inv a` ASSUME_TAC THENL [ MATCH_MP_TAC REAL_LE_INV THEN ASM_REWRITE_TAC[]; ALL_TAC ] THEN
1330          EXPAND_TAC "b" THEN EXPAND_TAC "d" THEN
1331          CONJ_TAC THEN MATCH_MP_TAC REAL_LE_MUL THEN ASM_REWRITE_TAC[REAL_ARITH `&0 <= &1 - a <=> a <= &1`];
1332        ALL_TAC
1333      ] THEN
1334
1335      ABBREV_TAC `x = t1 / (b + t1)` THEN
1336      MAP_EVERY EXISTS_TAC [`x:real`; `(&1 - x) * t2 + x * d`] THEN
1337      SUBGOAL_THEN `&0 <= x /\ x <= &1` ASSUME_TAC THENL
1338      [
1339        EXPAND_TAC "x" THEN
1340          CONJ_TAC THENL
1341          [
1342            MATCH_MP_TAC REAL_LE_DIV THEN
1343              ASM_REWRITE_TAC[] THEN
1344              MATCH_MP_TAC REAL_LE_ADD THEN ASM_REWRITE_TAC[];
1345            ALL_TAC
1346          ] THEN
1347          MATCH_MP_TAC Trigonometry2.REAL_LE_LDIV THEN
1348          CONJ_TAC THENL
1349          [
1350            MATCH_MP_TAC REAL_LET_ADD THEN
1351              ASM_REWRITE_TAC[REAL_LT_LE];
1352            ALL_TAC
1353          ] THEN
1354          ASM_REWRITE_TAC[REAL_ARITH `t1 <= b + t1 <=> &0 <= b`];
1355        ALL_TAC
1356      ] THEN
1357
1358      ASM_REWRITE_TAC[] THEN
1359      CONJ_TAC THENL
1360      [
1361        MATCH_MP_TAC REAL_LE_ADD THEN
1362          CONJ_TAC THEN MATCH_MP_TAC REAL_LE_MUL THEN ASM_REWRITE_TAC[REAL_ARITH `&0 <= &1 - x <=> x <= &1`];
1363        ALL_TAC
1364      ] THEN
1365
1366      REWRITE_TAC[REAL_ARITH `((&1 - x) * t2 + x * d) - (&1 - x) * t2 = x * d`] THEN
1367      SUBGOAL_THEN `--x * b = --((&1 - x) * t1)` (fun th -> REWRITE_TAC[th]) THEN
1368      SUBGOAL_THEN `&1 - x = b * x * inv t1` (fun th -> REWRITE_TAC[th]) THENL
1369      [
1370        EXPAND_TAC "x" THEN
1371          SUBGOAL_THEN `~(b + t1 = &0)` ASSUME_TAC THENL
1372          [
1373            MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~(a = &0)`) THEN
1374              MATCH_MP_TAC REAL_LET_ADD THEN
1375              ASM_REWRITE_TAC[REAL_LT_LE];
1376            ALL_TAC
1377          ] THEN
1378          MATCH_MP_TAC REAL_EQ_LCANCEL_IMP THEN
1379          EXISTS_TAC `b + t1:real` THEN
1380          FIRST_ASSUM (fun th -> REWRITE_TAC[th; real_div]) THEN
1381          REWRITE_TAC[REAL_ARITH `bt * (&1 - t1 * ibt) = bt - t1 * (bt * ibt)`] THEN
1382          REWRITE_TAC[REAL_ARITH `bt * b * (t * ibt) * it = (bt * ibt) * (t * it) * b`] THEN
1383          ASM_SIMP_TAC[REAL_MUL_RINV] THEN
1384          REAL_ARITH_TAC;
1385        ALL_TAC
1386      ] THEN
1387
1388      REWRITE_TAC[GSYM REAL_MUL_ASSOC] THEN
1389      ASM_SIMP_TAC[REAL_MUL_LINV] THEN
1390      REAL_ARITH_TAC);;
1391
1392
1393
1394 (* A special version of the rotation lemma for intersecting segments *)
1395 let rotation_lemma_segments = prove(`!v w u n:real^N. 3 <= dimindex (:N) /\
1396                                       ~(v = vec 0) /\ ~(u = vec 0) /\
1397                                       v dot n = &0 /\ w dot n = &0 /\ u dot n = &0 /\
1398                                       ~(segment [vec 0,u] INTER segment [v,w] = {})
1399                                       ==> ?f:real^1->real^N. f continuous_on UNIV /\
1400                                                              f (lift (&0)) = v /\
1401                                                              f (lift (&1)) = norm v / norm u % u /\
1402                                                              (!t. norm (f t) = norm v /\ f t dot n = &0) /\
1403                                                              (!t. &0 <= t /\ t <= &1 ==> dist (f (lift t), u) <= dist (v, u) /\
1404                                                                        dist (f (lift t), w) <= dist (v, w)) /\
1405                                                              (!t. &0 <= t /\ t <= &1 ==> ~(segment [f (lift t), w] INTER aff_ge {vec 0} {u} = {}))`,
1406    REPEAT STRIP_TAC THEN
1407      SUBGOAL_THEN `~collinear {vec 0, v, w:real^N} ==> ~(w = vec 0) /\ (!t. ~((&1 - t) % v + t % w = vec 0))` ASSUME_TAC THENL
1408      [
1409        REWRITE_TAC[COLLINEAR_LEMMA; DE_MORGAN_THM; NOT_EXISTS_THM] THEN STRIP_TAC THEN
1410          ASM_REWRITE_TAC[] THEN
1411          GEN_TAC THEN
1412          ASM_CASES_TAC `t = &0` THEN ASM_REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_RID; REAL_SUB_RZERO; VECTOR_MUL_LID] THEN
1413          DISCH_THEN (MP_TAC o AP_TERM `\x:real^N. inv t % x`) THEN
1414          REWRITE_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC] THEN
1415          ASM_SIMP_TAC[REAL_MUL_LINV; VECTOR_MUL_LID; VECTOR_MUL_RZERO] THEN
1416          ASM_REWRITE_TAC[VECTOR_ARITH `a % v + w = vec 0 <=> w = (--a) % v:real^N`];
1417        ALL_TAC
1418      ] THEN
1419
1420      SUBGOAL_THEN `~(segment [v,w] INTER aff_ge {vec 0} {u:real^N} = {})` ASSUME_TAC THENL
1421      [
1422        UNDISCH_TAC `~(segment [vec 0,u] INTER segment [v,w:real^N] = {})` THEN
1423          REWRITE_TAC[GSYM MEMBER_NOT_EMPTY; IN_INTER] THEN
1424          STRIP_TAC THEN
1425          EXISTS_TAC `x:real^N` THEN
1426          ASM_REWRITE_TAC[] THEN
1427          MATCH_MP_TAC Hypermap.lemma_in_subset THEN
1428          EXISTS_TAC `segment [vec 0,u:real^N]` THEN
1429          ASM_REWRITE_TAC[SEGMENT_SUBSET_HALFLINE];
1430        ALL_TAC
1431      ] THEN
1432
1433      SUBGOAL_THEN `?x c. &0 <= x /\ x <= &1 /\ &0 <= c /\ (&1 - x) % v + x % w = c % u:real^N` MP_TAC THENL
1434      [
1435        POP_ASSUM MP_TAC THEN
1436          REWRITE_TAC[GSYM MEMBER_NOT_EMPTY; IN_INTER; IN_SEGMENT; HALFLINE; IN_ELIM_THM] THEN
1437          REWRITE_TAC[VECTOR_MUL_RZERO; VECTOR_ADD_LID] THEN
1438          STRIP_TAC THEN
1439          MAP_EVERY EXISTS_TAC [`u':real`; `t:real`] THEN
1440          ASM_REWRITE_TAC[] THEN
1441          POP_ASSUM (fun th -> ASM_REWRITE_TAC[SYM th]);
1442        ALL_TAC
1443      ] THEN
1444      STRIP_TAC THEN
1445
1446      ASM_CASES_TAC `~collinear {vec 0, v, u:real^N}` THENL
1447      [
1448        MP_TAC (SPECL [`v:real^N`; `u:real^N`; `n:real^N`] rotation_lemma_special) THEN
1449          ASM_SIMP_TAC[] THEN
1450          STRIP_TAC THEN
1451          EXISTS_TAC `f:real^1->real^N` THEN
1452          ASM_REWRITE_TAC[] THEN
1453
1454          ASM_CASES_TAC `w = vec 0:real^N` THENL
1455          [
1456            ASM_REWRITE_TAC[DIST_0; REAL_LE_REFL] THEN
1457              REWRITE_TAC[GSYM MEMBER_NOT_EMPTY] THEN
1458              REPEAT STRIP_TAC THEN
1459              EXISTS_TAC `vec 0:real^N` THEN
1460              REWRITE_TAC[IN_INTER; ENDS_IN_SEGMENT; ENDS_IN_HALFLINE];
1461            ALL_TAC
1462          ] THEN
1463
1464          ASM_CASES_TAC `~collinear {vec 0, v, w:real^N}` THENL
1465          [
1466            FIRST_ASSUM (fun th -> FIRST_X_ASSUM (MP_TAC o MATCH_MP th)) THEN
1467              STRIP_TAC THEN
1468              CONJ_TAC THEN GEN_TAC THEN DISCH_TAC THENL
1469              [
1470                ASM_SIMP_TAC[] THEN
1471                  MATCH_MP_TAC rotation_dist_decrease_lemma THEN
1472                  ASM_REWRITE_TAC[] THEN
1473                  SUBGOAL_THEN `?a b. &0 <= a /\ &0 <= b /\ u = a % v + b % w:real^N` MP_TAC THENL
1474                  [
1475                    FIRST_X_ASSUM (MP_TAC o SPEC `x:real`) THEN
1476                      DISCH_TAC THEN
1477                      UNDISCH_TAC `(&1 - x) % v + x % w = c % u:real^N` THEN
1478                      ASM_CASES_TAC `c = &0` THENL [ ASM_REWRITE_TAC[VECTOR_MUL_LZERO]; ALL_TAC ] THEN
1479                      DISCH_THEN (MP_TAC o AP_TERM `\v:real^N. inv c % v`) THEN
1480                      ASM_SIMP_TAC[VECTOR_MUL_ASSOC; VECTOR_ADD_LDISTRIB; REAL_MUL_LINV; VECTOR_MUL_LID] THEN
1481                      DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN
1482                      MAP_EVERY EXISTS_TAC [`inv c * (&1 - x)`; `inv c * x`] THEN
1483                      REWRITE_TAC[] THEN
1484                      SUBGOAL_THEN `&0 <= inv c` ASSUME_TAC THENL [ MATCH_MP_TAC REAL_LE_INV THEN ASM_REWRITE_TAC[]; ALL_TAC ] THEN
1485                      CONJ_TAC THEN MATCH_MP_TAC REAL_LE_MUL THEN ASM_REWRITE_TAC[REAL_ARITH `&0 <= &1 - x <=> x <= &1`];
1486                    ALL_TAC
1487                  ] THEN
1488                  STRIP_TAC THEN
1489
1490                  ASM_SIMP_TAC[aff_ge_0_2; IN_ELIM_THM] THEN
1491                  REPLICATE_TAC 2 (FIRST_X_ASSUM (MP_TAC o SPEC `t:real`)) THEN
1492                  ASM_SIMP_TAC[aff_ge_0_2; IN_ELIM_THM] THEN
1493                  STRIP_TAC THEN DISCH_THEN (fun th -> ALL_TAC) THEN
1494                  MAP_EVERY EXISTS_TAC [`t1 + t2 * a:real`; `t2 * b:real`] THEN
1495                  CONJ_TAC THENL
1496                  [
1497                    MATCH_MP_TAC REAL_LE_ADD THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC REAL_LE_MUL THEN ASM_REWRITE_TAC[];
1498                    ALL_TAC
1499                  ] THEN
1500                  CONJ_TAC THENL [ MATCH_MP_TAC REAL_LE_MUL THEN ASM_REWRITE_TAC[]; ALL_TAC ] THEN
1501                  ASM_REWRITE_TAC[] THEN
1502                  VECTOR_ARITH_TAC;
1503                ALL_TAC
1504              ] THEN
1505
1506              MATCH_MP_TAC aff_ge_inter_segments THEN
1507              EXISTS_TAC `v:real^N` THEN
1508              ASM_SIMP_TAC[];
1509            ALL_TAC
1510          ] THEN
1511
1512          CONJ_TAC THEN GEN_TAC THEN DISCH_TAC THENL
1513          [
1514            ASM_SIMP_TAC[] THEN
1515              SUBGOAL_THEN `c = &0` ASSUME_TAC THENL
1516              [
1517                UNDISCH_TAC `~ ~collinear {vec 0, v, w:real^N}` THEN
1518                  ASM_REWRITE_TAC[COLLINEAR_LEMMA; DE_MORGAN_THM] THEN
1519                  STRIP_TAC THEN
1520                  UNDISCH_TAC `~collinear {vec 0, v, u:real^N}` THEN
1521                  ASM_REWRITE_TAC[COLLINEAR_LEMMA; DE_MORGAN_THM; NOT_EXISTS_THM] THEN
1522                  DISCH_TAC THEN
1523                  ASM_CASES_TAC `c = &0` THEN ASM_REWRITE_TAC[] THEN
1524                  UNDISCH_TAC `(&1 - x) % v + x % w = c % u:real^N` THEN
1525                  DISCH_THEN (MP_TAC o AP_TERM `\x:real^N. inv c % x`) THEN
1526                  ASM_SIMP_TAC[VECTOR_MUL_ASSOC; REAL_MUL_LINV; VECTOR_MUL_LID] THEN
1527                  ASM_REWRITE_TAC[VECTOR_ARITH `a % (b % v + c % v) = (a * b + a * c) % v`];
1528                ALL_TAC
1529              ] THEN
1530
1531              SUBGOAL_THEN `~(x = &0)` ASSUME_TAC THENL
1532              [
1533                ASM_CASES_TAC `x = &0` THEN ASM_REWRITE_TAC[] THEN
1534                  UNDISCH_TAC `(&1 - x) % v + x % w = c % u:real^N` THEN
1535                  ASM_REWRITE_TAC[REAL_SUB_RZERO; VECTOR_MUL_LID; VECTOR_MUL_LZERO; VECTOR_ADD_RID];
1536                ALL_TAC
1537              ] THEN
1538
1539              MATCH_MP_TAC rotation_dist_decrease_special_case THEN
1540              EXISTS_TAC `inv x * (&1 - x)` THEN
1541              ASM_SIMP_TAC[] THEN
1542              CONJ_TAC THENL
1543              [
1544                MATCH_MP_TAC REAL_LE_MUL THEN ASM_REWRITE_TAC[REAL_ARITH `&0 <= &1 - x <=> x <= &1`] THEN
1545                  MATCH_MP_TAC REAL_LE_INV THEN ASM_REWRITE_TAC[];
1546                ALL_TAC
1547              ] THEN
1548
1549              UNDISCH_TAC `(&1 - x) % v + x % w = c % u:real^N` THEN
1550              ASM_REWRITE_TAC[VECTOR_MUL_LZERO] THEN
1551              REWRITE_TAC[VECTOR_ARITH `a % v + x % w = vec 0:real^N <=> x % w = --a % v`] THEN
1552              DISCH_THEN (MP_TAC o AP_TERM `\v:real^N. inv x % v`) THEN
1553              ASM_SIMP_TAC[VECTOR_MUL_ASSOC; REAL_MUL_LINV; VECTOR_MUL_LID] THEN
1554              DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
1555              VECTOR_ARITH_TAC;
1556            ALL_TAC
1557          ] THEN
1558
1559          MATCH_MP_TAC aff_ge_inter_segments THEN
1560          EXISTS_TAC `v:real^N` THEN
1561          ASM_SIMP_TAC[];
1562        ALL_TAC
1563      ] THEN
1564
1565      POP_ASSUM MP_TAC THEN
1566      REWRITE_TAC[] THEN
1567      MP_TAC (ISPECL [`vec 0:real^N`; `u:real^N`; `v:real^N`] (GEN_ALL (CONJUNCT1 Collect_geom.PER_SET3))) THEN
1568      DISCH_THEN (fun th -> ONCE_REWRITE_TAC[th]) THEN
1569      ASM_REWRITE_TAC[COLLINEAR_LEMMA; DE_MORGAN_THM] THEN
1570      DISCH_THEN (X_CHOOSE_THEN `b:real` (LABEL_TAC "v" o SYM)) THEN
1571      ASM_CASES_TAC `&0 <= b` THENL
1572      [
1573        EXISTS_TAC `\t:real^1. v:real^N` THEN
1574          ASM_REWRITE_TAC[CONTINUOUS_ON_CONST; REAL_LE_REFL] THEN
1575          REMOVE_THEN "v" (fun th -> REWRITE_TAC[SYM th]) THEN
1576          REWRITE_TAC[NORM_MUL; real_div; GSYM REAL_MUL_ASSOC] THEN
1577          UNDISCH_TAC `~(u = vec 0:real^N)` THEN
1578          REWRITE_TAC[GSYM NORM_EQ_0] THEN
1579          SIMP_TAC[REAL_MUL_RINV; REAL_MUL_RID] THEN
1580          SUBGOAL_THEN `abs b = b` (fun th -> REWRITE_TAC[th]) THEN
1581          ASM_REWRITE_TAC[REAL_ABS_REFL];
1582        ALL_TAC
1583      ] THEN
1584
1585      POP_ASSUM MP_TAC THEN REWRITE_TAC[REAL_NOT_LE] THEN DISCH_TAC THEN
1586      MP_TAC (SPECL [`v:real^N`; `u:real^N`; `n:real^N`] rotation_lemma_special) THEN
1587      ASM_REWRITE_TAC[] THEN
1588      STRIP_TAC THEN
1589      EXISTS_TAC `f:real^1->real^N` THEN
1590      ASM_SIMP_TAC[] THEN
1591
1592      ASM_CASES_TAC `w = vec 0:real^N` THENL
1593      [
1594        ASM_REWRITE_TAC[DIST_0; REAL_LE_REFL] THEN
1595          REWRITE_TAC[GSYM MEMBER_NOT_EMPTY] THEN
1596          REPEAT STRIP_TAC THEN
1597          EXISTS_TAC `vec 0:real^N` THEN
1598          REWRITE_TAC[IN_INTER; ENDS_IN_SEGMENT; ENDS_IN_HALFLINE];
1599        ALL_TAC
1600      ] THEN
1601
1602      SUBGOAL_THEN `?d. &0 <= d /\ w = d % u:real^N` ASSUME_TAC THENL
1603      [
1604        SUBGOAL_THEN `~(x = &0)` ASSUME_TAC THENL
1605          [
1606            DISCH_TAC THEN
1607              UNDISCH_TAC `(&1 - x) % v + x % w = c % u:real^N` THEN
1608              ASM_REWRITE_TAC[REAL_SUB_RZERO; VECTOR_MUL_LID; VECTOR_MUL_LZERO; VECTOR_ADD_RID] THEN
1609              REMOVE_THEN "v" (fun th -> REWRITE_TAC[SYM th]) THEN
1610              ASM_REWRITE_TAC[VECTOR_ARITH `b % u = c % u <=> (c + --b) % u = vec 0:real^N`; VECTOR_MUL_EQ_0] THEN
1611              MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~(a = &0)`) THEN
1612              MATCH_MP_TAC REAL_LET_ADD THEN
1613              ASM_REWRITE_TAC[REAL_NEG_GT0];
1614            ALL_TAC
1615          ] THEN
1616
1617          UNDISCH_TAC `(&1 - x) % v + x % w = c % u:real^N` THEN
1618          DISCH_THEN (MP_TAC o AP_TERM `\v:real^N. inv x % v`) THEN
1619          ASM_SIMP_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC; REAL_MUL_LINV; VECTOR_MUL_LID] THEN
1620          REWRITE_TAC[VECTOR_ARITH `a + w = b <=> w = b - a:real^N`] THEN
1621          DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
1622          REMOVE_THEN "v" (fun th -> REWRITE_TAC[SYM th; VECTOR_MUL_ASSOC; GSYM VECTOR_SUB_RDISTRIB]) THEN
1623          ABBREV_TAC `d = inv x * c - ((inv x * (&1 - x)) * b)` THEN
1624
1625          EXISTS_TAC `d:real` THEN
1626          ASM_REWRITE_TAC[] THEN
1627          EXPAND_TAC "d" THEN
1628          REWRITE_TAC[GSYM REAL_MUL_ASSOC; GSYM REAL_SUB_LDISTRIB] THEN
1629          MATCH_MP_TAC REAL_LE_MUL THEN
1630          CONJ_TAC THENL [ MATCH_MP_TAC REAL_LE_INV THEN ASM_REWRITE_TAC[]; ALL_TAC ] THEN
1631          REWRITE_TAC[REAL_ARITH `c - a * b = c + a * (--b)`] THEN
1632          MATCH_MP_TAC REAL_LE_ADD THEN
1633          ASM_REWRITE_TAC[] THEN
1634          MATCH_MP_TAC REAL_LE_MUL THEN
1635          ASM_REWRITE_TAC[REAL_NEG_GE0; REAL_ARITH `&0 <= &1 - x <=> x <= &1`] THEN
1636          ASM_SIMP_TAC[REAL_LT_IMP_LE];
1637        ALL_TAC
1638      ] THEN
1639
1640      POP_ASSUM MP_TAC THEN STRIP_TAC THEN
1641      CONJ_TAC THEN GEN_TAC THEN DISCH_TAC THENL
1642      [
1643        MATCH_MP_TAC rotation_dist_decrease_special_case THEN
1644          EXISTS_TAC `--inv b * d` THEN
1645          ASM_SIMP_TAC[] THEN
1646          CONJ_TAC THENL
1647          [
1648            MATCH_MP_TAC REAL_LE_MUL THEN
1649              ASM_REWRITE_TAC[GSYM REAL_INV_NEG] THEN
1650              MATCH_MP_TAC REAL_LE_INV THEN
1651              ASM_SIMP_TAC[REAL_NEG_GE0; REAL_LT_IMP_LE];
1652            ALL_TAC
1653          ] THEN
1654
1655          REMOVE_THEN "v" (fun th -> REWRITE_TAC[SYM th]) THEN
1656          REWRITE_TAC[VECTOR_MUL_ASSOC; REAL_ARITH `--(--inv b * d) * b = d * b * inv b`] THEN
1657          ASM_SIMP_TAC[REAL_ARITH `b < &0 ==> ~(b = &0)`; REAL_MUL_RINV; REAL_MUL_RID];
1658        ALL_TAC
1659      ] THEN
1660
1661      REWRITE_TAC[GSYM MEMBER_NOT_EMPTY; IN_INTER; IN_SEGMENT; HALFLINE; IN_ELIM_THM] THEN
1662      EXISTS_TAC `w:real^N` THEN
1663      CONJ_TAC THENL
1664      [
1665        EXISTS_TAC `&1` THEN
1666          ASM_REWRITE_TAC[REAL_LE_01; REAL_LE_REFL; REAL_SUB_REFL; VECTOR_MUL_LZERO; VECTOR_ADD_LID; VECTOR_MUL_LID];
1667        ALL_TAC
1668      ] THEN
1669      EXISTS_TAC `d:real` THEN
1670      ASM_REWRITE_TAC[VECTOR_MUL_RZERO; VECTOR_ADD_LID]);;
1671
1672
1673
1674
1675 (* Rotation about an axis lemma *)
1676 let rotation_about_axis = prove(`!d v w:real^N. 3 <= dimindex (:N) /\ ~(d = vec 0) /\
1677                                   ~(projection d w = vec 0) /\
1678                                   ~(projection d v = vec 0)
1679                                   ==> ?(f:real^1->real^N) a b. &0 < a /\
1680                                         f continuous_on UNIV /\
1681                                         f(lift (&0)) = v /\
1682                                         f(lift (&1)) = a % w + b % d /\
1683                                         (!t c. dist (f t, c % d) = dist (v, c % d)) /\
1684                                         (!t. &0 <= t /\ t <= &1 ==> dist (f (lift t), w) <= dist (v, w))`,
1685    REPEAT STRIP_TAC THEN
1686      SUBGOAL_THEN `~(norm (projection d (v:real^N)) = &0) /\ ~(norm (projection d (w:real^N)) = &0)` ASSUME_TAC THENL
1687      [
1688        ASM_REWRITE_TAC[NORM_EQ_0];
1689        ALL_TAC
1690      ] THEN
1691      MP_TAC (SPECL [`projection d (v:real^N)`; `projection d (w:real^N)`; `d:real^N`] rotation_lemma_special) THEN
1692      ASM_REWRITE_TAC[PROJECTION_ORTHOGONAL] THEN
1693
1694      DISCH_THEN (X_CHOOSE_THEN `g:real^1->real^N` MP_TAC) THEN
1695      STRIP_TAC THEN
1696
1697      EXISTS_TAC `\t:real^1. g t + (v - projection d (v:real^N))` THEN
1698      EXISTS_TAC `norm (projection d (v:real^N)) / norm (projection d (w:real^N))` THEN
1699      ABBREV_TAC `a = norm (projection d (v:real^N)) / norm (projection d (w:real^N))` THEN
1700      EXISTS_TAC `(v dot (d:real^N)) / norm d pow 2 - a * (w dot d) / norm d pow 2` THEN
1701
1702      CONJ_TAC THENL
1703      [
1704        EXPAND_TAC "a" THEN
1705          MATCH_MP_TAC REAL_LT_DIV THEN
1706          ASM_REWRITE_TAC[NORM_POS_LT];
1707        ALL_TAC
1708      ] THEN
1709
1710      CONJ_TAC THENL
1711      [
1712        MATCH_MP_TAC CONTINUOUS_ON_ADD THEN
1713          ASM_REWRITE_TAC[CONTINUOUS_ON_CONST];
1714        ALL_TAC
1715      ] THEN
1716
1717      CONJ_TAC THENL
1718      [
1719        ASM_REWRITE_TAC[] THEN
1720          VECTOR_ARITH_TAC;
1721        ALL_TAC
1722      ] THEN
1723
1724      CONJ_TAC THENL
1725      [
1726        ASM_REWRITE_TAC[] THEN
1727          REWRITE_TAC[projection; VECTOR_SUB_LDISTRIB; NORM_POW_2; real_div; VECTOR_MUL_ASSOC; VECTOR_SUB_RDISTRIB] THEN
1728          VECTOR_ARITH_TAC;
1729        ALL_TAC
1730      ] THEN
1731
1732      CONJ_TAC THENL
1733      [
1734        REPEAT GEN_TAC THEN
1735          REWRITE_TAC[DIST_EQ] THEN
1736          ASM_SIMP_TAC[PROJECTION_DIST_SPECIAL_EQ; PROJECTION_LINEAR; PROJECTION_ZERO] THEN
1737          ASM_REWRITE_TAC[VECTOR_MUL_RZERO; DIST_0] THEN
1738          REAL_ARITH_TAC;
1739        ALL_TAC
1740      ] THEN
1741
1742      REPEAT STRIP_TAC THEN
1743      REWRITE_TAC[] THEN
1744      MATCH_MP_TAC PROJECTION_DIST_SPECIAL_LE THEN
1745      ASM_SIMP_TAC[]);;
1746
1747
1748
1749
1750
1751 (******************************************************)
1752
1753 (* The main lemma: continuous intersection of [f(t),w] and aff_ge {0} {v1,v2} *)
1754
1755 let continuous_solution_aux = prove(`!a11 a12 a21 a22 f g t1 t2.
1756                                       f real_continuous_on real_interval [t1,t2] /\
1757                                       g real_continuous_on real_interval [t1,t2] /\
1758                                       ~(a11 * a22 - a12 * a21 = &0)
1759                                       ==> ?x1 x2. x1 real_continuous_on real_interval [t1,t2] /\
1760                                                   x2 real_continuous_on real_interval [t1,t2] /\
1761                                                   (!t. a11 * x1 t + a12 * x2 t = f t /\
1762                                                        a21 * x1 t + a22 * x2 t = g t /\
1763                                                        (!y1 y2. a11 * y1 + a12 * y2 = f t /\
1764                                                                 a21 * y1 + a22 * y2 = g t ==> y1 = x1 t /\ y2 = x2 t))`,
1765    REPEAT STRIP_TAC THEN
1766      ABBREV_TAC `d = a11 * a22 - a12 * a21` THEN
1767      MAP_EVERY EXISTS_TAC [`\t. (a22 * (f:real->real) t - a12 * (g:real->real) t) * inv(d)`; `\t. (a11 * (g:real->real) t - a21 * (f:real->real) t) * inv d`] THEN
1768      REPEAT CONJ_TAC THENL
1769      [
1770        MATCH_MP_TAC REAL_CONTINUOUS_ON_RMUL THEN
1771          MATCH_MP_TAC REAL_CONTINUOUS_ON_SUB THEN
1772          CONJ_TAC THEN MATCH_MP_TAC REAL_CONTINUOUS_ON_LMUL THEN ASM_REWRITE_TAC[];
1773        MATCH_MP_TAC REAL_CONTINUOUS_ON_RMUL THEN
1774          MATCH_MP_TAC REAL_CONTINUOUS_ON_SUB THEN
1775          CONJ_TAC THEN MATCH_MP_TAC REAL_CONTINUOUS_ON_LMUL THEN ASM_REWRITE_TAC[];
1776        ALL_TAC
1777      ] THEN
1778      GEN_TAC THEN
1779      POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN
1780      BETA_TAC THEN
1781      CONV_TAC REAL_FIELD);;
1782
1783
1784
1785 let continuous_intersection_point = prove(`!v1 v2 n (f:real^1->real^3) w t1.
1786                                             ~collinear {vec 0,v1,v2} /\
1787                                             f continuous_on interval [lift (&0), lift (t1)] /\ &0 <= t1 /\
1788                                             v1 dot n = &0 /\ v2 dot n = &0 /\
1789                                             &0 < w dot n /\
1790                                             (!t. &0 <= t /\ t <= t1 ==> f (lift t) dot n <= &0)
1791                                             ==> (?a b. a real_continuous_on real_interval [&0, t1] /\
1792                                                        b real_continuous_on real_interval [&0, t1] /\
1793                                                        (!t. &0 <= t /\ t <= t1 ==> segment [f (lift t),w] INTER affine hull {vec 0,v1,v2} = {a t % v1 + b t % v2}))`,
1794    REPEAT STRIP_TAC THEN
1795      ABBREV_TAC `u0 = (\t. --((f o lift) t dot n:real^3) / (w dot n - ((f o lift) t dot n)))` THEN
1796      ABBREV_TAC `f1 = (\t. ((f o lift) t dot v1:real^3) + u0 t * (w - (f o lift) t) dot v1)` THEN
1797      ABBREV_TAC `f2 = (\t. ((f o lift) t dot v2:real^3) + u0 t * (w - (f o lift) t) dot v2)` THEN
1798      MP_TAC (SPECL [`v1 dot v1:real^3`; `v1 dot v2:real^3`; `v1 dot v2:real^3`; `v2 dot v2:real^3`; `f1:real->real`; `f2:real->real`; `&0`; `t1:real`] continuous_solution_aux) THEN
1799      ANTS_TAC THENL
1800      [
1801        SUBGOAL_THEN `!v:real^3. (\t. (f o lift) t dot v) real_continuous_on real_interval [&0,t1]` ASSUME_TAC THENL
1802          [
1803            GEN_TAC THEN REWRITE_TAC[REAL_CONTINUOUS_ON] THEN
1804              SUBGOAL_THEN `lift o (\t. (f o lift) t dot v:real^3) o drop = (lift o (\y. v dot y)) o f` (fun th -> REWRITE_TAC[th]) THENL
1805              [
1806                REWRITE_TAC[FUN_EQ_THM; o_THM; DOT_SYM; LIFT_DROP];
1807                ALL_TAC
1808              ] THEN
1809              MATCH_MP_TAC CONTINUOUS_ON_COMPOSE THEN
1810              ASM_REWRITE_TAC[IMAGE_LIFT_REAL_INTERVAL; CONTINUOUS_ON_LIFT_DOT];
1811            ALL_TAC
1812          ] THEN
1813
1814          SUBGOAL_THEN `u0 real_continuous_on real_interval[&0,t1]` ASSUME_TAC THENL
1815          [
1816            EXPAND_TAC "u0" THEN
1817              REWRITE_TAC[real_div] THEN
1818              MATCH_MP_TAC REAL_CONTINUOUS_ON_MUL THEN
1819              CONJ_TAC THENL [ MATCH_MP_TAC REAL_CONTINUOUS_ON_NEG THEN ASM_REWRITE_TAC[]; ALL_TAC ] THEN
1820              REWRITE_TAC[REAL_CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN] THEN
1821              REPEAT STRIP_TAC THEN
1822              MATCH_MP_TAC REAL_CONTINUOUS_INV_WITHINREAL THEN
1823              CONJ_TAC THENL
1824              [
1825                POP_ASSUM MP_TAC THEN SPEC_TAC (`x:real`, `x:real`) THEN
1826                  ONCE_REWRITE_TAC[GSYM REAL_CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN] THEN
1827                  MATCH_MP_TAC REAL_CONTINUOUS_ON_SUB THEN ASM_REWRITE_TAC[REAL_CONTINUOUS_ON_CONST];
1828                ALL_TAC
1829              ] THEN
1830              MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~(a = &0)`) THEN
1831              REWRITE_TAC[REAL_ARITH `a - b = a + (--b)`] THEN
1832              MATCH_MP_TAC REAL_LTE_ADD THEN
1833              ASM_REWRITE_TAC[] THEN
1834              FIRST_X_ASSUM (MP_TAC o SPEC `x:real`) THEN
1835              ASM_REWRITE_TAC[GSYM IN_REAL_INTERVAL; o_THM] THEN
1836              REAL_ARITH_TAC;
1837            ALL_TAC
1838          ] THEN
1839
1840          CONJ_TAC THENL
1841          [
1842            EXPAND_TAC "f1" THEN
1843              MATCH_MP_TAC REAL_CONTINUOUS_ON_ADD THEN
1844              ASM_REWRITE_TAC[] THEN
1845              MATCH_MP_TAC REAL_CONTINUOUS_ON_MUL THEN
1846              ASM_REWRITE_TAC[VECTOR_ARITH `(w - f) dot v = w dot v - f dot v:real^3`] THEN
1847              MATCH_MP_TAC REAL_CONTINUOUS_ON_SUB THEN
1848              ASM_REWRITE_TAC[REAL_CONTINUOUS_ON_CONST];
1849            ALL_TAC
1850          ] THEN
1851
1852          CONJ_TAC THENL
1853          [
1854            EXPAND_TAC "f2" THEN
1855              MATCH_MP_TAC REAL_CONTINUOUS_ON_ADD THEN
1856              ASM_REWRITE_TAC[] THEN
1857              MATCH_MP_TAC REAL_CONTINUOUS_ON_MUL THEN
1858              ASM_REWRITE_TAC[VECTOR_ARITH `(w - f) dot v = w dot v - f dot v:real^3`] THEN
1859              MATCH_MP_TAC REAL_CONTINUOUS_ON_SUB THEN
1860              ASM_REWRITE_TAC[REAL_CONTINUOUS_ON_CONST];
1861            ALL_TAC
1862          ] THEN
1863
1864          REWRITE_TAC[REAL_ARITH `v11 * v22 - v12 * v12 = &0 <=> v12 pow 2 = v11 * v22`] THEN
1865          ASM_REWRITE_TAC[DOT_CAUCHY_SCHWARZ_EQUAL];
1866        ALL_TAC
1867      ] THEN
1868
1869      STRIP_TAC THEN
1870      MAP_EVERY EXISTS_TAC [`x1:real->real`; `x2:real->real`] THEN
1871      ASM_REWRITE_TAC[] THEN
1872      GEN_TAC THEN DISCH_TAC THEN
1873
1874      REPEAT (FIRST_X_ASSUM (MP_TAC o SPEC `t:real`)) THEN
1875      ASM_REWRITE_TAC[] THEN REPEAT STRIP_TAC THEN
1876
1877      REWRITE_TAC [SET_RULE `!s (x:A). s = {x} <=> (?x. x IN s) /\ (!y. y IN s ==> y = x)`] THEN
1878      CONJ_TAC THENL
1879      [
1880        MATCH_MP_TAC intersection_point_exists THEN
1881          EXISTS_TAC `n:real^3` THEN ASM_REWRITE_TAC[] THEN
1882          ASM_SIMP_TAC[REAL_LT_IMP_LE] THEN
1883          DISCH_TAC THEN
1884          UNDISCH_TAC `&0 < w dot n:real^3` THEN
1885          ASM_REWRITE_TAC[DOT_RZERO; REAL_LT_REFL];
1886        ALL_TAC
1887      ] THEN
1888
1889      GEN_TAC THEN REWRITE_TAC[IN_INTER; IN_SEGMENT; AFFINE_HULL_3; IN_ELIM_THM; VECTOR_MUL_RZERO; VECTOR_ADD_LID] THEN
1890      STRIP_TAC THEN
1891      SUBGOAL_THEN `u:real = u0 (t:real)` ASSUME_TAC THENL
1892      [
1893        UNDISCH_TAC `y:real^3 = (&1 - u) % f (lift t) + u % w` THEN
1894          DISCH_THEN (MP_TAC o AP_TERM `(\y:real^3. y dot n)`) THEN
1895          FIRST_X_ASSUM (fun th -> REWRITE_TAC[th]) THEN
1896          ASM_REWRITE_TAC[DOT_LADD; DOT_LMUL; REAL_MUL_RZERO; REAL_ADD_RID] THEN
1897          EXPAND_TAC "u0" THEN
1898          REWRITE_TAC[o_THM] THEN
1899          SUBGOAL_THEN `&0 < w:real^3 dot n - f (lift t) dot n` MP_TAC THENL
1900          [
1901            REWRITE_TAC[REAL_ARITH `a - b = a + (--b)`] THEN
1902              MATCH_MP_TAC REAL_LTE_ADD THEN
1903              ASM_REWRITE_TAC[REAL_ARITH `&0 <= --a <=> a <= &0`];
1904            ALL_TAC
1905          ] THEN
1906          CONV_TAC REAL_FIELD;
1907        ALL_TAC
1908      ] THEN
1909
1910      SUBGOAL_THEN `v:real = x1 (t:real) /\ w':real = x2 t` ASSUME_TAC THENL
1911      [
1912        FIRST_X_ASSUM MATCH_MP_TAC THEN
1913          REWRITE_TAC[VECTOR_ARITH `(v1 dot v1) * v + (v1 dot v2:real^3) * w' = (v % v1 + w' % v2) dot v1`] THEN
1914          REWRITE_TAC[VECTOR_ARITH `(v1 dot v2) * v + (v2 dot v2:real^3) * w' = (v % v1 + w' % v2) dot v2`] THEN
1915          EXPAND_TAC "f1" THEN EXPAND_TAC "f2" THEN
1916          POP_ASSUM (fun th -> REWRITE_TAC[SYM th; o_THM]) THEN
1917          POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN
1918          ASM_REWRITE_TAC[] THEN
1919          VECTOR_ARITH_TAC;
1920        ALL_TAC
1921      ] THEN
1922      UNDISCH_TAC `y:real^3 = v % v1 + w' % v2` THEN
1923      DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
1924      ASM_REWRITE_TAC[]);;
1925
1926
1927
1928 let in_aff_ge_cases_lemma = prove(`!v1 v2 v w:real^N. ~collinear {vec 0,v1,v2} /\ ~(between (vec 0) (v,w)) /\
1929                                     v IN affine hull {vec 0,v1,v2} /\ w IN aff_ge {vec 0} {v1,v2}
1930                                       ==> v IN aff_ge {vec 0} {v1,v2} \/
1931                                           v1 IN aff_ge {vec 0} {v,w} \/
1932                                           v2 IN aff_ge {vec 0} {v,w}`,
1933    REPEAT STRIP_TAC THEN
1934      UNDISCH_TAC `~collinear {vec 0, v1, v2:real^N}` THEN DISCH_TAC THEN
1935      FIRST_ASSUM MP_TAC THEN REWRITE_TAC[COLLINEAR_LEMMA; DE_MORGAN_THM; NOT_EXISTS_THM] THEN DISCH_TAC THEN
1936      FIRST_X_ASSUM (MP_TAC o MATCH_MP zero_not_between) THEN
1937      STRIP_TAC THEN
1938
1939      ASM_CASES_TAC `v:real^N IN aff_ge {vec 0} {v1,v2}` THEN ASM_REWRITE_TAC[] THEN
1940      SUBGOAL_THEN `?t1 t2. v:real^N = t1 % v1 + t2 % v2 /\ (t1 < &0 \/ t2 < &0)` MP_TAC THENL
1941      [
1942        UNDISCH_TAC `v IN affine hull {vec 0, v1, v2:real^N}` THEN
1943          POP_ASSUM MP_TAC THEN
1944          REWRITE_TAC[AFFINE_HULL_3; IN_ELIM_THM; VECTOR_MUL_RZERO; VECTOR_ADD_LID] THEN
1945          ASM_SIMP_TAC[aff_ge_0_2; IN_ELIM_THM; NOT_EXISTS_THM] THEN
1946          DISCH_TAC THEN STRIP_TAC THEN
1947          MAP_EVERY EXISTS_TAC [`v':real`; `w':real`] THEN
1948          ASM_REWRITE_TAC[] THEN
1949          FIRST_X_ASSUM (MP_TAC o SPECL [`v':real`; `w':real`]) THEN
1950          REWRITE_TAC[DE_MORGAN_THM; REAL_NOT_LE] THEN
1951          ASM_REWRITE_TAC[];
1952        ALL_TAC
1953      ] THEN
1954      REPEAT (DISCH_THEN (CHOOSE_THEN MP_TAC)) THEN
1955      DISCH_THEN (CONJUNCTS_THEN2 (LABEL_TAC "v" o SYM) ASSUME_TAC) THEN
1956
1957      SUBGOAL_THEN `?t3 t4. w:real^N = t3 % v1 + t4 % v2 /\ &0 <= t3 /\ &0 <= t4` MP_TAC THENL
1958      [
1959        UNDISCH_TAC `w:real^N IN aff_ge {vec 0} {v1,v2}` THEN
1960          ASM_SIMP_TAC[aff_ge_0_2; IN_ELIM_THM] THEN
1961          STRIP_TAC THEN
1962          MAP_EVERY EXISTS_TAC [`t1':real`; `t2':real`] THEN
1963          ASM_REWRITE_TAC[];
1964        ALL_TAC
1965      ] THEN
1966      REPEAT (DISCH_THEN (CHOOSE_THEN MP_TAC)) THEN
1967      DISCH_THEN (CONJUNCTS_THEN2 (LABEL_TAC "w" o SYM) ASSUME_TAC) THEN
1968
1969      SUBGOAL_THEN `~(v = vec 0:real^N)` ASSUME_TAC THENL
1970      [
1971        ASM_CASES_TAC `v = vec 0:real^N` THEN ASM_REWRITE_TAC[] THEN
1972          UNDISCH_TAC `~(v IN aff_ge {vec 0} {v1,v2:real^N})` THEN
1973          ASM_REWRITE_TAC[points_in_aff_ge_0_2];
1974        ALL_TAC
1975      ] THEN
1976
1977      ASM_SIMP_TAC[aff_ge_0_2; IN_ELIM_THM] THEN
1978      ASM_CASES_TAC `t3 = &0` THENL
1979      [
1980        REMOVE_THEN "w" (MP_TAC o SYM) THEN
1981          ASM_REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_LID] THEN
1982          ASM_CASES_TAC `t4 = &0` THENL [ ASM_REWRITE_TAC[VECTOR_MUL_LZERO]; ALL_TAC ] THEN
1983          DISCH_THEN (MP_TAC o AP_TERM `\w:real^N. inv(t4) % w`) THEN
1984          ASM_SIMP_TAC[VECTOR_MUL_ASSOC; REAL_MUL_LINV; VECTOR_MUL_LID] THEN
1985          DISCH_TAC THEN
1986          DISJ2_TAC THEN
1987          MAP_EVERY EXISTS_TAC [`&0`; `inv t4`] THEN
1988          ASM_SIMP_TAC[REAL_LE_INV; REAL_LE_REFL; VECTOR_MUL_LZERO; VECTOR_ADD_LID];
1989        ALL_TAC
1990      ] THEN
1991      ASM_CASES_TAC `t4 = &0` THENL
1992      [
1993        REMOVE_THEN "w" (MP_TAC o SYM) THEN
1994          ASM_REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_RID] THEN
1995          DISCH_THEN (MP_TAC o AP_TERM `\w:real^N. inv(t3) % w`) THEN
1996          ASM_SIMP_TAC[VECTOR_MUL_ASSOC; REAL_MUL_LINV; VECTOR_MUL_LID] THEN
1997          DISCH_THEN (ASSUME_TAC o SYM) THEN
1998          DISJ1_TAC THEN
1999          MAP_EVERY EXISTS_TAC [`&0`; `inv t3`] THEN
2000          ASM_SIMP_TAC[REAL_LE_INV; REAL_LE_REFL; VECTOR_MUL_LZERO; VECTOR_ADD_LID];
2001        ALL_TAC
2002      ] THEN
2003
2004      SUBGOAL_THEN `&0 < t3 /\ &0 < t4` ASSUME_TAC THENL
2005      [
2006        ASM_REWRITE_TAC[REAL_ARITH `&0 < a <=> &0 <= a /\ ~(a = &0)`];
2007        ALL_TAC
2008      ] THEN
2009
2010      SUBGOAL_THEN `~(t2 * t3 - t1 * t4 = &0)` ASSUME_TAC THENL
2011      [
2012        REWRITE_TAC[REAL_ARITH `a - b = &0 <=> a = b`] THEN
2013          ASM_CASES_TAC `t1 < &0` THENL
2014          [
2015            DISCH_TAC THEN
2016              REMOVE_THEN "w" (MP_TAC o AP_TERM `(\x:real^N. t1 % x)`) THEN
2017              ASM_REWRITE_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC; REAL_MUL_AC] THEN
2018              POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN
2019              ONCE_REWRITE_TAC[REAL_MUL_AC] THEN
2020              ONCE_REWRITE_TAC[GSYM VECTOR_MUL_ASSOC] THEN
2021              ONCE_REWRITE_TAC[GSYM VECTOR_ADD_LDISTRIB] THEN
2022              ASM_SIMP_TAC[];
2023            ALL_TAC
2024          ] THEN
2025          SUBGOAL_THEN `t2 < &0` ASSUME_TAC THENL
2026          [
2027            UNDISCH_TAC `t1 < &0 \/ t2 < &0` THEN
2028              POP_ASSUM MP_TAC THEN
2029              SIMP_TAC[];
2030            ALL_TAC
2031          ] THEN
2032
2033          DISCH_TAC THEN
2034          REMOVE_THEN "w" (MP_TAC o AP_TERM `(\x:real^N. t2 % x)`) THEN
2035          ASM_REWRITE_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC; REAL_MUL_AC] THEN
2036          ONCE_REWRITE_TAC[REAL_MUL_AC] THEN
2037          ONCE_REWRITE_TAC[GSYM VECTOR_MUL_ASSOC] THEN
2038          ASM_REWRITE_TAC[GSYM VECTOR_ADD_LDISTRIB] THEN
2039          ASM_SIMP_TAC[];
2040        ALL_TAC
2041      ] THEN
2042
2043      ABBREV_TAC `d:real = t2 * t3 - t1 * t4` THEN
2044      SUBGOAL_THEN `v2:real^N = inv(d) % (t3 % v + (--t1) % w)` ASSUME_TAC THENL
2045      [
2046        MATCH_MP_TAC VECTOR_MUL_LCANCEL_IMP THEN
2047          EXISTS_TAC `d:real` THEN
2048          ASM_SIMP_TAC[VECTOR_MUL_ASSOC; REAL_MUL_RINV; VECTOR_MUL_LID] THEN
2049          REMOVE_THEN "w" (MP_TAC o AP_TERM `\w:real^N. (--t1) % w`) THEN
2050          REMOVE_THEN "v" (MP_TAC o AP_TERM `\v:real^N. t3 % v`) THEN
2051          BETA_TAC THEN EXPAND_TAC "d" THEN
2052          VECTOR_ARITH_TAC;
2053        ALL_TAC
2054      ] THEN
2055      SUBGOAL_THEN `v1:real^N = --inv(d) % (t4 % v + (--t2) % w)` ASSUME_TAC THENL
2056      [
2057        MATCH_MP_TAC VECTOR_MUL_LCANCEL_IMP THEN
2058          EXISTS_TAC `d:real` THEN
2059          ASM_SIMP_TAC[VECTOR_MUL_ASSOC; REAL_MUL_RNEG; REAL_MUL_RINV] THEN
2060          REMOVE_THEN "w" (MP_TAC o AP_TERM `\w:real^N. t2 % w`) THEN
2061          REMOVE_THEN "v" (MP_TAC o AP_TERM `\v:real^N. t4 % v`) THEN
2062          BETA_TAC THEN EXPAND_TAC "d" THEN
2063          VECTOR_ARITH_TAC;
2064        ALL_TAC
2065      ] THEN
2066
2067      ASM_CASES_TAC `t1 < &0` THENL
2068      [
2069        ASM_CASES_TAC `t2 < &0` THENL
2070          [
2071            ASM_CASES_TAC `d < &0` THENL
2072              [
2073                DISJ1_TAC THEN
2074                  MAP_EVERY EXISTS_TAC [`(--inv d) * t4`; `(--inv d) * (--t2)`] THEN
2075                  ASM_REWRITE_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC] THEN
2076                  REWRITE_TAC[GSYM REAL_INV_NEG] THEN
2077                  CONJ_TAC THEN MATCH_MP_TAC REAL_LE_MUL THENL
2078                  [
2079                    ASM_REWRITE_TAC[] THEN
2080                      MATCH_MP_TAC REAL_LE_INV THEN
2081                      ASM_SIMP_TAC[REAL_NEG_GE0; REAL_LT_IMP_LE];
2082                    ASM_SIMP_TAC[REAL_NEG_GE0; REAL_LT_IMP_LE] THEN
2083                      MATCH_MP_TAC REAL_LE_INV THEN
2084                      ASM_SIMP_TAC[REAL_NEG_GE0; REAL_LT_IMP_LE]
2085                  ];
2086                ALL_TAC
2087              ] THEN
2088              POP_ASSUM MP_TAC THEN REWRITE_TAC[REAL_NOT_LT] THEN DISCH_TAC THEN
2089              DISJ2_TAC THEN
2090              MAP_EVERY EXISTS_TAC [`inv d * t3`; `inv d * (--t1)`] THEN
2091              ASM_REWRITE_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC] THEN
2092              CONJ_TAC THEN MATCH_MP_TAC REAL_LE_MUL THEN ASM_SIMP_TAC[REAL_NEG_GE0; REAL_LT_IMP_LE] THEN MATCH_MP_TAC REAL_LE_INV THEN ASM_REWRITE_TAC[];
2093            ALL_TAC
2094          ] THEN
2095          POP_ASSUM MP_TAC THEN REWRITE_TAC[REAL_NOT_LT] THEN DISCH_TAC THEN
2096          SUBGOAL_THEN `&0 <= inv d` ASSUME_TAC THENL
2097          [
2098            EXPAND_TAC "d" THEN
2099              MATCH_MP_TAC REAL_LE_INV THEN
2100              REWRITE_TAC[REAL_ARITH `a - t1 * t4 = a + (--t1) * t4`] THEN
2101              MATCH_MP_TAC REAL_LE_ADD THEN
2102              CONJ_TAC THEN MATCH_MP_TAC REAL_LE_MUL THEN ASM_SIMP_TAC[REAL_NEG_GE0; REAL_LT_IMP_LE];
2103            ALL_TAC
2104          ] THEN
2105
2106          DISJ2_TAC THEN
2107          MAP_EVERY EXISTS_TAC [`inv d * t3`; `inv d * (--t1)`] THEN
2108          ASM_REWRITE_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC] THEN
2109          CONJ_TAC THEN MATCH_MP_TAC REAL_LE_MUL THEN ASM_SIMP_TAC[REAL_NEG_GE0; REAL_LT_IMP_LE];
2110        ALL_TAC
2111      ] THEN
2112
2113      SUBGOAL_THEN `&0 <= t1 /\ t2 < &0` ASSUME_TAC THENL
2114      [
2115        UNDISCH_TAC `t1 < &0 \/ t2 < &0` THEN
2116          ASM_REWRITE_TAC[GSYM REAL_NOT_LT];
2117        ALL_TAC
2118      ] THEN
2119
2120      SUBGOAL_THEN `&0 <= --inv d` ASSUME_TAC THENL
2121      [
2122        REWRITE_TAC[GSYM REAL_INV_NEG] THEN
2123          EXPAND_TAC "d" THEN
2124          MATCH_MP_TAC REAL_LE_INV THEN
2125          REWRITE_TAC[REAL_ARITH `--(t2 * t3 - t1 * t4) = (--t2) * t3 + t1 * t4`] THEN
2126          MATCH_MP_TAC REAL_LE_ADD THEN
2127          CONJ_TAC THEN MATCH_MP_TAC REAL_LE_MUL THEN ASM_SIMP_TAC[REAL_NEG_GE0; REAL_LT_IMP_LE];
2128        ALL_TAC
2129      ] THEN
2130
2131      DISJ1_TAC THEN
2132      MAP_EVERY EXISTS_TAC [`--inv d * t4`; `--inv d * (--t2)`] THEN
2133      ASM_REWRITE_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC] THEN
2134      CONJ_TAC THEN MATCH_MP_TAC REAL_LE_MUL THEN ASM_SIMP_TAC[REAL_NEG_GE0; REAL_LT_IMP_LE]);;
2135
2136
2137
2138 let segment_intersects_aff_ge_lemma = prove(`!v1 v2 v w:real^N. ~collinear {vec 0,v1,v2} /\ ~between (vec 0) (v,w) /\
2139                                               v IN affine hull {vec 0,v1,v2} /\ w IN affine hull {vec 0,v1,v2} /\
2140                                               ~(segment [v,w] INTER aff_ge {vec 0} {v1,v2} = {})
2141                                               ==> v IN aff_ge {vec 0} {v1,v2} \/
2142                                                   v1 IN aff_ge {vec 0} {v,w} \/
2143                                                   v2 IN aff_ge {vec 0} {v,w}`,
2144    REPEAT STRIP_TAC THEN
2145      POP_ASSUM MP_TAC THEN REWRITE_TAC[GSYM MEMBER_NOT_EMPTY] THEN
2146      DISCH_THEN (X_CHOOSE_THEN `p:real^N` MP_TAC) THEN
2147      REWRITE_TAC[IN_INTER] THEN DISCH_THEN (CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN DISCH_TAC THEN
2148      FIRST_ASSUM MP_TAC THEN REWRITE_TAC[IN_SEGMENT] THEN STRIP_TAC THEN
2149      POP_ASSUM MP_TAC THEN
2150      ASM_CASES_TAC `u = &0` THENL
2151      [
2152        ASM_REWRITE_TAC[REAL_SUB_RZERO; VECTOR_MUL_LZERO; VECTOR_MUL_LID; VECTOR_ADD_RID] THEN
2153          DISCH_THEN (fun th -> ASM_REWRITE_TAC[SYM th]);
2154        ALL_TAC
2155      ] THEN
2156      DISCH_THEN (LABEL_TAC "p" o SYM) THEN
2157
2158      FIRST_ASSUM (MP_TAC o MATCH_MP zero_not_between) THEN
2159      STRIP_TAC THEN
2160
2161      MP_TAC (SPECL [`v1:real^N`; `v2:real^N`; `v:real^N`; `p:real^N`] in_aff_ge_cases_lemma) THEN
2162      ASM_REWRITE_TAC[] THEN
2163
2164      ANTS_TAC THENL
2165      [
2166        REWRITE_TAC[BETWEEN_IN_SEGMENT] THEN DISCH_TAC THEN
2167          UNDISCH_TAC `~between (vec 0:real^N) (v,w)` THEN
2168          REWRITE_TAC[BETWEEN_IN_SEGMENT] THEN
2169          MATCH_MP_TAC Hypermap.lemma_in_subset THEN
2170          EXISTS_TAC `segment [v,p:real^N]` THEN
2171          ASM_REWRITE_TAC[SUBSET_SEGMENT; ENDS_IN_SEGMENT];
2172        ALL_TAC
2173      ] THEN
2174
2175      SUBGOAL_THEN `p IN aff_ge {vec 0:real^N} {v,w}` ASSUME_TAC THENL
2176      [
2177        MATCH_MP_TAC in_segment_imp_in_aff_ge_0_2 THEN
2178          ASM_REWRITE_TAC[];
2179        ALL_TAC
2180      ] THEN
2181
2182      STRIP_TAC THEN ASM_REWRITE_TAC[] THENL
2183      [
2184        DISJ2_TAC THEN DISJ1_TAC THEN
2185          MATCH_MP_TAC Hypermap.lemma_in_subset THEN
2186          EXISTS_TAC `aff_ge {vec 0} {v:real^N,p}` THEN
2187          ASM_REWRITE_TAC[] THEN
2188          MATCH_MP_TAC aff_ge_0_2_SUBSET THEN
2189          ASM_REWRITE_TAC[points_in_aff_ge_0_2];
2190        ALL_TAC
2191      ] THEN
2192      DISJ2_TAC THEN DISJ2_TAC THEN
2193      MATCH_MP_TAC Hypermap.lemma_in_subset THEN
2194      EXISTS_TAC `aff_ge {vec 0} {v:real^N,p}` THEN
2195      ASM_REWRITE_TAC[] THEN
2196      MATCH_MP_TAC aff_ge_0_2_SUBSET THEN
2197      ASM_REWRITE_TAC[points_in_aff_ge_0_2]);;
2198
2199
2200
2201
2202 (* The main lemma *)
2203
2204 let continuous_lemma_aff_ge = prove(`!v1 v2 (f:real^1->real^3) w h. &0 <= h /\
2205                                       f continuous_on interval [lift (&0), lift h] /\
2206                                       ~(segment [f (lift (&0)), w] INTER aff_ge {vec 0} {v1,v2} = {}) /\
2207                                       (!t. t IN interval [lift (&0), lift h] ==> ~between (vec 0) (f t, w)) /\
2208                                       ~collinear {vec 0,v1,v2}
2209                                       ==> (!t. t IN interval [lift (&0), lift h] ==> ~(segment [f t, w] INTER aff_ge {vec 0} {v1,v2} = {})) \/
2210                                           (?x. &0 <= x /\ x <= h /\
2211                                              (!t. t IN interval [lift (&0), lift x] ==> ~(segment [f t, w] INTER aff_ge {vec 0} {v1,v2} = {})) /\
2212                                              (f (lift x) IN aff_ge {vec 0} {v1,v2} \/ v1 IN aff_ge {vec 0} {f (lift x), w} \/ v2 IN aff_ge {vec 0} {f (lift x), w}))`,
2213    REPEAT STRIP_TAC THEN
2214      SUBGOAL_THEN `!y b. (lift y) IN interval [lift (&0), lift b] <=> &0 <= y /\ y <= b` ASSUME_TAC THENL
2215      [
2216        ASM_REWRITE_TAC[IN_INTERVAL_1];
2217        ALL_TAC
2218      ] THEN
2219
2220      (* Aux *)
2221      SUBGOAL_THEN `lift (&0) IN interval [lift (&0), lift h]` ASSUME_TAC THENL
2222      [
2223        ASM_REWRITE_TAC[IN_INTERVAL_1; REAL_LE_REFL];
2224        ALL_TAC
2225      ] THEN
2226
2227      (* v1, v2, w != 0 *)
2228      SUBGOAL_THEN `~(v1:real^3 = vec 0) /\ ~(v2:real^3 = vec 0) /\ ~(w:real^3 = vec 0)` ASSUME_TAC THENL
2229      [
2230        UNDISCH_TAC `~collinear {vec 0,v1,v2:real^3}` THEN
2231          SIMP_TAC[COLLINEAR_LEMMA; DE_MORGAN_THM] THEN DISCH_TAC THEN
2232          FIRST_X_ASSUM (MP_TAC o SPEC `lift (&0)`) THEN
2233          ASM_REWRITE_TAC[] THEN
2234          DISCH_THEN (MP_TAC o MATCH_MP zero_not_between) THEN
2235          SIMP_TAC[];
2236        ALL_TAC
2237      ] THEN
2238
2239      (* ~between (vec 0) (f(t), w) expanded *)
2240      SUBGOAL_THEN `!t. &0 <= t /\ t <= h ==> ~(f (lift t) = vec 0) /\ (!u. &0 <= u /\ u <= &1 ==> ~((&1 - u) % f (lift t) + u % w = vec 0:real^3))` (LABEL_TAC "fw") THENL
2241      [
2242        GEN_TAC THEN DISCH_TAC THEN
2243          FIRST_X_ASSUM (MP_TAC o SPEC `lift t`) THEN
2244          ASM_REWRITE_TAC[IN_INTERVAL_1] THEN
2245          DISCH_THEN (MP_TAC o MATCH_MP zero_not_between) THEN
2246          STRIP_TAC THEN
2247          ASM_REWRITE_TAC[] THEN
2248
2249          GEN_TAC THEN DISCH_TAC THEN
2250          ASM_CASES_TAC `u = &0` THENL
2251          [
2252            ASM_REWRITE_TAC[REAL_SUB_RZERO; VECTOR_MUL_LID; VECTOR_MUL_LZERO; VECTOR_ADD_RID];
2253            ALL_TAC
2254          ] THEN
2255          ASM_CASES_TAC `u = &1` THENL
2256          [
2257            ASM_REWRITE_TAC[REAL_SUB_REFL; VECTOR_MUL_LZERO; VECTOR_ADD_LID; VECTOR_MUL_LID];
2258            ALL_TAC
2259          ] THEN
2260          FIRST_X_ASSUM (MP_TAC o SPECL [`--u:real`; `&1 - u`]) THEN
2261          ANTS_TAC THENL
2262          [
2263            REPLICATE_TAC 3 (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC;
2264            ALL_TAC
2265          ] THEN
2266          REWRITE_TAC[VECTOR_ARITH `--u % (w:real^N) = (&1 - u) % x <=> (&1 - u) % x + u % w = vec 0`];
2267        ALL_TAC
2268      ] THEN
2269
2270      (* First case *)
2271      ASM_CASES_TAC `!t. t IN interval [lift (&0),lift h] ==> ~(segment [f t,w] INTER aff_ge {vec 0} {v1,v2:real^3} = {})` THEN ASM_REWRITE_TAC[] THEN
2272      POP_ASSUM MP_TAC THEN REWRITE_TAC[NOT_FORALL_THM] THEN
2273      REWRITE_TAC[TAUT `~(A ==> ~B) <=> A /\ B`] THEN
2274      DISCH_THEN (X_CHOOSE_THEN `t1:real^1` (LABEL_TAC "A")) THEN
2275
2276      (* Find a normal vector to the plane of aff_ge {vec 0} {v1,v2} *)
2277      SUBGOAL_THEN `?n:real^3. ~(n = vec 0) /\ v1 dot n = &0 /\ v2 dot n = &0 /\ f (lift (&0)) dot n <= &0` MP_TAC THENL
2278      [
2279        ASM_CASES_TAC `f (lift (&0)) dot (v1:real^3 cross v2) <= &0` THENL
2280          [
2281            EXISTS_TAC `v1 cross v2` THEN
2282              ASM_REWRITE_TAC[CROSS_EQ_0; DOT_CROSS_SELF];
2283            ALL_TAC
2284          ] THEN
2285          EXISTS_TAC `--(v1 cross v2)` THEN
2286          ASM_REWRITE_TAC[VECTOR_NEG_EQ_0; CROSS_EQ_0; DOT_RNEG; DOT_CROSS_SELF] THEN
2287          POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;
2288        ALL_TAC
2289      ] THEN
2290      STRIP_TAC THEN
2291
2292      (* Aux *)
2293      SUBGOAL_THEN `!p. p IN aff_ge {vec 0} {v1,v2:real^3} ==> p dot n = &0` ASSUME_TAC THENL
2294      [
2295        GEN_TAC THEN ASM_SIMP_TAC[aff_ge_0_2; IN_ELIM_THM] THEN
2296          STRIP_TAC THEN ASM_REWRITE_TAC[DOT_LADD; DOT_LMUL; REAL_MUL_RZERO; REAL_ADD_LID];
2297        ALL_TAC
2298      ] THEN
2299
2300      (* Need for the next two cases *)
2301      UNDISCH_TAC `~(segment [f (lift (&0)), w] INTER aff_ge {vec 0:real^3} {v1,v2} = {})` THEN DISCH_TAC THEN
2302      FIRST_ASSUM MP_TAC THEN REWRITE_TAC[GSYM MEMBER_NOT_EMPTY] THEN
2303      DISCH_THEN (X_CHOOSE_THEN `p:real^3` (LABEL_TAC "B")) THEN
2304      FIRST_ASSUM (MP_TAC o REWRITE_RULE [IN_INTER; IN_SEGMENT]) THEN
2305      DISCH_THEN (CONJUNCTS_THEN2 (X_CHOOSE_THEN `up:real` MP_TAC) ASSUME_TAC) THEN
2306      GEN_REWRITE_TAC LAND_CONV [CONJ_ASSOC] THEN
2307      DISCH_THEN (CONJUNCTS_THEN2 ASSUME_TAC (LABEL_TAC "p1" o SYM)) THEN
2308      FIRST_ASSUM (MP_TAC o SPEC `p:real^3`) THEN
2309      FIRST_ASSUM (fun th -> CHANGED_TAC (REWRITE_TAC[th])) THEN DISCH_TAC THEN
2310
2311      (* w dot n < 0 *)
2312      DISJ_CASES_TAC (REAL_ARITH `w:real^3 dot n < &0 \/ w dot n = &0 \/ &0 < w dot n`) THENL
2313      [
2314        SUBGOAL_THEN `up = &0` ASSUME_TAC THENL
2315          [
2316            REMOVE_THEN "p1" (MP_TAC o AP_TERM `\v:real^3. v dot n`) THEN
2317              ASM_REWRITE_TAC[DOT_LADD; DOT_LMUL; REAL_MUL_RZERO; REAL_ADD_LID] THEN
2318              ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN
2319              DISCH_TAC THEN
2320              MATCH_MP_TAC (REAL_ARITH `&0 < --a ==> ~(a = &0)`) THEN
2321              REWRITE_TAC[REAL_ARITH `--(a * b + c * d) = a * (--b) + c * (--d)`] THEN
2322              MATCH_MP_TAC REAL_LET_ADD THEN
2323              CONJ_TAC THENL
2324              [
2325                MATCH_MP_TAC REAL_LE_MUL THEN
2326                  ASM_REWRITE_TAC[REAL_ARITH `&0 <= &1 - up <=> up <= &1`; REAL_NEG_GE0];
2327                ALL_TAC
2328              ] THEN
2329              MATCH_MP_TAC REAL_LT_MUL THEN
2330              ASM_REWRITE_TAC[REAL_ARITH `&0 < up <=> &0 <= up /\ ~(up = &0)`; REAL_NEG_GT0];
2331            ALL_TAC
2332          ] THEN
2333
2334          REMOVE_THEN "p1" MP_TAC THEN
2335          ASM_REWRITE_TAC[REAL_SUB_RZERO; VECTOR_MUL_LZERO; VECTOR_ADD_RID; VECTOR_MUL_LID] THEN
2336          DISCH_TAC THEN
2337          EXISTS_TAC `&0` THEN
2338          ASM_REWRITE_TAC[REAL_LE_REFL; REAL_LE_01; INTERVAL_SING; IN_SING] THEN
2339          GEN_TAC THEN
2340          DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
2341          EXISTS_TAC `p:real^3` THEN ASM_REWRITE_TAC[];
2342        ALL_TAC
2343      ] THEN
2344
2345      (* w dot n = 0 *)
2346      FIRST_X_ASSUM DISJ_CASES_TAC THENL
2347      [
2348        ASM_CASES_TAC `w:real^3 IN aff_ge {vec 0} {v1,v2}` THENL
2349          [
2350            SUBGOAL_THEN `~(segment [f (t1:real^1),w] INTER aff_ge {vec 0} {v1,v2:real^3} = {})` MP_TAC THENL
2351              [
2352                REWRITE_TAC[GSYM MEMBER_NOT_EMPTY] THEN
2353                  EXISTS_TAC `w:real^3` THEN
2354                  REWRITE_TAC[IN_INTER; ENDS_IN_SEGMENT] THEN POP_ASSUM (fun th -> REWRITE_TAC[th]);
2355                ALL_TAC
2356              ] THEN
2357              ASM_REWRITE_TAC[];
2358            ALL_TAC
2359          ] THEN
2360
2361          EXISTS_TAC `&0` THEN
2362          ASM_REWRITE_TAC[REAL_LE_REFL; INTERVAL_SING; IN_SING] THEN
2363          CONJ_TAC THENL
2364          [
2365            GEN_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN
2366              EXISTS_TAC `p:real^3` THEN ASM_REWRITE_TAC[];
2367            ALL_TAC
2368          ] THEN
2369
2370          MATCH_MP_TAC segment_intersects_aff_ge_lemma THEN
2371          ASM_REWRITE_TAC[] THEN
2372          FIRST_X_ASSUM (MP_TAC o SPEC `lift (&0)`) THEN
2373          ASM_REWRITE_TAC[] THEN
2374          DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
2375
2376          ASM_SIMP_TAC[affine_hull_3_plane] THEN
2377          ASM_REWRITE_TAC[IN_ELIM_THM] THEN
2378          SUBGOAL_THEN `~(up = &1)` ASSUME_TAC THENL
2379          [
2380            POP_ASSUM MP_TAC THEN REWRITE_TAC[CONTRAPOS_THM] THEN DISCH_TAC THEN
2381              REMOVE_THEN "p1" MP_TAC THEN ASM_REWRITE_TAC[REAL_SUB_REFL; VECTOR_MUL_LID; VECTOR_MUL_LZERO; VECTOR_ADD_LID] THEN
2382              ASM_SIMP_TAC[];
2383            ALL_TAC
2384          ] THEN
2385
2386          REMOVE_THEN "p1" (MP_TAC o AP_TERM `\v:real^3. v dot n`) THEN
2387          ASM_REWRITE_TAC[DOT_LADD; DOT_LMUL; REAL_MUL_RZERO] THEN
2388          POP_ASSUM MP_TAC THEN CONV_TAC REAL_FIELD;
2389        ALL_TAC
2390      ] THEN
2391
2392      (* Remove unnessary assumptions before considering the last case *)
2393      POP_ASSUM MP_TAC THEN REPLICATE_TAC 5 REMOVE_ASSUM THEN DISCH_TAC THEN
2394
2395      (* w dot n > 0 *)
2396
2397      (* Consider two major cases: f(t) intersects affine hull {vec 0,v1,v2} at some point or not *)
2398      SUBGOAL_THEN `?r. &0 <= r /\ r <= h /\
2399                        (!t. &0 <= t /\ t <= r ==> f (lift t) dot (n:real^3) <= &0) /\
2400                        (((!t. &0 <= t /\ t <= r ==> ~(segment [f (lift t), w] INTER aff_ge {vec 0} {v1,v2} = {})) /\ f (lift r) IN aff_ge {vec 0} {v1, v2}) \/
2401                           (?t1. &0 <= t1 /\ t1 <= r /\ segment [f (lift t1), w] INTER aff_ge {vec 0} {v1,v2} = {}))` MP_TAC THENL
2402      [
2403        ASM_CASES_TAC `!t. &0 <= t /\ t <= h ==> f (lift t) dot (n:real^3) <= &0` THENL
2404          [
2405            EXISTS_TAC `h:real` THEN
2406              ASM_REWRITE_TAC[REAL_LE_REFL] THEN
2407              DISJ2_TAC THEN
2408              EXISTS_TAC `drop (t1:real^1)` THEN
2409              ASM_REWRITE_TAC[LIFT_DROP] THEN
2410              FIRST_X_ASSUM (MP_TAC o SPECL [`drop (t1:real^1)`; `h:real`]) THEN
2411              ASM_REWRITE_TAC[LIFT_DROP];
2412            ALL_TAC
2413          ] THEN
2414
2415          POP_ASSUM MP_TAC THEN REWRITE_TAC[NOT_FORALL_THM] THEN
2416          DISCH_THEN (X_CHOOSE_THEN `tt:real` MP_TAC) THEN
2417          REWRITE_TAC[TAUT `~(A ==> B) <=> A /\ ~B`; REAL_NOT_LE] THEN
2418          DISCH_TAC THEN
2419          MP_TAC (SPECL [`\t:real. f (lift t) dot n:real^3`; `&0`; `tt:real`] continuous_lemma_inc) THEN
2420          ANTS_TAC THENL
2421          [
2422            ASM_SIMP_TAC[REAL_LT_IMP_LE] THEN
2423              REWRITE_TAC[REAL_CONTINUOUS_ON] THEN
2424              SUBGOAL_THEN `lift o (\t:real. f (lift t) dot n:real^3) o drop = (lift o (\y:real^3. n dot y)) o f` (fun th -> REWRITE_TAC[th]) THENL
2425              [
2426                REWRITE_TAC[FUN_EQ_THM; o_THM; LIFT_DROP; DOT_SYM];
2427                ALL_TAC
2428              ] THEN
2429              MATCH_MP_TAC CONTINUOUS_ON_COMPOSE THEN
2430              REWRITE_TAC[IMAGE_LIFT_REAL_INTERVAL; CONTINUOUS_ON_LIFT_DOT] THEN
2431              MATCH_MP_TAC CONTINUOUS_ON_SUBSET THEN
2432              EXISTS_TAC `interval [lift (&0), lift (h)]` THEN
2433              ASM_REWRITE_TAC[SUBSET_INTERVAL_1; LIFT_DROP; REAL_LE_REFL];
2434            ALL_TAC
2435          ] THEN
2436          BETA_TAC THEN STRIP_TAC THEN
2437          EXISTS_TAC `x:real` THEN
2438          ASM_REWRITE_TAC[] THEN
2439          CONJ_TAC THENL
2440          [
2441            MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `tt:real` THEN ASM_REWRITE_TAC[];
2442            ALL_TAC
2443          ] THEN
2444          CONJ_TAC THENL
2445          [
2446            REPEAT STRIP_TAC THEN
2447              ASM_CASES_TAC `t = x:real` THENL [ ASM_SIMP_TAC[REAL_ARITH `a = &0 ==> a <= &0`]; ALL_TAC ] THEN
2448              MATCH_MP_TAC REAL_LT_IMP_LE THEN
2449              FIRST_X_ASSUM MATCH_MP_TAC THEN
2450              ASM_REWRITE_TAC[REAL_LT_LE];
2451            ALL_TAC
2452          ] THEN
2453
2454          ASM_CASES_TAC `?t1. &0 <= t1 /\ t1 <= x /\ segment [f (lift t1),w:real^3] INTER aff_ge {vec 0} {v1,v2} = {}` THEN ASM_REWRITE_TAC[] THEN
2455          POP_ASSUM MP_TAC THEN REWRITE_TAC[NOT_EXISTS_THM; DE_MORGAN_THM] THEN
2456          DISCH_TAC THEN
2457          SUBGOAL_THEN `!t. &0 <= t /\ t <= x ==> ~(segment [f (lift t),w:real^3] INTER aff_ge {vec 0} {v1,v2} = {})` ASSUME_TAC THENL
2458          [
2459            REPEAT STRIP_TAC THEN
2460              FIRST_X_ASSUM (MP_TAC o SPEC `t:real`) THEN
2461              ASM_REWRITE_TAC[DE_MORGAN_THM];
2462            ALL_TAC
2463          ] THEN
2464
2465          ASM_REWRITE_TAC[] THEN
2466          FIRST_X_ASSUM (MP_TAC o SPEC `x:real`) THEN
2467          ASM_REWRITE_TAC[REAL_LE_REFL; GSYM MEMBER_NOT_EMPTY] THEN
2468          DISCH_THEN (X_CHOOSE_THEN `p:real^3` MP_TAC) THEN
2469          REWRITE_TAC[IN_INTER; IN_SEGMENT] THEN
2470          STRIP_TAC THEN
2471          UNDISCH_TAC `p = (&1 - u) % f (lift x) + u % w:real^3` THEN DISCH_THEN (LABEL_TAC "p1" o SYM) THEN
2472          FIRST_ASSUM (MP_TAC o AP_TERM `\v:real^3. v dot n`) THEN
2473          FIRST_X_ASSUM (MP_TAC o SPEC `p:real^3`) THEN
2474          ASM_REWRITE_TAC[DOT_LADD; DOT_LMUL; REAL_MUL_RZERO; REAL_ADD_LID] THEN
2475          DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
2476          REWRITE_TAC[REAL_ENTIRE] THEN
2477          ASM_SIMP_TAC[REAL_ARITH `&0 < w dot n ==> ~(w:real^3 dot n = &0)`] THEN
2478          DISCH_TAC THEN
2479          REMOVE_THEN "p1" MP_TAC THEN
2480          ASM_SIMP_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_RID; REAL_SUB_RZERO; VECTOR_MUL_LID];
2481        ALL_TAC
2482      ] THEN
2483
2484
2485      (* Deal with two possible cases *)
2486      STRIP_TAC THENL
2487      [
2488        EXISTS_TAC `r:real` THEN
2489          ASM_REWRITE_TAC[] THEN
2490          REPEAT STRIP_TAC THEN
2491          FIRST_X_ASSUM (MP_TAC o SPEC `drop (t:real^1)`) THEN
2492          FIRST_X_ASSUM (MP_TAC o SPECL [`drop (t:real^1)`; `r:real`]) THEN
2493          DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN
2494          ASM_REWRITE_TAC[LIFT_DROP; MEMBER_NOT_EMPTY];
2495        ALL_TAC
2496      ] THEN
2497
2498      (* The main case *)
2499      MP_TAC (SPECL [`v1:real^3`; `v2:real^3`; `n:real^3`; `f:real^1->real^3`; `w:real^3`; `r:real`] continuous_intersection_point) THEN
2500      ASM_REWRITE_TAC[] THEN
2501      ANTS_TAC THENL
2502      [
2503        MATCH_MP_TAC CONTINUOUS_ON_SUBSET THEN
2504          EXISTS_TAC `interval [lift (&0), lift h]` THEN
2505          ASM_REWRITE_TAC[SUBSET_INTERVAL_1; LIFT_DROP; REAL_LE_REFL];
2506        ALL_TAC
2507      ] THEN
2508
2509      STRIP_TAC THEN
2510
2511      (* Aux *)
2512      SUBGOAL_THEN `!t. &0 <= t /\ t <= r ==> a t % v1 + b t % v2:real^3 IN segment [f (lift t),w] INTER affine hull {vec 0,v1,v2}` (LABEL_TAC "a1") THENL
2513      [
2514        REPEAT STRIP_TAC THEN FIRST_X_ASSUM (MP_TAC o SPEC `t:real`) THEN
2515          ASM_REWRITE_TAC[EXTENSION; IN_SING; IN_INTER] THEN
2516          DISCH_THEN (MP_TAC o SPEC `a (t:real) % v1 + b t % v2:real^3`) THEN
2517          ASM_REWRITE_TAC[];
2518        ALL_TAC
2519      ] THEN
2520
2521      (* Aux *)
2522      SUBGOAL_THEN `!t. &0 <= t /\ t <= r ==> ?u. &0 <= u /\ u <= &1 /\ a t % v1 + b t % v2 = (&1 - u) % f (lift t) + u % w:real^3` (LABEL_TAC "a2") THENL
2523      [
2524        REPEAT STRIP_TAC THEN
2525          FIRST_X_ASSUM (MP_TAC o SPEC `t:real`) THEN
2526          ASM_REWRITE_TAC[IN_INTER; IN_SEGMENT] THEN
2527          STRIP_TAC THEN
2528          EXISTS_TAC `u:real` THEN
2529          ASM_REWRITE_TAC[];
2530        ALL_TAC
2531      ] THEN
2532
2533      (* Aux *)
2534      SUBGOAL_THEN `!t. &0 <= t /\ t <= r /\ &0 <= a t /\ &0 <= b t ==> (?x. x IN segment [f (lift t),w:real^3] INTER aff_ge {vec 0} {v1,v2})` (LABEL_TAC "a3") THENL
2535      [
2536        REPEAT STRIP_TAC THEN
2537          EXISTS_TAC `a (t:real) % (v1:real^3) + b t % v2` THEN
2538          REWRITE_TAC[IN_INTER] THEN
2539          REMOVE_THEN "a1" (MP_TAC o SPEC `t:real`) THEN
2540          ASM_SIMP_TAC[IN_INTER] THEN DISCH_TAC THEN
2541          ASM_SIMP_TAC[aff_ge_0_2; IN_ELIM_THM] THEN
2542          MAP_EVERY EXISTS_TAC [`(a:real->real) t`; `(b:real->real) t`] THEN
2543          ASM_REWRITE_TAC[];
2544        ALL_TAC
2545      ] THEN
2546
2547      (* Aux *)
2548      SUBGOAL_THEN `!t. &0 <= t /\ t <= r /\ ~(segment [f (lift t),w] INTER aff_ge {vec 0:real^3} {v1,v2} = {}) ==> &0 <= a t /\ &0 <= b t` (LABEL_TAC "a4") THENL
2549      [
2550        GEN_TAC THEN DISCH_THEN STRIP_ASSUME_TAC THEN
2551          POP_ASSUM MP_TAC THEN REWRITE_TAC[GSYM MEMBER_NOT_EMPTY; IN_INTER] THEN
2552          STRIP_TAC THEN
2553          SUBGOAL_THEN `x:real^3 IN segment [f (lift t),w] INTER affine hull {vec 0,v1,v2}` MP_TAC THENL
2554          [
2555            ASM_REWRITE_TAC[IN_INTER] THEN
2556              MATCH_MP_TAC Hypermap.lemma_in_subset THEN
2557              EXISTS_TAC `aff_ge {vec 0:real^3} {v1,v2}` THEN
2558              ASM_REWRITE_TAC[] THEN
2559              REWRITE_TAC[SET_RULE `{vec 0:real^3,v1,v2} = {vec 0} UNION {v1,v2}`] THEN
2560              REWRITE_TAC[AFF_GE_SUBSET_AFFINE_HULL];
2561            ALL_TAC
2562          ] THEN
2563          DISCH_TAC THEN FIRST_ASSUM MP_TAC THEN
2564          FIRST_ASSUM (ASSUME_TAC o REWRITE_RULE[IN_INTER]) THEN
2565          MP_TAC (ISPECL [`v1:real^3`; `v2:real^3`; `x:real^3`] in_affine_hull_lemma) THEN
2566          ASM_REWRITE_TAC[] THEN
2567          REMOVE_ASSUM THEN POP_ASSUM MP_TAC THEN
2568
2569          MAP_EVERY (fun s -> REMOVE_THEN s (fun th -> ALL_TAC)) ["a1"; "a2"; "a3"] THEN
2570          FIRST_X_ASSUM (MP_TAC o SPEC `t:real`) THEN
2571          ASM_REWRITE_TAC[] THEN
2572          DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
2573          REWRITE_TAC[IN_SING] THEN
2574          DISCH_THEN (LABEL_TAC "x1" o SYM) THEN
2575          STRIP_TAC THEN
2576          FIRST_X_ASSUM (LABEL_TAC "x2" o SYM o check (is_eq o concl)) THEN
2577          UNDISCH_TAC `x IN aff_ge {vec 0} {v1,v2:real^3}` THEN
2578          MP_TAC (ISPECL [`v1:real^3`; `v2:real^3`] aff_ge_0_2) THEN
2579          ASM_REWRITE_TAC[] THEN DISCH_THEN (fun th -> REWRITE_TAC[th; IN_ELIM_THM]) THEN
2580          STRIP_TAC THEN
2581          SUBGOAL_THEN `a (t:real) = t1'':real /\ b (t:real) = t2:real` MP_TAC THENL
2582          [
2583            FIRST_X_ASSUM MATCH_MP_TAC THEN
2584              REMOVE_THEN "x1" (fun th -> REWRITE_TAC[th]);
2585            ALL_TAC
2586          ] THEN
2587          SUBGOAL_THEN `t1''' = t1'':real /\ t2' = t2:real` MP_TAC THENL
2588          [
2589            FIRST_X_ASSUM MATCH_MP_TAC THEN
2590              POP_ASSUM (fun th -> REWRITE_TAC[th]);
2591            ALL_TAC
2592          ] THEN
2593          DISCH_THEN (fun th -> REWRITE_TAC[GSYM th]) THEN
2594          DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
2595          ASM_REWRITE_TAC[];
2596        ALL_TAC
2597      ] THEN
2598
2599      (* Aux *)
2600      SUBGOAL_THEN `&0 <= a (&0) /\ &0 <= b (&0)` (LABEL_TAC "a5") THENL
2601      [
2602        FIRST_X_ASSUM MATCH_MP_TAC THEN
2603          ASM_REWRITE_TAC[REAL_LE_REFL; REAL_LE_01];
2604        ALL_TAC
2605      ] THEN
2606
2607
2608      (* Cases for a(t) and b(t) *)
2609      SUBGOAL_THEN `?x. &0 <= x /\ x <= r /\ (!t. &0 <= t /\ t <= x ==> &0 <= a t /\ &0 <= b t) /\ (a x = &0 \/ b x = &0)` MP_TAC THENL
2610      [
2611        (* 0 <= a(t) for all t *)
2612        ASM_CASES_TAC `!t. &0 <= t /\ t <= r ==> &0 <= a t` THENL
2613          [
2614            MP_TAC (SPECL [`b:real->real`; `&0`; `t1':real`] continuous_lemma_dec) THEN
2615              ASM_REWRITE_TAC[] THEN
2616              ANTS_TAC THENL
2617              [
2618                CONJ_TAC THENL
2619                  [
2620                    MATCH_MP_TAC REAL_CONTINUOUS_ON_SUBSET THEN
2621                      EXISTS_TAC `real_interval [&0,r]` THEN
2622                      ASM_REWRITE_TAC[SUBSET_REAL_INTERVAL; REAL_LE_REFL];
2623                    ALL_TAC
2624                  ] THEN
2625                  FIRST_X_ASSUM (MP_TAC o check (is_eq o concl)) THEN
2626                  ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN
2627                  REWRITE_TAC[REAL_NOT_LE; GSYM MEMBER_NOT_EMPTY] THEN
2628                  DISCH_TAC THEN
2629                  FIRST_X_ASSUM MATCH_MP_TAC THEN
2630                  ASM_SIMP_TAC[REAL_LT_IMP_LE];
2631                ALL_TAC
2632              ] THEN
2633              STRIP_TAC THEN
2634
2635              EXISTS_TAC `x:real` THEN
2636              SUBGOAL_THEN `x <= r` ASSUME_TAC THENL
2637              [
2638                MATCH_MP_TAC REAL_LE_TRANS THEN
2639                  EXISTS_TAC `t1':real` THEN
2640                  ASM_REWRITE_TAC[];
2641                ALL_TAC
2642              ] THEN
2643              ASM_REWRITE_TAC[] THEN
2644              GEN_TAC THEN DISCH_TAC THEN
2645              CONJ_TAC THENL
2646              [
2647                FIRST_X_ASSUM MATCH_MP_TAC THEN
2648                  ASM_REWRITE_TAC[] THEN
2649                  MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `x:real` THEN
2650                  ASM_REWRITE_TAC[];
2651                ALL_TAC
2652              ] THEN
2653              ASM_CASES_TAC `t = x:real` THEN ASM_REWRITE_TAC[REAL_LE_REFL] THEN
2654              MATCH_MP_TAC REAL_LT_IMP_LE THEN
2655              FIRST_X_ASSUM MATCH_MP_TAC THEN
2656              ASM_REWRITE_TAC[REAL_ARITH `t < x <=> t <= x /\ ~(t = x)`];
2657            ALL_TAC
2658          ] THEN
2659
2660          (* a(ta) < 0 *)
2661          POP_ASSUM MP_TAC THEN
2662          REWRITE_TAC[NOT_FORALL_THM; TAUT `~(A ==> B) <=> A /\ ~B`; REAL_NOT_LE] THEN
2663          DISCH_THEN (X_CHOOSE_THEN `ta:real` ASSUME_TAC) THEN
2664
2665          MP_TAC (SPECL [`a:real->real`; `&0`; `ta:real`] continuous_lemma_dec) THEN
2666          ASM_SIMP_TAC[REAL_LT_IMP_LE] THEN
2667          ANTS_TAC THENL
2668          [
2669            MATCH_MP_TAC REAL_CONTINUOUS_ON_SUBSET THEN
2670              EXISTS_TAC `real_interval [&0,r]` THEN
2671              ASM_REWRITE_TAC[SUBSET_REAL_INTERVAL; REAL_LE_REFL];
2672            ALL_TAC
2673          ] THEN
2674          DISCH_THEN (X_CHOOSE_THEN `xa:real` MP_TAC) THEN
2675          STRIP_TAC THEN
2676          SUBGOAL_THEN `!t. &0 <= t /\ t <= xa ==> &0 <= a t` MP_TAC THENL
2677          [
2678            GEN_TAC THEN DISCH_TAC THEN
2679              ASM_CASES_TAC `t = xa:real` THEN ASM_REWRITE_TAC[REAL_LE_REFL] THEN
2680              MATCH_MP_TAC REAL_LT_IMP_LE THEN
2681              FIRST_X_ASSUM MATCH_MP_TAC THEN
2682              ASM_REWRITE_TAC[REAL_ARITH `t < xa <=> t <= xa /\ ~(t = xa)`];
2683            ALL_TAC
2684          ] THEN
2685          REMOVE_ASSUM THEN DISCH_TAC THEN
2686
2687          (* 0 <= b(t) for all t *)
2688          ASM_CASES_TAC `!t. &0 <= t /\ t <= r ==> &0 <= b t` THENL
2689          [
2690            EXISTS_TAC `xa:real` THEN
2691              SUBGOAL_THEN `xa <= r` ASSUME_TAC THENL
2692              [
2693                MATCH_MP_TAC REAL_LE_TRANS THEN
2694                  EXISTS_TAC `ta:real` THEN
2695                  ASM_REWRITE_TAC[];
2696                ALL_TAC
2697              ] THEN
2698              ASM_REWRITE_TAC[] THEN
2699              GEN_TAC THEN DISCH_TAC THEN
2700              CONJ_TAC THENL
2701              [
2702                FIRST_X_ASSUM MATCH_MP_TAC THEN
2703                  ASM_REWRITE_TAC[];
2704                ALL_TAC
2705              ] THEN
2706              FIRST_X_ASSUM MATCH_MP_TAC THEN
2707              ASM_REWRITE_TAC[] THEN
2708              MATCH_MP_TAC REAL_LE_TRANS THEN
2709              EXISTS_TAC `xa:real` THEN
2710              ASM_REWRITE_TAC[];
2711            ALL_TAC
2712          ] THEN
2713
2714          (* b(tb) < 0 *)
2715          POP_ASSUM MP_TAC THEN
2716          REWRITE_TAC[NOT_FORALL_THM; TAUT `~(A ==> B) <=> A /\ ~B`; REAL_NOT_LE] THEN
2717          DISCH_THEN (X_CHOOSE_THEN `tb:real` ASSUME_TAC) THEN
2718
2719          MP_TAC (SPECL [`b:real->real`; `&0`; `tb:real`] continuous_lemma_dec) THEN
2720          ASM_SIMP_TAC[REAL_LT_IMP_LE] THEN
2721          ANTS_TAC THENL
2722          [
2723            MATCH_MP_TAC REAL_CONTINUOUS_ON_SUBSET THEN
2724              EXISTS_TAC `real_interval [&0,r]` THEN
2725              ASM_REWRITE_TAC[SUBSET_REAL_INTERVAL; REAL_LE_REFL];
2726            ALL_TAC
2727          ] THEN
2728          DISCH_THEN (X_CHOOSE_THEN `xb:real` MP_TAC) THEN
2729          STRIP_TAC THEN
2730          SUBGOAL_THEN `!t. &0 <= t /\ t <= xb ==> &0 <= b t` MP_TAC THENL
2731          [
2732            GEN_TAC THEN DISCH_TAC THEN
2733              ASM_CASES_TAC `t = xb:real` THEN ASM_REWRITE_TAC[REAL_LE_REFL] THEN
2734              MATCH_MP_TAC REAL_LT_IMP_LE THEN
2735              FIRST_X_ASSUM MATCH_MP_TAC THEN
2736              ASM_REWRITE_TAC[REAL_ARITH `t < xa <=> t <= xa /\ ~(t = xa)`];
2737            ALL_TAC
2738          ] THEN
2739          REMOVE_ASSUM THEN DISCH_TAC THEN
2740
2741          EXISTS_TAC `min xa xb` THEN
2742          ASM_REWRITE_TAC[REAL_LE_MIN] THEN
2743          CONJ_TAC THENL
2744          [
2745            MATCH_MP_TAC REAL_LE_TRANS THEN
2746              EXISTS_TAC `xa:real` THEN
2747              REWRITE_TAC[REAL_MIN_MIN] THEN
2748              MATCH_MP_TAC REAL_LE_TRANS THEN
2749              EXISTS_TAC `ta:real` THEN
2750              ASM_REWRITE_TAC[];
2751            ALL_TAC
2752          ] THEN
2753          CONJ_TAC THENL
2754          [
2755            GEN_TAC THEN DISCH_TAC THEN
2756              CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[];
2757            ALL_TAC
2758          ] THEN
2759          REWRITE_TAC[real_min] THEN
2760          COND_CASES_TAC THEN ASM_REWRITE_TAC[];
2761        ALL_TAC
2762      ] THEN
2763
2764      (* The final stage *)
2765      DISCH_THEN (CHOOSE_THEN MP_TAC) THEN
2766      ONCE_REWRITE_TAC[TAUT `A /\ B /\ C /\ D <=> (A /\ B) /\ C /\ D`] THEN
2767      DISCH_THEN (CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
2768      DISCH_THEN (CONJUNCTS_THEN ASSUME_TAC) THEN
2769
2770      EXISTS_TAC `x:real` THEN
2771      ASM_REWRITE_TAC[] THEN
2772      CONJ_TAC THENL
2773      [
2774        MATCH_MP_TAC REAL_LE_TRANS THEN
2775          EXISTS_TAC `r:real` THEN
2776          ASM_REWRITE_TAC[];
2777        ALL_TAC
2778      ] THEN
2779      CONJ_TAC THENL
2780      [
2781        GEN_TAC THEN
2782          FIRST_X_ASSUM (MP_TAC o SPECL [`drop (t:real^1)`; `x:real`]) THEN
2783          REWRITE_TAC[LIFT_DROP] THEN
2784          DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
2785          DISCH_TAC THEN
2786          REMOVE_THEN "a3" (MP_TAC o SPEC `drop (t:real^1)`) THEN
2787          ANTS_TAC THENL
2788          [
2789            ASM_REWRITE_TAC[] THEN
2790              CONJ_TAC THENL [ MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `x:real` THEN ASM_REWRITE_TAC[]; ALL_TAC ] THEN
2791              FIRST_X_ASSUM MATCH_MP_TAC THEN
2792              ASM_REWRITE_TAC[];
2793            ALL_TAC
2794          ] THEN
2795          SIMP_TAC[LIFT_DROP];
2796        ALL_TAC
2797      ] THEN
2798
2799      (* The final case split: a x = 0 or b x = 0 *)
2800      POP_ASSUM DISJ_CASES_TAC THENL
2801      [
2802        DISJ2_TAC THEN DISJ2_TAC THEN
2803          REMOVE_THEN "fw" (MP_TAC o SPEC `x:real`) THEN
2804          ANTS_TAC THENL
2805          [
2806            ASM_REWRITE_TAC[] THEN
2807              MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `r:real` THEN ASM_REWRITE_TAC[];
2808            ALL_TAC
2809          ] THEN
2810          STRIP_TAC THEN
2811          ASM_SIMP_TAC[aff_ge_0_2; IN_ELIM_THM] THEN
2812          REMOVE_THEN "a2" (MP_TAC o SPEC `x:real`) THEN
2813          ASM_REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_LID] THEN
2814          STRIP_TAC THEN
2815          POP_ASSUM MP_TAC THEN
2816          ASM_CASES_TAC `b (x:real) = &0` THENL [ ASM_SIMP_TAC[VECTOR_MUL_LZERO]; ALL_TAC ] THEN
2817          DISCH_THEN (MP_TAC o AP_TERM `\v:real^3. inv ((b:real->real) x) % v`) THEN
2818          REWRITE_TAC[VECTOR_MUL_ASSOC; VECTOR_ADD_LDISTRIB] THEN
2819          ASM_SIMP_TAC[REAL_MUL_LINV; VECTOR_MUL_LID] THEN
2820          DISCH_TAC THEN
2821          MAP_EVERY EXISTS_TAC [`inv (b (x:real)) * (&1 - u)`; `inv (b (x:real)) * u`] THEN
2822          REWRITE_TAC[] THEN
2823          SUBGOAL_THEN `&0 <= inv (b (x:real))` ASSUME_TAC THENL
2824          [
2825            MATCH_MP_TAC REAL_LE_INV THEN
2826              REPLICATE_TAC 2 (FIRST_X_ASSUM (MP_TAC o SPEC `x:real`)) THEN
2827              ASM_SIMP_TAC[REAL_LE_REFL];
2828            ALL_TAC
2829          ] THEN
2830          CONJ_TAC THEN MATCH_MP_TAC REAL_LE_MUL THEN CONJ_TAC THEN ASM_REWRITE_TAC[REAL_ARITH `&0 <= &1 - u <=> u <= &1`];
2831        ALL_TAC
2832      ] THEN
2833
2834      DISJ2_TAC THEN DISJ1_TAC THEN
2835      REMOVE_THEN "fw" (MP_TAC o SPEC `x:real`) THEN
2836      ANTS_TAC THENL
2837      [
2838        ASM_REWRITE_TAC[] THEN
2839          MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `r:real` THEN ASM_REWRITE_TAC[];
2840        ALL_TAC
2841      ] THEN
2842      STRIP_TAC THEN
2843      ASM_SIMP_TAC[aff_ge_0_2; IN_ELIM_THM] THEN
2844      REMOVE_THEN "a2" (MP_TAC o SPEC `x:real`) THEN
2845      ASM_REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_RID] THEN
2846      STRIP_TAC THEN
2847      POP_ASSUM MP_TAC THEN
2848      ASM_CASES_TAC `a (x:real) = &0` THENL [ ASM_SIMP_TAC[VECTOR_MUL_LZERO]; ALL_TAC ] THEN
2849      DISCH_THEN (MP_TAC o AP_TERM `\v:real^3. inv ((a:real->real) x) % v`) THEN
2850      REWRITE_TAC[VECTOR_MUL_ASSOC; VECTOR_ADD_LDISTRIB] THEN
2851      ASM_SIMP_TAC[REAL_MUL_LINV; VECTOR_MUL_LID] THEN
2852      DISCH_TAC THEN
2853      MAP_EVERY EXISTS_TAC [`inv (a (x:real)) * (&1 - u)`; `inv (a (x:real)) * u`] THEN
2854      REWRITE_TAC[] THEN
2855      SUBGOAL_THEN `&0 <= inv (a (x:real))` ASSUME_TAC THENL
2856      [
2857        MATCH_MP_TAC REAL_LE_INV THEN
2858          REPLICATE_TAC 2 (FIRST_X_ASSUM (MP_TAC o SPEC `x:real`)) THEN
2859          ASM_SIMP_TAC[REAL_LE_REFL];
2860        ALL_TAC
2861      ] THEN
2862      CONJ_TAC THEN MATCH_MP_TAC REAL_LE_MUL THEN CONJ_TAC THEN ASM_REWRITE_TAC[REAL_ARITH `&0 <= &1 - u <=> u <= &1`]
2863 );;
2864
2865
2866
2867
2868 (* v1 and v3 in a 4-point configuration are separated by the plane affine hull {0,v2,v4} *)
2869
2870 let separation_plane_4_points = prove(`!v1 v2 v3 v4:real^3. v1 IN ball_annulus /\ v2 IN ball_annulus /\ v3 IN ball_annulus /\ v4 IN ball_annulus /\
2871                                         dist (v2, v4) <= &2 * h0 /\ dist (v1, v3) <= &2 * h0 /\ &2 <= dist (v2, v4) /\
2872                                         &2 <= dist (v1, v2) /\ &2 <= dist (v1, v4) /\
2873                                         &2 <= dist (v2, v3) /\ &2 <= dist (v3, v4) /\
2874                                         ~(segment [v1, v3] INTER aff_ge {vec 0} {v2, v4} = {})
2875                                           ==> ?n. ~(n = vec 0) /\ v2 dot n = &0 /\ v4 dot n = &0 /\
2876                                               v1 dot n < &0 /\ &0 < v3 dot n`,
2877    REPEAT STRIP_TAC THEN
2878      SUBGOAL_THEN `~(v1 = vec 0:real^3) /\ ~(v2 = vec 0:real^3) /\ ~(v3 = vec 0:real^3) /\ ~(v4 = vec 0:real^3)` ASSUME_TAC THENL
2879      [
2880        REPEAT (FIRST_X_ASSUM (MP_TAC o check (is_binary "IN" o concl))) THEN
2881          SIMP_TAC[in_ball_annulus];
2882        ALL_TAC
2883      ] THEN
2884      SUBGOAL_THEN `~collinear {vec 0, v2, v4:real^3}` ASSUME_TAC THENL
2885      [
2886        ASM_SIMP_TAC[estd_non_collinear_lemma];
2887        ALL_TAC
2888      ] THEN
2889      SUBGOAL_THEN `~between (vec 0) (v1:real^3,v3)` ASSUME_TAC THENL
2890      [
2891        ASM_SIMP_TAC[zero_not_between_estd];
2892        ALL_TAC
2893      ] THEN
2894
2895      SUBGOAL_THEN `?n:real^3. ~(n = vec 0) /\ v2 dot n = &0 /\ v4 dot n = &0 /\ v1 dot n <= &0` MP_TAC THENL
2896      [
2897        ASM_CASES_TAC `v1 dot (v2 cross v4) <= &0` THENL
2898          [
2899            EXISTS_TAC `v2 cross v4` THEN
2900              ASM_REWRITE_TAC[CROSS_EQ_0; DOT_CROSS_SELF];
2901            ALL_TAC
2902          ] THEN
2903          EXISTS_TAC `--(v2 cross v4)` THEN
2904          ASM_REWRITE_TAC[VECTOR_NEG_EQ_0; CROSS_EQ_0; DOT_RNEG; DOT_CROSS_SELF] THEN
2905          POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;
2906        ALL_TAC
2907      ] THEN
2908      STRIP_TAC THEN
2909
2910      EXISTS_TAC `n:real^3` THEN
2911      SUBGOAL_THEN `~(v1 IN aff_ge {vec 0:real^3} {v2, v4}) /\ ~(v3 IN aff_ge {vec 0} {v2, v4})` ASSUME_TAC THENL
2912      [
2913        CONJ_TAC THEN DISCH_TAC THEN MATCH_MP_TAC LEMMA_3_POINTS_FINAL THENL
2914          [
2915            MAP_EVERY EXISTS_TAC [`v2:real^3`; `v4:real^3`; `v1:real^3`];
2916            MAP_EVERY EXISTS_TAC [`v2:real^3`; `v4:real^3`; `v3:real^3`]
2917          ] THEN
2918          ASM_REWRITE_TAC[DIST_SYM];
2919        ALL_TAC
2920      ] THEN
2921      SUBGOAL_THEN `~(v2 IN aff_ge {vec 0:real^3} {v1, v3}) /\ ~(v4 IN aff_ge {vec 0:real^3} {v1, v3})` ASSUME_TAC THENL
2922      [
2923        CONJ_TAC THEN DISCH_TAC THEN MATCH_MP_TAC LEMMA_3_POINTS_FINAL THENL
2924          [
2925            MAP_EVERY EXISTS_TAC [`v1:real^3`; `v3:real^3`; `v2:real^3`];
2926            MAP_EVERY EXISTS_TAC [`v1:real^3`; `v3:real^3`; `v4:real^3`]
2927          ] THEN
2928          ASM_REWRITE_TAC[DIST_SYM];
2929        ALL_TAC
2930      ] THEN
2931
2932      ASM_REWRITE_TAC[] THEN
2933      ASM_CASES_TAC `v1 dot n:real^3 = &0` THENL
2934      [
2935        ASM_CASES_TAC `v3 dot n:real^3 = &0` THENL
2936          [
2937            MP_TAC (ISPECL [`v2:real^3`; `v4:real^3`; `v1:real^3`; `v3:real^3`] segment_intersects_aff_ge_lemma) THEN
2938              ANTS_TAC THENL
2939              [
2940                ASM_REWRITE_TAC[] THEN
2941                  ASM_SIMP_TAC[affine_hull_3_plane; IN_ELIM_THM];
2942                ALL_TAC
2943              ] THEN
2944              ASM_REWRITE_TAC[];
2945            ALL_TAC
2946          ] THEN
2947          MP_TAC (ISPECL [`v2:real^3`; `v4:real^3`; `v1:real^3`; `v3:real^3`; `n:real^3`] segment_inter_aff_ge_ends) THEN
2948          ASM_REWRITE_TAC[];
2949        ALL_TAC
2950      ] THEN
2951
2952      CONJ_TAC THENL [ ASM_REWRITE_TAC[REAL_LT_LE]; ALL_TAC ] THEN
2953      DISJ_CASES_TAC (REAL_ARITH `v3 dot n:real^3 < &0 \/ v3 dot n = &0 \/ &0 < v3 dot n`) THENL
2954      [
2955        UNDISCH_TAC `~(segment [v1:real^3,v3] INTER aff_ge {vec 0} {v2,v4} = {})` THEN
2956          REWRITE_TAC[GSYM MEMBER_NOT_EMPTY] THEN
2957          REWRITE_TAC[IN_INTER; IN_SEGMENT] THEN
2958          ASM_SIMP_TAC[aff_ge_0_2; IN_ELIM_THM] THEN
2959          STRIP_TAC THEN
2960          POP_ASSUM (MP_TAC o AP_TERM `\v:real^3. v dot n`) THEN
2961          ASM_REWRITE_TAC[DOT_LADD; DOT_LMUL; REAL_MUL_RZERO; REAL_ADD_LID] THEN
2962          ASM_CASES_TAC `u = &0` THEN ASM_REWRITE_TAC[] THENL
2963          [
2964            ASM_REWRITE_TAC[REAL_SUB_RZERO; REAL_MUL_LZERO; REAL_MUL_LID; REAL_ADD_RID];
2965            ALL_TAC
2966          ] THEN
2967          SUBGOAL_THEN `(&1 - u) * (v1 dot n:real^3) + u * (v3 dot n) < &0` MP_TAC THENL
2968          [
2969            REWRITE_TAC[REAL_ARITH `(&1 - u) * a + u * b < &0 <=> &0 < u * --b + (&1 - u) * --a`] THEN
2970              MATCH_MP_TAC REAL_LTE_ADD THEN
2971              CONJ_TAC THENL
2972              [
2973                MATCH_MP_TAC REAL_LT_MUL THEN
2974                  ASM_REWRITE_TAC[REAL_NEG_GT0; REAL_LT_LE];
2975                ALL_TAC
2976              ] THEN
2977              MATCH_MP_TAC REAL_LE_MUL THEN
2978              ASM_REWRITE_TAC[REAL_NEG_GE0; REAL_LT_LE] THEN
2979              ASM_REWRITE_TAC[REAL_ARITH `&0 <= &1 - u <=> u <= &1`];
2980            ALL_TAC
2981          ] THEN
2982          REAL_ARITH_TAC;
2983        ALL_TAC
2984      ] THEN
2985
2986      POP_ASSUM DISJ_CASES_TAC THENL
2987      [
2988        MP_TAC (ISPECL [`v2:real^3`; `v4:real^3`; `v3:real^3`; `v1:real^3`; `n:real^3`] segment_inter_aff_ge_ends) THEN
2989          ASM_REWRITE_TAC[SEGMENT_SYM];
2990        ALL_TAC
2991      ] THEN
2992      ASM_REWRITE_TAC[]);;
2993
2994
2995
2996
2997
2998 (************************************************************************************)
2999
3000
3001
3002 (* The first rotation lemma for a 4-point configuration *)
3003 let lemma_4_points_rotation1 = prove(`!v1 v2 v3 v4. v1 IN ball_annulus /\ v2 IN ball_annulus /\ v3 IN ball_annulus /\ v4 IN ball_annulus /\
3004                                        dist (v1, v3) <= &2 * h0 /\ dist (v2, v4) <= &2 * h0 /\
3005                                        &2 <= dist (v1, v2) /\ &2 <= dist (v1, v4) /\
3006                                        &2 <= dist (v2, v3) /\ &2 <= dist (v3, v4) /\
3007                                        &2 <= dist (v2, v4) /\
3008                                        ~(segment [v1, v3] INTER aff_ge {vec 0} {v2, v4} = {})
3009                                        ==> (?v1'. v1' IN ball_annulus /\ norm v1' = norm v1 /\
3010                                               dist (v1', v3) <= &2 * h0 /\
3011                                               dist (v1', v2) = dist (v1, v2) /\ dist (v1', v4) = &2 /\
3012                                               ~(segment [v1',v3] INTER aff_ge {vec 0} {v2,v4} = {}))`,
3013    REPEAT STRIP_TAC THEN
3014      SUBGOAL_THEN `~collinear {vec 0, v2, v4:real^3}` ASSUME_TAC THENL
3015      [
3016        MATCH_MP_TAC estd_non_collinear_lemma THEN
3017          ASM_REWRITE_TAC[];
3018        ALL_TAC
3019      ] THEN
3020
3021      SUBGOAL_THEN `~(v1 = vec 0:real^3) /\ ~(v2 = vec 0:real^3) /\ ~(v3 = vec 0:real^3) /\ ~(v4 = vec 0:real^3)` ASSUME_TAC THENL
3022      [
3023        REPEAT (FIRST_X_ASSUM (MP_TAC o check (is_binary "IN" o concl))) THEN
3024          SIMP_TAC[in_ball_annulus];
3025        ALL_TAC
3026      ] THEN
3027
3028      MP_TAC (SPEC_ALL separation_plane_4_points) THEN
3029      ASM_REWRITE_TAC[] THEN
3030      STRIP_TAC THEN
3031
3032      MP_TAC (ISPECL [`v2:real^3`; `v1:real^3`; `v3:real^3`] rotation_about_axis) THEN
3033      ASM_REWRITE_TAC[DIMINDEX_3; LE_REFL; projection] THEN
3034      ANTS_TAC THENL
3035      [
3036        CONJ_TAC THEN DISCH_THEN (MP_TAC o AP_TERM `\x:real^3. x dot n`) THEN ASM_REWRITE_TAC[DOT_LSUB; DOT_LMUL; DOT_LZERO; REAL_MUL_RZERO; REAL_SUB_RZERO] THENL
3037          [
3038            ASM_SIMP_TAC[REAL_ARITH `&0 < a ==> ~(a = &0)`];
3039            ASM_SIMP_TAC[REAL_LT_IMP_NE]
3040          ];
3041        ALL_TAC
3042      ] THEN
3043      STRIP_TAC THEN
3044
3045      SUBGOAL_THEN `!t. (f:real^1->real^3) t IN ball_annulus` ASSUME_TAC THENL
3046      [
3047        GEN_TAC THEN REWRITE_TAC[in_ball_annulus] THEN
3048          REWRITE_TAC[GSYM NORM_EQ_0] THEN
3049          SUBGOAL_THEN `norm ((f:real^1->real^3) t) = norm (v1:real^3)` (fun th -> REWRITE_TAC[th]) THENL
3050          [
3051            FIRST_X_ASSUM (MP_TAC o SPECL [`t:real^1`; `&0`]) THEN
3052              SIMP_TAC[VECTOR_MUL_LZERO; DIST_0];
3053            ALL_TAC
3054          ] THEN
3055          REWRITE_TAC[NORM_EQ_0] THEN
3056          REWRITE_TAC[GSYM in_ball_annulus] THEN ASM_REWRITE_TAC[];
3057        ALL_TAC
3058      ] THEN
3059
3060      MP_TAC (ISPECL [`v2:real^3`; `v4:real^3`; `f:real^1->real^3`; `v3:real^3`; `&1`] continuous_lemma_aff_ge) THEN
3061      ANTS_TAC THENL
3062      [
3063        ASM_REWRITE_TAC[REAL_LE_01] THEN
3064          CONJ_TAC THENL
3065          [
3066            MATCH_MP_TAC CONTINUOUS_ON_SUBSET THEN
3067              EXISTS_TAC `(:real^1)` THEN
3068              ASM_REWRITE_TAC[SUBSET_UNIV];
3069            ALL_TAC
3070          ] THEN
3071          GEN_TAC THEN DISCH_TAC THEN
3072          MATCH_MP_TAC zero_not_between_estd THEN
3073          ASM_REWRITE_TAC[] THEN
3074          MATCH_MP_TAC REAL_LE_TRANS THEN
3075          EXISTS_TAC `dist (v1:real^3,v3)` THEN
3076          ASM_REWRITE_TAC[] THEN
3077           FIRST_X_ASSUM (MP_TAC o SPEC `drop (t:real^1)`) THEN
3078          ANTS_TAC THENL
3079          [
3080            POP_ASSUM MP_TAC THEN
3081              SUBGOAL_THEN `t = lift (drop (t:real^1))` (fun th -> GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [th]) THENL
3082              [
3083                REWRITE_TAC[LIFT_DROP];
3084                ALL_TAC
3085              ] THEN
3086              REWRITE_TAC[IN_INTERVAL_1];
3087            ALL_TAC
3088          ] THEN
3089          REWRITE_TAC[LIFT_DROP];
3090        ALL_TAC
3091      ] THEN
3092
3093      DISCH_THEN DISJ_CASES_TAC THENL
3094      [
3095        MATCH_MP_TAC (TAUT `F ==> A`) THEN
3096          POP_ASSUM (MP_TAC o SPEC `lift (&1)`) THEN
3097          REWRITE_TAC[GSYM MEMBER_NOT_EMPTY] THEN
3098          REWRITE_TAC[IN_INTERVAL_1; REAL_LE_REFL; REAL_LE_01] THEN
3099          REWRITE_TAC[IN_INTER; IN_SEGMENT] THEN
3100          ASM_SIMP_TAC[aff_ge_0_2; IN_ELIM_THM] THEN
3101          STRIP_TAC THEN
3102          POP_ASSUM (MP_TAC o AP_TERM `\x:real^3. x dot n`) THEN
3103          ASM_REWRITE_TAC[DOT_LADD; DOT_LMUL; REAL_MUL_RZERO; REAL_ADD_RID] THEN
3104          MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~(a = &0)`) THEN
3105          REWRITE_TAC[REAL_ARITH `(&1 - u) * a * b + u * b = b * (a * (&1 - u) + u)`] THEN
3106          MATCH_MP_TAC REAL_LT_MUL THEN
3107          ASM_REWRITE_TAC[] THEN
3108          ASM_CASES_TAC `u = &0` THENL
3109          [
3110            ASM_REWRITE_TAC[REAL_SUB_RZERO; REAL_MUL_RID; REAL_ADD_RID];
3111            ALL_TAC
3112          ] THEN
3113          MATCH_MP_TAC REAL_LET_ADD THEN
3114          ASM_REWRITE_TAC[REAL_LT_LE] THEN
3115          MATCH_MP_TAC REAL_LE_MUL THEN
3116          ASM_SIMP_TAC[REAL_LT_IMP_LE; REAL_ARITH `&0 <= &1 - u <=> u <= &1`];
3117        ALL_TAC
3118      ] THEN
3119
3120      POP_ASSUM MP_TAC THEN
3121      DISCH_THEN (CHOOSE_THEN MP_TAC) THEN
3122      REWRITE_TAC[CONJ_ASSOC] THEN
3123      DISCH_THEN (CONJUNCTS_THEN ASSUME_TAC) THEN
3124
3125      SUBGOAL_THEN `!t. &2 <= dist (f (t:real^1), v2:real^3)` ASSUME_TAC THENL
3126      [
3127        GEN_TAC THEN
3128          FIRST_X_ASSUM (MP_TAC o SPECL [`t:real^1`; `&1`]) THEN
3129          ASM_SIMP_TAC[VECTOR_MUL_LID];
3130        ALL_TAC
3131      ] THEN
3132
3133      SUBGOAL_THEN `!t. &0 <= t /\ t <= &1 ==> dist (f (lift t),v3:real^3) <= &2 * h0` ASSUME_TAC THENL
3134      [
3135        REPEAT STRIP_TAC THEN
3136          MATCH_MP_TAC REAL_LE_TRANS THEN
3137          EXISTS_TAC `dist (v1:real^3, v3)` THEN
3138          ASM_SIMP_TAC[];
3139        ALL_TAC
3140      ] THEN
3141
3142      SUBGOAL_THEN `dist (f (lift x), v4:real^3) < &2` ASSUME_TAC THENL
3143      [
3144        FIRST_X_ASSUM (MP_TAC o check (is_disj o concl)) THEN
3145          ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN
3146          REWRITE_TAC[REAL_NOT_LT; DE_MORGAN_THM] THEN
3147          DISCH_TAC THEN
3148
3149          REPEAT CONJ_TAC THEN DISCH_TAC THEN MATCH_MP_TAC LEMMA_3_POINTS_FINAL THENL
3150          [
3151            MAP_EVERY EXISTS_TAC [`v2:real^3`; `v4:real^3`; `f (lift x):real^3`] THEN
3152              ASM_REWRITE_TAC[DIST_SYM];
3153            MAP_EVERY EXISTS_TAC [`f (lift x):real^3`; `v3:real^3`; `v2:real^3`] THEN
3154              ASM_SIMP_TAC[DIST_SYM];
3155            MAP_EVERY EXISTS_TAC [`f (lift x):real^3`; `v3:real^3`; `v4:real^3`] THEN
3156              ASM_SIMP_TAC[];
3157          ];
3158        ALL_TAC
3159      ] THEN
3160
3161      MP_TAC (ISPECL [`f:real^1->real^3`; `v4:real^3`; `x:real`; `&2`] dist_decreasing_ivt_lemma) THEN
3162      ASM_SIMP_TAC[REAL_LT_IMP_LE] THEN
3163      STRIP_TAC THEN
3164      EXISTS_TAC `(f:real^1->real^3) t` THEN
3165
3166      SUBGOAL_THEN `!t:real^1. dist ((f t):real^3,v2) = dist (v1,v2)` ASSUME_TAC THENL
3167      [
3168        GEN_TAC THEN
3169          FIRST_X_ASSUM (MP_TAC o SPECL [`t':real^1`; `&1`]) THEN
3170          SIMP_TAC[VECTOR_MUL_LID];
3171        ALL_TAC
3172      ] THEN
3173
3174      ASM_SIMP_TAC[] THEN
3175      CONJ_TAC THENL
3176      [
3177        FIRST_X_ASSUM (MP_TAC o SPECL [`t:real^1`; `&0`]) THEN
3178          SIMP_TAC[VECTOR_MUL_LZERO; DIST_0];
3179        ALL_TAC
3180      ] THEN
3181
3182      FIRST_X_ASSUM (MP_TAC o SPEC `drop (t:real^1)`) THEN
3183      ANTS_TAC THENL
3184      [
3185        REWRITE_TAC[GSYM IN_INTERVAL_1; LIFT_DROP] THEN
3186          MATCH_MP_TAC Hypermap.lemma_in_subset THEN
3187          EXISTS_TAC `interval [lift (&0), lift x]` THEN
3188          ASM_REWRITE_TAC[SUBSET_INTERVAL] THEN
3189          REWRITE_TAC[DIMINDEX_1; ARITH_RULE `1 <= i /\ i <= 1 <=> i = 1`] THEN
3190          SIMP_TAC[] THEN
3191          ASM_REWRITE_TAC[GSYM drop; LIFT_DROP; REAL_LE_REFL];
3192        ALL_TAC
3193      ] THEN
3194
3195      REWRITE_TAC[LIFT_DROP]);;
3196
3197
3198
3199
3200 (*****************************************************************************************)
3201
3202
3203 let lemma_4_points_rotation1_full = prove(`!v1 v2 v3 v4. v1 IN ball_annulus /\ v2 IN ball_annulus /\ v3 IN ball_annulus /\ v4 IN ball_annulus /\
3204                                             dist (v1,v3) <= &2 * h0 /\ dist (v2,v4) <= &2 * h0 /\
3205                                             &2 <= dist (v1,v2) /\ &2 <= dist (v1,v4) /\
3206                                             &2 <= dist (v2,v3) /\ &2 <= dist (v3,v4) /\
3207                                             &2 <= dist (v2,v4) /\
3208                                             ~(segment [v1,v3] INTER aff_ge {vec 0} {v2, v4} = {})
3209                                             ==> (?v1' v3'. v1' IN ball_annulus /\ v3' IN ball_annulus /\
3210                                                    norm v1' = norm v1 /\ norm v3' = norm v3 /\
3211                                                    dist (v1',v3') <= &2 * h0 /\
3212                                                    dist (v1',v2) = &2 /\ dist (v1',v4) = &2 /\
3213                                                    dist (v2,v3') = &2 /\ dist (v3',v4) = &2 /\
3214                                                    ~(segment [v1',v3'] INTER aff_ge {vec 0} {v2, v4} = {}))`,
3215    REPEAT STRIP_TAC THEN
3216      (* v1 about v2 *)
3217      MP_TAC (SPEC_ALL lemma_4_points_rotation1) THEN
3218      ASM_REWRITE_TAC[] THEN
3219      STRIP_TAC THEN
3220      SUBGOAL_THEN `&2 <= dist (v1':real^3,v2)` ASSUME_TAC THENL
3221      [
3222        ASM_REWRITE_TAC[];
3223        ALL_TAC
3224      ] THEN
3225      UNDISCH_TAC `norm (v1':real^3) = norm (v1:real^3)` THEN
3226      REPEAT (FIRST_X_ASSUM ((fun th -> ALL_TAC) o check (free_in `v1:real^3` o concl))) THEN
3227      DISCH_TAC THEN
3228
3229      (* v1 about v4 *)
3230      MP_TAC (SPECL [`v1':real^3`; `v4:real^3`; `v3:real^3`; `v2:real^3`] lemma_4_points_rotation1) THEN
3231      ASM_REWRITE_TAC[REAL_LE_REFL; DIST_SYM; Collect_geom.PER_SET2] THEN
3232      REMOVE_ASSUM THEN
3233      REPEAT (FIRST_X_ASSUM ((fun th -> ALL_TAC) o check (free_in `v1':real^3` o concl))) THEN
3234      DISCH_THEN (X_CHOOSE_THEN `v1':real^3` MP_TAC) THEN STRIP_TAC THEN
3235
3236      (* v3 about v2 *)
3237      MP_TAC (SPECL [`v3:real^3`; `v2:real^3`; `v1':real^3`; `v4:real^3`] lemma_4_points_rotation1) THEN
3238      ASM_REWRITE_TAC[DIST_SYM; REAL_LE_REFL; SEGMENT_SYM] THEN
3239      DISCH_THEN (X_CHOOSE_THEN `v3':real^3` MP_TAC) THEN
3240      REWRITE_TAC[DIST_SYM] THEN STRIP_TAC THEN
3241      UNDISCH_TAC `norm (v3':real^3) = norm (v3:real^3)` THEN
3242      SUBGOAL_THEN `&2 <= dist (v2:real^3,v3')` ASSUME_TAC THENL
3243      [
3244        ASM_REWRITE_TAC[];
3245        ALL_TAC
3246      ] THEN
3247      REPEAT (FIRST_X_ASSUM ((fun th -> ALL_TAC) o check (free_in `v3:real^3` o concl))) THEN
3248      DISCH_TAC THEN
3249
3250      (* v3 about v4 *)
3251      MP_TAC (SPECL [`v3':real^3`; `v4:real^3`; `v1':real^3`; `v2:real^3`] lemma_4_points_rotation1) THEN
3252      ASM_REWRITE_TAC[REAL_LE_REFL; DIST_SYM; Collect_geom.PER_SET2; SEGMENT_SYM] THEN
3253      REPEAT (FIRST_X_ASSUM ((fun th -> ALL_TAC) o check (free_in `v3':real^3` o concl))) THEN
3254      DISCH_THEN (X_CHOOSE_THEN `v3':real^3` MP_TAC) THEN STRIP_TAC THEN
3255
3256      MAP_EVERY EXISTS_TAC [`v1':real^3`; `v3':real^3`] THEN
3257      ASM_REWRITE_TAC[DIST_SYM; SEGMENT_SYM]);;
3258
3259
3260
3261 (*******************************************************************************************)
3262
3263
3264 (* Auxiliary result for the second rotation lemma *)
3265
3266 let segment_inter_conv = prove(`!v1 v2 v3 v4 n:real^N. ~(v2 = vec 0) /\ ~(v4 = vec 0) /\ ~(v2 = v4) /\
3267                                  ~(projection (v4 - v2) (--v2) = vec 0) /\
3268                                  ~(segment [v1, v3] INTER aff_ge {vec 0} {v2, v4} = {}) /\
3269                                  v1 dot n < &0 /\ &0 < v3 dot n /\ v2 dot n = &0 /\ v4 dot n = &0 /\
3270                                  ~(segment [projection (v4 - v2) (v1 - v2), projection (v4 - v2) (v3 - v2)] INTER
3271                                      aff_ge {vec 0} {projection (v4 - v2) (--v2)} = {})
3272                                  ==> ~(segment [v1, v3] INTER convex hull {vec 0, v2, v4} = {})`,
3273     REPEAT STRIP_TAC THEN
3274       POP_ASSUM MP_TAC THEN REWRITE_TAC[GSYM MEMBER_NOT_EMPTY] THEN
3275       REWRITE_TAC[IN_SEGMENT; CONVEX_HULL_3_ALT; IN_INTER; IN_ELIM_THM; VECTOR_SUB_RZERO; VECTOR_ADD_LID] THEN
3276
3277       UNDISCH_TAC `~(segment [v1,v3] INTER aff_ge {vec 0} {v2,v4:real^N} = {})` THEN
3278       REWRITE_TAC[GSYM MEMBER_NOT_EMPTY; IN_SEGMENT; IN_INTER] THEN
3279       ASM_SIMP_TAC[aff_ge_0_2; IN_ELIM_THM] THEN
3280       REPEAT STRIP_TAC THEN
3281       EXISTS_TAC `x:real^N` THEN
3282       CONJ_TAC THENL
3283       [
3284         EXISTS_TAC `u:real` THEN
3285           ASM_REWRITE_TAC[];
3286         ALL_TAC
3287       ] THEN
3288
3289       MAP_EVERY EXISTS_TAC [`t1:real`; `t2:real`] THEN
3290       FIRST_ASSUM (fun th -> REWRITE_TAC[th]) THEN
3291       ASM_REWRITE_TAC[] THEN
3292
3293       ABBREV_TAC `d = v4 - v2:real^N` THEN
3294       ABBREV_TAC `v = v1 - v2:real^N` THEN
3295       ABBREV_TAC `w = v3 - v2:real^N` THEN
3296
3297       FIRST_X_ASSUM (MP_TAC o check (is_neg o concl)) THEN
3298       REWRITE_TAC[GSYM MEMBER_NOT_EMPTY; IN_INTER; IN_SEGMENT; HALFLINE; IN_ELIM_THM] THEN
3299       DISCH_THEN (X_CHOOSE_THEN `px:real^N` MP_TAC) THEN
3300       DISCH_THEN (CONJUNCTS_THEN2 (X_CHOOSE_THEN `up:real` MP_TAC) (X_CHOOSE_THEN `tp:real` MP_TAC)) THEN
3301       REWRITE_TAC[VECTOR_MUL_RZERO; VECTOR_ADD_LID] THEN
3302       STRIP_TAC THEN POP_ASSUM (LABEL_TAC "px1") THEN
3303       ONCE_REWRITE_TAC[CONJ_ASSOC] THEN
3304       DISCH_THEN (CONJUNCTS_THEN2 ASSUME_TAC (LABEL_TAC "px2")) THEN
3305
3306       SUBGOAL_THEN `(&1 - u) % v + u % w = t2 % d + (&1 - t1 - t2) % (--v2:real^N)` MP_TAC THENL
3307       [
3308         REPLICATE_TAC 4 REMOVE_ASSUM THEN
3309           REPLICATE_TAC 3 (POP_ASSUM (fun th -> REWRITE_TAC[SYM th])) THEN
3310           REWRITE_TAC [VECTOR_ARITH `(&1 - u) % (v1 - v2) + u % (v3 - v2) = ((&1 - u) % v1 + u % v3) - v2:real^N`] THEN
3311           FIRST_X_ASSUM (fun th -> CHANGED_TAC (REWRITE_TAC[SYM th])) THEN
3312           ASM_REWRITE_TAC[] THEN
3313           VECTOR_ARITH_TAC;
3314         ALL_TAC
3315       ] THEN
3316
3317       SUBGOAL_THEN `~(d = vec 0:real^N)` ASSUME_TAC THENL
3318       [
3319         EXPAND_TAC "d" THEN
3320           ASM_REWRITE_TAC[VECTOR_SUB_EQ];
3321         ALL_TAC
3322       ] THEN
3323
3324       DISCH_THEN (MP_TAC o AP_TERM `\v:real^N. projection d v`) THEN
3325       REWRITE_TAC[PROJECTION_LINEAR] THEN
3326       ASM_SIMP_TAC[PROJECTION_ZERO; VECTOR_MUL_RZERO; VECTOR_ADD_LID] THEN
3327
3328       SUBGOAL_THEN `projection d (--v2) dot n = &0 /\ projection d v dot n = v1 dot n /\ projection d w dot n = v3 dot n:real^N` ASSUME_TAC THENL
3329       [
3330         MAP_EVERY EXPAND_TAC ["d"; "v"; "w"] THEN
3331           REWRITE_TAC[projection] THEN
3332           ASM_REWRITE_TAC[DOT_LSUB; DOT_LNEG; DOT_LMUL; REAL_SUB_REFL; REAL_MUL_RZERO] THEN
3333           REAL_ARITH_TAC;
3334         ALL_TAC
3335       ] THEN
3336
3337       DISCH_TAC THEN
3338       FIRST_ASSUM (MP_TAC o AP_TERM `\v:real^N. v dot n`) THEN
3339       USE_THEN "px2" MP_TAC THEN USE_THEN "px1" (fun th -> REWRITE_TAC[th]) THEN
3340       DISCH_THEN (MP_TAC o AP_TERM `\v:real^N. v dot n`) THEN
3341       ASM_REWRITE_TAC[DOT_LADD; DOT_LMUL; REAL_MUL_RZERO] THEN
3342       DISCH_THEN (LABEL_TAC "A" o SYM) THEN DISCH_THEN (LABEL_TAC "B") THEN
3343
3344       SUBGOAL_THEN `u = up:real` ASSUME_TAC THENL
3345       [
3346         MATCH_MP_TAC EQ_TRANS THEN
3347           ABBREV_TAC `a = v1 dot n:real^N` THEN
3348           ABBREV_TAC `b = v3 dot n:real^N` THEN
3349           EXISTS_TAC `a / (a - b)` THEN
3350           SUBGOAL_THEN `~(a - b = &0)` ASSUME_TAC THENL
3351           [
3352             MATCH_MP_TAC (REAL_ARITH `&0 < b + --a ==> ~(a - b = &0)`) THEN
3353               MATCH_MP_TAC REAL_LT_ADD THEN
3354               ASM_REWRITE_TAC[REAL_NEG_GT0];
3355             ALL_TAC
3356           ] THEN
3357
3358           CONJ_TAC THEN MATCH_MP_TAC REAL_EQ_RCANCEL_IMP THEN EXISTS_TAC `a - b:real` THEN REWRITE_TAC[real_div; GSYM REAL_MUL_ASSOC] THEN ASM_SIMP_TAC[REAL_MUL_LINV] THENL
3359           [
3360             REMOVE_THEN "B" MP_TAC THEN REAL_ARITH_TAC;
3361             ALL_TAC
3362           ] THEN
3363           REMOVE_THEN "A" MP_TAC THEN
3364           REAL_ARITH_TAC;
3365         ALL_TAC
3366       ] THEN
3367
3368       REMOVE_THEN "px2" MP_TAC THEN
3369       POP_ASSUM (fun th -> ASM_REWRITE_TAC[SYM th]) THEN
3370       ASM_REWRITE_TAC[VECTOR_MUL_RCANCEL] THEN
3371       UNDISCH_TAC `&0 <= tp` THEN
3372       REAL_ARITH_TAC);;
3373
3374
3375
3376
3377 (* The second rotation lemma for a 4-point configuration *)
3378
3379 let lemma_4_points_rotation2 = prove(`!v1 v2 v3 v4. v1 IN ball_annulus /\ v2 IN ball_annulus /\ v3 IN ball_annulus /\ v4 IN ball_annulus /\
3380                                        dist (v1,v3) <= &2 * h0 /\ dist (v2,v4) <= &2 * h0 /\
3381                                        &2 <= dist (v1,v2) /\ &2 <= dist (v1,v4) /\
3382                                        &2 <= dist (v2,v3) /\ &2 <= dist (v3,v4) /\
3383                                        &2 <= dist (v2,v4) /\
3384                                        ~(segment [v1,v3] INTER convex hull {vec 0,v2,v4} = {})
3385                                        ==> (?v1'. v1' IN ball_annulus /\ norm v1' = &2 /\
3386                                                   dist (v1',v3) <= &2 * h0 /\
3387                                                   dist (v1',v2) = dist (v1,v2) /\
3388                                                   dist (v1',v4) = dist (v1,v4) /\
3389                                                   ~(segment [v1',v3] INTER convex hull {vec 0,v2,v4} = {}))`,
3390    REPEAT STRIP_TAC THEN
3391      SUBGOAL_THEN `?u t2 t4. (&0 <= u /\ u <= &1 /\ &0 <= t2 /\ &0 <= t4 /\ t2 + t4 <= &1) /\ (&1 - u) % (v1 - v2) + u % (v3 - v2) = t4 % (v4 - v2) + (&1 - t2 - t4) % (--v2:real^3)` MP_TAC THENL
3392      [
3393        POP_ASSUM MP_TAC THEN
3394          REWRITE_TAC[GSYM MEMBER_NOT_EMPTY; IN_INTER; IN_SEGMENT; CONVEX_HULL_3_ALT; IN_ELIM_THM] THEN
3395          REWRITE_TAC[VECTOR_SUB_RZERO; VECTOR_ADD_LID] THEN
3396          REPEAT STRIP_TAC THEN
3397          MAP_EVERY EXISTS_TAC [`u:real`; `u':real`; `v:real`] THEN
3398          ASM_REWRITE_TAC[] THEN
3399          REWRITE_TAC[VECTOR_ARITH `(&1 - u) % (v1 - v2) + u % (v3 - v2) = ((&1 - u) % v1 + u % v3) - v2:real^3`] THEN
3400          POP_ASSUM MP_TAC THEN
3401          FIRST_X_ASSUM (fun th -> CHANGED_TAC (REWRITE_TAC[SYM th])) THEN
3402          DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
3403          VECTOR_ARITH_TAC;
3404        ALL_TAC
3405      ] THEN
3406
3407      SUBGOAL_THEN `~collinear {vec 0, v2, v4:real^3} /\ ~(v2 = vec 0) /\ ~(v4 = vec 0)` ASSUME_TAC THENL
3408      [
3409        REPLICATE_TAC 3 (FIRST_X_ASSUM (MP_TAC o check (is_binary "IN" o concl))) THEN
3410          SIMP_TAC[in_ball_annulus] THEN
3411          REPEAT DISCH_TAC THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[] THEN
3412          MATCH_MP_TAC estd_non_collinear_lemma THEN
3413          ASM_REWRITE_TAC[in_ball_annulus];
3414        ALL_TAC
3415      ] THEN
3416
3417      SUBGOAL_THEN `~(segment [v1,v3] INTER aff_ge {vec 0} {v2,v4:real^3} = {})` MP_TAC THENL
3418      [
3419        FIRST_X_ASSUM (MP_TAC o check (is_neg o concl)) THEN
3420          REWRITE_TAC[GSYM MEMBER_NOT_EMPTY; IN_INTER] THEN
3421          STRIP_TAC THEN EXISTS_TAC `x:real^3` THEN ASM_REWRITE_TAC[] THEN
3422          MATCH_MP_TAC Hypermap.lemma_in_subset THEN
3423          EXISTS_TAC `convex hull {vec 0,v2,v4:real^3}` THEN
3424          ASM_REWRITE_TAC[] THEN
3425          ASM_SIMP_TAC[CONVEX_HULL_3_ALT; aff_ge_0_2; SUBSET; IN_ELIM_THM; VECTOR_SUB_RZERO; VECTOR_ADD_LID] THEN
3426          REPEAT STRIP_TAC THEN
3427          MAP_EVERY EXISTS_TAC [`u:real`; `v:real`] THEN
3428          ASM_REWRITE_TAC[];
3429        ALL_TAC
3430      ] THEN
3431
3432      FIRST_X_ASSUM ((fun th -> ALL_TAC) o check (is_neg o concl)) THEN
3433      DISCH_TAC THEN
3434
3435      MAP_EVERY (fun tm -> DISCH_THEN (X_CHOOSE_THEN tm MP_TAC)) [`u:real`; `t2:real`; `t4:real`] THEN
3436      DISCH_THEN (CONJUNCTS_THEN2 ASSUME_TAC (LABEL_TAC "A")) THEN
3437
3438      MP_TAC (SPEC_ALL separation_plane_4_points) THEN
3439      ASM_REWRITE_TAC[] THEN
3440      STRIP_TAC THEN
3441
3442      ABBREV_TAC `v:real^3 = v1 - v2` THEN
3443      ABBREV_TAC `w:real^3 = v3 - v2` THEN
3444      ABBREV_TAC `d:real^3 = v4 - v2` THEN
3445
3446      SUBGOAL_THEN `~(d = vec 0:real^3)` ASSUME_TAC THENL
3447      [
3448        EXPAND_TAC "d" THEN
3449          REWRITE_TAC[GSYM NORM_EQ_0; GSYM dist; DIST_SYM] THEN
3450          ASM_SIMP_TAC[REAL_ARITH `&2 <= a ==> ~(a = &0)`];
3451        ALL_TAC
3452      ] THEN
3453
3454      (* Rotation *)
3455      MP_TAC (ISPECL [`projection d v:real^3`; `projection d w:real^3`; `projection d (--v2):real^3`; `d:real^3`] rotation_lemma_segments) THEN
3456      SUBGOAL_THEN `~(projection d (--v2) = vec 0:real^3)` ASSUME_TAC THENL
3457      [
3458        EXPAND_TAC "d" THEN
3459          REWRITE_TAC[projection] THEN
3460          ABBREV_TAC `k = (--v2 dot (v4 - v2:real^3)) / ((v4 - v2) dot (v4 - v2))` THEN
3461          ASM_CASES_TAC `k = &0` THENL
3462          [
3463            ASM_REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_SUB_RZERO; VECTOR_NEG_EQ_0];
3464            ALL_TAC
3465          ] THEN
3466
3467          DISCH_THEN (MP_TAC o AP_TERM `\v:real^3. inv (k) % v`) THEN
3468          ASM_SIMP_TAC[VECTOR_SUB_LDISTRIB; VECTOR_MUL_ASSOC; REAL_MUL_LINV] THEN
3469          REWRITE_TAC[VECTOR_MUL_LID; VECTOR_MUL_RZERO] THEN
3470          REWRITE_TAC[VECTOR_ARITH `a % (--v2) - (v4 - v2) = vec 0 <=> v4 = (&1 - a) % v2:real^3`] THEN
3471          UNDISCH_TAC `~collinear {vec 0,v2,v4} /\ ~(v2 = vec 0) /\ ~(v4 = vec 0:real^3)` THEN
3472          SIMP_TAC[COLLINEAR_LEMMA_ALT; DE_MORGAN_THM; NOT_EXISTS_THM];
3473        ALL_TAC
3474      ] THEN
3475
3476      ANTS_TAC THENL
3477      [
3478        SUBGOAL_THEN `v dot n = v1 dot n /\ w dot n = v3 dot n /\ d dot n:real^3 = &0` ASSUME_TAC THENL
3479          [
3480            MAP_EVERY EXPAND_TAC ["v"; "w"; "d"] THEN
3481              ASM_REWRITE_TAC[DOT_LSUB; REAL_SUB_RZERO];
3482            ALL_TAC
3483          ] THEN
3484          ASM_REWRITE_TAC[DIMINDEX_3; LE_REFL; PROJECTION_ORTHOGONAL] THEN
3485
3486          CONJ_TAC THENL
3487          [
3488            DISCH_THEN (MP_TAC o AP_TERM `\x:real^3. x dot n`) THEN
3489              REWRITE_TAC[projection] THEN
3490              ASM_REWRITE_TAC[DOT_LSUB; DOT_LMUL; DOT_LZERO; REAL_MUL_RZERO; REAL_SUB_RZERO] THEN
3491              ASM_SIMP_TAC[REAL_ARITH `a < &0 ==> ~(a = &0)`];
3492            ALL_TAC
3493          ] THEN
3494
3495          REWRITE_TAC[GSYM MEMBER_NOT_EMPTY] THEN
3496          REWRITE_TAC[IN_INTER; IN_SEGMENT; VECTOR_MUL_RZERO; VECTOR_ADD_LID] THEN
3497          EXISTS_TAC `(&1 - t2 - t4) % projection d (--v2:real^3)` THEN
3498          CONJ_TAC THENL
3499          [
3500            EXISTS_TAC `&1 - t2 - t4` THEN
3501              ASM_REWRITE_TAC[REAL_ARITH `&0 <= &1 - t2 - t4 <=> t2 + t4 <= &1`] THEN
3502              MATCH_MP_TAC (REAL_ARITH `&0 <= t2 /\ &0 <= t4 ==> &1 - t2 - t4 <= &1`) THEN
3503              ASM_REWRITE_TAC[];
3504            ALL_TAC
3505          ] THEN
3506
3507          EXISTS_TAC `u:real` THEN
3508          ASM_REWRITE_TAC[] THEN
3509          REMOVE_THEN "A" (MP_TAC o AP_TERM `\v:real^3. projection d v`) THEN
3510          REWRITE_TAC[PROJECTION_LINEAR] THEN
3511          ASM_SIMP_TAC[PROJECTION_ZERO; VECTOR_MUL_RZERO; VECTOR_ADD_LID];
3512        ALL_TAC
3513      ] THEN
3514
3515      DISCH_THEN (X_CHOOSE_THEN `g:real^1->real^3` STRIP_ASSUME_TAC) THEN
3516
3517      (* f(t) *)
3518      ABBREV_TAC `f = (\t:real^1. (g t + v - projection d v) + v2:real^3)` THEN
3519
3520      (* f(0) = v1 and (f(1) dot n) = 0 *)
3521      SUBGOAL_THEN `f (lift (&0)) = v1:real^3 /\ f (lift (&1)) dot n = &0` ASSUME_TAC THENL
3522      [
3523        EXPAND_TAC "f" THEN
3524          ASM_REWRITE_TAC[VECTOR_ARITH `pv + v - pv = v:real^3`] THEN
3525          CONJ_TAC THENL
3526          [
3527            EXPAND_TAC "v" THEN VECTOR_ARITH_TAC;
3528            ALL_TAC
3529          ] THEN
3530
3531          REWRITE_TAC[DOT_LADD; DOT_LMUL] THEN
3532          SUBGOAL_THEN `d dot n:real^3 = &0` ASSUME_TAC THENL [ EXPAND_TAC "d" THEN ASM_REWRITE_TAC[DOT_LSUB; REAL_SUB_RZERO]; ALL_TAC ] THEN
3533          SUBGOAL_THEN `(v - projection d v) dot n:real^3 = &0` (fun th -> REWRITE_TAC[th]) THENL
3534          [
3535            GEN_REWRITE_TAC (PAT_CONV `\x:real^3. (x - y) dot z = &0`) [VECTOR_PROJECTION] THEN
3536              REWRITE_TAC[VECTOR_ARITH `(a + b) - a = b:real^3`] THEN
3537              ASM_REWRITE_TAC[DOT_LMUL; REAL_MUL_RZERO];
3538            ALL_TAC
3539          ] THEN
3540
3541          ASM_REWRITE_TAC[projection; DOT_LSUB; DOT_LMUL; DOT_LNEG; REAL_MUL_RZERO; REAL_SUB_LZERO; REAL_NEG_0; REAL_ADD_LID];
3542        ALL_TAC
3543      ] THEN
3544
3545      (* d(f(t), v2) = d(v1, v2) *)
3546      SUBGOAL_THEN `!t. dist (f (t:real^1), v2:real^3) = dist (v1, v2) /\ dist (f t, v4) = dist (v1, v4)` ASSUME_TAC THENL
3547      [
3548        GEN_TAC THEN EXPAND_TAC "f" THEN
3549          REWRITE_TAC[dist; VECTOR_ARITH `(a + b) - b = a:real^3 - vec 0`] THEN
3550          REWRITE_TAC[VECTOR_ARITH `((a + b - c) + v2) - v4 = (a + b - c) - (v4 - v2:real^3)`] THEN
3551          REWRITE_TAC[GSYM dist; DIST_EQ] THEN
3552          ASM_SIMP_TAC[PROJECTION_DIST_SPECIAL_EQ; PROJECTION_ZERO] THEN
3553          ASM_REWRITE_TAC[PROJECTION_0; DIST_0] THEN
3554          EXPAND_TAC "v" THEN EXPAND_TAC "d" THEN REWRITE_TAC[dist] THEN
3555          REWRITE_TAC[VECTOR_ARITH `v1 - v2 - (v4 - v2) = v1 - v4:real^3`] THEN
3556          REAL_ARITH_TAC;
3557        ALL_TAC
3558      ] THEN
3559
3560      (* d(f(t), v3) <= d(v1,v3) <= 2 h0 *)
3561      SUBGOAL_THEN `!t. &0 <= t /\ t <= &1 ==> dist (f (lift t), v3:real^3) <= &2 * h0` MP_TAC THENL
3562      [
3563        REPEAT STRIP_TAC THEN
3564          MATCH_MP_TAC REAL_LE_TRANS THEN
3565          EXISTS_TAC `dist (v1,v3:real^3)` THEN
3566          ASM_REWRITE_TAC[] THEN
3567          EXPAND_TAC "f" THEN
3568          REWRITE_TAC[dist] THEN
3569          ASM_REWRITE_TAC[VECTOR_ARITH `((g + v - pv) + v2) - v3:real^3 = (g + v - pv) - (v3 - v2)`] THEN
3570          GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV) [VECTOR_ARITH `v1 - v3 = (v1 - v2) - (v3 - v2:real^3)`] THEN
3571          ASM_REWRITE_TAC[] THEN
3572          REWRITE_TAC[GSYM dist] THEN
3573          MATCH_MP_TAC PROJECTION_DIST_SPECIAL_LE THEN
3574          ASM_SIMP_TAC[];
3575        ALL_TAC
3576      ] THEN
3577
3578      (* |f(t)| <= |v1| *)
3579      SUBGOAL_THEN `!t. &0 <= t /\ t <= &1 ==> norm (f (lift t):real^3) <= norm (v1:real^3)` MP_TAC THENL
3580      [
3581        REPEAT STRIP_TAC THEN
3582          EXPAND_TAC "f" THEN
3583          ASM_REWRITE_TAC[VECTOR_ARITH `(g + v - pv) + v2:real^3 = (g + v - pv) - (--v2)`] THEN
3584          GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV) [VECTOR_ARITH `v1 = (v1 - v2) - (--v2:real^3)`] THEN
3585          ASM_REWRITE_TAC[] THEN
3586          REWRITE_TAC[GSYM dist] THEN
3587          MATCH_MP_TAC PROJECTION_DIST_SPECIAL_LE THEN
3588          ASM_SIMP_TAC[];
3589        ALL_TAC
3590      ] THEN
3591
3592      REPEAT DISCH_TAC THEN
3593
3594      (* If 2 <= |f(t)|, then f IN ball_annulus *)
3595      SUBGOAL_THEN `!t. &0 <= t /\ t <= &1 /\ &2 <= norm (f (lift t):real^3) ==> f (lift t) IN ball_annulus` ASSUME_TAC THENL
3596      [
3597        REPEAT STRIP_TAC THEN
3598          ASM_SIMP_TAC[in_ball_annulus; GSYM NORM_EQ_0; REAL_ARITH `&2 <= a ==> ~(a = &0)`] THEN
3599          MATCH_MP_TAC REAL_LE_TRANS THEN
3600          EXISTS_TAC `norm (v1:real^3)` THEN
3601          ASM_SIMP_TAC[] THEN
3602          UNDISCH_TAC `v1 IN ball_annulus` THEN
3603          SIMP_TAC[in_ball_annulus];
3604        ALL_TAC
3605      ] THEN
3606
3607      SUBGOAL_THEN `f:real^1->real^3 continuous_on interval [lift (&0), lift (&1)]` ASSUME_TAC THENL
3608      [
3609        EXPAND_TAC "f" THEN
3610          REPEAT (MATCH_MP_TAC CONTINUOUS_ON_ADD THEN REWRITE_TAC[CONTINUOUS_ON_CONST]) THEN
3611          MATCH_MP_TAC CONTINUOUS_ON_SUBSET THEN
3612          EXISTS_TAC `UNIV:real^1->bool` THEN
3613          ASM_REWRITE_TAC[SUBSET_UNIV];
3614        ALL_TAC
3615      ] THEN
3616
3617      REPLICATE_TAC 2 (FIRST_X_ASSUM (MP_TAC o check (free_in `g:real^1->real^3` o concl))) THEN
3618      SUBGOAL_THEN `!t:real^1. projection d (g t) = (g t):real^3` MP_TAC THENL
3619      [
3620        GEN_TAC THEN REWRITE_TAC[projection] THEN
3621          ASM_REWRITE_TAC[real_div; REAL_MUL_LZERO; VECTOR_MUL_LZERO; VECTOR_SUB_RZERO];
3622        ALL_TAC
3623      ] THEN
3624
3625      REPEAT (FIRST_X_ASSUM ((fun th -> ALL_TAC) o check (free_in `g:real^1->real^3` o concl))) THEN
3626      REPEAT DISCH_TAC THEN
3627
3628      ASM_CASES_TAC `!h. &0 <= h /\ h <= &1 ==> &2 <= norm (f (lift h):real^3)` THENL
3629      [
3630        MATCH_MP_TAC (TAUT `F ==> A`) THEN
3631          MP_TAC (SPECL [`v2:real^3`; `v4:real^3`; `f:real^1->real^3`; `v3:real^3`; `&1`] continuous_lemma_aff_ge) THEN
3632          ANTS_TAC THENL
3633          [
3634            ASM_REWRITE_TAC[REAL_LE_01] THEN
3635              GEN_TAC THEN DISCH_TAC THEN
3636              SUBGOAL_THEN `t:real^1 = lift (drop t)` (fun th -> ONCE_REWRITE_TAC[th]) THENL [ REWRITE_TAC[LIFT_DROP]; ALL_TAC ] THEN
3637              SUBGOAL_THEN `&0 <= drop (t:real^1) /\ drop t <= &1` ASSUME_TAC THENL
3638              [
3639                ASM_REWRITE_TAC[GSYM IN_INTERVAL_1; LIFT_DROP];
3640                ALL_TAC
3641              ] THEN
3642              MATCH_MP_TAC zero_not_between_estd THEN
3643              ASM_SIMP_TAC[];
3644            ALL_TAC
3645          ] THEN
3646
3647          DISCH_THEN DISJ_CASES_TAC THENL
3648          [
3649            MP_TAC (ISPECL [`v2:real^3`; `v4:real^3`; `f (lift (&1)):real^3`; `v3:real^3`; `n:real^3`] segment_inter_aff_ge_ends) THEN
3650              ASM_SIMP_TAC[REAL_ARITH `&0 < a ==> ~(a = &0)`; IN_INTERVAL_1; REAL_LE_REFL; REAL_LE_01] THEN
3651              DISCH_TAC THEN
3652              MATCH_MP_TAC LEMMA_3_POINTS_FINAL THEN
3653              MAP_EVERY EXISTS_TAC [`v2:real^3`; `v4:real^3`; `f (lift (&1)):real^3`] THEN
3654              ASM_SIMP_TAC[DIST_SYM; REAL_LE_REFL; REAL_LE_01];
3655            ALL_TAC
3656          ] THEN
3657
3658          POP_ASSUM MP_TAC THEN STRIP_TAC THEN MATCH_MP_TAC LEMMA_3_POINTS_FINAL THENL
3659          [
3660            MAP_EVERY EXISTS_TAC [`v2:real^3`; `v4:real^3`; `f (lift x):real^3`] THEN
3661              ASM_SIMP_TAC[DIST_SYM];
3662            MAP_EVERY EXISTS_TAC [`f (lift x):real^3`; `v3:real^3`; `v2:real^3`] THEN
3663              ASM_SIMP_TAC[DIST_SYM];
3664            MAP_EVERY EXISTS_TAC [`f (lift x):real^3`; `v3:real^3`; `v4:real^3`] THEN
3665              ASM_SIMP_TAC[DIST_SYM]
3666          ];
3667        ALL_TAC
3668      ] THEN
3669
3670      (* ?h. f(h) <= 2 *)
3671      POP_ASSUM MP_TAC THEN REWRITE_TAC[NOT_FORALL_THM; NOT_IMP; REAL_NOT_LE] THEN
3672      DISCH_THEN (CHOOSE_THEN ASSUME_TAC) THEN
3673
3674      SUBGOAL_THEN `?s. &0 <= s /\ s <= &1 /\ norm (f (lift s):real^3) = &2 /\ (!t. &0 <= t /\ t <= s ==> &2 <= norm (f (lift t)))` MP_TAC THENL
3675      [
3676        MP_TAC (SPECL [`\t:real. norm (f (lift t):real^3)`; `&2`; `h:real`] continuous_lemma_dec) THEN
3677          ANTS_TAC THENL
3678          [
3679            ASM_SIMP_TAC[REAL_LT_IMP_LE] THEN
3680              UNDISCH_TAC `v1 IN ball_annulus` THEN
3681              SIMP_TAC[in_ball_annulus] THEN DISCH_TAC THEN
3682              REWRITE_TAC[REAL_CONTINUOUS_ON; IMAGE_LIFT_REAL_INTERVAL] THEN
3683              SUBGOAL_THEN `lift o (\t. norm (f (lift t):real^3)) o drop = (lift o norm) o f` (fun th -> REWRITE_TAC[th]) THENL
3684              [
3685                REWRITE_TAC[FUN_EQ_THM; o_THM; LIFT_DROP];
3686                ALL_TAC
3687              ] THEN
3688              MATCH_MP_TAC CONTINUOUS_ON_COMPOSE THEN
3689              REWRITE_TAC[CONTINUOUS_ON_LIFT_NORM] THEN
3690              MATCH_MP_TAC CONTINUOUS_ON_SUBSET THEN
3691              EXISTS_TAC `interval [lift (&0), lift (&1)]` THEN
3692              ASM_REWRITE_TAC[SUBSET_INTERVAL_1; LIFT_DROP; REAL_LE_REFL];
3693            ALL_TAC
3694          ] THEN
3695
3696          BETA_TAC THEN STRIP_TAC THEN
3697          EXISTS_TAC `x:real` THEN
3698          ASM_REWRITE_TAC[] THEN
3699          CONJ_TAC THENL [ MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `h:real` THEN ASM_REWRITE_TAC[]; ALL_TAC ] THEN
3700          REPEAT STRIP_TAC THEN
3701          ASM_CASES_TAC `t = x:real` THENL [ ASM_REWRITE_TAC[REAL_LE_REFL]; ALL_TAC ] THEN
3702          MATCH_MP_TAC REAL_LT_IMP_LE THEN
3703          FIRST_X_ASSUM MATCH_MP_TAC THEN
3704          ASM_REWRITE_TAC[REAL_LT_LE];
3705        ALL_TAC
3706      ] THEN
3707      STRIP_TAC THEN
3708      SUBGOAL_THEN `!t. t <= s ==> t <= &1` ASSUME_TAC THENL
3709      [
3710        REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_LE_TRANS THEN
3711          EXISTS_TAC `s:real` THEN ASM_REWRITE_TAC[];
3712        ALL_TAC
3713      ] THEN
3714
3715      (* The main step *)
3716      MP_TAC (SPECL [`v2:real^3`; `v4:real^3`; `f:real^1->real^3`; `v3:real^3`; `s:real`] continuous_lemma_aff_ge) THEN
3717      ANTS_TAC THENL
3718      [
3719        ASM_REWRITE_TAC[] THEN
3720          CONJ_TAC THENL
3721          [
3722            MATCH_MP_TAC CONTINUOUS_ON_SUBSET THEN
3723              EXISTS_TAC `interval [lift (&0), lift (&1)]` THEN
3724              ASM_REWRITE_TAC[SUBSET_INTERVAL_1; LIFT_DROP; REAL_LE_REFL];
3725            ALL_TAC
3726          ] THEN
3727
3728          GEN_TAC THEN DISCH_TAC THEN
3729          SUBGOAL_THEN `t:real^1 = lift (drop t)` (fun th -> ONCE_REWRITE_TAC[th]) THENL [ REWRITE_TAC[LIFT_DROP]; ALL_TAC ] THEN
3730          SUBGOAL_THEN `&0 <= drop (t:real^1) /\ drop t <= s` ASSUME_TAC THENL
3731          [
3732            ASM_REWRITE_TAC[GSYM IN_INTERVAL_1; LIFT_DROP];
3733            ALL_TAC
3734          ] THEN
3735          MATCH_MP_TAC zero_not_between_estd THEN
3736          ASM_SIMP_TAC[];
3737        ALL_TAC
3738      ] THEN
3739
3740      ONCE_REWRITE_TAC[DISJ_SYM] THEN
3741      DISCH_THEN DISJ_CASES_TAC THENL
3742      [
3743        MATCH_MP_TAC (TAUT `F ==> A`) THEN
3744          POP_ASSUM MP_TAC THEN STRIP_TAC THEN MATCH_MP_TAC LEMMA_3_POINTS_FINAL THENL
3745          [
3746            MAP_EVERY EXISTS_TAC [`v2:real^3`; `v4:real^3`; `f (lift x):real^3`] THEN
3747              ASM_SIMP_TAC[DIST_SYM];
3748            MAP_EVERY EXISTS_TAC [`f (lift x):real^3`; `v3:real^3`; `v2:real^3`] THEN
3749              ASM_SIMP_TAC[DIST_SYM];
3750            MAP_EVERY EXISTS_TAC [`f (lift x):real^3`; `v3:real^3`; `v4:real^3`] THEN
3751              ASM_SIMP_TAC[DIST_SYM]
3752          ];
3753        ALL_TAC
3754      ] THEN
3755
3756      EXISTS_TAC `f (lift s):real^3` THEN
3757      ASM_SIMP_TAC[REAL_LE_REFL] THEN
3758
3759      (* [f(s), v3] INTER convex hull {0,v2,v4} *)
3760      MATCH_MP_TAC segment_inter_conv THEN
3761      ASM_REWRITE_TAC[] THEN
3762
3763      MP_TAC (SPECL [`f (lift s):real^3`; `v2:real^3`; `v3:real^3`; `v4:real^3`] separation_plane_4_points) THEN
3764      ANTS_TAC THENL
3765      [
3766        ASM_SIMP_TAC[REAL_LE_REFL] THEN
3767          FIRST_X_ASSUM MATCH_MP_TAC THEN
3768          ASM_REWRITE_TAC[IN_INTERVAL_1; REAL_LE_REFL];
3769        ALL_TAC
3770      ] THEN
3771
3772      REPEAT (FIRST_X_ASSUM ((fun th -> ALL_TAC) o check (free_in `n:real^3` o concl))) THEN
3773      STRIP_TAC THEN
3774      EXISTS_TAC `n:real^3` THEN
3775      ASM_REWRITE_TAC[] THEN
3776      CONJ_TAC THENL
3777      [
3778        ONCE_REWRITE_TAC[VECTOR_ARITH `v2 = v4:real^3 <=> v4 - v2 = vec 0`] THEN
3779          ASM_REWRITE_TAC[];
3780        ALL_TAC
3781      ] THEN
3782
3783      CONJ_TAC THENL
3784      [
3785        FIRST_X_ASSUM MATCH_MP_TAC THEN
3786          ASM_REWRITE_TAC[IN_INTERVAL_1; REAL_LE_REFL];
3787        ALL_TAC
3788      ] THEN
3789
3790      SUBGOAL_THEN `projection d (f (lift s) - v2:real^3) = projection d (g (lift s))` (fun th -> REWRITE_TAC[th]) THENL
3791      [
3792        EXPAND_TAC "f" THEN
3793          REWRITE_TAC[VECTOR_ARITH `(a + v2) - v2 = a:real^3`] THEN
3794          REWRITE_TAC[PROJECTION_LINEAR] THEN
3795          SUBGOAL_THEN `?a. v - projection d v = a % d:real^3` MP_TAC THENL
3796          [
3797            EXISTS_TAC `(v dot d:real^3) / (d dot d)` THEN
3798              REWRITE_TAC[projection] THEN
3799              VECTOR_ARITH_TAC;
3800            ALL_TAC
3801          ] THEN
3802          STRIP_TAC THEN
3803          ASM_SIMP_TAC[PROJECTION_LINEAR; PROJECTION_ZERO; VECTOR_MUL_RZERO; VECTOR_ADD_RID];
3804        ALL_TAC
3805      ] THEN
3806
3807      ASM_SIMP_TAC[]);;
3808
3809
3810
3811 (******************************************************************)
3812
3813
3814 let lemma_4_points_rotation2_full = prove(`!v1 v2 v3 v4. v1 IN ball_annulus /\ v2 IN ball_annulus /\ v3 IN ball_annulus /\ v4 IN ball_annulus /\
3815                                             dist (v1,v3) <= &2 * h0 /\ dist (v2,v4) <= &2 * h0 /\
3816                                             &2 <= dist (v1,v2) /\ &2 <= dist (v1,v4) /\
3817                                             &2 <= dist (v2,v3) /\ &2 <= dist (v3,v4) /\
3818                                             &2 <= dist (v2,v4) /\
3819                                             ~(segment [v1,v3] INTER convex hull {vec 0, v2, v4} = {})
3820                                             ==> (?v1' v3'. v1' IN ball_annulus /\ v3' IN ball_annulus /\
3821                                                    norm v1' = &2 /\ norm v3' = &2 /\
3822                                                    dist (v1',v3') <= &2 * h0 /\
3823                                                    dist (v1',v2) = dist (v1,v2) /\ dist (v1',v4) = dist (v1,v4) /\
3824                                                    dist (v2,v3') = dist (v2,v3) /\ dist (v3',v4) = dist (v3,v4) /\
3825                                                    ~(segment [v1',v3'] INTER aff_ge {vec 0} {v2, v4} = {}))`,
3826    REPEAT STRIP_TAC THEN
3827      (* v1 about v2-v4 *)
3828      MP_TAC (SPEC_ALL lemma_4_points_rotation2) THEN
3829      ASM_REWRITE_TAC[] THEN
3830      STRIP_TAC THEN
3831      EXISTS_TAC `v1':real^3` THEN
3832      ASM_REWRITE_TAC[] THEN
3833
3834      (* v3 about v2-v4 *)
3835      MP_TAC (SPECL [`v3:real^3`; `v2:real^3`; `v1':real^3`; `v4:real^3`] lemma_4_points_rotation2) THEN
3836      ASM_REWRITE_TAC[REAL_LE_REFL; DIST_SYM; SEGMENT_SYM] THEN
3837      DISCH_THEN (X_CHOOSE_THEN `v3':real^3` MP_TAC) THEN REWRITE_TAC[DIST_SYM] THEN
3838      STRIP_TAC THEN
3839      EXISTS_TAC `v3':real^3` THEN
3840      ASM_REWRITE_TAC[DIST_SYM] THEN
3841
3842      POP_ASSUM MP_TAC THEN
3843      REWRITE_TAC[GSYM MEMBER_NOT_EMPTY; IN_INTER] THEN
3844      STRIP_TAC THEN
3845      EXISTS_TAC `x:real^3` THEN ASM_REWRITE_TAC[] THEN
3846      MATCH_MP_TAC Hypermap.lemma_in_subset THEN
3847      EXISTS_TAC `convex hull {vec 0, v2, v4:real^3}` THEN
3848      ASM_REWRITE_TAC[] THEN
3849      UNDISCH_TAC `v2 IN ball_annulus` THEN
3850      UNDISCH_TAC `v4 IN ball_annulus` THEN
3851      SIMP_TAC[in_ball_annulus; aff_ge_0_2] THEN
3852      REPEAT DISCH_TAC THEN
3853      REWRITE_TAC[SUBSET; CONVEX_HULL_3_ALT; IN_ELIM_THM; VECTOR_SUB_RZERO; VECTOR_ADD_LID] THEN
3854      REPEAT STRIP_TAC THEN
3855      MAP_EVERY EXISTS_TAC [`u:real`; `v:real`] THEN
3856      ASM_REWRITE_TAC[]);;
3857
3858
3859
3860
3861 (******************************************************************************************)
3862
3863
3864 (* Prove that a certain configuration of 4 points is impossible *)
3865
3866 let lemma_4_points_circumcenter = prove(`!v1 v2 v3 v4. ~(collinear {vec 0,v2,v4}) /\
3867                                           v2 IN ball_annulus /\ v4 IN ball_annulus /\
3868                                           ~(segment [v1,v3] INTER aff_ge {vec 0} {v2,v4} = {}) /\
3869                                           norm v1 = &2 /\ norm v3 = &2 /\
3870                                           dist (v1,v2) = &2 /\ dist (v1,v4) = &2 /\
3871                                           dist (v3,v2) = &2 /\ dist (v3,v4) = &2
3872                                               ==> norm(v1 + v3) = &2 * eta_y (norm v2) (norm v4) (dist (v2,v4))`,
3873   REWRITE_TAC[in_ball_annulus] THEN
3874     REPEAT STRIP_TAC THEN
3875     SUBGOAL_THEN `!v w:real^3. norm v = &2 /\ dist (v,w) = &2 ==> v dot w = norm w pow 2 / &2` ASSUME_TAC THENL
3876     [
3877       REWRITE_TAC[DIST_SQR; REAL_ARITH `&0 <= &2`] THEN
3878         REWRITE_TAC[dist; NORM_POW_2] THEN
3879         REWRITE_TAC[DOT_LSUB; DOT_RSUB; DOT_SQUARE_NORM; DOT_SYM] THEN
3880         REPEAT GEN_TAC THEN
3881         STRIP_TAC THEN POP_ASSUM MP_TAC THEN
3882         ASM_REWRITE_TAC[] THEN
3883         REAL_ARITH_TAC;
3884       ALL_TAC
3885     ] THEN
3886     FIRST_ASSUM (MP_TAC o SPECL [`v1:real^3`; `v2:real^3`]) THEN
3887     FIRST_ASSUM (MP_TAC o SPECL [`v1:real^3`; `v4:real^3`]) THEN
3888     FIRST_ASSUM (MP_TAC o SPECL [`v3:real^3`; `v2:real^3`]) THEN
3889     FIRST_X_ASSUM (MP_TAC o SPECL [`v3:real^3`; `v4:real^3`]) THEN
3890     ASM_REWRITE_TAC[DOT_SYM] THEN
3891     REPEAT STRIP_TAC THEN
3892
3893     ABBREV_TAC `v = inv(&2) % (v1 + v3:real^3)` THEN
3894
3895     SUBGOAL_THEN `v:real^3 IN affine hull {vec 0,v2,v4}` ASSUME_TAC THENL
3896     [
3897       FIRST_X_ASSUM (MP_TAC o check (is_neg o concl)) THEN
3898         REWRITE_TAC[GSYM MEMBER_NOT_EMPTY] THEN
3899         REWRITE_TAC[IN_INTER; IN_SEGMENT] THEN
3900         ASM_SIMP_TAC[aff_ge_0_2; IN_ELIM_THM] THEN
3901         STRIP_TAC THEN
3902         SUBGOAL_THEN `x:real^3 dot v1 = x dot v3` MP_TAC THENL
3903         [
3904           POP_ASSUM (fun th -> REWRITE_TAC[th]) THEN
3905             ASM_REWRITE_TAC[DOT_LADD; DOT_LMUL; DOT_SYM];
3906           ALL_TAC
3907         ] THEN
3908         POP_ASSUM (LABEL_TAC "A" o SYM) THEN
3909         ASM_REWRITE_TAC[DOT_LADD; DOT_LMUL] THEN
3910         ASM_REWRITE_TAC[DOT_SYM; DOT_SQUARE_NORM; REAL_ARITH `&2 pow 2 = &4`] THEN
3911         ONCE_REWRITE_TAC[REAL_ARITH `a = b <=> a - b = &0`] THEN
3912         REWRITE_TAC[REAL_ARITH `((&1 - u) * &4 + u * a13) - ((&1 - u) * a13 + u * &4) = &2 * u * (a13 - &4) - (a13 - &4)`] THEN
3913
3914         ASM_CASES_TAC `v1:real^3 dot v3 = &4` THENL
3915         [
3916           DISCH_THEN (fun th -> ALL_TAC) THEN
3917             SUBGOAL_THEN `norm (v3) % v1:real^3 = norm (v1) % v3` MP_TAC THENL
3918             [
3919               REWRITE_TAC[GSYM NORM_CAUCHY_SCHWARZ_EQ] THEN
3920                 ASM_REWRITE_TAC[DOT_SYM] THEN
3921                 REAL_ARITH_TAC;
3922               ALL_TAC
3923             ] THEN
3924             ASM_REWRITE_TAC[VECTOR_ARITH `&2 % v1 = &2 % v3 <=> v1 = v3`] THEN
3925             DISCH_TAC THEN UNDISCH_TAC `x = (&1 - u) % v1 + u % v3:real^3` THEN
3926             EXPAND_TAC "v" THEN
3927             POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN
3928             REWRITE_TAC[VECTOR_ARITH `(&1 - u) % v1 + u % v1 = v1:real^3`] THEN
3929             EXPAND_TAC "x" THEN
3930             REWRITE_TAC[VECTOR_ARITH `inv(&2) % (v1 + v1) = v1:real^3`] THEN
3931             DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN
3932             REWRITE_TAC[AFFINE_HULL_3; IN_ELIM_THM] THEN
3933             MAP_EVERY EXISTS_TAC [`&1 - t1 - t2`; `t1:real`; `t2:real`] THEN
3934             CONJ_TAC THENL [ REAL_ARITH_TAC; ALL_TAC ] THEN
3935             VECTOR_ARITH_TAC;
3936           ALL_TAC
3937         ] THEN
3938
3939         DISCH_TAC THEN
3940         SUBGOAL_THEN `u = inv(&2)` ASSUME_TAC THENL
3941         [
3942           POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN
3943             CONV_TAC REAL_FIELD;
3944           ALL_TAC
3945         ] THEN
3946
3947         SUBGOAL_THEN `v = x:real^3` (fun th -> REWRITE_TAC[th]) THENL
3948         [
3949           ASM_REWRITE_TAC[] THEN
3950             EXPAND_TAC "v" THEN
3951             VECTOR_ARITH_TAC;
3952           ALL_TAC
3953         ] THEN
3954
3955         EXPAND_TAC "x" THEN
3956         REWRITE_TAC[AFFINE_HULL_3; IN_ELIM_THM] THEN
3957         MAP_EVERY EXISTS_TAC [`&1 - t1 - t2`; `t1:real`; `t2:real`] THEN
3958         CONJ_TAC THENL [ REAL_ARITH_TAC; ALL_TAC ] THEN
3959         VECTOR_ARITH_TAC;
3960       ALL_TAC
3961     ] THEN
3962
3963     SUBGOAL_THEN `dist (v:real^3,v2) = norm v /\ dist (v,v4) = norm v` ASSUME_TAC THENL
3964     [
3965       REWRITE_TAC[DIST_SQR] THEN
3966         REWRITE_TAC[dist; NORM_POS_LE; NORM_POW_2] THEN
3967         REWRITE_TAC[DOT_LSUB; DOT_RSUB] THEN
3968         REWRITE_TAC[REAL_ARITH `a - b - c = a <=> b + c = &0`] THEN
3969         EXPAND_TAC "v" THEN
3970         REWRITE_TAC[DOT_LMUL; DOT_RMUL; DOT_LADD; DOT_RADD] THEN
3971         ASM_REWRITE_TAC[DOT_SYM; DOT_SQUARE_NORM] THEN
3972         REAL_ARITH_TAC;
3973       ALL_TAC
3974     ] THEN
3975
3976     SUBGOAL_THEN `v:real^3 = circumcenter {vec 0,v2,v4}` ASSUME_TAC THENL
3977     [
3978       MATCH_MP_TAC (GEN_ALL Collect_geom.DIST_EQ_IS_UNIQUE) THEN
3979         MAP_EVERY EXISTS_TAC [`v2:real^3`; `v4:real^3`; `vec 0:real^3`] THEN
3980         ASM_REWRITE_TAC[DIST_0] THEN
3981         MP_TAC (SPECL [`vec 0:real^3`; `v2:real^3`; `v4:real^3`] Collect_geom.CIRCUMCENTER_PROPTIES) THEN
3982         ASM_REWRITE_TAC[] THEN
3983         STRIP_TAC THEN
3984         FIRST_ASSUM (MP_TAC o SPEC `vec 0:real^3`) THEN
3985         SIMP_TAC[IN_INSERT; DIST_0] THEN
3986         DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN
3987         FIRST_ASSUM (MP_TAC o SPEC `v2:real^3`) THEN
3988         FIRST_ASSUM (MP_TAC o SPEC `v4:real^3`) THEN
3989         SIMP_TAC[IN_INSERT] THEN
3990         REPEAT (DISCH_THEN (fun th -> ALL_TAC)) THEN
3991         REWRITE_TAC[SUBSET; IN_INSERT; NOT_IN_EMPTY] THEN
3992         GEN_TAC THEN
3993         STRIP_TAC THEN ASM_REWRITE_TAC[];
3994       ALL_TAC
3995     ] THEN
3996
3997     SUBGOAL_THEN `norm (v:real^3) = radV {vec 0,v2,v4:real^3}` ASSUME_TAC THENL
3998     [
3999       ASM_REWRITE_TAC[GSYM DIST_0; DIST_SYM] THEN
4000         MP_TAC (GEN_ALL Collect_geom.NOT_COL_IMP_RADV_PROPERTIY) THEN
4001         DISCH_THEN (MP_TAC o SPECL [`vec 0:real^3`; `v2:real^3`; `v4:real^3`]) THEN
4002         ASM_REWRITE_TAC[] THEN
4003         DISCH_THEN (MATCH_MP_TAC o GSYM) THEN
4004         ONCE_REWRITE_TAC[GSYM IN] THEN
4005         REWRITE_TAC[IN_INSERT];
4006       ALL_TAC
4007     ] THEN
4008
4009     POP_ASSUM MP_TAC THEN
4010     MP_TAC (SPECL [`v4:real^3`; `v2:real^3`; `vec 0:real^3`; `norm (v2:real^3)`; `norm (v4:real^3)`; `dist (v2:real^3,v4:real^3)`] Collect_geom.CDEUSDF) THEN
4011     REWRITE_TAC[Collect_geom.dist3; DIST_0; DIST_SYM] THEN
4012     SUBGOAL_THEN `{v4,v2,vec 0:real^3} = {vec 0,v2,v4}` (fun th -> ONCE_REWRITE_TAC[th]) THENL
4013     [
4014       SET_TAC[];
4015       ALL_TAC
4016     ] THEN
4017     REMOVE_ASSUM THEN
4018     ASM_REWRITE_TAC[] THEN
4019     REPLICATE_TAC 2 (DISCH_THEN (CONJUNCTS_THEN2 (fun th -> ALL_TAC) MP_TAC)) THEN
4020     DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
4021     DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN
4022     EXPAND_TAC "v" THEN
4023     REWRITE_TAC[NORM_MUL] THEN
4024     REAL_ARITH_TAC);;
4025
4026
4027
4028 let PARALLELOGRAM_LAW = prove(`!v1 v2:real^N. &2 * (norm v1 pow 2 + norm v2 pow 2) = norm (v1 + v2) pow 2 + norm (v1 - v2) pow 2`,
4029    REPEAT GEN_TAC THEN
4030      REWRITE_TAC[NORM_POW_2] THEN
4031      VECTOR_ARITH_TAC);;
4032
4033
4034
4035 let lemma_4_points_contradiction = prove(`!v1 v2 v3 v4.
4036                                            v2 IN ball_annulus /\ v4 IN ball_annulus /\
4037                                            &2 <= dist (v2,v4) /\ dist (v2,v4) <= &2 * h0 /\
4038                                            ~(segment [v1,v3] INTER aff_ge {vec 0} {v2, v4} = {}) /\
4039                                            norm v1 = &2 /\ norm v3 = &2 /\
4040                                            dist (v1,v2) = &2 /\ dist (v1,v4) = &2 /\
4041                                            dist (v3,v2) = &2 /\ dist (v3,v4) = &2 /\
4042                                            dist (v1,v3) <= &2 * h0
4043                                              ==> F`,
4044    REPEAT STRIP_TAC THEN
4045      SUBGOAL_THEN `~collinear {vec 0:real^3,v2,v4}` ASSUME_TAC THENL
4046      [
4047        MATCH_MP_TAC estd_non_collinear_lemma THEN
4048          ASM_REWRITE_TAC[];
4049        ALL_TAC
4050      ] THEN
4051      MP_TAC (SPEC_ALL lemma_4_points_circumcenter) THEN
4052      ASM_REWRITE_TAC[] THEN
4053      DISCH_TAC THEN
4054      MP_TAC (ISPECL [`v1:real^3`; `v3:real^3`] PARALLELOGRAM_LAW) THEN
4055      ASM_REWRITE_TAC[GSYM dist] THEN
4056      MATCH_MP_TAC (REAL_ARITH `a < b ==> ~(b = a)`) THEN
4057      CONV_TAC REAL_RAT_REDUCE_CONV THEN
4058      ONCE_REWRITE_TAC[REAL_ARITH `&16 = (&16 - (&2 * h0) pow 2) + (&2 * h0) pow 2`] THEN
4059      MATCH_MP_TAC REAL_LTE_ADD2 THEN
4060      CONJ_TAC THENL
4061      [
4062        MATCH_MP_TAC REAL_LET_TRANS THEN
4063          EXISTS_TAC `&4 * #2.2` THEN
4064          CONJ_TAC THENL
4065          [
4066            REWRITE_TAC[REAL_POW_MUL] THEN
4067              MATCH_MP_TAC REAL_LE_MUL2 THEN
4068              ASM_REWRITE_TAC[Collect_geom.REAL_LE_POW_2; REAL_ARITH `&2 pow 2 <= &4`] THEN
4069
4070              MP_TAC Tame_inequalities.ETA_Y_4_POINTS_INEQ THEN
4071
4072              REWRITE_TAC[Tame_inequalities.INEQ_ALT; ALL] THEN
4073              DISCH_THEN MATCH_MP_TAC THEN
4074              REPEAT (FIRST_X_ASSUM (MP_TAC o check (is_binary "IN" o concl))) THEN
4075              ASM_SIMP_TAC[in_ball_annulus];
4076            ALL_TAC
4077          ] THEN
4078          REWRITE_TAC[Sphere.h0] THEN
4079          REAL_ARITH_TAC;
4080        ALL_TAC
4081      ] THEN
4082
4083      REWRITE_TAC[GSYM REAL_LE_SQUARE_ABS] THEN
4084      REWRITE_TAC[dist; REAL_ABS_NORM] THEN
4085      REWRITE_TAC[GSYM dist] THEN
4086      UNDISCH_TAC `dist(v1,v3:real^3) <= &2 * h0` THEN
4087      REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);;
4088
4089
4090
4091 (* The final result *)
4092
4093 let LEMMA_4_POINTS_FINAL = prove(`!v1 v2 v3 v4. v1 IN ball_annulus /\ v2 IN ball_annulus /\ v3 IN ball_annulus /\ v4 IN ball_annulus /\
4094                                    dist (v1, v3) <= &2 * h0 /\ dist (v2, v4) <= &2 * h0 /\
4095                                    &2 <= dist (v1,v2) /\ &2 <= dist (v1,v4) /\
4096                                    &2 <= dist (v2,v3) /\ &2 <= dist (v3,v4) /\
4097                                    &2 <= dist (v1,v3) /\ &2 <= dist (v2,v4)
4098                                    ==> aff_ge {vec 0} {v1,v3} INTER aff_ge {vec 0} {v2,v4} = {vec 0}`,
4099    REPEAT STRIP_TAC THEN
4100      ASM_CASES_TAC `aff_ge {vec 0} {v1,v3} INTER aff_ge {vec 0} {v2,v4} = {vec 0:real^3}` THEN ASM_REWRITE_TAC[] THEN
4101      SUBGOAL_THEN `?p. ~(p = vec 0:real^3) /\ p IN aff_ge {vec 0} {v1,v3} INTER aff_ge {vec 0} {v2,v4}` MP_TAC THENL
4102      [
4103        POP_ASSUM MP_TAC THEN
4104          REWRITE_TAC[EXTENSION; IN_SING; NOT_FORALL_THM] THEN
4105          DISCH_THEN (CHOOSE_THEN MP_TAC) THEN
4106          ASM_CASES_TAC `x = vec 0:real^3` THENL
4107          [
4108            ASM_REWRITE_TAC[IN_INTER; points_in_aff_ge_0_2];
4109            ALL_TAC
4110          ] THEN
4111          ASM_REWRITE_TAC[] THEN
4112          DISCH_TAC THEN
4113          EXISTS_TAC `x:real^3` THEN
4114          ASM_REWRITE_TAC[];
4115        ALL_TAC
4116      ] THEN
4117
4118      STRIP_TAC THEN
4119      POP_ASSUM MP_TAC THEN
4120      SUBGOAL_THEN `~(v1 = vec 0:real^3) /\ ~(v2 = vec 0:real^3) /\ ~(v3 = vec 0:real^3) /\ ~(v4 = vec 0:real^3)` ASSUME_TAC THENL
4121      [
4122        REPEAT (FIRST_X_ASSUM (MP_TAC o check (is_binary "IN" o concl))) THEN
4123          SIMP_TAC[in_ball_annulus];
4124        ALL_TAC
4125      ] THEN
4126
4127      ASM_SIMP_TAC[aff_ge_0_2; IN_ELIM_THM; IN_INTER] THEN
4128      STRIP_TAC THEN
4129      UNDISCH_TAC `p = t1 % v1 + t2 % v3:real^3` THEN
4130      POP_ASSUM (LABEL_TAC "p2" o SYM) THEN
4131      DISCH_THEN (LABEL_TAC "p1" o SYM) THEN
4132
4133      SUBGOAL_THEN `!v v1 v2 v3 v4 t1 t2 t1' t2'. &0 <= t1 /\ &0 <= t2 /\ &0 <= t1' /\ &0 <= t2' /\ ~(v = vec 0) /\
4134                                t1 % v1 + t2 % v3 = v /\  t1' % v2 + t2' % v4 = v /\
4135                                t1' + t2' <= t1 + t2
4136                                  ==> ~(segment [v1,v3] INTER convex hull {vec 0,v2,v4:real^3} = {})` ASSUME_TAC THENL
4137      [
4138        REPEAT REMOVE_ASSUM THEN
4139          REWRITE_TAC[GSYM MEMBER_NOT_EMPTY] THEN
4140          REPEAT STRIP_TAC THEN
4141          SUBGOAL_THEN `&0 < t1 + t2` ASSUME_TAC THENL
4142          [
4143            ASM_CASES_TAC `t1 = &0` THENL
4144              [
4145                UNDISCH_TAC `t1 % v1 + t2 % v3:real^3 = v` THEN
4146                  POP_ASSUM (fun th -> REWRITE_TAC[th]) THEN
4147                  REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_LID] THEN
4148                  ASM_CASES_TAC `t2 = &0` THENL
4149                  [
4150                    POP_ASSUM (fun th -> REWRITE_TAC[th; VECTOR_MUL_LZERO; VECTOR_ADD_LID]) THEN
4151                      ASM_REWRITE_TAC[];
4152                    ALL_TAC
4153                  ] THEN
4154                  DISCH_TAC THEN
4155                  ASM_REWRITE_TAC[REAL_ADD_LID; REAL_LT_LE];
4156                ALL_TAC
4157              ] THEN
4158
4159              MATCH_MP_TAC REAL_LTE_ADD THEN
4160              ASM_REWRITE_TAC[REAL_LT_LE];
4161            ALL_TAC
4162          ] THEN
4163
4164          REWRITE_TAC[IN_INTER; IN_SEGMENT; CONVEX_HULL_3_ALT; IN_ELIM_THM] THEN
4165          EXISTS_TAC `inv (t1 + t2) % v:real^3` THEN
4166          CONJ_TAC THENL
4167          [
4168            EXISTS_TAC `t2 * inv (t1 + t2)` THEN
4169              CONJ_TAC THENL
4170              [
4171                MATCH_MP_TAC REAL_LE_MUL THEN ASM_REWRITE_TAC[] THEN
4172                  MATCH_MP_TAC REAL_LE_INV THEN ASM_SIMP_TAC[REAL_LT_IMP_LE];
4173                ALL_TAC
4174              ] THEN
4175
4176              CONJ_TAC THENL
4177              [
4178                REWRITE_TAC[GSYM real_div] THEN
4179                  MATCH_MP_TAC Trigonometry2.REAL_LE_LDIV THEN
4180                  ASM_REWRITE_TAC[REAL_ARITH `t2 <= t1 + t2 <=> &0 <= t1`];
4181                ALL_TAC
4182              ] THEN
4183
4184              UNDISCH_TAC `t1 % v1 + t2 % v3:real^3 = v` THEN
4185              DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN
4186              SUBGOAL_THEN `&1 - t2 * inv(t1 + t2) = t1 * inv (t1 + t2)` (fun th -> REWRITE_TAC[th]) THENL
4187              [
4188                MATCH_MP_TAC REAL_EQ_RCANCEL_IMP THEN
4189                  EXISTS_TAC `t1 + t2:real` THEN
4190                  REWRITE_TAC[REAL_SUB_RDISTRIB] THEN
4191                  ONCE_REWRITE_TAC[GSYM REAL_MUL_ASSOC] THEN
4192                  ASM_SIMP_TAC[REAL_ARITH `&0 < a ==> ~(a = &0)`; REAL_MUL_LINV] THEN
4193                  REAL_ARITH_TAC;
4194                ALL_TAC
4195              ] THEN
4196
4197              VECTOR_ARITH_TAC;
4198            ALL_TAC
4199          ] THEN
4200
4201          REWRITE_TAC[VECTOR_ADD_LID; VECTOR_SUB_RZERO] THEN
4202          MAP_EVERY EXISTS_TAC [`inv (t1 + t2) * t1'`; `inv (t1 + t2) * t2'`] THEN
4203          REWRITE_TAC[CONJ_ASSOC] THEN
4204          CONJ_TAC THENL
4205          [
4206            CONJ_TAC THENL
4207              [
4208                CONJ_TAC THEN MATCH_MP_TAC REAL_LE_MUL THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC REAL_LE_INV THEN ASM_SIMP_TAC[REAL_LT_IMP_LE];
4209                ALL_TAC
4210              ] THEN
4211
4212              REWRITE_TAC[GSYM REAL_ADD_LDISTRIB; REAL_MUL_AC; GSYM real_div] THEN
4213              MATCH_MP_TAC Trigonometry2.REAL_LE_LDIV THEN
4214              ASM_REWRITE_TAC[];
4215            ALL_TAC
4216          ] THEN
4217
4218          UNDISCH_TAC `t1' % v2 + t2' % v4:real^3 = v` THEN
4219          DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN
4220          VECTOR_ARITH_TAC;
4221        ALL_TAC
4222      ] THEN
4223
4224      SUBGOAL_THEN `?v1 v2 v3 v4. v1 IN ball_annulus /\ v2 IN ball_annulus /\ v3 IN ball_annulus /\ v4 IN ball_annulus /\
4225                                  dist (v1,v3) <= &2 * h0 /\ dist (v2,v4) <= &2 * h0 /\
4226                                  &2 <= dist (v1,v2) /\ &2 <= dist (v1,v4) /\
4227                                  &2 <= dist (v2,v3) /\ &2 <= dist (v3,v4) /\
4228                                  &2 <= dist (v2,v4) /\
4229                                  ~(segment [v1,v3] INTER convex hull {vec 0,v2,v4} = {})` MP_TAC THENL
4230      [
4231        ASM_CASES_TAC `t1' + t2' <= t1 + t2:real` THENL
4232          [
4233            MAP_EVERY EXISTS_TAC [`v1:real^3`; `v2:real^3`; `v3:real^3`; `v4:real^3`] THEN
4234              ASM_REWRITE_TAC[] THEN
4235              FIRST_X_ASSUM MATCH_MP_TAC THEN
4236              MAP_EVERY EXISTS_TAC [`p:real^3`; `t1:real`; `t2:real`; `t1':real`; `t2':real`] THEN
4237              ASM_REWRITE_TAC[];
4238            ALL_TAC
4239          ] THEN
4240
4241          POP_ASSUM MP_TAC THEN REWRITE_TAC[REAL_NOT_LE] THEN
4242          DISCH_TAC THEN
4243          MAP_EVERY EXISTS_TAC [`v2:real^3`; `v1:real^3`; `v4:real^3`; `v3:real^3`] THEN
4244          ASM_REWRITE_TAC[DIST_SYM] THEN
4245          FIRST_X_ASSUM MATCH_MP_TAC THEN
4246          MAP_EVERY EXISTS_TAC [`p:real^3`; `t1':real`; `t2':real`; `t1:real`; `t2:real`] THEN
4247          ASM_SIMP_TAC[REAL_LT_IMP_LE];
4248        ALL_TAC
4249      ] THEN
4250
4251      REPEAT REMOVE_ASSUM THEN
4252      STRIP_TAC THEN
4253
4254      (* First rotation *)
4255      MP_TAC (SPEC_ALL lemma_4_points_rotation2_full) THEN
4256      ASM_REWRITE_TAC[] THEN
4257      STRIP_TAC THEN
4258
4259      (* Second rotation *)
4260      MP_TAC (SPECL [`v1':real^3`; `v2:real^3`; `v3':real^3`; `v4:real^3`] lemma_4_points_rotation1_full) THEN
4261      ASM_REWRITE_TAC[] THEN
4262      MAP_EVERY (fun tm -> REPEAT (FIRST_X_ASSUM ((fun th -> ALL_TAC) o check (free_in tm o concl)))) [`v1:real^3`; `v3:real^3`; `v1':real^3`; `v3':real^3`] THEN
4263
4264      STRIP_TAC THEN
4265      MATCH_MP_TAC lemma_4_points_contradiction THEN
4266      MAP_EVERY EXISTS_TAC [`v1'':real^3`; `v2:real^3`; `v3'':real^3`; `v4:real^3`] THEN
4267      ASM_REWRITE_TAC[DIST_SYM]);;
4268
4269
4270
4271
4272 end;;