Combinatorial (pre-)games

The basic theory of combinatorial games, following Conway's book On Numbers and Games.

In ZFC, games are built inductively out of two other sets of games, representing the options for two players Left and Right. In Lean, we instead define the type of games IGame as arising from two Small sets of games, with notation !{s | t}. A u-small type α : Type v is one that is equivalent to some β : Type u, and the distinction between small and large types in a given universe closely mimics the ZFC distinction between sets and proper classes.

This definition requires some amount of setup, since Lean's inductive types aren't powerful enough to express this on their own. See the docstring on GameFunctor for more information.

We are also interested in further quotients of IGame. The quotient of games under equivalence x ≈ y ↔ x ≤ y ∧ y ≤ x, which in the literature is often what is meant by a "combinatorial game", is defined as Game in CombinatorialGames.Game.Basic. The surreal numbers Surreal are defined as a quotient (of a subtype) of games in CombinatorialGames.Surreal.Basic.

Conway induction

Most constructions within game theory, and as such, many proofs within it, are done by structural induction. Structural induction on games is sometimes called "Conway induction".

The most straightforward way to employ Conway induction is by using the termination checker, with the auxiliary igame_wf tactic. This uses solve_by_elim to search the context for proofs of the form y ∈ xᴸ or y ∈ xᴿ, which prove termination. Alternatively, you can use the explicit recursion principles IGame.ofSetsRecOn or IGame.moveRecOn.

Order properties

Pregames have both a ≤ and a < relation, satisfying the properties of a Preorder. The relation 0 < x means that x can always be won by Left, while 0 ≤ x means that x can be won by Left as the second player. Likewise, x < 0 means that x can always be won by Right, while x ≤ 0 means that x can be won by Right as the second player.

Note that we don't actually prove these characterizations. Indeed, in Conway's setup, combinatorial game theory can be done entirely without the concept of a strategy. For instance, IGame.zero_le implies that if 0 ≤ x, then any move by Right satisfies ¬ x ≤ 0, and IGame.zero_lf implies that if ¬ x ≤ 0, then some move by Left satisfies 0 ≤ x. The strategy is thus already encoded within these game relations.

For convenience, we define notation x ⧏ y (pronounced "less or fuzzy") for ¬ y ≤ x, notation x ‖ y for ¬ x ≤ y ∧ ¬ y ≤ x, and notation x ≈ y for x ≤ y ∧ y ≤ x.

You can prove most (simple) inequalities on concrete games through the game_cmp tactic, which repeatedly unfolds the definition of ≤ and applies simp until it solves the goal.

Algebraic structures

Most of the usual arithmetic operations can be defined for games. Addition is defined for x = !{s₁ | t₁} and y = !{s₂ | t₂} by x + y = !{s₁ + y, x + s₂ | t₁ + y, x + t₂}. Negation is defined by -!{s | t} = !{-t | -s}.

The order structures interact in the expected way with arithmetic. In particular, Game is an OrderedAddCommGroup. Meanwhile, IGame satisfies the slightly weaker axioms of a SubtractionCommMonoid, since the equation x - x = 0 is only true up to equivalence.

Game moves

@[irreducible]

def IGame : Type (u + 1)

Well-founded games up to identity.

IGame uses the set-theoretic notion of equality on games, meaning that two IGames are equal exactly when their left and right sets of options are.

This is not the same equivalence as used broadly in combinatorial game theory literature, as a game like {0, 1 | 0} is not identical to {1 | 0}, despite being equivalent. However, many theorems can be proven over the 'identical' equivalence relation, and the literature may occasionally specifically use the 'identical' equivalence relation for this reason. The quotient Game of games up to equality is defined in CombinatorialGames.Game.Basic.

More precisely, IGame is the inductive type for the single constructor

  | ofSets (s t : Set IGame.{u}) [Small.{u} s] [Small.{u} t] : IGame.{u}

(though for technical reasons it's not literally defined as such). A consequence of this is that there is no infinite line of play. See LGame for a definition of loopy games.

Equations

• IGame = QPF.Fix GameFunctor

instance IGame.instOfSetsTrue : OfSets IGame fun (x : Player → Set IGame) => True

Construct an IGame from its left and right sets.

This function is regrettably noncomputable. Among other issues, sets simply do not carry data in Lean. To perform computations on IGame we can instead make use of the game_cmp tactic.

Equations

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

def IGame.moves (p : Player) (x : IGame) : Set IGame

The set of moves of the game.

Equations

• IGame.moves p x = ↑(QPF.Fix.dest x) p

def IGame.«term_ᴸ» : Lean.TrailingParserDescr

The set of left moves of the game.

Equations

• IGame.«term_ᴸ» = Lean.ParserDescr.trailingNode `IGame.«term_ᴸ» 1024 1024 (Lean.ParserDescr.symbol "ᴸ")

def IGame.«term_ᴿ» : Lean.TrailingParserDescr

The set of right moves of the game.

Equations

• IGame.«term_ᴿ» = Lean.ParserDescr.trailingNode `IGame.«term_ᴿ» 1024 1024 (Lean.ParserDescr.symbol "ᴿ")

instance IGame.instSmallElemMoves (p : Player) (x : IGame) : Small.{u, u + 1} ↑(moves p x)

@[simp]

theorem IGame.moves_ofSets (p : Player) (st : Player → Set IGame) [Small.{u, u + 1} ↑(st left)] [Small.{u, u + 1} ↑(st right)] : moves p !{st} = st p

@[simp]

theorem IGame.ofSets_moves (x : IGame) : !{fun (p : Player) => moves p x} = x

theorem IGame.leftMoves_ofSets (s t : Set IGame) [Small.{u, u + 1} ↑s] [Small.{u, u + 1} ↑t] : moves left !{s | t} = s

theorem IGame.rightMoves_ofSets (s t : Set IGame) [Small.{u, u + 1} ↑s] [Small.{u, u + 1} ↑t] : moves right !{s | t} = t

@[simp]

theorem IGame.ofSets_leftMoves_rightMoves (x : IGame) : !{moves left x | moves right x} = x

theorem IGame.ext {x y : IGame} (h : ∀ (p : Player), moves p x = moves p y) : x = y

Two IGames are equal when their move sets are.

For the weaker but more common notion of equivalence where x = y if x ≤ y and y ≤ x, use Game.

theorem IGame.ext_iff {x y : IGame} : x = y ↔ ∀ (p : Player), moves p x = moves p y

@[simp]

theorem IGame.ofSets_inj' {st₁ st₂ : Player → Set IGame} [Small.{u_1, u_1 + 1} ↑(st₁ left)] [Small.{u_1, u_1 + 1} ↑(st₁ right)] [Small.{u_1, u_1 + 1} ↑(st₂ left)] [Small.{u_1, u_1 + 1} ↑(st₂ right)] : !{st₁} = !{st₂} ↔ st₁ = st₂

theorem IGame.ofSets_inj {s₁ s₂ t₁ t₂ : Set IGame} [Small.{u_1, u_1 + 1} ↑s₁] [Small.{u_1, u_1 + 1} ↑s₂] [Small.{u_1, u_1 + 1} ↑t₁] [Small.{u_1, u_1 + 1} ↑t₂] : !{s₁ | t₁} = !{s₂ | t₂} ↔ s₁ = s₂ ∧ t₁ = t₂

def IGame.IsOption (x y : IGame) : Prop

IsOption x y means that x is either a left or a right move for y.

Equations

• x.IsOption y = (x ∈ ⋃ (p : Player), IGame.moves p y)

theorem IGame.isOption_iff_mem_union {x y : IGame} : x.IsOption y ↔ x ∈ moves left y ∪ moves right y

theorem IGame.IsOption.of_mem_moves {p : Player} {x y : IGame} (h : x ∈ moves p y) : x.IsOption y

instance IGame.instSmallSubtypeIsOption (x : IGame) : Small.{u, u + 1} { y : IGame // y.IsOption x }

theorem IGame.isOption_wf : WellFounded IsOption

instance IGame.instIsWellFoundedIsOption : IsWellFounded IGame IsOption

theorem IGame.IsOption.irrefl (x : IGame) : ¬x.IsOption x

theorem IGame.self_notMem_moves (p : Player) (x : IGame) : x ∉ moves p x

def IGame.moveRecOn {motive : IGame → Sort u_1} (x : IGame) (mk : (x : IGame) → ((p : Player) → (y : IGame) → y ∈ moves p x → motive y) → motive x) : motive x

Conway recursion: build data for a game by recursively building it on its left and right sets. You rarely need to use this explicitly, as the termination checker will handle things for you.

See ofSetsRecOn for an alternate form.

Equations

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

theorem IGame.moveRecOn_eq {motive : IGame → Sort u_1} (x : IGame) (mk : (x : IGame) → ((p : Player) → (y : IGame) → y ∈ moves p x → motive y) → motive x) : moveRecOn x mk = mk x fun (x_1 : Player) (y : IGame) (x : y ∈ moves x_1 x) => moveRecOn y mk

def IGame.ofSetsRecOn {motive : IGame → Sort u_1} (x : IGame) (mk : (s t : Set IGame) → [inst : Small.{u, u + 1} ↑s] → [inst_1 : Small.{u, u + 1} ↑t] → ((x : IGame) → x ∈ s → motive x) → ((x : IGame) → x ∈ t → motive x) → motive !{s | t}) : motive x

Conway recursion: build data for a game by recursively building it on its left and right sets. You rarely need to use this explicitly, as the termination checker will handle things for you.

See moveRecOn for an alternate form.

Equations

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

@[simp]

theorem IGame.ofSetsRecOn_ofSets {motive : IGame → Sort u_1} (s t : Set IGame) [Small.{u, u + 1} ↑s] [Small.{u, u + 1} ↑t] (mk : (s t : Set IGame) → [inst : Small.{u, u + 1} ↑s] → [inst_1 : Small.{u, u + 1} ↑t] → ((x : IGame) → x ∈ s → motive x) → ((x : IGame) → x ∈ t → motive x) → motive !{s | t}) : ofSetsRecOn !{s | t} mk = mk s t (fun (y : IGame) (x : y ∈ s) => ofSetsRecOn y mk) fun (y : IGame) (x : y ∈ t) => ofSetsRecOn y mk

def IGame.Subposition : IGame → IGame → Prop

A (proper) subposition is any game in the transitive closure of IsOption.

Equations

• IGame.Subposition = Relation.TransGen IGame.IsOption

theorem IGame.Subposition.of_mem_moves {p : Player} {x y : IGame} (h : x ∈ moves p y) : x.Subposition y

theorem IGame.Subposition.trans {x y z : IGame} (h₁ : x.Subposition y) (h₂ : y.Subposition z) : x.Subposition z

instance IGame.instSmallSubtypeSubposition (x : IGame) : Small.{u, u + 1} { y : IGame // y.Subposition x }

instance IGame.instIsTransSubposition : IsTrans IGame Subposition

instance IGame.instIsWellFoundedSubposition : IsWellFounded IGame Subposition

instance IGame.instWellFoundedRelation : WellFoundedRelation IGame

Equations

• IGame.instWellFoundedRelation = { rel := IGame.Subposition, wf := ⋯ }

def IGame.tacticIgame_wf : Lean.ParserDescr

Discharges proof obligations of the form ⊢ Subposition .. arising in termination proofs of definitions using well-founded recursion on IGame.

Equations

• IGame.tacticIgame_wf = Lean.ParserDescr.node `IGame.tacticIgame_wf 1024 (Lean.ParserDescr.nonReservedSymbol "igame_wf" false)

Basic games

instance IGame.instZero : Zero IGame

The game 0 = !{∅ | ∅}.

Equations

• IGame.instZero = { zero := !{fun (x : Player) => ∅} }

theorem IGame.zero_def : 0 = !{fun (x : Player) => ∅}

@[simp]

theorem IGame.moves_zero (p : Player) : moves p 0 = ∅

instance IGame.instInhabited : Inhabited IGame

Equations

• IGame.instInhabited = { default := 0 }

instance IGame.instOne : One IGame

The game 1 = !{{0} | ∅}.

Equations

• IGame.instOne = { one := !{{0} | ∅} }

theorem IGame.one_def : 1 = !{{0} | ∅}

@[simp]

theorem IGame.leftMoves_one : moves left 1 = {0}

@[simp]

theorem IGame.rightMoves_one : moves right 1 = ∅

Order relations

instance IGame.instLE : LE IGame

The less or equal relation on games.

If 0 ≤ x, then Left can win x as the second player. x ≤ y means that 0 ≤ y - x.

Equations

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

def IGame.«term_⧏_» : Lean.TrailingParserDescr

The less or fuzzy relation on games. x ⧏ y is notation for ¬ y ≤ x.

If 0 ⧏ x, then Left can win x as the first player. x ⧏ y means that 0 ⧏ y - x.

Conventions for notations in identifiers:

• The recommended spelling of ⧏ in identifiers is lf.

Equations

• IGame.«term_⧏_» = Lean.ParserDescr.trailingNode `IGame.«term_⧏_» 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⧏ ") (Lean.ParserDescr.cat `term 50))

theorem IGame.le_iff_forall_lf {x y : IGame} : x ≤ y ↔ (∀ z ∈ moves left x, ¬y ≤ z) ∧ ∀ z ∈ moves right y, ¬z ≤ x

Definition of x ≤ y on games, in terms of ⧏.

theorem IGame.lf_iff_exists_le {x y : IGame} : ¬y ≤ x ↔ (∃ z ∈ moves left y, x ≤ z) ∨ ∃ z ∈ moves right x, z ≤ y

Definition of x ⧏ y on games, in terms of ≤.

theorem IGame.zero_le {x : IGame} : 0 ≤ x ↔ ∀ y ∈ moves right x, ¬y ≤ 0

The definition of 0 ≤ x on games, in terms of 0 ⧏.

theorem IGame.le_zero {x : IGame} : x ≤ 0 ↔ ∀ y ∈ moves left x, ¬0 ≤ y

The definition of x ≤ 0 on games, in terms of ⧏ 0.

theorem IGame.zero_lf {x : IGame} : ¬x ≤ 0 ↔ ∃ y ∈ moves left x, 0 ≤ y

The definition of 0 ⧏ x on games, in terms of 0 ≤.

theorem IGame.lf_zero {x : IGame} : ¬0 ≤ x ↔ ∃ y ∈ moves right x, y ≤ 0

The definition of x ⧏ 0 on games, in terms of ≤ 0.

theorem IGame.le_def {x y : IGame} : x ≤ y ↔ (∀ a ∈ moves left x, (∃ b ∈ moves left y, a ≤ b) ∨ ∃ b ∈ moves right a, b ≤ y) ∧ ∀ a ∈ moves right y, (∃ b ∈ moves left a, x ≤ b) ∨ ∃ b ∈ moves right x, b ≤ a

The definition of x ≤ y on games, in terms of ≤ two moves later.

Note that it's often more convenient to use le_iff_forall_lf, which only unfolds the definition by one step.

theorem IGame.lf_def {x y : IGame} : ¬y ≤ x ↔ (∃ a ∈ moves left y, (∀ b ∈ moves left x, ¬a ≤ b) ∧ ∀ b ∈ moves right a, ¬b ≤ x) ∨ ∃ a ∈ moves right x, (∀ b ∈ moves left a, ¬y ≤ b) ∧ ∀ b ∈ moves right y, ¬b ≤ a

The definition of x ⧏ y on games, in terms of ⧏ two moves later.

Note that it's often more convenient to use lf_iff_exists_le, which only unfolds the definition by one step.

theorem IGame.left_lf_of_le {x y z : IGame} (h : x ≤ y) (h' : z ∈ moves left x) : ¬y ≤ z

theorem IGame.lf_right_of_le {x y z : IGame} (h : x ≤ y) (h' : z ∈ moves right y) : ¬z ≤ x

theorem IGame.lf_of_le_left {x y z : IGame} (h : x ≤ z) (h' : z ∈ moves left y) : ¬y ≤ x

theorem IGame.lf_of_right_le {x y z : IGame} (h : z ≤ y) (h' : z ∈ moves right x) : ¬y ≤ x

instance IGame.instPreorder : Preorder IGame

Equations

• IGame.instPreorder = { toLE := IGame.instLE, lt := fun (a b : IGame) => a ≤ b ∧ ¬b ≤ a, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := IGame.instPreorder._proof_1 }

theorem IGame.left_lf {x y : IGame} (h : y ∈ moves left x) : ¬x ≤ y

theorem IGame.lf_right {x y : IGame} (h : y ∈ moves right x) : ¬y ≤ x

def IGame.«term_≈_» : Lean.TrailingParserDescr

The equivalence relation x ≈ y means that x ≤ y and y ≤ x. This is notation for AntisymmRel (⬝ ≤ ⬝) x y.

Conventions for notations in identifiers:

• The recommended spelling of ≈ in identifiers is equiv.

Equations

• IGame.«term_≈_» = Lean.ParserDescr.trailingNode `IGame.«term_≈_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≈ ") (Lean.ParserDescr.cat `term 51))

def IGame.«term_‖_» : Lean.TrailingParserDescr

The "fuzzy" relation x ‖ y means that x ⧏ y and y ⧏ x. This is notation for IncompRel (⬝ ≤ ⬝) x y.

Conventions for notations in identifiers:

• The recommended spelling of ‖ in identifiers is fuzzy.

Equations

• IGame.«term_‖_» = Lean.ParserDescr.trailingNode `IGame.«term_‖_» 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ‖ ") (Lean.ParserDescr.cat `term 50))

def IGame.delabEquiv : Lean.PrettyPrinter.Delaborator.Delab

Equations

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

def IGame.delabFuzzy : Lean.PrettyPrinter.Delaborator.Delab

Equations

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

theorem IGame.equiv_of_forall_lf {x y : IGame} (hl₁ : ∀ a ∈ moves left x, ¬y ≤ a) (hr₁ : ∀ a ∈ moves right x, ¬a ≤ y) (hl₂ : ∀ b ∈ moves left y, ¬x ≤ b) (hr₂ : ∀ b ∈ moves right y, ¬b ≤ x) : x ≈ y

theorem IGame.equiv_of_exists_le {x y : IGame} (hl₁ : ∀ a ∈ moves left x, ∃ b ∈ moves left y, a ≤ b) (hr₁ : ∀ a ∈ moves right x, ∃ b ∈ moves right y, b ≤ a) (hl₂ : ∀ b ∈ moves left y, ∃ a ∈ moves left x, b ≤ a) (hr₂ : ∀ b ∈ moves right y, ∃ a ∈ moves right x, a ≤ b) : x ≈ y

theorem IGame.equiv_of_exists {x y : IGame} (hl₁ : ∀ a ∈ moves left x, ∃ b ∈ moves left y, a ≈ b) (hr₁ : ∀ a ∈ moves right x, ∃ b ∈ moves right y, a ≈ b) (hl₂ : ∀ b ∈ moves left y, ∃ a ∈ moves left x, a ≈ b) (hr₂ : ∀ b ∈ moves right y, ∃ a ∈ moves right x, a ≈ b) : x ≈ y

@[simp]

theorem IGame.zero_lt_one : 0 < 1

instance IGame.instZeroLEOneClass : ZeroLEOneClass IGame

Negation

instance IGame.instNeg : Neg IGame

The negative of a game is defined by -!{s | t} = !{-t | -s}.

Equations

• IGame.instNeg = { neg := IGame.neg'✝ }

instance IGame.instInvolutiveNeg : InvolutiveNeg IGame

Equations

• IGame.instInvolutiveNeg = { toNeg := IGame.instNeg, neg_neg := IGame.instInvolutiveNeg._proof_1 }

@[simp]

theorem IGame.neg_ofSets (s t : Set IGame) [Small.{u_1, u_1 + 1} ↑s] [Small.{u_1, u_1 + 1} ↑t] : -!{s | t} = !{-t | -s}

theorem IGame.neg_ofSets' (st : Player → Set IGame) [Small.{u_1, u_1 + 1} ↑(st left)] [Small.{u_1, u_1 + 1} ↑(st right)] : -!{st} = !{fun (p : Player) => -st (-p)}

@[simp]

theorem IGame.neg_ofSets_const (s : Set IGame) [Small.{u_1, u_1 + 1} ↑s] : -!{fun (x : Player) => s} = !{fun (x : Player) => -s}

instance IGame.instNegZeroClass : NegZeroClass IGame

Equations

• IGame.instNegZeroClass = { toZero := IGame.instZero, toNeg := IGame.instNeg, neg_zero := IGame.instNegZeroClass._proof_1 }

theorem IGame.neg_eq (x : IGame) : -x = !{-moves right x | -moves left x}

theorem IGame.neg_eq' (x : IGame) : -x = !{fun (p : Player) => -moves (-p) x}

@[simp]

theorem IGame.moves_neg (p : Player) (x : IGame) : moves p (-x) = -moves (-p) x

theorem IGame.isOption_neg {x y : IGame} : x.IsOption (-y) ↔ (-x).IsOption y

@[simp]

theorem IGame.isOption_neg_neg {x y : IGame} : (-x).IsOption (-y) ↔ x.IsOption y

theorem IGame.forall_moves_neg {P : IGame → Prop} {p : Player} {x : IGame} : (∀ y ∈ moves p (-x), P y) ↔ ∀ y ∈ moves (-p) x, P (-y)

theorem IGame.exists_moves_neg {P : IGame → Prop} {p : Player} {x : IGame} : (∃ y ∈ moves p (-x), P y) ↔ ∃ y ∈ moves (-p) x, P (-y)

@[simp]

theorem IGame.neg_le_neg_iff {x y : IGame} : -x ≤ -y ↔ y ≤ x

theorem IGame.neg_le {x y : IGame} : -x ≤ y ↔ -y ≤ x

theorem IGame.le_neg {x y : IGame} : x ≤ -y ↔ y ≤ -x

@[simp]

theorem IGame.neg_lt_neg_iff {x y : IGame} : -x < -y ↔ y < x

theorem IGame.neg_lt {x y : IGame} : -x < y ↔ -y < x

theorem IGame.lt_neg {x y : IGame} : x < -y ↔ y < -x

@[simp]

theorem IGame.neg_equiv_neg_iff {x y : IGame} : -x ≈ -y ↔ x ≈ y

theorem IGame.neg_congr {x y : IGame} : x ≈ y → -x ≈ -y

Alias of the reverse direction of IGame.neg_equiv_neg_iff.

@[simp]

theorem IGame.neg_fuzzy_neg_iff {x y : IGame} : -x ‖ -y ↔ x ‖ y

@[simp]

theorem IGame.neg_le_zero {x : IGame} : -x ≤ 0 ↔ 0 ≤ x

@[simp]

theorem IGame.zero_le_neg {x : IGame} : 0 ≤ -x ↔ x ≤ 0

@[simp]

theorem IGame.neg_lt_zero {x : IGame} : -x < 0 ↔ 0 < x

@[simp]

theorem IGame.zero_lt_neg {x : IGame} : 0 < -x ↔ x < 0

@[simp]

theorem IGame.neg_equiv_zero {x : IGame} : -x ≈ 0 ↔ x ≈ 0

@[simp]

theorem IGame.zero_equiv_neg {x : IGame} : 0 ≈ -x ↔ 0 ≈ x

@[simp]

theorem IGame.neg_fuzzy_zero {x : IGame} : -x ‖ 0 ↔ x ‖ 0

@[simp]

theorem IGame.zero_fuzzy_neg {x : IGame} : 0 ‖ -x ↔ 0 ‖ x

Addition and subtraction

instance IGame.instAdd : Add IGame

The sum of x = !{s₁ | t₁} and y = !{s₂ | t₂} is !{s₁ + y, x + s₂ | t₁ + y, x + t₂}.

Equations

• IGame.instAdd = { add := IGame.add'✝ }

theorem IGame.add_eq (x y : IGame) : x + y = !{(fun (x : IGame) => x + y) '' moves left x ∪ (fun (x_1 : IGame) => x + x_1) '' moves left y | (fun (x : IGame) => x + y) '' moves right x ∪ (fun (x_1 : IGame) => x + x_1) '' moves right y}

theorem IGame.add_eq' (x y : IGame) : x + y = !{fun (p : Player) => (fun (x : IGame) => x + y) '' moves p x ∪ (fun (x_1 : IGame) => x + x_1) '' moves p y}

theorem IGame.ofSets_add_ofSets (s₁ t₁ s₂ t₂ : Set IGame) [Small.{u_1, u_1 + 1} ↑s₁] [Small.{u_1, u_1 + 1} ↑t₁] [Small.{u_1, u_1 + 1} ↑s₂] [Small.{u_1, u_1 + 1} ↑t₂] : !{s₁ | t₁} + !{s₂ | t₂} = !{(fun (x : IGame) => x + !{s₂ | t₂}) '' s₁ ∪ (fun (x : IGame) => !{s₁ | t₁} + x) '' s₂ | (fun (x : IGame) => x + !{s₂ | t₂}) '' t₁ ∪ (fun (x : IGame) => !{s₁ | t₁} + x) '' t₂}

theorem IGame.ofSets_add_ofSets' (st₁ st₂ : Player → Set IGame) [Small.{u_1, u_1 + 1} ↑(st₁ left)] [Small.{u_1, u_1 + 1} ↑(st₂ left)] [Small.{u_1, u_1 + 1} ↑(st₁ right)] [Small.{u_1, u_1 + 1} ↑(st₂ right)] : !{st₁} + !{st₂} = !{fun (p : Player) => (fun (x : IGame) => x + !{st₂}) '' st₁ p ∪ (fun (x : IGame) => !{st₁} + x) '' st₂ p}

@[simp]

theorem IGame.moves_add (p : Player) (x y : IGame) : moves p (x + y) = (fun (x : IGame) => x + y) '' moves p x ∪ (fun (x_1 : IGame) => x + x_1) '' moves p y

theorem IGame.add_left_mem_moves_add {p : Player} {x y : IGame} (h : x ∈ moves p y) (z : IGame) : z + x ∈ moves p (z + y)

theorem IGame.add_right_mem_moves_add {p : Player} {x y : IGame} (h : x ∈ moves p y) (z : IGame) : x + z ∈ moves p (y + z)

theorem IGame.IsOption.add_left {x y z : IGame} (h : x.IsOption y) : (z + x).IsOption (z + y)

theorem IGame.IsOption.add_right {x y z : IGame} (h : x.IsOption y) : (x + z).IsOption (y + z)

theorem IGame.forall_moves_add {p : Player} {P : IGame → Prop} {x y : IGame} : (∀ a ∈ moves p (x + y), P a) ↔ (∀ a ∈ moves p x, P (a + y)) ∧ ∀ b ∈ moves p y, P (x + b)

theorem IGame.exists_moves_add {p : Player} {P : IGame → Prop} {x y : IGame} : (∃ a ∈ moves p (x + y), P a) ↔ (∃ a ∈ moves p x, P (a + y)) ∨ ∃ b ∈ moves p y, P (x + b)

@[simp]

theorem IGame.add_eq_zero_iff {x y : IGame} : x + y = 0 ↔ x = 0 ∧ y = 0

instance IGame.instAddCommMonoid : AddCommMonoid IGame

Equations

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

instance IGame.instSubNegMonoid : SubNegMonoid IGame

The subtraction of x and y is defined as x + (-y).

Equations

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

@[simp]

theorem IGame.moves_sub (p : Player) (x y : IGame) : moves p (x - y) = (fun (x : IGame) => x - y) '' moves p x ∪ (fun (x_1 : IGame) => x + x_1) '' (-moves (-p) y)

theorem IGame.sub_left_mem_moves_sub {p : Player} {x y : IGame} (h : x ∈ moves p y) (z : IGame) : z - x ∈ moves (-p) (z - y)

theorem IGame.sub_left_mem_moves_sub_neg {p : Player} {x y : IGame} (h : x ∈ moves (-p) y) (z : IGame) : z - x ∈ moves p (z - y)

theorem IGame.sub_right_mem_moves_sub {p : Player} {x y : IGame} (h : x ∈ moves p y) (z : IGame) : x - z ∈ moves p (y - z)

instance IGame.instSubtractionCommMonoid : SubtractionCommMonoid IGame

Equations

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

theorem IGame.sub_self_equiv (x : IGame) : x - x ≈ 0

The sum of a game and its negative is equivalent, though not necessarily identical to zero.

theorem IGame.neg_add_equiv (x : IGame) : -x + x ≈ 0

The sum of a game and its negative is equivalent, though not necessarily identical to zero.

instance IGame.instAddLeftMono : AddLeftMono IGame

instance IGame.instAddRightMono : AddRightMono IGame

instance IGame.instAddLeftReflectLE : AddLeftReflectLE IGame

instance IGame.instAddRightReflectLE : AddRightReflectLE IGame

instance IGame.instAddLeftStrictMono : AddLeftStrictMono IGame

instance IGame.instAddRightStrictMono : AddRightStrictMono IGame

instance IGame.instAddLeftReflectLT : AddLeftReflectLT IGame

instance IGame.instAddRightReflectLT : AddRightReflectLT IGame

theorem IGame.add_congr {a b : IGame} (h₁ : a ≈ b) {c d : IGame} (h₂ : c ≈ d) : a + c ≈ b + d

theorem IGame.add_congr_left {a b c : IGame} (h : a ≈ b) : a + c ≈ b + c

theorem IGame.add_congr_right {a b c : IGame} (h : a ≈ b) : c + a ≈ c + b

@[simp]

theorem IGame.add_fuzzy_add_iff_left {a b c : IGame} : a + b ‖ a + c ↔ b ‖ c

@[simp]

theorem IGame.add_fuzzy_add_iff_right {a b c : IGame} : b + a ‖ c + a ↔ b ‖ c

theorem IGame.sub_congr {a b : IGame} (h₁ : a ≈ b) {c d : IGame} (h₂ : c ≈ d) : a - c ≈ b - d

theorem IGame.sub_congr_left {a b c : IGame} (h : a ≈ b) : a - c ≈ b - c

theorem IGame.sub_congr_right {a b c : IGame} (h : a ≈ b) : c - a ≈ c - b

instance IGame.instAddCommMonoidWithOne : AddCommMonoidWithOne IGame

We define the NatCast instance as ↑0 = 0 and ↑(n + 1) = !{{↑n} | ∅}.

Note that this is equivalent, but not identical, to the more common definition ↑n = !{Iio n | ∅}. For that, use NatOrdinal.toIGame.

Equations

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

theorem IGame.leftMoves_natCast_succ' (n : ℕ) : moves left ↑n.succ = {↑n}

This version of the theorem is more convenient for the game_cmp tactic.

@[simp]

theorem IGame.leftMoves_natCast_succ (n : ℕ) : moves left (↑n + 1) = {↑n}

@[simp]

theorem IGame.rightMoves_natCast (n : ℕ) : moves right ↑n = ∅

@[simp]

theorem IGame.leftMoves_ofNat (n : ℕ) [n.AtLeastTwo] : moves left (OfNat.ofNat n) = {↑(n - 1)}

@[simp]

theorem IGame.rightMoves_ofNat (n : ℕ) [n.AtLeastTwo] : moves right (OfNat.ofNat n) = ∅

theorem IGame.natCast_succ_eq (n : ℕ) : ↑n + 1 = !{{↑n} | ∅}

theorem IGame.eq_natCast_of_mem_leftMoves_natCast {n : ℕ} {x : IGame} (hx : x ∈ moves left ↑n) : ∃ m < n, ↑m = x

Every left option of a natural number is equal to a smaller natural number.

instance IGame.instIntCast : IntCast IGame

Equations

• IGame.instIntCast = { intCast := fun (x : ℤ) => match x with | Int.ofNat n => ↑n | Int.negSucc n => -(↑n + 1) }

@[simp]

theorem IGame.intCast_nat (n : ℕ) : ↑↑n = ↑n

@[simp]

theorem IGame.intCast_ofNat (n : ℕ) : ↑(OfNat.ofNat n) = ↑n

@[simp]

theorem IGame.intCast_negSucc (n : ℕ) : ↑(Int.negSucc n) = -(↑n + 1)

theorem IGame.intCast_zero : ↑0 = 0

theorem IGame.intCast_one : ↑1 = 1

@[simp]

theorem IGame.intCast_neg (n : ℤ) : ↑(-n) = -↑n

theorem IGame.eq_sub_one_of_mem_leftMoves_intCast {n : ℤ} {x : IGame} (hx : x ∈ moves left ↑n) : x = ↑(n - 1)

theorem IGame.eq_add_one_of_mem_rightMoves_intCast {n : ℤ} {x : IGame} (hx : x ∈ moves right ↑n) : x = ↑(n + 1)

theorem IGame.eq_intCast_of_mem_leftMoves_intCast {n : ℤ} {x : IGame} (hx : x ∈ moves left ↑n) : ∃ m < n, ↑m = x

Every left option of an integer is equal to a smaller integer.

theorem IGame.eq_intCast_of_mem_rightMoves_intCast {n : ℤ} {x : IGame} (hx : x ∈ moves right ↑n) : ∃ (m : ℤ), n < m ∧ ↑m = x

Every right option of an integer is equal to a larger integer.

Multiplication

@[irreducible]

def IGame.mul' (x y : IGame) : IGame

Equations

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

instance IGame.instMul : Mul IGame

The product of x = !{s₁ | t₁} and y = !{s₂ | t₂} is !{a₁ * y + x * b₁ - a₁ * b₁ | a₂ * y + x * b₂ - a₂ * b₂}, where (a₁, b₁) ∈ s₁ ×ˢ s₂ ∪ t₁ ×ˢ t₂ and (a₂, b₂) ∈ s₁ ×ˢ t₂ ∪ t₁ ×ˢ s₂.

Using IGame.mulOption, this can alternatively be written as x * y = !{mulOption x y a₁ b₁ | mulOption x y a₂ b₂}.

Equations

• IGame.instMul = { mul := IGame.mul' }

def IGame.mulOption (x y a b : IGame) : IGame

The general option of x * y looks like a * y + x * b - a * b, for a and b options of x and y, respectively.

Equations

• IGame.mulOption x y a b = a * y + x * b - a * b

theorem IGame.mul_eq (x y : IGame) : x * y = !{(fun (a : IGame × IGame) => mulOption x y a.1 a.2) '' (moves left x ×ˢ moves left y ∪ moves right x ×ˢ moves right y) | (fun (a : IGame × IGame) => mulOption x y a.1 a.2) '' (moves left x ×ˢ moves right y ∪ moves right x ×ˢ moves left y)}

theorem IGame.mul_eq' (x y : IGame) : x * y = !{fun (p : Player) => (fun (a : IGame × IGame) => mulOption x y a.1 a.2) '' (moves left x ×ˢ moves p y ∪ moves right x ×ˢ moves (-p) y)}

theorem IGame.ofSets_mul_ofSets (s₁ t₁ s₂ t₂ : Set IGame) [Small.{u_1, u_1 + 1} ↑s₁] [Small.{u_1, u_1 + 1} ↑t₁] [Small.{u_1, u_1 + 1} ↑s₂] [Small.{u_1, u_1 + 1} ↑t₂] : !{s₁ | t₁} * !{s₂ | t₂} = !{(fun (a : IGame × IGame) => mulOption !{s₁ | t₁} !{s₂ | t₂} a.1 a.2) '' (s₁ ×ˢ s₂ ∪ t₁ ×ˢ t₂) | (fun (a : IGame × IGame) => mulOption !{s₁ | t₁} !{s₂ | t₂} a.1 a.2) '' (s₁ ×ˢ t₂ ∪ t₁ ×ˢ s₂)}

@[simp]

theorem IGame.moves_mul (p : Player) (x y : IGame) : moves p (x * y) = (fun (a : IGame × IGame) => mulOption x y a.1 a.2) '' (moves left x ×ˢ moves p y ∪ moves right x ×ˢ moves (-p) y)

@[simp]

theorem IGame.moves_mulOption (p : Player) (x y a b : IGame) : moves p (mulOption x y a b) = moves p (a * y + x * b - a * b)

theorem IGame.mulOption_mem_moves_mul {px py : Player} {x y a b : IGame} (h₁ : a ∈ moves px x) (h₂ : b ∈ moves py y) : mulOption x y a b ∈ moves (px * py) (x * y)

theorem IGame.IsOption.mul {x y a b : IGame} (h₁ : a.IsOption x) (h₂ : b.IsOption y) : (mulOption x y a b).IsOption (x * y)

theorem IGame.forall_moves_mul {p : Player} {P : IGame → Prop} {x y : IGame} : (∀ a ∈ moves p (x * y), P a) ↔ ∀ (p' : Player), ∀ a ∈ moves p' x, ∀ b ∈ moves (p' * p) y, P (mulOption x y a b)

theorem IGame.exists_moves_mul {p : Player} {P : IGame → Prop} {x y : IGame} : (∃ a ∈ moves p (x * y), P a) ↔ ∃ (p' : Player), ∃ a ∈ moves p' x, ∃ b ∈ moves (p' * p) y, P (mulOption x y a b)

instance IGame.instCommMagma : CommMagma IGame

Equations

• IGame.instCommMagma = { toMul := IGame.instMul, mul_comm := IGame.mul_comm'✝ }

instance IGame.instMulZeroClass : MulZeroClass IGame

Equations

• IGame.instMulZeroClass = { toMul := IGame.instMul, toZero := IGame.instZero, zero_mul := IGame.zero_mul'✝, mul_zero := IGame.instMulZeroClass._proof_1 }

instance IGame.instMulZeroOneClass : MulZeroOneClass IGame

Equations

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

theorem IGame.mulOption_comm (x y a b : IGame) : mulOption x y a b = mulOption y x b a

instance IGame.instHasDistribNeg : HasDistribNeg IGame

Equations

• IGame.instHasDistribNeg = { toInvolutiveNeg := IGame.instInvolutiveNeg, neg_mul := IGame.neg_mul'✝, mul_neg := IGame.instHasDistribNeg._proof_1 }

theorem IGame.mulOption_neg_left (x y a b : IGame) : mulOption (-x) y a b = -mulOption x y (-a) b

theorem IGame.mulOption_neg_right (x y a b : IGame) : mulOption x (-y) a b = -mulOption x y a (-b)

theorem IGame.mulOption_neg (x y a b : IGame) : mulOption (-x) (-y) a b = mulOption x y (-a) (-b)

@[simp]

theorem IGame.mulOption_zero_left (x y a : IGame) : mulOption x y 0 a = x * a

@[simp]

theorem IGame.mulOption_zero_right (x y a : IGame) : mulOption x y a 0 = a * y

Distributivity and associativity only hold up to equivalence; we prove this in CombinatorialGames.Game.Basic.

Division

instance IGame.instInv : Inv IGame

The inverse of a positive game x = !{s | t} is !{s' | t'}, where s' and t' are the smallest sets such that 0 ∈ s', and such that (1 + (z - x) * a) / z, (1 + (y - x) * b) / y ∈ s' and (1 + (y - x) * a) / y, (1 + (z - x) * b) / z ∈ t' for y ∈ s positive, z ∈ t, a ∈ s', and b ∈ t'.

If x is negative, we define x⁻¹ = -(-x)⁻¹. For any other game, we set x⁻¹ = 0.

If x is a non-zero numeric game, then x * x⁻¹ ≈ 1. The value of this function on any non-numeric game should be treated as a junk value.

Equations

• IGame.instInv = { inv := fun (x : IGame) => if 0 < x then IGame.inv'✝ x else if x < 0 then -IGame.inv'✝¹ (-x) else 0 }

instance IGame.instDiv : Div IGame

Equations

• IGame.instDiv = { div := fun (x y : IGame) => x * y⁻¹ }

theorem IGame.div_eq_mul_inv (x y : IGame) : x / y = x * y⁻¹

theorem IGame.inv_of_equiv_zero {x : IGame} (h : x ≈ 0) : x⁻¹ = 0

@[simp]

theorem IGame.inv_zero : 0⁻¹ = 0

@[simp]

theorem IGame.zero_div (x : IGame) : 0 / x = 0

@[simp]

theorem IGame.neg_div (x y : IGame) : -x / y = -(x / y)

@[simp]

theorem IGame.inv_neg (x : IGame) : (-x)⁻¹ = -x⁻¹

def IGame.invOption (x y a : IGame) : IGame

The general option of x⁻¹ looks like (1 + (y - x) * a) / y, for y an option of x, and a some other "earlier" option of x⁻¹.

Equations

• IGame.invOption x y a = (1 + (y - x) * a) / y

theorem IGame.zero_mem_leftMoves_inv {x : IGame} (hx : 0 < x) : 0 ∈ moves left x⁻¹

theorem IGame.inv_nonneg {x : IGame} (hx : 0 < x) : ¬x⁻¹ ≤ 0

theorem IGame.invOption_mem_moves_inv {x y a : IGame} {p₁ p₂ : Player} (hx : 0 < x) (hy : 0 < y) (hyx : y ∈ moves (-(p₁ * p₂)) x) (ha : a ∈ moves p₁ x⁻¹) : invOption x y a ∈ moves p₂ x⁻¹

theorem IGame.invRec {x : IGame} (hx : 0 < x) {P : (p : Player) → (y : IGame) → y ∈ moves p x⁻¹ → Prop} (zero : P left 0 ⋯) (mk : ∀ (p₁ p₂ : Player) (y : IGame) (hy : 0 < y) (hyx : y ∈ moves (-(p₁ * p₂)) x) (a : IGame) (ha : a ∈ moves p₁ x⁻¹), P p₁ a ha → P p₂ (invOption x y a) ⋯) (p : Player) (y : IGame) (hy : y ∈ moves p x⁻¹) : P p y hy

An induction principle on left and right moves of x⁻¹.

instance IGame.instRatCast : RatCast IGame

Equations

• IGame.instRatCast = { ratCast := fun (q : ℚ) => ↑q.num / ↑q.den }

theorem IGame.ratCast_def (q : ℚ) : ↑q = ↑q.num / ↑q.den

@[simp]

theorem IGame.ratCast_zero : ↑0 = 0

@[simp]

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