如何证明Coq中的“ Type <> Set”（即Type不等于Set）？

Question

Type和SetCoq 之间是否存在平等或不平等关系？

我正在学习Coq的类型系统，并了解Setis Type@{Set+1}的类型和Type@{k}is 的类型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悖论，该悖论本质上说较小的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。正如您所发现的那样，无论出于什么原因，自反性本身都不能强加宇宙约束。为此，我们需要使两个引理Universe都具有多态性，以便可以使用特定的Universe级别实例化它们。

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.所有事物之前。