structure
Hex.GraphIso.Nauty.Generic.ReferencePolicy
{n : Nat}
{σ α γ : Type}
[Policy σ n]
(ctx : γ)
(inf tcLevel : Nat)
(project : σ → α)
:
Local operations outside the first descent preserve a projection of the policy state, such as the first labelling, codes, and target array.
- visit (level numcells : Nat) (st : σ) : project (Policy.visit ctx level numcells st).snd.snd = project st
- classify (level numcells : Nat) (st : σ) : project (Policy.classify ctx level numcells st).snd = project st
- leaf (leaf : Leaf) (level : Nat) (st : σ) : project (Policy.leafExit leaf level st).snd = project st
- cheap (first : Bool) (level : Nat) (st : σ) : project (Policy.cheapCheck first level st) = project st
- child (first : Bool) (level tc tv : Nat) (st : σ) : project (Policy.child first level tc tv st) = project st
- afterSweep (first : Bool) (level size index : Nat) (st : σ) : project (Policy.afterSweep first level size index st) = project st
Instances For
theorem
Hex.GraphIso.Nauty.Generic.ReferencePolicy.stable
{n : Nat}
{σ α γ : Type}
[Policy σ n]
{ctx : γ}
{inf tcLevel : Nat}
{project : σ → α}
(h : ReferencePolicy ctx inf tcLevel project)
(ref : α)
:
StablePolicy ctx inf tcLevel fun (st : σ) => project st = ref
Equal projections preserve the invariant of matching a fixed reference.
theorem
Hex.GraphIso.Nauty.Generic.node_reference
{n : Nat}
{σ α γ : Type}
[Policy σ n]
{ctx : γ}
{inf tcLevel : Nat}
{project : σ → α}
(h : ReferencePolicy ctx inf tcLevel project)
(fuel level numcells : Nat)
(st : σ)
:
An off-path node preserves the projected reference fields.
theorem
Hex.GraphIso.Nauty.Generic.sweep_reference
{n : Nat}
{σ α γ : Type}
[Policy σ n]
{ctx : γ}
{inf tcLevel : Nat}
{project : σ → α}
(h : ReferencePolicy ctx inf tcLevel project)
(first : Bool)
(fuel cfuel level numcells tc tv1 index : Nat)
(cursor : Option Nat)
(cell : VSet n)
(st : σ)
(hpast : Past first tv1 cursor)
:
Later siblings preserve the projected reference fields.