うーむ、ムズカシイ。Coq、難しいなぁ。
Coqのプロモーションのために、「大丈夫、あなたも出来ます」みたいなこと言っちゃダメですよ。予備知識も心構えもなく安易に入門しても挫折するもの。「女子高校生でもやってます」って、ものすごく特殊な女子高校生でしょ。マララさんを例に出して「女子高校生でもノーベル賞とれます」って言っても、ノーベル賞とれないでしょ、ふつう。
まー、ノーベル賞に比べれば「大丈夫、あなたも出来る可能性が高いです」とは言えます。Coqがどんなものであり、どのへんに難所が潜んでいるかを知っておけば、Coqが出来るようになる可能性はより高まると思います（たぶん）。
僕自身、早々と挫折しかかっていたのですが、見方を変えると少しだけ見通しが立ちました。なので、これはCoqを触って困惑した人の助けにチョットはなるかも。
内容：
- Coqで使われる言語を分類しておく
- そもそもCoqはプログラミング言語なのだろうか？
- 業務ソフト／ゲームソフトと考えれば納得しやすい
- 業務ソフト／ゲームソフトとしてはマダマダ
- インターネット上の参考資料など
Coqで使われる言語を分類しておく
「誰も書かないCoq入門以前の話」に書いたように、Coqシステムは複数の言語を持ち、それらを混ぜて使います。とりあえず、Coq言語を次の3種類に分類しておくのがよいと思います。
- 式言語（expression language）
- コマンド言語
- タクティク言語
式言語の部分は、pCic（predicative Calculus of Inductive Constructions）の構文です。pCicは言語の名前というよりは、形式的計算体系に付けられた名前です。ここでは不正確なのを承知で、CoqにおけるpCic実装をpCic式言語と呼ぶことにします。pCic式言語は、型付きラムダ計算ベースの関数型言語です。
コマンド言語はVernacular（バーナキュラー）ですね（「誰も書かないCoq入門以前の話」参照）。入門者として当面必要なVernacularコマンドは二つだけです。DefinitionとInductive、これだけで大抵のことはできます*1。ただし、pCicの知識を前提にしてですが。
タクティクというのは、コマンドの一種です。タクティクはVernacularコマンド言語の一部なのかも知れませんが、明らかに異質です。Vernacular文は、大文字で始まりピリオドで終わります。複文（複数の文のグループを一文とみなすこと）は許されていません。一方タクティクは、小文字から始まるコマンドで、セミコロンで区切った複文を書くことができます。
タクティクは、証明の遂行のためだけに使わるコマンドです。VernacularコマンドはCoqに組み込みのようですが、タクティクはユーザーにより追加できます。タクティク(ス)ライブラリを利用したり提供したりができるわけです。
といったようにタクティクは、構文も用途も他のVernacularコマンドとは違うので、これは第三の言語として別扱いしたほうが分かりやすいです。
そもそもCoqはプログラミング言語なのだろうか？
単一システムに複数の言語を持ってるなんて、プログラミング言語好きにはたまらないなー、と； いや、なんか違う気がします。Coqって、プログラミング言語（達）とその処理系なのでしょうか？ 理屈の上ではYESと答えていいでしょうが、感触としてはNOです。
まず、pCic式言語に注目しましょう。これは確かに関数型プログラミング言語とみなせます。記述力はとても高く、構文も洗練されています。好みの問題はあるにしても、よくできた関数型プログラミング言語だと思います。
でも、関数型プログラミング言語としてだけ使う目的でCoqを選ぶ必然性はあまりない気がします。「pCic言語に惚れた」っていう人もいるかも知れませんが、Coqの実装言語であるOCamlやその他の関数型プログラミング言語でも同じ目的は達せられるでしょう。
Coqを使うということは、やっぱりVernacularスクリプトを書くことです。とはいえ先に述べたように、DefinitionコマンドとInductiveコマンドがあれば間に合うので、これだけならpCicのオマケのようなもんです。となると、Coqが他の関数型プログラミング言語と一線を画すゆえんは、第三の言語であるタクティク言語の存在だとなります。
タクティク言語は証明記述専用のコマンド言語です。一種のDSL（domain-specific language）と言っていいでしょう。言語としては極端に簡単な構文なので、キーボードからのコマンド入力に限らず、タクティク(ス)ツールバー／パレットとかのUIも可能でしょう。
一般に通用しているCoqの冠（肩書）は、「プログラミング言語Coq」ではなくて「証明アシスタントCoq」です。確かにアシスタントです。人間の代わりに証明を書いてくれるわけではありません。でも、タクティクという命令を出すと面倒な単純作業を着実にやってくれます。賢いタクティクを足してあげれば、アシスタントとしてより知的・有能になるのです。
タクティクという呪文を使って機械のアシスタントを操りながら、証明を作成していくことが、CoqをCoqらしく使う姿です。この使い方は、通常のプログラミング言語処理系を使うこととは大きくかけ離れた印象があります。
業務ソフト／ゲームソフトと考えれば納得しやすい
Coqが通常のプログラミング言語と違うな、と感じるもうひとつの理由は、ソースコード（Vernacularスクリプト）を読んでも学習の効果が薄いことです。Coqは対話的に使うソフトウェアなので、最終結果として清書されたスクリプトからは、途中の対話過程が見えません。
ワープロで作った印刷文書を精読したらワープロを使えるようになるか？ 会計ソフトで出力した決算報告書をたくさん見たら会計ソフトを使えるようになるか？ なりませんよね。それと似た事情があって、ソースコードリーディングしても理解が捗りません。
文章と図でCoqとの対話過程を見せることは大変です。Coqの解説を書いている人はみなさん苦慮されていると思います。coqideやProof Generalは三画面構成で、(1)スクリプトの編集画面、(2)Coqからの応答出力の画面、(3)現在の証明の状態を表示する画面 があります。これらの画面が時々刻々と変化していきます。画面キャプチャを大量に使うのも面倒だし鬱陶しい。ビデオ教材が有効かも知れませんが、それも手間。
要するに、効果的な解説／学習の方法が、通常のプログラミング言語とはどうも違うのです。むしろ、特定業務の仕事の効率化・生産性アップの道具、つまり業務ソフトと考えればいいのか、と思い至りました。どんな業務かと言えば、記号計算や証明に関連する業務です。
仕事が効率化するなら、業務ソフトを学ぶモチベーションがあるでしょう。しかし、記号計算や証明の業務に携わる人が多いとは思えません。すべての人にとってCoqが意味あるとするなら、それはゲームソフトとしてでしょう。証明という名のゲームで遊べるソフトウェアです。
Coqは誰でも簡単に使えるソフトウェアではありませんが、目的が業務またはゲームならば、「仕事だから苦労してもやるぞ」「難しいゲームほどチャレンジしがいがある」とかの動機は生まれるでしょう。
業務ソフト／ゲームソフトとしてはマダマダ
pCic式言語は、プログラミング言語理論・型理論の新し目の成果を取り入れたモダンで完成度の高い関数型言語です。しかし、証明を行う業務ソフト／ゲームソフトとしてのCoqは、未成熟で使い勝手が悪いソフトウェアであり、これはマダマダだなー、と感じます。
Coqの本領である証明の記述が、とにかく分かりにくい！ 人間可読性が最悪です。Coqの証明の実体はpCic式なので、その式を直接手で書いて証明を与えることもできますが、通常はタクティクの列で証明を記述します。タクティクの列は、証明であるpCic式そのものではなくて、pCic式を組み立てる手順を記録したものです。
自分でCoq処理系＝アシスタントと対話しているときは分かっていた気でも、出来上がった証明スクリプト（タクティクの列）の解読は至難の業です。Coq処理系にスクリプトを読ませてリプレイするしかないでしょう。このことも、「ソースコードを読んでもしょうもない」感じを募らせます。
教科書や論文にある自然言語による証明は、読んだら分かるように書かれています。もちろん、それ相応の予備知識と努力は必要ですが、推論の筋道を人間が追いかけられるように書いてあります。Coqの証明はそうではなくて、機械を動作させる命令列で、いわば「推論機械のアセンブラ言語で書かれたプログラム」です。
これ、ちょっと何とかならないの？ と思います。C-zar（シーザー？）http://www-verimag.imag.fr/~corbinea/mmode.en.html という試みがあるらしいです。が、現状どんな按配か不明です。"A Synthesis of the Procedural and Declarative Styles of Interactive Theorem Proving"（Freek Wiedijk）に、より高水準の証明言語の例が幾つも出ています。「これからに期待」という感じです。
業務ソフト／ゲームソフトとして考えれば、UIの工夫はいくらでもあるでしょう。今のCoq処理系は外枠にウィンドウシステムを使っているだけで、画面（ペイン）の中身は色付きテキストだけですからね。これじゃ楽しくない。もっとグラフィカル、嫌味でない程度のエフェクトとか。アシスタントなのだから、もっと可愛げや色気が欲しいし； このへんは日本のゲーム文化／オタク文化の出番かもしれません。
インターネット上の参考資料など
Coqは、畳の上の水練の効果がない処理系です。実際に対話的処理系に触らないと何も分からないです。その意味では、僕のこのエントリーも含めて「読んだだけで分かる記事」なんてないでしょう。触りながら参照する資料としては：
Coq本家サイトのドキュメント（https://coq.inria.fr/documentation）がものすごく充実しています。とても読み切れる量ではありませんが、リファレンスマニュアル（https://coq.inria.fr/distrib/current/refman/）の索引を利用して必要なところだけ参照するのがおすすめです。
チュートリアルは、https://coq.inria.fr/documentation からリンクされているCoq in a Hurry（https://cel.archives-ouvertes.fr/inria-00001173）が良さそうです。
pCicについて手早く知りたいなら、スライド http://www3.di.uminho.pt/~mjf/pub/SFV-CIC-2up.pdf をざっと眺めるといいでしょう。このスライドをちゃんと理解する必要はないでしょう（僕は分からないです）が、ラムダ計算の基本か関数型言語のどれか（OCaml、Haskell、Lisp／Schemeの方言、Scalaなど）をかじっておくと、CoqのpCic実装の理解が早いです。
*1:Fixpointは、pCic側のfixを使えばなくても大丈夫。
