Equations is a plugin for the Coq proof assistant which provides a notation for defining programs by dependent pattern-matching and structural or well-founded recursion. It additionally derives useful high-level proof principles for demonstrating properties about them, abstracting away from the implementation details of the function and its compiled form. The general design and implementation of the plug-in presented in [Sozeau and Mangin 2019] provides a robust and expressive function definition package as a definitional extension to the Coq kernel. At the core of the system is a new simplifier for dependent equalities based on an original handling of the no-confusion property of constructors.

In this tutorial talk, we will present Eqations’ main features from the user point-of-view. This includes Eqations’ grammar for defining programs by dependent pattern-matching and well- founded recursion, highlighting the treatment of Uniqueness of Identity Proofs and the facilities provided for the definition of well- founded or structurally recursive nested or mutually recursive functions. The package also includes supporting tactics for reason- ing a posteriori on Eqations definitions: an elimination principle tailored to the function definition and a set of rewrite rules cor- responding to its clauses; both allow the development of concise and robust proof scripts involving the definitions. Finally, the de- pendent pattern-matching engine at the core of Eqations is also made available in proof mode through a general purpose depen- dent pattern-matching tactic that is more expressive than current destruction tactics and intro-patterns (destruct, inversion or Ssreflect’s elim and vanilla Coq or Ssreflect intro-patterns). The material presented here is part of lecture notes to be integrated in an upcoming volume of Software Foundations centered on the use of advanced tools in Coq.