一个简单的宇宙不一致案例

Question

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

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}（宇宙不一致）。

我怎样才能调整上面的归纳定义，以便c1 (T nat)不会导致宇宙不一致，并且不设置宇宙多态性？

以下工作，但我更喜欢不添加平等的解决方案：

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)
*)

Answer 1

让我首先回答为什么我们会得到宇宙不一致的问题。

宇宙不一致是 Coq 报告的错误，以避免False通过罗素悖论的证明，这是由于考虑了所有不包含自身的集合的集合。

有一种在类型理论中更便于形式化的变体，称为 Hurken 悖论；Coq.Logic.Hurkens有关更多详细信息，请参阅。Hurken 悖论的一个特例证明没有任何类型可以缩回到更小的类型。也就是说，给定

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

我们可以证明False。

这几乎就是您Inductive类型的设置。用 Universe 注释你的类型，你从

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

请注意，我们可以反转这个归纳；我们可以写

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 变体的设置！我们可以定义

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 需要实现一个规则来避免这种悖论。如所描述的在这里，规则是，每个（非参数）参数来感应的一个构造中，如果参数的类型在宇宙排序u，则感应的宇宙被约束>= u。在这种情况下，这比 Coq 需要的更严格。正如 SkySkimmer在这里提到的，Coq 可以识别直接出现在作为归纳索引的位置的参数，并以与忽略参数相同的方式忽略那些参数。

因此，为了最终回答您的问题，我相信以下是您唯一的选择：

1. 你可以Set Universe Polymorphism这样，在T (T nat)，你的两个Ts 采取不同的宇宙论点。（等效地，您可以编写Polymorphic Inductive.）
2. 您可以利用 Coq 如何特别处理归纳类型的参数，这要求在您的情况下使用相等。（使用相等的要求是从索引归纳类型到参数化归纳类型的一般属性——从将参数从后面移动:到前面。）
3. 您可以通过 Coq 标志-type-in-type来完全禁用 Universe 检查。
4. 您可以修复错误 #7929，这是我在深入研究这个问题时报告的，使 Coq 处理出现在归纳中索引位置的构造函数的参数，就像它处理归纳类型的参数一样。
5. （你可以找到系统的另一个边缘情况，并设法欺骗 Coq 忽略你想要跳过它的宇宙，并且可能False在这个过程中找到一个证明。（可能涉及模块子类型，参见，例如，这个最近的错误在带有宇宙的模块中。))