{"id":"arxiv:2609.32115","kind":"preprint","title":"A Transfer Tactic for Lean","authors":["Zhaoxi Chen","Daniel Raggi"],"author_count":2,"year":2026,"published":"2026-09-26","venue":null,"cited_by":null,"doi":null,"arxiv_id":"2609.32115","nct_id":null,"source_url":"https://arxiv.org/abs/2609.32115","archive_url":"https://space-kitty.com/papers/arxiv:2609.32115","updated":"2026-09-26","pmid":null,"pmcid":null,"openalex_id":null,"pdf_url":"https://arxiv.org/pdf/2609.32115","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.","abstract_license":"CC0-1.0 (arXiv descriptive metadata)","license":null,"is_open_access":false,"retracted":false,"peer_reviewed":false,"categories":["cs.LO"],"details":null,"provenance":"arxiv","attribution":"Abstract: arXiv descriptive metadata (CC0). Thank you to arXiv for use of its open access interoperability. This service was not reviewed or approved by, nor does it necessarily express or reflect the policies or opinions of, arXiv.","topics":[],"cited_in_dossiers":[]}