The search tree, and what the search is looking for

IsoGraph.Canon.Equivariance proves that the ingredients of the search — refinement, individualisation, the certificate — are equivariant, and that every leaf the search records is an honest one. This file is about the search tree:

• lexCmpU64 is shown to be compare on List UInt64, which hands us a linear order (Std's OrientedOrd/TransOrd/LawfulEqOrd instances) for free.
• Reach describes the leaves of the unpruned tree, and key the quantity the search maximises: the pair (node-invariant path, certificate), encoded as a List (List UInt64) so that lexicographic compare on it is the comparison leafUpdate performs.
• reach_transfer transports leaves along a renaming, and bestKey_transfer concludes that the specification — "the largest key of any leaf" — is an isomorphism invariant.

The bridge from the algorithm to the specification — that the search's winner really is the largest key, i.e. that none of the three pruning rules ever discards it — is dfsNode_dom of IsoGraph/Canon/Optimal.lean; the two are joined in IsoGraph/Canon/Correct.lean.

The comparison used to pick the winner

lexCmpU64 is compare on the underlying lists, so it is a linear order: antisymmetric (LawfulEqCmp), total (OrientedCmp) and transitive (TransCmp).

theorem IsoGraph.Canon.lexCmpFrom_eq_compare (a b : Array UInt64) (fuel i : ℕ) : i + fuel = min a.size b.size → lexCmpFrom a b fuel i = compare (List.drop i a.toList) (List.drop i b.toList)

theorem IsoGraph.Canon.lexCmpU64_eq_compare (a b : Array UInt64) : lexCmpU64 a b = compare a.toList b.toList

The search's comparison is compare on the underlying lists.

theorem IsoGraph.Canon.lexCmpU64_eq_iff {a b : Array UInt64} : lexCmpU64 a b = Ordering.eq ↔ a = b

theorem IsoGraph.Canon.lexCmpU64_refl (a : Array UInt64) : lexCmpU64 a a = Ordering.eq

def IsoGraph.Canon.leafKey (invPath cert : Array UInt64) : List (List UInt64)

The key a leaf is judged by: its node-invariant path first, its certificate second. Packing the two as a List (List UInt64) makes lexicographic compare on the pair — exactly the comparison leafUpdate performs — available with all of Std's order lemmas.

Equations

• IsoGraph.Canon.leafKey invPath cert = [invPath.toList, cert.toList]

theorem IsoGraph.Canon.compare_leafKey (i c i' c' : Array UInt64) : compare (leafKey i c) (leafKey i' c') = match lexCmpU64 i i' with | Ordering.eq => lexCmpU64 c c' | o => o

compare on keys is the two-stage comparison of leafUpdate.

theorem IsoGraph.Canon.leafKey_inj {i c i' c' : Array UInt64} (h : leafKey i c = leafKey i' c') : i = i' ∧ c = c'

The search tree

Reach n f invPath p k says that the tree rooted at the refined partition p — the unpruned tree, in which every vertex of the target cell is individualised in turn — has a leaf with key k. This is the search's specification: canonical is supposed to return the largest such key (BestKey), and that is manifestly an isomorphism invariant (bestKey_transfer).

def IsoGraph.Canon.child (G : Graph) (p : Part) (v : ℕ) : Part × UInt64

The child of p obtained by individualising v and re-refining, with the trace of the refinement. This is exactly the step dfsChildren takes.

Equations

• IsoGraph.Canon.child G p v = IsoGraph.Canon.refine G (IsoGraph.Canon.individualize p v).1 ((Array.replicate G.n false).set! (IsoGraph.Canon.individualize p v).2 true) IsoGraph.Canon.hashSeed

def IsoGraph.Canon.childInv (G : Graph) (invPath : Array UInt64) (p : Part) (v : ℕ) : Array UInt64

The node invariant of that child, appended to the path invariant.

Equations

• IsoGraph.Canon.childInv G invPath p v = invPath.push (IsoGraph.Canon.mix (IsoGraph.Canon.child G p v).2 ((IsoGraph.Canon.child G p v).1.shapeHash G.n))

inductive IsoGraph.Canon.Reach (n : ℕ) (f : ℕ → ℕ → Bool) : Array UInt64 → Part → List (List UInt64) → Prop

The leaves of the unpruned search tree below p, described by their keys.

• leaf {n : ℕ} {f : ℕ → ℕ → Bool} {invPath : Array UInt64} {p : Part} (h : p.targetCell n = none) : Reach n f invPath p (leafKey invPath (certOf (Graph.ofOracle n f) p.lab))
• step {n : ℕ} {f : ℕ → ℕ → Bool} {invPath : Array UInt64} {p : Part} {c v : ℕ} {k : List (List UInt64)} (hc : p.targetCell n = some c) (hv : v < n) (hcell : p.cst[p.pos[v]!]! = c) (h : Reach n f (childInv (Graph.ofOracle n f) invPath p v) (child (Graph.ofOracle n f) p v).1 k) : Reach n f invPath p k

The tree is equivariant

theorem IsoGraph.Canon.child_equiv {n : ℕ} {σ : ℕ → ℕ} {f : ℕ → ℕ → Bool} {p q : Part} (hσ : IsPerm n σ) (hp : Part.WF n p) (hq : Part.WF n q) (h : PartEquiv n σ p q) {v : ℕ} (hv : v < n) : PartEquiv n σ (child (Graph.ofOracle n f) p (σ v)).1 (child (Graph.ofOracle n fun (a b : ℕ) => f (σ a) (σ b)) q v).1 ∧ (child (Graph.ofOracle n f) p (σ v)).2 = (child (Graph.ofOracle n fun (a b : ℕ) => f (σ a) (σ b)) q v).2

theorem IsoGraph.Canon.childInv_equiv {n : ℕ} {σ : ℕ → ℕ} {f : ℕ → ℕ → Bool} {p q : Part} (hσ : IsPerm n σ) (hp : Part.WF n p) (hq : Part.WF n q) (h : PartEquiv n σ p q) (invPath : Array UInt64) {v : ℕ} (hv : v < n) : childInv (Graph.ofOracle n f) invPath p (σ v) = childInv (Graph.ofOracle n fun (a b : ℕ) => f (σ a) (σ b)) invPath q v

theorem IsoGraph.Canon.reach_transfer {n : ℕ} {σ : ℕ → ℕ} {f : ℕ → ℕ → Bool} (hσ : IsPerm n σ) {invPath : Array UInt64} {q : Part} {k : List (List UInt64)} (hr : Reach n (fun (a b : ℕ) => f (σ a) (σ b)) invPath q k) {p : Part} : Part.WF n p → Part.WF n q → PartEquiv n σ p q → Reach n f invPath p k

Leaves transport along a renaming. If p is q renamed by σ, every leaf of the tree below q in the renamed graph has a leaf below p in the original one with the same key.

theorem IsoGraph.Canon.reach_transfer' {n : ℕ} {σ : ℕ → ℕ} {f : ℕ → ℕ → Bool} (hσ : IsPerm n σ) {invPath : Array UInt64} {p : Part} {k : List (List UInt64)} (hr : Reach n f invPath p k) {q : Part} : Part.WF n p → Part.WF n q → PartEquiv n σ p q → Reach n (fun (a b : ℕ) => f (σ a) (σ b)) invPath q k

The converse direction: a leaf below p gives one below q, again with the same key. The vertex to individualise is pulled back through σ.

The specification, and its invariance

def IsoGraph.Canon.rootPart (n : ℕ) (f : ℕ → ℕ → Bool) : Part

The root of the search: the initially refined partition and its one-entry invariant path.

Equations

• IsoGraph.Canon.rootPart n f = (IsoGraph.Canon.initialRefine (IsoGraph.Canon.Graph.ofOracle n f)).1

def IsoGraph.Canon.rootInv (n : ℕ) (f : ℕ → ℕ → Bool) : Array UInt64

The invariant path at the root.

Equations

• IsoGraph.Canon.rootInv n f = #[IsoGraph.Canon.mix (IsoGraph.Canon.initialRefine (IsoGraph.Canon.Graph.ofOracle n f)).2 ((IsoGraph.Canon.rootPart n f).shapeHash n)]

def IsoGraph.Canon.Leafkey (n : ℕ) (f : ℕ → ℕ → Bool) (k : List (List UInt64)) : Prop

k is the key of a leaf of the whole (unpruned) search tree.

Equations

• IsoGraph.Canon.Leafkey n f k = IsoGraph.Canon.Reach n f (IsoGraph.Canon.rootInv n f) (IsoGraph.Canon.rootPart n f) k

def IsoGraph.Canon.BestKey (n : ℕ) (f : ℕ → ℕ → Bool) (k : List (List UInt64)) : Prop

The specification of canonical: the largest key of any leaf.

Equations

• IsoGraph.Canon.BestKey n f k = (IsoGraph.Canon.Leafkey n f k ∧ ∀ (k' : List (List UInt64)), IsoGraph.Canon.Leafkey n f k' → compare k' k ≠ Ordering.gt)

theorem IsoGraph.Canon.bestKey_unique {n : ℕ} {f : ℕ → ℕ → Bool} {k k' : List (List UInt64)} (h : BestKey n f k) (h' : BestKey n f k') : k = k'

theorem IsoGraph.Canon.leafkey_transfer {n : ℕ} {σ : ℕ → ℕ} {f : ℕ → ℕ → Bool} (hσ : IsPerm n σ) (k : List (List UInt64)) : Leafkey n (fun (a b : ℕ) => f (σ a) (σ b)) k ↔ Leafkey n f k

The specification is an isomorphism invariant. Renaming the graph does not change the set of leaf keys, hence not the largest one.

theorem IsoGraph.Canon.bestKey_transfer {n : ℕ} {σ : ℕ → ℕ} {f : ℕ → ℕ → Bool} (hσ : IsPerm n σ) (k : List (List UInt64)) : BestKey n (fun (a b : ℕ) => f (σ a) (σ b)) k ↔ BestKey n f k

The target cell really is a cell

theorem IsoGraph.Canon.cenTargetFrom_cst {n : ℕ} {p : Part} (hp : Part.WF n p) (fuel i : ℕ) : (i < n → p.cst[i]! = i) → ∀ (c : ℕ), cenTargetFrom p.cen n fuel i = some c → p.cst[c]! = c

theorem IsoGraph.Canon.targetCell_cst {n : ℕ} {p : Part} (hp : Part.WF n p) {c : ℕ} (h : p.targetCell n = some c) : p.cst[c]! = c

The target cell is a cell start.

theorem IsoGraph.Canon.mem_extract_cell {n : ℕ} {p : Part} (hp : Part.WF n p) {c v : ℕ} (hc : c < n) (hcst : p.cst[c]! = c) (h : v ∈ (p.lab.extract c p.cen[c]!).toList) : p.cst[p.pos[v]!]! = c

The children dfsChildren enumerates are exactly the vertices of the target cell.

The winner is a leaf of the tree

The induction is parametric in a predicate P on keys: if everything reachable below the current node satisfies P, and everything the state already holds satisfies P, then so does everything the state holds afterwards. Taking P to be "is a leaf key of the whole tree" at the root gives canonical_leafkey.

def IsoGraph.Canon.StP (P : List (List UInt64) → Prop) (st : St) : Prop

Every leaf the state holds satisfies P.

Equations

• IsoGraph.Canon.StP P st = ∀ (l : IsoGraph.Canon.Leaf), st.best = some l → P (IsoGraph.Canon.leafKey l.invPath l.cert)

theorem IsoGraph.Canon.pruneNode_P {P : List (List UInt64) → Prop} {invPath : Array UInt64} {st st' : St} (h : pruneNode invPath st = some st') (hst : StP P st) : StP P st'

theorem IsoGraph.Canon.StP.addAuto {P : List (List UInt64) → Prop} {st : St} (h : StP P st) (g : Array ℕ) : StP P (st.addAuto g)

theorem IsoGraph.Canon.StP.unwind {P : List (List UInt64) → Prop} {st : St} (h : StP P st) (path : Array ℕ) : StP P (Canon.unwind path st)

theorem IsoGraph.Canon.leafUpdate_P {P : List (List UInt64) → Prop} {G : Graph} {path : Array ℕ} {invPath : Array UInt64} {lab : Array ℕ} {st : St} (hl : P (leafKey invPath (certOf G lab))) (hst : StP P st) : StP P (leafUpdate G path invPath lab st)

theorem IsoGraph.Canon.dfsNode_reach (n : ℕ) (f : ℕ → ℕ → Bool) (P : List (List UInt64) → Prop) (fuel : ℕ) (path : Array ℕ) (invPath : Array UInt64) (p : Part) (st : St) : Part.WF n p → (∀ (k : List (List UInt64)), Reach n f invPath p k → P k) → StP P st → StP P (dfsNode (Graph.ofOracle n f) fuel path invPath p st)

The search only ever holds leaves of the tree below the current node.

The winner is a leaf of the whole tree

def IsoGraph.Canon.canonSt (n : ℕ) (f : ℕ → ℕ → Bool) : St

The final state of the search on Graph.ofOracle n f.

Equations

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

theorem IsoGraph.Canon.canonical_eq (n : ℕ) (f : ℕ → ℕ → Bool) : canonical (Graph.ofOracle n f) = match (canonSt n f).best with | none => { lab := Array.range n, cert := certOf (Graph.ofOracle n f) (Array.range n), autos := #[], nodes := (canonSt n f).nodes } | some b => { lab := b.lab, cert := b.cert, autos := (canonSt n f).autos, nodes := (canonSt n f).nodes }

theorem IsoGraph.Canon.canonSt_leafkey (n : ℕ) (f : ℕ → ℕ → Bool) : StP (Leafkey n f) (canonSt n f)

Soundness of the search. Whatever leaf the search ends up holding really is a leaf of the (unpruned) tree.

theorem IsoGraph.Canon.canonical_cert_leafkey (n : ℕ) (f : ℕ → ℕ → Bool) (b : Leaf) (hb : (canonSt n f).best = some b) : (canonical (Graph.ofOracle n f)).cert = b.cert ∧ Leafkey n f (leafKey b.invPath b.cert)

Leaves extend the invariant path of the node they hang below

theorem IsoGraph.Canon.reach_extends {n : ℕ} {f : ℕ → ℕ → Bool} {invPath : Array UInt64} {p : Part} {k : List (List UInt64)} (h : Reach n f invPath p k) : ∃ (tail : List UInt64) (c : List UInt64), k = [invPath.toList ++ tail, c]

theorem IsoGraph.Canon.compare_append_lt {ip b : List UInt64} (tail : List UInt64) (h : compare ip (List.take ip.length b) = Ordering.lt) : compare (ip ++ tail) b = Ordering.lt

If a node's invariant path is already worse than the incumbent's, so is every leaf below it.

theorem IsoGraph.Canon.compare_leafKey_lt {ip b tail c c' : List UInt64} (h : compare ip (List.take ip.length b) = Ordering.lt) : compare [ip ++ tail, c] [b, c'] = Ordering.lt

Invariant pruning is sound

def IsoGraph.Canon.Beaten (st : St) (k : List (List UInt64)) : Prop

k is beaten by the leaf the state currently holds.

Equations

• IsoGraph.Canon.Beaten st k = ∃ (l : IsoGraph.Canon.Leaf), st.best = some l ∧ compare k (IsoGraph.Canon.leafKey l.invPath l.cert) = Ordering.lt

theorem IsoGraph.Canon.lexCmpU64_extract {a b : Array UInt64} : lexCmpU64 a (b.extract 0 a.size) = compare a.toList (List.take a.size b.toList)

theorem IsoGraph.Canon.pruneNode_none {n : ℕ} {f : ℕ → ℕ → Bool} {invPath : Array UInt64} {p : Part} {st : St} (h : pruneNode invPath st = none) {k : List (List UInt64)} (hk : Reach n f invPath p k) : Beaten st k

When pruneNode discards the subtree, every leaf below the node is beaten.