coq开始使用coq


备注

本节概述了coq是什么,以及开发人员可能想要使用它的原因。

它还应该提到coq中的任何大型主题,并链接到相关主题。由于coq的文档是新的,您可能需要创建这些相关主题的初始版本。

测试和安装Coq

测试无需安装

对于希望开始测试Coq而不在其机器上安装Coq的新用户,有一个名为JsCoq的在线IDE此处为演示文稿)。包子窗口允许测试各种众所周知的附加包。

安装

下载页面包含Windows和MacOS的安装程序。

通常建议使用Linux的用户使用opam从源代码编译,以获得最新版本。 这里给出有关如何操作的基本说明。

一个简单的证据

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

在浏览器中试用它

通过归纳证明的例子

这是一个简单的归纳证明。

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.
 

在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。如果遇到版本不匹配问题,可能必须再次运行makefile,明确指定Emacs路径

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

使用Nix安装

警告:这不是安装Coq的标准方法。

对于Linux(和MacOS)的用户,他们希望获得对Coq的最新版本的访问权限,或者能够在同一台机器上使用多个版本的Coq,而无需使用opam,也无需编译来源,这是一种替代解决方案。

Nix是Unix类型操作系统(如Linux和MacOS)的软件包管理器。它带有自己的软件包集合,通常比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