Inductive Bit : Set :=
H | V
| TL | TR
| BL | BR.
Definition State :=
(Bit * Bit * Bit *
Bit * Bit *
Bit * Bit * Bit)%type.
Inductive Move : State -> State -> Set :=
| refl : forall S, Move S S
| top_left : forall A B C D E F G H, Move
(A, B, C,
D, E,
F, G, H)
(B, C, A,
D, E,
F, G, H)
| left_down : forall A B C D E F G H, Move
(A, B, C,
D, E,
F, G, H)
(F, B, C,
A, E,
D, G, H)
| right_down : forall A B C D E F G H, Move
(A, B, C,
D, E,
F, G, H)
(A, B, H,
D, C,
F, G, E)
| bottom_left : forall A B C D E F G H, Move
(A, B, C,
D, E,
F, G, H)
(A, B, C,
D, E,
G, H, F)
| trans_closure : forall A M Z,
Move A M -> Move M Z -> Move A Z.
Definition solution state := Move state (TL, H, TR,
V, V,
BL, H, BR).
Theorem prolog_example :
solution (H, BR, BL,
H, TL,
TR, V, V).
unfold solution.
eapply trans_closure.
apply top_left.
change (solution (BR, BL, H, H, TL, TR, V, V)).
Ltac whack direction :=
unfold solution;
eapply trans_closure;
[ apply direction
| match goal with
| |- Move ?x _ => change (solution x)
end
].
Ltac wtop := whack top_left.
Ltac wleft := whack left_down.
Ltac wright := whack right_down.
Ltac wbottom := whack bottom_left.
wtop.
wtop.
wtop.
wtop.
wbottom.
wbottom.
wleft.
wright.
wbottom.
wbottom.
wleft.
wright.
unfold solution.
apply refl.
Qed.
Theorem automated_example :
solution (H, BR, BL,
H, TL,
TR, V, V).
Inductive Marker (A : State) : Set := mkMarker.
Ltac save_state :=
match goal with
| |- solution ?state =>
let seen := fresh "seen"
in pose (seen := mkMarker state)
end.
Ltac check_progress :=
match goal with
| |- solution ?State =>
match goal with
| _ : Marker State |- _ =>
pose (dead_end := True)
| _ => idtac
end
end.
Ltac swtop := save_state; whack top_left; check_progress.
Ltac swleft := save_state; whack left_down; check_progress.
Ltac swright := save_state; whack right_down; check_progress.
Ltac swbottom := save_state; whack bottom_left; check_progress.
Ltac swhack n :=
(unfold solution; apply refl) ||
match n with
| 0 => fail
| S ?m => swtop; pose (dead_end := False); clear dead_end; swhack m
| S ?m => swleft; pose (dead_end := False); clear dead_end; swhack m
| S ?m => swright; pose (dead_end := False); clear dead_end; swhack m
| S ?m => swbottom; pose (dead_end := False); clear dead_end; swhack m
end.
swhack 12.
Defined.
Print automated_example.
(*
automated_example =
let seen := mkMarker (H, BR, BL, H, TL, TR, V, V) in
trans_closure (H, BR, BL, H, TL, TR, V, V) (BR, BL, H, H, TL, TR, V, V)
(TL, H, TR, V, V, BL, H, BR) (top_left H BR BL H TL TR V V)
(let dead_end := False in
let seen0 := mkMarker (BR, BL, H, H, TL, TR, V, V) in
trans_closure (BR, BL, H, H, TL, TR, V, V) (BL, H, BR, H, TL, TR, V, V)
(TL, H, TR, V, V, BL, H, BR) (top_left BR BL H H TL TR V V)
(let dead_end0 := False in
let seen1 := mkMarker (BL, H, BR, H, TL, TR, V, V) in
trans_closure (BL, H, BR, H, TL, TR, V, V) (TR, H, BR, BL, TL, H, V, V)
(TL, H, TR, V, V, BL, H, BR) (left_down BL H BR H TL TR V V)
(let dead_end1 := False in
let seen2 := mkMarker (TR, H, BR, BL, TL, H, V, V) in
...
*)
Require Import List.
Inductive Move2 : Set := top_left2 | left_down2 | right_down2 | bottom_left2.
Fixpoint display_moves p q (m : Move p q) : list Move2 :=
match m with
| refl _ => nil
| top_left _ _ _ _ _ _ _ _ => top_left2::nil
| left_down _ _ _ _ _ _ _ _ => left_down2::nil
| right_down _ _ _ _ _ _ _ _ => right_down2::nil
| bottom_left _ _ _ _ _ _ _ _ => bottom_left2::nil
| trans_closure _ _ _ x y => display_moves _ _ x ++ display_moves _ _ y
end.
Eval compute in (display_moves _ _ automated_example).
(*
= top_left2
:: top_left2
:: left_down2
:: top_left2
:: right_down2
:: top_left2
:: top_left2
:: bottom_left2
:: bottom_left2
:: left_down2
:: right_down2
:: right_down2
:: nil
: list Move2
*)
Thursday, 21 August 2008
Unscrambling without Prolog
Subscribe to:
Post Comments (Atom)
No comments:
Post a Comment