One step of the QBF machine

The transition table of DescriptiveComplexity.Problems.Machine.QsatProgram says which tuples are transitions; this file says what they do. There is one lemma per line of the program, each of the shape

in this state, at this cell, reading this symbol, the machine steps to that state, that cell, and that tape

with the movement supplied as a DescriptiveComplexity.SuccPos hypothesis, so that the boundary cases – the outermost variable, the innermost one, the degenerate instance with no variable at all – are handled by passing a different lemma of DescriptiveComplexity.Problems.Machine.QsatGeom rather than by duplicating each line of the program.

The tape after a step is never built here either: it is an arbitrary σ' required to hold the written symbol at the head and to agree with σ everywhere else, which is exactly what DescriptiveComplexity.TMData.Step asks and what the run induction will supply.

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.QsatTM.markerPos {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (d : Bool) : QV A

The marker a sweep in direction d ends at, as a position.

Equations

• DescriptiveComplexity.QsatTM.markerPos d = if d = true then DescriptiveComplexity.QsatTM.posEnd else DescriptiveComplexity.QsatTM.posStart

Descending

theorem DescriptiveComplexity.QsatTM.step_descStart {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {σ : QV A → QV A} {p' : QV A} (hσ : σ posStart = symStart) (hnext : SuccPos QLe QPosn posStart p') : (qsatMachine A).Step { state := stDesc, head := posStart, tape := σ } { state := stDesc, head := p', tape := σ }

Descent, over the left marker.

theorem DescriptiveComplexity.QsatTM.step_descCell {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) {b f : Bool} (hσ : σ (posCell x) = symV b f x) (hw : σ' (posCell x) = symV false false x) (hfr : ∀ (r : QV A), r ≠ posCell x → σ' r = σ r) (hnext : SuccPos QLe QPosn (posCell x) p') : (qsatMachine A).Step { state := stDesc, head := posCell x, tape := σ } { state := stDesc, head := p', tape := σ' }

Descent, at a variable's cell: reset it and move on.

theorem DescriptiveComplexity.QsatTM.step_descEndTrue {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {σ : QV A → QV A} {p' : QV A} (hno : ∀ (e : A), ¬QCl e) (hσ : σ posEnd = symEnd) (hprev : SuccPos QLe QPosn p' posEnd) : (qsatMachine A).Step { state := stDesc, head := posEnd, tape := σ } { state := stProc true, head := p', tape := σ }

Descent over, with an empty matrix: it is true, so start returning.

theorem DescriptiveComplexity.QsatTM.step_descEndEval {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {σ : QV A → QV A} {p' : QV A} {c : A} (hc : QMinCl c) (hσ : σ posEnd = symEnd) (hprev : SuccPos QLe QPosn p' posEnd) : (qsatMachine A).Step { state := stDesc, head := posEnd, tape := σ } { state := stEval false false c, head := p', tape := σ }

Descent over: start evaluating the matrix at its lowest clause.

Evaluating the matrix

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

The movement of an evaluation sweep, in its own direction.

Equations

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

theorem DescriptiveComplexity.QsatTM.step_eval_true {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {σ : QV A → QV A} {p' : QV A} {c x : A} (hc : QCl c) (hx : IsQVar x) {b f fl d : Bool} (hlit : fl = true ∨ QLit c x b) (hσ : σ (posCell x) = symV b f x) (hmove : SweepMove d (posCell x) p') : (qsatMachine A).Step { state := stEval fl d c, head := posCell x, tape := σ } { state := stEval true d c, head := p', tape := σ }

A sweep step that sets the flag: either it was already set, or the literal at this cell satisfies the clause.

theorem DescriptiveComplexity.QsatTM.step_eval_false {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {σ : QV A → QV A} {p' : QV A} {c x : A} (hc : QCl c) (hx : IsQVar x) {b f d : Bool} (hlit : ¬QLit c x b) (hσ : σ (posCell x) = symV b f x) (hmove : SweepMove d (posCell x) p') : (qsatMachine A).Step { state := stEval false d c, head := posCell x, tape := σ } { state := stEval false d c, head := p', tape := σ }

A sweep step that leaves the flag down: it was down and the literal at this cell does not satisfy the clause.

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

The movement of a turn, against the direction just swept.

Equations

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

theorem DescriptiveComplexity.QsatTM.step_turnNext {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {σ : QV A → QV A} {p' : QV A} {c c₂ : A} (hcc : QNextCl c c₂) {d : Bool} (hσ : σ (markerPos d) = markerSym d) (hmove : TurnMove d (markerPos d) p') : (qsatMachine A).Step { state := stEval true d c, head := markerPos d, tape := σ } { state := stEval false (!d) c₂, head := p', tape := σ }

Turn: the clause is satisfied and another one follows.

theorem DescriptiveComplexity.QsatTM.step_turnLast {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {σ : QV A → QV A} {p' : QV A} {c : A} (hc : QMaxCl c) {d : Bool} (hσ : σ (markerPos d) = markerSym d) (hmove : TurnMove d (markerPos d) p') : (qsatMachine A).Step { state := stEval true d c, head := markerPos d, tape := σ } { state := stToEnd true, head := p', tape := σ }

Turn: the clause is satisfied and it was the last one, so the matrix is true.

theorem DescriptiveComplexity.QsatTM.step_turnFalse {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {σ : QV A → QV A} {p' : QV A} {c : A} (hc : QCl c) {d : Bool} (hσ : σ (markerPos d) = markerSym d) (hmove : TurnMove d (markerPos d) p') : (qsatMachine A).Step { state := stEval false d c, head := markerPos d, tape := σ } { state := stToEnd false, head := p', tape := σ }

Turn: the clause is not satisfied, so the matrix is false.

Carrying the value to the right marker

theorem DescriptiveComplexity.QsatTM.step_toEndCell {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) {v b f : Bool} (hσ : σ (posCell x) = symV b f x) (hnext : SuccPos QLe QPosn (posCell x) p') : (qsatMachine A).Step { state := stToEnd v, head := posCell x, tape := σ } { state := stToEnd v, head := p', tape := σ }

Carry, over a variable's cell.

theorem DescriptiveComplexity.QsatTM.step_toEndStart {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {σ : QV A → QV A} {p' : QV A} {v : Bool} (hσ : σ posStart = symStart) (hnext : SuccPos QLe QPosn posStart p') : (qsatMachine A).Step { state := stToEnd v, head := posStart, tape := σ } { state := stToEnd v, head := p', tape := σ }

Carry, over the left marker.

theorem DescriptiveComplexity.QsatTM.step_toEndTurn {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {σ : QV A → QV A} {p' : QV A} {v : Bool} (hσ : σ posEnd = symEnd) (hprev : SuccPos QLe QPosn p' posEnd) : (qsatMachine A).Step { state := stToEnd v, head := posEnd, tape := σ } { state := stProc v, head := p', tape := σ }

Carry over: the right marker is reached, so turn round and return.

Returning through the prefix

theorem DescriptiveComplexity.QsatTM.step_procSkip {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) {v b f : Bool} (hdec : QShort v x ∨ f = true) (hσ : σ (posCell x) = symV b f x) (hprev : SuccPos QLe QPosn p' (posCell x)) : (qsatMachine A).Step { state := stProc v, head := posCell x, tape := σ } { state := stProc v, head := p', tape := σ }

Return, past a decided level: the quantifier settles it, or both its values have already been tried.

theorem DescriptiveComplexity.QsatTM.step_procSwitch {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) {v b : Bool} (hdec : ¬QShort v x) (hσ : σ (posCell x) = symV b false x) (hw : σ' (posCell x) = symV true true x) (hfr : ∀ (r : QV A), r ≠ posCell x → σ' r = σ r) (hnext : SuccPos QLe QPosn (posCell x) p') : (qsatMachine A).Step { state := stProc v, head := posCell x, tape := σ } { state := stDesc, head := p', tape := σ' }

Return, at an undecided level: try the second value and descend again.

theorem DescriptiveComplexity.QsatTM.step_procAcc {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {σ : QV A → QV A} {p' : QV A} (hσ : σ posStart = symStart) (hnext : SuccPos QLe QPosn posStart p') : (qsatMachine A).Step { state := stProc true, head := posStart, tape := σ } { state := stAcc, head := p', tape := σ }

Return over: the prefix is exhausted and the value is true, so accept.

The initial configuration

Where the machine starts: descending, at the left marker, on the tape the instance prescribes. Every cell of the tape carries a symbol – the markers their own, a variable's cell the value false with the flag down – so the blank is never read, and it is only there because DescriptiveComplexity.TMData.InitTape needs a default for the tuples that are not cells at all.

noncomputable def DescriptiveComplexity.QsatTM.initTape {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (p : QV A) : QV A

The tape the machine starts on. It depends on the tag and on the first coordinate alone, which is what makes it agree with DescriptiveComplexity.QsatTM.QInp at every tuple, junk included.

Equations

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

theorem DescriptiveComplexity.QsatTM.not_qInp_of_junk {A : Type} [LinearOrder A] {p : QV A} (h : p.1 ≠ QTag.pStart) (h' : p.1 ≠ QTag.pCell) (h'' : p.1 ≠ QTag.pEnd) (a : QV A) : ¬QInp p a

Away from the three position tags the instance prescribes nothing.

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

The starting tape is the initial tape of the instance.

theorem DescriptiveComplexity.QsatTM.isInit_start {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (hwf : QsatWf A) : (qsatMachine A).IsInit { state := stDesc, head := posStart, tape := initTape }

The machine starts descending at the left marker.

@[simp]

theorem DescriptiveComplexity.QsatTM.initTape_posStart {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : initTape posStart = symStart

The starting tape, read at the left marker.

@[simp]

theorem DescriptiveComplexity.QsatTM.initTape_posEnd {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : initTape posEnd = symEnd

The starting tape, read at the right marker.

@[simp]

theorem DescriptiveComplexity.QsatTM.initTape_posCell {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (x : A) : initTape (posCell x) = symV false false x

The starting tape, read at a variable's cell.

Where the machine stops

The two dead ends, both of them facts about the table alone: nothing follows an accepting configuration, and nothing follows a false returned past the outermost quantifier. They are exactly the side conditions of DescriptiveComplexity.TMData.not_acceptsSpace_of_reaches_dead, which is what turns one exhibited run into non-acceptance for a no-instance.

theorem DescriptiveComplexity.QsatTM.qStateTag_ne_acc (t : QTag) : qIsTrTag t = true → qStateTag t ≠ QTag.qAcc

No transition applies in the accepting state.

theorem DescriptiveComplexity.QsatTM.qStateTag_procFalse (t : QTag) : qIsTrTag t = true → qStateTag t = QTag.qProc false → qReadTag t ≠ QTag.sStart

No transition applies to a false at the left marker: the two return transitions read a variable's cell, and the accepting one needs a true.

theorem DescriptiveComplexity.QsatTM.not_step_of_acc {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {c c' : Config (QV A)} (hacc : (qsatMachine A).Acc c.state) : ¬(qsatMachine A).Step c c'

The accepting state is a sink.

theorem DescriptiveComplexity.QsatTM.not_step_procFalse {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {σ : QV A → QV A} (hσ : σ posStart = symStart) {c' : Config (QV A)} : ¬(qsatMachine A).Step { state := stProc false, head := posStart, tape := σ } c'

A false returned past the outermost quantifier is a dead end.

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

The accepting configuration is accepting, on a well-formed instance: the guard on DescriptiveComplexity.QsatTM.QAcc is discharged.

theorem DescriptiveComplexity.QsatTM.not_acc_stProcFalse {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] : ¬(qsatMachine A).Acc (stProc false)

A false at the left marker is not accepting.