Documentation

CombinatorialGames.Nimber.Basic

Nimbers #

The goal of this file is to define the nimbers, constructed as ordinals endowed with new arithmetical operations. The nim sum a + b is recursively defined as the least ordinal not equal to any a' + b or a + b' for a' < a and b' < b. There is also a nim product, defined in the CombinatorialGames.Nimber.Field file.

Nim arithmetic arises within the context of impartial games. By the Sprague-Grundy theorem, each impartial game is equivalent to some game of nim. If x ≈ nim o₁ and y ≈ nim o₂, then x + y ≈ nim (o₁ + o₂) and x * y ≈ nim (o₁ * o₂), where the ordinals are summed or multiplied together as nimbers.

Notation #

Following [On Numbers And Games][conway2001] (p. 121), we define notation ∗o for the cast from Ordinal to Nimber. Note that for general n : ℕ, ∗n is not the same as ↑n. For instance, ∗2 ≠ 0, whereas ↑2 = ↑1 + ↑1 = 0.

Implementation notes #

The nimbers inherit the order from the ordinals - this makes working with minimum excluded values much more convenient. However, the fact that nimbers are of characteristic 2 prevents the order from interacting with the arithmetic in any nice way.

To reduce API duplication, we opt not to implement operations on Nimber on Ordinal. The order isomorphisms Nimber.of and Nimber.val allow us to cast between them whenever needed.

Basic casts between `Ordinal` and `Nimber` #

instance Nimber.instNeZeroOfNat :

instance Nimber.instUncountable :

Uncountable Nimber

theorem Nimber.of_eq_iff {a✝ : Ordinal.{u_1}} {b✝ : Nimber} :

of a✝ = b✝ ↔ a✝ = val b✝

theorem Nimber.of_le_iff {a✝ : Ordinal.{u_1}} {b✝ : Nimber} :

of a✝ ≤ b✝ ↔ a✝ ≤ val b✝

@[simp]

theorem Nimber.succ_zero :

Order.succ 0 = 1

instance Nimber.instSmallElemIio (a✝ : Nimber) :

Small.{u✝, u✝ + 1} ↑(Set.Iio a✝)

instance Nimber.instIsEmptyElemIioOfNat :

IsEmpty ↑(Set.Iio 0)

@[simp]

theorem Nimber.val_of (a✝ : Ordinal.{u_1}) :

val (of a✝) = a✝

@[simp]

theorem Nimber.succ_ne_zero (a✝ : Nimber) :

Order.succ a✝ ≠ 0

instance instNontrivialNimber :

Nontrivial Nimber

Equations

instNontrivialNimber = Ordinal.nontrivial

noncomputable instance Nimber.instConditionallyCompleteLinearOrderBot :

ConditionallyCompleteLinearOrderBot Nimber

Equations

Nimber.instConditionallyCompleteLinearOrderBot = inferInstanceAs (ConditionallyCompleteLinearOrderBot Ordinal.{?u.2})

instance Nimber.instOrderBot :

OrderBot Nimber

Equations

Nimber.instOrderBot = inferInstanceAs (OrderBot Ordinal.{?u.2})

@[simp]

theorem Nimber.of_eq_zero {a✝ : Ordinal.{u_1}} :

of a✝ = 0 ↔ a✝ = 0

@[simp]

theorem Nimber.of_zero :

of 0 = 0

@[simp]

theorem Nimber.Iio_one_default_eq :

default = ⟨0, ⋯⟩

instance Nimber.instPartialOrder :

PartialOrder Nimber

Equations

Nimber.instPartialOrder = inferInstanceAs (PartialOrder Ordinal.{?u.2})

@[simp]

theorem Nimber.of_eq_one {a✝ : Ordinal.{u_1}} :

of a✝ = 1 ↔ a✝ = 1

@[simp]

theorem Nimber.of_symm :

instance Nimber.instSuccOrder :

SuccOrder Nimber

Equations

Nimber.instSuccOrder = inferInstanceAs (SuccOrder Ordinal.{?u.2})

instance Nimber.instSmallElemIco (a✝ b✝ : Nimber) :

Small.{u✝, u✝ + 1} ↑(Set.Ico a✝ b✝)

theorem Nimber.iSup_eq_zero_iff {ι✝ : Type u_1} [Small.{u✝, u_1} ι✝] {f✝ : ι✝ → Nimber} :

⨆ (i : ι✝), f✝ i = 0 ↔ ∀ (i : ι✝), f✝ i = 0

@[simp]

theorem Nimber.bot_eq_zero :

@[simp]

theorem Nimber.lt_one_iff_zero {a✝ : Nimber} :

a✝ < 1 ↔ a✝ = 0

@[simp]

theorem Nimber.of_one :

of 1 = 1

theorem Nimber.of_lt_iff {a✝ : Ordinal.{u_1}} {b✝ : Nimber} :

of a✝ < b✝ ↔ a✝ < val b✝

theorem Nimber.le_one_iff {a✝ : Nimber} :

a✝ ≤ 1 ↔ a✝ = 0 ∨ a✝ = 1

theorem Nimber.val_lt_iff {a✝ : Nimber} {b✝ : Ordinal.{u_1}} :

val a✝ < b✝ ↔ a✝ < of b✝

@[simp]

theorem Nimber.val_image_Iio (a✝ : Nimber) :

⇑val '' Set.Iio a✝ = Set.Iio (val a✝)

@[simp]

theorem Nimber.one_le_iff_ne_zero {a✝ : Nimber} :

1 ≤ a✝ ↔ a✝ ≠ 0

theorem Nimber.not_bddAbove_compl_of_small (s✝ : Set Nimber) [Small.{u✝, u✝ + 1} ↑s✝] :

¬BddAbove s✝ᶜ

noncomputable instance Nimber.instLinearOrder :

LinearOrder Nimber

Equations

Nimber.instLinearOrder = Ordinal.instLinearOrder

theorem Nimber.lt_wf :

WellFounded fun (x1 x2 : Nimber) => x1 < x2

@[simp]

theorem Nimber.val_symm :

instance instWellFoundedRelationNimber :

WellFoundedRelation Nimber

Equations

instWellFoundedRelationNimber = Ordinal.wellFoundedRelation

instance Nimber.instZeroLEOneClass :

ZeroLEOneClass Nimber

@[simp]

theorem Nimber.of_val (a✝ : Nimber) :

of (val a✝) = a✝

instance Nimber.instSmallElemIoo (a✝ b✝ : Nimber) :

Small.{u✝, u✝ + 1} ↑(Set.Ioo a✝ b✝)

theorem Nimber.val_eq_iff {a✝ : Nimber} {b✝ : Ordinal.{u_1}} :

val a✝ = b✝ ↔ a✝ = of b✝

instance instInhabitedNimber :

Inhabited Nimber

Equations

instInhabitedNimber = Ordinal.inhabited

@[simp]

theorem Nimber.le_zero {a✝ : Nimber} :

a✝ ≤ 0 ↔ a✝ = 0

instance Nimber.instNoMaxOrder :

NoMaxOrder Nimber

@[simp]

theorem Nimber.val_one :

val 1 = 1

@[simp]

theorem Nimber.zero_le (a✝ : Nimber) :

0 ≤ a✝

@[simp]

theorem Nimber.val_zero :

val 0 = 0

instance Nimber.instSmallElemIic (a✝ : Nimber) :

Small.{u✝, u✝ + 1} ↑(Set.Iic a✝)

instance instZeroNimber :

Equations

instZeroNimber = Ordinal.zero

theorem Nimber.induction {p✝ : Nimber → Prop} (i✝ : Nimber) :

(∀ (j : Nimber), (∀ k < j, p✝ k) → p✝ j) → p✝ i✝

Well-founded induction for Nimber.

instance Nimber.instWellFoundedLT :

WellFoundedLT Nimber

@[simp]

theorem Nimber.succ_of (a✝ : Ordinal.{u_1}) :

Order.succ (of a✝) = of (a✝ + 1)

instance Nimber.instSmallElemIoc (a✝ b✝ : Nimber) :

Small.{u✝, u✝ + 1} ↑(Set.Ioc a✝ b✝)

theorem Nimber.bddAbove_iff_small {s✝ : Set Nimber} :

BddAbove s✝ ↔ Small.{u✝, u✝ + 1} ↑s✝

@[simp]

theorem Nimber.of_image_Iio (a✝ : Ordinal.{u_1}) :

⇑of '' Set.Iio a✝ = Set.Iio (of a✝)

def Nimber.ind {motive✝ : Nimber → Sort u_1} (mk : (a : Ordinal.{u_2}) → motive✝ (of a)) (a✝ : Nimber) :

motive✝ a✝

A recursor for Nimber. Use as induction x.

Equations

Nimber.ind mk a✝ = mk (Nimber.val a✝)

Instances For

@[simp]

theorem Nimber.val_eq_zero {a✝ : Nimber} :

val a✝ = 0 ↔ a✝ = 0

theorem Nimber.pos_iff_ne_zero {a✝ : Nimber} :

0 < a✝ ↔ a✝ ≠ 0

def Nimber :

Type (u_1 + 1)

A type synonym for ordinals with nimber addition and multiplication.

Equations

Nimber = Ordinal.{?u.2}

Instances For

theorem Nimber.eq_natCast_of_le_natCast {a✝ : Nimber} {b✝ : ℕ} :

a✝ ≤ of ↑b✝ → ∃ (c : ℕ), a✝ = of ↑c

@[simp]

theorem Nimber.val_eq_one {a✝ : Nimber} :

val a✝ = 1 ↔ a✝ = 1

theorem Nimber.bddAbove_of_small (s✝ : Set Nimber) [Small.{u✝, u✝ + 1} ↑s✝] :

instance instOneNimber :

Equations

instOneNimber = Ordinal.one

theorem Nimber.le_iSup {ι✝ : Type u_1} (f✝ : ι✝ → Nimber) [Small.{u✝, u_1} ι✝] (i✝ : ι✝) :

f✝ i✝ ≤ iSup f✝

theorem Nimber.lt_iSup_iff {ι✝ : Type u_1} [Small.{u✝, u_1} ι✝] (f✝ : ι✝ → Nimber) {x✝ : Nimber} :

x✝ < ⨆ (i : ι✝), f✝ i ↔ ∃ (i : ι✝), x✝ < f✝ i

@[match_pattern]

def Nimber.of :

Ordinal.{u_1} ≃o Nimber

The identity function between Ordinal._@.CombinatorialGames.Nimber.Basic.3967026805._hygCtx._hyg.3 and Nimber.

Equations

Nimber.of = OrderIso.refl Ordinal.{?u.2}

Instances For

theorem Nimber.iSup_le_iff {ι✝ : Type u_1} {f✝ : ι✝ → Nimber} {a✝ : Nimber} [Small.{u✝, u_1} ι✝] :

⨆ (i : ι✝), f✝ i ≤ a✝ ↔ ∀ (i : ι✝), f✝ i ≤ a✝

instance Nimber.instSmallElemIcc (a✝ b✝ : Nimber) :

Small.{u✝, u✝ + 1} ↑(Set.Icc a✝ b✝)

@[simp]

theorem Nimber.not_neg (a✝ : Nimber) :

¬a✝ < 0

theorem Nimber.val_le_iff {a✝ : Nimber} {b✝ : Ordinal.{u_1}} :

val a✝ ≤ b✝ ↔ a✝ ≤ of b✝

@[match_pattern]

def Nimber.val :

Nimber ≃o Ordinal.{u_1}

The identity function between Nimber and Ordinal._@.CombinatorialGames.Nimber.Basic.3967026805._hygCtx._hyg.3.

Equations

Nimber.val = OrderIso.refl Nimber

Instances For

theorem Nimber.eq_zero_or_pos (a✝ : Nimber) :

a✝ = 0 ∨ 0 < a✝

theorem Nimber.succ_def (a✝ : Nimber) :

Order.succ a✝ = of (val a✝ + 1)

instance Nimber.instUniqueElemIioOfNat :

Unique ↑(Set.Iio 1)

Equations

Nimber.instUniqueElemIioOfNat = Ordinal.uniqueIioOne

def Nimber.«term∗_» :

Lean.ParserDescr

The identity function between Ordinal._@.CombinatorialGames.Nimber.Basic.3967026805._hygCtx._hyg.3 and Nimber.

Conventions for notations in identifiers:

The recommended spelling of ∗ in identifiers is of.

Equations

Nimber.«term∗_» = Lean.ParserDescr.node `Nimber.«term∗_» 75 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "∗") (Lean.ParserDescr.cat `term 75))

Instances For

Nimber addition #

@[irreducible]

def Nimber.add (a b : Nimber) :

Nimber addition is recursively defined so that a + b is the smallest nimber not equal to a' + b or a + b' for a' < a and b' < b.

Equations

a.add b = sInf {x : Nimber | (∃ (a' : Nimber) (_ : a' < a), a'.add b = x) ∨ ∃ (b' : Nimber) (_ : b' < b), a.add b' = x}ᶜ

Instances For

instance Nimber.instAdd :

Equations

Nimber.instAdd = { add := Nimber.add }

theorem Nimber.add_def (a b : Nimber) :

a + b = sInf {x : Nimber | (∃ a' < a, a' + b = x) ∨ ∃ b' < b, a + b' = x}ᶜ

theorem Nimber.exists_of_lt_add {a b c : Nimber} (h : c < a + b) :

(∃ a' < a, a' + b = c) ∨ ∃ b' < b, a + b' = c

theorem Nimber.add_le_of_forall_ne {a b c : Nimber} (h₁ : ∀ a' < a, a' + b ≠ c) (h₂ : ∀ b' < b, a + b' ≠ c) :

a + b ≤ c

@[irreducible]

theorem Nimber.add_comm (a b : Nimber) :

a + b = b + a

instance Nimber.instIsLeftCancelAdd :

IsLeftCancelAdd Nimber

instance Nimber.instIsRightCancelAdd :

IsRightCancelAdd Nimber

@[irreducible]

theorem Nimber.add_eq_zero {a b : Nimber} :

a + b = 0 ↔ a = b

theorem Nimber.add_ne_zero_iff {a b : Nimber} :

a + b ≠ 0 ↔ a ≠ b

@[simp]

theorem Nimber.add_self (a : Nimber) :

a + a = 0

@[irreducible]

theorem Nimber.add_assoc (a b c : Nimber) :

a + b + c = a + (b + c)

@[irreducible]

theorem Nimber.add_zero (a : Nimber) :

a + 0 = a

theorem Nimber.zero_add (a : Nimber) :

0 + a = a

instance Nimber.instNeg :

Equations

Nimber.instNeg = { neg := id }

@[simp]

theorem Nimber.neg_eq (a : Nimber) :

-a = a

instance Nimber.instAddCommGroupWithOne :

AddCommGroupWithOne Nimber

Equations

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

theorem Nimber.natCast_eq_if (n : ℕ) :

↑n = if Even n then 0 else 1

theorem Nimber.natCast_eq_mod (n : ℕ) :

↑n = ↑(n % 2)

@[simp]

theorem Nimber.ofNat_eq_mod (n : ℕ) [n.AtLeastTwo] :

OfNat.ofNat n = ↑(n % 2)

@[simp]

theorem Nimber.add_cancel_right (a b : Nimber) :

a + b + b = a

@[simp]

theorem Nimber.add_cancel_left (a b : Nimber) :

a + (a + b) = b

theorem Nimber.add_trichotomy {a b c : Nimber} (h : a + b + c ≠ 0) :

b + c < a ∨ c + a < b ∨ a + b < c

theorem Nimber.lt_add_cases {a b c : Nimber} (h : a < b + c) :

a + c < b ∨ a + b < c

@[irreducible]

theorem Nimber.add_nat (a b : ℕ) :

of ↑a + of ↑b = of ↑(a ^^^ b)

Nimber addition of naturals corresponds to the bitwise XOR operation.