LeanPool.MisereGames.Form.Classes

Misere combinatorial games.

source

def MisereGames.Form.IsLong {G : Type (u + 1)} (x : G) :

Prop

The ambient space of all games, imposing no restriction. This is the counterpart of IsShort.

Equations

MisereGames.Form.IsLong x = (x = x)

Instances For

source

theorem MisereGames.Form.isLong {G : Type (u + 1)} (g : G) :

IsLong g

source

class MisereGames.Form.HasZero {G : Type (u + 1)} [Form G] (A : G → Prop) :

Prop

A set of forms containing zero.

has_zero : A 0

Instances

source

class MisereGames.Form.HasNat {G : Type (u + 1)} [Form G] (A : G → Prop) :

Prop

A set of forms containing all natural-number games.

has_nat (n : ℕ) : A ↑n

Instances

source

class MisereGames.Form.HasInt {G : Type (u + 1)} [Form G] (A : G → Prop) :

Prop

A set of forms containing all integer games.

has_int (n : ℤ) : A ↑n

Instances

source

instance MisereGames.Form.instHasZeroOfHasNat {G : Type (u + 1)} [Form G] {A : G → Prop} [HasNat A] :

HasZero A

source

instance MisereGames.Form.instHasNatOfHasInt {G : Type (u + 1)} [Form G] {A : G → Prop} [HasInt A] :

HasNat A

source

instance MisereGames.Form.instHasIntIsLong {G : Type (u + 1)} [Form G] :

HasInt IsLong

source

theorem MisereGames.Form.HasInt.has_neg_int {G : Type (u + 1)} [Form G] {A : G → Prop} [HasInt A] (n : ℕ) :

A (-↑n)

source

theorem MisereGames.Form.HasNat.zero {G : Type (u + 1)} [Form G] {A : G → Prop} [HasNat A] :

A 0

source

theorem MisereGames.Form.HasNat.one {G : Type (u + 1)} [Form G] {A : G → Prop} [HasNat A] :

A 1

source

class MisereGames.Form.ClosedUnderAddNat {G : Type (u + 1)} [Form G] (A : G → Prop) :

Prop

A set of forms closed under adding natural-number games on the right.

has_add {g : G} (h1 : A g) (n : ℕ) : A (g + ↑n)

Instances

source

instance MisereGames.Form.instClosedUnderAddNatIsLong {G : Type (u + 1)} [Form G] :

ClosedUnderAddNat IsLong

source

class MisereGames.Form.ClosedUnderAdd {G : Type (u + 1)} [Form G] (A : G → Prop) :

Prop

A set of forms closed under addition.

has_add (g h : G) (h_g : A g) (h_h : A h) : A (g + h)

Instances

source

instance MisereGames.Form.instClosedUnderAddIsLong {G : Type (u + 1)} [Form G] :

ClosedUnderAdd IsLong

source

class MisereGames.Form.Hereditary {G : Type (u + 1)} [Form G] (A : G → Prop) :

Prop

A set of forms closed under passing to options.

has_option {g g' : G} (h1 : A g) (h2 : IsOption g' g) : A g'

Instances

source

theorem MisereGames.Form.Hereditary.of_mem_moves {G : Type (u + 1)} [Form G] {A : G → Prop} [Hereditary A] {p : Player} {g g' : G} (hA : A g) (h_mem : g' ∈ moves p g) :

A g'

source

instance MisereGames.Form.instHereditaryIsLong {G : Type (u + 1)} [Form G] :

Hereditary IsLong

source

theorem MisereGames.Form.exists_isZeroLike {G : Type (u + 1)} [Form G] {A : G → Prop} [Hereditary A] (h : ∃ (g : G), A g) :

∃ (z : G), A z ∧ IsZeroLike z

A nonempty hereditary set of forms contains a zero-like form.

source

class MisereGames.Form.ClosedUnderNeg {G : Type (u + 1)} [Form G] (A : G → Prop) :

Prop

A set of forms closed under conjugation.

neg_of {g : G} (h1 : A g) : A (-g)

Instances

source

instance MisereGames.Form.instClosedUnderNegIsLong {G : Type (u + 1)} [Form G] :

ClosedUnderNeg IsLong

source

theorem MisereGames.Form.ClosedUnderNeg.neg_iff {G : Type (u + 1)} [Form G] {A : G → Prop} [ClosedUnderNeg A] {g : G} :

A (-g) ↔ A g

source

theorem MisereGames.Form.HasInt.of_hasNat {G : Type (u + 1)} [Form G] {A : G → Prop} [HasNat A] [ClosedUnderNeg A] :

HasInt A

source

theorem MisereGames.Form.ClosedUnderAddNat.has_add_neg {G : Type (u + 1)} [Form G] {A : G → Prop} [ClosedUnderAddNat A] [ClosedUnderNeg A] {g : G} (hAg : A g) (n : ℕ) :

A (g + -↑n)

source

theorem MisereGames.Form.ClosedUnderAddNat.has_add_int {G : Type (u + 1)} [Form G] {A : G → Prop} [ClosedUnderAddNat A] [ClosedUnderNeg A] [HasInt A] {g : G} (hAg : A g) (n : ℤ) :

A (g + ↑n)

source

theorem MisereGames.Form.ClosedUnderAddNat.has_add_int_neg {G : Type (u + 1)} [Form G] {A : G → Prop} [ClosedUnderAddNat A] [ClosedUnderNeg A] [HasInt A] {g : G} (hAg : A g) (n : ℤ) :

A (g + -↑n)