TensorRocq: Enabling Diagrammatic Reasoning in Rocq

Symmetric monoidal categories (SMCs) are a common framework for reasoning about computation, focusing on the parallel and sequential compositionality of operations. String diagrams are a ubiquitous and powerful tool for reasoning about equations in SMCs, eliding the fine details of compositionality to focus on connectivity. However, when working with SMCs in a proof assistant, the rigid equational structure of composition obscures the essential connective information, leading to longer proofs filled with syntactic manipulation. To address the gap between proof assistants and paper proofs, we have developed verified tools for diagrammatic reasoning in Rocq, including inferring term equivalence and rewriting modulo the deformation of string diagrams. This is achieved by converting between syntactic representations of SMC terms and hypergraphs with interfaces, while preserving a common tensor semantics. We provide tools to develop simple SMC theories from generators and relations, and perform equational reasoning over these systems. Our tactics can also be used in existing verification projects about symmetric monoidal categories that can be treated as tensors.