编辑“︁Lean简化器”︁

{{DISPLAYTITLE:Lean简化器}}

== 简介 ==
'''Lean简化器'''（Lean Simplifier）是[[Lean定理证明器]]中用于自动化简化数学表达式和逻辑命题的核心工具。它通过应用一系列预定义的''简化规则''（simp rules）来重写目标表达式，使其变得更简单或更接近可证明的形式。简化器常用于处理代数运算、逻辑等价转换以及条件表达式化简等场景。

简化器的主要特点包括：
* '''可扩展性'''：用户可自定义简化规则
* '''策略组合'''：常与其他策略（如`rw`、`apply`）配合使用
* '''可控性'''：可通过配置调整简化深度和方向

== 基础用法 ==
最基本的简化器调用方式是使用`simp`策略：

<syntaxhighlight lang="lean">
example : (a + 0) * 1 = a := by
  simp  -- 自动应用加法零元和乘法单位元规则
</syntaxhighlight>

=== 常用配置参数 ===
{| class="wikitable"
|-
! 参数 !! 效果 !! 示例
|-
| `simp only` || 仅使用明确指定的规则 || `simp only [add_zero]`
|-
| `simp [...]` || 使用额外规则 || `simp [mul_comm]`
|-
| `simp at h` || 在假设h上简化 || `simp at ⊢ h`
|-
| `simp!` || 更积极地简化 || `simp!`
|}

== 简化规则系统 ==
简化器的工作基于''简化规则集''，这些规则本质上是定向的等式定理。规则的一般形式为：

<math>\forall x_1 \ldots x_n, \quad l = r</math>

其中当`l`匹配目标时会被替换为`r`。

=== 规则优先级 ===
<mermaid>
graph TD
    A[用户本地规则] -->|最高优先级| B[库中标记为[simp]的规则]
    B --> C[内置核心规则]
</mermaid>

== 实际案例 ==
=== 代数表达式简化 ===
<syntaxhighlight lang="lean">
example (x y : Nat) : (x + y) ^ 2 = x ^ 2 + 2 * x * y + y ^ 2 := by
  simp [pow_succ, mul_add, add_mul, add_assoc, add_comm, add_left_comm]
  -- 逐步展开平方定义并重组项
</syntaxhighlight>

=== 条件逻辑简化 ===
<syntaxhighlight lang="lean">
def isEven (n : Nat) : Bool := n % 2 == 0

example (h : n % 2 = 0) : isEven n = true := by
  simp [isEven, h]  -- 将定义展开并用假设h简化
</syntaxhighlight>

== 高级主题 ==
=== 自定义简化规则 ===
通过`@[simp]`属性声明规则：

<syntaxhighlight lang="lean">
@[simp] theorem reverse_nil : reverse [] = [] := rfl
@[simp] theorem reverse_cons (h : α) (t : List α) : 
  reverse (h :: t) = reverse t ++ [h] := by ...
</syntaxhighlight>

=== 调试简化过程 ===
使用`simp?`查看建议的简化规则：

<syntaxhighlight lang="lean">
example : (a + 0) * 1 = a := by
  simp?  -- 输出：Try this: simp only [mul_one, add_zero]
</syntaxhighlight>

== 性能考虑 ==
简化器可能遇到以下情况时需要特别注意：
* '''规则循环'''：相互引用的规则导致无限循环
* '''过度简化'''：意外改变表达式语义
* '''性能瓶颈'''：大型规则集导致速度下降

解决方案包括：
* 使用`simp only`限制规则范围
* 添加规则优先级注解
* 划分模块化规则集

== 参见 ==
* [[重写策略]]（`rw`）
* [[决策过程]]
* [[自定义策略]]

{{Lean证明技术导航}}

[[Category:计算机科学]]
[[Category:Lean]]
[[Category:Lean高级证明技术]]