IsabelleについてのQ&A

• => : HOLのfunction type constructor

• ==> : Pure logicのimplication

• --> : HOLのimplication

(この辺の話は後半のところでもやる予定なんですが)Isabelleはライブラリのとは別に組み込みのロジックあって、これがPure logicと呼ばれています。 そもそもIsabelleは本来Pure logic上で証明を行うproof assistantなんですが、このPure logicの上に別のlogicを構成することが出来て、それがHOLやZFCです。

なのでHOLの証明は内部的には全てPure logicの証明図に置き換えてcheckされます。 AgdaやCoqなどの言語ではこういうことはしない(組み込みのものをそのまま使う)ので慣れないと不思議に感じるかもしれません。

ないよ(無慈悲)

• isar-ref.pdfのAppendixにquick referenceあるので眺めるとよいかも？

これは慣れもありますが、 (1) goalを優しくする (2) 証明の選び方 の2点がポイントです。

まずsledgehammerは優秀とはいえそれでも人間の「自明」とはかなり感覚が違います。 そもそも人間が自明だと思っていてもformalizeにはたくさん補題が必要だったりするので、出来る限りsledgehammerに与える命題は分かりやすく、すぐ示せそうなものだけにしたほうがいいです。

あと、余分な仮定が多いと探索が失敗しやすいです。goalが複雑なときは示したい命題を補題として切り出したりしたほうがいいこともあります。

それと、どうしても上手くいかないときは命題を見直しましょう。「簡単なはずなのにsledgehammerが答えを返さないぞ？」ってときはそもそも間違っている(goalが成り立たない)ことがあります。

次に、探索に成功し証明が複数出た場合、可能ならば簡単で応答の早い証明を選んだほうがいいです。 気をつけるべきはmetisで、これは現実的な時間では終わらない場合があるので避けられるならmetisを含まないものにするか、またはmetisに与えられた補題で先に使えるものは使ってしまいましょう。

例えば、

  by (metis lemmaA lemmaB lemmaC)

の時に、lemmaAが先に適用されてそれ以後使わないことがはっきりしているなら

  apply (rule lemmaA)
  by (metis lemmaB lemmC)

としたほうが応答が早くなります。あるいはapplyの後にもう一度sledehammerをかけてもいいでしょう。

ある程度はね。

• simp: 式変形のみ

• auto: 便利コマンドに見えるけれどこいつは(今注目していないものも含めて)全てのgoalに対して変形を行うので注意が必要, 代わりに失敗しても(完全にゴールが解消できなくても)ある程度変形した形を保ってくれるのでsimp_allの代わりに使える場合もある

• fastforce: autoみたいに使えて現在のgoalに対する変形しかしないので便利 代わりに証明完了or失敗(何もしない)で挙動が極端

• blast: 体感では汎用的な証明力が強い。代わりにauto/fastforceと違ってsimp add:できないので打つのがめんどくさい

• その他: 自動証明コマンドはいろいろあるけど、これ以外はsledgehammerが返した時に大人しく従うくらいで自分から使う必要は多分ない

lemmaやtheoremのassumesに現れる仮定や、Isarで名前を付けられる命題は項をスペースで区切って列挙が出来ます。 具体的に、 "A" "B" みたいに横に並べることが出来て、これには一度に名前を付けられるので、 x: "A" "B" とするとx(1)でAを、x(2)でBを参照できます。

jEditならQueryパネルにダブルクォートで囲って項を渡すとその項を含む定理を検索できます。ここにはパターンを渡すのでワイルドカードとしてアンダーバーも使えます。 name: hoge とかやると定理の名前にhogeを含むものという意味にもなります。

• 紫: コマンド評価中。これが数秒同じ所で止まっているならその証明は重いのでやめたほうがいいかもしれない。

• 赤下線: エラー

• 青下線: info的な情報を出してくれます。前の定理から即座に示せる場合はsolve_direct、反例が見つかる場合はquickcheckなどがたまに教えてくれます。

• オレンジ下線: 警告。パース関係の警告(この項は〜とも〜ともパースできるよみたいなやつ)は無視しないほうがいいです。

Isabelleはユニコード文字をタグみたいにして埋め込むのでソースコード自体は直接読むに耐えないのですが、 例えばgithubとかに公開するとかブラウザが使えるならドキュメントを用意しておくのがおすすめです。

詳しくはドキュメントを見てもらうといいんですが、プロジェクトのルートにROOTというファイルを置いて内容書いてコマンド走らせると公式のソースコード表示しているやつみたいな感じでHTMLが生成されます。 ちなみにpdfにも吐けます。