(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(*                                                                            *)
(* Chapter: Trigonometry                                                             *)
(* Author: John Harrison                                                    *)
(* Date: 2011-07-01                                                           *)
(* ========================================================================== *)

(* ========================================================================= *)
(* A missing lemma from the trig chapter.                                    *)
(* ========================================================================= *)

module Hvihvec = struct

let VECTOR_ANGLE_DOUBLECROSS = 
prove (`!u v w. ~(w = vec 0) /\ u dot w = &0 /\ v dot w = &0 ==> vector_angle (u cross w) (v cross w) = vector_angle u v`,
REPEAT GEN_TAC THEN ASM_CASES_TAC `u:real^3 = vec 0` THENL [ASM_REWRITE_TAC[vector_angle; CROSS_0]; ALL_TAC] THEN ASM_CASES_TAC `v:real^3 = vec 0` THENL [ASM_REWRITE_TAC[vector_angle; CROSS_0]; ALL_TAC] THEN STRIP_TAC THEN SUBGOAL_THEN `~(u cross w = vec 0) /\ ~(v cross w = vec 0)` ASSUME_TAC THENL [REPEAT(POP_ASSUM MP_TAC) THEN REWRITE_TAC[GSYM DOT_EQ_0] THEN VEC3_TAC; ALL_TAC] THEN ASM_SIMP_TAC[VECTOR_ANGLE_EQ] THEN SIMP_TAC[vector_norm; GSYM SQRT_MUL; DOT_POS_LE] THEN ASM_REWRITE_TAC[DOT_CROSS; REAL_MUL_LZERO; REAL_SUB_RZERO] THEN REWRITE_TAC[REAL_ARITH `(x * y) * (z * y):real = (y * y) * x * z`] THEN SIMP_TAC[SQRT_MUL; DOT_POS_LE; REAL_LE_SQUARE; REAL_LE_MUL] THEN SIMP_TAC[SQRT_POW_2; DOT_POS_LE; GSYM REAL_POW_2] THEN REAL_ARITH_TAC);;
let HVIHVEC = 
prove (`!v0 v1 v2 v3. ~(v0 = v1) ==> dihV v0 v1 v2 v3 = let w1 = v1 - v0 and w2 = v2 - v0 and w3 = v3 - v0 in vector_angle (w1 cross w2) (w1 cross w3)`,
let lemma = prove  
   (`(v1 dot v1) % v2 - (v2 dot v1) % v1 = (v1 cross v2) cross v1`,VEC3_TAC) in
  REPEAT GEN_TAC THEN CONV_TAC(ONCE_DEPTH_CONV let_CONV) THEN
  GEN_GEOM_ORIGIN_TAC `v0:real^3` [] THEN
  REWRITE_TAC[dihV] THEN CONV_TAC(TOP_DEPTH_CONV let_CONV) THEN
  REWRITE_TAC[VECTOR_SUB_RZERO] THEN
  REWRITE_TAC[ARCV_ANGLE; angle; VECTOR_SUB_RZERO] THEN
  REWRITE_TAC[lemma] THEN
  REPEAT STRIP_TAC THEN MATCH_MP_TAC VECTOR_ANGLE_DOUBLECROSS THEN
  ASM_REWRITE_TAC[] THEN VEC3_TAC);;
end;;