Почему моя сортировка записей типа отображается как сортировка по множеству? - PullRequest
Новая
       10

Почему моя сортировка записей типа отображается как сортировка по множеству?

1 голос
/ 24 апреля 2019

Когда я использую макрос Record для создания типа записи, он отображается как сортировка Set вместо сортировки Type.

Я создал минимальный тестовый пример, демонстрирующий то же поведение: 

Record little_test : Type :=
  {
    bit1 : nat;
    bit2 : nat;
  }.

Check little_test.

little_test
     : Set

1 Ответ

4 голосов
/ 25 апреля 2019

Set - это просто самый низкий уровень в бесконечной иерархии Type. Поскольку вселенные Coq являются кумулятивными, это означает, что little_test также обитает на каждом более высоком уровне. Обычно вы не хотите ограничивать ваши типы только на более высоких уровнях, поэтому Coq просто минимизирует уровень вселенной. Если вы действительно хотите, чтобы little_test был на более высоком уровне, вы можете явно попросить об этом.

Если вы используете CoqIDE, установите «Показать уровни юниверса» в меню «Вид» вместо Set Printing Universes.. Другие IDE (Proof General и т. Д.) Также могут по-своему отображать уровни вселенной. 

Set Printing Universes.

Record little_test@{i} : Type@{i} :=
  {
    bit1 : nat;
    bit2 : nat;
  }.

Check little_test.

Этот подход объявляет фиксированный уровень вселенной (little_set.i) и заставляет little_set обитать Type@{little_test.i}. Если у вас уже есть уровень вселенной откуда-то еще, вы можете не указывать уровень вселенной. 

Set Printing Universes.

Record little_test1@{i} : Type@{i} :=
  {
    bit1 : nat;
    bit2 : nat;
  }.

Record little_test2 : Type@{little_test1.i} :=
  {
    bit3 : nat;
    bit4 : nat;
  }.

Check little_test1.
Check little_test2.

В этом подходе little_test1 и little_test2 имеют одинаковый минимальный уровень (но помните, что совокупная вселенная означает, что они оба обитают на каждом более высоком уровне).

Этот последний подход объявляет бесконечное число little_test с - по одному для каждого уровня вселенной. 

Set Printing Universes.
Unset Universe Minimization ToSet.

Polymorphic Record little_test@{i} : Type@{i} :=
  {
    bit1 : nat;
    bit2 : nat;
  }.

Check little_test.

Однако по умолчанию Coq минимизирует уровень юниверса, когда вы используете little_test без параметра юниверса (до Set, если нет ограничений), поэтому нам нужно Unset Universe Minimization ToSet, чтобы изменить это поведение. Если вы хотите, чтобы все ваши типы Record и Inductive были полиморфными, вы можете Set Universe Polymorphism. Обратите внимание, что вы все равно должны использовать @{i} (или другое имя для уровня юниверса), чтобы указать, где находится полиморфизм.

...