8.7. 単純化と書き換え（Simplification vs Rewriting）🔗

simp と rw ・ rewrite はどちらも等式の補題を使用して、項の一部を同値な代替の項に置き換えます。しかし、それらの意図された用途と書き換え戦略は異なります。 simp の族のタクティクは、主に標準化された方法で問題を再定式化するために使用され、人間の理解とさらなる自動化の両方に供します。特に、単純化することで、他に証明可能なゴールが不可能になるようなことがあってはなりません。 rw の族のタクティクは主に手作業で選択された変換を適用するために使用されます。これは証明可能性を常に保持したり、項を標準化された形式に配置したりしません。これらの異なる強調点は、2つのタクティクの族の動作の違いに反映されています。

simp タクティクは主に内側から外側へ書き換えます。可能な限り小さい式が最初に単純化され、周囲の式のさらなる単純化の機会を解放します。 rw タクティクは、パターンにマッチする最も左の外側の部分項を選択し、それを1回だけ書き換えます。どちらのタクティクもその戦略を上書きすることができます：simp セットに補題を追加するとき、↓ 修飾子は部分項の単純化の前に適用されるようにし、 rw の設定パラメータの occs フィールドは複数の出現に対してホワイトリストかブラックリストのいずれかの選択を可能にします。