Exhaustion of the actual positional frontier

The search of [KKR18], arXiv:1602.03124v6, Algorithm 1 step 2 (printed p. 10), exhausts exactly when every incidence of every visited variable has been used. This is a theorem about a fresh executable run, without a search-completeness hypothesis. Forest.Optimality combines this coverage with even-delta-matroid exchange and a counting argument to prove Lemma 45 for a fresh exhausted run.

Main results

• search_exhausted_frontier: a fresh exhausted run has no unused incidence at a visited variable.

def Cslib.Logic.PL.CSP.Forest.Covers {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (es : Log F) (remaining : List F.Occurrence) : Prop

Every port not yet used remains in the finite work list. Repeated labels and sparse labels do not change this positional coverage property.

theorem Cslib.Logic.PL.CSP.Forest.Covers.next {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} {es : Log F} {remaining : List F.Occurrence} (hc : Covers es remaining) (e : Expansion F) : Covers (e :: es) (List.filter (fun (a : F.Occurrence) => decide (a ∉ Log.used (e :: es))) (remaining.erase e.input))

Coverage survives the exact erase-and-filter operation performed on continuation.

theorem Cslib.Logic.PL.CSP.Forest.run_exhausted_frontier {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (sem : Rel → List Bool → Bool) (f : F.OccurrenceLabeling Bool) (rs : List V) (es : Log F) (remaining : List F.Occurrence) (hc : Covers es remaining) {out : Log F} (hr : run sem f rs es remaining = Result.exhausted out) (o : F.Occurrence) : Log.Visited rs out o.var → o ∈ out.used

A returned exhausted forest has no unused port at a visited variable, provided its initial work list covered every unused port. No event or optimality property is assumed.

theorem Cslib.Logic.PL.CSP.Forest.search_exhausted_frontier {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (sem : Rel → List Bool → Bool) (f : F.OccurrenceLabeling Bool) {out : Log F} (hr : search sem f = Result.exhausted out) (o : F.Occurrence) : Log.Visited (roots f) out o.var → o ∈ out.used

Fresh-run exhaustion of step 2, paid for by the actual incidence list. This does not replace the separate optimality conclusion of source Lemma 45.