問題タブ [isabelle]

型のペアで作業していると仮定し、それにパターン マッチングを('a × 'a)使用して を定義します。fun

a_btypeの変数がある場合、それを適用スタイル証明の('a × 'a)ペア表現に置き換えるにはどうすればよいでしょうか。(a,b)たとえば、次の補題を示す最良の方法は何ですか? test a_b cに置き換えるにはどうすればよいtest (a,b) cですか?

これは仮定のペアにも当てはまりますか?

disj_union商型 ( ) にリフトしたいセットに部分的に定義された演算子 (以下) がありますnatq。道徳的には、これは問題ないと思います。なぜなら、演算子が定義されている代表を等価クラスで見つけることが常に可能だからです[*]。disj_unionただし、は部分的にしか定義されていないため、リフトされた定義が等価性を保持するという証明を完成させることはできません。以下の私の理論ファイルでは、演算子を定義するために見つけた 1 つの方法を提案していますが、多くのand関数disj_unionを備えているので気に入らず、操作が難しいと思います (右?)。absRep

イザベルで商を使ってこの種のものを定義する良い方法は何ですか?

[*] これは、バインドされた変数が衝突しないという条件でのみキャプチャ回避置換が定義される方法に少し似ています。アルファ等価クラスの別の代表者に名前を変更することで常に満たすことができる条件。

次の目標があります。

P 0この目標を、P 1、P 2、 、P 3の6 つのサブ目標に分割したいと思いP 4ますP 5。これは、 によって簡単に実行できapply autoます。しかし、これを行うために使用している関連するルールは何autoですか? 私の実際の目標は次のように見えるので、私は尋ねます：

apply autoその目標を同じように分解することはありません（それは私に与えます

代わりは）。

次のばかげた例を考えてみましょう

次に、補題を使用してとの両方をstrict_subset置き換えたいと思います。それは実行されますが、既存の名前が に変更され、補題を導入する目的が完全に無効になります。AABAAa

導出されたレンマを使用すると、strict_subset2すべてうまくいくので、私の推論は正しいと確信しています。

要点は、ほとんどの標準補題は形式のものであり、形式のものstrict_subsetではなくstrict_subset2、Isabelle の作成者は私がstrict_subset2最初に自分自身を作成することを意図していない可能性があるということです。したがって、私は何か間違ったことをしているに違いありません.

名前が変更された理由を知りたいAですか？タイプが正確である限り、メタユニバーサル定量化が問題にならなかった例も見たことがあると思うので、それはタイピングシステムと関係があると思います。

Aもう1つの質問は、どうにかして名前の変更を防ぐことができるかどうかです。

もちろん、私はまだ Isabelle に慣れていないので、両方の質問が本当に正しい答えと無関係になる可能性は十分にあります。

PS。ここでもイザベルから素敵なシンボルを手に入れることはできますか?

セットがあるとしますA ⊆ nat。Isabelle a function でモデル化したいと思いますf : A ⇒ Y。次のいずれかを使用できます。

1. 部分関数、つまり typenat ⇒ Y optionのいずれか、または
2. 合計関数、つまり にnat ⇒ Yない入力に対して指定されていない型の 1 つA。

どちらが「より良い」オプションなのだろうか。いくつかの要因があります。

• 「部分関数」アプローチは、部分関数の等価性を比較する方が簡単であるため、優れています。つまり、 がf別の関数 と等しいかどうかを確認したい場合はg : A ⇒ Y、 とだけ言いf = gます。f指定されていない合計関数とを比較するgには、 と言わざるを得ません∀x ∈ A. f x = g x。

• 「指定されていない合計関数」アプローチの方が優れています。これは、構築/分解option型を常に気にする必要がないためです。たとえば、fが指定されていない合計関数でありx ∈ A、 である場合は とだけ言えますが、 が部分関数であるf x場合は と言わなければなりません。別の例として、関数全体よりも部分関数で関数合成を行う方がトリッキーです。f(the ∘ f) x

この質問に関連する具体的な例として、単純なグラフを形式化する次の試みを検討してください。

グラフは、一連のノード、ノード間のエッジ関係、およびlabel各ノードの で構成されます。にあるノードのラベルだけを気にしVます。では、 をlabel含む部分関数node ⇒ 'a optionにする必要がありますか、それともdom label = Vの外で指定されていない合計関数にする必要がありVますか?

Isabelle では、中間タイプの項が証明の正確性にとって重要である証明の目標を達成できることがよくあります。たとえば、nat42 を に変換して'a wordから元に戻す次の補題を考えてみましょう。

ここで、このステートメントの真偽は のタイプに依存します。 でof_nat 42ある場合32 word、ステートメントは真であり、 である場合2 word、ステートメントは偽です。

残念ながら、Isabelle にこの中間タイプを表示してもらうことはできないようです。

私は次のことを試しました：

• declare [[show_types]]
• declare [[show_sorts]]
• local_setup {* Config.put show_all_types true *}

すべてが表示されます:

ピンチでは、次のことができます。

の生のダンプを取得しますtermが、もっと良い方法があることを望んでいました。

証明の目標で中間項の型を表示する良い方法はありますか?

コード生成の非常に単純な定義があるとします。特定のケースに対してのみ定義され、それ以外の場合は実行時例外をスローします。

blubb今、私は正しいことを示したいと思います。例外がスローされるケースは無視する必要があります (数学的な観点ではなく、私の観点から)。Xただし、任意の値がであると仮定するサブゴールになってしまいますundefined。次の補題はサブゴールとほぼ同等です。False例外がスローされる (つまり、undefined返される)ケースを無視したいので、表示したいと思います。

これは証明できません。

例外をスローしたり処理したりする可能性のある関数の正確性を示す最良の方法は何undefinedですか? これはこの質問に関連しています。

この質問は、Isabelle/HOL定理証明者によるコード生成に関するものです。

distinctリスト上の関数のコードをエクスポートするとき

次のコードを取得します

このコードには2次ランタイムがあります。より高速なバージョンはありますか？理論の最初に文字列をインポート"~~/src/HOL/Library/Code_Char"するようなものを考えており、リストの効率的なコード生成が設定されています。のより良い実装はdistinct、O（n log n）でリストをソートし、リストを1回繰り返すことです。しかし、私は人がもっとうまくいくことができると思いますか？

とにかく、利用可能なdistinct他の関数のより高速な実装はありMainますか？

apply-scriptで使用する場合apply (rule)、通常、適切なルールが選択されます。同じことがproof構造化された証明にも当てはまります。使用されたルールの名前はどこで学習/検索できますか？

Isabelle/HOL理論マニュアルからコード生成を読みました。しかし、私はまだ少し迷っています。どこにあるのlinorder？たとえば、赤黒木を使用して処理を高速化するにはどうすればよいですか？localeプログラムの改良の文脈でどのように使用されますか？..。

改良を始めるためのチュートリアルはありますか？そうでない場合は、短い、自己完結型の正しい例がありますか？

例を開発できますか？

A :: 'a set私たちが持っていて、知っていると仮定しましょうfinite A。たとえば、の効率的なコードを生成するにはどうすればよいですa ∈ Aか？

の知識をどのように表現しますかfinite A。a ∈ A数学的理論（ ）をコード生成および最適化から分離するにはどうすればよいですか？