From 6e93340f682b6c0f07031ff636703be120a319f9 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Fri, 3 Jan 2025 17:08:41 +0100 Subject: [PATCH] update meta and readme --- README.md | 57 ++++++++++++++++++++++++--------------- coq-trocq.opam | 45 ++++++++++++++++--------------- meta.yml | 73 ++++++++++++++++++++++++++------------------------ 3 files changed, 97 insertions(+), 78 deletions(-) diff --git a/README.md b/README.md index 349a6a6..0051bcc 100644 --- a/README.md +++ b/README.md @@ -23,19 +23,30 @@ Follow the instructions on https://github.com/coq-community/templates to regener [doi-shield]: https://zenodo.org/badge/DOI/10.5281/zenodo.10492403.svg [doi-link]: https://doi.org/10.5281/zenodo.10492403 -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](https://arxiv.org/abs/1209.6336), -[univalent parametricity](https://arxiv.org/abs/1209.6336) and -[CoqEAL](https://github.com/coq-community/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. +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](https://arxiv.org/abs/1209.6336), [univalent +parametricity](https://doi.org/10.1145/3429979) and +[CoqEAL](https://github.com/coq-community/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 @@ -58,11 +69,12 @@ The plugin is implemented in Coq-Elpi and the code of the parametricity translat ## Building and installation instructions -Trocq is a still a prototype. In particular, it depends on a [custom version](https://github.com/ecranceMERCE/coq-elpi/tree/strat) of Coq-Elpi. -It is not yet packaged in Opam or Nix. +Trocq is a still a prototype. In particular, it depends on a [custom +version](https://github.com/ecranceMERCE/coq-elpi/tree/strat) 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](INSTALL.md). +There are however three ways to experiment with it, all documented +in the [INSTALL.md file](INSTALL.md). ## Documentation @@ -70,14 +82,15 @@ See the [tutorial](artifact-doc/TUTORIAL.md) 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. + 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 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 Register Funext fe` to declare a function extensionality + axiom `fe`. ## ESOP 2024 artifact documentation diff --git a/coq-trocq.opam b/coq-trocq.opam index f1f95e0..d59df24 100644 --- a/coq-trocq.opam +++ b/coq-trocq.opam @@ -12,27 +12,30 @@ license: "LGPL-3.0-or-later" synopsis: "A modular parametricity plugin for proof transfer in Coq" description: """ -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](https://doi.org/10.1145/3429979) and -[CoqEAL](https://github.com/coq-community/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.""" +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](https://arxiv.org/abs/1209.6336), [univalent +parametricity](https://doi.org/10.1145/3429979) and +[CoqEAL](https://github.com/coq-community/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.""" build: [make "-j%{jobs}%"] install: [make "install"] diff --git a/meta.yml b/meta.yml index 1694f6c..86eddb4 100644 --- a/meta.yml +++ b/meta.yml @@ -11,27 +11,30 @@ synopsis: >- A modular parametricity plugin for proof transfer in Coq description: |- - 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](https://doi.org/10.1145/3429979) and - [CoqEAL](https://github.com/coq-community/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. + 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](https://arxiv.org/abs/1209.6336), [univalent + parametricity](https://doi.org/10.1145/3429979) and + [CoqEAL](https://github.com/coq-community/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. publications: - pub_url: https://hal.science/hal-04177913/document @@ -98,30 +101,30 @@ categories: build: |- ## Building and installation instructions - As Trocq is a prototype, it is currently unreleased, and depends on a - [custom version](https://github.com/ecranceMERCE/coq-elpi/tree/strat) - 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](INSTALL.md). + Trocq is a still a prototype. In particular, it depends on a [custom + version](https://github.com/ecranceMERCE/coq-elpi/tree/strat) 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](INSTALL.md). documentation: |- ## Documentation - For now, there is one tactic: + See the [tutorial](artifact-doc/TUTORIAL.md) 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. + 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 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 Register Funext fe` to declare a function extensionality + axiom `fe`. - See the [tutorial](artifact-doc/TUTORIAL.md) for concrete usecases. ## ESOP 2024 artifact documentation