Incidence trails and prefix-valid edge-CSP walks

A step is a pair of actual ordered occurrences in one constraint. Traversed incidences are never reused, while constraint positions may repeat. Closed and length-zero trails are allowed. Walk.IsFWalk additionally requires distinct variable endpoints, consistent internal variables, and validity after every variable-ended prefix. This is Definitions 22–23 of [KKR18], arXiv v6, printed p. 9.

Main definitions

• Walk.IsWalk: a trail of indexed incidence pairs, allowing closed walks.
• Walk.IsFWalk: distinct endpoints, consistent internal variables, and prefix validity.
• Walk.IsAugmenting: an f-walk with two defective endpoints.

Main results

• Walk.IsWalk.partner_transition: consecutive steps use the partner involution.
• Walk.IsFPrefix.valid_take: every variable-ended prefix flip is valid.
• Walk.IsAugmenting.card_defects_flip_add_two: augmentation removes exactly two defects.

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

A variable-to-variable trail is represented by its starting variable and its sequence of incidence pairs. IsWalk checks incidence adjacency and absence of repeated incidences.

• start : V

  Starting variable, also the endpoint of a length-zero trail.

• steps : List (F.Occurrence × F.Occurrence)

  Ordered variable-to-variable steps, each represented by its two incidences.

def Cslib.Logic.PL.CSP.Walk.finishFrom {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (v : V) : List (F.Occurrence × F.Occurrence) → V

The terminal variable, also defined for length-zero walks.

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

Terminal variable of a walk.

def Cslib.Logic.PL.CSP.Walk.edgesOf {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (s : List (F.Occurrence × F.Occurrence)) : List F.Occurrence

Traversed incidences, in traversal order.

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

Traversed incidences of a walk.

def Cslib.Logic.PL.CSP.Walk.flipSteps {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (f : F.OccurrenceLabeling Bool) : List (F.Occurrence × F.Occurrence) → F.OccurrenceLabeling Bool

Flip each incidence in a list of steps, in order. For a trail this is the set flip.

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

Flip the incidences of a walk.

def Cslib.Logic.PL.CSP.Walk.Linked {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (v : V) : List (F.Occurrence × F.Occurrence) → Prop

Consecutive steps meet at their variable endpoints; the two incidences of each step belong to the same positional constraint.

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

An incidence trail, allowing closed trails and repeated constraint positions.

def Cslib.Logic.PL.CSP.Walk.PrefixValid {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (sem : Rel → List Bool → Bool) : F.OccurrenceLabeling Bool → List (F.Occurrence × F.Occurrence) → Prop

Every intermediate labeling (including the initial one) is valid.

def Cslib.Logic.PL.CSP.Walk.InternallyConsistent {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (f : F.OccurrenceLabeling Bool) : List (F.Occurrence × F.Occurrence) → Prop

Internal variable endpoints are consistent in the original labeling.

def Cslib.Logic.PL.CSP.Walk.IsFPrefix {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (sem : Rel → List Bool → Bool) (f : F.OccurrenceLabeling Bool) (w : F.Walk) : Prop

The prefix conditions of an f-walk, permitting a length-zero initial prefix.

def Cslib.Logic.PL.CSP.Walk.IsFWalk {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (sem : Rel → List Bool → Bool) (f : F.OccurrenceLabeling Bool) (w : F.Walk) : Prop

An f-walk has distinct variable endpoints, consistent internal variables, and a valid labeling after every variable-ended prefix. Final validity alone does not suffice.

def Cslib.Logic.PL.CSP.Walk.IsAugmenting {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (sem : Rel → List Bool → Bool) (f : F.OccurrenceLabeling Bool) (w : F.Walk) : Prop

An augmenting f-walk has two f-inconsistent variable endpoints.

def Cslib.Logic.PL.CSP.Walk.snoc {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (w : F.Walk) (o p : F.Occurrence) : F.Walk

Append a variable-to-variable step.

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

A prefix ends at a variable, so it contains whole incidence pairs.

@[simp]

theorem Cslib.Logic.PL.CSP.Walk.edgesOf_cons {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (o p : F.Occurrence) (s : List (F.Occurrence × F.Occurrence)) : edgesOf ((o, p) :: s) = o :: p :: edgesOf s

@[simp]

theorem Cslib.Logic.PL.CSP.Walk.edgesOf_append {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (s t : List (F.Occurrence × F.Occurrence)) : edgesOf (s ++ t) = edgesOf s ++ edgesOf t

@[simp]

theorem Cslib.Logic.PL.CSP.Walk.finishFrom_append {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (v : V) (s t : List (F.Occurrence × F.Occurrence)) : finishFrom v (s ++ t) = finishFrom (finishFrom v s) t

@[simp]

theorem Cslib.Logic.PL.CSP.Walk.finish_snoc {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (w : F.Walk) (o p : F.Occurrence) : (w.snoc o p).finish = p.var

theorem Cslib.Logic.PL.CSP.Walk.flipSteps_eq_flipOn {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (f : F.OccurrenceLabeling Bool) (s : List (F.Occurrence × F.Occurrence)) (hs : (edgesOf s).Nodup) : flipSteps f s = BitString.flipOn (edgesOf s).toFinset f

Stepwise and setwise flips agree for incidence trails.

theorem Cslib.Logic.PL.CSP.Walk.PrefixValid.final {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) : ValidLabeling sem (flipSteps f s)

Prefix validity includes validity after the final step.

theorem Cslib.Logic.PL.CSP.Walk.IsFPrefix.valid_flip {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) : ValidLabeling sem (w.flip f)

In particular, the set flip of an f-walk is valid.

theorem Cslib.Logic.PL.CSP.Walk.flipSteps_append {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (f : F.OccurrenceLabeling Bool) (s t : List (F.Occurrence × F.Occurrence)) : flipSteps f (s ++ t) = flipSteps (flipSteps f s) t

Flipping concatenated step lists is sequential composition.

theorem Cslib.Logic.PL.CSP.Walk.nodup_edges_snoc {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (w : F.Walk) (o p : F.Occurrence) (hw : w.edges.Nodup) (ho : o ∉ w.edges) (hp : p ∉ w.edges) (hop : o ≠ p) : (w.snoc o p).edges.Nodup

Appending a step with two distinct fresh incidences preserves incidence uniqueness.

theorem Cslib.Logic.PL.CSP.Walk.flip_snoc {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (w : F.Walk) (f : F.OccurrenceLabeling Bool) (o p : F.Occurrence) (hw : w.IsWalk) (ho : o ∉ w.edges) (hp : p ∉ w.edges) (hop : o ≠ p) : (w.snoc o p).flip f = BitString.flipOn {o, p} (w.flip f)

Appending one fresh step flips precisely its two incidences.

theorem Cslib.Logic.PL.CSP.Walk.Linked.snoc {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} {v : V} {s : List (F.Occurrence × F.Occurrence)} (hl : Linked v s) {o p : F.Occurrence} (ho : o.var = finishFrom v s) (hc : o.fst = p.fst) : Linked v (s ++ [(o, p)])

Incidence adjacency is preserved by a step from the previous endpoint.

theorem Cslib.Logic.PL.CSP.Walk.PrefixValid.snoc {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)} (hv : PrefixValid sem f s) (o p : F.Occurrence) (hn : ValidLabeling sem (BitString.flipOn {o, p} (flipSteps f s))) : PrefixValid sem f (s ++ [(o, p)])

All prefixes remain valid after a valid final step is appended.

theorem Cslib.Logic.PL.CSP.Walk.InternallyConsistent.snoc {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} {f : F.OccurrenceLabeling Bool} {s : List (F.Occurrence × F.Occurrence)} (hi : InternallyConsistent f s) (v : V) (o p : F.Occurrence) (hend : s = [] ∨ ¬Inconsistent f (finishFrom v s)) : InternallyConsistent f (s ++ [(o, p)])

The old endpoint becomes an internal variable when appending a step.

theorem Cslib.Logic.PL.CSP.Walk.IsFPrefix.snoc {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} {sem : Rel → List Bool → Bool} {f : F.OccurrenceLabeling Bool} {w : F.Walk} (hw : IsFPrefix sem f w) {o p : F.Occurrence} (ho : o.var = w.finish) (hc : o.fst = p.fst) (hne : o ≠ p) (hno : o ∉ w.edges) (hnp : p ∉ w.edges) (hi : w.steps = [] ∨ ¬Inconsistent f w.finish) (hv : ValidLabeling sem (BitString.flipOn {o, p} (w.flip f))) : IsFPrefix sem f (w.snoc o p)

Append a fresh locally valid step to a prefix-valid trail.

theorem Cslib.Logic.PL.CSP.Walk.IsWalk.defects_flip {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (h : F.EdgeInstance) {w : F.Walk} (hw : w.IsWalk) (f : F.OccurrenceLabeling Bool) : defects (w.flip f) = symmDiff (symmDiff (defects f) {w.start}) {w.finish}

The set of defects after a trail flip differs only at its variable endpoints. This includes closed trails, whose endpoint toggles cancel.

theorem Cslib.Logic.PL.CSP.Walk.IsAugmenting.card_defects_flip_add_two {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (h : F.EdgeInstance) {sem : Rel → List Bool → Bool} {f : F.OccurrenceLabeling Bool} {w : F.Walk} (hw : IsAugmenting sem f w) : (defects (w.flip f)).card + 2 = (defects f).card

Augmentation removes exactly two distinct variable defects.

theorem Cslib.Logic.PL.CSP.Walk.prefixValid_iff_forall_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)} : PrefixValid sem f s ↔ ∀ n ≤ s.length, ValidLabeling sem (flipSteps f (List.take n s))

The recursive prefix condition is exactly validity after every variable-ended prefix, including the initial labeling.

theorem Cslib.Logic.PL.CSP.Walk.linked_append_iff {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (v : V) (s t : List (F.Occurrence × F.Occurrence)) : Linked v (s ++ t) ↔ Linked v s ∧ Linked (finishFrom v s) t

Splitting a trail at a variable preserves the positional adjacency conditions.

theorem Cslib.Logic.PL.CSP.Walk.IsWalk.partner_transition {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (h : F.EdgeInstance) {w : F.Walk} (hw : w.IsWalk) {s t : List (F.Occurrence × F.Occurrence)} {a b o p : F.Occurrence} (he : w.steps = s ++ (a, b) :: (o, p) :: t) : o = h.partner b

Consecutive constraint steps cross a variable by its actual partner incidence. No incidence may be traversed in both directions or reused at a later visit.

theorem Cslib.Logic.PL.CSP.Walk.IsWalk.take {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} {w : F.Walk} (hw : w.IsWalk) (n : ℕ) : (w.take n).IsWalk

Every variable-ended prefix of an incidence trail is itself an incidence trail.

theorem Cslib.Logic.PL.CSP.Walk.IsFPrefix.valid_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} (hw : IsFPrefix sem f w) (n : ℕ) (hn : n ≤ w.steps.length) : ValidLabeling sem ((w.take n).flip f)

Every variable-ended prefix flip of an f-prefix is valid, in the set-flip formulation of Definition 23. This includes prefixes shorter than a returned augmenting walk.