Используйте False_rec для создания псевдонима типа списка в Coq - PullRequest
Новая
       7

Используйте False_rec для создания псевдонима типа списка в Coq

0 голосов
/ 24 августа 2018

Я хотел бы создать зависимую функцию, но я сталкиваюсь с ошибкой несоответствия типов в термине False_rec. Я пытаюсь сделать что-то похожее на следующее: 

Definition env A := list A.

Fixpoint zip (xs ys : env nat) (H : length xs = length ys) : env (nat * nat).
Proof.
  refine
  (match xs, ys with
  | [], [] => []
  | x :: xs, y :: ys =>
      (x, y) :: zip xs ys _
  | _, _ => False_rec _ _
  end).
...

Однако я получаю следующую ошибку: 

The term "False_rec ?P ?f" has type "?P" while it is expected to have type 
"env (nat * nat)" (unable to find a well-typed instantiation for 
"?P": cannot ensure that "Type" is a subtype of "Set").

Стандартный список, когда ему дается набор, становится самим набором, но, похоже, он этого не делает, когда создается псевдоним таким образом. Например: 

Check (list nat). (* list nat : Set *)
Check (env nat). (* env nat : Type *)

Есть ли причина этого несоответствия? И есть ли способ обойти это? (Например, могу ли я убедить Coq, что (env nat) - это Set? Или я могу использовать более общую функцию False_rec, которая работает на Type вместо Set?)

1 Ответ

0 голосов
/ 24 августа 2018

Есть ли причина этого несоответствия?

Да. Type - это сущность, которая может содержать (большие) вещи, которые не вписываются в Set. Например. nat вписывается в Set, но Set не вписывается в себя. Я думаю, что на SO должно быть более одного превосходного ответа, объясняющего эту проблему.

(Например, могу ли я убедить Coq, что (env nat) является Set?

Вы можете использовать явные аннотации типов: 

Definition env (A : Set) : Set := list A.

Или я могу использовать более общую функцию False_rec, которая работает на Type вместо Set?

Да, вы можете. Это называется False_rect.

Обратите внимание, что простое выражение match не будет работать в вашем случае (независимо от бизнеса Set / Type), вам нужно будет использовать зависимое сопоставление с образцом. Другая возможность - использовать режим проверки для определения вашей функции.

...