Libraries of formalized mathematics use a possibly broad range of different representations for a same mathematical concept. Yet light to major manual input from users remains most often required for obtaining the corresponding variants of theorems, when such obvious replacements are typically left implicit on paper. This article presents Trocq, a new proof transfer framework for dependent type theory. Trocq is based on a novel formulation of type equivalence, used to generalize the univalent parametricity translation. This framework takes care of avoiding dependency on the axiom of univalence when possible, and may be used with more relations than just equivalences. We have implemented a corresponding plugin for the Coq proof assistant, in the CoqElpi meta-language. We use this plugin on a gallery of representative examples of proof transfer issues in interactive theorem proving, and illustrate how Trocq covers the spectrum of several existing tools, used in program verification as well as in formalized mathematics in the broad sense.

翻译：形式化数学库对同一数学概念可能采用广泛不同的表示方式。然而，获取这些概念对应定理的变体时，用户通常仍需提供从轻微到主要的手动输入，尽管这类显而易见的替换在纸面文献中通常默认省略。本文介绍了Trocq——一种适用于依赖类型理论的新的证明迁移框架。Trocq基于类型等价的新表述，用于推广单值参数性翻译。该框架在可能的情况下避免了依赖单价性公理，并且可以处理比等价关系更广泛的关系。我们在Coq证明助手的CoqElpi元语言中实现了相应的插件。通过一系列交互式定理证明中证明迁移问题的代表性实例库，我们展示了Trocq如何涵盖多种现有工具的功能范围，这些工具广泛用于程序验证及形式化数学领域。