1 (* ========================================================================== *)
\r
2 (* FLYSPECK - BOOK FORMALIZATION *)
\r
4 (* Chapter: Trigonometry *)
\r
5 (* Author: Jason Rute, Thomas C. Hales *)
\r
6 (* Date: 2010-02-09 *)
\r
7 (* ========================================================================== *)
\r
13 module type Trigonometry1_type = sig
\r
19 Formal Proofs Blueprint Chapter on Trigonometry
\r
20 some proofs copied from John Harrison.
\r
23 flyspeck_needs "general/sphere.hl";;
\r
26 module Trigonometry1 (* : Trigonometry1_type *) = struct
\r
28 let atn2 = Sphere.atn2;;
\r
29 let arclength = Sphere.arclength;;
\r
30 let ups_x = Sphere.ups_x;;
\r
35 (* This is close to CIRCLE_SINCOS *)
\r
37 let atn2_spec_t = `!x y. ?r. ((-- pi < atn2(x, y)) /\ (atn2(x,y) <= pi) /\
\r
38 (x = r* (cos(atn2(x,y)))) /\ (y = r* (sin (atn2( x, y)))) /\
\r
41 let acs_atn2_t = `!y. (-- &1 <= y /\ y <= &1) ==> (acs y = pi/(&2) - atn2(sqrt(&1 - y pow 2),y))`;;
\r
43 let arcVarc_t = `!u v w:real^3. ~(u=v) /\ ~(u=w) ==> arcV u v w = arclength (dist( u, v)) (dist( u, w)) (dist( v, w))`;;
\r
45 let law_of_cosines_t = `!a b c. (&0 < a) /\ (&0 < b) /\ (&0 <= c) /\ (c <= a + b) /\ (a <= b + c) /\ (b <= c + a) ==>
\r
46 ((c pow 2) = (a pow 2) + (b pow 2) - &2 * a * b * (cos(arclength a b c)))`;;
\r
48 let law_of_sines_t = `!a b c. (&0 < a) /\ (&0 < b) /\ (&0 <= c) /\ (c <= a + b) /\ (a <= b + c) /\ (b <= c + a) ==>
\r
49 (&2 * a * b * sin (arclength a b c) = sqrt(ups_x (a pow 2) (b pow 2) (c pow 2)))`;;
\r
51 let cross_mag_t = `!u v. norm (u cross v) = (norm u) * (norm v) * sin(arcV (vec 0) u v)`;;
\r
53 let cross_skew_t = `!u v. (u cross v) = -- (v cross u)`;;
\r
55 let cross_triple_t = `!u v w. (u cross v) dot w = (v cross w) dot u`;;
\r
58 (* law of cosines *)
\r
60 let spherical_loc_t = `!v0 va vb vc:real^3.
\r
61 ~(collinear {v0,va,vc}) /\ ~(collinear {v0,vb,vc}) ==>
\r
63 let gamma = dihV v0 vc va vb in
\r
64 let a = arcV v0 vb vc in
\r
65 let b = arcV v0 va vc in
\r
66 let c = arcV v0 va vb in
\r
67 (cos(gamma) = (cos(c) - cos(a)*cos(b))/(sin(a)*sin(b))))`;;
\r
69 let spherical_loc2_t = `!v0 va vb vc:real^3.
\r
70 ~(collinear {v0,va,vc}) /\ ~(collinear {v0,vb,vc}) ==>
\r
72 let alpha = dihV v0 va vb vc in
\r
73 let beta = dihV v0 vb va vc in
\r
74 let gamma = dihV v0 vc vb va in
\r
75 let c = arcV v0 va vb in
\r
76 (cos(c) = (cos(gamma) + cos(alpha)*cos(beta))/(sin(alpha)*sin(beta))))`;;
\r
78 let dih_formula_t = `!v0 v1 v2 v3:real^3.
\r
79 ~(collinear {v0,v1,v2}) /\ ~(collinear {v0,v1,v3}) ==>
\r
81 let (x1,x2,x3,x4,x5,x6) = xlist v0 v1 v2 v3 in
\r
82 (dihV v0 v1 v2 v3 = dih_x x1 x2 x3 x4 x5 x6)
\r
85 let dih_x_acs_t = `!x1 x2 x3 x4 x5 x6.
\r
86 (&0 < ups_x x1 x2 x6) /\ (&0 < ups_x x1 x3 x5) /\ (&0 <= delta_x x1 x2 x3 x4 x5 x6) /\ (&0 <= x1) ==>
\r
87 dih_x x1 x2 x3 x4 x5 x6 = acs ((delta_x4 x1 x2 x3 x4 x5 x6)/
\r
88 ((sqrt (ups_x x1 x2 x6)) * (sqrt (ups_x x1 x3 x5))))`;;
\r
90 let beta_cone_t = `!v0 v1 v2 v3:real^3.
\r
91 ~(collinear {v0,v1,v2}) /\ ~(collinear {v0,v1,v3}) /\
\r
92 (dihV v0 v3 v1 v2 = pi/(&2)) ==>
\r
93 (dihV v0 v1 v2 v3 = beta (arcV v0 v1 v3) (arcV v0 v1 v2))`;;
\r
95 let euler_triangle_t = `!v0 v1 v2 v3:real^3.
\r
96 let p = euler_p v0 v1 v2 v3 in
\r
97 let (x1,x2,x3,x4,x5,x6) = xlist v0 v1 v2 v3 in
\r
98 let alpha1 = dihV v0 v1 v2 v3 in
\r
99 let alpha2 = dihV v0 v2 v3 v1 in
\r
100 let alpha3 = dihV v0 v3 v1 v2 in
\r
101 let d = delta_x x1 x2 x3 x4 x5 x6 in
\r
103 (alpha1 + alpha2 + alpha3 - pi = pi - &2 * atn2(sqrt(d), (&2 * p))))`;;
\r
105 let polar_cycle_rotate_t = `!V psi u f.
\r
106 (!x y. f (x,y) = (x*cos psi + y*sin psi, -- x*sin psi + y*cos psi)) /\
\r
107 FINITE V /\ V u ==>
\r
108 (polar_cycle (IMAGE f V) (f u) = f (polar_cycle V u))`;;
\r
110 let thetaij_t = `!theta1 theta2 k12 k21 theta12 theta21.
\r
111 (&0 <= theta1) /\ (theta1 < &2 * pi) /\ (&0 <= theta2) /\ (theta2 < &2 * pi) /\
\r
112 (theta12 = theta2 - theta1 + &2 * pi * (&k12)) /\
\r
113 (theta21 = theta1 - theta2 + &2 * pi * (&k21)) /\
\r
114 (&0 <= theta12) /\ (theta12 < &2 * pi) /\
\r
115 (&0 <= theta21) /\ (theta21 < &2 * pi) ==>
\r
116 ((theta12+theta21) = (if (theta1=theta2) then (&0) else (&2 * pi)))`;;
\r
118 (* JMR: Changed `polar_angle (FST u) (SND u)` to `Arg(complex u)` *)
\r
120 let thetapq_wind_t = `!W n thetapq kpq.
\r
121 (!x y. (W (x,y) ==> (~(x= &0) /\ ~(y = &0)))) /\
\r
123 (!u v. W u /\ W v ==>
\r
124 ((thetapq u v = Arg(complex v) - Arg(complex u) + &2 * pi * kpq u v) /\ (&0 <= thetapq u v) /\ (thetapq u v < &2 * pi)))
\r
126 ((!u i j. (W u /\ (0 <= i) /\ (i <= j) /\ (j < n)) ==>
\r
127 thetapq u (ITER i (polar_cycle W) u) + thetapq (ITER i (polar_cycle W) u) (ITER j (polar_cycle W) u) = thetapq u (ITER j (polar_cycle W) u)) /\
\r
128 ((!u v. (W u /\ W v) ==> (Arg(complex u) = Arg(complex v))) \/
\r
129 (!u. (W u) ==> (sum(0 .. n-1) (\i. thetapq (ITER i (polar_cycle W) u) (ITER (SUC i) (polar_cycle W) u)) = &2 * pi)) ))`;;
\r
131 let zenith_t = `!u v w:real^3. ~(u=v) /\ ~(w = v) ==>
\r
133 (phi = arcV v u w) /\ (r = dist( u, v)) /\ ((dist( w, v)) % e3 = (w-v)) /\
\r
134 ( u' dot e3 = &0) /\ (u = v + u' + (r*cos(phi)) % e3))`;;
\r
136 (* spherical_coord_t deprecated, replaced with Harrison's SPHERICAL_COORDINATES theorem,
\r
137 which is worded slightly differently.
\r
140 let polar_coord_zenith_t = `!u v w u' n.
\r
141 ~(collinear {u,v,w}) /\ (aff {u,v,w} u') /\ ~(u' = v) /\
\r
142 (n = (w - v) cross (u - v)) ==>
\r
143 (arcV v (v + n) u' = pi/ (&2))`;;
\r
145 let azim_pair_t = `!v w w1 w2.
\r
146 let a1 = azim v w w1 w2 in
\r
147 let a2 = azim v w w2 w1 in
\r
148 (cyclic_set {w1,w2} v w) ==>
\r
149 (a1 + a2 = (if (a1 = &0) then (&0) else (&2 * pi)))`;;
\r
151 let azim_cycle_sum_t = `!W v w n.
\r
152 (cyclic_set W v w) /\
\r
154 (!p i j. (W p /\ (0 <= i) /\ (i <= j) /\ (j < n)) ==>
\r
155 ((!q. W q ==> (azim v w p q = &0) ) \/
\r
156 (sum(0 .. n-1) (\i. azim v w (ITER i (azim_cycle W v w) p) (ITER (SUC i) (azim_cycle W v w) p)) = &2 * pi )))`;;
\r
158 let dih_azim_t = `!v w v1 v2.
\r
159 ~(collinear {v,w,v1}) /\ ~(collinear {v,w,v2}) ==>
\r
160 (cos(azim v w v1 v2) = cos(dihV v w v1 v2))`;;
\r
162 let sph_triangle_ineq_t = `!p u v w:real^3.
\r
163 ~(collinear {p,u,w}) /\ ~(collinear {p,u,v}) /\ ~(collinear {p,v,w}) ==>
\r
164 (arcV p u w <= arcV p u v + arcV p v w)`;;
\r
166 let sph_triangle_ineq_sum_t = `!p:real^3 u r.
\r
167 (!i. (i < r) ==> ~(collinear {p,u i, u (SUC i)})) /\
\r
168 ~(collinear {p,u 0, u r}) ==>
\r
169 (arcV p (u 0) (u r) <= sum(0 .. r-1) (\i. arcV p (u i) (u (SUC i))))`;;
\r
171 let azim_t = `!v w w1 w2 e1 e2 e3.
\r
173 ~collinear {v, w, w1} /\
\r
174 ~collinear {v, w, w2} /\
\r
175 orthonormal e1 e2 e3 /\
\r
176 (dist( w, v) % e3 = w - v)
\r
177 ==> &0 <= azim v w w1 w2 /\
\r
178 azim v w w1 w2 < &2 * pi /\
\r
182 (r1 * cos psi) % e1 + (r1 * sin psi) % e2 + h1 % (w - v) /\
\r
184 (r2 * cos (psi + azim v w w1 w2)) % e1 +
\r
185 (r2 * sin (psi + azim v w w1 w2)) % e2 +
\r
188 (* signature for trig theorems.
\r
189 This is the list of theorems that should be provided by
\r
190 an implementation of the blueprint on trig.
\r
191 The signature can be extended, but care needs to made
\r
192 in removing anything, because it may create incompatibilities
\r
193 with other pieces of code. *)
\r
195 (* In every case, there is a term giving the precise theorem to
\r
199 module type Trigsig = sig
\r
200 val atn2_spec : thm (* atn2_spec_t *)
\r
201 val acs_atn2: thm (* acs_atn2_t *)
\r
202 val arcVarc : thm (* arcVarc_t *)
\r
203 val law_of_cosines : thm (* law_of_cosines_t *)
\r
204 val law_of_sines : thm (* law_of_sines_t *)
\r
205 val cross_mag : thm (* cross_mag_t *)
\r
206 val cross_skew : thm (* cross_skew_t *)
\r
207 val cross_triple : thm (* cross_triple_t *)
\r
208 val spherical_loc : thm (* spherical_loc_t *)
\r
209 val spherical_loc2 : thm (* spherical_loc2_t *)
\r
210 val dih_formula : thm (* dih_formula_t *)
\r
211 val dih_x_acs : thm (* dih_x_acs_t *)
\r
212 val beta_cone : thm (* beta_cone_t *)
\r
213 val euler_triangle : thm (* euler_triangle_t *)
\r
214 (* val polar_coords : thm (* polar_coords_t *) *)
\r
215 val polar_cycle_rotate : thm (* polar_cycle_rotate_t *)
\r
216 val thetaij : thm (* thetaij_t *)
\r
217 val thetapq_wind : thm (* thetapq_wind_t *)
\r
218 val zenith : thm (* zenith_t *)
\r
219 (* val spherical_coord : thm (* spherical_coord_t *) *)
\r
220 val polar_coord_zenith : thm (* polar_coord_zenith_t *)
\r
221 val azim_pair : thm (* azim_pair_t *)
\r
222 val azim_cycle_sum : thm (* azim_cycle_sum_t *)
\r
223 val dih_azim : thm (* dih_azim_t *)
\r
224 val sph_triangle_ineq : thm (* sph_triangle_ineq_t *)
\r
225 val sph_triangle_ineq_sum : thm (* sph_triangle_ineq_sum_t *)
\r
226 val azim : thm (* azim_t *)
\r
229 (* Here is a single axiom that permits a quick implementation of the
\r
230 module with the given signature.
\r
231 The axiom can be used so that the proofs in different chapters can
\r
232 proceed independently. *)
\r
235 let trig_term_list = new_definition (mk_eq (`trig_term:bool`, (list_mk_conj
\r
251 polar_cycle_rotate_t ;
\r
255 polar_coord_zenith_t ;
\r
259 sph_triangle_ineq_t ;
\r
260 sph_triangle_ineq_sum_t ;
\r
266 (* ---------------------------------------------------------------------- *)
\r
267 (* These are theorems proved in HOL Light, but not in the *)
\r
268 (* Multivariate files. Unless noted, all proofs by John Harrison. *)
\r
269 (* ---------------------------------------------------------------------- *)
\r
271 (* REAL_LE_POW_2 is in HOL-Light Examples/transc.ml. *)
\r
272 (* Also called REAL_LE_SQUARE_POW in Examples/analysis.ml. *)
\r
274 let REAL_LE_POW_2 = prove
\r
275 (`!x. &0 <= x pow 2`,
\r
276 REWRITE_TAC[REAL_POW_2; REAL_LE_SQUARE]);;
\r
278 (* REAL_DIV_MUL2 is in HOL-Light Examples/analysis.ml. *)
\r
279 (* Proof in now trivial *)
\r
281 let REAL_DIV_MUL2 = REAL_FIELD
\r
282 `!x z. ~(x = &0) /\ ~(z = &0) ==> !y. y / z = (x * y) / (x * z)`;;
\r
284 (* ---------------------------------------------------------------------- *)
\r
285 (* Useful theorems about real numbers. *)
\r
286 (* ---------------------------------------------------------------------- *)
\r
288 let REAL_LT_MUL_3 = prove
\r
289 (`!x y z. &0 < x /\ &0 < y /\ &0 < z ==> &0 < x * y * z`,
\r
290 REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_LT_MUL THEN ASM_REWRITE_TAC [] THEN
\r
291 MATCH_MP_TAC REAL_LT_MUL THEN ASM_REWRITE_TAC []);;
\r
293 let SQRT_MUL_L = prove
\r
294 (`!x y. &0 <= x /\ &0 <= y ==> x * sqrt y = sqrt(x pow 2 * y)`,
\r
295 REPEAT STRIP_TAC THEN ASM_SIMP_TAC [REAL_LE_POW_2; SQRT_MUL; POW_2_SQRT]);;
\r
297 let SQRT_MUL_R = prove
\r
298 (`!x y. &0 <= x /\ &0 <= y ==> sqrt x * y = sqrt(x * y pow 2)`,
\r
299 REPEAT STRIP_TAC THEN ASM_SIMP_TAC [REAL_LE_POW_2; SQRT_MUL; POW_2_SQRT]);;
\r
301 (* ---------------------------------------------------------------------- *)
\r
302 (* Basic trig results not included in Examples/transc.ml *)
\r
303 (* ---------------------------------------------------------------------- *)
\r
305 (* Next two proofs similar to TAN_PERIODIC_NPI in *)
\r
306 (* Examples/transc.ml by John Harrison *)
\r
307 (* They are no longer needed, but may be useful later. *)
\r
309 let SIN_PERIODIC_N2PI = prove
\r
310 (`!x n. sin(x + &n * (&2 * pi)) = sin(x)`,
\r
311 GEN_TAC THEN INDUCT_TAC THEN REWRITE_TAC[REAL_MUL_LZERO; REAL_ADD_RID] THEN
\r
312 REWRITE_TAC[GSYM REAL_OF_NUM_SUC; REAL_ADD_RDISTRIB; REAL_MUL_LID] THEN
\r
313 ASM_REWRITE_TAC[REAL_ADD_ASSOC; SIN_PERIODIC]);;
\r
315 let COS_PERIODIC_N2PI = prove
\r
316 (`!x n. cos(x + &n * (&2 * pi)) = cos(x)`,
\r
317 GEN_TAC THEN INDUCT_TAC THEN REWRITE_TAC[REAL_MUL_LZERO; REAL_ADD_RID] THEN
\r
318 REWRITE_TAC[GSYM REAL_OF_NUM_SUC; REAL_ADD_RDISTRIB; REAL_MUL_LID] THEN
\r
319 ASM_REWRITE_TAC[REAL_ADD_ASSOC; COS_PERIODIC]);;
\r
321 let CIRCLE_SINCOS_PI = prove
\r
322 (`!x y. (x pow 2 + y pow 2 = &1) ==>
\r
323 ?t. (--pi < t /\ t <= pi) /\ ((x = cos(t)) /\ (y = sin(t)))`,
\r
324 ASM_MESON_TAC [CIRCLE_SINCOS; SINCOS_PRINCIPAL_VALUE]);;
\r
326 let SIN_NEGPOS_PI = prove
\r
327 (`!x. (--pi < x /\ x <= pi) ==>
\r
328 (sin x < &0 <=> --pi < x /\ x < &0) /\
\r
329 (sin x = &0 <=> (x = &0 \/ x = pi)) /\
\r
330 (&0 < sin x <=> &0 < x /\ x < pi)`,
\r
331 STRIP_TAC THEN STRIP_TAC THEN SUBGOAL_THEN
\r
332 `if (sin x < &0) then (sin x < &0 <=> --pi < x /\ x < &0) else
\r
333 if (sin x = &0) then (sin x = &0 <=> (x = &0 \/ x = pi)) else
\r
334 (&0 < sin x <=> &0 < x /\ x < pi)` MP_TAC THENL
\r
335 [ SUBGOAL_TAC "a" `--pi < x /\ x < &0 ==> sin x < &0`
\r
336 [ MP_TAC (REWRITE_RULE [SIN_NEG] (SPEC `--x:real` SIN_POS_PI)) THEN
\r
337 REAL_ARITH_TAC ] THEN
\r
338 SUBGOAL_TAC "b" `x = &0 ==> sin x = &0`
\r
339 [ STRIP_TAC THEN ASM_REWRITE_TAC [SIN_0] ] THEN
\r
340 SUBGOAL_TAC "c" `x = pi ==> sin x = &0`
\r
341 [ STRIP_TAC THEN ASM_REWRITE_TAC [SIN_PI] ] THEN
\r
342 LABEL_TAC "d" (SPEC `x:real` SIN_POS_PI) THEN
\r
343 REPEAT (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC;
\r
344 REPEAT (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC ]);;
\r
346 let COS_NEGPOS_PI = prove
\r
347 (`!x. (--pi < x /\ x <= pi) ==>
\r
348 (cos x < &0 <=> (--pi < x /\ x < --(pi / &2)) \/
\r
349 (pi / &2 < x /\ x <= pi)) /\
\r
350 (cos x = &0 <=> (x = --(pi / &2) \/ x = pi / &2)) /\
\r
351 (&0 < cos x <=> --(pi / &2) < x /\ x < pi / &2)`,
\r
352 STRIP_TAC THEN STRIP_TAC THEN SUBGOAL_THEN
\r
353 `if (cos x < &0) then (cos x < &0 <=> (--pi < x /\ x < --(pi / &2)) \/
\r
354 (pi / &2 < x /\ x <= pi)) else
\r
355 if (cos x = &0) then
\r
356 (cos x = &0 <=> (x = --(pi / &2) \/ x = pi / &2)) else
\r
357 (&0 < cos x <=> --(pi / &2) < x /\ x < pi / &2)` MP_TAC THENL
\r
358 [ SUBGOAL_TAC "a" `--pi < x /\ x < --(pi / &2) ==> cos x < &0`
\r
359 [ MP_TAC (REWRITE_RULE [COS_PERIODIC_PI]
\r
360 (SPEC `x + pi:real` COS_POS_PI2)) THEN
\r
361 REAL_ARITH_TAC ] THEN
\r
362 SUBGOAL_TAC "b" `pi / &2 < x /\ x <= pi ==> cos x < &0`
\r
363 [ MP_TAC (REWRITE_RULE [SIN_NEG; GSYM COS_SIN]
\r
364 (SPEC `--(pi / &2 - x)` SIN_POS_PI2)) THEN
\r
365 SUBGOAL_TAC "b1" `x = pi ==> cos x < &0`
\r
366 [ STRIP_TAC THEN ASM_REWRITE_TAC [COS_PI; REAL_ARITH `&0 < &1`] THEN
\r
367 REAL_ARITH_TAC ] THEN
\r
368 POP_ASSUM MP_TAC THEN REAL_ARITH_TAC ] THEN
\r
369 SUBGOAL_TAC "c" `x = --(pi / &2) ==> cos x = &0`
\r
370 [ STRIP_TAC THEN ASM_REWRITE_TAC [COS_NEG; COS_PI2] ] THEN
\r
371 SUBGOAL_TAC "d" `x = pi / &2 ==> cos x = &0`
\r
372 [ STRIP_TAC THEN ASM_REWRITE_TAC [COS_PI2] ] THEN
\r
373 LABEL_TAC "e" (SPEC `x:real` COS_POS_PI) THEN
\r
374 REPEAT (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC;
\r
375 REPEAT (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC ]);;
\r
378 (* ----------------------------------------------------------------------- *)
\r
379 (* Theory of atan_2 function. See sphere.hl for the definiton. *)
\r
380 (* ----------------------------------------------------------------------- *)
\r
382 (* lemma:atn2_spec *)
\r
384 let dist_lemma = prove
\r
385 (`!x y. ~(x = &0) \/ ~(y = &0) ==>
\r
386 (x / sqrt(x pow 2 + y pow 2)) pow 2 +
\r
387 (y / sqrt(x pow 2 + y pow 2)) pow 2 = &1 /\
\r
388 &0 < sqrt(x pow 2 + y pow 2)`,
\r
389 STRIP_TAC THEN STRIP_TAC THEN STRIP_TAC THEN
\r
390 SUBGOAL_TAC "sum_pos" `&0 < x pow 2 + y pow 2 /\ &0 <= x pow 2 + y pow 2`
\r
391 [ MP_TAC (SPEC `x:real` REAL_LE_POW_2) THEN
\r
392 MP_TAC (SPEC `y:real` REAL_LE_POW_2) THEN
\r
393 IMP_RES_THEN MP_TAC (SPECL [`x:real`; `2`] REAL_POW_NZ) THEN
\r
394 IMP_RES_THEN MP_TAC (SPECL [`y:real`; `2`] REAL_POW_NZ) THEN
\r
395 REAL_ARITH_TAC ] THEN
\r
396 POP_ASSUM MP_TAC THEN STRIP_TAC THEN
\r
397 ASM_SIMP_TAC [REAL_POW_DIV; SQRT_POW_2; SQRT_POS_LT] THEN
\r
398 POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN
\r
399 CONV_TAC REAL_FIELD);;
\r
401 let ATAN2_EXISTS = prove
\r
402 (`!x y. ?t. (--pi < t /\ t <= pi) /\
\r
403 x = sqrt(x pow 2 + y pow 2) * cos t /\
\r
404 y = sqrt(x pow 2 + y pow 2) * sin t`,
\r
405 REPEAT STRIP_TAC THEN ASM_CASES_TAC `(x = &0) /\ (y = &0)` THENL
\r
406 [ ASM_REWRITE_TAC [(SPEC `2` REAL_POW_ZERO)] THEN
\r
407 NUM_REDUCE_TAC THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
\r
408 REWRITE_TAC [SQRT_0] THEN EXISTS_TAC `pi` THEN MP_TAC PI_POS THEN
\r
410 IMP_RES_THEN STRIP_ASSUME_TAC
\r
411 (REWRITE_RULE [TAUT `(~A \/ ~B) <=> ~(A /\ B)`] dist_lemma) THEN
\r
412 IMP_RES_THEN STRIP_ASSUME_TAC CIRCLE_SINCOS_PI THEN
\r
413 POP_ASSUM (MP_TAC o GSYM) THEN POP_ASSUM (MP_TAC o GSYM) THEN
\r
414 STRIP_TAC THEN STRIP_TAC THEN EXISTS_TAC `t:real` THEN
\r
415 ASM_REWRITE_TAC [] THEN
\r
416 POP_ASSUM (K ALL_TAC) THEN POP_ASSUM (K ALL_TAC) THEN
\r
417 POP_ASSUM (K ALL_TAC) THEN POP_ASSUM (K ALL_TAC) THEN
\r
418 POP_ASSUM MP_TAC THEN CONV_TAC REAL_FIELD ]);;
\r
420 (* The official Kepler definition (atn2) is different, but it was easier *)
\r
421 (* to start with this one and prove it is equivalent. *)
\r
423 let ATAN2_TEMP_DEF = new_definition
\r
424 `atan2_temp (x,y) = if (x = &0 /\ y = &0)
\r
426 else @t. (--pi < t /\ t <= pi) /\
\r
427 x = sqrt(x pow 2 + y pow 2) * cos t /\
\r
428 y = sqrt(x pow 2 + y pow 2) * sin t`;;
\r
430 let ATAN2_TEMP = prove
\r
431 (`!x y. (--pi < atan2_temp (x,y) /\ atan2_temp (x,y) <= pi) /\
\r
432 x = sqrt(x pow 2 + y pow 2) * cos (atan2_temp (x,y)) /\
\r
433 y = sqrt(x pow 2 + y pow 2) * sin (atan2_temp (x,y))`,
\r
434 STRIP_TAC THEN STRIP_TAC THEN REWRITE_TAC [ATAN2_TEMP_DEF] THEN
\r
435 COND_CASES_TAC THENL
\r
436 [ ASM_REWRITE_TAC [(SPEC `2` REAL_POW_ZERO)] THEN
\r
437 NUM_REDUCE_TAC THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
\r
438 REWRITE_TAC [SQRT_0] THEN MP_TAC PI_POS THEN
\r
440 REWRITE_TAC [(SELECT_RULE (SPECL [`x:real`;`y:real`] ATAN2_EXISTS))]]);;
\r
442 let ATAN2_TEMP_SPEC = prove
\r
443 (`!x y. ?r. ((-- pi < atan2_temp(x, y)) /\ (atan2_temp(x,y) <= pi) /\
\r
444 (x = r* (cos(atan2_temp(x,y)))) /\ (y = r* (sin (atan2_temp( x, y)))) /\
\r
446 STRIP_TAC THEN STRIP_TAC THEN EXISTS_TAC `sqrt(x pow 2 + y pow 2)` THEN
\r
447 REWRITE_TAC [ATAN2_TEMP] THEN SUBGOAL_TAC "sum_pos" `&0 <= x pow 2 + y pow 2`
\r
448 [ MP_TAC (SPEC `x:real` REAL_LE_POW_2) THEN
\r
449 MP_TAC (SPEC `y:real` REAL_LE_POW_2) THEN
\r
450 REAL_ARITH_TAC ] THEN
\r
451 MP_TAC (SPEC `x pow 2 + y pow 2` SQRT_POS_LE) THEN POP_ASSUM MP_TAC THEN
\r
454 let ATAN2_TEMP_BREAKDOWN = prove
\r
455 (`!x y. (&0 < x ==> atan2_temp(x,y) = atn(y / x)) /\
\r
456 (&0 < y ==> atan2_temp(x,y) = pi / &2 - atn(x / y)) /\
\r
457 (y < &0 ==> atan2_temp(x,y) = --(pi / &2) - atn(x / y)) /\
\r
458 (y = &0 /\ x <= &0 ==> atan2_temp(x,y) = pi)`,
\r
459 REPEAT GEN_TAC THEN REPEAT CONJ_TAC THENL
\r
460 [ STRIP_ASSUME_TAC (SPECL [`x:real`;`y:real`] ATAN2_TEMP) THEN
\r
461 ABBREV_TAC `t = atan2_temp (x,y)` THEN
\r
462 ABBREV_TAC `r = sqrt (x pow 2 + y pow 2)` THEN STRIP_TAC THEN
\r
463 SUBGOAL_TAC "r_pos" `&0 < r`
\r
464 [ EXPAND_TAC "r" THEN MP_TAC (SPECL [`x:real`;`y:real`] dist_lemma) THEN
\r
465 POP_ASSUM MP_TAC THEN REAL_ARITH_TAC] THEN
\r
466 SUBGOAL_TAC "tan" `(r * sin t) / (r * cos t) = tan t`
\r
467 [ REWRITE_TAC [tan] THEN POP_ASSUM MP_TAC THEN CONV_TAC REAL_FIELD ] THEN
\r
468 ASM_REWRITE_TAC [] THEN MATCH_MP_TAC (GSYM TAN_ATN) THEN
\r
469 POP_ASSUM (K ALL_TAC) THEN
\r
470 POP_ASSUM (fun th -> POP_ASSUM MP_TAC THEN ASSUME_TAC th) THEN
\r
471 ASM_SIMP_TAC [GSYM COS_NEGPOS_PI; REAL_LT_MUL_EQ] THEN REAL_ARITH_TAC ;
\r
473 STRIP_ASSUME_TAC (SPECL [`x:real`;`y:real`] ATAN2_TEMP) THEN
\r
474 ABBREV_TAC `t = atan2_temp (x,y)` THEN
\r
475 ABBREV_TAC `r = sqrt (x pow 2 + y pow 2)` THEN STRIP_TAC THEN
\r
476 SUBGOAL_TAC "r_pos" `&0 < r`
\r
477 [ EXPAND_TAC "r" THEN MP_TAC (SPECL [`x:real`;`y:real`] dist_lemma) THEN
\r
478 POP_ASSUM MP_TAC THEN REAL_ARITH_TAC] THEN
\r
479 SUBGOAL_TAC "tan" `(r * cos t) / (r * sin t) = inv (tan t)`
\r
480 [ REWRITE_TAC [tan] THEN POP_ASSUM MP_TAC THEN
\r
481 CONV_TAC REAL_FIELD ] THEN
\r
482 ASM_REWRITE_TAC [GSYM TAN_COT] THEN
\r
483 SUBGOAL_THEN `pi / &2 - t = atn (tan (pi / &2 - t))`
\r
484 (fun th -> REWRITE_TAC [GSYM th] THEN REAL_ARITH_TAC) THEN
\r
485 MATCH_MP_TAC (GSYM TAN_ATN) THEN
\r
486 SUBGOAL_THEN `&0 < t /\ t < pi`
\r
487 (fun th -> MP_TAC th THEN REAL_ARITH_TAC) THEN
\r
488 POP_ASSUM (K ALL_TAC) THEN
\r
489 POP_ASSUM (fun th -> POP_ASSUM MP_TAC THEN ASSUME_TAC th) THEN
\r
490 ASM_SIMP_TAC [GSYM SIN_NEGPOS_PI; REAL_LT_MUL_EQ] THEN REAL_ARITH_TAC ;
\r
492 STRIP_ASSUME_TAC (SPECL [`x:real`;`y:real`] ATAN2_TEMP) THEN
\r
493 ABBREV_TAC `t = atan2_temp (x,y)` THEN
\r
494 ABBREV_TAC `r = sqrt (x pow 2 + y pow 2)` THEN STRIP_TAC THEN
\r
495 SUBGOAL_TAC "r_pos" `&0 < r`
\r
496 [ EXPAND_TAC "r" THEN MP_TAC (SPECL [`x:real`;`y:real`] dist_lemma) THEN
\r
497 POP_ASSUM MP_TAC THEN REAL_ARITH_TAC] THEN
\r
498 SUBGOAL_TAC "tan" `(r * cos t) / (r * sin t) = --inv (tan (--t))`
\r
499 [ REWRITE_TAC [TAN_NEG; REAL_INV_NEG] THEN
\r
500 REWRITE_TAC [tan; REAL_NEG_NEG] THEN
\r
501 POP_ASSUM MP_TAC THEN CONV_TAC REAL_FIELD ] THEN
\r
502 ASM_REWRITE_TAC [GSYM TAN_COT; ATN_NEG] THEN
\r
503 SUBGOAL_THEN `pi / &2 + t = atn (tan (pi / &2 + t))`
\r
504 (fun th -> REWRITE_TAC [REAL_ARITH `pi / &2 - --t = pi / &2 + t`;GSYM th]
\r
505 THEN REAL_ARITH_TAC) THEN
\r
506 MATCH_MP_TAC (GSYM TAN_ATN) THEN
\r
507 SUBGOAL_THEN `--pi < t /\ t < &0`
\r
508 (fun th -> MP_TAC th THEN REAL_ARITH_TAC) THEN
\r
509 POP_ASSUM (K ALL_TAC) THEN
\r
510 POP_ASSUM (fun th -> POP_ASSUM (MP_TAC o (REWRITE_RULE [GSYM REAL_NEG_GT0]))
\r
511 THEN ASSUME_TAC th) THEN
\r
512 ASM_SIMP_TAC [GSYM SIN_NEGPOS_PI; REAL_LT_MUL_EQ; REAL_NEG_RMUL] THEN
\r
515 ASM_CASES_TAC `x = &0` THENL
\r
516 [ STRIP_TAC THEN ASM_REWRITE_TAC [ATAN2_TEMP_DEF];
\r
518 STRIP_ASSUME_TAC (SPECL [`x:real`;`y:real`] ATAN2_TEMP) THEN
\r
519 ABBREV_TAC `t = atan2_temp (x,y)` THEN
\r
520 ABBREV_TAC `r = sqrt (x pow 2 + y pow 2)` THEN STRIP_TAC THEN
\r
521 SUBGOAL_TAC "r_pos" `&0 < r`
\r
522 [ EXPAND_TAC "r" THEN MP_TAC (SPECL [`x:real`;`y:real`] dist_lemma) THEN
\r
523 POP_ASSUM MP_TAC THEN FIND_ASSUM MP_TAC `~(x = &0)` THEN
\r
524 REAL_ARITH_TAC ] THEN
\r
525 SUBGOAL_TAC "sin_cos" `sin t = &0 /\ cos t < &0 ==> t = pi`
\r
526 [ ASM_SIMP_TAC [SIN_NEGPOS_PI; COS_NEGPOS_PI] THEN MP_TAC PI_POS THEN
\r
527 REAL_ARITH_TAC ] THEN
\r
528 POP_ASSUM MATCH_MP_TAC THEN
\r
529 SUBGOAL_TAC "x_pos" `&0 < --x`
\r
530 [ FIND_ASSUM MP_TAC `x <= &0` THEN FIND_ASSUM MP_TAC `~(x = &0)` THEN
\r
531 REAL_ARITH_TAC ] THEN
\r
532 POP_ASSUM MP_TAC THEN
\r
533 POP_ASSUM (fun th -> POP_ASSUM (K ALL_TAC) THEN POP_ASSUM MP_TAC THEN
\r
534 ASSUME_TAC th) THEN
\r
535 ASM_SIMP_TAC [REAL_LT_MUL_EQ; REAL_NEG_RMUL] THEN POP_ASSUM MP_TAC THEN
\r
536 CONV_TAC REAL_FIELD]);;
\r
538 let ATAN2_TEMP_ALT = prove
\r
539 (`!x y. atan2_temp (x,y) =
\r
540 if ( abs y < x ) then atn(y / x) else
\r
541 (if (&0 < y) then ((pi / &2) - atn(x / y)) else
\r
542 (if (y < &0) then (-- (pi/ &2) - atn (x / y)) else ( pi )))`,
\r
543 STRIP_TAC THEN STRIP_TAC THEN COND_CASES_TAC THENL
\r
544 [ SUBGOAL_THEN `&0 < x`
\r
545 (fun th -> SIMP_TAC [th; ATAN2_TEMP_BREAKDOWN]) THEN
\r
546 POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;
\r
547 COND_CASES_TAC THENL
\r
548 [ SUBGOAL_THEN `&0 < y`
\r
549 (fun th -> SIMP_TAC [th; ATAN2_TEMP_BREAKDOWN]) THEN
\r
550 POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;
\r
551 COND_CASES_TAC THENL
\r
552 [ SUBGOAL_THEN `y < &0`
\r
553 (fun th -> SIMP_TAC [th; ATAN2_TEMP_BREAKDOWN]) THEN
\r
554 POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;
\r
555 SUBGOAL_THEN `y = &0`
\r
556 (fun th -> POP_ASSUM (K ALL_TAC) THEN POP_ASSUM (K ALL_TAC) THEN
\r
557 ASSUME_TAC th) THENL
\r
558 [ POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN REAL_ARITH_TAC ;
\r
559 SUBGOAL_THEN `x <= &0`
\r
560 (fun th -> ASM_SIMP_TAC [th; ATAN2_TEMP_BREAKDOWN]) THEN
\r
561 POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN REAL_ARITH_TAC ]]]]);;
\r
563 (* Show that the working def and the official def are equivalent. *)
\r
565 let ATAN_TEMP_ATN2 = prove
\r
566 (`atn2 = atan2_temp`,
\r
567 REWRITE_TAC [FORALL_PAIR_THM; FUN_EQ_THM; atn2; ATAN2_TEMP_ALT]);;
\r
569 (* These three and the definition should suffice as the basic *)
\r
570 (* specifications for atn2. No more need for atan2_temp.*)
\r
572 let atn2_spec = prove
\r
574 REWRITE_TAC [ATAN_TEMP_ATN2; ATAN2_TEMP_SPEC]);;
\r
576 let ATN2_BREAKDOWN = prove
\r
577 (`!x y. (&0 < x ==> atn2 (x,y) = atn(y / x)) /\
\r
578 (&0 < y ==> atn2 (x,y) = pi / &2 - atn(x / y)) /\
\r
579 (y < &0 ==> atn2 (x,y) = --(pi / &2) - atn(x / y)) /\
\r
580 (y = &0 /\ x <= &0 ==> atn2(x,y) = pi)`,
\r
581 REWRITE_TAC [ATAN_TEMP_ATN2; ATAN2_TEMP_BREAKDOWN]);;
\r
583 let ATN2_CIRCLE = prove
\r
584 (`!x y. (--pi < atan2_temp (x,y) /\ atan2_temp (x,y) <= pi) /\
\r
585 x = sqrt(x pow 2 + y pow 2) * cos (atan2_temp (x,y)) /\
\r
586 y = sqrt(x pow 2 + y pow 2) * sin (atan2_temp (x,y))`,
\r
587 REWRITE_TAC [ATAN_TEMP_ATN2; ATAN2_TEMP]);;
\r
589 (* Useful properties of atn2. *)
\r
591 let ATN2_0_1 = prove
\r
592 (`atn2 (&0, &1) = pi / &2`,
\r
593 ASSUME_TAC (REAL_ARITH `&0 < &1`) THEN
\r
594 ASM_SIMP_TAC [ATN2_BREAKDOWN] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
\r
595 REWRITE_TAC [ATN_0] THEN REAL_ARITH_TAC);;
\r
597 let ATN2_0_NEG_1 = prove
\r
598 (`atn2 (&0, --(&1)) = --(pi / &2)`,
\r
599 ASSUME_TAC (REAL_ARITH `--(&1) < &0`) THEN
\r
600 ASM_SIMP_TAC [ATN2_BREAKDOWN] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
\r
601 REWRITE_TAC [ATN_0] THEN REAL_ARITH_TAC);;
\r
603 let ATN2_LMUL_EQ = prove
\r
604 (`!a x y. &0 < a ==> atn2(a * x, a * y) = atn2 (x, y)`,
\r
605 REPEAT STRIP_TAC THEN STRIP_ASSUME_TAC
\r
606 (REAL_ARITH `&0 < x \/ &0 < y \/ y < &0 \/ (y = &0 /\ x <= &0)`) THENL
\r
607 [ SUBGOAL_TAC "pos_x" `&0 < a * x`
\r
608 [ let th = SPECL [`&0`;`x:real`;`a:real`] REAL_LT_LMUL_EQ in
\r
609 let th2 = REWRITE_RULE [REAL_MUL_RZERO] th in
\r
610 ASM_SIMP_TAC [th2] ] ;
\r
611 SUBGOAL_TAC "pos_y" `&0 < a * y`
\r
612 [ let th = SPECL [`&0`;`y:real`;`a:real`] REAL_LT_LMUL_EQ in
\r
613 let th2 = REWRITE_RULE [REAL_MUL_RZERO] th in
\r
614 ASM_SIMP_TAC [th2] ] ;
\r
615 SUBGOAL_TAC "neg_y" `a * y < &0`
\r
616 [ let th = SPECL [`y:real`;`&0`;`a:real`] REAL_LT_LMUL_EQ in
\r
617 let th2 = REWRITE_RULE [REAL_MUL_RZERO] th in
\r
618 ASM_SIMP_TAC [th2] ] ;
\r
619 SUBGOAL_TAC "other" `a * y = &0 /\ a * x <= &0`
\r
620 [ ASM_REWRITE_TAC [REAL_MUL_RZERO] THEN
\r
621 let th = SPECL [`x:real`;`&0`;`a:real`] REAL_LE_LMUL_EQ in
\r
622 let th2 = REWRITE_RULE [REAL_MUL_RZERO] th in
\r
623 ASM_SIMP_TAC [th2] ] ] THEN
\r
624 let th1 = SPECL [`x:real`;`y:real`] ATN2_BREAKDOWN in
\r
625 let th2 = SPECL [`a * x:real`;`a * y:real`] ATN2_BREAKDOWN in
\r
626 let th3 = REAL_ARITH `!x. (x < &0 \/ &0 < x) ==> ~(&0 = x)` in
\r
627 ASM_SIMP_TAC [th1; th2; th3; GSYM (SPEC `a:real` REAL_DIV_MUL2)] );;
\r
629 let ATN2_RNEG = prove
\r
630 (`!x y. (~(y = &0) \/ &0 < x) ==> atn2(x,--y) = --(atn2(x,y))`,
\r
631 STRIP_TAC THEN STRIP_TAC THEN STRIP_ASSUME_TAC
\r
632 (REAL_ARITH `&0 < x \/ &0 < y \/ y < &0 \/ (y = &0 /\ x <= &0)`) THENL
\r
633 [ ASM_REWRITE_TAC [] ;
\r
634 ASM_SIMP_TAC [REAL_LT_IMP_NE] THEN SUBGOAL_TAC "neg" `--y < &0`
\r
635 [ ASM_REWRITE_TAC [REAL_NEG_LT0] ] ;
\r
636 ASM_SIMP_TAC [REAL_LT_IMP_NE] THEN SUBGOAL_TAC "pos" `&0 < --y`
\r
637 [ ASM_REWRITE_TAC [REAL_NEG_GT0] ] ;
\r
638 ASM_REWRITE_TAC [real_lt] ] THEN
\r
639 let th1 = SPECL [`x:real`;`y:real`] ATN2_BREAKDOWN in
\r
640 let th2 = SPECL [`x:real`;`--y:real`] ATN2_BREAKDOWN in
\r
641 let th3 = REAL_ARITH `(--x)/y = --(x/y)` in
\r
642 let th4 = REAL_FIELD `(y < &0 \/ &0 < y) ==> x / (--y) = --(x/y)` in
\r
643 ASM_SIMP_TAC [th1; th2; th3; th4; ATN_NEG] THEN REAL_ARITH_TAC);;
\r
645 (* lemma:acs_atn2 *)
\r
647 let acs_atn2 = prove
\r
649 STRIP_TAC THEN ASM_CASES_TAC `y = &1 \/ y = --(&1)` THENL
\r
650 [ POP_ASSUM DISJ_CASES_TAC THENL
\r
651 [ ASM_REWRITE_TAC [] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
\r
652 REWRITE_TAC [ACS_1; SQRT_0; ATN2_0_1] THEN REAL_ARITH_TAC ;
\r
653 ASM_REWRITE_TAC [] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
\r
654 REWRITE_TAC [ACS_NEG_1; SQRT_0; ATN2_0_NEG_1] THEN REAL_ARITH_TAC ] ;
\r
656 SUBGOAL_TAC "sqrt" `&0 < sqrt (&1 - y pow 2)`
\r
657 [ MATCH_MP_TAC SQRT_POS_LT THEN
\r
658 SUBGOAL_THEN `&0 <= y pow 2 /\ y pow 2 < &1`
\r
659 (fun th -> MP_TAC th THEN REAL_ARITH_TAC) THEN
\r
660 REWRITE_TAC [REAL_LE_POW_2; REAL_ARITH `a < &1 <=> a < &1 pow 2`;
\r
661 GSYM REAL_LT_SQUARE_ABS ] THEN
\r
662 REPEAT (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC ] THEN
\r
663 ASM_SIMP_TAC [ATN2_BREAKDOWN] THEN MATCH_MP_TAC ACS_ATN THEN
\r
664 REPEAT (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC ]);;
\r
666 (* ----------------------------------------------------------------------- *)
\r
667 (* Theory of triangles (without vectors). Includes laws of cosines/sines. *)
\r
668 (* ----------------------------------------------------------------------- *)
\r
670 let UPS_X_SQUARES = prove
\r
671 (`!a b c. ups_x (a * a) (b * b) (c * c) =
\r
672 &16 * ((a + b + c) / &2) *
\r
673 (((a + b + c) / &2) - a) *
\r
674 (((a + b + c) / &2) - b) *
\r
675 (((a + b + c) / &2) - c)`,
\r
676 REPEAT STRIP_TAC THEN REWRITE_TAC [ups_x] THEN REAL_ARITH_TAC);;
\r
678 (* Theorems assuming a, b, c are lengths of a triangle (c not 0). *)
\r
680 let TRI_UPS_X_POS = prove
\r
681 (`!a b c. (&0 < a) /\ (&0 < b) /\ (&0 <= c) /\ (c <= a + b) /\ (a <= b + c) /\ (b <= c + a) ==>
\r
682 &0 <= ups_x (a * a) (b * b) (c * c)`,
\r
683 REPEAT STRIP_TAC THEN REWRITE_TAC [UPS_X_SQUARES] THEN
\r
684 REPEAT (MATCH_MP_TAC REAL_LE_MUL THEN STRIP_TAC) THENL
\r
686 REPEAT (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC ;
\r
687 SUBGOAL_THEN `&2 * a <= a + b + c`
\r
688 (fun th -> MP_TAC th THEN REAL_ARITH_TAC) THEN
\r
689 REPEAT (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC ;
\r
690 SUBGOAL_THEN `&2 * b <= a + b + c`
\r
691 (fun th -> MP_TAC th THEN REAL_ARITH_TAC) THEN
\r
692 REPEAT (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC ;
\r
693 SUBGOAL_THEN `&2 * c <= a + b + c`
\r
694 (fun th -> MP_TAC th THEN REAL_ARITH_TAC) THEN
\r
695 REPEAT (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC ]);;
\r
697 let TRI_SQUARES_BOUNDS = prove
\r
698 (`!a b c. (&0 < a) /\ (&0 < b) /\ (&0 <= c) /\ (c <= a + b) /\ (a <= b + c) /\ (b <= c + a) ==>
\r
699 --(&1) <= ((a * a) + (b * b) - (c * c)) / (&2 * a * b) /\
\r
700 ((a * a) + (b * b) - (c * c)) / (&2 * a * b) <= &1`,
\r
701 REPEAT STRIP_TAC THEN
\r
702 SUBGOAL_TAC "2ab_pos" `&0 < &2 * a * b`
\r
703 [ ASM_SIMP_TAC [REAL_LT_MUL_3; REAL_ARITH `&0 < &2`] ] THENL
\r
704 [ SUBGOAL_TAC "abc_square" `c*c <= (a + b) * (a + b)`
\r
705 [ MATCH_MP_TAC (REWRITE_RULE [IMP_IMP] REAL_LE_MUL2) THEN
\r
706 REPEAT (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC ] THEN
\r
707 ASM_SIMP_TAC [REAL_LE_RDIV_EQ] THEN REMOVE_THEN "abc_square" MP_TAC THEN
\r
709 SUBGOAL_TAC "abc_square" `(a - b) * (a - b) <= c*c`
\r
710 [ DISJ_CASES_TAC (REAL_ARITH `a <= b \/ b <= a`) THENL
\r
711 [ SUBST1_TAC (REAL_ARITH `(a-b)*(a-b)=(b-a)*(b-a)`); ALL_TAC ] THEN
\r
712 MATCH_MP_TAC (REWRITE_RULE [IMP_IMP] REAL_LE_MUL2) THEN
\r
713 REPEAT (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC ] THEN
\r
714 ASM_SIMP_TAC [REAL_LE_LDIV_EQ] THEN REMOVE_THEN "abc_square" MP_TAC THEN
\r
715 REAL_ARITH_TAC ]);;
\r
717 let ATN2_ARCLENGTH = prove
\r
718 (`!a b c. (&0 < a) /\ (&0 < b) /\ (&0 <= c) /\ (c <= a + b) /\ (a <= b + c) /\ (b <= c + a) ==>
\r
719 arclength a b c = pi / &2 - atn2(sqrt(ups_x (a*a) (b*b) (c*c)), (a*a) + (b*b) - (c*c))`,
\r
720 REPEAT STRIP_TAC THEN
\r
721 let th = REAL_ARITH `c * c - a * a - b * b = --(a * a + b * b - c * c)` in
\r
722 REWRITE_TAC [arclength; th; ATN2_RNEG] THEN
\r
723 SUBGOAL_THEN `~(a * a + b * b - c * c = &0) \/
\r
724 &0 < sqrt(ups_x (a*a) (b*b) (c*c))`
\r
725 (fun th -> ASM_SIMP_TAC [th; ATN2_RNEG] THEN
\r
726 REAL_ARITH_TAC) THEN
\r
727 REWRITE_TAC [TAUT `(~A \/ B) <=> (A ==> B)`] THEN STRIP_TAC THEN
\r
728 SUBGOAL_TAC "c_ab" `c*c = a*a + b*b`
\r
729 [ POP_ASSUM MP_TAC THEN REAL_ARITH_TAC ] THEN
\r
730 REMOVE_THEN "c_ab" (fun th -> REWRITE_TAC [ups_x; th]) THEN
\r
731 MATCH_MP_TAC SQRT_POS_LT THEN
\r
732 CONV_TAC (DEPTH_BINOP_CONV `(<)` REAL_POLY_CONV) THEN
\r
733 MATCH_MP_TAC REAL_LT_MUL_3 THEN STRIP_TAC THENL
\r
735 ASM_SIMP_TAC [REAL_POW_LT] ]);;
\r
737 let TRI_LEMMA = prove
\r
738 (`!a b c. (&0 < a) /\ (&0 < b) /\ (&0 <= c) /\ (c <= a + b) /\ (a <= b + c) /\ (b <= c + a) ==>
\r
739 (&2 * a * b) * (a * a + b * b - c * c) / (&2 * a * b) =
\r
740 a * a + b * b - c * c`,
\r
741 REPEAT STRIP_TAC THEN
\r
742 SUBGOAL_TAC "2ab_pos" `&0 < &2 * a * b`
\r
743 [ ASM_SIMP_TAC [REAL_LT_MUL_3; REAL_ARITH `&0 < &2`] ] THEN
\r
744 SUBGOAL_TAC "2ab_not0" `~(&2 * a * b = &0)`
\r
745 [ POP_ASSUM MP_TAC THEN REAL_ARITH_TAC ] THEN
\r
746 ASM_SIMP_TAC [REAL_DIV_LMUL]);;
\r
748 let TRI_UPS_X_SQUARES = prove
\r
749 (`!a b c. (&0 < a) /\ (&0 < b) /\ (&0 <= c) /\ (c <= a + b) /\ (a <= b + c) /\ (b <= c + a) ==>
\r
750 ups_x (a * a) (b * b) (c * c) =
\r
751 (&2 * a * b) pow 2 * (&1 - ((a * a + b * b - c * c) / (&2 * a * b)) pow 2)`,
\r
752 REPEAT STRIP_TAC THEN
\r
753 ASM_SIMP_TAC [ups_x; REAL_SUB_LDISTRIB; GSYM REAL_POW_MUL; TRI_LEMMA] THEN
\r
756 let TRI_UPS_X_SQRT = prove
\r
757 (`!a b c. (&0 < a) /\ (&0 < b) /\ (&0 <= c) /\ (c <= a + b) /\ (a <= b + c) /\ (b <= c + a) ==>
\r
758 sqrt(ups_x (a * a) (b * b) (c * c)) =
\r
759 (&2 * a * b) * sqrt(&1 - ((a * a + b * b - c * c) / (&2 * a * b)) pow 2)`,
\r
760 REPEAT STRIP_TAC THEN
\r
761 SUBGOAL_TAC "2ab_pos" `&0 < &2 * a * b`
\r
762 [ ASM_SIMP_TAC [REAL_LT_MUL_3; REAL_ARITH `&0 < &2`] ] THEN
\r
763 SUBGOAL_TAC "other_pos" `&0 <= &1 - ((a * a + b * b - c * c) / (&2 * a * b)) pow 2`
\r
764 [ SUBGOAL_THEN `((a * a + b * b - c * c) / (&2 * a * b)) pow 2 <= &1`
\r
765 (fun th -> MP_TAC th THEN REAL_ARITH_TAC) THEN
\r
766 ASM_SIMP_TAC [ABS_SQUARE_LE_1; REAL_ABS_BOUNDS; TRI_SQUARES_BOUNDS] ] THEN
\r
767 ASM_SIMP_TAC [SQRT_MUL_L; REAL_LT_IMP_LE; TRI_UPS_X_SQUARES] );;
\r
769 let ACS_ARCLENGTH = prove
\r
770 (`!a b c. (&0 < a) /\ (&0 < b) /\ (&0 <= c) /\ (c <= a + b) /\ (a <= b + c) /\ (b <= c + a) ==>
\r
771 arclength a b c = acs (((a * a) + (b * b) - (c * c)) / (&2 * a * b))`,
\r
772 REPEAT STRIP_TAC THEN ASM_SIMP_TAC [ATN2_ARCLENGTH; TRI_SQUARES_BOUNDS; acs_atn2] THEN
\r
773 SUBGOAL_TAC "2ab_pos" `&0 < &2 * a * b`
\r
774 [ ASM_SIMP_TAC [REAL_LT_MUL_3; REAL_ARITH `&0 < &2`] ] THEN
\r
776 `(sqrt (ups_x (a * a) (b * b) (c * c)), a * a + b * b - c * c) =
\r
777 ((&2 * a * b) * sqrt (&1 - ((a * a + b * b - c * c) / (&2 * a * b)) pow 2),
\r
778 (&2 * a * b) * ((a * a + b * b - c * c) / (&2 * a * b)))`
\r
779 (fun th -> ASM_SIMP_TAC [ATN2_LMUL_EQ; th]) THEN
\r
780 ASM_SIMP_TAC [TRI_UPS_X_SQRT; TRI_LEMMA]);;
\r
782 let law_of_cosines = prove
\r
784 REPEAT STRIP_TAC THEN
\r
785 REWRITE_TAC [REAL_ARITH `&2 * a * b * x = (&2 * a * b) * x`] THEN
\r
786 ASM_SIMP_TAC [ACS_ARCLENGTH; TRI_SQUARES_BOUNDS; COS_ACS; TRI_LEMMA] THEN
\r
789 let law_of_sines = prove
\r
791 REPEAT STRIP_TAC THEN
\r
792 REWRITE_TAC [REAL_ARITH `&2 * a * b * x = (&2 * a * b) * x`;
\r
793 REAL_ARITH `x pow 2 = x * x` ] THEN
\r
794 ASM_SIMP_TAC [ACS_ARCLENGTH; TRI_SQUARES_BOUNDS; SIN_ACS; TRI_UPS_X_SQRT]);;
\r
796 (* ----------------------------------------------------------------------- *)
\r
797 (* Cross product properties. *)
\r
798 (* ----------------------------------------------------------------------- *)
\r
800 let DIST_TRIANGLE_DETAILS = prove
\r
801 (`~(u = v) /\ ~(u = w) <=>
\r
802 &0 < dist(u,v) /\ &0 < dist(u,w) /\
\r
804 dist(v,w) <= dist(u,v) + dist(u,w) /\
\r
805 dist(u,v) <= dist(u,w) + dist(v,w) /\
\r
806 dist(u,w) <= dist(v,w) + dist(u,v)`,
\r
809 let arcVarc = prove
\r
811 SIMP_TAC [DIST_TRIANGLE_DETAILS; arcV; ACS_ARCLENGTH] THEN
\r
812 REPEAT STRIP_TAC THEN AP_TERM_TAC THEN
\r
813 REWRITE_TAC [DOT_NORM_NEG; dist] THEN
\r
814 let tha = NORM_ARITH `norm (v - u) = norm (u - v)` in
\r
815 let thb = NORM_ARITH `norm (w - u) = norm (u - w)` in
\r
816 let thc = NORM_ARITH `norm (v - u - (w - u)) = norm (v - w)` in
\r
817 REWRITE_TAC [tha; thb; thc] THEN CONV_TAC REAL_FIELD);;
\r
819 let DIST_LAW_OF_COS = prove
\r
820 (`(dist(v:real^3,w)) pow 2 = (dist(u,v)) pow 2 + (dist(u,w)) pow 2 -
\r
821 &2 * (dist(u,v)) * (dist(u,w)) * cos (arcV u v w)`,
\r
822 ASM_CASES_TAC `~(u = v:real^3) /\ ~(u = w)` THEN POP_ASSUM MP_TAC THENL
\r
823 [ ASM_SIMP_TAC [arcVarc] THEN
\r
824 REWRITE_TAC [law_of_cosines; DIST_TRIANGLE_DETAILS];
\r
825 REWRITE_TAC [TAUT `~(~A /\ ~B) <=> (A \/ B)`] THEN STRIP_TAC THEN
\r
826 ASM_REWRITE_TAC [DIST_REFL; DIST_SYM] THEN REAL_ARITH_TAC]);;
\r
828 let DIST_L_ZERO = prove
\r
829 (`!v. dist(vec 0, v) = norm v`,
\r
832 (* I would like to change this to real^N but that means changing arcV to real^N *)
\r
834 let DOT_COS = prove
\r
835 (`u:real^3 dot v = (norm u) * (norm v) * cos (arcV (vec 0) u v)`,
\r
836 MP_TAC (INST [`vec 0:real^3`,`u:real^3`;
\r
837 `u:real^3`,`v:real^3`;
\r
838 `v:real^3`,`w:real^3`] DIST_LAW_OF_COS) THEN
\r
840 `dist(u:real^3,v) pow 2 =
\r
841 dist(vec 0, v) pow 2 + dist(vec 0, u) pow 2 - &2 * u dot v`
\r
842 (fun th -> REWRITE_TAC [th; DIST_L_ZERO] THEN REAL_ARITH_TAC) THEN
\r
843 REWRITE_TAC [NORM_POW_2; dist; DOT_RSUB; DOT_LSUB;
\r
844 DOT_SYM; DOT_LZERO; DOT_RZERO] THEN
\r
847 (* DIMINDEX_3, FORALL_3, SUM_3, DOT_3, VECTOR_3, FORALL_VECTOR_3 *)
\r
848 (* are all very useful. Any time you see a theorem you need with *)
\r
849 (* 1 <= i /\ i <= dimindex(:3), first use INST_TYPE and then rewrite *)
\r
850 (* with DIMINDEX_3 and FORALL_3 or see if it's in the list below. *)
\r
852 let CART_EQ_3 = prove
\r
853 (`!x y. (x:A^3) = y <=> x$1 = y$1 /\ x$2 = y$2 /\ x$3 = y$3`,
\r
854 REWRITE_TAC [CART_EQ; DIMINDEX_3; FORALL_3]);;
\r
856 let LAMBDA_BETA_3 = prove
\r
857 (`((lambda) g:A^3) $1 = g 1 /\
\r
858 ((lambda) g:A^3) $2 = g 2 /\
\r
859 ((lambda) g:A^3) $3 = g 3`,
\r
860 let th = REWRITE_RULE [DIMINDEX_3; FORALL_3]
\r
861 (INST_TYPE [`:3`,`:B`] LAMBDA_BETA) in
\r
862 REWRITE_TAC [th]);;
\r
864 let VEC_COMPONENT_3 = prove
\r
865 (`!k. (vec k :real^3)$1 = &k /\
\r
866 (vec k :real^3)$2 = &k /\
\r
867 (vec k :real^3)$3 = &k`,
\r
868 let th = REWRITE_RULE [DIMINDEX_3; FORALL_3]
\r
869 (INST_TYPE [`:3`,`:N`] VEC_COMPONENT) in
\r
870 REWRITE_TAC [th]);;
\r
872 let VECTOR_ADD_COMPONENT_3 = prove
\r
873 (`!x:real^3 y. (x + y)$1 = x$1 + y$1 /\
\r
874 (x + y)$2 = x$2 + y$2 /\
\r
875 (x + y)$3 = x$3 + y$3`,
\r
876 let th = REWRITE_RULE [DIMINDEX_3; FORALL_3]
\r
877 (INST_TYPE [`:3`,`:N`] VECTOR_ADD_COMPONENT) in
\r
878 REWRITE_TAC [th]);;
\r
880 let VECTOR_SUB_COMPONENT_3 = prove
\r
881 (`!x:real^3 y. (x - y)$1 = x$1 - y$1 /\
\r
882 (x - y)$2 = x$2 - y$2 /\
\r
883 (x - y)$3 = x$3 - y$3`,
\r
884 let th = REWRITE_RULE [DIMINDEX_3; FORALL_3]
\r
885 (INST_TYPE [`:3`,`:N`] VECTOR_SUB_COMPONENT) in
\r
886 REWRITE_TAC [th]);;
\r
888 let VECTOR_NEG_COMPONENT_3 = prove
\r
889 (`!x:real^3. (--x)$1 = --(x$1) /\
\r
890 (--x)$2 = --(x$2) /\
\r
891 (--x)$3 = --(x$3)`,
\r
892 let th = REWRITE_RULE [DIMINDEX_3; FORALL_3]
\r
893 (INST_TYPE [`:3`,`:N`] VECTOR_NEG_COMPONENT) in
\r
894 REWRITE_TAC [th]);;
\r
896 let VECTOR_MUL_COMPONENT_3 = prove
\r
897 (`!c x:real^3. (c % x)$1 = c * x$1 /\
\r
898 (c % x)$2 = c * x$2 /\
\r
899 (c % x)$3 = c * x$3`,
\r
900 let th = REWRITE_RULE [DIMINDEX_3; FORALL_3]
\r
901 (INST_TYPE [`:3`,`:N`] VECTOR_MUL_COMPONENT) in
\r
902 REWRITE_TAC [th]);;
\r
904 (* COND_COMPONENT_3 - no need, COND_COMPONENT works fine. *)
\r
906 let BASIS_3 = prove
\r
907 (`(basis 1:real^3)$1 = &1 /\ (basis 1:real^3)$2 = &0 /\ (basis 1:real^3)$3 = &0 /\
\r
908 (basis 2:real^3)$1 = &0 /\ (basis 2:real^3)$2 = &1 /\ (basis 2:real^3)$3 = &0 /\
\r
909 (basis 3:real^3)$1 = &0 /\ (basis 3:real^3)$2 = &0 /\ (basis 3:real^3)$3 = &1`,
\r
910 REWRITE_TAC [basis;
\r
911 REWRITE_RULE [DIMINDEX_3; FORALL_3]
\r
912 (INST_TYPE [`:3`,`:B`] LAMBDA_BETA)] THEN
\r
915 let COMPONENTS_3 = prove
\r
916 (`!v. v:real^3 = v$1 % basis 1 + v$2 % basis 2 + v$3 % basis 3`,
\r
917 REWRITE_TAC [CART_EQ_3; VECTOR_ADD_COMPONENT_3;
\r
918 VECTOR_MUL_COMPONENT_3; BASIS_3] THEN REAL_ARITH_TAC);;
\r
920 let VECTOR_COMPONENTS_3 = prove
\r
921 (`!a b c. vector [a;b;c]:real^3 = a % basis 1 + b % basis 2 + c % basis 3`,
\r
922 let th = REWRITE_RULE [VECTOR_3]
\r
923 (ISPEC `vector [a;b;c]:real^3` COMPONENTS_3) in
\r
924 REWRITE_TAC [th]);;
\r
926 let cross_skew = prove
\r
928 REWRITE_TAC [CART_EQ_3; CROSS_COMPONENTS; VECTOR_NEG_COMPONENT_3] THEN
\r
931 let cross_triple = prove
\r
933 REWRITE_TAC [ DOT_3; CROSS_COMPONENTS] THEN REAL_ARITH_TAC);;
\r
935 let NORM_CAUCHY_SCHWARZ_FRAC = prove
\r
936 (`!(u:real^N) v. ~(u = vec 0) /\ ~(v = vec 0) ==>
\r
937 -- &1 <= (u dot v) / (norm u * norm v) /\
\r
938 (u dot v) / (norm u * norm v) <= &1`,
\r
939 REPEAT STRIP_TAC THEN
\r
940 SUBGOAL_TAC "norm_pos" `&0 < norm (u:real^N) * norm (v:real^N)`
\r
941 [ POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN
\r
942 SIMP_TAC [GSYM NORM_POS_LT; IMP_IMP; REAL_LT_MUL] ] THEN
\r
943 MP_TAC (SPECL [`u:real^N`;`v:real^N`] NORM_CAUCHY_SCHWARZ_ABS) THEN
\r
944 ASM_SIMP_TAC [REAL_ABS_BOUNDS; REAL_LE_RDIV_EQ; REAL_LE_LDIV_EQ] THEN
\r
947 let CROSS_LZERO = prove
\r
948 (`!x. (vec 0) cross x = vec 0`,
\r
949 REWRITE_TAC [CART_EQ_3; CROSS_COMPONENTS; VEC_COMPONENT_3] THEN
\r
952 let CROSS_RZERO = prove
\r
953 (`!x. x cross (vec 0) = vec 0`,
\r
954 REWRITE_TAC [CART_EQ_3; CROSS_COMPONENTS; VEC_COMPONENT_3] THEN
\r
957 let CROSS_SQUARED = prove
\r
958 (`!u v. (u cross v) dot (u cross v) =
\r
959 (ups_x (u dot u) (v dot v) ((u - v) dot (u - v))) / &4`,
\r
960 REWRITE_TAC [DOT_3; CROSS_COMPONENTS; ups_x; VECTOR_SUB_COMPONENT_3] THEN
\r
963 let DIST_UPS_X_POS = prove
\r
964 (`~(u = v) /\ ~(u = w) ==>
\r
965 &0 <= ups_x (dist(u,v) pow 2) (dist(u,w) pow 2) (dist(v,w) pow 2)`,
\r
966 REWRITE_TAC [DIST_TRIANGLE_DETAILS; TRI_UPS_X_POS; REAL_POW_2]);;
\r
968 let SQRT_DIV_R = prove
\r
969 (`&0 <= x /\ &0 <= y ==> sqrt (x) / y = sqrt (x/ (y pow 2)) /\ &0 <= x/(y pow 2)`,
\r
970 SIMP_TAC [SQRT_DIV; REAL_LE_POW_2; POW_2_SQRT; REAL_LE_DIV]);;
\r
972 let NORM_CROSS = prove
\r
973 (`!u v. ~(vec 0 = u) /\ ~(vec 0 = v) ==>
\r
974 norm (u cross v) =
\r
975 sqrt (ups_x ((norm u) pow 2)
\r
977 ((dist(u,v)) pow 2)) / &2`,
\r
978 REPEAT GEN_TAC THEN DISCH_TAC THEN IMP_RES_THEN MP_TAC DIST_UPS_X_POS THEN
\r
979 REWRITE_TAC [DIST_L_ZERO] THEN
\r
980 SIMP_TAC[SQRT_DIV_R; REAL_ARITH `&0 <= &2`; REAL_ARITH `&2 pow 2 = &4`] THEN
\r
981 DISCH_TAC THEN MATCH_MP_TAC (GSYM SQRT_UNIQUE) THEN
\r
982 REWRITE_TAC [dist; NORM_POW_2; CROSS_SQUARED] THEN NORM_ARITH_TAC);;
\r
984 let VECTOR_LAW_OF_SINES = prove
\r
985 (`~(vec 0 = u:real^3) /\ ~(vec 0 = v) ==>
\r
986 &2 * (norm u) * (norm v) * sin (arcV (vec 0) u v) =
\r
987 sqrt (ups_x (norm u pow 2) (norm v pow 2) (dist (u,v) pow 2))`,
\r
988 SIMP_TAC [arcVarc; DIST_TRIANGLE_DETAILS; law_of_sines; DIST_L_ZERO]);;
\r
990 let cross_mag = prove
\r
992 REPEAT STRIP_TAC THEN
\r
993 REWRITE_TAC [arcVarc; VECTOR_SUB_RZERO] THEN
\r
994 ASM_CASES_TAC `(u:real^3) = vec 0 \/ (v:real^3) = vec 0` THENL
\r
995 [ POP_ASSUM STRIP_ASSUME_TAC THEN
\r
996 ASM_REWRITE_TAC [CROSS_LZERO; CROSS_RZERO; NORM_0] THEN REAL_ARITH_TAC ;
\r
997 POP_ASSUM MP_TAC THEN
\r
998 REWRITE_TAC [DE_MORGAN_THM; MESON [] `a = vec 0 <=> vec 0 = a`] THEN
\r
999 SIMP_TAC [NORM_CROSS; GSYM VECTOR_LAW_OF_SINES] THEN REAL_ARITH_TAC ]);;
\r