编辑“︁Lean向量”︁

{{DISPLAYTITLE:Lean向量}}

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

== 基本概念 ==
在Lean中，'''Vector α n'''表示一个长度为''n''且元素类型为''α''的固定长度数组，其核心特性包括：
* 类型安全：长度信息编码在类型系统中（依赖类型）
* 不可变性：所有操作返回新实例而非修改原数据
* 严格索引检查：编译时/运行时防止越界访问

数学上可表示为：
<math>
\text{Vector} : \text{Type} \rightarrow \mathbb{N} \rightarrow \text{Type}
</math>

== 核心操作 ==
=== 构造向量 ===
<syntaxhighlight lang="lean">
-- 空向量
#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]
</syntaxhighlight>

=== 基本操作示例 ===
{| class="wikitable"
|+ 常用方法对照表
! 操作 !! 类型签名 !! 示例
|-
| 获取长度 || <code>Vector.length : Vector α n → Nat</code> || <code>v1.length → 3</code>
|-
| 索引访问 || <code>Vector.get : Fin n → Vector α n → α</code> || <code>v1.get 1 → 2</code>
|-
| 映射 || <code>Vector.map : (α → β) → Vector α n → Vector β n</code> || <code>v1.map (·+1) → [2,3,4]</code>
|}

=== 高级操作 ===
<syntaxhighlight lang="lean">
-- 向量拼接（需长度匹配）
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⟩⟩
</syntaxhighlight>

== 实现原理 ==
Lean向量基于以下关键设计：

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

类型安全性通过依赖类型保证：
<math>
\text{get} : (i : \text{Fin } n) \rightarrow \text{Vector } \alpha \ n \rightarrow \alpha
</math>

== 实际应用案例 ==
=== 案例1：矩阵运算 ===
<syntaxhighlight lang="lean">
-- 点积计算
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
</syntaxhighlight>

=== 案例2：类型安全队列 ===
<syntaxhighlight lang="lean">
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
</syntaxhighlight>

== 性能特性 ==
{| class="wikitable"
|+ 时间复杂度分析
! 操作 !! 时间复杂度 !! 备注
|-
| 索引访问 || O(1) || 底层数组存储
|-
| 追加 || O(n) || 需复制整个向量
|-
| 映射 || O(n) || 惰性求值优化
|}

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

<syntaxhighlight lang="lean">
-- 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⟩
</syntaxhighlight>

== 进阶主题 ==
=== 依赖类型编程 ===
利用长度信息实现编译时验证：
<syntaxhighlight lang="lean">
def replicate (α : Type) (n : Nat) (x : α) : Vector α n :=
  ⟨List.replicate n x, by simp⟩

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

=== 与数组的互操作 ===
<syntaxhighlight lang="lean">
-- 从原生数组转换（需长度验证）
def fromArray (arr : Array α) (h : arr.size = n) : Vector α n :=
  ⟨arr.toList, h⟩
</syntaxhighlight>

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

{{警告|注意：向量拼接操作<code>v1 ++ v2</code>要求编译时已知长度关系}}

== 参见 ==
* [[依赖类型]]
* [[Lean中的列表处理]]
* [[定理证明中的数据结构]]

[[Category:Lean编程]]
[[Category:函数式数据结构]]

[[Category:计算机科学]]
[[Category:Lean]]
[[Category:Lean数据结构]]