Combinatorial games

In this file we construct the quotient of games IGame under equivalence, and prove that it forms an OrderedAddCommGroup. We take advantage of this structure to prove two particularly tedious theorems on IGame, namely IGame.mul_add_equiv and IGame.mul_assoc_equiv.

It might be tempting to write mk (x * y) as mk x * mk y, but the latter is not well-defined, as there exist x₁ ≈ x₂ and y₁ ≈ y₂ with x₁ * y₁ ≉ x₂ * y₂. See CombinatorialGames.Counterexamples.Multiplication for a proof.

def Game : Type (u + 1)

Games up to equivalence.

If x and y are combinatorial games (IGame), we say that x ≈ y when both x ≤ y and y ≤ x. Broadly, this means neither player has a preference in playing either game, as a component of a larger game. This is the standard meaning of x = y in the literature, though it is not a strict equality, e.g. {0, 1 | 0} and {1 | 0} are equivalent, but not identical as the former has an extra move for Left.

In particular, note that a Game has no well-defined notion of left and right options. This means you should prefer IGame when analyzing specific games.

Equations

• Game = Antisymmetrization IGame fun (x1 x2 : IGame) => x1 ≤ x2

def Game.mk (x : IGame) : Game

The quotient map from IGame into Game.

Equations

• Game.mk x = ⟦x⟧

theorem Game.mk_eq_mk {x y : IGame} : mk x = mk y ↔ x ≈ y

theorem Game.mk_eq {x y : IGame} : x ≈ y → mk x = mk y

Alias of the reverse direction of Game.mk_eq_mk.

theorem Game.ind {P : Game → Prop} (H : ∀ (y : IGame), P (mk y)) (x : Game) : P x

def Game.out (x : Game) : IGame

Choose an element of the equivalence class using the axiom of choice.

Equations

• x.out = Quotient.out x

@[simp]

theorem Game.out_eq (x : Game) : mk x.out = x

theorem Game.mk_out_equiv (x : IGame) : (mk x).out ≈ x

theorem Game.equiv_mk_out (x : IGame) : x ≈ (mk x).out

def Game.ofSets (s t : Set Game) [Small.{u, u + 1} ↑s] [Small.{u, u + 1} ↑t] : Game

Construct a Game from its left and right sets.

This is given notation {s | t}ᴳ, where the superscript G is to disambiguate from set builder notation, and from the analogous constructors on IGame and Surreal.

Note that although this function is well-defined, this function isn't injective, nor do equivalence classes in Game have a canonical representative.

Equations

• {s | t}ᴳ = Game.mk {Game.out '' s | Game.out '' t}ᴵ

def Game.«term{_|_}ᴳ» : Lean.ParserDescr

Construct a Game from its left and right sets.

This is given notation {s | t}ᴳ, where the superscript G is to disambiguate from set builder notation, and from the analogous constructors on IGame and Surreal.

Note that although this function is well-defined, this function isn't injective, nor do equivalence classes in Game have a canonical representative.

Equations

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

@[simp]

theorem Game.mk_ofSets (s t : Set IGame) [Small.{u, u + 1} ↑s] [Small.{u, u + 1} ↑t] : mk {s | t}ᴵ = {mk '' s | mk '' t}ᴳ

instance Game.instZero : Zero Game

Equations

• Game.instZero = { zero := Game.mk 0 }

instance Game.instOne : One Game

Equations

• Game.instOne = { one := Game.mk 1 }

instance Game.instAdd : Add Game

Equations

• Game.instAdd = { add := Quotient.map₂ HAdd.hAdd @IGame.add_congr }

instance Game.instNeg : Neg Game

Equations

• Game.instNeg = { neg := Quotient.map Neg.neg @IGame.neg_congr }

instance Game.instPartialOrder : PartialOrder Game

Equations

• Game.instPartialOrder = inferInstanceAs (PartialOrder (Antisymmetrization IGame fun (x1 x2 : IGame) => x1 ≤ x2))

instance Game.instInhabited : Inhabited Game

Equations

• Game.instInhabited = { default := 0 }

instance Game.instAddCommGroupWithOne : AddCommGroupWithOne Game

Equations

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

instance Game.instIsOrderedAddMonoid : IsOrderedAddMonoid Game

instance Game.instRatCast : RatCast Game

Equations

• Game.instRatCast = { ratCast := fun (q : ℚ) => Game.mk ↑q }

@[simp]

theorem Game.mk_zero : mk 0 = 0

@[simp]

theorem Game.mk_one : mk 1 = 1

@[simp]

theorem Game.mk_add (x y : IGame) : mk (x + y) = mk x + mk y

@[simp]

theorem Game.mk_neg (x : IGame) : mk (-x) = -mk x

@[simp]

theorem Game.mk_sub (x y : IGame) : mk (x - y) = mk x - mk y

theorem Game.mk_mulOption (x y a b : IGame) : mk (IGame.mulOption x y a b) = mk (a * y) + mk (x * b) - mk (a * b)

@[simp]

theorem Game.mk_le_mk {x y : IGame} : mk x ≤ mk y ↔ x ≤ y

@[simp]

theorem Game.mk_lt_mk {x y : IGame} : mk x < mk y ↔ x < y

@[simp]

theorem Game.mk_natCast (n : ℕ) : mk ↑n = ↑n

@[simp]

theorem Game.mk_intCast (n : ℤ) : mk ↑n = ↑n

@[simp]

theorem Game.mk_ratCast (q : ℚ) : mk ↑q = ↑q

@[simp]

theorem Game.ratCast_neg (q : ℚ) : ↑(-q) = -↑q

theorem Game.zero_def : 0 = {∅ | ∅}ᴳ

theorem Game.one_def : 1 = {{0} | ∅}ᴳ

instance Game.instZeroLEOneClass : ZeroLEOneClass Game

instance Game.instNeZeroOfNat : NeZero 1

instance Game.instNontrivial : Nontrivial Game

instance Game.instCharZero : CharZero Game

@[irreducible]

theorem Game.mk_mul_add (x y z : IGame) : mk (x * (y + z)) = mk (x * y) + mk (x * z)

theorem Game.mk_mul_sub (x y z : IGame) : mk (x * (y - z)) = mk (x * y) - mk (x * z)

theorem Game.mk_add_mul (x y z : IGame) : mk ((x + y) * z) = mk (x * z) + mk (y * z)

theorem Game.mk_sub_mul (x y z : IGame) : mk ((x - y) * z) = mk (x * z) - mk (y * z)

theorem Set.prod_image_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → γ) (s : Set α) (t : Set β) : (f '' s) ×ˢ t = (fun (x : α × β) => (f x.1, x.2)) '' s ×ˢ t

theorem Set.prod_image_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → γ) (s : Set α) (t : Set β) : t ×ˢ (f '' s) = (fun (x : β × α) => (x.1, f x.2)) '' t ×ˢ s

@[irreducible]

theorem Game.mk_mul_assoc (x y z : IGame) : mk (x * y * z) = mk (x * (y * z))

theorem IGame.sub_le_iff_le_add {x y z : IGame} : x - z ≤ y ↔ x ≤ y + z

theorem IGame.le_sub_iff_add_le {x y z : IGame} : x ≤ z - y ↔ x + y ≤ z

theorem IGame.sub_lt_iff_lt_add {x y z : IGame} : x - z < y ↔ x < y + z

theorem IGame.lt_sub_iff_add_lt {x y z : IGame} : x < z - y ↔ x + y < z

theorem IGame.sub_nonneg {x y : IGame} : 0 ≤ x - y ↔ y ≤ x

theorem IGame.sub_nonpos {x y : IGame} : x - y ≤ 0 ↔ x ≤ y

theorem IGame.sub_pos {x y : IGame} : 0 < x - y ↔ y < x

theorem IGame.sub_neg {x y : IGame} : x - y < 0 ↔ x < y

theorem IGame.mul_add_equiv (x y z : IGame) : x * (y + z) ≈ x * y + x * z

theorem IGame.mul_sub_equiv (x y z : IGame) : x * (y - z) ≈ x * y - x * z

theorem IGame.add_mul_equiv (x y z : IGame) : (x + y) * z ≈ x * z + y * z

theorem IGame.sub_mul_equiv (x y z : IGame) : (x - y) * z ≈ x * z - y * z

theorem IGame.mul_assoc_equiv (x y z : IGame) : x * y * z ≈ x * (y * z)

@[simp]

theorem IGame.natCast_le {m n : ℕ} : ↑m ≤ ↑n ↔ m ≤ n

@[simp]

theorem IGame.natCast_lt {m n : ℕ} : ↑m < ↑n ↔ m < n

theorem IGame.natCast_strictMono : StrictMono Nat.cast

instance IGame.instCharZero : CharZero IGame

@[simp]

theorem IGame.natCast_equiv {m n : ℕ} : ↑m ≈ ↑n ↔ m = n

@[simp]

theorem IGame.intCast_le {m n : ℤ} : ↑m ≤ ↑n ↔ m ≤ n

@[simp]

theorem IGame.intCast_lt {m n : ℤ} : ↑m < ↑n ↔ m < n

theorem IGame.intCast_strictMono : StrictMono Int.cast

@[simp]

theorem IGame.intCast_inj {m n : ℤ} : ↑m = ↑n ↔ m = n

@[simp]

theorem IGame.intCast_equiv {m n : ℤ} : ↑m ≈ ↑n ↔ m = n

theorem IGame.intCast_add_equiv (m n : ℤ) : ↑(m + n) ≈ ↑m + ↑n

theorem IGame.intCast_sub_equiv (m n : ℤ) : ↑(m - n) ≈ ↑m - ↑n

@[simp]

theorem IGame.zero_lt_intCast {n : ℤ} : 0 < ↑n ↔ 0 < n

@[simp]

theorem IGame.intCast_lt_zero {n : ℤ} : ↑n < 0 ↔ n < 0

@[simp]

theorem IGame.zero_le_intCast {n : ℤ} : 0 ≤ ↑n ↔ 0 ≤ n

@[simp]

theorem IGame.intCast_le_zero {n : ℤ} : ↑n ≤ 0 ↔ n ≤ 0