証明駆動開発で有効なツールであるCoqの導入についてメモを残します。
MacであればHomebrewを使ってインストールできます。
brew install coq
ただ、おそらく最新版を常にインストールできるようなサポートは受けてないと思います。
気持ちよく証明を書いていくためには証明の過程を対話形式で表示してくれるツールが必要です。多くの場合はCoqIDEを導入すると思いますが、僕はVSCoqというVS Codeのプラグインを採用しています。証明をCoqIDEと同じように確認しながら書けるだけでなく、シンタックスハイライトも綺麗で見やすいです。
VS Code上でMarketplaceから検索して導入することもできますし、コマンドで導入することもできます。
code --install-extension maximedenes.vscoq
実際の画像はこんな感じで、右側に証明の現在の状態が表示されます。また、下にはSearchRewrite
など出力があれば表示します。
Macではcontrol + option + 十字キー
で証明を進めたり戻したりします。
CoqIDEが必要な場合は同じくHomebrewで導入できます。
brew cask install coqide