Release 1.2beta2 of Equations is available, as source and
coq-equations.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 pattern-matching and structural or well-founded, 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 well-founded 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 the
Equations.Init.unfold_recursortactic and dependent elimination tactics. After this proof the equations and the elimination principle of the definition are still derived automatically.
WithKDecare deprecated in favor of a single
With UIPflag (off by default). When set, this flag lets Equations use instances of the class
UIPto simplify pattern-matching problems. The user can add a general
UIPaxiomatic instance for all types to allow the general
Krule if desired.
Two instances of the library are provided, one using Coq’s standard library equality in
Prop(default) and another one using a proof-relevant equality in
Type, and proof-relevant notion of accessibility. The later can be used by requiring
Equations.Equations. In this setting, Equations definitions are compatible with the univalence axiom and proof-relevant reasoning in general. Note that extracted programs will keep all the proof-relevant manipulations of equality and accessibility in that case. A branch of Equations compatible with the
Coq-HoTTlibrary 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
Typeif possible (e.g. if the program does not produce a proposition which might involved case-splitting on other propositions). This allows applying the eliminator in proof-relevant contexts, e.g. when building
funelimtactic produces less generated names, but is still fragile with respect to naming. An alternative
apply_funelimtactic can be used instead of the
funelimtactic, generating simpler subgoals and leaving introductions to the user, but not generalizing the initial goals by equalities. Similarly to Coq’s built-in
inductiontactic, the user must do induction loading explicitely, generalizing the goal by equalities or variables to ensure that subgoals are provable when using this variant.
dependent eliminationtactic should also produce less generated names (prefering a user-given name in case of unification with a generated one) and is now robust with respect to the presence of let-bound variables in the context.
See the reference manual for details on these new features.
– Matthieu Sozeau