在 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 user manual 更详细地描述了强制转换。

Defining subtype relation in Coq