All news
Equations  a function definition plugin.
Copyright 20092020 Matthieu Sozeau matthieu.sozeau@inria.fr
Copyright 20152018 Cyprien Mangin cyprien.mangin@m4x.org
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
patternmatching and (wellfounded) recursion
in Coq. It compiles everything down to
eliminators for inductive types, equality and accessibility,
providing a definitional extension to the Coq kernel.
The plugin can be used with Coq’s standard logic in Prop
for a proofirrelevant, erasable interpretation of patternmatching,
or with a polymorphic logic in Type
or reusing the prelude
of the HoTT/Coq library for a
proofrelevant interpretation. In all cases, the resulting
definitions are axiomfree.
Table of Contents
Live demo
Try it now in your browser with JSCoq!
Documentation

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.
Papers and presentations

Equations Reloaded: HighLevel DependentlyTyped Functional Programming and Proving in Coq. Matthieu Sozeau and Cyprien Mangin. In: Proc. ACM Program. Lang. 3, ICFP, Article 86 (August 2019), 29 pages. DOI, slides.
This presents version 1.2 and above of the package. See Equations Reloaded for associated material, including a VM to run the examples.

Equations for HoTT. Matthieu Sozeau, Talk given at the Homotopy Type Theory 2019 Conference in Pittsburgh, PA, August 2019.
This explains the noconfusion principle and strong equivalences used by Equations and Jesper Cockx’s version of dependent patternmatching in Agda in terms of HoTT.

Equations for Hereditary Substitution in Leivant’s Predicative System F: 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.
This is a case study on a proof of normalization for an hereditary substitution procedure on a variant of System F.

Equations: A Dependent PatternMatching 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.
This presents an earlier version of the package.
Installation
The latest version works with Coq 8.11 (branch 8.11), Coq 8.12 (branch 8.12), and the current Coq master branch (branch master).
See releases for sources and official releases.
Install with OPAM
This package is available on OPAM. Activate the Coq repository if you didn’t do it yet:
opam repo add coqreleased https://coq.inria.fr/opam/released
and run:
opam install coqequations
To get the beta versions of Coq, activate the repository:
opam repo add coqcoredev https://coq.inria.fr/opam/coredev
To get the development version of Equations, activate the repository:
opam repo add coqextradev https://coq.inria.fr/opam/extradev
Install from source
Alternatively, to compile Equations, simply run:
./configure.sh
make
in the toplevel directory, with coqc
and ocamlc
in your path.
Optionally, one can build the testsuite or examples:
make examples testsuite
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 systemwide, 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.
HoTT Variant
The HoTT variant of Equations works with the coqhott library for Coq 8.10 and up.
To install the plugin in an environment where hoqc
is available, simply run:
./configure.sh HoTT
Then you can follow the standard instructions:
make all install
Note that only one of the HoTT variant or the standard variant can be installed
at any given time. To use hoqtop
or hoqc
, one needs to pass the following options:
hoqtop/hoqc I `coqc where`/usercontrib/Equations Q `coqc where`/usercontrib ""
Then, one can import the plugin in Coq, using:
From Equations Require Import HoTT.All.
subscribe via RSS