Special games

This file defines some simple yet notable combinatorial games:

• ⋆ = {0 | 0}
• ½ = {0 | 1}
• ↑ = {0 | ⋆}
• ↓ = {⋆ | 0}.

Star

def IGame.star : IGame

The game ⋆ = {0 | 0}, which is fuzzy with zero.

Equations

• ⋆ = !{fun (x : Player) => {0}}

def IGame.«term⋆» : Lean.ParserDescr

The game ⋆ = {0 | 0}, which is fuzzy with zero.

Conventions for notations in identifiers:

• The recommended spelling of ⋆ in identifiers is star.

Equations

• IGame.«term⋆» = Lean.ParserDescr.node `IGame.«term⋆» 1024 (Lean.ParserDescr.symbol "⋆")

@[simp]

theorem IGame.moves_star (p : Player) : moves p ⋆ = {0}

@[simp]

theorem IGame.zero_lf_star : ¬⋆ ≤ 0

@[simp]

theorem IGame.star_lf_zero : ¬0 ≤ ⋆

theorem IGame.star_fuzzy_zero : ⋆ ‖ 0

theorem IGame.zero_fuzzy_star : 0 ‖ ⋆

@[simp]

theorem IGame.neg_star : -⋆ = ⋆

@[simp]

theorem IGame.star_mul_star : ⋆ * ⋆ = ⋆

@[simp]

instance IGame.instShortStar : ⋆.Short

Half

def IGame.half : IGame

The game ½ = {0 | 1}, which we prove satisfies ½ + ½ = 1.

Equations

• ½ = !{{0} | {1}}

def IGame.«term½» : Lean.ParserDescr

The game ½ = {0 | 1}, which we prove satisfies ½ + ½ = 1.

Conventions for notations in identifiers:

• The recommended spelling of ½ in identifiers is half.

Equations

• IGame.«term½» = Lean.ParserDescr.node `IGame.«term½» 1024 (Lean.ParserDescr.symbol "½")

@[simp]

theorem IGame.leftMoves_half : moves left ½ = {0}

@[simp]

theorem IGame.rightMoves_half : moves right ½ = {1}

theorem IGame.zero_lt_half : 0 < ½

theorem IGame.half_lt_one : ½ < 1

theorem IGame.half_add_half_equiv_one : ½ + ½ ≈ 1

instance IGame.instShortHalf : ½.Short

Up and down

def IGame.up : IGame

The game ↑ = {0 | ⋆}.

Equations

• ↑ = !{{0} | {⋆}}

def IGame.«term↑» : Lean.ParserDescr

The game ↑ = {0 | ⋆}.

Conventions for notations in identifiers:

• The recommended spelling of ↑ in identifiers is up.

Equations

• IGame.«term↑» = Lean.ParserDescr.node `IGame.«term↑» 1024 (Lean.ParserDescr.symbol "↑")

@[simp]

theorem IGame.leftMoves_up : moves left ↑ = {0}

@[simp]

theorem IGame.rightMoves_up : moves right ↑ = {⋆}

@[simp]

theorem IGame.up_pos : 0 < ↑

theorem IGame.up_fuzzy_star : ↑ ‖ ⋆

theorem IGame.star_fuzzy_up : ⋆ ‖ ↑

instance IGame.instShortUp : ↑.Short

def IGame.down : IGame

The game ↓ = {⋆ | 0}.

Equations

• ↓ = !{{⋆} | {0}}

def IGame.«term↓» : Lean.ParserDescr

The game ↓ = {⋆ | 0}.

Conventions for notations in identifiers:

• The recommended spelling of ↓ in identifiers is down.

Equations

• IGame.«term↓» = Lean.ParserDescr.node `IGame.«term↓» 1024 (Lean.ParserDescr.symbol "↓")

@[simp]

theorem IGame.leftMoves_down : moves left ↓ = {⋆}

@[simp]

theorem IGame.rightMoves_down : moves right ↓ = {0}

@[simp]

theorem IGame.neg_down : -↓ = ↑

@[simp]

theorem IGame.neg_up : -↑ = ↓

@[simp]

theorem IGame.down_neg : ↓ < 0

theorem IGame.down_fuzzy_star : ↓ ‖ ⋆

theorem IGame.star_fuzzy_down : ⋆ ‖ ↓

instance IGame.instShortDown : ↓.Short

Tiny and miny

def IGame.tiny (x : IGame) : IGame

A tiny game ⧾x is defined as {0 | {0 | -x}}, and is amongst the smallest of the infinitesimals.

Equations

• ⧾x = !{{0} | {!{{0} | {-x}}}}

def IGame.«term⧾_» : Lean.ParserDescr

A tiny game ⧾x is defined as {0 | {0 | -x}}, and is amongst the smallest of the infinitesimals.

Conventions for notations in identifiers:

• The recommended spelling of ⧾ in identifiers is tiny.

Equations

• IGame.«term⧾_» = Lean.ParserDescr.node `IGame.«term⧾_» 75 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⧾") (Lean.ParserDescr.cat `term 75))

@[simp]

theorem IGame.leftMoves_tiny (x : IGame) : moves left (⧾x) = {0}

@[simp]

theorem IGame.rightMoves_tiny (x : IGame) : moves right (⧾x) = {!{{0} | {-x}}}

instance IGame.instShortTiny (x : IGame) [x.Short] : (⧾x).Short

def IGame.miny (x : IGame) : IGame

A miny game ⧿x is defined as {{x | 0} | 0}.

Equations

• ⧿x = !{{!{{x} | {0}}} | {0}}

def IGame.«term⧿_» : Lean.ParserDescr

A miny game ⧿x is defined as {{x | 0} | 0}.

Conventions for notations in identifiers:

• The recommended spelling of ⧿ in identifiers is miny.

Equations

• IGame.«term⧿_» = Lean.ParserDescr.node `IGame.«term⧿_» 75 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⧿") (Lean.ParserDescr.cat `term 75))

@[simp]

theorem IGame.leftMoves_miny (x : IGame) : moves left (⧿x) = {!{{x} | {0}}}

@[simp]

theorem IGame.rightMoves_miny (x : IGame) : moves right (⧿x) = {0}

@[simp]

theorem IGame.neg_tiny (x : IGame) : -⧾x = ⧿x

@[simp]

theorem IGame.neg_miny (x : IGame) : -⧿x = ⧾x

instance IGame.instShortMiny (x : IGame) [x.Short] : (⧿x).Short

@[simp]

theorem IGame.tiny_pos (x : IGame) : 0 < ⧾x

@[simp]

theorem IGame.miny_neg (x : IGame) : ⧿x < 0

Switches

def IGame.switch (x : IGame) : IGame

A switch ±x is defined as {x | -x}: switches are their own confusion interval!

Equations

• ±x = !{{x} | {-x}}

def IGame.«term±_» : Lean.ParserDescr

A switch ±x is defined as {x | -x}: switches are their own confusion interval!

Conventions for notations in identifiers:

• The recommended spelling of ± in identifiers is switch.

Equations

• IGame.«term±_» = Lean.ParserDescr.node `IGame.«term±_» 75 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "±") (Lean.ParserDescr.cat `term 75))

@[simp]

theorem IGame.leftMoves_switch (x : IGame) : moves left (±x) = {x}

@[simp]

theorem IGame.rightMoves_switch (x : IGame) : moves right (±x) = {-x}

@[simp]

theorem IGame.neg_switch (x : IGame) : -±x = ±x

@[simp]

theorem IGame.switch_zero : ±0 = ⋆