Update from HH
[hl193./.git] / 100 / feuerbach.ml
1 (* ========================================================================= *)
2 (* Feuerbach's theorem.                                                      *)
3 (* ========================================================================= *)
4
5 needs "Multivariate/convex.ml";;
6
7 (* ------------------------------------------------------------------------- *)
8 (* Algebraic condition for two circles to be tangent to each other.          *)
9 (* ------------------------------------------------------------------------- *)
10
11 let CIRCLES_TANGENT = prove
12  (`!r1 r2 c1 c2.
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;
25     ALL_TAC] THEN
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
31      [REWRITE_TAC[dist;
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
62      [REWRITE_TAC[dist;
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];
80         ALL_TAC] THEN
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
95       DISJ1_TAC THEN
96       REPEAT(POP_ASSUM MP_TAC) THEN CONV_TAC REAL_FIELD]]);;
97
98 (* ------------------------------------------------------------------------- *)
99 (*                       Feuerbach's theorem                                 *)
100 (*                                                                           *)
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 (* ------------------------------------------------------------------------- *)
110
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
143   REPEAT GEN_TAC 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);;
152
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 (* ------------------------------------------------------------------------- *)
159
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`,
175   REPEAT GEN_TAC THEN
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);;
186
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`,
203   REPEAT GEN_TAC THEN
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);;