Почему мой способ определения Принуждения в этом примере неверен, и каков правильный путь? - PullRequest
Новая
       22

Почему мой способ определения Принуждения в этом примере неверен, и каков правильный путь?

3 голосов
/ 27 апреля 2020

Мой код Coq выглядит следующим образом: 

    Inductive A (X: Type) :=
      n1 : nat -> X -> (A X)
    .

    Arguments n1 {X} _ _. 

    Inductive B :=
      m1 : (A nat) -> B |
      m2 : B -> B -> B
    .

    Coercion m1 : A >-> B.

    Check m2 (m1 (n1 1 2)) (m1 (n1 2 2)). (* 1st Check *)
    Check m2 (n1 1 2) (n1 2 2). (* 2nd Check *)

Я определил типы A и B (A является полиморфным типом c). При записи выражения B, связанного оператором «m2» (например, «1-я проверка»), я буду sh опускать конструктор «m1» (например, «2-я проверка»), поэтому я определил приведение, как указано выше. , Однако работает только первая проверка, вторая проверка не работает.

Как правильно использовать принуждение здесь? И почему мое определение неверно?

1 Ответ

2 голосов
/ 27 апреля 2020

Я не думаю, что есть какой-то удобный способ получить то, что вы хотите, с текущим механизмом принуждения. Когда вы вводите m1 как принуждение, Coq говорит, что оно не соблюдает условие равномерного наследования. Это происходит, когда вы объявляете принуждение между семействами типов, которое фиксирует некоторые параметры; здесь вы исправили X, чтобы быть nat. Когда это условие нарушается, средство проверки типов Coq отказывается применять принуждение.

Одним частичным решением является введение промежуточного типа: 

Inductive A (X: Type) :=
      n1 : nat -> X -> (A X)
    .

    Arguments n1 {X} _ _.

Definition Anat := A nat.
Identity Coercion Anat_of_A : Anat >-> A.

Inductive B :=
  m1 : Anat -> B |
  m2 : B -> B -> B
.

Coercion m1 : Anat >-> B.

Check m2 (m1 (n1 1 2)) (m1 (n1 2 2)). (* 1st Check *)
Check m2 (n1 1 2 : Anat) (n1 2 2 : Anat). (* 2nd Check *)

Проблема в том, что n1 все еще что-то производит типа A в конце вместо Anat. Следовательно, вам нужно явное приведение, чтобы убедить Coq вызвать принуждение. Конечно, вы также можете определить версию n1, которая специализируется на X, но это не позволит сделать A polymorphi c.

...