Documentation

CombinatorialGames.Game.Canonical

Canonical games #

For any game G, its canonical game G' is the unique IGame game with smallest birthday such that G'.Fits G. From the literature, this file provides an explicit (though noncomputable) construction of canonical games through undominating and unreversing games.

Todo #

source
@[irreducible]
noncomputable def IGame.undominate (x : IGame) :
IGame

Undominating a game. This returns garbage values on non-short games

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[irreducible]
    theorem IGame.birthday_undominate_le (x : IGame) :
    x.undominate.birthday ≤ x.birthday
    source
    theorem IGame.undominate_def {x : IGame} :
    x.undominate = {{y : IGame | y ∈ undominate '' x.leftMoves ∧ ∀ z ∈ x.leftMoves, ¬y < z} | {y : IGame | y ∈ undominate '' x.rightMoves ∧ ∀ z ∈ x.rightMoves, ¬z < y}}ᴵ
    source
    @[simp]
    theorem IGame.leftMoves_undominate {x : IGame} :
    x.undominate.leftMoves = {y : IGame | y ∈ undominate '' x.leftMoves ∧ ∀ z ∈ x.leftMoves, ¬y < z}
    source
    @[simp]
    theorem IGame.rightMoves_undominate {x : IGame} :
    x.undominate.rightMoves = {y : IGame | y ∈ undominate '' x.rightMoves ∧ ∀ z ∈ x.rightMoves, ¬z < y}
    source
    instance IGame.instShortUndominate {x : IGame} [hx : x.Short] :
    x.undominate.Short
    source
    @[simp, irreducible]
    theorem IGame.undominate_neg (x : IGame) :
    (-x).undominate = -x.undominate
    source
    theorem IGame.undominate_equiv (x : IGame) [x.Short] :
    x.undominate ≈ x