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

theorem DescriptiveComplexity.SatOcc.satClauses_occ {A : Type} [FirstOrder.Language.sat.Structure A] {ν : A → Prop} (hν : ∀ (c : A), FirstOrder.Language.Structure.RelMap FirstOrder.Language.satIsClause ![c] → ∃ (x : A), FirstOrder.Language.Structure.RelMap FirstOrder.Language.satPosIn ![c, x] ∧ ν x ∨ FirstOrder.Language.Structure.RelMap FirstOrder.Language.satNegIn ![c, x] ∧ ¬ν x) (c : A) : IsCl c → ∃ (x : A) (s : Bool), OccIn c x s ∧ LitTrue ν x s

Bridge from the Satisfiable form of clause satisfaction to the occurrence form.

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

theorem DescriptiveComplexity.SatOcc.eq_of_minOcc_of_maxOcc {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {c x z : A} {s u : Bool} (hmin : MinOcc c x s) (hmax : MaxOcc c x s) (hz : OccIn c z u) : z = x ∧ u = s

If (x, s) is both the first and last occurrence of c, it is the only one.

theorem DescriptiveComplexity.SatOcc.succOcc_occLt_iff {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {c y x z : A} {t s u : Bool} (hsucc : SuccOcc c y t x s) (hz : OccIn c z u) : occLt z u x s ↔ occLt z u y t ∨ z = y ∧ u = t

Occurrences up to the immediate predecessor (y, t) of (x, s) are exactly the occurrences strictly before (x, s).

theorem DescriptiveComplexity.SatOcc.succOcc_right_unique {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {c y x₁ x₂ : A} {t s₁ s₂ : Bool} (h₁ : SuccOcc c y t x₁ s₁) (h₂ : SuccOcc c y t x₂ s₂) : x₁ = x₂ ∧ s₁ = s₂

The successor of a given occurrence is unique.

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.not_prefixOrStrict_min {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {ν : A → Prop} {c y : A} {t : Bool} (hmin : MinOcc c y t) : ¬PrefixOrStrict ν c y t

theorem DescriptiveComplexity.SatOcc.prefixOr_iff {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {ν : A → Prop} {c x : A} {s : Bool} (hx : OccIn c x s) : PrefixOr ν c x s ↔ PrefixOrStrict ν c x s ∨ LitTrue ν x s

theorem DescriptiveComplexity.SatOcc.prefixOrStrict_succ {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {ν : A → Prop} {c y x : A} {t s : Bool} (hsucc : SuccOcc c y t x s) : PrefixOrStrict ν c x s ↔ PrefixOr ν c y t

theorem DescriptiveComplexity.SatOcc.prefixOrStrict_of_min_succ {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {ν : A → Prop} {c y x : A} {t s : Bool} (hmin : MinOcc c y t) (hsucc : SuccOcc c y t x s) : PrefixOrStrict ν c x s ↔ LitTrue ν y t

theorem DescriptiveComplexity.SatOcc.prefixOr_of_max {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {ν : A → Prop} {c x y : A} {s t : Bool} (hmax : MaxOcc c x s) (hy : OccIn c y t) (hT : LitTrue ν y t) : PrefixOr ν c x s

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

A clause with an occurrence has a first occurrence.

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

A clause with an occurrence has a last occurrence.

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.

theorem DescriptiveComplexity.SatOcc.exists_succOcc_right {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] {c x : A} {s : Bool} (hx : OccIn c x s) (hne : ∃ (y : A) (t : Bool), OccIn c y t ∧ occLt x s y t) : ∃ (y : A) (t : Bool), SuccOcc c x s y t

An occurrence with a later occurrence has an immediate successor.