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 dots and at).
Top of the page
Last update: 04/08/12