Coq：固定的宇宙层次结构w /明确的宇宙

我正在研究使用explicit universes在Coq中构建固定的Universe层次结构的可能性。使用常数的尝试（2，3，4）构建失败：在最后，所有的组合仍然类型检查（即所有申报的宇宙被视为层次任意）：Coq：固定的宇宙层次结构w /明确的宇宙

Universe k l m x y z. 
Let x := 2. 
Definition k := [email protected]{x}. 
Notation y := 3. 
Definition l := [email protected]{y}. 
Notation z := 4. 
Definition m := [email protected]{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 := [email protected]{2}和Definition k := [email protected]{x+1}结果在语法错误。是否有可能使用明确的宇宙来建立一个固定的层次结构，如果是的话，如何呢？

来源

2017-01-16 jaam

人们可以使用Constraint命令：

Universes x y z. 

Constraint x < y, y < z. 

Definition X := [email protected]{x}. 
Definition Y := [email protected]{y}. 
Definition Z := [email protected]{z}. 

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

注意，这种方法并不能真正解决宇宙水平以及。

来源

2017-01-18 16:51:30

很明显，这是它意味着要完成的方式。我怀疑这是不可能的，以解决声明的宇宙变量的水平 – jaam

我认为你是对的。我没有看过源代码，但从我读过的论文中可以看出，没有明确的宇宙级数字，只有抽象变量之间的约束。但我可能是错的。如果你想确定要问的最好的地方是Coq俱乐部邮件列表。 –

我已经得到了它的工作方式如下：？

Universe X Y Z. 
Definition x := [email protected]{X}. 
Definition y := [email protected]{Y}. 
Definition z := [email protected]{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 "[email protected]{Z+1}" while it is expected to have type "y" 
    (universe inconsistency: Cannot enforce Z < Y because Y < Z). 
*)

（但也许有人更了解比我会附和更好的想法特别是，这种做法不允许申报。固定常数，所以仍可能在声明的水平之间任意多层次）

来源

2017-01-17 18:09:49 nobody

您可以规定一个固定的宇宙层次瓦特/一个公理：

Universe X Y Z. 
Notation X := [email protected]{X}. 
Notation Y := [email protected]{Y}. 
Definition Z := [email protected]{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.

特定由人造成的问题仍然是一个悬而未决的挑战

来源

2017-01-17 20:48:46 jaam

Coq：固定的宇宙层次结构w /明确的宇宙

回答

相关问题