Playing a whole quantifier block at once

DescriptiveComplexity.QsatWins plays one variable at a time, in the order the instance prescribes: that is what makes it the honest reading of a quantifier prefix, and what the membership walk of DescriptiveComplexity.Problems.Qsat.Membership follows step by step. Every hardness proof needs the opposite reading, the one the textbooks write: the prefix is a sequence of blocks of like polarity, and a block is a single quantifier over an assignment of the whole block.

This file proves the two peeling lemmas that turn one reading into the other, DescriptiveComplexity.qsatWins_block_ex and DescriptiveComplexity.qsatWins_block_all: if B is a set of unplayed variables of the same polarity that comes first among the unplayed ones (DescriptiveComplexity.QBlock), then winning the position (D, τ) is winning (D ∪ B, τ) for some (resp. every) assignment of B. Iterating them along the blocks of a constructed instance is how a reduction into QSAT states its correctness.

Both go by induction on the size of B: the next variable to play lies in B as soon as B is nonempty, and the induction hypothesis applies to B minus that variable. The bookkeeping is done with Prop-valued updates (DescriptiveComplexity.qSet) rather than the Bool-valued ones of the game rules, so that a block assignment ν : A → Prop never has to be converted; the two are related by DescriptiveComplexity.qsatWins_ex_iff' and DescriptiveComplexity.qsatWins_all_iff'.

Propositional updates

def DescriptiveComplexity.qSet {A : Type} (τ : A → Prop) (x : A) (P : Prop) : A → Prop

Giving the variable x the value P, a proposition rather than a Boolean: the shape a block assignment produces.

Equations

• DescriptiveComplexity.qSet τ x P y = (y = x ∧ P ∨ y ≠ x ∧ τ y)

@[simp]

theorem DescriptiveComplexity.qSet_self {A : Type} (τ : A → Prop) (x : A) (P : Prop) : qSet τ x P x ↔ P

theorem DescriptiveComplexity.qSet_ne {A : Type} (τ : A → Prop) {x y : A} (P : Prop) (h : y ≠ x) : qSet τ x P y ↔ τ y

theorem DescriptiveComplexity.qSet_congr {A : Type} (τ : A → Prop) (x : A) {P Q : Prop} (h : P ↔ Q) : qSet τ x P = qSet τ x Q

theorem DescriptiveComplexity.qSet_self_eq {A : Type} (τ : A → Prop) (x : A) : qSet τ x (τ x) = τ

The one-variable rules, propositionally

theorem DescriptiveComplexity.qsatWins_ex_iff' {A : Type} [FirstOrder.Language.qsat.Structure A] (hwf : QsatWf A) {D τ : A → Prop} {x : A} (hx : QLeast D x) (hq : ¬IsQAll x) : QsatWins D τ ↔ ∃ (P : Prop), QsatWins (qAdd D x) (qSet τ x P)

The existential rule, with the played value a proposition.

theorem DescriptiveComplexity.qsatWins_all_iff' {A : Type} [FirstOrder.Language.qsat.Structure A] (hwf : QsatWf A) {D τ : A → Prop} {x : A} (hx : QLeast D x) (hq : IsQAll x) : QsatWins D τ ↔ ∀ (P : Prop), QsatWins (qAdd D x) (qSet τ x P)

The universal rule, with the played value a proposition.

Blocks

def DescriptiveComplexity.qUnion {A : Type} (D B : A → Prop) : A → Prop

The union of the played variables and a block.

Equations

• DescriptiveComplexity.qUnion D B y = (D y ∨ B y)

def DescriptiveComplexity.qOver {A : Type} (B τ ν : A → Prop) : A → Prop

The valuation that reads ν on the block B and τ outside it.

Equations

• DescriptiveComplexity.qOver B τ ν y = (B y ∧ ν y ∨ ¬B y ∧ τ y)

structure DescriptiveComplexity.QBlock {A : Type} [FirstOrder.Language.qsat.Structure A] (D B : A → Prop) : Prop

B is the next block of the position (D, ·): a set of unplayed variables that comes first among the unplayed ones. Together with a uniform polarity this is what lets the whole of B be played by one quantifier.

• isVar (x : A) : B x → IsQVar x

  A block holds variables.

• unplayed (x : A) : B x → ¬D x

  A block holds unplayed variables.

• first (x y : A) : B x → IsQVar y → ¬D y → ¬B y → QPrec x y

  A block comes first among the unplayed variables.

theorem DescriptiveComplexity.QBlock.mem_of_qLeast {A : Type} [FirstOrder.Language.qsat.Structure A] {D B : A → Prop} (hB : QBlock D B) {x z : A} (hx : QLeast D x) (hz : B z) : B x

The next variable to play lies in the block, as soon as the block is nonempty.

theorem DescriptiveComplexity.qOver_qSet {A : Type} {B : A → Prop} {x : A} (hBx : B x) (τ ν : A → Prop) (P : Prop) : qOver (qRem B x) (qSet τ x P) ν = qOver B τ (qSet ν x P)

theorem DescriptiveComplexity.qUnion_qAdd_qRem {A : Type} {D B : A → Prop} {x : A} (hBx : B x) : qUnion (qAdd D x) (qRem B x) = qUnion D B

theorem DescriptiveComplexity.qBlock_qRem {A : Type} [FirstOrder.Language.qsat.Structure A] {D B : A → Prop} {x : A} (hB : QBlock D B) : QBlock (qAdd D x) (qRem B x)

theorem DescriptiveComplexity.qOver_of_empty {A : Type} {B τ ν : A → Prop} (hB : ∀ (y : A), ¬B y) : qOver B τ ν = τ

theorem DescriptiveComplexity.qUnion_of_empty {A : Type} {D B : A → Prop} (hB : ∀ (y : A), ¬B y) : qUnion D B = D

theorem DescriptiveComplexity.qsatWins_block_ex {A : Type} [FirstOrder.Language.qsat.Structure A] [Finite A] (hwf : QsatWf A) {D B τ : A → Prop} (hdc : QDownClosed D) (hB : QBlock D B) (hpol : ∀ (x : A), B x → ¬IsQAll x) : QsatWins D τ ↔ ∃ (ν : A → Prop), QsatWins (qUnion D B) (qOver B τ ν)

An existential block is played by one quantifier: if B is the next block of the position (D, τ) and all its variables are existential, winning (D, τ) is winning (D ∪ B, τ) under some assignment of B.

theorem DescriptiveComplexity.qsatWins_block_all {A : Type} [FirstOrder.Language.qsat.Structure A] [Finite A] (hwf : QsatWf A) {D B τ : A → Prop} (hdc : QDownClosed D) (hB : QBlock D B) (hpol : ∀ (x : A), B x → IsQAll x) : QsatWins D τ ↔ ∀ (ν : A → Prop), QsatWins (qUnion D B) (qOver B τ ν)

A universal block is played by one quantifier: dually, under every assignment of B.