coq学习笔记

因为没找到比较好的 Coq 中文学习资料,所以主要根据官方 doctutorial-nahas等国外的教程来学习。

这篇文章被 deprecated 掉了,详见 Software Foundation 做题的 Notes

预备知识

  1. 形式证明
    首先了解形式证明(formal proof),可以通过下面的链接进行了解
    http://en.wikipedia.org/wiki/Intuitionistic_logic
    http://en.wikipedia.org/wiki/Curry-Howard_correspondence
    http://en.wikipedia.org/wiki/BHK_interpretation
  2. 注释
    使用 (* COMMENTS HERE *) 进行注释
  3. 分隔符
    每个 Coq 命令都要加上 . 表示结束
  4. 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.

它的证明是这样的

1
2
3
4
5
6
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(引理)、RemarkFactCorollary(推论)和Proposition(命题),它们的含义是相同的。
下面的 Proof 表示证明开始,Qed 还有 AdmittedDefined 表示证明结束。

vernacular、tactics和Gallina

Coq中有三套不同的语言:

  1. Vernacular
    用来处理定义,使用大写字母开头,例如 TheoremProofQed
  2. Tactics
    用作证明过程,以小写字母开头,例如 introsexact
  3. Gallina
    用来描述定理,例如 (forall A : Prop, A -> A)

查看证明过程

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

1
2
3
4
5
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表示一个自然数0true : bool表示一个布尔值true
->for all的缩写,A -> A表示(forall something_of_type_A : A, A)
证明开始,首先遇到第一个 tactic introsintros 等于 assume,作为假设。于是现在假设有一个任意的假设 A,它在可能情况下要和 subgoal 中的变量同名

1
2
3
4
1 subgoal
A : Prop
______________________________________(1/1)
A -> A

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

Gallina

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

Reference

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