1 (* ========================================================================= *)
2 (* (c) Copyright, Bill Richter 2013 *)
3 (* Distributed under the same license as HOL Light *)
5 (* Proof of the Bug Puzzle conjecture of the HOL Light tutorial: Any two *)
6 (* triples of points in the plane with the same oriented area can be *)
7 (* connected in 5 moves or less (FivemovesOrLess). Much of the code is *)
8 (* due to John Harrison: a proof (NOTENOUGH_4) showing this is the best *)
9 (* possible result; an early version of Noncollinear_2Span; the *)
10 (* definition of move, which defines a closed subset *)
11 (* {(A,B,C,A',B',C') | move (A,B,C) (A',B',C')} of R^6 x R^6, *)
12 (* i.e. the zero set of a continuous function; FivemovesOrLess_STRONG, *)
13 (* which handles the degenerate case (collinear or non-distinct triples), *)
14 (* giving a satisfying answer using this "closed" definition of move. *)
16 (* The mathematical proofs are essentially due to Tom Hales. *)
17 (* ========================================================================= *)
19 needs "Multivariate/determinants.ml";;
20 needs "RichterHilbertAxiomGeometry/readable.ml";;
22 new_type_abbrev("triple",`:real^2#real^2#real^2`);;
25 SIMP_TAC[CART_EQ; LAMBDA_BETA; FORALL_2; SUM_2; DIMINDEX_2; VECTOR_2;
26 vector_add; vec; dot; orthogonal; basis;
27 vector_neg; vector_sub; vector_mul; ARITH] THEN
30 let oriented_area = new_definition
31 `oriented_area (a:real^2,b:real^2,c:real^2) =
32 ((b$1 - a$1) * (c$2 - a$2) - (c$1 - a$1) * (b$2 - a$2)) / &2`;;
34 let move = NewDefinition `;
35 ∀A B C A' B' C':real^2. move (A,B,C) (A',B',C') ⇔
36 (B = B' ∧ C = C' ∧ collinear {vec 0,C - B,A' - A} ∨
37 A = A' ∧ C = C' ∧ collinear {vec 0,C - A,B' - B} ∨
38 A = A' ∧ B = B' ∧ collinear {vec 0,B - A,C' - C})`;;
40 let reachable = NewDefinition `;
42 reachable p p' ⇔ ∃n. ∃s. s 0 = p ∧ s n = p' ∧
43 (∀m. 0 <= m ∧ m < n ⇒ move (s m) (s (SUC m)))`;;
45 let reachableN = NewDefinition `;
47 reachableN p p' n ⇔ ∃s. s 0 = p ∧ s n = p' ∧
48 (∀m. 0 <= m ∧ m < n ⇒ move (s m) (s (SUC m)))`;;
50 let move2Cond = NewDefinition `;
51 ∀ A B A' B':real^2. move2Cond A B A' B' ⇔
52 ¬collinear {B,A,A'} ∧ ¬collinear {A',B,B'} ∨
53 ¬collinear {A,B,B'} ∧ ¬collinear {B',A,A'}`;;
56 let oriented_areaSymmetry = theorem `;
57 oriented_area (A,B,C) = oriented_area(A',B',C') ⇒
58 oriented_area (B,C,A) = oriented_area (B',C',A') ∧
59 oriented_area (C,A,B) = oriented_area (C',A',B') ∧
60 oriented_area (A,C,B) = oriented_area (A',C',B') ∧
61 oriented_area (B,A,C) = oriented_area (B',A',C') ∧
62 oriented_area (C,B,A) = oriented_area (C',B',A')
64 rewrite oriented_area; VEC2_TAC;
68 let COLLINEAR_3_2Dzero = theorem `;
69 ∀y z:real^2. collinear{vec 0,y,z} ⇔
72 rewrite COLLINEAR_3_2D; VEC2_TAC; qed;
75 let Noncollinear_3ImpliesDistinct = theorem `;
76 ¬collinear {a,b,c} ⇒ ¬(a = b) ∧ ¬(a = c) ∧ ¬(b = c)
77 by fol COLLINEAR_BETWEEN_CASES BETWEEN_REFL`;;
79 let collinearSymmetry = theorem `;
81 ⇒ collinear {A,C,B} ∧ collinear {B,A,C} ∧
82 collinear {B,C,A} ∧ collinear {C,A,B} ∧ collinear {C,B,A}
84 {A,C,B} ⊂ {A,B,C} ∧ {B,A,C} ⊂ {A,B,C} ∧
85 {B,C,A} ⊂ {A,B,C} ∧ {C,A,B} ⊂ {A,B,C} ∧ {C,B,A} ⊂ {A,B,C} [] by set;
86 fol - COLLINEAR_SUBSET;
90 let Noncollinear_2Span = theorem `;
91 ∀u v w:real^2. ¬collinear {vec 0,v,w} ⇒ ∃ s t. s % v + t % w = u
95 ¬(v$1 * w$2 - w$1 * v$2 = &0) [H1'] by fol H1 COLLINEAR_3_2Dzero REAL_SUB_0;
97 M = transp(vector[v;w]):real^2^2 [Mexists] by fol -;
99 (∀ x. (M ** x)$1 = v$1 * x$1 + w$1 * x$2 ∧
100 (M ** x)$2 = v$2 * x$1 + w$2 * x$2) [MatMult] by simplify H1' Mexists matrix_vector_mul DIMINDEX_2 SUM_2
101 TRANSP_COMPONENT VECTOR_2 LAMBDA_BETA ARITH CART_EQ FORALL_2 DET_2;
102 ∀ r n. ¬(r < n) ∧ r <= MIN n n ⇒ r = n [] by arithmetic;
103 consider x such that M ** x = u [xDef] by fol MatMult - DET_EQ_0_RANK RANK_BOUND MATRIX_FULL_LINEAR_EQUATIONS;
106 x$1 * v$1 + x$2 * w$1 = u$1 ∧
107 x$1 * v$2 + x$2 * w$2 = u$2 [xDef] by fol MatMult xDef REAL_MUL_SYM;
108 simplify - CART_EQ LAMBDA_BETA FORALL_2 SUM_2 DIMINDEX_2 VECTOR_2 vector_add vector_mul ARITH;
112 let moveInvariant = theorem `;
113 ∀p p'. move p p' ⇒ oriented_area p = oriented_area p'
115 rewrite FORALL_PAIR_THM move oriented_area COLLINEAR_LEMMA vector_mul; VEC2_TAC;
119 let ReachLemma = theorem `;
120 ∀p p'. reachable p p' ⇔ ∃n. reachableN p p' n
122 rewrite reachable reachableN;
126 let reachableN_CLAUSES = theorem `;
127 ∀ p p'. (reachableN p p' 0 ⇔ p = p') ∧
128 ∀ n. reachableN p p' (SUC n) ⇔ ∃ q. reachableN p q n ∧ move q p'
132 consider s0 such that s0 = λm:num. p:triple [s0exists] by fol;
133 reachableN p p' 0 ⇔ p = p' [0CLAUSE] by fol s0exists LE_0 reachableN LT;
134 ∀ n. reachableN p p' (SUC n) ⇒ ∃ q. reachableN p q n ∧ move q p' [Imp1]
138 s 0 = p ∧ s (SUC n) = p' ∧ ∀m. m < SUC n ⇒ move (s m) (s (SUC m)) [sDef] by fol H1 LE_0 reachableN;
139 consider q such that q = s n [qDef] by fol;
140 fol sDef qDef LE_0 reachableN LT;
142 ∀n. (∃ q. reachableN p q n ∧ move q p') ⇒ reachableN p p' (SUC n) [Imp2]
145 rewrite IMP_CONJ LEFT_IMP_EXISTS_THM;
146 intro_TAC ∀q, nReach, move_qp';
148 s 0 = p ∧ s n = q ∧ ∀m. m < n ⇒ move (s m) (s (SUC m)) [sDef] by fol nReach reachableN LT LE_0;
149 rewrite reachableN LT LE_0;
150 exists_TAC λm. if m < SUC n then s m else p';
151 fol sDef move_qp' LT_0 LT_REFL LT LT_SUC;
153 fol 0CLAUSE Imp1 Imp2;
157 let reachableInvariant = theorem `;
158 ∀p p'. reachable p p' ⇒ oriented_area p = oriented_area p'
161 simplify ReachLemma LEFT_IMP_EXISTS_THM SWAP_FORALL_THM;
162 MATCH_MP_TAC num_INDUCTION;
163 simplify reachableN_CLAUSES;
165 fol nStep moveInvariant;
169 let reachableN_One = theorem `;
170 reachableN P0 P1 1 ⇔ move P0 P1
171 by fol ONE reachableN reachableN_CLAUSES`;;
173 let reachableN_Two = theorem `;
174 reachableN P0 P2 2 ⇔ ∃P1. move P0 P1 ∧ move P1 P2
175 by fol TWO reachableN_One reachableN_CLAUSES`;;
177 let reachableN_Three = theorem `;
178 reachableN P0 P3 3 ⇔ ∃P1 P2. move P0 P1 ∧ move P1 P2 ∧ move P2 P3
179 by fol ARITH_RULE [3 = SUC 2] reachableN_Two reachableN_CLAUSES`;;
181 let reachableN_Four = theorem `;
182 reachableN P0 P4 4 ⇔ ∃P1 P2 P3. move P0 P1 ∧ move P1 P2 ∧
183 move P2 P3 ∧ move P3 P4
184 by fol ARITH_RULE [4 = SUC 3] reachableN_Three reachableN_CLAUSES`;;
186 let reachableN_Five = theorem `;
187 reachableN P0 P5 5 ⇔ ∃P1 P2 P3 P4. move P0 P1 ∧ move P1 P2 ∧
188 move P2 P3 ∧ move P3 P4 ∧ move P4 P5
190 rewrite ARITH_RULE [5 = SUC 4] reachableN_CLAUSES;
195 let moveSymmetry = theorem `;
196 move (A,B,C) (A',B',C') ⇒
197 move (B,C,A) (B',C',A') ∧ move (C,A,B) (C',A',B') ∧
198 move (A,C,B) (A',C',B') ∧ move (B,A,C) (B',A',C') ∧ move (C,B,A) (C',B',A')
201 ∀X Y Z X':real^2. collinear {vec 0, Z - Y, X' - X}
202 ⇒ collinear {vec 0, Y - Z, X' - X} []
203 proof rewrite COLLINEAR_3_2Dzero; VEC2_TAC; qed;
206 ∀X Y Z X':real^2. collinear {vec 0, Z - Y, X' - X}
207 ⇒ collinear {vec 0, Y - Z, X' - X} []
208 proof rewrite COLLINEAR_3_2Dzero; VEC2_TAC; qed;
215 let reachableNSymmetry = theorem `;
216 ∀ n. ∀ A B C A' B' C'. reachableN (A,B,C) (A',B',C') n ⇒
217 reachableN (B,C,A) (B',C',A') n ∧ reachableN (C,A,B) (C',A',B') n ∧
218 reachableN (A,C,B) (A',C',B') n ∧ reachableN (B,A,C) (B',A',C') n ∧
219 reachableN (C,B,A) (C',B',A') n
222 MATCH_MP_TAC num_INDUCTION;
223 rewrite reachableN_CLAUSES; simplify PAIR_EQ;
224 intro_TAC ∀n, nStep, ∀A B C A' B' C';
225 rewrite LEFT_IMP_EXISTS_THM FORALL_PAIR_THM;
228 rewrite RIGHT_AND_EXISTS_THM LEFT_AND_EXISTS_THM;
234 simplify nStep XYZexists moveSymmetry;
238 let ORIENTED_AREA_COLLINEAR_CONG = theorem `;
240 oriented_area (A,B,C) = oriented_area (A',B',C')
241 ⇒ (collinear {A,B,C} ⇔ collinear {A',B',C'})
243 rewrite COLLINEAR_3_2D oriented_area; real_ring;
247 let Basic2move_THM = theorem `;
248 ∀ A B C A'. ¬collinear {A,B,C} ∧ ¬collinear {B,A,A'} ⇒
249 ∃X. move (A,B,C) (A,B,X) ∧ move (A,B,X) (A',B,X)
252 intro_TAC ∀A B C A', H1 H2;
253 ∀r. r % (A - B) = (--r) % (B - A) ∧
254 r % (A - B) = r % (A - B) + &0 % (C - B) [add0vector_mul] by VEC2_TAC;
255 ¬ ∃ r. A' - A = r % (A - B) [H2'] by fol - H2 COLLINEAR_3 COLLINEAR_LEMMA;
256 consider r t such that A' - A = r % (A - B) + t % (C - B) [rExists] by fol - H1 COLLINEAR_3 Noncollinear_2Span;
257 ¬(t = &0) [tNonzero] by fol - add0vector_mul H2';
258 consider s X such that s = r / t ∧ X = C + s % (A - B) [Xexists] by fol rExists;
259 A' - A = (t * s) % (A - B) + t % (C - B) [] by fol - rExists tNonzero REAL_DIV_LMUL;
260 A' - A = t % (X - B) ∧ X - C = (-- s) % (B - A) []
261 proof rewrite - Xexists; VEC2_TAC; qed;
262 collinear {vec 0,B - A,X - C} ∧ collinear {vec 0,X - B,A' - A} [] by fol - COLLINEAR_LEMMA;
267 let FourStepMoveAB = theorem `;
268 ∀A B C A' B'. ¬collinear {A,B,C} ⇒
269 ¬collinear {B,A,A'} ∧ ¬collinear {A',B,B'} ⇒
270 ∃ X Y. move (A,B,C) (A,B,X) ∧ move (A,B,X) (A',B,X) ∧
271 move (A',B,X) (A',B,Y) ∧ move (A',B,Y) (A',B',Y)
274 intro_TAC ∀A B C A' B', H1, H2;
276 move (A,B,C) (A,B,X) ∧ move (A,B,X) (A',B,X) [ABX] by fol H1 H2 Basic2move_THM;
277 ¬collinear {A,B,X} ∧ ¬collinear {A',B,X} [] by fol - H1 moveInvariant ORIENTED_AREA_COLLINEAR_CONG;
278 ¬collinear {B,A',X} [] by fol - collinearSymmetry;
280 move (B,A',X) (B,A',Y) ∧ move (B,A',Y) (B',A',Y) [BA'Y] by fol - H2 Basic2move_THM;
281 move (A',B,X) (A',B,Y) ∧ move (A',B,Y) (A',B',Y) [] by fol - BA'Y moveSymmetry;
286 let FourStepMoveABBAreach = theorem `;
287 ∀A B C A' B'. ¬collinear {A,B,C} ∧ move2Cond A B A' B' ⇒
288 ∃ Y. reachableN (A,B,C) (A',B',Y) 4
291 intro_TAC ∀A B C A' B', H1 H2;
292 case_split Case1 | Case2 by fol - H2 move2Cond;
293 suppose ¬collinear {B,A,A'} ∧ ¬collinear {A',B,B'};
294 fol - H1 FourStepMoveAB reachableN_Four;
296 suppose ¬collinear {A,B,B'} ∧ ¬collinear {B',A,A'};
297 ¬collinear {B,A,C} [] by fol H1 collinearSymmetry;
298 consider X Y such that
299 move (B,A,C) (B,A,X) ∧ move (B,A,X) (B',A,X) ∧
300 move (B',A,X) (B',A,Y) ∧ move (B',A,Y) (B',A',Y) [BAX] by fol Case2 - FourStepMoveAB;
301 fol - moveSymmetry reachableN_Four;
306 let NotMove2ImpliesCollinear = theorem `;
307 ∀A B C A' B' C'. ¬collinear {A,B,C} ∧ ¬collinear {A',B',C'} ∧
308 ¬(A = A') ∧ ¬(B = B') ∧ ¬move2Cond A B A' B' ⇒
309 collinear {A,B,A',B'}
312 intro_TAC ∀A B C A' B' C', H1 H1' H2 H2' H3;
313 ¬(A = B) ∧ ¬(A' = B') [Distinct] by fol H1 H1' Noncollinear_3ImpliesDistinct;
314 {A,B,A',B'} ⊂ {A,A',B,B'} ∧
315 {A,B,A',B'} ⊂ {B,B',A',A} ∧ {A,B,A',B'} ⊂ {A',B',B,A} [set4symmetry] by SET_TAC;
316 case_split Case1 | Case2 | Case3 | Case4 by fol H3 move2Cond;
317 suppose collinear {B,A,A'} ∧ collinear {A,B,B'};
318 fol - Distinct H2 H2' set4symmetry collinearSymmetry COLLINEAR_4_3 COLLINEAR_SUBSET;
320 suppose collinear {B,A,A'} ∧ collinear {B',A,A'};
321 fol - Distinct H2 H2' set4symmetry collinearSymmetry COLLINEAR_4_3 COLLINEAR_SUBSET;
323 suppose collinear {A',B,B'} ∧ collinear {A,B,B'};
324 fol - Distinct H2 H2' set4symmetry collinearSymmetry COLLINEAR_4_3 COLLINEAR_SUBSET;
326 suppose collinear {A',B,B'} ∧ collinear {B',A,A'};
327 fol - Distinct H2 H2' set4symmetry collinearSymmetry COLLINEAR_4_3 COLLINEAR_SUBSET;
332 let NotMove2ImpliesCollinear = theorem `;
333 ∀A B C A' B' C'. ¬collinear {A,B,C} ∧ ¬collinear {A',B',C'} ∧
334 ¬(A = A') ∧ ¬(B = B') ∧ ¬move2Cond A B A' B' ⇒
335 collinear {A,B,A',B'}
338 intro_TAC ∀A B C A' B' C', H1 H1' H2 H2' H3;
339 ¬(A = B) ∧ ¬(A' = B') [Distinct] by fol H1 H1' Noncollinear_3ImpliesDistinct;
340 {A,B,A',B'} ⊂ {A,A',B,B'} ∧
341 {A,B,A',B'} ⊂ {B,B',A',A} ∧ {A,B,A',B'} ⊂ {A',B',B,A} [set4symmetry] by SET_TAC;
342 collinear {B,A,A'} ∧ collinear {A,B,B'} ∨
343 collinear {B,A,A'} ∧ collinear {B',A,A'} ∨
344 collinear {A',B,B'} ∧ collinear {A,B,B'} ∨
345 collinear {A',B,B'} ∧ collinear {B',A,A'} [] by fol H3 move2Cond;
346 fol - Distinct H2 H2' set4symmetry collinearSymmetry COLLINEAR_4_3 COLLINEAR_SUBSET;
350 let DistinctImplies2moveable = theorem `;
351 ∀A B C A' B' C'. ¬collinear {A,B,C} ∧ ¬collinear {A',B',C'} ∧
352 ¬(A = A') ∧ ¬(B = B') ∧ ¬(C = C') ⇒
353 move2Cond A B A' B' ∨ move2Cond B C B' C'
356 intro_TAC ∀A B C A' B' C', H1 H1' H2a H2b H2c;
357 {A,B,B'} ⊂ {A,B,A',B'} ∧ {B,B',C} ⊂ {B,C,B',C'} [3subset4] by SET_TAC;
358 assume ¬move2Cond A B A' B' ∧ ¬move2Cond B C B' C' [Con] by fol;
359 collinear {A,B,A',B'} ∧ collinear {B,C,B',C'} [] by fol - H1 H1' H2a H2b H2c collinearSymmetry NotMove2ImpliesCollinear;
360 collinear {A,B,C} [] by fol - 3subset4 H2a H2b H2c COLLINEAR_SUBSET COLLINEAR_3_TRANS;
365 let SameCdiffAB = theorem `;
366 ∀A B C A' B' C'. ¬collinear {A,B,C} ∧ ¬collinear {A',B',C'} ⇒
367 C = C' ∧ ¬(A = A') ∧ ¬(B = B') ⇒
368 ∃ Y. reachableN (A,B,C) (Y,B',C') 2 ∨ reachableN (A,B,C) (A',B',Y) 4
371 intro_TAC ∀A B C A' B' C', H1, H2;
372 {B,B',A} ⊂ {A,B,A',B'} ∧ {A,B,C} ⊂ {B,B',A,C} [easy_set] by SET_TAC;
373 case_split Ncol | move | col_Nmove by fol;
374 suppose ¬collinear {C,B,B'};
375 consider X such that move (B,C,A) (B,C,X) ∧ move (B,C,X) (B',C',X) [BCX] by fol - easy_set H1 H2 collinearSymmetry Basic2move_THM;
376 fol BCX reachableN_Two reachableNSymmetry;
378 suppose move2Cond A B A' B';
379 fol - H1 FourStepMoveABBAreach;
381 suppose collinear {C,B,B'} ∧ ¬move2Cond A B A' B';
382 collinear {B,B',A} ∧ collinear {B,B',C} [] by fol - H1 H2 easy_set NotMove2ImpliesCollinear COLLINEAR_SUBSET collinearSymmetry;
383 fol - H2 easy_set H1 COLLINEAR_4_3 COLLINEAR_SUBSET;
388 let FourMovesToCorrectTwo = theorem `;
389 ∀A B C A' B' C'. ¬collinear {A,B,C} ∧ ¬collinear {A',B',C'} ⇒
390 ∃ n. n < 5 ∧ ∃ Y. reachableN (A,B,C) (A',B',Y) n ∨
391 reachableN (A,B,C) (A',Y,C') n ∨ reachableN (A,B,C) (Y,B',C') n
394 intro_TAC ∀A B C A' B' C', H1;
396 ¬collinear{B',C',A'} ∧ ¬collinear {C,A,B} ∧ ¬collinear {C',A',B'} [H1'] by fol H1 collinearSymmetry;
397 0 < 5 ∧ 2 < 5 ∧ 3 < 5 ∧ 4 < 5 [easy_arith] by ARITH_TAC;
398 case_split case01 | case2 | case3 by fol;
399 suppose A = A' ∧ B = B' ∧ C = C' ∨
400 A = A' ∧ B = B' ∧ ¬(C = C') ∨ A = A' ∧ ¬(B = B') ∧ C = C' ∨
401 ¬(A = A') ∧ B = B' ∧ C = C';
402 fol - easy_arith reachableN_CLAUSES;
404 suppose A = A' ∧ ¬(B = B') ∧ ¬(C = C') ∨
405 ¬(A = A') ∧ B = B' ∧ ¬(C = C') ∨ ¬(A = A') ∧ ¬(B = B') ∧ C = C';
406 fol - H1 H1' easy_arith SameCdiffAB reachableNSymmetry;
408 suppose ¬(A = A') ∧ ¬(B = B') ∧ ¬(C = C');
410 simplify easy_arith reachableN_CLAUSES;
411 fol - H1 H1' DistinctImplies2moveable FourStepMoveABBAreach
412 reachableNSymmetry reachableN_Four;
417 let CorrectFinalPoint = theorem `;
418 oriented_area (A,B,C) = oriented_area (A,B,C') ⇒
419 move (A,B,C) (A,B,C')
421 rewrite move oriented_area COLLINEAR_3_2Dzero; VEC2_TAC;
425 let FiveMovesOrLess = theorem `;
426 ∀A B C A' B' C'. ¬collinear {A,B,C} ∧
427 oriented_area (A,B,C) = oriented_area (A',B',C') ⇒
428 ∃ n. n <= 5 ∧ reachableN (A,B,C) (A',B',C') n
431 intro_TAC ∀A B C A' B' C', H1 H2;
432 ¬collinear {A',B',C'} [H1'] by fol H1 H2 ORIENTED_AREA_COLLINEAR_CONG;
433 ¬(A = B) ∧ ¬(A = C) ∧ ¬(B = C) ∧
434 ¬(A' = B') ∧ ¬(A' = C') ∧ ¬(B' = C') [Distinct] by fol - H1 Noncollinear_3ImpliesDistinct;
435 consider n Y such that
436 n < 5 ∧ (reachableN (A,B,C) (A',B',Y) n ∨
437 reachableN (A,B,C) (A',Y,C') n ∨ reachableN (A,B,C) (Y,B',C') n) [2Correct] by fol H1 H1' FourMovesToCorrectTwo;
438 case_split A'B'Y | A'YC' | YB'C' by fol 2Correct;
439 suppose reachableN (A,B,C) (A',B',Y) n;
440 oriented_area (A',B',Y) = oriented_area (A',B',C') [] by fol - H2 ReachLemma reachableInvariant;
441 move (A',B',Y) (A',B',C') [] by fol - Distinct CorrectFinalPoint;
442 fol A'B'Y - 2Correct reachableN_CLAUSES LE_SUC_LT;
444 suppose reachableN (A,B,C) (A',Y,C') n;
445 oriented_area (A',C',Y) = oriented_area (A',C',B') [] by fol H2 - ReachLemma reachableInvariant oriented_areaSymmetry;
446 move (A',Y,C') (A',B',C') [] by fol - Distinct CorrectFinalPoint moveSymmetry;
447 fol A'YC' - 2Correct reachableN_CLAUSES LE_SUC_LT;
449 suppose reachableN (A,B,C) (Y,B',C') n;
450 oriented_area (B',C',Y) = oriented_area (B',C',A') [] by fol H2 - ReachLemma reachableInvariant oriented_areaSymmetry;
451 move (Y,B',C') (A',B',C') [] by fol - Distinct CorrectFinalPoint moveSymmetry;
452 fol YB'C' - 2Correct reachableN_CLAUSES LE_SUC_LT;
457 let NOTENOUGH_4 = theorem `;
458 ∃p0 p4. oriented_area p0 = oriented_area p4 ∧ ¬reachableN p0 p4 4
461 consider p0 p4 such that
462 p0:triple = vector [&0;&0],vector [&0;&1],vector [&1;&0] ∧
463 p4:triple = vector [&1;&1],vector [&1;&2],vector [&2;&1] [p04Def] by
465 oriented_area p0 = oriented_area p4 [equal_areas]
466 proof rewrite - oriented_area; VEC2_TAC; qed;
467 ¬reachableN p0 p4 4 []
469 rewrite p04Def reachableN_Four NOT_EXISTS_THM FORALL_PAIR_THM move COLLINEAR_3_2Dzero FORALL_VECTOR_2;
476 let FiveMovesOrLess_STRONG = theorem `;
478 oriented_area (A,B,C) = oriented_area (A',B',C') ⇒
479 ∃n. n <= 5 ∧ reachableN (A,B,C) (A',B',C') n
482 intro_TAC ∀A B C A' B' C', H1;
483 (∀X Y:real^2. collinear {X,Y,Y}) ∧
484 (∀A B A'. move (A,B,B) (A',B,B)) ∧
485 ∀A B C B'. (collinear {A,B,C} ∧ collinear {A,B',C} ⇒
486 move (A,B,C) (A,B',C)) [EZcollinear]
487 proof rewrite move COLLINEAR_3_2D; VEC2_TAC; qed;
488 case_split ABCncol | ABCcol by fol ;
489 suppose ¬collinear {A,B,C};
490 fol - H1 FiveMovesOrLess;
492 suppose collinear {A,B,C};
493 collinear {A',B',C'} [A'B'C'col] by fol - H1 ORIENTED_AREA_COLLINEAR_CONG;
494 consider P1 P2 P3 P4 such that
495 P1 = A,C,C ∧ P2 = B',C,C ∧ P3 = B',B',C ∧ P4 = B',B',C' [P1234exist] by fol;
496 move (A,B,C) P1 ∧ move P1 P2 ∧ move P2 P3 ∧ move P3 P4 ∧
497 move P4 (A',B',C') [] by fol ABCcol A'B'C'col EZcollinear P1234exist
498 collinearSymmetry moveSymmetry;
499 fol - reachableN_Five LE_REFL;