Documentation

LeanPool.MisereGames.Form.Birthday

Misere combinatorial games.

Birthdays of games #

There are two related but distinct notions of a birthday within combinatorial game theory. One is the birthday of an GameForm, which represents the "step" at which it is constructed; the day on which it is born. This is sometimes called the formal birthday of a game (see [Siegel, Definition 1.27 on p. 61][siegel:CombinatorialGameTheory:2013]).

It can be defined recursively as the least ordinal strictly larger than the birthdays of its Left and Right options.

The birthday of an GameForm can also be understood as the depth of its game tree.

source
@[irreducible]
noncomputable def MisereGames.Form.birthday {G : Type (u + 1)} [g_form : Form G] (x : G) :
NatOrdinal

The birthday of a form is inductively defined as the least ordinal strictly larger than the birthdays of its options. It may be thought as the "step" in which the given game is constructed.

Equations
Instances For
    source
    theorem MisereGames.Form.lt_birthday_iff' {G : Type (u + 1)} [g_form : Form G] {x : G} {o : NatOrdinal} :
    o < birthday x ↔ ∃ (y : G), IsOption y x ∧ o ≤ birthday y
    source
    theorem MisereGames.Form.birthday_le_iff' {G : Type (u + 1)} [g_form : Form G] {x : G} {o : NatOrdinal} :
    birthday x ≤ o ↔ ∀ (y : G), IsOption y x → birthday y < o
    source
    theorem MisereGames.Form.lt_birthday_iff {G : Type (u + 1)} [g_form : Form G] {x : G} {o : NatOrdinal} :
    o < birthday x ↔ (∃ y ∈ moves Player.left x, o ≤ birthday y) ∨ ∃ y ∈ moves Player.right x, o ≤ birthday y
    source
    theorem MisereGames.Form.birthday_le_iff {G : Type (u + 1)} [g_form : Form G] {x : G} {o : NatOrdinal} :
    birthday x ≤ o ↔ (∀ y ∈ moves Player.left x, birthday y < o) ∧ ∀ y ∈ moves Player.right x, birthday y < o
    source
    theorem MisereGames.Form.birthday_eq_max {G : Type (u + 1)} [g_form : Form G] (x : G) :
    birthday x = max (⨆ (y : ↑(moves Player.left x)), Order.succ (birthday ↑y)) (⨆ (y : ↑(moves Player.right x)), Order.succ (birthday ↑y))
    source
    theorem MisereGames.Form.birthday_lt_of_mem_moves {G : Type (u + 1)} [g_form : Form G] {p : Player} {x y : G} (hy : y ∈ moves p x) :
    birthday y < birthday x
    source
    theorem MisereGames.Form.birthday_lt_of_isOption {G : Type (u + 1)} [g_form : Form G] {x y : G} (hy : IsOption y x) :
    birthday y < birthday x
    source
    theorem MisereGames.Form.birthday_lt_of_subposition {G : Type (u + 1)} [g_form : Form G] {x y : G} (hy : Subposition y x) :
    birthday y < birthday x
    source
    @[simp]
    theorem MisereGames.Form.birthday_neg {G : Type (u + 1)} [g_form : Form G] (x : G) :
    birthday (-x) = birthday x
    source
    @[simp]
    theorem MisereGames.Form.birthday_add {G : Type (u + 1)} [g_form : Form G] (g h : G) :
    birthday (g + h) = birthday g + birthday h
    source
    theorem MisereGames.Form.birthday_add_lt_left {G : Type (u + 1)} [g_form : Form G] {g' g h : G} (hlt : birthday g' < birthday g) :
    birthday g' + birthday h < birthday g + birthday h
    source
    theorem MisereGames.Form.birthday_add_lt_right {G : Type (u + 1)} [g_form : Form G] {g h' h : G} (hlt : birthday h' < birthday h) :
    birthday g + birthday h' < birthday g + birthday h
    source
    @[simp]
    theorem MisereGames.Form.birthday_ofSets {G : Type (u + 1)} [g_form : Form G] (s t : Set G) [Small.{u, u + 1} ↑s] [Small.{u, u + 1} ↑t] :
    birthday !{s | t} = max (sSup (Order.succ ∘ birthday '' s)) (sSup (Order.succ ∘ birthday '' t))
    source
    @[simp]
    theorem MisereGames.Form.birthday_ofSets_const {G : Type (u + 1)} [g_form : Form G] (s : Set G) [Small.{u, u + 1} ↑s] :
    birthday !{fun (x : Player) => s} = sSup (Order.succ ∘ birthday '' s)
    source
    @[simp]
    theorem MisereGames.Form.birthday_zero {G : Type (u + 1)} [g_form : Form G] :
    birthday 0 = 0
    source
    @[simp]
    theorem MisereGames.Form.birthday_one {G : Type (u + 1)} [g_form : Form G] :
    birthday 1 = 1
    source
    @[simp]
    theorem MisereGames.Form.birthday_natCast {G : Type (u + 1)} [g_form : Form G] (n : ℕ) :
    birthday ↑n = ↑n
    source
    @[simp]
    theorem MisereGames.Form.birthday_ofNat {G : Type (u + 1)} [g_form : Form G] (n : ℕ) [n.AtLeastTwo] :
    birthday (OfNat.ofNat n) = ↑n
    source
    @[simp]
    theorem MisereGames.Form.birthday_intCast {G : Type (u + 1)} [g_form : Form G] (k : ℤ) :
    birthday ↑k = ↑k.natAbs
    source
    def MisereGames.Form.gameformBirthday :
    Lean.ParserDescr

    Add birthday inequalities from move hypotheses, then simplify birthday arithmetic.

    Equations
    Instances For