証明検証系Mizarを試してみる

Mizarは証明検証系です。形式的な証明記述言語とその処理系という括りではCoqやIsabelleの仲間ですが、対話的ではないので使い勝手はだいぶ違います。とりあえずインストールして使ってみましょう。

内容：

インストール

Mizarのオフィシャルサイトは：

• http://mizar.org/

信州大学の日本語ページもあります。

• http://markun.cs.shinshu-u.ac.jp/kiso/projects/proofchecker/mizar/index-j.html

信州大学のアーカイブから、自分の環境に応じたバイナリをダウンロードします。

• ftp://markun.cs.shinshu-u.ac.jp/pub/mizar/system/current/ （バイナリの一覧）

Windowsの場合、現時点（2016年12月）ではmizar-8.1.04_5.33.1254-i386-win32.exeが最新のバイナリです。このファイルは単なる自己解凍形式のZIPファイルです。

例えば次のようにしてZIPファイルを展開します（シェルはbash）。

$ mkdir mizar-install-tmp

$ cd mizar-install-tmp

$ mv ../mizar-8.1.04_5.33.1254-i386-win32.exe .

$ ./mizar-8.1.04_5.33.1254-i386-win32.exe

  ナニヤラカニヤラ

$ ls -1
./
../
abstr.zip
install.bat*
license
mizar-8.1.04_5.33.1254-i386-win32.exe*
mizbib.zip
mizdb1.zip
mizdoc.zip
mizsys.zip
mizutil.zip
mizxml.zip
mmlfull.zip
prel.zip
readme.txt
unzip.exe*

$

ZIPを展開すると、さらにいくつかのZIPファイルと実行ファイルと文書ファイルが現れます。このなかのinstall.batを実行すればいいわけですが、えっらく古臭いインストール方法ですね。

CoqもIsabelleもインストーラーはモダンで作業は非常に簡単でした。Coqのインストールについて「WindowsへのCoqのインストール」に顛末を書いてますが、Coq本体ではなくてProof Generalに手間取ったからです。

それに比べると、インストールがバッチファイルって …… 念のためにMizarインストーラーであるinstall.batの中身を読んでみました； 引数に与えられたディレクトリパスに対してファイルを展開・コピーするだけです。デフォルトのディレクトリはc:\mizarです。

install.batのメッセージ文言を切り出してみると：

The Mizar system ver. 8.1.04 installation is now completed.

Make sure the line:  %1;
is in your path. For example, to run any of the PC Mizar programs
or utilities from anywhere on your system, your AUTOEXEC.BAT file
could contain a path like the following:
   PATH %1;
and
   SET MIZFILES=%1

AUTOEXEC.BATって、いつの時代の話だよ？ 2016年の時点で、このスクリプトを使い続けている点で少し不安になったりします。

こういう古いスタイルのインストール・バッチファイル（と、システム本体）だと、パスに空白や'/'が混じっていたり名前の大文字小文字でトラブったりするので注意したほうがいいでしょう。このバッチファイルによるコピーにはかなり時間がかかります。

先のメッセージ文言にもあったとおり、環境変数を自分で設定しなくてはいけません。Mizarをインストールしたディレクトリを環境変数PATHに加えて、同じディレクトリを環境変数MIZFILESにセットします。

使ってみる

信州大学がMizarプロジェクトに参加しているので、日本語の資料があります。Mizarの概要を知るには、

• http://markun.cs.shinshu-u.ac.jp/kiso/projects/proofchecker/mizar/Mizar4/ja_wframe/index.html

日本語PDFマニュアル『Mizar 講義録』は、

• http://markun.cs.shinshu-u.ac.jp/kiso/projects/proofchecker/mizar/Mizar4/printout/mizar4ja_prn.pdf （132ページ、Version 6.1.12対応なので少し古い）

Mizarを使うには、ワーキングディレクトリにサブディレクトリ構造が必要ということなので、次のようなサブディレクトリを作ります。

$ mkdir mizar-test

$ cd mizar-test/

$ mkdir text dict prel

$ ls
./  ../  dict/  prel/  text/

$

Mizarの記述単位をアーティクルと呼び、ファイル拡張子は.mizです。今作ったtextサブディレクトリに.mizファイルを置くようです。Mizarアーティクル（.miz）を書いたら、mizfというコマンド（Windowsでの実体はバッチファイル）で処理します。

スライド http://mizar.org/cicm_tutorial/mizar.pdf の45ページにあった次のコードを試してみます。

reserve i,j,k,l,m,n for natural number;
i+k = j+k implies i=j;
proof
  defpred P[natural number] means
    i+$1 = j+$1 implies i=j;
  A1: P[0]
  proof
    assume B0: i+0 = j+0;
    B1: i+0 = i by INDUCT:3;
    B2: j+0 = j by INDUCT:3;
    hence thesis by B0,B1,B2;
  end;
  A2: for k st P[k] holds P[succ k]
  proof
    let l such that C1: P[l];
    assume C2: i+succ l=j+succ l;
    then C3: succ(i+l) = j+succ l by C2,INDUCT:4
    .= succ(j+l) by INDUCT:4;
    hence thesis by C1,INDUCT:2;
  end;
  for k holds P[k] from INDUCT:sch 1(A1,A2);
  hence thesis;
end;

mizfコマンドはバッチファイルですから、PowerShellかcmd.exeからの実行が無難です（僕は、「Windowsのcmd.exeとbashのどちらでも実行できるバッチファイルの書き方」の方法でbashからも実行してますが。）

 mizar-test > mizf .\text\test.miz
Make Environment, Mizar Ver. 8.1.04 (Win32/FPC)
Copyright (c) 1990-2015 Association of Mizar Users

**** 2 errors detected

 mizar-test >

エラーメッセージは、text/test.mizファイル内にコメントとして埋め込まれます。以下の「::>」の行です。ウーンン、タグジャンプが使えないので辛い*1。

reserve i,j,k,l,m,n for natural number;
::>   *212,213
i+k = j+k implies i=j;
proof
  defpred P[natural number] means
    i+$1 = j+$1 implies i=j;
  A1: P[0]
  proof
    assume B0: i+0 = j+0;
    B1: i+0 = i by INDUCT:3;
    B2: j+0 = j by INDUCT:3;
    hence thesis by B0,B1,B2;
  end;
  A2: for k st P[k] holds P[succ k]
  proof
    let l such that C1: P[l];
    assume C2: i+succ l=j+succ l;
    then C3: succ(i+l) = j+succ l by C2,INDUCT:4
    .= succ(j+l) by INDUCT:4;
    hence thesis by C1,INDUCT:2;
  end;
  for k holds P[k] from INDUCT:sch 1(A1,A2);
  hence thesis;
end;
::>
::> 212: "environ" expected
::> 213: "begin" missing

environとbeginが必要だ、ってことらしい。先頭にenvironとbeginと書いた2行を挿入。

 mizar-test > mizf .\text\test.miz
Make Environment, Mizar Ver. 8.1.04 (Win32/FPC)
Copyright (c) 1990-2015 Association of Mizar Users

-Vocabularies  [   1]
-Constructors  [   1]
-Requirements  [   1]
-Registrations [   1]
-Notations     [   1]

Verifier based on More Strict Mizar Processor, Mizar Ver. 8.1.04 (Win32/FPC)
Copyright (c) 1990-2015 Association of Mizar Users
Processing: .\text\test.miz

Parser   [  29 *12]   0:00
MSM      [  25 *16]   0:00
Analyzer [  26 *16]   0:00
Checker  [  26 *16]   0:00
Time of mizaring: 0:00

 mizar-test >

うまくいったのか？ lsしてみると、やたらにイッパイファイルがあります。

 mizar-test > ls text | %{ $_.name}
test.aco
test.ano
test.atr
test.cho
test.dct
test.dcx
test.ecl
test.eno
test.ere
test.err
test.evl
test.fil
test.frm
test.frx
test.idx
test.log
test.miz
test.msx
test.nol
test.par
test.prf
test.ref
test.sgl
test.vcl
test.wsx
test.xml

 mizar-test >

元ファイル1個に付き2527個のファイルが生成されますが、すべて内部的に使用するものだとか。test.mizを見たら、エラーメッセージは残っています。

::>
::> 140: Unknown variable
::> 203: Unknown token, maybe an illegal character used in an identifier
::> 306: Attribute symbol expected
::> 330: Unexpected end of an item (perhaps ";" missing)
::> 371: "]" expected
::> 396: Formula expected

その後しばらくいじったみたのですが、どうもうまくいきません*2。色々な文書を見ても概念や構文の説明ばっかりで動く例がないのですよ。疑似コードやスニペットだけで、驚くほど実サンプルがない！

チュートリアル https://www.cs.ru.nl/~freek/mizar/mizman.pdf （54ページの文書）によると、Mizarのenviron部をキチンと書くのは難しいようです。

The most difficult part of writing Mizar is finding what you need in the MML which is the name of the Mizar Mathematical Library.

---

Mizarを書くときに一番難しいところは、MML(Mizar Mathematical Library)のなかから、必要な（インポートすべき）アーティクルを特定することだ。

It is hard to get the environment of a Mizar article correct.

---

Mizarアーティクルのenviron部を正しく書くのは難しいぞー。

MML（Mizar Mathematical Library）は膨大なファイル群からなるライブラリです。その内容や相互関係を把握して、適切にインポートするのは確かにシンドそうです。「難しいぞ」「頑張れよ」って書いてあるだけで、ノウハウもツールも示してません(泣)*3。

感想

Mizarは1973年から開発が続いています。80年代からはじまったCoq, Isabelleよりさらに古い言語／システムです。歴史が長いシステムであっても、最近の傾向を取り込んでいたり斬新なもの（Isabelle/jEditとか）もありますが、Mizarは20世紀で時間が止まってしまったような印象を受けます。

「動くサンプルコードがない」といいましたが、MMLライブラリという膨大なサンプルがあるとも言えます。MMLの資産はさすがに凄いなと思います。が、MMLをブラウズしたり検索するツールは見当たりません。ツールや手法に関する論文はあるけど動くツールがなかったりします（例：MML Query）。インターネット上に公開されたオンラインツールもたいていはリンク切れ。本家サイトさえも貧弱で安定してないようです。なにから何まで今風じゃなくて、MS-DOSの時代にタイムスリップしたみたい。

でも、証明記述の可読性が高いのは本当で、構文の設計は優れたものだと思います。CoqやIsabelleとは比べものにならないくらい読みやすいです。それだけに、ソフトウェアシステムとしての時代遅れ感が残念です。

• 続報：証明検証系Mizarのジレンマと証明系の村
• 第三報：Mizar、嫌いじゃないんだけどな

*1:[追記]EmacsのMizarモードを使うと、タグジャンプ形式に変換してくれます。[/追記]

*2:[追記]修正した結果は「Mizar証明の抜群な分かりやすさ」[/追記]

*3:[追記]ノウハウもツールもないのが実情のようです。[/追記]