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 neighbour 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 neighbours.

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 #

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

x is the variable the prefix binds first.

Equations
Instances For
    Dependency graph
    source
    def DescriptiveComplexity.QsatTM.QMaxVar {A : Type} [FirstOrder.Language.qsat.Structure A] (x : A) :
    Prop

    x is the variable the prefix binds last.

    Equations
    Instances For
      Dependency graph
      source
      def DescriptiveComplexity.QsatTM.QNextVar {A : Type} [FirstOrder.Language.qsat.Structure A] (x y : A) :
      Prop

      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 #

        source
        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
        source
        theorem DescriptiveComplexity.QsatTM.qPosn_posStart {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] :
        QPosn posStart
        Dependency graph
        source
        theorem DescriptiveComplexity.QsatTM.qPosn_posEnd {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] :
        QPosn posEnd
        Dependency graph
        source
        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
        source
        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 #

        source
        theorem DescriptiveComplexity.QsatTM.pLe_cases {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] {x y : A} (h : PLe x y) :
        IsQVar x ∧ IsQVar y ∧ (x = y ∨ QPrec x y) ∨ IsQVar x ∧ ¬IsQVar y ∨ ¬IsQVar x ∧ ¬IsQVar y ∧ x ≤ y

        The three cases of the tape order on elements, as a disjunction rcases can see (DescriptiveComplexity.QsatTM.PLe is a def).

        Dependency graph
        source
        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
        source
        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
        source
        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
        source
        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
        source
        theorem DescriptiveComplexity.QsatTM.qLe_start_end {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] :
        QLe posStart posEnd
        Dependency graph
        source
        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
        source
        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
        source
        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
        source
        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 #

        source
        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
        source
        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

        Neighbours #

        source
        theorem DescriptiveComplexity.QsatTM.succPos_start_cell {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (hwf : QsatWf A) {x : A} (hx : QMinVar x) :
        SuccPos QLe QPosn posStart (posCell x)

        The left marker and the outermost variable are neighbours.

        Dependency graph
        source
        theorem DescriptiveComplexity.QsatTM.succPos_start_end {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (hno : ∀ (x : A), ¬IsQVar x) :
        SuccPos QLe QPosn posStart posEnd

        With no quantified variable the two markers are neighbours.

        Dependency graph
        source
        theorem DescriptiveComplexity.QsatTM.succPos_cell_cell {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (hwf : QsatWf A) {x y : A} (hxy : QNextVar x y) :
        SuccPos QLe QPosn (posCell x) (posCell y)

        Consecutive variables of the prefix are neighbours on the tape.

        Dependency graph
        source
        theorem DescriptiveComplexity.QsatTM.succPos_cell_end {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (hwf : QsatWf A) {x : A} (hx : QMaxVar x) :
        SuccPos QLe QPosn (posCell x) posEnd

        The innermost variable and the right marker are neighbours.

        Dependency graph