coq学习笔记

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

预备知识

  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

Coq应该是少数的不能输出Hello, World的编程语言之一了。而对应于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(还可以使用Lemma(引理)、RemarkFactCorollary(推论)和Proposition(命题),它们的含义是相同的)来声明一个定理my_first_proof(forall A : Prop, A -> A)
下面的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 subgoal
A : Prop
proof_of_A : A
______________________________________(1/1)
A

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

tactic

首先回到开始状态

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)
证明开始,首先遇到第一个tacticintrosintros等于assume,作为我们的假设。于是现在假设有一个任意的假设A,它在可能情况下要和subgoal中的变量同名

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

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