Proposal to move project trocq to coq-community

[CohenCyril]

Project name:
Trocq - A modular parametricity plugin for proof transfer in Coq

Initial author(s):

• @CohenCyril - Cyril Cohen [email protected]
• @ecranceMERCE - Enzo Crance [email protected]
• @amahboubi - Assia Mahboubi [email protected]

Current URL:
https://github.com/ecranceMERCE/trocq

Kind:
Coq-ELPI plugin / library

License:
LGPL-3.0-or-later

Description:
Trocq is a prototype of 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, among which univalent parametricity [1] and CoqEAL [2], under 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.

[1] The marriage of univalence and parametricity, Tabareau et al. (2021)
[2] https://github.com/coq-community/coqeal

Status:
Actively maintained

New maintainer:
The initial authors should be maintainers

[palmskog]

@CohenCyril this project looks very welcome here at a glance, but it would be good to clarify two things:

1. The license is claimed to be GPLv3 here, but the LICENSE file says LGPL-3.0. Even if we assume GPLv3 is incorrect, would the correct license be LGPL-3.0-only or LGPL-3.0-or-later?
2. The README file says that this project depends on a custom version of Coq-ELPI. Will this custom version of Coq-ELPI be transferred to Coq-community as well? Otherwise, I am worried that the project could stop working if its dependency can't be maintained. Is there a plan to port to the regular Coq-ELPI?

[palmskog]

I have my answers now thanks to @ecranceMERCE:

1. The correct license is LGPL-3.0-or-later
2. The changes to Coq-ELPI are available as a PR: Missing API on universes LPCIC/coq-elpi#544

We will have to figure out together with the Coq-ELPI maintainer how this PR might be handled, but I think that can be a later issue. @CohenCyril feel free to transfer the Trocq repository when you are ready.

[CohenCyril]

@ecranceMERCE you only have the rights to make the transfer.

[palmskog]

Thanks everyone, the repo has been transferred: https://github.com/coq-community/trocq

Let's continue the discussion about the project as issues and pull requests to the public repo.