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);;