Graphical languages are a convenient shorthand to represent computation, with rewrite rules relating one graph to another. In contrast, proof assistants rely heavily on inductive datatypes, particularly when giving semantics to embedded languages. This creates obstacles to formally reasoning about graphical languages, since imposing an inductive structure obfuscates the diagrammatic nature of graphical languages, along with their corresponding equational theories. To address this gap, we present VyZX, a verified library for reasoning about inductively defined graphical languages. These inductive constructs arise naturally from category-theoretic definitions. We developed VyZX to Verify the ZX-calculus, a graphical langauge 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 soundness of the ZX-calculus rewrite rules and apply them in practice using standard proof assistant techniques. We also provide an IDE-integrated visualizer for proof engineers to directly reason about diagrams in graphical form.

翻译：图形化语言是表示计算的便捷速记符号，其重写规则用于关联不同图形。然而，证明助手严重依赖归纳数据类型，尤其在为嵌入式语言赋予语义时。这给图形化语言的形式化推理造成障碍，因为施加归纳结构会模糊图形化语言的图示本质及其对应的等式理论。为填补这一空白，我们提出VyZX——一个用于推理归纳定义图形化语言的验证库。这些归纳构造自然源自范畴论定义。我们开发VyZX用于验证ZX-演算——一种推理量子计算的图形化语言。ZX-演算附带一组保持图形语义解释的图示重写规则。我们展示如何利用VyZX中的归纳图来证明ZX-演算重写规则的可靠性，并通过标准证明助手技术将其应用于实践。我们还提供集成到IDE中的可视化工具，使证明工程师能够直接以图形形式推理图表。