2 (* ========================================================================= *)
3 (* FLYSPECK - BOOK FORMALIZATION *)
4 (* COMPLEMENT LEMMAS FOR EULER TRIANGLE LEMMA *)
6 (* LEMMA ABOUT RESCALING *)
8 (* Authour : VU KHAC KY *)
10 (* ========================================================================= *)
13 flyspeck_needs "trigonometry/delta_x.hl";;
15 (* ========================================================================= *)
16 (* SOME USEFUL TACTICS *)
17 (* ========================================================================= *)
18 module Euler_complement = struct
23 open Prove_by_refinement;;
26 let UP_ASM_TAC = FIRST_X_ASSUM MP_TAC;;
28 let DEL_TAC = FIRST_X_ASSUM MP_TAC THEN MATCH_MP_TAC (MESON[] `a ==> b ==> a`);;
31 FIRST_X_ASSUM MP_TAC THEN
32 FIRST_X_ASSUM MP_TAC THEN
33 MATCH_MP_TAC (MESON[] `(a ==> b ==> c) ==> (b ==> a ==> c)`) THEN
37 (* ========================================================================= *)
39 (* ========================================================================= *)
41 let euler_after_rescale_t =
44 ==> norm (v2 - v0) = &1
45 ==> norm (v3 - v0) = &1
48 (v2 - v0) dot (v3 - v0) +
49 (v3 - v0) dot (v1 - v0) +
50 (v1 - v0) dot (v2 - v0)) =
52 (v2 - v3) dot (v2 - v3) -
53 (v1 - v3) dot (v1 - v3) -
54 (v1 - v2) dot (v1 - v2)`;;
56 let LEMMA_FOR_EULER_AFTER_RESCALE = prove_by_refinement (euler_after_rescale_t,
58 [(REPEAT GEN_TAC THEN REPEAT DISCH_TAC);
59 (ABBREV_TAC `a = v1:real^3 - v0`);
60 (ABBREV_TAC `b = v2:real^3 - v0`);
61 (ABBREV_TAC `c = v3:real^3 - v0`);
63 (ONCE_REWRITE_TAC[VECTOR_ARITH `x:real^3 - y = (x - v0) - (y - v0)`]);
64 (PURE_ONCE_ASM_REWRITE_TAC[]);
65 (DEL_TAC THEN DEL_TAC THEN DEL_TAC);
66 (REWRITE_TAC[VECTOR_ARITH
67 `(x:real^3 - y) dot (x - y) = x dot x + y dot y - &2 * x dot y`]) ;
69 (PURE_ONCE_REWRITE_TAC[GSYM NORM_POW_2]);
70 (PURE_ONCE_ASM_REWRITE_TAC[]);
71 (PURE_ONCE_REWRITE_TAC[REAL_ARITH `&1 pow 2 = &1`]);
72 (PURE_REWRITE_TAC[DOT_SYM]);
75 (*========================================================================= *)
77 (* THE SECOND LEMMA : DIHV UNCHANGED *)
79 (* =========================================================================*)
81 let dihv_rescale_unchanged_t =
83 `!v0 v1 v2 v3 w0 w1:real^3 w2 w3 m n p.
84 v1 - v0 = m % (w1 - w0) /\
85 v2 - v0 = n % (w2 - w0) /\
86 v3 - v0 = p % (w3 - w0) /\
90 ==> dihV v0 v1 v2 v3 = dihV w0 w1 w2 w3`;;
92 let DIHV_RESCALE_UNCHANGED = prove_by_refinement (dihv_rescale_unchanged_t ,
94 [(REPEAT GEN_TAC THEN REPEAT STRIP_TAC);
95 (REWRITE_TAC[dihV] THEN REPEAT LET_TAC);
98 (REWRITE_TAC[VECTOR_SUB_RZERO]);
100 (* Begin subgoal 1 *)
102 (SUBGOAL_THEN `vap':real^3 = (m * m * n) % vap` ASSUME_TAC);
103 (EXPAND_TAC "vap'" THEN EXPAND_TAC "vap");
104 (PURE_ONCE_REWRITE_TAC[ASSUME `(vc':real^3) = m % vc`]);
105 (PURE_ONCE_REWRITE_TAC[ASSUME `(va':real^3) = n % va`]);
106 (PURE_REWRITE_TAC[DOT_LMUL;DOT_RMUL]);
107 (REWRITE_TAC[VECTOR_SUB_LDISTRIB;VECTOR_MUL_ASSOC]);
108 (REWRITE_TAC[REAL_ARITH `(a * b * c) * d = (a * b * d) * c`]);
110 (AP_THM_TAC THEN AP_TERM_TAC THEN AP_THM_TAC THEN AP_TERM_TAC);
114 (* Begin subgoal 2 *)
116 (SUBGOAL_THEN `vbp':real^3 = (m * m * p) % vbp` ASSUME_TAC);
117 (EXPAND_TAC "vbp'" THEN EXPAND_TAC "vbp");
118 (PURE_ONCE_REWRITE_TAC[ASSUME `(vc':real^3) = m % vc`]);
119 (PURE_ONCE_REWRITE_TAC[ASSUME `(vb':real^3) = p % vb`]);
120 (PURE_REWRITE_TAC[DOT_LMUL;DOT_RMUL]);
121 (REWRITE_TAC[VECTOR_SUB_LDISTRIB;VECTOR_MUL_ASSOC]);
122 (REWRITE_TAC[REAL_ARITH `(a * b * c) * d = (a * b * d) * c`]);
124 (AP_THM_TAC THEN AP_TERM_TAC THEN AP_THM_TAC THEN AP_TERM_TAC);
128 (PURE_ONCE_ASM_REWRITE_TAC[]);
129 (PURE_REWRITE_TAC[DOT_LMUL;DOT_RMUL]);
130 (PURE_REWRITE_TAC[NORM_MUL]);
131 (PURE_ONCE_REWRITE_TAC[REAL_ARITH `(a * b) * c * d = (a * c) * b * d`]);
132 (PURE_REWRITE_TAC[REAL_ABS_MUL]);
135 (SUBGOAL_THEN `&0 <= m /\ &0 <= n /\ &0 <= p` ASSUME_TAC);
138 (SUBGOAL_THEN `abs m = m /\ abs n = n /\ abs p = p` ASSUME_TAC);
139 (UP_ASM_TAC THEN MESON_TAC[GSYM REAL_ABS_REFL]);
141 (UP_ASM_TAC THEN STRIP_TAC);
142 (PURE_ONCE_ASM_REWRITE_TAC[]);
143 (PURE_ONCE_REWRITE_TAC[REAL_MUL_ASSOC]);
144 (PURE_ONCE_REWRITE_TAC[REAL_ARITH
145 `(m * m * m * p) * m * n = (m * m * n) * m * m * p`]);
146 (ABBREV_TAC `s = (m * m * n) * m * m * p`);
147 (PURE_ONCE_REWRITE_TAC[GSYM REAL_MUL_ASSOC]);
148 (PURE_REWRITE_TAC[real_div;REAL_INV_MUL]);
149 (PURE_ONCE_REWRITE_TAC[REAL_ARITH `(a * b * c) = (c * b) * a`]);
150 (REWRITE_TAC[REAL_ARITH `((a * b) * c) * d * e = (((c * d) * b) * a) * e`]);
151 (AP_THM_TAC THEN AP_TERM_TAC);
152 (AP_THM_TAC THEN AP_TERM_TAC);
154 (PURE_ONCE_REWRITE_TAC[GSYM REAL_MUL_LID]);
155 (ONCE_REWRITE_TAC[REAL_ARITH `&1 * x * y = x * y`]);
156 (AP_THM_TAC THEN AP_TERM_TAC);
157 (MATCH_MP_TAC REAL_MUL_LINV);
159 (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~(a = &0)`));
160 (ASM_MESON_TAC[REAL_LT_MUL])]);;
162 (*===========================================================================*)
163 (* THE THIRD LEMMA : *)
164 (* The lemmas help to compute p after rescaling *)
167 (*===========================================================================*)
169 let compute_euler_p_after_rescale_t =
170 `!v0:real^3 v1 v2 v3 v0' v1' v2' v3' m n p.
171 v1 - v0 = m % (v1' - v0') /\
172 v2 - v0 = n % (v2' - v0') /\
173 v3 - v0 = p % (v3' - v0') /\
177 ==> euler_p v0 v1 v2 v3 = (m * n * p) * euler_p v0' v1' v2' v3'`;;
180 let COMPUTE_EULER_P_AFTER_RESCALE =
181 prove_by_refinement (compute_euler_p_after_rescale_t,
183 [(REPEAT GEN_TAC THEN STRIP_TAC);
184 (REWRITE_TAC[euler_p]);
185 (PURE_ONCE_REWRITE_TAC[ylist]);
187 (REPLICATE_TAC 8 UP_ASM_TAC);
188 (PURE_REWRITE_TAC[PAIR_EQ]);
189 (PURE_ONCE_REWRITE_TAC[DIST_SYM]);
190 (PURE_REWRITE_TAC[dist]);
193 (EXPAND_TAC "y1'" THEN EXPAND_TAC "y2'" THEN EXPAND_TAC "y3'");
194 (EXPAND_TAC "y1" THEN EXPAND_TAC "y2" THEN EXPAND_TAC "y3");
195 (REPLICATE_TAC 3 UP_ASM_TAC);
196 (REPLICATE_TAC 6 DEL_TAC);
197 (REPLICATE_TAC 3 UP_ASM_TAC);
198 (REPLICATE_TAC 6 DEL_TAC);
201 (PURE_ONCE_ASM_REWRITE_TAC[]);
202 (REPLICATE_TAC 6 DEL_TAC);
203 (PURE_ONCE_ASM_REWRITE_TAC[]);
204 (PURE_ONCE_REWRITE_TAC[NORM_MUL]);
207 (SUBGOAL_THEN `&0 <= m /\ &0 <= n /\ &0 <= p` ASSUME_TAC);
208 (ASM_MESON_TAC[REAL_ARITH `&0 < a ==> &0 <= a`]);
209 (SUBGOAL_THEN `abs m = m /\ abs n = n /\ abs p = p` ASSUME_TAC);
210 (UP_ASM_TAC THEN MESON_TAC[REAL_ABS_REFL]);
212 (PURE_ONCE_ASM_REWRITE_TAC[]);
213 (PURE_REWRITE_TAC[DOT_RMUL;DOT_LMUL]);
216 (* ========================================================================= *)
218 (* This lemma is for computing delta_x *)
220 (* ========================================================================= *)
222 let VECTOR_EQ_COMPONENT = prove
223 (`!x:real^N y i. x = y ==> x$i = y$i`,
225 SUBGOAL_THEN `?k. 1 <= k /\ k <= dimindex(:N) /\ !z:real^N. z$i = z$k`
227 [REWRITE_TAC[FINITE_INDEX_INRANGE];
228 ASM_SIMP_TAC[vector_sub; CART_EQ; LAMBDA_BETA]]);;
230 let compute_delta_x_after_rescale_t =
231 `!v0 v1 v2 v3 v0' v1' v2' v3' m n p x1 x2 x3 x4 x5 x6 x1' x2' x3' x4' x5' x6'.
232 v1:real^3 - v0 = m % (v1' - v0') /\
233 v2 - v0 = n % (v2' - v0') /\
234 v3 - v0 = p % (v3' - v0') /\
238 x1',x2',x3',x4',x5',x6' = xlist v0' v1' v2' v3' /\
239 x1,x2,x3,x4,x5,x6 = xlist v0 v1 v2 v3 /\
240 &0 <= delta_x x1' x2' x3' x4' x5' x6'
241 ==> delta_x x1 x2 x3 x4 x5 x6 =
242 (m * n * p) * (m * n * p) * delta_x x1' x2' x3' x4' x5' x6'`;;
245 let COMPUTE_DELTA_X_AFTER_RESCALE =
247 prove_by_refinement (compute_delta_x_after_rescale_t ,
249 [(REPEAT GEN_TAC THEN REPEAT STRIP_TAC);
251 (SUBGOAL_THEN `delta_x x1 x2 x3 x4 x5 x6 =
252 (let a = v1:real^3 - v0 in
255 &4 * (a$1 * b$2 * c$3 - a$1 * b$3 * c$2 - a$2 * b$1 * c$3 +
256 a$2 * b$3 * c$1 + a$3 * b$1 * c$2 - a$3 * b$2 * c$1) pow 2)`
258 (ASM_MESON_TAC[COMPUTE_DELTA_X]);
260 (SUBGOAL_THEN `delta_x x1' x2' x3' x4' x5' x6' =
261 (let a' = v1':real^3 - v0' in
262 let b' = v2' - v0' in
263 let c' = v3' - v0' in
264 &4 * (a'$1 * b'$2 * c'$3 - a'$1 * b'$3 * c'$2 - a'$2 * b'$1 * c'$3 +
265 a'$2 * b'$3 * c'$1 + a'$3 * b'$1 * c'$2 - a'$3 * b'$2 * c'$1) pow 2)`
267 (ASM_MESON_TAC[COMPUTE_DELTA_X]);
272 (SUBGOAL_THEN `(a:real^3)$1 = m * (a':real^3)$1 /\
273 (b:real^3)$1 = n * (b':real^3)$1 /\
274 (c:real^3)$1 = p * (c':real^3)$1 /\
280 c$3 = p * c'$3` ASSUME_TAC);
282 (ASM_MESON_TAC[VECTOR_EQ_COMPONENT;VECTOR_MUL_COMPONENT]);
283 (ONCE_ASM_REWRITE_TAC[]);
284 (REWRITE_TAC[POW_2]);
287 (* =========================================================================*)
288 (* THE 5-TH LEMMA : *)
289 (* Similar lemma for computing Sqrt(delta_x) *)
290 (*==========================================================================*)
292 let sqrt_delta_x_after_rescale =
293 `!v0 v1 v2 v3 v0' v1' v2' v3' m n p x1 x2 x3 x4 x5 x6 x1' x2' x3' x4' x5' x6'.
294 v1:real^3 - v0 = m % (v1' - v0') /\
295 v2 - v0 = n % (v2' - v0') /\
296 v3 - v0 = p % (v3' - v0') /\
300 x1',x2',x3',x4',x5',x6' = xlist v0' v1' v2' v3' /\
301 x1,x2,x3,x4,x5,x6 = xlist v0 v1 v2 v3 /\
302 &0 <= delta_x x1' x2' x3' x4' x5' x6'
303 ==> sqrt (delta_x x1 x2 x3 x4 x5 x6) =
304 (m * n * p) * sqrt (delta_x x1' x2' x3' x4' x5' x6')`;;
306 let SQRT_DELTA_X_AFTER_RESCALE =
307 prove_by_refinement (sqrt_delta_x_after_rescale,
309 [(REPEAT GEN_TAC THEN REPEAT STRIP_TAC);
312 `delta_x x1 x2 x3 x4 x5 x6 =
313 (m * n * p) * (m * n * p) * delta_x x1' x2' x3' x4' x5' x6'`
315 (ASM_MESON_TAC[COMPUTE_DELTA_X_AFTER_RESCALE]);
317 (PURE_ONCE_ASM_REWRITE_TAC[]);
318 (ABBREV_TAC `S = m * n * p`);
319 (PURE_REWRITE_TAC[REAL_MUL_ASSOC]);
322 `sqrt ((S * S) * delta_x x1' x2' x3' x4' x5' x6') =
323 sqrt (S * S) * sqrt (delta_x x1' x2' x3' x4' x5' x6')`
325 (MATCH_MP_TAC SQRT_MUL);
327 (ASM_MESON_TAC[REAL_LE_MUL]);
329 (PURE_ONCE_ASM_REWRITE_TAC[]);
330 (AP_THM_TAC THEN AP_TERM_TAC);
332 (SUBGOAL_THEN `sqrt (S * S) = sqrt S pow 2` ASSUME_TAC);
333 (REWRITE_TAC[REAL_POW_2]);
334 (MATCH_MP_TAC SQRT_MUL);
336 (ASM_MESON_TAC[REAL_LE_MUL]);
338 (PURE_ONCE_ASM_REWRITE_TAC[]);
339 (MATCH_MP_TAC SQRT_POW_2);
341 (ASM_MESON_TAC[REAL_LE_MUL])]);;
344 (* ===========================================================================*)
345 (* THE SIXTH LEMMA : *)
347 (* This following sub-lemma is necessary for proving the 6-th Lemma *)
349 (* ===========================================================================*)
351 let SQRT_OF_POW_2_LE = prove_by_refinement (
352 `!x. (&0 <= x) ==> sqrt (x pow 2) = x`,
354 [(GEN_TAC THEN DISCH_TAC);
355 (REWRITE_TAC[REAL_POW_2]);
356 (SUBGOAL_THEN `sqrt (x * x) = (sqrt x) pow 2` ASSUME_TAC); (PURE_REWRITE_TAC[REAL_POW_2]);
357 (MATCH_MP_TAC SQRT_MUL);
359 (PURE_ASM_REWRITE_TAC[]);
360 (ASM_MESON_TAC[SQRT_POW_2])]);;
362 (* ===========================================================================*)
363 (* THE SIXTH LEMMA : *)
364 (* This lemma says that if the Euler formulation holds *)
365 (* for the case where x1 = x2 = x3 = 1 then it holds for all cases *)
367 (* ===========================================================================*)
369 let EULER_FORMULA_RESCALE = prove_by_refinement (
370 `(!v0 v1:real^3 v2 v3 p x1 x2 x3 x4 x5 x6 alpha1 alpha2 alpha3 d w1 w2 w3.
371 p = euler_p v0 v1 v2 v3 /\
372 x1,x2,x3,x4,x5,x6 = xlist v0 v1 v2 v3 /\
373 alpha1 = dihV v0 v1 v2 v3 /\
374 alpha2 = dihV v0 v2 v3 v1 /\
375 alpha3 = dihV v0 v3 v1 v2 /\
376 d = delta_x x1 x2 x3 x4 x5 x6 /\
384 ==> alpha1 + alpha2 + alpha3 - pi = pi - &2 * atn2 (sqrt d,&2 * p))
385 ==> (!v0 v1:real^3 v2 v3.
386 let p = euler_p v0 v1 v2 v3 in
387 let x1,x2,x3,x4,x5,x6 = xlist v0 v1 v2 v3 in
388 let alpha1 = dihV v0 v1 v2 v3 in
389 let alpha2 = dihV v0 v2 v3 v1 in
390 let alpha3 = dihV v0 v3 v1 v2 in
391 let d = delta_x x1 x2 x3 x4 x5 x6 in
393 ==> alpha1 + alpha2 + alpha3 - pi = pi - &2 * atn2 (sqrt d,&2 * p))`,
395 (* -------------------------------------------------------------------------*)
396 (* Rescale by considering new points v1',v2',v3' *)
397 (* -------------------------------------------------------------------------*)
399 [(DISCH_TAC THEN REPEAT GEN_TAC THEN REPEAT LET_TAC THEN DISCH_TAC);
401 (ABBREV_TAC `v1' = v0 + inv (norm(v1:real^3 - v0)) % (v1 - v0)`);
402 (ABBREV_TAC `v2' = v0 + inv (norm(v2:real^3 - v0)) % (v2 - v0)`);
403 (ABBREV_TAC `v3' = v0 + inv (norm(v3:real^3 - v0)) % (v3 - v0)`);
404 (ABBREV_TAC `w1' = (v1':real^3) - v0`);
405 (ABBREV_TAC `w2' = (v2':real^3) - v0`);
406 (ABBREV_TAC `w3' = (v3':real^3)- v0`);
408 (* -------------------------------------------------------------------------*)
409 (* Subgoal 1: &0 < norm (v1 - v0) *)
410 (* &0 < norm (v2 - v0) *)
411 (* &0 < norm (v3 - v0) *)
412 (* -------------------------------------------------------------------------*)
415 `&0 < norm (v1:real^3 - v0) /\
416 &0 < norm (v2:real^3 - v0) /\
417 &0 < norm (v3:real^3 - v0)`
420 (PURE_ONCE_REWRITE_TAC[NORM_POS_LT]);
421 (PURE_REWRITE_TAC[VECTOR_ARITH `(a - b = vec 0) <=> (a = b)`;
422 MESON[] `(a <=> b) <=> ~ a <=> ~ b`]);
423 (REPEAT CONJ_TAC); (* Break into 3 subgoal *)
426 (SUBGOAL_THEN `collinear {v0:real^3 , v1, v2}` ASSUME_TAC);
427 (PURE_ONCE_ASM_REWRITE_TAC[]);
428 (PURE_REWRITE_TAC[collinear; SET_RULE `{a, a, b} = {a , b}`]);
429 (EXISTS_TAC `v2:real^3 - v0`);
431 (REWRITE_TAC[SET_RULE ` x IN {a, b} <=> (x = a \/ x = b)`]);
432 STRIP_TAC; (* Break into 4 subgoals *)
434 (PURE_ONCE_ASM_REWRITE_TAC[]);
435 (EXISTS_TAC `&0` THEN VECTOR_ARITH_TAC);
436 (PURE_ONCE_ASM_REWRITE_TAC[]);
437 (EXISTS_TAC `-- &1` THEN VECTOR_ARITH_TAC);
438 (PURE_ONCE_ASM_REWRITE_TAC[]);
439 (EXISTS_TAC `&1` THEN VECTOR_ARITH_TAC);
440 (PURE_ONCE_ASM_REWRITE_TAC[]);
441 (EXISTS_TAC `&0` THEN VECTOR_ARITH_TAC);
442 (ASM_MESON_TAC[DELTA_X_LT_0_COLLINEAR]);
445 (SUBGOAL_THEN `collinear {v0:real^3 , v1, v2}` ASSUME_TAC);
446 (PURE_ONCE_ASM_REWRITE_TAC[]);
447 (PURE_REWRITE_TAC[collinear; SET_RULE `{a, b, a} = {a , b}`]);
448 (EXISTS_TAC `v1:real^3 - v0`);
450 (REWRITE_TAC[SET_RULE ` x IN {a, b} <=> (x = a \/ x = b)`]);
451 STRIP_TAC; (* Break into 4 subgoals *)
453 (PURE_ONCE_ASM_REWRITE_TAC[]);
454 (EXISTS_TAC `&0` THEN VECTOR_ARITH_TAC);
455 (PURE_ONCE_ASM_REWRITE_TAC[]);
456 (EXISTS_TAC `-- &1` THEN VECTOR_ARITH_TAC);
457 (PURE_ONCE_ASM_REWRITE_TAC[]);
458 (EXISTS_TAC `&1` THEN VECTOR_ARITH_TAC);
459 (PURE_ONCE_ASM_REWRITE_TAC[]);
460 (EXISTS_TAC `&0` THEN VECTOR_ARITH_TAC);
461 (ASM_MESON_TAC[DELTA_X_LT_0_COLLINEAR]);
464 (SUBGOAL_THEN `collinear {v0:real^3 , v1, v3}` ASSUME_TAC);
465 (PURE_ONCE_ASM_REWRITE_TAC[]);
466 (PURE_REWRITE_TAC[collinear; SET_RULE `{a, b, a} = {a , b}`]);
467 (EXISTS_TAC `v1:real^3 - v0`);
469 (REWRITE_TAC[SET_RULE ` x IN {a, b} <=> (x = a \/ x = b)`]);
470 STRIP_TAC; (* Break into 4 subgoals *)
472 (PURE_ONCE_ASM_REWRITE_TAC[]);
473 (EXISTS_TAC `&0` THEN VECTOR_ARITH_TAC);
474 (PURE_ONCE_ASM_REWRITE_TAC[]);
475 (EXISTS_TAC `-- &1` THEN VECTOR_ARITH_TAC);
476 (PURE_ONCE_ASM_REWRITE_TAC[]);
477 (EXISTS_TAC `&1` THEN VECTOR_ARITH_TAC);
478 (PURE_ONCE_ASM_REWRITE_TAC[]);
479 (EXISTS_TAC `&0` THEN VECTOR_ARITH_TAC);
480 (ASM_MESON_TAC[DELTA_X_LT_0_COLLINEAR]);
483 (* -------------------------------------------------------------------------*)
484 (* Subgoal 2: w1', w2', w3' havnorms equal 1 *)
485 (* -------------------------------------------------------------------------*)
488 `norm (w1':real^3) = &1 /\
489 norm (w2':real^3) = &1 /\
490 norm (w3':real^3) = &1`
493 (EXPAND_TAC "w1'" THEN EXPAND_TAC "w2'" THEN EXPAND_TAC "w3'");
494 (UP_ASM_TAC THEN REPLICATE_TAC 3 DEL_TAC THEN DISCH_TAC);
495 (EXPAND_TAC "v1'" THEN EXPAND_TAC "v2'" THEN EXPAND_TAC "v3'");
496 (ONCE_REWRITE_TAC[VECTOR_ARITH `((a:real^3) + b) - a = b`]);
497 (REWRITE_TAC[NORM_MUL;REAL_ABS_INV]);
500 `abs (norm (v1 - v0)) = norm (v1:real^3 - v0) /\
501 abs (norm (v2 - v0)) = norm (v2:real^3 - v0) /\
502 abs (norm (v3 - v0)) = norm (v3:real^3 - v0)`
504 (SIMP_TAC[NORM_POS_LE;REAL_ABS_REFL]);
506 (ONCE_ASM_REWRITE_TAC[]);
507 (ASM_SIMP_TAC[REAL_ARITH `&0 < a ==> ~(a = &0)`;REAL_MUL_LINV]);
509 (* ------------------------------------------------------------------------- *)
511 (* alpha1, alpha2, alpha3 arunchanged *)
512 (* ------------------------------------------------------------------------- *)
514 (ABBREV_TAC `alpha1' = dihV (v0:real^3) v1' v2' v3'`);
515 (ABBREV_TAC `alpha2' = dihV (v0:real^3) v2' v3' v1'`);
516 (ABBREV_TAC `alpha3' = dihV (v0:real^3) v3' v1' v2'`);
519 `alpha1:real = alpha1' /\ alpha2:real = alpha2' /\ alpha3:real = alpha3'`
521 (EXPAND_TAC "alpha1" THEN EXPAND_TAC "alpha2" THEN EXPAND_TAC "alpha3");
522 (EXPAND_TAC "alpha1'" THEN EXPAND_TAC "alpha2'" THEN EXPAND_TAC "alpha3'");
523 (ABBREV_TAC `m = inv (norm (v1:real^3 - v0))`);
524 (ABBREV_TAC `n = inv (norm (v2:real^3 - v0))`);
525 (ABBREV_TAC `q = inv (norm (v3:real^3 - v0))`);
528 ` v1' - v0 = m % (v1:real^3 - v0) /\
529 v2' - v0 = n % (v2:real^3 - v0) /\
530 v3' - v0 = q % (v3:real^3 - v0)`
532 (EXPAND_TAC "v1'" THEN EXPAND_TAC "v2'" THEN EXPAND_TAC "v3'");
535 (SUBGOAL_THEN `&0 < m /\ &0 < n /\ &0 < q ` ASSUME_TAC);
536 (EXPAND_TAC "m" THEN EXPAND_TAC "n" THEN EXPAND_TAC "q");
537 (REPLICATE_TAC 8 DEL_TAC THEN UP_ASM_TAC THEN STRIP_TAC);
538 (ASM_MESON_TAC[REAL_LT_INV]);
540 (ASM_MESON_TAC[DIHV_RESCALE_UNCHANGED]);
543 (* ========================================================================== *)
545 (* (x1',x2',x3,'x4',x5',x6') = xlist (v0:real^3) v1' v2' v3' *)
546 (* ========================================================================== *)
548 (ABBREV_TAC `p' = euler_p (v0:real^3) v1' v2' v3'`);
549 (ABBREV_TAC `x1' = dist (v0:real^3,v1') pow 2`);
550 (ABBREV_TAC `x2' = dist (v0:real^3,v2') pow 2`);
551 (ABBREV_TAC `x3' = dist (v0:real^3,v3') pow 2`);
552 (ABBREV_TAC `x4' = dist (v2':real^3,v3') pow 2`);
553 (ABBREV_TAC `x5' = dist (v1':real^3,v3') pow 2`);
554 (ABBREV_TAC `x6' = dist (v1':real^3,v2') pow 2`);
555 (ABBREV_TAC `d' = delta_x (x1':real) x2' x3' x4' x5' x6' `);
558 `x1':real,x2',x3',x4',x5',x6' =
559 xlist (v0:real^3) v1' v2' v3'`
562 (REWRITE_TAC[xlist;ylist]);
564 (UP_ASM_TAC THEN PURE_REWRITE_TAC[PAIR_EQ] THEN STRIP_TAC);
565 (ASM_MESON_TAC[PAIR_EQ]);
567 (* --------------------------------------------------------------------------*)
569 (* p' = k * p with somk *)
570 (*---------------------------------------------------------------------------*)
572 (ABBREV_TAC `t1 = inv (norm ((v1:real^3) - v0)) `);
573 (ABBREV_TAC `t2 = inv (norm ((v2:real^3) - v0)) `);
574 (ABBREV_TAC `t3 = inv (norm ((v3:real^3) - v0)) `);
576 (SUBGOAL_THEN `p' = (t1 * t2 * t3) * p` ASSUME_TAC);
577 (EXPAND_TAC "p" THEN EXPAND_TAC "p'");
578 (MATCH_MP_TAC COMPUTE_EULER_P_AFTER_RESCALE);
579 (EXPAND_TAC "v1'" THEN EXPAND_TAC "v2'" THEN EXPAND_TAC "v3'");
580 (REWRITE_TAC[VECTOR_ARITH `((a:real^3) + b) - a = b`]);
581 (EXPAND_TAC "t1" THEN EXPAND_TAC "t2" THEN EXPAND_TAC "t3");
582 (ASM_MESON_TAC[REAL_LT_INV]);
584 (* --------------------------------------------------------------------------*)
586 (* d' = k * d with somk *)
587 (*---------------------------------------------------------------------------*)
589 (SUBGOAL_THEN `d' = (t1 * t2 * t3) * (t1 * t2 * t3) * d` ASSUME_TAC);
590 (EXPAND_TAC "d" THEN EXPAND_TAC "d'");
591 (MATCH_MP_TAC COMPUTE_DELTA_X_AFTER_RESCALE);
592 (EXISTS_TAC `v0:real^3`);
593 (EXISTS_TAC `v1':real^3`);
594 (EXISTS_TAC `v2':real^3`);
595 (EXISTS_TAC `v3':real^3`);
596 (EXISTS_TAC `v0:real^3`);
597 (EXISTS_TAC `v1:real^3`);
598 (EXISTS_TAC `v2:real^3`);
599 (EXISTS_TAC `v3:real^3`);
600 (EXPAND_TAC "v1'" THEN EXPAND_TAC "v2'" THEN EXPAND_TAC "v3'");
601 (REWRITE_TAC[VECTOR_ARITH `((a:real^3) + b) - a = b`]);
604 (SUBGOAL_THEN `&0 < t1 /\ &0 < t2 /\ &0 < t3 /\ &0 < d` ASSUME_TAC);
605 (EXPAND_TAC "t1" THEN EXPAND_TAC "t2" THEN EXPAND_TAC "t3");
606 (REPLICATE_TAC 18 DEL_TAC);
607 (UP_ASM_TAC THEN REPLICATE_TAC 6 DEL_TAC THEN UP_ASM_TAC);
608 (MESON_TAC[REAL_LT_INV]);
610 (UP_ASM_TAC THEN MESON_TAC[REAL_ARITH `&0 < a ==> &0 <= a`]);
613 (* -------------------------------------------------------------------------- *)
615 (* This part is thproof of d' > 0 *)
616 (* -------------------------------------------------------------------------- *)
619 (SUBGOAL_THEN `&0 < d'` ASSUME_TAC);
620 (PURE_ONCE_ASM_REWRITE_TAC[]);
622 (SUBGOAL_THEN `&0 < t1 /\ &0 < t2 /\ &0 < t3 /\ &0 < d` ASSUME_TAC);
623 (EXPAND_TAC "t1" THEN EXPAND_TAC "t2" THEN EXPAND_TAC "t3");
624 (REPLICATE_TAC 19 DEL_TAC);
625 (UP_ASM_TAC THEN REPLICATE_TAC 6 DEL_TAC THEN UP_ASM_TAC);
626 (MESON_TAC[REAL_LT_INV]);
628 (UP_ASM_TAC THEN MESON_TAC[REAL_LT_MUL]);
630 (*---------------------------------------------------------------------------*)
632 (* atn2 (sqrt d,&2 * p) is unchanged *)
633 (*---------------------------------------------------------------------------*)
635 (SUBGOAL_THEN `&2 * atn2 (sqrt (d':real), &2 * (p':real)) =
636 &2 * atn2 (sqrt (d:real), &2 * (p:real))` ASSUME_TAC);
640 (SUBGOAL_THEN `&0 < sqrt d /\ &0 < sqrt d'` ASSUME_TAC);
641 (MESON_TAC[ASSUME `&0 < d`; ASSUME `&0 < d'`; SQRT_POS_LT]);
643 (SUBGOAL_THEN `atn2 (sqrt d,&2 * p) = atn ((&2 * p) / sqrt d)`
645 (FIRST_ASSUM MP_TAC THEN MESON_TAC[ATN2_BREAKDOWN]);
648 (SUBGOAL_THEN `atn2 (sqrt d',&2 * p') = atn ((&2 * p') / sqrt d')`
650 (MESON_TAC[ASSUME `&0 < sqrt d /\ &0 < sqrt d'`; ATN2_BREAKDOWN]);
652 (ONCE_ASM_REWRITE_TAC[]);
654 (DEL_TAC THEN DEL_TAC THEN UP_ASM_TAC THEN STRIP_TAC);
657 (SUBGOAL_THEN `((&2 * p') / sqrt d' = (&2 * p) / sqrt d) <=>
658 &2 * p' = ((&2 * p) / sqrt d) * sqrt d'`
660 (UP_ASM_TAC THEN MESON_TAC[REAL_EQ_LDIV_EQ]);
662 (ONCE_ASM_REWRITE_TAC[]);
663 (REWRITE_TAC[REAL_ARITH `((x * y) / b) * c = x * (c * y) / b`]);
666 (PURE_ASM_REWRITE_TAC[REAL_EQ_LDIV_EQ]);
667 (PURE_ONCE_REWRITE_TAC[REAL_ARITH `(x * y) / b = (x / b) * y`]);
668 (AP_THM_TAC THEN AP_TERM_TAC);
669 (ABBREV_TAC `S = t1 * t2 * t3`);
670 (REWRITE_TAC[REAL_MUL_ASSOC;GSYM REAL_POW_2]);
673 (SUBGOAL_THEN `sqrt (S pow 2 * d) = sqrt (S pow 2) * sqrt d` ASSUME_TAC);
674 (MATCH_MP_TAC SQRT_MUL);
675 (ASM_SIMP_TAC[REAL_ARITH `&0 < a ==> &0 <= a`]);
676 (MESON_TAC[REAL_LE_POW_2]);
678 (ONCE_ASM_REWRITE_TAC[]);
679 (ONCE_REWRITE_TAC[REAL_ARITH `(a * b) / c = a * (b / c)`]);
682 (SUBGOAL_THEN `sqrt d / sqrt d = &1` ASSUME_TAC);
683 (MATCH_MP_TAC REAL_DIV_REFL);
684 (ASM_SIMP_TAC[REAL_ARITH `&0 < a ==> ~ (a = &0)`]);
686 (ONCE_ASM_REWRITE_TAC[]);
687 (REWRITE_TAC[REAL_MUL_RID]);
688 (MATCH_MP_TAC (GSYM SQRT_OF_POW_2_LE));
689 (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> &0 <= a`));
693 (SUBGOAL_THEN `&0 < t1 /\ &0 < t2 /\ &0 < t3 /\ &0 < d` ASSUME_TAC);
694 (EXPAND_TAC "t1" THEN EXPAND_TAC "t2" THEN EXPAND_TAC "t3");
695 (REPLICATE_TAC 19 DEL_TAC);
696 (ASM_MESON_TAC[REAL_LT_INV]);
697 (UP_ASM_TAC THEN MESON_TAC[REAL_LT_MUL]);
699 (*---------------------------------------------------------------------------*)
701 (* Finish the lemma about rescaling *)
702 (*---------------------------------------------------------------------------*)
705 `alpha1' + alpha2' + alpha3' - pi = pi - &2 * atn2 (sqrt d',&2 * p')`
709 (ASM_MESON_TAC[])]);;
711 (* ==========================================================================*)
713 (* ~ collinear {a, b, c} ==> norm(a - b) > &0 *)
714 (* ==========================================================================*)
716 let COLLINEAR_NORM_LT_0 = prove_by_refinement (
717 `!(a:real^3) b c. ~collinear {a, b, c} ==> &0 < norm (a - b)`,
719 [(REPEAT GEN_TAC THEN REPEAT STRIP_TAC);
720 (REWRITE_TAC[NORM_POS_LT]);
722 (UP_ASM_TAC THEN PURE_ONCE_REWRITE_TAC[
723 VECTOR_ARITH `(a:real^3) - b = vec 0 <=> b - a = vec 0`]);
726 (SUBGOAL_THEN `collinear {(a:real^3), b, c}` ASSUME_TAC);
727 (MATCH_MP_TAC (GEN_ALL ALLEMI_COLLINEAR));
729 (MESON_TAC [VECTOR_ARITH `a dot vec 0 = &0`;
730 VECTOR_ARITH `a % vec 0 = vec 0`;
731 VECTOR_ARITH `(&0) % c = vec 0`]);
732 (ASM_MESON_TAC[])]);;
734 (* ========================================================================= *)
736 (* ========================================================================= *)
738 let REAL_LT_RSQRT2 = prove
739 (`!x y. x pow 2 < y ==> -- sqrt y < x`,
740 REPEAT STRIP_TAC THEN
741 MATCH_MP_TAC(REAL_ARITH `abs x < a ==> -- a < x`) THEN
742 REWRITE_TAC[GSYM POW_2_SQRT_ABS] THEN
743 MATCH_MP_TAC SQRT_MONO_LT THEN
744 ASM_REWRITE_TAC[REAL_POW_2; REAL_LE_SQUARE]);;
746 let EULER_TRIANGLE_REAL_INTERVAL = prove_by_refinement (
748 s = {x | &0 < ups_x x b c - x * b * c} /\ &0 < ups_x a b c - a * b * c
749 ==> is_realinterval s`,
751 [(REPEAT GEN_TAC THEN STRIP_TAC);
752 (ABBREV_TAC `d = b * c * b * c / &4 - b * c * (b + c) + &4 * b * c `);
753 (ABBREV_TAC `f = (\a. a - b - c + b * c / &2)`);
755 (* ------------------------------------------------------------------------- *)
757 (* ------------------------------------------------------------------------- *)
760 (SUBGOAL_THEN `&0 < d` ASSUME_TAC);
761 (EXPAND_TAC "d" THEN DEL_TAC THEN DEL_TAC);
762 (UP_ASM_TAC THEN REWRITE_TAC[ups_x] THEN DISCH_TAC);
763 (MATCH_MP_TAC (REAL_ARITH
764 `&0 <= (a - b - c + b * c / &2) pow 2 /\
765 &0 < S - (a - b - c + b * c / &2) pow 2 ==> &0 < S`));
766 (REWRITE_TAC[REAL_LE_POW_2]);
769 (* ------------------------------------------------------------------------- *)
771 (* ------------------------------------------------------------------------- *)
774 `!(z:real). z IN s <=> f z < sqrt d /\ --sqrt d < f z`
777 (ONCE_ASM_REWRITE_TAC[] THEN ONCE_ASM_REWRITE_TAC[IN_ELIM_THM]);
778 (EQ_TAC); (* Break into 2 subgoal 2.1 and 2.2 *)
780 (REWRITE_TAC[ups_x] THEN DISCH_TAC);
781 (SUBGOAL_THEN `(f (z:real)) pow 2 < d /\ (f z) pow 2 < d` ASSUME_TAC);
782 (EXPAND_TAC "d" THEN EXPAND_TAC "f");
783 (PURE_REWRITE_TAC[REAL_POW_2]);
784 (ASM_REAL_ARITH_TAC);
785 (ASM_MESON_TAC[REAL_LT_RSQRT;REAL_LT_RSQRT2]);
787 (REWRITE_TAC[ups_x] THEN EXPAND_TAC "f");
789 (REWRITE_TAC[REAL_ARITH
790 `(--z * z - b * b - c * c + &2 * z * c + &2 * z * b + &2 * b * c) -
792 (b * c * b * c / &4 - b * c * (b + c) + &4 * b * c) -
793 (z - b - c + b * c / &2) pow 2`]);
794 (REWRITE_TAC[REAL_ARITH `&0 < a - b <=> b < a`]);
795 (PURE_ONCE_ASM_REWRITE_TAC[]);
796 (REPLICATE_TAC 2 UP_ASM_TAC THEN PURE_REWRITE_TAC[MESON[REAL_BOUNDS_LT]
797 `(a < x ==> -- x < a ==> y) <=> abs a < x ==> y` ]);
800 (SUBGOAL_THEN `d = sqrt d pow 2` ASSUME_TAC);
801 (ASM_MESON_TAC[REAL_ARITH `&0 < a ==> &0 <= a`; SQRT_POW_2]);
802 (PURE_ONCE_ASM_REWRITE_TAC[]);
803 (ASM_REWRITE_TAC[GSYM REAL_LT_SQUARE_ABS]);
804 (MATCH_MP_TAC (REAL_ARITH `x = sqrt d /\ y < sqrt d ==> y < x`));
806 (PURE_REWRITE_TAC[REAL_ABS_REFL]);
807 (MATCH_MP_TAC (REAL_ARITH `&0 < x ==> &0 <= x`));
808 (ASM_MESON_TAC[SQRT_POS_LT]);
810 (* ------------------------------------------------------------------------- *)
812 (* ------------------------------------------------------------------------- *)
814 (REWRITE_TAC[is_realinterval]);
815 (REPEAT GEN_TAC THEN STRIP_TAC);
816 (ONCE_ASM_REWRITE_TAC[]);
819 (SUBGOAL_THEN `f (c':real) <= f b'` ASSUME_TAC);
820 (EXPAND_TAC "f" THEN ASM_REAL_ARITH_TAC);
821 (SUBGOAL_THEN `f (b':real) < sqrt d` ASSUME_TAC);
822 (EXPAND_TAC "f" THEN ASM_MESON_TAC[]);
823 (ASM_REAL_ARITH_TAC);
825 (SUBGOAL_THEN `f (a':real) <= f c'` ASSUME_TAC);
826 (EXPAND_TAC "f" THEN ASM_REAL_ARITH_TAC);
827 (SUBGOAL_THEN `-- sqrt d < f (a':real)` ASSUME_TAC);
828 (EXPAND_TAC "f" THEN ASM_MESON_TAC[]);
829 (ASM_REAL_ARITH_TAC)]);;
831 (* ==========================================================================*)
834 (* ==========================================================================*)
837 prove (`!v0:real^3 v1 v2 v3.
838 let ga = dihV v0 v1 v2 v3 in
839 let v01 = dist (v0,v1) pow 2 in
840 let v02 = dist (v0,v2) pow 2 in
841 let v03 = dist (v0,v3) pow 2 in
842 let v12 = dist (v1,v2) pow 2 in
843 let v13 = dist (v1,v3) pow 2 in
844 let v23 = dist (v2,v3) pow 2 in
845 ~collinear {v0, v1, v2} /\ ~collinear {v0, v1, v3}
849 (sqrt (&4 * v01 * delta_x v01 v02 v03 v23 v13 v12),
850 delta_x4 v01 v02 v03 v23 v13 v12)`,
851 MP_TAC OJEKOJF THEN REPEAT LET_TAC THEN MESON_TAC[]);;
853 let COMPUTE_DIHV_ATN2 = prove
854 (`!(v0:real^3) v1 v2 v3 gamma x1 x2 x3 x4 x5 x6.
855 gamma = dihV v0 v1 v2 v3 /\
856 x1 = dist (v0,v1) pow 2 /\
857 x2 = dist (v0,v2) pow 2 /\
858 x3 = dist (v0,v3) pow 2 /\
859 x6 = dist (v1,v2) pow 2 /\
860 x5 = dist (v1,v3) pow 2 /\
861 x4 = dist (v2,v3) pow 2 /\
862 ~collinear {v0, v1, v2} /\
863 ~collinear {v0, v1, v3}
864 ==> gamma = pi / &2 - atn2( sqrt ( &4 * x1 * delta_x x1 x2 x3 x4 x5 x6),
865 delta_x4 x1 x2 x3 x4 x5 x6)`,
866 REPEAT STRIP_TAC THEN MP_TAC OJEKOJF2 THEN REPEAT LET_TAC THEN
867 ASM_REWRITE_TAC[] THEN EXPAND_TAC "ga" THEN
868 EXPAND_TAC "v01" THEN EXPAND_TAC "v02" THEN EXPAND_TAC "v03" THEN
869 EXPAND_TAC "v13" THEN EXPAND_TAC "v23" THEN EXPAND_TAC "v12" THEN
870 DISCH_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]);;