# coq开始使用coq

## 一个简单的证据

``````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.

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

`brew install coq`

`sudo port install coq`

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

``````;; Open .v files with Proof General's Coq mode
``` ```

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

## 使用Nix安装

Nix是Unix类型操作系统（如Linux和MacOS）的软件包管理器。它带有自己的软件包集合，通常比Debian或Ubuntu更新。它与您的发行版的包管理器不冲突，因为它不会在`/usr/bin` 等中安装任何东西。

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

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

``````\$ nix-env -iA nixpkgs.coq_8_6
``` ```

``````\$ nix-shell -p coq_8_6 --run coqide
``` ```

``````\$ nix-shell -p coq_8_6 --run emacs
``` ```

``````\$ nix-shell -p coq_8_5 --run coqide
``` ```