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通过可视化和自动化功能，能够轻松集成到证明工程师的工作流程中。