Mathematical representations of graphs often resemble adjacency matrices or lists, representations that facilitate whiteboard reasoning and algorithm design. In the realm of proof assistants, inductive representations effectively define semantics for formal reasoning. This highlights a gap where algorithm design and proof assistants require a fundamentally different structure of graphs, particularly for process theories which represent programs using graphs. To address this gap, we present VyZX, a verified library for reasoning about inductively defined graphical languages. These inductive constructs arise naturally from category theory definitions. A key goal for VyZX is to Verify the ZX-calculus, a graphical language for reasoning about quantum computation. The ZX-calculus comes with a collection of diagrammatic rewrite rules that preserve the graph's semantic interpretation. We show how inductive graphs in VyZX are used to prove the correctness of the ZX-calculus rewrite rules and apply them in practice using standard proof assistant techniques. VyZX integrates easily with the proof engineer's workflow through visualization and automation.

翻译：图的数学表示通常类似于邻接矩阵或邻接表，这类表示便于白板推理与算法设计。在证明辅助工具的领域中，归纳表示能有效定义形式化推理所需的语义。这突显出一个鸿沟：算法设计与证明辅助工具需要本质上不同的图结构，尤其对于使用图表示程序的进程理论而言。为弥合此鸿沟，我们提出VyZX——一个用于推理归纳定义图形化语言的已验证库。这些归纳构造天然产生于范畴论的定义。VyZX的一个核心目标是验证ZX演算，这是一种用于量子计算推理的图形化语言。ZX演算附带一组保持图语义解释的图形式重写规则。我们展示了如何利用VyZX中的归纳图来证明ZX演算重写规则的正确性，并借助标准证明辅助技术在实践中应用它们。VyZX通过可视化与自动化功能，能轻松融入证明工程师的工作流程。