Nominal Sets in Rocq
Fabrício Sanches Paranhos, Daniel Ventura
TL;DR
The paper addresses the challenge of formalizing constructive nominal sets within Rocq, bridging nominal techniques with a dependent type framework. It develops a typeclass-based Rocq formalization of core nominal concepts including freshness, alpha-equivalence, name abstraction, and finitely supported functions, leveraging Rocq's generalized rewriting to reduce setoid boilerplate. Key constructive results are established, notably the Freshness Theorem and the Freshness Condition for Binders, alongside the NameAbstraction construction and bundled finitely supported function definitions. The work sets the stage for alpha-structural reasoning in Rocq, outlining approaches to alpha-structural recursion and induction and discussing future directions for a fully nominal framework in dependent-type systems.
Abstract
Nominal techniques have been praised for their ability to formalize grammars with binding structures closer to their informal developments. At its core, there lies the definition of nominal sets, which capture the notion of name (in)dependence through a simple, and uniform, metatheory based on name permutations. We present a formal constructive development of nominal sets in Rocq (formerly known as Coq), with its main design and project decisions. Furthermore, we formalize the concepts of freshness, nominal alpha-equivalence, name abstraction, and finitely supported functions. Our implementation relies on a type class hierarchy which, combined with Rocq generalized rewriting mechanism, achieves concise definitions and proofs, whilst easing the well-known "setoid hell" scenario. We conclude with a discussion on how to obtain the constructive alpha-structural recursion and induction combinators, towards a nominal framework.