1 (* ========================================================================== *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
4 (* Chapter: Tame Hypermap *)
5 (* Author: Alexey Solovyev *)
7 (* (V,ESTD V) is a fan (4-point case) *)
8 (* ========================================================================== *)
10 flyspeck_needs "tame/CKQOWSA_3.hl";;
13 module Ckqowsa_4_points = struct
16 open Ckqowsa_3_points;;
22 let IN_INTERVAL_1 = prove(`!a b c. lift c IN interval [lift a, lift b] <=> a <= c /\ c <= b`,
24 SIMP_TAC[IN_INTERVAL; DIMINDEX_1; ARITH_RULE `1 <= i /\ i <= 1 <=> i = 1`] THEN
25 REWRITE_TAC[GSYM drop; LIFT_DROP] THEN
26 EQ_TAC THEN SIMP_TAC[] THEN
27 DISCH_THEN (MP_TAC o SPEC `1`) THEN
31 let DIST_SQR = prove(`!v (w:real^N) d. dist(v,w) = d <=> dist(v,w) pow 2 = d pow 2 /\ &0 <= d`,
32 REPEAT STRIP_TAC THEN EQ_TAC THEN STRIP_TAC THENL
34 FIRST_X_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN
35 REWRITE_TAC[DIST_POS_LE];
36 ASSUME_TAC (REAL_ARITH `!d. &0 <= d ==> d = abs(d)`) THEN
37 FIRST_ASSUM (MP_TAC o SPEC `d:real`) THEN
38 FIRST_X_ASSUM (MP_TAC o SPEC `dist(v:real^N,w)`) THEN
39 ASM_REWRITE_TAC[DIST_POS_LE] THEN
40 REPLICATE_TAC 2 (DISCH_THEN (fun th -> ONCE_REWRITE_TAC[th])) THEN
41 ASM_REWRITE_TAC[REAL_EQ_SQUARE_ABS]
45 let estd_non_collinear_lemma = prove(`!v w. v IN ball_annulus /\ w IN ball_annulus /\
46 &2 <= dist (v,w) /\ dist (v,w) <= &2 * h0
47 ==> ~collinear {vec 0, v, w}`,
48 REWRITE_TAC[in_ball_annulus] THEN
49 REWRITE_TAC[COLLINEAR_BETWEEN_CASES; between; DIST_0; DIST_SYM] THEN
50 REWRITE_TAC[Sphere.h0] THEN
55 let zero_not_between = prove(`!v w:real^N. ~between (vec 0) (v, w) ==> ~(v = vec 0) /\ ~(w = vec 0) /\
56 (!a b. a < &0 /\ &0 < b ==> ~(a % w = b % v))`,
57 REPEAT GEN_TAC THEN DISCH_TAC THEN
58 SUBGOAL_THEN `~(v = vec 0:real^N) /\ ~(w = vec 0:real^N)` ASSUME_TAC THENL
61 REWRITE_TAC[GSYM NORM_EQ_0] THEN
62 REWRITE_TAC[between; DIST_0] THEN
63 ASM_CASES_TAC `norm (v:real^N) = &0` THEN ASM_REWRITE_TAC[] THENL
65 POP_ASSUM MP_TAC THEN REWRITE_TAC[NORM_EQ_0] THEN
66 DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
67 REWRITE_TAC[DIST_0; REAL_ADD_LID];
70 ASM_CASES_TAC `norm (w:real^N) = &0` THEN ASM_REWRITE_TAC[] THEN
71 POP_ASSUM MP_TAC THEN REWRITE_TAC[NORM_EQ_0] THEN
72 DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
73 REWRITE_TAC[DIST_0; REAL_ADD_RID];
76 ASM_REWRITE_TAC[] THEN
79 UNDISCH_TAC `~between (vec 0:real^N) (v,w)` THEN
80 REWRITE_TAC[between; DIST_0] THEN
81 POP_ASSUM (MP_TAC o AP_TERM `\v:real^N. inv(a) % v`) THEN
82 REWRITE_TAC[VECTOR_MUL_ASSOC] THEN
83 ASM_SIMP_TAC[REAL_ARITH `a < &0 ==> ~(a = &0)`; REAL_MUL_LINV; VECTOR_MUL_LID] THEN
85 REWRITE_TAC[dist; VECTOR_ARITH `v - a % v = (&1 - a) % v:real^N`] THEN
86 REWRITE_TAC[NORM_MUL] THEN
88 SUBGOAL_THEN `&0 <= --(inv a * b)` ASSUME_TAC THENL
90 REWRITE_TAC[REAL_ARITH `&0 <= --(a * b) <=> &0 <= --a * b`] THEN
91 MATCH_MP_TAC REAL_LE_MUL THEN
92 ASM_SIMP_TAC[REAL_LT_IMP_LE] THEN
93 REWRITE_TAC[GSYM REAL_INV_NEG] THEN
94 MATCH_MP_TAC REAL_LE_INV THEN
95 ASM_SIMP_TAC[REAL_ARITH `a < &0 ==> &0 <= --a`];
99 SUBGOAL_THEN `abs (&1 - inv a * b) = &1 - inv a * b` (fun th -> REWRITE_TAC[th]) THENL
101 REWRITE_TAC[REAL_ABS_REFL] THEN
102 REWRITE_TAC[REAL_ARITH `&1 - a = &1 + (--a)`] THEN
103 MATCH_MP_TAC REAL_LE_ADD THEN
104 ASM_REWRITE_TAC[REAL_LE_01];
108 SUBGOAL_THEN `abs (inv a * b) = --(inv a * b)` (fun th -> REWRITE_TAC[th]) THENL
110 POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;
117 let zero_not_between_estd = prove(`!v w. v IN ball_annulus /\ w IN ball_annulus /\ dist (v,w) <= &2 * h0
118 ==> ~between (vec 0) (v,w)`,
119 REWRITE_TAC[in_ball_annulus; between; DIST_0; Sphere.h0] THEN
124 (******************************************************************)
126 (* Some properties of projections *)
128 let projection = Sphere.projection;;
131 let PROJECTION_ORTHOGONAL = prove(`!d v:real^N. projection d v dot d = &0`,
132 REWRITE_TAC[DOT_SYM; projection; VECTOR_SUB_PROJECT_ORTHOGONAL]);;
135 let VECTOR_PROJECTION = prove(`!d v:real^N. v = projection d v + (v dot d) / (d dot d) % d`,
136 REWRITE_TAC[projection] THEN VECTOR_ARITH_TAC);;
140 let PROJECTION_0 = prove(`!d:real^N. projection d (vec 0) = vec 0`,
141 REWRITE_TAC[projection; DOT_LZERO; real_div; REAL_MUL_LZERO] THEN
145 let PROJECTION_ZERO = prove(`!d:real^N. ~(d = vec 0) ==> projection d d = vec 0`,
146 REWRITE_TAC[GSYM NORM_EQ_0] THEN GEN_TAC THEN DISCH_TAC THEN
147 REWRITE_TAC[NORM_EQ_0; projection; DOT_SQUARE_NORM] THEN
148 SUBGOAL_THEN `norm d pow 2 / norm (d:real^N) pow 2 = &1` (fun th -> REWRITE_TAC[th]) THENL
150 REWRITE_TAC[real_div; REAL_POW_2; REAL_INV_MUL] THEN
151 REWRITE_TAC[REAL_ARITH `(d * d) * id * id = d * (d * id) * id`] THEN
152 ASM_SIMP_TAC[REAL_MUL_RINV; REAL_MUL_LID];
158 let PROJECTION_LINEAR = prove(`!(d:real^N) v w a. projection d (v + w) = projection d v + projection d w /\
159 projection d (a % v) = a % projection d v`,
161 REWRITE_TAC[projection; DOT_LMUL; DOT_LADD; real_div; REAL_ADD_RDISTRIB; VECTOR_SUB_LDISTRIB; VECTOR_MUL_ASSOC; REAL_MUL_ASSOC] THEN
162 REWRITE_TAC[VECTOR_ADD_RDISTRIB] THEN
166 let PROJECTION_NEG = prove(`!(d:real^N) v. projection d (--v) = --projection d v`,
167 REWRITE_TAC[VECTOR_ARITH `--v:real^N = -- &1 % v`; PROJECTION_LINEAR]);;
170 let PROJECTION_SUB = prove(`!(d:real^N) v w. projection d (v - w) = projection d v - projection d w`,
171 REWRITE_TAC[VECTOR_ARITH `a - b:real^N = a + (--b)`; PROJECTION_LINEAR; PROJECTION_NEG]);;
175 let PROJECTION_DIST2 = prove(`!d v w:real^N. ~(d = vec 0) ==>
176 dist (projection d v, projection d w) pow 2 = dist (v,w) pow 2 - ((v - w) dot d) pow 2 / (norm d pow 2)`,
177 REWRITE_TAC[GSYM NORM_EQ_0] THEN REPEAT STRIP_TAC THEN
178 REWRITE_TAC[dist; projection] THEN
179 REWRITE_TAC[VECTOR_ARITH `v - a % d - (w - b % d) = (v - w) - (a - b) % d:real^N`] THEN
181 ABBREV_TAC `x = v - w:real^N` THEN
182 ABBREV_TAC `y = ((v dot d) / (d dot d) - (w dot d) / (d dot d)) % d:real^N` THEN
184 SUBGOAL_THEN `!a. a / (d dot d) * (d dot d:real^N) = a` ASSUME_TAC THENL
186 REWRITE_TAC[real_div; DOT_SQUARE_NORM; REAL_POW_2; REAL_INV_MUL] THEN
187 REWRITE_TAC[REAL_ARITH `(a * id * id) * d * d = a * (id * (id * d) * d)`] THEN
188 ASM_SIMP_TAC[REAL_MUL_LINV; REAL_MUL_LID; REAL_MUL_RID];
192 SUBGOAL_THEN `x:real^N dot y = y dot y` ASSUME_TAC THENL
195 REWRITE_TAC[real_div] THEN
196 REWRITE_TAC[GSYM REAL_SUB_RDISTRIB; GSYM DOT_LSUB] THEN
198 REWRITE_TAC[DOT_LMUL; DOT_RMUL; DOT_SYM] THEN
199 REWRITE_TAC[REAL_ARITH `(dv * id) * (dv * id) * d = ((dv * dv * id) * id) * d`] THEN
200 ASM_REWRITE_TAC[GSYM real_div] THEN
205 ASM_REWRITE_TAC[NORM_POW_2; DOT_LSUB; DOT_RSUB; DOT_SYM] THEN
206 REWRITE_TAC[REAL_ARITH `x - y - (y - y) = x - z <=> y = z`] THEN
208 REWRITE_TAC[real_div] THEN
209 ASM_REWRITE_TAC[GSYM REAL_SUB_RDISTRIB; GSYM DOT_LSUB] THEN
210 REWRITE_TAC[DOT_LMUL; DOT_RMUL] THEN
211 ASM_REWRITE_TAC[GSYM real_div; DOT_SYM] THEN
216 let PROJECTION_SUM_DIST = prove(`!(d:real^N) x y a b. x dot d = &0 /\ y dot d = &0
217 ==> dist (x + a % d, y + b % d) pow 2 = dist (x, y) pow 2 + (a - b) pow 2 * (d dot d)`,
218 REPEAT STRIP_TAC THEN
219 GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [dist] THEN
220 REWRITE_TAC[VECTOR_ARITH `(x + a % d) - (y + b % d) = (x - y) + (a - b) % d:real^N`] THEN
221 SUBGOAL_THEN `(x - y:real^N) dot ((a - b) % d) = &0` ASSUME_TAC THENL
223 ASM_REWRITE_TAC[DOT_RMUL; DOT_LSUB; REAL_MUL_RZERO; REAL_SUB_RZERO];
226 ASM_SIMP_TAC[Trigonometry2.PITHAGO_THEOREM] THEN
227 REWRITE_TAC[GSYM dist] THEN
228 REWRITE_TAC[NORM_MUL; REAL_POW_MUL; REAL_POW2_ABS; DOT_SQUARE_NORM]);;
232 let PROJECTION_DIST_SPECIAL_EQ = prove(`!d x v w:real^N. ~(d = vec 0) /\ x dot d = &0
233 ==> dist (x + (v - projection d v), w) pow 2 = dist (x, projection d w) pow 2 - dist (projection d v, projection d w) pow 2 + dist (v, w) pow 2`,
234 REWRITE_TAC[GSYM NORM_EQ_0] THEN
235 REPEAT STRIP_TAC THEN
236 SUBGOAL_THEN `!a. a / (d dot d) * (d dot d:real^N) = a` ASSUME_TAC THENL
238 REWRITE_TAC[real_div; DOT_SQUARE_NORM; REAL_POW_2; REAL_INV_MUL] THEN
239 REWRITE_TAC[REAL_ARITH `(a * id * id) * d * d = a * (id * (id * d) * d)`] THEN
240 ASM_SIMP_TAC[REAL_MUL_LINV; REAL_MUL_LID; REAL_MUL_RID];
244 SUBGOAL_THEN `dist (x + v - projection d v, w) pow 2 = dist (x, projection d w) pow 2 + ((v - w) dot d:real^N) pow 2 / norm d pow 2` (fun th -> REWRITE_TAC[th]) THENL
246 MP_TAC (SPECL [`d:real^N`; `w:real^N`] VECTOR_PROJECTION) THEN
247 DISCH_THEN (fun th -> GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [th]) THEN
248 SUBGOAL_THEN `v - projection d (v:real^N) = (v dot d) / (d dot d) % d` (fun th -> REWRITE_TAC[th]) THENL
250 REWRITE_TAC[projection] THEN
254 ASM_SIMP_TAC[PROJECTION_ORTHOGONAL; PROJECTION_SUM_DIST] THEN
255 REWRITE_TAC[real_div] THEN
256 REWRITE_TAC[GSYM REAL_SUB_RDISTRIB; GSYM DOT_LSUB] THEN
257 REWRITE_TAC[REAL_ARITH `(a * b) pow 2 * c = ((a pow 2 * b) * b) * c`] THEN
258 ASM_REWRITE_TAC[GSYM real_div; NORM_POW_2];
261 MP_TAC (SPECL [`d:real^N`; `v:real^N`; `w:real^N`] PROJECTION_DIST2) THEN
262 ASM_REWRITE_TAC[GSYM NORM_EQ_0] THEN
267 let PROJECTION_DIST_SPECIAL_LE = prove(`!d x v w:real^N. ~(d = vec 0) /\ x dot d = &0 /\ dist (x, projection d w) <= dist (projection d v, projection d w)
268 ==> dist (x + v - projection d v, w) <= dist (v, w)`,
269 REPEAT STRIP_TAC THEN
270 POP_ASSUM MP_TAC THEN
271 REWRITE_TAC[dist] THEN ONCE_REWRITE_TAC[GSYM REAL_ABS_NORM] THEN
272 REWRITE_TAC[REAL_LE_SQUARE_ABS] THEN
273 REWRITE_TAC[GSYM dist] THEN
274 ASM_SIMP_TAC[PROJECTION_DIST_SPECIAL_EQ] THEN
279 (***********************************************)
282 (* General properties of affine hull and aff_ge *)
284 let aff_ge_0_2_eq_segment = prove(`!v:real^N. aff_ge {vec 0} {vec 0,v} = segment [vec 0,v] /\ aff_ge {vec 0} {v,vec 0} = segment [vec 0,v]`,
286 REWRITE_TAC[SET_RULE `{v:real^N, vec 0} = {vec 0,v}`] THEN
287 ONCE_REWRITE_TAC[AFF_GE_DISJOINT_DIFF] THEN
288 REWRITE_TAC[SET_RULE `{vec 0} DIFF {vec 0,v:real^N} = {}`] THEN
289 REWRITE_TAC[GSYM CONVEX_HULL_AFF_GE; SEGMENT_CONVEX_HULL]);;
292 let in_segment_imp_in_aff_ge_0_2 = prove(`!v v1 v2:real^N. v IN segment [v1,v2] ==> v IN aff_ge {vec 0} {v1,v2}`,
294 ASM_CASES_TAC `v1:real^N = vec 0` THENL
296 ASM_SIMP_TAC[aff_ge_0_2_eq_segment];
299 ASM_CASES_TAC `v2:real^N = vec 0` THENL
301 ASM_REWRITE_TAC[aff_ge_0_2_eq_segment; SEGMENT_SYM];
304 ASM_SIMP_TAC[aff_ge_0_2] THEN
305 REWRITE_TAC[IN_SEGMENT; IN_ELIM_THM] THEN
307 MAP_EVERY EXISTS_TAC [`&1 - u`; `u:real`] THEN
308 ASM_REWRITE_TAC[] THEN
309 UNDISCH_TAC `u <= &1` THEN REAL_ARITH_TAC);;
313 let points_in_aff_ge_0_2 = prove(`!v1 v2:real^N. vec 0 IN aff_ge {vec 0} {v1, v2} /\
314 v1 IN aff_ge {vec 0} {v1, v2} /\
315 v2 IN aff_ge {vec 0} {v1, v2}`,
317 ASM_CASES_TAC `v1:real^N = vec 0` THENL
319 ASM_REWRITE_TAC[aff_ge_0_2_eq_segment; ENDS_IN_SEGMENT];
322 ASM_CASES_TAC `v2:real^N = vec 0` THENL
324 ASM_REWRITE_TAC[aff_ge_0_2_eq_segment; ENDS_IN_SEGMENT];
327 ASM_SIMP_TAC[aff_ge_0_2; IN_ELIM_THM] THEN
328 REPEAT CONJ_TAC THENL
330 MAP_EVERY EXISTS_TAC [`&0`; `&0`];
331 MAP_EVERY EXISTS_TAC [`&1`; `&0`];
332 MAP_EVERY EXISTS_TAC [`&0`; `&1`]
334 REWRITE_TAC[REAL_LE_REFL; REAL_LE_01; VECTOR_MUL_LZERO; VECTOR_ADD_LID; VECTOR_MUL_LID; VECTOR_ADD_RID]);;
338 let aff_ge_0_2_SUBSET = prove(`!v1 v2 v w:real^N. ~(v1 = vec 0) /\ ~(v2 = vec 0) /\
339 v IN aff_ge {vec 0} {v1,v2} /\ w IN aff_ge {vec 0} {v1,v2}
340 ==> aff_ge {vec 0} {v,w} SUBSET aff_ge {vec 0} {v1,v2}`,
341 REPEAT STRIP_TAC THEN
342 MP_TAC (ISPECL [`{vec 0:real^N}`; `{v1:real^N,v2}`] CONVEX_AFF_GE) THEN
343 REWRITE_TAC[CONVEX_CONTAINS_SEGMENT] THEN DISCH_TAC THEN
344 ASM_CASES_TAC `v:real^N = vec 0` THENL
346 ASM_REWRITE_TAC[aff_ge_0_2_eq_segment] THEN
347 FIRST_X_ASSUM MATCH_MP_TAC THEN
348 ASM_REWRITE_TAC[points_in_aff_ge_0_2];
351 ASM_CASES_TAC `w:real^N = vec 0` THENL
353 ASM_REWRITE_TAC[aff_ge_0_2_eq_segment] THEN
354 FIRST_X_ASSUM MATCH_MP_TAC THEN
355 ASM_REWRITE_TAC[points_in_aff_ge_0_2];
358 REPEAT (FIRST_X_ASSUM (MP_TAC o check (is_binary "IN" o concl))) THEN
359 ASM_SIMP_TAC[aff_ge_0_2; IN_ELIM_THM; SUBSET] THEN
360 REPEAT STRIP_TAC THEN
361 MAP_EVERY EXISTS_TAC [`t1'' * t1 + t2'' * t1'`; `t1'' * t2 + t2'' * t2'`] THEN
362 REWRITE_TAC[CONJ_ASSOC] THEN
365 CONJ_TAC THEN MATCH_MP_TAC REAL_LE_ADD THEN CONJ_TAC THEN MATCH_MP_TAC REAL_LE_MUL THEN ASM_REWRITE_TAC[];
368 ASM_REWRITE_TAC[] THEN
373 let segment_inter_aff_ge_ends = prove(`!v1 v2 v w n:real^N. ~(v1 = vec 0) /\ ~(v2 = vec 0) /\
374 v1 dot n = &0 /\ v2 dot n = &0 /\
375 v dot n = &0 /\ ~(w dot n = &0) /\
376 ~(segment [v,w] INTER aff_ge {vec 0} {v1,v2} = {})
377 ==> v IN aff_ge {vec 0} {v1,v2}`,
378 REPEAT STRIP_TAC THEN
379 POP_ASSUM MP_TAC THEN
380 REWRITE_TAC[GSYM MEMBER_NOT_EMPTY] THEN
381 REWRITE_TAC[IN_INTER; IN_SEGMENT] THEN
382 REPEAT STRIP_TAC THEN
383 FIRST_ASSUM MP_TAC THEN
384 SUBGOAL_THEN `?t1 t2. &0 <= t1 /\ &0 <= t2 /\ x = t1 % v1 + t2 % v2:real^N` MP_TAC THENL
386 POP_ASSUM MP_TAC THEN
387 ASM_SIMP_TAC[aff_ge_0_2; IN_ELIM_THM];
391 SUBGOAL_THEN `u = &0` ASSUME_TAC THENL
393 POP_ASSUM (MP_TAC o AP_TERM `\v:real^N. v dot n`) THEN
394 FIRST_X_ASSUM (MP_TAC o AP_TERM `\v:real^N. v dot n`) THEN
395 DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
396 ASM_REWRITE_TAC[DOT_LADD; DOT_LMUL; REAL_MUL_RZERO; REAL_ADD_LID] THEN
397 UNDISCH_TAC `~(w dot n:real^N = &0)` THEN
401 UNDISCH_TAC `x = (&1 - u) % v + u % w:real^N` THEN
402 POP_ASSUM (fun th -> REWRITE_TAC[th]) THEN
404 REWRITE_TAC[REAL_SUB_RZERO; VECTOR_MUL_LZERO; VECTOR_MUL_LID; VECTOR_ADD_RID] THEN
405 DISCH_THEN (fun th -> ASM_REWRITE_TAC[SYM th]));;
410 let in_affine_hull_lemma = prove(`!v1 v2 v:real^N. ~collinear {vec 0,v1,v2} /\ v IN affine hull {vec 0,v1,v2}
411 ==> ?t1 t2. v = t1 % v1 + t2 % v2 /\
412 (!t1' t2'. v = t1' % v1 + t2' % v2 ==> t1' = t1 /\ t2' = t2)`,
413 REWRITE_TAC[AFFINE_HULL_3; IN_ELIM_THM] THEN
414 REWRITE_TAC[VECTOR_MUL_RZERO; VECTOR_ADD_LID] THEN
415 REPEAT STRIP_TAC THEN
416 UNDISCH_TAC `~collinear {vec 0,v1,v2:real^N}` THEN DISCH_TAC THEN
417 FIRST_ASSUM MP_TAC THEN REWRITE_TAC[COLLINEAR_LEMMA] THEN
418 FIRST_X_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[SET_RULE `{vec 0:real^N,v1,v2} = {vec 0,v2,v1}`] THEN
419 REWRITE_TAC[COLLINEAR_LEMMA; DE_MORGAN_THM; NOT_EXISTS_THM] THEN
420 REPEAT STRIP_TAC THEN
422 MAP_EVERY EXISTS_TAC [`v':real`; `w:real`] THEN
423 ASM_REWRITE_TAC[] THEN
424 REPEAT STRIP_TAC THENL
426 ASM_CASES_TAC `t1' = v':real` THEN ASM_REWRITE_TAC[] THEN
427 SUBGOAL_TAC "A" `~(v' - t1' = &0)` [ POP_ASSUM MP_TAC THEN REAL_ARITH_TAC ] THEN
428 FIRST_X_ASSUM (MP_TAC o check (is_eq o concl)) THEN
429 REWRITE_TAC[VECTOR_ARITH `t1 % v1 + t2 % v2 = t1' % v1 + t2' % v2 <=> (t1 - t1') % v1 = (t2' - t2) % v2:real^N`] THEN
430 DISCH_THEN (MP_TAC o AP_TERM `(\v:real^N. inv(v' - t1') % v)`) THEN BETA_TAC THEN
431 REWRITE_TAC[VECTOR_MUL_ASSOC] THEN
432 ASM_SIMP_TAC[REAL_MUL_LINV; VECTOR_MUL_LID];
433 ASM_CASES_TAC `t2' = w:real` THEN ASM_REWRITE_TAC[] THEN
434 SUBGOAL_TAC "A" `~(w - t2' = &0)` [ POP_ASSUM MP_TAC THEN REAL_ARITH_TAC ] THEN
435 FIRST_X_ASSUM (MP_TAC o check (is_eq o concl)) THEN
436 REWRITE_TAC[VECTOR_ARITH `t1 % v1 + t2 % v2 = t1' % v1 + t2' % v2 <=> (t2 - t2') % v2 = (t1' - t1) % v1:real^N`] THEN
437 DISCH_THEN (MP_TAC o AP_TERM `(\v:real^N. inv(w - t2') % v)`) THEN BETA_TAC THEN
438 REWRITE_TAC[VECTOR_MUL_ASSOC] THEN
439 ASM_SIMP_TAC[REAL_MUL_LINV; VECTOR_MUL_LID]
445 let affine_hull_3_plane = prove(`!v1 v2 n:real^3. ~collinear {vec 0,v1,v2} /\ ~(n = vec 0) /\
446 v1 dot n = &0 /\ v2 dot n = &0
447 ==> affine hull {vec 0,v1,v2} = {v | v dot n = &0}`,
448 REPEAT STRIP_TAC THEN
449 SUBGOAL_THEN `dim {n,v1,v2:real^3} = 3` ASSUME_TAC THENL
451 ONCE_REWRITE_TAC[DIM_INSERT] THEN
452 SUBGOAL_THEN `~(n IN span {v1,v2:real^3})` (fun th -> REWRITE_TAC[th]) THENL
454 REWRITE_TAC[SPAN_2; IN_UNIV; IN_ELIM_THM] THEN
456 POP_ASSUM (MP_TAC o AP_TERM `(dot) (n:real^3)`) THEN
457 POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN
458 SIMP_TAC[DOT_RADD; DOT_RMUL; DOT_SYM] THEN
459 ASM_REWRITE_TAC[REAL_MUL_RZERO; REAL_ADD_LID; DOT_EQ_0];
463 ONCE_REWRITE_TAC[DIM_INSERT] THEN
464 SUBGOAL_THEN `~(v1:real^3 IN span {v2})` (fun th -> REWRITE_TAC[th]) THENL
466 REWRITE_TAC[SPAN_SING; IN_ELIM_THM; IN_UNIV] THEN
467 UNDISCH_TAC `~collinear {vec 0:real^3,v1,v2}` THEN
468 ONCE_REWRITE_TAC[SET_RULE `{vec 0:real^3,v1,v2} = {vec 0,v2,v1}`] THEN
469 SIMP_TAC[COLLINEAR_LEMMA; DE_MORGAN_THM];
472 REWRITE_TAC[DIM_SING] THEN
473 UNDISCH_TAC `~collinear {vec 0:real^3,v1,v2}` THEN
474 SIMP_TAC[COLLINEAR_LEMMA; DE_MORGAN_THM] THEN
478 MP_TAC (ISPEC `{n:real^3,v1,v2}` DIM_EQ_FULL) THEN
479 ASM_REWRITE_TAC[AFFINE_HULL_3; DIMINDEX_3; SPAN_3; IN_UNIV; EXTENSION; IN_ELIM_THM] THEN DISCH_TAC THEN
480 REWRITE_TAC[VECTOR_MUL_RZERO; VECTOR_ADD_LID] THEN
484 STRIP_TAC THEN ASM_REWRITE_TAC[DOT_LADD; DOT_LMUL; REAL_MUL_RZERO; REAL_ADD_RID];
487 POP_ASSUM (MP_TAC o SPEC `x:real^3`) THEN
488 STRIP_TAC THEN ASM_REWRITE_TAC[DOT_LADD; DOT_LMUL; REAL_MUL_RZERO; REAL_ADD_RID] THEN
489 ASM_REWRITE_TAC[REAL_ENTIRE; DOT_EQ_0] THEN
491 MAP_EVERY EXISTS_TAC [`&1 - v - w`; `v:real`; `w:real`] THEN
492 CONJ_TAC THENL [ REAL_ARITH_TAC; ALL_TAC ] THEN
493 ASM_REWRITE_TAC[] THEN VECTOR_ARITH_TAC);;
498 let intersection_point_exists = prove(`!v1 v2 n v w:real^3.
499 ~collinear {vec 0,v1,v2} /\ ~(n = vec 0) /\
500 v1 dot n = &0 /\ v2 dot n = &0 /\
503 ==> ?p. p IN segment [v,w] INTER affine hull {vec 0,v1,v2}`,
504 REPEAT STRIP_TAC THEN
505 ASM_SIMP_TAC[IN_INTER; IN_SEGMENT; affine_hull_3_plane; IN_ELIM_THM] THEN
506 ABBREV_TAC `d = (\u. ((&1 - u) % v + u % w) dot n:real^3)` THEN
507 SUBGOAL_THEN `?u. (&0 <= u /\ u <= &1) /\ d u = &0` ASSUME_TAC THENL
509 REWRITE_TAC[GSYM IN_REAL_INTERVAL] THEN
510 MATCH_MP_TAC REAL_IVT_INCREASING THEN
511 REWRITE_TAC[REAL_LE_01] THEN
513 ASM_REWRITE_TAC[REAL_SUB_RZERO; VECTOR_MUL_LZERO; VECTOR_ADD_RID; VECTOR_MUL_LID; REAL_SUB_REFL] THEN
514 ASM_REWRITE_TAC[VECTOR_ADD_LID] THEN
516 REWRITE_TAC[VECTOR_ARITH `((&1 - u) % v + u % w:real^3) dot n = v dot n + u * ((w - v) dot n)`] THEN
517 MATCH_MP_TAC REAL_CONTINUOUS_ON_ADD THEN
518 REWRITE_TAC[REAL_CONTINUOUS_ON_CONST] THEN
519 MATCH_MP_TAC REAL_CONTINUOUS_ON_MUL THEN
520 REWRITE_TAC[REAL_CONTINUOUS_ON_CONST; REAL_CONTINUOUS_ON_ID];
523 POP_ASSUM MP_TAC THEN STRIP_TAC THEN
524 EXISTS_TAC `(&1 - u) % v + u % w:real^3` THEN
525 POP_ASSUM MP_TAC THEN EXPAND_TAC "d" THEN SIMP_TAC[] THEN
527 EXISTS_TAC `u:real` THEN ASM_REWRITE_TAC[]);;
533 let aux_ineq = prove(`!a b x. &0 < a /\ &0 < b /\ x = (&1 - a * a - b * b) / (&2 * a * b) /\ -- &1 <= x /\ x <= &1
534 ==> x * (&1 - a) <= b`,
536 REWRITE_TAC[GSYM IMP_IMP] THEN
537 DISCH_TAC THEN DISCH_TAC THEN
538 DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
539 REPEAT DISCH_TAC THEN
541 SUBGOAL_THEN `&0 < &2 * a * b` ASSUME_TAC THENL
543 MATCH_MP_TAC REAL_LT_MUL THEN
544 REWRITE_TAC[REAL_ARITH `&0 < &2`] THEN
545 MATCH_MP_TAC REAL_LT_MUL THEN ASM_REWRITE_TAC[];
548 SUBGOAL_THEN `&1 <= (a + b) pow 2` ASSUME_TAC THENL
550 FIRST_X_ASSUM (MP_TAC o check (is_binop `(<=):real->real->bool` o concl)) THEN
551 MP_TAC (GEN_ALL RAT_LEMMA4) THEN
552 DISCH_THEN (MP_TAC o SPECL [`&1 - a * a - b * b`; `&1`; `&1`; `&2 * a * b`]) THEN
553 ASM_REWRITE_TAC[REAL_ARITH `&0 < &1`; REAL_ARITH `&1 / &1 = &1`] THEN
554 DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
558 SUBGOAL_THEN `(a - b) pow 2 <= &1` ASSUME_TAC THENL
560 UNDISCH_TAC `-- &1 <= (&1 - a * a - b * b) / (&2 * a * b)` THEN
561 MP_TAC (GEN_ALL RAT_LEMMA4) THEN
562 DISCH_THEN (MP_TAC o SPECL [`-- &1`; `&2 * a * b`; `&1 - a * a - b * b`; `&1`]) THEN
563 ASM_REWRITE_TAC[REAL_ARITH `&0 < &1`; REAL_ARITH `-- &1 / &1 = -- &1`] THEN
564 DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
568 DISJ_CASES_TAC (REAL_ARITH `&0 < &1 - a \/ &1 - a = &0 \/ &1 - a < &0`) THENL
570 ASM_CASES_TAC `(&1 - a * a - b * b) / (&2 * a * b) < &0` THENL
572 MATCH_MP_TAC REAL_LE_TRANS THEN
574 ASM_SIMP_TAC[REAL_LT_IMP_LE] THEN
575 REWRITE_TAC[REAL_ARITH `a * b <= &0 <=> &0 <= (--a) * b`] THEN
576 MATCH_MP_TAC REAL_LE_MUL THEN
577 ASM_SIMP_TAC[REAL_LT_IMP_LE; REAL_ARITH `x < &0 ==> &0 <= --x`];
580 POP_ASSUM MP_TAC THEN
581 REWRITE_TAC[REAL_NOT_LT] THEN DISCH_TAC THEN
582 ONCE_REWRITE_TAC[REAL_ARITH `x <= b <=> x <= &1 * b`] THEN
583 MATCH_MP_TAC REAL_LE_MUL2 THEN
584 ASM_SIMP_TAC[REAL_LT_IMP_LE] THEN
585 REWRITE_TAC[REAL_ARITH `&1 - a <= b <=> &1 <= a + b`] THEN
586 SUBGOAL_THEN `&0 <= a + b` MP_TAC THENL
588 MATCH_MP_TAC REAL_LE_ADD THEN ASM_SIMP_TAC[REAL_LT_IMP_LE];
591 ONCE_REWRITE_TAC[GSYM REAL_ABS_REFL] THEN
592 DISCH_THEN (fun th -> ONCE_REWRITE_TAC[SYM th]) THEN
593 ONCE_REWRITE_TAC[REAL_ARITH `&1 = abs(&1)`] THEN
594 ASM_REWRITE_TAC[REAL_LE_SQUARE_ABS; REAL_ARITH `&1 pow 2 = &1`];
597 POP_ASSUM DISJ_CASES_TAC THENL
599 ASM_SIMP_TAC[REAL_MUL_RZERO; REAL_LT_IMP_LE];
602 ASM_CASES_TAC `&0 < (&1 - a * a - b * b) / (&2 * a * b)` THENL
604 MATCH_MP_TAC REAL_LE_TRANS THEN
606 ASM_SIMP_TAC[REAL_LT_IMP_LE] THEN
607 REWRITE_TAC[REAL_ARITH `a * b <= &0 <=> &0 <= a * (--b)`] THEN
608 MATCH_MP_TAC REAL_LE_MUL THEN
609 ASM_SIMP_TAC[REAL_LT_IMP_LE; REAL_ARITH `x < &0 ==> &0 <= --x`];
612 POP_ASSUM MP_TAC THEN
613 REWRITE_TAC[REAL_NOT_LT] THEN DISCH_TAC THEN
614 ONCE_REWRITE_TAC[REAL_ARITH `x * y <= b <=> (--x) * (--y) <= &1 * b`] THEN
615 MATCH_MP_TAC REAL_LE_MUL2 THEN
616 ASM_SIMP_TAC[REAL_ARITH `x <= &0 ==> &0 <= --x`; REAL_ARITH `&1 - a < &0 ==> &0 <= --(&1 - a)`] THEN
617 ASM_REWRITE_TAC[REAL_ARITH `-- x <= &1 <=> -- &1 <= x`] THEN
618 REMOVE_ASSUM THEN REMOVE_ASSUM THEN POP_ASSUM MP_TAC THEN
619 REWRITE_TAC[ABS_SQUARE_LE_1] THEN
624 let rotation_dist_decrease_lemma = prove(`!v w u:real^N. u IN aff_ge {vec 0} {v,w} /\ norm u = norm v
625 ==> dist (u,w) <= dist (v,w)`,
626 REPEAT STRIP_TAC THEN
627 ASM_CASES_TAC `v:real^N = vec 0` THENL
629 UNDISCH_TAC `norm (u:real^N) = norm (v:real^N)` THEN
630 ASM_REWRITE_TAC[NORM_0; NORM_EQ_0] THEN
631 SIMP_TAC[REAL_LE_REFL];
634 ASM_CASES_TAC `w:real^N = vec 0` THENL
636 ASM_REWRITE_TAC[DIST_0; REAL_LE_REFL];
639 REWRITE_TAC[dist] THEN
640 ONCE_REWRITE_TAC[GSYM REAL_ABS_NORM] THEN
641 REWRITE_TAC[REAL_LE_SQUARE_ABS] THEN
642 REWRITE_TAC[NORM_POW_2; DOT_LSUB; DOT_RSUB] THEN
643 ASM_REWRITE_TAC[DOT_SYM; DOT_SQUARE_NORM] THEN
644 REWRITE_TAC[REAL_ARITH `v - uw - (uw - w) <= v - vw - (vw - w) <=> vw <= uw`] THEN
645 SUBGOAL_THEN `~(u = vec 0:real^N)` ASSUME_TAC THENL
647 ASM_REWRITE_TAC[GSYM NORM_EQ_0] THEN
648 ASM_REWRITE_TAC[NORM_EQ_0];
652 MAP_EVERY ABBREV_TAC [`v':real^N = inv (norm v) % v`; `w':real^N = inv (norm w) % w`; `u':real^N = inv (norm u) % u`] THEN
653 SUBGOAL_THEN `norm (v':real^N) = &1 /\ norm (w':real^N) = &1 /\ norm (u':real^N) = &1` ASSUME_TAC THENL
655 REPLICATE_TAC 3 (POP_ASSUM (fun th -> REWRITE_TAC[SYM th])) THEN
656 REPLICATE_TAC 3 (POP_ASSUM MP_TAC) THEN
657 REWRITE_TAC[GSYM NORM_EQ_0; NORM_MUL] THEN
658 SUBGOAL_THEN `!v:real^N. abs (inv (norm v)) = inv (norm v)` (fun th -> REWRITE_TAC[th]) THENL
660 REWRITE_TAC[REAL_ABS_REFL] THEN
661 GEN_TAC THEN MATCH_MP_TAC REAL_LE_INV THEN
662 REWRITE_TAC[NORM_POS_LE];
665 SIMP_TAC[REAL_MUL_LINV];
668 SUBGOAL_THEN `v:real^N = norm v % v' /\ w:real^N = norm w % w' /\ u:real^N = norm u % u'` ASSUME_TAC THENL
671 REPLICATE_TAC 3 (POP_ASSUM (fun th -> REWRITE_TAC[SYM th])) THEN
672 REPLICATE_TAC 3 (POP_ASSUM MP_TAC) THEN
673 REWRITE_TAC[VECTOR_ARITH `a % b % v = (a * b) % v:real^N`; GSYM NORM_EQ_0] THEN
674 SIMP_TAC[REAL_MUL_RINV] THEN
675 REWRITE_TAC[VECTOR_MUL_LID];
678 SUBGOAL_THEN `?a b. &0 <= a /\ &0 <= b /\ u':real^N = a % v' + b % w'` ASSUME_TAC THENL
680 REMOVE_ASSUM THEN REMOVE_ASSUM THEN
681 REPLICATE_TAC 3 (POP_ASSUM (fun th -> REWRITE_TAC[SYM th])) THEN
682 FIRST_X_ASSUM (MP_TAC o check (is_binary "IN" o concl)) THEN
683 ASM_SIMP_TAC[aff_ge_0_2] THEN
684 REWRITE_TAC[IN_ELIM_THM] THEN
685 REPLICATE_TAC 3 (POP_ASSUM MP_TAC) THEN
686 REWRITE_TAC[GSYM NORM_EQ_0] THEN REPEAT STRIP_TAC THEN
687 MAP_EVERY EXISTS_TAC [`t1:real`; `inv (norm (v:real^N)) * t2 * norm (w:real^N)`] THEN
688 CONJ_TAC THEN ASM_REWRITE_TAC[] THEN
691 MATCH_MP_TAC REAL_LE_MUL THEN
692 CONJ_TAC THENL [ MATCH_MP_TAC REAL_LE_INV THEN REWRITE_TAC[NORM_POS_LE]; ALL_TAC ] THEN
693 MATCH_MP_TAC REAL_LE_MUL THEN
694 ASM_REWRITE_TAC[NORM_POS_LE];
697 REWRITE_TAC[VECTOR_ARITH `(vv * t2 * ww) % iw % w = (vv * t2 * (ww * iw)) % (w:real^N)`] THEN
698 ASM_SIMP_TAC[REAL_MUL_RINV; REAL_MUL_RID] THEN
703 POP_ASSUM MP_TAC THEN
704 POP_ASSUM (fun th -> ONCE_REWRITE_TAC[th]) THEN
705 REPLICATE_TAC 3 (FIRST_X_ASSUM ((fun th -> ALL_TAC) o check (is_eq o concl))) THEN
707 ASM_REWRITE_TAC[DOT_LMUL; DOT_RMUL] THEN
708 MATCH_MP_TAC REAL_LE_LMUL THEN ASM_REWRITE_TAC[NORM_POS_LE] THEN
709 MATCH_MP_TAC REAL_LE_LMUL THEN ASM_REWRITE_TAC[NORM_POS_LE] THEN
711 ASM_CASES_TAC `a = &0` THENL
713 UNDISCH_TAC `u':real^N = a % v' + b % w'` THEN
714 ASM_REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_LID] THEN
715 DISCH_THEN (MP_TAC o AP_TERM `norm:real^N->real`) THEN
716 ASM_REWRITE_TAC[NORM_MUL; REAL_MUL_LZERO; REAL_ADD_LID] THEN
717 ASM_SIMP_TAC[REAL_ARITH `&0 <= b ==> abs b = b`; REAL_MUL_RID] THEN
718 DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN
719 REWRITE_TAC[DOT_LMUL; DOT_SQUARE_NORM; REAL_MUL_LID] THEN
720 ASM_REWRITE_TAC[VECTOR_ANGLE; REAL_POW_2; REAL_MUL_LID] THEN
721 REWRITE_TAC[COS_BOUNDS];
725 ASM_CASES_TAC `b = &0` THENL
727 UNDISCH_TAC `u':real^N = a % v' + b % w'` THEN
728 ASM_REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_RID] THEN
729 DISCH_THEN (MP_TAC o AP_TERM `norm:real^N -> real`) THEN
730 ASM_SIMP_TAC[NORM_MUL; REAL_ARITH `&0 <= t1 ==> abs t1 = t1`; REAL_MUL_RID] THEN
731 DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN
732 REWRITE_TAC[DOT_LMUL; REAL_MUL_LID; REAL_LE_REFL];
736 ASM_REWRITE_TAC[DOT_LADD; DOT_LMUL; DOT_SQUARE_NORM; REAL_POW_2; REAL_MUL_RID] THEN
737 REWRITE_TAC[REAL_ARITH `vw <= a * vw + b <=> vw * (&1 - a) <= b`] THEN
738 MATCH_MP_TAC aux_ineq THEN
739 ASM_REWRITE_TAC[REAL_ARITH `&0 < a <=> &0 <= a /\ ~(a = &0)`] THEN
742 UNDISCH_TAC `u':real^N = a % v' + b % w'` THEN
743 DISCH_THEN (MP_TAC o AP_TERM `norm:real^N->real`) THEN
744 ASM_REWRITE_TAC[] THEN
745 ONCE_REWRITE_TAC[GSYM REAL_ABS_NORM] THEN
746 ONCE_REWRITE_TAC[REAL_ARITH `&1 = abs(&1)`] THEN
747 REWRITE_TAC[REAL_EQ_SQUARE_ABS; NORM_POW_2; DOT_LADD; DOT_RADD; DOT_SYM; DOT_LMUL; DOT_RMUL] THEN
748 ASM_REWRITE_TAC[DOT_SQUARE_NORM; REAL_MUL_RID; REAL_POW_2; REAL_MUL_RID] THEN
749 REWRITE_TAC[REAL_ARITH `abs(&1) = &1`] THEN
750 POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN
754 ASM_REWRITE_TAC[VECTOR_ANGLE; REAL_MUL_LID; COS_BOUNDS]);;
758 let rotation_dist_decrease_special_case = prove(`!(v:real^N) w u a. &0 <= a /\ w = --a % v /\ norm u = norm v ==> dist (u,w) <= dist (v,w)`,
759 REPEAT STRIP_TAC THEN
760 REWRITE_TAC[dist] THEN ONCE_REWRITE_TAC[GSYM REAL_ABS_NORM] THEN
761 REWRITE_TAC[REAL_LE_SQUARE_ABS] THEN
762 REWRITE_TAC[NORM_POW_2; DOT_LSUB; DOT_RSUB] THEN
763 REWRITE_TAC[DOT_SYM; DOT_SQUARE_NORM] THEN
764 ASM_REWRITE_TAC[DOT_RMUL] THEN
765 REWRITE_TAC[REAL_ARITH `vv - uv - (uv - ww) <= vv - v2 - (v2 - ww) <=> --uv <= --v2`] THEN
766 REWRITE_TAC[REAL_NEG_LMUL; REAL_NEG_NEG] THEN
767 MATCH_MP_TAC REAL_LE_LMUL THEN ASM_REWRITE_TAC[] THEN
768 ASM_REWRITE_TAC[VECTOR_ANGLE] THEN
769 REPEAT (MATCH_MP_TAC REAL_LE_LMUL THEN REWRITE_TAC[NORM_POS_LE]) THEN
770 REWRITE_TAC[VECTOR_ANGLE_REFL] THEN
771 ASM_CASES_TAC `v:real^N = vec 0` THEN ASM_REWRITE_TAC[] THENL
773 REWRITE_TAC[vector_angle; REAL_LE_REFL];
774 REWRITE_TAC[COS_0; COS_BOUNDS]
780 (******************************************************************)
782 (* Lemmas about continuous functions *)
785 let continuous_lemma_inc = prove(`!f c t1. &0 <= t1 /\
786 f real_continuous_on real_interval [&0,t1] /\
787 f (&0) <= c /\ c <= f t1
788 ==> ?x. &0 <= x /\ x <= t1 /\ f x = c /\
789 (!t. &0 <= t /\ t < x ==> f t < c)`,
790 REPEAT STRIP_TAC THEN
791 ABBREV_TAC `s = {t | &0 <= t /\ t <= t1 /\ c <= f t}` THEN
792 SUBGOAL_THEN `t1:real IN s` ASSUME_TAC THENL
794 EXPAND_TAC "s" THEN ASM_REWRITE_TAC[IN_ELIM_THM; REAL_LE_REFL];
797 EXISTS_TAC `inf s` THEN
798 MP_TAC (SPEC `s:real->bool` INF) THEN
801 ASM_REWRITE_TAC[GSYM MEMBER_NOT_EMPTY] THEN
802 CONJ_TAC THENL [ EXISTS_TAC `t1:real` THEN ASM_REWRITE_TAC[]; EXISTS_TAC `&0` ] THEN
803 GEN_TAC THEN EXPAND_TAC "s" THEN
804 SIMP_TAC[IN_ELIM_THM];
810 SUBGOAL_THEN `&0 <= inf s` ASSUME_TAC THENL
812 POP_ASSUM (MP_TAC o SPEC `&0`) THEN
813 ANTS_TAC THEN SIMP_TAC[] THEN
814 GEN_TAC THEN EXPAND_TAC "s" THEN
815 SIMP_TAC[IN_ELIM_THM];
820 SUBGOAL_THEN `inf s <= t1` ASSUME_TAC THENL
822 REMOVE_ASSUM THEN POP_ASSUM (MP_TAC o SPEC `t1:real`) THEN
827 (* f t < c for all t IN [0,inf s) *)
828 SUBGOAL_THEN `!t. &0 <= t /\ t < inf s ==> f t < c` ASSUME_TAC THENL
831 DISCH_THEN (LABEL_TAC "A") THEN
832 SUBGOAL_THEN `&0 <= t /\ t <= t1` ASSUME_TAC THENL
834 ASM_REWRITE_TAC[] THEN
835 MATCH_MP_TAC REAL_LT_IMP_LE THEN
836 MATCH_MP_TAC REAL_LTE_TRANS THEN
837 EXISTS_TAC `inf s` THEN
841 USE_THEN "A" MP_TAC THEN
842 ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN
843 REWRITE_TAC[REAL_NOT_LT; DE_MORGAN_THM] THEN
844 DISCH_TAC THEN DISJ2_TAC THEN
845 FIRST_X_ASSUM MATCH_MP_TAC THEN
846 EXPAND_TAC "s" THEN ASM_REWRITE_TAC[IN_ELIM_THM];
850 ASM_REWRITE_TAC[] THEN
853 DISJ_CASES_TAC (REAL_ARITH `c < f (inf s) \/ f (inf s) = c \/ f (inf s) < c`) THENL
856 MP_TAC (SPECL [`f:real->real`; `&0`; `inf s`; `c:real`] REAL_IVT_INCREASING) THEN
859 ASM_SIMP_TAC[REAL_LT_IMP_LE] THEN
860 MATCH_MP_TAC REAL_CONTINUOUS_ON_SUBSET THEN
861 EXISTS_TAC `real_interval [&0,t1]` THEN
862 ASM_REWRITE_TAC[] THEN
863 ASM_REWRITE_TAC[SUBSET_REAL_INTERVAL; REAL_LE_REFL];
866 REWRITE_TAC[IN_REAL_INTERVAL] THEN
868 ASM_CASES_TAC `x = inf s` THENL
870 UNDISCH_TAC `f (x:real) = c:real` THEN
874 FIRST_X_ASSUM (MP_TAC o SPEC `x:real`) THEN
875 ASM_REWRITE_TAC[REAL_ARITH `x < inf s <=> x <= inf s /\ ~(x = inf s)`] THEN
876 REWRITE_TAC[REAL_LT_REFL];
879 POP_ASSUM DISJ_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
882 UNDISCH_TAC `f real_continuous_on real_interval [&0,t1]` THEN
883 REWRITE_TAC[real_continuous_on] THEN
884 DISCH_THEN (MP_TAC o SPEC `inf s`) THEN
885 ASM_REWRITE_TAC[IN_REAL_INTERVAL] THEN
886 DISCH_THEN (MP_TAC o SPEC `c - f (inf s)`) THEN
889 POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;
893 ABBREV_TAC `p = inf s + min (d / &2) (t1 - inf s)` THEN
894 SUBGOAL_THEN `!t. &0 <= t /\ t <= p ==> f t < c` ASSUME_TAC THENL
897 ASM_CASES_TAC `t < inf s` THENL
899 DISCH_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
903 POP_ASSUM MP_TAC THEN REWRITE_TAC[REAL_NOT_LT] THEN
904 REPEAT STRIP_TAC THEN
905 FIRST_X_ASSUM (MP_TAC o SPEC `t:real`) THEN
908 ASM_REWRITE_TAC[] THEN
911 MATCH_MP_TAC REAL_LE_TRANS THEN
912 EXISTS_TAC `p:real` THEN
913 ASM_REWRITE_TAC[] THEN
915 REWRITE_TAC[REAL_ARITH `a + b <= t1 <=> b <= t1 - a`] THEN
916 REWRITE_TAC[REAL_MIN_MIN];
919 MATCH_MP_TAC (REAL_ARITH `!a. &0 < d /\ a < d /\ &0 <= a ==> abs a < d`) THEN
920 ASM_REWRITE_TAC[REAL_ARITH `&0 <= a - b <=> b <= a`] THEN
921 MATCH_MP_TAC REAL_LET_TRANS THEN
922 EXISTS_TAC `p - inf s` THEN
923 ASM_REWRITE_TAC[REAL_ARITH `a - b <= c - b <=> a <= c`] THEN
925 REWRITE_TAC[REAL_ARITH `(a + b) - a = b`] THEN
926 MATCH_MP_TAC REAL_LET_TRANS THEN
927 EXISTS_TAC `d / &2` THEN
928 ASM_SIMP_TAC[REAL_MIN_MIN; REAL_ARITH `&0 < d ==> d / &2 < d`];
934 SUBGOAL_THEN `p <= inf s` MP_TAC THENL
936 FIRST_X_ASSUM MATCH_MP_TAC THEN
938 ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN
939 REWRITE_TAC[REAL_NOT_LE] THEN
940 DISCH_TAC THEN FIRST_X_ASSUM (MP_TAC o SPEC `x:real`) THEN
941 EXPAND_TAC "s" THEN REWRITE_TAC[IN_ELIM_THM; DE_MORGAN_THM] THEN
942 ASM_SIMP_TAC[REAL_LT_IMP_LE] THEN
943 ASM_CASES_TAC `&0 <= x` THEN ASM_REWRITE_TAC[] THEN
944 SIMP_TAC[REAL_NOT_LE];
947 SUBGOAL_THEN `inf s < p` MP_TAC THENL
950 REWRITE_TAC[REAL_ARITH `a < a + b <=> &0 < b`] THEN
951 ASM_SIMP_TAC[REAL_LT_MIN; REAL_ARITH `&0 < d ==> &0 < d / &2`] THEN
952 ASM_CASES_TAC `inf s = t1` THENL
954 UNDISCH_TAC `f (inf s) < c` THEN
955 POP_ASSUM (fun th -> REWRITE_TAC[th]) THEN
956 UNDISCH_TAC `c <= f (t1:real)` THEN
960 ASM_REWRITE_TAC[REAL_ARITH `&0 < t1 - inf s <=> inf s <= t1 /\ ~(inf s = t1)`];
967 let continuous_lemma_dec = prove(`!f c t1. &0 <= t1 /\
968 f real_continuous_on real_interval [&0,t1] /\
969 c <= f (&0) /\ f t1 <= c
970 ==> ?x. &0 <= x /\ x <= t1 /\ f x = c /\
971 (!t. &0 <= t /\ t < x ==> c < f t)`,
972 REPEAT STRIP_TAC THEN
973 MP_TAC (SPECL [`\t. --(f:real->real) t`; `--c:real`; `t1:real`] continuous_lemma_inc) THEN
974 ASM_REWRITE_TAC[] THEN
979 MATCH_MP_TAC REAL_CONTINUOUS_ON_NEG THEN
983 ASM_REWRITE_TAC[REAL_LE_NEG];
987 EXISTS_TAC `x:real` THEN
988 ASM_REWRITE_TAC[] THEN
991 ONCE_REWRITE_TAC[REAL_ARITH `a = b <=> --a = --b`] THEN
995 GEN_TAC THEN STRIP_TAC THEN
996 FIRST_X_ASSUM (MP_TAC o SPEC `t:real`) THEN
997 ASM_REWRITE_TAC[REAL_LT_NEG]);;
1007 (******************************************************)
1009 (* Rotation lemmas *)
1012 let rotation_lemma_special = prove(`!v w n:real^N. ~(v = vec 0) /\ ~(w = vec 0) /\
1013 (v dot n = &0) /\ (w dot n = &0) /\
1014 3 <= dimindex(:N) ==>
1015 ?f:real^1->real^N. f continuous_on UNIV /\
1016 f(lift (&0)) = v /\ f(lift (&1)) = norm v / norm w % w /\
1017 (!t. norm (f t) = norm v /\ f t dot n = &0) /\
1018 (!t. &0 <= t /\ t <= &1 ==> dist (f (lift t), w) <= dist (v, w)) /\
1019 (~collinear {vec 0, v, w} ==> (!t. &0 <= t /\ t <= &1 ==> f (lift t) IN aff_ge {vec 0} {v, w}))`,
1020 REPEAT GEN_TAC THEN STRIP_TAC THEN
1021 SUBGOAL_THEN `~(norm (v:real^N) = &0) /\ ~(norm (w:real^N) = &0)` ASSUME_TAC THENL
1023 ASM_REWRITE_TAC[NORM_EQ_0];
1027 ABBREV_TAC `u = norm (v:real^N) / norm w % w:real^N` THEN
1028 SUBGOAL_THEN `norm (u:real^N) = norm (v:real^N)` ASSUME_TAC THENL
1030 POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN
1031 REWRITE_TAC[NORM_MUL; REAL_ABS_DIV; REAL_ABS_NORM; real_div] THEN
1032 ASM_SIMP_TAC[GSYM REAL_MUL_ASSOC; REAL_MUL_LINV; REAL_MUL_RID];
1035 SUBGOAL_THEN `~(u = vec 0:real^N)` ASSUME_TAC THENL
1037 ASM_REWRITE_TAC[GSYM NORM_EQ_0];
1040 SUBGOAL_THEN `aff_ge {vec 0} {v,w} = aff_ge {vec 0:real^N} {v,u}` ASSUME_TAC THENL
1042 MATCH_MP_TAC aff_ge_eq_lemma THEN
1043 EXISTS_TAC `norm (v:real^N) / norm (w:real^N)` THEN
1044 ASM_REWRITE_TAC[] THEN
1045 MATCH_MP_TAC REAL_LT_DIV THEN
1046 ASM_REWRITE_TAC[NORM_POS_LE; REAL_ARITH `&0 < a <=> &0 <= a /\ ~(a = &0)`];
1049 SUBGOAL_THEN `collinear {vec 0, v, w:real^N} <=> collinear {vec 0, v, u}` (fun th -> REWRITE_TAC[th]) THENL
1051 MP_TAC (ISPECL [`&1`; `norm (v:real^N) / norm (w:real^N)`; `v:real^N`; `w:real^N`] COLLINEAR_SCALE_ALL) THEN
1054 REWRITE_TAC[REAL_ARITH `~(&1 = &0)`] THEN
1055 MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~(a = &0)`) THEN
1056 MATCH_MP_TAC REAL_LT_DIV THEN
1057 ASM_REWRITE_TAC[NORM_POS_LT];
1060 DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN
1061 ASM_REWRITE_TAC[VECTOR_MUL_LID];
1065 ASM_CASES_TAC `~collinear {vec 0,v,u:real^N}` THENL
1067 MP_TAC (SPECL [`v:real^N`; `u:real^N`] rotation_lemma) THEN
1068 ASM_REWRITE_TAC[] THEN
1070 EXISTS_TAC `f:real^1->real^N` THEN
1071 ASM_REWRITE_TAC[] THEN
1075 UNDISCH_TAC `!t:real^1. ?a b. f t = a % v + b % u:real^N` THEN
1076 DISCH_THEN (MP_TAC o SPEC `t:real^1`) THEN STRIP_TAC THEN
1077 ASM_REWRITE_TAC[] THEN
1078 UNDISCH_TAC `f (lift (&1)) = u:real^N` THEN
1079 DISCH_THEN (fun th -> ALL_TAC) THEN
1081 REWRITE_TAC[DOT_LADD; DOT_LMUL] THEN
1082 ASM_REWRITE_TAC[REAL_MUL_RZERO; REAL_ADD_LID];
1087 REPEAT STRIP_TAC THEN
1088 MATCH_MP_TAC rotation_dist_decrease_lemma THEN
1089 ASM_REWRITE_TAC[] THEN
1090 FIRST_X_ASSUM MATCH_MP_TAC THEN
1091 ASM_REWRITE_TAC[IN_INTERVAL_1];
1094 REPEAT STRIP_TAC THEN
1095 FIRST_X_ASSUM MATCH_MP_TAC THEN
1096 ASM_REWRITE_TAC[IN_INTERVAL_1];
1100 ASM_REWRITE_TAC[] THEN
1101 POP_ASSUM MP_TAC THEN
1102 ASM_REWRITE_TAC[COLLINEAR_LEMMA_ALT] THEN
1104 FIRST_ASSUM (MP_TAC o AP_TERM `norm:real^N->real`) THEN
1105 ASM_REWRITE_TAC[NORM_MUL] THEN
1106 ASM_REWRITE_TAC[REAL_ARITH `v = c * v <=> v * (c - &1) = &0`; REAL_ENTIRE; REAL_ARITH `abs c - &1 = &0 <=> c = &1 \/ c = -- &1`] THEN
1107 DISCH_THEN DISJ_CASES_TAC THENL
1109 EXISTS_TAC `(\t:real^1. v:real^N)` THEN
1110 ASM_REWRITE_TAC[CONTINUOUS_ON_CONST; VECTOR_MUL_LID; REAL_LE_REFL];
1114 SUBGOAL_THEN `?e:real^N. e dot v = &0 /\ norm e = norm v /\ e dot n = &0` ASSUME_TAC THENL
1116 SUBGOAL_THEN `dim {v:real^N,n} < dimindex (:N)` ASSUME_TAC THENL
1118 MATCH_MP_TAC LET_TRANS THEN
1120 ASM_SIMP_TAC[ARITH_RULE `3 <= a ==> 2 < a`] THEN
1121 MATCH_MP_TAC LE_TRANS THEN
1122 EXISTS_TAC `CARD {v:real^N,n}` THEN
1123 SUBGOAL_THEN `FINITE {v:real^N,n}` ASSUME_TAC THENL
1125 REWRITE_TAC[FINITE_INSERT; FINITE_EMPTY];
1128 ASM_SIMP_TAC[DIM_LE_CARD] THEN
1129 REWRITE_TAC[Geomdetail.CARD2];
1132 MP_TAC (SPEC `{v:real^N,n}` ORTHOGONAL_TO_SUBSPACE_EXISTS) THEN
1133 ASM_REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY; orthogonal] THEN
1135 EXISTS_TAC `norm (v:real^N) / norm (x:real^N) % x:real^N` THEN
1136 FIRST_ASSUM (MP_TAC o SPEC `v:real^N`) THEN
1137 FIRST_X_ASSUM (MP_TAC o SPEC `n:real^N`) THEN
1138 REWRITE_TAC[] THEN REPEAT DISCH_TAC THEN
1139 ASM_REWRITE_TAC[NORM_MUL; REAL_ABS_DIV; REAL_ABS_NORM; real_div; GSYM REAL_MUL_ASSOC; DOT_LMUL; REAL_MUL_RZERO] THEN
1140 UNDISCH_TAC `~(x:real^N = vec 0)` THEN
1141 SIMP_TAC[GSYM NORM_EQ_0; REAL_MUL_LINV; REAL_MUL_RID];
1145 POP_ASSUM MP_TAC THEN STRIP_TAC THEN
1147 ABBREV_TAC `f = (\t:real^1. cos (pi * drop t) % v + sin (pi * drop t) % e:real^N)` THEN
1148 EXISTS_TAC `f:real^1->real^N` THEN
1153 MATCH_MP_TAC CONTINUOUS_ON_ADD THEN
1154 CONJ_TAC THEN MATCH_MP_TAC CONTINUOUS_ON_VMUL THENL
1156 SUBGOAL_THEN `lift o (\t:real^1. cos (pi * drop t)) = (lift o cos o drop) o (\t:real^1. pi % t)` (fun th -> REWRITE_TAC[th]) THENL
1158 REWRITE_TAC[FUN_EQ_THM; o_THM; DROP_CMUL];
1161 MATCH_MP_TAC CONTINUOUS_ON_COMPOSE THEN
1162 CONJ_TAC THENL [ MATCH_MP_TAC CONTINUOUS_ON_CMUL THEN REWRITE_TAC [CONTINUOUS_ON_ID]; ALL_TAC ] THEN
1163 MATCH_MP_TAC CONTINUOUS_AT_IMP_CONTINUOUS_ON THEN
1164 GEN_TAC THEN DISCH_TAC THEN
1165 MP_TAC (SPEC `drop (x:real^1)` REAL_CONTINUOUS_AT_COS) THEN
1166 REWRITE_TAC[REAL_CONTINUOUS_CONTINUOUS_ATREAL; LIFT_DROP];
1168 SUBGOAL_THEN `lift o (\t:real^1. sin (pi * drop t)) = (lift o sin o drop) o (\t:real^1. pi % t)` (fun th -> REWRITE_TAC[th]) THENL
1170 REWRITE_TAC[FUN_EQ_THM; o_THM; DROP_CMUL];
1173 MATCH_MP_TAC CONTINUOUS_ON_COMPOSE THEN
1174 CONJ_TAC THENL [ MATCH_MP_TAC CONTINUOUS_ON_CMUL THEN REWRITE_TAC [CONTINUOUS_ON_ID]; ALL_TAC ] THEN
1175 MATCH_MP_TAC CONTINUOUS_AT_IMP_CONTINUOUS_ON THEN
1176 GEN_TAC THEN DISCH_TAC THEN
1177 MP_TAC (SPEC `drop (x:real^1)` REAL_CONTINUOUS_AT_SIN) THEN
1178 REWRITE_TAC[REAL_CONTINUOUS_CONTINUOUS_ATREAL; LIFT_DROP];
1186 REWRITE_TAC[LIFT_DROP; REAL_MUL_RZERO; COS_0; SIN_0; VECTOR_MUL_LID; VECTOR_MUL_LZERO; VECTOR_ADD_RID];
1193 ASM_REWRITE_TAC[LIFT_DROP; REAL_MUL_RID; COS_PI; SIN_PI; VECTOR_MUL_LZERO; VECTOR_ADD_RID];
1197 SUBGOAL_THEN `!t:real^1. norm ((f:real^1->real^N) t) = norm (v:real^N)` ASSUME_TAC THENL
1201 ONCE_REWRITE_TAC[GSYM REAL_ABS_NORM] THEN
1202 REWRITE_TAC[REAL_EQ_SQUARE_ABS] THEN
1203 ASM_REWRITE_TAC[NORM_POW_2; DOT_LADD; DOT_RADD; DOT_LMUL; DOT_RMUL; DOT_SYM; REAL_MUL_RZERO; REAL_ADD_LID; REAL_ADD_RID] THEN
1204 ASM_REWRITE_TAC[DOT_SQUARE_NORM] THEN
1205 REWRITE_TAC[REAL_ARITH `c * c * n + s * s * n = (s pow 2 + c pow 2) * n`] THEN
1206 REWRITE_TAC[SIN_CIRCLE; REAL_MUL_LID];
1210 ASM_REWRITE_TAC[] THEN
1213 GEN_TAC THEN EXPAND_TAC "f" THEN
1214 ASM_REWRITE_TAC[DOT_LADD; DOT_LMUL; REAL_MUL_RZERO; REAL_ADD_RID];
1218 GEN_TAC THEN DISCH_TAC THEN
1219 MATCH_MP_TAC rotation_dist_decrease_special_case THEN
1220 ASM_REWRITE_TAC[] THEN
1221 EXISTS_TAC `norm(w:real^N) / norm(v:real^N)` THEN
1224 MATCH_MP_TAC REAL_LE_DIV THEN
1225 REWRITE_TAC[NORM_POS_LE];
1228 UNDISCH_TAC `norm (v:real^N) / norm (w:real^N) % w = u` THEN
1229 DISCH_THEN (MP_TAC o AP_TERM `\x:real^N. norm (w:real^N) / norm (v:real^N) % x`) THEN
1230 REWRITE_TAC[VECTOR_MUL_ASSOC; real_div] THEN
1231 ONCE_REWRITE_TAC[REAL_ARITH `(w * iv) * v * iw = (w * iw) * (v * iv)`] THEN
1232 ASM_SIMP_TAC[REAL_MUL_RINV; REAL_MUL_LID; VECTOR_MUL_LID] THEN
1237 (* Consider properties of intersecting segments *)
1238 let aff_ge_inter_segments = prove(`!v w u p:real^N. ~collinear {vec 0, v, u} /\ p IN aff_ge {vec 0} {v, u} /\
1239 ~(segment [v, w] INTER aff_ge {vec 0} {u} = {})
1240 ==> ~(segment [p, w] INTER aff_ge {vec 0} {u} = {})`,
1241 REPEAT STRIP_TAC THEN
1242 SUBGOAL_THEN `(?x y. &0 <= x /\ x <= &1 /\ &0 <= y /\ (&1 - x) % p + x % w:real^N = y % u) ==> ~(segment [p,w] INTER aff_ge {vec 0} {u} = {})` MP_TAC THENL
1245 REWRITE_TAC[GSYM MEMBER_NOT_EMPTY] THEN
1246 REWRITE_TAC[IN_INTER; IN_SEGMENT; HALFLINE; VECTOR_MUL_RZERO; VECTOR_ADD_LID] THEN
1247 EXISTS_TAC `(&1 - x) % p + x % w:real^N` THEN
1251 EXISTS_TAC `x:real` THEN
1255 ASM_REWRITE_TAC[IN_ELIM_THM] THEN
1256 EXISTS_TAC `y:real` THEN
1260 ASM_REWRITE_TAC[TAUT `~(A ==> ~B) <=> A /\ B`] THEN
1263 SUBGOAL_THEN `~(v = vec 0:real^N) /\ ~(u = vec 0:real^N)` ASSUME_TAC THENL
1265 UNDISCH_TAC `~collinear {vec 0, v, u:real^N}` THEN
1266 SIMP_TAC[COLLINEAR_LEMMA; DE_MORGAN_THM];
1270 UNDISCH_TAC `p IN aff_ge {vec 0:real^N} {v, u}` THEN
1271 ASM_SIMP_TAC[aff_ge_0_2; IN_ELIM_THM] THEN
1274 SUBGOAL_THEN `?a c. &0 <= a /\ a <= &1 /\ &0 <= c /\ (&1 - a) % v + a % w = c % u:real^N` MP_TAC THENL
1276 UNDISCH_TAC `~(segment [v,w] INTER aff_ge {vec 0} {u:real^N} = {})` THEN
1277 REWRITE_TAC[GSYM MEMBER_NOT_EMPTY; IN_INTER; IN_SEGMENT; HALFLINE; IN_ELIM_THM] THEN
1278 REWRITE_TAC[VECTOR_MUL_RZERO; VECTOR_ADD_LID] THEN
1280 MAP_EVERY EXISTS_TAC [`u':real`; `t:real`] THEN
1281 ASM_REWRITE_TAC[] THEN
1282 POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN
1288 ASM_CASES_TAC `a = &0` THENL
1290 MAP_EVERY EXISTS_TAC [`&0`; `t1 * c + t2:real`] THEN
1291 REWRITE_TAC[REAL_LE_REFL; REAL_LE_01; VECTOR_MUL_LZERO; VECTOR_ADD_RID; REAL_SUB_RZERO; VECTOR_MUL_LID] THEN
1294 MATCH_MP_TAC REAL_LE_ADD THEN
1295 ASM_REWRITE_TAC[] THEN
1296 MATCH_MP_TAC REAL_LE_MUL THEN
1301 ASM_REWRITE_TAC[] THEN
1302 UNDISCH_TAC `(&1 - a) % v + a % w = c % u:real^N` THEN
1303 ASM_REWRITE_TAC[REAL_SUB_RZERO; VECTOR_MUL_LID; VECTOR_MUL_LZERO; VECTOR_ADD_RID] THEN
1304 DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
1309 FIRST_X_ASSUM (MP_TAC o AP_TERM `\x:real^N. inv a % x` o check (is_eq o concl)) THEN
1310 ASM_REWRITE_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC] THEN
1311 ASM_SIMP_TAC[REAL_MUL_LINV; VECTOR_MUL_LID] THEN
1312 REWRITE_TAC[VECTOR_ARITH `v + w = z <=> w = z - v:real^N`] THEN
1313 DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
1314 REWRITE_TAC[VECTOR_ARITH `x % (a % u - b % v) = (x * a) % u + (--x * b) % v:real^N`] THEN
1315 REWRITE_TAC[VECTOR_ARITH `y % u - (a % v + b % u) = (y - b) % u + (--a) % v:real^N`] THEN
1317 ABBREV_TAC `b = inv a * (&1 - a)` THEN
1318 ABBREV_TAC `d = inv a * c` THEN
1320 ASM_CASES_TAC `t1 = &0` THENL
1322 MAP_EVERY EXISTS_TAC [`&0`; `t2:real`] THEN
1323 ASM_REWRITE_TAC[REAL_LE_REFL; REAL_LE_01; REAL_MUL_LZERO; VECTOR_MUL_LZERO; REAL_MUL_LNEG; VECTOR_MUL_LNEG; REAL_SUB_RZERO; REAL_SUB_REFL; REAL_MUL_LID];
1327 SUBGOAL_THEN `&0 <= b /\ &0 <= d` ASSUME_TAC THENL
1329 SUBGOAL_THEN `&0 <= inv a` ASSUME_TAC THENL [ MATCH_MP_TAC REAL_LE_INV THEN ASM_REWRITE_TAC[]; ALL_TAC ] THEN
1330 EXPAND_TAC "b" THEN EXPAND_TAC "d" THEN
1331 CONJ_TAC THEN MATCH_MP_TAC REAL_LE_MUL THEN ASM_REWRITE_TAC[REAL_ARITH `&0 <= &1 - a <=> a <= &1`];
1335 ABBREV_TAC `x = t1 / (b + t1)` THEN
1336 MAP_EVERY EXISTS_TAC [`x:real`; `(&1 - x) * t2 + x * d`] THEN
1337 SUBGOAL_THEN `&0 <= x /\ x <= &1` ASSUME_TAC THENL
1342 MATCH_MP_TAC REAL_LE_DIV THEN
1343 ASM_REWRITE_TAC[] THEN
1344 MATCH_MP_TAC REAL_LE_ADD THEN ASM_REWRITE_TAC[];
1347 MATCH_MP_TAC Trigonometry2.REAL_LE_LDIV THEN
1350 MATCH_MP_TAC REAL_LET_ADD THEN
1351 ASM_REWRITE_TAC[REAL_LT_LE];
1354 ASM_REWRITE_TAC[REAL_ARITH `t1 <= b + t1 <=> &0 <= b`];
1358 ASM_REWRITE_TAC[] THEN
1361 MATCH_MP_TAC REAL_LE_ADD THEN
1362 CONJ_TAC THEN MATCH_MP_TAC REAL_LE_MUL THEN ASM_REWRITE_TAC[REAL_ARITH `&0 <= &1 - x <=> x <= &1`];
1366 REWRITE_TAC[REAL_ARITH `((&1 - x) * t2 + x * d) - (&1 - x) * t2 = x * d`] THEN
1367 SUBGOAL_THEN `--x * b = --((&1 - x) * t1)` (fun th -> REWRITE_TAC[th]) THEN
1368 SUBGOAL_THEN `&1 - x = b * x * inv t1` (fun th -> REWRITE_TAC[th]) THENL
1371 SUBGOAL_THEN `~(b + t1 = &0)` ASSUME_TAC THENL
1373 MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~(a = &0)`) THEN
1374 MATCH_MP_TAC REAL_LET_ADD THEN
1375 ASM_REWRITE_TAC[REAL_LT_LE];
1378 MATCH_MP_TAC REAL_EQ_LCANCEL_IMP THEN
1379 EXISTS_TAC `b + t1:real` THEN
1380 FIRST_ASSUM (fun th -> REWRITE_TAC[th; real_div]) THEN
1381 REWRITE_TAC[REAL_ARITH `bt * (&1 - t1 * ibt) = bt - t1 * (bt * ibt)`] THEN
1382 REWRITE_TAC[REAL_ARITH `bt * b * (t * ibt) * it = (bt * ibt) * (t * it) * b`] THEN
1383 ASM_SIMP_TAC[REAL_MUL_RINV] THEN
1388 REWRITE_TAC[GSYM REAL_MUL_ASSOC] THEN
1389 ASM_SIMP_TAC[REAL_MUL_LINV] THEN
1394 (* A special version of the rotation lemma for intersecting segments *)
1395 let rotation_lemma_segments = prove(`!v w u n:real^N. 3 <= dimindex (:N) /\
1396 ~(v = vec 0) /\ ~(u = vec 0) /\
1397 v dot n = &0 /\ w dot n = &0 /\ u dot n = &0 /\
1398 ~(segment [vec 0,u] INTER segment [v,w] = {})
1399 ==> ?f:real^1->real^N. f continuous_on UNIV /\
1400 f (lift (&0)) = v /\
1401 f (lift (&1)) = norm v / norm u % u /\
1402 (!t. norm (f t) = norm v /\ f t dot n = &0) /\
1403 (!t. &0 <= t /\ t <= &1 ==> dist (f (lift t), u) <= dist (v, u) /\
1404 dist (f (lift t), w) <= dist (v, w)) /\
1405 (!t. &0 <= t /\ t <= &1 ==> ~(segment [f (lift t), w] INTER aff_ge {vec 0} {u} = {}))`,
1406 REPEAT STRIP_TAC THEN
1407 SUBGOAL_THEN `~collinear {vec 0, v, w:real^N} ==> ~(w = vec 0) /\ (!t. ~((&1 - t) % v + t % w = vec 0))` ASSUME_TAC THENL
1409 REWRITE_TAC[COLLINEAR_LEMMA; DE_MORGAN_THM; NOT_EXISTS_THM] THEN STRIP_TAC THEN
1410 ASM_REWRITE_TAC[] THEN
1412 ASM_CASES_TAC `t = &0` THEN ASM_REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_RID; REAL_SUB_RZERO; VECTOR_MUL_LID] THEN
1413 DISCH_THEN (MP_TAC o AP_TERM `\x:real^N. inv t % x`) THEN
1414 REWRITE_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC] THEN
1415 ASM_SIMP_TAC[REAL_MUL_LINV; VECTOR_MUL_LID; VECTOR_MUL_RZERO] THEN
1416 ASM_REWRITE_TAC[VECTOR_ARITH `a % v + w = vec 0 <=> w = (--a) % v:real^N`];
1420 SUBGOAL_THEN `~(segment [v,w] INTER aff_ge {vec 0} {u:real^N} = {})` ASSUME_TAC THENL
1422 UNDISCH_TAC `~(segment [vec 0,u] INTER segment [v,w:real^N] = {})` THEN
1423 REWRITE_TAC[GSYM MEMBER_NOT_EMPTY; IN_INTER] THEN
1425 EXISTS_TAC `x:real^N` THEN
1426 ASM_REWRITE_TAC[] THEN
1427 MATCH_MP_TAC Hypermap.lemma_in_subset THEN
1428 EXISTS_TAC `segment [vec 0,u:real^N]` THEN
1429 ASM_REWRITE_TAC[SEGMENT_SUBSET_HALFLINE];
1433 SUBGOAL_THEN `?x c. &0 <= x /\ x <= &1 /\ &0 <= c /\ (&1 - x) % v + x % w = c % u:real^N` MP_TAC THENL
1435 POP_ASSUM MP_TAC THEN
1436 REWRITE_TAC[GSYM MEMBER_NOT_EMPTY; IN_INTER; IN_SEGMENT; HALFLINE; IN_ELIM_THM] THEN
1437 REWRITE_TAC[VECTOR_MUL_RZERO; VECTOR_ADD_LID] THEN
1439 MAP_EVERY EXISTS_TAC [`u':real`; `t:real`] THEN
1440 ASM_REWRITE_TAC[] THEN
1441 POP_ASSUM (fun th -> ASM_REWRITE_TAC[SYM th]);
1446 ASM_CASES_TAC `~collinear {vec 0, v, u:real^N}` THENL
1448 MP_TAC (SPECL [`v:real^N`; `u:real^N`; `n:real^N`] rotation_lemma_special) THEN
1451 EXISTS_TAC `f:real^1->real^N` THEN
1452 ASM_REWRITE_TAC[] THEN
1454 ASM_CASES_TAC `w = vec 0:real^N` THENL
1456 ASM_REWRITE_TAC[DIST_0; REAL_LE_REFL] THEN
1457 REWRITE_TAC[GSYM MEMBER_NOT_EMPTY] THEN
1458 REPEAT STRIP_TAC THEN
1459 EXISTS_TAC `vec 0:real^N` THEN
1460 REWRITE_TAC[IN_INTER; ENDS_IN_SEGMENT; ENDS_IN_HALFLINE];
1464 ASM_CASES_TAC `~collinear {vec 0, v, w:real^N}` THENL
1466 FIRST_ASSUM (fun th -> FIRST_X_ASSUM (MP_TAC o MATCH_MP th)) THEN
1468 CONJ_TAC THEN GEN_TAC THEN DISCH_TAC THENL
1471 MATCH_MP_TAC rotation_dist_decrease_lemma THEN
1472 ASM_REWRITE_TAC[] THEN
1473 SUBGOAL_THEN `?a b. &0 <= a /\ &0 <= b /\ u = a % v + b % w:real^N` MP_TAC THENL
1475 FIRST_X_ASSUM (MP_TAC o SPEC `x:real`) THEN
1477 UNDISCH_TAC `(&1 - x) % v + x % w = c % u:real^N` THEN
1478 ASM_CASES_TAC `c = &0` THENL [ ASM_REWRITE_TAC[VECTOR_MUL_LZERO]; ALL_TAC ] THEN
1479 DISCH_THEN (MP_TAC o AP_TERM `\v:real^N. inv c % v`) THEN
1480 ASM_SIMP_TAC[VECTOR_MUL_ASSOC; VECTOR_ADD_LDISTRIB; REAL_MUL_LINV; VECTOR_MUL_LID] THEN
1481 DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN
1482 MAP_EVERY EXISTS_TAC [`inv c * (&1 - x)`; `inv c * x`] THEN
1484 SUBGOAL_THEN `&0 <= inv c` ASSUME_TAC THENL [ MATCH_MP_TAC REAL_LE_INV THEN ASM_REWRITE_TAC[]; ALL_TAC ] THEN
1485 CONJ_TAC THEN MATCH_MP_TAC REAL_LE_MUL THEN ASM_REWRITE_TAC[REAL_ARITH `&0 <= &1 - x <=> x <= &1`];
1490 ASM_SIMP_TAC[aff_ge_0_2; IN_ELIM_THM] THEN
1491 REPLICATE_TAC 2 (FIRST_X_ASSUM (MP_TAC o SPEC `t:real`)) THEN
1492 ASM_SIMP_TAC[aff_ge_0_2; IN_ELIM_THM] THEN
1493 STRIP_TAC THEN DISCH_THEN (fun th -> ALL_TAC) THEN
1494 MAP_EVERY EXISTS_TAC [`t1 + t2 * a:real`; `t2 * b:real`] THEN
1497 MATCH_MP_TAC REAL_LE_ADD THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC REAL_LE_MUL THEN ASM_REWRITE_TAC[];
1500 CONJ_TAC THENL [ MATCH_MP_TAC REAL_LE_MUL THEN ASM_REWRITE_TAC[]; ALL_TAC ] THEN
1501 ASM_REWRITE_TAC[] THEN
1506 MATCH_MP_TAC aff_ge_inter_segments THEN
1507 EXISTS_TAC `v:real^N` THEN
1512 CONJ_TAC THEN GEN_TAC THEN DISCH_TAC THENL
1515 SUBGOAL_THEN `c = &0` ASSUME_TAC THENL
1517 UNDISCH_TAC `~ ~collinear {vec 0, v, w:real^N}` THEN
1518 ASM_REWRITE_TAC[COLLINEAR_LEMMA; DE_MORGAN_THM] THEN
1520 UNDISCH_TAC `~collinear {vec 0, v, u:real^N}` THEN
1521 ASM_REWRITE_TAC[COLLINEAR_LEMMA; DE_MORGAN_THM; NOT_EXISTS_THM] THEN
1523 ASM_CASES_TAC `c = &0` THEN ASM_REWRITE_TAC[] THEN
1524 UNDISCH_TAC `(&1 - x) % v + x % w = c % u:real^N` THEN
1525 DISCH_THEN (MP_TAC o AP_TERM `\x:real^N. inv c % x`) THEN
1526 ASM_SIMP_TAC[VECTOR_MUL_ASSOC; REAL_MUL_LINV; VECTOR_MUL_LID] THEN
1527 ASM_REWRITE_TAC[VECTOR_ARITH `a % (b % v + c % v) = (a * b + a * c) % v`];
1531 SUBGOAL_THEN `~(x = &0)` ASSUME_TAC THENL
1533 ASM_CASES_TAC `x = &0` THEN ASM_REWRITE_TAC[] THEN
1534 UNDISCH_TAC `(&1 - x) % v + x % w = c % u:real^N` THEN
1535 ASM_REWRITE_TAC[REAL_SUB_RZERO; VECTOR_MUL_LID; VECTOR_MUL_LZERO; VECTOR_ADD_RID];
1539 MATCH_MP_TAC rotation_dist_decrease_special_case THEN
1540 EXISTS_TAC `inv x * (&1 - x)` THEN
1544 MATCH_MP_TAC REAL_LE_MUL THEN ASM_REWRITE_TAC[REAL_ARITH `&0 <= &1 - x <=> x <= &1`] THEN
1545 MATCH_MP_TAC REAL_LE_INV THEN ASM_REWRITE_TAC[];
1549 UNDISCH_TAC `(&1 - x) % v + x % w = c % u:real^N` THEN
1550 ASM_REWRITE_TAC[VECTOR_MUL_LZERO] THEN
1551 REWRITE_TAC[VECTOR_ARITH `a % v + x % w = vec 0:real^N <=> x % w = --a % v`] THEN
1552 DISCH_THEN (MP_TAC o AP_TERM `\v:real^N. inv x % v`) THEN
1553 ASM_SIMP_TAC[VECTOR_MUL_ASSOC; REAL_MUL_LINV; VECTOR_MUL_LID] THEN
1554 DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
1559 MATCH_MP_TAC aff_ge_inter_segments THEN
1560 EXISTS_TAC `v:real^N` THEN
1565 POP_ASSUM MP_TAC THEN
1567 MP_TAC (ISPECL [`vec 0:real^N`; `u:real^N`; `v:real^N`] (GEN_ALL (CONJUNCT1 Collect_geom.PER_SET3))) THEN
1568 DISCH_THEN (fun th -> ONCE_REWRITE_TAC[th]) THEN
1569 ASM_REWRITE_TAC[COLLINEAR_LEMMA; DE_MORGAN_THM] THEN
1570 DISCH_THEN (X_CHOOSE_THEN `b:real` (LABEL_TAC "v" o SYM)) THEN
1571 ASM_CASES_TAC `&0 <= b` THENL
1573 EXISTS_TAC `\t:real^1. v:real^N` THEN
1574 ASM_REWRITE_TAC[CONTINUOUS_ON_CONST; REAL_LE_REFL] THEN
1575 REMOVE_THEN "v" (fun th -> REWRITE_TAC[SYM th]) THEN
1576 REWRITE_TAC[NORM_MUL; real_div; GSYM REAL_MUL_ASSOC] THEN
1577 UNDISCH_TAC `~(u = vec 0:real^N)` THEN
1578 REWRITE_TAC[GSYM NORM_EQ_0] THEN
1579 SIMP_TAC[REAL_MUL_RINV; REAL_MUL_RID] THEN
1580 SUBGOAL_THEN `abs b = b` (fun th -> REWRITE_TAC[th]) THEN
1581 ASM_REWRITE_TAC[REAL_ABS_REFL];
1585 POP_ASSUM MP_TAC THEN REWRITE_TAC[REAL_NOT_LE] THEN DISCH_TAC THEN
1586 MP_TAC (SPECL [`v:real^N`; `u:real^N`; `n:real^N`] rotation_lemma_special) THEN
1587 ASM_REWRITE_TAC[] THEN
1589 EXISTS_TAC `f:real^1->real^N` THEN
1592 ASM_CASES_TAC `w = vec 0:real^N` THENL
1594 ASM_REWRITE_TAC[DIST_0; REAL_LE_REFL] THEN
1595 REWRITE_TAC[GSYM MEMBER_NOT_EMPTY] THEN
1596 REPEAT STRIP_TAC THEN
1597 EXISTS_TAC `vec 0:real^N` THEN
1598 REWRITE_TAC[IN_INTER; ENDS_IN_SEGMENT; ENDS_IN_HALFLINE];
1602 SUBGOAL_THEN `?d. &0 <= d /\ w = d % u:real^N` ASSUME_TAC THENL
1604 SUBGOAL_THEN `~(x = &0)` ASSUME_TAC THENL
1607 UNDISCH_TAC `(&1 - x) % v + x % w = c % u:real^N` THEN
1608 ASM_REWRITE_TAC[REAL_SUB_RZERO; VECTOR_MUL_LID; VECTOR_MUL_LZERO; VECTOR_ADD_RID] THEN
1609 REMOVE_THEN "v" (fun th -> REWRITE_TAC[SYM th]) THEN
1610 ASM_REWRITE_TAC[VECTOR_ARITH `b % u = c % u <=> (c + --b) % u = vec 0:real^N`; VECTOR_MUL_EQ_0] THEN
1611 MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~(a = &0)`) THEN
1612 MATCH_MP_TAC REAL_LET_ADD THEN
1613 ASM_REWRITE_TAC[REAL_NEG_GT0];
1617 UNDISCH_TAC `(&1 - x) % v + x % w = c % u:real^N` THEN
1618 DISCH_THEN (MP_TAC o AP_TERM `\v:real^N. inv x % v`) THEN
1619 ASM_SIMP_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC; REAL_MUL_LINV; VECTOR_MUL_LID] THEN
1620 REWRITE_TAC[VECTOR_ARITH `a + w = b <=> w = b - a:real^N`] THEN
1621 DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
1622 REMOVE_THEN "v" (fun th -> REWRITE_TAC[SYM th; VECTOR_MUL_ASSOC; GSYM VECTOR_SUB_RDISTRIB]) THEN
1623 ABBREV_TAC `d = inv x * c - ((inv x * (&1 - x)) * b)` THEN
1625 EXISTS_TAC `d:real` THEN
1626 ASM_REWRITE_TAC[] THEN
1628 REWRITE_TAC[GSYM REAL_MUL_ASSOC; GSYM REAL_SUB_LDISTRIB] THEN
1629 MATCH_MP_TAC REAL_LE_MUL THEN
1630 CONJ_TAC THENL [ MATCH_MP_TAC REAL_LE_INV THEN ASM_REWRITE_TAC[]; ALL_TAC ] THEN
1631 REWRITE_TAC[REAL_ARITH `c - a * b = c + a * (--b)`] THEN
1632 MATCH_MP_TAC REAL_LE_ADD THEN
1633 ASM_REWRITE_TAC[] THEN
1634 MATCH_MP_TAC REAL_LE_MUL THEN
1635 ASM_REWRITE_TAC[REAL_NEG_GE0; REAL_ARITH `&0 <= &1 - x <=> x <= &1`] THEN
1636 ASM_SIMP_TAC[REAL_LT_IMP_LE];
1640 POP_ASSUM MP_TAC THEN STRIP_TAC THEN
1641 CONJ_TAC THEN GEN_TAC THEN DISCH_TAC THENL
1643 MATCH_MP_TAC rotation_dist_decrease_special_case THEN
1644 EXISTS_TAC `--inv b * d` THEN
1648 MATCH_MP_TAC REAL_LE_MUL THEN
1649 ASM_REWRITE_TAC[GSYM REAL_INV_NEG] THEN
1650 MATCH_MP_TAC REAL_LE_INV THEN
1651 ASM_SIMP_TAC[REAL_NEG_GE0; REAL_LT_IMP_LE];
1655 REMOVE_THEN "v" (fun th -> REWRITE_TAC[SYM th]) THEN
1656 REWRITE_TAC[VECTOR_MUL_ASSOC; REAL_ARITH `--(--inv b * d) * b = d * b * inv b`] THEN
1657 ASM_SIMP_TAC[REAL_ARITH `b < &0 ==> ~(b = &0)`; REAL_MUL_RINV; REAL_MUL_RID];
1661 REWRITE_TAC[GSYM MEMBER_NOT_EMPTY; IN_INTER; IN_SEGMENT; HALFLINE; IN_ELIM_THM] THEN
1662 EXISTS_TAC `w:real^N` THEN
1665 EXISTS_TAC `&1` THEN
1666 ASM_REWRITE_TAC[REAL_LE_01; REAL_LE_REFL; REAL_SUB_REFL; VECTOR_MUL_LZERO; VECTOR_ADD_LID; VECTOR_MUL_LID];
1669 EXISTS_TAC `d:real` THEN
1670 ASM_REWRITE_TAC[VECTOR_MUL_RZERO; VECTOR_ADD_LID]);;
1675 (* Rotation about an axis lemma *)
1676 let rotation_about_axis = prove(`!d v w:real^N. 3 <= dimindex (:N) /\ ~(d = vec 0) /\
1677 ~(projection d w = vec 0) /\
1678 ~(projection d v = vec 0)
1679 ==> ?(f:real^1->real^N) a b. &0 < a /\
1680 f continuous_on UNIV /\
1682 f(lift (&1)) = a % w + b % d /\
1683 (!t c. dist (f t, c % d) = dist (v, c % d)) /\
1684 (!t. &0 <= t /\ t <= &1 ==> dist (f (lift t), w) <= dist (v, w))`,
1685 REPEAT STRIP_TAC THEN
1686 SUBGOAL_THEN `~(norm (projection d (v:real^N)) = &0) /\ ~(norm (projection d (w:real^N)) = &0)` ASSUME_TAC THENL
1688 ASM_REWRITE_TAC[NORM_EQ_0];
1691 MP_TAC (SPECL [`projection d (v:real^N)`; `projection d (w:real^N)`; `d:real^N`] rotation_lemma_special) THEN
1692 ASM_REWRITE_TAC[PROJECTION_ORTHOGONAL] THEN
1694 DISCH_THEN (X_CHOOSE_THEN `g:real^1->real^N` MP_TAC) THEN
1697 EXISTS_TAC `\t:real^1. g t + (v - projection d (v:real^N))` THEN
1698 EXISTS_TAC `norm (projection d (v:real^N)) / norm (projection d (w:real^N))` THEN
1699 ABBREV_TAC `a = norm (projection d (v:real^N)) / norm (projection d (w:real^N))` THEN
1700 EXISTS_TAC `(v dot (d:real^N)) / norm d pow 2 - a * (w dot d) / norm d pow 2` THEN
1705 MATCH_MP_TAC REAL_LT_DIV THEN
1706 ASM_REWRITE_TAC[NORM_POS_LT];
1712 MATCH_MP_TAC CONTINUOUS_ON_ADD THEN
1713 ASM_REWRITE_TAC[CONTINUOUS_ON_CONST];
1719 ASM_REWRITE_TAC[] THEN
1726 ASM_REWRITE_TAC[] THEN
1727 REWRITE_TAC[projection; VECTOR_SUB_LDISTRIB; NORM_POW_2; real_div; VECTOR_MUL_ASSOC; VECTOR_SUB_RDISTRIB] THEN
1735 REWRITE_TAC[DIST_EQ] THEN
1736 ASM_SIMP_TAC[PROJECTION_DIST_SPECIAL_EQ; PROJECTION_LINEAR; PROJECTION_ZERO] THEN
1737 ASM_REWRITE_TAC[VECTOR_MUL_RZERO; DIST_0] THEN
1742 REPEAT STRIP_TAC THEN
1744 MATCH_MP_TAC PROJECTION_DIST_SPECIAL_LE THEN
1751 (******************************************************)
1753 (* The main lemma: continuous intersection of [f(t),w] and aff_ge {0} {v1,v2} *)
1755 let continuous_solution_aux = prove(`!a11 a12 a21 a22 f g t1 t2.
1756 f real_continuous_on real_interval [t1,t2] /\
1757 g real_continuous_on real_interval [t1,t2] /\
1758 ~(a11 * a22 - a12 * a21 = &0)
1759 ==> ?x1 x2. x1 real_continuous_on real_interval [t1,t2] /\
1760 x2 real_continuous_on real_interval [t1,t2] /\
1761 (!t. a11 * x1 t + a12 * x2 t = f t /\
1762 a21 * x1 t + a22 * x2 t = g t /\
1763 (!y1 y2. a11 * y1 + a12 * y2 = f t /\
1764 a21 * y1 + a22 * y2 = g t ==> y1 = x1 t /\ y2 = x2 t))`,
1765 REPEAT STRIP_TAC THEN
1766 ABBREV_TAC `d = a11 * a22 - a12 * a21` THEN
1767 MAP_EVERY EXISTS_TAC [`\t. (a22 * (f:real->real) t - a12 * (g:real->real) t) * inv(d)`; `\t. (a11 * (g:real->real) t - a21 * (f:real->real) t) * inv d`] THEN
1768 REPEAT CONJ_TAC THENL
1770 MATCH_MP_TAC REAL_CONTINUOUS_ON_RMUL THEN
1771 MATCH_MP_TAC REAL_CONTINUOUS_ON_SUB THEN
1772 CONJ_TAC THEN MATCH_MP_TAC REAL_CONTINUOUS_ON_LMUL THEN ASM_REWRITE_TAC[];
1773 MATCH_MP_TAC REAL_CONTINUOUS_ON_RMUL THEN
1774 MATCH_MP_TAC REAL_CONTINUOUS_ON_SUB THEN
1775 CONJ_TAC THEN MATCH_MP_TAC REAL_CONTINUOUS_ON_LMUL THEN ASM_REWRITE_TAC[];
1779 POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN
1781 CONV_TAC REAL_FIELD);;
1785 let continuous_intersection_point = prove(`!v1 v2 n (f:real^1->real^3) w t1.
1786 ~collinear {vec 0,v1,v2} /\
1787 f continuous_on interval [lift (&0), lift (t1)] /\ &0 <= t1 /\
1788 v1 dot n = &0 /\ v2 dot n = &0 /\
1790 (!t. &0 <= t /\ t <= t1 ==> f (lift t) dot n <= &0)
1791 ==> (?a b. a real_continuous_on real_interval [&0, t1] /\
1792 b real_continuous_on real_interval [&0, t1] /\
1793 (!t. &0 <= t /\ t <= t1 ==> segment [f (lift t),w] INTER affine hull {vec 0,v1,v2} = {a t % v1 + b t % v2}))`,
1794 REPEAT STRIP_TAC THEN
1795 ABBREV_TAC `u0 = (\t. --((f o lift) t dot n:real^3) / (w dot n - ((f o lift) t dot n)))` THEN
1796 ABBREV_TAC `f1 = (\t. ((f o lift) t dot v1:real^3) + u0 t * (w - (f o lift) t) dot v1)` THEN
1797 ABBREV_TAC `f2 = (\t. ((f o lift) t dot v2:real^3) + u0 t * (w - (f o lift) t) dot v2)` THEN
1798 MP_TAC (SPECL [`v1 dot v1:real^3`; `v1 dot v2:real^3`; `v1 dot v2:real^3`; `v2 dot v2:real^3`; `f1:real->real`; `f2:real->real`; `&0`; `t1:real`] continuous_solution_aux) THEN
1801 SUBGOAL_THEN `!v:real^3. (\t. (f o lift) t dot v) real_continuous_on real_interval [&0,t1]` ASSUME_TAC THENL
1803 GEN_TAC THEN REWRITE_TAC[REAL_CONTINUOUS_ON] THEN
1804 SUBGOAL_THEN `lift o (\t. (f o lift) t dot v:real^3) o drop = (lift o (\y. v dot y)) o f` (fun th -> REWRITE_TAC[th]) THENL
1806 REWRITE_TAC[FUN_EQ_THM; o_THM; DOT_SYM; LIFT_DROP];
1809 MATCH_MP_TAC CONTINUOUS_ON_COMPOSE THEN
1810 ASM_REWRITE_TAC[IMAGE_LIFT_REAL_INTERVAL; CONTINUOUS_ON_LIFT_DOT];
1814 SUBGOAL_THEN `u0 real_continuous_on real_interval[&0,t1]` ASSUME_TAC THENL
1816 EXPAND_TAC "u0" THEN
1817 REWRITE_TAC[real_div] THEN
1818 MATCH_MP_TAC REAL_CONTINUOUS_ON_MUL THEN
1819 CONJ_TAC THENL [ MATCH_MP_TAC REAL_CONTINUOUS_ON_NEG THEN ASM_REWRITE_TAC[]; ALL_TAC ] THEN
1820 REWRITE_TAC[REAL_CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN] THEN
1821 REPEAT STRIP_TAC THEN
1822 MATCH_MP_TAC REAL_CONTINUOUS_INV_WITHINREAL THEN
1825 POP_ASSUM MP_TAC THEN SPEC_TAC (`x:real`, `x:real`) THEN
1826 ONCE_REWRITE_TAC[GSYM REAL_CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN] THEN
1827 MATCH_MP_TAC REAL_CONTINUOUS_ON_SUB THEN ASM_REWRITE_TAC[REAL_CONTINUOUS_ON_CONST];
1830 MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~(a = &0)`) THEN
1831 REWRITE_TAC[REAL_ARITH `a - b = a + (--b)`] THEN
1832 MATCH_MP_TAC REAL_LTE_ADD THEN
1833 ASM_REWRITE_TAC[] THEN
1834 FIRST_X_ASSUM (MP_TAC o SPEC `x:real`) THEN
1835 ASM_REWRITE_TAC[GSYM IN_REAL_INTERVAL; o_THM] THEN
1842 EXPAND_TAC "f1" THEN
1843 MATCH_MP_TAC REAL_CONTINUOUS_ON_ADD THEN
1844 ASM_REWRITE_TAC[] THEN
1845 MATCH_MP_TAC REAL_CONTINUOUS_ON_MUL THEN
1846 ASM_REWRITE_TAC[VECTOR_ARITH `(w - f) dot v = w dot v - f dot v:real^3`] THEN
1847 MATCH_MP_TAC REAL_CONTINUOUS_ON_SUB THEN
1848 ASM_REWRITE_TAC[REAL_CONTINUOUS_ON_CONST];
1854 EXPAND_TAC "f2" THEN
1855 MATCH_MP_TAC REAL_CONTINUOUS_ON_ADD THEN
1856 ASM_REWRITE_TAC[] THEN
1857 MATCH_MP_TAC REAL_CONTINUOUS_ON_MUL THEN
1858 ASM_REWRITE_TAC[VECTOR_ARITH `(w - f) dot v = w dot v - f dot v:real^3`] THEN
1859 MATCH_MP_TAC REAL_CONTINUOUS_ON_SUB THEN
1860 ASM_REWRITE_TAC[REAL_CONTINUOUS_ON_CONST];
1864 REWRITE_TAC[REAL_ARITH `v11 * v22 - v12 * v12 = &0 <=> v12 pow 2 = v11 * v22`] THEN
1865 ASM_REWRITE_TAC[DOT_CAUCHY_SCHWARZ_EQUAL];
1870 MAP_EVERY EXISTS_TAC [`x1:real->real`; `x2:real->real`] THEN
1871 ASM_REWRITE_TAC[] THEN
1872 GEN_TAC THEN DISCH_TAC THEN
1874 REPEAT (FIRST_X_ASSUM (MP_TAC o SPEC `t:real`)) THEN
1875 ASM_REWRITE_TAC[] THEN REPEAT STRIP_TAC THEN
1877 REWRITE_TAC [SET_RULE `!s (x:A). s = {x} <=> (?x. x IN s) /\ (!y. y IN s ==> y = x)`] THEN
1880 MATCH_MP_TAC intersection_point_exists THEN
1881 EXISTS_TAC `n:real^3` THEN ASM_REWRITE_TAC[] THEN
1882 ASM_SIMP_TAC[REAL_LT_IMP_LE] THEN
1884 UNDISCH_TAC `&0 < w dot n:real^3` THEN
1885 ASM_REWRITE_TAC[DOT_RZERO; REAL_LT_REFL];
1889 GEN_TAC THEN REWRITE_TAC[IN_INTER; IN_SEGMENT; AFFINE_HULL_3; IN_ELIM_THM; VECTOR_MUL_RZERO; VECTOR_ADD_LID] THEN
1891 SUBGOAL_THEN `u:real = u0 (t:real)` ASSUME_TAC THENL
1893 UNDISCH_TAC `y:real^3 = (&1 - u) % f (lift t) + u % w` THEN
1894 DISCH_THEN (MP_TAC o AP_TERM `(\y:real^3. y dot n)`) THEN
1895 FIRST_X_ASSUM (fun th -> REWRITE_TAC[th]) THEN
1896 ASM_REWRITE_TAC[DOT_LADD; DOT_LMUL; REAL_MUL_RZERO; REAL_ADD_RID] THEN
1897 EXPAND_TAC "u0" THEN
1898 REWRITE_TAC[o_THM] THEN
1899 SUBGOAL_THEN `&0 < w:real^3 dot n - f (lift t) dot n` MP_TAC THENL
1901 REWRITE_TAC[REAL_ARITH `a - b = a + (--b)`] THEN
1902 MATCH_MP_TAC REAL_LTE_ADD THEN
1903 ASM_REWRITE_TAC[REAL_ARITH `&0 <= --a <=> a <= &0`];
1906 CONV_TAC REAL_FIELD;
1910 SUBGOAL_THEN `v:real = x1 (t:real) /\ w':real = x2 t` ASSUME_TAC THENL
1912 FIRST_X_ASSUM MATCH_MP_TAC THEN
1913 REWRITE_TAC[VECTOR_ARITH `(v1 dot v1) * v + (v1 dot v2:real^3) * w' = (v % v1 + w' % v2) dot v1`] THEN
1914 REWRITE_TAC[VECTOR_ARITH `(v1 dot v2) * v + (v2 dot v2:real^3) * w' = (v % v1 + w' % v2) dot v2`] THEN
1915 EXPAND_TAC "f1" THEN EXPAND_TAC "f2" THEN
1916 POP_ASSUM (fun th -> REWRITE_TAC[SYM th; o_THM]) THEN
1917 POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN
1918 ASM_REWRITE_TAC[] THEN
1922 UNDISCH_TAC `y:real^3 = v % v1 + w' % v2` THEN
1923 DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
1924 ASM_REWRITE_TAC[]);;
1928 let in_aff_ge_cases_lemma = prove(`!v1 v2 v w:real^N. ~collinear {vec 0,v1,v2} /\ ~(between (vec 0) (v,w)) /\
1929 v IN affine hull {vec 0,v1,v2} /\ w IN aff_ge {vec 0} {v1,v2}
1930 ==> v IN aff_ge {vec 0} {v1,v2} \/
1931 v1 IN aff_ge {vec 0} {v,w} \/
1932 v2 IN aff_ge {vec 0} {v,w}`,
1933 REPEAT STRIP_TAC THEN
1934 UNDISCH_TAC `~collinear {vec 0, v1, v2:real^N}` THEN DISCH_TAC THEN
1935 FIRST_ASSUM MP_TAC THEN REWRITE_TAC[COLLINEAR_LEMMA; DE_MORGAN_THM; NOT_EXISTS_THM] THEN DISCH_TAC THEN
1936 FIRST_X_ASSUM (MP_TAC o MATCH_MP zero_not_between) THEN
1939 ASM_CASES_TAC `v:real^N IN aff_ge {vec 0} {v1,v2}` THEN ASM_REWRITE_TAC[] THEN
1940 SUBGOAL_THEN `?t1 t2. v:real^N = t1 % v1 + t2 % v2 /\ (t1 < &0 \/ t2 < &0)` MP_TAC THENL
1942 UNDISCH_TAC `v IN affine hull {vec 0, v1, v2:real^N}` THEN
1943 POP_ASSUM MP_TAC THEN
1944 REWRITE_TAC[AFFINE_HULL_3; IN_ELIM_THM; VECTOR_MUL_RZERO; VECTOR_ADD_LID] THEN
1945 ASM_SIMP_TAC[aff_ge_0_2; IN_ELIM_THM; NOT_EXISTS_THM] THEN
1946 DISCH_TAC THEN STRIP_TAC THEN
1947 MAP_EVERY EXISTS_TAC [`v':real`; `w':real`] THEN
1948 ASM_REWRITE_TAC[] THEN
1949 FIRST_X_ASSUM (MP_TAC o SPECL [`v':real`; `w':real`]) THEN
1950 REWRITE_TAC[DE_MORGAN_THM; REAL_NOT_LE] THEN
1954 REPEAT (DISCH_THEN (CHOOSE_THEN MP_TAC)) THEN
1955 DISCH_THEN (CONJUNCTS_THEN2 (LABEL_TAC "v" o SYM) ASSUME_TAC) THEN
1957 SUBGOAL_THEN `?t3 t4. w:real^N = t3 % v1 + t4 % v2 /\ &0 <= t3 /\ &0 <= t4` MP_TAC THENL
1959 UNDISCH_TAC `w:real^N IN aff_ge {vec 0} {v1,v2}` THEN
1960 ASM_SIMP_TAC[aff_ge_0_2; IN_ELIM_THM] THEN
1962 MAP_EVERY EXISTS_TAC [`t1':real`; `t2':real`] THEN
1966 REPEAT (DISCH_THEN (CHOOSE_THEN MP_TAC)) THEN
1967 DISCH_THEN (CONJUNCTS_THEN2 (LABEL_TAC "w" o SYM) ASSUME_TAC) THEN
1969 SUBGOAL_THEN `~(v = vec 0:real^N)` ASSUME_TAC THENL
1971 ASM_CASES_TAC `v = vec 0:real^N` THEN ASM_REWRITE_TAC[] THEN
1972 UNDISCH_TAC `~(v IN aff_ge {vec 0} {v1,v2:real^N})` THEN
1973 ASM_REWRITE_TAC[points_in_aff_ge_0_2];
1977 ASM_SIMP_TAC[aff_ge_0_2; IN_ELIM_THM] THEN
1978 ASM_CASES_TAC `t3 = &0` THENL
1980 REMOVE_THEN "w" (MP_TAC o SYM) THEN
1981 ASM_REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_LID] THEN
1982 ASM_CASES_TAC `t4 = &0` THENL [ ASM_REWRITE_TAC[VECTOR_MUL_LZERO]; ALL_TAC ] THEN
1983 DISCH_THEN (MP_TAC o AP_TERM `\w:real^N. inv(t4) % w`) THEN
1984 ASM_SIMP_TAC[VECTOR_MUL_ASSOC; REAL_MUL_LINV; VECTOR_MUL_LID] THEN
1987 MAP_EVERY EXISTS_TAC [`&0`; `inv t4`] THEN
1988 ASM_SIMP_TAC[REAL_LE_INV; REAL_LE_REFL; VECTOR_MUL_LZERO; VECTOR_ADD_LID];
1991 ASM_CASES_TAC `t4 = &0` THENL
1993 REMOVE_THEN "w" (MP_TAC o SYM) THEN
1994 ASM_REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_RID] THEN
1995 DISCH_THEN (MP_TAC o AP_TERM `\w:real^N. inv(t3) % w`) THEN
1996 ASM_SIMP_TAC[VECTOR_MUL_ASSOC; REAL_MUL_LINV; VECTOR_MUL_LID] THEN
1997 DISCH_THEN (ASSUME_TAC o SYM) THEN
1999 MAP_EVERY EXISTS_TAC [`&0`; `inv t3`] THEN
2000 ASM_SIMP_TAC[REAL_LE_INV; REAL_LE_REFL; VECTOR_MUL_LZERO; VECTOR_ADD_LID];
2004 SUBGOAL_THEN `&0 < t3 /\ &0 < t4` ASSUME_TAC THENL
2006 ASM_REWRITE_TAC[REAL_ARITH `&0 < a <=> &0 <= a /\ ~(a = &0)`];
2010 SUBGOAL_THEN `~(t2 * t3 - t1 * t4 = &0)` ASSUME_TAC THENL
2012 REWRITE_TAC[REAL_ARITH `a - b = &0 <=> a = b`] THEN
2013 ASM_CASES_TAC `t1 < &0` THENL
2016 REMOVE_THEN "w" (MP_TAC o AP_TERM `(\x:real^N. t1 % x)`) THEN
2017 ASM_REWRITE_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC; REAL_MUL_AC] THEN
2018 POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN
2019 ONCE_REWRITE_TAC[REAL_MUL_AC] THEN
2020 ONCE_REWRITE_TAC[GSYM VECTOR_MUL_ASSOC] THEN
2021 ONCE_REWRITE_TAC[GSYM VECTOR_ADD_LDISTRIB] THEN
2025 SUBGOAL_THEN `t2 < &0` ASSUME_TAC THENL
2027 UNDISCH_TAC `t1 < &0 \/ t2 < &0` THEN
2028 POP_ASSUM MP_TAC THEN
2034 REMOVE_THEN "w" (MP_TAC o AP_TERM `(\x:real^N. t2 % x)`) THEN
2035 ASM_REWRITE_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC; REAL_MUL_AC] THEN
2036 ONCE_REWRITE_TAC[REAL_MUL_AC] THEN
2037 ONCE_REWRITE_TAC[GSYM VECTOR_MUL_ASSOC] THEN
2038 ASM_REWRITE_TAC[GSYM VECTOR_ADD_LDISTRIB] THEN
2043 ABBREV_TAC `d:real = t2 * t3 - t1 * t4` THEN
2044 SUBGOAL_THEN `v2:real^N = inv(d) % (t3 % v + (--t1) % w)` ASSUME_TAC THENL
2046 MATCH_MP_TAC VECTOR_MUL_LCANCEL_IMP THEN
2047 EXISTS_TAC `d:real` THEN
2048 ASM_SIMP_TAC[VECTOR_MUL_ASSOC; REAL_MUL_RINV; VECTOR_MUL_LID] THEN
2049 REMOVE_THEN "w" (MP_TAC o AP_TERM `\w:real^N. (--t1) % w`) THEN
2050 REMOVE_THEN "v" (MP_TAC o AP_TERM `\v:real^N. t3 % v`) THEN
2051 BETA_TAC THEN EXPAND_TAC "d" THEN
2055 SUBGOAL_THEN `v1:real^N = --inv(d) % (t4 % v + (--t2) % w)` ASSUME_TAC THENL
2057 MATCH_MP_TAC VECTOR_MUL_LCANCEL_IMP THEN
2058 EXISTS_TAC `d:real` THEN
2059 ASM_SIMP_TAC[VECTOR_MUL_ASSOC; REAL_MUL_RNEG; REAL_MUL_RINV] THEN
2060 REMOVE_THEN "w" (MP_TAC o AP_TERM `\w:real^N. t2 % w`) THEN
2061 REMOVE_THEN "v" (MP_TAC o AP_TERM `\v:real^N. t4 % v`) THEN
2062 BETA_TAC THEN EXPAND_TAC "d" THEN
2067 ASM_CASES_TAC `t1 < &0` THENL
2069 ASM_CASES_TAC `t2 < &0` THENL
2071 ASM_CASES_TAC `d < &0` THENL
2074 MAP_EVERY EXISTS_TAC [`(--inv d) * t4`; `(--inv d) * (--t2)`] THEN
2075 ASM_REWRITE_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC] THEN
2076 REWRITE_TAC[GSYM REAL_INV_NEG] THEN
2077 CONJ_TAC THEN MATCH_MP_TAC REAL_LE_MUL THENL
2079 ASM_REWRITE_TAC[] THEN
2080 MATCH_MP_TAC REAL_LE_INV THEN
2081 ASM_SIMP_TAC[REAL_NEG_GE0; REAL_LT_IMP_LE];
2082 ASM_SIMP_TAC[REAL_NEG_GE0; REAL_LT_IMP_LE] THEN
2083 MATCH_MP_TAC REAL_LE_INV THEN
2084 ASM_SIMP_TAC[REAL_NEG_GE0; REAL_LT_IMP_LE]
2088 POP_ASSUM MP_TAC THEN REWRITE_TAC[REAL_NOT_LT] THEN DISCH_TAC THEN
2090 MAP_EVERY EXISTS_TAC [`inv d * t3`; `inv d * (--t1)`] THEN
2091 ASM_REWRITE_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC] THEN
2092 CONJ_TAC THEN MATCH_MP_TAC REAL_LE_MUL THEN ASM_SIMP_TAC[REAL_NEG_GE0; REAL_LT_IMP_LE] THEN MATCH_MP_TAC REAL_LE_INV THEN ASM_REWRITE_TAC[];
2095 POP_ASSUM MP_TAC THEN REWRITE_TAC[REAL_NOT_LT] THEN DISCH_TAC THEN
2096 SUBGOAL_THEN `&0 <= inv d` ASSUME_TAC THENL
2099 MATCH_MP_TAC REAL_LE_INV THEN
2100 REWRITE_TAC[REAL_ARITH `a - t1 * t4 = a + (--t1) * t4`] THEN
2101 MATCH_MP_TAC REAL_LE_ADD THEN
2102 CONJ_TAC THEN MATCH_MP_TAC REAL_LE_MUL THEN ASM_SIMP_TAC[REAL_NEG_GE0; REAL_LT_IMP_LE];
2107 MAP_EVERY EXISTS_TAC [`inv d * t3`; `inv d * (--t1)`] THEN
2108 ASM_REWRITE_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC] THEN
2109 CONJ_TAC THEN MATCH_MP_TAC REAL_LE_MUL THEN ASM_SIMP_TAC[REAL_NEG_GE0; REAL_LT_IMP_LE];
2113 SUBGOAL_THEN `&0 <= t1 /\ t2 < &0` ASSUME_TAC THENL
2115 UNDISCH_TAC `t1 < &0 \/ t2 < &0` THEN
2116 ASM_REWRITE_TAC[GSYM REAL_NOT_LT];
2120 SUBGOAL_THEN `&0 <= --inv d` ASSUME_TAC THENL
2122 REWRITE_TAC[GSYM REAL_INV_NEG] THEN
2124 MATCH_MP_TAC REAL_LE_INV THEN
2125 REWRITE_TAC[REAL_ARITH `--(t2 * t3 - t1 * t4) = (--t2) * t3 + t1 * t4`] THEN
2126 MATCH_MP_TAC REAL_LE_ADD THEN
2127 CONJ_TAC THEN MATCH_MP_TAC REAL_LE_MUL THEN ASM_SIMP_TAC[REAL_NEG_GE0; REAL_LT_IMP_LE];
2132 MAP_EVERY EXISTS_TAC [`--inv d * t4`; `--inv d * (--t2)`] THEN
2133 ASM_REWRITE_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC] THEN
2134 CONJ_TAC THEN MATCH_MP_TAC REAL_LE_MUL THEN ASM_SIMP_TAC[REAL_NEG_GE0; REAL_LT_IMP_LE]);;
2138 let segment_intersects_aff_ge_lemma = prove(`!v1 v2 v w:real^N. ~collinear {vec 0,v1,v2} /\ ~between (vec 0) (v,w) /\
2139 v IN affine hull {vec 0,v1,v2} /\ w IN affine hull {vec 0,v1,v2} /\
2140 ~(segment [v,w] INTER aff_ge {vec 0} {v1,v2} = {})
2141 ==> v IN aff_ge {vec 0} {v1,v2} \/
2142 v1 IN aff_ge {vec 0} {v,w} \/
2143 v2 IN aff_ge {vec 0} {v,w}`,
2144 REPEAT STRIP_TAC THEN
2145 POP_ASSUM MP_TAC THEN REWRITE_TAC[GSYM MEMBER_NOT_EMPTY] THEN
2146 DISCH_THEN (X_CHOOSE_THEN `p:real^N` MP_TAC) THEN
2147 REWRITE_TAC[IN_INTER] THEN DISCH_THEN (CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN DISCH_TAC THEN
2148 FIRST_ASSUM MP_TAC THEN REWRITE_TAC[IN_SEGMENT] THEN STRIP_TAC THEN
2149 POP_ASSUM MP_TAC THEN
2150 ASM_CASES_TAC `u = &0` THENL
2152 ASM_REWRITE_TAC[REAL_SUB_RZERO; VECTOR_MUL_LZERO; VECTOR_MUL_LID; VECTOR_ADD_RID] THEN
2153 DISCH_THEN (fun th -> ASM_REWRITE_TAC[SYM th]);
2156 DISCH_THEN (LABEL_TAC "p" o SYM) THEN
2158 FIRST_ASSUM (MP_TAC o MATCH_MP zero_not_between) THEN
2161 MP_TAC (SPECL [`v1:real^N`; `v2:real^N`; `v:real^N`; `p:real^N`] in_aff_ge_cases_lemma) THEN
2162 ASM_REWRITE_TAC[] THEN
2166 REWRITE_TAC[BETWEEN_IN_SEGMENT] THEN DISCH_TAC THEN
2167 UNDISCH_TAC `~between (vec 0:real^N) (v,w)` THEN
2168 REWRITE_TAC[BETWEEN_IN_SEGMENT] THEN
2169 MATCH_MP_TAC Hypermap.lemma_in_subset THEN
2170 EXISTS_TAC `segment [v,p:real^N]` THEN
2171 ASM_REWRITE_TAC[SUBSET_SEGMENT; ENDS_IN_SEGMENT];
2175 SUBGOAL_THEN `p IN aff_ge {vec 0:real^N} {v,w}` ASSUME_TAC THENL
2177 MATCH_MP_TAC in_segment_imp_in_aff_ge_0_2 THEN
2182 STRIP_TAC THEN ASM_REWRITE_TAC[] THENL
2184 DISJ2_TAC THEN DISJ1_TAC THEN
2185 MATCH_MP_TAC Hypermap.lemma_in_subset THEN
2186 EXISTS_TAC `aff_ge {vec 0} {v:real^N,p}` THEN
2187 ASM_REWRITE_TAC[] THEN
2188 MATCH_MP_TAC aff_ge_0_2_SUBSET THEN
2189 ASM_REWRITE_TAC[points_in_aff_ge_0_2];
2192 DISJ2_TAC THEN DISJ2_TAC THEN
2193 MATCH_MP_TAC Hypermap.lemma_in_subset THEN
2194 EXISTS_TAC `aff_ge {vec 0} {v:real^N,p}` THEN
2195 ASM_REWRITE_TAC[] THEN
2196 MATCH_MP_TAC aff_ge_0_2_SUBSET THEN
2197 ASM_REWRITE_TAC[points_in_aff_ge_0_2]);;
2202 (* The main lemma *)
2204 let continuous_lemma_aff_ge = prove(`!v1 v2 (f:real^1->real^3) w h. &0 <= h /\
2205 f continuous_on interval [lift (&0), lift h] /\
2206 ~(segment [f (lift (&0)), w] INTER aff_ge {vec 0} {v1,v2} = {}) /\
2207 (!t. t IN interval [lift (&0), lift h] ==> ~between (vec 0) (f t, w)) /\
2208 ~collinear {vec 0,v1,v2}
2209 ==> (!t. t IN interval [lift (&0), lift h] ==> ~(segment [f t, w] INTER aff_ge {vec 0} {v1,v2} = {})) \/
2210 (?x. &0 <= x /\ x <= h /\
2211 (!t. t IN interval [lift (&0), lift x] ==> ~(segment [f t, w] INTER aff_ge {vec 0} {v1,v2} = {})) /\
2212 (f (lift x) IN aff_ge {vec 0} {v1,v2} \/ v1 IN aff_ge {vec 0} {f (lift x), w} \/ v2 IN aff_ge {vec 0} {f (lift x), w}))`,
2213 REPEAT STRIP_TAC THEN
2214 SUBGOAL_THEN `!y b. (lift y) IN interval [lift (&0), lift b] <=> &0 <= y /\ y <= b` ASSUME_TAC THENL
2216 ASM_REWRITE_TAC[IN_INTERVAL_1];
2221 SUBGOAL_THEN `lift (&0) IN interval [lift (&0), lift h]` ASSUME_TAC THENL
2223 ASM_REWRITE_TAC[IN_INTERVAL_1; REAL_LE_REFL];
2227 (* v1, v2, w != 0 *)
2228 SUBGOAL_THEN `~(v1:real^3 = vec 0) /\ ~(v2:real^3 = vec 0) /\ ~(w:real^3 = vec 0)` ASSUME_TAC THENL
2230 UNDISCH_TAC `~collinear {vec 0,v1,v2:real^3}` THEN
2231 SIMP_TAC[COLLINEAR_LEMMA; DE_MORGAN_THM] THEN DISCH_TAC THEN
2232 FIRST_X_ASSUM (MP_TAC o SPEC `lift (&0)`) THEN
2233 ASM_REWRITE_TAC[] THEN
2234 DISCH_THEN (MP_TAC o MATCH_MP zero_not_between) THEN
2239 (* ~between (vec 0) (f(t), w) expanded *)
2240 SUBGOAL_THEN `!t. &0 <= t /\ t <= h ==> ~(f (lift t) = vec 0) /\ (!u. &0 <= u /\ u <= &1 ==> ~((&1 - u) % f (lift t) + u % w = vec 0:real^3))` (LABEL_TAC "fw") THENL
2242 GEN_TAC THEN DISCH_TAC THEN
2243 FIRST_X_ASSUM (MP_TAC o SPEC `lift t`) THEN
2244 ASM_REWRITE_TAC[IN_INTERVAL_1] THEN
2245 DISCH_THEN (MP_TAC o MATCH_MP zero_not_between) THEN
2247 ASM_REWRITE_TAC[] THEN
2249 GEN_TAC THEN DISCH_TAC THEN
2250 ASM_CASES_TAC `u = &0` THENL
2252 ASM_REWRITE_TAC[REAL_SUB_RZERO; VECTOR_MUL_LID; VECTOR_MUL_LZERO; VECTOR_ADD_RID];
2255 ASM_CASES_TAC `u = &1` THENL
2257 ASM_REWRITE_TAC[REAL_SUB_REFL; VECTOR_MUL_LZERO; VECTOR_ADD_LID; VECTOR_MUL_LID];
2260 FIRST_X_ASSUM (MP_TAC o SPECL [`--u:real`; `&1 - u`]) THEN
2263 REPLICATE_TAC 3 (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC;
2266 REWRITE_TAC[VECTOR_ARITH `--u % (w:real^N) = (&1 - u) % x <=> (&1 - u) % x + u % w = vec 0`];
2271 ASM_CASES_TAC `!t. t IN interval [lift (&0),lift h] ==> ~(segment [f t,w] INTER aff_ge {vec 0} {v1,v2:real^3} = {})` THEN ASM_REWRITE_TAC[] THEN
2272 POP_ASSUM MP_TAC THEN REWRITE_TAC[NOT_FORALL_THM] THEN
2273 REWRITE_TAC[TAUT `~(A ==> ~B) <=> A /\ B`] THEN
2274 DISCH_THEN (X_CHOOSE_THEN `t1:real^1` (LABEL_TAC "A")) THEN
2276 (* Find a normal vector to the plane of aff_ge {vec 0} {v1,v2} *)
2277 SUBGOAL_THEN `?n:real^3. ~(n = vec 0) /\ v1 dot n = &0 /\ v2 dot n = &0 /\ f (lift (&0)) dot n <= &0` MP_TAC THENL
2279 ASM_CASES_TAC `f (lift (&0)) dot (v1:real^3 cross v2) <= &0` THENL
2281 EXISTS_TAC `v1 cross v2` THEN
2282 ASM_REWRITE_TAC[CROSS_EQ_0; DOT_CROSS_SELF];
2285 EXISTS_TAC `--(v1 cross v2)` THEN
2286 ASM_REWRITE_TAC[VECTOR_NEG_EQ_0; CROSS_EQ_0; DOT_RNEG; DOT_CROSS_SELF] THEN
2287 POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;
2293 SUBGOAL_THEN `!p. p IN aff_ge {vec 0} {v1,v2:real^3} ==> p dot n = &0` ASSUME_TAC THENL
2295 GEN_TAC THEN ASM_SIMP_TAC[aff_ge_0_2; IN_ELIM_THM] THEN
2296 STRIP_TAC THEN ASM_REWRITE_TAC[DOT_LADD; DOT_LMUL; REAL_MUL_RZERO; REAL_ADD_LID];
2300 (* Need for the next two cases *)
2301 UNDISCH_TAC `~(segment [f (lift (&0)), w] INTER aff_ge {vec 0:real^3} {v1,v2} = {})` THEN DISCH_TAC THEN
2302 FIRST_ASSUM MP_TAC THEN REWRITE_TAC[GSYM MEMBER_NOT_EMPTY] THEN
2303 DISCH_THEN (X_CHOOSE_THEN `p:real^3` (LABEL_TAC "B")) THEN
2304 FIRST_ASSUM (MP_TAC o REWRITE_RULE [IN_INTER; IN_SEGMENT]) THEN
2305 DISCH_THEN (CONJUNCTS_THEN2 (X_CHOOSE_THEN `up:real` MP_TAC) ASSUME_TAC) THEN
2306 GEN_REWRITE_TAC LAND_CONV [CONJ_ASSOC] THEN
2307 DISCH_THEN (CONJUNCTS_THEN2 ASSUME_TAC (LABEL_TAC "p1" o SYM)) THEN
2308 FIRST_ASSUM (MP_TAC o SPEC `p:real^3`) THEN
2309 FIRST_ASSUM (fun th -> CHANGED_TAC (REWRITE_TAC[th])) THEN DISCH_TAC THEN
2312 DISJ_CASES_TAC (REAL_ARITH `w:real^3 dot n < &0 \/ w dot n = &0 \/ &0 < w dot n`) THENL
2314 SUBGOAL_THEN `up = &0` ASSUME_TAC THENL
2316 REMOVE_THEN "p1" (MP_TAC o AP_TERM `\v:real^3. v dot n`) THEN
2317 ASM_REWRITE_TAC[DOT_LADD; DOT_LMUL; REAL_MUL_RZERO; REAL_ADD_LID] THEN
2318 ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN
2320 MATCH_MP_TAC (REAL_ARITH `&0 < --a ==> ~(a = &0)`) THEN
2321 REWRITE_TAC[REAL_ARITH `--(a * b + c * d) = a * (--b) + c * (--d)`] THEN
2322 MATCH_MP_TAC REAL_LET_ADD THEN
2325 MATCH_MP_TAC REAL_LE_MUL THEN
2326 ASM_REWRITE_TAC[REAL_ARITH `&0 <= &1 - up <=> up <= &1`; REAL_NEG_GE0];
2329 MATCH_MP_TAC REAL_LT_MUL THEN
2330 ASM_REWRITE_TAC[REAL_ARITH `&0 < up <=> &0 <= up /\ ~(up = &0)`; REAL_NEG_GT0];
2334 REMOVE_THEN "p1" MP_TAC THEN
2335 ASM_REWRITE_TAC[REAL_SUB_RZERO; VECTOR_MUL_LZERO; VECTOR_ADD_RID; VECTOR_MUL_LID] THEN
2337 EXISTS_TAC `&0` THEN
2338 ASM_REWRITE_TAC[REAL_LE_REFL; REAL_LE_01; INTERVAL_SING; IN_SING] THEN
2340 DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
2341 EXISTS_TAC `p:real^3` THEN ASM_REWRITE_TAC[];
2346 FIRST_X_ASSUM DISJ_CASES_TAC THENL
2348 ASM_CASES_TAC `w:real^3 IN aff_ge {vec 0} {v1,v2}` THENL
2350 SUBGOAL_THEN `~(segment [f (t1:real^1),w] INTER aff_ge {vec 0} {v1,v2:real^3} = {})` MP_TAC THENL
2352 REWRITE_TAC[GSYM MEMBER_NOT_EMPTY] THEN
2353 EXISTS_TAC `w:real^3` THEN
2354 REWRITE_TAC[IN_INTER; ENDS_IN_SEGMENT] THEN POP_ASSUM (fun th -> REWRITE_TAC[th]);
2361 EXISTS_TAC `&0` THEN
2362 ASM_REWRITE_TAC[REAL_LE_REFL; INTERVAL_SING; IN_SING] THEN
2365 GEN_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN
2366 EXISTS_TAC `p:real^3` THEN ASM_REWRITE_TAC[];
2370 MATCH_MP_TAC segment_intersects_aff_ge_lemma THEN
2371 ASM_REWRITE_TAC[] THEN
2372 FIRST_X_ASSUM (MP_TAC o SPEC `lift (&0)`) THEN
2373 ASM_REWRITE_TAC[] THEN
2374 DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
2376 ASM_SIMP_TAC[affine_hull_3_plane] THEN
2377 ASM_REWRITE_TAC[IN_ELIM_THM] THEN
2378 SUBGOAL_THEN `~(up = &1)` ASSUME_TAC THENL
2380 POP_ASSUM MP_TAC THEN REWRITE_TAC[CONTRAPOS_THM] THEN DISCH_TAC THEN
2381 REMOVE_THEN "p1" MP_TAC THEN ASM_REWRITE_TAC[REAL_SUB_REFL; VECTOR_MUL_LID; VECTOR_MUL_LZERO; VECTOR_ADD_LID] THEN
2386 REMOVE_THEN "p1" (MP_TAC o AP_TERM `\v:real^3. v dot n`) THEN
2387 ASM_REWRITE_TAC[DOT_LADD; DOT_LMUL; REAL_MUL_RZERO] THEN
2388 POP_ASSUM MP_TAC THEN CONV_TAC REAL_FIELD;
2392 (* Remove unnessary assumptions before considering the last case *)
2393 POP_ASSUM MP_TAC THEN REPLICATE_TAC 5 REMOVE_ASSUM THEN DISCH_TAC THEN
2397 (* Consider two major cases: f(t) intersects affine hull {vec 0,v1,v2} at some point or not *)
2398 SUBGOAL_THEN `?r. &0 <= r /\ r <= h /\
2399 (!t. &0 <= t /\ t <= r ==> f (lift t) dot (n:real^3) <= &0) /\
2400 (((!t. &0 <= t /\ t <= r ==> ~(segment [f (lift t), w] INTER aff_ge {vec 0} {v1,v2} = {})) /\ f (lift r) IN aff_ge {vec 0} {v1, v2}) \/
2401 (?t1. &0 <= t1 /\ t1 <= r /\ segment [f (lift t1), w] INTER aff_ge {vec 0} {v1,v2} = {}))` MP_TAC THENL
2403 ASM_CASES_TAC `!t. &0 <= t /\ t <= h ==> f (lift t) dot (n:real^3) <= &0` THENL
2405 EXISTS_TAC `h:real` THEN
2406 ASM_REWRITE_TAC[REAL_LE_REFL] THEN
2408 EXISTS_TAC `drop (t1:real^1)` THEN
2409 ASM_REWRITE_TAC[LIFT_DROP] THEN
2410 FIRST_X_ASSUM (MP_TAC o SPECL [`drop (t1:real^1)`; `h:real`]) THEN
2411 ASM_REWRITE_TAC[LIFT_DROP];
2415 POP_ASSUM MP_TAC THEN REWRITE_TAC[NOT_FORALL_THM] THEN
2416 DISCH_THEN (X_CHOOSE_THEN `tt:real` MP_TAC) THEN
2417 REWRITE_TAC[TAUT `~(A ==> B) <=> A /\ ~B`; REAL_NOT_LE] THEN
2419 MP_TAC (SPECL [`\t:real. f (lift t) dot n:real^3`; `&0`; `tt:real`] continuous_lemma_inc) THEN
2422 ASM_SIMP_TAC[REAL_LT_IMP_LE] THEN
2423 REWRITE_TAC[REAL_CONTINUOUS_ON] THEN
2424 SUBGOAL_THEN `lift o (\t:real. f (lift t) dot n:real^3) o drop = (lift o (\y:real^3. n dot y)) o f` (fun th -> REWRITE_TAC[th]) THENL
2426 REWRITE_TAC[FUN_EQ_THM; o_THM; LIFT_DROP; DOT_SYM];
2429 MATCH_MP_TAC CONTINUOUS_ON_COMPOSE THEN
2430 REWRITE_TAC[IMAGE_LIFT_REAL_INTERVAL; CONTINUOUS_ON_LIFT_DOT] THEN
2431 MATCH_MP_TAC CONTINUOUS_ON_SUBSET THEN
2432 EXISTS_TAC `interval [lift (&0), lift (h)]` THEN
2433 ASM_REWRITE_TAC[SUBSET_INTERVAL_1; LIFT_DROP; REAL_LE_REFL];
2436 BETA_TAC THEN STRIP_TAC THEN
2437 EXISTS_TAC `x:real` THEN
2438 ASM_REWRITE_TAC[] THEN
2441 MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `tt:real` THEN ASM_REWRITE_TAC[];
2446 REPEAT STRIP_TAC THEN
2447 ASM_CASES_TAC `t = x:real` THENL [ ASM_SIMP_TAC[REAL_ARITH `a = &0 ==> a <= &0`]; ALL_TAC ] THEN
2448 MATCH_MP_TAC REAL_LT_IMP_LE THEN
2449 FIRST_X_ASSUM MATCH_MP_TAC THEN
2450 ASM_REWRITE_TAC[REAL_LT_LE];
2454 ASM_CASES_TAC `?t1. &0 <= t1 /\ t1 <= x /\ segment [f (lift t1),w:real^3] INTER aff_ge {vec 0} {v1,v2} = {}` THEN ASM_REWRITE_TAC[] THEN
2455 POP_ASSUM MP_TAC THEN REWRITE_TAC[NOT_EXISTS_THM; DE_MORGAN_THM] THEN
2457 SUBGOAL_THEN `!t. &0 <= t /\ t <= x ==> ~(segment [f (lift t),w:real^3] INTER aff_ge {vec 0} {v1,v2} = {})` ASSUME_TAC THENL
2459 REPEAT STRIP_TAC THEN
2460 FIRST_X_ASSUM (MP_TAC o SPEC `t:real`) THEN
2461 ASM_REWRITE_TAC[DE_MORGAN_THM];
2465 ASM_REWRITE_TAC[] THEN
2466 FIRST_X_ASSUM (MP_TAC o SPEC `x:real`) THEN
2467 ASM_REWRITE_TAC[REAL_LE_REFL; GSYM MEMBER_NOT_EMPTY] THEN
2468 DISCH_THEN (X_CHOOSE_THEN `p:real^3` MP_TAC) THEN
2469 REWRITE_TAC[IN_INTER; IN_SEGMENT] THEN
2471 UNDISCH_TAC `p = (&1 - u) % f (lift x) + u % w:real^3` THEN DISCH_THEN (LABEL_TAC "p1" o SYM) THEN
2472 FIRST_ASSUM (MP_TAC o AP_TERM `\v:real^3. v dot n`) THEN
2473 FIRST_X_ASSUM (MP_TAC o SPEC `p:real^3`) THEN
2474 ASM_REWRITE_TAC[DOT_LADD; DOT_LMUL; REAL_MUL_RZERO; REAL_ADD_LID] THEN
2475 DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
2476 REWRITE_TAC[REAL_ENTIRE] THEN
2477 ASM_SIMP_TAC[REAL_ARITH `&0 < w dot n ==> ~(w:real^3 dot n = &0)`] THEN
2479 REMOVE_THEN "p1" MP_TAC THEN
2480 ASM_SIMP_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_RID; REAL_SUB_RZERO; VECTOR_MUL_LID];
2485 (* Deal with two possible cases *)
2488 EXISTS_TAC `r:real` THEN
2489 ASM_REWRITE_TAC[] THEN
2490 REPEAT STRIP_TAC THEN
2491 FIRST_X_ASSUM (MP_TAC o SPEC `drop (t:real^1)`) THEN
2492 FIRST_X_ASSUM (MP_TAC o SPECL [`drop (t:real^1)`; `r:real`]) THEN
2493 DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN
2494 ASM_REWRITE_TAC[LIFT_DROP; MEMBER_NOT_EMPTY];
2499 MP_TAC (SPECL [`v1:real^3`; `v2:real^3`; `n:real^3`; `f:real^1->real^3`; `w:real^3`; `r:real`] continuous_intersection_point) THEN
2500 ASM_REWRITE_TAC[] THEN
2503 MATCH_MP_TAC CONTINUOUS_ON_SUBSET THEN
2504 EXISTS_TAC `interval [lift (&0), lift h]` THEN
2505 ASM_REWRITE_TAC[SUBSET_INTERVAL_1; LIFT_DROP; REAL_LE_REFL];
2512 SUBGOAL_THEN `!t. &0 <= t /\ t <= r ==> a t % v1 + b t % v2:real^3 IN segment [f (lift t),w] INTER affine hull {vec 0,v1,v2}` (LABEL_TAC "a1") THENL
2514 REPEAT STRIP_TAC THEN FIRST_X_ASSUM (MP_TAC o SPEC `t:real`) THEN
2515 ASM_REWRITE_TAC[EXTENSION; IN_SING; IN_INTER] THEN
2516 DISCH_THEN (MP_TAC o SPEC `a (t:real) % v1 + b t % v2:real^3`) THEN
2522 SUBGOAL_THEN `!t. &0 <= t /\ t <= r ==> ?u. &0 <= u /\ u <= &1 /\ a t % v1 + b t % v2 = (&1 - u) % f (lift t) + u % w:real^3` (LABEL_TAC "a2") THENL
2524 REPEAT STRIP_TAC THEN
2525 FIRST_X_ASSUM (MP_TAC o SPEC `t:real`) THEN
2526 ASM_REWRITE_TAC[IN_INTER; IN_SEGMENT] THEN
2528 EXISTS_TAC `u:real` THEN
2534 SUBGOAL_THEN `!t. &0 <= t /\ t <= r /\ &0 <= a t /\ &0 <= b t ==> (?x. x IN segment [f (lift t),w:real^3] INTER aff_ge {vec 0} {v1,v2})` (LABEL_TAC "a3") THENL
2536 REPEAT STRIP_TAC THEN
2537 EXISTS_TAC `a (t:real) % (v1:real^3) + b t % v2` THEN
2538 REWRITE_TAC[IN_INTER] THEN
2539 REMOVE_THEN "a1" (MP_TAC o SPEC `t:real`) THEN
2540 ASM_SIMP_TAC[IN_INTER] THEN DISCH_TAC THEN
2541 ASM_SIMP_TAC[aff_ge_0_2; IN_ELIM_THM] THEN
2542 MAP_EVERY EXISTS_TAC [`(a:real->real) t`; `(b:real->real) t`] THEN
2548 SUBGOAL_THEN `!t. &0 <= t /\ t <= r /\ ~(segment [f (lift t),w] INTER aff_ge {vec 0:real^3} {v1,v2} = {}) ==> &0 <= a t /\ &0 <= b t` (LABEL_TAC "a4") THENL
2550 GEN_TAC THEN DISCH_THEN STRIP_ASSUME_TAC THEN
2551 POP_ASSUM MP_TAC THEN REWRITE_TAC[GSYM MEMBER_NOT_EMPTY; IN_INTER] THEN
2553 SUBGOAL_THEN `x:real^3 IN segment [f (lift t),w] INTER affine hull {vec 0,v1,v2}` MP_TAC THENL
2555 ASM_REWRITE_TAC[IN_INTER] THEN
2556 MATCH_MP_TAC Hypermap.lemma_in_subset THEN
2557 EXISTS_TAC `aff_ge {vec 0:real^3} {v1,v2}` THEN
2558 ASM_REWRITE_TAC[] THEN
2559 REWRITE_TAC[SET_RULE `{vec 0:real^3,v1,v2} = {vec 0} UNION {v1,v2}`] THEN
2560 REWRITE_TAC[AFF_GE_SUBSET_AFFINE_HULL];
2563 DISCH_TAC THEN FIRST_ASSUM MP_TAC THEN
2564 FIRST_ASSUM (ASSUME_TAC o REWRITE_RULE[IN_INTER]) THEN
2565 MP_TAC (ISPECL [`v1:real^3`; `v2:real^3`; `x:real^3`] in_affine_hull_lemma) THEN
2566 ASM_REWRITE_TAC[] THEN
2567 REMOVE_ASSUM THEN POP_ASSUM MP_TAC THEN
2569 MAP_EVERY (fun s -> REMOVE_THEN s (fun th -> ALL_TAC)) ["a1"; "a2"; "a3"] THEN
2570 FIRST_X_ASSUM (MP_TAC o SPEC `t:real`) THEN
2571 ASM_REWRITE_TAC[] THEN
2572 DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
2573 REWRITE_TAC[IN_SING] THEN
2574 DISCH_THEN (LABEL_TAC "x1" o SYM) THEN
2576 FIRST_X_ASSUM (LABEL_TAC "x2" o SYM o check (is_eq o concl)) THEN
2577 UNDISCH_TAC `x IN aff_ge {vec 0} {v1,v2:real^3}` THEN
2578 MP_TAC (ISPECL [`v1:real^3`; `v2:real^3`] aff_ge_0_2) THEN
2579 ASM_REWRITE_TAC[] THEN DISCH_THEN (fun th -> REWRITE_TAC[th; IN_ELIM_THM]) THEN
2581 SUBGOAL_THEN `a (t:real) = t1'':real /\ b (t:real) = t2:real` MP_TAC THENL
2583 FIRST_X_ASSUM MATCH_MP_TAC THEN
2584 REMOVE_THEN "x1" (fun th -> REWRITE_TAC[th]);
2587 SUBGOAL_THEN `t1''' = t1'':real /\ t2' = t2:real` MP_TAC THENL
2589 FIRST_X_ASSUM MATCH_MP_TAC THEN
2590 POP_ASSUM (fun th -> REWRITE_TAC[th]);
2593 DISCH_THEN (fun th -> REWRITE_TAC[GSYM th]) THEN
2594 DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
2600 SUBGOAL_THEN `&0 <= a (&0) /\ &0 <= b (&0)` (LABEL_TAC "a5") THENL
2602 FIRST_X_ASSUM MATCH_MP_TAC THEN
2603 ASM_REWRITE_TAC[REAL_LE_REFL; REAL_LE_01];
2608 (* Cases for a(t) and b(t) *)
2609 SUBGOAL_THEN `?x. &0 <= x /\ x <= r /\ (!t. &0 <= t /\ t <= x ==> &0 <= a t /\ &0 <= b t) /\ (a x = &0 \/ b x = &0)` MP_TAC THENL
2611 (* 0 <= a(t) for all t *)
2612 ASM_CASES_TAC `!t. &0 <= t /\ t <= r ==> &0 <= a t` THENL
2614 MP_TAC (SPECL [`b:real->real`; `&0`; `t1':real`] continuous_lemma_dec) THEN
2615 ASM_REWRITE_TAC[] THEN
2620 MATCH_MP_TAC REAL_CONTINUOUS_ON_SUBSET THEN
2621 EXISTS_TAC `real_interval [&0,r]` THEN
2622 ASM_REWRITE_TAC[SUBSET_REAL_INTERVAL; REAL_LE_REFL];
2625 FIRST_X_ASSUM (MP_TAC o check (is_eq o concl)) THEN
2626 ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN
2627 REWRITE_TAC[REAL_NOT_LE; GSYM MEMBER_NOT_EMPTY] THEN
2629 FIRST_X_ASSUM MATCH_MP_TAC THEN
2630 ASM_SIMP_TAC[REAL_LT_IMP_LE];
2635 EXISTS_TAC `x:real` THEN
2636 SUBGOAL_THEN `x <= r` ASSUME_TAC THENL
2638 MATCH_MP_TAC REAL_LE_TRANS THEN
2639 EXISTS_TAC `t1':real` THEN
2643 ASM_REWRITE_TAC[] THEN
2644 GEN_TAC THEN DISCH_TAC THEN
2647 FIRST_X_ASSUM MATCH_MP_TAC THEN
2648 ASM_REWRITE_TAC[] THEN
2649 MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `x:real` THEN
2653 ASM_CASES_TAC `t = x:real` THEN ASM_REWRITE_TAC[REAL_LE_REFL] THEN
2654 MATCH_MP_TAC REAL_LT_IMP_LE THEN
2655 FIRST_X_ASSUM MATCH_MP_TAC THEN
2656 ASM_REWRITE_TAC[REAL_ARITH `t < x <=> t <= x /\ ~(t = x)`];
2661 POP_ASSUM MP_TAC THEN
2662 REWRITE_TAC[NOT_FORALL_THM; TAUT `~(A ==> B) <=> A /\ ~B`; REAL_NOT_LE] THEN
2663 DISCH_THEN (X_CHOOSE_THEN `ta:real` ASSUME_TAC) THEN
2665 MP_TAC (SPECL [`a:real->real`; `&0`; `ta:real`] continuous_lemma_dec) THEN
2666 ASM_SIMP_TAC[REAL_LT_IMP_LE] THEN
2669 MATCH_MP_TAC REAL_CONTINUOUS_ON_SUBSET THEN
2670 EXISTS_TAC `real_interval [&0,r]` THEN
2671 ASM_REWRITE_TAC[SUBSET_REAL_INTERVAL; REAL_LE_REFL];
2674 DISCH_THEN (X_CHOOSE_THEN `xa:real` MP_TAC) THEN
2676 SUBGOAL_THEN `!t. &0 <= t /\ t <= xa ==> &0 <= a t` MP_TAC THENL
2678 GEN_TAC THEN DISCH_TAC THEN
2679 ASM_CASES_TAC `t = xa:real` THEN ASM_REWRITE_TAC[REAL_LE_REFL] THEN
2680 MATCH_MP_TAC REAL_LT_IMP_LE THEN
2681 FIRST_X_ASSUM MATCH_MP_TAC THEN
2682 ASM_REWRITE_TAC[REAL_ARITH `t < xa <=> t <= xa /\ ~(t = xa)`];
2685 REMOVE_ASSUM THEN DISCH_TAC THEN
2687 (* 0 <= b(t) for all t *)
2688 ASM_CASES_TAC `!t. &0 <= t /\ t <= r ==> &0 <= b t` THENL
2690 EXISTS_TAC `xa:real` THEN
2691 SUBGOAL_THEN `xa <= r` ASSUME_TAC THENL
2693 MATCH_MP_TAC REAL_LE_TRANS THEN
2694 EXISTS_TAC `ta:real` THEN
2698 ASM_REWRITE_TAC[] THEN
2699 GEN_TAC THEN DISCH_TAC THEN
2702 FIRST_X_ASSUM MATCH_MP_TAC THEN
2706 FIRST_X_ASSUM MATCH_MP_TAC THEN
2707 ASM_REWRITE_TAC[] THEN
2708 MATCH_MP_TAC REAL_LE_TRANS THEN
2709 EXISTS_TAC `xa:real` THEN
2715 POP_ASSUM MP_TAC THEN
2716 REWRITE_TAC[NOT_FORALL_THM; TAUT `~(A ==> B) <=> A /\ ~B`; REAL_NOT_LE] THEN
2717 DISCH_THEN (X_CHOOSE_THEN `tb:real` ASSUME_TAC) THEN
2719 MP_TAC (SPECL [`b:real->real`; `&0`; `tb:real`] continuous_lemma_dec) THEN
2720 ASM_SIMP_TAC[REAL_LT_IMP_LE] THEN
2723 MATCH_MP_TAC REAL_CONTINUOUS_ON_SUBSET THEN
2724 EXISTS_TAC `real_interval [&0,r]` THEN
2725 ASM_REWRITE_TAC[SUBSET_REAL_INTERVAL; REAL_LE_REFL];
2728 DISCH_THEN (X_CHOOSE_THEN `xb:real` MP_TAC) THEN
2730 SUBGOAL_THEN `!t. &0 <= t /\ t <= xb ==> &0 <= b t` MP_TAC THENL
2732 GEN_TAC THEN DISCH_TAC THEN
2733 ASM_CASES_TAC `t = xb:real` THEN ASM_REWRITE_TAC[REAL_LE_REFL] THEN
2734 MATCH_MP_TAC REAL_LT_IMP_LE THEN
2735 FIRST_X_ASSUM MATCH_MP_TAC THEN
2736 ASM_REWRITE_TAC[REAL_ARITH `t < xa <=> t <= xa /\ ~(t = xa)`];
2739 REMOVE_ASSUM THEN DISCH_TAC THEN
2741 EXISTS_TAC `min xa xb` THEN
2742 ASM_REWRITE_TAC[REAL_LE_MIN] THEN
2745 MATCH_MP_TAC REAL_LE_TRANS THEN
2746 EXISTS_TAC `xa:real` THEN
2747 REWRITE_TAC[REAL_MIN_MIN] THEN
2748 MATCH_MP_TAC REAL_LE_TRANS THEN
2749 EXISTS_TAC `ta:real` THEN
2755 GEN_TAC THEN DISCH_TAC THEN
2756 CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[];
2759 REWRITE_TAC[real_min] THEN
2760 COND_CASES_TAC THEN ASM_REWRITE_TAC[];
2764 (* The final stage *)
2765 DISCH_THEN (CHOOSE_THEN MP_TAC) THEN
2766 ONCE_REWRITE_TAC[TAUT `A /\ B /\ C /\ D <=> (A /\ B) /\ C /\ D`] THEN
2767 DISCH_THEN (CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
2768 DISCH_THEN (CONJUNCTS_THEN ASSUME_TAC) THEN
2770 EXISTS_TAC `x:real` THEN
2771 ASM_REWRITE_TAC[] THEN
2774 MATCH_MP_TAC REAL_LE_TRANS THEN
2775 EXISTS_TAC `r:real` THEN
2782 FIRST_X_ASSUM (MP_TAC o SPECL [`drop (t:real^1)`; `x:real`]) THEN
2783 REWRITE_TAC[LIFT_DROP] THEN
2784 DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
2786 REMOVE_THEN "a3" (MP_TAC o SPEC `drop (t:real^1)`) THEN
2789 ASM_REWRITE_TAC[] THEN
2790 CONJ_TAC THENL [ MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `x:real` THEN ASM_REWRITE_TAC[]; ALL_TAC ] THEN
2791 FIRST_X_ASSUM MATCH_MP_TAC THEN
2795 SIMP_TAC[LIFT_DROP];
2799 (* The final case split: a x = 0 or b x = 0 *)
2800 POP_ASSUM DISJ_CASES_TAC THENL
2802 DISJ2_TAC THEN DISJ2_TAC THEN
2803 REMOVE_THEN "fw" (MP_TAC o SPEC `x:real`) THEN
2806 ASM_REWRITE_TAC[] THEN
2807 MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `r:real` THEN ASM_REWRITE_TAC[];
2811 ASM_SIMP_TAC[aff_ge_0_2; IN_ELIM_THM] THEN
2812 REMOVE_THEN "a2" (MP_TAC o SPEC `x:real`) THEN
2813 ASM_REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_LID] THEN
2815 POP_ASSUM MP_TAC THEN
2816 ASM_CASES_TAC `b (x:real) = &0` THENL [ ASM_SIMP_TAC[VECTOR_MUL_LZERO]; ALL_TAC ] THEN
2817 DISCH_THEN (MP_TAC o AP_TERM `\v:real^3. inv ((b:real->real) x) % v`) THEN
2818 REWRITE_TAC[VECTOR_MUL_ASSOC; VECTOR_ADD_LDISTRIB] THEN
2819 ASM_SIMP_TAC[REAL_MUL_LINV; VECTOR_MUL_LID] THEN
2821 MAP_EVERY EXISTS_TAC [`inv (b (x:real)) * (&1 - u)`; `inv (b (x:real)) * u`] THEN
2823 SUBGOAL_THEN `&0 <= inv (b (x:real))` ASSUME_TAC THENL
2825 MATCH_MP_TAC REAL_LE_INV THEN
2826 REPLICATE_TAC 2 (FIRST_X_ASSUM (MP_TAC o SPEC `x:real`)) THEN
2827 ASM_SIMP_TAC[REAL_LE_REFL];
2830 CONJ_TAC THEN MATCH_MP_TAC REAL_LE_MUL THEN CONJ_TAC THEN ASM_REWRITE_TAC[REAL_ARITH `&0 <= &1 - u <=> u <= &1`];
2834 DISJ2_TAC THEN DISJ1_TAC THEN
2835 REMOVE_THEN "fw" (MP_TAC o SPEC `x:real`) THEN
2838 ASM_REWRITE_TAC[] THEN
2839 MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `r:real` THEN ASM_REWRITE_TAC[];
2843 ASM_SIMP_TAC[aff_ge_0_2; IN_ELIM_THM] THEN
2844 REMOVE_THEN "a2" (MP_TAC o SPEC `x:real`) THEN
2845 ASM_REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_RID] THEN
2847 POP_ASSUM MP_TAC THEN
2848 ASM_CASES_TAC `a (x:real) = &0` THENL [ ASM_SIMP_TAC[VECTOR_MUL_LZERO]; ALL_TAC ] THEN
2849 DISCH_THEN (MP_TAC o AP_TERM `\v:real^3. inv ((a:real->real) x) % v`) THEN
2850 REWRITE_TAC[VECTOR_MUL_ASSOC; VECTOR_ADD_LDISTRIB] THEN
2851 ASM_SIMP_TAC[REAL_MUL_LINV; VECTOR_MUL_LID] THEN
2853 MAP_EVERY EXISTS_TAC [`inv (a (x:real)) * (&1 - u)`; `inv (a (x:real)) * u`] THEN
2855 SUBGOAL_THEN `&0 <= inv (a (x:real))` ASSUME_TAC THENL
2857 MATCH_MP_TAC REAL_LE_INV THEN
2858 REPLICATE_TAC 2 (FIRST_X_ASSUM (MP_TAC o SPEC `x:real`)) THEN
2859 ASM_SIMP_TAC[REAL_LE_REFL];
2862 CONJ_TAC THEN MATCH_MP_TAC REAL_LE_MUL THEN CONJ_TAC THEN ASM_REWRITE_TAC[REAL_ARITH `&0 <= &1 - u <=> u <= &1`]
2868 (* v1 and v3 in a 4-point configuration are separated by the plane affine hull {0,v2,v4} *)
2870 let separation_plane_4_points = prove(`!v1 v2 v3 v4:real^3. v1 IN ball_annulus /\ v2 IN ball_annulus /\ v3 IN ball_annulus /\ v4 IN ball_annulus /\
2871 dist (v2, v4) <= &2 * h0 /\ dist (v1, v3) <= &2 * h0 /\ &2 <= dist (v2, v4) /\
2872 &2 <= dist (v1, v2) /\ &2 <= dist (v1, v4) /\
2873 &2 <= dist (v2, v3) /\ &2 <= dist (v3, v4) /\
2874 ~(segment [v1, v3] INTER aff_ge {vec 0} {v2, v4} = {})
2875 ==> ?n. ~(n = vec 0) /\ v2 dot n = &0 /\ v4 dot n = &0 /\
2876 v1 dot n < &0 /\ &0 < v3 dot n`,
2877 REPEAT STRIP_TAC THEN
2878 SUBGOAL_THEN `~(v1 = vec 0:real^3) /\ ~(v2 = vec 0:real^3) /\ ~(v3 = vec 0:real^3) /\ ~(v4 = vec 0:real^3)` ASSUME_TAC THENL
2880 REPEAT (FIRST_X_ASSUM (MP_TAC o check (is_binary "IN" o concl))) THEN
2881 SIMP_TAC[in_ball_annulus];
2884 SUBGOAL_THEN `~collinear {vec 0, v2, v4:real^3}` ASSUME_TAC THENL
2886 ASM_SIMP_TAC[estd_non_collinear_lemma];
2889 SUBGOAL_THEN `~between (vec 0) (v1:real^3,v3)` ASSUME_TAC THENL
2891 ASM_SIMP_TAC[zero_not_between_estd];
2895 SUBGOAL_THEN `?n:real^3. ~(n = vec 0) /\ v2 dot n = &0 /\ v4 dot n = &0 /\ v1 dot n <= &0` MP_TAC THENL
2897 ASM_CASES_TAC `v1 dot (v2 cross v4) <= &0` THENL
2899 EXISTS_TAC `v2 cross v4` THEN
2900 ASM_REWRITE_TAC[CROSS_EQ_0; DOT_CROSS_SELF];
2903 EXISTS_TAC `--(v2 cross v4)` THEN
2904 ASM_REWRITE_TAC[VECTOR_NEG_EQ_0; CROSS_EQ_0; DOT_RNEG; DOT_CROSS_SELF] THEN
2905 POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;
2910 EXISTS_TAC `n:real^3` THEN
2911 SUBGOAL_THEN `~(v1 IN aff_ge {vec 0:real^3} {v2, v4}) /\ ~(v3 IN aff_ge {vec 0} {v2, v4})` ASSUME_TAC THENL
2913 CONJ_TAC THEN DISCH_TAC THEN MATCH_MP_TAC LEMMA_3_POINTS_FINAL THENL
2915 MAP_EVERY EXISTS_TAC [`v2:real^3`; `v4:real^3`; `v1:real^3`];
2916 MAP_EVERY EXISTS_TAC [`v2:real^3`; `v4:real^3`; `v3:real^3`]
2918 ASM_REWRITE_TAC[DIST_SYM];
2921 SUBGOAL_THEN `~(v2 IN aff_ge {vec 0:real^3} {v1, v3}) /\ ~(v4 IN aff_ge {vec 0:real^3} {v1, v3})` ASSUME_TAC THENL
2923 CONJ_TAC THEN DISCH_TAC THEN MATCH_MP_TAC LEMMA_3_POINTS_FINAL THENL
2925 MAP_EVERY EXISTS_TAC [`v1:real^3`; `v3:real^3`; `v2:real^3`];
2926 MAP_EVERY EXISTS_TAC [`v1:real^3`; `v3:real^3`; `v4:real^3`]
2928 ASM_REWRITE_TAC[DIST_SYM];
2932 ASM_REWRITE_TAC[] THEN
2933 ASM_CASES_TAC `v1 dot n:real^3 = &0` THENL
2935 ASM_CASES_TAC `v3 dot n:real^3 = &0` THENL
2937 MP_TAC (ISPECL [`v2:real^3`; `v4:real^3`; `v1:real^3`; `v3:real^3`] segment_intersects_aff_ge_lemma) THEN
2940 ASM_REWRITE_TAC[] THEN
2941 ASM_SIMP_TAC[affine_hull_3_plane; IN_ELIM_THM];
2947 MP_TAC (ISPECL [`v2:real^3`; `v4:real^3`; `v1:real^3`; `v3:real^3`; `n:real^3`] segment_inter_aff_ge_ends) THEN
2952 CONJ_TAC THENL [ ASM_REWRITE_TAC[REAL_LT_LE]; ALL_TAC ] THEN
2953 DISJ_CASES_TAC (REAL_ARITH `v3 dot n:real^3 < &0 \/ v3 dot n = &0 \/ &0 < v3 dot n`) THENL
2955 UNDISCH_TAC `~(segment [v1:real^3,v3] INTER aff_ge {vec 0} {v2,v4} = {})` THEN
2956 REWRITE_TAC[GSYM MEMBER_NOT_EMPTY] THEN
2957 REWRITE_TAC[IN_INTER; IN_SEGMENT] THEN
2958 ASM_SIMP_TAC[aff_ge_0_2; IN_ELIM_THM] THEN
2960 POP_ASSUM (MP_TAC o AP_TERM `\v:real^3. v dot n`) THEN
2961 ASM_REWRITE_TAC[DOT_LADD; DOT_LMUL; REAL_MUL_RZERO; REAL_ADD_LID] THEN
2962 ASM_CASES_TAC `u = &0` THEN ASM_REWRITE_TAC[] THENL
2964 ASM_REWRITE_TAC[REAL_SUB_RZERO; REAL_MUL_LZERO; REAL_MUL_LID; REAL_ADD_RID];
2967 SUBGOAL_THEN `(&1 - u) * (v1 dot n:real^3) + u * (v3 dot n) < &0` MP_TAC THENL
2969 REWRITE_TAC[REAL_ARITH `(&1 - u) * a + u * b < &0 <=> &0 < u * --b + (&1 - u) * --a`] THEN
2970 MATCH_MP_TAC REAL_LTE_ADD THEN
2973 MATCH_MP_TAC REAL_LT_MUL THEN
2974 ASM_REWRITE_TAC[REAL_NEG_GT0; REAL_LT_LE];
2977 MATCH_MP_TAC REAL_LE_MUL THEN
2978 ASM_REWRITE_TAC[REAL_NEG_GE0; REAL_LT_LE] THEN
2979 ASM_REWRITE_TAC[REAL_ARITH `&0 <= &1 - u <=> u <= &1`];
2986 POP_ASSUM DISJ_CASES_TAC THENL
2988 MP_TAC (ISPECL [`v2:real^3`; `v4:real^3`; `v3:real^3`; `v1:real^3`; `n:real^3`] segment_inter_aff_ge_ends) THEN
2989 ASM_REWRITE_TAC[SEGMENT_SYM];
2992 ASM_REWRITE_TAC[]);;
2998 (************************************************************************************)
3002 (* The first rotation lemma for a 4-point configuration *)
3003 let lemma_4_points_rotation1 = prove(`!v1 v2 v3 v4. v1 IN ball_annulus /\ v2 IN ball_annulus /\ v3 IN ball_annulus /\ v4 IN ball_annulus /\
3004 dist (v1, v3) <= &2 * h0 /\ dist (v2, v4) <= &2 * h0 /\
3005 &2 <= dist (v1, v2) /\ &2 <= dist (v1, v4) /\
3006 &2 <= dist (v2, v3) /\ &2 <= dist (v3, v4) /\
3007 &2 <= dist (v2, v4) /\
3008 ~(segment [v1, v3] INTER aff_ge {vec 0} {v2, v4} = {})
3009 ==> (?v1'. v1' IN ball_annulus /\ norm v1' = norm v1 /\
3010 dist (v1', v3) <= &2 * h0 /\
3011 dist (v1', v2) = dist (v1, v2) /\ dist (v1', v4) = &2 /\
3012 ~(segment [v1',v3] INTER aff_ge {vec 0} {v2,v4} = {}))`,
3013 REPEAT STRIP_TAC THEN
3014 SUBGOAL_THEN `~collinear {vec 0, v2, v4:real^3}` ASSUME_TAC THENL
3016 MATCH_MP_TAC estd_non_collinear_lemma THEN
3021 SUBGOAL_THEN `~(v1 = vec 0:real^3) /\ ~(v2 = vec 0:real^3) /\ ~(v3 = vec 0:real^3) /\ ~(v4 = vec 0:real^3)` ASSUME_TAC THENL
3023 REPEAT (FIRST_X_ASSUM (MP_TAC o check (is_binary "IN" o concl))) THEN
3024 SIMP_TAC[in_ball_annulus];
3028 MP_TAC (SPEC_ALL separation_plane_4_points) THEN
3029 ASM_REWRITE_TAC[] THEN
3032 MP_TAC (ISPECL [`v2:real^3`; `v1:real^3`; `v3:real^3`] rotation_about_axis) THEN
3033 ASM_REWRITE_TAC[DIMINDEX_3; LE_REFL; projection] THEN
3036 CONJ_TAC THEN DISCH_THEN (MP_TAC o AP_TERM `\x:real^3. x dot n`) THEN ASM_REWRITE_TAC[DOT_LSUB; DOT_LMUL; DOT_LZERO; REAL_MUL_RZERO; REAL_SUB_RZERO] THENL
3038 ASM_SIMP_TAC[REAL_ARITH `&0 < a ==> ~(a = &0)`];
3039 ASM_SIMP_TAC[REAL_LT_IMP_NE]
3045 SUBGOAL_THEN `!t. (f:real^1->real^3) t IN ball_annulus` ASSUME_TAC THENL
3047 GEN_TAC THEN REWRITE_TAC[in_ball_annulus] THEN
3048 REWRITE_TAC[GSYM NORM_EQ_0] THEN
3049 SUBGOAL_THEN `norm ((f:real^1->real^3) t) = norm (v1:real^3)` (fun th -> REWRITE_TAC[th]) THENL
3051 FIRST_X_ASSUM (MP_TAC o SPECL [`t:real^1`; `&0`]) THEN
3052 SIMP_TAC[VECTOR_MUL_LZERO; DIST_0];
3055 REWRITE_TAC[NORM_EQ_0] THEN
3056 REWRITE_TAC[GSYM in_ball_annulus] THEN ASM_REWRITE_TAC[];
3060 MP_TAC (ISPECL [`v2:real^3`; `v4:real^3`; `f:real^1->real^3`; `v3:real^3`; `&1`] continuous_lemma_aff_ge) THEN
3063 ASM_REWRITE_TAC[REAL_LE_01] THEN
3066 MATCH_MP_TAC CONTINUOUS_ON_SUBSET THEN
3067 EXISTS_TAC `(:real^1)` THEN
3068 ASM_REWRITE_TAC[SUBSET_UNIV];
3071 GEN_TAC THEN DISCH_TAC THEN
3072 MATCH_MP_TAC zero_not_between_estd THEN
3073 ASM_REWRITE_TAC[] THEN
3074 MATCH_MP_TAC REAL_LE_TRANS THEN
3075 EXISTS_TAC `dist (v1:real^3,v3)` THEN
3076 ASM_REWRITE_TAC[] THEN
3077 FIRST_X_ASSUM (MP_TAC o SPEC `drop (t:real^1)`) THEN
3080 POP_ASSUM MP_TAC THEN
3081 SUBGOAL_THEN `t = lift (drop (t:real^1))` (fun th -> GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [th]) THENL
3083 REWRITE_TAC[LIFT_DROP];
3086 REWRITE_TAC[IN_INTERVAL_1];
3089 REWRITE_TAC[LIFT_DROP];
3093 DISCH_THEN DISJ_CASES_TAC THENL
3095 MATCH_MP_TAC (TAUT `F ==> A`) THEN
3096 POP_ASSUM (MP_TAC o SPEC `lift (&1)`) THEN
3097 REWRITE_TAC[GSYM MEMBER_NOT_EMPTY] THEN
3098 REWRITE_TAC[IN_INTERVAL_1; REAL_LE_REFL; REAL_LE_01] THEN
3099 REWRITE_TAC[IN_INTER; IN_SEGMENT] THEN
3100 ASM_SIMP_TAC[aff_ge_0_2; IN_ELIM_THM] THEN
3102 POP_ASSUM (MP_TAC o AP_TERM `\x:real^3. x dot n`) THEN
3103 ASM_REWRITE_TAC[DOT_LADD; DOT_LMUL; REAL_MUL_RZERO; REAL_ADD_RID] THEN
3104 MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~(a = &0)`) THEN
3105 REWRITE_TAC[REAL_ARITH `(&1 - u) * a * b + u * b = b * (a * (&1 - u) + u)`] THEN
3106 MATCH_MP_TAC REAL_LT_MUL THEN
3107 ASM_REWRITE_TAC[] THEN
3108 ASM_CASES_TAC `u = &0` THENL
3110 ASM_REWRITE_TAC[REAL_SUB_RZERO; REAL_MUL_RID; REAL_ADD_RID];
3113 MATCH_MP_TAC REAL_LET_ADD THEN
3114 ASM_REWRITE_TAC[REAL_LT_LE] THEN
3115 MATCH_MP_TAC REAL_LE_MUL THEN
3116 ASM_SIMP_TAC[REAL_LT_IMP_LE; REAL_ARITH `&0 <= &1 - u <=> u <= &1`];
3120 POP_ASSUM MP_TAC THEN
3121 DISCH_THEN (CHOOSE_THEN MP_TAC) THEN
3122 REWRITE_TAC[CONJ_ASSOC] THEN
3123 DISCH_THEN (CONJUNCTS_THEN ASSUME_TAC) THEN
3125 SUBGOAL_THEN `!t. &2 <= dist (f (t:real^1), v2:real^3)` ASSUME_TAC THENL
3128 FIRST_X_ASSUM (MP_TAC o SPECL [`t:real^1`; `&1`]) THEN
3129 ASM_SIMP_TAC[VECTOR_MUL_LID];
3133 SUBGOAL_THEN `!t. &0 <= t /\ t <= &1 ==> dist (f (lift t),v3:real^3) <= &2 * h0` ASSUME_TAC THENL
3135 REPEAT STRIP_TAC THEN
3136 MATCH_MP_TAC REAL_LE_TRANS THEN
3137 EXISTS_TAC `dist (v1:real^3, v3)` THEN
3142 SUBGOAL_THEN `dist (f (lift x), v4:real^3) < &2` ASSUME_TAC THENL
3144 FIRST_X_ASSUM (MP_TAC o check (is_disj o concl)) THEN
3145 ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN
3146 REWRITE_TAC[REAL_NOT_LT; DE_MORGAN_THM] THEN
3149 REPEAT CONJ_TAC THEN DISCH_TAC THEN MATCH_MP_TAC LEMMA_3_POINTS_FINAL THENL
3151 MAP_EVERY EXISTS_TAC [`v2:real^3`; `v4:real^3`; `f (lift x):real^3`] THEN
3152 ASM_REWRITE_TAC[DIST_SYM];
3153 MAP_EVERY EXISTS_TAC [`f (lift x):real^3`; `v3:real^3`; `v2:real^3`] THEN
3154 ASM_SIMP_TAC[DIST_SYM];
3155 MAP_EVERY EXISTS_TAC [`f (lift x):real^3`; `v3:real^3`; `v4:real^3`] THEN
3161 MP_TAC (ISPECL [`f:real^1->real^3`; `v4:real^3`; `x:real`; `&2`] dist_decreasing_ivt_lemma) THEN
3162 ASM_SIMP_TAC[REAL_LT_IMP_LE] THEN
3164 EXISTS_TAC `(f:real^1->real^3) t` THEN
3166 SUBGOAL_THEN `!t:real^1. dist ((f t):real^3,v2) = dist (v1,v2)` ASSUME_TAC THENL
3169 FIRST_X_ASSUM (MP_TAC o SPECL [`t':real^1`; `&1`]) THEN
3170 SIMP_TAC[VECTOR_MUL_LID];
3177 FIRST_X_ASSUM (MP_TAC o SPECL [`t:real^1`; `&0`]) THEN
3178 SIMP_TAC[VECTOR_MUL_LZERO; DIST_0];
3182 FIRST_X_ASSUM (MP_TAC o SPEC `drop (t:real^1)`) THEN
3185 REWRITE_TAC[GSYM IN_INTERVAL_1; LIFT_DROP] THEN
3186 MATCH_MP_TAC Hypermap.lemma_in_subset THEN
3187 EXISTS_TAC `interval [lift (&0), lift x]` THEN
3188 ASM_REWRITE_TAC[SUBSET_INTERVAL] THEN
3189 REWRITE_TAC[DIMINDEX_1; ARITH_RULE `1 <= i /\ i <= 1 <=> i = 1`] THEN
3191 ASM_REWRITE_TAC[GSYM drop; LIFT_DROP; REAL_LE_REFL];
3195 REWRITE_TAC[LIFT_DROP]);;
3200 (*****************************************************************************************)
3203 let lemma_4_points_rotation1_full = prove(`!v1 v2 v3 v4. v1 IN ball_annulus /\ v2 IN ball_annulus /\ v3 IN ball_annulus /\ v4 IN ball_annulus /\
3204 dist (v1,v3) <= &2 * h0 /\ dist (v2,v4) <= &2 * h0 /\
3205 &2 <= dist (v1,v2) /\ &2 <= dist (v1,v4) /\
3206 &2 <= dist (v2,v3) /\ &2 <= dist (v3,v4) /\
3207 &2 <= dist (v2,v4) /\
3208 ~(segment [v1,v3] INTER aff_ge {vec 0} {v2, v4} = {})
3209 ==> (?v1' v3'. v1' IN ball_annulus /\ v3' IN ball_annulus /\
3210 norm v1' = norm v1 /\ norm v3' = norm v3 /\
3211 dist (v1',v3') <= &2 * h0 /\
3212 dist (v1',v2) = &2 /\ dist (v1',v4) = &2 /\
3213 dist (v2,v3') = &2 /\ dist (v3',v4) = &2 /\
3214 ~(segment [v1',v3'] INTER aff_ge {vec 0} {v2, v4} = {}))`,
3215 REPEAT STRIP_TAC THEN
3217 MP_TAC (SPEC_ALL lemma_4_points_rotation1) THEN
3218 ASM_REWRITE_TAC[] THEN
3220 SUBGOAL_THEN `&2 <= dist (v1':real^3,v2)` ASSUME_TAC THENL
3225 UNDISCH_TAC `norm (v1':real^3) = norm (v1:real^3)` THEN
3226 REPEAT (FIRST_X_ASSUM ((fun th -> ALL_TAC) o check (free_in `v1:real^3` o concl))) THEN
3230 MP_TAC (SPECL [`v1':real^3`; `v4:real^3`; `v3:real^3`; `v2:real^3`] lemma_4_points_rotation1) THEN
3231 ASM_REWRITE_TAC[REAL_LE_REFL; DIST_SYM; Collect_geom.PER_SET2] THEN
3233 REPEAT (FIRST_X_ASSUM ((fun th -> ALL_TAC) o check (free_in `v1':real^3` o concl))) THEN
3234 DISCH_THEN (X_CHOOSE_THEN `v1':real^3` MP_TAC) THEN STRIP_TAC THEN
3237 MP_TAC (SPECL [`v3:real^3`; `v2:real^3`; `v1':real^3`; `v4:real^3`] lemma_4_points_rotation1) THEN
3238 ASM_REWRITE_TAC[DIST_SYM; REAL_LE_REFL; SEGMENT_SYM] THEN
3239 DISCH_THEN (X_CHOOSE_THEN `v3':real^3` MP_TAC) THEN
3240 REWRITE_TAC[DIST_SYM] THEN STRIP_TAC THEN
3241 UNDISCH_TAC `norm (v3':real^3) = norm (v3:real^3)` THEN
3242 SUBGOAL_THEN `&2 <= dist (v2:real^3,v3')` ASSUME_TAC THENL
3247 REPEAT (FIRST_X_ASSUM ((fun th -> ALL_TAC) o check (free_in `v3:real^3` o concl))) THEN
3251 MP_TAC (SPECL [`v3':real^3`; `v4:real^3`; `v1':real^3`; `v2:real^3`] lemma_4_points_rotation1) THEN
3252 ASM_REWRITE_TAC[REAL_LE_REFL; DIST_SYM; Collect_geom.PER_SET2; SEGMENT_SYM] THEN
3253 REPEAT (FIRST_X_ASSUM ((fun th -> ALL_TAC) o check (free_in `v3':real^3` o concl))) THEN
3254 DISCH_THEN (X_CHOOSE_THEN `v3':real^3` MP_TAC) THEN STRIP_TAC THEN
3256 MAP_EVERY EXISTS_TAC [`v1':real^3`; `v3':real^3`] THEN
3257 ASM_REWRITE_TAC[DIST_SYM; SEGMENT_SYM]);;
3261 (*******************************************************************************************)
3264 (* Auxiliary result for the second rotation lemma *)
3266 let segment_inter_conv = prove(`!v1 v2 v3 v4 n:real^N. ~(v2 = vec 0) /\ ~(v4 = vec 0) /\ ~(v2 = v4) /\
3267 ~(projection (v4 - v2) (--v2) = vec 0) /\
3268 ~(segment [v1, v3] INTER aff_ge {vec 0} {v2, v4} = {}) /\
3269 v1 dot n < &0 /\ &0 < v3 dot n /\ v2 dot n = &0 /\ v4 dot n = &0 /\
3270 ~(segment [projection (v4 - v2) (v1 - v2), projection (v4 - v2) (v3 - v2)] INTER
3271 aff_ge {vec 0} {projection (v4 - v2) (--v2)} = {})
3272 ==> ~(segment [v1, v3] INTER convex hull {vec 0, v2, v4} = {})`,
3273 REPEAT STRIP_TAC THEN
3274 POP_ASSUM MP_TAC THEN REWRITE_TAC[GSYM MEMBER_NOT_EMPTY] THEN
3275 REWRITE_TAC[IN_SEGMENT; CONVEX_HULL_3_ALT; IN_INTER; IN_ELIM_THM; VECTOR_SUB_RZERO; VECTOR_ADD_LID] THEN
3277 UNDISCH_TAC `~(segment [v1,v3] INTER aff_ge {vec 0} {v2,v4:real^N} = {})` THEN
3278 REWRITE_TAC[GSYM MEMBER_NOT_EMPTY; IN_SEGMENT; IN_INTER] THEN
3279 ASM_SIMP_TAC[aff_ge_0_2; IN_ELIM_THM] THEN
3280 REPEAT STRIP_TAC THEN
3281 EXISTS_TAC `x:real^N` THEN
3284 EXISTS_TAC `u:real` THEN
3289 MAP_EVERY EXISTS_TAC [`t1:real`; `t2:real`] THEN
3290 FIRST_ASSUM (fun th -> REWRITE_TAC[th]) THEN
3291 ASM_REWRITE_TAC[] THEN
3293 ABBREV_TAC `d = v4 - v2:real^N` THEN
3294 ABBREV_TAC `v = v1 - v2:real^N` THEN
3295 ABBREV_TAC `w = v3 - v2:real^N` THEN
3297 FIRST_X_ASSUM (MP_TAC o check (is_neg o concl)) THEN
3298 REWRITE_TAC[GSYM MEMBER_NOT_EMPTY; IN_INTER; IN_SEGMENT; HALFLINE; IN_ELIM_THM] THEN
3299 DISCH_THEN (X_CHOOSE_THEN `px:real^N` MP_TAC) THEN
3300 DISCH_THEN (CONJUNCTS_THEN2 (X_CHOOSE_THEN `up:real` MP_TAC) (X_CHOOSE_THEN `tp:real` MP_TAC)) THEN
3301 REWRITE_TAC[VECTOR_MUL_RZERO; VECTOR_ADD_LID] THEN
3302 STRIP_TAC THEN POP_ASSUM (LABEL_TAC "px1") THEN
3303 ONCE_REWRITE_TAC[CONJ_ASSOC] THEN
3304 DISCH_THEN (CONJUNCTS_THEN2 ASSUME_TAC (LABEL_TAC "px2")) THEN
3306 SUBGOAL_THEN `(&1 - u) % v + u % w = t2 % d + (&1 - t1 - t2) % (--v2:real^N)` MP_TAC THENL
3308 REPLICATE_TAC 4 REMOVE_ASSUM THEN
3309 REPLICATE_TAC 3 (POP_ASSUM (fun th -> REWRITE_TAC[SYM th])) THEN
3310 REWRITE_TAC [VECTOR_ARITH `(&1 - u) % (v1 - v2) + u % (v3 - v2) = ((&1 - u) % v1 + u % v3) - v2:real^N`] THEN
3311 FIRST_X_ASSUM (fun th -> CHANGED_TAC (REWRITE_TAC[SYM th])) THEN
3312 ASM_REWRITE_TAC[] THEN
3317 SUBGOAL_THEN `~(d = vec 0:real^N)` ASSUME_TAC THENL
3320 ASM_REWRITE_TAC[VECTOR_SUB_EQ];
3324 DISCH_THEN (MP_TAC o AP_TERM `\v:real^N. projection d v`) THEN
3325 REWRITE_TAC[PROJECTION_LINEAR] THEN
3326 ASM_SIMP_TAC[PROJECTION_ZERO; VECTOR_MUL_RZERO; VECTOR_ADD_LID] THEN
3328 SUBGOAL_THEN `projection d (--v2) dot n = &0 /\ projection d v dot n = v1 dot n /\ projection d w dot n = v3 dot n:real^N` ASSUME_TAC THENL
3330 MAP_EVERY EXPAND_TAC ["d"; "v"; "w"] THEN
3331 REWRITE_TAC[projection] THEN
3332 ASM_REWRITE_TAC[DOT_LSUB; DOT_LNEG; DOT_LMUL; REAL_SUB_REFL; REAL_MUL_RZERO] THEN
3338 FIRST_ASSUM (MP_TAC o AP_TERM `\v:real^N. v dot n`) THEN
3339 USE_THEN "px2" MP_TAC THEN USE_THEN "px1" (fun th -> REWRITE_TAC[th]) THEN
3340 DISCH_THEN (MP_TAC o AP_TERM `\v:real^N. v dot n`) THEN
3341 ASM_REWRITE_TAC[DOT_LADD; DOT_LMUL; REAL_MUL_RZERO] THEN
3342 DISCH_THEN (LABEL_TAC "A" o SYM) THEN DISCH_THEN (LABEL_TAC "B") THEN
3344 SUBGOAL_THEN `u = up:real` ASSUME_TAC THENL
3346 MATCH_MP_TAC EQ_TRANS THEN
3347 ABBREV_TAC `a = v1 dot n:real^N` THEN
3348 ABBREV_TAC `b = v3 dot n:real^N` THEN
3349 EXISTS_TAC `a / (a - b)` THEN
3350 SUBGOAL_THEN `~(a - b = &0)` ASSUME_TAC THENL
3352 MATCH_MP_TAC (REAL_ARITH `&0 < b + --a ==> ~(a - b = &0)`) THEN
3353 MATCH_MP_TAC REAL_LT_ADD THEN
3354 ASM_REWRITE_TAC[REAL_NEG_GT0];
3358 CONJ_TAC THEN MATCH_MP_TAC REAL_EQ_RCANCEL_IMP THEN EXISTS_TAC `a - b:real` THEN REWRITE_TAC[real_div; GSYM REAL_MUL_ASSOC] THEN ASM_SIMP_TAC[REAL_MUL_LINV] THENL
3360 REMOVE_THEN "B" MP_TAC THEN REAL_ARITH_TAC;
3363 REMOVE_THEN "A" MP_TAC THEN
3368 REMOVE_THEN "px2" MP_TAC THEN
3369 POP_ASSUM (fun th -> ASM_REWRITE_TAC[SYM th]) THEN
3370 ASM_REWRITE_TAC[VECTOR_MUL_RCANCEL] THEN
3371 UNDISCH_TAC `&0 <= tp` THEN
3377 (* The second rotation lemma for a 4-point configuration *)
3379 let lemma_4_points_rotation2 = prove(`!v1 v2 v3 v4. v1 IN ball_annulus /\ v2 IN ball_annulus /\ v3 IN ball_annulus /\ v4 IN ball_annulus /\
3380 dist (v1,v3) <= &2 * h0 /\ dist (v2,v4) <= &2 * h0 /\
3381 &2 <= dist (v1,v2) /\ &2 <= dist (v1,v4) /\
3382 &2 <= dist (v2,v3) /\ &2 <= dist (v3,v4) /\
3383 &2 <= dist (v2,v4) /\
3384 ~(segment [v1,v3] INTER convex hull {vec 0,v2,v4} = {})
3385 ==> (?v1'. v1' IN ball_annulus /\ norm v1' = &2 /\
3386 dist (v1',v3) <= &2 * h0 /\
3387 dist (v1',v2) = dist (v1,v2) /\
3388 dist (v1',v4) = dist (v1,v4) /\
3389 ~(segment [v1',v3] INTER convex hull {vec 0,v2,v4} = {}))`,
3390 REPEAT STRIP_TAC THEN
3391 SUBGOAL_THEN `?u t2 t4. (&0 <= u /\ u <= &1 /\ &0 <= t2 /\ &0 <= t4 /\ t2 + t4 <= &1) /\ (&1 - u) % (v1 - v2) + u % (v3 - v2) = t4 % (v4 - v2) + (&1 - t2 - t4) % (--v2:real^3)` MP_TAC THENL
3393 POP_ASSUM MP_TAC THEN
3394 REWRITE_TAC[GSYM MEMBER_NOT_EMPTY; IN_INTER; IN_SEGMENT; CONVEX_HULL_3_ALT; IN_ELIM_THM] THEN
3395 REWRITE_TAC[VECTOR_SUB_RZERO; VECTOR_ADD_LID] THEN
3396 REPEAT STRIP_TAC THEN
3397 MAP_EVERY EXISTS_TAC [`u:real`; `u':real`; `v:real`] THEN
3398 ASM_REWRITE_TAC[] THEN
3399 REWRITE_TAC[VECTOR_ARITH `(&1 - u) % (v1 - v2) + u % (v3 - v2) = ((&1 - u) % v1 + u % v3) - v2:real^3`] THEN
3400 POP_ASSUM MP_TAC THEN
3401 FIRST_X_ASSUM (fun th -> CHANGED_TAC (REWRITE_TAC[SYM th])) THEN
3402 DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
3407 SUBGOAL_THEN `~collinear {vec 0, v2, v4:real^3} /\ ~(v2 = vec 0) /\ ~(v4 = vec 0)` ASSUME_TAC THENL
3409 REPLICATE_TAC 3 (FIRST_X_ASSUM (MP_TAC o check (is_binary "IN" o concl))) THEN
3410 SIMP_TAC[in_ball_annulus] THEN
3411 REPEAT DISCH_TAC THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[] THEN
3412 MATCH_MP_TAC estd_non_collinear_lemma THEN
3413 ASM_REWRITE_TAC[in_ball_annulus];
3417 SUBGOAL_THEN `~(segment [v1,v3] INTER aff_ge {vec 0} {v2,v4:real^3} = {})` MP_TAC THENL
3419 FIRST_X_ASSUM (MP_TAC o check (is_neg o concl)) THEN
3420 REWRITE_TAC[GSYM MEMBER_NOT_EMPTY; IN_INTER] THEN
3421 STRIP_TAC THEN EXISTS_TAC `x:real^3` THEN ASM_REWRITE_TAC[] THEN
3422 MATCH_MP_TAC Hypermap.lemma_in_subset THEN
3423 EXISTS_TAC `convex hull {vec 0,v2,v4:real^3}` THEN
3424 ASM_REWRITE_TAC[] THEN
3425 ASM_SIMP_TAC[CONVEX_HULL_3_ALT; aff_ge_0_2; SUBSET; IN_ELIM_THM; VECTOR_SUB_RZERO; VECTOR_ADD_LID] THEN
3426 REPEAT STRIP_TAC THEN
3427 MAP_EVERY EXISTS_TAC [`u:real`; `v:real`] THEN
3432 FIRST_X_ASSUM ((fun th -> ALL_TAC) o check (is_neg o concl)) THEN
3435 MAP_EVERY (fun tm -> DISCH_THEN (X_CHOOSE_THEN tm MP_TAC)) [`u:real`; `t2:real`; `t4:real`] THEN
3436 DISCH_THEN (CONJUNCTS_THEN2 ASSUME_TAC (LABEL_TAC "A")) THEN
3438 MP_TAC (SPEC_ALL separation_plane_4_points) THEN
3439 ASM_REWRITE_TAC[] THEN
3442 ABBREV_TAC `v:real^3 = v1 - v2` THEN
3443 ABBREV_TAC `w:real^3 = v3 - v2` THEN
3444 ABBREV_TAC `d:real^3 = v4 - v2` THEN
3446 SUBGOAL_THEN `~(d = vec 0:real^3)` ASSUME_TAC THENL
3449 REWRITE_TAC[GSYM NORM_EQ_0; GSYM dist; DIST_SYM] THEN
3450 ASM_SIMP_TAC[REAL_ARITH `&2 <= a ==> ~(a = &0)`];
3455 MP_TAC (ISPECL [`projection d v:real^3`; `projection d w:real^3`; `projection d (--v2):real^3`; `d:real^3`] rotation_lemma_segments) THEN
3456 SUBGOAL_THEN `~(projection d (--v2) = vec 0:real^3)` ASSUME_TAC THENL
3459 REWRITE_TAC[projection] THEN
3460 ABBREV_TAC `k = (--v2 dot (v4 - v2:real^3)) / ((v4 - v2) dot (v4 - v2))` THEN
3461 ASM_CASES_TAC `k = &0` THENL
3463 ASM_REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_SUB_RZERO; VECTOR_NEG_EQ_0];
3467 DISCH_THEN (MP_TAC o AP_TERM `\v:real^3. inv (k) % v`) THEN
3468 ASM_SIMP_TAC[VECTOR_SUB_LDISTRIB; VECTOR_MUL_ASSOC; REAL_MUL_LINV] THEN
3469 REWRITE_TAC[VECTOR_MUL_LID; VECTOR_MUL_RZERO] THEN
3470 REWRITE_TAC[VECTOR_ARITH `a % (--v2) - (v4 - v2) = vec 0 <=> v4 = (&1 - a) % v2:real^3`] THEN
3471 UNDISCH_TAC `~collinear {vec 0,v2,v4} /\ ~(v2 = vec 0) /\ ~(v4 = vec 0:real^3)` THEN
3472 SIMP_TAC[COLLINEAR_LEMMA_ALT; DE_MORGAN_THM; NOT_EXISTS_THM];
3478 SUBGOAL_THEN `v dot n = v1 dot n /\ w dot n = v3 dot n /\ d dot n:real^3 = &0` ASSUME_TAC THENL
3480 MAP_EVERY EXPAND_TAC ["v"; "w"; "d"] THEN
3481 ASM_REWRITE_TAC[DOT_LSUB; REAL_SUB_RZERO];
3484 ASM_REWRITE_TAC[DIMINDEX_3; LE_REFL; PROJECTION_ORTHOGONAL] THEN
3488 DISCH_THEN (MP_TAC o AP_TERM `\x:real^3. x dot n`) THEN
3489 REWRITE_TAC[projection] THEN
3490 ASM_REWRITE_TAC[DOT_LSUB; DOT_LMUL; DOT_LZERO; REAL_MUL_RZERO; REAL_SUB_RZERO] THEN
3491 ASM_SIMP_TAC[REAL_ARITH `a < &0 ==> ~(a = &0)`];
3495 REWRITE_TAC[GSYM MEMBER_NOT_EMPTY] THEN
3496 REWRITE_TAC[IN_INTER; IN_SEGMENT; VECTOR_MUL_RZERO; VECTOR_ADD_LID] THEN
3497 EXISTS_TAC `(&1 - t2 - t4) % projection d (--v2:real^3)` THEN
3500 EXISTS_TAC `&1 - t2 - t4` THEN
3501 ASM_REWRITE_TAC[REAL_ARITH `&0 <= &1 - t2 - t4 <=> t2 + t4 <= &1`] THEN
3502 MATCH_MP_TAC (REAL_ARITH `&0 <= t2 /\ &0 <= t4 ==> &1 - t2 - t4 <= &1`) THEN
3507 EXISTS_TAC `u:real` THEN
3508 ASM_REWRITE_TAC[] THEN
3509 REMOVE_THEN "A" (MP_TAC o AP_TERM `\v:real^3. projection d v`) THEN
3510 REWRITE_TAC[PROJECTION_LINEAR] THEN
3511 ASM_SIMP_TAC[PROJECTION_ZERO; VECTOR_MUL_RZERO; VECTOR_ADD_LID];
3515 DISCH_THEN (X_CHOOSE_THEN `g:real^1->real^3` STRIP_ASSUME_TAC) THEN
3518 ABBREV_TAC `f = (\t:real^1. (g t + v - projection d v) + v2:real^3)` THEN
3520 (* f(0) = v1 and (f(1) dot n) = 0 *)
3521 SUBGOAL_THEN `f (lift (&0)) = v1:real^3 /\ f (lift (&1)) dot n = &0` ASSUME_TAC THENL
3524 ASM_REWRITE_TAC[VECTOR_ARITH `pv + v - pv = v:real^3`] THEN
3527 EXPAND_TAC "v" THEN VECTOR_ARITH_TAC;
3531 REWRITE_TAC[DOT_LADD; DOT_LMUL] THEN
3532 SUBGOAL_THEN `d dot n:real^3 = &0` ASSUME_TAC THENL [ EXPAND_TAC "d" THEN ASM_REWRITE_TAC[DOT_LSUB; REAL_SUB_RZERO]; ALL_TAC ] THEN
3533 SUBGOAL_THEN `(v - projection d v) dot n:real^3 = &0` (fun th -> REWRITE_TAC[th]) THENL
3535 GEN_REWRITE_TAC (PAT_CONV `\x:real^3. (x - y) dot z = &0`) [VECTOR_PROJECTION] THEN
3536 REWRITE_TAC[VECTOR_ARITH `(a + b) - a = b:real^3`] THEN
3537 ASM_REWRITE_TAC[DOT_LMUL; REAL_MUL_RZERO];
3541 ASM_REWRITE_TAC[projection; DOT_LSUB; DOT_LMUL; DOT_LNEG; REAL_MUL_RZERO; REAL_SUB_LZERO; REAL_NEG_0; REAL_ADD_LID];
3545 (* d(f(t), v2) = d(v1, v2) *)
3546 SUBGOAL_THEN `!t. dist (f (t:real^1), v2:real^3) = dist (v1, v2) /\ dist (f t, v4) = dist (v1, v4)` ASSUME_TAC THENL
3548 GEN_TAC THEN EXPAND_TAC "f" THEN
3549 REWRITE_TAC[dist; VECTOR_ARITH `(a + b) - b = a:real^3 - vec 0`] THEN
3550 REWRITE_TAC[VECTOR_ARITH `((a + b - c) + v2) - v4 = (a + b - c) - (v4 - v2:real^3)`] THEN
3551 REWRITE_TAC[GSYM dist; DIST_EQ] THEN
3552 ASM_SIMP_TAC[PROJECTION_DIST_SPECIAL_EQ; PROJECTION_ZERO] THEN
3553 ASM_REWRITE_TAC[PROJECTION_0; DIST_0] THEN
3554 EXPAND_TAC "v" THEN EXPAND_TAC "d" THEN REWRITE_TAC[dist] THEN
3555 REWRITE_TAC[VECTOR_ARITH `v1 - v2 - (v4 - v2) = v1 - v4:real^3`] THEN
3560 (* d(f(t), v3) <= d(v1,v3) <= 2 h0 *)
3561 SUBGOAL_THEN `!t. &0 <= t /\ t <= &1 ==> dist (f (lift t), v3:real^3) <= &2 * h0` MP_TAC THENL
3563 REPEAT STRIP_TAC THEN
3564 MATCH_MP_TAC REAL_LE_TRANS THEN
3565 EXISTS_TAC `dist (v1,v3:real^3)` THEN
3566 ASM_REWRITE_TAC[] THEN
3568 REWRITE_TAC[dist] THEN
3569 ASM_REWRITE_TAC[VECTOR_ARITH `((g + v - pv) + v2) - v3:real^3 = (g + v - pv) - (v3 - v2)`] THEN
3570 GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV) [VECTOR_ARITH `v1 - v3 = (v1 - v2) - (v3 - v2:real^3)`] THEN
3571 ASM_REWRITE_TAC[] THEN
3572 REWRITE_TAC[GSYM dist] THEN
3573 MATCH_MP_TAC PROJECTION_DIST_SPECIAL_LE THEN
3578 (* |f(t)| <= |v1| *)
3579 SUBGOAL_THEN `!t. &0 <= t /\ t <= &1 ==> norm (f (lift t):real^3) <= norm (v1:real^3)` MP_TAC THENL
3581 REPEAT STRIP_TAC THEN
3583 ASM_REWRITE_TAC[VECTOR_ARITH `(g + v - pv) + v2:real^3 = (g + v - pv) - (--v2)`] THEN
3584 GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV) [VECTOR_ARITH `v1 = (v1 - v2) - (--v2:real^3)`] THEN
3585 ASM_REWRITE_TAC[] THEN
3586 REWRITE_TAC[GSYM dist] THEN
3587 MATCH_MP_TAC PROJECTION_DIST_SPECIAL_LE THEN
3592 REPEAT DISCH_TAC THEN
3594 (* If 2 <= |f(t)|, then f IN ball_annulus *)
3595 SUBGOAL_THEN `!t. &0 <= t /\ t <= &1 /\ &2 <= norm (f (lift t):real^3) ==> f (lift t) IN ball_annulus` ASSUME_TAC THENL
3597 REPEAT STRIP_TAC THEN
3598 ASM_SIMP_TAC[in_ball_annulus; GSYM NORM_EQ_0; REAL_ARITH `&2 <= a ==> ~(a = &0)`] THEN
3599 MATCH_MP_TAC REAL_LE_TRANS THEN
3600 EXISTS_TAC `norm (v1:real^3)` THEN
3602 UNDISCH_TAC `v1 IN ball_annulus` THEN
3603 SIMP_TAC[in_ball_annulus];
3607 SUBGOAL_THEN `f:real^1->real^3 continuous_on interval [lift (&0), lift (&1)]` ASSUME_TAC THENL
3610 REPEAT (MATCH_MP_TAC CONTINUOUS_ON_ADD THEN REWRITE_TAC[CONTINUOUS_ON_CONST]) THEN
3611 MATCH_MP_TAC CONTINUOUS_ON_SUBSET THEN
3612 EXISTS_TAC `UNIV:real^1->bool` THEN
3613 ASM_REWRITE_TAC[SUBSET_UNIV];
3617 REPLICATE_TAC 2 (FIRST_X_ASSUM (MP_TAC o check (free_in `g:real^1->real^3` o concl))) THEN
3618 SUBGOAL_THEN `!t:real^1. projection d (g t) = (g t):real^3` MP_TAC THENL
3620 GEN_TAC THEN REWRITE_TAC[projection] THEN
3621 ASM_REWRITE_TAC[real_div; REAL_MUL_LZERO; VECTOR_MUL_LZERO; VECTOR_SUB_RZERO];
3625 REPEAT (FIRST_X_ASSUM ((fun th -> ALL_TAC) o check (free_in `g:real^1->real^3` o concl))) THEN
3626 REPEAT DISCH_TAC THEN
3628 ASM_CASES_TAC `!h. &0 <= h /\ h <= &1 ==> &2 <= norm (f (lift h):real^3)` THENL
3630 MATCH_MP_TAC (TAUT `F ==> A`) THEN
3631 MP_TAC (SPECL [`v2:real^3`; `v4:real^3`; `f:real^1->real^3`; `v3:real^3`; `&1`] continuous_lemma_aff_ge) THEN
3634 ASM_REWRITE_TAC[REAL_LE_01] THEN
3635 GEN_TAC THEN DISCH_TAC THEN
3636 SUBGOAL_THEN `t:real^1 = lift (drop t)` (fun th -> ONCE_REWRITE_TAC[th]) THENL [ REWRITE_TAC[LIFT_DROP]; ALL_TAC ] THEN
3637 SUBGOAL_THEN `&0 <= drop (t:real^1) /\ drop t <= &1` ASSUME_TAC THENL
3639 ASM_REWRITE_TAC[GSYM IN_INTERVAL_1; LIFT_DROP];
3642 MATCH_MP_TAC zero_not_between_estd THEN
3647 DISCH_THEN DISJ_CASES_TAC THENL
3649 MP_TAC (ISPECL [`v2:real^3`; `v4:real^3`; `f (lift (&1)):real^3`; `v3:real^3`; `n:real^3`] segment_inter_aff_ge_ends) THEN
3650 ASM_SIMP_TAC[REAL_ARITH `&0 < a ==> ~(a = &0)`; IN_INTERVAL_1; REAL_LE_REFL; REAL_LE_01] THEN
3652 MATCH_MP_TAC LEMMA_3_POINTS_FINAL THEN
3653 MAP_EVERY EXISTS_TAC [`v2:real^3`; `v4:real^3`; `f (lift (&1)):real^3`] THEN
3654 ASM_SIMP_TAC[DIST_SYM; REAL_LE_REFL; REAL_LE_01];
3658 POP_ASSUM MP_TAC THEN STRIP_TAC THEN MATCH_MP_TAC LEMMA_3_POINTS_FINAL THENL
3660 MAP_EVERY EXISTS_TAC [`v2:real^3`; `v4:real^3`; `f (lift x):real^3`] THEN
3661 ASM_SIMP_TAC[DIST_SYM];
3662 MAP_EVERY EXISTS_TAC [`f (lift x):real^3`; `v3:real^3`; `v2:real^3`] THEN
3663 ASM_SIMP_TAC[DIST_SYM];
3664 MAP_EVERY EXISTS_TAC [`f (lift x):real^3`; `v3:real^3`; `v4:real^3`] THEN
3665 ASM_SIMP_TAC[DIST_SYM]
3671 POP_ASSUM MP_TAC THEN REWRITE_TAC[NOT_FORALL_THM; NOT_IMP; REAL_NOT_LE] THEN
3672 DISCH_THEN (CHOOSE_THEN ASSUME_TAC) THEN
3674 SUBGOAL_THEN `?s. &0 <= s /\ s <= &1 /\ norm (f (lift s):real^3) = &2 /\ (!t. &0 <= t /\ t <= s ==> &2 <= norm (f (lift t)))` MP_TAC THENL
3676 MP_TAC (SPECL [`\t:real. norm (f (lift t):real^3)`; `&2`; `h:real`] continuous_lemma_dec) THEN
3679 ASM_SIMP_TAC[REAL_LT_IMP_LE] THEN
3680 UNDISCH_TAC `v1 IN ball_annulus` THEN
3681 SIMP_TAC[in_ball_annulus] THEN DISCH_TAC THEN
3682 REWRITE_TAC[REAL_CONTINUOUS_ON; IMAGE_LIFT_REAL_INTERVAL] THEN
3683 SUBGOAL_THEN `lift o (\t. norm (f (lift t):real^3)) o drop = (lift o norm) o f` (fun th -> REWRITE_TAC[th]) THENL
3685 REWRITE_TAC[FUN_EQ_THM; o_THM; LIFT_DROP];
3688 MATCH_MP_TAC CONTINUOUS_ON_COMPOSE THEN
3689 REWRITE_TAC[CONTINUOUS_ON_LIFT_NORM] THEN
3690 MATCH_MP_TAC CONTINUOUS_ON_SUBSET THEN
3691 EXISTS_TAC `interval [lift (&0), lift (&1)]` THEN
3692 ASM_REWRITE_TAC[SUBSET_INTERVAL_1; LIFT_DROP; REAL_LE_REFL];
3696 BETA_TAC THEN STRIP_TAC THEN
3697 EXISTS_TAC `x:real` THEN
3698 ASM_REWRITE_TAC[] THEN
3699 CONJ_TAC THENL [ MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `h:real` THEN ASM_REWRITE_TAC[]; ALL_TAC ] THEN
3700 REPEAT STRIP_TAC THEN
3701 ASM_CASES_TAC `t = x:real` THENL [ ASM_REWRITE_TAC[REAL_LE_REFL]; ALL_TAC ] THEN
3702 MATCH_MP_TAC REAL_LT_IMP_LE THEN
3703 FIRST_X_ASSUM MATCH_MP_TAC THEN
3704 ASM_REWRITE_TAC[REAL_LT_LE];
3708 SUBGOAL_THEN `!t. t <= s ==> t <= &1` ASSUME_TAC THENL
3710 REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_LE_TRANS THEN
3711 EXISTS_TAC `s:real` THEN ASM_REWRITE_TAC[];
3716 MP_TAC (SPECL [`v2:real^3`; `v4:real^3`; `f:real^1->real^3`; `v3:real^3`; `s:real`] continuous_lemma_aff_ge) THEN
3719 ASM_REWRITE_TAC[] THEN
3722 MATCH_MP_TAC CONTINUOUS_ON_SUBSET THEN
3723 EXISTS_TAC `interval [lift (&0), lift (&1)]` THEN
3724 ASM_REWRITE_TAC[SUBSET_INTERVAL_1; LIFT_DROP; REAL_LE_REFL];
3728 GEN_TAC THEN DISCH_TAC THEN
3729 SUBGOAL_THEN `t:real^1 = lift (drop t)` (fun th -> ONCE_REWRITE_TAC[th]) THENL [ REWRITE_TAC[LIFT_DROP]; ALL_TAC ] THEN
3730 SUBGOAL_THEN `&0 <= drop (t:real^1) /\ drop t <= s` ASSUME_TAC THENL
3732 ASM_REWRITE_TAC[GSYM IN_INTERVAL_1; LIFT_DROP];
3735 MATCH_MP_TAC zero_not_between_estd THEN
3740 ONCE_REWRITE_TAC[DISJ_SYM] THEN
3741 DISCH_THEN DISJ_CASES_TAC THENL
3743 MATCH_MP_TAC (TAUT `F ==> A`) THEN
3744 POP_ASSUM MP_TAC THEN STRIP_TAC THEN MATCH_MP_TAC LEMMA_3_POINTS_FINAL THENL
3746 MAP_EVERY EXISTS_TAC [`v2:real^3`; `v4:real^3`; `f (lift x):real^3`] THEN
3747 ASM_SIMP_TAC[DIST_SYM];
3748 MAP_EVERY EXISTS_TAC [`f (lift x):real^3`; `v3:real^3`; `v2:real^3`] THEN
3749 ASM_SIMP_TAC[DIST_SYM];
3750 MAP_EVERY EXISTS_TAC [`f (lift x):real^3`; `v3:real^3`; `v4:real^3`] THEN
3751 ASM_SIMP_TAC[DIST_SYM]
3756 EXISTS_TAC `f (lift s):real^3` THEN
3757 ASM_SIMP_TAC[REAL_LE_REFL] THEN
3759 (* [f(s), v3] INTER convex hull {0,v2,v4} *)
3760 MATCH_MP_TAC segment_inter_conv THEN
3761 ASM_REWRITE_TAC[] THEN
3763 MP_TAC (SPECL [`f (lift s):real^3`; `v2:real^3`; `v3:real^3`; `v4:real^3`] separation_plane_4_points) THEN
3766 ASM_SIMP_TAC[REAL_LE_REFL] THEN
3767 FIRST_X_ASSUM MATCH_MP_TAC THEN
3768 ASM_REWRITE_TAC[IN_INTERVAL_1; REAL_LE_REFL];
3772 REPEAT (FIRST_X_ASSUM ((fun th -> ALL_TAC) o check (free_in `n:real^3` o concl))) THEN
3774 EXISTS_TAC `n:real^3` THEN
3775 ASM_REWRITE_TAC[] THEN
3778 ONCE_REWRITE_TAC[VECTOR_ARITH `v2 = v4:real^3 <=> v4 - v2 = vec 0`] THEN
3785 FIRST_X_ASSUM MATCH_MP_TAC THEN
3786 ASM_REWRITE_TAC[IN_INTERVAL_1; REAL_LE_REFL];
3790 SUBGOAL_THEN `projection d (f (lift s) - v2:real^3) = projection d (g (lift s))` (fun th -> REWRITE_TAC[th]) THENL
3793 REWRITE_TAC[VECTOR_ARITH `(a + v2) - v2 = a:real^3`] THEN
3794 REWRITE_TAC[PROJECTION_LINEAR] THEN
3795 SUBGOAL_THEN `?a. v - projection d v = a % d:real^3` MP_TAC THENL
3797 EXISTS_TAC `(v dot d:real^3) / (d dot d)` THEN
3798 REWRITE_TAC[projection] THEN
3803 ASM_SIMP_TAC[PROJECTION_LINEAR; PROJECTION_ZERO; VECTOR_MUL_RZERO; VECTOR_ADD_RID];
3811 (******************************************************************)
3814 let lemma_4_points_rotation2_full = prove(`!v1 v2 v3 v4. v1 IN ball_annulus /\ v2 IN ball_annulus /\ v3 IN ball_annulus /\ v4 IN ball_annulus /\
3815 dist (v1,v3) <= &2 * h0 /\ dist (v2,v4) <= &2 * h0 /\
3816 &2 <= dist (v1,v2) /\ &2 <= dist (v1,v4) /\
3817 &2 <= dist (v2,v3) /\ &2 <= dist (v3,v4) /\
3818 &2 <= dist (v2,v4) /\
3819 ~(segment [v1,v3] INTER convex hull {vec 0, v2, v4} = {})
3820 ==> (?v1' v3'. v1' IN ball_annulus /\ v3' IN ball_annulus /\
3821 norm v1' = &2 /\ norm v3' = &2 /\
3822 dist (v1',v3') <= &2 * h0 /\
3823 dist (v1',v2) = dist (v1,v2) /\ dist (v1',v4) = dist (v1,v4) /\
3824 dist (v2,v3') = dist (v2,v3) /\ dist (v3',v4) = dist (v3,v4) /\
3825 ~(segment [v1',v3'] INTER aff_ge {vec 0} {v2, v4} = {}))`,
3826 REPEAT STRIP_TAC THEN
3827 (* v1 about v2-v4 *)
3828 MP_TAC (SPEC_ALL lemma_4_points_rotation2) THEN
3829 ASM_REWRITE_TAC[] THEN
3831 EXISTS_TAC `v1':real^3` THEN
3832 ASM_REWRITE_TAC[] THEN
3834 (* v3 about v2-v4 *)
3835 MP_TAC (SPECL [`v3:real^3`; `v2:real^3`; `v1':real^3`; `v4:real^3`] lemma_4_points_rotation2) THEN
3836 ASM_REWRITE_TAC[REAL_LE_REFL; DIST_SYM; SEGMENT_SYM] THEN
3837 DISCH_THEN (X_CHOOSE_THEN `v3':real^3` MP_TAC) THEN REWRITE_TAC[DIST_SYM] THEN
3839 EXISTS_TAC `v3':real^3` THEN
3840 ASM_REWRITE_TAC[DIST_SYM] THEN
3842 POP_ASSUM MP_TAC THEN
3843 REWRITE_TAC[GSYM MEMBER_NOT_EMPTY; IN_INTER] THEN
3845 EXISTS_TAC `x:real^3` THEN ASM_REWRITE_TAC[] THEN
3846 MATCH_MP_TAC Hypermap.lemma_in_subset THEN
3847 EXISTS_TAC `convex hull {vec 0, v2, v4:real^3}` THEN
3848 ASM_REWRITE_TAC[] THEN
3849 UNDISCH_TAC `v2 IN ball_annulus` THEN
3850 UNDISCH_TAC `v4 IN ball_annulus` THEN
3851 SIMP_TAC[in_ball_annulus; aff_ge_0_2] THEN
3852 REPEAT DISCH_TAC THEN
3853 REWRITE_TAC[SUBSET; CONVEX_HULL_3_ALT; IN_ELIM_THM; VECTOR_SUB_RZERO; VECTOR_ADD_LID] THEN
3854 REPEAT STRIP_TAC THEN
3855 MAP_EVERY EXISTS_TAC [`u:real`; `v:real`] THEN
3856 ASM_REWRITE_TAC[]);;
3861 (******************************************************************************************)
3864 (* Prove that a certain configuration of 4 points is impossible *)
3866 let lemma_4_points_circumcenter = prove(`!v1 v2 v3 v4. ~(collinear {vec 0,v2,v4}) /\
3867 v2 IN ball_annulus /\ v4 IN ball_annulus /\
3868 ~(segment [v1,v3] INTER aff_ge {vec 0} {v2,v4} = {}) /\
3869 norm v1 = &2 /\ norm v3 = &2 /\
3870 dist (v1,v2) = &2 /\ dist (v1,v4) = &2 /\
3871 dist (v3,v2) = &2 /\ dist (v3,v4) = &2
3872 ==> norm(v1 + v3) = &2 * eta_y (norm v2) (norm v4) (dist (v2,v4))`,
3873 REWRITE_TAC[in_ball_annulus] THEN
3874 REPEAT STRIP_TAC THEN
3875 SUBGOAL_THEN `!v w:real^3. norm v = &2 /\ dist (v,w) = &2 ==> v dot w = norm w pow 2 / &2` ASSUME_TAC THENL
3877 REWRITE_TAC[DIST_SQR; REAL_ARITH `&0 <= &2`] THEN
3878 REWRITE_TAC[dist; NORM_POW_2] THEN
3879 REWRITE_TAC[DOT_LSUB; DOT_RSUB; DOT_SQUARE_NORM; DOT_SYM] THEN
3881 STRIP_TAC THEN POP_ASSUM MP_TAC THEN
3882 ASM_REWRITE_TAC[] THEN
3886 FIRST_ASSUM (MP_TAC o SPECL [`v1:real^3`; `v2:real^3`]) THEN
3887 FIRST_ASSUM (MP_TAC o SPECL [`v1:real^3`; `v4:real^3`]) THEN
3888 FIRST_ASSUM (MP_TAC o SPECL [`v3:real^3`; `v2:real^3`]) THEN
3889 FIRST_X_ASSUM (MP_TAC o SPECL [`v3:real^3`; `v4:real^3`]) THEN
3890 ASM_REWRITE_TAC[DOT_SYM] THEN
3891 REPEAT STRIP_TAC THEN
3893 ABBREV_TAC `v = inv(&2) % (v1 + v3:real^3)` THEN
3895 SUBGOAL_THEN `v:real^3 IN affine hull {vec 0,v2,v4}` ASSUME_TAC THENL
3897 FIRST_X_ASSUM (MP_TAC o check (is_neg o concl)) THEN
3898 REWRITE_TAC[GSYM MEMBER_NOT_EMPTY] THEN
3899 REWRITE_TAC[IN_INTER; IN_SEGMENT] THEN
3900 ASM_SIMP_TAC[aff_ge_0_2; IN_ELIM_THM] THEN
3902 SUBGOAL_THEN `x:real^3 dot v1 = x dot v3` MP_TAC THENL
3904 POP_ASSUM (fun th -> REWRITE_TAC[th]) THEN
3905 ASM_REWRITE_TAC[DOT_LADD; DOT_LMUL; DOT_SYM];
3908 POP_ASSUM (LABEL_TAC "A" o SYM) THEN
3909 ASM_REWRITE_TAC[DOT_LADD; DOT_LMUL] THEN
3910 ASM_REWRITE_TAC[DOT_SYM; DOT_SQUARE_NORM; REAL_ARITH `&2 pow 2 = &4`] THEN
3911 ONCE_REWRITE_TAC[REAL_ARITH `a = b <=> a - b = &0`] THEN
3912 REWRITE_TAC[REAL_ARITH `((&1 - u) * &4 + u * a13) - ((&1 - u) * a13 + u * &4) = &2 * u * (a13 - &4) - (a13 - &4)`] THEN
3914 ASM_CASES_TAC `v1:real^3 dot v3 = &4` THENL
3916 DISCH_THEN (fun th -> ALL_TAC) THEN
3917 SUBGOAL_THEN `norm (v3) % v1:real^3 = norm (v1) % v3` MP_TAC THENL
3919 REWRITE_TAC[GSYM NORM_CAUCHY_SCHWARZ_EQ] THEN
3920 ASM_REWRITE_TAC[DOT_SYM] THEN
3924 ASM_REWRITE_TAC[VECTOR_ARITH `&2 % v1 = &2 % v3 <=> v1 = v3`] THEN
3925 DISCH_TAC THEN UNDISCH_TAC `x = (&1 - u) % v1 + u % v3:real^3` THEN
3927 POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN
3928 REWRITE_TAC[VECTOR_ARITH `(&1 - u) % v1 + u % v1 = v1:real^3`] THEN
3930 REWRITE_TAC[VECTOR_ARITH `inv(&2) % (v1 + v1) = v1:real^3`] THEN
3931 DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN
3932 REWRITE_TAC[AFFINE_HULL_3; IN_ELIM_THM] THEN
3933 MAP_EVERY EXISTS_TAC [`&1 - t1 - t2`; `t1:real`; `t2:real`] THEN
3934 CONJ_TAC THENL [ REAL_ARITH_TAC; ALL_TAC ] THEN
3940 SUBGOAL_THEN `u = inv(&2)` ASSUME_TAC THENL
3942 POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN
3943 CONV_TAC REAL_FIELD;
3947 SUBGOAL_THEN `v = x:real^3` (fun th -> REWRITE_TAC[th]) THENL
3949 ASM_REWRITE_TAC[] THEN
3956 REWRITE_TAC[AFFINE_HULL_3; IN_ELIM_THM] THEN
3957 MAP_EVERY EXISTS_TAC [`&1 - t1 - t2`; `t1:real`; `t2:real`] THEN
3958 CONJ_TAC THENL [ REAL_ARITH_TAC; ALL_TAC ] THEN
3963 SUBGOAL_THEN `dist (v:real^3,v2) = norm v /\ dist (v,v4) = norm v` ASSUME_TAC THENL
3965 REWRITE_TAC[DIST_SQR] THEN
3966 REWRITE_TAC[dist; NORM_POS_LE; NORM_POW_2] THEN
3967 REWRITE_TAC[DOT_LSUB; DOT_RSUB] THEN
3968 REWRITE_TAC[REAL_ARITH `a - b - c = a <=> b + c = &0`] THEN
3970 REWRITE_TAC[DOT_LMUL; DOT_RMUL; DOT_LADD; DOT_RADD] THEN
3971 ASM_REWRITE_TAC[DOT_SYM; DOT_SQUARE_NORM] THEN
3976 SUBGOAL_THEN `v:real^3 = circumcenter {vec 0,v2,v4}` ASSUME_TAC THENL
3978 MATCH_MP_TAC (GEN_ALL Collect_geom.DIST_EQ_IS_UNIQUE) THEN
3979 MAP_EVERY EXISTS_TAC [`v2:real^3`; `v4:real^3`; `vec 0:real^3`] THEN
3980 ASM_REWRITE_TAC[DIST_0] THEN
3981 MP_TAC (SPECL [`vec 0:real^3`; `v2:real^3`; `v4:real^3`] Collect_geom.CIRCUMCENTER_PROPTIES) THEN
3982 ASM_REWRITE_TAC[] THEN
3984 FIRST_ASSUM (MP_TAC o SPEC `vec 0:real^3`) THEN
3985 SIMP_TAC[IN_INSERT; DIST_0] THEN
3986 DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN
3987 FIRST_ASSUM (MP_TAC o SPEC `v2:real^3`) THEN
3988 FIRST_ASSUM (MP_TAC o SPEC `v4:real^3`) THEN
3989 SIMP_TAC[IN_INSERT] THEN
3990 REPEAT (DISCH_THEN (fun th -> ALL_TAC)) THEN
3991 REWRITE_TAC[SUBSET; IN_INSERT; NOT_IN_EMPTY] THEN
3993 STRIP_TAC THEN ASM_REWRITE_TAC[];
3997 SUBGOAL_THEN `norm (v:real^3) = radV {vec 0,v2,v4:real^3}` ASSUME_TAC THENL
3999 ASM_REWRITE_TAC[GSYM DIST_0; DIST_SYM] THEN
4000 MP_TAC (GEN_ALL Collect_geom.NOT_COL_IMP_RADV_PROPERTIY) THEN
4001 DISCH_THEN (MP_TAC o SPECL [`vec 0:real^3`; `v2:real^3`; `v4:real^3`]) THEN
4002 ASM_REWRITE_TAC[] THEN
4003 DISCH_THEN (MATCH_MP_TAC o GSYM) THEN
4004 ONCE_REWRITE_TAC[GSYM IN] THEN
4005 REWRITE_TAC[IN_INSERT];
4009 POP_ASSUM MP_TAC THEN
4010 MP_TAC (SPECL [`v4:real^3`; `v2:real^3`; `vec 0:real^3`; `norm (v2:real^3)`; `norm (v4:real^3)`; `dist (v2:real^3,v4:real^3)`] Collect_geom.CDEUSDF) THEN
4011 REWRITE_TAC[Collect_geom.dist3; DIST_0; DIST_SYM] THEN
4012 SUBGOAL_THEN `{v4,v2,vec 0:real^3} = {vec 0,v2,v4}` (fun th -> ONCE_REWRITE_TAC[th]) THENL
4018 ASM_REWRITE_TAC[] THEN
4019 REPLICATE_TAC 2 (DISCH_THEN (CONJUNCTS_THEN2 (fun th -> ALL_TAC) MP_TAC)) THEN
4020 DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
4021 DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN
4023 REWRITE_TAC[NORM_MUL] THEN
4028 let PARALLELOGRAM_LAW = prove(`!v1 v2:real^N. &2 * (norm v1 pow 2 + norm v2 pow 2) = norm (v1 + v2) pow 2 + norm (v1 - v2) pow 2`,
4030 REWRITE_TAC[NORM_POW_2] THEN
4035 let lemma_4_points_contradiction = prove(`!v1 v2 v3 v4.
4036 v2 IN ball_annulus /\ v4 IN ball_annulus /\
4037 &2 <= dist (v2,v4) /\ dist (v2,v4) <= &2 * h0 /\
4038 ~(segment [v1,v3] INTER aff_ge {vec 0} {v2, v4} = {}) /\
4039 norm v1 = &2 /\ norm v3 = &2 /\
4040 dist (v1,v2) = &2 /\ dist (v1,v4) = &2 /\
4041 dist (v3,v2) = &2 /\ dist (v3,v4) = &2 /\
4042 dist (v1,v3) <= &2 * h0
4044 REPEAT STRIP_TAC THEN
4045 SUBGOAL_THEN `~collinear {vec 0:real^3,v2,v4}` ASSUME_TAC THENL
4047 MATCH_MP_TAC estd_non_collinear_lemma THEN
4051 MP_TAC (SPEC_ALL lemma_4_points_circumcenter) THEN
4052 ASM_REWRITE_TAC[] THEN
4054 MP_TAC (ISPECL [`v1:real^3`; `v3:real^3`] PARALLELOGRAM_LAW) THEN
4055 ASM_REWRITE_TAC[GSYM dist] THEN
4056 MATCH_MP_TAC (REAL_ARITH `a < b ==> ~(b = a)`) THEN
4057 CONV_TAC REAL_RAT_REDUCE_CONV THEN
4058 ONCE_REWRITE_TAC[REAL_ARITH `&16 = (&16 - (&2 * h0) pow 2) + (&2 * h0) pow 2`] THEN
4059 MATCH_MP_TAC REAL_LTE_ADD2 THEN
4062 MATCH_MP_TAC REAL_LET_TRANS THEN
4063 EXISTS_TAC `&4 * #2.2` THEN
4066 REWRITE_TAC[REAL_POW_MUL] THEN
4067 MATCH_MP_TAC REAL_LE_MUL2 THEN
4068 ASM_REWRITE_TAC[Collect_geom.REAL_LE_POW_2; REAL_ARITH `&2 pow 2 <= &4`] THEN
4070 MP_TAC Tame_inequalities.ETA_Y_4_POINTS_INEQ THEN
4072 REWRITE_TAC[Tame_inequalities.INEQ_ALT; ALL] THEN
4073 DISCH_THEN MATCH_MP_TAC THEN
4074 REPEAT (FIRST_X_ASSUM (MP_TAC o check (is_binary "IN" o concl))) THEN
4075 ASM_SIMP_TAC[in_ball_annulus];
4078 REWRITE_TAC[Sphere.h0] THEN
4083 REWRITE_TAC[GSYM REAL_LE_SQUARE_ABS] THEN
4084 REWRITE_TAC[dist; REAL_ABS_NORM] THEN
4085 REWRITE_TAC[GSYM dist] THEN
4086 UNDISCH_TAC `dist(v1,v3:real^3) <= &2 * h0` THEN
4087 REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);;
4091 (* The final result *)
4093 let LEMMA_4_POINTS_FINAL = prove(`!v1 v2 v3 v4. v1 IN ball_annulus /\ v2 IN ball_annulus /\ v3 IN ball_annulus /\ v4 IN ball_annulus /\
4094 dist (v1, v3) <= &2 * h0 /\ dist (v2, v4) <= &2 * h0 /\
4095 &2 <= dist (v1,v2) /\ &2 <= dist (v1,v4) /\
4096 &2 <= dist (v2,v3) /\ &2 <= dist (v3,v4) /\
4097 &2 <= dist (v1,v3) /\ &2 <= dist (v2,v4)
4098 ==> aff_ge {vec 0} {v1,v3} INTER aff_ge {vec 0} {v2,v4} = {vec 0}`,
4099 REPEAT STRIP_TAC THEN
4100 ASM_CASES_TAC `aff_ge {vec 0} {v1,v3} INTER aff_ge {vec 0} {v2,v4} = {vec 0:real^3}` THEN ASM_REWRITE_TAC[] THEN
4101 SUBGOAL_THEN `?p. ~(p = vec 0:real^3) /\ p IN aff_ge {vec 0} {v1,v3} INTER aff_ge {vec 0} {v2,v4}` MP_TAC THENL
4103 POP_ASSUM MP_TAC THEN
4104 REWRITE_TAC[EXTENSION; IN_SING; NOT_FORALL_THM] THEN
4105 DISCH_THEN (CHOOSE_THEN MP_TAC) THEN
4106 ASM_CASES_TAC `x = vec 0:real^3` THENL
4108 ASM_REWRITE_TAC[IN_INTER; points_in_aff_ge_0_2];
4111 ASM_REWRITE_TAC[] THEN
4113 EXISTS_TAC `x:real^3` THEN
4119 POP_ASSUM MP_TAC THEN
4120 SUBGOAL_THEN `~(v1 = vec 0:real^3) /\ ~(v2 = vec 0:real^3) /\ ~(v3 = vec 0:real^3) /\ ~(v4 = vec 0:real^3)` ASSUME_TAC THENL
4122 REPEAT (FIRST_X_ASSUM (MP_TAC o check (is_binary "IN" o concl))) THEN
4123 SIMP_TAC[in_ball_annulus];
4127 ASM_SIMP_TAC[aff_ge_0_2; IN_ELIM_THM; IN_INTER] THEN
4129 UNDISCH_TAC `p = t1 % v1 + t2 % v3:real^3` THEN
4130 POP_ASSUM (LABEL_TAC "p2" o SYM) THEN
4131 DISCH_THEN (LABEL_TAC "p1" o SYM) THEN
4133 SUBGOAL_THEN `!v v1 v2 v3 v4 t1 t2 t1' t2'. &0 <= t1 /\ &0 <= t2 /\ &0 <= t1' /\ &0 <= t2' /\ ~(v = vec 0) /\
4134 t1 % v1 + t2 % v3 = v /\ t1' % v2 + t2' % v4 = v /\
4135 t1' + t2' <= t1 + t2
4136 ==> ~(segment [v1,v3] INTER convex hull {vec 0,v2,v4:real^3} = {})` ASSUME_TAC THENL
4138 REPEAT REMOVE_ASSUM THEN
4139 REWRITE_TAC[GSYM MEMBER_NOT_EMPTY] THEN
4140 REPEAT STRIP_TAC THEN
4141 SUBGOAL_THEN `&0 < t1 + t2` ASSUME_TAC THENL
4143 ASM_CASES_TAC `t1 = &0` THENL
4145 UNDISCH_TAC `t1 % v1 + t2 % v3:real^3 = v` THEN
4146 POP_ASSUM (fun th -> REWRITE_TAC[th]) THEN
4147 REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_LID] THEN
4148 ASM_CASES_TAC `t2 = &0` THENL
4150 POP_ASSUM (fun th -> REWRITE_TAC[th; VECTOR_MUL_LZERO; VECTOR_ADD_LID]) THEN
4155 ASM_REWRITE_TAC[REAL_ADD_LID; REAL_LT_LE];
4159 MATCH_MP_TAC REAL_LTE_ADD THEN
4160 ASM_REWRITE_TAC[REAL_LT_LE];
4164 REWRITE_TAC[IN_INTER; IN_SEGMENT; CONVEX_HULL_3_ALT; IN_ELIM_THM] THEN
4165 EXISTS_TAC `inv (t1 + t2) % v:real^3` THEN
4168 EXISTS_TAC `t2 * inv (t1 + t2)` THEN
4171 MATCH_MP_TAC REAL_LE_MUL THEN ASM_REWRITE_TAC[] THEN
4172 MATCH_MP_TAC REAL_LE_INV THEN ASM_SIMP_TAC[REAL_LT_IMP_LE];
4178 REWRITE_TAC[GSYM real_div] THEN
4179 MATCH_MP_TAC Trigonometry2.REAL_LE_LDIV THEN
4180 ASM_REWRITE_TAC[REAL_ARITH `t2 <= t1 + t2 <=> &0 <= t1`];
4184 UNDISCH_TAC `t1 % v1 + t2 % v3:real^3 = v` THEN
4185 DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN
4186 SUBGOAL_THEN `&1 - t2 * inv(t1 + t2) = t1 * inv (t1 + t2)` (fun th -> REWRITE_TAC[th]) THENL
4188 MATCH_MP_TAC REAL_EQ_RCANCEL_IMP THEN
4189 EXISTS_TAC `t1 + t2:real` THEN
4190 REWRITE_TAC[REAL_SUB_RDISTRIB] THEN
4191 ONCE_REWRITE_TAC[GSYM REAL_MUL_ASSOC] THEN
4192 ASM_SIMP_TAC[REAL_ARITH `&0 < a ==> ~(a = &0)`; REAL_MUL_LINV] THEN
4201 REWRITE_TAC[VECTOR_ADD_LID; VECTOR_SUB_RZERO] THEN
4202 MAP_EVERY EXISTS_TAC [`inv (t1 + t2) * t1'`; `inv (t1 + t2) * t2'`] THEN
4203 REWRITE_TAC[CONJ_ASSOC] THEN
4208 CONJ_TAC THEN MATCH_MP_TAC REAL_LE_MUL THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC REAL_LE_INV THEN ASM_SIMP_TAC[REAL_LT_IMP_LE];
4212 REWRITE_TAC[GSYM REAL_ADD_LDISTRIB; REAL_MUL_AC; GSYM real_div] THEN
4213 MATCH_MP_TAC Trigonometry2.REAL_LE_LDIV THEN
4218 UNDISCH_TAC `t1' % v2 + t2' % v4:real^3 = v` THEN
4219 DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN
4224 SUBGOAL_THEN `?v1 v2 v3 v4. v1 IN ball_annulus /\ v2 IN ball_annulus /\ v3 IN ball_annulus /\ v4 IN ball_annulus /\
4225 dist (v1,v3) <= &2 * h0 /\ dist (v2,v4) <= &2 * h0 /\
4226 &2 <= dist (v1,v2) /\ &2 <= dist (v1,v4) /\
4227 &2 <= dist (v2,v3) /\ &2 <= dist (v3,v4) /\
4228 &2 <= dist (v2,v4) /\
4229 ~(segment [v1,v3] INTER convex hull {vec 0,v2,v4} = {})` MP_TAC THENL
4231 ASM_CASES_TAC `t1' + t2' <= t1 + t2:real` THENL
4233 MAP_EVERY EXISTS_TAC [`v1:real^3`; `v2:real^3`; `v3:real^3`; `v4:real^3`] THEN
4234 ASM_REWRITE_TAC[] THEN
4235 FIRST_X_ASSUM MATCH_MP_TAC THEN
4236 MAP_EVERY EXISTS_TAC [`p:real^3`; `t1:real`; `t2:real`; `t1':real`; `t2':real`] THEN
4241 POP_ASSUM MP_TAC THEN REWRITE_TAC[REAL_NOT_LE] THEN
4243 MAP_EVERY EXISTS_TAC [`v2:real^3`; `v1:real^3`; `v4:real^3`; `v3:real^3`] THEN
4244 ASM_REWRITE_TAC[DIST_SYM] THEN
4245 FIRST_X_ASSUM MATCH_MP_TAC THEN
4246 MAP_EVERY EXISTS_TAC [`p:real^3`; `t1':real`; `t2':real`; `t1:real`; `t2:real`] THEN
4247 ASM_SIMP_TAC[REAL_LT_IMP_LE];
4251 REPEAT REMOVE_ASSUM THEN
4254 (* First rotation *)
4255 MP_TAC (SPEC_ALL lemma_4_points_rotation2_full) THEN
4256 ASM_REWRITE_TAC[] THEN
4259 (* Second rotation *)
4260 MP_TAC (SPECL [`v1':real^3`; `v2:real^3`; `v3':real^3`; `v4:real^3`] lemma_4_points_rotation1_full) THEN
4261 ASM_REWRITE_TAC[] THEN
4262 MAP_EVERY (fun tm -> REPEAT (FIRST_X_ASSUM ((fun th -> ALL_TAC) o check (free_in tm o concl)))) [`v1:real^3`; `v3:real^3`; `v1':real^3`; `v3':real^3`] THEN
4265 MATCH_MP_TAC lemma_4_points_contradiction THEN
4266 MAP_EVERY EXISTS_TAC [`v1'':real^3`; `v2:real^3`; `v3'':real^3`; `v4:real^3`] THEN
4267 ASM_REWRITE_TAC[DIST_SYM]);;