100/cosine.ml

   1 (* ========================================================================= *)
   2 (* The law of cosines, of sines, and sum of angles of a triangle.            *)
   3 (* ========================================================================= *)
   4
   5 needs "Multivariate/transcendentals.ml";;
   6
   7 prioritize_vector();;
   8
   9 (* ------------------------------------------------------------------------- *)
  10 (* Angle between vectors (always 0 <= angle <= pi).                          *)
  11 (* ------------------------------------------------------------------------- *)
  12
  13 let vangle = new_definition
  14  `vangle x y = if x = vec 0 \/ y = vec 0 then pi / &2
  15                else acs((x dot y) / (norm x * norm y))`;;
  16
  17 (* ------------------------------------------------------------------------- *)
  18 (* Traditional geometric notion of angle (but always 0 <= theta <= pi).      *)
  19 (* ------------------------------------------------------------------------- *)
  20
  21 let angle = new_definition
  22  `angle(a,b,c) = vangle (a - b) (c - b)`;;
  23
  24 (* ------------------------------------------------------------------------- *)
  25 (* Lemmas (more than we need for this result).                               *)
  26 (* ------------------------------------------------------------------------- *)
  27
  28 let VANGLE = prove
  29  (`!x y:real^N. x dot y = norm(x) * norm(y) * cos(vangle x y)`,
  30   REPEAT GEN_TAC THEN REWRITE_TAC[vangle] THEN
  31   ASM_CASES_TAC `x:real^N = vec 0` THEN
  32   ASM_REWRITE_TAC[DOT_LZERO; NORM_0; REAL_MUL_LZERO] THEN
  33   ASM_CASES_TAC `y:real^N = vec 0` THEN
  34   ASM_REWRITE_TAC[DOT_RZERO; NORM_0; REAL_MUL_LZERO; REAL_MUL_RZERO] THEN
  35   ONCE_REWRITE_TAC[AC REAL_MUL_AC `a * b * c:real = c * a * b`] THEN
  36   ASM_SIMP_TAC[GSYM REAL_EQ_LDIV_EQ; REAL_LT_MUL; NORM_POS_LT] THEN
  37   MATCH_MP_TAC(GSYM COS_ACS) THEN
  38   ASM_SIMP_TAC[REAL_LE_RDIV_EQ; REAL_LE_LDIV_EQ; NORM_POS_LT; REAL_LT_MUL] THEN
  39   MP_TAC(SPECL [`x:real^N`; `y:real^N`] NORM_CAUCHY_SCHWARZ_ABS) THEN
  40   REAL_ARITH_TAC);;
  41
  42 let VANGLE_RANGE = prove
  43  (`!x y:real^N. &0 <= vangle x y /\ vangle x y <= pi`,
  44   REPEAT GEN_TAC THEN REWRITE_TAC[vangle] THEN COND_CASES_TAC THENL
  45    [MP_TAC PI_POS THEN REAL_ARITH_TAC; ALL_TAC] THEN
  46   RULE_ASSUM_TAC(REWRITE_RULE[DE_MORGAN_THM]) THEN MATCH_MP_TAC ACS_BOUNDS THEN
  47   ASM_SIMP_TAC[REAL_LE_RDIV_EQ; REAL_LE_LDIV_EQ; REAL_LT_MUL; NORM_POS_LT] THEN
  48   MATCH_MP_TAC(REAL_ARITH `abs(x) <= a ==> -- &1 * a <= x /\ x <= &1 * a`) THEN
  49   REWRITE_TAC[NORM_CAUCHY_SCHWARZ_ABS]);;
  50
  51 let ORTHOGONAL_VANGLE = prove
  52  (`!x y:real^N. orthogonal x y <=> vangle x y = pi / &2`,
  53   REPEAT STRIP_TAC THEN REWRITE_TAC[orthogonal; vangle] THEN
  54   ASM_CASES_TAC `x:real^N = vec 0` THEN ASM_REWRITE_TAC[DOT_LZERO] THEN
  55   ASM_CASES_TAC `y:real^N = vec 0` THEN ASM_REWRITE_TAC[DOT_RZERO] THEN
  56   EQ_TAC THENL
  57    [SIMP_TAC[real_div; REAL_MUL_LZERO] THEN DISCH_TAC THEN
  58     REWRITE_TAC[GSYM real_div; GSYM COS_PI2] THEN
  59     MATCH_MP_TAC ACS_COS THEN MP_TAC PI_POS THEN REAL_ARITH_TAC;
  60     MP_TAC(SPECL [`x:real^N`; `y:real^N`] NORM_CAUCHY_SCHWARZ_ABS) THEN
  61     GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [GSYM REAL_MUL_LID] THEN
  62     REWRITE_TAC[GSYM REAL_BOUNDS_LE] THEN
  63     ONCE_REWRITE_TAC[GSYM REAL_MUL_LNEG] THEN
  64     ASM_SIMP_TAC[GSYM REAL_LE_RDIV_EQ; GSYM REAL_LE_LDIV_EQ;
  65                  REAL_LT_MUL; NORM_POS_LT] THEN
  66     STRIP_TAC THEN DISCH_THEN(MP_TAC o AP_TERM `cos`) THEN
  67     ASM_SIMP_TAC[COS_ACS; COS_PI2] THEN
  68     REWRITE_TAC[real_div; REAL_ENTIRE; REAL_INV_EQ_0] THEN
  69     ASM_REWRITE_TAC[NORM_EQ_0]]);;
  70
  71 let VANGLE_EQ_PI = prove
  72  (`!x y:real^N. vangle x y = pi ==> norm(x) % y + norm(y) % x = vec 0`,
  73   REPEAT STRIP_TAC THEN
  74   MP_TAC(SPECL [`x:real^N`; `y:real^N`] VANGLE) THEN
  75   ASM_REWRITE_TAC[COS_PI] THEN STRIP_TAC THEN
  76   MP_TAC(ISPECL [`x:real^N`; `--y:real^N`] NORM_CAUCHY_SCHWARZ_EQ) THEN
  77   REWRITE_TAC[NORM_NEG; DOT_RNEG; VECTOR_MUL_RNEG] THEN
  78   ASM_REWRITE_TAC[REAL_MUL_RNEG; REAL_NEG_NEG; REAL_MUL_RID] THEN
  79   VECTOR_ARITH_TAC);;
  80
  81 let ANGLE_EQ_PI = prove
  82  (`!A B C:real^N. angle(A,B,C) = pi ==> dist(A,C) = dist(A,B) + dist(B,C)`,
  83   REPEAT GEN_TAC THEN REWRITE_TAC[angle] THEN
  84   DISCH_THEN(MP_TAC o MATCH_MP VANGLE_EQ_PI) THEN
  85   REWRITE_TAC[VECTOR_ARITH `a + x % (b - c) = vec 0 <=> a = x % (c - b)`] THEN
  86   GEN_REWRITE_TAC (funpow 3 LAND_CONV) [NORM_SUB] THEN
  87   REWRITE_TAC[GSYM NORM_TRIANGLE_EQ] THEN
  88   REWRITE_TAC[VECTOR_ARITH `(B - A) + (C - B):real^N = C - A`] THEN
  89   REWRITE_TAC[dist; NORM_SUB]);;
  90
  91 let SIN_ANGLE_POS = prove
  92  (`!A B C. &0 <= sin(angle(A,B,C))`,
  93   SIMP_TAC[SIN_POS_PI_LE; angle; VANGLE_RANGE]);;
  94
  95 let ANGLE = prove
  96  (`!A B C. (A - C) dot (B - C) = dist(A,C) * dist(B,C) * cos(angle(A,C,B))`,
  97   REWRITE_TAC[angle; dist; GSYM VANGLE]);;
  98
  99 let ANGLE_REFL = prove
 100  (`!A B. angle(A,A,B) = pi / &2 /\
 101          angle(B,A,A) = pi / &2`,
 102   REWRITE_TAC[angle; vangle; VECTOR_SUB_REFL]);;
 103
 104 let ANGLE_REFL_MID = prove
 105  (`!A B. ~(A = B) ==> angle(A,B,A) = &0`,
 106   SIMP_TAC[angle; vangle; VECTOR_SUB_EQ; GSYM NORM_POW_2; GSYM REAL_POW_2;
 107            REAL_DIV_REFL; ACS_1; REAL_POW_EQ_0; ARITH; NORM_EQ_0]);;
 108
 109 let ANGLE_SYM = prove
 110  (`!A B C. angle(A,B,C) = angle(C,B,A)`,
 111   REWRITE_TAC[angle; vangle; VECTOR_SUB_EQ; DISJ_SYM; REAL_MUL_SYM; DOT_SYM]);;
 112
 113 let ANGLE_RANGE = prove
 114  (`!A B C. &0 <= angle(A,B,C) /\ angle(A,B,C) <= pi`,
 115   REWRITE_TAC[angle; VANGLE_RANGE]);;
 116
 117 (* ------------------------------------------------------------------------- *)
 118 (* The law of cosines.                                                       *)
 119 (* ------------------------------------------------------------------------- *)
 120
 121 let LAW_OF_COSINES = prove
 122  (`!A B C:real^N.
 123      dist(B,C) pow 2 = dist(A,B) pow 2 + dist(A,C) pow 2 -
 124                          &2 * dist(A,B) * dist(A,C) * cos(angle(B,A,C))`,
 125   REPEAT GEN_TAC THEN
 126   REWRITE_TAC[angle; ONCE_REWRITE_RULE[NORM_SUB] dist; GSYM VANGLE;
 127               NORM_POW_2] THEN
 128   VECTOR_ARITH_TAC);;
 129
 130 (* ------------------------------------------------------------------------- *)
 131 (* The law of sines.                                                         *)
 132 (* ------------------------------------------------------------------------- *)
 133
 134 let LAW_OF_SINES = prove
 135  (`!A B C:real^N.
 136       sin(angle(A,B,C)) * dist(B,C) = sin(angle(B,A,C)) * dist(A,C)`,
 137   REPEAT GEN_TAC THEN MATCH_MP_TAC REAL_POW_EQ THEN EXISTS_TAC `2` THEN
 138   SIMP_TAC[SIN_ANGLE_POS; DIST_POS_LE; REAL_LE_MUL; ARITH] THEN
 139   REWRITE_TAC[REAL_POW_MUL; MATCH_MP
 140    (REAL_ARITH `x + y = &1 ==> x = &1 - y`) (SPEC_ALL SIN_CIRCLE)] THEN
 141   ASM_CASES_TAC `A:real^N = B` THEN ASM_REWRITE_TAC[ANGLE_REFL; COS_PI2] THEN
 142   RULE_ASSUM_TAC(ONCE_REWRITE_RULE[GSYM VECTOR_SUB_EQ]) THEN
 143   RULE_ASSUM_TAC(REWRITE_RULE[GSYM NORM_EQ_0]) THEN
 144   FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_RING
 145    `~(a = &0) ==> a pow 2 * x = a pow 2 * y ==> x = y`)) THEN
 146   ONCE_REWRITE_TAC[DIST_SYM] THEN REWRITE_TAC[GSYM dist] THEN
 147   GEN_REWRITE_TAC (RAND_CONV o LAND_CONV o ONCE_DEPTH_CONV) [DIST_SYM] THEN
 148   REWRITE_TAC[REAL_RING
 149    `a * (&1 - x) * b = c * (&1 - y) * d <=>
 150     a * b - a * b * x = c * d - c * d * y`] THEN
 151   REWRITE_TAC[GSYM REAL_POW_MUL; GSYM ANGLE] THEN
 152   REWRITE_TAC[REAL_POW_MUL; dist; NORM_POW_2] THEN
 153   REWRITE_TAC[DOT_LSUB; DOT_RSUB; DOT_SYM] THEN CONV_TAC REAL_RING);;
 154
 155 (* ------------------------------------------------------------------------- *)
 156 (* Hence the sum of the angles of a triangle.                                *)
 157 (* ------------------------------------------------------------------------- *)
 158
 159 let TRIANGLE_ANGLE_SUM_LEMMA = prove
 160  (`!A B C:real^N. ~(A = B) /\ ~(A = C) /\ ~(B = C)
 161                   ==> cos(angle(B,A,C) + angle(A,B,C) + angle(B,C,A)) = -- &1`,
 162   REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[GSYM VECTOR_SUB_EQ] THEN
 163   REWRITE_TAC[GSYM NORM_EQ_0] THEN
 164   MP_TAC(ISPECL [`A:real^N`; `B:real^N`; `C:real^N`] LAW_OF_COSINES) THEN
 165   MP_TAC(ISPECL [`B:real^N`; `A:real^N`; `C:real^N`] LAW_OF_COSINES) THEN
 166   MP_TAC(ISPECL [`C:real^N`; `B:real^N`; `A:real^N`] LAW_OF_COSINES) THEN
 167   MP_TAC(ISPECL [`A:real^N`; `B:real^N`; `C:real^N`] LAW_OF_SINES) THEN
 168   MP_TAC(ISPECL [`B:real^N`; `A:real^N`; `C:real^N`] LAW_OF_SINES) THEN
 169   MP_TAC(ISPECL [`B:real^N`; `C:real^N`; `A:real^N`] LAW_OF_SINES) THEN
 170   REWRITE_TAC[COS_ADD; SIN_ADD; dist; NORM_SUB] THEN
 171   MAP_EVERY (fun t -> MP_TAC(SPEC t SIN_CIRCLE))
 172    [`angle(B:real^N,A,C)`; `angle(A:real^N,B,C)`; `angle(B:real^N,C,A)`] THEN
 173   REWRITE_TAC[COS_ADD; SIN_ADD; ANGLE_SYM] THEN CONV_TAC REAL_RING);;
 174
 175 let COS_MINUS1_LEMMA = prove
 176  (`!x. cos(x) = -- &1 /\ &0 <= x /\ x < &3 * pi ==> x = pi`,
 177   REPEAT STRIP_TAC THEN
 178   SUBGOAL_THEN `?n. integer n /\ x = n * pi`
 179    (X_CHOOSE_THEN `nn:real` (CONJUNCTS_THEN2 ASSUME_TAC SUBST_ALL_TAC)) THEN
 180   REWRITE_TAC[GSYM SIN_EQ_0] THENL
 181    [MP_TAC(SPEC `x:real` SIN_CIRCLE) THEN ASM_REWRITE_TAC[] THEN
 182     CONV_TAC REAL_RING;
 183     ALL_TAC] THEN
 184   SUBGOAL_THEN `?n. nn = &n` (X_CHOOSE_THEN `n:num` SUBST_ALL_TAC) THENL
 185    [FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [REAL_MUL_POS_LE]) THEN
 186     SIMP_TAC[PI_POS; REAL_ARITH `&0 < p ==> ~(p < &0) /\ ~(p = &0)`] THEN
 187     ASM_MESON_TAC[INTEGER_POS; REAL_LT_LE];
 188     ALL_TAC] THEN
 189   MATCH_MP_TAC(REAL_RING `n = &1 ==> n * p = p`) THEN
 190   REWRITE_TAC[REAL_OF_NUM_EQ] THEN
 191   MATCH_MP_TAC(ARITH_RULE `n < 3 /\ ~(n = 0) /\ ~(n = 2) ==> n = 1`) THEN
 192   RULE_ASSUM_TAC(SIMP_RULE[REAL_LT_RMUL_EQ; PI_POS; REAL_OF_NUM_LT]) THEN
 193   ASM_REWRITE_TAC[] THEN CONJ_TAC THEN DISCH_THEN SUBST_ALL_TAC THEN
 194   REPEAT(POP_ASSUM MP_TAC) THEN SIMP_TAC[COS_0; REAL_MUL_LZERO; COS_NPI] THEN
 195   REAL_ARITH_TAC);;
 196
 197 let TRIANGLE_ANGLE_SUM = prove
 198  (`!A B C:real^N. ~(A = B) /\ ~(A = C) /\ ~(B = C)
 199                   ==> angle(B,A,C) + angle(A,B,C) + angle(B,C,A) = pi`,
 200   REPEAT STRIP_TAC THEN MATCH_MP_TAC COS_MINUS1_LEMMA THEN
 201   ASM_SIMP_TAC[TRIANGLE_ANGLE_SUM_LEMMA; REAL_LE_ADD; ANGLE_RANGE] THEN
 202   MATCH_MP_TAC(REAL_ARITH
 203    `&0 <= x /\ x <= p /\ &0 <= y /\ y <= p /\ &0 <= z /\ z <= p /\
 204     ~(x = p /\ y = p /\ z = p)
 205     ==> x + y + z < &3 * p`) THEN
 206   ASM_SIMP_TAC[ANGLE_RANGE] THEN REPEAT STRIP_TAC THEN
 207   REPEAT(FIRST_X_ASSUM(MP_TAC o MATCH_MP ANGLE_EQ_PI)) THEN
 208   REPEAT(FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE RAND_CONV
 209    [GSYM VECTOR_SUB_EQ])) THEN
 210   REWRITE_TAC[GSYM NORM_EQ_0; dist; NORM_SUB] THEN REAL_ARITH_TAC);;