Documentation

DescriptiveComplexity.Problems.Machine.AltCheck

The intended run: the check phase #

Once the k sweeps have written DescriptiveComplexity.qbfVal in every cell, the machine walks the clauses one by one, sweeping the tape and accumulating a flag. The tape never changes again, so the frame condition of every step here is rfl.

The flag means two different things, and that is the whole of the disjunctive case. For a conjunctive matrix it records that some literal of the clause is satisfied; for a disjunctive one, that some literal of the term is violated. The two are the same test at the flipped truth value (DescriptiveComplexity.xorB), so one transition family serves both, and the accepting turn fires at the flag cnf: set for a conjunctive matrix, where it means the clause is satisfied, clear for a disjunctive one, where it means no literal of the term is violated.

A sweep alternates direction with each clause, as in DescriptiveComplexity.Problems.Machine.Hardness: the first runs rightwards from the first cell, having been entered by DescriptiveComplexity.step_toChk.

What the check tests #

def DescriptiveComplexity.AltQbf.QGood (k : ℕ) {A : Type} [(FirstOrder.Language.qbf k).Structure A] (cnf : Bool) (c x : A) (v : Bool) :

The literal test of the check phase: for a conjunctive matrix, that the cell of x holding v satisfies the clause c; for a disjunctive one, that it violates it.

Equations

DescriptiveComplexity.AltQbf.QGood k cnf c x v = DescriptiveComplexity.AltQbf.QbfLit k c x (DescriptiveComplexity.AltQbf.xorB cnf v)

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.AltQbf.chkVal {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] (νs : Fin k → A → Prop) (x : A) :

The value the tape holds in the cell of x once every sweep has run.

Equations

DescriptiveComplexity.AltQbf.chkVal νs x = DescriptiveComplexity.AltQbf.valAfter νs k x

Instances For

Dependency graph

theorem DescriptiveComplexity.AltQbf.tapeAfter_top_at_cell {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {νs : Fin k → A → Prop} {p : AltV k A} (hp : AltPosn p) (hb : p.1.1 = AltBase.pCell) :

tapeAfter νs k p = symV (chkVal νs (p.2 0)) (p.2 0)

The tape of the check phase reads a real cell as the truth value of its variable.

Dependency graph

A rightward check sweep #

noncomputable def DescriptiveComplexity.AltQbf.chkFlagR {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] (cnf : Bool) (νs : Fin k → A → Prop) (c : A) (p : AltV k A) :

The flag of a rightward check sweep with the head at p: some cell already visited – that is, strictly below p – is good for the clause c.

Equations

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

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.AltQbf.confChkR {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] (cnf : Bool) (νs : Fin k → A → Prop) (c : A) (p : AltV k A) :

Config (AltV k A)

The configuration during a rightward check sweep of the clause c.

Equations

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

Instances For

Dependency graph

theorem DescriptiveComplexity.AltQbf.chkFlagR_bot {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {νs : Fin k → A → Prop} (cnf : Bool) (c : A) :

chkFlagR cnf νs c (posCell qbotA) = false

A rightward sweep starts with an empty flag: nothing lies below the lowest cell.

Dependency graph

theorem DescriptiveComplexity.AltQbf.chkFlagR_succ {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {νs : Fin k → A → Prop} (cnf : Bool) (c : A) {p q : AltV k A} (hsucc : SuccPos tagTupleLe AltPosn p q) (hp : p.1.1 = AltBase.pCell) :

chkFlagR cnf νs c q = true ↔ chkFlagR cnf νs c p = true ∨ QGood k cnf c (p.2 0) (chkVal νs (p.2 0))

Stepping up adds exactly one literal to the flag. Moving the head from p to the position above it brings p's own cell into view and nothing else, because DescriptiveComplexity.SuccPos leaves no room between them.

Dependency graph

theorem DescriptiveComplexity.AltQbf.step_chkR {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {νs : Fin k → A → Prop} {cnf : Bool} {c : A} (hc : QbfCl k c) {p q : AltV k A} (hsucc : SuccPos tagTupleLe AltPosn p q) (hp : p.1.1 = AltBase.pCell) :

(altMachine k A cnf).Step (confChkR cnf νs c p) (confChkR cnf νs c q)

One step of a rightward check sweep. The machine reads the cell it is on, folds that literal into the flag, and moves one place right.

Dependency graph

theorem DescriptiveComplexity.AltQbf.steps_chkR {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {νs : Fin k → A → Prop} {cnf : Bool} {c : A} (hc : QbfCl k c) :

(altMachine k A cnf).StepsIn (bitRank tagTupleLe AltPosn posEnd - bitRank tagTupleLe AltPosn (posCell qbotA)) (confChkR cnf νs c (posCell qbotA)) (confChkR cnf νs c posEnd)

A whole rightward check sweep: from the lowest cell to the right marker, the flag accumulating the literals of c met along the way.

Dependency graph

A leftward check sweep #

noncomputable def DescriptiveComplexity.AltQbf.chkFlagL {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] (cnf : Bool) (νs : Fin k → A → Prop) (c : A) (p : AltV k A) :

The flag of a leftward check sweep with the head at p: some cell already visited – that is, strictly above p – is good for the clause c.

Equations

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

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.AltQbf.confChkL {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] (cnf : Bool) (νs : Fin k → A → Prop) (c : A) (p : AltV k A) :

Config (AltV k A)

The configuration during a leftward check sweep of the clause c.

Equations

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

Instances For

Dependency graph

theorem DescriptiveComplexity.AltQbf.chkFlagL_top {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {νs : Fin k → A → Prop} (cnf : Bool) (c : A) :

chkFlagL cnf νs c (posCell qtopA) = false

A leftward sweep starts with an empty flag: nothing lies above the highest cell.

Dependency graph

theorem DescriptiveComplexity.AltQbf.chkFlagL_succ {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {νs : Fin k → A → Prop} (cnf : Bool) (c : A) {p q : AltV k A} (hsucc : SuccPos tagTupleLe AltPosn p q) (hq : q.1.1 = AltBase.pCell) :

chkFlagL cnf νs c p = true ↔ chkFlagL cnf νs c q = true ∨ QGood k cnf c (q.2 0) (chkVal νs (q.2 0))

Stepping down adds exactly one literal to the flag.

Dependency graph

theorem DescriptiveComplexity.AltQbf.step_chkL {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {νs : Fin k → A → Prop} {cnf : Bool} {c : A} (hc : QbfCl k c) {p q : AltV k A} (hsucc : SuccPos tagTupleLe AltPosn p q) (hq : q.1.1 = AltBase.pCell) :

(altMachine k A cnf).Step (confChkL cnf νs c q) (confChkL cnf νs c p)

One step of a leftward check sweep.

Dependency graph

theorem DescriptiveComplexity.AltQbf.steps_chkL {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {νs : Fin k → A → Prop} {cnf : Bool} {c : A} (hc : QbfCl k c) :

(altMachine k A cnf).StepsIn (bitRank tagTupleLe AltPosn (posCell qtopA) - bitRank tagTupleLe AltPosn posStart) (confChkL cnf νs c (posCell qtopA)) (confChkL cnf νs c posStart)

A whole leftward check sweep: from the highest cell down to the left marker.

Dependency graph

The turns #

theorem DescriptiveComplexity.AltQbf.step_turnNextR {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {νs : Fin k → A → Prop} {cnf : Bool} {c c' : A} (hnext : QbfNextCl k c c') (hflag : chkFlagR cnf νs c posEnd = true) :

(altMachine k A cnf).Step (confChkR cnf νs c posEnd) (confChkL cnf νs c' (posCell qtopA))

The turn at the right marker, when another clause follows.

Dependency graph

theorem DescriptiveComplexity.AltQbf.step_turnAccR {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {νs : Fin k → A → Prop} {cnf : Bool} {c : A} (hc : QbfCl k c) (hmax : cnf = true → QbfMaxCl k c) (hflag : chkFlagR cnf νs c posEnd = cnf) :

(altMachine k A cnf).Step (confChkR cnf νs c posEnd) { state := stAcc, head := posCell qtopA, tape := tapeAfter νs k }

The turn at the right marker, when the clause settles the run.

Dependency graph

theorem DescriptiveComplexity.AltQbf.step_turnNextL {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {νs : Fin k → A → Prop} {cnf : Bool} {c c' : A} (hnext : QbfNextCl k c c') (hflag : chkFlagL cnf νs c posStart = true) :

(altMachine k A cnf).Step (confChkL cnf νs c posStart) (confChkR cnf νs c' (posCell qbotA))

The turn at the left marker, when another clause follows.

Dependency graph

theorem DescriptiveComplexity.AltQbf.step_turnAccL {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {νs : Fin k → A → Prop} {cnf : Bool} {c : A} (hc : QbfCl k c) (hmax : cnf = true → QbfMaxCl k c) (hflag : chkFlagL cnf νs c posStart = cnf) :

(altMachine k A cnf).Step (confChkL cnf νs c posStart) { state := stAcc, head := posCell qbotA, tape := tapeAfter νs k }

The turn at the left marker, when the clause settles the run.

Dependency graph

One clause, checked end to end #

theorem DescriptiveComplexity.AltQbf.chkFlagR_posEnd {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {νs : Fin k → A → Prop} (cnf : Bool) (c : A) :

chkFlagR cnf νs c posEnd = true ↔ ∃ (y : A), QGood k cnf c y (chkVal νs y)

At the far marker the flag has seen every cell.

Dependency graph

theorem DescriptiveComplexity.AltQbf.chkFlagL_posStart {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {νs : Fin k → A → Prop} (cnf : Bool) (c : A) :

chkFlagL cnf νs c posStart = true ↔ ∃ (y : A), QGood k cnf c y (chkVal νs y)

At the far marker the flag has seen every cell.

Dependency graph

theorem DescriptiveComplexity.AltQbf.bitRank_posStart {k : ℕ} {A : Type} [LinearOrder A] [Finite A] [Nonempty A] :

bitRank tagTupleLe AltPosn posStart = 0

The left marker has rank 0.

Dependency graph

theorem DescriptiveComplexity.AltQbf.bitRank_posEnd_eq {k : ℕ} {A : Type} [LinearOrder A] [Finite A] [Nonempty A] :

bitRank tagTupleLe AltPosn posEnd = bitRank tagTupleLe AltPosn (posCell qtopA) + 1

The right marker sits one step above the last cell.

Dependency graph

theorem DescriptiveComplexity.AltQbf.bitRank_posCell_qbotA {k : ℕ} {A : Type} [LinearOrder A] [Finite A] [Nonempty A] :

bitRank tagTupleLe AltPosn (posCell qbotA) = 1

The first cell has rank 1.

Dependency graph

theorem DescriptiveComplexity.AltQbf.steps_clauseR {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {νs : Fin k → A → Prop} {cnf : Bool} {c c' : A} (hc : QbfCl k c) (hnext : QbfNextCl k c c') (hgood : ∃ (y : A), QGood k cnf c y (chkVal νs y)) :

∃ n ≤ bitRank tagTupleLe AltPosn posEnd, (altMachine k A cnf).StepsIn n (confChkR cnf νs c (posCell qbotA)) (confChkL cnf νs c' (posCell qtopA))

Checking c rightwards and moving on to the next clause.

Dependency graph

theorem DescriptiveComplexity.AltQbf.steps_clauseL {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {νs : Fin k → A → Prop} {cnf : Bool} {c c' : A} (hc : QbfCl k c) (hnext : QbfNextCl k c c') (hgood : ∃ (y : A), QGood k cnf c y (chkVal νs y)) :

∃ n ≤ bitRank tagTupleLe AltPosn posEnd, (altMachine k A cnf).StepsIn n (confChkL cnf νs c (posCell qtopA)) (confChkR cnf νs c' (posCell qbotA))

Checking c leftwards and moving on to the next clause.

Dependency graph

theorem DescriptiveComplexity.AltQbf.steps_clauseAccR {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {νs : Fin k → A → Prop} {cnf : Bool} {c : A} (hc : QbfCl k c) (hmax : cnf = true → QbfMaxCl k c) (hflag : chkFlagR cnf νs c posEnd = cnf) :

∃ n ≤ bitRank tagTupleLe AltPosn posEnd, ∃ (cfin : Config (AltV k A)), (altMachine k A cnf).StepsIn n (confChkR cnf νs c (posCell qbotA)) cfin ∧ AltAccSt cfin.state

Checking c rightwards and accepting.

Dependency graph

theorem DescriptiveComplexity.AltQbf.steps_clauseAccL {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {νs : Fin k → A → Prop} {cnf : Bool} {c : A} (hc : QbfCl k c) (hmax : cnf = true → QbfMaxCl k c) (hflag : chkFlagL cnf νs c posStart = cnf) :

∃ n ≤ bitRank tagTupleLe AltPosn posEnd, ∃ (cfin : Config (AltV k A)), (altMachine k A cnf).StepsIn n (confChkL cnf νs c (posCell qtopA)) cfin ∧ AltAccSt cfin.state

Checking c leftwards and accepting.

Dependency graph

Walking the clauses #

theorem DescriptiveComplexity.AltQbf.exists_qNextCl {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] {c : A} (hc : QbfCl k c) (hnmax : ¬QbfMaxCl k c) :

∃ (c' : A), QbfNextCl k c c'

Every clause but the last has a next one.

Dependency graph

theorem DescriptiveComplexity.AltQbf.ncard_qclauses_next {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] {c c' : A} (hnext : QbfNextCl k c c') :

{e : A | QbfCl k e ∧ c ≤ e}.ncard = {e : A | QbfCl k e ∧ c' ≤ e}.ncard + 1

Passing to the next clause removes exactly one clause from those still to be checked.

Dependency graph

theorem DescriptiveComplexity.AltQbf.accepts_from_chk_cnf {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {νs : Fin k → A → Prop} {cnf : Bool} (hcnf : cnf = true) (hsat : ∀ (e : A), QbfCl k e → ∃ (y : A), QGood k cnf e y (chkVal νs y)) (c : A) :

QbfCl k c → (∃ (n : ℕ) (cfin : Config (AltV k A)), n ≤ {e : A | QbfCl k e ∧ c ≤ e}.ncard * bitRank tagTupleLe AltPosn posEnd ∧ (altMachine k A cnf).StepsIn n (confChkL cnf νs c (posCell qtopA)) cfin ∧ AltAccSt cfin.state) ∧ ∃ (n : ℕ) (cfin : Config (AltV k A)), n ≤ {e : A | QbfCl k e ∧ c ≤ e}.ncard * bitRank tagTupleLe AltPosn posEnd ∧ (altMachine k A cnf).StepsIn n (confChkR cnf νs c (posCell qbotA)) cfin ∧ AltAccSt cfin.state

A conjunctive matrix: the machine checks every remaining clause and accepts, in at most one sweep's worth of steps per clause.

Dependency graph

theorem DescriptiveComplexity.AltQbf.accepts_from_chk_dnf {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {νs : Fin k → A → Prop} {cnf : Bool} (hcnf : cnf = false) {c₀ : A} (hc₀ : QbfCl k c₀) (hgood : ∀ (y : A), ¬QGood k cnf c₀ y (chkVal νs y)) (c : A) :

QbfCl k c → c ≤ c₀ → (∃ (n : ℕ) (cfin : Config (AltV k A)), n ≤ {e : A | QbfCl k e ∧ c ≤ e}.ncard * bitRank tagTupleLe AltPosn posEnd ∧ (altMachine k A cnf).StepsIn n (confChkL cnf νs c (posCell qtopA)) cfin ∧ AltAccSt cfin.state) ∧ ∃ (n : ℕ) (cfin : Config (AltV k A)), n ≤ {e : A | QbfCl k e ∧ c ≤ e}.ncard * bitRank tagTupleLe AltPosn posEnd ∧ (altMachine k A cnf).StepsIn n (confChkR cnf νs c (posCell qbotA)) cfin ∧ AltAccSt cfin.state

A disjunctive matrix: the machine walks the terms until one has no violated literal, and accepts there. The flag is clear at such a term, which is exactly what the accepting turn fires at when cnf is false.

Dependency graph

A deterministic run accepts at either polarity #

The check phase is deterministic, so its run is a legitimate move for the universal player as much as for the existential one: “every successor accepts” and “some successor accepts” say the same thing when there is exactly one.

theorem DescriptiveComplexity.AltQbf.altAcc_of_stepsIn_det {k : ℕ} {A : Type} {M : ATMData (AltV k A)} {start : Bool} {P : Config (AltV k A) → Prop} (hclosed : ∀ (e e' : Config (AltV k A)), P e → M.Step e e' → P e') (hdet : ∀ (e e' e'' : Config (AltV k A)), P e → M.Step e e' → M.Step e e'' → e' = e'') (m n : ℕ) (c d : Config (AltV k A)) :

m ≤ n → P c → M.StepsIn m c d → M.Acc d.state → M.AltAcc start n c

A deterministic run accepts whatever the polarity of its block. The existential half is DescriptiveComplexity.ATMData.altAcc_of_steps; this is the version that also serves a universal block, and could be hoisted to DescriptiveComplexity.MachinesAltPlay.

Dependency graph

The check phase is deterministic #

def DescriptiveComplexity.AltQbf.InCheck {k : ℕ} {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (c : Config (AltV k A)) :

Being in the check phase: the state is a checking state or the accepting one.

Equations

DescriptiveComplexity.AltQbf.InCheck c = ((∃ (f : Bool) (d : Bool) (cl : A), c.state = DescriptiveComplexity.AltQbf.stChk f d cl) ∨ c.state = DescriptiveComplexity.AltQbf.stAcc)

Instances For

Dependency graph

theorem DescriptiveComplexity.AltQbf.inCheck_closed {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {cnf : Bool} (c c' : Config (AltV k A)) (hP : InCheck c) (hstep : (altMachine k A cnf).Step c c') :

The check phase never returns to a sweep.

Dependency graph

theorem DescriptiveComplexity.AltQbf.inCheck_det {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {cnf : Bool} (c c' c'' : Config (AltV k A)) (hP : InCheck c) (h₁ : (altMachine k A cnf).Step c c') (h₂ : (altMachine k A cnf).Step c c'') :

c' = c''

The check phase is deterministic: none of its configurations is a guessing choice.

Dependency graph

theorem DescriptiveComplexity.AltQbf.altAcc_of_check {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {cnf start : Bool} {m n : ℕ} {c d : Config (AltV k A)} (hmn : m ≤ n) (hP : InCheck c) (hrun : (altMachine k A cnf).StepsIn m c d) (hacc : AltAccSt d.state) :

(altMachine k A cnf).AltAcc start n c

The check phase accepts, at either polarity of its block, as soon as a run through it reaches an accepting state.

Dependency graph

The run is short enough #

The budget of DescriptiveComplexity.ATMData.AltAccepts counts the positions of the tape, of which the fillers alone supply 8(k+1)n². A sweep, by contrast, costs about as many steps as the instance has elements: only the left marker and the cells lie below the right marker.

theorem DescriptiveComplexity.AltQbf.base_le_pEnd {t : AltBase} (h : altBaseIdx t ≤ altBaseIdx AltBase.pEnd) :

t = AltBase.pStart ∨ t = AltBase.pCell ∨ t = AltBase.pEnd

Only the three bracketing base tags are at or below the right marker's.

Dependency graph

theorem DescriptiveComplexity.AltQbf.bitRank_posEnd_le {k : ℕ} {A : Type} [LinearOrder A] [Finite A] [Nonempty A] :

bitRank tagTupleLe AltPosn posEnd ≤ Nat.card A + 1

A sweep is short. Proved by injecting the positions below the right marker into Option A rather than by counting.

Dependency graph

theorem DescriptiveComplexity.AltQbf.sweepLen_le {k : ℕ} {A : Type} [LinearOrder A] [Finite A] [Nonempty A] :

sweepLen k A ≤ 2 * (Nat.card A + 1)

A sweep costs about twice the size of the instance: down the tape and back.

Dependency graph