1 (* ========================================================================= *)
2 (* Isosceles triangle theorem. *)
3 (* ========================================================================= *)
5 needs "Multivariate/geom.ml";;
7 (* ------------------------------------------------------------------------- *)
8 (* The theorem, according to Wikipedia. *)
9 (* ------------------------------------------------------------------------- *)
11 let ISOSCELES_TRIANGLE_THEOREM = prove
12 (`!A B C:real^N. dist(A,C) = dist(B,C) ==> angle(C,A,B) = angle(A,B,C)`,
13 MP_TAC(INST_TYPE [`:N`,`:M`] CONGRUENT_TRIANGLES_SSS) THEN
14 MESON_TAC[DIST_SYM; ANGLE_SYM]);;
16 (* ------------------------------------------------------------------------- *)
17 (* The obvious converse. *)
18 (* ------------------------------------------------------------------------- *)
20 let ISOSCELES_TRIANGLE_CONVERSE = prove
21 (`!A B C:real^N. angle(C,A,B) = angle(A,B,C) /\ ~(collinear {A,B,C})
22 ==> dist(A,C) = dist(B,C)`,
23 MP_TAC(INST_TYPE [`:N`,`:M`] CONGRUENT_TRIANGLES_ASA_FULL) THEN
24 MESON_TAC[DIST_SYM; ANGLE_SYM]);;
26 (* ------------------------------------------------------------------------- *)
27 (* Some other equivalents sometimes called the ITT (see the Web page *)
28 (* http://www.sonoma.edu/users/w/wilsonst/Courses/Math_150/Theorems/itt.html *)
29 (* ------------------------------------------------------------------------- *)
34 ==> (orthogonal (A - B) (C - D) <=>
35 angle(A,D,C) = pi / &2 /\ angle(B,D,C) = pi / &2)`,
37 ASM_CASES_TAC `D:real^N = A` THENL
38 [DISCH_TAC THEN ASM_SIMP_TAC[ANGLE_REFL] THEN
39 GEN_REWRITE_TAC LAND_CONV [GSYM ORTHOGONAL_LNEG] THEN
40 REWRITE_TAC[VECTOR_NEG_SUB; ORTHOGONAL_VECTOR_ANGLE; angle];
42 ASM_CASES_TAC `D:real^N = B` THENL
43 [DISCH_TAC THEN ASM_SIMP_TAC[ANGLE_REFL] THEN
44 REWRITE_TAC[ORTHOGONAL_VECTOR_ANGLE; angle];
47 MP_TAC(ISPECL [`A:real^N`; `B:real^N`; `D:real^N`; `C:real^N`]
48 ANGLES_ALONG_LINE) THEN
49 ASM_REWRITE_TAC[ORTHOGONAL_VECTOR_ANGLE] THEN
50 MATCH_MP_TAC(REAL_ARITH
51 `x = z ==> x + y = p ==> (z = p / &2 <=> x = p / &2 /\ y = p / &2)`) THEN
52 REWRITE_TAC[angle] THEN MATCH_MP_TAC VECTOR_ANGLE_EQ_0_RIGHT THEN
53 ONCE_REWRITE_TAC[GSYM VECTOR_ANGLE_NEG2] THEN
54 REWRITE_TAC[VECTOR_NEG_SUB; GSYM angle] THEN
55 ASM_MESON_TAC[ANGLE_EQ_PI_OTHERS; BETWEEN_ANGLE]);;
57 let ISOSCELES_TRIANGLE_1 = prove
59 dist(A,C) = dist(B,C) /\ D = midpoint(A,B)
60 ==> angle(A,C,D) = angle(B,C,D)`,
62 MP_TAC(ISPECL [`A:real^N`; `D:real^N`; `C:real^N`;
63 `B:real^N`; `D:real^N`; `C:real^N`]
64 CONGRUENT_TRIANGLES_SSS_FULL) THEN
65 ASM_REWRITE_TAC[DIST_MIDPOINT] THEN ASM_MESON_TAC[DIST_SYM; ANGLE_SYM]);;
67 let ISOSCELES_TRIANGLE_2 = prove
70 dist(A,C) = dist(B,C) /\ angle(A,C,D) = angle(B,C,D)
71 ==> orthogonal (A - B) (C - D)`,
73 FIRST_ASSUM(ASSUME_TAC o MATCH_MP ISOSCELES_TRIANGLE_THEOREM) THEN
74 MP_TAC(ISPECL [`D:real^N`; `C:real^N`; `A:real^N`;
75 `D:real^N`; `C:real^N`; `B:real^N`]
76 CONGRUENT_TRIANGLES_SAS_FULL) THEN
77 ANTS_TAC THENL [ASM_MESON_TAC[DIST_SYM; ANGLE_SYM]; ALL_TAC] THEN
78 ASM_CASES_TAC `D:real^N = B` THEN
79 ASM_SIMP_TAC[DIST_EQ_0; DIST_REFL; VECTOR_SUB_REFL; ORTHOGONAL_0] THEN
80 ASM_CASES_TAC `D:real^N = A` THENL [ASM_MESON_TAC[DIST_EQ_0]; ALL_TAC] THEN
81 ASM_SIMP_TAC[lemma] THEN
82 MP_TAC(ISPECL [`A:real^N`; `B:real^N`; `D:real^N`; `C:real^N`]
83 ANGLES_ALONG_LINE) THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);;
85 let ISOSCELES_TRIANGLE_3 = prove
88 dist(A,C) = dist(B,C) /\ orthogonal (A - B) (C - D)
89 ==> D = midpoint(A,B)`,
90 REPEAT GEN_TAC THEN ASM_CASES_TAC `A:real^N = B` THEN
91 ASM_SIMP_TAC[BETWEEN_REFL_EQ; MIDPOINT_REFL] THEN
92 ASM_CASES_TAC `D:real^N = A` THENL
93 [ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
94 MP_TAC(ISPECL [`B:real^N`; `A:real^N`; `C:real^N`] PYTHAGORAS) THEN
96 [ASM_MESON_TAC[ORTHOGONAL_LNEG; VECTOR_NEG_SUB]; ALL_TAC] THEN
97 ONCE_REWRITE_TAC[NORM_SUB] THEN ASM_REWRITE_TAC[GSYM dist] THEN
98 ASM_REWRITE_TAC[REAL_RING `a = x pow 2 + a <=> x = &0`; DIST_EQ_0];
100 ASM_CASES_TAC `D:real^N = B` THENL
101 [ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
102 MP_TAC(ISPECL [`A:real^N`; `B:real^N`; `C:real^N`] PYTHAGORAS) THEN
104 [ASM_MESON_TAC[ORTHOGONAL_LNEG; VECTOR_NEG_SUB]; ALL_TAC] THEN
105 ONCE_REWRITE_TAC[NORM_SUB] THEN ASM_REWRITE_TAC[GSYM dist] THEN
106 ASM_REWRITE_TAC[REAL_RING `a = x pow 2 + a <=> x = &0`; DIST_EQ_0];
108 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
109 ASM_SIMP_TAC[lemma; MIDPOINT_COLLINEAR; BETWEEN_IMP_COLLINEAR] THEN
111 FIRST_ASSUM(ASSUME_TAC o MATCH_MP ISOSCELES_TRIANGLE_THEOREM) THEN
113 [`A:real^N`; `C:real^N`; `D:real^N`;
114 `B:real^N`; `C:real^N`; `D:real^N`]
115 CONGRUENT_TRIANGLES_SAS) THEN
116 ANTS_TAC THENL [ALL_TAC; MESON_TAC[DIST_SYM]] THEN
117 ASM_REWRITE_TAC[] THEN
118 MP_TAC(ISPECL [`A:real^N`; `C:real^N`; `D:real^N`] TRIANGLE_ANGLE_SUM) THEN
119 ANTS_TAC THENL [ASM_MESON_TAC[DIST_EQ_0]; ALL_TAC] THEN
120 MP_TAC(ISPECL [`B:real^N`; `C:real^N`; `D:real^N`] TRIANGLE_ANGLE_SUM) THEN
121 ANTS_TAC THENL [ASM_MESON_TAC[DIST_EQ_0]; ALL_TAC] THEN
122 MATCH_MP_TAC(REAL_ARITH
123 `a:real = a' /\ b = b'
124 ==> a + x + b = p ==> a' + x' + b' = p ==> x' = x`) THEN
125 CONJ_TAC THENL [ALL_TAC; ASM_MESON_TAC[ANGLE_SYM]] THEN
126 CONV_TAC SYM_CONV THEN
127 UNDISCH_TAC `angle(C:real^N,A,B) = angle (A,B,C)` THEN
128 MATCH_MP_TAC EQ_IMP THEN BINOP_TAC THENL
129 [MATCH_MP_TAC ANGLE_EQ_0_LEFT;
130 GEN_REWRITE_TAC RAND_CONV [ANGLE_SYM] THEN
131 MATCH_MP_TAC ANGLE_EQ_0_RIGHT] THEN
132 ASM_MESON_TAC[ANGLE_EQ_PI_OTHERS; BETWEEN_ANGLE]);;
134 (* ------------------------------------------------------------------------- *)
135 (* Now the converses to those as well. *)
136 (* ------------------------------------------------------------------------- *)
138 let ISOSCELES_TRIANGLE_4 = prove
140 D = midpoint(A,B) /\ orthogonal (A - B) (C - D)
141 ==> dist(A,C) = dist(B,C)`,
142 REPEAT GEN_TAC THEN ASM_SIMP_TAC[IMP_CONJ; BETWEEN_MIDPOINT; lemma] THEN
143 DISCH_THEN(ASSUME_TAC o SYM) THEN ASM_REWRITE_TAC[] THEN
144 REPEAT DISCH_TAC THEN MATCH_MP_TAC CONGRUENT_TRIANGLES_SAS THEN
145 MAP_EVERY EXISTS_TAC [`D:real^N`; `D:real^N`] THEN
146 ASM_REWRITE_TAC[] THEN EXPAND_TAC "D" THEN REWRITE_TAC[DIST_MIDPOINT]);;
148 let ISOSCELES_TRIANGLE_5 = prove
150 ~collinear{D,C,A} /\ between D (A,B) /\
151 angle(A,C,D) = angle(B,C,D) /\ orthogonal (A - B) (C - D)
152 ==> dist(A,C) = dist(B,C)`,
154 ASM_CASES_TAC `C:real^N = D` THENL
155 [ASM_REWRITE_TAC[INSERT_AC; COLLINEAR_2]; ALL_TAC] THEN
156 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
157 UNDISCH_TAC `~(C:real^N = D)` THEN
158 REWRITE_TAC[GSYM IMP_CONJ_ALT; GSYM CONJ_ASSOC] THEN
159 ASM_CASES_TAC `A:real^N = B` THEN ASM_REWRITE_TAC[] THEN
160 ASM_CASES_TAC `C:real^N = A` THENL
161 [DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
162 ASM_REWRITE_TAC[ANGLE_REFL] THEN
163 FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [BETWEEN_ANGLE]) THEN
164 ASM_CASES_TAC `D:real^N = A` THEN ASM_REWRITE_TAC[] THEN
165 ASM_CASES_TAC `D:real^N = B` THEN ASM_REWRITE_TAC[] THEN
166 ASM_SIMP_TAC[ANGLE_REFL_MID; REAL_ARITH `x / &2 = &0 <=> x = &0`;
168 DISCH_THEN(MP_TAC o MATCH_MP ANGLE_EQ_PI_OTHERS) THEN
169 MP_TAC PI_NZ THEN REAL_ARITH_TAC;
171 ASM_CASES_TAC `C:real^N = B` THENL
172 [DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
173 ASM_REWRITE_TAC[ANGLE_REFL] THEN
174 FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [BETWEEN_ANGLE]) THEN
175 ASM_CASES_TAC `D:real^N = B` THEN ASM_REWRITE_TAC[] THEN
176 ASM_CASES_TAC `D:real^N = A` THEN ASM_REWRITE_TAC[] THEN
177 ASM_SIMP_TAC[ANGLE_REFL_MID; REAL_ARITH `&0 = x / &2 <=> x = &0`;
179 DISCH_THEN(MP_TAC o MATCH_MP ANGLE_EQ_PI_OTHERS) THEN
180 MP_TAC PI_NZ THEN REAL_ARITH_TAC;
182 ASM_SIMP_TAC[IMP_CONJ; lemma] THEN
183 REPEAT DISCH_TAC THEN MP_TAC(
184 ISPECL [`D:real^N`; `C:real^N`; `A:real^N`;
185 `D:real^N`; `C:real^N`; `B:real^N`]
186 CONGRUENT_TRIANGLES_ASA_FULL) THEN
187 ANTS_TAC THENL [ALL_TAC; MESON_TAC[DIST_SYM]] THEN
188 ONCE_REWRITE_TAC[ANGLE_SYM] THEN ASM_REWRITE_TAC[]);;
190 let ISOSCELES_TRIANGLE_6 = prove
192 ~collinear{D,C,A} /\ D = midpoint(A,B) /\ angle(A,C,D) = angle(B,C,D)
193 ==> dist(A,C) = dist(B,C)`,
194 REPEAT GEN_TAC THEN DISCH_THEN(STRIP_ASSUME_TAC o GSYM) THEN
195 ASM_CASES_TAC `A:real^N = B` THEN ASM_REWRITE_TAC[] THEN
196 MP_TAC(ISPECL [`A:real^N`; `C:real^N`; `D:real^N`] LAW_OF_SINES) THEN
197 MP_TAC(ISPECL [`B:real^N`; `C:real^N`; `D:real^N`] LAW_OF_SINES) THEN
198 ASM_REWRITE_TAC[] THEN DISCH_THEN SUBST1_TAC THEN
199 EXPAND_TAC "D" THEN REWRITE_TAC[DIST_MIDPOINT] THEN
200 ASM_SIMP_TAC[REAL_EQ_MUL_RCANCEL; REAL_LT_IMP_NZ; REAL_HALF; DIST_POS_LT;
203 [MP_TAC(ISPECL [`D:real^N`; `C:real^N`; `A:real^N`;
204 `D:real^N`; `C:real^N`; `B:real^N`]
205 CONGRUENT_TRIANGLES_AAS) THEN
206 ANTS_TAC THENL [ALL_TAC; MESON_TAC[DIST_SYM]] THEN
207 ASM_REWRITE_TAC[] THEN ONCE_REWRITE_TAC[ANGLE_SYM] THEN
209 MP_TAC(ISPECL [`A:real^N`; `B:real^N`; `C:real^N`]
210 TRIANGLE_ANGLE_SUM) THEN
211 ASM_REWRITE_TAC[] THEN
212 SUBGOAL_THEN `angle(A:real^N,B,C) = angle(C,B,D) /\
213 angle(B,A,C) = angle(C,A,D)`
214 (CONJUNCTS_THEN SUBST1_TAC)
216 [CONJ_TAC THEN GEN_REWRITE_TAC LAND_CONV [ANGLE_SYM] THEN
217 MATCH_MP_TAC ANGLE_EQ_0_LEFT THEN
218 MP_TAC(ISPECL [`A:real^N`; `B:real^N`] BETWEEN_MIDPOINT) THEN
219 ASM_REWRITE_TAC[BETWEEN_ANGLE] THEN EXPAND_TAC "D" THEN
220 REWRITE_TAC[MIDPOINT_EQ_ENDPOINT] THEN ASM_REWRITE_TAC[] THEN
221 MESON_TAC[ANGLE_EQ_PI_OTHERS];
223 ASM_REWRITE_TAC[REAL_ARITH `a + pi - a + x = pi <=> x = &0`] THEN
224 MAP_EVERY ASM_CASES_TAC
225 [`B:real^N = C`; `A:real^N = C`] THEN
226 ASM_REWRITE_TAC[ANGLE_REFL; REAL_ARITH `p / &2 = &0 <=> p = &0`] THEN
227 ASM_REWRITE_TAC[PI_NZ] THEN DISCH_TAC THEN
228 MP_TAC(ISPECL [`B:real^N`; `C:real^N`; `A:real^N`] COLLINEAR_ANGLE) THEN
229 ASM_REWRITE_TAC[] THEN
230 UNDISCH_TAC `~collinear{D:real^N,C,A}` THEN
231 MATCH_MP_TAC(TAUT `(q ==> p) ==> ~p ==> q ==> r`) THEN
232 ONCE_REWRITE_TAC[SET_RULE `{bd,c,a} = {c,a,bd}`] THEN
233 ONCE_REWRITE_TAC[COLLINEAR_3] THEN
234 REWRITE_TAC[COLLINEAR_LEMMA] THEN ASM_REWRITE_TAC[VECTOR_SUB_EQ] THEN
235 EXPAND_TAC "D" THEN REWRITE_TAC[midpoint] THEN
236 REWRITE_TAC[VECTOR_ARITH `inv(&2) % (A + B) - A = inv(&2) % (B - A)`] THEN
237 MESON_TAC[VECTOR_MUL_ASSOC]]);;