Lean简化器
简介[编辑 | 编辑源代码]
Lean简化器（Lean Simplifier）是Lean定理证明器中用于自动化简化数学表达式和逻辑命题的核心工具。它通过应用一系列预定义的简化规则（simp rules）来重写目标表达式，使其变得更简单或更接近可证明的形式。简化器常用于处理代数运算、逻辑等价转换以及条件表达式化简等场景。
简化器的主要特点包括：
- 可扩展性：用户可自定义简化规则
- 策略组合：常与其他策略（如`rw`、`apply`）配合使用
- 可控性：可通过配置调整简化深度和方向
基础用法[编辑 | 编辑源代码]
最基本的简化器调用方式是使用`simp`策略：
example : (a + 0) * 1 = a := by
simp -- 自动应用加法零元和乘法单位元规则
常用配置参数[编辑 | 编辑源代码]
| 参数 | 效果 | 示例 |
|---|---|---|
| `simp only` | 仅使用明确指定的规则 | `simp only [add_zero]` |
| `simp [...]` | 使用额外规则 | `simp [mul_comm]` |
| `simp at h` | 在假设h上简化 | `simp at ⊢ h` |
| `simp!` | 更积极地简化 | `simp!` |
简化规则系统[编辑 | 编辑源代码]
简化器的工作基于简化规则集，这些规则本质上是定向的等式定理。规则的一般形式为：
其中当`l`匹配目标时会被替换为`r`。
规则优先级[编辑 | 编辑源代码]
实际案例[编辑 | 编辑源代码]
代数表达式简化[编辑 | 编辑源代码]
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]
-- 逐步展开平方定义并重组项
条件逻辑简化[编辑 | 编辑源代码]
def isEven (n : Nat) : Bool := n % 2 == 0
example (h : n % 2 = 0) : isEven n = true := by
simp [isEven, h] -- 将定义展开并用假设h简化
高级主题[编辑 | 编辑源代码]
自定义简化规则[编辑 | 编辑源代码]
通过`@[simp]`属性声明规则：
@[simp] theorem reverse_nil : reverse [] = [] := rfl
@[simp] theorem reverse_cons (h : α) (t : List α) :
reverse (h :: t) = reverse t ++ [h] := by ...
调试简化过程[编辑 | 编辑源代码]
使用`simp?`查看建议的简化规则：
example : (a + 0) * 1 = a := by
simp? -- 输出：Try this: simp only [mul_one, add_zero]
性能考虑[编辑 | 编辑源代码]
简化器可能遇到以下情况时需要特别注意：
- 规则循环：相互引用的规则导致无限循环
- 过度简化：意外改变表达式语义
- 性能瓶颈：大型规则集导致速度下降
解决方案包括：
- 使用`simp only`限制规则范围
- 添加规则优先级注解
- 划分模块化规则集