Trocq: Proof Transfer for Free, With or Without Univalence - Université Côte d'Azur Access content directly
Conference Papers Year : 2024

Trocq: Proof Transfer for Free, With or Without Univalence


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 (743.67 Ko) 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)



  • HAL Id : hal-04177913 , version 5


Cyril Cohen, Enzo Crance, Assia Mahboubi. Trocq: Proof Transfer for Free, With or Without Univalence. ESOP 2024 - 33rd European Symposium on Programming, Apr 2024, Luxembourg, Luxembourg. pp.239-268. ⟨hal-04177913v5⟩
521 View
437 Download


Gmail Mastodon Facebook X LinkedIn More