Documentation

LeanPool.MisereGames.Form.Short

Misere combinatorial games.

Short games #

A combinatorial game is Short if it is finite and loopfree: it has only finite many distinct subpositions, and every run has finite length. See [Siegel, Definition 4.1 on p. 34][siegel:CombinatorialGameTheory:2013].

source
@[irreducible]
def MisereGames.Form.IsShort {G : Type (u + 1)} [Form G] (x : G) :
Prop

Short forms have finitely many options, all of which are short.

Equations
Instances For
    source
    theorem MisereGames.Form.short_def {G : Type (u + 1)} [Form G] {x : G} :
    IsShort x ↔ ∀ (p : Player), (moves p x).Finite ∧ ∀ y ∈ moves p x, IsShort y
    source
    theorem MisereGames.Form.Short.mk {G : Type (u + 1)} [Form G] {x : G} :
    (∀ (p : Player), (moves p x).Finite ∧ ∀ y ∈ moves p x, IsShort y) → IsShort x

    Alias of the reverse direction of MisereGames.Form.short_def.

    source
    theorem MisereGames.Form.Short.finite_moves {G : Type (u + 1)} [Form G] (p : Player) {x : G} (hx : IsShort x) :
    (moves p x).Finite
    source
    theorem MisereGames.Form.Short.finite_moves' {G : Type (u + 1)} [Form G] (p : Player) {x : G} (hx : IsShort x) :
    Finite ↑(moves p x)
    source
    theorem MisereGames.Form.Short.finite_setOf_isOption {G : Type (u + 1)} [Form G] {x : G} (hx : IsShort x) :
    {y : G | IsOption y x}.Finite
    source
    theorem MisereGames.Form.Short.of_mem_moves {G : Type (u + 1)} [Form G] {x y : G} (hx : IsShort x) {p : Player} (hy : y ∈ moves p x) :
    IsShort y
    source
    theorem MisereGames.Form.Short.isOption {G : Type (u + 1)} [Form G] {x y : G} (hx : IsShort x) (h : IsOption y x) :
    IsShort y
    source
    theorem Moves.IsOption.short {G : Type (u + 1)} [MisereGames.Form G] {x y : G} (hx : MisereGames.Form.IsShort x) (h : MisereGames.Moves.IsOption y x) :
    MisereGames.Form.IsShort y

    Alias of MisereGames.Form.Short.isOption.

    source
    theorem MisereGames.Form.Short.subposition {G : Type (u + 1)} [Form G] {x y : G} (hx : IsShort x) (h : Subposition y x) :
    IsShort y
    source
    theorem Moves.IsOption.subposition {G : Type (u + 1)} [MisereGames.Form G] {x y : G} (hx : MisereGames.Form.IsShort x) (h : MisereGames.Moves.Subposition y x) :
    MisereGames.Form.IsShort y

    Alias of MisereGames.Form.Short.subposition.

    source
    theorem MisereGames.Form.Short.finite_setOf_subposition {G : Type (u + 1)} [Form G] {x : G} (hx : IsShort x) :
    {y : G | Subposition y x}.Finite
    source
    theorem Moves.short_iff_finite_setOf_subposition {G : Type (u + 1)} [MisereGames.Form G] {x : G} :
    MisereGames.Form.IsShort x ↔ {y : G | MisereGames.Moves.Subposition y x}.Finite
    source
    theorem MisereGames.Form.Short.add {G : Type (u + 1)} [Form G] {x y : G} (hx : IsShort x) (hy : IsShort y) :
    IsShort (x + y)
    source
    theorem MisereGames.Form.Short.neg {G : Type (u + 1)} [Form G] {x : G} (hx : IsShort x) :
    IsShort (-x)
    source
    instance MisereGames.Form.Short.instClosedUnderNegIsShort {G : Type (u + 1)} [Form G] :
    ClosedUnderNeg IsShort
    source
    instance MisereGames.Form.Short.instHereditaryIsShort {G : Type (u + 1)} [Form G] :
    Hereditary IsShort
    source
    theorem MisereGames.Form.Short.neg_iff {G : Type (u + 1)} [Form G] {x : G} :
    IsShort (-x) ↔ IsShort x
    source
    theorem MisereGames.Form.Short.short_iff_finite_setOf_subposition {G : Type (u + 1)} [Form G] {x : G} :
    IsShort x ↔ {y : G | Subposition y x}.Finite
    source
    @[simp]
    theorem MisereGames.Form.Short.zero {G : Type (u + 1)} [Form G] :
    IsShort 0
    source
    instance MisereGames.Form.Short.instHasZeroIsShort {G : Type (u + 1)} [Form G] :
    HasZero IsShort
    source
    theorem MisereGames.Form.Short.ofSets {G : Type (u + 1)} [Form G] {s t : Set G} [Small.{u, u + 1} ↑s] [Small.{u, u + 1} ↑t] (hs_fin : s.Finite) (hs_short : ∀ g ∈ s, IsShort g) (ht_fin : t.Finite) (ht_short : ∀ g ∈ t, IsShort g) :
    IsShort !{s | t}
    source
    @[simp]
    theorem MisereGames.Form.Short.star {G : Type (u + 1)} [Form G] :
    IsShort !{{0} | {0}}
    source
    @[simp]
    theorem MisereGames.Form.Short.one {G : Type (u + 1)} [Form G] :
    IsShort 1
    source
    theorem MisereGames.Form.Short.sub {x y : GameForm} (hx : IsShort x) (hy : IsShort y) :
    IsShort (x - y)
    source
    @[simp]
    theorem MisereGames.Form.Short.natCast {G : Type (u + 1)} [Form G] (n : ℕ) :
    IsShort ↑n
    source
    @[simp]
    theorem MisereGames.Form.Short.ofNat {G : Type (u + 1)} [Form G] (n : ℕ) [n.AtLeastTwo] :
    IsShort (OfNat.ofNat n)
    source
    @[simp]
    theorem MisereGames.Form.Short.intCast {G : Type (u + 1)} [Form G] (n : ℤ) :
    IsShort ↑n
    source
    theorem MisereGames.GameForm.short_iff_birthday_finite {g : GameForm} :
    Form.IsShort g ↔ Form.birthday g < NatOrdinal.of Ordinal.omega0
    source
    theorem MisereGames.GameForm.short_iff_birthday_nat {x : GameForm} :
    Form.IsShort x ↔ ∃ (n : ℕ), Form.birthday x = ↑n