依赖对类型

Question

在软件基础知识中，Coq 中的逻辑，我们引入了参数化命题：

Definition is_three (n : nat) : Prop :=
n = 3.
Check is_three.
(* ===> nat -> Prop *)

这让我想起了依赖对类型，从Reading HoTT in Coq我们需要定义依赖对类型：

Inductive sigT {A:Type} (P:A -> Type) : Type :=
existT : forall x :A, P x -> sigT P.

有人可以解释一下它们有什么不同吗？在 Reading HoTT in Coq 中，它说“因为我们还没有定义命题相等，所以我们不能做 这里有很多有趣的事情”，为什么我们不能在没有命题相等的情况下做任何有趣的事情？

Answer 1

现在让我们假设 HoTT 代码使用

A -> Prop

而不是

A -> Type

；两者之间的区别与你的问题正交。

参数化命题

P : A -> Prop

只是

A

类型元素的属性。 除了上面简单的

is_three

命题之外，我们还可以用这种方式表达自然数更复杂的属性。 例如：

Definition even (n : nat) : Prop :=
  exists p, n = 2 * p.

Definition prime (n : nat) : Prop :=
  n >= 2 /\
  forall p q, n = p * q -> p = n \/ p = 1.

类型

sigT A P

类型允许我们将类型

A

限制为满足属性

P

的元素。 例如，

sigT nat even

是所有偶数的类型，

sigT nat prime

是所有素数的类型等等。在Coq中，属性是更原始的概念，像

sigT

这样的子集类型是派生概念。

在传统数学中，属性和子集的概念几乎可以混为一谈：说2是素数就相当于说它属于所有素数的集合。 在 Coq 的类型理论中，情况并非如此，因为作为类型的元素不是一个命题：例如，你不能陈述一个定理说 2 是

sigT nat prime

的元素。 以下代码片段会引发错误：

Lemma bogus : (2 : {x : nat & prime x}).
(* Error: *)
(* The term "2" has type "nat" while it is expected to have type *)
(*  "{x : nat & prime x}". *)

（

{ ... & ... }

是Coq标准库中定义的

sigT

类型的语法糖。）

我们能得到的最接近的是可以从该类型中提取 2：

Lemma fixed : exists x : {x : nat & prime x}, 2 = projT1 x.

其中

projT1

是提取依赖对的第一个分量的函数。 然而，这比简单地声明 2 是素数要麻烦得多：

Lemma prime_two : prime 2.

一般来说，参数化命题在 Coq 中更有用，但有些情况下

sigT

类型会派上用场；例如，当我们只关心满足某个属性的类型的元素时。 想象一下，您使用一种二叉搜索树在 Coq 中实现关联映射。 您可以首先定义

任意

树的类型 tree：

Inductive tree :
| Leaf : tree
| Node : tree -> nat -> nat -> tree -> tree.

该类型定义了一棵二叉树，其节点存储自然数的键值对。 为了使用这种类型实现查找元素、更新值等功能，我们可以维护树的键已排序的不变量（即，左子树上的键小于一个节点，右子树则相反）。 由于该树的用户不想考虑不满足此不变量的树，因此我们可以使用类型

sigT tree well_formed

来代替，其中

well_formed : tree -> Prop

表示上述不变量。 主要优点是，这简化了我们库的接口：而不是有一个单独的引理来说明插入函数保留不变式，这将自动以插入函数本身的类型表示；用户甚至不需要费心争论他们使用接口构建的树是否尊重不变式。

关于你的第二个问题，平等是如此基本，没有它就很难定义有趣的属性。 例如，上面的属性

even

和

prime

都是使用相等性定义的。