def Hex.GraphIso.atD {α : Type} : List α → Nat → α → α

Indexed list access built for cheap kernel reduction: one bare match per step, no bounds proofs, no Array wrapper.

Equations

• Hex.GraphIso.atD [] x✝¹ x✝ = x✝
• Hex.GraphIso.atD (a :: tail) 0 x✝ = a
• Hex.GraphIso.atD (head :: as) i.succ x✝ = Hex.GraphIso.atD as i x✝

theorem Hex.GraphIso.atD_eq_getElem {α : Type} {d : α} (l : List α) (i : Nat) (h : i < l.length) : atD l i d = l[i]

def Hex.GraphIso.chunkRows : Nat → Nat → List Bool → List (List Bool)

The flat matrix list cut into r rows of m entries.

Equations

• Hex.GraphIso.chunkRows 0 x✝¹ x✝ = []
• Hex.GraphIso.chunkRows r.succ x✝¹ x✝ = List.take x✝¹ x✝ :: Hex.GraphIso.chunkRows r x✝¹ (List.drop x✝¹ x✝)

theorem Hex.GraphIso.atD_chunkRows (m r : Nat) (l : List Bool) (i : Nat) : i < r → atD (chunkRows r m l) i [] = List.take m (List.drop (m * i) l)

theorem Hex.GraphIso.chunkRows_length (m r : Nat) (l : List Bool) : (chunkRows r m l).length = r

theorem Hex.GraphIso.atD_chunk_flat {n : Nat} {l : List Bool} {i j : Nat} (hlen : l.length = n * n) (hi : i < n) (hj : j < n) : atD (atD (chunkRows n n l) i []) j false = l.getD (n * i + j) false

The flat-index read of a chunked literal is the flat read.

theorem Hex.GraphIso.adj_eq_toList_flat {n : Nat} (Gm : Graph n) (i j : Fin n) : Gm.adj i j = Gm.adjMatrix.data.toList.getD (↑i * n + ↑j) false

The flat-list read of an adjacency matrix is the adjacency test.

def Hex.GraphIso.Kernel.checkIso (n : Nat) (flatA flatB : List Bool) (cellsA cellsB pl : List Nat) : Bool

Validate a forward transporter on literal data: flatA/flatB are the flat adjacency lists, cellsA/cellsB the colour values, and pl the transporter images, each identified with the graph it comes from by a hypothesis of Kernel.isIso_of_checkIso.

Equations

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

theorem Hex.GraphIso.Kernel.isIso_of_checkIso {n k : Nat} {G H : Colored n k} {p : Perm n} {LA LB : List Bool} {CA CB PL : List Nat} (hA : G.graph.adjMatrix.data.toList = LA) (hB : H.graph.adjMatrix.data.toList = LB) (hcA : List.map Fin.val G.coloring.cells.toList = CA) (hcB : List.map Fin.val H.coloring.cells.toList = CB) (hp : List.map Fin.val p.vec.toList = PL) (hchk : checkIso n LA LB CA CB PL = true) : IsIso G H p

Equalities identifying the graph data with the literals, plus a literal transporter check, prove that the permutation transports. The kernel evaluates each graph once, into its literal, and the rest of the check runs on literals.

theorem Hex.GraphIso.Kernel.isomorphic_of_checkIso {n k : Nat} {G H : Colored n k} {p : Perm n} {LA LB : List Bool} {CA CB PL : List Nat} (hA : G.graph.adjMatrix.data.toList = LA) (hB : H.graph.adjMatrix.data.toList = LB) (hcA : List.map Fin.val G.coloring.cells.toList = CA) (hcB : List.map Fin.val H.coloring.cells.toList = CB) (hp : List.map Fin.val p.vec.toList = PL) (hchk : checkIso n LA LB CA CB PL = true) : Isomorphic G H

Equalities identifying the graph data with the literals, plus a literal transporter check, prove isomorphism.