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

Canonical row updates and leaf comparison implement lexicographic leaf-row comparison.

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.