(* ========================================================================= *)
(* (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 of points in the plane with the same oriented area can be *)
(* connected in 5 moves or less (FivemovesOrLess). Much of the code is *)
(* due to John Harrison: a proof (NOTENOUGH_4) showing this is the best *)
(* possible result; an early version of Noncollinear_2Span; the *)
(* definition of move, which defines a closed subset *)
(* {(A,B,C,A',B',C') | move (A,B,C) (A',B',C')} of R^6 x R^6, *)
(* i.e. the zero set of a continuous function; FivemovesOrLess_STRONG, *)
(* which handles the degenerate case (collinear or non-distinct triples), *)
(* giving a satisfying answer using this "closed" definition of move. *)
(* *)
(* The mathematical proofs are essentially due to Tom Hales. The code *)
(* tries to mix declarative and procedural proof styles, using ideas due *)
(* to John Harrison (section 12.1 "Towards more readable proofs" of the *)
(* HOL Light tutorial), Freek Wiedijk (arxiv.org/pdf/1201.3601 "A *)
(* Synthesis of the Procedural and Declarative Styles of Interactive *)
(* Theorem Proving"), Marco Maggesi, who wrote the tactic constructs *)
(* INTRO_TAC & HYP, which goes well with the older SUBGOAL_TAC, and Petros *)
(* Papapanagiotou, coauthor of IsabelleLight, who wrote BuildExist below, a *)
(* a crucial part of consider. *)
(* ========================================================================= *)
needs "Multivariate/determinants.ml";;
new_type_abbrev("triple",`:real^2#real^2#real^2`);;
let so = fun tac -> FIRST_ASSUM MP_TAC THEN tac;;
let BuildExist x t =
let try_type tp tm =
try inst (type_match (type_of tm) tp []) tm
with Failure _ -> tm in
(* Check if two variables match allowing only type instantiations: *)
let vars_match tm1 tm2 =
let inst = try term_match [] tm1 tm2 with Failure _ -> [],[tm2,tm1],[] in
match inst with
[],[],_ -> tm2
| _ -> failwith "vars_match: no match" in
(* Find the type of a matching variable in t. *)
let tp = try type_of (tryfind (vars_match x) (frees t))
with Failure _ ->
warn true ("BuildExist: `" ^ string_of_term x ^ "` not be found in
`" ^ string_of_term t ^ "`") ;
type_of x in
(* Try to force x to type tp. *)
let x' = try_type tp x in
mk_exists (x',t);;
let consider vars_SuchThat t prfs lab =
(* Functions ident and parse_using borrowed from HYP in tactics.ml *)
let ident = function
Ident s::rest when isalnum s -> s,rest
| _ -> raise Noparse in
let parse_using = many ident in
let rec findSuchThat = function
n -> if String.sub vars_SuchThat n 9 = "such that" then n
else findSuchThat (n + 1) in
let n = findSuchThat 1 in
let vars = String.sub vars_SuchThat 0 (n - 1) in
let xl = map parse_term ((fst o parse_using o lex o explode) vars) in
let tm = itlist BuildExist xl t in
match prfs with
p::ps -> (warn (ps <> []) "consider: additional subproofs ignored";
SUBGOAL_THEN tm (DESTRUCT_TAC ("@" ^ vars ^ "." ^ lab))
THENL [p; ALL_TAC])
| [] -> failwith "consider: no subproof given";;
let cases sDestruct disjthm tac =
SUBGOAL_TAC "" disjthm tac THEN FIRST_X_ASSUM
(DESTRUCT_TAC sDestruct);;
let raa lab t tac = SUBGOAL_THEN (mk_imp(t, `F`)) (LABEL_TAC lab) THENL
[INTRO_TAC lab; tac];;
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 collinearSymmetry = prove
(`collinear {A,B,C}
==> collinear {A,C,B} /\ collinear {B,A,C} /\
collinear {B,C,A} /\ collinear {C,A,B} /\ collinear {C,B,A}`,
MESON_TAC[SET_RULE `{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}`;
COLLINEAR_SUBSET]);;
let oriented_areaSymmetry = prove
(`
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')`,
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 reachableN_CLAUSES = prove
(`! p p'. (reachableN p p' 0 <=> p = p') /\
! n. reachableN p p' (SUC n) <=> ? q. reachableN p q n /\ move q p'`,
INTRO_TAC "!p p'" THEN
consider "s0 such that" `s0 = \m:num. p':triple` [MESON_TAC[]] "s0exists" THEN
SUBGOAL_TAC "0CLAUSE" `reachableN p p' 0 <=> p = p'`
[HYP MESON_TAC "s0exists" [
LE_0; reachableN;
LT]] THEN SUBGOAL_TAC "Imp1"
`! n. reachableN p p' (SUC n) ==> ? q. reachableN p q n /\ move q p'`
[INTRO_TAC "!n; H1" THEN
consider "s such that"
`s 0 = p /\ s (SUC n) = p' /\ !m. m < SUC n ==> move (s m) (s (SUC m))`
[HYP MESON_TAC "H1" [
LE_0; reachableN]] "sDef" THEN
consider "q such that" `q:triple = s n` [MESON_TAC[]] "qDef" THEN
HYP MESON_TAC "sDef qDef" [
LE_0; reachableN;
LT]] THEN SUBGOAL_TAC "Imp2"
`!n. (? q. reachableN p q n /\ move q p') ==> reachableN p p' (SUC n)`
[INTRO_TAC "!n" THEN REWRITE_TAC[
IMP_CONJ;
LEFT_IMP_EXISTS_THM] THEN
INTRO_TAC "!q; nReach; move_qp'" THEN
consider "s such that"
`s 0 = p /\ s n = q /\ !m. m < n ==> move (s m) (s (SUC m))`
[HYP MESON_TAC "nReach" [reachableN;
LT;
LE_0]] "sDef" THEN
REWRITE_TAC[reachableN;
LT;
LE_0] THEN
EXISTS_TAC `\m. if m < SUC n then s m else p':triple` THEN
HYP MESON_TAC "sDef move_qp'" [
LT_0;
LT_REFL;
LT;
LT_SUC]] THEN
HYP MESON_TAC "0CLAUSE Imp1 Imp2" []);;
let move2Cond = new_definition
`! A B A' B':real^2. move2Cond A B A' B' <=>
~collinear {B,A,A'} /\ ~collinear {A',B,B'} \/
~collinear {A,B,B'} /\ ~collinear {B',A,A'}`;;let reachableN_Four = prove
(`reachableN P0 P4 4 <=> ?P1 P2 P3. move P0 P1 /\ move P1 P2 /\
move P2 P3 /\ move P3 P4`,
let reachableN_Five = prove
(`reachableN P0 P5 5 <=> ?P1 P2 P3 P4. move P0 P1 /\ move P1 P2 /\
move P2 P3 /\ move P3 P4 /\ move P4 P5`,
let moveSymmetry = prove
(`move (A,B,C) (A',B',C') ==>
move (B,C,A) (B',C',A') /\ move (C,A,B) (C',A',B') /\
move (A,C,B) (A',C',B') /\ move (B,A,C) (B',A',C') /\ move (C,B,A) (C',B',A')`,
SUBGOAL_TAC "" `!A B C A':real^2. collinear {vec 0, C - B, A' - A}
==> collinear {vec 0, B - C, A' - A}`
[REWRITE_TAC[
COLLINEAR_3_2Dzero] THEN VEC2_TAC] THEN
so (REWRITE_TAC[move]) THEN MESON_TAC[]);;
let reachableNSymmetry = prove
(`! n. ! A B C A' B' C'. reachableN (A,B,C) (A',B',C') n ==>
reachableN (B,C,A) (B',C',A') n /\ reachableN (C,A,B) (C',A',B') n /\
reachableN (A,C,B) (A',C',B') n /\ reachableN (B,A,C) (B',A',C') n /\
reachableN (C,B,A) (C',B',A') n`,
MATCH_MP_TAC
num_INDUCTION THEN REWRITE_TAC[
reachableN_CLAUSES] THEN
SIMP_TAC[
PAIR_EQ] THEN
INTRO_TAC "!n;nStep; !A B C A' B' C'" THEN
REWRITE_TAC[
LEFT_IMP_EXISTS_THM;
FORALL_PAIR_THM] THEN
MAP_EVERY X_GEN_TAC [`X:real^2`; `Y:real^2`; `Z:real^2`] THEN
INTRO_TAC "XYZexists" THEN
REWRITE_TAC[
RIGHT_AND_EXISTS_THM;
LEFT_AND_EXISTS_THM] THEN
MAP_EVERY EXISTS_TAC [`(Y,Z,X):triple`; `(Z,X,Y):triple`;
`(X,Z,Y):triple`; `(Y,X,Z):triple`; `(Z,Y,X):triple`] THEN
HYP SIMP_TAC "nStep XYZexists" [moveSymmetry]);;
let Basic2move_THM = prove
(`! A B C A'. ~collinear {A,B,C} /\ ~collinear {B,A,A'} ==>
?X. move (A,B,C) (A,B,X) /\ move (A,B,X) (A',B,X)`,
INTRO_TAC "!A B C A';
let FourStepMoveAB = prove
(`!A B C A' B'. ~collinear {A,B,C} ==>
~collinear {B,A,A'} /\ ~collinear {A',B,B'} ==>
? X Y. move (A,B,C) (A,B,X) /\ move (A,B,X) (A',B,X) /\
move (A',B,X) (A',B,Y) /\ move (A',B,Y) (A',B',Y)`,
INTRO_TAC "!A B C A' B';
let FourStepMoveABBAreach = prove
(`!A B C A' B'. ~collinear {A,B,C} /\ move2Cond A B A' B' ==>
? Y. reachableN (A,B,C) (A',B',Y) 4`,
INTRO_TAC "!A B C A' B';
let NotMove2ImpliesCollinear = prove
(`!A B C A' B' C'. ~collinear {A,B,C} /\ ~collinear {A',B',C'} /\
~(A = A') /\ ~(B = B') /\ ~move2Cond A B A' B' ==>
collinear {A,B,A',B'}`,
INTRO_TAC "!A B C A' B' C';
let DistinctImplies2moveable = prove
(`!A B C A' B' C'. ~collinear {A,B,C} /\ ~collinear {A',B',C'} /\
~(A = A') /\ ~(B = B') /\ ~(C = C') ==>
move2Cond A B A' B' \/ move2Cond B C B' C'`,
INTRO_TAC "!A B C A' B' C';
let SameCdiffAB = prove
(`!A B C A' B' C'. ~collinear {A,B,C} /\ ~collinear {A',B',C'} ==>
C = C' /\ ~(A = A') /\ ~(B = B') ==>
? Y. reachableN (A,B,C) (Y,B',C') 2 \/ reachableN (A,B,C) (A',B',Y) 4`,
INTRO_TAC "!A B C A' B' C';
let FourMovesToCorrectTwo = prove
(`!A B C A' B' C'. ~collinear {A,B,C} /\ ~collinear {A',B',C'} ==>
? n. n < 5 /\ ? Y. reachableN (A,B,C) (A',B',Y) n \/
reachableN (A,B,C) (A',Y,C') n \/ reachableN (A,B,C) (Y,B',C') n`,
INTRO_TAC "!A B C A' B' C';
let FiveMovesOrLess = prove
(`!A B C A' B' C'. ~collinear {A,B,C} ==>
oriented_area (A,B,C) =
oriented_area (A',B',C') ==>
? n. n <= 5 /\ reachableN (A,B,C) (A',B',C') n`,
INTRO_TAC "!A B C A' B' C';