Sharing proofs with predicative theories through universe-polymorphic elaboration

TL;DR

This paper introduces a universe-polymorphic elaboration method for translating impredicative proofs into predicative proof systems, enabling proof sharing and reuse across different logical frameworks.

Contribution

It presents a novel transformation technique using universe polymorphism and unification solving, implemented in the Predicativize tool for proof translation.

Findings

Successfully translated non-trivial proofs like Bertrand's Postulate and Fermat's Little Theorem.

Implemented a partial but practical translation method for proofs not relying on impredicativity.

Provided a complete characterization of unification problems with universe levels.

Abstract

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. It consists in trying to elaborate each 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 elaboration, 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 a partial algorithm which uses a constraint-postponement strategy for trying 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 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.