Quotients of Bounded Natural Functors

TL;DR

This paper investigates conditions under which quotient types inherit bounded natural functor (BNF) structures in higher-order logic, extending the theory and automating the process in Isabelle/HOL with practical case studies.

Contribution

It identifies sufficient conditions for quotients to inherit BNF structures and introduces an automated command in Isabelle/HOL to facilitate this process.

Findings

Quotients do not always inherit BNF structure with naive lifting.

A more general lifting scheme supports problematic quotients.

Automated command reduces proof effort in Isabelle/HOL.

Abstract

The functorial structure of type constructors is the foundation for many definition and proof principles in higher-order logic (HOL). For example, inductive and coinductive datatypes can be built modularly from bounded natural functors (BNFs), a class of well-behaved type constructors. Composition, fixpoints, and, under certain conditions, subtypes are known to preserve the BNF structure. In this article, we tackle the preservation question for quotients, the last important principle for introducing new types in HOL. We identify sufficient conditions under which a quotient inherits the BNF structure from its underlying type. Surprisingly, lifting the structure in the obvious manner fails for some quotients, a problem that also affects the quotients of polynomial functors used in the Lean proof assistant. We provide a strictly more general lifting scheme that supports such problematic quotients. We extend the Isabelle/HOL proof assistant with a command that automates the registration of a quotient type as a BNF, reducing the proof burden on the user from the full set of BNF axioms to our inheritance conditions. We demonstrate the command's usefulness through several case studies.