はじめに

久々に Coq で遊びたくなったので、M1 Mac にインストールしてみた。 最近の Coq は VSCode で書くのが主流？らしいが、今回は Emacs + Proof-General で環境構築を行う。

環境構築の方法

基本的にbrewやmelpaなどの package 管理システムになるべく依存した形で環境構築を行う。

はじめに、Coqのインストール(–build-from-source をつけないとcoqtop実行時にエラーが出た。)

brew install coq --build-from-source

GUI 版 Emacs のインストール

brew install emacs --cask

Emacs の設定

次は Emacs の設定を行う。 Emacs の設定ファイルは~/.emacs.d/init.elに記載する。

まずはmelpa(Emacs のプラグインのパッケージマネージャー)のセットアップを行う。 ~/.emacs.d/init.elに以下を記載し、

(require 'package)
(let* ((no-ssl (and (memq system-type '(windows-nt ms-dos))
                    (not (gnutls-available-p))))
       (proto (if no-ssl "http" "https")))
  (add-to-list 'package-archives
               (cons "melpa" (concat proto "://melpa.org/packages/")) t))
(package-initialize)

emacs を起動して

M-x package-refresh-contents RET ← 初回のみ実行

を実行する。

次に、~/.emacs.d/init.elに以下を記載し、

(setq proof-splash-enable nil)

(custom-set-variables
  '(coq-prog-name "/opt/homebrew/bin/coqtop")
  '(package-selected-packages
     (quote
       (company-coq company proof-general)))
  '(proof-three-window-enable t))

(add-hook 'coq-mode-hook 'company-coq-mode)

emacs を起動して

M-x package-install-selected-packages RET

を実行する。 これで環境構築が完了。

おまけ

ssreflect のインストール

brew install ssreflect --build-from-source

参考: SSReflect ノート

ProofGeneral で使うキーバインド

キー動作
C-c C-n次の.まで進む
C-c C-u次の.まで進む
C-c C-Enterカーソル位置まで進める

参考: ProofGeneral/Keybinds

ヒルベルトの公理系を示す。

久々の Coq なのでウォーミングアップとしてヒルベルトの公理系を証明してみる。

From mathcomp
       Require Import ssreflect.

Require Import Classical.

Section Coq_test.

  Variable A B C:Prop.

  Lemma H1: A->(B->A).
  Proof.
    move => //.
  Qed.

  Lemma H2: (A->(B->C))->((A->B)->(A->C)).
  Proof.
    move => x y z.
    apply x => //.
    apply y => //.
  Qed.

  Lemma H3: (~C-> ~A)->(A->C).
  Proof.
    move => x y.
    specialize (classic C).
    elim => z //.
    specialize (x z).
    contradiction.
  Qed.

End Coq_test.

感想

  • CoqIDE もいいけど、Emacs + ProofGeneral + company-coq をやると最強になる。