Documentation

DescriptiveComplexity.Problems.Machine.QsatGeom

The geometry of the QBF machine's tape #

Where the cells sit: which tagged tuples are positions, which is the lowest and which the highest, and what the immediate neighbor of each one is. Everything the run needs to know about movement, proved once, before any transition is taken.

The content is that the tape

  ⊢   v₁ v₂ … vₙ   ⊣

is exactly the position order DescriptiveComplexity.QsatTM.QLe: the left marker is DescriptiveComplexity.MinPos, the right marker is DescriptiveComplexity.MaxPos, and DescriptiveComplexity.SuccPos steps from the left marker to the outermost variable, from a variable to the next one the prefix binds, and from the innermost variable to the right marker. The degenerate instance – no quantified variable at all – is the case where the two markers are neighbors.

All of it needs the instance to be well formed, since that is exactly when the prefix order is a linear order on the variables and QLe is a linear order at all (DescriptiveComplexity.QsatTM.isLinOrd_qLe).

The three position tags, compared #

Walking the quantifier prefix #

def DescriptiveComplexity.QsatTM.QMinVar {A : Type} [FirstOrder.Language.qsat.Structure A] (x : A) :

x is the variable the prefix binds first.

Equations

DescriptiveComplexity.QsatTM.QMinVar x = (DescriptiveComplexity.IsQVar x ∧ ∀ (y : A), DescriptiveComplexity.IsQVar y → ¬DescriptiveComplexity.QPrec y x)

Instances For

Dependency graph

def DescriptiveComplexity.QsatTM.QMaxVar {A : Type} [FirstOrder.Language.qsat.Structure A] (x : A) :

x is the variable the prefix binds last.

Equations

DescriptiveComplexity.QsatTM.QMaxVar x = (DescriptiveComplexity.IsQVar x ∧ ∀ (y : A), DescriptiveComplexity.IsQVar y → ¬DescriptiveComplexity.QPrec x y)

Instances For

Dependency graph

def DescriptiveComplexity.QsatTM.QNextVar {A : Type} [FirstOrder.Language.qsat.Structure A] (x y : A) :

y is the variable the prefix binds immediately after x.

Equations

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

Instances For

Dependency graph

The positions #

theorem DescriptiveComplexity.QsatTM.eq_qBot_tup {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {w : Fin 2 → A} (h : IsMinTup w) :

w = fun (x : Fin 2) => qBot

A tuple pinned at both coordinates is the tuple of least elements.

Dependency graph

theorem DescriptiveComplexity.QsatTM.qPosn_posStart {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] :

Dependency graph

theorem DescriptiveComplexity.QsatTM.qPosn_posEnd {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] :

Dependency graph

theorem DescriptiveComplexity.QsatTM.qPosn_posCell {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {x : A} (hx : IsQVar x) :

QPosn (posCell x)

Dependency graph

theorem DescriptiveComplexity.QsatTM.qPosn_iff {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (p : QV A) :

QPosn p ↔ p = posStart ∨ (∃ (x : A), IsQVar x ∧ p = posCell x) ∨ p = posEnd

The positions of the tape, listed: the two markers and one cell per quantified variable.

Dependency graph

Comparing positions #

theorem DescriptiveComplexity.QsatTM.qLe_posCell_iff {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (hwf : QsatWf A) {x y : A} :

QLe (posCell x) (posCell y) ↔ PLe x y

Between two cells the tape order is the prefix order.

Dependency graph

theorem DescriptiveComplexity.QsatTM.qLe_of_tagIdx_lt {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] {p q : QV A} (h : qTagIdx p.1 < qTagIdx q.1) :

QLe p q

A tag strictly lower in the index order is lower on the tape.

Dependency graph

theorem DescriptiveComplexity.QsatTM.qLe_refl {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] (hwf : QsatWf A) (p : QV A) :

QLe p p

The tape order is reflexive on a well-formed instance.

Dependency graph

theorem DescriptiveComplexity.QsatTM.qLe_start_cell {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (x : A) :

QLe posStart (posCell x)

Dependency graph

theorem DescriptiveComplexity.QsatTM.qLe_start_end {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] :

QLe posStart posEnd

Dependency graph

theorem DescriptiveComplexity.QsatTM.qLe_cell_end {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (x : A) :

QLe (posCell x) posEnd

Dependency graph

theorem DescriptiveComplexity.QsatTM.not_qLe_cell_start {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (x : A) :

¬QLe (posCell x) posStart

Dependency graph

theorem DescriptiveComplexity.QsatTM.not_qLe_end_cell {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (x : A) :

¬QLe posEnd (posCell x)

Dependency graph

theorem DescriptiveComplexity.QsatTM.not_qLe_end_start {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] :

¬QLe posEnd posStart

Dependency graph

The ends of the tape #

theorem DescriptiveComplexity.QsatTM.minPos_posStart {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (hwf : QsatWf A) :

MinPos QLe QPosn posStart

The left marker is the lowest position.

Dependency graph

theorem DescriptiveComplexity.QsatTM.maxPos_posEnd {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (hwf : QsatWf A) :

MaxPos QLe QPosn posEnd

The right marker is the highest position.

Dependency graph

Neighbors #