問題タブ [totality]

Coq で Ackermann-Peters 関数を定義しようとしていますが、理解できないエラー メッセージが表示されます。ご覧のとおりa, b、Ackermann の引数をペアでパッケージ化していますab。引数の順序付け関数を定義する順序付けを提供します。次に、Functionフォームを使用して Ackermann 自体を定義し、引数の順序付け関数を提供しabます。

私が得るのは、次のエラーメッセージです。

エラー: そのようなセクション変数または仮定はありません: ack。

何が Coq を悩ませているのかわかりませんが、インターネットを検索すると、再帰呼び出しが一致内で発生する場合に、順序付けまたはメジャーで定義された再帰関数の使用に問題がある可能性があるという提案が見つかりました。ただし、射影fstおよびsndを使用するとif-then-else、別のエラー メッセージが生成されました。誰かが Coq で Ackermann を定義する方法を提案できますか?

編集

次のようなエラーメッセージが表示されました。dpProofへの再帰呼び出しの主引数は次のとおりです。

相互再帰を使用せず、ネストされた固定小数点を使用すると、結合されて終了チェッカーに合格します。これが正常に結合されたコードです。

終了チェッカーに合格できない理由を詳しく知りたいのですが。彼らが議論の減少を推測できないからですか？相互再帰を使用して関数を表現する方法はありますdpGraphProcか？

dpGraphProcまた、リスト全体をチェックする関数を作成するにはどうすればよいですか？ここでは、引数の使い方がわかりませんcs'。

私はCoqをいじっています。具体的には、マージソートを実装して、それが機能することを証明しようとしています。

実装の私の試みは次のとおりでした：

この結果として私が得るエラーは次のとおりです。

これらのエラーの私の解釈は、lとl0は、頭のないls、x、xのないls、およびxの後の要素（yと呼ぶことにしたと思います）です。私がこれらのリストの1つで再帰せず、代わりにローカルで定義されたリストで再帰したのは気が狂っています。

パターンマッチから直接得られるものにのみ再帰することは許可されていますか？はいの場合、これは厳しい制限のようです。それを回避する方法はありますか？Coqは関数が終了することを認識できないと思います。左右がxsよりも小さいことを証明する方法はありますか？

game組み合わせゲームの誘導型を定義しようとしています。lessOrEq2 つのゲームが、greatOrEq、lessOrConfまたはであるかどうかを判断する比較方法が必要greatOrConfです。次に、2 つのゲームが両方とも である場合に等しいかどうかを確認できlessOrEqますgreatOrEq。

しかし、このチェックを行うための相互再帰的なメソッドを定義しようとすると、次のようになります。

エラー: の減少引数を推測できませんfix。

これは、再帰呼び出しごとにどちらか一方のゲームのサイズだけが減少するためだと思います (両方ではありません)。これをCoqにどのように示すことができますか?

これが私のコードです。失敗する部分は、 、 、 の相互再帰的gameCompareなinnerGCompare定義listGameCompareですgameListCompare。

aと の間の累積和を計算すると終了することを証明したいと思いbます。

Acc lt xこのように、再帰が減少することを示すために用語を使用します

すべてのサブゴールをクリアしますが、Qedステートメントでの型チェックは行いません。Coq は次のように不満を述べています。

L1再帰呼び出しの用語の引数が実際には小さいことを示すために何らかの形で使用する必要があると思いHますが、どうすればよいですか?

Coq で自然除算を計算する関数を作成しようとしていますが、構造的な再帰ではないため、定義に問題があります。

私のコードは次のとおりです。

ご覧のとおり、Coq は私の関数 div が好きではありません。

エラー: の減少引数を推測できませんfix。

Coq でこの関数の終了証明を提供するにはどうすればよいですか? n>O ^ n<=m -> (mn) < m の場合、証明できます。

sの戦術のようなものはありsimplますProgram Fixpointか？

特に、次の些細なステートメントをどのように証明できますか?

明らかに、このおもちゃの例には必要ありませんが、手動でProgram Fixpointの終了を証明する必要がある、より複雑な設定で同じ問題に直面しています。Program Fixpoint

次のコードが提示された場合:

イドリスはエラーを出します:

このコードを他のいくつかの方法で書き直しましたが、Idris に全体として認識させることができません。それが合計であるというのは私が間違っているのでしょうか、それとも Idris が合計であると判断できないだけですか? それが本質的に合計である場合、イドリスがそれを合計として認識するようにどのように書き直すことができますか?