Misere combinatorial games.

Augmented Form

This module defines AugmentedForm: these are Siegel's augmented forms, which apart from ordinary options may also have tombstones, as defined in [Siegel, Definition 5.1 on p. 212][siegel:GeneralDeadendingUniverse:2025].

The main result is AugmentedForm.instForm.

References

• [A. N. Siegel, On the general dead-ending universe of partizan games][siegel:GeneralDeadendingUniverse:2025]

@[irreducible]

def MisereGames.AugmentedForm : Type (u + 1)

Like GameForm, but each position may contain Left and/or Right tombstones.

Equations

• MisereGames.AugmentedForm = QPF.Fix MisereGames.AugmentedFunctor✝

@[implicit_reducible]

instance MisereGames.AugmentedForm.instMoves : Moves AugmentedForm

Equations

• MisereGames.AugmentedForm.instMoves = { moves := MisereGames.AugmentedForm.moves'✝, isOption'_wf := MisereGames.AugmentedForm.instMoves._proof_1✝ }

def MisereGames.AugmentedForm.hasTombstone (p : Player) (x : AugmentedForm) : Prop

Check if a given Player has a tombstone.

Equations

• MisereGames.AugmentedForm.hasTombstone p x = (QPF.Fix.dest x).2 p

noncomputable def MisereGames.AugmentedForm.ofSetsWithTombs (st : Player → Set AugmentedForm) (tomb : Player → Prop) [Small.{u, u + 1} ↑(st Player.left)] [Small.{u, u + 1} ↑(st Player.right)] : AugmentedForm

Construct an AugmentedForm from available options and tombstones.

Equations

• MisereGames.AugmentedForm.ofSetsWithTombs st tomb = QPF.Fix.mk (⟨st, ⋯⟩, tomb)

@[implicit_reducible]

noncomputable instance MisereGames.AugmentedForm.instOfSetsTrue : OfSets AugmentedForm fun (x : Player → Set AugmentedForm) => True

Equations

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

@[simp]

theorem MisereGames.AugmentedForm.moves_ofSetsWithTombs (p : Player) (st : Player → Set AugmentedForm) (tomb : Player → Prop) [Small.{u, u + 1} ↑(st Player.left)] [Small.{u, u + 1} ↑(st Player.right)] : Moves.moves p (ofSetsWithTombs st tomb) = st p

@[simp]

theorem MisereGames.AugmentedForm.hasTombstone_ofSets (st : Player → Set AugmentedForm) [Small.{u, u + 1} ↑(st Player.left)] [Small.{u, u + 1} ↑(st Player.right)] (p : Player) : ¬hasTombstone p !{st}

@[simp]

theorem MisereGames.AugmentedForm.hasTombstone_ofSetsWithTombs (p : Player) (st : Player → Set AugmentedForm) [Small.{u, u + 1} ↑(st Player.left)] [Small.{u, u + 1} ↑(st Player.right)] (tomb : Player → Prop) : hasTombstone p (ofSetsWithTombs st tomb) = tomb p

instance MisereGames.AugmentedForm.instSmallElemMoves (p : Player) (x : AugmentedForm) : Small.{u, u + 1} ↑(Moves.moves p x)

@[simp]

theorem MisereGames.AugmentedForm.ofSets_moves_tombs (x : AugmentedForm) : (ofSetsWithTombs (fun (p : Player) => Moves.moves p x) fun (p : Player) => hasTombstone p x) = x

theorem MisereGames.AugmentedForm.ext {x y : AugmentedForm} (h_moves : ∀ (p : Player), Moves.moves p x = Moves.moves p y) (h_tomb : ∀ (p : Player), hasTombstone p x ↔ hasTombstone p y) : x = y

Two AugmentedForms are equal if they have the same options and tombstones.

theorem MisereGames.AugmentedForm.ext_iff {x y : AugmentedForm} : x = y ↔ (∀ (p : Player), Moves.moves p x = Moves.moves p y) ∧ ∀ (p : Player), hasTombstone p x ↔ hasTombstone p y

@[irreducible]

def MisereGames.AugmentedForm.moveRecOn {motive : AugmentedForm → Sort u_1} (x : AugmentedForm) (mk : (x : AugmentedForm) → ((p : Player) → (y : AugmentedForm) → y ∈ Moves.moves p x → motive y) → motive x) : motive x

This is Conway induction.

Equations

• MisereGames.AugmentedForm.moveRecOn x mk = mk x fun (p : MisereGames.Player) (y : MisereGames.AugmentedForm) (x : y ∈ MisereGames.Moves.moves p x) => MisereGames.AugmentedForm.moveRecOn y mk

theorem MisereGames.AugmentedForm.moveRecOn_eq {motive : AugmentedForm → Sort u_1} (x : AugmentedForm) (mk : (x : AugmentedForm) → ((p : Player) → (y : AugmentedForm) → y ∈ Moves.moves p x → motive y) → motive x) : moveRecOn x mk = mk x fun (x_1 : Player) (y : AugmentedForm) (x : y ∈ Moves.moves x_1 x) => moveRecOn y mk

@[implicit_reducible]

noncomputable instance MisereGames.AugmentedForm.instAdd : Add AugmentedForm

Equations

• MisereGames.AugmentedForm.instAdd = { add := MisereGames.AugmentedForm.add'✝ }

@[irreducible]

def MisereGames.AugmentedForm.ofGameForm (g : GameForm) : AugmentedForm

Convert a GameForm to an AugmentedForm with no tombstones.

Equations

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

@[implicit_reducible]

noncomputable instance MisereGames.AugmentedForm.instCoeGameForm : Coe GameForm AugmentedForm

Equations

• MisereGames.AugmentedForm.instCoeGameForm = { coe := MisereGames.AugmentedForm.ofGameForm }

@[irreducible]

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

An AugmentedForm is TombstoneFree if no player has a tombstone and all options are TombstoneFree.

Equations

• g.TombstoneFree = ((∀ (p : MisereGames.Player), ¬MisereGames.AugmentedForm.hasTombstone p g) ∧ ∀ (p : MisereGames.Player), ∀ h ∈ MisereGames.Moves.moves p g, h.TombstoneFree)

theorem MisereGames.AugmentedForm.TombstoneFree.not_hasTombstone {g : AugmentedForm} (h1 : g.TombstoneFree) (p : Player) : ¬hasTombstone p g

theorem MisereGames.AugmentedForm.TombstoneFree.moves {g : AugmentedForm} (h1 : g.TombstoneFree) (p : Player) (h : AugmentedForm) : h ∈ Moves.moves p g → h.TombstoneFree

theorem MisereGames.AugmentedForm.ofSetsWithTombs_ff_TombstoneFree {st : Player → Set AugmentedForm} [Small.{u, u + 1} ↑(st Player.left)] [Small.{u, u + 1} ↑(st Player.right)] (h1 : ∀ (p : Player), ∀ gp ∈ st p, gp.TombstoneFree) : (ofSetsWithTombs st fun (x : Player) => False).TombstoneFree

@[irreducible]

def MisereGames.AugmentedForm.toGameForm (g : AugmentedForm) (h : g.TombstoneFree) : GameForm

Convert a TombstoneFree AugmentedForm to a GameForm by 'forgetting' about the missing tombstones.

Equations

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

theorem MisereGames.AugmentedForm.ofGameForm_tombstoneFree (g : GameForm) : (ofGameForm g).TombstoneFree

@[simp]

theorem MisereGames.AugmentedForm.not_hasTombstone_ofGameForm (g : GameForm) (p : Player) : ¬hasTombstone p (ofGameForm g)

theorem MisereGames.AugmentedForm.ofSetsWithTombs_eq {as : Player → Set AugmentedForm} [Small.{u, u + 1} ↑(as Player.left)] [Small.{u, u + 1} ↑(as Player.right)] {bs : Player → Set AugmentedForm} [Small.{u, u + 1} ↑(bs Player.left)] [Small.{u, u + 1} ↑(bs Player.right)] {tombL tombR : Player → Prop} (h1 : ofSetsWithTombs as tombL = ofSetsWithTombs bs tombR) : as = bs

theorem MisereGames.AugmentedForm.ofGameForm_Injective : Function.Injective ofGameForm

theorem MisereGames.AugmentedForm.ofGameForm_moves_mem_iff {g gp : GameForm} {p : Player} : ofGameForm gp ∈ Moves.moves p (ofGameForm g) ↔ gp ∈ Moves.moves p g

theorem MisereGames.AugmentedForm.toGameForm_moves_mem' {g gp : AugmentedForm} {p : Player} (h1 : gp ∈ Moves.moves p g) (h2 : g.TombstoneFree) : gp.toGameForm ⋯ ∈ Moves.moves p (g.toGameForm h2)

@[simp]

theorem MisereGames.AugmentedForm.toGameForm_ofGameForm (g : GameForm) : (ofGameForm g).toGameForm ⋯ = g

@[simp]

theorem MisereGames.AugmentedForm.ofGameForm_toGameForm (g : AugmentedForm) (h1 : g.TombstoneFree) : ofGameForm (g.toGameForm h1) = g

theorem MisereGames.AugmentedForm.hasTombstone_add_assoc (x y z : AugmentedForm) (p : Player) : hasTombstone p (x + y + z) ↔ hasTombstone p (x + (y + z))

theorem MisereGames.AugmentedForm.ofGameForm_exists_preimage {a : AugmentedForm} (h1 : a.TombstoneFree) : ∃ (g : GameForm), ofGameForm g = a

theorem MisereGames.AugmentedForm.mem_moves_ofGameForm {g : GameForm} {ap : AugmentedForm} {p : Player} (h1 : ap ∈ Moves.moves p (ofGameForm g)) : ∃ gp ∈ Moves.moves p g, ofGameForm gp = ap

theorem MisereGames.AugmentedForm.ofGameForm_add (g h : GameForm) : ofGameForm (g + h) = ofGameForm g + ofGameForm h

@[implicit_reducible]

noncomputable instance MisereGames.AugmentedForm.instNeg : Neg AugmentedForm

Equations

• MisereGames.AugmentedForm.instNeg = { neg := MisereGames.AugmentedForm.neg'✝ }

theorem MisereGames.AugmentedForm.neg_eq (x : AugmentedForm) : -x = ofSetsWithTombs (fun (p : Player) => Set.range fun (xp : ↑(Moves.moves (-p) x)) => -↑xp) fun (p : Player) => hasTombstone (-p) x

@[implicit_reducible]

noncomputable instance MisereGames.AugmentedForm.instInvolutiveNeg : InvolutiveNeg AugmentedForm

Equations

• MisereGames.AugmentedForm.instInvolutiveNeg = { toNeg := MisereGames.AugmentedForm.instNeg, neg_neg := MisereGames.AugmentedForm.instInvolutiveNeg._private_1 }

@[implicit_reducible]

noncomputable instance MisereGames.AugmentedForm.instAddCommSemigroup : AddCommSemigroup AugmentedForm

Equations

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

theorem MisereGames.AugmentedForm.not_hasTombstone_zero' (p : Player) : ¬hasTombstone p !{fun (x : Player) => ∅}

theorem MisereGames.AugmentedForm.add_eq_zero_iff {x y : AugmentedForm} : x + y = !{fun (x : Player) => ∅} ↔ x = !{fun (x : Player) => ∅} ∧ y = !{fun (x : Player) => ∅}

@[implicit_reducible]

noncomputable instance MisereGames.AugmentedForm.instForm : Form AugmentedForm

Equations

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

theorem MisereGames.AugmentedForm.IsEndLike_iff {g : AugmentedForm} {p : Player} : Form.IsEndLike p g ↔ hasTombstone p g ∨ Form.IsEnd p g

theorem MisereGames.AugmentedForm.ofGameForm_zero : ofGameForm 0 = 0

noncomputable def MisereGames.AugmentedForm.ofGameFormHom : GameForm →+ AugmentedForm

The coercion from GameForm to AugmentedForm is an additive monoid homomorphism.

Equations

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

theorem MisereGames.AugmentedForm.ofGameFormHom_injective : Function.Injective ⇑ofGameFormHom

theorem MisereGames.AugmentedForm.hasTombstone_neg_iff {g : AugmentedForm} {p : Player} : hasTombstone p (-g) ↔ hasTombstone (-p) g

@[simp]

theorem MisereGames.AugmentedForm.hasTombstone_add {x y : AugmentedForm} {p : Player} : hasTombstone p (x + y) ↔ hasTombstone p x ∧ Form.IsEndLike p y ∨ hasTombstone p y ∧ Form.IsEndLike p x

theorem MisereGames.AugmentedForm.not_isEndLike_iff {g : AugmentedForm} {p : Player} : ¬Form.IsEndLike p g ↔ ¬hasTombstone p g ∧ ¬Form.IsEnd p g

@[simp]

theorem MisereGames.AugmentedForm.isEndLike_ofGameForm_iff_isEnd {g : GameForm} {p : Player} : Form.IsEndLike p (ofGameForm g) ↔ Form.IsEnd p g

theorem MisereGames.AugmentedForm.mem_ofGameForm_exists_mem {g : GameForm} {gp : AugmentedForm} {p : Player} (h1 : gp.TombstoneFree) (h2 : gp ∈ Moves.moves p (ofGameForm g)) : ∃ gp' ∈ Moves.moves p g, ofGameForm gp' = gp