# CoqParam

CoqParam is the starting point of an implementation of a generator of
"theorems for free" in Coq, based on parametricity theory. For the
moment, it is made up with a tactic and a vernacular command that, given
a closed Coq term and its type, compute:
- the parametricity relation generated by the type;
- a proof that the term satisfies the parametricity relation.

It is a new way to prove some theorems in Coq, like commutation
theorems.

This is a prototype, and lots of things remain to do! In particular, it
would be nice to be able to automatically instantiate the free theorems
with the right parametricity relations to automatically solve Coq goals.

It is mainly developed
by Chantal
Keller at École Polytechnique and INRIA Saclay-Île-de-France
and Marc Lasson at
École Normale Supérieure de Lyon.

## Sources

The source code is distributed under the terms of the GNU Lesser General
Public License, version 3.

Download:
To compile it, please report to the installation instructions available
in the archive.
Top of the page

## Use

The code of the tactic comes with different examples, situated in
the `Examples` directory:
`Example.v` is a sample file presenting how to use the
command and the tatic;
`Church.v` uses the command to show that any parametric
term whose type is the type of Church numerals *is* a Church
numeral;
`Tree.v` uses parametricity to prove the naturality of
multiplication in the tree monad;
`FiniteGroups.v` uses parametricity to prove standard
properties about finite groups;
`Peirce.v` show that Peirce's law is provably not
parametric, and thus independent of Coq.

Top of the page

## Suggestions and bugs report

Do not hesitate to make any suggestion or to report bugs to
Chantal
Keller (remove the anti-spam *dot*s and *at*).
Top of the page

Last update: 04/08/12