Rewriting is a powerful and principled term transformation technique with uses across theorem proving and compilation. In theorem proving, each rewrite is a proof step; in compilation, rewrites optimize a program term. While developing rewrite sequences manually is possible, this process does not scale when larger rewrite sequences are needed. Automated rewriting techniques, like greedy simplification or equality saturation, work well without requiring human input. Yet, they do not scale to large and complex search spaces, which limits the complexity of tasks where automated rewriting is effective, and means that just a small increase in term size or rewrite sequence length may result in failure.

This paper proposes a semi-automatic rewriting technique as a means to scale rewriting by allowing for human input at key decision points. Specifically, we propose guided equality saturation that embraces human guidance when fully automated equality saturation does not scale. A human provides an intermediate guide, and the rewriting is split into two simpler automatic equality saturation steps: from the original term to the guide, and from the guide to the target. A complex rewriting task may require multiple guides, resulting in a sequence of equality saturation steps. A guide need not be a complete term, it can also be a sketch containing undefined elements that are instantiated by the equality saturation search. Such sketches may be much more concise than complete program terms.

We demonstrate the generality and effectiveness of guided equality saturation using case studies in theorem proving and program optimization. First, we introduce guided equality saturation as a novel tactic in the Lean 4 proof assistant, allowing proofs to be written in the style of textbook proof sketches, i.e., as a series of calculations that omit details and skip steps. This tactic concludes in fractions of a second instead of minutes when compared to unguided equality saturation, and can find complex proofs that previously had to be done manually. Second, in the compiler of the RISE functional array language, where unguided equality saturation fails to perform advanced optimizations within an hour and using 60 GB of memory, guided equality saturation performs the same optimizations with up to 3 guides, within seconds and using less than 1 GB of memory.