Explicit Boolean relation tables

CSP.Table is a relation alphabet for the existing CSP, not a second instance format. Rows are lists, including duplicates; the arity and width guard distinguish the empty nullary relation from the nullary relation containing the empty row. Malformed tables reject all rows.

The local update Table.contract implements [KKR18], arXiv v6, Section 5.3, printed pp. 12–13: positions are the distinct internal variables in a constraint, reference is its current feasible local row, and the last output bit is the fresh connector. Outside coordinates retain their original order. Zero internal deviations give connector false, one gives true, and more than one discard the row. This module does not prove delta-matroid preservation, blossom validity, or the correctness of the edge solver. The elementary list implementation and its proofs are original formalization details.

Table.exactlyOne constructs the new connector relation from the length of a supplied scope. It stores one row per connector, rather than treating all possible active relations as a fixed finite alphabet. Its semantics agrees with Example 17 and the new constraint in Section 5.3 of the cited paper. In particular, its zero-connector relation is empty.

Main definitions

• Cslib.Logic.PL.CSP.Table: arity and explicit rows.
• Cslib.Logic.PL.CSP.Table.contract: guarded local contraction table update.
• Cslib.Logic.PL.CSP.Table.exactlyOne: explicit exactly-one connector table.

structure Cslib.Logic.PL.CSP.Table : Type

An explicit Boolean relation, with an arity even when its row list is empty. Duplicate rows are permitted. Use this as Rel in the existing CSP Rel V.

• arity : ℕ

  The number of coordinates.

• rows : List (List Bool)

  Accepted rows; the guard checks their widths.

@[instance_reducible]

instance Cslib.Logic.PL.CSP.instDecidableEqTable : DecidableEq Table

def Cslib.Logic.PL.CSP.instDecidableEqTable.decEq (x✝ x✝¹ : Table) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance Cslib.Logic.PL.CSP.instReprTable : Repr Table

def Cslib.Logic.PL.CSP.instReprTable.repr : Table → ℕ → Std.Format

def Cslib.Logic.PL.CSP.Table.wellFormed (table : Table) : Bool

Every stored row has the declared width. Empty tables are well formed at every arity.

def Cslib.Logic.PL.CSP.Table.sem (table : Table) (row : List Bool) : Bool

Membership semantics for the existing CSP evaluator. Malformed tables reject everything.

@[simp]

theorem Cslib.Logic.PL.CSP.Table.wellFormed_eq_true {table : Table} : table.wellFormed = true ↔ ∀ row ∈ table.rows, row.length = table.arity

The width guard characterizes well-formedness.

@[simp]

theorem Cslib.Logic.PL.CSP.Table.sem_eq_true {table : Table} {row : List Bool} : table.sem row = true ↔ table.wellFormed = true ∧ row ∈ table.rows

The executable semantics is precisely guarded row membership.

def Cslib.Logic.PL.CSP.Table.validPositions (width : ℕ) (positions : List ℕ) : Bool

Guard for distinct, in-range coordinate positions. Counting does not deduplicate the input.

theorem Cslib.Logic.PL.CSP.Table.validPositions_eq_true {width : ℕ} {positions : List ℕ} : validPositions width positions = true ↔ positions.Nodup ∧ ∀ i ∈ positions, i < width

The position guard requires both distinctness and range, including for an empty selection.

def Cslib.Logic.PL.CSP.Table.outsidePositions (width : ℕ) (positions : List ℕ) : List ℕ

Outside coordinates in increasing original order.

theorem Cslib.Logic.PL.CSP.Table.outsidePositions_sublist (width : ℕ) (positions : List ℕ) : (outsidePositions width positions).Sublist (List.range width)

Outside positions are a sublist of the original coordinate order.

theorem Cslib.Logic.PL.CSP.Table.length_outsidePositions_le (width : ℕ) (positions : List ℕ) : (outsidePositions width positions).length ≤ width

Selecting outside positions never increases width, even for malformed selections.

theorem Cslib.Logic.PL.CSP.Table.length_outsidePositions_add {width : ℕ} {positions : List ℕ} (h : validPositions width positions = true) : (outsidePositions width positions).length + positions.length = width

Distinct in-range positions and the outside positions partition the original width.

def Cslib.Logic.PL.CSP.Table.project (row : List Bool) (positions : List ℕ) : List Bool

Read coordinates, with a total fallback for malformed indices.

def Cslib.Logic.PL.CSP.Table.deviations (reference row : List Bool) (positions : List ℕ) : ℕ

Number of selected coordinates differing from the current local row. Positions must be distinct and in range when interpreted as internal variables.

def Cslib.Logic.PL.CSP.Table.canContract (table : Table) (reference : List Bool) (positions : List ℕ) : Bool

Preconditions for a local contraction: a feasible reference row and valid internal positions.

theorem Cslib.Logic.PL.CSP.Table.canContract_eq_true {table : Table} {reference : List Bool} {positions : List ℕ} : table.canContract reference positions = true ↔ table.wellFormed = true ∧ reference ∈ table.rows ∧ positions.Nodup ∧ ∀ i ∈ positions, i < table.arity

The contraction contract includes feasible-row membership, well-formedness and distinct in-range internal coordinates; no delta-matroid or blossom property is assumed here.

def Cslib.Logic.PL.CSP.Table.contract (table : Table) (reference : List Bool) (positions : List ℕ) : Table

Local contraction. Malformed data gives the empty nullary table. The implementation only ranges over the explicit reference row, never over an unchecked binary arity.

theorem Cslib.Logic.PL.CSP.Table.contract_of_not_canContract {table : Table} {reference : List Bool} {positions : List ℕ} (h : table.canContract reference positions = false) : table.contract reference positions = { arity := 0, rows := [] }

Invalid tables, references or position lists have a total rejecting output.

theorem Cslib.Logic.PL.CSP.Table.length_rows_contract_le (table : Table) (reference : List Bool) (positions : List ℕ) : (table.contract reference positions).rows.length ≤ table.rows.length

Contraction preserves row multiplicity and cannot increase the number of rows.

theorem Cslib.Logic.PL.CSP.Table.arity_contract {table : Table} {reference : List Bool} {positions : List ℕ} (h : table.canContract reference positions = true) : (table.contract reference positions).arity = (outsidePositions reference.length positions).length + 1

A guarded contraction has exactly the outside width plus one connector coordinate.

theorem Cslib.Logic.PL.CSP.Table.arity_contract_lt {table : Table} {reference : List Bool} {positions : List ℕ} (h : table.canContract reference positions = true) (htwo : 2 ≤ positions.length) : (table.contract reference positions).arity < table.arity

The actual blossom hypothesis of at least two internal coordinates strictly decreases local width. Feasibility alone is insufficient for this conclusion.

@[simp]

theorem Cslib.Logic.PL.CSP.Table.wellFormed_contract (table : Table) (reference : List Bool) (positions : List ℕ) : (table.contract reference positions).wellFormed = true

Every output row has the new declared width, including on malformed inputs.

theorem Cslib.Logic.PL.CSP.Table.sem_contract_eq_true {table : Table} {reference row : List Bool} {positions : List ℕ} (h : table.canContract reference positions = true) : (table.contract reference positions).sem row = true ↔ ∃ old ∈ table.rows, deviations reference old positions ≤ 1 ∧ project old (outsidePositions reference.length positions) ++ [decide (deviations reference old positions = 1)] = row

Exact contraction membership, with the output connector computed from zero or one internal changes. The original row is retained as a witness for later lifting.

theorem Cslib.Logic.PL.CSP.Table.sem_contract_cases {table : Table} {reference row : List Bool} {positions : List ℕ} (h : table.canContract reference positions = true) : (table.contract reference positions).sem row = true ↔ ∃ old ∈ table.rows, deviations reference old positions = 0 ∧ project old (outsidePositions reference.length positions) ++ [false] = row ∨ deviations reference old positions = 1 ∧ project old (outsidePositions reference.length positions) ++ [true] = row

The paper's two cases, stated without a numeric-to-Boolean connector conversion.

@[simp]

theorem Cslib.Logic.PL.CSP.Table.deviations_self (reference : List Bool) (positions : List ℕ) : deviations reference reference positions = 0

The feasible reference has no internal deviations.

theorem Cslib.Logic.PL.CSP.Table.sem_contract_reference {table : Table} {reference : List Bool} {positions : List ℕ} (h : table.canContract reference positions = true) : (table.contract reference positions).sem (project reference (outsidePositions reference.length positions) ++ [false]) = true

A guarded contraction retains the current feasible row, with its connector set to zero.

def Cslib.Logic.PL.CSP.Table.exactlyOne {V : Type u_1} (scope : List V) : Table

Explicit exactly-one table. The scope's length supplies the output-size resource; its entries need not be distinct, since this constructs only a relation, not a CSP scope guard.

@[simp]

theorem Cslib.Logic.PL.CSP.Table.length_rows_exactlyOne {V : Type u_1} (scope : List V) : (exactlyOne scope).rows.length = scope.length

Exactly-one stores one row per connector.

@[simp]

theorem Cslib.Logic.PL.CSP.Table.wellFormed_exactlyOne {V : Type u_1} (scope : List V) : (exactlyOne scope).wellFormed = true

Exactly-one tables have the declared width.

theorem Cslib.Logic.PL.CSP.Table.sem_exactlyOne_eq_true {V : Type u_1} (scope : List V) (row : List Bool) : (exactlyOne scope).sem row = true ↔ row.length = scope.length ∧ List.count true row = 1

Exactly-one semantics, independently of row ordering and the names in the supplied scope.

theorem Cslib.Logic.PL.CSP.Table.rows_exactlyOne_ne_nil {V : Type u_1} (scope : List V) : (exactlyOne scope).rows ≠ [] ↔ 0 < scope.length

The connector relation is nonempty precisely when there is a connector.

theorem Cslib.Logic.PL.CSP.Table.exists_sem_exactlyOne {V : Type u_1} (scope : List V) : (∃ (row : List Bool), (exactlyOne scope).sem row = true) ↔ 0 < scope.length

Exactly-one admits a satisfying row precisely when the scope supplies a connector.