theorem
Hex.GraphIso.Nauty.Generic.CursorFuel.next
{n cfuel tv : Nat}
{cell : VSet n}
(h : n ≤ tv + (cfuel + 1))
:
CursorFuel n cfuel (cell.nextElem (some tv))
Advancing a bitset cursor consumes at most one unit of the bound.
def
Hex.GraphIso.Nauty.Generic.fuelContract
{n k : Nat}
{σ : Type}
(G : Colored n k)
(view : σ → Search n)
:
Contract σ n
Partition reachability together with conditional absence of exhaustion. The partition assertions hold even when the bounds are insufficient.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Hex.GraphIso.Nauty.Generic.fuel_node_reach
{n k : Nat}
{σ : Type}
{G : Colored n k}
{view : σ → Search n}
{fuel : Nat}
{f : NodeFn σ}
(h : (fuelContract G view).nodeValid fuel f)
:
(reachContract G view).nodeValid fuel f
Forget the node exhaustion guarantee while retaining its frame effect.
theorem
Hex.GraphIso.Nauty.Generic.fuel_sweep_reach
{n k : Nat}
{σ : Type}
{G : Colored n k}
{view : σ → Search n}
{fuel cfuel : Nat}
{f : SweepFn σ n}
(h : (fuelContract G view).sweepValid fuel cfuel f)
:
(reachContract G view).sweepValid fuel cfuel f
Forget the sweep exhaustion guarantee while retaining its frame effect.
theorem
Hex.GraphIso.Nauty.Generic.nodeStep_safe
{n k : Nat}
{σ γ : Type}
[Policy σ n]
{G : Colored n k}
{ctx : γ}
{inf tcLevel : Nat}
{view : σ → Search n}
(h : ReachPolicy G ctx inf tcLevel view)
(hleaf : ∀ (leaf : Leaf) (level : Nat) (st : σ), (Policy.leafExit leaf level st).fst ≠ Exit.fuel)
{fuel : Nat}
{next : SweepFn σ n}
(hnext : (fuelContract G view).sweepValid fuel (n + 1) next)
(first : Bool)
(level numcells : Nat)
(st : σ)
(hlevel : 1 ≤ level)
(hok : SearchOk G level numcells (view st))
(hfuel : n + 1 ≤ level + (fuel + 1))
:
Refinement and local node decisions cannot exhaust a sufficient bound.
theorem
Hex.GraphIso.Nauty.Generic.sweepStep_safe
{n k : Nat}
{σ γ : Type}
[Policy σ n]
{G : Colored n k}
{ctx : γ}
{inf tcLevel : Nat}
{view : σ → Search n}
(h : ReachPolicy G ctx inf tcLevel view)
{fuel cfuel : Nat}
{descend : NodeFn σ}
{next : SweepFn σ n}
(hdescend : (fuelContract G view).nodeValid fuel descend)
(hnext : (fuelContract G view).sweepValid fuel cfuel next)
(first : Bool)
(level numcells tc tv1 tv index : Nat)
(cell : VSet n)
(st : σ)
(hlevel : 1 ≤ level)
(hok : SearchOk G level numcells (view st))
(htarget : Target view level tc cell st)
(htv : cell.mem tv = true)
(hfuel : n ≤ level + fuel)
(hcursor : n ≤ tv + (cfuel + 1))
:
The child increases the level and the remaining sweep increases the cursor, so both recursive calls have sufficient bounds.
theorem
Hex.GraphIso.Nauty.Generic.fuel_sound
{n k : Nat}
{σ γ : Type}
[Policy σ n]
{G : Colored n k}
{ctx : γ}
{inf tcLevel : Nat}
{view : σ → Search n}
(h : ReachPolicy G ctx inf tcLevel view)
(hleaf : ∀ (leaf : Leaf) (level : Nat) (st : σ), (Policy.leafExit leaf level st).fst ≠ Exit.fuel)
:
SoundPolicy ctx inf tcLevel (fuelContract G view)
The partition rules and non-exhausting leaf actions suffice for the generic search's level and cursor bounds.
theorem
Hex.GraphIso.Nauty.Generic.node_noFuel
{n k : Nat}
{σ γ : Type}
[Policy σ n]
{G : Colored n k}
{ctx : γ}
{inf tcLevel : Nat}
{view : σ → Search n}
(h : ReachPolicy G ctx inf tcLevel view)
(hleaf : ∀ (leaf : Leaf) (level : Nat) (st : σ), (Policy.leafExit leaf level st).fst ≠ Exit.fuel)
(first : Bool)
(fuel level numcells : Nat)
(st : σ)
(hlevel : 1 ≤ level)
(hok : SearchOk G level numcells (view st))
(hfuel : n + 1 ≤ level + fuel)
:
A valid node cannot exhaust a bound reaching beyond the maximum level.
theorem
Hex.GraphIso.Nauty.Generic.sweep_noFuel
{n k : Nat}
{σ γ : Type}
[Policy σ n]
{G : Colored n k}
{ctx : γ}
{inf tcLevel : Nat}
{view : σ → Search n}
(h : ReachPolicy G ctx inf tcLevel view)
(hleaf : ∀ (leaf : Leaf) (level : Nat) (st : σ), (Policy.leafExit leaf level st).fst ≠ Exit.fuel)
(first : Bool)
(fuel cfuel level numcells tc tv1 index : Nat)
(cursor : Option Nat)
(cell : VSet n)
(st : σ)
(hlevel : 1 ≤ level)
(hok : SearchOk G level numcells (view st))
(htarget : Target view level tc cell st)
(hcursor : ∀ (v : Nat), cursor = some v → cell.mem v = true)
(hfuel : n ≤ level + fuel)
(hcfuel : CursorFuel n cfuel cursor)
:
A valid sweep cannot exhaust sufficient level and cursor bounds.