Towards Pen-and-Paper-Style Equational Reasoning in Interactive Theorem Provers by Equality Saturation (steuwer.info)

The paper introduces a technique to recover “pen-and‑paper” style equational reasoning inside interactive theorem provers by treating theorems as conditional rewrite rules and using equality saturation over e-graphs to automate the rewriting. Rather than forcing users to spell out every implicit precondition (types, algebraic structure, domain constraints), their tactic in Lean translates a class of equational theorems from Lean’s type theory into conditional rewrites, runs an efficient equality‑saturation engine (egg) to explore equivalent terms, and then decodes the e‑graph proof into justificatory steps. Preconditions that cannot be discharged automatically are emitted as concise proof obligations for the user, preserving trustworthiness while removing much of the low‑level noise that normally clutters formal proofs. Technically, the work gives (1) a characterization of which equational theorems can be encoded as conditional rewrites in Lean, (2) an encoding that handles propositional preconditions and type‑class instantiations, and (3) a decoding mechanism that explains how theorems were instantiated and which conditions were used. Implemented as a Lean tactic backed by egg, the approach was evaluated on examples (including the binomial theorem) to show it reproduces intuitive textbook-style calculational proofs while hiding boilerplate rewrites. The method promises to improve readability and productivity in formalization by automating contextual equational reasoning without sacrificing soundness.