Document Open Access Logo

Translating Proofs from an Impredicative Type System to a Predicative One

Authors Thiago Felicissimo, Frédéric Blanqui, Ashish Kumar Barnawal



PDF
Thumbnail PDF

File

LIPIcs.CSL.2023.19.pdf
  • Filesize: 1.08 MB
  • 19 pages

Document Identifiers

Author Details

Thiago Felicissimo
  • Université Paris-Saclay, INRIA project, Deducteam, Laboratoire Méthodes Formelles, ENS Paris-Saclay, 91190 France
Frédéric Blanqui
  • Université Paris-Saclay, INRIA project, Deducteam, Laboratoire Méthodes Formelles, ENS Paris-Saclay, 91190 France
Ashish Kumar Barnawal
  • Indian Institute of Technology Guwahati, Guwahati 781039, Assam, India

Acknowledgements

The authors would like to thank François Thiré for the help while developing Predicativize, Gilles Dowek for remarks about previous versions of this paper, Jesper Cockx and Vincent Moreau for discussions about universe levels and the anonymous reviewers for the very helpful comments and remarks.

Cite AsGet BibTex

Thiago Felicissimo, Frédéric Blanqui, and Ashish Kumar Barnawal. Translating Proofs from an Impredicative Type System to a Predicative One. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 19:1-19:19, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.CSL.2023.19

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, such as Coq, Matita and the HOL family, to proof assistants based on predicative logics like Agda, whenever impredicativity is not used in an essential way. In this paper we present an algorithm to do such a translation between a core impredicative type system and a core predicative one allowing prenex universe polymorphism like in Agda. It consists in trying to turn a potentially impredicative term into a universe polymorphic term as general as possible. The use of universe polymorphism is justified by the fact that mapping an impredicative universe to a fixed predicative one is not sufficient in most cases. During the algorithm, we need to solve unification problems modulo the max-successor algebra on universe levels. But, in this algebra, there are solvable problems having no most general solution. We however provide an incomplete algorithm whose solutions, when it succeeds, are most general ones. 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 Bertrand’s Postulate and Fermat’s Little Theorem, which were not available in Agda yet.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic
  • Theory of computation → Type theory
  • Theory of computation → Equational logic and rewriting
Keywords
  • Type Theory
  • Impredicativity
  • Predicativity
  • Proof Translation
  • Universe Polymorphism
  • Unification Modulo Max
  • Agda
  • Dedukti

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads

References

  1. Andrea Asperti and Wilmer Ricciotti. A proof of bertrand’s postulate. Journal of Formalized Reasoning, 5(1):37-57, 2012. Google Scholar
  2. Ali Assaf. A framework for defining computational higher-order logics. These, École polytechnique, September 2015. URL: https://pastel.archives-ouvertes.fr/tel-01235303.
  3. Ali Assaf, Guillaume Burel, Raphaël Cauderlier, D Delahaye, G Dowek, C Dubois, F Gilbert, P Halmagrand, O Hermant, and R Saillard. Dedukti: a logical framework based on the λ π-calculus modulo theory. Unpublished, 2016. Google Scholar
  4. H. P. Barendregt. Lambda Calculi with Types, pages 117-309. Oxford University Press, Inc., USA, 1993. Google Scholar
  5. Michael Beeson, Julien Narboux, and Freek Wiedijk. Proof-checking Euclid. Annals of Mathematics and Artificial Intelligence, page 53, January 2019. URL: https://doi.org/10.1007/s10472-018-9606-x.
  6. F. Blanqui. Rewriting modulo in deduction modulo. In Proceedings of the 14th International Conference on Rewriting Techniques and Applications, Lecture Notes in Computer Science 2706, 2003. 15 pages. URL: https://doi.org/10.1007/3-540-44881-0_28.
  7. F. Blanqui. Definitions by rewriting in the calculus of constructions. Mathematical Structures in Computer Science, 15(1):37-92, 2005. URL: https://doi.org/10.1017/S0960129504004426.
  8. Frédéric Blanqui. Théorie des types et réécriture. (Type theory and rewriting). PhD thesis, University of Paris-Sud, Orsay, France, 2001. URL: https://tel.archives-ouvertes.fr/tel-00105522.
  9. Frédéric Blanqui. Type safety of rewrite rules in dependent types. In 5th International Conference on Formal Structures for Computation and Deduction, 2020. Google Scholar
  10. Frédéric Blanqui. Encoding type universes without using matching modulo AC. In Proceedings of the 7th International Conference on Formal Structures for Computation and Deduction, Leibniz International Proceedings in Informatics 228, 2022. URL: https://doi.org/10.4230/LIPIcs.FSCD.2022.24.
  11. Frédéric Blanqui, Gilles Dowek, Émilie Grienenberger, Gabriel Hondet, and François Thiré. Some axioms for mathematics. In Naoki Kobayashi, editor, 6th International Conference on Formal Structures for Computation and Deduction, FSCD 2021, July 17-24, 2021, Buenos Aires, Argentina (Virtual Conference), volume 195 of LIPIcs, pages 20:1-20:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.FSCD.2021.20.
  12. Denis Cousineau and Gilles Dowek. Embedding pure type systems in the lambda-pi-calculus modulo. In Simona Ronchi Della Rocca, editor, Typed Lambda Calculi and Applications, pages 102-117, Berlin, Heidelberg, 2007. Springer Berlin Heidelberg. Google Scholar
  13. Tristan Delort. Importer les preuves de Logipedia dans Agda. Internship report, Inria Saclay Ile de France, November 2020. URL: https://hal.inria.fr/hal-02985530.
  14. Thiago Felicissimo. Adequate and Computational Encodings in the Logical Framework Dedukti. In Amy P. Felty, editor, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022), volume 228 of Leibniz International Proceedings in Informatics (LIPIcs), pages 25:1-25:18, Dagstuhl, Germany, 2022. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.FSCD.2022.25.
  15. Gaspard Ferey. Higher-Order Confluence and Universe Embedding in the Logical Framework. These, Université Paris-Saclay, June 2021. URL: https://tel.archives-ouvertes.fr/tel-03418761.
  16. Guillaume Genestier. Encoding agda programs using rewriting. In Zena M. Ariola, editor, 5th International Conference on Formal Structures for Computation and Deduction, FSCD 2020, June 29-July 6, 2020, Paris, France (Virtual Conference), volume 167 of LIPIcs, pages 31:1-31:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPIcs.FSCD.2020.31.
  17. Yoan Géran. Euclid’s elements book 1 in dedukti. URL: https://github.com/Karnaj/sttfa_geocoq_euclid [cited 2022].
  18. Robert Harper and Robert Pollack. Type checking with universes. Theor. Comput. Sci., 89(1):107-136, August 1991. URL: https://doi.org/10.1016/0304-3975(90)90108-T.
  19. R. Saillard. Type checking in the Lambda-Pi-calculus modulo: theory and practice. PhD thesis, Mines ParisTech, France, 2015. URL: https://pastel.archives-ouvertes.fr/tel-01299180.
  20. Ronan Saillard. Type checking in the Lambda-Pi-calculus modulo: theory and practice. PhD thesis, PhD thesis, Mines ParisTech, France, 2015. Google Scholar
  21. Matthieu Sozeau and Nicolas Tabareau. Universe polymorphism in coq. In International Conference on Interactive Theorem Proving, pages 499-514. Springer, 2014. Google Scholar
  22. Agda Development Team. Agda 2.6.2.1 documentation. URL: https://agda.readthedocs.io/en/v2.6.2.1/index.html [cited 2022].
  23. François Thiré. Sharing a library between proof assistants: Reaching out to the HOL family. In Frédéric Blanqui and Giselle Reis, editors, Proceedings of the 13th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP@FSCD 2018, Oxford, UK, 7th July 2018, volume 274 of EPTCS, pages 57-71, 2018. URL: https://doi.org/10.4204/EPTCS.274.5.
  24. François Thiré. Interoperability between proof systems using the logical framework Dedukti. PhD thesis, ENS Paris-Saclay, 2020. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail