Harvested automorphisms, and how they act on the search tree

When two leaves of the search tree carry the same certificate, the algorithm records the permutation autoOf that carries one labelling to the other and uses it to prune: any child of the current node that is in the orbit of an already-processed child can be skipped.

This file proves the two facts that pruning rests on:

• autoOf_isAuto — the recorded permutation really is an automorphism;
• reach_child_auto — an automorphism fixing the current partition carries the subtree below one child bijectively onto the subtree below its image, with the same leaf keys, so skipping the image loses nothing.

The bridge between the two is ofOracle_congr: an automorphism γ of G satisfies Graph.ofOracle n (f ∘ γ) = Graph.ofOracle n f, which turns every equivariance lemma of IsoGraph.Canon.Equivariance into a statement about the action of Aut G on the tree.

autoOf really produces an automorphism

structure IsoGraph.Canon.PermArr (n : ℕ) (a : Array ℕ) : Prop

A PermArr n a is an array that represents a permutation of {0, …, n-1}: the shape the labelling of a leaf always has (LeafOk).

• size : a.size = n

  It has the right length.

• lt (i : ℕ) : i < n → a[i]! < n

  Its entries are vertices.

• inj (i : ℕ) : i < n → ∀ j < n, a[i]! = a[j]! → i = j

  Its entries are distinct.

theorem IsoGraph.Canon.PermArr.isPerm {n : ℕ} {a : Array ℕ} (h : PermArr n a) : IsPerm n fun (i : ℕ) => a[i]!

The function view of a permutation array.

theorem IsoGraph.Canon.PermArr.surj {n : ℕ} {a : Array ℕ} (h : PermArr n a) {w : ℕ} (hw : w < n) : ∃ i < n, a[i]! = w

theorem IsoGraph.Canon.autoOf_foldl_size (σ τ : Array ℕ) (l : List ℕ) (b : Array ℕ) : (List.foldl (fun (g : Array ℕ) (i : ℕ) => g.set! σ[i]! τ[i]!) b l).size = b.size

theorem IsoGraph.Canon.autoOf_foldl_unchanged (σ τ : Array ℕ) (l : List ℕ) (b : Array ℕ) (x : ℕ) (h : ∀ i ∈ l, σ[i]! ≠ x) : (List.foldl (fun (g : Array ℕ) (i : ℕ) => g.set! σ[i]! τ[i]!) b l)[x]! = b[x]!

theorem IsoGraph.Canon.autoOf_foldl_get (n : ℕ) (σ τ : Array ℕ) (l : List ℕ) (hnd : l.Nodup) (hinj : ∀ i ∈ l, ∀ j ∈ l, σ[i]! = σ[j]! → i = j) (b : Array ℕ) (hb : b.size = n) (i : ℕ) (hi : i ∈ l) (hσi : σ[i]! < n) : (List.foldl (fun (g : Array ℕ) (i : ℕ) => g.set! σ[i]! τ[i]!) b l)[σ[i]!]! = τ[i]!

theorem IsoGraph.Canon.autoOf_get {n : ℕ} {σ τ : Array ℕ} (hσ : PermArr n σ) {i : ℕ} (hi : i < n) : (autoOf n σ τ)[σ[i]!]! = τ[i]!

Reading autoOf back: it sends the vertex at position i of σ to the one at position i of τ.

theorem IsoGraph.Canon.autoOf_size (n : ℕ) (σ τ : Array ℕ) : (autoOf n σ τ).size = n

theorem IsoGraph.Canon.autoOf_permArr {n : ℕ} {σ τ : Array ℕ} (hσ : PermArr n σ) (hτ : PermArr n τ) : PermArr n (autoOf n σ τ)

autoOf of two permutation arrays is a permutation array.

theorem IsoGraph.Canon.autoOf_auto {n : ℕ} {f : ℕ → ℕ → Bool} {σ τ : Array ℕ} (hσ : PermArr n σ) (hτ : PermArr n τ) (hcert : certOf (Graph.ofOracle n f) σ = certOf (Graph.ofOracle n f) τ) {u v : ℕ} (hu : u < n) (hv : v < n) : f (autoOf n σ τ)[u]! (autoOf n σ τ)[v]! = f u v

Automorphism harvesting is correct. Two leaf labellings with the same certificate differ by an automorphism, and autoOf computes it.

Automorphisms act on the search tree

theorem IsoGraph.Canon.ofOracle_congr {n : ℕ} {f f' : ℕ → ℕ → Bool} (h : ∀ a < n, ∀ b < n, f a b = f' a b) : Graph.ofOracle n f = Graph.ofOracle n f'

Oracles that agree on {0, …, n-1} build the same graph.

theorem IsoGraph.Canon.reach_congr {n : ℕ} {f f' : ℕ → ℕ → Bool} (h : ∀ a < n, ∀ b < n, f a b = f' a b) {invPath : Array UInt64} {p : Part} {k : List (List UInt64)} (hr : Reach n f invPath p k) : Reach n f' invPath p k

Reach only looks at the oracle inside {0, …, n-1}.

structure IsoGraph.Canon.IsAutoArr (n : ℕ) (f : ℕ → ℕ → Bool) (g : Array ℕ) : Prop

g is an automorphism of Graph.ofOracle n f, in array form.

• perm : PermArr n g

  It permutes the vertices.

• adj (u : ℕ) : u < n → ∀ v < n, f g[u]! g[v]! = f u v

  It preserves adjacency.

theorem IsoGraph.Canon.autoOf_isAuto {n : ℕ} {f : ℕ → ℕ → Bool} {σ τ : Array ℕ} (hσ : PermArr n σ) (hτ : PermArr n τ) (hcert : certOf (Graph.ofOracle n f) σ = certOf (Graph.ofOracle n f) τ) : IsAutoArr n f (autoOf n σ τ)

What automorphism harvesting yields.

theorem IsoGraph.Canon.IsAutoArr.graph {n : ℕ} {f : ℕ → ℕ → Bool} {g : Array ℕ} (hg : IsAutoArr n f g) : (Graph.ofOracle n fun (a b : ℕ) => f g[a]! g[b]!) = Graph.ofOracle n f

An automorphism does not change the graph it is an automorphism of.

theorem IsoGraph.Canon.reach_auto {n : ℕ} {f : ℕ → ℕ → Bool} {g : Array ℕ} (hg : IsAutoArr n f g) {invPath : Array UInt64} {p q : Part} {k : List (List UInt64)} (hp : Part.WF n p) (hq : Part.WF n q) (he : PartEquiv n (fun (x : ℕ) => g[x]!) p q) (h : Reach n f invPath q k) : Reach n f invPath p k

Automorphisms permute the leaves. If p is γ-invariant, transporting along γ sends leaves below p to leaves below p with the same key.

theorem IsoGraph.Canon.child_wf {n : ℕ} {f : ℕ → ℕ → Bool} {p : Part} (hp : Part.WF n p) {v : ℕ} (hv : v < n) : Part.WF n (child (Graph.ofOracle n f) p v).1

theorem IsoGraph.Canon.reach_child_auto {n : ℕ} {f : ℕ → ℕ → Bool} {g : Array ℕ} (hg : IsAutoArr n f g) {p : Part} (hp : Part.WF n p) (he : PartEquiv n (fun (x : ℕ) => g[x]!) p p) {invPath : Array UInt64} {v : ℕ} {k : List (List UInt64)} (hv : v < n) (h : Reach n f (childInv (Graph.ofOracle n f) invPath p v) (child (Graph.ofOracle n f) p v).1 k) : Reach n f (childInv (Graph.ofOracle n f) invPath p g[v]!) (child (Graph.ofOracle n f) p g[v]!).1 k

Orbit pruning is sound. If γ is an automorphism fixing the current partition, the subtree below the child v and the subtree below the child γ v have the same leaf keys.