Reversing and joining indexed incidence trails

These elementary list operations support parent-path assembly in the edge-CSP forest search. Reversal preserves the underlying trail predicate. Prefix validity requires separate reasoning about the selected DAG subpaths; no closure of arbitrary f-walks under reversal is asserted.

Main definitions

• Cslib.Logic.PL.CSP.Walk.reverse: reverse the step order and swap each incidence pair.
• Cslib.Logic.PL.CSP.Walk.append: concatenate candidate step lists.

Main results

• Cslib.Logic.PL.CSP.Walk.IsWalk.reverse: reversal preserves incidence trails.
• Cslib.Logic.PL.CSP.Walk.IsWalk.append: linked disjoint trails concatenate.
• Cslib.Logic.PL.CSP.Walk.flip_reverse: reversal leaves the flipped incidence set unchanged.
• Cslib.Logic.PL.CSP.Walk.IsFPrefix.take: closure under prefixes.
• Cslib.Logic.PL.CSP.Walk.IsFPrefix.not_inconsistent_finish_take: consistency at positive proper endpoints.

def Cslib.Logic.PL.CSP.Walk.reverse {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (w : F.Walk) : F.Walk

Reverse the step order and swap the two incidences of each candidate step.

def Cslib.Logic.PL.CSP.Walk.append {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (w z : F.Walk) : F.Walk

Concatenate candidate steps, retaining the first candidate's starting variable.

theorem Cslib.Logic.PL.CSP.Walk.edgesOf_reverse_map_swap {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (s : List (F.Occurrence × F.Occurrence)) : edgesOf (List.map Prod.swap s.reverse) = (edgesOf s).reverse

Reversing all incidence pairs reverses the traversed incidence list.

@[simp]

theorem Cslib.Logic.PL.CSP.Walk.edges_reverse {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (w : F.Walk) : w.reverse.edges = w.edges.reverse

A reversed candidate traverses precisely the original incidences in reverse order.

theorem Cslib.Logic.PL.CSP.Walk.Linked.finishFrom_reverse {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} {v : V} {s : List (F.Occurrence × F.Occurrence)} (h : Linked v s) : finishFrom (finishFrom v s) (List.map Prod.swap s.reverse) = v

A linked candidate returns to its original start when read in reverse.

theorem Cslib.Logic.PL.CSP.Walk.Linked.reverse {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} {v : V} {s : List (F.Occurrence × F.Occurrence)} (h : Linked v s) : Linked (finishFrom v s) (List.map Prod.swap s.reverse)

Incidence linkage is preserved by reversing a trail's candidate steps.

@[simp]

theorem Cslib.Logic.PL.CSP.Walk.finish_reverse {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (w : F.Walk) (h : Linked w.start w.steps) : w.reverse.finish = w.start

The endpoint of a reversed linked candidate is its original starting variable.

theorem Cslib.Logic.PL.CSP.Walk.IsWalk.reverse {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} {w : F.Walk} (h : w.IsWalk) : w.reverse.IsWalk

Reversing a trail preserves linkage and absence of repeated incidences.

@[simp]

theorem Cslib.Logic.PL.CSP.Walk.edges_append {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (w z : F.Walk) : (w.append z).edges = w.edges ++ z.edges

Concatenation appends the two traversed incidence lists.

theorem Cslib.Logic.PL.CSP.Walk.IsWalk.append {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} {w z : F.Walk} (hw : w.IsWalk) (hz : z.IsWalk) (hend : w.finish = z.start) (hd : w.edges.Disjoint z.edges) : (w.append z).IsWalk

Linked incidence trails concatenate when their incidence lists are disjoint.

theorem Cslib.Logic.PL.CSP.Walk.flip_reverse {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (w : F.Walk) (f : F.OccurrenceLabeling Bool) : w.reverse.flip f = w.flip f

The set of flipped incidences is independent of traversal orientation.

theorem Cslib.Logic.PL.CSP.Walk.PrefixValid.take {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} {sem : Rel → List Bool → Bool} {f : F.OccurrenceLabeling Bool} {s : List (F.Occurrence × F.Occurrence)} (h : PrefixValid sem f s) (n : ℕ) : PrefixValid sem f (List.take n s)

Every shorter candidate prefix inherits validity after each of its prefixes.

theorem Cslib.Logic.PL.CSP.Walk.InternallyConsistent.take {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} {f : F.OccurrenceLabeling Bool} {s : List (F.Occurrence × F.Occurrence)} (h : InternallyConsistent f s) (n : ℕ) : InternallyConsistent f (List.take n s)

Internal consistency is inherited by a shorter candidate prefix.

theorem Cslib.Logic.PL.CSP.Walk.IsFPrefix.take {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} {sem : Rel → List Bool → Bool} {f : F.OccurrenceLabeling Bool} {w : F.Walk} (h : IsFPrefix sem f w) (n : ℕ) : IsFPrefix sem f (w.take n)

Every variable-ended prefix inherits the f-prefix conditions.

theorem Cslib.Logic.PL.CSP.Walk.InternallyConsistent.not_inconsistent_finishFrom_take {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} {f : F.OccurrenceLabeling Bool} {s : List (F.Occurrence × F.Occurrence)} (h : InternallyConsistent f s) (v : V) {n : ℕ} (hn : 0 < n) (hlt : n < s.length) : ¬Inconsistent f (finishFrom v (List.take n s))

A positive proper prefix ends at an original internal variable.

theorem Cslib.Logic.PL.CSP.Walk.IsFPrefix.not_inconsistent_finish_take {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} {sem : Rel → List Bool → Bool} {f : F.OccurrenceLabeling Bool} {w : F.Walk} (h : IsFPrefix sem f w) {n : ℕ} (hn : 0 < n) (hlt : n < w.steps.length) : ¬Inconsistent f (w.take n).finish

The endpoint of a positive proper f-prefix is consistent in the original labeling.