First-order formulas for literal occurrences, over the ordered expansion

First-order counterpart of DescriptiveComplexity.OccurrenceOrder, shared by the reductions from SAT (to 3-colorability, to 3SAT…): parameterized formula builders over the ordered expansion Language.sat.sum Language.order (DescriptiveComplexity.SatOcc.satOrd) mirroring the semantic predicates on literal occurrences – occF for OccIn, minOccF/maxOccF for MinOcc/MaxOcc, succOccF for SuccOcc, chainedF for Chained, emptyClF for EmptyCl, … – together with their realization lemmas (realize_occF…).

All builders are parameterized by the indices of their free variables, so that they can be instantiated at any variable type (in particular under quantifiers). Occurrence signs are static (Lean-level) Bool parameters: a quantification over signs becomes a finite conjunction or disjunction of formulas.

@[reducible, inline]

abbrev DescriptiveComplexity.SatOcc.satOrd : FirstOrder.Language

The ordered expansion of the language of CNF instances.

Equations

• DescriptiveComplexity.SatOcc.satOrd = FirstOrder.Language.sat.sum FirstOrder.Language.order

@[reducible, inline]

abbrev DescriptiveComplexity.SatOcc.clSym : satOrd.Relations 1

The symbol for “is a clause” in the ordered expansion.

Equations

• DescriptiveComplexity.SatOcc.clSym = Sum.inl FirstOrder.Language.satIsClause

@[reducible, inline]

abbrev DescriptiveComplexity.SatOcc.posSym : satOrd.Relations 2

The symbol for “occurs positively in” in the ordered expansion.

Equations

• DescriptiveComplexity.SatOcc.posSym = Sum.inl FirstOrder.Language.satPosIn

@[reducible, inline]

abbrev DescriptiveComplexity.SatOcc.negSym : satOrd.Relations 2

The symbol for “occurs negatively in” in the ordered expansion.

Equations

• DescriptiveComplexity.SatOcc.negSym = Sum.inl FirstOrder.Language.satNegIn

Formula builders

def DescriptiveComplexity.SatOcc.clF {α : Type} (c : α) : satOrd.Formula α

c is a clause, as a formula.

Equations

• DescriptiveComplexity.SatOcc.clF c = DescriptiveComplexity.SatOcc.clSym.formula₁ (FirstOrder.Language.var c)

def DescriptiveComplexity.SatOcc.posF {α : Type} (c x : α) : satOrd.Formula α

x occurs positively in c, as a formula.

Equations

• DescriptiveComplexity.SatOcc.posF c x = DescriptiveComplexity.SatOcc.posSym.formula₂ (FirstOrder.Language.var c) (FirstOrder.Language.var x)

def DescriptiveComplexity.SatOcc.negF {α : Type} (c x : α) : satOrd.Formula α

x occurs negatively in c, as a formula.

Equations

• DescriptiveComplexity.SatOcc.negF c x = DescriptiveComplexity.SatOcc.negSym.formula₂ (FirstOrder.Language.var c) (FirstOrder.Language.var x)

def DescriptiveComplexity.SatOcc.leF {α : Type} (x y : α) : satOrd.Formula α

x ≤ y, as a formula.

Equations

• DescriptiveComplexity.SatOcc.leF x y = FirstOrder.Language.leSymb.formula₂ (FirstOrder.Language.var x) (FirstOrder.Language.var y)

def DescriptiveComplexity.SatOcc.eqF {α : Type} (x y : α) : satOrd.Formula α

x = y, as a formula.

Equations

• DescriptiveComplexity.SatOcc.eqF x y = (FirstOrder.Language.var x).equal (FirstOrder.Language.var y)

def DescriptiveComplexity.SatOcc.ltF {α : Type} (x y : α) : satOrd.Formula α

x < y, as a formula.

Equations

• DescriptiveComplexity.SatOcc.ltF x y = DescriptiveComplexity.SatOcc.leF x y ⊓ FirstOrder.Language.BoundedFormula.not (DescriptiveComplexity.SatOcc.eqF x y)

def DescriptiveComplexity.SatOcc.occF {α : Type} (s : Bool) (c x : α) : satOrd.Formula α

The literal (x, s) occurs in the clause c, as a formula.

Equations

• DescriptiveComplexity.SatOcc.occF s c x = DescriptiveComplexity.SatOcc.clF c ⊓ if s = true then DescriptiveComplexity.SatOcc.posF c x else DescriptiveComplexity.SatOcc.negF c x

def DescriptiveComplexity.SatOcc.occLtF {α : Type} (s t : Bool) (x y : α) : satOrd.Formula α

The occurrence position (x, s) precedes (y, t), as a formula (the signs are fixed parameters, so this is just ≤ or < on the variables).

Equations

• DescriptiveComplexity.SatOcc.occLtF s t x y = if s < t then DescriptiveComplexity.SatOcc.leF x y else DescriptiveComplexity.SatOcc.ltF x y

noncomputable def DescriptiveComplexity.SatOcc.existsEarlierF {α : Type} (s : Bool) (c x : α) : satOrd.Formula α

Some occurrence of c lies strictly before (x, s), as a formula.

Equations

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

noncomputable def DescriptiveComplexity.SatOcc.existsLaterF {α : Type} (s : Bool) (c x : α) : satOrd.Formula α

Some occurrence of c lies strictly after (x, s), as a formula.

Equations

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

noncomputable def DescriptiveComplexity.SatOcc.minOccF {α : Type} (s : Bool) (c x : α) : satOrd.Formula α

(x, s) is the first occurrence of c, as a formula.

Equations

• DescriptiveComplexity.SatOcc.minOccF s c x = DescriptiveComplexity.SatOcc.occF s c x ⊓ FirstOrder.Language.BoundedFormula.not (DescriptiveComplexity.SatOcc.existsEarlierF s c x)

noncomputable def DescriptiveComplexity.SatOcc.maxOccF {α : Type} (s : Bool) (c x : α) : satOrd.Formula α

(x, s) is the last occurrence of c, as a formula.

Equations

• DescriptiveComplexity.SatOcc.maxOccF s c x = DescriptiveComplexity.SatOcc.occF s c x ⊓ FirstOrder.Language.BoundedFormula.not (DescriptiveComplexity.SatOcc.existsLaterF s c x)

noncomputable def DescriptiveComplexity.SatOcc.chainedF {α : Type} (s : Bool) (c x : α) : satOrd.Formula α

(x, s) is a non-first occurrence of c, as a formula.

Equations

• DescriptiveComplexity.SatOcc.chainedF s c x = DescriptiveComplexity.SatOcc.occF s c x ⊓ FirstOrder.Language.BoundedFormula.not (DescriptiveComplexity.SatOcc.minOccF s c x)

noncomputable def DescriptiveComplexity.SatOcc.succOccF {α : Type} (t s : Bool) (c y x : α) : satOrd.Formula α

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

Equations

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

noncomputable def DescriptiveComplexity.SatOcc.unitLitF {α : Type} (s : Bool) (x : α) : satOrd.Formula α

(x, s) is the unique literal of some clause, as a formula.

Equations

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

noncomputable def DescriptiveComplexity.SatOcc.emptyClF {α : Type} (c : α) : satOrd.Formula α

c is an empty clause, as a formula.

Equations

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

noncomputable def DescriptiveComplexity.SatOcc.exEmptyClF {α : Type} : satOrd.Formula α

Some clause is empty, as a (closed) formula: the standard spoiler condition of reductions from SAT, making the whole CNF unsatisfiable.

Equations

• DescriptiveComplexity.SatOcc.exEmptyClF = FirstOrder.Language.Formula.iExs Unit (DescriptiveComplexity.SatOcc.emptyClF (Sum.inr ()))

Realization lemmas

@[simp]

theorem DescriptiveComplexity.SatOcc.realize_clF {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {α : Type} {v : α → A} {c : α} : (clF c).Realize v ↔ IsCl (v c)

@[simp]

theorem DescriptiveComplexity.SatOcc.realize_posF {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {α : Type} {v : α → A} {c x : α} : (posF c x).Realize v ↔ PosIn (v c) (v x)

@[simp]

theorem DescriptiveComplexity.SatOcc.realize_negF {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {α : Type} {v : α → A} {c x : α} : (negF c x).Realize v ↔ NegIn (v c) (v x)

@[simp]

theorem DescriptiveComplexity.SatOcc.realize_leF {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {α : Type} {v : α → A} {x y : α} : (leF x y).Realize v ↔ v x ≤ v y

@[simp]

theorem DescriptiveComplexity.SatOcc.realize_eqF {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {α : Type} {v : α → A} {x y : α} : (eqF x y).Realize v ↔ v x = v y

@[simp]

theorem DescriptiveComplexity.SatOcc.realize_ltF {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {α : Type} {v : α → A} {x y : α} : (ltF x y).Realize v ↔ v x < v y

@[simp]

theorem DescriptiveComplexity.SatOcc.realize_occF {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {α : Type} {v : α → A} {s : Bool} {c x : α} : (occF s c x).Realize v ↔ OccIn (v c) (v x) s

@[simp]

theorem DescriptiveComplexity.SatOcc.realize_occLtF {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {α : Type} {v : α → A} {s t : Bool} {x y : α} : (occLtF s t x y).Realize v ↔ occLt (v x) s (v y) t

@[simp]

theorem DescriptiveComplexity.SatOcc.realize_existsEarlierF {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {α : Type} {v : α → A} {s : Bool} {c x : α} : (existsEarlierF s c x).Realize v ↔ ∃ (y : A) (t : Bool), OccIn (v c) y t ∧ occLt y t (v x) s

@[simp]

theorem DescriptiveComplexity.SatOcc.realize_existsLaterF {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {α : Type} {v : α → A} {s : Bool} {c x : α} : (existsLaterF s c x).Realize v ↔ ∃ (y : A) (t : Bool), OccIn (v c) y t ∧ occLt (v x) s y t

@[simp]

theorem DescriptiveComplexity.SatOcc.realize_minOccF {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {α : Type} {v : α → A} {s : Bool} {c x : α} : (minOccF s c x).Realize v ↔ MinOcc (v c) (v x) s

@[simp]

theorem DescriptiveComplexity.SatOcc.realize_maxOccF {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {α : Type} {v : α → A} {s : Bool} {c x : α} : (maxOccF s c x).Realize v ↔ MaxOcc (v c) (v x) s

@[simp]

theorem DescriptiveComplexity.SatOcc.realize_chainedF {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {α : Type} {v : α → A} {s : Bool} {c x : α} : (chainedF s c x).Realize v ↔ Chained (v c) (v x) s

@[simp]

theorem DescriptiveComplexity.SatOcc.realize_succOccF {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {α : Type} {v : α → A} {t s : Bool} {c y x : α} : (succOccF t s c y x).Realize v ↔ SuccOcc (v c) (v y) t (v x) s

@[simp]

theorem DescriptiveComplexity.SatOcc.realize_unitLitF {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {α : Type} {v : α → A} {s : Bool} {x : α} : (unitLitF s x).Realize v ↔ ∃ (c : A), MinOcc c (v x) s ∧ MaxOcc c (v x) s

@[simp]

theorem DescriptiveComplexity.SatOcc.realize_emptyClF {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {α : Type} {v : α → A} {c : α} : (emptyClF c).Realize v ↔ EmptyCl (v c)

@[simp]

theorem DescriptiveComplexity.SatOcc.realize_exEmptyClF {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {α : Type} {v : α → A} : exEmptyClF.Realize v ↔ ∃ (c : A), EmptyCl c