(* ========================================================================= *)
(* Isosceles triangle theorem.                                               *)
(* ========================================================================= *)

needs "Multivariate/geom.ml";;

(* ------------------------------------------------------------------------- *)
(* The theorem, according to Wikipedia.                                      *)
(* ------------------------------------------------------------------------- *)

let ISOSCELES_TRIANGLE_THEOREM = 
prove (`!A B C:real^N. dist(A,C) = dist(B,C) ==> angle(C,A,B) = angle(A,B,C)`,
MP_TAC(INST_TYPE [`:N`,`:M`] CONGRUENT_TRIANGLES_SSS) THEN MESON_TAC[DIST_SYM; ANGLE_SYM]);;
(* ------------------------------------------------------------------------- *) (* The obvious converse. *) (* ------------------------------------------------------------------------- *)
let ISOSCELES_TRIANGLE_CONVERSE = 
prove (`!A B C:real^N. angle(C,A,B) = angle(A,B,C) /\ ~(collinear {A,B,C}) ==> dist(A,C) = dist(B,C)`,
MP_TAC(INST_TYPE [`:N`,`:M`] CONGRUENT_TRIANGLES_ASA_FULL) THEN MESON_TAC[DIST_SYM; ANGLE_SYM]);;
(* ------------------------------------------------------------------------- *) (* Some other equivalents sometimes called the ITT (see the Web page *) (* http://www.sonoma.edu/users/w/wilsonst/Courses/Math_150/Theorems/itt.html *) (* ------------------------------------------------------------------------- *)
let lemma = 
prove (`!A B C D:real^N. between D (A,B) ==> (orthogonal (A - B) (C - D) <=> angle(A,D,C) = pi / &2 /\ angle(B,D,C) = pi / &2)`,
REPEAT GEN_TAC THEN ASM_CASES_TAC `D:real^N = A` THENL [DISCH_TAC THEN ASM_SIMP_TAC[ANGLE_REFL] THEN GEN_REWRITE_TAC LAND_CONV [GSYM ORTHOGONAL_LNEG] THEN REWRITE_TAC[VECTOR_NEG_SUB; ORTHOGONAL_VECTOR_ANGLE; angle]; ALL_TAC] THEN ASM_CASES_TAC `D:real^N = B` THENL [DISCH_TAC THEN ASM_SIMP_TAC[ANGLE_REFL] THEN REWRITE_TAC[ORTHOGONAL_VECTOR_ANGLE; angle]; ALL_TAC] THEN DISCH_TAC THEN MP_TAC(ISPECL [`A:real^N`; `B:real^N`; `D:real^N`; `C:real^N`] ANGLES_ALONG_LINE) THEN ASM_REWRITE_TAC[ORTHOGONAL_VECTOR_ANGLE] THEN MATCH_MP_TAC(REAL_ARITH `x = z ==> x + y = p ==> (z = p / &2 <=> x = p / &2 /\ y = p / &2)`) THEN REWRITE_TAC[angle] THEN MATCH_MP_TAC VECTOR_ANGLE_EQ_0_RIGHT THEN ONCE_REWRITE_TAC[GSYM VECTOR_ANGLE_NEG2] THEN REWRITE_TAC[VECTOR_NEG_SUB; GSYM angle] THEN ASM_MESON_TAC[ANGLE_EQ_PI_OTHERS; BETWEEN_ANGLE]);;
let ISOSCELES_TRIANGLE_1 = 
prove (`!A B C D:real^N. dist(A,C) = dist(B,C) /\ D = midpoint(A,B) ==> angle(A,C,D) = angle(B,C,D)`,
REPEAT STRIP_TAC THEN MP_TAC(ISPECL [`A:real^N`; `D:real^N`; `C:real^N`; `B:real^N`; `D:real^N`; `C:real^N`] CONGRUENT_TRIANGLES_SSS_FULL) THEN ASM_REWRITE_TAC[DIST_MIDPOINT] THEN ASM_MESON_TAC[DIST_SYM; ANGLE_SYM]);;
let ISOSCELES_TRIANGLE_2 = 
prove (`!A B C D:real^N. between D (A,B) /\ dist(A,C) = dist(B,C) /\ angle(A,C,D) = angle(B,C,D) ==> orthogonal (A - B) (C - D)`,
REPEAT STRIP_TAC THEN FIRST_ASSUM(ASSUME_TAC o MATCH_MP ISOSCELES_TRIANGLE_THEOREM) THEN MP_TAC(ISPECL [`D:real^N`; `C:real^N`; `A:real^N`; `D:real^N`; `C:real^N`; `B:real^N`] CONGRUENT_TRIANGLES_SAS_FULL) THEN ANTS_TAC THENL [ASM_MESON_TAC[DIST_SYM; ANGLE_SYM]; ALL_TAC] THEN ASM_CASES_TAC `D:real^N = B` THEN ASM_SIMP_TAC[DIST_EQ_0; DIST_REFL; VECTOR_SUB_REFL; ORTHOGONAL_0] THEN ASM_CASES_TAC `D:real^N = A` THENL [ASM_MESON_TAC[DIST_EQ_0]; ALL_TAC] THEN ASM_SIMP_TAC[lemma] THEN MP_TAC(ISPECL [`A:real^N`; `B:real^N`; `D:real^N`; `C:real^N`] ANGLES_ALONG_LINE) THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);;
let ISOSCELES_TRIANGLE_3 = 
prove (`!A B C D:real^N. between D (A,B) /\ dist(A,C) = dist(B,C) /\ orthogonal (A - B) (C - D) ==> D = midpoint(A,B)`,
REPEAT GEN_TAC THEN ASM_CASES_TAC `A:real^N = B` THEN ASM_SIMP_TAC[BETWEEN_REFL_EQ; MIDPOINT_REFL] THEN ASM_CASES_TAC `D:real^N = A` THENL [ASM_REWRITE_TAC[] THEN STRIP_TAC THEN MP_TAC(ISPECL [`B:real^N`; `A:real^N`; `C:real^N`] PYTHAGORAS) THEN ANTS_TAC THENL [ASM_MESON_TAC[ORTHOGONAL_LNEG; VECTOR_NEG_SUB]; ALL_TAC] THEN ONCE_REWRITE_TAC[NORM_SUB] THEN ASM_REWRITE_TAC[GSYM dist] THEN ASM_REWRITE_TAC[REAL_RING `a = x pow 2 + a <=> x = &0`; DIST_EQ_0]; ALL_TAC] THEN ASM_CASES_TAC `D:real^N = B` THENL [ASM_REWRITE_TAC[] THEN STRIP_TAC THEN MP_TAC(ISPECL [`A:real^N`; `B:real^N`; `C:real^N`] PYTHAGORAS) THEN ANTS_TAC THENL [ASM_MESON_TAC[ORTHOGONAL_LNEG; VECTOR_NEG_SUB]; ALL_TAC] THEN ONCE_REWRITE_TAC[NORM_SUB] THEN ASM_REWRITE_TAC[GSYM dist] THEN ASM_REWRITE_TAC[REAL_RING `a = x pow 2 + a <=> x = &0`; DIST_EQ_0]; ALL_TAC] THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN ASM_SIMP_TAC[lemma; MIDPOINT_COLLINEAR; BETWEEN_IMP_COLLINEAR] THEN STRIP_TAC THEN FIRST_ASSUM(ASSUME_TAC o MATCH_MP ISOSCELES_TRIANGLE_THEOREM) THEN MP_TAC(ISPECL [`A:real^N`; `C:real^N`; `D:real^N`; `B:real^N`; `C:real^N`; `D:real^N`] CONGRUENT_TRIANGLES_SAS) THEN ANTS_TAC THENL [ALL_TAC; MESON_TAC[DIST_SYM]] THEN ASM_REWRITE_TAC[] THEN MP_TAC(ISPECL [`A:real^N`; `C:real^N`; `D:real^N`] TRIANGLE_ANGLE_SUM) THEN ANTS_TAC THENL [ASM_MESON_TAC[DIST_EQ_0]; ALL_TAC] THEN MP_TAC(ISPECL [`B:real^N`; `C:real^N`; `D:real^N`] TRIANGLE_ANGLE_SUM) THEN ANTS_TAC THENL [ASM_MESON_TAC[DIST_EQ_0]; ALL_TAC] THEN MATCH_MP_TAC(REAL_ARITH `a:real = a' /\ b = b' ==> a + x + b = p ==> a' + x' + b' = p ==> x' = x`) THEN CONJ_TAC THENL [ALL_TAC; ASM_MESON_TAC[ANGLE_SYM]] THEN CONV_TAC SYM_CONV THEN UNDISCH_TAC `angle(C:real^N,A,B) = angle (A,B,C)` THEN MATCH_MP_TAC EQ_IMP THEN BINOP_TAC THENL [MATCH_MP_TAC ANGLE_EQ_0_LEFT; GEN_REWRITE_TAC RAND_CONV [ANGLE_SYM] THEN MATCH_MP_TAC ANGLE_EQ_0_RIGHT] THEN ASM_MESON_TAC[ANGLE_EQ_PI_OTHERS; BETWEEN_ANGLE]);;
(* ------------------------------------------------------------------------- *) (* Now the converses to those as well. *) (* ------------------------------------------------------------------------- *)
let ISOSCELES_TRIANGLE_4 = 
prove (`!A B C D:real^N. D = midpoint(A,B) /\ orthogonal (A - B) (C - D) ==> dist(A,C) = dist(B,C)`,
REPEAT GEN_TAC THEN ASM_SIMP_TAC[IMP_CONJ; BETWEEN_MIDPOINT; lemma] THEN DISCH_THEN(ASSUME_TAC o SYM) THEN ASM_REWRITE_TAC[] THEN REPEAT DISCH_TAC THEN MATCH_MP_TAC CONGRUENT_TRIANGLES_SAS THEN MAP_EVERY EXISTS_TAC [`D:real^N`; `D:real^N`] THEN ASM_REWRITE_TAC[] THEN EXPAND_TAC "D" THEN REWRITE_TAC[DIST_MIDPOINT]);;
let ISOSCELES_TRIANGLE_5 = 
prove (`!A B C D:real^N. ~collinear{D,C,A} /\ between D (A,B) /\ angle(A,C,D) = angle(B,C,D) /\ orthogonal (A - B) (C - D) ==> dist(A,C) = dist(B,C)`,
REPEAT GEN_TAC THEN ASM_CASES_TAC `C:real^N = D` THENL [ASM_REWRITE_TAC[INSERT_AC; COLLINEAR_2]; ALL_TAC] THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN UNDISCH_TAC `~(C:real^N = D)` THEN REWRITE_TAC[GSYM IMP_CONJ_ALT; GSYM CONJ_ASSOC] THEN ASM_CASES_TAC `A:real^N = B` THEN ASM_REWRITE_TAC[] THEN ASM_CASES_TAC `C:real^N = A` THENL [DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN ASM_REWRITE_TAC[ANGLE_REFL] THEN FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [BETWEEN_ANGLE]) THEN ASM_CASES_TAC `D:real^N = A` THEN ASM_REWRITE_TAC[] THEN ASM_CASES_TAC `D:real^N = B` THEN ASM_REWRITE_TAC[] THEN ASM_SIMP_TAC[ANGLE_REFL_MID; REAL_ARITH `x / &2 = &0 <=> x = &0`; PI_NZ] THEN DISCH_THEN(MP_TAC o MATCH_MP ANGLE_EQ_PI_OTHERS) THEN MP_TAC PI_NZ THEN REAL_ARITH_TAC; ALL_TAC] THEN ASM_CASES_TAC `C:real^N = B` THENL [DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN ASM_REWRITE_TAC[ANGLE_REFL] THEN FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [BETWEEN_ANGLE]) THEN ASM_CASES_TAC `D:real^N = B` THEN ASM_REWRITE_TAC[] THEN ASM_CASES_TAC `D:real^N = A` THEN ASM_REWRITE_TAC[] THEN ASM_SIMP_TAC[ANGLE_REFL_MID; REAL_ARITH `&0 = x / &2 <=> x = &0`; PI_NZ] THEN DISCH_THEN(MP_TAC o MATCH_MP ANGLE_EQ_PI_OTHERS) THEN MP_TAC PI_NZ THEN REAL_ARITH_TAC; ALL_TAC] THEN ASM_SIMP_TAC[IMP_CONJ; lemma] THEN REPEAT DISCH_TAC THEN MP_TAC( ISPECL [`D:real^N`; `C:real^N`; `A:real^N`; `D:real^N`; `C:real^N`; `B:real^N`] CONGRUENT_TRIANGLES_ASA_FULL) THEN ANTS_TAC THENL [ALL_TAC; MESON_TAC[DIST_SYM]] THEN ONCE_REWRITE_TAC[ANGLE_SYM] THEN ASM_REWRITE_TAC[]);;
let ISOSCELES_TRIANGLE_6 = 
prove (`!A B C D:real^N. ~collinear{D,C,A} /\ D = midpoint(A,B) /\ angle(A,C,D) = angle(B,C,D) ==> dist(A,C) = dist(B,C)`,
REPEAT GEN_TAC THEN DISCH_THEN(STRIP_ASSUME_TAC o GSYM) THEN ASM_CASES_TAC `A:real^N = B` THEN ASM_REWRITE_TAC[] THEN MP_TAC(ISPECL [`A:real^N`; `C:real^N`; `D:real^N`] LAW_OF_SINES) THEN MP_TAC(ISPECL [`B:real^N`; `C:real^N`; `D:real^N`] LAW_OF_SINES) THEN ASM_REWRITE_TAC[] THEN DISCH_THEN SUBST1_TAC THEN EXPAND_TAC "D" THEN REWRITE_TAC[DIST_MIDPOINT] THEN ASM_SIMP_TAC[REAL_EQ_MUL_RCANCEL; REAL_LT_IMP_NZ; REAL_HALF; DIST_POS_LT; SIN_ANGLE_EQ] THEN STRIP_TAC THENL [MP_TAC(ISPECL [`D:real^N`; `C:real^N`; `A:real^N`; `D:real^N`; `C:real^N`; `B:real^N`] CONGRUENT_TRIANGLES_AAS) THEN ANTS_TAC THENL [ALL_TAC; MESON_TAC[DIST_SYM]] THEN ASM_REWRITE_TAC[] THEN ONCE_REWRITE_TAC[ANGLE_SYM] THEN ASM_REWRITE_TAC[]; MP_TAC(ISPECL [`A:real^N`; `B:real^N`; `C:real^N`] TRIANGLE_ANGLE_SUM) THEN ASM_REWRITE_TAC[] THEN SUBGOAL_THEN `angle(A:real^N,B,C) = angle(C,B,D) /\ angle(B,A,C) = angle(C,A,D)` (CONJUNCTS_THEN SUBST1_TAC) THENL [CONJ_TAC THEN GEN_REWRITE_TAC LAND_CONV [ANGLE_SYM] THEN MATCH_MP_TAC ANGLE_EQ_0_LEFT THEN MP_TAC(ISPECL [`A:real^N`; `B:real^N`] BETWEEN_MIDPOINT) THEN ASM_REWRITE_TAC[BETWEEN_ANGLE] THEN EXPAND_TAC "D" THEN REWRITE_TAC[MIDPOINT_EQ_ENDPOINT] THEN ASM_REWRITE_TAC[] THEN MESON_TAC[ANGLE_EQ_PI_OTHERS]; ALL_TAC] THEN ASM_REWRITE_TAC[REAL_ARITH `a + pi - a + x = pi <=> x = &0`] THEN MAP_EVERY ASM_CASES_TAC [`B:real^N = C`; `A:real^N = C`] THEN ASM_REWRITE_TAC[ANGLE_REFL; REAL_ARITH `p / &2 = &0 <=> p = &0`] THEN ASM_REWRITE_TAC[PI_NZ] THEN DISCH_TAC THEN MP_TAC(ISPECL [`B:real^N`; `C:real^N`; `A:real^N`] COLLINEAR_ANGLE) THEN ASM_REWRITE_TAC[] THEN UNDISCH_TAC `~collinear{D:real^N,C,A}` THEN MATCH_MP_TAC(TAUT `(q ==> p) ==> ~p ==> q ==> r`) THEN ONCE_REWRITE_TAC[SET_RULE `{bd,c,a} = {c,a,bd}`] THEN ONCE_REWRITE_TAC[COLLINEAR_3] THEN REWRITE_TAC[COLLINEAR_LEMMA] THEN ASM_REWRITE_TAC[VECTOR_SUB_EQ] THEN EXPAND_TAC "D" THEN REWRITE_TAC[midpoint] THEN REWRITE_TAC[VECTOR_ARITH `inv(&2) % (A + B) - A = inv(&2) % (B - A)`] THEN MESON_TAC[VECTOR_MUL_ASSOC]]);;