The running invariants of the optimality induction

The depth-first search prunes three ways — invariant pruning, orbit pruning and backjumping — and each needs its own reason why the leaves it skips were already accounted for. This file sets up the bookkeeping for the third and hardest one, backjumping.

• take_getElemD, pathPre_of_take — PathPre and "the first j entries agree" say the same thing.
• ancReach_full, ancReach_push, ancReach_child — the leaves below the depth-j ancestor of a path, related to Reach at the node itself and to SubR at one of its children.
• mem_usableAutos — the generators the search is willing to prune with really do fix the path.
• Rec / Pth / Jmp / JmpC — the invariants themselves. Jmp says every branch a recorded leaf went down and the current path has already left behind consists of keys the caller has already accounted for; JmpC is the variant that holds while a node works through its own children.
• leaf_abort_dom — the payoff: the backjump a leaf update requests never skips a leaf that is not already dominated. This is jump_sound fed by Jmp.

Prefixes

theorem IsoGraph.Canon.pathPre_of_take {a b : Array ℕ} (hab : a.size ≤ b.size) (h : List.take a.size a.toList = List.take a.size b.toList) : PathPre a b

theorem IsoGraph.Canon.take_of_pathPre {a b : Array ℕ} (h : PathPre a b) : List.take a.size a.toList = List.take a.size b.toList

Ancestors

theorem IsoGraph.Canon.ancReach_full {n : ℕ} {f : ℕ → ℕ → Bool} {path : Array ℕ} {invPath : Array UInt64} {p : Part} (h : Node n f path invPath p) (k : List (List UInt64)) : ancReach n f path path.size k ↔ Reach n f invPath p k

theorem IsoGraph.Canon.ancReach_push {n : ℕ} {f : ℕ → ℕ → Bool} (path : Array ℕ) (v j : ℕ) (hj : j ≤ path.size) (k : List (List UInt64)) : ancReach n f (path.push v) j k ↔ ancReach n f path j k

theorem IsoGraph.Canon.ancReach_child {n : ℕ} {f : ℕ → ℕ → Bool} {path : Array ℕ} {invPath : Array UInt64} {p : Part} (h : Node n f path invPath p) (v : ℕ) (k : List (List UInt64)) : ancReach n f (path.push v) (path.size + 1) k ↔ SubR n f invPath p v k

Usable automorphisms

theorem IsoGraph.Canon.mem_usableAutos {autos : Array (Array ℕ)} {path g : Array ℕ} (h : g ∈ usableAutos autos path) : g ∈ autos ∧ ∀ i < path.size, g[path[i]!]! = path[i]!

The running invariants

def IsoGraph.Canon.Rec (st : St) (l : Leaf) : Prop

A leaf the state records.

Equations

• IsoGraph.Canon.Rec st l = (st.best = some l ∨ st.first = some l)

def IsoGraph.Canon.Pth (st : St) (path : Array ℕ) : Prop

No recorded leaf lies below the current node.

Equations

• IsoGraph.Canon.Pth st path = ∀ (l : IsoGraph.Canon.Leaf), IsoGraph.Canon.Rec st l → ¬IsoGraph.Canon.PathPre path l.path

def IsoGraph.Canon.Jmp (n : ℕ) (f : ℕ → ℕ → Bool) (P : List (List UInt64) → Prop) (path : Array ℕ) (st : St) : Prop

The backjump invariant, relative to a target predicate P on leaf keys. Every branch a recorded leaf went down and that the current path has already left behind consists entirely of keys satisfying P. At the use site P is "dominated by the incumbent, or already accounted for by the caller".

Equations

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

def IsoGraph.Canon.JmpC (n : ℕ) (f : ℕ → ℕ → Bool) (P : List (List UInt64) → Prop) (path : Array ℕ) (st : St) : Prop

The same, also covering the branches leaving the current node itself: what holds while a node is working through its children.

Equations

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

theorem IsoGraph.Canon.JmpC.child {n : ℕ} {f : ℕ → ℕ → Bool} {P : List (List UInt64) → Prop} {st : St} {path : Array ℕ} (h : JmpC n f P path st) (v : ℕ) : Jmp n f P (path.push v) st

theorem IsoGraph.Canon.JmpC.of_jmp {n : ℕ} {f : ℕ → ℕ → Bool} {P : List (List UInt64) → Prop} {st : St} {path : Array ℕ} (h : Jmp n f P path st) (hp : Pth st path) : JmpC n f P path st

The leaf case of the optimality induction

theorem IsoGraph.Canon.Node.ancestor' {n : ℕ} {f : ℕ → ℕ → Bool} {path : Array ℕ} {ip : Array UInt64} {p : Part} (h : Node n f path ip p) (j : ℕ) (hj : j ≤ path.size) : Node n f (path.extract 0 j) (nodePath n f (List.take j path.toList)).1 (nodePath n f (List.take j path.toList)).2

theorem IsoGraph.Canon.leaf_abort_dom {n : ℕ} {f : ℕ → ℕ → Bool} {path : Array ℕ} {invPath : Array UInt64} {p : Part} (hnode : Node n f path invPath p) {st : St} {P : List (List UInt64) → Prop} (hgood : StGood n f st) (hpth : Pth st path) (hjmp : Jmp n f P path st) {j : ℕ} (hab : (leafUpdate (Graph.ofOracle n f) path invPath p.lab st).abortTo = some j) : j < path.size ∧ ∀ (k : List (List UInt64)), ancReach n f path (j + 1) k → P k

The backjump a leaf update requests is covered by the jump invariant.