A function definition package for Coq
Copyright 2009-2020 Matthieu Sozeau
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.
Try it now in your browser with JSCoq!
A gallery of examples provides more consequent developments using Equations.
Two articles describing the system are available:
Equations Reloaded: High-Level Dependently-Typed Functional Programming and Proving in Coq. Matthieu Sozeau and Cyprien Mangin. 2019. Proc. ACM Program. Lang. 3, ICFP, Article 86 (August 2019), 29 pages. DOI. See Equations Reloaded for associated material, including a VM to run the examples.
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:
See releases for sources and official releases.
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
Alternatively, to compile Equations, simply run:
in the toplevel directory, with
ocamlcin your path.
Optionally, one can build the test-suite or examples:
make examples test-suite
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
sudoand then enter your user account password when prompted.
The HoTT variant of Equations currently requires a version of Coq master and a modification of the HoTT library which can be built using:
This will clone a branch of HoTT and build it in Equations-HoTT, then one can make Equations and its library using: