宇宙不一致的简单案例 [英] A simple case of universe inconsistency

问题描述

我可以定义以下归纳类型：

I can define the following inductive type:

Inductive T : Type -> Type :=
| c1 : forall (A : Type), A -> T A
| c2 : T unit.

但是随后命令 Check（c1（T nat））失败，并显示以下消息：术语 T nat 具有类型 Type @ {max（Set，Top.3 + 1）} ，而其类型应该为 Type @ {Top.3} （宇宙不一致）。

But then the command Check (c1 (T nat)) fails with the message: The term T nat has type Type@{max(Set, Top.3+1)} while it is expected to have type Type@{Top.3} (universe inconsistency).

如何调整上面的归纳定义，以使 c1（T nat）不会导致Universe不一致，并且不设置Universe多态性？

How can I tweak the above inductive definition so that c1 (T nat) does not cause a universe inconsistency, and without setting universe polymorphism on?

以下方法可行，但我更希望在不添加相等性的情况下进行解决：

The following works, but I would prefer a solution without adding equality:

Inductive T (A : Type) : Type :=
| c1 : A -> T A
| c2' : A = unit -> T A.

Definition c2 : T unit := c2' unit eq_refl.

Check (c1 (T nat)).
(*
c1 (T nat)
     : T nat -> T (T nat)
*)

推荐答案

首先让我回答一个问题，为什么我们首先会导致宇宙不一致。

Let me first answer the question of why we get the universe inconsistency in the first place.

宇宙不一致是Coq为避免通过罗素悖论证明 False 的证据而报告的错误，其原因是考虑了所有不

Universe inconsistencies are the errors that Coq reports to avoid proofs of False via Russell's paradox, which results from considering the set of all sets which do not contain themselves.

有一个变体在类型理论中更方便形式化，称为Hurken悖论。参见 Coq.Logic.Hurkens 了解更多信息。 Hurken的悖论有一个特殊之处，那就是证明没有任何类型可以退缩到较小的类型。也就是说，给定

There's a variant which is more convenient to formalize in type theory called Hurken's Paradox; see Coq.Logic.Hurkens for more details. There is a specialization of Hurken's paradox which proves that no type can retract to a smaller type. That is, given

U := Type@{u}
A : U
down : U -> A
up : A -> U
up_down : forall (X:U), up (down X) = X

我们可以证明 False 。

这几乎就是设置归纳类型的。用Universe注释类型，您可以从

This is almost exactly the setup of your Inductive type. Annotating your type with universes, you start with

Inductive T : Type@{i} -> Type@{j} :=
| c1 : forall (A : Type@{i}), A -> T A
| c2 : T unit.

请注意，我们可以将这种归纳求反。我们可以写

Note that we can invert this inductive; we may write

Definition c1' (A : Type@{i}) (v : T A) : A
  := match v with
     | c1 A x => x
     | c2 => tt
     end.

Lemma c1'_c1 (A : Type@{i}) : forall v, c1' A (c1 A v) = v.
Proof. reflexivity. Qed.

暂时假设 c1（T nat）类型检查。由于 T nat：Type @ {j} ，因此这需要 j< = i 。如果它给了我们 j< i ，那么我们就定了。我们可以编写 c1 Type @ {j} 。这正是我上面提到的Hurken变体的设置！我们可以定义

Suppose, for a moment, that c1 (T nat) typechecked. Since T nat : Type@{j}, this would require j <= i. If it gave us that j < i, then we would be set. We could write c1 Type@{j}. And this is exactly the setup for the variant of Hurken's that I mentioned above! We could define

u = j
U := Type@{j}
A := T Type@{j}
down : U -> A := c1 Type@{j}
up : A -> U := c1' Type@{j}
up_down := c1'_c1 Type@{j}

，因此证明 False 。

Coq需要实施避免这种悖论的规则。如此处所述，规则是每个（非参数） ）自变量构造函数的参数，如果自变量类型在Universe u 中具有某种排序，则该归纳函数的Universe被限制为> = u 。在这种情况下，这比Coq需要严格。正如SkySkimmer在此处所述，Coq可以识别直接出现在归纳为索引的位置，并以忽略参数的方式忽略它们。

Coq needs to implement a rule for avoiding this paradox. As described here, the rule is that for each (non-parameter) argument to a constructor of an inductive, if the type of the argument has a sort in universe u, then the universe of the inductive is constrained to be >= u. In this case, this is stricter than Coq needs to be. As mentioned by SkySkimmer here, Coq could recognize arguments which appear directly in locations which are indices of the inductive, and disregard those in the same way that it disregards parameters.

回答您的问题，我相信以下是您唯一的选择：

So, to finally answer your question, I believe the following are your only options:

1. 您可以设置宇宙多态性，这样在 T（T nat）中，您的两个 T 接受不同的Universe参数。 （等效地，您可以编写 Polymorphic Inductive 。）


2. 您可以利用Coq如何特别对待归纳类型的参数，从而强制执行在你的情况下使用平等。 （使用相等性的要求是从索引归纳类型到参数化归纳类型的一般属性-从将：之后的参数移动到它之前的参数。）


3. 您可以传递Coq标志 -type-in​​-type 以完全禁用Universe检查。


4. 您可以修复错误＃7929 ，这是我研究此问​​题的一部分，以使Coq处理构造函数的参数，该参数以与处理归纳类型的参数相同的方式出现在归纳的索引位置。


5. （您可以找到系统的另一种情况，并诱使Coq忽略要滑过的宇宙，并可能在此过程中找到 False 的证据。（可能涉及模块子类型化，请参见，例如， 最近在Universe模块中出现的错误。 ））

1. You can Set Universe Polymorphism so that in T (T nat), your two Ts take different universe arguments. (Equivalently, you can write Polymorphic Inductive.)
2. You can take advantage of how Coq treats parameters of inductive types specially, which mandates using equality in your case. (The requirement of using equality is a general property of going from indexed inductive types to parameterized inductives types---from moving arguments from after the : to before it.)
3. You can pass Coq the flag -type-in-type to entirely disable universe checking.
4. You can fix bug #7929, which I reported as part of digging into this question, to make Coq handle arguments of constructors which appear in index-position in the inductive in the same way it handles parameters of inductive types.
5. (You can find another edge case of the system, and manage to trick Coq into ignoring the universes you want to slip past it, and probably find a proof of False in the process. (Possibly involving module subtyping, see, e.g., this recent bug in modules with universes.))

这篇关于宇宙不一致的简单案例的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！