Lean向量

Lean向量是Lean定理证明器中用于表示动态数组的数据结构，结合了函数式编程的不可变特性与高效随机访问能力。本文将从基础概念到高级应用全面解析Lean向量的实现原理、操作方法及实际用例。

基本概念

在Lean中，Vector α n表示一个长度为n且元素类型为α的固定长度数组，其核心特性包括：

• 类型安全：长度信息编码在类型系统中（依赖类型）
• 不可变性：所有操作返回新实例而非修改原数据
• 严格索引检查：编译时/运行时防止越界访问

数学上可表示为： $\text{Vector}:\text{Type}\to \mathbb{\mathbb{N}}\to \text{Type}$

核心操作

构造向量

-- 空向量
#check Vector.nil : Vector Nat 0

-- 通过cons构建
def v1 : Vector Nat 3 := Vector.cons 1 (Vector.cons 2 (Vector.cons 3 Vector.nil))

-- 字面量语法（需打开语法扩展）
open Vector
def v2 : Vector Nat 3 := [1, 2, 3]

基本操作示例

常用方法对照表

操作	类型签名	示例
获取长度	Vector.length : Vector α n → Nat	v1.length → 3
索引访问	Vector.get : Fin n → Vector α n → α	v1.get 1 → 2
映射	Vector.map : (α → β) → Vector α n → Vector β n	v1.map (·+1) → [2,3,4]

高级操作

-- 向量拼接（需长度匹配）
def concat_example (v1 : Vector Nat 2) (v2 : Vector Nat 3) : Vector Nat 5 :=
  v1 ++ v2  -- 类型系统验证长度和

-- 矩阵转置（展示嵌套向量）
def matrix : Vector (Vector Nat 3) 2 :=
  [[1, 2, 3], [4, 5, 6]]

def transpose : Vector (Vector Nat 2) 3 :=
  ⟨List.ofFn fun i => ⟨List.ofFn fun j => matrix.get j |>.get i⟩⟩

实现原理

Lean向量基于以下关键设计：

graph TD A[Vector α n] --> B[结构体] B --> C[数据存储: List α] B --> D[长度证明: length list = n]

类型安全性通过依赖类型保证： $\text{get}:(i:\text{Fin }n)\to \text{Vector }\alpha n\to \alpha$

实际应用案例

案例1：矩阵运算

-- 点积计算
def dotProduct (v1 v2 : Vector Float n) : Float :=
  (v1.zipWith v2 (· * ·)).foldl (· + ·) 0

#eval dotProduct [1.0, 2.0] [3.0, 4.0]  -- 输出: 11.0

案例2：类型安全队列

structure SafeQueue (α : Type) (max : Nat) where
  current : Vector α n
  size : n ≤ max

def enqueue [DecidableEq α] (item : α) (q : SafeQueue α max) : Option (SafeQueue α max) :=
  if q.size < max then
    some { q with current := q.current.concat item, size := q.size + 1 }
  else none

性能特性

时间复杂度分析

操作	时间复杂度	备注
索引访问	O(1)	底层数组存储
追加	O(n)	需复制整个向量
映射	O(n)	惰性求值优化

与List对比

• 长度处理：Vector在类型中编码长度，List需运行时检查
• 内存布局：Vector连续存储，List链式存储
• 模式匹配：List支持更简洁的匹配语法

-- List匹配示例
def listSum : List Nat → Nat
  | [] => 0
  | x :: xs => x + listSum xs

-- Vector匹配需要处理长度约束
def vectorSum : Vector Nat n → Nat
  | ⟨[], _⟩ => 0
  | ⟨x :: xs, _⟩ => x + vectorSum ⟨xs, by simp⟩

进阶主题

依赖类型编程

利用长度信息实现编译时验证：

def replicate (α : Type) (n : Nat) (x : α) : Vector α n :=
  ⟨List.replicate n x, by simp⟩

-- 类型系统保证长度正确
#check replicate Nat 5 0  -- Vector Nat 5

与数组的互操作

-- 从原生数组转换（需长度验证）
def fromArray (arr : Array α) (h : arr.size = n) : Vector α n :=
  ⟨arr.toList, h⟩

最佳实践

1. 优先使用Vector处理固定长度集合 2. 对于频繁修改的场景考虑使用Array 3. 利用类型系统捕获长度相关错误 4. 复杂操作可结合Fin n类型使用

参见

• 依赖类型
• Lean中的列表处理
• 定理证明中的数据结构