Trocq: Proof Transfer for Free, With or Without Univalence
In: https://hal.science/hal-04177913 ; 2023, 2023
Online
report
Zugriff:
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.
Titel: |
Trocq: Proof Transfer for Free, With or Without Univalence
|
---|---|
Autor/in / Beteiligte Person: | Cohen, Cyril ; Crance, Enzo ; Mahboubi, Assia ; Sûreté du logiciel et Preuves Mathématiques Formalisées (STAMP) ; Inria Sophia Antipolis - Méditerranée (CRISAM) ; Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria) ; Mitsubishi Electric R&D Centre Europe France (MERCE-France) ; Mitsubishi Electric France ; Gallinette : vers une nouvelle génération d'assistant à la preuve (GALLINETTE) ; Inria Rennes – Bretagne Atlantique ; Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire des Sciences du Numérique de Nantes (LS2N) ; Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique) ; Institut Mines-Télécom Paris (IMT)-Institut Mines-Télécom Paris (IMT)-École Centrale de Nantes (Nantes Univ - ECN) ; Nantes Université (Nantes Univ)-Nantes Université (Nantes Univ)-Nantes université - UFR des Sciences et des Techniques (Nantes univ - UFR ST) ; Nantes Université - pôle Sciences et technologie ; Nantes Université (Nantes Univ)-Nantes Université (Nantes Univ)-Nantes Université - pôle Sciences et technologie ; Nantes Université (Nantes Univ)-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique) ; Nantes Université (Nantes Univ) ; European Project: 101001995,FRESCO(2021) |
Link: | |
Zeitschrift: | https://hal.science/hal-04177913 ; 2023, 2023 |
Veröffentlichung: | HAL CCSD, 2023 |
Medientyp: | report |
Schlagwort: |
|
Sonstiges: |
|