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.AltQbf.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.AltQbf.altTail_iff_altQuant), by an induction that pushes one block from the tail into the prefix at a time. The gluing map DescriptiveComplexity.AltQbf.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 ν

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✝¹

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

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.