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):
  • Parametricity in an Impredicative Sort doi:10.4230/LIPIcs.CSL.2012.381

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)