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 Lean4GlCoalgebras.Player : Type

Two players, A and B.

• A : Player
• B : Player

@[implicit_reducible]

instance Lean4GlCoalgebras.instDecidableEqPlayer : DecidableEq Player

Equations

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

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

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

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

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

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

def Lean4GlCoalgebras.other : Player → Player

Auxiliary declaration used in the GL coalgebra development.

Equations

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

@[simp]

theorem Lean4GlCoalgebras.other_A_eq_B : other Player.A = Player.B

@[simp]

theorem Lean4GlCoalgebras.other_B_eq_A : other Player.B = Player.A

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

class Lean4GlCoalgebras.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 (aka finitely branching)
• a well-founded relation to ensure that the game ends.

• 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.

@[implicit_reducible]

instance Lean4GlCoalgebras.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

• Lean4GlCoalgebras.instWellFoundedRelationPos = Lean4GlCoalgebras.Game.wf

@[reducible, inline]

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

Allow notation p.moves for g.moves p.

Equations

• Lean4GlCoalgebras.Game.Pos.moves = Lean4GlCoalgebras.Game.moves

theorem Lean4GlCoalgebras.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.

@[implicit_reducible]

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

Equations

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

Strategies

def Lean4GlCoalgebras.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

• Lean4GlCoalgebras.Strategy g i = ((p : Lean4GlCoalgebras.Game.Pos) → Lean4GlCoalgebras.Game.turn p = i → p.moves.Nonempty → ↥p.moves)

noncomputable def Lean4GlCoalgebras.chooseMove {g : Game} {p : Game.Pos} : p.moves.Nonempty → ↥p.moves

Auxiliary declaration used in the GL coalgebra development.

Equations

• Lean4GlCoalgebras.chooseMove = Classical.choice ∘ ⋯

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

There is always some strategy.

@[irreducible]

def Lean4GlCoalgebras.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

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

def Lean4GlCoalgebras.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

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

Good positions

@[irreducible]

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

Auxiliary declaration used in the GL coalgebra development.

Equations

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

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

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

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

noncomputable def Lean4GlCoalgebras.goodStrat {g : Game} (i : Player) : Strategy g i

Auxiliary declaration used in the GL coalgebra development.

Equations

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

Cones

inductive Lean4GlCoalgebras.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 Lean4GlCoalgebras.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 Lean4GlCoalgebras.good_cone {i : Player} {g : Game} {p r : Game.Pos} (W : good i p) (h : inMyCone (goodStrat i) p r) : good i r

The cone of the goodStrat stays inside good positions.

Zermelo's Theorem

theorem Lean4GlCoalgebras.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 Lean4GlCoalgebras.good_strat_winning {g : Game} {i : Player} {p : Game.Pos} (W : good i p) : winning (goodStrat i) p

theorem Lean4GlCoalgebras.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.

Additional Helper Theorems

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

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

theorem Lean4GlCoalgebras.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 Lean4GlCoalgebras.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

theorem Lean4GlCoalgebras.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 Lean4GlCoalgebras.winning_of_whatever_other_move {i : Player} {g : Game} {sI : Strategy g i} {p : Game.Pos} (h : Game.turn p = other i) (sI_wins_p : winning sI p) (m : ↥(Game.moves p)) : winning sI ↑m

Helper for gameP_general.

theorem Lean4GlCoalgebras.winning_of_in_cone_winning {g : Game} {i : Player} {p q : Game.Pos} {sI : Strategy g i} (in_cone : inMyCone sI p q) (h : winning sI p) : winning sI q