(* ========================================================================= *)
(* Some geometric notions in real^N. *)
(* ========================================================================= *)
needs "Multivariate/realanalysis.ml";;
prioritize_vector();;
(* ------------------------------------------------------------------------- *)
(* Pythagoras's theorem is almost immediate. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Angle between vectors (always 0 <= angle <= pi). *)
(* ------------------------------------------------------------------------- *)
add_linear_invariants [VECTOR_ANGLE_LINEAR_IMAGE_EQ];;
(* ------------------------------------------------------------------------- *)
(* Basic properties of vector angles. *)
(* ------------------------------------------------------------------------- *)
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]]);;
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'))`,
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')`,
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 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 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')`,
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]);;
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')`,