Examples/inverse_bug_puzzle_tac.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.  The code       *)
  17 (* tries to mix declarative and procedural proof styles, using ideas due     *)
  18 (* to John Harrison (section 12.1 "Towards more readable proofs" of the      *)
  19 (* HOL Light tutorial), Freek Wiedijk (arxiv.org/pdf/1201.3601 "A            *)
  20 (* Synthesis of the Procedural and Declarative Styles of Interactive         *)
  21 (* Theorem Proving"), Marco Maggesi, who wrote the tactic constructs         *)
  22 (* INTRO_TAC & HYP, which goes well with the older SUBGOAL_TAC, and Petros   *)
  23 (* Papapanagiotou, coauthor of IsabelleLight, who wrote BuildExist below, a  *)
  24 (* a crucial part of consider.                                               *)
  25 (* ========================================================================= *)
  26
  27 needs "Multivariate/determinants.ml";;
  28
  29 new_type_abbrev("triple",`:real^2#real^2#real^2`);;
  30
  31 let so = fun tac -> FIRST_ASSUM MP_TAC THEN tac;;
  32
  33 let BuildExist x t =
  34   let try_type tp tm =
  35     try inst (type_match (type_of tm) tp []) tm
  36     with Failure _ -> tm in
  37
  38   (* Check if two variables match allowing only type instantiations: *)
  39   let vars_match tm1 tm2 =
  40     let inst = try term_match [] tm1 tm2 with Failure _ -> [],[tm2,tm1],[] in
  41       match inst with
  42         [],[],_ -> tm2
  43       | _  -> failwith "vars_match: no match" in
  44
  45   (* Find the type of a matching variable in t. *)
  46   let tp = try type_of (tryfind (vars_match x) (frees t))
  47   with Failure _ ->
  48   warn true ("BuildExist: `" ^ string_of_term x ^ "` not be found in
  49   `" ^ string_of_term t ^ "`") ;
  50   type_of x in
  51   (* Try to force x to type tp. *)
  52   let x' = try_type tp x in
  53   mk_exists (x',t);;
  54
  55 let consider vars_SuchThat t prfs lab =
  56   (* Functions ident and parse_using borrowed from HYP in tactics.ml *)
  57   let ident = function
  58       Ident s::rest when isalnum s -> s,rest
  59     | _ -> raise Noparse in
  60   let parse_using = many ident in
  61   let rec findSuchThat = function
  62       n -> if String.sub vars_SuchThat n 9 = "such that" then n
  63       else findSuchThat (n + 1) in
  64   let n = findSuchThat 1 in
  65   let vars = String.sub vars_SuchThat 0 (n - 1) in
  66   let xl = map parse_term ((fst o parse_using o lex o explode) vars) in
  67   let tm = itlist BuildExist xl t in
  68   match prfs with
  69     p::ps -> (warn (ps <> []) "consider: additional subproofs ignored";
  70     SUBGOAL_THEN tm (DESTRUCT_TAC ("@" ^ vars ^ "." ^ lab))
  71     THENL [p; ALL_TAC])
  72   | [] -> failwith "consider: no subproof given";;
  73
  74 let cases sDestruct disjthm tac =
  75   SUBGOAL_TAC "" disjthm tac THEN FIRST_X_ASSUM
  76   (DESTRUCT_TAC sDestruct);;
  77
  78 let raa lab t tac = SUBGOAL_THEN (mk_imp(t, `F`)) (LABEL_TAC lab) THENL
  79   [INTRO_TAC lab; tac];;
  80
  81 let VEC2_TAC =
  82   SIMP_TAC[CART_EQ; LAMBDA_BETA; FORALL_2; SUM_2; DIMINDEX_2; VECTOR_2;
  83            vector_add; vec; dot; orthogonal; basis;
  84            vector_neg; vector_sub; vector_mul; ARITH] THEN
  85   CONV_TAC REAL_RING;;
  86
  87 let COLLINEAR_3_2Dzero = prove
  88  (`!y z:real^2. collinear{vec 0,y,z} <=>
  89                   z$1 * y$2 = y$1 * z$2`,
  90   REWRITE_TAC[COLLINEAR_3_2D] THEN VEC2_TAC);;
  91
  92 let Noncollinear_3ImpliesDistinct = prove
  93   (`~collinear {a,b,c}  ==>  ~(a = b) /\ ~(a = c) /\ ~(b = c)`,
  94   MESON_TAC[COLLINEAR_BETWEEN_CASES; BETWEEN_REFL]);;
  95
  96 let collinearSymmetry = prove
  97 (`collinear {A,B,C}
  98          ==> collinear {A,C,B} /\ collinear {B,A,C} /\
  99              collinear {B,C,A} /\ collinear {C,A,B} /\ collinear {C,B,A}`,
 100   MESON_TAC[SET_RULE `{A,C,B} SUBSET {A,B,C} /\  {B,A,C} SUBSET {A,B,C} /\
 101   {B,C,A} SUBSET {A,B,C} /\  {C,A,B} SUBSET {A,B,C} /\  {C,B,A} SUBSET {A,B,C}`;
 102   COLLINEAR_SUBSET]);;
 103
 104 let Noncollinear_2Span = prove
 105  (`!u v w:real^2. ~collinear  {vec 0,v,w} ==> ? s t. s % v + t % w = u`,
 106   INTRO_TAC "!u v w; H1" THEN
 107   SUBGOAL_TAC "H1'" `~(v$1 * w$2 - (w:real^2)$1 * (v:real^2)$2 = &0)`
 108   [HYP MESON_TAC "H1" [COLLINEAR_3_2Dzero; REAL_SUB_0]] THEN
 109   consider "M such that"
 110   `M = transp(vector[v:real^2;w:real^2]):real^2^2` [MESON_TAC[]] "Mexists" THEN
 111   SUBGOAL_TAC "MatMult" `~(det (M:real^2^2) = &0) /\
 112   (! x. (M ** x)$1 = (v:real^2)$1 * x$1 + (w:real^2)$1 * x$2  /\
 113   (M ** x)$2 = v$2 * x$1 + w$2 * x$2)`
 114   [HYP SIMP_TAC "H1' Mexists" [matrix_vector_mul; DIMINDEX_2; SUM_2;
 115   TRANSP_COMPONENT; VECTOR_2; LAMBDA_BETA; ARITH; CART_EQ; FORALL_2; DET_2] THEN VEC2_TAC] THEN
 116   consider "x such that" `(M:real^2^2) ** x = u`
 117   [so (MESON_TAC [ARITH_RULE `~(r < n)  /\  r <= MIN n n  ==>  r = n`;
 118   DET_EQ_0_RANK; RANK_BOUND; MATRIX_FULL_LINEAR_EQUATIONS])] "xDef" THEN
 119   MAP_EVERY EXISTS_TAC [`(x:real^2)$1`; `(x:real^2)$2`] THEN SUBGOAL_TAC ""
 120   `(x:real^2)$1 * (v:real^2)$1 + (x:real^2)$2 * (w:real^2)$1 = (u:real^2)$1  /\
 121   x$1 * v$2 + x$2 * w$2 = u$2` [HYP MESON_TAC "MatMult xDef" [REAL_MUL_SYM]]
 122   THEN so (SIMP_TAC[CART_EQ; LAMBDA_BETA; FORALL_2; SUM_2; DIMINDEX_2; VECTOR_2; vector_add; vector_mul; ARITH]));;
 123
 124 let oriented_area = new_definition
 125   `oriented_area (a:real^2,b:real^2,c:real^2) =
 126   ((b$1 - a$1) * (c$2 - a$2) - (c$1 - a$1) * (b$2 - a$2)) / &2`;;
 127
 128 let oriented_areaSymmetry = prove
 129  (`oriented_area (A,B,C) = oriented_area(A',B',C')  ==>
 130   oriented_area (B,C,A) = oriented_area (B',C',A')  /\
 131   oriented_area (C,A,B) = oriented_area (C',A',B')  /\
 132   oriented_area (A,C,B) = oriented_area (A',C',B')  /\
 133   oriented_area (B,A,C) = oriented_area (B',A',C')  /\
 134   oriented_area (C,B,A) = oriented_area (C',B',A')`,
 135   REWRITE_TAC[oriented_area] THEN VEC2_TAC);;
 136
 137 let move = new_definition
 138   `!A B C A' B' C':real^2. move (A,B,C) (A',B',C') <=>
 139   (B = B' /\ C = C' /\ collinear {vec 0,C - B,A' - A} \/
 140   A = A' /\ C = C' /\ collinear {vec 0,C - A,B' - B} \/
 141   A = A' /\ B = B' /\ collinear {vec 0,B - A,C' - C})`;;
 142
 143 let moveInvariant = prove
 144   (`!p p'. move p p' ==> oriented_area p = oriented_area p'`,
 145   REWRITE_TAC[FORALL_PAIR_THM; move; oriented_area; COLLINEAR_LEMMA;  vector_mul] THEN VEC2_TAC);;
 146
 147 let reachable = new_definition
 148   `!p p'.
 149   reachable p p' <=> ?n. ?s.
 150   s 0 = p /\ s n = p' /\
 151   (!m. 0 <= m /\ m < n ==> move (s m) (s (SUC m)))`;;
 152
 153 let reachableN = new_definition
 154   `!p p'. !n.
 155   reachableN p p' n <=> ?s.
 156   s 0 = p /\ s n = p' /\
 157   (!m. 0 <= m /\ m < n ==> move (s m) (s (SUC m)))`;;
 158
 159 let ReachLemma = prove
 160  (`!p p'. reachable p p'  <=>  ?n.  reachableN p p' n`,
 161   REWRITE_TAC[reachable; reachableN]);;
 162
 163 let reachableN_CLAUSES = prove
 164  (`! p p'. (reachableN p p' 0  <=>  p = p') /\
 165   ! n. reachableN p p' (SUC n)  <=>  ? q. reachableN p q n  /\ move q p'`,
 166   INTRO_TAC "!p p'" THEN
 167   consider "s0 such that" `s0 =  \m:num. p':triple` [MESON_TAC[]] "s0exists" THEN
 168   SUBGOAL_TAC "0CLAUSE" `reachableN p p' 0  <=>  p = p'`
 169   [HYP MESON_TAC "s0exists" [LE_0; reachableN; LT]] THEN SUBGOAL_TAC "Imp1"
 170   `! n. reachableN p p' (SUC n)  ==>  ? q. reachableN p q n  /\ move q p'`
 171   [INTRO_TAC "!n; H1" THEN
 172   consider "s such that"
 173   `s 0 = p /\ s (SUC n) = p' /\ !m. m < SUC n ==> move (s m) (s (SUC m))`
 174   [HYP MESON_TAC "H1" [LE_0; reachableN]] "sDef" THEN
 175   consider "q such that" `q:triple = s n` [MESON_TAC[]]  "qDef" THEN
 176   HYP MESON_TAC "sDef qDef" [LE_0; reachableN; LT]] THEN SUBGOAL_TAC "Imp2"
 177   `!n. (? q. reachableN p q n  /\ move q p')  ==>  reachableN p p' (SUC n)`
 178   [INTRO_TAC "!n" THEN REWRITE_TAC[IMP_CONJ; LEFT_IMP_EXISTS_THM] THEN
 179   INTRO_TAC "!q; nReach; move_qp'" THEN
 180   consider "s such that"
 181   `s 0 = p /\ s n = q /\ !m. m < n ==> move (s m) (s (SUC m))`
 182   [HYP MESON_TAC "nReach" [reachableN; LT; LE_0]] "sDef" THEN
 183   REWRITE_TAC[reachableN; LT; LE_0] THEN
 184   EXISTS_TAC `\m. if m < SUC n then s m else p':triple` THEN
 185   HYP MESON_TAC "sDef move_qp'" [LT_0; LT_REFL; LT; LT_SUC]] THEN
 186   HYP MESON_TAC "0CLAUSE Imp1 Imp2" []);;
 187
 188 let reachableInvariant = prove
 189  (`!p p'. reachable p p'  ==>  oriented_area p = oriented_area p'`,
 190   SIMP_TAC[ReachLemma; LEFT_IMP_EXISTS_THM; SWAP_FORALL_THM] THEN
 191   INDUCT_TAC THEN ASM_MESON_TAC[reachableN_CLAUSES; moveInvariant]);;
 192
 193 let move2Cond = new_definition
 194   `! A B A' B':real^2. move2Cond A B A' B'  <=>
 195   ~collinear {B,A,A'} /\ ~collinear {A',B,B'}   \/
 196   ~collinear {A,B,B'} /\ ~collinear {B',A,A'}`;;
 197
 198 let reachableN_One = prove
 199  (`reachableN P0 P1 1 <=> move P0 P1`,
 200   MESON_TAC[ONE; reachableN; reachableN_CLAUSES]);;
 201
 202 let reachableN_Two = prove
 203  (`reachableN P0 P2 2 <=> ?P1. move P0 P1 /\ move P1 P2`,
 204   MESON_TAC[TWO; reachableN_One; reachableN_CLAUSES]);;
 205
 206 let reachableN_Three = prove
 207  (`reachableN P0 P3 3  <=>  ?P1 P2. move P0 P1 /\ move P1 P2 /\ move P2 P3`,
 208   MESON_TAC[ARITH_RULE `3 = SUC 2`; reachableN_Two; reachableN_CLAUSES]);;
 209
 210 let reachableN_Four = prove
 211  (`reachableN P0 P4 4  <=>  ?P1 P2 P3. move P0 P1 /\ move P1 P2 /\
 212   move P2 P3 /\ move P3 P4`,
 213   MESON_TAC[ARITH_RULE `4 = SUC 3`; reachableN_Three; reachableN_CLAUSES]);;
 214
 215 let reachableN_Five = prove
 216  (`reachableN P0 P5 5  <=>  ?P1 P2 P3 P4. move P0 P1 /\ move P1 P2 /\
 217   move P2 P3 /\ move P3 P4 /\ move P4 P5`,
 218   REWRITE_TAC[ARITH_RULE `5 = SUC 4`; reachableN_CLAUSES] THEN
 219   MESON_TAC[reachableN_Four]);;
 220
 221 let moveSymmetry = prove
 222  (`move (A,B,C) (A',B',C') ==>
 223   move (B,C,A) (B',C',A') /\ move (C,A,B) (C',A',B') /\
 224   move (A,C,B) (A',C',B') /\ move (B,A,C) (B',A',C') /\ move (C,B,A) (C',B',A')`,
 225   SUBGOAL_TAC "" `!A B C A':real^2. collinear {vec 0, C - B, A' - A}
 226   ==> collinear {vec 0, B - C, A' - A}`
 227   [REWRITE_TAC[COLLINEAR_3_2Dzero] THEN VEC2_TAC] THEN
 228   so (REWRITE_TAC[move]) THEN MESON_TAC[]);;
 229
 230 let reachableNSymmetry = prove
 231  (`! n. ! A B C A' B' C'. reachableN (A,B,C) (A',B',C') n  ==>
 232 reachableN (B,C,A) (B',C',A') n  /\  reachableN (C,A,B) (C',A',B') n /\
 233 reachableN (A,C,B) (A',C',B') n  /\  reachableN (B,A,C) (B',A',C') n /\
 234 reachableN (C,B,A) (C',B',A') n`,
 235   MATCH_MP_TAC num_INDUCTION THEN REWRITE_TAC[reachableN_CLAUSES] THEN
 236   SIMP_TAC[PAIR_EQ] THEN
 237   INTRO_TAC "!n;nStep; !A B C A' B' C'" THEN
 238   REWRITE_TAC[LEFT_IMP_EXISTS_THM; FORALL_PAIR_THM] THEN
 239   MAP_EVERY X_GEN_TAC [`X:real^2`; `Y:real^2`; `Z:real^2`] THEN
 240   INTRO_TAC "XYZexists" THEN
 241   REWRITE_TAC[RIGHT_AND_EXISTS_THM; LEFT_AND_EXISTS_THM] THEN
 242   MAP_EVERY EXISTS_TAC [`(Y,Z,X):triple`; `(Z,X,Y):triple`;
 243   `(X,Z,Y):triple`; `(Y,X,Z):triple`; `(Z,Y,X):triple`] THEN
 244   HYP SIMP_TAC "nStep XYZexists" [moveSymmetry]);;
 245
 246 let ORIENTED_AREA_COLLINEAR_CONG = prove
 247  (`! A B C A' B' C.
 248         oriented_area (A,B,C) = oriented_area (A',B',C')
 249         ==> (collinear {A,B,C} <=> collinear {A',B',C'})`,
 250   REWRITE_TAC[COLLINEAR_3_2D; oriented_area] THEN CONV_TAC REAL_RING);;
 251
 252 let Basic2move_THM = prove
 253  (`! A B C A'. ~collinear {A,B,C} /\ ~collinear {B,A,A'} ==>
 254   ?X. move (A,B,C) (A,B,X)  /\  move (A,B,X) (A',B,X)`,
 255   INTRO_TAC "!A B C A'; H1 H2" THEN SUBGOAL_TAC "add0vector_mul"
 256   `!r. r % ((A:real^2) - B) = (--r) % (B - A)  /\
 257   r % (A - B) = r % (A - B) + &0 % (C - B)` [VEC2_TAC] THEN
 258   SUBGOAL_TAC "H2'" `~ ? r. A' - (A:real^2) = r % (A - B)`
 259   [so (HYP MESON_TAC "H2" [COLLINEAR_3; COLLINEAR_LEMMA])] THEN
 260   consider "r t such that" `A' - (A:real^2) = r % (A - B) + t % (C - B)`
 261   [HYP MESON_TAC "H1" [COLLINEAR_3; Noncollinear_2Span]] "rExists" THEN
 262   SUBGOAL_TAC "tNonzero" `~(t = &0)`
 263   [so (HYP MESON_TAC "add0vector_mul H2'" [])] THEN
 264   consider "s X such that" `s = r / t  /\  X:real^2 = C + s % (A - B)`
 265   [HYP MESON_TAC "rExists" []] "Xexists" THEN
 266   SUBGOAL_TAC "" `A' - (A:real^2) = (t * s) % (A - B) + t % (C - B)`
 267   [so (HYP MESON_TAC "rExists tNonzero" [REAL_DIV_LMUL])] THEN SUBGOAL_TAC ""
 268   `A' - (A:real^2) = t % (X - B) /\ X - C = (-- s) % (B - (A:real^2))`
 269   [(so (HYP REWRITE_TAC "Xexists" [])) THEN VEC2_TAC] THEN SUBGOAL_TAC ""
 270   `collinear {vec 0,B - (A:real^2),X - C}  /\  collinear {vec 0,X - B,A' - A}`
 271   [so (HYP MESON_TAC "" [COLLINEAR_LEMMA])] THEN so (MESON_TAC [move]));;
 272
 273 let FourStepMoveAB = prove
 274  (`!A B C A' B'. ~collinear {A,B,C} ==>
 275   ~collinear {B,A,A'} /\ ~collinear {A',B,B'} ==>
 276   ? X Y. move (A,B,C) (A,B,X)  /\  move (A,B,X) (A',B,X)  /\
 277   move (A',B,X) (A',B,Y)  /\  move (A',B,Y) (A',B',Y)`,
 278   INTRO_TAC "!A B C A' B'; H1; H2" THEN
 279   consider "X such that" `move (A,B,C) (A,B,X)  /\  move (A,B,X) (A',B,X)`
 280   [HYP MESON_TAC "H1 H2" [Basic2move_THM]]"ABX" THEN
 281   SUBGOAL_TAC "" `~collinear {(A:real^2),B,X} /\ ~collinear {A',B,X}`
 282   [so (HYP MESON_TAC "H1" [moveInvariant; ORIENTED_AREA_COLLINEAR_CONG])]
 283   THEN SUBGOAL_TAC "" `~collinear {(B:real^2),A',X}`
 284   [so (MESON_TAC [collinearSymmetry])] THEN
 285   consider "Y such that" `move (B,A',X) (B,A',Y)  /\  move (B,A',Y) (B',A',Y)`
 286   [so (HYP MESON_TAC "H2" [Basic2move_THM])]  "BA'Y" THEN
 287   SUBGOAL_TAC "" `move (A',B,X) (A',B,Y)  /\  move (A',B,Y) (A',B',Y)`
 288   [HYP MESON_TAC "BA'Y" [moveSymmetry]] THEN so (HYP MESON_TAC "ABX" []));;
 289
 290 let FourStepMoveABBAreach = prove
 291  (`!A B C A' B'. ~collinear {A,B,C} /\ move2Cond A B A' B' ==>
 292   ? Y. reachableN (A,B,C) (A',B',Y) 4`,
 293   INTRO_TAC "!A B C A' B'; H1 H2" THEN
 294   cases "Case1 | Case2"
 295   `~collinear {B,(A:real^2),A'} /\ ~collinear {A',B,B'}  \/
 296   ~collinear {A,B,B'} /\ ~collinear {B',A,A'}`
 297   [HYP MESON_TAC "H2" [move2Cond]]
 298   THENL
 299   [so (HYP MESON_TAC "H1" [FourStepMoveAB; reachableN_Four]);
 300   SUBGOAL_TAC "" `~collinear {B,(A:real^2),C}`
 301   [HYP MESON_TAC "H1" [collinearSymmetry]]] THEN
 302   SUBGOAL_TAC "" `~collinear {B,(A:real^2),C}`
 303   [HYP MESON_TAC "H1" [collinearSymmetry]] THEN
 304   consider "X Y such that"
 305   `move (B,A,C) (B,A,X)  /\  move (B,A,X) (B',A,X)  /\
 306   move (B',A,X) (B',A,Y)  /\  move (B',A,Y) (B',A',Y)`
 307   [so (HYP MESON_TAC "Case2" [FourStepMoveAB])] "BAX" THEN
 308   HYP MESON_TAC "BAX" [moveSymmetry; reachableN_Four]);;
 309
 310 let NotMove2ImpliesCollinear = prove
 311  (`!A B C A' B' C'. ~collinear {A,B,C} /\ ~collinear {A',B',C'} /\
 312   ~(A = A') /\ ~(B = B') /\ ~move2Cond A B A' B' ==>
 313   collinear {A,B,A',B'}`,
 314   INTRO_TAC "!A B C A' B' C'; H1 H1' H2 H2' H3" THEN
 315   SUBGOAL_TAC "Distinct" `~((A:real^2) = B) /\ ~((A':real^2) = B')`
 316   [HYP MESON_TAC "H1 H1'" [Noncollinear_3ImpliesDistinct]] THEN
 317   SUBGOAL_TAC "set4symmetry" `{(A:real^2),B,A',B'} SUBSET {A,A',B,B'}  /\
 318   {A,B,A',B'} SUBSET {B,B',A',A}  /\  {A,B,A',B'} SUBSET {A',B',B,A}` [SET_TAC[]] THEN
 319   cases "Case1 | Case2 | Case3 | Case4"
 320   `collinear {B,(A:real^2),A'} /\ collinear {A,B,B'}  \/
 321   collinear {B,A,A'} /\ collinear {B',A,A'}  \/
 322   collinear {A',B,B'} /\ collinear {A,B,B'}  \/
 323   collinear {A',B,B'} /\ collinear {B',A,A'}`
 324   [HYP MESON_TAC "H3" [move2Cond]] THEN
 325   so (HYP MESON_TAC "Distinct H2 H2' set4symmetry"
 326   [collinearSymmetry; COLLINEAR_4_3; COLLINEAR_SUBSET]));;
 327
 328 let DistinctImplies2moveable = prove
 329  (`!A B C A' B' C'. ~collinear {A,B,C} /\ ~collinear {A',B',C'} /\
 330   ~(A = A') /\ ~(B = B') /\ ~(C = C')  ==>
 331   move2Cond A B A' B' \/ move2Cond B C B' C'`,
 332   INTRO_TAC "!A B C A' B' C'; H1 H1' H2a H2b H2c" THEN SUBGOAL_TAC "3subset4"
 333   `{(A:real^2),B,B'} SUBSET {A,B,A',B'} /\ {B,B',C} SUBSET {B,C,B',C'}`
 334   [SET_TAC[]] THEN
 335   raa "Con" `~move2Cond A B A' B'  /\
 336   ~move2Cond B C B' C'` (HYP MESON_TAC "Con" []) THEN
 337   SUBGOAL_TAC "" `collinear {(A:real^2),B,A',B'} /\ collinear {B,C,B',C'}`
 338   [so (HYP MESON_TAC "H1 H1' H2a H2b H2c" [collinearSymmetry; NotMove2ImpliesCollinear])]
 339   THEN SUBGOAL_TAC "" `collinear {(A:real^2),B,C}`
 340   [so (HYP MESON_TAC "3subset4 H2a H2b H2c" [COLLINEAR_SUBSET; COLLINEAR_3_TRANS])]
 341   THEN so (HYP MESON_TAC "H1 H1'" []));;
 342
 343 let SameCdiffAB = prove
 344  (`!A B C A' B' C'.  ~collinear {A,B,C} /\ ~collinear {A',B',C'} ==>
 345  C = C' /\ ~(A = A') /\ ~(B = B') ==>
 346   ? Y. reachableN (A,B,C) (Y,B',C') 2  \/ reachableN (A,B,C) (A',B',Y) 4`,
 347   INTRO_TAC "!A B C A' B' C'; H1; H2" THEN SUBGOAL_TAC "easy_set"
 348   `{B,B',(A:real^2)} SUBSET {A,B,A',B'}  /\  {A,B,C} SUBSET {B,B',A,C}` [SET_TAC[]]  THEN
 349   cases "Ncol | move | col_Nmove"
 350   `~collinear {C,B,B'}  \/
 351   move2Cond A B A' B'  \/
 352   collinear {C,B,B'} /\ ~move2Cond A B A' B'`
 353   [MESON_TAC[]] THENL
 354   [consider "X such that" `move (B,C,A) (B,C,X) /\ move (B,C,X) (B',C',X)`
 355   [so (HYP MESON_TAC "easy_set H1 H2" [collinearSymmetry; Basic2move_THM])] "BCX"
 356   THEN HYP MESON_TAC "BCX" [reachableN_Two; reachableNSymmetry];
 357   so (HYP MESON_TAC "H1" [FourStepMoveABBAreach]);
 358   SUBGOAL_TAC "" `collinear {(B:real^2),B',A} /\ collinear {B,B',C}`
 359   [so (HYP MESON_TAC "H1 H2 easy_set"
 360   [NotMove2ImpliesCollinear; COLLINEAR_SUBSET; collinearSymmetry])]  THEN
 361   so (HYP MESON_TAC "H2 easy_set H1" [COLLINEAR_4_3; COLLINEAR_SUBSET])]);;
 362
 363 let FourMovesToCorrectTwo = prove
 364  (`!A B C A' B' C'. ~collinear {A,B,C} /\ ~collinear {A',B',C'} ==>
 365   ? n. n < 5 /\ ? Y. reachableN (A,B,C) (A',B',Y) n  \/
 366   reachableN (A,B,C) (A',Y,C') n  \/ reachableN (A,B,C) (Y,B',C') n`,
 367   INTRO_TAC "!A B C A' B' C'; H1" THEN
 368   SUBGOAL_TAC "H1'" `~collinear {B,C,(A:real^2)} /\
 369   ~collinear{B',C',(A':real^2)} /\ ~collinear {C,A,B} /\ ~collinear {C',A',B'}`
 370   [HYP MESON_TAC "H1" [collinearSymmetry]]   THEN
 371   SUBGOAL_TAC "easy_arith" `0 < 5 /\ 2 < 5 /\ 3 < 5 /\ 4 < 5` [ARITH_TAC] THEN
 372   cases "case01 | case2 | case3"
 373   `((A:real^2) = A' /\ (B:real^2) = B' /\ (C:real^2) = C'  \/
 374   A = A' /\ B = B' /\ ~(C = C')  \/  A = A' /\ ~(B = B') /\ C = C' \/
 375   ~(A = A') /\ B = B' /\ C = C')  \/
 376   (A = A' /\ ~(B = B') /\ ~(C = C')  \/
 377   ~(A = A') /\ B = B' /\ ~(C = C')  \/  ~(A = A') /\ ~(B = B') /\ C = C')  \/
 378   ~(A = A') /\ ~(B = B') /\ ~(C = C')`
 379   [MESON_TAC []] THENL
 380   [so (HYP MESON_TAC "easy_arith" [reachableN_CLAUSES]);
 381   so (HYP MESON_TAC "H1 H1' easy_arith" [SameCdiffAB; reachableNSymmetry]);
 382   EXISTS_TAC `4` THEN HYP SIMP_TAC "easy_arith" [] THEN
 383   so (HYP MESON_TAC "H1  H1'" [DistinctImplies2moveable; FourStepMoveABBAreach;
 384   reachableNSymmetry; reachableN_Four])]);;
 385
 386 let CorrectFinalPoint = prove
 387  (`oriented_area (A,B,C) = oriented_area (A,B,C') ==>
 388   move (A,B,C) (A,B,C')`,
 389   REWRITE_TAC [move; oriented_area; COLLINEAR_3_2Dzero]  THEN VEC2_TAC);;
 390
 391 let FiveMovesOrLess = prove
 392  (`!A B C A' B' C'. ~collinear {A,B,C} ==>
 393   oriented_area (A,B,C) = oriented_area (A',B',C') ==>
 394   ? n. n <= 5 /\ reachableN (A,B,C) (A',B',C') n`,
 395   INTRO_TAC "!A B C A' B' C'; H1; H2"  THEN
 396   SUBGOAL_TAC "H1'" `~collinear {(A':real^2),B',C'}`
 397   [HYP MESON_TAC "H1 H2" [ORIENTED_AREA_COLLINEAR_CONG]]  THEN
 398   SUBGOAL_TAC "Distinct" `~((A:real^2) = B) /\ ~(A = C) /\ ~(B = C) /\
 399   ~((A':real^2) = B') /\ ~(A' = C') /\ ~(B' = C')`
 400   [so (HYP MESON_TAC "H1" [Noncollinear_3ImpliesDistinct])]  THEN
 401   consider "n Y such that"
 402   `n < 5 /\ (reachableN (A,B,C) (A',B',Y) n \/
 403   reachableN (A,B,C) (A',Y,C') n \/ reachableN (A,B,C) (Y,B',C') n)`
 404   [HYP MESON_TAC "H1 H1'" [FourMovesToCorrectTwo]] "2Correct" THEN
 405   cases "A'B'Y | A'YC' | YB'C'"
 406   `reachableN (A,B,C) (A',B',Y) n  \/
 407   reachableN (A,B,C) (A',Y,C') n  \/
 408   reachableN (A,B,C) (Y,B',C') n` [HYP MESON_TAC "2Correct" []] THENL
 409   [SUBGOAL_TAC "" `oriented_area (A',B',Y) = oriented_area (A',B',C')`
 410   [so (HYP MESON_TAC "H2" [ReachLemma; reachableInvariant])]  THEN
 411   SUBGOAL_TAC "" `move (A',B',Y) (A',B',C')`
 412   [so (HYP MESON_TAC "Distinct" [CorrectFinalPoint])]  THEN
 413   so (HYP MESON_TAC "A'B'Y 2Correct" [reachableN_CLAUSES; LE_SUC_LT]);
 414   SUBGOAL_TAC "" `oriented_area (A',C',Y) = oriented_area (A',C',B')`
 415   [so (HYP MESON_TAC "H2" [ReachLemma; reachableInvariant; oriented_areaSymmetry])]
 416   THEN SUBGOAL_TAC "" `move (A',Y,C') (A',B',C')`
 417   [so (HYP MESON_TAC "Distinct" [CorrectFinalPoint; moveSymmetry])]  THEN
 418   so (HYP MESON_TAC "A'YC' 2Correct" [reachableN_CLAUSES; LE_SUC_LT]);
 419 SUBGOAL_TAC "" `oriented_area (B',C',Y) = oriented_area (B',C',A')`
 420   [so (HYP MESON_TAC "H2" [ReachLemma; reachableInvariant; oriented_areaSymmetry])]
 421   THEN SUBGOAL_TAC "" `move (Y,B',C') (A',B',C')`
 422   [so (HYP MESON_TAC "Distinct" [CorrectFinalPoint; moveSymmetry])]  THEN
 423   so (HYP MESON_TAC "YB'C' 2Correct" [reachableN_CLAUSES; LE_SUC_LT])]);;
 424
 425 let NOTENOUGH_4 = prove
 426  (`?p0 p4. oriented_area p0 = oriented_area p4 /\ ~reachableN p0 p4 4`,
 427   consider "p0 p4 such that"
 428   `p0:triple = vector [&0;&0],vector [&0;&1],vector [&1;&0]  /\
 429   p4:triple = vector [&1;&1],vector [&1;&2],vector [&2;&1]`
 430   [MESON_TAC []] "p04Def" THEN
 431   SUBGOAL_TAC "equal_areas" `oriented_area p0 = oriented_area p4`
 432   [HYP REWRITE_TAC "p04Def" [oriented_area] THEN VEC2_TAC] THEN
 433   SUBGOAL_TAC "" `~reachableN p0 p4 4`
 434   [HYP REWRITE_TAC "p04Def" [reachableN_Four; NOT_EXISTS_THM; FORALL_PAIR_THM;  move; COLLINEAR_3_2Dzero; FORALL_VECTOR_2] THEN VEC2_TAC] THEN
 435   so (HYP MESON_TAC "equal_areas" []));;
 436
 437 let FiveMovesOrLess_STRONG = prove
 438  (`!A B C A' B' C'.
 439   oriented_area (A,B,C) = oriented_area (A',B',C') ==>
 440   ?n. n <= 5 /\ reachableN (A,B,C) (A',B',C') n`,
 441   INTRO_TAC "!A B C A' B' C'; H1" THEN
 442   SUBGOAL_TAC "EZcollinear"
 443   `(!X Y:real^2. collinear {X,Y,Y}) /\
 444   (!A B A'. move (A,B,B) (A',B,B))  /\
 445   !A B C B'. (collinear {A,B,C} /\ collinear {A,B',C}  ==>
 446   move (A,B,C) (A,B',C))`
 447   [REWRITE_TAC[move; COLLINEAR_3_2D] THEN VEC2_TAC] THEN
 448   cases "ABCncol | ABCcol"
 449   `~collinear {(A:real^2),B,C}  \/  collinear {A,B,C}`
 450   [MESON_TAC []] THENL
 451   [so (HYP MESON_TAC "H1" [FiveMovesOrLess]);
 452   SUBGOAL_TAC "A'B'C'col" `collinear {(A':real^2),B',C'}`
 453   [so (HYP MESON_TAC "H1" [ORIENTED_AREA_COLLINEAR_CONG])] THEN
 454   consider "P1 P2 P3 P4 such that"
 455   `P1:triple = A,C,C  /\  P2:triple = B',C,C  /\  P3 = B',B',C  /\
 456   P4:triple = B',B',C'` [MESON_TAC []] "P1234exist" THEN
 457   SUBGOAL_TAC "" `move (A,B,C) (P1:triple)  /\  move P1 P2  /\
 458   move P2 P3  /\  move P3 P4  /\  move P4 (A',B',C')`
 459   [HYP MESON_TAC "ABCcol A'B'C'col EZcollinear P1234exist"
 460   [collinearSymmetry; moveSymmetry]] THEN
 461   so (MESON_TAC [reachableN_Five; LE_REFL])]);;