Lean数组

Lean数组是Lean定理证明器中用于存储同类型元素的高效数据结构，它结合了函数式编程的不可变特性与底层内存连续存储的优势。本文将从基础定义到高级应用全面解析Lean数组的设计原理、操作方法及性能特征。

基本概念[编辑 | 编辑源代码]

在Lean中，数组（`Array`）是固定大小或动态调整的序列容器，提供O(1)随机访问能力。与列表（`List`）不同，数组在内存中连续存储元素，其类型定义为：

structure Array (α : Type u) where
  data : List α
  size : Nat

关键特征：

类型安全：所有元素必须为同一类型 $α$
长度可变：通过`push`/`pop`操作动态调整
不可变设计：修改操作返回新数组而非改变原对象

核心操作[编辑 | 编辑源代码]

创建数组[编辑 | 编辑源代码]

-- 空数组
#check Array.empty : Array Nat

-- 字面量构造
def primes := #[2, 3, 5, 7]  -- 类型推断为 Array Nat

-- 通过函数生成
def squares := Array.mk (List.range 10 |>.map (· ^ 2))

元素访问[编辑 | 编辑源代码]

使用`get`函数（索引从0开始）：

#eval primes.get! 1  -- 输出: 3
#eval primes[2]!     -- 语法糖，输出: 5

修改操作[编辑 | 编辑源代码]

由于不可变性，"修改"实际创建新数组：

def updated := primes.set 0 11  -- 首元素改为11
#eval updated  -- 输出: #[11, 3, 5, 7]

常用方法[编辑 | 编辑源代码]

方法	描述	示例
`push`	末尾添加元素	`#[1,2].push 3` → `#[1,2,3]`
`pop`	移除末尾元素	`#[1,2,3].pop` → `#[1,2]`
`++`	数组合并	`#[1,2] ++ #[3]` → `#[1,2,3]`
`map`	元素转换	`#[1,2].map (·+1)` → `#[2,3]`

内存模型[编辑 | 编辑源代码]

性能特征对比：

访问：O(1)（优于List的O(n)）
追加：平均O(1)（动态扩容）
中间插入：O(n)（需移动后续元素）

高级技巧[编辑 | 编辑源代码]

切片操作[编辑 | 编辑源代码]

使用`extract`获取子数组：

def nums := #[0,1,2,3,4,5]
#eval nums.extract 2 5  -- 输出: #[2,3,4]

并行处理[编辑 | 编辑源代码]

利用`mapTask`进行并行计算：

import Task
def heavyCompute (x : Nat) := x * x

def input := Array.range 1000
def output ← input.mapTask heavyCompute  -- 并行映射

实际案例[编辑 | 编辑源代码]

矩阵转置实现：

def transpose (mat : Array (Array α)) : Array (Array α) :=
  if mat.isEmpty then #[]
  else 
    let n := mat[0]!.size
    Array.mk <| List.range n |>.map fun j =>
      Array.mk <| mat.toList.map (·[j]!)

示例输入/输出：

#eval transpose #[#[1,2], #[3,4], #[5,6]] 
-- 输出: #[#[1, 3, 5], #[2, 4, 6]]

数学表示[编辑 | 编辑源代码]

数组可形式化为： $Array α = {f : ℕ ⇀ α ∣ \exists n \in ℕ, dom (f) = {0, \dots, n - 1}}$

最佳实践[编辑 | 编辑源代码]

1. 优先使用数组而非列表当需要频繁随机访问 2. 批量操作时使用`modifyM`避免临时对象创建 3. 大型数组考虑使用`IO.Array`进行内存映射

页面模块:Message box/ambox.css没有内容。

通过本文的学习，读者应能掌握Lean数组的核心操作方法与适用场景，在定理证明和算法实现中高效运用这一数据结构。