問題タブ [coinduction]

次のように無限ストリームを定義しました。

そして、ストリーム内のいくつかの要素が最終的に述語を満たすことを示す帰納型:

ストリームの先頭が述語を満たすまで、ストリームの要素をスキップする関数を書きたいと思います。確実に終了するには、要素が最終的に述語を満たすことを知っておく必要があります。そうしないと、永遠にループする可能性があります。したがって、 の定義をEventually引数として渡す必要があります。さらに、関数は、終了を証明するためだけに存在するため、述語に計算上依存するべきではありませんEventually。そのため、消去された引数にしたいと考えています。

ここに問題があります。定義の穴を埋めたいと思います。スコープ内からcontra、ストリームの先頭が を満たさないことがわかっているためP、最終的に の定義により、ストリームの末尾の要素が を満たさなければなりませんP。Eventuallyこのコンテキストで が消去されていなければ、単純に述語のパターン マッチを行い、そのケースが不可能であることを証明できhereます。通常、これらのシナリオでは、次の行に消去された補助関数を記述します。

このアプローチの問題は、Eventually証明が の構造的に再帰的な引数でdropUntilあり、Agda が関数定義の「内部を調べない」ため、この補助関数を呼び出しても終了チェッカーを通過しないことです。

私が試した別のアプローチは、上記の消去された関数を の定義にインライン化することですdropUntil。残念ながら、私はこのアプローチでもうまくいきませんでした -case ... ofここで説明されているようなの定義を使用https://agda.readthedocs.io/en/v2.5.2/language/with-abstraction.htmlも終了チェッカーに合格しませんでした。

私は (消去された型ではなく型を使用して) 受け入れられる同等のプログラムを Coq で作成したPropので、私の推論が正しいと確信しています。Coq が定義を受け入れ、Agda が受け入れなかった主な理由は、Coq の終了チェッカーが関数定義を展開し、「補助消去関数」アプローチが成功したためです。

編集：

これはサイズのある型を使用した私の試みですが、終了チェッカーに合格せず、その理由がわかりません。

私は単純な怠惰なバイナリツリーの実装を持っています:

そして、次のプロパティ:

有限ツリーには無限分岐がないという定理を証明したいと思います。

...しかし、最初のいくつかの戦術で迷子になりました。仮説自体はかなり些細なことのように思えますが、私はそれから始めることさえできません. そのような定理の証明はどのように見えるでしょうか?

帰導型に関する「帰導原理」を証明できますか? たとえば、ストリーム タイプの結合原理の擬似コードは次のようになります。

これは正しいと思いますが、Coq や Agda でそれを証明する方法が思いつきません。

Haskell で同種ストリームと異種ストリームの両方を定義する方法を理解しています。

異種ストリームの特定のケースとして、一定のストリームをどのように定義できますか? 定数型のストリームの型ファミリを定義しようとすると、「リダクション スタック オーバーフロー」エラーが発生します。これは、型チェック アルゴリズムが十分に怠惰ではなく、型のConstant aストリーム全体を計算しようとすることに関係していると思います。

この問題を回避し、一定の異種ストリームを定義する方法はありますか? 代わりに試してみるべき他の同様の構造はありますか？