编辑“︁Lean列表”︁

{{DISPLAYTITLE:Lean列表}}

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

== 定义与语法 ==
Lean标准库（`List`命名空间）中列表的归纳定义如下：
<syntaxhighlight lang="lean">
inductive List (α : Type u) where
  | nil : List α
  | cons (head : α) (tail : List α) : List α
</syntaxhighlight>
* `nil`表示空列表
* `cons`用于在列表头部添加元素（构造非空列表）

=== 语法糖 ===
Lean提供简写形式：
* `[]`等价于`nil`
* `a :: l`等价于`cons a l`
* `[a, b, c]`等价于`a :: b :: c :: []`

== 基本操作 ==
=== 构造列表 ===
<syntaxhighlight lang="lean">
-- 空列表
def emptyList : List Nat := []

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

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

=== 长度计算 ===
递归计算列表长度的典型实现：
<syntaxhighlight lang="lean">
def length {α : Type} : List α → Nat
  | [] => 0
  | _ :: tail => 1 + length tail

#eval length [true, false]  -- 输出: 2
</syntaxhighlight>

=== 连接操作 ===
使用`++`运算符或递归实现：
<syntaxhighlight lang="lean">
def concat {α : Type} : List α → List α → List α
  | [], l => l
  | h :: t, l => h :: concat t l

#eval [1, 2] ++ [3, 4]  -- 输出: [1, 2, 3, 4]
</syntaxhighlight>

== 高级操作 ==
=== 映射（Map） ===
使用`List.map`对每个元素应用函数：
<syntaxhighlight lang="lean">
#eval List.map (fun x => x * 2) [1, 2, 3]  -- 输出: [2, 4, 6]
</syntaxhighlight>

=== 过滤（Filter） ===
使用谓词筛选元素：
<syntaxhighlight lang="lean">
#eval List.filter (fun x => x % 2 == 0) [1, 2, 3, 4]  -- 输出: [2, 4]
</syntaxhighlight>

=== 折叠（Fold） ===
左右折叠实现：
<syntaxhighlight lang="lean">
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
</syntaxhighlight>

== 内存结构 ==
<mermaid>
graph LR
  A[cons] --> B[1]
  A --> C[cons]
  C --> D[2]
  C --> E[cons]
  E --> F[3]
  E --> G[nil]
</mermaid>

== 数学性质 ==
列表操作满足以下代数定律：
* 连接结合律：<math>(l_1 ++ l_2) ++ l_3 = l_1 ++ (l_2 ++ l_3)</math>
* 单位元：<math>[] ++ l = l ++ [] = l</math>
* 映射复合：<math>map\ f \circ map\ g = map\ (f \circ g)</math>

== 实际案例 ==
=== 矩阵转置 ===
使用列表实现矩阵操作：
<syntaxhighlight lang="lean">
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]]
</syntaxhighlight>

=== 快速排序 ===
经典算法实现：
<syntaxhighlight lang="lean">
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]
</syntaxhighlight>

== 性能考虑 ==
* '''时间复杂度'''：
  {| class="wikitable"
  ! 操作 !! 复杂度
  |-
  | 索引访问 || O(n)
  |-
  | 头部插入 || O(1)
  |-
  | 尾部追加 || O(n)
  |-
  | 连接 || O(n)
  |}

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

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

[[Category:计算机科学]]
[[Category:Lean]]