(* ========================================================================= *)
(* (c) Copyright, Bill Richter 2013 *)
(* Distributed under the same license as HOL Light *)
(* *)
(* Proof of the Bug Puzzle conjecture of the HOL Light tutorial: *)
(* Any two triples with the same oriented area can be connected in *)
(* 5 moves or less (FiveMovesOrLess). Also a proof that 4 moves is not *)
(* enough, with an explicit counterexample. This result (NOTENOUGH_4) *)
(* is due to John Harrison, as is much of the basic vector code, and *)
(* the definition of move, which defines a closed subset *)
(* {(A,B,C,A',B',C') | move (A,B,C) (A',B',C')} subset R^6 x R^6 *)
(* and also a result FiveMovesOrLess_STRONG that handles the degenerate *)
(* case (the two triples not required to be non-collinear), which has a *)
(* very satisfying answer using this "closed" definition of move. *)
(* *)
(* The mathematical proofs are essentially due to Tom Hales. The *)
(* code is all in miz3, and was an attempt to explore Freek Wiedijk's *)
(* vision of mixing the procedural and declarative proof styles. *)
(* ========================================================================= *)
needs "Multivariate/determinants.ml";;
#load "unix.cma";;
loadt "miz3/miz3.ml";;
new_type_abbrev("triple",`:real^2#real^2#real^2`);;
default_prover := ("ya prover",
fun thl -> REWRITE_TAC thl THEN CONV_TAC (HOL_BY thl));;
horizon := 0;;
timeout := 500;;
let VEC2_TAC =
SIMP_TAC[CART_EQ; LAMBDA_BETA; FORALL_2; SUM_2; DIMINDEX_2; VECTOR_2;
vector_add; vec; dot; orthogonal; basis;
vector_neg; vector_sub; vector_mul; ARITH] THEN
CONV_TAC REAL_RING;;
let COLLINEAR_3_2Dzero = thm `;
!y z:real^2. collinear{vec 0,y,z} <=>
z$1 * y$2 = y$1 * z$2
by REWRITE_TAC[COLLINEAR_3_2D] THEN VEC2_TAC;
`;;
let Noncollinear_3ImpliesDistinct = thm `;
!a b c:real^N. ~collinear {a,b,c} ==> ~(a = b) /\ ~(a = c) /\ ~(b = c)
by COLLINEAR_BETWEEN_CASES, BETWEEN_REFL;
`;;
let collinearSymmetry = thm `;
let A B C be real^N;
thus collinear {A,B,C} ==> collinear {A,C,B} /\ collinear {B,A,C} /\
collinear {B,C,A} /\ collinear {C,A,B} /\ collinear {C,B,A}
proof
{A,C,B} SUBSET {A,B,C} /\ {B,A,C} SUBSET {A,B,C} /\ {B,C,A} SUBSET {A,B,C} /\
{C,A,B} SUBSET {A,B,C} /\ {C,B,A} SUBSET {A,B,C} by SET_RULE;
qed by -, COLLINEAR_SUBSET;
`;;
let Noncollinear_2Span = thm `;
let u v w be real^2;
assume ~collinear {vec 0,v,w} [H1];
thus ? s t. s % v + t % w = u
proof
!n r. ~(r < n) /\ r <= MIN n n ==> r = n [easy_arith] by ARITH_RULE;
~(w$1 * v$2 = v$1 * w$2) [H1'] by H1, COLLINEAR_3_2Dzero;
consider M such that
M = transp(vector[v;w]):real^2^2 [Mexists];
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;
~(det M = &0) by -, H1', REAL_ARITH;
consider x s t such that
M ** x = u /\ s = x$1 /\ t = x$2 by -, easy_arith, DET_EQ_0_RANK, RANK_BOUND, MATRIX_FULL_LINEAR_EQUATIONS;
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[];
s % v + t % w = u by -, REAL_MUL_SYM, VECTOR_MUL_COMPONENT, VECTOR_ADD_COMPONENT, VEC2_TAC;
qed by -;
`;;
let oriented_areaSymmetry = thm `;
!A B C A' B' C':real^2.
oriented_area (A,B,C) = oriented_area(A',B',C') ==>
oriented_area (B,C,A) = oriented_area (B',C',A') /\
oriented_area (C,A,B) = oriented_area (C',A',B') /\
oriented_area (A,C,B) = oriented_area (A',C',B') /\
oriented_area (B,A,C) = oriented_area (B',A',C') /\
oriented_area (C,B,A) = oriented_area (C',B',A')
by REWRITE_TAC[oriented_area] THEN VEC2_TAC;
`;;
let move = new_definition
`!A B C A' B' C':real^2. move (A,B,C) (A',B',C') <=>
(B = B' /\ C = C' /\ collinear {vec 0,C - B,A' - A} \/
A = A' /\ C = C' /\ collinear {vec 0,C - A,B' - B} \/
A = A' /\ B = B' /\ collinear {vec 0,B - A,C' - C})`;;let reachable = new_definition
`!p p'.
reachable p p' <=> ?n. ?s.
s 0 = p /\ s n = p' /\
(!m. 0 <= m /\ m < n ==> move (s m) (s (SUC m)))`;;
let move2Cond = new_definition
`move2Cond (A,B,C) (A',B',C') <=>
~collinear {B,A,A'} /\ ~collinear {A',B,B'} \/
~collinear {A,B,B'} /\ ~collinear {B',A,A'}`;;