Coqサブセットについての考察

一昨日（表示は昨日になるかもしれない）、Coqのサブセットを作ろうかな、と書いた。
でもサブセットってどのくらいよ？という問題が出てくる。
少し考えてみよう。


まず、Coqのサポートしている範囲を挙げる。

1. 言語について：Vernacular（コマンド用言語、もはや言語というかはよくわからない）、Gallina（項記述言語、プログラムなども含む）、Ltac（証明記述用言語、Vernacularとは違った意味で便利な機能がある）。
2. 元としている計算について：Predicative Calculus of Inductive Constructions。*1
3. そのほか：CoInductiveな要素もある。

挙げればきりがないので、このあたりでやめよう。


サブセットを作るとして、気にしなければいけないのは次のいくつか。

1. 簡単な定理証明ができる。というかそれができないと意味がない。
2. プログラムが書ける。以下同文。
3. Ltacのサブセットが書ける。一応なくても証明はできるが、ないと厳しい。
4. CoInductiveな要素はいらない。この要素、使う側も作る側も気にすることが多すぎる。
5. etc...

なんだろう・・・？とても無謀な気がするのは（笑）。
気が向いたら考えよう。うん。今考える必要はない。
でもCoInductiveはいらんな。これは絶対だ。（後で必要に応じて付ければいい。面倒くさそうだが。）

*1:なぜかPredicativeがよく抜かれる。一応違うものだが、Coq以外の文脈でこの計算について述べることがそれほど多くないので、あまり意識されない。