1 (* ========================================================================= *)
2 (* Feuerbach's theorem. *)
3 (* ========================================================================= *)
5 needs "Multivariate/convex.ml";;
7 (* ------------------------------------------------------------------------- *)
8 (* Algebraic condition for two circles to be tangent to each other. *)
9 (* ------------------------------------------------------------------------- *)
11 let CIRCLES_TANGENT = prove
13 &0 <= r1 /\ &0 <= r2 /\
14 (dist(c1,c2) = r1 + r2 \/ dist(c1,c2) = abs(r1 - r2))
15 ==> c1 = c2 /\ r1 = r2 \/
16 ?!x:real^2. dist(c1,x) = r1 /\ dist(c2,x) = r2`,
17 MATCH_MP_TAC REAL_WLOG_LE THEN CONJ_TAC THENL
18 [REPEAT GEN_TAC THEN MATCH_MP_TAC(MESON[]
19 `(!x y. P x y <=> Q y x) ==> ((!x y. P x y) <=> (!x y. Q x y))`) THEN
20 MESON_TAC[DIST_SYM; REAL_ADD_SYM; REAL_ABS_SUB]; ALL_TAC] THEN
21 REPEAT GEN_TAC THEN DISCH_TAC THEN REPEAT GEN_TAC THEN
22 ASM_CASES_TAC `r1 = &0` THENL
23 [ASM_REWRITE_TAC[DIST_EQ_0; MESON[] `(?!x. a = x /\ P x) <=> P a`] THEN
24 REWRITE_TAC[DIST_SYM] THEN REAL_ARITH_TAC;
26 ASM_CASES_TAC `r2 = &0` THENL [ASM_REAL_ARITH_TAC; ALL_TAC] THEN
27 ASM_SIMP_TAC[REAL_ARITH `r1 <= r2 ==> abs(r1 - r2) = r2 - r1`] THEN
28 ASM_REWRITE_TAC[REAL_LE_LT] THEN STRIP_TAC THENL
29 [DISJ2_TAC THEN REWRITE_TAC[EXISTS_UNIQUE] THEN
30 EXISTS_TAC `c1 + r1 / (r1 + r2) % (c2 - c1):real^2` THEN CONJ_TAC THENL
32 VECTOR_ARITH `c1 - (c1 + a % (x - y)):real^2 = a % (y - x)`;
33 VECTOR_ARITH `z - (x + a % (z - x)):real^N = (a - &1) % (x - z)`] THEN
34 ASM_REWRITE_TAC[NORM_MUL; GSYM dist] THEN
35 ASM_SIMP_TAC[REAL_ABS_DIV; REAL_ABS_NEG;
36 REAL_FIELD `&0 < r1 /\ &0 < r2
37 ==> r1 / (r1 + r2) - &1 = --r2 / (r1 + r2)`] THEN
38 ASM_SIMP_TAC[real_abs; REAL_LT_IMP_LE; REAL_LT_ADD] THEN
39 REPEAT(POP_ASSUM MP_TAC) THEN CONV_TAC REAL_FIELD;
40 X_GEN_TAC `y:real^2` THEN STRIP_TAC THEN
41 SUBGOAL_THEN `(y:real^2) IN segment[c1,c2]` MP_TAC THENL
42 [ASM_REWRITE_TAC[GSYM BETWEEN_IN_SEGMENT; between] THEN
43 ASM_MESON_TAC[DIST_SYM];
44 REWRITE_TAC[IN_SEGMENT]] THEN
45 DISCH_THEN(X_CHOOSE_THEN `u:real` MP_TAC) THEN
46 REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
47 DISCH_THEN SUBST_ALL_TAC THEN
48 UNDISCH_TAC `dist(c1:real^2,(&1 - u) % c1 + u % c2) = r1` THEN
49 REWRITE_TAC[VECTOR_ARITH
50 `(&1 - u) % c1 + u % c2:real^N = c1 + u % (c2 - c1)`] THEN
51 REWRITE_TAC[NORM_ARITH `dist(x:real^2,x + y) = norm y`] THEN
52 ONCE_REWRITE_TAC[GSYM NORM_NEG] THEN
53 REWRITE_TAC[VECTOR_ARITH `--(a % (x - y)):real^N = a % (y - x)`] THEN
54 ASM_REWRITE_TAC[NORM_MUL; GSYM dist; real_abs] THEN
55 DISCH_TAC THEN AP_TERM_TAC THEN AP_THM_TAC THEN AP_TERM_TAC THEN
56 REPEAT(POP_ASSUM MP_TAC) THEN CONV_TAC REAL_FIELD];
57 ASM_CASES_TAC `r1:real = r2` THENL
58 [ASM_MESON_TAC[REAL_SUB_REFL; DIST_EQ_0]; DISJ2_TAC] THEN
59 SUBGOAL_THEN `r1 < r2` ASSUME_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC] THEN
60 REWRITE_TAC[EXISTS_UNIQUE] THEN
61 EXISTS_TAC `c2 + r2 / (r2 - r1) % (c1 - c2):real^2` THEN CONJ_TAC THENL
63 VECTOR_ARITH `c1 - (c1 + a % (x - y)):real^2 = --(a % (x - y)) /\
64 c1 - (c2 + a % (c1 - c2)):real^2 = (&1 - a) % (c1 - c2)`] THEN
65 ASM_REWRITE_TAC[NORM_MUL; NORM_NEG; GSYM dist] THEN
66 ASM_SIMP_TAC[REAL_ABS_DIV; REAL_ABS_NEG;
67 REAL_FIELD `r1 < r2 ==> &1 - r2 / (r2 - r1) = --(r1 / (r2 - r1))`] THEN
68 ASM_SIMP_TAC[real_abs; REAL_SUB_LE; REAL_LT_IMP_LE] THEN
69 REPEAT(POP_ASSUM MP_TAC) THEN CONV_TAC REAL_FIELD;
70 X_GEN_TAC `y:real^2` THEN STRIP_TAC THEN
71 SUBGOAL_THEN `(c1:real^2) IN segment[c2,y]` MP_TAC THENL
72 [ASM_REWRITE_TAC[GSYM BETWEEN_IN_SEGMENT; between] THEN
73 ONCE_REWRITE_TAC[DIST_SYM] THEN ASM_REAL_ARITH_TAC;
74 REWRITE_TAC[IN_SEGMENT]] THEN
75 DISCH_THEN(X_CHOOSE_THEN `u:real` MP_TAC) THEN
76 REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
77 ASM_CASES_TAC `u = &0` THENL
78 [ASM_REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_RID; REAL_SUB_RZERO] THEN
79 REWRITE_TAC[VECTOR_MUL_LID] THEN ASM_MESON_TAC[DIST_EQ_0; REAL_SUB_0];
81 DISCH_THEN SUBST_ALL_TAC THEN
82 UNDISCH_TAC `dist((&1 - u) % c2 + u % y:real^2,c2) = r2 - r1` THEN
83 REWRITE_TAC[VECTOR_ARITH
84 `(&1 - u) % c1 + u % c2:real^N = c1 + u % (c2 - c1)`] THEN
85 REWRITE_TAC[NORM_ARITH `dist(x + y:real^2,x) = norm y`] THEN
86 ONCE_REWRITE_TAC[GSYM NORM_NEG] THEN
87 REWRITE_TAC[VECTOR_ARITH `--(a % (x - y)):real^N = a % (y - x)`] THEN
88 ASM_REWRITE_TAC[NORM_MUL; GSYM dist; real_abs] THEN
89 REWRITE_TAC[VECTOR_ARITH
90 `c + v % ((c + u % (y - c)) - c):real^2 = c + v % u % (y - c)`] THEN
91 DISCH_THEN(SUBST1_TAC o SYM) THEN
92 REWRITE_TAC[VECTOR_MUL_EQ_0; VECTOR_ARITH
93 `y:real^2 = c + u % v % (y - c) <=>
94 (&1 - u * v) % (y - c) = vec 0`] THEN
96 REPEAT(POP_ASSUM MP_TAC) THEN CONV_TAC REAL_FIELD]]);;
98 (* ------------------------------------------------------------------------- *)
99 (* Feuerbach's theorem *)
101 (* Given a non-degenerate triangle abc, let the circle passing through *)
102 (* the midpoints of its sides (the "9 point circle") have center "ncenter" *)
103 (* and radius "nradius". Now suppose the circle with center "icenter" and *)
104 (* radius "iradius" is tangent to three sides (either internally or *)
105 (* externally to one side and two produced sides), meaning that it's either *)
106 (* the inscribed circle or one of the three escribed circles. Then the two *)
107 (* circles are tangent to each other, i.e. either they are identical or they *)
108 (* touch at exactly one point. *)
109 (* ------------------------------------------------------------------------- *)
111 let FEUERBACH = prove
112 (`!a b c mbc mac mab pbc pac pab ncenter icenter nradius iradius.
113 ~(collinear {a,b,c}) /\
114 midpoint(a,b) = mab /\
115 midpoint(b,c) = mbc /\
116 midpoint(c,a) = mac /\
117 dist(ncenter,mbc) = nradius /\
118 dist(ncenter,mac) = nradius /\
119 dist(ncenter,mab) = nradius /\
120 dist(icenter,pbc) = iradius /\
121 dist(icenter,pac) = iradius /\
122 dist(icenter,pab) = iradius /\
123 collinear {a,b,pab} /\ orthogonal (a - b) (icenter - pab) /\
124 collinear {b,c,pbc} /\ orthogonal (b - c) (icenter - pbc) /\
125 collinear {a,c,pac} /\ orthogonal (a - c) (icenter - pac)
126 ==> ncenter = icenter /\ nradius = iradius \/
127 ?!x:real^2. dist(ncenter,x) = nradius /\ dist(icenter,x) = iradius`,
128 REPEAT GEN_TAC THEN DISCH_TAC THEN MATCH_MP_TAC CIRCLES_TANGENT THEN
129 POP_ASSUM MP_TAC THEN MAP_EVERY (fun t ->
130 ASM_CASES_TAC t THENL [ALL_TAC; ASM_MESON_TAC[DIST_POS_LE]])
131 [`&0 <= nradius`; `&0 <= iradius`] THEN
132 ASM_REWRITE_TAC[dist; NORM_EQ_SQUARE] THEN
133 ASM_SIMP_TAC[REAL_LE_ADD; REAL_ABS_POS; GSYM NORM_POW_2; GSYM dist] THEN
134 REWRITE_TAC[REAL_POW2_ABS] THEN POP_ASSUM_LIST(K ALL_TAC) THEN
135 ONCE_REWRITE_TAC[TAUT `a /\ b /\ c /\ d /\ e <=> b /\ c /\ d /\ a /\ e`] THEN
136 GEOM_ORIGIN_TAC `a:real^2` THEN
137 GEOM_NORMALIZE_TAC `b:real^2` THEN CONJ_TAC THENL
138 [REWRITE_TAC[INSERT_AC; COLLINEAR_2]; ALL_TAC] THEN
139 GEOM_BASIS_MULTIPLE_TAC 1 `b:real^2` THEN
140 SIMP_TAC[NORM_MUL; NORM_BASIS; DIMINDEX_2; ARITH; real_abs] THEN
141 GEN_TAC THEN DISCH_THEN(K ALL_TAC) THEN REWRITE_TAC[REAL_MUL_RID] THEN
142 DISCH_THEN SUBST1_TAC THEN REWRITE_TAC[VECTOR_MUL_LID] THEN
144 REPLICATE_TAC 3 (DISCH_THEN(CONJUNCTS_THEN2 (ASSUME_TAC o SYM) MP_TAC)) THEN
145 REWRITE_TAC[COLLINEAR_3_2D] THEN
146 REWRITE_TAC[orthogonal; dist; NORM_POW_2] THEN
147 ASM_REWRITE_TAC[midpoint] THEN
148 REWRITE_TAC[DOT_2; DOT_LSUB; DOT_RSUB] THEN
149 SIMP_TAC[VECTOR_ADD_COMPONENT; VECTOR_SUB_COMPONENT; VEC_COMPONENT;
150 VECTOR_MUL_COMPONENT; BASIS_COMPONENT; DIMINDEX_2; ARITH] THEN
151 CONV_TAC REAL_RING);;
153 (* ------------------------------------------------------------------------- *)
154 (* As a little bonus, verify that the circle passing through the *)
155 (* midpoints of the sides is indeed a 9-point circle, i.e. it passes *)
156 (* through the feet of the altitudes and the midpoints of the lines joining *)
157 (* the vertices to the orthocenter (where the alititudes intersect). *)
158 (* ------------------------------------------------------------------------- *)
160 let NINE_POINT_CIRCLE_1 = prove
161 (`!a b c:real^2 mbc mac mab fbc fac fab ncenter nradius.
162 ~(collinear {a,b,c}) /\
163 midpoint(a,b) = mab /\
164 midpoint(b,c) = mbc /\
165 midpoint(c,a) = mac /\
166 dist(ncenter,mbc) = nradius /\
167 dist(ncenter,mac) = nradius /\
168 dist(ncenter,mab) = nradius /\
169 collinear {a,b,fab} /\ orthogonal (a - b) (c - fab) /\
170 collinear {b,c,fbc} /\ orthogonal (b - c) (a - fbc) /\
171 collinear {c,a,fac} /\ orthogonal (c - a) (b - fac)
172 ==> dist(ncenter,fab) = nradius /\
173 dist(ncenter,fbc) = nradius /\
174 dist(ncenter,fac) = nradius`,
176 ONCE_REWRITE_TAC[TAUT `a /\ b /\ c /\ d /\ e <=> b /\ c /\ d /\ a /\ e`] THEN
177 REPLICATE_TAC 3 (DISCH_THEN(CONJUNCTS_THEN2 (ASSUME_TAC o SYM) MP_TAC)) THEN
178 ASM_REWRITE_TAC[dist; NORM_EQ_SQUARE; REAL_POS] THEN
179 REWRITE_TAC[COLLINEAR_3_2D] THEN
180 REWRITE_TAC[orthogonal; dist; NORM_POW_2] THEN
181 ASM_REWRITE_TAC[midpoint] THEN
182 REWRITE_TAC[DOT_2; DOT_LSUB; DOT_RSUB] THEN
183 REWRITE_TAC[VECTOR_ADD_COMPONENT; VECTOR_SUB_COMPONENT;
184 VECTOR_MUL_COMPONENT; VEC_COMPONENT] THEN
185 SIMP_TAC[] THEN CONV_TAC REAL_RING);;
187 let NINE_POINT_CIRCLE_2 = prove
188 (`!a b c:real^2 mbc mac mab fbc fac fab ncenter nradius.
189 ~(collinear {a,b,c}) /\
190 midpoint(a,b) = mab /\
191 midpoint(b,c) = mbc /\
192 midpoint(c,a) = mac /\
193 dist(ncenter,mbc) = nradius /\
194 dist(ncenter,mac) = nradius /\
195 dist(ncenter,mab) = nradius /\
196 collinear {a,b,fab} /\ orthogonal (a - b) (c - fab) /\
197 collinear {b,c,fbc} /\ orthogonal (b - c) (a - fbc) /\
198 collinear {c,a,fac} /\ orthogonal (c - a) (b - fac) /\
199 collinear {oc,a,fbc} /\ collinear {oc,b,fac} /\ collinear{oc,c,fab}
200 ==> dist(ncenter,midpoint(oc,a)) = nradius /\
201 dist(ncenter,midpoint(oc,b)) = nradius /\
202 dist(ncenter,midpoint(oc,c)) = nradius`,
204 ONCE_REWRITE_TAC[TAUT `a /\ b /\ c /\ d /\ e <=> b /\ c /\ d /\ a /\ e`] THEN
205 REPLICATE_TAC 3 (DISCH_THEN(CONJUNCTS_THEN2 (ASSUME_TAC o SYM) MP_TAC)) THEN
206 ASM_REWRITE_TAC[dist; NORM_EQ_SQUARE; REAL_POS] THEN
207 REWRITE_TAC[COLLINEAR_3_2D] THEN
208 REWRITE_TAC[orthogonal; dist; NORM_POW_2] THEN
209 ASM_REWRITE_TAC[midpoint] THEN
210 REWRITE_TAC[DOT_2; DOT_LSUB; DOT_RSUB] THEN
211 REWRITE_TAC[VECTOR_ADD_COMPONENT; VECTOR_SUB_COMPONENT;
212 VECTOR_MUL_COMPONENT; VEC_COMPONENT] THEN
213 SIMP_TAC[] THEN CONV_TAC REAL_RING);;