問題タブ [theorem-proving]

Coq で弱く指定された型で関数を定義しようとしています。具体的には、一連の再帰コンストラクターによって帰納的に定義された型があり、これらのサブセットを使用して引数が構築された場合にのみ定義される関数を定義したいと考えています。

より具体的には、次の型定義があります。

これで、グラウンド ケースにのみ適用される関数ができました。(次の定義は明らかに機能しませんが、私の意図を示唆するものです。)

理想的には、引数 x が汎用型コンストラクターのサブセット (この場合は Example_cons0) を使用して構築されていることを伝えたいと思います。この事実を述べる述語を定義し、述語の証明を引数として渡すことで、これができると考えました。例えば：

そして (Robin Green の推奨に従って) 次のようにします。

残念ながら、これをどのように行うかはわかりません。これが、弱く指定された型で制限された関数を定義する正しい方法であるかどうかさえわかりません。

ガイダンス、ヒント、または提案をいただければ幸いです。- リー

アップデート：

jozefg による推奨に従って、関数の例を次のように定義できます。

詳細については、彼のコメントを参照してください。この関数は、次の構文を使用して評価できます。これは、証明項が Coq でどのように表現されるかを示しています。

「7 つの互いに素な正方形の 3 つのコレクションごとに、各コレクションから 1 つの正方形を選択して、3 つの代表が内部的に互いに素になるようにすることは可能ですか?」など、正方形に関連する幾何学のいくつかの定理を自動的に証明/反証しようとしています。

私はOpenGeoProverを使用しようとしましたが、正方形の次の説明を思いつきました:

これが私が立ち往生している場所です:「正方形Aと正方形Bが交差する」という単純なステートメントをどのように定義するのですか?

Z3 では、この問題にどのようにアプローチできますか?

これは、Satchmo の定理を証明するための私のコードです。それはいくつかの統合を行います。

それがどのように機能しているかを理解するために、?-spy([satchmo]) でそれを行うことができます。

1- 指定されたクエリが次のような事実である場合:

また

プログラムはそれが事実であることを証明します。

2- ホーン ビットのクエリが次の場合:

ホーン規則であるため、プログラムはそれを証明します。

3- 非ホーン ビットのクエリが次の場合:

それも証明されます。

これは完全に機能しています。しかし、私がそれを少し変えようとしたとき。統一の代わりに、次のことを証明できる別の種類のマッチングを行う必要があります。

私が持っている場合：

私は証明したい：

これを行うために、コードを少し修正しました。代わりに、次のようにします。

私は非常によく似たものを入れました：

そして、次のように一致を定義しました：

この動きによって何もしていないことはわかっていますが、必要なことを証明できるように、一致の定義を少し修正することを考えています。

ここのどこかで立ち往生しています。現在のコードを見てください。

ここで、サブセットをテストできます。

ここでの問題は、次のことを証明して目標を達成する方法がわからないことです。

から：

一致の定義を変更することでそれを行うことができますか? そうでない場合、それを行う他の方法はありますか？

Isabelle で次のことを証明しようとしています。

と のインスタンス化された値を取得するにはどうすればよいhですbか?

Coqで型クラスを使ってMaybeモナドを定義したい。 Monadを継承しFunctorます。

Some (f x') = fmap f (Some x')モナド則の一つであるを証明したい。compute、reflexivityおよびを使用しdestruct option_functorましたが、証明できませんでした。fmap私は適切に単純化することはできません。

Z3 で与えられた一般的なトポロジーの定理を証明しようとしています。

TPTP トポロジ

次のZ3-SMT-LIBコードを使用して、そこにあるコードを翻訳しています

対応する出力は

この例をここでオンラインで実行してください

最初satは正しいです。しかし、2 番目satは間違っていますunsat。つまり、Z3 は定理とその否定が同時に真であると言っているのです。

この場合どうなるか教えてください。どうもありがとう。ではごきげんよう。

私がそれを正しく理解していれば (主にapplyTactic関数の存在から)、Idris で定理証明用のカスタム タクティクスを作成することが可能です。その方法を学ぶために使用できる例は何 (またはどこ) ですか?