homebrew で MathComp を入れる

追記 2015/11/11

今だったら公式の opam リポジトリから入れたほうが簡単にマルチコアを使えて速いし安心だと思います。

opam repo add coq-released https://coq.inria.fr/opam/released    # opam に Coq 関連のライブラリを追加
opam install -j4 coq.8.4.6 coq:ssreflect.1.5.0 coq:math-comp.1.5.0 # 安定版を指定してのインストール

---

MathComp (mathematical components) は Coq の拡張である SSReflect を使った、数学系の問題に特化したライブラリです。

で、Mac でよく使われているパッケージマネージャである homebrew には coq も ssreflect も標準であるのに、なぜか mathcomp はありません。homebrew の ssreflect formula は ssreflect-1.4 以前からあり、ssreflect は 1.5 から ssreflect と mathcomp の2つに分かれたのであってもいいはずなのですが、なぜかありません。

なので formula を作りました。

amutake/homebrew-mathcomp · GitHub

% brew tap amutake/mathcomp
% brew update # 最新の ssreflect が必要なので
% brew install mathcomp

これで mathcomp が入ります。mathcomp は ssreflect に依存しているので、ssreflect も入るようになっています。mathcomp のインストールは1時間くらいは普通にかかるので、気長に待ちましょう。

ところで homebrew の formula って依存パッケージのバージョンは指定できないんでしょうか…この場合だと ssreflect-1.5 が必要なので…

coqtop -emacs のプロンプト

プロンプトについて

ProofGeneral や、coqtop-vim は裏で coqtop -emacs というコマンドを実行して、そこと通信しています。

coqtop -emacs を実行すると、標準エラー出力に <prompt>Coq < 1 || 0 < </prompt> というのが出てきます。ここを見ると現在の coqtop の状態がわかります。今回の記事はこれの説明です。(もしかしたら8.4系のみ)

プロンプトの文法と意味

プロンプトの構造は

<prompt>$current_theorem < $whole_state_number |$theorem_stack1|...|$theorem_stackn| $theorem_state_number < </prompt>

となっています。それぞれについて説明します。

current_theorem

現在証明しようとしている定理の名前が入ります。 例えば、

Theorem plus_n_O : forall n : nat, n = n + O.

と入力すると、current_theorem は plus_n_O になります。

Goal forall n : nat, n = n + O.

の場合は、Unnamed_thm や Unnamed_thm0 ... となります。

証明モードに入っていないとき(トップレベルのとき)には、Coq と表示されます。

whole_state_number

その coqtop プロセスの状態番号です。一つのコマンドを行うと、1増えます。Back 1. を行うと1減って、その番号の状態になります。

theorem_stack

証明しようとしている定理のスタックです。

例えば、

Thoerem Theorem_A : ... .
Proof.
  
  Theorem Theorem_B : ... .
  Proof.

のように、ある命題 Theorem_A の証明モードに入っているときに、命題 Theorem_B の証明モードに入ると、theorem_stack は |Theorem_B|Theorem_A| となります。Theorem_B の証明が終わると、|Theorem_A| となります。

証明モードに入っていないときにはここは空で、|| になります。

theorem_state_number

現在の証明の状態番号です。証明モードに入っていないときは0ですが、証明モードに入ると1になります。 その後、証明を進めると1ずつ増えます。証明の状態を進めるようなコマンドではないときには増えません。Qed. を行うと、0(または theorem_stack の2番めの定理の状態番号)に戻ります。

どう使うか

プロンプトを使って、コマンドの結果の出力がどのような意味を持つかを判断することができます。

例えば、

• whole_state_number も theorem_state_number も変化なし => エラー
• theorem_state_number (と whole_state_number) が変化 => 現在のサブゴールの状態
• theorem_state_number は変化せず、whole_state_number のみ変化 => その他のいろいろな情報

となります。

coqtop server を書いた

Android 開発の授業の最終課題で Android 上で動く ProofGeneral 風のアプリを作ることにしたので、JSON API で操作できる coqtop サーバを書きました。その授業の発表が終わり次第公開すると思います。

can't load .so/.DLL for: というエラー

下のようなエラーが出たとき

<command line>: can't load .so/.DLL for: /Users/amutake/work/jype/jype-doc/.cabal-sandbox/lib/x86_64-osx-ghc-7.8.2/jype-0.0.1/libHSjype-0.0.1-ghc7.8.2.dylib (dlopen(/Users/amutake/work/jype/jype-doc/.
cabal-sandbox/lib/x86_64-osx-ghc-7.8.2/jype-0.0.1/libHSjype-0.0.1-ghc7.8.2.dylib, 9): Symbol not found: _jypezm0zi0zi1_DataziJypeziError_JypeCheckError_con_info
  Referenced from: /Users/amutake/work/jype/jype-doc/.cabal-sandbox/lib/x86_64-osx-ghc-7.8.2/jype-0.0.1/libHSjype-0.0.1-ghc7.8.2.dylib
  Expected in: flat namespace
 in /Users/amutake/work/jype/jype-doc/.cabal-sandbox/lib/x86_64-osx-ghc-7.8.2/jype-0.0.1/libHSjype-0.0.1-ghc7.8.2.dylib)

cabal ファイルの exposed-modules にモジュール名を書けば直る。 エラーがわかりにくい…

cabal-install の bootstrap.sh で module ‘foobar-0.0.0:Main’ is defined in multiple files ...

cabal-install の bootstrap.sh で module ‘stm-2.4.3:Main’ is defined in multiple files: ... みたいなエラーが出てコケたときは、

% cd stm-2.4.3
% ./Setup install
% cd ../
% ./bootstrap.sh

とやればよい。仕組みは不明。

$GOPATH

golang の GOPATH について。

昨日まで GOPATH で指定したディレクトリは、Haskell の .cabal ディレクトリみたいにパッケージがインストールされるだけの場所だと思ってたけど、自分でコードを書くときもこの中で作業をするということを知った。

研究室の先輩のリポジトリとか見ると、

import (
    "github.com/username/repo/package1"
    "github.com/username/repo/package2"
)

こんなふうに書いてあって、「必ず github とかに上げないといけないのだろうか…」とか思ってたけど、GOPATH の中で直接作業をすることで github に上げなくても良くなってる。

いままでそこら辺に転がっている個人のブログしか見てなかったけど、ちゃんと公式のドキュメントに書いてた。 http://golang.org/doc/code.html

更新を楽しみにしているWeb漫画10

個人的に更新を楽しみにしているWeb漫画10選です。順不同。

• パペラキュウ
• All You Need Is Kill
• 市場クロガネは稼ぎたい
• はるこ少女期
• 徒然チルドレン
• 働かないふたり
• 俺とヒーローと魔法少女
• T.Yめもり～ず
• アクアの魔法
• 裏ジャック

Why3 で遊んでみた

Why3 で遊んでみたのでメモ．インストールで手間取った．環境は Mac OS X 10.9.1 です．

Why3 のインストール

※この方法は Mac OS X かつ Homebrew 専用です．Linux や MacPorts でのインストールはわかりません．

ソースからは面倒なので，OCaml のパッケージマネージャである opam でいれます．(追記: https://github.com/mht208/homebrew-formal に Why3 の formulae があったのでそっちのほうが簡単かもしれない(試してない))

まず依存ライブラリなどをインストール．

• XQuartz をインストール
  • インストール後は再ログインが必要かもしれない
• brew install gmp
• brew install gtksourceview
  • XQuartz が必要

次に，https://github.com/OCamlPro/ocaml-top/issues/42#issuecomment-22091964 に書いてあるように，下のスクリプトを .zshrc か何かに書きこんで source .zshrc をします．これをしないと conf-gtksourceview をインストールするときにコケます．

export PKG_CONFIG_PATH=$PKG_CONFIG_PATH:/usr/X11/lib/pkgconfig/
for i in `ls /usr/local/opt/`;
do
    if [ -d "/usr/local/opt/$i/lib/pkgconfig" ];
    then export PKG_CONFIG_PATH=$PKG_CONFIG_PATH:"/usr/local/opt/$i/lib/pkgconfig";
    fi;
done

最後に opam install why3 でインストールできます．たぶん．

% why3 --version
Why3 platform, version 0.82 (build date: Fri Jan 17 00:48:01 JST 2014)

Why3IDE で遊んでみる

Why3 には IDE が付属しているので，それで遊んでみます．

IDE を起動させる前に，まずは Prover を探させます．

% why3config --detect-provers
Found prover Alt-Ergo version 0.95.2, Ok.
Warning: prover Coq version 8.4pl3 is not known to be supported.
1 provers detected and 1 provers detected with unsupported version
== Found /Users/amutake/.opam/4.01.0/lib/why3/lib/why3/plugins/dimacs.cmxs ==
== Found /Users/amutake/.opam/4.01.0/lib/why3/lib/why3/plugins/genequlin.cmxs ==
== Found /Users/amutake/.opam/4.01.0/lib/why3/lib/why3/plugins/hypothesis_selection.cmxs ==
== Found /Users/amutake/.opam/4.01.0/lib/why3/lib/why3/plugins/tptp.cmxs ==
Save config to /Users/amutake/.why3.conf

なんか Coq 8.4pl3 で Warning でてるけど気にしない．

why3ide コマンドで起動．

% why3ide .
[Info] Init the GTK interface... done.
[Info] reading icons... done.
[Info] Creating tree model... done
[Info] found directory '.' for the project
[Info] Opening session...

[Info] Opening session: update done

[Info] Opening session: done

これで X11 が立ち上がって IDE が起動するはずです．起動しない場合は XQuartz.app を立ち上げた状態で実行してみたり，マシンを再起動してみたりすると直るかもしれません．

Hello Proofs!

さて，無事起動できたので，マニュアルの 1.1 Hello Proofs をやってみます．

一旦 IDE を閉じて，以下の内容の hello_proof.why というファイルを作ってください．

theory HelloProof "My very first Why3 theory"

  goal G1 : true

  goal G2 : (true -> false) /\ (true \/ false)

  use import int.Int

  goal G3 : forall x : int. x * x >= 0

end

そしてターミナルで why3ide hello_proof.why とやると，hello_proof.why を読み込んだ IDE が起動します．

こんなかんじになるはずです．

G1 を選択して，左の Alt-Ergo ボタンを押してみましょう．

緑のチェックマークがつきました．G1 : true という命題が証明された，ということです．

HelloProof を選択して左の Alt-Ergo ボタンを押してみると，こうなります．

G2 : (true -> false) /\ (true \/ false) が残りました． 次はこの G2 をCoqを使って証明し(ようとし)てみます．

G2 を選択して，Coq ボタンを押してください．できた行を選択すると "Please Edit" と書いてあるので，左の Edit ボタンを押します．

hello_proof.why があるディレクトリに hello_proof というディレクトリができ，その中に hello_proof_HelloProof_G2_1.v というCoqのソースファイルができます．このファイルの内容は以下のようになっています．

明らかにこれは証明できません! 命題を編集して証明できるものにしましょう． 現在の Why3IDE は why ファイルを直接編集することはできないので，適当なテキストエディタで G2 を以下のように編集します．

goal G2 : (false -> false) /\ (true \/ false)

編集したら，IDE に戻ってリロード(Ctrl-r)します．obsolete になります．

G2 を選択して Alt-Ergo，Coq ボタンを押すと，もう一度 try させることができます．代わりに左上のラジオボタンを All goals にして Replay ボタンを押しても同じことができます．

Alt-Ergo で証明できてしまいましたが，せっかくなので Coq でも証明してみたいと思います．

hello_proof/hello_proof_HelloProof_G2_1.v を開くと，Theorem G2 : False. だったのがTheorem G2 : True. になっています．これは auto タクティクで証明できそうです．

保存したら IDE に戻り，G2 の Coq の行を選択して，左の Coq ボタンを押します．

緑のチェックマークがつきました!

まとめ

• Why3 をインストールしてみたよ．Why3 のインストールはすこし面倒だった．
• Why3IDE を使って簡単な命題を証明してみたよ．