def
Hex.GraphIso.Nauty.Generation.ChildPath
{n : Nat}
(ctx : Ctx n)
(tcLevel boundary level : Nat)
(st : RefineSt n)
(tc : Nat)
(targets : List Nat)
(key : Key n)
(o : Nat)
:
The reference occurrence sought in one frozen child of a sweep.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[reducible, inline]
abbrev
Hex.GraphIso.Nauty.Generation.PathCover
{n : Nat}
(ctx : Ctx n)
(tcLevel boundary level : Nat)
(st : RefineSt n)
(tc len : Nat)
(targets : List Nat)
(key : Key n)
(tcell : VSet n)
(cursor : Option Nat)
:
Coverage of references carrying a saved uniformity boundary. The sweep accounting is shared with ordinary leaf coverage.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Hex.GraphIso.Nauty.Generation.PathCover.advance
{n : Nat}
{ctx : Ctx n}
{tcLevel boundary level tc len : Nat}
{st : RefineSt n}
{targets : List Nat}
{key : Key n}
{tcell : VSet n}
{cursor : Option Nat}
(h : PathCover ctx tcLevel boundary level st tc len targets key tcell cursor)
{tv : Nat}
(hnext : tcell.nextElem cursor = some tv)
(hcur : ∀ (o : Nat), o < len → st.lab[tc + o]! = tv → ¬ChildPath ctx tcLevel boundary level st tc targets key o)
:
A child proved to have no matching occurrence advances the sweep.
theorem
Hex.GraphIso.Nauty.Generation.PathCover.filterDesc
{n : Nat}
{ctx : Ctx n}
{tcLevel boundary level tc len : Nat}
{st : RefineSt n}
{targets : List Nat}
{key : Key n}
{tcell tcell' : VSet n}
{cursor : Option Nat}
(h : PathCover ctx tcLevel boundary level st tc len targets key tcell cursor)
(hstep :
∀ (o : Nat),
ChildLive st.lab tc len tcell cursor o →
tcell'.mem st.lab[tc + o]! = true ∨ ∃ (j : Nat), j < len ∧ ChildPath ctx tcLevel boundary level st tc targets key o = ChildPath ctx tcLevel boundary level st tc targets key j ∧ st.lab[tc + j]! < st.lab[tc + o]!)
(hsub : ∀ (v : Nat), tcell'.mem v = true → tcell.mem v = true)
:
PathCover ctx tcLevel boundary level st tc len targets key tcell' cursor
A descending filter preserves absence coverage through arbitrarily many earlier filters. Equality here is equality of occurrence propositions, so it retains the target hints as well as the complete leaf key.
theorem
Hex.GraphIso.Nauty.Generation.PathCover.filterAutom
{n : Nat}
{ctx : Ctx n}
{tcLevel boundary level tc len : Nat}
{st : RefineSt n}
{targets : List Nat}
{key : Key n}
{tcell tcell' : VSet n}
{cursor : Option Nat}
(h : PathCover ctx tcLevel boundary level st tc len targets key tcell cursor)
{e : Nat}
(hok : IterOk ctx level st)
(hlvl : level < n)
(hgsz : ctx.g.size = n)
(hcell : (tc, e) ∈ cells st.ptn level n)
(hne : tc < e)
(hlen : len = e + 1 - tc)
(hdrop :
∀ (o : Nat),
ChildLive st.lab tc len tcell cursor o →
tcell'.mem st.lab[tc + o]! = false →
∃ (γ : Array Nat), checkAutom ctx.g γ = true ∧ CellStab st.ptn level st.lab γ ∧ γ[st.lab[tc + o]!]! < st.lab[tc + o]!)
(hsub : ∀ (v : Nat), tcell'.mem v = true → tcell.mem v = true)
:
PathCover ctx tcLevel boundary level st tc len targets key tcell' cursor
A checked cell stabilizer transports the entire reference occurrence through a pruning step. It need not belong to the emitted generator list.
theorem
Hex.GraphIso.Nauty.Generation.PathCover.longprune
{n : Nat}
{ctx : Ctx n}
{tcLevel boundary level tc len : Nat}
{st : RefineSt n}
{targets : List Nat}
{key : Key n}
{tcell : VSet n}
{cursor : Option Nat}
(h : PathCover ctx tcLevel boundary level st tc len targets key tcell cursor)
{e : Nat}
(hok : IterOk ctx level st)
(hlvl : level < n)
(hgsz : ctx.g.size = n)
(hcell : (tc, e) ∈ cells st.ptn level n)
(hne : tc < e)
(hlen : len = e + 1 - tc)
{fixedpts : VSet n}
{autos : Array (VSet n × VSet n)}
(haut :
∀ (p : VSet n × VSet n),
p ∈ autos.toList → fixedpts.subset p.fst = true → PairOk ctx.g st.ptn st.lab level p.fst p.snd)
:
PathCover ctx tcLevel boundary level st tc len targets key (Nauty.longprune tcell fixedpts autos) cursor
The off-path long-prune ledger preserves every sought reference.
theorem
Hex.GraphIso.Nauty.Generation.PathCover.shortprune
{n : Nat}
{ctx : Ctx n}
{tcLevel boundary level tc len : Nat}
{st : RefineSt n}
{targets : List Nat}
{key : Key n}
{tcell : VSet n}
{cursor : Option Nat}
(h : PathCover ctx tcLevel boundary level st tc len targets key tcell cursor)
{e : Nat}
(hok : IterOk ctx level st)
(hlvl : level < n)
(hgsz : ctx.g.size = n)
(hcell : (tc, e) ∈ cells st.ptn level n)
(hne : tc < e)
(hlen : len = e + 1 - tc)
{out : SearchSt n}
(hlast : ∀ (fix mcr : VSet n), out.autos.back? = some (fix, mcr) → PairOk ctx.g st.ptn st.lab level fix mcr)
:
PathCover ctx tcLevel boundary level st tc len targets key (Nauty.shortprune tcell out) cursor
The off-path short-prune ledger preserves every sought reference, including when the last pair is implicit.
theorem
Hex.GraphIso.Nauty.Generation.PathCover.finish
{n : Nat}
{ctx : Ctx n}
{tcLevel boundary level tc len : Nat}
{st : RefineSt n}
{targets : List Nat}
{key : Key n}
{tcell : VSet n}
{cursor : Option Nat}
(h : PathCover ctx tcLevel boundary level st tc len targets key tcell cursor)
(hnext : tcell.nextElem cursor = none)
(o : Nat)
:
Exhausting a sweep with no matching visited child rules out every matching child of the original target window.
theorem
Hex.GraphIso.Nauty.Generation.PathCover.smaller
{n : Nat}
{ctx : Ctx n}
{tcLevel boundary level tc len : Nat}
{st : RefineSt n}
{targets : List Nat}
{key : Key n}
{tcell : VSet n}
{cursor : Option Nat}
(h : PathCover ctx tcLevel boundary level st tc len targets key tcell cursor)
{tv o : Nat}
(hnext : tcell.nextElem cursor = some tv)
(ho : o < len)
(hlt : st.lab[tc + o]! < tv)
:
An earlier original child has no matching occurrence, even if an older pruning filter removed it from the current target set.
theorem
Hex.GraphIso.Nauty.Generation.PathCover.carrier
{n : Nat}
{ctx : Ctx n}
{tcLevel boundary level tc len : Nat}
{st : RefineSt n}
{targets : List Nat}
{key : Key n}
{tcell : VSet n}
{cursor : Option Nat}
(h : PathCover ctx tcLevel boundary level st tc len targets key tcell cursor)
{tv e oRef : Nat}
{ref cur : Array Nat}
{store : Array (Array Nat)}
(hnext : tcell.nextElem cursor = some tv)
(hok : IterOk ctx level st)
(hlvl : level < n)
(hgsz : ctx.g.size = n)
(hcell : (tc, e) ∈ cells st.ptn level n)
(hne : tc < e)
(hlen : len = e + 1 - tc)
(href : oRef < len)
(habsent : ¬ChildPath ctx tcLevel boundary level st tc targets key oRef)
(hcarrier : CellCarrier ctx st.ptn level st.lab ref cur store)
(hatRef : ref[tc]! = st.lab[tc + oRef]!)
(hatCur : cur[tc]! = tv)
:
A recorded carrier transfers absence from its reference child to the current child. This consumes canonical returns without claiming that the interrupted child was exhaustively searched.
theorem
Hex.GraphIso.Nauty.Generation.PathCover.reference
{n : Nat}
{ctx : Ctx n}
{tcLevel boundary level tc len : Nat}
{st : RefineSt n}
{targets : List Nat}
{key : Key n}
{tcell : VSet n}
{cursor : Option Nat}
(h : PathCover ctx tcLevel boundary level st tc len targets key tcell cursor)
{tv e oRef : Nat}
{ref cur : Array Nat}
{store : Array (Array Nat)}
(hnext : tcell.nextElem cursor = some tv)
(hok : IterOk ctx level st)
(hlvl : level < n)
(hgsz : ctx.g.size = n)
(hcell : (tc, e) ∈ cells st.ptn level n)
(hne : tc < e)
(hlen : len = e + 1 - tc)
(href : oRef < len)
(hearlier : st.lab[tc + oRef]! < tv)
(hcarrier : CellCarrier ctx st.ptn level st.lab ref cur store)
(hatRef : ref[tc]! = st.lab[tc + oRef]!)
(hatCur : cur[tc]! = tv)
:
A carrier to an earlier reference child discharges the current child using the ranked coverage invariant, including references removed by previous filters.