この記事は, 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の記事を(備忘録として)書いていきたい.