We’re looking for a good library for reasoning about graphs in Coq. Some key features with would want to support include: Topological sorting (ideally along with other graph algorithms) Manipulation based on adjacency Merging of adjacent nodes Subgraph pattern recognition Code extraction Preferably, directed and undirected graphs with multi-edges and self-loops Inductive reasoning on graphs

Our goal is to verify aspects of the ZX calculus (https://zxcalculus.com/), which consists of an undirected graph with nodes containing a color and a real number. These graphs can be given a semantics in terms of matrices of complex numbers, provided an evaluation order is imposed (hence the topological sort).

If possible, we would like to use open graphs so our ZX diagrams can have inputs and outputs, but a source and sink node would suffice.

Does anybody know of any Coq libraries that meet some, if not all, of our criteria?



Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.