类型论与coq (5-2)

比如我们要证明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

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