問題タブ [coq]

それが私の質問の正しい場所であることを願っています。実は私は coq ユーザーで、「Mac OS X Lion 10.7.4」で ocaml を使って新しい戦術を実装しようとしています。必要なライブラリをすべてインストールしました。私の ocaml ファイルをコンパイルした後、それを coq にインポートしようとすると (私は Proofgenral と Aquamacs を使用しています)、エラー Error: Dynamic link not supported. が表示されます。長い検索の結果、ライブラリのリンクに問題があることがわかりましたが、修正方法が見つかりません。

Coqにおける存在例化と存在汎化の簡単な例を教えてもらえますか？を証明したいとき、を使用するものexists x, PはどこにPありますか、私はしばしば名前を付け（またはそのようなものとして）、Pを操作したいと思います。これはCoqの1つである可能性がありますか？Propxxx0

ある性質を満たすオブジェクトが存在することを示す定理があります。オブジェクトを構成することによって、この定理を証明しました。次に、別の証明として、第 2 の定理のステートメントで、第 1 の定理で定義されたオブジェクトを参照したいと思います。Qed ではなく Defined でプルーフを閉じれば、オブジェクトにアクセスできるはずですが、アクセスする方法がわかりません。例えば：

定理 T1: 存在 x, P x. 証拠。...定義されています。

定理 T2: T1 で構築された同じ x に対して、Q x \/ R x。証拠。... ケド。

これをCoqでどのように表現しますか?

プルーフチェッカーcoqでドメインを定義しようとしています。どうすればよいですか？

私はと同等のことをしようとしていますV in [0,10]。

私はやろうとしましたが、これはCoqに従っていないDefinition V := forall v in R, 0 <= v /\ v <= 10.などの定数の問題につながります。0V

私の証明では、A /\ B /\ C私の仮定に がある問題に出くわし、証明する必要があり(A /\ B) /\ Cます。これらは論理的にはまったく同じですが、coq はこれらを では解決しませんassumption.。

私は公理を適用してこれらを解決してきましたが、これを処理するためのよりエレガントな (そして正しい) 方法はありますか?

形式化されたものを証明する必要があります。2 つの関数があり、いくつかの文字列と文字列の配列を取得し、一致するかどうかを比較して、bool を返します。補題で両方をテストし、検証したいと思います。プログラミングでは、関数は次のようになります。

両方の関数が true を返し、それを証明する場合に true になるはずの Coq の補題を述べたいと思います。お気に入り

質問:

1) これらの関数を定義するにはどうすればよいですか? これらは帰納関数でも再帰関数でもありません（私はそう思います）。それらは次のようにする必要がありますか、それとも他のオプションですか?

2) サブセットを処理するにはどうすればよいですか? 世界とヨーロッパの国のセットをどのように扱うことができますか? 私の要件は、関数が単一の名前と文字列の配列を取得することです。

3) Countryname、World、Name、Students の 4 つの要素の型は何ですか?

Coqでこのような問題を解決するのに役立つ資料への参照を取得したいと思います.

ありがとう、

ウィラヤット

以下の補題を証明したい。戦術「破壊」を使用しようとしていますが、それを証明できません。そのような補題をどのように証明できるか教えてください。EmptyString については証明できますが、変数 s1 と s2 については証明できません。ありがとう

Prop についての代入定理を証明しようとしていますが、惨めに失敗しています。次の定理は coq で証明できますか? そうでない場合は、その理由を教えてください。

ポイントは、証明は論理的には帰納法によるものだということです。私が見る限り、プロップは帰納的に定義されていません。そのような定理は Coq でどのように証明されるでしょうか?

いくつかの文字列変数とリスト変数を含む補題を証明したいというシナリオがあります。おそらく、それは「誘導」を必要としますが、誰かが私が以下に与えられた見出語を証明するのを手伝ってくれるでしょうか。残りのコードが必要な場合は、それも提供できます。

要素の bst への挿入関数の正しさを証明しようとして、一見些細な補題を証明しようとして立ち往生しました。これまでの私の試み：

ツリー内のすべてが よりも小さくn、n <= mすべてが よりも小さい場合は明らかですmが、coq に私を信じさせることはできないようです。どうすれば続行できますか?