The prefix phases play the alternating prefix #

The first of the two correctness halves of the graph game: from a phase pre s tx ty j pol, the game plays exactly j more rounds, alternating from pol, and is then decided by the kernel of the question s (DescriptiveComplexity.ExpExpansion.wins_pre). The proof is a plain induction on j against DescriptiveComplexity.altBlockQuant's own recursion – which is what carrying the polarity in the phase buys.

Two things make the base and the step line up.

A leaf is existential and moveless. movesFrom returns [] at j = 0 and Ph.IsUniv is false there, so the position wins exactly when it wins outright, i.e., exactly when the kernel holds. A question the player cannot prove therefore loses, which is the whole point of asking it as a move.
Filling a round is changing one round. The move out of pre … (j+1) … freezes every round but n - (j + 1), and DescriptiveComplexity.ExpExpansion.fillRounds_succ is the identity between filling j + 1 rounds of the state left and filling j rounds of the state entered.

`Fin.cons` at an index known by its value #

source

theorem DescriptiveComplexity.cons_of_val_zero {α : Type} {k : ℕ} (v : α) (τs : Fin k → α) (j : Fin (k + 1)) (h : ↑j = 0) :

Fin.cons v τs j = v

Dependency graph

source

theorem DescriptiveComplexity.cons_of_val_succ {α : Type} {k : ℕ} (v : α) (τs : Fin k → α) (j : Fin (k + 1)) (m : Fin k) (h : ↑j = ↑m + 1) :

Fin.cons v τs j = τs m

Dependency graph

Filling the last rounds #

source

noncomputable def DescriptiveComplexity.ExpExpansion.fillRounds {L : FirstOrder.Language} {X : ExpExpansion L} {n : ℕ} {A : Type} {k : ℕ} (hk : k ≤ n) (ρs : Fin n → X.pointBlock.Assignment A) (τs : Fin k → X.pointBlock.Assignment A) :

Fin n → X.pointBlock.Assignment A

The rounds ρs with the last k overwritten by τs, in order.

Equations

DescriptiveComplexity.ExpExpansion.fillRounds hk ρs τs i = if x : n - k ≤ ↑i then τs ⟨↑i - (n - k), ⋯⟩ else ρs i

Instances For

Dependency graph

source

theorem DescriptiveComplexity.ExpExpansion.fillRounds_zero {L : FirstOrder.Language} {X : ExpExpansion L} {n : ℕ} {A : Type} (hk : 0 ≤ n) (ρs : Fin n → X.pointBlock.Assignment A) (τs : Fin 0 → X.pointBlock.Assignment A) :

fillRounds hk ρs τs = ρs

Dependency graph

source

theorem DescriptiveComplexity.ExpExpansion.fillRounds_succ {L : FirstOrder.Language} {X : ExpExpansion L} {n : ℕ} {A : Type} (k : ℕ) (hk : k + 1 ≤ n) (ρs σs : Fin n → X.pointBlock.Assignment A) (τs : Fin k → X.pointBlock.Assignment A) (r : Fin n) (hr : ↑r = n - (k + 1)) (hag : ∀ (i : Fin n), i ≠ r → ρs i = σs i) :

fillRounds hk ρs (Fin.cons (σs r) τs) = fillRounds ⋯ σs τs

Filling one more round is filling one fewer round of the state the move enters, provided that state differs from the one it leaves only at the round being filled.

Dependency graph

The moves out of a prefix phase #

source

theorem DescriptiveComplexity.ExpExpansion.movesFrom_pre_zero {T : Type} [Finite T] {d n Dm : ℕ} {hn : n = 2 * d + Dm} {D : Sub → T → T → ℕ} {hD : ∀ (s : Sub) (tx ty : T), D s tx ty ≤ Dm} (hk : 0 < Dm + 1) (s : Sub) (tx ty : T) (pol : Bool) :

movesFrom hn D hD (Ph.pre s tx ty ⟨0, hk⟩ pol) = []

Dependency graph

source

theorem DescriptiveComplexity.ExpExpansion.movesFrom_pre_succ {T : Type} [Finite T] {d n Dm : ℕ} {hn : n = 2 * d + Dm} {D : Sub → T → T → ℕ} {hD : ∀ (s : Sub) (tx ty : T), D s tx ty ≤ Dm} (k : ℕ) (hk : k + 1 < Dm + 1) (r : Fin n) (hr : ↑r = n - (k + 1)) (s : Sub) (tx ty : T) (pol : Bool) :

movesFrom hn D hD (Ph.pre s tx ty ⟨k + 1, hk⟩ pol) = [{ tgt := Ph.pre s tx ty ⟨k, ⋯⟩ !pol, keep := keepOff n fun (i : Fin n) => decide (i = r), guard := [] }]

Dependency graph