Equations - a function definition plugin.
Copyright 2009-2020 Matthieu Sozeau
Copyright 2015-2018 Cyprien Mangin
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 plugin can be used with Coq’s standard logic in
for a proof-irrelevant, erasable interpretation of pattern-matching,
or with a polymorphic logic in
Type or re-using the prelude
of the HoTT/Coq library for a
proof-relevant interpretation. In all cases, the resulting
definitions are axiom-free.
Table of Contents
Try it now in your browser with JSCoq!
A gallery of examples provides more consequent developments using Equations.
Papers and presentations
Equations Reloaded: High-Level Dependently-Typed 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.
This explains the no-confusion principle and strong equivalences used by Equations and Jesper Cockx’s version of dependent pattern-matching 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 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.
This presents an earlier version of the package.
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:
in the toplevel directory, with
ocamlc in 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
sudo and then enter your user account password when prompted.
The HoTT variant of Equations works with the coq-hott library for Coq 8.10 and up.
To install the plugin in an environment where
hoqc is available, simply run:
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
hoqc, one needs to pass the following options:
hoqtop/hoqc -I `coqc -where`/user-contrib/Equations -Q `coqc -where`/user-contrib ""
Then, one can import the plugin in Coq, using:
From Equations Require Import HoTT.All.
subscribe via RSS