Examples/inverse_bug_puzzle_miz3.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:            *)
   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.           *)
  15 (*                                                                           *)
  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 (* ========================================================================= *)
  20
  21 needs "Multivariate/determinants.ml";;
  22
  23 #load "unix.cma";;
  24 loadt "miz3/miz3.ml";;
  25
  26 new_type_abbrev("triple",`:real^2#real^2#real^2`);;
  27
  28 default_prover := ("ya prover",
  29     fun thl -> REWRITE_TAC thl THEN CONV_TAC (HOL_BY thl));;
  30
  31 horizon := 0;;
  32 timeout := 500;;
  33
  34 let VEC2_TAC =
  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
  38   CONV_TAC REAL_RING;;
  39
  40 let COLLINEAR_3_2Dzero = thm `;
  41   !y z:real^2. collinear{vec 0,y,z} <=>
  42                   z$1 * y$2 = y$1 * z$2
  43   by REWRITE_TAC[COLLINEAR_3_2D] THEN VEC2_TAC;
  44 `;;
  45
  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;
  49 `;;
  50
  51 let collinearSymmetry = thm `;
  52   let A B C be real^N;
  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}
  55
  56   proof
  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;
  60 `;;
  61
  62 let Noncollinear_2Span = thm `;
  63   let u v w be real^2;
  64   assume ~collinear  {vec 0,v,w}        [H1];
  65   thus ? s t. s % v + t % w = u
  66
  67   proof
  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;
  70     consider M such that
  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;
  78   qed     by -;
  79 `;;
  80
  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`;;
  84
  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;
  94 `;;
  95
  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})`;;
 101
 102 let moveInvariant = thm `;
 103   let p p' be triple;
 104   assume move p p'                                              [H1];
 105   thus oriented_area p = oriented_area p'
 106
 107   proof
 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;
 112   qed     by -, pDef;
 113 `;;
 114
 115 let reachable = new_definition
 116   `!p p'.
 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)))`;;
 120
 121 let reachableN = new_definition
 122   `!p p'. !n.
 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)))`;;
 126
 127 let ReachLemma = thm `;
 128   !p p'. reachable p p'  <=>  ?n.  reachableN p p' n
 129   by reachable, reachableN;
 130 `;;
 131
 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'
 135
 136   proof
 137     let p p' be triple;
 138     consider s0 such that
 139     s0 = \m:num. p';
 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]
 142     proof
 143       let n be num;
 144       assume reachableN p p' (SUC n)     [H1];
 145       consider s such that
 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)
 150     proof
 151       let n be num;
 152       assume ? q. reachableN p q n  /\ move q p';
 153       consider q such that
 154       reachableN p q n  /\ move q p'     [qExists] by -;
 155       consider s such that
 156       s 0 = p /\ s n = q /\ !m. m < n ==> move (s m) (s (SUC m))     [sDef] by -, reachableN, LT, LE_0;
 157       consider t such that
 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, -;
 162 `;;
 163
 164 let reachableInvariant = thm `;
 165   !p p':triple. reachable p p'  ==>
 166   oriented_area p = oriented_area p'
 167
 168   proof
 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;
 171 `;;
 172
 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'}`;;
 177
 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;
 182 `;;
 183
 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
 187
 188    proof
 189      3 = SUC 2     by ARITH_RULE;
 190    qed     by -, reachableN_Two, reachableN_CLAUSES;
 191 `;;
 192
 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
 196
 197    proof
 198      4 = SUC 3     by ARITH_RULE;
 199   qed     by -, reachableN_Three, reachableN_CLAUSES;
 200 `;;
 201
 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')
 207
 208   proof
 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;
 211   qed     by H1, -, move;
 212 `;;
 213
 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
 219
 220   proof
 221     let A B C be real^2;
 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];
 226     consider P such that
 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)
 230     proof
 231       let n be num;
 232       assume P n [Pn];
 233       ! A' B' C'. reachableN (A,B,C) (A',B',C') (SUC n)  ==> Q (SUC n) A' B' C'
 234       proof
 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;
 240     qed     by -, Pdef;
 241     !n. P n     by Base, -, INDUCT_TAC;
 242   qed     by -, Pdef, Qdef;
 243 `;;
 244
 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;
 250 `;;
 251
 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)
 257
 258   proof
 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;
 270   qed     by -, move;
 271 `;;
 272
 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)
 279
 280   proof
 281     consider X such that
 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;
 285     consider Y such that
 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;
 288   qed     by -, ABX;
 289 `;;
 290
 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
 296
 297   proof
 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;
 307   end;
 308 `;;
 309
 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'}
 316
 317   proof
 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;
 337   end;
 338 `;;
 339
 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')
 345
 346   proof
 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;
 354   qed     by  -, H1;
 355 `;;
 356
 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
 362
 363   proof
 364     {B,B',A} SUBSET {A,B,A',B'}  /\  {A,B,C} SUBSET {B,B',A,C}     [easy_set] by SET_RULE;
 365     cases;
 366     suppose ~collinear {C,B,B'};
 367       consider X such that
 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;
 375   end;
 376 `;;
 377
 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
 383
 384   proof
 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;
 387     cases;
 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;
 399   end;
 400 `;;
 401
 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')
 406
 407   proof
 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;
 413   qed     by -, move;
 414 `;;
 415
 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
 421
 422   proof
 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;
 428     cases     by 2Correct;
 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;
 441   end;
 442 `;;
 443
 444 let NOTENOUGH_4 = thm `;
 445   ?p0 p4. oriented_area p0 = oriented_area p4 /\ ~reachableN p0 p4 4
 446
 447   proof
 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, -;
 454 `;;
 455
 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
 459
 460   proof
 461     5 = SUC 4     by ARITH_RULE;
 462   qed by -, reachableN_CLAUSES, reachableN_Four;
 463 `;;
 464
 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;
 470 `;;
 471
 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
 476
 477   proof
 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;
 479     cases;
 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;
 488   end;
 489 `;;