Type of players

This file implements the two-element type of players (Left, Right), alongside other basic notational machinery to be used within game theory.

Players

inductive Player : Type

Either the Left or Right player.

• left : Player

  The Left player.

• right : Player

  The Right player.

instance instDecidableEqPlayer : DecidableEq Player

Equations

• instDecidableEqPlayer x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance instFintypePlayer : Fintype Player

Equations

• instFintypePlayer = { elems := { val := ↑Player.enumList, nodup := Player.enumList_nodup }, complete := instFintypePlayer._proof_1 }

def instInhabitedPlayer.default : Player

Equations

• instInhabitedPlayer.default = Player.left

instance instInhabitedPlayer : Inhabited Player

Equations

• instInhabitedPlayer = { default := instInhabitedPlayer.default }

@[reducible, inline]

abbrev Player.cases {α : Sort u_1} (l r : α) : Player → α

Specify a function Player → α from its two outputs.

Equations

• Player.cases l r Player.left = l
• Player.cases l r Player.right = r

theorem Player.apply_cases {α : Sort u_1} {β : Sort u_2} (f : α → β) (l r : α) (p : Player) : f (cases l r p) = cases (f l) (f r) p

@[simp]

theorem Player.cases_inj {α : Sort u_1} {l₁ r₁ l₂ r₂ : α} : cases l₁ r₁ = cases l₂ r₂ ↔ l₁ = l₂ ∧ r₁ = r₂

theorem Player.const_of_left_eq_right {α : Sort u_1} {f : Player → α} (hf : f left = f right) (p q : Player) : f p = f q

theorem Player.const_of_left_eq_right' {f : Player → Prop} (hf : f left ↔ f right) (p q : Player) : f p ↔ f q

@[simp]

theorem Player.forall {p : Player → Prop} : (∀ (x : Player), p x) ↔ p left ∧ p right

@[simp]

theorem Player.exists {p : Player → Prop} : (∃ (x : Player), p x) ↔ p left ∨ p right

instance Player.instNeg : Neg Player

Equations

• Player.instNeg = { neg := Player.cases Player.right Player.left }

@[simp]

theorem Player.neg_left : -left = right

@[simp]

theorem Player.neg_right : -right = left

instance Player.instInvolutiveNeg : InvolutiveNeg Player

Equations

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

instance Player.instMul : Mul Player

The multiplication of Players is used to state the lemmas about the multiplication of combinatorial games, such as IGame.mulOption_mem_moves_mul.

Equations

• Player.instMul = { mul := fun (x x_1 : Player) => match x, x_1 with | Player.left, p => p | Player.right, p => -p }

@[simp]

theorem Player.left_mul (p : Player) : left * p = p

@[simp]

theorem Player.right_mul (p : Player) : right * p = -p

@[simp]

theorem Player.mul_left (p : Player) : p * left = p

@[simp]

theorem Player.mul_right (p : Player) : p * right = -p

@[simp]

theorem Player.mul_self (p : Player) : p * p = left

instance Player.instHasDistribNeg : HasDistribNeg Player

Equations

• Player.instHasDistribNeg = { toInvolutiveNeg := Player.instInvolutiveNeg, neg_mul := Player.instHasDistribNeg._proof_1, mul_neg := Player.instHasDistribNeg._proof_2 }

instance Player.instCommGroup : CommGroup Player

Equations

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

@[simp]

theorem Player.one_eq_left : 1 = left

@[simp]

theorem Player.inv_eq_self (p : Player) : p⁻¹ = p

OfSets

class OfSets (α : Type (u + 1)) (Valid : outParam ((Player → Set α) → Prop)) : Type (u + 1)

Type class for the ofSets operation. Used to implement the !{st} and !{s | t} syntax.

• ofSets (st : Player → Set α) (h : Valid st) [Small.{u, u + 1} ↑(st Player.left)] [Small.{u, u + 1} ↑(st Player.right)] : α

  Construct a combinatorial game from its left and right sets.

  Conventions for notations in identifiers:

  • The recommended spelling of !{st}'h in identifiers is ofSets.

  • The recommended spelling of !{s | t}'h in identifiers is ofSets.

  • The recommended spelling of !{st} in identifiers is ofSets.

  • The recommended spelling of !{s | t} in identifiers is ofSets.

def «term!{_}'_» : Lean.ParserDescr

Construct a combinatorial game from its left and right sets.

Conventions for notations in identifiers:

• The recommended spelling of !{st}'h in identifiers is ofSets.

Equations

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

def «term!{_|_}'_» : Lean.ParserDescr

Construct a combinatorial game from its left and right sets.

Conventions for notations in identifiers:

• The recommended spelling of !{s | t}'h in identifiers is ofSets.

Equations

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

def tacticOf_sets_tactic : Lean.ParserDescr

Equations

• tacticOf_sets_tactic = Lean.ParserDescr.node `tacticOf_sets_tactic 1024 (Lean.ParserDescr.nonReservedSymbol "of_sets_tactic" false)

def «term!{_}» : Lean.ParserDescr

Construct a combinatorial game from its left and right sets.

Conventions for notations in identifiers:

• The recommended spelling of !{st} in identifiers is ofSets.

Equations

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

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

Construct a combinatorial game from its left and right sets.

Conventions for notations in identifiers:

• The recommended spelling of !{s | t} in identifiers is ofSets.

Equations

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

def delabOfSets : Lean.PrettyPrinter.Delaborator.Delab

Equations

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

theorem ofSets_eq_ofSets_cases {α : Type (u_1 + 1)} {Valid : (Player → Set α) → Prop} [OfSets α Valid] (st : Player → Set α) (h : Valid st) [Small.{u_1, u_1 + 1} ↑(st Player.left)] [Small.{u_1, u_1 + 1} ↑(st Player.right)] : !{st} = !{st Player.left | st Player.right}