The game, read back

The backward simulation of the game itself: a winning configuration of the machine is a winning state of the game. It is one induction on DescriptiveComplexity.ATMData.AltWin, whose motive is a conjunction with one clause per phase the game proper can be in.

What each phase proves

The conclusions at play, splitEx and splitAll are all spec.Wins ρ, because what a split proves is exactly the premises of the matching constructor of DescriptiveComplexity.SOGameSpec.Wins. The others are the DescriptiveComplexity.ContGoal a sweep's continuation names:

start   ⟶ IsStart ρ ∧ Wins ρ            certify ⟶ Move ρ σ
exMove  ⟶ Move ρ σ ∧ Wins σ             allMove ⟶ ¬ Move ρ σ ∨ Wins σ

In each case of the induction most clauses are one line: at acc no phase of the game is accepting, and at ex/all the clauses of the other polarity are killed by IsUniv.

The one trap, and the motive that avoids it

A universal sweep cannot be read backwards: its clause is every candidate is answered, and at a half-finished sweep that is false – the cells already written cannot be changed. So the motive is strengthened to

Sound c : for every d reachable from c by steps whose sources are universal sweeps, the clauses hold at d.

The clauses at c follow by the reflexive chain, and in the all case the chain's first step is a successor, so the induction hypothesis covers the rest of it. That lets the universal sweep be proved forward: its run supplies the chain, the handover the last step, and the motive delivers the clauses at the rewind configuration – whose clause is the ContGoal wanted.

def DescriptiveComplexity.WalkCfg {B : SOBlock} {V M : ℕ} {A : Type} [LinearOrder A] (a₀ : A) (hdim : blockArityBound B ≤ gameDim B V) (vars : GameQuestion → ℕ) (ρ σ : B.Assignment A) (p : MachPh V M) (c : Config (GamePt B V M A)) : Prop

A configuration in the middle of a walk: the phase at the constant valuation, the head anywhere among the positions, and the tape holding the two assignments. Unlike DescriptiveComplexity.CtrlCfg it does not pin the head to a sentinel, which is exactly what a rewind needs.

Equations

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

def DescriptiveComplexity.ContGoal {L : FirstOrder.Language} (spec : SOGameSpec L) {A : Type} [L.Structure A] [LinearOrder A] (cont : SweepCont) (r : Bool) (ρ σ : spec.B.Assignment A) : Prop

What a sweep's continuation has to prove, one clause per place the control guesses an assignment.

Equations

• DescriptiveComplexity.ContGoal spec DescriptiveComplexity.SweepCont.start r ρ σ = (spec.IsStart (bif r then σ else ρ) ∧ spec.Wins (bif r then σ else ρ))
• DescriptiveComplexity.ContGoal spec DescriptiveComplexity.SweepCont.exMove r ρ σ = (spec.Move (bif r then σ else ρ) (bif !r then σ else ρ) ∧ spec.Wins (bif !r then σ else ρ))
• DescriptiveComplexity.ContGoal spec DescriptiveComplexity.SweepCont.certify r ρ σ = spec.Move (bif r then σ else ρ) (bif !r then σ else ρ)
• DescriptiveComplexity.ContGoal spec DescriptiveComplexity.SweepCont.allMove r ρ σ = (¬spec.Move (bif r then σ else ρ) (bif !r then σ else ρ) ∨ spec.Wins (bif !r then σ else ρ))

structure DescriptiveComplexity.GameStmt {L : FirstOrder.Language} (spec : SOGameSpec L) {V M : ℕ} (prog : GameProg (L.sum FirstOrder.Language.order) spec.B V M) {A : Type} [L.Structure A] [LinearOrder A] (a₀ : A) (hdim : blockArityBound spec.B ≤ gameDim spec.B V) (d : Config (GamePt spec.B V M A)) : Prop

What a win proves, phase by phase.

• play (ρ₀ σ₀ : spec.B.Assignment A) (r par : Bool) : CtrlCfg a₀ hdim prog.vars ρ₀ σ₀ (MachPh.playPh r par) (fun (x : Fin (gameDim spec.B V)) => a₀) d → spec.Wins (bif r then σ₀ else ρ₀)

  A position of the game is winning.

• splitEx (ρ₀ σ₀ : spec.B.Assignment A) (r par : Bool) : CtrlCfg a₀ hdim prog.vars ρ₀ σ₀ (MachPh.splitExPh r par) (fun (x : Fin (gameDim spec.B V)) => a₀) d → spec.Wins (bif r then σ₀ else ρ₀)

  So is the existential clause.

• splitAll (ρ₀ σ₀ : spec.B.Assignment A) (r par : Bool) : CtrlCfg a₀ hdim prog.vars ρ₀ σ₀ (MachPh.splitAllPh r par) (fun (x : Fin (gameDim spec.B V)) => a₀) d → spec.Wins (bif r then σ₀ else ρ₀)

  And the universal one.

• splitMove (ρ₀ σ₀ : spec.B.Assignment A) (r par : Bool) : CtrlCfg a₀ hdim prog.vars ρ₀ σ₀ (MachPh.splitMovePh r par) (fun (x : Fin (gameDim spec.B V)) => a₀) d → ContGoal spec SweepCont.exMove r ρ₀ σ₀

  After an existential move: it is legal, and the play goes on.

• allStep (ρ₀ σ₀ : spec.B.Assignment A) (r par : Bool) : CtrlCfg a₀ hdim prog.vars ρ₀ σ₀ (MachPh.allStepPh r par) (fun (x : Fin (gameDim spec.B V)) => a₀) d → ContGoal spec SweepCont.allMove r ρ₀ σ₀

  After a universal move: it is refuted, or the play goes on.

• splitStart (ρ₀ σ₀ : spec.B.Assignment A) (r par : Bool) : CtrlCfg a₀ hdim prog.vars ρ₀ σ₀ (MachPh.splitStartPh r par) (fun (x : Fin (gameDim spec.B V)) => a₀) d → ContGoal spec SweepCont.start r ρ₀ σ₀

  At the start: the position starts the game, and wins it.

• rewind (ρ₀ σ₀ : spec.B.Assignment A) (r tgt : Bool) (cont : SweepCont) (par : Bool) : WalkCfg a₀ hdim prog.vars ρ₀ σ₀ (MachPh.rewindPh r tgt cont par) d → ContGoal spec cont r ρ₀ σ₀

  A rewind proves what its continuation must.

• sweepEx (ρ₀ σ₀ : spec.B.Assignment A) (r tgt : Bool) (cont : SweepCont) (par : Bool) : cont ≠ SweepCont.allMove → SweptCfg a₀ hdim prog.vars ρ₀ σ₀ tgt (MachPh.sweepPh r tgt cont par) d → ∃ (ρ' : spec.B.Assignment A) (σ' : spec.B.Assignment A), (∀ (rr : Bool), rr ≠ tgt → (bif rr then σ' else ρ') = bif rr then σ₀ else ρ₀) ∧ ContGoal spec cont r ρ' σ'

  An existential sweep proves it for some assignment of its region.

• sweepAll (ρ₀ σ₀ : spec.B.Assignment A) (r tgt par : Bool) : SweptCfg a₀ hdim prog.vars ρ₀ σ₀ tgt (MachPh.sweepPh r tgt SweepCont.allMove par) d → d.head = leftPt a₀ par → ∀ (ρ' σ' : spec.B.Assignment A), (∀ (rr : Bool), rr ≠ tgt → (bif rr then σ' else ρ') = bif rr then σ₀ else ρ₀) → ContGoal spec SweepCont.allMove r ρ' σ'

  A universal sweep proves it for every assignment of its region – but only at its entry, the head on the sentinel its parity names.

def DescriptiveComplexity.AtAllSweep {L : FirstOrder.Language} {spec : SOGameSpec L} {V M : ℕ} {A : Type} (a₀ : A) (d : Config (GamePt spec.B V M A)) : Prop

The guard of the chain the motive quantifies over: a step taken from a universal sweep.

Equations

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

def DescriptiveComplexity.Sound {L : FirstOrder.Language} (spec : SOGameSpec L) {V M : ℕ} (prog : GameProg (L.sum FirstOrder.Language.order) spec.B V M) {A : Type} [L.Structure A] [LinearOrder A] (a₀ : A) (hdim : blockArityBound spec.B ≤ gameDim spec.B V) (c : Config (GamePt spec.B V M A)) : Prop

The motive: the clauses hold not only here but everywhere a universal sweep can carry the play. See the module docstring for why.

Equations

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

Small conversions between the three shapes of a configuration

theorem DescriptiveComplexity.WalkCfg.of_ctrlCfg {L : FirstOrder.Language} {spec : SOGameSpec L} {V M : ℕ} {prog : GameProg (L.sum FirstOrder.Language.order) spec.B V M} {A : Type} [LinearOrder A] {a₀ : A} {hdim : blockArityBound spec.B ≤ gameDim spec.B V} {ρ₀ σ₀ : spec.B.Assignment A} {p : MachPh V M} {d : Config (GamePt spec.B V M A)} (h₀ : IsBot a₀) (h : CtrlCfg a₀ hdim prog.vars ρ₀ σ₀ p (fun (x : Fin (gameDim spec.B V)) => a₀) d) : WalkCfg a₀ hdim prog.vars ρ₀ σ₀ p d

theorem DescriptiveComplexity.CtrlCfg.of_walkCfg {L : FirstOrder.Language} {spec : SOGameSpec L} {V M : ℕ} {prog : GameProg (L.sum FirstOrder.Language.order) spec.B V M} {A : Type} [LinearOrder A] {a₀ : A} {hdim : blockArityBound spec.B ≤ gameDim spec.B V} {ρ₀ σ₀ : spec.B.Assignment A} {p : MachPh V M} {d : Config (GamePt spec.B V M A)} (h₀ : IsBot a₀) (h : WalkCfg a₀ hdim prog.vars ρ₀ σ₀ p d) (hhead : d.head = leftPt a₀ p.par) : CtrlCfg a₀ hdim prog.vars ρ₀ σ₀ p (fun (x : Fin (gameDim spec.B V)) => a₀) d

theorem DescriptiveComplexity.SweptCfg.of_ctrlCfg {L : FirstOrder.Language} {spec : SOGameSpec L} {V M : ℕ} {prog : GameProg (L.sum FirstOrder.Language.order) spec.B V M} {A : Type} [LinearOrder A] {a₀ : A} {hdim : blockArityBound spec.B ≤ gameDim spec.B V} {ρ₀ σ₀ : spec.B.Assignment A} {tgt : Bool} {p : MachPh V M} {d : Config (GamePt spec.B V M A)} (h₀ : IsBot a₀) (h : CtrlCfg a₀ hdim prog.vars ρ₀ σ₀ p (fun (x : Fin (gameDim spec.B V)) => a₀) d) : SweptCfg a₀ hdim prog.vars ρ₀ σ₀ tgt p d

theorem DescriptiveComplexity.not_acc_of_state {L : FirstOrder.Language} {spec : SOGameSpec L} {V M : ℕ} {prog : GameProg (L.sum FirstOrder.Language.order) spec.B V M} {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} {hdim : blockArityBound spec.B ≤ gameDim spec.B V} {d : Config (GamePt spec.B V M A)} {p : MachPh V M} {vv : Fin (gameDim spec.B V) → A} (hst : d.state = phasePt p vv) (hk : p.kind ≠ PhKind.acc) : ¬(gameMachine prog.vars prog.pol a₀ hdim (gameRule prog.vars prog.natoms prog.concOk prog.isTarget)).Acc d.state

No phase of the game is accepting.

theorem DescriptiveComplexity.isUniv_state {L : FirstOrder.Language} {spec : SOGameSpec L} {V M : ℕ} {prog : GameProg (L.sum FirstOrder.Language.order) spec.B V M} {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} {hdim : blockArityBound spec.B ≤ gameDim spec.B V} {d : Config (GamePt spec.B V M A)} {p : MachPh V M} {vv : Fin (gameDim spec.B V) → A} (hst : d.state = phasePt p vv) : (gameMachine prog.vars prog.pol a₀ hdim (gameRule prog.vars prog.natoms prog.concOk prog.isTarget)).IsUniv true d.state ↔ MachPh.IsUniv prog.pol p = true

A configuration belongs to the universal player exactly when its phase does.

The three cases of the induction

theorem DescriptiveComplexity.gameStmt_of_acc {L : FirstOrder.Language} {spec : SOGameSpec L} {V M : ℕ} {prog : GameProg (L.sum FirstOrder.Language.order) spec.B V M} {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} {hdim : blockArityBound spec.B ≤ gameDim spec.B V} {d : Config (GamePt spec.B V M A)} (hacc : (gameMachine prog.vars prog.pol a₀ hdim (gameRule prog.vars prog.natoms prog.concOk prog.isTarget)).Acc d.state) : GameStmt spec prog a₀ hdim d

At an accepting configuration the clauses are vacuous: no phase of the game is the accepting one.

theorem DescriptiveComplexity.gameStmt_of_ex {L : FirstOrder.Language} {spec : SOGameSpec L} {V M : ℕ} {prog : GameProg (L.sum FirstOrder.Language.order) spec.B V M} {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} {hdim : blockArityBound spec.B ≤ gameDim spec.B V} (h₀ : IsBot a₀) (hplays : ∀ (q : GameQuestion), (prog.data q).Plays (spec.question q)) {d d' : Config (GamePt spec.B V M A)} (hnu : ¬(gameMachine prog.vars prog.pol a₀ hdim (gameRule prog.vars prog.natoms prog.concOk prog.isTarget)).IsUniv true d.state) (hstep : (gameMachine prog.vars prog.pol a₀ hdim (gameRule prog.vars prog.natoms prog.concOk prog.isTarget)).Step d d') (hw' : (gameMachine prog.vars prog.pol a₀ hdim (gameRule prog.vars prog.natoms prog.concOk prog.isTarget)).AltWin true d') (ihd : GameStmt spec prog a₀ hdim d') : GameStmt spec prog a₀ hdim d

At an existential configuration, the play chose one successor and what that choice proves is read off the step analysis.

theorem DescriptiveComplexity.chain_atAllSweep {L : FirstOrder.Language} {spec : SOGameSpec L} {V M : ℕ} {prog : GameProg (L.sum FirstOrder.Language.order) spec.B V M} {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} {hdim : blockArityBound spec.B ≤ gameDim spec.B V} {r tgt par : Bool} {d dR : Config (GamePt spec.B V M A)} (hst : d.state = phasePt (MachPh.sweepPh r tgt SweepCont.allMove par) fun (x : Fin (gameDim spec.B V)) => a₀) (h : Relation.ReflTransGen (fun (x y : Config (GamePt spec.B V M A)) => (gameMachine prog.vars prog.pol a₀ hdim (gameRule prog.vars prog.natoms prog.concOk prog.isTarget)).Step x y ∧ x.state = d.state) d dR) : Relation.ReflTransGen (fun (x y : Config (GamePt spec.B V M A)) => (gameMachine prog.vars prog.pol a₀ hdim (gameRule prog.vars prog.natoms prog.concOk prog.isTarget)).Step x y ∧ AtAllSweep a₀ x) d dR

The chain a sweep's run produces is guarded by at a universal sweep.

theorem DescriptiveComplexity.gameStmt_of_all {L : FirstOrder.Language} {spec : SOGameSpec L} {V M : ℕ} {prog : GameProg (L.sum FirstOrder.Language.order) spec.B V M} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] {a₀ : A} {hdim : blockArityBound spec.B ≤ gameDim spec.B V} (h₀ : IsBot a₀) (hplays : ∀ (q : GameQuestion), (prog.data q).Plays (spec.question q)) {d : Config (GamePt spec.B V M A)} (hu : (gameMachine prog.vars prog.pol a₀ hdim (gameRule prog.vars prog.natoms prog.concOk prog.isTarget)).IsUniv true d.state) (hall : ∀ (c' : Config (GamePt spec.B V M A)), (gameMachine prog.vars prog.pol a₀ hdim (gameRule prog.vars prog.natoms prog.concOk prog.isTarget)).Step d c' → (gameMachine prog.vars prog.pol a₀ hdim (gameRule prog.vars prog.natoms prog.concOk prog.isTarget)).AltWin true c') (ih : ∀ (c' : Config (GamePt spec.B V M A)), (gameMachine prog.vars prog.pol a₀ hdim (gameRule prog.vars prog.natoms prog.concOk prog.isTarget)).Step d c' → Sound spec prog a₀ hdim c') : GameStmt spec prog a₀ hdim d

At a universal configuration every successor wins, so the play may be instantiated at each of the ones the forward direction knows how to build. The universal sweep is the exception: it is followed forward, through the chain the motive quantifies over.

The induction, and the entry

theorem DescriptiveComplexity.sound_of_altWin {L : FirstOrder.Language} {spec : SOGameSpec L} {V M : ℕ} {prog : GameProg (L.sum FirstOrder.Language.order) spec.B V M} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] {a₀ : A} {hdim : blockArityBound spec.B ≤ gameDim spec.B V} (h₀ : IsBot a₀) (hplays : ∀ (q : GameQuestion), (prog.data q).Plays (spec.question q)) (c : Config (GamePt spec.B V M A)) : (gameMachine prog.vars prog.pol a₀ hdim (gameRule prog.vars prog.natoms prog.concOk prog.isTarget)).AltWin true c → Sound spec prog a₀ hdim c

A winning configuration of the machine proves what its phase says. One induction on DescriptiveComplexity.ATMData.AltWin, the three cases being the three lemmas above; the chain in the motive is what carries a universal sweep.

theorem DescriptiveComplexity.accepts_of_altAcceptsSpace {L : FirstOrder.Language} {spec : SOGameSpec L} {V M : ℕ} {prog : GameProg (L.sum FirstOrder.Language.order) spec.B V M} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] {a₀ : A} {hdim : blockArityBound spec.B ≤ gameDim spec.B V} (h₀ : IsBot a₀) (hplays : ∀ (q : GameQuestion), (prog.data q).Plays (spec.question q)) (hacc : (gameMachine prog.vars prog.pol a₀ hdim (gameRule prog.vars prog.natoms prog.concOk prog.isTarget)).AltAcceptsSpace true) : spec.Accepts A

The game accepts when the machine does. The very first sweep is the one that guessed the starting position, so what it proves – by DescriptiveComplexity.ContGoal at start – is that some assignment starts the game and wins it.

theorem DescriptiveComplexity.altAcceptsSpace_iff_accepts {L : FirstOrder.Language} {spec : SOGameSpec L} {V M : ℕ} {prog : GameProg (L.sum FirstOrder.Language.order) spec.B V M} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] {a₀ : A} {hdim : blockArityBound spec.B ≤ gameDim spec.B V} (h₀ : IsBot a₀) (hplays : ∀ (q : GameQuestion), (prog.data q).Plays (spec.question q)) : (gameMachine prog.vars prog.pol a₀ hdim (gameRule prog.vars prog.natoms prog.concOk prog.isTarget)).AltAcceptsSpace true ↔ spec.Accepts A

The machine accepts exactly when the game does. Both halves of the simulation, in one statement – and the whole of what SO-GAME ≤ʳᶠᵒ[≤] ATMAcceptSpace needs of the machine.