Special games

This file defines some simple yet notable combinatorial games:

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

Star

def IGame.star : IGame

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

Equations

• ⋆ = {{0} | {0}}ᴵ

def IGame.«term⋆» : Lean.ParserDescr

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

Equations

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

@[simp]

theorem IGame.leftMoves_star : ⋆.leftMoves = {0}

@[simp]

theorem IGame.rightMoves_star : ⋆.rightMoves = {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.

Equations

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

@[simp]

theorem IGame.leftMoves_half : ½.leftMoves = {0}

@[simp]

theorem IGame.rightMoves_half : ½.rightMoves = {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 | ⋆}.

Equations

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

@[simp]

theorem IGame.leftMoves_up : ↑.leftMoves = {0}

@[simp]

theorem IGame.rightMoves_up : ↑.rightMoves = {⋆}

@[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}.

Equations

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

@[simp]

theorem IGame.leftMoves_down : ↓.leftMoves = {⋆}

@[simp]

theorem IGame.rightMoves_down : ↓.rightMoves = {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.

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) : (⧾x).leftMoves = {0}

@[simp]

theorem IGame.rightMoves_tiny (x : IGame) : (⧾x).rightMoves = {{{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}.

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) : (⧿x).leftMoves = {{{x} | {0}}ᴵ}

@[simp]

theorem IGame.rightMoves_miny (x : IGame) : (⧿x).rightMoves = {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

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!

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) : (±x).leftMoves = {x}

@[simp]

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

@[simp]

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

@[simp]

theorem IGame.switch_zero : ±0 = ⋆