在Coq中定义子类型关系 [英] Defining subtype relation in Coq

问题描述

有没有一种方法可以在Coq中定义子类型关系?

我读到有关子集类型的信息，其中使用谓词来确定子类型的内容，但这不是我的目标.我只想定义一个理论，其中有一个类型(U)和另一个类型(I)，它是(U)的子类型.

解决方案

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用户手册详细介绍了强制./p>

Is there a way to define subtype relationship in Coq?

I read about subset typing, in which a predicate is used to determine what goes into the subtype, but this is not what I am aiming for. I just want to define a theory in which there is a type (U) and another type (I), which is subtype of (U).

解决方案

There is no true subtyping in Coq (except for universe subtyping, which is probably not what you want). The closest alternative is to use coercions, which are functions that the Coq type checker inserts automatically whenever it is expecting an element of one type but finds an element of another type instead. For instance, consider the following coercion from booleans to natural numbers:

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

Coercion nat_of_bool : bool >-> nat.

After running this snippet, Coq uses nat_of_bool to convert bool to nat, as shown here:

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

Thus, bool starts behaving almost as if it were a subtype of nat.

Though nat_of_bool does not appear here, it is just being hidden by Coq's printer. This term is actually the same thing as nat_of_bool true + 3, as we can see by asking Coq to print all coercions:

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

The :> symbol you had asked about earlier, when used in a record declaration, is doing the same thing. For instance, the code

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

is equivalent to

Record foo := Foo {
  sort : Type
}.

Coercion sort : foo >-> Sortclass.

where Sortclass is a special coercion target for Type, Prop and Set.

The Coq user manual describes coercions in more detail.

这篇关于在Coq中定义子类型关系的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！