Transferring an alternating prefix from valuations to block assignments

The hardness proof for DescriptiveComplexity.QBF reduces a Σₖ-definable problem to a quantified Boolean formula whose propositional variables encode the relation variables of the k second-order blocks. Both sides are alternating quantifications – DescriptiveComplexity.altQuant over truth assignments of the QBF instance, DescriptiveComplexity.altAssign over the components of a merged block assignment – so what is needed is a way to move between them block by block.

DescriptiveComplexity.altQuant_iff_altAssign does exactly that. It is parameterized by a reading DescriptiveComplexity.BlockRead, which says how the relation assigned to each merged relation variable is read off a truth assignment, and it needs only two things: that the quantified predicates correspond under the reading, and that the reading is surjective at every block (DescriptiveComplexity.ReadSurj) – the propositional variables of a block are free enough to realize any relation.

Which block a merged relation variable belongs to

Reading block assignments off a truth assignment

@[reducible, inline]

abbrev DescriptiveComplexity.BlockRead (A A' : Type) (Bs : List SOBlock) : Type

A reading of relations off a truth assignment of the propositional variables: rd i ν is the relation that the valuation ν assigns to the merged relation variable i.

Equations

• DescriptiveComplexity.BlockRead A A' Bs = ((i : (DescriptiveComplexity.mergeBlocks Bs).ι) → (A' → Prop) → (Fin ((DescriptiveComplexity.mergeBlocks Bs).arity i) → A) → Prop)

def DescriptiveComplexity.readAll {A A' : Type} (Bs : List SOBlock) : BlockRead A A' Bs → (Fin Bs.length → A' → Prop) → (mergeBlocks Bs).Assignment A

The merged assignment read off a tuple of truth assignments: each relation variable is read from the truth assignment of the block it belongs to.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.readAll [] x_3 x_4 = DescriptiveComplexity.nilAssign A

theorem DescriptiveComplexity.readAll_cons {A A' : Type} (B : SOBlock) (Bs : List SOBlock) (rd : BlockRead A A' (B :: Bs)) (ν : A' → Prop) (νs : Fin Bs.length → A' → Prop) : readAll (B :: Bs) rd (Fin.cons ν νs) = consAssign (fun (i : B.ι) (a : Fin (B.arity i) → A) => rd (Sum.inl i) ν a) (readAll Bs (fun (i : (mergeBlocks Bs).ι) => rd (Sum.inr i)) νs)

def DescriptiveComplexity.ReadSurj {A A' : Type} (Bs : List SOBlock) : BlockRead A A' Bs → Prop

The reading is surjective at every block: the propositional variables of a block can realize an arbitrary relation.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.ReadSurj [] x_2 = True

Reading an enlarged prefix

When the innermost block has been enlarged by a block Gt of auxiliary variables (DescriptiveComplexity.consLast), a reading built from DescriptiveComplexity.splitIdx decomposes along DescriptiveComplexity.combineLast: the original relation variables are read from the truth assignment of their own block, the auxiliary ones from the innermost. The index map DescriptiveComplexity.markC says which, and is stated at Fin (consLast Gt B Bs).length – the type readAll uses – so that the induction needs no transport along DescriptiveComplexity.consLast_length.

def DescriptiveComplexity.markC (Gt B : SOBlock) (Bs : List SOBlock) : (mergeBlocks (B :: Bs)).ι ⊕ Gt.ι → Fin (consLast Gt B Bs).length

Which quantifier block of the enlarged prefix a variable belongs to: its own block for a relation variable of the original prefix, the innermost one for a variable of the extra block.

Equations

• DescriptiveComplexity.markC Gt x✝ [] (Sum.inl (Sum.inl val)) = 0
• DescriptiveComplexity.markC Gt x✝ [] (Sum.inl (Sum.inr e)) = Empty.elim e
• DescriptiveComplexity.markC Gt x✝ [] (Sum.inr val) = 0
• DescriptiveComplexity.markC Gt x✝ (head :: tail) (Sum.inl (Sum.inl val)) = 0
• DescriptiveComplexity.markC Gt x✝ (B' :: Bs) (Sum.inl (Sum.inr y)) = (DescriptiveComplexity.markC Gt B' Bs (Sum.inl y)).succ
• DescriptiveComplexity.markC Gt x✝ (B' :: Bs) (Sum.inr j) = (DescriptiveComplexity.markC Gt B' Bs (Sum.inr j)).succ

theorem DescriptiveComplexity.readAll_consLast {A A' : Type} (Gt : SOBlock) {D : ℕ} (pdf : {m : ℕ} → (Fin m → A) → Fin D → A) (B : SOBlock) (Bs : List SOBlock) (el : (mergeBlocks (B :: Bs)).ι ⊕ Gt.ι → (Fin D → A) → A') (νs : Fin (consLast Gt B Bs).length → A' → Prop) : readAll (consLast Gt B Bs) (fun (i : (mergeBlocks (consLast Gt B Bs)).ι) (ν : A' → Prop) (a : Fin ((mergeBlocks (consLast Gt B Bs)).arity i) → A) => ν (el (splitIdx Gt B Bs i) (pdf a))) νs = combineLast Gt B Bs (fun (i' : (mergeBlocks (B :: Bs)).ι) (a : Fin ((mergeBlocks (B :: Bs)).arity i') → A) => νs (markC Gt B Bs (Sum.inl i')) (el (Sum.inl i') (pdf a))) fun (j : Gt.ι) (x : Fin (Gt.arity j) → A) => νs (markC Gt B Bs (Sum.inr j)) (el (Sum.inr j) (pdf x))

The reading of an enlarged prefix splits: reading each variable from the truth assignment of the block markC assigns it is the same as assembling the original assignment and the auxiliary one with DescriptiveComplexity.combineLast.

theorem DescriptiveComplexity.readSurj_consLast {A A' : Type} (Gt : SOBlock) {D : ℕ} (pdf : {m : ℕ} → (Fin m → A) → Fin D → A) (B : SOBlock) (Bs : List SOBlock) (el : (mergeBlocks (B :: Bs)).ι ⊕ Gt.ι → (Fin D → A) → A') : (∀ (z z' : (mergeBlocks (B :: Bs)).ι ⊕ Gt.ι) (u u' : Fin D → A), el z u = el z' u' → z = z' ∧ u = u') → (∀ (i : (mergeBlocks (consLast Gt B Bs)).ι) (a a' : Fin ((mergeBlocks (consLast Gt B Bs)).arity i) → A), pdf a = pdf a' → a = a') → ReadSurj (consLast Gt B Bs) fun (i : (mergeBlocks (consLast Gt B Bs)).ι) (ν : A' → Prop) (a : Fin ((mergeBlocks (consLast Gt B Bs)).arity i) → A) => ν (el (splitIdx Gt B Bs i) (pdf a))

A reading built from an injective tagging is surjective at every block: a truth assignment realizing a prescribed relation is obtained by reading the tag back off each propositional variable.

The transfer

theorem DescriptiveComplexity.altQuant_iff_altAssign {A A' : Type} (Bs : List SOBlock) (rd : BlockRead A A' Bs) : ReadSurj Bs rd → ∀ (F : (Fin Bs.length → A' → Prop) → Prop) (G : (mergeBlocks Bs).Assignment A → Prop), (∀ (νs : Fin Bs.length → A' → Prop), F νs ↔ G (readAll Bs rd νs)) → ∀ (pol : Bool), altQuant A' Bs.length F pol ↔ altAssign A Bs G pol

Transfer of an alternating prefix: alternating quantification over truth assignments of the propositional variables is alternating quantification over the components of the merged block assignment they encode.