def GameFunctor (α : Type (u + 1)) : Type (u + 1)

Equations

• GameFunctor α = { s : Player → Set α // ∀ (p : Player), Small.{?u.10, ?u.10 + 1} ↑(s p) }

theorem GameFunctor.ext {α : Type (u + 1)} {x y : GameFunctor α} : ↑x = ↑y → x = y

theorem GameFunctor.ext_iff {α : Type (u + 1)} {x y : GameFunctor α} : x = y ↔ ↑x = ↑y

instance GameFunctor.instSmallElemValForallPlayerSetForall {α : Type (u + 1)} (x : GameFunctor α) (p : Player) : Small.{u, u + 1} ↑(↑x p)

@[instance_reducible]

instance GameFunctor.instFunctor : Functor GameFunctor

Equations

• GameFunctor.instFunctor = { map := fun {α β : Type (?u.21 + 1)} (f : α → β) (s : GameFunctor α) => ⟨fun (x : Player) => f '' ↑s x, ⋯⟩ }

theorem GameFunctor.map_def {α β : Type (u_1 + 1)} (f : α → β) (s : GameFunctor α) : f <$> s = ⟨fun (x : Player) => f '' ↑s x, ⋯⟩

@[instance_reducible]

instance GameFunctor.instQPF : QPF GameFunctor

Equations

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

@[irreducible]

def GameForm : Type (u + 1)

Equations

• GameForm = QPF.Fix GameFunctor

@[instance_reducible]

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

Construct a GameForm from its Left and Right options.

Equations

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

@[instance_reducible]

instance GameForm.instMoves : Moves GameForm

Equations

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

def GameForm.«term_ᴸ» : Lean.TrailingParserDescr

The set of Left options of the game.

Equations

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

def GameForm.«term_ᴿ» : Lean.TrailingParserDescr

The set of Right options of the game.

Equations

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

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

@[simp]

theorem GameForm.ofSets_moves (x : GameForm) : !{fun (p : Player) => Moves.moves p x} = x

@[simp]

theorem GameForm.ofSets_leftMoves_rightMoves (x : GameForm) : !{Moves.moves Player.left x | Moves.moves Player.right x} = x

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

Two GameForms are equal when their option sets are.

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

theorem GameForm.ofSets_inj {s₁ s₂ t₁ t₂ : Set GameForm} [Small.{u_1, u_1 + 1} ↑s₁] [Small.{u_1, u_1 + 1} ↑s₂] [Small.{u_1, u_1 + 1} ↑t₁] [Small.{u_1, u_1 + 1} ↑t₂] : !{s₁ | t₁} = !{s₂ | t₂} ↔ s₁ = s₂ ∧ t₁ = t₂

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

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

@[irreducible]

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

Conway induction: build data for a game by recursively building it on its Left and Right sets. This rarely needs to be used explicitly, as the termination checker will handle it.

See ofSetsRecOn for an alternate form.

Equations

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

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

def GameForm.ofSetsRecOn {motive : GameForm → Sort u_1} (x : GameForm) (mk : (s t : Set GameForm) → [inst : Small.{u, u + 1} ↑s] → [inst_1 : Small.{u, u + 1} ↑t] → ((x : GameForm) → x ∈ s → motive x) → ((x : GameForm) → x ∈ t → motive x) → motive !{s | t}) : motive x

Conway induction: build data for a game by recursively building it on its Left and Right sets. This rarely needs to be used explicitly, as the termination checker will handle it.

See moveRecOn for an alternate form.

Equations

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

@[simp]

theorem GameForm.ofSetsRecOn_ofSets {motive : GameForm → Sort u_1} (s t : Set GameForm) [Small.{u, u + 1} ↑s] [Small.{u, u + 1} ↑t] (mk : (s t : Set GameForm) → [inst : Small.{u, u + 1} ↑s] → [inst_1 : Small.{u, u + 1} ↑t] → ((x : GameForm) → x ∈ s → motive x) → ((x : GameForm) → x ∈ t → motive x) → motive !{s | t}) : ofSetsRecOn !{s | t} mk = mk s t (fun (y : GameForm) (x : y ∈ s) => ofSetsRecOn y mk) fun (y : GameForm) (x : y ∈ t) => ofSetsRecOn y mk

@[instance_reducible]

instance GameForm.instNeg : Neg GameForm

$\def\form<#1>[#2]{\left\{#1 \mid #2\right\}}$ The conjugate of a game is defined by -!{s | t} = !{-t | -s}. In the literature, one would see $$ \overline{G}=\form<\overline{G^\mathcal{R}}>[\overline{G^\mathcal{L}}]. $$ In this repository, the conjugate is often referred to as the 'negative', even though it is not necessarily an additive inverse.

Equations

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

@[instance_reducible]

instance GameForm.instInvolutiveNeg : InvolutiveNeg GameForm

Equations

• GameForm.instInvolutiveNeg = { toNeg := GameForm.instNeg, neg_neg := ⋯ }

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

theorem GameForm.neg_eq (x : GameForm) : -x = !{-Moves.moves Player.right x | -Moves.moves Player.left x}

theorem GameForm.neg_eq' (x : GameForm) : -x = !{fun (p : Player) => -Moves.moves (-p) x}

Addition and subtraction

@[instance_reducible]

instance GameForm.instAdd : Add GameForm

$\def\form<#1>[#2]{\left\{#1 \mid #2\right\}}$ The sum of x = !{s₁ | t₁} and y = !{s₂ | t₂} is !{s₁ + y, x + s₂ | t₁ + y, x + t₂}. In the literature, one would see $$ G+H=\form<G^\mathcal{L}+H,G+H^\mathcal{L}>[G^\mathcal{R}+H,G+H^\mathcal{R}]. $$

Equations

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

theorem GameForm.add_eq (x y : GameForm) : x + y = !{(fun (x : GameForm) => x + y) '' Moves.moves Player.left x ∪ (fun (x_1 : GameForm) => x + x_1) '' Moves.moves Player.left y | (fun (x : GameForm) => x + y) '' Moves.moves Player.right x ∪ (fun (x_1 : GameForm) => x + x_1) '' Moves.moves Player.right y}

theorem GameForm.add_eq' (x y : GameForm) : x + y = !{fun (p : Player) => (fun (x : GameForm) => x + y) '' Moves.moves p x ∪ (fun (x_1 : GameForm) => x + x_1) '' Moves.moves p y}

theorem GameForm.ofSets_add_ofSets (s₁ t₁ s₂ t₂ : Set GameForm) [Small.{u_1, u_1 + 1} ↑s₁] [Small.{u_1, u_1 + 1} ↑t₁] [Small.{u_1, u_1 + 1} ↑s₂] [Small.{u_1, u_1 + 1} ↑t₂] : !{s₁ | t₁} + !{s₂ | t₂} = !{(fun (x : GameForm) => x + !{s₂ | t₂}) '' s₁ ∪ (fun (x : GameForm) => !{s₁ | t₁} + x) '' s₂ | (fun (x : GameForm) => x + !{s₂ | t₂}) '' t₁ ∪ (fun (x : GameForm) => !{s₁ | t₁} + x) '' t₂}

theorem GameForm.ofSets_add_ofSets' (st₁ st₂ : Player → Set GameForm) [Small.{u_1, u_1 + 1} ↑(st₁ Player.left)] [Small.{u_1, u_1 + 1} ↑(st₂ Player.left)] [Small.{u_1, u_1 + 1} ↑(st₁ Player.right)] [Small.{u_1, u_1 + 1} ↑(st₂ Player.right)] : !{st₁} + !{st₂} = !{fun (p : Player) => (fun (x : GameForm) => x + !{st₂}) '' st₁ p ∪ (fun (x : GameForm) => !{st₁} + x) '' st₂ p}

theorem GameForm.isOption_neg {x y : GameForm} : Moves.IsOption x (-y) ↔ Moves.IsOption (-x) y

@[simp]

theorem GameForm.isOption_neg_neg {x y : GameForm} : Moves.IsOption (-x) (-y) ↔ Moves.IsOption x y

theorem GameForm.forall_moves_neg {P : GameForm → Prop} {p : Player} {x : GameForm} : (∀ y ∈ Moves.moves p (-x), P y) ↔ ∀ y ∈ Moves.moves (-p) x, P (-y)

theorem GameForm.IsOption.add_left {x y z : GameForm} (h : Moves.IsOption x y) : Moves.IsOption (z + x) (z + y)

theorem GameForm.IsOption.add_right {x y z : GameForm} (h : Moves.IsOption x y) : Moves.IsOption (x + z) (y + z)

@[instance_reducible]

instance GameForm.instAddCommSemigroup : AddCommSemigroup GameForm

Equations

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

@[instance_reducible]

instance GameForm.instForm : Form GameForm

Equations

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

@[simp]

theorem GameForm.isEndLike_iff_isEnd {g : GameForm} {p : Player} : Form.IsEndLike p g ↔ Form.IsEnd p g

theorem GameForm.leftEnd_rightEnd_eq_zero {g : GameForm} (h1 : Form.IsEnd Player.left g) (h2 : Form.IsEnd Player.right g) : g = 0

theorem GameForm.both_ends_eq_zero {g : GameForm} {p : Player} (h1 : Form.IsEnd p g) (h2 : Form.IsEnd (-p) g) : g = 0

theorem GameForm.ne_zero_not_end {g : GameForm} (h1 : g ≠ 0) : ∃ (p : Player), ¬Form.IsEnd p g

@[simp]

theorem GameForm.zero_not_both_end {g : GameForm} {p : Player} (h1 : g ≠ 0) (h2 : Form.IsEnd p g) : ¬Form.IsEnd (-p) g

theorem GameForm.isOption_zero_add_iff {g h : GameForm} : Moves.IsOption 0 (g + h) ↔ Moves.IsOption 0 g ∧ h = 0 ∨ Moves.IsOption 0 h ∧ g = 0