如何使用依赖类型在 Coq 中构建仅包含真实元素的列表？

Question

我正在从数学角度阅读 Coq 书。我试图定义一个依赖类型的函数，它返回一个包含 n 个 true 的长度列表，具体取决于我们想要的 true 数量。 Coq 抱怨事物没有正确的类型，但是当我看到它时，如果它在进行类型比较时展开我的定义，它应该可以工作，但事实并非如此。为什么？

代码：

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

  Definition t {A: Type} (n : nat) : Type :=
    match n with
    | 0 => @Vector A 0
    | S n' => @Vector A (S n')
    end.
  Check t. (* nat -> Type *)
  Check @t. (* Type -> nat -> Type *)

  (* meant to mimic Definition g : forall n: nat, t n. *)
  Fixpoint g (n : nat) : t n :=
    match n with
    | 0 => vnil
    | S n' => vcons n' true (g n')
    end.
End playing_with_types2.

Coq 的错误：

In environment
g : forall n : nat, t n
n : nat
The term "vnil" has type "Vector 0" while it is expected to have type
 "t ?n@{n1:=0}".
Not in proof mode.

即 t ?n@{n1:=0} 是 Vector 0...不是吗？

Answer 1

在这种情况下，Coq 似乎无法推断 match 表达式的返回类型，因此最好的办法是显式给出它：

Fixpoint g (n : nat) : t n :=
  match n return t n with
  | 0 => vnil
  | S n' => vcons n' true (g n')
  end.

注意添加的 return 条款。

然后出现真正的错误消息：

In environment
g : forall n : nat, t n
n : nat
n' : nat
The term "g n'" has type "t n'" while it is expected to have type "Vector n'".

这次确实是，一般来说 t n' 与 Vector n' 不同，因为 t n' 被卡住（它还不知道 n' 是 0 还是某个 S n''）。