The Coq mailing list

[Matthieu Sozeau <matthieu.sozeau AT inria.fr>]

Dear Coq-clubbers,

  We are pleased to announce release 1.0-beta of the Equations

package. Equations is a function definition plugin for Coq (supporting

Coq 8.6 currently), that allows the definition of functions by

dependent pattern-matching and (well-founded) recursion and compiles

them into core terms. This version of Equations is based on a new

simplification engine for dependent equalities appearing in dependent

eliminations that is also usable as a separate tactic, providing an

axiom-free variant of [dependent destruction].  The main features of

Equations include:

  - Dependent pattern-matching in the style of Agda/Epigram, with

    inaccessible patterns, `with` and `where` clauses.  The use of the K

    axiom or a proof of K is configurable.

  - Support for well-founded recursion using `by rec` annotations, and

    automatic derivation of the subterm relation for inductive families.

  

  - Automatic generation of the defining equations as rewrite rules for

    every definition.

  

  - Automatic generation of the unfolding lemma for well-founded

    definitions (requiring only functional extensionality).

  

  - Automatic derivation of the graph of the function and its

    elimination principle.  In case the automation fails to prove these

    principles, the user is asked to provide a proof.

  

  - A new `dependent elimination` tactic based on the same splitting

    tree compilation scheme that can advantageously replace `dependent

    destruction` and sometimes `inversion` as well. The `as` clause of

    `dependent elimination` allows to specify exactly the patterns and

    naming of new variables needed for an elimination.

  

  - A set of `Derive` commands for automatic derivation of constructions

    from an inductive type: its signature, no-confusion property,

    well-founded subterm relation and decidable equality proof.

The current system still has known limitations we will address (see

faq), but is already usable for developing non-toy programs and

proofs. Documentation and examples are available on the website.

We are seeking and welcoming feedback from you on the usage of 

these tools!

Release 1.0-beta of Equations is available as source on github and through `opam` (package `coq-equations.1.0~beta`).

release: https://github.com/mattam82/Coq-Equations/releases/tag/v1.0-beta

www: http://mattam82.github.io/Coq-Equations

faq: http://mattam82.github.io/Coq-Equations/FAQ

issues: http://github.com/mattam82/Coq-Equations/issues

Enjoy!

-- Matthieu Sozeau and Cyprien Mangin