The incumbent never gets worse

The search keeps one leaf, St.best, and replaces it only when it finds a better one. This file makes that precise: whatever the search ends up holding is at least as good as anything it held on the way.

There is one place where the incumbent is dropped rather than improved — pruneNode, when the node's invariant path already beats the incumbent's. That is still monotone, but only because of Progress.lean: the node is then guaranteed to come back with a leaf of its own subtree (dfsNode_best, dfsNode_reach), and every leaf of that subtree beats what was dropped (pruneNode_cleared). dfsNode_mono_cleared packages the two, and dfsNode_prune_shift — that clearing the incumbent does not change what the node does next — is what lets it be applied to the whole dfsNode call rather than to its innards.

The comparison used throughout is compare k k' ≠ .gt on leafKeys, the same order BestKey is stated with.

Order helpers

theorem IsoGraph.Canon.cmp_le_refl (k : List (List UInt64)) : compare k k ≠ Ordering.gt

theorem IsoGraph.Canon.cmp_le_trans {a b c : List (List UInt64)} (h1 : compare a b ≠ Ordering.gt) (h2 : compare b c ≠ Ordering.gt) : compare a c ≠ Ordering.gt

theorem IsoGraph.Canon.lexCmpU64_gt_symm {a b : Array UInt64} (h : lexCmpU64 a b = Ordering.gt) : lexCmpU64 b a = Ordering.lt

Domination

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

k is no better than the leaf the state holds.

Equations

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

def IsoGraph.Canon.BestMono (st st' : St) : Prop

The incumbent never gets worse.

Equations

• IsoGraph.Canon.BestMono st st' = ∀ (l : IsoGraph.Canon.Leaf), st.best = some l → IsoGraph.Canon.Dom st' (IsoGraph.Canon.leafKey l.invPath l.cert)

theorem IsoGraph.Canon.BestMono.rfl (st : St) : BestMono st st

theorem IsoGraph.Canon.Dom.mono {st st' : St} {k : List (List UInt64)} (h : Dom st k) (hm : BestMono st st') : Dom st' k

theorem IsoGraph.Canon.BestMono.trans {st st' st'' : St} (h : BestMono st st') (h' : BestMono st' st'') : BestMono st st''

theorem IsoGraph.Canon.BestMono.of_best_eq {st st' : St} (h : st'.best = st.best) : BestMono st st'

leafUpdate improves the incumbent

theorem IsoGraph.Canon.leafUpdate_best_ge (G : Graph) (path : Array ℕ) (invPath : Array UInt64) (lab : Array ℕ) (st : St) : (leafUpdate G path invPath lab st).best = st.best ∨ (leafUpdate G path invPath lab st).best = some { path := path, invPath := invPath, cert := certOf G lab, lab := lab } ∧ ∀ (b : Leaf), st.best = some b → lexCmpU64 invPath b.invPath = Ordering.gt ∨ lexCmpU64 invPath b.invPath = Ordering.eq ∧ lexCmpU64 (certOf G lab) b.cert = Ordering.gt

theorem IsoGraph.Canon.leafUpdate_mono (G : Graph) (path : Array ℕ) (invPath : Array UInt64) (lab : Array ℕ) (st : St) : BestMono st (leafUpdate G path invPath lab st)

pruneNode only discards a dominated incumbent

theorem IsoGraph.Canon.pruneNode_mono {invPath : Array UInt64} {st st' : St} (h : pruneNode invPath st = some st') : st'.best = st.best ∨ st'.best = none ∧ ∀ (b : Leaf), st.best = some b → lexCmpU64 invPath (b.invPath.extract 0 invPath.size) = Ordering.gt

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

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

theorem IsoGraph.Canon.pruneNode_cleared {n : ℕ} {f : ℕ → ℕ → Bool} {invPath : Array UInt64} {p : Part} {st st' : St} {b : Leaf} {k : List (List UInt64)} (h : pruneNode invPath st = some st') (hnone : st'.best = none) (hb : st.best = some b) (hk : Reach n f invPath p k) : compare (leafKey b.invPath b.cert) k ≠ Ordering.gt

When pruneNode throws the incumbent away, every leaf below the node beats it.

theorem IsoGraph.Canon.pruneNode_mono' {invPath : Array UInt64} {st st' : St} (h : pruneNode invPath st = some st') : st' = st ∨ st' = { best := none, first := st.first, autos := st.autos, nodes := st.nodes, abortTo := st.abortTo } ∧ ∀ (b : Leaf), st.best = some b → lexCmpU64 invPath (b.invPath.extract 0 invPath.size) = Ordering.gt

theorem IsoGraph.Canon.dfsNode_prune_shift {G : Graph} {fuel : ℕ} {path : Array ℕ} {invPath : Array UInt64} {p : Part} {st st' : St} (habort : st.abortTo.isSome = false) (hprune : pruneNode invPath st = some st') (hnone : st'.best = none) : dfsNode G (fuel + 1) path invPath p st = dfsNode G (fuel + 1) path invPath p st'

Discarding the incumbent at a node does not change what the node does next.

theorem IsoGraph.Canon.dfsNode_mono_cleared (n : ℕ) (f : ℕ → ℕ → Bool) (fuel : ℕ) (path : Array ℕ) (invPath : Array UInt64) (p : Part) (st st' : St) (hp : Part.WF n p) (hfuel : n + 1 ≤ numCells n p + fuel) (habort : st.abortTo.isSome = false) (hprune : pruneNode invPath st = some st') (hnone : st'.best = none) : BestMono st (dfsNode (Graph.ofOracle n f) fuel path invPath p st)

The clearing case of monotonicity: if the node throws the incumbent away, the leaf it comes back with is one from below the node, and every such leaf beats what was thrown away.

theorem IsoGraph.Canon.dfsNode_mono (n : ℕ) (f : ℕ → ℕ → Bool) (fuel : ℕ) (path : Array ℕ) (invPath : Array UInt64) (p : Part) (st : St) : Part.WF n p → n + 1 ≤ numCells n p + fuel → BestMono st (dfsNode (Graph.ofOracle n f) fuel path invPath p st)

The incumbent never gets worse.