Ordered argument occurrences of CSP instances

An occurrence is a constraint position together with a position in its scope. Neither repeated constraints nor repeated variables are identified. Local labelings read scopes in argument order; consistency requires equal labels at all occurrences of a variable. A consistent local labeling reconstructs a global assignment, using an explicitly supplied value for nonoccurring variables. These definitions use the existing CSP and its arbitrary-domain semantics.

Main definitions

• Cslib.Logic.PL.CSP.Occurrence: dependent indices into the existing instance.
• Cslib.Logic.PL.CSP.occurrences: executable records in constraint-then-scope order.
• Cslib.Logic.PL.CSP.ValidLabeling, Cslib.Logic.PL.CSP.ConsistentLabeling: local validity and agreement on variables.
• Cslib.Logic.PL.CSP.EdgeInstance: every occurring variable has precisely two occurrences, in distinct constraint positions.

References

The Boolean specialization of EdgeInstance matches [KKR18], Section 2, Definition 3 (arXiv v6, p. 3). That source uses set scopes; the distinct-position and exactly-two requirements here explicitly enforce its no-repeat convention without normalizing input scopes. Local validity and agreement specialize Section 5.1, Definition 20. The occurrence enumeration and reconstruction proofs are original, and impose no planarity or arity bound.

@[reducible, inline]

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

A constraint position and an argument position in that constraint's ordered scope.

def Cslib.Logic.PL.CSP.Occurrence.relation {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (o : F.Occurrence) : Rel

Relation symbol at this occurrence's constraint position.

def Cslib.Logic.PL.CSP.Occurrence.scope {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (o : F.Occurrence) : List V

Ordered scope at this occurrence's constraint position.

def Cslib.Logic.PL.CSP.Occurrence.var {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (o : F.Occurrence) : V

Variable at this argument position, retaining repeated occurrences.

def Cslib.Logic.PL.CSP.Occurrence.record {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (o : F.Occurrence) : ℕ × ℕ × V

Executable record: constraint index, scope index, variable.

theorem Cslib.Logic.PL.CSP.Occurrence.record_injective {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} : Function.Injective record

The two position indices identify an occurrence independently of variable names.

theorem Cslib.Logic.PL.CSP.Occurrence.var_mem {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (o : F.Occurrence) : o.var ∈ F.vars

Every named variable is an occurring variable of the original CSP.

theorem Cslib.Logic.PL.CSP.exists_occurrence_iff {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (v : V) : (∃ (o : F.Occurrence), o.var = v) ↔ v ∈ F.vars

Every occurring variable has a constraint-position/scope-position witness.

def Cslib.Logic.PL.CSP.occurrences {Rel : Type u_1} {V : Type u_2} (F : CSP Rel V) : List (ℕ × ℕ × V)

Occurrence records in constraint order, then scope order. The positive-CNF adapter preserves all positions and lets us reuse the existing executable occurrence enumeration.

theorem Cslib.Logic.PL.CSP.mem_occurrences {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} {r : ℕ × ℕ × V} : r ∈ F.occurrences ↔ ∃ (o : F.Occurrence), o.record = r

The enumeration contains exactly the valid position/variable records.

theorem Cslib.Logic.PL.CSP.map_occurrences {Rel : Type u_1} {V : Type u_2} (F : CSP Rel V) : List.map (fun (o : ℕ × ℕ × V) => o.2.2) F.occurrences = F.vars

Forgetting positions gives the original occurrence list, including repetitions.

theorem Cslib.Logic.PL.CSP.occurrences_nodup {Rel : Type u_1} {V : Type u_2} (F : CSP Rel V) : F.occurrences.Nodup

Every position record occurs exactly once, even if its variable or constraint is repeated.

theorem Cslib.Logic.PL.CSP.length_occurrences {Rel : Type u_1} {V : Type u_2} (F : CSP Rel V) : F.occurrences.length = (List.map (fun (c : Constraint Rel V) => c.2.length) F).sum

The number of argument occurrences is the sum of the scope lengths.

@[reducible, inline]

abbrev Cslib.Logic.PL.CSP.OccurrenceLabeling {Rel : Type u_1} {V : Type u_2} (F : CSP Rel V) (D : Type u_4) : Type u_4

A local labeling assigns a domain value separately to each argument occurrence.

def Cslib.Logic.PL.CSP.localTuple {Rel : Type u_1} {V : Type u_2} {D : Type u_3} {F : CSP Rel V} (l : F.OccurrenceLabeling D) (i : Fin (List.length F)) : List D

The tuple at a constraint reads its argument labels in their original order.

def Cslib.Logic.PL.CSP.ValidLabeling {Rel : Type u_1} {V : Type u_2} {D : Type u_3} {F : CSP Rel V} (sem : Rel → List D → Bool) (l : F.OccurrenceLabeling D) : Prop

Every constraint accepts its own ordered tuple of occurrence labels.

def Cslib.Logic.PL.CSP.ConsistentLabeling {Rel : Type u_1} {V : Type u_2} {D : Type u_3} {F : CSP Rel V} (l : F.OccurrenceLabeling D) : Prop

All occurrences of the same variable have the same label.

def Cslib.Logic.PL.CSP.labelAssignment {Rel : Type u_1} {V : Type u_2} {D : Type u_3} {F : CSP Rel V} (σ : V → D) : F.OccurrenceLabeling D

Restrict a global assignment to the ordered argument occurrences.

theorem Cslib.Logic.PL.CSP.consistentLabeling_labelAssignment {Rel : Type u_1} {V : Type u_2} {D : Type u_3} {F : CSP Rel V} (σ : V → D) : ConsistentLabeling (labelAssignment σ)

Global assignments always induce consistent labels.

@[simp]

theorem Cslib.Logic.PL.CSP.localTuple_labelAssignment {Rel : Type u_1} {V : Type u_2} {D : Type u_3} {F : CSP Rel V} (σ : V → D) (i : Fin (List.length F)) : localTuple (labelAssignment σ) i = List.map σ F[i].2

Restricting an assignment preserves each constraint's ordered tuple.

theorem Cslib.Logic.PL.CSP.validLabeling_labelAssignment_iff {Rel : Type u_1} {V : Type u_2} {D : Type u_3} {F : CSP Rel V} (sem : Rel → List D → Bool) (σ : V → D) : ValidLabeling sem (labelAssignment σ) ↔ eval sem σ F = true

Local validity of assignment labels is exactly the existing CSP evaluation.

noncomputable def Cslib.Logic.PL.CSP.reconstruct {Rel : Type u_1} {V : Type u_2} {D : Type u_3} {F : CSP Rel V} (l : F.OccurrenceLabeling D) (outside : D) : V → D

Recover an assignment by choosing one occurrence of each occurring variable; outside is the value on every variable absent from the instance.

theorem Cslib.Logic.PL.CSP.reconstruct_of_not_mem {Rel : Type u_1} {V : Type u_2} {D : Type u_3} {F : CSP Rel V} (l : F.OccurrenceLabeling D) (outside : D) {v : V} (hv : v ∉ F.vars) : reconstruct l outside v = outside

The reconstructed assignment has precisely the supplied value off the occurring variables.

theorem Cslib.Logic.PL.CSP.reconstruct_variable {Rel : Type u_1} {V : Type u_2} {D : Type u_3} {F : CSP Rel V} {l : F.OccurrenceLabeling D} (h : ConsistentLabeling l) (outside : D) (o : F.Occurrence) : reconstruct l outside o.var = l o

Consistency makes reconstruction independent of the chosen representative occurrence.

theorem Cslib.Logic.PL.CSP.eval_reconstruct {Rel : Type u_1} {V : Type u_2} {D : Type u_3} {F : CSP Rel V} {sem : Rel → List D → Bool} {l : F.OccurrenceLabeling D} (hl : ValidLabeling sem l) (hc : ConsistentLabeling l) (outside : D) : eval sem (reconstruct l outside) F = true

A consistent valid local labeling reconstructs a model of the original CSP.

theorem Cslib.Logic.PL.CSP.consistentLabeling_iff_exists_assignment {Rel : Type u_1} {V : Type u_2} {D : Type u_3} {F : CSP Rel V} (l : F.OccurrenceLabeling D) (outside : D) : ConsistentLabeling l ↔ ∃ (σ : V → D), labelAssignment σ = l

Consistent occurrence labels are exactly restrictions of global assignments.

theorem Cslib.Logic.PL.CSP.satisfiable_iff_exists_labeling {Rel : Type u_1} {V : Type u_2} {D : Type u_3} {F : CSP Rel V} (sem : Rel → List D → Bool) (outside : D) : Satisfiable sem F ↔ ∃ (l : F.OccurrenceLabeling D), ValidLabeling sem l ∧ ConsistentLabeling l

Satisfiability is equivalent to existence of a valid, consistent occurrence labeling.

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

Every occurring variable appears exactly twice, at distinct constraint positions. This also excludes repetitions within one scope, without changing the instance.

noncomputable def Cslib.Logic.PL.CSP.EdgeInstance.partner {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (h : F.EdgeInstance) (o : F.Occurrence) : F.Occurrence

The other occurrence of an edge variable.

theorem Cslib.Logic.PL.CSP.EdgeInstance.partner_constraint_ne {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (h : F.EdgeInstance) (o : F.Occurrence) : o.fst ≠ (h.partner o).fst

An edge's two occurrences belong to different constraint positions.

theorem Cslib.Logic.PL.CSP.EdgeInstance.partner_variable {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (h : F.EdgeInstance) (o : F.Occurrence) : o.var = (h.partner o).var

Both ends of an edge name the same variable.

theorem Cslib.Logic.PL.CSP.EdgeInstance.partner_ne {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (h : F.EdgeInstance) (o : F.Occurrence) : o ≠ h.partner o

The partner is a genuinely different argument occurrence.

theorem Cslib.Logic.PL.CSP.EdgeInstance.eq_or_eq_partner {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (h : F.EdgeInstance) {o p : F.Occurrence} (hp : p.var = o.var) : p = o ∨ p = h.partner o

A variable has no occurrences beyond these two ends.

theorem Cslib.Logic.PL.CSP.EdgeInstance.eq_of_constraint_eq {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (h : F.EdgeInstance) {o p : F.Occurrence} (hv : o.var = p.var) (hi : o.fst = p.fst) : o = p

Each of the two constraint scopes contains the variable only once.

@[simp]

theorem Cslib.Logic.PL.CSP.EdgeInstance.partner_partner {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (h : F.EdgeInstance) (o : F.Occurrence) : h.partner (h.partner o) = o

Taking the other end twice returns the original argument occurrence.

def Cslib.Logic.PL.CSP.EdgeInstance.Agrees {Rel : Type u_1} {V : Type u_2} {D : Type u_3} {F : CSP Rel V} (h : F.EdgeInstance) (l : F.OccurrenceLabeling D) : Prop

The two endpoint labels agree on each edge variable.

theorem Cslib.Logic.PL.CSP.EdgeInstance.agrees_iff_consistent {Rel : Type u_1} {V : Type u_2} {D : Type u_3} {F : CSP Rel V} (h : F.EdgeInstance) (l : F.OccurrenceLabeling D) : h.Agrees l ↔ ConsistentLabeling l

For edge instances, agreement of the two endpoint labels is exactly global consistency.

theorem Cslib.Logic.PL.CSP.EdgeInstance.satisfiable_iff_exists_agrees {Rel : Type u_1} {V : Type u_2} {D : Type u_3} {F : CSP Rel V} (h : F.EdgeInstance) (sem : Rel → List D → Bool) (outside : D) : Satisfiable sem F ↔ ∃ (l : F.OccurrenceLabeling D), ValidLabeling sem l ∧ h.Agrees l

A model exists iff there is a valid local labeling with agreeing endpoints on every edge. This includes the empty instance and retains nullary constraints.