From the canonical labelling algorithm to permutations, and its specification

IsoGraph.Canon.Algorithm computes with raw Array Nats. This file wraps that up as an honest Equiv.Perm (Fin n) and states the two properties that characterise it.

The wrapper

permOfArrays turns the algorithm's output and its inverse into an Equiv.Perm (Fin n) by checking at run time (in O(n)) that the two arrays really are mutually inverse, falling back to the identity if not. That keeps canonPerm total, and it makes exists_relabel_of_canonAdj_eq below hold for whatever the algorithm returns: canonAdj n adj is the graph adj read through some permutation, hence isomorphic to it.

The specification

Write relabel σ adj for adj with its vertices renamed along σ. Two statements matter.

• Soundness — canonAdj n adjG = canonAdj n adjH → adjG ≅ adjH (exists_relabel_of_canonAdj_eq): a canonical-form comparison never conflates non-isomorphic graphs. The run-time check above is exactly what buys it.

• Invariance — canonAdj n (relabel σ adj) = canonAdj n adj (canonAdj_relabel): the canonical form depends only on the isomorphism class, so anything defined through it descends to the quotient. On raw arrays the same statement is LabellingInvariant, which IsoGraph/Canon/Correct.lean obtains from the soundness and optimality of the search.

Arrays as permutations

def IsoGraph.Canon.finFn (n : ℕ) (a : Array ℕ) (i : Fin n) : Fin n

Read an array of naturals as a function Fin n → Fin n, sending out-of-range entries to themselves.

Equations

• IsoGraph.Canon.finFn n a i = if h : a[↑i]! < n then ⟨a[↑i]!, h⟩ else i

def IsoGraph.Canon.permOfArrays (n : ℕ) (a b : Array ℕ) : Equiv.Perm (Fin n)

Build a permutation of Fin n out of an array and its claimed inverse.

The two arrays are checked (in O(n)) to be mutually inverse, and the identity is returned if they are not. So this is total and needs no facts about the algorithm that produced them; the fallback is unreachable in practice.

Equations

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

def IsoGraph.Canon.invArray (n : ℕ) (a : Array ℕ) : Array ℕ

The inverse of an array-encoded permutation of {0, …, n-1}.

Equations

• IsoGraph.Canon.invArray n a = IsoGraph.Canon.invLab n a

Tabulating an adjacency function

An adjacency function is called far more than n² times by the search below, and for most graphs each call does real work — a scan of an edge list, a comparison of two coordinates, a recursive call under a complement. Filling an n × n array of Bool once and reading it thereafter is therefore worth several times the cost of the fill; CGraph.canonOfArray does exactly that, and CGraph.cache in Cache.lean offers it to the rest of the library.

The shape is forced. Lean maximises the arity of a top-level definition, so a def whose type ends in Fin n → Fin n → Bool and whose body builds a table is compiled with the table inside the two-argument function, and rebuilds it on every query. matLookup is therefore a top-level definition of its own, applied to the array alone: what is passed around is a closure holding the table.

def IsoGraph.Canon.adjArray (n : ℕ) (adj : Fin n → Fin n → Bool) : Array (Array Bool)

The adjacency matrix of adj, as an array of rows.

Equations

• IsoGraph.Canon.adjArray n adj = Array.ofFn fun (i : Fin n) => Array.ofFn fun (j : Fin n) => adj i j

def IsoGraph.Canon.matLookup (n : ℕ) (a : Array (Array Bool)) (i j : Fin n) : Bool

Read the entry of an adjacency matrix at (i, j). Top-level, and meant to be applied to the array alone, for the reason above.

Equations

• IsoGraph.Canon.matLookup n a i j = (a.getD ↑i #[]).getD (↑j) false

@[simp]

theorem IsoGraph.Canon.matLookup_adjArray (n : ℕ) (adj : Fin n → Fin n → Bool) (i j : Fin n) : matLookup n (adjArray n adj) i j = adj i j

theorem IsoGraph.Canon.matLookup_adjArray_eq (n : ℕ) (adj : Fin n → Fin n → Bool) : matLookup n (adjArray n adj) = adj

def IsoGraph.Canon.oracleOfFin (n : ℕ) (adj : Fin n → Fin n → Bool) (v w : ℕ) : Bool

Adjacency oracle on {0, …, n-1} coming from an adjacency function on Fin n.

Equations

• IsoGraph.Canon.oracleOfFin n adj v w = if hv : v < n then if hw : w < n then adj ⟨v, hv⟩ ⟨w, hw⟩ else false else false

def IsoGraph.Canon.canonPerm (n : ℕ) (adj : Fin n → Fin n → Bool) : Equiv.Perm (Fin n)

The canonical labelling of a graph on Fin n: canonical position i holds the vertex canonPerm n adj i.

Equations

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

def IsoGraph.Canon.canonAdj (n : ℕ) (adj : Fin n → Fin n → Bool) : Fin n → Fin n → Bool

The canonical form of a graph on Fin n: the graph relabelled so that its adjacency matrix is the canonical one.

This is the specification, not the way to compute. Lean η-expands every function-typed definition, so each query canonAdj n adj i j re-runs the whole search. To compute, use canonMatrix, whose result is a structure and therefore shares the search across queries.

Equations

• IsoGraph.Canon.canonAdj n adj = fun (i j : Fin n) => adj ((IsoGraph.Canon.canonPerm n adj) i) ((IsoGraph.Canon.canonPerm n adj) j)

def IsoGraph.Canon.finEq {m n : ℕ} (h : m = n) : Fin m ≃ Fin n

Fin m ≃ Fin n from m = n. Unlike Equiv.cast this has a definitional val.

Equations

• IsoGraph.Canon.finEq h = { toFun := fun (i : Fin m) => ⟨↑i, ⋯⟩, invFun := fun (j : Fin n) => ⟨↑j, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem IsoGraph.Canon.finEq_val {m n : ℕ} (h : m = n) (i : Fin m) : ↑((finEq h) i) = ↑i

@[simp]

theorem IsoGraph.Canon.finEq_symm_val {m n : ℕ} (h : m = n) (j : Fin n) : ↑((finEq h).symm j) = ↑j

theorem IsoGraph.Canon.oracleOfFin_apply {n : ℕ} (f : Fin n → Fin n → Bool) {a b : ℕ} (ha : a < n) (hb : b < n) : oracleOfFin n f a b = f ⟨a, ha⟩ ⟨b, hb⟩

theorem IsoGraph.Canon.oracleOfFin_comm {n : ℕ} {f : Fin n → Fin n → Bool} (hf : ∀ (i j : Fin n), f i j = f j i) (a b : ℕ) : oracleOfFin n f a b = oracleOfFin n f b a

theorem IsoGraph.Canon.oracleOfFin_irrefl {n : ℕ} {f : Fin n → Fin n → Bool} (hf : ∀ (i : Fin n), f i i = false) (a : ℕ) : oracleOfFin n f a a = false

Adjacency matrices

The type the canonical form is actually delivered in. Two things are going on:

• it is a structure, not a bare Fin n → Fin n → Bool, because the compiler η-expands every definition whose type is a function type — a def f (x) : Fin n → Fin n → Bool := <search>; fun i j ↦ … re-runs <search> on every single query. One field is enough to block that, and a one-field structure is unboxed at runtime, so the wrapper is free;
• it is indexed by its size, so that "the canonical form of a graph on V" can live in AdjMatrix (Fintype.card V) — a type that does not mention the listing of V used to compute it, which is what makes the quotient lift in IsoGraph.Basic typecheck.

structure IsoGraph.Canon.AdjMatrix (n : ℕ) : Type

The adjacency matrix of a graph on Fin n.

• adj : Fin n → Fin n → Bool

  The adjacency function.

theorem IsoGraph.Canon.AdjMatrix.ext' {n : ℕ} {M N : AdjMatrix n} (h : M.adj = N.adj) : M = N

def IsoGraph.Canon.AdjMatrix.get {n : ℕ} (M : AdjMatrix n) (a b : ℕ) : Bool

Query a matrix at plain naturals; false out of range.

Equations

• M.get a b = IsoGraph.Canon.oracleOfFin n M.adj a b

theorem IsoGraph.Canon.AdjMatrix.get_eq {n : ℕ} (M : AdjMatrix n) {a b : ℕ} (ha : a < n) (hb : b < n) : M.get a b = M.adj ⟨a, ha⟩ ⟨b, hb⟩

def IsoGraph.Canon.AdjMatrix.reindex {n : ℕ} (M : AdjMatrix n) (m : ℕ) : AdjMatrix m

Move a matrix onto the index set Fin m, reading false outside the common range.

This is the one place where an index set of the "wrong" size is tolerated, and it is what lets the canonical form of a graph be stated on Fin (Fintype.card V) while being computed from a listing whose length is only provably that.

Equations

• M.reindex m = { adj := fun (i j : Fin m) => M.get ↑i ↑j }

@[simp]

theorem IsoGraph.Canon.AdjMatrix.reindex_adj {n m : ℕ} (M : AdjMatrix n) (i j : Fin m) : (M.reindex m).adj i j = M.get ↑i ↑j

theorem IsoGraph.Canon.AdjMatrix.reindex_congr {n k m : ℕ} {M : AdjMatrix n} {N : AdjMatrix k} (h : ∀ (a b : ℕ), M.get a b = N.get a b) : M.reindex m = N.reindex m

theorem IsoGraph.Canon.AdjMatrix.get_comm {n : ℕ} {M : AdjMatrix n} (h : ∀ (i j : Fin n), M.adj i j = M.adj j i) (a b : ℕ) : M.get a b = M.get b a

theorem IsoGraph.Canon.AdjMatrix.get_irrefl {n : ℕ} {M : AdjMatrix n} (h : ∀ (i : Fin n), M.adj i i = false) (a : ℕ) : M.get a a = false

theorem IsoGraph.Canon.AdjMatrix.heq_of_adj {m n : ℕ} (h : m = n) {M : AdjMatrix m} {N : AdjMatrix n} (hMN : ∀ (x y : Fin m), M.adj x y = N.adj ((finEq h) x) ((finEq h) y)) : M ≍ N

Matrices of the same size, agreeing pointwise up to the identification of the index sets, are heterogeneously equal.

def IsoGraph.Canon.matrixOfPerm (n : ℕ) (adj : Fin n → Fin n → Bool) (σ : Equiv.Perm (Fin n)) : AdjMatrix n

The graph adj read through the permutation σ, as a matrix.

Equations

• IsoGraph.Canon.matrixOfPerm n adj σ = { adj := fun (i j : Fin n) => adj (σ i) (σ j) }

def IsoGraph.Canon.canonMatrix (n : ℕ) (adj : Fin n → Fin n → Bool) : AdjMatrix n

The canonical form of a graph on Fin n, computed. The search runs once, when this is forced — σ is an argument of matrixOfPerm, so it is evaluated before the closure is built — and each query of the resulting adj is then O(1).

Equations

• IsoGraph.Canon.canonMatrix n adj = IsoGraph.Canon.matrixOfPerm n adj (IsoGraph.Canon.canonPerm n adj)

@[simp]

theorem IsoGraph.Canon.canonMatrix_adj (n : ℕ) (adj : Fin n → Fin n → Bool) : (canonMatrix n adj).adj = canonAdj n adj

theorem IsoGraph.Canon.canonMatrix_get (n : ℕ) (adj : Fin n → Fin n → Bool) (a b : ℕ) : (canonMatrix n adj).get a b = oracleOfFin n (canonAdj n adj) a b

Relabelling

def IsoGraph.Canon.relabel {n : ℕ} (σ : Equiv.Perm (Fin n)) (adj : Fin n → Fin n → Bool) : Fin n → Fin n → Bool

adj with its vertices renamed along σ: the vertex i of relabel σ adj plays the role of the vertex σ i of adj.

Equations

• IsoGraph.Canon.relabel σ adj i j = adj (σ i) (σ j)

@[simp]

theorem IsoGraph.Canon.relabel_apply {n : ℕ} (σ : Equiv.Perm (Fin n)) (adj : Fin n → Fin n → Bool) (i j : Fin n) : relabel σ adj i j = adj (σ i) (σ j)

@[simp]

theorem IsoGraph.Canon.relabel_refl {n : ℕ} (adj : Fin n → Fin n → Bool) : relabel (Equiv.refl (Fin n)) adj = adj

theorem IsoGraph.Canon.relabel_relabel {n : ℕ} (σ τ : Equiv.Perm (Fin n)) (adj : Fin n → Fin n → Bool) : relabel σ (relabel τ adj) = relabel (Equiv.trans σ τ) adj

@[simp]

theorem IsoGraph.Canon.canonAdj_apply {n : ℕ} (adj : Fin n → Fin n → Bool) (i j : Fin n) : canonAdj n adj i j = adj ((canonPerm n adj) i) ((canonPerm n adj) j)

canonAdj is, pointwise, the original adjacency read through canonPerm.

theorem IsoGraph.Canon.canonAdj_eq_relabel {n : ℕ} (adj : Fin n → Fin n → Bool) : canonAdj n adj = relabel (canonPerm n adj) adj

The canonical form is a relabelling of the original graph.

theorem IsoGraph.Canon.canonAdj_comm {n : ℕ} {adj : Fin n → Fin n → Bool} (h : ∀ (i j : Fin n), adj i j = adj j i) (i j : Fin n) : canonAdj n adj i j = canonAdj n adj j i

theorem IsoGraph.Canon.canonAdj_irrefl {n : ℕ} {adj : Fin n → Fin n → Bool} (h : ∀ (i : Fin n), ¬adj i i = true) (i : Fin n) : ¬canonAdj n adj i i = true

Soundness: equal canonical forms come from isomorphic graphs

theorem IsoGraph.Canon.exists_relabel_of_canonAdj_eq {n : ℕ} {adjG adjH : Fin n → Fin n → Bool} (h : canonAdj n adjG = canonAdj n adjH) : ∃ (σ : Equiv.Perm (Fin n)), relabel σ adjG = adjH

Soundness. If two graphs on Fin n have the same canonical form then they are isomorphic — indeed, an explicit isomorphism is produced.

Nothing about the search is needed here. canonAdj n adj is by construction adj read through the permutation canonPerm n adj, and permOfArrays guarantees that this really is a permutation whatever the algorithm returned; so equal canonical forms exhibit the two graphs as relabellings of one common graph.

Invariance

Renaming the vertices of a graph does not change its canonical form: canonAdj_relabel below. Consequently the canonical form depends only on the isomorphism class, and IsoGraph may be Quotient.lifted through it.

The statement is phrased here for Equiv.Perm (Fin n), and comes from two statements about the raw array algorithm, LabellingIsPerm and LabellingInvariant, which mention nothing but Array Nat and canonicalLabellingOfOracle. The Fin/Equiv.Perm wrapper in between — the permOfArrays run-time check, the invArray inverse, the translation between Equiv.Perm (Fin n) and a renaming of {0, …, n-1} — is what this section is about; see IsoGraph/Canon/Equivariance.lean for the groundwork on the other side.

Of the two, LabellingIsPerm is cheap: canonicalLabellingOfOracle verifies it at run time in O(n). LabellingInvariant is where all the work is; it comes from canonical_cert_relabel of IsoGraph/Canon/Correct.lean.

@[reducible, inline]

abbrev IsoGraph.Canon.labelling (m : ℕ) (f : ℕ → ℕ → Bool) : Array ℕ

The labelling the search returns for the oracle f on m vertices: canonical position i holds the vertex labelling m f.

Equations

• IsoGraph.Canon.labelling m f = IsoGraph.Canon.canonicalLabellingOfOracle m f

def IsoGraph.Canon.LabellingIsPerm : Prop

The labelling is a permutation of the vertices. canonicalLabellingOfOracle checks this in O(n) and returns the identity if the check fails, so it holds regardless of what the search does. See labellingIsPerm.

Equations

• IsoGraph.Canon.LabellingIsPerm = ∀ (m : ℕ) (f : ℕ → ℕ → Bool), (IsoGraph.Canon.labelling m f).size = m ∧ IsoGraph.Canon.IsPerm m fun (v : ℕ) => (IsoGraph.Canon.labelling m f)[v]!

def IsoGraph.Canon.LabellingInvariant : Prop

The labelling the search settles on is equivariant.

Renaming the vertices along s and canonicalising gives the same adjacency matrix as canonicalising and not renaming. Note this is weaker than "the labelling itself transforms along s", which is false: the winner is only determined up to an automorphism, and which of several equally-good leaves the search happens to reach does depend on vertex names. What must not depend on them is the matrix read off at the winner, which is what this says.

Equations

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

theorem IsoGraph.Canon.labellingIsPerm : LabellingIsPerm

theorem IsoGraph.Canon.labellingInvariant : LabellingInvariant

The search's answer satisfies the specification BestKey (canonSt_bestKey), which is manifestly an isomorphism invariant, so the certificate it returns does not depend on the vertex names (canonical_cert_relabel); certOf_get reads the adjacency matrix back out of that certificate.

invArray and permOfArrays on a genuine permutation

theorem IsoGraph.Canon.invArray_size (m : ℕ) (a : Array ℕ) : (invArray m a).size = m

theorem IsoGraph.Canon.invArray_apply {m : ℕ} {a : Array ℕ} (h : IsPerm m fun (v : ℕ) => a[v]!) (i : ℕ) (hi : i < m) : (invArray m a)[a[i]!]! = i

On a permutation array, invArray really is the inverse.

theorem IsoGraph.Canon.permOfArrays_val {m : ℕ} {a : Array ℕ} (h : IsPerm m fun (v : ℕ) => a[v]!) (hinv : ∀ i < m, (invArray m a)[a[i]!]! = i) (i : Fin m) : ↑((permOfArrays m a (invArray m a)) i) = a[↑i]!

So the run-time check inside permOfArrays succeeds, and the permutation it returns is the array read literally.

The renaming of {0, …, n-1} induced by a permutation of Fin n

def IsoGraph.Canon.natOfPerm (m : ℕ) (σ : Equiv.Perm (Fin m)) (v : ℕ) : ℕ

σ as a renaming of plain naturals, fixing everything outside the vertex set.

Equations

• IsoGraph.Canon.natOfPerm m σ v = if h : v < m then ↑(σ ⟨v, h⟩) else v

theorem IsoGraph.Canon.natOfPerm_lt {m : ℕ} (σ : Equiv.Perm (Fin m)) {v : ℕ} (hv : v < m) : natOfPerm m σ v = ↑(σ ⟨v, hv⟩)

theorem IsoGraph.Canon.natOfPerm_isPerm (m : ℕ) (σ : Equiv.Perm (Fin m)) : IsPerm m (natOfPerm m σ)

theorem IsoGraph.Canon.oracleOfFin_relabel (m : ℕ) (σ : Equiv.Perm (Fin m)) (adj : Fin m → Fin m → Bool) : oracleOfFin m (relabel σ adj) = fun (v w : ℕ) => oracleOfFin m adj (natOfPerm m σ v) (natOfPerm m σ w)

Relabelling a graph on Fin n is renaming its oracle.

From the array level to Equiv.Perm

theorem IsoGraph.Canon.canonPerm_val {n : ℕ} (hA : LabellingIsPerm) (adj : Fin n → Fin n → Bool) (i : Fin n) : ↑((canonPerm n adj) i) = (labelling n (oracleOfFin n adj))[↑i]!

When the labelling is a permutation, canonPerm is the labelling array read literally.

theorem IsoGraph.Canon.canonAdj_eq_oracle {n : ℕ} (hA : LabellingIsPerm) (adj : Fin n → Fin n → Bool) (i j : Fin n) : canonAdj n adj i j = oracleOfFin n adj (labelling n (oracleOfFin n adj))[↑i]! (labelling n (oracleOfFin n adj))[↑j]!

The canonical form, evaluated: it is the oracle read at the labelling.

theorem IsoGraph.Canon.canonAdj_relabel_of {n : ℕ} (hA : LabellingIsPerm) (hB : LabellingInvariant) (σ : Equiv.Perm (Fin n)) (adj : Fin n → Fin n → Bool) : canonAdj n (relabel σ adj) = canonAdj n adj

Invariance of the canonical form, from the two array-level statements. Nothing else about the algorithm enters.

theorem IsoGraph.Canon.canonAdj_relabel {n : ℕ} (σ : Equiv.Perm (Fin n)) (adj : Fin n → Fin n → Bool) : canonAdj n (relabel σ adj) = canonAdj n adj

Invariance of the canonical form. Renaming the vertices of a graph does not change its canonical form, so the canonical form depends only on the isomorphism class of the graph and anything read off it is a graph invariant.

The labelling is not equivariant: the winner is determined only up to an automorphism, and which of several equally-good leaves the search reaches does depend on the vertex names. What does not depend on them is the adjacency matrix read off at the winner.

theorem IsoGraph.Canon.canonAdj_eq_of_equiv {n : ℕ} {A B : Fin n → Fin n → Bool} (σ : Equiv.Perm (Fin n)) (hσ : ∀ (a b : Fin n), B (σ a) (σ b) = A a b) : canonAdj n A = canonAdj n B

Two adjacency functions related by a permutation have the same canonical form.

theorem IsoGraph.Canon.oracleOfFin_canonAdj_congr {m k : ℕ} (h : m = k) {A : Fin m → Fin m → Bool} {B : Fin k → Fin k → Bool} (σ : Fin m ≃ Fin k) (hσ : ∀ (a b : Fin m), B (σ a) (σ b) = A a b) : oracleOfFin m (canonAdj m A) = oracleOfFin k (canonAdj k B)

The ℕ-indexed form of canonAdj_eq_of_equiv: two adjacency functions, on index sets of the same size, related by a bijection, have the same canonical adjacency oracle.

theorem IsoGraph.Canon.canonMatrix_get_congr {m k : ℕ} (h : m = k) {A : Fin m → Fin m → Bool} {B : Fin k → Fin k → Bool} (σ : Fin m ≃ Fin k) (hσ : ∀ (a b : Fin m), B (σ a) (σ b) = A a b) (a b : ℕ) : (canonMatrix m A).get a b = (canonMatrix k B).get a b

Canonical forms of isomorphic graphs agree entrywise, at the level of plain naturals.

theorem IsoGraph.Canon.canonMatrix_reindex_congr {m k : ℕ} (h : m = k) {A : Fin m → Fin m → Bool} {B : Fin k → Fin k → Bool} (σ : Fin m ≃ Fin k) (hσ : ∀ (a b : Fin m), B (σ a) (σ b) = A a b) (N : ℕ) : (canonMatrix m A).reindex N = (canonMatrix k B).reindex N

Canonical forms of isomorphic graphs, moved onto a common index set, are equal. N is arbitrary, so it may be taken to be Fintype.card V, independently of any listing of the vertices.

theorem IsoGraph.Canon.canonAdj_eq_iff {n : ℕ} {adjG adjH : Fin n → Fin n → Bool} : canonAdj n adjG = canonAdj n adjH ↔ ∃ (σ : Equiv.Perm (Fin n)), relabel σ adjG = adjH

Two graphs on Fin n have the same canonical form exactly when they are isomorphic.

theorem IsoGraph.Canon.canonAdj_congr {m n : ℕ} (h : m = n) {adjG : Fin m → Fin m → Bool} {adjH : Fin n → Fin n → Bool} (σ : Fin m ≃ Fin n) (hσ : ∀ (a b : Fin m), adjH (σ a) (σ b) = adjG a b) (x y : Fin m) : canonAdj m adjG x y = canonAdj n adjH (h ▸ x) (h ▸ y)

The transported form of canonAdj_relabel: graphs on Fin m and Fin n that are isomorphic (so in particular m = n) have the same canonical form.