この記事は株式会社 proof ninja の助成を受けて書いています．
小ネタです．今回は Rocq で迷路を解いていこうと思います．
といっても迷路を解くような(Gallina の)関数を定義するわけではなく，Rocq のタクティクに迷路を解かせようと思います．
どういうことか早速見ていきましょう．
まず，迷路の仕様です．迷路の盤面は自然数の二重リストで表し，0は通れるマス，正の値を通れないマスを表すとします．
また，一度通ったマスはその後通れないということにします．
マスの移動は，今いるマスから縦横に隣り合うマスに移動できるものとします．
これらの仕様を Rocq で書きます．
Require Import List.
Import ListNotations.
Definition Board := list (list nat).
Definition Point := (nat * nat)%type.
(* 盤面 [board] の座標 [p] での値を返す *)
Definition val (p : Point)(board : Board) :=
let (n,m) := p in
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.
(* 盤面 [board] の座標 [p] のマスを値を 1 にする．一度通ったところを通れなくするために使う *)
Fixpoint fill (p : Point)(board : Board) : Board :=
let (n,m) := p in
match board with
| [] => []
| r::rs =>
match n with
| O => fill' m r :: rs
| S n' => r :: fill (n', m) rs
end
end.
Inductive Direction := Left | Right | Up | Down.
(* [moves_to p board p' board' dir] =
「盤面 [board] のマス [p] にいるプレイヤーは方向 [dir] に移動でき，
移動するとプレイヤーの座標は [p']，盤面は [board'] になる」 *)
Inductive moves_to :
Point -> Board -> Point -> Board -> Direction -> Prop :=
| moveLeft : forall n m board,
val (n, m-1) board = 0 ->
moves_to (n, m) board (n, m-1) (fill (n, m-1) board) Left
| moveRight : forall n m board,
val (n, 1+m) board = 0 ->
moves_to (n, m) board (n, 1+m) (fill (n, 1+m) board) Right
| moveUp : forall n m board,
val (n-1, m) board = 0 ->
moves_to (n, m) board (n-1,m) (fill (n-1, m) board) Up
| moveDown : forall n m board,
val (1+n, m) board = 0 ->
moves_to (n, m) board (1+n,m) (fill (1+n, m) board) Down.
(* [accept p p' board l] =
「盤面 [board] 上で，マス [p] からスタートして方向のリスト [l] に沿って移動するとマス [p'] に辿りつく」 *)
Inductive accept :
Point -> Point -> Board -> list Direction -> 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,
moves_to (n, m) board (n',m') board' d ->
accept (n', m') (goaln, goalm) board' ds ->
accept (n, m) (goaln, goalm) board (d :: ds).
コメントに説明を書いた通りですが，moves_to p board p' board' dir 移動に関する述語を表しています．
一度通ったマスを通れなくするため，board' は board の座標 p の値が 1 になったものとなっています．
また，accept p p' board l が，方向のリスト l はスタート p，ゴール p' の解であるという述語になっています．
迷路を解くには，この述語をみたすような l を見付ければよい，ということになります．
迷路の具体例を Rocq に解かせてみます．
Definition example :=
[[1;0;1;0];
[0;0;0;1];
[1;0;1;0];
[0;0;0;0]].
Global Hint Constructors moves_to accept.
Theorem ex : { l | accept (0, 0) (2, 3) example l }.
Proof.
eexists. eauto 20.
Defined.
Eval simpl in proj1_sig ex.
(*
= [Down; Right; Down; Down; Right; Right; Up]
: list Dirc
*)
具体的な迷路の盤面 example を定義しました．
また，ex の型 { l | accept (0, 0) (2, 3) example l } は「盤面 example でスタート (0,0) からゴール (2，3) への迷路の解 l が存在する」という命題です．
(一般に，{x | P x} は「P x をみたす x が存在する」という意味の Type 型の値です．)
つまり，ex が証明できれば解 l も得られます．
ここで，Global Hint Constructors moves_to accept. コマンドで moves_to や accept のコンストラクタをグローバルなヒントデータベースに与えています．
これによって，auto や eauto タクティクが moveLeft などや accept_goal, accept_next を自動で apply してくれるようになります．
ex の証明はとても短くできます．何をしているのかというと，まず eexists タクティクでゴール
{ l | accept (0, 0) (2, 3) example l }
を
accept (0, 0) (2, 3) example ?l
に変えます．通常なら l の存在を証明をするときは具体的に l を作ってタクティク exists l などで渡してやりますが，eexists はまず existential variable (evar) と呼ばれるメタ変数 ?l を作った後，exists ?l のような動作をします．
?l の実態はこの後の証明をしながら具体的に決めていきます．
つまり，存在証明をするとき具体的な l を作るのを後回しにできるわけです．
その後の eauto は evar があるとき用の auto で，evar を埋めながら自動証明をしてくれます．
具体的には，仮定やヒントにある命題などをどんどん apply して，失敗したらバックトラックを繰替えしています．
つまり，eauto は accept_next や moveLeft/moveRight/... などを apply していき，迷路に詰まったらバックトラックして正しい解が得られるまで繰替えします．eauto 20 の 20 は探索の深さを指定しています．
そんなわけで eexists と eauto のみで証明が完了しました．
実際に得られた解を見るために，コマンド Eval simpl in proj1_sig ex. を使っています．
proj1_sig ex が ex の証明の中で具体的に得られた l を指し，Eval simpl in でその項を簡約しています．
このコマンドの出力は [Down; Right; Down; Down; Right; Right; Up] で，実際に迷路上をたどってみればちゃんと迷路の答えになっていることが分かります．
ということで Rocq を自動証明の機能を使うとバックトラックが簡単にできました．…が，これは深さ優先探索なので実は大きい迷路を解くのには適していません．
ですがこのテクニックは使える場面も多いです．たとえばコンパイルの正しさを定義し，「プログラム A の変換結果が B である」というという述語を定義した上でタクティクを使ってプログラム A を B にコンパイルすることができたりします．この場合，コンパイルは事前に定義した意味で正しいコンパイルとなっていることが同時に証明されます．
そんなわけで単に証明するだけとは少し違った Rocq の使い方を紹介してみました．