100/isosceles.ml

   1 (* ========================================================================= *)
   2 (* Isosceles triangle theorem.                                               *)
   3 (* ========================================================================= *)
   4
   5 needs "Multivariate/geom.ml";;
   6
   7 (* ------------------------------------------------------------------------- *)
   8 (* The theorem, according to Wikipedia.                                      *)
   9 (* ------------------------------------------------------------------------- *)
  10
  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]);;
  15
  16 (* ------------------------------------------------------------------------- *)
  17 (* The obvious converse.                                                     *)
  18 (* ------------------------------------------------------------------------- *)
  19
  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]);;
  25
  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 (* ------------------------------------------------------------------------- *)
  30
  31 let lemma = prove
  32  (`!A B C D:real^N.
  33         between D (A,B)
  34         ==> (orthogonal (A - B) (C - D) <=>
  35                 angle(A,D,C) = pi / &2 /\ angle(B,D,C) = pi / &2)`,
  36   REPEAT GEN_TAC THEN
  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];
  41     ALL_TAC] THEN
  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];
  45     ALL_TAC] THEN
  46   DISCH_TAC THEN
  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]);;
  56
  57 let ISOSCELES_TRIANGLE_1 = prove
  58  (`!A B C D:real^N.
  59         dist(A,C) = dist(B,C) /\ D = midpoint(A,B)
  60         ==> angle(A,C,D) = angle(B,C,D)`,
  61   REPEAT STRIP_TAC THEN
  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]);;
  66
  67 let ISOSCELES_TRIANGLE_2 = prove
  68  (`!A B C D:real^N.
  69         between D (A,B) /\
  70         dist(A,C) = dist(B,C) /\ angle(A,C,D) = angle(B,C,D)
  71         ==> orthogonal (A - B) (C - D)`,
  72   REPEAT STRIP_TAC THEN
  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);;
  84
  85 let ISOSCELES_TRIANGLE_3 = prove
  86  (`!A B C D:real^N.
  87         between D (A,B) /\
  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
  95     ANTS_TAC THENL
  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];
  99     ALL_TAC] THEN
 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
 103     ANTS_TAC THENL
 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];
 107     ALL_TAC] THEN
 108   DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
 109   ASM_SIMP_TAC[lemma; MIDPOINT_COLLINEAR; BETWEEN_IMP_COLLINEAR] THEN
 110   STRIP_TAC THEN
 111   FIRST_ASSUM(ASSUME_TAC o MATCH_MP ISOSCELES_TRIANGLE_THEOREM) THEN
 112   MP_TAC(ISPECL
 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]);;
 133
 134 (* ------------------------------------------------------------------------- *)
 135 (* Now the converses to those as well.                                       *)
 136 (* ------------------------------------------------------------------------- *)
 137
 138 let ISOSCELES_TRIANGLE_4 = prove
 139  (`!A B C D:real^N.
 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]);;
 147
 148 let ISOSCELES_TRIANGLE_5 = prove
 149  (`!A B C D:real^N.
 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)`,
 153   REPEAT GEN_TAC THEN
 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`;
 167                  PI_NZ] THEN
 168     DISCH_THEN(MP_TAC o MATCH_MP ANGLE_EQ_PI_OTHERS) THEN
 169     MP_TAC PI_NZ THEN REAL_ARITH_TAC;
 170     ALL_TAC] THEN
 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`;
 178                  PI_NZ] THEN
 179     DISCH_THEN(MP_TAC o MATCH_MP ANGLE_EQ_PI_OTHERS) THEN
 180     MP_TAC PI_NZ THEN REAL_ARITH_TAC;
 181     ALL_TAC] THEN
 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[]);;
 189
 190 let ISOSCELES_TRIANGLE_6 = prove
 191  (`!A B C D:real^N.
 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;
 201                SIN_ANGLE_EQ] THEN
 202   STRIP_TAC THENL
 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
 208     ASM_REWRITE_TAC[];
 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)
 215     THENL
 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];
 222       ALL_TAC] THEN
 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]]);;