structure Hex.GraphIso.Raw : Type

The non-dependent runtime image of a coloured graph, so elaboration-time meta code can evaluate closed Colored n k terms without knowing n and k at compile time.

• n : Nat

  The number of vertices.

• k : Nat

  The number of colours.

• rows : Array (Nauty.VSet self.n)

  The packed adjacency rows.

• colors : Array Nat

  The colour of each vertex.

@[instance_reducible]

instance Hex.GraphIso.instInhabitedRaw : Inhabited Raw

Equations

• Hex.GraphIso.instInhabitedRaw = { default := { n := 0, k := 0, rows := #[], colors := #[] } }

def Hex.GraphIso.Colored.toRaw {n k : Nat} (G : Colored n k) : Raw

The runtime image of a coloured graph.

Equations

• G.toRaw = { n := n, k := k, rows := Hex.GraphIso.Nauty.rowsOf G, colors := Array.ofFn fun (i : Fin n) => ↑G.coloring.cells[i] }

structure Hex.GraphIso.Tactic.Config : Type

The logical limits of one graph_iso call.

• maxSearchNodes : Nat

  Nodes the compiled search may visit per graph, both for the witness search and for the certificate producer.

• maxCertRecords : Nat

  Certificate records per graph the kernel replays. Exceeding it abandons the certificate route, not the tactic.

• maxKernelSteps : Nat

  Estimated kernel work: checkCost n for a witness, and (records + autom + 2) * checkCost n for a certificate pair. This is the limit that bounds the work the kernel itself does, so it is the one to raise for a goal the elaborator solves but the kernel cannot finish.

def Hex.GraphIso.Tactic.elabGraphIsoConfig (cfg : Lean.Syntax) (init : Config := { }) (logExceptions : Bool := true) : Lean.Elab.Tactic.TacticM Config

Elaborate the (field := value) limits of one graph_iso call.

Equations

• One or more equations did not get rendered due to their size.

def Hex.GraphIso.Tactic.evalColored (e : Lean.Expr) : Lean.MetaM Raw

Evaluate a closed Colored n k expression to its runtime image.

Equations

• One or more equations did not get rendered due to their size.

def Hex.GraphIso.Tactic.rawCanon (r : Raw) : Nauty.RunResult r.n

Run the nauty-compatible canonical search on a runtime graph.

Equations

• One or more equations did not get rendered due to their size.

def Hex.GraphIso.Tactic.rawCheckIso (a b : Raw) (p : Array Nat) : Bool

Check a raw transporter: colour preservation and adjacency transport.

Equations

• One or more equations did not get rendered due to their size.

def Hex.GraphIso.Tactic.rawFindIso (a b : Raw) : Option (Array Nat) × Nat

The untrusted elaboration-time search: compare canonical forms and compose the two canonical labels into a forward transporter. Returns the transporter, or none for non-isomorphic inputs, together with the total node count.

Equations

• One or more equations did not get rendered due to their size.

def Hex.GraphIso.Tactic.permExpr (n : Nat) (p : Array Nat) : Lean.MetaM Lean.Expr

Build the literal Perm n expression (Perm.ofNatArray? n #[...]).getD (Perm.id n).

Equations

• One or more equations did not get rendered due to their size.

def Hex.GraphIso.Tactic.kernelDecideProof (p : Lean.Expr) : Lean.MetaM Lean.Expr

Build of_decide_eq_true (Eq.refl true) : p without reducing decide p in the elaborator: the kernel performs the one decisive evaluation when it checks the ascribed Eq.refl. mkDecideProof evaluates twice, once at elaboration and once at kernel checking, which doubles the cost of every replay.

Equations

• One or more equations did not get rendered due to their size.

def Hex.GraphIso.Tactic.rawFlat (r : Raw) : List Bool

The flat Bool literal of a raw graph's adjacency matrix, in row-major order.

Equations

• Hex.GraphIso.Tactic.rawFlat r = List.flatMap (fun (i : Nat) => List.map (fun (j : Nat) => r.rows[i]!.mem j) (List.range r.n)) (List.range r.n)

def Hex.GraphIso.Tactic.boolListLit (bs : List Bool) : Lean.MetaM Lean.Expr

A List Bool literal expression.

Equations

• Hex.GraphIso.Tactic.boolListLit bs = Lean.Meta.mkListLit (Lean.mkConst `Bool) (List.map (fun (bb : Bool) => Lean.mkConst (if bb = true then `Bool.true else `Bool.false)) bs)

def Hex.GraphIso.Tactic.matrixListSide (e : Lean.Expr) : Lean.MetaM Lean.Expr

The expression e.graph.adjMatrix.data.toList for a coloured graph expression e: the left-hand side of the flat-literal equality.

Equations

• One or more equations did not get rendered due to their size.

def Hex.GraphIso.Tactic.matrixPackedSide (n : Nat) (e : Lean.Expr) : Lean.MetaM Lean.Expr

The expression Kernel.packRows n e.graph.adjMatrix.data.toList: the left-hand side of the packed-rows equality the negative routes replay.

Equations

• Hex.GraphIso.Tactic.matrixPackedSide n e = do let __do_lift ← Hex.GraphIso.Tactic.matrixListSide e Lean.Meta.mkAppM `Hex.GraphIso.Kernel.packRows #[Lean.mkNatLit n, __do_lift]

def Hex.GraphIso.Tactic.rawPackedRows (r : Raw) : Nat

The packed rows of a runtime graph, row v at bits [n * v, n * (v + 1)): the right-hand side of the packed-rows equality.

Equations

• Hex.GraphIso.Tactic.rawPackedRows r = List.foldr (fun (v acc : Nat) => r.rows[v]!.toNat + acc <<< r.n) 0 (List.range r.n)

structure Hex.GraphIso.Tactic.Side : Type

One side of a negative goal: the graph expression, its runtime image, the packed-rows literal, and the proof that the graph's adjacency packs to that literal. Both negative routes replay against these, so each side is evaluated once per call.

• expr : Lean.Expr

  The coloured graph expression.

• raw : Raw

  Its runtime image.

• tie : Lean.Expr

  The proof of Kernel.packRows n expr.graph.adjMatrix.data.toList = lit.

• lit : Lean.Expr

  The packed-rows literal.

def Hex.GraphIso.Tactic.mkSide (e : Lean.Expr) : Lean.MetaM Side

Evaluate a coloured graph expression and prove its packed rows equal to a literal, in one kernel evaluation of the graph's adjacency.

Equations

• One or more equations did not get rendered due to their size.

partial def Hex.GraphIso.Tactic.certNodeExpr : Nauty.CertNode → Lean.MetaM Lean.Expr

Reify a certificate tree as a literal expression.

def Hex.GraphIso.Tactic.keyExpr (K : Kernel.Key) : Lean.Expr

Reify a literal canonical key as an expression.

Equations

• Hex.GraphIso.Tactic.keyExpr K = Lean.mkApp2 (Lean.mkConst `Hex.GraphIso.Kernel.Key.mk) (Lean.toExpr K.codes) (Lean.toExpr K.rows)

def Hex.GraphIso.Tactic.matchGoal? (target : Lean.Expr) : Lean.MetaM (Option (Bool × Lean.Expr × Lean.Expr × Lean.Expr × Lean.Expr))

Match Isomorphic G H (returning (false, n, k, G, H)) or ¬ Isomorphic G H (returning true first). Other goals give none.

Equations

• One or more equations did not get rendered due to their size.

def Hex.GraphIso.Tactic.matchUncoloredGoal? (target : Lean.Expr) : Lean.MetaM (Option (Bool × Lean.Expr × Lean.Expr × Lean.Expr))

Match the uncoloured Graph.Isomorphic G H (returning (false, n, G, H)) or its negation (returning true first). Other goals give none.

Equations

• One or more equations did not get rendered due to their size.

def Hex.GraphIso.Tactic.proveNotIsoRoot? (G H : Side) : Lean.MetaM (Option Lean.Expr)

The root-separator leg of the negative path. When the two root refinement codes already differ (the typical case for irregular pairs) the kernel evaluates one refinement per graph, so this leg is tried first on every negative goal.

Equations

• One or more equations did not get rendered due to their size.

def Hex.GraphIso.Tactic.proveNotIsoCerts (cfg : Config) (G H : Side) : Lean.MetaM (Except Lean.MessageData Lean.Expr)

The certificate leg of the negative path. Compiled code produces one budgeted certificate per side and compares the two canonical keys. The kernel then replays two Boolean Kernel.checkKey calls and one checkDiffL call. When a limit runs out the result names that limit. When the two keys agree this throws, because the goal is then not provable.

Equations

• One or more equations did not get rendered due to their size.

def Hex.GraphIso.Tactic.proveNotIso (cfg : Config) (GE HE : Lean.Expr) : Lean.MetaM Lean.Expr

Produce a proof of ¬ Isomorphic G H for closed executable coloured graphs: the root separator first, then certificate replay. The certificates replay only because every declaration they reach is exposed across module boundaries, which HexGraphIso.ModuleBoundaryTests checks. Both the Colored negative branch and downstream extensions use this: HexGraphIsoMathlib calls it on the encoded graphs.

Equations

• One or more equations did not get rendered due to their size.

def Hex.GraphIso.Tactic.proveIsIso (cfg : Config) (n : Nat) (GE HE : Lean.Expr) (a b : Raw) (p : Array Nat) (nodes : Nat) : Lean.MetaM (Lean.Expr × Lean.Expr)

The witness leg of the positive path: prove each side's adjacency, its colouring and the transporter equal to literals, then check the transporter on those literals. Returns the permutation expression and the proof of IsIso G H p. The Colored branch wraps that proof as Isomorphic, and downstream extensions decode it.

Equations

• One or more equations did not get rendered due to their size.

structure Hex.GraphIso.Tactic.Extension : Type

A graph_iso goal handler contributed by a downstream library. A public meta def of this type tagged @[graph_iso_extension] extends the same graph_iso syntax to that library's goal shapes.

• prove? : Config → Lean.Expr → Lean.MetaM (Option Lean.Expr)

  Handle a goal, returning its proof term, or none when the goal shape is not this extension's.

opaque Hex.GraphIso.Tactic.extensionExt : Lean.SimplePersistentEnvExtension Lean.Name (Array Lean.Name)

The registered graph_iso extensions, in declaration order.

def Hex.GraphIso.Tactic.extensions : Lean.MetaM (List Extension)

All extensions present in the current environment, in lookup order.

Equations

• One or more equations did not get rendered due to their size.

def Hex.GraphIso.Tactic.proveGraphIso (cfg : Config) (target : Lean.Expr) (parsed : Bool × Lean.Expr × Lean.Expr × Lean.Expr × Lean.Expr) : Lean.MetaM Lean.Expr

Prove a graph_iso goal over executable coloured graphs.

Equations

• One or more equations did not get rendered due to their size.

def Hex.GraphIso.Tactic.proveGraphIsoUncolored (cfg : Config) (target : Lean.Expr) (parsed : Bool × Lean.Expr × Lean.Expr × Lean.Expr) : Lean.MetaM Lean.Expr

Prove a graph_iso goal over executable uncoloured graphs: colour every vertex alike, hand the pair to proveGraphIso, and transport the conclusion back through Graph.isomorphic_singleColor_iff. Both directions of that equivalence are proof terms, so the uncoloured route costs the kernel nothing beyond the coloured goal's replay and the one 0 < n decision.

Equations

• One or more equations did not get rendered due to their size.

def Hex.GraphIso.graphIsoTac : Lean.ParserDescr

Close a closed Isomorphic or ¬ Isomorphic goal over executable graphs, coloured (Colored n k) or uncoloured (Graph n).

Three logical limits are optional and may appear in any order:

graph_iso (maxSearchNodes := 200000) (maxCertRecords := 200000)
  (maxKernelSteps := 10000000)

They default to 100000, 100000, and 5000000. Importing HexGraphIsoMathlib extends this same tactic to Mathlib SimpleGraph goals. See the module docstring for the proof routes.

Equations

• One or more equations did not get rendered due to their size.

def Hex.GraphIso.evalGraphIsoTac : Lean.Elab.Tactic.Tactic

Elaborator for graph_iso: parse the optional limits, then dispatch to proveGraphIso on the core Colored goal shapes, proveGraphIsoUncolored on the Graph shapes, and then each registered Extension in turn.

Equations

• One or more equations did not get rendered due to their size.