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）集成的可视化工具，使证明工程师能够直接以图形形式对图表进行推理。