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.

theorem DescriptiveComplexity.not_acc_ctrlCfg {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} {p : MachPh V M} {vv : Fin (gameDim B V) → A} {c : Config (GamePt B V M A)} (h : CtrlCfg a₀ hdim vars ρ σ p vv c) (hk : p.kind ≠ PhKind.acc) : ¬(gameMachine vars pol a₀ hdim (gameRule vars natoms concOk isTarget)).Acc c.state

A configuration of the control accepts only in the accepting phase.

What a winning seek delivers

theorem DescriptiveComplexity.seekCfg_cases {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 c' : Config (GamePt B V M A)} (hstate : c.state = phasePt ph vv) (hpos : (gameMachine vars pol a₀ hdim (gameRule vars natoms concOk isTarget)).Posn c.head) (htape : ∀ (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) (hstep : (gameMachine vars pol a₀ hdim (gameRule vars natoms concOk isTarget)).Step c c') : (c'.state = c.state ∧ (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

What a step of a seek may be: it stays in the phase with the tape untouched, or it is the arrival at the cell the seek was looking for.

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

theorem DescriptiveComplexity.rewindCfg_cases {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₀) {r tgt : Bool} {cont : SweepCont} {par : Bool} {c c' : Config (GamePt B V M A)} (hstate : c.state = phasePt (MachPh.rewindPh r tgt cont par) fun (x : Fin (gameDim B V)) => a₀) (hpos : (gameMachine vars pol a₀ hdim (gameRule vars natoms concOk isTarget)).Posn c.head) (htape : ∀ (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) (hstep : (gameMachine vars pol a₀ hdim (gameRule vars natoms concOk isTarget)).Step c c') : (c'.state = c.state ∨ (c'.state = phasePt (MachPh.rewindPh r tgt cont par).rewindTarget fun (x : Fin (gameDim B V)) => a₀) ∧ c'.head = leftPt a₀ false) ∧ (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

A rewind either walks on or hands over, and either way the tape is untouched – both its rules write back what they read. The handover lands on the lowest position, which is what the two sentinels being adjacent buys.

A phase with one successor

theorem DescriptiveComplexity.exists_altWin_succ_uniq {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 p' : MachPh V M} {vv : Fin (gameDim B V) → A} {c : Config (GamePt B V M A)} (hsw : p.kind ≠ PhKind.sweep) (hrw : p.kind ≠ PhKind.rewind) (hsk : p.kind ≠ PhKind.seek) (hnc : p.kind ≠ PhKind.conc) (hna : p.kind ≠ PhKind.acc) (harity : MachPh.arity vars p' = MachPh.arity vars p) (hcs : MachPh.CtrlStep vars natoms p p') (hcsu : ∀ (p'' : MachPh V M), MachPh.CtrlStep vars natoms p p'' → p'' = p') (h : CtrlCfg a₀ hdim vars ρ σ p vv c) (hw : (gameMachine vars pol a₀ hdim (gameRule vars natoms concOk isTarget)).AltWin true c) : ∃ (c' : Config (GamePt B V M A)), CtrlCfg a₀ hdim vars ρ σ p' vv c' ∧ (gameMachine vars pol a₀ hdim (gameRule vars natoms concOk isTarget)).AltWin true c'

A phase with exactly one successor hands its win on, whichever player owns it: the universal one because every successor wins, the existential one because the successor it chose is that one. The valuation is carried over because the two phases declare the same coordinates.

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.