8.7. Simplification vs Rewriting🔗

Both simp and rw/rewrite use equational lemmas to replace parts of terms with equivalent alternatives. Their intended uses and their rewriting strategies differ, however. Tactics in the simp family are primarily used to reformulate a problem in a standardized way, making it more amenable to both human understanding and further automation. In particular, simplification should never render an otherwise-provable goal impossible. Tactics in the rw family are primarily used to apply hand-selected transformations that do not always preserve provability nor place terms in standardized forms. These different emphases are reflected in the differences of behavior between the two families of tactics.

The simp tactics primarily rewrite from the inside out. The smallest possible expressions are simplified first so that they can unlock further simplification opportunities for the surrounding expressions. The rw tactics select the leftmost outermost subterm that matches the pattern, rewriting it a single time. Both tactics allow their strategy to be overridden: when adding a lemma to a simp set, the ↓ modifier causes it to be applied prior to the simplification of subterms, and the occs field of rw's configuration parameter allows a different occurrence to be selected, either via a whitelist or a blacklist.