Need help with Coq-Equations?
Click the “chat” button below for chat support from the developer who created it, or find similar developers for support.

About the developer

mattam82
159 Stars 34 Forks GNU Lesser General Public License v2.1 1.4K Commits 54 Opened issues

Description

A function definition package for Coq

Services available

!
?

Need anything else?

Contributors list

No Data

Equations - a function definition plugin.

Build Status DOI Gitter

Copyright 2009-2020 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.

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

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:

Installation

The current development version works with Coq 8.8 (branch 8.8), Coq 8.9 (branch 8.9), Coq 8.10 (branch 8.10), 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 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

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 test-suite or examples:

make examples test-suite

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.

HoTT Variant

The HoTT variant of Equations currently requires a version of Coq master and a modification of the HoTT library which can be built using:

./configure.sh HoTT

This will clone a branch of HoTT and build it in Equations-HoTT, then one can make Equations and its library using:

make

We use cookies. If you continue to browse the site, you agree to the use of cookies. For more information on our use of cookies please see our Privacy Policy.