Equations - a function definition plugin.
Copyright 2009-2019 Matthieu Sozeau
Copyright 2015-2018 Cyprien Mangin
Distributed under the terms of the GNU Lesser General Public License Version 2.1 (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.
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.
See releases for sources and official releases.
Install with OPAM
opam repo add coq-released https://coq.inria.fr/opam/released
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
Install from source
Alternatively, to compile Equations, simply run:
coq_makefile -f _CoqProject -o Makefile make
in the toplevel directory, with
ocamlc in your path.
Then add the paths to your
Add ML Path "/Users/mat/research/coq/equations/src". Add Rec LoadPath "/Users/mat/research/coq/equations/theories" as Equations.
Or install it:
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.