1 (* ========================================================================== *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
4 (* Chapter: Trigonometry *)
5 (* Author: John Harrison *)
7 (* ========================================================================== *)
9 (* ========================================================================= *)
10 (* A missing lemma from the trig chapter. *)
11 (* ========================================================================= *)
13 module Hvihvec = struct
15 let VECTOR_ANGLE_DOUBLECROSS = prove
17 ~(w = vec 0) /\ u dot w = &0 /\ v dot w = &0
18 ==> vector_angle (u cross w) (v cross w) = vector_angle u v`,
19 REPEAT GEN_TAC THEN ASM_CASES_TAC `u:real^3 = vec 0` THENL
20 [ASM_REWRITE_TAC[vector_angle; CROSS_0]; ALL_TAC] THEN
21 ASM_CASES_TAC `v:real^3 = vec 0` THENL
22 [ASM_REWRITE_TAC[vector_angle; CROSS_0]; ALL_TAC] THEN
24 SUBGOAL_THEN `~(u cross w = vec 0) /\ ~(v cross w = vec 0)` ASSUME_TAC THENL
25 [REPEAT(POP_ASSUM MP_TAC) THEN REWRITE_TAC[GSYM DOT_EQ_0] THEN VEC3_TAC;
27 ASM_SIMP_TAC[VECTOR_ANGLE_EQ] THEN
28 SIMP_TAC[vector_norm; GSYM SQRT_MUL; DOT_POS_LE] THEN
29 ASM_REWRITE_TAC[DOT_CROSS; REAL_MUL_LZERO; REAL_SUB_RZERO] THEN
30 REWRITE_TAC[REAL_ARITH `(x * y) * (z * y):real = (y * y) * x * z`] THEN
31 SIMP_TAC[SQRT_MUL; DOT_POS_LE; REAL_LE_SQUARE; REAL_LE_MUL] THEN
32 SIMP_TAC[SQRT_POW_2; DOT_POS_LE; GSYM REAL_POW_2] THEN REAL_ARITH_TAC);;
37 ==> dihV v0 v1 v2 v3 =
41 vector_angle (w1 cross w2) (w1 cross w3)`,
43 (`(v1 dot v1) % v2 - (v2 dot v1) % v1 = (v1 cross v2) cross v1`,VEC3_TAC) in
44 REPEAT GEN_TAC THEN CONV_TAC(ONCE_DEPTH_CONV let_CONV) THEN
45 GEN_GEOM_ORIGIN_TAC `v0:real^3` [] THEN
46 REWRITE_TAC[dihV] THEN CONV_TAC(TOP_DEPTH_CONV let_CONV) THEN
47 REWRITE_TAC[VECTOR_SUB_RZERO] THEN
48 REWRITE_TAC[ARCV_ANGLE; angle; VECTOR_SUB_RZERO] THEN
49 REWRITE_TAC[lemma] THEN
50 REPEAT STRIP_TAC THEN MATCH_MP_TAC VECTOR_ANGLE_DOUBLECROSS THEN
51 ASM_REWRITE_TAC[] THEN VEC3_TAC);;