def Hex.GraphIso.Nauty.adjBit {n k : Nat} (G : Colored n k) (i j : Nat) : Bool

The Boolean adjacency test underlying rowOf.

Equations

• Hex.GraphIso.Nauty.adjBit G i j = if h : i < n ∧ j < n then G.graph.adj ⟨i, ⋯⟩ ⟨j, ⋯⟩ else false

theorem Hex.GraphIso.Nauty.mem_rowOf_lt {n k : Nat} (G : Colored n k) {i t : Nat} (hi : i < n) (ht : t < n) : (rowOf G i).mem t = G.graph.adj ⟨i, hi⟩ ⟨t, ht⟩

theorem Hex.GraphIso.Nauty.size_rowsOf {n k : Nat} (G : Colored n k) : (rowsOf G).size = n

theorem Hex.GraphIso.Nauty.getElem!_rowsOf {n k : Nat} (G : Colored n k) {i : Nat} (hi : i < n) : (rowsOf G)[i]! = rowOf G i

def Hex.GraphIso.Nauty.renamingOf {n : Nat} (p : Perm n) : Renaming n

The vertex renaming of a permutation: p.get below n, the identity above.

Equations

• Hex.GraphIso.Nauty.renamingOf p = { toFun := fun (v : Nat) => if h : v < n then ↑(p.get ⟨v, h⟩) else v, inj := ⋯, maps := ⋯ }

theorem Hex.GraphIso.Nauty.renamingOf_lt {n : Nat} (p : Perm n) {v : Nat} (hv : v < n) : (renamingOf p).toFun v = ↑(p.get ⟨v, hv⟩)

theorem Hex.GraphIso.Nauty.rowsMap_of_isIso {n k : Nat} {G H : Colored n k} {p : Perm n} (h : IsIso G H p) : RowsMap (renamingOf p) (rowsOf G) (rowsOf H)

theorem Hex.GraphIso.Nauty.nodup_map_of_inj {f : Nat → Nat} (hf : ∀ (a b : Nat), f a = f b → a = b) {l : List Nat} : l.Nodup → (List.map f l).Nodup

theorem Hex.GraphIso.Nauty.mem_colorClass {n k : Nat} {G : Colored n k} {c v : Nat} : v ∈ colorClass G c ↔ ∃ (hv : v < n), ∃ (hc : c < k), G.coloring.cells[⟨v, hv⟩] = ⟨c, hc⟩

theorem Hex.GraphIso.Nauty.nodup_colorClass {n k : Nat} (G : Colored n k) (c : Nat) : (colorClass G c).Nodup

theorem Hex.GraphIso.Nauty.colorClass_perm {n k : Nat} {G H : Colored n k} {p : Perm n} (h : IsIso G H p) (c : Nat) : (colorClass H c).Perm (List.map (renamingOf p).toFun (colorClass G c))

theorem Hex.GraphIso.Nauty.length_colorClass_eq {n k : Nat} {G H : Colored n k} {p : Perm n} (h : IsIso G H p) (c : Nat) : (colorClass H c).length = (colorClass G c).length

theorem Hex.GraphIso.Nauty.flatMap_filter_key_perm (key : Nat → Nat) (K : Nat) (l : List Nat) : (∀ (v : Nat), v ∈ l → key v < K) → (List.flatMap id (List.map (fun (c : Nat) => List.filter (fun (v : Nat) => key v == c) l) (List.range K))).Perm l

def Hex.GraphIso.Nauty.keyOf {n k : Nat} (G : Colored n k) (v : Nat) : Nat

The colour of a vertex, as a plain Nat.

Equations

• Hex.GraphIso.Nauty.keyOf G v = if h : v < n then ↑G.coloring.cells[⟨v, h⟩] else 0

theorem Hex.GraphIso.Nauty.colorClass_eq_key {n k : Nat} {G : Colored n k} {c : Nat} (hc : c < k) : colorClass G c = List.filter (fun (v : Nat) => keyOf G v == c) (List.range n)

theorem Hex.GraphIso.Nauty.flatten_classes_perm {n k : Nat} (G : Colored n k) : (List.flatMap id (List.map (colorClass G) (List.range k))).Perm (List.range n)

theorem Hex.GraphIso.Nauty.initialPartition_fst {n k : Nat} (G : Colored n k) : (initialPartition G).fst = (List.flatMap id (List.map (colorClass G) (List.range k))).toArray

theorem Hex.GraphIso.Nauty.size_initialPartition {n k : Nat} (G : Colored n k) : (initialPartition G).fst.size = n

theorem Hex.GraphIso.Nauty.labOk_initialPartition {n k : Nat} (G : Colored n k) : LabOk (initialPartition G).fst n

theorem Hex.GraphIso.Nauty.foldl_ends_congr (cls cls' : List (List Nat)) (acc : List Nat × Nat) : List.map List.length cls = List.map List.length cls' → List.foldl (fun (acc : List Nat × Nat) (cl : List Nat) => if cl.isEmpty = true then acc else ((acc.snd + cl.length - 1) :: acc.fst, acc.snd + cl.length)) acc cls = List.foldl (fun (acc : List Nat × Nat) (cl : List Nat) => if cl.isEmpty = true then acc else ((acc.snd + cl.length - 1) :: acc.fst, acc.snd + cl.length)) acc cls'

theorem Hex.GraphIso.Nauty.initialPartition_snd {n k : Nat} (G : Colored n k) : (initialPartition G).snd = (List.foldl (fun (acc : List Nat × Nat) (cl : List Nat) => if cl.isEmpty = true then acc else ((acc.snd + cl.length - 1) :: acc.fst, acc.snd + cl.length)) ([], 0) (List.map (colorClass G) (List.range k))).fst.reverse

theorem Hex.GraphIso.Nauty.cellEnds_eq {n k : Nat} {G H : Colored n k} {p : Perm n} (h : IsIso G H p) : (initialPartition H).snd = (initialPartition G).snd

def Hex.GraphIso.Nauty.totalOf (cls : List (List Nat)) : Nat

Total number of vertices across a list of classes.

Equations

• Hex.GraphIso.Nauty.totalOf cls = (List.map List.length cls).sum

theorem Hex.GraphIso.Nauty.totalOf_nil : totalOf [] = 0

theorem Hex.GraphIso.Nauty.totalOf_cons (cl : List Nat) (cls : List (List Nat)) : totalOf (cl :: cls) = cl.length + totalOf cls

def Hex.GraphIso.Nauty.endsOf : List (List Nat) → Nat → List Nat

The recorded cell end positions of a list of classes laid out from offset s: one entry per nonempty class.

Equations

• Hex.GraphIso.Nauty.endsOf [] x✝ = []
• Hex.GraphIso.Nauty.endsOf (cl :: cls) x✝ = if cl.isEmpty = true then Hex.GraphIso.Nauty.endsOf cls x✝ else (x✝ + cl.length - 1) :: Hex.GraphIso.Nauty.endsOf cls (x✝ + cl.length)

theorem Hex.GraphIso.Nauty.foldl_ends_eq (cls : List (List Nat)) (acc : List Nat) (s : Nat) : List.foldl (fun (acc : List Nat × Nat) (cl : List Nat) => if cl.isEmpty = true then acc else ((acc.snd + cl.length - 1) :: acc.fst, acc.snd + cl.length)) (acc, s) cls = ((endsOf cls s).reverse ++ acc, s + totalOf cls)

theorem Hex.GraphIso.Nauty.initialPartition_snd_eq {n k : Nat} (G : Colored n k) : (initialPartition G).snd = endsOf (List.map (colorClass G) (List.range k)) 0

theorem Hex.GraphIso.Nauty.totalOf_classes {n k : Nat} (G : Colored n k) : totalOf (List.map (colorClass G) (List.range k)) = n

theorem Hex.GraphIso.Nauty.endsOf_ge (cls : List (List Nat)) (s e : Nat) : e ∈ endsOf cls s → s ≤ e

theorem Hex.GraphIso.Nauty.endsOf_lt (cls : List (List Nat)) (s e : Nat) : e ∈ endsOf cls s → e < s + totalOf cls

theorem Hex.GraphIso.Nauty.endsOf_last_mem (cls : List (List Nat)) (s : Nat) : 0 < totalOf cls → s + totalOf cls - 1 ∈ endsOf cls s

theorem Hex.GraphIso.Nauty.size_foldl_set0 (ends : List Nat) (a : Array Nat) : (List.foldl (fun (ptn : Array Nat) (e : Nat) => ptn.set! e 0) a ends).size = a.size

theorem Hex.GraphIso.Nauty.size_initPtn (n inf : Nat) (ends : List Nat) : (initPtn n inf ends).size = n

theorem Hex.GraphIso.Nauty.getElem!_foldl_set0 (ends : List Nat) (a : Array Nat) (q : Nat) : (List.foldl (fun (ptn : Array Nat) (e : Nat) => ptn.set! e 0) a ends)[q]! = if q ∈ ends ∧ q < a.size then 0 else a[q]!

theorem Hex.GraphIso.Nauty.getElem!_initPtn (n inf : Nat) (ends : List Nat) (q : Nat) : (initPtn n inf ends)[q]! = if q ∈ ends ∧ q < n then 0 else if q < n then inf else 0

theorem Hex.GraphIso.Nauty.mem_foldl_active {n : Nat} (ends : List Nat) (acc : VSet n × Nat) (w : Nat) : (List.foldl (fun (p : VSet n × Nat) (e : Nat) => (p.fst.insert p.snd, e + 1)) acc ends).fst.mem w = true → acc.fst.mem w = true ∨ w = acc.snd ∨ ∃ (e : Nat), e ∈ ends ∧ w = e + 1

theorem Hex.GraphIso.Nauty.endsOf_pairwise (cls : List (List Nat)) (s : Nat) : List.Pairwise (fun (x1 x2 : Nat) => x1 < x2) (endsOf cls s)

theorem Hex.GraphIso.Nauty.cell_align (cls : List (List Nat)) (s a len : Nat) : 1 ≤ len → a = s ∨ 1 ≤ a ∧ a - 1 ∈ endsOf cls s → a + len - 1 ∈ endsOf cls s → (∀ (q : Nat), a ≤ q → q < a + len - 1 → ¬q ∈ endsOf cls s) → ∃ (pre : List (List Nat)), ∃ (cl : List Nat), ∃ (suf : List (List Nat)), cls = pre ++ cl :: suf ∧ cl.isEmpty = false ∧ a = s + totalOf pre ∧ len = cl.length

theorem Hex.GraphIso.Nauty.getElem!_append_middle {α : Type} [Inhabited α] (l₁ : List α) (c : α) (rest : List α) : (l₁ ++ c :: rest)[l₁.length]! = c

theorem Hex.GraphIso.Nauty.segN_toArray_middle (cl l₁ l₂ : List Nat) : segN (l₁ ++ cl ++ l₂).toArray l₁.length cl.length = cl

theorem Hex.GraphIso.Nauty.segN_flatten (pre : List (List Nat)) (cl : List Nat) (suf : List (List Nat)) : segN (List.flatMap id (pre ++ cl :: suf)).toArray (totalOf pre) cl.length = cl

theorem Hex.GraphIso.Nauty.segN_map_of_le (f : Nat → Nat) (arr : Array Nat) (lo len : Nat) (h : lo + len ≤ arr.size) : segN (Array.map f arr) lo len = List.map f (segN arr lo len)

theorem Hex.GraphIso.Nauty.initial_cellsPerm {n k : Nat} {G H : Colored n k} {p : Perm n} (h : IsIso G H p) (hn0 : 0 < n) : cellsPerm (initPtn n (n + 2) (initialPartition G).snd) 1 (initialPartition H).fst (Array.map (renamingOf p).toFun (initialPartition G).fst)

theorem Hex.GraphIso.Nauty.labOk_map_renaming {n k : Nat} (G : Colored n k) (p : Perm n) : LabOk (Array.map (renamingOf p).toFun (initialPartition G).fst) n

theorem Hex.GraphIso.Nauty.canonSpecKey_eq_of_isIso {n k : Nat} {G H : Colored n k} {p : Perm n} (h : IsIso G H p) : canonSpecKey H = canonSpecKey G

Isomorphic coloured graphs have the same nauty-semantic canonical key.

theorem Hex.GraphIso.Nauty.canonSpecKey_eq_of_isomorphic {n k : Nat} {G H : Colored n k} (h : Isomorphic G H) : canonSpecKey G = canonSpecKey H

Isomorphic coloured graphs have equal nauty-semantic canonical keys.