Documentation

CombinatorialGames.Game.Loopy.Outcome

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

Instances For

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

Instances For

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) :

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

Instances For

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_setOfPred_isLoss (p : Player) :

IsStrategy p {x : LGame | IsLoss (-p) x}

theorem LGame.isStrategy_setOfPred_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) :

@[simp]

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

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

IsDraw p x means that p draws x going first.

Equations

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

Instances For

@[simp]

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

@[simp]

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

theorem LGame.not_isDraw_iff {p : Player} {x : LGame} :

¬IsDraw p x ↔ IsWin p x ∨ IsLoss p x

inductive LGame.Outcome :

The three possible outcomes of a game.

win : Outcome
draw : Outcome
loss : Outcome

Instances For

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

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

Instances For

@[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) :

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

@[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)