Release 1.2beta2 of Equations is available, as source and through opam (packages coq-equations.1.2~beta2+8.8 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_recursor tactic and dependent elimination tactics. After this proof the equations and the elimination principle of the definition are still derived automatically.

  • Flags WithK and WithKDec are deprecated in favor of a single With UIP flag (off by default). When set, this flag lets Equations use instances of the class UIP to simplify pattern-matching problems. The user can add a general UIP axiomatic instance for all types to allow the general K 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 proof-relevant equality in Type, and proof-relevant notion of accessibility. The later can be used by requiring Equations.Type.All instead of 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-HoTT 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 case-splitting on other propositions). This allows applying the eliminator in proof-relevant contexts, e.g. when building reflect proofs.

  • The funelim tactic produces less generated names, but is still fragile with respect to naming. An alternative apply_funelim tactic can be used instead of the funelim tactic, generating simpler subgoals and leaving introductions to the user, but not generalizing the initial goals by equalities. Similarly to Coq’s built-in induction 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 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