36.1. Introduction🔗

HexGraphIso computes canonical forms and isomorphisms of finite simple undirected graphs with ordered vertex colours. It implements both dense and sparse nauty 2.9.3 in Lean. Conformance tests compare each implementation with its corresponding C engine, including the search decisions and canonical labels. The Lean theorems prove totality and correctness of the implementations themselves. The nauty canonical labelling algorithm describes the dense algorithm and the rules that differ in sparse nauty.

Import HexGraphIso for both native graph representations, their operations and graph_iso. The computational library does not depend on Mathlib. Import HexGraphIsoTheory for the correspondence theorems and tactic support on Mathlib graphs.

The graph type selects the implementation. Graph and Colored use dense nauty. SparseGraph and Sparse.Colored use sparse nauty. Both provide canonicalization, isomorphism search and automorphism groups. There is no automatic switch based on graph size or density. The sparse examples show the native edge constructor and explain when an explicit conversion is useful.

Within either implementation, two coloured graphs are isomorphic exactly when their canonical forms are equal, by iso_iff_canon_eq or Sparse.iso_iff_canon_eq. The public canonicalization functions execute the search directly, without producing or replaying a certificate. The graph_iso tactic produces kernel proofs: positive goals use a checked transporter, and negative goals use a separating root refinement code or checked canonical-key certificates. The same syntax supports both graph types.

Colours are the general input, but a graph with no colours to speak of should not have to acquire one. The same operations and the same tactic are available on a bare Graph: Graph.canon, Graph.findIso, Graph.isIso and the rest read the one-cell view Graph.singleColor and hand the conclusion back uncoloured, through the single equivalence Graph.isomorphic_singleColor_iff.

The separate nauty-ffi package is available for users who want direct access to the corresponding dense-nauty operations from Lean. It is an unverified native convenience package, not a dependency or part of the verified HexGraphIso library.

structure

Hex.GraphIso.Colored (n k : ℕ) : Type
Hex.GraphIso.Colored (n k : ℕ) : Type

A coloured graph: a simple undirected graph on Fin n together with an ordered onto colouring by Fin k.

Constructor

Hex.GraphIso.Colored.mk

Fields

graph : Hex.Graph n

The underlying simple graph.

coloring : Hex.GraphIso.Coloring n k

The ordered vertex colouring.

def

Hex.GraphIso.canonicalize {n k : ℕ} (G : Hex.GraphIso.Colored n k) :
  Hex.GraphIso.CanonResult n k
Hex.GraphIso.canonicalize {n k : ℕ}
  (G : Hex.GraphIso.Colored n k) :
  Hex.GraphIso.CanonResult n k

Compute the canonical form of a coloured graph together with the label producing it: the checked result of the pinned nauty search. Total; worst-case cost is factorial. Its answer is the one the certificate replay validates (canonicalize_eq_certifyCanon), which is how every theorem below reaches it.

def

Hex.Graph.Isomorphic {n : ℕ} (G H : Hex.Graph n) : Prop
Hex.Graph.Isomorphic {n : ℕ}
  (G H : Hex.Graph n) : Prop

Two graphs are isomorphic when some forward permutation transports one onto the other.