Equations 1.0 is released!
Release 1.0 of Equations is available, as source and
through opam
(package coqequations.1.0
for Coq 8.6,
coqequations.1.0+8.7
for 8.7 and coqequations.1.0+8.8
for Coq 8.8).
We are pleased to announce release 1.0 of the Equations package. Equations is a function definition plugin for Coq (supporting Coq 8.6 and 8.7), that allows the definition of functions by dependent patternmatching and wellfounded, mutual or nested structural recursion and compiles them into core terms. It automatically derives the clauses equations, the graph of the function and its associated elimination principle.
This version of Equations is based on a new simplification engine for
the dependent equalities appearing in dependent eliminations that is
also usable as a separate tactic, providing an axiomfree variant of
dependent destruction
. The main features of Equations include:

Dependent patternmatching in the style of Agda/Epigram, with inaccessible patterns,
with
andwhere
clauses. The use of the K axiom or a proof of K is configurable. 
Support for wellfounded recursion using
by rec
annotations, and automatic derivation of the subterm relation for inductive families. 
Support for mutual and nested structural recursion using
with
andwhere
auxilliary definitions, allowing to factor multiple uses of the same nested fixpoint definition. It proves the expected elimination principles for mutual and nested definitions. 
Automatic generation of the defining equations as rewrite rules for every definition.

Automatic generation of the unfolding lemma for wellfounded 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 replacedependent destruction
and sometimesinversion
as well. Theas
clause ofdependent 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, noconfusion property, wellfounded subterm relation and decidable equality proof, if applicable.
The current system is usable for developping nontoy programs and proofs (see examples), although it still has some limitations. Documentation is available on the website, including a reference manual with an introduction to the features of the plugin. We are seeking and welcoming feedback from you on the usage of these tools!
– Matthieu Sozeau and Cyprien Mangin