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

Question

Я хотел бы создать зависимую функцию, но я сталкиваюсь с ошибкой несоответствия типов на 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?)

Answer 1

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

Да. 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 бизнес), вам нужно будет использовать зависимое сопоставление с образцом. Другая возможность - использовать режим проверки для определения вашей функции.