Outcomes of loopy games

We define when a loopy game is a win, a draw, or a loss with each player going first (under the normal play convention).

inductive LGame.IsWin : Player → LGame → Prop

IsWin p x means that player p wins x going first.

• intro {p : Player} {x y : LGame} : y ∈ moves p x → IsLoss (-p) y → IsWin p x

inductive LGame.IsLoss : Player → LGame → Prop

IsLoss p x means that player p loses x going first.

• intro {p : Player} {x : LGame} : (∀ y ∈ moves p x, IsWin (-p) y) → IsLoss p x

theorem LGame.isWin_iff_exists {p : Player} {x : LGame} : IsWin p x ↔ ∃ y ∈ moves p x, IsLoss (-p) y

theorem LGame.isLoss_iff_forall {p : Player} {x : LGame} : IsLoss p x ↔ ∀ y ∈ moves p x, IsWin (-p) y

theorem LGame.IsLoss.isWin_of_mem_moves {p : Player} {x y : LGame} (h : IsLoss p x) (hy : y ∈ moves p x) : IsWin (-p) y

theorem LGame.not_isWin_iff_forall {p : Player} {x : LGame} : ¬IsWin p x ↔ ∀ y ∈ moves p x, ¬IsLoss (-p) y

theorem LGame.not_isLoss_iff_exists {p : Player} {x : LGame} : ¬IsLoss p x ↔ ∃ y ∈ moves p x, ¬IsWin (-p) y

def LGame.IsStrategy (p : Player) (s : Set LGame) : Prop

A surviving strategy for player p, going second.

This is a set of states, such that for every move the opposite player makes, p can bring it back to the set.

You can think of this as a nonconstructive version of the more common definition of a strategy, which gives an explicit answer for every reachable state.

Equations

• LGame.IsStrategy p s = ∀ y ∈ s, ∀ z ∈ LGame.moves (-p) y, ∃ r ∈ LGame.moves p z, r ∈ s

theorem LGame.IsStrategy.neg {p : Player} {s : Set LGame} (h : IsStrategy p s) : IsStrategy (-p) (-s)

@[simp]

theorem LGame.isStrategy_neg {p : Player} {s : Set LGame} : IsStrategy p (-s) ↔ IsStrategy (-p) s

theorem LGame.IsStrategy.iUnion {p : Player} {ι : Sort u_1} {s : ι → Set LGame} (h : ∀ (i : ι), IsStrategy p (s i)) : IsStrategy p (⋃ (i : ι), s i)

theorem LGame.IsStrategy.sUnion {p : Player} {S : Set (Set LGame)} (h : ∀ s ∈ S, IsStrategy p s) : IsStrategy p (⋃₀ S)

theorem LGame.isStrategy_setOf_isLoss (p : Player) : IsStrategy p {x : LGame | IsLoss (-p) x}

theorem LGame.isStrategy_setOf_not_isWin (p : Player) : IsStrategy p {x : LGame | ¬IsWin (-p) x}

theorem LGame.not_isWin_iff_mem_Strategy {p : Player} {x : LGame} : ¬IsWin p x ↔ ∃ (s : Set LGame), x ∈ s ∧ IsStrategy (-p) s

@[simp]

theorem LGame.not_isLoss_of_isWin {p : Player} {x : LGame} (h : IsWin p x) : ¬IsLoss p x

@[simp]

theorem LGame.not_isWin_of_isLoss {p : Player} {x : LGame} (h : IsLoss p x) : ¬IsWin p x

def LGame.IsDraw (p : Player) (x : LGame) : Prop

IsDraw p x means that p draws x going first.

Equations

• LGame.IsDraw p x = (¬LGame.IsWin p x ∧ ¬LGame.IsLoss p x)

@[simp]

theorem LGame.IsDraw.not_isWin {p : Player} {x : LGame} (h : IsDraw p x) : ¬IsWin p x

@[simp]

theorem LGame.IsDraw.not_isLoss {p : Player} {x : LGame} (h : IsDraw p x) : ¬IsLoss p x

theorem LGame.not_isDraw_iff {p : Player} {x : LGame} : ¬IsDraw p x ↔ IsWin p x ∨ IsLoss p x

inductive LGame.Outcome : Type

The three possible outcomes of a game.

• win : Outcome
• draw : Outcome
• loss : Outcome

noncomputable def LGame.outcomeFor (p : Player) (x : LGame) : Outcome

outcomeFor p x is the outcome of x with p going first.

Equations

• LGame.outcomeFor p x = if LGame.IsWin p x then LGame.Outcome.win else if LGame.IsLoss p x then LGame.Outcome.loss else LGame.Outcome.draw

@[simp]

theorem LGame.outcomeFor_eq_win_iff {p : Player} {x : LGame} : outcomeFor p x = Outcome.win ↔ IsWin p x

@[simp]

theorem LGame.outcomeFor_eq_loss_iff {p : Player} {x : LGame} : outcomeFor p x = Outcome.loss ↔ IsLoss p x

@[simp]

theorem LGame.outcomeFor_eq_draw_iff {p : Player} {x : LGame} : outcomeFor p x = Outcome.draw ↔ IsDraw p x

theorem LGame.StopperFor.not_isDraw {p : Player} {x : LGame} (h : StopperFor p x) : ¬IsDraw p x

theorem LGame.Stopper.not_isDraw (p : Player) {x : LGame} (h : x.Stopper) : ¬IsDraw p x

@[simp]

theorem IGame.not_isDraw (p : Player) (x : IGame) : ¬LGame.IsDraw p (toLGame x)

@[simp]

theorem IGame.isWin_left_iff_zero_lf {x : IGame} : LGame.IsWin left (toLGame x) ↔ ¬x ≤ 0

@[simp]

theorem IGame.isLoss_left_iff_le_zero {x : IGame} : LGame.IsLoss left (toLGame x) ↔ x ≤ 0

@[simp]

theorem IGame.isWin_right_iff_lf_zero {x : IGame} : LGame.IsWin right (toLGame x) ↔ ¬0 ≤ x

@[simp]

theorem IGame.isLoss_right_iff_zero_le {x : IGame} : LGame.IsLoss right (toLGame x) ↔ 0 ≤ x

theorem IGame.fuzzy_zero_iff_isWin {x : IGame} : x ‖ 0 ↔ ∀ (p : Player), LGame.IsWin p (toLGame x)

theorem IGame.equiv_zero_iff_isLoss {x : IGame} : x ≈ 0 ↔ ∀ (p : Player), LGame.IsLoss p (toLGame x)

theorem IGame.lt_zero_iff_isLoss_and_isWin {x : IGame} : x < 0 ↔ LGame.IsLoss left (toLGame x) ∧ LGame.IsWin right (toLGame x)

theorem IGame.zero_lt_iff_isWin_and_isLoss {x : IGame} : 0 < x ↔ LGame.IsWin left (toLGame x) ∧ LGame.IsLoss right (toLGame x)