Awesome
<!--- This file was generated from `meta.yml`, please do not edit manually. Follow the instructions on https://github.com/coq-community/templates to regenerate. --->Paramcoq
A Coq plugin providing commands for generating parametricity statements. Typical applications of such statements are in data refinement proofs. Note that the plugin is still in an experimental state - it is not very user friendly (lack of good error messages) and still contains bugs. But it is usable enough to "translate" a large chunk of the standard library.
Meta
- Author(s):
- Chantal Keller (initial)
- Marc Lasson (initial)
- Abhishek Anand
- Pierre Roux
- Emilio Jesús Gallego Arias
- Cyril Cohen
- Matthieu Sozeau
- Coq-community maintainer(s):
- Pierre Roux (@proux01)
- License: MIT License
- Compatible Coq versions: The master branch tracks the development version of Coq, see releases for compatibility with released versions of Coq
- Additional dependencies: none
- Coq namespace:
Param - Related publication(s):
Building and installation instructions
The easiest way to install the latest released version of Paramcoq is via OPAM:
opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-paramcoq
To instead build and install manually, do:
git clone https://github.com/coq-community/paramcoq.git
cd paramcoq
make # or make -j <number-of-cores-on-your-machine>
make install
Usage and Commands
To load the plugin and make its commands available:
From Param Require Import Param.
The command scheme for named translations is:
Parametricity <ident> as <name> [arity <n>].
For example, the following command generates a translation named my_param
of the constant or inductive my_id with arity 2 (the default):
Parametricity my_id as my_param.
The command scheme for automatically named translations is:
Parametricity [Recursive] <ident> [arity <n>] [qualified].
Such commands generate and name translations based on the given identifier.
The Recursive option can be used to recursively translate all the constants
and inductives which are used by the constant or inductive with the given
identifier. The qualified option allows you to use a qualified default name
for the translated constants and inductives. The default name then has the form
Module_o_Submodule_o_my_id if the identifier my_id is declared in the
Module.Submodule namespace.
Instead of using identifiers, you can provide explicit terms to translate, according to the following command scheme:
Parametricity Translation <term> [as <name>] [arity <n>].
This defines a new constant containing the parametricity translation of the given term.
To recursively translate everything in a module:
Parametricity Module <module_path>.
When translating terms containing section variables or axioms, it may be useful to declare a term to be the translation of a constant:
Realizer <constant_or_variable> [as <name>] [arity <n>] := <term>.
Note that translating a term or module may lead to proof obligations (for some
fixpoints and opaque terms if you did not import ProofIrrelevence). You need to
declare a tactic to solve such proof obligations:
Parametricity Tactic := <tactic>.
(supports global/export/local attributes like Obligation Tactic)