maze.v

Require Import List.
Import ListNotations.

Definition Board := list (list nat).

Definition size (board : Board) := length board.

Definition val (n m : nat)(board : Board) := nth m (nth n board []) 1.

Fixpoint fill' m (l : list nat) : list nat :=
  match l with
  | [] => []
  | x::xs =>
    match m with
    | O => 1::xs
    | S m' => x :: fill' m' xs
    end
  end.

Fixpoint fill (n m : nat)(board : Board) : Board :=
  match board with
  | [] => []
  | r::rs =>
    match n with
    | O => fill' m r :: rs
    | S n' => r :: fill n' m rs
    end
  end.

Inductive Dirc := Left | Right | Up | Down.

Inductive move :
  nat -> nat -> nat -> nat -> Board -> Board -> Dirc -> Prop :=
| moveLeft : forall n m board,
    val n (pred m) board = 0 ->
    move n m n (pred m) board (fill n (pred m) board) Left
| moveRight : forall n m board,
    val n (S m) board = 0 ->
    move n m n (S m) board (fill n (S m) board) Right
| moveUp : forall n m board,
    val (pred n) m board = 0 ->
    move n m (pred n) m board (fill (pred n) m board) Up
| moveDown : forall n m board,
    val (S n) m board = 0 ->
    move n m (S n) m board (fill (S n) m board) Down.

Inductive accept :
  nat -> nat -> nat -> nat -> Board -> list Dirc -> Prop :=
| accept_goal : forall n m board,
    accept n m n m board []
| accept_next : forall n m n' m' goaln goalm board board' d ds,
    move n m n' m' board board' d ->
    accept n' m' goaln goalm board' ds ->
    accept n m goaln goalm board (d :: ds).

Hint Constructors move accept.

Definition example :=
  [[1;0;1;0];
   [0;0;0;1];
   [1;0;1;0];
   [0;0;0;0]].

Example ex : { ds | accept 0 0 2 3 example ds }.
  eexists. eauto 20.
Defined.

Eval simpl in proj1_sig ex.
(*
   = [Down; Right; Down; Down; Right; Right; Up]
   : list Dirc
*)