如何在 Coq 中证明 "Type <> Set"（即 Type 不等于 Set）？

Question

Coq中Type和Set之间是否存在相等或不等关系？

我正在学习 Coq 的类型系统，了解到 Set 的类型是 Type@{Set+1}，Type@{k} 的类型是 Type@{k+1}。我试图证明 Type = Set，然后试图证明 Type <> Set，但我在这两种情况下都失败了。

我从

开始

Lemma set_is_type :  Type = Set.
Proof.
reflexivity.

给出一条错误消息，指出 无法将 "Set" 与 "Type@{Top.74}" 统一。

然后我试了

Lemma set_is_not_type : Type <> Set.
Proof.
intros contra.

此时我不知道如何进行。战术 discriminate 没有奏效，inversion contra.

也没有奏效

以上两个引理中哪一个可以证明？

Answer 1

这实际上不是一个完全微不足道的定理。要证明 Type = Set 导致悖论（因此有必要 Type 的单独级别），您需要使用类似于集合论中的罗素悖论的标准结果。具体来说，您需要 Hurken's paradox，这实际上表示较小的 Types 不能与较大的 Types 处于同等地位（请记住 Type 在 Coq 中是多态的，特别是，Set 是最低级别（如果包含 Prop，则为第二低级别）。

我们想要的特定定理可以在标准库中找到。

Require Logic.Hurkens.
Import Logic.Hurkens.TypeNeqSmallType.

Check paradox.

paradox 具有类型签名 forall A : Type, Type = A -> False。这几乎就是我们想要证明的，因为 Set: Type（至少如果 Type 足够大）。

Lemma set_is_not_type: Type <> Set.
Proof.
  intro F.
  exact (paradox _ F).
Defined.

Coq 自动对这个引理中的 Type 设置限制，以确保 Set: Type.

另一方面，Set等于一些层的Type，所以我们应该可以证明Type = Set对此 Type 有一些不同的限制。我发现最简单的方法是证明 Type = Type，然后用 Set 实例化这个定理。无论出于何种原因，正如您发现的那样，反身性本身无法强制执行宇宙约束。为此，我们需要使引理宇宙成为多态的，以便它们可以用特定的宇宙级别实例化。

Polymorphic Lemma type_is_type: Type = Type.
Proof.
  reflexivity.
Defined.

Polymorphic Lemma type_is_set: Type = Set.
Proof.
  apply type_is_type.
Defined.

让宇宙中的一切都具有多态性的更简单方法是将 Set Universe Polymorphism. 放在一切之前。

如何在 Coq 中证明 "Type <> Set"（即 Type 不等于 Set）？

How to prove that "Type <> Set" (i.e. Type is not equal to Set) in Coq?

coq

dependent-type

theorem-proving

type-theory