From 997fa572f1b3fba1536f43e6747341d19ec7a78c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Violeta=20Hern=C3=A1ndez?= Date: Wed, 3 Aug 2022 06:38:53 +0000 Subject: [PATCH] refactor(set_theory/game/nim): remove `nim` namespace (#15366) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit A lot of theorems that already had `nim` in the name were also in the `pgame.nim` namespace. We remove the `nim` namespace entirely, and rename the few theorems that didn't have `nim` in the name: - `non_zero_first_wins` → `nim_fuzzy_zero_of_ne_zero` - `add_equiv_zero_iff_eq` → `nim_add_equiv_zero_iff` - `add_fuzzy_zero_iff_ne` → `nim_add_fuzzy_zero_iff` - `equiv_iff_eq` → `nim_equiv_iff_eq` - `grundy_value` → `nim_grundy_value` Further, we move `nim` itself into the `pgame` namespace. --- src/set_theory/game/nim.lean | 47 +++++++++++++++--------------------- 1 file changed, 20 insertions(+), 27 deletions(-) diff --git a/src/set_theory/game/nim.lean b/src/set_theory/game/nim.lean index 58935edcf070d..5324f471fe80b 100644 --- a/src/set_theory/game/nim.lean +++ b/src/set_theory/game/nim.lean @@ -32,6 +32,10 @@ noncomputable theory universe u +open_locale pgame + +namespace pgame + /-- The definition of single-heap nim, which can be viewed as a pile of stones where each player can take a positive number of stones from it on their turn. -/ -- Uses `noncomputable!` to avoid `rec_fn_macro only allowed in meta definitions` VM error @@ -43,15 +47,6 @@ noncomputable! def nim : ordinal.{u} → pgame.{u} in ⟨o₁.out.α, o₁.out.α, f, f⟩ using_well_founded { dec_tac := tactic.assumption } -namespace pgame - -local infix ` ⧏ `:50 := lf -local infix ` ≈ ` := equiv -local infix ` ∥ `:50 := fuzzy -local infix ` ≡r `:50 := relabelling - -namespace nim - open ordinal lemma nim_def (o : ordinal) : nim o = pgame.mk o.out.α o.out.α @@ -161,14 +156,14 @@ lemma exists_ordinal_move_left_eq {o : ordinal} (i) : ∃ o' < o, (nim o).move_l lemma exists_move_left_eq {o o' : ordinal} (h : o' < o) : ∃ i, (nim o).move_left i = nim o' := ⟨to_left_moves_nim ⟨o', h⟩, by simp⟩ -lemma non_zero_first_wins {o : ordinal} (ho : o ≠ 0) : nim o ∥ 0 := +lemma nim_fuzzy_zero_of_ne_zero {o : ordinal} (ho : o ≠ 0) : nim o ∥ 0 := begin rw [impartial.fuzzy_zero_iff_lf, nim_def, lf_zero_le], rw ←ordinal.pos_iff_ne_zero at ho, exact ⟨(ordinal.principal_seg_out ho).top, by simp⟩ end -@[simp] lemma add_equiv_zero_iff_eq (o₁ o₂ : ordinal) : nim o₁ + nim o₂ ≈ 0 ↔ o₁ = o₂ := +@[simp] lemma nim_add_equiv_zero_iff (o₁ o₂ : ordinal) : nim o₁ + nim o₂ ≈ 0 ↔ o₁ = o₂ := begin split, { contrapose, @@ -186,13 +181,11 @@ begin exact impartial.add_self (nim o₁) } end -@[simp] lemma add_fuzzy_zero_iff_ne (o₁ o₂ : ordinal) : nim o₁ + nim o₂ ∥ 0 ↔ o₁ ≠ o₂ := -by rw [iff_not_comm, impartial.not_fuzzy_zero_iff, add_equiv_zero_iff_eq] - -@[simp] lemma equiv_iff_eq (o₁ o₂ : ordinal) : nim o₁ ≈ nim o₂ ↔ o₁ = o₂ := -by rw [impartial.equiv_iff_add_equiv_zero, add_equiv_zero_iff_eq] +@[simp] lemma nim_add_fuzzy_zero_iff {o₁ o₂ : ordinal} : nim o₁ + nim o₂ ∥ 0 ↔ o₁ ≠ o₂ := +by rw [iff_not_comm, impartial.not_fuzzy_zero_iff, nim_add_equiv_zero_iff] -end nim +@[simp] lemma nim_equiv_iff_eq {o₁ o₂ : ordinal} : nim o₁ ≈ nim o₂ ↔ o₁ = o₂ := +by rw [impartial.equiv_iff_add_equiv_zero, nim_add_equiv_zero_iff] /-- The Grundy value of an impartial game, the ordinal which corresponds to the game of nim that the game is equivalent to -/ @@ -216,7 +209,7 @@ begin { intro i₁, rw add_move_left_inl, apply (fuzzy_congr_left (add_congr_left (equiv_nim_grundy_value (G.move_left i₁)).symm)).1, - rw nim.add_fuzzy_zero_iff_ne, + rw nim_add_fuzzy_zero_iff, intro heq, rw [eq_comm, grundy_value_def G] at heq, have h := ordinal.ne_mex _, @@ -225,7 +218,7 @@ begin { intro i₂, rw [add_move_left_inr, ←impartial.exists_left_move_equiv_iff_fuzzy_zero], revert i₂, - rw nim.nim_def, + rw nim_def, intro i₂, have h' : ∃ i : G.left_moves, (grundy_value (G.move_left i)) = @@ -247,9 +240,9 @@ using_well_founded { dec_tac := pgame_wf_tac } lemma grundy_value_eq_iff_equiv_nim {G : pgame} [G.impartial] {o : ordinal} : grundy_value G = o ↔ G ≈ nim o := ⟨by { rintro rfl, exact equiv_nim_grundy_value G }, - by { intro h, rw ←nim.equiv_iff_eq, exact (equiv_nim_grundy_value G).symm.trans h }⟩ + by { intro h, rw ←nim_equiv_iff_eq, exact (equiv_nim_grundy_value G).symm.trans h }⟩ -@[simp] lemma nim.grundy_value (o : ordinal.{u}) : grundy_value (nim o) = o := +@[simp] lemma nim_grundy_value (o : ordinal.{u}) : grundy_value (nim o) = o := grundy_value_eq_iff_equiv_nim.2 pgame.equiv_rfl lemma grundy_value_eq_iff_equiv (G H : pgame) [G.impartial] [H.impartial] : @@ -257,13 +250,13 @@ lemma grundy_value_eq_iff_equiv (G H : pgame) [G.impartial] [H.impartial] : grundy_value_eq_iff_equiv_nim.trans (equiv_congr_left.1 (equiv_nim_grundy_value H) _).symm @[simp] lemma grundy_value_zero : grundy_value 0 = 0 := -grundy_value_eq_iff_equiv_nim.2 nim.nim_zero_equiv.symm +grundy_value_eq_iff_equiv_nim.2 nim_zero_equiv.symm lemma grundy_value_iff_equiv_zero (G : pgame) [G.impartial] : grundy_value G = 0 ↔ G ≈ 0 := by rw [←grundy_value_eq_iff_equiv, grundy_value_zero] @[simp] lemma grundy_value_star : grundy_value star = 1 := -grundy_value_eq_iff_equiv_nim.2 nim.nim_one_equiv.symm +grundy_value_eq_iff_equiv_nim.2 nim_one_equiv.symm @[simp] lemma grundy_value_nim_add_nim (n m : ℕ) : grundy_value (nim.{u} n + nim.{u} m) = nat.lxor n m := @@ -288,7 +281,7 @@ begin all_goals { -- One of the piles is reduced to `k` stones, with `k < n` or `k < m`. intro a, - obtain ⟨ok, hk, hk'⟩ := nim.exists_ordinal_move_left_eq a, + obtain ⟨ok, hk, hk'⟩ := 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, @@ -319,11 +312,11 @@ begin -- 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), + { obtain ⟨i, hi⟩ := exists_move_left_eq (ordinal.nat_cast_lt.2 h), refine ⟨to_left_moves_add (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), + { obtain ⟨i, hi⟩ := exists_move_left_eq (ordinal.nat_cast_lt.2 h), refine ⟨to_left_moves_add (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] } }, @@ -340,7 +333,7 @@ by rw [←grundy_value_eq_iff_equiv_nim, 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), grundy_value_eq_iff_equiv], + rw [←nim_grundy_value (nat.lxor n m), grundy_value_eq_iff_equiv], refine equiv.trans _ nim_add_nim_equiv, convert add_congr (equiv_nim_grundy_value G) (equiv_nim_grundy_value H); simp only [hG, hH]