余帰納的(coinductive)な型のsimpl

無限ストリームの型はCoInductiveという構文で宣言された余帰納的な型である。
無限ストリームはCoFixpointという余帰納的な関数(?)を作る構文で定義する。Fixpointは最小不動点(Coqなら「いつか必ず止まる」)だがCoFixpointは最大不動点(止まらない、無限?)になる。
coinductive型の関数適用は癖もので simpl ではβ簡約されない。 Coq'Art や アダムッチさんのチュートリアルに載っているのは、何もせずパターンマッチするだけのidentity function (frob)をrewrite (frob_eq 対象).で入れてからsimplする方法だ。よくわからんけど評価の進み方も双対的なので外から強制しないと簡約が進まないということらしい(違ったかもしれない)。
Fixpointは帰納的な型の値を「消費する」のに対し、CoFixpointは値を「生み出す」、という説明があった。つまりそういうことだ(よくわからない)。Fixpointは、引数が狭義単調減少していることを示す必要があるのに対し、CoFixpointは、再帰がコンストラクタでガードされている必要がある。つまり、再帰の各ステップで「狭義単調増加」している必要がある。…という説明は何となくわかる…かも