Lean4模式匹配

Lean4模式匹配是Lean4编程语言中一种强大的结构分解机制，允许开发者根据数据的形状或值进行条件分支处理。它是函数式编程的核心特性之一，能够显著提升代码的简洁性和可读性。

基本概念

模式匹配通过将输入值与预定义的模式进行比较，选择第一个匹配的分支执行。在Lean4中，模式匹配不仅限于简单值，还可用于解构归纳类型（inductive types）、记录类型（records）等复杂数据结构。

语法结构

基本语法使用match ... with表达式：

match expression with
| pattern1 => result1
| pattern2 => result2
...

基础示例

简单值匹配

def isZero : Nat → Bool
| 0 => true
| _ => false  -- 通配符 `_` 匹配任何值

#eval isZero 0  -- 输出: true
#eval isZero 3  -- 输出: false

递归类型匹配

匹配自然数的归纳定义：

inductive Nat where
| zero : Nat
| succ (n : Nat) : Nat

def pred : Nat → Nat
| Nat.zero => Nat.zero
| Nat.succ n => n

高级特性

多参数匹配

可同时匹配多个参数：

def and : Bool → Bool → Bool
| true, true => true
| _, _ => false

嵌套模式

支持嵌套结构解构：

inductive Tree where
| leaf : Nat → Tree
| node : Tree → Tree → Tree

def depth : Tree → Nat
| Tree.leaf _ => 1
| Tree.node l r => max (depth l) (depth r) + 1

带条件的模式（Pattern Guards）

使用if添加额外条件：

def isEven : Nat → Bool
| n => if n % 2 == 0 then true else false

实际应用案例

列表处理

实现标准map函数：

def map {α β : Type} (f : α → β) : List α → List β
| [] => []
| x :: xs => f x :: map f xs

表达式求值

处理简单算术表达式：

inductive Expr where
| num : Nat → Expr
| plus : Expr → Expr → Expr
| minus : Expr → Expr → Expr

def eval : Expr → Nat
| Expr.num n => n
| Expr.plus a b => eval a + eval b
| Expr.minus a b => eval a - eval b

模式匹配原理

Lean4的模式匹配在编译时会转换为递归方程（recursion equations）。例如： $\{\begin{array}{l}\text{isZero }0=\text{true}\\ \text{isZero }(\text{succ }n)=\text{false}\end{array}$

graph TD A[match表达式] --> B[模式1] A --> C[模式2] A --> D[...] B --> E[匹配成功时执行] C --> F[匹配成功时执行]

常见错误与提示

1. 非穷尽模式：未覆盖所有可能情况时，Lean会发出警告。解决方案是添加通配符或完整模式。 2. 冗余模式：被前面模式完全覆盖的模式会触发警告。 3. 类型不匹配：确保模式与输入值的类型一致。

最佳实践

• 优先使用模式匹配而非if/else处理复杂条件
• 对归纳类型使用结构化的模式匹配
• 为可读性考虑限制嵌套深度
• 使用通配符_明确表示不关心的值

进阶主题

依赖模式匹配

在依赖类型中匹配类型参数：

inductive Vec (α : Type) : Nat → Type where
| nil : Vec α 0
| cons : α → Vec α n → Vec α (n+1)

def head {α : Type} : Vec α (n+1) → α
| Vec.cons x xs => x

模式匹配编译细节

Lean4会执行以下转换步骤： 1. 模式编译（将模式转换为决策树） 2. 冗余检查 3. 代码生成

与其他语言的对比

特性	Lean4	Haskell	OCaml
通配符	_	_	_
模式守卫	通过if实现	条件	when子句
依赖模式	支持	有限支持	不支持

练习建议

1. 实现List.filter函数 2. 为二叉树编写mirror函数 3. 扩展Expr类型支持乘法并修改求值器