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.

翻译：对称幺半范畴（SMCs）是推理计算过程的通用框架，重点研究操作的并行与顺序组合性。弦图是一种广泛运用的强大工具，用于推理SMCs中的等式，通过省略组合性的精细细节来聚焦于连接关系。然而，在证明助手中处理SMCs时，组合的严格等式结构会遮蔽关键的连接信息，导致证明冗长且充斥着无意义的语法操作。为解决证明助手与纸面证明之间的鸿沟，我们开发了用于Rocq中图表推理的形式化验证工具，包括推断项等价性以及基于弦图形变的模重写。该实现通过在SMC项与带接口超图之间的语法表示转换（同时保持公共的张量语义）达成。我们提供工具以从生成元和关系开发简单的SMC理论，并在这些系统中执行等式推理。此外，我们的策略可应用于现有关于SMCs的验证项目——这些项目可赋予张量表达式语义。