Release 1.0-beta of Equations is available, as source and
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 the 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
Dependent pattern-matching in the style of Agda/Epigram, with inaccessible patterns,
whereclauses. The use of the K axiom or a proof of K is configurable.
Support for well-founded recursion using
by recannotations, 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.
dependent eliminationtactic based on the same splitting tree compilation scheme that can advantageously replace
dependent destructionand sometimes
inversionas well. The
dependent eliminationallows to specify exactly the patterns and naming of new variables needed for an elimination.
A set of
Derivecommands 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 has known limitations we will address (see FAQ), but is already usable for developping non-toy programs and proofs (see examples). Documentation is available on the website. We are seeking and welcoming feedback from you on the usage of these tools!
– Matthieu Sozeau and Cyprien Mangin