Lean列表

简介[编辑 | 编辑源代码]

Lean列表是Lean定理证明器中最基础的数据结构之一，用于存储有序的元素序列。列表在函数式编程中扮演核心角色，其不可变特性与递归处理方式使其成为构建复杂算法的理想工具。在Lean中，列表通过归纳类型定义，支持模式匹配和递归操作，是学习更高级数据结构前必须掌握的概念。

定义与语法[编辑 | 编辑源代码]

Lean标准库（`List`命名空间）中列表的归纳定义如下：

inductive List (α : Type u) where
  | nil : List α
  | cons (head : α) (tail : List α) : List α

`nil`表示空列表
`cons`用于在列表头部添加元素（构造非空列表）

语法糖[编辑 | 编辑源代码]

Lean提供简写形式：

`[]`等价于`nil`
`a :: l`等价于`cons a l`
`[a, b, c]`等价于`a :: b :: c :: []`

基本操作[编辑 | 编辑源代码]

构造列表[编辑 | 编辑源代码]

-- 空列表
def emptyList : List Nat := []

-- 含三个元素的列表
def numbers : List Nat := [1, 2, 3]

-- 使用cons构造
def colors : List String := "red" :: "green" :: "blue" :: []

长度计算[编辑 | 编辑源代码]

递归计算列表长度的典型实现：

def length {α : Type} : List α → Nat
  | [] => 0
  | _ :: tail => 1 + length tail

#eval length [true, false]  -- 输出: 2

连接操作[编辑 | 编辑源代码]

使用`++`运算符或递归实现：

def concat {α : Type} : List α → List α → List α
  | [], l => l
  | h :: t, l => h :: concat t l

#eval [1, 2] ++ [3, 4]  -- 输出: [1, 2, 3, 4]

高级操作[编辑 | 编辑源代码]

映射（Map）[编辑 | 编辑源代码]

使用`List.map`对每个元素应用函数：

#eval List.map (fun x => x * 2) [1, 2, 3]  -- 输出: [2, 4, 6]

过滤（Filter）[编辑 | 编辑源代码]

使用谓词筛选元素：

#eval List.filter (fun x => x % 2 == 0) [1, 2, 3, 4]  -- 输出: [2, 4]

折叠（Fold）[编辑 | 编辑源代码]

左右折叠实现：

def foldl {α β} (f : α → β → α) (init : α) : List β → α
  | [] => init
  | h :: t => foldl f (f init h) t

#eval foldl (fun acc x => acc + x) 0 [1, 2, 3]  -- 输出: 6

内存结构[编辑 | 编辑源代码]

数学性质[编辑 | 编辑源代码]

列表操作满足以下代数定律：

连接结合律： $(l_{1} + + l_{2}) + + l_{3} = l_{1} + + (l_{2} + + l_{3})$
单位元： $[] + + l = l + + [] = l$
映射复合： $m a p f \circ m a p g = m a p (f \circ g)$

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

矩阵转置[编辑 | 编辑源代码]

使用列表实现矩阵操作：

def transpose {α : Type} : List (List α) → List (List α)
  | [] => []
  | [] :: _ => []
  | rows => List.map List.head! rows :: transpose (List.map List.tail! rows)

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

快速排序[编辑 | 编辑源代码]

经典算法实现：

def qsort : List Nat → List Nat
  | [] => []
  | h :: t =>
    let lesser := t.filter (· ≤ h)
    let greater := t.filter (· > h)
    qsort lesser ++ [h] ++ qsort greater

#eval qsort [3, 1, 4, 1, 5]  -- 输出: [1, 1, 3, 4, 5]

性能考虑[编辑 | 编辑源代码]

时间复杂度：

操作	复杂度
索引访问	O(n)
头部插入	O(1)
尾部追加	O(n)
连接	O(n)

参见[编辑 | 编辑源代码]

Lean向量（更高效的随机访问结构）
Lean归纳类型（理解列表的理论基础）