如何在Lean 4中将带长度编码的多态Vector定义为List的Subtype

你之前的核心认知偏差是没有将长度参数n纳入子类型谓词的依赖范围：Subtype的谓词不需要是全局固定的恒真/恒假判断，完全可以依赖外部传入的参数，针对特定长度筛选符合要求的列表。

类型定义 #

Vector a n的定义非常简洁，直接用Subtype语法糖即可：

def Vector (a : Type) (n : Nat) : Type := { l : List a // l.length = n }

这个定义里，Vector a n的每个值本质是一个依赖对：

• 存储的底层数据是普通的List a，可以通过.val字段直接访问
• 附带一个证明项，通过.property字段访问，证明这个底层列表的长度恰好等于类型中标注的n

这种实现方式可以直接复用List的所有内置方法，不需要重复造轮子。比如你提到的concat函数，几行代码就能实现，且类型签名会自动校验长度正确性：

def concat {a : Type} {m n : Nat} (u : Vector a m) (v : Vector a n) : Vector a (m + n) :=
  ⟨u.val ++ v.val, by
    simp [List.length_append, u.property, v.property]
    <;> rfl⟩

这里直接复用List的++运算实现拼接，只需要用简单的策略证明两个列表拼接后的长度为m + n即可，类型系统会强制保证返回值的长度符合签名约定，不会出现长度不匹配的问题。

从List构造Vector实例 #

Subtype值的标准构造格式是⟨底层值, 谓词成立的证明⟩，针对Vector场景有两种常用构造方式：

• 当列表长度和目标n定义上相等（比如字面量列表、编译期可确定长度的场景），直接用rfl即可完成证明：

-- 构造存储Nat类型、长度为3的向量
def exampleVec : Vector Nat 3 := ⟨[10, 20, 30], by rfl⟩

rfl会直接对列表长度做规约计算，确认[10,20,30].length = 3成立，不需要手动写复杂证明。

• 当列表长度是动态计算得到时，可以先做长度判断，再返回构造结果，比如实现一个安全的构造函数：

def Vector.fromList {a : Type} (l : List a) (targetLen : Nat) : Option (Vector a targetLen) :=
  if h : l.length = targetLen then
    some ⟨l, h⟩
  else
    none

调用这个函数时，只有传入的列表长度和目标长度一致时才会返回合法的Vector，否则返回none，从根源避免长度不匹配的错误：

#eval Vector.fromList [1,2,3] 3 -- 返回some包裹的合法Vector
#eval Vector.fromList [1,2] 3 -- 返回none

日常使用时，大部分关于List长度的证明义务都可以交给simp、aesop等内置自动证明策略完成，你只需要聚焦在业务逻辑上，直接通过.val调用List的map、fold、join等已有方法即可，不需要为Vector重新实现底层逻辑。

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