Misere combinatorial games.

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

The polynomial functor describing Left and Right option sets.

Equations

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

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

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

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

@[implicit_reducible]

instance MisereGames.GameFunctor.instFunctor : Functor GameFunctor

Equations

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

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

@[implicit_reducible]

noncomputable instance MisereGames.GameFunctor.instQPF : QPF GameFunctor

Equations

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

@[irreducible]

def MisereGames.GameForm : Type (u + 1)

The canonical type of combinatorial game forms.

Equations

• MisereGames.GameForm = QPF.Fix MisereGames.GameFunctor

@[implicit_reducible]

noncomputable instance MisereGames.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.

@[implicit_reducible]

instance MisereGames.GameForm.instMoves : Moves GameForm

Equations

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

def MisereGames.GameForm.«term_ᴸ» : Lean.TrailingParserDescr

The set of Left options of the game.

Equations

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

def MisereGames.GameForm.«term_ᴿ» : Lean.TrailingParserDescr

The set of Right options of the game.

Equations

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

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

@[simp]

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

@[simp]

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

theorem MisereGames.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 MisereGames.GameForm.ext_iff {x y : GameForm} : x = y ↔ ∀ (p : Player), Moves.moves p x = Moves.moves p y

theorem MisereGames.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 MisereGames.GameForm.instSmallSubtypeIsOption (x : GameForm) : Small.{u, u + 1} { y : GameForm // Moves.IsOption y x }

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

@[irreducible]

def MisereGames.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

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

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

@[implicit_reducible]

noncomputable instance MisereGames.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

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

@[implicit_reducible]

noncomputable instance MisereGames.GameForm.instInvolutiveNeg : InvolutiveNeg GameForm

Equations

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

theorem MisereGames.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 MisereGames.GameForm.neg_eq (x : GameForm) : -x = !{-Moves.moves Player.right x | -Moves.moves Player.left x}

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

Addition and subtraction

@[implicit_reducible]

noncomputable instance MisereGames.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

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

theorem MisereGames.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 MisereGames.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 MisereGames.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 MisereGames.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 MisereGames.GameForm.isOption_neg {x y : GameForm} : Moves.IsOption x (-y) ↔ Moves.IsOption (-x) y

@[simp]

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

theorem MisereGames.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 MisereGames.GameForm.IsOption.add_left {x y z : GameForm} (h : Moves.IsOption x y) : Moves.IsOption (z + x) (z + y)

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

@[implicit_reducible]

noncomputable instance MisereGames.GameForm.instAddCommSemigroup : AddCommSemigroup GameForm

Equations

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

@[implicit_reducible]

noncomputable instance MisereGames.GameForm.instForm : Form GameForm

Equations

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

@[simp]

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

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

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

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

@[simp]

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

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