structure Hex.GraphIso.Nauty.Sparse.Index.Prefix (n : Nat) (lab ptn : Array Nat) (level upto : Nat) (starts ends : Array Nat) : Prop

The cache is correct for all cells starting before upto. Singleton vertices carry the sentinel n; other vertices carry their cell's start.

• starts_size : starts.size = n
• ends_size : ends.size = n
• ends_eq (a len : Nat) : IsCell ptn level a len → a + len ≤ n → a < upto → ends[a]! = a + len - 1
• starts_eq (a len : Nat) : IsCell ptn level a len → a + len ≤ n → a < upto → ∀ (i : Nat), a ≤ i → i < a + len → starts[lab[i]!]! = if len = 1 then n else a

@[reducible, inline]

abbrev Hex.GraphIso.Nauty.Sparse.Index.Valid (n : Nat) (lab ptn : Array Nat) (level : Nat) (starts ends : Array Nat) : Prop

A completed cache describes every bounded cell of the partition.

Equations

• Hex.GraphIso.Nauty.Sparse.Index.Valid n lab ptn level starts ends = Hex.GraphIso.Nauty.Sparse.Index.Prefix n lab ptn level n starts ends

theorem Hex.GraphIso.Nauty.Sparse.Index.Prefix.zero {n : Nat} {lab ptn : Array Nat} {level : Nat} {starts ends : Array Nat} (hs : starts.size = n) (he : ends.size = n) : Prefix n lab ptn level 0 starts ends

theorem Hex.GraphIso.Nauty.Sparse.Index.Prefix.extend {lab ptn starts ends out : Array Nat} {n level first last : Nat} (h : Prefix n lab ptn level first starts ends) (hc : IsCell ptn level first (last + 1 - first)) (hg : first ≤ last) (hb : last < n) (hs : out.size = n) (ho : ∀ (i : Nat), i < n → out[lab[i]!]! = if first ≤ i ∧ i ≤ last then if first < last then first else n else starts[lab[i]!]!) : Prefix n lab ptn level (last + 1) out (ends.set! first last)

Writing one whole cell extends the cache through its last position. Disjoint cells do not share vertices because the labelling is injective.

structure Hex.GraphIso.Nauty.Sparse.Index.Scatter (n : Nat) (lab before after : Array Nat) (first upto value : Nat) : Prop

A partial scatter changes precisely the already traversed positions.

• size : after.size = n
• get (i : Nat) : i < n → after[lab[i]!]! = if first ≤ i ∧ i < upto then value else before[lab[i]!]!

theorem Hex.GraphIso.Nauty.Sparse.Index.Scatter.initial {n : Nat} {lab before : Array Nat} {first value : Nat} (h : before.size = n) : Scatter n lab before before first first value

theorem Hex.GraphIso.Nauty.Sparse.Index.Scatter.step {lab before after : Array Nat} {n first upto value : Nat} (h : Scatter n lab before after first upto value) (hbound : ∀ (i : Nat), i < n → lab[i]! < n) (hinj : ∀ (i j : Nat), i < n → j < n → lab[i]! = lab[j]! → i = j) (hlo : first ≤ upto) (hhi : upto < n) : Scatter n lab before (after.set! lab[upto]! value) first (upto + 1) value