TensorRocq: Enabling diagrammatic reasoning in Rocq

TL;DR

TensorRocq introduces verified tools for diagrammatic reasoning in symmetric monoidal categories, bridging the gap between formal proof assistants and paper proofs through hypergraph representations.

Contribution

It provides a method to convert SMC terms to hypergraphs, enabling automated reasoning and rewriting in proof assistants.

Findings

Developed verified tools for diagrammatic reasoning in Rocq.

Enabled inference of term equivalence and rewriting modulo diagram deformation.

Supported development of SMC theories from generators and relations.

Abstract

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, leveraging 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 occludes the essential connective information, longer proofs filled with uninformative syntactic manipulation. To address the gap between proof assistants and paper proof, 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 these systems. We also enable our tactics to be used in existing verification projects about SMCs which can be given semantics as tensor expressions.