As the development of formal proofs is a time-consuming task, it is important to devise ways of sharing the already written proofs to prevent wasting time redoing them. One of the challenges in this domain is to translate proofs written in proof assistants based on impredicative logics to proof assistants based on predicative logics, whenever impredicativity is not used in an essential way. In this paper we present a transformation for sharing proofs with a core predicative system supporting prenex universe polymorphism (like in Agda). It consists in trying to elaborate a potentially impredicative term into a predicative universe polymorphic term as general as possible. The use of universe polymorphism is justified by the fact that mapping each universe to a fixed one in the target theory is not sufficient in most cases. During the algorithm, we need to solve unification problems in the equational theory of universe levels. In order to do this, we give a complete characterization of when a single equation admits a most general unifier. This characterization is then employed in an algorithm which uses a constraint-postponement strategy to solve unification problems. The proposed translation is of course partial, but in practice allows one to translate many proofs that do not use impredicativity in an essential way. Indeed, it was implemented in the tool Predicativize and then used to translate semi-automatically many non-trivial developments from Matita's arithmetic library to Agda, including proofs of Bertrand's Postulate and Fermat's Little Theorem, which (as far as we know) were not available in Agda yet.

翻译：形式化证明的开发是一项耗时任务，因此设计一种能够重用已有证明的方法至关重要，以避免重复劳动。该领域的主要挑战之一，是在非本质使用非谓词性的情况下，将基于非谓词逻辑的证明辅助工具中的证明，翻译到基于谓词逻辑的证明辅助工具中。本文提出了一种转换方法，用于将证明共享给支持前束宇宙多态性（如Agda）的谓词核心系统。该方法尝试将一个可能具有非谓词性的项，精化为尽可能通用的谓词宇宙多态项。宇宙多态性的使用基于以下事实：在大多数情况下，仅将每个宇宙映射到目标理论中的固定宇宙是不够的。在算法实现过程中，我们需要在宇宙层级的等式理论下解决合一问题。为此，我们给出了单个方程在何种情况下存在最一般合一子的完整刻画。该刻画被应用于采用约束延迟策略的合一问题求解算法。所提出的翻译方法显然是部分的，但在实践中能够翻译大量未实质使用非谓词性的证明。该翻译方法已在工具Predicativize中实现，并成功应用于将Matita算术库中的多个非平凡数学证明（包括伯特兰公设和费马小定理的证明）半自动地翻译至Agda，这些证明此前（据我们所知）在Agda中尚不可用。