Partial scans and terminal forest graphs

Lemma 34 of [KKR18], arXiv:1602.03124v6, printed pp. 15–16, including a scan before saturation and the graph obtained by pruning every outgoing arc of the terminal copy. Certificates below are derived from the executable scan and run. They impose no even-delta-matroid assumption: incidence uniqueness, the old scans' saturation, and validity of the reference labeling suffice.

Main results

• scan_isFDAG: any partial feasible-partner scan preserves all six f-DAG conditions.
• search_terminal_isFDAG: both the actual partial forest and its terminal pruned graph are f-DAGs, including the isolated children retained in the variable support.

theorem Cslib.Logic.PL.CSP.Forest.Log.sameParent_of_mem_outgoing {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] {es : Log F} (hn : es.children.Nodup) {o : F.Occurrence} (ho : o ∈ es.outgoing) : es.SameParent o.var o.fst

With unique discovery variables, every outgoing port identifies its actual parent. The original constraint position, rather than the timestamp, is tested in step 4b.

theorem Cslib.Logic.PL.CSP.Forest.Grown.not_partner_of_unused {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} (hg : Grown sem f rs es) (hF : F.EdgeInstance) {a : DAG.Arc F} (ha : a ∈ es.arcs) (hi : a.incoming = true) {b : F.Occurrence} (hu : b ∉ es.used) (hc : a.occurrence.fst = b.fst) : ¬ValidLabeling sem (DAG.pairFlip f a.occurrence b)

A fresh port cannot be a feasible partner of an older incoming port. Saturation of the older scan, including step-4b skips, is the essential reason.

structure Cslib.Logic.PL.CSP.Forest.Partial {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) (e : Expansion F) : Prop

Local facts about the current expansion before its scan is complete. In contrast to Grown, no saturation condition on the current copy is asserted.

• grown : Grown sem f rs es

  Older scans really completed.

• visited : Log.Visited rs es e.input.var

  Step 2 chose a visited variable.

• unused : e.input ∉ es.used

  Step 2 chose an unused incidence.

• fresh (o : F.Occurrence) : o ∈ e.outputs → ¬Log.Visited rs es o.var

  Every inserted child is a new variable.

• distinct : (List.map Occurrence.var e.outputs).Nodup

  No child was inserted twice.

• feasible (o : F.Occurrence) : o ∈ e.outputs → o ∈ partners sem f e.input

  Every inserted child passed the actual partner test.

theorem Cslib.Logic.PL.CSP.Forest.Partial.port_unused {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} {e : Expansion F} (h : Partial sem f rs es e) {o : F.Occurrence} (ho : o = e.input ∨ o ∈ e.outputs) : o ∉ es.used

The new ports of a partial expansion are all unused in the older log.

theorem Cslib.Logic.PL.CSP.Forest.Partial.used_nodup {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} {e : Expansion F} (h : Partial sem f rs es e) : (Log.used (e :: es)).Nodup

Partial scans preserve uniqueness of used positional incidences.

theorem Cslib.Logic.PL.CSP.Forest.Partial.children_nodup {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} {e : Expansion F} (h : Partial sem f rs es e) : (Log.children (e :: es)).Nodup

Partial scans preserve unique discovery variables.

theorem Cslib.Logic.PL.CSP.Forest.Partial.isFDAG {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} {e : Expansion F} (h : Partial sem f rs es e) (hF : F.EdgeInstance) (hf : ValidLabeling sem f) : DAG.IsFDAG sem f (Log.toDAG rs (e :: es))

Every partial scan satisfies all six f-DAG conditions. The current copy need not yet be saturated, and the local relations need not be even delta-matroids.

theorem Cslib.Logic.PL.CSP.Forest.scan_isFDAG {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] {sem : Rel → List Bool → Bool} {f : F.OccurrenceLabeling Bool} (hF : F.EdgeInstance) (hf : ValidLabeling sem f) {rs : List V} {es : Log F} (hg : Grown sem f rs es) {input : F.Occurrence} (hv : Log.Visited rs es input.var) (hu : input ∉ es.used) (bs : List F.Occurrence) (hb : bs ⊆ partners sem f input) : DAG.IsFDAG sem f (Log.toDAG rs ({ input := input, outputs := (scan rs es input [] bs).outputs } :: es))

Lemma 34 during an actual scan, including every scanned prefix of the candidate list. The scan may have continued or stopped at its first meeting.

theorem Cslib.Logic.PL.CSP.Forest.scan_meeting_spec {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (rs : List V) (es : Log F) (input : F.Occurrence) (bs os : List F.Occurrence) {out : List F.Occurrence} {b : F.Occurrence} (hs : scan rs es input os bs = ScanResult.meeting out b) : b ∈ bs ∧ Log.Visited rs ({ input := input, outputs := out } :: es) b.var ∧ ¬Log.SameParent ({ input := input, outputs := out } :: es) b.var input.fst

Exact stopping conditions at the first meeting of an actual scan.

structure Cslib.Logic.PL.CSP.Forest.Meeting.Trace {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (sem : Rel → List Bool → Bool) (f : F.OccurrenceLabeling Bool) (m : Meeting F) : Prop

Local execution evidence for a terminal record. No graph invariant or event-correctness conclusion is a field; these facts follow from the actual partner scan.

• roots_eq : m.roots = Forest.roots f

  The initial nodes are exactly the inconsistent roots.

• expansion : Partial sem f m.roots m.older m.current

  Local insertion and frontier conditions of the partial expansion.

• partner : m.output ∈ partners sem f m.current.input

  The meeting port passed the feasible-pair test.

• visited : Log.Visited m.roots (m.current :: m.older) m.output.var

  The meeting variable is visited at scan termination.

• not_parent : ¬Log.SameParent (m.current :: m.older) m.output.var m.current.input.fst

  Source step 4b did not apply.

theorem Cslib.Logic.PL.CSP.Forest.Meeting.Trace.old_visited {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] {sem : Rel → List Bool → Bool} {f : F.OccurrenceLabeling Bool} {m : Meeting F} (h : Trace sem f m) : Log.Visited m.roots m.older m.output.var

A terminal partner cannot be a child just inserted at the current copy: its predecessor would have this original constraint position, triggering source step 4b.

theorem Cslib.Logic.PL.CSP.Forest.Meeting.Trace.output_unused {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] {sem : Rel → List Bool → Bool} {f : F.OccurrenceLabeling Bool} {m : Meeting F} (h : Trace sem f m) : m.output ∉ m.older.used

The second incoming port is fresh even if its variable was visited long ago. Old outgoing ports trigger step 4b; old incoming ports contradict saturation and current-input freshness.

theorem Cslib.Logic.PL.CSP.Forest.Meeting.Trace.pruned_arcs {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] {sem : Rel → List Bool → Bool} {f : F.OccurrenceLabeling Bool} {m : Meeting F} (h : Trace sem f m) : m.prunedDAG.arcs = insert { occurrence := m.output, time := List.length m.older, incoming := true } (insert { occurrence := m.current.input, time := List.length m.older, incoming := true } m.older.arcs.toFinset)

After pruning, exactly the two incoming arcs remain at the terminal copy. All older arcs survive, and the supported variables include the pruned, now isolated children.

theorem Cslib.Logic.PL.CSP.Forest.Meeting.Trace.pruned_isFDAG {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] {sem : Rel → List Bool → Bool} {f : F.OccurrenceLabeling Bool} {m : Meeting F} (h : Trace sem f m) (hF : F.EdgeInstance) (hf : ValidLabeling sem f) : DAG.IsFDAG sem f m.prunedDAG

The terminal graph of Lemma 34's moreover clause is an f-DAG. This proves the claim for the executable pruning operation, including its retained isolated child support.

def Cslib.Logic.PL.CSP.Forest.Result.Events {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (P : Meeting F → Prop) : Result F → Prop

A property of every terminal event, vacuous for exhaustion.

theorem Cslib.Logic.PL.CSP.Forest.run_trace {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (sem : Rel → List Bool → Bool) (f : F.OccurrenceLabeling Bool) (hF : F.EdgeInstance) (es : Log F) (remaining : List F.Occurrence) (hg : Grown sem f (roots f) es) (hu : ∀ o ∈ remaining, o ∉ es.used) : Result.Events (Meeting.Trace sem f) (run sem f (roots f) es remaining)

Execution derives terminal scan evidence, independently of graph and event correctness.

theorem Cslib.Logic.PL.CSP.Forest.search_trace {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (sem : Rel → List Bool → Bool) (f : F.OccurrenceLabeling Bool) (hF : F.EdgeInstance) : Result.Events (Meeting.Trace sem f) (search sem f)

Every terminal event in a fresh run has evidence obtained from its real scans.

theorem Cslib.Logic.PL.CSP.Forest.search_terminal_isFDAG {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (sem : Rel → List Bool → Bool) (f : F.OccurrenceLabeling Bool) (hF : F.EdgeInstance) (hf : ValidLabeling sem f) : Result.Events (fun (m : Meeting F) => DAG.IsFDAG sem f m.toDAG ∧ DAG.IsFDAG sem f m.prunedDAG) (search sem f)

Lemma 34 for both terminal graphs actually returned by a fresh search. No event or forest-correctness premise and no even-delta-matroid hypothesis is required.