cocolog:83987064

定理証明システム Isabelle/HOL の Tutorial、Isabelle2015/doc/tutorial.pdf を読んだ。いつもの読書と違って英語。 (JRF 1656)

JRF 2015年11月26日 (木) Tweet

《Isabelle》
https://isabelle.in.tum.de/
http://www.cl.cam.ac.uk/research/hvg/Isabelle/

JRF2015/11/262663

私の場合、普通、英語の文章は日本語の文章に比べて読むのに三倍以上の時間がかかるものだが、「昔取った杵柄[きねづか]」というやつか、大昔(15年以上前)にやってた分野だからか、割とスラスラ読めた。

Tutorial (入門)を進めていく途中の環境設定についてはエントリを別にして、一つ前に「ひとこと」している([cocolog:83987061])。

JRF2015/11/265584

……。

入門の感想(?)に入る前に、私の Isabelle の経験について。

私は上で書いたように 15年以上前の時代に Isabelle を使っていた。当然 Isar はなく、tactic と tactical のみで証明していた。証明は ZF 上で、ラムダ計算のα同値性(の無矛盾性)に関する証明をして、それを(指導教官の否定的見解をおしきって)修士論文(相当)にした。

JRF2015/11/265872

それがイヤな思い出になったのかはわからないが、それ以降は Isabelle を自宅環境にインストールしたりしたこともあったが、結局、いじらずじまいということが続いた。「今後の方針」(↓)にも以前から Isabelle を触ろうと書きはしていたがとりかかる気になれなかった。それを今回は、Isabelle を起動し Tutorial をやるところまで行った。「トラウマ」があったとすれば時間がそれを克服したのかな…といったところ。

JRF2015/11/266415

《JRF の私見：雑記: 今後の方針》
http://jrf.cocolog-nifty.com/column/cat21172478/index.html?mode=long

JRF2015/11/261596

とりあえずの目標は、上で述べた修論のα同値性に関する証明を今の Isabelle 上でやること。が、そこまで気力が続くかはわからない。

JRF2015/11/266765

……。

2015-11-21 には、Tutorial からやろうということで、2015-11-20 に一端 Logics_ZF にしたのを HOL に Theory を選択しなおして起動。ToyList.thy を作って、とりあえず end を入力するところまで行く。その後、"The Value of a Boolean Expression" の例をするかどうか迷う。その例はあとまわしにして、とりあえず２章を読み進んだ。

JRF2015/11/262081

２章を読んだあと、迷っていた例を入力していくことにした。Exercise 2.5.2 で何をやっていいかわからなくなてつまづく。↓を見て解決。Exercise の文から normal の定義を変えないといけないのはわかったが、normif も CIF の部分は、normif (CIF b) t e = (if b then t else e) に変える必要があり、そうすると normal t & normal e --> normal(normif b t e) が証明できて、さらに normal(norm b) が定理として証明できるとのことだった。

JRF2015/11/266893

《Isabelle Tutorial その4 - caeruiro》
http://d.hatena.ne.jp/caeruiro/20100321/1269136916

JRF2015/11/264376

３章も読んだ。が、ここの練習問題は面倒臭く感じてやる気が起きず、やらなかった。私は ZF を使う予定なので、このあとにある Set Theory に関心がある。そこになったら、また練習問題をするかもしれないが、しばらくはやらなくていいかな…と思う。

JRF2015/11/263218

あと、ペラペラと最後までページをめくってみた(ディスプレイ上で、印刷はしてないので)。すると、チラと他のサイトを見たときに紹介されていた proof や have や qed が出てくる証明がこの Tutorial には(ほぼ)出て来ないことがわかった。tutorial.pdf にあるのは、apply ... done タイプの証明と言われる形式だけらしい。Isar を「読みやすく」書くのは別のところを読む必要がありそうだ。以前、↓から読んだ記事が参考になりそう。

JRF2015/11/262118

《Isabelle/Isar（その１） - ATPとCASのこと（謄）》
http://ehito.hatenablog.com/entry/20130503/1367582411

JRF2015/11/260700

……。

2015-11-22 に４章を読んだが、LaTeX が必要となるような「発見」ができるまでこれから先どれぐらいかかるのだろう。それまでここに書いてたことを覚えていられるかな…という印象。

５章も読んだが、gcd などの例を３章でやってなかったからか、いくつか失敗する証明やできない証明があり、そこは飛ばしつつ読んだ。昔とは全々違うが昔のおもかげもあるところもある。でも、これらも覚えてられないな…と思いつつ読んだ。読んでおいたから、やってれば、こういうのがあったと気付けるような気もするんだけど…。

JRF2015/11/269056

……。

2015-11-23 に Logics_ZF 上で、以前作った証明の一部である Infinite の理論を作ってみることにした。blast の力はすごく、以前証明した命題はすぐに証明できたが、欲が出て、Infinite(nat) を証明しようとしていろいろはまった。

JRF2015/11/260674

なかなかできなかったがそれがやっとできたので、次に Infinite(lfp(D,h)) という一般化を試してみたが、それをつかった Infinite(nat) の証明はとても難しそうで歯が立たなかった。Axiom of Choice が必要かどうかはわからないが、term のサイズを見る関数を定義してその最大のものを指定してそこに bnd_mono な h をかけるみたいなことをしないといけなさそうで、とりあえず諦めた。

JRF2015/11/263067

(おそらく "F: Fin(X) ==> F ~= 0 --> EX x: F. length(x) = Union({length(y). y: F})" みたいなのが言えればいい。それは帰納法だけで言えるはずで length 関数があれば、選択公理はいらないはず。)

JRF2015/11/266875

(ちなみに、Infinite(X) ならば、任意の F: Fin(X) に対して EX x: X. x ~: F が、選択公理なしに言える。背理法さえ使えれば、有限とか無限に関係なく、もっと強い "[| A ~= B; B <= A |] ==> EX x: A. x ~: B" も言える。ほんと、「選択公理」って思った以上に使わなくてもいけるんだよね。)

JRF2015/11/261268

ちなみに、apply ... done 形式しか使っていないが、Tutorial がそうなってるんだから、別に気にしなくていいのかな？

JRF2015/11/269147

……。

2015-11-23 に Tutorial の６章を読んだ。私は昔ずっと ZF でやってたので、HOL の well-foundedness の話とか知らず、とても興味深く読んだ。また↓にお世話になったが、言われている通り動かしているだけで、意味はよくわかっていない。

《Isabelle Tutorial その18 - caeruiro》
http://d.hatena.ne.jp/caeruiro/20100428/1272454217

JRF2015/11/266489

しかし、よく Exercise が解けるなぁ。すごい。同じ apply ... done 形式の証明でも、私が Logics_ZF で証明してるのはすべてこんなにエレガントなものじゃない。レベルの違いというか「超えられない壁」を感じる。私はダメだなぁ…。

JRF2015/11/260131

……。

2015-11-24 には７章を読んだ。例によって Exercise は自分で解かず、↓を参照するだけ。7.3節は読んでいてわけがわからなかった。7.4節の長大な証明で途中 apply(rule S_A_B.intros) が失敗したが↓をよくみると apply (rename_tac v) が tutorial.pdf には抜けていた。

JRF2015/11/262197

《Isabelle Tutorial その20 - caeruiro》
http://d.hatena.ne.jp/caeruiro/20100506/1273155367

《Isabelle Tutorial その21 - caeruiro》
http://d.hatena.ne.jp/caeruiro/20100507/1273242196

JRF2015/11/267304

……。

2015-11-25 に８章を読んだ。例によって↓を参照。この章は、はじめはわかりやすい。証明しようとするとややこしいんだろうけど、概念はやさしい。

《Isabelle Tutorial その22 - caeruiro》
http://d.hatena.ne.jp/caeruiro/20100512/1273669794

JRF2015/11/262685

「オブジェクト指向」っぽいことというのは Isabelle/HOL 内だとこう構築していくんだね。Perl (↓)の手作り感あふれるオブジェクト指向をちょっと思い出す。

《Perl でオブジェクト指向 C++風》
http://jrf.cocolog-nifty.com/software/2010/12/post.html

JRF2015/11/265901

8.4 節では 0 (ゼロ) なのか O (オー)なのか、または l(エル) なのか I (アイ) なのか 1 (ワン) なのかで迷う。エラーやコンテクストを見ながら見わけた。証明が↓の apply ... done から tutorial.pdf では proof ... have ... qed を使うタイプの証明(structured Isar proofs というらしい)になっていた。将来的には他の部分も proof ... qed を使った証明になっていくんだろうか。だとすると、ますます私はやりにくくなるな…。

JRF2015/11/262544

《Isabelle Tutorial その23 - caeruiro》
http://d.hatena.ne.jp/caeruiro/20100516/1274018433

proof ... qed タイプは文法をまだまったく学んでないのでそんなところに "." を打つか…というのを気付くまで悩んだりした。

JRF2015/11/267519

９章も読んだ。↓を見て Exercise の解を入力した。なお、変数名の衝突があったので ToyList.thy の他にファイルを二つ作ったのだが、9.2節の例をやるために前のファイルの途中に戻ったりした。

《Isabelle Tutorial その26 - caeruiro》
http://d.hatena.ne.jp/caeruiro/20100606/1275810766

JRF2015/11/260174

……。

2015-11-26 に１０章を読んだ。まず、{|X, Y|} が MPair X Y のことだというのだが、それが infix とかを利用せずに定義されていて、どうすればいいのかよくわからず、tutorial.pdf や↓には {|X,Y|} と記述されているのをいちいち MPair X Y と書けばいいんだな…と思って入力した…。が、まず最初の lemma が解けない。induct でいいと書いてるが、そこからわからない。↓にも証明が書いてない…ということで例をやるのはあきらめて、ただ読んでいくだけになった。

JRF2015/11/262286

《Isabelle Tutorial その27 - caeruiro》
http://d.hatena.ne.jp/caeruiro/20100620/1277038979

JRF2015/11/264247

……。

私は ZF か ZFC かの世界につまずいてしまって、ガンコにそこから進もうとしなかった…という面があった。この Tutorial でそれを超えた世界を見せられ、その世界の豊かさに驚いた。私は何にこだわってたんだろう…という感じ。

ときおり気になって、Isabelle2015/src/HOL 以下にあるソースを見ると、structured Isar proof の世界で、その記述は読める気はするけど全々書ける気がしない私は、これからどうしたらいいんだろうと、とまどうばかりだった。

JRF2015/11/267125

この先、Isabelle で何かするかどうかはわからない。tutorial.pdf が終って、なんだか気落ちしてしまったというのが正直な感想…。

JRF2015/11/266040