ViCAR: Visualizing Categories with Automated Rewriting in Coq

We present ViCAR, a library for working with monoidal categories in the Coq proof assistant.ViCAR provides definitions for categorical structures that users can instantiate with their own verification projects.Upon verifying relevant coherence conditions, ViCAR gives a set of lemmas and tactics for manipulating categorical structures.We also provide a visualizer that can display any composition and tensor product of morphisms as a string diagram, showing its categorical structure.This enables graphical reasoning and automated rewriting for Coq projects with monoidal structures. IntroductionJust as category theory provides a unifying framework for diverse concepts in mathematics, category theory can be used in formal verification as a basis for generalization.We can abstract away common structural patterns to yield reusable tactics, lemmas, and techniques for proof assistants.Many constructs that appear in program verification resemble symmetric monoidal categories.ViCAR, a library for Visualizing Categories with Automated Rewriting, takes advantage of the shared structure across symmetric monoidal instances to understand and manipulate morphisms in Coq.ViCAR emerged from Vy ZX, an effort to verify the ZX-calculus, a graphical reasoning system for quantum programs [21].The ZX-calculus [7] forms a symmetric monoidal category whose morphisms are the ZX-diagrams which make up the language.ViCAR generalizes the tools developed in VyZX to assist Coq verification for all concrete monoidal categories.ViCAR consists of three parts: typeclasses for categorical structures in Coq, a visualizer to represent morphisms using string diagrams, and a set of tactics for manipulating typeclass instances.Other popular examples of monoidal categories include the calculus of relations and matrices.The former is the category whose objects are types and morphisms are binary relations.The latter has matrices as its morphisms between vector spaces.The similarities between these examples are initially unclear.Reframing each categorically, however, reveals their shared structure and hints at how the verification of one could help another.To explore and justify this claim, we imported or implemented these instances in Coq then applied ViCAR's monoidal category framework.We found that for a well-developed project, we could easily instantiate the relevant categorical definitions.The tactics and visualization gained were valuable and helped project-specific proofs by removing proof and cognitive overhead.We discuss these examples in more detail in Section 6.ViCAR's key contributions are as follows: We define symmetric monoidal categories in Coq, easily instantiable by user-created structures.