feat: birthday of Dyadic.toIGame x

CombinatorialGames/Mathlib/Dyadic.lean

@@ -75,6 +75,25 @@ theorem den_mem_powers (x : Dyadic) : x.den ∈ Submonoid.powers 2 := by
   | case3 => exact one_mem _ -- integer
   | case2 => apply pow_mem; exact Submonoid.mem_powers 2 -- dyadic rational
 
+theorem den_eq_two_pow_toNat_precision (x : Dyadic) :
+    x.den = 2 ^ (x.precision.getD 0).toNat := by
+  cases x with
+  | zero => rfl
+  | ofOdd n k hn =>
+    cases k with
+    | ofNat k => rfl
+    | negSucc k => rfl
+
+theorem precision_eq_none {x : Dyadic} : x.precision = none ↔ x = 0 := by
+  cases x <;> simp
+
+theorem isSome_precision_eq_true {x : Dyadic} : x.precision.isSome = true ↔ x ≠ 0 :=
+  Option.isSome_iff_ne_none.trans Dyadic.precision_eq_none.not
+
+theorem isSome_precision_eq_true_of_den_ne_one {x : Dyadic} (hx : x.den ≠ 1) :
+    x.precision.isSome = true :=
+  x.isSome_precision_eq_true.mpr (mt (by rintro rfl; rfl) hx)
+
 @[simp]
 theorem den_le_one_iff_eq_one {x : Dyadic} : x.den ≤ 1 ↔ x.den = 1 := by
   simp_rw [Nat.le_one_iff_eq_zero_or_eq_one, x.den_ne_zero, false_or]

CombinatorialGames/Surreal/Birthday/Dyadic.lean

@@ -13,11 +13,22 @@ import CombinatorialGames.Surreal.Birthday.Cut
 /-!
 # Birthday of dyadic rationals
 
-We prove that a surreal number has a finite birthday iff it's a dyadic number.
+We prove that a surreal number has a finite birthday iff it's a dyadic number,
+and give an explicit formula for the birthday of a dyadic number.
 -/
 
 public section
 
+theorem Nat.div_lt_div_iff_exists {a b c : ℕ} : a / c < b / c ↔ ∃ d, a < d ∧ d ≤ b ∧ c ∣ d := by
+  constructor
+  · intro h
+    refine ⟨b - b % c, ?_, Nat.sub_le b _, Nat.dvd_sub_mod b⟩
+    have hc0 : c ≠ 0 := by rintro rfl; simp at h
+    rwa [← Nat.div_lt_div_right hc0 (Nat.dvd_sub_mod b), ← Nat.div_eq_sub_mod_div]
+  · intro ⟨d, ha, hb, hc⟩
+    grw [← hb]
+    exact Nat.div_lt_div_of_lt_of_dvd hc ha
+
 local notation "ω" => NatOrdinal.of Ordinal.omega0
 
 @[simp]
@@ -37,12 +48,170 @@ theorem Surreal.birthday_lt_omega0_iff {x : Surreal} :
   · rintro ⟨q, rfl⟩
     exact Surreal.birthday_dyadic_lt_omega0 q
 
+/-- The birthday of a dyadic number can be computed explicitly. -/
+@[expose]
+def Dyadic.birthday (x : Dyadic) : Nat :=
+  if h : x.den = 1 then x.num.natAbs else
+  (x.precision.get (isSome_precision_eq_true_of_den_ne_one h)).toNat + x.num.natAbs / x.den + 1
+
+@[simp]
+theorem Dyadic.birthday_intCast (n : Int) : Dyadic.birthday n = n.natAbs := by
+  unfold Dyadic.birthday
+  rw [dite_eq_left (Dyadic.den_intCast n), Dyadic.num_intCast]
+
+@[simp]
+theorem Dyadic.birthday_natCast (n : Nat) : Dyadic.birthday n = n := by
+  rw [← Int.cast_natCast, Dyadic.birthday_intCast, Int.natAbs_natCast]
+
+theorem Dyadic.birthday_of_den_eq_one {x : Dyadic} (hx : x.den = 1) :
+    x.birthday = x.num.natAbs :=
+  (congrArg birthday (intCast_num_eq_self_of_den_eq_one hx)).symm.trans
+    (birthday_intCast x.num)
+
+theorem Dyadic.birthday_of_den_ne_one {x : Dyadic} (hx : x.den ≠ 1) :
+    x.birthday =
+      (x.precision.get (isSome_precision_eq_true_of_den_ne_one hx)).toNat +
+        x.num.natAbs / x.den + 1 :=
+  dite_eq_right hx
+
+example : Dyadic.birthday ((13 : Dyadic) >>> 2) = 6 := rfl -- birthday 3.25 = 6
+example : Dyadic.birthday ((1 : Dyadic) >>> 1) = 2 := rfl  -- birthday 1/2 = 2
+example : Dyadic.birthday 7 = 7 := rfl                     -- birthday 7 = 7
+example : Dyadic.birthday ((-5 : Dyadic) >>> 1) = 4 := rfl -- birthday -2.5 = 4
+example : Dyadic.birthday ((1 : Dyadic) <<< 4) = 16 := rfl -- birthday 16 = 16
+
+theorem Dyadic.natAbs_num_div_den_lower_eq_natAbs_num_div_den {x : Dyadic}
+    (hxl : x.lower.den ≠ 1) : x.lower.num.natAbs / x.lower.den = x.num.natAbs / x.den := by
+  have hcd : x.num / x.den = x.toRat := x.toRat.num_div_den
+  have hd : x.den ≠ 1 := by
+    contrapose hxl
+    rw [x.lower_eq_of_den_eq_one hxl, ← Int.cast_one, ← Int.cast_sub, Dyadic.den_intCast]
+  have hle : x.lower.toRat = Int.cast (x.num - 1) / x.den := by
+    rw [x.coe_lower, ← hcd, ← one_div, ← sub_div, ← Rat.intCast_one, ← Int.cast_sub]
+  have hlnd : x.lower.num.natAbs / x.lower.den = (x.num - 1).natAbs / x.den := by
+    rw [Dyadic.num, Dyadic.den, x.coe_lower, ← hcd, ← one_div, ← sub_div,
+      ← Int.cast_one, ← Int.cast_sub, ← Rat.mkRat_eq_div, Rat.num_mkRat, Rat.den_mkRat,
+      ite_eq_right x.den_ne_zero, ite_eq_right x.den_ne_zero,
+      Int.natAbs_ediv_of_dvd (Int.natCast_dvd.2 (Nat.gcd_dvd_right _ _)),
+      Int.natAbs_natCast, ← Nat.mul_div_mul_right _ _ (Nat.gcd_pos_of_pos_left _ x.den_pos),
+      Nat.div_mul_cancel (Nat.gcd_dvd_left _ _), Nat.div_mul_cancel (Nat.gcd_dvd_right _ _)]
+  rw [hlnd]
+  apply le_antisymm
+  · rw [← not_lt, Nat.div_lt_div_iff_exists]
+    push Not
+    intro k hkl hkr
+    cases le_antisymm (Nat.add_one_le_of_lt hkl) (hkr.trans (Int.natAbs_sub_le _ 1))
+    rw [le_antisymm hkr (Int.natAbs_sub_le _ 1), ← Int.natCast_dvd]
+    contrapose! hxl
+    obtain ⟨e, he⟩ := hxl
+    rw [he, Int.cast_mul, Int.cast_natCast, mul_div_cancel_left₀ _ (by positivity)] at hle
+    rw [Dyadic.den, hle, Rat.den_intCast]
+  · rw [← not_lt, Nat.div_lt_div_iff_exists]
+    push Not
+    intro k hkl hkr
+    rw [← Int.sub_add_cancel x.num 1] at hkr
+    cases le_antisymm (Nat.add_one_le_of_lt hkl) (hkr.trans (Int.natAbs_add_le _ 1))
+    rw [le_antisymm hkr (Int.natAbs_add_le _ 1), Int.sub_add_cancel, ← Int.natCast_dvd]
+    contrapose! hd
+    obtain ⟨e, he⟩ := hd
+    rw [he, Int.cast_mul, Int.cast_natCast, mul_div_cancel_left₀ _ (by positivity)] at hcd
+    rw [Dyadic.den, ← hcd, Rat.den_intCast]
+
+theorem Dyadic.natAbs_num_div_den_upper_eq_natAbs_num_div_den {x : Dyadic}
+    (hxl : x.upper.den ≠ 1) : x.upper.num.natAbs / x.upper.den = x.num.natAbs / x.den := by
+  rw [← den_neg] at hxl
+  rw [← Int.natAbs_neg x.upper.num, ← Int.natAbs_neg x.num, ← den_neg x.upper, ← den_neg x,
+    ← num_neg x.upper, ← num_neg x]
+  rw [← lower_neg] at hxl ⊢
+  exact Dyadic.natAbs_num_div_den_lower_eq_natAbs_num_div_den hxl
+
+theorem Dyadic.max_birthday_lower_birthday_upper_add_one_of_den_ne_one {x : Dyadic}
+    (hx : x.den ≠ 1) : max x.lower.birthday x.upper.birthday + 1 = x.birthday := by
+  have hcd : x.num / x.den = x.toRat := x.toRat.num_div_den
+  have hnd := x.max_den_lower_upper hx
+  have hnd0 : (x.precision.getD 0).toNat ≠ 0 := by
+    apply_fun (2 ^ ·)
+    rwa [← Dyadic.den_eq_two_pow_toNat_precision]
+  simp_rw [Dyadic.den_eq_two_pow_toNat_precision] at hnd
+  rw [← (pow_right_monotone one_le_two).map_max,
+    ← Nat.pow_sub_one two_ne_zero hnd0, pow_right_inj₀ Nat.two_pos (by decide),
+    eq_comm, Nat.sub_eq_iff_eq_add (Nat.one_le_iff_ne_zero.2 hnd0)] at hnd
+  rw [birthday_of_den_ne_one hx, Option.get_eq_getD, hnd, Nat.add_one_inj, Nat.add_right_comm]
+  have hk (c : ℤ) (d : ℕ) : (Rat.num (c / d)).natAbs / Rat.den (c / d) = c.natAbs / d := by
+    obtain hd0 | hd0 := eq_zero_or_pos d
+    · simp [hd0]
+    · rw [← Rat.mkRat_eq_div, Rat.num_mkRat, Rat.den_mkRat,
+        ite_eq_right hd0.ne', ite_eq_right hd0.ne',
+        Int.natAbs_ediv_of_dvd (Int.natCast_dvd.2 (Nat.gcd_dvd_right _ _)),
+        Int.natAbs_natCast, ← Nat.mul_div_mul_right _ _ (Nat.gcd_pos_of_pos_left c.natAbs hd0),
+        Nat.div_mul_cancel (Nat.gcd_dvd_left _ _), Nat.div_mul_cancel (Nat.gcd_dvd_right _ _)]
+  have hle : x.lower.toRat = Int.cast (x.num - 1) / x.den := by
+    rw [x.coe_lower, ← hcd, ← one_div, ← sub_div, ← Rat.intCast_one, ← Int.cast_sub]
+  have hue : x.upper.toRat = Int.cast (x.num + 1) / x.den := by
+    rw [x.coe_upper, ← hcd, ← one_div, ← add_div, ← Rat.intCast_one, ← Int.cast_add]
+  have hlnd (hl : x.lower.den = 1) : x.lower.num.natAbs = (x.num - 1).natAbs / x.den := by
+    have hlnd := congr((x.lower.num / $hl : ℚ))
+    rw [Nat.cast_one, div_one, ← Int.cast_natCast, ← Rat.intCast_div _ _ (by simp [hl]),
+      Int.cast_inj] at hlnd
+    rw [← hlnd, Int.natAbs_ediv_of_dvd (by simp [hl]), Int.natAbs_natCast,
+      Dyadic.num, Dyadic.den, hle, hk]
+  have hund (hr : x.upper.den = 1) : x.upper.num.natAbs = (x.num + 1).natAbs / x.den := by
+    have hund := congr((x.upper.num / $hr : Rat))
+    rw [Nat.cast_one, div_one, ← Int.cast_natCast, ← Rat.intCast_div _ _ (by simp [hr]),
+      Int.cast_inj] at hund
+    rw [← hund, Int.natAbs_ediv_of_dvd (by simp [hr]), Int.natAbs_natCast,
+      Dyadic.num, Dyadic.den, hue, hk]
+  by_cases hl : x.lower.den = 1 <;> by_cases hr : x.upper.den = 1
+  · rw [birthday_of_den_eq_one hl, birthday_of_den_eq_one hr]
+    rw [Dyadic.den_eq_two_pow_toNat_precision, Nat.pow_eq_one, or_iff_right (by decide)] at hl hr
+    rw [hl, hr, max_self, zero_add, ← Nat.pow_right_inj Nat.one_lt_two, Nat.pow_one,
+      ← Dyadic.den_eq_two_pow_toNat_precision] at hnd
+    rw [hnd, hl, hr, max_self, zero_add]
+    obtain ⟨c, hc⟩ := x.odd_num hx
+    unfold Dyadic.num
+    rw [hle, hue, hnd, hc, Int.add_sub_cancel, Int.add_assoc, ← two_mul, ← Int.mul_add,
+      Rat.intCast_mul, Rat.intCast_mul, Rat.intCast_ofNat, Rat.natCast_ofNat,
+      mul_div_cancel_left₀ _ two_ne_zero, mul_div_cancel_left₀ _ two_ne_zero,
+      Rat.num_intCast, Rat.num_intCast]
+    lia
+  · rw [birthday_of_den_eq_one hl, birthday_of_den_ne_one hr,
+      Dyadic.natAbs_num_div_den_upper_eq_natAbs_num_div_den hr, hlnd hl]
+    rw [Dyadic.den_eq_two_pow_toNat_precision, Nat.pow_eq_one, or_iff_right (by decide)] at hl
+    rw [hl, zero_max] at hnd ⊢
+    rw [Option.get_eq_getD, max_eq_right_iff, Nat.add_assoc]
+    apply le_add_of_le_right
+    grw [Int.natAbs_sub_le]
+    rw [Int.natAbs_one, Nat.succ_div, Nat.add_le_add_iff_left]
+    apply ite_le_sup
+  · rw [birthday_of_den_ne_one hl, birthday_of_den_eq_one hr,
+      Dyadic.natAbs_num_div_den_lower_eq_natAbs_num_div_den hl, hund hr]
+    rw [Dyadic.den_eq_two_pow_toNat_precision, Nat.pow_eq_one, or_iff_right (by decide)] at hr
+    rw [hr, max_zero] at hnd ⊢
+    rw [Option.get_eq_getD, max_eq_left_iff, Nat.add_assoc]
+    apply le_add_of_le_right
+    grw [Int.natAbs_add_le]
+    rw [Int.natAbs_one, Nat.succ_div, Nat.add_le_add_iff_left]
+    apply ite_le_sup
+  · rw [birthday_of_den_ne_one hl, birthday_of_den_ne_one hr,
+      Dyadic.natAbs_num_div_den_lower_eq_natAbs_num_div_den hl,
+      Dyadic.natAbs_num_div_den_upper_eq_natAbs_num_div_den hr,
+      Nat.add_max_add_right, Nat.add_max_add_right, Option.get_eq_getD, Option.get_eq_getD]
+
+@[simp]
+theorem IGame.birthday_dyadic (x : Dyadic) : IGame.birthday x = x.birthday := by
+  induction hd : x.den using Nat.strongRec generalizing x with | ind d ih
+  subst hd
+  obtain hd | hd := eq_or_ne x.den 1
+  · rw [Dyadic.birthday_of_den_eq_one hd, Dyadic.toIGame_of_den_eq_one hd, IGame.birthday_intCast]
+  · rw [Dyadic.toIGame_of_den_ne_one hd, birthday_ofSets]
+    simp_rw [Set.image_singleton, csSup_singleton, Function.comp_apply]
+    rw [ih _ (x.den_lower_lt hd) _ rfl, ih _ (x.den_upper_lt hd) _ rfl,
+      Order.succ_eq_add_one, Order.succ_eq_add_one, ← Nat.cast_add_one, ← Nat.cast_add_one,
+      ← Nat.cast_max, Nat.cast_inj, Nat.add_max_add_right,
+      Dyadic.max_birthday_lower_birthday_upper_add_one_of_den_ne_one hd]
+
 -- `Dyadic.toIGame` is canonical, so it minimizes the birthday in its equivalence class.
 proof_wanted Surreal.birthday_dyadic (x : Dyadic) :
-    Surreal.birthday x = IGame.birthday x
-
--- It's actually possible to explicitly compute the birthday of a dyadic number.
-proof_wanted IGame.birthday_dyadic (x : Dyadic) :
-    IGame.birthday x = ⌈x.num.natAbs⌉₊ + Nat.log2 x.den
+    Surreal.birthday x = x.birthday
 
 end

CombinatorialGames/Surreal/Dyadic.lean

@@ -10,6 +10,7 @@ public import CombinatorialGames.Mathlib.Dyadic
 public import CombinatorialGames.Surreal.Division
 
 import Mathlib.Data.Finset.DenselyOrdered
+import Mathlib.Data.Nat.Prime.Basic
 
 /-!
 # Dyadic games
@@ -129,6 +130,44 @@ theorem le_upper_add_of_den_ge {x y : Dyadic} (h : y.den ≤ x.den) :
     upper x + y ≤ upper (x + y) := by
   simpa [add_comm] using le_upper_add_of_den_le h
 
+theorem max_den_lower_upper {x : Dyadic} (hx : x.den ≠ 1) :
+    max x.lower.den x.upper.den = x.den / 2 := by
+  unfold Dyadic.den at hx ⊢
+  rw [coe_lower, coe_upper]
+  unfold Dyadic.den
+  rw [Rat.sub_def', Rat.den_mkRat, ite_eq_right (by positivity),
+    Rat.add_def', Rat.den_mkRat, ite_eq_right (by positivity),
+    Rat.den_inv_of_ne_zero (by positivity), Rat.num_inv, Rat.num_natCast,
+    Int.natAbs_natCast, Rat.den_natCast, Int.sign_natCast_of_ne_zero x.den_ne_zero,
+    Nat.cast_one, Int.one_mul, ← Int.sub_mul, ← Int.add_mul,
+    Int.natAbs_mul, Int.natAbs_mul, Int.natAbs_natCast,
+    Nat.gcd_mul_right, Nat.mul_div_mul_right _ _ x.den_pos,
+    Nat.gcd_mul_right, Nat.mul_div_mul_right _ _ x.den_pos]
+  generalize hn : x.toRat.num = n, hd : x.toRat.den = d
+  obtain ⟨e, rfl⟩ : ∃ e, 2 ^ e = d := by
+    rw [← hd, ← Submonoid.mem_powers_iff]
+    exact x.den_mem_powers
+  cases e with
+  | zero => exact (hx hd).elim
+  | succ e =>
+    have ⟨l2, hl2⟩ : Even (n - 1).natAbs := by simpa [hn] using x.odd_num hx
+    have ⟨u2, hu2⟩ : Even (n + 1).natAbs := by simpa [hn] using x.odd_num hx
+    rw [pow_succ, Nat.mul_div_cancel _ two_pos, hl2, hu2,
+      ← Nat.mul_two, ← Nat.mul_two, Nat.gcd_mul_right, Nat.gcd_mul_right,
+      Nat.mul_div_mul_right _ _ two_pos, Nat.mul_div_mul_right _ _ two_pos]
+    refine le_antisymm (max_le (Nat.div_le_self _ _) (Nat.div_le_self _ _)) ?_
+    suffices h : Nat.gcd 2 l2 = 1 ∨ Nat.gcd 2 u2 = 1 by
+      obtain h | h := h
+      · rw [Nat.gcd_pow_left_of_gcd_eq_one h, Nat.div_one]
+        exact Nat.le_max_left _ _
+      · rw [Nat.gcd_pow_left_of_gcd_eq_one h, Nat.div_one]
+        exact Nat.le_max_right _ _
+    rw [← Nat.coprime_iff_gcd_eq_one, ← Nat.coprime_iff_gcd_eq_one,
+      Nat.coprime_two_left, Nat.coprime_two_left,
+      ← Nat.not_even_iff_odd, ← Nat.not_even_iff_odd, ← not_and_or]
+    rintro ⟨⟨l4, rfl⟩, ⟨u4, rfl⟩⟩
+    lia
+
 /-! ### Dyadic numbers to games -/
 
 /-- Converts a dyadic rational into an `IGame`. This map is defined so that: