少し悟ったぞ。
Coq入門以前でとどまってしまう事情
Coqはゲームソフトだ（と僕は認識してます）から、理屈や内部構造は後回しだと思えてきました。僕自身は、どうしても理屈や内部構造に目がいってしまうので、それを納得しないまま先に進むことが出来ないのですが、Coqと向き合う正しい姿勢とは言いがたいような。
例えばですね、「Coqの証明ゲームの表側と裏側 （誰も書かないCoq入門以前 4）」より：
Coqのゴールは、自然演繹の推論図に似ています。リファレンスマニュアルにもそれらしいことが書いてあります。それで僕は、Coqの証明は自然演繹の証明として解釈できるのだろう、と思っていました。
しかし、実際に操作した感触では、自然演繹とは違うのです。むしろ、シーケント計算に近いのか？ 今度はシーケント計算と対応付けようと試みました。ですが、シーケント計算とも違うところがあって、うまくいきません。
「自然演繹かシーケント計算か、おまえはどっちなんだ？」という態度、これは間違ってますよね。「演繹系とお絵描き圏論」において、片側シーケント計算の例を出した後で、僕は次のようなことを言っています。
こんな例[片側シーケント計算]もあるので、こっからここまでは自然演繹、ここから先がシーケント計算なんて境界を明確に設定するのは無理だし、たいした意味もないってことです。もちろん、境界領域から遠く離れた典型的な自然演繹、典型的なシーケント計算と呼べるシステムが存在しますがね。
Coqの証明システムは、典型的な自然演繹でも典型的なシーケント計算でもない、中間的な存在だったわけです。それを「おまえはどっちなんだ？」と問うのは「たいした意味もない」行為です。自分が指摘した過ちを自分が犯しているという、情けない話。
CoqはCoqとしての論理計算／証明のシステムを持っていて、それは（典型的な）自然演繹に近いところもあれば、（典型的な）シーケント計算に似てるところもあるけれど、どちらかに一致しているわけではありません。それだけのこと。
Coqの証明ゲームを、既存の論理計算に引き寄せて解釈することがいいのか悪いのか？ 疑問を感じるところですが、少なくとも僕自身は、そうしないと分かった気分になれないので、シーケント計算との類似性をもう少し探るつもりです。
既存の論理計算に引き寄せ過ぎるのは良くないです。同一でないことを承知で類似性を探るのは悪くはないでしょう＞自分。
UIのパターンとオペレーションから証明に習熟する道もあるし、若者はそうしてCoqの達人に成長するかも知れません。
UIのパターンとオペレーションから入るのが正しい、いや何が正しいかはさておき、効率的な学習法ですね。まずは遊んでみないとゲームの楽しさが分かりませんから。あるいは、業務ソフトとして役立つかどうかも使ってみないと分からないし。
Coqに関する情報はけっこう多いのですが、ゲームとして遊び始めるための良い説明は少ないです。多くの人が入門的な解説を試みてはいますが、Coqの入門的な説明はとても困難だと思います。
画面の見方、ゲームの始め方、タクティク（呪文）の基本的な使い方などを説明するには、UI画面のbefore／afterを示して、いったい何が起きたのかを説明することになるので、非常に面倒です。それを読む側もウンザリするでしょう。
一方で、関数型言語や論理の予備知識もある程度は必要です。証明メカニズムの背景であるカリー／ハワード対応は必須じゃないでしょうが、論理記号や推論図くらいは知ってないとゲームのルールを説明できません。
そして、説明に使う言葉がまた問題です。Coqの説明には、関数型言語、論理、型理論などの言葉が入り混じって登場します。型理論の用語や記号が無茶苦茶のグチャグチャであることは「用語法／記号法／図示法は、ほんっとうーに方言が多い」からリンクされている一連のエントリーを参照してください。Coqでは型理論の用語に加え、論理やラムダ計算の用語、Coq独自の用語も混じるので、さらに輪をかけてグッチャングッチャンです。同意語、多義語、曖昧語がたくさんたくさん使われています。その一例は、「Coqの証明ゲームの表側と裏側 （誰も書かないCoq入門以前 4）」に挙げた「ゴール」という言葉です。混乱を招く用語法や、ミスリーディングな説明の仕方が、伝統や文化として定着してしまっているのでしょうか。
Coq証明ゲームの遊び方をどう説明したらいいのだろう
GUIウィンドウのキャプチャやコンソール画面のコピーが悩みのタネ、使わないで済ませられないか？ で、思ったんですが、シーケントでしょ。ここで誤解なきよう、シーケント計算の知識を仮定するんじゃないですよ。コンパクトな記法としてシーケントを採用するのです。
「Coqの証明ゲームの表側と裏側 （誰も書かないCoq入門以前 4）」で既に導入しているのですが、コンソール画面よりだいぶ紙面を節約できますし、スクリーンキャプチャしたりコピーを貼り付ける手間がかかりません。
1 subgoalH1 : A
H2 : B
============================
B /\ Aand_is_commutative < split.
2 subgoalsH1 : A
H2 : B
============================
Bsubgoal 2 is:
Aand_is_commutative <
上と同じ意味のシーケント記法↓。
H1:A, H2:B ⇒ B∧A ----------------------------------------↓ split H1:A, H2:B ⇒ B H1:A, H2:B ⇒ A
それと、複数のゴールがあると、GUIでもコンソールでもカレントゴール以外は結論しか表示されない（全体が見えない）という問題も解消できます。
タクティクは、モンスター＝ゴールを弱体化させて、最終的には消滅させるための呪文です。タクティクを使えない限り証明ゲームを行えません。基本的で重要なタクティクを選んで、上記のシーケント推論図風の図式で解説を付ければ、最初に必要な「ゲームの基本ルール集」はできるでしょう。実際、「Coqの証明ゲームの表側と裏側 （誰も書かないCoq入門以前 4）」で紹介した2つのスライドはそういう説明の方法をとっています。
基本的なタクティクが使えるようになれば、あとは実務的な課題解決だとか難しい定理の証明とかに向かえばいいでしょうが、それは入門の範囲外ですから、まずは基本タクティク。
次にCoqに関する記事を書くとすれば、「Coq入門以前」から「Coq入門」にしようと思います。
