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)
  • 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-Elpi custom version
  • Coq-HoTT 8.17
• Coq namespace: Trocq
• Related publication(s):
  • Trocq: Proof Transfer for Free, With or Without Univalence

Building and installation instructions

Trocq is a still a prototype. In particular, it depends on a custom version of Coq-Elpi. 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.

And three 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.

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.