使用 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").

标准列表在被赋予 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-expression 在您的情况下不起作用(无论Set/Type业务如何(，您将需要使用依赖模式匹配。另一种可能性是使用证明模式来定义函数。