colo12-c703.uibk.ac.at Git - Multivariate Analysis/.git/blob - Multivariate/geom.ml

   1 (* ========================================================================= *)
   2 (* Some geometric notions in real^N.                                         *)
   3 (* ========================================================================= *)
   4
   5 needs "Multivariate/realanalysis.ml";;
   6
   7 prioritize_vector();;
   8
   9 (* ------------------------------------------------------------------------- *)
  10 (* Pythagoras's theorem is almost immediate.                                 *)
  11 (* ------------------------------------------------------------------------- *)
  12
  13 let PYTHAGORAS = prove
  14  (`!A B C:real^N.
  15         orthogonal (A - B) (C - B)
  16         ==> norm(C - A) pow 2 = norm(B - A) pow 2 + norm(C - B) pow 2`,
  17   REWRITE_TAC[NORM_POW_2; orthogonal; DOT_LSUB; DOT_RSUB; DOT_SYM] THEN
  18   CONV_TAC REAL_RING);;
  19
  20 (* ------------------------------------------------------------------------- *)
  21 (* Angle between vectors (always 0 <= angle <= pi).                          *)
  22 (* ------------------------------------------------------------------------- *)
  23
  24 let vector_angle = new_definition
  25  `vector_angle x y = if x = vec 0 \/ y = vec 0 then pi / &2
  26                else acs((x dot y) / (norm x * norm y))`;;
  27
  28 let VECTOR_ANGLE_LINEAR_IMAGE_EQ = prove
  29  (`!f x y. linear f /\ (!x. norm(f x) = norm x)
  30            ==> (vector_angle (f x) (f y) = vector_angle x y)`,
  31   REPEAT STRIP_TAC THEN ASM_SIMP_TAC[vector_angle; GSYM NORM_EQ_0] THEN
  32   ASM_MESON_TAC[PRESERVES_NORM_PRESERVES_DOT]);;
  33
  34 add_linear_invariants [VECTOR_ANGLE_LINEAR_IMAGE_EQ];;
  35
  36 (* ------------------------------------------------------------------------- *)
  37 (* Basic properties of vector angles.                                        *)
  38 (* ------------------------------------------------------------------------- *)
  39
  40 let VECTOR_ANGLE_REFL = prove
  41  (`!x. vector_angle x x = if x = vec 0 then pi / &2 else &0`,
  42   GEN_TAC THEN REWRITE_TAC[vector_angle; DISJ_ACI] THEN
  43   COND_CASES_TAC THEN ASM_REWRITE_TAC[GSYM NORM_POW_2; REAL_POW_2] THEN
  44   ASM_SIMP_TAC[REAL_DIV_REFL; REAL_ENTIRE; NORM_EQ_0; ACS_1]);;
  45
  46 let VECTOR_ANGLE_SYM = prove
  47  (`!x y. vector_angle x y = vector_angle y x`,
  48   REWRITE_TAC[vector_angle; DISJ_SYM; DOT_SYM; REAL_MUL_SYM]);;
  49
  50 let VECTOR_ANGLE_LMUL = prove
  51  (`!a x y:real^N.
  52         vector_angle (a % x) y =
  53                 if a = &0 then pi / &2
  54                 else if &0 <= a then vector_angle x y
  55                 else pi - vector_angle x y`,
  56   REPEAT STRIP_TAC THEN COND_CASES_TAC THEN
  57   ASM_REWRITE_TAC[vector_angle; VECTOR_MUL_EQ_0] THEN
  58   ASM_CASES_TAC `x:real^N = vec 0 \/ y:real^N = vec 0` THEN
  59   ASM_REWRITE_TAC[] THENL [REAL_ARITH_TAC; ALL_TAC] THEN
  60   REWRITE_TAC[NORM_MUL; DOT_LMUL; real_div; REAL_INV_MUL; real_abs] THEN
  61   COND_CASES_TAC THEN
  62   ASM_REWRITE_TAC[REAL_INV_NEG; REAL_MUL_LNEG; REAL_MUL_RNEG] THEN
  63   ASM_SIMP_TAC[REAL_FIELD
  64    `~(a = &0) ==> (a * x) * (inv a * y) * z = x * y * z`] THEN
  65   MATCH_MP_TAC ACS_NEG THEN
  66   REWRITE_TAC[GSYM REAL_ABS_BOUNDS; GSYM REAL_INV_MUL] THEN
  67   REWRITE_TAC[GSYM real_div; NORM_CAUCHY_SCHWARZ_DIV]);;
  68
  69 let VECTOR_ANGLE_RMUL = prove
  70  (`!a x y:real^N.
  71         vector_angle x (a % y) =
  72                 if a = &0 then pi / &2
  73                 else if &0 <= a then vector_angle x y
  74                 else pi - vector_angle x y`,
  75   ONCE_REWRITE_TAC[VECTOR_ANGLE_SYM] THEN
  76   REWRITE_TAC[VECTOR_ANGLE_LMUL]);;
  77
  78 let VECTOR_ANGLE_LNEG = prove
  79  (`!x y. vector_angle (--x) y = pi - vector_angle x y`,
  80   REWRITE_TAC[VECTOR_ARITH `--x = -- &1 % x`; VECTOR_ANGLE_LMUL] THEN
  81   CONV_TAC REAL_RAT_REDUCE_CONV);;
  82
  83 let VECTOR_ANGLE_RNEG = prove
  84  (`!x y. vector_angle x (--y) = pi - vector_angle x y`,
  85   ONCE_REWRITE_TAC[VECTOR_ANGLE_SYM] THEN REWRITE_TAC[VECTOR_ANGLE_LNEG]);;
  86
  87 let VECTOR_ANGLE_NEG2 = prove
  88  (`!x y. vector_angle (--x) (--y) = vector_angle x y`,
  89   REWRITE_TAC[VECTOR_ANGLE_LNEG; VECTOR_ANGLE_RNEG] THEN REAL_ARITH_TAC);;
  90
  91 let VECTOR_ANGLE = prove
  92  (`!x y:real^N. x dot y = norm(x) * norm(y) * cos(vector_angle x y)`,
  93   REPEAT GEN_TAC THEN REWRITE_TAC[vector_angle] THEN
  94   ASM_CASES_TAC `x:real^N = vec 0` THEN
  95   ASM_REWRITE_TAC[DOT_LZERO; NORM_0; REAL_MUL_LZERO] THEN
  96   ASM_CASES_TAC `y:real^N = vec 0` THEN
  97   ASM_REWRITE_TAC[DOT_RZERO; NORM_0; REAL_MUL_LZERO; REAL_MUL_RZERO] THEN
  98   ONCE_REWRITE_TAC[AC REAL_MUL_AC `a * b * c:real = c * a * b`] THEN
  99   ASM_SIMP_TAC[GSYM REAL_EQ_LDIV_EQ; REAL_LT_MUL; NORM_POS_LT] THEN
 100   MATCH_MP_TAC(GSYM COS_ACS) THEN
 101   ASM_REWRITE_TAC[REAL_BOUNDS_LE; NORM_CAUCHY_SCHWARZ_DIV]);;
 102
 103 let VECTOR_ANGLE_RANGE = prove
 104  (`!x y:real^N. &0 <= vector_angle x y /\ vector_angle x y <= pi`,
 105   REPEAT GEN_TAC THEN REWRITE_TAC[vector_angle] THEN COND_CASES_TAC THENL
 106    [MP_TAC PI_POS THEN REAL_ARITH_TAC; ALL_TAC] THEN
 107   RULE_ASSUM_TAC(REWRITE_RULE[DE_MORGAN_THM]) THEN MATCH_MP_TAC ACS_BOUNDS THEN
 108   ASM_REWRITE_TAC[REAL_BOUNDS_LE; NORM_CAUCHY_SCHWARZ_DIV]);;
 109
 110 let ORTHOGONAL_VECTOR_ANGLE = prove
 111  (`!x y:real^N. orthogonal x y <=> vector_angle x y = pi / &2`,
 112   REPEAT STRIP_TAC THEN REWRITE_TAC[orthogonal; vector_angle] THEN
 113   ASM_CASES_TAC `x:real^N = vec 0` THEN ASM_REWRITE_TAC[DOT_LZERO] THEN
 114   ASM_CASES_TAC `y:real^N = vec 0` THEN ASM_REWRITE_TAC[DOT_RZERO] THEN
 115   EQ_TAC THENL
 116    [SIMP_TAC[real_div; REAL_MUL_LZERO] THEN DISCH_TAC THEN
 117     REWRITE_TAC[GSYM real_div; GSYM COS_PI2] THEN
 118     MATCH_MP_TAC ACS_COS THEN MP_TAC PI_POS THEN REAL_ARITH_TAC;
 119     DISCH_THEN(MP_TAC o AP_TERM `cos`) THEN
 120     SIMP_TAC[COS_ACS; REAL_BOUNDS_LE; NORM_CAUCHY_SCHWARZ_DIV; COS_PI2] THEN
 121     ASM_SIMP_TAC[REAL_EQ_LDIV_EQ; REAL_LT_MUL; NORM_POS_LT; REAL_MUL_LZERO]]);;
 122
 123 let VECTOR_ANGLE_EQ_0 = prove
 124  (`!x y:real^N. vector_angle x y = &0 <=>
 125                 ~(x = vec 0) /\ ~(y = vec 0) /\ norm(x) % y = norm(y) % x`,
 126   REPEAT GEN_TAC THEN
 127   MAP_EVERY ASM_CASES_TAC [`x:real^N = vec 0`; `y:real^N = vec 0`] THEN
 128   ASM_SIMP_TAC[vector_angle; PI_NZ; REAL_ARITH `x / &2 = &0 <=> x = &0`] THEN
 129   REWRITE_TAC[GSYM NORM_CAUCHY_SCHWARZ_EQ] THEN
 130   GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [GSYM REAL_MUL_LID] THEN
 131   ASM_SIMP_TAC[GSYM REAL_EQ_LDIV_EQ; NORM_POS_LT; REAL_LT_MUL] THEN
 132   MESON_TAC[ACS_1; COS_ACS; REAL_BOUNDS_LE; NORM_CAUCHY_SCHWARZ_DIV; COS_0]);;
 133
 134 let VECTOR_ANGLE_EQ_PI = prove
 135  (`!x y:real^N. vector_angle x y = pi <=>
 136                 ~(x = vec 0) /\ ~(y = vec 0) /\
 137                 norm(x) % y + norm(y) % x = vec 0`,
 138   REPEAT GEN_TAC THEN
 139   MP_TAC(ISPECL [`x:real^N`; `--y:real^N`] VECTOR_ANGLE_EQ_0) THEN
 140   SIMP_TAC[VECTOR_ANGLE_RNEG; REAL_ARITH `pi - x = &0 <=> x = pi`] THEN
 141   STRIP_TAC THEN
 142   REWRITE_TAC[NORM_NEG; VECTOR_ARITH `--x = vec 0 <=> x = vec 0`] THEN
 143   AP_TERM_TAC THEN AP_TERM_TAC THEN VECTOR_ARITH_TAC);;
 144
 145 let VECTOR_ANGLE_EQ_0_DIST = prove
 146  (`!x y:real^N. vector_angle x y = &0 <=>
 147                 ~(x = vec 0) /\ ~(y = vec 0) /\ norm(x + y) = norm x + norm y`,
 148   REWRITE_TAC[VECTOR_ANGLE_EQ_0; GSYM NORM_TRIANGLE_EQ]);;
 149
 150 let VECTOR_ANGLE_EQ_PI_DIST = prove
 151  (`!x y:real^N. vector_angle x y = pi <=>
 152                 ~(x = vec 0) /\ ~(y = vec 0) /\ norm(x - y) = norm x + norm y`,
 153   REPEAT GEN_TAC THEN
 154   MP_TAC(ISPECL [`x:real^N`; `--y:real^N`] VECTOR_ANGLE_EQ_0_DIST) THEN
 155   SIMP_TAC[VECTOR_ANGLE_RNEG; REAL_ARITH `pi - x = &0 <=> x = pi`] THEN
 156   STRIP_TAC THEN REWRITE_TAC[NORM_NEG] THEN NORM_ARITH_TAC);;
 157
 158 let SIN_VECTOR_ANGLE_POS = prove
 159  (`!v w. &0 <= sin(vector_angle v w)`,
 160   SIMP_TAC[SIN_POS_PI_LE; VECTOR_ANGLE_RANGE]);;
 161
 162 let SIN_VECTOR_ANGLE_EQ_0 = prove
 163  (`!x y. sin(vector_angle x y) = &0 <=>
 164            vector_angle x y = &0 \/ vector_angle x y = pi`,
 165   MESON_TAC[SIN_POS_PI; VECTOR_ANGLE_RANGE; REAL_LT_LE; SIN_0; SIN_PI]);;
 166
 167 let ASN_SIN_VECTOR_ANGLE = prove
 168  (`!x y:real^N.
 169         asn(sin(vector_angle x y)) =
 170           if vector_angle x y <= pi / &2 then vector_angle x y
 171           else pi - vector_angle x y`,
 172   REPEAT GEN_TAC THEN COND_CASES_TAC THENL
 173    [ALL_TAC;
 174     MATCH_MP_TAC EQ_TRANS THEN
 175     EXISTS_TAC `asn(sin(pi - vector_angle (x:real^N) y))` THEN CONJ_TAC THENL
 176      [AP_TERM_TAC THEN REWRITE_TAC[SIN_SUB; SIN_PI; COS_PI] THEN
 177       REAL_ARITH_TAC;
 178       ALL_TAC]] THEN
 179   MATCH_MP_TAC ASN_SIN THEN
 180   MP_TAC(ISPECL [`x:real^N`; `y:real^N`] VECTOR_ANGLE_RANGE) THEN
 181   ASM_REAL_ARITH_TAC);;
 182
 183 let SIN_VECTOR_ANGLE_EQ = prove
 184  (`!x y w z.
 185         sin(vector_angle x y) = sin(vector_angle w z) <=>
 186             vector_angle x y = vector_angle w z \/
 187             vector_angle x y = pi - vector_angle w z`,
 188   REPEAT GEN_TAC THEN EQ_TAC THEN
 189   STRIP_TAC THEN ASM_REWRITE_TAC[SIN_SUB; SIN_PI; COS_PI] THENL
 190    [ALL_TAC; REAL_ARITH_TAC] THEN
 191   FIRST_X_ASSUM(MP_TAC o AP_TERM `asn`) THEN
 192   REWRITE_TAC[ASN_SIN_VECTOR_ANGLE] THEN REAL_ARITH_TAC);;
 193
 194 let CONTINUOUS_WITHIN_CX_VECTOR_ANGLE_COMPOSE = prove
 195  (`!f:real^M->real^N g x s.
 196      ~(f x = vec 0) /\ ~(g x = vec 0) /\
 197      f continuous (at x within s) /\
 198      g continuous (at x within s)
 199      ==> (\x. Cx(vector_angle (f x) (g x))) continuous (at x within s)`,
 200   REPEAT STRIP_TAC THEN
 201   ASM_CASES_TAC `trivial_limit(at (x:real^M) within s)` THEN
 202   ASM_SIMP_TAC[CONTINUOUS_TRIVIAL_LIMIT; vector_angle] THEN
 203   SUBGOAL_THEN
 204    `(cacs o (\x. Cx(((f x:real^N) dot g x) / (norm(f x) * norm(g x)))))
 205     continuous (at (x:real^M) within s)`
 206   MP_TAC THENL
 207    [MATCH_MP_TAC CONTINUOUS_WITHIN_COMPOSE THEN CONJ_TAC THENL
 208      [REWRITE_TAC[CX_DIV; CX_MUL] THEN REWRITE_TAC[WITHIN_UNIV] THEN
 209       MATCH_MP_TAC CONTINUOUS_COMPLEX_DIV THEN
 210       ASM_SIMP_TAC[NETLIMIT_WITHIN; COMPLEX_ENTIRE; CX_INJ; NORM_EQ_0] THEN
 211       REWRITE_TAC[CONTINUOUS_CX_LIFT; GSYM CX_MUL; LIFT_CMUL] THEN
 212       ASM_SIMP_TAC[CONTINUOUS_LIFT_DOT2] THEN
 213       MATCH_MP_TAC CONTINUOUS_MUL THEN
 214       ASM_SIMP_TAC[CONTINUOUS_LIFT_NORM_COMPOSE; o_DEF];
 215       MATCH_MP_TAC CONTINUOUS_WITHIN_SUBSET THEN
 216       EXISTS_TAC `{z | real z /\ abs(Re z) <= &1}` THEN
 217       REWRITE_TAC[CONTINUOUS_WITHIN_CACS_REAL] THEN
 218       REWRITE_TAC[SUBSET; FORALL_IN_IMAGE; IN_UNIV; IN_ELIM_THM] THEN
 219       REWRITE_TAC[REAL_CX; RE_CX; NORM_CAUCHY_SCHWARZ_DIV]];
 220     ASM_SIMP_TAC[CONTINUOUS_WITHIN; CX_ACS; o_DEF;
 221                  NORM_CAUCHY_SCHWARZ_DIV] THEN
 222     MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ] LIM_TRANSFORM_EVENTUALLY) THEN
 223     SUBGOAL_THEN
 224       `eventually (\y. ~((f:real^M->real^N) y = vec 0) /\
 225                        ~((g:real^M->real^N) y = vec 0))
 226                   (at x within s)`
 227     MP_TAC THENL
 228      [REWRITE_TAC[EVENTUALLY_AND] THEN CONJ_TAC THENL
 229        [UNDISCH_TAC `(f:real^M->real^N) continuous (at x within s)`;
 230         UNDISCH_TAC `(g:real^M->real^N) continuous (at x within s)`] THEN
 231       REWRITE_TAC[CONTINUOUS_WITHIN; tendsto] THENL
 232        [DISCH_THEN(MP_TAC o SPEC `norm((f:real^M->real^N) x)`);
 233         DISCH_THEN(MP_TAC o SPEC `norm((g:real^M->real^N) x)`)] THEN
 234       ASM_REWRITE_TAC[NORM_POS_LT] THEN
 235       MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ] EVENTUALLY_MONO) THEN
 236       REWRITE_TAC[] THEN CONV_TAC NORM_ARITH;
 237       MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ] EVENTUALLY_MONO) THEN
 238       SIMP_TAC[CX_ACS; NORM_CAUCHY_SCHWARZ_DIV]]]);;
 239
 240 let CONTINUOUS_AT_CX_VECTOR_ANGLE = prove
 241  (`!c x:real^N. ~(x = vec 0) ==> (Cx o vector_angle c) continuous (at x)`,
 242   REPEAT STRIP_TAC THEN REWRITE_TAC[o_DEF; vector_angle] THEN
 243   ASM_CASES_TAC `c:real^N = vec 0` THEN ASM_REWRITE_TAC[CONTINUOUS_CONST] THEN
 244   MATCH_MP_TAC CONTINUOUS_TRANSFORM_AT THEN
 245   MAP_EVERY EXISTS_TAC [`\x:real^N. cacs(Cx((c dot x) / (norm c * norm x)))`;
 246                         `norm(x:real^N)`] THEN
 247   ASM_REWRITE_TAC[NORM_POS_LT] THEN CONJ_TAC THENL
 248    [X_GEN_TAC `z:real^N` THEN DISCH_TAC THEN COND_CASES_TAC THENL
 249      [ASM_MESON_TAC[NORM_ARITH `~(dist(vec 0,x) < norm x)`]; ALL_TAC] THEN
 250     MATCH_MP_TAC(GSYM CX_ACS) THEN REWRITE_TAC[NORM_CAUCHY_SCHWARZ_DIV];
 251     ALL_TAC] THEN
 252   ONCE_REWRITE_TAC[GSYM WITHIN_UNIV] THEN
 253   MATCH_MP_TAC(REWRITE_RULE[o_DEF] CONTINUOUS_WITHIN_COMPOSE) THEN
 254   CONJ_TAC THENL
 255    [REWRITE_TAC[CX_DIV; CX_MUL] THEN REWRITE_TAC[WITHIN_UNIV] THEN
 256     MATCH_MP_TAC CONTINUOUS_COMPLEX_DIV THEN
 257     ASM_REWRITE_TAC[NETLIMIT_AT; COMPLEX_ENTIRE; CX_INJ; NORM_EQ_0] THEN
 258     SIMP_TAC[CONTINUOUS_COMPLEX_MUL; CONTINUOUS_CONST;
 259              CONTINUOUS_AT_CX_NORM; CONTINUOUS_AT_CX_DOT];
 260     MATCH_MP_TAC CONTINUOUS_WITHIN_SUBSET THEN
 261     EXISTS_TAC `{z | real z /\ abs(Re z) <= &1}` THEN
 262     REWRITE_TAC[CONTINUOUS_WITHIN_CACS_REAL] THEN
 263     REWRITE_TAC[SUBSET; FORALL_IN_IMAGE; IN_UNIV; IN_ELIM_THM] THEN
 264     REWRITE_TAC[REAL_CX; RE_CX; NORM_CAUCHY_SCHWARZ_DIV]]);;
 265
 266 let CONTINUOUS_WITHIN_CX_VECTOR_ANGLE = prove
 267  (`!c x:real^N s.
 268      ~(x = vec 0) ==> (Cx o vector_angle c) continuous (at x within s)`,
 269   SIMP_TAC[CONTINUOUS_AT_WITHIN; CONTINUOUS_AT_CX_VECTOR_ANGLE]);;
 270
 271 let REAL_CONTINUOUS_AT_VECTOR_ANGLE = prove
 272  (`!c x:real^N. ~(x = vec 0) ==> (vector_angle c) real_continuous (at x)`,
 273   REWRITE_TAC[REAL_CONTINUOUS_CONTINUOUS; CONTINUOUS_AT_CX_VECTOR_ANGLE]);;
 274
 275 let REAL_CONTINUOUS_WITHIN_VECTOR_ANGLE = prove
 276  (`!c s x:real^N. ~(x = vec 0)
 277                   ==> (vector_angle c) real_continuous (at x within s)`,
 278   REWRITE_TAC[REAL_CONTINUOUS_CONTINUOUS; CONTINUOUS_WITHIN_CX_VECTOR_ANGLE]);;
 279
 280 let CONTINUOUS_ON_CX_VECTOR_ANGLE = prove
 281  (`!s. ~(vec 0 IN s) ==> (Cx o vector_angle c) continuous_on s`,
 282   REPEAT STRIP_TAC THEN REWRITE_TAC[CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN] THEN
 283   ASM_MESON_TAC[CONTINUOUS_WITHIN_CX_VECTOR_ANGLE]);;
 284
 285 let VECTOR_ANGLE_EQ = prove
 286  (`!u v x y. ~(u = vec 0) /\  ~(v = vec 0) /\ ~(x = vec 0) /\ ~(y = vec 0)
 287              ==> (vector_angle u v = vector_angle x y <=>
 288                         (x dot y) * norm(u) * norm(v) =
 289                         (u dot v) * norm(x) * norm(y))`,
 290   SIMP_TAC[vector_angle; NORM_EQ_0; REAL_FIELD
 291    `~(u = &0) /\ ~(v = &0) /\ ~(x = &0) /\ ~(y = &0)
 292     ==> (a * u * v = b * x * y <=> a / (x * y) = b / (u * v))`] THEN
 293   REPEAT STRIP_TAC THEN EQ_TAC THEN SIMP_TAC[] THEN
 294   DISCH_THEN(MP_TAC o AP_TERM `cos`) THEN
 295   SIMP_TAC[COS_ACS; NORM_CAUCHY_SCHWARZ_DIV; REAL_BOUNDS_LE]);;
 296
 297 let COS_VECTOR_ANGLE_EQ = prove
 298  (`!u v x y.
 299         cos(vector_angle u v) = cos(vector_angle x y) <=>
 300         vector_angle u v = vector_angle x y`,
 301   MESON_TAC[ACS_COS; VECTOR_ANGLE_RANGE]);;
 302
 303 let COLLINEAR_VECTOR_ANGLE = prove
 304  (`!x y. ~(x = vec 0) /\ ~(y = vec 0)
 305          ==> (collinear {vec 0,x,y} <=>
 306                 vector_angle x y = &0 \/ vector_angle x y = pi)`,
 307   REWRITE_TAC[GSYM NORM_CAUCHY_SCHWARZ_EQUAL; NORM_CAUCHY_SCHWARZ_ABS_EQ;
 308               VECTOR_ANGLE_EQ_0; VECTOR_ANGLE_EQ_PI] THEN
 309   REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN BINOP_TAC THEN
 310   VECTOR_ARITH_TAC);;
 311
 312 let COLLINEAR_SIN_VECTOR_ANGLE = prove
 313  (`!x y. ~(x = vec 0) /\ ~(y = vec 0)
 314          ==> (collinear {vec 0,x,y} <=> sin(vector_angle x y) = &0)`,
 315   REWRITE_TAC[SIN_VECTOR_ANGLE_EQ_0; COLLINEAR_VECTOR_ANGLE]);;
 316
 317 let COLLINEAR_SIN_VECTOR_ANGLE_IMP = prove
 318  (`!x y. sin(vector_angle x y) = &0
 319          ==> ~(x = vec 0) /\ ~(y = vec 0) /\ collinear {vec 0,x,y}`,
 320   MESON_TAC[COLLINEAR_SIN_VECTOR_ANGLE; SIN_VECTOR_ANGLE_EQ_0;
 321             VECTOR_ANGLE_EQ_0_DIST; VECTOR_ANGLE_EQ_PI_DIST]);;
 322
 323 let VECTOR_ANGLE_EQ_0_RIGHT = prove
 324  (`!x y z:real^N. vector_angle x y = &0
 325                   ==> (vector_angle x z = vector_angle y z)`,
 326   REWRITE_TAC[VECTOR_ANGLE_EQ_0] THEN REPEAT STRIP_TAC THEN
 327   MATCH_MP_TAC EQ_TRANS THEN
 328   EXISTS_TAC `vector_angle (norm(x:real^N) % y) (z:real^N)` THEN CONJ_TAC THENL
 329    [ASM_REWRITE_TAC[] THEN
 330     ASM_REWRITE_TAC[VECTOR_ANGLE_LMUL; NORM_EQ_0; NORM_POS_LE];
 331     REWRITE_TAC[VECTOR_ANGLE_LMUL] THEN
 332     ASM_REWRITE_TAC[NORM_EQ_0; NORM_POS_LE]]);;
 333
 334 let VECTOR_ANGLE_EQ_0_LEFT = prove
 335  (`!x y z:real^N. vector_angle x y = &0
 336                   ==> (vector_angle z x = vector_angle z y)`,
 337   MESON_TAC[VECTOR_ANGLE_EQ_0_RIGHT; VECTOR_ANGLE_SYM]);;
 338
 339 let VECTOR_ANGLE_EQ_PI_RIGHT = prove
 340  (`!x y z:real^N. vector_angle x y = pi
 341                   ==> (vector_angle x z = pi - vector_angle y z)`,
 342   REPEAT STRIP_TAC THEN
 343   MP_TAC(ISPECL [`--x:real^N`; `y:real^N`; `z:real^N`]
 344    VECTOR_ANGLE_EQ_0_RIGHT) THEN
 345   ASM_REWRITE_TAC[VECTOR_ANGLE_LNEG] THEN REAL_ARITH_TAC);;
 346
 347 let VECTOR_ANGLE_EQ_PI_LEFT = prove
 348  (`!x y z:real^N. vector_angle x y = pi
 349                   ==> (vector_angle z x = pi - vector_angle z y)`,
 350   MESON_TAC[VECTOR_ANGLE_EQ_PI_RIGHT; VECTOR_ANGLE_SYM]);;
 351
 352 let COS_VECTOR_ANGLE = prove
 353  (`!x y:real^N.
 354         cos(vector_angle x y) = if x = vec 0 \/ y = vec 0 then &0
 355                                 else (x dot y) / (norm x * norm y)`,
 356   REPEAT GEN_TAC THEN
 357   ASM_CASES_TAC `x:real^N = vec 0` THENL
 358    [ASM_REWRITE_TAC[vector_angle; COS_PI2]; ALL_TAC] THEN
 359   ASM_CASES_TAC `y:real^N = vec 0` THENL
 360    [ASM_REWRITE_TAC[vector_angle; COS_PI2]; ALL_TAC] THEN
 361   ASM_SIMP_TAC[REAL_EQ_RDIV_EQ; REAL_LT_MUL; NORM_POS_LT; VECTOR_ANGLE] THEN
 362   REAL_ARITH_TAC);;
 363
 364 let SIN_VECTOR_ANGLE = prove
 365  (`!x y:real^N.
 366         sin(vector_angle x y) =
 367             if x = vec 0 \/ y = vec 0 then &1
 368             else sqrt(&1 - ((x dot y) / (norm x * norm y)) pow 2)`,
 369   SIMP_TAC[SIN_COS_SQRT; SIN_VECTOR_ANGLE_POS; COS_VECTOR_ANGLE] THEN
 370   REPEAT GEN_TAC THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
 371   CONV_TAC REAL_RAT_REDUCE_CONV THEN REWRITE_TAC[SQRT_1]);;
 372
 373 let SIN_SQUARED_VECTOR_ANGLE = prove
 374  (`!x y:real^N.
 375         sin(vector_angle x y) pow 2 =
 376             if x = vec 0 \/ y = vec 0 then &1
 377             else &1 - ((x dot y) / (norm x * norm y)) pow 2`,
 378   REPEAT GEN_TAC THEN REWRITE_TAC
 379    [REWRITE_RULE [REAL_ARITH `s + c = &1 <=> s = &1 - c`] SIN_CIRCLE] THEN
 380   REWRITE_TAC[COS_VECTOR_ANGLE] THEN REAL_ARITH_TAC);;
 381
 382 let VECTOR_ANGLE_COMPLEX_LMUL = prove
 383  (`!a. ~(a = Cx(&0))
 384        ==> vector_angle (a * x) (a * y) = vector_angle x y`,
 385   REPEAT STRIP_TAC THEN
 386   ASM_CASES_TAC `x = Cx(&0)` THENL
 387    [ASM_REWRITE_TAC[COMPLEX_MUL_RZERO; vector_angle; COMPLEX_VEC_0];
 388     ALL_TAC] THEN
 389   ASM_CASES_TAC `y = Cx(&0)` THENL
 390    [ASM_REWRITE_TAC[COMPLEX_MUL_RZERO; vector_angle; COMPLEX_VEC_0];
 391     ALL_TAC] THEN
 392   MP_TAC(ISPECL
 393    [`a * x:complex`; `a * y:complex`; `x:complex`; `y:complex`]
 394         VECTOR_ANGLE_EQ) THEN
 395   ASM_REWRITE_TAC[COMPLEX_VEC_0; COMPLEX_ENTIRE] THEN
 396   DISCH_THEN SUBST1_TAC THEN
 397   REWRITE_TAC[COMPLEX_NORM_MUL] THEN MATCH_MP_TAC(REAL_RING
 398    `a pow 2 * xy:real = d ==> xy * (a * x) * (a * y) = d * x * y`) THEN
 399   REWRITE_TAC[NORM_POW_2] THEN
 400   REWRITE_TAC[DOT_2; complex_mul; GSYM RE_DEF; GSYM IM_DEF; RE; IM] THEN
 401   REAL_ARITH_TAC);;
 402
 403 let VECTOR_ANGLE_1 = prove
 404  (`!x. vector_angle x (Cx(&1)) = acs(Re x / norm x)`,
 405   GEN_TAC THEN
 406   SIMP_TAC[vector_angle; COMPLEX_VEC_0; CX_INJ; REAL_OF_NUM_EQ; ARITH_EQ] THEN
 407   COND_CASES_TAC THENL
 408    [ASM_REWRITE_TAC[real_div; RE_CX; ACS_0; REAL_MUL_LZERO]; ALL_TAC] THEN
 409   REWRITE_TAC[COMPLEX_NORM_CX; REAL_ABS_NUM; REAL_MUL_RID] THEN
 410   REWRITE_TAC[DOT_2; GSYM RE_DEF; GSYM IM_DEF; RE_CX; IM_CX] THEN
 411   AP_TERM_TAC THEN REAL_ARITH_TAC);;
 412
 413 let ARG_EQ_VECTOR_ANGLE_1 = prove
 414  (`!z. ~(z = Cx(&0)) /\ &0 <= Im z ==> Arg z = vector_angle z (Cx(&1))`,
 415   REPEAT STRIP_TAC THEN REWRITE_TAC[VECTOR_ANGLE_1] THEN
 416   GEN_REWRITE_TAC (RAND_CONV o RAND_CONV o LAND_CONV o RAND_CONV) [ARG] THEN
 417   REWRITE_TAC[RE_MUL_CX; RE_CEXP; RE_II; IM_MUL_II; IM_CX; RE_CX] THEN
 418   REWRITE_TAC[REAL_MUL_LZERO; REAL_EXP_0; REAL_MUL_LID] THEN
 419   ASM_SIMP_TAC[COMPLEX_NORM_ZERO; REAL_FIELD
 420    `~(z = &0) ==> (z * x) / z = x`] THEN
 421   CONV_TAC SYM_CONV THEN MATCH_MP_TAC ACS_COS THEN
 422   ASM_REWRITE_TAC[ARG; ARG_LE_PI]);;
 423
 424 let VECTOR_ANGLE_ARG = prove
 425  (`!w z. ~(w = Cx(&0)) /\ ~(z = Cx(&0))
 426          ==> vector_angle w z = if &0 <= Im(z / w) then Arg(z / w)
 427                                 else &2 * pi - Arg(z / w)`,
 428   REPEAT STRIP_TAC THEN COND_CASES_TAC THENL
 429    [SUBGOAL_THEN `z = w * (z / w) /\ w = w * Cx(&1)` MP_TAC THENL
 430      [REPEAT(POP_ASSUM MP_TAC) THEN CONV_TAC COMPLEX_FIELD; ALL_TAC];
 431     SUBGOAL_THEN `w = z * (w / z) /\ z = z * Cx(&1)` MP_TAC THENL
 432      [REPEAT(POP_ASSUM MP_TAC) THEN CONV_TAC COMPLEX_FIELD; ALL_TAC]] THEN
 433   DISCH_THEN(fun th -> GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [th]) THEN
 434   ASM_SIMP_TAC[VECTOR_ANGLE_COMPLEX_LMUL] THENL
 435    [ONCE_REWRITE_TAC[VECTOR_ANGLE_SYM] THEN CONV_TAC SYM_CONV THEN
 436     MATCH_MP_TAC ARG_EQ_VECTOR_ANGLE_1 THEN ASM_REWRITE_TAC[] THEN
 437     REPEAT(POP_ASSUM MP_TAC) THEN CONV_TAC COMPLEX_FIELD;
 438     MP_TAC(ISPEC `z / w:complex` ARG_INV) THEN ANTS_TAC THENL
 439      [ASM_MESON_TAC[real; REAL_LE_REFL]; DISCH_THEN(SUBST1_TAC o SYM)] THEN
 440     REWRITE_TAC[COMPLEX_INV_DIV] THEN CONV_TAC SYM_CONV THEN
 441     MATCH_MP_TAC ARG_EQ_VECTOR_ANGLE_1 THEN CONJ_TAC THENL
 442      [REPEAT(POP_ASSUM MP_TAC) THEN CONV_TAC COMPLEX_FIELD;
 443       ONCE_REWRITE_TAC[GSYM COMPLEX_INV_DIV] THEN
 444       REWRITE_TAC[IM_COMPLEX_INV_GE_0] THEN ASM_REAL_ARITH_TAC]]);;
 445
 446 (* ------------------------------------------------------------------------- *)
 447 (* Traditional geometric notion of angle (always 0 <= theta <= pi).          *)
 448 (* ------------------------------------------------------------------------- *)
 449
 450 let angle = new_definition
 451  `angle(a,b,c) = vector_angle (a - b) (c - b)`;;
 452
 453 let ANGLE_LINEAR_IMAGE_EQ = prove
 454  (`!f a b c.
 455         linear f /\ (!x. norm(f x) = norm x)
 456         ==> angle(f a,f b,f c) = angle(a,b,c)`,
 457   SIMP_TAC[angle; GSYM LINEAR_SUB; VECTOR_ANGLE_LINEAR_IMAGE_EQ]);;
 458
 459 add_linear_invariants [ANGLE_LINEAR_IMAGE_EQ];;
 460
 461 let ANGLE_TRANSLATION_EQ = prove
 462  (`!a b c d. angle(a + b,a + c,a + d) = angle(b,c,d)`,
 463   REPEAT GEN_TAC THEN REWRITE_TAC[angle] THEN
 464   BINOP_TAC THEN VECTOR_ARITH_TAC);;
 465
 466 add_translation_invariants [ANGLE_TRANSLATION_EQ];;
 467
 468 let VECTOR_ANGLE_ANGLE = prove
 469  (`vector_angle x y = angle(x,vec 0,y)`,
 470   REWRITE_TAC[angle; VECTOR_SUB_RZERO]);;
 471
 472 let ANGLE_EQ_PI_DIST = prove
 473  (`!A B C:real^N.
 474         angle(A,B,C) = pi <=>
 475         ~(A = B) /\ ~(C = B) /\ dist(A,C) = dist(A,B) + dist(B,C)`,
 476   REWRITE_TAC[angle; VECTOR_ANGLE_EQ_PI_DIST] THEN NORM_ARITH_TAC);;
 477
 478 let SIN_ANGLE_POS = prove
 479  (`!A B C. &0 <= sin(angle(A,B,C))`,
 480   REWRITE_TAC[angle; SIN_VECTOR_ANGLE_POS]);;
 481
 482 let ANGLE = prove
 483  (`!A B C. (A - C) dot (B - C) = dist(A,C) * dist(B,C) * cos(angle(A,C,B))`,
 484   REWRITE_TAC[angle; dist; GSYM VECTOR_ANGLE]);;
 485
 486 let ANGLE_REFL = prove
 487  (`!A B. angle(A,A,B) = pi / &2 /\ angle(B,A,A) = pi / &2`,
 488   REWRITE_TAC[angle; vector_angle; VECTOR_SUB_REFL]);;
 489
 490 let ANGLE_REFL_MID = prove
 491  (`!A B. ~(A = B) ==> angle(A,B,A) = &0`,
 492   SIMP_TAC[angle; vector_angle; VECTOR_SUB_EQ; GSYM NORM_POW_2; ARITH;
 493     GSYM REAL_POW_2; REAL_DIV_REFL; ACS_1; REAL_POW_EQ_0; NORM_EQ_0]);;
 494
 495 let ANGLE_SYM = prove
 496  (`!A B C. angle(A,B,C) = angle(C,B,A)`,
 497   REWRITE_TAC[angle; vector_angle; VECTOR_SUB_EQ; DISJ_SYM;
 498               REAL_MUL_SYM; DOT_SYM]);;
 499
 500 let ANGLE_RANGE = prove
 501  (`!A B C. &0 <= angle(A,B,C) /\ angle(A,B,C) <= pi`,
 502   REWRITE_TAC[angle; VECTOR_ANGLE_RANGE]);;
 503
 504 let COS_ANGLE_EQ = prove
 505  (`!a b c a' b' c'.
 506         cos(angle(a,b,c)) = cos(angle(a',b',c')) <=>
 507         angle(a,b,c) = angle(a',b',c')`,
 508   REWRITE_TAC[angle; COS_VECTOR_ANGLE_EQ]);;
 509
 510 let ANGLE_EQ = prove
 511  (`!a b c a' b' c'.
 512         ~(a = b) /\ ~(c = b) /\ ~(a' = b') /\ ~(c' = b')
 513         ==> (angle(a,b,c) = angle(a',b',c') <=>
 514                 ((a' - b') dot (c' - b')) * norm (a - b) * norm (c - b) =
 515                 ((a - b) dot (c - b)) * norm (a' - b') * norm (c' - b'))`,
 516   SIMP_TAC[angle; VECTOR_ANGLE_EQ; VECTOR_SUB_EQ]);;
 517
 518 let SIN_ANGLE_EQ_0 = prove
 519  (`!A B C. sin(angle(A,B,C)) = &0 <=> angle(A,B,C) = &0 \/ angle(A,B,C) = pi`,
 520   REWRITE_TAC[angle; SIN_VECTOR_ANGLE_EQ_0]);;
 521
 522 let SIN_ANGLE_EQ = prove
 523  (`!A B C A' B' C'. sin(angle(A,B,C)) = sin(angle(A',B',C')) <=>
 524                         angle(A,B,C) = angle(A',B',C') \/
 525                         angle(A,B,C) = pi - angle(A',B',C')`,
 526   REWRITE_TAC[angle; SIN_VECTOR_ANGLE_EQ]);;
 527
 528 let COLLINEAR_ANGLE = prove
 529  (`!A B C. ~(A = B) /\ ~(B = C)
 530            ==> (collinear {A,B,C} <=> angle(A,B,C) = &0 \/ angle(A,B,C) = pi)`,
 531   ONCE_REWRITE_TAC[COLLINEAR_3] THEN
 532   SIMP_TAC[COLLINEAR_VECTOR_ANGLE; VECTOR_SUB_EQ; angle]);;
 533
 534 let COLLINEAR_SIN_ANGLE = prove
 535  (`!A B C. ~(A = B) /\ ~(B = C)
 536            ==> (collinear {A,B,C} <=> sin(angle(A,B,C)) = &0)`,
 537   REWRITE_TAC[SIN_ANGLE_EQ_0; COLLINEAR_ANGLE]);;
 538
 539 let COLLINEAR_SIN_ANGLE_IMP = prove
 540  (`!A B C. sin(angle(A,B,C)) = &0
 541            ==> ~(A = B) /\ ~(B = C) /\ collinear {A,B,C}`,
 542   REPEAT GEN_TAC THEN
 543   ONCE_REWRITE_TAC[COLLINEAR_3] THEN REWRITE_TAC[angle] THEN
 544   DISCH_THEN(MP_TAC o MATCH_MP COLLINEAR_SIN_VECTOR_ANGLE_IMP) THEN
 545   SIMP_TAC[VECTOR_SUB_EQ]);;
 546
 547 let ANGLE_EQ_0_RIGHT = prove
 548  (`!A B C. angle(A,B,C) = &0 ==> angle(A,B,D) = angle(C,B,D)`,
 549   REWRITE_TAC[VECTOR_ANGLE_EQ_0_RIGHT; angle]);;
 550
 551 let ANGLE_EQ_0_LEFT = prove
 552  (`!A B C. angle(A,B,C) = &0 ==> angle(D,B,A) = angle(D,B,C)`,
 553   MESON_TAC[ANGLE_EQ_0_RIGHT; ANGLE_SYM]);;
 554
 555 let ANGLE_EQ_PI_RIGHT = prove
 556  (`!A B C. angle(A,B,C) = pi ==> angle(A,B,D) = pi - angle(C,B,D)`,
 557   REWRITE_TAC[VECTOR_ANGLE_EQ_PI_RIGHT; angle]);;
 558
 559 let ANGLE_EQ_PI_LEFT = prove
 560  (`!A B C. angle(A,B,C) = pi ==> angle(A,B,D) = pi - angle(C,B,D)`,
 561   MESON_TAC[ANGLE_EQ_PI_RIGHT; ANGLE_SYM]);;
 562
 563 let COS_ANGLE = prove
 564  (`!a b c. cos(angle(a,b,c)) = if a = b \/ c = b then &0
 565                                else ((a - b) dot (c - b)) /
 566                                     (norm(a - b) * norm(c - b))`,
 567   REWRITE_TAC[angle; COS_VECTOR_ANGLE; VECTOR_SUB_EQ]);;
 568
 569 let SIN_ANGLE = prove
 570  (`!a b c. sin(angle(a,b,c)) =
 571              if a = b \/ c = b then &1
 572              else sqrt(&1 - (((a - b) dot (c - b)) /
 573                              (norm(a - b) * norm(c - b))) pow 2)`,
 574   REWRITE_TAC[angle; SIN_VECTOR_ANGLE; VECTOR_SUB_EQ]);;
 575
 576 let SIN_SQUARED_ANGLE = prove
 577  (`!a b c. sin(angle(a,b,c)) pow 2 =
 578              if a = b \/ c = b then &1
 579              else &1 - (((a - b) dot (c - b)) /
 580                         (norm(a - b) * norm(c - b))) pow 2`,
 581   REWRITE_TAC[angle; SIN_SQUARED_VECTOR_ANGLE; VECTOR_SUB_EQ]);;
 582
 583 (* ------------------------------------------------------------------------- *)
 584 (* The law of cosines.                                                       *)
 585 (* ------------------------------------------------------------------------- *)
 586
 587 let LAW_OF_COSINES = prove
 588  (`!A B C:real^N.
 589         dist(B,C) pow 2 = (dist(A,B) pow 2 + dist(A,C) pow 2) -
 590                           &2 * dist(A,B) * dist(A,C) * cos(angle(B,A,C))`,
 591   REPEAT GEN_TAC THEN
 592   REWRITE_TAC[angle; ONCE_REWRITE_RULE[NORM_SUB] dist; GSYM VECTOR_ANGLE;
 593               NORM_POW_2] THEN
 594   VECTOR_ARITH_TAC);;
 595
 596 (* ------------------------------------------------------------------------- *)
 597 (* The law of sines.                                                         *)
 598 (* ------------------------------------------------------------------------- *)
 599
 600 let LAW_OF_SINES = prove
 601  (`!A B C:real^N.
 602       sin(angle(A,B,C)) * dist(B,C) = sin(angle(B,A,C)) * dist(A,C)`,
 603   REPEAT GEN_TAC THEN MATCH_MP_TAC REAL_POW_EQ THEN EXISTS_TAC `2` THEN
 604   SIMP_TAC[SIN_ANGLE_POS; DIST_POS_LE; REAL_LE_MUL; ARITH] THEN
 605   REWRITE_TAC[REAL_POW_MUL; MATCH_MP
 606    (REAL_ARITH `x + y = &1 ==> x = &1 - y`) (SPEC_ALL SIN_CIRCLE)] THEN
 607   ASM_CASES_TAC `A:real^N = B` THEN ASM_REWRITE_TAC[ANGLE_REFL; COS_PI2] THEN
 608   RULE_ASSUM_TAC(ONCE_REWRITE_RULE[GSYM VECTOR_SUB_EQ]) THEN
 609   RULE_ASSUM_TAC(REWRITE_RULE[GSYM NORM_EQ_0]) THEN
 610   FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_RING
 611    `~(a = &0) ==> a pow 2 * x = a pow 2 * y ==> x = y`)) THEN
 612   ONCE_REWRITE_TAC[DIST_SYM] THEN REWRITE_TAC[GSYM dist] THEN
 613   GEN_REWRITE_TAC (RAND_CONV o LAND_CONV o ONCE_DEPTH_CONV) [DIST_SYM] THEN
 614   REWRITE_TAC[REAL_RING
 615    `a * (&1 - x) * b = c * (&1 - y) * d <=>
 616     a * b - a * b * x = c * d - c * d * y`] THEN
 617   REWRITE_TAC[GSYM REAL_POW_MUL; GSYM ANGLE] THEN
 618   REWRITE_TAC[REAL_POW_MUL; dist; NORM_POW_2] THEN
 619   REWRITE_TAC[DOT_LSUB; DOT_RSUB; DOT_SYM] THEN CONV_TAC REAL_RING);;
 620
 621 (* ------------------------------------------------------------------------- *)
 622 (* The sum of the angles of a triangle.                                      *)
 623 (* ------------------------------------------------------------------------- *)
 624
 625 let TRIANGLE_ANGLE_SUM_LEMMA = prove
 626  (`!A B C:real^N. ~(A = B) /\ ~(A = C) /\ ~(B = C)
 627                   ==> cos(angle(B,A,C) + angle(A,B,C) + angle(B,C,A)) = -- &1`,
 628   REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[GSYM VECTOR_SUB_EQ] THEN
 629   REWRITE_TAC[GSYM NORM_EQ_0] THEN
 630   MP_TAC(ISPECL [`A:real^N`; `B:real^N`; `C:real^N`] LAW_OF_COSINES) THEN
 631   MP_TAC(ISPECL [`B:real^N`; `A:real^N`; `C:real^N`] LAW_OF_COSINES) THEN
 632   MP_TAC(ISPECL [`C:real^N`; `B:real^N`; `A:real^N`] LAW_OF_COSINES) THEN
 633   MP_TAC(ISPECL [`A:real^N`; `B:real^N`; `C:real^N`] LAW_OF_SINES) THEN
 634   MP_TAC(ISPECL [`B:real^N`; `A:real^N`; `C:real^N`] LAW_OF_SINES) THEN
 635   MP_TAC(ISPECL [`B:real^N`; `C:real^N`; `A:real^N`] LAW_OF_SINES) THEN
 636   REWRITE_TAC[COS_ADD; SIN_ADD; dist; NORM_SUB] THEN
 637   MAP_EVERY (fun t -> MP_TAC(SPEC t SIN_CIRCLE))
 638    [`angle(B:real^N,A,C)`; `angle(A:real^N,B,C)`; `angle(B:real^N,C,A)`] THEN
 639   REWRITE_TAC[COS_ADD; SIN_ADD; ANGLE_SYM] THEN CONV_TAC REAL_RING);;
 640
 641 let COS_MINUS1_LEMMA = prove
 642  (`!x. cos(x) = -- &1 /\ &0 <= x /\ x < &3 * pi ==> x = pi`,
 643   REPEAT STRIP_TAC THEN
 644   SUBGOAL_THEN `?n. integer n /\ x = n * pi`
 645    (X_CHOOSE_THEN `nn:real` (CONJUNCTS_THEN2 ASSUME_TAC SUBST_ALL_TAC)) THEN
 646   REWRITE_TAC[GSYM SIN_EQ_0] THENL
 647    [MP_TAC(SPEC `x:real` SIN_CIRCLE) THEN ASM_REWRITE_TAC[] THEN
 648     CONV_TAC REAL_RING;
 649     ALL_TAC] THEN
 650   SUBGOAL_THEN `?n. nn = &n` (X_CHOOSE_THEN `n:num` SUBST_ALL_TAC) THENL
 651    [FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [REAL_MUL_POS_LE]) THEN
 652     SIMP_TAC[PI_POS; REAL_ARITH `&0 < p ==> ~(p < &0) /\ ~(p = &0)`] THEN
 653     ASM_MESON_TAC[INTEGER_POS; REAL_LT_LE];
 654     ALL_TAC] THEN
 655   MATCH_MP_TAC(REAL_RING `n = &1 ==> n * p = p`) THEN
 656   REWRITE_TAC[REAL_OF_NUM_EQ] THEN
 657   MATCH_MP_TAC(ARITH_RULE `n < 3 /\ ~(n = 0) /\ ~(n = 2) ==> n = 1`) THEN
 658   RULE_ASSUM_TAC(SIMP_RULE[REAL_LT_RMUL_EQ; PI_POS; REAL_OF_NUM_LT]) THEN
 659   ASM_REWRITE_TAC[] THEN CONJ_TAC THEN DISCH_THEN SUBST_ALL_TAC THEN
 660   REPEAT(POP_ASSUM MP_TAC) THEN SIMP_TAC[COS_0; REAL_MUL_LZERO; COS_NPI] THEN
 661   REAL_ARITH_TAC);;
 662
 663 let TRIANGLE_ANGLE_SUM = prove
 664  (`!A B C:real^N. ~(A = B /\ B = C /\ A = C)
 665                   ==> angle(B,A,C) + angle(A,B,C) + angle(B,C,A) = pi`,
 666   REPEAT GEN_TAC THEN MAP_EVERY ASM_CASES_TAC
 667    [`A:real^N = B`; `B:real^N = C`; `A:real^N = C`] THEN
 668   ASM_SIMP_TAC[ANGLE_REFL_MID; ANGLE_REFL; REAL_HALF; REAL_ADD_RID] THEN
 669   REPEAT(FIRST_X_ASSUM SUBST_ALL_TAC) THEN
 670   REPEAT(POP_ASSUM MP_TAC) THEN REWRITE_TAC[REAL_ADD_LID; REAL_HALF] THEN
 671   REPEAT STRIP_TAC THEN MATCH_MP_TAC COS_MINUS1_LEMMA THEN
 672   ASM_SIMP_TAC[TRIANGLE_ANGLE_SUM_LEMMA; REAL_LE_ADD; ANGLE_RANGE] THEN
 673   MATCH_MP_TAC(REAL_ARITH
 674    `&0 <= x /\ x <= p /\ &0 <= y /\ y <= p /\ &0 <= z /\ z <= p /\
 675     ~(x = p /\ y = p /\ z = p)
 676     ==> x + y + z < &3 * p`) THEN
 677   ASM_SIMP_TAC[ANGLE_RANGE] THEN REPEAT STRIP_TAC THEN
 678   REPEAT(FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [ANGLE_EQ_PI_DIST])) THEN
 679   REPEAT(FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE RAND_CONV
 680    [GSYM VECTOR_SUB_EQ])) THEN
 681   REWRITE_TAC[GSYM NORM_EQ_0; dist; NORM_SUB] THEN REAL_ARITH_TAC);;
 682
 683 (* ------------------------------------------------------------------------- *)
 684 (* A few more lemmas about angles.                                           *)
 685 (* ------------------------------------------------------------------------- *)
 686
 687 let ANGLE_EQ_PI_OTHERS = prove
 688  (`!A B C:real^N.
 689         angle(A,B,C) = pi
 690         ==> angle(B,C,A) = &0 /\ angle(A,C,B) = &0 /\
 691             angle(B,A,C) = &0 /\ angle(C,A,B) = &0`,
 692   REPEAT GEN_TAC THEN DISCH_TAC THEN
 693   FIRST_ASSUM(STRIP_ASSUME_TAC o GEN_REWRITE_RULE I [ANGLE_EQ_PI_DIST]) THEN
 694   MP_TAC(ISPECL [`A:real^N`; `B:real^N`; `C:real^N`] TRIANGLE_ANGLE_SUM) THEN
 695   ASM_REWRITE_TAC[] THEN DISCH_THEN(MP_TAC o MATCH_MP (REAL_ARITH
 696    `x + p + y = p ==> &0 <= x /\ &0 <= y ==> x = &0 /\ y = &0`)) THEN
 697   SIMP_TAC[ANGLE_RANGE; ANGLE_SYM]);;
 698
 699 let ANGLE_EQ_0_DIST = prove
 700  (`!A B C:real^N. angle(A,B,C) = &0 <=>
 701                   ~(A = B) /\ ~(C = B) /\
 702                   (dist(A,B) = dist(A,C) + dist(C,B) \/
 703                    dist(B,C) = dist(A,C) + dist(A,B))`,
 704   REPEAT GEN_TAC THEN
 705   ASM_CASES_TAC `A:real^N = B` THENL
 706    [ASM_REWRITE_TAC[angle; VECTOR_ANGLE_EQ_0; VECTOR_SUB_EQ]; ALL_TAC] THEN
 707   ASM_CASES_TAC `B:real^N = C` THENL
 708    [ASM_REWRITE_TAC[angle; VECTOR_ANGLE_EQ_0; VECTOR_SUB_EQ]; ALL_TAC] THEN
 709   ASM_CASES_TAC `A:real^N = C` THENL
 710    [ASM_SIMP_TAC[ANGLE_REFL_MID; DIST_REFL; REAL_ADD_LID]; ALL_TAC] THEN
 711   EQ_TAC THENL
 712    [ALL_TAC;
 713     STRIP_TAC THENL
 714      [MP_TAC(ISPECL[`A:real^N`; `C:real^N`; `B:real^N`] ANGLE_EQ_PI_DIST);
 715       MP_TAC(ISPECL[`B:real^N`; `A:real^N`; `C:real^N`] ANGLE_EQ_PI_DIST)] THEN
 716     ASM_REWRITE_TAC[] THEN REWRITE_TAC[DIST_SYM; REAL_ADD_AC] THEN
 717     DISCH_THEN(MP_TAC o MATCH_MP ANGLE_EQ_PI_OTHERS) THEN SIMP_TAC[]] THEN
 718   ASM_REWRITE_TAC[angle; VECTOR_ANGLE_EQ_0; VECTOR_SUB_EQ] THEN
 719   REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC
 720     (ISPECL [`norm(A - B:real^N)`; `norm(C - B:real^N)`]
 721                 REAL_LT_TOTAL)
 722   THENL
 723    [ASM_REWRITE_TAC[VECTOR_MUL_LCANCEL; NORM_EQ_0; VECTOR_SUB_EQ;
 724                     VECTOR_ARITH `c - b:real^N = a - b <=> a = c`];
 725     ONCE_REWRITE_TAC[VECTOR_ARITH
 726      `norm(A - B) % (C - B) = norm(C - B) % (A - B) <=>
 727       (norm(C - B) - norm(A - B)) % (A - B) = norm(A - B) % (C - A)`];
 728     ONCE_REWRITE_TAC[VECTOR_ARITH
 729      `norm(A - B) % (C - B) = norm(C - B) % (A - B) <=>
 730       (norm(A - B) - norm(C - B)) % (C - B) = norm(C - B) % (A - C)`]] THEN
 731   DISCH_THEN(MP_TAC o MATCH_MP
 732    (REWRITE_RULE[IMP_CONJ] NORM_CROSS_MULTIPLY)) THEN
 733   ASM_SIMP_TAC[REAL_SUB_LT; NORM_POS_LT; VECTOR_SUB_EQ] THEN
 734   SIMP_TAC[GSYM DIST_TRIANGLE_EQ] THEN SIMP_TAC[DIST_SYM]);;
 735
 736 let ANGLE_EQ_0_DIST_ABS = prove
 737  (`!A B C:real^N. angle(A,B,C) = &0 <=>
 738                   ~(A = B) /\ ~(C = B) /\
 739                    dist(A,C) = abs(dist(A,B) - dist(C,B))`,
 740   REPEAT GEN_TAC THEN REWRITE_TAC[ANGLE_EQ_0_DIST] THEN
 741   AP_TERM_TAC THEN AP_TERM_TAC THEN
 742   MP_TAC(ISPECL [`A:real^N`; `C:real^N`] DIST_POS_LE) THEN
 743   REWRITE_TAC[DIST_SYM] THEN REAL_ARITH_TAC);;
 744
 745 (* ------------------------------------------------------------------------- *)
 746 (* Some rules for congruent triangles (not necessarily in the same real^N).  *)
 747 (* ------------------------------------------------------------------------- *)
 748
 749 let CONGRUENT_TRIANGLES_SSS = prove
 750  (`!A B C:real^M A' B' C':real^N.
 751         dist(A,B) = dist(A',B') /\
 752         dist(B,C) = dist(B',C') /\
 753         dist(C,A) = dist(C',A')
 754         ==> angle(A,B,C) = angle(A',B',C')`,
 755   REPEAT GEN_TAC THEN MAP_EVERY ASM_CASES_TAC
 756    [`dist(A':real^N,B') = &0`; `dist(B':real^N,C') = &0`] THEN
 757   ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
 758   RULE_ASSUM_TAC(REWRITE_RULE[DIST_EQ_0]) THEN
 759   ASM_SIMP_TAC[ANGLE_REFL_MID; ANGLE_REFL] THEN
 760   ONCE_REWRITE_TAC[GSYM COS_ANGLE_EQ] THEN
 761   MP_TAC(ISPECL [`B:real^M`; `A:real^M`; `C:real^M`] LAW_OF_COSINES) THEN
 762   MP_TAC(ISPECL [`B':real^N`; `A':real^N`; `C':real^N`] LAW_OF_COSINES) THEN
 763   REPEAT(POP_ASSUM MP_TAC) THEN REWRITE_TAC[GSYM DIST_EQ_0; DIST_SYM] THEN
 764   CONV_TAC REAL_FIELD);;
 765
 766 let CONGRUENT_TRIANGLES_SAS = prove
 767  (`!A B C:real^M A' B' C':real^N.
 768         dist(A,B) = dist(A',B') /\
 769         angle(A,B,C) = angle(A',B',C') /\
 770         dist(B,C) = dist(B',C')
 771         ==> dist(A,C) = dist(A',C')`,
 772   REPEAT STRIP_TAC THEN REWRITE_TAC[DIST_EQ] THEN
 773   MP_TAC(ISPECL [`B:real^M`; `A:real^M`; `C:real^M`] LAW_OF_COSINES) THEN
 774   MP_TAC(ISPECL [`B':real^N`; `A':real^N`; `C':real^N`] LAW_OF_COSINES) THEN
 775   REPEAT(DISCH_THEN SUBST1_TAC) THEN
 776   REPEAT BINOP_TAC THEN ASM_MESON_TAC[DIST_SYM]);;
 777
 778 let CONGRUENT_TRIANGLES_AAS = prove
 779  (`!A B C:real^M A' B' C':real^N.
 780         angle(A,B,C) = angle(A',B',C') /\
 781         angle(B,C,A) = angle(B',C',A') /\
 782         dist(A,B) = dist(A',B') /\
 783         ~(collinear {A,B,C})
 784         ==> dist(A,C) = dist(A',C') /\ dist(B,C) = dist(B',C')`,
 785   REPEAT GEN_TAC THEN ASM_CASES_TAC `A:real^M = B` THENL
 786    [FIRST_X_ASSUM SUBST_ALL_TAC THEN REWRITE_TAC[INSERT_AC; COLLINEAR_2];
 787     ALL_TAC] THEN
 788   DISCH_TAC THEN SUBGOAL_THEN `~(A':real^N = B')` ASSUME_TAC THENL
 789    [ASM_MESON_TAC[DIST_EQ_0]; ALL_TAC] THEN
 790   SUBGOAL_THEN `angle(C:real^M,A,B) = angle(C':real^N,A',B')` ASSUME_TAC THENL
 791    [MP_TAC(ISPECL [`A:real^M`; `B:real^M`; `C:real^M`] TRIANGLE_ANGLE_SUM) THEN
 792     MP_TAC(ISPECL [`A':real^N`; `B':real^N`; `C':real^N`]
 793       TRIANGLE_ANGLE_SUM) THEN ASM_REWRITE_TAC[IMP_IMP] THEN
 794     REWRITE_TAC[ANGLE_SYM] THEN REAL_ARITH_TAC;
 795     ALL_TAC] THEN
 796   MATCH_MP_TAC(TAUT `a /\ (a ==> b) ==> a /\ b`) THEN CONJ_TAC THENL
 797    [MP_TAC(ISPECL [`C:real^M`; `B:real^M`; `A:real^M`] LAW_OF_SINES) THEN
 798     MP_TAC(ISPECL [`C':real^N`; `B':real^N`; `A':real^N`] LAW_OF_SINES) THEN
 799     SUBGOAL_THEN `~(sin(angle(B':real^N,C',A')) = &0)` MP_TAC THENL
 800      [ASM_MESON_TAC[COLLINEAR_SIN_ANGLE_IMP; INSERT_AC];
 801       ASM_REWRITE_TAC[] THEN ONCE_REWRITE_TAC[ANGLE_SYM; DIST_SYM] THEN
 802       ASM_REWRITE_TAC[] THEN REWRITE_TAC[ANGLE_SYM; DIST_SYM] THEN
 803       CONV_TAC REAL_FIELD];
 804     ASM_MESON_TAC[CONGRUENT_TRIANGLES_SAS; DIST_SYM; ANGLE_SYM]]);;
 805
 806 let CONGRUENT_TRIANGLES_ASA = prove
 807  (`!A B C:real^M A' B' C':real^N.
 808         angle(A,B,C) = angle(A',B',C') /\
 809         dist(A,B) = dist(A',B') /\
 810         angle(B,A,C) = angle(B',A',C') /\
 811         ~(collinear {A,B,C})
 812         ==> dist(A,C) = dist(A',C')`,
 813   REPEAT GEN_TAC THEN ASM_CASES_TAC `A:real^M = B` THENL
 814    [FIRST_X_ASSUM SUBST_ALL_TAC THEN REWRITE_TAC[INSERT_AC; COLLINEAR_2];
 815     ALL_TAC] THEN
 816   REPEAT STRIP_TAC THEN SUBGOAL_THEN `~(A':real^N = B')` ASSUME_TAC THENL
 817    [ASM_MESON_TAC[DIST_EQ_0]; ALL_TAC] THEN
 818   MP_TAC(ISPECL [`A:real^M`; `B:real^M`; `C:real^M`] TRIANGLE_ANGLE_SUM) THEN
 819   MP_TAC(ISPECL [`A':real^N`; `B':real^N`; `C':real^N`]
 820     TRIANGLE_ANGLE_SUM) THEN
 821   ASM_REWRITE_TAC[IMP_IMP] THEN
 822   DISCH_THEN(MP_TAC o MATCH_MP (REAL_ARITH
 823     `a + b + x = pi /\ a + b + y = pi ==> x = y`)) THEN
 824   ASM_MESON_TAC[CONGRUENT_TRIANGLES_AAS; DIST_SYM; ANGLE_SYM]);;
 825
 826 (* ------------------------------------------------------------------------- *)
 827 (* Full versions where we deduce everything from the conditions.             *)
 828 (* ------------------------------------------------------------------------- *)
 829
 830 let CONGRUENT_TRIANGLES_SSS_FULL = prove
 831  (`!A B C:real^M A' B' C':real^N.
 832         dist(A,B) = dist(A',B') /\
 833         dist(B,C) = dist(B',C') /\
 834         dist(C,A) = dist(C',A')
 835         ==> dist(A,B) = dist(A',B') /\
 836             dist(B,C) = dist(B',C') /\
 837             dist(C,A) = dist(C',A') /\
 838             angle(A,B,C) = angle(A',B',C') /\
 839             angle(B,C,A) = angle(B',C',A') /\
 840             angle(C,A,B) = angle(C',A',B')`,
 841   MESON_TAC[CONGRUENT_TRIANGLES_SSS; DIST_SYM; ANGLE_SYM]);;
 842
 843 let CONGRUENT_TRIANGLES_SAS_FULL = prove
 844  (`!A B C:real^M A' B' C':real^N.
 845         dist(A,B) = dist(A',B') /\
 846         angle(A,B,C) = angle(A',B',C') /\
 847         dist(B,C) = dist(B',C')
 848         ==> dist(A,B) = dist(A',B') /\
 849             dist(B,C) = dist(B',C') /\
 850             dist(C,A) = dist(C',A') /\
 851             angle(A,B,C) = angle(A',B',C') /\
 852             angle(B,C,A) = angle(B',C',A') /\
 853             angle(C,A,B) = angle(C',A',B')`,
 854   MESON_TAC[CONGRUENT_TRIANGLES_SSS; DIST_SYM; ANGLE_SYM;
 855             CONGRUENT_TRIANGLES_SAS]);;
 856
 857 let CONGRUENT_TRIANGLES_AAS_FULL = prove
 858  (`!A B C:real^M A' B' C':real^N.
 859         angle(A,B,C) = angle(A',B',C') /\
 860         angle(B,C,A) = angle(B',C',A') /\
 861         dist(A,B) = dist(A',B') /\
 862         ~(collinear {A,B,C})
 863         ==> dist(A,B) = dist(A',B') /\
 864             dist(B,C) = dist(B',C') /\
 865             dist(C,A) = dist(C',A') /\
 866             angle(A,B,C) = angle(A',B',C') /\
 867             angle(B,C,A) = angle(B',C',A') /\
 868             angle(C,A,B) = angle(C',A',B')`,
 869   MESON_TAC[CONGRUENT_TRIANGLES_SSS; DIST_SYM; ANGLE_SYM;
 870             CONGRUENT_TRIANGLES_AAS]);;
 871
 872 let CONGRUENT_TRIANGLES_ASA_FULL = prove
 873  (`!A B C:real^M A' B' C':real^N.
 874         angle(A,B,C) = angle(A',B',C') /\
 875         dist(A,B) = dist(A',B') /\
 876         angle(B,A,C) = angle(B',A',C') /\
 877         ~(collinear {A,B,C})
 878         ==> dist(A,B) = dist(A',B') /\
 879             dist(B,C) = dist(B',C') /\
 880             dist(C,A) = dist(C',A') /\
 881             angle(A,B,C) = angle(A',B',C') /\
 882             angle(B,C,A) = angle(B',C',A') /\
 883             angle(C,A,B) = angle(C',A',B')`,
 884   MESON_TAC[CONGRUENT_TRIANGLES_ASA; CONGRUENT_TRIANGLES_SAS_FULL;
 885             DIST_SYM; ANGLE_SYM]);;
 886
 887 (* ------------------------------------------------------------------------- *)
 888 (* Between-ness.                                                             *)
 889 (* ------------------------------------------------------------------------- *)
 890
 891 let ANGLE_BETWEEN = prove
 892  (`!a b x. angle(a,x,b) = pi <=> ~(x = a) /\ ~(x = b) /\ between x (a,b)`,
 893   REPEAT GEN_TAC THEN REWRITE_TAC[between; ANGLE_EQ_PI_DIST] THEN
 894   REWRITE_TAC[EQ_SYM_EQ]);;
 895
 896 let BETWEEN_ANGLE = prove
 897  (`!a b x. between x (a,b) <=> x = a \/ x = b \/ angle(a,x,b) = pi`,
 898   REPEAT GEN_TAC THEN REWRITE_TAC[ANGLE_BETWEEN] THEN
 899   MESON_TAC[BETWEEN_REFL]);;
 900
 901 let ANGLES_ALONG_LINE = prove
 902  (`!A B C D:real^N.
 903       ~(C = A) /\ ~(C = B) /\ between C (A,B)
 904       ==> angle(A,C,D) + angle(B,C,D) = pi`,
 905   REPEAT GEN_TAC THEN REWRITE_TAC[GSYM ANGLE_BETWEEN] THEN
 906   DISCH_THEN(SUBST1_TAC o MATCH_MP ANGLE_EQ_PI_LEFT) THEN REAL_ARITH_TAC);;
 907
 908 let ANGLES_ADD_BETWEEN = prove
 909  (`!A B C D:real^N.
 910         between C (A,B) /\ ~(D = A) /\ ~(D = B)
 911         ==> angle(A,D,C) + angle(C,D,B) = angle(A,D,B)`,
 912   REPEAT GEN_TAC THEN ASM_CASES_TAC `A:real^N = B` THENL
 913    [ASM_SIMP_TAC[BETWEEN_REFL_EQ] THEN
 914     DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
 915     ASM_SIMP_TAC[ANGLE_REFL_MID; REAL_ADD_LID];
 916     ALL_TAC] THEN
 917   ASM_CASES_TAC `C:real^N = A` THEN
 918   ASM_SIMP_TAC[ANGLE_REFL_MID; REAL_ADD_LID] THEN
 919   ASM_CASES_TAC `C:real^N = B` THEN
 920   ASM_SIMP_TAC[ANGLE_REFL_MID; REAL_ADD_RID] THEN
 921   STRIP_TAC THEN
 922   MP_TAC(ISPECL [`A:real^N`; `B:real^N`; `C:real^N`; `D:real^N`]
 923         ANGLES_ALONG_LINE) THEN
 924   MP_TAC(ISPECL [`A:real^N`; `B:real^N`; `D:real^N`] TRIANGLE_ANGLE_SUM) THEN
 925   MP_TAC(ISPECL [`A:real^N`; `C:real^N`; `D:real^N`] TRIANGLE_ANGLE_SUM) THEN
 926   MP_TAC(ISPECL [`B:real^N`; `C:real^N`; `D:real^N`] TRIANGLE_ANGLE_SUM) THEN
 927   ASM_REWRITE_TAC[] THEN
 928   SUBGOAL_THEN `angle(C:real^N,A,D) = angle(B,A,D) /\
 929                 angle(A,B,D) = angle(C,B,D)`
 930    (CONJUNCTS_THEN SUBST1_TAC)
 931   THENL [ALL_TAC; REWRITE_TAC[ANGLE_SYM] THEN REAL_ARITH_TAC] THEN
 932   CONJ_TAC THEN MATCH_MP_TAC ANGLE_EQ_0_RIGHT THEN
 933   ASM_MESON_TAC[ANGLE_EQ_PI_OTHERS; BETWEEN_ANGLE]);;