15.4. simp 范式🔗

默认的simp 集包含所有以 simp 属性标记的定理和简化过程。 表达式的 simp 范式，是通过 simp 策略应用默认 simp 集，直至没有规则可以继续应用而得到的结果。 当表达式处于 simp 范式时，它已经按照默认 simp 集尽可能充分地归约，因此通常更便于在证明中使用。

simp 策略不保证合流性，这意味着表达式的 simp 范式可能取决于默认 simp 集中各元素的应用顺序。 设置 simp 属性时可以指定优先级，从而改变规则的应用顺序。

设计 Lean 库时，必须考虑库中各种运算符组合应当采用哪种合适的 simp 范式。 这可以指导开发者选择库应向默认 simp 集添加哪些规则。 特别是，simp 引理的右侧应当处于 simp 范式；这有助于确保简化终止。 此外，即使一个概念有多种等价的陈述方式，库中也应通过一种 simp 范式来表达它。 如果不同的 simp 引理以两种不同方式陈述同一概念，那么简化器可能无法把二者联系起来，致使某些预期的简化无法发生。

尽管简化不必具有合流性，力求合流仍然很有帮助，因为这会使库的行为更可预测，也往往能暴露缺失或选择不当的 simp 引理。 默认 simp 集和库所导出常量的类型签名一样，都是库接口的一部分。

库不应向默认 simp 集添加未提及该库所定义的任何常量的规则。 否则，导入一个库可能会改变 simp 对某个不相关库的行为。 如果一个库依赖其他库中定义或声明的额外简化规则，请创建自定义 simp 集，并指示用户使用它，或者提供专用策略。