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.

The main result is AugmentedForm.instForm.

References

• A. N. Siegel, On the general dead-ending universe of partizan games

@[irreducible]

def AugmentedForm : Type (u + 1)

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

Equations

• AugmentedForm = QPF.Fix AugmentedFunctor✝

@[instance_reducible]

instance AugmentedForm.instMoves : Moves AugmentedForm

Equations

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

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

Check if a given Player has a tombstone.

Equations

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

def 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

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

@[instance_reducible]

instance 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 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 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 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 AugmentedForm.instSmallElemMoves (p : Player) (x : AugmentedForm) : Small.{u, u + 1} ↑(Moves.moves p x)

@[simp]

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

theorem 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 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 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

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

theorem 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

@[instance_reducible]

noncomputable instance AugmentedForm.instAdd : Add AugmentedForm

Equations

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

@[irreducible]

def AugmentedForm.ofGameForm (g : GameForm) : AugmentedForm

Convert a GameForm to an AugmentedForm with no tombstones.

Equations

• AugmentedForm.ofGameForm g = AugmentedForm.ofSetsWithTombs (fun (p : Player) => Set.range fun (gp : ↑(Moves.moves p g)) => AugmentedForm.ofGameForm ↑gp) fun (x : Player) => False

@[instance_reducible]

instance AugmentedForm.instCoeGameForm : Coe GameForm AugmentedForm

Equations

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

@[irreducible]

def AugmentedForm.TombstoneFree (g : AugmentedForm) : Prop

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

Equations

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

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

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

theorem 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 AugmentedForm.toGameForm (g : AugmentedForm) (h : g.TombstoneFree) : GameForm

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

Equations

• g.toGameForm h = !{Set.range fun (gl : ↑(Moves.moves Player.left g)) => (↑gl).toGameForm ⋯ | Set.range fun (gr : ↑(Moves.moves Player.right g)) => (↑gr).toGameForm ⋯}

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

@[simp]

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

theorem 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 AugmentedForm.ofGameForm_Injective : Function.Injective ofGameForm

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

theorem 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, irreducible]

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

@[simp, irreducible]

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

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

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

theorem 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

@[irreducible]

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

@[instance_reducible]

instance AugmentedForm.instNeg : Neg AugmentedForm

Equations

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

theorem 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

@[instance_reducible]

instance AugmentedForm.instInvolutiveNeg : InvolutiveNeg AugmentedForm

Equations

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

@[instance_reducible]

instance AugmentedForm.instAddCommSemigroup : AddCommSemigroup AugmentedForm

Equations

• AugmentedForm.instAddCommSemigroup = { toAdd := AugmentedForm.instAdd, add_assoc := AugmentedForm.instAddCommSemigroup._private_1, add_comm := AugmentedForm.instAddCommSemigroup._private_2 }

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

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

@[instance_reducible]

noncomputable instance AugmentedForm.instForm : Form AugmentedForm

Equations

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

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

theorem AugmentedForm.ofGameForm_zero : ofGameForm 0 = 0

def AugmentedForm.ofGameFormHom : GameForm →+ AugmentedForm

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

Equations

• AugmentedForm.ofGameFormHom = { toFun := AugmentedForm.ofGameForm, map_zero' := AugmentedForm.ofGameForm_zero, map_add' := AugmentedForm.ofGameForm_add }

theorem AugmentedForm.ofGameFormHom_injective : Function.Injective ⇑ofGameFormHom

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

@[simp]

theorem 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 AugmentedForm.not_isEndLike_iff {g : AugmentedForm} {p : Player} : ¬Form.IsEndLike p g ↔ ¬hasTombstone p g ∧ ¬Form.IsEnd p g

@[simp]

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

theorem 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