RichterHilbertAxiomGeometry/inverse_bug_puzzle_read.ml

   1 (* ========================================================================= *)
   2 (*                (c) Copyright, Bill Richter 2013                           *)
   3 (*          Distributed under the same license as HOL Light                  *)
   4 (*                                                                           *)
   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.        *)
  15 (*                                                                           *)
  16 (* The mathematical proofs are essentially due to Tom Hales.                 *)
  17 (* ========================================================================= *)
  18
  19 needs "Multivariate/determinants.ml";;
  20 needs "RichterHilbertAxiomGeometry/readable.ml";;
  21
  22 new_type_abbrev("triple",`:real^2#real^2#real^2`);;
  23
  24 let VEC2_TAC =
  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
  28   CONV_TAC REAL_RING;;
  29
  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`;;
  33
  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})`;;
  39
  40 let reachable = NewDefinition `;
  41   ∀p p'.
  42   reachable p p'  ⇔  ∃n. ∃s. s 0 = p ∧ s n = p' ∧
  43   (∀m. 0 <= m ∧ m < n ⇒ move (s m) (s (SUC m)))`;;
  44
  45 let reachableN = NewDefinition `;
  46   ∀p p'. ∀n.
  47   reachableN p p' n  ⇔  ∃s. s 0 = p ∧ s n = p' ∧
  48   (∀m. 0 <= m ∧ m < n ⇒ move (s m) (s (SUC m)))`;;
  49
  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'}`;;
  54
  55
  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')
  63   proof
  64     rewrite oriented_area; VEC2_TAC;
  65   qed;
  66 `;;
  67
  68 let COLLINEAR_3_2Dzero = theorem `;
  69   ∀y z:real^2. collinear{vec 0,y,z} ⇔
  70                   z$1 * y$2 = y$1 * z$2
  71   proof
  72     rewrite COLLINEAR_3_2D;     VEC2_TAC;     qed;
  73 `;;
  74
  75 let Noncollinear_3ImpliesDistinct = theorem `;
  76   ¬collinear {a,b,c}  ⇒  ¬(a = b) ∧ ¬(a = c) ∧ ¬(b = c)
  77   by fol COLLINEAR_BETWEEN_CASES BETWEEN_REFL`;;
  78
  79 let collinearSymmetry = theorem `;
  80   collinear {A,B,C}
  81          ⇒ collinear {A,C,B} ∧ collinear {B,A,C} ∧
  82              collinear {B,C,A} ∧ collinear {C,A,B} ∧ collinear {C,B,A}
  83   proof
  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;
  87   qed;
  88 `;;
  89
  90 let Noncollinear_2Span = theorem `;
  91   ∀u v w:real^2. ¬collinear  {vec 0,v,w} ⇒ ∃ s t. s % v + t % w = u
  92
  93   proof
  94     intro_TAC ∀u v w, H1;
  95     ¬(v$1 * w$2 - w$1 * v$2 = &0)     [H1'] by fol H1 COLLINEAR_3_2Dzero REAL_SUB_0;
  96     consider M such that
  97     M = transp(vector[v;w]):real^2^2     [Mexists] by fol -;
  98     ¬(det M = &0) ∧
  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;
 104     exists_TAC x$1;
 105     exists_TAC x$2;
 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;
 109   qed;
 110 `;;
 111
 112 let moveInvariant = theorem `;
 113   ∀p p'. move p p' ⇒ oriented_area p = oriented_area p'
 114   proof
 115     rewrite FORALL_PAIR_THM move oriented_area COLLINEAR_LEMMA  vector_mul; VEC2_TAC;
 116   qed;
 117 `;;
 118
 119 let ReachLemma = theorem `;
 120   ∀p p'. reachable p p'  ⇔  ∃n.  reachableN p p' n
 121   proof
 122     rewrite reachable reachableN;
 123   qed;
 124 `;;
 125
 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'
 129
 130   proof
 131     intro_TAC ∀p 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]
 135     proof
 136       intro_TAC ∀n, H1;
 137       consider s such that
 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;
 141     qed;
 142     ∀n. (∃ q. reachableN p q n  ∧ move q p')  ⇒  reachableN p p' (SUC n)     [Imp2]
 143     proof
 144       intro_TAC ∀n;
 145       rewrite IMP_CONJ LEFT_IMP_EXISTS_THM;
 146       intro_TAC ∀q, nReach, move_qp';
 147       consider s such that
 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;
 152     qed;
 153     fol 0CLAUSE Imp1 Imp2;
 154   qed;
 155 `;;
 156
 157 let reachableInvariant = theorem `;
 158   ∀p p'. reachable p p'  ⇒  oriented_area p = oriented_area p'
 159
 160   proof
 161     simplify ReachLemma LEFT_IMP_EXISTS_THM SWAP_FORALL_THM;
 162     MATCH_MP_TAC num_INDUCTION;
 163     simplify reachableN_CLAUSES;
 164     intro_TAC ∀n, nStep;
 165     fol nStep moveInvariant;
 166   qed;
 167 `;;
 168
 169 let reachableN_One = theorem `;
 170   reachableN P0 P1 1 ⇔ move P0 P1
 171   by fol ONE reachableN reachableN_CLAUSES`;;
 172
 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`;;
 176
 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`;;
 180
 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`;;
 185
 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
 189   proof
 190     rewrite ARITH_RULE [5 = SUC 4] reachableN_CLAUSES;
 191     fol reachableN_Four;
 192   qed;
 193 `;;
 194
 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')
 199
 200   proof
 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;
 204     MP_TAC -;
 205     rewrite move;
 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;
 209     MP_TAC -;
 210     rewrite move;
 211     fol;
 212   qed;
 213 `;;
 214
 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
 220
 221   proof
 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;
 226     X_genl_TAC X Y Z;
 227     intro_TAC XYZexists;
 228     rewrite RIGHT_AND_EXISTS_THM LEFT_AND_EXISTS_THM;
 229     exists_TAC (Y,Z,X);
 230     exists_TAC (Z,X,Y);
 231     exists_TAC (X,Z,Y);
 232     exists_TAC (Y,X,Z);
 233     exists_TAC (Z,Y,X);
 234     simplify nStep XYZexists moveSymmetry;
 235   qed;
 236 `;;
 237
 238 let ORIENTED_AREA_COLLINEAR_CONG = theorem `;
 239   ∀ A B C A' B' C.
 240     oriented_area (A,B,C) = oriented_area (A',B',C')
 241     ⇒ (collinear {A,B,C} ⇔ collinear {A',B',C'})
 242   proof
 243     rewrite COLLINEAR_3_2D oriented_area; real_ring;
 244   qed;
 245 `;;
 246
 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)
 250
 251   proof
 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;
 263     fol - move;
 264   qed;
 265 `;;
 266
 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)
 272
 273   proof
 274     intro_TAC ∀A B C A' B', H1, H2;
 275     consider X such that
 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;
 279     consider Y such that
 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;
 282     fol - ABX;
 283   qed;
 284 `;;
 285
 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
 289
 290   proof
 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;
 295     end;
 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;
 302     end;
 303   qed;
 304 `;;
 305
 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'}
 310
 311   proof
 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;
 319     end;
 320     suppose collinear {B,A,A'} ∧ collinear {B',A,A'};
 321       fol - Distinct H2 H2' set4symmetry collinearSymmetry COLLINEAR_4_3 COLLINEAR_SUBSET;
 322     end;
 323     suppose collinear {A',B,B'} ∧ collinear {A,B,B'};
 324       fol - Distinct H2 H2' set4symmetry collinearSymmetry COLLINEAR_4_3 COLLINEAR_SUBSET;
 325     end;
 326     suppose collinear {A',B,B'} ∧ collinear {B',A,A'};
 327       fol - Distinct H2 H2' set4symmetry collinearSymmetry COLLINEAR_4_3 COLLINEAR_SUBSET;
 328     end;
 329   qed;
 330 `;;
 331
 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'}
 336
 337   proof
 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;
 347   qed;
 348 `;;
 349
 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'
 354
 355   proof
 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;
 361     fol - H1 H1';
 362   qed;
 363 `;;
 364
 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
 369
 370   proof
 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;
 377     end;
 378     suppose move2Cond A B A' B';
 379       fol - H1 FourStepMoveABBAreach;
 380     end;
 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;
 384     end;
 385   qed;
 386 `;;
 387
 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
 392
 393   proof
 394     intro_TAC ∀A B C A' B' C', H1;
 395     ¬collinear {B,C,A} ∧
 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;
 403     end;
 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;
 407     end;
 408     suppose ¬(A = A') ∧ ¬(B = B') ∧ ¬(C = C');
 409       exists_TAC 4;
 410       simplify easy_arith reachableN_CLAUSES;
 411       fol - H1  H1' DistinctImplies2moveable FourStepMoveABBAreach
 412     reachableNSymmetry reachableN_Four;
 413     end;
 414   qed;
 415 `;;
 416
 417 let CorrectFinalPoint = theorem `;
 418  oriented_area (A,B,C) = oriented_area (A,B,C') ⇒
 419    move (A,B,C) (A,B,C')
 420   proof
 421     rewrite move oriented_area COLLINEAR_3_2Dzero; VEC2_TAC;
 422   qed;
 423 `;;
 424
 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
 429
 430   proof
 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;
 443     end;
 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;
 448     end;
 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;
 453     end;
 454   qed;
 455 `;;
 456
 457 let NOTENOUGH_4 = theorem `;
 458   ∃p0 p4. oriented_area p0 = oriented_area p4 ∧ ¬reachableN p0 p4 4
 459
 460   proof
 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
 464     fol;
 465     oriented_area p0 = oriented_area p4     [equal_areas]
 466     proof     rewrite - oriented_area;     VEC2_TAC;     qed;
 467     ¬reachableN p0 p4 4     []
 468     proof
 469       rewrite p04Def reachableN_Four NOT_EXISTS_THM FORALL_PAIR_THM move COLLINEAR_3_2Dzero FORALL_VECTOR_2;
 470       VEC2_TAC;
 471     qed;
 472     fol - equal_areas;
 473   qed;
 474 `;;
 475
 476 let FiveMovesOrLess_STRONG = theorem `;
 477   ∀A B C A' B' C'.
 478     oriented_area (A,B,C) = oriented_area (A',B',C') ⇒
 479     ∃n. n <= 5 ∧ reachableN (A,B,C) (A',B',C') n
 480
 481   proof
 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;
 491     end;
 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;
 500     end;
 501   qed;
 502 `;;
 503