feat(set_theory/game): computation of grundy_value (nim n + nim m) (#…

…3977)

src/data/nat/bitwise.lean

@@ -149,4 +149,34 @@ by { rw [lxor_comm n m, lxor_comm n' m] at h, exact lxor_right_inj h }
 lemma lxor_eq_zero {n m : ℕ} : lxor n m = 0 ↔ n = m :=
 ⟨by { rw ←lxor_self m, exact lxor_left_inj  }, by { rintro rfl, exact lxor_self _ }⟩
 
+lemma lxor_trichotomy {a b c : ℕ} (h : lxor a (lxor b c) ≠ 0) :
+  lxor b c < a ∨ lxor a c < b ∨ lxor a b < c :=
+begin
+  set v := lxor a (lxor b c) with hv,
+
+  -- The xor of any two of `a`, `b`, `c` is the xor of `v` and the third.
+  have hab : lxor a b = lxor c v,
+  { rw hv, conv_rhs { rw lxor_comm, simp [lxor_assoc] } },
+  have hac : lxor a c = lxor b v,
+  { rw hv,
+    conv_rhs { congr, skip, rw lxor_comm },
+    rw [←lxor_assoc, ←lxor_assoc, lxor_self, zero_lxor, lxor_comm] },
+  have hbc : lxor b c = lxor a v,
+  { simp [hv, ←lxor_assoc] },
+
+  -- If `i` is the position of the most significant bit of `v`, then at least one of `a`, `b`, `c`
+  -- has a one bit at position `i`.
+  obtain ⟨i, ⟨hi, hi'⟩⟩ := exists_most_significant_bit h,
+  have : test_bit a i = tt ∨ test_bit b i = tt ∨ test_bit c i = tt,
+  { contrapose! hi,
+    simp only [eq_ff_eq_not_eq_tt, ne, test_bit_lxor] at ⊢ hi,
+    rw [hi.1, hi.2.1, hi.2.2, bxor_ff, bxor_ff] },
+
+  -- If, say, `a` has a one bit at position `i`, then `a xor v` has a zero bit at position `i`, but
+  -- the same bits as `a` in positions greater than `j`, so `a xor v < a`.
+  rcases this with h|h|h;
+  [{ left, rw hbc }, { right, left, rw hac }, { right, right, rw hab }];
+  exact lt_of_test_bit i (by simp [h, hi]) h (λ j hj, by simp [hi' _ hj])
+end
+
 end nat

src/set_theory/game/nim.lean

@@ -1,33 +1,37 @@
 /-
 Copyright (c) 2020 Fox Thomson. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Fox Thomson
+Authors: Fox Thomson, Markus Himmel
 -/
+import data.nat.bitwise
 import set_theory.game.impartial
-import set_theory.ordinal
-import data.set
-import logic.basic
-
-universes u v
+import set_theory.ordinal_arithmetic
 
 /-!
 # Nim and the Sprague-Grundy theorem
 
 This file contains the definition for nim for any ordinal `O`. In the game of `nim O₁` both players
 may move to `nim O₂` for any `O₂ < O₁`.
 We also define a Grundy value for an impartial game `G` and prove the Sprague-Grundy theorem, that
-`G` is equivalent to `nim (Grundy_value G)`.
+`G` is equivalent to `nim (grundy_value G)`.
+Finally, we compute the sum of finite Grundy numbers: if `G` and `H` have Grundy values `n` and `m`,
+where `n` and `m` are natural numbers, then `G + H` has the Grundy value `n xor m`.
 
 ## Implementation details
 
-The pen-and-paper definition of nim defines the possible moves of `nim O` to be `{ O' | O' < O}`.
+The pen-and-paper definition of nim defines the possible moves of `nim O` to be `{O' | O' < O}`.
 However, this definition does not work for us because it would make the type of nim
 `ordinal.{u} → pgame.{u + 1}`, which would make it impossible for us to state the Sprague-Grundy
 theorem, since that requires the type of `nim` to be `ordinal.{u} → pgame.{u}`. For this reason, we
 instead use `O.out.α` for the possible moves, which makes proofs significantly more messy and
 tedious, but avoids the universe bump.
 
+The lemma `nim_def` is somewhat prone to produce "motive is not type correct" errors. If you run
+into this problem, you may find the lemmas `exists_ordinal_move_left_eq` and `exists_move_left_eq`
+useful.
+
 -/
+universes u
 
 /-- `ordinal.out` and `ordinal.type_out'` are required to make the definition of nim computable.
  `ordinal.out` performs the same job as `quotient.out` but is specific to ordinals. -/
@@ -98,6 +102,12 @@ begin
 end
 using_well_founded { dec_tac := tactic.assumption }
 
+lemma exists_ordinal_move_left_eq (O : ordinal) : ∀ i, ∃ O' < O, (nim O).move_left i = nim O' :=
+by { rw nim_def, exact λ i, ⟨ordinal.typein O.out.r i, ⟨nim_wf_lemma _, rfl⟩⟩ }
+
+lemma exists_move_left_eq (O : ordinal) : ∀ O' < O, ∃ i, (nim O).move_left i = nim O' :=
+by { rw nim_def, exact λ _ h, ⟨(ordinal.principal_seg_out h).top, by simp⟩ }
+
 lemma zero_first_loses : (nim (0 : ordinal)).first_loses :=
 begin
   rw [impartial.first_loses_symm, nim_def, le_def_lt],
@@ -240,12 +250,105 @@ begin
 end
 using_well_founded { dec_tac := pgame_wf_tac }
 
-lemma equiv_nim_iff_grundy_value_eq {G : pgame.{u}} (hG : impartial G) (O : ordinal) :
+lemma equiv_nim_iff_grundy_value_eq (G : pgame) [G.impartial] (O : ordinal) :
   G ≈ nim O ↔ grundy_value G = O :=
 ⟨by { intro h, rw ←nim.equiv_iff_eq, exact equiv_trans (equiv_symm (equiv_nim_grundy_value G)) h },
  by { rintro rfl, exact equiv_nim_grundy_value G }⟩
 
 lemma nim.grundy_value (O : ordinal.{u}) : grundy_value (nim O) = O :=
 by rw ←equiv_nim_iff_grundy_value_eq
 
+lemma equiv_iff_grundy_value_eq (G H : pgame) [G.impartial] [H.impartial] :
+  G ≈ H ↔ grundy_value G = grundy_value H :=
+(equiv_congr_left.1 (equiv_nim_grundy_value H) _).trans $ equiv_nim_iff_grundy_value_eq _ _
+
+lemma grundy_value_zero : grundy_value 0 = 0 :=
+by rw [(equiv_iff_grundy_value_eq 0 (nim 0)).1 (equiv_symm nim.zero_first_loses), nim.grundy_value]
+
+lemma equiv_zero_iff_grundy_value (G : pgame) [G.impartial] : G ≈ 0 ↔ grundy_value G = 0 :=
+by rw [equiv_iff_grundy_value_eq, grundy_value_zero]
+
+lemma grundy_value_nim_add_nim (n m : ℕ) : grundy_value (nim n + nim m) = nat.lxor n m :=
+begin
+  induction n using nat.strong_induction_on with n hn generalizing m,
+  induction m using nat.strong_induction_on with m hm,
+  rw [grundy_value_def],
+
+  -- We want to show that `n xor m` is the smallest unreachable Grundy value. We will do this in two
+  -- steps:
+  -- h₀: `n xor m` is not a reachable grundy number.
+  -- h₁: every Grundy number strictly smaller than `n xor m` is reachable.
+
+  have h₀ : (nat.lxor n m : ordinal) ∈ nonmoves (λ i, grundy_value ((nim n + nim m).move_left i)),
+  { -- To show that `n xor m` is unreachable, we show that every move produces a Grundy number
+    -- different from `n xor m`.
+    simp only [nonmoves, not_exists, set.mem_set_of_eq],
+    equiv_rw left_moves_add _ _,
+
+    -- The move operates either on the left pile or on the right pile.
+    rintro (a|a),
+
+    all_goals
+    { -- One of the piles is reduced to `k` stones, with `k < n` or `k < m`.
+      obtain ⟨ok, ⟨hk, hk'⟩⟩ := nim.exists_ordinal_move_left_eq _ a,
+      obtain ⟨k, rfl⟩ := ordinal.lt_omega.1 (lt_trans hk (ordinal.nat_lt_omega _)),
+      replace hk := ordinal.nat_cast_lt.1 hk,
+
+      -- Thus, the problem is reduced to computing the Grundy value of `nim n + nim k` or
+      -- `nim k + nim m`, both of which can be dealt with using an inductive hypothesis.
+      simp only [hk', add_move_left_inl, add_move_left_inr, id],
+      rw hn _ hk <|> rw hm _ hk,
+
+      -- But of course xor is injective, so if we change one of the arguments, we will not get the
+      -- same value again.
+      intro h,
+      rw ordinal.nat_cast_inj at h,
+      try { rw [nat.lxor_comm n k, nat.lxor_comm n m] at h },
+      exact _root_.ne_of_lt hk (nat.lxor_left_inj h) } },
+
+  have h₁ : ∀ (u : ordinal), u < nat.lxor n m →
+    u ∉ nonmoves (λ i, grundy_value ((nim n + nim m).move_left i)),
+  { -- Take any natural number `u` less than `n xor m`.
+    intros ou hu,
+    obtain ⟨u, rfl⟩ := ordinal.lt_omega.1 (lt_trans hu (ordinal.nat_lt_omega _)),
+    replace hu := ordinal.nat_cast_lt.1 hu,
+
+    -- Our goal is to produce a move that gives the Grundy value `u`.
+    simp only [nonmoves, not_exists, not_not, set.mem_set_of_eq, not_forall],
+
+    -- By a lemma about xor, either `u xor m < n` or `u xor n < m`.
+    have : nat.lxor u (nat.lxor n m) ≠ 0,
+    { intro h, rw nat.lxor_eq_zero at h, linarith },
+    rcases nat.lxor_trichotomy this with h|h|h,
+    { linarith },
+
+    -- Therefore, we can play the corresponding move, and by the inductive hypothesis the new state
+    -- is `(u xor m) xor m = u` or `n xor (u xor n) = u` as required.
+    { obtain ⟨i, hi⟩ := nim.exists_move_left_eq _ _ (ordinal.nat_cast_lt.2 h),
+      refine ⟨(left_moves_add _ _).symm (sum.inl i), _⟩,
+      simp only [hi, add_move_left_inl],
+      rw [hn _ h, nat.lxor_assoc, nat.lxor_self, nat.lxor_zero] },
+    { obtain ⟨i, hi⟩ := nim.exists_move_left_eq _ _ (ordinal.nat_cast_lt.2 h),
+      refine ⟨(left_moves_add _ _).symm (sum.inr i), _⟩,
+      simp only [hi, add_move_left_inr],
+      rw [hm _ h, nat.lxor_comm, nat.lxor_assoc, nat.lxor_self, nat.lxor_zero] } },
+
+  -- We are done!
+  apply le_antisymm (ordinal.omin_le h₀),
+  contrapose! h₁,
+  exact ⟨_, ⟨h₁, ordinal.omin_mem _ _⟩⟩
+end
+
+lemma nim_add_nim_equiv {n m : ℕ} : nim n + nim m ≈ nim (nat.lxor n m) :=
+by rw [equiv_nim_iff_grundy_value_eq, grundy_value_nim_add_nim]
+
+lemma grundy_value_add (G H : pgame) [G.impartial] [H.impartial] {n m : ℕ} (hG : grundy_value G = n)
+  (hH : grundy_value H = m) : grundy_value (G + H) = nat.lxor n m :=
+begin
+  rw [←nim.grundy_value (nat.lxor n m), ←equiv_iff_grundy_value_eq],
+  refine equiv_trans _ nim_add_nim_equiv,
+  convert add_congr (equiv_nim_grundy_value G) (equiv_nim_grundy_value H);
+  simp only [hG, hH]
+end
+
 end pgame

src/set_theory/pgame.lean

@@ -428,6 +428,14 @@ theorem le_congr {x₁ y₁ x₂ y₂} : x₁ ≈ x₂ → y₁ ≈ y₂ → (x
 theorem lt_congr {x₁ y₁ x₂ y₂} (hx : x₁ ≈ x₂) (hy : y₁ ≈ y₂) : x₁ < y₁ ↔ x₂ < y₂ :=
 not_le.symm.trans $ (not_congr (le_congr hy hx)).trans not_le
 
+theorem equiv_congr_left {y₁ y₂} : y₁ ≈ y₂ ↔ ∀ x₁, x₁ ≈ y₁ ↔ x₁ ≈ y₂ :=
+⟨λ h x₁, ⟨λ h', equiv_trans h' h, λ h', equiv_trans h' (equiv_symm h)⟩,
+ λ h, (h y₁).1 $ equiv_refl _⟩
+
+theorem equiv_congr_right {x₁ x₂} : x₁ ≈ x₂ ↔ ∀ y₁, x₁ ≈ y₁ ↔ x₂ ≈ y₁ :=
+⟨λ h y₁, ⟨λ h', equiv_trans (equiv_symm h) h', λ h', equiv_trans h h'⟩,
+ λ h, (h x₂).2 $ equiv_refl _⟩
+
 /-- `restricted x y` says that Left always has no more moves in `x` than in `y`,
      and Right always has no more moves in `y` than in `x` -/
 inductive restricted : pgame.{u} → pgame.{u} → Type (u+1)