この記事は, VSCodeでCoqを動かすための環境構築に関する備忘録です.
この記事は備忘録であるので, あまり参考にしない方が良いと思います.
私の環境で上手く動くようになっただけで, これが正しいかは分かりません.

VSCodeでCoqの環境構築

Coqのインストール

Coqの公式サイト上部のGet Coqを押す.
The Coq PlatformのWindows and macOS installersを押すと, GithubのCoq/platformに飛ぶ.
1番下のAssetsから最新版(Coq-Platform-release-yyyy.mm.dd-version_hoge_yyyy.mm.dd-windows-x86_64_signed.exe)を選択する.
インストールした.exeファイルを押すと, Coqのインストールが始まる.

環境変数の編集

環境変数の編集でPathの編集から

C:\Coq-Platform~8.15~2022.04\bin

を追加する. (数字はインストールしたCoqのverによって変わる.)

VSCodeで書いてみる

Coqのインストールは済んだので, VSCode上で動かすための準備をする.

VSCodeの拡張機能

VSCodeの拡張機能の検索でvscoqと入力し, 出てくるvscoqをインストールする.

ファイルの作成1

Ctrl + Nで作成し, test1.vで保存し, 以下のコードを書く. (Coqの拡張子は.vである.)

Definition one := 1.
Print one.

プレビュー機能

Fn + F1でコマンドパレットを開き, >Coq: Open proof viewを押す. この時, 右側にPrrofView:test1.vが出れば良い.
ソースコードの1番上の行にカーソルを合わせて, Alt + ↓キーで1番下まで選択する.
この時, 下のOUTPUTに

 one = 1
     : nat

と出力される.
右のプレビュー画面は

Not in proof mode

である.

ファイルの作成2

Ctrl + Nで作成し, test2.vで保存し, 以下のコードを書く.

Require Import Arith.
Definition f x := x + 1.

Definition g x := x - 1.

Theorem g_f : forall x, g (f x) = x.
Proof.
    intros x.
    unfold f, g.
    SearchRewrite(_ + _ - _).
    rewrite Nat.add_sub.
    reflexivity.
Qed.

プレビュー画面の変化を見ていく.
(詳しい説明は次回以降の記事でしたい.)
ソースコードの1番上の行にカーソルを合わせて, Alt + ↓キーで6行目まで進めると,

(1/1)
forall x : nat, g (f x) = x

8行目まで進めると,

x : nat
(1/1)
g (f x) = x

9行目まで進めると,

x : nat
(1/1)
x + 1 - 1 = x

10行目まで進めると, OUTPUTに

Nat.add_sub: forall n m : nat, n + m - m = n
minus_plus: forall n m : nat, n + m - n = m
minus_plus_simpl_l_reverse: forall n m p : nat, n - m = p + n - (p + m)
Nat.add_sub_swap: forall n m p : nat, p <= n -> n + m - p = n - p + m
Nat.add_sub_assoc: forall n m p : nat, p <= m -> n + (m - p) = n + m - p

11行目まで進めると,

x : nat
(1/1)
x = x

12行目まで進めると,

No more subgoals

13行目まで進めると,

Not in proof mode

となる.

終わりに

意外に簡単だったので, これでこの先も上手くいくことを願います.
次回以降で, Coqの記事を(備忘録として)書いていきたい.

参考文献

Coqの公式サイト
 Visial Studio CodeでCoqの環境作ってみた