coq-intro

Coq 入門

---

Coq とは

• 証明が正しいことを保証してくれる装置。

---

インストール

Coq 8.8.0 まではインストーラが用意されている。

• 新しさより簡単さ重視：レポジトリからインストーラを入手

• 最新版を入れたい：Coq/SSReflect/MathCompの設定を参考にコンソール上でインストール

  • sudo apt get installでなくsudo apt install
  • WSLでは「新しいライブラリの設定が要るかも」の箇所でsudo apt install -y libgmp-devが必要だった(参考)

---

エディタ

• VScode+VSCoqがおすすめ。VScode上で拡張機能(Ctrl+Shift+X)から「vscoq」と検索すれば出てくる。
  • Windowsの人はWSL上で動かせるようにRemote - WSLも入れよう。
• インストーラから入れた場合はCoqIDEも利用できる(がVSCoqの方が便利)