Reading a win back: the phases of a question

The backward simulation, for the phases that settle a question. Where the forward direction builds a play, this one reads one back, so the two players change roles: an existential phase now has to be case-analyzed (the play chose one successor, and we must see what that choice proves) and a universal one may be instantiated at the successors we care about.

Everything it needs was built as an equivalence for exactly this reason – DescriptiveComplexity.ctrlCfg_cases reads a control step back, and the _det-style rule lemmas read a walk step back.

The three shapes of a phase

• existential (claim, conc, seek, pre at an existential variable): DescriptiveComplexity.exists_altWin_succ_of_ex gives the successor the play chose, and the step analysis says what it can be;
• universal (check, pre at a universal variable): DescriptiveComplexity.altWin_succ_of_univ instantiates the play at any successor we can build – which is what the forward direction's step lemmas supply;
• a walk (seek): neither, but an induction on DescriptiveComplexity.ATMData.AltWin itself, the invariant being the one thing the walk is looking for. That the seek's phase does not change along the way is what makes it work.

What a seek proves

DescriptiveComplexity.SeekArrives is what a winning seek delivers: a cell whose symbol answers the test, together with the transition's tuple – the seek's own valuation up to the arity its phase declares, and an address that argsOf reads as the cell's. The tuple is kept because isTarget is a condition on it, and only the program knows that the coordinates outside those two halves are irrelevant.

Reading a win back, one step

theorem DescriptiveComplexity.altWin_succ_of_univ {U : Type} {N : ATMData U} {start : Bool} {c c' : Config U} (hnacc : ¬N.Acc c.state) (hu : N.IsUniv start c.state) (hc : N.AltWin start c) (hstep : N.Step c c') : N.AltWin start c'

At a universal configuration every successor wins.

theorem DescriptiveComplexity.exists_altWin_succ_of_ex {U : Type} {N : ATMData U} {start : Bool} {c : Config U} (hnacc : ¬N.Acc c.state) (hnu : ¬N.IsUniv start c.state) (hc : N.AltWin start c) : ∃ (c' : Config U), N.Step c c' ∧ N.AltWin start c'

At an existential configuration some successor wins, and it is the one the play chose.

def DescriptiveComplexity.SeekArrives {B : SOBlock} {V M : ℕ} {A : Type} [LinearOrder A] (a₀ : A) (isTarget : MachPh V M → SymTag B → (Fin (gameDim B V) → A) → Prop) (vars : GameQuestion → ℕ) (ph : MachPh V M) (vv : Fin (gameDim B V) → A) (tape : GamePt B V M A → GamePt B V M A) (pos : GamePt B V M A) : Prop

The cell a winning seek arrived at: its symbol answers the test, at a tuple carrying the phase's valuation and an address argsOf reads as the cell's.

Equations

• One or more equations did not get rendered due to their size.

What a winning seek delivers

theorem DescriptiveComplexity.seekArrives_of_altWin {B : SOBlock} {V M : ℕ} {A : Type} [LinearOrder A] {vars natoms : GameQuestion → ℕ} {pol : GameQuestion → ℕ → Bool} {a₀ : A} {hdim : blockArityBound B ≤ gameDim B V} {concOk : MachPh V M → (Fin (gameDim B V) → A) → Prop} {isTarget : MachPh V M → SymTag B → (Fin (gameDim B V) → A) → Prop} {ρ σ : B.Assignment A} (h₀ : IsBot a₀) {ph : MachPh V M} (hk : ph.kind = PhKind.seek) (hmark : ∀ (b : Bool) (w : Fin (gameDim B V) → A), ¬isTarget ph (SymTag.mark b) w) {vv : Fin (gameDim B V) → A} (hcv : Canon (MachPh.arity vars ph) vv) (c : Config (GamePt B V M A)) : (gameMachine vars pol a₀ hdim (gameRule vars natoms concOk isTarget)).AltWin true c → c.state = phasePt ph vv → (gameMachine vars pol a₀ hdim (gameRule vars natoms concOk isTarget)).Posn c.head → (∀ (q : GamePt B V M A), (gameMachine vars pol a₀ hdim (gameRule vars natoms concOk isTarget)).Posn q → c.tape q = tapeOfAssign a₀ hdim ρ σ q) → ∃ (pos : GamePt B V M A), (gameMachine vars pol a₀ hdim (gameRule vars natoms concOk isTarget)).Posn pos ∧ SeekArrives a₀ isTarget vars ph vv (tapeOfAssign a₀ hdim ρ σ) pos

A winning seek has arrived somewhere. The phase never changes along the walk and the tape is never touched, so the induction is on DescriptiveComplexity.ATMData.AltWin itself.

What a step of a rewind may be

A phase with one successor

The concluding phase, the challenge round, the claim

theorem DescriptiveComplexity.concOk_of_altWin {B : SOBlock} {V M : ℕ} {A : Type} [LinearOrder A] {vars natoms : GameQuestion → ℕ} {pol : GameQuestion → ℕ → Bool} {a₀ : A} {hdim : blockArityBound B ≤ gameDim B V} {concOk : MachPh V M → (Fin (gameDim B V) → A) → Prop} {isTarget : MachPh V M → SymTag B → (Fin (gameDim B V) → A) → Prop} {ρ σ : B.Assignment A} (h₀ : IsBot a₀) {p : MachPh V M} {vv : Fin (gameDim B V) → A} {c : Config (GamePt B V M A)} (hk : p.kind = PhKind.conc) (hcong : ∀ (w : Fin (gameDim B V) → A), Agree (MachPh.arity vars p) w vv → concOk p w → concOk p vv) (h : CtrlCfg a₀ hdim vars ρ σ p vv c) (hw : (gameMachine vars pol a₀ hdim (gameRule vars natoms concOk isTarget)).AltWin true c) : concOk p vv

A winning concluding phase has its guard satisfied – which is the only thing it can be doing, since a false guard leaves it with no transition.

theorem DescriptiveComplexity.check_of_altWin {B : SOBlock} {V M : ℕ} {A : Type} [LinearOrder A] {vars natoms : GameQuestion → ℕ} {pol : GameQuestion → ℕ → Bool} {a₀ : A} {hdim : blockArityBound B ≤ gameDim B V} {concOk : MachPh V M → (Fin (gameDim B V) → A) → Prop} {isTarget : MachPh V M → SymTag B → (Fin (gameDim B V) → A) → Prop} {ρ σ : B.Assignment A} (h₀ : IsBot a₀) {p : MachPh V M} {vv : Fin (gameDim B V) → A} {c : Config (GamePt B V M A)} (hk : p.kind = PhKind.check) (hmark : ∀ (k : Fin (M + 1)) (b : Bool) (w : Fin (gameDim B V) → A), ¬isTarget (MachPh.seekPh p.q p.r p.claims k !p.par) (SymTag.mark b) w) (hcong : ∀ (w : Fin (gameDim B V) → A), Agree (vars p.q) w vv → concOk (MachPh.concPh p.q p.r p.claims !p.par) w → concOk (MachPh.concPh p.q p.r p.claims !p.par) vv) (h : CtrlCfg a₀ hdim vars ρ σ p vv c) (hw : (gameMachine vars pol a₀ hdim (gameRule vars natoms concOk isTarget)).AltWin true c) : (∀ (k : Fin (M + 1)), ↑k < natoms p.q → ∃ (pos : GamePt B V M A), (gameMachine vars pol a₀ hdim (gameRule vars natoms concOk isTarget)).Posn pos ∧ SeekArrives a₀ isTarget vars (MachPh.seekPh p.q p.r p.claims k !p.par) vv (tapeOfAssign a₀ hdim ρ σ) pos) ∧ concOk (MachPh.concPh p.q p.r p.claims !p.par) vv

A winning challenge round has correct claims and a satisfied guard. The phase is universal, so the play answers every challenge and the concluding branch as well; each is a successor we build.

theorem DescriptiveComplexity.claim_of_altWin {B : SOBlock} {V M : ℕ} {A : Type} [LinearOrder A] {vars natoms : GameQuestion → ℕ} {pol : GameQuestion → ℕ → Bool} {a₀ : A} {hdim : blockArityBound B ≤ gameDim B V} {concOk : MachPh V M → (Fin (gameDim B V) → A) → Prop} {isTarget : MachPh V M → SymTag B → (Fin (gameDim B V) → A) → Prop} {ρ σ : B.Assignment A} (h₀ : IsBot a₀) {p : MachPh V M} {vv : Fin (gameDim B V) → A} {c : Config (GamePt B V M A)} (hk : p.kind = PhKind.claim) (hmark : ∀ (b' : Fin M → Bool) (k : Fin (M + 1)) (b : Bool) (w : Fin (gameDim B V) → A), ¬isTarget (MachPh.seekPh p.q p.r b' k p.par) (SymTag.mark b) w) (hcong : ∀ (b' : Fin M → Bool) (w : Fin (gameDim B V) → A), Agree (vars p.q) w vv → concOk (MachPh.concPh p.q p.r b' p.par) w → concOk (MachPh.concPh p.q p.r b' p.par) vv) (h : CtrlCfg a₀ hdim vars ρ σ p vv c) (hw : (gameMachine vars pol a₀ hdim (gameRule vars natoms concOk isTarget)).AltWin true c) : ∃ (b : Fin M → Bool), (∀ (k : Fin (M + 1)), ↑k < natoms p.q → ∃ (pos : GamePt B V M A), (gameMachine vars pol a₀ hdim (gameRule vars natoms concOk isTarget)).Posn pos ∧ SeekArrives a₀ isTarget vars (MachPh.seekPh p.q p.r b k p.par) vv (tapeOfAssign a₀ hdim ρ σ) pos) ∧ concOk (MachPh.concPh p.q p.r b p.par) vv

A winning claim phase has claimed something that survives the round.

The prefix, read back

theorem DescriptiveComplexity.pre_of_altWin {B : SOBlock} {V M : ℕ} {A : Type} [LinearOrder A] {vars natoms : GameQuestion → ℕ} {pol : GameQuestion → ℕ → Bool} {a₀ : A} {hdim : blockArityBound B ≤ gameDim B V} {concOk : MachPh V M → (Fin (gameDim B V) → A) → Prop} {isTarget : MachPh V M → SymTag B → (Fin (gameDim B V) → A) → Prop} {ρ σ : B.Assignment A} (h₀ : IsBot a₀) (hV : ∀ (q : GameQuestion), vars q ≤ V) {q : GameQuestion} {P : (Fin (vars q) → A) → Prop} {r : Bool} (hclaim : ∀ (par : Bool) (vv : Fin (gameDim B V) → A) (c : Config (GamePt B V M A)), CtrlCfg a₀ hdim vars ρ σ (MachPh.claimPh q r par) vv c → (gameMachine vars pol a₀ hdim (gameRule vars natoms concOk isTarget)).AltWin true c → P (qval hV q vv)) (fuel j : ℕ) : vars q - j ≤ fuel → j ≤ vars q → ∀ (par : Bool) (jj : Fin (V + 1)), ↑jj = j → ∀ (vv : Fin (gameDim B V) → A) (c : Config (GamePt B V M A)), CtrlCfg a₀ hdim vars ρ σ (MachPh.prePh q r jj par) vv c → (gameMachine vars pol a₀ hdim (gameRule vars natoms concOk isTarget)).AltWin true c → altQuantFrom (pol q) P j (qval hV q vv)

A winning prefix phase proves its prefix. The mirror of DescriptiveComplexity.altWin_pre, with the players' roles exchanged: at an existential variable the play chose a value and we read it off, at a universal one we instantiate the play at every value – each being a successor the forward direction knows how to build.