CoqのLtacでmap関数を実装する

はじめに

Ltac は、Coq において証明の探索を自動化するための Domain Specific Language です。Coq においてプログラムを記述する言語は Gallina と呼ばれていて、これは依存型を持つ普通の関数型言語で意味論も目的も Ltac とは全く別物です。
Gallina で map関数を実装することは Haskell や OCaml で map関数を実装するのとほとんど同じで普通のことです。一方、Ltac は証明の探索の自動化を目的としているので普通の関数型言語と同じようにとはいかないのですが、 proof を具体的に構成するために直接 Gallina の項を生成したり、関数の引数として扱うことが可能であることを利用して関数型言語っぽいプログラミングが可能です。
この記事では Coq 入門者のバイブル？の Adam Chlipala の Certified Programming with Dependent Types の 14章3節の内容を参考に、 Ltac で map関数を実装する方法を紹介したいと思います。実際に map関数を Ltac で実装することには実用上の意味は全くありません。実装を通して Ltac の仕様を学ぶことが目的です。

length関数を実装する

map関数を実装する前に length関数を実装することを通していくつか基本的な Ltac の仕様を確認します。

Gallina 風の実装

とりあえず Gallina 風に Ltac で length関数を実装しようとすると以下のようになります。

Ltac length ls :=
  match ls with
    | nil => O
    | _ :: ls’ => S (length ls’)
end.

これを Coq に読み込ませると以下のようなエラーになります。

Error: The reference ls’ was not found in the current environment

Ltac の match 節では、パターンマッチする変数に ? をプレフィックスとしてつける必要があります。よってここでは ls' を ?ls' に修正します。

Ltac length ls :=
  match ls with
    | nil => O
    | _ :: ?ls’ => S (length ls’)
end.

Ltac から Gallina へ

上のコードを Coq に読み込ませると次のエラーが出力されます。

Error: The reference S was not found in the current environment

これは Ltac としてパースする際に S が tactics として定義されていないといっています。ここで S は nat のコンストラクタなので Gallina の項です。よってそのことをパーサーに明示的に指定してやる必要があります。そのために constr:(Gallina の項) という構文を使用します。

Ltac length ls :=
  match ls with
    | nil => O
    | _ :: ?ls’ => constr:(S (length ls’))
end.

これで Coq に length の定義を読み込ませることに成功します。実際に実行して結果を確認しましょう。結果の確認は以下のようにすると簡単です。

Goal False.
  let n := length (1 :: 2 :: 3 :: nil) in
  pose n.

実行すると以下のような出力が表示されます。

n := S (length (2 :: 3 :: nil)) : nat
==================
False

n := 3 : nat という結果を期待していたので、期待はずれですね。ここでの問題は constr:() 内で呼び出されている length が、今 Ltac で定義した length ではなく Gallina の list に対して定義されている length を参照している点です。

Gallina の項を Ltac 呼び出しの結果として受け取る

Gallina の項を返す Ltac を呼び出した結果を受け取って利用したい場合には let 構文を使用して一度変数に代入してやる必要があります。よって実装は以下のようになります。

Ltac length ls :=
  match ls with
    | nil => O
    | _ :: ?ls' =>
      let ls'' := length ls' in
      constr:(S ls'')
  end.

上と同様に実行すると以下の結果が表示されます。

n := 3 : nat
===================
False

望む結果が得られました。

気持ち悪い点

実装としては上の定義で良いのですが一点気持ち悪い点があります。
気づいた方もいらっしゃるかもしれませんが、S はそんな tactic は定義されていないとエラーになるのに、同様に Gallina の項で nat のコンスタラクタである O はそのまま記述しても意図した通りにパースできてしまう点です。詳しく仕様を調べていないのでなんとも言えませんが、S を同様に O の方も constr:O としておいた方がよい定義と言えるのではないかと思います。

map関数(Ltac引数)を実装する

次に引数の関数として Ltac の関数を取る map関数を実装します。

Ltac map T f :=
  let rec map' ls :=
    match ls with
      | nil => constr:(@nil T)
      | ?x :: ?ls' =>
        let x' := f x in
        let ls'' := map' ls' in
        constr:(x' :: ls'')
    end in
  map'.

let rec 構文を使用することでローカルな再帰関数を定義することができます。
constr:(@nil T) を constr:nil とすることができないのは、Ltac からはこの nil が何の型のリストか知ることができないからです。
Ltac には type of という関数が用意されていて Gallina の項の型を Ltac から知ることができます。引数 f が Gallina の項なら type of f とすることによって引数 f の返り値の型を知ることができますが、今引数 f は Ltac の関数なので type of を使用することはできません。よって明示的に map関数への引数として引数 f の返り値の型を渡しています。
この map関数を使用するには以下のように呼び出します。

Goal False.
  let ls := map (nat * nat)%type ltac:(fun n => constr:(n, n)) (1 :: 2 :: 3 :: nil) in
  pose ls

ここで ltac:() という構文が使用されています。これは constr:() と反対で、Gallina としてパースが行われている文脈で、Ltac の項としてパースするように指示する構文です。
Coq の proof editting mode では apply H. といった形の tactic の呼び出しを何度も見ると思います。この時 apply は Ltac で定義された tactic であるのに対して H は Gallina の項です。
つまり簡潔に proof を記述できるようにするために、二つのパースモードが自動的に切り替わっています。先頭のみを Ltac で定義された tactic として解釈し、続く項は Gallina の項として解釈されます。
このパースモードの挙動は map関数を定義する際にも有効であることが確認できます。つまり上の map関数の定義で f x としているところでは、f は Ltac の項で x は Gallina の項です。その下の map' ls' のところも同様です。
今定義した map関数では２つ目の項は Ltac の関数としてパースして欲しいので、ltac:() 構文を使用しています。
結果を確認してみましょう。

ls := (1, 1) :: (2, 2) :: (3, 3) :: nil : list (nat * nat)
===========================
False

これで Ltac の関数を引数として受け取る map関数を定義することができました。

map関数(Gallina引数)を実装する

最後に引数として Gallina の関数を取る map関数を実装します。これは Adam Chlipala の書籍にも載っていない例です。

Ltac map f :=
  match type of f with
    | ?T1 -> ?T2 =>
      let rec map' ls :=
        match ls with
          | nil => constr:(@nil T2)
          | ?x :: ?ls' =>
            let x' := eval compute in (f x) in
            let ls'' := map' ls' in
            constr:(x' :: ls'')  
        end in
      map'
  end.

上で説明した type of 関数を使用しています。type of 関数の返り値である引数 f の型をパターンマッチで分解することで、引数 f の返り値の型を取得することができます。ここでは ?T2 にバインドしています。
もう一点 eval ~ in という tactic が新しく出てきています。compute の箇所は、simpl や unfold など他にも指定できるものがいくつかあります。
もし eval を呼び出さずに f x の結果をそのまま constr:(f x) として使用したらどのようになるのでしょうか？そのように変更したと仮定して実行してみます。

Goal False.
  let ls := map (fun n : nat => (n, n)) (1 :: 2 :: 3 :: nil) in
  pose ls

今回は引数は Gallina の項なので ltac:() は必要ありません。また結果の型は (fun n : nat => (n, n)) の nat の部分を指定することで自動的に推論されます。全く型を指定しないと型の推論に失敗してエラーになります。この辺りは Ltac と Gallina の間で型情報をやり取りするタイミングなどの問題もあり複雑そうです。
結果は以下のようになります。

ls := (fun n : nat => (n, n)) 1 :: (fun n : nat => (n, n)) 2 :: (fun n : nat => (n, n)) 3 :: nil : list (nat * nat)
=======================
False 

β変換つまり関数適用が一切行われずにそのまま出力されてしまっています。ここでは評価を強制するために eval を使用しています。eval を使用した定義では以下のように出力されます。

ls := (1, 1) :: (2, 2) :: (3, 3) :: nil : list (nat * nat)
===========================
False

eval によって項の評価が行われるようになりました。

最後に

このように単純な例を実装することを通してでも、Ltac のセマンティクスなどについていくつか学べるところがあって面白いのではないかと思います。
Coq が他の定理証明支援系と比較して圧倒的に優れているのは Ltac の存在、つまり証明を自動化するプログラムを記述する能力にあるのではないかと個人的に考えています。
Ltac を征するものは Coq を征するといっても過言ではない？と思いつつ、これからも Ltac ハックに励んでいきたいと思います。

参考書籍

Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant