Classes of games

This file collects multiple basic classes of games, so as to make them available on most files. We develop their theory elsewhere.

Dicotic games

A game is dicotic when every non-zero subposition has both left and right moves. The Lawnmower theorem (proven in CombinatorialGames.Game.Small) shows that every dicotic game is small.

Impartial games

We define an impartial game as one where every subposition is equivalent to its negative. This is a weaker definition than that found in the literature (which requires equality, rather than equivalence), but this is still strong enough to prove the Sprague--Grundy theorem, as well as closure under the basic arithmetic operations of multiplication and division.

Numeric games

A game is Numeric if all the Left options are strictly smaller than all the Right options, and all those options are themselves numeric. In terms of combinatorial games, the numeric games have "frozen"; you can only make your position worse by playing, and Left is some definite "number" of moves ahead (or behind) Right.

Short games

A combinatorial game is Short if it has only finitely many subpositions. In particular, this means there is a finite set of moves at every point.

We historically defined Short x as data, which we then used to enable some degree of computation on combinatorial games. This functionality is now implemented through the game_cmp tactic instead.

Dicotic games

class IGame.Dicotic (x : IGame) : Prop

A game x is dicotic if both players can move from every nonempty subposition of x.

• of_DicoticAux :: (
• out : IGame.DicoticAux✝ x
• )

theorem IGame.dicotic_iff_aux (x : IGame) : x.Dicotic ↔ IGame.DicoticAux✝ x

theorem IGame.dicotic_def {x : IGame} : x.Dicotic ↔ (moves left x = ∅ ↔ moves right x = ∅) ∧ ∀ (p : Player), ∀ l ∈ moves p x, l.Dicotic

theorem IGame.Dicotic.mk {x : IGame} (h₁ : moves left x = ∅ ↔ moves right x = ∅) (h₂ : ∀ (p : Player), ∀ y ∈ moves p x, y.Dicotic) : x.Dicotic

theorem IGame.Dicotic.eq_zero_iff {x : IGame} [hx : x.Dicotic] : x = 0 ↔ ∃ (p : Player), moves p x = ∅

theorem IGame.Dicotic.ne_zero_iff {x : IGame} [x.Dicotic] : x ≠ 0 ↔ ∀ (p : Player), moves p x ≠ ∅

theorem IGame.Dicotic.moves_eq_empty_iff {x : IGame} [hx : x.Dicotic] (p q : Player) : moves p x = ∅ ↔ moves q x = ∅

theorem IGame.Dicotic.of_mem_moves {x y : IGame} {p : Player} [hx : x.Dicotic] (h : y ∈ moves p x) : y.Dicotic

def IGame.Dicotic.tacticDicotic : Lean.ParserDescr

dicotic eagerly adds all possible Dicotic hypotheses.

Equations

• IGame.Dicotic.tacticDicotic = Lean.ParserDescr.node `IGame.Dicotic.tacticDicotic 1024 (Lean.ParserDescr.nonReservedSymbol "dicotic" false)

@[simp]

instance IGame.Dicotic.zero : Dicotic 0

@[irreducible]

instance IGame.Dicotic.neg (x : IGame) [x.Dicotic] : (-x).Dicotic

Impartial games

class IGame.Impartial (x : IGame) : Prop

An impartial game is one that's equivalent to its negative, such that each left and right move is also impartial.

Note that this is a slightly more general definition than the one that's usually in the literature, as we don't require x = -x. Despite this, the Sprague-Grundy theorem still holds: see IGame.equiv_nim_grundyValue.

In such a game, both players have the same payoffs at any subposition.

• of_ImpartialAux :: (
• out : IGame.ImpartialAux✝ x
• )

theorem IGame.impartial_iff_aux (x : IGame) : x.Impartial ↔ IGame.ImpartialAux✝ x

theorem IGame.impartial_def {x : IGame} : x.Impartial ↔ -x ≈ x ∧ ∀ (p : Player), ∀ y ∈ moves p x, y.Impartial

theorem IGame.Impartial.mk {x : IGame} (h₁ : -x ≈ x) (h₂ : ∀ (p : Player), ∀ y ∈ moves p x, y.Impartial) : x.Impartial

@[simp]

theorem IGame.Impartial.neg_equiv (x : IGame) [hx : x.Impartial] : -x ≈ x

@[simp]

theorem IGame.Impartial.equiv_neg (x : IGame) [hx : x.Impartial] : x ≈ -x

theorem IGame.Impartial.sub_equiv (x y : IGame) [hy : y.Impartial] : x - y ≈ x + y

theorem IGame.Impartial.of_mem_moves {p : Player} {x y : IGame} [h : x.Impartial] : y ∈ moves p x → y.Impartial

def IGame.Impartial.tacticImpartial : Lean.ParserDescr

impartial eagerly adds all possible Impartial hypotheses.

Equations

• IGame.Impartial.tacticImpartial = Lean.ParserDescr.node `IGame.Impartial.tacticImpartial 1024 (Lean.ParserDescr.nonReservedSymbol "impartial" false)

@[simp]

instance IGame.Impartial.zero : Impartial 0

@[irreducible]

instance IGame.Impartial.neg (x : IGame) [x.Impartial] : (-x).Impartial

@[irreducible]

instance IGame.Impartial.add (x y : IGame) [x.Impartial] [y.Impartial] : (x + y).Impartial

instance IGame.Impartial.sub (x y : IGame) [x.Impartial] [y.Impartial] : (x - y).Impartial

theorem IGame.Impartial.le_comm {x y : IGame} [x.Impartial] [y.Impartial] : x ≤ y ↔ y ≤ x

The product instance is proven in Game.Impartial.Grundy.

@[simp]

theorem IGame.Impartial.not_lt (x y : IGame) [hx : x.Impartial] [hy : y.Impartial] : ¬x < y

theorem IGame.Impartial.equiv_or_fuzzy (x y : IGame) [hx : x.Impartial] [hy : y.Impartial] : x ≈ y ∨ x ‖ y

By setting y = 0, we find that in an impartial game, either the first player always wins, or the second player always wins.

@[simp]

theorem IGame.Impartial.not_equiv_iff {x y : IGame} [hx : x.Impartial] [hy : y.Impartial] : ¬x ≈ y ↔ x ‖ y

@[simp]

theorem IGame.Impartial.not_fuzzy_iff {x y : IGame} [hx : x.Impartial] [hy : y.Impartial] : ¬x ‖ y ↔ x ≈ y

@[simp]

theorem IGame.Impartial.le_iff_equiv {x y : IGame} [hx : x.Impartial] [hy : y.Impartial] : x ≤ y ↔ x ≈ y

theorem IGame.Impartial.ge_iff_equiv {x y : IGame} [hx : x.Impartial] [hy : y.Impartial] : y ≤ x ↔ x ≈ y

theorem IGame.Impartial.lf_iff_fuzzy {x y : IGame} [hx : x.Impartial] [hy : y.Impartial] : ¬y ≤ x ↔ x ‖ y

theorem IGame.Impartial.gf_iff_fuzzy {x y : IGame} [hx : x.Impartial] [hy : y.Impartial] : ¬x ≤ y ↔ x ‖ y

theorem IGame.Impartial.fuzzy_of_mem_moves {x : IGame} [hx : x.Impartial] {y : IGame} {p : Player} (hy : y ∈ moves p x) : y ‖ x

theorem IGame.Impartial.equiv_iff_forall_fuzzy {x y : IGame} [hx : x.Impartial] [hy : y.Impartial] (p : Player) : x ≈ y ↔ (∀ z ∈ moves p x, z ‖ y) ∧ ∀ z ∈ moves (-p) y, x ‖ z

theorem IGame.Impartial.fuzzy_iff_exists_equiv {x y : IGame} [hx : x.Impartial] [hy : y.Impartial] (p : Player) : x ‖ y ↔ (∃ z ∈ moves p x, z ≈ y) ∨ ∃ z ∈ moves (-p) y, x ≈ z

theorem IGame.Impartial.equiv_zero {x : IGame} [hx : x.Impartial] (p : Player) : x ≈ 0 ↔ ∀ y ∈ moves p x, y ‖ 0

theorem IGame.Impartial.fuzzy_zero {x : IGame} [hx : x.Impartial] (p : Player) : x ‖ 0 ↔ ∃ y ∈ moves p x, y ≈ 0

theorem IGame.Impartial.fuzzy_zero_of_forall_exists {x : IGame} [hx : x.Impartial] {p : Player} {y : IGame} (hy : y ∈ moves p x) (H : ∀ z ∈ moves p y, ∃ w ∈ moves p x, z ≈ w) : x ‖ 0

A strategy stealing argument. If there's a move in x, such that any immediate move could have also been reached in the first turn, then x is won by the first player.

Numeric games

class IGame.Numeric (x : IGame) : Prop

A game !{s | t} is numeric if everything in s is less than everything in t, and all the elements of these sets are also numeric.

The Surreal numbers are built as the quotient of numeric games under equivalence.

• of_NumericAux :: (
• out : IGame.NumericAux✝ x
• )

theorem IGame.numeric_iff_aux (x : IGame) : x.Numeric ↔ IGame.NumericAux✝ x

theorem IGame.numeric_def {x : IGame} : x.Numeric ↔ (∀ y ∈ moves left x, ∀ z ∈ moves right x, y < z) ∧ ∀ (p : Player), ∀ y ∈ moves p x, y.Numeric

theorem IGame.Numeric.mk {x : IGame} (h₁ : ∀ y ∈ moves left x, ∀ z ∈ moves right x, y < z) (h₂ : ∀ (p : Player), ∀ y ∈ moves p x, y.Numeric) : x.Numeric

theorem IGame.Numeric.left_lt_right {x y z : IGame} [h : x.Numeric] (hy : y ∈ moves left x) (hz : z ∈ moves right x) : y < z

theorem IGame.Numeric.of_mem_moves {x y : IGame} {p : Player} [h : x.Numeric] (hy : y ∈ moves p x) : y.Numeric

def IGame.Numeric.tacticNumeric : Lean.ParserDescr

numeric eagerly adds all possible Numeric hypotheses.

Equations

• IGame.Numeric.tacticNumeric = Lean.ParserDescr.node `IGame.Numeric.tacticNumeric 1024 (Lean.ParserDescr.nonReservedSymbol "numeric" false)

theorem IGame.Numeric.subposition {x y : IGame} [x.Numeric] (h : y.Subposition x) : y.Numeric

@[simp]

instance IGame.Numeric.zero : Numeric 0

@[simp]

instance IGame.Numeric.one : Numeric 1

instance IGame.Numeric.subtype (x : Subtype Numeric) : (↑x).Numeric

instance IGame.Numeric.moves {x : IGame} [x.Numeric] {p : Player} (y : ↑(moves p x)) : (↑y).Numeric

@[irreducible]

theorem IGame.Numeric.le_of_not_le {x y : IGame} [x.Numeric] [y.Numeric] : ¬x ≤ y → y ≤ x

theorem IGame.Numeric.le_total (x y : IGame) [x.Numeric] [y.Numeric] : x ≤ y ∨ y ≤ x

theorem IGame.Numeric.lt_of_not_ge {x y : IGame} [x.Numeric] [y.Numeric] (h : ¬x ≤ y) : y < x

@[simp]

theorem IGame.Numeric.not_le {x y : IGame} [x.Numeric] [y.Numeric] : ¬x ≤ y ↔ y < x

@[simp]

theorem IGame.Numeric.not_lt {x y : IGame} [x.Numeric] [y.Numeric] : ¬x < y ↔ y ≤ x

theorem IGame.Numeric.le_or_gt (x y : IGame) [x.Numeric] [y.Numeric] : x ≤ y ∨ y < x

theorem IGame.Numeric.lt_or_ge (x y : IGame) [x.Numeric] [y.Numeric] : x < y ∨ y ≤ x

theorem IGame.Numeric.not_fuzzy (x y : IGame) [x.Numeric] [y.Numeric] : ¬x ‖ y

theorem IGame.Numeric.lt_or_equiv_or_gt (x y : IGame) [x.Numeric] [y.Numeric] : x < y ∨ x ≈ y ∨ y < x

theorem IGame.Numeric.mk_of_lf {x : IGame} (h₁ : ∀ y ∈ moves left x, ∀ z ∈ moves right x, ¬z ≤ y) (h₂ : ∀ (p : Player), ∀ y ∈ moves p x, y.Numeric) : x.Numeric

To prove a game is numeric, it suffices to show the left options are less or fuzzy to the right options.

theorem IGame.Numeric.le_iff_forall_lt {x y : IGame} [x.Numeric] [y.Numeric] : x ≤ y ↔ (∀ z ∈ moves left x, z < y) ∧ ∀ z ∈ moves right y, x < z

theorem IGame.Numeric.lt_iff_exists_le {x y : IGame} [x.Numeric] [y.Numeric] : x < y ↔ (∃ z ∈ moves left y, x ≤ z) ∨ ∃ z ∈ moves right x, z ≤ y

theorem IGame.Numeric.left_lt {x y : IGame} [x.Numeric] (h : y ∈ moves left x) : y < x

theorem IGame.Numeric.lt_right {x y : IGame} [x.Numeric] (h : y ∈ moves right x) : x < y

@[irreducible]

instance IGame.Numeric.neg (x : IGame) [x.Numeric] : (-x).Numeric

@[simp]

theorem IGame.Numeric.neg_iff {x : IGame} : (-x).Numeric ↔ x.Numeric

@[irreducible]

instance IGame.Numeric.add (x y : IGame) [x.Numeric] [y.Numeric] : (x + y).Numeric

instance IGame.Numeric.sub (x y : IGame) [x.Numeric] [y.Numeric] : (x - y).Numeric

instance IGame.Numeric.natCast (n : ℕ) : (↑n).Numeric

instance IGame.Numeric.ofNat (n : ℕ) [n.AtLeastTwo] : (OfNat.ofNat n).Numeric

instance IGame.Numeric.intCast (n : ℤ) : (↑n).Numeric

Short games

class IGame.Short (x : IGame) : Prop

A short game is one with finitely many subpositions. That is, the left and right sets are finite, and all of the games in them are short as well.

• of_shortAux :: (
• out : IGame.ShortAux✝ x
• )

theorem IGame.short_iff_aux (x : IGame) : x.Short ↔ IGame.ShortAux✝ x

theorem IGame.short_def {x : IGame} : x.Short ↔ ∀ (p : Player), (moves p x).Finite ∧ ∀ y ∈ moves p x, y.Short

theorem IGame.Short.mk {x : IGame} : (∀ (p : Player), (moves p x).Finite ∧ ∀ y ∈ moves p x, y.Short) → x.Short

Alias of the reverse direction of IGame.short_def.

theorem IGame.Short.finite_moves (p : Player) (x : IGame) [h : x.Short] : (moves p x).Finite

instance IGame.Short.instFiniteElemMoves (p : Player) (x : IGame) [x.Short] : Finite ↑(moves p x)

theorem IGame.Short.of_mem_moves {x y : IGame} [h : x.Short] {p : Player} (hy : y ∈ moves p x) : y.Short

def IGame.Short.tacticShort : Lean.ParserDescr

short eagerly adds all possible Short hypotheses.

Equations

• IGame.Short.tacticShort = Lean.ParserDescr.node `IGame.Short.tacticShort 1024 (Lean.ParserDescr.nonReservedSymbol "short" false)

theorem IGame.Short.subposition {y x : IGame} [x.Short] (h : y.Subposition x) : y.Short

theorem IGame.Short.finite_setOf_subposition (x : IGame) [x.Short] : {y : IGame | y.Subposition x}.Finite

instance IGame.Short.instFiniteSubtypeSubposition (x : IGame) [x.Short] : Finite { y : IGame // y.Subposition x }

@[irreducible]

theorem IGame.short_iff_finite_setOf_subposition {x : IGame} : x.Short ↔ {y : IGame | y.Subposition x}.Finite

@[simp]

instance IGame.Short.zero : Short 0

@[simp]

instance IGame.Short.one : Short 1

@[irreducible]

instance IGame.Short.neg (x : IGame) [x.Short] : (-x).Short

@[simp]

theorem IGame.Short.neg_iff {x : IGame} : (-x).Short ↔ x.Short

@[irreducible]

instance IGame.Short.add (x y : IGame) [x.Short] [y.Short] : (x + y).Short

instance IGame.Short.sub (x y : IGame) [x.Short] [y.Short] : (x - y).Short

instance IGame.Short.natCast (n : ℕ) : (↑n).Short

instance IGame.Short.ofNat (n : ℕ) [n.AtLeastTwo] : (OfNat.ofNat n).Short

instance IGame.Short.intCast (n : ℤ) : (↑n).Short

@[irreducible]

instance IGame.Short.mul (x y : IGame) [x.Short] [y.Short] : (x * y).Short

instance IGame.Short.mulOption (x y a b : IGame) [x.Short] [y.Short] [a.Short] [b.Short] : (mulOption x y a b).Short