Unfolding `of` and `val` from Nimbers in the CGT repo

Stream: Is there code for X?

[SaNoy SaKnoi]

I'm not quite sure how to handle the of and val aliases used in nimbers. It seems we have to use dance around them usingforall_moves_nim_ofNat and mem_moves_nim_of_lt, but I can't seem to avoid it when proving equality of games.

import CombinatorialGames.Game.Specific.Nim

open Nimber IGame

-- prove equivalence, ok
example : !{ {0, ⋆} | {0, ⋆} } ≈ nim (∗2) := by
  game_cmp

-- prove equality
example : !{ {0, ⋆} | {0, ⋆} } = nim (∗2) := by
  ext (_ | _) g
  all_goals
    constructor
    intro h
    simp at h
    rcases h with (rfl | rfl)
    rw [← nim_zero]
    simp
    use 0
    simp
    sorry -- 0 < of 2
    rw [← nim_one]
    simp
    use 1
    simp
    sorry -- 1 < of 2
    revert g
    rw [forall_moves_nim_ofNat]
    intro m h
    match m with
    | 0 => simp
    | 1 => simp
    | x + 2 => simp at h

[Aaron Liu]

Does game_cmp not help you here too

[Aaron Liu]

@Violeta Hernández

[Violeta Hernández]

#combinatorial-games might be a more appropriate channel for this

[Violeta Hernández]

As for your question, you should be able to do something like this. nim 2 has Iio (of 2) as its left/right moves, which is equal to of '' Iio 2, which is equal to of '' natCast '' Iio 2. And then hopefully Mathlib has some easy way to show Iio 2 = {0, 1} on the naturals. simp should take care of the rest.

[Violeta Hernández]

Or if you simply want to solve your subgoals, you can turn 0 < of 2 into of 0 < of 2 and then 0 < 2 in the ordinals, which hopefully simp should be able to solve.

[Violeta Hernández]

Here's a proof of your theorem:

import CombinatorialGames.Game.Specific.Nim

open Nimber IGame

example : !{ {0, ⋆} | {0, ⋆} } = nim (∗2) := by
  rw [← ofSets_eq_ofSets_cases (fun _ ↦ {0, ⋆}) ⟨⟩, nim_def]
  congr!
  have : Set.Iio (2 : Ordinal) = {0, 1} := by
    rw [← Ordinal.succ_one, Order.Iio_succ]
    aesop (add simp [Ordinal.le_one_iff])
  rw [← of_image_Iio, this]
  simp [Set.image_pair]

[SaNoy SaKnoi]

Thanks! It seems I can also use change to turn of n into (n : Ordinal) as well.

[Violeta Hernández]

You can, but you really shouldn't. of and val exist as an API barrier.

[Violeta Hernández]

It's an analogous situation with docs#OrderDual.