1 (* ========================================================================= *)
2 (* Formalization of Alain Connes's paper "A new proof of Morley's theorem". *)
3 (* ========================================================================= *)
5 needs "Library/iter.ml";;
6 needs "Multivariate/geom.ml";;
8 (* ------------------------------------------------------------------------- *)
9 (* Reflection about the line[0,e^{i t}] *)
10 (* ------------------------------------------------------------------------- *)
12 let reflect2d = new_definition
13 `reflect2d t = rotate2d t o cnj o rotate2d(--t)`;;
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);;
24 (* ------------------------------------------------------------------------- *)
25 (* Rotation about point "a" by angle "t". *)
26 (* ------------------------------------------------------------------------- *)
28 let rotate_about = new_definition
29 `rotate_about a t x = a + rotate2d t (x - a)`;;
31 (* ------------------------------------------------------------------------- *)
32 (* Reflection across line (a,b). *)
33 (* ------------------------------------------------------------------------- *)
35 let reflect_across = new_definition
36 `reflect_across (a,b) x = a + reflect2d (Arg(b - a)) (x - a)`;;
38 let REFLECT_ACROSS_COMPOSE = prove
41 ==> reflect_across(a,b) o reflect_across(a,c) =
42 rotate_about a (&2 * Arg((b - a) / (c - a)))`,
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]);;
51 let REFLECT_ACROSS_COMPOSE_ANGLE = prove
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]);;
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);;
68 let REFLECT_ACROSS_SYM = prove
69 (`!a b. reflect_across(a,b) = reflect_across(b,a)`,
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]]);;
95 (* ------------------------------------------------------------------------- *)
96 (* Some additional lemmas. *)
97 (* ------------------------------------------------------------------------- *)
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);;
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
115 let ROTATE_ABOUT_INVERT = prove
116 (`rotate_about a t w = z <=> w = rotate_about a (--t) z`,
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);;
124 let ROTATE_EQ_REFLECT_LEMMA = prove
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
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
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);;
157 let ROTATE_EQ_REFLECT_PI_LEMMA = prove
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
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]);;
175 (* ------------------------------------------------------------------------- *)
176 (* Algebraic characterization of equilateral triangle. *)
177 (* ------------------------------------------------------------------------- *)
179 let EQUILATERAL_TRIANGLE_ALGEBRAIC = prove
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;
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
196 (* ------------------------------------------------------------------------- *)
197 (* The main algebraic lemma. *)
198 (* ------------------------------------------------------------------------- *)
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);;
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);;
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);;
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);;
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);;
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)) /\
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
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)`
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);;
262 (* ------------------------------------------------------------------------- *)
263 (* A tactic to avoid some duplication over cyclic permutations. *)
264 (* ------------------------------------------------------------------------- *)
266 let CYCLIC_PERM_SUBGOAL_THEN =
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)`
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);;
297 (* ------------------------------------------------------------------------- *)
298 (* Morley's theorem a la Connes. *)
299 (* ------------------------------------------------------------------------- *)
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)`,
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
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[];
327 REPEAT GEN_TAC THEN DISCH_TAC THEN REPEAT GEN_TAC THEN
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
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)`
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];
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
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];
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
396 MATCH_MP_TAC(REAL_ARITH
397 `a <= pi /\ &0 < pi ==> ~(a / &3 = pi / &2)`) THEN
398 REWRITE_TAC[ANGLE_RANGE; PI_POS];
400 CYCLIC_PERM_SUBGOAL_THEN
401 `(g3:complex->complex)(g1(Q)) = Q`
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
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];
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
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];
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
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
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]];
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[]);;