Coq：带有显式宇宙的固定宇宙层次结构

Question

我正在研究使用 explicit universes 在 Coq 中构建 固定宇宙层次结构 的可能性。在构建它时使用常量 (2, 3, 4) 的尝试失败了：最后，所有组合仍然进行类型检查（即所有声明的宇宙都被视为分层任意）：

Universe k l m x y z.
Let x := 2.
Definition k := Type@{x}.
Notation y := 3.
Definition l := Type@{y}.
Notation z := 4.
Definition m := Type@{z}.
Print x. (*x = 2: nat*)
Print y. (*Notation y := 3*)
Check l:k:m.
Check m:k:l.
Check k:m:l.

请注意，Definition k := Type@{2} 和 Definition k := Type@{x+1} 会导致语法错误。是否可以使用显式 Universe 来构建固定层次结构？如果可以，如何构建？

Answer 1

我使用它的方式如下：

Universe X Y Z.
Definition x := Type@{X}.
Definition y := Type@{Y}.
Definition z := Type@{Z}.

(* bogus definition to fix hierarchy *)
Definition dummy:x:y:z := unit.

Check x:y.
(* ok:
   x : y
        : y
*)

Check x:z.
(* also ok (transitivity is still acceptable):
   x : z
        : z
*)

Check z:y.
(* Error:
   The term "z" has type "Type@{Z+1}" while it is expected to have type "y"
   (universe inconsistency: Cannot enforce Z < Y because Y < Z).
*)

（但也许比我更有见识的人会提出更好的想法？特别是，这种方法不允许声明固定常量，因此在声明的级别之间可能仍然存在任意多个级别。）

Answer 2

您可以使用公理规定固定的宇宙层次结构：

Universe X Y Z.
Notation X := Type@{X}.
Notation Y := Type@{Y}.
Definition Z := Type@{Z}.
Axiom fuh: (fun (x:Type) => x)(X:Y:Z).
Check X:Y.
Check Y:Z.
Check X:Z.
Fail Check Z:Y.
Fail Check Y:X.
Fail Check Z:X.

没有人提出的特定问题仍然是一个开放的挑战

Answer 3

可以使用Constraint命令：

Universes x y z.

Constraint x < y, y < z.

Definition X := Type@{x}.
Definition Y := Type@{y}.
Definition Z := Type@{z}.

Check X:Y.
Check Y:Z.
Check X:Z.
Fail Check Z:Y.
Fail Check Y:X.
Fail Check Z:X.

请注意，这种方法并没有真正修复宇宙水平。

Coq：带有显式宇宙的固定宇宙层次结构

Coq: fixed universe hierarchy w/ explicit universes

types

coq