Dyadic games

A combinatorial game that is both Short and Numeric is called dyadic. We show that the dyadic games are in correspondence with the Dyadic rationals, in the sense that there exists a map Dyadic.toIGame such that:

• Dyadic.toIGame x is always a dyadic game.
• For any dyadic game y, there exists x with Dyadic.toIGame x ≈ y.
• The map Dyadic.toGame (defined in the obvious way) is a ring homomorphism.

Todo

Show the latter two bullet points.

For Mathlib

theorem le_of_le_of_lt_of_lt {α : Type u_1} {β : Type u_2} [PartialOrder α] [Preorder β] {x y : α} {f : α → β} (h : x < y → f x < f y) (hxy : x ≤ y) : f x ≤ f y

theorem Nat.pow_log_eq_self_iff {b n : ℕ} (hb : b ≠ 0) : b ^ log b n = n ↔ n ∈ Set.range fun (x : ℕ) => b ^ x

theorem Set.range_if {α : Type u_1} {β : Type u_2} {p : α → Prop} [DecidablePred p] {x y : β} (hp : ∃ (a : α), p a) (hn : ∃ (a : α), ¬p a) : (range fun (a : α) => if p a then x else y) = {x, y}

theorem range_zero_pow {M : Type u_1} [MonoidWithZero M] : (Set.range fun (x : ℕ) => 0 ^ x) = {1, 0}

instance instDecidableMemNatSetRangeHPow_combinatorialGames (b n : ℕ) : Decidable (n ∈ Set.range fun (x : ℕ) => b ^ x)

Equations

• instDecidableMemNatSetRangeHPow_combinatorialGames 0 n = decidable_of_iff (n ∈ {1, 0}) ⋯
• instDecidableMemNatSetRangeHPow_combinatorialGames b_2.succ n = decidable_of_iff ((b_2 + 1) ^ Nat.log (b_2 + 1) n = n) ⋯

theorem pos_of_mem_powers {n : ℕ} (h : n ∈ Submonoid.powers 2) : 0 < n

theorem ne_zero_of_mem_powers {n : ℕ} (h : n ∈ Submonoid.powers 2) : n ≠ 0

theorem dvd_iff_le_of_mem_powers {m n : ℕ} (hm : m ∈ Submonoid.powers 2) (hn : n ∈ Submonoid.powers 2) : m ∣ n ↔ m ≤ n

Dyadic numbers

This material belongs in Mathlib, though we do need to consider if the definition of Dyadic used here is the best one.

def IsDyadic (x : ℚ) : Prop

A dyadic rational number is one whose denominator is a power of two.

Equations

• IsDyadic x = (x.den ∈ Submonoid.powers 2)

instance instDecidableMemNatSubmonoidPowers_combinatorialGames {m n : ℕ} : Decidable (m ∈ Submonoid.powers n)

Equations

• instDecidableMemNatSubmonoidPowers_combinatorialGames = decidable_of_iff (m ∈ Set.range fun (x : ℕ) => n ^ x) ⋯

instance instDecidablePredRatIsDyadic : DecidablePred IsDyadic

Equations

• instDecidablePredRatIsDyadic x = inferInstanceAs (Decidable (x.den ∈ Submonoid.powers 2))

theorem IsDyadic.mkRat (x : ℤ) {y : ℕ} (hy : y ∈ Submonoid.powers 2) : IsDyadic (_root_.mkRat x y)

theorem IsDyadic.neg {x : ℚ} (hx : IsDyadic x) : IsDyadic (-x)

@[simp]

theorem IsDyadic.neg_iff {x : ℚ} : IsDyadic (-x) ↔ IsDyadic x

theorem IsDyadic.natCast (n : ℕ) : IsDyadic ↑n

theorem IsDyadic.intCast (n : ℤ) : IsDyadic ↑n

theorem IsDyadic.add {x y : ℚ} (hx : IsDyadic x) (hy : IsDyadic y) : IsDyadic (x + y)

theorem IsDyadic.sub {x y : ℚ} (hx : IsDyadic x) (hy : IsDyadic y) : IsDyadic (x - y)

theorem IsDyadic.mul {x y : ℚ} (hx : IsDyadic x) (hy : IsDyadic y) : IsDyadic (x * y)

theorem IsDyadic.nsmul {x : ℚ} (n : ℕ) (hx : IsDyadic x) : IsDyadic (n • x)

theorem IsDyadic.zsmul {x : ℚ} (n : ℤ) (hx : IsDyadic x) : IsDyadic (n • x)

theorem IsDyadic.pow {x : ℚ} (hx : IsDyadic x) (n : ℕ) : IsDyadic (x ^ n)

@[reducible, inline]

abbrev Dyadic : Type

The subtype of IsDyadic numbers.

We don't use Localization.Away 2, as this would not give us any computability, nor would it allow us to talk about numerators and denominators.

Equations

• Dyadic = Subtype IsDyadic

@[reducible, inline]

abbrev Dyadic.num (x : Dyadic) : ℤ

Numerator of a dyadic number.

Equations

• x.num = (↑x).num

@[reducible, inline]

abbrev Dyadic.den (x : Dyadic) : ℕ

Denominator of a dyadic number.

Equations

• x.den = (↑x).den

theorem Dyadic.den_ne_zero (x : Dyadic) : x.den ≠ 0

theorem Dyadic.den_pos (x : Dyadic) : 0 < x.den

theorem Dyadic.den_mem_powers (x : Dyadic) : x.den ∈ Submonoid.powers 2

@[simp]

theorem Dyadic.den_le_one_iff_eq_one {x : Dyadic} : x.den ≤ 1 ↔ x.den = 1

theorem Dyadic.ext {x y : Dyadic} (h : ↑x = ↑y) : x = y

theorem Dyadic.ext_iff {x y : Dyadic} : x = y ↔ ↑x = ↑y

instance Dyadic.instNatCast : NatCast Dyadic

Equations

• Dyadic.instNatCast = { natCast := fun (n : ℕ) => ⟨↑n, ⋯⟩ }

@[simp]

theorem Dyadic.val_natCast (n : ℕ) : ↑↑n = ↑n

@[simp]

theorem Dyadic.num_natCast (n : ℕ) : (↑n).num = ↑n

@[simp]

theorem Dyadic.den_natCast (n : ℕ) : (↑n).den = 1

instance Dyadic.instIntCast : IntCast Dyadic

Equations

• Dyadic.instIntCast = { intCast := fun (n : ℤ) => ⟨↑n, ⋯⟩ }

@[simp]

theorem Dyadic.val_intCast (n : ℤ) : ↑↑n = ↑n

@[simp]

theorem Dyadic.mk_intCast {n : ℤ} (h : IsDyadic ↑n) : ⟨↑n, h⟩ = ↑n

@[simp]

theorem Dyadic.num_intCast (n : ℤ) : (↑n).num = n

@[simp]

theorem Dyadic.den_intCast (n : ℤ) : (↑n).den = 1

instance Dyadic.instZero : Zero Dyadic

Equations

• Dyadic.instZero = { zero := ↑0 }

@[simp]

theorem Dyadic.val_zero : ↑0 = 0

@[simp]

theorem Dyadic.mk_zero (h : IsDyadic 0) : ⟨0, h⟩ = 0

@[simp]

theorem Dyadic.num_zero : num 0 = 0

@[simp]

theorem Dyadic.den_zero : den 0 = 1

instance Dyadic.instOne : One Dyadic

Equations

• Dyadic.instOne = { one := ↑1 }

@[simp]

theorem Dyadic.val_one : ↑1 = 1

@[simp]

theorem Dyadic.mk_one (h : IsDyadic 1) : ⟨1, h⟩ = 1

@[simp]

theorem Dyadic.num_one : num 1 = 1

@[simp]

theorem Dyadic.den_one : den 1 = 1

instance Dyadic.instNontrivial : Nontrivial Dyadic

instance Dyadic.instNeg : Neg Dyadic

Equations

• Dyadic.instNeg = { neg := fun (x : Dyadic) => ⟨-↑x, ⋯⟩ }

@[simp]

theorem Dyadic.val_neg (x : Dyadic) : ↑(-x) = -↑x

@[simp]

theorem Dyadic.neg_mk {x : ℚ} (hx : IsDyadic x) : -⟨x, hx⟩ = ⟨-x, ⋯⟩

@[simp]

theorem Dyadic.num_neg (x : Dyadic) : (-x).num = -x.num

@[simp]

theorem Dyadic.den_neg (x : Dyadic) : (-x).den = x.den

instance Dyadic.instAdd : Add Dyadic

Equations

• Dyadic.instAdd = { add := fun (x y : Dyadic) => ⟨↑x + ↑y, ⋯⟩ }

@[simp]

theorem Dyadic.val_add (x y : Dyadic) : ↑(x + y) = ↑x + ↑y

instance Dyadic.instSub : Sub Dyadic

Equations

• Dyadic.instSub = { sub := fun (x y : Dyadic) => ⟨↑x - ↑y, ⋯⟩ }

@[simp]

theorem Dyadic.val_sub (x y : Dyadic) : ↑(x - y) = ↑x - ↑y

instance Dyadic.instMul : Mul Dyadic

Equations

• Dyadic.instMul = { mul := fun (x y : Dyadic) => ⟨↑x * ↑y, ⋯⟩ }

@[simp]

theorem Dyadic.val_mul (x y : Dyadic) : ↑(x * y) = ↑x * ↑y

instance Dyadic.instSMulNat : SMul ℕ Dyadic

Equations

• Dyadic.instSMulNat = { smul := fun (x : ℕ) (y : Dyadic) => ⟨x • ↑y, ⋯⟩ }

@[simp]

theorem Dyadic.val_nsmul (x : ℕ) (y : Dyadic) : ↑(x • y) = x • ↑y

instance Dyadic.instSMulInt : SMul ℤ Dyadic

Equations

• Dyadic.instSMulInt = { smul := fun (x : ℤ) (y : Dyadic) => ⟨x • ↑y, ⋯⟩ }

@[simp]

theorem Dyadic.val_zsmul (x : ℤ) (y : Dyadic) : ↑(x • y) = x • ↑y

instance Dyadic.instNatPow : NatPow Dyadic

Equations

• Dyadic.instNatPow = { pow := fun (x : Dyadic) (y : ℕ) => ⟨↑x ^ y, ⋯⟩ }

@[simp]

theorem Dyadic.val_pow (x : Dyadic) (y : ℕ) : ↑(x ^ y) = ↑x ^ y

def Dyadic.half : Dyadic

The dyadic number ½.

Equations

• Dyadic.half = ⟨2⁻¹, Dyadic.half._proof_1⟩

@[simp]

theorem Dyadic.val_half : ↑half = 2⁻¹

@[simp]

theorem Dyadic.num_half : half.num = 1

@[simp]

theorem Dyadic.num_den : half.den = 2

def Dyadic.mkRat (m : ℤ) {n : ℕ} (h : n ∈ Submonoid.powers 2) : Dyadic

Constructor for the fraction m / n.

Equations

• Dyadic.mkRat m h = ⟨mkRat m n, ⋯⟩

@[simp]

theorem Dyadic.val_mkRat (m : ℤ) {n : ℕ} (h : n ∈ Submonoid.powers 2) : ↑(Dyadic.mkRat m h) = mkRat m n

@[simp]

theorem Dyadic.mkRat_self (x : Dyadic) : Dyadic.mkRat x.num ⋯ = x

@[simp]

theorem Dyadic.mkRat_one (m : ℤ) (h : 1 ∈ Submonoid.powers 2) : Dyadic.mkRat m h = ↑m

@[simp]

theorem Dyadic.mkRat_lt_mkRat {m n : ℤ} {k : ℕ} (h₁ h₂ : k ∈ Submonoid.powers 2) : Dyadic.mkRat m h₁ < Dyadic.mkRat n h₂ ↔ m < n

@[simp]

theorem Dyadic.mkRat_le_mkRat {m n : ℤ} {k : ℕ} (h₁ h₂ : k ∈ Submonoid.powers 2) : Dyadic.mkRat m h₁ ≤ Dyadic.mkRat n h₂ ↔ m ≤ n

instance Dyadic.instCommRing : CommRing Dyadic

Equations

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

instance Dyadic.instIsStrictOrderedRing : IsStrictOrderedRing Dyadic

theorem Dyadic.even_den {x : Dyadic} (hx : x.den ≠ 1) : Even x.den

theorem Dyadic.odd_num {x : Dyadic} (hx : x.den ≠ 1) : Odd x.num

theorem Dyadic.num_eq_self_of_den_eq_one {x : Dyadic} (hx : x.den = 1) : ↑x.num = x

theorem Dyadic.eq_mkRat_of_den_le {x : Dyadic} {n : ℕ} (h : x.den ≤ n) (hn : n ∈ Submonoid.powers 2) : ∃ (m : ℤ), x = Dyadic.mkRat m hn

instance Dyadic.instCanLiftIntCastEqNatDenValRatIsDyadicOfNat : CanLift Dyadic ℤ Int.cast fun (x : Dyadic) => (↑x).den = 1

Dyadic games

def Dyadic.lower (x : Dyadic) : Dyadic

For a dyadic number m / n, returns (m - 1) / n.

Equations

• x.lower = Dyadic.mkRat (x.num - 1) ⋯

def Dyadic.upper (x : Dyadic) : Dyadic

For a dyadic number m / n, returns (m + 1) / n.

Equations

• x.upper = Dyadic.mkRat (x.num + 1) ⋯

theorem Dyadic.den_lower_lt {x : Dyadic} (h : x.den ≠ 1) : x.lower.den < x.den

theorem Dyadic.den_upper_lt {x : Dyadic} (h : x.den ≠ 1) : x.upper.den < x.den

def Dyadic.tacticDyadic_wf : Lean.ParserDescr

An auxiliary tactic for inducting on the denominator of a Dyadic.

Equations

• Dyadic.tacticDyadic_wf = Lean.ParserDescr.node `Dyadic.tacticDyadic_wf 1024 (Lean.ParserDescr.nonReservedSymbol "dyadic_wf" false)

@[simp]

theorem Dyadic.lower_neg (x : Dyadic) : (-x).lower = -x.upper

@[simp]

theorem Dyadic.upper_neg (x : Dyadic) : (-x).upper = -x.lower

theorem Dyadic.le_lower_of_lt {x y : Dyadic} (hd : x.den ≤ y.den) (h : x < y) : x ≤ y.lower

theorem Dyadic.upper_le_of_lt {x y : Dyadic} (hd : y.den ≤ x.den) (h : x < y) : x.upper ≤ y

theorem Dyadic.lower_eq_of_den_eq_one {x : Dyadic} (h : x.den = 1) : x.lower = ↑x.num - 1

theorem Dyadic.upper_eq_of_den_eq_one {x : Dyadic} (h : x.den = 1) : x.upper = ↑x.num + 1

theorem Dyadic.lower_lt_upper (x : Dyadic) : x.lower < x.upper

@[irreducible]

noncomputable def Dyadic.toIGame (x : Dyadic) : IGame

Converts a dyadic rational into an IGame. This map is defined so that:

• If x : ℤ, then toIGame x = ↑x.
• Otherwise, if x = m / n with n even, then toIGame x = {(m - 1) / n | (m + 1) / n}ᴵ. Note that both options will have smaller denominators.

Equations

• x.toIGame = if x_1 : x.den = 1 then ↑x.num else {{x.lower.toIGame} | {x.upper.toIGame}}ᴵ

theorem Dyadic.toIGame_of_den_eq_one {x : Dyadic} (hx : x.den = 1) : x.toIGame = ↑x.num

@[simp]

theorem Dyadic.toIGame_intCast (n : ℤ) : (↑n).toIGame = ↑n

@[simp]

theorem Dyadic.toIGame_natCast (n : ℕ) : (↑n).toIGame = ↑n

@[simp]

theorem Dyadic.toIGame_zero : toIGame 0 = 0

@[simp]

theorem Dyadic.toIGame_one : toIGame 1 = 1

theorem Dyadic.toIGame_of_den_ne_one {x : Dyadic} (hx : x.den ≠ 1) : x.toIGame = {{x.lower.toIGame} | {x.upper.toIGame}}ᴵ

@[simp]

theorem Dyadic.toIGame_half : half.toIGame = ½

@[simp, irreducible]

theorem Dyadic.toIGame_neg (x : Dyadic) : (-x).toIGame = -x.toIGame

theorem Dyadic.toIGame_equiv_lower_upper (x : Dyadic) : x.toIGame ≈ {{x.lower.toIGame} | {x.upper.toIGame}}ᴵ

A dyadic number x is always equivalent to {lower x | upper x}ᴵ, though this may not necessarily be the canonical form.

@[irreducible]

instance IGame.Short.dyadic (x : Dyadic) : x.toIGame.Short

@[irreducible]

instance IGame.Numeric.dyadic (x : Dyadic) : x.toIGame.Numeric

noncomputable def Dyadic.toIGameEmbedding : Dyadic ↪o IGame

Dyadic.toIGame as an OrderEmbedding.

Equations

• Dyadic.toIGameEmbedding = OrderEmbedding.ofStrictMono Dyadic.toIGame Dyadic.toIGameEmbedding._proof_1

@[simp]

theorem Dyadic.toIGameEmbedding_apply (x : Dyadic) : toIGameEmbedding x = x.toIGame

@[simp]

theorem Dyadic.toIGame_le_toIGame {x y : Dyadic} : x.toIGame ≤ y.toIGame ↔ x ≤ y

@[simp]

theorem Dyadic.toIGame_lt_toIGame {x y : Dyadic} : x.toIGame < y.toIGame ↔ x < y

@[simp]

theorem Dyadic.toIGame_equiv_toIGame {x y : Dyadic} : x.toIGame ≈ y.toIGame ↔ x = y

@[simp]

theorem Dyadic.toIGame_inj {x y : Dyadic} : x.toIGame = y.toIGame ↔ x = y