Thiago Felicissimo ; Frédéric Blanqui - Sharing proofs with predicative theories through universe-polymorphic elaboration

lmcs:12213 - Logical Methods in Computer Science, September 10, 2024, Volume 20, Issue 3 - https://doi.org/10.46298/lmcs-20(3:23)2024
Sharing proofs with predicative theories through universe-polymorphic elaborationArticle

Authors: Thiago Felicissimo ; Frédéric Blanqui

    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.


    Volume: Volume 20, Issue 3
    Published on: September 10, 2024
    Accepted on: June 17, 2024
    Submitted on: August 31, 2023
    Keywords: Computer Science - Logic in Computer Science

    Consultation statistics

    This page has been seen 373 times.
    This article's PDF has been downloaded 164 times.