The occurrences of a variable, cyclically ordered

DescriptiveComplexity.OccurrenceOrder walks the occurrences of a clause; this file walks those of a variable – the same signed positions (c, s), read along the other index – and closes the walk into a cycle (DescriptiveComplexity.SatOcc.VarNext): the last occurrence of a variable is followed by its first one.

That cycle is what a truth-setting gadget needs. A gadget laid along a path of occurrences is forced into a single configuration, and forces the variable to one truth value; laid along a cycle it admits exactly two, which is what makes it an assignment. It is used by the reduction to 3-dimensional matching (DescriptiveComplexity.Problems.ThreeDimMatching.Hardness).

Everything here has a first-order counterpart, over the ordered expansion DescriptiveComplexity.SatOcc.satOrd, since the successor is “the next occurrence, or the first one if there is no next”, and both halves are first-order.

The cyclic order on the occurrences of a variable

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

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

Equations

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

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

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

Equations

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

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

(c', t) is the occurrence of x immediately after (c, s).

Equations

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

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

(c', t) follows (c, s) cyclically among the occurrences of x: the next one, or the first one when (c, s) is the last.

Equations

• DescriptiveComplexity.SatOcc.VarNext x c s c' t = (DescriptiveComplexity.SatOcc.VarStep x c s c' t ∨ DescriptiveComplexity.SatOcc.VarMax x c s ∧ DescriptiveComplexity.SatOcc.VarMin x c' t)

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

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

theorem DescriptiveComplexity.SatOcc.varMin_unique {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {x c c' : A} {s t : Bool} (h : VarMin x c s) (h' : VarMin x c' t) : c = c' ∧ s = t

The first occurrence of a variable is unique.

theorem DescriptiveComplexity.SatOcc.varMax_unique {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {x c c' : A} {s t : Bool} (h : VarMax x c s) (h' : VarMax x c' t) : c = c' ∧ s = t

The last occurrence of a variable is unique.

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

The immediate successor is unique.

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

The immediate predecessor is unique.

theorem DescriptiveComplexity.SatOcc.exists_minOccP {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] {x : A} {P : A → Bool → Prop} (h : ∃ (c : A) (s : Bool), OccIn c x s ∧ P c s) : ∃ (c : A) (s : Bool), OccIn c x s ∧ P c s ∧ ∀ (c' : A) (t : Bool), OccIn c' x t → P c' t → ¬occLt c' t c s

A nonempty set of occurrences of a variable has an occLt-least element.

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

A variable with an occurrence has a first one.

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

A variable with an occurrence has a last one.

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

An occurrence with a later one has an immediate successor.

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

An occurrence with an earlier one has an immediate predecessor.

theorem DescriptiveComplexity.SatOcc.exists_varNext {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] {x c : A} {s : Bool} (hx : OccIn c x s) : ∃ (c' : A) (t : Bool), VarNext x c s c' t

Every occurrence has a cyclic successor: the next one, or the first one when it is the last.

theorem DescriptiveComplexity.SatOcc.exists_varPrev {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] {x c' : A} {t : Bool} (hx : OccIn c' x t) : ∃ (c : A) (s : Bool), VarNext x c s c' t

Every occurrence has a cyclic predecessor.

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

The cyclic successor is unique.

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

The cyclic predecessor is unique.

The first-order counterparts

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

Some occurrence of x lies strictly between (c, s) and (c', t), as a formula.

Equations

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

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

(c', t) is the occurrence of x immediately after (c, s), as a formula.

Equations

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

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

(c', t) follows (c, s) cyclically among the occurrences of x, as a formula.

Equations

• DescriptiveComplexity.SatOcc.varNextF s t x c c' = DescriptiveComplexity.SatOcc.varStepF s t x c c' ⊔ DescriptiveComplexity.SatOcc.varMaxF s x c ⊓ DescriptiveComplexity.SatOcc.varMinF t x c'

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem DescriptiveComplexity.SatOcc.realize_varStepF {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {α : Type} {v : α → A} {s t : Bool} {x c c' : α} : (varStepF s t x c c').Realize v ↔ VarStep (v x) (v c) s (v c') t

@[simp]

theorem DescriptiveComplexity.SatOcc.realize_varNextF {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {α : Type} {v : α → A} {s t : Bool} {x c c' : α} : (varNextF s t x c c').Realize v ↔ VarNext (v x) (v c) s (v c') t