Where the search records its leaves

Two bookkeeping facts that the optimality argument needs, neither of which says anything about which leaf is best.

• extract_nodup — the children of a node are pairwise distinct. A node's child list is a slice of Part.lab, and Part.lab is a permutation of the vertices, so no vertex is visited twice.
• dfsNode_paths — a call to dfsNode at path only ever records leaves below path. It is stated parametrically in a predicate P on paths: if everything the state already holds satisfies P, and everything extending path satisfies P, then that is still true when the call returns. Instantiating P differently at each use turns this one lemma into the running invariant "the incumbent's path does not go down a branch we have not explored yet".

The children of a node are distinct

theorem IsoGraph.Canon.lab_nodup {n : ℕ} {p : Part} (hp : Part.WF n p) : p.lab.toList.Nodup

theorem IsoGraph.Canon.extract_nodup {n : ℕ} {p : Part} (hp : Part.WF n p) (a b : ℕ) : (p.lab.extract a b).toList.Nodup

Prefixes of paths

def IsoGraph.Canon.PathPre (a b : Array ℕ) : Prop

a is an initial segment of b.

Equations

• IsoGraph.Canon.PathPre a b = (a.size ≤ b.size ∧ ∀ i < a.size, a[i]! = b[i]!)

theorem IsoGraph.Canon.PathPre.refl (a : Array ℕ) : PathPre a a

theorem IsoGraph.Canon.PathPre.trans {a b c : Array ℕ} (h1 : PathPre a b) (h2 : PathPre b c) : PathPre a c

theorem IsoGraph.Canon.PathPre.push_self (a : Array ℕ) (v : ℕ) : PathPre a (a.push v)

theorem IsoGraph.Canon.PathPre.of_push {a b : Array ℕ} {v : ℕ} (h : PathPre (a.push v) b) : PathPre a b

theorem IsoGraph.Canon.PathPre.push_iff {a b : Array ℕ} {v : ℕ} : PathPre (a.push v) b ↔ PathPre a b ∧ a.size < b.size ∧ b[a.size]! = v

The search only records leaves of the subtree it is in

def IsoGraph.Canon.StQ (P : Array ℕ → Prop) (st : St) : Prop

Every leaf a state remembers — incumbent or first — has a path satisfying P.

Equations

• IsoGraph.Canon.StQ P st = ((∀ (l : IsoGraph.Canon.Leaf), st.best = some l → P l.path) ∧ ∀ (l : IsoGraph.Canon.Leaf), st.first = some l → P l.path)

theorem IsoGraph.Canon.StQ.mono {P P' : Array ℕ → Prop} {st : St} (h : StQ P st) (hPP : ∀ (Q : Array ℕ), P Q → P' Q) : StQ P' st

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

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

theorem IsoGraph.Canon.pruneNode_Q {P : Array ℕ → Prop} {invPath : Array UInt64} {st st' : St} (h : pruneNode invPath st = some st') (hst : StQ P st) : StQ P st'

theorem IsoGraph.Canon.leafUpdate_Q {P : Array ℕ → Prop} {G : Graph} {path : Array ℕ} {invPath : Array UInt64} {lab : Array ℕ} {st : St} (hp : P path) (hst : StQ P st) : StQ P (leafUpdate G path invPath lab st)

theorem IsoGraph.Canon.dfsNode_paths (n : ℕ) (f : ℕ → ℕ → Bool) (P : Array ℕ → Prop) (fuel : ℕ) (path : Array ℕ) (invPath : Array UInt64) (p : Part) (st : St) : (∀ (Q : Array ℕ), PathPre path Q → P Q) → StQ P st → StQ P (dfsNode (Graph.ofOracle n f) fuel path invPath p st)

The leaves a node records lie below it. Anything the state already held keeps whatever property it had; anything added while the node runs has a path extending the node's.