Thursday, 21 August 2008

Unscrambling without Prolog


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
*)

No comments: