Coq: фиксированная иерархия юниверсов с явными юниверсами

Я изучаю возможность использования explicit universes для построения фиксированной иерархии юниверсов в Coq. Попытка использовать константы (2, 3, 4) в строительстве он не удалось: в конце концов, все комбинации еще typecheck (т.е. все объявленные вселенные рассматриваются как иерархически произвольно):Coq: фиксированная иерархия юниверсов с явными юниверсами

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 Club. –

Путь Я получил его на работу следующим образом:

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 "Ty[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: фиксированная иерархия юниверсов с явными юниверсами

ответ

Смежные вопросы