問題タブ [theorem-proving]

という名前の Isabelle 理論ファイルがありますJohn.thy。友人に見せたいのですが、友人は Isabelle を持っておらず、生の.thyファイルを読むのは簡単ではありません。Isabelle ライブラリ (このようなもの: http://isabelle.in.tum.de/library/HOL/Finite_Set.html ) で、かなり構文が強調表示されている Web ページをいくつか見たことがあります。そのように。

では、どうやって作ることができJohn.htmlますか？私はドキュメンテーションを見てきましたが、すべてのビルドファイルやメイクファイルなど、かなり恐ろしく難しいように見えます。これを行う最も簡単な方法を親切な魂が説明できますか?

というレコード タイプを作成しgraph、適切な「のサブグラフである」関係を定義しました。ordグラフのセットとサブグラフの関係が一緒になって順序を形成すること、つまりクラスのインスタンスであることを示したいと思います。しかし、私はそれを機能させることができません。これが私の最小限の作業例です：

エラーが発生します：

Type unification failed: No type arity graph_ext :: ord"

instantiation graph :: ordや などを入力してみinstantiation graph_ext :: ordましたが、何もうまくいかないようです。何か案は？

イザベル理論 (HOL セッションなど) の HTML ドキュメントを生成したいのですが、証明は含めません。

つまり、 http://isabelle.in.tum.de/library/HOL/Nat.htmlのようなページを作成したい のですが、たとえば、

私だけが見たい

その理由は、利用可能な定理を調べるために HTML ページを使用しているからですが、その場合、証明は気を散らすだけです。(PDF を生成するときにプルーフを省略できることは知っていますが、特に HTML ドキュメントに興味があります。)

ときどき<statement> solve_direct(通常は を介し​​て呼び出し<statement> tryます) は多数のライブラリ定理をリストし、「現在の目標は次の方法で直接解決できます: …」と述べています。

<theorem>を の検索結果の 1 つとすると、solve_directほとんどの場合、 を証明でき<statement> by (rule theorem)ます。

ただし、そのような証明が受け入れられない場合があり、その結果、「最初の証明方法を適用できませんでした」というエラー メッセージが表示されます。

によって見つかった定理を再利用するための一般的な別の手法はありsolve_directますか?

それとも個々の状況によるのでしょうか？最小限の例を作成して、この質問に添付することができます。

n各単項式の指数が より小さいか等しい場合、単項式の和の次数は常に より小さいか等しいことを示す補題に取り組んでいnます。

これまでのところ、次のことを行う必要があります (Isabelle の初心者であることに注意してください)。

ここに問題があります。次の補題が証明を完了するのに十分でない理由がわかりません。特に、最後の部分 (申し訳ありませんが) は、大槌が証明を見つけるのに十分なほど単純であると思います。

.
Brian Huffman の優れた回答からの解決策:
.

Coq が何であるかを把握しようとして、本質的にそれを証明する必要がある状況に陥りましたa=b -> nat_compare a b = Eq。

次のようにして簡単に始めることができます。

それは私に与える：

最初は些細なことです：

しかし、次の目標は私を困惑させます。

できます

与える：

(この正確なポイントに によって到達することもできますsimpl。これはより理にかなっているようです。)

さて、ペンと紙を使って、これが帰納法による私の証明であると主張したいと思います..

私はこれに正しい方法でアプローチしていますか？これを適切に行う方法をどこで学ぶことができますか?

私はすでに楽しみbubble_mainが注文されていることを証明しようとしましたが、どのアプローチも機能していないようです. ここで誰かが補題を証明するのを手伝ってくれませんかis_ordered (bubble_main L)。

イザベルが証明を見つけるのに役立つものはないように見えるので、以前の補題をすべて削除しました。ここに私のコード/理論があります:

理由はわかりませんが、Coq でプログラム仕様を証明しようとすると、OR 仮説を​​排除しようとするとエラーが発生します。

これは私が証明したい定理です:

これは、エラーが発生したときの目標とコンテキストです。

この定理の前に、次の定義とインポートがあります。

この戦術を使用しようとすると、前のエラーが発生します。

何が原因なのかよくわかりません。