def
Hex.GraphIso.Nauty.prepareOther
{n : Nat}
(ctx : Ctx n)
(tcLevel level numcells : Nat)
(st : Search n)
:
Refinement, comparison and target selection at an off-path node.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Hex.GraphIso.Nauty.maketargetcell_nonempty
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel level numcells : Nat}
{st : Search n}
(hint : Int)
(hn0 : 0 < n)
(hlevel : 1 ≤ level)
(hok : SearchOk G level numcells st)
(hnc : numcells < n)
:
A target selected from a non-discrete reached partition contains a vertex.
theorem
Hex.GraphIso.Nauty.chooseTarget_phase
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel level numcells : Nat}
{st : Search n}
(hn0 : 0 < n)
(hlevel : 1 ≤ level)
(hok : SearchOk G level numcells st)
:
A continuing node with an upward comparison has a first child to settle that comparison before any sibling filter can run.
theorem
Hex.GraphIso.Nauty.NodePre.phase
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel level numcells : Nat}
{st : Search n}
(h : NodePre G ctx tcLevel level numcells st)
(hn0 : 0 < n)
:
An off-path node enters its sweep with a settled comparison or a nonempty target whose first child will settle it.
theorem
Hex.GraphIso.Nauty.NodePre.prepare
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel level numcells : Nat}
{st : Search n}
(hin : NodePre G ctx tcLevel level numcells st)
(hn0 : 0 < n)
(hgsz : ctx.g.size = n)
(hsymm : ∀ (u v : Nat), u < n → v < n → ctx.g[u]!.mem v = ctx.g[v]!.mem u)
(hloop : ∀ (v : Nat), v < n → ctx.g[v]!.mem v = false)
:
have p := prepareOther ctx tcLevel level numcells st;
have t := p.snd.snd;
have state := t.snd.snd.snd;
SearchOk G level p.fst state ∧ RunInv G ctx state ∧ History ctx tcLevel level level p.fst state ∧ (have c := classify ctx level p.fst state;
RunInv G ctx (leafExit c.fst level c.snd).snd) ∧ ((classify ctx level p.fst state).fst = Generic.Leaf.internal →
SweepPre G ctx tcLevel false level p.fst t.fst.toNat ((t.snd.fst.nextElem none).getD 0)
(t.snd.fst.nextElem none) t.snd.fst (cheapCheck false level state))
Preparing an off-path node supplies the checked leaf action and the complete sweep precondition whenever classification continues.
theorem
Hex.GraphIso.Nauty.SweepPre.child
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel level numcells tc tv1 tv : Nat}
{first : Bool}
{cell : VSet n}
{st : Search n}
(hin : SweepPre G ctx tcLevel first level numcells tc tv1 (some tv) cell st)
(hn0 : 0 < n)
(hgsz : ctx.g.size = n)
(hsymm : ∀ (u v : Nat), u < n → v < n → ctx.g[u]!.mem v = ctx.g[v]!.mem u)
:
NodePre G ctx tcLevel (level + 1) (numcells + 1) (Nauty.child first level tc tv st)
An eligible sweep entry supplies the precondition of its off-path child.
theorem
Hex.GraphIso.Nauty.SweepPre.next
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel level numcells tc tv1 tv : Nat}
{first : Bool}
{cell smaller : VSet n}
{st : Search n}
(h : SweepPre G ctx tcLevel first level numcells tc tv1 (some tv) cell st)
(hsub : ∀ (v : Nat), smaller.mem v = true → cell.mem v = true)
:
Advancing to a surviving larger entry retains the sweep's local invariants.
theorem
Hex.GraphIso.Nauty.SweepPre.restore
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel fuel level numcells tc tv1 tv : Nat}
{first : Bool}
{cell : VSet n}
{st : Search n}
(hin : SweepPre G ctx tcLevel first level numcells tc tv1 (some tv) cell st)
(hn0 : 0 < n)
(hgsz : ctx.g.size = n)
(hsymm : ∀ (u v : Nat), u < n → v < n → ctx.g[u]!.mem v = ctx.g[v]!.mem u)
(hstored :
RunInv G ctx (node false ctx (n + 2) tcLevel fuel (level + 1) (numcells + 1) (Nauty.child first level tc tv st)).snd)
:
have out := (node false ctx (n + 2) tcLevel fuel (level + 1) (numcells + 1) (Nauty.child first level tc tv st)).snd;
have left :=
{ lab := out.lab, ptn := out.ptn, active := out.active, orbits := out.orbits, fixedpts := out.fixedpts.erase tv,
autos := out.autos, wsCap := out.wsCap, firstcode := out.firstcode, canoncode := out.canoncode,
firsttc := out.firsttc, firstlab := out.firstlab, canonlab := out.canonlab, canong := out.canong,
samerows := out.samerows, compCanon := out.compCanon, eqlevFirst := out.eqlevFirst, eqlevCanon := out.eqlevCanon,
gcaFirst := out.gcaFirst, gcaCanon := out.gcaCanon, canonlevel := out.canonlevel,
noncheaplevel := out.noncheaplevel, allsamelevel := out.allsamelevel, cosetindex := out.cosetindex,
stabvertex := out.stabvertex, numnodes := out.numnodes, tctotal := out.tctotal, canupdates := out.canupdates,
numorbits := out.numorbits, numgenerators := out.numgenerators, numbadleaves := out.numbadleaves,
maxlevel := out.maxlevel, order := out.order, genTrace := out.genTrace, workperm := out.workperm };
SweepPre G ctx tcLevel first level numcells tc tv1 (some tv) cell (recover (n + 2) level left)
Returning from the actual off-path child restores the parent history, fixed points, and local stabilizer ledger.