What does "Error: Universe inconsistency" mean in Coq?
What does "Error: Universe inconsistency" mean in Coq?
我正在研究 Software Foundations，目前正在做关于教会数字的练习。这是自然数的类型签名：
Definition nat := forall X : Type, (X -> X) -> X -> X.
我定义了一个类型为 nat -> nat 的函数 succ。我现在想像这样定义一个加法函数：
Definition plus (n m : nat) : nat := n nat succ m.
但是，我收到以下错误消息：
Error: Universe inconsistency.
此错误消息的实际含义是什么？
在 Coq 中，一切都有类型。 Type 也不例外：如果你用 Check 命令询问 Coq，它会告诉你它的类型是... Type!
实际上，这是一个谎言。如果您通过发出指令 Set Printing Universes. 来询问更多详细信息，Coq 会告诉您 Type 与第一个不同，而是一个 "bigger"。形式上，每个 Type 都有一个与之关联的索引，称为它的宇宙级别。通常打印表达式时，该索引是不可见的。因此，该问题的正确答案是 Type_i 具有类型 Type_j，对于任何索引 j > i。这是确保 Coq 理论的一致性所必需的：如果只有一个 Type，则可能会出现矛盾，类似于如果假设有一组所有套装。
为了更轻松地使用类型索引，Coq 为您提供了一些灵活性：实际上没有类型具有与之关联的固定索引。相反，Coq 会在您每次编写 Type 时生成一个新的索引变量，并跟踪内部约束以确保它们可以用满足理论要求的限制的具体值实例化。
您看到的错误消息意味着 Coq 的宇宙级别约束求解器说无法解决您要求的约束系统。问题是 nat 定义中的 forall 在 Type_i 上被量化，但是 Coq 的逻辑强制 nat 本身是 Type_j 类型，j > i。另一方面，应用程序 n nat 要求 j <= i，导致一组不可满足的索引约束。
我正在研究 Software Foundations，目前正在做关于教会数字的练习。这是自然数的类型签名：
Definition nat := forall X : Type, (X -> X) -> X -> X.
我定义了一个类型为 nat -> nat 的函数 succ。我现在想像这样定义一个加法函数：
Definition plus (n m : nat) : nat := n nat succ m.
但是，我收到以下错误消息：
Error: Universe inconsistency.
此错误消息的实际含义是什么？
在 Coq 中，一切都有类型。 Type 也不例外：如果你用 Check 命令询问 Coq，它会告诉你它的类型是... Type!
实际上，这是一个谎言。如果您通过发出指令 Set Printing Universes. 来询问更多详细信息，Coq 会告诉您 Type 与第一个不同，而是一个 "bigger"。形式上，每个 Type 都有一个与之关联的索引，称为它的宇宙级别。通常打印表达式时，该索引是不可见的。因此，该问题的正确答案是 Type_i 具有类型 Type_j，对于任何索引 j > i。这是确保 Coq 理论的一致性所必需的：如果只有一个 Type，则可能会出现矛盾，类似于如果假设有一组所有套装。
为了更轻松地使用类型索引，Coq 为您提供了一些灵活性：实际上没有类型具有与之关联的固定索引。相反，Coq 会在您每次编写 Type 时生成一个新的索引变量，并跟踪内部约束以确保它们可以用满足理论要求的限制的具体值实例化。
您看到的错误消息意味着 Coq 的宇宙级别约束求解器说无法解决您要求的约束系统。问题是 nat 定义中的 forall 在 Type_i 上被量化，但是 Coq 的逻辑强制 nat 本身是 Type_j 类型，j > i。另一方面，应用程序 n nat 要求 j <= i，导致一组不可满足的索引约束。