Trocq: Proof Transfer for Free, With or Without Univalence - Université Côte d'Azur
Preprints, Working Papers, ... (Working Paper) Year : 2023

Trocq: Proof Transfer for Free, With or Without Univalence

Abstract

In interactive theorem proving, a range of different representations may be available for a single mathematical concept, and some proofs may rely on several representations. Without automated support such as proof transfer, theorems available with different representations cannot be combined, without light to major manual input from the user. Tools with such a purpose exist, but in proof assistants based on dependent type theory, it still requires human effort to prove transfer, whereas it is obvious and often left implicit on paper. This paper presents Trocq, a new proof transfer framework, based on a generalization of the univalent parametricity translation, thanks to a new formulation of type equivalence. This translation takes care to avoid dependency on the axiom of univalence for transfers in a delimited class of statements, and may be used with relations that are not necessarily isomorphisms. We motivate and apply our framework on a set of examples designed to show that it unifies several existing proof transfer tools. The article also discusses an implementation of this translation for the Coq proof assistant, in the Coq-Elpi metalanguage.
Fichier principal
Vignette du fichier
main.pdf (1.03 Mo) Télécharger le fichier
Origin Files produced by the author(s)

Dates and versions

hal-04177913 , version 1 (06-08-2023)
hal-04177913 , version 2 (17-10-2023)
hal-04177913 , version 3 (19-10-2023)
hal-04177913 , version 4 (24-01-2024)
hal-04177913 , version 5 (24-01-2024)

Licence

Identifiers

  • HAL Id : hal-04177913 , version 1

Cite

Cyril Cohen, Enzo Crance, Assia Mahboubi. Trocq: Proof Transfer for Free, With or Without Univalence. 2023. ⟨hal-04177913v1⟩
670 View
545 Download

Share

More