Trocq

Trocq is a modular parametricity plugin for Coq. It can be used to achieve proof transfer by both translating a user goal into another, related, variant, and computing a proof that proves the corresponding implication.

The plugin features a hierarchy of structures on relations, whose instances are computed from registered user-defined proof via parametricity. This hierarchy ranges from structure-less relations to an original formulation of type equivalence. The resulting framework generalizes raw parametricity, univalent parametricity and CoqEAL, and includes them in a unified framework.

The plugin computes a parametricity translation "à la carte", by performing a fine-grained analysis of the requires properties for a given proof of relatedness. In particular, it is able to prove implications without resorting to full-blown type equivalence, allowing this way to perform proof transfer without necessarily pulling in the univalence axiom.

The plugin is implemented in Coq-Elpi and the code of the parametricity translation is fairly close to a pen-and-paper sequent-style presentation.

Meta

• Author(s):
  • Cyril Cohen (initial)
  • Enzo Crance (initial)
  • Lucie Lahaye
  • Assia Mahboubi (initial)
• Coq-community maintainer(s):
  • Cyril Cohen (@CohenCyril)
  • Enzo Crance (@ecranceMERCE)
  • Lucie Lahaye (@lweqx)
  • Assia Mahboubi (@amahboubi)
• License: GNU Lesser General Public License v3.0
• Compatible Coq versions: 8.20, 9.0 and 9.1
• Additional dependencies:
  • Coq-Elpi
• Coq namespace: Trocq
• Related publication(s):
  • Trocq: Proof Transfer for Free, With or Without Univalence

Building and installation instructions

Trocq is still a prototype. It is not yet packaged in Opam or Nix.

There are however three ways to experiment with it, all documented in the INSTALL.md file.

Documentation

See the tutorial for concrete use cases.

In short, the plugin provides a 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. - trocq R1 R2 ... which works similarly to its argumentless counterpart except that it also uses translations associated to the relations R1, R2... ; see below regarding how to associated translations to a relation.

And four commands: - Trocq Use t to use a translation t during the subsequent calls to the tactic trocq. - Trocq Register Univalence u to declare a univalence axiom u. - Trocq Register Funext fe to declare a function extensionality axiom fe. - Trocq RelatedWith R t1 t2 ... to associate t1, t2, ... to R. Subsequent calls to trocq R will be able to use the translations t1, t2, ... - Trocq Logging "off"|"info"|"debug"|"trace" to set the verbosity level.

ESOP 2024 artifact documentation

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.