The quantifier prefix, read from the middle

DescriptiveComplexity.altQuant quantifies the k block assignments from the outside in, building the tuple with Fin.cons: the assignment of index 0 is the outermost, and the type shrinks as the recursion goes. That is the right shape for a definition and the wrong one for a run, which fixes the blocks in place and rewrites them one at a time with Function.update.

DescriptiveComplexity.AltTail is the second shape: AltTail P r m νs pol quantifies the r blocks from m up, leaving the blocks below m at whatever νs says. The two agree (DescriptiveComplexity.altTail_iff_altQuant), by an induction that pushes one block from the tail into the prefix at a time. The gluing map DescriptiveComplexity.glueTail is what translates between them, and the whole content of the bridge is that pushing a block past it is Function.update.

Quantification from the middle of the prefix

def DescriptiveComplexity.AltQbf.polQuant {A : Type} (pol : Bool) (Q : (A → Prop) → Prop) : Prop

One quantifier at the polarity pol.

Equations

• DescriptiveComplexity.AltQbf.polQuant true Q = ∃ (ν : A → Prop), Q ν
• DescriptiveComplexity.AltQbf.polQuant false Q = ∀ (ν : A → Prop), Q ν

theorem DescriptiveComplexity.AltQbf.polQuant_congr {A : Type} {pol : Bool} {Q Q' : (A → Prop) → Prop} (h : ∀ (ν : A → Prop), Q ν ↔ Q' ν) : polQuant pol Q ↔ polQuant pol Q'

def DescriptiveComplexity.AltQbf.AltTail {k : ℕ} {A : Type} (P : (Fin k → A → Prop) → Prop) : ℕ → ℕ → (Fin k → A → Prop) → Bool → Prop

Quantifying the last r blocks, the ones below m already fixed by νs. Each block is written in place, which is the shape a run of the machine produces: round m replaces the m-th assignment and leaves the others alone.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.AltQbf.AltTail P 0 x✝² x✝¹ x✝ = P x✝¹

theorem DescriptiveComplexity.AltQbf.altTail_succ {k : ℕ} {A : Type} (P : (Fin k → A → Prop) → Prop) {r m : ℕ} (h : m < k) (νs : Fin k → A → Prop) (pol : Bool) : AltTail P (r + 1) m νs pol = polQuant pol fun (ν : A → Prop) => AltTail P r (m + 1) (Function.update νs ⟨m, h⟩ ν) !pol

Gluing a tail onto a prefix

def DescriptiveComplexity.AltQbf.glueTail {k : ℕ} {A : Type} (m r : ℕ) (νs : Fin k → A → Prop) (σ : Fin r → A → Prop) (i : Fin k) : A → Prop

The tuple that follows νs below m and reads the r blocks from m up off σ.

Equations

• DescriptiveComplexity.AltQbf.glueTail m r νs σ i = if ↑i < m then νs i else if h : ↑i - m < r then σ ⟨↑i - m, h⟩ else νs i

theorem DescriptiveComplexity.AltQbf.glueTail_zero {k : ℕ} {A : Type} (m : ℕ) (νs : Fin k → A → Prop) (σ : Fin 0 → A → Prop) : glueTail m 0 νs σ = νs

Gluing nothing leaves the prefix alone.

theorem DescriptiveComplexity.AltQbf.glueTail_cons {k : ℕ} {A : Type} {m r : ℕ} (h : m < k) (νs : Fin k → A → Prop) (ν : A → Prop) (σ : Fin r → A → Prop) : glueTail m (r + 1) νs (Fin.cons ν σ) = glueTail (m + 1) r (Function.update νs ⟨m, h⟩ ν) σ

Pushing one block from the tail into the prefix is an update. This is the whole content of the bridge between the two shapes of the prefix.

The two shapes agree

theorem DescriptiveComplexity.AltQbf.altTail_iff_altQuant {k : ℕ} {A : Type} (P : (Fin k → A → Prop) → Prop) (r m : ℕ) : m + r ≤ k → ∀ (νs : Fin k → A → Prop) (pol : Bool), AltTail P r m νs pol ↔ altQuant A r (fun (σ : Fin r → A → Prop) => P (glueTail m r νs σ)) pol

Quantifying from the middle is quantifying from the outside, once the blocks already fixed are glued back on.

theorem DescriptiveComplexity.AltQbf.altTail_zero_iff_altQuant {k : ℕ} {A : Type} (P : (Fin k → A → Prop) → Prop) (νs : Fin k → A → Prop) (pol : Bool) : AltTail P k 0 νs pol ↔ altQuant A k P pol

The whole prefix: quantifying every block in place is the alternating quantification of DescriptiveComplexity.QbfProblem.