theorem
Hex.GraphIso.Nauty.LoopExit.toNodeSomeInc
{n : Nat}
{ctx : Ctx n}
{tcLevel nodeSpecFuel loopSpecFuel nodeRunFuel runFuel loopFuel level tc len nodeNumcells loopNumcells : Nat}
{tcell : VSet n}
{nodeCodes loopCodes : List Nat}
{rsLab rsPtn : Array Nat}
{cursor : Option Nat}
{bound : Key n}
{nodeSt loopSt out : SearchSt n}
{best outBest : Option (Key n)}
{trail : FrameTrail}
{value : Int}
(hinc : incMax best bound = incMax best (nodeKey ctx tcLevel nodeSpecFuel level nodeCodes nodeSt nodeNumcells))
(hprefix : List.take nodeCodes.length loopCodes = nodeCodes)
(h :
LoopExit ctx tcLevel loopSpecFuel runFuel loopFuel level loopCodes rsLab rsPtn tc len loopNumcells tcell cursor bound
loopSt out best outBest trail (some value))
:
NodeExit ctx tcLevel nodeSpecFuel nodeRunFuel level nodeCodes nodeSt out nodeNumcells best outBest trail value
An early integer-valued loop exit becomes a node exit whenever the loop bound and the node key produce the same incumbent maximum.
theorem
Hex.GraphIso.Nauty.LoopExit.toNodeNoneInc
{n : Nat}
{ctx : Ctx n}
{tcLevel nodeSpecFuel loopSpecFuel nodeRunFuel runFuel loopFuel level tc len nodeNumcells loopNumcells : Nat}
{tcell : VSet n}
{nodeCodes loopCodes : List Nat}
{rsLab rsPtn : Array Nat}
{cursor : Option Nat}
{bound : Key n}
{nodeSt loopSt out : SearchSt n}
{best outBest : Option (Key n)}
{trail : FrameTrail}
(hinc : incMax best bound = incMax best (nodeKey ctx tcLevel nodeSpecFuel level nodeCodes nodeSt nodeNumcells))
(hfuel : n < cursorRank cursor + loopFuel)
(h :
LoopExit ctx tcLevel loopSpecFuel runFuel loopFuel level loopCodes rsLab rsPtn tc len loopNumcells tcell cursor bound
loopSt out best outBest trail none)
:
A sufficiently fuelled none loop exit becomes the node's ordinary
return whenever the loop bound and the node key produce the same incumbent
maximum.
theorem
Hex.GraphIso.Nauty.OtherLoopRun.toNodeSomeInc
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel nodeSpecFuel loopSpecFuel nodeRunFuel runFuel loopFuel level : Nat}
{nodeCodes loopCodes fs : List Nat}
{rsLab rsPtn : Array Nat}
{tc len nodeNumcells loopNumcells : Nat}
{tcell : VSet n}
{cursor : Option Nat}
{bound : Key n}
{nodeSt loopSt out : SearchSt n}
{best outBest : Option (Key n)}
{receiptTrail eventTrail : FrameTrail}
{r : Int}
(hinc : incMax best bound = incMax best (nodeKey ctx tcLevel nodeSpecFuel level nodeCodes nodeSt nodeNumcells))
(hprefix : List.take nodeCodes.length loopCodes = nodeCodes)
(hfixed : loopSt.fixedpts = nodeSt.fixedpts)
(hcoset : loopSt.cosetindex = nodeSt.cosetindex)
(hguide : GuideRel level nodeSt out)
(h :
OtherLoopRun G ctx tcLevel loopSpecFuel runFuel loopFuel level nodeCodes loopCodes fs rsLab rsPtn tc len loopNumcells
tcell cursor bound loopSt out best outBest receiptTrail eventTrail (some r))
:
OtherRun G ctx tcLevel nodeSpecFuel nodeRunFuel level nodeCodes fs nodeSt out nodeNumcells best outBest receiptTrail
eventTrail r
An early integer-valued off-path sweep becomes its enclosing off-path node, given the guide relation between the node entry and the sweep result.
theorem
Hex.GraphIso.Nauty.OtherLoopRun.toNodeNoneInc
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel nodeSpecFuel loopSpecFuel nodeRunFuel runFuel loopFuel level : Nat}
{nodeCodes loopCodes fs : List Nat}
{rsLab rsPtn : Array Nat}
{tc len nodeNumcells loopNumcells : Nat}
{tcell : VSet n}
{cursor : Option Nat}
{bound : Key n}
{nodeSt loopSt out : SearchSt n}
{best outBest : Option (Key n)}
{receiptTrail eventTrail : FrameTrail}
(hinc : incMax best bound = incMax best (nodeKey ctx tcLevel nodeSpecFuel level nodeCodes nodeSt nodeNumcells))
(hfuel : n < cursorRank cursor + loopFuel)
(hfixed : loopSt.fixedpts = nodeSt.fixedpts)
(hcoset : loopSt.cosetindex = nodeSt.cosetindex)
(hguide : GuideRel level nodeSt out)
(h :
OtherLoopRun G ctx tcLevel loopSpecFuel runFuel loopFuel level nodeCodes loopCodes fs rsLab rsPtn tc len loopNumcells
tcell cursor bound loopSt out best outBest receiptTrail eventTrail none)
:
A sufficiently fuelled none off-path sweep is genuine completion and
becomes its enclosing off-path node's ordinary return.
theorem
Hex.GraphIso.Nauty.OtherLoopRun.toNodeSome
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel nodeSpecFuel loopSpecFuel nodeRunFuel runFuel loopFuel level : Nat}
{nodeCodes loopCodes fs : List Nat}
{rsLab rsPtn : Array Nat}
{tc len nodeNumcells loopNumcells : Nat}
{tcell : VSet n}
{cursor : Option Nat}
{bound : Key n}
{nodeSt loopSt out : SearchSt n}
{best outBest : Option (Key n)}
{receiptTrail eventTrail : FrameTrail}
{r : Int}
(hbound : bound = nodeKey ctx tcLevel nodeSpecFuel level nodeCodes nodeSt nodeNumcells)
(hprefix : List.take nodeCodes.length loopCodes = nodeCodes)
(hfixed : loopSt.fixedpts = nodeSt.fixedpts)
(hcoset : loopSt.cosetindex = nodeSt.cosetindex)
(hguide : GuideRel level nodeSt out)
(h :
OtherLoopRun G ctx tcLevel loopSpecFuel runFuel loopFuel level nodeCodes loopCodes fs rsLab rsPtn tc len loopNumcells
tcell cursor bound loopSt out best outBest receiptTrail eventTrail (some r))
:
OtherRun G ctx tcLevel nodeSpecFuel nodeRunFuel level nodeCodes fs nodeSt out nodeNumcells best outBest receiptTrail
eventTrail r
The ordinary case: the loop bound is the node key itself.
theorem
Hex.GraphIso.Nauty.OtherLoopRun.toNodeNone
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel nodeSpecFuel loopSpecFuel nodeRunFuel runFuel loopFuel level : Nat}
{nodeCodes loopCodes fs : List Nat}
{rsLab rsPtn : Array Nat}
{tc len nodeNumcells loopNumcells : Nat}
{tcell : VSet n}
{cursor : Option Nat}
{bound : Key n}
{nodeSt loopSt out : SearchSt n}
{best outBest : Option (Key n)}
{receiptTrail eventTrail : FrameTrail}
(hbound : bound = nodeKey ctx tcLevel nodeSpecFuel level nodeCodes nodeSt nodeNumcells)
(hfuel : n < cursorRank cursor + loopFuel)
(hfixed : loopSt.fixedpts = nodeSt.fixedpts)
(hcoset : loopSt.cosetindex = nodeSt.cosetindex)
(hguide : GuideRel level nodeSt out)
(h :
OtherLoopRun G ctx tcLevel loopSpecFuel runFuel loopFuel level nodeCodes loopCodes fs rsLab rsPtn tc len loopNumcells
tcell cursor bound loopSt out best outBest receiptTrail eventTrail none)
:
The ordinary case: the loop bound is the node key itself.
The node preparation leaves the active set alone.
def
Hex.GraphIso.Nauty.sweepStart
{n : Nat}
(ctx : Ctx n)
(level numcells len : Nat)
(st : SearchSt n)
:
SearchSt n
The sweep entry state: the prepared frame charged with the target cell size and, when the cheap-automorphism test fails, parked one level below.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Hex.GraphIso.Nauty.sweepStart_frames
{n : Nat}
(ctx : Ctx n)
(level numcells len : Nat)
(st : SearchSt n)
:
have rs := refine ctx level st.lab st.ptn st.active numcells;
have start := sweepStart ctx level numcells len st;
start.lab = rs.lab ∧ start.ptn = rs.ptn ∧ start.active = rs.active ∧ start.fixedpts = st.fixedpts ∧ start.gcaFirst = st.gcaFirst ∧ start.gcaCanon = st.gcaCanon ∧ start.canonlab = st.canonlab ∧ start.genTrace = st.genTrace ∧ start.orbits = st.orbits ∧ start.cosetindex = st.cosetindex ∧ start.firstlab = st.firstlab ∧ start.needshortprune = st.needshortprune ∧ (start.noncheaplevel = st.noncheaplevel ∨ start.noncheaplevel = level + 1) ∧ (cheapautom rs.ptn level n = false → start.noncheaplevel = level + 1) ∧ (cheapautom rs.ptn level n = true → start.noncheaplevel = st.noncheaplevel)
Every logical field of the sweep entry state is inherited from the node entry or the refinement.
theorem
Hex.GraphIso.Nauty.NodeInv.sweepHyp
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel sf level numcells tc len : Nat}
{codes bs fs : List Nat}
{st : SearchSt n}
{best : Option (Key n)}
{trail : FrameTrail}
(hg : ctx.g = rowsOf G)
(hn0 : 0 < n)
(hlevel : 1 ≤ level)
(hcheap : st.noncheaplevel ≤ level)
(hdesc : CheapDesc ctx level st.noncheaplevel (refine ctx level st.lab st.ptn st.active numcells))
(hnode : NodeInv G ctx tcLevel level codes bs fs numcells st best trail)
(hlive : Live ctx level st trail)
(hpathOk : PathOk ctx (initPtn n (n + 2) (initialPartition G).snd) (initialPartition G).fst level st)
(horb : OrbSound (OrbConn st.genTrace.toList n) st.orbits n)
(hcoset : st.cosetindex < n)
(hdom : ∀ (b : Key n), best = some b → keyLe (pathLeafKey ctx fs st.firstlab) b)
:
have rs := refine ctx level st.lab st.ptn st.active numcells;
have full := codes ++ [rs.longcode];
have tcell := worksetOf n rs.lab tc (tc + len - 1);
have start := sweepStart ctx level numcells len st;
LoopInv G ctx tcLevel sf level full bs fs rs.numcells rs.lab rs.ptn tc len tcell none start start best trail →
OtherLoopHyp G ctx tcLevel sf level full bs fs rs.numcells rs.lab rs.ptn tc len tcell none st.noncheaplevel start
start best trail
Refinement and target bookkeeping establish the complete entry invariant used by a fresh off-path sibling sweep.
theorem
Hex.GraphIso.Nauty.NodeInv.sweepNode
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{inf tcLevel sf runFuel level numcells tc len : Nat}
{codes bs fs : List Nat}
{st : SearchSt n}
{best : Option (Key n)}
{trail : FrameTrail}
{bound : Key n}
(hg : ctx.g = rowsOf G)
(hinf : inf = n + 2)
(hn0 : 0 < n)
(ih : OtherTotal G ctx inf tcLevel runFuel)
(hlevel : 2 ≤ level)
(hpath : level = codes.length + 1)
(hspec : level + (sf + 1) = n + 1)
(hfuel : n + 2 < level + (runFuel + 1))
(hcheap : st.noncheaplevel ≤ level)
(hdesc : CheapDesc ctx level st.noncheaplevel (refine ctx level st.lab st.ptn st.active numcells))
(hnode : NodeInv G ctx tcLevel level codes bs fs numcells st best trail)
(hlive : Live ctx level st trail)
(hpathOk : PathOk ctx (initPtn n (n + 2) (initialPartition G).snd) (initialPartition G).fst level st)
(horb : OrbSound (OrbConn st.genTrace.toList n) st.orbits n)
(hcoset : st.cosetindex < n)
(hdom : ∀ (b : Key n), best = some b → keyLe (pathLeafKey ctx fs st.firstlab) b)
(hlen2 : 2 ≤ len)
:
have rs := refine ctx level st.lab st.ptn st.active numcells;
have full := codes ++ [rs.longcode];
have tcell := worksetOf n rs.lab tc (tc + len - 1);
have start := sweepStart ctx level numcells len st;
have L :=
otherChildLoop ctx inf tcLevel runFuel (n + 1) level rs.numcells tc ((tcell.nextElem none).getD 0)
(tcell.nextElem none) tcell start;
LoopInv G ctx tcLevel sf level full bs fs rs.numcells rs.lab rs.ptn tc len tcell none start start best trail →
incMax best bound = incMax best (nodeKey ctx tcLevel (sf + 1) level codes st numcells) →
bound = keysMax (sweepKey ctx tcLevel sf level full rs.lab rs.ptn tc rs.numcells 0)
(List.map (fun (o : Nat) => sweepKey ctx tcLevel sf level full rs.lab rs.ptn tc rs.numcells (o + 1))
(List.range (len - 1))) →
(∀ (r : Int) (out : SearchSt n),
L = (some r, out) → otherNode ctx inf tcLevel (runFuel + 1) level numcells st = (r, out)) →
(∀ (out : SearchSt n),
L = (none, out) → otherNode ctx inf tcLevel (runFuel + 1) level numcells st = (Int.ofNat level - 1, out)) →
∃ (outBest : Option (Key n)), ∃ (eventTrail : FrameTrail), OtherRun G ctx tcLevel (sf + 1) (runFuel + 1) level codes fs st
(otherNode ctx inf tcLevel (runFuel + 1) level numcells st).snd numcells best outBest trail eventTrail
(otherNode ctx inf tcLevel (runFuel + 1) level numcells st).fst ∧ OtherKeep ctx level st (otherNode ctx inf tcLevel (runFuel + 1) level numcells st).snd
An off-path internal node whose child sweep starts at sweepStart
with a loop invariant, given the two state equations of the executable
node and a common incumbent maximum for the loop bound and the node key.
theorem
Hex.GraphIso.Nauty.NodeInv.plainSweep
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{inf tcLevel sf runFuel level numcells : Nat}
{codes bs fs : List Nat}
{st : SearchSt n}
{best : Option (Key n)}
{trail : FrameTrail}
(hg : ctx.g = rowsOf G)
(hinf : inf = n + 2)
(hn0 : 0 < n)
(ih : OtherTotal G ctx inf tcLevel runFuel)
(hlevel : 2 ≤ level)
(hpath : level = codes.length + 1)
(hspec : level + (sf + 1) = n + 1)
(hfuel : n + 2 < level + (runFuel + 1))
(hcheap : st.noncheaplevel ≤ level)
(hdesc : CheapDesc ctx level st.noncheaplevel (refine ctx level st.lab st.ptn st.active numcells))
(hnode : NodeInv G ctx tcLevel level codes bs fs numcells st best trail)
(hlive : Live ctx level st trail)
(hpathOk : PathOk ctx (initPtn n (n + 2) (initialPartition G).snd) (initialPartition G).fst level st)
(horb : OrbSound (OrbConn st.genTrace.toList n) st.orbits n)
(hcoset : st.cosetindex < n)
(hdom : ∀ (b : Key n), best = some b → keyLe (pathLeafKey ctx fs st.firstlab) b)
(hnum : (refine ctx level st.lab st.ptn st.active numcells).numcells < n)
(hnonneg : (otherLeafSt ctx level numcells st).compCanon ≥ 0)
:
∃ (outBest : Option (Key n)), ∃ (eventTrail : FrameTrail), OtherRun G ctx tcLevel (sf + 1) (runFuel + 1) level codes fs st
(otherNode ctx inf tcLevel (runFuel + 1) level numcells st).snd numcells best outBest trail eventTrail
(otherNode ctx inf tcLevel (runFuel + 1) level numcells st).fst ∧ OtherKeep ctx level st (otherNode ctx inf tcLevel (runFuel + 1) level numcells st).snd
An off-path internal node with a nonnegative comparison sweeps the specification's target cell.
theorem
Hex.GraphIso.Nauty.NodeInv.hintSweep
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{inf tcLevel sf runFuel level numcells : Nat}
{codes bs fs : List Nat}
{st : SearchSt n}
{best : Option (Key n)}
{trail : FrameTrail}
(hg : ctx.g = rowsOf G)
(hinf : inf = n + 2)
(hn0 : 0 < n)
(ih : OtherTotal G ctx inf tcLevel runFuel)
(hlevel : 2 ≤ level)
(hpath : level = codes.length + 1)
(hspec : level + (sf + 1) = n + 1)
(hfuel : n + 2 < level + (runFuel + 1))
(hcheap : st.noncheaplevel ≤ level)
(hdesc : CheapDesc ctx level st.noncheaplevel (refine ctx level st.lab st.ptn st.active numcells))
(hnode : NodeInv G ctx tcLevel level codes bs fs numcells st best trail)
(hlive : Live ctx level st trail)
(hpathOk : PathOk ctx (initPtn n (n + 2) (initialPartition G).snd) (initialPartition G).fst level st)
(horb : OrbSound (OrbConn st.genTrace.toList n) st.orbits n)
(hcoset : st.cosetindex < n)
(hdom : ∀ (b : Key n), best = some b → keyLe (pathLeafKey ctx fs st.firstlab) b)
(hnum : (refine ctx level st.lab st.ptn st.active numcells).numcells < n)
(heq : ((otherLeafSt ctx level numcells st).eqlevFirst == level) = true)
(hneg : (otherLeafSt ctx level numcells st).compCanon < 0)
(hmatch :
Int.ofNat
(maketargetcell ctx (otherLeafSt ctx level numcells st).lab (otherLeafSt ctx level numcells st).ptn level tcLevel
(otherLeafSt ctx level numcells st).firsttc[level]!).fst = (otherLeafSt ctx level numcells st).firsttc[level]!)
:
∃ (outBest : Option (Key n)), ∃ (eventTrail : FrameTrail), OtherRun G ctx tcLevel (sf + 1) (runFuel + 1) level codes fs st
(otherNode ctx inf tcLevel (runFuel + 1) level numcells st).snd numcells best outBest trail eventTrail
(otherNode ctx inf tcLevel (runFuel + 1) level numcells st).fst ∧ OtherKeep ctx level st (otherNode ctx inf tcLevel (runFuel + 1) level numcells st).snd
A frozen off-path internal node that still agrees with the first path sweeps the first path's target cell when the stored hint is confirmed. The sweep bound is not the node key, but both are dominated by the incumbent.
theorem
Hex.GraphIso.Nauty.NodeInv.internalOther
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{inf tcLevel specFuel runFuel level numcells : Nat}
{codes bs fs : List Nat}
{st : SearchSt n}
{best : Option (Key n)}
{trail : FrameTrail}
(hg : ctx.g = rowsOf G)
(hinf : inf = n + 2)
(hn0 : 0 < n)
(ih : OtherTotal G ctx inf tcLevel runFuel)
(hlevel : 2 ≤ level)
(hpath : level = codes.length + 1)
(hspec : level + specFuel = n + 1)
(hfuel : n + 2 < level + (runFuel + 1))
(hcheap : st.noncheaplevel ≤ level)
(hdesc : CheapDesc ctx level st.noncheaplevel (refine ctx level st.lab st.ptn st.active numcells))
(hnode : NodeInv G ctx tcLevel level codes bs fs numcells st best trail)
(hlive : Live ctx level st trail)
(hpathOk : PathOk ctx (initPtn n (n + 2) (initialPartition G).snd) (initialPartition G).fst level st)
(horb : OrbSound (OrbConn st.genTrace.toList n) st.orbits n)
(hcoset : st.cosetindex < n)
(hdom : ∀ (b : Key n), best = some b → keyLe (pathLeafKey ctx fs st.firstlab) b)
(hnum : (refine ctx level st.lab st.ptn st.active numcells).numcells < n)
:
∃ (outBest : Option (Key n)), ∃ (eventTrail : FrameTrail), OtherRun G ctx tcLevel specFuel (runFuel + 1) level codes fs st
(otherNode ctx inf tcLevel (runFuel + 1) level numcells st).snd numcells best outBest trail eventTrail
(otherNode ctx inf tcLevel (runFuel + 1) level numcells st).fst ∧ OtherKeep ctx level st (otherNode ctx inf tcLevel (runFuel + 1) level numcells st).snd
Totality of an off-path internal node at the next executable fuel, given totality of every off-path node at the current fuel.
theorem
Hex.GraphIso.Nauty.NodeInv.leafTotal
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{inf tcLevel specFuel fuel level numcells : Nat}
{codes bs fs : List Nat}
{st : SearchSt n}
{best : Option (Key n)}
{trail : FrameTrail}
(hg : ctx.g = rowsOf G)
(hn0 : 0 < n)
(hlevel : 2 ≤ level)
(hpath : level = codes.length + 1)
(hcheap : st.noncheaplevel ≤ level)
(hnum : (refine ctx level st.lab st.ptn st.active numcells).numcells = n)
(hnode : NodeInv G ctx tcLevel level codes bs fs numcells st best trail)
(hlive : Live ctx level st trail)
(hsound : OrbSound (OrbConn st.genTrace.toList n) st.orbits n)
(hcoset : st.cosetindex < n)
(hdom : ∀ (b : Key n), best = some b → keyLe (pathLeafKey ctx fs st.firstlab) b)
:
∃ (outBest : Option (Key n)), OtherRun G ctx tcLevel (specFuel + 1) (fuel + 1) level codes fs st
(otherNode ctx inf tcLevel (fuel + 1) level numcells st).snd numcells best outBest trail trail
(otherNode ctx inf tcLevel (fuel + 1) level numcells st).fst ∧ OtherKeep ctx level st (otherNode ctx inf tcLevel (fuel + 1) level numcells st).snd
An off-path leaf at any executable fuel is total.
theorem
Hex.GraphIso.Nauty.OtherTotal.succ
{n k : Nat}
(G : Colored n k)
(ctx : Ctx n)
(inf tcLevel runFuel : Nat)
(ih : OtherTotal G ctx inf tcLevel runFuel)
:
OtherTotal G ctx inf tcLevel (runFuel + 1)
Every off-path node at the next executable fuel is total once every node at the current fuel is.