問題タブ [coq]

私はタイプを持っています

リストの先頭からタイプを取得し、option dその後リスト全体を確認したいと思います。私のコードは次のようになります。

私の質問は、リスト全体でテストしたいので、if forallb (fun li => forallb (fun ci =>do_something ci d))ls)l'追加したテストです。しかし、私はその議論をまったく使用しませんでした。forallb (fun li =>...)l'li

編集：私の質問はに焦点を当てていif forallb (fun li => forallb (fun ci => do_something ci d))ls)l'ます。forallb (fun li =>リストの残りの部分でテストしたいので、追加しましたl'。このテストforallb (fun liをアーカイブすることはできif (forallb (fun ci => do_something ci d))lsませんが、リストでこの状態を再度テストする方法がわかりませんl'。

編集

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

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

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

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

「C:\Users\WK\Desktop\Personal\coq-project」フォルダーに保存された Makefile を含む、多数のファイル (x1.v、x2.v、... xn.v など) を含む Coq プロジェクトがあります。 Windows 7 マシンの「C:\Coq」に Coq 8.3 をインストールしました。

Coq プログラム (ファイル) は相互に依存しています。Coq で単一のプログラム (x1.v など) を実行するにはどうすればよいですか? Coq でファイルを開き、それを理解するために 1 行ずつコンパイルしたいのですが、(.vo) 形式のファイルがなく、それぞれにインポートされたファイルが多数あるため、エラーが発生します。コマンド coqc、coqtop、make、またはこれらの組み合わせが使用されていると思いますが、コマンド、引数、および順序の正確な形式はわかりません。上記のパスを念頭に置いて、完全なパスを含む完全なコマンドを教えてください。

ありがとう、

ウィラヤット

• Coq を少し学んで以来、実際には論理命題である、いわゆる除算アルゴリズムの Coq 証明を書きたいと思っていました。forall n m : nat, exists q : nat, exists r : nat, n = q * m + r
• 私は最近、Software Foundationsから学んだことを使用して、そのタスクを達成しました。
• Coq は建設的な証明を開発するためのシステムであり、私の証明は事実上、値qとrから適切な値mを構成する方法nです。
• Coq には、Coq のアルゴリズム言語 (Gallina) のアルゴリズムを、Haskell などの汎用関数型プログラミング言語に「抽出」するための興味深い機能があります。
• これとは別に、divmod 操作を Gallina として記述し、それFixpointを抽出することができました。そのタスクはここで検討しているものではないことに注意してください。
• Adam Chlipala は、Certified Programming with Dependent Typesで次のように書いています。

Haskell への私の証明に暗示されているアルゴリズムを抽出することさえ可能ですか? 可能であれば、どのように行われますか?

2進数の自然数（ビットのリスト）の先行関数を定義しようとしています。関数の入力を、トリミングされた（先行ゼロがない）数値と正の数値（つまり、ゼロの前身について心配する必要がない）に制限したいと思います。

演算子の定義は次のpredとおりです。

私の最初の義務は次のとおりです。

しかし、私はそれを解決する方法がわかりません。

矛盾は明らかににありH2ます。しかし、それはに依存するのでH1、私はただrewrite nat1でEmpt、そして次に(is_pos Empt H1)ですることはできませんFalse。

これをどのように証明すればよいですか？

Coqで定理を証明しようとしていますが、発生した問題を解決できません。私は解決しようとしています：

私はCoqを初めて使用するので、それが実際に何を意味するのかわかりません。私はインターネットでいくつかの調査をしましたが、解決策を見つけることができませんでした。この問題が何から来ているのか誰かが知っていますか？

Coq で証明しようとしていますが、すでに定義および証明されている補題を使用したいと考えています。以下のコードは可能ですか？

上記では、~(A /\ B) が ~(B /\ A) と同じであることを証明するために、A /\B が B /\ A と同じであるという事実を使用したいと考えています。私の証明された補題を使用することは可能ですか?

帰納述語についての簡単な証明に行き詰まっています。自然の 0 が正ではないことを証明する必要があります。ここで、自然はビットのリストであり、0 は 0 のビットのみを含む任意のリストです。

依存型を使用した認定プログラミングのこの章では、を使用することをお勧めしているようですinversionが、エラー メッセージが表示されます。

私は現在、SoftwareFoundationsという本を読んでいます。定理が定義されるとき、私は接続詞がより理にかなっていると私が信じる含意の連鎖をしばしば見ます。たとえば、鳩の巣原理を定義する際に、著者は次のように書いています。

この定義は、次のようになっていると、私にはもっと意味があります。

最初のバージョンが正しいのはなぜですか？接続詞がより適切ではないのはなぜですか？

それはほんの一例です。より一般的には、接続詞がcoqの含意の連鎖を支持して避けられているように見える理由を尋ねています。

forall nat1: Nat, Trim nat1 -> Trim (pred nat1)以前、私は次のの定義を証明することができましたpred。

しかし、次の新しい定義ではpred、証明する方法がわかりませんforall nat1: {nat2: Nat | Trim nat2 /\ Pos nat2}, Trim (pred nat1)。

誰かが私にヒントを教えてもらえますか？で何かを証明することについては何も知りませんsig。または多分私は何か間違ったことをしています。知らない。完全なコードはここにあります。ここに前のコード。