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