如何在 Coq 中定义具有命名参数的依赖类型而不导致构造函数中出现统一问题？

Question

我想定义一个长列表，但我喜欢在归纳定义顶部带有名称的参数。每当我尝试这样做时，我都会遇到我希望起作用的东西的统一错误，并且被迫做一个显然有错误的定义，例如允许一个列表，其中所有内容的长度都是 0 但有 1 个元素。我该如何解决这个问题？

  Inductive Vector {A : Type} (n : nat) : Type :=
    | vnil (* not quite right...*)
    | vcons (hd : A) (tail: Vector (n-1)).
  Check vnil 0.
  Check vcons 1 true (vnil 0).

  (* Inductive Vector' (n : nat) : Type :=
  | vnil': Vector' 0
  | vcons': A -> Vector' n -> Vector' (S n). *)

  Inductive Vector' {A: Type} : nat -> Type :=
  | vnil': Vector' 0
  | vcons': forall n : nat, A -> Vector' n -> Vector' (S n).
  Check vnil'.
  Check vcons' 0 true (vnil').

  Inductive Vector'' {A : Type} (n : nat) : Type :=
  | vnil'': Vector'' n (* seems weird, wants to unify with n, argh! *)
  | vcons'': A -> Vector'' (n-1) -> Vector'' n.
  Check vnil'' 0.
  Check vcons'' 1 true (vnil'' 0).
  (* Check vcons'' 0 true (vnil'' 0). *) (* it also worked! nooooo! hope the -1 did the trick but not *)

Answer 1

: 左侧的命名参数（它们称为参数）在每个构造函数中隐式 forall'，并且必须在每个构造函数的返回类型中显示为相同的变量。右侧的参数（它们称为索引）不是隐式地 forall 的，并且可以显示为任何内容。您的定义的部分问题在于，在编写每个构造函数的类型时已经引入了 n ，因此您不能完全将其限制为 Z 或 S m 此时。

这个想法是参数应该是整个归纳定义的参数。 向量 A n 和 向量 B m 彼此不依赖；将Vector A和Vector B视为不同的归纳定义，并将Vector视为由参数化的归纳系列是有意义的>输入。另一方面，Vector A (S n) 指Vector A n；如果不首先构造 Vector A n，则无法构造类型 Vector A (S n)，因此它们应被视为归纳构造 Vector A : nat - 的一部分>输入。

这种解释并没有严格执行——你可以用 Intropic E (n : nat) : Set := | 在其中戳一个洞。 mk_E：E(Sn)→ E n.-但是关于构造函数返回类型中的参数与索引的规则是强制执行的。 Coq 的设计意图是定义 Vector 的“最自然”方式是

(* making A an implicit argument to Vector seems a bad idea... *)
Inductive Vector (A : Type) : nat -> Type :=
| vnil  : Vector A O
| vcons : forall n, A -> Vector A n -> Vector A (S n).
(* if you want to clean up vnil and vcons afterwards you can issue something like *)
Arguments vnil {A}.
Arguments vcons {A n}.
(* it would also work to define Vector with A implicit and then just use Arguments on Vector to make A explicit (it would leave n explicit in vcons), but that's just weird *)

如果你想澄清 nat 是什么 评论

(* A [Vector A n] is a list of [n] elements of type [A]. *)

这样做，您可以留下类似或的

Inductive Vector (A : Type) : (* n *) nat -> Type :=

如果您真的想要Inducing Vector (A : Type) (n : nat) : Type，那么您必须诉诸某些东西就像

Inductive Vector (A : Type) (n : nat) : Type :=
| vnil  (prf : n = O)
| vcons (m : nat) (prf : n = S m) (x : A) (xs : Vector A m).

这让一切变得混乱。