問題タブ [theorem-proving]

イザベルの「商型パターン」とは？

インターネット上で説明を見つけることができませんでした。

OCaml で Coq タクティックを開発しようとしています。ここで用語を作成constrし、この用語を使用してゴール内の存在変数をインスタンス化したいと考えています。Evar_tactic.instantiate私は戦術を発動しようとしています。しかし、 type の引数が必要です Tacinterp.interp_sign * Glob_term.glob_constr。とにかくconstrこのタイプに変換する方法はありますか? または、OCaml レベルから evar をインスタンス化できる他の方法はありますか?

次に、Coq にはsetand と呼ばれるタクティックがあります。poseそれらが定義されている場所が見つかりませんでした。それらを OCaml から使いたい場合、どうすればよいですか?

私は Coq を使った定理証明の初心者であり、この目標に行き詰まっています。

誰でも簡単にできますか？

Z3 で「for all」を正しく使用する方法を誰かが教えてくれませんか。ドキュメントを調べましたが、情報が見つかりませんでした。私がやろうとしていることは

「foo」内で、Z3で次のことを言う必要があります

"let (u,r) be runnable(t) in { (assert ((u,r) is in users) (assert (r,t) is in roles)) }"

私が知らないのは、ランナブルの最初の要素を取得してユーザーにあることをアサートし、2 番目の要素をロールにあることをアサートする方法です。

(declare-sort Task) (declare-sort Role) (declare-sort User) (declare-fun runnable (Task) (User Role)) (declare-fun perm (Role Task) Bool) (declare-fun users (User Role) ) ブール)

(assert (forall (t タスク)) (foo))

(check-sat) (get-model)

4 つの並べ替え (タスク、ロール、ユーザー、および実行) を作成しました。最後のものは 2 つのパラメーターを受け取ります。次に、Run の 1 つを含め、それぞれの楽しみを宣言し、2 つのパラメーターを受け取る P を呼び出して、Run の「インスタンス」を作成します。 . 次に、ユーザーと役割の「関係」(Privs) を含む 2 つの配列と、役割とタスクの「関係」(役割) を含むもう 1 つの配列を作成しました。この 2 つの配列を使用して、ユーザー u を検索するときに Privs で役割 r を持っているかどうか、および Roles で役割 r を検索するときにタスク t を持っているかどうかをアサートします。これまでは、次のように別々の行でこれを行うことができました。

しかし今、私は Run (ユーザー、ロールのペア) を受け取り、関数内で同じことをアサートする楽しみを作ろうとしていますが、P のすべてのユーザーとそのすべてのロールに対してです。これは、実行ソート変数を関数に渡すことによって実行できますか??..内部の要素(ユーザー、ロール)にアクセスするために??

私は Prover9/Mace4 を通していくつかの格子証明を実行しています。私は格子結合操作の非標準の公理化を使用していますが、結合が交換可能、結合的、冪等であることはすぐにはわかりません。(私は Prover9 にそれが正しいことを証明してもらうことができます -- 最終的に。)

Prover9 がこれらのプロパティを探して、検索を高速化することを知っています。これらのプロパティを追加入力セクションに入れてみました (GUI バージョン 0.5 を実行しています)。

Q1: ヒントを見てもらう方法はこれですか？

Q2: 証明/ヒントとコツを高速化するためのヘルプを探すのに適した場所はありますか? (これを機能させることができれば、ヒントを提供したい演算子が他にもあります。)

参考までに、私の公理は次のとおりです（プリミティブ操作が1つだけの双格子）：

（DougSの回答が投稿された後に編集してください。）

わお！ありがとうございました。桁違いのスピードアップ。

もしよろしければ、いくつかの後続のqがあります...

Q3: 生成されたヒントには、最初の公理と目標がすべて含まれているように見えます。（おそらく、すべてのヒントを必要としないというあなたのコメントです。公理を削除すると証明が速くなることを確かに経験しました。）

Q4: (結果として) 公理によって正当化されないヒントを追加するとどうなりますか? それらは無視されますか？

Q5: 公理に反するヒントを追加するとどうなりますか? (いくつかの試行から、これにより Prover9 が誤って推論することはありません。)

Q6: 証明 (試行) がタイムアウトした場合、これまでに推論された数式を取得し、次の試行を高速化するためのヒントとして再利用する方法はありますか? (Q3 と Q4 に関して私が見たものにもかかわらず、これはある種の誤謬を引きずり込むだろうと私は感じています。)

Isabelle/HOL でのプログラミングと証明には、「データ型 exp」として表される単純な算術式で「algebra_simps」を使用することを提案する演習 2.4 があります。algebra_simps を使用して、そのような式のいくつかの単純なプロパティを証明する方法を誰かが例を挙げてもらえますか? たとえば、「Mult ab = Mult b a」?

一般に、同様の形式で表された単純な算術式の同等性を証明しようとしています (演算子のセットは限られています)。

回文の帰納的な定義は次のとおりです。

そして、 Software Foundationsから、私が証明したい定理:

証明の非公式な概要は次のとおりです。

が のような任意l0のリストであるとしl0 = rev l0ます。その場合、次の 3 つのケースのいずれかが成り立つ必要があります。l0もっている：

(a) ゼロ要素。この場合、定義により回文です。

(b) 1 つの要素。この場合、定義上は回文でもあります。

(c) 2つ以上のl0 = x :: l1 ++ [x]要素。xl1l1 = rev l1

からl1 = rev l1、次の 3 つのケースのいずれかが成立する必要があります...

l0再帰的なケース分析は、分析されたリストの長さが反復ごとに 2 ずつ減少するため、有限リストに対して終了します。任意の list で終了する場合、 回文の両端に 2 つの同一の要素を追加して作成されたリストも回文であるため、lnまでの外側のリストもすべて回文です。l0

その理由付けは正しいと思いますが、それを形式化する方法がわかりません。Coqで証明に変えられますか? 使用された戦術がどのように機能するかについてのいくつかの説明は、特に役立ちます。

構文と Haskell との違いに慣れるために、Idris で基本的なモナド パーサーを作成しています。私はそれがうまく機能する基本を持っていますが、パーサー用の VerifiedSemigroup と VerifiedMonoid インスタンスを作成しようとして立ち往生しています。

これ以上苦労することなく、パーサー タイプ、Semigroup、および Monoid インスタンス、および VerifiedSemigroup インスタンスの開始を次に示します。

私は基本的に の後intros、次の証明者の状態で立ち往生しています:

rewriteどうにか一緒に使えそうな気がするappendAssociativeのですが、 lambda の「中に入る」方法がわかりません\s。

とにかく、私は演習の定理証明の部分で立ち往生しています - イドリス中心の定理証明のドキュメントをあまり見つけられないようです。おそらく、Agda のチュートリアルを見始める必要があると思います (ただし、Idris は、私が学びたいと確信している依存型型言語です!)。