text_formalization/trigonometry/HVIHVEC.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Chapter: Trigonometry                                                             *)
   5 (* Author: John Harrison                                                    *)
   6 (* Date: 2011-07-01                                                           *)
   7 (* ========================================================================== *)
   8
   9 (* ========================================================================= *)
  10 (* A missing lemma from the trig chapter.                                    *)
  11 (* ========================================================================= *)
  12
  13 module Hvihvec = struct
  14
  15 let VECTOR_ANGLE_DOUBLECROSS = prove
  16  (`!u v w.
  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
  23   STRIP_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;
  26     ALL_TAC] THEN
  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);;
  33
  34 let HVIHVEC = prove
  35  (`!v0 v1 v2 v3.
  36         ~(v0 = v1)
  37         ==> dihV v0 v1 v2 v3 =
  38             let w1 = v1 - v0
  39             and w2 = v2 - v0
  40             and w3 = v3 - v0 in
  41             vector_angle (w1 cross w2) (w1 cross w3)`,
  42   let lemma = prove
  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);;
  52
  53 end;;