(* ------------------------------------------------------------------------- *) (* Three bugs are crawling on the coordinate plane. They move *) (* one at a time, and each bug will only crawl in a direction *) (* parallel to the line joining the other two. *) (* *) (* (a) If the bugs start out at (0,0), (3,0), and (0,3), is it *) (* possible that after some time the first bug will end up *) (* back where it started, while the other two bugs switch *) (* places? *) (* *) (* (b) Can the bugs end up at (1,2), (2,5), and (-2,3)? *) (* ------------------------------------------------------------------------- *) prioritize_real();; let move = new_definition `move ((ax,ay),(bx,by),(cx,cy)) ((ax',ay'),(bx',by'),(cx',cy')) <=> (?a. ax' = ax + a * (cx - bx) /\ ay' = ay + a * (cy - by) /\ bx' = bx /\ by' = by /\ cx' = cx /\ cy' = cy) \/ (?b. bx' = bx + b * (ax - cx) /\ by' = by + b * (ay - cy) /\ ax' = ax /\ ay' = ay /\ cx' = cx /\ cy' = cy) \/ (?c. ax' = ax /\ ay' = ay /\ bx' = bx /\ by' = by /\ cx' = cx + c * (bx - ax) /\ cy' = cy + c * (by - ay))`;; let reachable_RULES,reachable_INDUCT,reachable_CASES = new_inductive_definition `(!p. reachable p p) /\ (!p q r. move p q /\ reachable q r ==> reachable p r)`;; let oriented_area = new_definition `oriented_area ((ax,ay),(bx,by),(cx,cy)) = ((bx - ax) * (cy - ay) - (cx - ax) * (by - ay)) / &2`;; let MOVE_INVARIANT = prove (`!p p'. move p p' ==> oriented_area p = oriented_area p'`, REWRITE_TAC[FORALL_PAIR_THM; move; oriented_area] THEN CONV_TAC REAL_RING);; let REACHABLE_INVARIANT = prove (`!p p'. reachable p p' ==> oriented_area p = oriented_area p'`, MATCH_MP_TAC reachable_INDUCT THEN MESON_TAC[MOVE_INVARIANT]);; let IMPOSSIBILITY_B = prove (`~(reachable ((&0,&0),(&3,&0),(&0,&3)) ((&1,&2),(&2,&5),(-- &2,&3)) \/ reachable ((&0,&0),(&3,&0),(&0,&3)) ((&1,&2),(-- &2,&3),(&2,&5)) \/ reachable ((&0,&0),(&3,&0),(&0,&3)) ((&2,&5),(&1,&2),(-- &2,&3)) \/ reachable ((&0,&0),(&3,&0),(&0,&3)) ((&2,&5),(-- &2,&3),(&1,&2)) \/ reachable ((&0,&0),(&3,&0),(&0,&3)) ((-- &2,&3),(&1,&2),(&2,&5)) \/ reachable ((&0,&0),(&3,&0),(&0,&3)) ((-- &2,&3),(&2,&5),(&1,&2)))`, STRIP_TAC THEN FIRST_ASSUM(MP_TAC o MATCH_MP REACHABLE_INVARIANT) THEN REWRITE_TAC[oriented_area] THEN REAL_ARITH_TAC);;