Misere combinatorial games.

Normal augmented forms

An augmented form is normal when every subposition is both Left and Right end-like. Normal forms are invertible modulo any set of forms, so they form a subgroup of the invertible subgroup of both the long augmented misère monoid (all augmented forms) and the short one.

Note that comparing two normal forms modulo a promain set relies only on the maintenance, since the proviso is always satisfied.

Comparison of end-like forms

theorem MisereGames.Form.Strong.of_isEndLike {G : Type (u + 1)} [Form G] {A : G → Prop} {h : G} {p : Player} (hh : IsEndLike p h) : Strong A h p

An end-like form wins going first against any end-like test form, so it is strong.

theorem MisereGames.Form.misereGE_of_maintenance_of_isEndLike {G : Type (u + 1)} [Form G] {A : G → Prop} [Hereditary A] {g h : G} (hg : IsEndLike Player.left g) (hh : IsEndLike Player.right h) (hr : Maintenance A g h Player.right) (hl : Maintenance A g h Player.left) : g ≥m A h

When g and h are end-like for both players, the proviso is automatic, so g ≥m A h follows from maintenance alone.

theorem MisereGames.Form.misereGE_iff_maintenance_of_isEndLike {G : Type (u + 1)} [Form G] {A IsAmbient : G → Prop} (h_promain : Promain IsAmbient A) {g h : G} (hg : ∀ (p : Player), IsEndLike p g) (hh : ∀ (p : Player), IsEndLike p h) (hgA : IsAmbient g) (hhA : IsAmbient h) : g ≥m A h ↔ Maintenance A g h Player.right ∧ Maintenance A g h Player.left

For forms that are end-like for both players, comparison modulo a promain set A drops the proviso: g ≥m A h is just maintenance.

Normal forms

@[irreducible]

def MisereGames.AugmentedForm.Normal (g : AugmentedForm) : Prop

An augmented form is normal if every subposition is end-like for both players.

Equations

• One or more equations did not get rendered due to their size.

theorem MisereGames.AugmentedForm.Normal.isEndLike {g : AugmentedForm} (hg : g.Normal) (p : Player) : Form.IsEndLike p g

theorem MisereGames.AugmentedForm.Normal.moves {g h : AugmentedForm} (hg : g.Normal) {p : Player} (hh : h ∈ Moves.moves p g) : h.Normal

theorem MisereGames.AugmentedForm.Normal.add_neg_isEndLike {g : AugmentedForm} (hg : g.Normal) (p : Player) : Form.IsEndLike p (g + -g)

theorem MisereGames.AugmentedForm.Normal.neg {g : AugmentedForm} (hg : g.Normal) : (-g).Normal

@[simp]

theorem MisereGames.AugmentedForm.Normal.zero : Normal 0

theorem MisereGames.AugmentedForm.Normal.add {g h : AugmentedForm} (hg : g.Normal) (hh : h.Normal) : (g + h).Normal

theorem MisereGames.AugmentedForm.Normal.misereGE_iff_maintenance {g h : AugmentedForm} (hg : g.Normal) (hh : h.Normal) : g ≥m Form.IsLong h ↔ Form.Maintenance Form.IsLong g h Player.right ∧ Form.Maintenance Form.IsLong g h Player.left

theorem MisereGames.AugmentedForm.Normal.misereGE_iff_maintenance_isShort {g h : AugmentedForm} (hgs : Form.IsShort g) (hhs : Form.IsShort h) (hg : g.Normal) (hh : h.Normal) : g ≥m Form.IsShort h ↔ Form.Maintenance Form.IsShort g h Player.right ∧ Form.Maintenance Form.IsShort g h Player.left

theorem MisereGames.AugmentedForm.Normal.add_neg_misereEQ_zero {g : AugmentedForm} (hg : g.Normal) : (g + -g) =m Form.IsLong 0

theorem MisereGames.AugmentedForm.Normal.neg_add_misereEQ_zero {g : AugmentedForm} (hg : g.Normal) : (-g + g) =m Form.IsLong 0

The augmented misère monoids and the 'normal' subgroup

@[reducible, inline]

abbrev MisereGames.Form.MisereQuotient.Augmented.LongQuotient : Type (u + 1)

The long augmented misère monoid: augmented forms modulo misère equality.

Equations

• MisereGames.Form.MisereQuotient.Augmented.LongQuotient = MisereGames.MisereQuotient MisereGames.Form.IsLong

noncomputable def MisereGames.Form.MisereQuotient.Augmented.mkLong (g : AugmentedForm) : LongQuotient

The class of an augmented form in the long quotient.

Equations

• MisereGames.Form.MisereQuotient.Augmented.mkLong g = MisereGames.Form.MisereQuotient.mk ⟨g, ⋯⟩

@[simp]

theorem MisereGames.Form.MisereQuotient.Augmented.mkLong_add (g h : AugmentedForm) : mkLong (g + h) = mkLong g + mkLong h

@[simp]

theorem MisereGames.Form.MisereQuotient.Augmented.mkLong_zero : mkLong 0 = 0

theorem MisereGames.Form.MisereQuotient.Augmented.mkLong_add_neg {g : AugmentedForm} (hg : g.Normal) : mkLong g + mkLong (-g) = 0

theorem MisereGames.Form.MisereQuotient.Augmented.mkLong_neg_add {g : AugmentedForm} (hg : g.Normal) : mkLong (-g) + mkLong g = 0

theorem MisereGames.Form.MisereQuotient.Augmented.isAddUnit_mkLong_of_normal {g : AugmentedForm} (hg : g.Normal) : IsAddUnit (mkLong g)

noncomputable def MisereGames.Form.MisereQuotient.Augmented.normalLong : AddSubgroup (AddUnits LongQuotient)

The normal augmented forms form a subgroup of the invertible subgroup of the long quotient monoid.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev MisereGames.Form.MisereQuotient.Augmented.ShortQuotient : Type (u + 1)

The short augmented misère monoid: short augmented forms modulo misère equality.

Equations

• MisereGames.Form.MisereQuotient.Augmented.ShortQuotient = MisereGames.MisereQuotient MisereGames.Form.IsShort

noncomputable def MisereGames.Form.MisereQuotient.Augmented.mkShort (g : AugmentedForm) (hg : IsShort g) : ShortQuotient

The class of a short augmented form in the short quotient.

Equations

• MisereGames.Form.MisereQuotient.Augmented.mkShort g hg = MisereGames.Form.MisereQuotient.mk ⟨g, hg⟩

@[simp]

theorem MisereGames.Form.MisereQuotient.Augmented.mkShort_add (g h : AugmentedForm) (hg : IsShort g) (hh : IsShort h) : mkShort (g + h) ⋯ = mkShort g hg + mkShort h hh

@[simp]

theorem MisereGames.Form.MisereQuotient.Augmented.mkShort_zero : mkShort 0 ⋯ = 0

theorem MisereGames.Form.MisereQuotient.Augmented.mkShort_add_neg {g : AugmentedForm} (hgs : IsShort g) (hg : g.Normal) : mkShort g hgs + mkShort (-g) ⋯ = 0

theorem MisereGames.Form.MisereQuotient.Augmented.mkShort_neg_add {g : AugmentedForm} (hgs : IsShort g) (hg : g.Normal) : mkShort (-g) ⋯ + mkShort g hgs = 0

theorem MisereGames.Form.MisereQuotient.Augmented.isAddUnit_mkShort_of_normal {g : AugmentedForm} (hgs : IsShort g) (hg : g.Normal) : IsAddUnit (mkShort g hgs)

noncomputable def MisereGames.Form.MisereQuotient.Augmented.normalShort : AddSubgroup (AddUnits ShortQuotient)

The short normal augmented forms form a subgroup of the invertible subgroup of the short quotient monoid.

Equations

• One or more equations did not get rendered due to their size.