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.leftMoves (x : LGame) : Set LGame

The set of left moves of the game.

Equations

• x.leftMoves = (↑(QPF.Cofix.dest x)).1

def LGame.rightMoves (x : LGame) : Set LGame

The set of right moves of the game.

Equations

• x.rightMoves = (↑(QPF.Cofix.dest x)).2

instance LGame.small_leftMoves (x : LGame) : Small.{u, u + 1} ↑x.leftMoves

instance LGame.small_rightMoves (x : LGame) : Small.{u, u + 1} ↑x.rightMoves

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 ∈ y.leftMoves ∪ y.rightMoves)

theorem LGame.IsOption.of_mem_leftMoves {x y : LGame} : x ∈ y.leftMoves → x.IsOption y

theorem LGame.IsOption.of_mem_rightMoves {x y : LGame} : x ∈ y.rightMoves → 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_leftMoves {x y : LGame} (h : x ∈ y.leftMoves) : x.Subposition y

theorem LGame.Subposition.of_mem_rightMoves {x y : LGame} (h : x ∈ y.rightMoves) : 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 → (∃ (s : Set (LGame × LGame)), Prod.fst '' s = x.leftMoves ∧ Prod.snd '' s = y.leftMoves ∧ ∀ z ∈ s, r z.1 z.2) ∧ ∃ (t : Set (LGame × LGame)), Prod.fst '' t = x.rightMoves ∧ Prod.snd '' t = y.rightMoves ∧ ∀ z ∈ t, 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} (hl : x.leftMoves = y.leftMoves) (hr : x.rightMoves = y.rightMoves) : 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 ↔ x.leftMoves = y.leftMoves ∧ x.rightMoves = y.rightMoves

def LGame.corec {α : Type v} (leftMoves rightMoves : α → Set α) [∀ (a : α), Small.{u, v} ↑(leftMoves a)] [∀ (a : α), Small.{u, v} ↑(rightMoves 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 ⊤ ⊥ ().

Equations

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

@[simp]

theorem LGame.leftMoves_corec {α : Type v} (leftMoves rightMoves : α → Set α) [∀ (a : α), Small.{u, v} ↑(leftMoves a)] [∀ (a : α), Small.{u, v} ↑(rightMoves a)] (init : α) : (corec leftMoves rightMoves init).leftMoves = corec leftMoves rightMoves '' leftMoves init

@[simp]

theorem LGame.rightMoves_corec {α : Type v} (leftMoves rightMoves : α → Set α) [∀ (a : α), Small.{u, v} ↑(leftMoves a)] [∀ (a : α), Small.{u, v} ↑(rightMoves a)] (init : α) : (corec leftMoves rightMoves init).rightMoves = corec leftMoves rightMoves '' rightMoves init

theorem LGame.leftMoves_comp_corec {α : Type v} (leftMoves rightMoves : α → Set α) [∀ (a : α), Small.{u, v} ↑(leftMoves a)] [∀ (a : α), Small.{u, v} ↑(rightMoves a)] : LGame.leftMoves ∘ corec leftMoves rightMoves = Set.image (corec leftMoves rightMoves) ∘ leftMoves

theorem LGame.rightMoves_comp_corec {α : Type v} (leftMoves rightMoves : α → Set α) [∀ (a : α), Small.{u, v} ↑(leftMoves a)] [∀ (a : α), Small.{u, v} ↑(rightMoves a)] : LGame.rightMoves ∘ corec leftMoves rightMoves = Set.image (corec leftMoves rightMoves) ∘ rightMoves

theorem LGame.hom_unique_apply {α : Type v} {leftMoves rightMoves : α → Set α} [∀ (a : α), Small.{u, v} ↑(leftMoves a)] [∀ (a : α), Small.{u, v} ↑(rightMoves a)] (f g : α → LGame) (hlf : LGame.leftMoves ∘ f = Set.image f ∘ leftMoves) (hrf : LGame.rightMoves ∘ f = Set.image f ∘ rightMoves) (hlg : LGame.leftMoves ∘ g = Set.image g ∘ leftMoves) (hrg : LGame.rightMoves ∘ g = Set.image g ∘ rightMoves) (x : α) : f x = g x

theorem LGame.hom_unique {α : Type v} {leftMoves rightMoves : α → Set α} [∀ (a : α), Small.{u, v} ↑(leftMoves a)] [∀ (a : α), Small.{u, v} ↑(rightMoves a)] (f g : α → LGame) (hlf : LGame.leftMoves ∘ f = Set.image f ∘ leftMoves) (hrf : LGame.rightMoves ∘ f = Set.image f ∘ rightMoves) (hlg : LGame.leftMoves ∘ g = Set.image g ∘ leftMoves) (hrg : LGame.rightMoves ∘ g = Set.image g ∘ rightMoves) : f = g

theorem LGame.corec_comp_hom {α : Type v} {β : Type w} {leftMovesα rightMovesα : α → Set α} {leftMovesβ rightMovesβ : β → Set β} [∀ (a : α), Small.{u, v} ↑(leftMovesα a)] [∀ (a : α), Small.{u, v} ↑(rightMovesα a)] [∀ (b : β), Small.{u, w} ↑(leftMovesβ b)] [∀ (b : β), Small.{u, w} ↑(rightMovesβ b)] (f : α → β) (hlf : leftMovesβ ∘ f = Set.image f ∘ leftMovesα) (hrf : rightMovesβ ∘ f = Set.image f ∘ rightMovesα) : corec leftMovesβ rightMovesβ ∘ f = corec leftMovesα rightMovesα

theorem LGame.corec_comp_hom_apply {α : Type v} {β : Type w} {leftMovesα rightMovesα : α → Set α} {leftMovesβ rightMovesβ : β → Set β} [∀ (a : α), Small.{u, v} ↑(leftMovesα a)] [∀ (a : α), Small.{u, v} ↑(rightMovesα a)] [∀ (b : β), Small.{u, w} ↑(leftMovesβ b)] [∀ (b : β), Small.{u, w} ↑(rightMovesβ b)] (f : α → β) (hlf : leftMovesβ ∘ f = Set.image f ∘ leftMovesα) (hrf : rightMovesβ ∘ f = Set.image f ∘ rightMovesα) (x : α) : corec leftMovesβ rightMovesβ (f x) = corec leftMovesα rightMovesα x

@[simp]

theorem LGame.corec_leftMoves_rightMoves : corec leftMoves rightMoves = id

theorem LGame.corec_leftMoves_rightMoves_apply (x : LGame) : corec leftMoves rightMoves x = x

noncomputable def LGame.ofSets (l r : Set LGame) [Small.{u, u + 1} ↑l] [Small.{u, u + 1} ↑r] : LGame

Construct an LGame from its left and right sets.

This is given notation {s | t}ᴸ, where the superscript L is to disambiguate from set builder notation, and from the analogous constructors on other game types.

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.

def LGame.«term{_|_}ᴸ» : Lean.ParserDescr

Construct an LGame from its left and right sets.

This is given notation {s | t}ᴸ, where the superscript L is to disambiguate from set builder notation, and from the analogous constructors on other game types.

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

Conventions for notations in identifiers:

• The recommended spelling of {· | ·}ᴸ in identifiers is ofSets.

Equations

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

@[simp]

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

@[simp]

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

Basic games

instance LGame.instZero : Zero LGame

The game 0 = {∅ | ∅}ᴸ.

Equations

• LGame.instZero = { zero := {∅ | ∅}ᴸ }

theorem LGame.zero_def : 0 = {∅ | ∅}ᴸ

@[simp]

theorem LGame.leftMoves_zero : leftMoves 0 = ∅

@[simp]

theorem LGame.rightMoves_zero : rightMoves 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 : leftMoves 1 = {0}

@[simp]

theorem LGame.rightMoves_one : rightMoves 1 = ∅

def LGame.on : LGame

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

Equations

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

@[simp]

theorem LGame.leftMoves_on : on.leftMoves = {on}

@[simp]

theorem LGame.rightMoves_on : on.rightMoves = ∅

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

theorem LGame.eq_on {x : LGame} : x = on ↔ x.leftMoves = {x} ∧ x.rightMoves = ∅

def LGame.off : LGame

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

Equations

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

@[simp]

theorem LGame.leftMoves_off : off.leftMoves = ∅

@[simp]

theorem LGame.rightMoves_off : off.rightMoves = {off}

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

theorem LGame.eq_off {x : LGame} : x = off ↔ x.leftMoves = ∅ ∧ x.rightMoves = {x}

def LGame.dud : LGame

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

Equations

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

@[simp]

theorem LGame.leftMoves_dud : dud.leftMoves = {dud}

@[simp]

theorem LGame.rightMoves_dud : dud.rightMoves = {dud}

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

theorem LGame.eq_dud {x : LGame} : x = dud ↔ x.leftMoves = {x} ∧ x.rightMoves = {x}

def LGame.tis : LGame

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

Equations

• LGame.tis = LGame.corec (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 (fun (t : Bool) => Bool.rec ∅ {false} t) (fun (t : Bool) => Bool.rec {true} ∅ t) false

@[simp]

theorem LGame.leftMoves_tis : tis.leftMoves = {tisn}

@[simp]

theorem LGame.rightMoves_tis : tis.rightMoves = ∅

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

@[simp]

theorem LGame.leftMoves_tisn : tisn.leftMoves = ∅

@[simp]

theorem LGame.rightMoves_tisn : tisn.rightMoves = {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 LGame.rightMoves LGame.leftMoves }

@[simp]

theorem LGame.corec_rightMoves_leftMoves : corec rightMoves leftMoves = fun (x : LGame) => -x

theorem LGame.corec_rightMoves_leftMoves_apply (x : LGame) : corec rightMoves leftMoves x = -x

theorem LGame.neg_corec {α : Type v} (leftMoves rightMoves : α → Set α) [∀ (x : α), Small.{u, v} ↑(leftMoves x)] [∀ (x : α), Small.{u, v} ↑(rightMoves x)] : -corec leftMoves rightMoves = corec rightMoves leftMoves

theorem LGame.neg_corec_apply {α : Type v} (leftMoves rightMoves : α → Set α) [∀ (x : α), Small.{u, v} ↑(leftMoves x)] [∀ (x : α), Small.{u, v} ↑(rightMoves x)] (init : α) : -corec leftMoves rightMoves init = corec rightMoves leftMoves init

instance LGame.instInvolutiveNeg : InvolutiveNeg LGame

Equations

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

@[simp]

theorem LGame.leftMoves_neg (x : LGame) : (-x).leftMoves = -x.rightMoves

@[simp]

theorem LGame.rightMoves_neg (x : LGame) : (-x).rightMoves = -x.leftMoves

@[simp]

theorem LGame.neg_ofSets (s t : Set LGame) [Small.{u, u + 1} ↑s] [Small.{u, u + 1} ↑t] : -{s | t}ᴸ = {-t | -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} {leftMovesα rightMovesα : α → Set α} {leftMovesβ rightMovesβ : β → Set β} [∀ (x : α), Small.{u, v} ↑(leftMovesα x)] [∀ (x : α), Small.{u, v} ↑(rightMovesα x)] [∀ (x : β), Small.{u, w} ↑(leftMovesβ x)] [∀ (x : β), Small.{u, w} ↑(rightMovesβ x)] (initα : α) (initβ : β) : corec leftMovesα rightMovesα initα + corec leftMovesβ rightMovesβ initβ = corec (fun (x : α × β) => (fun (y : α) => (y, x.2)) '' leftMovesα x.1 ∪ (fun (y : β) => (x.1, y)) '' leftMovesβ x.2) (fun (x : α × β) => (fun (y : α) => (y, x.2)) '' rightMovesα x.1 ∪ (fun (y : β) => (x.1, y)) '' rightMovesβ x.2) (initα, initβ)

@[simp]

theorem LGame.leftMoves_add (x y : LGame) : (x + y).leftMoves = (fun (x : LGame) => x + y) '' x.leftMoves ∪ (fun (x_1 : LGame) => x + x_1) '' y.leftMoves

@[simp]

theorem LGame.rightMoves_add (x y : LGame) : (x + y).rightMoves = (fun (x : LGame) => x + y) '' x.rightMoves ∪ (fun (x_1 : LGame) => x + x_1) '' y.rightMoves

@[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.leftMoves_sum (m : Multiset LGame) : m.sum.leftMoves = ⋃ y ∈ m, (fun (x : LGame) => x + (m.erase y).sum) '' y.leftMoves

theorem LGame.rightMoves_sum (m : Multiset LGame) : m.sum.rightMoves = ⋃ y ∈ m, (fun (x : LGame) => x + (m.erase y).sum) '' y.rightMoves

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} {leftMovesα rightMovesα : α → Set α} {leftMovesβ rightMovesβ : β → Set β} [∀ (x : α), Small.{u, v} ↑(leftMovesα x)] [∀ (x : α), Small.{u, v} ↑(rightMovesα x)] [∀ (x : β), Small.{u, w} ↑(leftMovesβ x)] [∀ (x : β), Small.{u, w} ↑(rightMovesβ x)] (initα : α) (initβ : β) : corec leftMovesα rightMovesα initα - corec leftMovesβ rightMovesβ initβ = corec (fun (x : α × β) => (fun (y : α) => (y, x.2)) '' leftMovesα x.1 ∪ (fun (y : β) => (x.1, y)) '' rightMovesβ x.2) (fun (x : α × β) => (fun (y : α) => (y, x.2)) '' rightMovesα x.1 ∪ (fun (y : β) => (x.1, y)) '' leftMovesβ x.2) (initα, initβ)

@[simp]

theorem LGame.leftMoves_sub (x y : LGame) : (x - y).leftMoves = (fun (x : LGame) => x - y) '' x.leftMoves ∪ (fun (x_1 : LGame) => x + x_1) '' (-y.rightMoves)

@[simp]

theorem LGame.rightMoves_sub (x y : LGame) : (x - y).rightMoves = (fun (x : LGame) => x - y) '' x.rightMoves ∪ (fun (x_1 : LGame) => x + x_1) '' (-y.leftMoves)

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 (Bool × α × β). Each term corresponds to a sum Σ ±aᵢ * bᵢ, where aᵢ and bᵢ are terms of α and β respectively, and the attached bool represents each term's sign.

Equations

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

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 : Bool × α × β) => (!y.1, y.2)) x, neg_neg := ⋯ }

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

@[simp]

theorem LGame.MulTy.mem_neg {α : Type v} {β : Type w} {x : Bool × α × β} {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 : Bool × α × β) : -{a} = {(!a.1, a.2)}

@[simp]

theorem LGame.MulTy.neg_cons {α : Type v} {β : Type w} (a : Bool × α × β) (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 : Bool × α × β) : -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 : Bool × α × β) => (a.1, a.2.swap)) x

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

@[simp]

theorem LGame.MulTy.mem_swap {α : Type v} {β : Type w} {x : Bool × β × α} {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 : Bool × α × β) : {a}.swap = {(a.1, a.2.swap)}

@[simp]

theorem LGame.MulTy.swap_cons {α : Type v} {β : Type w} (a : Bool × α × β) (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 : Bool × α × β) : swap (Multiset.erase x a) = Multiset.erase x.swap (a.1, a.2.swap)

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

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

If the boolean argument is false, all signs are flipped.

Equations

• LGame.MulTy.mulOption b x y = {(b, y.1, x.2), (b, x.1, y.2), (!b, y.1, y.2)}

@[simp]

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

@[simp]

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

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

def LGame.MulTy.leftMovesSet {α : Type v} {β : Type w} (leftMovesα rightMovesα : α → Set α) (leftMovesβ rightMovesβ : β → Set β) (x : Bool × α × β) : Set (α × β)

The set of pairs α × β used in leftMovesSingle.

Equations

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

def LGame.MulTy.rightMovesSet {α : Type v} {β : Type w} (leftMovesα rightMovesα : α → Set α) (leftMovesβ rightMovesβ : β → Set β) (x : Bool × α × β) : Set (α × β)

The set of pairs α × β used in rightMovesSingle.

Equations

• LGame.MulTy.rightMovesSet leftMovesα rightMovesα leftMovesβ rightMovesβ x = LGame.MulTy.leftMovesSet leftMovesα rightMovesα leftMovesβ rightMovesβ (!x.1, x.2)

theorem LGame.MulTy.leftMovesSet_neg {α : Type v} {β : Type w} (leftMovesα rightMovesα : α → Set α) (leftMovesβ rightMovesβ : β → Set β) (x : Bool × α × β) : leftMovesSet leftMovesα rightMovesα leftMovesβ rightMovesβ (!x.1, x.2) = rightMovesSet leftMovesα rightMovesα leftMovesβ rightMovesβ x

theorem LGame.MulTy.rightMovesSet_neg {α : Type v} {β : Type w} (leftMovesα rightMovesα : α → Set α) (leftMovesβ rightMovesβ : β → Set β) (x : Bool × α × β) : rightMovesSet leftMovesα rightMovesα leftMovesβ rightMovesβ (!x.1, x.2) = leftMovesSet leftMovesα rightMovesα leftMovesβ rightMovesβ x

theorem LGame.MulTy.leftMovesSet_neg' (x : Bool × LGame × LGame) : leftMovesSet LGame.leftMoves LGame.rightMoves LGame.leftMoves LGame.rightMoves (x.1, -x.2.1, x.2.2) = (fun (y : LGame × LGame) => (-y.1, y.2)) '' rightMovesSet LGame.leftMoves LGame.rightMoves LGame.leftMoves LGame.rightMoves x

theorem LGame.MulTy.rightMovesSet_neg' (x : Bool × LGame × LGame) : rightMovesSet LGame.leftMoves LGame.rightMoves LGame.leftMoves LGame.rightMoves (x.1, -x.2.1, x.2.2) = (fun (y : LGame × LGame) => (-y.1, y.2)) '' leftMovesSet LGame.leftMoves LGame.rightMoves LGame.leftMoves LGame.rightMoves x

theorem LGame.MulTy.leftMovesSet_swap {α : Type v} {β : Type w} (leftMovesα rightMovesα : α → Set α) (leftMovesβ rightMovesβ : β → Set β) (x : Bool × α × β) : leftMovesSet leftMovesβ rightMovesβ leftMovesα rightMovesα (x.1, x.2.swap) = Prod.swap '' leftMovesSet leftMovesα rightMovesα leftMovesβ rightMovesβ x

theorem LGame.MulTy.rightMovesSet_swap {α : Type v} {β : Type w} (leftMovesα rightMovesα : α → Set α) (leftMovesβ rightMovesβ : β → Set β) (x : Bool × α × β) : rightMovesSet leftMovesβ rightMovesβ leftMovesα rightMovesα (x.1, x.2.swap) = Prod.swap '' rightMovesSet leftMovesα rightMovesα leftMovesβ rightMovesβ x

def LGame.MulTy.leftMovesSingle {α : Type v} {β : Type w} (leftMovesα rightMovesα : α → Set α) (leftMovesβ rightMovesβ : β → Set β) (x : Bool × α × β) : Set (MulTy α β)

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

Equations

• LGame.MulTy.leftMovesSingle leftMovesα rightMovesα leftMovesβ rightMovesβ x = LGame.MulTy.mulOption x.1 x.2 '' LGame.MulTy.leftMovesSet leftMovesα rightMovesα leftMovesβ rightMovesβ x

def LGame.MulTy.rightMovesSingle {α : Type v} {β : Type w} (leftMovesα rightMovesα : α → Set α) (leftMovesβ rightMovesβ : β → Set β) (x : Bool × α × β) : Set (MulTy α β)

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

Equations

• LGame.MulTy.rightMovesSingle leftMovesα rightMovesα leftMovesβ rightMovesβ x = LGame.MulTy.mulOption x.1 x.2 '' LGame.MulTy.rightMovesSet leftMovesα rightMovesα leftMovesβ rightMovesβ x

theorem LGame.MulTy.leftMovesSingle_neg {α : Type v} {β : Type w} (leftMovesα rightMovesα : α → Set α) (leftMovesβ rightMovesβ : β → Set β) (x : Bool × α × β) : leftMovesSingle leftMovesα rightMovesα leftMovesβ rightMovesβ (!x.1, x.2) = -rightMovesSingle leftMovesα rightMovesα leftMovesβ rightMovesβ x

theorem LGame.MulTy.rightMovesSingle_neg {α : Type v} {β : Type w} (leftMovesα rightMovesα : α → Set α) (leftMovesβ rightMovesβ : β → Set β) (x : Bool × α × β) : rightMovesSingle leftMovesα rightMovesα leftMovesβ rightMovesβ (!x.1, x.2) = -leftMovesSingle leftMovesα rightMovesα leftMovesβ rightMovesβ x

theorem LGame.MulTy.leftMovesSingle_neg' (x : Bool × LGame × LGame) : leftMovesSingle LGame.leftMoves LGame.rightMoves LGame.leftMoves LGame.rightMoves (x.1, -x.2.1, x.2.2) = (Multiset.map fun (y : Bool × LGame × LGame) => (y.1, -y.2.1, y.2.2)) '' rightMovesSingle LGame.leftMoves LGame.rightMoves LGame.leftMoves LGame.rightMoves x

theorem LGame.MulTy.rightMovesSingle_neg' (x : Bool × LGame × LGame) : rightMovesSingle LGame.leftMoves LGame.rightMoves LGame.leftMoves LGame.rightMoves (x.1, -x.2.1, x.2.2) = (Multiset.map fun (y : Bool × LGame × LGame) => (y.1, -y.2.1, y.2.2)) '' leftMovesSingle LGame.leftMoves LGame.rightMoves LGame.leftMoves LGame.rightMoves x

theorem LGame.MulTy.leftMovesSingle_swap {α : Type v} {β : Type w} (leftMovesα rightMovesα : α → Set α) (leftMovesβ rightMovesβ : β → Set β) (x : Bool × α × β) : leftMovesSingle leftMovesβ rightMovesβ leftMovesα rightMovesα (x.1, x.2.swap) = swap '' leftMovesSingle leftMovesα rightMovesα leftMovesβ rightMovesβ x

theorem LGame.MulTy.rightMovesSingle_swap {α : Type v} {β : Type w} (leftMovesα rightMovesα : α → Set α) (leftMovesβ rightMovesβ : β → Set β) (x : Bool × α × β) : rightMovesSingle leftMovesβ rightMovesβ leftMovesα rightMovesα (x.1, x.2.swap) = swap '' rightMovesSingle leftMovesα rightMovesα leftMovesβ rightMovesβ x

def LGame.MulTy.leftMoves {α : Type v} {β : Type w} (leftMovesα rightMovesα : α → Set α) (leftMovesβ rightMovesβ : β → Set β) [Hα : DecidableEq α] [Hβ : DecidableEq β] (x : MulTy α β) : Set (MulTy α β)

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

Equations

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

def LGame.MulTy.rightMoves {α : Type v} {β : Type w} (leftMovesα rightMovesα : α → Set α) (leftMovesβ rightMovesβ : β → Set β) [Hα : DecidableEq α] [Hβ : DecidableEq β] (x : MulTy α β) : Set (MulTy α β)

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

Equations

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

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.leftMoves_neg {α : Type v} {β : Type w} (leftMovesα rightMovesα : α → Set α) (leftMovesβ rightMovesβ : β → Set β) [Hα : DecidableEq α] [Hβ : DecidableEq β] (x : MulTy α β) : leftMoves leftMovesα rightMovesα leftMovesβ rightMovesβ (-x) = -rightMoves leftMovesα rightMovesα leftMovesβ rightMovesβ x

theorem LGame.MulTy.rightMoves_neg {α : Type v} {β : Type w} (leftMovesα rightMovesα : α → Set α) (leftMovesβ rightMovesβ : β → Set β) [Hα : DecidableEq α] [Hβ : DecidableEq β] (x : MulTy α β) : rightMoves leftMovesα rightMovesα leftMovesβ rightMovesβ (-x) = -leftMoves leftMovesα rightMovesα leftMovesβ rightMovesβ x

theorem LGame.MulTy.leftMoves_neg' (x : MulTy LGame LGame) : leftMoves LGame.leftMoves LGame.rightMoves LGame.leftMoves LGame.rightMoves (Multiset.map (fun (y : Bool × LGame × LGame) => (y.1, -y.2.1, y.2.2)) x) = (Multiset.map fun (y : Bool × LGame × LGame) => (y.1, -y.2.1, y.2.2)) '' rightMoves LGame.leftMoves LGame.rightMoves LGame.leftMoves LGame.rightMoves x

theorem LGame.MulTy.rightMoves_neg' (x : MulTy LGame LGame) : rightMoves LGame.leftMoves LGame.rightMoves LGame.leftMoves LGame.rightMoves (Multiset.map (fun (y : Bool × LGame × LGame) => (y.1, -y.2.1, y.2.2)) x) = (Multiset.map fun (y : Bool × LGame × LGame) => (y.1, -y.2.1, y.2.2)) '' leftMoves LGame.leftMoves LGame.rightMoves LGame.leftMoves LGame.rightMoves x

theorem LGame.MulTy.leftMoves_swap {α : Type v} {β : Type w} (leftMovesα rightMovesα : α → Set α) (leftMovesβ rightMovesβ : β → Set β) [Hα : DecidableEq α] [Hβ : DecidableEq β] (x : MulTy α β) : leftMoves leftMovesβ rightMovesβ leftMovesα rightMovesα x.swap = swap '' leftMoves leftMovesα rightMovesα leftMovesβ rightMovesβ x

theorem LGame.MulTy.rightMoves_swap {α : Type v} {β : Type w} (leftMovesα rightMovesα : α → Set α) (leftMovesβ rightMovesβ : β → Set β) [Hα : DecidableEq α] [Hβ : DecidableEq β] (x : MulTy α β) : rightMoves leftMovesβ rightMovesβ leftMovesα rightMovesα x.swap = swap '' rightMoves leftMovesα rightMovesα leftMovesβ rightMovesβ 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 : Bool × α₁ × β₁} (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 : Bool) (x y : α₁ × β₁) : map f g (mulOption b x y) = mulOption b (Prod.map f g x) (Prod.map f g y)

theorem LGame.MulTy.leftMovesSingle_comp_prodMap {α₁ : Type u_1} {β₁ : Type u_2} {α₂ : Type u_3} {β₂ : Type u_4} {leftMovesα₁ rightMovesα₁ : α₁ → Set α₁} {leftMovesβ₁ rightMovesβ₁ : β₁ → Set β₁} {leftMovesα₂ rightMovesα₂ : α₂ → Set α₂} {leftMovesβ₂ rightMovesβ₂ : β₂ → Set β₂} {f : α₁ → α₂} {g : β₁ → β₂} (hlf : leftMovesα₂ ∘ f = Set.image f ∘ leftMovesα₁) (hrf : rightMovesα₂ ∘ f = Set.image f ∘ rightMovesα₁) (hlg : leftMovesβ₂ ∘ g = Set.image g ∘ leftMovesβ₁) (hrg : rightMovesβ₂ ∘ g = Set.image g ∘ rightMovesβ₁) : leftMovesSingle leftMovesα₂ rightMovesα₂ leftMovesβ₂ rightMovesβ₂ ∘ Prod.map id (Prod.map f g) = Set.image (map f g) ∘ leftMovesSingle leftMovesα₁ rightMovesα₁ leftMovesβ₁ rightMovesβ₁

theorem LGame.MulTy.rightMovesSingle_comp_prodMap {α₁ : Type u_1} {β₁ : Type u_2} {α₂ : Type u_3} {β₂ : Type u_4} {leftMovesα₁ rightMovesα₁ : α₁ → Set α₁} {leftMovesβ₁ rightMovesβ₁ : β₁ → Set β₁} {leftMovesα₂ rightMovesα₂ : α₂ → Set α₂} {leftMovesβ₂ rightMovesβ₂ : β₂ → Set β₂} {f : α₁ → α₂} {g : β₁ → β₂} (hlf : leftMovesα₂ ∘ f = Set.image f ∘ leftMovesα₁) (hrf : rightMovesα₂ ∘ f = Set.image f ∘ rightMovesα₁) (hlg : leftMovesβ₂ ∘ g = Set.image g ∘ leftMovesβ₁) (hrg : rightMovesβ₂ ∘ g = Set.image g ∘ rightMovesβ₁) : rightMovesSingle leftMovesα₂ rightMovesα₂ leftMovesβ₂ rightMovesβ₂ ∘ Prod.map id (Prod.map f g) = Set.image (map f g) ∘ rightMovesSingle leftMovesα₁ rightMovesα₁ leftMovesβ₁ rightMovesβ₁

theorem LGame.MulTy.leftMoves_comp_map {α₁ : Type u_1} {β₁ : Type u_2} {α₂ : Type u_3} {β₂ : Type u_4} {leftMovesα₁ rightMovesα₁ : α₁ → Set α₁} {leftMovesβ₁ rightMovesβ₁ : β₁ → Set β₁} {leftMovesα₂ rightMovesα₂ : α₂ → Set α₂} {leftMovesβ₂ rightMovesβ₂ : β₂ → Set β₂} {f : α₁ → α₂} {g : β₁ → β₂} [Hα₁ : DecidableEq α₁] [Hβ₁ : DecidableEq β₁] [Hα₂ : DecidableEq α₂] [Hβ₂ : DecidableEq β₂] (hlf : leftMovesα₂ ∘ f = Set.image f ∘ leftMovesα₁) (hrf : rightMovesα₂ ∘ f = Set.image f ∘ rightMovesα₁) (hlg : leftMovesβ₂ ∘ g = Set.image g ∘ leftMovesβ₁) (hrg : rightMovesβ₂ ∘ g = Set.image g ∘ rightMovesβ₁) : leftMoves leftMovesα₂ rightMovesα₂ leftMovesβ₂ rightMovesβ₂ ∘ map f g = Set.image (map f g) ∘ leftMoves leftMovesα₁ rightMovesα₁ leftMovesβ₁ rightMovesβ₁

theorem LGame.MulTy.rightMoves_comp_map {α₁ : Type u_1} {β₁ : Type u_2} {α₂ : Type u_3} {β₂ : Type u_4} {leftMovesα₁ rightMovesα₁ : α₁ → Set α₁} {leftMovesβ₁ rightMovesβ₁ : β₁ → Set β₁} {leftMovesα₂ rightMovesα₂ : α₂ → Set α₂} {leftMovesβ₂ rightMovesβ₂ : β₂ → Set β₂} {f : α₁ → α₂} {g : β₁ → β₂} [Hα₁ : DecidableEq α₁] [Hβ₁ : DecidableEq β₁] [Hα₂ : DecidableEq α₂] [Hβ₂ : DecidableEq β₂] (hlf : leftMovesα₂ ∘ f = Set.image f ∘ leftMovesα₁) (hrf : rightMovesα₂ ∘ f = Set.image f ∘ rightMovesα₁) (hlg : leftMovesβ₂ ∘ g = Set.image g ∘ leftMovesβ₁) (hrg : rightMovesβ₂ ∘ g = Set.image g ∘ rightMovesβ₁) : rightMoves leftMovesα₂ rightMovesα₂ leftMovesβ₂ rightMovesβ₂ ∘ map f g = Set.image (map f g) ∘ rightMoves leftMovesα₁ rightMovesα₁ leftMovesβ₁ rightMovesβ₁

instance LGame.MulTy.instSmallElemLeftMovesSingle {α : Type v} {β : Type w} (leftMovesα rightMovesα : α → Set α) (leftMovesβ rightMovesβ : β → Set β) [∀ (x : α), Small.{u, v} ↑(leftMovesα x)] [∀ (x : α), Small.{u, v} ↑(rightMovesα x)] [∀ (x : β), Small.{u, w} ↑(leftMovesβ x)] [∀ (x : β), Small.{u, w} ↑(rightMovesβ x)] (x : Bool × α × β) : Small.{u, max v w} ↑(leftMovesSingle leftMovesα rightMovesα leftMovesβ rightMovesβ x)

instance LGame.MulTy.instSmallElemRightMovesSingle {α : Type v} {β : Type w} (leftMovesα rightMovesα : α → Set α) (leftMovesβ rightMovesβ : β → Set β) [∀ (x : α), Small.{u, v} ↑(leftMovesα x)] [∀ (x : α), Small.{u, v} ↑(rightMovesα x)] [∀ (x : β), Small.{u, w} ↑(leftMovesβ x)] [∀ (x : β), Small.{u, w} ↑(rightMovesβ x)] (x : Bool × α × β) : Small.{u, max v w} ↑(rightMovesSingle leftMovesα rightMovesα leftMovesβ rightMovesβ x)

instance LGame.MulTy.instSmallElemLeftMoves {α : Type v} {β : Type w} (leftMovesα rightMovesα : α → Set α) (leftMovesβ rightMovesβ : β → Set β) [Hα : DecidableEq α] [Hβ : DecidableEq β] [∀ (x : α), Small.{u, v} ↑(leftMovesα x)] [∀ (x : α), Small.{u, v} ↑(rightMovesα x)] [∀ (x : β), Small.{u, w} ↑(leftMovesβ x)] [∀ (x : β), Small.{u, w} ↑(rightMovesβ x)] (x : MulTy α β) : Small.{u, max v w} ↑(leftMoves leftMovesα rightMovesα leftMovesβ rightMovesβ x)

instance LGame.MulTy.instSmallElemRightMoves {α : Type v} {β : Type w} (leftMovesα rightMovesα : α → Set α) (leftMovesβ rightMovesβ : β → Set β) [Hα : DecidableEq α] [Hβ : DecidableEq β] [∀ (x : α), Small.{u, v} ↑(leftMovesα x)] [∀ (x : α), Small.{u, v} ↑(rightMovesα x)] [∀ (x : β), Small.{u, w} ↑(leftMovesβ x)] [∀ (x : β), Small.{u, w} ↑(rightMovesβ x)] (x : MulTy α β) : Small.{u, max v w} ↑(rightMoves leftMovesα rightMovesα leftMovesβ rightMovesβ x)

@[reducible, inline]

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

The game ±xᵢ * yᵢ.

Equations

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

theorem LGame.MulTy.leftMoves_toLGame {α : Type v} {β : Type w} (leftMovesα rightMovesα : α → Set α) (leftMovesβ rightMovesβ : β → Set β) [Hα : DecidableEq α] [Hβ : DecidableEq β] [∀ (x : α), Small.{u, v} ↑(leftMovesα x)] [∀ (x : α), Small.{u, v} ↑(rightMovesα x)] [∀ (x : β), Small.{u, w} ↑(leftMovesβ x)] [∀ (x : β), Small.{u, w} ↑(rightMovesβ x)] (x : Bool × α × β) : (toLGame leftMovesα rightMovesα leftMovesβ rightMovesβ x).leftMoves = corec (leftMoves leftMovesα rightMovesα leftMovesβ rightMovesβ) (rightMoves leftMovesα rightMovesα leftMovesβ rightMovesβ) '' leftMovesSingle leftMovesα rightMovesα leftMovesβ rightMovesβ x

theorem LGame.MulTy.rightMoves_toLGame {α : Type v} {β : Type w} (leftMovesα rightMovesα : α → Set α) (leftMovesβ rightMovesβ : β → Set β) [Hα : DecidableEq α] [Hβ : DecidableEq β] [∀ (x : α), Small.{u, v} ↑(leftMovesα x)] [∀ (x : α), Small.{u, v} ↑(rightMovesα x)] [∀ (x : β), Small.{u, w} ↑(leftMovesβ x)] [∀ (x : β), Small.{u, w} ↑(rightMovesβ x)] (x : Bool × α × β) : (toLGame leftMovesα rightMovesα leftMovesβ rightMovesβ x).rightMoves = corec (leftMoves leftMovesα rightMovesα leftMovesβ rightMovesβ) (rightMoves leftMovesα rightMovesα leftMovesβ rightMovesβ) '' rightMovesSingle leftMovesα rightMovesα leftMovesβ rightMovesβ x

@[simp]

theorem LGame.MulTy.corec_zero {α : Type v} {β : Type w} (leftMovesα rightMovesα : α → Set α) (leftMovesβ rightMovesβ : β → Set β) [Hα : DecidableEq α] [Hβ : DecidableEq β] [∀ (x : α), Small.{u, v} ↑(leftMovesα x)] [∀ (x : α), Small.{u, v} ↑(rightMovesα x)] [∀ (x : β), Small.{u, w} ↑(leftMovesβ x)] [∀ (x : β), Small.{u, w} ↑(rightMovesβ x)] : corec (leftMoves leftMovesα rightMovesα leftMovesβ rightMovesβ) (rightMoves leftMovesα rightMovesα leftMovesβ rightMovesβ) 0 = 0

theorem LGame.MulTy.corec_neg {α : Type v} {β : Type w} (leftMovesα rightMovesα : α → Set α) (leftMovesβ rightMovesβ : β → Set β) [Hα : DecidableEq α] [Hβ : DecidableEq β] [∀ (x : α), Small.{u, v} ↑(leftMovesα x)] [∀ (x : α), Small.{u, v} ↑(rightMovesα x)] [∀ (x : β), Small.{u, w} ↑(leftMovesβ x)] [∀ (x : β), Small.{u, w} ↑(rightMovesβ x)] (init : MulTy α β) : corec (leftMoves leftMovesα rightMovesα leftMovesβ rightMovesβ) (rightMoves leftMovesα rightMovesα leftMovesβ rightMovesβ) (-init) = -corec (leftMoves leftMovesα rightMovesα leftMovesβ rightMovesβ) (rightMoves leftMovesα rightMovesα leftMovesβ rightMovesβ) init

theorem LGame.MulTy.corec_add {α : Type v} {β : Type w} (leftMovesα rightMovesα : α → Set α) (leftMovesβ rightMovesβ : β → Set β) [Hα : DecidableEq α] [Hβ : DecidableEq β] [∀ (x : α), Small.{u, v} ↑(leftMovesα x)] [∀ (x : α), Small.{u, v} ↑(rightMovesα x)] [∀ (x : β), Small.{u, w} ↑(leftMovesβ x)] [∀ (x : β), Small.{u, w} ↑(rightMovesβ x)] (init₁ init₂ : MulTy α β) : corec (leftMoves leftMovesα rightMovesα leftMovesβ rightMovesβ) (rightMoves leftMovesα rightMovesα leftMovesβ rightMovesβ) (init₁ + init₂) = corec (leftMoves leftMovesα rightMovesα leftMovesβ rightMovesβ) (rightMoves leftMovesα rightMovesα leftMovesβ rightMovesβ) init₁ + corec (leftMoves leftMovesα rightMovesα leftMovesβ rightMovesβ) (rightMoves leftMovesα rightMovesα leftMovesβ rightMovesβ) init₂

theorem LGame.MulTy.corec_mulOption {α : Type v} {β : Type w} (leftMovesα rightMovesα : α → Set α) (leftMovesβ rightMovesβ : β → Set β) [Hα : DecidableEq α] [Hβ : DecidableEq β] [∀ (x : α), Small.{u, v} ↑(leftMovesα x)] [∀ (x : α), Small.{u, v} ↑(rightMovesα x)] [∀ (x : β), Small.{u, w} ↑(leftMovesβ x)] [∀ (x : β), Small.{u, w} ↑(rightMovesβ x)] (b : Bool) (x y : α × β) : corec (leftMoves leftMovesα rightMovesα leftMovesβ rightMovesβ) (rightMoves leftMovesα rightMovesα leftMovesβ rightMovesβ) (mulOption b x y) = toLGame leftMovesα rightMovesα leftMovesβ rightMovesβ (b, y.1, x.2) + toLGame leftMovesα rightMovesα leftMovesβ rightMovesβ (b, x.1, y.2) - toLGame leftMovesα rightMovesα leftMovesβ rightMovesβ (b, y.1, y.2)

theorem LGame.corec_mulTy {α : Type v} {β : Type w} (leftMovesα rightMovesα : α → Set α) (leftMovesβ rightMovesβ : β → Set β) [Hα : DecidableEq α] [Hβ : DecidableEq β] [∀ (x : α), Small.{u, v} ↑(leftMovesα x)] [∀ (x : α), Small.{u, v} ↑(rightMovesα x)] [∀ (x : β), Small.{u, w} ↑(leftMovesβ x)] [∀ (x : β), Small.{u, w} ↑(rightMovesβ x)] (x : MulTy α β) : corec (MulTy.leftMoves leftMovesα rightMovesα leftMovesβ rightMovesβ) (MulTy.rightMoves leftMovesα rightMovesα leftMovesβ rightMovesβ) x = (Multiset.map (MulTy.toLGame leftMovesα rightMovesα leftMovesβ rightMovesβ) x).sum

theorem LGame.MulTy.corec_swap {α : Type v} {β : Type w} (leftMovesα rightMovesα : α → Set α) (leftMovesβ rightMovesβ : β → Set β) [Hα : DecidableEq α] [Hβ : DecidableEq β] [∀ (x : α), Small.{u, v} ↑(leftMovesα x)] [∀ (x : α), Small.{u, v} ↑(rightMovesα x)] [∀ (x : β), Small.{u, w} ↑(leftMovesβ x)] [∀ (x : β), Small.{u, w} ↑(rightMovesβ x)] (x : MulTy α β) : corec (leftMoves leftMovesβ rightMovesβ leftMovesα rightMovesα) (rightMoves leftMovesβ rightMovesβ leftMovesα rightMovesα) x.swap = corec (leftMoves leftMovesα rightMovesα leftMovesβ rightMovesβ) (rightMoves leftMovesα rightMovesα leftMovesβ rightMovesβ) 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.leftMoves LGame.rightMoves LGame.leftMoves LGame.rightMoves (true, x, y) }

theorem LGame.corec_mul_corec {α : Type v} {β : Type w} (leftMovesα rightMovesα : α → Set α) (leftMovesβ rightMovesβ : β → Set β) [Hα : DecidableEq α] [Hβ : DecidableEq β] [∀ (x : α), Small.{u, v} ↑(leftMovesα x)] [∀ (x : α), Small.{u, v} ↑(rightMovesα x)] [∀ (x : β), Small.{u, w} ↑(leftMovesβ x)] [∀ (x : β), Small.{u, w} ↑(rightMovesβ x)] (initα : α) (initβ : β) : corec leftMovesα rightMovesα initα * corec leftMovesβ rightMovesβ initβ = MulTy.toLGame leftMovesα rightMovesα leftMovesβ rightMovesβ (true, 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.leftMoves_mul (x y : LGame) : (x * y).leftMoves = (fun (a : LGame × LGame) => mulOption x y a.1 a.2) '' (x.leftMoves ×ˢ y.leftMoves ∪ x.rightMoves ×ˢ y.rightMoves)

@[simp]

theorem LGame.rightMoves_mul (x y : LGame) : (x * y).rightMoves = (fun (a : LGame × LGame) => mulOption x y a.1 a.2) '' (x.leftMoves ×ˢ y.rightMoves ∪ x.rightMoves ×ˢ y.leftMoves)

@[simp]

theorem LGame.leftMoves_mulOption (x y a b : LGame) : (mulOption x y a b).leftMoves = (a * y + x * b - a * b).leftMoves

@[simp]

theorem LGame.rightMoves_mulOption (x y a b : LGame) : (mulOption x y a b).rightMoves = (a * y + x * b - a * b).rightMoves

instance LGame.instCommMagma : CommMagma LGame

Equations

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

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 }