在Coq中定义子类型关系

Question

是否有方法在Coq中定义子类型关系？

我读过关于子集类型的文章，在子集类型中，谓词用于确定进入子类型的内容，但这不是我的目标。我只想定义一个理论，在这个理论中有一个类型(U(和另一种类型(I(，它是(U(的子类型。

Answer 1

Coq中没有真正的子类型(除了universe子类型，这可能不是你想要的(。最接近的替代方案是使用矫顽力，这是Coq类型检查器在期望一个类型的元素但却找到另一个类型元素时自动插入的函数。例如，考虑以下从布尔到自然数的强制：

Definition nat_of_bool (b : bool) : nat :=
if b then 1 else 0.
Coercion nat_of_bool : bool >-> nat.

运行此代码段后，Coq使用nat_of_bool将bool转换为nat，如下所示：

Check true + 3.
(* true + 3 : nat *)

因此，bool开始表现得几乎就像它是nat的一个亚型。

虽然nat_of_bool没有出现在这里，但它只是被Coq的打印机隐藏了。这个术语实际上和nat_of_bool true + 3是一样的，我们可以通过要求Coq打印所有矫顽力来看到：

Set Printing Coercions.
Check true + 3.
(* nat_of_bool true + 3 : nat *)

当您在记录声明中使用之前询问的:>符号时，它也在做同样的事情。例如，代码

Record foo := Foo {
sort :> Type
}.

相当于

Record foo := Foo {
sort : Type
}.
Coercion sort : foo >-> Sortclass.

其中Sortclass是针对Type、Prop和Set的特殊强制目标。

Coq用户手册更详细地描述了胁迫。