(* ========================================================================= *)
(* Formalization of Alain Connes's paper "A new proof of Morley's theorem".  *)
(* ========================================================================= *)

needs "Library/iter.ml";;
needs "Multivariate/geom.ml";;

(* ------------------------------------------------------------------------- *)
(* Reflection about the line[0,e^{i t}]                                      *)
(* ------------------------------------------------------------------------- *)

let reflect2d = new_definition
 `reflect2d t = rotate2d t o cnj o rotate2d(--t)`;;
let REFLECT2D_COMPOSE = 
prove (`!s t. reflect2d s o reflect2d t = rotate2d (&2 * (s - t))`,
REWRITE_TAC[FUN_EQ_THM; o_THM; reflect2d] THEN REPEAT GEN_TAC THEN REWRITE_TAC[ROTATE2D_COMPLEX; CNJ_CEXP; CNJ_MUL; CNJ_CNJ] THEN REWRITE_TAC[CNJ_II; CNJ_CX; CNJ_NEG; COMPLEX_MUL_ASSOC] THEN AP_THM_TAC THEN AP_TERM_TAC THEN REWRITE_TAC[GSYM CEXP_ADD] THEN REWRITE_TAC[CX_NEG; COMPLEX_MUL_LNEG; COMPLEX_MUL_RNEG; CX_MUL] THEN AP_TERM_TAC THEN SIMPLE_COMPLEX_ARITH_TAC);;
(* ------------------------------------------------------------------------- *) (* Rotation about point "a" by angle "t". *) (* ------------------------------------------------------------------------- *)
let rotate_about = new_definition
 `rotate_about a t x = a + rotate2d t (x - a)`;;
(* ------------------------------------------------------------------------- *) (* Reflection across line (a,b). *) (* ------------------------------------------------------------------------- *)
let reflect_across = new_definition
 `reflect_across (a,b) x = a + reflect2d (Arg(b - a)) (x - a)`;;
let REFLECT_ACROSS_COMPOSE = 
prove (`!a b c. ~(b = a) /\ ~(c = a) ==> reflect_across(a,b) o reflect_across(a,c) = rotate_about a (&2 * Arg((b - a) / (c - a)))`,
REPEAT STRIP_TAC THEN REWRITE_TAC[reflect_across; FUN_EQ_THM; o_THM; rotate_about] THEN REWRITE_TAC[VECTOR_ARITH `(a + x) - a:real^N = x`] THEN REWRITE_TAC[REWRITE_RULE[FUN_EQ_THM; o_THM] REFLECT2D_COMPOSE] THEN X_GEN_TAC `x:complex` THEN AP_TERM_TAC THEN REWRITE_TAC[REAL_MUL_2; ROTATE2D_ADD] THEN ASM_SIMP_TAC[ROTATE2D_SUB_ARG; COMPLEX_SUB_0]);;
let REFLECT_ACROSS_COMPOSE_ANGLE = 
prove (`!a b c. ~(b = a) /\ ~(c = a) /\ &0 <= Im((c - a) / (b - a)) ==> reflect_across(a,c) o reflect_across(a,b) = rotate_about a (&2 * angle(c,a,b))`,
REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[ANGLE_SYM] THEN ASM_SIMP_TAC[REFLECT_ACROSS_COMPOSE] THEN ASM_SIMP_TAC[angle; VECTOR_ANGLE_ARG; COMPLEX_SUB_0; REAL_SUB_ARG; ARG_LE_PI]);;
let REFLECT_ACROSS_COMPOSE_INVOLUTION = 
prove (`!a b. ~(a = b) ==> reflect_across(a,b) o reflect_across(a,b) = I`,
SIMP_TAC[REFLECT_ACROSS_COMPOSE; COMPLEX_DIV_REFL; COMPLEX_SUB_0] THEN REWRITE_TAC[ARG_NUM; REAL_MUL_RZERO; rotate_about; FUN_EQ_THM] THEN REWRITE_TAC[ROTATE2D_ZERO; I_THM] THEN REPEAT STRIP_TAC THEN VECTOR_ARITH_TAC);;
let REFLECT_ACROSS_SYM = 
prove (`!a b. reflect_across(a,b) = reflect_across(b,a)`,
REPEAT GEN_TAC THEN ASM_CASES_TAC `a:complex = b` THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[FUN_EQ_THM; reflect_across; reflect2d; o_THM] THEN REWRITE_TAC[ROTATE2D_COMPLEX; CNJ_CEXP; CNJ_MUL; CNJ_CX; CNJ_II] THEN REWRITE_TAC[CX_NEG; COMPLEX_RING `--ii * --z = ii * z`] THEN SUBGOAL_THEN `cexp(ii * Cx(Arg(b - a))) = (b - a) / Cx(norm(b - a)) /\ cexp(ii * Cx(Arg(a - b))) = (a - b) / Cx(norm(a - b))` (CONJUNCTS_THEN SUBST1_TAC) THENL [CONJ_TAC THEN MATCH_MP_TAC(COMPLEX_FIELD `~(a = Cx(&0)) /\ a * b = c ==> b = c / a`) THEN ASM_REWRITE_TAC[GSYM ARG; CX_INJ; NORM_EQ_0; VECTOR_SUB_EQ]; REWRITE_TAC[COMPLEX_RING `a * a * cnj b = a pow 2 * cnj b`] THEN SUBST1_TAC(ISPECL [`a:complex`; `b:complex`] NORM_SUB) THEN X_GEN_TAC `z:complex` THEN REWRITE_TAC[complex_div] THEN MATCH_MP_TAC(COMPLEX_RING `b - a = ((b - a) * n) pow 2 * (cnj za - cnj zb) ==> a + ((b - a) * n) pow 2 * cnj za = b + ((a - b) * n) pow 2 * cnj zb`) THEN REWRITE_TAC[CNJ_SUB; COMPLEX_RING `(z - a) - (z - b):complex = b - a`] THEN MATCH_MP_TAC(COMPLEX_FIELD `(b' - a') * (b - a) = n pow 2 /\ ~(n = Cx(&0)) ==> b - a = ((b - a) * inv n) pow 2 * (b' - a')`) THEN REWRITE_TAC[GSYM CNJ_SUB; COMPLEX_MUL_CNJ; CX_INJ] THEN ASM_REWRITE_TAC[COMPLEX_NORM_ZERO; COMPLEX_SUB_0]]);;
(* ------------------------------------------------------------------------- *) (* Some additional lemmas. *) (* ------------------------------------------------------------------------- *)
let ITER_ROTATE_ABOUT = 
prove (`!n a t. ITER n (rotate_about a t) = rotate_about a (&n * t)`,
REWRITE_TAC[FUN_EQ_THM; rotate_about] THEN REWRITE_TAC[VECTOR_ARITH `a + b:real^N = a + c <=> b = c`] THEN INDUCT_TAC THEN REWRITE_TAC[ITER_ALT; REAL_MUL_LZERO; ROTATE2D_ZERO] THEN REWRITE_TAC[VECTOR_ARITH `a + x - a:real^N = x`; GSYM REAL_OF_NUM_SUC] THEN ASM_REWRITE_TAC[REAL_ADD_RDISTRIB; ROTATE2D_ADD] THEN REPEAT GEN_TAC THEN AP_TERM_TAC THEN AP_TERM_TAC THEN REWRITE_TAC[rotate_about; REAL_MUL_LID] THEN VECTOR_ARITH_TAC);;
let REAL_LE_IM_DIV_CYCLIC = 
prove (`!a b c. &0 <= Im ((c - a) / (b - a)) <=> &0 <= Im((a - b) / (c - b))`,
REWRITE_TAC[IM_COMPLEX_DIV_GE_0] THEN REWRITE_TAC[complex_mul; IM; IM_SUB; RE_SUB; IM_CNJ; CNJ_SUB; RE_CNJ] THEN REAL_ARITH_TAC);;
let ROTATE_ABOUT_INVERT = 
prove (`rotate_about a t w = z <=> w = rotate_about a (--t) z`,
MATCH_MP_TAC(MESON[] `(!x. f(g x) = x) /\ (!y. g(f y) = y) ==> (f x = y <=> x = g y)`) THEN REWRITE_TAC[rotate_about; VECTOR_ADD_SUB; GSYM ROTATE2D_ADD] THEN REWRITE_TAC[REAL_ADD_LINV; REAL_ADD_RINV] THEN REWRITE_TAC[ROTATE2D_ZERO] THEN VECTOR_ARITH_TAC);;
let ROTATE_EQ_REFLECT_LEMMA = 
prove (`!a b z t. ~(b = a) /\ &2 * Arg((b - a) / (z - a)) = t ==> rotate_about a t z = reflect_across (a,b) z`,
REPEAT STRIP_TAC THEN REWRITE_TAC[rotate_about; reflect_across] THEN AP_TERM_TAC THEN REWRITE_TAC[ROTATE2D_COMPLEX; reflect2d; o_THM] THEN REWRITE_TAC[CNJ_MUL; COMPLEX_MUL_ASSOC; CNJ_CEXP; CNJ_II] THEN REWRITE_TAC[CNJ_CX; COMPLEX_MUL_LNEG; COMPLEX_MUL_RNEG; COMPLEX_NEG_NEG; GSYM CEXP_ADD; CX_NEG] THEN REWRITE_TAC[COMPLEX_RING `ii * a + ii * a = ii * Cx(&2) * a`] THEN ASM_CASES_TAC `z:complex = a` THEN ASM_REWRITE_TAC[CNJ_CX; COMPLEX_MUL_RZERO; COMPLEX_SUB_REFL] THEN FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP (COMPLEX_RING `~(z = a) ==> c * (z - a) pow 2 = b * cnj (z - a) * (z - a) ==> c * (z - a) = b * cnj(z - a)`)) THEN REWRITE_TAC[COMPLEX_MUL_CNJ] THEN GEN_REWRITE_TAC (LAND_CONV o RAND_CONV o LAND_CONV) [ARG] THEN MATCH_MP_TAC(COMPLEX_RING `(e1:complex) * e2 pow 2 = e3 ==> e1 * (n * e2) pow 2 = e3 * n pow 2`) THEN REWRITE_TAC[GSYM CEXP_ADD; GSYM CEXP_N; CEXP_EQ] THEN REWRITE_TAC[COMPLEX_RING `ii * t + Cx(&2) * ii * z = ii * u + v * ii <=> t + Cx(&2) * z - u = v`] THEN REWRITE_TAC[GSYM CX_MUL; GSYM CX_SUB; GSYM CX_ADD; CX_INJ] THEN EXPAND_TAC "t" THEN REWRITE_TAC[GSYM REAL_SUB_LDISTRIB; GSYM REAL_ADD_LDISTRIB] THEN REWRITE_TAC[REAL_ARITH `&2 * a = &2 * b <=> a = b`] THEN ONCE_REWRITE_TAC[REAL_ARITH `a + (b - c):real = a - (c - b)`] THEN ASM_SIMP_TAC[REAL_SUB_ARG; COMPLEX_SUB_0] THEN COND_CASES_TAC THENL [EXISTS_TAC `&0`; EXISTS_TAC `&2`] THEN SIMP_TAC[INTEGER_CLOSED] THEN REAL_ARITH_TAC);;
let ROTATE_EQ_REFLECT_PI_LEMMA = 
prove (`!a b z t. ~(b = a) /\ &2 * Arg((b - a) / (z - a)) = &4 * pi + t ==> rotate_about a t z = reflect_across (a,b) z`,
REWRITE_TAC[REAL_ARITH `a = &4 * pi + t <=> t = a + --(&4 * pi)`] THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC `rotate_about a (&2 * Arg((b - a) / (z - a))) z` THEN CONJ_TAC THENL [ALL_TAC; MATCH_MP_TAC ROTATE_EQ_REFLECT_LEMMA THEN ASM_REWRITE_TAC[]] THEN REWRITE_TAC[rotate_about; ROTATE2D_ADD] THEN AP_TERM_TAC THEN AP_TERM_TAC THEN REWRITE_TAC[ROTATE2D_COMPLEX] THEN REWRITE_TAC[EULER; RE_MUL_II; IM_MUL_II; RE_CX; IM_CX; COS_NEG; SIN_NEG] THEN REWRITE_TAC[SIN_NPI; COS_NPI; REAL_EXP_NEG; REAL_EXP_0; CX_NEG] THEN REWRITE_TAC[COMPLEX_NEG_0; COMPLEX_MUL_RZERO; COMPLEX_ADD_RID] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN REWRITE_TAC[COMPLEX_MUL_LID]);;
(* ------------------------------------------------------------------------- *) (* Algebraic characterization of equilateral triangle. *) (* ------------------------------------------------------------------------- *)
let EQUILATERAL_TRIANGLE_ALGEBRAIC = 
prove (`!A B C j. j pow 3 = Cx(&1) /\ ~(j = Cx(&1)) /\ A + j * B + j pow 2 * C = Cx(&0) ==> dist(A,B) = dist(B,C) /\ dist(C,A) = dist(B,C)`,
REPEAT GEN_TAC THEN STRIP_TAC THEN REWRITE_TAC[dist] THEN SUBGOAL_THEN `C - A:complex = j * (B - C) /\ A - B = j pow 2 * (B - C)` (CONJUNCTS_THEN SUBST1_TAC) THENL [REPEAT(POP_ASSUM MP_TAC) THEN CONV_TAC COMPLEX_RING; ALL_TAC] THEN SUBGOAL_THEN `norm(j pow 3) = &1` MP_TAC THENL [ASM_REWRITE_TAC[COMPLEX_NORM_CX; REAL_ABS_NUM]; REWRITE_TAC[COMPLEX_NORM_POW; REAL_POW_EQ_1; ARITH; REAL_ABS_NORM] THEN DISCH_THEN(ASSUME_TAC o CONJUNCT1)] THEN ASM_REWRITE_TAC[COMPLEX_NORM_MUL; COMPLEX_NORM_POW] THEN REAL_ARITH_TAC);;
(* ------------------------------------------------------------------------- *) (* The main algebraic lemma. *) (* ------------------------------------------------------------------------- *)
let AFFINE_GROUP_ITER_3 = 
prove (`ITER 3 (\z. a * z + b) = (\z. a pow 3 * z + b * (Cx(&1) + a + a pow 2))`,
REWRITE_TAC[TOP_DEPTH_CONV num_CONV `3`] THEN REWRITE_TAC[ITER; FUN_EQ_THM] THEN CONV_TAC NUM_REDUCE_CONV THEN CONV_TAC COMPLEX_RING);;
let AFFINE_GROUP_COMPOSE = 
prove (`(\z. a1 * z + b1) o (\z. a2 * z + b2) = (\z. (a1 * a2) * z + (b1 + a1 * b2))`,
REWRITE_TAC[o_THM; FUN_EQ_THM] THEN CONV_TAC COMPLEX_RING);;
let AFFINE_GROUP_I = 
prove (`I = (\z. Cx(&1) * z + Cx(&0))`,
REWRITE_TAC[I_THM; FUN_EQ_THM] THEN CONV_TAC COMPLEX_RING);;
let AFFINE_GROUP_EQ = 
prove (`!a b a' b. (\z. a * z + b) = (\z. a' * z + b') <=> a = a' /\ b = b'`,
REPEAT GEN_TAC THEN EQ_TAC THEN SIMP_TAC[FUN_EQ_THM] THEN DISCH_TAC THEN FIRST_ASSUM(MP_TAC o SPEC `Cx(&0)`) THEN FIRST_X_ASSUM(MP_TAC o SPEC `Cx(&1)`) THEN CONV_TAC COMPLEX_RING);;
let AFFINE_GROUP_ROTATE_ABOUT = 
prove (`!a t. rotate_about a t = (\z. cexp(ii * Cx(t)) * z + (Cx(&1) - cexp(ii * Cx(t))) * a)`,
REWRITE_TAC[rotate_about; FUN_EQ_THM; ROTATE2D_COMPLEX] THEN CONV_TAC COMPLEX_RING);;
let ALGEBRAIC_LEMMA = 
prove (`!a1 a2 a3 b1 b2 b3 A B C. (\z. a3 * z + b3) ((\z. a1 * z + b1) B) = B /\ (\z. a1 * z + b1) ((\z. a2 * z + b2) C) = C /\ (\z. a2 * z + b2) ((\z. a3 * z + b3) A) = A /\ ITER 3 (\z. a1 * z + b1) o ITER 3 (\z. a2 * z + b2) o ITER 3 (\z. a3 * z + b3) = I /\ ~(a1 * a2 * a3 = Cx(&1)) /\ ~(a1 * a2 = Cx(&1)) /\ ~(a2 * a3 = Cx(&1)) /\ ~(a3 * a1 = Cx(&1)) ==> (a1 * a2 * a3) pow 3 = Cx (&1) /\ ~(a1 * a2 * a3 = Cx (&1)) /\ C + (a1 * a2 * a3) * A + (a1 * a2 * a3) pow 2 * B = Cx(&0)`,
REWRITE_TAC[AFFINE_GROUP_ITER_3; AFFINE_GROUP_COMPOSE; AFFINE_GROUP_I; AFFINE_GROUP_EQ] THEN REPEAT GEN_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN CONJ_TAC THENL [REPEAT(POP_ASSUM MP_TAC) THEN CONV_TAC COMPLEX_RING; ALL_TAC] THEN SUBGOAL_THEN `(a1 * a2 * a3) * a1 pow 2 * a2 * (a1 - a1 * a2 * a3) * (a2 - a1 * a2 * a3) * (a3 - a1 * a2 * a3) * (C + (a1 * a2 * a3) * A + (a1 * a2 * a3) pow 2 * B) = Cx(&0)` MP_TAC THENL [REPEAT(FIRST_X_ASSUM(MP_TAC o MATCH_MP (COMPLEX_FIELD `a3 * (a1 * B + b1) + b3 = B ==> ~(a1 * a3 = Cx(&1)) ==> B = (a3 * b1 + b3) / (Cx(&1) - a1 * a3)`))) THEN REPEAT(ANTS_TAC THENL [ASM_MESON_TAC[COMPLEX_MUL_SYM]; DISCH_THEN SUBST1_TAC]) THEN FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (COMPLEX_RING `s = Cx(&0) ==> s + t = Cx(&0) ==> t = Cx(&0)`)); REWRITE_TAC[COMPLEX_ENTIRE]] THEN REPEAT(POP_ASSUM MP_TAC) THEN CONV_TAC COMPLEX_FIELD);;
(* ------------------------------------------------------------------------- *) (* A tactic to avoid some duplication over cyclic permutations. *) (* ------------------------------------------------------------------------- *) let CYCLIC_PERM_SUBGOAL_THEN = let lemma = MESON[] `(!A B C P Q R a b c g1 g2 g3. 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) ==> (!A B C P Q R a b c g1 g2 g3. Ant A B C P Q R a b c g1 g2 g3 ==> Ant B C A Q R P b c a g2 g3 g1) ==> (!A B C P Q R a b c g1 g2 g3. 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 /\ Cns B C A Q R P b c a g2 g3 g1 /\ Cns C A B R P Q c a b g3 g1 g2)` and vars = [`A:complex`; `B:complex`; `C:complex`; `P:complex`; `Q:complex`; `R:complex`; `a:real`; `b:real`; `c:real`; `g1:complex->complex`; `g2:complex->complex`; `g3:complex->complex`] in fun t ttac (asl,w) -> let asm = list_mk_conj (map (concl o snd) (rev asl)) in let gnw = list_mk_forall(vars,mk_imp(asm,t)) in let th1 = MATCH_MP lemma (ASSUME gnw) in let tm1 = fst(dest_imp(concl th1)) in let th2 = REWRITE_CONV[INSERT_AC; CONJ_ACI; ANGLE_SYM; EQ_SYM_EQ] tm1 in let th3 = DISCH_ALL(MP th1 (EQT_ELIM th2)) in (MP_TAC th3 THEN ANTS_TAC THENL [POP_ASSUM_LIST(K ALL_TAC) THEN REPEAT GEN_TAC THEN STRIP_TAC; DISCH_THEN(MP_TAC o SPEC_ALL) THEN ANTS_TAC THENL [REPEAT CONJ_TAC THEN FIRST_ASSUM ACCEPT_TAC; DISCH_THEN(CONJUNCTS_THEN2 ttac MP_TAC) THEN DISCH_THEN(CONJUNCTS_THEN ttac)]]) (asl,w);; (* ------------------------------------------------------------------------- *) (* Morley's theorem a la Connes. *) (* ------------------------------------------------------------------------- *)
let MORLEY = 
prove (`!A B C:real^2 P Q R. ~collinear{A,B,C} /\ {P,Q,R} SUBSET convex hull {A,B,C} /\ angle(A,B,R) = angle(A,B,C) / &3 /\ angle(B,A,R) = angle(B,A,C) / &3 /\ angle(B,C,P) = angle(B,C,A) / &3 /\ angle(C,B,P) = angle(C,B,A) / &3 /\ angle(C,A,Q) = angle(C,A,B) / &3 /\ angle(A,C,Q) = angle(A,C,B) / &3 ==> dist(R,P) = dist(P,Q) /\ dist(Q,R) = dist(P,Q)`,
MATCH_MP_TAC(MESON[] `(!A B C. &0 <= Im((C - A) / (B - A)) \/ &0 <= Im((B - A) / (C - A))) /\ (!A B C. Property A B C ==> Property A C B) /\ (!A B C. &0 <= Im((C - A) / (B - A)) ==> Property A B C) ==> !A B C. Property A B C`) THEN REPEAT CONJ_TAC THENL [REPEAT GEN_TAC THEN GEN_REWRITE_TAC RAND_CONV [GSYM IM_COMPLEX_INV_LE_0] THEN REWRITE_TAC[COMPLEX_INV_DIV] THEN REAL_ARITH_TAC; REPEAT GEN_TAC THEN DISCH_TAC THEN MAP_EVERY X_GEN_TAC [`P:real^2`; `Q:real^2`; `R:real^2`] THEN REWRITE_TAC[ANGLE_SYM; DIST_SYM; INSERT_AC] THEN FIRST_X_ASSUM(MP_TAC o SPECL [`P:real^2`; `R:real^2`; `Q:real^2`]) THEN REWRITE_TAC[ANGLE_SYM; DIST_SYM; INSERT_AC] THEN MESON_TAC[]; ALL_TAC] THEN REPEAT GEN_TAC THEN DISCH_TAC THEN REPEAT GEN_TAC THEN MAP_EVERY (fun t -> ASM_CASES_TAC t THENL [ASM_REWRITE_TAC[COLLINEAR_2; INSERT_AC]; ALL_TAC]) [`A:real^2 = B`; `A:real^2 = C`; `B:real^2 = C`] THEN STRIP_TAC THEN FIRST_ASSUM(fun th -> let th' = GEN_REWRITE_RULE I [REAL_LE_IM_DIV_CYCLIC] th in let th'' = GEN_REWRITE_RULE I [REAL_LE_IM_DIV_CYCLIC] th' in ASSUME_TAC th' THEN ASSUME_TAC th'') THEN ABBREV_TAC `a = angle(C:real^2,A,B) / &3` THEN ABBREV_TAC `b = angle(A:real^2,B,C) / &3` THEN ABBREV_TAC `c = angle(B:real^2,C,A) / &3` THEN ABBREV_TAC `g1 = rotate_about A (&2 * a)` THEN ABBREV_TAC `g2 = rotate_about B (&2 * b)` THEN ABBREV_TAC `g3 = rotate_about C (&2 * c)` THEN CYCLIC_PERM_SUBGOAL_THEN `ITER 3 g1 o ITER 3 g2 o ITER 3 g3 = (I:real^2->real^2)` ASSUME_TAC THENL [MAP_EVERY EXPAND_TAC ["g1";
"g2"; "g3"] THEN REWRITE_TAC[ITER_ROTATE_ABOUT] THEN MAP_EVERY EXPAND_TAC ["a"; "b"; "c"] THEN REWRITE_TAC[REAL_ARITH `&3 * &2 * a / &3 = &2 * a`] THEN ASM_SIMP_TAC[GSYM REFLECT_ACROSS_COMPOSE_ANGLE] THEN REWRITE_TAC[FUN_EQ_THM; o_THM; I_THM; REFLECT_ACROSS_SYM] THEN ASM_SIMP_TAC[REWRITE_RULE[FUN_EQ_THM; I_THM; o_THM] REFLECT_ACROSS_COMPOSE_INVOLUTION]; ALL_TAC] THEN CYCLIC_PERM_SUBGOAL_THEN `&0 <= Im((P - B) / (C - B))` STRIP_ASSUME_TAC THENL [FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [INSERT_SUBSET]) THEN REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET] THEN REPEAT(MATCH_MP_TAC MONO_AND THEN CONJ_TAC) THEN REWRITE_TAC[CONVEX_HULL_3; IN_ELIM_THM] THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN SIMP_TAC[VECTOR_ARITH `(u % A + v % B + w % C) - B:real^N = u % (A - B) + w % (C - B) + ((u + v + w) - &1) % B`] THEN ASM_REWRITE_TAC[REAL_SUB_REFL; VECTOR_MUL_LZERO; VECTOR_ADD_RID] THEN REWRITE_TAC[complex_div; COMPLEX_ADD_RDISTRIB; IM_ADD; COMPLEX_CMUL] THEN REWRITE_TAC[GSYM COMPLEX_MUL_ASSOC] THEN REWRITE_TAC[GSYM complex_div] THEN ASM_SIMP_TAC[IM_MUL_CX; COMPLEX_DIV_REFL; COMPLEX_SUB_0; IM_CX] THEN SIMP_TAC[REAL_MUL_RZERO; REAL_ADD_RID] THEN MATCH_MP_TAC REAL_LE_MUL THEN ASM_REAL_ARITH_TAC; ALL_TAC] THEN CYCLIC_PERM_SUBGOAL_THEN `&0 <= Im((B - C) / (P - C))` STRIP_ASSUME_TAC THENL [REWRITE_TAC[GSYM IM_COMPLEX_INV_LE_0; COMPLEX_INV_DIV] THEN FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [INSERT_SUBSET]) THEN REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET] THEN REPEAT(MATCH_MP_TAC MONO_AND THEN CONJ_TAC) THEN REWRITE_TAC[CONVEX_HULL_3; IN_ELIM_THM] THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN SIMP_TAC[VECTOR_ARITH `(u % A + v % B + w % C) - C:real^N = v % (B - C) + u % (A - C) + ((u + v + w) - &1) % C`] THEN ASM_REWRITE_TAC[REAL_SUB_REFL; VECTOR_MUL_LZERO; VECTOR_ADD_RID] THEN REWRITE_TAC[complex_div; COMPLEX_ADD_RDISTRIB; IM_ADD; COMPLEX_CMUL] THEN REWRITE_TAC[GSYM COMPLEX_MUL_ASSOC] THEN REWRITE_TAC[GSYM complex_div] THEN ASM_SIMP_TAC[IM_MUL_CX; COMPLEX_DIV_REFL; COMPLEX_SUB_0; IM_CX] THEN SIMP_TAC[REAL_MUL_RZERO; REAL_ADD_LID] THEN MATCH_MP_TAC(REAL_ARITH `&0 <= u * --a ==> u * a <= &0`) THEN MATCH_MP_TAC REAL_LE_MUL THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[REAL_ARITH `&0 <= --x <=> x <= &0`] THEN ASM_REWRITE_TAC[GSYM IM_COMPLEX_INV_GE_0; COMPLEX_INV_DIV]; ALL_TAC] THEN CYCLIC_PERM_SUBGOAL_THEN `~(P:real^2 = B) /\ ~(P = C)` STRIP_ASSUME_TAC THENL [SUBGOAL_THEN `!x y z. ~(angle(x:real^2,y,z) / &3 = pi / &2)` (fun th -> ASM_MESON_TAC[th; ANGLE_REFL]) THEN REPEAT GEN_TAC THEN MATCH_MP_TAC(REAL_ARITH `a <= pi /\ &0 < pi ==> ~(a / &3 = pi / &2)`) THEN REWRITE_TAC[ANGLE_RANGE; PI_POS]; ALL_TAC] THEN CYCLIC_PERM_SUBGOAL_THEN `(g3:complex->complex)(g1(Q)) = Q` ASSUME_TAC THENL [MAP_EVERY EXPAND_TAC ["g1"; "g3"] THEN ONCE_REWRITE_TAC[ROTATE_ABOUT_INVERT] THEN MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC `reflect_across(A,C) Q` THEN CONJ_TAC THENL [MATCH_MP_TAC ROTATE_EQ_REFLECT_LEMMA THEN ASM_REWRITE_TAC[] THEN AP_TERM_TAC THEN GEN_REWRITE_TAC RAND_CONV [SYM(ASSUME `angle(C:real^2,A,Q) = a`)] THEN REWRITE_TAC[angle] THEN ONCE_REWRITE_TAC[VECTOR_ANGLE_SYM] THEN ASM_SIMP_TAC[VECTOR_ANGLE_ARG; COMPLEX_SUB_0]; ALL_TAC] THEN CONV_TAC SYM_CONV THEN ONCE_REWRITE_TAC[REFLECT_ACROSS_SYM] THEN MATCH_MP_TAC ROTATE_EQ_REFLECT_PI_LEMMA THEN ASM_REWRITE_TAC[GSYM REAL_MUL_RNEG] THEN REWRITE_TAC[REAL_ARITH `&2 * a = &4 * pi + &2 * --c <=> a = &2 * pi - c`] THEN GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [SYM(ASSUME `angle(B:real^2,C,A) / &3 = c`)] THEN ONCE_REWRITE_TAC[ANGLE_SYM] THEN FIRST_ASSUM(fun th -> GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [SYM th]) THEN REWRITE_TAC[angle] THEN ASM_SIMP_TAC[VECTOR_ANGLE_ARG; COMPLEX_SUB_0] THEN GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [GSYM COMPLEX_INV_DIV] THEN MATCH_MP_TAC ARG_INV THEN REWRITE_TAC[GSYM ARG_EQ_0] THEN DISCH_TAC THEN SUBGOAL_THEN `angle(A:real^2,C,Q) = &0` MP_TAC THENL [REWRITE_TAC[angle] THEN ASM_SIMP_TAC[VECTOR_ANGLE_ARG; COMPLEX_SUB_0]; ASM_REWRITE_TAC[REAL_ARITH `a / &3 = &0 <=> a = &0`]] THEN ASM_MESON_TAC[COLLINEAR_ANGLE; ANGLE_SYM; INSERT_AC]; ALL_TAC] THEN REPEAT(FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE LAND_CONV [AFFINE_GROUP_ROTATE_ABOUT])) THEN CYCLIC_PERM_SUBGOAL_THEN `~(cexp(ii * Cx(&2 * a)) * cexp(ii * Cx(&2 * b)) = Cx(&1)) /\ ~(cexp(ii * Cx(&2 * a)) * cexp(ii * Cx(&2 * b)) * cexp(ii * Cx(&2 * c)) = Cx(&1))` STRIP_ASSUME_TAC THENL [REWRITE_TAC[GSYM CEXP_ADD; GSYM COMPLEX_ADD_LDISTRIB; GSYM CX_ADD] THEN MP_TAC(REAL_ARITH `&0 <= a /\ &0 <= b /\ &0 <= c /\ &0 < pi /\ &3 * a + &3 * b + &3 * c = pi /\ ~(&3 * c = pi) ==> (&0 < &2 * a + &2 * b /\ &2 * a + &2 * b < &2 * pi) /\ (&0 < &2 * a + &2 * b + &2 * c /\ &2 * a + &2 * b + &2 * c < &2 * pi)`) THEN ANTS_TAC THENL [MAP_EVERY EXPAND_TAC ["a"; "b"; "c"] THEN REWRITE_TAC[REAL_ARITH `&3 * x / &3 = x`; PI_POS] THEN SIMP_TAC[ANGLE_RANGE; REAL_LE_DIV; REAL_POS] THEN CONJ_TAC THENL [ASM_MESON_TAC[TRIANGLE_ANGLE_SUM; ADD_AC; ANGLE_SYM]; ASM_MESON_TAC[COLLINEAR_ANGLE; ANGLE_SYM; INSERT_AC]]; MATCH_MP_TAC MONO_AND THEN CONJ_TAC THEN REWRITE_TAC[CEXP_II_NE_1; GSYM CX_ADD]]; ALL_TAC] THEN MAP_EVERY ABBREV_TAC [`a1 = cexp(ii * Cx(&2 * a))`; `a2 = cexp(ii * Cx(&2 * b))`; `a3 = cexp(ii * Cx(&2 * c))`; `b1 = (Cx (&1) - a1) * A`; `b2 = (Cx (&1) - a2) * B`; `b3 = (Cx (&1) - a3) * C`] THEN REPEAT DISCH_TAC THEN MATCH_MP_TAC EQUILATERAL_TRIANGLE_ALGEBRAIC THEN EXISTS_TAC `a1 * a2 * a3:complex` THEN MATCH_MP_TAC ALGEBRAIC_LEMMA THEN MAP_EVERY EXISTS_TAC [`b1:complex`; `b2:complex`; `b3:complex`] THEN PURE_ASM_REWRITE_TAC[] THEN REWRITE_TAC[]);;