15.7. 简化与重写🔗

simp 和 rw/rewrite 都使用等式引理将部分术语替换为等效替代项。 然而，它们的预期用途和重写策略有所不同。 simp 系列中的策略主要用于以标准化方式重新表述问题，使其更易于人类理解和进一步自动化。 特别是，简化决不应该使本来可以证明的目标变得不可能。 rw 系列中的策略主要用于应用手动选择的转换，这些转换并不总是保留可证明性，也不以标准化形式放置术语。 这些不同的侧重点体现在策略的两个家族之间的行为差异上。

simp策略主要是从内到外重写。 首先简化尽可能小的表达式，以便它们可以为周围的表达式释放进一步简化的机会。 rw策略选择与模式匹配的最左边最外层的子项，并重写它一次。 策略都允许覆盖其策略：将引理添加到 simp 集中时，↓ 修饰符会使其在子项简化之前应用，并且 rw 配置参数的 occs 字段允许通过白名单或黑名单选择不同的出现。