Trocq is a prototype of a modular parametricity plugin for Coq, aiming to perform proof transfer by translating the goal into an associated goal featuring the target data structures as well as a rich parametricity witness from which a function justifying the goal substitution can be extracted.
The plugin features a hierarchy of parametricity witness types, ranging from structure-less relations to a new formulation of type equivalence, gathering several pre-existing parametricity translations, including univalent parametricity and CoqEAL, in the same framework.
This modular translation performs a fine-grained analysis and generates witnesses that are rich enough to preprocess the goal yet are not always a full-blown type equivalence, allowing to perform proof transfer with the power of univalent parametricity, but trying not to pull in the univalence axiom in cases where it is not required.
The translation is implemented in Coq-Elpi and features transparent and readable code with respect to a sequent-style theoretical presentation.
- Author(s):
- Cyril Cohen (initial)
- Enzo Crance (initial)
- Assia Mahboubi (initial)
- Coq-community maintainer(s):
- Cyril Cohen (@CohenCyril)
- Enzo Crance (@ecranceMERCE)
- Assia Mahboubi (@amahboubi)
- License: GNU Lesser General Public License v3.0
- Compatible Coq versions: 8.17
- Additional dependencies:
- Coq namespace:
Trocq
- Related publication(s):
As Trocq is a prototype, it is currently unreleased, and depends on a custom version of Coq-Elpi. It is not yet packaged in Opam or Nix, but will be in the near future.
There are however three ways to develop it and experiment with it, they are documented in the INSTALL.md file.
For now, there is one tactic:
trocq
(without arguments) which attempts to run a translation on a given goal, using the information provided by the user with the commands described below.
And three commands:
Trocq Use t
to use a translationt
during the subsequent calls to the tactictrocq
.Trocq Register Univalence u
to declare a univalence axiomu
.Trocq Register Funext fe
to declare a function extensionality axiomfe
.
See the tutorial for concrete usecases.
The ESOP 2024 artifact documentation files can be found in the artifact-doc
directory, except for INSTALL.md
that can be found in the current directory.