15.4. 简单范式🔗

默认的 simp set 包含用 simp 属性标记的所有定理和简化过程。 表达式的 simp 范式 是通过 simp策略应用默认 simp 集的结果，直到无法应用更多规则。 当表达式采用 simp 范式时，它会根据默认的 simp 集尽可能地简化，通常使其更容易在证明中使用。

simp策略不保证汇合，这意味着表达式的 simp 范式可能取决于应用默认 simp 集的元素的顺序。 在设置 simp 属性时，可以通过分配优先级来更改应用规则的顺序。

设计 Lean 库时，重要的是要考虑适合库运算符的各种组合的简单范式。 这可以作为选择库应添加到默认 simp 集中的规则的指南。 特别是，simpl 引理的右侧应该是 simpl 范式；这有助于确保简化终止。 此外，库中的每个概念都应该通过一种 simpl 范式来表达，即使有多种等效的方式来表达它。 如果一个概念在不同的 simpl 引理中以两种不同的方式陈述，那么某些所需的简化可能不会发生，因为简化器没有连接它们。

尽管简化不需要汇合，但努力汇合是有帮助的，因为它使库更具可预测性，并且往往会揭示丢失或选择不当的简化引理。 默认 simp 集与其导出的常量的类型签名一样，都是库接口的一部分。

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