def Hex.GraphIso.Nauty.leafRow {n : Nat} (ctx : Ctx n) (lab : Array Nat) (i : Nat) : VSet n

The leaf row of g^lab at position i: entry i of the leaf key's row list.

Equations

• Hex.GraphIso.Nauty.leafRow ctx lab i = ctx.g[lab[i]!]!.permset (Hex.GraphIso.Nauty.invPerm lab)

theorem Hex.GraphIso.Nauty.leafRows_eq_map {n : Nat} (ctx : Ctx n) (lab : Array Nat) : leafRows ctx lab = List.map (leafRow ctx lab) (List.range n)

def Hex.GraphIso.Nauty.ordInt : Ordering → Int

The comparison trichotomy in nauty's Int convention.

Equations

• Hex.GraphIso.Nauty.ordInt Ordering.lt = -1
• Hex.GraphIso.Nauty.ordInt Ordering.eq = 0
• Hex.GraphIso.Nauty.ordInt Ordering.gt = 1

def Hex.GraphIso.Nauty.CanongInv {n : Nat} (ctx : Ctx n) (canong : Array (VSet n)) (canonlab : Array Nat) (samerows : Nat) : Prop

The stored-canonical-graph invariant at samerows: the store has one row per vertex and its first samerows rows are the leaf rows of canonlab.

Equations

• Hex.GraphIso.Nauty.CanongInv ctx canong canonlab samerows = (canong.size = n ∧ ∀ (i : Nat), i < samerows → canong[i]! = Hex.GraphIso.Nauty.leafRow ctx canonlab i)

theorem Hex.GraphIso.Nauty.canongInv_size {n : Nat} {ctx : Ctx n} {canong : Array (VSet n)} {canonlab : Array Nat} {samerows : Nat} (hinv : CanongInv ctx canong canonlab samerows) : canong.size = n

The store size, projected out of the invariant.

theorem Hex.GraphIso.Nauty.canongInv_zero {n : Nat} {ctx : Ctx n} {canong : Array (VSet n)} (canonlab : Array Nat) (hsz : canong.size = n) : CanongInv ctx canong canonlab 0

The invariant with no rows recorded is the size fact alone: the form every fresh install re-seeds.

theorem Hex.GraphIso.Nauty.rows_of_canongInv {n : Nat} {ctx : Ctx n} {canong : Array (VSet n)} {canonlab : Array Nat} (hinv : CanongInv ctx canong canonlab n) : List.map (fun (x : Nat) => canong[x]!) (List.range n) = leafRows ctx canonlab

A store satisfying the invariant at n holds the leaf rows of its incumbent as its row list.

theorem Hex.GraphIso.Nauty.size_updatecan {n : Nat} (ctx : Ctx n) (canong : Array (VSet n)) (lab : Array Nat) (samerows : Nat) : (updatecan ctx canong lab samerows).size = canong.size

theorem Hex.GraphIso.Nauty.getElem!_updatecan {n : Nat} (ctx : Ctx n) (canong : Array (VSet n)) (lab : Array Nat) (samerows j : Nat) : (updatecan ctx canong lab samerows)[j]! = if samerows ≤ j ∧ j < n ∧ j < canong.size then leafRow ctx lab j else canong[j]!

theorem Hex.GraphIso.Nauty.updatecan_inv {n : Nat} {ctx : Ctx n} {canong : Array (VSet n)} {canonlab : Array Nat} {samerows : Nat} (hinv : CanongInv ctx canong canonlab samerows) : CanongInv ctx (updatecan ctx canong canonlab samerows) canonlab n

Under the samerows invariant, updatecan installs exactly the leaf rows of the incumbent.

theorem Hex.GraphIso.Nauty.testcanlab_fst {n : Nat} (ctx : Ctx n) (canong : Array (VSet n)) (lab : Array Nat) : (testcanlab ctx canong lab).fst = ordInt (listCmp VSet.rowCmp (leafRows ctx lab) (List.map (fun (x : Nat) => canong[x]!) (List.range n)))

testcanlab returns the trichotomy of the lexicographic VSet.rowCmp comparison of the leaf rows against the stored rows.

theorem Hex.GraphIso.Nauty.testcanlab_prefix {n : Nat} (ctx : Ctx n) (canong : Array (VSet n)) (lab : Array Nat) (i : Nat) : i < (testcanlab ctx canong lab).snd → leafRow ctx lab i = canong[i]!

The second component of testcanlab is a leading-agreement count: every earlier leaf row agrees with the store.

theorem Hex.GraphIso.Nauty.testcanlab_snd_le {n : Nat} (ctx : Ctx n) (canong : Array (VSet n)) (lab : Array Nat) : (testcanlab ctx canong lab).snd ≤ n

The leading-agreement count never exceeds n.

theorem Hex.GraphIso.Nauty.leafEvent_faithful {n : Nat} {ctx : Ctx n} {canong : Array (VSet n)} {canonlab lab : Array Nat} {samerows : Nat} (hinv : CanongInv ctx canong canonlab samerows) : (testcanlab ctx (updatecan ctx canong canonlab samerows) lab).fst = ordInt (listCmp VSet.rowCmp (leafRows ctx lab) (leafRows ctx canonlab)) ∧ CanongInv ctx (updatecan ctx canong canonlab samerows) canonlab n ∧ CanongInv ctx (updatecan ctx canong canonlab samerows) lab (testcanlab ctx (updatecan ctx canong canonlab samerows) lab).snd

The per-leaf clause for the simulation induction: at a code-tied leaf, processnode updates the store and compares. Under the store invariant, the comparison outcome is the model row comparison of the two leaf keys, and the updated store satisfies the invariant both at n against the incumbent and at the returned prefix length against the fresh leaf, so CanongInv holds again whichever way the leaf resolves.

theorem Hex.GraphIso.Nauty.keyCmp_codes_eq {n : Nat} {cs : List Nat} {r1 r2 : List (VSet n)} : keyCmp { codes := cs, rows := r1 } { codes := cs, rows := r2 } = listCmp VSet.rowCmp r1 r2

On equal code lists the key comparison is the row comparison.