def Hex.GraphIso.Nauty.segN (lab : Array Nat) (lo len : Nat) : List Nat

The labelling segment of len positions from lo, as a list.

Equations

• Hex.GraphIso.Nauty.segN lab lo len = List.map (fun (o : Nat) => lab[lo + o]!) (List.range len)

theorem Hex.GraphIso.Nauty.segN_length (lab : Array Nat) (lo len : Nat) : (segN lab lo len).length = len

theorem Hex.GraphIso.Nauty.segN_zero (lab : Array Nat) (lo : Nat) : segN lab lo 0 = []

theorem Hex.GraphIso.Nauty.segN_cons (lab : Array Nat) (lo len : Nat) : segN lab lo (len + 1) = lab[lo]! :: segN lab (lo + 1) len

Split the first position off a segment.

theorem Hex.GraphIso.Nauty.segN_concat (lab : Array Nat) (lo len : Nat) : segN lab lo (len + 1) = segN lab lo len ++ [lab[lo + len]!]

Split the last position off a segment.

theorem Hex.GraphIso.Nauty.segN_congr {lab lab' : Array Nat} {lo len : Nat} (h : ∀ (o : Nat), o < len → lab[lo + o]! = lab'[lo + o]!) : segN lab lo len = segN lab' lo len

Segments agree when the underlying positions agree.

theorem Hex.GraphIso.Nauty.splitCellLoop_spec {n : Nat} {gRow : VSet n} (k fuel : Nat) (lab : Array Nat) (c1 c2 : Int) : 0 ≤ c1 → c2 < ↑lab.size → c2 + 1 - c1 = ↑k → k + 1 ≤ fuel → (splitCellLoop gRow fuel lab c1 c2).snd.fst = c1 + ↑(List.countP (fun (x : Nat) => gRow.mem x) (segN lab c1.toNat k)) ∧ (splitCellLoop gRow fuel lab c1 c2).snd.snd = c1 + ↑(List.countP (fun (x : Nat) => gRow.mem x) (segN lab c1.toNat k)) - 1 ∧ (splitCellLoop gRow fuel lab c1 c2).fst.size = lab.size ∧ (∀ (j : Nat), ↑j < c1 ∨ c2 < ↑j → (splitCellLoop gRow fuel lab c1 c2).fst[j]! = lab[j]!) ∧ (segN (splitCellLoop gRow fuel lab c1 c2).fst c1.toNat (List.countP (fun (x : Nat) => gRow.mem x) (segN lab c1.toNat k))).Perm (List.filter (fun (x : Nat) => gRow.mem x) (segN lab c1.toNat k)) ∧ (segN (splitCellLoop gRow fuel lab c1 c2).fst (c1.toNat + List.countP (fun (x : Nat) => gRow.mem x) (segN lab c1.toNat k)) (k - List.countP (fun (x : Nat) => gRow.mem x) (segN lab c1.toNat k))).Perm (List.filter (fun (v : Nat) => !gRow.mem v) (segN lab c1.toNat k))

The two-pointer partition, characterized: the final pointers are the adjacency count of the cell multiset, positions outside the cell are untouched, and the two output segments are permutations of the adjacency filters.

def Hex.GraphIso.Nauty.IsCell (ptn : Array Nat) (level a len : Nat) : Prop

A maximal run of the partition at level: len positions from a, open on the inside and closed at both ends.

Equations

• Hex.GraphIso.Nauty.IsCell ptn level a len = (0 < len ∧ (a = 0 ∨ ptn[a - 1]! ≤ level) ∧ (∀ (i : Nat), a ≤ i → i + 1 < a + len → ptn[i]! > level) ∧ ptn[a + len - 1]! ≤ level)

theorem Hex.GraphIso.Nauty.cellEnd_go_interior {ptn : Array Nat} {level : Nat} (fuel j i : Nat) : j ≤ i → i < cellEnd.go ptn level fuel j → ptn[i]! > level

theorem Hex.GraphIso.Nauty.cellEnd_go_end {ptn : Array Nat} {level : Nat} (hend : ptn[ptn.size - 1]! ≤ level) (fuel j : Nat) : j < ptn.size → ptn.size ≤ fuel + j → ptn[cellEnd.go ptn level fuel j]! ≤ level

theorem Hex.GraphIso.Nauty.isCell_cellEnd {ptn : Array Nat} {level a : Nat} (ha : a < ptn.size) (hstart : a = 0 ∨ ptn[a - 1]! ≤ level) (hend : ptn[ptn.size - 1]! ≤ level) : IsCell ptn level a (cellEnd ptn level a + 1 - a)

A cell of the partition, as reported by cellEnd, is a maximal run.

theorem Hex.GraphIso.Nauty.cells_go_isCell {ptn : Array Nat} {level nn : Nat} (hnn : nn ≤ ptn.size) (hend : ptn[ptn.size - 1]! ≤ level) (fuel c1 : Nat) : c1 = 0 ∨ ptn[c1 - 1]! ≤ level → ∀ (p : Nat × Nat), p ∈ cells.go ptn level nn fuel c1 → IsCell ptn level p.fst (p.snd + 1 - p.fst)

theorem Hex.GraphIso.Nauty.cells_isCell {ptn : Array Nat} {level nn : Nat} (hnn : nn ≤ ptn.size) (hend : ptn[ptn.size - 1]! ≤ level) (p : Nat × Nat) : p ∈ cells ptn level nn → IsCell ptn level p.fst (p.snd + 1 - p.fst)

Every cell of the partition list is a maximal run.

def Hex.GraphIso.Nauty.cellsPerm (ptn : Array Nat) (level : Nat) (lab lab' : Array Nat) : Prop

The two labellings agree, as multisets, on every cell of the partition.

Equations

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

theorem Hex.GraphIso.Nauty.cellsPerm_singleton {ptn : Array Nat} {level : Nat} {lab lab' : Array Nat} (h : cellsPerm ptn level lab lab') {a : Nat} (hc : IsCell ptn level a 1) : lab[a]! = lab'[a]!

On singleton cells, cell-equivalent labellings agree exactly.

theorem Hex.GraphIso.Nauty.cellsPerm_set! {ptn : Array Nat} {level : Nat} {lab lab' : Array Nat} {A lenA c : Nat} (hcell : IsCell ptn level A lenA) (hsize : A + lenA ≤ ptn.size) (hcA : A ≤ c) (hc2 : c + 1 < A + lenA) (hL : (segN lab A (c + 1 - A)).Perm (segN lab' A (c + 1 - A))) (hR : (segN lab (c + 1) (A + lenA - (c + 1))).Perm (segN lab' (c + 1) (A + lenA - (c + 1)))) (hout : ∀ (a len : Nat), IsCell ptn level a len → a + len ≤ A ∨ A + lenA ≤ a → (segN lab a len).Perm (segN lab' a len)) : cellsPerm (ptn.set! c level) level lab lab'

Splitting one cell at an interior boundary: the new partition's cells are the two halves of the split cell and the untouched old cells, so cell-contents equivalence follows from equivalence of the halves and of every disjoint old cell.

theorem Hex.GraphIso.Nauty.segN_append (lab : Array Nat) (lo m p : Nat) : segN lab lo (m + p) = segN lab lo m ++ segN lab (lo + m) p

Concatenate adjacent segments.

structure Hex.GraphIso.Nauty.StPerm {n : Nat} (level : Nat) (st st' : RefineSt n) : Prop

Equal position-level fields with cell-multiset-equal labellings, relative to the state's own partition.

• ptn : st'.ptn = st.ptn
• active : st'.active = st.active
• numcells : st'.numcells = st.numcells
• hint : st'.hint = st.hint
• maxpos : st'.maxpos = st.maxpos
• longcode : st'.longcode = st.longcode
• labSize : st'.lab.size = st.lab.size
• cells : cellsPerm st.ptn level st.lab st'.lab

theorem Hex.GraphIso.Nauty.StPerm.eq_setLab {n level : Nat} {st st' : RefineSt n} (h : StPerm level st st') : st' = { lab := st'.lab, ptn := st.ptn, active := st.active, numcells := st.numcells, hint := st.hint, maxpos := st.maxpos, longcode := st.longcode }

A cell-equivalent state is its partner with the labelling swapped out.

theorem Hex.GraphIso.Nauty.trivialSplit_setLab {n : Nat} (level cell1 cell2 : Nat) (c1 c2 : Int) (st : RefineSt n) (X : Array Nat) : trivialSplit level cell1 cell2 c1 c2 { lab := X, ptn := st.ptn, active := st.active, numcells := st.numcells, hint := st.hint, maxpos := st.maxpos, longcode := st.longcode } = have __src := trivialSplit level cell1 cell2 c1 c2 st; { lab := X, ptn := __src.ptn, active := __src.active, numcells := __src.numcells, hint := __src.hint, maxpos := __src.maxpos, longcode := __src.longcode }

The split bookkeeping never reads the labelling, so it commutes with swapping the labelling out.

theorem Hex.GraphIso.Nauty.isCell_disjoint_or_eq {ptn : Array Nat} {level a len a' len' : Nat} (h : IsCell ptn level a len) (h' : IsCell ptn level a' len') : a' + len' ≤ a ∨ a + len ≤ a' ∨ a = a' ∧ len = len'

Two maximal runs either coincide or are disjoint.

theorem Hex.GraphIso.Nauty.trivialCell_perm {n level cell1 cell2 : Nat} {gRow : VSet n} {st st' : RefineSt n} (h : StPerm level st st') (hcell : IsCell st.ptn level cell1 (cell2 + 1 - cell1)) (hc12 : cell1 ≤ cell2) (h2 : cell2 < st.lab.size) (hsz : st.ptn.size = st.lab.size) : StPerm level (trivialCell level gRow cell1 cell2 st) (trivialCell level gRow cell1 cell2 st') ∧ (∀ (q : Nat), q < cell1 ∨ cell2 ≤ q → (trivialCell level gRow cell1 cell2 st).ptn[q]! = st.ptn[q]!) ∧ (trivialCell level gRow cell1 cell2 st).ptn.size = st.ptn.size ∧ (trivialCell level gRow cell1 cell2 st).lab.size = st.lab.size

One trivial-splitter cell preserves cell-contents equivalence: the positional results agree and the labellings stay cell-equivalent for the result's partition.

theorem Hex.GraphIso.Nauty.cells_go_start {ptn : Array Nat} {level nn : Nat} (fuel c1 : Nat) (p : Nat × Nat) : p ∈ cells.go ptn level nn fuel c1 → c1 ≤ p.fst

theorem Hex.GraphIso.Nauty.cells_go_pairwise {ptn : Array Nat} {level nn : Nat} (fuel c1 : Nat) : List.Pairwise (fun (p q : Nat × Nat) => p.snd < q.fst) (cells.go ptn level nn fuel c1)

theorem Hex.GraphIso.Nauty.cells_pairwise {ptn : Array Nat} {level nn : Nat} : List.Pairwise (fun (p q : Nat × Nat) => p.snd < q.fst) (cells ptn level nn)

The partition's cells are listed in strictly increasing position order.

theorem Hex.GraphIso.Nauty.isCell_of_agree {ptn ptn' : Array Nat} {level a len : Nat} (h : IsCell ptn level a len) (hagree : ∀ (q : Nat), a - 1 ≤ q → q ≤ a + len - 1 → ptn'[q]! = ptn[q]!) : IsCell ptn' level a len

A maximal run survives partition edits that avoid its closed neighbourhood.

theorem Hex.GraphIso.Nauty.refineTrivial_go_perm {n level : Nat} {gRow : VSet n} (cs : List (Nat × Nat)) (st st' : RefineSt n) : StPerm level st st' → st.ptn.size = st.lab.size → (∀ (p : Nat × Nat), p ∈ cs → IsCell st.ptn level p.fst (p.snd + 1 - p.fst) ∧ p.snd < st.lab.size) → List.Pairwise (fun (p q : Nat × Nat) => p.snd < q.fst) cs → StPerm level (refineTrivial.go level gRow cs st) (refineTrivial.go level gRow cs st') ∧ (refineTrivial.go level gRow cs st).lab.size = st.lab.size ∧ (refineTrivial.go level gRow cs st).ptn.size = st.ptn.size

theorem Hex.GraphIso.Nauty.refineTrivial_perm {n : Nat} {ctx : Ctx n} {level split1 : Nat} {st st' : RefineSt n} (h : StPerm level st st') (hsz : st.ptn.size = st.lab.size) (hnn : n ≤ st.ptn.size) (hend : st.ptn[st.ptn.size - 1]! ≤ level) (hsplit : IsCell st.ptn level split1 1) : StPerm level (refineTrivial ctx level split1 st) (refineTrivial ctx level split1 st') ∧ (refineTrivial ctx level split1 st).lab.size = st.lab.size ∧ (refineTrivial ctx level split1 st).ptn.size = st.ptn.size

The trivial-splitter pass preserves cell-contents equivalence.

theorem Hex.GraphIso.Nauty.cellsPerm_of_region {ptn ptn' : Array Nat} {level : Nat} {lab lab' : Array Nat} {A lenA : Nat} (hcell : IsCell ptn level A lenA) (hagree : ∀ (q : Nat), q < A ∨ A + lenA - 1 ≤ q → ptn'[q]! = ptn[q]!) (hin : ∀ (x len' : Nat), IsCell ptn' level x len' → A ≤ x → x + len' ≤ A + lenA → (segN lab x len').Perm (segN lab' x len')) (hout : ∀ (x len' : Nat), IsCell ptn level x len' → x + len' ≤ A ∨ A + lenA ≤ x → (segN lab x len').Perm (segN lab' x len')) : cellsPerm ptn' level lab lab'

Cell-contents equivalence after arbitrary partition edits confined to the interior of one old cell: every new cell either lies inside the edited region (equivalence supplied per new cell) or is an untouched old cell.

theorem Hex.GraphIso.Nauty.mem_worksetOf {n : Nat} (lab : Array Nat) (lo hi v : Nat) : (worksetOf n lab lo hi).mem v = (decide (v < n) && (segN lab lo (hi + 1 - lo)).any fun (x : Nat) => x == v)

The splitter set holds exactly the segment's members.

theorem Hex.GraphIso.Nauty.worksetOf_perm {n : Nat} {lab lab' : Array Nat} {lo hi : Nat} (h : (segN lab lo (hi + 1 - lo)).Perm (segN lab' lo (hi + 1 - lo))) : worksetOf n lab lo hi = worksetOf n lab' lo hi

Cell-equivalent segments give the same splitter set.

theorem Hex.GraphIso.Nauty.countsOf_eq_map {n : Nat} (ctx : Ctx n) (lab : Array Nat) (workset : VSet n) (cell1 cell2 : Nat) : countsOf ctx lab workset cell1 cell2 = List.map (fun (v : Nat) => workset.cardInter ctx.g[v]!) (segN lab cell1 (cell2 + 1 - cell1))

The neighbour counts are the segment mapped through the per-vertex count.

theorem Hex.GraphIso.Nauty.foldl_min_le (l : List Nat) (a : Nat) : List.foldl Nat.min a l ≤ a

theorem Hex.GraphIso.Nauty.foldl_min_le_mem (l : List Nat) (a x : Nat) : x ∈ l → List.foldl Nat.min a l ≤ x

theorem Hex.GraphIso.Nauty.foldl_min_choice (l : List Nat) (a : Nat) : List.foldl Nat.min a l = a ∨ List.foldl Nat.min a l ∈ l

theorem Hex.GraphIso.Nauty.foldl_min_headD_perm {l l' : List Nat} (h : l.Perm l') : List.foldl Nat.min (l.headD 0) l = List.foldl Nat.min (l'.headD 0) l'

The running minimum seeded by the head is permutation-invariant.

theorem Hex.GraphIso.Nauty.foldl_max_ge (l : List Nat) (a : Nat) : a ≤ List.foldl Nat.max a l

theorem Hex.GraphIso.Nauty.foldl_max_ge_mem (l : List Nat) (a x : Nat) : x ∈ l → x ≤ List.foldl Nat.max a l

theorem Hex.GraphIso.Nauty.foldl_max_choice (l : List Nat) (a : Nat) : List.foldl Nat.max a l = a ∨ List.foldl Nat.max a l ∈ l

theorem Hex.GraphIso.Nauty.foldl_max_headD_perm {l l' : List Nat} (h : l.Perm l') : List.foldl Nat.max (l.headD 0) l = List.foldl Nat.max (l'.headD 0) l'

The running maximum seeded by the head is permutation-invariant.