Equations 1.2beta is released!
Release 1.2beta of Equations is available, as source and
through opam
(packages coqequations.1.2~beta+8.8
and
coqequations.1.2~beta+8.9
for Coq 8.8 and Coq 8.9).
I am pleased to announce release 1.2beta of the Equations package. Equations is a function definition plugin for Coq, that supports the definition of functions by dependent patternmatching and structural or wellfounded, mutual or nested recursion and compiles them into core Coq terms without axioms. It automatically derives the clauses’ equations, the graph of the function and its associated elimination principle.
This version of Equations is based on an improved simplification
engine for the dependent equalities appearing during dependent
eliminations that is also usable as a separate dependent elimination
tactic, providing an axiomfree variant of dependent destruction
and a
more powerful form of inversion
. Along with bug fixes, this version
introduces a few important changes:

At the syntax level, patterns on the lefthand sides of definitions are now interpreted using Coq’s standard term interpreter, so that they naturally support implicit arguments and notations. Recursive and local notations are also available. Finally one does not have to introduce binders for arguments in the function’s prototype, e.g.:
Equations plus : nat > nat > nat := { 0 + m := m; S n + m := S (n + m) } where "x + y" := (plus x y).

The annotations for recursive programs are now written using a
by
annotation before the program’s clauses, as in:Equations gcd (x y : nat) : nat by wf (x + y) lt := gcd 0 x := x ; gcd x 0 := x ; gcd x y with gt_eq_gt_dec x y := {  inleft (left ygtx) := gcd x (y  x) ;  inleft (right refl) := x ;  inright xgty := gcd (x  y) y }.
The reference manual defines the input syntax precisely.

An homogeneous noconfusion principle on indexed families can be automatically derived for those families whose noconfusion property does not require uniqueness of identity proofs. This includes, e.g.
fin
,vector
and many other indexed data structures (examples: definterp, polynomials). 
Support for nested wellfounded recursion, which naturally express standard patterns of functional programming like the worker/wrapper pattern (example: accumulator).

Mutual wellfounded recursive definitions can be implemented by mixing wellfounded recursion and dependent patternmatching (example: mutualwfrec).

Dependent
where
clauses help incrementally build dependentlytyped values. A notation for patternmatching lambdas, which are elaborated towhere
clauses is also available (example: definterp). 
An experimental refinement mode opens the proof mode to fill the holes of an Equations program, making expected types and contexts of partial definitions easier to see, and lets one seamlessly switch between refinement and proof mode. BEWARE:
abstract
does not work well in that case. The syntax to switch to this mode is currentlyEquations?
. Otherwise, the obligations are generated as for Program. 
A relocatable library of support lemmas allows one to use Equations in the context of HoTTCoq or to benefit from strict propositions (WIP).
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 mutual and nested wellfounded recursion using
by wf
annotations, and automatic derivation of the subterm relation for inductive families. 
Support for mutual and nested structural recursion using
with
andwhere
auxiliary definitions, allowing one 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 the functional extensionality axiom).

Automatic derivation of the graph of the function and its elimination principle.

A new
dependent elimination
tactic based on the same splitting tree compilation scheme that can advantageously replacedependent destruction
andinversion
. Theas
clause ofdependent elimination
can be used to specify exactly the patterns and naming of new variables needed by an elimination. 
A set of
Derive
commands for automatic derivation of constructions from an inductive type: its signature, noconfusion properties, wellfounded subterm relation and decidable equality proof, if applicable.
The current system is usable for developing 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. Feedback is very welcome!
– Matthieu Sozeau