Coq列表转向量实现遇空向量错误，求解决方法

你的代码报错核心原因是空列表分支的nil缺少明确的类型与长度标注，Coq无法自动推断它对应Vector.t X 0，而length List.nil的结果是0，两者类型不匹配触发错误。同时cons的调用可以简化，无需手动传递冗余参数。

修正后的代码如下：

Require Import Vector List.

Fixpoint list_to_vec {X : Type} (l : list X) : Vector.t X (length l) :=
  match l with
  | List.nil => Vector.nil X
  | List.cons h t => Vector.cons h (list_to_vec t)
  end.

关键修正点说明： #

• 空列表分支：明确使用Vector.nil X，指定其类型为X，对应长度自动推导为0，完美匹配length List.nil的结果。
• 非空列表分支：直接用Vector.cons h (list_to_vec t)，Coq会自动推导list_to_vec t的类型是Vector.t X (length t)，而Vector.cons会将长度升级为S (length t)，恰好等于length (List.cons h t)，满足依赖类型的匹配要求。

测试示例 #

可以用以下代码验证转换正确性：

Example test_list_to_vec : list_to_vec (1::2::3::nil) = Vector.cons 1 (Vector.cons 2 (Vector.cons 3 (Vector.nil nat))).
Proof. reflexivity. Qed.

内容的提问来源于stack exchange，提问作者Helen