15.7. 简化与重写🔗

simp 和 rw/rewrite 都使用等式引理，将项的一部分替换为等价形式。 不过，它们的预期用途和重写策略有所不同。 simp 系列的策略主要以标准化方式重新表述问题，使问题更便于人类理解和进一步自动化。 特别是，简化绝不应使原本可证的目标变得不可证。 rw 系列的策略主要用于应用人工选定的变换；这些变换不一定保持可证性，也不一定将项变为标准形式。 两类策略行为上的差异反映了各自侧重点的不同。

simp 策略主要从内向外重写。 它首先简化尽可能小的表达式，从而为外围表达式带来更多简化机会。 rw 策略选择与模式匹配的最左、最外层子项，并只重写一次。 两类策略都允许覆盖其默认策略：向 simp 集添加引理时，↓ 修饰符使其在简化子项之前应用；rw 配置参数的 occs 字段则允许通过白名单或黑名单选择其他出现位置。