预备知识

形式证明
首先了解形式证明(formal proof)，可以通过下面的链接进行了解
http://en.wikipedia.org/wiki/Intuitionistic_logic
http://en.wikipedia.org/wiki/Curry-Howard_correspondence
http://en.wikipedia.org/wiki/BHK_interpretation
注释
使用 (* COMMENTS HERE *) 进行注释
分隔符
每个 Coq 命令都要加上 . 表示结束
IDE
Coq 有自带的 CoqIDE，另有命令行程序 coqtop 和 Emacs 扩展 Proof General

hello world

my_first_proof

对应于 HelloWorld 的是一个简单的命题

for all things you could prove, if you have a proof of it, then you have a proof of it.

它的证明是这样的

Theorem my_first_proof : (forall A : Prop, A -> A).
Proof.
  intros A.
  intros proof_of_A.
  exact proof_of_A.
Qed.

首先通过 Theorem 来声明一个定理 my_first_proof：(forall A : Prop, A -> A)。还可以使用Lemma(引理)、Remark、Fact、 Corollary(推论)和Proposition(命题)，它们的含义是相同的。
下面的 Proof 表示证明开始，Qed 还有 Admitted、Defined 表示证明结束。

vernacular、tactics和Gallina

Coq中有三套不同的语言：

Vernacular
用来处理定义，使用大写字母开头，例如 Theorem、Proof、Qed
Tactics
用作证明过程，以小写字母开头，例如 intros、exact
Gallina
用来描述定理，例如 (forall A : Prop, A -> A)

查看证明过程

Coq 是可以查看证明的中间过程的，在菜单栏或者工具栏选择 GoTo Cursor 即可。
现在将运行到 intros proof_of_A 这行上，可以发现右上角输出如下

1 subgoal
A : Prop
proof_of_A : A
______________________________________(1/1)
A

在水平线上的称为假设(hypotheses)或上下文(the context)，在水平线下的是要证明的东西，称为 the current subgoal
我们要证明的定理(theorem)称为 goal，而 subgoal 指的是在证明过程的任意一点需要证明的东西

tactic

首先回到开始状态

1
2
3

1 subgoal
______________________________________(1/1)
forall A : Prop, A -> A

可以看到目前context啥都没有，goal是要证明的theorem。这里的A : Prop表示一个具有Prop类型的A。类似的有0 : nat表示一个自然数0，true : bool表示一个布尔值true。
->是for all的缩写，A -> A表示(forall something_of_type_A : A, A)。
证明开始，首先遇到第一个 tactic intros，intros 等于 assume，作为假设。于是现在假设有一个任意的假设 A，它在可能情况下要和 subgoal 中的变量同名

1 subgoal
A : Prop
______________________________________(1/1)
A -> A

在运行完 intros A. 后，subgoal 变成了 A -> A，在 context 中有了一个 Prop 类型的 A。
下面运行第2个 intros

Gallina

有个在 Coq 中形式化 100 个定理的网站挺有意思，可以试试。

Reference

https://coq-zh.github.io/SF-zh/lf-current/Basics.html