問題タブ [coq]

私はメイクファイルを持っています：

コマンドを追加しcoqtop -R coqdirます。コンピューターに物理パスを指定する必要がありますが、このディレクトリはユーザー ディレクトリに依存します。( ~/color/trunk/color/devel/gwen Devel and ~/color/trunk/color CoLoR)。

物理パスを指定せずにプログラムを呼び出して結合する別の方法はありますか?

coq で基本ライブラリをインポート解除または非表示にする方法はありますか?

tmpcoq から ocaml に抽出した後に生成されるフォルダーがあります。

main.mlで 1 つの関数を呼び出すために使用するファイルですcpf0。

Cpf0.proofバインドされていないというエラーが表示されました。使用しようとしました: (proofに存在しCpf0ます)。

同じエラーが発生しました。

Ocaml リンク:ocamlc -I tmp -c main.ml

受け入れない理由がわかりませんCpf0か？

しかし、open Cpf0;;単独では、リンクしてもエラーは発生しません。の別のファイルでテストしましたtmpが、そのファイルのすべての機能を使用できます。

私はファイルを持っています：

• String0.mlから抽出しましたString.v（Coqライブラリからです）

• String.ml: Ocamlの文字列ライブラリです

テストファイルを Coq から Ocaml に展開した後、Ocaml のライブラリで使用したいので、すべてをString.mlに置き換える置換コマンドを作成します。String0String

問題はファイルtest.vにあります。定義の1つを使用しました：

関数string_decは Ocaml のライブラリにはありませんが、Coq の文字列ライブラリにはあります

そのため、コンパイル時にエラーが発生しますtest.ml

エラー: バインドされていない値 string_dec

すべての抽出ファイルに Ocaml の文字列ライブラリを使用したいと考えています。どうすればコンパイルできますstring_decか?

私は抽出変換natを行っていますbig_int

ライブラリを使用したとき: ExtrOcamlNatBigInt、正しい型を返しませbig_intんOcaml

nat_caseだから私はそれを修正します（ファイルExtrOcamlNatBigInt）が、Ocamlのライブラリには function がないため、関数を定義する方法が見つかりBig_intませんnat_case。

nat_casebyの 2 番目の定義を定義しようとしています。

2 番目の定義を使用した後の結果を次に示します。

n次の行でエラーが発生しましたelse f0 (n - one):

ファイル "Datatypes.ml"、68 行目、51 ～ 52 文字目: エラー: この式には Big_int.big_int 型がありますが、int 型の式が予期されていました

minus( -) のせいだと思います。

minus抽出も変更します：

nat_caseの関数を定義するのを手伝ってくれませんBig_intか? どうもありがとうございました。

この質問は、Emacs の Proof General 内で Coq モードを設定することに関するものです。

Emacs に Coq のキーワードと表記を対応する Unicode グリフに自動的に置き換えさせようとしています。funギリシャ語の小文字のラムダ λ や、全称量化記号 ∀ などを定義forallすることができました。単語の記号を定義するのに問題はありませんでした。

問題は、演算子=>、->、<->などを Unicode シンボル ⇒→↔ に定義しようとすると、Coq の対応する Unicode グリフに置き換えられないことです。ただし、*scratch*テストすると、バッファ内で置き換えられます。同じメカニズムを使用して、Unicode グリプを Coq 表記と一致させています。

問題は、Coq モードが特定の句読点を特別なものとしてマークするため、Emacs が私のコードを無視してそれらを Unicode グリフに置き換えることにあると思われますが、よくわかりません。誰かが私のためにこれに光を当てることができますか?

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

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

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

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

こんにちは、Coq から Ocaml への抽出を書いています。型を変換したいと思います。

しかし、私はタイプを維持したいZですint

これらの条件を抽出するために私が行っているコードは次のとおりです。

Coq のライブラリ ( BinInt.v )でZ -> int定義されているため、保持することはできません。Z

エラーが発生しました: (function coq_Zdouble_plus_one)

ファイル「BinInt.ml」、38 行目、4 ～ 5 文字目:

エラー: この式は int 型ですが、式は int32 型である必要があります

を抽出すればZ -> int32OKですが、私が望むものではありません。

偶数の性質を証明するための帰納仮説を書こうとしています。以下を定式化し、証明した。

それが証明されているという事実にもかかわらず、それを使用しようとすると、エラー メッセージが表示されます。

誘導仮説の問題点、またはそれを適用する方法を教えてください。

ありがとう、

マイヤー