coq - 宇宙不一致的一个简单例子

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) 不会导致 universe 不一致，并且无需设置 universe 多态性？

以下可行，但我更喜欢不添加相等性的解决方案:

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

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

Universe 不一致是 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 需要实现一个规则来避免这个悖论。如所述here ，规则是对于归纳构造函数的每个(非参数)参数，如果参数的类型在宇宙中有一个排序 u , 那么归纳的宇宙被约束为 >= u .在这种情况下，这比 Coq 需要的更严格。正如 SkySkimmer 所述 here ，Coq 可以识别直接出现在归纳索引位置的参数，并以与忽略参数相同的方式忽略这些参数。

---

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

1. 你可以Set Universe Polymorphism所以在T (T nat) ，你的两个T我们采用不同的宇宙参数。 (等价地，你可以写成 Polymorphic Inductive 。)
2. 您可以利用 Coq 特殊对待归纳类型参数的方式，这要求在您的情况下使用相等性。 (使用相等性的要求是从索引归纳类型到参数化归纳类型的一般属性——从将参数从 : 之后移动到它之前。)
3. 你可以将标志传递给 Coq -type-in-type完全禁用 Universe 检查。
4. 你可以fix bug #7929 ，作为深入研究这个问题的一部分，我报告了这一点，使 Coq 处理出现在归纳中索引位置的构造函数的参数，其处理方式与处理归纳类型的参数的方式相同。
5. (您可以找到系统的另一个边缘情况，并设法诱使 Coq 忽略您想要跳过它的宇宙，并可能在此过程中找到 False 的证明。(可能涉及模块子类型化，请参阅, 例如 this recent bug in modules with universes .))