Abstract

ZX-diagrams are typically represented as adjacency-based graphs, reflecting the guiding principle that “only connectivity matters”. In the context of formal theorem provers like Coq, however, such graphs are difficult to reason about, especially when we seek to give them semantics. To address this gap, we build VyZX, a verified library for reasoning about the ZX-calculus, using inductive constructs that arise naturally from category theoretic definitions. One of the issues arising from this representation is that we explicitly encode associativity information that can be an obstacle to reasoning about connectivity. To address this, we present DC⇕AC, a solver to automatically reason about associativity structures built on top of the e-graph solver egg. egg performs equivalence saturation with all possible structural rewrites in an efficient manner. We incorporate egg into VyZX to allow easy rewriting with the rules of the ZX-calculus.

QPL’24 program