类型论与coq

简介

COQ是基于类型论的一门语言，类型论算是一种定义数学基础的方式，事实上类型论是可以拿来代替集合论的。不过类型论和集合论有几个比较大的差别。

第一个就是类型论里面所有东西都属于某个Type，在集合论中两个比较主要的记号构成了整个集合论的东西，一个是集合，另一个则是性质(Propersition)，而在类型论中只有一个基本记号就是Type，我们应该把性质理解为用来区别一些元素的方式，或者可以这么想，我们把具有这个性质的“元素”都装进一个type里，那么证明这个性质就变成了我们要构造这个Type内的一些元素，从而在集合论中我们讲性质A有一个证明，在类型论中我们就会写作α：A，读作α是Type A里面的一个元素，当然当我们把A当作一个集合来看待的时候α：A就等于是α∈A。这里值得一提的是当我们使用α：A这个记号的时候，我们相当于事先承认了α，A的存在性，所以我们就没有办法说比如“如果α：A”，或者其他一些类似的说法。

函数Type

我们介绍的第一个Type是函数这个Type

Def 1. 给定两个Type A，B，我们构造一个函数Type：A → B，其中他的定义域为A，陪域为B，对于一个函数f：A → B，我们将一个定义域内的元素α：A作用f，得到α对应的值，f(α)：B

我们有几种办法来定义如何通过A中的元素来找到对应B中的元素，第一种是我们直接给出一个表达式Φ，然后我们记作

f：≡Φ

𝔸 𝔹 ℂ 𝔻 𝔼 𝔽 𝔾 ℍ 𝕀 𝕁 𝕂 𝕃 𝕄 ℕ 𝕆 ℙ ℚ ℝ 𝕊 𝕋 𝕌 𝕍 𝕎 𝕏 𝕐 ℤ

这里我们注意到我们其实需要去验证定义的合法性，也就是说我们需要验证给定x：A，Φ是否给出一个B中的元素，举个例子f：ℕ → ℕ，f：≡ x＋x。

那么此时f(2)就会定义等于2＋2，这里注意到一点，在类型论中等于有两种不同的等于，第一种叫定义等于，我们记作α≡b，所谓定义等于就跟他的名字一样，意思就是说我们可以直接通过定义来发现他们之间是相等的，比如在这里根据定义我们知道f(2)≡2＋2，另一种我们则称为性质等于，为什么叫性质等于呢，因为这个等于更多的是在说这两个元素在当前这个性质下是一样的，形式的讲，给定一个Type A，和α，b：A，我们记作α＝ᴀ b 如果α，b不可以通过A被区分出来，比如说这里我们就可以发现通过加法我们并没有办法区分f(2)和4，所以我们就有f(2)＝4，这里就应该是性质等于。

如果我们不想给这个函数一个名字，那么我们也可以使用λ-abstration，即λ(x：A). Φ，所以我们有

(λ(x：A).Φ)：A → B

或者我们也可以简记为λx，比如说上文那个例子我们就可以写成λx.x＋x。我们有时候也用一条横线来代替变量，比如说g(x，–)就是λy.g(x，y)，很自然的我们应该可以发现

f≡(λx.f(x))

这个也叫做uniqueness principle for function type.

就像我们之前讲的，在类型论里所有东西都是Type，那么自然的性质也是一种Type，那么自然在coq里面也是如此，我们可以通过以下方法来定义。

Require Import ssreflect.

Parameter A B C D : Prop.

这里我们可以先稍微提一下在类型论中是怎么证明定理的，当然在之后我们会给出更多的信息。

比如我们要证明A → B，我们想想我们应该如何做证明，是不是就是我们考虑任意一个满足性质A的东西，然后我们通过"证明"来得到一个对应的属于性质B的元素，那这个就好比说我们先找一个α：A，然后我们构造一个函数f，这个函数f自然只能使用我们已有的条件，最后我们应该能得到f(α)：B，即f：A → B.

那在coq中怎么做呢，我们需要介绍几个关键字，第一个是move，比如说我们现在要证明

Lemma move_ex : A-＞A.

我们可以使用move指令来获得一个A中的元素，具体是这么操作的

move=＞a.

这个可以这么看，我们通过move指令获得了A → A定义域中的一个元素，然后我们就现在需要做的是，根据我们已有条件α：A，这是通过move得到的，我们希望证明，或者说我们希望构造一个函数最后获得一个A中的元素，怎么做呢？自然是直接返回我们已有的α就好了，所以整个完整的证明就是。

Lemma move_ex : A-＞A.

proof.

move=＞ a.

apply a.

Qed.

这里值得一提的是在Coq中每行末尾需要使用一个.来表示结束，并且在证明结束的时候使用Qed.表示完结。

那让我们来再看一个例子

Lemma move_ex : A-＞B-＞A.

我们自然而然地还是先获得我们的假设条件

move=＞a.

于是我们现在需要做的是要通过这个α：A构造一个B → A的东西，那很自然的我们想我们再继续获得B中的一个元素。

move=＞b.

这里我们也可以把这两行写到一行变成：

move=＞a b.

于是现在我们只需要给出一个A中的元素就行了，所以我们可以进行

apply a.

此处我们留一道习题以示友好

Lemma ex1 : (A -＞ B -＞ C) -＞ (B -＞ A) -＞ B -＞ C.

宇宙和族

在类型论里面类似于集合论的我们也有宇宙和类型族的概念，但是这里的宇宙跟集合论里的宇宙其实不太一样，在这里我们把元素为Type的Type作为宇宙，比如说所有的Prop就是一个宇宙，因为里面的元素都是一些别的Type，比如说性质A，但是于集合论相似的是我们仍然没有办法找到一个宇宙使得他自己包含自己。

为了避免自指的情况出现，我们对宇宙进行分层，这是一个很常见的操作，具体行为如下：

U₀：U₁：U₂：. . .

当然一般在不引起歧义的情况下我们更愿意直接写成U。

至于类型族的定义则是完全于集合论类似的，对于给定一个Type A，我们考虑函数B：A → U，这个函数我们就成为一个类型族，毕竟如果考虑α：A，f(α)：U是一个Type

∏-Type与∑-Type/Dependent function types

这个东西给出了函数的更一般的定义，我们回顾之前我们定义的函数，是f：A → B，于是我们给一个α：A，f(α)：B，这是一个非常局限的定义，有时候我们会希望α对应的值所在的类依赖于α的选取，那么这个时候我们就需要用到∏-Type。具体定义如下：

Def 2. 给定一个类型A：U，和一个类型族B：A → U，我们考虑函数

∏，B(x)：U

x：A

注意到当B是一个常类型族即将所有的α：A都映到同一个类，此时

∏ B：U≡(A → B)

x：A

介绍完这个之后我们再来稍微介绍一下所谓的∑-Type，其实这个Type就是笛卡尔积的推广

Def 3. 给定一个类型A：U，和一个类型族B：A → U，我们考虑函数

∑ B(x)：U，

x：A

注意到当B是一个常类型族即将所有的α：A都映到同一个类，此时

∑ B：U≡(A × B)，

x：A

并且我们有，对于给定的α：A，b：B(α)那么

(α，b)：∑ 。

(x：A)B(x)

这里有个非常有意思的值得一提的点是在集合论中我们假设A × B中的元素都是形如(α，b)的，而在类型论中则不然，我们更多的是通过假设定义在

∑ B(x)

x：A

的函数只需要给出在所有形如(α，b)处的值，那么这个函数就是良定的，通过这一点我们就可以证明所有

∑ B(x)

x：A

的元素都是形如(α，b)的了

在这里我们希望多提一点的是，如果我们给定了一个函数

g：∏ B(x) → C，

x：A

那么我们可以递归的定义一个函数f：(∑B(x)) → C，并且f满足

x：A

f((α，b))：≡g(α)(b)

首先我们先定义投影函数如下

pr₁：(∑B(x)) → A

x：A

＜br＞pr₁((α，b))：≡α

以及

pr₂： ∏ B(pr₁(p))

p：∑x：A B(x)

我们希望归纳的定义p₂，那现在考虑一个类型族C：(∑B(x)) → U假设我们已经有了函数 x：A

g：∏ ∏ C((α，b))

α：A b∈B(α)

那么我们就可定义

f： ∏ → C(p)

p：∑x：A B(x)

为

f((α，b))：≡g(α)(b)

于是我们现在可以令C(p)：≡ B(pr₁(p))，于是我们就可以定义我们的

pr₂： ∏ B(pr₁(p))了，

p：∑x：A B(x)

pr₂((α，b))：≡b

我们现在可以把我们上面做的递归和归纳的东西打包成两个函数

rec∑x：A B(x)：∏(Πx：A B)(x) → C) ↓

C：U

→ (Σx：A B(x)) → C

写成表达式就是

recΣx：A B(x)： ∏ (Πα：AΠb：B(α)C((α，b))) → ∏ C(p)

C：(Σx：A B(x)) → U

p：Σx：A B(x)

写成表达式就是

indΣx：A B(x)(C，g，(α，b))：≡g(α)(b)

当然，很明显的看到当递归其实就是归纳在C是常数的特例

其实这两个类型并不是只是代表函数和笛卡尔积这么简单，我们其实可以把∏看作“对于任意的”，∑看作"存在"，比如说Πx：A B(x)就是说对于任意的x∈A都有B(x)成立，比如P，Q是关于正整数的两个性质，我们想描述对于任意的n∈ℕ都有P(n) → Q(n)，写法就是Πn：ℕ(P(n) → Q(n))，对于∑是类似的，那我们怎么在coq里面写有量词的证明呢？

先来看“对于任意的”，想想什么叫对于任意的n∈ℕ，其实我们是不是也可以这么理解，我们先固定一个n，但是我们不假设n具有任何特殊的性质，除了他是整数以外，如果我们还能得到命题成立，或者用类型论的话说能够找到这个性质内的一个元素，那么我们就可以说对于任意的n∈ℕ这个性质都成立。

所以我们可以继续使用

move =＞ a

来获得任意取一个A里面的元素的结果。

对于存在量词的证明就更为简单了，我们只需要使用

exists

就可以了。

首先对本节的下文我们事先假设

Parameter P : nat -＞ Prop.

Parameter Q : nat -＞ Prop.

Axiom PQ : forall n, P n -＞ Q n.

我们来看一道题：

Lemma q1 : (P 3) -＞ exists x, Q x.

我们要证明这个引理，我们想想要怎么办，首先看看我们的条件，我们有的是P3是正确的所以我们可以先通过move指令来获得这个条件，然后我们就等于是知道了在x＝3的时候P成立，根据我们上文定义的公理我们知道如果Pn成立那么Qn也成立，于是我们就只需要exists3然后再运用公理即可，完整代码如下

Lemma q1 : (P 3) -＞ exists x, Q x.

Proof.

move =＞ P3.

exists 3.

apply PQ.

apply P3.

Qed.

那我们来稍微进阶一点，考虑这个习题

Lemma q1' : (exists x, P x) -＞ exists x, Q x.

这里我们韦依需要改变的地方就是在第一步提取条件的时候，首先我们进行

move =＞ px.

这个时候你会发现我们同时把

(exists x, P x)

给提出来了，我们还需要知道P成立时的x所以我们还需要move指令

move:px=＞[x p].

其余的都没有什么区别，完整代码如下：

Lemma q1' : (exists x, P x) -＞ exists x, Q x.

Proof.

move =＞ px.

move: px =＞ [x p].

exists x.

apply PQ.

apply p.

Qed.

现在我们来看一下对于forall的证明

Lemma q2 : ~(exists x, P x) -＞ forall x, ~P x.

这里值得重新回顾一下的是在coq里面 A其实就是A → fαlse所以其实这里面是有 A这个假设的，或者说我们实际上是要找到一个函数f：A → fαlse。

我们第一步当然是先获得假设条件

move =＞ nx.

这个时候我们需要做的是证明Πx：A fαlse，就像我们前文所说的，这里我们其实可以固定一个x：A只不过我们没有任何额外的关于x的信息，所以我们可以

move =＞ x.

在然后我们会发现我们现在要的东西变成了P(x) → fαlse，所以我们还可以

move =＞ Px.

这个时候我们看看我们都有什么已知的东西：

nx : ~ (exists x : nat, P x)

x : nat

px : P x

而我们要的是一个False，那我们已有的里面谁的值域是False呢，自然是nx，所以我们使用

apply nx.

这个时候我们要的变成了nx的定义域也就是

exists x0 : nat, P x0

于是我们只需要

exists x.

apply px.

就行了，完整代码如下：

Lemma q2 : ~(exists x, P x) -＞ forall x, ~P x.

Proof.

move =＞ nx x px.

apply nx.

exists x.

apply px.

Qed.

现在我们给出如下公理

Axiom DNE : forall A : Prop, ~(~A) -＞ A.

然后留两个习题

Lemma excluded_middle : forall A:Prop, A \/ ~A.

Lemma drinker_paradox (P : nat -＞ Prop) :

exists x : nat, forall y : nat, P x -＞ P y.

数学联邦政治世界观提示您：看后求收藏（笔尖小说网http://www.bjxsw.cc），接着再看更方便。