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）是推理计算过程、关注运算平行与顺序组合性的通用框架。弦图作为一种普适且强大的SMC等式推理工具，通过忽略组合性的具体细节来聚焦连接关系。然而，在证明助手中处理SMCs时，组合的严格等式结构会遮蔽关键的连接信息，导致证明冗长且充斥无意义的语法操作。为解决证明助手与纸笔证明之间的鸿沟，我们开发了Rocq中图解推理的验证工具，包括推断项等价性以及基于弦图变形的重写运算。该方法通过在保留共同张量语义的前提下，建立SMC项句法表示与带接口超图之间的转换。我们提供了从生成元和关系构建简单SMC理论及其等式推理系统的工具。同时，相关策略可应用于已有涉及SMCs、并可用张量表达式赋予语义的验证项目。