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