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: *)
6 (* Any two triples with the same oriented area can be connected in *)
7 (* 5 moves or less (FiveMovesOrLess). Also a proof that 4 moves is not *)
8 (* enough, with an explicit counterexample. This result (NOTENOUGH_4) *)
9 (* is due to John Harrison, as is much of the basic vector code, and *)
10 (* the definition of move, which defines a closed subset *)
11 (* {(A,B,C,A',B',C') | move (A,B,C) (A',B',C')} subset R^6 x R^6 *)
12 (* and also a result FiveMovesOrLess_STRONG that handles the degenerate *)
13 (* case (the two triples not required to be non-collinear), which has a *)
14 (* very satisfying answer using this "closed" definition of move. *)
16 (* The mathematical proofs are essentially due to Tom Hales. The *)
17 (* code is all in miz3, and was an attempt to explore Freek Wiedijk's *)
18 (* vision of mixing the procedural and declarative proof styles. *)
19 (* ========================================================================= *)
21 needs "Multivariate/determinants.ml";;
24 loadt "miz3/miz3.ml";;
26 new_type_abbrev("triple",`:real^2#real^2#real^2`);;
28 default_prover := ("ya prover",
29 fun thl -> REWRITE_TAC thl THEN CONV_TAC (HOL_BY thl));;
35 SIMP_TAC[CART_EQ; LAMBDA_BETA; FORALL_2; SUM_2; DIMINDEX_2; VECTOR_2;
36 vector_add; vec; dot; orthogonal; basis;
37 vector_neg; vector_sub; vector_mul; ARITH] THEN
40 let COLLINEAR_3_2Dzero = thm `;
41 !y z:real^2. collinear{vec 0,y,z} <=>
43 by REWRITE_TAC[COLLINEAR_3_2D] THEN VEC2_TAC;
46 let Noncollinear_3ImpliesDistinct = thm `;
47 !a b c:real^N. ~collinear {a,b,c} ==> ~(a = b) /\ ~(a = c) /\ ~(b = c)
48 by COLLINEAR_BETWEEN_CASES, BETWEEN_REFL;
51 let collinearSymmetry = thm `;
53 thus collinear {A,B,C} ==> collinear {A,C,B} /\ collinear {B,A,C} /\
54 collinear {B,C,A} /\ collinear {C,A,B} /\ collinear {C,B,A}
57 {A,C,B} SUBSET {A,B,C} /\ {B,A,C} SUBSET {A,B,C} /\ {B,C,A} SUBSET {A,B,C} /\
58 {C,A,B} SUBSET {A,B,C} /\ {C,B,A} SUBSET {A,B,C} by SET_RULE;
59 qed by -, COLLINEAR_SUBSET;
62 let Noncollinear_2Span = thm `;
64 assume ~collinear {vec 0,v,w} [H1];
65 thus ? s t. s % v + t % w = u
68 !n r. ~(r < n) /\ r <= MIN n n ==> r = n [easy_arith] by ARITH_RULE;
69 ~(w$1 * v$2 = v$1 * w$2) [H1'] by H1, COLLINEAR_3_2Dzero;
71 M = transp(vector[v;w]):real^2^2 [Mexists];
72 det M = v$1 * w$2 - w$1 * v$2 by -, DIMINDEX_2, SUM_2, TRANSP_COMPONENT, VECTOR_2, LAMBDA_BETA, ARITH, CART_EQ, FORALL_2, DET_2;
73 ~(det M = &0) by -, H1', REAL_ARITH;
74 consider x s t such that
75 M ** x = u /\ s = x$1 /\ t = x$2 by -, easy_arith, DET_EQ_0_RANK, RANK_BOUND, MATRIX_FULL_LINEAR_EQUATIONS;
76 v$1 * s + w$1 * t = u$1 /\ v$2 * s + w$2 * t = u$2 by Mexists, -, SIMP_TAC[matrix_vector_mul; DIMINDEX_2; SUM_2; TRANSP_COMPONENT; VECTOR_2; LAMBDA_BETA; ARITH; CART_EQ; FORALL_2] THEN MESON_TAC[];
77 s % v + t % w = u by -, REAL_MUL_SYM, VECTOR_MUL_COMPONENT, VECTOR_ADD_COMPONENT, VEC2_TAC;
81 let oriented_area = new_definition
82 `oriented_area (a:real^2,b:real^2,c:real^2) =
83 ((b$1 - a$1) * (c$2 - a$2) - (c$1 - a$1) * (b$2 - a$2)) / &2`;;
85 let oriented_areaSymmetry = thm `;
86 !A B C A' B' C':real^2.
87 oriented_area (A,B,C) = oriented_area(A',B',C') ==>
88 oriented_area (B,C,A) = oriented_area (B',C',A') /\
89 oriented_area (C,A,B) = oriented_area (C',A',B') /\
90 oriented_area (A,C,B) = oriented_area (A',C',B') /\
91 oriented_area (B,A,C) = oriented_area (B',A',C') /\
92 oriented_area (C,B,A) = oriented_area (C',B',A')
93 by REWRITE_TAC[oriented_area] THEN VEC2_TAC;
96 let move = new_definition
97 `!A B C A' B' C':real^2. move (A,B,C) (A',B',C') <=>
98 (B = B' /\ C = C' /\ collinear {vec 0,C - B,A' - A} \/
99 A = A' /\ C = C' /\ collinear {vec 0,C - A,B' - B} \/
100 A = A' /\ B = B' /\ collinear {vec 0,B - A,C' - C})`;;
102 let moveInvariant = thm `;
104 assume move p p' [H1];
105 thus oriented_area p = oriented_area p'
108 consider X Y Z X' Y' Z' such that
109 p = X,Y,Z /\ p' = X',Y',Z' [pDef] by PAIR_SURJECTIVE;
110 move (X,Y,Z) (X',Y',Z') by -, H1;
111 oriented_area (X,Y,Z) = oriented_area (X',Y',Z') by -, SIMP_TAC[move; oriented_area; COLLINEAR_3; COLLINEAR_3_2Dzero] THEN VEC2_TAC;
115 let reachable = new_definition
117 reachable p p' <=> ?n. ?s.
118 s 0 = p /\ s n = p' /\
119 (!m. 0 <= m /\ m < n ==> move (s m) (s (SUC m)))`;;
121 let reachableN = new_definition
123 reachableN p p' n <=> ?s.
124 s 0 = p /\ s n = p' /\
125 (!m. 0 <= m /\ m < n ==> move (s m) (s (SUC m)))`;;
127 let ReachLemma = thm `;
128 !p p'. reachable p p' <=> ?n. reachableN p p' n
129 by reachable, reachableN;
132 let reachableN_CLAUSES = thm `;
133 ! p p'. (reachableN p p' 0 <=> p = p') /\
134 ! n. reachableN p p' (SUC n) <=> ? q. reachableN p q n /\ move q p'
138 consider s0 such that
140 reachableN p p' 0 <=> p = p' [0CLAUSE] by -, reachableN, LT, LE_0;
141 ! n. reachableN p p' (SUC n) ==> ? q. reachableN p q n /\ move q p' [Imp1]
144 assume reachableN p p' (SUC n) [H1];
146 s 0 = p /\ s (SUC n) = p' /\ !m. m < SUC n ==> move (s m) (s (SUC m)) [sDef] by H1, LE_0, reachableN;
147 consider q such that q = s n;
148 qed by sDef, -, LE_0, reachableN, LT;
149 ! n. (? q. reachableN p q n /\ move q p') ==> reachableN p p' (SUC n)
152 assume ? q. reachableN p q n /\ move q p';
154 reachableN p q n /\ move q p' [qExists] by -;
156 s 0 = p /\ s n = q /\ !m. m < n ==> move (s m) (s (SUC m)) [sDef] by -, reachableN, LT, LE_0;
158 t = \m. if m < SUC n then s m else p';
159 t 0 = p /\ t (SUC n) = p' /\ !m. m < SUC n ==> move (t m) (t (SUC m)) [tProp] by qExists, sDef, -, LT_0, LT_REFL, LT, LT_SUC;
160 qed by -, reachableN, LT, LE_0;
161 qed by 0CLAUSE, Imp1, -;
164 let reachableInvariant = thm `;
165 !p p':triple. reachable p p' ==>
166 oriented_area p = oriented_area p'
169 !n. !p p'. reachableN p p' n ==> oriented_area p = oriented_area p' by INDUCT_TAC THEN ASM_MESON_TAC[reachableN_CLAUSES; moveInvariant];
170 qed by -, ReachLemma;
173 let move2Cond = new_definition
174 `move2Cond (A,B,C) (A',B',C') <=>
175 ~collinear {B,A,A'} /\ ~collinear {A',B,B'} \/
176 ~collinear {A,B,B'} /\ ~collinear {B',A,A'}`;;
178 let reachableN_Two = thm `;
179 !P0 P2:triple. reachableN P0 P2 2 <=>
180 ?P1. move P0 P1 /\ move P1 P2
181 by ONE, TWO, reachableN_CLAUSES;
184 let reachableN_Three = thm `;
185 !P0 P3:triple. reachableN P0 P3 3 <=>
186 ?P1 P2. move P0 P1 /\ move P1 P2 /\ move P2 P3
189 3 = SUC 2 by ARITH_RULE;
190 qed by -, reachableN_Two, reachableN_CLAUSES;
193 let reachableN_Four = thm `;
194 !P0 P4:triple. reachableN P0 P4 4 <=>
195 ?P1 P2 P3. move P0 P1 /\ move P1 P2 /\ move P2 P3 /\ move P3 P4
198 4 = SUC 3 by ARITH_RULE;
199 qed by -, reachableN_Three, reachableN_CLAUSES;
202 let moveSymmetry = thm `;
203 let A B C A' B' C' be real^2;
204 assume move (A,B,C) (A',B',C') [H1];
205 thus move (B,C,A) (B',C',A') /\ move (C,A,B) (C',A',B') /\
206 move (A,C,B) (A',C',B') /\ move (B,A,C) (B',A',C') /\ move (C,B,A) (C',B',A')
209 !A B C A':real^2. collinear {vec 0, C - B, A' - A} ==>
210 collinear {vec 0, B - C, A' - A} by REWRITE_TAC[COLLINEAR_3_2Dzero] THEN VEC2_TAC;
214 let reachableNSymmetry = thm `;
215 ! A B C A' B' C' n. reachableN (A,B,C) (A',B',C') n ==>
216 reachableN (B,C,A) (B',C',A') n /\ reachableN (C,A,B) (C',A',B') n /\
217 reachableN (A,C,B) (A',C',B') n /\ reachableN (B,A,C) (B',A',C') n /\
218 reachableN (C,B,A) (C',B',A') n
222 consider Q such that Q = \n A' B' C'.
223 reachableN (B,C,A) (B',C',A') n /\ reachableN (C,A,B) (C',A',B') n /\
224 reachableN (A,C,B) (A',C',B') n /\ reachableN (B,A,C) (B',A',C') n /\
225 reachableN (C,B,A) (C',B',A') n [Qdef];
227 P = \n. ! A' B' C'. reachableN (A,B,C) (A',B',C') n ==> Q n A' B' C' [Pdef];
228 P 0 [Base] by -, Qdef, reachableN_CLAUSES, PAIR_EQ;
229 !n. P n ==> P (SUC n)
233 ! A' B' C'. reachableN (A,B,C) (A',B',C') (SUC n) ==> Q (SUC n) A' B' C'
235 let A' B' C' be real^2;
236 assume reachableN (A,B,C) (A',B',C') (SUC n);
237 consider X Y Z such that
238 reachableN (A,B,C) (X,Y,Z) n /\ move (X,Y,Z) (A',B',C') [XYZdef] by -, reachableN_CLAUSES, PAIR_SURJECTIVE;
239 qed by -, Qdef, Pdef, Pn, XYZdef, moveSymmetry, reachableN_CLAUSES;
241 !n. P n by Base, -, INDUCT_TAC;
242 qed by -, Pdef, Qdef;
245 let ORIENTED_AREA_COLLINEAR_CONG = thm `;
246 let A B C A' B' C' be real^2;
247 assume oriented_area (A,B,C) = oriented_area (A',B',C') [H1];
248 thus collinear {A,B,C} <=> collinear {A',B',C'}
249 by H1, REWRITE_TAC[COLLINEAR_3_2D; oriented_area] THEN CONV_TAC REAL_RING;
252 let Basic2move_THM = thm `;
253 let A B C A' be real^2;
254 assume ~collinear {A,B,C} [H1];
255 assume ~collinear {B,A,A'} [H2];
256 thus ? X. move (A,B,C) (A,B,X) /\ move (A,B,X) (A',B,X)
259 !r. r % (A - B) = (--r) % (B - A) /\ r % (A - B) = r % (A - B) + &0 % (C - B) [add0vector_mul] by VEC2_TAC;
260 ~ ? r. A' - A = r % (A - B) [H2'] by H2, COLLINEAR_3, COLLINEAR_LEMMA, -;
261 consider r t such that
262 A' - A = r % (A - B) + t % (C - B) [rExists] by H1, COLLINEAR_3, Noncollinear_2Span;
263 ~(t = &0) [tNonzero] by -, add0vector_mul, H2';
264 consider s X such that
265 s = r / t /\ X = C + s % (A - B) [Xexists] by rExists;
266 A' - A = (t * s) % (A - B) + t % (C - B) by rExists, -, tNonzero, REAL_DIV_LMUL;
267 A' - A = t % (X - B) [tProp] by -, Xexists, VEC2_TAC;
268 X - C = (-- s) % (B - A) by -, Xexists, VEC2_TAC;
269 collinear {vec 0,B - A,X - C} /\ collinear {vec 0,X - B,A' - A} by -, tProp, COLLINEAR_LEMMA;
273 let FourStepMoveAB = thm `;
274 let A B C A' B' C' be real^2;
275 assume ~collinear {A,B,C} [H1];
276 assume ~collinear {B,A,A'} /\ ~collinear {A',B,B'} [H2];
277 thus ? X Y. move (A,B,C) (A,B,X) /\ move (A,B,X) (A',B,X) /\
278 move (A',B,X) (A',B,Y) /\ move (A',B,Y) (A',B',Y)
282 move (A,B,C) (A,B,X) /\ move (A,B,X) (A',B,X) [ABX] by H1, H2, -, Basic2move_THM;
283 ~collinear {A,B,X} /\ ~collinear {A',B,X} by H1, -, moveInvariant, ORIENTED_AREA_COLLINEAR_CONG;
284 ~collinear {B,A',X} by -, collinearSymmetry;
286 move (B,A',X) (B,A',Y) /\ move (B,A',Y) (B',A',Y) by -, H2, Basic2move_THM;
287 move (A',B,X) (A',B,Y) /\ move (A',B,Y) (A',B',Y) by -, moveSymmetry;
291 let FourStepMoveABBAreach = thm `;
292 let A B C A' B' C' be real^2;
293 assume ~collinear {A,B,C} [H1];
294 assume move2Cond (A,B,C) (A',B',C') [H2];
295 thus ? Y. reachableN (A,B,C) (A',B',Y) 4
298 cases by H2, move2Cond;
299 suppose ~collinear {B,A,A'} /\ ~collinear {A',B,B'};
300 qed by H1, -, FourStepMoveAB, reachableN_Four;
301 suppose ~collinear {A,B,B'} /\ ~collinear {B',A,A'} [Case2];
302 ~collinear {B,A,C} by H1, collinearSymmetry;
303 consider X Y such that
304 move (B,A,C) (B,A,X) /\ move (B,A,X) (B',A,X) /\
305 move (B',A,X) (B',A,Y) /\ move (B',A,Y) (B',A',Y) by -, Case2, FourStepMoveAB;
306 qed by -, moveSymmetry, reachableN_Four;
310 let NotMove2Impliescollinear = thm `;
311 let A B C A' B' C' be real^2;
312 assume ~collinear {A,B,C} /\ ~collinear {A',B',C'} [H1];
313 assume ~(A = A') /\ ~(B = B') [H2];
314 assume ~move2Cond (A,B,C) (A',B',C') [H3];
315 thus collinear {A,B,A',B'}
318 ~(A = B) /\ ~(A' = B') [Distinct] by H1, Noncollinear_3ImpliesDistinct;
319 {A,B,A',B'} SUBSET {A,A',B,B'} /\ {A,B,A',B'} SUBSET {B,B',A',A} /\
320 {A,B,A',B'} SUBSET {A',B',B,A} [set4symmetry] by SET_RULE;
321 cases by H3, move2Cond;
322 suppose collinear {B,A,A'} /\ collinear {A,B,B'};
323 collinear {A,B,A'} /\ collinear {A,B,B'} by -, collinearSymmetry;
324 qed by Distinct, -, COLLINEAR_4_3;
325 suppose collinear {B,A,A'} /\ collinear {B',A,A'};
326 collinear {A,A',B} /\ collinear {A,A',B'} by -, collinearSymmetry;
327 collinear {A,A',B,B'} by H2, -, COLLINEAR_4_3;
328 qed by -, set4symmetry, COLLINEAR_SUBSET;
329 suppose collinear {A',B,B'} /\ collinear {A,B,B'};
330 collinear {B,B',A'} /\ collinear {B,B',A} by -, collinearSymmetry;
331 collinear {B,B',A',A} by H2, -, COLLINEAR_4_3;
332 qed by -, set4symmetry, COLLINEAR_SUBSET;
333 suppose collinear {A',B,B'} /\ collinear {B',A,A'};
334 collinear {A',B',B} /\ collinear {A',B',A} by -, collinearSymmetry;
335 collinear {A',B',B,A} by Distinct, -, COLLINEAR_4_3;
336 qed by -, set4symmetry, COLLINEAR_SUBSET;
340 let DistinctImplies2moveable = thm `;
341 let A B C A' B' C' be real^2;
342 assume ~collinear {A,B,C} /\ ~collinear {A',B',C'} [H1];
343 assume ~(A = A') /\ ~(B = B') /\ ~(C = C') [H2];
344 thus move2Cond (A,B,C) (A',B',C') \/ move2Cond (B,C,A) (B',C',A')
347 {A, B, B'} SUBSET {A, B, A', B'} /\ {B,B',C} SUBSET {B,C,B',C'} [3subset4] by SET_RULE;
348 ~collinear {B,C,A} /\ ~collinear {B',C',A'} [H1'] by H1, collinearSymmetry;
349 assume ~(move2Cond (A,B,C) (A',B',C') \/ move2Cond (B,C,A) (B',C',A'));
350 ~move2Cond (A,B,C) (A',B',C') /\ ~move2Cond (B,C,A) (B',C',A') by -;
351 collinear {A, B, A', B'} /\ collinear {B,C,B',C'} by H1, H1', -, H2, NotMove2Impliescollinear;
352 collinear {A, B, B'} /\ collinear {B,B',C} by -, 3subset4, COLLINEAR_SUBSET;
353 collinear {A, B, C} by -, H2, COLLINEAR_3_TRANS;
357 let SameCdiffAB = thm `;
358 let A B C A' B' C' be real^2;
359 assume ~collinear {A,B,C} /\ ~collinear {A',B',C'} [H1];
360 assume C = C' /\ ~(A = A') /\ ~(B = B') [H2];
361 thus ? Y. reachableN (A,B,C) (Y,B',C') 2 \/ reachableN (A,B,C) (A',B',Y) 4
364 {B,B',A} SUBSET {A,B,A',B'} /\ {A,B,C} SUBSET {B,B',A,C} [easy_set] by SET_RULE;
366 suppose ~collinear {C,B,B'};
368 move (B,C,A) (B,C,X) /\ move (B,C,X) (B',C',X) by H1, collinearSymmetry, -, H2, Basic2move_THM;
369 qed by -, reachableN_Two, reachableNSymmetry;
370 suppose move2Cond (A,B,C) (A',B',C');
371 qed by H1, -, FourStepMoveABBAreach;
372 suppose collinear {C,B,B'} /\ ~move2Cond (A,B,C) (A',B',C');
373 collinear {B,B',A} /\ collinear {B,B',C} by H1, H2, -, NotMove2Impliescollinear, easy_set, COLLINEAR_SUBSET, collinearSymmetry;
374 qed by -, H2, COLLINEAR_4_3, easy_set, COLLINEAR_SUBSET, H1;
378 let FourMovesToCorrectTwo = thm `;
379 let A B C A' B' C' be real^2;
380 assume ~collinear {A,B,C} /\ ~collinear {A',B',C'} [H1];
381 thus ? n. n < 5 /\ ? Y. reachableN (A,B,C) (A',B',Y) n \/
382 reachableN (A,B,C) (A',Y,C') n \/ reachableN (A,B,C) (Y,B',C') n
385 ~collinear {B,C,A} /\ ~collinear {B',C',A'} /\ ~collinear {C,A,B} /\ ~collinear {C',A',B'} [H1'] by H1, collinearSymmetry;
386 0 < 5 /\ 2 < 5 /\ 3 < 5 /\ 4 < 5 [easy_arith] by ARITH_RULE;
388 suppose A = A' /\ B = B' /\ C = C' \/ A = A' /\ B = B' /\ ~(C = C') \/
389 A = A' /\ ~(B = B') /\ C = C' \/ ~(A = A') /\ B = B' /\ C = C';
390 reachableN (A,B,C) (A',B',C') 0 \/ reachableN (A,B,C) (A',B',C) 0 \/
391 reachableN (A,B,C) (A',B,C') 0 \/ reachableN (A,B,C) (A,B',C') 0 by -, reachableN_CLAUSES;
392 qed by -, easy_arith;
393 suppose A = A' /\ ~(B = B') /\ ~(C = C') \/
394 ~(A = A') /\ B = B' /\ ~(C = C') \/ ~(A = A') /\ ~(B = B') /\ C = C';
395 qed by H1, H1', -, SameCdiffAB, reachableNSymmetry, easy_arith;
396 suppose ~(A = A') /\ ~(B = B') /\ ~(C = C');
397 move2Cond (A,B,C) (A',B',C') \/ move2Cond (B,C,A) (B',C',A') by H1, -, DistinctImplies2moveable;
398 qed by H1, H1', -, FourStepMoveABBAreach, reachableNSymmetry, reachableN_Four, easy_arith;
402 let CorrectFinalPoint = thm `;
403 let A B C A' C' be real^2;
404 assume oriented_area (A,B,C) = oriented_area (A,B,C') [H1];
405 thus move (A,B,C) (A,B,C')
408 ((B$1 - A$1) * (C$2 - A$2) - (C$1 - A$1) * (B$2 - A$2)) / &2 =
409 ((B$1 - A$1) * (C'$2 - A$2) - (C'$1 - A$1) * (B$2 - A$2)) / &2 by H1, oriented_area;
410 (C$1 - C'$1) * (B$2 - A$2) = (B$1 - A$1) * (C$2 - C'$2) by -, REAL_ARITH;
411 (C' - C)$1 * (B - A)$2 = (B - A)$1 * (C' - C)$2 by -, VEC2_TAC;
412 collinear {vec 0, B - A, C' - C} by -, COLLINEAR_3_2Dzero;
416 let FiveMovesOrLess = thm `;
417 let A B C A' B' C' be real^2;
418 assume ~collinear {A,B,C} [H1];
419 assume oriented_area (A,B,C) = oriented_area (A',B',C') [H2];
420 thus ? n. n <= 5 /\ reachableN (A,B,C) (A',B',C') n
423 ~collinear {A',B',C'} [H1'] by H1, H2, ORIENTED_AREA_COLLINEAR_CONG;
424 ~(A = B) /\ ~(A = C) /\ ~(B = C) /\ ~(A' = B') /\ ~(A' = C') /\ ~(B' = C') [Distinct] by H1, -, Noncollinear_3ImpliesDistinct;
425 consider n Y such that
426 n < 5 /\ (reachableN (A,B,C) (A',B',Y) n \/
427 reachableN (A,B,C) (A',Y,C') n \/ reachableN (A,B,C) (Y,B',C') n) [2Correct] by H1, H1', FourMovesToCorrectTwo;
429 suppose reachableN (A,B,C) (A',B',Y) n [Case];
430 oriented_area (A',B',Y) = oriented_area (A',B',C') by H2, -, ReachLemma, reachableInvariant;
431 move (A',B',Y) (A',B',C') by -, Distinct, CorrectFinalPoint;
432 qed by Case, -, reachableN_CLAUSES, 2Correct, LE_SUC_LT;
433 suppose reachableN (A,B,C) (A',Y,C') n [Case];
434 oriented_area (A',C',Y) = oriented_area (A',C',B') by H2, -, ReachLemma, reachableInvariant, oriented_areaSymmetry;
435 move (A',Y,C') (A',B',C') by -, Distinct, CorrectFinalPoint, moveSymmetry;
436 qed by Case, -, reachableN_CLAUSES, 2Correct, LE_SUC_LT;
437 suppose reachableN (A,B,C) (Y,B',C') n [Case];
438 oriented_area (B',C',Y) = oriented_area (B',C',A') by H2, -, ReachLemma, reachableInvariant, oriented_areaSymmetry;
439 move (Y,B',C') (A',B',C') by -, Distinct, CorrectFinalPoint, moveSymmetry;
440 qed by Case, -, reachableN_CLAUSES, 2Correct, LE_SUC_LT;
444 let NOTENOUGH_4 = thm `;
445 ?p0 p4. oriented_area p0 = oriented_area p4 /\ ~reachableN p0 p4 4
448 consider p0 p4 such that
449 p0 = vector [&0;&0]:real^2,vector [&0;&1]:real^2,vector [&1;&0]:real^2 /\
450 p4 = vector [&1;&1]:real^2,vector [&1;&2]:real^2,vector [&2;&1]:real^2 [p04Def];
451 oriented_area p0 = oriented_area p4 [equal_areas] by -, ASM_REWRITE_TAC[oriented_area] THEN VEC2_TAC;
452 ~reachableN p0 p4 4 by p04Def, ASM_REWRITE_TAC[reachableN_Four; NOT_EXISTS_THM; FORALL_PAIR_THM; move; COLLINEAR_3_2Dzero; FORALL_VECTOR_2] THEN VEC2_TAC;
453 qed by equal_areas, -;
456 let reachableN_Five = thm `;
457 !P0 P5:triple. reachableN P0 P5 5 <=>
458 ?P1 P2 P3 P4. move P0 P1 /\ move P1 P2 /\ move P2 P3 /\ move P3 P4 /\ move P4 P5
461 5 = SUC 4 by ARITH_RULE;
462 qed by -, reachableN_CLAUSES, reachableN_Four;
465 let EasyCollinearMoves = thm `;
466 (!A A' B:real^2. move (A:real^2,B,B) (A',B,B)) /\
467 !A B B' C:real^2. collinear {A:real^2,B,C} /\ collinear {A,B',C}
468 ==> move (A,B,C) (A,B',C)
469 by REWRITE_TAC[move; COLLINEAR_3_2D] THEN VEC2_TAC;
472 let FiveMovesOrLess_STRONG = thm `;
473 let A B C A' B' C' be real^2;
474 assume oriented_area (A,B,C) = oriented_area (A',B',C') [H1];
475 thus ?n. n <= 5 /\ reachableN (A,B,C) (A',B',C') n
478 {A,C,C} = {A,C} /\ {B',C,C} = {B',C} /\ {B',B',C} = {B',C} /\ {B',B',C'} = {B',C'} [easy_sets] by SET_RULE;
480 suppose ~collinear {A,B,C};
481 qed by -, H1, FiveMovesOrLess;
482 suppose collinear {A,B,C} [ABCcol];
483 collinear {A',B',C'} [A'B'C'col] by -, H1, ORIENTED_AREA_COLLINEAR_CONG;
484 consider P1 P2 P3 P4 such that
485 P1 = A,C,C /\ P2 = B',C,C /\ P3 = B',B',C /\ P4 = B',B',C';
486 move (A,B,C) P1 /\ move P1 P2 /\ move P2 P3 /\ move P3 P4 /\ move P4 (A',B',C') by -, ABCcol, A'B'C'col, easy_sets, COLLINEAR_2, collinearSymmetry, moveSymmetry, EasyCollinearMoves;
487 qed by -, reachableN_Five, LE_REFL;