Equations 1.2beta2 is released!
Release 1.2beta2 of Equations is available, as source and
through opam
(packages coqequations.1.2~beta2+8.8
and
coqequations.1.2~beta2+8.9
for Coq 8.8 and Coq 8.9).
I am pleased to announce release 1.2beta2 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 release contains many fixes and improvements with respect to the 1.2beta version:

A new flag
With Funext
(on by default) can be used to disable the use of functional extensionality in proofs of unfolding lemmas for wellfounded definitions. When off, the automation might fail to prove the extensionality of the functional defined by Equations. The user can then prove the obligation on its own, with the help of theEquations.Init.unfold_recursor
tactic and dependent elimination tactics. After this proof the equations and the elimination principle of the definition are still derived automatically. 
Flags
WithK
andWithKDec
are deprecated in favor of a singleWith UIP
flag (off by default). When set, this flag lets Equations use instances of the classUIP
to simplify patternmatching problems. The user can add a generalUIP
axiomatic instance for all types to allow the generalK
rule if desired. 
Two instances of the library are provided, one using Coq’s standard library equality in
Prop
(default) and another one using a proofrelevant equality inType
, and proofrelevant notion of accessibility. The later can be used by requiringEquations.Type.All
instead ofEquations.Equations
. In this setting, Equations definitions are compatible with the univalence axiom and proofrelevant reasoning in general. Note that extracted programs will keep all the proofrelevant manipulations of equality and accessibility in that case. A branch of Equations compatible with theCoqHoTT
library is also available, but will stay in a beta stage until the release of Coq 8.10. 
Graphs of functions and elimination principles are now defined in
Type
if possible (e.g. if the program does not produce a proposition which might involved casesplitting on other propositions). This allows applying the eliminator in proofrelevant contexts, e.g. when buildingreflect
proofs. 
The
funelim
tactic produces less generated names, but is still fragile with respect to naming. An alternativeapply_funelim
tactic can be used instead of thefunelim
tactic, generating simpler subgoals and leaving introductions to the user, but not generalizing the initial goals by equalities. Similarly to Coq’s builtininduction
tactic, the user must do induction loading explicitely, generalizing the goal by equalities or variables to ensure that subgoals are provable when using this variant. 
The
dependent elimination
tactic should also produce less generated names (prefering a usergiven name in case of unification with a generated one) and is now robust with respect to the presence of letbound variables in the context.
See the reference manual for details on these new features.
– Matthieu Sozeau