A General Theory for Determined Two-player Games

Nothing here is specific about PDL, but we give a general definition of games and show that one of the two players must have a winning strategy: gamedet at the end.

Games

inductive Player : Type

Two players, A and B.

• A : Player
• B : Player

instance instDecidableEqPlayer : DecidableEq Player

Equations

• instDecidableEqPlayer x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[simp]

theorem Player.ne_A_iff_eq_B {p : Player} : p ≠ A ↔ p = B

@[simp]

theorem Player.ne_B_iff_eq_A {p : Player} : p ≠ B ↔ p = A

@[simp]

theorem Player.not_eq_iff_eq_other {p : Player} : ¬p = A ↔ p = B

@[simp]

theorem Player.not_eq_B_iff_eq_A {p : Player} : ¬p = B ↔ p = A

theorem Player.eq_A_or_eq_B {p : Player} : p = A ∨ p = B

def other : Player → Player

Equations

• other Player.A = Player.B
• other Player.B = Player.A

@[simp]

theorem other_A_eq_B : other Player.A = Player.B

@[simp]

theorem other_B_eq_A : other Player.B = Player.A

@[simp]

theorem Player.not_eq_i_eq_other {p i : Player} : ¬p = i ↔ p = other i

@[simp]

theorem Player.not_eq_other_eq_i {p i : Player} : ¬p = other i ↔ p = i

@[simp]

theorem Player.not_i_eq_other {i : Player} : ¬i = other i

@[simp]

theorem Player.not_other_i_eq_i {i : Player} : ¬other i = i

@[simp]

theorem other_other {i : Player} : other (other i) = i

class Game : Type 1

Two-player game with

• perfect information
• sequential moves (i.e. only one player moves at each position)
• finitely many moves at each step
• a decreasing bound on the number of remaining steps

• Pos : Type

  Positions in the game.

• turn : Pos → Player

  Whose turn is it?

• moves : Pos → Finset Pos

  What are the available moves?

• wf : WellFoundedRelation Pos

  A wellfounded relation on positions.

• move_rel (p next : Pos) : next ∈ moves p → WellFoundedRelation.rel next p

  Every move goes a step down in the relation.

instance instWellFoundedRelationPos {g : Game} : WellFoundedRelation Game.Pos

This seems a bit hacky, but makes termination_by (p : g.Pos) work in winner and elsewhere. If the instance causes trouble, change to termination_by g.wf.2.wrap p via WellFounded.wrap.

Equations

• instWellFoundedRelationPos = Game.wf

@[reducible, inline]

abbrev Game.Pos.moves {g : Game} : Pos → Finset Pos

Allow notation p.moves for g.moves p.

Equations

• Game.Pos.moves = Game.moves

theorem Game.no_moves_of_no_rel {g : Game} {p : Pos} (no_rel : ∀ (q : Pos), ¬WellFoundedRelation.rel q p) : moves p = ∅

If the bound bound is zero then there are no more moves.

instance instLTPos {g : Game} : LT Game.Pos

Equations

• instLTPos = { lt := fun (p q : Game.Pos) => WellFoundedRelation.rel q p }

Strategies

def Strategy (g : Game) (i : Player) : Type

A strategy in g for i, whenever it is i's turn, chooses a move, if there are any.

Equations

• Strategy g i = ((p : Game.Pos) → Game.turn p = i → p.moves.Nonempty → { x : Game.Pos // x ∈ p.moves })

noncomputable def choose_move {g : Game} {p : Game.Pos} : p.moves.Nonempty → { x : Game.Pos // x ∈ p.moves }

Equations

• choose_move = Classical.choice ∘ ⋯

instance Strategy.instNonempty {g : Game} {i : Player} : Nonempty (Strategy g i)

There is always some strategy.

@[irreducible]

def winner {i : Player} {g : Game} (sI : Strategy g i) (sJ : Strategy g (other i)) (p : Game.Pos) : Player

Winner of a game, if the given strategies are used. A player loses iff it is their turn and there are no moves. A player wins if the opponent loses.

Equations

• winner sI sJ p = if h1 : (Game.moves p).Nonempty then if h2 : Game.turn p = i then winner sI sJ ↑(sI p h2 h1) else winner sI sJ ↑(sJ p ⋯ h1) else other (Game.turn p)

def winning {g : Game} {i : Player} (sI : Strategy g i) (p : Game.Pos) : Prop

A strategy is winning at p if it wins against all strategies of the other player.

Equations

• winning sI p = ∀ (sJ : Strategy g (other i)), winner sI sJ p = i

Good positions

@[irreducible]

def good {g : Game} (i : Player) (p : Game.Pos) : Prop

Equations

• good i p = ((Game.turn p = i ∧ ∃ (q : Game.Pos) (_ : q ∈ p.moves), good i q) ∨ Game.turn p = other i ∧ ∀ q ∈ p.moves, good i q)

theorem good_is_surviving {i : Player} {g : Game} {p : Game.Pos} : good i p → Game.turn p = i → p.moves.Nonempty

theorem good_or_other {g : Game} (p : Game.Pos) : good (Game.turn p) p ∨ good (other (Game.turn p)) p

theorem good_A_or_B {g : Game} (p : Game.Pos) : good Player.A p ∨ good Player.B p

noncomputable def good_strat {g : Game} (i : Player) : Strategy g i

Equations

• good_strat i p turn nempty = if W : good i p then have E := ⋯; ⟨E.choose, ⋯⟩ else choose_move nempty

Cones

inductive inMyCone {i : Player} {g : Game} (sI : Strategy g i) (p : Game.Pos) : Game.Pos → Prop

The cone of all positions reachable from p assuming that i plays sI.

• nil {i : Player} {g : Game} {sI : Strategy g i} {p : Game.Pos} : inMyCone sI p p
• myStep {i : Player} {g : Game} {sI : Strategy g i} {p q : Game.Pos} : inMyCone sI p q → ∀ (has_moves : q.moves.Nonempty) (h : Game.turn q = i), inMyCone sI p ↑(sI q h has_moves)
• oStep {i : Player} {g : Game} {sI : Strategy g i} {p q r : Game.Pos} : inMyCone sI p q → Game.turn q = other i → r ∈ Game.moves q → inMyCone sI p r

theorem inMyCone_trans {g : Game} {i : Player} {p q r : Game.Pos} {s : Strategy g i} : inMyCone s p q → inMyCone s q r → inMyCone s p r

theorem good_cone {i : Player} {g : Game} {p r : Game.Pos} (W : good i p) (h : inMyCone (good_strat i) p r) : good i r

The cone of the good_strat stays inside good positions.

Zermelo's Theorem

@[irreducible]

theorem surviving_is_winning {g : Game} {i : Player} {p : Game.Pos} {sI : Strategy g i} (surv : ∀ (q : Game.Pos), inMyCone sI p q → Game.turn q = i → q.moves.Nonempty) : winning sI p

theorem good_strat_winning {i : Player} {self✝ : Game} {p : Game.Pos} (W : good i p) : winning (good_strat i) p

theorem gamedet (g : Game) (p : Game.Pos) : (∃ (s : Strategy g Player.A), winning s p) ∨ ∃ (s : Strategy g Player.B), winning s p

Zermelo's Theorem: In every Game position one of the two players has a winning strategy. https://en.wikipedia.org/wiki/Zermelo%27s_theorem_(game_theory)

Additional Helper Theorems

theorem winning_has_moves {g : Game} {i : Player} {sI : Strategy g i} {p : Game.Pos} (h : Game.turn p = i) (sI_wins_p : winning sI p) : (Game.moves p).Nonempty

theorem winning_of_winning_move {g : Game} {i : Player} {sI : Strategy g i} {p : Game.Pos} (h : Game.turn p = i) (sI_wins_p : winning sI p) : winning sI ↑(sI p h ⋯)

theorem game_wf_rel_of_cone {i : Player} {g : Game} {p r : Game.Pos} (sI : Strategy g i) (r_in : inMyCone sI p r) : Relation.ReflTransGen WellFoundedRelation.rel r p

theorem not_in_cone_of_move {i : Player} {g : Game} {p q : Game.Pos} (q_in : q ∈ Game.moves p) (sI : Strategy g i) : ¬inMyCone sI q p

@[irreducible]

theorem same_winner_of_same_in_cone {i : Player} {g : Game} {sI : Strategy g i} {sJ sJ' : Strategy g (other i)} {p : Game.Pos} (same_cone : ∀ (r : Game.Pos), inMyCone sJ p r → sJ r = sJ' r) : winner sI sJ p = winner sI sJ' p

theorem winning_of_whatever_other_move {g : Game} {i : Player} {sI : Strategy g i} {p : Game.Pos} (h : Game.turn p = other i) (sI_wins_p : winning sI p) (m : { x : Game.Pos // x ∈ Game.moves p }) : winning sI ↑m

Helper for gameP_general.