类型论与coq (5-1)

简介

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.

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

数学联邦政治世界观提示您：看后求收藏（同人小说网http://tongren.me），接着再看更方便。