問題タブ [isar]

ほとんどの証明アシスタントは、従属型を持つ関数型プログラミング言語です。プログラム/アルゴリズムを証明できます。代わりに、数学のみに最適な証明アシスタント (たとえば微積分) に興味があります。1つお勧めできますか？Mizar について聞いたことがありますが、ソース コードが閉じられているのは好きではありませんが、数学に最適な場合は使用します。Agda や Idris などの新しい言語は、数学的な証明にどの程度適していますか?

ここに証明があります：

depth値は証明全体で 0 ですが、その後

に変わります

ここでとはdepthどういう意味ですか? 証明を行う際に重要なことはありますか?

私はまだ Isabelle のセマンティックの平等について推論しようとしています。2 つの数式を比較して、それらが等しいかどうかを確認したい。これには商型が必要だと以前に言われました。だから私は自分自身をquotiernttypeに定義しようとしましたが、私の定義の後にコードを書くことができないように見えるので、どうやら私の定義は完全ではありません。これまでの私のコードは次のとおりです。

私はいくつかの基本的な式とその複雑なバージョンを持っており、複雑なタイプについて推論したいので、等式関係の 3 つの公理と 3 つの追加の簡単な公理で等号を定義しました。

編集:どうやら私は引用符を追加するのを忘れたばかです-.-ここから先の考えを続ける方法がまだわかりません。

私は持っている

証拠の後、私は得る

私はスレッジハンマーからメティスの電話を受けました。

構造的な_偶数.イントロ(1) =構造的な_偶数0

私は得る

それから。しかし、次の後に私は得る

したがって、システムが「エクスポートされたルールによってゴールを解決する試みに成功しました」と言ったにもかかわらず、1. に些細な残りのサブゴールがあります。

なぜこれが起こるのか、どうすれば修正できますか?

イザベルのように目標があるときは、"∀x. P x"書くことができることを知っています

しかし、目標がである場合"∀x>0. P x"、私にはそれができません。proof目標を単純化するために後で使用できる同様のルール/方法はありますか? という形の目標を持っているシチュエーションにも興味があります"∃x>0. P x"。

proof (rule something)スタイルを使用する Isar プルーフを探しています。