Ubuntu 16.04上にCoq, SSReflect, MathCompのインストール

Coq/SSReflect/MathCompによる定理証明フリーソフトではじめる数学の形式化 | 森北出版株式会社を買ったので、とりあえず環境だけ整える。

インストール環境

% uname -a
Linux pi 4.4.0-122-generic #146-Ubuntu SMP Mon Apr 23 15:34:04 UTC 2018 x86_64 x86_64 x86_64 GNU/Linux

% more /etc/lsb-release 
DISTRIB_ID=Ubuntu
DISTRIB_RELEASE=16.04
DISTRIB_CODENAME=xenial
DISTRIB_DESCRIPTION="Ubuntu 16.04.4 LTS"

Ubuntu 16.04のパッケージシステムに従うとcoqのヴァージョンが古いのでCoq/SSReflect/MathCompの設定を参考にコンパイルする。

Ocamlのインストール

% sudo aptitude install ocaml
% ocamlc -v
The OCaml compiler, version 4.02.3
Standard library directory: /usr/lib/ocaml

Coqのインストール

Releases · coq/coq · GitHubよりダウンロード。本では8.7.0をインストールしているが、8.8.0をインストールしてみる。

上述の本のバージョンよりかなり古い。

% tar xvfz coq-8.8.0.tar.gz
% cd coq-8.8.0
% ./configure |& tee configure.log
% make -j |& tee make.log
% sudo make install |& tee make_install.log
% coqc -v
The Coq Proof Assistant, version 8.8.0 (May 2018)
compiled on May 8 2018 20:32:08 with OCaml 4.02.3

MathCompとSSReflectのインストール

Releases · math-comp/math-comp · GitHubから1.7.0をダウンロードする。

% tar xvfz math-comp-mathcomp-1.7.0.tar.gz
% cd math-comp-mathcomp-1.7.0/mathcomp
% export COQBIN=/usr/local/bin/  （bashやzshの場合）
% setenv COQBIN /usr/local/bin/  （cshやtcshの場合）
% make -j 3 |& tee make.log
% sudo make install |& tee make_install.log

動作確認

起動する。

% coqide &

開いたウィンドウの左側に以下を入力する。

From mathcomp Require Import ssreflect.

Section ModusPonens.

Variables X Y : Prop.

Hypothesis XtoY_is_true: X -> Y.
Hypothesis X_is_true: X.

Theorem MP : Y.

Proof.
move: X_is_true.
by [].
Qed.

End ModusPonens.

実行してみる。

発声練習