はじめに
最近Coqの余帰納法について勉強したので、まとめてみました。余帰納法とは、簡単に言えば無限長の集合の定理証明に使われる手法です。このような証明は無限に続くデータがある性質を満たしているかを、それこそ無限に示し続ける必要があるので、いろいろと条件が複雑で通常の定理証明とは一味違います。この記事ではその内容を簡単に紹介していけたらと思います。
(Coq歴はまだ数ヶ月程度なので、間違いがあればぜひ教えていただきたいです。)
無限長のデータ
導入
Haskellのような遅延評価型の関数型言語では、無限のデータ構造に触れる機会がたくさんあります。遅延評価というのは引数を必要になったときに初めて計算する評価方法のことです。これのおかげでHaskellでは無限のデータも扱うことができます。カリーハワード同型対応により関数型言語と証明は同一視することができますが、実際にCoqでも余帰納型というデータ型によって無限データ構造を定義することができます。
具体例
例として、無限長データで最も基本的なstream型を定義していきます。stream型はConsコンストラクタと余帰納型を扱うためのCoInductiveを使って、以下のように書くことができます。
CoInductive stream (A: Type): Type :=
| Cons: A -> stream A -> stream A.
ここでは無限に続くリストを多相的に定義しています。このstream型を使って、0が無限に続くリストzerosと1が無限に続くリストonesは以下のように定義することができます。
0が無限に続くリストzeros
CoFixpoint zeros : stream nat := Cons nat 0 zeros.
1が無限に続くリストones
CoFixpoint ones : stream nat := Cons nat 1 ones.
CoFixpointとは、無限に再帰を繰り返す余再帰関数というものをCoqで扱うためのキーワードです。他にもnat型ではなく、bool型の無限長のデータを定義ずることができます。
無限にtrueが続くリストtrues
CoFixpoint trues : stream bool := Cons bool true trues.
ガード制約
ここまでいくつか無限長のデータを余帰納的に扱ってきましたが、以下の定義は可能でしょうか？
CoFixpoint looper : stream nat := looper.
実はこのような定義の仕方は不適切です。このlooperとzerosなどとの違いは、どのような関数に適用させても無限ループになるか否かという点にあります。例えば、stream型の先頭を返す関数hd_streamがあったとして、これをzerosやonesに適用すると、それぞれ0、1という結果が返ってきます。しかし、looperに適用した場合、計算は永遠に停止しません。そのため、Coqで余帰納型を扱う際は、looperのような形になっていないことを検査する必要があります。この検査で使われる条件をガード制約といい、このガード制約を満たしているとき余帰納的な定義が可能になります。
ガードとは？
ガード制約の検査は、証明項に含まれる余再帰呼び出しを表す変数が、対応する型のコンストラクタにガードされている形かどうか調べることです。導入された余再帰呼び出しを表す変数が含まれない、もしくは導入した余再帰呼び出しが含まれているが、コンストラクタにガードされている形であればガード制約を満たしていることになります。ガード制約は以下の通りです。
（1）余帰納呼び出しは、CoInductiveのコンストラクタを含まなければならない
（2）余帰納呼び出しは、CoInductiveのコンストラクタで包まなければならない
（3）余再帰呼び出しは、CoInductiveのコンストラクタの引数の一番外側で行わなければならない
（1）の反例が先ほどのlooperです。（2）と（3）の反例は以下の通りです。
（2）の反例（tl_streamはstreamの後ろを返す関数）
CoFixpoint exFail2 : stream nat := tl_stream (Cons 1 exFail2).
（3）の反例
CoFixpoint exFail3 : stream nat := Cons 1 (tl_stream exFail3).
ガード制約の検査
具体的な例を挙げて、ガード制約を使った検査について説明していきます。例として、nから始まる自然数の無限リストを返す関数countupを以下のような証明項として定義し、ガード制約の条件を満たすか見ていきます。（countup 0 = [0, 1, 2, ....]）
CoFixpoint countup (n : nat) : stream nat :=
Cons nat n (countup (S n)).
この定義にはCoInductiveのコンストラクタConsがあり、また余再帰呼び出しはそのConsコンストラクタに包まれいるので、（1）と（2）は満たしてます。では（3）はどうでしょうか？余再帰呼び出しを行っているConsの第二引数countup (S n)を見ると、一番外側でcountupを呼び出しているので、これも満たしています。
続いて今度はcountupと機能は同じだけど、定義の仕方が違うcountup'について考えていきます。（map関数は関数fとstreamを引数にとって、streamの各要素に関数f1を適用する）
CoFixpoint map f ( Cons h t ) := Cons ( f h ) ( map f t )
CoFixpoint countup' (n : nat) : stream nat :=
Cons nat n ( map S ( countup n ))
これも順番に見ていくと、ガード制約の（1）と（2）は満たしてそうです。しかし、Consの第二引数map S (countup n)では余再帰呼び出しが内側で行われてしまっています。そのため（3）を満たさず、countup'は余帰納的な定義として正しくないことが分かりました。
余帰納法を使った証明
onesとzerosの全ての要素に1を足した2つのstreamが等しいことを余帰納法によって証明していきます。最初にstream型の全ての要素に1を足すallSを定義します。
CoFixpoint allS s : stream nat :=
match s with
| Cons _ h t => Cons _ (S h) (allS t)
end.
続いて、引数としてとった2つのstreamが等しいstream_eqを定義します。
CoInductive stream_eq (A: Type) : stream A -> stream A -> Prop :=
| SEqCons : forall h x y ,
stream_eq A x y -> stream_eq A ( Cons _ h x ) ( Cons _ h y ).
このstream_eq は、自然数の無限リスト (Cons h x) と (Cons h y) が stream_eq を満たしているとき，それぞれの先頭要素を除いた自然数の無限リスト x と y が stream_eq を満たしていることを余帰納的に定義しています。この stream_eq を用いて，証明すべき命題は stream_eq ones (allS zeros) と書くことができます。このように余帰納的に定義された性質についての証明は，余帰納法で行っていきます。
では実際に証明してみましょう。
Lemma ones_succzeros_eq : stream_eq nat ones ( allS zeros ).
cofix ones_succzeros_eq .
assumption.
Qed.
しかし、この方法では以下のようなエラーメッセージによって中断されてしまいます。
Recursive definition of ones_succzeros_eq is ill-formed.
In environment
ones_succzeros_eq : stream_eq nat ones (allS zeros)
Unguarded recursive call in "ones_succzeros_eq".
Recursive definition is: "ones_succzeros_eq".
無限ループの形の証明項となるため，ガード条件を満たさないことが問題のようです。
そこで追加で関数を定義していきます。
Definition frob A (s : stream A) : stream A :=
match s with
| Cons _ h t => Cons _ h t
end.
Theorem frob_eq : forall A (s : stream A), s = frob _ s.
destruct s; reflexivity.
Qed.
今度はこれらを使って、証明してみます。
Lemma ones_succzeros_eq : stream_eq nat ones ( allS zeros ).
cofix ones_succzeros_eq .
rewrite ( frob_eq nat ones ).
rewrite ( frob_eq nat ( allS zeros )).
simpl .
apply SEqCons .
apply ones_succzeros_eq .
Qed .
実はこれで最後まで証明を完了させることができます。
この証明でポイントになるには2つの書き換え部分です。
rewrite ( frob_eq nat ones ).
rewrite ( frob_eq nat ( allS zeros )).
これらによって、stream_eq nat ones (allS zeros)は以下の形に書き換えられます。
1 subgoal
ones_succzeros_eq : stream_eq nat ones (allS zeros)
______________________________________(1/1)
stream_eq nat (frob nat ones) (frob nat (allS zeros))
そして、
simpl.
によって、ストリームを簡約し以下のようになります。
1 subgoal
ones_succzeros_eq : stream_eq nat ones (allS zeros)
______________________________________(1/1)
stream_eq nat (Cons nat 1 ones) (Cons nat 1 (allS zeros))
つまり、frob_eqを使った書き換えでは、onesとallS zerosをそれぞれ展開するような処理を行っていました。あとはstream_eqのコンストラクタを適用していくだけです。
apply SEqCons .
1 subgoal
ones_succzeros_eq : stream_eq nat ones (allS zeros)
______________________________________(1/1)
stream_eq nat ones (allS zeros)
apply ones_succzeros_eq .
No more subgoals.
証明の流れをざっくり書くと、
stream_eq ones (allS zeros) → stream_eq (frob ones) (frob (allS zeros))
→ stream_eq (Cons 1 ones) (Cons 1 (allS zeros))
→ stream_eq ones (allS zeros)
→ …
このように、余帰納法では性質が満たされていることを部分的に証明いく形になります。
まとめ
今回はCoqで余帰納的なデータを扱い方やその制約についてざっくりと話してきました。特にガード制約に関してはとにかく分かりやすさを重視したので、かなり大雑把な説明でしたが、本当はしっかりとしたアルゴリズムがあるらしいです。今後はより厳密な部分を学びながら、Coqを使いこなせるようになりたいと考えています。
参考文献
Certified Programming with Dependent Types 5 Infinite Data and Proofs
Coq によるビットストリームの余帰納的な形式化