1 (* ========================================================================= *)
2 (* Some geometric notions in real^N. *)
3 (* ========================================================================= *)
5 needs "Multivariate/realanalysis.ml";;
9 (* ------------------------------------------------------------------------- *)
10 (* Pythagoras's theorem is almost immediate. *)
11 (* ------------------------------------------------------------------------- *)
13 let PYTHAGORAS = prove
15 orthogonal (A - B) (C - B)
16 ==> norm(C - A) pow 2 = norm(B - A) pow 2 + norm(C - B) pow 2`,
17 REWRITE_TAC[NORM_POW_2; orthogonal; DOT_LSUB; DOT_RSUB; DOT_SYM] THEN
20 (* ------------------------------------------------------------------------- *)
21 (* Angle between vectors (always 0 <= angle <= pi). *)
22 (* ------------------------------------------------------------------------- *)
24 let vector_angle = new_definition
25 `vector_angle x y = if x = vec 0 \/ y = vec 0 then pi / &2
26 else acs((x dot y) / (norm x * norm y))`;;
28 let VECTOR_ANGLE_LINEAR_IMAGE_EQ = prove
29 (`!f x y. linear f /\ (!x. norm(f x) = norm x)
30 ==> (vector_angle (f x) (f y) = vector_angle x y)`,
31 REPEAT STRIP_TAC THEN ASM_SIMP_TAC[vector_angle; GSYM NORM_EQ_0] THEN
32 ASM_MESON_TAC[PRESERVES_NORM_PRESERVES_DOT]);;
34 add_linear_invariants [VECTOR_ANGLE_LINEAR_IMAGE_EQ];;
36 (* ------------------------------------------------------------------------- *)
37 (* Basic properties of vector angles. *)
38 (* ------------------------------------------------------------------------- *)
40 let VECTOR_ANGLE_REFL = prove
41 (`!x. vector_angle x x = if x = vec 0 then pi / &2 else &0`,
42 GEN_TAC THEN REWRITE_TAC[vector_angle; DISJ_ACI] THEN
43 COND_CASES_TAC THEN ASM_REWRITE_TAC[GSYM NORM_POW_2; REAL_POW_2] THEN
44 ASM_SIMP_TAC[REAL_DIV_REFL; REAL_ENTIRE; NORM_EQ_0; ACS_1]);;
46 let VECTOR_ANGLE_SYM = prove
47 (`!x y. vector_angle x y = vector_angle y x`,
48 REWRITE_TAC[vector_angle; DISJ_SYM; DOT_SYM; REAL_MUL_SYM]);;
50 let VECTOR_ANGLE_LMUL = prove
52 vector_angle (a % x) y =
53 if a = &0 then pi / &2
54 else if &0 <= a then vector_angle x y
55 else pi - vector_angle x y`,
56 REPEAT STRIP_TAC THEN COND_CASES_TAC THEN
57 ASM_REWRITE_TAC[vector_angle; VECTOR_MUL_EQ_0] THEN
58 ASM_CASES_TAC `x:real^N = vec 0 \/ y:real^N = vec 0` THEN
59 ASM_REWRITE_TAC[] THENL [REAL_ARITH_TAC; ALL_TAC] THEN
60 REWRITE_TAC[NORM_MUL; DOT_LMUL; real_div; REAL_INV_MUL; real_abs] THEN
62 ASM_REWRITE_TAC[REAL_INV_NEG; REAL_MUL_LNEG; REAL_MUL_RNEG] THEN
63 ASM_SIMP_TAC[REAL_FIELD
64 `~(a = &0) ==> (a * x) * (inv a * y) * z = x * y * z`] THEN
65 MATCH_MP_TAC ACS_NEG THEN
66 REWRITE_TAC[GSYM REAL_ABS_BOUNDS; GSYM REAL_INV_MUL] THEN
67 REWRITE_TAC[GSYM real_div; NORM_CAUCHY_SCHWARZ_DIV]);;
69 let VECTOR_ANGLE_RMUL = prove
71 vector_angle x (a % y) =
72 if a = &0 then pi / &2
73 else if &0 <= a then vector_angle x y
74 else pi - vector_angle x y`,
75 ONCE_REWRITE_TAC[VECTOR_ANGLE_SYM] THEN
76 REWRITE_TAC[VECTOR_ANGLE_LMUL]);;
78 let VECTOR_ANGLE_LNEG = prove
79 (`!x y. vector_angle (--x) y = pi - vector_angle x y`,
80 REWRITE_TAC[VECTOR_ARITH `--x = -- &1 % x`; VECTOR_ANGLE_LMUL] THEN
81 CONV_TAC REAL_RAT_REDUCE_CONV);;
83 let VECTOR_ANGLE_RNEG = prove
84 (`!x y. vector_angle x (--y) = pi - vector_angle x y`,
85 ONCE_REWRITE_TAC[VECTOR_ANGLE_SYM] THEN REWRITE_TAC[VECTOR_ANGLE_LNEG]);;
87 let VECTOR_ANGLE_NEG2 = prove
88 (`!x y. vector_angle (--x) (--y) = vector_angle x y`,
89 REWRITE_TAC[VECTOR_ANGLE_LNEG; VECTOR_ANGLE_RNEG] THEN REAL_ARITH_TAC);;
91 let VECTOR_ANGLE = prove
92 (`!x y:real^N. x dot y = norm(x) * norm(y) * cos(vector_angle x y)`,
93 REPEAT GEN_TAC THEN REWRITE_TAC[vector_angle] THEN
94 ASM_CASES_TAC `x:real^N = vec 0` THEN
95 ASM_REWRITE_TAC[DOT_LZERO; NORM_0; REAL_MUL_LZERO] THEN
96 ASM_CASES_TAC `y:real^N = vec 0` THEN
97 ASM_REWRITE_TAC[DOT_RZERO; NORM_0; REAL_MUL_LZERO; REAL_MUL_RZERO] THEN
98 ONCE_REWRITE_TAC[AC REAL_MUL_AC `a * b * c:real = c * a * b`] THEN
99 ASM_SIMP_TAC[GSYM REAL_EQ_LDIV_EQ; REAL_LT_MUL; NORM_POS_LT] THEN
100 MATCH_MP_TAC(GSYM COS_ACS) THEN
101 ASM_REWRITE_TAC[REAL_BOUNDS_LE; NORM_CAUCHY_SCHWARZ_DIV]);;
103 let VECTOR_ANGLE_RANGE = prove
104 (`!x y:real^N. &0 <= vector_angle x y /\ vector_angle x y <= pi`,
105 REPEAT GEN_TAC THEN REWRITE_TAC[vector_angle] THEN COND_CASES_TAC THENL
106 [MP_TAC PI_POS THEN REAL_ARITH_TAC; ALL_TAC] THEN
107 RULE_ASSUM_TAC(REWRITE_RULE[DE_MORGAN_THM]) THEN MATCH_MP_TAC ACS_BOUNDS THEN
108 ASM_REWRITE_TAC[REAL_BOUNDS_LE; NORM_CAUCHY_SCHWARZ_DIV]);;
110 let ORTHOGONAL_VECTOR_ANGLE = prove
111 (`!x y:real^N. orthogonal x y <=> vector_angle x y = pi / &2`,
112 REPEAT STRIP_TAC THEN REWRITE_TAC[orthogonal; vector_angle] THEN
113 ASM_CASES_TAC `x:real^N = vec 0` THEN ASM_REWRITE_TAC[DOT_LZERO] THEN
114 ASM_CASES_TAC `y:real^N = vec 0` THEN ASM_REWRITE_TAC[DOT_RZERO] THEN
116 [SIMP_TAC[real_div; REAL_MUL_LZERO] THEN DISCH_TAC THEN
117 REWRITE_TAC[GSYM real_div; GSYM COS_PI2] THEN
118 MATCH_MP_TAC ACS_COS THEN MP_TAC PI_POS THEN REAL_ARITH_TAC;
119 DISCH_THEN(MP_TAC o AP_TERM `cos`) THEN
120 SIMP_TAC[COS_ACS; REAL_BOUNDS_LE; NORM_CAUCHY_SCHWARZ_DIV; COS_PI2] THEN
121 ASM_SIMP_TAC[REAL_EQ_LDIV_EQ; REAL_LT_MUL; NORM_POS_LT; REAL_MUL_LZERO]]);;
123 let VECTOR_ANGLE_EQ_0 = prove
124 (`!x y:real^N. vector_angle x y = &0 <=>
125 ~(x = vec 0) /\ ~(y = vec 0) /\ norm(x) % y = norm(y) % x`,
127 MAP_EVERY ASM_CASES_TAC [`x:real^N = vec 0`; `y:real^N = vec 0`] THEN
128 ASM_SIMP_TAC[vector_angle; PI_NZ; REAL_ARITH `x / &2 = &0 <=> x = &0`] THEN
129 REWRITE_TAC[GSYM NORM_CAUCHY_SCHWARZ_EQ] THEN
130 GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [GSYM REAL_MUL_LID] THEN
131 ASM_SIMP_TAC[GSYM REAL_EQ_LDIV_EQ; NORM_POS_LT; REAL_LT_MUL] THEN
132 MESON_TAC[ACS_1; COS_ACS; REAL_BOUNDS_LE; NORM_CAUCHY_SCHWARZ_DIV; COS_0]);;
134 let VECTOR_ANGLE_EQ_PI = prove
135 (`!x y:real^N. vector_angle x y = pi <=>
136 ~(x = vec 0) /\ ~(y = vec 0) /\
137 norm(x) % y + norm(y) % x = vec 0`,
139 MP_TAC(ISPECL [`x:real^N`; `--y:real^N`] VECTOR_ANGLE_EQ_0) THEN
140 SIMP_TAC[VECTOR_ANGLE_RNEG; REAL_ARITH `pi - x = &0 <=> x = pi`] THEN
142 REWRITE_TAC[NORM_NEG; VECTOR_ARITH `--x = vec 0 <=> x = vec 0`] THEN
143 AP_TERM_TAC THEN AP_TERM_TAC THEN VECTOR_ARITH_TAC);;
145 let VECTOR_ANGLE_EQ_0_DIST = prove
146 (`!x y:real^N. vector_angle x y = &0 <=>
147 ~(x = vec 0) /\ ~(y = vec 0) /\ norm(x + y) = norm x + norm y`,
148 REWRITE_TAC[VECTOR_ANGLE_EQ_0; GSYM NORM_TRIANGLE_EQ]);;
150 let VECTOR_ANGLE_EQ_PI_DIST = prove
151 (`!x y:real^N. vector_angle x y = pi <=>
152 ~(x = vec 0) /\ ~(y = vec 0) /\ norm(x - y) = norm x + norm y`,
154 MP_TAC(ISPECL [`x:real^N`; `--y:real^N`] VECTOR_ANGLE_EQ_0_DIST) THEN
155 SIMP_TAC[VECTOR_ANGLE_RNEG; REAL_ARITH `pi - x = &0 <=> x = pi`] THEN
156 STRIP_TAC THEN REWRITE_TAC[NORM_NEG] THEN NORM_ARITH_TAC);;
158 let SIN_VECTOR_ANGLE_POS = prove
159 (`!v w. &0 <= sin(vector_angle v w)`,
160 SIMP_TAC[SIN_POS_PI_LE; VECTOR_ANGLE_RANGE]);;
162 let SIN_VECTOR_ANGLE_EQ_0 = prove
163 (`!x y. sin(vector_angle x y) = &0 <=>
164 vector_angle x y = &0 \/ vector_angle x y = pi`,
165 MESON_TAC[SIN_POS_PI; VECTOR_ANGLE_RANGE; REAL_LT_LE; SIN_0; SIN_PI]);;
167 let ASN_SIN_VECTOR_ANGLE = prove
169 asn(sin(vector_angle x y)) =
170 if vector_angle x y <= pi / &2 then vector_angle x y
171 else pi - vector_angle x y`,
172 REPEAT GEN_TAC THEN COND_CASES_TAC THENL
174 MATCH_MP_TAC EQ_TRANS THEN
175 EXISTS_TAC `asn(sin(pi - vector_angle (x:real^N) y))` THEN CONJ_TAC THENL
176 [AP_TERM_TAC THEN REWRITE_TAC[SIN_SUB; SIN_PI; COS_PI] THEN
179 MATCH_MP_TAC ASN_SIN THEN
180 MP_TAC(ISPECL [`x:real^N`; `y:real^N`] VECTOR_ANGLE_RANGE) THEN
181 ASM_REAL_ARITH_TAC);;
183 let SIN_VECTOR_ANGLE_EQ = prove
185 sin(vector_angle x y) = sin(vector_angle w z) <=>
186 vector_angle x y = vector_angle w z \/
187 vector_angle x y = pi - vector_angle w z`,
188 REPEAT GEN_TAC THEN EQ_TAC THEN
189 STRIP_TAC THEN ASM_REWRITE_TAC[SIN_SUB; SIN_PI; COS_PI] THENL
190 [ALL_TAC; REAL_ARITH_TAC] THEN
191 FIRST_X_ASSUM(MP_TAC o AP_TERM `asn`) THEN
192 REWRITE_TAC[ASN_SIN_VECTOR_ANGLE] THEN REAL_ARITH_TAC);;
194 let CONTINUOUS_WITHIN_CX_VECTOR_ANGLE_COMPOSE = prove
195 (`!f:real^M->real^N g x s.
196 ~(f x = vec 0) /\ ~(g x = vec 0) /\
197 f continuous (at x within s) /\
198 g continuous (at x within s)
199 ==> (\x. Cx(vector_angle (f x) (g x))) continuous (at x within s)`,
200 REPEAT STRIP_TAC THEN
201 ASM_CASES_TAC `trivial_limit(at (x:real^M) within s)` THEN
202 ASM_SIMP_TAC[CONTINUOUS_TRIVIAL_LIMIT; vector_angle] THEN
204 `(cacs o (\x. Cx(((f x:real^N) dot g x) / (norm(f x) * norm(g x)))))
205 continuous (at (x:real^M) within s)`
207 [MATCH_MP_TAC CONTINUOUS_WITHIN_COMPOSE THEN CONJ_TAC THENL
208 [REWRITE_TAC[CX_DIV; CX_MUL] THEN REWRITE_TAC[WITHIN_UNIV] THEN
209 MATCH_MP_TAC CONTINUOUS_COMPLEX_DIV THEN
210 ASM_SIMP_TAC[NETLIMIT_WITHIN; COMPLEX_ENTIRE; CX_INJ; NORM_EQ_0] THEN
211 REWRITE_TAC[CONTINUOUS_CX_LIFT; GSYM CX_MUL; LIFT_CMUL] THEN
212 ASM_SIMP_TAC[CONTINUOUS_LIFT_DOT2] THEN
213 MATCH_MP_TAC CONTINUOUS_MUL THEN
214 ASM_SIMP_TAC[CONTINUOUS_LIFT_NORM_COMPOSE; o_DEF];
215 MATCH_MP_TAC CONTINUOUS_WITHIN_SUBSET THEN
216 EXISTS_TAC `{z | real z /\ abs(Re z) <= &1}` THEN
217 REWRITE_TAC[CONTINUOUS_WITHIN_CACS_REAL] THEN
218 REWRITE_TAC[SUBSET; FORALL_IN_IMAGE; IN_UNIV; IN_ELIM_THM] THEN
219 REWRITE_TAC[REAL_CX; RE_CX; NORM_CAUCHY_SCHWARZ_DIV]];
220 ASM_SIMP_TAC[CONTINUOUS_WITHIN; CX_ACS; o_DEF;
221 NORM_CAUCHY_SCHWARZ_DIV] THEN
222 MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ] LIM_TRANSFORM_EVENTUALLY) THEN
224 `eventually (\y. ~((f:real^M->real^N) y = vec 0) /\
225 ~((g:real^M->real^N) y = vec 0))
228 [REWRITE_TAC[EVENTUALLY_AND] THEN CONJ_TAC THENL
229 [UNDISCH_TAC `(f:real^M->real^N) continuous (at x within s)`;
230 UNDISCH_TAC `(g:real^M->real^N) continuous (at x within s)`] THEN
231 REWRITE_TAC[CONTINUOUS_WITHIN; tendsto] THENL
232 [DISCH_THEN(MP_TAC o SPEC `norm((f:real^M->real^N) x)`);
233 DISCH_THEN(MP_TAC o SPEC `norm((g:real^M->real^N) x)`)] THEN
234 ASM_REWRITE_TAC[NORM_POS_LT] THEN
235 MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ] EVENTUALLY_MONO) THEN
236 REWRITE_TAC[] THEN CONV_TAC NORM_ARITH;
237 MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ] EVENTUALLY_MONO) THEN
238 SIMP_TAC[CX_ACS; NORM_CAUCHY_SCHWARZ_DIV]]]);;
240 let CONTINUOUS_AT_CX_VECTOR_ANGLE = prove
241 (`!c x:real^N. ~(x = vec 0) ==> (Cx o vector_angle c) continuous (at x)`,
242 REPEAT STRIP_TAC THEN REWRITE_TAC[o_DEF; vector_angle] THEN
243 ASM_CASES_TAC `c:real^N = vec 0` THEN ASM_REWRITE_TAC[CONTINUOUS_CONST] THEN
244 MATCH_MP_TAC CONTINUOUS_TRANSFORM_AT THEN
245 MAP_EVERY EXISTS_TAC [`\x:real^N. cacs(Cx((c dot x) / (norm c * norm x)))`;
246 `norm(x:real^N)`] THEN
247 ASM_REWRITE_TAC[NORM_POS_LT] THEN CONJ_TAC THENL
248 [X_GEN_TAC `z:real^N` THEN DISCH_TAC THEN COND_CASES_TAC THENL
249 [ASM_MESON_TAC[NORM_ARITH `~(dist(vec 0,x) < norm x)`]; ALL_TAC] THEN
250 MATCH_MP_TAC(GSYM CX_ACS) THEN REWRITE_TAC[NORM_CAUCHY_SCHWARZ_DIV];
252 ONCE_REWRITE_TAC[GSYM WITHIN_UNIV] THEN
253 MATCH_MP_TAC(REWRITE_RULE[o_DEF] CONTINUOUS_WITHIN_COMPOSE) THEN
255 [REWRITE_TAC[CX_DIV; CX_MUL] THEN REWRITE_TAC[WITHIN_UNIV] THEN
256 MATCH_MP_TAC CONTINUOUS_COMPLEX_DIV THEN
257 ASM_REWRITE_TAC[NETLIMIT_AT; COMPLEX_ENTIRE; CX_INJ; NORM_EQ_0] THEN
258 SIMP_TAC[CONTINUOUS_COMPLEX_MUL; CONTINUOUS_CONST;
259 CONTINUOUS_AT_CX_NORM; CONTINUOUS_AT_CX_DOT];
260 MATCH_MP_TAC CONTINUOUS_WITHIN_SUBSET THEN
261 EXISTS_TAC `{z | real z /\ abs(Re z) <= &1}` THEN
262 REWRITE_TAC[CONTINUOUS_WITHIN_CACS_REAL] THEN
263 REWRITE_TAC[SUBSET; FORALL_IN_IMAGE; IN_UNIV; IN_ELIM_THM] THEN
264 REWRITE_TAC[REAL_CX; RE_CX; NORM_CAUCHY_SCHWARZ_DIV]]);;
266 let CONTINUOUS_WITHIN_CX_VECTOR_ANGLE = prove
268 ~(x = vec 0) ==> (Cx o vector_angle c) continuous (at x within s)`,
269 SIMP_TAC[CONTINUOUS_AT_WITHIN; CONTINUOUS_AT_CX_VECTOR_ANGLE]);;
271 let REAL_CONTINUOUS_AT_VECTOR_ANGLE = prove
272 (`!c x:real^N. ~(x = vec 0) ==> (vector_angle c) real_continuous (at x)`,
273 REWRITE_TAC[REAL_CONTINUOUS_CONTINUOUS; CONTINUOUS_AT_CX_VECTOR_ANGLE]);;
275 let REAL_CONTINUOUS_WITHIN_VECTOR_ANGLE = prove
276 (`!c s x:real^N. ~(x = vec 0)
277 ==> (vector_angle c) real_continuous (at x within s)`,
278 REWRITE_TAC[REAL_CONTINUOUS_CONTINUOUS; CONTINUOUS_WITHIN_CX_VECTOR_ANGLE]);;
280 let CONTINUOUS_ON_CX_VECTOR_ANGLE = prove
281 (`!s. ~(vec 0 IN s) ==> (Cx o vector_angle c) continuous_on s`,
282 REPEAT STRIP_TAC THEN REWRITE_TAC[CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN] THEN
283 ASM_MESON_TAC[CONTINUOUS_WITHIN_CX_VECTOR_ANGLE]);;
285 let VECTOR_ANGLE_EQ = prove
286 (`!u v x y. ~(u = vec 0) /\ ~(v = vec 0) /\ ~(x = vec 0) /\ ~(y = vec 0)
287 ==> (vector_angle u v = vector_angle x y <=>
288 (x dot y) * norm(u) * norm(v) =
289 (u dot v) * norm(x) * norm(y))`,
290 SIMP_TAC[vector_angle; NORM_EQ_0; REAL_FIELD
291 `~(u = &0) /\ ~(v = &0) /\ ~(x = &0) /\ ~(y = &0)
292 ==> (a * u * v = b * x * y <=> a / (x * y) = b / (u * v))`] THEN
293 REPEAT STRIP_TAC THEN EQ_TAC THEN SIMP_TAC[] THEN
294 DISCH_THEN(MP_TAC o AP_TERM `cos`) THEN
295 SIMP_TAC[COS_ACS; NORM_CAUCHY_SCHWARZ_DIV; REAL_BOUNDS_LE]);;
297 let COS_VECTOR_ANGLE_EQ = prove
299 cos(vector_angle u v) = cos(vector_angle x y) <=>
300 vector_angle u v = vector_angle x y`,
301 MESON_TAC[ACS_COS; VECTOR_ANGLE_RANGE]);;
303 let COLLINEAR_VECTOR_ANGLE = prove
304 (`!x y. ~(x = vec 0) /\ ~(y = vec 0)
305 ==> (collinear {vec 0,x,y} <=>
306 vector_angle x y = &0 \/ vector_angle x y = pi)`,
307 REWRITE_TAC[GSYM NORM_CAUCHY_SCHWARZ_EQUAL; NORM_CAUCHY_SCHWARZ_ABS_EQ;
308 VECTOR_ANGLE_EQ_0; VECTOR_ANGLE_EQ_PI] THEN
309 REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN BINOP_TAC THEN
312 let COLLINEAR_SIN_VECTOR_ANGLE = prove
313 (`!x y. ~(x = vec 0) /\ ~(y = vec 0)
314 ==> (collinear {vec 0,x,y} <=> sin(vector_angle x y) = &0)`,
315 REWRITE_TAC[SIN_VECTOR_ANGLE_EQ_0; COLLINEAR_VECTOR_ANGLE]);;
317 let COLLINEAR_SIN_VECTOR_ANGLE_IMP = prove
318 (`!x y. sin(vector_angle x y) = &0
319 ==> ~(x = vec 0) /\ ~(y = vec 0) /\ collinear {vec 0,x,y}`,
320 MESON_TAC[COLLINEAR_SIN_VECTOR_ANGLE; SIN_VECTOR_ANGLE_EQ_0;
321 VECTOR_ANGLE_EQ_0_DIST; VECTOR_ANGLE_EQ_PI_DIST]);;
323 let VECTOR_ANGLE_EQ_0_RIGHT = prove
324 (`!x y z:real^N. vector_angle x y = &0
325 ==> (vector_angle x z = vector_angle y z)`,
326 REWRITE_TAC[VECTOR_ANGLE_EQ_0] THEN REPEAT STRIP_TAC THEN
327 MATCH_MP_TAC EQ_TRANS THEN
328 EXISTS_TAC `vector_angle (norm(x:real^N) % y) (z:real^N)` THEN CONJ_TAC THENL
329 [ASM_REWRITE_TAC[] THEN
330 ASM_REWRITE_TAC[VECTOR_ANGLE_LMUL; NORM_EQ_0; NORM_POS_LE];
331 REWRITE_TAC[VECTOR_ANGLE_LMUL] THEN
332 ASM_REWRITE_TAC[NORM_EQ_0; NORM_POS_LE]]);;
334 let VECTOR_ANGLE_EQ_0_LEFT = prove
335 (`!x y z:real^N. vector_angle x y = &0
336 ==> (vector_angle z x = vector_angle z y)`,
337 MESON_TAC[VECTOR_ANGLE_EQ_0_RIGHT; VECTOR_ANGLE_SYM]);;
339 let VECTOR_ANGLE_EQ_PI_RIGHT = prove
340 (`!x y z:real^N. vector_angle x y = pi
341 ==> (vector_angle x z = pi - vector_angle y z)`,
342 REPEAT STRIP_TAC THEN
343 MP_TAC(ISPECL [`--x:real^N`; `y:real^N`; `z:real^N`]
344 VECTOR_ANGLE_EQ_0_RIGHT) THEN
345 ASM_REWRITE_TAC[VECTOR_ANGLE_LNEG] THEN REAL_ARITH_TAC);;
347 let VECTOR_ANGLE_EQ_PI_LEFT = prove
348 (`!x y z:real^N. vector_angle x y = pi
349 ==> (vector_angle z x = pi - vector_angle z y)`,
350 MESON_TAC[VECTOR_ANGLE_EQ_PI_RIGHT; VECTOR_ANGLE_SYM]);;
352 let COS_VECTOR_ANGLE = prove
354 cos(vector_angle x y) = if x = vec 0 \/ y = vec 0 then &0
355 else (x dot y) / (norm x * norm y)`,
357 ASM_CASES_TAC `x:real^N = vec 0` THENL
358 [ASM_REWRITE_TAC[vector_angle; COS_PI2]; ALL_TAC] THEN
359 ASM_CASES_TAC `y:real^N = vec 0` THENL
360 [ASM_REWRITE_TAC[vector_angle; COS_PI2]; ALL_TAC] THEN
361 ASM_SIMP_TAC[REAL_EQ_RDIV_EQ; REAL_LT_MUL; NORM_POS_LT; VECTOR_ANGLE] THEN
364 let SIN_VECTOR_ANGLE = prove
366 sin(vector_angle x y) =
367 if x = vec 0 \/ y = vec 0 then &1
368 else sqrt(&1 - ((x dot y) / (norm x * norm y)) pow 2)`,
369 SIMP_TAC[SIN_COS_SQRT; SIN_VECTOR_ANGLE_POS; COS_VECTOR_ANGLE] THEN
370 REPEAT GEN_TAC THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
371 CONV_TAC REAL_RAT_REDUCE_CONV THEN REWRITE_TAC[SQRT_1]);;
373 let SIN_SQUARED_VECTOR_ANGLE = prove
375 sin(vector_angle x y) pow 2 =
376 if x = vec 0 \/ y = vec 0 then &1
377 else &1 - ((x dot y) / (norm x * norm y)) pow 2`,
378 REPEAT GEN_TAC THEN REWRITE_TAC
379 [REWRITE_RULE [REAL_ARITH `s + c = &1 <=> s = &1 - c`] SIN_CIRCLE] THEN
380 REWRITE_TAC[COS_VECTOR_ANGLE] THEN REAL_ARITH_TAC);;
382 let VECTOR_ANGLE_COMPLEX_LMUL = prove
384 ==> vector_angle (a * x) (a * y) = vector_angle x y`,
385 REPEAT STRIP_TAC THEN
386 ASM_CASES_TAC `x = Cx(&0)` THENL
387 [ASM_REWRITE_TAC[COMPLEX_MUL_RZERO; vector_angle; COMPLEX_VEC_0];
389 ASM_CASES_TAC `y = Cx(&0)` THENL
390 [ASM_REWRITE_TAC[COMPLEX_MUL_RZERO; vector_angle; COMPLEX_VEC_0];
393 [`a * x:complex`; `a * y:complex`; `x:complex`; `y:complex`]
394 VECTOR_ANGLE_EQ) THEN
395 ASM_REWRITE_TAC[COMPLEX_VEC_0; COMPLEX_ENTIRE] THEN
396 DISCH_THEN SUBST1_TAC THEN
397 REWRITE_TAC[COMPLEX_NORM_MUL] THEN MATCH_MP_TAC(REAL_RING
398 `a pow 2 * xy:real = d ==> xy * (a * x) * (a * y) = d * x * y`) THEN
399 REWRITE_TAC[NORM_POW_2] THEN
400 REWRITE_TAC[DOT_2; complex_mul; GSYM RE_DEF; GSYM IM_DEF; RE; IM] THEN
403 let VECTOR_ANGLE_1 = prove
404 (`!x. vector_angle x (Cx(&1)) = acs(Re x / norm x)`,
406 SIMP_TAC[vector_angle; COMPLEX_VEC_0; CX_INJ; REAL_OF_NUM_EQ; ARITH_EQ] THEN
408 [ASM_REWRITE_TAC[real_div; RE_CX; ACS_0; REAL_MUL_LZERO]; ALL_TAC] THEN
409 REWRITE_TAC[COMPLEX_NORM_CX; REAL_ABS_NUM; REAL_MUL_RID] THEN
410 REWRITE_TAC[DOT_2; GSYM RE_DEF; GSYM IM_DEF; RE_CX; IM_CX] THEN
411 AP_TERM_TAC THEN REAL_ARITH_TAC);;
413 let ARG_EQ_VECTOR_ANGLE_1 = prove
414 (`!z. ~(z = Cx(&0)) /\ &0 <= Im z ==> Arg z = vector_angle z (Cx(&1))`,
415 REPEAT STRIP_TAC THEN REWRITE_TAC[VECTOR_ANGLE_1] THEN
416 GEN_REWRITE_TAC (RAND_CONV o RAND_CONV o LAND_CONV o RAND_CONV) [ARG] THEN
417 REWRITE_TAC[RE_MUL_CX; RE_CEXP; RE_II; IM_MUL_II; IM_CX; RE_CX] THEN
418 REWRITE_TAC[REAL_MUL_LZERO; REAL_EXP_0; REAL_MUL_LID] THEN
419 ASM_SIMP_TAC[COMPLEX_NORM_ZERO; REAL_FIELD
420 `~(z = &0) ==> (z * x) / z = x`] THEN
421 CONV_TAC SYM_CONV THEN MATCH_MP_TAC ACS_COS THEN
422 ASM_REWRITE_TAC[ARG; ARG_LE_PI]);;
424 let VECTOR_ANGLE_ARG = prove
425 (`!w z. ~(w = Cx(&0)) /\ ~(z = Cx(&0))
426 ==> vector_angle w z = if &0 <= Im(z / w) then Arg(z / w)
427 else &2 * pi - Arg(z / w)`,
428 REPEAT STRIP_TAC THEN COND_CASES_TAC THENL
429 [SUBGOAL_THEN `z = w * (z / w) /\ w = w * Cx(&1)` MP_TAC THENL
430 [REPEAT(POP_ASSUM MP_TAC) THEN CONV_TAC COMPLEX_FIELD; ALL_TAC];
431 SUBGOAL_THEN `w = z * (w / z) /\ z = z * Cx(&1)` MP_TAC THENL
432 [REPEAT(POP_ASSUM MP_TAC) THEN CONV_TAC COMPLEX_FIELD; ALL_TAC]] THEN
433 DISCH_THEN(fun th -> GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [th]) THEN
434 ASM_SIMP_TAC[VECTOR_ANGLE_COMPLEX_LMUL] THENL
435 [ONCE_REWRITE_TAC[VECTOR_ANGLE_SYM] THEN CONV_TAC SYM_CONV THEN
436 MATCH_MP_TAC ARG_EQ_VECTOR_ANGLE_1 THEN ASM_REWRITE_TAC[] THEN
437 REPEAT(POP_ASSUM MP_TAC) THEN CONV_TAC COMPLEX_FIELD;
438 MP_TAC(ISPEC `z / w:complex` ARG_INV) THEN ANTS_TAC THENL
439 [ASM_MESON_TAC[real; REAL_LE_REFL]; DISCH_THEN(SUBST1_TAC o SYM)] THEN
440 REWRITE_TAC[COMPLEX_INV_DIV] THEN CONV_TAC SYM_CONV THEN
441 MATCH_MP_TAC ARG_EQ_VECTOR_ANGLE_1 THEN CONJ_TAC THENL
442 [REPEAT(POP_ASSUM MP_TAC) THEN CONV_TAC COMPLEX_FIELD;
443 ONCE_REWRITE_TAC[GSYM COMPLEX_INV_DIV] THEN
444 REWRITE_TAC[IM_COMPLEX_INV_GE_0] THEN ASM_REAL_ARITH_TAC]]);;
446 (* ------------------------------------------------------------------------- *)
447 (* Traditional geometric notion of angle (always 0 <= theta <= pi). *)
448 (* ------------------------------------------------------------------------- *)
450 let angle = new_definition
451 `angle(a,b,c) = vector_angle (a - b) (c - b)`;;
453 let ANGLE_LINEAR_IMAGE_EQ = prove
455 linear f /\ (!x. norm(f x) = norm x)
456 ==> angle(f a,f b,f c) = angle(a,b,c)`,
457 SIMP_TAC[angle; GSYM LINEAR_SUB; VECTOR_ANGLE_LINEAR_IMAGE_EQ]);;
459 add_linear_invariants [ANGLE_LINEAR_IMAGE_EQ];;
461 let ANGLE_TRANSLATION_EQ = prove
462 (`!a b c d. angle(a + b,a + c,a + d) = angle(b,c,d)`,
463 REPEAT GEN_TAC THEN REWRITE_TAC[angle] THEN
464 BINOP_TAC THEN VECTOR_ARITH_TAC);;
466 add_translation_invariants [ANGLE_TRANSLATION_EQ];;
468 let VECTOR_ANGLE_ANGLE = prove
469 (`vector_angle x y = angle(x,vec 0,y)`,
470 REWRITE_TAC[angle; VECTOR_SUB_RZERO]);;
472 let ANGLE_EQ_PI_DIST = prove
474 angle(A,B,C) = pi <=>
475 ~(A = B) /\ ~(C = B) /\ dist(A,C) = dist(A,B) + dist(B,C)`,
476 REWRITE_TAC[angle; VECTOR_ANGLE_EQ_PI_DIST] THEN NORM_ARITH_TAC);;
478 let SIN_ANGLE_POS = prove
479 (`!A B C. &0 <= sin(angle(A,B,C))`,
480 REWRITE_TAC[angle; SIN_VECTOR_ANGLE_POS]);;
483 (`!A B C. (A - C) dot (B - C) = dist(A,C) * dist(B,C) * cos(angle(A,C,B))`,
484 REWRITE_TAC[angle; dist; GSYM VECTOR_ANGLE]);;
486 let ANGLE_REFL = prove
487 (`!A B. angle(A,A,B) = pi / &2 /\ angle(B,A,A) = pi / &2`,
488 REWRITE_TAC[angle; vector_angle; VECTOR_SUB_REFL]);;
490 let ANGLE_REFL_MID = prove
491 (`!A B. ~(A = B) ==> angle(A,B,A) = &0`,
492 SIMP_TAC[angle; vector_angle; VECTOR_SUB_EQ; GSYM NORM_POW_2; ARITH;
493 GSYM REAL_POW_2; REAL_DIV_REFL; ACS_1; REAL_POW_EQ_0; NORM_EQ_0]);;
495 let ANGLE_SYM = prove
496 (`!A B C. angle(A,B,C) = angle(C,B,A)`,
497 REWRITE_TAC[angle; vector_angle; VECTOR_SUB_EQ; DISJ_SYM;
498 REAL_MUL_SYM; DOT_SYM]);;
500 let ANGLE_RANGE = prove
501 (`!A B C. &0 <= angle(A,B,C) /\ angle(A,B,C) <= pi`,
502 REWRITE_TAC[angle; VECTOR_ANGLE_RANGE]);;
504 let COS_ANGLE_EQ = prove
506 cos(angle(a,b,c)) = cos(angle(a',b',c')) <=>
507 angle(a,b,c) = angle(a',b',c')`,
508 REWRITE_TAC[angle; COS_VECTOR_ANGLE_EQ]);;
512 ~(a = b) /\ ~(c = b) /\ ~(a' = b') /\ ~(c' = b')
513 ==> (angle(a,b,c) = angle(a',b',c') <=>
514 ((a' - b') dot (c' - b')) * norm (a - b) * norm (c - b) =
515 ((a - b) dot (c - b)) * norm (a' - b') * norm (c' - b'))`,
516 SIMP_TAC[angle; VECTOR_ANGLE_EQ; VECTOR_SUB_EQ]);;
518 let SIN_ANGLE_EQ_0 = prove
519 (`!A B C. sin(angle(A,B,C)) = &0 <=> angle(A,B,C) = &0 \/ angle(A,B,C) = pi`,
520 REWRITE_TAC[angle; SIN_VECTOR_ANGLE_EQ_0]);;
522 let SIN_ANGLE_EQ = prove
523 (`!A B C A' B' C'. sin(angle(A,B,C)) = sin(angle(A',B',C')) <=>
524 angle(A,B,C) = angle(A',B',C') \/
525 angle(A,B,C) = pi - angle(A',B',C')`,
526 REWRITE_TAC[angle; SIN_VECTOR_ANGLE_EQ]);;
528 let COLLINEAR_ANGLE = prove
529 (`!A B C. ~(A = B) /\ ~(B = C)
530 ==> (collinear {A,B,C} <=> angle(A,B,C) = &0 \/ angle(A,B,C) = pi)`,
531 ONCE_REWRITE_TAC[COLLINEAR_3] THEN
532 SIMP_TAC[COLLINEAR_VECTOR_ANGLE; VECTOR_SUB_EQ; angle]);;
534 let COLLINEAR_SIN_ANGLE = prove
535 (`!A B C. ~(A = B) /\ ~(B = C)
536 ==> (collinear {A,B,C} <=> sin(angle(A,B,C)) = &0)`,
537 REWRITE_TAC[SIN_ANGLE_EQ_0; COLLINEAR_ANGLE]);;
539 let COLLINEAR_SIN_ANGLE_IMP = prove
540 (`!A B C. sin(angle(A,B,C)) = &0
541 ==> ~(A = B) /\ ~(B = C) /\ collinear {A,B,C}`,
543 ONCE_REWRITE_TAC[COLLINEAR_3] THEN REWRITE_TAC[angle] THEN
544 DISCH_THEN(MP_TAC o MATCH_MP COLLINEAR_SIN_VECTOR_ANGLE_IMP) THEN
545 SIMP_TAC[VECTOR_SUB_EQ]);;
547 let ANGLE_EQ_0_RIGHT = prove
548 (`!A B C. angle(A,B,C) = &0 ==> angle(A,B,D) = angle(C,B,D)`,
549 REWRITE_TAC[VECTOR_ANGLE_EQ_0_RIGHT; angle]);;
551 let ANGLE_EQ_0_LEFT = prove
552 (`!A B C. angle(A,B,C) = &0 ==> angle(D,B,A) = angle(D,B,C)`,
553 MESON_TAC[ANGLE_EQ_0_RIGHT; ANGLE_SYM]);;
555 let ANGLE_EQ_PI_RIGHT = prove
556 (`!A B C. angle(A,B,C) = pi ==> angle(A,B,D) = pi - angle(C,B,D)`,
557 REWRITE_TAC[VECTOR_ANGLE_EQ_PI_RIGHT; angle]);;
559 let ANGLE_EQ_PI_LEFT = prove
560 (`!A B C. angle(A,B,C) = pi ==> angle(A,B,D) = pi - angle(C,B,D)`,
561 MESON_TAC[ANGLE_EQ_PI_RIGHT; ANGLE_SYM]);;
563 let COS_ANGLE = prove
564 (`!a b c. cos(angle(a,b,c)) = if a = b \/ c = b then &0
565 else ((a - b) dot (c - b)) /
566 (norm(a - b) * norm(c - b))`,
567 REWRITE_TAC[angle; COS_VECTOR_ANGLE; VECTOR_SUB_EQ]);;
569 let SIN_ANGLE = prove
570 (`!a b c. sin(angle(a,b,c)) =
571 if a = b \/ c = b then &1
572 else sqrt(&1 - (((a - b) dot (c - b)) /
573 (norm(a - b) * norm(c - b))) pow 2)`,
574 REWRITE_TAC[angle; SIN_VECTOR_ANGLE; VECTOR_SUB_EQ]);;
576 let SIN_SQUARED_ANGLE = prove
577 (`!a b c. sin(angle(a,b,c)) pow 2 =
578 if a = b \/ c = b then &1
579 else &1 - (((a - b) dot (c - b)) /
580 (norm(a - b) * norm(c - b))) pow 2`,
581 REWRITE_TAC[angle; SIN_SQUARED_VECTOR_ANGLE; VECTOR_SUB_EQ]);;
583 (* ------------------------------------------------------------------------- *)
584 (* The law of cosines. *)
585 (* ------------------------------------------------------------------------- *)
587 let LAW_OF_COSINES = prove
589 dist(B,C) pow 2 = (dist(A,B) pow 2 + dist(A,C) pow 2) -
590 &2 * dist(A,B) * dist(A,C) * cos(angle(B,A,C))`,
592 REWRITE_TAC[angle; ONCE_REWRITE_RULE[NORM_SUB] dist; GSYM VECTOR_ANGLE;
596 (* ------------------------------------------------------------------------- *)
597 (* The law of sines. *)
598 (* ------------------------------------------------------------------------- *)
600 let LAW_OF_SINES = prove
602 sin(angle(A,B,C)) * dist(B,C) = sin(angle(B,A,C)) * dist(A,C)`,
603 REPEAT GEN_TAC THEN MATCH_MP_TAC REAL_POW_EQ THEN EXISTS_TAC `2` THEN
604 SIMP_TAC[SIN_ANGLE_POS; DIST_POS_LE; REAL_LE_MUL; ARITH] THEN
605 REWRITE_TAC[REAL_POW_MUL; MATCH_MP
606 (REAL_ARITH `x + y = &1 ==> x = &1 - y`) (SPEC_ALL SIN_CIRCLE)] THEN
607 ASM_CASES_TAC `A:real^N = B` THEN ASM_REWRITE_TAC[ANGLE_REFL; COS_PI2] THEN
608 RULE_ASSUM_TAC(ONCE_REWRITE_RULE[GSYM VECTOR_SUB_EQ]) THEN
609 RULE_ASSUM_TAC(REWRITE_RULE[GSYM NORM_EQ_0]) THEN
610 FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_RING
611 `~(a = &0) ==> a pow 2 * x = a pow 2 * y ==> x = y`)) THEN
612 ONCE_REWRITE_TAC[DIST_SYM] THEN REWRITE_TAC[GSYM dist] THEN
613 GEN_REWRITE_TAC (RAND_CONV o LAND_CONV o ONCE_DEPTH_CONV) [DIST_SYM] THEN
614 REWRITE_TAC[REAL_RING
615 `a * (&1 - x) * b = c * (&1 - y) * d <=>
616 a * b - a * b * x = c * d - c * d * y`] THEN
617 REWRITE_TAC[GSYM REAL_POW_MUL; GSYM ANGLE] THEN
618 REWRITE_TAC[REAL_POW_MUL; dist; NORM_POW_2] THEN
619 REWRITE_TAC[DOT_LSUB; DOT_RSUB; DOT_SYM] THEN CONV_TAC REAL_RING);;
621 (* ------------------------------------------------------------------------- *)
622 (* The sum of the angles of a triangle. *)
623 (* ------------------------------------------------------------------------- *)
625 let TRIANGLE_ANGLE_SUM_LEMMA = prove
626 (`!A B C:real^N. ~(A = B) /\ ~(A = C) /\ ~(B = C)
627 ==> cos(angle(B,A,C) + angle(A,B,C) + angle(B,C,A)) = -- &1`,
628 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[GSYM VECTOR_SUB_EQ] THEN
629 REWRITE_TAC[GSYM NORM_EQ_0] THEN
630 MP_TAC(ISPECL [`A:real^N`; `B:real^N`; `C:real^N`] LAW_OF_COSINES) THEN
631 MP_TAC(ISPECL [`B:real^N`; `A:real^N`; `C:real^N`] LAW_OF_COSINES) THEN
632 MP_TAC(ISPECL [`C:real^N`; `B:real^N`; `A:real^N`] LAW_OF_COSINES) THEN
633 MP_TAC(ISPECL [`A:real^N`; `B:real^N`; `C:real^N`] LAW_OF_SINES) THEN
634 MP_TAC(ISPECL [`B:real^N`; `A:real^N`; `C:real^N`] LAW_OF_SINES) THEN
635 MP_TAC(ISPECL [`B:real^N`; `C:real^N`; `A:real^N`] LAW_OF_SINES) THEN
636 REWRITE_TAC[COS_ADD; SIN_ADD; dist; NORM_SUB] THEN
637 MAP_EVERY (fun t -> MP_TAC(SPEC t SIN_CIRCLE))
638 [`angle(B:real^N,A,C)`; `angle(A:real^N,B,C)`; `angle(B:real^N,C,A)`] THEN
639 REWRITE_TAC[COS_ADD; SIN_ADD; ANGLE_SYM] THEN CONV_TAC REAL_RING);;
641 let COS_MINUS1_LEMMA = prove
642 (`!x. cos(x) = -- &1 /\ &0 <= x /\ x < &3 * pi ==> x = pi`,
643 REPEAT STRIP_TAC THEN
644 SUBGOAL_THEN `?n. integer n /\ x = n * pi`
645 (X_CHOOSE_THEN `nn:real` (CONJUNCTS_THEN2 ASSUME_TAC SUBST_ALL_TAC)) THEN
646 REWRITE_TAC[GSYM SIN_EQ_0] THENL
647 [MP_TAC(SPEC `x:real` SIN_CIRCLE) THEN ASM_REWRITE_TAC[] THEN
650 SUBGOAL_THEN `?n. nn = &n` (X_CHOOSE_THEN `n:num` SUBST_ALL_TAC) THENL
651 [FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [REAL_MUL_POS_LE]) THEN
652 SIMP_TAC[PI_POS; REAL_ARITH `&0 < p ==> ~(p < &0) /\ ~(p = &0)`] THEN
653 ASM_MESON_TAC[INTEGER_POS; REAL_LT_LE];
655 MATCH_MP_TAC(REAL_RING `n = &1 ==> n * p = p`) THEN
656 REWRITE_TAC[REAL_OF_NUM_EQ] THEN
657 MATCH_MP_TAC(ARITH_RULE `n < 3 /\ ~(n = 0) /\ ~(n = 2) ==> n = 1`) THEN
658 RULE_ASSUM_TAC(SIMP_RULE[REAL_LT_RMUL_EQ; PI_POS; REAL_OF_NUM_LT]) THEN
659 ASM_REWRITE_TAC[] THEN CONJ_TAC THEN DISCH_THEN SUBST_ALL_TAC THEN
660 REPEAT(POP_ASSUM MP_TAC) THEN SIMP_TAC[COS_0; REAL_MUL_LZERO; COS_NPI] THEN
663 let TRIANGLE_ANGLE_SUM = prove
664 (`!A B C:real^N. ~(A = B /\ B = C /\ A = C)
665 ==> angle(B,A,C) + angle(A,B,C) + angle(B,C,A) = pi`,
666 REPEAT GEN_TAC THEN MAP_EVERY ASM_CASES_TAC
667 [`A:real^N = B`; `B:real^N = C`; `A:real^N = C`] THEN
668 ASM_SIMP_TAC[ANGLE_REFL_MID; ANGLE_REFL; REAL_HALF; REAL_ADD_RID] THEN
669 REPEAT(FIRST_X_ASSUM SUBST_ALL_TAC) THEN
670 REPEAT(POP_ASSUM MP_TAC) THEN REWRITE_TAC[REAL_ADD_LID; REAL_HALF] THEN
671 REPEAT STRIP_TAC THEN MATCH_MP_TAC COS_MINUS1_LEMMA THEN
672 ASM_SIMP_TAC[TRIANGLE_ANGLE_SUM_LEMMA; REAL_LE_ADD; ANGLE_RANGE] THEN
673 MATCH_MP_TAC(REAL_ARITH
674 `&0 <= x /\ x <= p /\ &0 <= y /\ y <= p /\ &0 <= z /\ z <= p /\
675 ~(x = p /\ y = p /\ z = p)
676 ==> x + y + z < &3 * p`) THEN
677 ASM_SIMP_TAC[ANGLE_RANGE] THEN REPEAT STRIP_TAC THEN
678 REPEAT(FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [ANGLE_EQ_PI_DIST])) THEN
679 REPEAT(FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE RAND_CONV
680 [GSYM VECTOR_SUB_EQ])) THEN
681 REWRITE_TAC[GSYM NORM_EQ_0; dist; NORM_SUB] THEN REAL_ARITH_TAC);;
683 (* ------------------------------------------------------------------------- *)
684 (* A few more lemmas about angles. *)
685 (* ------------------------------------------------------------------------- *)
687 let ANGLE_EQ_PI_OTHERS = prove
690 ==> angle(B,C,A) = &0 /\ angle(A,C,B) = &0 /\
691 angle(B,A,C) = &0 /\ angle(C,A,B) = &0`,
692 REPEAT GEN_TAC THEN DISCH_TAC THEN
693 FIRST_ASSUM(STRIP_ASSUME_TAC o GEN_REWRITE_RULE I [ANGLE_EQ_PI_DIST]) THEN
694 MP_TAC(ISPECL [`A:real^N`; `B:real^N`; `C:real^N`] TRIANGLE_ANGLE_SUM) THEN
695 ASM_REWRITE_TAC[] THEN DISCH_THEN(MP_TAC o MATCH_MP (REAL_ARITH
696 `x + p + y = p ==> &0 <= x /\ &0 <= y ==> x = &0 /\ y = &0`)) THEN
697 SIMP_TAC[ANGLE_RANGE; ANGLE_SYM]);;
699 let ANGLE_EQ_0_DIST = prove
700 (`!A B C:real^N. angle(A,B,C) = &0 <=>
701 ~(A = B) /\ ~(C = B) /\
702 (dist(A,B) = dist(A,C) + dist(C,B) \/
703 dist(B,C) = dist(A,C) + dist(A,B))`,
705 ASM_CASES_TAC `A:real^N = B` THENL
706 [ASM_REWRITE_TAC[angle; VECTOR_ANGLE_EQ_0; VECTOR_SUB_EQ]; ALL_TAC] THEN
707 ASM_CASES_TAC `B:real^N = C` THENL
708 [ASM_REWRITE_TAC[angle; VECTOR_ANGLE_EQ_0; VECTOR_SUB_EQ]; ALL_TAC] THEN
709 ASM_CASES_TAC `A:real^N = C` THENL
710 [ASM_SIMP_TAC[ANGLE_REFL_MID; DIST_REFL; REAL_ADD_LID]; ALL_TAC] THEN
714 [MP_TAC(ISPECL[`A:real^N`; `C:real^N`; `B:real^N`] ANGLE_EQ_PI_DIST);
715 MP_TAC(ISPECL[`B:real^N`; `A:real^N`; `C:real^N`] ANGLE_EQ_PI_DIST)] THEN
716 ASM_REWRITE_TAC[] THEN REWRITE_TAC[DIST_SYM; REAL_ADD_AC] THEN
717 DISCH_THEN(MP_TAC o MATCH_MP ANGLE_EQ_PI_OTHERS) THEN SIMP_TAC[]] THEN
718 ASM_REWRITE_TAC[angle; VECTOR_ANGLE_EQ_0; VECTOR_SUB_EQ] THEN
719 REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC
720 (ISPECL [`norm(A - B:real^N)`; `norm(C - B:real^N)`]
723 [ASM_REWRITE_TAC[VECTOR_MUL_LCANCEL; NORM_EQ_0; VECTOR_SUB_EQ;
724 VECTOR_ARITH `c - b:real^N = a - b <=> a = c`];
725 ONCE_REWRITE_TAC[VECTOR_ARITH
726 `norm(A - B) % (C - B) = norm(C - B) % (A - B) <=>
727 (norm(C - B) - norm(A - B)) % (A - B) = norm(A - B) % (C - A)`];
728 ONCE_REWRITE_TAC[VECTOR_ARITH
729 `norm(A - B) % (C - B) = norm(C - B) % (A - B) <=>
730 (norm(A - B) - norm(C - B)) % (C - B) = norm(C - B) % (A - C)`]] THEN
731 DISCH_THEN(MP_TAC o MATCH_MP
732 (REWRITE_RULE[IMP_CONJ] NORM_CROSS_MULTIPLY)) THEN
733 ASM_SIMP_TAC[REAL_SUB_LT; NORM_POS_LT; VECTOR_SUB_EQ] THEN
734 SIMP_TAC[GSYM DIST_TRIANGLE_EQ] THEN SIMP_TAC[DIST_SYM]);;
736 let ANGLE_EQ_0_DIST_ABS = prove
737 (`!A B C:real^N. angle(A,B,C) = &0 <=>
738 ~(A = B) /\ ~(C = B) /\
739 dist(A,C) = abs(dist(A,B) - dist(C,B))`,
740 REPEAT GEN_TAC THEN REWRITE_TAC[ANGLE_EQ_0_DIST] THEN
741 AP_TERM_TAC THEN AP_TERM_TAC THEN
742 MP_TAC(ISPECL [`A:real^N`; `C:real^N`] DIST_POS_LE) THEN
743 REWRITE_TAC[DIST_SYM] THEN REAL_ARITH_TAC);;
745 (* ------------------------------------------------------------------------- *)
746 (* Some rules for congruent triangles (not necessarily in the same real^N). *)
747 (* ------------------------------------------------------------------------- *)
749 let CONGRUENT_TRIANGLES_SSS = prove
750 (`!A B C:real^M A' B' C':real^N.
751 dist(A,B) = dist(A',B') /\
752 dist(B,C) = dist(B',C') /\
753 dist(C,A) = dist(C',A')
754 ==> angle(A,B,C) = angle(A',B',C')`,
755 REPEAT GEN_TAC THEN MAP_EVERY ASM_CASES_TAC
756 [`dist(A':real^N,B') = &0`; `dist(B':real^N,C') = &0`] THEN
757 ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
758 RULE_ASSUM_TAC(REWRITE_RULE[DIST_EQ_0]) THEN
759 ASM_SIMP_TAC[ANGLE_REFL_MID; ANGLE_REFL] THEN
760 ONCE_REWRITE_TAC[GSYM COS_ANGLE_EQ] THEN
761 MP_TAC(ISPECL [`B:real^M`; `A:real^M`; `C:real^M`] LAW_OF_COSINES) THEN
762 MP_TAC(ISPECL [`B':real^N`; `A':real^N`; `C':real^N`] LAW_OF_COSINES) THEN
763 REPEAT(POP_ASSUM MP_TAC) THEN REWRITE_TAC[GSYM DIST_EQ_0; DIST_SYM] THEN
764 CONV_TAC REAL_FIELD);;
766 let CONGRUENT_TRIANGLES_SAS = prove
767 (`!A B C:real^M A' B' C':real^N.
768 dist(A,B) = dist(A',B') /\
769 angle(A,B,C) = angle(A',B',C') /\
770 dist(B,C) = dist(B',C')
771 ==> dist(A,C) = dist(A',C')`,
772 REPEAT STRIP_TAC THEN REWRITE_TAC[DIST_EQ] THEN
773 MP_TAC(ISPECL [`B:real^M`; `A:real^M`; `C:real^M`] LAW_OF_COSINES) THEN
774 MP_TAC(ISPECL [`B':real^N`; `A':real^N`; `C':real^N`] LAW_OF_COSINES) THEN
775 REPEAT(DISCH_THEN SUBST1_TAC) THEN
776 REPEAT BINOP_TAC THEN ASM_MESON_TAC[DIST_SYM]);;
778 let CONGRUENT_TRIANGLES_AAS = prove
779 (`!A B C:real^M A' B' C':real^N.
780 angle(A,B,C) = angle(A',B',C') /\
781 angle(B,C,A) = angle(B',C',A') /\
782 dist(A,B) = dist(A',B') /\
784 ==> dist(A,C) = dist(A',C') /\ dist(B,C) = dist(B',C')`,
785 REPEAT GEN_TAC THEN ASM_CASES_TAC `A:real^M = B` THENL
786 [FIRST_X_ASSUM SUBST_ALL_TAC THEN REWRITE_TAC[INSERT_AC; COLLINEAR_2];
788 DISCH_TAC THEN SUBGOAL_THEN `~(A':real^N = B')` ASSUME_TAC THENL
789 [ASM_MESON_TAC[DIST_EQ_0]; ALL_TAC] THEN
790 SUBGOAL_THEN `angle(C:real^M,A,B) = angle(C':real^N,A',B')` ASSUME_TAC THENL
791 [MP_TAC(ISPECL [`A:real^M`; `B:real^M`; `C:real^M`] TRIANGLE_ANGLE_SUM) THEN
792 MP_TAC(ISPECL [`A':real^N`; `B':real^N`; `C':real^N`]
793 TRIANGLE_ANGLE_SUM) THEN ASM_REWRITE_TAC[IMP_IMP] THEN
794 REWRITE_TAC[ANGLE_SYM] THEN REAL_ARITH_TAC;
796 MATCH_MP_TAC(TAUT `a /\ (a ==> b) ==> a /\ b`) THEN CONJ_TAC THENL
797 [MP_TAC(ISPECL [`C:real^M`; `B:real^M`; `A:real^M`] LAW_OF_SINES) THEN
798 MP_TAC(ISPECL [`C':real^N`; `B':real^N`; `A':real^N`] LAW_OF_SINES) THEN
799 SUBGOAL_THEN `~(sin(angle(B':real^N,C',A')) = &0)` MP_TAC THENL
800 [ASM_MESON_TAC[COLLINEAR_SIN_ANGLE_IMP; INSERT_AC];
801 ASM_REWRITE_TAC[] THEN ONCE_REWRITE_TAC[ANGLE_SYM; DIST_SYM] THEN
802 ASM_REWRITE_TAC[] THEN REWRITE_TAC[ANGLE_SYM; DIST_SYM] THEN
803 CONV_TAC REAL_FIELD];
804 ASM_MESON_TAC[CONGRUENT_TRIANGLES_SAS; DIST_SYM; ANGLE_SYM]]);;
806 let CONGRUENT_TRIANGLES_ASA = prove
807 (`!A B C:real^M A' B' C':real^N.
808 angle(A,B,C) = angle(A',B',C') /\
809 dist(A,B) = dist(A',B') /\
810 angle(B,A,C) = angle(B',A',C') /\
812 ==> dist(A,C) = dist(A',C')`,
813 REPEAT GEN_TAC THEN ASM_CASES_TAC `A:real^M = B` THENL
814 [FIRST_X_ASSUM SUBST_ALL_TAC THEN REWRITE_TAC[INSERT_AC; COLLINEAR_2];
816 REPEAT STRIP_TAC THEN SUBGOAL_THEN `~(A':real^N = B')` ASSUME_TAC THENL
817 [ASM_MESON_TAC[DIST_EQ_0]; ALL_TAC] THEN
818 MP_TAC(ISPECL [`A:real^M`; `B:real^M`; `C:real^M`] TRIANGLE_ANGLE_SUM) THEN
819 MP_TAC(ISPECL [`A':real^N`; `B':real^N`; `C':real^N`]
820 TRIANGLE_ANGLE_SUM) THEN
821 ASM_REWRITE_TAC[IMP_IMP] THEN
822 DISCH_THEN(MP_TAC o MATCH_MP (REAL_ARITH
823 `a + b + x = pi /\ a + b + y = pi ==> x = y`)) THEN
824 ASM_MESON_TAC[CONGRUENT_TRIANGLES_AAS; DIST_SYM; ANGLE_SYM]);;
826 (* ------------------------------------------------------------------------- *)
827 (* Full versions where we deduce everything from the conditions. *)
828 (* ------------------------------------------------------------------------- *)
830 let CONGRUENT_TRIANGLES_SSS_FULL = prove
831 (`!A B C:real^M A' B' C':real^N.
832 dist(A,B) = dist(A',B') /\
833 dist(B,C) = dist(B',C') /\
834 dist(C,A) = dist(C',A')
835 ==> dist(A,B) = dist(A',B') /\
836 dist(B,C) = dist(B',C') /\
837 dist(C,A) = dist(C',A') /\
838 angle(A,B,C) = angle(A',B',C') /\
839 angle(B,C,A) = angle(B',C',A') /\
840 angle(C,A,B) = angle(C',A',B')`,
841 MESON_TAC[CONGRUENT_TRIANGLES_SSS; DIST_SYM; ANGLE_SYM]);;
843 let CONGRUENT_TRIANGLES_SAS_FULL = prove
844 (`!A B C:real^M A' B' C':real^N.
845 dist(A,B) = dist(A',B') /\
846 angle(A,B,C) = angle(A',B',C') /\
847 dist(B,C) = dist(B',C')
848 ==> dist(A,B) = dist(A',B') /\
849 dist(B,C) = dist(B',C') /\
850 dist(C,A) = dist(C',A') /\
851 angle(A,B,C) = angle(A',B',C') /\
852 angle(B,C,A) = angle(B',C',A') /\
853 angle(C,A,B) = angle(C',A',B')`,
854 MESON_TAC[CONGRUENT_TRIANGLES_SSS; DIST_SYM; ANGLE_SYM;
855 CONGRUENT_TRIANGLES_SAS]);;
857 let CONGRUENT_TRIANGLES_AAS_FULL = prove
858 (`!A B C:real^M A' B' C':real^N.
859 angle(A,B,C) = angle(A',B',C') /\
860 angle(B,C,A) = angle(B',C',A') /\
861 dist(A,B) = dist(A',B') /\
863 ==> dist(A,B) = dist(A',B') /\
864 dist(B,C) = dist(B',C') /\
865 dist(C,A) = dist(C',A') /\
866 angle(A,B,C) = angle(A',B',C') /\
867 angle(B,C,A) = angle(B',C',A') /\
868 angle(C,A,B) = angle(C',A',B')`,
869 MESON_TAC[CONGRUENT_TRIANGLES_SSS; DIST_SYM; ANGLE_SYM;
870 CONGRUENT_TRIANGLES_AAS]);;
872 let CONGRUENT_TRIANGLES_ASA_FULL = prove
873 (`!A B C:real^M A' B' C':real^N.
874 angle(A,B,C) = angle(A',B',C') /\
875 dist(A,B) = dist(A',B') /\
876 angle(B,A,C) = angle(B',A',C') /\
878 ==> dist(A,B) = dist(A',B') /\
879 dist(B,C) = dist(B',C') /\
880 dist(C,A) = dist(C',A') /\
881 angle(A,B,C) = angle(A',B',C') /\
882 angle(B,C,A) = angle(B',C',A') /\
883 angle(C,A,B) = angle(C',A',B')`,
884 MESON_TAC[CONGRUENT_TRIANGLES_ASA; CONGRUENT_TRIANGLES_SAS_FULL;
885 DIST_SYM; ANGLE_SYM]);;
887 (* ------------------------------------------------------------------------- *)
889 (* ------------------------------------------------------------------------- *)
891 let ANGLE_BETWEEN = prove
892 (`!a b x. angle(a,x,b) = pi <=> ~(x = a) /\ ~(x = b) /\ between x (a,b)`,
893 REPEAT GEN_TAC THEN REWRITE_TAC[between; ANGLE_EQ_PI_DIST] THEN
894 REWRITE_TAC[EQ_SYM_EQ]);;
896 let BETWEEN_ANGLE = prove
897 (`!a b x. between x (a,b) <=> x = a \/ x = b \/ angle(a,x,b) = pi`,
898 REPEAT GEN_TAC THEN REWRITE_TAC[ANGLE_BETWEEN] THEN
899 MESON_TAC[BETWEEN_REFL]);;
901 let ANGLES_ALONG_LINE = prove
903 ~(C = A) /\ ~(C = B) /\ between C (A,B)
904 ==> angle(A,C,D) + angle(B,C,D) = pi`,
905 REPEAT GEN_TAC THEN REWRITE_TAC[GSYM ANGLE_BETWEEN] THEN
906 DISCH_THEN(SUBST1_TAC o MATCH_MP ANGLE_EQ_PI_LEFT) THEN REAL_ARITH_TAC);;
908 let ANGLES_ADD_BETWEEN = prove
910 between C (A,B) /\ ~(D = A) /\ ~(D = B)
911 ==> angle(A,D,C) + angle(C,D,B) = angle(A,D,B)`,
912 REPEAT GEN_TAC THEN ASM_CASES_TAC `A:real^N = B` THENL
913 [ASM_SIMP_TAC[BETWEEN_REFL_EQ] THEN
914 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
915 ASM_SIMP_TAC[ANGLE_REFL_MID; REAL_ADD_LID];
917 ASM_CASES_TAC `C:real^N = A` THEN
918 ASM_SIMP_TAC[ANGLE_REFL_MID; REAL_ADD_LID] THEN
919 ASM_CASES_TAC `C:real^N = B` THEN
920 ASM_SIMP_TAC[ANGLE_REFL_MID; REAL_ADD_RID] THEN
922 MP_TAC(ISPECL [`A:real^N`; `B:real^N`; `C:real^N`; `D:real^N`]
923 ANGLES_ALONG_LINE) THEN
924 MP_TAC(ISPECL [`A:real^N`; `B:real^N`; `D:real^N`] TRIANGLE_ANGLE_SUM) THEN
925 MP_TAC(ISPECL [`A:real^N`; `C:real^N`; `D:real^N`] TRIANGLE_ANGLE_SUM) THEN
926 MP_TAC(ISPECL [`B:real^N`; `C:real^N`; `D:real^N`] TRIANGLE_ANGLE_SUM) THEN
927 ASM_REWRITE_TAC[] THEN
928 SUBGOAL_THEN `angle(C:real^N,A,D) = angle(B,A,D) /\
929 angle(A,B,D) = angle(C,B,D)`
930 (CONJUNCTS_THEN SUBST1_TAC)
931 THENL [ALL_TAC; REWRITE_TAC[ANGLE_SYM] THEN REAL_ARITH_TAC] THEN
932 CONJ_TAC THEN MATCH_MP_TAC ANGLE_EQ_0_RIGHT THEN
933 ASM_MESON_TAC[ANGLE_EQ_PI_OTHERS; BETWEEN_ANGLE]);;