Literal occurrences of a CNF structure, ordered

Semantic layer shared by the reductions from SAT (to 3-colorability, to 3SAT…): literal occurrences of a Language.sat-structure, their traversal along a linear order of the universe, and the truth of literals and of prefix disjunctions under an assignment.

An occurrence of a clause c is a pair (x, s) with x an element and s : Bool a sign, such that x occurs in c with sign s (OccIn). Occurrences are ordered lexicographically (variable first, then sign, false < true): occLt. On a finite universe every clause with at least one occurrence has a first (MinOcc) and last (MaxOcc) occurrence, and every occurrence that is not first has an immediate predecessor (SuccOcc, exists_succOcc), which is unique in both directions. These are the facts needed to thread a gadget chain (an OR-gadget chain for 3-colorability, a clause-splitting chain for 3SAT) along the occurrences of each clause.

For chain-correctness arguments, LitTrue states that a literal is true under an assignment, and PrefixOr/PrefixOrStrict state that some occurrence of a clause up to (resp. strictly before) a given position is true; the lemmas relating them to MinOcc/MaxOcc/SuccOcc implement the usual invariant of chain constructions.

Everything in this file is first-order definable over Language.sat.sum Language.order; the corresponding formulas and their realization lemmas are in DescriptiveComplexity.OccurrenceFormulas.

def DescriptiveComplexity.SatOcc.IsCl {A : Type} [FirstOrder.Language.sat.Structure A] (c : A) : Prop

c is a clause.

Equations

• DescriptiveComplexity.SatOcc.IsCl c = FirstOrder.Language.Structure.RelMap FirstOrder.Language.satIsClause ![c]

def DescriptiveComplexity.SatOcc.PosIn {A : Type} [FirstOrder.Language.sat.Structure A] (c x : A) : Prop

x occurs positively in c.

Equations

• DescriptiveComplexity.SatOcc.PosIn c x = FirstOrder.Language.Structure.RelMap FirstOrder.Language.satPosIn ![c, x]

def DescriptiveComplexity.SatOcc.NegIn {A : Type} [FirstOrder.Language.sat.Structure A] (c x : A) : Prop

x occurs negatively in c.

Equations

• DescriptiveComplexity.SatOcc.NegIn c x = FirstOrder.Language.Structure.RelMap FirstOrder.Language.satNegIn ![c, x]

def DescriptiveComplexity.SatOcc.OccIn {A : Type} [FirstOrder.Language.sat.Structure A] (c x : A) (s : Bool) : Prop

The literal (x, s) occurs in the clause c (s = true for a positive occurrence). Occurrences are restricted to actual clauses, so that stray posIn/negIn facts on non-clause elements do not create gadgets.

Equations

• DescriptiveComplexity.SatOcc.OccIn c x s = (DescriptiveComplexity.SatOcc.IsCl c ∧ if s = true then DescriptiveComplexity.SatOcc.PosIn c x else DescriptiveComplexity.SatOcc.NegIn c x)

@[simp]

theorem DescriptiveComplexity.SatOcc.occIn_true {A : Type} [FirstOrder.Language.sat.Structure A] {c x : A} : OccIn c x true ↔ IsCl c ∧ PosIn c x

@[simp]

theorem DescriptiveComplexity.SatOcc.occIn_false {A : Type} [FirstOrder.Language.sat.Structure A] {c x : A} : OccIn c x false ↔ IsCl c ∧ NegIn c x

theorem DescriptiveComplexity.SatOcc.OccIn.isCl {A : Type} [FirstOrder.Language.sat.Structure A] {c x : A} {s : Bool} (h : OccIn c x s) : IsCl c

def DescriptiveComplexity.SatOcc.EmptyCl {A : Type} [FirstOrder.Language.sat.Structure A] (c : A) : Prop

c is a clause with no literal: an unsatisfiable clause.

Equations

• DescriptiveComplexity.SatOcc.EmptyCl c = (DescriptiveComplexity.SatOcc.IsCl c ∧ ∀ (x : A) (s : Bool), ¬DescriptiveComplexity.SatOcc.OccIn c x s)

def DescriptiveComplexity.SatOcc.LitTrue {A : Type} (ν : A → Prop) (x : A) (s : Bool) : Prop

The literal (x, s) is true under the assignment ν.

Equations

• DescriptiveComplexity.SatOcc.LitTrue ν x s = if s = true then ν x else ¬ν x

theorem DescriptiveComplexity.SatOcc.litTrue_not {A : Type} {ν : A → Prop} {x : A} {s : Bool} : LitTrue ν x !s ↔ ¬LitTrue ν x s

def DescriptiveComplexity.SatOcc.occLt {A : Type} [LinearOrder A] (x : A) (s : Bool) (y : A) (t : Bool) : Prop

Strict lexicographic order on occurrence positions: variable first, then sign (with false < true).

Equations

• DescriptiveComplexity.SatOcc.occLt x s y t = (x < y ∨ x = y ∧ s < t)

theorem DescriptiveComplexity.SatOcc.occLt_irrefl {A : Type} [LinearOrder A] (x : A) (s : Bool) : ¬occLt x s x s

theorem DescriptiveComplexity.SatOcc.occLt_trans {A : Type} [LinearOrder A] {x y z : A} {s t u : Bool} (h₁ : occLt x s y t) (h₂ : occLt y t z u) : occLt x s z u

theorem DescriptiveComplexity.SatOcc.occLt_asymm {A : Type} [LinearOrder A] {x y : A} {s t : Bool} (h : occLt x s y t) : ¬occLt y t x s

theorem DescriptiveComplexity.SatOcc.occLt_trichotomy {A : Type} [LinearOrder A] (x : A) (s : Bool) (y : A) (t : Bool) : occLt x s y t ∨ x = y ∧ s = t ∨ occLt y t x s

def DescriptiveComplexity.SatOcc.MinOcc {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (c x : A) (s : Bool) : Prop

(x, s) is the first occurrence of the clause c.

Equations

• One or more equations did not get rendered due to their size.

def DescriptiveComplexity.SatOcc.MaxOcc {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (c x : A) (s : Bool) : Prop

(x, s) is the last occurrence of the clause c.

Equations

• One or more equations did not get rendered due to their size.

def DescriptiveComplexity.SatOcc.SuccOcc {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (c y : A) (t : Bool) (x : A) (s : Bool) : Prop

(x, s) is an occurrence of c immediately preceded by the occurrence (y, t).

Equations

• One or more equations did not get rendered due to their size.

def DescriptiveComplexity.SatOcc.Chained {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (c x : A) (s : Bool) : Prop

(x, s) is an occurrence of c that is not the first one: an OR-gate of the chain of c sits on it.

Equations

• DescriptiveComplexity.SatOcc.Chained c x s = (DescriptiveComplexity.SatOcc.OccIn c x s ∧ ¬DescriptiveComplexity.SatOcc.MinOcc c x s)

theorem DescriptiveComplexity.SatOcc.MinOcc.occIn {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {c x : A} {s : Bool} (h : MinOcc c x s) : OccIn c x s

theorem DescriptiveComplexity.SatOcc.MaxOcc.occIn {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {c x : A} {s : Bool} (h : MaxOcc c x s) : OccIn c x s

theorem DescriptiveComplexity.SatOcc.Chained.occIn {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {c x : A} {s : Bool} (h : Chained c x s) : OccIn c x s

Truth of prefix disjunctions

def DescriptiveComplexity.SatOcc.PrefixOrStrict {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (ν : A → Prop) (c x : A) (s : Bool) : Prop

Some occurrence of c strictly before (x, s) is true under ν.

Equations

• One or more equations did not get rendered due to their size.

def DescriptiveComplexity.SatOcc.PrefixOr {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (ν : A → Prop) (c x : A) (s : Bool) : Prop

Some occurrence of c up to (x, s) (inclusive) is true under ν.

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.SatOcc.exists_succOcc {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] {c x : A} {s : Bool} (h : Chained c x s) : ∃ (y : A) (t : Bool), SuccOcc c y t x s

A non-first occurrence has an immediate predecessor.