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

Unscrambling with Prolog

%% I'm playing this Oxyd game (inside Enigma [link])
%% One of the puzzles is this scrambled configuration

starting(([-,⌋,⌊]
         ,[-,  ⌈]
         ,[⌉,|,|])).

%% And you've to hit against the sides to unscramble it into:

solution(([⌈,-,⌉]
         ,[|,  |]
         ,[⌊,-,⌋])).

%% Then it explodes and you win a spring
%% The moves you can do are:

move(top_left,
    ([A,B,C]
    ,[D,  E]
    ,[F,G,H]) --> ([B,C,A]
                  ,[D,  E]
                  ,[F,G,H])).

move(left_down,
    ([A,B,C]
    ,[D,  E]
    ,[F,G,H]) --> ([F,B,C]
                  ,[A,  E]
                  ,[D,G,H])).

move(right_down,
    ([A,B,C]
    ,[D,  E]
    ,[F,G,H]) --> ([A,B,H]
                  ,[D,  C]
                  ,[F,G,E])).

move(bottom_left,
    ([A,B,C]
    ,[D,  E]
    ,[F,G,H]) --> ([A,B,C]
                  ,[D,  E]
                  ,[G,H,F])).

%% I want Prolog to solve this automatically for me though,
%% My first attempt is to use recursion like so,

%: solve(Win,[]) :- solution(Win).
%: solve(State,[Move|Moves]) :- move(Move,State --> Next), solve(Next,Moves).

%! ?- starting(State), solve(State,Moves).
%! ERROR: Out of local stack

%% Since Prolog searches depth first, this just kept trying top_left,
%% again and again, getting nowhere, infact it seeing the same config.
%% so I can pass along a list of seen configurations now, and fail when
%% the same one is seen twice.

%: solve(Win,[],_) :- solution(Win).
%: solve(State,[Move|Moves],Seen) :- move(Move,State --> Next), not(member(Next,Seen)), solve(Next,Moves,[State|Seen]).

%! ?- starting(State), solve(State,Moves,[State]).
%! State = ([-, '⌋', '⌊'], [-, '⌈'], ['⌉', ('|'), ('|')]),
%! Moves = [top_left, top_left, left_down, top_left, top_left, left_down, ...]

%% I got a solution this time... but it's thousands of moves, I think the puzzle can be solved
%% Within at least 10 moves, so Prolog should fail if it gets into a branch in the search tree that deep

solve(Win,[],_,_) :- solution(Win).
solve(State,[Move|Moves],Seen,Limit) :-
 move(Move,State --> Next), not(member(Next,Seen)), succ(LowerLimit,Limit), solve(Next,Moves,[State|Seen],LowerLimit).

solve(Solution) :- starting(State), solve(State,Solution,[State],10).

%! ?- solve(Moves).
%! Moves = [top_left, top_left, bottom_left, bottom_left, left_down, right_down, bottom_left,
%!          bottom_left, left_down, right_down].

Lights out solver using CLP

:- use_module(library(clpfd)).

solve(Puzzle,Solution) :-
 dimensions(Puzzle,Rows,Cols), dimensions(Solution,Rows,Cols),
 flatten(Solution,Variables), Variables ins 0..1,
 cells_of(Puzzle --> configure(Solution)), label(Variables).

configure(Solution,(X,Y,o)) :- around(X,Y,Solution,Group), off(Group).
configure(Solution,(X,Y,*)) :- around(X,Y,Solution,Group), on(Group).

on(Lights) :- sum(Lights, #=, On), 1 #= On mod 2.
off(Lights) :- sum(Lights, #=, Off), 0 #= Off mod 2.

around(X,Y,Grid,[Up,Left,Down,Right,Middle]) :-
 Yu is Y-1, Xl is X-1,
 Yd is Y+1, Xr is X+1,
 ( Grid@([Yu,X]->Up) -> true ; Up = 0 ),
 ( Grid@([Y,Xl]->Left) -> true ; Left = 0 ),
 ( Grid@([Yd,X]->Down) -> true ; Down = 0 ),
 ( Grid@([Y,Xr]->Right) -> true ; Right = 0 ),
 ( Grid@([Y,X]->Middle) -> true ; Middle = 0 ).

game([[*,o,o,o,o,o,*,o],
      [*,*,o,*,*,*,*,*],
      [*,*,o,*,*,*,o,*],
      [*,o,o,o,o,o,o,o],
      [o,*,*,o,o,o,*,*],
      [o,*,o,o,o,o,o,o],
      [*,*,*,*,*,*,o,o],
      [o,*,*,*,*,*,*,*]]).





:- op(500,xfy,@).
:- op(1050,yfx,<-).

flatten([],[]).
flatten([X|Xs],Zs) :- flatten(Xs,Ys), append(X,Ys,Zs).

flip(P,Y,X) :- call(P,X,Y).
dimensions(Grid, Rows, Cols) :- length(Grid, Rows), maplist(flip(length,Cols),Grid).

E@([]->E)         :- !.
[X|_]@([0|Ns]->E) :- !, X@(Ns->E).
[_|X]@([N|Ns]->E) :- !, N > 0, succ(M, N), X@([M|Ns]->E).

_/E@([]<-E)               :- !.
[X|Xs]/[Y|Xs]@([0|Ns]<-E) :- !, X/Y@(Ns<-E).
[X|Xs]/[X|Ys]@([N|Ns]<-E) :- !, N > 0, succ(M, N), Xs/Ys@([M|Ns]<-E).

tuple(Board,Tuples) :- tuple((0,0),Board,Tuples).
tuple(_,[],[]).
tuple((X,Y),[Row|Rows],Tuples) :-
 tuprow((X,Y),Row-Tail,Tuples),
 succ(Y,Y1), tuple((X,Y1),Rows,Tail).
tuprow(_,[]-X,X).
tuprow((I,J),[E|Es]-X,[(I,J,E)|Xs]) :- succ(I,I1),tuprow((I1,J),Es-X,Xs).

cells_of(Grid --> Pred) :- tuple(Grid, Tuples), maplist(Pred, Tuples).