寄り道Coq： exactタクティクと型理論と圏論 - 檜山正幸のキマイラ飼育記 (はてなBlog)

次にCoqに関する記事を書くとすれば、「Coq入門以前」から「Coq入門」にしようと思います。

と言っておきながら、「入門」ではない重箱の隅のような事を書きます；「Coqの証明ゲームの表側と裏側（誰も書かないCoq入門以前 4）」の「証明ゲームの裏側へ」的な話題ですね。

Coqのタクティクにexactってのがあるのですが、これはかなり特殊なタクティクです。exactの引数には項（term、CoqのpCic構文の式）を書いて、これ一発でモンスター＝ゴールを仕留めます。

Coqの証明の実体は項です。カリー／ハワード対応では、Propositions-as-Types, Proofs-as-Terms と解釈するので、型がAである項tを実際に作れるなら、「命題としての型A」は「証明としての項t」により“証明された”とみなします。この事情をもう少しハッキリさせます。

型理論を少しだけ

「名前 : 型」という形を型宣言と呼びましょう。型理論では、型宣言という用語をあまり使いませんが、「型宣言」は多くの人に馴染みがある言葉だと思います。型宣言のコロンの左にある名前の用途は実にさまざまで、変数名、定数名、関数名、単なるラベルなどの解釈が可能です。特定の用途を想定しないで、単に名前（identifier）と呼ぶことにします。

A, Bなどは型だとします。x, yなどは名前だとします。A, B, x, yなどは特定の型／名前というよりは、型／名前を表すメタ変数だと捉えてください。x:A, y:B のように、型宣言をいくつか並べたカンマ区切りのリストを型コンテキスト、あるいは単にコンテキストと呼びます。長さが0のリスト、つまり空な表現も型コンテキストとして認めます。リストに同じ名前が二度以上出現するのはダメです。型コンテキスト全体をΓ, Δなどのギリシャ文字大文字で表します。

Γをなんらかの型コンテキストとして、Γに含まれる型宣言をすべて仮定して、項tの型を決めることを型付け（typing）と呼びます。型付けの例は、「型推論に関わる論理の概念と用語その5：型付けの簡単な例から型判断へ」にあります。

型付け規則（typing rules）を固定して、その規則による演繹系をTとすると、メタな命題 Γ |-_T t:B が意味を持ちます。Γ |-_T t:B の意味は次のとおりです。

型コンテキスト（型宣言のリスト）Γを仮定すると、型付けの演繹システムTにより、tの型がBであることが演繹できる。

Γ |-_T t:B はメタな命題ですが、この形を再び形式的体系で扱う記号表現と考えて、シーケント計算類似の論理計算システムを作れます。型理論では通常、シーケントを型判断（typing judgement）と呼びます。

型判断（型に関するシーケントのこと）を Γ ⇒ t:B と書きましょう。具体例を挙げます。

x:A, y:B, f:A→(B→C) ⇒ (f x y):C

この型判断（シーケント）は次のように解釈できます。

xの型はAである。
yの型はBである。
fの型はA→(B→C)である。
以上の仮定のもとで、
項(f x y)の型はCである。

exactタクティク

Coqのゴール（「ゴール」の意味は「Coqの証明ゲームの表側と裏側（誰も書かないCoq入門以前 4）」を参照）は、「⇒」の右側の項が未定になっている型判断（シーケント）と考えられます。そこで、Coqのゴールを、Γ ⇒ ?:B のような形で表します。Γは型コンテキスト、Bは型です。

Coqにおける推論（証明の基本ステップ）は逆向き推論です。まずは順方向の推論を挙げます。

   x:A ⇒ (λy:B.x):B→A
 -------------------------------↓xによるラムダ抽象
  ⇒ λx:A.(λy:B.x):A→(B→A)

逆方向の推論を表すのに、上下の位置は変えないで逆向き矢印↑を使います。

   x:A ⇒ ?:B→A
 -------------------↑intro x.
  ⇒ ?:A→(B→A)

Coqの証明手順を下から上に向かって続けると：

         *
 -------------------↑assumption.
   x:A, y:B ⇒ ?:A
 -------------------↑intro y.
   x:A ⇒ ?:B→A
 -------------------↑intro x.
  ⇒ ?:A→(B→A)

一番上段の「*」は、そこでゴールが消滅して何もないことを示す目印です。

exactは、クエスチョンマーク「?」のところに当てはまる項を直接埋めてしまうタクティクです。上の証明の最後のassumptionはexactでも書けます。

         *
 -------------------↑exact x
   x:A, y:B ⇒ ?:A
 -------------------↑intro y.
   x:A ⇒ ?:B→A
 -------------------↑intro x.
  ⇒ ?:A→(B→A)

次もexactの使用例です。ラムダ式はCoqの構文（Unicode文字使用）で書きます。

         *
 -------------------↑exact (λ y:B, x).
   x:A ⇒ ?:B→A
 -------------------↑intro x.
  ⇒ ?:A→(B→A)

いきなりexactでもかまいません。

         *
 -------------------↑exact (λ x:A, λ y:B, x).
  ⇒ ?:A→(B→A)

正しいexactの条件

exactを使えば一発でモンスター＝ゴールを仕留めることができます。しかし、exactに渡す項が何でもいいわけではありません。tを項として、exact t. がちゃんとゴールを消滅させる条件を考えてみます。

次の状況を考えるわけです。

       *
 -------------↑exact t.
  Γ ⇒ ?:B

Γは型コンテキストで、Bは個別の型ではなくて、型一般を示します。

上記の状況を順方向に直して考えると、t:B が正しい型付けであることです。

       *
 -------------↓
  Γ ⇒ t:B

Γ ⇒ t:B という型判断（シーケント）は、Γ |-_T t:B というメタな命題の表現なので、exact t. が正しいのは、Γ |-_T t:B であることに他なりません。次の具体例を考えてください。

         *
 -------------------↑exact (λ y:B, x).
   x:A ⇒ ?:B→A

この逆向き推論が表していることは、次のメタな命題です。

x:A |-_T (λ y:B, x):B→A

Coqは型付け演繹系を持っているので、メタな命題の |-_T の部分がシステムにビルトインになっています。なので、exactによって項tを渡されたとき、tとゴールを照合して型判断の検証を実施します。

大きなラムダ式／小さなラムダ式

メタな命題 Γ |-_T t:B と型判断（シーケント）Γ ⇒ t:B は内容的には同じことを意味します。「項tが、Γの仮定のもとで、型Bを持つ」ことを主張しています。このとき、<Γ | t:B> という書き方も許すことにします。

なんで三番目の記法を出すかというと、圏論との相性がいいからです。<Γ | t:B> は、「大きなラムダ式／小さなラムダ式」で紹介した大きなラムダ式です。

コンテキストΓが、x₁:A₁, ..., x_n:A_n の形のとき、<x₁:A₁, ..., x_n:A_n | t:B> は、A₁× ... ×A_n → B という射を表現します。<x₁:A₁, ..., x_n:A_n | t:B> が構文的・意味的に合法であるためには、次の条件が必要です。

項tに含まれる自由変数は、コンテキストに出現する名前の集合 {x₁, ..., x_n} の部分集合である。
項tの型は実際にBである。

大きなラムダ式は、圏の射を表現しています。そして、大きなラムダ式と型判断（シーケント）は事実上同じものです。つまり、型判断のシーケントは圏の射になっています。そして、Coqのゴールは、未知の項を含む型判断（判断つうより疑問文）なので、Coqにおける逆方向の証明は、与えられたプロファイル条件（域と余域）を満たす射を作り出す行為になっています。射を作り出すときに使っていい素材は；事前に与えられた射である公理、射の変形または組合せ操作である推論規則です。