100/morley.ml

   1 (* ========================================================================= *)
   2 (* Formalization of Alain Connes's paper "A new proof of Morley's theorem".  *)
   3 (* ========================================================================= *)
   4
   5 needs "Library/iter.ml";;
   6 needs "Multivariate/geom.ml";;
   7
   8 (* ------------------------------------------------------------------------- *)
   9 (* Reflection about the line[0,e^{i t}]                                      *)
  10 (* ------------------------------------------------------------------------- *)
  11
  12 let reflect2d = new_definition
  13  `reflect2d t = rotate2d t o cnj o rotate2d(--t)`;;
  14
  15 let REFLECT2D_COMPOSE = prove
  16  (`!s t. reflect2d s o reflect2d t = rotate2d (&2 * (s - t))`,
  17   REWRITE_TAC[FUN_EQ_THM; o_THM; reflect2d] THEN REPEAT GEN_TAC THEN
  18   REWRITE_TAC[ROTATE2D_COMPLEX; CNJ_CEXP; CNJ_MUL; CNJ_CNJ] THEN
  19   REWRITE_TAC[CNJ_II; CNJ_CX; CNJ_NEG; COMPLEX_MUL_ASSOC] THEN
  20   AP_THM_TAC THEN AP_TERM_TAC THEN REWRITE_TAC[GSYM CEXP_ADD] THEN
  21   REWRITE_TAC[CX_NEG; COMPLEX_MUL_LNEG; COMPLEX_MUL_RNEG; CX_MUL] THEN
  22   AP_TERM_TAC THEN SIMPLE_COMPLEX_ARITH_TAC);;
  23
  24 (* ------------------------------------------------------------------------- *)
  25 (* Rotation about point "a" by angle "t".                                    *)
  26 (* ------------------------------------------------------------------------- *)
  27
  28 let rotate_about = new_definition
  29  `rotate_about a t x = a + rotate2d t (x - a)`;;
  30
  31 (* ------------------------------------------------------------------------- *)
  32 (* Reflection across line (a,b).                                             *)
  33 (* ------------------------------------------------------------------------- *)
  34
  35 let reflect_across = new_definition
  36  `reflect_across (a,b) x = a + reflect2d (Arg(b - a)) (x - a)`;;
  37
  38 let REFLECT_ACROSS_COMPOSE = prove
  39  (`!a b c.
  40         ~(b = a) /\ ~(c = a)
  41         ==> reflect_across(a,b) o reflect_across(a,c) =
  42             rotate_about a (&2 * Arg((b - a) / (c - a)))`,
  43   REPEAT STRIP_TAC THEN
  44   REWRITE_TAC[reflect_across; FUN_EQ_THM; o_THM; rotate_about] THEN
  45   REWRITE_TAC[VECTOR_ARITH `(a + x) - a:real^N = x`] THEN
  46   REWRITE_TAC[REWRITE_RULE[FUN_EQ_THM; o_THM] REFLECT2D_COMPOSE] THEN
  47   X_GEN_TAC `x:complex` THEN AP_TERM_TAC THEN
  48   REWRITE_TAC[REAL_MUL_2; ROTATE2D_ADD] THEN
  49   ASM_SIMP_TAC[ROTATE2D_SUB_ARG; COMPLEX_SUB_0]);;
  50
  51 let REFLECT_ACROSS_COMPOSE_ANGLE = prove
  52  (`!a b c.
  53         ~(b = a) /\ ~(c = a) /\ &0 <= Im((c - a) / (b - a))
  54         ==> reflect_across(a,c) o reflect_across(a,b) =
  55             rotate_about a (&2 * angle(c,a,b))`,
  56   REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[ANGLE_SYM] THEN
  57   ASM_SIMP_TAC[REFLECT_ACROSS_COMPOSE] THEN
  58   ASM_SIMP_TAC[angle; VECTOR_ANGLE_ARG; COMPLEX_SUB_0;
  59                REAL_SUB_ARG; ARG_LE_PI]);;
  60
  61 let REFLECT_ACROSS_COMPOSE_INVOLUTION = prove
  62  (`!a b. ~(a = b) ==> reflect_across(a,b) o reflect_across(a,b) = I`,
  63   SIMP_TAC[REFLECT_ACROSS_COMPOSE; COMPLEX_DIV_REFL; COMPLEX_SUB_0] THEN
  64   REWRITE_TAC[ARG_NUM; REAL_MUL_RZERO; rotate_about; FUN_EQ_THM] THEN
  65   REWRITE_TAC[ROTATE2D_ZERO; I_THM] THEN
  66   REPEAT STRIP_TAC THEN VECTOR_ARITH_TAC);;
  67
  68 let REFLECT_ACROSS_SYM = prove
  69  (`!a b. reflect_across(a,b) = reflect_across(b,a)`,
  70   REPEAT GEN_TAC THEN
  71   ASM_CASES_TAC `a:complex = b` THEN ASM_REWRITE_TAC[] THEN
  72   REWRITE_TAC[FUN_EQ_THM; reflect_across; reflect2d; o_THM] THEN
  73   REWRITE_TAC[ROTATE2D_COMPLEX; CNJ_CEXP; CNJ_MUL; CNJ_CX; CNJ_II] THEN
  74   REWRITE_TAC[CX_NEG; COMPLEX_RING `--ii * --z = ii * z`] THEN
  75   SUBGOAL_THEN `cexp(ii * Cx(Arg(b - a))) = (b - a) / Cx(norm(b - a)) /\
  76                 cexp(ii * Cx(Arg(a - b))) = (a - b) / Cx(norm(a - b))`
  77   (CONJUNCTS_THEN SUBST1_TAC) THENL
  78    [CONJ_TAC THEN MATCH_MP_TAC(COMPLEX_FIELD
  79      `~(a = Cx(&0)) /\ a * b = c ==> b = c / a`) THEN
  80     ASM_REWRITE_TAC[GSYM ARG; CX_INJ; NORM_EQ_0; VECTOR_SUB_EQ];
  81     REWRITE_TAC[COMPLEX_RING `a * a * cnj b = a pow 2 * cnj b`] THEN
  82     SUBST1_TAC(ISPECL [`a:complex`; `b:complex`] NORM_SUB) THEN
  83     X_GEN_TAC `z:complex` THEN REWRITE_TAC[complex_div] THEN
  84     MATCH_MP_TAC(COMPLEX_RING
  85      `b - a = ((b - a) * n) pow 2 * (cnj za - cnj zb)
  86       ==> a + ((b - a) * n) pow 2 * cnj za =
  87           b + ((a - b) * n) pow 2 * cnj zb`) THEN
  88     REWRITE_TAC[CNJ_SUB; COMPLEX_RING `(z - a) - (z - b):complex = b - a`] THEN
  89     MATCH_MP_TAC(COMPLEX_FIELD
  90      `(b' - a') * (b - a) = n pow 2 /\ ~(n = Cx(&0))
  91       ==> b - a = ((b - a) * inv n) pow 2 * (b' - a')`) THEN
  92     REWRITE_TAC[GSYM CNJ_SUB; COMPLEX_MUL_CNJ; CX_INJ] THEN
  93     ASM_REWRITE_TAC[COMPLEX_NORM_ZERO; COMPLEX_SUB_0]]);;
  94
  95 (* ------------------------------------------------------------------------- *)
  96 (* Some additional lemmas.                                                   *)
  97 (* ------------------------------------------------------------------------- *)
  98
  99 let ITER_ROTATE_ABOUT = prove
 100  (`!n a t. ITER n (rotate_about a t) = rotate_about a (&n * t)`,
 101   REWRITE_TAC[FUN_EQ_THM; rotate_about] THEN
 102   REWRITE_TAC[VECTOR_ARITH `a + b:real^N = a + c <=> b = c`] THEN
 103   INDUCT_TAC THEN REWRITE_TAC[ITER_ALT; REAL_MUL_LZERO; ROTATE2D_ZERO] THEN
 104   REWRITE_TAC[VECTOR_ARITH `a + x - a:real^N = x`; GSYM REAL_OF_NUM_SUC] THEN
 105   ASM_REWRITE_TAC[REAL_ADD_RDISTRIB; ROTATE2D_ADD] THEN
 106   REPEAT GEN_TAC THEN AP_TERM_TAC THEN AP_TERM_TAC THEN
 107   REWRITE_TAC[rotate_about; REAL_MUL_LID] THEN VECTOR_ARITH_TAC);;
 108
 109 let REAL_LE_IM_DIV_CYCLIC = prove
 110  (`!a b c. &0 <= Im ((c - a) / (b - a)) <=> &0 <= Im((a - b) / (c - b))`,
 111   REWRITE_TAC[IM_COMPLEX_DIV_GE_0] THEN
 112   REWRITE_TAC[complex_mul; IM; IM_SUB; RE_SUB; IM_CNJ; CNJ_SUB; RE_CNJ] THEN
 113   REAL_ARITH_TAC);;
 114
 115 let ROTATE_ABOUT_INVERT = prove
 116  (`rotate_about a t w = z <=> w = rotate_about a (--t) z`,
 117   MATCH_MP_TAC(MESON[]
 118    `(!x. f(g x) = x) /\ (!y. g(f y) = y)
 119     ==> (f x = y <=> x = g y)`) THEN
 120   REWRITE_TAC[rotate_about; VECTOR_ADD_SUB; GSYM ROTATE2D_ADD] THEN
 121   REWRITE_TAC[REAL_ADD_LINV; REAL_ADD_RINV] THEN
 122   REWRITE_TAC[ROTATE2D_ZERO] THEN VECTOR_ARITH_TAC);;
 123
 124 let ROTATE_EQ_REFLECT_LEMMA = prove
 125  (`!a b z t.
 126         ~(b = a) /\ &2 * Arg((b - a) / (z - a)) = t
 127         ==> rotate_about a t z = reflect_across (a,b) z`,
 128   REPEAT STRIP_TAC THEN REWRITE_TAC[rotate_about; reflect_across] THEN
 129   AP_TERM_TAC THEN REWRITE_TAC[ROTATE2D_COMPLEX; reflect2d; o_THM] THEN
 130   REWRITE_TAC[CNJ_MUL; COMPLEX_MUL_ASSOC; CNJ_CEXP; CNJ_II] THEN
 131   REWRITE_TAC[CNJ_CX; COMPLEX_MUL_LNEG; COMPLEX_MUL_RNEG; COMPLEX_NEG_NEG;
 132               GSYM CEXP_ADD; CX_NEG] THEN
 133   REWRITE_TAC[COMPLEX_RING `ii * a + ii * a = ii * Cx(&2) * a`] THEN
 134   ASM_CASES_TAC `z:complex = a` THEN
 135   ASM_REWRITE_TAC[CNJ_CX; COMPLEX_MUL_RZERO; COMPLEX_SUB_REFL] THEN
 136   FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP (COMPLEX_RING
 137    `~(z = a)
 138     ==> c * (z - a) pow 2 = b * cnj (z - a) * (z - a)
 139         ==> c * (z - a) = b * cnj(z - a)`)) THEN
 140   REWRITE_TAC[COMPLEX_MUL_CNJ] THEN
 141   GEN_REWRITE_TAC (LAND_CONV o RAND_CONV o LAND_CONV) [ARG] THEN
 142   MATCH_MP_TAC(COMPLEX_RING
 143    `(e1:complex) * e2 pow 2 = e3 ==> e1 * (n * e2) pow 2 = e3 * n pow 2`) THEN
 144   REWRITE_TAC[GSYM CEXP_ADD; GSYM CEXP_N; CEXP_EQ] THEN
 145   REWRITE_TAC[COMPLEX_RING
 146    `ii * t + Cx(&2) * ii * z = ii * u + v * ii <=>
 147     t + Cx(&2) * z - u = v`] THEN
 148   REWRITE_TAC[GSYM CX_MUL; GSYM CX_SUB; GSYM CX_ADD; CX_INJ] THEN
 149   EXPAND_TAC "t" THEN
 150   REWRITE_TAC[GSYM REAL_SUB_LDISTRIB; GSYM REAL_ADD_LDISTRIB] THEN
 151   REWRITE_TAC[REAL_ARITH `&2 * a = &2 * b <=> a = b`] THEN
 152   ONCE_REWRITE_TAC[REAL_ARITH `a + (b - c):real = a - (c - b)`] THEN
 153   ASM_SIMP_TAC[REAL_SUB_ARG; COMPLEX_SUB_0] THEN COND_CASES_TAC THENL
 154    [EXISTS_TAC `&0`; EXISTS_TAC `&2`] THEN
 155   SIMP_TAC[INTEGER_CLOSED] THEN REAL_ARITH_TAC);;
 156
 157 let ROTATE_EQ_REFLECT_PI_LEMMA = prove
 158  (`!a b z t.
 159         ~(b = a) /\ &2 * Arg((b - a) / (z - a)) = &4 * pi + t
 160         ==> rotate_about a t z = reflect_across (a,b) z`,
 161   REWRITE_TAC[REAL_ARITH `a = &4 * pi + t <=> t = a + --(&4 * pi)`] THEN
 162   REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
 163   MATCH_MP_TAC EQ_TRANS THEN
 164   EXISTS_TAC `rotate_about a (&2 * Arg((b - a) / (z - a))) z` THEN
 165   CONJ_TAC THENL
 166    [ALL_TAC; MATCH_MP_TAC ROTATE_EQ_REFLECT_LEMMA THEN ASM_REWRITE_TAC[]] THEN
 167   REWRITE_TAC[rotate_about; ROTATE2D_ADD] THEN
 168   AP_TERM_TAC THEN AP_TERM_TAC THEN
 169   REWRITE_TAC[ROTATE2D_COMPLEX] THEN
 170   REWRITE_TAC[EULER; RE_MUL_II; IM_MUL_II; RE_CX; IM_CX; COS_NEG; SIN_NEG] THEN
 171   REWRITE_TAC[SIN_NPI; COS_NPI; REAL_EXP_NEG; REAL_EXP_0; CX_NEG] THEN
 172   REWRITE_TAC[COMPLEX_NEG_0; COMPLEX_MUL_RZERO; COMPLEX_ADD_RID] THEN
 173   CONV_TAC REAL_RAT_REDUCE_CONV THEN REWRITE_TAC[COMPLEX_MUL_LID]);;
 174
 175 (* ------------------------------------------------------------------------- *)
 176 (* Algebraic characterization of equilateral triangle.                       *)
 177 (* ------------------------------------------------------------------------- *)
 178
 179 let EQUILATERAL_TRIANGLE_ALGEBRAIC = prove
 180  (`!A B C j.
 181         j pow 3 = Cx(&1) /\ ~(j = Cx(&1)) /\
 182         A + j * B + j pow 2 * C = Cx(&0)
 183         ==> dist(A,B) = dist(B,C) /\ dist(C,A) = dist(B,C)`,
 184   REPEAT GEN_TAC THEN STRIP_TAC THEN REWRITE_TAC[dist] THEN
 185   SUBGOAL_THEN `C - A:complex = j * (B - C) /\ A - B = j pow 2 * (B - C)`
 186   (CONJUNCTS_THEN SUBST1_TAC) THENL
 187    [REPEAT(POP_ASSUM MP_TAC) THEN CONV_TAC COMPLEX_RING;
 188     ALL_TAC] THEN
 189   SUBGOAL_THEN `norm(j pow 3) = &1` MP_TAC THENL
 190    [ASM_REWRITE_TAC[COMPLEX_NORM_CX; REAL_ABS_NUM];
 191     REWRITE_TAC[COMPLEX_NORM_POW; REAL_POW_EQ_1; ARITH; REAL_ABS_NORM] THEN
 192     DISCH_THEN(ASSUME_TAC o CONJUNCT1)] THEN
 193   ASM_REWRITE_TAC[COMPLEX_NORM_MUL; COMPLEX_NORM_POW] THEN
 194   REAL_ARITH_TAC);;
 195
 196 (* ------------------------------------------------------------------------- *)
 197 (* The main algebraic lemma.                                                 *)
 198 (* ------------------------------------------------------------------------- *)
 199
 200 let AFFINE_GROUP_ITER_3 = prove
 201  (`ITER 3 (\z. a * z + b) = (\z. a pow 3 * z + b * (Cx(&1) + a + a pow 2))`,
 202   REWRITE_TAC[TOP_DEPTH_CONV num_CONV `3`] THEN
 203   REWRITE_TAC[ITER; FUN_EQ_THM] THEN CONV_TAC NUM_REDUCE_CONV THEN
 204   CONV_TAC COMPLEX_RING);;
 205
 206 let AFFINE_GROUP_COMPOSE = prove
 207  (`(\z. a1 * z + b1) o (\z. a2 * z + b2) =
 208    (\z. (a1 * a2) * z + (b1 + a1 * b2))`,
 209   REWRITE_TAC[o_THM; FUN_EQ_THM] THEN CONV_TAC COMPLEX_RING);;
 210
 211 let AFFINE_GROUP_I = prove
 212  (`I = (\z. Cx(&1) * z + Cx(&0))`,
 213   REWRITE_TAC[I_THM; FUN_EQ_THM] THEN CONV_TAC COMPLEX_RING);;
 214
 215 let AFFINE_GROUP_EQ = prove
 216  (`!a b a' b. (\z. a * z + b) = (\z. a' * z + b') <=> a = a' /\ b = b'`,
 217   REPEAT GEN_TAC THEN EQ_TAC THEN SIMP_TAC[FUN_EQ_THM] THEN DISCH_TAC THEN
 218   FIRST_ASSUM(MP_TAC o SPEC `Cx(&0)`) THEN
 219   FIRST_X_ASSUM(MP_TAC o SPEC `Cx(&1)`) THEN
 220   CONV_TAC COMPLEX_RING);;
 221
 222 let AFFINE_GROUP_ROTATE_ABOUT = prove
 223  (`!a t. rotate_about a t =
 224          (\z. cexp(ii * Cx(t)) * z + (Cx(&1) - cexp(ii * Cx(t))) * a)`,
 225   REWRITE_TAC[rotate_about; FUN_EQ_THM; ROTATE2D_COMPLEX] THEN
 226   CONV_TAC COMPLEX_RING);;
 227
 228 let ALGEBRAIC_LEMMA = prove
 229  (`!a1 a2 a3 b1 b2 b3 A B C.
 230         (\z. a3 * z + b3) ((\z. a1 * z + b1) B) = B /\
 231         (\z. a1 * z + b1) ((\z. a2 * z + b2) C) = C /\
 232         (\z. a2 * z + b2) ((\z. a3 * z + b3) A) = A /\
 233         ITER 3 (\z. a1 * z + b1) o ITER 3 (\z. a2 * z + b2) o
 234         ITER 3 (\z. a3 * z + b3) = I /\
 235         ~(a1 * a2 * a3 = Cx(&1)) /\
 236         ~(a1 * a2 = Cx(&1)) /\
 237         ~(a2 * a3 = Cx(&1)) /\
 238         ~(a3 * a1 = Cx(&1))
 239         ==> (a1 * a2 * a3) pow 3 = Cx (&1) /\
 240             ~(a1 * a2 * a3 = Cx (&1)) /\
 241             C + (a1 * a2 * a3) * A + (a1 * a2 * a3) pow 2 * B = Cx(&0)`,
 242   REWRITE_TAC[AFFINE_GROUP_ITER_3; AFFINE_GROUP_COMPOSE; AFFINE_GROUP_I;
 243               AFFINE_GROUP_EQ] THEN
 244   REPEAT GEN_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN CONJ_TAC THENL
 245    [REPEAT(POP_ASSUM MP_TAC) THEN CONV_TAC COMPLEX_RING; ALL_TAC] THEN
 246   SUBGOAL_THEN
 247    `(a1 * a2 * a3) * a1 pow 2 * a2 *
 248     (a1 - a1 * a2 * a3) * (a2 - a1 * a2 * a3) * (a3 - a1 * a2 * a3) *
 249     (C + (a1 * a2 * a3) * A + (a1 * a2 * a3) pow 2 * B) = Cx(&0)`
 250   MP_TAC THENL
 251    [REPEAT(FIRST_X_ASSUM(MP_TAC o MATCH_MP (COMPLEX_FIELD
 252      `a3 * (a1 * B + b1) + b3 = B
 253       ==> ~(a1 * a3 = Cx(&1))
 254           ==> B = (a3 * b1 + b3) / (Cx(&1) - a1 * a3)`))) THEN
 255     REPEAT(ANTS_TAC THENL
 256      [ASM_MESON_TAC[COMPLEX_MUL_SYM]; DISCH_THEN SUBST1_TAC]) THEN
 257     FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (COMPLEX_RING
 258      `s = Cx(&0) ==> s + t = Cx(&0) ==> t = Cx(&0)`));
 259     REWRITE_TAC[COMPLEX_ENTIRE]] THEN
 260   REPEAT(POP_ASSUM MP_TAC) THEN CONV_TAC COMPLEX_FIELD);;
 261
 262 (* ------------------------------------------------------------------------- *)
 263 (* A tactic to avoid some duplication over cyclic permutations.              *)
 264 (* ------------------------------------------------------------------------- *)
 265
 266 let CYCLIC_PERM_SUBGOAL_THEN =
 267   let lemma = MESON[]
 268    `(!A B C P Q R a b c g1 g2 g3.
 269        Ant A B C P Q R a b c g1 g2 g3 ==> Cns A B C P Q R a b c g1 g2 g3)
 270     ==> (!A B C P Q R a b c g1 g2 g3.
 271            Ant A B C P Q R a b c g1 g2 g3
 272            ==> Ant B C A Q R P b c a g2 g3 g1)
 273         ==> (!A B C P Q R a b c g1 g2 g3.
 274                    Ant A B C P Q R a b c g1 g2 g3
 275                    ==> Cns A B C P Q R a b c g1 g2 g3 /\
 276                        Cns B C A Q R P b c a g2 g3 g1 /\
 277                        Cns C A B R P Q c a b g3 g1 g2)`
 278   and vars =
 279    [`A:complex`; `B:complex`; `C:complex`;
 280     `P:complex`; `Q:complex`; `R:complex`;
 281     `a:real`; `b:real`; `c:real`;
 282     `g1:complex->complex`; `g2:complex->complex`; `g3:complex->complex`] in
 283   fun t ttac (asl,w) ->
 284       let asm = list_mk_conj (map (concl o snd) (rev asl)) in
 285       let gnw = list_mk_forall(vars,mk_imp(asm,t)) in
 286       let th1 = MATCH_MP lemma (ASSUME gnw) in
 287       let tm1 = fst(dest_imp(concl th1)) in
 288       let th2 = REWRITE_CONV[INSERT_AC; CONJ_ACI; ANGLE_SYM; EQ_SYM_EQ] tm1 in
 289       let th3 = DISCH_ALL(MP th1 (EQT_ELIM th2)) in
 290       (MP_TAC th3 THEN ANTS_TAC THENL
 291         [POP_ASSUM_LIST(K ALL_TAC) THEN REPEAT GEN_TAC THEN STRIP_TAC;
 292          DISCH_THEN(MP_TAC o SPEC_ALL) THEN ANTS_TAC THENL
 293           [REPEAT CONJ_TAC THEN FIRST_ASSUM ACCEPT_TAC;
 294            DISCH_THEN(CONJUNCTS_THEN2 ttac MP_TAC) THEN
 295            DISCH_THEN(CONJUNCTS_THEN ttac)]]) (asl,w);;
 296
 297 (* ------------------------------------------------------------------------- *)
 298 (* Morley's theorem a la Connes.                                             *)
 299 (* ------------------------------------------------------------------------- *)
 300
 301 let MORLEY = prove
 302  (`!A B C:real^2 P Q R.
 303      ~collinear{A,B,C} /\ {P,Q,R} SUBSET convex hull {A,B,C} /\
 304      angle(A,B,R) = angle(A,B,C) / &3 /\
 305      angle(B,A,R) = angle(B,A,C) / &3 /\
 306      angle(B,C,P) = angle(B,C,A) / &3 /\
 307      angle(C,B,P) = angle(C,B,A) / &3 /\
 308      angle(C,A,Q) = angle(C,A,B) / &3 /\
 309      angle(A,C,Q) = angle(A,C,B) / &3
 310      ==> dist(R,P) = dist(P,Q) /\ dist(Q,R) = dist(P,Q)`,
 311   MATCH_MP_TAC(MESON[]
 312     `(!A B C. &0 <= Im((C - A) / (B - A)) \/
 313               &0 <= Im((B - A) / (C - A))) /\
 314      (!A B C. Property A B C ==> Property A C B) /\
 315      (!A B C. &0 <= Im((C - A) / (B - A)) ==> Property A B C)
 316      ==> !A B C. Property A B C`) THEN
 317   REPEAT CONJ_TAC THENL
 318    [REPEAT GEN_TAC THEN
 319     GEN_REWRITE_TAC RAND_CONV [GSYM IM_COMPLEX_INV_LE_0] THEN
 320     REWRITE_TAC[COMPLEX_INV_DIV] THEN REAL_ARITH_TAC;
 321     REPEAT GEN_TAC THEN DISCH_TAC THEN
 322     MAP_EVERY X_GEN_TAC [`P:real^2`; `Q:real^2`; `R:real^2`] THEN
 323     REWRITE_TAC[ANGLE_SYM; DIST_SYM; INSERT_AC] THEN
 324     FIRST_X_ASSUM(MP_TAC o SPECL [`P:real^2`; `R:real^2`; `Q:real^2`]) THEN
 325     REWRITE_TAC[ANGLE_SYM; DIST_SYM; INSERT_AC] THEN MESON_TAC[];
 326     ALL_TAC] THEN
 327   REPEAT GEN_TAC THEN DISCH_TAC THEN REPEAT GEN_TAC THEN
 328   MAP_EVERY (fun t ->
 329     ASM_CASES_TAC t THENL [ASM_REWRITE_TAC[COLLINEAR_2; INSERT_AC]; ALL_TAC])
 330    [`A:real^2 = B`; `A:real^2 = C`; `B:real^2 = C`] THEN
 331   STRIP_TAC THEN
 332   FIRST_ASSUM(fun th ->
 333        let th' = GEN_REWRITE_RULE I [REAL_LE_IM_DIV_CYCLIC] th in
 334        let th'' = GEN_REWRITE_RULE I [REAL_LE_IM_DIV_CYCLIC] th' in
 335        ASSUME_TAC th' THEN ASSUME_TAC th'') THEN
 336   ABBREV_TAC `a = angle(C:real^2,A,B) / &3` THEN
 337   ABBREV_TAC `b = angle(A:real^2,B,C) / &3` THEN
 338   ABBREV_TAC `c = angle(B:real^2,C,A) / &3` THEN
 339   ABBREV_TAC `g1 = rotate_about A (&2 * a)` THEN
 340   ABBREV_TAC `g2 = rotate_about B (&2 * b)` THEN
 341   ABBREV_TAC `g3 = rotate_about C (&2 * c)` THEN
 342   CYCLIC_PERM_SUBGOAL_THEN
 343     `ITER 3 g1 o ITER 3 g2 o ITER 3 g3 = (I:real^2->real^2)`
 344   ASSUME_TAC THENL
 345    [MAP_EVERY EXPAND_TAC ["g1"; "g2"; "g3"] THEN
 346     REWRITE_TAC[ITER_ROTATE_ABOUT] THEN
 347     MAP_EVERY EXPAND_TAC ["a"; "b"; "c"] THEN
 348     REWRITE_TAC[REAL_ARITH `&3 * &2 * a / &3 = &2 * a`] THEN
 349     ASM_SIMP_TAC[GSYM REFLECT_ACROSS_COMPOSE_ANGLE] THEN
 350     REWRITE_TAC[FUN_EQ_THM; o_THM; I_THM; REFLECT_ACROSS_SYM] THEN
 351     ASM_SIMP_TAC[REWRITE_RULE[FUN_EQ_THM; I_THM; o_THM]
 352                  REFLECT_ACROSS_COMPOSE_INVOLUTION];
 353     ALL_TAC] THEN
 354   CYCLIC_PERM_SUBGOAL_THEN `&0 <= Im((P - B) / (C - B))`
 355   STRIP_ASSUME_TAC THENL
 356    [FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [INSERT_SUBSET]) THEN
 357     REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET] THEN
 358     REPEAT(MATCH_MP_TAC MONO_AND THEN CONJ_TAC) THEN
 359     REWRITE_TAC[CONVEX_HULL_3; IN_ELIM_THM] THEN
 360     STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
 361     SIMP_TAC[VECTOR_ARITH `(u % A + v % B + w % C) - B:real^N =
 362                  u % (A - B) + w % (C - B) + ((u + v + w) - &1) % B`] THEN
 363     ASM_REWRITE_TAC[REAL_SUB_REFL; VECTOR_MUL_LZERO; VECTOR_ADD_RID] THEN
 364     REWRITE_TAC[complex_div; COMPLEX_ADD_RDISTRIB; IM_ADD; COMPLEX_CMUL] THEN
 365     REWRITE_TAC[GSYM COMPLEX_MUL_ASSOC] THEN REWRITE_TAC[GSYM complex_div] THEN
 366     ASM_SIMP_TAC[IM_MUL_CX; COMPLEX_DIV_REFL; COMPLEX_SUB_0; IM_CX] THEN
 367     SIMP_TAC[REAL_MUL_RZERO; REAL_ADD_RID] THEN MATCH_MP_TAC REAL_LE_MUL THEN
 368     ASM_REAL_ARITH_TAC;
 369     ALL_TAC] THEN
 370   CYCLIC_PERM_SUBGOAL_THEN `&0 <= Im((B - C) / (P - C))`
 371   STRIP_ASSUME_TAC THENL
 372    [REWRITE_TAC[GSYM IM_COMPLEX_INV_LE_0; COMPLEX_INV_DIV] THEN
 373     FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [INSERT_SUBSET]) THEN
 374     REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET] THEN
 375     REPEAT(MATCH_MP_TAC MONO_AND THEN CONJ_TAC) THEN
 376     REWRITE_TAC[CONVEX_HULL_3; IN_ELIM_THM] THEN
 377     STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
 378     SIMP_TAC[VECTOR_ARITH `(u % A + v % B + w % C) - C:real^N =
 379                    v % (B - C) + u % (A - C) + ((u + v + w) - &1) % C`] THEN
 380     ASM_REWRITE_TAC[REAL_SUB_REFL; VECTOR_MUL_LZERO; VECTOR_ADD_RID] THEN
 381     REWRITE_TAC[complex_div; COMPLEX_ADD_RDISTRIB; IM_ADD; COMPLEX_CMUL] THEN
 382     REWRITE_TAC[GSYM COMPLEX_MUL_ASSOC] THEN REWRITE_TAC[GSYM complex_div] THEN
 383     ASM_SIMP_TAC[IM_MUL_CX; COMPLEX_DIV_REFL; COMPLEX_SUB_0; IM_CX] THEN
 384     SIMP_TAC[REAL_MUL_RZERO; REAL_ADD_LID] THEN
 385     MATCH_MP_TAC(REAL_ARITH `&0 <= u * --a ==> u * a <= &0`) THEN
 386     MATCH_MP_TAC REAL_LE_MUL THEN ASM_REWRITE_TAC[] THEN
 387     REWRITE_TAC[REAL_ARITH `&0 <= --x <=> x <= &0`] THEN
 388     ASM_REWRITE_TAC[GSYM IM_COMPLEX_INV_GE_0; COMPLEX_INV_DIV];
 389     ALL_TAC] THEN
 390   CYCLIC_PERM_SUBGOAL_THEN
 391    `~(P:real^2 = B) /\ ~(P = C)`
 392   STRIP_ASSUME_TAC THENL
 393    [SUBGOAL_THEN `!x y z. ~(angle(x:real^2,y,z) / &3 = pi / &2)`
 394      (fun th -> ASM_MESON_TAC[th; ANGLE_REFL]) THEN
 395     REPEAT GEN_TAC THEN
 396     MATCH_MP_TAC(REAL_ARITH
 397      `a <= pi /\ &0 < pi ==> ~(a / &3 = pi / &2)`) THEN
 398     REWRITE_TAC[ANGLE_RANGE; PI_POS];
 399     ALL_TAC] THEN
 400   CYCLIC_PERM_SUBGOAL_THEN
 401    `(g3:complex->complex)(g1(Q)) = Q`
 402   ASSUME_TAC THENL
 403    [MAP_EVERY EXPAND_TAC ["g1"; "g3"] THEN
 404     ONCE_REWRITE_TAC[ROTATE_ABOUT_INVERT] THEN
 405     MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC `reflect_across(A,C) Q` THEN
 406     CONJ_TAC THENL
 407      [MATCH_MP_TAC ROTATE_EQ_REFLECT_LEMMA THEN
 408       ASM_REWRITE_TAC[] THEN AP_TERM_TAC THEN
 409       GEN_REWRITE_TAC RAND_CONV [SYM(ASSUME `angle(C:real^2,A,Q) = a`)] THEN
 410       REWRITE_TAC[angle] THEN ONCE_REWRITE_TAC[VECTOR_ANGLE_SYM] THEN
 411       ASM_SIMP_TAC[VECTOR_ANGLE_ARG; COMPLEX_SUB_0];
 412       ALL_TAC] THEN
 413     CONV_TAC SYM_CONV THEN ONCE_REWRITE_TAC[REFLECT_ACROSS_SYM] THEN
 414     MATCH_MP_TAC ROTATE_EQ_REFLECT_PI_LEMMA THEN
 415     ASM_REWRITE_TAC[GSYM REAL_MUL_RNEG] THEN
 416     REWRITE_TAC[REAL_ARITH `&2 * a = &4 * pi + &2 * --c <=>
 417                             a = &2 * pi - c`] THEN
 418     GEN_REWRITE_TAC (RAND_CONV o RAND_CONV)
 419      [SYM(ASSUME `angle(B:real^2,C,A) / &3 = c`)] THEN
 420     ONCE_REWRITE_TAC[ANGLE_SYM] THEN FIRST_ASSUM(fun th ->
 421      GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [SYM th]) THEN
 422     REWRITE_TAC[angle] THEN
 423     ASM_SIMP_TAC[VECTOR_ANGLE_ARG; COMPLEX_SUB_0] THEN
 424     GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [GSYM COMPLEX_INV_DIV] THEN
 425     MATCH_MP_TAC ARG_INV THEN REWRITE_TAC[GSYM ARG_EQ_0] THEN
 426     DISCH_TAC THEN
 427     SUBGOAL_THEN `angle(A:real^2,C,Q) = &0` MP_TAC THENL
 428      [REWRITE_TAC[angle] THEN ASM_SIMP_TAC[VECTOR_ANGLE_ARG; COMPLEX_SUB_0];
 429       ASM_REWRITE_TAC[REAL_ARITH `a / &3 = &0 <=> a = &0`]] THEN
 430     ASM_MESON_TAC[COLLINEAR_ANGLE; ANGLE_SYM; INSERT_AC];
 431     ALL_TAC] THEN
 432   REPEAT(FIRST_X_ASSUM(MP_TAC o
 433     GEN_REWRITE_RULE LAND_CONV [AFFINE_GROUP_ROTATE_ABOUT])) THEN
 434   CYCLIC_PERM_SUBGOAL_THEN
 435    `~(cexp(ii * Cx(&2 * a)) * cexp(ii * Cx(&2 * b)) = Cx(&1)) /\
 436     ~(cexp(ii * Cx(&2 * a)) * cexp(ii * Cx(&2 * b)) *
 437       cexp(ii * Cx(&2 * c)) = Cx(&1))`
 438   STRIP_ASSUME_TAC THENL
 439    [REWRITE_TAC[GSYM CEXP_ADD; GSYM COMPLEX_ADD_LDISTRIB; GSYM CX_ADD] THEN
 440     MP_TAC(REAL_ARITH
 441      `&0 <= a /\ &0 <= b /\ &0 <= c /\ &0 < pi /\
 442       &3 * a + &3 * b + &3 * c = pi /\ ~(&3 * c = pi)
 443       ==> (&0 < &2 * a + &2 * b /\ &2 * a + &2 * b < &2 * pi) /\
 444           (&0 < &2 * a + &2 * b + &2 * c /\
 445            &2 * a + &2 * b + &2 * c < &2 * pi)`) THEN
 446     ANTS_TAC THENL
 447      [MAP_EVERY EXPAND_TAC ["a"; "b"; "c"] THEN
 448       REWRITE_TAC[REAL_ARITH `&3 * x / &3 = x`; PI_POS] THEN
 449       SIMP_TAC[ANGLE_RANGE; REAL_LE_DIV; REAL_POS] THEN CONJ_TAC THENL
 450        [ASM_MESON_TAC[TRIANGLE_ANGLE_SUM; ADD_AC; ANGLE_SYM];
 451         ASM_MESON_TAC[COLLINEAR_ANGLE; ANGLE_SYM; INSERT_AC]];
 452       MATCH_MP_TAC MONO_AND THEN CONJ_TAC THEN
 453       REWRITE_TAC[CEXP_II_NE_1; GSYM CX_ADD]];
 454     ALL_TAC] THEN
 455   MAP_EVERY ABBREV_TAC
 456    [`a1 = cexp(ii * Cx(&2 * a))`;
 457     `a2 = cexp(ii * Cx(&2 * b))`;
 458     `a3 = cexp(ii * Cx(&2 * c))`;
 459     `b1 = (Cx (&1) - a1) * A`;
 460     `b2 = (Cx (&1) - a2) * B`;
 461     `b3 = (Cx (&1) - a3) * C`] THEN
 462   REPEAT DISCH_TAC THEN MATCH_MP_TAC EQUILATERAL_TRIANGLE_ALGEBRAIC THEN
 463   EXISTS_TAC `a1 * a2 * a3:complex` THEN
 464   MATCH_MP_TAC ALGEBRAIC_LEMMA THEN
 465   MAP_EVERY EXISTS_TAC [`b1:complex`; `b2:complex`; `b3:complex`] THEN
 466   PURE_ASM_REWRITE_TAC[] THEN REWRITE_TAC[]);;