Coqの余帰納法についてまとめました

# はじめに
最近Coqの余帰納法について勉強したので、まとめてみました。余帰納法とは、簡単に言えば無限長の集合の定理証明に使われる手法です。このような証明は無限に続くデータがある性質を満たしているかを、それこそ無限に示し続ける必要があるので、いろいろと条件が複雑で通常の定理証明とは一味違います。この記事ではその内容を簡単に紹介していけたらと思います。

<font color="blue">(Coq歴はまだ数ヶ月程度なので、間違いがあればぜひ教えていただきたいです。)</font>

# 無限長のデータ
### 導入
Haskellのような遅延評価型の関数型言語では、無限のデータ構造に触れる機会がたくさんあります。遅延評価というのは引数を必要になったときに初めて計算する評価方法のことです。これのおかげでHaskellでは無限のデータも扱うことができます。カリーハワード同型対応により関数型言語と証明は同一視することができますが、実際にCoqでも余帰納型というデータ型によって無限データ構造を定義することができます。

### 具体例
例として、無限長データで最も基本的なstream型を定義していきます。stream型はConsコンストラクタと余帰納型を扱うためのCoInductiveを使って、以下のように書くことができます。
```coq
CoInductive stream (A: Type): Type :=
| Cons: A -> stream A -> stream A.
```
ここでは無限に続くリストを多相的に定義しています。このstream型を使って、0が無限に続くリストzerosと1が無限に続くリストonesは以下のように定義することができます。

0が無限に続くリストzeros
```coq
CoFixpoint zeros : stream nat := Cons nat 0 zeros.
```

1が無限に続くリストones
```coq
CoFixpoint ones : stream nat := Cons nat 1 ones.
```
CoFixpointとは、無限に再帰を繰り返す余再帰関数というものをCoqで扱うためのキーワードです。他にもnat型ではなく、bool型の無限長のデータを定義ずることができます。

無限にtrueが続くリストtrues
```coq
CoFixpoint trues : stream bool := Cons bool true trues.
```
<!--
### 余帰納法を使った証明
#### 帰納法
Coqではタクティクと呼ばれるコマンドを使って、証明を行います。以下では、n+0=nを帰納法を表すinductionタクティクを使って証明を行っています。
```coq
Theorem plus_n_O : forall n:nat, n = n + 0.
Proof.
  intros n. induction n as [| n' IHn'].
  - reflexivity.
  - simpl. rewrite <- IHn'. reflexivity. Qed.
```
ここでは通常の帰納法と同じように、n+0=0を示すためにP(0)とP(n')->{(S n')の二つをそれぞれ証明しています。(Coqではn'+1をS n'と書く)

#### 余帰納法
Coqでは帰納法だけでなく、余帰納的に定義された性質についての証明を行う余帰納法も扱うことができます。今回は例として上で定義したonesとallS zerosが等価であることを証明していきます。allSとはstream型の全ての要素に1を加算するような関数です。
-->


# ガード制約
ここまでいくつか無限長のデータを余帰納的に扱ってきましたが、以下の定義は可能でしょうか？
```coq
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の後ろを返す関数）
```coq
CoFixpoint exFail2 : stream nat := tl_stream (Cons 1 exFail2).
```

（3）の反例
```coq
CoFixpoint exFail3 : stream nat := Cons 1 (tl_stream exFail3).
```

### ガード制約の検査
具体的な例を挙げて、ガード制約を使った検査について説明していきます。例として、nから始まる自然数の無限リストを返す関数countupを以下のような証明項として定義し、ガード制約の条件を満たすか見ていきます。（countup 0 = [0, 1, 2, ....]）
```coq
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を適用する）
```coq
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を定義します。
```coq
CoFixpoint allS s : stream nat :=
  match s with 
  | Cons _ h t => Cons _ (S h) (allS t) 
  end.
```
続いて、引数としてとった2つのstreamが等しいstream_eqを定義します。
```coq
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) と書くことができます。このように余帰納的に定義された性質についての証明は，余帰納法で行っていきます。

では実際に証明してみましょう。
```coq
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".
```
無限ループの形の証明項となるため，ガード条件を満たさないことが問題のようです。
そこで追加で関数を定義していきます。
```coq
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.
```
今度はこれらを使って、証明してみます。
```coq
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つの書き換え部分です。
```coq
 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))
```
そして、
```coq
 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のコンストラクタを適用していくだけです。
```coq
 apply SEqCons .
```
```
1 subgoal
ones_succzeros_eq : stream_eq nat ones (allS zeros)
______________________________________(1/1)
stream_eq nat ones (allS zeros)
```
```coq
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](http://adam.chlipala.net/cpdt/html/Coinductive.html#ones%27)
[Coq によるビットストリームの余帰納的な形式化](https://www.topic.ad.jp/ipsj-tohoku/lib/exe/fetch.php?media=report:2019-5-4-4.pdf)