問題タブ [coinduction]

と述語を取り、プロパティが保持するストリームの最長プレフィックスをStreamとして返すCoq 関数を作成しようとしています。listこれは私が持っているものです:

しかし、この関数で計算を実行しようとすると、すべての定義が展開された非常に大きな用語が得られます。理由は定かではありませんが、Coq が総帰納的Streamな議論を展開することに消極的であると推測しています。次に例を示します。

これを考えると、Eval compute in take_while (fun s => lt_dec (hd s) 5) (nats 0) (increasing_nats 0 5)上で述べたように、コマンドは非常に大きな項につながります。

誰でもこれについてのガイダンスを教えてもらえますか?

Prolog では、統合X = [1|X]は無限のリストを取得するための適切な方法ですか? SWI-Prolog には問題はありませんが、GNU Prolog は単にハングします。

ほとんどの場合、リストを次のように置き換えることができることを知っています

しかし、私の質問はX = [1|X], member(Y, X), Y = 1、「正気の」Prolog実装で式を使用できるかどうかです。

Coqの「実践的結合」の最初の例を証明しようとしています。最初の例は、整数の無限ストリームの辞書編集順序が推移的であることを証明することです。

Guardedness 条件を回避するための証明を定式化できていません

これが私のこれまでの開発です。まず、無限ストリームの通常の定義です。次に、 と呼ばれる辞書編集順序の定義lex。そして最後に、推移性定理の失敗した証明。

これが私が証明したい補題です。最終的に からの「仮説」を使用できるようになることを期待して、コンストラクターを適用できるようにゴールを準備することから始めますcofix。

ここから先はどうすればいいですか？ヒントをありがとう！

• 編集

Arthur の (いつものように!) 有益で啓発的な回答のおかげで、私も証明を完成させることができました。参考までに私のバージョンを以下に示します。

補題を使用して、とcons_htの値を「拡張」します。ここ (と)の定義は、実用的結合の逐語的な定式化により近いです。Arthur は、Coq が値を自動的に拡張する、より洗練された手法を使用しています。s1s3lexheadtail

私は使っている：

次のCoInductiveタイプを定義しましたstream:

次に、次のCoFixpoint定義を定義しようとしましたzeros。

ただし、代わりに次のエラーが発生しました。

変数を明示的にインスタンス化する必要があることがわかりましたA：

ACoq が の型を単独で推測しないのはなぜですか? の型を推測するにはどうすればよいAですか?

私はストリームに似たものを書いてきました。各ファンクターの法則を証明することはできますが、それが合計であることを証明する方法がわかりません。

与えます:

全体性チェッカーも通過するcodataに対するファンクターの法則を証明するトリックはありますか?

初めての投稿です、間違っていたらすみません。

Coq では、Stream のような帰納的型には決定可能な等価性がないのではないかと思います。つまり、2 つのストリーム s と t が与えられた場合、s=t か ~(s=t) かを識別することはできません。これは、Coq のすべての導帰型に当てはまると思います。

スタック交換による簡単なグーグル検索と検索では、確認は得られません。誰かがこれを確認したり、私を修正したりできますか?

任意の帰納型はそのように定義されます

inductionタイプがあり(f a -> a) -> Ind f -> aます。これには、共誘導と呼ばれる二重の概念があります。

coinductionタイプがあり(a -> f a) -> a -> CoInd fます。inductionとが二重であることに注意してくださいcoinduction。帰納的および共導的なデータ型の例として、このファンクターを見てください。

再帰がなければ、Ind StringFは有限文字列であり、有限文字列CoInd StringFまたは無限文字列です (再帰を使用すると、それらは両方とも有限文字列または無限文字列または未定義文字列になります)。Ind f -> CoInd f一般に、任意の Functorに変換できfます。たとえば、ファンクター値を共導型にラップできます

Maybeこの操作は、各ステップに余分な操作 (パターン マッチング) を追加します。これは、O(n)オーバーヘッドが発生することを意味します。

Ind fとをwrap得るために帰納法を使うことができますCoInd f。

これはO(n^2)。(最初のレイヤーを取得するのは ですO(1)が、n 番目の要素はO(n)入れ子になったMaybes によるため、この合計になります。) 二重に、帰納型を取り、その最上位の Functor レイヤーを明らかにする をO(n^2)定義できます。cowrap

inductionいつもO(n)そうですcowrap。

からとcoinductionを生成するために使用できます。CoInd fcowrapInd f

これもO(n)要素を取得するたびに、合計でO(n^2).

Ind f私の質問は、再帰を (直接的または間接的に) 使用せずにCoInd f、O(n)時間内に変換できるかどうかです。

私は再帰でそれを行う方法を知っています (に変換Ind fしてFix fからFix f(CoInd f最初の変換はO(n)に変換されますが、 からの各要素CoInd fはO(1)であり、2 番目の変換のO(n)合計は になりO(n) + O(n) = O(n)ます))、それなしで可能かどうかを確認したいと思います。

直接的または間接的に再帰を使用していないことconvertに注意してください。convert'気の利いたですね！