coq - `Set` 类型的具体示例是什么？ `Set` 的含义是什么？

Question

我一直在努力理解 Set 是什么除了this great discussion in SO 是在Adam Chlipala 的书中遇到之后.他的第一个示例定义二进制操作使用 Set :

Inductive binop : Set := Plus | Times.

他在那本书中说:

Second, there is the : Set fragment, which declares that we are defining a datatype that should be thought of as a constituent of programs.

这让我很困惑。 Adam 在这里是什么意思？

此外，我认为一些额外的具体例子将有助于我的理解。我不是 Coq 专家，所以我不确定哪种类型的示例会有帮助，但一些简单且非常具体/ Root 的示例可能会有用。

请注意，我已经看到 Set是类型层次结构中的第一个“类型集”，例如Set = Type(0) <= Type = Type(1) <= Type(2) <= ... .我想这种直觉上是有道理的，就像我假设的一样 nat \in Type以及所有常用的编程类型，但不确定 Type 中的内容那不会在 Set 中.也许递归类型？不确定这是否是正确的示例，但我正在努力思考这个概念的含义以及它在概念(和实践)上的用处。

Answer 1

虽然 Set 和 Type 在 Coq 中是不同的，但这主要是由于历史原因造成的。如今，大多数开发并不依赖于 Set 不同于 Type。特别是，如果您在所有地方将 Set 替换为 Type，Adam 的评论也会有意义。要点是，当你想定义一个你可以在执行期间计算的数据类型(例如一个数字)时，你想把它放在 Set 或 Type < em>而不是 Prop。这是因为当您从 Coq 中提取程序时，Prop 中的内容会被删除，因此 Prop 中定义的内容最终不会计算任何内容。

关于您的第二个问题:Set 存在于 Type 中，但不存在于 Set 中，如以下代码片段所示。

Check Set : Type. (* This works *)
Fail Check Set : Set.
(* The command has indeed failed with message: *)
(* The term "Set" has type "Type" while it is expected to have type  *)
(* "Set" (universe inconsistency: Cannot enforce Set+1 <= Set). *)

这个限制是为了防止理论中的悖论。默认情况下，这几乎是您在 Set 和 Type 之间看到的唯一区别。您还可以通过使用 -impredicative-set 选项调用 Coq 来使它们更加不同:

(* Needs -impredicative-set; otherwise, the first line will also fail.*)
Check (forall A : Set, A -> A) : Set.
Universe u.
Fail Check (forall A : Type@{u}, A -> A) : Type@{u}.
(* The command has indeed failed with message: *)
(* The term "forall A : Type, A -> A" has type "Type@{u+1}" *)
(* while it is expected to have type "Type@{u}" (universe inconsistency: Cannot enforce *)
(* u < u because u = u). *)

请注意，我必须添加 Universe u. 声明以强制 Type 的两次出现处于同一级别。如果没有这个声明，Coq 会默默地将两个 Type 放在不同的宇宙级别，并且命令会被接受。 (这并不意味着 Type 与本例中的 Set 具有相同的行为，因为 Type@{u} 和 Type当 u 和 v 不同时，@{v} 是不同的东西!)

如果您想知道此功能为何有用，那绝非偶然。绝大多数 Coq 开发并不依赖于它。它默认关闭，因为它与一些通常被认为在 Coq 开发中更有用的公理不兼容，例如强排中律:

forall A : Prop, {A} + {~ A}

启用 -impredicative-set 时，此公理会产生一个悖论，但默认情况下使用它是安全的。