Loopy games

The standard notion of a game studied in combinatorial game theory is that of a terminating game, meaning that there exists no infinite sequence of moves. Loopy games relax this condition by allowing "self-refential" games, with the basic examples being on = {on | }, off = { | off}, and dud = {dud | dud}.

In the literature, loopy games are defined as rooted directed graphs up to isomorphism. However, it's simpler to define LGame as the coinductive type for the single constructor:

  | ofSets (s t : Set LGame.{u}) [Small.{u} s] [Small.{u} t] : LGame.{u}

(The inductive type for this same constructor would be IGame.) This gives us a powerful corecursion principle LGame.corec, which can be interpreted as saying "for any graph we can draw on a type α, as long as the amount of branches per node is u-small, there's an LGame isomorphic to it".

Although extensionality still holds, it's not always sufficient to prove two games equal. For instance, if x = !{x | x} and y = !{y | y}, then x = y, but trying to use extensionality to prove this just leads to a cyclic argument. Instead, we can use LGame.eq_of_bisim, which can roughly be interpreted as saying "if two games have the same shape, they're equal". In this case, the relation r a b ↔ a = x ∧ b = y is a bisimulation between both games, which proves their equality.

For Mathlib

theorem small_succ' (α : Type u) [Small.{v, u} α] : Small.{v + 1, u} α

theorem QPF.Cofix.unique {F : Type u → Type u} [QPF F] {α : Type u} (a : α → F α) (f g : α → Cofix F) (hf : dest ∘ f = Functor.map f ∘ a) (hg : dest ∘ g = Functor.map g ∘ a) : f = g

Game moves

@[irreducible]

def LGame : Type (u_1 + 1)

The type of loopy games.

Most games studied within game theory are terminating, which means that the IsOption relation is well-founded. A loopy game relaxes this constraint. Thus, LGame contains all normal IGames, but it also contains games such as on = {on | }, off = { | off}, and dud = {dud | dud}.

See the module docstring for guidance on how to make use of this type.

Equations

• LGame = QPF.Cofix GameFunctor

instance LGame.instDecidableEq : DecidableEq LGame

Equations

• LGame.instDecidableEq = Classical.decEq LGame

def LGame.moves (p : Player) (x : LGame) : Set LGame

The set of moves of the game.

Equations

• LGame.moves p x = ↑(QPF.Cofix.dest x) p

def LGame.«term_ᴸ» : Lean.TrailingParserDescr

The set of left moves of the game.

Equations

• LGame.«term_ᴸ» = Lean.ParserDescr.trailingNode `LGame.«term_ᴸ» 1024 1024 (Lean.ParserDescr.symbol "ᴸ")

def LGame.«term_ᴿ» : Lean.TrailingParserDescr

The set of right moves of the game.

Equations

• LGame.«term_ᴿ» = Lean.ParserDescr.trailingNode `LGame.«term_ᴿ» 1024 1024 (Lean.ParserDescr.symbol "ᴿ")

instance LGame.small_moves (p : Player) (x : LGame) : Small.{u, u + 1} ↑(moves p x)

def LGame.IsOption (x y : LGame) : Prop

IsOption x y means that x is either a left or a right move for y.

Equations

• x.IsOption y = (x ∈ ⋃ (p : Player), LGame.moves p y)

theorem LGame.isOption_iff_mem_union {x y : LGame} : x.IsOption y ↔ x ∈ moves left y ∪ moves right y

theorem LGame.IsOption.of_mem_moves {p : Player} {x y : LGame} (h : x ∈ moves p y) : x.IsOption y

instance LGame.instSmallSubtypeIsOption (x : LGame) : Small.{u, u + 1} { y : LGame // y.IsOption x }

def LGame.Subposition : LGame → LGame → Prop

A (proper) subposition is any game in the transitive closure of IsOption.

Equations

• LGame.Subposition = Relation.TransGen LGame.IsOption

theorem LGame.Subposition.of_mem_moves {p : Player} {x y : LGame} (h : x ∈ moves p y) : x.Subposition y

theorem LGame.Subposition.trans {x y z : LGame} (h₁ : x.Subposition y) (h₂ : y.Subposition z) : x.Subposition z

instance LGame.instSmallSubtypeSubposition (x : LGame) : Small.{u, u + 1} { y : LGame // y.Subposition x }

theorem LGame.eq_of_bisim (r : LGame → LGame → Prop) (H : ∀ (x y : LGame), r x y → ∀ (p : Player), ∃ (s : Set (LGame × LGame)), Prod.fst '' s = moves p x ∧ Prod.snd '' s = moves p y ∧ ∀ z ∈ s, r z.1 z.2) {x y : LGame} (hxy : r x y) : x = y

Two loopy games are equal when there exists a bisimulation between them.

A way to think about this is that r defines a pairing between nodes of the game trees, which then shows that the trees are isomorphic.

theorem LGame.ext {x y : LGame} (h : ∀ (p : Player), moves p x = moves p y) : x = y

Two LGames are equal when their move sets are.

This is not always sufficient to prove that two games are equal. For instance, if x = !{x | x} and y = !{y | y}, then x = y, but trying to use extensionality to prove this just leads to a cyclic argument. For these situations, you can use eq_of_bisim instead.

theorem LGame.ext_iff {x y : LGame} : x = y ↔ ∀ (p : Player), moves p x = moves p y

def LGame.corec {α : Type v} (mov : Player → α → Set α) [∀ (a : α), Small.{u, v} ↑(mov left a)] [∀ (a : α), Small.{u, v} ↑(mov right a)] (init : α) : LGame

The corecursor on LGame.

You can use this in order to define an arbitrary LGame by "drawing" its move graph on some other type. As an example, on = !{on | } is defined as corec (Player.cases ⊤ ⊥) ().

Equations

• LGame.corec mov init = LGame.corec'✝ mov init ⟨init, ⋯⟩

@[simp]

theorem LGame.moves_corec {α : Type v} (p : Player) (mov : Player → α → Set α) [∀ (a : α), Small.{u, v} ↑(mov left a)] [∀ (a : α), Small.{u, v} ↑(mov right a)] (init : α) : moves p (corec mov init) = corec mov '' mov p init

theorem LGame.moves_comp_corec {α : Type v} (p : Player) (mov : Player → α → Set α) [∀ (a : α), Small.{u, v} ↑(mov left a)] [∀ (a : α), Small.{u, v} ↑(mov right a)] : moves p ∘ corec mov = Set.image (corec mov) ∘ mov p

theorem LGame.hom_unique_apply {α : Type v} {mov : Player → α → Set α} [∀ (a : α), Small.{u, v} ↑(mov left a)] [∀ (a : α), Small.{u, v} ↑(mov right a)] (f g : α → LGame) (hf : ∀ (p : Player), moves p ∘ f = Set.image f ∘ mov p) (hg : ∀ (p : Player), moves p ∘ g = Set.image g ∘ mov p) (x : α) : f x = g x

theorem LGame.hom_unique {α : Type v} {mov : Player → α → Set α} [∀ (a : α), Small.{u, v} ↑(mov left a)] [∀ (a : α), Small.{u, v} ↑(mov right a)] (f g : α → LGame) (hf : ∀ (p : Player), moves p ∘ f = Set.image f ∘ mov p) (hg : ∀ (p : Player), moves p ∘ g = Set.image g ∘ mov p) : f = g

theorem LGame.corec_comp_hom {α : Type v} {β : Type w} {movα : Player → α → Set α} {movβ : Player → β → Set β} [∀ (a : α), Small.{u, v} ↑(movα left a)] [∀ (a : α), Small.{u, v} ↑(movα right a)] [∀ (b : β), Small.{u, w} ↑(movβ left b)] [∀ (b : β), Small.{u, w} ↑(movβ right b)] (f : α → β) (hf : ∀ (p : Player), movβ p ∘ f = Set.image f ∘ movα p) : corec movβ ∘ f = corec movα

theorem LGame.corec_comp_hom_apply {α : Type v} {β : Type w} {movα : Player → α → Set α} {movβ : Player → β → Set β} [∀ (a : α), Small.{u, v} ↑(movα left a)] [∀ (a : α), Small.{u, v} ↑(movα right a)] [∀ (b : β), Small.{u, w} ↑(movβ left b)] [∀ (b : β), Small.{u, w} ↑(movβ right b)] (f : α → β) (hf : ∀ (p : Player), movβ p ∘ f = Set.image f ∘ movα p) (x : α) : corec movβ (f x) = corec movα x

@[simp]

theorem LGame.corec_moves : corec moves = id

theorem LGame.corec_moves_apply (x : LGame) : corec moves x = x

instance LGame.instOfSetsTrue : OfSets LGame fun (x : Player → Set LGame) => True

Construct an LGame from its left and right sets.

It's not possible to create a non-well-founded game through this constructor alone. For that, see LGame.corec.

Equations

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

@[simp]

theorem LGame.moves_ofSets (p : Player) (lr : Player → Set LGame) [Small.{u, u + 1} ↑(lr left)] [Small.{u, u + 1} ↑(lr right)] : moves p !{lr} = lr p

theorem LGame.leftMoves_ofSets (l r : Set LGame) [Small.{u, u + 1} ↑l] [Small.{u, u + 1} ↑r] : moves left !{l | r} = l

theorem LGame.rightMoves_ofSets (l r : Set LGame) [Small.{u, u + 1} ↑l] [Small.{u, u + 1} ↑r] : moves right !{l | r} = r

Basic games

instance LGame.instZero : Zero LGame

The game 0 = !{∅ | ∅}.

Equations

• LGame.instZero = { zero := !{fun (x : Player) => ∅} }

theorem LGame.zero_def : 0 = !{fun (x : Player) => ∅}

@[simp]

theorem LGame.moves_zero (p : Player) : moves p 0 = ∅

instance LGame.instInhabited : Inhabited LGame

Equations

• LGame.instInhabited = { default := 0 }

instance LGame.instOne : One LGame

The game 1 = !{{0} | ∅}.

Equations

• LGame.instOne = { one := !{{0} | ∅} }

theorem LGame.one_def : 1 = !{{0} | ∅}

@[simp]

theorem LGame.leftMoves_one : moves left 1 = {0}

@[simp]

theorem LGame.rightMoves_one : moves right 1 = ∅

def LGame.on : LGame

The game on = !{{on} | ∅}.

Equations

• LGame.on = LGame.corec (Player.cases ⊤ ⊥) ()

@[simp]

theorem LGame.leftMoves_on : moves left on = {on}

@[simp]

theorem LGame.rightMoves_on : moves right on = ∅

@[simp]

theorem LGame.isOption_on_iff {x : LGame} : x.IsOption on ↔ x = on

theorem LGame.on_eq : on = !{{on} | ∅}

theorem LGame.eq_on {x : LGame} : x = on ↔ moves left x = {x} ∧ moves right x = ∅

def LGame.off : LGame

The game off = !{∅ | {off}}.

Equations

• LGame.off = LGame.corec (Player.cases ⊥ ⊤) ()

@[simp]

theorem LGame.leftMoves_off : moves left off = ∅

@[simp]

theorem LGame.rightMoves_off : moves right off = {off}

@[simp]

theorem LGame.isOption_off_iff {x : LGame} : x.IsOption off ↔ x = off

theorem LGame.off_eq : off = !{∅ | {off}}

theorem LGame.eq_off {x : LGame} : x = off ↔ moves left x = ∅ ∧ moves right x = {x}

def LGame.dud : LGame

The game dud = !{{dud} | {dud}}.

Equations

• LGame.dud = LGame.corec (Player.cases ⊤ ⊤) ()

@[simp]

theorem LGame.moves_dud (p : Player) : moves p dud = {dud}

@[simp]

theorem LGame.isOption_dud_iff {x : LGame} : x.IsOption dud ↔ x = dud

theorem LGame.dud_eq : dud = !{{dud} | {dud}}

theorem LGame.eq_dud {x : LGame} : x = dud ↔ moves left x = {x} ∧ moves right x = {x}

def LGame.tis : LGame

The game tis = !{{tisn} | ∅}, where tisn = !{∅ | {tis}}.

Equations

• LGame.tis = LGame.corec (Player.cases (fun (t : Bool) => Bool.rec ∅ {false} t) fun (t : Bool) => Bool.rec {true} ∅ t) true

def LGame.tisn : LGame

The game tisn = !{∅ | {tis}}, where tis = !{{tisn} | ∅}.

Equations

• LGame.tisn = LGame.corec (Player.cases (fun (t : Bool) => Bool.rec ∅ {false} t) fun (t : Bool) => Bool.rec {true} ∅ t) false

@[simp]

theorem LGame.leftMoves_tis : moves left tis = {tisn}

@[simp]

theorem LGame.rightMoves_tis : moves right tis = ∅

theorem LGame.tis_eq : tis = !{{tisn} | ∅}

@[simp]

theorem LGame.leftMoves_tisn : moves left tisn = ∅

@[simp]

theorem LGame.rightMoves_tisn : moves right tisn = {tis}

theorem LGame.tisn_eq : tisn = !{∅ | {tis}}

Negation

instance LGame.instNeg : Neg LGame

The negative of a game is defined by -!{s | t} = !{-t | -s}.

Equations

• LGame.instNeg = { neg := LGame.corec fun (p : Player) => LGame.moves (-p) }

@[simp]

theorem LGame.corec_moves_neg : (corec fun (p : Player) => moves (-p)) = fun (x : LGame) => -x

theorem LGame.corec_moves_neg_apply (x : LGame) : corec (fun (p : Player) => moves (-p)) x = -x

theorem LGame.neg_corec {α : Type v} (mov : Player → α → Set α) [∀ (x : α), Small.{u, v} ↑(mov left x)] [∀ (x : α), Small.{u, v} ↑(mov right x)] : -corec mov = corec fun (p : Player) => mov (-p)

theorem LGame.neg_corec_apply {α : Type v} (mov : Player → α → Set α) [∀ (x : α), Small.{u, v} ↑(mov left x)] [∀ (x : α), Small.{u, v} ↑(mov right x)] (init : α) : -corec mov init = corec (fun (p : Player) => mov (-p)) init

instance LGame.instInvolutiveNeg : InvolutiveNeg LGame

Equations

• LGame.instInvolutiveNeg = { toNeg := LGame.instNeg, neg_neg := LGame.instInvolutiveNeg._proof_1 }

@[simp]

theorem LGame.moves_neg (p : Player) (x : LGame) : moves p (-x) = -moves (-p) x

@[simp]

theorem LGame.neg_ofSets (s t : Set LGame) [Small.{u, u + 1} ↑s] [Small.{u, u + 1} ↑t] : -!{s | t} = !{-t | -s}

theorem LGame.neg_ofSets' (st : Player → Set LGame) [Small.{u_1, u_1 + 1} ↑(st left)] [Small.{u_1, u_1 + 1} ↑(st right)] : -!{st} = !{fun (p : Player) => -st (-p)}

@[simp]

theorem LGame.neg_ofSets_const (s : Set LGame) [Small.{u_1, u_1 + 1} ↑s] : -!{fun (x : Player) => s} = !{fun (x : Player) => -s}

instance LGame.instNegZeroClass : NegZeroClass LGame

Equations

• LGame.instNegZeroClass = { toZero := LGame.instZero, toNeg := LGame.instNeg, neg_zero := LGame.instNegZeroClass._proof_1 }

@[simp]

theorem LGame.neg_on : -on = off

@[simp]

theorem LGame.neg_off : -off = on

@[simp]

theorem LGame.neg_dud : -dud = dud

@[simp]

theorem LGame.neg_tis : -tis = tisn

@[simp]

theorem LGame.neg_tisn : -tisn = tis

Addition

instance LGame.instAdd : Add LGame

The sum of x = !{s₁ | t₁} and y = !{s₂ | t₂} is !{s₁ + y, x + s₂ | t₁ + y, x + t₂}.

Equations

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

theorem LGame.corec_add_corec {α : Type v} {β : Type w} {movα : Player → α → Set α} {movβ : Player → β → Set β} [∀ (x : α), Small.{u, v} ↑(movα left x)] [∀ (x : α), Small.{u, v} ↑(movα right x)] [∀ (x : β), Small.{u, w} ↑(movβ left x)] [∀ (x : β), Small.{u, w} ↑(movβ right x)] (initα : α) (initβ : β) : corec movα initα + corec movβ initβ = corec (fun (p : Player) (x : α × β) => (fun (y : α) => (y, x.2)) '' movα p x.1 ∪ (fun (y : β) => (x.1, y)) '' movβ p x.2) (initα, initβ)

@[simp]

theorem LGame.moves_add (p : Player) (x y : LGame) : moves p (x + y) = (fun (x : LGame) => x + y) '' moves p x ∪ (fun (x_1 : LGame) => x + x_1) '' moves p y

@[simp]

theorem LGame.add_eq_zero_iff {x y : LGame} : x + y = 0 ↔ x = 0 ∧ y = 0

instance LGame.instAddCommMonoid : AddCommMonoid LGame

Equations

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

@[simp]

theorem LGame.on_add_off : on + off = dud

@[simp]

theorem LGame.off_add_on : off + on = dud

@[simp]

theorem LGame.add_dud (x : LGame) : x + dud = dud

@[simp]

theorem LGame.dud_add (x : LGame) : dud + x = dud

theorem LGame.moves_sum (p : Player) (m : Multiset LGame) : moves p m.sum = ⋃ y ∈ m, (fun (x : LGame) => x + (m.erase y).sum) '' moves p y

instance LGame.instSubNegMonoid : SubNegMonoid LGame

The subtraction of x and y is defined as x + (-y).

Equations

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

theorem LGame.corec_sub_corec {α : Type v} {β : Type w} {movα : Player → α → Set α} {movβ : Player → β → Set β} [∀ (x : α), Small.{u, v} ↑(movα left x)] [∀ (x : α), Small.{u, v} ↑(movα right x)] [∀ (x : β), Small.{u, w} ↑(movβ left x)] [∀ (x : β), Small.{u, w} ↑(movβ right x)] (initα : α) (initβ : β) : corec movα initα - corec movβ initβ = corec (fun (p : Player) (x : α × β) => (fun (y : α) => (y, x.2)) '' movα p x.1 ∪ (fun (y : β) => (x.1, y)) '' movβ (-p) x.2) (initα, initβ)

@[simp]

theorem LGame.moves_sub (p : Player) (x y : LGame) : moves p (x - y) = (fun (x : LGame) => x - y) '' moves p x ∪ (fun (x_1 : LGame) => x + x_1) '' (-moves (-p) y)

instance LGame.instSubtractionCommMonoid : SubtractionCommMonoid LGame

Equations

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

@[simp]

theorem LGame.on_sub_on : on - on = dud

@[simp]

theorem LGame.off_sub_off : off - off = dud

@[simp]

theorem LGame.sub_dud (x : LGame) : x - dud = dud

Multiplication

@[reducible, inline]

abbrev LGame.MulTy (α : Type u_1) (β : Type u_2) : Type (max u_2 u_1)

Given two game graphs drawn on types α and β, the graph for the product can be drawn on the type Multiset (Player × α × β). Each term corresponds to a sum Σ ±aᵢ * bᵢ, where aᵢ and bᵢ are terms of α and β respectively, and the attached player represents each term's sign.

Equations

• LGame.MulTy α β = Multiset (Player × α × β)

instance LGame.MulTy.instInvolutiveNeg {α : Type v} {β : Type w} : InvolutiveNeg (MulTy α β)

Inverts the sign of all entries.

Equations

• LGame.MulTy.instInvolutiveNeg = { neg := fun (x : LGame.MulTy α β) => Multiset.map (fun (y : Player × α × β) => (-y.1, y.2)) x, neg_neg := ⋯ }

theorem LGame.MulTy.neg_def {α : Type v} {β : Type w} (x : MulTy α β) : -x = Multiset.map (fun (y : Player × α × β) => (-y.1, y.2)) x

@[simp]

theorem LGame.MulTy.mem_neg {α : Type v} {β : Type w} {x : Player × α × β} {y : MulTy α β} : x ∈ -y ↔ (-x.1, x.2) ∈ y

@[simp]

theorem LGame.MulTy.neg_zero {α : Type v} {β : Type w} : -0 = 0

@[simp]

theorem LGame.MulTy.neg_singleton {α : Type v} {β : Type w} (a : Player × α × β) : -{a} = {(-a.1, a.2)}

@[simp]

theorem LGame.MulTy.neg_cons {α : Type v} {β : Type w} (a : Player × α × β) (x : MulTy α β) : -(a ::ₘ x) = (-a.1, a.2) ::ₘ -x

@[simp]

theorem LGame.MulTy.neg_add {α : Type v} {β : Type w} (x y : MulTy α β) : -(x + y) = -x + -y

@[simp]

theorem LGame.MulTy.neg_erase {α : Type v} {β : Type w} [DecidableEq α] [DecidableEq β] (x : MulTy α β) (a : Player × α × β) : -Multiset.erase x a = Multiset.erase (-x) (-a.1, a.2)

def LGame.MulTy.swap {α : Type v} {β : Type w} (x : MulTy α β) : MulTy β α

Swaps the entries in all pairs.

Equations

• x.swap = Multiset.map (fun (a : Player × α × β) => (a.1, a.2.swap)) x

theorem LGame.MulTy.swap_def {α : Type v} {β : Type w} (x : MulTy α β) : x.swap = Multiset.map (fun (a : Player × α × β) => (a.1, a.2.swap)) x

@[simp]

theorem LGame.MulTy.mem_swap {α : Type v} {β : Type w} {x : Player × β × α} {y : MulTy α β} : x ∈ y.swap ↔ (x.1, x.2.swap) ∈ y

@[simp]

theorem LGame.MulTy.swap_zero {α : Type v} {β : Type w} : swap 0 = 0

@[simp]

theorem LGame.MulTy.swap_singleton {α : Type v} {β : Type w} (a : Player × α × β) : {a}.swap = {(a.1, a.2.swap)}

@[simp]

theorem LGame.MulTy.swap_cons {α : Type v} {β : Type w} (a : Player × α × β) (x : MulTy α β) : swap (a ::ₘ x) = (a.1, a.2.swap) ::ₘ x.swap

@[simp]

theorem LGame.MulTy.swap_add {α : Type v} {β : Type w} (x y : MulTy α β) : (x + y).swap = x.swap + y.swap

@[simp]

theorem LGame.MulTy.swap_erase {α : Type v} {β : Type w} [DecidableEq α] [DecidableEq β] (x : MulTy α β) (a : Player × α × β) : swap (Multiset.erase x a) = Multiset.erase x.swap (a.1, a.2.swap)

def LGame.MulTy.mulOption {α : Type v} {β : Type w} (p : Player) (x y : α × β) : MulTy α β

The general form of an option of x * y is a * y + x * b - a * b.

If the player argument is left, all signs are flipped.

Equations

• LGame.MulTy.mulOption p x y = {(p, y.1, x.2), (p, x.1, y.2), (-p, y.1, y.2)}

@[simp]

theorem LGame.MulTy.neg_mulOption {α : Type v} {β : Type w} (p : Player) (x y : α × β) : -mulOption p x y = mulOption (-p) x y

@[simp]

theorem LGame.MulTy.swap_mulOption {α : Type v} {β : Type w} (p : Player) (x y : α × β) : (mulOption p x y).swap = mulOption p x.swap y.swap

theorem LGame.MulTy.mulOption_eq_add {α : Type v} {β : Type w} (p : Player) (x y : α × β) : mulOption p x y = {(p, y.1, x.2)} + {(p, x.1, y.2)} + {(-p, y.1, y.2)}

def LGame.MulTy.movesSet {α : Type v} {β : Type w} (p : Player) (movα : Player → α → Set α) (movβ : Player → β → Set β) (x : Player × α × β) : Set (α × β)

The set of pairs α × β used in movesSingle.

Equations

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

theorem LGame.MulTy.movesSet_neg {α : Type v} {β : Type w} (p : Player) (movα : Player → α → Set α) (movβ : Player → β → Set β) (x : Player × α × β) : movesSet p movα movβ (-x.1, x.2) = movesSet (-p) movα movβ x

theorem LGame.MulTy.movesSet_neg' (p : Player) (x : Player × LGame × LGame) : movesSet p moves moves (x.1, -x.2.1, x.2.2) = (fun (y : LGame × LGame) => (-y.1, y.2)) '' movesSet (-p) moves moves x

theorem LGame.MulTy.movesSet_swap {α : Type v} {β : Type w} (p : Player) (movα : Player → α → Set α) (movβ : Player → β → Set β) (x : Player × α × β) : movesSet p movβ movα (x.1, x.2.swap) = Prod.swap '' movesSet p movα movβ x

def LGame.MulTy.movesSingle {α : Type v} {β : Type w} (p : Player) (movα : Player → α → Set α) (movβ : Player → β → Set β) (x : Player × α × β) : Set (MulTy α β)

The left or right moves of ±x * y are left or right moves of x * y if the sign is positive, or the negatives of right or left moves of x * y if the sign is negative.

Equations

• LGame.MulTy.movesSingle p movα movβ x = LGame.MulTy.mulOption x.1 x.2 '' LGame.MulTy.movesSet p movα movβ x

theorem LGame.MulTy.movesSingle_neg {α : Type v} {β : Type w} (p : Player) (movα : Player → α → Set α) (movβ : Player → β → Set β) (x : Player × α × β) : movesSingle p movα movβ (-x.1, x.2) = -movesSingle (-p) movα movβ x

theorem LGame.MulTy.movesSingle_neg' (p : Player) (x : Player × LGame × LGame) : movesSingle p moves moves (x.1, -x.2.1, x.2.2) = (Multiset.map fun (y : Player × LGame × LGame) => (y.1, -y.2.1, y.2.2)) '' movesSingle (-p) moves moves x

theorem LGame.MulTy.movesSingle_swap {α : Type v} {β : Type w} (p : Player) (movα : Player → α → Set α) (movβ : Player → β → Set β) (x : Player × α × β) : movesSingle p movβ movα (x.1, x.2.swap) = swap '' movesSingle p movα movβ x

def LGame.MulTy.moves {α : Type v} {β : Type w} (p : Player) (movα : Player → α → Set α) (movβ : Player → β → Set β) [Hα : DecidableEq α] [Hβ : DecidableEq β] (x : MulTy α β) : Set (MulTy α β)

The set of left or right moves of Σ ±xᵢ * yᵢ are zᵢ + Σ ±xⱼ * yⱼ for all i, where cᵢ is a left or right move of ±xᵢ * yᵢ, and the summation is taken over indices j ≠ i.

Equations

• LGame.MulTy.moves p movα movβ x = ⋃ y ∈ x, (fun (x_1 : LGame.MulTy α β) => Multiset.erase x y + x_1) '' LGame.MulTy.movesSingle p movα movβ y

theorem Multiset.iUnion_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (m : Multiset α) (f : α → β) (g : β → Set γ) : ⋃ x ∈ map f m, g x = ⋃ x ∈ m, g (f x)

theorem LGame.MulTy.moves_neg {α : Type v} {β : Type w} (p : Player) (movα : Player → α → Set α) (movβ : Player → β → Set β) [Hα : DecidableEq α] [Hβ : DecidableEq β] (x : MulTy α β) : MulTy.moves p movα movβ (-x) = -MulTy.moves (-p) movα movβ x

theorem LGame.MulTy.moves_neg' (p : Player) (x : MulTy LGame LGame) : MulTy.moves p moves moves (Multiset.map (fun (y : Player × LGame × LGame) => (y.1, -y.2.1, y.2.2)) x) = (Multiset.map fun (y : Player × LGame × LGame) => (y.1, -y.2.1, y.2.2)) '' MulTy.moves (-p) moves moves x

theorem LGame.MulTy.moves_swap {α : Type v} {β : Type w} (p : Player) (movα : Player → α → Set α) (movβ : Player → β → Set β) [Hα : DecidableEq α] [Hβ : DecidableEq β] (x : MulTy α β) : MulTy.moves p movβ movα x.swap = swap '' MulTy.moves p movα movβ x

def LGame.MulTy.map {α₁ : Type u_1} {β₁ : Type u_2} {α₂ : Type u_3} {β₂ : Type u_4} (f : α₁ → α₂) (g : β₁ → β₂) : MulTy α₁ β₁ → MulTy α₂ β₂

Map MulTy α₁ β₁ to MulTy α₂ β₂ using f : α₁ → α₂ and g : β₁ → β₂ in the natural way.

Equations

• LGame.MulTy.map f g = Multiset.map (Prod.map id (Prod.map f g))

@[simp]

theorem LGame.MulTy.map_add {α₁ : Type u_1} {β₁ : Type u_2} {α₂ : Type u_3} {β₂ : Type u_4} (f : α₁ → α₂) (g : β₁ → β₂) (x y : MulTy α₁ β₁) : map f g (x + y) = map f g x + map f g y

theorem LGame.MulTy.map_erase {α₁ : Type u_1} {β₁ : Type u_2} {α₂ : Type u_3} {β₂ : Type u_4} (f : α₁ → α₂) (g : β₁ → β₂) [DecidableEq α₁] [DecidableEq β₁] [DecidableEq α₂] [DecidableEq β₂] {x : MulTy α₁ β₁} {y : Player × α₁ × β₁} (hy : y ∈ x) : map f g (Multiset.erase x y) = Multiset.erase (map f g x) (y.1, f y.2.1, g y.2.2)

@[simp]

theorem LGame.MulTy.map_mulOption {α₁ : Type u_1} {β₁ : Type u_2} {α₂ : Type u_3} {β₂ : Type u_4} (f : α₁ → α₂) (g : β₁ → β₂) (b : Player) (x y : α₁ × β₁) : map f g (mulOption b x y) = mulOption b (Prod.map f g x) (Prod.map f g y)

theorem LGame.MulTy.movesSingle_comp_prodMap {p : Player} {α₁ : Type u_1} {β₁ : Type u_2} {α₂ : Type u_3} {β₂ : Type u_4} {movα₁ : Player → α₁ → Set α₁} {movβ₁ : Player → β₁ → Set β₁} {movα₂ : Player → α₂ → Set α₂} {movβ₂ : Player → β₂ → Set β₂} {f : α₁ → α₂} {g : β₁ → β₂} (hf : ∀ (p : Player), movα₂ p ∘ f = Set.image f ∘ movα₁ p) (hg : ∀ (p : Player), movβ₂ p ∘ g = Set.image g ∘ movβ₁ p) : movesSingle p movα₂ movβ₂ ∘ Prod.map id (Prod.map f g) = Set.image (map f g) ∘ movesSingle p movα₁ movβ₁

theorem LGame.MulTy.moves_comp_map {p : Player} {α₁ : Type u_1} {β₁ : Type u_2} {α₂ : Type u_3} {β₂ : Type u_4} {movα₁ : Player → α₁ → Set α₁} {movβ₁ : Player → β₁ → Set β₁} {movα₂ : Player → α₂ → Set α₂} {movβ₂ : Player → β₂ → Set β₂} {f : α₁ → α₂} {g : β₁ → β₂} [Hα₁ : DecidableEq α₁] [Hβ₁ : DecidableEq β₁] [Hα₂ : DecidableEq α₂] [Hβ₂ : DecidableEq β₂] (hf : ∀ (p : Player), movα₂ p ∘ f = Set.image f ∘ movα₁ p) (hg : ∀ (p : Player), movβ₂ p ∘ g = Set.image g ∘ movβ₁ p) : MulTy.moves p movα₂ movβ₂ ∘ map f g = Set.image (map f g) ∘ MulTy.moves p movα₁ movβ₁

instance LGame.MulTy.instSmallElemMovesSingle {α : Type v} {β : Type w} (p : Player) (movα : Player → α → Set α) (movβ : Player → β → Set β) [∀ (x : α), Small.{u, v} ↑(movα left x)] [∀ (x : α), Small.{u, v} ↑(movα right x)] [∀ (x : β), Small.{u, w} ↑(movβ left x)] [∀ (x : β), Small.{u, w} ↑(movβ right x)] (x : Player × α × β) : Small.{u, max v w} ↑(movesSingle p movα movβ x)

instance LGame.MulTy.instSmallElemMoves {α : Type v} {β : Type w} (p : Player) (movα : Player → α → Set α) (movβ : Player → β → Set β) [Hα : DecidableEq α] [Hβ : DecidableEq β] [∀ (x : α), Small.{u, v} ↑(movα left x)] [∀ (x : α), Small.{u, v} ↑(movα right x)] [∀ (x : β), Small.{u, w} ↑(movβ left x)] [∀ (x : β), Small.{u, w} ↑(movβ right x)] (x : MulTy α β) : Small.{u, max v w} ↑(MulTy.moves p movα movβ x)

@[reducible, inline]

abbrev LGame.MulTy.toLGame {α : Type v} {β : Type w} (movα : Player → α → Set α) (movβ : Player → β → Set β) [Hα : DecidableEq α] [Hβ : DecidableEq β] [∀ (x : α), Small.{u, v} ↑(movα left x)] [∀ (x : α), Small.{u, v} ↑(movα right x)] [∀ (x : β), Small.{u, w} ↑(movβ left x)] [∀ (x : β), Small.{u, w} ↑(movβ right x)] (x : Player × α × β) : LGame

The game ±xᵢ * yᵢ.

Equations

• LGame.MulTy.toLGame movα movβ x = LGame.corec (fun (x : Player) => LGame.MulTy.moves x movα movβ) {x}

theorem LGame.MulTy.moves_toLGame {α : Type v} {β : Type w} (p : Player) (movα : Player → α → Set α) (movβ : Player → β → Set β) [Hα : DecidableEq α] [Hβ : DecidableEq β] [∀ (x : α), Small.{u, v} ↑(movα left x)] [∀ (x : α), Small.{u, v} ↑(movα right x)] [∀ (x : β), Small.{u, w} ↑(movβ left x)] [∀ (x : β), Small.{u, w} ↑(movβ right x)] (x : Player × α × β) : moves p (toLGame movα movβ x) = (corec fun (x : Player) => MulTy.moves x movα movβ) '' movesSingle p movα movβ x

@[simp]

theorem LGame.MulTy.corec_zero {α : Type v} {β : Type w} (movα : Player → α → Set α) (movβ : Player → β → Set β) [Hα : DecidableEq α] [Hβ : DecidableEq β] [∀ (x : α), Small.{u, v} ↑(movα left x)] [∀ (x : α), Small.{u, v} ↑(movα right x)] [∀ (x : β), Small.{u, w} ↑(movβ left x)] [∀ (x : β), Small.{u, w} ↑(movβ right x)] : corec (fun (x : Player) => MulTy.moves x movα movβ) 0 = 0

theorem LGame.MulTy.corec_neg {α : Type v} {β : Type w} (movα : Player → α → Set α) (movβ : Player → β → Set β) [Hα : DecidableEq α] [Hβ : DecidableEq β] [∀ (x : α), Small.{u, v} ↑(movα left x)] [∀ (x : α), Small.{u, v} ↑(movα right x)] [∀ (x : β), Small.{u, w} ↑(movβ left x)] [∀ (x : β), Small.{u, w} ↑(movβ right x)] (init : MulTy α β) : corec (fun (x : Player) => MulTy.moves x movα movβ) (-init) = -corec (fun (x : Player) => MulTy.moves x movα movβ) init

theorem LGame.MulTy.corec_add {α : Type v} {β : Type w} (movα : Player → α → Set α) (movβ : Player → β → Set β) [Hα : DecidableEq α] [Hβ : DecidableEq β] [∀ (x : α), Small.{u, v} ↑(movα left x)] [∀ (x : α), Small.{u, v} ↑(movα right x)] [∀ (x : β), Small.{u, w} ↑(movβ left x)] [∀ (x : β), Small.{u, w} ↑(movβ right x)] (init₁ init₂ : MulTy α β) : corec (fun (x : Player) => MulTy.moves x movα movβ) (init₁ + init₂) = corec (fun (x : Player) => MulTy.moves x movα movβ) init₁ + corec (fun (x : Player) => MulTy.moves x movα movβ) init₂

theorem LGame.MulTy.corec_mulOption {α : Type v} {β : Type w} (movα : Player → α → Set α) (movβ : Player → β → Set β) [Hα : DecidableEq α] [Hβ : DecidableEq β] [∀ (x : α), Small.{u, v} ↑(movα left x)] [∀ (x : α), Small.{u, v} ↑(movα right x)] [∀ (x : β), Small.{u, w} ↑(movβ left x)] [∀ (x : β), Small.{u, w} ↑(movβ right x)] (p : Player) (x y : α × β) : corec (fun (x : Player) => MulTy.moves x movα movβ) (mulOption p x y) = toLGame movα movβ (p, y.1, x.2) + toLGame movα movβ (p, x.1, y.2) - toLGame movα movβ (p, y.1, y.2)

theorem LGame.corec_mulTy {α : Type v} {β : Type w} (movα : Player → α → Set α) (movβ : Player → β → Set β) [Hα : DecidableEq α] [Hβ : DecidableEq β] [∀ (x : α), Small.{u, v} ↑(movα left x)] [∀ (x : α), Small.{u, v} ↑(movα right x)] [∀ (x : β), Small.{u, w} ↑(movβ left x)] [∀ (x : β), Small.{u, w} ↑(movβ right x)] (x : MulTy α β) : corec (fun (x : Player) => MulTy.moves x movα movβ) x = (Multiset.map (MulTy.toLGame movα movβ) x).sum

theorem LGame.MulTy.corec_swap {α : Type v} {β : Type w} (movα : Player → α → Set α) (movβ : Player → β → Set β) [Hα : DecidableEq α] [Hβ : DecidableEq β] [∀ (x : α), Small.{u, v} ↑(movα left x)] [∀ (x : α), Small.{u, v} ↑(movα right x)] [∀ (x : β), Small.{u, w} ↑(movβ left x)] [∀ (x : β), Small.{u, w} ↑(movβ right x)] (x : MulTy α β) : corec (fun (x : Player) => MulTy.moves x movβ movα) x.swap = corec (fun (x : Player) => MulTy.moves x movα movβ) x

instance LGame.instMul : Mul LGame

The product of x = !{s₁ | t₁} and y = !{s₂ | t₂} is !{a₁ * y + x * b₁ - a₁ * b₁ | a₂ * y + x * b₂ - a₂ * b₂}, where (a₁, b₁) ∈ s₁ ×ˢ s₂ ∪ t₁ ×ˢ t₂ and (a₂, b₂) ∈ s₁ ×ˢ t₂ ∪ t₁ ×ˢ s₂.

Using LGame.mulOption, this can alternatively be written as x * y = !{mulOption x y a₁ b₁ | mulOption x y a₂ b₂}.

Equations

• LGame.instMul = { mul := fun (x y : LGame) => LGame.MulTy.toLGame LGame.moves LGame.moves (Player.right, x, y) }

theorem LGame.corec_mul_corec {α : Type v} {β : Type w} (movα : Player → α → Set α) (movβ : Player → β → Set β) [Hα : DecidableEq α] [Hβ : DecidableEq β] [∀ (x : α), Small.{u, v} ↑(movα left x)] [∀ (x : α), Small.{u, v} ↑(movα right x)] [∀ (x : β), Small.{u, w} ↑(movβ left x)] [∀ (x : β), Small.{u, w} ↑(movβ right x)] (initα : α) (initβ : β) : corec movα initα * corec movβ initβ = MulTy.toLGame movα movβ (right, initα, initβ)

def LGame.mulOption (x y a b : LGame) : LGame

The general option of x * y looks like a * y + x * b - a * b, for a and b options of x and y, respectively.

Equations

• LGame.mulOption x y a b = a * y + x * b - a * b

@[simp]

theorem LGame.moves_mul (p : Player) (x y : LGame) : moves p (x * y) = (fun (a : LGame × LGame) => mulOption x y a.1 a.2) '' (moves left x ×ˢ moves p y ∪ moves right x ×ˢ moves (-p) y)

@[simp]

theorem LGame.moves_mulOption (p : Player) (x y a b : LGame) : moves p (mulOption x y a b) = moves p (a * y + x * b - a * b)

instance LGame.instCommMagma : CommMagma LGame

Equations

• LGame.instCommMagma = { toMul := LGame.instMul, mul_comm := LGame.instCommMagma._proof_3 }

instance LGame.instMulZeroClass : MulZeroClass LGame

Equations

• LGame.instMulZeroClass = { toMul := LGame.instMul, toZero := LGame.instZero, zero_mul := LGame.instMulZeroClass._proof_1, mul_zero := LGame.instMulZeroClass._proof_2 }

instance LGame.instMulOneClass : MulOneClass LGame

Equations

• LGame.instMulOneClass = { toOne := LGame.instOne, toMul := LGame.instMul, one_mul := LGame.one_mul'✝, mul_one := LGame.instMulOneClass._proof_1 }

instance LGame.instHasDistribNeg : HasDistribNeg LGame

Equations

• LGame.instHasDistribNeg = { toInvolutiveNeg := LGame.instInvolutiveNeg, neg_mul := LGame.neg_mul'✝, mul_neg := LGame.instHasDistribNeg._proof_1 }

Stoppers

inductive LGame.StopperFor : Player → LGame → Prop

A game is a stopper for player p when an alternating sequence of moves starting with said player always terminates.

• mk {p : Player} {x : LGame} : (∀ y ∈ moves p x, StopperFor (-p) y) → StopperFor p x

theorem LGame.stopperFor_iff (a✝ : Player) (a✝¹ : LGame) : StopperFor a✝ a✝¹ ↔ ∀ y ∈ moves a✝ a✝¹, StopperFor (-a✝) y

theorem LGame.StopperFor.of_mem_moves {p : Player} {x y : LGame} (h : StopperFor p x) (hy : y ∈ moves p x) : StopperFor (-p) y

theorem LGame.StopperFor.neg {p : Player} {x : LGame} (h : StopperFor p x) : StopperFor (-p) (-x)

@[simp]

theorem LGame.stopperFor_neg_iff {p : Player} {x : LGame} : StopperFor p (-x) ↔ StopperFor (-p) x

def LGame.Stopper (x : LGame) : Prop

A game is a stopper when it's StopperFor for both players.

Equations

• x.Stopper = ∀ (p : Player), LGame.StopperFor p x

@[simp]

theorem LGame.Stopper.stopperFor (p : Player) {x : LGame} (h : x.Stopper) : StopperFor p x

theorem LGame.Stopper.mk {x : LGame} (H : ∀ (p : Player), ∀ y ∈ moves p x, y.Stopper) : x.Stopper

A game is a stopper when all its options are stoppers.

Note that this is not an iff, as e.g. { | { | dud}} is a stopper, but { | dud} isn't.

theorem LGame.Stopper.neg {x : LGame} (h : x.Stopper) : (-x).Stopper

@[simp]

theorem LGame.stopper_neg_iff {x : LGame} : (-x).Stopper ↔ x.Stopper

@[simp]

theorem LGame.stopper_zero : Stopper 0

@[simp]

theorem LGame.stopper_one : Stopper 1

@[simp]

theorem LGame.stopper_on : on.Stopper

@[simp]

theorem LGame.stopper_off : off.Stopper

@[simp]

theorem LGame.not_stopperFor_dud (p : Player) : ¬StopperFor p dud

@[simp]

theorem LGame.not_stopper_dud : ¬dud.Stopper

@[simp]

theorem LGame.stopperFor_right_tis : StopperFor right tis

@[simp]

theorem LGame.stopperFor_left_tisn : StopperFor left tisn

@[simp]

theorem LGame.not_stopperFor_left_tis : ¬StopperFor left tis

@[simp]

theorem LGame.not_stopperFor_right_tisn : ¬StopperFor right tisn

@[simp]

theorem LGame.not_stopper_tis : ¬tis.Stopper

@[simp]

theorem LGame.not_stopper_tisn : ¬tisn.Stopper