Lean tactic enables flexible proof rewriting across related types
A Transfer Tactic for Lean
Logic in Computer Science
Summary
In computer-assisted math proofs, rewriting helps replace parts of proofs with equivalent or related expressions. There are different levels of rewriting, each allowing more flexibility but needing more complex justifications. The authors created a new tactic for the Lean 4 system that supports the most flexible kind, which works across different types and operations. This tactic uses a database of tagged rules to automate these transfers and was tested on many existing proofs, successfully closing many cases. The evaluation showed the tactic is broadly useful and saves effort over time, especially where few existing theorems are available.
What this means in practice
- •For formal methods engineers: Enable more automated proof rewriting across different data types to speed up formal verification workflows.
- •For programming language developers: Improve type-related reasoning automation in language proof systems by integrating the transfer tactic for complex type relations.
Authors
Zhaoxi Chen, Daniel Raggi
Abstract
Rewriting in proof assistants spans a strict hierarchy. Equational rewriting substitutes based on extensional equality; subequational rewriting substitutes based on homogeneous relations such as $\leq$ or $\subseteq$, justified by monotonicity lemmas; and generalized rewriting relates different operations across different types, justified by transfer rules. All three are specializations of one schema, the function relator $(R \Rightarrow S)\,f\,g$. Lean 4's rw and Mathlib's grw/gcongr implement the first two levels, but the third has had no Lean implementation. We present one: a transfer tactic family over a tagged rule database, benchmarked using Mathlib's own test suites, of which 112 of 178 ported tests close through the transfer engine. An evaluation of the design's three motivating hypotheses returns a mixed result: generality holds, authoring effort wins in its amortized form (averaged per use), but on dependency footprint, transfer only ties a mature library and loses on coercions. This shows that transfer's value is concentrated on transferring into domains where few theorems exist.