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

Question

除了在 SO 中的精彩讨论之外，我一直试图了解Set在 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.

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

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

请注意，我已经看到这Set是类型层次结构中的第一个“类型集”，例如Set = Type(0) <= Type = Type(1) <= Type(2) <= ... . 我想这种直觉是有道理的，就像我假设的那样nat \in Type，所有常用的编程类型都在其中，但不确定其中的内容Type不会出现在Set. 也许是递归类型？不确定这是否是正确的例子，但我试图围绕这个概念的含义以及它的概念（和实际）有用性。

标签： coq

Answer 1

虽然Set和Type在 Coq 中有所不同，但这主要是由于历史原因。如今，大多数发展并不依赖于Set不同于Type. Set特别是，如果您替换为Type到处，亚当的评论也很有意义。要点是，当您要定义可以在执行期间计算的数据类型（例如数字）时，您希望将其放入SetorType 而不是 Prop. 这是因为Prop当你从 Coq 中提取程序时，存在的东西会被删除，所以定义的东西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 会默默地把这两个Types 放在不同的宇宙层级，命令就会被接受。（这并不意味着它将具有与此示例中Type相同的行为，因为当和不同时和是不同的东西！）SetType@{u}Type@{v}uv

如果您想知道为什么此功能有用，这绝非偶然。绝大多数 Coq 开发都不依赖它。默认情况下它是关闭的，因为它与一些通常被认为在 Coq 开发中更有用的公理不兼容，例如强排中定律：

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

-impredicative-set打开后，这个公理会产生一个悖论，而默认情况下使用它是安全的。