Skip to content

Instantly share code, notes, and snippets.

@erutuf
Created March 21, 2017 13:32

Revisions

  1. erutuf created this gist Mar 21, 2017.
    72 changes: 72 additions & 0 deletions maze.v
    Original file line number Diff line number Diff line change
    @@ -0,0 +1,72 @@
    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
    *)