証明駆動開発で有効なツールであるCoqの導入についてメモを残します。

Homebrewを使ってCoqをいれる

MacであればHomebrewを使ってインストールできます。

brew install coq

ただ、おそらく最新版を常にインストールできるようなサポートは受けてないと思います。

VS Codeプラグインの導入

気持ちよく証明を書いていくためには証明の過程を対話形式で表示してくれるツールが必要です。多くの場合はCoqIDEを導入すると思いますが、僕はVSCoqというVS Codeのプラグインを採用しています。証明をCoqIDEと同じように確認しながら書けるだけでなく、シンタックスハイライトも綺麗で見やすいです。

VS Code上でMarketplaceから検索して導入することもできますし、コマンドで導入することもできます。

code --install-extension maximedenes.vscoq

実際の画像はこんな感じで、右側に証明の現在の状態が表示されます。また、下にはSearchRewriteなど出力があれば表示します。

Macではcontrol + option + 十字キーで証明を進めたり戻したりします。

CoqIDE

CoqIDEが必要な場合は同じくHomebrewで導入できます。

brew cask install coqide