天泣記

最近、少し Coq を勉強していて、False について納得するのに困難を感じていた。

悩んでいた話を忘れる前に書いておこう。

False は矛盾を表現する命題である
命題と型、証明とプログラム (型つきラムダ計算の項) が対応しているというカリー-ハワード同型対応という関係が知られている
False は命題なので型でもある
Coq で False は Inductive False : Prop :=. と定義されている。これはコンストラクタが存在しない代数的データ型である
コンストラクタがないので、値はない (値を生成することはできない)
矛盾から任意の命題が導けるという命題は、False 型を受け取って A 型を返す関数型 (False -> A) に対応する
False -> A を Coq で証明すると次のプログラムが生成される
```
fun (A : Prop) (H : False) => match H return A with end : forall A : Prop, False -> A
```
これは False 型の引数 H を受け取って、A 型を返す関数である。この関数が存在することによって False -> A が証明されたことになる
match 式の with と end のあいだには各コンストラクタに対応して分岐する節が入るが、False にはコンストラクタがないので空になっている
match 式自体の型は A とされているが、それと矛盾するものはなにもない (分岐がひとつもない) ので問題はない
そんな分岐がない分岐は実行できないし問題大有りだろうと感じるわけだが、そもそも False 型の値は存在しないので、引数を用意できず、この関数を呼び出すことはできないのでやっぱり問題はない
また、False は矛盾なので、証明できないはずである。False を証明しようとすると、False 型のプログラムを生成することになる。それはできちゃうんじゃないの、と最初思ったのだが、結局はできないっぽいのが感じられるようになった。まずコンストラクタはないので使えない。上のように任意の命題を導くことができるケースでは (A に False を割り当てることにより) False 型を生成できるが、それはもともと False 型の引数があるからで、矛盾から矛盾を導けるのは問題ない (False 型の引数がないのであれば、空の match 式は使えない)

順列組み合わせについてもけっこう悩んだ。ふたつのリストが順列組み合わせの関係にあるという Permutation という述語は以下のように定義される。

Inductive Permutation : list A -> list A -> Prop :=
| perm_nil: Permutation [] []
| perm_skip x l l' : Permutat|on l l' -> Permutation (x::l) (x::l')
| perm_swap x y l : Permutation (y::x::l) (x::y::l)
| perm_trans l l' l'' : Permutation l l' -> Permutation l' l'' -> Permutation l l''.

空リストと空リストは順列組み合わせ (perm_nil)、順列組み合わせとなっている l, l' があったときに先頭に同じ要素を前置したものは順列組み合わせ (perm_skip)、長さ2以上のリストで、先頭の2要素をひっくり返したものは順列組み合わせ (perm_swap)、推移律 (perm_trans)

これらで生成されるものが順列組み合わせであることは明らかなのだが、すべての順列組み合わせがこれらで生成できるというのは納得できなかった

納得するまでにけっこう時間がかかったのだが、こういうことだろう。

先頭要素が異なるリスト a::l と b::l' が順列組み合わせなら、l の中には b が入っているはずで、そうすると l と b::l'' が順列組み合わせになるように l'' を選べる。そうやって選んだ l'' を使うと、perm_skip により a::l と a::b::l'' は順列組合わせ。a::b::l'' と b::a::l'' は perm_swap により順列組み合わせ。a::l'' と l' は順列組み合わせのはずなので、perm_skip により b::a::l'' と b::l' も順列組み合わせ。だからひとつ短いリストの順列組み合わせの関係に帰着できる。

ここで、「はず」というのが 2回でてくる。l と b::l'' および a::l'' と l' の順列組み合わせの関係は、リストの長さがひとつ短いものに対する関係なので、帰納法みたいな感じで仮定してよい。というか、これはリストの長さに関する帰納法をやっているわけだよな。

天泣記

2015-01-27 (Tue)