Copyright 2009-2019 Matthieu Sozeau [email protected]
Copyright 2015-2018 Cyprien Mangin [email protected]
Distributed under the terms of the GNU Lesser General Public License Version 2.1 or later (see LICENSE for details).
Equations provides a notation for writing programs by dependent pattern-matching and (well-founded) recursion in Coq. It compiles everything down to eliminators for inductive types, equality and accessibility, providing a definitional extension to the Coq kernel.
-
The reference manual provides an introduction and a summary of the commands and options. This introduction can also be followed interactively with Equations installed: equations_intro.v
-
A gallery of examples provides more consequent developments using Equations.
Two articles describing the system are available:
- Equations Reloaded, Cyprien Mangin and Matthieu Sozeau (March 2019). Submitted.
- Equations: A Dependent Pattern-Matching Compiler Matthieu Sozeau (2010) In: Kaufmann M., Paulson L.C. (eds) Interactive Theorem Proving. ITP 2010. Lecture Notes in Computer Science, vol 6172. Springer, Berlin, Heidelberg.
We did a case study on a proof of normalization for an hereditary substitution procedure:
- Equations for Hereditary Substitution in Leivant's Predicative SystemF: A Case Study Cyprien Mangin and Matthieu Sozeau. In: Proceedings Tenth International Workshop on Logical Frameworks and Meta Languages: Theory and Practice. Volume 185 of EPTCS. May 2015 - LFMTP'15.
The current development version works with Coq 8.8 (branch 8.8), Coq 8.9 (branch 8.9) and the current Coq master branch (branch master).
See releases for sources and official releases.
This package is available on OPAM. Activate the Coq repository if you didn't do it yet:
opam repo add coq-released https://coq.inria.fr/opam/released
and run:
opam install coq-equations
To get the beta versions of Coq, activate the repository:
opam repo add coq-core-dev https://coq.inria.fr/opam/core-dev
To get the development version of Equations, activate the repository:
opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev
Alternatively, to compile Equations, simply run:
coq_makefile -f _CoqProject -o Makefile
make
in the toplevel directory, with coqc and ocamlc in your path.
Then add the paths to your .coqrc:
Add ML Path "/Users/mat/research/coq/equations/src".
Add Rec LoadPath "/Users/mat/research/coq/equations/theories" as Equations.
Or install it:
make install
As usual, you will need to run this command with the appropriate privileges
if the version of Coq you are using is installed system-wide, rather than
in your own directory. E.g. on Ubuntu, you would prefix the command with
sudo and then enter your user account password when prompted.