Coqの証明ゲームの表側と裏側（誰も書かないCoq入門以前 4） - 檜山正幸のキマイラ飼育記 (はてなBlog)

Coqの理解が進まないで難儀しております。でもまー、J言語よりはマシ。J言語、演算子の記憶が辛過ぎる。Coqのコマンド名は省略なしのフルスペルだから、書くのが面倒だけど記憶はしやすいです。

思うに、僕が難儀しているのは年寄りだからでしょう。理解力や気力の問題ももちろんありますが、拘りや先入観が理解を阻害している感じです。あんまり色々考えないで、業務ソフト／ゲームソフトとしての操作だけにフォーカスしたほうが習得が早いでしょう（僕はそれが出来ない）。

論理を学ぶ前にCoqを道具（あるいは遊具）として使いこなすような世代は、我々旧世代とは違った直感*1を手に入れるのじゃないのかな、と思います。ですが、僕のような旧世代オッサンは、過去の知識や自分の思い込みと照合させてみないと理解した気になれない。という次第で、ゲームとしての証明*2を解説した後で、従来型の（教科書に書いてあるような）論理とCoqとの関係を考えてみたいと思います（未完ですが）。

内容：

Coqによる証明の実例
「ゴール」という言葉の困った使い方
Coqはどんなゲームソフトなのか
老人は背後の理屈が気になる
ゴールはシーケントなのかも知れない
ゴールとシーケント
証明ゲームの裏側へ

Coqによる証明の実例

「業務ソフトまたはゲームソフトとしてのCoq （誰も書かないCoq入門以前 2）」より：

coqideやProof Generalは三画面構成で、(1)スクリプトの編集画面、(2)Coqからの応答出力の画面、(3)現在の証明の状態を表示する画面があります。

この3つの画面（ペイン）を何と呼べばいいのでしょうね。「(1)スクリプトの編集画面は」素直にスクリプトペインと呼ぶことにします。「(2)Coqからの応答出力の画面」は、Proof Generalではresponseとタイトルが付いているので応答ペイン、「(3)現在の証明の状態を表示する画面」は、同じくProof Generalではgoalsなのでゴールズペインと呼ぶことにします。複数形の「ズ」をカタカナ書きでも残すのは、複数（かも知れない）であることが重要だと思うからです。

3つのペインのなかでゴールズペインは、証明を行っている最中だけ使うものです。ゴールズペインとにらめっこしながら、タクティク（証明遂行コマンド）を投入していきます。Undoが自由にできるので、ダメなら戻ってやり直し。行きつ戻りつの試行錯誤です。

「業務ソフトまたはゲームソフトとしてのCoq （誰も書かないCoq入門以前 2）」に書いたように、実際の証明の様子を引用するのは面倒です。

文章と図でCoqとの対話過程を見せることは大変です。Coqの解説を書いている人はみなさん苦慮されていると思います。
[...snip...]
これらの画面が時々刻々と変化していきます。画面キャプチャを大量に使うのも面倒だし鬱陶しい。ビデオ教材が有効かも知れませんが、それも手間。

よく使われている方法は、coqideやProof Generalではなくて、コンソールで使うインタープリタであるcoqtopの出力をテキストとして貼り付ける方法です。僕もこの方法を使うことにします。

まず、Vernacularスクリプトを挙げます。

Parameter A B : Prop.
Theorem and_is_commutative : A∧B → B∧A.
Proof.
 intros.
 destruct H as [H1 H2].
 split.
 assumption.
 assumption.
Qed.

証明したい定理は、「AND演算は可換である」という意味を持つ命題です。実際に証明（Proof.からQed.まで）が付いています。まー、分かりませんよね、これ見ても。

ここで驚いて欲しいのは、命題を「A∧B → B∧A」のように書けることです。これを可能にするには、Vernacularスクリプトの冒頭で Require Import Utf8_core. としておきます。「∀」「∃」、ラムダ式の「λ」なんかも使えるようになります。

coqtopのコンソール記録を以下に貼ります。とりあえず素材を提示したいだけでして、現時点で意味不明でも気にしないでください。coqtopでは、「∧」などが使えないようで*3、残念ながらアスキー表現の「/\」などを使います。なお、Proof.は冗長なだけなので省いています。



Coq < Parameter A B : Prop.

A is assumed

B is assumed
Coq < Theorem and_is_commutative : A/\B -> B/\A.

1 subgoal
  ============================

   A /\ B -> B /\ A
and_is_commutative < intros.

1 subgoal
  H : A /\ B

  ============================

   B /\ A
and_is_commutative < destruct H as [H1 H2].

1 subgoal
  H1 : A

  H2 : B

  ============================

   B /\ A
and_is_commutative < split.

2 subgoals
  H1 : A

  H2 : B

  ============================

   B
subgoal 2 is:

 A
and_is_commutative < assumption.

1 subgoal
  H1 : A

  H2 : B

  ============================

   A
and_is_commutative < assumption.

No more subgoals.
and_is_commutative < Qed.

intros.

destruct H as (H1, H2).

split.

 assumption.
 assumption.
and_is_commutative is defined
Coq <

coqtopでは、時間的な推移がそのままダラダラとコンソールに残りますが、coqide／Proof Generalでは、ゴールズペインが次々と書き換わります。ここらへんの説明を文章でするのは面倒で虚しいので、まー触ってみてください。

「ゴール」という言葉の困った使い方

さて、Coqはゴールズペインに次のような形を表示します。

  H1 : A
  H2 : B
  ============================
   B /\ A

これを何と呼ぶのでしょうか？しばらく分かりませんでした。結論を言えば「ゴール」と呼びます。

ところが、"Coq in a Hurry"でもリファレンスマニュアルの"Chapter 8 Tactics"でも、ゴールの意味は違った定義で導入され、いつのまにか意味をすり替えています。こういう説明のやり口は僕は嫌いです。混乱をまねき迷惑な話です。

"Coq in a Hurry"を見てみましょう。最初に、the goal is displayed under the horizontal line と定義されます。the horizontal line（横線）はイコールの並びなので、上の例では、B ∧ A（非アスキー文字使います）がゴールということになります。

しばらくすると、次のようなことが書いてあります。

Each goal actually has two parts, a context and a conclusion.

はぁ？上の例では B ∧ A がゴールだったけど、そのゴールは、コンテキストと結論（conclusion）を持つって？ B ∧ A のどこがコンテキストでどこが結論だよ？？

実は、横線の下をゴールと呼ぶのは嘘で、横線の上と下を合わせた全体がゴールです。横線の下は、the conclusion of the goal（ゴールの結論）と呼びます。「嘘」というと言い過ぎかも知れませんが、狭義のゴール（横線の下、結論）と広義のゴール（横線の上も含める）が断りなしに混ぜて使われます。もうやめて欲しい！

リファレンスマニュアルはもっとひどくて、最初のほうの説明からは次のような印象を受けます。

  サブゴール1
  サブゴール2
  ============================
   ゴール

こういう理解をしていると、後のほうの説明や他の資料に書いてあることがサッパリ意味不明になります。なんでそういうミスリードな説明をするのかなぁ。

もう一度繰り返してハッキリさせておきます。ゴールは横線の上下全体を意味します。横線の下はゴールの結論です。横線の上はゴールのコンテキストです。コンテキストは何行かに渡る場合もあるし、空のときもあります。コンテキストを構成する各行に書かれているモノをゴールの仮定（hypothesis、または premise, assumption）と呼びます。別な言い方をすると、ゴールのコンテキストは、幾つかの仮定からなります。0個（空）の仮定も許します。

サブゴールという言葉は、ゴールのあいだの相対的関係を表しています。ゴールのあいだに一種の親子関係があって、あるゴールから見て子供または子孫のゴールをサブゴールと呼んでいます。ゴールのあいだの親子関係についてはいずれ述べるでしょう。

Coqはどんなゲームソフトなのか

1個のゴールを1匹のモンスターだとしましょう。ゴールズペインはモンスターズペイン、あるいはバトルエリアとなります。証明ゲームは、モンスターを倒すゲームです。証明＝バトルを行っているあいだはバトルエリアに1匹以上のモンスターがいます。複数のモンスターがエリアにいることもあります。

我々がモンスターと戦う武器は呪文です。そう、タクティクですね。適切なタクティクを投入すれば、モンスターはだんだん弱ってきて、とどめを刺して消滅させることができます。とどめによく使われる呪文はassumption.です。ゲーム中にモンスターが増えてしまうこともあることに注意してください。

1匹のモンスター＝ゴールを消滅させることをゴールを解決（solve）するといいます。ただし、1匹のモンスター＝ゴールを解決しても、それで戦い＝証明に勝利するとは限りません。注目しているモンスター（カレントゴール）が消滅すると同時に、別なモンスターが前面に来て相手になります。バトルエリアにモンスターが1匹もいなくなったとき、我々は勝利します。勝利のあかしにQed.という呪文で締めくくります（他の勝利宣言もあります）。

先に出したゲーム事例をたどっていきましょう。ゲームの実況を文章でするのは、いかにもバカバカしいのですが、まーしょうがない。



Coq < Parameter A B : Prop.

A is assumed

B is assumed

これ(↑)は戦いの前の準備。



Coq < Theorem and_is_commutative : A/\B -> B/\A.

これ(↑)が戦い開始の宣言です。戦う相手を指定します。



1 subgoal
  ============================

   A /\ B -> B /\ A
and_is_commutative <

subgoalと出てますが、これはメインゴールですね。Coqの表示は常にsubgoalなのでsubに意味はありません。宣戦布告（Theorem）で指定した相手がバトルエリアに現れます。正確に言えば、Theoremで指定した命題を結論とするゴールが出現します。ゴールのコンテキストは最初は空です。



and_is_commutative < intros.

これ（intros）は定番の呪文です。今は、意味や効果は気にしないでください。



1 subgoal
  H : A /\ B

  ============================

   B /\ A
and_is_commutative <

ゴールの結論が単純になって、仮定（横線の上）が増えました。これは、ゴール＝モンスターが多少弱っていることを示します。次の呪文を投入します。



and_is_commutative < destruct H as [H1 H2].

1 subgoal
  H1 : A

  H2 : B

  ============================

   B /\ A
and_is_commutative <

Hという名前（ラベル）の仮定が、destruct H as [H1 H2]. により、H1とH2という2つの仮定に分解します。ゴール＝モンスターはさらに弱っています。



and_is_commutative < split.

2 subgoals
  H1 : A

  H2 : B

  ============================

   B
subgoal 2 is:

 A
and_is_commutative <

splitを使うと、ゴール＝モンスターが2匹に増えます。表示が分かりにくいのですが、subgoal 2は、同じコンテキストを持ち結論がAである新たなゴールです（[追記]注意：複数のサブゴールがいつでも同じコンテキストを持つわけではありません！[/追記]）。攻撃したつもりが相手は増強してしまった？いや、大丈夫です。数が増えてもそれぞれのモンスターは弱体化していて、容易にとどめを刺せます。



and_is_commutative < assumption.

1 subgoal
  H1 : A

  H2 : B

  ============================

   A
and_is_commutative < assumption.

No more subgoals.
and_is_commutative < Qed.

1番目のゴールにassumption.でとどめを刺すと消滅して、代わりの元の2番（subgoal 2）が正面に来ます。こいつを同じくassumption.でやっつけてしまうと、もはやバトルエリア（ゴールズペイン）にモンスター（ゴール）はいなくなり、この戦い（証明）に勝利しました。やったぜ、Qed.

老人は背後の理屈が気になる

試行錯誤をしていると、タクティクの効果が予測できるようになり、証明ゲームを楽しめるようになるかも知れません。UIのパターンとオペレーションから証明に習熟する道もあるし、若者はそうしてCoqの達人に成長するかも知れません。

しかし老人には気になることがあります。

Coqシステムは、そして自分は、いったい何をやっているんだ？
これが証明って、いったい何でだ？

こういう疑問を払拭できないのは、CoqのUIが貧弱なせいもあると思います。眼前の敵＝モンスター＝ゴールだけを表示するのは、バトルに没入するにはいいかも知れませんが、全般的な戦況が読めないのです。証明の現状を俯瞰的に眺めたいとか、出来上がった証明＝終わった戦いを（時系列ではなくて）構造的に視覚化したいとかの要望に応える機能がありません。

しょうがないので、頭のなかに証明の状況や構造を描こうと思うのですが、それに対するモデル＝考え方の基準がなんだか分からないのです。その結果、「何をやっているんだ？」「いったい何でだ？」とフラストレーションが募ります。

ゴールはシーケントなのかも知れない

Coqのゴールは、自然演繹の推論図に似ています。リファレンスマニュアルにもそれらしいことが書いてあります。それで僕は、Coqの証明は自然演繹の証明として解釈できるのだろう、と思っていました。

しかし、実際に操作した感触では、自然演繹とは違うのです。むしろ、シーケント計算に近いのか？今度はシーケント計算と対応付けようと試みました。ですが、シーケント計算とも違うところがあって、うまくいきません。

自然演繹とも違うし、シーケント計算とも違う、んもー、まったくー、と煮詰まっていたとき、次の2つのスライドを見つけました。

Title: Lecture 1 : Basics of COQ system
Author: Christine Paulin-Mohring
URL: https://www.lri.fr/~paulin/LASER/coq-slides1.pdf

Title: Proofs in Proposition Logic and Predicate Logic 1
Author: Pierre Caste'ran
URL: http://www.labri.fr/perso/casteran/CoqArt/Tsinghua/C3.pdf

どちらも説明にシーケントを使っています。純正のシーケントとは少しだけ違います。この少し違う点が僕が引っかかっていたところなんだ、と気が付きました。

1個のゴールは1個のシーケントに正確に対応します。しかし、明示的には現れない隠れたシーケントがあります。この隠れたシーケントを勘定に入れるとどうやら辻褄があいます。

ゴールとシーケント

「シーケントって何だよ？」と思っている方にはこう言いましょう。Coqのゴールの別な書き方である、と。

ゴールからシーケントへの書き換えの手順は次のとおりです。

コンテキストとして縦に並んだ名前（ラベル）付き命題を、カンマ区切りで横に並べる。
横線（イコールの並び）の代わりに、矢印「⇒」で左右を区切る。
矢印「⇒」の右側に結論の命題を書く。

実例：

  H1 : A
  H2 : B
  ============================
   B /\ A

上のゴールは、次のシーケントになります。

H1 : A, H2 : B ⇒ B ∧ A

複数のシーケントを横に並べるときは空白で区切るので、シーケント自体は空白をなるべく詰めて書いて、区切りの空白は広めに取ることにします。以下が例。

H1:A, H2:B ⇒ B    H1:A, H2:B ⇒ A

一番最初に出したコンソールのコピーはけっこうなスペースを要しましたが、シーケントにするとコンパクトに書けます。シーケントを時間順に縦方向に並べますが、このときの上下の区切りはハイフンの並びを使います。

   ⇒ A∧B → B∧A
 ----------------------------------------
   H:A∧B ⇒ B∧A
 ----------------------------------------
   H1:A, H2:B ⇒ B∧A
 ----------------------------------------
   H1:A, H2:B ⇒ B    H1:A, H2:B ⇒ A
 ----------------------------------------
   H1:A, H2:B⇒ A

上の図はCoqの証明の時間順に、上から下へと流れています。Coqの証明は通常とは逆順（backward reasoning）なので、上下を、つまり時間順を逆転させて描き直すと次のようになります（元の最下段は冗長なので省略します。）。

   H1:A, H2:B ⇒ B    H1:A, H2:B ⇒ A
 ----------------------------------------
          H1:A, H2:B ⇒ B∧A
 ----------------------------------------
          H:A∧B ⇒ B∧A
 ----------------------------------------
          ⇒ A∧B → B∧A

シーケント計算を知っている人は、これがシーケント計算の証明図になっていることが分かるでしょう。

シーケント計算については、例えば、竹内外史さんの『層・圏・トポス』の第4章に書いてあります。計算技法は載ってませんが、意味論について詳しい記述があります。Wikipediaの項目「Sequent calculus」もけっこう充実していて、そのPDF版が http://www.cs.brandeis.edu/~cs112/2006-cs112/docs/sequentcalculus.pdf にあります。

証明ゲームの裏側へ

シーケント計算の証明図の上下をひっくり返すとほぼCoqの証明過程になるのは分かったのですが、ただ単純にひっくり返すだけではうまくなくて、先に触れた隠れたシーケントを補足して、逆方向の証明を構成します。

逆方向なので、証明すべき最終的な結果（それが最初のゴール）から出発して公理へと向かう手順になります。シーケント計算の通常の証明図の描き方を思い浮かべると、一番下側から上へと逆推論図を積み上げていって証明図を完成させる感じです。大筋はそれでいいのですが、僕が最初引っかかていたような、細かい注意点はいくつかあります。

Coqの証明ゲームを、既存の論理計算に引き寄せて解釈することがいいのか悪いのか？疑問を感じるところですが、少なくとも僕自身は、そうしないと分かった気分になれないので、シーケント計算との類似性をもう少し探るつもりです。

*1:直観か直感か、毎度悩む。

*2:ゲームセマンティクスとかではない。

*3:コンソールによりけりかも知れません。コンソールがutf-8入力OKなら大丈夫かも。