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.IsLeftWin :

IsLeftWin x means that left wins x going first.

intro (x y : LGame) : y ∈ x.leftMoves → y.IsRightLoss → x.IsLeftWin

Instances For

inductive LGame.IsRightLoss :

IsRightLoss x means that right loses x going first.

intro (x : LGame) : (∀ y ∈ x.rightMoves, y.IsLeftWin) → x.IsRightLoss

Instances For

inductive LGame.IsRightWin :

IsRightWin x means that right wins x going first.

intro (x y : LGame) : y ∈ x.rightMoves → y.IsLeftLoss → x.IsRightWin

Instances For

inductive LGame.IsLeftLoss :

IsLeftLoss x means that left loses x going first.

intro (x : LGame) : (∀ y ∈ x.leftMoves, y.IsRightWin) → x.IsLeftLoss

Instances For

theorem LGame.isLeftWin_iff_exists {x : LGame} :

x.IsLeftWin ↔ ∃ y ∈ x.leftMoves, y.IsRightLoss

theorem LGame.isRightWin_iff_exists {x : LGame} :

x.IsRightWin ↔ ∃ y ∈ x.rightMoves, y.IsLeftLoss

theorem LGame.isLeftLoss_iff_forall {x : LGame} :

x.IsLeftLoss ↔ ∀ y ∈ x.leftMoves, y.IsRightWin

theorem LGame.isRightLoss_iff_forall {x : LGame} :

x.IsRightLoss ↔ ∀ y ∈ x.rightMoves, y.IsLeftWin

theorem LGame.not_isLeftWin_iff_forall {x : LGame} :

¬x.IsLeftWin ↔ ∀ y ∈ x.leftMoves, ¬y.IsRightLoss

theorem LGame.not_isRightWin_iff_forall {x : LGame} :

¬x.IsRightWin ↔ ∀ y ∈ x.rightMoves, ¬y.IsLeftLoss

theorem LGame.not_isLeftLoss_iff_exists {x : LGame} :

¬x.IsLeftLoss ↔ ∃ y ∈ x.leftMoves, ¬y.IsRightWin

theorem LGame.not_isRightLoss_iff_exists {x : LGame} :

¬x.IsRightLoss ↔ ∃ y ∈ x.rightMoves, ¬y.IsLeftWin

def LGame.IsLeftStrategy (s : Set LGame) :

A surviving strategy for Left, going second.

This is a set of states, such that for every move Right makes, Left 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.IsLeftStrategy s = ∀ y ∈ s, ∀ z ∈ y.rightMoves, ∃ r ∈ z.leftMoves, r ∈ s

Instances For

def LGame.IsRightStrategy (s : Set LGame) :

A surviving strategy for Right, going second.

This is a set of states, such that for every move Left makes, Right 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.IsRightStrategy s = ∀ y ∈ s, ∀ z ∈ y.leftMoves, ∃ r ∈ z.rightMoves, r ∈ s

Instances For

@[simp]

theorem LGame.isLeftStrategy_neg {s : Set LGame} :

IsLeftStrategy (-s) ↔ IsRightStrategy s

@[simp]

theorem LGame.isRightStrategy_neg {s : Set LGame} :

IsRightStrategy (-s) ↔ IsLeftStrategy s

theorem LGame.IsLeftStrategy.iUnion {ι : Sort u_1} {s : ι → Set LGame} (h : ∀ (i : ι), IsLeftStrategy (s i)) :

IsLeftStrategy (⋃ (i : ι), s i)

theorem LGame.IsRightStrategy.iUnion {ι : Sort u_1} {s : ι → Set LGame} (h : ∀ (i : ι), IsRightStrategy (s i)) :

IsRightStrategy (⋃ (i : ι), s i)

theorem LGame.IsLeftStrategy.sUnion {S : Set (Set LGame)} (h : ∀ s ∈ S, IsLeftStrategy s) :

IsLeftStrategy (⋃₀ S)

theorem LGame.IsRightStrategy.sUnion {S : Set (Set LGame)} (h : ∀ s ∈ S, IsRightStrategy s) :

IsRightStrategy (⋃₀ S)

theorem LGame.isLeftStrategy_isRightLoss :

IsLeftStrategy {x : LGame | x.IsRightLoss}

theorem LGame.isRightStrategy_isLeftLoss :

IsRightStrategy {x : LGame | x.IsLeftLoss}

theorem LGame.isLeftStrategy_not_isRightWin :

IsLeftStrategy {x : LGame | ¬x.IsRightWin}

theorem LGame.isRightStrategy_not_isLeftWin :

IsRightStrategy {x : LGame | ¬x.IsLeftWin}

theorem LGame.not_isRightWin_iff_mem_leftStrategy {x : LGame} :

¬x.IsRightWin ↔ ∃ (s : Set LGame), x ∈ s ∧ IsLeftStrategy s

theorem LGame.not_isLeftWin_iff_mem_rightStrategy {x : LGame} :

¬x.IsLeftWin ↔ ∃ (s : Set LGame), x ∈ s ∧ IsRightStrategy s

theorem LGame.not_isLeftWin_and_isLeftLoss {x : LGame} :

¬(x.IsLeftWin ∧ x.IsLeftLoss)

theorem LGame.not_isRightWin_and_isRightLoss {x : LGame} :

¬(x.IsRightWin ∧ x.IsRightLoss)

def LGame.IsLeftDraw (x : LGame) :

IsLeftDraw x means that left draws x going first.

Equations

x.IsLeftDraw = (¬x.IsLeftWin ∧ ¬x.IsLeftLoss)

Instances For

def LGame.IsRightDraw (x : LGame) :

IsRightDraw x means that right draws x going first.

Equations

x.IsRightDraw = (¬x.IsRightWin ∧ ¬x.IsRightLoss)

Instances For

inductive LGame.Outcome :

The three possible outcomes of a game.

win : Outcome
draw : Outcome
loss : Outcome

Instances For

noncomputable def LGame.leftOutcome (x : LGame) :

leftOutcome x is the outcome of x with left going first.

Equations

x.leftOutcome = if x.IsLeftWin then LGame.Outcome.win else if x.IsLeftLoss then LGame.Outcome.loss else LGame.Outcome.draw

Instances For

noncomputable def LGame.rightOutcome (x : LGame) :

rightOutcome x is the outcome of x with right going first.

Equations

x.rightOutcome = if x.IsRightWin then LGame.Outcome.win else if x.IsRightLoss then LGame.Outcome.loss else LGame.Outcome.draw

Instances For

theorem LGame.leftOutcome_eq_win_iff {x : LGame} :

x.leftOutcome = Outcome.win ↔ x.IsLeftWin

theorem LGame.rightOutcome_eq_win_iff {x : LGame} :

x.rightOutcome = Outcome.win ↔ x.IsRightWin

theorem LGame.leftOutcome_eq_loss_iff {x : LGame} :

x.leftOutcome = Outcome.loss ↔ x.IsLeftLoss

theorem LGame.rightOutcome_eq_loss_iff {x : LGame} :

x.rightOutcome = Outcome.loss ↔ x.IsRightLoss

theorem LGame.leftOutcome_eq_draw_iff {x : LGame} :

x.leftOutcome = Outcome.draw ↔ x.IsLeftDraw

theorem LGame.rightOutcome_eq_draw_iff {x : LGame} :

x.rightOutcome = Outcome.draw ↔ x.IsRightDraw

theorem LGame.not_isLeftDraw_of_acc_comp {x : LGame} (h : Acc (fun (z x : LGame) => ∃ y ∈ x.leftMoves, z ∈ y.rightMoves) x) :

If there is no infinite play starting by from x with right going second, then x cannot end in a draw with right going second.

theorem LGame.not_isRightDraw_of_acc_comp {x : LGame} (h : Acc (fun (z x : LGame) => ∃ y ∈ x.rightMoves, z ∈ y.leftMoves) x) :

¬x.IsRightDraw

If there is no infinite play starting from x with right going first, then x cannot end in a draw with right going first.

theorem LGame.not_isLeftDraw_of_acc_isOption {x : LGame} (h : Acc IsOption x) :

theorem LGame.not_isRightDraw_of_acc_isOption {x : LGame} (h : Acc IsOption x) :

¬x.IsRightDraw

theorem IGame.not_isLeftDraw (x : IGame) :

¬(toLGame x).IsLeftDraw

theorem IGame.not_isRightDraw (x : IGame) :

¬(toLGame x).IsRightDraw

theorem IGame.isLeftWin_iff_zero_lf {x : IGame} :

(toLGame x).IsLeftWin ↔ ¬x ≤ 0

theorem IGame.isLeftLoss_iff_le_zero {x : IGame} :

(toLGame x).IsLeftLoss ↔ x ≤ 0

theorem IGame.isRightWin_iff_lf_zero {x : IGame} :

(toLGame x).IsRightWin ↔ ¬0 ≤ x

theorem IGame.isRightLoss_iff_zero_le {x : IGame} :

(toLGame x).IsRightLoss ↔ 0 ≤ x

theorem IGame.fuzzy_zero_iff_and {x : IGame} :

x ‖ 0 ↔ (toLGame x).IsLeftWin ∧ (toLGame x).IsRightWin

theorem IGame.equiv_zero_iff_and {x : IGame} :

x ≈ 0 ↔ (toLGame x).IsLeftLoss ∧ (toLGame x).IsRightLoss

theorem IGame.lt_zero_iff_and {x : IGame} :

x < 0 ↔ (toLGame x).IsLeftLoss ∧ (toLGame x).IsRightWin

theorem IGame.zero_lt_iff_and {x : IGame} :

0 < x ↔ (toLGame x).IsLeftWin ∧ (toLGame x).IsRightLoss