(* ========================================================================= *)
(* Some geometric notions in real^N.                                         *)
(* ========================================================================= *)

needs "Multivariate/realanalysis.ml";;

prioritize_vector();;

(* ------------------------------------------------------------------------- *)
(* Pythagoras's theorem is almost immediate.                                 *)
(* ------------------------------------------------------------------------- *)


let PYTHAGORAS = 
prove
 (`!A B C:real^N.
        orthogonal (A - B) (C - B)
        ==> norm(C - A) pow 2 = norm(B - A) pow 2 + norm(C - B) pow 2`,

  REWRITE_TAC[NORM_POW_2; orthogonal; DOT_LSUB; DOT_RSUB; DOT_SYM] THEN
  CONV_TAC REAL_RING);;

(* ------------------------------------------------------------------------- *)
(* Angle between vectors (always 0 <= angle <= pi).                          *)
(* ------------------------------------------------------------------------- *)


let vector_angle = new_definition
 `vector_angle x y = if x = vec 0 \/ y = vec 0 then pi / &2
               else acs((x dot y) / (norm x * norm y))`;;


let VECTOR_ANGLE_LINEAR_IMAGE_EQ = 
prove
 (`!f x y. linear f /\ (!x. norm(f x) = norm x)
           ==> (vector_angle (f x) (f y) = vector_angle x y)`,

  REPEAT STRIP_TAC THEN ASM_SIMP_TAC[vector_angle; GSYM NORM_EQ_0] THEN
  ASM_MESON_TAC[PRESERVES_NORM_PRESERVES_DOT]);;

add_linear_invariants [VECTOR_ANGLE_LINEAR_IMAGE_EQ];;

(* ------------------------------------------------------------------------- *)
(* Basic properties of vector angles.                                        *)
(* ------------------------------------------------------------------------- *)


let VECTOR_ANGLE_REFL = 
prove
 (`!x. vector_angle x x = if x = vec 0 then pi / &2 else &0`,

  GEN_TAC THEN REWRITE_TAC[vector_angle; DISJ_ACI] THEN
  COND_CASES_TAC THEN ASM_REWRITE_TAC[GSYM NORM_POW_2; REAL_POW_2] THEN
  ASM_SIMP_TAC[REAL_DIV_REFL; REAL_ENTIRE; NORM_EQ_0; ACS_1]);;


let VECTOR_ANGLE_SYM = 
prove
 (`!x y. vector_angle x y = vector_angle y x`,

  REWRITE_TAC[vector_angle; DISJ_SYM; DOT_SYM; REAL_MUL_SYM]);;


let VECTOR_ANGLE_LMUL = 
prove
 (`!a x y:real^N.
        vector_angle (a % x) y =
                if a = &0 then pi / &2
                else if &0 <= a then vector_angle x y
                else pi - vector_angle x y`,

  REPEAT STRIP_TAC THEN COND_CASES_TAC THEN
  ASM_REWRITE_TAC[vector_angle; VECTOR_MUL_EQ_0] THEN
  ASM_CASES_TAC `x:real^N = vec 0 \/ y:real^N = vec 0` THEN
  ASM_REWRITE_TAC[] THENL [REAL_ARITH_TAC; ALL_TAC] THEN
  REWRITE_TAC[NORM_MUL; DOT_LMUL; real_div; REAL_INV_MUL; real_abs] THEN
  COND_CASES_TAC THEN
  ASM_REWRITE_TAC[REAL_INV_NEG; REAL_MUL_LNEG; REAL_MUL_RNEG] THEN
  ASM_SIMP_TAC[REAL_FIELD
   `~(a = &0) ==> (a * x) * (inv a * y) * z = x * y * z`] THEN
  MATCH_MP_TAC ACS_NEG THEN
  REWRITE_TAC[GSYM REAL_ABS_BOUNDS; GSYM REAL_INV_MUL] THEN
  REWRITE_TAC[GSYM real_div; NORM_CAUCHY_SCHWARZ_DIV]);;


let VECTOR_ANGLE_RMUL = 
prove
 (`!a x y:real^N.
        vector_angle x (a % y) =
                if a = &0 then pi / &2
                else if &0 <= a then vector_angle x y
                else pi - vector_angle x y`,

  ONCE_REWRITE_TAC[VECTOR_ANGLE_SYM] THEN
  REWRITE_TAC[VECTOR_ANGLE_LMUL]);;


let VECTOR_ANGLE_LNEG = 
prove
 (`!x y. vector_angle (--x) y = pi - vector_angle x y`,

  REWRITE_TAC[VECTOR_ARITH `--x = -- &1 % x`; VECTOR_ANGLE_LMUL] THEN
  CONV_TAC REAL_RAT_REDUCE_CONV);;


let VECTOR_ANGLE_RNEG = 
prove
 (`!x y. vector_angle x (--y) = pi - vector_angle x y`,

  ONCE_REWRITE_TAC[VECTOR_ANGLE_SYM] THEN REWRITE_TAC[VECTOR_ANGLE_LNEG]);;


let VECTOR_ANGLE_NEG2 = 
prove
 (`!x y. vector_angle (--x) (--y) = vector_angle x y`,

  REWRITE_TAC[VECTOR_ANGLE_LNEG; VECTOR_ANGLE_RNEG] THEN REAL_ARITH_TAC);;


let VECTOR_ANGLE = 
prove
 (`!x y:real^N. x dot y = norm(x) * norm(y) * cos(vector_angle x y)`,

  REPEAT GEN_TAC THEN REWRITE_TAC[vector_angle] THEN
  ASM_CASES_TAC `x:real^N = vec 0` THEN
  ASM_REWRITE_TAC[DOT_LZERO; NORM_0; REAL_MUL_LZERO] THEN
  ASM_CASES_TAC `y:real^N = vec 0` THEN
  ASM_REWRITE_TAC[DOT_RZERO; NORM_0; REAL_MUL_LZERO; REAL_MUL_RZERO] THEN
  ONCE_REWRITE_TAC[AC REAL_MUL_AC `a * b * c:real = c * a * b`] THEN
  ASM_SIMP_TAC[GSYM REAL_EQ_LDIV_EQ; REAL_LT_MUL; NORM_POS_LT] THEN
  MATCH_MP_TAC(GSYM COS_ACS) THEN
  ASM_REWRITE_TAC[REAL_BOUNDS_LE; NORM_CAUCHY_SCHWARZ_DIV]);;


let VECTOR_ANGLE_RANGE = 
prove
 (`!x y:real^N. &0 <= vector_angle x y /\ vector_angle x y <= pi`,

  REPEAT GEN_TAC THEN REWRITE_TAC[vector_angle] THEN COND_CASES_TAC THENL
   [MP_TAC PI_POS THEN REAL_ARITH_TAC; ALL_TAC] THEN
  RULE_ASSUM_TAC(REWRITE_RULE[DE_MORGAN_THM]) THEN MATCH_MP_TAC ACS_BOUNDS THEN
  ASM_REWRITE_TAC[REAL_BOUNDS_LE; NORM_CAUCHY_SCHWARZ_DIV]);;


let ORTHOGONAL_VECTOR_ANGLE = 
prove
 (`!x y:real^N. orthogonal x y <=> vector_angle x y = pi / &2`,

  REPEAT STRIP_TAC THEN REWRITE_TAC[orthogonal; vector_angle] THEN
  ASM_CASES_TAC `x:real^N = vec 0` THEN ASM_REWRITE_TAC[DOT_LZERO] THEN
  ASM_CASES_TAC `y:real^N = vec 0` THEN ASM_REWRITE_TAC[DOT_RZERO] THEN
  EQ_TAC THENL
   [SIMP_TAC[real_div; REAL_MUL_LZERO] THEN DISCH_TAC THEN
    REWRITE_TAC[GSYM real_div; GSYM COS_PI2] THEN
    MATCH_MP_TAC ACS_COS THEN MP_TAC PI_POS THEN REAL_ARITH_TAC;
    DISCH_THEN(MP_TAC o AP_TERM `cos`) THEN
    SIMP_TAC[COS_ACS; REAL_BOUNDS_LE; NORM_CAUCHY_SCHWARZ_DIV; COS_PI2] THEN
    ASM_SIMP_TAC[REAL_EQ_LDIV_EQ; REAL_LT_MUL; NORM_POS_LT; REAL_MUL_LZERO]]);;


let VECTOR_ANGLE_EQ_0 = 
prove
 (`!x y:real^N. vector_angle x y = &0 <=>
                ~(x = vec 0) /\ ~(y = vec 0) /\ norm(x) % y = norm(y) % x`,

  REPEAT GEN_TAC THEN
  MAP_EVERY ASM_CASES_TAC [`x:real^N = vec 0`; `y:real^N = vec 0`] THEN
  ASM_SIMP_TAC[vector_angle; PI_NZ; REAL_ARITH `x / &2 = &0 <=> x = &0`] THEN
  REWRITE_TAC[GSYM NORM_CAUCHY_SCHWARZ_EQ] THEN
  GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [GSYM REAL_MUL_LID] THEN
  ASM_SIMP_TAC[GSYM REAL_EQ_LDIV_EQ; NORM_POS_LT; REAL_LT_MUL] THEN
  MESON_TAC[ACS_1; COS_ACS; REAL_BOUNDS_LE; NORM_CAUCHY_SCHWARZ_DIV; COS_0]);;


let VECTOR_ANGLE_EQ_PI = 
prove
 (`!x y:real^N. vector_angle x y = pi <=>
                ~(x = vec 0) /\ ~(y = vec 0) /\
                norm(x) % y + norm(y) % x = vec 0`,

  REPEAT GEN_TAC THEN
  MP_TAC(ISPECL [`x:real^N`; `--y:real^N`] VECTOR_ANGLE_EQ_0) THEN
  SIMP_TAC[VECTOR_ANGLE_RNEG; REAL_ARITH `pi - x = &0 <=> x = pi`] THEN
  STRIP_TAC THEN
  REWRITE_TAC[NORM_NEG; VECTOR_ARITH `--x = vec 0 <=> x = vec 0`] THEN
  AP_TERM_TAC THEN AP_TERM_TAC THEN VECTOR_ARITH_TAC);;


let VECTOR_ANGLE_EQ_0_DIST = 
prove
 (`!x y:real^N. vector_angle x y = &0 <=>
                ~(x = vec 0) /\ ~(y = vec 0) /\ norm(x + y) = norm x + norm y`,

  REWRITE_TAC[VECTOR_ANGLE_EQ_0; GSYM NORM_TRIANGLE_EQ]);;


let VECTOR_ANGLE_EQ_PI_DIST = 
prove
 (`!x y:real^N. vector_angle x y = pi <=>
                ~(x = vec 0) /\ ~(y = vec 0) /\ norm(x - y) = norm x + norm y`,

  REPEAT GEN_TAC THEN
  MP_TAC(ISPECL [`x:real^N`; `--y:real^N`] VECTOR_ANGLE_EQ_0_DIST) THEN
  SIMP_TAC[VECTOR_ANGLE_RNEG; REAL_ARITH `pi - x = &0 <=> x = pi`] THEN
  STRIP_TAC THEN REWRITE_TAC[NORM_NEG] THEN NORM_ARITH_TAC);;


let SIN_VECTOR_ANGLE_POS = 
prove
 (`!v w. &0 <= sin(vector_angle v w)`,


let SIN_VECTOR_ANGLE_EQ_0 = 
prove
 (`!x y. sin(vector_angle x y) = &0 <=>
           vector_angle x y = &0 \/ vector_angle x y = pi`,


let ASN_SIN_VECTOR_ANGLE = 
prove
 (`!x y:real^N.
        asn(sin(vector_angle x y)) =
          if vector_angle x y <= pi / &2 then vector_angle x y
          else pi - vector_angle x y`,

  REPEAT GEN_TAC THEN COND_CASES_TAC THENL
   [ALL_TAC;
    MATCH_MP_TAC EQ_TRANS THEN
    EXISTS_TAC `asn(sin(pi - vector_angle (x:real^N) y))` THEN CONJ_TAC THENL
     [AP_TERM_TAC THEN REWRITE_TAC[SIN_SUB; SIN_PI; COS_PI] THEN
      REAL_ARITH_TAC;
      ALL_TAC]] THEN
  MATCH_MP_TAC ASN_SIN THEN
  MP_TAC(ISPECL [`x:real^N`; `y:real^N`] VECTOR_ANGLE_RANGE) THEN
  ASM_REAL_ARITH_TAC);;


let SIN_VECTOR_ANGLE_EQ = 
prove
 (`!x y w z.
        sin(vector_angle x y) = sin(vector_angle w z) <=>
            vector_angle x y = vector_angle w z \/
            vector_angle x y = pi - vector_angle w z`,

  REPEAT GEN_TAC THEN EQ_TAC THEN
  STRIP_TAC THEN ASM_REWRITE_TAC[SIN_SUB; SIN_PI; COS_PI] THENL
   [ALL_TAC; REAL_ARITH_TAC] THEN
  FIRST_X_ASSUM(MP_TAC o AP_TERM `asn`) THEN
  REWRITE_TAC[ASN_SIN_VECTOR_ANGLE] THEN REAL_ARITH_TAC);;


let CONTINUOUS_WITHIN_CX_VECTOR_ANGLE_COMPOSE = 
prove
 (`!f:real^M->real^N g x s.
     ~(f x = vec 0) /\ ~(g x = vec 0) /\
     f continuous (at x within s) /\
     g continuous (at x within s)
     ==> (\x. Cx(vector_angle (f x) (g x))) continuous (at x within s)`,

  REPEAT STRIP_TAC THEN
  ASM_CASES_TAC `trivial_limit(at (x:real^M) within s)` THEN
  ASM_SIMP_TAC[CONTINUOUS_TRIVIAL_LIMIT; vector_angle] THEN
  SUBGOAL_THEN
   `(cacs o (\x. Cx(((f x:real^N) dot g x) / (norm(f x) * norm(g x)))))
    continuous (at (x:real^M) within s)`
  MP_TAC THENL
   [MATCH_MP_TAC CONTINUOUS_WITHIN_COMPOSE THEN CONJ_TAC THENL
     [REWRITE_TAC[CX_DIV; CX_MUL] THEN REWRITE_TAC[WITHIN_UNIV] THEN
      MATCH_MP_TAC CONTINUOUS_COMPLEX_DIV THEN
      ASM_SIMP_TAC[NETLIMIT_WITHIN; COMPLEX_ENTIRE; CX_INJ; NORM_EQ_0] THEN
      REWRITE_TAC[CONTINUOUS_CX_LIFT; GSYM CX_MUL; LIFT_CMUL] THEN
      ASM_SIMP_TAC[CONTINUOUS_LIFT_DOT2] THEN
      MATCH_MP_TAC CONTINUOUS_MUL THEN
      ASM_SIMP_TAC[CONTINUOUS_LIFT_NORM_COMPOSE; o_DEF];
      MATCH_MP_TAC CONTINUOUS_WITHIN_SUBSET THEN
      EXISTS_TAC `{z | real z /\ abs(Re z) <= &1}` THEN
      REWRITE_TAC[CONTINUOUS_WITHIN_CACS_REAL] THEN
      REWRITE_TAC[SUBSET; FORALL_IN_IMAGE; IN_UNIV; IN_ELIM_THM] THEN
      REWRITE_TAC[REAL_CX; RE_CX; NORM_CAUCHY_SCHWARZ_DIV]];
    ASM_SIMP_TAC[CONTINUOUS_WITHIN; CX_ACS; o_DEF;
                 NORM_CAUCHY_SCHWARZ_DIV] THEN
    MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ] LIM_TRANSFORM_EVENTUALLY) THEN
    SUBGOAL_THEN
      `eventually (\y. ~((f:real^M->real^N) y = vec 0) /\
                       ~((g:real^M->real^N) y = vec 0))
                  (at x within s)`
    MP_TAC THENL
     [REWRITE_TAC[EVENTUALLY_AND] THEN CONJ_TAC THENL
       [UNDISCH_TAC `(f:real^M->real^N) continuous (at x within s)`;
        UNDISCH_TAC `(g:real^M->real^N) continuous (at x within s)`] THEN
      REWRITE_TAC[CONTINUOUS_WITHIN; tendsto] THENL
       [DISCH_THEN(MP_TAC o SPEC `norm((f:real^M->real^N) x)`);
        DISCH_THEN(MP_TAC o SPEC `norm((g:real^M->real^N) x)`)] THEN
      ASM_REWRITE_TAC[NORM_POS_LT] THEN
      MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ] EVENTUALLY_MONO) THEN
      REWRITE_TAC[] THEN CONV_TAC NORM_ARITH;
      MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ] EVENTUALLY_MONO) THEN
      SIMP_TAC[CX_ACS; NORM_CAUCHY_SCHWARZ_DIV]]]);;


let CONTINUOUS_AT_CX_VECTOR_ANGLE = 
prove
 (`!c x:real^N. ~(x = vec 0) ==> (Cx o vector_angle c) continuous (at x)`,

  REPEAT STRIP_TAC THEN REWRITE_TAC[o_DEF; vector_angle] THEN
  ASM_CASES_TAC `c:real^N = vec 0` THEN ASM_REWRITE_TAC[CONTINUOUS_CONST] THEN
  MATCH_MP_TAC CONTINUOUS_TRANSFORM_AT THEN
  MAP_EVERY EXISTS_TAC [`\x:real^N. cacs(Cx((c dot x) / (norm c * norm x)))`;
                        `norm(x:real^N)`] THEN
  ASM_REWRITE_TAC[NORM_POS_LT] THEN CONJ_TAC THENL
   [X_GEN_TAC `z:real^N` THEN DISCH_TAC THEN COND_CASES_TAC THENL
     [ASM_MESON_TAC[NORM_ARITH `~(dist(vec 0,x) < norm x)`]; ALL_TAC] THEN
    MATCH_MP_TAC(GSYM CX_ACS) THEN REWRITE_TAC[NORM_CAUCHY_SCHWARZ_DIV];
    ALL_TAC] THEN
  ONCE_REWRITE_TAC[GSYM WITHIN_UNIV] THEN
  MATCH_MP_TAC(REWRITE_RULE[o_DEF] CONTINUOUS_WITHIN_COMPOSE) THEN
  CONJ_TAC THENL
   [REWRITE_TAC[CX_DIV; CX_MUL] THEN REWRITE_TAC[WITHIN_UNIV] THEN
    MATCH_MP_TAC CONTINUOUS_COMPLEX_DIV THEN
    ASM_REWRITE_TAC[NETLIMIT_AT; COMPLEX_ENTIRE; CX_INJ; NORM_EQ_0] THEN
    SIMP_TAC[CONTINUOUS_COMPLEX_MUL; CONTINUOUS_CONST;
             CONTINUOUS_AT_CX_NORM; CONTINUOUS_AT_CX_DOT];
    MATCH_MP_TAC CONTINUOUS_WITHIN_SUBSET THEN
    EXISTS_TAC `{z | real z /\ abs(Re z) <= &1}` THEN
    REWRITE_TAC[CONTINUOUS_WITHIN_CACS_REAL] THEN
    REWRITE_TAC[SUBSET; FORALL_IN_IMAGE; IN_UNIV; IN_ELIM_THM] THEN
    REWRITE_TAC[REAL_CX; RE_CX; NORM_CAUCHY_SCHWARZ_DIV]]);;


let CONTINUOUS_WITHIN_CX_VECTOR_ANGLE = 
prove
 (`!c x:real^N s.
     ~(x = vec 0) ==> (Cx o vector_angle c) continuous (at x within s)`,


let REAL_CONTINUOUS_AT_VECTOR_ANGLE = 
prove
 (`!c x:real^N. ~(x = vec 0) ==> (vector_angle c) real_continuous (at x)`,


let REAL_CONTINUOUS_WITHIN_VECTOR_ANGLE = 
prove
 (`!c s x:real^N. ~(x = vec 0)
                  ==> (vector_angle c) real_continuous (at x within s)`,


let CONTINUOUS_ON_CX_VECTOR_ANGLE = 
prove
 (`!s. ~(vec 0 IN s) ==> (Cx o vector_angle c) continuous_on s`,

  REPEAT STRIP_TAC THEN REWRITE_TAC[CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN] THEN
  ASM_MESON_TAC[CONTINUOUS_WITHIN_CX_VECTOR_ANGLE]);;


let VECTOR_ANGLE_EQ = 
prove
 (`!u v x y. ~(u = vec 0) /\  ~(v = vec 0) /\ ~(x = vec 0) /\ ~(y = vec 0)
             ==> (vector_angle u v = vector_angle x y <=>
                        (x dot y) * norm(u) * norm(v) =
                        (u dot v) * norm(x) * norm(y))`,

  SIMP_TAC[vector_angle; NORM_EQ_0; REAL_FIELD
   `~(u = &0) /\ ~(v = &0) /\ ~(x = &0) /\ ~(y = &0)
    ==> (a * u * v = b * x * y <=> a / (x * y) = b / (u * v))`] THEN
  REPEAT STRIP_TAC THEN EQ_TAC THEN SIMP_TAC[] THEN
  DISCH_THEN(MP_TAC o AP_TERM `cos`) THEN
  SIMP_TAC[COS_ACS; NORM_CAUCHY_SCHWARZ_DIV; REAL_BOUNDS_LE]);;


let COS_VECTOR_ANGLE_EQ = 
prove
 (`!u v x y.
        cos(vector_angle u v) = cos(vector_angle x y) <=>
        vector_angle u v = vector_angle x y`,

  MESON_TAC[ACS_COS; VECTOR_ANGLE_RANGE]);;


let COLLINEAR_VECTOR_ANGLE = 
prove
 (`!x y. ~(x = vec 0) /\ ~(y = vec 0)
         ==> (collinear {vec 0,x,y} <=>
                vector_angle x y = &0 \/ vector_angle x y = pi)`,

  REWRITE_TAC[GSYM NORM_CAUCHY_SCHWARZ_EQUAL; NORM_CAUCHY_SCHWARZ_ABS_EQ;
              VECTOR_ANGLE_EQ_0; VECTOR_ANGLE_EQ_PI] THEN
  REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN BINOP_TAC THEN
  VECTOR_ARITH_TAC);;


let COLLINEAR_SIN_VECTOR_ANGLE = 
prove
 (`!x y. ~(x = vec 0) /\ ~(y = vec 0)
         ==> (collinear {vec 0,x,y} <=> sin(vector_angle x y) = &0)`,


let COLLINEAR_SIN_VECTOR_ANGLE_IMP = 
prove
 (`!x y. sin(vector_angle x y) = &0
         ==> ~(x = vec 0) /\ ~(y = vec 0) /\ collinear {vec 0,x,y}`,


let VECTOR_ANGLE_EQ_0_RIGHT = 
prove
 (`!x y z:real^N. vector_angle x y = &0
                  ==> (vector_angle x z = vector_angle y z)`,

  REWRITE_TAC[VECTOR_ANGLE_EQ_0] THEN REPEAT STRIP_TAC THEN
  MATCH_MP_TAC EQ_TRANS THEN
  EXISTS_TAC `vector_angle (norm(x:real^N) % y) (z:real^N)` THEN CONJ_TAC THENL
   [ASM_REWRITE_TAC[] THEN
    ASM_REWRITE_TAC[VECTOR_ANGLE_LMUL; NORM_EQ_0; NORM_POS_LE];
    REWRITE_TAC[VECTOR_ANGLE_LMUL] THEN
    ASM_REWRITE_TAC[NORM_EQ_0; NORM_POS_LE]]);;


let VECTOR_ANGLE_EQ_0_LEFT = 
prove
 (`!x y z:real^N. vector_angle x y = &0
                  ==> (vector_angle z x = vector_angle z y)`,


let VECTOR_ANGLE_EQ_PI_RIGHT = 
prove
 (`!x y z:real^N. vector_angle x y = pi
                  ==> (vector_angle x z = pi - vector_angle y z)`,

  REPEAT STRIP_TAC THEN
  MP_TAC(ISPECL [`--x:real^N`; `y:real^N`; `z:real^N`]
   VECTOR_ANGLE_EQ_0_RIGHT) THEN
  ASM_REWRITE_TAC[VECTOR_ANGLE_LNEG] THEN REAL_ARITH_TAC);;


let VECTOR_ANGLE_EQ_PI_LEFT = 
prove
 (`!x y z:real^N. vector_angle x y = pi
                  ==> (vector_angle z x = pi - vector_angle z y)`,


let COS_VECTOR_ANGLE = 
prove
 (`!x y:real^N.
        cos(vector_angle x y) = if x = vec 0 \/ y = vec 0 then &0
                                else (x dot y) / (norm x * norm y)`,

  REPEAT GEN_TAC THEN
  ASM_CASES_TAC `x:real^N = vec 0` THENL
   [ASM_REWRITE_TAC[vector_angle; COS_PI2]; ALL_TAC] THEN
  ASM_CASES_TAC `y:real^N = vec 0` THENL
   [ASM_REWRITE_TAC[vector_angle; COS_PI2]; ALL_TAC] THEN
  ASM_SIMP_TAC[REAL_EQ_RDIV_EQ; REAL_LT_MUL; NORM_POS_LT; VECTOR_ANGLE] THEN
  REAL_ARITH_TAC);;


let SIN_VECTOR_ANGLE = 
prove
 (`!x y:real^N.
        sin(vector_angle x y) =
            if x = vec 0 \/ y = vec 0 then &1
            else sqrt(&1 - ((x dot y) / (norm x * norm y)) pow 2)`,

  SIMP_TAC[SIN_COS_SQRT; SIN_VECTOR_ANGLE_POS; COS_VECTOR_ANGLE] THEN
  REPEAT GEN_TAC THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
  CONV_TAC REAL_RAT_REDUCE_CONV THEN REWRITE_TAC[SQRT_1]);;


let SIN_SQUARED_VECTOR_ANGLE = 
prove
 (`!x y:real^N.
        sin(vector_angle x y) pow 2 =
            if x = vec 0 \/ y = vec 0 then &1
            else &1 - ((x dot y) / (norm x * norm y)) pow 2`,

  REPEAT GEN_TAC THEN REWRITE_TAC
   [REWRITE_RULE [REAL_ARITH `s + c = &1 <=> s = &1 - c`] SIN_CIRCLE] THEN
  REWRITE_TAC[COS_VECTOR_ANGLE] THEN REAL_ARITH_TAC);;


let VECTOR_ANGLE_COMPLEX_LMUL = 
prove
 (`!a. ~(a = Cx(&0))
       ==> vector_angle (a * x) (a * y) = vector_angle x y`,

  REPEAT STRIP_TAC THEN
  ASM_CASES_TAC `x = Cx(&0)` THENL
   [ASM_REWRITE_TAC[COMPLEX_MUL_RZERO; vector_angle; COMPLEX_VEC_0];
    ALL_TAC] THEN
  ASM_CASES_TAC `y = Cx(&0)` THENL
   [ASM_REWRITE_TAC[COMPLEX_MUL_RZERO; vector_angle; COMPLEX_VEC_0];
    ALL_TAC] THEN
  MP_TAC(ISPECL
   [`a * x:complex`; `a * y:complex`; `x:complex`; `y:complex`]
        VECTOR_ANGLE_EQ) THEN
  ASM_REWRITE_TAC[COMPLEX_VEC_0; COMPLEX_ENTIRE] THEN
  DISCH_THEN SUBST1_TAC THEN
  REWRITE_TAC[COMPLEX_NORM_MUL] THEN MATCH_MP_TAC(REAL_RING
   `a pow 2 * xy:real = d ==> xy * (a * x) * (a * y) = d * x * y`) THEN
  REWRITE_TAC[NORM_POW_2] THEN
  REWRITE_TAC[DOT_2; complex_mul; GSYM RE_DEF; GSYM IM_DEF; RE; IM] THEN
  REAL_ARITH_TAC);;


let VECTOR_ANGLE_1 = 
prove
 (`!x. vector_angle x (Cx(&1)) = acs(Re x / norm x)`,

  GEN_TAC THEN
  SIMP_TAC[vector_angle; COMPLEX_VEC_0; CX_INJ; REAL_OF_NUM_EQ; ARITH_EQ] THEN
  COND_CASES_TAC THENL
   [ASM_REWRITE_TAC[real_div; RE_CX; ACS_0; REAL_MUL_LZERO]; ALL_TAC] THEN
  REWRITE_TAC[COMPLEX_NORM_CX; REAL_ABS_NUM; REAL_MUL_RID] THEN
  REWRITE_TAC[DOT_2; GSYM RE_DEF; GSYM IM_DEF; RE_CX; IM_CX] THEN
  AP_TERM_TAC THEN REAL_ARITH_TAC);;


let ARG_EQ_VECTOR_ANGLE_1 = 
prove
 (`!z. ~(z = Cx(&0)) /\ &0 <= Im z ==> Arg z = vector_angle z (Cx(&1))`,

  REPEAT STRIP_TAC THEN REWRITE_TAC[VECTOR_ANGLE_1] THEN
  GEN_REWRITE_TAC (RAND_CONV o RAND_CONV o LAND_CONV o RAND_CONV) [ARG] THEN
  REWRITE_TAC[RE_MUL_CX; RE_CEXP; RE_II; IM_MUL_II; IM_CX; RE_CX] THEN
  REWRITE_TAC[REAL_MUL_LZERO; REAL_EXP_0; REAL_MUL_LID] THEN
  ASM_SIMP_TAC[COMPLEX_NORM_ZERO; REAL_FIELD
   `~(z = &0) ==> (z * x) / z = x`] THEN
  CONV_TAC SYM_CONV THEN MATCH_MP_TAC ACS_COS THEN
  ASM_REWRITE_TAC[ARG; ARG_LE_PI]);;


let VECTOR_ANGLE_ARG = 
prove
 (`!w z. ~(w = Cx(&0)) /\ ~(z = Cx(&0))
         ==> vector_angle w z = if &0 <= Im(z / w) then Arg(z / w)
                                else &2 * pi - Arg(z / w)`,

  REPEAT STRIP_TAC THEN COND_CASES_TAC THENL
   [SUBGOAL_THEN `z = w * (z / w) /\ w = w * Cx(&1)` MP_TAC THENL
     [REPEAT(POP_ASSUM MP_TAC) THEN CONV_TAC COMPLEX_FIELD; ALL_TAC];
    SUBGOAL_THEN `w = z * (w / z) /\ z = z * Cx(&1)` MP_TAC THENL
     [REPEAT(POP_ASSUM MP_TAC) THEN CONV_TAC COMPLEX_FIELD; ALL_TAC]] THEN
  DISCH_THEN(fun th -> GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [th]) THEN
  ASM_SIMP_TAC[VECTOR_ANGLE_COMPLEX_LMUL] THENL
   [ONCE_REWRITE_TAC[VECTOR_ANGLE_SYM] THEN CONV_TAC SYM_CONV THEN
    MATCH_MP_TAC ARG_EQ_VECTOR_ANGLE_1 THEN ASM_REWRITE_TAC[] THEN
    REPEAT(POP_ASSUM MP_TAC) THEN CONV_TAC COMPLEX_FIELD;
    MP_TAC(ISPEC `z / w:complex` ARG_INV) THEN ANTS_TAC THENL
     [ASM_MESON_TAC[real; REAL_LE_REFL]; DISCH_THEN(SUBST1_TAC o SYM)] THEN
    REWRITE_TAC[COMPLEX_INV_DIV] THEN CONV_TAC SYM_CONV THEN
    MATCH_MP_TAC ARG_EQ_VECTOR_ANGLE_1 THEN CONJ_TAC THENL
     [REPEAT(POP_ASSUM MP_TAC) THEN CONV_TAC COMPLEX_FIELD;
      ONCE_REWRITE_TAC[GSYM COMPLEX_INV_DIV] THEN
      REWRITE_TAC[IM_COMPLEX_INV_GE_0] THEN ASM_REAL_ARITH_TAC]]);;

(* ------------------------------------------------------------------------- *)
(* Traditional geometric notion of angle (always 0 <= theta <= pi).          *)
(* ------------------------------------------------------------------------- *)


let angle = new_definition
 `angle(a,b,c) = vector_angle (a - b) (c - b)`;;


let ANGLE_LINEAR_IMAGE_EQ = 
prove
 (`!f a b c.
        linear f /\ (!x. norm(f x) = norm x)
        ==> angle(f a,f b,f c) = angle(a,b,c)`,

  SIMP_TAC[angle; GSYM LINEAR_SUB; VECTOR_ANGLE_LINEAR_IMAGE_EQ]);;

add_linear_invariants [ANGLE_LINEAR_IMAGE_EQ];;


let ANGLE_TRANSLATION_EQ = 
prove
 (`!a b c d. angle(a + b,a + c,a + d) = angle(b,c,d)`,

  REPEAT GEN_TAC THEN REWRITE_TAC[angle] THEN
  BINOP_TAC THEN VECTOR_ARITH_TAC);;

add_translation_invariants [ANGLE_TRANSLATION_EQ];;


let VECTOR_ANGLE_ANGLE = 
prove
 (`vector_angle x y = angle(x,vec 0,y)`,

  REWRITE_TAC[angle; VECTOR_SUB_RZERO]);;


let ANGLE_EQ_PI_DIST = 
prove
 (`!A B C:real^N.
        angle(A,B,C) = pi <=>
        ~(A = B) /\ ~(C = B) /\ dist(A,C) = dist(A,B) + dist(B,C)`,

  REWRITE_TAC[angle; VECTOR_ANGLE_EQ_PI_DIST] THEN NORM_ARITH_TAC);;


let SIN_ANGLE_POS = 
prove
 (`!A B C. &0 <= sin(angle(A,B,C))`,

  REWRITE_TAC[angle; SIN_VECTOR_ANGLE_POS]);;


let ANGLE = 
prove
 (`!A B C. (A - C) dot (B - C) = dist(A,C) * dist(B,C) * cos(angle(A,C,B))`,

  REWRITE_TAC[angle; dist; GSYM VECTOR_ANGLE]);;


let ANGLE_REFL = 
prove
 (`!A B. angle(A,A,B) = pi / &2 /\ angle(B,A,A) = pi / &2`,

  REWRITE_TAC[angle; vector_angle; VECTOR_SUB_REFL]);;


let ANGLE_REFL_MID = 
prove
 (`!A B. ~(A = B) ==> angle(A,B,A) = &0`,

  SIMP_TAC[angle; vector_angle; VECTOR_SUB_EQ; GSYM NORM_POW_2; ARITH;
    GSYM REAL_POW_2; REAL_DIV_REFL; ACS_1; REAL_POW_EQ_0; NORM_EQ_0]);;


let ANGLE_SYM = 
prove
 (`!A B C. angle(A,B,C) = angle(C,B,A)`,

  REWRITE_TAC[angle; vector_angle; VECTOR_SUB_EQ; DISJ_SYM;
              REAL_MUL_SYM; DOT_SYM]);;


let ANGLE_RANGE = 
prove
 (`!A B C. &0 <= angle(A,B,C) /\ angle(A,B,C) <= pi`,

  REWRITE_TAC[angle; VECTOR_ANGLE_RANGE]);;


let COS_ANGLE_EQ = 
prove
 (`!a b c a' b' c'.
        cos(angle(a,b,c)) = cos(angle(a',b',c')) <=>
        angle(a,b,c) = angle(a',b',c')`,

  REWRITE_TAC[angle; COS_VECTOR_ANGLE_EQ]);;


let ANGLE_EQ = 
prove
 (`!a b c a' b' c'.
        ~(a = b) /\ ~(c = b) /\ ~(a' = b') /\ ~(c' = b')
        ==> (angle(a,b,c) = angle(a',b',c') <=>
                ((a' - b') dot (c' - b')) * norm (a - b) * norm (c - b) =
                ((a - b) dot (c - b)) * norm (a' - b') * norm (c' - b'))`,

  SIMP_TAC[angle; VECTOR_ANGLE_EQ; VECTOR_SUB_EQ]);;


let SIN_ANGLE_EQ_0 = 
prove
 (`!A B C. sin(angle(A,B,C)) = &0 <=> angle(A,B,C) = &0 \/ angle(A,B,C) = pi`,

  REWRITE_TAC[angle; SIN_VECTOR_ANGLE_EQ_0]);;


let SIN_ANGLE_EQ = 
prove
 (`!A B C A' B' C'. sin(angle(A,B,C)) = sin(angle(A',B',C')) <=>
                        angle(A,B,C) = angle(A',B',C') \/
                        angle(A,B,C) = pi - angle(A',B',C')`,

  REWRITE_TAC[angle; SIN_VECTOR_ANGLE_EQ]);;


let COLLINEAR_ANGLE = 
prove
 (`!A B C. ~(A = B) /\ ~(B = C)
           ==> (collinear {A,B,C} <=> angle(A,B,C) = &0 \/ angle(A,B,C) = pi)`,

  ONCE_REWRITE_TAC[COLLINEAR_3] THEN
  SIMP_TAC[COLLINEAR_VECTOR_ANGLE; VECTOR_SUB_EQ; angle]);;


let COLLINEAR_SIN_ANGLE = 
prove
 (`!A B C. ~(A = B) /\ ~(B = C)
           ==> (collinear {A,B,C} <=> sin(angle(A,B,C)) = &0)`,


let COLLINEAR_SIN_ANGLE_IMP = 
prove
 (`!A B C. sin(angle(A,B,C)) = &0
           ==> ~(A = B) /\ ~(B = C) /\ collinear {A,B,C}`,

  REPEAT GEN_TAC THEN
  ONCE_REWRITE_TAC[COLLINEAR_3] THEN REWRITE_TAC[angle] THEN
  DISCH_THEN(MP_TAC o MATCH_MP COLLINEAR_SIN_VECTOR_ANGLE_IMP) THEN
  SIMP_TAC[VECTOR_SUB_EQ]);;


let ANGLE_EQ_0_RIGHT = 
prove
 (`!A B C. angle(A,B,C) = &0 ==> angle(A,B,D) = angle(C,B,D)`,

  REWRITE_TAC[VECTOR_ANGLE_EQ_0_RIGHT; angle]);;


let ANGLE_EQ_0_LEFT = 
prove
 (`!A B C. angle(A,B,C) = &0 ==> angle(D,B,A) = angle(D,B,C)`,

  MESON_TAC[ANGLE_EQ_0_RIGHT; ANGLE_SYM]);;


let ANGLE_EQ_PI_RIGHT = 
prove
 (`!A B C. angle(A,B,C) = pi ==> angle(A,B,D) = pi - angle(C,B,D)`,

  REWRITE_TAC[VECTOR_ANGLE_EQ_PI_RIGHT; angle]);;


let ANGLE_EQ_PI_LEFT = 
prove
 (`!A B C. angle(A,B,C) = pi ==> angle(A,B,D) = pi - angle(C,B,D)`,


let COS_ANGLE = 
prove
 (`!a b c. cos(angle(a,b,c)) = if a = b \/ c = b then &0
                               else ((a - b) dot (c - b)) /
                                    (norm(a - b) * norm(c - b))`,

  REWRITE_TAC[angle; COS_VECTOR_ANGLE; VECTOR_SUB_EQ]);;


let SIN_ANGLE = 
prove
 (`!a b c. sin(angle(a,b,c)) =
             if a = b \/ c = b then &1
             else sqrt(&1 - (((a - b) dot (c - b)) /
                             (norm(a - b) * norm(c - b))) pow 2)`,

  REWRITE_TAC[angle; SIN_VECTOR_ANGLE; VECTOR_SUB_EQ]);;


let SIN_SQUARED_ANGLE = 
prove
 (`!a b c. sin(angle(a,b,c)) pow 2 =
             if a = b \/ c = b then &1
             else &1 - (((a - b) dot (c - b)) /
                        (norm(a - b) * norm(c - b))) pow 2`,

  REWRITE_TAC[angle; SIN_SQUARED_VECTOR_ANGLE; VECTOR_SUB_EQ]);;

(* ------------------------------------------------------------------------- *)
(* The law of cosines.                                                       *)
(* ------------------------------------------------------------------------- *)


let LAW_OF_COSINES = 
prove
 (`!A B C:real^N.
        dist(B,C) pow 2 = (dist(A,B) pow 2 + dist(A,C) pow 2) -
                          &2 * dist(A,B) * dist(A,C) * cos(angle(B,A,C))`,

  REPEAT GEN_TAC THEN
  REWRITE_TAC[angle; ONCE_REWRITE_RULE[NORM_SUB] dist; GSYM VECTOR_ANGLE;
              NORM_POW_2] THEN
  VECTOR_ARITH_TAC);;

(* ------------------------------------------------------------------------- *)
(* The law of sines.                                                         *)
(* ------------------------------------------------------------------------- *)


let LAW_OF_SINES = 
prove
 (`!A B C:real^N.
      sin(angle(A,B,C)) * dist(B,C) = sin(angle(B,A,C)) * dist(A,C)`,

  REPEAT GEN_TAC THEN MATCH_MP_TAC REAL_POW_EQ THEN EXISTS_TAC `2` THEN
  SIMP_TAC[SIN_ANGLE_POS; DIST_POS_LE; REAL_LE_MUL; ARITH] THEN
  REWRITE_TAC[REAL_POW_MUL; MATCH_MP
   (REAL_ARITH `x + y = &1 ==> x = &1 - y`) (SPEC_ALL SIN_CIRCLE)] THEN
  ASM_CASES_TAC `A:real^N = B` THEN ASM_REWRITE_TAC[ANGLE_REFL; COS_PI2] THEN
  RULE_ASSUM_TAC(ONCE_REWRITE_RULE[GSYM VECTOR_SUB_EQ]) THEN
  RULE_ASSUM_TAC(REWRITE_RULE[GSYM NORM_EQ_0]) THEN
  FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_RING
   `~(a = &0) ==> a pow 2 * x = a pow 2 * y ==> x = y`)) THEN
  ONCE_REWRITE_TAC[DIST_SYM] THEN REWRITE_TAC[GSYM dist] THEN
  GEN_REWRITE_TAC (RAND_CONV o LAND_CONV o ONCE_DEPTH_CONV) [DIST_SYM] THEN
  REWRITE_TAC[REAL_RING
   `a * (&1 - x) * b = c * (&1 - y) * d <=>
    a * b - a * b * x = c * d - c * d * y`] THEN
  REWRITE_TAC[GSYM REAL_POW_MUL; GSYM ANGLE] THEN
  REWRITE_TAC[REAL_POW_MUL; dist; NORM_POW_2] THEN
  REWRITE_TAC[DOT_LSUB; DOT_RSUB; DOT_SYM] THEN CONV_TAC REAL_RING);;

(* ------------------------------------------------------------------------- *)
(* The sum of the angles of a triangle.                                      *)
(* ------------------------------------------------------------------------- *)


let TRIANGLE_ANGLE_SUM_LEMMA = 
prove
 (`!A B C:real^N. ~(A = B) /\ ~(A = C) /\ ~(B = C)
                  ==> cos(angle(B,A,C) + angle(A,B,C) + angle(B,C,A)) = -- &1`,

  REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[GSYM VECTOR_SUB_EQ] THEN
  REWRITE_TAC[GSYM NORM_EQ_0] THEN
  MP_TAC(ISPECL [`A:real^N`; `B:real^N`; `C:real^N`] LAW_OF_COSINES) THEN
  MP_TAC(ISPECL [`B:real^N`; `A:real^N`; `C:real^N`] LAW_OF_COSINES) THEN
  MP_TAC(ISPECL [`C:real^N`; `B:real^N`; `A:real^N`] LAW_OF_COSINES) THEN
  MP_TAC(ISPECL [`A:real^N`; `B:real^N`; `C:real^N`] LAW_OF_SINES) THEN
  MP_TAC(ISPECL [`B:real^N`; `A:real^N`; `C:real^N`] LAW_OF_SINES) THEN
  MP_TAC(ISPECL [`B:real^N`; `C:real^N`; `A:real^N`] LAW_OF_SINES) THEN
  REWRITE_TAC[COS_ADD; SIN_ADD; dist; NORM_SUB] THEN
  MAP_EVERY (fun t -> MP_TAC(SPEC t SIN_CIRCLE))
   [`angle(B:real^N,A,C)`; `angle(A:real^N,B,C)`; `angle(B:real^N,C,A)`] THEN
  REWRITE_TAC[COS_ADD; SIN_ADD; ANGLE_SYM] THEN CONV_TAC REAL_RING);;


let COS_MINUS1_LEMMA = 
prove
 (`!x. cos(x) = -- &1 /\ &0 <= x /\ x < &3 * pi ==> x = pi`,

  REPEAT STRIP_TAC THEN
  SUBGOAL_THEN `?n. integer n /\ x = n * pi`
   (X_CHOOSE_THEN `nn:real` (CONJUNCTS_THEN2 ASSUME_TAC SUBST_ALL_TAC)) THEN
  REWRITE_TAC[GSYM SIN_EQ_0] THENL
   [MP_TAC(SPEC `x:real` SIN_CIRCLE) THEN ASM_REWRITE_TAC[] THEN
    CONV_TAC REAL_RING;
    ALL_TAC] THEN
  SUBGOAL_THEN `?n. nn = &n` (X_CHOOSE_THEN `n:num` SUBST_ALL_TAC) THENL
   [FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [REAL_MUL_POS_LE]) THEN
    SIMP_TAC[PI_POS; REAL_ARITH `&0 < p ==> ~(p < &0) /\ ~(p = &0)`] THEN
    ASM_MESON_TAC[INTEGER_POS; REAL_LT_LE];
    ALL_TAC] THEN
  MATCH_MP_TAC(REAL_RING `n = &1 ==> n * p = p`) THEN
  REWRITE_TAC[REAL_OF_NUM_EQ] THEN
  MATCH_MP_TAC(ARITH_RULE `n < 3 /\ ~(n = 0) /\ ~(n = 2) ==> n = 1`) THEN
  RULE_ASSUM_TAC(SIMP_RULE[REAL_LT_RMUL_EQ; PI_POS; REAL_OF_NUM_LT]) THEN
  ASM_REWRITE_TAC[] THEN CONJ_TAC THEN DISCH_THEN SUBST_ALL_TAC THEN
  REPEAT(POP_ASSUM MP_TAC) THEN SIMP_TAC[COS_0; REAL_MUL_LZERO; COS_NPI] THEN
  REAL_ARITH_TAC);;


let TRIANGLE_ANGLE_SUM = 
prove
 (`!A B C:real^N. ~(A = B /\ B = C /\ A = C)
                  ==> angle(B,A,C) + angle(A,B,C) + angle(B,C,A) = pi`,

  REPEAT GEN_TAC THEN MAP_EVERY ASM_CASES_TAC
   [`A:real^N = B`; `B:real^N = C`; `A:real^N = C`] THEN
  ASM_SIMP_TAC[ANGLE_REFL_MID; ANGLE_REFL; REAL_HALF; REAL_ADD_RID] THEN
  REPEAT(FIRST_X_ASSUM SUBST_ALL_TAC) THEN
  REPEAT(POP_ASSUM MP_TAC) THEN REWRITE_TAC[REAL_ADD_LID; REAL_HALF] THEN
  REPEAT STRIP_TAC THEN MATCH_MP_TAC COS_MINUS1_LEMMA THEN
  ASM_SIMP_TAC[TRIANGLE_ANGLE_SUM_LEMMA; REAL_LE_ADD; ANGLE_RANGE] THEN
  MATCH_MP_TAC(REAL_ARITH
   `&0 <= x /\ x <= p /\ &0 <= y /\ y <= p /\ &0 <= z /\ z <= p /\
    ~(x = p /\ y = p /\ z = p)
    ==> x + y + z < &3 * p`) THEN
  ASM_SIMP_TAC[ANGLE_RANGE] THEN REPEAT STRIP_TAC THEN
  REPEAT(FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [ANGLE_EQ_PI_DIST])) THEN
  REPEAT(FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE RAND_CONV
   [GSYM VECTOR_SUB_EQ])) THEN
  REWRITE_TAC[GSYM NORM_EQ_0; dist; NORM_SUB] THEN REAL_ARITH_TAC);;

(* ------------------------------------------------------------------------- *)
(* A few more lemmas about angles.                                           *)
(* ------------------------------------------------------------------------- *)


let ANGLE_EQ_PI_OTHERS = 
prove
 (`!A B C:real^N.
        angle(A,B,C) = pi
        ==> angle(B,C,A) = &0 /\ angle(A,C,B) = &0 /\
            angle(B,A,C) = &0 /\ angle(C,A,B) = &0`,

  REPEAT GEN_TAC THEN DISCH_TAC THEN
  FIRST_ASSUM(STRIP_ASSUME_TAC o GEN_REWRITE_RULE I [ANGLE_EQ_PI_DIST]) THEN
  MP_TAC(ISPECL [`A:real^N`; `B:real^N`; `C:real^N`] TRIANGLE_ANGLE_SUM) THEN
  ASM_REWRITE_TAC[] THEN DISCH_THEN(MP_TAC o MATCH_MP (REAL_ARITH
   `x + p + y = p ==> &0 <= x /\ &0 <= y ==> x = &0 /\ y = &0`)) THEN
  SIMP_TAC[ANGLE_RANGE; ANGLE_SYM]);;


let ANGLE_EQ_0_DIST = 
prove
 (`!A B C:real^N. angle(A,B,C) = &0 <=>
                  ~(A = B) /\ ~(C = B) /\
                  (dist(A,B) = dist(A,C) + dist(C,B) \/
                   dist(B,C) = dist(A,C) + dist(A,B))`,

  REPEAT GEN_TAC THEN
  ASM_CASES_TAC `A:real^N = B` THENL
   [ASM_REWRITE_TAC[angle; VECTOR_ANGLE_EQ_0; VECTOR_SUB_EQ]; ALL_TAC] THEN
  ASM_CASES_TAC `B:real^N = C` THENL
   [ASM_REWRITE_TAC[angle; VECTOR_ANGLE_EQ_0; VECTOR_SUB_EQ]; ALL_TAC] THEN
  ASM_CASES_TAC `A:real^N = C` THENL
   [ASM_SIMP_TAC[ANGLE_REFL_MID; DIST_REFL; REAL_ADD_LID]; ALL_TAC] THEN
  EQ_TAC THENL
   [ALL_TAC;
    STRIP_TAC THENL
     [MP_TAC(ISPECL[`A:real^N`; `C:real^N`; `B:real^N`] ANGLE_EQ_PI_DIST);
      MP_TAC(ISPECL[`B:real^N`; `A:real^N`; `C:real^N`] ANGLE_EQ_PI_DIST)] THEN
    ASM_REWRITE_TAC[] THEN REWRITE_TAC[DIST_SYM; REAL_ADD_AC] THEN
    DISCH_THEN(MP_TAC o MATCH_MP ANGLE_EQ_PI_OTHERS) THEN SIMP_TAC[]] THEN
  ASM_REWRITE_TAC[angle; VECTOR_ANGLE_EQ_0; VECTOR_SUB_EQ] THEN
  REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC
    (ISPECL [`norm(A - B:real^N)`; `norm(C - B:real^N)`]
                REAL_LT_TOTAL)
  THENL
   [ASM_REWRITE_TAC[VECTOR_MUL_LCANCEL; NORM_EQ_0; VECTOR_SUB_EQ;
                    VECTOR_ARITH `c - b:real^N = a - b <=> a = c`];
    ONCE_REWRITE_TAC[VECTOR_ARITH
     `norm(A - B) % (C - B) = norm(C - B) % (A - B) <=>
      (norm(C - B) - norm(A - B)) % (A - B) = norm(A - B) % (C - A)`];
    ONCE_REWRITE_TAC[VECTOR_ARITH
     `norm(A - B) % (C - B) = norm(C - B) % (A - B) <=>
      (norm(A - B) - norm(C - B)) % (C - B) = norm(C - B) % (A - C)`]] THEN
  DISCH_THEN(MP_TAC o MATCH_MP
   (REWRITE_RULE[IMP_CONJ] NORM_CROSS_MULTIPLY)) THEN
  ASM_SIMP_TAC[REAL_SUB_LT; NORM_POS_LT; VECTOR_SUB_EQ] THEN
  SIMP_TAC[GSYM DIST_TRIANGLE_EQ] THEN SIMP_TAC[DIST_SYM]);;


let ANGLE_EQ_0_DIST_ABS = 
prove
 (`!A B C:real^N. angle(A,B,C) = &0 <=>
                  ~(A = B) /\ ~(C = B) /\
                   dist(A,C) = abs(dist(A,B) - dist(C,B))`,

  REPEAT GEN_TAC THEN REWRITE_TAC[ANGLE_EQ_0_DIST] THEN
  AP_TERM_TAC THEN AP_TERM_TAC THEN
  MP_TAC(ISPECL [`A:real^N`; `C:real^N`] DIST_POS_LE) THEN
  REWRITE_TAC[DIST_SYM] THEN REAL_ARITH_TAC);;

(* ------------------------------------------------------------------------- *)
(* Some rules for congruent triangles (not necessarily in the same real^N).  *)
(* ------------------------------------------------------------------------- *)


let CONGRUENT_TRIANGLES_SSS = 
prove
 (`!A B C:real^M A' B' C':real^N.
        dist(A,B) = dist(A',B') /\
        dist(B,C) = dist(B',C') /\
        dist(C,A) = dist(C',A')
        ==> angle(A,B,C) = angle(A',B',C')`,

  REPEAT GEN_TAC THEN MAP_EVERY ASM_CASES_TAC
   [`dist(A':real^N,B') = &0`; `dist(B':real^N,C') = &0`] THEN
  ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
  RULE_ASSUM_TAC(REWRITE_RULE[DIST_EQ_0]) THEN
  ASM_SIMP_TAC[ANGLE_REFL_MID; ANGLE_REFL] THEN
  ONCE_REWRITE_TAC[GSYM COS_ANGLE_EQ] THEN
  MP_TAC(ISPECL [`B:real^M`; `A:real^M`; `C:real^M`] LAW_OF_COSINES) THEN
  MP_TAC(ISPECL [`B':real^N`; `A':real^N`; `C':real^N`] LAW_OF_COSINES) THEN
  REPEAT(POP_ASSUM MP_TAC) THEN REWRITE_TAC[GSYM DIST_EQ_0; DIST_SYM] THEN
  CONV_TAC REAL_FIELD);;


let CONGRUENT_TRIANGLES_SAS = 
prove
 (`!A B C:real^M A' B' C':real^N.
        dist(A,B) = dist(A',B') /\
        angle(A,B,C) = angle(A',B',C') /\
        dist(B,C) = dist(B',C')
        ==> dist(A,C) = dist(A',C')`,

  REPEAT STRIP_TAC THEN REWRITE_TAC[DIST_EQ] THEN
  MP_TAC(ISPECL [`B:real^M`; `A:real^M`; `C:real^M`] LAW_OF_COSINES) THEN
  MP_TAC(ISPECL [`B':real^N`; `A':real^N`; `C':real^N`] LAW_OF_COSINES) THEN
  REPEAT(DISCH_THEN SUBST1_TAC) THEN
  REPEAT BINOP_TAC THEN ASM_MESON_TAC[DIST_SYM]);;


let CONGRUENT_TRIANGLES_AAS = 
prove
 (`!A B C:real^M A' B' C':real^N.
        angle(A,B,C) = angle(A',B',C') /\
        angle(B,C,A) = angle(B',C',A') /\
        dist(A,B) = dist(A',B') /\
        ~(collinear {A,B,C})
        ==> dist(A,C) = dist(A',C') /\ dist(B,C) = dist(B',C')`,

  REPEAT GEN_TAC THEN ASM_CASES_TAC `A:real^M = B` THENL
   [FIRST_X_ASSUM SUBST_ALL_TAC THEN REWRITE_TAC[INSERT_AC; COLLINEAR_2];
    ALL_TAC] THEN
  DISCH_TAC THEN SUBGOAL_THEN `~(A':real^N = B')` ASSUME_TAC THENL
   [ASM_MESON_TAC[DIST_EQ_0]; ALL_TAC] THEN
  SUBGOAL_THEN `angle(C:real^M,A,B) = angle(C':real^N,A',B')` ASSUME_TAC THENL
   [MP_TAC(ISPECL [`A:real^M`; `B:real^M`; `C:real^M`] TRIANGLE_ANGLE_SUM) THEN
    MP_TAC(ISPECL [`A':real^N`; `B':real^N`; `C':real^N`]
      TRIANGLE_ANGLE_SUM) THEN ASM_REWRITE_TAC[IMP_IMP] THEN
    REWRITE_TAC[ANGLE_SYM] THEN REAL_ARITH_TAC;
    ALL_TAC] THEN
  MATCH_MP_TAC(TAUT `a /\ (a ==> b) ==> a /\ b`) THEN CONJ_TAC THENL
   [MP_TAC(ISPECL [`C:real^M`; `B:real^M`; `A:real^M`] LAW_OF_SINES) THEN
    MP_TAC(ISPECL [`C':real^N`; `B':real^N`; `A':real^N`] LAW_OF_SINES) THEN
    SUBGOAL_THEN `~(sin(angle(B':real^N,C',A')) = &0)` MP_TAC THENL
     [ASM_MESON_TAC[COLLINEAR_SIN_ANGLE_IMP; INSERT_AC];
      ASM_REWRITE_TAC[] THEN ONCE_REWRITE_TAC[ANGLE_SYM; DIST_SYM] THEN
      ASM_REWRITE_TAC[] THEN REWRITE_TAC[ANGLE_SYM; DIST_SYM] THEN
      CONV_TAC REAL_FIELD];
    ASM_MESON_TAC[CONGRUENT_TRIANGLES_SAS; DIST_SYM; ANGLE_SYM]]);;


let CONGRUENT_TRIANGLES_ASA = 
prove
 (`!A B C:real^M A' B' C':real^N.
        angle(A,B,C) = angle(A',B',C') /\
        dist(A,B) = dist(A',B') /\
        angle(B,A,C) = angle(B',A',C') /\
        ~(collinear {A,B,C})
        ==> dist(A,C) = dist(A',C')`,

  REPEAT GEN_TAC THEN ASM_CASES_TAC `A:real^M = B` THENL
   [FIRST_X_ASSUM SUBST_ALL_TAC THEN REWRITE_TAC[INSERT_AC; COLLINEAR_2];
    ALL_TAC] THEN
  REPEAT STRIP_TAC THEN SUBGOAL_THEN `~(A':real^N = B')` ASSUME_TAC THENL
   [ASM_MESON_TAC[DIST_EQ_0]; ALL_TAC] THEN
  MP_TAC(ISPECL [`A:real^M`; `B:real^M`; `C:real^M`] TRIANGLE_ANGLE_SUM) THEN
  MP_TAC(ISPECL [`A':real^N`; `B':real^N`; `C':real^N`]
    TRIANGLE_ANGLE_SUM) THEN
  ASM_REWRITE_TAC[IMP_IMP] THEN
  DISCH_THEN(MP_TAC o MATCH_MP (REAL_ARITH
    `a + b + x = pi /\ a + b + y = pi ==> x = y`)) THEN
  ASM_MESON_TAC[CONGRUENT_TRIANGLES_AAS; DIST_SYM; ANGLE_SYM]);;

(* ------------------------------------------------------------------------- *)
(* Full versions where we deduce everything from the conditions.             *)
(* ------------------------------------------------------------------------- *)


let CONGRUENT_TRIANGLES_SSS_FULL = 
prove
 (`!A B C:real^M A' B' C':real^N.
        dist(A,B) = dist(A',B') /\
        dist(B,C) = dist(B',C') /\
        dist(C,A) = dist(C',A')
        ==> dist(A,B) = dist(A',B') /\
            dist(B,C) = dist(B',C') /\
            dist(C,A) = dist(C',A') /\
            angle(A,B,C) = angle(A',B',C') /\
            angle(B,C,A) = angle(B',C',A') /\
            angle(C,A,B) = angle(C',A',B')`,


let CONGRUENT_TRIANGLES_SAS_FULL = 
prove
 (`!A B C:real^M A' B' C':real^N.
        dist(A,B) = dist(A',B') /\
        angle(A,B,C) = angle(A',B',C') /\
        dist(B,C) = dist(B',C')
        ==> dist(A,B) = dist(A',B') /\
            dist(B,C) = dist(B',C') /\
            dist(C,A) = dist(C',A') /\
            angle(A,B,C) = angle(A',B',C') /\
            angle(B,C,A) = angle(B',C',A') /\
            angle(C,A,B) = angle(C',A',B')`,


let CONGRUENT_TRIANGLES_AAS_FULL = 
prove
 (`!A B C:real^M A' B' C':real^N.
        angle(A,B,C) = angle(A',B',C') /\
        angle(B,C,A) = angle(B',C',A') /\
        dist(A,B) = dist(A',B') /\
        ~(collinear {A,B,C})
        ==> dist(A,B) = dist(A',B') /\
            dist(B,C) = dist(B',C') /\
            dist(C,A) = dist(C',A') /\
            angle(A,B,C) = angle(A',B',C') /\
            angle(B,C,A) = angle(B',C',A') /\
            angle(C,A,B) = angle(C',A',B')`,


let CONGRUENT_TRIANGLES_ASA_FULL = 
prove
 (`!A B C:real^M A' B' C':real^N.
        angle(A,B,C) = angle(A',B',C') /\
        dist(A,B) = dist(A',B') /\
        angle(B,A,C) = angle(B',A',C') /\
        ~(collinear {A,B,C})
        ==> dist(A,B) = dist(A',B') /\
            dist(B,C) = dist(B',C') /\
            dist(C,A) = dist(C',A') /\
            angle(A,B,C) = angle(A',B',C') /\
            angle(B,C,A) = angle(B',C',A') /\
            angle(C,A,B) = angle(C',A',B')`,

(* ------------------------------------------------------------------------- *)
(* Between-ness.                                                             *)
(* ------------------------------------------------------------------------- *)


let ANGLE_BETWEEN = 
prove
 (`!a b x. angle(a,x,b) = pi <=> ~(x = a) /\ ~(x = b) /\ between x (a,b)`,

  REPEAT GEN_TAC THEN REWRITE_TAC[between; ANGLE_EQ_PI_DIST] THEN
  REWRITE_TAC[EQ_SYM_EQ]);;


let BETWEEN_ANGLE = 
prove
 (`!a b x. between x (a,b) <=> x = a \/ x = b \/ angle(a,x,b) = pi`,

  REPEAT GEN_TAC THEN REWRITE_TAC[ANGLE_BETWEEN] THEN
  MESON_TAC[BETWEEN_REFL]);;


let ANGLES_ALONG_LINE = 
prove
 (`!A B C D:real^N.
      ~(C = A) /\ ~(C = B) /\ between C (A,B)
      ==> angle(A,C,D) + angle(B,C,D) = pi`,

  REPEAT GEN_TAC THEN REWRITE_TAC[GSYM ANGLE_BETWEEN] THEN
  DISCH_THEN(SUBST1_TAC o MATCH_MP ANGLE_EQ_PI_LEFT) THEN REAL_ARITH_TAC);;


let ANGLES_ADD_BETWEEN = 
prove
 (`!A B C D:real^N.
        between C (A,B) /\ ~(D = A) /\ ~(D = B)
        ==> angle(A,D,C) + angle(C,D,B) = angle(A,D,B)`,

  REPEAT GEN_TAC THEN ASM_CASES_TAC `A:real^N = B` THENL
   [ASM_SIMP_TAC[BETWEEN_REFL_EQ] THEN
    DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
    ASM_SIMP_TAC[ANGLE_REFL_MID; REAL_ADD_LID];
    ALL_TAC] THEN
  ASM_CASES_TAC `C:real^N = A` THEN
  ASM_SIMP_TAC[ANGLE_REFL_MID; REAL_ADD_LID] THEN
  ASM_CASES_TAC `C:real^N = B` THEN
  ASM_SIMP_TAC[ANGLE_REFL_MID; REAL_ADD_RID] THEN
  STRIP_TAC THEN
  MP_TAC(ISPECL [`A:real^N`; `B:real^N`; `C:real^N`; `D:real^N`]
        ANGLES_ALONG_LINE) THEN
  MP_TAC(ISPECL [`A:real^N`; `B:real^N`; `D:real^N`] TRIANGLE_ANGLE_SUM) THEN
  MP_TAC(ISPECL [`A:real^N`; `C:real^N`; `D:real^N`] TRIANGLE_ANGLE_SUM) THEN
  MP_TAC(ISPECL [`B:real^N`; `C:real^N`; `D:real^N`] TRIANGLE_ANGLE_SUM) THEN
  ASM_REWRITE_TAC[] THEN
  SUBGOAL_THEN `angle(C:real^N,A,D) = angle(B,A,D) /\
                angle(A,B,D) = angle(C,B,D)`
   (CONJUNCTS_THEN SUBST1_TAC)
  THENL [ALL_TAC; REWRITE_TAC[ANGLE_SYM] THEN REAL_ARITH_TAC] THEN
  CONJ_TAC THEN MATCH_MP_TAC ANGLE_EQ_0_RIGHT THEN
  ASM_MESON_TAC[ANGLE_EQ_PI_OTHERS; BETWEEN_ANGLE]);;