(* ========================================================================== *)
(* 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;;