coq チュートリアル
coqを使い始める

備考

Coqのテストとインストール

インストールせずにテストする

マシンにインストールせずにCoqのテストを開始したい新しいユーザーのために、 JsCoqと呼ばれるオンラインIDEがあります （ ここでのプレゼンテーション）。パッケージサブウィンドウは、よく知られているさまざまな追加パッケージのテストを可能にします。

インストール

ダウンロードページには、WindowsとMacOSのインストーラが含まれています。

Linuxのユーザーは、一般的に最新のバージョンを入手するために、opamを使用してソースからコンパイルすることをお勧めします。これを行う方法の基本的な説明がここに記載されています 。

簡単な証明

Theorem my_first_theorem : 1 + 1 = 2.
Proof.
  reflexivity.
Qed.

あなたのブラウザで試してみてください 。

MacOSにCoqをインストールする

ここからdmgパッケージをダウンロードすると、バンドル全体をインストールできます 。

このバンドルにはCoqIDEが含まれています。この証明書はあなたの証明書の作成に使用できます。また、 coqtopコマンドを使用して端末上でインタープリタを実行することもできます

MacOS上にCoqをインストールすることは、自作ソフトを使っても簡単です

brew install coq

またはMacPortsを使用している場合

sudo port install coq

Coqには良いviサポートはありません。使いやすさの良いemacsでProof Generalを使うことができます。

Proof Generalをインストールするには、Proof Generalの古いバージョンを削除します。GitHubから新しいバージョンを複製します。

git clone https://github.com/ProofGeneral/PG ~/.emacs.d/lisp/PG
cd ~/.emacs.d/lisp/PG
make

次に、あなたの.emacsに以下を追加してください：

;; Open .v files with Proof General's Coq mode
(load "~/.emacs.d/lisp/PG/generic/proof-site")

実際のEmacsを実行しているEmacsであることを確認してください。バージョンの不一致の問題が発生した場合は、明示的にEmacsパスを指定してmakefileを再度実行する必要があります

make clean; make EMACS=/Applications/Emacs.app/Contents/MacOS/Emacs

Nixによるインストール

警告：これはCoqをインストールする標準的な方法ではありません。

最新のCoqのバージョンにアクセスしたい、あるいは同じマシン上で複数のバージョンのCoqを使用できるようにするLinux（およびMacOS）のユーザーにとっては、opamの使用が面倒でなく、またコンパイルする必要もありませんこれは別の解決策です。

NixはLinuxやMacOSのようなUnix型OSのパッケージマネージャです。これにはDebianやUbuntuよりもはるかに最新の状態に保たれた独自のパッケージが付属しています。 /usr/binなどには何もインストールされないので、ディストリビューションのパッケージマネージャーと競合しません。

まず、 Nixをインストールする必要があります。

$ curl https://nixos.org/nix/install | sh

必要な環境変数が設定されていることを確認するには、再度ログインするか、次のように入力します。

. $HOME/.nix-profile/etc/profile.d/nix.sh

次に、次のコマンドを実行してCoqの最新バージョンをインストールします。

$ nix-env -iA nixpkgs.coq_8_6

PATHに何も追加せずにCoqIDEを実行することもできます：

$ nix-shell -p coq_8_6 --run coqide

同様に（すでにEmacsとProof-Generalがインストールされていると仮定します）：

$ nix-shell -p coq_8_6 --run emacs

これは、必要なときに異なるバージョンを実行するのに非常に便利です。たとえば、Coq 8.5を実行するには、次のコマンドを使用します。

$ nix-shell -p coq_8_5 --run coqide

帰納法による証明の例

ここで誘導による簡単な証明があります。

Require Import Coq.Setoids.Setoid.
Require Import Coq.Arith.Lt.

(* A number is less than or equal to itself *)
Theorem aLTEa : forall a,
    a <= a.
    auto with arith. (* This follows by simple arithmetic *)
    Qed.

Theorem simplALTE : forall a b,
    S a <= S b <-> a <= b. (* If a <= b, then a + 1 <= b + 1 *)
Proof.
Admitted.

Theorem ltAlwaysLt: forall a b,
    a <= a + b.
Proof.
  intros. (* Introduce relevant variables *)
  induction a, b. (* Induction on every variable *)
  simpl. apply aLTEa. (* 0 <= 0 + S b *)
  rewrite -> plus_O_n. auto with arith. (* 0 <= S b *)
  rewrite <- plus_n_O. apply aLTEa. (* S a <= S a + 0 *)
  rewrite <- simplALTE in IHa. (* IHa: a <= a + S b. Goal: S a <= S a + S b. *)
  apply IHa. (* We rewrote the induction hypothesis to be in the same form as the goal, so it applies immediately now *)
  Qed.