发表机构
University of Cambridge（剑桥大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
针对 Lean 中缺失的广义重写层次，提出基于带标签规则库的传递策略族，在 Mathlib 测试中 112/178 通过，验证了通用性与摊销创作成本优势，但依赖足迹仅持平。
AI 中文摘要
证明助手中的重写遵循一个严格的分层结构。等式重写基于外延相等进行替换；亚等式重写基于同质关系（如 $\leq$ 或 $\subseteq$）进行替换，并由单调性引理提供依据；广义重写则在不同类型之间关联不同的运算，由传递规则提供依据。这三者都是同一模式——函数关系子 $(R \Rightarrow S)\\,f\\,g$——的特例。Lean 4 的 rw 和 Mathlib 的 grw/gcongr 实现了前两个层次，但第三个层次在 Lean 中尚无实现。我们提出了一种实现：一个基于带标签规则数据库的传递策略族，并使用 Mathlib 自身的测试套件进行基准测试，其中 178 个移植测试中有 112 个通过传递引擎闭合。对该设计三个核心假设的评估结果呈现混合状态：通用性成立；在创作成本方面，其摊销形式（按每次使用平均）具有优势；但在依赖足迹方面，传递仅能与成熟库持平，且在强制类型转换上有所不足。这表明传递的价值集中于将结果传递到定理稀缺的领域。
英文摘要
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.
Comments10 pages, 3 tables. Submitted for publication
