text_formalization/tame/CKQOWSA_3.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 (3-point case)                                         *)
   8 (* ========================================================================== *)
   9
  10 flyspeck_needs "fan/fan_defs.hl";;
  11 flyspeck_needs "packing/pack_defs.hl";;
  12
  13 flyspeck_needs "tame/Inequalities.hl";;
  14
  15
  16 module Ckqowsa_3_points = struct
  17
  18
  19 open Fan_defs;;
  20
  21
  22 let REMOVE_ASSUM = POP_ASSUM (fun th -> ALL_TAC);;
  23
  24
  25
  26 let coplanar_eq_coplanar_alt = prove(`!s:real^N->bool. 2 <= dimindex(:N) ==> (coplanar s <=> coplanar_alt s)`,
  27    REPEAT STRIP_TAC THEN
  28      ASM_SIMP_TAC[COPLANAR; Collect_geom.coplanar_alt]);;
  29
  30
  31
  32
  33 let in_ball_annulus = prove(`!v. v IN ball_annulus <=> &2 <= norm v /\ norm v <= &2 * h0 /\ ~(v = vec 0)`,
  34    REWRITE_TAC[Pack_defs.ball_annulus] THEN
  35      REWRITE_TAC[IN_DIFF; cball; ball; IN_ELIM_THM; DIST_0] THEN
  36      REWRITE_TAC[GSYM NORM_EQ_0] THEN
  37      REAL_ARITH_TAC);;
  38
  39
  40
  41
  42 let projection_lemma = prove(`!v n:real^N. ~(n = vec 0) ==>
  43                                ?a x. (v dot n) / (n dot n) = a /\ x dot n = &0 /\ v = x + a % n`,
  44    REWRITE_TAC[GSYM NORM_EQ_0] THEN
  45      REPEAT STRIP_TAC THEN
  46      EXISTS_TAC `(v dot n:real^N) / (n dot n)` THEN
  47      EXISTS_TAC `v - (v dot n:real^N) / (n dot n) % n` THEN
  48      REWRITE_TAC[] THEN
  49      CONJ_TAC THENL
  50      [
  51        REWRITE_TAC[DOT_LSUB; DOT_LMUL; DOT_SQUARE_NORM] THEN
  52          POP_ASSUM MP_TAC THEN
  53          CONV_TAC REAL_FIELD;
  54        ALL_TAC
  55      ] THEN
  56      VECTOR_ARITH_TAC);;
  57
  58
  59
  60
  61 let dist_lower_bound = prove(`!v1 v2 n:real^N. ~(n = vec 0) ==>
  62                                dist (v1, v2) pow 2 >= ((v1 - v2) dot n) pow 2 / (n dot n)`,
  63    REPEAT STRIP_TAC THEN
  64      FIRST_ASSUM MP_TAC THEN
  65      REWRITE_TAC[dist; GSYM DOT_SQUARE_NORM; GSYM NORM_EQ_0] THEN
  66      MP_TAC (SPECL [`v1:real^N`; `n:real^N`] projection_lemma) THEN
  67      MP_TAC (SPECL [`v2:real^N`; `n:real^N`] projection_lemma) THEN
  68      ASM_REWRITE_TAC[] THEN
  69      REPEAT STRIP_TAC THEN
  70      ASM_REWRITE_TAC[] THEN
  71      REWRITE_TAC[VECTOR_ARITH `((x' + a' % n) - (x + a % n)) dot ((x' + a' % n) - (x + a % n:real^N)) = (x' - x) dot (x' - x) + (a' - a) pow 2 * (n dot n) + &2 * (a' - a) * (x' dot n - x dot n)`] THEN
  72      ASM_REWRITE_TAC[VECTOR_ARITH `((x' + a' % n:real^N) - (x + a % n)) dot n = (a' - a) * (n dot n) + x' dot n - x dot n`] THEN
  73      REWRITE_TAC[REAL_MUL_RZERO; REAL_SUB_RZERO; REAL_ADD_RID] THEN
  74      REWRITE_TAC[REAL_POW_MUL; DOT_SQUARE_NORM] THEN
  75      ASM_SIMP_TAC[REAL_FIELD `~(n = &0) ==> (a pow 2 * n pow 2 pow 2) / n pow 2 = a pow 2 * n pow 2`] THEN
  76      REWRITE_TAC[REAL_ARITH `a + b >= b <=> &0 <= a`] THEN
  77      REWRITE_TAC[GSYM DOT_SQUARE_NORM] THEN
  78      REWRITE_TAC[DOT_POS_LE]);;
  79
  80
  81
  82
  83
  84 let non_collinear_lemma = prove(`!v w. v IN ball_annulus /\ w IN ball_annulus /\ &2 <= dist (v,w) /\ &0 < v dot w
  85                                   ==> ~(collinear {vec 0, v, w})`,
  86    REWRITE_TAC[COLLINEAR_BETWEEN_CASES; DE_MORGAN_THM] THEN
  87      REWRITE_TAC[in_ball_annulus; Pack_defs.h0; REAL_ARITH `&2 * #1.26 = #2.52`] THEN
  88      REPEAT GEN_TAC THEN DISCH_THEN STRIP_ASSUME_TAC THEN
  89      CONJ_TAC THENL
  90      [
  91        REWRITE_TAC[BETWEEN_DOT] THEN
  92          REWRITE_TAC[VECTOR_SUB_LZERO; VECTOR_SUB_RZERO; NORM_NEG; DOT_LNEG] THEN
  93          MATCH_MP_TAC (REAL_ARITH `&0 < a /\ &0 <= b ==> ~(--a = b)`) THEN
  94          ASM_REWRITE_TAC[] THEN
  95          MATCH_MP_TAC REAL_LE_MUL THEN
  96          REWRITE_TAC[NORM_POS_LE];
  97        ALL_TAC
  98      ] THEN
  99
 100      REWRITE_TAC[between; DIST_0] THEN
 101      REPEAT (POP_ASSUM MP_TAC) THEN
 102      REWRITE_TAC[DIST_SYM] THEN
 103      REAL_ARITH_TAC);;
 104
 105
 106
 107
 108
 109
 110
 111
 112
 113
 114
 115 let aff_ge_0_2 = prove(`!u v:real^N. ~(u = vec 0) /\ ~(v = vec 0) ==> aff_ge {vec 0} {u,v} = {y | ?t1 t2. &0 <= t1 /\ &0 <= t2 /\ y = t1 % u + t2 % v}`,
 116    REPEAT STRIP_TAC THEN
 117      SUBGOAL_THEN `DISJOINT {vec 0} {u:real^N, v}` ASSUME_TAC THENL
 118      [
 119        REWRITE_TAC[DISJOINT; EXTENSION; IN_INTER; IN_INSERT; NOT_IN_EMPTY; DE_MORGAN_THM] THEN
 120          ASM_MESON_TAC[];
 121        ALL_TAC
 122      ] THEN
 123      ASM_SIMP_TAC[Fan.AFF_GE_1_2] THEN
 124      REWRITE_TAC[EXTENSION] THEN GEN_TAC THEN
 125      REWRITE_TAC[IN_ELIM_THM] THEN
 126      EQ_TAC THEN STRIP_TAC THENL
 127      [
 128        MAP_EVERY EXISTS_TAC [`t2:real`; `t3:real`] THEN
 129          POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[] THEN
 130          VECTOR_ARITH_TAC;
 131        MAP_EVERY EXISTS_TAC [`&1 - t1 - t2`; `t1:real`; `t2:real`] THEN
 132          ASM_REWRITE_TAC[] THEN CONJ_TAC THENL
 133          [
 134            REAL_ARITH_TAC;
 135            ALL_TAC
 136          ] THEN
 137          POP_ASSUM MP_TAC THEN
 138          VECTOR_ARITH_TAC
 139      ]);;
 140
 141
 142
 143 let in_aff_ge_0_2 = prove(`!v1 v2 w. v1 IN ball_annulus /\ v2 IN ball_annulus /\ w IN ball_annulus /\
 144                             &2 <= dist (v1,w) /\ &2 <= dist (v2,w) /\
 145                             w IN aff_ge {vec 0} {v1,v2}
 146                             ==> ?t1 t2. &0 < t1 /\ &0 < t2 /\ w = t1 % v1 + t2 % v2`,
 147    REPEAT STRIP_TAC THEN
 148      SUBGOAL_THEN `~(w = vec 0:real^3) /\ ~(v1 = vec 0:real^3) /\ ~(v2 = vec 0:real^3)` ASSUME_TAC THENL
 149      [
 150        REPEAT (POP_ASSUM MP_TAC) THEN
 151          REWRITE_TAC[in_ball_annulus; GSYM NORM_EQ_0] THEN
 152          SIMP_TAC[REAL_ARITH `&2 <= a ==> ~(a = &0)`];
 153        ALL_TAC
 154      ] THEN
 155      FIRST_X_ASSUM (MP_TAC o check (is_binary "IN" o concl)) THEN
 156      ASM_SIMP_TAC[aff_ge_0_2] THEN
 157      REWRITE_TAC[IN_ELIM_THM] THEN
 158      STRIP_TAC THEN
 159      MAP_EVERY EXISTS_TAC [`t1:real`; `t2:real`] THEN
 160      ASM_REWRITE_TAC[REAL_ARITH `&0 < t <=> &0 <= t /\ ~(t = &0)`] THEN
 161      CONJ_TAC THEN DISCH_TAC THENL
 162      [
 163        SUBGOAL_THEN `collinear {vec 0:real^3,v2,w}` MP_TAC THENL
 164          [
 165            ONCE_REWRITE_TAC[COLLINEAR_LEMMA_ALT] THEN
 166              ASM_REWRITE_TAC[] THEN
 167              EXISTS_TAC `t2:real` THEN
 168              VECTOR_ARITH_TAC;
 169            ALL_TAC
 170          ];
 171
 172        SUBGOAL_THEN `collinear {vec 0:real^3,v1,w}` MP_TAC THENL
 173          [
 174            ONCE_REWRITE_TAC[COLLINEAR_LEMMA_ALT] THEN
 175              ASM_REWRITE_TAC[] THEN
 176              EXISTS_TAC `t1:real` THEN
 177              VECTOR_ARITH_TAC;
 178            ALL_TAC
 179          ]
 180      ] THEN
 181
 182      REWRITE_TAC[] THEN
 183      MATCH_MP_TAC non_collinear_lemma THEN
 184      ASM_REWRITE_TAC[] THEN
 185      REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_LID; DOT_RMUL; VECTOR_ADD_RID] THEN
 186      MATCH_MP_TAC REAL_LT_MUL THEN
 187      REWRITE_TAC[REAL_ARITH `&0 < t <=> &0 <= t /\ ~(t = &0)`] THEN
 188      ASM_REWRITE_TAC[DOT_POS_LE; DOT_EQ_0] THEN
 189      DISCH_TAC THEN UNDISCH_TAC `w = t1 % v1 + t2 % v2:real^3` THEN
 190      ASM_REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_LID]);;
 191
 192
 193
 194 let in_aff_ge_0_2_imp_dot_pos = prove(`!v1 v2 w:real^N. &0 < v1 dot v2 /\ w IN aff_ge {vec 0} {v1,v2} /\ ~(w = vec 0)
 195                                         ==> &0 < v1 dot w /\ &0 < v2 dot w`,
 196    REPEAT GEN_TAC THEN DISCH_THEN STRIP_ASSUME_TAC THEN
 197      SUBGOAL_THEN `~(v1 = vec 0:real^N) /\ ~(v2 = vec 0:real^N)` ASSUME_TAC THENL
 198      [
 199        CONJ_TAC THEN DISCH_TAC THEN UNDISCH_TAC `&0 < v1:real^N dot v2` THEN
 200          ASM_REWRITE_TAC[DOT_LZERO; DOT_RZERO; REAL_LT_REFL];
 201        ALL_TAC
 202      ] THEN
 203      FIRST_X_ASSUM (MP_TAC o check (is_binary "IN" o concl)) THEN
 204      ASM_SIMP_TAC[aff_ge_0_2] THEN
 205      REWRITE_TAC[IN_ELIM_THM] THEN STRIP_TAC THEN
 206      ASM_REWRITE_TAC[DOT_RADD; DOT_RMUL] THEN
 207      ASM_CASES_TAC `t1 = &0` THENL
 208      [
 209        ASM_REWRITE_TAC[REAL_MUL_LZERO; REAL_ADD_LID] THEN
 210          ASM_CASES_TAC `t2 = &0` THENL
 211          [
 212            UNDISCH_TAC `w = t1 % v1 + t2 % v2:real^N` THEN
 213              ASM_REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_LID];
 214            ALL_TAC
 215          ] THEN
 216          CONJ_TAC THEN MATCH_MP_TAC REAL_LT_MUL THEN
 217          ASM_REWRITE_TAC[DOT_POS_LT; REAL_ARITH `&0 < t <=> &0 <= t /\ ~(t = &0)`];
 218        ALL_TAC
 219      ] THEN
 220
 221      CONJ_TAC THEN MATCH_MP_TAC REAL_LTE_ADD THENL
 222      [
 223        CONJ_TAC THENL
 224          [
 225            MATCH_MP_TAC REAL_LT_MUL THEN
 226              ASM_REWRITE_TAC[DOT_POS_LT] THEN
 227              ASM_REWRITE_TAC[REAL_ARITH `&0 < t <=> &0 <= t /\ ~(t = &0)`];
 228            MATCH_MP_TAC REAL_LE_MUL THEN
 229              ASM_SIMP_TAC[REAL_LT_IMP_LE]
 230          ];
 231
 232        CONJ_TAC THENL
 233          [
 234            MATCH_MP_TAC REAL_LT_MUL THEN
 235              ASM_REWRITE_TAC[DOT_SYM] THEN
 236              ASM_REWRITE_TAC[REAL_ARITH `&0 < t <=> &0 <= t /\ ~(t = &0)`];
 237            MATCH_MP_TAC REAL_LE_MUL THEN
 238              ASM_REWRITE_TAC[DOT_POS_LE]
 239          ]
 240      ]);;
 241
 242
 243
 244 let aff_ge_eq_lemma = prove(`!a v1 v2 u:real^N. &0 < a /\ u = a % v2 /\ ~(v1 = vec 0) /\ ~(v2 = vec 0)
 245                              ==> aff_ge {vec 0} {v1,v2} = aff_ge {vec 0} {v1,u}`,
 246    REPEAT STRIP_TAC THEN
 247      SUBGOAL_THEN `~(u:real^N = vec 0)` ASSUME_TAC THENL
 248      [
 249        ASM_REWRITE_TAC[VECTOR_MUL_EQ_0] THEN
 250          REPEAT (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC;
 251        ALL_TAC
 252      ] THEN
 253      ASM_SIMP_TAC[aff_ge_0_2] THEN
 254      REWRITE_TAC[EXTENSION; IN_ELIM_THM] THEN
 255      GEN_TAC THEN EQ_TAC THENL
 256      [
 257        STRIP_TAC THEN
 258          MAP_EVERY EXISTS_TAC [`t1:real`; `t2 * inv(a)`] THEN
 259          ASM_REWRITE_TAC[] THEN
 260          CONJ_TAC THENL
 261          [
 262            MATCH_MP_TAC REAL_LE_MUL THEN
 263              ASM_REWRITE_TAC[] THEN
 264              MATCH_MP_TAC REAL_LE_INV THEN
 265              ASM_SIMP_TAC[REAL_LT_IMP_LE];
 266            ALL_TAC
 267          ] THEN
 268
 269          REWRITE_TAC[VECTOR_ARITH `(t2 * inva ) % a % v2 = (t2 * (inva * a)) % v2:real^N`] THEN
 270          ASM_SIMP_TAC[REAL_FIELD `&0 < a ==> inv a * a = &1`] THEN
 271          VECTOR_ARITH_TAC;
 272        ALL_TAC
 273      ] THEN
 274      STRIP_TAC THEN
 275      MAP_EVERY EXISTS_TAC [`t1:real`; `t2 * a`] THEN
 276      ASM_REWRITE_TAC[VECTOR_ARITH `(t2 * a) % v2 = t2 % a % v2:real^N`] THEN
 277      MATCH_MP_TAC REAL_LE_MUL THEN
 278      ASM_SIMP_TAC[REAL_LT_IMP_LE]);;
 279
 280
 281
 282
 283 let triangle_height_lemma = prove(`!v w:real^3. ~(w = vec 0)
 284                                   ==> ?a n. v = a % w + n /\ n dot w = &0 /\ norm n = norm (v cross w) / norm w`,
 285    REPEAT STRIP_TAC THEN FIRST_ASSUM MP_TAC THEN
 286      REWRITE_TAC[GSYM NORM_EQ_0] THEN
 287      DISCH_TAC THEN
 288      EXISTS_TAC `(v:real^3 dot w) / (w dot w)` THEN
 289      EXISTS_TAC `v - (v:real^3 dot w) / (w dot w) % w` THEN
 290      REPEAT CONJ_TAC THENL
 291      [
 292        VECTOR_ARITH_TAC;
 293        REWRITE_TAC[DOT_LSUB; DOT_LMUL; DOT_SQUARE_NORM] THEN
 294          POP_ASSUM MP_TAC THEN
 295          CONV_TAC REAL_FIELD;
 296        ALL_TAC
 297      ] THEN
 298
 299      SUBGOAL_THEN `!x:real^3. norm x = abs (norm x)` (fun th -> ONCE_REWRITE_TAC[th]) THENL
 300      [
 301        GEN_TAC THEN MP_TAC (ISPEC `x:real^3` NORM_POS_LE) THEN
 302          REAL_ARITH_TAC;
 303        ALL_TAC
 304      ] THEN
 305      REWRITE_TAC[GSYM REAL_ABS_DIV] THEN
 306      REWRITE_TAC[REAL_EQ_SQUARE_ABS] THEN
 307      REWRITE_TAC[NORM_POW_2; NORM_CROSS] THEN
 308      REWRITE_TAC[REAL_POW_DIV; REAL_POW_MUL] THEN
 309      REWRITE_TAC[SIN_SQUARED_VECTOR_ANGLE] THEN
 310      ASM_CASES_TAC `v:real^3 = vec 0` THEN ASM_REWRITE_TAC[] THENL
 311      [
 312        REWRITE_TAC[NORM_0; DOT_LZERO; REAL_POW_ZERO; Collect_geom.REAL_DIV_LZERO; VECTOR_MUL_LZERO; VECTOR_SUB_RZERO] THEN
 313          REWRITE_TAC[ARITH_RULE `~(2 = 0)`] THEN
 314          REAL_ARITH_TAC;
 315        ALL_TAC
 316      ] THEN
 317
 318      REWRITE_TAC[DOT_LSUB; DOT_RSUB; DOT_LMUL; DOT_RMUL] THEN
 319      REWRITE_TAC[DOT_SQUARE_NORM] THEN
 320      POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN
 321      REWRITE_TAC[GSYM NORM_EQ_0] THEN
 322      REWRITE_TAC[DOT_SYM] THEN
 323      CONV_TAC REAL_FIELD);;
 324
 325
 326
 327 let in_aff_ge_dist_lemma = prove(`!v1 v2 n1 n2 a b w:real^N. ~(w = vec 0) /\ ~(v1 = vec 0) /\ ~(v2 = vec 0) /\
 328                                    w IN aff_ge {vec 0} {v1, v2} /\
 329                                    v1 = a % w + n1 /\ v2 = b % w + n2 /\
 330                                    n1 dot w = &0 /\ n2 dot w = &0
 331                                    ==> norm (n1 - n2) = norm n1 + norm n2`,
 332    REPEAT STRIP_TAC THEN
 333      ASM_CASES_TAC `n1:real^N = vec 0` THENL
 334      [
 335        ASM_REWRITE_TAC[NORM_0; VECTOR_SUB_LZERO; NORM_NEG; REAL_ADD_LID];
 336        ALL_TAC
 337      ] THEN
 338      FIRST_X_ASSUM (MP_TAC o check (is_binary "IN" o concl)) THEN
 339      ASM_SIMP_TAC[aff_ge_0_2] THEN
 340      REWRITE_TAC[IN_ELIM_THM] THEN STRIP_TAC THEN
 341      SUBGOAL_THEN `n1:real^N dot w = t1 * (n1 dot n1) + t2 * (n1 dot n2)` MP_TAC THENL
 342      [
 343        POP_ASSUM (fun th -> ONCE_REWRITE_TAC[th]) THEN
 344          ASM_REWRITE_TAC[DOT_RADD; DOT_RMUL] THEN
 345          REAL_ARITH_TAC;
 346        ALL_TAC
 347      ] THEN
 348      SUBGOAL_THEN `n2:real^N dot w = t1 * (n1 dot n2) + t2 * (n2 dot n2)` MP_TAC THENL
 349      [
 350        POP_ASSUM (fun th -> ONCE_REWRITE_TAC[th]) THEN
 351          ASM_REWRITE_TAC[DOT_RADD; DOT_RMUL; DOT_SYM] THEN
 352          REAL_ARITH_TAC;
 353        ALL_TAC
 354      ] THEN
 355      POP_ASSUM (LABEL_TAC "A") THEN
 356      ASM_REWRITE_TAC[] THEN
 357
 358      ASM_CASES_TAC `t2 = &0` THENL
 359      [
 360        ASM_REWRITE_TAC[] THEN
 361          DISCH_TAC THEN
 362          ASM_CASES_TAC `t1 = &0` THENL
 363          [
 364            REMOVE_THEN "A" MP_TAC THEN
 365              ASM_REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_RID];
 366            ALL_TAC
 367          ] THEN
 368          REWRITE_TAC[REAL_MUL_LZERO; REAL_ADD_RID] THEN
 369          ASM_REWRITE_TAC[REAL_ENTIRE; EQ_SYM_EQ] THEN
 370          ASM_REWRITE_TAC[DOT_EQ_0];
 371        ALL_TAC
 372      ] THEN
 373
 374      REPEAT (DISCH_THEN (ASSUME_TAC o SYM)) THEN
 375      SUBGOAL_THEN `n1:real^N dot n2 = --(t1 / t2) * (n1 dot n1)` ASSUME_TAC THENL
 376      [
 377        REPLICATE_TAC 3 (POP_ASSUM MP_TAC) THEN
 378          CONV_TAC REAL_FIELD;
 379        ALL_TAC
 380      ] THEN
 381
 382      SUBGOAL_THEN `n1 dot n2:real^N <= &0` MP_TAC THENL
 383      [
 384        ASM_REWRITE_TAC[] THEN
 385          REWRITE_TAC[REAL_ARITH `--a * b <= &0 <=> &0 <= a * b`] THEN
 386          MATCH_MP_TAC REAL_LE_MUL THEN
 387          REWRITE_TAC[DOT_POS_LE] THEN
 388          MATCH_MP_TAC REAL_LE_DIV THEN
 389          ASM_REWRITE_TAC[];
 390        ALL_TAC
 391      ] THEN
 392      REMOVE_ASSUM THEN DISCH_TAC THEN
 393
 394      UNDISCH_TAC `~(n1 = vec 0:real^N)` THEN
 395      REWRITE_TAC[GSYM NORM_EQ_0] THEN
 396      DISCH_TAC THEN
 397      SUBGOAL_THEN `(n1:real^N dot n2) pow 2 = (norm n1 pow 2) * (norm n2 pow 2)` ASSUME_TAC THENL
 398      [
 399        POP_ASSUM MP_TAC THEN
 400          REMOVE_ASSUM THEN
 401          REPLICATE_TAC 3 (POP_ASSUM MP_TAC) THEN
 402          REWRITE_TAC[DOT_SQUARE_NORM] THEN
 403          CONV_TAC REAL_FIELD;
 404        ALL_TAC
 405      ] THEN
 406
 407      POP_ASSUM MP_TAC THEN
 408      REWRITE_TAC[GSYM REAL_POW_MUL] THEN
 409      REWRITE_TAC[GSYM REAL_EQ_SQUARE_ABS; REAL_ABS_MUL; REAL_ABS_NORM] THEN
 410      SUBGOAL_THEN `abs (n1:real^N dot n2) = --(n1 dot n2)` (fun th -> REWRITE_TAC[th]) THENL
 411      [
 412        REMOVE_ASSUM THEN POP_ASSUM MP_TAC THEN
 413          REAL_ARITH_TAC;
 414        ALL_TAC
 415      ] THEN
 416
 417      DISCH_TAC THEN
 418      SUBGOAL_THEN `norm (n1:real^N) + norm (n2:real^N) = abs (norm n1 + norm n2) /\ norm (n1 - n2) = abs (norm (n1 - n2))` (fun th -> ONCE_REWRITE_TAC[th]) THENL
 419      [
 420        REWRITE_TAC[REAL_ABS_NORM] THEN
 421          MP_TAC (ISPEC `n1:real^N` NORM_POS_LE) THEN
 422          MP_TAC (ISPEC `n2:real^N` NORM_POS_LE) THEN
 423          REAL_ARITH_TAC;
 424        ALL_TAC
 425      ] THEN
 426
 427      REWRITE_TAC[REAL_EQ_SQUARE_ABS] THEN
 428      REWRITE_TAC[GSYM DOT_SQUARE_NORM] THEN
 429      REWRITE_TAC[DOT_LSUB; DOT_RSUB; DOT_SYM; REAL_POW_2; REAL_ADD_LDISTRIB; REAL_ADD_RDISTRIB] THEN
 430      ASM_REWRITE_TAC[DOT_SQUARE_NORM] THEN
 431      POP_ASSUM MP_TAC THEN
 432      REAL_ARITH_TAC);;
 433
 434
 435
 436 let in_aff_ge_dist_lower_bound = prove(`!v1 v2 w. ~(v1 = vec 0) /\ ~(v2 = vec 0) /\ ~(w = vec 0) /\
 437                                          w IN aff_ge {vec 0} {v1, v2}
 438                                          ==> dist (v1,v2) >= (norm (v1 cross w) + norm (v2 cross w)) / norm w`,
 439    REPEAT STRIP_TAC THEN
 440      MP_TAC (SPECL [`v1:real^3`; `w:real^3`] triangle_height_lemma) THEN
 441      MP_TAC (SPECL [`v2:real^3`; `w:real^3`] triangle_height_lemma) THEN
 442      ASM_REWRITE_TAC[] THEN
 443      REPEAT STRIP_TAC THEN
 444
 445      MP_TAC (ISPECL [`v1:real^3`; `v2:real^3`; `n':real^3`; `n:real^3`; `a':real`; `a:real`; `w:real^3`] in_aff_ge_dist_lemma) THEN
 446      ANTS_TAC THENL
 447      [
 448        ASM_REWRITE_TAC[];
 449        ALL_TAC
 450      ] THEN
 451      DISCH_TAC THEN
 452
 453      SUBGOAL_THEN `dist (v1,v2:real^3) = sqrt ((a - a') pow 2* norm (w:real^3) pow 2 + (n - n':real^3) dot (n - n'))` (fun th -> REWRITE_TAC[th]) THENL
 454      [
 455        ASM_REWRITE_TAC[dist; vector_norm] THEN
 456          ASM_REWRITE_TAC[DOT_LSUB; DOT_RSUB; DOT_LMUL; DOT_RMUL; DOT_RADD; DOT_LADD; DOT_SYM] THEN
 457          AP_TERM_TAC THEN
 458          REWRITE_TAC[GSYM vector_norm; DOT_SQUARE_NORM] THEN
 459          REAL_ARITH_TAC;
 460        ALL_TAC
 461      ] THEN
 462
 463      REWRITE_TAC[real_ge] THEN
 464      MATCH_MP_TAC REAL_LE_TRANS THEN
 465      EXISTS_TAC `sqrt ((n:real^3 - n') dot (n - n'))` THEN
 466      CONJ_TAC THENL
 467      [
 468        POP_ASSUM MP_TAC THEN
 469          REWRITE_TAC[GSYM vector_norm; NORM_SUB] THEN
 470          ASM_SIMP_TAC[] THEN
 471          REAL_ARITH_TAC;
 472        ALL_TAC
 473      ] THEN
 474
 475      MATCH_MP_TAC SQRT_MONO_LE THEN
 476      REWRITE_TAC[DOT_POS_LE] THEN
 477      REWRITE_TAC[REAL_ARITH `a <= b + a <=> &0 <= b`] THEN
 478      MATCH_MP_TAC REAL_LE_MUL THEN
 479      REWRITE_TAC[Trigonometry1.REAL_LE_POW_2]);;
 480
 481
 482
 483 let triangle_area_lower_bound = prove(`!v w. v IN ball_annulus /\ w IN ball_annulus /\ dist (v,w) = &2
 484                                         ==> #1.48 * sqrt(&3) <= norm (v cross w)`,
 485    REWRITE_TAC[in_ball_annulus; Sphere.h0; REAL_ARITH `&2 * #1.26 = #2.52`] THEN
 486      REPEAT STRIP_TAC THEN
 487      SUBGOAL_THEN `~(v = vec 0:real^3) /\ ~(w = vec 0:real^3)` ASSUME_TAC THENL
 488      [
 489        REWRITE_TAC[GSYM NORM_EQ_0] THEN
 490          ASM_SIMP_TAC[REAL_ARITH `&2 <= n ==> ~(n = &0)`];
 491        ALL_TAC
 492      ] THEN
 493
 494      ASM_SIMP_TAC[Trigonometry1.NORM_CROSS] THEN
 495      REWRITE_TAC[Trigonometry2.UPS_X_AND_HERON] THEN
 496      REWRITE_TAC[REAL_ARITH `a <= b / &2 <=> &2 * a <= b`] THEN
 497      SUBGOAL_THEN `&2 * #1.48 * sqrt (&3) = sqrt(&6 * &2 * (&4 - #2.52) * (&4 - #2.52))` (fun th -> REWRITE_TAC[th]) THENL
 498      [
 499        REWRITE_TAC[REAL_ARITH `&6 * &2 * (&4 - #2.52) * (&4 - #2.52) = &2 pow 2 * (#1.48) pow 2 * &3`] THEN
 500          ASSUME_TAC (REAL_ARITH `&0 <= &2 pow 2 /\ &0 <= #1.48 pow 2 * &3 /\ &0 <= &3 /\ &0 <= #1.48 pow 2`) THEN
 501          ASM_SIMP_TAC[SQRT_MUL] THEN
 502          REWRITE_TAC[POW_2_SQRT_ABS] THEN
 503          REAL_ARITH_TAC;
 504        ALL_TAC
 505      ] THEN
 506
 507      MATCH_MP_TAC SQRT_MONO_LE THEN
 508      CONJ_TAC THENL
 509      [
 510        CONV_TAC REAL_RAT_REDUCE_CONV;
 511        ALL_TAC
 512      ] THEN
 513
 514      MATCH_MP_TAC REAL_LE_MUL2 THEN
 515      CONJ_TAC THENL [ REAL_ARITH_TAC; ALL_TAC ] THEN
 516      CONJ_TAC THENL
 517      [
 518        REPEAT (POP_ASSUM MP_TAC) THEN
 519          REAL_ARITH_TAC;
 520        ALL_TAC
 521      ] THEN
 522      CONJ_TAC THENL [ REAL_ARITH_TAC; ALL_TAC ] THEN
 523
 524      MATCH_MP_TAC REAL_LE_MUL2 THEN
 525      CONJ_TAC THENL [ REAL_ARITH_TAC; ALL_TAC ] THEN
 526      CONJ_TAC THENL
 527      [
 528        REPEAT (POP_ASSUM MP_TAC) THEN
 529          REAL_ARITH_TAC;
 530        ALL_TAC
 531      ] THEN
 532      CONJ_TAC THENL [ REAL_ARITH_TAC; ALL_TAC ] THEN
 533
 534      MATCH_MP_TAC REAL_LE_MUL2 THEN
 535      REPEAT (POP_ASSUM MP_TAC) THEN
 536      REAL_ARITH_TAC);;
 537
 538
 539
 540
 541 let DIST_LOWER_BOUND_lemma = prove(`!v1 v2 w. v1 IN ball_annulus /\ v2 IN ball_annulus /\ w IN ball_annulus /\
 542                                      w IN aff_ge {vec 0} {v1, v2} /\
 543                                      dist (v1, w) = &2 /\
 544                                      dist (v2, w) = &2
 545                                      ==> &1 <= dist (v1,v2)`,
 546    REWRITE_TAC[in_ball_annulus] THEN
 547      REPEAT STRIP_TAC THEN
 548      SUBGOAL_THEN `~(v1 = vec 0:real^3) /\ ~(v2 = vec 0:real^3) /\ ~(w = vec 0:real^3)` ASSUME_TAC THENL
 549      [
 550        REWRITE_TAC[GSYM NORM_EQ_0] THEN
 551          ASM_SIMP_TAC[REAL_ARITH `&2 <= n ==> ~(n = &0)`];
 552        ALL_TAC
 553      ] THEN
 554      MP_TAC (SPEC_ALL in_aff_ge_dist_lower_bound) THEN
 555      ASM_REWRITE_TAC[real_ge] THEN
 556      MP_TAC (SPECL [`v1:real^3`; `w:real^3`] triangle_area_lower_bound) THEN
 557      MP_TAC (SPECL [`v2:real^3`; `w:real^3`] triangle_area_lower_bound) THEN
 558      ASM_REWRITE_TAC[in_ball_annulus] THEN
 559      REPEAT DISCH_TAC THEN
 560
 561      SUBGOAL_THEN `&1 <= sqrt (&3)` ASSUME_TAC THENL
 562      [
 563        ONCE_REWRITE_TAC[GSYM SQRT_1] THEN
 564          MATCH_MP_TAC SQRT_MONO_LE THEN
 565          REAL_ARITH_TAC;
 566        ALL_TAC
 567      ] THEN
 568
 569      MATCH_MP_TAC REAL_LE_TRANS THEN
 570      EXISTS_TAC `#1.48 * sqrt(&3) / #1.26` THEN
 571      CONJ_TAC THENL
 572      [
 573        POP_ASSUM MP_TAC THEN
 574          REAL_ARITH_TAC;
 575        ALL_TAC
 576      ] THEN
 577
 578      MATCH_MP_TAC REAL_LE_TRANS THEN
 579      EXISTS_TAC `(#1.48 * sqrt (&3) + #1.48 * sqrt (&3)) / (&2 * h0)` THEN
 580      CONJ_TAC THENL
 581      [
 582        REWRITE_TAC[Sphere.h0] THEN
 583          REAL_ARITH_TAC;
 584        ALL_TAC
 585      ] THEN
 586
 587      MATCH_MP_TAC REAL_LE_TRANS THEN
 588      EXISTS_TAC `(norm (v1 cross w) + norm (v2 cross w)) / norm w` THEN
 589      CONJ_TAC THENL
 590      [
 591        SUBGOAL_THEN `&0 < &2 * h0 /\ &0 < norm (w:real^3)` ASSUME_TAC THENL
 592          [
 593            ASM_SIMP_TAC[Sphere.h0; REAL_ARITH `&2 <= n ==> &0 < n`] THEN
 594              REAL_ARITH_TAC;
 595            ALL_TAC
 596          ] THEN
 597          ASM_SIMP_TAC[RAT_LEMMA4] THEN
 598          MATCH_MP_TAC REAL_LE_MUL2 THEN
 599          REPEAT CONJ_TAC THENL
 600          [
 601            REMOVE_ASSUM THEN POP_ASSUM MP_TAC THEN
 602              REAL_ARITH_TAC;
 603            MATCH_MP_TAC REAL_LE_ADD2 THEN
 604              ASM_REWRITE_TAC[];
 605            REWRITE_TAC[NORM_POS_LE];
 606            ALL_TAC
 607          ] THEN
 608          ASM_REWRITE_TAC[];
 609        ALL_TAC
 610      ] THEN
 611      ASM_REWRITE_TAC[]);;
 612
 613
 614
 615
 616
 617 let aff_ge_trans = prove(`!v1 v2 v3 v:real^N. v3 IN aff_ge {vec 0} {v1,v2} /\
 618                     v IN aff_ge {vec 0} {v1,v3} /\ ~(v = vec 0) /\ ~(v1 = vec 0) /\ ~(v2 = vec 0) /\ ~(v3 = vec 0)
 619                   ==> v3 IN aff_ge {vec 0} {v,v2}`,
 620    REPEAT STRIP_TAC THEN
 621      REPEAT (FIRST_X_ASSUM (MP_TAC o check (is_binary "IN" o concl))) THEN
 622      ASM_SIMP_TAC[aff_ge_0_2] THEN
 623      REWRITE_TAC[IN_ELIM_THM] THEN
 624      REPEAT STRIP_TAC THEN
 625      POP_ASSUM MP_TAC THEN
 626      ASM_CASES_TAC `t1' = &0` THENL
 627      [
 628        POP_ASSUM (fun th -> REWRITE_TAC[th]) THEN
 629          REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_LID] THEN
 630          DISCH_TAC THEN
 631          MAP_EVERY EXISTS_TAC [`inv (t2')`; `&0`] THEN
 632          POP_ASSUM MP_TAC THEN
 633          POP_ASSUM (fun th -> SIMP_TAC[th; REAL_LE_INV]) THEN
 634          REWRITE_TAC[REAL_LE_REFL] THEN
 635          DISCH_TAC THEN
 636          REWRITE_TAC[VECTOR_ARITH `a % b % v = (a * b) % (v:real^N)`] THEN
 637          SUBGOAL_THEN `inv t2' * t2' = &1` (fun th -> REWRITE_TAC[th]) THENL
 638          [
 639            MATCH_MP_TAC REAL_MUL_LINV THEN
 640              DISCH_TAC THEN UNDISCH_TAC `v:real^N = t2' % v3` THEN
 641              POP_ASSUM (fun th -> REWRITE_TAC[th]) THEN
 642              ASM_REWRITE_TAC[VECTOR_MUL_LZERO];
 643            ALL_TAC
 644          ] THEN
 645          VECTOR_ARITH_TAC;
 646        ALL_TAC
 647      ] THEN
 648
 649      DISCH_TAC THEN
 650      MAP_EVERY EXISTS_TAC [`t1 / (t1' + t2' * t1)`; `t2 * t1' / (t1' + t2' * t1)`] THEN
 651      ASM_REWRITE_TAC[] THEN
 652      SUBGOAL_THEN `&0 < t1' + t2' * t1` ASSUME_TAC THENL
 653      [
 654        MATCH_MP_TAC (REAL_ARITH `&0 < a /\ &0 <= b ==> &0 < a + b`) THEN
 655          ASM_REWRITE_TAC[REAL_ARITH `&0 < a <=> &0 <= a /\ ~(a = &0)`] THEN
 656          MATCH_MP_TAC REAL_LE_MUL THEN
 657          ASM_REWRITE_TAC[];
 658        ALL_TAC
 659      ] THEN
 660
 661      REPEAT CONJ_TAC THENL
 662      [
 663        MATCH_MP_TAC REAL_LE_DIV THEN
 664          ASM_SIMP_TAC[REAL_LT_IMP_LE];
 665        MATCH_MP_TAC REAL_LE_MUL THEN
 666          ASM_REWRITE_TAC[] THEN
 667          MATCH_MP_TAC REAL_LE_DIV THEN
 668          ASM_SIMP_TAC[REAL_LT_IMP_LE];
 669        ALL_TAC
 670      ] THEN
 671
 672      POP_ASSUM MP_TAC THEN
 673      REWRITE_TAC[VECTOR_ARITH `t1 / a % (t1' % (v1:real^N) + t2' % (t1 % v1 + t2 % v2)) + (t2 * t1' / a) % v2 = (t1 * (t1' + t2' * t1) / a) % v1 + (t2 * (t1' + t2' * t1) / a) % v2`] THEN
 674      SIMP_TAC[REAL_FIELD `&0 < a ==> b * a / a = b`]);;
 675
 676
 677
 678 let rotation_dist_decrease = prove(`!v w u:real^N. norm u = norm v /\ &0 <= v dot w /\ ~(w = vec 0) /\
 679                                     u IN aff_ge {vec 0} {v,w}
 680                                     ==> dist (u,w) <= dist (v,w)`,
 681    REPEAT STRIP_TAC THEN
 682      ASM_CASES_TAC `v:real^N = vec 0` THENL
 683      [
 684        UNDISCH_TAC `norm (u:real^N) = norm (v:real^N)` THEN
 685          ASM_REWRITE_TAC[NORM_0; NORM_EQ_0] THEN
 686          DISCH_TAC THEN ASM_REWRITE_TAC[REAL_LE_REFL];
 687        ALL_TAC
 688      ] THEN
 689      FIRST_X_ASSUM (MP_TAC o check (is_binary "IN" o concl)) THEN
 690      ASM_SIMP_TAC[aff_ge_0_2] THEN
 691      REWRITE_TAC[IN_ELIM_THM] THEN STRIP_TAC THEN
 692      REWRITE_TAC[dist] THEN
 693      ONCE_REWRITE_TAC[GSYM REAL_ABS_NORM] THEN
 694      REWRITE_TAC[REAL_LE_SQUARE_ABS] THEN
 695      REWRITE_TAC[NORM_POW_2] THEN
 696      REWRITE_TAC[VECTOR_ARITH `(u:real^N - w) dot (u - w) = u dot u + w dot w - &2 * u dot w`] THEN
 697      ASM_REWRITE_TAC[DOT_SQUARE_NORM] THEN
 698      REWRITE_TAC[REAL_ARITH `a + b - &2*c <= a + b - &2*d <=> &0 <= c - d`] THEN
 699      REWRITE_TAC[VECTOR_ARITH `(t1 % v + t2 % w:real^N) dot w - v dot w = t1 * (v dot w) + t2 * (w dot w) - v dot w`] THEN
 700      REWRITE_TAC[REAL_ARITH `&0 <= a + c - b <=> b <= a + c`] THEN
 701      SUBGOAL_THEN `norm (u:real^N) pow 2 = t1 * t1 * (v dot v:real^N) + t2 * t2 * (w dot w:real^N) + &2 * t1 * t2 * (v dot w)` MP_TAC THENL
 702      [
 703        POP_ASSUM (fun th -> REWRITE_TAC[th]) THEN
 704          REWRITE_TAC[NORM_POW_2] THEN
 705          VECTOR_ARITH_TAC;
 706        ALL_TAC
 707      ] THEN
 708      ASM_REWRITE_TAC[] THEN
 709      REWRITE_TAC[NORM_POW_2] THEN DISCH_TAC THEN
 710      SUBGOAL_THEN `t1 <= &1` ASSUME_TAC THENL
 711      [
 712        MP_TAC (REAL_ARITH `&0 <= t1 ==> t1 = abs (t1)`) THEN
 713          ASM_REWRITE_TAC[] THEN
 714          DISCH_THEN (fun th -> ONCE_REWRITE_TAC[th]) THEN
 715          ONCE_REWRITE_TAC[REAL_ARITH `&1 = abs (&1)`] THEN
 716          REWRITE_TAC[REAL_LE_SQUARE_ABS; REAL_POW_2] THEN
 717          MATCH_MP_TAC REAL_LE_RCANCEL_IMP THEN
 718          EXISTS_TAC `v:real^N dot v` THEN
 719          CONJ_TAC THENL
 720          [
 721            ASM_REWRITE_TAC[DOT_POS_LT];
 722            ALL_TAC
 723          ] THEN
 724          POP_ASSUM (fun th -> GEN_REWRITE_TAC (RAND_CONV o DEPTH_CONV) [th]) THEN
 725          REWRITE_TAC[REAL_MUL_LID; REAL_MUL_ASSOC] THEN
 726          REWRITE_TAC[REAL_ARITH `a <= a + c <=> &0 <= c`] THEN
 727          MATCH_MP_TAC REAL_LE_ADD THEN
 728          CONJ_TAC THEN MATCH_MP_TAC REAL_LE_MUL THEN ASM_REWRITE_TAC[DOT_POS_LE] THENL
 729          [
 730            MATCH_MP_TAC REAL_LE_MUL THEN ASM_REWRITE_TAC[];
 731            ALL_TAC
 732          ] THEN
 733          MATCH_MP_TAC REAL_LE_MUL THEN ASM_REWRITE_TAC[] THEN
 734          MATCH_MP_TAC REAL_LE_MUL THEN ASM_REWRITE_TAC[REAL_ARITH `&0 <= &2`];
 735        ALL_TAC
 736      ] THEN
 737
 738      ABBREV_TAC `x = t2 * (w:real^N dot w)` THEN
 739      ABBREV_TAC `y = (v:real^N dot w)` THEN
 740      SUBGOAL_THEN `&0 <= t1 * y + x` ASSUME_TAC THENL
 741      [
 742        MATCH_MP_TAC REAL_LE_ADD THEN
 743          CONJ_TAC THENL
 744          [
 745            MATCH_MP_TAC REAL_LE_MUL THEN
 746              ASM_REWRITE_TAC[];
 747            ALL_TAC
 748          ] THEN
 749          EXPAND_TAC "x" THEN MATCH_MP_TAC REAL_LE_MUL THEN
 750          ASM_REWRITE_TAC[DOT_POS_LE];
 751        ALL_TAC
 752      ] THEN
 753      POP_ASSUM (MP_TAC o REWRITE_RULE[GSYM REAL_ABS_REFL]) THEN
 754      DISCH_THEN (fun th -> ONCE_REWRITE_TAC[SYM th]) THEN
 755      UNDISCH_TAC `&0 <= y` THEN
 756      DISCH_TAC THEN FIRST_ASSUM MP_TAC THEN
 757      REWRITE_TAC[GSYM REAL_ABS_REFL] THEN
 758      DISCH_THEN (fun th -> ONCE_REWRITE_TAC[SYM th]) THEN
 759      REWRITE_TAC[REAL_LE_SQUARE_ABS] THEN
 760      SUBGOAL_THEN `(v dot v:real^N) * (w dot w:real^N) = t1 * t1 * (v dot v:real^N) * (w dot w:real^N) + x pow 2 + &2 * t1 * y * x` ASSUME_TAC THENL
 761      [
 762        EXPAND_TAC "x" THEN
 763          REWRITE_TAC[REAL_ARITH `t1 * t1 * v * w + (t2 * w) pow 2 + &2 * t1 * y * t2 * w = (t1 * t1 * v + t2 * (t2 * w) + &2 * t1 * t2 * y) * w`] THEN
 764          REWRITE_TAC[REAL_EQ_MUL_RCANCEL] THEN
 765          DISJ1_TAC THEN ASM_REWRITE_TAC[] THEN
 766          REPLICATE_TAC 4 REMOVE_ASSUM THEN
 767          POP_ASSUM ACCEPT_TAC;
 768        ALL_TAC
 769      ] THEN
 770      SUBGOAL_THEN `(t1 * abs y + x) pow 2 = x pow 2 + &2 * t1 * y * x + t1 * t1 * (y pow 2)` (fun th -> REWRITE_TAC[th]) THENL
 771      [
 772        REMOVE_ASSUM THEN POP_ASSUM MP_TAC THEN
 773          REAL_ARITH_TAC;
 774        ALL_TAC
 775      ] THEN
 776      REWRITE_TAC[REAL_ADD_ASSOC] THEN
 777      SUBGOAL_THEN `x pow 2 + &2 * t1 * y * x = (v dot v) * (w dot w) - t1 pow 2 * (v dot v:real^N) * (w dot w:real^N)` (fun th -> REWRITE_TAC[th]) THENL
 778      [
 779        POP_ASSUM MP_TAC THEN
 780          REAL_ARITH_TAC;
 781        ALL_TAC
 782      ] THEN
 783      REWRITE_TAC[REAL_ARITH `a <= v * w - t pow 2 * v * w + t * t * a <=> &0 <= (&1 - t * t) * (v * w - a)`] THEN
 784      MATCH_MP_TAC REAL_LE_MUL THEN
 785      CONJ_TAC THENL
 786      [
 787        REWRITE_TAC[REAL_ARITH `&0 <= &1 - t1 * t1 <=> t1 * t1 <= &1 * &1`] THEN
 788          MATCH_MP_TAC REAL_LE_MUL2 THEN
 789          ASM_REWRITE_TAC[];
 790        ALL_TAC
 791      ] THEN
 792      EXPAND_TAC "y" THEN
 793      REWRITE_TAC[REAL_ARITH `&0 <= v * w - vw <=> vw <= v * w`] THEN
 794      REWRITE_TAC[DOT_SQUARE_NORM; GSYM REAL_POW_MUL] THEN
 795      REWRITE_TAC[Trigonometry2.SQUARE_NORM_CAUCHY_SCHWARZ_POW2]);;
 796
 797
 798
 799
 800
 801
 802 let pos_vector_angle_bounds = prove(`!v u:real^N. v dot u > &0 ==> &0 <= vector_angle v u /\ vector_angle v u <= pi / &2`,
 803    REPEAT GEN_TAC THEN DISCH_TAC THEN
 804      REWRITE_TAC[VECTOR_ANGLE_RANGE] THEN
 805      REWRITE_TAC[vector_angle] THEN
 806      COND_CASES_TAC THEN ASM_REWRITE_TAC[REAL_LE_REFL] THEN
 807      SUBGOAL_THEN `pi / &2 = acs (cos (pi / &2))` MP_TAC THENL
 808      [
 809        MATCH_MP_TAC (GSYM ACS_COS) THEN
 810          MP_TAC PI_POS THEN
 811          REAL_ARITH_TAC;
 812        ALL_TAC
 813      ] THEN
 814      DISCH_THEN (fun th -> ONCE_REWRITE_TAC[th]) THEN
 815      MATCH_MP_TAC ACS_MONO_LE THEN
 816      REWRITE_TAC[COS_PI2; REAL_ARITH `-- &1 <= &0`] THEN
 817      CONJ_TAC THENL
 818      [
 819        MATCH_MP_TAC REAL_LE_DIV THEN
 820          ASM_SIMP_TAC[REAL_ARITH `a > &0 ==> &0 <= a`] THEN
 821          MATCH_MP_TAC REAL_LE_MUL THEN
 822          REWRITE_TAC[NORM_POS_LE];
 823        ALL_TAC
 824      ] THEN
 825      POP_ASSUM MP_TAC THEN REWRITE_TAC[DE_MORGAN_THM] THEN
 826      SIMP_TAC[Trigonometry1.NORM_CAUCHY_SCHWARZ_FRAC]);;
 827
 828
 829
 830
 831
 832
 833 let rotation_lemma = prove(`!v (u:real^N). ~collinear {vec 0, v, u} /\ norm v = norm u
 834                           ==> ?f. f(lift (&0)) = v /\ f(lift (&1)) = u /\
 835                               (!t. ?a b. f t = a % v + b % u) /\
 836                               (!t. norm (f t) = norm v) /\
 837                               (!t. t IN interval [lift (&0), lift (&1)] ==> f t IN aff_ge {vec 0} {v, u}) /\
 838                               f continuous_on UNIV`,
 839    REPEAT STRIP_TAC THEN
 840      SUBGOAL_THEN `~(v:real^N = vec 0) /\ ~(u:real^N = vec 0) /\ ~(v = u) /\ ~(u = --v)` ASSUME_TAC THENL
 841      [
 842        UNDISCH_TAC `~collinear {vec 0:real^N,v,u}` THEN
 843          SIMP_TAC[COLLINEAR_LEMMA_ALT; DE_MORGAN_THM] THEN
 844          ASM_SIMP_TAC[GSYM NORM_EQ_0; NOT_EXISTS_THM] THEN
 845          STRIP_TAC THEN
 846          FIRST_ASSUM (MP_TAC o SPEC `&1`) THEN
 847          FIRST_X_ASSUM (MP_TAC o SPEC `-- &1`) THEN
 848          SIMP_TAC[VECTOR_MUL_LID; VECTOR_MUL_LNEG];
 849        ALL_TAC
 850      ] THEN
 851
 852      SUBGOAL_THEN `norm (u:real^N) > &0 /\ ~(norm u = &0)` ASSUME_TAC THENL
 853      [
 854        ASM_REWRITE_TAC[real_gt; NORM_POS_LT; NORM_EQ_0];
 855        ALL_TAC
 856      ] THEN
 857
 858      ABBREV_TAC `phi = vector_angle (v:real^N) (u:real^N)` THEN
 859      ABBREV_TAC `e:real^N = inv (sin phi) % u - cos phi % inv(sin phi) % v` THEN
 860
 861      SUBGOAL_THEN `&0 < sin phi` ASSUME_TAC THENL
 862      [
 863        REWRITE_TAC[REAL_ARITH `&0 < a <=> &0 <= a /\ ~(a = &0)`] THEN
 864          EXPAND_TAC "phi" THEN
 865          REWRITE_TAC[SIN_VECTOR_ANGLE_POS] THEN
 866          REWRITE_TAC[SIN_VECTOR_ANGLE_EQ_0] THEN
 867          ASM_REWRITE_TAC[VECTOR_ANGLE_EQ_0; VECTOR_ANGLE_EQ_PI; DE_MORGAN_THM] THEN
 868          REWRITE_TAC[VECTOR_ARITH `a % u + a % v = vec 0 <=> a % u = a % (--v:real^N)`] THEN
 869          ASM_REWRITE_TAC[VECTOR_MUL_LCANCEL];
 870        ALL_TAC
 871      ] THEN
 872
 873      SUBGOAL_THEN `(u dot u) * (v dot v) - (u:real^N dot v) pow 2 > &0` ASSUME_TAC THENL
 874      [
 875        REWRITE_TAC[DOT_SQUARE_NORM] THEN
 876          REWRITE_TAC[REAL_ARITH `a - b > &0 <=> b <= a /\ ~(b = a)`] THEN
 877          REWRITE_TAC[GSYM REAL_POW_MUL] THEN
 878          CONJ_TAC THENL
 879          [
 880            REWRITE_TAC[Trigonometry2.SQUARE_NORM_CAUCHY_SCHWARZ_POW2];
 881            ALL_TAC
 882          ] THEN
 883          REWRITE_TAC[GSYM REAL_EQ_SQUARE_ABS] THEN
 884          REWRITE_TAC[REAL_ABS_MUL; REAL_ABS_NORM] THEN
 885          ASM_REWRITE_TAC[NORM_CAUCHY_SCHWARZ_ABS_EQ; DE_MORGAN_THM] THEN
 886          REWRITE_TAC[VECTOR_ARITH `--a % v = a % (--v:real^N)`] THEN
 887          ASM_REWRITE_TAC[VECTOR_MUL_LCANCEL; VECTOR_ARITH `v = --u <=> u = --v:real^N`];
 888        ALL_TAC
 889      ] THEN
 890
 891      SUBGOAL_THEN `e:real^N dot v = &0` ASSUME_TAC THENL
 892      [
 893        EXPAND_TAC "e" THEN
 894          REWRITE_TAC[DOT_LSUB; DOT_LMUL] THEN
 895          REWRITE_TAC[REAL_ARITH `a * b - c * a * d = a * (b - c * d)`] THEN
 896          REWRITE_TAC[REAL_ENTIRE] THEN
 897          DISJ2_TAC THEN
 898          EXPAND_TAC "phi" THEN ASM_REWRITE_TAC[COS_VECTOR_ANGLE] THEN
 899          ASM_REWRITE_TAC[DOT_SYM; DOT_SQUARE_NORM] THEN
 900          UNDISCH_TAC `norm (u:real^N) > &0 /\ ~(norm u = &0)` THEN
 901          CONV_TAC REAL_FIELD;
 902        ALL_TAC
 903      ] THEN
 904
 905      ABBREV_TAC `d = norm (u:real^N) pow 4 - (u dot v) pow 2` THEN
 906      SUBGOAL_THEN `&0 < d` ASSUME_TAC THENL
 907      [
 908        POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN
 909          REMOVE_ASSUM THEN POP_ASSUM MP_TAC THEN
 910          ASM_REWRITE_TAC[DOT_SQUARE_NORM] THEN
 911          REAL_ARITH_TAC;
 912        ALL_TAC
 913      ] THEN
 914
 915      SUBGOAL_THEN `inv (sin phi) pow 2 = norm (u:real^N) pow 4 / d /\ cos phi pow 2 = (u dot v) pow 2 / norm u pow 4` ASSUME_TAC THENL
 916      [
 917        REWRITE_TAC[REAL_POW_INV] THEN
 918          EXPAND_TAC "phi" THEN
 919          ASM_REWRITE_TAC[SIN_SQUARED_VECTOR_ANGLE; COS_VECTOR_ANGLE; DOT_SYM] THEN
 920          UNDISCH_TAC `norm (u:real^N) > &0 /\ ~(norm u = &0)` THEN
 921          POP_ASSUM MP_TAC THEN EXPAND_TAC "d" THEN
 922          CONV_TAC REAL_FIELD;
 923        ALL_TAC
 924      ] THEN
 925
 926      SUBGOAL_THEN `e:real^N dot e = v:real^N dot v` ASSUME_TAC THENL
 927      [
 928        EXPAND_TAC "e" THEN
 929          REWRITE_TAC[VECTOR_ARITH `(a % u - b % a % v) dot (a % u - b % a % v) = (a pow 2) * ((u dot u) + (b pow 2) * v dot v - &2 * b * (u dot v:real^N))`] THEN
 930          ASM_REWRITE_TAC[] THEN
 931          EXPAND_TAC "phi" THEN ASM_REWRITE_TAC[COS_VECTOR_ANGLE; DOT_SYM] THEN
 932          ASM_REWRITE_TAC[DOT_SQUARE_NORM] THEN
 933          REMOVE_ASSUM THEN POP_ASSUM MP_TAC THEN
 934          POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN
 935          UNDISCH_TAC `norm (u:real^N) > &0 /\ ~(norm u = &0)` THEN
 936          CONV_TAC REAL_FIELD;
 937        ALL_TAC
 938      ] THEN
 939
 940      ABBREV_TAC `f = (\t:real^1. cos (phi * drop t) % (v:real^N) + sin (phi * drop t) % e)` THEN
 941      EXISTS_TAC `f:real^1->real^N` THEN
 942      REPEAT CONJ_TAC THENL
 943      [
 944        (* f(0) = v *)
 945        EXPAND_TAC "f" THEN BETA_TAC THEN
 946          REWRITE_TAC[LIFT_DROP; REAL_MUL_RZERO] THEN
 947          REWRITE_TAC[COS_0; SIN_0] THEN
 948          VECTOR_ARITH_TAC;
 949
 950        (* f(1) = u *)
 951        EXPAND_TAC "f" THEN BETA_TAC THEN
 952          REWRITE_TAC[LIFT_DROP; REAL_MUL_RID] THEN
 953          EXPAND_TAC "e" THEN
 954          REWRITE_TAC[VECTOR_ARITH `s % (is % u - c % is % v) = (s * is) % (u - c % v)`] THEN
 955          ASM_SIMP_TAC[REAL_FIELD `&0 < s ==> s * inv (s) = &1`] THEN
 956          VECTOR_ARITH_TAC;
 957
 958        (* f(t) = a v + b u *)
 959        GEN_TAC THEN
 960          EXPAND_TAC "f" THEN EXPAND_TAC "e" THEN
 961          EXISTS_TAC `cos (phi * drop (t:real^1)) - sin(phi * drop t) * cos phi * inv(sin phi)` THEN
 962          EXISTS_TAC `sin (phi * drop (t:real^1)) * inv(sin phi)` THEN
 963          VECTOR_ARITH_TAC;
 964
 965        (* |f(t)| = |v| *)
 966        GEN_TAC THEN
 967          REWRITE_TAC[NORM_EQ] THEN
 968          EXPAND_TAC "f" THEN BETA_TAC THEN
 969          REWRITE_TAC[VECTOR_ARITH `(c % v + s % e:real^N) dot (c % v + s % e) = (c pow 2) * (v dot v) + (s pow 2) * (e dot e) + &2 * c * s * (e dot v)`] THEN
 970          ASM_REWRITE_TAC[] THEN
 971          REWRITE_TAC[REAL_ARITH `c pow 2 * v + s pow 2 * v + &2 * c * s * &0 = (s pow 2 + c pow 2) * v`] THEN
 972          REWRITE_TAC[SIN_CIRCLE] THEN
 973          REAL_ARITH_TAC;
 974
 975        (* f(t) IN aff_ge 0 {v, u} *)
 976        GEN_TAC THEN REWRITE_TAC[IN_INTERVAL] THEN
 977          DISCH_THEN (MP_TAC o SPEC `1`) THEN
 978          REWRITE_TAC[LE_REFL; DIMINDEX_1] THEN
 979          REWRITE_TAC[GSYM drop; LIFT_DROP] THEN
 980          DISCH_TAC THEN
 981          ASM_SIMP_TAC[aff_ge_0_2] THEN
 982          REWRITE_TAC[IN_ELIM_THM] THEN
 983          EXPAND_TAC "f" THEN EXPAND_TAC "e" THEN
 984
 985          MAP_EVERY EXISTS_TAC [`cos (phi * drop (t:real^1)) - sin (phi * drop t) * cos phi * inv(sin phi)`; `sin (phi * drop (t:real^1)) * inv(sin phi)`] THEN
 986          SUBGOAL_THEN `&0 < phi /\ phi < pi` ASSUME_TAC THENL
 987          [
 988            REWRITE_TAC[REAL_ARITH `&0 < phi <=> ~(phi = &0) /\ &0 <= phi`; REAL_ARITH `phi < pi <=> phi <= pi /\ ~(phi = pi)`] THEN
 989              EXPAND_TAC "phi" THEN REWRITE_TAC[VECTOR_ANGLE_RANGE] THEN
 990              ASM_REWRITE_TAC[] THEN
 991              CONJ_TAC THEN DISCH_TAC THEN UNDISCH_TAC `&0 < sin phi` THEN ASM_REWRITE_TAC[SIN_0; SIN_PI; REAL_LT_REFL];
 992            ALL_TAC
 993          ] THEN
 994
 995          CONJ_TAC THENL
 996          [
 997            REWRITE_TAC[GSYM real_div; REAL_ARITH `&0 <= a - b * c * d <=> (b * c) * d <= a / &1`] THEN
 998              MP_TAC (GEN_ALL RAT_LEMMA4) THEN
 999              DISCH_THEN (MP_TAC o SPECL [`sin (phi * drop (t:real^1)) * cos phi`; `&1`; `cos (phi * drop (t:real^1))`; `sin phi`]) THEN
1000              ASM_REWRITE_TAC[REAL_LT_01] THEN
1001              DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
1002              REWRITE_TAC[REAL_ARITH `(s1 * c) * &1 <= c1 * s <=> &0 <= s * c1 - c * s1`] THEN
1003              REWRITE_TAC[GSYM SIN_SUB] THEN
1004              MATCH_MP_TAC SIN_POS_PI_LE THEN
1005              REWRITE_TAC[REAL_ARITH `phi - phi * t = phi * (&1 - t)`] THEN
1006              CONJ_TAC THENL [ MATCH_MP_TAC REAL_LE_MUL THEN ASM_SIMP_TAC[REAL_LT_IMP_LE; REAL_ARITH `t <= &1 ==> &0 <= &1 - t`]; ALL_TAC ] THEN
1007              ONCE_REWRITE_TAC[REAL_ARITH `pi = pi * &1`] THEN
1008              MATCH_MP_TAC REAL_LE_MUL2 THEN
1009              POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN
1010              REAL_ARITH_TAC;
1011            ALL_TAC
1012          ] THEN
1013
1014          CONJ_TAC THENL
1015          [
1016            MATCH_MP_TAC REAL_LE_MUL THEN
1017              CONJ_TAC THENL
1018              [
1019                MATCH_MP_TAC SIN_POS_PI_LE THEN
1020                  CONJ_TAC THENL [ MATCH_MP_TAC REAL_LE_MUL THEN ASM_SIMP_TAC[REAL_LT_IMP_LE]; ALL_TAC ] THEN
1021                  ONCE_REWRITE_TAC[REAL_ARITH `pi = pi * &1`] THEN
1022                  MATCH_MP_TAC REAL_LE_MUL2 THEN
1023                  ASM_REWRITE_TAC[] THEN
1024                  POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;
1025                ALL_TAC
1026              ] THEN
1027              MATCH_MP_TAC REAL_LE_INV THEN
1028              ASM_SIMP_TAC[REAL_LT_IMP_LE];
1029            ALL_TAC
1030          ] THEN
1031          VECTOR_ARITH_TAC;
1032
1033        (* f is continuous *)
1034        EXPAND_TAC "f" THEN
1035          MATCH_MP_TAC CONTINUOUS_ON_ADD THEN
1036          CONJ_TAC THEN MATCH_MP_TAC CONTINUOUS_ON_VMUL THENL
1037          [
1038            MATCH_MP_TAC CONTINUOUS_AT_IMP_CONTINUOUS_ON THEN
1039              REPEAT STRIP_TAC THEN
1040              REWRITE_TAC[GSYM REAL_CONTINUOUS_CONTINUOUS1] THEN
1041              SUBGOAL_THEN `(\t:real^1. cos (phi * drop t)) = cos o (\t. phi * drop t)` (fun th -> REWRITE_TAC[th]) THENL
1042              [
1043                REWRITE_TAC[FUN_EQ_THM; o_THM];
1044                ALL_TAC
1045              ] THEN
1046              MATCH_MP_TAC REAL_CONTINUOUS_AT_COMPOSE THEN
1047              REWRITE_TAC[REAL_CONTINUOUS_WITHIN_COS] THEN
1048              REWRITE_TAC[drop] THEN
1049              MATCH_MP_TAC REAL_CONTINUOUS_LMUL THEN
1050              MATCH_MP_TAC REAL_CONTINUOUS_AT_COMPONENT THEN
1051              REWRITE_TAC[DIMINDEX_1] THEN ARITH_TAC;
1052
1053            MATCH_MP_TAC CONTINUOUS_AT_IMP_CONTINUOUS_ON THEN
1054              REPEAT STRIP_TAC THEN
1055              REWRITE_TAC[GSYM REAL_CONTINUOUS_CONTINUOUS1] THEN
1056              SUBGOAL_THEN `(\t:real^1. sin (phi * drop t)) = sin o (\t. phi * drop t)` (fun th -> REWRITE_TAC[th]) THENL
1057              [
1058                REWRITE_TAC[FUN_EQ_THM; o_THM];
1059                ALL_TAC
1060              ] THEN
1061              MATCH_MP_TAC REAL_CONTINUOUS_AT_COMPOSE THEN
1062              REWRITE_TAC[REAL_CONTINUOUS_WITHIN_SIN] THEN
1063              REWRITE_TAC[drop] THEN
1064              MATCH_MP_TAC REAL_CONTINUOUS_LMUL THEN
1065              MATCH_MP_TAC REAL_CONTINUOUS_AT_COMPONENT THEN
1066              REWRITE_TAC[DIMINDEX_1] THEN ARITH_TAC
1067          ]
1068      ]);;
1069
1070
1071
1072
1073
1074
1075
1076 let dot_pos_lemma = prove(`!v w. v IN ball_annulus /\ w IN ball_annulus /\ dist (v,w) <= &2 * h0 ==> v dot w > &0`,
1077    REWRITE_TAC[in_ball_annulus] THEN
1078      REPEAT STRIP_TAC THEN
1079      POP_ASSUM MP_TAC THEN
1080      REWRITE_TAC[dist] THEN DISCH_TAC THEN
1081      SUBGOAL_THEN `(v - w) dot (v:real^3 - w) <= (&2 * h0) * (&2 * h0)` MP_TAC THENL
1082      [
1083        REWRITE_TAC[DOT_SQUARE_NORM; REAL_POW_2] THEN
1084          MATCH_MP_TAC REAL_LE_MUL2 THEN
1085          ASM_REWRITE_TAC[NORM_POS_LE];
1086        ALL_TAC
1087      ] THEN
1088      ASM_CASES_TAC `v:real^3 dot w > &0` THEN ASM_REWRITE_TAC[] THEN
1089      REWRITE_TAC[REAL_NOT_LE] THEN
1090      REWRITE_TAC[VECTOR_ARITH `(v - w:real^3) dot (v - w) = v dot v + w dot w - &2 * (v dot w)`] THEN
1091      MATCH_MP_TAC REAL_LTE_TRANS THEN
1092      EXISTS_TAC `(v dot v:real^3) + (w dot w:real^3)` THEN
1093      CONJ_TAC THENL
1094      [
1095        REWRITE_TAC[Pack_defs.h0; DOT_SQUARE_NORM] THEN
1096          SUBGOAL_THEN `&2 * &2 <= norm (v:real^3) pow 2 /\ &2 * &2 <= norm (w:real^3) pow 2` MP_TAC THENL
1097          [
1098            REWRITE_TAC[REAL_POW_2] THEN
1099              CONJ_TAC THEN MATCH_MP_TAC REAL_LE_MUL2 THEN ASM_REWRITE_TAC[REAL_ARITH `&0 <= &2`];
1100            ALL_TAC
1101          ] THEN
1102          REAL_ARITH_TAC;
1103        ALL_TAC
1104      ] THEN
1105      REWRITE_TAC[REAL_ARITH `v + w <= v + w - &2 * vw <=> vw <= &0`] THEN
1106      POP_ASSUM MP_TAC THEN
1107      REAL_ARITH_TAC);;
1108
1109
1110
1111 let dist_decreasing_ivt_lemma = prove(`!f (v:real^N) t1 d. &0 <= t1 /\
1112                                            f continuous_on UNIV /\
1113                                            dist (f(lift t1), v) <= d /\
1114                                            d <= dist (f(lift (&0)), v)
1115                                            ==> ?t. t IN interval [lift (&0), lift t1] /\ dist (f t, v) = d`,
1116    REPEAT STRIP_TAC THEN
1117      MP_TAC (ISPECL [`(lift o (\x. dist (x,v:real^N))) o (f:real^1->real^N)`; `lift (&0)`; `lift t1`; `d:real`; `1`] IVT_DECREASING_COMPONENT_1) THEN
1118      ASM_REWRITE_TAC[LIFT_DROP; LE_REFL; DIMINDEX_1] THEN
1119      ANTS_TAC THENL
1120      [
1121        REPEAT CONJ_TAC THENL
1122          [
1123            REPEAT STRIP_TAC THEN
1124              MATCH_MP_TAC CONTINUOUS_AT_COMPOSE THEN
1125              UNDISCH_TAC `(f:real^1->real^N) continuous_on UNIV` THEN
1126              REWRITE_TAC[CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN; WITHIN_UNIV; IN_UNIV] THEN
1127              DISCH_TAC THEN ASM_REWRITE_TAC[] THEN
1128              SUBGOAL_THEN `lift o (\x. dist (x,v:real^N)) = (lift o norm) o (\x. x - v)` (fun th -> REWRITE_TAC[th]) THENL
1129              [
1130                REWRITE_TAC[FUN_EQ_THM; o_THM; dist];
1131                ALL_TAC
1132              ] THEN
1133              MATCH_MP_TAC CONTINUOUS_AT_COMPOSE THEN
1134              REWRITE_TAC[CONTINUOUS_AT_LIFT_NORM] THEN
1135              MATCH_MP_TAC CONTINUOUS_SUB THEN
1136              REWRITE_TAC[CONTINUOUS_AT_ID; CONTINUOUS_CONST];
1137            ASM_REWRITE_TAC[o_THM; GSYM drop; LIFT_DROP];
1138            ASM_REWRITE_TAC[o_THM; GSYM drop; LIFT_DROP]
1139          ];
1140        ALL_TAC
1141      ] THEN
1142
1143      STRIP_TAC THEN
1144      EXISTS_TAC `x:real^1` THEN
1145      ASM_REWRITE_TAC[] THEN
1146      POP_ASSUM MP_TAC THEN
1147      REWRITE_TAC[o_THM; GSYM drop; LIFT_DROP]);;
1148
1149
1150
1151
1152 let lemma_3_points = prove(`!v1 v2 v3. v3 IN aff_ge {vec 0} {v1,v2} /\
1153                                        v1 IN ball_annulus /\ v2 IN ball_annulus /\ v3 IN ball_annulus /\
1154                                        dist (v1,v2) <= &2 * h0 /\ &2 <= dist (v1,v3) /\ &2 <= dist (v2,v3)
1155                                        ==> ?v. v IN ball_annulus /\
1156                                                v3 IN aff_ge {vec 0} {v,v2} /\
1157                                                dist (v,v2) <= &2 * h0 /\ dist (v,v3) = &2`,
1158    REPEAT STRIP_TAC THEN
1159      MP_TAC (SPECL [`v1:real^3`; `v2:real^3`] dot_pos_lemma) THEN
1160      ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
1161      REPLICATE_TAC 3 (FIRST_X_ASSUM (MP_TAC o check (is_binary "IN" o concl))) THEN
1162      REWRITE_TAC[IMP_IMP] THEN DISCH_TAC THEN FIRST_ASSUM MP_TAC THEN
1163      REWRITE_TAC[in_ball_annulus] THEN
1164      DISCH_TAC THEN
1165
1166      MP_TAC (SPECL [`v1:real^3`; `v2:real^3`; `v3:real^3`] in_aff_ge_0_2) THEN
1167      ASM_REWRITE_TAC[] THEN
1168      STRIP_TAC THEN
1169      POP_ASSUM (LABEL_TAC "A" o SYM) THEN
1170
1171      ABBREV_TAC `u:real^3 = (norm (v1:real^3) / norm (v3:real^3)) % v3` THEN
1172
1173      MP_TAC (ISPECL [`v1:real^3`; `u:real^3`] rotation_lemma) THEN
1174      SUBGOAL_THEN `~collinear {vec 0, v1, v3:real^3}` ASSUME_TAC THENL
1175      [
1176        MATCH_MP_TAC non_collinear_lemma THEN
1177          ASM_REWRITE_TAC[] THEN
1178          REMOVE_THEN "A" (fun th -> REWRITE_TAC[SYM th]) THEN
1179          REWRITE_TAC[DOT_RADD; DOT_RMUL] THEN
1180          MATCH_MP_TAC REAL_LT_ADD THEN
1181          CONJ_TAC THEN MATCH_MP_TAC REAL_LT_MUL THEN ASM_REWRITE_TAC[] THENL
1182          [
1183            ASM_REWRITE_TAC[DOT_POS_LT];
1184            ALL_TAC
1185          ] THEN
1186          ASM_REWRITE_TAC[GSYM real_gt];
1187        ALL_TAC
1188      ] THEN
1189
1190      SUBGOAL_THEN `dist (u,v3:real^3) < &2` ASSUME_TAC THENL
1191      [
1192        REWRITE_TAC[dist] THEN
1193          EXPAND_TAC "u" THEN
1194          REWRITE_TAC[VECTOR_ARITH `a % v3 - v3 = (a - &1) % v3:real^3`] THEN
1195          REWRITE_TAC[NORM_MUL] THEN
1196          SUBGOAL_THEN `norm (v3:real^3) = abs (norm v3)` MP_TAC THENL
1197          [
1198            ASM_SIMP_TAC[REAL_ARITH `&2 <= n3 ==> n3 = abs(n3)`];
1199            ALL_TAC
1200          ] THEN
1201          DISCH_TAC THEN
1202          FIRST_ASSUM (fun th -> ONCE_REWRITE_TAC[th]) THEN
1203          REWRITE_TAC[GSYM REAL_ABS_MUL] THEN
1204          POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN
1205          ASM_SIMP_TAC[REAL_FIELD `&2 <= n3 ==> (n1 / n3 - &1) * n3 = (n1 - n3)`] THEN
1206          REPEAT (FIRST_X_ASSUM (MP_TAC o check (is_conj o concl))) THEN
1207          REWRITE_TAC[Pack_defs.h0] THEN
1208          REAL_ARITH_TAC;
1209        ALL_TAC
1210      ] THEN
1211
1212      ANTS_TAC THENL
1213      [
1214        CONJ_TAC THENL
1215          [
1216            UNDISCH_TAC `~collinear {vec 0:real^3,v1,v3}` THEN
1217              MP_TAC (ISPECL [`&1`; `norm (v1:real^3) / norm (v3:real^3)`; `v1:real^3`; `v3:real^3`] COLLINEAR_SCALE_ALL) THEN
1218              ANTS_TAC THENL
1219              [
1220                REWRITE_TAC[REAL_ARITH `~(&1 = &0)`] THEN
1221                  MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~(a = &0)`) THEN
1222                  MATCH_MP_TAC REAL_LT_DIV THEN
1223                  ASM_SIMP_TAC[REAL_ARITH `&2 <= n ==> &0 < n`];
1224                ALL_TAC
1225              ] THEN
1226              ASM_SIMP_TAC[VECTOR_MUL_LID];
1227            ALL_TAC
1228          ] THEN
1229
1230          EXPAND_TAC "u" THEN
1231          REWRITE_TAC[NORM_MUL] THEN
1232          SUBGOAL_THEN `abs (norm (v1:real^3) / norm (v3:real^3)) = norm v1 / norm v3` (fun th -> REWRITE_TAC[th]) THENL
1233          [
1234            REWRITE_TAC[REAL_ABS_REFL] THEN
1235              MATCH_MP_TAC REAL_LE_DIV THEN
1236              REWRITE_TAC[NORM_POS_LE];
1237            ALL_TAC
1238          ] THEN
1239          ASM_SIMP_TAC[REAL_FIELD `&2 <= n3 ==> n1 / n3 * n3 = n1`];
1240        ALL_TAC
1241      ] THEN
1242
1243      STRIP_TAC THEN
1244      MP_TAC (ISPECL [`f:real^1->real^3`; `v3:real^3`; `&1`; `&2`] dist_decreasing_ivt_lemma) THEN
1245      ASM_SIMP_TAC[REAL_ARITH `dist (u:real^3,v3) < &2 ==> dist(u,v3) <= &2`; REAL_LE_01] THEN
1246      STRIP_TAC THEN
1247      EXISTS_TAC `(f:real^1->real^3) t` THEN
1248      ASM_REWRITE_TAC[] THEN
1249
1250      SUBGOAL_THEN `aff_ge {vec 0} {v1:real^3,v3} = aff_ge {vec 0} {v1,u}` ASSUME_TAC THENL
1251      [
1252        MATCH_MP_TAC aff_ge_eq_lemma THEN
1253          EXISTS_TAC `norm (v1:real^3) / norm (v3:real^3)` THEN
1254          ASM_REWRITE_TAC[] THEN
1255          MATCH_MP_TAC REAL_LT_DIV THEN
1256          ASM_SIMP_TAC[REAL_ARITH `&2 <= n ==> &0 < n`];
1257        ALL_TAC
1258      ] THEN
1259
1260      CONJ_TAC THENL
1261      [
1262        ASM_REWRITE_TAC[GSYM NORM_EQ_0] THEN
1263          ASM_REWRITE_TAC[NORM_EQ_0];
1264        ALL_TAC
1265      ] THEN
1266
1267      CONJ_TAC THENL
1268      [
1269        MATCH_MP_TAC aff_ge_trans THEN
1270          EXISTS_TAC `v1:real^3` THEN
1271          ASM_REWRITE_TAC[] THEN
1272          FIRST_X_ASSUM (MP_TAC o SPEC `t:real^1`) THEN
1273          ASM_REWRITE_TAC[] THEN
1274          SIMP_TAC[] THEN
1275          DISCH_TAC THEN
1276          ASM_REWRITE_TAC[GSYM NORM_EQ_0] THEN
1277          ASM_REWRITE_TAC[NORM_EQ_0];
1278        ALL_TAC
1279      ] THEN
1280
1281      MATCH_MP_TAC REAL_LE_TRANS THEN
1282      EXISTS_TAC `dist (v1,v2:real^3)` THEN
1283      ASM_REWRITE_TAC[] THEN
1284      MATCH_MP_TAC rotation_dist_decrease THEN
1285      ASM_SIMP_TAC[REAL_ARITH `a > &0 ==> &0 <= a`] THEN
1286
1287      FIRST_X_ASSUM (MP_TAC o SPEC `t:real^1`) THEN
1288      POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN
1289      ASM_SIMP_TAC[aff_ge_0_2] THEN
1290      REWRITE_TAC[IN_ELIM_THM] THEN
1291      REMOVE_THEN "A" (fun th -> REWRITE_TAC[SYM th]) THEN
1292      STRIP_TAC THEN
1293      MAP_EVERY EXISTS_TAC [`t1' + t2' * t1:real`; `t2' * t2:real`] THEN
1294      REPEAT CONJ_TAC THENL
1295      [
1296        MATCH_MP_TAC REAL_LE_ADD THEN
1297          ASM_REWRITE_TAC[] THEN
1298          MATCH_MP_TAC REAL_LE_MUL THEN
1299          ASM_SIMP_TAC[REAL_LT_IMP_LE];
1300        MATCH_MP_TAC REAL_LE_MUL THEN
1301          ASM_SIMP_TAC[REAL_LT_IMP_LE];
1302        ALL_TAC
1303      ] THEN
1304      POP_ASSUM MP_TAC THEN
1305      VECTOR_ARITH_TAC);;
1306
1307
1308
1309
1310
1311 let LEMMA_3_POINTS = prove(`!v1 v2 v3. v3 IN aff_ge {vec 0} {v1,v2} /\
1312                              v1 IN ball_annulus /\ v2 IN ball_annulus /\ v3 IN ball_annulus /\
1313                              dist (v1,v2) <= &2 * h0 /\
1314                              &2 <= dist (v1,v3) /\
1315                              &2 <= dist (v2,v3)
1316                              ==> (?v1' v2'. v3 IN aff_ge {vec 0} {v1',v2'} /\
1317                                     v1' IN ball_annulus /\ v2' IN ball_annulus /\ v3 IN ball_annulus /\
1318                                     dist (v1',v2') <= &2 * h0 /\
1319                                     dist (v1',v3) = &2 /\
1320                                     dist (v2',v3) = &2)`,
1321    REPEAT STRIP_TAC THEN
1322      MP_TAC (SPEC_ALL lemma_3_points) THEN
1323      ASM_REWRITE_TAC[real_ge] THEN
1324      DISCH_THEN (X_CHOOSE_THEN `v1':real^3` MP_TAC) THEN
1325      STRIP_TAC THEN
1326
1327      MP_TAC (SPECL [`v2:real^3`; `v1':real^3`; `v3:real^3`] lemma_3_points) THEN
1328      ANTS_TAC THENL
1329      [
1330        ASM_REWRITE_TAC[] THEN
1331        CONJ_TAC THENL
1332          [
1333            ASM_REWRITE_TAC[SET_RULE `{v2,v1'} = {v1',v2}`];
1334            ALL_TAC
1335          ] THEN
1336          ASM_SIMP_TAC[DIST_SYM; real_ge; REAL_LE_REFL];
1337        ALL_TAC
1338      ] THEN
1339
1340      DISCH_THEN (X_CHOOSE_THEN `v2':real^3` MP_TAC) THEN
1341      STRIP_TAC THEN
1342      MAP_EVERY EXISTS_TAC [`v1':real^3`; `v2':real^3`] THEN
1343      ASM_REWRITE_TAC[] THEN
1344      CONJ_TAC THENL
1345      [
1346        ASSUME_TAC (SET_RULE `{v1':real^3,v2'} = {v2',v1'}`) THEN
1347          POP_ASSUM (fun th -> ONCE_REWRITE_TAC [th]) THEN
1348          ASM_REWRITE_TAC[];
1349        REMOVE_ASSUM THEN POP_ASSUM MP_TAC THEN
1350          SIMP_TAC[DIST_SYM]
1351      ]);;
1352
1353
1354
1355 let LEMMA_3_POINTS_FINAL = prove(`!v1 v2 v3.
1356                                    v3 IN aff_ge {vec 0} {v1,v2} /\
1357                                    v1 IN ball_annulus /\ v2 IN ball_annulus /\ v3 IN ball_annulus /\
1358                                    dist (v1,v2) <= &2 * h0 /\
1359                                    &2 <= dist (v1,v3) /\
1360                                    &2 <= dist (v2,v3)
1361                                    ==> F`,
1362    REPEAT GEN_TAC THEN DISCH_TAC THEN
1363      FIRST_X_ASSUM (MP_TAC o MATCH_MP LEMMA_3_POINTS) THEN
1364      REPEAT STRIP_TAC THEN
1365      REPLICATE_TAC 3 (FIRST_X_ASSUM (MP_TAC o check (is_binary "IN" o concl))) THEN
1366      REWRITE_TAC[in_ball_annulus] THEN
1367      REPEAT STRIP_TAC THEN
1368
1369      MP_TAC (SPECL [`vec 0:real^3`; `v1':real^3`; `v2':real^3`; `v3:real^3`] Collect_geom.POLFLZY) THEN
1370      REWRITE_TAC[Tame_inequalities.DELTA_EQ_DELTA_X] THEN
1371
1372      CONV_TAC (DEPTH_CONV let_CONV) THEN
1373      SUBGOAL_THEN `coplanar_alt {vec 0, v1':real^3, v2', v3}` (fun th -> REWRITE_TAC[th]) THENL
1374      [
1375        MP_TAC (ISPEC `{vec 0,v1',v2',v3:real^3}` coplanar_eq_coplanar_alt) THEN
1376          REWRITE_TAC[DIMINDEX_3] THEN ANTS_TAC THENL [ ARITH_TAC; ALL_TAC ] THEN
1377          DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN
1378          REWRITE_TAC[coplanar] THEN
1379
1380          MAP_EVERY EXISTS_TAC [`vec 0:real^3`; `v1':real^3`; `v2':real^3`] THEN
1381          REWRITE_TAC[AFFINE_HULL_3; VECTOR_MUL_RZERO; VECTOR_ADD_LID] THEN
1382          REWRITE_TAC[SUBSET; IN_INSERT; NOT_IN_EMPTY; IN_ELIM_THM] THEN
1383          REPEAT STRIP_TAC THENL
1384          [
1385            MAP_EVERY EXISTS_TAC [`&1`; `&0`; `&0`] THEN
1386              ASM_REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_LID] THEN
1387              REAL_ARITH_TAC;
1388            MAP_EVERY EXISTS_TAC [`&0`; `&1`; `&0`] THEN
1389              ASM_REWRITE_TAC[VECTOR_MUL_LID; VECTOR_MUL_LZERO; VECTOR_ADD_RID] THEN
1390              REAL_ARITH_TAC;
1391            MAP_EVERY EXISTS_TAC [`&0`; `&0`; `&1`] THEN
1392              ASM_REWRITE_TAC[VECTOR_MUL_LID; VECTOR_MUL_LZERO; VECTOR_ADD_LID] THEN
1393              REAL_ARITH_TAC;
1394            ALL_TAC
1395          ] THEN
1396          SUBGOAL_THEN `~(v1':real^3 = vec 0) /\ ~(v2':real^3 = vec 0)` ASSUME_TAC THENL
1397          [
1398            REWRITE_TAC[GSYM NORM_EQ_0] THEN
1399              ASM_SIMP_TAC[REAL_ARITH `&2 <= norm n ==> ~(norm n = &0)`];
1400            ALL_TAC
1401          ] THEN
1402          FIRST_X_ASSUM (MP_TAC o check (is_binary "IN" o concl)) THEN
1403          ASM_SIMP_TAC[aff_ge_0_2] THEN
1404          REWRITE_TAC[IN_ELIM_THM] THEN
1405          STRIP_TAC THEN
1406          MAP_EVERY EXISTS_TAC [`&1 - t1 - t2`; `t1:real`; `t2:real`] THEN
1407          ASM_REWRITE_TAC[] THEN
1408          REAL_ARITH_TAC;
1409        ALL_TAC
1410      ] THEN
1411
1412      MATCH_MP_TAC (REAL_ARITH `a >= #13.0 ==> ~(a = &0)`) THEN
1413      ASM_REWRITE_TAC[REAL_ARITH `&2 pow 2 = #4.0`] THEN
1414      MATCH_MP_TAC (REWRITE_RULE [Tame_inequalities.INEQ_ALT; ALL] Tame_inequalities.delta_x_3_points) THEN
1415      REWRITE_TAC[DIST_0] THEN
1416
1417      SUBGOAL_THEN `!a. &2 <= a ==> #4.0 <= a pow 2` (fun th -> ASM_SIMP_TAC[th]) THENL
1418      [
1419        REPEAT STRIP_TAC THEN REWRITE_TAC[REAL_ARITH `#4.0 = &2 * &2`; REAL_POW_2] THEN
1420          MATCH_MP_TAC REAL_LE_MUL2 THEN
1421          ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC;
1422        ALL_TAC
1423      ] THEN
1424
1425      SUBGOAL_THEN `!a. &2 <= a /\ a <= &2 * h0 ==> a pow 2 <= #6.3504` (fun th -> ASM_SIMP_TAC[th]) THENL
1426      [
1427        REWRITE_TAC[Pack_defs.h0; REAL_ARITH `&2 * #1.26 = #2.52`] THEN
1428          REPEAT STRIP_TAC THEN REWRITE_TAC[REAL_ARITH `#6.3504 = #2.52 * #2.52`; REAL_POW_2] THEN
1429          MATCH_MP_TAC REAL_LE_MUL2 THEN
1430          ASM_SIMP_TAC[REAL_ARITH `&2 <= a ==> &0 <= a`];
1431        ALL_TAC
1432      ] THEN
1433
1434      MP_TAC (SPECL [`v1':real^3`; `v2':real^3`; `v3:real^3`] DIST_LOWER_BOUND_lemma) THEN
1435      ASM_REWRITE_TAC[in_ball_annulus] THEN
1436      DISCH_TAC THEN
1437      SUBGOAL_THEN `!a. &1 <= a /\ a <= &2 * h0 ==> #0.64 <= a pow 2 /\ a pow 2 <= #6.3504` (fun th -> ASM_SIMP_TAC[th]) THEN
1438      REWRITE_TAC[Pack_defs.h0; REAL_ARITH `&2 * #1.26 = #2.52`] THEN
1439      REPEAT STRIP_TAC THENL
1440      [
1441        REWRITE_TAC[REAL_ARITH `#0.64 = #0.8 * #0.8`; REAL_POW_2] THEN
1442          MATCH_MP_TAC REAL_LE_MUL2 THEN
1443          POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN
1444          REAL_ARITH_TAC;
1445        ALL_TAC
1446      ] THEN
1447      REWRITE_TAC[REAL_ARITH `#6.3504 = #2.52 * #2.52`; REAL_POW_2] THEN
1448      MATCH_MP_TAC REAL_LE_MUL2 THEN
1449      ASM_SIMP_TAC[REAL_ARITH `&1 <= a ==> &0 <= a`]);;
1450
1451
1452
1453
1454
1455 end;;