Skip to content

Commit

Permalink
updating README
Browse files Browse the repository at this point in the history
  • Loading branch information
amahboubi committed Jul 26, 2024
1 parent e070818 commit d417b00
Showing 1 changed file with 20 additions and 29 deletions.
49 changes: 20 additions & 29 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -23,27 +23,19 @@ 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 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://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.

## Meta

Expand All @@ -66,17 +58,17 @@ and readable code with respect to a sequent-style theoretical presentation.

## 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.
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 develop it and experiment with it,
they are 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

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.
Expand All @@ -87,7 +79,6 @@ the tactic `trocq`.
- `Trocq Register Univalence u` to declare a univalence axiom `u`.
- `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

Expand Down

0 comments on commit d417b00

Please sign in to comment.