Isabelle で次のデータ型を定義しました
datatype bc_t = B | C
次の基本補題を証明する方法がわかりません
lemma "∀ x::bc_t . (x=B ⟶ x≠C)"
仮定B≠Cの下で、証明は次のようになります。
lemma "⟦B≠C; x=B⟧ ⟹ x≠C"
by metis
BとCが異なるという明示的な仮定なしに補題を証明する方法はありますか?
更新:[simp] Manuel Eberl が回答へのコメントで示唆したように、単純化プロセスをループさせ、自動生成された単純化ルールを無視する誤った単純化規則 (属性を持つレンマ、ここでは省略) がB≠C問題の原因でしたC≠B(bs_t.simpsクリスが答えで指摘したように）。gc44 による回答のようsimpに、通常の状況で補題を証明するのに十分です。
自動ツールで大きな有利なスタートを切ることができます。自動ツールからフィードバックを得る複数の方法を説明するには、定理を証明するよりもはるかに多くの作業が必要です。
datatype bc_t = B | C
lemma "∀ x::bc_t . (x = B ⟶ x ~= C)"
try0
using[[simp_trace]]
using [[simp_trace_depth_limit=100]]
apply(simp)
done
lemma "∀ x::bc_t . (x = B ⟶ x ~= C)"
sledgehammer
by (metis bc_t.distinct(1))
「プラグインオプション/イザベル/全般」でtry0チェックを外していたので使用しました。Auto Methodsオプションで、Sledgehammer 以外のすべての自動ツール ボックスにチェックを入れていることが何度もあります。
そこで示したように使用sledgehammerすることも、PIDE の Sledgehammer パネルで使用することもできます。ではsimp_trace、カーソルを の行に置くと、置換規則に基づいてメソッドがそれをapply(simp)どのように証明したかを知ることができます。simp
更新 140108_1305
自動ツールは作業を高速化するのに役立ちますが、証明の基本的なロジックを理解することも重要です。これはsimp_trace、メソッドの他の属性simpが役立つ場所です。を読んtutorial.pdfで、prog-prove.pdfのisar-ref.pdf使用に関する詳細とレッスンを確認してくださいsimp。
simpメソッドを制御するための 3 つの属性は、、、addおよびdelですonly。
あなたの例ではsimp_trace、 とともにを使用して、only使用されているルールを明示し、ロジックを理解できるようにしたいと考えています。
metisSledgehammer による証明は、simpいくつかのルールしか使用していない可能性があることを示しています。simpトレースを見てsimp、コントロール パネルからカット アンド ペーストできるルールのみを使用します。私は 4 つの名前付きルールを数えましたが、これは実際に行う価値のあるものであるとは言えませんが、それを見つける必要がありました。
[更新140101_0745: 状況を分析しすぎないようにしていましたが、使用するdelという私の壮大な計画onlyがうまくいかなかったため、使用することになりました。以下simp onlyの代わりに を使用すると、メソッドはエラーで失敗します。これは、この 4 つのルールだけではゴールを単純化できないことを意味します。これは、代わりにの場合には当てはまりません。このメソッドはその方法に制限されておらず、呼び出しなど、説明していない多くのことを実行できます。]simp delapplyauto simp onlysimp onlyautosimpblast
lemma "∀ x::bc_t . (x = B ⟶ x ~= C)"
using[[simp_trace]]
using [[simp_trace_depth_limit=100]]
apply(simp del:
bc_t.distinct(1)
simp_thms(8)
simp_thms(17)
simp_thms(35)
)
oops
さて、最新のsimpトレースを見ると、さらに多くのsimpルールがあります。簡略化には、鳥を殺すための石が 1 つ以上あるので、あきらめます。
覚えておくべきことの 1 つは、およびのようなsimpメソッドで使用できることです。特に、ルールが定理を証明するのに十分でない場合、トレースに表示されない の使用に頼る可能性があります。これは、 を使用するときに知っておくことが重要です。そのため、 によって検出される証明に必要なのはルールだけであるという印象を受けません。autofastforceapply(auto simp add: stufferThm)autosimpblastsimponlysimpauto
ここで、以下のコメントについていくつかコメントします。
simpEberl が言及しているように、非常に長い間紫色のままである場合は、膨大な数の単純化を行う必要があるか、終了しないループに陥っています。どちらかが悪い。simp私は、40 秒の証明は良い証明とは考えていません。
基本的に、特に独自のルールを定義している場合はsimp、ループや を呼び出す他のメソッドに入るのは非常に簡単です。この方法は、うまくいくと簡単です。そうでない場合は、ロジックのために作業する必要がある場合があります。simpsimpsimp
を使用try0し、証明が見つからない場合はforce、fastforce、auto、 などの実験用の自動証明方法のリストが表示されます。simpが でループしている場合はauto、 で試してみてくださいfastforce。実験は非常に重要です。
覚えておくべきもう 1 つの重要なことは、simpルールではない定義を展開することです。Sledgehammer は定義を見つけることができる場合もありますが、定義が展開されていないために最も単純な定理が証明できない場合もあります。
[更新140109_0750: 一般化には常にリスクが伴います。定義を展開すると、多くの場合、Sledgehammer が証明を見つけることができなくなります。Sledgehammer は、高レベルの定理を一致させることでうまく機能するため、絶望的に拡張された式は、何度も失敗する運命にあります。非常に拡張された式でさえ、他の自動メソッドが証明を見つけることができなくなる可能性があります。ただし、方程式に基づく計算的な性質のものについては、定義を拡張simpすると、巨大で複雑な式を完全に減らすことができます。いつそれらを保持し、いつ展開するかを知る必要があります。素晴らしいことは、多くのことをかなり速く簡単に試すことができることです。]
definition stuffTrue :: "bool" where
"stuffTrue = True"
theorem "stuffTrue"
apply(unfold stuffTrue_def)
by(simp)
些細な問題ではありません。単純なことは必ずしも簡単に証明できるとは限りません。些細なことは、自動ツールの使用方法を習得した後に必要となるタイピングです。
datatype一連の単純化規則を作成すると、自動的に ( という名前で<datatype-name>.simps) 導出され、単純化器に追加されます。あなたの例では、それは
datatype bc_t = B | C
thm bc_t.simps
B ≠ C
C ≠ B
(case B of B ⇒ ?f1.0 | C ⇒ ?f2.0) = ?f1.0
(case C of B ⇒ ?f1.0 | C ⇒ ?f2.0) = ?f2.0
bc_t_rec ?f1.0 ?f2.0 B = ?f1.0
bc_t_rec ?f1.0 ?f2.0 C = ?f2.
Bこれには、とCが異なるという事実が含まれます。(これらの事実のサブセットであり、識別性についてのみ述べているものは、名前を介して入手できますbc_t.distinct。)
これらの単純化規則が整っていれば、補題を解くことができますby simp。