In interactive theorem proving, a single mathematical concept may have multiple representations, and proofs often involve reasoning across these. Without automated support such as proof transfer, theorems stated using different representations cannot be easily combined—requiring anything from light to substantial manual effort from the user.
A seamless and formally verified transfer of formal definitions and statements, that blurs irrelevant syntactic differences between semantically similar concepts has many potential benefits, for enhancing the productivity of user. In this project we will specifically address the two following applications :
- the discovery and validation of existing results in the available ecosystem of formal libraries of the prover, or even that of other provers based on similar foundations;
- the improvement and maintenance of existing code, enhancing its robustness and conciseness, via automated proof-repair.
While some existing prototypes already address this challenge, proof assistants based on dependent type theory still demand human intervention to establish such transfers, even when the equivalences are straightforward and left implicit in mathematical practice.
Recently, Trocq, a proof transfer framework based on a generalized form of univalent parametricity, enabled by a novel formulation of type equivalence. Trocq is implemented in the Rocq prover assistant, using the Rocq-Elpi metaprogramming language.
The objective of this project is to make this framework scale, and accommodate the needs created by AI-generated formal code, e.g. by translation or by refactoring tools.
