32.1. Introduction🔗

HexGraphIso computes canonical forms and isomorphisms of finite simple undirected graphs with ordered vertex colours. The canonical labelling algorithm used in HexGraphIso is an exact translation of the nauty 2.9.3 algorithm into Lean. (We use conformance testing, rather than a theorem, to ensure they are identical, and prove our theorems about the Lean translation.) The exact algorithm, including the output-relevant choices absent from the published literature, is specified in The nauty canonical labelling algorithm. The public names (canonicalize, canon, label, isIso) run that translation directly, and the theorems reach them because a proven certificate checker is shown to accept the translation's answer on every input. Two coloured graphs are isomorphic exactly when their canonical forms are equal (iso_iff_canon_eq), and the graph_iso tactic closes both positive and negative isomorphism goals with the kernel performing the decisive replay: positive goals through the checked transporter, negative goals through the root refinement code when it separates the two graphs and through a checked canonical-key certificate otherwise.

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.

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

Hex.GraphIso.Colored.mk

graph : Hex.Graph n

coloring : Hex.GraphIso.Coloring n k

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

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