编辑“︁Lean4模式匹配”︁

{{DISPLAYTITLE:Lean4模式匹配}}

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

== 基本概念 ==

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

=== 语法结构 ===
基本语法使用<code>match ... with</code>表达式：
<syntaxhighlight lang="lean">
match expression with
| pattern1 => result1
| pattern2 => result2
...
</syntaxhighlight>

== 基础示例 ==

=== 简单值匹配 ===
<syntaxhighlight lang="lean">
def isZero : Nat → Bool
| 0 => true
| _ => false  -- 通配符 `_` 匹配任何值

#eval isZero 0  -- 输出: true
#eval isZero 3  -- 输出: false
</syntaxhighlight>

=== 递归类型匹配 ===
匹配自然数的归纳定义：
<syntaxhighlight lang="lean">
inductive Nat where
| zero : Nat
| succ (n : Nat) : Nat

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

== 高级特性 ==

=== 多参数匹配 ===
可同时匹配多个参数：
<syntaxhighlight lang="lean">
def and : Bool → Bool → Bool
| true, true => true
| _, _ => false
</syntaxhighlight>

=== 嵌套模式 ===
支持嵌套结构解构：
<syntaxhighlight lang="lean">
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
</syntaxhighlight>

=== 带条件的模式（Pattern Guards） ===
使用<code>if</code>添加额外条件：
<syntaxhighlight lang="lean">
def isEven : Nat → Bool
| n => if n % 2 == 0 then true else false
</syntaxhighlight>

== 实际应用案例 ==

=== 列表处理 ===
实现标准<code>map</code>函数：
<syntaxhighlight lang="lean">
def map {α β : Type} (f : α → β) : List α → List β
| [] => []
| x :: xs => f x :: map f xs
</syntaxhighlight>

=== 表达式求值 ===
处理简单算术表达式：
<syntaxhighlight lang="lean">
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
</syntaxhighlight>

== 模式匹配原理 ==

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

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

== 常见错误与提示 ==

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

== 最佳实践 ==

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

== 进阶主题 ==

=== 依赖模式匹配 ===
在依赖类型中匹配类型参数：
<syntaxhighlight lang="lean">
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
</syntaxhighlight>

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

== 与其他语言的对比 ==

{| class="wikitable"
|-
! 特性 !! Lean4 !! Haskell !! OCaml
|-
| 通配符 || <code>_</code> || <code>_</code> || <code>_</code>
|-
| 模式守卫 || 通过<code>if</code>实现 || <code>|</code>条件 || <code>when</code>子句
|-
| 依赖模式 || 支持 || 有限支持 || 不支持
|}

== 练习建议 ==

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

{{Lean4特性导航}}

[[Category:计算机科学]]
[[Category:Lean]]
[[Category:Lean4特性]]