1 (* ========================================================================== *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
4 (* Chapter: Tame Hypermap *)
5 (* Author: Alexey Solovyev *)
7 (* (V,ESTD V) is a fan (3-point case) *)
8 (* ========================================================================== *)
10 flyspeck_needs "fan/fan_defs.hl";;
11 flyspeck_needs "packing/pack_defs.hl";;
13 flyspeck_needs "tame/Inequalities.hl";;
16 module Ckqowsa_3_points = struct
22 let REMOVE_ASSUM = POP_ASSUM (fun th -> ALL_TAC);;
26 let coplanar_eq_coplanar_alt = prove(`!s:real^N->bool. 2 <= dimindex(:N) ==> (coplanar s <=> coplanar_alt s)`,
28 ASM_SIMP_TAC[COPLANAR; Collect_geom.coplanar_alt]);;
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
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
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
51 REWRITE_TAC[DOT_LSUB; DOT_LMUL; DOT_SQUARE_NORM] THEN
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)`,
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
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]);;
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
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];
100 REWRITE_TAC[between; DIST_0] THEN
101 REPEAT (POP_ASSUM MP_TAC) THEN
102 REWRITE_TAC[DIST_SYM] THEN
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
119 REWRITE_TAC[DISJOINT; EXTENSION; IN_INTER; IN_INSERT; NOT_IN_EMPTY; DE_MORGAN_THM] 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
128 MAP_EVERY EXISTS_TAC [`t2:real`; `t3:real`] THEN
129 POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[] THEN
131 MAP_EVERY EXISTS_TAC [`&1 - t1 - t2`; `t1:real`; `t2:real`] THEN
132 ASM_REWRITE_TAC[] THEN CONJ_TAC THENL
137 POP_ASSUM MP_TAC THEN
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
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)`];
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
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
163 SUBGOAL_THEN `collinear {vec 0:real^3,v2,w}` MP_TAC THENL
165 ONCE_REWRITE_TAC[COLLINEAR_LEMMA_ALT] THEN
166 ASM_REWRITE_TAC[] THEN
167 EXISTS_TAC `t2:real` THEN
172 SUBGOAL_THEN `collinear {vec 0:real^3,v1,w}` MP_TAC THENL
174 ONCE_REWRITE_TAC[COLLINEAR_LEMMA_ALT] THEN
175 ASM_REWRITE_TAC[] THEN
176 EXISTS_TAC `t1:real` 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]);;
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
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];
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
209 ASM_REWRITE_TAC[REAL_MUL_LZERO; REAL_ADD_LID] THEN
210 ASM_CASES_TAC `t2 = &0` THENL
212 UNDISCH_TAC `w = t1 % v1 + t2 % v2:real^N` THEN
213 ASM_REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_LID];
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)`];
221 CONJ_TAC THEN MATCH_MP_TAC REAL_LTE_ADD THENL
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]
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]
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
249 ASM_REWRITE_TAC[VECTOR_MUL_EQ_0] THEN
250 REPEAT (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC;
253 ASM_SIMP_TAC[aff_ge_0_2] THEN
254 REWRITE_TAC[EXTENSION; IN_ELIM_THM] THEN
255 GEN_TAC THEN EQ_TAC THENL
258 MAP_EVERY EXISTS_TAC [`t1:real`; `t2 * inv(a)`] THEN
259 ASM_REWRITE_TAC[] THEN
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];
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
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]);;
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
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
293 REWRITE_TAC[DOT_LSUB; DOT_LMUL; DOT_SQUARE_NORM] THEN
294 POP_ASSUM MP_TAC THEN
299 SUBGOAL_THEN `!x:real^3. norm x = abs (norm x)` (fun th -> ONCE_REWRITE_TAC[th]) THENL
301 GEN_TAC THEN MP_TAC (ISPEC `x:real^3` NORM_POS_LE) 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
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
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);;
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
335 ASM_REWRITE_TAC[NORM_0; VECTOR_SUB_LZERO; NORM_NEG; REAL_ADD_LID];
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
343 POP_ASSUM (fun th -> ONCE_REWRITE_TAC[th]) THEN
344 ASM_REWRITE_TAC[DOT_RADD; DOT_RMUL] THEN
348 SUBGOAL_THEN `n2:real^N dot w = t1 * (n1 dot n2) + t2 * (n2 dot n2)` MP_TAC THENL
350 POP_ASSUM (fun th -> ONCE_REWRITE_TAC[th]) THEN
351 ASM_REWRITE_TAC[DOT_RADD; DOT_RMUL; DOT_SYM] THEN
355 POP_ASSUM (LABEL_TAC "A") THEN
356 ASM_REWRITE_TAC[] THEN
358 ASM_CASES_TAC `t2 = &0` THENL
360 ASM_REWRITE_TAC[] THEN
362 ASM_CASES_TAC `t1 = &0` THENL
364 REMOVE_THEN "A" MP_TAC THEN
365 ASM_REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_RID];
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];
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
377 REPLICATE_TAC 3 (POP_ASSUM MP_TAC) THEN
382 SUBGOAL_THEN `n1 dot n2:real^N <= &0` MP_TAC THENL
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
392 REMOVE_ASSUM THEN DISCH_TAC THEN
394 UNDISCH_TAC `~(n1 = vec 0:real^N)` THEN
395 REWRITE_TAC[GSYM NORM_EQ_0] THEN
397 SUBGOAL_THEN `(n1:real^N dot n2) pow 2 = (norm n1 pow 2) * (norm n2 pow 2)` ASSUME_TAC THENL
399 POP_ASSUM MP_TAC THEN
401 REPLICATE_TAC 3 (POP_ASSUM MP_TAC) THEN
402 REWRITE_TAC[DOT_SQUARE_NORM] THEN
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
412 REMOVE_ASSUM THEN POP_ASSUM MP_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
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
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
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
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
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
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
458 REWRITE_TAC[GSYM vector_norm; DOT_SQUARE_NORM] THEN
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
468 POP_ASSUM MP_TAC THEN
469 REWRITE_TAC[GSYM vector_norm; NORM_SUB] THEN
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]);;
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
489 REWRITE_TAC[GSYM NORM_EQ_0] THEN
490 ASM_SIMP_TAC[REAL_ARITH `&2 <= n ==> ~(n = &0)`];
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
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
507 MATCH_MP_TAC SQRT_MONO_LE THEN
510 CONV_TAC REAL_RAT_REDUCE_CONV;
514 MATCH_MP_TAC REAL_LE_MUL2 THEN
515 CONJ_TAC THENL [ REAL_ARITH_TAC; ALL_TAC ] THEN
518 REPEAT (POP_ASSUM MP_TAC) THEN
522 CONJ_TAC THENL [ REAL_ARITH_TAC; ALL_TAC ] THEN
524 MATCH_MP_TAC REAL_LE_MUL2 THEN
525 CONJ_TAC THENL [ REAL_ARITH_TAC; ALL_TAC ] THEN
528 REPEAT (POP_ASSUM MP_TAC) THEN
532 CONJ_TAC THENL [ REAL_ARITH_TAC; ALL_TAC ] THEN
534 MATCH_MP_TAC REAL_LE_MUL2 THEN
535 REPEAT (POP_ASSUM MP_TAC) THEN
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} /\
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
550 REWRITE_TAC[GSYM NORM_EQ_0] THEN
551 ASM_SIMP_TAC[REAL_ARITH `&2 <= n ==> ~(n = &0)`];
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
561 SUBGOAL_THEN `&1 <= sqrt (&3)` ASSUME_TAC THENL
563 ONCE_REWRITE_TAC[GSYM SQRT_1] THEN
564 MATCH_MP_TAC SQRT_MONO_LE THEN
569 MATCH_MP_TAC REAL_LE_TRANS THEN
570 EXISTS_TAC `#1.48 * sqrt(&3) / #1.26` THEN
573 POP_ASSUM MP_TAC THEN
578 MATCH_MP_TAC REAL_LE_TRANS THEN
579 EXISTS_TAC `(#1.48 * sqrt (&3) + #1.48 * sqrt (&3)) / (&2 * h0)` THEN
582 REWRITE_TAC[Sphere.h0] THEN
587 MATCH_MP_TAC REAL_LE_TRANS THEN
588 EXISTS_TAC `(norm (v1 cross w) + norm (v2 cross w)) / norm w` THEN
591 SUBGOAL_THEN `&0 < &2 * h0 /\ &0 < norm (w:real^3)` ASSUME_TAC THENL
593 ASM_SIMP_TAC[Sphere.h0; REAL_ARITH `&2 <= n ==> &0 < n`] THEN
597 ASM_SIMP_TAC[RAT_LEMMA4] THEN
598 MATCH_MP_TAC REAL_LE_MUL2 THEN
599 REPEAT CONJ_TAC THENL
601 REMOVE_ASSUM THEN POP_ASSUM MP_TAC THEN
603 MATCH_MP_TAC REAL_LE_ADD2 THEN
605 REWRITE_TAC[NORM_POS_LE];
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
628 POP_ASSUM (fun th -> REWRITE_TAC[th]) THEN
629 REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_LID] 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
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
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];
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
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
661 REPEAT CONJ_TAC THENL
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];
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`]);;
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
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];
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
703 POP_ASSUM (fun th -> REWRITE_TAC[th]) THEN
704 REWRITE_TAC[NORM_POW_2] THEN
708 ASM_REWRITE_TAC[] THEN
709 REWRITE_TAC[NORM_POW_2] THEN DISCH_TAC THEN
710 SUBGOAL_THEN `t1 <= &1` ASSUME_TAC THENL
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
721 ASM_REWRITE_TAC[DOT_POS_LT];
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
730 MATCH_MP_TAC REAL_LE_MUL THEN ASM_REWRITE_TAC[];
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`];
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
742 MATCH_MP_TAC REAL_LE_ADD THEN
745 MATCH_MP_TAC REAL_LE_MUL THEN
749 EXPAND_TAC "x" THEN MATCH_MP_TAC REAL_LE_MUL THEN
750 ASM_REWRITE_TAC[DOT_POS_LE];
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
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;
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
772 REMOVE_ASSUM THEN POP_ASSUM MP_TAC 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
779 POP_ASSUM MP_TAC 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
787 REWRITE_TAC[REAL_ARITH `&0 <= &1 - t1 * t1 <=> t1 * t1 <= &1 * &1`] THEN
788 MATCH_MP_TAC REAL_LE_MUL2 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]);;
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
809 MATCH_MP_TAC (GSYM ACS_COS) 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
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];
825 POP_ASSUM MP_TAC THEN REWRITE_TAC[DE_MORGAN_THM] THEN
826 SIMP_TAC[Trigonometry1.NORM_CAUCHY_SCHWARZ_FRAC]);;
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
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
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];
852 SUBGOAL_THEN `norm (u:real^N) > &0 /\ ~(norm u = &0)` ASSUME_TAC THENL
854 ASM_REWRITE_TAC[real_gt; NORM_POS_LT; NORM_EQ_0];
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
861 SUBGOAL_THEN `&0 < sin phi` ASSUME_TAC THENL
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];
873 SUBGOAL_THEN `(u dot u) * (v dot v) - (u:real^N dot v) pow 2 > &0` ASSUME_TAC THENL
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
880 REWRITE_TAC[Trigonometry2.SQUARE_NORM_CAUCHY_SCHWARZ_POW2];
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`];
891 SUBGOAL_THEN `e:real^N dot v = &0` ASSUME_TAC THENL
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
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
905 ABBREV_TAC `d = norm (u:real^N) pow 4 - (u dot v) pow 2` THEN
906 SUBGOAL_THEN `&0 < d` ASSUME_TAC THENL
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
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
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
926 SUBGOAL_THEN `e:real^N dot e = v:real^N dot v` ASSUME_TAC THENL
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
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
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
951 EXPAND_TAC "f" THEN BETA_TAC THEN
952 REWRITE_TAC[LIFT_DROP; REAL_MUL_RID] 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
958 (* f(t) = a v + b u *)
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
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
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
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
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
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];
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
1016 MATCH_MP_TAC REAL_LE_MUL THEN
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;
1027 MATCH_MP_TAC REAL_LE_INV THEN
1028 ASM_SIMP_TAC[REAL_LT_IMP_LE];
1033 (* f is continuous *)
1035 MATCH_MP_TAC CONTINUOUS_ON_ADD THEN
1036 CONJ_TAC THEN MATCH_MP_TAC CONTINUOUS_ON_VMUL THENL
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
1043 REWRITE_TAC[FUN_EQ_THM; o_THM];
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;
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
1058 REWRITE_TAC[FUN_EQ_THM; o_THM];
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
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
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];
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
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
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`];
1105 REWRITE_TAC[REAL_ARITH `v + w <= v + w - &2 * vw <=> vw <= &0`] THEN
1106 POP_ASSUM MP_TAC THEN
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
1121 REPEAT CONJ_TAC THENL
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
1130 REWRITE_TAC[FUN_EQ_THM; o_THM; dist];
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]
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]);;
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
1166 MP_TAC (SPECL [`v1:real^3`; `v2:real^3`; `v3:real^3`] in_aff_ge_0_2) THEN
1167 ASM_REWRITE_TAC[] THEN
1169 POP_ASSUM (LABEL_TAC "A" o SYM) THEN
1171 ABBREV_TAC `u:real^3 = (norm (v1:real^3) / norm (v3:real^3)) % v3` THEN
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
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
1183 ASM_REWRITE_TAC[DOT_POS_LT];
1186 ASM_REWRITE_TAC[GSYM real_gt];
1190 SUBGOAL_THEN `dist (u,v3:real^3) < &2` ASSUME_TAC THENL
1192 REWRITE_TAC[dist] 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
1198 ASM_SIMP_TAC[REAL_ARITH `&2 <= n3 ==> n3 = abs(n3)`];
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
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
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`];
1226 ASM_SIMP_TAC[VECTOR_MUL_LID];
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
1234 REWRITE_TAC[REAL_ABS_REFL] THEN
1235 MATCH_MP_TAC REAL_LE_DIV THEN
1236 REWRITE_TAC[NORM_POS_LE];
1239 ASM_SIMP_TAC[REAL_FIELD `&2 <= n3 ==> n1 / n3 * n3 = n1`];
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
1247 EXISTS_TAC `(f:real^1->real^3) t` THEN
1248 ASM_REWRITE_TAC[] THEN
1250 SUBGOAL_THEN `aff_ge {vec 0} {v1:real^3,v3} = aff_ge {vec 0} {v1,u}` ASSUME_TAC THENL
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`];
1262 ASM_REWRITE_TAC[GSYM NORM_EQ_0] THEN
1263 ASM_REWRITE_TAC[NORM_EQ_0];
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
1276 ASM_REWRITE_TAC[GSYM NORM_EQ_0] THEN
1277 ASM_REWRITE_TAC[NORM_EQ_0];
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
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
1293 MAP_EVERY EXISTS_TAC [`t1' + t2' * t1:real`; `t2' * t2:real`] THEN
1294 REPEAT CONJ_TAC THENL
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];
1304 POP_ASSUM MP_TAC THEN
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) /\
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
1327 MP_TAC (SPECL [`v2:real^3`; `v1':real^3`; `v3:real^3`] lemma_3_points) THEN
1330 ASM_REWRITE_TAC[] THEN
1333 ASM_REWRITE_TAC[SET_RULE `{v2,v1'} = {v1',v2}`];
1336 ASM_SIMP_TAC[DIST_SYM; real_ge; REAL_LE_REFL];
1340 DISCH_THEN (X_CHOOSE_THEN `v2':real^3` MP_TAC) THEN
1342 MAP_EVERY EXISTS_TAC [`v1':real^3`; `v2':real^3`] THEN
1343 ASM_REWRITE_TAC[] THEN
1346 ASSUME_TAC (SET_RULE `{v1':real^3,v2'} = {v2',v1'}`) THEN
1347 POP_ASSUM (fun th -> ONCE_REWRITE_TAC [th]) THEN
1349 REMOVE_ASSUM THEN POP_ASSUM MP_TAC THEN
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) /\
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
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
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
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
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
1385 MAP_EVERY EXISTS_TAC [`&1`; `&0`; `&0`] THEN
1386 ASM_REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_LID] THEN
1388 MAP_EVERY EXISTS_TAC [`&0`; `&1`; `&0`] THEN
1389 ASM_REWRITE_TAC[VECTOR_MUL_LID; VECTOR_MUL_LZERO; VECTOR_ADD_RID] THEN
1391 MAP_EVERY EXISTS_TAC [`&0`; `&0`; `&1`] THEN
1392 ASM_REWRITE_TAC[VECTOR_MUL_LID; VECTOR_MUL_LZERO; VECTOR_ADD_LID] THEN
1396 SUBGOAL_THEN `~(v1':real^3 = vec 0) /\ ~(v2':real^3 = vec 0)` ASSUME_TAC THENL
1398 REWRITE_TAC[GSYM NORM_EQ_0] THEN
1399 ASM_SIMP_TAC[REAL_ARITH `&2 <= norm n ==> ~(norm n = &0)`];
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
1406 MAP_EVERY EXISTS_TAC [`&1 - t1 - t2`; `t1:real`; `t2:real`] THEN
1407 ASM_REWRITE_TAC[] THEN
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
1417 SUBGOAL_THEN `!a. &2 <= a ==> #4.0 <= a pow 2` (fun th -> ASM_SIMP_TAC[th]) THENL
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;
1425 SUBGOAL_THEN `!a. &2 <= a /\ a <= &2 * h0 ==> a pow 2 <= #6.3504` (fun th -> ASM_SIMP_TAC[th]) THENL
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`];
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
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
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
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`]);;