The leaves and generators a state holds

Bookkeeping for the optimality proof, one layer above Jump.lean.

• commonPrefix_comm — the backjump depth does not depend on which of the two leaves is "current".
• ancReach — the leaves below the depth-j ancestor of a path, phrased through nodePath so that it only depends on path.toList.take j. Node.ancestor_targetCell says an interior node of a path is never a leaf, which is what rules out one leaf's path being a prefix of another's.
• Chld / SubR / reach_iff_subR — a node's leaves are exactly the leaves of its children, and mem_extract_cell' identifies the children with the entries of the child list.
• invAuto — the inverse of a permutation array, needed because orbit pruning has to move leaves back along a generator.
• LeafNode / StGood / dfsNode_good — every leaf a state records is a genuine leaf of the tree, and every generator it records is a genuine automorphism.

commonPrefix is symmetric

theorem IsoGraph.Canon.commonPrefixFrom_comm (a b : Array ℕ) (m fuel i : ℕ) : commonPrefixFrom a b m fuel i = commonPrefixFrom b a m fuel i

theorem IsoGraph.Canon.commonPrefix_comm (a b : Array ℕ) : commonPrefix a b = commonPrefix b a

Ancestors as a function of the path

theorem IsoGraph.Canon.nodePath_take_succ (n : ℕ) (f : ℕ → ℕ → Bool) (path : Array ℕ) {j : ℕ} (hj : j < path.size) : nodePath n f (List.take (j + 1) path.toList) = (childInv (Graph.ofOracle n f) (nodePath n f (List.take j path.toList)).1 (nodePath n f (List.take j path.toList)).2 path[j]!, (child (Graph.ofOracle n f) (nodePath n f (List.take j path.toList)).2 path[j]!).1)

def IsoGraph.Canon.ancReach (n : ℕ) (f : ℕ → ℕ → Bool) (path : Array ℕ) (j : ℕ) (k : List (List UInt64)) : Prop

The leaves below the depth-j ancestor of path.

Equations

• IsoGraph.Canon.ancReach n f path j k = IsoGraph.Canon.Reach n f (IsoGraph.Canon.nodePath n f (List.take j path.toList)).1 (IsoGraph.Canon.nodePath n f (List.take j path.toList)).2 k

theorem IsoGraph.Canon.ancReach_congr {n : ℕ} {f : ℕ → ℕ → Bool} {a b : Array ℕ} {j : ℕ} (h : List.take j a.toList = List.take j b.toList) (k : List (List UInt64)) : ancReach n f a j k ↔ ancReach n f b j k

theorem IsoGraph.Canon.Node.ancestor_targetCell {n : ℕ} {f : ℕ → ℕ → Bool} {path : Array ℕ} {invPath : Array UInt64} {p : Part} (h : Node n f path invPath p) (j : ℕ) : j < path.size → (nodePath n f (List.take j path.toList)).2.targetCell n ≠ none

Interior nodes of a path are not leaves.

Children

def IsoGraph.Canon.Chld (n : ℕ) (p : Part) (w : ℕ) : Prop

w is a child of the node p: a vertex of its target cell.

Equations

• IsoGraph.Canon.Chld n p w = ∃ (c : ℕ), p.targetCell n = some c ∧ w < n ∧ p.cst[p.pos[w]!]! = c

def IsoGraph.Canon.SubR (n : ℕ) (f : ℕ → ℕ → Bool) (invPath : Array UInt64) (p : Part) (w : ℕ) (k : List (List UInt64)) : Prop

The leaves below the child w.

Equations

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

theorem IsoGraph.Canon.reach_iff_subR {n : ℕ} {f : ℕ → ℕ → Bool} {invPath : Array UInt64} {p : Part} {c : ℕ} (htc : p.targetCell n = some c) (k : List (List UInt64)) : Reach n f invPath p k ↔ ∃ (w : ℕ), Chld n p w ∧ SubR n f invPath p w k

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

Membership in the child list is exactly Chld.

Which automorphisms a leaf update can add

theorem IsoGraph.Canon.addAuto_mem {st : St} {g x : Array ℕ} (h : x ∈ (st.addAuto g).autos) : x ∈ st.autos ∨ x = g

theorem IsoGraph.Canon.addAuto_P {P : Array ℕ → Prop} {st : St} {a : Array ℕ} (hst : ∀ g ∈ st.autos, P g) (ha : P a) (g : Array ℕ) : g ∈ (st.addAuto a).autos → P g

theorem IsoGraph.Canon.leafUpdate_autos {P : Array ℕ → Prop} {G : Graph} {path : Array ℕ} {invPath : Array UInt64} {lab : Array ℕ} {st : St} (hst : ∀ g ∈ st.autos, P g) (hl : ∀ (l : Leaf), st.first = some l ∨ st.best = some l → lexCmpU64 (certOf G lab) l.cert = Ordering.eq → P (autoOf G.n lab l.lab)) (g : Array ℕ) : g ∈ (leafUpdate G path invPath lab st).autos → P g

Every automorphism a leaf update adds is autoOf against one of the recorded leaves.

Inverse automorphisms

theorem IsoGraph.Canon.range_permArr (n : ℕ) : PermArr n (Array.range n)

def IsoGraph.Canon.invAuto (n : ℕ) (g : Array ℕ) : Array ℕ

The inverse of a permutation array, built with the same machinery as autoOf.

Equations

• IsoGraph.Canon.invAuto n g = IsoGraph.Canon.autoOf n g (Array.range n)

theorem IsoGraph.Canon.invAuto_get {n : ℕ} {g : Array ℕ} (hg : PermArr n g) {i : ℕ} (hi : i < n) : (invAuto n g)[g[i]!]! = i

theorem IsoGraph.Canon.invAuto_isAuto {n : ℕ} {f : ℕ → ℕ → Bool} {g : Array ℕ} (hg : IsAutoArr n f g) : IsAutoArr n f (invAuto n g)

The leaves the search records are genuine tree leaves

def IsoGraph.Canon.LeafNode (n : ℕ) (f : ℕ → ℕ → Bool) (l : Leaf) : Prop

l really is a leaf of the search tree: its path individualises down to a discrete partition, and its labelling and certificate are that partition's.

Equations

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

theorem IsoGraph.Canon.LeafNode.permArr {n : ℕ} {f : ℕ → ℕ → Bool} {l : Leaf} (h : LeafNode n f l) : PermArr n l.lab

theorem IsoGraph.Canon.LeafNode.cert_eq {n : ℕ} {f : ℕ → ℕ → Bool} {l : Leaf} (h : LeafNode n f l) : l.cert = certOf (Graph.ofOracle n f) l.lab

def IsoGraph.Canon.StGood (n : ℕ) (f : ℕ → ℕ → Bool) (st : St) : Prop

Everything a state remembers is genuine: both recorded leaves, and every generator.

Equations

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

theorem IsoGraph.Canon.unwind_autos (path : Array ℕ) (st : St) : (unwind path st).autos = st.autos

theorem IsoGraph.Canon.StGood.unwind {n : ℕ} {f : ℕ → ℕ → Bool} {st : St} (h : StGood n f st) (path : Array ℕ) : StGood n f (Canon.unwind path st)

theorem IsoGraph.Canon.pruneNode_good {n : ℕ} {f : ℕ → ℕ → Bool} {invPath : Array UInt64} {st st' : St} (h : pruneNode invPath st = some st') (hst : StGood n f st) : StGood n f st'

theorem IsoGraph.Canon.leafUpdate_good {n : ℕ} {f : ℕ → ℕ → Bool} {path : Array ℕ} {invPath : Array UInt64} {lab : Array ℕ} {st : St} (hl : LeafNode n f { path := path, invPath := invPath, cert := certOf (Graph.ofOracle n f) lab, lab := lab }) (hst : StGood n f st) : StGood n f (leafUpdate (Graph.ofOracle n f) path invPath lab st)

theorem IsoGraph.Canon.dfsNode_good (n : ℕ) (f : ℕ → ℕ → Bool) (fuel : ℕ) (path : Array ℕ) (invPath : Array UInt64) (p : Part) (st : St) : Node n f path invPath p → StGood n f st → StGood n f (dfsNode (Graph.ofOracle n f) fuel path invPath p st)

Everything the search records is genuine.