类型论与coq (5-4)

其实这两个类型并不是只是代表函数和笛卡尔积这么简单，我们其实可以把∏看作“对于任意的”，∑看作"存在"，比如说Π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.

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