一句话：为 Rocq 提供基于字符串图的张量范畴等价推理与重写工具。
在证明助手中处理对称单体范畴（SMC）时，组合的刚性等式结构会掩盖连接信息，导致证明冗长且充满语法操作。作者为 Rocq 开发了经过验证的图示推理工具，通过在 SMC 项的语法表示与带接口超图之间转换，并保持共同的张量语义，支持项等价推断和模字符串图变形的重写。工具还允许从生成元与关系定义简单 SMC 理论，并对这些系统进行等式推理；其策略可复用于已有将 SMC 视为张量的验证项目。
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.
@article{abs-2604-17592,
title = {TensorRocq: Enabling Diagrammatic Reasoning in Rocq},
author = {Ben Caldwell and William Spencer and Aleks Kissinger and Robert Rand},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {OOPSLA2},
year = {2026},
doi = {10.1145/3839532}
}