The run of the QBF machine

What the machine computes. This file opens with the dictionary between a tape and a valuation, since that is what the evaluation sweep and the game semantics have to be compared through.

A tape of the machine is laid out (DescriptiveComplexity.QsatTM.TapeOk) when every quantified variable's cell holds one of the four sVal symbols – which the initial tape does and every transition preserves. Such a tape is a valuation (DescriptiveComplexity.QsatTM.TapeTrue: the variable is true when its cell holds the value true), and under that dictionary the first-order literal test the transition table performs (DescriptiveComplexity.QsatTM.QLit) is the literal of DescriptiveComplexity.QsatMatrix. DescriptiveComplexity.QsatTM.qsatMatrix_iff is the resulting reading of the matrix: it holds exactly when every clause has a variable whose cell satisfies it, which is what one full sweep of the Eval phase decides.

A tape is a valuation

def DescriptiveComplexity.QsatTM.TapeOk {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (σ : QV A → QV A) : Prop

A tape is laid out when every quantified variable's cell holds a value and a flag. The initial tape is, and every transition preserves it.

Equations

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

def DescriptiveComplexity.QsatTM.TapeTrue {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (σ : QV A → QV A) (x : A) : Prop

The valuation a tape encodes: the variable x is true when its cell holds the value true.

Equations

• DescriptiveComplexity.QsatTM.TapeTrue σ x = ∃ (f : Bool), σ (DescriptiveComplexity.QsatTM.posCell x) = DescriptiveComplexity.QsatTM.symV true f x

theorem DescriptiveComplexity.QsatTM.tapeTrue_iff {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {σ : QV A → QV A} {x : A} {b f : Bool} (hσ : σ (posCell x) = symV b f x) : TapeTrue σ x ↔ b = true

Reading the valuation off a cell whose contents are known.

theorem DescriptiveComplexity.QsatTM.qLit_iff_tapeTrue {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {σ : QV A → QV A} {c x : A} {b f : Bool} (hσ : σ (posCell x) = symV b f x) : QLit c x b ↔ QPosIn c x ∧ TapeTrue σ x ∨ QNegIn c x ∧ ¬TapeTrue σ x

The transition table's literal test is the literal of the matrix. The sweep asks QLit c x b of the symbol it reads; the game asks whether the valuation satisfies the literal. Under the dictionary they agree.

The matrix, read off the tape

theorem DescriptiveComplexity.QsatTM.qsatMatrix_iff {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {σ : QV A → QV A} (hok : TapeOk σ) : QsatMatrix (TapeTrue σ) ↔ ∀ (c : A), QCl c → ∃ (x : A) (b : Bool) (f : Bool), IsQVar x ∧ σ (posCell x) = symV b f x ∧ QLit c x b

The matrix holds of a laid-out tape exactly when every clause has a cell satisfying it. The right-hand side is what one full sweep of the evaluation phase decides, clause by clause; the left-hand side is what the game asks at a leaf.

Writing a cell

Every transition that changes the tape changes one cell of one variable, so the run only ever needs this one update. The step lemmas of DescriptiveComplexity.Problems.Machine.QsatStep take the next tape as an arbitrary σ' pinned at the head; DescriptiveComplexity.QsatTM.setCell is the σ' the run will always pass them.

noncomputable def DescriptiveComplexity.QsatTM.setCell {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (σ : QV A → QV A) (x : A) (b f : Bool) : QV A → QV A

The tape σ with the cell of x set to the value b and the flag f.

Equations

• DescriptiveComplexity.QsatTM.setCell σ x b f r = if r = DescriptiveComplexity.QsatTM.posCell x then DescriptiveComplexity.QsatTM.symV b f x else σ r

@[simp]

theorem DescriptiveComplexity.QsatTM.setCell_self {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {σ : QV A → QV A} (x : A) (b f : Bool) : setCell σ x b f (posCell x) = symV b f x

theorem DescriptiveComplexity.QsatTM.setCell_ne {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {σ : QV A → QV A} {x : A} {b f : Bool} {r : QV A} (h : r ≠ posCell x) : setCell σ x b f r = σ r

theorem DescriptiveComplexity.QsatTM.setCell_other {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {σ : QV A → QV A} {x y : A} {b f : Bool} (h : y ≠ x) : setCell σ x b f (posCell y) = σ (posCell y)

Another variable's cell is untouched.

theorem DescriptiveComplexity.QsatTM.tapeOk_setCell {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {σ : QV A → QV A} (hok : TapeOk σ) (x : A) (b f : Bool) : TapeOk (setCell σ x b f)

Writing a cell keeps the tape laid out.

@[simp]

theorem DescriptiveComplexity.QsatTM.tapeTrue_setCell_self {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {σ : QV A → QV A} {x : A} {b f : Bool} : TapeTrue (setCell σ x b f) x ↔ b = true

Writing a cell sets that variable's value.

theorem DescriptiveComplexity.QsatTM.tapeTrue_setCell_other {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {σ : QV A → QV A} {x y : A} {b f : Bool} (h : y ≠ x) : TapeTrue (setCell σ x b f) y ↔ TapeTrue σ y

Writing a cell leaves every other variable's value alone.

theorem DescriptiveComplexity.QsatTM.setCell_frame {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {σ : QV A → QV A} (x : A) (b f : Bool) (r : QV A) : r ≠ posCell x → setCell σ x b f r = σ r

The frame condition the step lemmas ask for, discharged for DescriptiveComplexity.QsatTM.setCell.

The descent

The machine's first act, and the act it repeats every time a level switches to its second value: sweep rightwards to the right marker, resetting every variable's cell on the way. The sweep is the segment primitive of DescriptiveComplexity.Problems.Machine.Program, whose configuration family is p ↦ ⟨stDesc, p, resetSeg σ p₀ p⟩ – the tape with every variable cell of the half-open segment [p₀, p) reset.

noncomputable def DescriptiveComplexity.QsatTM.resetSeg {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (σ : QV A → QV A) (p₀ p r : QV A) : QV A

The tape σ with every variable cell of the segment [p₀, p) reset.

Equations

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

theorem DescriptiveComplexity.QsatTM.resetSeg_of_not {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {σ : QV A → QV A} {p₀ p r : QV A} (h : ¬(QPosn r ∧ r.1 = QTag.pCell ∧ QLe p₀ r ∧ QLe r p ∧ r ≠ p)) : resetSeg σ p₀ p r = σ r

theorem DescriptiveComplexity.QsatTM.resetSeg_self {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {σ : QV A → QV A} (p₀ p : QV A) : resetSeg σ p₀ p p = σ p

theorem DescriptiveComplexity.QsatTM.resetSeg_bot {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {σ : QV A → QV A} (hwf : QsatWf A) (p₀ : QV A) : resetSeg σ p₀ p₀ = σ

An empty segment changes nothing.

theorem DescriptiveComplexity.QsatTM.resetSeg_frame {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {σ : QV A → QV A} (hwf : QsatWf A) {p₀ p q : QV A} (hs : SuccPos QLe QPosn p q) (hle : QLe p₀ p) (r : QV A) : r ≠ p → resetSeg σ p₀ q r = resetSeg σ p₀ p r

Extending the segment by one position changes only that position.

theorem DescriptiveComplexity.QsatTM.resetSeg_at {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {σ : QV A → QV A} {p₀ p q : QV A} {x : A} (hs : SuccPos QLe QPosn p q) (hle : QLe p₀ p) (hp : p = posCell x) : resetSeg σ p₀ q p = symV false false x

Extending the segment past a variable's cell resets that cell.

theorem DescriptiveComplexity.QsatTM.reach_descent {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {σ : QV A → QV A} (hwf : QsatWf A) (hok : TapeOk σ) (hstart : σ posStart = symStart) {p₀ : QV A} (hp₀ : QPosn p₀) : Relation.ReflTransGen (qsatMachine A).Step { state := stDesc, head := p₀, tape := σ } { state := stDesc, head := posEnd, tape := resetSeg σ p₀ posEnd }

The descent runs to the right marker, resetting every variable's cell from p₀ on.

The evaluation sweep

One pass over the tape for one clause. The state carries the flag, and the flag at a position is exactly "some variable's cell already swept satisfies the clause"; the pass therefore ends at the far marker with the flag set iff the clause holds of the tape.

def DescriptiveComplexity.QsatTM.CellSat {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (σ : QV A → QV A) (c x : A) : Prop

A variable's cell satisfies the clause c.

Equations

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

def DescriptiveComplexity.QsatTM.SatAbove {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (σ : QV A → QV A) (c : A) (p : QV A) : Prop

Some cell strictly above p satisfies the clause: the flag of a leftward sweep that has reached p.

Equations

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

def DescriptiveComplexity.QsatTM.SatAll {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (σ : QV A → QV A) (c : A) : Prop

Some cell satisfies the clause: what a whole pass decides.

Equations

• DescriptiveComplexity.QsatTM.SatAll σ c = ∃ (x : A), DescriptiveComplexity.QsatTM.CellSat σ c x

noncomputable def DescriptiveComplexity.QsatTM.flagAbove {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (σ : QV A → QV A) (c : A) (p : QV A) : Bool

The flag of a leftward sweep that has reached p.

Equations

• DescriptiveComplexity.QsatTM.flagAbove σ c p = decide (DescriptiveComplexity.QsatTM.SatAbove σ c p)

theorem DescriptiveComplexity.QsatTM.flagAbove_eq_true {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (σ : QV A → QV A) (c : A) (p : QV A) : flagAbove σ c p = true ↔ SatAbove σ c p

theorem DescriptiveComplexity.QsatTM.flagAbove_eq_false {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (σ : QV A → QV A) (c : A) (p : QV A) : flagAbove σ c p = false ↔ ¬SatAbove σ c p

theorem DescriptiveComplexity.QsatTM.satAbove_succ {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {σ : QV A → QV A} (hwf : QsatWf A) {c x : A} {b f : Bool} {p q : QV A} (hs : SuccPos QLe QPosn p q) (hq : q = posCell x) (hx : IsQVar x) (hσ : σ (posCell x) = symV b f x) : SatAbove σ c p ↔ SatAbove σ c q ∨ QLit c x b

The flag accumulates: sweeping one cell further adds that cell's verdict.

theorem DescriptiveComplexity.QsatTM.satAbove_posStart {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (σ : QV A → QV A) (c : A) : SatAbove σ c posStart ↔ SatAll σ c

At the left marker the flag is the verdict on the whole tape.

theorem DescriptiveComplexity.QsatTM.not_satAbove_top {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (σ : QV A → QV A) (c : A) {p₁ : QV A} (hs : SuccPos QLe QPosn p₁ posEnd) : ¬SatAbove σ c p₁

Just below the right marker nothing has been swept yet.

theorem DescriptiveComplexity.QsatTM.reach_sweepDown {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {σ : QV A → QV A} (hwf : QsatWf A) (hok : TapeOk σ) {c : A} (hc : QCl c) {p₁ : QV A} (hs : SuccPos QLe QPosn p₁ posEnd) : Relation.ReflTransGen (qsatMachine A).Step { state := stEval false false c, head := p₁, tape := σ } { state := stEval (flagAbove σ c posStart) false c, head := posStart, tape := σ }

A leftward pass decides the clause. From just below the right marker, with the flag down, the machine sweeps to the left marker and arrives with the flag set exactly when some cell satisfies the clause.

def DescriptiveComplexity.QsatTM.SatBelow {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (σ : QV A → QV A) (c : A) (p : QV A) : Prop

Some cell strictly below p satisfies the clause: the flag of a rightward sweep that has reached p.

Equations

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

noncomputable def DescriptiveComplexity.QsatTM.flagBelow {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (σ : QV A → QV A) (c : A) (p : QV A) : Bool

The flag of a rightward sweep that has reached p.

Equations

• DescriptiveComplexity.QsatTM.flagBelow σ c p = decide (DescriptiveComplexity.QsatTM.SatBelow σ c p)

theorem DescriptiveComplexity.QsatTM.flagBelow_eq_true {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (σ : QV A → QV A) (c : A) (p : QV A) : flagBelow σ c p = true ↔ SatBelow σ c p

theorem DescriptiveComplexity.QsatTM.flagBelow_eq_false {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (σ : QV A → QV A) (c : A) (p : QV A) : flagBelow σ c p = false ↔ ¬SatBelow σ c p

theorem DescriptiveComplexity.QsatTM.satBelow_succ {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {σ : QV A → QV A} (hwf : QsatWf A) {c x : A} {b f : Bool} {p q : QV A} (hs : SuccPos QLe QPosn p q) (hp : p = posCell x) (hx : IsQVar x) (hσ : σ (posCell x) = symV b f x) : SatBelow σ c q ↔ SatBelow σ c p ∨ QLit c x b

The flag accumulates, rightwards.

theorem DescriptiveComplexity.QsatTM.satBelow_posEnd {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (σ : QV A → QV A) (c : A) : SatBelow σ c posEnd ↔ SatAll σ c

At the right marker the flag is the verdict on the whole tape.

theorem DescriptiveComplexity.QsatTM.not_satBelow_bot {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (σ : QV A → QV A) (c : A) {p₀ : QV A} (hs : SuccPos QLe QPosn posStart p₀) : ¬SatBelow σ c p₀

Just above the left marker nothing has been swept yet.

theorem DescriptiveComplexity.QsatTM.reach_sweepUp {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {σ : QV A → QV A} (hwf : QsatWf A) (hok : TapeOk σ) {c : A} (hc : QCl c) {p₀ : QV A} (hs : SuccPos QLe QPosn posStart p₀) : Relation.ReflTransGen (qsatMachine A).Step { state := stEval false true c, head := p₀, tape := σ } { state := stEval (flagBelow σ c posEnd) true c, head := posEnd, tape := σ }

A rightward pass decides the clause.

The clause loop

One pass per clause, alternating direction, until a clause fails or the last one succeeds. The recursion is on the clause in the ambient order, which is well founded because the instance is finite.

noncomputable def DescriptiveComplexity.QsatTM.satFlag {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (σ : QV A → QV A) (c : A) : Bool

The verdict on one clause.

Equations

• DescriptiveComplexity.QsatTM.satFlag σ c = decide (DescriptiveComplexity.QsatTM.SatAll σ c)

noncomputable def DescriptiveComplexity.QsatTM.matrixFrom {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (σ : QV A → QV A) (c : A) : Bool

The verdict on every clause from c on: what the loop started at c returns.

Equations

• DescriptiveComplexity.QsatTM.matrixFrom σ c = decide (∀ (e : A), DescriptiveComplexity.QsatTM.QCl e → c ≤ e → DescriptiveComplexity.QsatTM.SatAll σ e)

theorem DescriptiveComplexity.QsatTM.flagAbove_posStart {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (σ : QV A → QV A) (c : A) : flagAbove σ c posStart = satFlag σ c

theorem DescriptiveComplexity.QsatTM.flagBelow_posEnd {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (σ : QV A → QV A) (c : A) : flagBelow σ c posEnd = satFlag σ c

def DescriptiveComplexity.QsatTM.SweepStart {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (d : Bool) (p : QV A) : Prop

Where a sweep in direction d starts: one step in from the marker it will end at going the other way.

Equations

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

theorem DescriptiveComplexity.QsatTM.reach_pass {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {σ : QV A → QV A} (hwf : QsatWf A) (hok : TapeOk σ) {c : A} (hc : QCl c) {d : Bool} {p : QV A} (hp : SweepStart d p) : Relation.ReflTransGen (qsatMachine A).Step { state := stEval false d c, head := p, tape := σ } { state := stEval (satFlag σ c) d c, head := markerPos d, tape := σ }

One pass: whatever the direction, the machine sweeps from its starting position to the far marker and arrives with the clause's verdict.

theorem DescriptiveComplexity.QsatTM.matrixFrom_eq_false {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {σ : QV A → QV A} {c : A} (hc : QCl c) (h : ¬SatAll σ c) : matrixFrom σ c = false

An unsatisfied clause is a counterexample to every clause from c on.

theorem DescriptiveComplexity.QsatTM.matrixFrom_eq_true_of_max {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {σ : QV A → QV A} {c : A} (hc : QMaxCl c) (h : SatAll σ c) : matrixFrom σ c = true

The last clause satisfied settles the loop.

theorem DescriptiveComplexity.QsatTM.matrixFrom_succ {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {σ : QV A → QV A} {c c₂ : A} (hcc : QNextCl c c₂) (h : SatAll σ c) : matrixFrom σ c = matrixFrom σ c₂

Passing a satisfied clause leaves the rest of the loop to decide.

theorem DescriptiveComplexity.QsatTM.exists_afterStart {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (hwf : QsatWf A) : ∃ (p : QV A), SuccPos QLe QPosn posStart p

The left marker has a neighbour: the right marker is above it.

theorem DescriptiveComplexity.QsatTM.exists_beforeEnd {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (hwf : QsatWf A) : ∃ (p : QV A), SuccPos QLe QPosn p posEnd

The right marker has a neighbour: the left marker is below it.

theorem DescriptiveComplexity.QsatTM.turn_pos {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (hwf : QsatWf A) (d : Bool) : ∃ (p' : QV A), QPosn p' ∧ TurnMove d (markerPos d) p' ∧ SweepStart (!d) p'

Where a turn lands: one step in from the marker just reached, which is where the next sweep – in the opposite direction – starts.

theorem DescriptiveComplexity.QsatTM.qMaxCl_or_next {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] {c : A} (hc : QCl c) : QMaxCl c ∨ ∃ (c₂ : A), QNextCl c c₂

Every clause is the last one or has a successor.

theorem DescriptiveComplexity.QsatTM.marker_tape {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {σ : QV A → QV A} (hS : σ posStart = symStart) (hE : σ posEnd = symEnd) (d : Bool) : σ (markerPos d) = markerSym d

theorem DescriptiveComplexity.QsatTM.turn_unsat {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {σ : QV A → QV A} (hwf : QsatWf A) (hok : TapeOk σ) (hM : ∀ (d : Bool), σ (markerPos d) = markerSym d) {c : A} (hc : QCl c) (hunsat : ¬SatAll σ c) {d : Bool} {p : QV A} (hp : SweepStart d p) : ∃ (q : QV A), QPosn q ∧ Relation.ReflTransGen (qsatMachine A).Step { state := stEval false d c, head := p, tape := σ } { state := stToEnd (matrixFrom σ c), head := q, tape := σ }

An unsatisfied clause ends the loop: the matrix is false.

theorem DescriptiveComplexity.QsatTM.turn_final {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {σ : QV A → QV A} (hwf : QsatWf A) (hok : TapeOk σ) (hM : ∀ (d : Bool), σ (markerPos d) = markerSym d) {c : A} (hc : QCl c) (hmax : QMaxCl c) {d : Bool} {p : QV A} (hp : SweepStart d p) : ∃ (q : QV A), QPosn q ∧ Relation.ReflTransGen (qsatMachine A).Step { state := stEval false d c, head := p, tape := σ } { state := stToEnd (matrixFrom σ c), head := q, tape := σ }

The last clause ends the loop, whichever way it goes.

theorem DescriptiveComplexity.QsatTM.reach_evalLoop {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {σ : QV A → QV A} (hwf : QsatWf A) (hok : TapeOk σ) (hS : σ posStart = symStart) (hE : σ posEnd = symEnd) (n : ℕ) (c : A) : {e : A | c < e}.ncard ≤ n → QCl c → ∀ (d : Bool) (p : QV A), SweepStart d p → ∃ (q : QV A), QPosn q ∧ Relation.ReflTransGen (qsatMachine A).Step { state := stEval false d c, head := p, tape := σ } { state := stToEnd (matrixFrom σ c), head := q, tape := σ }

The clause loop. Starting a sweep for the clause c, the machine carries out one pass per clause from c on, alternating direction, and hands the verdict to the carry phase. The recursion is on the number of clauses left above c.

Carrying the verdict back

theorem DescriptiveComplexity.QsatTM.reach_toEnd {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {σ : QV A → QV A} (hwf : QsatWf A) (hok : TapeOk σ) (hS : σ posStart = symStart) (hE : σ posEnd = symEnd) (v : Bool) {q : QV A} (hq : QPosn q) {p' : QV A} (hp' : SuccPos QLe QPosn p' posEnd) : Relation.ReflTransGen (qsatMachine A).Step { state := stToEnd v, head := q, tape := σ } { state := stProc v, head := p', tape := σ }

The carry phase walks to the right marker and turns round, leaving the machine returning the verdict at the innermost variable.

theorem DescriptiveComplexity.QsatTM.reach_matrix {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {σ : QV A → QV A} (hwf : QsatWf A) (hok : TapeOk σ) (hS : σ posStart = symStart) (hE : σ posEnd = symEnd) {p' : QV A} (hp' : SuccPos QLe QPosn p' posEnd) : ∃ (b : Bool), (b = true ↔ QsatMatrix (TapeTrue σ)) ∧ Relation.ReflTransGen (qsatMachine A).Step { state := stDesc, head := posEnd, tape := σ } { state := stProc b, head := p', tape := σ }

The whole evaluation phase: from the right marker with the descent just finished, the machine decides the matrix and comes back returning it at the innermost variable.

The position of the game, read off the tape

The dictionary for the prefix, as DescriptiveComplexity.QsatTM.TapeTrue was the dictionary for the valuation: the head sitting at p means the game has already quantified exactly the variables whose cells lie strictly below p.

def DescriptiveComplexity.QsatTM.Before {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (p : QV A) (x : A) : Prop

The variables the prefix binds strictly before the position p: the D of the game position the machine is in when its head is at p.

Equations

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

theorem DescriptiveComplexity.QsatTM.before_posEnd {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (x : A) : Before posEnd x ↔ IsQVar x

At the right marker every variable has been quantified, so the game is at a leaf.

theorem DescriptiveComplexity.QsatTM.qLeast_before {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (hwf : QsatWf A) {v : A} (hv : IsQVar v) : QLeast (Before (posCell v)) v

At a variable's cell, that variable is the one the prefix binds next.

theorem DescriptiveComplexity.QsatTM.before_succ {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (hwf : QsatWf A) {v : A} (hv : IsQVar v) {q : QV A} (hs : SuccPos QLe QPosn (posCell v) q) : Before q = qAdd (Before (posCell v)) v

Stepping the head past a variable's cell quantifies that variable.

theorem DescriptiveComplexity.QsatTM.tapeTrue_setCell {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {σ : QV A → QV A} (v : A) (b f : Bool) : TapeTrue (setCell σ v b f) = qUpd (TapeTrue σ) v b

Writing a cell is updating the valuation.

The two ways a level is decided

The Proc phase reads a returned value and either settles the level or tries its second value. These are the two game-theoretic facts behind that, and they are about DescriptiveComplexity.QsatWins alone – no machine.

theorem DescriptiveComplexity.QsatTM.qsatWins_of_short {A : Type} [FirstOrder.Language.qsat.Structure A] (hwf : QsatWf A) {D τ : A → Prop} {w : A} (hw : QLeast D w) {b bw : Bool} (hbr : b = true ↔ QsatWins (qAdd D w) (qUpd τ w bw)) (hsh : QShort b w) : b = true ↔ QsatWins D τ

A short circuit settles the level. An existential level reached by a winning branch is won; a universal level reached by a losing branch is lost.

theorem DescriptiveComplexity.QsatTM.qsatWins_of_second {A : Type} [FirstOrder.Language.qsat.Structure A] (hwf : QsatWf A) {D τ : A → Prop} {w : A} (hw : QLeast D w) {b₁ b₂ : Bool} (hns : ¬QShort b₁ w) (hb1 : b₁ = true ↔ QsatWins (qAdd D w) (qUpd τ w false)) (hb2 : b₂ = true ↔ QsatWins (qAdd D w) (qUpd τ w true)) : b₂ = true ↔ QsatWins D τ

Without a short circuit the second branch settles the level.

The game induction

The last step, and the one the whole file was preparing: the machine's descent and return compute the value of the game position its head sits at.

Two nested recursions. The outer one is on the variables still to be quantified at p; the inner one walks the Proc phase leftwards from the innermost variable back to p. The inner walk calls the outer one exactly once, at a switch, and on strictly fewer variables – which is what makes the pair well founded.

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

The variables the prefix has still to bind when the head is at p.

Equations

• DescriptiveComplexity.QsatTM.RestCells p = {x : A | DescriptiveComplexity.IsQVar x ∧ DescriptiveComplexity.QsatTM.QLe p (DescriptiveComplexity.QsatTM.posCell x)}

theorem DescriptiveComplexity.QsatTM.qUpd_tapeTrue {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {σ : QV A → QV A} {w : A} {bw f : Bool} (hσ : σ (posCell w) = symV bw f w) : qUpd (TapeTrue σ) w bw = TapeTrue σ

A cell holding its own value updates the valuation to itself.

theorem DescriptiveComplexity.QsatTM.qsatWins_before_congr {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {p : QV A} {σ τ : QV A → QV A} (h : ∀ (x : A), IsQVar x → QLe (posCell x) p → posCell x ≠ p → (TapeTrue σ x ↔ TapeTrue τ x)) : QsatWins (Before p) (TapeTrue σ) ↔ QsatWins (Before p) (TapeTrue τ)

The game position at p only reads the cells strictly below p, so two tapes agreeing there decide it alike.

theorem DescriptiveComplexity.QsatTM.reach_game_posEnd {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {σ : QV A → QV A} (hwf : QsatWf A) (hok : TapeOk σ) (hS : σ posStart = symStart) (hE : σ posEnd = symEnd) {p' : QV A} (hp' : SuccPos QLe QPosn p' posEnd) : ∃ (b : Bool), (b = true ↔ QsatWins (Before posEnd) (TapeTrue σ)) ∧ Relation.ReflTransGen (qsatMachine A).Step { state := stDesc, head := posEnd, tape := σ } { state := stProc b, head := p', tape := σ }

At the right marker the descent is over and the game is at a leaf.

theorem DescriptiveComplexity.QsatTM.not_succPos_posStart {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (hwf : QsatWf A) {p' : QV A} (hp' : SuccPos QLe QPosn p' posStart) : False

The left marker has nothing below it.

The tape after a descent

theorem DescriptiveComplexity.QsatTM.resetSeg_posEnd_cell {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {σ : QV A → QV A} {p₀ : QV A} {x : A} (hx : IsQVar x) (hle : QLe p₀ (posCell x)) : resetSeg σ p₀ posEnd (posCell x) = symV false false x

theorem DescriptiveComplexity.QsatTM.resetSeg_of_not_le {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {σ : QV A → QV A} {p₀ p r : QV A} (h : ¬QLe p₀ r) : resetSeg σ p₀ p r = σ r

theorem DescriptiveComplexity.QsatTM.resetSeg_posStart {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {σ : QV A → QV A} {p₀ p : QV A} : resetSeg σ p₀ p posStart = σ posStart

theorem DescriptiveComplexity.QsatTM.resetSeg_posEnd {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {σ : QV A → QV A} {p₀ p : QV A} : resetSeg σ p₀ p posEnd = σ posEnd

theorem DescriptiveComplexity.QsatTM.tapeOk_resetSeg {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {σ : QV A → QV A} (hok : TapeOk σ) (p₀ p : QV A) : TapeOk (resetSeg σ p₀ p)

The tape after a descent is laid out.

theorem DescriptiveComplexity.QsatTM.exists_beforeCell {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (hwf : QsatWf A) {w : A} (hw : IsQVar w) : ∃ (r : QV A), SuccPos QLe QPosn r (posCell w)

Every variable's cell has a neighbour below it.

theorem DescriptiveComplexity.QsatTM.cell_of_between {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {v w : A} {r : QV A} (hr : QPosn r) (h1 : QLe (posCell v) r) (h2 : QLe r (posCell w)) : ∃ (u : A), IsQVar u ∧ r = posCell u

A position between two variables' cells is a variable's cell.

theorem DescriptiveComplexity.QsatTM.mem_restCells {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {p : QV A} {x : A} (hx : IsQVar x) (hle : QLe p (posCell x)) : x ∈ RestCells p

The cell of a variable at or after p is one of the variables p leaves to be quantified.

theorem DescriptiveComplexity.QsatTM.reach_game {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (hwf : QsatWf A) (n : ℕ) (p : QV A) : QPosn p → (RestCells p).ncard ≤ n → ∀ (ρ : QV A → QV A), TapeOk ρ → ρ posStart = symStart → ρ posEnd = symEnd → ∀ (p' : QV A), SuccPos QLe QPosn p' p → ∃ (b : Bool) (ρ' : QV A → QV A), TapeOk ρ' ∧ ρ' posStart = symStart ∧ ρ' posEnd = symEnd ∧ (∀ (x : A), IsQVar x → QLe (posCell x) p → posCell x ≠ p → ρ' (posCell x) = ρ (posCell x)) ∧ (b = true ↔ QsatWins (Before p) (TapeTrue ρ)) ∧ Relation.ReflTransGen (qsatMachine A).Step { state := stDesc, head := p, tape := ρ } { state := stProc b, head := p', tape := ρ' }

The machine computes the game. From the descent at p the machine comes back, at the position just below p, returning the value of the game position whose already-quantified variables are exactly those below p.

The outer recursion is on the variables still to be bound at p; the inner one – walk – follows the return phase leftwards from the innermost variable back to p, and calls the outer one once, at a switch, on strictly fewer variables.

The tape the machine starts on

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

The initial tape is laid out.

theorem DescriptiveComplexity.QsatTM.not_tapeTrue_initTape {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (x : A) : ¬TapeTrue initTape x

The initial tape makes every variable false.

The machine decides QSAT

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

The machine is well formed on a well-formed instance.

theorem DescriptiveComplexity.QsatTM.before_afterStart {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {p₀ : QV A} (hs : SuccPos QLe QPosn posStart p₀) : Before p₀ = fun (x : A) => False

Nothing is quantified when the head has only just left the left marker.

theorem DescriptiveComplexity.QsatTM.qsatMachine_acceptsSpace_iff {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (hwf : QsatWf A) : (qsatMachine A).AcceptsSpace ↔ QsatWins (fun (x : A) => False) fun (x : A) => False

The machine accepts exactly the true formulas.

theorem DescriptiveComplexity.QsatTM.qsatMachine_correct {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] : (qsatMachine A).WellFormed ∧ (qsatMachine A).Deterministic ∧ (qsatMachine A).AcceptsSpace ↔ QsatHolds A

The machine of a QSAT instance decides it. A malformed instance has no accepting state, so it is a no-instance on both sides.